%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KRS157+1 : TPTP v8.1.2. Released v3.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n001.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 : Thu Aug 31 05:51:28 EDT 2023 % Result : Theorem 18.17s 3.20s % Output : Proof 29.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : KRS157+1 : TPTP v8.1.2. Released v3.1.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n001.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Aug 28 02:37:34 EDT 2023 % 0.13/0.35 % CPUTime : % 0.21/0.61 ________ _____ % 0.21/0.61 ___ __ \_________(_)________________________________ % 0.21/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.61 % 0.21/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.61 (2023-06-19) % 0.21/0.61 % 0.21/0.61 (c) Philipp Rümmer, 2009-2023 % 0.21/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.61 Amanda Stjerna. % 0.21/0.61 Free software under BSD-3-Clause. % 0.21/0.61 % 0.21/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.61 % 0.21/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.64 Running up to 7 provers in parallel. % 0.21/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.52/1.46 Prover 4: Preprocessing ... % 5.44/1.49 Prover 1: Preprocessing ... % 5.44/1.51 Prover 3: Preprocessing ... % 5.44/1.51 Prover 2: Preprocessing ... % 5.44/1.52 Prover 0: Preprocessing ... % 5.44/1.52 Prover 5: Preprocessing ... % 5.44/1.52 Prover 6: Preprocessing ... % 14.08/2.66 Prover 2: Proving ... % 14.08/2.68 Prover 5: Proving ... % 18.17/3.18 Prover 6: Proving ... % 18.17/3.20 Prover 2: proved (2552ms) % 18.17/3.20 % 18.17/3.20 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.17/3.20 % 18.17/3.20 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.17/3.20 Prover 5: stopped % 18.17/3.20 Prover 6: stopped % 18.17/3.21 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 18.50/3.23 Prover 1: Constructing countermodel ... % 18.50/3.23 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 18.66/3.29 Prover 3: Constructing countermodel ... % 18.66/3.32 Prover 3: stopped % 18.66/3.34 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 19.37/3.45 Prover 7: Preprocessing ... % 19.37/3.46 Prover 8: Preprocessing ... % 19.37/3.47 Prover 10: Preprocessing ... % 20.47/3.54 Prover 4: Constructing countermodel ... % 21.84/3.68 Prover 11: Preprocessing ... % 22.15/3.78 Prover 7: Warning: ignoring some quantifiers % 22.77/3.81 Prover 10: Warning: ignoring some quantifiers % 22.77/3.82 Prover 7: Constructing countermodel ... % 22.77/3.82 Prover 0: Proving ... % 22.77/3.83 Prover 0: stopped % 22.77/3.84 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 22.77/3.86 Prover 10: Constructing countermodel ... % 23.37/3.97 Prover 13: Preprocessing ... % 26.95/4.41 Prover 13: Warning: ignoring some quantifiers % 27.42/4.44 Prover 13: Constructing countermodel ... % 27.76/4.46 Prover 8: Warning: ignoring some quantifiers % 27.76/4.51 Prover 8: Constructing countermodel ... % 27.76/4.51 Prover 1: Found proof (size 238) % 27.76/4.51 Prover 1: proved (3867ms) % 27.76/4.51 Prover 4: stopped % 27.76/4.51 Prover 13: stopped % 27.76/4.51 Prover 7: stopped % 27.76/4.52 Prover 10: stopped % 27.76/4.52 Prover 8: stopped % 28.67/4.65 Prover 11: Constructing countermodel ... % 28.67/4.65 Prover 11: stopped % 28.67/4.65 % 28.67/4.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.67/4.66 % 28.67/4.67 % SZS output start Proof for theBenchmark % 28.67/4.68 Assumptions after simplification: % 28.67/4.68 --------------------------------- % 28.67/4.68 % 28.67/4.68 (axiom_0) % 28.67/4.70 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ $i(v0)) & % 28.67/4.70 ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 28.67/4.70 % 28.67/4.70 (axiom_1) % 28.67/4.71 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ $i(v0) | % 28.67/4.71 xsd_integer(v0) = 0) & ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | % 28.67/4.71 ? [v1: int] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) % 28.67/4.71 % 28.67/4.71 (axiom_121) % 28.67/4.71 ! [v0: $i] : ! [v1: any] : ( ~ (cC64(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 28.67/4.71 ? [v3: any] : (cC216(v0) = v2 & cC214xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 % 28.67/4.71 & v1 = 0)))) & ! [v0: $i] : ( ~ (cC64(v0) = 0) | ~ $i(v0) | ? [v1: % 28.67/4.71 any] : ? [v2: any] : (cC216(v0) = v2 & cC214xcomp(v0) = v1 & ( ~ (v1 = 0) % 28.67/4.71 | v2 = 0))) % 28.67/4.71 % 28.67/4.71 (axiom_131) % 28.67/4.71 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC28(v0) = v1) | ~ $i(v0) | ? % 28.67/4.71 [v2: any] : ? [v3: any] : (cC26xcomp(v0) = v3 & cC16xcomp(v0) = v2 & ( ~ % 28.67/4.71 (v3 = 0) | ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC28(v0) = 0) | ~ $i(v0) % 28.67/4.71 | (cC26xcomp(v0) = 0 & cC16xcomp(v0) = 0)) % 28.67/4.71 % 28.67/4.71 (axiom_132) % 28.67/4.71 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC30(v0) = v1) | ~ $i(v0) | ? % 28.67/4.71 [v2: any] : ? [v3: any] : (cC28(v0) = v2 & cC14(v0) = v3 & ( ~ (v3 = 0) | % 28.67/4.71 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC30(v0) = 0) | ~ $i(v0) | (cC28(v0) % 28.67/4.71 = 0 & cC14(v0) = 0)) % 28.67/4.71 % 28.67/4.71 (axiom_147) % 28.67/4.72 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC44(v0) = v1) | ~ $i(v0) | ? % 28.67/4.72 [v2: any] : ? [v3: any] : (cC42xcomp(v0) = v2 & cC32xcomp(v0) = v3 & ( ~ % 28.67/4.72 (v3 = 0) | ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC44(v0) = 0) | ~ $i(v0) % 28.67/4.72 | (cC42xcomp(v0) = 0 & cC32xcomp(v0) = 0)) % 28.67/4.72 % 28.67/4.72 (axiom_148) % 28.67/4.72 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC46(v0) = v1) | ~ $i(v0) | ? % 28.67/4.72 [v2: any] : ? [v3: any] : (cC44(v0) = v3 & cC30(v0) = v2 & ( ~ (v3 = 0) | % 28.67/4.72 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC46(v0) = 0) | ~ $i(v0) | (cC44(v0) % 28.67/4.72 = 0 & cC30(v0) = 0)) % 28.67/4.72 % 28.67/4.72 (axiom_166) % 28.67/4.72 ! [v0: $i] : ! [v1: any] : ( ~ (cTOP(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 28.67/4.72 ? [v3: any] : (cC62xcomp(v0) = v3 & cC64(v0) = v2 & ( ~ (v2 = 0) | (v3 = 0 & % 28.67/4.72 v1 = 0)))) & ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: % 28.67/4.72 any] : ? [v2: any] : (cC62xcomp(v0) = v1 & cC64(v0) = v2 & ( ~ (v1 = 0) | % 28.67/4.72 v2 = 0))) % 28.67/4.72 % 28.67/4.72 (axiom_201) % 28.67/4.72 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cTEST(v0) = v1) | ~ $i(v0) | ? % 28.67/4.72 [v2: any] : ? [v3: any] : (cC46(v0) = v3 & cC216(v0) = v2 & ( ~ (v3 = 0) | % 28.67/4.72 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | % 28.67/4.72 (cC46(v0) = 0 & cC216(v0) = 0)) % 28.67/4.72 % 28.67/4.72 (axiom_202) % 28.67/4.72 cTEST(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_203) % 28.67/4.72 cC2xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_205) % 28.67/4.72 cTOP(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_206) % 28.67/4.72 cC26xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_207) % 28.67/4.72 cC32xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_210) % 28.67/4.72 cC16xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_211) % 28.67/4.72 cC42xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_212) % 28.67/4.72 cC62xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_215) % 28.67/4.72 cC12xcomp(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_217) % 28.67/4.72 cowlThing(iV3102) = 0 & $i(iV3102) % 28.67/4.72 % 28.67/4.72 (axiom_44) % 28.67/4.72 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC14(v0) = v1) | ~ $i(v0) | ? % 28.67/4.72 [v2: any] : ? [v3: any] : (cC12xcomp(v0) = v3 & cC2xcomp(v0) = v2 & ( ~ (v3 % 28.67/4.72 = 0) | ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC14(v0) = 0) | ~ $i(v0) | % 28.67/4.72 (cC12xcomp(v0) = 0 & cC2xcomp(v0) = 0)) % 28.67/4.72 % 28.67/4.72 (the_axiom) % 28.67/4.73 $i(iV3102) & ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 28.67/4.73 [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : (cC46(iV3102) = v4 & % 28.67/4.73 cC44(iV3102) = v1 & cC30(iV3102) = v7 & cC28(iV3102) = v5 & cC64(iV3102) = % 28.67/4.73 v3 & cC216(iV3102) = v2 & cC14(iV3102) = v0 & cowlThing(iV3102) = v6 & ( ~ % 28.67/4.73 (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 % 28.67/4.73 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | ? [v8: $i] : ? [v9: any] : ? [v10: % 28.67/4.73 any] : (xsd_string(v8) = v9 & xsd_integer(v8) = v10 & $i(v8) & ((v10 = 0 % 28.67/4.73 & v9 = 0) | ( ~ (v10 = 0) & ~ (v9 = 0)))) | ? [v8: $i] : ? [v9: % 28.67/4.73 any] : ? [v10: any] : (cowlNothing(v8) = v10 & cowlThing(v8) = v9 & % 28.67/4.73 $i(v8) & ( ~ (v9 = 0) | v10 = 0)))) % 28.67/4.73 % 28.67/4.73 (function-axioms) % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 28.67/4.77 [v3: $i] : (v1 = v0 | ~ (ra_Px34(v3, v2) = v1) | ~ (ra_Px34(v3, v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 28.67/4.77 [v3: $i] : (v1 = v0 | ~ (ra_Px32(v3, v2) = v1) | ~ (ra_Px32(v3, v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 28.67/4.77 [v3: $i] : (v1 = v0 | ~ (ra_Px30(v3, v2) = v1) | ~ (ra_Px30(v3, v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 28.67/4.77 [v3: $i] : (v1 = v0 | ~ (ra_Px29(v3, v2) = v1) | ~ (ra_Px29(v3, v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 28.67/4.77 [v3: $i] : (v1 = v0 | ~ (ra_Px2(v3, v2) = v1) | ~ (ra_Px2(v3, v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px26(v3, v2) = v1) | ~ (ra_Px26(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px31(v3, v2) = v1) | ~ (ra_Px31(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px23(v3, v2) = v1) | ~ (ra_Px23(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px20(v3, v2) = v1) | ~ (ra_Px20(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px85(v3, v2) = v1) | ~ (ra_Px85(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px19(v3, v2) = v1) | ~ (ra_Px19(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px18(v3, v2) = v1) | ~ (ra_Px18(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px14(v3, v2) = v1) | ~ (ra_Px14(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px86(v3, v2) = v1) | ~ (ra_Px86(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px12(v3, v2) = v1) | ~ (ra_Px12(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px10(v3, v2) = v1) | ~ (ra_Px10(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px9(v3, v2) = v1) | ~ (ra_Px9(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px88(v3, v2) = v1) | ~ (ra_Px88(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px7(v3, v2) = v1) | ~ (ra_Px7(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px75(v3, v2) = v1) | ~ (ra_Px75(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px74(v3, v2) = v1) | ~ (ra_Px74(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px73(v3, v2) = v1) | ~ (ra_Px73(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px71(v3, v2) = v1) | ~ (ra_Px71(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px69(v3, v2) = v1) | ~ (ra_Px69(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px1(v3, v2) = v1) | ~ (ra_Px1(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px68(v3, v2) = v1) | ~ (ra_Px68(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px65(v3, v2) = v1) | ~ (ra_Px65(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px70(v3, v2) = v1) | ~ (ra_Px70(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px62(v3, v2) = v1) | ~ (ra_Px62(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px59(v3, v2) = v1) | ~ (ra_Px59(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px58(v3, v2) = v1) | ~ (ra_Px58(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px56(v3, v2) = v1) | ~ (ra_Px56(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px55(v3, v2) = v1) | ~ (ra_Px55(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px5(v3, v2) = v1) | ~ (ra_Px5(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px52(v3, v2) = v1) | ~ (ra_Px52(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px57(v3, v2) = v1) | ~ (ra_Px57(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px49(v3, v2) = v1) | ~ (ra_Px49(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px72(v3, v2) = v1) | ~ (ra_Px72(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px46(v3, v2) = v1) | ~ (ra_Px46(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px44(v3, v2) = v1) | ~ (ra_Px44(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px43(v3, v2) = v1) | ~ (ra_Px43(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px4(v3, v2) = v1) | ~ (ra_Px4(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px40(v3, v2) = v1) | ~ (ra_Px40(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px45(v3, v2) = v1) | ~ (ra_Px45(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px37(v3, v2) = v1) | ~ (ra_Px37(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (ra_Px76(v3, v2) = v1) | ~ (ra_Px76(v3, v2) = v0)) & ! % 28.67/4.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.67/4.77 $i] : (v1 = v0 | ~ (rR1(v3, v2) = v1) | ~ (rR1(v3, v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 28.67/4.77 : (v1 = v0 | ~ (ra_Px87(v3, v2) = v1) | ~ (ra_Px87(v3, v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC98(v2) = v1) | ~ % 28.67/4.77 (cC98(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC96xcomp(v2) = v1) | ~ (cC96xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC96(v2) = v1) | ~ (cC96(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC94xcomp(v2) = v1) % 28.67/4.77 | ~ (cC94xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC94(v2) = v1) | ~ % 28.67/4.77 (cC94(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC92(v2) = v1) | ~ (cC92(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC90xcomp(v2) = v1) | ~ (cC90xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC90(v2) = v1) | ~ (cC90(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC88(v2) = v1) | ~ % 28.67/4.77 (cC88(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC86(v2) = v1) | ~ (cC86(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC84(v2) = v1) | ~ (cC84(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC82(v2) = v1) | ~ % 28.67/4.77 (cC82(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC80(v2) = v1) | ~ (cC80(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC8(v2) = v1) | ~ (cC8(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC78xcomp(v2) = v1) | ~ % 28.67/4.77 (cC78xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC78(v2) = v1) | ~ % 28.67/4.77 (cC78(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC76(v2) = v1) | ~ (cC76(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC74(v2) = v1) | ~ (cC74(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC72xcomp(v2) = v1) | % 28.67/4.77 ~ (cC72xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC72(v2) = v1) | ~ % 28.67/4.77 (cC72(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC70xcomp(v2) = v1) | ~ (cC70xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC70(v2) = v1) | ~ (cC70(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC68(v2) = v1) | ~ % 28.67/4.77 (cC68(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC66(v2) = v1) | ~ (cC66(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cTOP(v2) = v1) | ~ (cTOP(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC62xcomp(v2) = v1) | % 28.67/4.77 ~ (cC62xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC62(v2) = v1) | ~ % 28.67/4.77 (cC62(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC60xcomp(v2) = v1) | ~ (cC60xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC60(v2) = v1) | ~ (cC60(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC6(v2) = v1) | ~ % 28.67/4.77 (cC6(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC58xcomp(v2) = v1) | ~ (cC58xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC58(v2) = v1) | ~ (cC58(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC56(v2) = v1) | ~ % 28.67/4.77 (cC56(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC54xcomp(v2) = v1) | ~ (cC54xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC54(v2) = v1) | ~ (cC54(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC52(v2) = v1) | ~ % 28.67/4.77 (cC52(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC50(v2) = v1) | ~ (cC50(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC48(v2) = v1) | ~ (cC48(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC46(v2) = v1) | ~ % 28.67/4.77 (cC46(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC44(v2) = v1) | ~ (cC44(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC42xcomp(v2) = v1) | ~ (cC42xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC42(v2) = v1) | ~ (cC42(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC40xcomp(v2) = v1) | % 28.67/4.77 ~ (cC40xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC40(v2) = v1) | ~ % 28.67/4.77 (cC40(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC38xcomp(v2) = v1) | ~ (cC38xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC38(v2) = v1) | ~ (cC38(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC36(v2) = v1) | ~ % 28.67/4.77 (cC36(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC34(v2) = v1) | ~ (cC34(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC32xcomp(v2) = v1) | ~ (cC32xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC32(v2) = v1) | ~ (cC32(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC30(v2) = v1) | ~ % 28.67/4.77 (cC30(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC28(v2) = v1) | ~ (cC28(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC26xcomp(v2) = v1) | ~ (cC26xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC26(v2) = v1) | ~ (cC26(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.77 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC24xcomp(v2) = v1) | % 28.67/4.77 ~ (cC24xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC24(v2) = v1) | ~ % 28.67/4.77 (cC24(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC22xcomp(v2) = v1) | ~ (cC22xcomp(v2) = v0)) & % 28.67/4.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 28.67/4.77 v0 | ~ (cC22(v2) = v1) | ~ (cC22(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.77 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC64(v2) = v1) | ~ % 28.67/4.77 (cC64(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.77 ! [v2: $i] : (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC214xcomp(v2) = v1) | ~ (cC214xcomp(v2) = v0)) & ! [v0: % 28.67/4.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.77 ~ (cC214(v2) = v1) | ~ (cC214(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC212xcomp(v2) = v1) | % 28.67/4.78 ~ (cC212xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC212(v2) = v1) | ~ % 28.67/4.78 (cC212(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC210(v2) = v1) | ~ (cC210(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC208xcomp(v2) = v1) | ~ (cC208xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC208(v2) = v1) | ~ (cC208(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC206(v2) = v1) | ~ % 28.67/4.78 (cC206(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC204(v2) = v1) | ~ (cC204(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC202xcomp(v2) = v1) | ~ (cC202xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC202(v2) = v1) | ~ (cC202(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC200xcomp(v2) = v1) | % 28.67/4.78 ~ (cC200xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC200(v2) = v1) | ~ % 28.67/4.78 (cC200(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC20(v2) = v1) | ~ (cC20(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC198(v2) = v1) | ~ % 28.67/4.78 (cC198(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC196xcomp(v2) = v1) | ~ (cC196xcomp(v2) = % 28.67/4.78 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 28.67/4.78 $i] : (v1 = v0 | ~ (cC196(v2) = v1) | ~ (cC196(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC194(v2) = v1) | ~ (cC194(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC192(v2) = v1) | ~ % 28.67/4.78 (cC192(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC190(v2) = v1) | ~ (cC190(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC188(v2) = v1) | ~ (cC188(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.78 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC186(v2) = v1) | ~ % 28.67/4.78 (cC186(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC184xcomp(v2) = v1) | ~ (cC184xcomp(v2) = % 28.67/4.78 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 28.67/4.78 $i] : (v1 = v0 | ~ (cC184(v2) = v1) | ~ (cC184(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC182(v2) = v1) | ~ (cC182(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC180(v2) = v1) | ~ % 28.67/4.78 (cC180(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC178xcomp(v2) = v1) | ~ (cC178xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC178(v2) = v1) | ~ (cC178(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC176xcomp(v2) = v1) | % 28.67/4.78 ~ (cC176xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC176(v2) = v1) | ~ % 28.67/4.78 (cC176(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC174(v2) = v1) | ~ (cC174(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC172(v2) = v1) | ~ (cC172(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.78 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC170(v2) = v1) | ~ % 28.67/4.78 (cC170(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC168xcomp(v2) = v1) | ~ (cC168xcomp(v2) = % 28.67/4.78 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 28.67/4.78 $i] : (v1 = v0 | ~ (cC168(v2) = v1) | ~ (cC168(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC166xcomp(v2) = v1) | ~ (cC166xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC166(v2) = v1) | ~ (cC166(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC164xcomp(v2) = v1) | % 28.67/4.78 ~ (cC164xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC164(v2) = v1) | ~ % 28.67/4.78 (cC164(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC162(v2) = v1) | ~ (cC162(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC160xcomp(v2) = v1) | ~ (cC160xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC160(v2) = v1) | ~ (cC160(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC158(v2) = v1) | ~ % 28.67/4.78 (cC158(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC156(v2) = v1) | ~ (cC156(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC154(v2) = v1) | ~ (cC154(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.78 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC152(v2) = v1) | ~ % 28.67/4.78 (cC152(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC150(v2) = v1) | ~ (cC150(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC148xcomp(v2) = v1) | ~ (cC148xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC148(v2) = v1) | ~ (cC148(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC146(v2) = v1) | ~ % 28.67/4.78 (cC146(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC144(v2) = v1) | ~ (cC144(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC142xcomp(v2) = v1) | ~ (cC142xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC142(v2) = v1) | ~ (cC142(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC140xcomp(v2) = v1) | % 28.67/4.78 ~ (cC140xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC140(v2) = v1) | ~ % 28.67/4.78 (cC140(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC138(v2) = v1) | ~ (cC138(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC136(v2) = v1) | ~ % 28.67/4.78 (cC136(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC134xcomp(v2) = v1) | ~ (cC134xcomp(v2) = % 28.67/4.78 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 28.67/4.78 $i] : (v1 = v0 | ~ (cC134(v2) = v1) | ~ (cC134(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC132xcomp(v2) = v1) | ~ (cC132xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC132(v2) = v1) | ~ (cC132(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC130xcomp(v2) = v1) | % 28.67/4.78 ~ (cC130xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC130(v2) = v1) | ~ % 28.67/4.78 (cC130(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC128(v2) = v1) | ~ (cC128(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC126xcomp(v2) = v1) | ~ (cC126xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC126(v2) = v1) | ~ (cC126(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC124(v2) = v1) | ~ % 28.67/4.78 (cC124(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC122(v2) = v1) | ~ (cC122(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC120(v2) = v1) | ~ (cC120(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.78 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC12xcomp(v2) = v1) | % 28.67/4.78 ~ (cC12xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC12(v2) = v1) | ~ % 28.67/4.78 (cC12(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.78 ! [v2: $i] : (v1 = v0 | ~ (cC118(v2) = v1) | ~ (cC118(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC116(v2) = v1) | ~ (cC116(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC114xcomp(v2) = v1) | % 28.67/4.78 ~ (cC114xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC114(v2) = v1) | ~ % 28.67/4.78 (cC114(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC112(v2) = v1) | ~ (cC112(v2) = v0)) & ! % 28.67/4.78 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 28.67/4.78 | ~ (cC110(v2) = v1) | ~ (cC110(v2) = v0)) & ! [v0: MultipleValueBool] : % 28.67/4.78 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC108xcomp(v2) = v1) % 28.67/4.78 | ~ (cC108xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC108(v2) = v1) | ~ % 28.67/4.78 (cC108(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 28.67/4.78 : ! [v2: $i] : (v1 = v0 | ~ (cC106xcomp(v2) = v1) | ~ (cC106xcomp(v2) = % 28.67/4.78 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 28.67/4.78 $i] : (v1 = v0 | ~ (cC106(v2) = v1) | ~ (cC106(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC104(v2) = v1) | ~ (cC104(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC16(v2) = v1) | ~ % 28.67/4.78 (cC16(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.78 ! [v2: $i] : (v1 = v0 | ~ (cC102(v2) = v1) | ~ (cC102(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC16xcomp(v2) = v1) | ~ (cC16xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC100xcomp(v2) = v1) | ~ (cC100xcomp(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cC100(v2) = v1) | ~ (cC100(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 28.67/4.78 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC98xcomp(v2) = v1) | % 28.67/4.78 ~ (cC98xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC10xcomp(v2) = v1) | ~ % 28.67/4.78 (cC10xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC8xcomp(v2) = v1) | ~ % 28.67/4.78 (cC8xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC2xcomp(v2) = v1) | ~ % 28.67/4.78 (cC2xcomp(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.67/4.78 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC10(v2) = v1) | ~ % 28.67/4.78 (cC10(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 28.67/4.78 ! [v2: $i] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) % 28.67/4.78 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 28.67/4.78 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) & ! [v0: % 28.67/4.78 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 28.67/4.78 ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 28.67/4.78 % 28.67/4.78 Further assumptions not needed in the proof: % 28.67/4.78 -------------------------------------------- % 28.67/4.78 axiom_10, axiom_100, axiom_101, axiom_102, axiom_103, axiom_104, axiom_105, % 28.67/4.78 axiom_106, axiom_107, axiom_108, axiom_109, axiom_11, axiom_110, axiom_111, % 28.67/4.78 axiom_112, axiom_113, axiom_114, axiom_115, axiom_116, axiom_117, axiom_118, % 28.67/4.78 axiom_119, axiom_12, axiom_120, axiom_122, axiom_123, axiom_124, axiom_125, % 28.67/4.78 axiom_126, axiom_127, axiom_128, axiom_129, axiom_13, axiom_130, axiom_133, % 28.67/4.78 axiom_134, axiom_135, axiom_136, axiom_137, axiom_138, axiom_139, axiom_14, % 28.67/4.78 axiom_140, axiom_141, axiom_142, axiom_143, axiom_144, axiom_145, axiom_146, % 28.67/4.78 axiom_149, axiom_15, axiom_150, axiom_151, axiom_152, axiom_153, axiom_154, % 28.67/4.78 axiom_155, axiom_156, axiom_157, axiom_158, axiom_159, axiom_16, axiom_160, % 28.67/4.78 axiom_161, axiom_162, axiom_163, axiom_164, axiom_165, axiom_167, axiom_168, % 28.67/4.78 axiom_169, axiom_17, axiom_170, axiom_171, axiom_172, axiom_173, axiom_174, % 28.67/4.78 axiom_175, axiom_176, axiom_177, axiom_178, axiom_179, axiom_18, axiom_180, % 28.67/4.78 axiom_181, axiom_182, axiom_183, axiom_184, axiom_185, axiom_186, axiom_187, % 28.67/4.78 axiom_188, axiom_189, axiom_19, axiom_190, axiom_191, axiom_192, axiom_193, % 28.67/4.78 axiom_194, axiom_195, axiom_196, axiom_197, axiom_198, axiom_199, axiom_2, % 28.67/4.78 axiom_20, axiom_200, axiom_204, axiom_208, axiom_209, axiom_21, axiom_213, % 28.67/4.78 axiom_214, axiom_216, axiom_218, axiom_22, axiom_23, axiom_24, axiom_25, % 28.67/4.78 axiom_26, axiom_27, axiom_28, axiom_29, axiom_3, axiom_30, axiom_31, axiom_32, % 28.67/4.78 axiom_33, axiom_34, axiom_35, axiom_36, axiom_37, axiom_38, axiom_39, axiom_4, % 28.67/4.78 axiom_40, axiom_41, axiom_42, axiom_43, axiom_45, axiom_46, axiom_47, axiom_48, % 28.67/4.78 axiom_49, axiom_5, axiom_50, axiom_51, axiom_52, axiom_53, axiom_54, axiom_55, % 28.67/4.78 axiom_56, axiom_57, axiom_58, axiom_59, axiom_6, axiom_60, axiom_61, axiom_62, % 28.67/4.78 axiom_63, axiom_64, axiom_65, axiom_66, axiom_67, axiom_68, axiom_69, axiom_7, % 28.67/4.78 axiom_70, axiom_71, axiom_72, axiom_73, axiom_74, axiom_75, axiom_76, axiom_77, % 28.67/4.78 axiom_78, axiom_79, axiom_8, axiom_80, axiom_81, axiom_82, axiom_83, axiom_84, % 28.67/4.78 axiom_85, axiom_86, axiom_87, axiom_88, axiom_89, axiom_9, axiom_90, axiom_91, % 28.67/4.78 axiom_92, axiom_93, axiom_94, axiom_95, axiom_96, axiom_97, axiom_98, axiom_99 % 28.67/4.78 % 28.67/4.78 Those formulas are unsatisfiable: % 28.67/4.78 --------------------------------- % 28.67/4.78 % 28.67/4.78 Begin of proof % 28.67/4.78 | % 28.67/4.78 | ALPHA: (axiom_0) implies: % 28.67/4.78 | (1) ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 28.67/4.78 | (2) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ % 28.67/4.78 | $i(v0)) % 28.67/4.78 | % 28.67/4.78 | ALPHA: (axiom_1) implies: % 28.67/4.78 | (3) ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ % 28.67/4.78 | (v1 = 0) & xsd_integer(v0) = v1)) % 28.67/4.79 | (4) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ % 28.67/4.79 | $i(v0) | xsd_integer(v0) = 0) % 28.67/4.79 | % 28.67/4.79 | ALPHA: (axiom_44) implies: % 28.86/4.79 | (5) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC14(v0) = v1) | ~ $i(v0) | % 28.86/4.79 | ? [v2: any] : ? [v3: any] : (cC12xcomp(v0) = v3 & cC2xcomp(v0) = v2 % 28.86/4.79 | & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_121) implies: % 28.86/4.79 | (6) ! [v0: $i] : ! [v1: any] : ( ~ (cC64(v0) = v1) | ~ $i(v0) | ? [v2: % 28.86/4.79 | any] : ? [v3: any] : (cC216(v0) = v2 & cC214xcomp(v0) = v3 & ( ~ % 28.86/4.79 | (v2 = 0) | (v3 = 0 & v1 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_131) implies: % 28.86/4.79 | (7) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC28(v0) = v1) | ~ $i(v0) | % 28.86/4.79 | ? [v2: any] : ? [v3: any] : (cC26xcomp(v0) = v3 & cC16xcomp(v0) = % 28.86/4.79 | v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_132) implies: % 28.86/4.79 | (8) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC30(v0) = v1) | ~ $i(v0) | % 28.86/4.79 | ? [v2: any] : ? [v3: any] : (cC28(v0) = v2 & cC14(v0) = v3 & ( ~ % 28.86/4.79 | (v3 = 0) | ~ (v2 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_147) implies: % 28.86/4.79 | (9) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC44(v0) = v1) | ~ $i(v0) | % 28.86/4.79 | ? [v2: any] : ? [v3: any] : (cC42xcomp(v0) = v2 & cC32xcomp(v0) = % 28.86/4.79 | v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_148) implies: % 28.86/4.79 | (10) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC46(v0) = v1) | ~ $i(v0) % 28.86/4.79 | | ? [v2: any] : ? [v3: any] : (cC44(v0) = v3 & cC30(v0) = v2 & ( ~ % 28.86/4.79 | (v3 = 0) | ~ (v2 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_166) implies: % 28.86/4.79 | (11) ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? [v2: % 28.86/4.79 | any] : (cC62xcomp(v0) = v1 & cC64(v0) = v2 & ( ~ (v1 = 0) | v2 = % 28.86/4.79 | 0))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_201) implies: % 28.86/4.79 | (12) ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | (cC46(v0) = 0 & % 28.86/4.79 | cC216(v0) = 0)) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_202) implies: % 28.86/4.79 | (13) cTEST(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_203) implies: % 28.86/4.79 | (14) cC2xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_205) implies: % 28.86/4.79 | (15) cTOP(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_206) implies: % 28.86/4.79 | (16) cC26xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_207) implies: % 28.86/4.79 | (17) cC32xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_210) implies: % 28.86/4.79 | (18) cC16xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_211) implies: % 28.86/4.79 | (19) cC42xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_212) implies: % 28.86/4.79 | (20) cC62xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_215) implies: % 28.86/4.79 | (21) cC12xcomp(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (axiom_217) implies: % 28.86/4.79 | (22) cowlThing(iV3102) = 0 % 28.86/4.79 | % 28.86/4.79 | ALPHA: (the_axiom) implies: % 28.86/4.79 | (23) $i(iV3102) % 28.86/4.79 | (24) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 28.86/4.79 | any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : (cC46(iV3102) = % 28.86/4.79 | v4 & cC44(iV3102) = v1 & cC30(iV3102) = v7 & cC28(iV3102) = v5 & % 28.86/4.79 | cC64(iV3102) = v3 & cC216(iV3102) = v2 & cC14(iV3102) = v0 & % 28.86/4.79 | cowlThing(iV3102) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | % 28.86/4.79 | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 28.86/4.79 | | ? [v8: $i] : ? [v9: any] : ? [v10: any] : (xsd_string(v8) = % 28.86/4.79 | v9 & xsd_integer(v8) = v10 & $i(v8) & ((v10 = 0 & v9 = 0) | ( ~ % 28.86/4.79 | (v10 = 0) & ~ (v9 = 0)))) | ? [v8: $i] : ? [v9: any] : ? % 28.86/4.79 | [v10: any] : (cowlNothing(v8) = v10 & cowlThing(v8) = v9 & $i(v8) % 28.86/4.79 | & ( ~ (v9 = 0) | v10 = 0)))) % 28.86/4.79 | % 28.86/4.79 | ALPHA: (function-axioms) implies: % 28.86/4.80 | (25) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 28.86/4.80 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 28.86/4.80 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC2xcomp(v2) = v1) | ~ (cC2xcomp(v2) = v0)) % 28.86/4.80 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC16xcomp(v2) = v1) | ~ (cC16xcomp(v2) = v0)) % 28.86/4.80 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC12xcomp(v2) = v1) | ~ (cC12xcomp(v2) = v0)) % 28.86/4.80 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) % 28.86/4.80 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) % 28.86/4.80 | (32) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) % 28.86/4.80 | (33) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC26xcomp(v2) = v1) | ~ (cC26xcomp(v2) = v0)) % 28.86/4.80 | (34) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC28(v2) = v1) | ~ (cC28(v2) = v0)) % 28.86/4.80 | (35) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC32xcomp(v2) = v1) | ~ (cC32xcomp(v2) = v0)) % 28.86/4.80 | (36) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC42xcomp(v2) = v1) | ~ (cC42xcomp(v2) = v0)) % 28.86/4.80 | (37) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC46(v2) = v1) | ~ (cC46(v2) = v0)) % 28.86/4.80 | (38) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.86/4.80 | : (v1 = v0 | ~ (cC62xcomp(v2) = v1) | ~ (cC62xcomp(v2) = v0)) % 28.86/4.80 | % 28.86/4.80 | DELTA: instantiating (24) with fresh symbols all_211_0, all_211_1, all_211_2, % 28.86/4.80 | all_211_3, all_211_4, all_211_5, all_211_6, all_211_7 gives: % 28.86/4.80 | (39) cC46(iV3102) = all_211_3 & cC44(iV3102) = all_211_6 & cC30(iV3102) = % 28.86/4.80 | all_211_0 & cC28(iV3102) = all_211_2 & cC64(iV3102) = all_211_4 & % 28.86/4.80 | cC216(iV3102) = all_211_5 & cC14(iV3102) = all_211_7 & % 28.86/4.80 | cowlThing(iV3102) = all_211_1 & ( ~ (all_211_0 = 0) | ~ (all_211_1 = % 28.86/4.80 | 0) | ~ (all_211_2 = 0) | ~ (all_211_3 = 0) | ~ (all_211_4 = 0) % 28.86/4.80 | | ~ (all_211_5 = 0) | ~ (all_211_6 = 0) | ~ (all_211_7 = 0) | ? % 28.86/4.80 | [v0: $i] : ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 28.86/4.80 | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) % 28.86/4.80 | & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.80 | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | % 28.86/4.80 | v2 = 0))) % 28.86/4.80 | % 28.86/4.80 | ALPHA: (39) implies: % 28.86/4.80 | (40) cowlThing(iV3102) = all_211_1 % 28.86/4.80 | (41) cC14(iV3102) = all_211_7 % 28.86/4.80 | (42) cC216(iV3102) = all_211_5 % 28.86/4.80 | (43) cC64(iV3102) = all_211_4 % 28.86/4.80 | (44) cC28(iV3102) = all_211_2 % 28.86/4.80 | (45) cC30(iV3102) = all_211_0 % 28.86/4.80 | (46) cC44(iV3102) = all_211_6 % 28.86/4.80 | (47) cC46(iV3102) = all_211_3 % 28.86/4.80 | (48) ~ (all_211_0 = 0) | ~ (all_211_1 = 0) | ~ (all_211_2 = 0) | ~ % 28.86/4.80 | (all_211_3 = 0) | ~ (all_211_4 = 0) | ~ (all_211_5 = 0) | ~ % 28.86/4.80 | (all_211_6 = 0) | ~ (all_211_7 = 0) | ? [v0: $i] : ? [v1: any] : ? % 28.86/4.80 | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) & % 28.86/4.80 | ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : % 28.86/4.80 | ? [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = % 28.86/4.80 | v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.80 | % 28.86/4.81 | GROUND_INST: instantiating (25) with 0, all_211_1, iV3102, simplifying with % 28.86/4.81 | (22), (40) gives: % 28.86/4.81 | (49) all_211_1 = 0 % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (5) with iV3102, all_211_7, simplifying with (23), % 28.86/4.81 | (41) gives: % 28.86/4.81 | (50) all_211_7 = 0 | ? [v0: any] : ? [v1: any] : (cC12xcomp(iV3102) = v1 % 28.86/4.81 | & cC2xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (6) with iV3102, all_211_4, simplifying with (23), % 28.86/4.81 | (43) gives: % 28.86/4.81 | (51) ? [v0: any] : ? [v1: any] : (cC216(iV3102) = v0 & cC214xcomp(iV3102) % 28.86/4.81 | = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_211_4 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (7) with iV3102, all_211_2, simplifying with (23), % 28.86/4.81 | (44) gives: % 28.86/4.81 | (52) all_211_2 = 0 | ? [v0: any] : ? [v1: any] : (cC26xcomp(iV3102) = v1 % 28.86/4.81 | & cC16xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (8) with iV3102, all_211_0, simplifying with (23), % 28.86/4.81 | (45) gives: % 28.86/4.81 | (53) all_211_0 = 0 | ? [v0: any] : ? [v1: any] : (cC28(iV3102) = v0 & % 28.86/4.81 | cC14(iV3102) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (9) with iV3102, all_211_6, simplifying with (23), % 28.86/4.81 | (46) gives: % 28.86/4.81 | (54) all_211_6 = 0 | ? [v0: any] : ? [v1: any] : (cC42xcomp(iV3102) = v0 % 28.86/4.81 | & cC32xcomp(iV3102) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (10) with iV3102, all_211_3, simplifying with (23), % 28.86/4.81 | (47) gives: % 28.86/4.81 | (55) all_211_3 = 0 | ? [v0: any] : ? [v1: any] : (cC44(iV3102) = v1 & % 28.86/4.81 | cC30(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (11) with iV3102, simplifying with (15), (23) % 28.86/4.81 | gives: % 28.86/4.81 | (56) ? [v0: any] : ? [v1: any] : (cC62xcomp(iV3102) = v0 & cC64(iV3102) = % 28.86/4.81 | v1 & ( ~ (v0 = 0) | v1 = 0)) % 28.86/4.81 | % 28.86/4.81 | GROUND_INST: instantiating (12) with iV3102, simplifying with (13), (23) % 28.86/4.81 | gives: % 28.86/4.81 | (57) cC46(iV3102) = 0 & cC216(iV3102) = 0 % 28.86/4.81 | % 28.86/4.81 | ALPHA: (57) implies: % 28.86/4.81 | (58) cC216(iV3102) = 0 % 28.86/4.81 | (59) cC46(iV3102) = 0 % 28.86/4.81 | % 28.86/4.81 | DELTA: instantiating (56) with fresh symbols all_236_0, all_236_1 gives: % 28.86/4.81 | (60) cC62xcomp(iV3102) = all_236_1 & cC64(iV3102) = all_236_0 & ( ~ % 28.86/4.81 | (all_236_1 = 0) | all_236_0 = 0) % 28.86/4.81 | % 28.86/4.81 | ALPHA: (60) implies: % 28.86/4.81 | (61) cC64(iV3102) = all_236_0 % 28.86/4.81 | (62) cC62xcomp(iV3102) = all_236_1 % 28.86/4.81 | (63) ~ (all_236_1 = 0) | all_236_0 = 0 % 28.86/4.81 | % 28.86/4.81 | DELTA: instantiating (51) with fresh symbols all_238_0, all_238_1 gives: % 28.86/4.81 | (64) cC216(iV3102) = all_238_1 & cC214xcomp(iV3102) = all_238_0 & ( ~ % 28.86/4.81 | (all_238_1 = 0) | (all_238_0 = 0 & all_211_4 = 0)) % 28.86/4.81 | % 28.86/4.81 | ALPHA: (64) implies: % 28.86/4.81 | (65) cC216(iV3102) = all_238_1 % 28.86/4.81 | % 28.86/4.81 | BETA: splitting (52) gives: % 28.86/4.81 | % 28.86/4.81 | Case 1: % 28.86/4.81 | | % 28.86/4.81 | | (66) all_211_2 = 0 % 28.86/4.81 | | % 28.86/4.81 | | REDUCE: (44), (66) imply: % 28.86/4.81 | | (67) cC28(iV3102) = 0 % 28.86/4.81 | | % 28.86/4.81 | | BETA: splitting (54) gives: % 28.86/4.81 | | % 28.86/4.81 | | Case 1: % 28.86/4.81 | | | % 28.86/4.81 | | | (68) all_211_6 = 0 % 28.86/4.81 | | | % 28.86/4.81 | | | BETA: splitting (50) gives: % 28.86/4.81 | | | % 28.86/4.81 | | | Case 1: % 28.86/4.81 | | | | % 28.86/4.81 | | | | (69) all_211_7 = 0 % 28.86/4.81 | | | | % 28.86/4.81 | | | | REDUCE: (41), (69) imply: % 28.86/4.81 | | | | (70) cC14(iV3102) = 0 % 28.86/4.81 | | | | % 28.86/4.81 | | | | BETA: splitting (53) gives: % 28.86/4.81 | | | | % 28.86/4.81 | | | | Case 1: % 28.86/4.81 | | | | | % 28.86/4.81 | | | | | (71) all_211_0 = 0 % 28.86/4.81 | | | | | % 28.86/4.81 | | | | | BETA: splitting (55) gives: % 28.86/4.81 | | | | | % 28.86/4.81 | | | | | Case 1: % 28.86/4.81 | | | | | | % 28.86/4.81 | | | | | | (72) all_211_3 = 0 % 28.86/4.81 | | | | | | % 28.86/4.81 | | | | | | GROUND_INST: instantiating (31) with all_211_5, all_238_1, iV3102, % 28.86/4.81 | | | | | | simplifying with (42), (65) gives: % 28.86/4.81 | | | | | | (73) all_238_1 = all_211_5 % 28.86/4.81 | | | | | | % 28.86/4.82 | | | | | | REF_CLOSE: (1), (2), (3), (4), (20), (26), (31), (32), (38), (43), % 28.86/4.82 | | | | | | (48), (49), (58), (61), (62), (63), (65), (66), (68), % 28.86/4.82 | | | | | | (69), (71), (72), (73) are inconsistent by sub-proof #1. % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | Case 2: % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | GROUND_INST: instantiating (37) with all_211_3, 0, iV3102, % 28.86/4.82 | | | | | | simplifying with (47), (59) gives: % 28.86/4.82 | | | | | | (74) all_211_3 = 0 % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | GROUND_INST: instantiating (31) with all_211_5, all_238_1, iV3102, % 28.86/4.82 | | | | | | simplifying with (42), (65) gives: % 28.86/4.82 | | | | | | (75) all_238_1 = all_211_5 % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | REF_CLOSE: (1), (2), (3), (4), (20), (26), (31), (32), (38), (43), % 28.86/4.82 | | | | | | (48), (49), (58), (61), (62), (63), (65), (66), (68), % 28.86/4.82 | | | | | | (69), (71), (74), (75) are inconsistent by sub-proof #1. % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | End of split % 28.86/4.82 | | | | | % 28.86/4.82 | | | | Case 2: % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | (76) ? [v0: any] : ? [v1: any] : (cC28(iV3102) = v0 & % 28.86/4.82 | | | | | cC14(iV3102) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | DELTA: instantiating (76) with fresh symbols all_256_0, all_256_1 % 28.86/4.82 | | | | | gives: % 28.86/4.82 | | | | | (77) cC28(iV3102) = all_256_1 & cC14(iV3102) = all_256_0 & ( ~ % 28.86/4.82 | | | | | (all_256_0 = 0) | ~ (all_256_1 = 0)) % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | ALPHA: (77) implies: % 28.86/4.82 | | | | | (78) cC14(iV3102) = all_256_0 % 28.86/4.82 | | | | | (79) cC28(iV3102) = all_256_1 % 28.86/4.82 | | | | | (80) ~ (all_256_0 = 0) | ~ (all_256_1 = 0) % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | GROUND_INST: instantiating (30) with 0, all_256_0, iV3102, simplifying % 28.86/4.82 | | | | | with (70), (78) gives: % 28.86/4.82 | | | | | (81) all_256_0 = 0 % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | GROUND_INST: instantiating (34) with 0, all_256_1, iV3102, simplifying % 28.86/4.82 | | | | | with (67), (79) gives: % 28.86/4.82 | | | | | (82) all_256_1 = 0 % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | BETA: splitting (80) gives: % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | Case 1: % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | (83) ~ (all_256_0 = 0) % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | REDUCE: (81), (83) imply: % 28.86/4.82 | | | | | | (84) $false % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | CLOSE: (84) is inconsistent. % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | Case 2: % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | (85) ~ (all_256_1 = 0) % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | REDUCE: (82), (85) imply: % 28.86/4.82 | | | | | | (86) $false % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | | CLOSE: (86) is inconsistent. % 28.86/4.82 | | | | | | % 28.86/4.82 | | | | | End of split % 28.86/4.82 | | | | | % 28.86/4.82 | | | | End of split % 28.86/4.82 | | | | % 28.86/4.82 | | | Case 2: % 28.86/4.82 | | | | % 28.86/4.82 | | | | (87) ? [v0: any] : ? [v1: any] : (cC12xcomp(iV3102) = v1 & % 28.86/4.82 | | | | cC2xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.82 | | | | % 28.86/4.82 | | | | DELTA: instantiating (87) with fresh symbols all_252_0, all_252_1 gives: % 28.86/4.82 | | | | (88) cC12xcomp(iV3102) = all_252_0 & cC2xcomp(iV3102) = all_252_1 & ( % 28.86/4.82 | | | | ~ (all_252_0 = 0) | ~ (all_252_1 = 0)) % 28.86/4.82 | | | | % 28.86/4.82 | | | | ALPHA: (88) implies: % 28.86/4.82 | | | | (89) cC2xcomp(iV3102) = all_252_1 % 28.86/4.82 | | | | (90) cC12xcomp(iV3102) = all_252_0 % 28.86/4.82 | | | | (91) ~ (all_252_0 = 0) | ~ (all_252_1 = 0) % 28.86/4.82 | | | | % 28.86/4.82 | | | | GROUND_INST: instantiating (27) with 0, all_252_1, iV3102, simplifying % 28.86/4.82 | | | | with (14), (89) gives: % 28.86/4.82 | | | | (92) all_252_1 = 0 % 28.86/4.82 | | | | % 28.86/4.82 | | | | GROUND_INST: instantiating (29) with 0, all_252_0, iV3102, simplifying % 28.86/4.82 | | | | with (21), (90) gives: % 28.86/4.82 | | | | (93) all_252_0 = 0 % 28.86/4.82 | | | | % 28.86/4.82 | | | | BETA: splitting (91) gives: % 28.86/4.82 | | | | % 28.86/4.82 | | | | Case 1: % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | (94) ~ (all_252_0 = 0) % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | REDUCE: (93), (94) imply: % 28.86/4.82 | | | | | (95) $false % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | CLOSE: (95) is inconsistent. % 28.86/4.82 | | | | | % 28.86/4.82 | | | | Case 2: % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | (96) ~ (all_252_1 = 0) % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | REDUCE: (92), (96) imply: % 28.86/4.82 | | | | | (97) $false % 28.86/4.82 | | | | | % 28.86/4.82 | | | | | CLOSE: (97) is inconsistent. % 28.86/4.82 | | | | | % 28.86/4.82 | | | | End of split % 28.86/4.82 | | | | % 28.86/4.82 | | | End of split % 28.86/4.82 | | | % 28.86/4.82 | | Case 2: % 28.86/4.82 | | | % 28.86/4.82 | | | (98) ? [v0: any] : ? [v1: any] : (cC42xcomp(iV3102) = v0 & % 28.86/4.82 | | | cC32xcomp(iV3102) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.82 | | | % 28.86/4.82 | | | DELTA: instantiating (98) with fresh symbols all_248_0, all_248_1 gives: % 28.86/4.82 | | | (99) cC42xcomp(iV3102) = all_248_1 & cC32xcomp(iV3102) = all_248_0 & ( % 28.86/4.82 | | | ~ (all_248_0 = 0) | ~ (all_248_1 = 0)) % 28.86/4.82 | | | % 28.86/4.82 | | | ALPHA: (99) implies: % 28.86/4.82 | | | (100) cC32xcomp(iV3102) = all_248_0 % 28.86/4.82 | | | (101) cC42xcomp(iV3102) = all_248_1 % 28.86/4.83 | | | (102) ~ (all_248_0 = 0) | ~ (all_248_1 = 0) % 28.86/4.83 | | | % 28.86/4.83 | | | BETA: splitting (50) gives: % 28.86/4.83 | | | % 28.86/4.83 | | | Case 1: % 28.86/4.83 | | | | % 28.86/4.83 | | | | % 28.86/4.83 | | | | GROUND_INST: instantiating (35) with 0, all_248_0, iV3102, simplifying % 28.86/4.83 | | | | with (17), (100) gives: % 28.86/4.83 | | | | (103) all_248_0 = 0 % 28.86/4.83 | | | | % 28.86/4.83 | | | | GROUND_INST: instantiating (36) with 0, all_248_1, iV3102, simplifying % 28.86/4.83 | | | | with (19), (101) gives: % 28.86/4.83 | | | | (104) all_248_1 = 0 % 28.86/4.83 | | | | % 28.86/4.83 | | | | BETA: splitting (102) gives: % 28.86/4.83 | | | | % 28.86/4.83 | | | | Case 1: % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | (105) ~ (all_248_0 = 0) % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | REDUCE: (103), (105) imply: % 28.86/4.83 | | | | | (106) $false % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | CLOSE: (106) is inconsistent. % 28.86/4.83 | | | | | % 28.86/4.83 | | | | Case 2: % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | (107) ~ (all_248_1 = 0) % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | REDUCE: (104), (107) imply: % 28.86/4.83 | | | | | (108) $false % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | CLOSE: (108) is inconsistent. % 28.86/4.83 | | | | | % 28.86/4.83 | | | | End of split % 28.86/4.83 | | | | % 28.86/4.83 | | | Case 2: % 28.86/4.83 | | | | % 28.86/4.83 | | | | (109) ? [v0: any] : ? [v1: any] : (cC12xcomp(iV3102) = v1 & % 28.86/4.83 | | | | cC2xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.83 | | | | % 28.86/4.83 | | | | DELTA: instantiating (109) with fresh symbols all_254_0, all_254_1 % 28.86/4.83 | | | | gives: % 28.86/4.83 | | | | (110) cC12xcomp(iV3102) = all_254_0 & cC2xcomp(iV3102) = all_254_1 & % 28.86/4.83 | | | | ( ~ (all_254_0 = 0) | ~ (all_254_1 = 0)) % 28.86/4.83 | | | | % 28.86/4.83 | | | | ALPHA: (110) implies: % 28.86/4.83 | | | | (111) cC2xcomp(iV3102) = all_254_1 % 28.86/4.83 | | | | (112) cC12xcomp(iV3102) = all_254_0 % 28.86/4.83 | | | | (113) ~ (all_254_0 = 0) | ~ (all_254_1 = 0) % 28.86/4.83 | | | | % 28.86/4.83 | | | | GROUND_INST: instantiating (27) with 0, all_254_1, iV3102, simplifying % 28.86/4.83 | | | | with (14), (111) gives: % 28.86/4.83 | | | | (114) all_254_1 = 0 % 28.86/4.83 | | | | % 28.86/4.83 | | | | GROUND_INST: instantiating (29) with 0, all_254_0, iV3102, simplifying % 28.86/4.83 | | | | with (21), (112) gives: % 28.86/4.83 | | | | (115) all_254_0 = 0 % 28.86/4.83 | | | | % 28.86/4.83 | | | | BETA: splitting (113) gives: % 28.86/4.83 | | | | % 28.86/4.83 | | | | Case 1: % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | (116) ~ (all_254_0 = 0) % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | REDUCE: (115), (116) imply: % 28.86/4.83 | | | | | (117) $false % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | CLOSE: (117) is inconsistent. % 28.86/4.83 | | | | | % 28.86/4.83 | | | | Case 2: % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | (118) ~ (all_254_1 = 0) % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | REDUCE: (114), (118) imply: % 28.86/4.83 | | | | | (119) $false % 28.86/4.83 | | | | | % 28.86/4.83 | | | | | CLOSE: (119) is inconsistent. % 28.86/4.83 | | | | | % 28.86/4.83 | | | | End of split % 28.86/4.83 | | | | % 28.86/4.83 | | | End of split % 28.86/4.83 | | | % 28.86/4.83 | | End of split % 28.86/4.83 | | % 28.86/4.83 | Case 2: % 28.86/4.83 | | % 28.86/4.83 | | (120) ? [v0: any] : ? [v1: any] : (cC26xcomp(iV3102) = v1 & % 28.86/4.83 | | cC16xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.83 | | % 28.86/4.83 | | DELTA: instantiating (120) with fresh symbols all_244_0, all_244_1 gives: % 28.86/4.83 | | (121) cC26xcomp(iV3102) = all_244_0 & cC16xcomp(iV3102) = all_244_1 & ( ~ % 28.86/4.83 | | (all_244_0 = 0) | ~ (all_244_1 = 0)) % 28.86/4.83 | | % 28.86/4.83 | | ALPHA: (121) implies: % 28.86/4.83 | | (122) cC16xcomp(iV3102) = all_244_1 % 28.86/4.83 | | (123) cC26xcomp(iV3102) = all_244_0 % 28.86/4.83 | | (124) ~ (all_244_0 = 0) | ~ (all_244_1 = 0) % 28.86/4.83 | | % 28.86/4.83 | | BETA: splitting (50) gives: % 28.86/4.83 | | % 28.86/4.83 | | Case 1: % 28.86/4.83 | | | % 28.86/4.83 | | | % 28.86/4.83 | | | GROUND_INST: instantiating (28) with 0, all_244_1, iV3102, simplifying % 28.86/4.83 | | | with (18), (122) gives: % 28.86/4.83 | | | (125) all_244_1 = 0 % 28.86/4.83 | | | % 28.86/4.83 | | | GROUND_INST: instantiating (33) with 0, all_244_0, iV3102, simplifying % 28.86/4.83 | | | with (16), (123) gives: % 28.86/4.83 | | | (126) all_244_0 = 0 % 28.86/4.83 | | | % 28.86/4.83 | | | BETA: splitting (124) gives: % 28.86/4.83 | | | % 28.86/4.83 | | | Case 1: % 28.86/4.83 | | | | % 28.86/4.83 | | | | (127) ~ (all_244_0 = 0) % 28.86/4.83 | | | | % 28.86/4.83 | | | | REDUCE: (126), (127) imply: % 28.86/4.83 | | | | (128) $false % 28.86/4.83 | | | | % 28.86/4.83 | | | | CLOSE: (128) is inconsistent. % 28.86/4.83 | | | | % 28.86/4.83 | | | Case 2: % 28.86/4.83 | | | | % 28.86/4.83 | | | | (129) ~ (all_244_1 = 0) % 28.86/4.83 | | | | % 28.86/4.83 | | | | REDUCE: (125), (129) imply: % 28.86/4.83 | | | | (130) $false % 28.86/4.83 | | | | % 28.86/4.83 | | | | CLOSE: (130) is inconsistent. % 28.86/4.83 | | | | % 28.86/4.83 | | | End of split % 28.86/4.83 | | | % 28.86/4.83 | | Case 2: % 28.86/4.83 | | | % 28.86/4.83 | | | (131) ? [v0: any] : ? [v1: any] : (cC12xcomp(iV3102) = v1 & % 28.86/4.83 | | | cC2xcomp(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.86/4.83 | | | % 28.86/4.83 | | | DELTA: instantiating (131) with fresh symbols all_254_0, all_254_1 gives: % 28.86/4.83 | | | (132) cC12xcomp(iV3102) = all_254_0 & cC2xcomp(iV3102) = all_254_1 & ( % 28.86/4.83 | | | ~ (all_254_0 = 0) | ~ (all_254_1 = 0)) % 28.86/4.83 | | | % 28.86/4.83 | | | ALPHA: (132) implies: % 28.86/4.83 | | | (133) cC2xcomp(iV3102) = all_254_1 % 28.86/4.83 | | | (134) cC12xcomp(iV3102) = all_254_0 % 28.86/4.83 | | | (135) ~ (all_254_0 = 0) | ~ (all_254_1 = 0) % 28.86/4.83 | | | % 28.86/4.83 | | | GROUND_INST: instantiating (27) with 0, all_254_1, iV3102, simplifying % 28.86/4.83 | | | with (14), (133) gives: % 28.86/4.83 | | | (136) all_254_1 = 0 % 28.86/4.83 | | | % 28.86/4.83 | | | GROUND_INST: instantiating (29) with 0, all_254_0, iV3102, simplifying % 28.86/4.83 | | | with (21), (134) gives: % 28.86/4.83 | | | (137) all_254_0 = 0 % 28.86/4.83 | | | % 28.86/4.83 | | | BETA: splitting (135) gives: % 28.86/4.83 | | | % 28.86/4.83 | | | Case 1: % 28.86/4.83 | | | | % 28.86/4.83 | | | | (138) ~ (all_254_0 = 0) % 28.86/4.83 | | | | % 28.86/4.83 | | | | REDUCE: (137), (138) imply: % 28.86/4.83 | | | | (139) $false % 28.86/4.83 | | | | % 28.86/4.83 | | | | CLOSE: (139) is inconsistent. % 28.86/4.83 | | | | % 28.86/4.83 | | | Case 2: % 28.86/4.83 | | | | % 28.86/4.83 | | | | (140) ~ (all_254_1 = 0) % 28.86/4.83 | | | | % 28.86/4.83 | | | | REDUCE: (136), (140) imply: % 28.86/4.83 | | | | (141) $false % 28.86/4.83 | | | | % 28.86/4.83 | | | | CLOSE: (141) is inconsistent. % 28.86/4.83 | | | | % 28.86/4.83 | | | End of split % 28.86/4.83 | | | % 28.86/4.83 | | End of split % 28.86/4.83 | | % 28.86/4.83 | End of split % 28.86/4.83 | % 28.86/4.83 End of proof % 28.86/4.83 % 28.86/4.83 Sub-proof #1 shows that the following formulas are inconsistent: % 28.86/4.83 ---------------------------------------------------------------- % 28.86/4.83 (1) all_211_7 = 0 % 28.86/4.83 (2) all_211_6 = 0 % 28.86/4.83 (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 28.86/4.83 (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 28.86/4.83 (4) cC62xcomp(iV3102) = 0 % 28.86/4.83 (5) cC64(iV3102) = all_236_0 % 28.86/4.83 (6) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 28.86/4.83 (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) % 28.86/4.83 (7) ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 28.86/4.83 (8) all_211_2 = 0 % 28.86/4.83 (9) cC216(iV3102) = 0 % 28.86/4.83 (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 28.86/4.83 (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) % 28.86/4.83 (11) cC216(iV3102) = all_238_1 % 28.86/4.83 (12) all_211_3 = 0 % 28.86/4.83 (13) all_211_1 = 0 % 28.86/4.83 (14) all_211_0 = 0 % 28.86/4.83 (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 28.86/4.83 (v1 = v0 | ~ (cC62xcomp(v2) = v1) | ~ (cC62xcomp(v2) = v0)) % 28.86/4.83 (16) cC64(iV3102) = all_211_4 % 28.86/4.83 (17) ~ (all_236_1 = 0) | all_236_0 = 0 % 28.86/4.84 (18) ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ % 28.86/4.84 (v1 = 0) & xsd_integer(v0) = v1)) % 28.86/4.84 (19) ~ (all_211_0 = 0) | ~ (all_211_1 = 0) | ~ (all_211_2 = 0) | ~ % 28.86/4.84 (all_211_3 = 0) | ~ (all_211_4 = 0) | ~ (all_211_5 = 0) | ~ % 28.86/4.84 (all_211_6 = 0) | ~ (all_211_7 = 0) | ? [v0: $i] : ? [v1: any] : ? % 28.86/4.84 [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) & ((v2 % 28.86/4.84 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? % 28.86/4.84 [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 28.86/4.84 $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 (20) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ % 28.86/4.84 $i(v0) | xsd_integer(v0) = 0) % 28.86/4.84 (21) cC62xcomp(iV3102) = all_236_1 % 28.86/4.84 (22) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ % 28.86/4.84 $i(v0)) % 28.86/4.84 (23) all_238_1 = all_211_5 % 28.86/4.84 % 28.86/4.84 Begin of proof % 28.86/4.84 | % 28.86/4.84 | GROUND_INST: instantiating (6) with 0, all_238_1, iV3102, simplifying with % 28.86/4.84 | (9), (11) gives: % 28.86/4.84 | (24) all_238_1 = 0 % 28.86/4.84 | % 28.86/4.84 | GROUND_INST: instantiating (10) with all_211_4, all_236_0, iV3102, simplifying % 28.86/4.84 | with (5), (16) gives: % 28.86/4.84 | (25) all_236_0 = all_211_4 % 28.86/4.84 | % 28.86/4.84 | GROUND_INST: instantiating (15) with 0, all_236_1, iV3102, simplifying with % 28.86/4.84 | (4), (21) gives: % 28.86/4.84 | (26) all_236_1 = 0 % 28.86/4.84 | % 28.86/4.84 | COMBINE_EQS: (23), (24) imply: % 28.86/4.84 | (27) all_211_5 = 0 % 28.86/4.84 | % 28.86/4.84 | SIMP: (27) implies: % 28.86/4.84 | (28) all_211_5 = 0 % 28.86/4.84 | % 28.86/4.84 | BETA: splitting (17) gives: % 28.86/4.84 | % 28.86/4.84 | Case 1: % 28.86/4.84 | | % 28.86/4.84 | | (29) ~ (all_236_1 = 0) % 28.86/4.84 | | % 28.86/4.84 | | REDUCE: (26), (29) imply: % 28.86/4.84 | | (30) $false % 28.86/4.84 | | % 28.86/4.84 | | CLOSE: (30) is inconsistent. % 28.86/4.84 | | % 28.86/4.84 | Case 2: % 28.86/4.84 | | % 28.86/4.84 | | (31) all_236_0 = 0 % 28.86/4.84 | | % 28.86/4.84 | | COMBINE_EQS: (25), (31) imply: % 28.86/4.84 | | (32) all_211_4 = 0 % 28.86/4.84 | | % 28.86/4.84 | | BETA: splitting (19) gives: % 28.86/4.84 | | % 28.86/4.84 | | Case 1: % 28.86/4.84 | | | % 28.86/4.84 | | | (33) ~ (all_211_0 = 0) % 28.86/4.84 | | | % 28.86/4.84 | | | REDUCE: (14), (33) imply: % 28.86/4.84 | | | (34) $false % 28.86/4.84 | | | % 28.86/4.84 | | | CLOSE: (34) is inconsistent. % 28.86/4.84 | | | % 28.86/4.84 | | Case 2: % 28.86/4.84 | | | % 28.86/4.84 | | | (35) ~ (all_211_1 = 0) | ~ (all_211_2 = 0) | ~ (all_211_3 = 0) | ~ % 28.86/4.84 | | | (all_211_4 = 0) | ~ (all_211_5 = 0) | ~ (all_211_6 = 0) | ~ % 28.86/4.84 | | | (all_211_7 = 0) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.84 | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & % 28.86/4.84 | | | v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? % 28.86/4.84 | | | [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = % 28.86/4.84 | | | v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | % 28.86/4.84 | | | BETA: splitting (35) gives: % 28.86/4.84 | | | % 28.86/4.84 | | | Case 1: % 28.86/4.84 | | | | % 28.86/4.84 | | | | (36) ~ (all_211_1 = 0) % 28.86/4.84 | | | | % 28.86/4.84 | | | | REDUCE: (13), (36) imply: % 28.86/4.84 | | | | (37) $false % 28.86/4.84 | | | | % 28.86/4.84 | | | | CLOSE: (37) is inconsistent. % 28.86/4.84 | | | | % 28.86/4.84 | | | Case 2: % 28.86/4.84 | | | | % 28.86/4.84 | | | | (38) ~ (all_211_2 = 0) | ~ (all_211_3 = 0) | ~ (all_211_4 = 0) | % 28.86/4.84 | | | | ~ (all_211_5 = 0) | ~ (all_211_6 = 0) | ~ (all_211_7 = 0) | ? % 28.86/4.84 | | | | [v0: $i] : ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 28.86/4.84 | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = % 28.86/4.84 | | | | 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : ? % 28.86/4.84 | | | | [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) % 28.86/4.84 | | | | & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | | % 28.86/4.84 | | | | BETA: splitting (38) gives: % 28.86/4.84 | | | | % 28.86/4.84 | | | | Case 1: % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | (39) ~ (all_211_2 = 0) % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | REDUCE: (8), (39) imply: % 28.86/4.84 | | | | | (40) $false % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | CLOSE: (40) is inconsistent. % 28.86/4.84 | | | | | % 28.86/4.84 | | | | Case 2: % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | (41) ~ (all_211_3 = 0) | ~ (all_211_4 = 0) | ~ (all_211_5 = 0) | % 28.86/4.84 | | | | | ~ (all_211_6 = 0) | ~ (all_211_7 = 0) | ? [v0: $i] : ? % 28.86/4.84 | | | | | [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 28.86/4.84 | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 % 28.86/4.84 | | | | | = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : % 28.86/4.84 | | | | | ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 28.86/4.84 | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | BETA: splitting (41) gives: % 28.86/4.84 | | | | | % 28.86/4.84 | | | | | Case 1: % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | (42) ~ (all_211_3 = 0) % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | REDUCE: (12), (42) imply: % 28.86/4.84 | | | | | | (43) $false % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | CLOSE: (43) is inconsistent. % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | Case 2: % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | (44) ~ (all_211_4 = 0) | ~ (all_211_5 = 0) | ~ (all_211_6 = 0) % 28.86/4.84 | | | | | | | ~ (all_211_7 = 0) | ? [v0: $i] : ? [v1: any] : ? [v2: % 28.86/4.84 | | | | | | any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 28.86/4.84 | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 28.86/4.84 | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.84 | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) & ( ~ % 28.86/4.84 | | | | | | (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | BETA: splitting (44) gives: % 28.86/4.84 | | | | | | % 28.86/4.84 | | | | | | Case 1: % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | (45) ~ (all_211_4 = 0) % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | REDUCE: (32), (45) imply: % 28.86/4.84 | | | | | | | (46) $false % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | CLOSE: (46) is inconsistent. % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | Case 2: % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | (47) ~ (all_211_5 = 0) | ~ (all_211_6 = 0) | ~ (all_211_7 = % 28.86/4.84 | | | | | | | 0) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.84 | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) & % 28.86/4.84 | | | | | | | ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? % 28.86/4.84 | | | | | | | [v0: $i] : ? [v1: any] : ? [v2: any] : (cowlNothing(v0) % 28.86/4.84 | | | | | | | = v2 & cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 = % 28.86/4.84 | | | | | | | 0)) % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | BETA: splitting (47) gives: % 28.86/4.84 | | | | | | | % 28.86/4.84 | | | | | | | Case 1: % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | (48) ~ (all_211_5 = 0) % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | REDUCE: (28), (48) imply: % 28.86/4.84 | | | | | | | | (49) $false % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | CLOSE: (49) is inconsistent. % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | Case 2: % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | (50) ~ (all_211_6 = 0) | ~ (all_211_7 = 0) | ? [v0: $i] : % 28.86/4.84 | | | | | | | | ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 28.86/4.84 | | | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( % 28.86/4.84 | | | | | | | | ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? % 28.86/4.84 | | | | | | | | [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & % 28.86/4.84 | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | BETA: splitting (50) gives: % 28.86/4.84 | | | | | | | | % 28.86/4.84 | | | | | | | | Case 1: % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | (51) ~ (all_211_6 = 0) % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | REDUCE: (2), (51) imply: % 28.86/4.84 | | | | | | | | | (52) $false % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | CLOSE: (52) is inconsistent. % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | Case 2: % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | (53) ~ (all_211_7 = 0) | ? [v0: $i] : ? [v1: any] : ? % 28.86/4.84 | | | | | | | | | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = % 28.86/4.84 | | | | | | | | | v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 28.86/4.84 | | | | | | | | | (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : ? % 28.86/4.84 | | | | | | | | | [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 % 28.86/4.84 | | | | | | | | | & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | BETA: splitting (53) gives: % 28.86/4.84 | | | | | | | | | % 28.86/4.84 | | | | | | | | | Case 1: % 28.86/4.84 | | | | | | | | | | % 28.86/4.84 | | | | | | | | | | (54) ~ (all_211_7 = 0) % 28.86/4.84 | | | | | | | | | | % 28.86/4.84 | | | | | | | | | | REDUCE: (1), (54) imply: % 28.86/4.84 | | | | | | | | | | (55) $false % 28.86/4.84 | | | | | | | | | | % 28.86/4.84 | | | | | | | | | | CLOSE: (55) is inconsistent. % 28.86/4.84 | | | | | | | | | | % 28.86/4.84 | | | | | | | | | Case 2: % 28.86/4.84 | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | (56) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.85 | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) % 28.86/4.85 | | | | | | | | | | & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 28.86/4.85 | | | | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: % 28.86/4.85 | | | | | | | | | | any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 % 28.86/4.85 | | | | | | | | | | & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.85 | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | BETA: splitting (56) gives: % 28.86/4.85 | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | Case 1: % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | (57) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.85 | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 28.86/4.85 | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 28.86/4.85 | | | | | | | | | | | (v1 = 0)))) % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | DELTA: instantiating (57) with fresh symbols all_330_0, % 28.86/4.85 | | | | | | | | | | | all_330_1, all_330_2 gives: % 28.86/4.85 | | | | | | | | | | | (58) xsd_string(all_330_2) = all_330_1 & % 28.86/4.85 | | | | | | | | | | | xsd_integer(all_330_2) = all_330_0 & $i(all_330_2) % 28.86/4.85 | | | | | | | | | | | & ((all_330_0 = 0 & all_330_1 = 0) | ( ~ % 28.86/4.85 | | | | | | | | | | | (all_330_0 = 0) & ~ (all_330_1 = 0))) % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | ALPHA: (58) implies: % 28.86/4.85 | | | | | | | | | | | (59) $i(all_330_2) % 28.86/4.85 | | | | | | | | | | | (60) xsd_integer(all_330_2) = all_330_0 % 28.86/4.85 | | | | | | | | | | | (61) xsd_string(all_330_2) = all_330_1 % 28.86/4.85 | | | | | | | | | | | (62) (all_330_0 = 0 & all_330_1 = 0) | ( ~ (all_330_0 = % 28.86/4.85 | | | | | | | | | | | 0) & ~ (all_330_1 = 0)) % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | GROUND_INST: instantiating (20) with all_330_2, all_330_1, % 28.86/4.85 | | | | | | | | | | | simplifying with (59), (61) gives: % 28.86/4.85 | | | | | | | | | | | (63) all_330_1 = 0 | xsd_integer(all_330_2) = 0 % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | BETA: splitting (62) gives: % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | Case 1: % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | (64) all_330_0 = 0 & all_330_1 = 0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | ALPHA: (64) implies: % 28.86/4.85 | | | | | | | | | | | | (65) all_330_1 = 0 % 28.86/4.85 | | | | | | | | | | | | (66) all_330_0 = 0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | REDUCE: (61), (65) imply: % 28.86/4.85 | | | | | | | | | | | | (67) xsd_string(all_330_2) = 0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | REDUCE: (60), (66) imply: % 28.86/4.85 | | | | | | | | | | | | (68) xsd_integer(all_330_2) = 0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_330_2, simplifying % 28.86/4.85 | | | | | | | | | | | | with (59), (67) gives: % 28.86/4.85 | | | | | | | | | | | | (69) ? [v0: int] : ( ~ (v0 = 0) & % 28.86/4.85 | | | | | | | | | | | | xsd_integer(all_330_2) = v0) % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | DELTA: instantiating (69) with fresh symbol all_344_0 % 28.86/4.85 | | | | | | | | | | | | gives: % 28.86/4.85 | | | | | | | | | | | | (70) ~ (all_344_0 = 0) & xsd_integer(all_330_2) = % 28.86/4.85 | | | | | | | | | | | | all_344_0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | ALPHA: (70) implies: % 28.86/4.85 | | | | | | | | | | | | (71) ~ (all_344_0 = 0) % 28.86/4.85 | | | | | | | | | | | | (72) xsd_integer(all_330_2) = all_344_0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | GROUND_INST: instantiating (3) with 0, all_344_0, all_330_2, % 28.86/4.85 | | | | | | | | | | | | simplifying with (68), (72) gives: % 28.86/4.85 | | | | | | | | | | | | (73) all_344_0 = 0 % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | REDUCE: (71), (73) imply: % 28.86/4.85 | | | | | | | | | | | | (74) $false % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | CLOSE: (74) is inconsistent. % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | Case 2: % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | (75) ~ (all_330_0 = 0) & ~ (all_330_1 = 0) % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | ALPHA: (75) implies: % 28.86/4.85 | | | | | | | | | | | | (76) ~ (all_330_1 = 0) % 28.86/4.85 | | | | | | | | | | | | (77) ~ (all_330_0 = 0) % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | BETA: splitting (63) gives: % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | Case 1: % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | (78) xsd_integer(all_330_2) = 0 % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_330_0, 0, all_330_2, % 28.86/4.85 | | | | | | | | | | | | | simplifying with (60), (78) gives: % 28.86/4.85 | | | | | | | | | | | | | (79) all_330_0 = 0 % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | REDUCE: (77), (79) imply: % 28.86/4.85 | | | | | | | | | | | | | (80) $false % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | CLOSE: (80) is inconsistent. % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | Case 2: % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | (81) all_330_1 = 0 % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | REDUCE: (76), (81) imply: % 28.86/4.85 | | | | | | | | | | | | | (82) $false % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | | CLOSE: (82) is inconsistent. % 28.86/4.85 | | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | | End of split % 28.86/4.85 | | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | End of split % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | Case 2: % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | (83) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 28.86/4.85 | | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 28.86/4.85 | | | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 28.86/4.85 | | | | | | | | | | | % 28.86/4.85 | | | | | | | | | | | DELTA: instantiating (83) with fresh symbols all_330_0, % 28.86/4.85 | | | | | | | | | | | all_330_1, all_330_2 gives: % 29.69/4.85 | | | | | | | | | | | (84) cowlNothing(all_330_2) = all_330_0 & % 29.69/4.85 | | | | | | | | | | | cowlThing(all_330_2) = all_330_1 & $i(all_330_2) & % 29.69/4.85 | | | | | | | | | | | ( ~ (all_330_1 = 0) | all_330_0 = 0) % 29.69/4.85 | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | ALPHA: (84) implies: % 29.69/4.85 | | | | | | | | | | | (85) $i(all_330_2) % 29.69/4.85 | | | | | | | | | | | (86) cowlThing(all_330_2) = all_330_1 % 29.69/4.85 | | | | | | | | | | | (87) cowlNothing(all_330_2) = all_330_0 % 29.69/4.85 | | | | | | | | | | | (88) ~ (all_330_1 = 0) | all_330_0 = 0 % 29.69/4.85 | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | GROUND_INST: instantiating (22) with all_330_2, all_330_1, % 29.69/4.85 | | | | | | | | | | | simplifying with (85), (86) gives: % 29.69/4.85 | | | | | | | | | | | (89) all_330_1 = 0 % 29.69/4.85 | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | BETA: splitting (88) gives: % 29.69/4.85 | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | Case 1: % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | (90) ~ (all_330_1 = 0) % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | REDUCE: (89), (90) imply: % 29.69/4.85 | | | | | | | | | | | | (91) $false % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | CLOSE: (91) is inconsistent. % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | Case 2: % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | (92) all_330_0 = 0 % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | REDUCE: (87), (92) imply: % 29.69/4.85 | | | | | | | | | | | | (93) cowlNothing(all_330_2) = 0 % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | GROUND_INST: instantiating (7) with all_330_2, simplifying with % 29.69/4.85 | | | | | | | | | | | | (85), (93) gives: % 29.69/4.85 | | | | | | | | | | | | (94) $false % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | | CLOSE: (94) is inconsistent. % 29.69/4.85 | | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | | End of split % 29.69/4.85 | | | | | | | | | | | % 29.69/4.85 | | | | | | | | | | End of split % 29.69/4.85 | | | | | | | | | | % 29.69/4.85 | | | | | | | | | End of split % 29.69/4.85 | | | | | | | | | % 29.69/4.85 | | | | | | | | End of split % 29.69/4.85 | | | | | | | | % 29.69/4.85 | | | | | | | End of split % 29.69/4.85 | | | | | | | % 29.69/4.85 | | | | | | End of split % 29.69/4.85 | | | | | | % 29.69/4.85 | | | | | End of split % 29.69/4.85 | | | | | % 29.69/4.85 | | | | End of split % 29.69/4.85 | | | | % 29.69/4.85 | | | End of split % 29.69/4.85 | | | % 29.69/4.85 | | End of split % 29.69/4.85 | | % 29.69/4.85 | End of split % 29.69/4.85 | % 29.69/4.85 End of proof % 29.69/4.85 % SZS output end Proof for theBenchmark % 29.69/4.85 % 29.69/4.85 4239ms %------------------------------------------------------------------------------