%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KRS158+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 : n009.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:29 EDT 2023 % Result : Theorem 8.89s 1.94s % Output : Proof 12.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS158+1 : TPTP v8.1.2. Released v3.1.0. % 0.07/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Aug 28 01:47:50 EDT 2023 % 0.12/0.34 % CPUTime : % 0.67/0.64 ________ _____ % 0.67/0.64 ___ __ \_________(_)________________________________ % 0.67/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.64 % 0.67/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.64 (2023-06-19) % 0.67/0.64 % 0.67/0.64 (c) Philipp Rümmer, 2009-2023 % 0.67/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.64 Amanda Stjerna. % 0.67/0.64 Free software under BSD-3-Clause. % 0.67/0.64 % 0.67/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.64 % 0.67/0.64 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.67/0.65 Running up to 7 provers in parallel. % 0.67/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.63/1.10 Prover 1: Preprocessing ... % 2.63/1.10 Prover 4: Preprocessing ... % 2.94/1.14 Prover 3: Preprocessing ... % 2.94/1.14 Prover 0: Preprocessing ... % 2.94/1.14 Prover 2: Preprocessing ... % 2.94/1.14 Prover 6: Preprocessing ... % 2.94/1.15 Prover 5: Preprocessing ... % 5.27/1.49 Prover 2: Proving ... % 5.27/1.50 Prover 5: Proving ... % 6.15/1.65 Prover 1: Constructing countermodel ... % 6.15/1.65 Prover 6: Proving ... % 6.92/1.69 Prover 3: Constructing countermodel ... % 6.92/1.73 Prover 4: Constructing countermodel ... % 7.45/1.81 Prover 0: Proving ... % 8.29/1.94 Prover 3: proved (1277ms) % 8.29/1.94 % 8.89/1.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.89/1.94 % 8.89/1.94 Prover 5: stopped % 8.89/1.94 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.89/1.94 Prover 6: stopped % 8.89/1.95 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.89/1.95 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 8.89/1.95 Prover 0: stopped % 8.89/1.95 Prover 2: stopped % 8.89/1.96 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.89/1.96 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 9.13/2.03 Prover 11: Preprocessing ... % 9.54/2.04 Prover 7: Preprocessing ... % 9.67/2.06 Prover 8: Preprocessing ... % 9.67/2.06 Prover 10: Preprocessing ... % 9.67/2.07 Prover 13: Preprocessing ... % 10.13/2.13 Prover 7: Warning: ignoring some quantifiers % 10.13/2.13 Prover 10: Warning: ignoring some quantifiers % 10.13/2.14 Prover 7: Constructing countermodel ... % 10.13/2.15 Prover 10: Constructing countermodel ... % 10.55/2.18 Prover 13: Warning: ignoring some quantifiers % 10.55/2.19 Prover 13: Constructing countermodel ... % 11.16/2.26 Prover 8: Warning: ignoring some quantifiers % 11.16/2.28 Prover 8: Constructing countermodel ... % 11.41/2.32 Prover 11: Constructing countermodel ... % 11.80/2.37 Prover 1: Found proof (size 140) % 11.80/2.37 Prover 1: proved (1710ms) % 11.80/2.37 Prover 11: stopped % 11.80/2.37 Prover 8: stopped % 11.80/2.37 Prover 13: stopped % 11.80/2.37 Prover 10: stopped % 11.80/2.37 Prover 4: stopped % 11.80/2.37 Prover 7: stopped % 11.80/2.37 % 11.80/2.37 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.80/2.37 % 11.80/2.40 % SZS output start Proof for theBenchmark % 11.80/2.40 Assumptions after simplification: % 11.80/2.40 --------------------------------- % 11.80/2.40 % 11.80/2.40 (axiom_0) % 12.19/2.43 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ $i(v0)) & % 12.19/2.43 ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 12.19/2.43 % 12.19/2.43 (axiom_1) % 12.19/2.43 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ $i(v0) | % 12.19/2.43 xsd_integer(v0) = 0) & ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | % 12.19/2.43 ? [v1: int] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) % 12.19/2.43 % 12.19/2.43 (axiom_14) % 12.19/2.43 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC6(v0) = v1) | ~ $i(v0) | ? [v2: % 12.19/2.43 any] : ? [v3: any] : (cC4xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 = % 12.19/2.43 0) | ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC6(v0) = 0) | ~ $i(v0) | % 12.19/2.43 (cC4xcomp(v0) = 0 & cC2xcomp(v0) = 0)) % 12.19/2.43 % 12.19/2.43 (axiom_16) % 12.19/2.43 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cTEST(v0) = v1) | ~ $i(v0) | ? % 12.19/2.43 [v2: any] : ? [v3: any] : (cTOP(v0) = v2 & cC18(v0) = v3 & ( ~ (v3 = 0) | % 12.19/2.44 ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | % 12.19/2.44 (cTOP(v0) = 0 & cC18(v0) = 0)) % 12.19/2.44 % 12.19/2.44 (axiom_17) % 12.19/2.44 cowlThing(iV16560) = 0 & $i(iV16560) % 12.19/2.44 % 12.19/2.44 (axiom_18) % 12.19/2.44 cTEST(iV16560) = 0 & $i(iV16560) % 12.19/2.44 % 12.19/2.44 (axiom_19) % 12.19/2.44 cTOP(iV16560) = 0 & $i(iV16560) % 12.19/2.44 % 12.19/2.44 (axiom_22) % 12.19/2.44 cowlThing(iV16561) = 0 & $i(iV16561) % 12.19/2.44 % 12.19/2.44 (axiom_24) % 12.19/2.44 cC4xcomp(iV16561) = 0 & $i(iV16561) % 12.19/2.44 % 12.19/2.44 (axiom_25) % 12.19/2.44 cC2xcomp(iV16561) = 0 & $i(iV16561) % 12.19/2.44 % 12.19/2.44 (axiom_26) % 12.19/2.44 cowlThing(iV16562) = 0 & $i(iV16562) % 12.19/2.44 % 12.19/2.44 (axiom_28) % 12.19/2.44 cC10xcomp(iV16562) = 0 & $i(iV16562) % 12.19/2.44 % 12.19/2.44 (axiom_29) % 12.19/2.44 cC2xcomp(iV16562) = 0 & $i(iV16562) % 12.19/2.44 % 12.19/2.44 (axiom_5) % 12.19/2.44 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ $i(v0) | ? % 12.19/2.44 [v2: any] : ? [v3: any] : (cC10xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 % 12.19/2.44 = 0) | ~ (v2 = 0)))) & ! [v0: $i] : ( ~ (cC12(v0) = 0) | ~ $i(v0) | % 12.19/2.44 (cC10xcomp(v0) = 0 & cC2xcomp(v0) = 0)) % 12.19/2.44 % 12.19/2.44 (axiom_7) % 12.19/2.45 ! [v0: $i] : ! [v1: any] : ( ~ (cC8(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 12.19/2.45 ? [v3: any] : (cC16(v0) = v2 & cC14(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = % 12.19/2.45 0)))) & ! [v0: $i] : ( ~ (cC8(v0) = 0) | ~ $i(v0) | ? [v1: any] : % 12.19/2.45 ? [v2: any] : (cC16(v0) = v2 & cC14(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 12.19/2.45 % 12.19/2.45 (axiom_8) % 12.19/2.45 ! [v0: $i] : ! [v1: any] : ( ~ (cTOP(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 12.19/2.45 ? [v3: any] : (cC18(v0) = v2 & cC16(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = % 12.19/2.45 0)))) & ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: any] : % 12.19/2.45 ? [v2: any] : (cC18(v0) = v2 & cC16(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 12.19/2.45 % 12.19/2.45 (the_axiom) % 12.19/2.45 $i(iV16561) & $i(iV16562) & $i(iV16560) & ? [v0: any] : ? [v1: any] : ? % 12.19/2.45 [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? % 12.19/2.45 [v7: any] : ? [v8: any] : (cC6(iV16561) = v5 & cC18(iV16560) = v0 & % 12.19/2.45 cC8(iV16560) = v2 & cC16(iV16560) = v3 & cC14(iV16560) = v1 & cC12(iV16562) % 12.19/2.45 = v7 & cowlThing(iV16561) = v6 & cowlThing(iV16562) = v8 & % 12.19/2.45 cowlThing(iV16560) = v4 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 % 12.19/2.45 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 12.19/2.45 0) | ? [v9: $i] : ? [v10: any] : ? [v11: any] : (xsd_string(v9) = v10 % 12.19/2.45 & xsd_integer(v9) = v11 & $i(v9) & ((v11 = 0 & v10 = 0) | ( ~ (v11 = 0) % 12.19/2.45 & ~ (v10 = 0)))) | ? [v9: $i] : ? [v10: any] : ? [v11: any] : % 12.19/2.45 (cowlNothing(v9) = v11 & cowlThing(v9) = v10 & $i(v9) & ( ~ (v10 = 0) | % 12.19/2.45 v11 = 0)))) % 12.19/2.45 % 12.19/2.45 (function-axioms) % 12.48/2.46 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 12.48/2.46 [v3: $i] : (v1 = v0 | ~ (ra_Px6(v3, v2) = v1) | ~ (ra_Px6(v3, v2) = v0)) & % 12.48/2.46 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 12.48/2.46 $i] : (v1 = v0 | ~ (ra_Px1(v3, v2) = v1) | ~ (ra_Px1(v3, v2) = v0)) & ! % 12.48/2.46 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 12.48/2.46 $i] : (v1 = v0 | ~ (rR1(v3, v2) = v1) | ~ (rR1(v3, v2) = v0)) & ! [v0: % 12.48/2.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 12.48/2.46 : (v1 = v0 | ~ (ra_Px3(v3, v2) = v1) | ~ (ra_Px3(v3, v2) = v0)) & ! [v0: % 12.48/2.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 12.48/2.46 ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 12.48/2.46 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC6(v2) = v1) | ~ % 12.48/2.46 (cC6(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 12.48/2.46 ! [v2: $i] : (v1 = v0 | ~ (cC4xcomp(v2) = v1) | ~ (cC4xcomp(v2) = v0)) & ! % 12.48/2.46 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 12.48/2.46 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 12.48/2.46 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ % 12.48/2.46 (cC2(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 12.48/2.46 ! [v2: $i] : (v1 = v0 | ~ (cTOP(v2) = v1) | ~ (cTOP(v2) = v0)) & ! [v0: % 12.48/2.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 12.48/2.46 ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 12.48/2.46 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC8(v2) = v1) | ~ % 12.48/2.46 (cC8(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 12.48/2.46 ! [v2: $i] : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) & ! [v0: % 12.48/2.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 12.48/2.46 ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 12.48/2.46 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cC12(v2) = v1) | ~ % 12.48/2.46 (cC12(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 12.48/2.46 ! [v2: $i] : (v1 = v0 | ~ (cC10xcomp(v2) = v1) | ~ (cC10xcomp(v2) = v0)) & % 12.48/2.46 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 12.48/2.46 v0 | ~ (cC2xcomp(v2) = v1) | ~ (cC2xcomp(v2) = v0)) & ! [v0: % 12.48/2.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 12.48/2.46 ~ (cC10(v2) = v1) | ~ (cC10(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 12.48/2.46 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (xsd_string(v2) = v1) | % 12.48/2.46 ~ (xsd_string(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 12.48/2.46 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ % 12.48/2.46 (xsd_integer(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 12.48/2.46 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cowlNothing(v2) = v1) | ~ % 12.48/2.46 (cowlNothing(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 12.48/2.46 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ % 12.48/2.46 (cowlThing(v2) = v0)) % 12.48/2.46 % 12.48/2.46 Further assumptions not needed in the proof: % 12.48/2.46 -------------------------------------------- % 12.48/2.46 axiom_10, axiom_11, axiom_12, axiom_13, axiom_15, axiom_2, axiom_20, axiom_21, % 12.48/2.46 axiom_23, axiom_27, axiom_3, axiom_4, axiom_6, axiom_9 % 12.48/2.46 % 12.48/2.46 Those formulas are unsatisfiable: % 12.48/2.46 --------------------------------- % 12.48/2.46 % 12.48/2.46 Begin of proof % 12.48/2.46 | % 12.48/2.46 | ALPHA: (axiom_0) implies: % 12.48/2.47 | (1) ! [v0: $i] : ( ~ (cowlNothing(v0) = 0) | ~ $i(v0)) % 12.48/2.47 | (2) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cowlThing(v0) = v1) | ~ % 12.48/2.47 | $i(v0)) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_1) implies: % 12.48/2.47 | (3) ! [v0: $i] : ( ~ (xsd_string(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ % 12.48/2.47 | (v1 = 0) & xsd_integer(v0) = v1)) % 12.48/2.47 | (4) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (xsd_string(v0) = v1) | ~ % 12.48/2.47 | $i(v0) | xsd_integer(v0) = 0) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_5) implies: % 12.48/2.47 | (5) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ $i(v0) | % 12.48/2.47 | ? [v2: any] : ? [v3: any] : (cC10xcomp(v0) = v2 & cC2xcomp(v0) = v3 % 12.48/2.47 | & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_7) implies: % 12.48/2.47 | (6) ! [v0: $i] : ! [v1: any] : ( ~ (cC8(v0) = v1) | ~ $i(v0) | ? [v2: % 12.48/2.47 | any] : ? [v3: any] : (cC16(v0) = v2 & cC14(v0) = v3 & ( ~ (v2 = 0) % 12.48/2.47 | | (v3 = 0 & v1 = 0)))) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_8) implies: % 12.48/2.47 | (7) ! [v0: $i] : ( ~ (cTOP(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? [v2: % 12.48/2.47 | any] : (cC18(v0) = v2 & cC16(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 12.48/2.47 | (8) ! [v0: $i] : ! [v1: any] : ( ~ (cTOP(v0) = v1) | ~ $i(v0) | ? [v2: % 12.48/2.47 | any] : ? [v3: any] : (cC18(v0) = v2 & cC16(v0) = v3 & ( ~ (v2 = 0) % 12.48/2.47 | | (v3 = 0 & v1 = 0)))) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_14) implies: % 12.48/2.47 | (9) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (cC6(v0) = v1) | ~ $i(v0) | % 12.48/2.47 | ? [v2: any] : ? [v3: any] : (cC4xcomp(v0) = v2 & cC2xcomp(v0) = v3 & % 12.48/2.47 | ( ~ (v3 = 0) | ~ (v2 = 0)))) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_16) implies: % 12.48/2.47 | (10) ! [v0: $i] : ( ~ (cTEST(v0) = 0) | ~ $i(v0) | (cTOP(v0) = 0 & % 12.48/2.47 | cC18(v0) = 0)) % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_17) implies: % 12.48/2.47 | (11) cowlThing(iV16560) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_18) implies: % 12.48/2.47 | (12) cTEST(iV16560) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_19) implies: % 12.48/2.47 | (13) cTOP(iV16560) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_22) implies: % 12.48/2.47 | (14) cowlThing(iV16561) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_24) implies: % 12.48/2.47 | (15) cC4xcomp(iV16561) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_25) implies: % 12.48/2.47 | (16) cC2xcomp(iV16561) = 0 % 12.48/2.47 | % 12.48/2.47 | ALPHA: (axiom_26) implies: % 12.48/2.47 | (17) cowlThing(iV16562) = 0 % 12.48/2.48 | % 12.48/2.48 | ALPHA: (axiom_28) implies: % 12.48/2.48 | (18) cC10xcomp(iV16562) = 0 % 12.48/2.48 | % 12.48/2.48 | ALPHA: (axiom_29) implies: % 12.48/2.48 | (19) cC2xcomp(iV16562) = 0 % 12.48/2.48 | % 12.48/2.48 | ALPHA: (the_axiom) implies: % 12.48/2.48 | (20) $i(iV16560) % 12.48/2.48 | (21) $i(iV16562) % 12.48/2.48 | (22) $i(iV16561) % 12.48/2.48 | (23) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 12.48/2.48 | any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 12.48/2.48 | (cC6(iV16561) = v5 & cC18(iV16560) = v0 & cC8(iV16560) = v2 & % 12.48/2.48 | cC16(iV16560) = v3 & cC14(iV16560) = v1 & cC12(iV16562) = v7 & % 12.48/2.48 | cowlThing(iV16561) = v6 & cowlThing(iV16562) = v8 & % 12.48/2.48 | cowlThing(iV16560) = v4 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 12.48/2.48 | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = % 12.48/2.48 | 0) | ~ (v0 = 0) | ? [v9: $i] : ? [v10: any] : ? [v11: any] : % 12.48/2.48 | (xsd_string(v9) = v10 & xsd_integer(v9) = v11 & $i(v9) & ((v11 = 0 % 12.48/2.48 | & v10 = 0) | ( ~ (v11 = 0) & ~ (v10 = 0)))) | ? [v9: $i] : % 12.48/2.48 | ? [v10: any] : ? [v11: any] : (cowlNothing(v9) = v11 & % 12.48/2.48 | cowlThing(v9) = v10 & $i(v9) & ( ~ (v10 = 0) | v11 = 0)))) % 12.48/2.48 | % 12.48/2.48 | ALPHA: (function-axioms) implies: % 12.48/2.48 | (24) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 12.48/2.48 | (25) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 12.48/2.48 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC2xcomp(v2) = v1) | ~ (cC2xcomp(v2) = v0)) % 12.48/2.48 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC10xcomp(v2) = v1) | ~ (cC10xcomp(v2) = v0)) % 12.48/2.48 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) % 12.48/2.48 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) % 12.48/2.48 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) % 12.48/2.48 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 12.48/2.48 | : (v1 = v0 | ~ (cC4xcomp(v2) = v1) | ~ (cC4xcomp(v2) = v0)) % 12.48/2.48 | % 12.48/2.48 | DELTA: instantiating (23) with fresh symbols all_23_0, all_23_1, all_23_2, % 12.48/2.48 | all_23_3, all_23_4, all_23_5, all_23_6, all_23_7, all_23_8 gives: % 12.48/2.49 | (32) cC6(iV16561) = all_23_3 & cC18(iV16560) = all_23_8 & cC8(iV16560) = % 12.48/2.49 | all_23_6 & cC16(iV16560) = all_23_5 & cC14(iV16560) = all_23_7 & % 12.48/2.49 | cC12(iV16562) = all_23_1 & cowlThing(iV16561) = all_23_2 & % 12.48/2.49 | cowlThing(iV16562) = all_23_0 & cowlThing(iV16560) = all_23_4 & ( ~ % 12.48/2.49 | (all_23_0 = 0) | ~ (all_23_1 = 0) | ~ (all_23_2 = 0) | ~ % 12.48/2.49 | (all_23_3 = 0) | ~ (all_23_4 = 0) | ~ (all_23_5 = 0) | ~ % 12.48/2.49 | (all_23_6 = 0) | ~ (all_23_7 = 0) | ~ (all_23_8 = 0) | ? [v0: $i] % 12.48/2.49 | : ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 12.48/2.49 | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) % 12.48/2.49 | & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.49 | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | % 12.48/2.49 | v2 = 0))) % 12.48/2.49 | % 12.48/2.49 | ALPHA: (32) implies: % 12.48/2.49 | (33) cowlThing(iV16560) = all_23_4 % 12.48/2.49 | (34) cowlThing(iV16562) = all_23_0 % 12.48/2.49 | (35) cowlThing(iV16561) = all_23_2 % 12.48/2.49 | (36) cC12(iV16562) = all_23_1 % 12.48/2.49 | (37) cC14(iV16560) = all_23_7 % 12.48/2.49 | (38) cC16(iV16560) = all_23_5 % 12.48/2.49 | (39) cC8(iV16560) = all_23_6 % 12.48/2.49 | (40) cC18(iV16560) = all_23_8 % 12.48/2.49 | (41) cC6(iV16561) = all_23_3 % 12.48/2.49 | (42) ~ (all_23_0 = 0) | ~ (all_23_1 = 0) | ~ (all_23_2 = 0) | ~ % 12.48/2.49 | (all_23_3 = 0) | ~ (all_23_4 = 0) | ~ (all_23_5 = 0) | ~ (all_23_6 % 12.48/2.49 | = 0) | ~ (all_23_7 = 0) | ~ (all_23_8 = 0) | ? [v0: $i] : ? [v1: % 12.48/2.49 | any] : ? [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.49 | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? % 12.48/2.49 | [v0: $i] : ? [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & % 12.48/2.49 | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.49 | % 12.48/2.49 | GROUND_INST: instantiating (24) with 0, all_23_4, iV16560, simplifying with % 12.48/2.49 | (11), (33) gives: % 12.48/2.49 | (43) all_23_4 = 0 % 12.48/2.49 | % 12.48/2.49 | GROUND_INST: instantiating (24) with 0, all_23_0, iV16562, simplifying with % 12.48/2.49 | (17), (34) gives: % 12.48/2.49 | (44) all_23_0 = 0 % 12.48/2.49 | % 12.48/2.49 | GROUND_INST: instantiating (24) with 0, all_23_2, iV16561, simplifying with % 12.48/2.49 | (14), (35) gives: % 12.48/2.49 | (45) all_23_2 = 0 % 12.48/2.49 | % 12.48/2.49 | GROUND_INST: instantiating (5) with iV16562, all_23_1, simplifying with (21), % 12.48/2.49 | (36) gives: % 12.48/2.49 | (46) all_23_1 = 0 | ? [v0: any] : ? [v1: any] : (cC10xcomp(iV16562) = v0 % 12.48/2.49 | & cC2xcomp(iV16562) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 12.48/2.49 | % 12.48/2.49 | GROUND_INST: instantiating (6) with iV16560, all_23_6, simplifying with (20), % 12.48/2.49 | (39) gives: % 12.48/2.49 | (47) ? [v0: any] : ? [v1: any] : (cC16(iV16560) = v0 & cC14(iV16560) = v1 % 12.48/2.49 | & ( ~ (v0 = 0) | (v1 = 0 & all_23_6 = 0))) % 12.48/2.49 | % 12.48/2.50 | GROUND_INST: instantiating (7) with iV16560, simplifying with (13), (20) % 12.48/2.50 | gives: % 12.48/2.50 | (48) ? [v0: any] : ? [v1: any] : (cC18(iV16560) = v1 & cC16(iV16560) = v0 % 12.48/2.50 | & ( ~ (v0 = 0) | v1 = 0)) % 12.48/2.50 | % 12.48/2.50 | GROUND_INST: instantiating (8) with iV16560, 0, simplifying with (13), (20) % 12.48/2.50 | gives: % 12.48/2.50 | (49) ? [v0: any] : ? [v1: any] : (cC18(iV16560) = v0 & cC16(iV16560) = v1 % 12.48/2.50 | & ( ~ (v0 = 0) | v1 = 0)) % 12.48/2.50 | % 12.48/2.50 | GROUND_INST: instantiating (9) with iV16561, all_23_3, simplifying with (22), % 12.48/2.50 | (41) gives: % 12.48/2.50 | (50) all_23_3 = 0 | ? [v0: any] : ? [v1: any] : (cC4xcomp(iV16561) = v0 & % 12.48/2.50 | cC2xcomp(iV16561) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 12.48/2.50 | % 12.48/2.50 | GROUND_INST: instantiating (10) with iV16560, simplifying with (12), (20) % 12.48/2.50 | gives: % 12.48/2.50 | (51) cTOP(iV16560) = 0 & cC18(iV16560) = 0 % 12.48/2.50 | % 12.48/2.50 | ALPHA: (51) implies: % 12.48/2.50 | (52) cC18(iV16560) = 0 % 12.48/2.50 | % 12.48/2.50 | DELTA: instantiating (49) with fresh symbols all_41_0, all_41_1 gives: % 12.48/2.50 | (53) cC18(iV16560) = all_41_1 & cC16(iV16560) = all_41_0 & ( ~ (all_41_1 = % 12.48/2.50 | 0) | all_41_0 = 0) % 12.48/2.50 | % 12.48/2.50 | ALPHA: (53) implies: % 12.48/2.50 | (54) cC16(iV16560) = all_41_0 % 12.48/2.50 | (55) cC18(iV16560) = all_41_1 % 12.48/2.50 | (56) ~ (all_41_1 = 0) | all_41_0 = 0 % 12.48/2.50 | % 12.48/2.50 | DELTA: instantiating (48) with fresh symbols all_43_0, all_43_1 gives: % 12.48/2.50 | (57) cC18(iV16560) = all_43_0 & cC16(iV16560) = all_43_1 & ( ~ (all_43_1 = % 12.48/2.50 | 0) | all_43_0 = 0) % 12.48/2.50 | % 12.48/2.50 | ALPHA: (57) implies: % 12.48/2.50 | (58) cC16(iV16560) = all_43_1 % 12.48/2.50 | (59) cC18(iV16560) = all_43_0 % 12.48/2.50 | % 12.48/2.50 | DELTA: instantiating (47) with fresh symbols all_45_0, all_45_1 gives: % 12.48/2.50 | (60) cC16(iV16560) = all_45_1 & cC14(iV16560) = all_45_0 & ( ~ (all_45_1 = % 12.48/2.50 | 0) | (all_45_0 = 0 & all_23_6 = 0)) % 12.48/2.50 | % 12.48/2.50 | ALPHA: (60) implies: % 12.48/2.50 | (61) cC14(iV16560) = all_45_0 % 12.48/2.50 | (62) cC16(iV16560) = all_45_1 % 12.48/2.50 | (63) ~ (all_45_1 = 0) | (all_45_0 = 0 & all_23_6 = 0) % 12.48/2.50 | % 12.48/2.50 | BETA: splitting (50) gives: % 12.48/2.50 | % 12.48/2.50 | Case 1: % 12.48/2.50 | | % 12.48/2.50 | | (64) all_23_3 = 0 % 12.48/2.50 | | % 12.48/2.50 | | BETA: splitting (46) gives: % 12.48/2.50 | | % 12.48/2.50 | | Case 1: % 12.48/2.50 | | | % 12.48/2.50 | | | (65) all_23_1 = 0 % 12.48/2.50 | | | % 12.48/2.50 | | | GROUND_INST: instantiating (28) with all_23_7, all_45_0, iV16560, % 12.48/2.50 | | | simplifying with (37), (61) gives: % 12.48/2.50 | | | (66) all_45_0 = all_23_7 % 12.48/2.50 | | | % 12.48/2.50 | | | GROUND_INST: instantiating (29) with all_23_5, all_45_1, iV16560, % 12.48/2.50 | | | simplifying with (38), (62) gives: % 12.48/2.50 | | | (67) all_45_1 = all_23_5 % 12.48/2.50 | | | % 12.48/2.50 | | | GROUND_INST: instantiating (29) with all_43_1, all_45_1, iV16560, % 12.48/2.50 | | | simplifying with (58), (62) gives: % 12.48/2.50 | | | (68) all_45_1 = all_43_1 % 12.48/2.50 | | | % 12.48/2.50 | | | GROUND_INST: instantiating (29) with all_41_0, all_45_1, iV16560, % 12.48/2.50 | | | simplifying with (54), (62) gives: % 12.48/2.50 | | | (69) all_45_1 = all_41_0 % 12.48/2.50 | | | % 12.48/2.50 | | | GROUND_INST: instantiating (30) with all_23_8, all_41_1, iV16560, % 12.48/2.50 | | | simplifying with (40), (55) gives: % 12.48/2.51 | | | (70) all_41_1 = all_23_8 % 12.48/2.51 | | | % 12.48/2.51 | | | GROUND_INST: instantiating (30) with all_41_1, all_43_0, iV16560, % 12.48/2.51 | | | simplifying with (55), (59) gives: % 12.48/2.51 | | | (71) all_43_0 = all_41_1 % 12.48/2.51 | | | % 12.48/2.51 | | | GROUND_INST: instantiating (30) with 0, all_43_0, iV16560, simplifying % 12.48/2.51 | | | with (52), (59) gives: % 12.48/2.51 | | | (72) all_43_0 = 0 % 12.48/2.51 | | | % 12.48/2.51 | | | COMBINE_EQS: (67), (68) imply: % 12.48/2.51 | | | (73) all_43_1 = all_23_5 % 12.48/2.51 | | | % 12.48/2.51 | | | COMBINE_EQS: (68), (69) imply: % 12.48/2.51 | | | (74) all_43_1 = all_41_0 % 12.48/2.51 | | | % 12.48/2.51 | | | COMBINE_EQS: (71), (72) imply: % 12.48/2.51 | | | (75) all_41_1 = 0 % 12.48/2.51 | | | % 12.48/2.51 | | | SIMP: (75) implies: % 12.48/2.51 | | | (76) all_41_1 = 0 % 12.48/2.51 | | | % 12.48/2.51 | | | COMBINE_EQS: (73), (74) imply: % 12.48/2.51 | | | (77) all_41_0 = all_23_5 % 12.48/2.51 | | | % 12.48/2.51 | | | COMBINE_EQS: (70), (76) imply: % 12.48/2.51 | | | (78) all_23_8 = 0 % 12.48/2.51 | | | % 12.48/2.51 | | | SIMP: (78) implies: % 12.48/2.51 | | | (79) all_23_8 = 0 % 12.48/2.51 | | | % 12.48/2.51 | | | BETA: splitting (56) gives: % 12.48/2.51 | | | % 12.48/2.51 | | | Case 1: % 12.48/2.51 | | | | % 12.48/2.51 | | | | (80) ~ (all_41_1 = 0) % 12.48/2.51 | | | | % 12.48/2.51 | | | | REDUCE: (76), (80) imply: % 12.48/2.51 | | | | (81) $false % 12.48/2.51 | | | | % 12.48/2.51 | | | | CLOSE: (81) is inconsistent. % 12.48/2.51 | | | | % 12.48/2.51 | | | Case 2: % 12.48/2.51 | | | | % 12.48/2.51 | | | | (82) all_41_0 = 0 % 12.48/2.51 | | | | % 12.48/2.51 | | | | COMBINE_EQS: (77), (82) imply: % 12.48/2.51 | | | | (83) all_23_5 = 0 % 12.48/2.51 | | | | % 12.48/2.51 | | | | COMBINE_EQS: (67), (83) imply: % 12.48/2.51 | | | | (84) all_45_1 = 0 % 12.48/2.51 | | | | % 12.48/2.51 | | | | BETA: splitting (63) gives: % 12.48/2.51 | | | | % 12.48/2.51 | | | | Case 1: % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | (85) ~ (all_45_1 = 0) % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | REDUCE: (84), (85) imply: % 12.48/2.51 | | | | | (86) $false % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | CLOSE: (86) is inconsistent. % 12.48/2.51 | | | | | % 12.48/2.51 | | | | Case 2: % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | (87) all_45_0 = 0 & all_23_6 = 0 % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | ALPHA: (87) implies: % 12.48/2.51 | | | | | (88) all_23_6 = 0 % 12.48/2.51 | | | | | (89) all_45_0 = 0 % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | COMBINE_EQS: (66), (89) imply: % 12.48/2.51 | | | | | (90) all_23_7 = 0 % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | BETA: splitting (42) gives: % 12.48/2.51 | | | | | % 12.48/2.51 | | | | | Case 1: % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | (91) ~ (all_23_0 = 0) % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | REDUCE: (44), (91) imply: % 12.48/2.51 | | | | | | (92) $false % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | CLOSE: (92) is inconsistent. % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | Case 2: % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | (93) ~ (all_23_1 = 0) | ~ (all_23_2 = 0) | ~ (all_23_3 = 0) | % 12.48/2.51 | | | | | | ~ (all_23_4 = 0) | ~ (all_23_5 = 0) | ~ (all_23_6 = 0) | % 12.48/2.51 | | | | | | ~ (all_23_7 = 0) | ~ (all_23_8 = 0) | ? [v0: $i] : ? [v1: % 12.48/2.51 | | | | | | any] : ? [v2: any] : (xsd_string(v0) = v1 & % 12.48/2.51 | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ % 12.48/2.51 | | | | | | (v2 = 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? [v1: any] % 12.48/2.51 | | | | | | : ? [v2: any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 % 12.48/2.51 | | | | | | & $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | BETA: splitting (93) gives: % 12.48/2.51 | | | | | | % 12.48/2.51 | | | | | | Case 1: % 12.48/2.51 | | | | | | | % 12.48/2.51 | | | | | | | (94) ~ (all_23_1 = 0) % 12.48/2.51 | | | | | | | % 12.48/2.51 | | | | | | | REDUCE: (65), (94) imply: % 12.48/2.51 | | | | | | | (95) $false % 12.48/2.51 | | | | | | | % 12.48/2.51 | | | | | | | CLOSE: (95) is inconsistent. % 12.48/2.51 | | | | | | | % 12.48/2.51 | | | | | | Case 2: % 12.48/2.51 | | | | | | | % 12.48/2.51 | | | | | | | (96) ~ (all_23_2 = 0) | ~ (all_23_3 = 0) | ~ (all_23_4 = 0) % 12.48/2.51 | | | | | | | | ~ (all_23_5 = 0) | ~ (all_23_6 = 0) | ~ (all_23_7 = % 12.48/2.51 | | | | | | | 0) | ~ (all_23_8 = 0) | ? [v0: $i] : ? [v1: any] : ? % 12.48/2.51 | | | | | | | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.51 | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 12.48/2.51 | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: any] % 12.48/2.51 | | | | | | | : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) & ( % 12.48/2.51 | | | | | | | ~ (v1 = 0) | v2 = 0)) % 12.48/2.52 | | | | | | | % 12.48/2.52 | | | | | | | BETA: splitting (96) gives: % 12.48/2.52 | | | | | | | % 12.48/2.52 | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | (97) ~ (all_23_2 = 0) % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | REDUCE: (45), (97) imply: % 12.48/2.52 | | | | | | | | (98) $false % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | CLOSE: (98) is inconsistent. % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | Case 2: % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | (99) ~ (all_23_3 = 0) | ~ (all_23_4 = 0) | ~ (all_23_5 = % 12.48/2.52 | | | | | | | | 0) | ~ (all_23_6 = 0) | ~ (all_23_7 = 0) | ~ % 12.48/2.52 | | | | | | | | (all_23_8 = 0) | ? [v0: $i] : ? [v1: any] : ? [v2: % 12.48/2.52 | | | | | | | | any] : (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.52 | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 12.48/2.52 | | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: % 12.48/2.52 | | | | | | | | any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 12.48/2.52 | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | BETA: splitting (99) gives: % 12.48/2.52 | | | | | | | | % 12.48/2.52 | | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | (100) ~ (all_23_3 = 0) % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | REDUCE: (64), (100) imply: % 12.48/2.52 | | | | | | | | | (101) $false % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | CLOSE: (101) is inconsistent. % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | Case 2: % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | (102) ~ (all_23_4 = 0) | ~ (all_23_5 = 0) | ~ (all_23_6 % 12.48/2.52 | | | | | | | | | = 0) | ~ (all_23_7 = 0) | ~ (all_23_8 = 0) | ? % 12.48/2.52 | | | | | | | | | [v0: $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.52 | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & $i(v0) % 12.48/2.52 | | | | | | | | | & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ (v1 = % 12.48/2.52 | | | | | | | | | 0)))) | ? [v0: $i] : ? [v1: any] : ? [v2: % 12.48/2.52 | | | | | | | | | any] : (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 12.48/2.52 | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | BETA: splitting (102) gives: % 12.48/2.52 | | | | | | | | | % 12.48/2.52 | | | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | (103) ~ (all_23_4 = 0) % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | REDUCE: (43), (103) imply: % 12.48/2.52 | | | | | | | | | | (104) $false % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | CLOSE: (104) is inconsistent. % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | Case 2: % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | (105) ~ (all_23_5 = 0) | ~ (all_23_6 = 0) | ~ % 12.48/2.52 | | | | | | | | | | (all_23_7 = 0) | ~ (all_23_8 = 0) | ? [v0: $i] : % 12.48/2.52 | | | | | | | | | | ? [v1: any] : ? [v2: any] : (xsd_string(v0) = v1 & % 12.48/2.52 | | | | | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = % 12.48/2.52 | | | | | | | | | | 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: % 12.48/2.52 | | | | | | | | | | $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.52 | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & $i(v0) % 12.48/2.52 | | | | | | | | | | & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | BETA: splitting (105) gives: % 12.48/2.52 | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | (106) ~ (all_23_5 = 0) % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | REDUCE: (83), (106) imply: % 12.48/2.52 | | | | | | | | | | | (107) $false % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | CLOSE: (107) is inconsistent. % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | Case 2: % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | (108) ~ (all_23_6 = 0) | ~ (all_23_7 = 0) | ~ % 12.48/2.52 | | | | | | | | | | | (all_23_8 = 0) | ? [v0: $i] : ? [v1: any] : ? % 12.48/2.52 | | | | | | | | | | | [v2: any] : (xsd_string(v0) = v1 & xsd_integer(v0) % 12.48/2.52 | | | | | | | | | | | = v2 & $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = % 12.48/2.52 | | | | | | | | | | | 0) & ~ (v1 = 0)))) | ? [v0: $i] : ? % 12.48/2.52 | | | | | | | | | | | [v1: any] : ? [v2: any] : (cowlNothing(v0) = v2 & % 12.48/2.52 | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 12.48/2.52 | | | | | | | | | | | = 0)) % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | BETA: splitting (108) gives: % 12.48/2.52 | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | (109) ~ (all_23_6 = 0) % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | REDUCE: (88), (109) imply: % 12.48/2.52 | | | | | | | | | | | | (110) $false % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | CLOSE: (110) is inconsistent. % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | Case 2: % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | (111) ~ (all_23_7 = 0) | ~ (all_23_8 = 0) | ? [v0: % 12.48/2.52 | | | | | | | | | | | | $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.52 | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.52 | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 12.48/2.52 | | | | | | | | | | | | (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : % 12.48/2.52 | | | | | | | | | | | | ? [v2: any] : (cowlNothing(v0) = v2 & % 12.48/2.52 | | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 12.48/2.52 | | | | | | | | | | | | = 0)) % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | BETA: splitting (111) gives: % 12.48/2.52 | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | Case 1: % 12.48/2.52 | | | | | | | | | | | | | % 12.48/2.52 | | | | | | | | | | | | | (112) ~ (all_23_7 = 0) % 12.48/2.52 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | REDUCE: (90), (112) imply: % 12.48/2.53 | | | | | | | | | | | | | (113) $false % 12.48/2.53 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | CLOSE: (113) is inconsistent. % 12.48/2.53 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | Case 2: % 12.48/2.53 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | (114) ~ (all_23_8 = 0) | ? [v0: $i] : ? [v1: any] : % 12.48/2.53 | | | | | | | | | | | | | ? [v2: any] : (xsd_string(v0) = v1 & % 12.48/2.53 | | | | | | | | | | | | | xsd_integer(v0) = v2 & $i(v0) & ((v2 = 0 & v1 = % 12.48/2.53 | | | | | | | | | | | | | 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) | ? [v0: % 12.48/2.53 | | | | | | | | | | | | | $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.53 | | | | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 12.48/2.53 | | | | | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.53 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | BETA: splitting (114) gives: % 12.48/2.53 | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | Case 1: % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | (115) ~ (all_23_8 = 0) % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | REDUCE: (79), (115) imply: % 12.48/2.53 | | | | | | | | | | | | | | (116) $false % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | CLOSE: (116) is inconsistent. % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | Case 2: % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | (117) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.53 | | | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.53 | | | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 12.48/2.53 | | | | | | | | | | | | | | (v1 = 0)))) | ? [v0: $i] : ? [v1: any] : % 12.48/2.53 | | | | | | | | | | | | | | ? [v2: any] : (cowlNothing(v0) = v2 & % 12.48/2.53 | | | | | | | | | | | | | | cowlThing(v0) = v1 & $i(v0) & ( ~ (v1 = 0) | v2 % 12.48/2.53 | | | | | | | | | | | | | | = 0)) % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | BETA: splitting (117) gives: % 12.48/2.53 | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | Case 1: % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | (118) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.53 | | | | | | | | | | | | | | | (xsd_string(v0) = v1 & xsd_integer(v0) = v2 & % 12.48/2.53 | | | | | | | | | | | | | | | $i(v0) & ((v2 = 0 & v1 = 0) | ( ~ (v2 = 0) & ~ % 12.48/2.53 | | | | | | | | | | | | | | | (v1 = 0)))) % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | DELTA: instantiating (118) with fresh symbols all_162_0, % 12.48/2.53 | | | | | | | | | | | | | | | all_162_1, all_162_2 gives: % 12.48/2.53 | | | | | | | | | | | | | | | (119) xsd_string(all_162_2) = all_162_1 & % 12.48/2.53 | | | | | | | | | | | | | | | xsd_integer(all_162_2) = all_162_0 & $i(all_162_2) % 12.48/2.53 | | | | | | | | | | | | | | | & ((all_162_0 = 0 & all_162_1 = 0) | ( ~ % 12.48/2.53 | | | | | | | | | | | | | | | (all_162_0 = 0) & ~ (all_162_1 = 0))) % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | ALPHA: (119) implies: % 12.48/2.53 | | | | | | | | | | | | | | | (120) $i(all_162_2) % 12.48/2.53 | | | | | | | | | | | | | | | (121) xsd_integer(all_162_2) = all_162_0 % 12.48/2.53 | | | | | | | | | | | | | | | (122) xsd_string(all_162_2) = all_162_1 % 12.48/2.53 | | | | | | | | | | | | | | | (123) (all_162_0 = 0 & all_162_1 = 0) | ( ~ (all_162_0 = % 12.48/2.53 | | | | | | | | | | | | | | | 0) & ~ (all_162_1 = 0)) % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_162_2, all_162_1, % 12.48/2.53 | | | | | | | | | | | | | | | simplifying with (120), (122) gives: % 12.48/2.53 | | | | | | | | | | | | | | | (124) all_162_1 = 0 | xsd_integer(all_162_2) = 0 % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | BETA: splitting (123) gives: % 12.48/2.53 | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | Case 1: % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | (125) all_162_0 = 0 & all_162_1 = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | ALPHA: (125) implies: % 12.48/2.53 | | | | | | | | | | | | | | | | (126) all_162_1 = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | (127) all_162_0 = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | REDUCE: (122), (126) imply: % 12.48/2.53 | | | | | | | | | | | | | | | | (128) xsd_string(all_162_2) = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | REDUCE: (121), (127) imply: % 12.48/2.53 | | | | | | | | | | | | | | | | (129) xsd_integer(all_162_2) = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_162_2, simplifying with % 12.48/2.53 | | | | | | | | | | | | | | | | (120), (128) gives: % 12.48/2.53 | | | | | | | | | | | | | | | | (130) ? [v0: int] : ( ~ (v0 = 0) & % 12.48/2.53 | | | | | | | | | | | | | | | | xsd_integer(all_162_2) = v0) % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | DELTA: instantiating (130) with fresh symbol all_176_0 % 12.48/2.53 | | | | | | | | | | | | | | | | gives: % 12.48/2.53 | | | | | | | | | | | | | | | | (131) ~ (all_176_0 = 0) & xsd_integer(all_162_2) = % 12.48/2.53 | | | | | | | | | | | | | | | | all_176_0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | ALPHA: (131) implies: % 12.48/2.53 | | | | | | | | | | | | | | | | (132) ~ (all_176_0 = 0) % 12.48/2.53 | | | | | | | | | | | | | | | | (133) xsd_integer(all_162_2) = all_176_0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (25) with 0, all_176_0, all_162_2, % 12.48/2.53 | | | | | | | | | | | | | | | | simplifying with (129), (133) gives: % 12.48/2.53 | | | | | | | | | | | | | | | | (134) all_176_0 = 0 % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | REDUCE: (132), (134) imply: % 12.48/2.53 | | | | | | | | | | | | | | | | (135) $false % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | CLOSE: (135) is inconsistent. % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | Case 2: % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | (136) ~ (all_162_0 = 0) & ~ (all_162_1 = 0) % 12.48/2.53 | | | | | | | | | | | | | | | | % 12.48/2.53 | | | | | | | | | | | | | | | | ALPHA: (136) implies: % 12.48/2.53 | | | | | | | | | | | | | | | | (137) ~ (all_162_1 = 0) % 12.48/2.54 | | | | | | | | | | | | | | | | (138) ~ (all_162_0 = 0) % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | BETA: splitting (124) gives: % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | Case 1: % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | (139) xsd_integer(all_162_2) = 0 % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (25) with all_162_0, 0, all_162_2, % 12.48/2.54 | | | | | | | | | | | | | | | | | simplifying with (121), (139) gives: % 12.48/2.54 | | | | | | | | | | | | | | | | | (140) all_162_0 = 0 % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | REDUCE: (138), (140) imply: % 12.48/2.54 | | | | | | | | | | | | | | | | | (141) $false % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | CLOSE: (141) is inconsistent. % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | Case 2: % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | (142) all_162_1 = 0 % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | REDUCE: (137), (142) imply: % 12.48/2.54 | | | | | | | | | | | | | | | | | (143) $false % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | | CLOSE: (143) is inconsistent. % 12.48/2.54 | | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | Case 2: % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | (144) ? [v0: $i] : ? [v1: any] : ? [v2: any] : % 12.48/2.54 | | | | | | | | | | | | | | | (cowlNothing(v0) = v2 & cowlThing(v0) = v1 & % 12.48/2.54 | | | | | | | | | | | | | | | $i(v0) & ( ~ (v1 = 0) | v2 = 0)) % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | DELTA: instantiating (144) with fresh symbols all_162_0, % 12.48/2.54 | | | | | | | | | | | | | | | all_162_1, all_162_2 gives: % 12.48/2.54 | | | | | | | | | | | | | | | (145) cowlNothing(all_162_2) = all_162_0 & % 12.48/2.54 | | | | | | | | | | | | | | | cowlThing(all_162_2) = all_162_1 & $i(all_162_2) & % 12.48/2.54 | | | | | | | | | | | | | | | ( ~ (all_162_1 = 0) | all_162_0 = 0) % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | ALPHA: (145) implies: % 12.48/2.54 | | | | | | | | | | | | | | | (146) $i(all_162_2) % 12.48/2.54 | | | | | | | | | | | | | | | (147) cowlThing(all_162_2) = all_162_1 % 12.48/2.54 | | | | | | | | | | | | | | | (148) cowlNothing(all_162_2) = all_162_0 % 12.48/2.54 | | | | | | | | | | | | | | | (149) ~ (all_162_1 = 0) | all_162_0 = 0 % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_162_2, all_162_1, % 12.48/2.54 | | | | | | | | | | | | | | | simplifying with (146), (147) gives: % 12.48/2.54 | | | | | | | | | | | | | | | (150) all_162_1 = 0 % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | BETA: splitting (149) gives: % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | Case 1: % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | (151) ~ (all_162_1 = 0) % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | REDUCE: (150), (151) imply: % 12.48/2.54 | | | | | | | | | | | | | | | | (152) $false % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | CLOSE: (152) is inconsistent. % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | Case 2: % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | (153) all_162_0 = 0 % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | REDUCE: (148), (153) imply: % 12.48/2.54 | | | | | | | | | | | | | | | | (154) cowlNothing(all_162_2) = 0 % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with all_162_2, simplifying with % 12.48/2.54 | | | | | | | | | | | | | | | | (146), (154) gives: % 12.48/2.54 | | | | | | | | | | | | | | | | (155) $false % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | | CLOSE: (155) is inconsistent. % 12.48/2.54 | | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | | % 12.48/2.54 | | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | | % 12.48/2.54 | | | | | | | | | End of split % 12.48/2.54 | | | | | | | | | % 12.48/2.54 | | | | | | | | End of split % 12.48/2.54 | | | | | | | | % 12.48/2.54 | | | | | | | End of split % 12.48/2.54 | | | | | | | % 12.48/2.54 | | | | | | End of split % 12.48/2.54 | | | | | | % 12.48/2.54 | | | | | End of split % 12.48/2.54 | | | | | % 12.48/2.54 | | | | End of split % 12.48/2.54 | | | | % 12.48/2.54 | | | End of split % 12.48/2.54 | | | % 12.48/2.54 | | Case 2: % 12.48/2.54 | | | % 12.48/2.54 | | | (156) ? [v0: any] : ? [v1: any] : (cC10xcomp(iV16562) = v0 & % 12.48/2.54 | | | cC2xcomp(iV16562) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 12.48/2.54 | | | % 12.48/2.54 | | | DELTA: instantiating (156) with fresh symbols all_55_0, all_55_1 gives: % 12.48/2.54 | | | (157) cC10xcomp(iV16562) = all_55_1 & cC2xcomp(iV16562) = all_55_0 & ( % 12.48/2.54 | | | ~ (all_55_0 = 0) | ~ (all_55_1 = 0)) % 12.48/2.54 | | | % 12.48/2.54 | | | ALPHA: (157) implies: % 12.48/2.54 | | | (158) cC2xcomp(iV16562) = all_55_0 % 12.48/2.54 | | | (159) cC10xcomp(iV16562) = all_55_1 % 12.48/2.54 | | | (160) ~ (all_55_0 = 0) | ~ (all_55_1 = 0) % 12.48/2.54 | | | % 12.48/2.54 | | | GROUND_INST: instantiating (26) with 0, all_55_0, iV16562, simplifying % 12.48/2.54 | | | with (19), (158) gives: % 12.48/2.54 | | | (161) all_55_0 = 0 % 12.48/2.54 | | | % 12.48/2.54 | | | GROUND_INST: instantiating (27) with 0, all_55_1, iV16562, simplifying % 12.48/2.54 | | | with (18), (159) gives: % 12.48/2.54 | | | (162) all_55_1 = 0 % 12.48/2.54 | | | % 12.48/2.54 | | | BETA: splitting (160) gives: % 12.48/2.54 | | | % 12.48/2.54 | | | Case 1: % 12.48/2.54 | | | | % 12.48/2.54 | | | | (163) ~ (all_55_0 = 0) % 12.48/2.54 | | | | % 12.48/2.54 | | | | REDUCE: (161), (163) imply: % 12.48/2.54 | | | | (164) $false % 12.48/2.54 | | | | % 12.48/2.54 | | | | CLOSE: (164) is inconsistent. % 12.48/2.54 | | | | % 12.48/2.54 | | | Case 2: % 12.48/2.54 | | | | % 12.48/2.54 | | | | (165) ~ (all_55_1 = 0) % 12.48/2.54 | | | | % 12.48/2.54 | | | | REDUCE: (162), (165) imply: % 12.48/2.54 | | | | (166) $false % 12.48/2.54 | | | | % 12.48/2.54 | | | | CLOSE: (166) is inconsistent. % 12.48/2.54 | | | | % 12.48/2.54 | | | End of split % 12.48/2.54 | | | % 12.48/2.54 | | End of split % 12.48/2.54 | | % 12.48/2.54 | Case 2: % 12.48/2.54 | | % 12.48/2.54 | | (167) ? [v0: any] : ? [v1: any] : (cC4xcomp(iV16561) = v0 & % 12.48/2.54 | | cC2xcomp(iV16561) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 12.48/2.54 | | % 12.48/2.54 | | DELTA: instantiating (167) with fresh symbols all_51_0, all_51_1 gives: % 12.48/2.54 | | (168) cC4xcomp(iV16561) = all_51_1 & cC2xcomp(iV16561) = all_51_0 & ( ~ % 12.48/2.54 | | (all_51_0 = 0) | ~ (all_51_1 = 0)) % 12.48/2.54 | | % 12.48/2.54 | | ALPHA: (168) implies: % 12.48/2.55 | | (169) cC2xcomp(iV16561) = all_51_0 % 12.48/2.55 | | (170) cC4xcomp(iV16561) = all_51_1 % 12.48/2.55 | | (171) ~ (all_51_0 = 0) | ~ (all_51_1 = 0) % 12.48/2.55 | | % 12.48/2.55 | | GROUND_INST: instantiating (26) with 0, all_51_0, iV16561, simplifying with % 12.48/2.55 | | (16), (169) gives: % 12.48/2.55 | | (172) all_51_0 = 0 % 12.48/2.55 | | % 12.48/2.55 | | GROUND_INST: instantiating (31) with 0, all_51_1, iV16561, simplifying with % 12.48/2.55 | | (15), (170) gives: % 12.48/2.55 | | (173) all_51_1 = 0 % 12.48/2.55 | | % 12.48/2.55 | | BETA: splitting (171) gives: % 12.48/2.55 | | % 12.48/2.55 | | Case 1: % 12.48/2.55 | | | % 12.48/2.55 | | | (174) ~ (all_51_0 = 0) % 12.48/2.55 | | | % 12.48/2.55 | | | REDUCE: (172), (174) imply: % 12.48/2.55 | | | (175) $false % 12.48/2.55 | | | % 12.48/2.55 | | | CLOSE: (175) is inconsistent. % 12.48/2.55 | | | % 12.48/2.55 | | Case 2: % 12.48/2.55 | | | % 12.48/2.55 | | | (176) ~ (all_51_1 = 0) % 12.48/2.55 | | | % 12.48/2.55 | | | REDUCE: (173), (176) imply: % 12.48/2.55 | | | (177) $false % 12.48/2.55 | | | % 12.48/2.55 | | | CLOSE: (177) is inconsistent. % 12.48/2.55 | | | % 12.48/2.55 | | End of split % 12.48/2.55 | | % 12.48/2.55 | End of split % 12.48/2.55 | % 12.48/2.55 End of proof % 12.48/2.55 % SZS output end Proof for theBenchmark % 12.48/2.55 % 12.48/2.55 1905ms %------------------------------------------------------------------------------