%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SET775+4 : TPTP v8.1.2. Released v2.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.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 15:26:23 EDT 2023 % Result : Theorem 12.59s 2.47s % Output : Proof 20.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SET775+4 : TPTP v8.1.2. Released v2.2.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n006.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 : Sat Aug 26 10:10:22 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.99/1.15 Prover 1: Preprocessing ... % 2.99/1.15 Prover 4: Preprocessing ... % 3.45/1.19 Prover 3: Preprocessing ... % 3.45/1.19 Prover 5: Preprocessing ... % 3.45/1.19 Prover 6: Preprocessing ... % 3.45/1.19 Prover 0: Preprocessing ... % 3.45/1.20 Prover 2: Preprocessing ... % 6.63/1.69 Prover 5: Proving ... % 7.31/1.73 Prover 2: Proving ... % 7.31/1.73 Prover 6: Proving ... % 7.31/1.76 Prover 3: Constructing countermodel ... % 7.31/1.79 Prover 1: Constructing countermodel ... % 8.58/1.94 Prover 3: gave up % 8.58/1.94 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.58/1.99 Prover 1: gave up % 8.58/1.99 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.58/2.04 Prover 8: Preprocessing ... % 8.58/2.04 Prover 7: Preprocessing ... % 8.58/2.05 Prover 4: Constructing countermodel ... % 9.21/2.06 Prover 0: Proving ... % 9.21/2.15 Prover 7: Warning: ignoring some quantifiers % 10.34/2.18 Prover 7: Constructing countermodel ... % 11.19/2.29 Prover 8: Warning: ignoring some quantifiers % 11.19/2.33 Prover 8: Constructing countermodel ... % 11.68/2.35 Prover 7: gave up % 11.68/2.35 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 11.86/2.39 Prover 9: Preprocessing ... % 12.30/2.44 Prover 8: gave up % 12.30/2.44 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 12.59/2.46 Prover 10: Preprocessing ... % 12.59/2.47 Prover 0: proved (1850ms) % 12.59/2.47 % 12.59/2.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.59/2.47 % 12.59/2.48 Prover 2: stopped % 12.59/2.49 Prover 6: stopped % 12.59/2.49 Prover 5: stopped % 12.59/2.50 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 12.59/2.50 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.59/2.50 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 12.59/2.50 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 12.59/2.52 Prover 11: Preprocessing ... % 12.59/2.52 Prover 13: Preprocessing ... % 12.59/2.52 Prover 10: Warning: ignoring some quantifiers % 13.15/2.53 Prover 19: Preprocessing ... % 13.15/2.54 Prover 10: Constructing countermodel ... % 13.15/2.54 Prover 16: Preprocessing ... % 13.46/2.60 Prover 10: gave up % 13.46/2.62 Prover 16: Warning: ignoring some quantifiers % 13.91/2.65 Prover 16: Constructing countermodel ... % 13.91/2.65 Prover 13: Warning: ignoring some quantifiers % 13.91/2.67 Prover 9: Constructing countermodel ... % 13.91/2.68 Prover 13: Constructing countermodel ... % 13.91/2.68 Prover 9: stopped % 13.91/2.77 Prover 19: Warning: ignoring some quantifiers % 14.66/2.80 Prover 19: Constructing countermodel ... % 14.66/2.84 Prover 11: Constructing countermodel ... % 17.04/3.08 Prover 19: gave up % 18.42/3.35 Prover 4: Found proof (size 438) % 18.42/3.35 Prover 4: proved (2716ms) % 18.42/3.35 Prover 16: stopped % 18.42/3.35 Prover 13: stopped % 18.42/3.35 Prover 11: stopped % 18.42/3.35 % 18.42/3.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.42/3.35 % 19.36/3.47 % SZS output start Proof for theBenchmark % 19.36/3.48 Assumptions after simplification: % 19.36/3.48 --------------------------------- % 19.36/3.48 % 19.36/3.48 (equivalence) % 19.83/3.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 19.83/3.52 int] : (v5 = 0 | ~ (equivalence(v1, v0) = 0) | ~ (apply(v1, v3, v4) = 0) | % 19.83/3.52 ~ (apply(v1, v2, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 19.83/3.52 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : % 19.83/3.52 (apply(v1, v2, v3) = v9 & member(v4, v0) = v8 & member(v3, v0) = v7 & % 19.83/3.52 member(v2, v0) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = % 19.83/3.52 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 19.83/3.52 [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (equivalence(v1, v0) = 0) | ~ % 19.83/3.52 (apply(v1, v2, v4) = v5) | ~ (apply(v1, v2, v3) = 0) | ~ $i(v4) | ~ % 19.83/3.52 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : % 19.83/3.52 ? [v8: any] : ? [v9: any] : (apply(v1, v3, v4) = v9 & member(v4, v0) = v8 & % 19.83/3.52 member(v3, v0) = v7 & member(v2, v0) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | % 19.83/3.52 ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 19.83/3.52 ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (equivalence(v1, v0) = % 19.83/3.52 0) | ~ (apply(v1, v2, v4) = v5) | ~ (member(v3, v0) = 0) | ~ $i(v4) | % 19.83/3.52 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : % 19.83/3.52 ? [v8: any] : ? [v9: any] : (apply(v1, v3, v4) = v9 & apply(v1, v2, v3) = % 19.83/3.52 v8 & member(v4, v0) = v7 & member(v2, v0) = v6 & ( ~ (v9 = 0) | ~ (v8 = % 19.83/3.52 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 19.83/3.52 [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (equivalence(v1, v0) = 0) % 19.83/3.52 | ~ (apply(v1, v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 19.83/3.52 $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : (apply(v1, v2, v3) = % 19.83/3.52 v7 & member(v3, v0) = v6 & member(v2, v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = % 19.83/3.52 0) | ~ (v5 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 19.83/3.52 [v3: $i] : ! [v4: $i] : ( ~ (equivalence(v1, v0) = 0) | ~ (apply(v1, v3, v4) % 19.83/3.52 = 0) | ~ (apply(v1, v2, v3) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 19.83/3.52 $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 19.83/3.52 any] : (apply(v1, v2, v4) = v8 & member(v4, v0) = v7 & member(v3, v0) = v6 % 19.83/3.52 & member(v2, v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v8 = % 19.83/3.52 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 19.83/3.52 $i] : ( ~ (equivalence(v1, v0) = 0) | ~ (apply(v1, v3, v4) = 0) | ~ % 19.83/3.52 (member(v2, v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 19.83/3.52 $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 19.83/3.52 (apply(v1, v2, v4) = v8 & apply(v1, v2, v3) = v7 & member(v4, v0) = v6 & % 19.83/3.52 member(v3, v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v8 = 0))) % 19.83/3.52 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 19.83/3.52 (equivalence(v1, v0) = 0) | ~ (apply(v1, v2, v3) = 0) | ~ (member(v4, v0) % 19.83/3.52 = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 19.83/3.52 any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : (apply(v1, v3, v4) = % 19.83/3.52 v7 & apply(v1, v2, v4) = v8 & member(v3, v0) = v6 & member(v2, v0) = v5 & % 19.83/3.52 ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v8 = 0))) & ! [v0: $i] : ! % 19.83/3.52 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (equivalence(v1, v0) % 19.83/3.52 = 0) | ~ (member(v4, v0) = 0) | ~ (member(v3, v0) = 0) | ~ (member(v2, % 19.83/3.52 v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 19.83/3.52 ? [v5: any] : ? [v6: any] : ? [v7: any] : (apply(v1, v3, v4) = v6 & % 19.83/3.52 apply(v1, v2, v4) = v7 & apply(v1, v2, v3) = v5 & ( ~ (v6 = 0) | ~ (v5 = % 19.83/3.52 0) | v7 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 19.83/3.52 int] : (v3 = 0 | ~ (equivalence(v1, v0) = 0) | ~ (apply(v1, v2, v2) = v3) % 19.83/3.52 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & % 19.83/3.52 member(v2, v0) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 19.83/3.52 $i] : ( ~ (equivalence(v1, v0) = 0) | ~ (apply(v1, v2, v3) = 0) | ~ $i(v3) % 19.83/3.52 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: % 19.83/3.52 any] : (apply(v1, v3, v2) = v6 & member(v3, v0) = v5 & member(v2, v0) = v4 % 19.83/3.52 & ( ~ (v5 = 0) | ~ (v4 = 0) | v6 = 0))) & ! [v0: $i] : ! [v1: $i] : ! % 19.83/3.52 [v2: int] : (v2 = 0 | ~ (equivalence(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | % 19.83/3.52 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? % 19.83/3.52 [v8: int] : ? [v9: int] : ? [v10: int] : ? [v11: int] : ? [v12: $i] : ? % 19.83/3.52 [v13: $i] : ? [v14: int] : ? [v15: int] : ? [v16: int] : ? [v17: int] : % 19.83/3.52 ? [v18: $i] : ? [v19: int] : ? [v20: int] : ($i(v18) & $i(v13) & $i(v12) & % 19.83/3.52 $i(v5) & $i(v4) & $i(v3) & ((v19 = 0 & ~ (v20 = 0) & apply(v1, v18, v18) % 19.83/3.52 = v20 & member(v18, v0) = 0) | (v16 = 0 & v15 = 0 & v14 = 0 & ~ (v17 % 19.83/3.52 = 0) & apply(v1, v13, v12) = v17 & apply(v1, v12, v13) = 0 & % 19.83/3.52 member(v13, v0) = 0 & member(v12, v0) = 0) | (v10 = 0 & v9 = 0 & v8 = % 19.83/3.52 0 & v7 = 0 & v6 = 0 & ~ (v11 = 0) & apply(v1, v4, v5) = 0 & apply(v1, % 19.83/3.52 v3, v5) = v11 & apply(v1, v3, v4) = 0 & member(v5, v0) = 0 & % 19.83/3.52 member(v4, v0) = 0 & member(v3, v0) = 0)))) & ! [v0: $i] : ! [v1: % 19.83/3.52 $i] : ! [v2: $i] : ( ~ (equivalence(v1, v0) = 0) | ~ (member(v2, v0) = 0) % 19.83/3.52 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | apply(v1, v2, v2) = 0) % 19.83/3.52 % 19.83/3.52 (pre_order) % 19.83/3.53 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 19.83/3.53 int] : (v5 = 0 | ~ (pre_order(v0, v1) = 0) | ~ (apply(v0, v3, v4) = 0) | % 19.83/3.53 ~ (apply(v0, v2, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 19.83/3.53 ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : % 19.83/3.53 (apply(v0, v2, v3) = v9 & member(v4, v1) = v8 & member(v3, v1) = v7 & % 19.83/3.53 member(v2, v1) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = % 19.83/3.53 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 19.83/3.53 [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (pre_order(v0, v1) = 0) | ~ (apply(v0, % 19.83/3.53 v2, v4) = v5) | ~ (apply(v0, v2, v3) = 0) | ~ $i(v4) | ~ $i(v3) | ~ % 19.83/3.53 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] % 19.83/3.53 : ? [v9: any] : (apply(v0, v3, v4) = v9 & member(v4, v1) = v8 & member(v3, % 19.83/3.53 v1) = v7 & member(v2, v1) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = % 19.83/3.53 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 19.83/3.53 [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (pre_order(v0, v1) = 0) | % 19.83/3.53 ~ (apply(v0, v2, v4) = v5) | ~ (member(v3, v1) = 0) | ~ $i(v4) | ~ % 19.83/3.53 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : % 19.83/3.53 ? [v8: any] : ? [v9: any] : (apply(v0, v3, v4) = v9 & apply(v0, v2, v3) = % 19.83/3.53 v8 & member(v4, v1) = v7 & member(v2, v1) = v6 & ( ~ (v9 = 0) | ~ (v8 = % 19.83/3.53 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 19.83/3.53 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (pre_order(v0, v1) = 0) | ~ % 19.83/3.53 (apply(v0, v3, v4) = 0) | ~ (apply(v0, v2, v3) = 0) | ~ $i(v4) | ~ $i(v3) % 19.83/3.53 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: % 19.83/3.53 any] : ? [v8: any] : (apply(v0, v2, v4) = v8 & member(v4, v1) = v7 & % 19.83/3.53 member(v3, v1) = v6 & member(v2, v1) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | % 19.83/3.53 ~ (v5 = 0) | v8 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 19.83/3.53 [v3: $i] : ! [v4: $i] : ( ~ (pre_order(v0, v1) = 0) | ~ (apply(v0, v3, v4) = % 19.83/3.53 0) | ~ (member(v2, v1) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 19.83/3.53 $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 19.83/3.53 any] : (apply(v0, v2, v4) = v8 & apply(v0, v2, v3) = v7 & member(v4, v1) = % 19.83/3.53 v6 & member(v3, v1) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v8 = % 19.83/3.53 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 19.83/3.53 $i] : ( ~ (pre_order(v0, v1) = 0) | ~ (apply(v0, v2, v3) = 0) | ~ % 19.83/3.53 (member(v4, v1) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 19.83/3.53 $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 19.83/3.53 (apply(v0, v3, v4) = v7 & apply(v0, v2, v4) = v8 & member(v3, v1) = v6 & % 19.83/3.53 member(v2, v1) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v8 = 0))) % 19.83/3.53 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 19.83/3.53 (pre_order(v0, v1) = 0) | ~ (member(v4, v1) = 0) | ~ (member(v3, v1) = 0) % 19.83/3.53 | ~ (member(v2, v1) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 19.83/3.53 ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : (apply(v0, v3, v4) = % 19.83/3.53 v6 & apply(v0, v2, v4) = v7 & apply(v0, v2, v3) = v5 & ( ~ (v6 = 0) | ~ % 19.83/3.53 (v5 = 0) | v7 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 19.83/3.53 int] : (v3 = 0 | ~ (pre_order(v0, v1) = 0) | ~ (apply(v0, v2, v2) = v3) | % 19.83/3.53 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & member(v2, % 19.83/3.53 v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 19.83/3.53 (pre_order(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] % 19.83/3.53 : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? [v8: int] : ? [v9: int] : % 19.83/3.53 ? [v10: int] : ? [v11: int] : ? [v12: $i] : ? [v13: int] : ? [v14: int] % 19.83/3.53 : ($i(v12) & $i(v5) & $i(v4) & $i(v3) & ((v13 = 0 & ~ (v14 = 0) & apply(v0, % 19.83/3.53 v12, v12) = v14 & member(v12, v1) = 0) | (v10 = 0 & v9 = 0 & v8 = 0 % 19.83/3.53 & v7 = 0 & v6 = 0 & ~ (v11 = 0) & apply(v0, v4, v5) = 0 & apply(v0, % 19.83/3.53 v3, v5) = v11 & apply(v0, v3, v4) = 0 & member(v5, v1) = 0 & % 19.83/3.53 member(v4, v1) = 0 & member(v3, v1) = 0)))) & ! [v0: $i] : ! [v1: % 19.83/3.53 $i] : ! [v2: $i] : ( ~ (pre_order(v0, v1) = 0) | ~ (member(v2, v1) = 0) | % 19.83/3.53 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | apply(v0, v2, v2) = 0) % 19.83/3.53 % 19.83/3.54 (thIII11) % 19.83/3.54 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) & % 19.83/3.54 pre_order(v1, v0) = 0 & equivalence(v2, v0) = v3 & $i(v2) & $i(v1) & $i(v0) % 19.83/3.54 & ! [v4: $i] : ! [v5: $i] : ! [v6: any] : ( ~ (apply(v2, v4, v5) = v6) | % 19.83/3.54 ~ $i(v5) | ~ $i(v4) | ? [v7: any] : ? [v8: any] : ? [v9: any] : ? % 19.83/3.54 [v10: any] : (apply(v1, v5, v4) = v10 & apply(v1, v4, v5) = v9 & % 19.83/3.54 member(v5, v0) = v8 & member(v4, v0) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | % 19.83/3.54 (( ~ (v10 = 0) | ~ (v9 = 0) | v6 = 0) & ( ~ (v6 = 0) | (v10 = 0 & v9 % 19.83/3.54 = 0)))))) & ! [v4: $i] : ! [v5: $i] : ! [v6: any] : ( ~ % 19.83/3.54 (apply(v1, v5, v4) = v6) | ~ $i(v5) | ~ $i(v4) | ? [v7: any] : ? [v8: % 19.83/3.54 any] : ? [v9: any] : ? [v10: any] : (apply(v2, v4, v5) = v9 & % 19.83/3.54 apply(v1, v4, v5) = v10 & member(v5, v0) = v8 & member(v4, v0) = v7 & ( % 19.83/3.54 ~ (v8 = 0) | ~ (v7 = 0) | (( ~ (v10 = 0) | ~ (v6 = 0) | v9 = 0) & ( % 19.83/3.54 ~ (v9 = 0) | (v10 = 0 & v6 = 0)))))) & ! [v4: $i] : ! [v5: $i] : % 19.83/3.54 ! [v6: any] : ( ~ (apply(v1, v4, v5) = v6) | ~ $i(v5) | ~ $i(v4) | ? % 19.83/3.54 [v7: any] : ? [v8: any] : ? [v9: any] : ? [v10: any] : (apply(v2, v4, % 19.83/3.54 v5) = v9 & apply(v1, v5, v4) = v10 & member(v5, v0) = v8 & member(v4, % 19.83/3.54 v0) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | (( ~ (v10 = 0) | ~ (v6 = 0) | % 19.83/3.54 v9 = 0) & ( ~ (v9 = 0) | (v10 = 0 & v6 = 0))))))) % 19.83/3.54 % 19.83/3.54 (function-axioms) % 19.83/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 19.83/3.55 | ~ (equivalence_class(v4, v3, v2) = v1) | ~ (equivalence_class(v4, v3, % 19.83/3.55 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 19.83/3.55 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = % 19.83/3.55 v1) | ~ (apply(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.83/3.55 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.83/3.55 (pre_order(v3, v2) = v1) | ~ (pre_order(v3, v2) = v0)) & ! [v0: % 19.83/3.55 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 19.83/3.55 : (v1 = v0 | ~ (equivalence(v3, v2) = v1) | ~ (equivalence(v3, v2) = v0)) & % 19.83/3.55 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 19.83/3.55 $i] : (v1 = v0 | ~ (partition(v3, v2) = v1) | ~ (partition(v3, v2) = v0)) % 19.83/3.55 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 19.83/3.55 [v3: $i] : (v1 = v0 | ~ (disjoint(v3, v2) = v1) | ~ (disjoint(v3, v2) = v0)) % 19.83/3.55 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.83/3.55 (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0: % 19.83/3.55 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.83/3.55 (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0: $i] : ! % 19.83/3.55 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (union(v3, v2) = v1) | ~ % 19.83/3.55 (union(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 19.83/3.55 $i] : (v1 = v0 | ~ (intersection(v3, v2) = v1) | ~ (intersection(v3, v2) = % 19.83/3.55 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 19.83/3.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (equal_set(v3, v2) = v1) | ~ % 19.83/3.55 (equal_set(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.83/3.55 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (subset(v3, % 19.83/3.55 v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 19.83/3.55 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.83/3.55 (member(v3, v2) = v1) | ~ (member(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 19.83/3.55 $i] : ! [v2: $i] : (v1 = v0 | ~ (product(v2) = v1) | ~ (product(v2) = % 19.83/3.55 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sum(v2) = % 19.83/3.55 v1) | ~ (sum(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 19.83/3.55 v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0: $i] : ! % 19.83/3.55 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (power_set(v2) = v1) | ~ % 19.83/3.55 (power_set(v2) = v0)) % 19.83/3.55 % 19.83/3.55 Further assumptions not needed in the proof: % 19.83/3.55 -------------------------------------------- % 19.83/3.55 difference, disjoint, empty_set, equal_set, equivalence_class, intersection, % 19.83/3.55 partition, power_set, product, singleton, subset, sum, union, unordered_pair % 19.83/3.55 % 19.83/3.55 Those formulas are unsatisfiable: % 19.83/3.55 --------------------------------- % 19.83/3.55 % 19.83/3.55 Begin of proof % 19.83/3.55 | % 19.83/3.55 | ALPHA: (equivalence) implies: % 19.83/3.55 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 19.83/3.55 | (equivalence(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? % 19.83/3.55 | [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? [v8: int] : % 19.83/3.55 | ? [v9: int] : ? [v10: int] : ? [v11: int] : ? [v12: $i] : ? % 19.83/3.55 | [v13: $i] : ? [v14: int] : ? [v15: int] : ? [v16: int] : ? [v17: % 19.83/3.55 | int] : ? [v18: $i] : ? [v19: int] : ? [v20: int] : ($i(v18) & % 19.83/3.55 | $i(v13) & $i(v12) & $i(v5) & $i(v4) & $i(v3) & ((v19 = 0 & ~ (v20 % 19.83/3.55 | = 0) & apply(v1, v18, v18) = v20 & member(v18, v0) = 0) | % 19.83/3.55 | (v16 = 0 & v15 = 0 & v14 = 0 & ~ (v17 = 0) & apply(v1, v13, v12) % 19.83/3.55 | = v17 & apply(v1, v12, v13) = 0 & member(v13, v0) = 0 & % 19.83/3.55 | member(v12, v0) = 0) | (v10 = 0 & v9 = 0 & v8 = 0 & v7 = 0 & v6 % 19.83/3.55 | = 0 & ~ (v11 = 0) & apply(v1, v4, v5) = 0 & apply(v1, v3, v5) % 19.83/3.55 | = v11 & apply(v1, v3, v4) = 0 & member(v5, v0) = 0 & member(v4, % 19.83/3.55 | v0) = 0 & member(v3, v0) = 0)))) % 19.83/3.55 | % 19.83/3.55 | ALPHA: (pre_order) implies: % 19.83/3.55 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (pre_order(v0, v1) = 0) | % 19.83/3.55 | ~ (member(v2, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 19.83/3.55 | apply(v0, v2, v2) = 0) % 19.83/3.55 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 19.83/3.55 | ~ (pre_order(v0, v1) = 0) | ~ (member(v4, v1) = 0) | ~ (member(v3, % 19.83/3.55 | v1) = 0) | ~ (member(v2, v1) = 0) | ~ $i(v4) | ~ $i(v3) | ~ % 19.83/3.55 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? % 19.83/3.55 | [v7: any] : (apply(v0, v3, v4) = v6 & apply(v0, v2, v4) = v7 & % 19.83/3.55 | apply(v0, v2, v3) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | v7 = 0))) % 19.83/3.55 | % 19.83/3.55 | ALPHA: (function-axioms) implies: % 19.83/3.55 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 19.83/3.56 | ! [v3: $i] : (v1 = v0 | ~ (member(v3, v2) = v1) | ~ (member(v3, v2) % 19.83/3.56 | = v0)) % 19.83/3.56 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 19.83/3.56 | ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = v1) | ~ % 19.83/3.56 | (apply(v4, v3, v2) = v0)) % 19.83/3.56 | % 19.83/3.56 | DELTA: instantiating (thIII11) with fresh symbols all_20_0, all_20_1, % 19.83/3.56 | all_20_2, all_20_3 gives: % 19.83/3.56 | (6) ~ (all_20_0 = 0) & pre_order(all_20_2, all_20_3) = 0 & % 19.83/3.56 | equivalence(all_20_1, all_20_3) = all_20_0 & $i(all_20_1) & % 19.83/3.56 | $i(all_20_2) & $i(all_20_3) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] % 19.83/3.56 | : ( ~ (apply(all_20_1, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 19.83/3.56 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 19.83/3.56 | (apply(all_20_2, v1, v0) = v6 & apply(all_20_2, v0, v1) = v5 & % 19.83/3.56 | member(v1, all_20_3) = v4 & member(v0, all_20_3) = v3 & ( ~ (v4 = % 19.83/3.56 | 0) | ~ (v3 = 0) | (( ~ (v6 = 0) | ~ (v5 = 0) | v2 = 0) & ( ~ % 19.83/3.56 | (v2 = 0) | (v6 = 0 & v5 = 0)))))) & ! [v0: $i] : ! [v1: $i] % 19.83/3.56 | : ! [v2: any] : ( ~ (apply(all_20_2, v1, v0) = v2) | ~ $i(v1) | ~ % 19.83/3.56 | $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 19.83/3.56 | (apply(all_20_1, v0, v1) = v5 & apply(all_20_2, v0, v1) = v6 & % 19.83/3.56 | member(v1, all_20_3) = v4 & member(v0, all_20_3) = v3 & ( ~ (v4 = % 19.83/3.56 | 0) | ~ (v3 = 0) | (( ~ (v6 = 0) | ~ (v2 = 0) | v5 = 0) & ( ~ % 19.83/3.56 | (v5 = 0) | (v6 = 0 & v2 = 0)))))) & ! [v0: $i] : ! [v1: $i] % 19.83/3.56 | : ! [v2: any] : ( ~ (apply(all_20_2, v0, v1) = v2) | ~ $i(v1) | ~ % 19.83/3.56 | $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 19.83/3.56 | (apply(all_20_1, v0, v1) = v5 & apply(all_20_2, v1, v0) = v6 & % 19.83/3.56 | member(v1, all_20_3) = v4 & member(v0, all_20_3) = v3 & ( ~ (v4 = % 19.83/3.56 | 0) | ~ (v3 = 0) | (( ~ (v6 = 0) | ~ (v2 = 0) | v5 = 0) & ( ~ % 19.83/3.56 | (v5 = 0) | (v6 = 0 & v2 = 0)))))) % 19.83/3.56 | % 19.83/3.56 | ALPHA: (6) implies: % 19.83/3.56 | (7) ~ (all_20_0 = 0) % 19.83/3.56 | (8) $i(all_20_3) % 19.83/3.56 | (9) $i(all_20_2) % 19.83/3.56 | (10) $i(all_20_1) % 19.83/3.56 | (11) equivalence(all_20_1, all_20_3) = all_20_0 % 19.83/3.56 | (12) pre_order(all_20_2, all_20_3) = 0 % 19.83/3.56 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_20_1, v0, % 19.83/3.56 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 19.83/3.56 | : ? [v5: any] : ? [v6: any] : (apply(all_20_2, v1, v0) = v6 & % 19.83/3.56 | apply(all_20_2, v0, v1) = v5 & member(v1, all_20_3) = v4 & % 19.83/3.56 | member(v0, all_20_3) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (( ~ (v6 % 19.83/3.56 | = 0) | ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | (v6 = 0 & v5 % 19.83/3.56 | = 0)))))) % 19.83/3.56 | % 19.83/3.56 | GROUND_INST: instantiating (1) with all_20_3, all_20_1, all_20_0, simplifying % 19.83/3.56 | with (8), (10), (11) gives: % 19.83/3.57 | (14) all_20_0 = 0 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] % 19.83/3.57 | : ? [v4: int] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: % 19.83/3.57 | int] : ? [v9: $i] : ? [v10: $i] : ? [v11: int] : ? [v12: int] : % 19.83/3.57 | ? [v13: int] : ? [v14: int] : ? [v15: $i] : ? [v16: int] : ? [v17: % 19.83/3.57 | int] : ($i(v15) & $i(v10) & $i(v9) & $i(v2) & $i(v1) & $i(v0) & % 19.83/3.57 | ((v16 = 0 & ~ (v17 = 0) & apply(all_20_1, v15, v15) = v17 & % 19.83/3.57 | member(v15, all_20_3) = 0) | (v13 = 0 & v12 = 0 & v11 = 0 & ~ % 19.83/3.57 | (v14 = 0) & apply(all_20_1, v10, v9) = v14 & apply(all_20_1, v9, % 19.83/3.57 | v10) = 0 & member(v10, all_20_3) = 0 & member(v9, all_20_3) = % 19.83/3.57 | 0) | (v7 = 0 & v6 = 0 & v5 = 0 & v4 = 0 & v3 = 0 & ~ (v8 = 0) & % 19.83/3.57 | apply(all_20_1, v1, v2) = 0 & apply(all_20_1, v0, v2) = v8 & % 19.83/3.57 | apply(all_20_1, v0, v1) = 0 & member(v2, all_20_3) = 0 & % 19.83/3.57 | member(v1, all_20_3) = 0 & member(v0, all_20_3) = 0))) % 19.83/3.57 | % 19.83/3.57 | BETA: splitting (14) gives: % 19.83/3.57 | % 19.83/3.57 | Case 1: % 19.83/3.57 | | % 19.83/3.57 | | (15) all_20_0 = 0 % 19.83/3.57 | | % 19.83/3.57 | | REDUCE: (7), (15) imply: % 19.83/3.57 | | (16) $false % 19.83/3.57 | | % 19.83/3.57 | | CLOSE: (16) is inconsistent. % 19.83/3.57 | | % 19.83/3.57 | Case 2: % 19.83/3.57 | | % 19.83/3.57 | | (17) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ? [v4: % 19.83/3.57 | | int] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: int] : % 19.83/3.57 | | ? [v9: $i] : ? [v10: $i] : ? [v11: int] : ? [v12: int] : ? % 19.83/3.57 | | [v13: int] : ? [v14: int] : ? [v15: $i] : ? [v16: int] : ? [v17: % 19.83/3.57 | | int] : ($i(v15) & $i(v10) & $i(v9) & $i(v2) & $i(v1) & $i(v0) & % 19.83/3.57 | | ((v16 = 0 & ~ (v17 = 0) & apply(all_20_1, v15, v15) = v17 & % 19.83/3.57 | | member(v15, all_20_3) = 0) | (v13 = 0 & v12 = 0 & v11 = 0 & ~ % 19.83/3.57 | | (v14 = 0) & apply(all_20_1, v10, v9) = v14 & apply(all_20_1, % 19.83/3.57 | | v9, v10) = 0 & member(v10, all_20_3) = 0 & member(v9, % 19.83/3.57 | | all_20_3) = 0) | (v7 = 0 & v6 = 0 & v5 = 0 & v4 = 0 & v3 = 0 % 19.83/3.57 | | & ~ (v8 = 0) & apply(all_20_1, v1, v2) = 0 & apply(all_20_1, % 19.83/3.57 | | v0, v2) = v8 & apply(all_20_1, v0, v1) = 0 & member(v2, % 19.83/3.57 | | all_20_3) = 0 & member(v1, all_20_3) = 0 & member(v0, % 19.83/3.57 | | all_20_3) = 0))) % 19.83/3.57 | | % 19.83/3.57 | | DELTA: instantiating (17) with fresh symbols all_30_0, all_30_1, all_30_2, % 19.83/3.57 | | all_30_3, all_30_4, all_30_5, all_30_6, all_30_7, all_30_8, all_30_9, % 19.83/3.57 | | all_30_10, all_30_11, all_30_12, all_30_13, all_30_14, all_30_15, % 19.83/3.57 | | all_30_16, all_30_17 gives: % 19.83/3.57 | | (18) $i(all_30_2) & $i(all_30_7) & $i(all_30_8) & $i(all_30_15) & % 19.83/3.57 | | $i(all_30_16) & $i(all_30_17) & ((all_30_1 = 0 & ~ (all_30_0 = 0) & % 19.83/3.57 | | apply(all_20_1, all_30_2, all_30_2) = all_30_0 & % 19.83/3.57 | | member(all_30_2, all_20_3) = 0) | (all_30_4 = 0 & all_30_5 = 0 & % 19.83/3.57 | | all_30_6 = 0 & ~ (all_30_3 = 0) & apply(all_20_1, all_30_7, % 19.83/3.57 | | all_30_8) = all_30_3 & apply(all_20_1, all_30_8, all_30_7) = 0 % 19.83/3.57 | | & member(all_30_7, all_20_3) = 0 & member(all_30_8, all_20_3) = % 19.83/3.57 | | 0) | (all_30_10 = 0 & all_30_11 = 0 & all_30_12 = 0 & all_30_13 % 19.83/3.57 | | = 0 & all_30_14 = 0 & ~ (all_30_9 = 0) & apply(all_20_1, % 19.83/3.57 | | all_30_16, all_30_15) = 0 & apply(all_20_1, all_30_17, % 19.83/3.57 | | all_30_15) = all_30_9 & apply(all_20_1, all_30_17, all_30_16) % 19.83/3.57 | | = 0 & member(all_30_15, all_20_3) = 0 & member(all_30_16, % 19.83/3.57 | | all_20_3) = 0 & member(all_30_17, all_20_3) = 0)) % 19.83/3.57 | | % 19.83/3.57 | | ALPHA: (18) implies: % 19.83/3.57 | | (19) $i(all_30_17) % 19.83/3.57 | | (20) $i(all_30_16) % 19.83/3.57 | | (21) $i(all_30_15) % 19.83/3.57 | | (22) $i(all_30_8) % 19.83/3.57 | | (23) $i(all_30_7) % 19.83/3.57 | | (24) $i(all_30_2) % 19.83/3.57 | | (25) (all_30_1 = 0 & ~ (all_30_0 = 0) & apply(all_20_1, all_30_2, % 19.83/3.57 | | all_30_2) = all_30_0 & member(all_30_2, all_20_3) = 0) | % 19.83/3.57 | | (all_30_4 = 0 & all_30_5 = 0 & all_30_6 = 0 & ~ (all_30_3 = 0) & % 19.83/3.57 | | apply(all_20_1, all_30_7, all_30_8) = all_30_3 & apply(all_20_1, % 19.83/3.57 | | all_30_8, all_30_7) = 0 & member(all_30_7, all_20_3) = 0 & % 19.83/3.57 | | member(all_30_8, all_20_3) = 0) | (all_30_10 = 0 & all_30_11 = 0 & % 19.83/3.57 | | all_30_12 = 0 & all_30_13 = 0 & all_30_14 = 0 & ~ (all_30_9 = 0) % 19.83/3.57 | | & apply(all_20_1, all_30_16, all_30_15) = 0 & apply(all_20_1, % 19.83/3.57 | | all_30_17, all_30_15) = all_30_9 & apply(all_20_1, all_30_17, % 19.83/3.57 | | all_30_16) = 0 & member(all_30_15, all_20_3) = 0 & % 19.83/3.57 | | member(all_30_16, all_20_3) = 0 & member(all_30_17, all_20_3) = 0) % 19.83/3.57 | | % 19.83/3.57 | | BETA: splitting (25) gives: % 19.83/3.57 | | % 19.83/3.57 | | Case 1: % 19.83/3.57 | | | % 19.83/3.57 | | | (26) all_30_1 = 0 & ~ (all_30_0 = 0) & apply(all_20_1, all_30_2, % 19.83/3.57 | | | all_30_2) = all_30_0 & member(all_30_2, all_20_3) = 0 % 19.83/3.57 | | | % 19.83/3.57 | | | ALPHA: (26) implies: % 19.83/3.57 | | | (27) ~ (all_30_0 = 0) % 19.83/3.57 | | | (28) member(all_30_2, all_20_3) = 0 % 19.83/3.57 | | | (29) apply(all_20_1, all_30_2, all_30_2) = all_30_0 % 19.83/3.57 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (2) with all_20_2, all_20_3, all_30_2, % 19.83/3.58 | | | simplifying with (8), (9), (12), (24), (28) gives: % 19.83/3.58 | | | (30) apply(all_20_2, all_30_2, all_30_2) = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (13) with all_30_2, all_30_2, all_30_0, % 19.83/3.58 | | | simplifying with (24), (29) gives: % 19.83/3.58 | | | (31) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 19.83/3.58 | | | (apply(all_20_2, all_30_2, all_30_2) = v3 & apply(all_20_2, % 19.83/3.58 | | | all_30_2, all_30_2) = v2 & member(all_30_2, all_20_3) = v1 & % 19.83/3.58 | | | member(all_30_2, all_20_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 19.83/3.58 | | | (( ~ (v3 = 0) | ~ (v2 = 0) | all_30_0 = 0) & ( ~ (all_30_0 = % 19.83/3.58 | | | 0) | (v3 = 0 & v2 = 0))))) % 19.83/3.58 | | | % 19.83/3.58 | | | DELTA: instantiating (31) with fresh symbols all_47_0, all_47_1, all_47_2, % 19.83/3.58 | | | all_47_3 gives: % 19.83/3.58 | | | (32) apply(all_20_2, all_30_2, all_30_2) = all_47_0 & apply(all_20_2, % 19.83/3.58 | | | all_30_2, all_30_2) = all_47_1 & member(all_30_2, all_20_3) = % 19.83/3.58 | | | all_47_2 & member(all_30_2, all_20_3) = all_47_3 & ( ~ (all_47_2 = % 19.83/3.58 | | | 0) | ~ (all_47_3 = 0) | (( ~ (all_47_0 = 0) | ~ (all_47_1 = % 19.83/3.58 | | | 0) | all_30_0 = 0) & ( ~ (all_30_0 = 0) | (all_47_0 = 0 & % 19.83/3.58 | | | all_47_1 = 0)))) % 19.83/3.58 | | | % 19.83/3.58 | | | ALPHA: (32) implies: % 19.83/3.58 | | | (33) member(all_30_2, all_20_3) = all_47_3 % 19.83/3.58 | | | (34) member(all_30_2, all_20_3) = all_47_2 % 19.83/3.58 | | | (35) apply(all_20_2, all_30_2, all_30_2) = all_47_1 % 19.83/3.58 | | | (36) apply(all_20_2, all_30_2, all_30_2) = all_47_0 % 19.83/3.58 | | | (37) ~ (all_47_2 = 0) | ~ (all_47_3 = 0) | (( ~ (all_47_0 = 0) | ~ % 19.83/3.58 | | | (all_47_1 = 0) | all_30_0 = 0) & ( ~ (all_30_0 = 0) | % 19.83/3.58 | | | (all_47_0 = 0 & all_47_1 = 0))) % 19.83/3.58 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (4) with 0, all_47_2, all_20_3, all_30_2, % 19.83/3.58 | | | simplifying with (28), (34) gives: % 19.83/3.58 | | | (38) all_47_2 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (4) with all_47_3, all_47_2, all_20_3, % 19.83/3.58 | | | all_30_2, simplifying with (33), (34) gives: % 19.83/3.58 | | | (39) all_47_2 = all_47_3 % 19.83/3.58 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (5) with all_47_1, all_47_0, all_30_2, % 19.83/3.58 | | | all_30_2, all_20_2, simplifying with (35), (36) gives: % 19.83/3.58 | | | (40) all_47_0 = all_47_1 % 19.83/3.58 | | | % 19.83/3.58 | | | GROUND_INST: instantiating (5) with 0, all_47_0, all_30_2, all_30_2, % 19.83/3.58 | | | all_20_2, simplifying with (30), (36) gives: % 19.83/3.58 | | | (41) all_47_0 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | COMBINE_EQS: (40), (41) imply: % 19.83/3.58 | | | (42) all_47_1 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | SIMP: (42) implies: % 19.83/3.58 | | | (43) all_47_1 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | COMBINE_EQS: (38), (39) imply: % 19.83/3.58 | | | (44) all_47_3 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | SIMP: (44) implies: % 19.83/3.58 | | | (45) all_47_3 = 0 % 19.83/3.58 | | | % 19.83/3.58 | | | BETA: splitting (37) gives: % 19.83/3.58 | | | % 19.83/3.58 | | | Case 1: % 19.83/3.58 | | | | % 19.83/3.58 | | | | (46) ~ (all_47_2 = 0) % 19.83/3.58 | | | | % 19.83/3.58 | | | | REDUCE: (38), (46) imply: % 19.83/3.58 | | | | (47) $false % 19.83/3.58 | | | | % 19.83/3.58 | | | | CLOSE: (47) is inconsistent. % 19.83/3.58 | | | | % 19.83/3.58 | | | Case 2: % 19.83/3.58 | | | | % 19.83/3.58 | | | | (48) ~ (all_47_3 = 0) | (( ~ (all_47_0 = 0) | ~ (all_47_1 = 0) | % 19.83/3.58 | | | | all_30_0 = 0) & ( ~ (all_30_0 = 0) | (all_47_0 = 0 & % 19.83/3.58 | | | | all_47_1 = 0))) % 19.83/3.58 | | | | % 19.83/3.58 | | | | BETA: splitting (48) gives: % 19.83/3.58 | | | | % 19.83/3.58 | | | | Case 1: % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | (49) ~ (all_47_3 = 0) % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | REDUCE: (45), (49) imply: % 19.83/3.58 | | | | | (50) $false % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | CLOSE: (50) is inconsistent. % 19.83/3.58 | | | | | % 19.83/3.58 | | | | Case 2: % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | (51) ( ~ (all_47_0 = 0) | ~ (all_47_1 = 0) | all_30_0 = 0) & ( ~ % 19.83/3.58 | | | | | (all_30_0 = 0) | (all_47_0 = 0 & all_47_1 = 0)) % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | ALPHA: (51) implies: % 19.83/3.58 | | | | | (52) ~ (all_47_0 = 0) | ~ (all_47_1 = 0) | all_30_0 = 0 % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | BETA: splitting (52) gives: % 19.83/3.58 | | | | | % 19.83/3.58 | | | | | Case 1: % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | (53) ~ (all_47_0 = 0) % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | REDUCE: (41), (53) imply: % 19.83/3.58 | | | | | | (54) $false % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | CLOSE: (54) is inconsistent. % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | Case 2: % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | (55) ~ (all_47_1 = 0) | all_30_0 = 0 % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | BETA: splitting (55) gives: % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | | Case 1: % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | (56) ~ (all_47_1 = 0) % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | REDUCE: (43), (56) imply: % 19.83/3.58 | | | | | | | (57) $false % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | CLOSE: (57) is inconsistent. % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | Case 2: % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | (58) all_30_0 = 0 % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | REDUCE: (27), (58) imply: % 19.83/3.58 | | | | | | | (59) $false % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | | CLOSE: (59) is inconsistent. % 19.83/3.58 | | | | | | | % 19.83/3.58 | | | | | | End of split % 19.83/3.58 | | | | | | % 19.83/3.58 | | | | | End of split % 19.83/3.58 | | | | | % 19.83/3.58 | | | | End of split % 19.83/3.58 | | | | % 19.83/3.58 | | | End of split % 19.83/3.58 | | | % 19.83/3.58 | | Case 2: % 19.83/3.58 | | | % 19.83/3.58 | | | (60) (all_30_4 = 0 & all_30_5 = 0 & all_30_6 = 0 & ~ (all_30_3 = 0) & % 19.83/3.58 | | | apply(all_20_1, all_30_7, all_30_8) = all_30_3 & apply(all_20_1, % 19.83/3.58 | | | all_30_8, all_30_7) = 0 & member(all_30_7, all_20_3) = 0 & % 19.83/3.58 | | | member(all_30_8, all_20_3) = 0) | (all_30_10 = 0 & all_30_11 = 0 % 19.83/3.58 | | | & all_30_12 = 0 & all_30_13 = 0 & all_30_14 = 0 & ~ (all_30_9 = % 19.83/3.58 | | | 0) & apply(all_20_1, all_30_16, all_30_15) = 0 & % 19.83/3.58 | | | apply(all_20_1, all_30_17, all_30_15) = all_30_9 & % 19.83/3.58 | | | apply(all_20_1, all_30_17, all_30_16) = 0 & member(all_30_15, % 19.83/3.58 | | | all_20_3) = 0 & member(all_30_16, all_20_3) = 0 & % 19.83/3.58 | | | member(all_30_17, all_20_3) = 0) % 19.83/3.58 | | | % 19.83/3.58 | | | BETA: splitting (60) gives: % 19.83/3.58 | | | % 19.83/3.58 | | | Case 1: % 19.83/3.58 | | | | % 19.83/3.58 | | | | (61) all_30_4 = 0 & all_30_5 = 0 & all_30_6 = 0 & ~ (all_30_3 = 0) & % 19.83/3.58 | | | | apply(all_20_1, all_30_7, all_30_8) = all_30_3 & apply(all_20_1, % 19.83/3.58 | | | | all_30_8, all_30_7) = 0 & member(all_30_7, all_20_3) = 0 & % 19.83/3.58 | | | | member(all_30_8, all_20_3) = 0 % 19.83/3.59 | | | | % 19.83/3.59 | | | | ALPHA: (61) implies: % 19.83/3.59 | | | | (62) ~ (all_30_3 = 0) % 19.83/3.59 | | | | (63) member(all_30_8, all_20_3) = 0 % 19.83/3.59 | | | | (64) member(all_30_7, all_20_3) = 0 % 19.83/3.59 | | | | (65) apply(all_20_1, all_30_8, all_30_7) = 0 % 19.83/3.59 | | | | (66) apply(all_20_1, all_30_7, all_30_8) = all_30_3 % 19.83/3.59 | | | | % 19.83/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_8, % 19.83/3.59 | | | | all_30_7, all_30_7, simplifying with (8), (9), (12), (22), % 19.83/3.59 | | | | (23), (63), (64) gives: % 19.83/3.59 | | | | (67) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 19.83/3.59 | | | | all_30_7, all_30_7) = v1 & apply(all_20_2, all_30_8, % 19.83/3.59 | | | | all_30_7) = v2 & apply(all_20_2, all_30_8, all_30_7) = v0 & % 19.83/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.83/3.59 | | | | % 19.83/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_7, % 19.83/3.59 | | | | all_30_8, all_30_7, simplifying with (8), (9), (12), (22), % 19.83/3.59 | | | | (23), (63), (64) gives: % 19.83/3.59 | | | | (68) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 19.83/3.59 | | | | all_30_7, all_30_7) = v2 & apply(all_20_2, all_30_7, % 19.83/3.59 | | | | all_30_8) = v0 & apply(all_20_2, all_30_8, all_30_7) = v1 & % 19.83/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.83/3.59 | | | | % 19.83/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_7, % 19.83/3.59 | | | | all_30_7, all_30_8, simplifying with (8), (9), (12), (22), % 19.83/3.59 | | | | (23), (63), (64) gives: % 19.83/3.59 | | | | (69) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 19.83/3.59 | | | | all_30_7, all_30_7) = v0 & apply(all_20_2, all_30_7, % 19.83/3.59 | | | | all_30_8) = v2 & apply(all_20_2, all_30_7, all_30_8) = v1 & % 19.83/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.83/3.59 | | | | % 20.31/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_8, % 20.31/3.59 | | | | all_30_8, all_30_7, simplifying with (8), (9), (12), (22), % 20.31/3.59 | | | | (23), (63), (64) gives: % 20.31/3.59 | | | | (70) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.31/3.59 | | | | all_30_8, all_30_7) = v2 & apply(all_20_2, all_30_8, % 20.31/3.59 | | | | all_30_7) = v1 & apply(all_20_2, all_30_8, all_30_8) = v0 & % 20.31/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.31/3.59 | | | | % 20.31/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_8, % 20.31/3.59 | | | | all_30_7, all_30_8, simplifying with (8), (9), (12), (22), % 20.31/3.59 | | | | (23), (63), (64) gives: % 20.31/3.59 | | | | (71) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.31/3.59 | | | | all_30_7, all_30_8) = v1 & apply(all_20_2, all_30_8, % 20.31/3.59 | | | | all_30_7) = v0 & apply(all_20_2, all_30_8, all_30_8) = v2 & % 20.31/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.31/3.59 | | | | % 20.31/3.59 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_7, % 20.31/3.59 | | | | all_30_8, all_30_8, simplifying with (8), (9), (12), (22), % 20.31/3.59 | | | | (23), (63), (64) gives: % 20.31/3.59 | | | | (72) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.31/3.59 | | | | all_30_7, all_30_8) = v2 & apply(all_20_2, all_30_7, % 20.31/3.59 | | | | all_30_8) = v0 & apply(all_20_2, all_30_8, all_30_8) = v1 & % 20.31/3.59 | | | | ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.31/3.59 | | | | % 20.31/3.59 | | | | GROUND_INST: instantiating (13) with all_30_8, all_30_7, 0, simplifying % 20.31/3.59 | | | | with (22), (23), (65) gives: % 20.31/3.59 | | | | (73) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 20.31/3.59 | | | | (apply(all_20_2, all_30_7, all_30_8) = v3 & apply(all_20_2, % 20.31/3.59 | | | | all_30_8, all_30_7) = v2 & member(all_30_7, all_20_3) = v1 & % 20.31/3.59 | | | | member(all_30_8, all_20_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 20.31/3.59 | | | | (v3 = 0 & v2 = 0))) % 20.31/3.59 | | | | % 20.31/3.59 | | | | GROUND_INST: instantiating (13) with all_30_7, all_30_8, all_30_3, % 20.31/3.59 | | | | simplifying with (22), (23), (66) gives: % 20.31/3.59 | | | | (74) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 20.31/3.59 | | | | (apply(all_20_2, all_30_7, all_30_8) = v2 & apply(all_20_2, % 20.31/3.59 | | | | all_30_8, all_30_7) = v3 & member(all_30_7, all_20_3) = v0 & % 20.31/3.59 | | | | member(all_30_8, all_20_3) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 20.31/3.59 | | | | (( ~ (v3 = 0) | ~ (v2 = 0) | all_30_3 = 0) & ( ~ (all_30_3 % 20.31/3.59 | | | | = 0) | (v3 = 0 & v2 = 0))))) % 20.31/3.59 | | | | % 20.31/3.59 | | | | DELTA: instantiating (72) with fresh symbols all_45_0, all_45_1, % 20.31/3.59 | | | | all_45_2 gives: % 20.31/3.59 | | | | (75) apply(all_20_2, all_30_7, all_30_8) = all_45_0 & apply(all_20_2, % 20.31/3.59 | | | | all_30_7, all_30_8) = all_45_2 & apply(all_20_2, all_30_8, % 20.31/3.59 | | | | all_30_8) = all_45_1 & ( ~ (all_45_1 = 0) | ~ (all_45_2 = 0) % 20.31/3.59 | | | | | all_45_0 = 0) % 20.31/3.59 | | | | % 20.31/3.59 | | | | ALPHA: (75) implies: % 20.31/3.59 | | | | (76) apply(all_20_2, all_30_7, all_30_8) = all_45_2 % 20.31/3.59 | | | | (77) apply(all_20_2, all_30_7, all_30_8) = all_45_0 % 20.31/3.59 | | | | % 20.31/3.59 | | | | DELTA: instantiating (67) with fresh symbols all_47_0, all_47_1, % 20.31/3.59 | | | | all_47_2 gives: % 20.34/3.59 | | | | (78) apply(all_20_2, all_30_7, all_30_7) = all_47_1 & apply(all_20_2, % 20.34/3.59 | | | | all_30_8, all_30_7) = all_47_0 & apply(all_20_2, all_30_8, % 20.34/3.59 | | | | all_30_7) = all_47_2 & ( ~ (all_47_1 = 0) | ~ (all_47_2 = 0) % 20.34/3.59 | | | | | all_47_0 = 0) % 20.34/3.59 | | | | % 20.34/3.59 | | | | ALPHA: (78) implies: % 20.34/3.59 | | | | (79) apply(all_20_2, all_30_8, all_30_7) = all_47_2 % 20.34/3.60 | | | | (80) apply(all_20_2, all_30_8, all_30_7) = all_47_0 % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (71) with fresh symbols all_51_0, all_51_1, % 20.34/3.60 | | | | all_51_2 gives: % 20.34/3.60 | | | | (81) apply(all_20_2, all_30_7, all_30_8) = all_51_1 & apply(all_20_2, % 20.34/3.60 | | | | all_30_8, all_30_7) = all_51_2 & apply(all_20_2, all_30_8, % 20.34/3.60 | | | | all_30_8) = all_51_0 & ( ~ (all_51_1 = 0) | ~ (all_51_2 = 0) % 20.34/3.60 | | | | | all_51_0 = 0) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (81) implies: % 20.34/3.60 | | | | (82) apply(all_20_2, all_30_8, all_30_7) = all_51_2 % 20.34/3.60 | | | | (83) apply(all_20_2, all_30_7, all_30_8) = all_51_1 % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (69) with fresh symbols all_53_0, all_53_1, % 20.34/3.60 | | | | all_53_2 gives: % 20.34/3.60 | | | | (84) apply(all_20_2, all_30_7, all_30_7) = all_53_2 & apply(all_20_2, % 20.34/3.60 | | | | all_30_7, all_30_8) = all_53_0 & apply(all_20_2, all_30_7, % 20.34/3.60 | | | | all_30_8) = all_53_1 & ( ~ (all_53_1 = 0) | ~ (all_53_2 = 0) % 20.34/3.60 | | | | | all_53_0 = 0) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (84) implies: % 20.34/3.60 | | | | (85) apply(all_20_2, all_30_7, all_30_8) = all_53_1 % 20.34/3.60 | | | | (86) apply(all_20_2, all_30_7, all_30_8) = all_53_0 % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (68) with fresh symbols all_55_0, all_55_1, % 20.34/3.60 | | | | all_55_2 gives: % 20.34/3.60 | | | | (87) apply(all_20_2, all_30_7, all_30_7) = all_55_0 & apply(all_20_2, % 20.34/3.60 | | | | all_30_7, all_30_8) = all_55_2 & apply(all_20_2, all_30_8, % 20.34/3.60 | | | | all_30_7) = all_55_1 & ( ~ (all_55_1 = 0) | ~ (all_55_2 = 0) % 20.34/3.60 | | | | | all_55_0 = 0) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (87) implies: % 20.34/3.60 | | | | (88) apply(all_20_2, all_30_8, all_30_7) = all_55_1 % 20.34/3.60 | | | | (89) apply(all_20_2, all_30_7, all_30_8) = all_55_2 % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (70) with fresh symbols all_57_0, all_57_1, % 20.34/3.60 | | | | all_57_2 gives: % 20.34/3.60 | | | | (90) apply(all_20_2, all_30_8, all_30_7) = all_57_0 & apply(all_20_2, % 20.34/3.60 | | | | all_30_8, all_30_7) = all_57_1 & apply(all_20_2, all_30_8, % 20.34/3.60 | | | | all_30_8) = all_57_2 & ( ~ (all_57_1 = 0) | ~ (all_57_2 = 0) % 20.34/3.60 | | | | | all_57_0 = 0) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (90) implies: % 20.34/3.60 | | | | (91) apply(all_20_2, all_30_8, all_30_7) = all_57_1 % 20.34/3.60 | | | | (92) apply(all_20_2, all_30_8, all_30_7) = all_57_0 % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (73) with fresh symbols all_61_0, all_61_1, % 20.34/3.60 | | | | all_61_2, all_61_3 gives: % 20.34/3.60 | | | | (93) apply(all_20_2, all_30_7, all_30_8) = all_61_0 & apply(all_20_2, % 20.34/3.60 | | | | all_30_8, all_30_7) = all_61_1 & member(all_30_7, all_20_3) = % 20.34/3.60 | | | | all_61_2 & member(all_30_8, all_20_3) = all_61_3 & ( ~ (all_61_2 % 20.34/3.60 | | | | = 0) | ~ (all_61_3 = 0) | (all_61_0 = 0 & all_61_1 = 0)) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (93) implies: % 20.34/3.60 | | | | (94) member(all_30_8, all_20_3) = all_61_3 % 20.34/3.60 | | | | (95) member(all_30_7, all_20_3) = all_61_2 % 20.34/3.60 | | | | (96) apply(all_20_2, all_30_8, all_30_7) = all_61_1 % 20.34/3.60 | | | | (97) apply(all_20_2, all_30_7, all_30_8) = all_61_0 % 20.34/3.60 | | | | (98) ~ (all_61_2 = 0) | ~ (all_61_3 = 0) | (all_61_0 = 0 & all_61_1 % 20.34/3.60 | | | | = 0) % 20.34/3.60 | | | | % 20.34/3.60 | | | | DELTA: instantiating (74) with fresh symbols all_63_0, all_63_1, % 20.34/3.60 | | | | all_63_2, all_63_3 gives: % 20.34/3.60 | | | | (99) apply(all_20_2, all_30_7, all_30_8) = all_63_1 & apply(all_20_2, % 20.34/3.60 | | | | all_30_8, all_30_7) = all_63_0 & member(all_30_7, all_20_3) = % 20.34/3.60 | | | | all_63_3 & member(all_30_8, all_20_3) = all_63_2 & ( ~ (all_63_2 % 20.34/3.60 | | | | = 0) | ~ (all_63_3 = 0) | (( ~ (all_63_0 = 0) | ~ % 20.34/3.60 | | | | (all_63_1 = 0) | all_30_3 = 0) & ( ~ (all_30_3 = 0) | % 20.34/3.60 | | | | (all_63_0 = 0 & all_63_1 = 0)))) % 20.34/3.60 | | | | % 20.34/3.60 | | | | ALPHA: (99) implies: % 20.34/3.60 | | | | (100) member(all_30_8, all_20_3) = all_63_2 % 20.34/3.60 | | | | (101) member(all_30_7, all_20_3) = all_63_3 % 20.34/3.60 | | | | (102) apply(all_20_2, all_30_8, all_30_7) = all_63_0 % 20.34/3.60 | | | | (103) apply(all_20_2, all_30_7, all_30_8) = all_63_1 % 20.34/3.60 | | | | (104) ~ (all_63_2 = 0) | ~ (all_63_3 = 0) | (( ~ (all_63_0 = 0) | % 20.34/3.60 | | | | ~ (all_63_1 = 0) | all_30_3 = 0) & ( ~ (all_30_3 = 0) | % 20.34/3.60 | | | | (all_63_0 = 0 & all_63_1 = 0))) % 20.34/3.60 | | | | % 20.34/3.60 | | | | GROUND_INST: instantiating (4) with 0, all_63_2, all_20_3, all_30_8, % 20.34/3.60 | | | | simplifying with (63), (100) gives: % 20.34/3.60 | | | | (105) all_63_2 = 0 % 20.34/3.60 | | | | % 20.34/3.60 | | | | GROUND_INST: instantiating (4) with all_61_3, all_63_2, all_20_3, % 20.34/3.60 | | | | all_30_8, simplifying with (94), (100) gives: % 20.34/3.60 | | | | (106) all_63_2 = all_61_3 % 20.34/3.60 | | | | % 20.34/3.60 | | | | GROUND_INST: instantiating (4) with 0, all_63_3, all_20_3, all_30_7, % 20.34/3.60 | | | | simplifying with (64), (101) gives: % 20.34/3.60 | | | | (107) all_63_3 = 0 % 20.34/3.60 | | | | % 20.34/3.60 | | | | GROUND_INST: instantiating (4) with all_61_2, all_63_3, all_20_3, % 20.34/3.60 | | | | all_30_7, simplifying with (95), (101) gives: % 20.37/3.60 | | | | (108) all_63_3 = all_61_2 % 20.37/3.60 | | | | % 20.37/3.60 | | | | GROUND_INST: instantiating (5) with all_47_2, all_55_1, all_30_7, % 20.37/3.60 | | | | all_30_8, all_20_2, simplifying with (79), (88) gives: % 20.37/3.60 | | | | (109) all_55_1 = all_47_2 % 20.37/3.60 | | | | % 20.37/3.60 | | | | GROUND_INST: instantiating (5) with all_57_1, all_57_0, all_30_7, % 20.37/3.60 | | | | all_30_8, all_20_2, simplifying with (91), (92) gives: % 20.37/3.60 | | | | (110) all_57_0 = all_57_1 % 20.37/3.60 | | | | % 20.37/3.60 | | | | GROUND_INST: instantiating (5) with all_55_1, all_57_0, all_30_7, % 20.37/3.60 | | | | all_30_8, all_20_2, simplifying with (88), (92) gives: % 20.37/3.60 | | | | (111) all_57_0 = all_55_1 % 20.37/3.60 | | | | % 20.37/3.60 | | | | GROUND_INST: instantiating (5) with all_51_2, all_57_0, all_30_7, % 20.37/3.60 | | | | all_30_8, all_20_2, simplifying with (82), (92) gives: % 20.37/3.60 | | | | (112) all_57_0 = all_51_2 % 20.37/3.60 | | | | % 20.37/3.60 | | | | GROUND_INST: instantiating (5) with all_57_0, all_61_1, all_30_7, % 20.37/3.60 | | | | all_30_8, all_20_2, simplifying with (92), (96) gives: % 20.37/3.60 | | | | (113) all_61_1 = all_57_0 % 20.37/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_61_1, all_63_0, all_30_7, % 20.38/3.60 | | | | all_30_8, all_20_2, simplifying with (96), (102) gives: % 20.38/3.60 | | | | (114) all_63_0 = all_61_1 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_47_0, all_63_0, all_30_7, % 20.38/3.60 | | | | all_30_8, all_20_2, simplifying with (80), (102) gives: % 20.38/3.60 | | | | (115) all_63_0 = all_47_0 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_45_2, all_53_0, all_30_8, % 20.38/3.60 | | | | all_30_7, all_20_2, simplifying with (76), (86) gives: % 20.38/3.60 | | | | (116) all_53_0 = all_45_2 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_53_0, all_55_2, all_30_8, % 20.38/3.60 | | | | all_30_7, all_20_2, simplifying with (86), (89) gives: % 20.38/3.60 | | | | (117) all_55_2 = all_53_0 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_51_1, all_55_2, all_30_8, % 20.38/3.60 | | | | all_30_7, all_20_2, simplifying with (83), (89) gives: % 20.38/3.60 | | | | (118) all_55_2 = all_51_1 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_53_0, all_61_0, all_30_8, % 20.38/3.60 | | | | all_30_7, all_20_2, simplifying with (86), (97) gives: % 20.38/3.60 | | | | (119) all_61_0 = all_53_0 % 20.38/3.60 | | | | % 20.38/3.60 | | | | GROUND_INST: instantiating (5) with all_53_1, all_61_0, all_30_8, % 20.38/3.60 | | | | all_30_7, all_20_2, simplifying with (85), (97) gives: % 20.38/3.60 | | | | (120) all_61_0 = all_53_1 % 20.38/3.60 | | | | % 20.38/3.61 | | | | GROUND_INST: instantiating (5) with all_61_0, all_63_1, all_30_8, % 20.38/3.61 | | | | all_30_7, all_20_2, simplifying with (97), (103) gives: % 20.38/3.61 | | | | (121) all_63_1 = all_61_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | GROUND_INST: instantiating (5) with all_45_0, all_63_1, all_30_8, % 20.38/3.61 | | | | all_30_7, all_20_2, simplifying with (77), (103) gives: % 20.38/3.61 | | | | (122) all_63_1 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (114), (115) imply: % 20.38/3.61 | | | | (123) all_61_1 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (123) implies: % 20.38/3.61 | | | | (124) all_61_1 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (121), (122) imply: % 20.38/3.61 | | | | (125) all_61_0 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (125) implies: % 20.38/3.61 | | | | (126) all_61_0 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (105), (106) imply: % 20.38/3.61 | | | | (127) all_61_3 = 0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (127) implies: % 20.38/3.61 | | | | (128) all_61_3 = 0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (107), (108) imply: % 20.38/3.61 | | | | (129) all_61_2 = 0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (119), (120) imply: % 20.38/3.61 | | | | (130) all_53_0 = all_53_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (130) implies: % 20.38/3.61 | | | | (131) all_53_0 = all_53_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (120), (126) imply: % 20.38/3.61 | | | | (132) all_53_1 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (113), (124) imply: % 20.38/3.61 | | | | (133) all_57_0 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (133) implies: % 20.38/3.61 | | | | (134) all_57_0 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (110), (112) imply: % 20.38/3.61 | | | | (135) all_57_1 = all_51_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (110), (111) imply: % 20.38/3.61 | | | | (136) all_57_1 = all_55_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (110), (134) imply: % 20.38/3.61 | | | | (137) all_57_1 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (135), (137) imply: % 20.38/3.61 | | | | (138) all_51_2 = all_47_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (135), (136) imply: % 20.38/3.61 | | | | (139) all_55_1 = all_51_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (139) implies: % 20.38/3.61 | | | | (140) all_55_1 = all_51_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (109), (140) imply: % 20.38/3.61 | | | | (141) all_51_2 = all_47_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (141) implies: % 20.38/3.61 | | | | (142) all_51_2 = all_47_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (117), (118) imply: % 20.38/3.61 | | | | (143) all_53_0 = all_51_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (143) implies: % 20.38/3.61 | | | | (144) all_53_0 = all_51_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (131), (144) imply: % 20.38/3.61 | | | | (145) all_53_1 = all_51_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (145) implies: % 20.38/3.61 | | | | (146) all_53_1 = all_51_1 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (116), (144) imply: % 20.38/3.61 | | | | (147) all_51_1 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (132), (146) imply: % 20.38/3.61 | | | | (148) all_51_1 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (148) implies: % 20.38/3.61 | | | | (149) all_51_1 = all_45_0 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (147), (149) imply: % 20.38/3.61 | | | | (150) all_45_0 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | SIMP: (150) implies: % 20.38/3.61 | | | | (151) all_45_0 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (138), (142) imply: % 20.38/3.61 | | | | (152) all_47_0 = all_47_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (132), (151) imply: % 20.38/3.61 | | | | (153) all_53_1 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (124), (152) imply: % 20.38/3.61 | | | | (154) all_61_1 = all_47_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (120), (153) imply: % 20.38/3.61 | | | | (155) all_61_0 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (122), (151) imply: % 20.38/3.61 | | | | (156) all_63_1 = all_45_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | COMBINE_EQS: (115), (152) imply: % 20.38/3.61 | | | | (157) all_63_0 = all_47_2 % 20.38/3.61 | | | | % 20.38/3.61 | | | | BETA: splitting (98) gives: % 20.38/3.61 | | | | % 20.38/3.61 | | | | Case 1: % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | (158) ~ (all_61_2 = 0) % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | REDUCE: (129), (158) imply: % 20.38/3.61 | | | | | (159) $false % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | CLOSE: (159) is inconsistent. % 20.38/3.61 | | | | | % 20.38/3.61 | | | | Case 2: % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | (160) ~ (all_61_3 = 0) | (all_61_0 = 0 & all_61_1 = 0) % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | BETA: splitting (160) gives: % 20.38/3.61 | | | | | % 20.38/3.61 | | | | | Case 1: % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | (161) ~ (all_61_3 = 0) % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | REDUCE: (128), (161) imply: % 20.38/3.61 | | | | | | (162) $false % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | CLOSE: (162) is inconsistent. % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | Case 2: % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | (163) all_61_0 = 0 & all_61_1 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | ALPHA: (163) implies: % 20.38/3.61 | | | | | | (164) all_61_1 = 0 % 20.38/3.61 | | | | | | (165) all_61_0 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | COMBINE_EQS: (155), (165) imply: % 20.38/3.61 | | | | | | (166) all_45_2 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | SIMP: (166) implies: % 20.38/3.61 | | | | | | (167) all_45_2 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | COMBINE_EQS: (154), (164) imply: % 20.38/3.61 | | | | | | (168) all_47_2 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | SIMP: (168) implies: % 20.38/3.61 | | | | | | (169) all_47_2 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | COMBINE_EQS: (156), (167) imply: % 20.38/3.61 | | | | | | (170) all_63_1 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | COMBINE_EQS: (157), (169) imply: % 20.38/3.61 | | | | | | (171) all_63_0 = 0 % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | BETA: splitting (104) gives: % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | | Case 1: % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | (172) ~ (all_63_2 = 0) % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | REDUCE: (105), (172) imply: % 20.38/3.61 | | | | | | | (173) $false % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | CLOSE: (173) is inconsistent. % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | Case 2: % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | (174) ~ (all_63_3 = 0) | (( ~ (all_63_0 = 0) | ~ (all_63_1 = % 20.38/3.61 | | | | | | | 0) | all_30_3 = 0) & ( ~ (all_30_3 = 0) | (all_63_0 % 20.38/3.61 | | | | | | | = 0 & all_63_1 = 0))) % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | BETA: splitting (174) gives: % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | | Case 1: % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | (175) ~ (all_63_3 = 0) % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | REDUCE: (107), (175) imply: % 20.38/3.61 | | | | | | | | (176) $false % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | CLOSE: (176) is inconsistent. % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | Case 2: % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | (177) ( ~ (all_63_0 = 0) | ~ (all_63_1 = 0) | all_30_3 = 0) % 20.38/3.61 | | | | | | | | & ( ~ (all_30_3 = 0) | (all_63_0 = 0 & all_63_1 = 0)) % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | ALPHA: (177) implies: % 20.38/3.61 | | | | | | | | (178) ~ (all_63_0 = 0) | ~ (all_63_1 = 0) | all_30_3 = 0 % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | BETA: splitting (178) gives: % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | | Case 1: % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | (179) ~ (all_63_0 = 0) % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | REDUCE: (171), (179) imply: % 20.38/3.61 | | | | | | | | | (180) $false % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | CLOSE: (180) is inconsistent. % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | Case 2: % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | (181) ~ (all_63_1 = 0) | all_30_3 = 0 % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | BETA: splitting (181) gives: % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | | Case 1: % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | (182) ~ (all_63_1 = 0) % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | REDUCE: (170), (182) imply: % 20.38/3.61 | | | | | | | | | | (183) $false % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | CLOSE: (183) is inconsistent. % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | Case 2: % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | (184) all_30_3 = 0 % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | REDUCE: (62), (184) imply: % 20.38/3.61 | | | | | | | | | | (185) $false % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | | CLOSE: (185) is inconsistent. % 20.38/3.61 | | | | | | | | | | % 20.38/3.61 | | | | | | | | | End of split % 20.38/3.61 | | | | | | | | | % 20.38/3.61 | | | | | | | | End of split % 20.38/3.61 | | | | | | | | % 20.38/3.61 | | | | | | | End of split % 20.38/3.61 | | | | | | | % 20.38/3.61 | | | | | | End of split % 20.38/3.61 | | | | | | % 20.38/3.61 | | | | | End of split % 20.38/3.61 | | | | | % 20.38/3.61 | | | | End of split % 20.38/3.61 | | | | % 20.38/3.61 | | | Case 2: % 20.38/3.61 | | | | % 20.38/3.62 | | | | (186) all_30_10 = 0 & all_30_11 = 0 & all_30_12 = 0 & all_30_13 = 0 & % 20.38/3.62 | | | | all_30_14 = 0 & ~ (all_30_9 = 0) & apply(all_20_1, all_30_16, % 20.38/3.62 | | | | all_30_15) = 0 & apply(all_20_1, all_30_17, all_30_15) = % 20.38/3.62 | | | | all_30_9 & apply(all_20_1, all_30_17, all_30_16) = 0 & % 20.38/3.62 | | | | member(all_30_15, all_20_3) = 0 & member(all_30_16, all_20_3) = % 20.38/3.62 | | | | 0 & member(all_30_17, all_20_3) = 0 % 20.38/3.62 | | | | % 20.38/3.62 | | | | ALPHA: (186) implies: % 20.38/3.62 | | | | (187) ~ (all_30_9 = 0) % 20.38/3.62 | | | | (188) member(all_30_17, all_20_3) = 0 % 20.38/3.62 | | | | (189) member(all_30_16, all_20_3) = 0 % 20.38/3.62 | | | | (190) member(all_30_15, all_20_3) = 0 % 20.38/3.62 | | | | (191) apply(all_20_1, all_30_17, all_30_16) = 0 % 20.38/3.62 | | | | (192) apply(all_20_1, all_30_17, all_30_15) = all_30_9 % 20.38/3.62 | | | | (193) apply(all_20_1, all_30_16, all_30_15) = 0 % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.62 | | | | all_30_16, all_30_16, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (194) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_16, all_30_16) = v1 & apply(all_20_2, all_30_17, % 20.38/3.62 | | | | all_30_16) = v2 & apply(all_20_2, all_30_17, all_30_16) = % 20.38/3.62 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.62 | | | | all_30_17, all_30_16, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (195) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_16, all_30_16) = v2 & apply(all_20_2, all_30_16, % 20.38/3.62 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_16) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.62 | | | | all_30_16, all_30_17, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (196) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_16, all_30_16) = v0 & apply(all_20_2, all_30_16, % 20.38/3.62 | | | | all_30_17) = v2 & apply(all_20_2, all_30_16, all_30_17) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.62 | | | | all_30_17, all_30_16, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (197) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_17, all_30_16) = v2 & apply(all_20_2, all_30_17, % 20.38/3.62 | | | | all_30_16) = v1 & apply(all_20_2, all_30_17, all_30_17) = % 20.38/3.62 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.62 | | | | all_30_16, all_30_17, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (198) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_16, all_30_17) = v1 & apply(all_20_2, all_30_17, % 20.38/3.62 | | | | all_30_16) = v0 & apply(all_20_2, all_30_17, all_30_17) = % 20.38/3.62 | | | | v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.62 | | | | all_30_17, all_30_17, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (20), (188), (189) gives: % 20.38/3.62 | | | | (199) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_16, all_30_17) = v2 & apply(all_20_2, all_30_16, % 20.38/3.62 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_17) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.62 | | | | all_30_15, all_30_15, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (20), (21), (189), (190) gives: % 20.38/3.62 | | | | (200) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_15, all_30_15) = v1 & apply(all_20_2, all_30_16, % 20.38/3.62 | | | | all_30_15) = v2 & apply(all_20_2, all_30_16, all_30_15) = % 20.38/3.62 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.62 | | | | all_30_16, all_30_15, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (20), (21), (189), (190) gives: % 20.38/3.62 | | | | (201) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_15, all_30_15) = v2 & apply(all_20_2, all_30_15, % 20.38/3.62 | | | | all_30_16) = v0 & apply(all_20_2, all_30_16, all_30_15) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.62 | | | | all_30_15, all_30_15, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (21), (188), (190) gives: % 20.38/3.62 | | | | (202) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_15, all_30_15) = v1 & apply(all_20_2, all_30_17, % 20.38/3.62 | | | | all_30_15) = v2 & apply(all_20_2, all_30_17, all_30_15) = % 20.38/3.62 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.62 | | | | all_30_17, all_30_15, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (19), (21), (188), (190) gives: % 20.38/3.62 | | | | (203) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_15, all_30_15) = v2 & apply(all_20_2, all_30_15, % 20.38/3.62 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_15) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.62 | | | | all_30_15, all_30_16, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (20), (21), (189), (190) gives: % 20.38/3.62 | | | | (204) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.62 | | | | all_30_15, all_30_15) = v0 & apply(all_20_2, all_30_15, % 20.38/3.62 | | | | all_30_16) = v2 & apply(all_20_2, all_30_15, all_30_16) = % 20.38/3.62 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.62 | | | | % 20.38/3.62 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.62 | | | | all_30_16, all_30_15, simplifying with (8), (9), (12), % 20.38/3.62 | | | | (20), (21), (189), (190) gives: % 20.38/3.63 | | | | (205) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_16, all_30_15) = v2 & apply(all_20_2, all_30_16, % 20.38/3.63 | | | | all_30_15) = v1 & apply(all_20_2, all_30_16, all_30_16) = % 20.38/3.63 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.63 | | | | all_30_15, all_30_16, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (20), (21), (189), (190) gives: % 20.38/3.63 | | | | (206) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_16) = v1 & apply(all_20_2, all_30_16, % 20.38/3.63 | | | | all_30_15) = v0 & apply(all_20_2, all_30_16, all_30_16) = % 20.38/3.63 | | | | v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.63 | | | | all_30_16, all_30_16, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (20), (21), (189), (190) gives: % 20.38/3.63 | | | | (207) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_16) = v2 & apply(all_20_2, all_30_15, % 20.38/3.63 | | | | all_30_16) = v0 & apply(all_20_2, all_30_16, all_30_16) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.63 | | | | all_30_16, all_30_15, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (208) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_16, all_30_15) = v1 & apply(all_20_2, all_30_17, % 20.38/3.63 | | | | all_30_15) = v2 & apply(all_20_2, all_30_17, all_30_16) = % 20.38/3.63 | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.63 | | | | all_30_15, all_30_16, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (209) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_16) = v1 & apply(all_20_2, all_30_17, % 20.38/3.63 | | | | all_30_15) = v0 & apply(all_20_2, all_30_17, all_30_16) = % 20.38/3.63 | | | | v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.63 | | | | all_30_17, all_30_16, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (210) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_16) = v2 & apply(all_20_2, all_30_15, % 20.38/3.63 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_16) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.63 | | | | all_30_15, all_30_17, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (21), (188), (190) gives: % 20.38/3.63 | | | | (211) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_15) = v0 & apply(all_20_2, all_30_15, % 20.38/3.63 | | | | all_30_17) = v2 & apply(all_20_2, all_30_15, all_30_17) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.63 | | | | all_30_17, all_30_15, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (212) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_16, all_30_15) = v2 & apply(all_20_2, all_30_16, % 20.38/3.63 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_15) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_16, % 20.38/3.63 | | | | all_30_15, all_30_17, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (213) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_17) = v1 & apply(all_20_2, all_30_16, % 20.38/3.63 | | | | all_30_15) = v0 & apply(all_20_2, all_30_16, all_30_17) = % 20.38/3.63 | | | | v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.63 | | | | all_30_16, all_30_17, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (20), (21), (188), (189), (190) gives: % 20.38/3.63 | | | | (214) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_16) = v0 & apply(all_20_2, all_30_15, % 20.38/3.63 | | | | all_30_17) = v2 & apply(all_20_2, all_30_16, all_30_17) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_17, % 20.38/3.63 | | | | all_30_15, all_30_17, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (21), (188), (190) gives: % 20.38/3.63 | | | | (215) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_17) = v1 & apply(all_20_2, all_30_17, % 20.38/3.63 | | | | all_30_15) = v0 & apply(all_20_2, all_30_17, all_30_17) = % 20.38/3.63 | | | | v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (3) with all_20_2, all_20_3, all_30_15, % 20.38/3.63 | | | | all_30_17, all_30_17, simplifying with (8), (9), (12), % 20.38/3.63 | | | | (19), (21), (188), (190) gives: % 20.38/3.63 | | | | (216) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_20_2, % 20.38/3.63 | | | | all_30_15, all_30_17) = v2 & apply(all_20_2, all_30_15, % 20.38/3.63 | | | | all_30_17) = v0 & apply(all_20_2, all_30_17, all_30_17) = % 20.38/3.63 | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (13) with all_30_17, all_30_16, 0, % 20.38/3.63 | | | | simplifying with (19), (20), (191) gives: % 20.38/3.63 | | | | (217) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 20.38/3.63 | | | | (apply(all_20_2, all_30_16, all_30_17) = v3 & apply(all_20_2, % 20.38/3.63 | | | | all_30_17, all_30_16) = v2 & member(all_30_16, all_20_3) = % 20.38/3.63 | | | | v1 & member(all_30_17, all_20_3) = v0 & ( ~ (v1 = 0) | ~ (v0 % 20.38/3.63 | | | | = 0) | (v3 = 0 & v2 = 0))) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (13) with all_30_17, all_30_15, all_30_9, % 20.38/3.63 | | | | simplifying with (19), (21), (192) gives: % 20.38/3.63 | | | | (218) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 20.38/3.63 | | | | (apply(all_20_2, all_30_15, all_30_17) = v3 & apply(all_20_2, % 20.38/3.63 | | | | all_30_17, all_30_15) = v2 & member(all_30_15, all_20_3) = % 20.38/3.63 | | | | v1 & member(all_30_17, all_20_3) = v0 & ( ~ (v1 = 0) | ~ (v0 % 20.38/3.63 | | | | = 0) | (( ~ (v3 = 0) | ~ (v2 = 0) | all_30_9 = 0) & ( ~ % 20.38/3.63 | | | | (all_30_9 = 0) | (v3 = 0 & v2 = 0))))) % 20.38/3.63 | | | | % 20.38/3.63 | | | | GROUND_INST: instantiating (13) with all_30_16, all_30_15, 0, % 20.38/3.63 | | | | simplifying with (20), (21), (193) gives: % 20.38/3.63 | | | | (219) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 20.38/3.63 | | | | (apply(all_20_2, all_30_15, all_30_16) = v3 & apply(all_20_2, % 20.38/3.63 | | | | all_30_16, all_30_15) = v2 & member(all_30_15, all_20_3) = % 20.38/3.63 | | | | v1 & member(all_30_16, all_20_3) = v0 & ( ~ (v1 = 0) | ~ (v0 % 20.38/3.63 | | | | = 0) | (v3 = 0 & v2 = 0))) % 20.38/3.63 | | | | % 20.38/3.63 | | | | DELTA: instantiating (200) with fresh symbols all_45_0, all_45_1, % 20.38/3.63 | | | | all_45_2 gives: % 20.38/3.63 | | | | (220) apply(all_20_2, all_30_15, all_30_15) = all_45_1 & % 20.38/3.63 | | | | apply(all_20_2, all_30_16, all_30_15) = all_45_0 & % 20.38/3.63 | | | | apply(all_20_2, all_30_16, all_30_15) = all_45_2 & ( ~ % 20.38/3.63 | | | | (all_45_1 = 0) | ~ (all_45_2 = 0) | all_45_0 = 0) % 20.38/3.63 | | | | % 20.38/3.63 | | | | ALPHA: (220) implies: % 20.38/3.63 | | | | (221) apply(all_20_2, all_30_16, all_30_15) = all_45_2 % 20.38/3.63 | | | | (222) apply(all_20_2, all_30_16, all_30_15) = all_45_0 % 20.38/3.63 | | | | % 20.38/3.63 | | | | DELTA: instantiating (194) with fresh symbols all_49_0, all_49_1, % 20.38/3.63 | | | | all_49_2 gives: % 20.38/3.63 | | | | (223) apply(all_20_2, all_30_16, all_30_16) = all_49_1 & % 20.38/3.63 | | | | apply(all_20_2, all_30_17, all_30_16) = all_49_0 & % 20.38/3.63 | | | | apply(all_20_2, all_30_17, all_30_16) = all_49_2 & ( ~ % 20.38/3.63 | | | | (all_49_1 = 0) | ~ (all_49_2 = 0) | all_49_0 = 0) % 20.38/3.63 | | | | % 20.38/3.63 | | | | ALPHA: (223) implies: % 20.38/3.63 | | | | (224) apply(all_20_2, all_30_17, all_30_16) = all_49_2 % 20.38/3.63 | | | | (225) apply(all_20_2, all_30_17, all_30_16) = all_49_0 % 20.38/3.63 | | | | % 20.38/3.63 | | | | DELTA: instantiating (198) with fresh symbols all_51_0, all_51_1, % 20.38/3.63 | | | | all_51_2 gives: % 20.38/3.64 | | | | (226) apply(all_20_2, all_30_16, all_30_17) = all_51_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_16) = all_51_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_17) = all_51_0 & ( ~ % 20.38/3.64 | | | | (all_51_1 = 0) | ~ (all_51_2 = 0) | all_51_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (226) implies: % 20.38/3.64 | | | | (227) apply(all_20_2, all_30_17, all_30_16) = all_51_2 % 20.38/3.64 | | | | (228) apply(all_20_2, all_30_16, all_30_17) = all_51_1 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (197) with fresh symbols all_53_0, all_53_1, % 20.38/3.64 | | | | all_53_2 gives: % 20.38/3.64 | | | | (229) apply(all_20_2, all_30_17, all_30_16) = all_53_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_16) = all_53_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_17) = all_53_2 & ( ~ % 20.38/3.64 | | | | (all_53_1 = 0) | ~ (all_53_2 = 0) | all_53_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (229) implies: % 20.38/3.64 | | | | (230) apply(all_20_2, all_30_17, all_30_16) = all_53_1 % 20.38/3.64 | | | | (231) apply(all_20_2, all_30_17, all_30_16) = all_53_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (216) with fresh symbols all_55_0, all_55_1, % 20.38/3.64 | | | | all_55_2 gives: % 20.38/3.64 | | | | (232) apply(all_20_2, all_30_15, all_30_17) = all_55_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_55_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_17) = all_55_1 & ( ~ % 20.38/3.64 | | | | (all_55_1 = 0) | ~ (all_55_2 = 0) | all_55_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (232) implies: % 20.38/3.64 | | | | (233) apply(all_20_2, all_30_15, all_30_17) = all_55_2 % 20.38/3.64 | | | | (234) apply(all_20_2, all_30_15, all_30_17) = all_55_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (204) with fresh symbols all_57_0, all_57_1, % 20.38/3.64 | | | | all_57_2 gives: % 20.38/3.64 | | | | (235) apply(all_20_2, all_30_15, all_30_15) = all_57_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_16) = all_57_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_16) = all_57_1 & ( ~ % 20.38/3.64 | | | | (all_57_1 = 0) | ~ (all_57_2 = 0) | all_57_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (235) implies: % 20.38/3.64 | | | | (236) apply(all_20_2, all_30_15, all_30_16) = all_57_1 % 20.38/3.64 | | | | (237) apply(all_20_2, all_30_15, all_30_16) = all_57_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (202) with fresh symbols all_59_0, all_59_1, % 20.38/3.64 | | | | all_59_2 gives: % 20.38/3.64 | | | | (238) apply(all_20_2, all_30_15, all_30_15) = all_59_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_59_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_59_2 & ( ~ % 20.38/3.64 | | | | (all_59_1 = 0) | ~ (all_59_2 = 0) | all_59_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (238) implies: % 20.38/3.64 | | | | (239) apply(all_20_2, all_30_17, all_30_15) = all_59_2 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (201) with fresh symbols all_61_0, all_61_1, % 20.38/3.64 | | | | all_61_2 gives: % 20.38/3.64 | | | | (240) apply(all_20_2, all_30_15, all_30_15) = all_61_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_16) = all_61_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_15) = all_61_1 & ( ~ % 20.38/3.64 | | | | (all_61_1 = 0) | ~ (all_61_2 = 0) | all_61_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (240) implies: % 20.38/3.64 | | | | (241) apply(all_20_2, all_30_16, all_30_15) = all_61_1 % 20.38/3.64 | | | | (242) apply(all_20_2, all_30_15, all_30_16) = all_61_2 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (203) with fresh symbols all_63_0, all_63_1, % 20.38/3.64 | | | | all_63_2 gives: % 20.38/3.64 | | | | (243) apply(all_20_2, all_30_15, all_30_15) = all_63_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_63_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_63_1 & ( ~ % 20.38/3.64 | | | | (all_63_1 = 0) | ~ (all_63_2 = 0) | all_63_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (243) implies: % 20.38/3.64 | | | | (244) apply(all_20_2, all_30_15, all_30_17) = all_63_2 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (199) with fresh symbols all_65_0, all_65_1, % 20.38/3.64 | | | | all_65_2 gives: % 20.38/3.64 | | | | (245) apply(all_20_2, all_30_16, all_30_17) = all_65_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_65_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_17) = all_65_1 & ( ~ % 20.38/3.64 | | | | (all_65_1 = 0) | ~ (all_65_2 = 0) | all_65_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (245) implies: % 20.38/3.64 | | | | (246) apply(all_20_2, all_30_16, all_30_17) = all_65_2 % 20.38/3.64 | | | | (247) apply(all_20_2, all_30_16, all_30_17) = all_65_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (215) with fresh symbols all_67_0, all_67_1, % 20.38/3.64 | | | | all_67_2 gives: % 20.38/3.64 | | | | (248) apply(all_20_2, all_30_15, all_30_17) = all_67_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_67_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_17) = all_67_0 & ( ~ % 20.38/3.64 | | | | (all_67_1 = 0) | ~ (all_67_2 = 0) | all_67_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (248) implies: % 20.38/3.64 | | | | (249) apply(all_20_2, all_30_15, all_30_17) = all_67_1 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (196) with fresh symbols all_73_0, all_73_1, % 20.38/3.64 | | | | all_73_2 gives: % 20.38/3.64 | | | | (250) apply(all_20_2, all_30_16, all_30_16) = all_73_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_73_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_73_1 & ( ~ % 20.38/3.64 | | | | (all_73_1 = 0) | ~ (all_73_2 = 0) | all_73_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (250) implies: % 20.38/3.64 | | | | (251) apply(all_20_2, all_30_16, all_30_17) = all_73_1 % 20.38/3.64 | | | | (252) apply(all_20_2, all_30_16, all_30_17) = all_73_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (195) with fresh symbols all_75_0, all_75_1, % 20.38/3.64 | | | | all_75_2 gives: % 20.38/3.64 | | | | (253) apply(all_20_2, all_30_16, all_30_16) = all_75_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_75_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_16) = all_75_1 & ( ~ % 20.38/3.64 | | | | (all_75_1 = 0) | ~ (all_75_2 = 0) | all_75_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (253) implies: % 20.38/3.64 | | | | (254) apply(all_20_2, all_30_17, all_30_16) = all_75_1 % 20.38/3.64 | | | | (255) apply(all_20_2, all_30_16, all_30_17) = all_75_2 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (214) with fresh symbols all_77_0, all_77_1, % 20.38/3.64 | | | | all_77_2 gives: % 20.38/3.64 | | | | (256) apply(all_20_2, all_30_15, all_30_16) = all_77_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_77_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_77_1 & ( ~ % 20.38/3.64 | | | | (all_77_1 = 0) | ~ (all_77_2 = 0) | all_77_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (256) implies: % 20.38/3.64 | | | | (257) apply(all_20_2, all_30_16, all_30_17) = all_77_1 % 20.38/3.64 | | | | (258) apply(all_20_2, all_30_15, all_30_17) = all_77_0 % 20.38/3.64 | | | | (259) apply(all_20_2, all_30_15, all_30_16) = all_77_2 % 20.38/3.64 | | | | (260) ~ (all_77_1 = 0) | ~ (all_77_2 = 0) | all_77_0 = 0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (213) with fresh symbols all_79_0, all_79_1, % 20.38/3.64 | | | | all_79_2 gives: % 20.38/3.64 | | | | (261) apply(all_20_2, all_30_15, all_30_17) = all_79_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_15) = all_79_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_79_0 & ( ~ % 20.38/3.64 | | | | (all_79_1 = 0) | ~ (all_79_2 = 0) | all_79_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (261) implies: % 20.38/3.64 | | | | (262) apply(all_20_2, all_30_16, all_30_17) = all_79_0 % 20.38/3.64 | | | | (263) apply(all_20_2, all_30_16, all_30_15) = all_79_2 % 20.38/3.64 | | | | (264) apply(all_20_2, all_30_15, all_30_17) = all_79_1 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (212) with fresh symbols all_81_0, all_81_1, % 20.38/3.64 | | | | all_81_2 gives: % 20.38/3.64 | | | | (265) apply(all_20_2, all_30_16, all_30_15) = all_81_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_17) = all_81_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_81_1 & ( ~ % 20.38/3.64 | | | | (all_81_1 = 0) | ~ (all_81_2 = 0) | all_81_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (265) implies: % 20.38/3.64 | | | | (266) apply(all_20_2, all_30_16, all_30_17) = all_81_2 % 20.38/3.64 | | | | (267) apply(all_20_2, all_30_16, all_30_15) = all_81_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (211) with fresh symbols all_83_0, all_83_1, % 20.38/3.64 | | | | all_83_2 gives: % 20.38/3.64 | | | | (268) apply(all_20_2, all_30_15, all_30_15) = all_83_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_83_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_83_1 & ( ~ % 20.38/3.64 | | | | (all_83_1 = 0) | ~ (all_83_2 = 0) | all_83_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (268) implies: % 20.38/3.64 | | | | (269) apply(all_20_2, all_30_15, all_30_17) = all_83_1 % 20.38/3.64 | | | | (270) apply(all_20_2, all_30_15, all_30_17) = all_83_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (208) with fresh symbols all_85_0, all_85_1, % 20.38/3.64 | | | | all_85_2 gives: % 20.38/3.64 | | | | (271) apply(all_20_2, all_30_16, all_30_15) = all_85_1 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_15) = all_85_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_16) = all_85_2 & ( ~ % 20.38/3.64 | | | | (all_85_1 = 0) | ~ (all_85_2 = 0) | all_85_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (271) implies: % 20.38/3.64 | | | | (272) apply(all_20_2, all_30_17, all_30_16) = all_85_2 % 20.38/3.64 | | | | (273) apply(all_20_2, all_30_17, all_30_15) = all_85_0 % 20.38/3.64 | | | | (274) apply(all_20_2, all_30_16, all_30_15) = all_85_1 % 20.38/3.64 | | | | (275) ~ (all_85_1 = 0) | ~ (all_85_2 = 0) | all_85_0 = 0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (207) with fresh symbols all_87_0, all_87_1, % 20.38/3.64 | | | | all_87_2 gives: % 20.38/3.64 | | | | (276) apply(all_20_2, all_30_15, all_30_16) = all_87_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_16) = all_87_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_16, all_30_16) = all_87_1 & ( ~ % 20.38/3.64 | | | | (all_87_1 = 0) | ~ (all_87_2 = 0) | all_87_0 = 0) % 20.38/3.64 | | | | % 20.38/3.64 | | | | ALPHA: (276) implies: % 20.38/3.64 | | | | (277) apply(all_20_2, all_30_15, all_30_16) = all_87_2 % 20.38/3.64 | | | | (278) apply(all_20_2, all_30_15, all_30_16) = all_87_0 % 20.38/3.64 | | | | % 20.38/3.64 | | | | DELTA: instantiating (210) with fresh symbols all_89_0, all_89_1, % 20.38/3.64 | | | | all_89_2 gives: % 20.38/3.64 | | | | (279) apply(all_20_2, all_30_15, all_30_16) = all_89_0 & % 20.38/3.64 | | | | apply(all_20_2, all_30_15, all_30_17) = all_89_2 & % 20.38/3.64 | | | | apply(all_20_2, all_30_17, all_30_16) = all_89_1 & ( ~ % 20.38/3.65 | | | | (all_89_1 = 0) | ~ (all_89_2 = 0) | all_89_0 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (279) implies: % 20.38/3.65 | | | | (280) apply(all_20_2, all_30_17, all_30_16) = all_89_1 % 20.38/3.65 | | | | (281) apply(all_20_2, all_30_15, all_30_17) = all_89_2 % 20.38/3.65 | | | | (282) apply(all_20_2, all_30_15, all_30_16) = all_89_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (209) with fresh symbols all_93_0, all_93_1, % 20.38/3.65 | | | | all_93_2 gives: % 20.38/3.65 | | | | (283) apply(all_20_2, all_30_15, all_30_16) = all_93_1 & % 20.38/3.65 | | | | apply(all_20_2, all_30_17, all_30_15) = all_93_2 & % 20.38/3.65 | | | | apply(all_20_2, all_30_17, all_30_16) = all_93_0 & ( ~ % 20.38/3.65 | | | | (all_93_1 = 0) | ~ (all_93_2 = 0) | all_93_0 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (283) implies: % 20.38/3.65 | | | | (284) apply(all_20_2, all_30_17, all_30_16) = all_93_0 % 20.38/3.65 | | | | (285) apply(all_20_2, all_30_17, all_30_15) = all_93_2 % 20.38/3.65 | | | | (286) apply(all_20_2, all_30_15, all_30_16) = all_93_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (206) with fresh symbols all_95_0, all_95_1, % 20.38/3.65 | | | | all_95_2 gives: % 20.38/3.65 | | | | (287) apply(all_20_2, all_30_15, all_30_16) = all_95_1 & % 20.38/3.65 | | | | apply(all_20_2, all_30_16, all_30_15) = all_95_2 & % 20.38/3.65 | | | | apply(all_20_2, all_30_16, all_30_16) = all_95_0 & ( ~ % 20.38/3.65 | | | | (all_95_1 = 0) | ~ (all_95_2 = 0) | all_95_0 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (287) implies: % 20.38/3.65 | | | | (288) apply(all_20_2, all_30_16, all_30_15) = all_95_2 % 20.38/3.65 | | | | (289) apply(all_20_2, all_30_15, all_30_16) = all_95_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (205) with fresh symbols all_97_0, all_97_1, % 20.38/3.65 | | | | all_97_2 gives: % 20.38/3.65 | | | | (290) apply(all_20_2, all_30_16, all_30_15) = all_97_0 & % 20.38/3.65 | | | | apply(all_20_2, all_30_16, all_30_15) = all_97_1 & % 20.38/3.65 | | | | apply(all_20_2, all_30_16, all_30_16) = all_97_2 & ( ~ % 20.38/3.65 | | | | (all_97_1 = 0) | ~ (all_97_2 = 0) | all_97_0 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (290) implies: % 20.38/3.65 | | | | (291) apply(all_20_2, all_30_16, all_30_15) = all_97_1 % 20.38/3.65 | | | | (292) apply(all_20_2, all_30_16, all_30_15) = all_97_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (217) with fresh symbols all_99_0, all_99_1, % 20.38/3.65 | | | | all_99_2, all_99_3 gives: % 20.38/3.65 | | | | (293) apply(all_20_2, all_30_16, all_30_17) = all_99_0 & % 20.38/3.65 | | | | apply(all_20_2, all_30_17, all_30_16) = all_99_1 & % 20.38/3.65 | | | | member(all_30_16, all_20_3) = all_99_2 & member(all_30_17, % 20.38/3.65 | | | | all_20_3) = all_99_3 & ( ~ (all_99_2 = 0) | ~ (all_99_3 = 0) % 20.38/3.65 | | | | | (all_99_0 = 0 & all_99_1 = 0)) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (293) implies: % 20.38/3.65 | | | | (294) member(all_30_17, all_20_3) = all_99_3 % 20.38/3.65 | | | | (295) member(all_30_16, all_20_3) = all_99_2 % 20.38/3.65 | | | | (296) apply(all_20_2, all_30_17, all_30_16) = all_99_1 % 20.38/3.65 | | | | (297) apply(all_20_2, all_30_16, all_30_17) = all_99_0 % 20.38/3.65 | | | | (298) ~ (all_99_2 = 0) | ~ (all_99_3 = 0) | (all_99_0 = 0 & % 20.38/3.65 | | | | all_99_1 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (219) with fresh symbols all_101_0, all_101_1, % 20.38/3.65 | | | | all_101_2, all_101_3 gives: % 20.38/3.65 | | | | (299) apply(all_20_2, all_30_15, all_30_16) = all_101_0 & % 20.38/3.65 | | | | apply(all_20_2, all_30_16, all_30_15) = all_101_1 & % 20.38/3.65 | | | | member(all_30_15, all_20_3) = all_101_2 & member(all_30_16, % 20.38/3.65 | | | | all_20_3) = all_101_3 & ( ~ (all_101_2 = 0) | ~ (all_101_3 = % 20.38/3.65 | | | | 0) | (all_101_0 = 0 & all_101_1 = 0)) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (299) implies: % 20.38/3.65 | | | | (300) member(all_30_16, all_20_3) = all_101_3 % 20.38/3.65 | | | | (301) member(all_30_15, all_20_3) = all_101_2 % 20.38/3.65 | | | | (302) apply(all_20_2, all_30_16, all_30_15) = all_101_1 % 20.38/3.65 | | | | (303) apply(all_20_2, all_30_15, all_30_16) = all_101_0 % 20.38/3.65 | | | | (304) ~ (all_101_2 = 0) | ~ (all_101_3 = 0) | (all_101_0 = 0 & % 20.38/3.65 | | | | all_101_1 = 0) % 20.38/3.65 | | | | % 20.38/3.65 | | | | DELTA: instantiating (218) with fresh symbols all_103_0, all_103_1, % 20.38/3.65 | | | | all_103_2, all_103_3 gives: % 20.38/3.65 | | | | (305) apply(all_20_2, all_30_15, all_30_17) = all_103_0 & % 20.38/3.65 | | | | apply(all_20_2, all_30_17, all_30_15) = all_103_1 & % 20.38/3.65 | | | | member(all_30_15, all_20_3) = all_103_2 & member(all_30_17, % 20.38/3.65 | | | | all_20_3) = all_103_3 & ( ~ (all_103_2 = 0) | ~ (all_103_3 = % 20.38/3.65 | | | | 0) | (( ~ (all_103_0 = 0) | ~ (all_103_1 = 0) | all_30_9 = % 20.38/3.65 | | | | 0) & ( ~ (all_30_9 = 0) | (all_103_0 = 0 & all_103_1 = % 20.38/3.65 | | | | 0)))) % 20.38/3.65 | | | | % 20.38/3.65 | | | | ALPHA: (305) implies: % 20.38/3.65 | | | | (306) member(all_30_17, all_20_3) = all_103_3 % 20.38/3.65 | | | | (307) member(all_30_15, all_20_3) = all_103_2 % 20.38/3.65 | | | | (308) apply(all_20_2, all_30_17, all_30_15) = all_103_1 % 20.38/3.65 | | | | (309) apply(all_20_2, all_30_15, all_30_17) = all_103_0 % 20.38/3.65 | | | | (310) ~ (all_103_2 = 0) | ~ (all_103_3 = 0) | (( ~ (all_103_0 = 0) % 20.38/3.65 | | | | | ~ (all_103_1 = 0) | all_30_9 = 0) & ( ~ (all_30_9 = 0) | % 20.38/3.65 | | | | (all_103_0 = 0 & all_103_1 = 0))) % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with 0, all_103_3, all_20_3, all_30_17, % 20.38/3.65 | | | | simplifying with (188), (306) gives: % 20.38/3.65 | | | | (311) all_103_3 = 0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with all_99_3, all_103_3, all_20_3, % 20.38/3.65 | | | | all_30_17, simplifying with (294), (306) gives: % 20.38/3.65 | | | | (312) all_103_3 = all_99_3 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with 0, all_101_3, all_20_3, all_30_16, % 20.38/3.65 | | | | simplifying with (189), (300) gives: % 20.38/3.65 | | | | (313) all_101_3 = 0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with all_99_2, all_101_3, all_20_3, % 20.38/3.65 | | | | all_30_16, simplifying with (295), (300) gives: % 20.38/3.65 | | | | (314) all_101_3 = all_99_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with 0, all_103_2, all_20_3, all_30_15, % 20.38/3.65 | | | | simplifying with (190), (307) gives: % 20.38/3.65 | | | | (315) all_103_2 = 0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (4) with all_101_2, all_103_2, all_20_3, % 20.38/3.65 | | | | all_30_15, simplifying with (301), (307) gives: % 20.38/3.65 | | | | (316) all_103_2 = all_101_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_53_0, all_75_1, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (231), (254) gives: % 20.38/3.65 | | | | (317) all_75_1 = all_53_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_53_1, all_85_2, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (230), (272) gives: % 20.38/3.65 | | | | (318) all_85_2 = all_53_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_49_0, all_85_2, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (225), (272) gives: % 20.38/3.65 | | | | (319) all_85_2 = all_49_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_85_2, all_93_0, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (272), (284) gives: % 20.38/3.65 | | | | (320) all_93_0 = all_85_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_53_0, all_93_0, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (231), (284) gives: % 20.38/3.65 | | | | (321) all_93_0 = all_53_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_51_2, all_93_0, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (227), (284) gives: % 20.38/3.65 | | | | (322) all_93_0 = all_51_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_89_1, all_99_1, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (280), (296) gives: % 20.38/3.65 | | | | (323) all_99_1 = all_89_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_75_1, all_99_1, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (254), (296) gives: % 20.38/3.65 | | | | (324) all_99_1 = all_75_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_49_2, all_99_1, all_30_16, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (224), (296) gives: % 20.38/3.65 | | | | (325) all_99_1 = all_49_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_85_0, all_93_2, all_30_15, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (273), (285) gives: % 20.38/3.65 | | | | (326) all_93_2 = all_85_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_93_2, all_103_1, all_30_15, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (285), (308) gives: % 20.38/3.65 | | | | (327) all_103_1 = all_93_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_59_2, all_103_1, all_30_15, % 20.38/3.65 | | | | all_30_17, all_20_2, simplifying with (239), (308) gives: % 20.38/3.65 | | | | (328) all_103_1 = all_59_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_73_1, all_73_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (251), (252) gives: % 20.38/3.65 | | | | (329) all_73_0 = all_73_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_65_2, all_73_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (246), (252) gives: % 20.38/3.65 | | | | (330) all_73_0 = all_65_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_73_1, all_79_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (251), (262) gives: % 20.38/3.65 | | | | (331) all_79_0 = all_73_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_51_1, all_79_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (228), (262) gives: % 20.38/3.65 | | | | (332) all_79_0 = all_51_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_77_1, all_81_2, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (257), (266) gives: % 20.38/3.65 | | | | (333) all_81_2 = all_77_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_73_1, all_81_2, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (251), (266) gives: % 20.38/3.65 | | | | (334) all_81_2 = all_73_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_65_0, all_81_2, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (247), (266) gives: % 20.38/3.65 | | | | (335) all_81_2 = all_65_0 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_81_2, all_99_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (266), (297) gives: % 20.38/3.65 | | | | (336) all_99_0 = all_81_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_75_2, all_99_0, all_30_17, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (255), (297) gives: % 20.38/3.65 | | | | (337) all_99_0 = all_75_2 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_61_1, all_79_2, all_30_15, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (241), (263) gives: % 20.38/3.65 | | | | (338) all_79_2 = all_61_1 % 20.38/3.65 | | | | % 20.38/3.65 | | | | GROUND_INST: instantiating (5) with all_79_2, all_85_1, all_30_15, % 20.38/3.65 | | | | all_30_16, all_20_2, simplifying with (263), (274) gives: % 20.38/3.65 | | | | (339) all_85_1 = all_79_2 % 20.38/3.65 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_85_1, all_95_2, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (274), (288) gives: % 20.38/3.66 | | | | (340) all_95_2 = all_85_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_95_2, all_97_1, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (288), (291) gives: % 20.38/3.66 | | | | (341) all_97_1 = all_95_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_45_0, all_97_1, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (222), (291) gives: % 20.38/3.66 | | | | (342) all_97_1 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_81_0, all_97_0, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (267), (292) gives: % 20.38/3.66 | | | | (343) all_97_0 = all_81_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_61_1, all_97_0, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (241), (292) gives: % 20.38/3.66 | | | | (344) all_97_0 = all_61_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_97_0, all_101_1, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (292), (302) gives: % 20.38/3.66 | | | | (345) all_101_1 = all_97_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_45_2, all_101_1, all_30_15, % 20.38/3.66 | | | | all_30_16, all_20_2, simplifying with (221), (302) gives: % 20.38/3.66 | | | | (346) all_101_1 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_55_2, all_63_2, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (233), (244) gives: % 20.38/3.66 | | | | (347) all_63_2 = all_55_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_63_2, all_67_1, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (244), (249) gives: % 20.38/3.66 | | | | (348) all_67_1 = all_63_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_55_0, all_83_1, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (234), (269) gives: % 20.38/3.66 | | | | (349) all_83_1 = all_55_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_83_0, all_89_2, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (270), (281) gives: % 20.38/3.66 | | | | (350) all_89_2 = all_83_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_83_1, all_89_2, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (269), (281) gives: % 20.38/3.66 | | | | (351) all_89_2 = all_83_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_79_1, all_89_2, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (264), (281) gives: % 20.38/3.66 | | | | (352) all_89_2 = all_79_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_89_2, all_103_0, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (281), (309) gives: % 20.38/3.66 | | | | (353) all_103_0 = all_89_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_77_0, all_103_0, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (258), (309) gives: % 20.38/3.66 | | | | (354) all_103_0 = all_77_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_67_1, all_103_0, all_30_17, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (249), (309) gives: % 20.38/3.66 | | | | (355) all_103_0 = all_67_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_77_2, all_87_2, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (259), (277) gives: % 20.38/3.66 | | | | (356) all_87_2 = all_77_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_61_2, all_87_2, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (242), (277) gives: % 20.38/3.66 | | | | (357) all_87_2 = all_61_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_87_0, all_93_1, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (278), (286) gives: % 20.38/3.66 | | | | (358) all_93_1 = all_87_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_77_2, all_93_1, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (259), (286) gives: % 20.38/3.66 | | | | (359) all_93_1 = all_77_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_89_0, all_95_1, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (282), (289) gives: % 20.38/3.66 | | | | (360) all_95_1 = all_89_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_77_2, all_95_1, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (259), (289) gives: % 20.38/3.66 | | | | (361) all_95_1 = all_77_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_57_0, all_95_1, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (237), (289) gives: % 20.38/3.66 | | | | (362) all_95_1 = all_57_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_93_1, all_101_0, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (286), (303) gives: % 20.38/3.66 | | | | (363) all_101_0 = all_93_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | GROUND_INST: instantiating (5) with all_57_1, all_101_0, all_30_16, % 20.38/3.66 | | | | all_30_15, all_20_2, simplifying with (236), (303) gives: % 20.38/3.66 | | | | (364) all_101_0 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (354), (355) imply: % 20.38/3.66 | | | | (365) all_77_0 = all_67_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (353), (354) imply: % 20.38/3.66 | | | | (366) all_89_2 = all_77_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (366) implies: % 20.38/3.66 | | | | (367) all_89_2 = all_77_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (327), (328) imply: % 20.38/3.66 | | | | (368) all_93_2 = all_59_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (368) implies: % 20.38/3.66 | | | | (369) all_93_2 = all_59_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (315), (316) imply: % 20.38/3.66 | | | | (370) all_101_2 = 0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (370) implies: % 20.38/3.66 | | | | (371) all_101_2 = 0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (311), (312) imply: % 20.38/3.66 | | | | (372) all_99_3 = 0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (372) implies: % 20.38/3.66 | | | | (373) all_99_3 = 0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (363), (364) imply: % 20.38/3.66 | | | | (374) all_93_1 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (374) implies: % 20.38/3.66 | | | | (375) all_93_1 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (345), (346) imply: % 20.38/3.66 | | | | (376) all_97_0 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (376) implies: % 20.38/3.66 | | | | (377) all_97_0 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (313), (314) imply: % 20.38/3.66 | | | | (378) all_99_2 = 0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (336), (337) imply: % 20.38/3.66 | | | | (379) all_81_2 = all_75_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (379) implies: % 20.38/3.66 | | | | (380) all_81_2 = all_75_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (323), (325) imply: % 20.38/3.66 | | | | (381) all_89_1 = all_49_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (323), (324) imply: % 20.38/3.66 | | | | (382) all_89_1 = all_75_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (343), (377) imply: % 20.38/3.66 | | | | (383) all_81_0 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (343), (344) imply: % 20.38/3.66 | | | | (384) all_81_0 = all_61_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (341), (342) imply: % 20.38/3.66 | | | | (385) all_95_2 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (385) implies: % 20.38/3.66 | | | | (386) all_95_2 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (360), (361) imply: % 20.38/3.66 | | | | (387) all_89_0 = all_77_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (360), (362) imply: % 20.38/3.66 | | | | (388) all_89_0 = all_57_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (340), (386) imply: % 20.38/3.66 | | | | (389) all_85_1 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (389) implies: % 20.38/3.66 | | | | (390) all_85_1 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (320), (322) imply: % 20.38/3.66 | | | | (391) all_85_2 = all_51_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (391) implies: % 20.38/3.66 | | | | (392) all_85_2 = all_51_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (321), (322) imply: % 20.38/3.66 | | | | (393) all_53_0 = all_51_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (393) implies: % 20.38/3.66 | | | | (394) all_53_0 = all_51_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (358), (375) imply: % 20.38/3.66 | | | | (395) all_87_0 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (358), (359) imply: % 20.38/3.66 | | | | (396) all_87_0 = all_77_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (326), (369) imply: % 20.38/3.66 | | | | (397) all_85_0 = all_59_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (387), (388) imply: % 20.38/3.66 | | | | (398) all_77_2 = all_57_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (398) implies: % 20.38/3.66 | | | | (399) all_77_2 = all_57_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (381), (382) imply: % 20.38/3.66 | | | | (400) all_75_1 = all_49_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (400) implies: % 20.38/3.66 | | | | (401) all_75_1 = all_49_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (350), (352) imply: % 20.38/3.66 | | | | (402) all_83_0 = all_79_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (350), (351) imply: % 20.38/3.66 | | | | (403) all_83_0 = all_83_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (350), (367) imply: % 20.38/3.66 | | | | (404) all_83_0 = all_77_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (395), (396) imply: % 20.38/3.66 | | | | (405) all_77_2 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (405) implies: % 20.38/3.66 | | | | (406) all_77_2 = all_57_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (356), (357) imply: % 20.38/3.66 | | | | (407) all_77_2 = all_61_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (407) implies: % 20.38/3.66 | | | | (408) all_77_2 = all_61_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (339), (390) imply: % 20.38/3.66 | | | | (409) all_79_2 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (409) implies: % 20.38/3.66 | | | | (410) all_79_2 = all_45_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (318), (319) imply: % 20.38/3.66 | | | | (411) all_53_1 = all_49_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (318), (392) imply: % 20.38/3.66 | | | | (412) all_53_1 = all_51_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (402), (403) imply: % 20.38/3.66 | | | | (413) all_83_1 = all_79_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (413) implies: % 20.38/3.66 | | | | (414) all_83_1 = all_79_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (402), (404) imply: % 20.38/3.66 | | | | (415) all_79_1 = all_77_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (349), (414) imply: % 20.38/3.66 | | | | (416) all_79_1 = all_55_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (416) implies: % 20.38/3.66 | | | | (417) all_79_1 = all_55_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (383), (384) imply: % 20.38/3.66 | | | | (418) all_61_1 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (418) implies: % 20.38/3.66 | | | | (419) all_61_1 = all_45_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (333), (335) imply: % 20.38/3.66 | | | | (420) all_77_1 = all_65_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (333), (334) imply: % 20.38/3.66 | | | | (421) all_77_1 = all_73_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (333), (380) imply: % 20.38/3.66 | | | | (422) all_77_1 = all_75_2 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (331), (332) imply: % 20.38/3.66 | | | | (423) all_73_1 = all_51_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (423) implies: % 20.38/3.66 | | | | (424) all_73_1 = all_51_1 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (415), (417) imply: % 20.38/3.66 | | | | (425) all_77_0 = all_55_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | SIMP: (425) implies: % 20.38/3.66 | | | | (426) all_77_0 = all_55_0 % 20.38/3.66 | | | | % 20.38/3.66 | | | | COMBINE_EQS: (338), (410) imply: % 20.38/3.67 | | | | (427) all_61_1 = all_45_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (427) implies: % 20.38/3.67 | | | | (428) all_61_1 = all_45_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (365), (426) imply: % 20.38/3.67 | | | | (429) all_67_1 = all_55_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (429) implies: % 20.38/3.67 | | | | (430) all_67_1 = all_55_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (420), (422) imply: % 20.38/3.67 | | | | (431) all_75_2 = all_65_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (421), (422) imply: % 20.38/3.67 | | | | (432) all_75_2 = all_73_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (406), (408) imply: % 20.38/3.67 | | | | (433) all_61_2 = all_57_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (399), (408) imply: % 20.38/3.67 | | | | (434) all_61_2 = all_57_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (317), (401) imply: % 20.38/3.67 | | | | (435) all_53_0 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (435) implies: % 20.38/3.67 | | | | (436) all_53_0 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (431), (432) imply: % 20.38/3.67 | | | | (437) all_73_1 = all_65_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (437) implies: % 20.38/3.67 | | | | (438) all_73_1 = all_65_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (329), (330) imply: % 20.38/3.67 | | | | (439) all_73_1 = all_65_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (439) implies: % 20.38/3.67 | | | | (440) all_73_1 = all_65_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (438), (440) imply: % 20.38/3.67 | | | | (441) all_65_0 = all_65_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (424), (438) imply: % 20.38/3.67 | | | | (442) all_65_0 = all_51_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (348), (430) imply: % 20.38/3.67 | | | | (443) all_63_2 = all_55_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (443) implies: % 20.38/3.67 | | | | (444) all_63_2 = all_55_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (441), (442) imply: % 20.38/3.67 | | | | (445) all_65_2 = all_51_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (347), (444) imply: % 20.38/3.67 | | | | (446) all_55_0 = all_55_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (419), (428) imply: % 20.38/3.67 | | | | (447) all_45_0 = all_45_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (433), (434) imply: % 20.38/3.67 | | | | (448) all_57_0 = all_57_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (394), (436) imply: % 20.38/3.67 | | | | (449) all_51_2 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (449) implies: % 20.38/3.67 | | | | (450) all_51_2 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (411), (412) imply: % 20.38/3.67 | | | | (451) all_51_2 = all_49_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | SIMP: (451) implies: % 20.38/3.67 | | | | (452) all_51_2 = all_49_0 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (450), (452) imply: % 20.38/3.67 | | | | (453) all_49_0 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (411), (453) imply: % 20.38/3.67 | | | | (454) all_53_1 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (431), (442) imply: % 20.38/3.67 | | | | (455) all_75_2 = all_51_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (422), (455) imply: % 20.38/3.67 | | | | (456) all_77_1 = all_51_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (426), (446) imply: % 20.38/3.67 | | | | (457) all_77_0 = all_55_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (318), (454) imply: % 20.38/3.67 | | | | (458) all_85_2 = all_49_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (390), (447) imply: % 20.38/3.67 | | | | (459) all_85_1 = all_45_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (337), (455) imply: % 20.38/3.67 | | | | (460) all_99_0 = all_51_1 % 20.38/3.67 | | | | % 20.38/3.67 | | | | COMBINE_EQS: (354), (457) imply: % 20.38/3.67 | | | | (461) all_103_0 = all_55_2 % 20.38/3.67 | | | | % 20.38/3.67 | | | | BETA: splitting (304) gives: % 20.38/3.67 | | | | % 20.38/3.67 | | | | Case 1: % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | (462) ~ (all_101_2 = 0) % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | REDUCE: (371), (462) imply: % 20.38/3.67 | | | | | (463) $false % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | CLOSE: (463) is inconsistent. % 20.38/3.67 | | | | | % 20.38/3.67 | | | | Case 2: % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | (464) ~ (all_101_3 = 0) | (all_101_0 = 0 & all_101_1 = 0) % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | BETA: splitting (464) gives: % 20.38/3.67 | | | | | % 20.38/3.67 | | | | | Case 1: % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | (465) ~ (all_101_3 = 0) % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | REDUCE: (313), (465) imply: % 20.38/3.67 | | | | | | (466) $false % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | CLOSE: (466) is inconsistent. % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | Case 2: % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | (467) all_101_0 = 0 & all_101_1 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | ALPHA: (467) implies: % 20.38/3.67 | | | | | | (468) all_101_1 = 0 % 20.38/3.67 | | | | | | (469) all_101_0 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | COMBINE_EQS: (364), (469) imply: % 20.38/3.67 | | | | | | (470) all_57_1 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | COMBINE_EQS: (346), (468) imply: % 20.38/3.67 | | | | | | (471) all_45_2 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | SIMP: (471) implies: % 20.38/3.67 | | | | | | (472) all_45_2 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | COMBINE_EQS: (406), (470) imply: % 20.38/3.67 | | | | | | (473) all_77_2 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | COMBINE_EQS: (459), (472) imply: % 20.38/3.67 | | | | | | (474) all_85_1 = 0 % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | BETA: splitting (298) gives: % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | | Case 1: % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | (475) ~ (all_99_2 = 0) % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | REDUCE: (378), (475) imply: % 20.38/3.67 | | | | | | | (476) $false % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | CLOSE: (476) is inconsistent. % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | Case 2: % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | (477) ~ (all_99_3 = 0) | (all_99_0 = 0 & all_99_1 = 0) % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | BETA: splitting (477) gives: % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | (478) ~ (all_99_3 = 0) % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | REDUCE: (373), (478) imply: % 20.38/3.67 | | | | | | | | (479) $false % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | CLOSE: (479) is inconsistent. % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | (480) all_99_0 = 0 & all_99_1 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | ALPHA: (480) implies: % 20.38/3.67 | | | | | | | | (481) all_99_1 = 0 % 20.38/3.67 | | | | | | | | (482) all_99_0 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | COMBINE_EQS: (460), (482) imply: % 20.38/3.67 | | | | | | | | (483) all_51_1 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | COMBINE_EQS: (325), (481) imply: % 20.38/3.67 | | | | | | | | (484) all_49_2 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | COMBINE_EQS: (456), (483) imply: % 20.38/3.67 | | | | | | | | (485) all_77_1 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | COMBINE_EQS: (458), (484) imply: % 20.38/3.67 | | | | | | | | (486) all_85_2 = 0 % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | BETA: splitting (260) gives: % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | (487) ~ (all_77_1 = 0) % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | REDUCE: (485), (487) imply: % 20.38/3.67 | | | | | | | | | (488) $false % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | CLOSE: (488) is inconsistent. % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | (489) ~ (all_77_2 = 0) | all_77_0 = 0 % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | BETA: splitting (489) gives: % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | (490) ~ (all_77_2 = 0) % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | REDUCE: (473), (490) imply: % 20.38/3.67 | | | | | | | | | | (491) $false % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | CLOSE: (491) is inconsistent. % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | (492) all_77_0 = 0 % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | COMBINE_EQS: (457), (492) imply: % 20.38/3.67 | | | | | | | | | | (493) all_55_2 = 0 % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | COMBINE_EQS: (461), (493) imply: % 20.38/3.67 | | | | | | | | | | (494) all_103_0 = 0 % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | BETA: splitting (275) gives: % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | (495) ~ (all_85_1 = 0) % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | REDUCE: (474), (495) imply: % 20.38/3.67 | | | | | | | | | | | (496) $false % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | CLOSE: (496) is inconsistent. % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | (497) ~ (all_85_2 = 0) | all_85_0 = 0 % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | BETA: splitting (497) gives: % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | (498) ~ (all_85_2 = 0) % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | REDUCE: (486), (498) imply: % 20.38/3.67 | | | | | | | | | | | | (499) $false % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | CLOSE: (499) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | (500) all_85_0 = 0 % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | COMBINE_EQS: (397), (500) imply: % 20.38/3.67 | | | | | | | | | | | | (501) all_59_2 = 0 % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | SIMP: (501) implies: % 20.38/3.67 | | | | | | | | | | | | (502) all_59_2 = 0 % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | COMBINE_EQS: (328), (502) imply: % 20.38/3.67 | | | | | | | | | | | | (503) all_103_1 = 0 % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | BETA: splitting (310) gives: % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | (504) ~ (all_103_2 = 0) % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | REDUCE: (315), (504) imply: % 20.38/3.67 | | | | | | | | | | | | | (505) $false % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | CLOSE: (505) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | (506) ~ (all_103_3 = 0) | (( ~ (all_103_0 = 0) | ~ % 20.38/3.67 | | | | | | | | | | | | | (all_103_1 = 0) | all_30_9 = 0) & ( ~ % 20.38/3.67 | | | | | | | | | | | | | (all_30_9 = 0) | (all_103_0 = 0 & all_103_1 = % 20.38/3.67 | | | | | | | | | | | | | 0))) % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | BETA: splitting (506) gives: % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | (507) ~ (all_103_3 = 0) % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | REDUCE: (311), (507) imply: % 20.38/3.67 | | | | | | | | | | | | | | (508) $false % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | CLOSE: (508) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | (509) ( ~ (all_103_0 = 0) | ~ (all_103_1 = 0) | % 20.38/3.67 | | | | | | | | | | | | | | all_30_9 = 0) & ( ~ (all_30_9 = 0) | (all_103_0 % 20.38/3.67 | | | | | | | | | | | | | | = 0 & all_103_1 = 0)) % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | ALPHA: (509) implies: % 20.38/3.67 | | | | | | | | | | | | | | (510) ~ (all_103_0 = 0) | ~ (all_103_1 = 0) | all_30_9 % 20.38/3.67 | | | | | | | | | | | | | | = 0 % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | BETA: splitting (510) gives: % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | (511) ~ (all_103_0 = 0) % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | REDUCE: (494), (511) imply: % 20.38/3.67 | | | | | | | | | | | | | | | (512) $false % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | CLOSE: (512) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | (513) ~ (all_103_1 = 0) | all_30_9 = 0 % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | BETA: splitting (513) gives: % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | Case 1: % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | (514) ~ (all_103_1 = 0) % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | REDUCE: (503), (514) imply: % 20.38/3.67 | | | | | | | | | | | | | | | | (515) $false % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | CLOSE: (515) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | Case 2: % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | (516) all_30_9 = 0 % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | REDUCE: (187), (516) imply: % 20.38/3.67 | | | | | | | | | | | | | | | | (517) $false % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | | CLOSE: (517) is inconsistent. % 20.38/3.67 | | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | | % 20.38/3.67 | | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | | % 20.38/3.67 | | | | | | | | | End of split % 20.38/3.67 | | | | | | | | | % 20.38/3.67 | | | | | | | | End of split % 20.38/3.67 | | | | | | | | % 20.38/3.67 | | | | | | | End of split % 20.38/3.67 | | | | | | | % 20.38/3.67 | | | | | | End of split % 20.38/3.67 | | | | | | % 20.38/3.67 | | | | | End of split % 20.38/3.67 | | | | | % 20.38/3.67 | | | | End of split % 20.38/3.67 | | | | % 20.38/3.68 | | | End of split % 20.38/3.68 | | | % 20.38/3.68 | | End of split % 20.38/3.68 | | % 20.38/3.68 | End of split % 20.38/3.68 | % 20.38/3.68 End of proof % 20.38/3.68 % SZS output end Proof for theBenchmark % 20.38/3.68 % 20.38/3.68 3074ms %------------------------------------------------------------------------------