%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : DAT040_1 : TPTP v8.1.2. Released v5.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.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 : Wed Aug 30 22:18:59 EDT 2023 % Result : Theorem 11.28s 2.19s % Output : Proof 18.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : DAT040_1 : TPTP v8.1.2. Released v5.0.0. % 0.03/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Aug 24 14:54:57 EDT 2023 % 0.14/0.34 % CPUTime : % 0.53/0.61 ________ _____ % 0.53/0.61 ___ __ \_________(_)________________________________ % 0.53/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.53/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.53/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.53/0.61 % 0.53/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.53/0.61 (2023-06-19) % 0.53/0.61 % 0.53/0.61 (c) Philipp Rümmer, 2009-2023 % 0.53/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.53/0.61 Amanda Stjerna. % 0.53/0.61 Free software under BSD-3-Clause. % 0.53/0.61 % 0.53/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.53/0.61 % 0.53/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.53/0.63 Running up to 7 provers in parallel. % 0.74/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.74/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.74/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.74/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.74/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.74/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.74/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.73/1.05 Prover 1: Preprocessing ... % 2.73/1.05 Prover 4: Preprocessing ... % 2.99/1.09 Prover 6: Preprocessing ... % 2.99/1.09 Prover 3: Preprocessing ... % 2.99/1.09 Prover 0: Preprocessing ... % 2.99/1.09 Prover 2: Preprocessing ... % 2.99/1.09 Prover 5: Preprocessing ... % 4.87/1.32 Prover 5: Proving ... % 4.87/1.33 Prover 6: Constructing countermodel ... % 4.87/1.33 Prover 3: Constructing countermodel ... % 4.87/1.33 Prover 1: Constructing countermodel ... % 5.18/1.37 Prover 4: Constructing countermodel ... % 5.18/1.41 Prover 2: Proving ... % 5.18/1.41 Prover 0: Proving ... % 5.78/1.44 Prover 3: gave up % 5.78/1.44 Prover 1: gave up % 5.78/1.44 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 5.78/1.44 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 5.78/1.44 Prover 6: gave up % 5.78/1.44 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 6.07/1.48 Prover 7: Preprocessing ... % 6.07/1.48 Prover 9: Preprocessing ... % 6.07/1.49 Prover 8: Preprocessing ... % 6.70/1.57 Prover 8: Warning: ignoring some quantifiers % 6.70/1.58 Prover 7: Constructing countermodel ... % 6.70/1.58 Prover 8: Constructing countermodel ... % 6.70/1.61 Prover 7: gave up % 6.70/1.61 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 7.25/1.64 Prover 10: Preprocessing ... % 7.25/1.66 Prover 9: Constructing countermodel ... % 7.56/1.68 Prover 8: gave up % 7.56/1.69 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 7.56/1.71 Prover 11: Preprocessing ... % 7.56/1.73 Prover 10: Constructing countermodel ... % 8.17/1.75 Prover 10: gave up % 8.17/1.75 Prover 12: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=2024365391 % 8.37/1.80 Prover 12: Preprocessing ... % 8.37/1.82 Prover 11: Constructing countermodel ... % 8.87/1.91 Prover 12: Proving ... % 11.28/2.19 Prover 0: proved (1556ms) % 11.28/2.19 % 11.28/2.19 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.28/2.19 % 11.28/2.19 Prover 9: stopped % 11.28/2.19 Prover 2: stopped % 11.28/2.21 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 11.28/2.21 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 11.28/2.21 Prover 12: stopped % 11.28/2.21 Prover 5: stopped % 11.28/2.21 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 11.28/2.21 Prover 13: Preprocessing ... % 11.28/2.21 Prover 16: Preprocessing ... % 11.28/2.22 Prover 19: Preprocessing ... % 11.87/2.25 Prover 16: Warning: ignoring some quantifiers % 11.87/2.26 Prover 16: Constructing countermodel ... % 11.87/2.27 Prover 13: Warning: ignoring some quantifiers % 11.87/2.27 Prover 13: Constructing countermodel ... % 11.87/2.28 Prover 19: Warning: ignoring some quantifiers % 12.27/2.28 Prover 19: Constructing countermodel ... % 12.92/2.37 Prover 19: gave up % 12.92/2.37 Prover 13: gave up % 13.49/2.51 Prover 16: gave up % 16.90/3.09 Prover 11: Found proof (size 391) % 16.90/3.09 Prover 11: proved (1406ms) % 16.90/3.09 Prover 4: stopped % 16.90/3.09 % 16.90/3.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.90/3.09 % 17.49/3.21 % SZS output start Proof for theBenchmark % 17.49/3.21 Assumptions after simplification: % 17.49/3.21 --------------------------------- % 17.49/3.21 % 17.49/3.21 (ax1) % 17.49/3.23 collection(empty) & ! [v0: collection] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) % 17.49/3.23 | ~ (count(v0) = v1) | ~ collection(v0)) & ! [v0: int] : ~ (in(v0, % 17.49/3.23 empty) = 0) % 17.49/3.23 % 17.49/3.23 (ax2) % 17.49/3.23 collection(empty) & ! [v0: int] : ! [v1: collection] : ! [v2: collection] : % 17.49/3.23 ( ~ (add(v0, v1) = v2) | ~ collection(v1) | in(v0, v2) = 0) & ! [v0: % 17.49/3.23 collection] : (v0 = empty | ~ (count(v0) = 0) | ~ collection(v0)) & ! % 17.49/3.23 [v0: int] : (v0 = 0 | ~ (count(empty) = v0)) % 17.49/3.23 % 17.49/3.23 (ax3) % 17.75/3.24 ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | ~ (in(v0, v1) = % 17.75/3.24 v2) | ~ collection(v1) | ? [v3: collection] : ? [v4: int] : (add(v0, % 17.75/3.24 v1) = v3 & count(v3) = v4 & count(v1) = $sum(v4, -1) & collection(v3))) % 17.75/3.24 & ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, % 17.75/3.24 v1) = v2) | ~ collection(v1) | ? [v3: int] : ( ~ (v3 = 0) & in(v0, v2) % 17.75/3.24 = v3)) & ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 17.75/3.24 (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 17.75/3.24 [v5: int] : (($difference(v5, v4) = -1 & count(v2) = v4 & count(v1) = % 17.75/3.24 $sum(v4, -1)) | (v3 = 0 & in(v0, v1) = 0))) & ! [v0: int] : ! [v1: % 17.75/3.24 collection] : ! [v2: collection] : ( ~ (add(v0, v1) = v2) | ~ % 17.75/3.24 collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: int] : (( ~ (v5 = 0) % 17.75/3.24 & in(v0, v1) = v5) | ( ~ ($difference(v4, v3) = -1) & count(v2) = v3 & % 17.75/3.24 count(v1) = v4))) & ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) % 17.75/3.24 = 0) | ~ collection(v1) | ? [v2: collection] : ? [v3: int] : ? [v4: % 17.75/3.24 int] : ( ~ ($difference(v4, v3) = -1) & add(v0, v1) = v2 & count(v2) = v3 % 17.75/3.24 & count(v1) = v4 & collection(v2))) % 17.75/3.24 % 17.75/3.24 (ax4) % 17.75/3.25 ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ! % 17.75/3.25 [v4: int] : (v4 = 0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = v4) | ~ % 17.75/3.25 collection(v1) | ? [v5: int] : ( ~ (v5 = 0) & in(v0, v1) = v5)) & ! [v0: % 17.75/3.25 int] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] : (v3 = 0 | % 17.75/3.25 ~ (add(v0, v1) = v2) | ~ (in(v0, v2) = v3) | ~ collection(v1)) & ! [v0: % 17.75/3.25 int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : (v2 = v0 | % 17.75/3.25 ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ collection(v1) | in(v0, v1) % 17.75/3.25 = 0) & ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | ~ % 17.75/3.25 (in(v0, v1) = v2) | ~ collection(v1) | ? [v3: collection] : ? [v4: int] : % 17.75/3.25 ? [v5: int] : ( ~ (v5 = v4) & add(v0, v1) = v3 & count(v3) = v4 & count(v1) % 17.75/3.25 = v5 & collection(v3))) & ! [v0: int] : ! [v1: collection] : ! [v2: % 17.75/3.25 collection] : ( ~ (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ? % 17.75/3.25 [v4: int] : ? [v5: int] : ((v5 = v4 & count(v2) = v4 & count(v1) = v4) | ( % 17.75/3.25 ~ (v3 = 0) & in(v0, v1) = v3))) & ! [v0: int] : ! [v1: collection] : % 17.75/3.25 ! [v2: collection] : ( ~ (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] % 17.75/3.25 : ? [v4: int] : ? [v5: int] : ((v5 = 0 & in(v0, v1) = 0) | ( ~ (v4 = v3) & % 17.75/3.25 count(v2) = v3 & count(v1) = v4))) & ! [v0: int] : ! [v1: collection] % 17.75/3.25 : ( ~ (in(v0, v1) = 0) | ~ collection(v1) | ? [v2: collection] : ? [v3: % 17.75/3.25 int] : (add(v0, v1) = v2 & count(v2) = v3 & count(v1) = v3 & % 17.75/3.25 collection(v2))) % 17.75/3.25 % 17.75/3.25 (ax5) % 17.75/3.26 ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ! % 17.75/3.26 [v4: int] : (v4 = 0 | v2 = v0 | ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = % 17.75/3.26 v4) | ~ collection(v1) | ? [v5: int] : ( ~ (v5 = 0) & in(v0, v1) = v5)) % 17.75/3.26 & ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ( % 17.75/3.26 ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ collection(v1) | in(v0, % 17.75/3.26 v1) = 0) & ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | % 17.75/3.26 ~ (in(v0, v1) = v2) | ~ collection(v1) | ? [v3: collection] : ? [v4: int] % 17.75/3.26 : ? [v5: int] : ( ~ ($difference(v5, v4) = 1) & remove(v0, v1) = v3 & % 17.75/3.26 count(v3) = v4 & count(v1) = v5 & collection(v3))) & ! [v0: int] : ! % 17.75/3.26 [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) = v2) | ~ % 17.75/3.26 (in(v0, v2) = 0) | ~ collection(v1)) & ! [v0: int] : ! [v1: collection] : % 17.75/3.26 ! [v2: collection] : ( ~ (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: % 17.75/3.26 int] : ? [v4: int] : ? [v5: int] : (($difference(v5, v4) = 1 & count(v2) % 17.75/3.26 = v4 & count(v1) = $sum(v4, 1)) | ( ~ (v3 = 0) & in(v0, v1) = v3))) & ! % 17.75/3.26 [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) = % 17.75/3.26 v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: int] : % 17.75/3.26 ((v5 = 0 & in(v0, v1) = 0) | ( ~ ($difference(v4, v3) = 1) & count(v2) = v3 % 17.75/3.26 & count(v1) = v4))) & ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, % 17.75/3.26 v1) = 0) | ~ collection(v1) | ? [v2: collection] : ? [v3: int] : % 17.75/3.26 (remove(v0, v1) = v2 & count(v2) = v3 & count(v1) = $sum(v3, 1) & % 17.75/3.26 collection(v2))) % 17.75/3.26 % 17.87/3.26 (ax6) % 17.87/3.27 ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | ~ (in(v0, v1) = % 17.87/3.27 v2) | ~ collection(v1) | ? [v3: collection] : ? [v4: int] : (remove(v0, % 17.87/3.27 v1) = v3 & count(v3) = v4 & count(v1) = v4 & collection(v3))) & ! [v0: % 17.87/3.27 int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) = v2) % 17.87/3.27 | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: int] : ((v5 = v4 % 17.87/3.27 & count(v2) = v4 & count(v1) = v4) | (v3 = 0 & in(v0, v1) = 0))) & ! % 17.87/3.27 [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) = % 17.87/3.27 v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: int] : (( % 17.87/3.27 ~ (v5 = 0) & in(v0, v1) = v5) | ( ~ (v4 = v3) & count(v2) = v3 & % 17.87/3.27 count(v1) = v4))) & ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) % 17.87/3.27 = 0) | ~ collection(v1) | ? [v2: collection] : ? [v3: int] : ? [v4: % 17.87/3.27 int] : ( ~ (v4 = v3) & remove(v0, v1) = v2 & count(v2) = v3 & count(v1) = % 17.87/3.27 v4 & collection(v2))) % 17.87/3.27 % 17.87/3.27 (ax7) % 17.87/3.27 ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) % 17.87/3.27 = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: collection] : ((v4 = v1 % 17.87/3.27 & add(v0, v2) = v1) | ( ~ (v3 = 0) & in(v0, v1) = v3))) & ! [v0: int] : % 17.87/3.27 ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ collection(v1) | ? [v2: % 17.87/3.27 collection] : (remove(v0, v1) = v2 & add(v0, v2) = v1 & collection(v2))) % 17.87/3.27 % 17.87/3.27 (co1) % 17.87/3.27 ? [v0: collection] : ? [v1: int] : ? [v2: int] : ($lesseq(7, v2) & % 17.87/3.27 $lesseq(v1, 2) & count(v0) = 2 & in(v2, v0) = 0 & in(v1, v0) = 0 & in(5, v0) % 17.87/3.27 = 0 & collection(v0)) % 17.87/3.27 % 17.87/3.27 (function-axioms) % 17.87/3.28 ! [v0: collection] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] % 17.87/3.28 : (v1 = v0 | ~ (remove(v3, v2) = v1) | ~ (remove(v3, v2) = v0)) & ! [v0: % 17.87/3.28 collection] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] : (v1 % 17.87/3.28 = v0 | ~ (add(v3, v2) = v1) | ~ (add(v3, v2) = v0)) & ! [v0: % 17.87/3.28 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: collection] : ! % 17.87/3.28 [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0: % 17.87/3.28 int] : ! [v1: int] : ! [v2: collection] : (v1 = v0 | ~ (count(v2) = v1) | % 17.87/3.28 ~ (count(v2) = v0)) % 17.87/3.28 % 17.87/3.28 Those formulas are unsatisfiable: % 17.87/3.28 --------------------------------- % 17.87/3.28 % 17.87/3.28 Begin of proof % 17.87/3.28 | % 17.87/3.28 | ALPHA: (ax1) implies: % 17.87/3.28 | (1) ! [v0: int] : ~ (in(v0, empty) = 0) % 17.87/3.28 | % 17.87/3.28 | ALPHA: (ax2) implies: % 17.87/3.28 | (2) ! [v0: collection] : (v0 = empty | ~ (count(v0) = 0) | ~ % 17.87/3.28 | collection(v0)) % 17.87/3.28 | % 17.87/3.28 | ALPHA: (ax3) implies: % 17.87/3.28 | (3) ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ % 17.87/3.28 | collection(v1) | ? [v2: collection] : ? [v3: int] : ? [v4: int] : % 17.87/3.28 | ( ~ ($difference(v4, v3) = -1) & add(v0, v1) = v2 & count(v2) = v3 & % 17.87/3.28 | count(v1) = v4 & collection(v2))) % 17.87/3.29 | (4) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 17.87/3.29 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 17.87/3.29 | [v5: int] : (( ~ (v5 = 0) & in(v0, v1) = v5) | ( ~ ($difference(v4, % 17.87/3.29 | v3) = -1) & count(v2) = v3 & count(v1) = v4))) % 17.87/3.29 | (5) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 17.87/3.29 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 17.87/3.29 | [v5: int] : (($difference(v5, v4) = -1 & count(v2) = v4 & count(v1) = % 17.87/3.29 | $sum(v4, -1)) | (v3 = 0 & in(v0, v1) = 0))) % 17.87/3.29 | (6) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 17.87/3.29 | (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ( ~ (v3 = % 17.87/3.29 | 0) & in(v0, v2) = v3)) % 17.87/3.29 | % 17.87/3.29 | ALPHA: (ax4) implies: % 17.87/3.29 | (7) ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ % 17.87/3.29 | collection(v1) | ? [v2: collection] : ? [v3: int] : (add(v0, v1) = % 17.87/3.29 | v2 & count(v2) = v3 & count(v1) = v3 & collection(v2))) % 17.87/3.29 | (8) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 17.87/3.29 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 17.87/3.29 | [v5: int] : ((v5 = 0 & in(v0, v1) = 0) | ( ~ (v4 = v3) & count(v2) = % 17.87/3.29 | v3 & count(v1) = v4))) % 17.87/3.29 | (9) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 17.87/3.29 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 17.87/3.29 | [v5: int] : ((v5 = v4 & count(v2) = v4 & count(v1) = v4) | ( ~ (v3 = % 17.87/3.29 | 0) & in(v0, v1) = v3))) % 17.87/3.30 | (10) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: % 17.87/3.30 | collection] : (v2 = v0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = 0) % 17.87/3.30 | | ~ collection(v1) | in(v0, v1) = 0) % 17.87/3.30 | % 17.87/3.30 | ALPHA: (ax5) implies: % 17.87/3.30 | (11) ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ % 17.87/3.30 | collection(v1) | ? [v2: collection] : ? [v3: int] : (remove(v0, % 17.87/3.30 | v1) = v2 & count(v2) = v3 & count(v1) = $sum(v3, 1) & % 17.87/3.30 | collection(v2))) % 17.87/3.30 | (12) ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | ~ % 17.87/3.30 | (in(v0, v1) = v2) | ~ collection(v1) | ? [v3: collection] : ? % 17.87/3.30 | [v4: int] : ? [v5: int] : ( ~ ($difference(v5, v4) = 1) & % 17.87/3.30 | remove(v0, v1) = v3 & count(v3) = v4 & count(v1) = v5 & % 17.87/3.30 | collection(v3))) % 17.87/3.30 | % 17.87/3.30 | ALPHA: (ax6) implies: % 17.87/3.30 | (13) ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ % 17.87/3.30 | collection(v1) | ? [v2: collection] : ? [v3: int] : ? [v4: int] : % 17.87/3.30 | ( ~ (v4 = v3) & remove(v0, v1) = v2 & count(v2) = v3 & count(v1) = % 17.87/3.30 | v4 & collection(v2))) % 17.87/3.30 | (14) ! [v0: int] : ! [v1: collection] : ! [v2: int] : (v2 = 0 | ~ % 17.87/3.30 | (in(v0, v1) = v2) | ~ collection(v1) | ? [v3: collection] : ? % 17.87/3.30 | [v4: int] : (remove(v0, v1) = v3 & count(v3) = v4 & count(v1) = v4 & % 17.87/3.30 | collection(v3))) % 17.87/3.30 | % 17.87/3.30 | ALPHA: (ax7) implies: % 17.87/3.30 | (15) ! [v0: int] : ! [v1: collection] : ( ~ (in(v0, v1) = 0) | ~ % 17.87/3.30 | collection(v1) | ? [v2: collection] : (remove(v0, v1) = v2 & % 17.87/3.30 | add(v0, v2) = v1 & collection(v2))) % 17.87/3.30 | % 17.87/3.30 | ALPHA: (function-axioms) implies: % 17.87/3.31 | (16) ! [v0: int] : ! [v1: int] : ! [v2: collection] : (v1 = v0 | ~ % 17.87/3.31 | (count(v2) = v1) | ~ (count(v2) = v0)) % 17.87/3.31 | (17) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.87/3.31 | collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 17.87/3.31 | (in(v3, v2) = v0)) % 17.87/3.31 | (18) ! [v0: collection] : ! [v1: collection] : ! [v2: collection] : ! % 17.87/3.31 | [v3: int] : (v1 = v0 | ~ (remove(v3, v2) = v1) | ~ (remove(v3, v2) = % 17.87/3.31 | v0)) % 17.87/3.31 | % 17.87/3.31 | DELTA: instantiating (co1) with fresh symbols all_13_0, all_13_1, all_13_2 % 17.87/3.31 | gives: % 17.87/3.31 | (19) $lesseq(7, all_13_0) & $lesseq(all_13_1, 2) & count(all_13_2) = 2 & % 17.87/3.31 | in(all_13_0, all_13_2) = 0 & in(all_13_1, all_13_2) = 0 & in(5, % 17.87/3.31 | all_13_2) = 0 & collection(all_13_2) % 17.87/3.31 | % 17.87/3.31 | ALPHA: (19) implies: % 17.87/3.31 | (20) $lesseq(all_13_1, 2) % 17.87/3.31 | (21) $lesseq(7, all_13_0) % 17.87/3.31 | (22) collection(all_13_2) % 17.87/3.31 | (23) in(5, all_13_2) = 0 % 17.87/3.31 | (24) in(all_13_1, all_13_2) = 0 % 17.87/3.31 | (25) in(all_13_0, all_13_2) = 0 % 17.87/3.31 | (26) count(all_13_2) = 2 % 17.87/3.31 | % 17.87/3.31 | GROUND_INST: instantiating (3) with 5, all_13_2, simplifying with (22), (23) % 17.87/3.31 | gives: % 17.87/3.31 | (27) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ % 17.87/3.31 | ($difference(v2, v1) = -1) & add(5, all_13_2) = v0 & count(v0) = v1 % 17.87/3.31 | & count(all_13_2) = v2 & collection(v0)) % 17.87/3.31 | % 17.87/3.31 | GROUND_INST: instantiating (13) with 5, all_13_2, simplifying with (22), (23) % 17.87/3.31 | gives: % 17.87/3.31 | (28) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = v1) & % 17.87/3.31 | remove(5, all_13_2) = v0 & count(v0) = v1 & count(all_13_2) = v2 & % 17.87/3.31 | collection(v0)) % 17.87/3.31 | % 17.87/3.31 | GROUND_INST: instantiating (11) with 5, all_13_2, simplifying with (22), (23) % 17.87/3.31 | gives: % 17.87/3.32 | (29) ? [v0: collection] : ? [v1: int] : (remove(5, all_13_2) = v0 & % 17.87/3.32 | count(v0) = v1 & count(all_13_2) = $sum(v1, 1) & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (7) with 5, all_13_2, simplifying with (22), (23) % 17.87/3.32 | gives: % 17.87/3.32 | (30) ? [v0: collection] : ? [v1: int] : (add(5, all_13_2) = v0 & % 17.87/3.32 | count(v0) = v1 & count(all_13_2) = v1 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (15) with 5, all_13_2, simplifying with (22), (23) % 17.87/3.32 | gives: % 17.87/3.32 | (31) ? [v0: collection] : (remove(5, all_13_2) = v0 & add(5, v0) = % 17.87/3.32 | all_13_2 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (3) with all_13_1, all_13_2, simplifying with (22), % 17.87/3.32 | (24) gives: % 17.87/3.32 | (32) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ % 17.87/3.32 | ($difference(v2, v1) = -1) & add(all_13_1, all_13_2) = v0 & % 17.87/3.32 | count(v0) = v1 & count(all_13_2) = v2 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (13) with all_13_1, all_13_2, simplifying with % 17.87/3.32 | (22), (24) gives: % 17.87/3.32 | (33) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = v1) & % 17.87/3.32 | remove(all_13_1, all_13_2) = v0 & count(v0) = v1 & count(all_13_2) = % 17.87/3.32 | v2 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (11) with all_13_1, all_13_2, simplifying with % 17.87/3.32 | (22), (24) gives: % 17.87/3.32 | (34) ? [v0: collection] : ? [v1: int] : (remove(all_13_1, all_13_2) = v0 % 17.87/3.32 | & count(v0) = v1 & count(all_13_2) = $sum(v1, 1) & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (7) with all_13_1, all_13_2, simplifying with (22), % 17.87/3.32 | (24) gives: % 17.87/3.32 | (35) ? [v0: collection] : ? [v1: int] : (add(all_13_1, all_13_2) = v0 & % 17.87/3.32 | count(v0) = v1 & count(all_13_2) = v1 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (15) with all_13_1, all_13_2, simplifying with % 17.87/3.32 | (22), (24) gives: % 17.87/3.32 | (36) ? [v0: collection] : (remove(all_13_1, all_13_2) = v0 & add(all_13_1, % 17.87/3.32 | v0) = all_13_2 & collection(v0)) % 17.87/3.32 | % 17.87/3.32 | GROUND_INST: instantiating (3) with all_13_0, all_13_2, simplifying with (22), % 17.87/3.32 | (25) gives: % 17.87/3.32 | (37) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ % 17.87/3.32 | ($difference(v2, v1) = -1) & add(all_13_0, all_13_2) = v0 & % 18.18/3.32 | count(v0) = v1 & count(all_13_2) = v2 & collection(v0)) % 18.18/3.32 | % 18.18/3.32 | GROUND_INST: instantiating (13) with all_13_0, all_13_2, simplifying with % 18.18/3.32 | (22), (25) gives: % 18.18/3.32 | (38) ? [v0: collection] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = v1) & % 18.18/3.32 | remove(all_13_0, all_13_2) = v0 & count(v0) = v1 & count(all_13_2) = % 18.18/3.32 | v2 & collection(v0)) % 18.18/3.32 | % 18.18/3.32 | GROUND_INST: instantiating (11) with all_13_0, all_13_2, simplifying with % 18.18/3.32 | (22), (25) gives: % 18.18/3.33 | (39) ? [v0: collection] : ? [v1: int] : (remove(all_13_0, all_13_2) = v0 % 18.18/3.33 | & count(v0) = v1 & count(all_13_2) = $sum(v1, 1) & collection(v0)) % 18.18/3.33 | % 18.18/3.33 | GROUND_INST: instantiating (7) with all_13_0, all_13_2, simplifying with (22), % 18.18/3.33 | (25) gives: % 18.18/3.33 | (40) ? [v0: collection] : ? [v1: int] : (add(all_13_0, all_13_2) = v0 & % 18.18/3.33 | count(v0) = v1 & count(all_13_2) = v1 & collection(v0)) % 18.18/3.33 | % 18.18/3.33 | GROUND_INST: instantiating (15) with all_13_0, all_13_2, simplifying with % 18.18/3.33 | (22), (25) gives: % 18.18/3.33 | (41) ? [v0: collection] : (remove(all_13_0, all_13_2) = v0 & add(all_13_0, % 18.18/3.33 | v0) = all_13_2 & collection(v0)) % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (41) with fresh symbol all_24_0 gives: % 18.18/3.33 | (42) remove(all_13_0, all_13_2) = all_24_0 & add(all_13_0, all_24_0) = % 18.18/3.33 | all_13_2 & collection(all_24_0) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (42) implies: % 18.18/3.33 | (43) add(all_13_0, all_24_0) = all_13_2 % 18.18/3.33 | (44) remove(all_13_0, all_13_2) = all_24_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (31) with fresh symbol all_26_0 gives: % 18.18/3.33 | (45) remove(5, all_13_2) = all_26_0 & add(5, all_26_0) = all_13_2 & % 18.18/3.33 | collection(all_26_0) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (45) implies: % 18.18/3.33 | (46) add(5, all_26_0) = all_13_2 % 18.18/3.33 | (47) remove(5, all_13_2) = all_26_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (36) with fresh symbol all_28_0 gives: % 18.18/3.33 | (48) remove(all_13_1, all_13_2) = all_28_0 & add(all_13_1, all_28_0) = % 18.18/3.33 | all_13_2 & collection(all_28_0) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (48) implies: % 18.18/3.33 | (49) add(all_13_1, all_28_0) = all_13_2 % 18.18/3.33 | (50) remove(all_13_1, all_13_2) = all_28_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (40) with fresh symbols all_30_0, all_30_1 gives: % 18.18/3.33 | (51) add(all_13_0, all_13_2) = all_30_1 & count(all_30_1) = all_30_0 & % 18.18/3.33 | count(all_13_2) = all_30_0 & collection(all_30_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (51) implies: % 18.18/3.33 | (52) count(all_13_2) = all_30_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (39) with fresh symbols all_32_0, all_32_1 gives: % 18.18/3.33 | (53) remove(all_13_0, all_13_2) = all_32_1 & count(all_32_1) = all_32_0 & % 18.18/3.33 | count(all_13_2) = $sum(all_32_0, 1) & collection(all_32_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (53) implies: % 18.18/3.33 | (54) collection(all_32_1) % 18.18/3.33 | (55) count(all_13_2) = $sum(all_32_0, 1) % 18.18/3.33 | (56) count(all_32_1) = all_32_0 % 18.18/3.33 | (57) remove(all_13_0, all_13_2) = all_32_1 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (34) with fresh symbols all_34_0, all_34_1 gives: % 18.18/3.33 | (58) remove(all_13_1, all_13_2) = all_34_1 & count(all_34_1) = all_34_0 & % 18.18/3.33 | count(all_13_2) = $sum(all_34_0, 1) & collection(all_34_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (58) implies: % 18.18/3.33 | (59) collection(all_34_1) % 18.18/3.33 | (60) count(all_13_2) = $sum(all_34_0, 1) % 18.18/3.33 | (61) count(all_34_1) = all_34_0 % 18.18/3.33 | (62) remove(all_13_1, all_13_2) = all_34_1 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (30) with fresh symbols all_36_0, all_36_1 gives: % 18.18/3.33 | (63) add(5, all_13_2) = all_36_1 & count(all_36_1) = all_36_0 & % 18.18/3.33 | count(all_13_2) = all_36_0 & collection(all_36_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (63) implies: % 18.18/3.33 | (64) count(all_13_2) = all_36_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (35) with fresh symbols all_38_0, all_38_1 gives: % 18.18/3.33 | (65) add(all_13_1, all_13_2) = all_38_1 & count(all_38_1) = all_38_0 & % 18.18/3.33 | count(all_13_2) = all_38_0 & collection(all_38_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (65) implies: % 18.18/3.33 | (66) count(all_13_2) = all_38_0 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (29) with fresh symbols all_40_0, all_40_1 gives: % 18.18/3.33 | (67) remove(5, all_13_2) = all_40_1 & count(all_40_1) = all_40_0 & % 18.18/3.33 | count(all_13_2) = $sum(all_40_0, 1) & collection(all_40_1) % 18.18/3.33 | % 18.18/3.33 | ALPHA: (67) implies: % 18.18/3.33 | (68) collection(all_40_1) % 18.18/3.33 | (69) count(all_13_2) = $sum(all_40_0, 1) % 18.18/3.33 | (70) remove(5, all_13_2) = all_40_1 % 18.18/3.33 | % 18.18/3.33 | DELTA: instantiating (38) with fresh symbols all_42_0, all_42_1, all_42_2 % 18.18/3.33 | gives: % 18.18/3.34 | (71) ~ (all_42_0 = all_42_1) & remove(all_13_0, all_13_2) = all_42_2 & % 18.18/3.34 | count(all_42_2) = all_42_1 & count(all_13_2) = all_42_0 & % 18.18/3.34 | collection(all_42_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (71) implies: % 18.18/3.34 | (72) count(all_13_2) = all_42_0 % 18.18/3.34 | (73) count(all_42_2) = all_42_1 % 18.18/3.34 | (74) remove(all_13_0, all_13_2) = all_42_2 % 18.18/3.34 | % 18.18/3.34 | DELTA: instantiating (37) with fresh symbols all_44_0, all_44_1, all_44_2 % 18.18/3.34 | gives: % 18.18/3.34 | (75) ~ ($difference(all_44_0, all_44_1) = -1) & add(all_13_0, all_13_2) = % 18.18/3.34 | all_44_2 & count(all_44_2) = all_44_1 & count(all_13_2) = all_44_0 & % 18.18/3.34 | collection(all_44_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (75) implies: % 18.18/3.34 | (76) count(all_13_2) = all_44_0 % 18.18/3.34 | % 18.18/3.34 | DELTA: instantiating (28) with fresh symbols all_46_0, all_46_1, all_46_2 % 18.18/3.34 | gives: % 18.18/3.34 | (77) ~ (all_46_0 = all_46_1) & remove(5, all_13_2) = all_46_2 & % 18.18/3.34 | count(all_46_2) = all_46_1 & count(all_13_2) = all_46_0 & % 18.18/3.34 | collection(all_46_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (77) implies: % 18.18/3.34 | (78) count(all_13_2) = all_46_0 % 18.18/3.34 | (79) remove(5, all_13_2) = all_46_2 % 18.18/3.34 | % 18.18/3.34 | DELTA: instantiating (27) with fresh symbols all_48_0, all_48_1, all_48_2 % 18.18/3.34 | gives: % 18.18/3.34 | (80) ~ ($difference(all_48_0, all_48_1) = -1) & add(5, all_13_2) = % 18.18/3.34 | all_48_2 & count(all_48_2) = all_48_1 & count(all_13_2) = all_48_0 & % 18.18/3.34 | collection(all_48_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (80) implies: % 18.18/3.34 | (81) count(all_13_2) = all_48_0 % 18.18/3.34 | % 18.18/3.34 | DELTA: instantiating (32) with fresh symbols all_50_0, all_50_1, all_50_2 % 18.18/3.34 | gives: % 18.18/3.34 | (82) ~ ($difference(all_50_0, all_50_1) = -1) & add(all_13_1, all_13_2) = % 18.18/3.34 | all_50_2 & count(all_50_2) = all_50_1 & count(all_13_2) = all_50_0 & % 18.18/3.34 | collection(all_50_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (82) implies: % 18.18/3.34 | (83) count(all_13_2) = all_50_0 % 18.18/3.34 | % 18.18/3.34 | DELTA: instantiating (33) with fresh symbols all_52_0, all_52_1, all_52_2 % 18.18/3.34 | gives: % 18.18/3.34 | (84) ~ (all_52_0 = all_52_1) & remove(all_13_1, all_13_2) = all_52_2 & % 18.18/3.34 | count(all_52_2) = all_52_1 & count(all_13_2) = all_52_0 & % 18.18/3.34 | collection(all_52_2) % 18.18/3.34 | % 18.18/3.34 | ALPHA: (84) implies: % 18.18/3.34 | (85) count(all_13_2) = all_52_0 % 18.18/3.34 | (86) count(all_52_2) = all_52_1 % 18.18/3.34 | (87) remove(all_13_1, all_13_2) = all_52_2 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with $sum(all_32_0, 1), all_36_0, all_13_2, % 18.18/3.34 | simplifying with (55), (64) gives: % 18.18/3.34 | (88) $difference(all_36_0, all_32_0) = 1 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with all_36_0, $sum(all_40_0, 1), all_13_2, % 18.18/3.34 | simplifying with (64), (69) gives: % 18.18/3.34 | (89) $difference(all_40_0, all_36_0) = -1 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with all_42_0, all_44_0, all_13_2, simplifying % 18.18/3.34 | with (72), (76) gives: % 18.18/3.34 | (90) all_44_0 = all_42_0 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with all_38_0, all_44_0, all_13_2, simplifying % 18.18/3.34 | with (66), (76) gives: % 18.18/3.34 | (91) all_44_0 = all_38_0 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with all_36_0, all_44_0, all_13_2, simplifying % 18.18/3.34 | with (64), (76) gives: % 18.18/3.34 | (92) all_44_0 = all_36_0 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with all_46_0, all_48_0, all_13_2, simplifying % 18.18/3.34 | with (78), (81) gives: % 18.18/3.34 | (93) all_48_0 = all_46_0 % 18.18/3.34 | % 18.18/3.34 | GROUND_INST: instantiating (16) with $sum(all_40_0, 1), all_48_0, all_13_2, % 18.18/3.34 | simplifying with (69), (81) gives: % 18.18/3.35 | (94) $difference(all_48_0, all_40_0) = 1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (16) with $sum(all_34_0, 1), all_48_0, all_13_2, % 18.18/3.35 | simplifying with (60), (81) gives: % 18.18/3.35 | (95) $difference(all_48_0, all_34_0) = 1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (16) with 2, all_50_0, all_13_2, simplifying with % 18.18/3.35 | (26), (83) gives: % 18.18/3.35 | (96) all_50_0 = 2 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (16) with $sum(all_32_0, 1), all_50_0, all_13_2, % 18.18/3.35 | simplifying with (55), (83) gives: % 18.18/3.35 | (97) $difference(all_50_0, all_32_0) = 1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (16) with all_42_0, all_52_0, all_13_2, simplifying % 18.18/3.35 | with (72), (85) gives: % 18.18/3.35 | (98) all_52_0 = all_42_0 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (16) with all_30_0, all_52_0, all_13_2, simplifying % 18.18/3.35 | with (52), (85) gives: % 18.18/3.35 | (99) all_52_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_40_1, all_46_2, all_13_2, 5, % 18.18/3.35 | simplifying with (70), (79) gives: % 18.18/3.35 | (100) all_46_2 = all_40_1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_26_0, all_46_2, all_13_2, 5, % 18.18/3.35 | simplifying with (47), (79) gives: % 18.18/3.35 | (101) all_46_2 = all_26_0 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_34_1, all_52_2, all_13_2, all_13_1, % 18.18/3.35 | simplifying with (62), (87) gives: % 18.18/3.35 | (102) all_52_2 = all_34_1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_28_0, all_52_2, all_13_2, all_13_1, % 18.18/3.35 | simplifying with (50), (87) gives: % 18.18/3.35 | (103) all_52_2 = all_28_0 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_32_1, all_42_2, all_13_2, all_13_0, % 18.18/3.35 | simplifying with (57), (74) gives: % 18.18/3.35 | (104) all_42_2 = all_32_1 % 18.18/3.35 | % 18.18/3.35 | GROUND_INST: instantiating (18) with all_24_0, all_42_2, all_13_2, all_13_0, % 18.18/3.35 | simplifying with (44), (74) gives: % 18.18/3.35 | (105) all_42_2 = all_24_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (98), (99) imply: % 18.18/3.35 | (106) all_42_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (106) implies: % 18.18/3.35 | (107) all_42_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (102), (103) imply: % 18.18/3.35 | (108) all_34_1 = all_28_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (108) implies: % 18.18/3.35 | (109) all_34_1 = all_28_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (96), (97) imply: % 18.18/3.35 | (110) all_32_0 = 1 % 18.18/3.35 | % 18.18/3.35 | SIMP: (110) implies: % 18.18/3.35 | (111) all_32_0 = 1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (93), (94) imply: % 18.18/3.35 | (112) $difference(all_46_0, all_40_0) = 1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (93), (95) imply: % 18.18/3.35 | (113) $difference(all_46_0, all_34_0) = 1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (112), (113) imply: % 18.18/3.35 | (114) all_40_0 = all_34_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (114) implies: % 18.18/3.35 | (115) all_40_0 = all_34_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (100), (101) imply: % 18.18/3.35 | (116) all_40_1 = all_26_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (90), (91) imply: % 18.18/3.35 | (117) all_42_0 = all_38_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (117) implies: % 18.18/3.35 | (118) all_42_0 = all_38_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (91), (92) imply: % 18.18/3.35 | (119) all_38_0 = all_36_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (107), (118) imply: % 18.18/3.35 | (120) all_38_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (120) implies: % 18.18/3.35 | (121) all_38_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (104), (105) imply: % 18.18/3.35 | (122) all_32_1 = all_24_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (122) implies: % 18.18/3.35 | (123) all_32_1 = all_24_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (89), (115) imply: % 18.18/3.35 | (124) $difference(all_36_0, all_34_0) = 1 % 18.18/3.35 | % 18.18/3.35 | SIMP: (124) implies: % 18.18/3.35 | (125) $difference(all_36_0, all_34_0) = 1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (119), (121) imply: % 18.18/3.35 | (126) all_36_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | SIMP: (126) implies: % 18.18/3.35 | (127) all_36_0 = all_30_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (88), (125) imply: % 18.18/3.35 | (128) all_34_0 = all_32_0 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (125), (127) imply: % 18.18/3.35 | (129) $difference(all_34_0, all_30_0) = -1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (128), (129) imply: % 18.18/3.35 | (130) $difference(all_32_0, all_30_0) = -1 % 18.18/3.35 | % 18.18/3.35 | SIMP: (130) implies: % 18.18/3.35 | (131) $difference(all_32_0, all_30_0) = -1 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (111), (131) imply: % 18.18/3.35 | (132) all_30_0 = 2 % 18.18/3.35 | % 18.18/3.35 | COMBINE_EQS: (129), (132) imply: % 18.18/3.35 | (133) all_34_0 = 1 % 18.18/3.35 | % 18.18/3.35 | REDUCE: (86), (103) imply: % 18.18/3.35 | (134) count(all_28_0) = all_52_1 % 18.18/3.35 | % 18.18/3.35 | REDUCE: (73), (105) imply: % 18.18/3.35 | (135) count(all_24_0) = all_42_1 % 18.18/3.35 | % 18.18/3.35 | REDUCE: (61), (109), (133) imply: % 18.18/3.35 | (136) count(all_28_0) = 1 % 18.18/3.36 | % 18.18/3.36 | REDUCE: (56), (111), (123) imply: % 18.18/3.36 | (137) count(all_24_0) = 1 % 18.18/3.36 | % 18.18/3.36 | REDUCE: (68), (116) imply: % 18.18/3.36 | (138) collection(all_26_0) % 18.18/3.36 | % 18.18/3.36 | REDUCE: (59), (109) imply: % 18.18/3.36 | (139) collection(all_28_0) % 18.18/3.36 | % 18.18/3.36 | REDUCE: (54), (123) imply: % 18.18/3.36 | (140) collection(all_24_0) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (16) with 1, all_42_1, all_24_0, simplifying with % 18.18/3.36 | (135), (137) gives: % 18.18/3.36 | (141) all_42_1 = 1 % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (16) with 1, all_52_1, all_28_0, simplifying with % 18.18/3.36 | (134), (136) gives: % 18.18/3.36 | (142) all_52_1 = 1 % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (5) with 5, all_26_0, all_13_2, simplifying with % 18.18/3.36 | (46), (138) gives: % 18.18/3.36 | (143) ? [v0: int] : ? [v1: int] : ? [v2: int] : (($difference(v2, v1) = % 18.18/3.36 | -1 & count(all_26_0) = $sum(v1, -1) & count(all_13_2) = v1) | (v0 % 18.18/3.36 | = 0 & in(5, all_26_0) = 0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (9) with 5, all_26_0, all_13_2, simplifying with % 18.18/3.36 | (46), (138) gives: % 18.18/3.36 | (144) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = v1 & % 18.18/3.36 | count(all_26_0) = v1 & count(all_13_2) = v1) | ( ~ (v0 = 0) & % 18.18/3.36 | in(5, all_26_0) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (8) with 5, all_26_0, all_13_2, simplifying with % 18.18/3.36 | (46), (138) gives: % 18.18/3.36 | (145) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = 0 & in(5, % 18.18/3.36 | all_26_0) = 0) | ( ~ (v1 = v0) & count(all_26_0) = v1 & % 18.18/3.36 | count(all_13_2) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (4) with 5, all_26_0, all_13_2, simplifying with % 18.18/3.36 | (46), (138) gives: % 18.18/3.36 | (146) ? [v0: int] : ? [v1: int] : ? [v2: int] : (( ~ (v2 = 0) & in(5, % 18.18/3.36 | all_26_0) = v2) | ( ~ ($difference(v1, v0) = -1) & % 18.18/3.36 | count(all_26_0) = v1 & count(all_13_2) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (10) with all_13_0, all_28_0, all_13_1, all_13_2, % 18.18/3.36 | simplifying with (25), (49), (139) gives: % 18.18/3.36 | (147) all_13_0 = all_13_1 | in(all_13_0, all_28_0) = 0 % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (10) with 5, all_28_0, all_13_1, all_13_2, % 18.18/3.36 | simplifying with (23), (49), (139) gives: % 18.18/3.36 | (148) all_13_1 = 5 | in(5, all_28_0) = 0 % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (5) with all_13_1, all_28_0, all_13_2, simplifying % 18.18/3.36 | with (49), (139) gives: % 18.18/3.36 | (149) ? [v0: int] : ? [v1: int] : ? [v2: int] : (($difference(v2, v1) = % 18.18/3.36 | -1 & count(all_28_0) = $sum(v1, -1) & count(all_13_2) = v1) | (v0 % 18.18/3.36 | = 0 & in(all_13_1, all_28_0) = 0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (9) with all_13_1, all_28_0, all_13_2, simplifying % 18.18/3.36 | with (49), (139) gives: % 18.18/3.36 | (150) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = v1 & % 18.18/3.36 | count(all_28_0) = v1 & count(all_13_2) = v1) | ( ~ (v0 = 0) & % 18.18/3.36 | in(all_13_1, all_28_0) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (8) with all_13_1, all_28_0, all_13_2, simplifying % 18.18/3.36 | with (49), (139) gives: % 18.18/3.36 | (151) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = 0 & in(all_13_1, % 18.18/3.36 | all_28_0) = 0) | ( ~ (v1 = v0) & count(all_28_0) = v1 & % 18.18/3.36 | count(all_13_2) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (4) with all_13_1, all_28_0, all_13_2, simplifying % 18.18/3.36 | with (49), (139) gives: % 18.18/3.36 | (152) ? [v0: int] : ? [v1: int] : ? [v2: int] : (( ~ (v2 = 0) & % 18.18/3.36 | in(all_13_1, all_28_0) = v2) | ( ~ ($difference(v1, v0) = -1) & % 18.18/3.36 | count(all_28_0) = v1 & count(all_13_2) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (5) with all_13_0, all_24_0, all_13_2, simplifying % 18.18/3.36 | with (43), (140) gives: % 18.18/3.36 | (153) ? [v0: int] : ? [v1: int] : ? [v2: int] : (($difference(v2, v1) = % 18.18/3.36 | -1 & count(all_24_0) = $sum(v1, -1) & count(all_13_2) = v1) | (v0 % 18.18/3.36 | = 0 & in(all_13_0, all_24_0) = 0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (9) with all_13_0, all_24_0, all_13_2, simplifying % 18.18/3.36 | with (43), (140) gives: % 18.18/3.36 | (154) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = v1 & % 18.18/3.36 | count(all_24_0) = v1 & count(all_13_2) = v1) | ( ~ (v0 = 0) & % 18.18/3.36 | in(all_13_0, all_24_0) = v0)) % 18.18/3.36 | % 18.18/3.36 | GROUND_INST: instantiating (8) with all_13_0, all_24_0, all_13_2, simplifying % 18.18/3.36 | with (43), (140) gives: % 18.18/3.37 | (155) ? [v0: int] : ? [v1: int] : ? [v2: int] : ((v2 = 0 & in(all_13_0, % 18.18/3.37 | all_24_0) = 0) | ( ~ (v1 = v0) & count(all_24_0) = v1 & % 18.18/3.37 | count(all_13_2) = v0)) % 18.18/3.37 | % 18.18/3.37 | GROUND_INST: instantiating (6) with 5, all_13_2, all_26_0, simplifying with % 18.18/3.37 | (22), (47) gives: % 18.18/3.37 | (156) ? [v0: int] : ( ~ (v0 = 0) & in(5, all_26_0) = v0) % 18.18/3.37 | % 18.18/3.37 | GROUND_INST: instantiating (6) with all_13_1, all_13_2, all_28_0, simplifying % 18.18/3.37 | with (22), (50) gives: % 18.18/3.37 | (157) ? [v0: int] : ( ~ (v0 = 0) & in(all_13_1, all_28_0) = v0) % 18.18/3.37 | % 18.18/3.37 | GROUND_INST: instantiating (6) with all_13_0, all_13_2, all_24_0, simplifying % 18.18/3.37 | with (22), (44) gives: % 18.18/3.37 | (158) ? [v0: int] : ( ~ (v0 = 0) & in(all_13_0, all_24_0) = v0) % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (158) with fresh symbol all_68_0 gives: % 18.18/3.37 | (159) ~ (all_68_0 = 0) & in(all_13_0, all_24_0) = all_68_0 % 18.18/3.37 | % 18.18/3.37 | ALPHA: (159) implies: % 18.18/3.37 | (160) ~ (all_68_0 = 0) % 18.18/3.37 | (161) in(all_13_0, all_24_0) = all_68_0 % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (157) with fresh symbol all_70_0 gives: % 18.18/3.37 | (162) ~ (all_70_0 = 0) & in(all_13_1, all_28_0) = all_70_0 % 18.18/3.37 | % 18.18/3.37 | ALPHA: (162) implies: % 18.18/3.37 | (163) ~ (all_70_0 = 0) % 18.18/3.37 | (164) in(all_13_1, all_28_0) = all_70_0 % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (156) with fresh symbol all_72_0 gives: % 18.18/3.37 | (165) ~ (all_72_0 = 0) & in(5, all_26_0) = all_72_0 % 18.18/3.37 | % 18.18/3.37 | ALPHA: (165) implies: % 18.18/3.37 | (166) ~ (all_72_0 = 0) % 18.18/3.37 | (167) in(5, all_26_0) = all_72_0 % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (150) with fresh symbols all_74_0, all_74_1, all_74_2 % 18.18/3.37 | gives: % 18.18/3.37 | (168) (all_74_0 = all_74_1 & count(all_28_0) = all_74_1 & count(all_13_2) = % 18.18/3.37 | all_74_1) | ( ~ (all_74_2 = 0) & in(all_13_1, all_28_0) = all_74_2) % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (149) with fresh symbols all_75_0, all_75_1, all_75_2 % 18.18/3.37 | gives: % 18.18/3.37 | (169) ($difference(all_75_0, all_75_1) = -1 & count(all_28_0) = % 18.18/3.37 | $sum(all_75_1, -1) & count(all_13_2) = all_75_1) | (all_75_2 = 0 & % 18.18/3.37 | in(all_13_1, all_28_0) = 0) % 18.18/3.37 | % 18.18/3.37 | DELTA: instantiating (155) with fresh symbols all_76_0, all_76_1, all_76_2 % 18.41/3.37 | gives: % 18.41/3.37 | (170) (all_76_0 = 0 & in(all_13_0, all_24_0) = 0) | ( ~ (all_76_1 = % 18.41/3.37 | all_76_2) & count(all_24_0) = all_76_1 & count(all_13_2) = % 18.41/3.37 | all_76_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (153) with fresh symbols all_77_0, all_77_1, all_77_2 % 18.41/3.37 | gives: % 18.41/3.37 | (171) ($difference(all_77_0, all_77_1) = -1 & count(all_24_0) = % 18.41/3.37 | $sum(all_77_1, -1) & count(all_13_2) = all_77_1) | (all_77_2 = 0 & % 18.41/3.37 | in(all_13_0, all_24_0) = 0) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (154) with fresh symbols all_78_0, all_78_1, all_78_2 % 18.41/3.37 | gives: % 18.41/3.37 | (172) (all_78_0 = all_78_1 & count(all_24_0) = all_78_1 & count(all_13_2) = % 18.41/3.37 | all_78_1) | ( ~ (all_78_2 = 0) & in(all_13_0, all_24_0) = all_78_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (143) with fresh symbols all_79_0, all_79_1, all_79_2 % 18.41/3.37 | gives: % 18.41/3.37 | (173) ($difference(all_79_0, all_79_1) = -1 & count(all_26_0) = % 18.41/3.37 | $sum(all_79_1, -1) & count(all_13_2) = all_79_1) | (all_79_2 = 0 & % 18.41/3.37 | in(5, all_26_0) = 0) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (146) with fresh symbols all_81_0, all_81_1, all_81_2 % 18.41/3.37 | gives: % 18.41/3.37 | (174) ( ~ (all_81_0 = 0) & in(5, all_26_0) = all_81_0) | ( ~ % 18.41/3.37 | ($difference(all_81_1, all_81_2) = -1) & count(all_26_0) = all_81_1 % 18.41/3.37 | & count(all_13_2) = all_81_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (152) with fresh symbols all_82_0, all_82_1, all_82_2 % 18.41/3.37 | gives: % 18.41/3.37 | (175) ( ~ (all_82_0 = 0) & in(all_13_1, all_28_0) = all_82_0) | ( ~ % 18.41/3.37 | ($difference(all_82_1, all_82_2) = -1) & count(all_28_0) = all_82_1 % 18.41/3.37 | & count(all_13_2) = all_82_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (151) with fresh symbols all_83_0, all_83_1, all_83_2 % 18.41/3.37 | gives: % 18.41/3.37 | (176) (all_83_0 = 0 & in(all_13_1, all_28_0) = 0) | ( ~ (all_83_1 = % 18.41/3.37 | all_83_2) & count(all_28_0) = all_83_1 & count(all_13_2) = % 18.41/3.37 | all_83_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (145) with fresh symbols all_84_0, all_84_1, all_84_2 % 18.41/3.37 | gives: % 18.41/3.37 | (177) (all_84_0 = 0 & in(5, all_26_0) = 0) | ( ~ (all_84_1 = all_84_2) & % 18.41/3.37 | count(all_26_0) = all_84_1 & count(all_13_2) = all_84_2) % 18.41/3.37 | % 18.41/3.37 | DELTA: instantiating (144) with fresh symbols all_85_0, all_85_1, all_85_2 % 18.41/3.37 | gives: % 18.41/3.37 | (178) (all_85_0 = all_85_1 & count(all_26_0) = all_85_1 & count(all_13_2) = % 18.41/3.37 | all_85_1) | ( ~ (all_85_2 = 0) & in(5, all_26_0) = all_85_2) % 18.41/3.37 | % 18.41/3.37 | BETA: splitting (148) gives: % 18.41/3.37 | % 18.41/3.37 | Case 1: % 18.41/3.37 | | % 18.41/3.37 | | (179) in(5, all_28_0) = 0 % 18.41/3.37 | | % 18.41/3.37 | | BETA: splitting (147) gives: % 18.41/3.37 | | % 18.41/3.37 | | Case 1: % 18.41/3.37 | | | % 18.41/3.37 | | | (180) in(all_13_0, all_28_0) = 0 % 18.41/3.37 | | | % 18.41/3.37 | | | BETA: splitting (168) gives: % 18.41/3.37 | | | % 18.41/3.37 | | | Case 1: % 18.41/3.37 | | | | % 18.41/3.37 | | | | (181) all_74_0 = all_74_1 & count(all_28_0) = all_74_1 & % 18.41/3.37 | | | | count(all_13_2) = all_74_1 % 18.41/3.37 | | | | % 18.41/3.37 | | | | ALPHA: (181) implies: % 18.41/3.37 | | | | (182) count(all_13_2) = all_74_1 % 18.41/3.37 | | | | (183) count(all_28_0) = all_74_1 % 18.41/3.37 | | | | % 18.41/3.37 | | | | GROUND_INST: instantiating (16) with 2, all_74_1, all_13_2, simplifying % 18.41/3.37 | | | | with (26), (182) gives: % 18.41/3.37 | | | | (184) all_74_1 = 2 % 18.41/3.37 | | | | % 18.41/3.37 | | | | GROUND_INST: instantiating (16) with 1, all_74_1, all_28_0, simplifying % 18.41/3.37 | | | | with (136), (183) gives: % 18.41/3.37 | | | | (185) all_74_1 = 1 % 18.41/3.37 | | | | % 18.41/3.37 | | | | COMBINE_EQS: (184), (185) imply: % 18.41/3.37 | | | | (186) $false % 18.41/3.37 | | | | % 18.41/3.37 | | | | CLOSE: (186) is inconsistent. % 18.41/3.37 | | | | % 18.41/3.38 | | | Case 2: % 18.41/3.38 | | | | % 18.41/3.38 | | | | (187) ~ (all_74_2 = 0) & in(all_13_1, all_28_0) = all_74_2 % 18.41/3.38 | | | | % 18.41/3.38 | | | | ALPHA: (187) implies: % 18.41/3.38 | | | | (188) in(all_13_1, all_28_0) = all_74_2 % 18.41/3.38 | | | | % 18.41/3.38 | | | | BETA: splitting (170) gives: % 18.41/3.38 | | | | % 18.41/3.38 | | | | Case 1: % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | (189) all_76_0 = 0 & in(all_13_0, all_24_0) = 0 % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | ALPHA: (189) implies: % 18.41/3.38 | | | | | (190) in(all_13_0, all_24_0) = 0 % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | REF_CLOSE: (16), (17), (26), (137), (160), (161), (172), (190) are % 18.41/3.38 | | | | | inconsistent by sub-proof #3. % 18.41/3.38 | | | | | % 18.41/3.38 | | | | Case 2: % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | (191) ~ (all_76_1 = all_76_2) & count(all_24_0) = all_76_1 & % 18.41/3.38 | | | | | count(all_13_2) = all_76_2 % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | ALPHA: (191) implies: % 18.41/3.38 | | | | | (192) count(all_13_2) = all_76_2 % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | BETA: splitting (169) gives: % 18.41/3.38 | | | | | % 18.41/3.38 | | | | | Case 1: % 18.41/3.38 | | | | | | % 18.41/3.38 | | | | | | (193) $difference(all_75_0, all_75_1) = -1 & count(all_28_0) = % 18.41/3.38 | | | | | | $sum(all_75_1, -1) & count(all_13_2) = all_75_1 % 18.41/3.38 | | | | | | % 18.41/3.38 | | | | | | ALPHA: (193) implies: % 18.41/3.38 | | | | | | (194) count(all_13_2) = all_75_1 % 18.41/3.38 | | | | | | (195) count(all_28_0) = $sum(all_75_1, -1) % 18.41/3.38 | | | | | | % 18.41/3.38 | | | | | | BETA: splitting (171) gives: % 18.41/3.38 | | | | | | % 18.41/3.38 | | | | | | Case 1: % 18.41/3.38 | | | | | | | % 18.41/3.38 | | | | | | | (196) $difference(all_77_0, all_77_1) = -1 & count(all_24_0) = % 18.41/3.38 | | | | | | | $sum(all_77_1, -1) & count(all_13_2) = all_77_1 % 18.41/3.38 | | | | | | | % 18.41/3.38 | | | | | | | ALPHA: (196) implies: % 18.41/3.38 | | | | | | | (197) count(all_13_2) = all_77_1 % 18.41/3.38 | | | | | | | % 18.41/3.38 | | | | | | | BETA: splitting (177) gives: % 18.41/3.38 | | | | | | | % 18.41/3.38 | | | | | | | Case 1: % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | (198) all_84_0 = 0 & in(5, all_26_0) = 0 % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | ALPHA: (198) implies: % 18.41/3.38 | | | | | | | | (199) in(5, all_26_0) = 0 % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | REF_CLOSE: (17), (166), (167), (199) are inconsistent by % 18.41/3.38 | | | | | | | | sub-proof #2. % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | Case 2: % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | (200) ~ (all_84_1 = all_84_2) & count(all_26_0) = all_84_1 & % 18.41/3.38 | | | | | | | | count(all_13_2) = all_84_2 % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | ALPHA: (200) implies: % 18.41/3.38 | | | | | | | | (201) count(all_13_2) = all_84_2 % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | BETA: splitting (173) gives: % 18.41/3.38 | | | | | | | | % 18.41/3.38 | | | | | | | | Case 1: % 18.41/3.38 | | | | | | | | | % 18.41/3.38 | | | | | | | | | (202) $difference(all_79_0, all_79_1) = -1 & % 18.41/3.38 | | | | | | | | | count(all_26_0) = $sum(all_79_1, -1) & % 18.41/3.38 | | | | | | | | | count(all_13_2) = all_79_1 % 18.41/3.38 | | | | | | | | | % 18.41/3.38 | | | | | | | | | ALPHA: (202) implies: % 18.41/3.38 | | | | | | | | | (203) count(all_13_2) = all_79_1 % 18.41/3.38 | | | | | | | | | (204) count(all_26_0) = $sum(all_79_1, -1) % 18.41/3.38 | | | | | | | | | % 18.41/3.38 | | | | | | | | | BETA: splitting (176) gives: % 18.41/3.38 | | | | | | | | | % 18.41/3.38 | | | | | | | | | Case 1: % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | (205) all_83_0 = 0 & in(all_13_1, all_28_0) = 0 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | ALPHA: (205) implies: % 18.41/3.38 | | | | | | | | | | (206) in(all_13_1, all_28_0) = 0 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | REF_CLOSE: (17), (163), (164), (188), (206) are inconsistent % 18.41/3.38 | | | | | | | | | | by sub-proof #1. % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | Case 2: % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | (207) ~ (all_83_1 = all_83_2) & count(all_28_0) = % 18.41/3.38 | | | | | | | | | | all_83_1 & count(all_13_2) = all_83_2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | ALPHA: (207) implies: % 18.41/3.38 | | | | | | | | | | (208) count(all_13_2) = all_83_2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (17) with all_70_0, all_74_2, % 18.41/3.38 | | | | | | | | | | all_28_0, all_13_1, simplifying with (164), (188) % 18.41/3.38 | | | | | | | | | | gives: % 18.41/3.38 | | | | | | | | | | (209) all_74_2 = all_70_0 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with all_75_1, all_76_2, % 18.41/3.38 | | | | | | | | | | all_13_2, simplifying with (192), (194) gives: % 18.41/3.38 | | | | | | | | | | (210) all_76_2 = all_75_1 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with all_76_2, all_77_1, % 18.41/3.38 | | | | | | | | | | all_13_2, simplifying with (192), (197) gives: % 18.41/3.38 | | | | | | | | | | (211) all_77_1 = all_76_2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with all_77_1, all_79_1, % 18.41/3.38 | | | | | | | | | | all_13_2, simplifying with (197), (203) gives: % 18.41/3.38 | | | | | | | | | | (212) all_79_1 = all_77_1 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with all_79_1, all_83_2, % 18.41/3.38 | | | | | | | | | | all_13_2, simplifying with (203), (208) gives: % 18.41/3.38 | | | | | | | | | | (213) all_83_2 = all_79_1 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with 2, all_84_2, all_13_2, % 18.41/3.38 | | | | | | | | | | simplifying with (26), (201) gives: % 18.41/3.38 | | | | | | | | | | (214) all_84_2 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | GROUND_INST: instantiating (16) with all_83_2, all_84_2, % 18.41/3.38 | | | | | | | | | | all_13_2, simplifying with (201), (208) gives: % 18.41/3.38 | | | | | | | | | | (215) all_84_2 = all_83_2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | COMBINE_EQS: (214), (215) imply: % 18.41/3.38 | | | | | | | | | | (216) all_83_2 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | SIMP: (216) implies: % 18.41/3.38 | | | | | | | | | | (217) all_83_2 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | COMBINE_EQS: (213), (217) imply: % 18.41/3.38 | | | | | | | | | | (218) all_79_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | SIMP: (218) implies: % 18.41/3.38 | | | | | | | | | | (219) all_79_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | COMBINE_EQS: (212), (219) imply: % 18.41/3.38 | | | | | | | | | | (220) all_77_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | SIMP: (220) implies: % 18.41/3.38 | | | | | | | | | | (221) all_77_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | COMBINE_EQS: (211), (221) imply: % 18.41/3.38 | | | | | | | | | | (222) all_76_2 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | SIMP: (222) implies: % 18.41/3.38 | | | | | | | | | | (223) all_76_2 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | COMBINE_EQS: (210), (223) imply: % 18.41/3.38 | | | | | | | | | | (224) all_75_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | SIMP: (224) implies: % 18.41/3.38 | | | | | | | | | | (225) all_75_1 = 2 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | REDUCE: (204), (219) imply: % 18.41/3.38 | | | | | | | | | | (226) count(all_26_0) = 1 % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | BETA: splitting (175) gives: % 18.41/3.38 | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | Case 1: % 18.41/3.38 | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | (227) ~ (all_82_0 = 0) & in(all_13_1, all_28_0) = % 18.41/3.38 | | | | | | | | | | | all_82_0 % 18.41/3.38 | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | ALPHA: (227) implies: % 18.41/3.38 | | | | | | | | | | | (228) ~ (all_82_0 = 0) % 18.41/3.38 | | | | | | | | | | | (229) in(all_13_1, all_28_0) = all_82_0 % 18.41/3.38 | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | BETA: splitting (178) gives: % 18.41/3.38 | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | Case 1: % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | (230) all_85_0 = all_85_1 & count(all_26_0) = all_85_1 & % 18.41/3.38 | | | | | | | | | | | | count(all_13_2) = all_85_1 % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | ALPHA: (230) implies: % 18.41/3.38 | | | | | | | | | | | | (231) count(all_13_2) = all_85_1 % 18.41/3.38 | | | | | | | | | | | | (232) count(all_26_0) = all_85_1 % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | GROUND_INST: instantiating (16) with 2, all_85_1, all_13_2, % 18.41/3.38 | | | | | | | | | | | | simplifying with (26), (231) gives: % 18.41/3.38 | | | | | | | | | | | | (233) all_85_1 = 2 % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | GROUND_INST: instantiating (16) with 1, all_85_1, all_26_0, % 18.41/3.38 | | | | | | | | | | | | simplifying with (226), (232) gives: % 18.41/3.38 | | | | | | | | | | | | (234) all_85_1 = 1 % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | COMBINE_EQS: (233), (234) imply: % 18.41/3.38 | | | | | | | | | | | | (235) $false % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.38 | | | | | | | | | | | | CLOSE: (235) is inconsistent. % 18.41/3.38 | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | Case 2: % 18.41/3.39 | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | (236) ~ (all_85_2 = 0) & in(5, all_26_0) = all_85_2 % 18.41/3.39 | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | ALPHA: (236) implies: % 18.41/3.39 | | | | | | | | | | | | (237) in(5, all_26_0) = all_85_2 % 18.41/3.39 | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | BETA: splitting (174) gives: % 18.41/3.39 | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | Case 1: % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | (238) ~ (all_81_0 = 0) & in(5, all_26_0) = all_81_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (238) implies: % 18.41/3.39 | | | | | | | | | | | | | (239) ~ (all_81_0 = 0) % 18.41/3.39 | | | | | | | | | | | | | (240) in(5, all_26_0) = all_81_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_72_0, all_85_2, % 18.41/3.39 | | | | | | | | | | | | | all_26_0, 5, simplifying with (167), (237) gives: % 18.41/3.39 | | | | | | | | | | | | | (241) all_85_2 = all_72_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_81_0, all_85_2, % 18.41/3.39 | | | | | | | | | | | | | all_26_0, 5, simplifying with (237), (240) gives: % 18.41/3.39 | | | | | | | | | | | | | (242) all_85_2 = all_81_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_70_0, all_82_0, % 18.41/3.39 | | | | | | | | | | | | | all_28_0, all_13_1, simplifying with (164), (229) % 18.41/3.39 | | | | | | | | | | | | | gives: % 18.41/3.39 | | | | | | | | | | | | | (243) all_82_0 = all_70_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | COMBINE_EQS: (241), (242) imply: % 18.41/3.39 | | | | | | | | | | | | | (244) all_81_0 = all_72_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 5, all_26_0, all_72_0, % 18.41/3.39 | | | | | | | | | | | | | simplifying with (138), (167) gives: % 18.41/3.39 | | | | | | | | | | | | | (245) all_72_0 = 0 | ? [v0: collection] : ? [v1: int] % 18.41/3.39 | | | | | | | | | | | | | : ? [v2: int] : ( ~ ($difference(v2, v1) = 1) & % 18.41/3.39 | | | | | | | | | | | | | remove(5, all_26_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_26_0) = v2 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (3) with 5, all_28_0, simplifying % 18.41/3.39 | | | | | | | | | | | | | with (139), (179) gives: % 18.41/3.39 | | | | | | | | | | | | | (246) ? [v0: collection] : ? [v1: int] : ? [v2: int] % 18.41/3.39 | | | | | | | | | | | | | : ( ~ ($difference(v2, v1) = -1) & add(5, % 18.41/3.39 | | | | | | | | | | | | | all_28_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_28_0) = v2 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 5, all_28_0, simplifying % 18.41/3.39 | | | | | | | | | | | | | with (139), (179) gives: % 18.41/3.39 | | | | | | | | | | | | | (247) ? [v0: collection] : ? [v1: int] : ? [v2: int] % 18.41/3.39 | | | | | | | | | | | | | : ( ~ (v2 = v1) & remove(5, all_28_0) = v0 & % 18.41/3.39 | | | | | | | | | | | | | count(v0) = v1 & count(all_28_0) = v2 & % 18.41/3.39 | | | | | | | | | | | | | collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (11) with 5, all_28_0, simplifying % 18.41/3.39 | | | | | | | | | | | | | with (139), (179) gives: % 18.41/3.39 | | | | | | | | | | | | | (248) ? [v0: collection] : ? [v1: int] : (remove(5, % 18.41/3.39 | | | | | | | | | | | | | all_28_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_28_0) = $sum(v1, 1) & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (7) with 5, all_28_0, simplifying % 18.41/3.39 | | | | | | | | | | | | | with (139), (179) gives: % 18.41/3.39 | | | | | | | | | | | | | (249) ? [v0: collection] : ? [v1: int] : (add(5, % 18.41/3.39 | | | | | | | | | | | | | all_28_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_28_0) = v1 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (15) with 5, all_28_0, simplifying % 18.41/3.39 | | | | | | | | | | | | | with (139), (179) gives: % 18.41/3.39 | | | | | | | | | | | | | (250) ? [v0: collection] : (remove(5, all_28_0) = v0 & % 18.41/3.39 | | | | | | | | | | | | | add(5, v0) = all_28_0 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_13_1, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | all_70_0, simplifying with (139), (164) gives: % 18.41/3.39 | | | | | | | | | | | | | (251) all_70_0 = 0 | ? [v0: collection] : ? [v1: int] % 18.41/3.39 | | | | | | | | | | | | | : ? [v2: int] : ( ~ ($difference(v2, v1) = 1) & % 18.41/3.39 | | | | | | | | | | | | | remove(all_13_1, all_28_0) = v0 & count(v0) = v1 % 18.41/3.39 | | | | | | | | | | | | | & count(all_28_0) = v2 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_13_1, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | all_70_0, simplifying with (139), (164) gives: % 18.41/3.39 | | | | | | | | | | | | | (252) all_70_0 = 0 | ? [v0: collection] : ? [v1: int] % 18.41/3.39 | | | | | | | | | | | | | : (remove(all_13_1, all_28_0) = v0 & count(v0) = % 18.41/3.39 | | | | | | | | | | | | | v1 & count(all_28_0) = v1 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_13_0, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | simplifying with (139), (180) gives: % 18.41/3.39 | | | | | | | | | | | | | (253) ? [v0: collection] : ? [v1: int] : ? [v2: int] % 18.41/3.39 | | | | | | | | | | | | | : ( ~ ($difference(v2, v1) = -1) & add(all_13_0, % 18.41/3.39 | | | | | | | | | | | | | all_28_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_28_0) = v2 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_13_0, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | simplifying with (139), (180) gives: % 18.41/3.39 | | | | | | | | | | | | | (254) ? [v0: collection] : ? [v1: int] : ? [v2: int] % 18.41/3.39 | | | | | | | | | | | | | : ( ~ (v2 = v1) & remove(all_13_0, all_28_0) = v0 % 18.41/3.39 | | | | | | | | | | | | | & count(v0) = v1 & count(all_28_0) = v2 & % 18.41/3.39 | | | | | | | | | | | | | collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (11) with all_13_0, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | simplifying with (139), (180) gives: % 18.41/3.39 | | | | | | | | | | | | | (255) ? [v0: collection] : ? [v1: int] : % 18.41/3.39 | | | | | | | | | | | | | (remove(all_13_0, all_28_0) = v0 & count(v0) = v1 % 18.41/3.39 | | | | | | | | | | | | | & count(all_28_0) = $sum(v1, 1) & % 18.41/3.39 | | | | | | | | | | | | | collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | GROUND_INST: instantiating (7) with all_13_0, all_28_0, % 18.41/3.39 | | | | | | | | | | | | | simplifying with (139), (180) gives: % 18.41/3.39 | | | | | | | | | | | | | (256) ? [v0: collection] : ? [v1: int] : % 18.41/3.39 | | | | | | | | | | | | | (add(all_13_0, all_28_0) = v0 & count(v0) = v1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_28_0) = v1 & collection(v0)) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (250) with fresh symbol all_175_0 % 18.41/3.39 | | | | | | | | | | | | | gives: % 18.41/3.39 | | | | | | | | | | | | | (257) remove(5, all_28_0) = all_175_0 & add(5, % 18.41/3.39 | | | | | | | | | | | | | all_175_0) = all_28_0 & collection(all_175_0) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (257) implies: % 18.41/3.39 | | | | | | | | | | | | | (258) add(5, all_175_0) = all_28_0 % 18.41/3.39 | | | | | | | | | | | | | (259) remove(5, all_28_0) = all_175_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (248) with fresh symbols all_201_0, % 18.41/3.39 | | | | | | | | | | | | | all_201_1 gives: % 18.41/3.39 | | | | | | | | | | | | | (260) remove(5, all_28_0) = all_201_1 & count(all_201_1) % 18.41/3.39 | | | | | | | | | | | | | = all_201_0 & count(all_28_0) = $sum(all_201_0, 1) % 18.41/3.39 | | | | | | | | | | | | | & collection(all_201_1) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (260) implies: % 18.41/3.39 | | | | | | | | | | | | | (261) collection(all_201_1) % 18.41/3.39 | | | | | | | | | | | | | (262) count(all_28_0) = $sum(all_201_0, 1) % 18.41/3.39 | | | | | | | | | | | | | (263) count(all_201_1) = all_201_0 % 18.41/3.39 | | | | | | | | | | | | | (264) remove(5, all_28_0) = all_201_1 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (255) with fresh symbols all_205_0, % 18.41/3.39 | | | | | | | | | | | | | all_205_1 gives: % 18.41/3.39 | | | | | | | | | | | | | (265) remove(all_13_0, all_28_0) = all_205_1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_205_1) = all_205_0 & count(all_28_0) = % 18.41/3.39 | | | | | | | | | | | | | $sum(all_205_0, 1) & collection(all_205_1) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (265) implies: % 18.41/3.39 | | | | | | | | | | | | | (266) count(all_28_0) = $sum(all_205_0, 1) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (249) with fresh symbols all_211_0, % 18.41/3.39 | | | | | | | | | | | | | all_211_1 gives: % 18.41/3.39 | | | | | | | | | | | | | (267) add(5, all_28_0) = all_211_1 & count(all_211_1) = % 18.41/3.39 | | | | | | | | | | | | | all_211_0 & count(all_28_0) = all_211_0 & % 18.41/3.39 | | | | | | | | | | | | | collection(all_211_1) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (267) implies: % 18.41/3.39 | | | | | | | | | | | | | (268) count(all_28_0) = all_211_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (256) with fresh symbols all_213_0, % 18.41/3.39 | | | | | | | | | | | | | all_213_1 gives: % 18.41/3.39 | | | | | | | | | | | | | (269) add(all_13_0, all_28_0) = all_213_1 & % 18.41/3.39 | | | | | | | | | | | | | count(all_213_1) = all_213_0 & count(all_28_0) = % 18.41/3.39 | | | | | | | | | | | | | all_213_0 & collection(all_213_1) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (269) implies: % 18.41/3.39 | | | | | | | | | | | | | (270) count(all_28_0) = all_213_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (253) with fresh symbols all_231_0, % 18.41/3.39 | | | | | | | | | | | | | all_231_1, all_231_2 gives: % 18.41/3.39 | | | | | | | | | | | | | (271) ~ ($difference(all_231_0, all_231_1) = -1) & % 18.41/3.39 | | | | | | | | | | | | | add(all_13_0, all_28_0) = all_231_2 & % 18.41/3.39 | | | | | | | | | | | | | count(all_231_2) = all_231_1 & count(all_28_0) = % 18.41/3.39 | | | | | | | | | | | | | all_231_0 & collection(all_231_2) % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | ALPHA: (271) implies: % 18.41/3.39 | | | | | | | | | | | | | (272) count(all_28_0) = all_231_0 % 18.41/3.39 | | | | | | | | | | | | | % 18.41/3.39 | | | | | | | | | | | | | DELTA: instantiating (254) with fresh symbols all_241_0, % 18.41/3.39 | | | | | | | | | | | | | all_241_1, all_241_2 gives: % 18.41/3.40 | | | | | | | | | | | | | (273) ~ (all_241_0 = all_241_1) & remove(all_13_0, % 18.41/3.40 | | | | | | | | | | | | | all_28_0) = all_241_2 & count(all_241_2) = % 18.41/3.40 | | | | | | | | | | | | | all_241_1 & count(all_28_0) = all_241_0 & % 18.41/3.40 | | | | | | | | | | | | | collection(all_241_2) % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | ALPHA: (273) implies: % 18.41/3.40 | | | | | | | | | | | | | (274) count(all_28_0) = all_241_0 % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | DELTA: instantiating (246) with fresh symbols all_253_0, % 18.41/3.40 | | | | | | | | | | | | | all_253_1, all_253_2 gives: % 18.41/3.40 | | | | | | | | | | | | | (275) ~ ($difference(all_253_0, all_253_1) = -1) & % 18.41/3.40 | | | | | | | | | | | | | add(5, all_28_0) = all_253_2 & count(all_253_2) = % 18.41/3.40 | | | | | | | | | | | | | all_253_1 & count(all_28_0) = all_253_0 & % 18.41/3.40 | | | | | | | | | | | | | collection(all_253_2) % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | ALPHA: (275) implies: % 18.41/3.40 | | | | | | | | | | | | | (276) count(all_28_0) = all_253_0 % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | DELTA: instantiating (247) with fresh symbols all_259_0, % 18.41/3.40 | | | | | | | | | | | | | all_259_1, all_259_2 gives: % 18.41/3.40 | | | | | | | | | | | | | (277) ~ (all_259_0 = all_259_1) & remove(5, all_28_0) = % 18.41/3.40 | | | | | | | | | | | | | all_259_2 & count(all_259_2) = all_259_1 & % 18.41/3.40 | | | | | | | | | | | | | count(all_28_0) = all_259_0 & % 18.41/3.40 | | | | | | | | | | | | | collection(all_259_2) % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | ALPHA: (277) implies: % 18.41/3.40 | | | | | | | | | | | | | (278) count(all_28_0) = all_259_0 % 18.41/3.40 | | | | | | | | | | | | | (279) count(all_259_2) = all_259_1 % 18.41/3.40 | | | | | | | | | | | | | (280) remove(5, all_28_0) = all_259_2 % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | BETA: splitting (251) gives: % 18.41/3.40 | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | Case 1: % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | (281) all_70_0 = 0 % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | REDUCE: (163), (281) imply: % 18.41/3.40 | | | | | | | | | | | | | | (282) $false % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | CLOSE: (282) is inconsistent. % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | Case 2: % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | (283) ? [v0: collection] : ? [v1: int] : ? [v2: int] % 18.41/3.40 | | | | | | | | | | | | | | : ( ~ ($difference(v2, v1) = 1) & remove(all_13_1, % 18.41/3.40 | | | | | | | | | | | | | | all_28_0) = v0 & count(v0) = v1 & % 18.41/3.40 | | | | | | | | | | | | | | count(all_28_0) = v2 & collection(v0)) % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | DELTA: instantiating (283) with fresh symbols all_265_0, % 18.41/3.40 | | | | | | | | | | | | | | all_265_1, all_265_2 gives: % 18.41/3.40 | | | | | | | | | | | | | | (284) ~ ($difference(all_265_0, all_265_1) = 1) & % 18.41/3.40 | | | | | | | | | | | | | | remove(all_13_1, all_28_0) = all_265_2 & % 18.41/3.40 | | | | | | | | | | | | | | count(all_265_2) = all_265_1 & count(all_28_0) = % 18.41/3.40 | | | | | | | | | | | | | | all_265_0 & collection(all_265_2) % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | ALPHA: (284) implies: % 18.41/3.40 | | | | | | | | | | | | | | (285) count(all_28_0) = all_265_0 % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | BETA: splitting (252) gives: % 18.41/3.40 | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | Case 1: % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | (286) all_70_0 = 0 % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | REDUCE: (163), (286) imply: % 18.41/3.40 | | | | | | | | | | | | | | | (287) $false % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | CLOSE: (287) is inconsistent. % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | Case 2: % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | (288) ? [v0: collection] : ? [v1: int] : % 18.41/3.40 | | | | | | | | | | | | | | | (remove(all_13_1, all_28_0) = v0 & count(v0) = v1 % 18.41/3.40 | | | | | | | | | | | | | | | & count(all_28_0) = v1 & collection(v0)) % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | DELTA: instantiating (288) with fresh symbols all_285_0, % 18.41/3.40 | | | | | | | | | | | | | | | all_285_1 gives: % 18.41/3.40 | | | | | | | | | | | | | | | (289) remove(all_13_1, all_28_0) = all_285_1 & % 18.41/3.40 | | | | | | | | | | | | | | | count(all_285_1) = all_285_0 & count(all_28_0) = % 18.41/3.40 | | | | | | | | | | | | | | | all_285_0 & collection(all_285_1) % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | ALPHA: (289) implies: % 18.41/3.40 | | | | | | | | | | | | | | | (290) count(all_28_0) = all_285_0 % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | BETA: splitting (245) gives: % 18.41/3.40 | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | Case 1: % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | (291) all_72_0 = 0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | REDUCE: (166), (291) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (292) $false % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | CLOSE: (292) is inconsistent. % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | Case 2: % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_211_0, all_241_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (268), (274) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (293) all_241_0 = all_211_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_213_0, all_259_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (270), (278) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (294) all_259_0 = all_213_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_241_0, all_265_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (274), (285) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (295) all_265_0 = all_241_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with $sum(all_201_0, 1), % 18.41/3.40 | | | | | | | | | | | | | | | | all_265_0, all_28_0, simplifying with (262), (285) % 18.41/3.40 | | | | | | | | | | | | | | | | gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (296) $difference(all_265_0, all_201_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with 1, all_285_0, all_28_0, % 18.41/3.40 | | | | | | | | | | | | | | | | simplifying with (136), (290) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (297) all_285_0 = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_259_0, all_285_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (278), (290) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (298) all_285_0 = all_259_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_253_0, all_285_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (276), (290) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (299) all_285_0 = all_253_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_231_0, all_285_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (272), (290) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (300) all_285_0 = all_231_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_211_0, all_285_0, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (268), (290) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (301) all_285_0 = all_211_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with $sum(all_205_0, 1), % 18.41/3.40 | | | | | | | | | | | | | | | | all_285_0, all_28_0, simplifying with (266), (290) % 18.41/3.40 | | | | | | | | | | | | | | | | gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (302) $difference(all_285_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_201_1, all_259_2, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, 5, simplifying with (264), (280) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (303) all_259_2 = all_201_1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_175_0, all_259_2, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, 5, simplifying with (259), (280) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (304) all_259_2 = all_175_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (298), (299) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (305) all_259_0 = all_253_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (305) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (306) all_259_0 = all_253_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (297), (299) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (307) all_253_0 = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (299), (302) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (308) $difference(all_253_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (299), (301) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (309) all_253_0 = all_211_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (299), (300) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (310) all_253_0 = all_231_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (295), (296) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (311) $difference(all_241_0, all_201_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (311) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (312) $difference(all_241_0, all_201_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (294), (306) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (313) all_253_0 = all_213_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (313) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (314) all_253_0 = all_213_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (303), (304) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (315) all_201_1 = all_175_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (315) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (316) all_201_1 = all_175_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (308), (310) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (317) $difference(all_231_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (310), (314) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (318) all_231_0 = all_213_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (307), (310) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (319) all_231_0 = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (309), (310) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (320) all_231_0 = all_211_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (293), (312) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (321) $difference(all_211_0, all_201_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (321) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (322) $difference(all_211_0, all_201_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (318), (320) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (323) all_213_0 = all_211_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (318), (319) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (324) all_213_0 = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (317), (318) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (325) $difference(all_213_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (323), (325) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (326) $difference(all_211_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (326) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (327) $difference(all_211_0, all_205_0) = 1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (324), (325) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (328) all_205_0 = 0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (322), (327) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (329) all_205_0 = all_201_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | SIMP: (329) implies: % 18.41/3.40 | | | | | | | | | | | | | | | | (330) all_205_0 = all_201_0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | COMBINE_EQS: (328), (330) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (331) all_201_0 = 0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | REDUCE: (279), (304) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (332) count(all_175_0) = all_259_1 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | REDUCE: (263), (316), (331) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (333) count(all_175_0) = 0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | REDUCE: (261), (316) imply: % 18.41/3.40 | | | | | | | | | | | | | | | | (334) collection(all_175_0) % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with 0, all_259_1, all_175_0, % 18.41/3.40 | | | | | | | | | | | | | | | | simplifying with (332), (333) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (335) all_259_1 = 0 % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_175_0, simplifying with % 18.41/3.40 | | | | | | | | | | | | | | | | (333), (334) gives: % 18.41/3.40 | | | | | | | | | | | | | | | | (336) all_175_0 = empty % 18.41/3.40 | | | | | | | | | | | | | | | | % 18.41/3.40 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_13_0, all_175_0, 5, % 18.41/3.40 | | | | | | | | | | | | | | | | all_28_0, simplifying with (180), (258), (334) % 18.41/3.40 | | | | | | | | | | | | | | | | gives: % 18.41/3.41 | | | | | | | | | | | | | | | | (337) all_13_0 = 5 | in(all_13_0, all_175_0) = 0 % 18.41/3.41 | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | BETA: splitting (337) gives: % 18.41/3.41 | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | Case 1: % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | (338) in(all_13_0, all_175_0) = 0 % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | REDUCE: (336), (338) imply: % 18.41/3.41 | | | | | | | | | | | | | | | | | (339) in(all_13_0, empty) = 0 % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with all_13_0, simplifying with % 18.41/3.41 | | | | | | | | | | | | | | | | | (339) gives: % 18.41/3.41 | | | | | | | | | | | | | | | | | (340) $false % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | CLOSE: (340) is inconsistent. % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | Case 2: % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | (341) all_13_0 = 5 % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | REDUCE: (21), (341) imply: % 18.41/3.41 | | | | | | | | | | | | | | | | | (342) $false % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | | CLOSE: (342) is inconsistent. % 18.41/3.41 | | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | Case 2: % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | (343) ~ ($difference(all_81_1, all_81_2) = -1) & % 18.41/3.41 | | | | | | | | | | | | | count(all_26_0) = all_81_1 & count(all_13_2) = % 18.41/3.41 | | | | | | | | | | | | | all_81_2 % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | ALPHA: (343) implies: % 18.41/3.41 | | | | | | | | | | | | | (344) ~ ($difference(all_81_1, all_81_2) = -1) % 18.41/3.41 | | | | | | | | | | | | | (345) count(all_13_2) = all_81_2 % 18.41/3.41 | | | | | | | | | | | | | (346) count(all_26_0) = all_81_1 % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | GROUND_INST: instantiating (16) with 2, all_81_2, all_13_2, % 18.41/3.41 | | | | | | | | | | | | | simplifying with (26), (345) gives: % 18.41/3.41 | | | | | | | | | | | | | (347) all_81_2 = 2 % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | GROUND_INST: instantiating (16) with 1, all_81_1, all_26_0, % 18.41/3.41 | | | | | | | | | | | | | simplifying with (226), (346) gives: % 18.41/3.41 | | | | | | | | | | | | | (348) all_81_1 = 1 % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | REDUCE: (344), (347), (348) imply: % 18.41/3.41 | | | | | | | | | | | | | (349) $false % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | | CLOSE: (349) is inconsistent. % 18.41/3.41 | | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | Case 2: % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | (350) ~ ($difference(all_82_1, all_82_2) = -1) & % 18.41/3.41 | | | | | | | | | | | count(all_28_0) = all_82_1 & count(all_13_2) = % 18.41/3.41 | | | | | | | | | | | all_82_2 % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | ALPHA: (350) implies: % 18.41/3.41 | | | | | | | | | | | (351) ~ ($difference(all_82_1, all_82_2) = -1) % 18.41/3.41 | | | | | | | | | | | (352) count(all_13_2) = all_82_2 % 18.41/3.41 | | | | | | | | | | | (353) count(all_28_0) = all_82_1 % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | GROUND_INST: instantiating (16) with 2, all_82_2, all_13_2, % 18.41/3.41 | | | | | | | | | | | simplifying with (26), (352) gives: % 18.41/3.41 | | | | | | | | | | | (354) all_82_2 = 2 % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | GROUND_INST: instantiating (16) with 1, all_82_1, all_28_0, % 18.41/3.41 | | | | | | | | | | | simplifying with (136), (353) gives: % 18.41/3.41 | | | | | | | | | | | (355) all_82_1 = 1 % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | REDUCE: (351), (354), (355) imply: % 18.41/3.41 | | | | | | | | | | | (356) $false % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | | CLOSE: (356) is inconsistent. % 18.41/3.41 | | | | | | | | | | | % 18.41/3.41 | | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | | % 18.41/3.41 | | | | | | | | | End of split % 18.41/3.41 | | | | | | | | | % 18.41/3.41 | | | | | | | | Case 2: % 18.41/3.41 | | | | | | | | | % 18.41/3.41 | | | | | | | | | (357) all_79_2 = 0 & in(5, all_26_0) = 0 % 18.41/3.41 | | | | | | | | | % 18.41/3.41 | | | | | | | | | ALPHA: (357) implies: % 18.41/3.41 | | | | | | | | | (358) in(5, all_26_0) = 0 % 18.41/3.41 | | | | | | | | | % 18.41/3.41 | | | | | | | | | REF_CLOSE: (17), (166), (167), (358) are inconsistent by % 18.41/3.41 | | | | | | | | | sub-proof #2. % 18.41/3.41 | | | | | | | | | % 18.41/3.41 | | | | | | | | End of split % 18.41/3.41 | | | | | | | | % 18.41/3.41 | | | | | | | End of split % 18.41/3.41 | | | | | | | % 18.41/3.41 | | | | | | Case 2: % 18.41/3.41 | | | | | | | % 18.41/3.41 | | | | | | | (359) all_77_2 = 0 & in(all_13_0, all_24_0) = 0 % 18.41/3.41 | | | | | | | % 18.41/3.41 | | | | | | | ALPHA: (359) implies: % 18.41/3.41 | | | | | | | (360) in(all_13_0, all_24_0) = 0 % 18.41/3.41 | | | | | | | % 18.41/3.41 | | | | | | | REF_CLOSE: (16), (17), (26), (137), (160), (161), (172), (360) are % 18.41/3.41 | | | | | | | inconsistent by sub-proof #3. % 18.41/3.41 | | | | | | | % 18.41/3.41 | | | | | | End of split % 18.41/3.41 | | | | | | % 18.41/3.41 | | | | | Case 2: % 18.41/3.41 | | | | | | % 18.41/3.41 | | | | | | (361) all_75_2 = 0 & in(all_13_1, all_28_0) = 0 % 18.41/3.41 | | | | | | % 18.41/3.41 | | | | | | ALPHA: (361) implies: % 18.41/3.41 | | | | | | (362) in(all_13_1, all_28_0) = 0 % 18.41/3.41 | | | | | | % 18.41/3.41 | | | | | | REF_CLOSE: (17), (163), (164), (188), (362) are inconsistent by % 18.41/3.41 | | | | | | sub-proof #1. % 18.41/3.41 | | | | | | % 18.41/3.41 | | | | | End of split % 18.41/3.41 | | | | | % 18.41/3.41 | | | | End of split % 18.41/3.41 | | | | % 18.41/3.41 | | | End of split % 18.41/3.41 | | | % 18.41/3.41 | | Case 2: % 18.41/3.41 | | | % 18.41/3.41 | | | (363) all_13_0 = all_13_1 % 18.41/3.41 | | | % 18.41/3.41 | | | REDUCE: (21), (363) imply: % 18.41/3.41 | | | (364) $lesseq(7, all_13_1) % 18.41/3.41 | | | % 18.41/3.41 | | | COMBINE_INEQS: (20), (364) imply: % 18.41/3.41 | | | (365) $false % 18.41/3.41 | | | % 18.41/3.41 | | | CLOSE: (365) is inconsistent. % 18.41/3.41 | | | % 18.41/3.41 | | End of split % 18.41/3.41 | | % 18.41/3.41 | Case 2: % 18.41/3.41 | | % 18.41/3.41 | | (366) all_13_1 = 5 % 18.41/3.41 | | % 18.41/3.41 | | REDUCE: (20), (366) imply: % 18.41/3.41 | | (367) $false % 18.41/3.41 | | % 18.41/3.41 | | CLOSE: (367) is inconsistent. % 18.41/3.41 | | % 18.41/3.41 | End of split % 18.41/3.41 | % 18.41/3.41 End of proof % 18.41/3.41 % 18.41/3.41 Sub-proof #1 shows that the following formulas are inconsistent: % 18.41/3.41 ---------------------------------------------------------------- % 18.41/3.41 (1) ~ (all_70_0 = 0) % 18.41/3.41 (2) in(all_13_1, all_28_0) = all_74_2 % 18.41/3.41 (3) in(all_13_1, all_28_0) = all_70_0 % 18.41/3.41 (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 18.41/3.41 collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 18.41/3.41 (in(v3, v2) = v0)) % 18.41/3.41 (5) in(all_13_1, all_28_0) = 0 % 18.41/3.41 % 18.41/3.41 Begin of proof % 18.41/3.41 | % 18.41/3.41 | GROUND_INST: instantiating (4) with all_70_0, all_74_2, all_28_0, all_13_1, % 18.41/3.41 | simplifying with (2), (3) gives: % 18.41/3.41 | (6) all_74_2 = all_70_0 % 18.41/3.41 | % 18.41/3.41 | GROUND_INST: instantiating (4) with 0, all_74_2, all_28_0, all_13_1, % 18.41/3.41 | simplifying with (2), (5) gives: % 18.41/3.41 | (7) all_74_2 = 0 % 18.41/3.41 | % 18.41/3.41 | COMBINE_EQS: (6), (7) imply: % 18.41/3.41 | (8) all_70_0 = 0 % 18.41/3.41 | % 18.41/3.41 | SIMP: (8) implies: % 18.41/3.41 | (9) all_70_0 = 0 % 18.41/3.41 | % 18.41/3.41 | REDUCE: (1), (9) imply: % 18.41/3.41 | (10) $false % 18.41/3.41 | % 18.41/3.41 | CLOSE: (10) is inconsistent. % 18.41/3.41 | % 18.41/3.41 End of proof % 18.41/3.41 % 18.41/3.41 Sub-proof #2 shows that the following formulas are inconsistent: % 18.41/3.41 ---------------------------------------------------------------- % 18.41/3.41 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 18.41/3.41 collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 18.41/3.41 (in(v3, v2) = v0)) % 18.41/3.41 (2) in(5, all_26_0) = all_72_0 % 18.41/3.41 (3) in(5, all_26_0) = 0 % 18.41/3.41 (4) ~ (all_72_0 = 0) % 18.41/3.41 % 18.41/3.41 Begin of proof % 18.41/3.41 | % 18.41/3.41 | GROUND_INST: instantiating (1) with 0, all_72_0, all_26_0, 5, simplifying with % 18.41/3.41 | (2), (3) gives: % 18.41/3.41 | (5) all_72_0 = 0 % 18.41/3.41 | % 18.41/3.41 | REDUCE: (4), (5) imply: % 18.41/3.41 | (6) $false % 18.41/3.41 | % 18.41/3.41 | CLOSE: (6) is inconsistent. % 18.41/3.41 | % 18.41/3.41 End of proof % 18.41/3.41 % 18.41/3.41 Sub-proof #3 shows that the following formulas are inconsistent: % 18.41/3.41 ---------------------------------------------------------------- % 18.41/3.41 (1) in(all_13_0, all_24_0) = all_68_0 % 18.41/3.41 (2) count(all_24_0) = 1 % 18.41/3.41 (3) in(all_13_0, all_24_0) = 0 % 18.41/3.41 (4) ~ (all_68_0 = 0) % 18.41/3.41 (5) count(all_13_2) = 2 % 18.41/3.41 (6) (all_78_0 = all_78_1 & count(all_24_0) = all_78_1 & count(all_13_2) = % 18.41/3.41 all_78_1) | ( ~ (all_78_2 = 0) & in(all_13_0, all_24_0) = all_78_2) % 18.41/3.41 (7) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 18.41/3.41 collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 18.41/3.41 (in(v3, v2) = v0)) % 18.41/3.41 (8) ! [v0: int] : ! [v1: int] : ! [v2: collection] : (v1 = v0 | ~ % 18.41/3.41 (count(v2) = v1) | ~ (count(v2) = v0)) % 18.41/3.41 % 18.41/3.41 Begin of proof % 18.41/3.41 | % 18.41/3.41 | BETA: splitting (6) gives: % 18.41/3.41 | % 18.41/3.41 | Case 1: % 18.41/3.41 | | % 18.41/3.42 | | (9) all_78_0 = all_78_1 & count(all_24_0) = all_78_1 & count(all_13_2) = % 18.41/3.42 | | all_78_1 % 18.41/3.42 | | % 18.41/3.42 | | ALPHA: (9) implies: % 18.41/3.42 | | (10) count(all_13_2) = all_78_1 % 18.41/3.42 | | (11) count(all_24_0) = all_78_1 % 18.41/3.42 | | % 18.41/3.42 | | GROUND_INST: instantiating (8) with 2, all_78_1, all_13_2, simplifying with % 18.41/3.42 | | (5), (10) gives: % 18.41/3.42 | | (12) all_78_1 = 2 % 18.41/3.42 | | % 18.41/3.42 | | GROUND_INST: instantiating (8) with 1, all_78_1, all_24_0, simplifying with % 18.41/3.42 | | (2), (11) gives: % 18.41/3.42 | | (13) all_78_1 = 1 % 18.41/3.42 | | % 18.41/3.42 | | COMBINE_EQS: (12), (13) imply: % 18.41/3.42 | | (14) $false % 18.41/3.42 | | % 18.41/3.42 | | CLOSE: (14) is inconsistent. % 18.41/3.42 | | % 18.41/3.42 | Case 2: % 18.41/3.42 | | % 18.41/3.42 | | (15) ~ (all_78_2 = 0) & in(all_13_0, all_24_0) = all_78_2 % 18.41/3.42 | | % 18.41/3.42 | | ALPHA: (15) implies: % 18.41/3.42 | | (16) in(all_13_0, all_24_0) = all_78_2 % 18.41/3.42 | | % 18.41/3.42 | | GROUND_INST: instantiating (7) with all_68_0, all_78_2, all_24_0, all_13_0, % 18.41/3.42 | | simplifying with (1), (16) gives: % 18.41/3.42 | | (17) all_78_2 = all_68_0 % 18.41/3.42 | | % 18.41/3.42 | | GROUND_INST: instantiating (7) with 0, all_78_2, all_24_0, all_13_0, % 18.41/3.42 | | simplifying with (3), (16) gives: % 18.41/3.42 | | (18) all_78_2 = 0 % 18.41/3.42 | | % 18.41/3.42 | | COMBINE_EQS: (17), (18) imply: % 18.41/3.42 | | (19) all_68_0 = 0 % 18.41/3.42 | | % 18.41/3.42 | | SIMP: (19) implies: % 18.41/3.42 | | (20) all_68_0 = 0 % 18.41/3.42 | | % 18.41/3.42 | | REDUCE: (4), (20) imply: % 18.41/3.42 | | (21) $false % 18.41/3.42 | | % 18.41/3.42 | | CLOSE: (21) is inconsistent. % 18.41/3.42 | | % 18.41/3.42 | End of split % 18.41/3.42 | % 18.41/3.42 End of proof % 18.41/3.42 % SZS output end Proof for theBenchmark % 18.41/3.42 % 18.41/3.42 2802ms %------------------------------------------------------------------------------