%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : DAT050_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 : n024.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:19:01 EDT 2023 % Result : Theorem 8.52s 1.84s % Output : Proof 13.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : DAT050_1 : TPTP v8.1.2. Released v5.0.0. % 0.06/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Aug 24 14:01:39 EDT 2023 % 0.12/0.33 % CPUTime : % 0.19/0.59 ________ _____ % 0.19/0.59 ___ __ \_________(_)________________________________ % 0.19/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.59 % 0.19/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.59 (2023-06-19) % 0.19/0.59 % 0.19/0.59 (c) Philipp Rümmer, 2009-2023 % 0.19/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.59 Amanda Stjerna. % 0.19/0.59 Free software under BSD-3-Clause. % 0.19/0.59 % 0.19/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.59 % 0.19/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.60 Running up to 7 provers in parallel. % 0.19/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.48/1.03 Prover 1: Preprocessing ... % 2.48/1.03 Prover 4: Preprocessing ... % 2.97/1.07 Prover 6: Preprocessing ... % 2.97/1.07 Prover 0: Preprocessing ... % 2.97/1.07 Prover 5: Preprocessing ... % 2.97/1.07 Prover 3: Preprocessing ... % 2.97/1.07 Prover 2: Preprocessing ... % 4.32/1.34 Prover 6: Constructing countermodel ... % 4.32/1.34 Prover 5: Proving ... % 4.32/1.35 Prover 1: Constructing countermodel ... % 4.32/1.35 Prover 3: Constructing countermodel ... % 4.74/1.39 Prover 0: Proving ... % 4.74/1.39 Prover 2: Proving ... % 4.74/1.39 Prover 4: Constructing countermodel ... % 8.52/1.84 Prover 3: proved (1223ms) % 8.52/1.84 % 8.52/1.84 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.52/1.84 % 8.52/1.84 Prover 6: stopped % 8.52/1.84 Prover 2: stopped % 8.52/1.84 Prover 5: stopped % 8.52/1.85 Prover 0: stopped % 8.52/1.86 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.52/1.86 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.52/1.86 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 8.52/1.86 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.52/1.86 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 9.06/1.89 Prover 8: Preprocessing ... % 9.06/1.90 Prover 13: Preprocessing ... % 9.06/1.91 Prover 7: Preprocessing ... % 9.06/1.91 Prover 10: Preprocessing ... % 9.06/1.91 Prover 11: Preprocessing ... % 9.06/1.95 Prover 8: Warning: ignoring some quantifiers % 9.06/1.95 Prover 8: Constructing countermodel ... % 9.06/1.97 Prover 10: Constructing countermodel ... % 9.06/1.97 Prover 13: Warning: ignoring some quantifiers % 9.06/1.98 Prover 11: Constructing countermodel ... % 9.06/1.99 Prover 13: Constructing countermodel ... % 9.06/1.99 Prover 7: Constructing countermodel ... % 11.99/2.33 Prover 1: Found proof (size 405) % 11.99/2.34 Prover 1: proved (1725ms) % 11.99/2.34 Prover 4: stopped % 11.99/2.34 Prover 7: stopped % 11.99/2.34 Prover 13: stopped % 11.99/2.34 Prover 8: stopped % 11.99/2.34 Prover 11: stopped % 11.99/2.34 Prover 10: stopped % 11.99/2.34 % 11.99/2.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.99/2.34 % 12.86/2.44 % SZS output start Proof for theBenchmark % 12.86/2.44 Assumptions after simplification: % 12.86/2.44 --------------------------------- % 12.86/2.45 % 12.86/2.45 (ax2) % 12.86/2.46 collection(empty) & ! [v0: int] : ! [v1: collection] : ! [v2: collection] : % 12.86/2.46 ! [v3: int] : (v3 = 0 | ~ (add(v0, v1) = v2) | ~ (in(v0, v2) = v3) | ~ % 12.86/2.46 collection(v1)) & ! [v0: collection] : (v0 = empty | ~ (count(v0) = 0) | % 12.86/2.46 ~ collection(v0)) & ! [v0: int] : (v0 = 0 | ~ (count(empty) = v0)) % 12.86/2.46 % 12.86/2.46 (ax3) % 12.86/2.47 ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) % 12.86/2.47 = v2) | ~ (in(v0, v2) = 0) | ~ collection(v1)) & ! [v0: int] : ! [v1: % 12.86/2.47 collection] : ! [v2: collection] : ( ~ (add(v0, v1) = v2) | ~ % 12.86/2.47 collection(v1) | ? [v3: any] : ? [v4: int] : ? [v5: int] : (count(v2) = % 12.86/2.47 v4 & count(v1) = v5 & in(v0, v1) = v3 & ($difference(v5, v4) = -1 | v3 = % 12.86/2.47 0))) & ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 12.86/2.47 (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 12.86/2.47 [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, v1) = v5 & ( ~ (v5 = % 12.86/2.47 0) | ~ ($difference(v4, v3) = -1)))) % 12.86/2.47 % 12.86/2.47 (ax4) % 12.86/2.47 ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ! % 12.86/2.47 [v4: int] : (v4 = 0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = v4) | ~ % 12.86/2.47 collection(v1) | ( ~ (v2 = v0) & ? [v5: int] : ( ~ (v5 = 0) & in(v0, v1) = % 12.86/2.47 v5))) & ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: % 12.86/2.47 collection] : (v2 = v0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ % 12.86/2.47 collection(v1) | in(v0, v1) = 0) & ! [v0: int] : ! [v1: collection] : ! % 12.86/2.47 [v2: collection] : ( ~ (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: any] : % 12.86/2.47 ? [v4: int] : ? [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, v1) % 12.86/2.47 = v3 & ( ~ (v3 = 0) | v5 = v4))) & ! [v0: int] : ! [v1: collection] : ! % 12.86/2.47 [v2: collection] : ( ~ (add(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : % 12.86/2.47 ? [v4: int] : ? [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, v1) % 12.86/2.47 = v5 & ( ~ (v4 = v3) | v5 = 0))) % 12.86/2.47 % 12.86/2.47 (ax5) % 12.86/2.48 ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ! % 12.86/2.48 [v4: int] : (v4 = 0 | v2 = v0 | ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = % 12.86/2.48 v4) | ~ collection(v1) | ? [v5: int] : ( ~ (v5 = 0) & in(v0, v1) = v5)) % 12.86/2.48 & ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : ( % 12.86/2.48 ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ collection(v1) | ( ~ (v2 % 12.86/2.48 = v0) & in(v0, v1) = 0)) & ! [v0: int] : ! [v1: collection] : ! [v2: % 12.86/2.48 collection] : ( ~ (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: any] : % 12.86/2.48 ? [v4: int] : ? [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, v1) % 12.86/2.48 = v3 & ( ~ (v3 = 0) | $difference(v5, v4) = 1))) & ! [v0: int] : ! [v1: % 12.86/2.48 collection] : ! [v2: collection] : ( ~ (remove(v0, v1) = v2) | ~ % 12.86/2.48 collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: any] : (count(v2) = % 12.86/2.48 v3 & count(v1) = v4 & in(v0, v1) = v5 & ( ~ ($difference(v4, v3) = 1) | v5 % 12.86/2.48 = 0))) % 12.86/2.48 % 12.86/2.48 (ax6) % 12.86/2.48 ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) % 12.86/2.48 = v2) | ~ collection(v1) | ? [v3: any] : ? [v4: int] : ? [v5: int] : % 12.86/2.48 (count(v2) = v4 & count(v1) = v5 & in(v0, v1) = v3 & (v5 = v4 | v3 = 0))) & % 12.86/2.48 ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (remove(v0, v1) % 12.86/2.48 = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? [v5: any] : % 12.86/2.48 (count(v2) = v3 & count(v1) = v4 & in(v0, v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = % 12.86/2.48 v3)))) % 12.86/2.48 % 12.86/2.48 (co1) % 12.86/2.48 ? [v0: collection] : ? [v1: int] : ? [v2: collection] : ? [v3: collection] % 12.86/2.48 : ? [v4: collection] : ? [v5: int] : ? [v6: collection] : ? [v7: % 12.86/2.48 collection] : ? [v8: int] : ( ~ (v8 = v5) & remove(v1, v2) = v3 & % 12.86/2.48 remove(v1, v0) = v6 & add(v1, v0) = v2 & add(0, v6) = v7 & add(0, v3) = v4 & % 12.86/2.48 count(v7) = v8 & count(v4) = v5 & collection(v7) & collection(v6) & % 12.86/2.48 collection(v4) & collection(v3) & collection(v2) & collection(v0)) % 12.86/2.48 % 12.86/2.48 (function-axioms) % 12.86/2.49 ! [v0: collection] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] % 12.86/2.49 : (v1 = v0 | ~ (remove(v3, v2) = v1) | ~ (remove(v3, v2) = v0)) & ! [v0: % 12.86/2.49 collection] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] : (v1 % 12.86/2.49 = v0 | ~ (add(v3, v2) = v1) | ~ (add(v3, v2) = v0)) & ! [v0: % 12.86/2.49 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: collection] : ! % 12.86/2.49 [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0: % 12.86/2.49 int] : ! [v1: int] : ! [v2: collection] : (v1 = v0 | ~ (count(v2) = v1) | % 12.86/2.49 ~ (count(v2) = v0)) % 12.86/2.49 % 12.86/2.49 Further assumptions not needed in the proof: % 12.86/2.49 -------------------------------------------- % 12.86/2.49 ax1, ax7 % 12.86/2.49 % 12.86/2.49 Those formulas are unsatisfiable: % 12.86/2.49 --------------------------------- % 12.86/2.49 % 12.86/2.49 Begin of proof % 12.86/2.49 | % 12.86/2.49 | ALPHA: (ax2) implies: % 12.86/2.49 | (1) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ! [v3: int] % 12.86/2.49 | : (v3 = 0 | ~ (add(v0, v1) = v2) | ~ (in(v0, v2) = v3) | ~ % 12.86/2.49 | collection(v1)) % 12.86/2.49 | % 12.86/2.49 | ALPHA: (ax3) implies: % 12.86/2.49 | (2) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 12.86/2.49 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 12.86/2.49 | [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, v1) = v5 & ( ~ % 12.86/2.49 | (v5 = 0) | ~ ($difference(v4, v3) = -1)))) % 12.86/2.49 | (3) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 12.86/2.49 | v1) = v2) | ~ collection(v1) | ? [v3: any] : ? [v4: int] : ? % 12.86/2.49 | [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, v1) = v3 & % 12.86/2.49 | ($difference(v5, v4) = -1 | v3 = 0))) % 12.86/2.49 | % 12.86/2.49 | ALPHA: (ax4) implies: % 12.86/2.49 | (4) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 12.86/2.49 | v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: int] : ? % 12.86/2.49 | [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, v1) = v5 & ( ~ % 12.86/2.49 | (v4 = v3) | v5 = 0))) % 12.86/2.49 | (5) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ (add(v0, % 12.86/2.49 | v1) = v2) | ~ collection(v1) | ? [v3: any] : ? [v4: int] : ? % 12.86/2.49 | [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, v1) = v3 & ( ~ % 12.86/2.50 | (v3 = 0) | v5 = v4))) % 12.86/2.50 | (6) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] % 12.86/2.50 | : (v2 = v0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ % 12.86/2.50 | collection(v1) | in(v0, v1) = 0) % 12.86/2.50 | (7) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] % 12.86/2.50 | : ! [v4: int] : (v4 = 0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = v4) % 12.86/2.50 | | ~ collection(v1) | ( ~ (v2 = v0) & ? [v5: int] : ( ~ (v5 = 0) & % 12.86/2.50 | in(v0, v1) = v5))) % 12.86/2.50 | % 12.86/2.50 | ALPHA: (ax5) implies: % 12.86/2.50 | (8) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 12.86/2.50 | (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: % 12.86/2.50 | int] : ? [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, v1) % 12.86/2.50 | = v5 & ( ~ ($difference(v4, v3) = 1) | v5 = 0))) % 12.86/2.50 | (9) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 12.86/2.50 | (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: any] : ? [v4: % 12.86/2.50 | int] : ? [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, v1) % 12.86/2.50 | = v3 & ( ~ (v3 = 0) | $difference(v5, v4) = 1))) % 12.86/2.50 | (10) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: % 12.86/2.50 | collection] : ( ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ % 12.86/2.50 | collection(v1) | ( ~ (v2 = v0) & in(v0, v1) = 0)) % 12.86/2.50 | (11) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: % 12.86/2.50 | collection] : ! [v4: int] : (v4 = 0 | v2 = v0 | ~ (remove(v2, v1) % 12.86/2.50 | = v3) | ~ (in(v0, v3) = v4) | ~ collection(v1) | ? [v5: int] : % 12.86/2.50 | ( ~ (v5 = 0) & in(v0, v1) = v5)) % 12.86/2.50 | % 12.86/2.50 | ALPHA: (ax6) implies: % 12.86/2.50 | (12) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 12.86/2.50 | (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: int] : ? [v4: % 12.86/2.50 | int] : ? [v5: any] : (count(v2) = v3 & count(v1) = v4 & in(v0, % 12.86/2.50 | v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = v3)))) % 12.86/2.50 | (13) ! [v0: int] : ! [v1: collection] : ! [v2: collection] : ( ~ % 12.86/2.50 | (remove(v0, v1) = v2) | ~ collection(v1) | ? [v3: any] : ? [v4: % 12.86/2.50 | int] : ? [v5: int] : (count(v2) = v4 & count(v1) = v5 & in(v0, % 12.86/2.50 | v1) = v3 & (v5 = v4 | v3 = 0))) % 12.86/2.50 | % 12.86/2.50 | ALPHA: (function-axioms) implies: % 12.86/2.50 | (14) ! [v0: int] : ! [v1: int] : ! [v2: collection] : (v1 = v0 | ~ % 12.86/2.50 | (count(v2) = v1) | ~ (count(v2) = v0)) % 12.86/2.50 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 12.86/2.50 | collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 12.86/2.50 | (in(v3, v2) = v0)) % 12.86/2.50 | % 12.86/2.50 | DELTA: instantiating (co1) with fresh symbols all_13_0, all_13_1, all_13_2, % 12.86/2.50 | all_13_3, all_13_4, all_13_5, all_13_6, all_13_7, all_13_8 gives: % 12.86/2.50 | (16) ~ (all_13_0 = all_13_3) & remove(all_13_7, all_13_6) = all_13_5 & % 12.86/2.50 | remove(all_13_7, all_13_8) = all_13_2 & add(all_13_7, all_13_8) = % 12.86/2.50 | all_13_6 & add(0, all_13_2) = all_13_1 & add(0, all_13_5) = all_13_4 & % 12.86/2.50 | count(all_13_1) = all_13_0 & count(all_13_4) = all_13_3 & % 12.86/2.50 | collection(all_13_1) & collection(all_13_2) & collection(all_13_4) & % 12.86/2.50 | collection(all_13_5) & collection(all_13_6) & collection(all_13_8) % 12.86/2.50 | % 12.86/2.50 | ALPHA: (16) implies: % 12.86/2.51 | (17) ~ (all_13_0 = all_13_3) % 12.86/2.51 | (18) collection(all_13_8) % 12.86/2.51 | (19) collection(all_13_6) % 12.86/2.51 | (20) collection(all_13_5) % 12.86/2.51 | (21) collection(all_13_2) % 12.86/2.51 | (22) count(all_13_4) = all_13_3 % 12.86/2.51 | (23) count(all_13_1) = all_13_0 % 12.86/2.51 | (24) add(0, all_13_5) = all_13_4 % 12.86/2.51 | (25) add(0, all_13_2) = all_13_1 % 12.86/2.51 | (26) add(all_13_7, all_13_8) = all_13_6 % 12.86/2.51 | (27) remove(all_13_7, all_13_8) = all_13_2 % 12.86/2.51 | (28) remove(all_13_7, all_13_6) = all_13_5 % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (5) with 0, all_13_5, all_13_4, simplifying with % 12.86/2.51 | (20), (24) gives: % 12.86/2.51 | (29) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_4) = v1 & % 12.86/2.51 | count(all_13_5) = v2 & in(0, all_13_5) = v0 & ( ~ (v0 = 0) | v2 = % 12.86/2.51 | v1)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (3) with 0, all_13_5, all_13_4, simplifying with % 12.86/2.51 | (20), (24) gives: % 12.86/2.51 | (30) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_4) = v1 & % 12.86/2.51 | count(all_13_5) = v2 & in(0, all_13_5) = v0 & ($difference(v2, v1) = % 12.86/2.51 | -1 | v0 = 0)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (2) with 0, all_13_5, all_13_4, simplifying with % 12.86/2.51 | (20), (24) gives: % 12.86/2.51 | (31) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_4) = v0 & % 12.86/2.51 | count(all_13_5) = v1 & in(0, all_13_5) = v2 & ( ~ (v2 = 0) | ~ % 12.86/2.51 | ($difference(v1, v0) = -1))) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (4) with 0, all_13_5, all_13_4, simplifying with % 12.86/2.51 | (20), (24) gives: % 12.86/2.51 | (32) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_4) = v0 & % 12.86/2.51 | count(all_13_5) = v1 & in(0, all_13_5) = v2 & ( ~ (v1 = v0) | v2 = % 12.86/2.51 | 0)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (5) with 0, all_13_2, all_13_1, simplifying with % 12.86/2.51 | (21), (25) gives: % 12.86/2.51 | (33) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_1) = v1 & % 12.86/2.51 | count(all_13_2) = v2 & in(0, all_13_2) = v0 & ( ~ (v0 = 0) | v2 = % 12.86/2.51 | v1)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (3) with 0, all_13_2, all_13_1, simplifying with % 12.86/2.51 | (21), (25) gives: % 12.86/2.51 | (34) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_1) = v1 & % 12.86/2.51 | count(all_13_2) = v2 & in(0, all_13_2) = v0 & ($difference(v2, v1) = % 12.86/2.51 | -1 | v0 = 0)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (2) with 0, all_13_2, all_13_1, simplifying with % 12.86/2.51 | (21), (25) gives: % 12.86/2.51 | (35) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_1) = v0 & % 12.86/2.51 | count(all_13_2) = v1 & in(0, all_13_2) = v2 & ( ~ (v2 = 0) | ~ % 12.86/2.51 | ($difference(v1, v0) = -1))) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (4) with 0, all_13_2, all_13_1, simplifying with % 12.86/2.51 | (21), (25) gives: % 12.86/2.51 | (36) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_1) = v0 & % 12.86/2.51 | count(all_13_2) = v1 & in(0, all_13_2) = v2 & ( ~ (v1 = v0) | v2 = % 12.86/2.51 | 0)) % 12.86/2.51 | % 12.86/2.51 | GROUND_INST: instantiating (5) with all_13_7, all_13_8, all_13_6, simplifying % 12.86/2.51 | with (18), (26) gives: % 12.86/2.52 | (37) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_6) = v1 & % 12.86/2.52 | count(all_13_8) = v2 & in(all_13_7, all_13_8) = v0 & ( ~ (v0 = 0) | % 12.86/2.52 | v2 = v1)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (3) with all_13_7, all_13_8, all_13_6, simplifying % 12.86/2.52 | with (18), (26) gives: % 12.86/2.52 | (38) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_6) = v1 & % 12.86/2.52 | count(all_13_8) = v2 & in(all_13_7, all_13_8) = v0 & % 12.86/2.52 | ($difference(v2, v1) = -1 | v0 = 0)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (2) with all_13_7, all_13_8, all_13_6, simplifying % 12.86/2.52 | with (18), (26) gives: % 12.86/2.52 | (39) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_6) = v0 & % 12.86/2.52 | count(all_13_8) = v1 & in(all_13_7, all_13_8) = v2 & ( ~ (v2 = 0) | % 12.86/2.52 | ~ ($difference(v1, v0) = -1))) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (4) with all_13_7, all_13_8, all_13_6, simplifying % 12.86/2.52 | with (18), (26) gives: % 12.86/2.52 | (40) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_6) = v0 & % 12.86/2.52 | count(all_13_8) = v1 & in(all_13_7, all_13_8) = v2 & ( ~ (v1 = v0) | % 12.86/2.52 | v2 = 0)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (9) with all_13_7, all_13_8, all_13_2, simplifying % 12.86/2.52 | with (18), (27) gives: % 12.86/2.52 | (41) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_2) = v1 & % 12.86/2.52 | count(all_13_8) = v2 & in(all_13_7, all_13_8) = v0 & ( ~ (v0 = 0) | % 12.86/2.52 | $difference(v2, v1) = 1)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (13) with all_13_7, all_13_8, all_13_2, simplifying % 12.86/2.52 | with (18), (27) gives: % 12.86/2.52 | (42) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_2) = v1 & % 12.86/2.52 | count(all_13_8) = v2 & in(all_13_7, all_13_8) = v0 & (v2 = v1 | v0 = % 12.86/2.52 | 0)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (12) with all_13_7, all_13_8, all_13_2, simplifying % 12.86/2.52 | with (18), (27) gives: % 12.86/2.52 | (43) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_2) = v0 & % 12.86/2.52 | count(all_13_8) = v1 & in(all_13_7, all_13_8) = v2 & ( ~ (v2 = 0) | % 12.86/2.52 | ~ (v1 = v0))) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (8) with all_13_7, all_13_8, all_13_2, simplifying % 12.86/2.52 | with (18), (27) gives: % 12.86/2.52 | (44) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_2) = v0 & % 12.86/2.52 | count(all_13_8) = v1 & in(all_13_7, all_13_8) = v2 & ( ~ % 12.86/2.52 | ($difference(v1, v0) = 1) | v2 = 0)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (9) with all_13_7, all_13_6, all_13_5, simplifying % 12.86/2.52 | with (19), (28) gives: % 12.86/2.52 | (45) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_5) = v1 & % 12.86/2.52 | count(all_13_6) = v2 & in(all_13_7, all_13_6) = v0 & ( ~ (v0 = 0) | % 12.86/2.52 | $difference(v2, v1) = 1)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (13) with all_13_7, all_13_6, all_13_5, simplifying % 12.86/2.52 | with (19), (28) gives: % 12.86/2.52 | (46) ? [v0: any] : ? [v1: int] : ? [v2: int] : (count(all_13_5) = v1 & % 12.86/2.52 | count(all_13_6) = v2 & in(all_13_7, all_13_6) = v0 & (v2 = v1 | v0 = % 12.86/2.52 | 0)) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (12) with all_13_7, all_13_6, all_13_5, simplifying % 12.86/2.52 | with (19), (28) gives: % 12.86/2.52 | (47) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_5) = v0 & % 12.86/2.52 | count(all_13_6) = v1 & in(all_13_7, all_13_6) = v2 & ( ~ (v2 = 0) | % 12.86/2.52 | ~ (v1 = v0))) % 12.86/2.52 | % 12.86/2.52 | GROUND_INST: instantiating (8) with all_13_7, all_13_6, all_13_5, simplifying % 12.86/2.52 | with (19), (28) gives: % 12.86/2.53 | (48) ? [v0: int] : ? [v1: int] : ? [v2: any] : (count(all_13_5) = v0 & % 12.86/2.53 | count(all_13_6) = v1 & in(all_13_7, all_13_6) = v2 & ( ~ % 12.86/2.53 | ($difference(v1, v0) = 1) | v2 = 0)) % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (34) with fresh symbols all_22_0, all_22_1, all_22_2 % 12.86/2.53 | gives: % 12.86/2.53 | (49) count(all_13_1) = all_22_1 & count(all_13_2) = all_22_0 & in(0, % 12.86/2.53 | all_13_2) = all_22_2 & ($difference(all_22_0, all_22_1) = -1 | % 12.86/2.53 | all_22_2 = 0) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (49) implies: % 12.86/2.53 | (50) in(0, all_13_2) = all_22_2 % 12.86/2.53 | (51) count(all_13_2) = all_22_0 % 12.86/2.53 | (52) count(all_13_1) = all_22_1 % 12.86/2.53 | (53) $difference(all_22_0, all_22_1) = -1 | all_22_2 = 0 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (33) with fresh symbols all_24_0, all_24_1, all_24_2 % 12.86/2.53 | gives: % 12.86/2.53 | (54) count(all_13_1) = all_24_1 & count(all_13_2) = all_24_0 & in(0, % 12.86/2.53 | all_13_2) = all_24_2 & ( ~ (all_24_2 = 0) | all_24_0 = all_24_1) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (54) implies: % 12.86/2.53 | (55) in(0, all_13_2) = all_24_2 % 12.86/2.53 | (56) count(all_13_2) = all_24_0 % 12.86/2.53 | (57) count(all_13_1) = all_24_1 % 12.86/2.53 | (58) ~ (all_24_2 = 0) | all_24_0 = all_24_1 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (42) with fresh symbols all_26_0, all_26_1, all_26_2 % 12.86/2.53 | gives: % 12.86/2.53 | (59) count(all_13_2) = all_26_1 & count(all_13_8) = all_26_0 & in(all_13_7, % 12.86/2.53 | all_13_8) = all_26_2 & (all_26_0 = all_26_1 | all_26_2 = 0) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (59) implies: % 12.86/2.53 | (60) in(all_13_7, all_13_8) = all_26_2 % 12.86/2.53 | (61) count(all_13_8) = all_26_0 % 12.86/2.53 | (62) count(all_13_2) = all_26_1 % 12.86/2.53 | (63) all_26_0 = all_26_1 | all_26_2 = 0 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (41) with fresh symbols all_28_0, all_28_1, all_28_2 % 12.86/2.53 | gives: % 12.86/2.53 | (64) count(all_13_2) = all_28_1 & count(all_13_8) = all_28_0 & in(all_13_7, % 12.86/2.53 | all_13_8) = all_28_2 & ( ~ (all_28_2 = 0) | $difference(all_28_0, % 12.86/2.53 | all_28_1) = 1) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (64) implies: % 12.86/2.53 | (65) in(all_13_7, all_13_8) = all_28_2 % 12.86/2.53 | (66) count(all_13_8) = all_28_0 % 12.86/2.53 | (67) count(all_13_2) = all_28_1 % 12.86/2.53 | (68) ~ (all_28_2 = 0) | $difference(all_28_0, all_28_1) = 1 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (38) with fresh symbols all_30_0, all_30_1, all_30_2 % 12.86/2.53 | gives: % 12.86/2.53 | (69) count(all_13_6) = all_30_1 & count(all_13_8) = all_30_0 & in(all_13_7, % 12.86/2.53 | all_13_8) = all_30_2 & ($difference(all_30_0, all_30_1) = -1 | % 12.86/2.53 | all_30_2 = 0) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (69) implies: % 12.86/2.53 | (70) in(all_13_7, all_13_8) = all_30_2 % 12.86/2.53 | (71) count(all_13_8) = all_30_0 % 12.86/2.53 | (72) count(all_13_6) = all_30_1 % 12.86/2.53 | (73) $difference(all_30_0, all_30_1) = -1 | all_30_2 = 0 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (37) with fresh symbols all_32_0, all_32_1, all_32_2 % 12.86/2.53 | gives: % 12.86/2.53 | (74) count(all_13_6) = all_32_1 & count(all_13_8) = all_32_0 & in(all_13_7, % 12.86/2.53 | all_13_8) = all_32_2 & ( ~ (all_32_2 = 0) | all_32_0 = all_32_1) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (74) implies: % 12.86/2.53 | (75) in(all_13_7, all_13_8) = all_32_2 % 12.86/2.53 | (76) count(all_13_8) = all_32_0 % 12.86/2.53 | (77) count(all_13_6) = all_32_1 % 12.86/2.53 | (78) ~ (all_32_2 = 0) | all_32_0 = all_32_1 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (36) with fresh symbols all_34_0, all_34_1, all_34_2 % 12.86/2.53 | gives: % 12.86/2.53 | (79) count(all_13_1) = all_34_2 & count(all_13_2) = all_34_1 & in(0, % 12.86/2.53 | all_13_2) = all_34_0 & ( ~ (all_34_1 = all_34_2) | all_34_0 = 0) % 12.86/2.53 | % 12.86/2.53 | ALPHA: (79) implies: % 12.86/2.53 | (80) in(0, all_13_2) = all_34_0 % 12.86/2.53 | (81) count(all_13_2) = all_34_1 % 12.86/2.53 | (82) count(all_13_1) = all_34_2 % 12.86/2.53 | % 12.86/2.53 | DELTA: instantiating (40) with fresh symbols all_36_0, all_36_1, all_36_2 % 12.86/2.53 | gives: % 12.86/2.53 | (83) count(all_13_6) = all_36_2 & count(all_13_8) = all_36_1 & in(all_13_7, % 12.86/2.53 | all_13_8) = all_36_0 & ( ~ (all_36_1 = all_36_2) | all_36_0 = 0) % 12.86/2.53 | % 12.86/2.54 | ALPHA: (83) implies: % 12.86/2.54 | (84) in(all_13_7, all_13_8) = all_36_0 % 12.86/2.54 | (85) count(all_13_8) = all_36_1 % 12.86/2.54 | (86) count(all_13_6) = all_36_2 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (39) with fresh symbols all_38_0, all_38_1, all_38_2 % 12.86/2.54 | gives: % 12.86/2.54 | (87) count(all_13_6) = all_38_2 & count(all_13_8) = all_38_1 & in(all_13_7, % 12.86/2.54 | all_13_8) = all_38_0 & ( ~ (all_38_0 = 0) | ~ % 12.86/2.54 | ($difference(all_38_1, all_38_2) = -1)) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (87) implies: % 12.86/2.54 | (88) in(all_13_7, all_13_8) = all_38_0 % 12.86/2.54 | (89) count(all_13_8) = all_38_1 % 12.86/2.54 | (90) count(all_13_6) = all_38_2 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (32) with fresh symbols all_40_0, all_40_1, all_40_2 % 12.86/2.54 | gives: % 12.86/2.54 | (91) count(all_13_4) = all_40_2 & count(all_13_5) = all_40_1 & in(0, % 12.86/2.54 | all_13_5) = all_40_0 & ( ~ (all_40_1 = all_40_2) | all_40_0 = 0) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (91) implies: % 12.86/2.54 | (92) in(0, all_13_5) = all_40_0 % 12.86/2.54 | (93) count(all_13_5) = all_40_1 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (31) with fresh symbols all_42_0, all_42_1, all_42_2 % 12.86/2.54 | gives: % 12.86/2.54 | (94) count(all_13_4) = all_42_2 & count(all_13_5) = all_42_1 & in(0, % 12.86/2.54 | all_13_5) = all_42_0 & ( ~ (all_42_0 = 0) | ~ % 12.86/2.54 | ($difference(all_42_1, all_42_2) = -1)) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (94) implies: % 12.86/2.54 | (95) in(0, all_13_5) = all_42_0 % 12.86/2.54 | (96) count(all_13_5) = all_42_1 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (48) with fresh symbols all_44_0, all_44_1, all_44_2 % 12.86/2.54 | gives: % 12.86/2.54 | (97) count(all_13_5) = all_44_2 & count(all_13_6) = all_44_1 & in(all_13_7, % 12.86/2.54 | all_13_6) = all_44_0 & ( ~ ($difference(all_44_1, all_44_2) = 1) | % 12.86/2.54 | all_44_0 = 0) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (97) implies: % 12.86/2.54 | (98) in(all_13_7, all_13_6) = all_44_0 % 12.86/2.54 | (99) count(all_13_6) = all_44_1 % 12.86/2.54 | (100) count(all_13_5) = all_44_2 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (47) with fresh symbols all_46_0, all_46_1, all_46_2 % 12.86/2.54 | gives: % 12.86/2.54 | (101) count(all_13_5) = all_46_2 & count(all_13_6) = all_46_1 & % 12.86/2.54 | in(all_13_7, all_13_6) = all_46_0 & ( ~ (all_46_0 = 0) | ~ (all_46_1 % 12.86/2.54 | = all_46_2)) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (101) implies: % 12.86/2.54 | (102) in(all_13_7, all_13_6) = all_46_0 % 12.86/2.54 | (103) count(all_13_6) = all_46_1 % 12.86/2.54 | (104) count(all_13_5) = all_46_2 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (30) with fresh symbols all_48_0, all_48_1, all_48_2 % 12.86/2.54 | gives: % 12.86/2.54 | (105) count(all_13_4) = all_48_1 & count(all_13_5) = all_48_0 & in(0, % 12.86/2.54 | all_13_5) = all_48_2 & ($difference(all_48_0, all_48_1) = -1 | % 12.86/2.54 | all_48_2 = 0) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (105) implies: % 12.86/2.54 | (106) in(0, all_13_5) = all_48_2 % 12.86/2.54 | (107) count(all_13_5) = all_48_0 % 12.86/2.54 | (108) count(all_13_4) = all_48_1 % 12.86/2.54 | (109) $difference(all_48_0, all_48_1) = -1 | all_48_2 = 0 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (46) with fresh symbols all_50_0, all_50_1, all_50_2 % 12.86/2.54 | gives: % 12.86/2.54 | (110) count(all_13_5) = all_50_1 & count(all_13_6) = all_50_0 & % 12.86/2.54 | in(all_13_7, all_13_6) = all_50_2 & (all_50_0 = all_50_1 | all_50_2 = % 12.86/2.54 | 0) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (110) implies: % 12.86/2.54 | (111) in(all_13_7, all_13_6) = all_50_2 % 12.86/2.54 | (112) count(all_13_6) = all_50_0 % 12.86/2.54 | (113) count(all_13_5) = all_50_1 % 12.86/2.54 | % 12.86/2.54 | DELTA: instantiating (45) with fresh symbols all_52_0, all_52_1, all_52_2 % 12.86/2.54 | gives: % 12.86/2.54 | (114) count(all_13_5) = all_52_1 & count(all_13_6) = all_52_0 & % 12.86/2.54 | in(all_13_7, all_13_6) = all_52_2 & ( ~ (all_52_2 = 0) | % 12.86/2.54 | $difference(all_52_0, all_52_1) = 1) % 12.86/2.54 | % 12.86/2.54 | ALPHA: (114) implies: % 12.86/2.54 | (115) in(all_13_7, all_13_6) = all_52_2 % 12.86/2.54 | (116) count(all_13_6) = all_52_0 % 12.86/2.54 | (117) count(all_13_5) = all_52_1 % 12.86/2.55 | (118) ~ (all_52_2 = 0) | $difference(all_52_0, all_52_1) = 1 % 12.86/2.55 | % 12.86/2.55 | DELTA: instantiating (44) with fresh symbols all_54_0, all_54_1, all_54_2 % 12.86/2.55 | gives: % 12.86/2.55 | (119) count(all_13_2) = all_54_2 & count(all_13_8) = all_54_1 & % 12.86/2.55 | in(all_13_7, all_13_8) = all_54_0 & ( ~ ($difference(all_54_1, % 12.86/2.55 | all_54_2) = 1) | all_54_0 = 0) % 12.86/2.55 | % 12.86/2.55 | ALPHA: (119) implies: % 12.86/2.55 | (120) in(all_13_7, all_13_8) = all_54_0 % 12.86/2.55 | (121) count(all_13_8) = all_54_1 % 12.86/2.55 | (122) count(all_13_2) = all_54_2 % 12.86/2.55 | % 12.86/2.55 | DELTA: instantiating (43) with fresh symbols all_56_0, all_56_1, all_56_2 % 12.86/2.55 | gives: % 12.86/2.55 | (123) count(all_13_2) = all_56_2 & count(all_13_8) = all_56_1 & % 12.86/2.55 | in(all_13_7, all_13_8) = all_56_0 & ( ~ (all_56_0 = 0) | ~ (all_56_1 % 12.86/2.55 | = all_56_2)) % 12.86/2.55 | % 12.86/2.55 | ALPHA: (123) implies: % 12.86/2.55 | (124) in(all_13_7, all_13_8) = all_56_0 % 12.86/2.55 | (125) count(all_13_8) = all_56_1 % 12.86/2.55 | (126) count(all_13_2) = all_56_2 % 12.86/2.55 | % 12.86/2.55 | DELTA: instantiating (29) with fresh symbols all_58_0, all_58_1, all_58_2 % 12.86/2.55 | gives: % 12.86/2.55 | (127) count(all_13_4) = all_58_1 & count(all_13_5) = all_58_0 & in(0, % 12.86/2.55 | all_13_5) = all_58_2 & ( ~ (all_58_2 = 0) | all_58_0 = all_58_1) % 12.86/2.55 | % 12.86/2.55 | ALPHA: (127) implies: % 12.86/2.55 | (128) in(0, all_13_5) = all_58_2 % 12.86/2.55 | (129) count(all_13_5) = all_58_0 % 12.86/2.55 | (130) count(all_13_4) = all_58_1 % 12.86/2.55 | (131) ~ (all_58_2 = 0) | all_58_0 = all_58_1 % 12.86/2.55 | % 12.86/2.55 | DELTA: instantiating (35) with fresh symbols all_60_0, all_60_1, all_60_2 % 12.86/2.55 | gives: % 12.86/2.55 | (132) count(all_13_1) = all_60_2 & count(all_13_2) = all_60_1 & in(0, % 12.86/2.55 | all_13_2) = all_60_0 & ( ~ (all_60_0 = 0) | ~ % 12.86/2.55 | ($difference(all_60_1, all_60_2) = -1)) % 12.86/2.55 | % 12.86/2.55 | ALPHA: (132) implies: % 12.86/2.55 | (133) in(0, all_13_2) = all_60_0 % 12.86/2.55 | (134) count(all_13_2) = all_60_1 % 12.86/2.55 | (135) count(all_13_1) = all_60_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_48_2, all_58_2, all_13_5, 0, % 12.86/2.55 | simplifying with (106), (128) gives: % 12.86/2.55 | (136) all_58_2 = all_48_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_42_0, all_58_2, all_13_5, 0, % 12.86/2.55 | simplifying with (95), (128) gives: % 12.86/2.55 | (137) all_58_2 = all_42_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_40_0, all_58_2, all_13_5, 0, % 12.86/2.55 | simplifying with (92), (128) gives: % 12.86/2.55 | (138) all_58_2 = all_40_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_24_2, all_34_0, all_13_2, 0, % 12.86/2.55 | simplifying with (55), (80) gives: % 12.86/2.55 | (139) all_34_0 = all_24_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_34_0, all_60_0, all_13_2, 0, % 12.86/2.55 | simplifying with (80), (133) gives: % 12.86/2.55 | (140) all_60_0 = all_34_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_22_2, all_60_0, all_13_2, 0, % 12.86/2.55 | simplifying with (50), (133) gives: % 12.86/2.55 | (141) all_60_0 = all_22_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_28_2, all_32_2, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (65), (75) gives: % 12.86/2.55 | (142) all_32_2 = all_28_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_26_2, all_32_2, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (60), (75) gives: % 12.86/2.55 | (143) all_32_2 = all_26_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_36_0, all_54_0, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (84), (120) gives: % 12.86/2.55 | (144) all_54_0 = all_36_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_32_2, all_54_0, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (75), (120) gives: % 12.86/2.55 | (145) all_54_0 = all_32_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_30_2, all_54_0, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (70), (120) gives: % 12.86/2.55 | (146) all_54_0 = all_30_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_54_0, all_56_0, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (120), (124) gives: % 12.86/2.55 | (147) all_56_0 = all_54_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_38_0, all_56_0, all_13_8, all_13_7, % 12.86/2.55 | simplifying with (88), (124) gives: % 12.86/2.55 | (148) all_56_0 = all_38_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_50_2, all_52_2, all_13_6, all_13_7, % 12.86/2.55 | simplifying with (111), (115) gives: % 12.86/2.55 | (149) all_52_2 = all_50_2 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_46_0, all_52_2, all_13_6, all_13_7, % 12.86/2.55 | simplifying with (102), (115) gives: % 12.86/2.55 | (150) all_52_2 = all_46_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (15) with all_44_0, all_52_2, all_13_6, all_13_7, % 12.86/2.55 | simplifying with (98), (115) gives: % 12.86/2.55 | (151) all_52_2 = all_44_0 % 12.86/2.55 | % 12.86/2.55 | GROUND_INST: instantiating (14) with all_26_0, all_30_0, all_13_8, simplifying % 12.86/2.56 | with (61), (71) gives: % 12.86/2.56 | (152) all_30_0 = all_26_0 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_30_0, all_36_1, all_13_8, simplifying % 12.86/2.56 | with (71), (85) gives: % 12.86/2.56 | (153) all_36_1 = all_30_0 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_36_1, all_38_1, all_13_8, simplifying % 12.86/2.56 | with (85), (89) gives: % 12.86/2.56 | (154) all_38_1 = all_36_1 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_32_0, all_38_1, all_13_8, simplifying % 12.86/2.56 | with (76), (89) gives: % 12.86/2.56 | (155) all_38_1 = all_32_0 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_54_1, all_56_1, all_13_8, simplifying % 12.86/2.56 | with (121), (125) gives: % 12.86/2.56 | (156) all_56_1 = all_54_1 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_36_1, all_56_1, all_13_8, simplifying % 12.86/2.56 | with (85), (125) gives: % 12.86/2.56 | (157) all_56_1 = all_36_1 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_28_0, all_56_1, all_13_8, simplifying % 12.86/2.56 | with (66), (125) gives: % 12.86/2.56 | (158) all_56_1 = all_28_0 % 12.86/2.56 | % 12.86/2.56 | GROUND_INST: instantiating (14) with all_36_2, all_38_2, all_13_6, simplifying % 12.86/2.56 | with (86), (90) gives: % 12.86/2.56 | (159) all_38_2 = all_36_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_44_1, all_46_1, all_13_6, simplifying % 13.27/2.56 | with (99), (103) gives: % 13.27/2.56 | (160) all_46_1 = all_44_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_38_2, all_46_1, all_13_6, simplifying % 13.27/2.56 | with (90), (103) gives: % 13.27/2.56 | (161) all_46_1 = all_38_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_32_1, all_46_1, all_13_6, simplifying % 13.27/2.56 | with (77), (103) gives: % 13.27/2.56 | (162) all_46_1 = all_32_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_50_0, all_52_0, all_13_6, simplifying % 13.27/2.56 | with (112), (116) gives: % 13.27/2.56 | (163) all_52_0 = all_50_0 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_36_2, all_52_0, all_13_6, simplifying % 13.27/2.56 | with (86), (116) gives: % 13.27/2.56 | (164) all_52_0 = all_36_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_30_1, all_52_0, all_13_6, simplifying % 13.27/2.56 | with (72), (116) gives: % 13.27/2.56 | (165) all_52_0 = all_30_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_44_2, all_48_0, all_13_5, simplifying % 13.27/2.56 | with (100), (107) gives: % 13.27/2.56 | (166) all_48_0 = all_44_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_40_1, all_48_0, all_13_5, simplifying % 13.27/2.56 | with (93), (107) gives: % 13.27/2.56 | (167) all_48_0 = all_40_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_48_0, all_50_1, all_13_5, simplifying % 13.27/2.56 | with (107), (113) gives: % 13.27/2.56 | (168) all_50_1 = all_48_0 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_46_2, all_50_1, all_13_5, simplifying % 13.27/2.56 | with (104), (113) gives: % 13.27/2.56 | (169) all_50_1 = all_46_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_50_1, all_52_1, all_13_5, simplifying % 13.27/2.56 | with (113), (117) gives: % 13.27/2.56 | (170) all_52_1 = all_50_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_52_1, all_58_0, all_13_5, simplifying % 13.27/2.56 | with (117), (129) gives: % 13.27/2.56 | (171) all_58_0 = all_52_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_42_1, all_58_0, all_13_5, simplifying % 13.27/2.56 | with (96), (129) gives: % 13.27/2.56 | (172) all_58_0 = all_42_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_48_1, all_58_1, all_13_4, simplifying % 13.27/2.56 | with (108), (130) gives: % 13.27/2.56 | (173) all_58_1 = all_48_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_13_3, all_58_1, all_13_4, simplifying % 13.27/2.56 | with (22), (130) gives: % 13.27/2.56 | (174) all_58_1 = all_13_3 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_22_0, all_26_1, all_13_2, simplifying % 13.27/2.56 | with (51), (62) gives: % 13.27/2.56 | (175) all_26_1 = all_22_0 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_26_1, all_28_1, all_13_2, simplifying % 13.27/2.56 | with (62), (67) gives: % 13.27/2.56 | (176) all_28_1 = all_26_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_54_2, all_56_2, all_13_2, simplifying % 13.27/2.56 | with (122), (126) gives: % 13.27/2.56 | (177) all_56_2 = all_54_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_34_1, all_56_2, all_13_2, simplifying % 13.27/2.56 | with (81), (126) gives: % 13.27/2.56 | (178) all_56_2 = all_34_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_28_1, all_56_2, all_13_2, simplifying % 13.27/2.56 | with (67), (126) gives: % 13.27/2.56 | (179) all_56_2 = all_28_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_54_2, all_60_1, all_13_2, simplifying % 13.27/2.56 | with (122), (134) gives: % 13.27/2.56 | (180) all_60_1 = all_54_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_24_0, all_60_1, all_13_2, simplifying % 13.27/2.56 | with (56), (134) gives: % 13.27/2.56 | (181) all_60_1 = all_24_0 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_13_0, all_34_2, all_13_1, simplifying % 13.27/2.56 | with (23), (82) gives: % 13.27/2.56 | (182) all_34_2 = all_13_0 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_34_2, all_60_2, all_13_1, simplifying % 13.27/2.56 | with (82), (135) gives: % 13.27/2.56 | (183) all_60_2 = all_34_2 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_24_1, all_60_2, all_13_1, simplifying % 13.27/2.56 | with (57), (135) gives: % 13.27/2.56 | (184) all_60_2 = all_24_1 % 13.27/2.56 | % 13.27/2.56 | GROUND_INST: instantiating (14) with all_22_1, all_60_2, all_13_1, simplifying % 13.27/2.56 | with (52), (135) gives: % 13.27/2.56 | (185) all_60_2 = all_22_1 % 13.27/2.56 | % 13.27/2.57 | COMBINE_EQS: (140), (141) imply: % 13.27/2.57 | (186) all_34_0 = all_22_2 % 13.27/2.57 | % 13.27/2.57 | SIMP: (186) implies: % 13.27/2.57 | (187) all_34_0 = all_22_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (180), (181) imply: % 13.27/2.57 | (188) all_54_2 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (188) implies: % 13.27/2.57 | (189) all_54_2 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (184), (185) imply: % 13.27/2.57 | (190) all_24_1 = all_22_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (183), (184) imply: % 13.27/2.57 | (191) all_34_2 = all_24_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (191) implies: % 13.27/2.57 | (192) all_34_2 = all_24_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (171), (172) imply: % 13.27/2.57 | (193) all_52_1 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (193) implies: % 13.27/2.57 | (194) all_52_1 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (173), (174) imply: % 13.27/2.57 | (195) all_48_1 = all_13_3 % 13.27/2.57 | % 13.27/2.57 | SIMP: (195) implies: % 13.27/2.57 | (196) all_48_1 = all_13_3 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (136), (138) imply: % 13.27/2.57 | (197) all_48_2 = all_40_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (136), (137) imply: % 13.27/2.57 | (198) all_48_2 = all_42_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (147), (148) imply: % 13.27/2.57 | (199) all_54_0 = all_38_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (199) implies: % 13.27/2.57 | (200) all_54_0 = all_38_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (156), (157) imply: % 13.27/2.57 | (201) all_54_1 = all_36_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (156), (158) imply: % 13.27/2.57 | (202) all_54_1 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (178), (179) imply: % 13.27/2.57 | (203) all_34_1 = all_28_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (177), (178) imply: % 13.27/2.57 | (204) all_54_2 = all_34_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (204) implies: % 13.27/2.57 | (205) all_54_2 = all_34_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (145), (200) imply: % 13.27/2.57 | (206) all_38_0 = all_32_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (144), (200) imply: % 13.27/2.57 | (207) all_38_0 = all_36_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (146), (200) imply: % 13.27/2.57 | (208) all_38_0 = all_30_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (201), (202) imply: % 13.27/2.57 | (209) all_36_1 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (209) implies: % 13.27/2.57 | (210) all_36_1 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (189), (205) imply: % 13.27/2.57 | (211) all_34_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (211) implies: % 13.27/2.57 | (212) all_34_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (163), (165) imply: % 13.27/2.57 | (213) all_50_0 = all_30_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (163), (164) imply: % 13.27/2.57 | (214) all_50_0 = all_36_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (170), (194) imply: % 13.27/2.57 | (215) all_50_1 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (215) implies: % 13.27/2.57 | (216) all_50_1 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (149), (151) imply: % 13.27/2.57 | (217) all_50_2 = all_44_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (149), (150) imply: % 13.27/2.57 | (218) all_50_2 = all_46_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (213), (214) imply: % 13.27/2.57 | (219) all_36_2 = all_30_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (219) implies: % 13.27/2.57 | (220) all_36_2 = all_30_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (168), (169) imply: % 13.27/2.57 | (221) all_48_0 = all_46_2 % 13.27/2.57 | % 13.27/2.57 | SIMP: (221) implies: % 13.27/2.57 | (222) all_48_0 = all_46_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (169), (216) imply: % 13.27/2.57 | (223) all_46_2 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (217), (218) imply: % 13.27/2.57 | (224) all_46_0 = all_44_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (224) implies: % 13.27/2.57 | (225) all_46_0 = all_44_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (166), (222) imply: % 13.27/2.57 | (226) all_46_2 = all_44_2 % 13.27/2.57 | % 13.27/2.57 | SIMP: (226) implies: % 13.27/2.57 | (227) all_46_2 = all_44_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (166), (167) imply: % 13.27/2.57 | (228) all_44_2 = all_40_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (197), (198) imply: % 13.27/2.57 | (229) all_42_0 = all_40_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (229) implies: % 13.27/2.57 | (230) all_42_0 = all_40_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (160), (161) imply: % 13.27/2.57 | (231) all_44_1 = all_38_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (160), (162) imply: % 13.27/2.57 | (232) all_44_1 = all_32_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (223), (227) imply: % 13.27/2.57 | (233) all_44_2 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (233) implies: % 13.27/2.57 | (234) all_44_2 = all_42_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (231), (232) imply: % 13.27/2.57 | (235) all_38_2 = all_32_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (235) implies: % 13.27/2.57 | (236) all_38_2 = all_32_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (228), (234) imply: % 13.27/2.57 | (237) all_42_1 = all_40_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (206), (207) imply: % 13.27/2.57 | (238) all_36_0 = all_32_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (207), (208) imply: % 13.27/2.57 | (239) all_36_0 = all_30_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (154), (155) imply: % 13.27/2.57 | (240) all_36_1 = all_32_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (240) implies: % 13.27/2.57 | (241) all_36_1 = all_32_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (159), (236) imply: % 13.27/2.57 | (242) all_36_2 = all_32_1 % 13.27/2.57 | % 13.27/2.57 | SIMP: (242) implies: % 13.27/2.57 | (243) all_36_2 = all_32_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (238), (239) imply: % 13.27/2.57 | (244) all_32_2 = all_30_2 % 13.27/2.57 | % 13.27/2.57 | SIMP: (244) implies: % 13.27/2.57 | (245) all_32_2 = all_30_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (210), (241) imply: % 13.27/2.57 | (246) all_32_0 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (153), (241) imply: % 13.27/2.57 | (247) all_32_0 = all_30_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (220), (243) imply: % 13.27/2.57 | (248) all_32_1 = all_30_1 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (139), (187) imply: % 13.27/2.57 | (249) all_24_2 = all_22_2 % 13.27/2.57 | % 13.27/2.57 | SIMP: (249) implies: % 13.27/2.57 | (250) all_24_2 = all_22_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (203), (212) imply: % 13.27/2.57 | (251) all_28_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (251) implies: % 13.27/2.57 | (252) all_28_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (182), (192) imply: % 13.27/2.57 | (253) all_24_1 = all_13_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (253) implies: % 13.27/2.57 | (254) all_24_1 = all_13_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (246), (247) imply: % 13.27/2.57 | (255) all_30_0 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (255) implies: % 13.27/2.57 | (256) all_30_0 = all_28_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (143), (245) imply: % 13.27/2.57 | (257) all_30_2 = all_26_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (142), (245) imply: % 13.27/2.57 | (258) all_30_2 = all_28_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (152), (256) imply: % 13.27/2.57 | (259) all_28_0 = all_26_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (257), (258) imply: % 13.27/2.57 | (260) all_28_2 = all_26_2 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (176), (252) imply: % 13.27/2.57 | (261) all_26_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | SIMP: (261) implies: % 13.27/2.57 | (262) all_26_1 = all_24_0 % 13.27/2.57 | % 13.27/2.57 | COMBINE_EQS: (175), (262) imply: % 13.27/2.58 | (263) all_24_0 = all_22_0 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (190), (254) imply: % 13.27/2.58 | (264) all_22_1 = all_13_0 % 13.27/2.58 | % 13.27/2.58 | SIMP: (264) implies: % 13.27/2.58 | (265) all_22_1 = all_13_0 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (252), (263) imply: % 13.27/2.58 | (266) all_28_1 = all_22_0 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (246), (259) imply: % 13.27/2.58 | (267) all_32_0 = all_26_0 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (194), (237) imply: % 13.27/2.58 | (268) all_52_1 = all_40_1 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (172), (237) imply: % 13.27/2.58 | (269) all_58_0 = all_40_1 % 13.27/2.58 | % 13.27/2.58 | GROUND_INST: instantiating (11) with 0, all_13_6, all_13_7, all_13_5, % 13.27/2.58 | all_40_0, simplifying with (19), (28), (92) gives: % 13.27/2.58 | (270) all_40_0 = 0 | all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, % 13.27/2.58 | all_13_6) = v0) % 13.27/2.58 | % 13.27/2.58 | GROUND_INST: instantiating (11) with 0, all_13_8, all_13_7, all_13_2, % 13.27/2.58 | all_22_2, simplifying with (18), (27), (50) gives: % 13.27/2.58 | (271) all_22_2 = 0 | all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, % 13.27/2.58 | all_13_8) = v0) % 13.27/2.58 | % 13.27/2.58 | GROUND_INST: instantiating (1) with all_13_7, all_13_8, all_13_6, all_44_0, % 13.27/2.58 | simplifying with (18), (26), (98) gives: % 13.27/2.58 | (272) all_44_0 = 0 % 13.27/2.58 | % 13.27/2.58 | COMBINE_EQS: (151), (272) imply: % 13.27/2.58 | (273) all_52_2 = 0 % 13.27/2.58 | % 13.27/2.58 | BETA: splitting (118) gives: % 13.27/2.58 | % 13.27/2.58 | Case 1: % 13.27/2.58 | | % 13.27/2.58 | | (274) ~ (all_52_2 = 0) % 13.27/2.58 | | % 13.27/2.58 | | REDUCE: (273), (274) imply: % 13.27/2.58 | | (275) $false % 13.27/2.58 | | % 13.27/2.58 | | CLOSE: (275) is inconsistent. % 13.27/2.58 | | % 13.27/2.58 | Case 2: % 13.27/2.58 | | % 13.27/2.58 | | (276) $difference(all_52_0, all_52_1) = 1 % 13.27/2.58 | | % 13.27/2.58 | | COMBINE_EQS: (165), (276) imply: % 13.27/2.58 | | (277) $difference(all_52_1, all_30_1) = -1 % 13.27/2.58 | | % 13.27/2.58 | | SIMP: (277) implies: % 13.27/2.58 | | (278) $difference(all_52_1, all_30_1) = -1 % 13.27/2.58 | | % 13.27/2.58 | | COMBINE_EQS: (268), (278) imply: % 13.27/2.58 | | (279) $difference(all_40_1, all_30_1) = -1 % 13.27/2.58 | | % 13.27/2.58 | | COMBINE_EQS: (167), (279) imply: % 13.27/2.58 | | (280) $difference(all_48_0, all_30_1) = -1 % 13.27/2.58 | | % 13.27/2.58 | | COMBINE_EQS: (269), (279) imply: % 13.27/2.58 | | (281) $difference(all_58_0, all_30_1) = -1 % 13.27/2.58 | | % 13.27/2.58 | | BETA: splitting (53) gives: % 13.27/2.58 | | % 13.27/2.58 | | Case 1: % 13.27/2.58 | | | % 13.27/2.58 | | | (282) all_22_2 = 0 % 13.27/2.58 | | | % 13.27/2.58 | | | COMBINE_EQS: (250), (282) imply: % 13.27/2.58 | | | (283) all_24_2 = 0 % 13.27/2.58 | | | % 13.27/2.58 | | | REDUCE: (50), (282) imply: % 13.27/2.58 | | | (284) in(0, all_13_2) = 0 % 13.27/2.58 | | | % 13.27/2.58 | | | BETA: splitting (58) gives: % 13.27/2.58 | | | % 13.27/2.58 | | | Case 1: % 13.27/2.58 | | | | % 13.27/2.58 | | | | (285) ~ (all_24_2 = 0) % 13.27/2.58 | | | | % 13.27/2.58 | | | | REDUCE: (283), (285) imply: % 13.27/2.58 | | | | (286) $false % 13.27/2.58 | | | | % 13.27/2.58 | | | | CLOSE: (286) is inconsistent. % 13.27/2.58 | | | | % 13.27/2.58 | | | Case 2: % 13.27/2.58 | | | | % 13.27/2.58 | | | | (287) all_24_0 = all_24_1 % 13.27/2.58 | | | | % 13.27/2.58 | | | | COMBINE_EQS: (263), (287) imply: % 13.27/2.58 | | | | (288) all_24_1 = all_22_0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | COMBINE_EQS: (254), (288) imply: % 13.27/2.58 | | | | (289) all_22_0 = all_13_0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | SIMP: (289) implies: % 13.27/2.58 | | | | (290) all_22_0 = all_13_0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | COMBINE_EQS: (175), (290) imply: % 13.27/2.58 | | | | (291) all_26_1 = all_13_0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | COMBINE_EQS: (266), (290) imply: % 13.27/2.58 | | | | (292) all_28_1 = all_13_0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | GROUND_INST: instantiating (10) with 0, all_13_8, all_13_7, all_13_2, % 13.27/2.58 | | | | simplifying with (18), (27), (284) gives: % 13.27/2.58 | | | | (293) ~ (all_13_7 = 0) & in(0, all_13_8) = 0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | ALPHA: (293) implies: % 13.27/2.58 | | | | (294) ~ (all_13_7 = 0) % 13.27/2.58 | | | | (295) in(0, all_13_8) = 0 % 13.27/2.58 | | | | % 13.27/2.58 | | | | BETA: splitting (63) gives: % 13.27/2.58 | | | | % 13.27/2.58 | | | | Case 1: % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | (296) all_26_2 = 0 % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | COMBINE_EQS: (260), (296) imply: % 13.27/2.58 | | | | | (297) all_28_2 = 0 % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | COMBINE_EQS: (143), (296) imply: % 13.27/2.58 | | | | | (298) all_32_2 = 0 % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | BETA: splitting (68) gives: % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | Case 1: % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | (299) ~ (all_28_2 = 0) % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | REDUCE: (297), (299) imply: % 13.27/2.58 | | | | | | (300) $false % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | CLOSE: (300) is inconsistent. % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | Case 2: % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | (301) $difference(all_28_0, all_28_1) = 1 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | COMBINE_EQS: (259), (301) imply: % 13.27/2.58 | | | | | | (302) $difference(all_28_1, all_26_0) = -1 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | COMBINE_EQS: (292), (302) imply: % 13.27/2.58 | | | | | | (303) $difference(all_26_0, all_13_0) = 1 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | SIMP: (303) implies: % 13.27/2.58 | | | | | | (304) $difference(all_26_0, all_13_0) = 1 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | COMBINE_EQS: (267), (304) imply: % 13.27/2.58 | | | | | | (305) $difference(all_32_0, all_13_0) = 1 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | BETA: splitting (78) gives: % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | Case 1: % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | (306) ~ (all_32_2 = 0) % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | REDUCE: (298), (306) imply: % 13.27/2.58 | | | | | | | (307) $false % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | CLOSE: (307) is inconsistent. % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | Case 2: % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | (308) all_32_0 = all_32_1 % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | COMBINE_EQS: (305), (308) imply: % 13.27/2.58 | | | | | | | (309) $difference(all_32_1, all_13_0) = 1 % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | COMBINE_EQS: (248), (309) imply: % 13.27/2.58 | | | | | | | (310) $difference(all_30_1, all_13_0) = 1 % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | COMBINE_EQS: (281), (310) imply: % 13.27/2.58 | | | | | | | (311) all_58_0 = all_13_0 % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | | REF_CLOSE: (7), (15), (17), (18), (26), (131), (138), (174), % 13.27/2.58 | | | | | | | (270), (294), (295), (311) are inconsistent by % 13.27/2.58 | | | | | | | sub-proof #2. % 13.27/2.58 | | | | | | | % 13.27/2.58 | | | | | | End of split % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | End of split % 13.27/2.58 | | | | | % 13.27/2.58 | | | | Case 2: % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | (312) all_26_0 = all_26_1 % 13.27/2.58 | | | | | (313) ~ (all_26_2 = 0) % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | COMBINE_EQS: (291), (312) imply: % 13.27/2.58 | | | | | (314) all_26_0 = all_13_0 % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | COMBINE_EQS: (152), (314) imply: % 13.27/2.58 | | | | | (315) all_30_0 = all_13_0 % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | BETA: splitting (73) gives: % 13.27/2.58 | | | | | % 13.27/2.58 | | | | | Case 1: % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | (316) all_30_2 = 0 % 13.27/2.58 | | | | | | % 13.27/2.58 | | | | | | COMBINE_EQS: (257), (316) imply: % 13.27/2.59 | | | | | | (317) all_26_2 = 0 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | REDUCE: (313), (317) imply: % 13.27/2.59 | | | | | | (318) $false % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | CLOSE: (318) is inconsistent. % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | Case 2: % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | (319) $difference(all_30_0, all_30_1) = -1 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | COMBINE_EQS: (315), (319) imply: % 13.27/2.59 | | | | | | (320) $difference(all_30_1, all_13_0) = 1 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | COMBINE_EQS: (281), (320) imply: % 13.27/2.59 | | | | | | (321) all_58_0 = all_13_0 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | REF_CLOSE: (7), (15), (17), (18), (26), (131), (138), (174), (270), % 13.27/2.59 | | | | | | (294), (295), (321) are inconsistent by sub-proof #2. % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | End of split % 13.27/2.59 | | | | | % 13.27/2.59 | | | | End of split % 13.27/2.59 | | | | % 13.27/2.59 | | | End of split % 13.27/2.59 | | | % 13.27/2.59 | | Case 2: % 13.27/2.59 | | | % 13.27/2.59 | | | (322) $difference(all_22_0, all_22_1) = -1 % 13.27/2.59 | | | (323) ~ (all_22_2 = 0) % 13.27/2.59 | | | % 13.27/2.59 | | | COMBINE_EQS: (265), (322) imply: % 13.27/2.59 | | | (324) $difference(all_22_0, all_13_0) = -1 % 13.27/2.59 | | | % 13.27/2.59 | | | COMBINE_EQS: (175), (324) imply: % 13.27/2.59 | | | (325) $difference(all_26_1, all_13_0) = -1 % 13.27/2.59 | | | % 13.27/2.59 | | | COMBINE_EQS: (266), (324) imply: % 13.27/2.59 | | | (326) $difference(all_28_1, all_13_0) = -1 % 13.27/2.59 | | | % 13.27/2.59 | | | BETA: splitting (63) gives: % 13.27/2.59 | | | % 13.27/2.59 | | | Case 1: % 13.27/2.59 | | | | % 13.27/2.59 | | | | (327) all_26_2 = 0 % 13.27/2.59 | | | | % 13.27/2.59 | | | | COMBINE_EQS: (260), (327) imply: % 13.27/2.59 | | | | (328) all_28_2 = 0 % 13.27/2.59 | | | | % 13.27/2.59 | | | | COMBINE_EQS: (143), (327) imply: % 13.27/2.59 | | | | (329) all_32_2 = 0 % 13.27/2.59 | | | | % 13.27/2.59 | | | | BETA: splitting (68) gives: % 13.27/2.59 | | | | % 13.27/2.59 | | | | Case 1: % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | (330) ~ (all_28_2 = 0) % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | REDUCE: (328), (330) imply: % 13.27/2.59 | | | | | (331) $false % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | CLOSE: (331) is inconsistent. % 13.27/2.59 | | | | | % 13.27/2.59 | | | | Case 2: % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | (332) $difference(all_28_0, all_28_1) = 1 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (259), (332) imply: % 13.27/2.59 | | | | | (333) $difference(all_28_1, all_26_0) = -1 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (326), (333) imply: % 13.27/2.59 | | | | | (334) all_26_0 = all_13_0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | SIMP: (334) implies: % 13.27/2.59 | | | | | (335) all_26_0 = all_13_0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (267), (335) imply: % 13.27/2.59 | | | | | (336) all_32_0 = all_13_0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | BETA: splitting (78) gives: % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | Case 1: % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | (337) ~ (all_32_2 = 0) % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | REDUCE: (329), (337) imply: % 13.27/2.59 | | | | | | (338) $false % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | CLOSE: (338) is inconsistent. % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | Case 2: % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | (339) all_32_0 = all_32_1 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | COMBINE_EQS: (336), (339) imply: % 13.27/2.59 | | | | | | (340) all_32_1 = all_13_0 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | COMBINE_EQS: (248), (340) imply: % 13.27/2.59 | | | | | | (341) all_30_1 = all_13_0 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | COMBINE_EQS: (280), (341) imply: % 13.27/2.59 | | | | | | (342) $difference(all_48_0, all_13_0) = -1 % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | | REF_CLOSE: (6), (10), (15), (17), (18), (19), (26), (28), (92), % 13.27/2.59 | | | | | | (109), (196), (197), (271), (323), (342) are inconsistent % 13.27/2.59 | | | | | | by sub-proof #1. % 13.27/2.59 | | | | | | % 13.27/2.59 | | | | | End of split % 13.27/2.59 | | | | | % 13.27/2.59 | | | | End of split % 13.27/2.59 | | | | % 13.27/2.59 | | | Case 2: % 13.27/2.59 | | | | % 13.27/2.59 | | | | (343) all_26_0 = all_26_1 % 13.27/2.59 | | | | (344) ~ (all_26_2 = 0) % 13.27/2.59 | | | | % 13.27/2.59 | | | | COMBINE_EQS: (325), (343) imply: % 13.27/2.59 | | | | (345) $difference(all_26_0, all_13_0) = -1 % 13.27/2.59 | | | | % 13.27/2.59 | | | | COMBINE_EQS: (152), (345) imply: % 13.27/2.59 | | | | (346) $difference(all_30_0, all_13_0) = -1 % 13.27/2.59 | | | | % 13.27/2.59 | | | | BETA: splitting (73) gives: % 13.27/2.59 | | | | % 13.27/2.59 | | | | Case 1: % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | (347) all_30_2 = 0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (257), (347) imply: % 13.27/2.59 | | | | | (348) all_26_2 = 0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | REDUCE: (344), (348) imply: % 13.27/2.59 | | | | | (349) $false % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | CLOSE: (349) is inconsistent. % 13.27/2.59 | | | | | % 13.27/2.59 | | | | Case 2: % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | (350) $difference(all_30_0, all_30_1) = -1 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (346), (350) imply: % 13.27/2.59 | | | | | (351) all_30_1 = all_13_0 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | COMBINE_EQS: (280), (351) imply: % 13.27/2.59 | | | | | (352) $difference(all_48_0, all_13_0) = -1 % 13.27/2.59 | | | | | % 13.27/2.59 | | | | | REF_CLOSE: (6), (10), (15), (17), (18), (19), (26), (28), (92), (109), % 13.27/2.59 | | | | | (196), (197), (271), (323), (352) are inconsistent by % 13.27/2.59 | | | | | sub-proof #1. % 13.27/2.59 | | | | | % 13.27/2.59 | | | | End of split % 13.27/2.59 | | | | % 13.27/2.59 | | | End of split % 13.27/2.59 | | | % 13.27/2.59 | | End of split % 13.27/2.59 | | % 13.27/2.59 | End of split % 13.27/2.59 | % 13.27/2.59 End of proof % 13.27/2.59 % 13.27/2.59 Sub-proof #1 shows that the following formulas are inconsistent: % 13.27/2.59 ---------------------------------------------------------------- % 13.27/2.59 (1) all_48_1 = all_13_3 % 13.27/2.59 (2) ~ (all_13_0 = all_13_3) % 13.27/2.59 (3) in(0, all_13_5) = all_40_0 % 13.27/2.59 (4) all_22_2 = 0 | all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, % 13.27/2.59 all_13_8) = v0) % 13.27/2.59 (5) collection(all_13_8) % 13.27/2.59 (6) collection(all_13_6) % 13.27/2.59 (7) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : % 13.27/2.59 (v2 = v0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ % 13.27/2.59 collection(v1) | in(v0, v1) = 0) % 13.27/2.59 (8) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : % 13.27/2.59 ( ~ (remove(v2, v1) = v3) | ~ (in(v0, v3) = 0) | ~ collection(v1) | ( ~ % 13.27/2.59 (v2 = v0) & in(v0, v1) = 0)) % 13.27/2.59 (9) all_48_2 = all_40_0 % 13.27/2.59 (10) ~ (all_22_2 = 0) % 13.27/2.59 (11) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 13.27/2.59 collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 13.27/2.59 (in(v3, v2) = v0)) % 13.27/2.59 (12) $difference(all_48_0, all_48_1) = -1 | all_48_2 = 0 % 13.27/2.59 (13) $difference(all_48_0, all_13_0) = -1 % 13.27/2.59 (14) remove(all_13_7, all_13_6) = all_13_5 % 13.27/2.59 (15) add(all_13_7, all_13_8) = all_13_6 % 13.27/2.59 % 13.27/2.59 Begin of proof % 13.27/2.59 | % 13.27/2.59 | BETA: splitting (12) gives: % 13.27/2.59 | % 13.27/2.59 | Case 1: % 13.27/2.59 | | % 13.27/2.59 | | (16) all_48_2 = 0 % 13.27/2.59 | | % 13.27/2.59 | | COMBINE_EQS: (9), (16) imply: % 13.27/2.59 | | (17) all_40_0 = 0 % 13.27/2.59 | | % 13.27/2.59 | | SIMP: (17) implies: % 13.27/2.59 | | (18) all_40_0 = 0 % 13.27/2.59 | | % 13.27/2.59 | | REDUCE: (3), (18) imply: % 13.27/2.59 | | (19) in(0, all_13_5) = 0 % 13.27/2.59 | | % 13.27/2.59 | | GROUND_INST: instantiating (8) with 0, all_13_6, all_13_7, all_13_5, % 13.27/2.59 | | simplifying with (6), (14), (19) gives: % 13.27/2.59 | | (20) ~ (all_13_7 = 0) & in(0, all_13_6) = 0 % 13.27/2.59 | | % 13.27/2.59 | | ALPHA: (20) implies: % 13.27/2.59 | | (21) ~ (all_13_7 = 0) % 13.27/2.59 | | (22) in(0, all_13_6) = 0 % 13.27/2.59 | | % 13.27/2.59 | | BETA: splitting (4) gives: % 13.27/2.59 | | % 13.27/2.59 | | Case 1: % 13.27/2.59 | | | % 13.27/2.59 | | | (23) all_22_2 = 0 % 13.27/2.59 | | | % 13.27/2.59 | | | REDUCE: (10), (23) imply: % 13.27/2.59 | | | (24) $false % 13.27/2.59 | | | % 13.27/2.59 | | | CLOSE: (24) is inconsistent. % 13.27/2.59 | | | % 13.27/2.59 | | Case 2: % 13.27/2.59 | | | % 13.27/2.60 | | | (25) all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, all_13_8) = v0) % 13.27/2.60 | | | % 13.27/2.60 | | | BETA: splitting (25) gives: % 13.27/2.60 | | | % 13.27/2.60 | | | Case 1: % 13.27/2.60 | | | | % 13.27/2.60 | | | | (26) all_13_7 = 0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | REDUCE: (21), (26) imply: % 13.27/2.60 | | | | (27) $false % 13.27/2.60 | | | | % 13.27/2.60 | | | | CLOSE: (27) is inconsistent. % 13.27/2.60 | | | | % 13.27/2.60 | | | Case 2: % 13.27/2.60 | | | | % 13.27/2.60 | | | | (28) ? [v0: int] : ( ~ (v0 = 0) & in(0, all_13_8) = v0) % 13.27/2.60 | | | | % 13.27/2.60 | | | | DELTA: instantiating (28) with fresh symbol all_124_0 gives: % 13.27/2.60 | | | | (29) ~ (all_124_0 = 0) & in(0, all_13_8) = all_124_0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | ALPHA: (29) implies: % 13.27/2.60 | | | | (30) ~ (all_124_0 = 0) % 13.27/2.60 | | | | (31) in(0, all_13_8) = all_124_0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | GROUND_INST: instantiating (7) with 0, all_13_8, all_13_7, all_13_6, % 13.27/2.60 | | | | simplifying with (5), (15), (22) gives: % 13.27/2.60 | | | | (32) all_13_7 = 0 | in(0, all_13_8) = 0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | BETA: splitting (32) gives: % 13.27/2.60 | | | | % 13.27/2.60 | | | | Case 1: % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | (33) in(0, all_13_8) = 0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | GROUND_INST: instantiating (11) with all_124_0, 0, all_13_8, 0, % 13.27/2.60 | | | | | simplifying with (31), (33) gives: % 13.27/2.60 | | | | | (34) all_124_0 = 0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | REDUCE: (30), (34) imply: % 13.27/2.60 | | | | | (35) $false % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | CLOSE: (35) is inconsistent. % 13.27/2.60 | | | | | % 13.27/2.60 | | | | Case 2: % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | (36) all_13_7 = 0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | REDUCE: (21), (36) imply: % 13.27/2.60 | | | | | (37) $false % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | CLOSE: (37) is inconsistent. % 13.27/2.60 | | | | | % 13.27/2.60 | | | | End of split % 13.27/2.60 | | | | % 13.27/2.60 | | | End of split % 13.27/2.60 | | | % 13.27/2.60 | | End of split % 13.27/2.60 | | % 13.27/2.60 | Case 2: % 13.27/2.60 | | % 13.27/2.60 | | (38) $difference(all_48_0, all_48_1) = -1 % 13.27/2.60 | | % 13.27/2.60 | | COMBINE_EQS: (13), (38) imply: % 13.27/2.60 | | (39) all_48_1 = all_13_0 % 13.27/2.60 | | % 13.27/2.60 | | COMBINE_EQS: (1), (39) imply: % 13.27/2.60 | | (40) all_13_0 = all_13_3 % 13.27/2.60 | | % 13.27/2.60 | | SIMP: (40) implies: % 13.27/2.60 | | (41) all_13_0 = all_13_3 % 13.27/2.60 | | % 13.27/2.60 | | REDUCE: (2), (41) imply: % 13.27/2.60 | | (42) $false % 13.27/2.60 | | % 13.27/2.60 | | CLOSE: (42) is inconsistent. % 13.27/2.60 | | % 13.27/2.60 | End of split % 13.27/2.60 | % 13.27/2.60 End of proof % 13.27/2.60 % 13.27/2.60 Sub-proof #2 shows that the following formulas are inconsistent: % 13.27/2.60 ---------------------------------------------------------------- % 13.27/2.60 (1) ~ (all_13_0 = all_13_3) % 13.27/2.60 (2) in(0, all_13_8) = 0 % 13.27/2.60 (3) all_58_0 = all_13_0 % 13.27/2.60 (4) ! [v0: int] : ! [v1: collection] : ! [v2: int] : ! [v3: collection] : % 13.27/2.60 ! [v4: int] : (v4 = 0 | ~ (add(v2, v1) = v3) | ~ (in(v0, v3) = v4) | % 13.27/2.60 ~ collection(v1) | ( ~ (v2 = v0) & ? [v5: int] : ( ~ (v5 = 0) & in(v0, % 13.27/2.60 v1) = v5))) % 13.27/2.60 (5) all_40_0 = 0 | all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, % 13.27/2.60 all_13_6) = v0) % 13.27/2.60 (6) collection(all_13_8) % 13.27/2.60 (7) ~ (all_13_7 = 0) % 13.27/2.60 (8) all_58_2 = all_40_0 % 13.27/2.60 (9) ~ (all_58_2 = 0) | all_58_0 = all_58_1 % 13.27/2.60 (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 13.27/2.60 collection] : ! [v3: int] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ % 13.27/2.60 (in(v3, v2) = v0)) % 13.27/2.60 (11) all_58_1 = all_13_3 % 13.27/2.60 (12) add(all_13_7, all_13_8) = all_13_6 % 13.27/2.60 % 13.27/2.60 Begin of proof % 13.27/2.60 | % 13.27/2.60 | BETA: splitting (9) gives: % 13.27/2.60 | % 13.27/2.60 | Case 1: % 13.27/2.60 | | % 13.27/2.60 | | (13) ~ (all_58_2 = 0) % 13.27/2.60 | | % 13.27/2.60 | | REDUCE: (8), (13) imply: % 13.27/2.60 | | (14) ~ (all_40_0 = 0) % 13.27/2.60 | | % 13.27/2.60 | | BETA: splitting (5) gives: % 13.27/2.60 | | % 13.27/2.60 | | Case 1: % 13.27/2.60 | | | % 13.27/2.60 | | | (15) all_40_0 = 0 % 13.27/2.60 | | | % 13.27/2.60 | | | REDUCE: (14), (15) imply: % 13.27/2.60 | | | (16) $false % 13.27/2.60 | | | % 13.27/2.60 | | | CLOSE: (16) is inconsistent. % 13.27/2.60 | | | % 13.27/2.60 | | Case 2: % 13.27/2.60 | | | % 13.27/2.60 | | | (17) all_13_7 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(0, all_13_6) = v0) % 13.27/2.60 | | | % 13.27/2.60 | | | BETA: splitting (17) gives: % 13.27/2.60 | | | % 13.27/2.60 | | | Case 1: % 13.27/2.60 | | | | % 13.27/2.60 | | | | (18) all_13_7 = 0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | REDUCE: (7), (18) imply: % 13.27/2.60 | | | | (19) $false % 13.27/2.60 | | | | % 13.27/2.60 | | | | CLOSE: (19) is inconsistent. % 13.27/2.60 | | | | % 13.27/2.60 | | | Case 2: % 13.27/2.60 | | | | % 13.27/2.60 | | | | (20) ? [v0: int] : ( ~ (v0 = 0) & in(0, all_13_6) = v0) % 13.27/2.60 | | | | % 13.27/2.60 | | | | DELTA: instantiating (20) with fresh symbol all_127_0 gives: % 13.27/2.60 | | | | (21) ~ (all_127_0 = 0) & in(0, all_13_6) = all_127_0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | ALPHA: (21) implies: % 13.27/2.60 | | | | (22) ~ (all_127_0 = 0) % 13.27/2.60 | | | | (23) in(0, all_13_6) = all_127_0 % 13.27/2.60 | | | | % 13.27/2.60 | | | | GROUND_INST: instantiating (4) with 0, all_13_8, all_13_7, all_13_6, % 13.27/2.60 | | | | all_127_0, simplifying with (6), (12), (23) gives: % 13.27/2.60 | | | | (24) all_127_0 = 0 | ( ~ (all_13_7 = 0) & ? [v0: int] : ( ~ (v0 = 0) % 13.27/2.60 | | | | & in(0, all_13_8) = v0)) % 13.27/2.60 | | | | % 13.27/2.60 | | | | BETA: splitting (24) gives: % 13.27/2.60 | | | | % 13.27/2.60 | | | | Case 1: % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | (25) all_127_0 = 0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | REDUCE: (22), (25) imply: % 13.27/2.60 | | | | | (26) $false % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | CLOSE: (26) is inconsistent. % 13.27/2.60 | | | | | % 13.27/2.60 | | | | Case 2: % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | (27) ~ (all_13_7 = 0) & ? [v0: int] : ( ~ (v0 = 0) & in(0, % 13.27/2.60 | | | | | all_13_8) = v0) % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | ALPHA: (27) implies: % 13.27/2.60 | | | | | (28) ? [v0: int] : ( ~ (v0 = 0) & in(0, all_13_8) = v0) % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | DELTA: instantiating (28) with fresh symbol all_140_0 gives: % 13.27/2.60 | | | | | (29) ~ (all_140_0 = 0) & in(0, all_13_8) = all_140_0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | ALPHA: (29) implies: % 13.27/2.60 | | | | | (30) ~ (all_140_0 = 0) % 13.27/2.60 | | | | | (31) in(0, all_13_8) = all_140_0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | GROUND_INST: instantiating (10) with 0, all_140_0, all_13_8, 0, % 13.27/2.60 | | | | | simplifying with (2), (31) gives: % 13.27/2.60 | | | | | (32) all_140_0 = 0 % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | REDUCE: (30), (32) imply: % 13.27/2.60 | | | | | (33) $false % 13.27/2.60 | | | | | % 13.27/2.60 | | | | | CLOSE: (33) is inconsistent. % 13.27/2.60 | | | | | % 13.27/2.60 | | | | End of split % 13.27/2.60 | | | | % 13.27/2.60 | | | End of split % 13.27/2.60 | | | % 13.27/2.60 | | End of split % 13.27/2.60 | | % 13.27/2.60 | Case 2: % 13.27/2.60 | | % 13.27/2.60 | | (34) all_58_0 = all_58_1 % 13.27/2.60 | | % 13.27/2.60 | | COMBINE_EQS: (3), (34) imply: % 13.27/2.60 | | (35) all_58_1 = all_13_0 % 13.27/2.60 | | % 13.27/2.60 | | SIMP: (35) implies: % 13.27/2.60 | | (36) all_58_1 = all_13_0 % 13.27/2.60 | | % 13.27/2.60 | | COMBINE_EQS: (11), (36) imply: % 13.27/2.60 | | (37) all_13_0 = all_13_3 % 13.27/2.60 | | % 13.27/2.60 | | SIMP: (37) implies: % 13.27/2.60 | | (38) all_13_0 = all_13_3 % 13.27/2.60 | | % 13.27/2.60 | | REDUCE: (1), (38) imply: % 13.27/2.60 | | (39) $false % 13.27/2.60 | | % 13.27/2.60 | | CLOSE: (39) is inconsistent. % 13.27/2.60 | | % 13.27/2.60 | End of split % 13.27/2.60 | % 13.27/2.60 End of proof % 13.27/2.60 % SZS output end Proof for theBenchmark % 13.27/2.60 % 13.27/2.60 2011ms %------------------------------------------------------------------------------