%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KRS149+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:26 EDT 2023 % Result : Theorem 15.38s 2.95s % Output : Proof 26.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS149+1 : TPTP v8.1.2. Released v3.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.34 % Computer : n001.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Mon Aug 28 01:55:49 EDT 2023 % 0.14/0.34 % CPUTime : % 0.21/0.62 ________ _____ % 0.21/0.62 ___ __ \_________(_)________________________________ % 0.21/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.62 % 0.21/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.62 (2023-06-19) % 0.21/0.62 % 0.21/0.62 (c) Philipp Rümmer, 2009-2023 % 0.21/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.62 Amanda Stjerna. % 0.21/0.62 Free software under BSD-3-Clause. % 0.21/0.62 % 0.21/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.62 % 0.21/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.63 Running up to 7 provers in parallel. % 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 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 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 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 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 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.72/1.39 Prover 1: Preprocessing ... % 4.72/1.40 Prover 4: Preprocessing ... % 4.72/1.44 Prover 5: Preprocessing ... % 4.72/1.44 Prover 6: Preprocessing ... % 4.72/1.44 Prover 3: Preprocessing ... % 4.72/1.44 Prover 2: Preprocessing ... % 4.72/1.44 Prover 0: Preprocessing ... % 12.08/2.42 Prover 5: Proving ... % 12.08/2.44 Prover 2: Proving ... % 14.69/2.83 Prover 6: Proving ... % 15.38/2.89 Prover 1: Constructing countermodel ... % 15.38/2.94 Prover 3: Constructing countermodel ... % 15.38/2.95 Prover 2: proved (2302ms) % 15.38/2.95 % 15.38/2.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.38/2.95 % 15.38/2.95 Prover 3: stopped % 15.38/2.97 Prover 6: stopped % 15.38/2.98 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.38/2.98 Prover 5: stopped % 15.38/3.00 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.38/3.00 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 15.38/3.00 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.48/3.29 Prover 4: Constructing countermodel ... % 18.48/3.31 Prover 7: Preprocessing ... % 18.48/3.32 Prover 11: Preprocessing ... % 18.48/3.33 Prover 10: Preprocessing ... % 18.48/3.34 Prover 8: Preprocessing ... % 19.38/3.45 Prover 0: Proving ... % 19.38/3.45 Prover 0: stopped % 19.38/3.47 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 20.13/3.60 Prover 7: Warning: ignoring some quantifiers % 20.13/3.61 Prover 13: Preprocessing ... % 20.13/3.62 Prover 7: Constructing countermodel ... % 20.13/3.62 Prover 10: Warning: ignoring some quantifiers % 20.13/3.65 Prover 10: Constructing countermodel ... % 23.00/3.91 Prover 13: Warning: ignoring some quantifiers % 23.00/3.94 Prover 13: Constructing countermodel ... % 24.04/4.04 Prover 8: Warning: ignoring some quantifiers % 24.45/4.09 Prover 8: Constructing countermodel ... % 24.45/4.10 Prover 1: Found proof (size 194) % 24.45/4.10 Prover 1: proved (3460ms) % 24.45/4.10 Prover 7: stopped % 24.45/4.10 Prover 8: stopped % 24.45/4.10 Prover 4: stopped % 24.45/4.10 Prover 13: stopped % 24.45/4.11 Prover 10: stopped % 25.14/4.31 Prover 11: Constructing countermodel ... % 25.14/4.31 Prover 11: stopped % 25.14/4.31 % 25.14/4.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.14/4.31 % 25.14/4.34 % SZS output start Proof for theBenchmark % 25.14/4.35 Assumptions after simplification: % 25.14/4.35 --------------------------------- % 25.14/4.35 % 25.14/4.35 (axiom_0) % 25.14/4.38 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ $i(v0)) & % 25.14/4.38 ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 25.14/4.38 % 25.14/4.38 (axiom_1) % 25.14/4.38 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ $i(v0) | % 25.14/4.38 xsd_integer(v0) = 0) & ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | % 25.14/4.38 ? [v1: int] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) % 25.14/4.38 % 25.14/4.38 (axiom_107) % 25.14/4.39 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cTEST(v0) = v1) | ~ $i(v0) | ? % 25.14/4.39 [v2: any] : ? [v3: any] : (cC46(v0) = v3 & cC216(v0) = v2 & ( ~ (v3 = 0) | % 25.14/4.39 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | % 25.14/4.39 (cC46(v0) = 0 & cC216(v0) = 0)) % 25.14/4.39 % 25.14/4.39 (axiom_108) % 25.14/4.39 cTEST(iV3102) = 0 & $i(iV3102) % 25.14/4.39 % 25.14/4.39 (axiom_109) % 25.14/4.39 cowlThing(iV3102) = 0 & $i(iV3102) % 25.14/4.39 % 25.14/4.39 (axiom_112) % 25.14/4.39 cTOP(iV3102) = 0 & $i(iV3102) % 25.14/4.39 % 25.14/4.39 (axiom_114) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC42(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_115) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC12(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_116) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC26(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_119) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC62(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_121) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC16(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_122) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC2(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_123) % 25.14/4.39 $i(iV3102) & ? [v0: int] : ( ~ (v0 = 0) & cC32(iV3102) = v0) % 25.14/4.39 % 25.14/4.39 (axiom_13) % 25.14/4.39 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ $i(v0) | ! % 25.14/4.39 [v2: $i] : ( ~ (cC10(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = 0) & % 25.14/4.39 rR1(v0, v2) = v3))) & ! [v0: $i] : ( ~ (cC12(v0) = 0) | ~ $i(v0) | ? % 25.14/4.39 [v1: $i] : (rR1(v0, v1) = 0 & cC10(v1) = 0 & $i(v1))) % 25.14/4.39 % 25.14/4.39 (axiom_24) % 25.14/4.39 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC14(v0) = v1) | ~ $i(v0) | ? % 25.14/4.39 [v2: any] : ? [v3: any] : (cC12(v0) = v2 & cC2(v0) = v3 & (v3 = 0 | v2 = % 25.14/4.39 0))) & ! [v0: $i] : ( ~ (cC14(v0) = 0) | ~ $i(v0) | ? [v1: int] : ? % 25.14/4.39 [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC12(v0) = v1 & cC2(v0) = v2)) % 25.14/4.39 % 25.14/4.39 (axiom_65) % 25.14/4.40 ! [v0: $i] : ! [v1: any] : ( ~ (cC64(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 25.14/4.40 ? [v3: any] : (cC216(v0) = v2 & cC214(v0) = v3 & ( ~ (v2 = 0) | (v1 = 0 & ~ % 25.14/4.40 (v3 = 0))))) & ! [v0: $i] : ( ~ (cC64(v0) = 0) | ~ $i(v0) | ? [v1: % 25.14/4.40 any] : ? [v2: any] : (cC216(v0) = v2 & cC214(v0) = v1 & (v2 = 0 | v1 = % 25.14/4.40 0))) % 25.14/4.40 % 25.14/4.40 (axiom_68) % 25.14/4.40 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC26(v0) = v1) | ~ $i(v0) | ! % 25.14/4.40 [v2: $i] : ( ~ (cC24(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = 0) & % 25.14/4.40 rR1(v0, v2) = v3))) & ! [v0: $i] : ( ~ (cC26(v0) = 0) | ~ $i(v0) | ? % 25.14/4.40 [v1: $i] : (cC24(v1) = 0 & rR1(v0, v1) = 0 & $i(v1))) % 25.14/4.40 % 25.14/4.40 (axiom_69) % 25.14/4.40 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC28(v0) = v1) | ~ $i(v0) | ? % 25.14/4.40 [v2: any] : ? [v3: any] : (cC26(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = % 25.14/4.40 0))) & ! [v0: $i] : ( ~ (cC28(v0) = 0) | ~ $i(v0) | ? [v1: int] : ? % 25.14/4.40 [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC26(v0) = v1 & cC16(v0) = v2)) % 25.14/4.40 % 25.14/4.40 (axiom_70) % 25.14/4.40 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC30(v0) = v1) | ~ $i(v0) | ? % 25.14/4.40 [v2: any] : ? [v3: any] : (cC28(v0) = v3 & cC14(v0) = v2 & ( ~ (v3 = 0) | % 25.14/4.40 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC30(v0) = 0) | ~ $i(v0) | (cC28(v0) % 25.14/4.40 = 0 & cC14(v0) = 0)) % 25.14/4.40 % 25.14/4.40 (axiom_76) % 25.14/4.40 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC42(v0) = v1) | ~ $i(v0) | ! % 25.14/4.40 [v2: $i] : ( ~ (cC40(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = 0) & % 25.14/4.40 rR1(v0, v2) = v3))) & ! [v0: $i] : ( ~ (cC42(v0) = 0) | ~ $i(v0) | ? % 25.14/4.40 [v1: $i] : (cC40(v1) = 0 & rR1(v0, v1) = 0 & $i(v1))) % 25.14/4.40 % 25.14/4.40 (axiom_77) % 25.14/4.40 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC44(v0) = v1) | ~ $i(v0) | ? % 25.14/4.40 [v2: any] : ? [v3: any] : (cC42(v0) = v3 & cC32(v0) = v2 & (v3 = 0 | v2 = % 25.14/4.40 0))) & ! [v0: $i] : ( ~ (cC44(v0) = 0) | ~ $i(v0) | ? [v1: int] : ? % 25.14/4.40 [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC42(v0) = v2 & cC32(v0) = v1)) % 25.14/4.40 % 25.14/4.40 (axiom_88) % 25.14/4.41 ! [v0: $i] : ! [v1: any] : ( ~ (cTOP(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 25.14/4.41 ? [v3: any] : (cC62(v0) = v3 & cC64(v0) = v2 & ( ~ (v2 = 0) | (v1 = 0 & ~ % 25.14/4.41 (v3 = 0))))) & ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: % 25.14/4.41 any] : ? [v2: any] : (cC62(v0) = v1 & cC64(v0) = v2 & (v2 = 0 | v1 = 0))) % 25.14/4.41 % 25.14/4.41 (the_axiom) % 25.14/4.41 $i(iV3102) & ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 25.14/4.41 [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : (cC46(iV3102) = v1 & % 25.14/4.41 cC44(iV3102) = v3 & cC30(iV3102) = v2 & cC28(iV3102) = v4 & cC64(iV3102) = % 25.14/4.41 v5 & cC216(iV3102) = v0 & cC14(iV3102) = v6 & cowlThing(iV3102) = v7 & ( ~ % 25.14/4.41 (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 % 25.14/4.41 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | ? [v8: $i] : ? [v9: any] : ? [v10: % 25.14/4.41 any] : (xsd_string(v8) = v9 & xsd_integer(v8) = v10 & $i(v8) & ((v10 = 0 % 25.14/4.41 & v9 = 0) | ( ~ (v10 = 0) & ~ (v9 = 0)))) | ? [v8: $i] : ? [v9: % 25.14/4.41 any] : ? [v10: any] : (cowlNothing(v8) = v10 & cowlThing(v8) = v9 & % 25.14/4.41 $i(v8) & ( ~ (v9 = 0) | v10 = 0)))) % 25.14/4.41 % 25.14/4.41 (function-axioms) % 25.14/4.45 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 25.14/4.45 [v3: $i] : (v1 = v0 | ~ (rR1(v3, v2) = v1) | ~ (rR1(v3, v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC96(v2) = v1) | ~ % 25.14/4.45 (cC96(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC94(v2) = v1) | ~ (cC94(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC92(v2) = v1) | ~ (cC92(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC90(v2) = v1) | ~ % 25.14/4.45 (cC90(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC88(v2) = v1) | ~ (cC88(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC86(v2) = v1) | ~ (cC86(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC84(v2) = v1) | ~ % 25.14/4.45 (cC84(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC82(v2) = v1) | ~ (cC82(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC80(v2) = v1) | ~ (cC80(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC78(v2) = v1) | ~ % 25.14/4.45 (cC78(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC76(v2) = v1) | ~ (cC76(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC74(v2) = v1) | ~ (cC74(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC72(v2) = v1) | ~ % 25.14/4.45 (cC72(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC70(v2) = v1) | ~ (cC70(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC68(v2) = v1) | ~ (cC68(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC66(v2) = v1) | ~ % 25.14/4.45 (cC66(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cTOP(v2) = v1) | ~ (cTOP(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC62(v2) = v1) | ~ (cC62(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC60(v2) = v1) | ~ % 25.14/4.45 (cC60(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC6(v2) = v1) | ~ (cC6(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC58(v2) = v1) | ~ (cC58(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC56(v2) = v1) | ~ % 25.14/4.45 (cC56(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC54(v2) = v1) | ~ (cC54(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC52(v2) = v1) | ~ (cC52(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC50(v2) = v1) | ~ % 25.14/4.45 (cC50(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC48(v2) = v1) | ~ (cC48(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC46(v2) = v1) | ~ (cC46(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC44(v2) = v1) | ~ % 25.14/4.45 (cC44(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC42(v2) = v1) | ~ (cC42(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC40(v2) = v1) | ~ (cC40(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ % 25.14/4.45 (cC4(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC38(v2) = v1) | ~ (cC38(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC36(v2) = v1) | ~ (cC36(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC34(v2) = v1) | ~ % 25.14/4.45 (cC34(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC32(v2) = v1) | ~ (cC32(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC30(v2) = v1) | ~ (cC30(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC28(v2) = v1) | ~ % 25.14/4.45 (cC28(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC26(v2) = v1) | ~ (cC26(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC24(v2) = v1) | ~ (cC24(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC22(v2) = v1) | ~ % 25.14/4.45 (cC22(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC214(v2) = v1) | ~ % 25.14/4.45 (cC214(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC212(v2) = v1) | ~ (cC212(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC210(v2) = v1) | ~ (cC210(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC208(v2) = v1) | ~ % 25.14/4.45 (cC208(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC206(v2) = v1) | ~ (cC206(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC204(v2) = v1) | ~ (cC204(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC202(v2) = v1) | ~ % 25.14/4.45 (cC202(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC200(v2) = v1) | ~ (cC200(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC20(v2) = v1) | ~ (cC20(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC198(v2) = v1) | ~ % 25.14/4.45 (cC198(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC196(v2) = v1) | ~ (cC196(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC194(v2) = v1) | ~ (cC194(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC192(v2) = v1) | ~ % 25.14/4.45 (cC192(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC190(v2) = v1) | ~ (cC190(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC188(v2) = v1) | ~ (cC188(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC186(v2) = v1) | ~ % 25.14/4.45 (cC186(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC184(v2) = v1) | ~ (cC184(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC182(v2) = v1) | ~ (cC182(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC180(v2) = v1) | ~ % 25.14/4.45 (cC180(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC178(v2) = v1) | ~ (cC178(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC176(v2) = v1) | ~ % 25.14/4.45 (cC176(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC174(v2) = v1) | ~ (cC174(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC172(v2) = v1) | ~ (cC172(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC170(v2) = v1) | ~ % 25.14/4.45 (cC170(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC168(v2) = v1) | ~ (cC168(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC166(v2) = v1) | ~ (cC166(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC164(v2) = v1) | ~ % 25.14/4.45 (cC164(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC162(v2) = v1) | ~ (cC162(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC160(v2) = v1) | ~ (cC160(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC158(v2) = v1) | ~ % 25.14/4.45 (cC158(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC156(v2) = v1) | ~ (cC156(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC154(v2) = v1) | ~ (cC154(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC152(v2) = v1) | ~ % 25.14/4.45 (cC152(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC150(v2) = v1) | ~ (cC150(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC148(v2) = v1) | ~ (cC148(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC146(v2) = v1) | ~ % 25.14/4.45 (cC146(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC144(v2) = v1) | ~ (cC144(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC142(v2) = v1) | ~ (cC142(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC140(v2) = v1) | ~ % 25.14/4.45 (cC140(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC138(v2) = v1) | ~ (cC138(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC136(v2) = v1) | ~ % 25.14/4.45 (cC136(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC134(v2) = v1) | ~ (cC134(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC132(v2) = v1) | ~ (cC132(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC130(v2) = v1) | ~ % 25.14/4.45 (cC130(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC128(v2) = v1) | ~ (cC128(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC126(v2) = v1) | ~ (cC126(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC124(v2) = v1) | ~ % 25.14/4.45 (cC124(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC122(v2) = v1) | ~ (cC122(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC120(v2) = v1) | ~ (cC120(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC12(v2) = v1) | ~ % 25.14/4.45 (cC12(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC118(v2) = v1) | ~ (cC118(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC116(v2) = v1) | ~ (cC116(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC114(v2) = v1) | ~ % 25.14/4.45 (cC114(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC112(v2) = v1) | ~ (cC112(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC110(v2) = v1) | ~ (cC110(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC108(v2) = v1) | ~ % 25.14/4.45 (cC108(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC106(v2) = v1) | ~ (cC106(v2) = v0)) & ! % 25.14/4.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 25.14/4.45 | ~ (cC104(v2) = v1) | ~ (cC104(v2) = v0)) & ! [v0: MultipleValueBool] : % 25.14/4.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC102(v2) = v1) | ~ % 25.14/4.45 (cC102(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.14/4.45 : ! [v2: $i] : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC100(v2) = v1) | ~ (cC100(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC98(v2) = v1) | ~ % 25.14/4.45 (cC98(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (cC8(v2) = v1) | ~ (cC8(v2) = v0)) & ! [v0: % 25.14/4.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.45 ~ (cC10(v2) = v1) | ~ (cC10(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.14/4.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ % 25.14/4.45 (cC2(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.14/4.45 ! [v2: $i] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) & % 25.14/4.45 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 25.14/4.46 v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) & ! [v0: % 25.14/4.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.46 ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) & ! [v0: % 25.14/4.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 25.14/4.46 ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 25.14/4.46 % 25.14/4.46 Further assumptions not needed in the proof: % 25.14/4.46 -------------------------------------------- % 25.14/4.46 axiom_10, axiom_100, axiom_101, axiom_102, axiom_103, axiom_104, axiom_105, % 25.14/4.46 axiom_106, axiom_11, axiom_110, axiom_111, axiom_113, axiom_117, axiom_118, % 25.14/4.46 axiom_12, axiom_120, axiom_124, axiom_14, axiom_15, axiom_16, axiom_17, % 25.14/4.46 axiom_18, axiom_19, axiom_2, axiom_20, axiom_21, axiom_22, axiom_23, axiom_25, % 25.14/4.46 axiom_26, axiom_27, axiom_28, axiom_29, axiom_3, axiom_30, axiom_31, axiom_32, % 25.14/4.46 axiom_33, axiom_34, axiom_35, axiom_36, axiom_37, axiom_38, axiom_39, axiom_4, % 25.14/4.46 axiom_40, axiom_41, axiom_42, axiom_43, axiom_44, axiom_45, axiom_46, axiom_47, % 25.14/4.46 axiom_48, axiom_49, axiom_5, axiom_50, axiom_51, axiom_52, axiom_53, axiom_54, % 25.14/4.46 axiom_55, axiom_56, axiom_57, axiom_58, axiom_59, axiom_6, axiom_60, axiom_61, % 25.14/4.46 axiom_62, axiom_63, axiom_64, axiom_66, axiom_67, axiom_7, axiom_71, axiom_72, % 25.14/4.46 axiom_73, axiom_74, axiom_75, axiom_78, axiom_79, axiom_8, axiom_80, axiom_81, % 25.14/4.46 axiom_82, axiom_83, axiom_84, axiom_85, axiom_86, axiom_87, axiom_89, axiom_9, % 25.14/4.46 axiom_90, axiom_91, axiom_92, axiom_93, axiom_94, axiom_95, axiom_96, axiom_97, % 25.14/4.46 axiom_98, axiom_99 % 25.14/4.46 % 25.14/4.46 Those formulas are unsatisfiable: % 25.14/4.46 --------------------------------- % 25.14/4.46 % 25.14/4.46 Begin of proof % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_0) implies: % 25.14/4.46 | (1) ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 25.14/4.46 | (2) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ % 25.14/4.46 | $i(v0)) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_1) implies: % 25.14/4.46 | (3) ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ % 25.14/4.46 | (v1 = 0) & xsd_integer(v0) = v1)) % 25.14/4.46 | (4) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ % 25.14/4.46 | $i(v0) | xsd_integer(v0) = 0) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_13) implies: % 25.14/4.46 | (5) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ $i(v0) | % 25.14/4.46 | ! [v2: $i] : ( ~ (cC10(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 % 25.14/4.46 | = 0) & rR1(v0, v2) = v3))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_24) implies: % 25.14/4.46 | (6) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC14(v0) = v1) | ~ $i(v0) | % 25.14/4.46 | ? [v2: any] : ? [v3: any] : (cC12(v0) = v2 & cC2(v0) = v3 & (v3 = 0 % 25.14/4.46 | | v2 = 0))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_65) implies: % 25.14/4.46 | (7) ! [v0: $i] : ! [v1: any] : ( ~ (cC64(v0) = v1) | ~ $i(v0) | ? [v2: % 25.14/4.46 | any] : ? [v3: any] : (cC216(v0) = v2 & cC214(v0) = v3 & ( ~ (v2 = % 25.14/4.46 | 0) | (v1 = 0 & ~ (v3 = 0))))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_68) implies: % 25.14/4.46 | (8) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC26(v0) = v1) | ~ $i(v0) | % 25.14/4.46 | ! [v2: $i] : ( ~ (cC24(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 % 25.14/4.46 | = 0) & rR1(v0, v2) = v3))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_69) implies: % 25.14/4.46 | (9) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC28(v0) = v1) | ~ $i(v0) | % 25.14/4.46 | ? [v2: any] : ? [v3: any] : (cC26(v0) = v2 & cC16(v0) = v3 & (v3 = % 25.14/4.46 | 0 | v2 = 0))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_70) implies: % 25.14/4.46 | (10) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC30(v0) = v1) | ~ $i(v0) % 25.14/4.46 | | ? [v2: any] : ? [v3: any] : (cC28(v0) = v3 & cC14(v0) = v2 & ( ~ % 25.14/4.46 | (v3 = 0) | ~ (v2 = 0)))) % 25.14/4.46 | % 25.14/4.46 | ALPHA: (axiom_76) implies: % 25.14/4.47 | (11) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC42(v0) = v1) | ~ $i(v0) % 25.14/4.47 | | ! [v2: $i] : ( ~ (cC40(v2) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ % 25.14/4.47 | (v3 = 0) & rR1(v0, v2) = v3))) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_77) implies: % 25.14/4.47 | (12) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC44(v0) = v1) | ~ $i(v0) % 25.14/4.47 | | ? [v2: any] : ? [v3: any] : (cC42(v0) = v3 & cC32(v0) = v2 & (v3 % 25.14/4.47 | = 0 | v2 = 0))) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_88) implies: % 25.14/4.47 | (13) ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? [v2: % 25.14/4.47 | any] : (cC62(v0) = v1 & cC64(v0) = v2 & (v2 = 0 | v1 = 0))) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_107) implies: % 25.14/4.47 | (14) ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | (cC46(v0) = 0 & % 25.14/4.47 | cC216(v0) = 0)) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_108) implies: % 25.14/4.47 | (15) cTEST(iV3102) = 0 % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_109) implies: % 25.14/4.47 | (16) cowlThing(iV3102) = 0 % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_112) implies: % 25.14/4.47 | (17) cTOP(iV3102) = 0 % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_114) implies: % 25.14/4.47 | (18) ? [v0: int] : ( ~ (v0 = 0) & cC42(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_115) implies: % 25.14/4.47 | (19) ? [v0: int] : ( ~ (v0 = 0) & cC12(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_116) implies: % 25.14/4.47 | (20) ? [v0: int] : ( ~ (v0 = 0) & cC26(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_119) implies: % 25.14/4.47 | (21) ? [v0: int] : ( ~ (v0 = 0) & cC62(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_121) implies: % 25.14/4.47 | (22) ? [v0: int] : ( ~ (v0 = 0) & cC16(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_122) implies: % 25.14/4.47 | (23) ? [v0: int] : ( ~ (v0 = 0) & cC2(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (axiom_123) implies: % 25.14/4.47 | (24) ? [v0: int] : ( ~ (v0 = 0) & cC32(iV3102) = v0) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (the_axiom) implies: % 25.14/4.47 | (25) $i(iV3102) % 25.14/4.47 | (26) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 25.14/4.47 | any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : (cC46(iV3102) = % 25.14/4.47 | v1 & cC44(iV3102) = v3 & cC30(iV3102) = v2 & cC28(iV3102) = v4 & % 25.14/4.47 | cC64(iV3102) = v5 & cC216(iV3102) = v0 & cC14(iV3102) = v6 & % 25.14/4.47 | cowlThing(iV3102) = v7 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | % 25.14/4.47 | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 25.14/4.47 | | ? [v8: $i] : ? [v9: any] : ? [v10: any] : (xsd_string(v8) = % 25.14/4.47 | v9 & xsd_integer(v8) = v10 & $i(v8) & ((v10 = 0 & v9 = 0) | ( ~ % 25.14/4.47 | (v10 = 0) & ~ (v9 = 0)))) | ? [v8: $i] : ? [v9: any] : ? % 25.14/4.47 | [v10: any] : (cowlNothing(v8) = v10 & cowlThing(v8) = v9 & $i(v8) % 25.14/4.47 | & ( ~ (v9 = 0) | v10 = 0)))) % 25.14/4.47 | % 25.14/4.47 | ALPHA: (function-axioms) implies: % 25.98/4.47 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 25.98/4.47 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 25.98/4.47 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) % 25.98/4.47 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) % 25.98/4.47 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cC12(v2) = v1) | ~ (cC12(v2) = v0)) % 25.98/4.47 | (32) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) % 25.98/4.47 | (33) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.47 | : (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) % 25.98/4.48 | (34) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) % 25.98/4.48 | (35) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC26(v2) = v1) | ~ (cC26(v2) = v0)) % 25.98/4.48 | (36) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC28(v2) = v1) | ~ (cC28(v2) = v0)) % 25.98/4.48 | (37) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC32(v2) = v1) | ~ (cC32(v2) = v0)) % 25.98/4.48 | (38) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC42(v2) = v1) | ~ (cC42(v2) = v0)) % 25.98/4.48 | (39) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC46(v2) = v1) | ~ (cC46(v2) = v0)) % 25.98/4.48 | (40) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 25.98/4.48 | : (v1 = v0 | ~ (cC62(v2) = v1) | ~ (cC62(v2) = v0)) % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (23) with fresh symbol all_117_0 gives: % 25.98/4.48 | (41) ~ (all_117_0 = 0) & cC2(iV3102) = all_117_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (41) implies: % 25.98/4.48 | (42) ~ (all_117_0 = 0) % 25.98/4.48 | (43) cC2(iV3102) = all_117_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (24) with fresh symbol all_119_0 gives: % 25.98/4.48 | (44) ~ (all_119_0 = 0) & cC32(iV3102) = all_119_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (44) implies: % 25.98/4.48 | (45) ~ (all_119_0 = 0) % 25.98/4.48 | (46) cC32(iV3102) = all_119_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (19) with fresh symbol all_121_0 gives: % 25.98/4.48 | (47) ~ (all_121_0 = 0) & cC12(iV3102) = all_121_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (47) implies: % 25.98/4.48 | (48) ~ (all_121_0 = 0) % 25.98/4.48 | (49) cC12(iV3102) = all_121_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (20) with fresh symbol all_123_0 gives: % 25.98/4.48 | (50) ~ (all_123_0 = 0) & cC26(iV3102) = all_123_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (50) implies: % 25.98/4.48 | (51) ~ (all_123_0 = 0) % 25.98/4.48 | (52) cC26(iV3102) = all_123_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (18) with fresh symbol all_125_0 gives: % 25.98/4.48 | (53) ~ (all_125_0 = 0) & cC42(iV3102) = all_125_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (53) implies: % 25.98/4.48 | (54) ~ (all_125_0 = 0) % 25.98/4.48 | (55) cC42(iV3102) = all_125_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (21) with fresh symbol all_129_0 gives: % 25.98/4.48 | (56) ~ (all_129_0 = 0) & cC62(iV3102) = all_129_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (56) implies: % 25.98/4.48 | (57) ~ (all_129_0 = 0) % 25.98/4.48 | (58) cC62(iV3102) = all_129_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (22) with fresh symbol all_131_0 gives: % 25.98/4.48 | (59) ~ (all_131_0 = 0) & cC16(iV3102) = all_131_0 % 25.98/4.48 | % 25.98/4.48 | ALPHA: (59) implies: % 25.98/4.48 | (60) ~ (all_131_0 = 0) % 25.98/4.48 | (61) cC16(iV3102) = all_131_0 % 25.98/4.48 | % 25.98/4.48 | DELTA: instantiating (26) with fresh symbols all_135_0, all_135_1, all_135_2, % 25.98/4.48 | all_135_3, all_135_4, all_135_5, all_135_6, all_135_7 gives: % 25.98/4.48 | (62) cC46(iV3102) = all_135_6 & cC44(iV3102) = all_135_4 & cC30(iV3102) = % 25.98/4.48 | all_135_5 & cC28(iV3102) = all_135_3 & cC64(iV3102) = all_135_2 & % 25.98/4.48 | cC216(iV3102) = all_135_7 & cC14(iV3102) = all_135_1 & % 25.98/4.48 | cowlThing(iV3102) = all_135_0 & ( ~ (all_135_0 = 0) | ~ (all_135_1 = % 25.98/4.48 | 0) | ~ (all_135_2 = 0) | ~ (all_135_3 = 0) | ~ (all_135_4 = 0) % 25.98/4.48 | | ~ (all_135_5 = 0) | ~ (all_135_6 = 0) | ~ (all_135_7 = 0) | ? % 25.98/4.48 | [v0: $i] : ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 25.98/4.48 | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) % 25.98/4.48 | & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.48 | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | % 25.98/4.48 | v2 = 0))) % 25.98/4.48 | % 25.98/4.48 | ALPHA: (62) implies: % 25.98/4.48 | (63) cowlThing(iV3102) = all_135_0 % 25.98/4.48 | (64) cC14(iV3102) = all_135_1 % 25.98/4.48 | (65) cC216(iV3102) = all_135_7 % 25.98/4.48 | (66) cC64(iV3102) = all_135_2 % 25.98/4.48 | (67) cC28(iV3102) = all_135_3 % 25.98/4.48 | (68) cC30(iV3102) = all_135_5 % 25.98/4.48 | (69) cC44(iV3102) = all_135_4 % 25.98/4.48 | (70) cC46(iV3102) = all_135_6 % 25.98/4.48 | (71) ~ (all_135_0 = 0) | ~ (all_135_1 = 0) | ~ (all_135_2 = 0) | ~ % 25.98/4.49 | (all_135_3 = 0) | ~ (all_135_4 = 0) | ~ (all_135_5 = 0) | ~ % 25.98/4.49 | (all_135_6 = 0) | ~ (all_135_7 = 0) | ? [v0: $i] : ? [v1: any] : ? % 25.98/4.49 | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) & % 25.98/4.49 | ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : % 25.98/4.49 | ? [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = % 25.98/4.49 | v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (27) with 0, all_135_0, iV3102, simplifying with % 25.98/4.49 | (16), (63) gives: % 25.98/4.49 | (72) all_135_0 = 0 % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (5) with iV3102, all_121_0, simplifying with (25), % 25.98/4.49 | (49) gives: % 25.98/4.49 | (73) all_121_0 = 0 | ! [v0: $i] : ( ~ (cC10(v0) = 0) | ~ $i(v0) | ? [v1: % 25.98/4.49 | int] : ( ~ (v1 = 0) & rR1(iV3102, v0) = v1)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (6) with iV3102, all_135_1, simplifying with (25), % 25.98/4.49 | (64) gives: % 25.98/4.49 | (74) all_135_1 = 0 | ? [v0: any] : ? [v1: any] : (cC12(iV3102) = v0 & % 25.98/4.49 | cC2(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (7) with iV3102, all_135_2, simplifying with (25), % 25.98/4.49 | (66) gives: % 25.98/4.49 | (75) ? [v0: any] : ? [v1: any] : (cC216(iV3102) = v0 & cC214(iV3102) = v1 % 25.98/4.49 | & ( ~ (v0 = 0) | (all_135_2 = 0 & ~ (v1 = 0)))) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (8) with iV3102, all_123_0, simplifying with (25), % 25.98/4.49 | (52) gives: % 25.98/4.49 | (76) all_123_0 = 0 | ! [v0: $i] : ( ~ (cC24(v0) = 0) | ~ $i(v0) | ? [v1: % 25.98/4.49 | int] : ( ~ (v1 = 0) & rR1(iV3102, v0) = v1)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (9) with iV3102, all_135_3, simplifying with (25), % 25.98/4.49 | (67) gives: % 25.98/4.49 | (77) all_135_3 = 0 | ? [v0: any] : ? [v1: any] : (cC26(iV3102) = v0 & % 25.98/4.49 | cC16(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (10) with iV3102, all_135_5, simplifying with (25), % 25.98/4.49 | (68) gives: % 25.98/4.49 | (78) all_135_5 = 0 | ? [v0: any] : ? [v1: any] : (cC28(iV3102) = v1 & % 25.98/4.49 | cC14(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (11) with iV3102, all_125_0, simplifying with (25), % 25.98/4.49 | (55) gives: % 25.98/4.49 | (79) all_125_0 = 0 | ! [v0: $i] : ( ~ (cC40(v0) = 0) | ~ $i(v0) | ? [v1: % 25.98/4.49 | int] : ( ~ (v1 = 0) & rR1(iV3102, v0) = v1)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (12) with iV3102, all_135_4, simplifying with (25), % 25.98/4.49 | (69) gives: % 25.98/4.49 | (80) all_135_4 = 0 | ? [v0: any] : ? [v1: any] : (cC42(iV3102) = v1 & % 25.98/4.49 | cC32(iV3102) = v0 & (v1 = 0 | v0 = 0)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (13) with iV3102, simplifying with (17), (25) % 25.98/4.49 | gives: % 25.98/4.49 | (81) ? [v0: any] : ? [v1: any] : (cC62(iV3102) = v0 & cC64(iV3102) = v1 & % 25.98/4.49 | (v1 = 0 | v0 = 0)) % 25.98/4.49 | % 25.98/4.49 | GROUND_INST: instantiating (14) with iV3102, simplifying with (15), (25) % 25.98/4.49 | gives: % 25.98/4.49 | (82) cC46(iV3102) = 0 & cC216(iV3102) = 0 % 25.98/4.49 | % 25.98/4.49 | ALPHA: (82) implies: % 25.98/4.49 | (83) cC216(iV3102) = 0 % 25.98/4.49 | (84) cC46(iV3102) = 0 % 25.98/4.49 | % 25.98/4.49 | DELTA: instantiating (81) with fresh symbols all_147_0, all_147_1 gives: % 25.98/4.49 | (85) cC62(iV3102) = all_147_1 & cC64(iV3102) = all_147_0 & (all_147_0 = 0 | % 25.98/4.49 | all_147_1 = 0) % 25.98/4.49 | % 25.98/4.49 | ALPHA: (85) implies: % 25.98/4.49 | (86) cC64(iV3102) = all_147_0 % 25.98/4.49 | (87) cC62(iV3102) = all_147_1 % 25.98/4.49 | (88) all_147_0 = 0 | all_147_1 = 0 % 25.98/4.49 | % 25.98/4.49 | DELTA: instantiating (75) with fresh symbols all_149_0, all_149_1 gives: % 25.98/4.49 | (89) cC216(iV3102) = all_149_1 & cC214(iV3102) = all_149_0 & ( ~ (all_149_1 % 25.98/4.49 | = 0) | (all_135_2 = 0 & ~ (all_149_0 = 0))) % 25.98/4.49 | % 25.98/4.49 | ALPHA: (89) implies: % 25.98/4.49 | (90) cC216(iV3102) = all_149_1 % 25.98/4.49 | % 25.98/4.49 | BETA: splitting (74) gives: % 25.98/4.49 | % 25.98/4.49 | Case 1: % 25.98/4.49 | | % 25.98/4.49 | | (91) all_135_1 = 0 % 25.98/4.49 | | % 25.98/4.49 | | REDUCE: (64), (91) imply: % 25.98/4.49 | | (92) cC14(iV3102) = 0 % 25.98/4.49 | | % 25.98/4.49 | | BETA: splitting (77) gives: % 25.98/4.49 | | % 25.98/4.49 | | Case 1: % 25.98/4.49 | | | % 25.98/4.49 | | | (93) all_135_3 = 0 % 25.98/4.49 | | | % 25.98/4.49 | | | REDUCE: (67), (93) imply: % 25.98/4.49 | | | (94) cC28(iV3102) = 0 % 25.98/4.49 | | | % 25.98/4.49 | | | BETA: splitting (78) gives: % 25.98/4.49 | | | % 25.98/4.49 | | | Case 1: % 25.98/4.49 | | | | % 25.98/4.49 | | | | (95) all_135_5 = 0 % 25.98/4.49 | | | | % 25.98/4.49 | | | | BETA: splitting (80) gives: % 25.98/4.49 | | | | % 25.98/4.49 | | | | Case 1: % 25.98/4.49 | | | | | % 25.98/4.49 | | | | | (96) all_135_4 = 0 % 25.98/4.49 | | | | | % 25.98/4.49 | | | | | GROUND_INST: instantiating (33) with all_135_7, all_149_1, iV3102, % 25.98/4.49 | | | | | simplifying with (65), (90) gives: % 25.98/4.49 | | | | | (97) all_149_1 = all_135_7 % 25.98/4.49 | | | | | % 25.98/4.49 | | | | | GROUND_INST: instantiating (33) with 0, all_149_1, iV3102, simplifying % 25.98/4.49 | | | | | with (83), (90) gives: % 25.98/4.49 | | | | | (98) all_149_1 = 0 % 25.98/4.49 | | | | | % 25.98/4.49 | | | | | GROUND_INST: instantiating (34) with all_135_2, all_147_0, iV3102, % 25.98/4.49 | | | | | simplifying with (66), (86) gives: % 25.98/4.49 | | | | | (99) all_147_0 = all_135_2 % 25.98/4.50 | | | | | % 25.98/4.50 | | | | | GROUND_INST: instantiating (40) with all_129_0, all_147_1, iV3102, % 25.98/4.50 | | | | | simplifying with (58), (87) gives: % 25.98/4.50 | | | | | (100) all_147_1 = all_129_0 % 25.98/4.50 | | | | | % 25.98/4.50 | | | | | COMBINE_EQS: (97), (98) imply: % 25.98/4.50 | | | | | (101) all_135_7 = 0 % 25.98/4.50 | | | | | % 25.98/4.50 | | | | | SIMP: (101) implies: % 25.98/4.50 | | | | | (102) all_135_7 = 0 % 25.98/4.50 | | | | | % 25.98/4.50 | | | | | BETA: splitting (88) gives: % 25.98/4.50 | | | | | % 25.98/4.50 | | | | | Case 1: % 25.98/4.50 | | | | | | % 25.98/4.50 | | | | | | (103) all_147_0 = 0 % 25.98/4.50 | | | | | | % 25.98/4.50 | | | | | | COMBINE_EQS: (99), (103) imply: % 25.98/4.50 | | | | | | (104) all_135_2 = 0 % 25.98/4.50 | | | | | | % 25.98/4.50 | | | | | | BETA: splitting (71) gives: % 25.98/4.50 | | | | | | % 25.98/4.50 | | | | | | Case 1: % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | (105) ~ (all_135_0 = 0) % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | REDUCE: (72), (105) imply: % 25.98/4.50 | | | | | | | (106) $false % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | CLOSE: (106) is inconsistent. % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | Case 2: % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | (107) ~ (all_135_1 = 0) | ~ (all_135_2 = 0) | ~ (all_135_3 = % 25.98/4.50 | | | | | | | 0) | ~ (all_135_4 = 0) | ~ (all_135_5 = 0) | ~ % 25.98/4.50 | | | | | | | (all_135_6 = 0) | ~ (all_135_7 = 0) | ? [v0: $i] : ? % 25.98/4.50 | | | | | | | [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 25.98/4.50 | | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( % 25.98/4.50 | | | | | | | ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: % 25.98/4.50 | | | | | | | any] : ? [v2: any] : (cowlNothing(v0) = v2 & % 25.98/4.50 | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | BETA: splitting (107) gives: % 25.98/4.50 | | | | | | | % 25.98/4.50 | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | (108) ~ (all_135_1 = 0) % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | REDUCE: (91), (108) imply: % 25.98/4.50 | | | | | | | | (109) $false % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | CLOSE: (109) is inconsistent. % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | Case 2: % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | (110) ~ (all_135_2 = 0) | ~ (all_135_3 = 0) | ~ (all_135_4 % 25.98/4.50 | | | | | | | | = 0) | ~ (all_135_5 = 0) | ~ (all_135_6 = 0) | ~ % 25.98/4.50 | | | | | | | | (all_135_7 = 0) | ? [v0: $i] : ? [v1: any] : ? [v2: % 25.98/4.50 | | | | | | | | any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 25.98/4.50 | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 25.98/4.50 | | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: % 25.98/4.50 | | | | | | | | any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 25.98/4.50 | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | BETA: splitting (110) gives: % 25.98/4.50 | | | | | | | | % 25.98/4.50 | | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | (111) ~ (all_135_2 = 0) % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | REDUCE: (104), (111) imply: % 25.98/4.50 | | | | | | | | | (112) $false % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | CLOSE: (112) is inconsistent. % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | Case 2: % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | (113) ~ (all_135_3 = 0) | ~ (all_135_4 = 0) | ~ % 25.98/4.50 | | | | | | | | | (all_135_5 = 0) | ~ (all_135_6 = 0) | ~ (all_135_7 % 25.98/4.50 | | | | | | | | | = 0) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.50 | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) % 25.98/4.50 | | | | | | | | | & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 25.98/4.50 | | | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: % 25.98/4.50 | | | | | | | | | any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 25.98/4.50 | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | BETA: splitting (113) gives: % 25.98/4.50 | | | | | | | | | % 25.98/4.50 | | | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | (114) ~ (all_135_3 = 0) % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | REDUCE: (93), (114) imply: % 25.98/4.50 | | | | | | | | | | (115) $false % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | CLOSE: (115) is inconsistent. % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | Case 2: % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | (116) ~ (all_135_4 = 0) | ~ (all_135_5 = 0) | ~ % 25.98/4.50 | | | | | | | | | | (all_135_6 = 0) | ~ (all_135_7 = 0) | ? [v0: $i] % 25.98/4.50 | | | | | | | | | | : ? [v1: any] : ? [v2: any] : (xsd_string(v0) = % 25.98/4.50 | | | | | | | | | | v1 & xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & % 25.98/4.50 | | | | | | | | | | v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? % 25.98/4.50 | | | | | | | | | | [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.50 | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) % 25.98/4.50 | | | | | | | | | | & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | BETA: splitting (116) gives: % 25.98/4.50 | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | (117) ~ (all_135_4 = 0) % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | REDUCE: (96), (117) imply: % 25.98/4.50 | | | | | | | | | | | (118) $false % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | CLOSE: (118) is inconsistent. % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | Case 2: % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | (119) ~ (all_135_5 = 0) | ~ (all_135_6 = 0) | ~ % 25.98/4.50 | | | | | | | | | | | (all_135_7 = 0) | ? [v0: $i] : ? [v1: any] : ? % 25.98/4.50 | | | | | | | | | | | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) % 25.98/4.50 | | | | | | | | | | | = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = % 25.98/4.50 | | | | | | | | | | | 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? % 25.98/4.50 | | | | | | | | | | | [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & % 25.98/4.50 | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 25.98/4.50 | | | | | | | | | | | = 0)) % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | BETA: splitting (119) gives: % 25.98/4.50 | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | (120) ~ (all_135_5 = 0) % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | REDUCE: (95), (120) imply: % 25.98/4.50 | | | | | | | | | | | | (121) $false % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | CLOSE: (121) is inconsistent. % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | Case 2: % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | (122) ~ (all_135_6 = 0) | ~ (all_135_7 = 0) | ? [v0: % 25.98/4.50 | | | | | | | | | | | | $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.50 | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 25.98/4.50 | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 25.98/4.50 | | | | | | | | | | | | (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : % 25.98/4.50 | | | | | | | | | | | | ? [v2: any] : (cowlNothing(v0) = v2 & % 25.98/4.50 | | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 25.98/4.50 | | | | | | | | | | | | = 0)) % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | BETA: splitting (122) gives: % 25.98/4.50 | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | Case 1: % 25.98/4.50 | | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | | (123) ~ (all_135_6 = 0) % 25.98/4.50 | | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | | GROUND_INST: instantiating (39) with all_135_6, 0, iV3102, % 25.98/4.50 | | | | | | | | | | | | | simplifying with (70), (84) gives: % 25.98/4.50 | | | | | | | | | | | | | (124) all_135_6 = 0 % 25.98/4.50 | | | | | | | | | | | | | % 25.98/4.50 | | | | | | | | | | | | | REDUCE: (123), (124) imply: % 25.98/4.51 | | | | | | | | | | | | | (125) $false % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | CLOSE: (125) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | (126) ~ (all_135_7 = 0) | ? [v0: $i] : ? [v1: any] : % 25.98/4.51 | | | | | | | | | | | | | ? [v2: any] : (xsd_string(v0) = v1 & % 25.98/4.51 | | | | | | | | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = % 25.98/4.51 | | | | | | | | | | | | | 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: % 25.98/4.51 | | | | | | | | | | | | | $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.51 | | | | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 25.98/4.51 | | | | | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | BETA: splitting (126) gives: % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | Case 1: % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | (127) ~ (all_135_7 = 0) % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | REDUCE: (102), (127) imply: % 25.98/4.51 | | | | | | | | | | | | | | (128) $false % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | CLOSE: (128) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | (129) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.51 | | | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 25.98/4.51 | | | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 25.98/4.51 | | | | | | | | | | | | | | (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : % 25.98/4.51 | | | | | | | | | | | | | | ? [v2: any] : (cowlNothing(v0) = v2 & % 25.98/4.51 | | | | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 25.98/4.51 | | | | | | | | | | | | | | = 0)) % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | BETA: splitting (129) gives: % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | Case 1: % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | (130) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.51 | | | | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 25.98/4.51 | | | | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 25.98/4.51 | | | | | | | | | | | | | | | (v1 = 0)))) % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | DELTA: instantiating (130) with fresh symbols all_261_0, % 25.98/4.51 | | | | | | | | | | | | | | | all_261_1, all_261_2 gives: % 25.98/4.51 | | | | | | | | | | | | | | | (131) xsd_string(all_261_2) = all_261_1 & % 25.98/4.51 | | | | | | | | | | | | | | | xsd_integer(all_261_2) = all_261_0 & $i(all_261_2) % 25.98/4.51 | | | | | | | | | | | | | | | & ((all_261_0 = 0 & all_261_1 = 0) | ( ~ % 25.98/4.51 | | | | | | | | | | | | | | | (all_261_0 = 0) & ~ (all_261_1 = 0))) % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | ALPHA: (131) implies: % 25.98/4.51 | | | | | | | | | | | | | | | (132) $i(all_261_2) % 25.98/4.51 | | | | | | | | | | | | | | | (133) xsd_integer(all_261_2) = all_261_0 % 25.98/4.51 | | | | | | | | | | | | | | | (134) xsd_string(all_261_2) = all_261_1 % 25.98/4.51 | | | | | | | | | | | | | | | (135) (all_261_0 = 0 & all_261_1 = 0) | ( ~ (all_261_0 = % 25.98/4.51 | | | | | | | | | | | | | | | 0) & ~ (all_261_1 = 0)) % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_261_2, all_261_1, % 25.98/4.51 | | | | | | | | | | | | | | | simplifying with (132), (134) gives: % 25.98/4.51 | | | | | | | | | | | | | | | (136) all_261_1 = 0 | xsd_integer(all_261_2) = 0 % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | BETA: splitting (135) gives: % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | Case 1: % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | (137) all_261_0 = 0 & all_261_1 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | ALPHA: (137) implies: % 25.98/4.51 | | | | | | | | | | | | | | | | (138) all_261_1 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | (139) all_261_0 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | REDUCE: (134), (138) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | (140) xsd_string(all_261_2) = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | REDUCE: (133), (139) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | (141) xsd_integer(all_261_2) = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_261_2, simplifying with % 25.98/4.51 | | | | | | | | | | | | | | | | (132), (140) gives: % 25.98/4.51 | | | | | | | | | | | | | | | | (142) ? [v0: int] : ( ~ (v0 = 0) & % 25.98/4.51 | | | | | | | | | | | | | | | | xsd_integer(all_261_2) = v0) % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | DELTA: instantiating (142) with fresh symbol all_275_0 % 25.98/4.51 | | | | | | | | | | | | | | | | gives: % 25.98/4.51 | | | | | | | | | | | | | | | | (143) ~ (all_275_0 = 0) & xsd_integer(all_261_2) = % 25.98/4.51 | | | | | | | | | | | | | | | | all_275_0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | ALPHA: (143) implies: % 25.98/4.51 | | | | | | | | | | | | | | | | (144) ~ (all_275_0 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | | (145) xsd_integer(all_261_2) = all_275_0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with 0, all_275_0, all_261_2, % 25.98/4.51 | | | | | | | | | | | | | | | | simplifying with (141), (145) gives: % 25.98/4.51 | | | | | | | | | | | | | | | | (146) all_275_0 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | REDUCE: (144), (146) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | (147) $false % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | CLOSE: (147) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | (148) ~ (all_261_0 = 0) & ~ (all_261_1 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | ALPHA: (148) implies: % 25.98/4.51 | | | | | | | | | | | | | | | | (149) ~ (all_261_1 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | | (150) ~ (all_261_0 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | BETA: splitting (136) gives: % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | Case 1: % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | (151) xsd_integer(all_261_2) = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with all_261_0, 0, all_261_2, % 25.98/4.51 | | | | | | | | | | | | | | | | | simplifying with (133), (151) gives: % 25.98/4.51 | | | | | | | | | | | | | | | | | (152) all_261_0 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | REDUCE: (150), (152) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | | (153) $false % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | CLOSE: (153) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | (154) all_261_1 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | REDUCE: (149), (154) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | | (155) $false % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | | CLOSE: (155) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | (156) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 25.98/4.51 | | | | | | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 25.98/4.51 | | | | | | | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | DELTA: instantiating (156) with fresh symbols all_261_0, % 25.98/4.51 | | | | | | | | | | | | | | | all_261_1, all_261_2 gives: % 25.98/4.51 | | | | | | | | | | | | | | | (157) cowlNothing(all_261_2) = all_261_0 & % 25.98/4.51 | | | | | | | | | | | | | | | cowlThing(all_261_2) = all_261_1 & $i(all_261_2) & % 25.98/4.51 | | | | | | | | | | | | | | | ( ~ (all_261_1 = 0) | all_261_0 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | ALPHA: (157) implies: % 25.98/4.51 | | | | | | | | | | | | | | | (158) $i(all_261_2) % 25.98/4.51 | | | | | | | | | | | | | | | (159) cowlThing(all_261_2) = all_261_1 % 25.98/4.51 | | | | | | | | | | | | | | | (160) cowlNothing(all_261_2) = all_261_0 % 25.98/4.51 | | | | | | | | | | | | | | | (161) ~ (all_261_1 = 0) | all_261_0 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_261_2, all_261_1, % 25.98/4.51 | | | | | | | | | | | | | | | simplifying with (158), (159) gives: % 25.98/4.51 | | | | | | | | | | | | | | | (162) all_261_1 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | BETA: splitting (161) gives: % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | Case 1: % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | (163) ~ (all_261_1 = 0) % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | REDUCE: (162), (163) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | (164) $false % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | CLOSE: (164) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | Case 2: % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | (165) all_261_0 = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | REDUCE: (160), (165) imply: % 25.98/4.51 | | | | | | | | | | | | | | | | (166) cowlNothing(all_261_2) = 0 % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with all_261_2, simplifying with % 25.98/4.51 | | | | | | | | | | | | | | | | (158), (166) gives: % 25.98/4.51 | | | | | | | | | | | | | | | | (167) $false % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | | CLOSE: (167) is inconsistent. % 25.98/4.51 | | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | | % 25.98/4.51 | | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | | % 25.98/4.51 | | | | | | | | | End of split % 25.98/4.51 | | | | | | | | | % 25.98/4.51 | | | | | | | | End of split % 25.98/4.51 | | | | | | | | % 25.98/4.51 | | | | | | | End of split % 25.98/4.51 | | | | | | | % 25.98/4.51 | | | | | | End of split % 25.98/4.51 | | | | | | % 25.98/4.51 | | | | | Case 2: % 25.98/4.51 | | | | | | % 25.98/4.51 | | | | | | (168) all_147_1 = 0 % 25.98/4.51 | | | | | | % 25.98/4.51 | | | | | | COMBINE_EQS: (100), (168) imply: % 25.98/4.52 | | | | | | (169) all_129_0 = 0 % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | REDUCE: (57), (169) imply: % 25.98/4.52 | | | | | | (170) $false % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | CLOSE: (170) is inconsistent. % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | End of split % 25.98/4.52 | | | | | % 25.98/4.52 | | | | Case 2: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | (171) ? [v0: any] : ? [v1: any] : (cC42(iV3102) = v1 & % 25.98/4.52 | | | | | cC32(iV3102) = v0 & (v1 = 0 | v0 = 0)) % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | DELTA: instantiating (171) with fresh symbols all_183_0, all_183_1 % 25.98/4.52 | | | | | gives: % 25.98/4.52 | | | | | (172) cC42(iV3102) = all_183_0 & cC32(iV3102) = all_183_1 & % 25.98/4.52 | | | | | (all_183_0 = 0 | all_183_1 = 0) % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | ALPHA: (172) implies: % 25.98/4.52 | | | | | (173) cC32(iV3102) = all_183_1 % 25.98/4.52 | | | | | (174) cC42(iV3102) = all_183_0 % 25.98/4.52 | | | | | (175) all_183_0 = 0 | all_183_1 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | GROUND_INST: instantiating (37) with all_119_0, all_183_1, iV3102, % 25.98/4.52 | | | | | simplifying with (46), (173) gives: % 25.98/4.52 | | | | | (176) all_183_1 = all_119_0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | GROUND_INST: instantiating (38) with all_125_0, all_183_0, iV3102, % 25.98/4.52 | | | | | simplifying with (55), (174) gives: % 25.98/4.52 | | | | | (177) all_183_0 = all_125_0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | BETA: splitting (175) gives: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | Case 1: % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | (178) all_183_0 = 0 % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | COMBINE_EQS: (177), (178) imply: % 25.98/4.52 | | | | | | (179) all_125_0 = 0 % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | REDUCE: (54), (179) imply: % 25.98/4.52 | | | | | | (180) $false % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | CLOSE: (180) is inconsistent. % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | Case 2: % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | (181) all_183_1 = 0 % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | COMBINE_EQS: (176), (181) imply: % 25.98/4.52 | | | | | | (182) all_119_0 = 0 % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | REDUCE: (45), (182) imply: % 25.98/4.52 | | | | | | (183) $false % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | CLOSE: (183) is inconsistent. % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | End of split % 25.98/4.52 | | | | | % 25.98/4.52 | | | | End of split % 25.98/4.52 | | | | % 25.98/4.52 | | | Case 2: % 25.98/4.52 | | | | % 25.98/4.52 | | | | (184) ? [v0: any] : ? [v1: any] : (cC28(iV3102) = v1 & cC14(iV3102) % 25.98/4.52 | | | | = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 25.98/4.52 | | | | % 25.98/4.52 | | | | DELTA: instantiating (184) with fresh symbols all_179_0, all_179_1 % 25.98/4.52 | | | | gives: % 25.98/4.52 | | | | (185) cC28(iV3102) = all_179_0 & cC14(iV3102) = all_179_1 & ( ~ % 25.98/4.52 | | | | (all_179_0 = 0) | ~ (all_179_1 = 0)) % 25.98/4.52 | | | | % 25.98/4.52 | | | | ALPHA: (185) implies: % 25.98/4.52 | | | | (186) cC14(iV3102) = all_179_1 % 25.98/4.52 | | | | (187) cC28(iV3102) = all_179_0 % 25.98/4.52 | | | | (188) ~ (all_179_0 = 0) | ~ (all_179_1 = 0) % 25.98/4.52 | | | | % 25.98/4.52 | | | | BETA: splitting (79) gives: % 25.98/4.52 | | | | % 25.98/4.52 | | | | Case 1: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | (189) all_125_0 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | REDUCE: (54), (189) imply: % 25.98/4.52 | | | | | (190) $false % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | CLOSE: (190) is inconsistent. % 25.98/4.52 | | | | | % 25.98/4.52 | | | | Case 2: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | GROUND_INST: instantiating (32) with 0, all_179_1, iV3102, simplifying % 25.98/4.52 | | | | | with (92), (186) gives: % 25.98/4.52 | | | | | (191) all_179_1 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | GROUND_INST: instantiating (36) with 0, all_179_0, iV3102, simplifying % 25.98/4.52 | | | | | with (94), (187) gives: % 25.98/4.52 | | | | | (192) all_179_0 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | BETA: splitting (188) gives: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | Case 1: % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | (193) ~ (all_179_0 = 0) % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | REDUCE: (192), (193) imply: % 25.98/4.52 | | | | | | (194) $false % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | CLOSE: (194) is inconsistent. % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | Case 2: % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | (195) ~ (all_179_1 = 0) % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | REDUCE: (191), (195) imply: % 25.98/4.52 | | | | | | (196) $false % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | | CLOSE: (196) is inconsistent. % 25.98/4.52 | | | | | | % 25.98/4.52 | | | | | End of split % 25.98/4.52 | | | | | % 25.98/4.52 | | | | End of split % 25.98/4.52 | | | | % 25.98/4.52 | | | End of split % 25.98/4.52 | | | % 25.98/4.52 | | Case 2: % 25.98/4.52 | | | % 25.98/4.52 | | | (197) ? [v0: any] : ? [v1: any] : (cC26(iV3102) = v0 & cC16(iV3102) = % 25.98/4.52 | | | v1 & (v1 = 0 | v0 = 0)) % 25.98/4.52 | | | % 25.98/4.52 | | | BETA: splitting (73) gives: % 25.98/4.52 | | | % 25.98/4.52 | | | Case 1: % 25.98/4.52 | | | | % 25.98/4.52 | | | | (198) all_121_0 = 0 % 25.98/4.52 | | | | % 25.98/4.52 | | | | REDUCE: (48), (198) imply: % 25.98/4.52 | | | | (199) $false % 25.98/4.52 | | | | % 25.98/4.52 | | | | CLOSE: (199) is inconsistent. % 25.98/4.52 | | | | % 25.98/4.52 | | | Case 2: % 25.98/4.52 | | | | % 25.98/4.52 | | | | % 25.98/4.52 | | | | DELTA: instantiating (197) with fresh symbols all_183_0, all_183_1 % 25.98/4.52 | | | | gives: % 25.98/4.52 | | | | (200) cC26(iV3102) = all_183_1 & cC16(iV3102) = all_183_0 & % 25.98/4.52 | | | | (all_183_0 = 0 | all_183_1 = 0) % 25.98/4.52 | | | | % 25.98/4.52 | | | | ALPHA: (200) implies: % 25.98/4.52 | | | | (201) cC16(iV3102) = all_183_0 % 25.98/4.52 | | | | (202) cC26(iV3102) = all_183_1 % 25.98/4.52 | | | | (203) all_183_0 = 0 | all_183_1 = 0 % 25.98/4.52 | | | | % 25.98/4.52 | | | | GROUND_INST: instantiating (30) with all_131_0, all_183_0, iV3102, % 25.98/4.52 | | | | simplifying with (61), (201) gives: % 25.98/4.52 | | | | (204) all_183_0 = all_131_0 % 25.98/4.52 | | | | % 25.98/4.52 | | | | GROUND_INST: instantiating (35) with all_123_0, all_183_1, iV3102, % 25.98/4.52 | | | | simplifying with (52), (202) gives: % 25.98/4.52 | | | | (205) all_183_1 = all_123_0 % 25.98/4.52 | | | | % 25.98/4.52 | | | | BETA: splitting (203) gives: % 25.98/4.52 | | | | % 25.98/4.52 | | | | Case 1: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | (206) all_183_0 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | COMBINE_EQS: (204), (206) imply: % 25.98/4.52 | | | | | (207) all_131_0 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | REDUCE: (60), (207) imply: % 25.98/4.52 | | | | | (208) $false % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | CLOSE: (208) is inconsistent. % 25.98/4.52 | | | | | % 25.98/4.52 | | | | Case 2: % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | (209) all_183_1 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | COMBINE_EQS: (205), (209) imply: % 25.98/4.52 | | | | | (210) all_123_0 = 0 % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | REDUCE: (51), (210) imply: % 25.98/4.52 | | | | | (211) $false % 25.98/4.52 | | | | | % 25.98/4.52 | | | | | CLOSE: (211) is inconsistent. % 25.98/4.52 | | | | | % 25.98/4.52 | | | | End of split % 25.98/4.52 | | | | % 25.98/4.52 | | | End of split % 25.98/4.52 | | | % 25.98/4.52 | | End of split % 25.98/4.52 | | % 25.98/4.52 | Case 2: % 25.98/4.52 | | % 25.98/4.52 | | (212) ? [v0: any] : ? [v1: any] : (cC12(iV3102) = v0 & cC2(iV3102) = v1 % 25.98/4.52 | | & (v1 = 0 | v0 = 0)) % 25.98/4.52 | | % 25.98/4.52 | | BETA: splitting (76) gives: % 25.98/4.52 | | % 25.98/4.52 | | Case 1: % 25.98/4.52 | | | % 25.98/4.52 | | | (213) all_123_0 = 0 % 25.98/4.52 | | | % 25.98/4.52 | | | REDUCE: (51), (213) imply: % 25.98/4.52 | | | (214) $false % 26.40/4.52 | | | % 26.40/4.52 | | | CLOSE: (214) is inconsistent. % 26.40/4.52 | | | % 26.40/4.52 | | Case 2: % 26.40/4.52 | | | % 26.40/4.52 | | | % 26.40/4.52 | | | DELTA: instantiating (212) with fresh symbols all_159_0, all_159_1 gives: % 26.40/4.52 | | | (215) cC12(iV3102) = all_159_1 & cC2(iV3102) = all_159_0 & (all_159_0 = % 26.40/4.52 | | | 0 | all_159_1 = 0) % 26.40/4.52 | | | % 26.40/4.52 | | | ALPHA: (215) implies: % 26.40/4.52 | | | (216) cC2(iV3102) = all_159_0 % 26.40/4.52 | | | (217) cC12(iV3102) = all_159_1 % 26.40/4.52 | | | (218) all_159_0 = 0 | all_159_1 = 0 % 26.40/4.52 | | | % 26.40/4.52 | | | BETA: splitting (79) gives: % 26.40/4.52 | | | % 26.40/4.52 | | | Case 1: % 26.40/4.52 | | | | % 26.40/4.52 | | | | (219) all_125_0 = 0 % 26.40/4.52 | | | | % 26.40/4.52 | | | | REDUCE: (54), (219) imply: % 26.40/4.52 | | | | (220) $false % 26.40/4.52 | | | | % 26.40/4.52 | | | | CLOSE: (220) is inconsistent. % 26.40/4.52 | | | | % 26.40/4.52 | | | Case 2: % 26.40/4.52 | | | | % 26.40/4.52 | | | | % 26.40/4.52 | | | | GROUND_INST: instantiating (29) with all_117_0, all_159_0, iV3102, % 26.40/4.52 | | | | simplifying with (43), (216) gives: % 26.40/4.52 | | | | (221) all_159_0 = all_117_0 % 26.40/4.52 | | | | % 26.40/4.52 | | | | GROUND_INST: instantiating (31) with all_121_0, all_159_1, iV3102, % 26.40/4.52 | | | | simplifying with (49), (217) gives: % 26.40/4.52 | | | | (222) all_159_1 = all_121_0 % 26.40/4.52 | | | | % 26.40/4.52 | | | | BETA: splitting (218) gives: % 26.40/4.52 | | | | % 26.40/4.52 | | | | Case 1: % 26.40/4.52 | | | | | % 26.40/4.53 | | | | | (223) all_159_0 = 0 % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | COMBINE_EQS: (221), (223) imply: % 26.40/4.53 | | | | | (224) all_117_0 = 0 % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | REDUCE: (42), (224) imply: % 26.40/4.53 | | | | | (225) $false % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | CLOSE: (225) is inconsistent. % 26.40/4.53 | | | | | % 26.40/4.53 | | | | Case 2: % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | (226) all_159_1 = 0 % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | COMBINE_EQS: (222), (226) imply: % 26.40/4.53 | | | | | (227) all_121_0 = 0 % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | REDUCE: (48), (227) imply: % 26.40/4.53 | | | | | (228) $false % 26.40/4.53 | | | | | % 26.40/4.53 | | | | | CLOSE: (228) is inconsistent. % 26.40/4.53 | | | | | % 26.40/4.53 | | | | End of split % 26.40/4.53 | | | | % 26.40/4.53 | | | End of split % 26.40/4.53 | | | % 26.40/4.53 | | End of split % 26.40/4.53 | | % 26.40/4.53 | End of split % 26.40/4.53 | % 26.40/4.53 End of proof % 26.40/4.53 % SZS output end Proof for theBenchmark % 26.40/4.53 % 26.40/4.53 3905ms %------------------------------------------------------------------------------