%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW584_2 : TPTP v8.1.2. Released v6.1.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 : Fri Sep 1 00:50:48 EDT 2023 % Result : Theorem 17.26s 3.03s % Output : Proof 29.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWW584_2 : TPTP v8.1.2. Released v6.1.0. % 0.04/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 19:03:10 EDT 2023 % 0.12/0.34 % CPUTime : % 0.53/0.59 ________ _____ % 0.53/0.59 ___ __ \_________(_)________________________________ % 0.53/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.53/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.53/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.53/0.59 % 0.53/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.53/0.59 (2023-06-19) % 0.53/0.59 % 0.53/0.59 (c) Philipp Rümmer, 2009-2023 % 0.53/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.53/0.59 Amanda Stjerna. % 0.53/0.59 Free software under BSD-3-Clause. % 0.53/0.59 % 0.53/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.53/0.59 % 0.53/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.53/0.61 Running up to 7 provers in parallel. % 0.53/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.53/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.53/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.53/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.53/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.53/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.53/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 3.70/1.20 Prover 0: Preprocessing ... % 3.70/1.20 Prover 2: Preprocessing ... % 3.70/1.20 Prover 6: Preprocessing ... % 3.70/1.20 Prover 5: Preprocessing ... % 3.70/1.20 Prover 1: Preprocessing ... % 3.70/1.20 Prover 4: Preprocessing ... % 3.70/1.20 Prover 3: Preprocessing ... % 8.06/1.81 Prover 1: Warning: ignoring some quantifiers % 8.61/1.85 Prover 3: Warning: ignoring some quantifiers % 8.61/1.91 Prover 4: Warning: ignoring some quantifiers % 8.61/1.92 Prover 1: Constructing countermodel ... % 8.61/1.92 Prover 3: Constructing countermodel ... % 9.11/1.92 Prover 6: Proving ... % 9.11/1.92 Prover 0: Proving ... % 9.11/1.92 Prover 5: Proving ... % 9.11/1.93 Prover 4: Constructing countermodel ... % 9.40/2.01 Prover 2: Proving ... % 14.02/2.59 Prover 3: gave up % 14.02/2.60 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.64/2.71 Prover 7: Preprocessing ... % 16.09/2.86 Prover 1: gave up % 16.09/2.88 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.09/2.88 Prover 7: Warning: ignoring some quantifiers % 16.35/2.92 Prover 7: Constructing countermodel ... % 16.35/2.93 Prover 8: Preprocessing ... % 17.26/3.03 Prover 0: proved (2415ms) % 17.26/3.03 % 17.26/3.03 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.26/3.03 % 17.26/3.03 Prover 2: stopped % 17.26/3.04 Prover 6: stopped % 17.26/3.04 Prover 5: stopped % 17.26/3.04 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 17.26/3.04 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 17.26/3.04 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 17.26/3.04 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 17.65/3.07 Prover 8: Warning: ignoring some quantifiers % 17.65/3.09 Prover 8: Constructing countermodel ... % 17.65/3.11 Prover 10: Preprocessing ... % 17.65/3.13 Prover 11: Preprocessing ... % 17.65/3.14 Prover 13: Preprocessing ... % 17.65/3.15 Prover 16: Preprocessing ... % 19.07/3.24 Prover 10: Warning: ignoring some quantifiers % 19.23/3.27 Prover 10: Constructing countermodel ... % 19.23/3.27 Prover 11: Warning: ignoring some quantifiers % 19.23/3.28 Prover 11: Constructing countermodel ... % 19.23/3.28 Prover 13: Warning: ignoring some quantifiers % 19.23/3.29 Prover 16: Warning: ignoring some quantifiers % 19.23/3.30 Prover 13: Constructing countermodel ... % 19.23/3.30 Prover 16: Constructing countermodel ... % 22.44/3.71 Prover 8: gave up % 22.44/3.72 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 23.28/3.79 Prover 13: gave up % 23.28/3.80 Prover 19: Preprocessing ... % 23.28/3.83 Prover 10: gave up % 24.48/3.93 Prover 19: Warning: ignoring some quantifiers % 24.48/3.96 Prover 19: Constructing countermodel ... % 26.25/4.23 Prover 16: gave up % 28.53/4.53 Prover 19: gave up % 28.97/4.54 Prover 11: Found proof (size 235) % 28.97/4.54 Prover 11: proved (1501ms) % 28.97/4.54 Prover 7: stopped % 28.97/4.54 Prover 4: stopped % 28.97/4.54 % 28.97/4.54 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.97/4.54 % 28.97/4.56 % SZS output start Proof for theBenchmark % 29.12/4.56 Assumptions after simplification: % 29.12/4.56 --------------------------------- % 29.12/4.57 % 29.12/4.57 (bridgeR) % 29.12/4.58 ! [v0: uni] : ! [v1: int] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | t2tb(v1) = % 29.12/4.58 v0) % 29.12/4.58 % 29.12/4.58 (bridgeR1) % 29.12/4.58 ! [v0: uni] : ! [v1: array_int] : ( ~ (tb2t1(v0) = v1) | ~ uni(v0) | % 29.12/4.58 t2tb1(v1) = v0) % 29.12/4.58 % 29.12/4.58 (contents_def1) % 29.12/4.58 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (mk_ref(v0, v1) = v2) | ~ % 29.12/4.58 ty(v0) | ~ uni(v1) | ? [v3: int] : ? [v4: uni] : ((v4 = v1 & contents(v0, % 29.12/4.58 v2) = v1) | ( ~ (v3 = 0) & sort1(v0, v1) = v3))) & ! [v0: ty] : ! % 29.12/4.58 [v1: uni] : ( ~ (sort1(v0, v1) = 0) | ~ ty(v0) | ~ uni(v1) | ? [v2: uni] : % 29.12/4.58 (contents(v0, v2) = v1 & mk_ref(v0, v1) = v2 & uni(v2))) % 29.12/4.58 % 29.12/4.58 (decrease1_def) % 29.12/4.59 ty(int) & ! [v0: array_int] : ! [v1: int] : (v1 = 0 | ~ (decrease11(v0) = % 29.12/4.59 v1) | ~ array_int(v0) | ? [v2: uni] : ? [v3: int] : ? [v4: int] : ? % 29.12/4.59 [v5: uni] : ? [v6: int] : ? [v7: uni] : ? [v8: int] : ($lesseq(2, % 29.12/4.59 $difference(v8, v6)) & $lesseq(2, $difference(v3, v4)) & $lesseq(0, v4) % 29.12/4.59 & t2tb1(v0) = v2 & tb2t(v7) = v8 & tb2t(v5) = v6 & get2(int, v2, $sum(v4, % 29.12/4.59 1)) = v5 & get2(int, v2, v4) = v7 & length1(int, v2) = v3 & uni(v7) & % 29.12/4.59 uni(v5) & uni(v2))) & ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = % 29.12/4.59 v1) | ~ array_int(v0) | ? [v2: int] : ? [v3: int] : ? [v4: int] : ? % 29.12/4.59 [v5: uni] : ? [v6: int] : ? [v7: uni] : ? [v8: int] : ((v3 = 0 & % 29.12/4.59 decrease11(v0) = 0) | ($lesseq(2, $difference(v8, v6)) & $lesseq(2, % 29.12/4.59 $difference(v2, v4)) & $lesseq(0, v4) & tb2t(v7) = v8 & tb2t(v5) = v6 % 29.12/4.59 & get2(int, v1, $sum(v4, 1)) = v5 & get2(int, v1, v4) = v7 & % 29.12/4.59 length1(int, v1) = v2 & uni(v7) & uni(v5)))) & ! [v0: array_int] : ! % 29.12/4.59 [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ array_int(v0) | ? [v2: int] : ? [v3: % 29.12/4.59 int] : (( ~ (v2 = 0) & decrease11(v0) = v2) | (length1(int, v1) = v3 & ! % 29.12/4.59 [v4: int] : ! [v5: uni] : ( ~ ($lesseq(2, $difference(v3, v4))) | ~ % 29.12/4.59 ($lesseq(0, v4)) | ~ (get2(int, v1, $sum(v4, 1)) = v5) | ? [v6: int] % 29.12/4.59 : ? [v7: uni] : ? [v8: int] : ($lesseq(-1, $difference(v6, v8)) & % 29.12/4.59 tb2t(v7) = v8 & tb2t(v5) = v6 & get2(int, v1, v4) = v7 & uni(v7))) & % 29.12/4.59 ! [v4: int] : ! [v5: uni] : ( ~ ($lesseq(2, $difference(v3, v4))) | ~ % 29.12/4.59 ($lesseq(0, v4)) | ~ (get2(int, v1, v4) = v5) | ? [v6: uni] : ? % 29.12/4.59 [v7: int] : ? [v8: int] : ($lesseq(-1, $difference(v7, v8)) & % 29.12/4.59 tb2t(v6) = v7 & tb2t(v5) = v8 & get2(int, v1, $sum(v4, 1)) = v6 & % 29.12/4.59 uni(v6)))))) & ! [v0: array_int] : ( ~ (decrease11(v0) = 0) | ~ % 29.12/4.59 array_int(v0) | ? [v1: uni] : ? [v2: int] : (t2tb1(v0) = v1 & length1(int, % 29.12/4.59 v1) = v2 & uni(v1) & ! [v3: int] : ! [v4: uni] : ( ~ ($lesseq(2, % 29.12/4.59 $difference(v2, v3))) | ~ ($lesseq(0, v3)) | ~ (get2(int, v1, % 29.12/4.59 $sum(v3, 1)) = v4) | ? [v5: int] : ? [v6: uni] : ? [v7: int] : % 29.12/4.59 ($lesseq(-1, $difference(v5, v7)) & tb2t(v6) = v7 & tb2t(v4) = v5 & % 29.12/4.59 get2(int, v1, v3) = v6 & uni(v6))) & ! [v3: int] : ! [v4: uni] : ( ~ % 29.12/4.59 ($lesseq(2, $difference(v2, v3))) | ~ ($lesseq(0, v3)) | ~ (get2(int, % 29.12/4.59 v1, v3) = v4) | ? [v5: uni] : ? [v6: int] : ? [v7: int] : % 29.12/4.59 ($lesseq(-1, $difference(v6, v7)) & tb2t(v5) = v6 & tb2t(v4) = v7 & % 29.12/4.59 get2(int, v1, $sum(v3, 1)) = v5 & uni(v5))))) % 29.12/4.59 % 29.12/4.59 (decrease1_induction) % 29.12/4.60 ty(int) & ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 29.12/4.60 array_int(v0) | ? [v2: int] : ? [v3: int] : (( ~ (v2 = 0) & decrease11(v0) % 29.12/4.60 = v2) | (length1(int, v1) = v3 & ! [v4: int] : ! [v5: int] : ! [v6: % 29.12/4.60 uni] : ! [v7: int] : ! [v8: uni] : ! [v9: int] : ( ~ ($lesseq(1, % 29.12/4.60 $sum($difference($difference(v9, v7), v5), v4))) | ~ ($lesseq(1, % 29.12/4.60 $difference(v3, v5))) | ~ ($lesseq(v4, v5)) | ~ ($lesseq(0, v4)) % 29.12/4.60 | ~ (tb2t(v8) = v9) | ~ (tb2t(v6) = v7) | ~ (get2(int, v1, v5) = % 29.12/4.60 v6) | ~ (get2(int, v1, v4) = v8))))) & ! [v0: array_int] : ( ~ % 29.12/4.60 (decrease11(v0) = 0) | ~ array_int(v0) | ? [v1: uni] : ? [v2: int] : % 29.12/4.60 (t2tb1(v0) = v1 & length1(int, v1) = v2 & uni(v1) & ! [v3: int] : ! [v4: % 29.12/4.60 int] : ! [v5: uni] : ! [v6: int] : ! [v7: uni] : ! [v8: int] : ( ~ % 29.12/4.60 ($lesseq(1, $sum($difference($difference(v8, v6), v4), v3))) | ~ % 29.12/4.60 ($lesseq(1, $difference(v2, v4))) | ~ ($lesseq(v3, v4)) | ~ % 29.12/4.60 ($lesseq(0, v3)) | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 29.12/4.60 (get2(int, v1, v4) = v5) | ~ (get2(int, v1, v3) = v7)))) % 29.12/4.60 % 29.12/4.60 (elts_def1) % 29.12/4.60 ty(int) & ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 29.12/4.60 (mk_array1(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ? [v4: ty] : ? % 29.12/4.60 [v5: int] : ? [v6: uni] : ((v6 = v2 & elts(v0, v3) = v2) | ( ~ (v5 = 0) & % 29.12/4.60 map(int, v0) = v4 & sort1(v4, v2) = v5 & ty(v4)))) % 29.12/4.60 % 29.12/4.60 (get_def) % 29.12/4.60 ty(int) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: % 29.12/4.60 uni] : ! [v5: uni] : ( ~ (t2tb(v2) = v4) | ~ (elts(v0, v1) = v3) | ~ % 29.12/4.60 (get(v0, int, v3, v4) = v5) | ~ ty(v0) | ~ uni(v1) | (get2(v0, v1, v2) = % 29.12/4.60 v5 & uni(v5))) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] % 29.12/4.60 : ( ~ (get2(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v1) | ? [v4: uni] : ? % 29.12/4.60 [v5: uni] : (t2tb(v2) = v5 & elts(v0, v1) = v4 & get(v0, int, v4, v5) = v3 & % 29.12/4.60 uni(v5) & uni(v4) & uni(v3))) % 29.12/4.60 % 29.12/4.60 (get_sort2) % 29.12/4.60 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ % 29.12/4.60 (get(v1, v0, v2, v3) = v4) | ~ ty(v1) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) % 29.12/4.60 | sort1(v1, v4) = 0) % 29.12/4.60 % 29.12/4.60 (length_def1) % 29.12/4.60 ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ (mk_array1(v0, % 29.12/4.60 v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | length1(v0, v3) = v1) % 29.12/4.60 % 29.12/4.60 (mk_ref_sort1) % 29.12/4.60 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (mk_ref(v0, v1) = v2) | ~ % 29.12/4.60 ty(v0) | ~ uni(v1) | ? [v3: ty] : (ref(v0) = v3 & sort1(v3, v2) = 0 & % 29.12/4.60 ty(v3))) % 29.12/4.60 % 29.12/4.60 (ref_inversion1) % 29.12/4.60 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (contents(v0, v1) = v2) | ~ % 29.12/4.60 ty(v0) | ~ uni(v1) | ? [v3: ty] : ? [v4: int] : ? [v5: uni] : ((v5 = v1 % 29.12/4.60 & mk_ref(v0, v2) = v1) | ( ~ (v4 = 0) & ref(v0) = v3 & sort1(v3, v1) = % 29.12/4.60 v4 & ty(v3)))) & ! [v0: ty] : ! [v1: uni] : ! [v2: ty] : ( ~ (ref(v0) % 29.12/4.60 = v2) | ~ (sort1(v2, v1) = 0) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : % 29.12/4.60 (contents(v0, v1) = v3 & mk_ref(v0, v3) = v1 & uni(v3))) % 29.12/4.60 % 29.12/4.60 (t2tb_sort2) % 29.12/4.60 ty(int) & ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : % 29.12/4.60 ! [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort1(v0, v2) = % 29.12/4.60 0)) % 29.12/4.60 % 29.12/4.60 (wP_parameter_search_rec) % 29.12/4.61 ty(int) & ? [v0: int] : ? [v1: map_int_int] : ? [v2: int] : ? [v3: uni] : % 29.12/4.61 ? [v4: uni] : ? [v5: array_int] : ? [v6: uni] : ? [v7: uni] : ? [v8: int] % 29.12/4.61 : ? [v9: int] : ? [v10: uni] : ? [v11: uni] : ? [v12: int] : ? [v13: int] % 29.12/4.61 : ? [v14: uni] : ? [v15: uni] : ? [v16: int] : ? [v17: int] : ? [v18: % 29.12/4.61 uni] : ? [v19: uni] : ? [v20: int] : ($lesseq(0, $sum(v8, v2)) & % 29.12/4.61 $lesseq(1, v8) & $lesseq(1, $difference(v0, v2)) & $lesseq(0, v2) & % 29.12/4.61 t2tb2(v1) = v3 & decrease11(v5) = 0 & tb2t1(v4) = v5 & tb2t(v7) = v8 & % 29.12/4.61 t2tb(v2) = v6 & mk_array1(int, v0, v3) = v4 & get(int, int, v3, v6) = v7 & % 29.12/4.61 map_int_int(v1) & array_int(v5) & uni(v7) & uni(v6) & uni(v4) & uni(v3) & ( % 29.12/4.61 ~ (v9 = -1) | (v20 = 0 & $lesseq(1, $difference(v0, v17)) & $lesseq(v2, % 29.12/4.61 v17) & tb2t(v19) = 0 & t2tb(v17) = v18 & get(int, int, v3, v18) = v19 % 29.12/4.61 & uni(v19) & uni(v18))) & ( ~ ($lesseq(1, $difference(v0, v9))) | ~ % 29.12/4.61 ($lesseq(v2, v9)) | (v16 = 0 & $lesseq(1, $difference(v9, v13)) & % 29.12/4.61 $lesseq(v2, v13) & tb2t(v15) = 0 & t2tb(v13) = v14 & get(int, int, v3, % 29.12/4.61 v14) = v15 & uni(v15) & uni(v14)) | ( ~ (v12 = 0) & tb2t(v11) = v12 & % 29.12/4.61 t2tb(v9) = v10 & get(int, int, v3, v10) = v11 & uni(v11) & uni(v10))) & % 29.12/4.61 ((v12 = 0 & $lesseq(1, $difference(v0, v9)) & $lesseq(v2, $difference(v9, % 29.12/4.61 v8)) & tb2t(v11) = 0 & t2tb(v9) = v10 & get(int, int, v3, v10) = v11 % 29.12/4.61 & uni(v11) & uni(v10) & ! [v21: int] : ! [v22: uni] : ( ~ ($lesseq(1, % 29.12/4.61 $difference(v9, v21))) | ~ ($lesseq(v2, $difference(v21, v8))) | % 29.12/4.61 ~ (t2tb(v21) = v22) | ? [v23: uni] : ? [v24: int] : ( ~ (v24 = 0) & % 29.12/4.61 tb2t(v23) = v24 & get(int, int, v3, v22) = v23 & uni(v23)))) | (v9 = % 29.12/4.61 -1 & ! [v21: int] : ! [v22: uni] : ( ~ ($lesseq(1, $difference(v0, % 29.12/4.61 v21))) | ~ ($lesseq(v2, $difference(v21, v8))) | ~ (t2tb(v21) % 29.12/4.61 = v22) | ? [v23: uni] : ? [v24: int] : ( ~ (v24 = 0) & tb2t(v23) = % 29.12/4.61 v24 & get(int, int, v3, v22) = v23 & uni(v23)))))) % 29.12/4.61 % 29.12/4.61 (function-axioms) % 29.12/4.61 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 29.12/4.61 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 29.12/4.61 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 29.12/4.61 : ! [v3: int] : ! [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ (set2(v5, v4, v3, % 29.12/4.61 v2) = v1) | ~ (set2(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 29.12/4.61 uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | % 29.12/4.61 ~ (get(v5, v4, v3, v2) = v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] % 29.12/4.61 : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : % 29.12/4.61 (v1 = v0 | ~ (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, % 29.12/4.61 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : % 29.12/4.61 ! [v4: ty] : (v1 = v0 | ~ (make1(v4, v3, v2) = v1) | ~ (make1(v4, v3, v2) = % 29.12/4.61 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: % 29.12/4.61 ty] : (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) & % 29.12/4.61 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : (v1 = % 29.12/4.61 v0 | ~ (mk_array1(v4, v3, v2) = v1) | ~ (mk_array1(v4, v3, v2) = v0)) & ! % 29.12/4.61 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 % 29.12/4.61 | ~ (const(v4, v3, v2) = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: uni] % 29.12/4.61 : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (elts(v3, v2) = % 29.12/4.61 v1) | ~ (elts(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] % 29.12/4.61 : ! [v3: ty] : (v1 = v0 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = % 29.12/4.61 v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | % 29.12/4.61 ~ (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] % 29.12/4.61 : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ % 29.12/4.61 (contents(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 29.12/4.61 [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & % 29.12/4.61 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! % 29.12/4.61 [v3: ty] : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! % 29.12/4.61 [v0: map_int_int] : ! [v1: map_int_int] : ! [v2: uni] : (v1 = v0 | ~ % 29.12/4.61 (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 29.12/4.61 [v2: map_int_int] : (v1 = v0 | ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! % 29.12/4.61 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: array_int] : % 29.12/4.61 (v1 = v0 | ~ (decrease11(v2) = v1) | ~ (decrease11(v2) = v0)) & ! [v0: % 29.12/4.61 array_int] : ! [v1: array_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = % 29.12/4.61 v1) | ~ (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 29.12/4.61 array_int] : (v1 = v0 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: % 29.12/4.61 int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ % 29.12/4.61 (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | % 29.12/4.61 ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! % 29.12/4.61 [v2: ty] : (v1 = v0 | ~ (array(v2) = v1) | ~ (array(v2) = v0)) & ! [v0: ty] % 29.12/4.61 : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (ref(v2) = v1) | ~ (ref(v2) = % 29.12/4.61 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ % 29.12/4.61 (witness1(v2) = v1) | ~ (witness1(v2) = v0)) % 29.12/4.61 % 29.12/4.61 Further assumptions not needed in the proof: % 29.12/4.61 -------------------------------------------- % 29.12/4.61 array_inversion1, bool_inversion, bridgeL, bridgeL1, bridgeL2, bridgeR2, % 29.12/4.61 compatOrderMult, const, const_sort1, contents_sort1, elts_sort1, get_sort3, % 29.12/4.61 make_def, make_sort1, match_bool_False, match_bool_True, match_bool_sort1, % 29.12/4.61 mk_array_sort1, select_eq, select_neq, set_def, set_sort2, set_sort3, t2tb_sort, % 29.12/4.61 t2tb_sort1, true_False, tuple0_inversion, witness_sort1 % 29.12/4.61 % 29.12/4.61 Those formulas are unsatisfiable: % 29.12/4.61 --------------------------------- % 29.12/4.61 % 29.12/4.61 Begin of proof % 29.12/4.61 | % 29.12/4.61 | ALPHA: (contents_def1) implies: % 29.12/4.62 | (1) ! [v0: ty] : ! [v1: uni] : ( ~ (sort1(v0, v1) = 0) | ~ ty(v0) | ~ % 29.12/4.62 | uni(v1) | ? [v2: uni] : (contents(v0, v2) = v1 & mk_ref(v0, v1) = v2 % 29.12/4.62 | & uni(v2))) % 29.12/4.62 | % 29.12/4.62 | ALPHA: (ref_inversion1) implies: % 29.12/4.62 | (2) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (contents(v0, v1) = v2) % 29.12/4.62 | | ~ ty(v0) | ~ uni(v1) | ? [v3: ty] : ? [v4: int] : ? [v5: uni] % 29.12/4.62 | : ((v5 = v1 & mk_ref(v0, v2) = v1) | ( ~ (v4 = 0) & ref(v0) = v3 & % 29.12/4.62 | sort1(v3, v1) = v4 & ty(v3)))) % 29.12/4.62 | % 29.12/4.62 | ALPHA: (elts_def1) implies: % 29.12/4.62 | (3) ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 29.12/4.62 | (mk_array1(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ? [v4: ty] : % 29.12/4.62 | ? [v5: int] : ? [v6: uni] : ((v6 = v2 & elts(v0, v3) = v2) | ( ~ % 29.12/4.62 | (v5 = 0) & map(int, v0) = v4 & sort1(v4, v2) = v5 & ty(v4)))) % 29.12/4.62 | % 29.12/4.62 | ALPHA: (get_def) implies: % 29.12/4.62 | (4) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: uni] % 29.12/4.62 | : ! [v5: uni] : ( ~ (t2tb(v2) = v4) | ~ (elts(v0, v1) = v3) | ~ % 29.12/4.62 | (get(v0, int, v3, v4) = v5) | ~ ty(v0) | ~ uni(v1) | (get2(v0, v1, % 29.12/4.62 | v2) = v5 & uni(v5))) % 29.12/4.62 | % 29.12/4.62 | ALPHA: (decrease1_def) implies: % 29.12/4.62 | (5) ! [v0: array_int] : ( ~ (decrease11(v0) = 0) | ~ array_int(v0) | ? % 29.12/4.62 | [v1: uni] : ? [v2: int] : (t2tb1(v0) = v1 & length1(int, v1) = v2 & % 29.12/4.62 | uni(v1) & ! [v3: int] : ! [v4: uni] : ( ~ ($lesseq(2, % 29.12/4.62 | $difference(v2, v3))) | ~ ($lesseq(0, v3)) | ~ (get2(int, % 29.12/4.62 | v1, $sum(v3, 1)) = v4) | ? [v5: int] : ? [v6: uni] : ? % 29.12/4.62 | [v7: int] : ($lesseq(-1, $difference(v5, v7)) & tb2t(v6) = v7 & % 29.12/4.62 | tb2t(v4) = v5 & get2(int, v1, v3) = v6 & uni(v6))) & ! [v3: % 29.12/4.62 | int] : ! [v4: uni] : ( ~ ($lesseq(2, $difference(v2, v3))) | ~ % 29.12/4.62 | ($lesseq(0, v3)) | ~ (get2(int, v1, v3) = v4) | ? [v5: uni] : % 29.12/4.62 | ? [v6: int] : ? [v7: int] : ($lesseq(-1, $difference(v6, v7)) & % 29.12/4.62 | tb2t(v5) = v6 & tb2t(v4) = v7 & get2(int, v1, $sum(v3, 1)) = v5 % 29.12/4.62 | & uni(v5))))) % 29.12/4.62 | (6) ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 29.12/4.62 | array_int(v0) | ? [v2: int] : ? [v3: int] : (( ~ (v2 = 0) & % 29.12/4.62 | decrease11(v0) = v2) | (length1(int, v1) = v3 & ! [v4: int] : ! % 29.12/4.62 | [v5: uni] : ( ~ ($lesseq(2, $difference(v3, v4))) | ~ % 29.12/4.62 | ($lesseq(0, v4)) | ~ (get2(int, v1, $sum(v4, 1)) = v5) | ? % 29.12/4.62 | [v6: int] : ? [v7: uni] : ? [v8: int] : ($lesseq(-1, % 29.12/4.62 | $difference(v6, v8)) & tb2t(v7) = v8 & tb2t(v5) = v6 & % 29.12/4.62 | get2(int, v1, v4) = v7 & uni(v7))) & ! [v4: int] : ! [v5: % 29.12/4.62 | uni] : ( ~ ($lesseq(2, $difference(v3, v4))) | ~ ($lesseq(0, % 29.12/4.62 | v4)) | ~ (get2(int, v1, v4) = v5) | ? [v6: uni] : ? [v7: % 29.12/4.62 | int] : ? [v8: int] : ($lesseq(-1, $difference(v7, v8)) & % 29.12/4.62 | tb2t(v6) = v7 & tb2t(v5) = v8 & get2(int, v1, $sum(v4, 1)) = % 29.12/4.62 | v6 & uni(v6)))))) % 29.12/4.62 | % 29.12/4.62 | ALPHA: (decrease1_induction) implies: % 29.12/4.62 | (7) ! [v0: array_int] : ( ~ (decrease11(v0) = 0) | ~ array_int(v0) | ? % 29.12/4.62 | [v1: uni] : ? [v2: int] : (t2tb1(v0) = v1 & length1(int, v1) = v2 & % 29.12/4.62 | uni(v1) & ! [v3: int] : ! [v4: int] : ! [v5: uni] : ! [v6: int] % 29.12/4.62 | : ! [v7: uni] : ! [v8: int] : ( ~ ($lesseq(1, % 29.12/4.62 | $sum($difference($difference(v8, v6), v4), v3))) | ~ % 29.12/4.62 | ($lesseq(1, $difference(v2, v4))) | ~ ($lesseq(v3, v4)) | ~ % 29.12/4.62 | ($lesseq(0, v3)) | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 29.12/4.62 | (get2(int, v1, v4) = v5) | ~ (get2(int, v1, v3) = v7)))) % 29.12/4.62 | (8) ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 29.12/4.62 | array_int(v0) | ? [v2: int] : ? [v3: int] : (( ~ (v2 = 0) & % 29.12/4.62 | decrease11(v0) = v2) | (length1(int, v1) = v3 & ! [v4: int] : ! % 29.12/4.62 | [v5: int] : ! [v6: uni] : ! [v7: int] : ! [v8: uni] : ! [v9: % 29.12/4.62 | int] : ( ~ ($lesseq(1, $sum($difference($difference(v9, v7), % 29.43/4.63 | v5), v4))) | ~ ($lesseq(1, $difference(v3, v5))) | ~ % 29.43/4.63 | ($lesseq(v4, v5)) | ~ ($lesseq(0, v4)) | ~ (tb2t(v8) = v9) | % 29.43/4.63 | ~ (tb2t(v6) = v7) | ~ (get2(int, v1, v5) = v6) | ~ (get2(int, % 29.43/4.63 | v1, v4) = v8))))) % 29.43/4.63 | % 29.43/4.63 | ALPHA: (t2tb_sort2) implies: % 29.43/4.63 | (9) ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : ! % 29.43/4.63 | [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort1(v0, v2) % 29.43/4.63 | = 0)) % 29.43/4.63 | % 29.43/4.63 | ALPHA: (wP_parameter_search_rec) implies: % 29.43/4.63 | (10) ty(int) % 29.43/4.63 | (11) ? [v0: int] : ? [v1: map_int_int] : ? [v2: int] : ? [v3: uni] : ? % 29.43/4.63 | [v4: uni] : ? [v5: array_int] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 29.43/4.63 | int] : ? [v9: int] : ? [v10: uni] : ? [v11: uni] : ? [v12: int] % 29.43/4.63 | : ? [v13: int] : ? [v14: uni] : ? [v15: uni] : ? [v16: int] : ? % 29.43/4.63 | [v17: int] : ? [v18: uni] : ? [v19: uni] : ? [v20: int] : % 29.43/4.63 | ($lesseq(0, $sum(v8, v2)) & $lesseq(1, v8) & $lesseq(1, % 29.43/4.63 | $difference(v0, v2)) & $lesseq(0, v2) & t2tb2(v1) = v3 & % 29.43/4.63 | decrease11(v5) = 0 & tb2t1(v4) = v5 & tb2t(v7) = v8 & t2tb(v2) = v6 % 29.43/4.63 | & mk_array1(int, v0, v3) = v4 & get(int, int, v3, v6) = v7 & % 29.43/4.63 | map_int_int(v1) & array_int(v5) & uni(v7) & uni(v6) & uni(v4) & % 29.43/4.63 | uni(v3) & ( ~ (v9 = -1) | (v20 = 0 & $lesseq(1, $difference(v0, % 29.43/4.63 | v17)) & $lesseq(v2, v17) & tb2t(v19) = 0 & t2tb(v17) = v18 & % 29.43/4.63 | get(int, int, v3, v18) = v19 & uni(v19) & uni(v18))) & ( ~ % 29.43/4.63 | ($lesseq(1, $difference(v0, v9))) | ~ ($lesseq(v2, v9)) | (v16 = % 29.43/4.63 | 0 & $lesseq(1, $difference(v9, v13)) & $lesseq(v2, v13) & % 29.43/4.63 | tb2t(v15) = 0 & t2tb(v13) = v14 & get(int, int, v3, v14) = v15 & % 29.43/4.63 | uni(v15) & uni(v14)) | ( ~ (v12 = 0) & tb2t(v11) = v12 & % 29.43/4.63 | t2tb(v9) = v10 & get(int, int, v3, v10) = v11 & uni(v11) & % 29.43/4.63 | uni(v10))) & ((v12 = 0 & $lesseq(1, $difference(v0, v9)) & % 29.43/4.63 | $lesseq(v2, $difference(v9, v8)) & tb2t(v11) = 0 & t2tb(v9) = % 29.43/4.63 | v10 & get(int, int, v3, v10) = v11 & uni(v11) & uni(v10) & ! % 29.43/4.63 | [v21: int] : ! [v22: uni] : ( ~ ($lesseq(1, $difference(v9, % 29.43/4.63 | v21))) | ~ ($lesseq(v2, $difference(v21, v8))) | ~ % 29.43/4.63 | (t2tb(v21) = v22) | ? [v23: uni] : ? [v24: int] : ( ~ (v24 = % 29.43/4.63 | 0) & tb2t(v23) = v24 & get(int, int, v3, v22) = v23 & % 29.43/4.63 | uni(v23)))) | (v9 = -1 & ! [v21: int] : ! [v22: uni] : ( ~ % 29.43/4.63 | ($lesseq(1, $difference(v0, v21))) | ~ ($lesseq(v2, % 29.43/4.63 | $difference(v21, v8))) | ~ (t2tb(v21) = v22) | ? [v23: % 29.43/4.63 | uni] : ? [v24: int] : ( ~ (v24 = 0) & tb2t(v23) = v24 & % 29.43/4.63 | get(int, int, v3, v22) = v23 & uni(v23)))))) % 29.43/4.63 | % 29.43/4.63 | ALPHA: (function-axioms) implies: % 29.43/4.63 | (12) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (ref(v2) = v1) % 29.43/4.63 | | ~ (ref(v2) = v0)) % 29.43/4.63 | (13) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb(v2) = % 29.43/4.63 | v1) | ~ (t2tb(v2) = v0)) % 29.43/4.63 | (14) ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = % 29.43/4.63 | v1) | ~ (tb2t(v2) = v0)) % 29.43/4.63 | (15) ! [v0: uni] : ! [v1: uni] : ! [v2: array_int] : (v1 = v0 | ~ % 29.43/4.63 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 29.43/4.63 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 29.43/4.63 | array_int] : (v1 = v0 | ~ (decrease11(v2) = v1) | ~ % 29.43/4.63 | (decrease11(v2) = v0)) % 29.43/4.63 | (17) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 29.43/4.63 | : ! [v3: ty] : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) % 29.43/4.63 | = v0)) % 29.43/4.63 | (18) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ % 29.43/4.63 | (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) % 29.43/4.63 | (19) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 29.43/4.63 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) % 29.43/4.63 | (20) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 29.43/4.63 | ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 29.43/4.63 | (get(v5, v4, v3, v2) = v0)) % 29.43/4.63 | % 29.43/4.64 | DELTA: instantiating (9) with fresh symbol all_52_0 gives: % 29.43/4.64 | (21) map(int, int) = all_52_0 & ty(all_52_0) & ! [v0: map_int_int] : ! % 29.43/4.64 | [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ map_int_int(v0) | % 29.43/4.64 | sort1(all_52_0, v1) = 0) % 29.43/4.64 | % 29.43/4.64 | ALPHA: (21) implies: % 29.43/4.64 | (22) ty(all_52_0) % 29.43/4.64 | (23) map(int, int) = all_52_0 % 29.43/4.64 | (24) ! [v0: map_int_int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ % 29.43/4.64 | map_int_int(v0) | sort1(all_52_0, v1) = 0) % 29.43/4.64 | % 29.43/4.64 | DELTA: instantiating (11) with fresh symbols all_59_0, all_59_1, all_59_2, % 29.43/4.64 | all_59_3, all_59_4, all_59_5, all_59_6, all_59_7, all_59_8, all_59_9, % 29.43/4.64 | all_59_10, all_59_11, all_59_12, all_59_13, all_59_14, all_59_15, % 29.43/4.64 | all_59_16, all_59_17, all_59_18, all_59_19, all_59_20 gives: % 29.43/4.64 | (25) $lesseq(0, $sum(all_59_12, all_59_18)) & $lesseq(1, all_59_12) & % 29.43/4.64 | $lesseq(1, $difference(all_59_20, all_59_18)) & $lesseq(0, all_59_18) % 29.43/4.64 | & t2tb2(all_59_19) = all_59_17 & decrease11(all_59_15) = 0 & % 29.43/4.64 | tb2t1(all_59_16) = all_59_15 & tb2t(all_59_13) = all_59_12 & % 29.43/4.64 | t2tb(all_59_18) = all_59_14 & mk_array1(int, all_59_20, all_59_17) = % 29.43/4.64 | all_59_16 & get(int, int, all_59_17, all_59_14) = all_59_13 & % 29.43/4.64 | map_int_int(all_59_19) & array_int(all_59_15) & uni(all_59_13) & % 29.43/4.64 | uni(all_59_14) & uni(all_59_16) & uni(all_59_17) & ( ~ (all_59_11 = % 29.43/4.64 | -1) | (all_59_0 = 0 & $lesseq(1, $difference(all_59_20, all_59_3)) % 29.43/4.64 | & $lesseq(all_59_18, all_59_3) & tb2t(all_59_1) = 0 & % 29.43/4.64 | t2tb(all_59_3) = all_59_2 & get(int, int, all_59_17, all_59_2) = % 29.43/4.64 | all_59_1 & uni(all_59_1) & uni(all_59_2))) & ( ~ ($lesseq(1, % 29.43/4.64 | $difference(all_59_20, all_59_11))) | ~ ($lesseq(all_59_18, % 29.43/4.64 | all_59_11)) | (all_59_4 = 0 & $lesseq(1, $difference(all_59_11, % 29.43/4.64 | all_59_7)) & $lesseq(all_59_18, all_59_7) & tb2t(all_59_5) = 0 % 29.43/4.64 | & t2tb(all_59_7) = all_59_6 & get(int, int, all_59_17, all_59_6) = % 29.43/4.64 | all_59_5 & uni(all_59_5) & uni(all_59_6)) | ( ~ (all_59_8 = 0) & % 29.43/4.64 | tb2t(all_59_9) = all_59_8 & t2tb(all_59_11) = all_59_10 & get(int, % 29.43/4.64 | int, all_59_17, all_59_10) = all_59_9 & uni(all_59_9) & % 29.43/4.64 | uni(all_59_10))) & ((all_59_8 = 0 & $lesseq(1, % 29.43/4.64 | $difference(all_59_20, all_59_11)) & $lesseq(all_59_18, % 29.43/4.64 | $difference(all_59_11, all_59_12)) & tb2t(all_59_9) = 0 & % 29.43/4.64 | t2tb(all_59_11) = all_59_10 & get(int, int, all_59_17, all_59_10) % 29.43/4.64 | = all_59_9 & uni(all_59_9) & uni(all_59_10) & ! [v0: int] : ! % 29.43/4.64 | [v1: uni] : ( ~ ($lesseq(1, $difference(all_59_11, v0))) | ~ % 29.43/4.64 | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ (t2tb(v0) % 29.43/4.64 | = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & tb2t(v2) % 29.43/4.64 | = v3 & get(int, int, all_59_17, v1) = v2 & uni(v2)))) | % 29.43/4.64 | (all_59_11 = -1 & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.43/4.64 | $difference(all_59_20, v0))) | ~ ($lesseq(all_59_18, % 29.43/4.64 | $difference(v0, all_59_12))) | ~ (t2tb(v0) = v1) | ? [v2: % 29.43/4.64 | uni] : ? [v3: int] : ( ~ (v3 = 0) & tb2t(v2) = v3 & get(int, % 29.43/4.64 | int, all_59_17, v1) = v2 & uni(v2))))) % 29.43/4.64 | % 29.43/4.64 | ALPHA: (25) implies: % 29.43/4.64 | (26) $lesseq(0, all_59_18) % 29.43/4.64 | (27) $lesseq(1, all_59_12) % 29.43/4.64 | (28) $lesseq(0, $sum(all_59_12, all_59_18)) % 29.43/4.64 | (29) uni(all_59_17) % 29.43/4.64 | (30) uni(all_59_16) % 29.43/4.64 | (31) uni(all_59_14) % 29.43/4.64 | (32) uni(all_59_13) % 29.43/4.64 | (33) array_int(all_59_15) % 29.43/4.64 | (34) map_int_int(all_59_19) % 29.43/4.64 | (35) get(int, int, all_59_17, all_59_14) = all_59_13 % 29.43/4.64 | (36) mk_array1(int, all_59_20, all_59_17) = all_59_16 % 29.43/4.64 | (37) t2tb(all_59_18) = all_59_14 % 29.43/4.64 | (38) tb2t(all_59_13) = all_59_12 % 29.43/4.64 | (39) tb2t1(all_59_16) = all_59_15 % 29.43/4.64 | (40) decrease11(all_59_15) = 0 % 29.43/4.64 | (41) t2tb2(all_59_19) = all_59_17 % 29.43/4.65 | (42) (all_59_8 = 0 & $lesseq(1, $difference(all_59_20, all_59_11)) & % 29.43/4.65 | $lesseq(all_59_18, $difference(all_59_11, all_59_12)) & % 29.43/4.65 | tb2t(all_59_9) = 0 & t2tb(all_59_11) = all_59_10 & get(int, int, % 29.43/4.65 | all_59_17, all_59_10) = all_59_9 & uni(all_59_9) & uni(all_59_10) % 29.43/4.65 | & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.43/4.65 | $difference(all_59_11, v0))) | ~ ($lesseq(all_59_18, % 29.43/4.65 | $difference(v0, all_59_12))) | ~ (t2tb(v0) = v1) | ? [v2: % 29.43/4.65 | uni] : ? [v3: int] : ( ~ (v3 = 0) & tb2t(v2) = v3 & get(int, % 29.43/4.65 | int, all_59_17, v1) = v2 & uni(v2)))) | (all_59_11 = -1 & ! % 29.43/4.65 | [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_59_20, % 29.43/4.65 | v0))) | ~ ($lesseq(all_59_18, $difference(v0, all_59_12))) % 29.43/4.65 | | ~ (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) % 29.43/4.65 | & tb2t(v2) = v3 & get(int, int, all_59_17, v1) = v2 & uni(v2)))) % 29.43/4.65 | (43) ~ ($lesseq(1, $difference(all_59_20, all_59_11))) | ~ % 29.43/4.65 | ($lesseq(all_59_18, all_59_11)) | (all_59_4 = 0 & $lesseq(1, % 29.43/4.65 | $difference(all_59_11, all_59_7)) & $lesseq(all_59_18, all_59_7) & % 29.43/4.65 | tb2t(all_59_5) = 0 & t2tb(all_59_7) = all_59_6 & get(int, int, % 29.43/4.65 | all_59_17, all_59_6) = all_59_5 & uni(all_59_5) & uni(all_59_6)) | % 29.43/4.65 | ( ~ (all_59_8 = 0) & tb2t(all_59_9) = all_59_8 & t2tb(all_59_11) = % 29.43/4.65 | all_59_10 & get(int, int, all_59_17, all_59_10) = all_59_9 & % 29.43/4.65 | uni(all_59_9) & uni(all_59_10)) % 29.43/4.65 | (44) ~ (all_59_11 = -1) | (all_59_0 = 0 & $lesseq(1, % 29.43/4.65 | $difference(all_59_20, all_59_3)) & $lesseq(all_59_18, all_59_3) & % 29.43/4.65 | tb2t(all_59_1) = 0 & t2tb(all_59_3) = all_59_2 & get(int, int, % 29.43/4.65 | all_59_17, all_59_2) = all_59_1 & uni(all_59_1) & uni(all_59_2)) % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (get_sort2) with int, int, all_59_17, all_59_14, % 29.43/4.65 | all_59_13, simplifying with (10), (29), (31), (35) gives: % 29.43/4.65 | (45) sort1(int, all_59_13) = 0 % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (length_def1) with int, all_59_20, all_59_17, % 29.43/4.65 | all_59_16, simplifying with (10), (29), (36) gives: % 29.43/4.65 | (46) length1(int, all_59_16) = all_59_20 % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (3) with int, all_59_20, all_59_17, all_59_16, % 29.43/4.65 | simplifying with (10), (29), (36) gives: % 29.43/4.65 | (47) ? [v0: ty] : ? [v1: int] : ? [v2: int] : ((v2 = all_59_17 & % 29.43/4.65 | elts(int, all_59_16) = all_59_17) | ( ~ (v1 = 0) & map(int, int) = % 29.43/4.65 | v0 & sort1(v0, all_59_17) = v1 & ty(v0))) % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (bridgeR1) with all_59_16, all_59_15, simplifying % 29.43/4.65 | with (30), (39) gives: % 29.43/4.65 | (48) t2tb1(all_59_15) = all_59_16 % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (7) with all_59_15, simplifying with (33), (40) % 29.43/4.65 | gives: % 29.43/4.65 | (49) ? [v0: uni] : ? [v1: int] : (t2tb1(all_59_15) = v0 & length1(int, % 29.43/4.65 | v0) = v1 & uni(v0) & ! [v2: int] : ! [v3: int] : ! [v4: uni] : % 29.43/4.65 | ! [v5: int] : ! [v6: uni] : ! [v7: int] : ( ~ ($lesseq(1, % 29.43/4.65 | $sum($difference($difference(v7, v5), v3), v2))) | ~ % 29.43/4.65 | ($lesseq(1, $difference(v1, v3))) | ~ ($lesseq(v2, v3)) | ~ % 29.43/4.65 | ($lesseq(0, v2)) | ~ (tb2t(v6) = v7) | ~ (tb2t(v4) = v5) | ~ % 29.43/4.65 | (get2(int, v0, v3) = v4) | ~ (get2(int, v0, v2) = v6))) % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (5) with all_59_15, simplifying with (33), (40) % 29.43/4.65 | gives: % 29.43/4.65 | (50) ? [v0: uni] : ? [v1: int] : (t2tb1(all_59_15) = v0 & length1(int, % 29.43/4.65 | v0) = v1 & uni(v0) & ! [v2: int] : ! [v3: uni] : ( ~ ($lesseq(2, % 29.43/4.65 | $difference(v1, v2))) | ~ ($lesseq(0, v2)) | ~ (get2(int, % 29.43/4.65 | v0, $sum(v2, 1)) = v3) | ? [v4: int] : ? [v5: uni] : ? [v6: % 29.43/4.65 | int] : ($lesseq(-1, $difference(v4, v6)) & tb2t(v5) = v6 & % 29.43/4.65 | tb2t(v3) = v4 & get2(int, v0, v2) = v5 & uni(v5))) & ! [v2: % 29.43/4.65 | int] : ! [v3: uni] : ( ~ ($lesseq(2, $difference(v1, v2))) | ~ % 29.43/4.65 | ($lesseq(0, v2)) | ~ (get2(int, v0, v2) = v3) | ? [v4: uni] : ? % 29.43/4.65 | [v5: int] : ? [v6: int] : ($lesseq(-1, $difference(v5, v6)) & % 29.43/4.65 | tb2t(v4) = v5 & tb2t(v3) = v6 & get2(int, v0, $sum(v2, 1)) = v4 % 29.43/4.65 | & uni(v4)))) % 29.43/4.65 | % 29.43/4.65 | GROUND_INST: instantiating (24) with all_59_19, all_59_17, simplifying with % 29.43/4.65 | (34), (41) gives: % 29.43/4.65 | (51) sort1(all_52_0, all_59_17) = 0 % 29.43/4.65 | % 29.43/4.65 | DELTA: instantiating (47) with fresh symbols all_72_0, all_72_1, all_72_2 % 29.43/4.65 | gives: % 29.43/4.65 | (52) (all_72_0 = all_59_17 & elts(int, all_59_16) = all_59_17) | ( ~ % 29.43/4.65 | (all_72_1 = 0) & map(int, int) = all_72_2 & sort1(all_72_2, % 29.43/4.65 | all_59_17) = all_72_1 & ty(all_72_2)) % 29.43/4.65 | % 29.43/4.65 | DELTA: instantiating (49) with fresh symbols all_73_0, all_73_1 gives: % 29.43/4.65 | (53) t2tb1(all_59_15) = all_73_1 & length1(int, all_73_1) = all_73_0 & % 29.43/4.65 | uni(all_73_1) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 29.43/4.65 | int] : ! [v4: uni] : ! [v5: int] : ( ~ ($lesseq(1, % 29.43/4.65 | $sum($difference($difference(v5, v3), v1), v0))) | ~ % 29.43/4.65 | ($lesseq(1, $difference(all_73_0, v1))) | ~ ($lesseq(v0, v1)) | ~ % 29.43/4.65 | ($lesseq(0, v0)) | ~ (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) | ~ % 29.43/4.65 | (get2(int, all_73_1, v1) = v2) | ~ (get2(int, all_73_1, v0) = v4)) % 29.43/4.65 | % 29.43/4.65 | ALPHA: (53) implies: % 29.43/4.65 | (54) uni(all_73_1) % 29.43/4.65 | (55) length1(int, all_73_1) = all_73_0 % 29.43/4.65 | (56) t2tb1(all_59_15) = all_73_1 % 29.43/4.65 | % 29.43/4.65 | DELTA: instantiating (50) with fresh symbols all_76_0, all_76_1 gives: % 29.43/4.65 | (57) t2tb1(all_59_15) = all_76_1 & length1(int, all_76_1) = all_76_0 & % 29.43/4.65 | uni(all_76_1) & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(2, % 29.43/4.65 | $difference(all_76_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 29.43/4.65 | (get2(int, all_76_1, $sum(v0, 1)) = v1) | ? [v2: int] : ? [v3: % 29.43/4.66 | uni] : ? [v4: int] : ($lesseq(-1, $difference(v2, v4)) & tb2t(v3) % 29.43/4.66 | = v4 & tb2t(v1) = v2 & get2(int, all_76_1, v0) = v3 & uni(v3))) & % 29.43/4.66 | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(2, $difference(all_76_0, % 29.43/4.66 | v0))) | ~ ($lesseq(0, v0)) | ~ (get2(int, all_76_1, v0) = % 29.43/4.66 | v1) | ? [v2: uni] : ? [v3: int] : ? [v4: int] : ($lesseq(-1, % 29.43/4.66 | $difference(v3, v4)) & tb2t(v2) = v3 & tb2t(v1) = v4 & get2(int, % 29.43/4.66 | all_76_1, $sum(v0, 1)) = v2 & uni(v2))) % 29.43/4.66 | % 29.43/4.66 | ALPHA: (57) implies: % 29.43/4.66 | (58) length1(int, all_76_1) = all_76_0 % 29.43/4.66 | (59) t2tb1(all_59_15) = all_76_1 % 29.43/4.66 | % 29.43/4.66 | BETA: splitting (52) gives: % 29.43/4.66 | % 29.43/4.66 | Case 1: % 29.43/4.66 | | % 29.43/4.66 | | (60) all_72_0 = all_59_17 & elts(int, all_59_16) = all_59_17 % 29.43/4.66 | | % 29.43/4.66 | | ALPHA: (60) implies: % 29.43/4.66 | | (61) elts(int, all_59_16) = all_59_17 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (15) with all_73_1, all_76_1, all_59_15, % 29.43/4.66 | | simplifying with (56), (59) gives: % 29.43/4.66 | | (62) all_76_1 = all_73_1 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (15) with all_59_16, all_76_1, all_59_15, % 29.43/4.66 | | simplifying with (48), (59) gives: % 29.43/4.66 | | (63) all_76_1 = all_59_16 % 29.43/4.66 | | % 29.43/4.66 | | COMBINE_EQS: (62), (63) imply: % 29.43/4.66 | | (64) all_73_1 = all_59_16 % 29.43/4.66 | | % 29.43/4.66 | | SIMP: (64) implies: % 29.43/4.66 | | (65) all_73_1 = all_59_16 % 29.43/4.66 | | % 29.43/4.66 | | REDUCE: (58), (63) imply: % 29.43/4.66 | | (66) length1(int, all_59_16) = all_76_0 % 29.43/4.66 | | % 29.43/4.66 | | REDUCE: (55), (65) imply: % 29.43/4.66 | | (67) length1(int, all_59_16) = all_73_0 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (19) with all_59_20, all_76_0, all_59_16, int, % 29.43/4.66 | | simplifying with (46), (66) gives: % 29.43/4.66 | | (68) all_76_0 = all_59_20 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (19) with all_73_0, all_76_0, all_59_16, int, % 29.43/4.66 | | simplifying with (66), (67) gives: % 29.43/4.66 | | (69) all_76_0 = all_73_0 % 29.43/4.66 | | % 29.43/4.66 | | COMBINE_EQS: (68), (69) imply: % 29.43/4.66 | | (70) all_73_0 = all_59_20 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (1) with int, all_59_13, simplifying with (10), % 29.43/4.66 | | (32), (45) gives: % 29.43/4.66 | | (71) ? [v0: uni] : (contents(int, v0) = all_59_13 & mk_ref(int, % 29.43/4.66 | | all_59_13) = v0 & uni(v0)) % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (1) with all_52_0, all_59_17, simplifying with % 29.43/4.66 | | (22), (29), (51) gives: % 29.43/4.66 | | (72) ? [v0: uni] : (contents(all_52_0, v0) = all_59_17 & % 29.43/4.66 | | mk_ref(all_52_0, all_59_17) = v0 & uni(v0)) % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (4) with int, all_59_16, all_59_18, all_59_17, % 29.43/4.66 | | all_59_14, all_59_13, simplifying with (10), (30), (35), (37), % 29.43/4.66 | | (61) gives: % 29.43/4.66 | | (73) get2(int, all_59_16, all_59_18) = all_59_13 & uni(all_59_13) % 29.43/4.66 | | % 29.43/4.66 | | ALPHA: (73) implies: % 29.43/4.66 | | (74) get2(int, all_59_16, all_59_18) = all_59_13 % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (8) with all_59_15, all_59_16, simplifying with % 29.43/4.66 | | (33), (48) gives: % 29.43/4.66 | | (75) ? [v0: int] : ? [v1: int] : (( ~ (v0 = 0) & decrease11(all_59_15) % 29.43/4.66 | | = v0) | (length1(int, all_59_16) = v1 & ! [v2: int] : ! [v3: % 29.43/4.66 | | int] : ! [v4: uni] : ! [v5: int] : ! [v6: uni] : ! [v7: % 29.43/4.66 | | int] : ( ~ ($lesseq(1, $sum($difference($difference(v7, v5), % 29.43/4.66 | | v3), v2))) | ~ ($lesseq(1, $difference(v1, v3))) | ~ % 29.43/4.66 | | ($lesseq(v2, v3)) | ~ ($lesseq(0, v2)) | ~ (tb2t(v6) = v7) | % 29.43/4.66 | | ~ (tb2t(v4) = v5) | ~ (get2(int, all_59_16, v3) = v4) | ~ % 29.43/4.66 | | (get2(int, all_59_16, v2) = v6)))) % 29.43/4.66 | | % 29.43/4.66 | | GROUND_INST: instantiating (6) with all_59_15, all_59_16, simplifying with % 29.43/4.66 | | (33), (48) gives: % 29.43/4.66 | | (76) ? [v0: int] : ? [v1: int] : (( ~ (v0 = 0) & decrease11(all_59_15) % 29.43/4.66 | | = v0) | (length1(int, all_59_16) = v1 & ! [v2: int] : ! [v3: % 29.43/4.66 | | uni] : ( ~ ($lesseq(2, $difference(v1, v2))) | ~ ($lesseq(0, % 29.43/4.66 | | v2)) | ~ (get2(int, all_59_16, $sum(v2, 1)) = v3) | ? % 29.43/4.66 | | [v4: int] : ? [v5: uni] : ? [v6: int] : ($lesseq(-1, % 29.43/4.66 | | $difference(v4, v6)) & tb2t(v5) = v6 & tb2t(v3) = v4 & % 29.43/4.66 | | get2(int, all_59_16, v2) = v5 & uni(v5))) & ! [v2: int] : % 29.43/4.66 | | ! [v3: uni] : ( ~ ($lesseq(2, $difference(v1, v2))) | ~ % 29.43/4.66 | | ($lesseq(0, v2)) | ~ (get2(int, all_59_16, v2) = v3) | ? % 29.43/4.66 | | [v4: uni] : ? [v5: int] : ? [v6: int] : ($lesseq(-1, % 29.43/4.66 | | $difference(v5, v6)) & tb2t(v4) = v5 & tb2t(v3) = v6 & % 29.43/4.66 | | get2(int, all_59_16, $sum(v2, 1)) = v4 & uni(v4))))) % 29.43/4.66 | | % 29.43/4.66 | | DELTA: instantiating (72) with fresh symbol all_104_0 gives: % 29.43/4.66 | | (77) contents(all_52_0, all_104_0) = all_59_17 & mk_ref(all_52_0, % 29.43/4.66 | | all_59_17) = all_104_0 & uni(all_104_0) % 29.43/4.66 | | % 29.43/4.66 | | ALPHA: (77) implies: % 29.61/4.66 | | (78) uni(all_104_0) % 29.61/4.66 | | (79) mk_ref(all_52_0, all_59_17) = all_104_0 % 29.61/4.66 | | % 29.61/4.66 | | DELTA: instantiating (71) with fresh symbol all_106_0 gives: % 29.61/4.66 | | (80) contents(int, all_106_0) = all_59_13 & mk_ref(int, all_59_13) = % 29.61/4.66 | | all_106_0 & uni(all_106_0) % 29.61/4.66 | | % 29.61/4.66 | | ALPHA: (80) implies: % 29.61/4.66 | | (81) uni(all_106_0) % 29.61/4.66 | | (82) mk_ref(int, all_59_13) = all_106_0 % 29.61/4.66 | | (83) contents(int, all_106_0) = all_59_13 % 29.61/4.66 | | % 29.61/4.66 | | DELTA: instantiating (75) with fresh symbols all_110_0, all_110_1 gives: % 29.61/4.66 | | (84) ( ~ (all_110_1 = 0) & decrease11(all_59_15) = all_110_1) | % 29.61/4.66 | | (length1(int, all_59_16) = all_110_0 & ! [v0: int] : ! [v1: int] : % 29.61/4.66 | | ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] : ( ~ % 29.61/4.66 | | ($lesseq(1, $sum($difference($difference(v5, v3), v1), v0))) | % 29.61/4.66 | | ~ ($lesseq(1, $difference(all_110_0, v1))) | ~ ($lesseq(v0, % 29.61/4.66 | | v1)) | ~ ($lesseq(0, v0)) | ~ (tb2t(v4) = v5) | ~ % 29.61/4.66 | | (tb2t(v2) = v3) | ~ (get2(int, all_59_16, v1) = v2) | ~ % 29.61/4.66 | | (get2(int, all_59_16, v0) = v4))) % 29.61/4.66 | | % 29.61/4.66 | | DELTA: instantiating (76) with fresh symbols all_112_0, all_112_1 gives: % 29.61/4.66 | | (85) ( ~ (all_112_1 = 0) & decrease11(all_59_15) = all_112_1) | % 29.61/4.66 | | (length1(int, all_59_16) = all_112_0 & ! [v0: int] : ! [v1: uni] : % 29.61/4.66 | | ( ~ ($lesseq(2, $difference(all_112_0, v0))) | ~ ($lesseq(0, v0)) % 29.61/4.66 | | | ~ (get2(int, all_59_16, $sum(v0, 1)) = v1) | ? [v2: int] : % 29.61/4.66 | | ? [v3: uni] : ? [v4: int] : ($lesseq(-1, $difference(v2, v4)) & % 29.61/4.66 | | tb2t(v3) = v4 & tb2t(v1) = v2 & get2(int, all_59_16, v0) = v3 % 29.61/4.67 | | & uni(v3))) & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(2, % 29.61/4.67 | | $difference(all_112_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 29.61/4.67 | | (get2(int, all_59_16, v0) = v1) | ? [v2: uni] : ? [v3: int] : % 29.61/4.67 | | ? [v4: int] : ($lesseq(-1, $difference(v3, v4)) & tb2t(v2) = v3 % 29.61/4.67 | | & tb2t(v1) = v4 & get2(int, all_59_16, $sum(v0, 1)) = v2 & % 29.61/4.67 | | uni(v2)))) % 29.61/4.67 | | % 29.61/4.67 | | BETA: splitting (84) gives: % 29.61/4.67 | | % 29.61/4.67 | | Case 1: % 29.61/4.67 | | | % 29.61/4.67 | | | (86) ~ (all_110_1 = 0) & decrease11(all_59_15) = all_110_1 % 29.61/4.67 | | | % 29.61/4.67 | | | ALPHA: (86) implies: % 29.61/4.67 | | | (87) ~ (all_110_1 = 0) % 29.61/4.67 | | | (88) decrease11(all_59_15) = all_110_1 % 29.61/4.67 | | | % 29.61/4.67 | | | GROUND_INST: instantiating (16) with 0, all_110_1, all_59_15, simplifying % 29.61/4.67 | | | with (40), (88) gives: % 29.61/4.67 | | | (89) all_110_1 = 0 % 29.61/4.67 | | | % 29.61/4.67 | | | REDUCE: (87), (89) imply: % 29.61/4.67 | | | (90) $false % 29.61/4.67 | | | % 29.61/4.67 | | | CLOSE: (90) is inconsistent. % 29.61/4.67 | | | % 29.61/4.67 | | Case 2: % 29.61/4.67 | | | % 29.61/4.67 | | | (91) length1(int, all_59_16) = all_110_0 & ! [v0: int] : ! [v1: int] % 29.61/4.67 | | | : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] : ( ~ % 29.61/4.67 | | | ($lesseq(1, $sum($difference($difference(v5, v3), v1), v0))) | % 29.61/4.67 | | | ~ ($lesseq(1, $difference(all_110_0, v1))) | ~ ($lesseq(v0, % 29.61/4.67 | | | v1)) | ~ ($lesseq(0, v0)) | ~ (tb2t(v4) = v5) | ~ % 29.61/4.67 | | | (tb2t(v2) = v3) | ~ (get2(int, all_59_16, v1) = v2) | ~ % 29.61/4.67 | | | (get2(int, all_59_16, v0) = v4)) % 29.61/4.67 | | | % 29.61/4.67 | | | ALPHA: (91) implies: % 29.61/4.67 | | | (92) length1(int, all_59_16) = all_110_0 % 29.61/4.67 | | | (93) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: int] : ! % 29.61/4.67 | | | [v4: uni] : ! [v5: int] : ( ~ ($lesseq(1, % 29.61/4.67 | | | $sum($difference($difference(v5, v3), v1), v0))) | ~ % 29.61/4.67 | | | ($lesseq(1, $difference(all_110_0, v1))) | ~ ($lesseq(v0, v1)) % 29.61/4.67 | | | | ~ ($lesseq(0, v0)) | ~ (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) % 29.61/4.67 | | | | ~ (get2(int, all_59_16, v1) = v2) | ~ (get2(int, all_59_16, % 29.61/4.67 | | | v0) = v4)) % 29.61/4.67 | | | % 29.61/4.67 | | | BETA: splitting (85) gives: % 29.61/4.67 | | | % 29.61/4.67 | | | Case 1: % 29.61/4.67 | | | | % 29.61/4.67 | | | | (94) ~ (all_112_1 = 0) & decrease11(all_59_15) = all_112_1 % 29.61/4.67 | | | | % 29.61/4.67 | | | | ALPHA: (94) implies: % 29.61/4.67 | | | | (95) ~ (all_112_1 = 0) % 29.61/4.67 | | | | (96) decrease11(all_59_15) = all_112_1 % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (16) with 0, all_112_1, all_59_15, % 29.61/4.67 | | | | simplifying with (40), (96) gives: % 29.61/4.67 | | | | (97) all_112_1 = 0 % 29.61/4.67 | | | | % 29.61/4.67 | | | | REDUCE: (95), (97) imply: % 29.61/4.67 | | | | (98) $false % 29.61/4.67 | | | | % 29.61/4.67 | | | | CLOSE: (98) is inconsistent. % 29.61/4.67 | | | | % 29.61/4.67 | | | Case 2: % 29.61/4.67 | | | | % 29.61/4.67 | | | | (99) length1(int, all_59_16) = all_112_0 & ! [v0: int] : ! [v1: % 29.61/4.67 | | | | uni] : ( ~ ($lesseq(2, $difference(all_112_0, v0))) | ~ % 29.61/4.67 | | | | ($lesseq(0, v0)) | ~ (get2(int, all_59_16, $sum(v0, 1)) = v1) % 29.61/4.67 | | | | | ? [v2: int] : ? [v3: uni] : ? [v4: int] : ($lesseq(-1, % 29.61/4.67 | | | | $difference(v2, v4)) & tb2t(v3) = v4 & tb2t(v1) = v2 & % 29.61/4.67 | | | | get2(int, all_59_16, v0) = v3 & uni(v3))) & ! [v0: int] : % 29.61/4.67 | | | | ! [v1: uni] : ( ~ ($lesseq(2, $difference(all_112_0, v0))) | ~ % 29.61/4.67 | | | | ($lesseq(0, v0)) | ~ (get2(int, all_59_16, v0) = v1) | ? % 29.61/4.67 | | | | [v2: uni] : ? [v3: int] : ? [v4: int] : ($lesseq(-1, % 29.61/4.67 | | | | $difference(v3, v4)) & tb2t(v2) = v3 & tb2t(v1) = v4 & % 29.61/4.67 | | | | get2(int, all_59_16, $sum(v0, 1)) = v2 & uni(v2))) % 29.61/4.67 | | | | % 29.61/4.67 | | | | ALPHA: (99) implies: % 29.61/4.67 | | | | (100) length1(int, all_59_16) = all_112_0 % 29.61/4.67 | | | | (101) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(2, % 29.61/4.67 | | | | $difference(all_112_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 29.61/4.67 | | | | (get2(int, all_59_16, v0) = v1) | ? [v2: uni] : ? [v3: int] % 29.61/4.67 | | | | : ? [v4: int] : ($lesseq(-1, $difference(v3, v4)) & tb2t(v2) % 29.61/4.67 | | | | = v3 & tb2t(v1) = v4 & get2(int, all_59_16, $sum(v0, 1)) = % 29.61/4.67 | | | | v2 & uni(v2))) % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (19) with all_59_20, all_112_0, all_59_16, % 29.61/4.67 | | | | int, simplifying with (46), (100) gives: % 29.61/4.67 | | | | (102) all_112_0 = all_59_20 % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (19) with all_110_0, all_112_0, all_59_16, % 29.61/4.67 | | | | int, simplifying with (92), (100) gives: % 29.61/4.67 | | | | (103) all_112_0 = all_110_0 % 29.61/4.67 | | | | % 29.61/4.67 | | | | COMBINE_EQS: (102), (103) imply: % 29.61/4.67 | | | | (104) all_110_0 = all_59_20 % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (mk_ref_sort1) with int, all_59_13, % 29.61/4.67 | | | | all_106_0, simplifying with (10), (32), (82) gives: % 29.61/4.67 | | | | (105) ? [v0: ty] : (ref(int) = v0 & sort1(v0, all_106_0) = 0 & % 29.61/4.67 | | | | ty(v0)) % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (mk_ref_sort1) with all_52_0, all_59_17, % 29.61/4.67 | | | | all_104_0, simplifying with (22), (29), (79) gives: % 29.61/4.67 | | | | (106) ? [v0: ty] : (ref(all_52_0) = v0 & sort1(v0, all_104_0) = 0 & % 29.61/4.67 | | | | ty(v0)) % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (2) with int, all_106_0, all_59_13, % 29.61/4.67 | | | | simplifying with (10), (81), (83) gives: % 29.61/4.67 | | | | (107) ? [v0: ty] : ? [v1: int] : ? [v2: int] : ((v2 = all_106_0 & % 29.61/4.67 | | | | mk_ref(int, all_59_13) = all_106_0) | ( ~ (v1 = 0) & % 29.61/4.67 | | | | ref(int) = v0 & sort1(v0, all_106_0) = v1 & ty(v0))) % 29.61/4.67 | | | | % 29.61/4.67 | | | | GROUND_INST: instantiating (101) with all_59_18, all_59_13, simplifying % 29.61/4.67 | | | | with (74) gives: % 29.61/4.67 | | | | (108) ~ ($lesseq(2, $difference(all_112_0, all_59_18))) | ~ % 29.61/4.67 | | | | ($lesseq(0, all_59_18)) | ? [v0: uni] : ? [v1: int] : ? [v2: % 29.61/4.67 | | | | int] : ($lesseq(-1, $difference(v1, v2)) & tb2t(v0) = v1 & % 29.61/4.67 | | | | tb2t(all_59_13) = v2 & get2(int, all_59_16, $sum(all_59_18, % 29.61/4.67 | | | | 1)) = v0 & uni(v0)) % 29.61/4.67 | | | | % 29.61/4.67 | | | | DELTA: instantiating (106) with fresh symbol all_138_0 gives: % 29.61/4.67 | | | | (109) ref(all_52_0) = all_138_0 & sort1(all_138_0, all_104_0) = 0 & % 29.61/4.67 | | | | ty(all_138_0) % 29.61/4.67 | | | | % 29.61/4.67 | | | | ALPHA: (109) implies: % 29.61/4.67 | | | | (110) ty(all_138_0) % 29.61/4.67 | | | | (111) sort1(all_138_0, all_104_0) = 0 % 29.61/4.67 | | | | % 29.61/4.67 | | | | DELTA: instantiating (105) with fresh symbol all_140_0 gives: % 29.61/4.67 | | | | (112) ref(int) = all_140_0 & sort1(all_140_0, all_106_0) = 0 & % 29.61/4.67 | | | | ty(all_140_0) % 29.61/4.67 | | | | % 29.61/4.67 | | | | ALPHA: (112) implies: % 29.61/4.67 | | | | (113) sort1(all_140_0, all_106_0) = 0 % 29.61/4.67 | | | | (114) ref(int) = all_140_0 % 29.61/4.67 | | | | % 29.61/4.67 | | | | DELTA: instantiating (107) with fresh symbols all_147_0, all_147_1, % 29.61/4.67 | | | | all_147_2 gives: % 29.61/4.67 | | | | (115) (all_147_0 = all_106_0 & mk_ref(int, all_59_13) = all_106_0) | % 29.61/4.67 | | | | ( ~ (all_147_1 = 0) & ref(int) = all_147_2 & sort1(all_147_2, % 29.61/4.67 | | | | all_106_0) = all_147_1 & ty(all_147_2)) % 29.61/4.67 | | | | % 29.61/4.67 | | | | BETA: splitting (115) gives: % 29.61/4.67 | | | | % 29.61/4.67 | | | | Case 1: % 29.61/4.67 | | | | | % 29.61/4.67 | | | | | % 29.61/4.67 | | | | | GROUND_INST: instantiating (1) with all_138_0, all_104_0, simplifying % 29.61/4.67 | | | | | with (78), (110), (111) gives: % 29.61/4.68 | | | | | (116) ? [v0: uni] : (contents(all_138_0, v0) = all_104_0 & % 29.61/4.68 | | | | | mk_ref(all_138_0, all_104_0) = v0 & uni(v0)) % 29.61/4.68 | | | | | % 29.61/4.68 | | | | | DELTA: instantiating (116) with fresh symbol all_184_0 gives: % 29.61/4.68 | | | | | (117) contents(all_138_0, all_184_0) = all_104_0 & % 29.61/4.68 | | | | | mk_ref(all_138_0, all_104_0) = all_184_0 & uni(all_184_0) % 29.61/4.68 | | | | | % 29.61/4.68 | | | | | ALPHA: (117) implies: % 29.61/4.68 | | | | | (118) uni(all_184_0) % 29.61/4.68 | | | | | (119) mk_ref(all_138_0, all_104_0) = all_184_0 % 29.61/4.68 | | | | | (120) contents(all_138_0, all_184_0) = all_104_0 % 29.61/4.68 | | | | | % 29.61/4.68 | | | | | BETA: splitting (44) gives: % 29.61/4.68 | | | | | % 29.61/4.68 | | | | | Case 1: % 29.61/4.68 | | | | | | % 29.61/4.68 | | | | | | (121) ~ (all_59_11 = -1) % 29.61/4.68 | | | | | | % 29.61/4.68 | | | | | | BETA: splitting (42) gives: % 29.61/4.68 | | | | | | % 29.61/4.68 | | | | | | Case 1: % 29.61/4.68 | | | | | | | % 29.61/4.68 | | | | | | | (122) all_59_8 = 0 & $lesseq(1, $difference(all_59_20, % 29.61/4.68 | | | | | | | all_59_11)) & $lesseq(all_59_18, % 29.61/4.68 | | | | | | | $difference(all_59_11, all_59_12)) & tb2t(all_59_9) = 0 % 29.61/4.68 | | | | | | | & t2tb(all_59_11) = all_59_10 & get(int, int, all_59_17, % 29.61/4.68 | | | | | | | all_59_10) = all_59_9 & uni(all_59_9) & uni(all_59_10) % 29.61/4.68 | | | | | | | & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.61/4.68 | | | | | | | $difference(all_59_11, v0))) | ~ % 29.61/4.68 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.68 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.68 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.68 | | | | | | | = v2 & uni(v2))) % 29.61/4.68 | | | | | | | % 29.61/4.68 | | | | | | | ALPHA: (122) implies: % 29.61/4.68 | | | | | | | (123) all_59_8 = 0 % 29.61/4.68 | | | | | | | (124) $lesseq(all_59_18, $difference(all_59_11, all_59_12)) % 29.61/4.68 | | | | | | | (125) $lesseq(1, $difference(all_59_20, all_59_11)) % 29.61/4.68 | | | | | | | (126) get(int, int, all_59_17, all_59_10) = all_59_9 % 29.61/4.68 | | | | | | | (127) t2tb(all_59_11) = all_59_10 % 29.61/4.68 | | | | | | | (128) tb2t(all_59_9) = 0 % 29.61/4.68 | | | | | | | (129) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.61/4.68 | | | | | | | $difference(all_59_11, v0))) | ~ % 29.61/4.68 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.68 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.68 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.68 | | | | | | | = v2 & uni(v2))) % 29.61/4.68 | | | | | | | % 29.61/4.68 | | | | | | | BETA: splitting (108) gives: % 29.61/4.68 | | | | | | | % 29.61/4.68 | | | | | | | Case 1: % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | (130) $lesseq(all_59_18, -1) % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | COMBINE_INEQS: (26), (130) imply: % 29.61/4.68 | | | | | | | | (131) $false % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | CLOSE: (131) is inconsistent. % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | Case 2: % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | (132) ~ ($lesseq(2, $difference(all_112_0, all_59_18))) | ? % 29.61/4.68 | | | | | | | | [v0: uni] : ? [v1: int] : ? [v2: int] : ($lesseq(-1, % 29.61/4.68 | | | | | | | | $difference(v1, v2)) & tb2t(v0) = v1 & % 29.61/4.68 | | | | | | | | tb2t(all_59_13) = v2 & get2(int, all_59_16, % 29.61/4.68 | | | | | | | | $sum(all_59_18, 1)) = v0 & uni(v0)) % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | BETA: splitting (132) gives: % 29.61/4.68 | | | | | | | | % 29.61/4.68 | | | | | | | | Case 1: % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | (133) $lesseq(-1, $difference(all_59_18, all_112_0)) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | REDUCE: (102), (133) imply: % 29.61/4.68 | | | | | | | | | (134) $lesseq(-1, $difference(all_59_18, all_59_20)) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | COMBINE_INEQS: (124), (125) imply: % 29.61/4.68 | | | | | | | | | (135) $lesseq(1, $sum($difference($product(-1, all_59_12), % 29.61/4.68 | | | | | | | | | all_59_18), all_59_20)) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | COMBINE_INEQS: (27), (135) imply: % 29.61/4.68 | | | | | | | | | (136) $lesseq(2, $difference(all_59_20, all_59_18)) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | COMBINE_INEQS: (134), (136) imply: % 29.61/4.68 | | | | | | | | | (137) $false % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | CLOSE: (137) is inconsistent. % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | Case 2: % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | (138) ? [v0: uni] : ? [v1: int] : ? [v2: int] : % 29.61/4.68 | | | | | | | | | ($lesseq(-1, $difference(v1, v2)) & tb2t(v0) = v1 & % 29.61/4.68 | | | | | | | | | tb2t(all_59_13) = v2 & get2(int, all_59_16, % 29.61/4.68 | | | | | | | | | $sum(all_59_18, 1)) = v0 & uni(v0)) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | DELTA: instantiating (138) with fresh symbols all_229_0, % 29.61/4.68 | | | | | | | | | all_229_1, all_229_2 gives: % 29.61/4.68 | | | | | | | | | (139) $lesseq(-1, $difference(all_229_1, all_229_0)) & % 29.61/4.68 | | | | | | | | | tb2t(all_229_2) = all_229_1 & tb2t(all_59_13) = % 29.61/4.68 | | | | | | | | | all_229_0 & get2(int, all_59_16, $sum(all_59_18, 1)) % 29.61/4.68 | | | | | | | | | = all_229_2 & uni(all_229_2) % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | ALPHA: (139) implies: % 29.61/4.68 | | | | | | | | | (140) get2(int, all_59_16, $sum(all_59_18, 1)) = all_229_2 % 29.61/4.68 | | | | | | | | | (141) tb2t(all_59_13) = all_229_0 % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | GROUND_INST: instantiating (14) with all_59_12, all_229_0, % 29.61/4.68 | | | | | | | | | all_59_13, simplifying with (38), (141) gives: % 29.61/4.68 | | | | | | | | | (142) all_229_0 = all_59_12 % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | BETA: splitting (43) gives: % 29.61/4.68 | | | | | | | | | % 29.61/4.68 | | | | | | | | | Case 1: % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | (143) $lesseq(1, $difference(all_59_18, all_59_11)) % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | COMBINE_INEQS: (124), (143) imply: % 29.61/4.68 | | | | | | | | | | (144) $lesseq(all_59_12, -1) % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | COMBINE_INEQS: (27), (144) imply: % 29.61/4.68 | | | | | | | | | | (145) $false % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | CLOSE: (145) is inconsistent. % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | Case 2: % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | (146) ~ ($lesseq(1, $difference(all_59_20, all_59_11))) % 29.61/4.68 | | | | | | | | | | | (all_59_4 = 0 & $lesseq(1, $difference(all_59_11, % 29.61/4.68 | | | | | | | | | | all_59_7)) & $lesseq(all_59_18, all_59_7) & % 29.61/4.68 | | | | | | | | | | tb2t(all_59_5) = 0 & t2tb(all_59_7) = all_59_6 & % 29.61/4.68 | | | | | | | | | | get(int, int, all_59_17, all_59_6) = all_59_5 & % 29.61/4.68 | | | | | | | | | | uni(all_59_5) & uni(all_59_6)) | ( ~ (all_59_8 = % 29.61/4.68 | | | | | | | | | | 0) & tb2t(all_59_9) = all_59_8 & % 29.61/4.68 | | | | | | | | | | t2tb(all_59_11) = all_59_10 & get(int, int, % 29.61/4.68 | | | | | | | | | | all_59_17, all_59_10) = all_59_9 & % 29.61/4.68 | | | | | | | | | | uni(all_59_9) & uni(all_59_10)) % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | BETA: splitting (146) gives: % 29.61/4.68 | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | Case 1: % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | (147) $lesseq(all_59_20, all_59_11) % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | COMBINE_INEQS: (125), (147) imply: % 29.61/4.68 | | | | | | | | | | | (148) $false % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | CLOSE: (148) is inconsistent. % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | Case 2: % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | (149) (all_59_4 = 0 & $lesseq(1, $difference(all_59_11, % 29.61/4.68 | | | | | | | | | | | all_59_7)) & $lesseq(all_59_18, all_59_7) & % 29.61/4.68 | | | | | | | | | | | tb2t(all_59_5) = 0 & t2tb(all_59_7) = all_59_6 & % 29.61/4.68 | | | | | | | | | | | get(int, int, all_59_17, all_59_6) = all_59_5 & % 29.61/4.68 | | | | | | | | | | | uni(all_59_5) & uni(all_59_6)) | ( ~ (all_59_8 = % 29.61/4.68 | | | | | | | | | | | 0) & tb2t(all_59_9) = all_59_8 & % 29.61/4.68 | | | | | | | | | | | t2tb(all_59_11) = all_59_10 & get(int, int, % 29.61/4.68 | | | | | | | | | | | all_59_17, all_59_10) = all_59_9 & % 29.61/4.68 | | | | | | | | | | | uni(all_59_9) & uni(all_59_10)) % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | BETA: splitting (149) gives: % 29.61/4.68 | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | Case 1: % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | (150) all_59_4 = 0 & $lesseq(1, $difference(all_59_11, % 29.61/4.68 | | | | | | | | | | | | all_59_7)) & $lesseq(all_59_18, all_59_7) & % 29.61/4.68 | | | | | | | | | | | | tb2t(all_59_5) = 0 & t2tb(all_59_7) = all_59_6 & % 29.61/4.68 | | | | | | | | | | | | get(int, int, all_59_17, all_59_6) = all_59_5 & % 29.61/4.68 | | | | | | | | | | | | uni(all_59_5) & uni(all_59_6) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | ALPHA: (150) implies: % 29.61/4.68 | | | | | | | | | | | | (151) $lesseq(all_59_18, all_59_7) % 29.61/4.68 | | | | | | | | | | | | (152) $lesseq(1, $difference(all_59_11, all_59_7)) % 29.61/4.68 | | | | | | | | | | | | (153) get(int, int, all_59_17, all_59_6) = all_59_5 % 29.61/4.68 | | | | | | | | | | | | (154) t2tb(all_59_7) = all_59_6 % 29.61/4.68 | | | | | | | | | | | | (155) tb2t(all_59_5) = 0 % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (mk_ref_sort1) with all_138_0, % 29.61/4.68 | | | | | | | | | | | | all_104_0, all_184_0, simplifying with (78), % 29.61/4.68 | | | | | | | | | | | | (110), (119) gives: % 29.61/4.68 | | | | | | | | | | | | (156) ? [v0: ty] : (ref(all_138_0) = v0 & sort1(v0, % 29.61/4.68 | | | | | | | | | | | | all_184_0) = 0 & ty(v0)) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_138_0, all_184_0, % 29.61/4.68 | | | | | | | | | | | | all_104_0, simplifying with (110), (118), (120) % 29.61/4.68 | | | | | | | | | | | | gives: % 29.61/4.68 | | | | | | | | | | | | (157) ? [v0: ty] : ? [v1: int] : ? [v2: int] : ((v2 = % 29.61/4.68 | | | | | | | | | | | | all_184_0 & mk_ref(all_138_0, all_104_0) = % 29.61/4.68 | | | | | | | | | | | | all_184_0) | ( ~ (v1 = 0) & ref(all_138_0) = % 29.61/4.68 | | | | | | | | | | | | v0 & sort1(v0, all_184_0) = v1 & ty(v0))) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (101) with $sum(all_59_18, 1), % 29.61/4.68 | | | | | | | | | | | | all_229_2, simplifying with (140) gives: % 29.61/4.68 | | | | | | | | | | | | (158) ~ ($lesseq(3, $difference(all_112_0, all_59_18))) % 29.61/4.68 | | | | | | | | | | | | | ~ ($lesseq(-1, all_59_18)) | ? [v0: uni] : ? % 29.61/4.68 | | | | | | | | | | | | [v1: int] : ? [v2: int] : ($lesseq(-1, % 29.61/4.68 | | | | | | | | | | | | $difference(v1, v2)) & tb2t(v0) = v1 & % 29.61/4.68 | | | | | | | | | | | | tb2t(all_229_2) = v2 & get2(int, all_59_16, % 29.61/4.68 | | | | | | | | | | | | $sum(all_59_18, 2)) = v0 & uni(v0)) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (4) with int, all_59_16, all_59_11, % 29.61/4.68 | | | | | | | | | | | | all_59_17, all_59_10, all_59_9, simplifying with % 29.61/4.68 | | | | | | | | | | | | (10), (30), (61), (126), (127) gives: % 29.61/4.68 | | | | | | | | | | | | (159) get2(int, all_59_16, all_59_11) = all_59_9 & % 29.61/4.68 | | | | | | | | | | | | uni(all_59_9) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | ALPHA: (159) implies: % 29.61/4.68 | | | | | | | | | | | | (160) uni(all_59_9) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (4) with int, all_59_16, all_59_7, % 29.61/4.68 | | | | | | | | | | | | all_59_17, all_59_6, all_59_5, simplifying with % 29.61/4.68 | | | | | | | | | | | | (10), (30), (61), (153), (154) gives: % 29.61/4.68 | | | | | | | | | | | | (161) get2(int, all_59_16, all_59_7) = all_59_5 & % 29.61/4.68 | | | | | | | | | | | | uni(all_59_5) % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | ALPHA: (161) implies: % 29.61/4.68 | | | | | | | | | | | | (162) uni(all_59_5) % 29.61/4.68 | | | | | | | | | | | | (163) get2(int, all_59_16, all_59_7) = all_59_5 % 29.61/4.68 | | | | | | | | | | | | % 29.61/4.68 | | | | | | | | | | | | GROUND_INST: instantiating (129) with all_59_7, all_59_6, % 29.61/4.68 | | | | | | | | | | | | simplifying with (154) gives: % 29.61/4.69 | | | | | | | | | | | | (164) ~ ($lesseq(1, $difference(all_59_11, all_59_7))) % 29.61/4.69 | | | | | | | | | | | | | ~ ($lesseq(all_59_18, $difference(all_59_7, % 29.61/4.69 | | | | | | | | | | | | all_59_12))) | ? [v0: uni] : ? [v1: int] : % 29.61/4.69 | | | | | | | | | | | | ( ~ (v1 = 0) & tb2t(v0) = v1 & get(int, int, % 29.61/4.69 | | | | | | | | | | | | all_59_17, all_59_6) = v0 & uni(v0)) % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_59_9, 0, % 29.61/4.69 | | | | | | | | | | | | simplifying with (128), (160) gives: % 29.61/4.69 | | | | | | | | | | | | (165) t2tb(0) = all_59_9 % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_59_5, 0, % 29.61/4.69 | | | | | | | | | | | | simplifying with (155), (162) gives: % 29.61/4.69 | | | | | | | | | | | | (166) t2tb(0) = all_59_5 % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | DELTA: instantiating (156) with fresh symbol all_275_0 % 29.61/4.69 | | | | | | | | | | | | gives: % 29.61/4.69 | | | | | | | | | | | | (167) ref(all_138_0) = all_275_0 & sort1(all_275_0, % 29.61/4.69 | | | | | | | | | | | | all_184_0) = 0 & ty(all_275_0) % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | ALPHA: (167) implies: % 29.61/4.69 | | | | | | | | | | | | (168) sort1(all_275_0, all_184_0) = 0 % 29.61/4.69 | | | | | | | | | | | | (169) ref(all_138_0) = all_275_0 % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | DELTA: instantiating (157) with fresh symbols all_283_0, % 29.61/4.69 | | | | | | | | | | | | all_283_1, all_283_2 gives: % 29.61/4.69 | | | | | | | | | | | | (170) (all_283_0 = all_184_0 & mk_ref(all_138_0, % 29.61/4.69 | | | | | | | | | | | | all_104_0) = all_184_0) | ( ~ (all_283_1 = 0) % 29.61/4.69 | | | | | | | | | | | | & ref(all_138_0) = all_283_2 & sort1(all_283_2, % 29.61/4.69 | | | | | | | | | | | | all_184_0) = all_283_1 & ty(all_283_2)) % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | BETA: splitting (164) gives: % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | (171) $lesseq(all_59_11, all_59_7) % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | COMBINE_INEQS: (152), (171) imply: % 29.61/4.69 | | | | | | | | | | | | | (172) $false % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | CLOSE: (172) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | (173) ~ ($lesseq(all_59_18, $difference(all_59_7, % 29.61/4.69 | | | | | | | | | | | | | all_59_12))) | ? [v0: uni] : ? [v1: int] : % 29.61/4.69 | | | | | | | | | | | | | ( ~ (v1 = 0) & tb2t(v0) = v1 & get(int, int, % 29.61/4.69 | | | | | | | | | | | | | all_59_17, all_59_6) = v0 & uni(v0)) % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | BETA: splitting (173) gives: % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | (174) $lesseq(1, $sum($difference(all_59_12, all_59_7), % 29.61/4.69 | | | | | | | | | | | | | | all_59_18)) % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | GROUND_INST: instantiating (93) with all_59_18, all_59_7, % 29.61/4.69 | | | | | | | | | | | | | | all_59_5, 0, all_59_13, all_59_12, simplifying % 29.61/4.69 | | | | | | | | | | | | | | with (38), (74), (155), (163) gives: % 29.61/4.69 | | | | | | | | | | | | | | (175) ~ ($lesseq(1, $difference(all_110_0, all_59_7))) % 29.61/4.69 | | | | | | | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, % 29.61/4.69 | | | | | | | | | | | | | | all_59_7), all_59_18))) | ~ % 29.61/4.69 | | | | | | | | | | | | | | ($lesseq(all_59_18, all_59_7)) | ~ ($lesseq(0, % 29.61/4.69 | | | | | | | | | | | | | | all_59_18)) % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | BETA: splitting (175) gives: % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | (176) $lesseq(all_59_18, -1) % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | COMBINE_INEQS: (26), (176) imply: % 29.61/4.69 | | | | | | | | | | | | | | | (177) $false % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | CLOSE: (177) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | (178) ~ ($lesseq(1, $difference(all_110_0, all_59_7))) % 29.61/4.69 | | | | | | | | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, % 29.61/4.69 | | | | | | | | | | | | | | | all_59_7), all_59_18))) | ~ % 29.61/4.69 | | | | | | | | | | | | | | | ($lesseq(all_59_18, all_59_7)) % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | BETA: splitting (178) gives: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | (179) $lesseq(1, $difference(all_59_18, all_59_7)) % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | COMBINE_INEQS: (151), (179) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | (180) $false % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | CLOSE: (180) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | (181) ~ ($lesseq(1, $difference(all_110_0, all_59_7))) % 29.61/4.69 | | | | | | | | | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, % 29.61/4.69 | | | | | | | | | | | | | | | | all_59_7), all_59_18))) % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | BETA: splitting (181) gives: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | (182) $lesseq(all_110_0, all_59_7) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | REDUCE: (104), (182) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (183) $lesseq(all_59_20, all_59_7) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (152), (183) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (184) $lesseq(1, $difference(all_59_11, all_59_20)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (125), (184) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (185) $false % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | CLOSE: (185) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | (186) $lesseq(all_59_18, $difference(all_59_7, % 29.61/4.69 | | | | | | | | | | | | | | | | | all_59_12)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (174), (186) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (187) $false % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | CLOSE: (187) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | (188) $lesseq(all_59_18, $difference(all_59_7, % 29.61/4.69 | | | | | | | | | | | | | | all_59_12)) % 29.61/4.69 | | | | | | | | | | | | | | (189) ? [v0: uni] : ? [v1: int] : ( ~ (v1 = 0) & % 29.61/4.69 | | | | | | | | | | | | | | tb2t(v0) = v1 & get(int, int, all_59_17, % 29.61/4.69 | | | | | | | | | | | | | | all_59_6) = v0 & uni(v0)) % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | DELTA: instantiating (189) with fresh symbols all_305_0, % 29.61/4.69 | | | | | | | | | | | | | | all_305_1 gives: % 29.61/4.69 | | | | | | | | | | | | | | (190) ~ (all_305_0 = 0) & tb2t(all_305_1) = all_305_0 & % 29.61/4.69 | | | | | | | | | | | | | | get(int, int, all_59_17, all_59_6) = all_305_1 & % 29.61/4.69 | | | | | | | | | | | | | | uni(all_305_1) % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | ALPHA: (190) implies: % 29.61/4.69 | | | | | | | | | | | | | | (191) ~ (all_305_0 = 0) % 29.61/4.69 | | | | | | | | | | | | | | (192) get(int, int, all_59_17, all_59_6) = all_305_1 % 29.61/4.69 | | | | | | | | | | | | | | (193) tb2t(all_305_1) = all_305_0 % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | BETA: splitting (170) gives: % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with all_59_5, all_305_1, % 29.61/4.69 | | | | | | | | | | | | | | | all_59_6, all_59_17, int, int, simplifying with % 29.61/4.69 | | | | | | | | | | | | | | | (153), (192) gives: % 29.61/4.69 | | | | | | | | | | | | | | | (194) all_305_1 = all_59_5 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_59_9, all_59_5, 0, % 29.61/4.69 | | | | | | | | | | | | | | | simplifying with (165), (166) gives: % 29.61/4.69 | | | | | | | | | | | | | | | (195) all_59_5 = all_59_9 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | COMBINE_EQS: (194), (195) imply: % 29.61/4.69 | | | | | | | | | | | | | | | (196) all_305_1 = all_59_9 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | REDUCE: (193), (196) imply: % 29.61/4.69 | | | | | | | | | | | | | | | (197) tb2t(all_59_9) = all_305_0 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_305_0, all_59_9, % 29.61/4.69 | | | | | | | | | | | | | | | simplifying with (128), (197) gives: % 29.61/4.69 | | | | | | | | | | | | | | | (198) all_305_0 = 0 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | REDUCE: (191), (198) imply: % 29.61/4.69 | | | | | | | | | | | | | | | (199) $false % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | CLOSE: (199) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | (200) ~ (all_283_1 = 0) & ref(all_138_0) = all_283_2 & % 29.61/4.69 | | | | | | | | | | | | | | | sort1(all_283_2, all_184_0) = all_283_1 & % 29.61/4.69 | | | | | | | | | | | | | | | ty(all_283_2) % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | ALPHA: (200) implies: % 29.61/4.69 | | | | | | | | | | | | | | | (201) ~ (all_283_1 = 0) % 29.61/4.69 | | | | | | | | | | | | | | | (202) sort1(all_283_2, all_184_0) = all_283_1 % 29.61/4.69 | | | | | | | | | | | | | | | (203) ref(all_138_0) = all_283_2 % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | BETA: splitting (158) gives: % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | (204) $lesseq(all_59_18, -2) % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | COMBINE_INEQS: (26), (204) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | (205) $false % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | CLOSE: (205) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | (206) ~ ($lesseq(3, $difference(all_112_0, all_59_18))) % 29.61/4.69 | | | | | | | | | | | | | | | | | ? [v0: uni] : ? [v1: int] : ? [v2: int] : % 29.61/4.69 | | | | | | | | | | | | | | | | ($lesseq(-1, $difference(v1, v2)) & tb2t(v0) = v1 % 29.61/4.69 | | | | | | | | | | | | | | | | & tb2t(all_229_2) = v2 & get2(int, all_59_16, % 29.61/4.69 | | | | | | | | | | | | | | | | $sum(all_59_18, 2)) = v0 & uni(v0)) % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | BETA: splitting (206) gives: % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | Case 1: % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | (207) $lesseq(-2, $difference(all_59_18, all_112_0)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | REDUCE: (102), (207) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (208) $lesseq(-2, $difference(all_59_18, all_59_20)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (152), (188) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (209) $lesseq(1, $difference($difference(all_59_11, % 29.61/4.69 | | | | | | | | | | | | | | | | | all_59_12), all_59_18)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (125), (209) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (210) $lesseq(2, $sum($difference($product(-1, % 29.61/4.69 | | | | | | | | | | | | | | | | | all_59_12), all_59_18), all_59_20)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (27), (210) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (211) $lesseq(3, $difference(all_59_20, all_59_18)) % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (208), (211) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (212) $false % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | CLOSE: (212) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_275_0, all_283_2, % 29.61/4.69 | | | | | | | | | | | | | | | | | all_138_0, simplifying with (169), (203) gives: % 29.61/4.69 | | | | | | | | | | | | | | | | | (213) all_283_2 = all_275_0 % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | REDUCE: (202), (213) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (214) sort1(all_275_0, all_184_0) = all_283_1 % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_283_1, all_184_0, % 29.61/4.69 | | | | | | | | | | | | | | | | | all_275_0, simplifying with (168), (214) gives: % 29.61/4.69 | | | | | | | | | | | | | | | | | (215) all_283_1 = 0 % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | REDUCE: (201), (215) imply: % 29.61/4.69 | | | | | | | | | | | | | | | | | (216) $false % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | | CLOSE: (216) is inconsistent. % 29.61/4.69 | | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | End of split % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | Case 2: % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | (217) ~ (all_59_8 = 0) & tb2t(all_59_9) = all_59_8 & % 29.61/4.69 | | | | | | | | | | | | t2tb(all_59_11) = all_59_10 & get(int, int, % 29.61/4.69 | | | | | | | | | | | | all_59_17, all_59_10) = all_59_9 & uni(all_59_9) % 29.61/4.69 | | | | | | | | | | | | & uni(all_59_10) % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.69 | | | | | | | | | | | | ALPHA: (217) implies: % 29.61/4.69 | | | | | | | | | | | | (218) ~ (all_59_8 = 0) % 29.61/4.69 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | REDUCE: (123), (218) imply: % 29.61/4.70 | | | | | | | | | | | | (219) $false % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | CLOSE: (219) is inconsistent. % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | End of split % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | End of split % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | Case 2: % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | (220) all_59_11 = -1 & ! [v0: int] : ! [v1: uni] : ( ~ % 29.61/4.70 | | | | | | | ($lesseq(1, $difference(all_59_20, v0))) | ~ % 29.61/4.70 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.70 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.70 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.70 | | | | | | | = v2 & uni(v2))) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | ALPHA: (220) implies: % 29.61/4.70 | | | | | | | (221) all_59_11 = -1 % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | REDUCE: (121), (221) imply: % 29.61/4.70 | | | | | | | (222) $false % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | CLOSE: (222) is inconsistent. % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | End of split % 29.61/4.70 | | | | | | % 29.61/4.70 | | | | | Case 2: % 29.61/4.70 | | | | | | % 29.61/4.70 | | | | | | (223) all_59_11 = -1 % 29.61/4.70 | | | | | | (224) all_59_0 = 0 & $lesseq(1, $difference(all_59_20, all_59_3)) % 29.61/4.70 | | | | | | & $lesseq(all_59_18, all_59_3) & tb2t(all_59_1) = 0 & % 29.61/4.70 | | | | | | t2tb(all_59_3) = all_59_2 & get(int, int, all_59_17, % 29.61/4.70 | | | | | | all_59_2) = all_59_1 & uni(all_59_1) & uni(all_59_2) % 29.61/4.70 | | | | | | % 29.61/4.70 | | | | | | ALPHA: (224) implies: % 29.61/4.70 | | | | | | (225) $lesseq(all_59_18, all_59_3) % 29.61/4.70 | | | | | | (226) $lesseq(1, $difference(all_59_20, all_59_3)) % 29.61/4.70 | | | | | | (227) get(int, int, all_59_17, all_59_2) = all_59_1 % 29.61/4.70 | | | | | | (228) t2tb(all_59_3) = all_59_2 % 29.61/4.70 | | | | | | (229) tb2t(all_59_1) = 0 % 29.61/4.70 | | | | | | % 29.61/4.70 | | | | | | BETA: splitting (42) gives: % 29.61/4.70 | | | | | | % 29.61/4.70 | | | | | | Case 1: % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | (230) all_59_8 = 0 & $lesseq(1, $difference(all_59_20, % 29.61/4.70 | | | | | | | all_59_11)) & $lesseq(all_59_18, % 29.61/4.70 | | | | | | | $difference(all_59_11, all_59_12)) & tb2t(all_59_9) = 0 % 29.61/4.70 | | | | | | | & t2tb(all_59_11) = all_59_10 & get(int, int, all_59_17, % 29.61/4.70 | | | | | | | all_59_10) = all_59_9 & uni(all_59_9) & uni(all_59_10) % 29.61/4.70 | | | | | | | & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.61/4.70 | | | | | | | $difference(all_59_11, v0))) | ~ % 29.61/4.70 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.70 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.70 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.70 | | | | | | | = v2 & uni(v2))) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | ALPHA: (230) implies: % 29.61/4.70 | | | | | | | (231) $lesseq(all_59_18, $difference(all_59_11, all_59_12)) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | REDUCE: (223), (231) imply: % 29.61/4.70 | | | | | | | (232) $lesseq(1, $difference($product(-1, all_59_12), % 29.61/4.70 | | | | | | | all_59_18)) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | COMBINE_INEQS: (28), (232) imply: % 29.61/4.70 | | | | | | | (233) $false % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | CLOSE: (233) is inconsistent. % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | Case 2: % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | (234) all_59_11 = -1 & ! [v0: int] : ! [v1: uni] : ( ~ % 29.61/4.70 | | | | | | | ($lesseq(1, $difference(all_59_20, v0))) | ~ % 29.61/4.70 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.70 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.70 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.70 | | | | | | | = v2 & uni(v2))) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | ALPHA: (234) implies: % 29.61/4.70 | | | | | | | (235) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 29.61/4.70 | | | | | | | $difference(all_59_20, v0))) | ~ % 29.61/4.70 | | | | | | | ($lesseq(all_59_18, $difference(v0, all_59_12))) | ~ % 29.61/4.70 | | | | | | | (t2tb(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 % 29.61/4.70 | | | | | | | = 0) & tb2t(v2) = v3 & get(int, int, all_59_17, v1) % 29.61/4.70 | | | | | | | = v2 & uni(v2))) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | GROUND_INST: instantiating (4) with int, all_59_16, all_59_3, % 29.61/4.70 | | | | | | | all_59_17, all_59_2, all_59_1, simplifying with (10), % 29.61/4.70 | | | | | | | (30), (61), (227), (228) gives: % 29.61/4.70 | | | | | | | (236) get2(int, all_59_16, all_59_3) = all_59_1 & uni(all_59_1) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | ALPHA: (236) implies: % 29.61/4.70 | | | | | | | (237) get2(int, all_59_16, all_59_3) = all_59_1 % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | GROUND_INST: instantiating (235) with all_59_3, all_59_2, % 29.61/4.70 | | | | | | | simplifying with (228) gives: % 29.61/4.70 | | | | | | | (238) ~ ($lesseq(1, $difference(all_59_20, all_59_3))) | ~ % 29.61/4.70 | | | | | | | ($lesseq(all_59_18, $difference(all_59_3, all_59_12))) | % 29.61/4.70 | | | | | | | ? [v0: uni] : ? [v1: int] : ( ~ (v1 = 0) & tb2t(v0) = v1 % 29.61/4.70 | | | | | | | & get(int, int, all_59_17, all_59_2) = v0 & uni(v0)) % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | BETA: splitting (238) gives: % 29.61/4.70 | | | | | | | % 29.61/4.70 | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | (239) $lesseq(all_59_20, all_59_3) % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | COMBINE_INEQS: (226), (239) imply: % 29.61/4.70 | | | | | | | | (240) $false % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | CLOSE: (240) is inconsistent. % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | (241) ~ ($lesseq(all_59_18, $difference(all_59_3, % 29.61/4.70 | | | | | | | | all_59_12))) | ? [v0: uni] : ? [v1: int] : ( ~ % 29.61/4.70 | | | | | | | | (v1 = 0) & tb2t(v0) = v1 & get(int, int, all_59_17, % 29.61/4.70 | | | | | | | | all_59_2) = v0 & uni(v0)) % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | BETA: splitting (241) gives: % 29.61/4.70 | | | | | | | | % 29.61/4.70 | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | (242) $lesseq(1, $sum($difference(all_59_12, all_59_3), % 29.61/4.70 | | | | | | | | | all_59_18)) % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | GROUND_INST: instantiating (93) with all_59_18, all_59_3, % 29.61/4.70 | | | | | | | | | all_59_1, 0, all_59_13, all_59_12, simplifying % 29.61/4.70 | | | | | | | | | with (38), (74), (229), (237) gives: % 29.61/4.70 | | | | | | | | | (243) ~ ($lesseq(1, $difference(all_110_0, all_59_3))) | % 29.61/4.70 | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, all_59_3), % 29.61/4.70 | | | | | | | | | all_59_18))) | ~ ($lesseq(all_59_18, % 29.61/4.70 | | | | | | | | | all_59_3)) | ~ ($lesseq(0, all_59_18)) % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | BETA: splitting (243) gives: % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | (244) $lesseq(all_59_18, -1) % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | COMBINE_INEQS: (26), (244) imply: % 29.61/4.70 | | | | | | | | | | (245) $false % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | CLOSE: (245) is inconsistent. % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | (246) ~ ($lesseq(1, $difference(all_110_0, all_59_3))) | % 29.61/4.70 | | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, % 29.61/4.70 | | | | | | | | | | all_59_3), all_59_18))) | ~ % 29.61/4.70 | | | | | | | | | | ($lesseq(all_59_18, all_59_3)) % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | BETA: splitting (246) gives: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | (247) $lesseq(1, $difference(all_59_18, all_59_3)) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | COMBINE_INEQS: (225), (247) imply: % 29.61/4.70 | | | | | | | | | | | (248) $false % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | CLOSE: (248) is inconsistent. % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | (249) ~ ($lesseq(1, $difference(all_110_0, all_59_3))) % 29.61/4.70 | | | | | | | | | | | | ~ ($lesseq(1, $sum($difference(all_59_12, % 29.61/4.70 | | | | | | | | | | | all_59_3), all_59_18))) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | BETA: splitting (249) gives: % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | (250) $lesseq(all_110_0, all_59_3) % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | REDUCE: (104), (250) imply: % 29.61/4.70 | | | | | | | | | | | | (251) $lesseq(all_59_20, all_59_3) % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | COMBINE_INEQS: (226), (251) imply: % 29.61/4.70 | | | | | | | | | | | | (252) $false % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | CLOSE: (252) is inconsistent. % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | (253) $lesseq(all_59_18, $difference(all_59_3, % 29.61/4.70 | | | | | | | | | | | | all_59_12)) % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | COMBINE_INEQS: (242), (253) imply: % 29.61/4.70 | | | | | | | | | | | | (254) $false % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | | CLOSE: (254) is inconsistent. % 29.61/4.70 | | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | End of split % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | (255) $lesseq(all_59_18, $difference(all_59_3, all_59_12)) % 29.61/4.70 | | | | | | | | | (256) ? [v0: uni] : ? [v1: int] : ( ~ (v1 = 0) & tb2t(v0) % 29.61/4.70 | | | | | | | | | = v1 & get(int, int, all_59_17, all_59_2) = v0 & % 29.61/4.70 | | | | | | | | | uni(v0)) % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | DELTA: instantiating (256) with fresh symbols all_264_0, % 29.61/4.70 | | | | | | | | | all_264_1 gives: % 29.61/4.70 | | | | | | | | | (257) ~ (all_264_0 = 0) & tb2t(all_264_1) = all_264_0 & % 29.61/4.70 | | | | | | | | | get(int, int, all_59_17, all_59_2) = all_264_1 & % 29.61/4.70 | | | | | | | | | uni(all_264_1) % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | ALPHA: (257) implies: % 29.61/4.70 | | | | | | | | | (258) ~ (all_264_0 = 0) % 29.61/4.70 | | | | | | | | | (259) get(int, int, all_59_17, all_59_2) = all_264_1 % 29.61/4.70 | | | | | | | | | (260) tb2t(all_264_1) = all_264_0 % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | BETA: splitting (108) gives: % 29.61/4.70 | | | | | | | | | % 29.61/4.70 | | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | (261) $lesseq(all_59_18, -1) % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | COMBINE_INEQS: (26), (261) imply: % 29.61/4.70 | | | | | | | | | | (262) $false % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | CLOSE: (262) is inconsistent. % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | (263) ~ ($lesseq(2, $difference(all_112_0, all_59_18))) % 29.61/4.70 | | | | | | | | | | | ? [v0: uni] : ? [v1: int] : ? [v2: int] : % 29.61/4.70 | | | | | | | | | | ($lesseq(-1, $difference(v1, v2)) & tb2t(v0) = v1 & % 29.61/4.70 | | | | | | | | | | tb2t(all_59_13) = v2 & get2(int, all_59_16, % 29.61/4.70 | | | | | | | | | | $sum(all_59_18, 1)) = v0 & uni(v0)) % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | BETA: splitting (263) gives: % 29.61/4.70 | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | Case 1: % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | (264) $lesseq(-1, $difference(all_59_18, all_112_0)) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | REDUCE: (102), (264) imply: % 29.61/4.70 | | | | | | | | | | | (265) $lesseq(-1, $difference(all_59_18, all_59_20)) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | COMBINE_INEQS: (226), (255) imply: % 29.61/4.70 | | | | | | | | | | | (266) $lesseq(1, $sum($difference($product(-1, % 29.61/4.70 | | | | | | | | | | | all_59_12), all_59_18), all_59_20)) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | COMBINE_INEQS: (27), (266) imply: % 29.61/4.70 | | | | | | | | | | | (267) $lesseq(2, $difference(all_59_20, all_59_18)) % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | COMBINE_INEQS: (265), (267) imply: % 29.61/4.70 | | | | | | | | | | | (268) $false % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | CLOSE: (268) is inconsistent. % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | Case 2: % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | GROUND_INST: instantiating (20) with all_59_1, all_264_1, % 29.61/4.70 | | | | | | | | | | | all_59_2, all_59_17, int, int, simplifying with % 29.61/4.70 | | | | | | | | | | | (227), (259) gives: % 29.61/4.70 | | | | | | | | | | | (269) all_264_1 = all_59_1 % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | REDUCE: (260), (269) imply: % 29.61/4.70 | | | | | | | | | | | (270) tb2t(all_59_1) = all_264_0 % 29.61/4.70 | | | | | | | | | | | % 29.61/4.70 | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_264_0, all_59_1, % 29.61/4.70 | | | | | | | | | | | simplifying with (229), (270) gives: % 29.61/4.70 | | | | | | | | | | | (271) all_264_0 = 0 % 29.61/4.71 | | | | | | | | | | | % 29.61/4.71 | | | | | | | | | | | REDUCE: (258), (271) imply: % 29.61/4.71 | | | | | | | | | | | (272) $false % 29.61/4.71 | | | | | | | | | | | % 29.61/4.71 | | | | | | | | | | | CLOSE: (272) is inconsistent. % 29.61/4.71 | | | | | | | | | | | % 29.61/4.71 | | | | | | | | | | End of split % 29.61/4.71 | | | | | | | | | | % 29.61/4.71 | | | | | | | | | End of split % 29.61/4.71 | | | | | | | | | % 29.61/4.71 | | | | | | | | End of split % 29.61/4.71 | | | | | | | | % 29.61/4.71 | | | | | | | End of split % 29.61/4.71 | | | | | | | % 29.61/4.71 | | | | | | End of split % 29.61/4.71 | | | | | | % 29.61/4.71 | | | | | End of split % 29.61/4.71 | | | | | % 29.61/4.71 | | | | Case 2: % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | (273) ~ (all_147_1 = 0) & ref(int) = all_147_2 & sort1(all_147_2, % 29.61/4.71 | | | | | all_106_0) = all_147_1 & ty(all_147_2) % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | ALPHA: (273) implies: % 29.61/4.71 | | | | | (274) ~ (all_147_1 = 0) % 29.61/4.71 | | | | | (275) sort1(all_147_2, all_106_0) = all_147_1 % 29.61/4.71 | | | | | (276) ref(int) = all_147_2 % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | GROUND_INST: instantiating (12) with all_140_0, all_147_2, int, % 29.61/4.71 | | | | | simplifying with (114), (276) gives: % 29.61/4.71 | | | | | (277) all_147_2 = all_140_0 % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | REDUCE: (275), (277) imply: % 29.61/4.71 | | | | | (278) sort1(all_140_0, all_106_0) = all_147_1 % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | GROUND_INST: instantiating (17) with 0, all_147_1, all_106_0, % 29.61/4.71 | | | | | all_140_0, simplifying with (113), (278) gives: % 29.61/4.71 | | | | | (279) all_147_1 = 0 % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | REDUCE: (274), (279) imply: % 29.61/4.71 | | | | | (280) $false % 29.61/4.71 | | | | | % 29.61/4.71 | | | | | CLOSE: (280) is inconsistent. % 29.61/4.71 | | | | | % 29.61/4.71 | | | | End of split % 29.61/4.71 | | | | % 29.61/4.71 | | | End of split % 29.61/4.71 | | | % 29.61/4.71 | | End of split % 29.61/4.71 | | % 29.61/4.71 | Case 2: % 29.61/4.71 | | % 29.61/4.71 | | (281) ~ (all_72_1 = 0) & map(int, int) = all_72_2 & sort1(all_72_2, % 29.61/4.71 | | all_59_17) = all_72_1 & ty(all_72_2) % 29.61/4.71 | | % 29.61/4.71 | | ALPHA: (281) implies: % 29.61/4.71 | | (282) ~ (all_72_1 = 0) % 29.61/4.71 | | (283) sort1(all_72_2, all_59_17) = all_72_1 % 29.61/4.71 | | (284) map(int, int) = all_72_2 % 29.61/4.71 | | % 29.61/4.71 | | GROUND_INST: instantiating (18) with all_52_0, all_72_2, int, int, % 29.61/4.71 | | simplifying with (23), (284) gives: % 29.61/4.71 | | (285) all_72_2 = all_52_0 % 29.61/4.71 | | % 29.61/4.71 | | REDUCE: (283), (285) imply: % 29.61/4.71 | | (286) sort1(all_52_0, all_59_17) = all_72_1 % 29.61/4.71 | | % 29.61/4.71 | | GROUND_INST: instantiating (17) with 0, all_72_1, all_59_17, all_52_0, % 29.61/4.71 | | simplifying with (51), (286) gives: % 29.61/4.71 | | (287) all_72_1 = 0 % 29.61/4.71 | | % 29.61/4.71 | | REDUCE: (282), (287) imply: % 29.61/4.71 | | (288) $false % 29.61/4.71 | | % 29.61/4.71 | | CLOSE: (288) is inconsistent. % 29.61/4.71 | | % 29.61/4.71 | End of split % 29.61/4.71 | % 29.61/4.71 End of proof % 29.61/4.71 % SZS output end Proof for theBenchmark % 29.61/4.71 % 29.61/4.71 4112ms %------------------------------------------------------------------------------