%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW594_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 : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:50 EDT 2023 % Result : Theorem 19.47s 3.31s % Output : Proof 25.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW594_2 : TPTP v8.1.2. Released v6.1.0. % 0.07/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Aug 27 22:23:20 EDT 2023 % 0.12/0.33 % CPUTime : % 0.60/0.60 ________ _____ % 0.60/0.60 ___ __ \_________(_)________________________________ % 0.60/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.60/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.60/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.60/0.60 % 0.60/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.60/0.60 (2023-06-19) % 0.60/0.60 % 0.60/0.60 (c) Philipp Rümmer, 2009-2023 % 0.60/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.60/0.60 Amanda Stjerna. % 0.60/0.60 Free software under BSD-3-Clause. % 0.60/0.60 % 0.60/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.60/0.60 % 0.60/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.63/0.62 Running up to 7 provers in parallel. % 0.63/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.63/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.63/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.63/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.63/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.63/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.63/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.92/1.41 Prover 4: Preprocessing ... % 4.92/1.41 Prover 2: Preprocessing ... % 4.92/1.41 Prover 1: Preprocessing ... % 4.92/1.41 Prover 6: Preprocessing ... % 4.92/1.42 Prover 5: Preprocessing ... % 4.92/1.42 Prover 0: Preprocessing ... % 4.92/1.42 Prover 3: Preprocessing ... % 12.69/2.40 Prover 1: Warning: ignoring some quantifiers % 12.81/2.45 Prover 3: Warning: ignoring some quantifiers % 12.81/2.46 Prover 4: Warning: ignoring some quantifiers % 12.81/2.49 Prover 6: Proving ... % 12.81/2.51 Prover 3: Constructing countermodel ... % 13.58/2.52 Prover 5: Proving ... % 13.58/2.54 Prover 1: Constructing countermodel ... % 13.58/2.55 Prover 4: Constructing countermodel ... % 13.58/2.56 Prover 0: Proving ... % 14.80/2.73 Prover 2: Proving ... % 18.74/3.31 Prover 0: proved (2682ms) % 19.47/3.31 % 19.47/3.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.47/3.31 % 19.47/3.31 Prover 6: stopped % 19.47/3.32 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 19.47/3.32 Prover 2: stopped % 19.47/3.33 Prover 3: stopped % 19.47/3.34 Prover 5: stopped % 19.47/3.34 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 19.47/3.34 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 19.47/3.34 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 19.47/3.34 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 21.78/3.61 Prover 7: Preprocessing ... % 21.78/3.67 Prover 13: Preprocessing ... % 21.78/3.67 Prover 8: Preprocessing ... % 22.36/3.68 Prover 10: Preprocessing ... % 22.36/3.71 Prover 11: Preprocessing ... % 23.48/3.85 Prover 4: Found proof (size 240) % 23.48/3.85 Prover 4: proved (3225ms) % 23.48/3.85 Prover 1: stopped % 23.48/3.85 Prover 10: stopped % 23.48/3.87 Prover 11: stopped % 23.48/3.89 Prover 13: stopped % 24.09/3.97 Prover 8: Warning: ignoring some quantifiers % 24.50/3.98 Prover 7: Warning: ignoring some quantifiers % 24.50/3.99 Prover 8: Constructing countermodel ... % 24.50/4.00 Prover 8: stopped % 24.50/4.01 Prover 7: Constructing countermodel ... % 24.50/4.03 Prover 7: stopped % 24.50/4.03 % 24.50/4.03 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.50/4.03 % 24.50/4.07 % SZS output start Proof for theBenchmark % 24.89/4.07 Assumptions after simplification: % 24.89/4.07 --------------------------------- % 24.89/4.07 % 24.89/4.07 (bridgeR) % 24.89/4.09 ! [v0: uni] : ! [v1: int] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | t2tb(v1) = % 24.89/4.09 v0) % 24.89/4.09 % 24.89/4.09 (bridgeR1) % 24.89/4.09 ! [v0: uni] : ! [v1: array_int] : ( ~ (tb2t1(v0) = v1) | ~ uni(v0) | % 24.89/4.09 t2tb1(v1) = v0) % 24.89/4.09 % 24.89/4.09 (elts_def) % 24.89/4.09 ty(int) & ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 24.89/4.09 (mk_array(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ? [v4: ty] : ? [v5: % 24.89/4.09 any] : ? [v6: uni] : (elts(v0, v3) = v6 & map(int, v0) = v4 & sort(v4, % 24.89/4.09 v2) = v5 & ty(v4) & uni(v6) & ( ~ (v5 = 0) | v6 = v2))) % 24.89/4.09 % 24.89/4.09 (found_def) % 24.99/4.10 ty(int) & ! [v0: array_int] : ! [v1: int] : (v1 = 0 | ~ (found(v0) = v1) | % 24.99/4.10 ~ array_int(v0) | ? [v2: uni] : ? [v3: uni] : ? [v4: int] : ? [v5: int] % 24.99/4.10 : ? [v6: int] : ? [v7: uni] : ? [v8: int] : ? [v9: uni] : ? [v10: int] % 24.99/4.10 : ($lesseq(v6, usN) & $lesseq(f, v6) & $lesseq(v5, f) & $lesseq(1, v5) & % 24.99/4.10 t2tb1(v0) = v2 & tb2t(v9) = v10 & tb2t(v7) = v8 & tb2t(v3) = v4 & % 24.99/4.10 get1(int, v2, v6) = v9 & get1(int, v2, v5) = v7 & get1(int, v2, f) = v3 & % 24.99/4.10 uni(v9) & uni(v7) & uni(v3) & uni(v2) & ( ~ ($lesseq(v4, v10)) | ~ % 24.99/4.10 ($lesseq(v8, v4))))) & ! [v0: array_int] : ! [v1: uni] : ( ~ % 24.99/4.10 (t2tb1(v0) = v1) | ~ array_int(v0) | ? [v2: uni] : ? [v3: int] : ? [v4: % 24.99/4.10 any] : ? [v5: int] : ? [v6: int] : ? [v7: uni] : ? [v8: int] : ? [v9: % 24.99/4.10 uni] : ? [v10: int] : (found(v0) = v4 & tb2t(v2) = v3 & get1(int, v1, f) % 24.99/4.10 = v2 & uni(v2) & (v4 = 0 | ($lesseq(v6, usN) & $lesseq(f, v6) & % 24.99/4.10 $lesseq(v5, f) & $lesseq(1, v5) & tb2t(v9) = v10 & tb2t(v7) = v8 & % 24.99/4.10 get1(int, v1, v6) = v9 & get1(int, v1, v5) = v7 & uni(v9) & uni(v7) & % 24.99/4.10 ( ~ ($lesseq(v3, v10)) | ~ ($lesseq(v8, v3))))))) & ! [v0: % 24.99/4.10 array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ array_int(v0) | ? % 24.99/4.10 [v2: any] : ? [v3: uni] : ? [v4: int] : (found(v0) = v2 & tb2t(v3) = v4 & % 24.99/4.10 get1(int, v1, f) = v3 & uni(v3) & ( ~ (v2 = 0) | ( ! [v5: int] : ! [v6: % 24.99/4.10 int] : ! [v7: uni] : ! [v8: int] : ! [v9: uni] : ! [v10: int] : % 24.99/4.10 ( ~ ($lesseq(1, $difference(v4, v10))) | ~ ($lesseq(v6, usN)) | ~ % 24.99/4.10 ($lesseq(f, v6)) | ~ ($lesseq(v5, f)) | ~ ($lesseq(1, v5)) | ~ % 24.99/4.10 (tb2t(v9) = v10) | ~ (tb2t(v7) = v8) | ~ (get1(int, v1, v6) = v9) % 24.99/4.10 | ~ (get1(int, v1, v5) = v7)) & ! [v5: int] : ! [v6: int] : ! % 24.99/4.10 [v7: uni] : ! [v8: int] : ! [v9: uni] : ! [v10: int] : ( ~ % 24.99/4.10 ($lesseq(1, $difference(v8, v4))) | ~ ($lesseq(v6, usN)) | ~ % 24.99/4.10 ($lesseq(f, v6)) | ~ ($lesseq(v5, f)) | ~ ($lesseq(1, v5)) | ~ % 24.99/4.10 (tb2t(v9) = v10) | ~ (tb2t(v7) = v8) | ~ (get1(int, v1, v6) = v9) % 24.99/4.10 | ~ (get1(int, v1, v5) = v7)))))) & ! [v0: array_int] : ( ~ % 24.99/4.10 (found(v0) = 0) | ~ array_int(v0) | ? [v1: uni] : ? [v2: uni] : ? [v3: % 24.99/4.10 int] : (t2tb1(v0) = v1 & tb2t(v2) = v3 & get1(int, v1, f) = v2 & uni(v2) & % 24.99/4.10 uni(v1) & ! [v4: int] : ! [v5: int] : ! [v6: uni] : ! [v7: int] : ! % 24.99/4.10 [v8: uni] : ! [v9: int] : ( ~ ($lesseq(1, $difference(v3, v9))) | ~ % 24.99/4.10 ($lesseq(v5, usN)) | ~ ($lesseq(f, v5)) | ~ ($lesseq(v4, f)) | ~ % 24.99/4.10 ($lesseq(1, v4)) | ~ (tb2t(v8) = v9) | ~ (tb2t(v6) = v7) | ~ % 24.99/4.10 (get1(int, v1, v5) = v8) | ~ (get1(int, v1, v4) = v6)) & ! [v4: int] : % 24.99/4.10 ! [v5: int] : ! [v6: uni] : ! [v7: int] : ! [v8: uni] : ! [v9: int] : % 24.99/4.10 ( ~ ($lesseq(1, $difference(v7, v3))) | ~ ($lesseq(v5, usN)) | ~ % 24.99/4.10 ($lesseq(f, v5)) | ~ ($lesseq(v4, f)) | ~ ($lesseq(1, v4)) | ~ % 24.99/4.10 (tb2t(v8) = v9) | ~ (tb2t(v6) = v7) | ~ (get1(int, v1, v5) = v8) | ~ % 24.99/4.10 (get1(int, v1, v4) = v6)))) % 24.99/4.10 % 24.99/4.10 (get_def) % 24.99/4.10 ty(int) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: % 24.99/4.10 uni] : ! [v5: uni] : ( ~ (t2tb(v2) = v4) | ~ (elts(v0, v1) = v3) | ~ % 24.99/4.10 (get(v0, int, v3, v4) = v5) | ~ ty(v0) | ~ uni(v1) | (get1(v0, v1, v2) = % 24.99/4.10 v5 & uni(v5))) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] % 24.99/4.10 : ( ~ (get1(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v1) | ? [v4: uni] : ? % 24.99/4.10 [v5: uni] : (t2tb(v2) = v5 & elts(v0, v1) = v4 & get(v0, int, v4, v5) = v3 & % 24.99/4.10 uni(v5) & uni(v4) & uni(v3))) % 24.99/4.10 % 24.99/4.10 (i_invariant_def) % 24.99/4.11 ty(int) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 24.99/4.11 array_int] : ! [v5: int] : (v5 = 0 | ~ ($lesseq(v0, v2)) | ~ % 24.99/4.11 (i_invariant(v0, v1, v2, v3, v4) = v5) | ~ array_int(v4) | ? [v6: uni] : % 24.99/4.11 ? [v7: int] : ? [v8: uni] : ? [v9: int] : (t2tb1(v4) = v6 & uni(v6) & % 24.99/4.11 (($lesseq(1, $difference(v9, v3)) & $lesseq(1, $difference(v2, v7)) & % 24.99/4.11 $lesseq(1, v7) & tb2t(v8) = v9 & get1(int, v6, v7) = v8 & uni(v8)) | % 24.99/4.11 ($lesseq(v2, v1) & ! [v10: int] : ! [v11: uni] : ( ~ ($lesseq(v10, % 24.99/4.11 v1)) | ~ ($lesseq(v2, v10)) | ~ (get1(int, v6, v10) = v11) | % 24.99/4.11 ? [v12: int] : ($lesseq(1, $difference(v3, v12)) & tb2t(v11) = % 24.99/4.11 v12)))))) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: % 24.99/4.11 int] : ! [v4: array_int] : ( ~ ($lesseq(1, $difference(v0, v2))) | ~ % 24.99/4.11 (i_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4)) & ! [v0: int] : % 24.99/4.11 ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: array_int] : ( ~ % 24.99/4.11 (i_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4) | ? [v5: uni] : ? % 24.99/4.11 [v6: int] : ? [v7: uni] : ? [v8: int] : (t2tb1(v4) = v5 & uni(v5) & ! % 24.99/4.11 [v9: int] : ! [v10: uni] : ( ~ ($lesseq(1, $difference(v2, v9))) | ~ % 24.99/4.11 ($lesseq(1, v9)) | ~ (get1(int, v5, v9) = v10) | ? [v11: int] : % 24.99/4.11 ($lesseq(v11, v3) & tb2t(v10) = v11)) & ( ~ ($lesseq(v2, v1)) | % 24.99/4.11 ($lesseq(v3, v8) & $lesseq(v6, v1) & $lesseq(v2, v6) & tb2t(v7) = v8 & % 24.99/4.11 get1(int, v5, v6) = v7 & uni(v7))))) % 24.99/4.11 % 24.99/4.11 (j_invariant_def) % 24.99/4.11 ty(int) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 24.99/4.11 array_int] : ! [v5: int] : (v5 = 0 | ~ ($lesseq(v2, v1)) | ~ % 24.99/4.11 (j_invariant(v0, v1, v2, v3, v4) = v5) | ~ array_int(v4) | ? [v6: uni] : % 24.99/4.11 ? [v7: int] : ? [v8: uni] : ? [v9: int] : (t2tb1(v4) = v6 & uni(v6) & % 24.99/4.11 (($lesseq(1, $difference(v3, v9)) & $lesseq(v7, usN) & $lesseq(1, % 24.99/4.11 $difference(v7, v2)) & tb2t(v8) = v9 & get1(int, v6, v7) = v8 & % 24.99/4.11 uni(v8)) | ($lesseq(v0, v2) & ! [v10: int] : ! [v11: uni] : ( ~ % 24.99/4.11 ($lesseq(v10, v2)) | ~ ($lesseq(v0, v10)) | ~ (get1(int, v6, v10) % 24.99/4.11 = v11) | ? [v12: int] : ($lesseq(1, $difference(v12, v3)) & % 24.99/4.11 tb2t(v11) = v12)))))) & ! [v0: int] : ! [v1: int] : ! [v2: int] % 24.99/4.11 : ! [v3: int] : ! [v4: array_int] : ( ~ ($lesseq(1, $difference(v2, v1))) | % 24.99/4.11 ~ (j_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4)) & ! [v0: int] : % 24.99/4.11 ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: array_int] : ( ~ % 24.99/4.11 (j_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4) | ? [v5: uni] : ? % 24.99/4.11 [v6: int] : ? [v7: uni] : ? [v8: int] : (t2tb1(v4) = v5 & uni(v5) & ! % 24.99/4.11 [v9: int] : ! [v10: uni] : ( ~ ($lesseq(v9, usN)) | ~ ($lesseq(1, % 24.99/4.11 $difference(v9, v2))) | ~ (get1(int, v5, v9) = v10) | ? [v11: int] % 24.99/4.11 : ($lesseq(v3, v11) & tb2t(v10) = v11)) & ( ~ ($lesseq(v0, v2)) | % 24.99/4.11 ($lesseq(v8, v3) & $lesseq(v6, v2) & $lesseq(v0, v6) & tb2t(v7) = v8 & % 24.99/4.11 get1(int, v5, v6) = v7 & uni(v7))))) % 24.99/4.11 % 24.99/4.11 (m_invariant_def) % 24.99/4.11 ty(int) & ! [v0: int] : ! [v1: array_int] : ! [v2: int] : (v2 = 0 | ~ % 24.99/4.11 ($lesseq(v0, f)) | ~ (m_invariant(v0, v1) = v2) | ~ array_int(v1) | ? % 24.99/4.11 [v3: uni] : ? [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: int] : ? % 24.99/4.11 [v8: uni] : ? [v9: int] : ($lesseq(1, $difference(v9, v7)) & $lesseq(v5, % 24.99/4.11 usN) & $lesseq(v0, v5) & $lesseq(1, $difference(v0, v4)) & $lesseq(1, % 24.99/4.11 v4) & t2tb1(v1) = v3 & tb2t(v8) = v9 & tb2t(v6) = v7 & get1(int, v3, v5) % 24.99/4.11 = v6 & get1(int, v3, v4) = v8 & uni(v8) & uni(v6) & uni(v3))) & ! [v0: % 24.99/4.11 int] : ! [v1: array_int] : ( ~ ($lesseq(1, $difference(v0, f))) | ~ % 24.99/4.11 (m_invariant(v0, v1) = 0) | ~ array_int(v1)) & ! [v0: int] : ! [v1: % 24.99/4.11 array_int] : ( ~ (m_invariant(v0, v1) = 0) | ~ array_int(v1) | ? [v2: uni] % 24.99/4.11 : (t2tb1(v1) = v2 & uni(v2) & ! [v3: int] : ! [v4: int] : ! [v5: uni] : % 24.99/4.11 ! [v6: int] : ! [v7: uni] : ! [v8: int] : ( ~ ($lesseq(1, % 24.99/4.11 $difference(v8, v6))) | ~ ($lesseq(v4, usN)) | ~ ($lesseq(v0, v4)) % 24.99/4.11 | ~ ($lesseq(1, $difference(v0, v3))) | ~ ($lesseq(1, v3)) | ~ % 24.99/4.11 (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ (get1(int, v2, v4) = v5) | ~ % 24.99/4.11 (get1(int, v2, v3) = v7)))) % 24.99/4.11 % 24.99/4.11 (n_invariant_def) % 24.99/4.12 ty(int) & ! [v0: int] : ! [v1: array_int] : ! [v2: int] : (v2 = 0 | ~ % 24.99/4.12 ($lesseq(f, v0)) | ~ (n_invariant(v0, v1) = v2) | ~ array_int(v1) | ? % 24.99/4.12 [v3: uni] : ? [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: int] : ? % 24.99/4.12 [v8: uni] : ? [v9: int] : ($lesseq(1, $difference(v9, v7)) & $lesseq(v5, % 24.99/4.12 usN) & $lesseq(1, $difference(v5, v0)) & $lesseq(v4, v0) & $lesseq(1, % 24.99/4.12 v4) & t2tb1(v1) = v3 & tb2t(v8) = v9 & tb2t(v6) = v7 & get1(int, v3, v5) % 24.99/4.12 = v6 & get1(int, v3, v4) = v8 & uni(v8) & uni(v6) & uni(v3))) & ! [v0: % 24.99/4.12 int] : ! [v1: array_int] : ( ~ ($lesseq(1, $difference(f, v0))) | ~ % 24.99/4.12 (n_invariant(v0, v1) = 0) | ~ array_int(v1)) & ! [v0: int] : ! [v1: % 24.99/4.12 array_int] : ( ~ (n_invariant(v0, v1) = 0) | ~ array_int(v1) | ? [v2: uni] % 24.99/4.12 : (t2tb1(v1) = v2 & uni(v2) & ! [v3: int] : ! [v4: int] : ! [v5: uni] : % 24.99/4.12 ! [v6: int] : ! [v7: uni] : ! [v8: int] : ( ~ ($lesseq(1, % 24.99/4.12 $difference(v8, v6))) | ~ ($lesseq(v4, usN)) | ~ ($lesseq(1, % 24.99/4.12 $difference(v4, v0))) | ~ ($lesseq(v3, v0)) | ~ ($lesseq(1, v3)) | % 24.99/4.12 ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ (get1(int, v2, v4) = v5) | % 24.99/4.12 ~ (get1(int, v2, v3) = v7)))) % 24.99/4.12 % 24.99/4.12 (permut_all_def) % 25.13/4.12 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! % 25.13/4.12 [v5: uni] : ! [v6: any] : ( ~ (permut(v0, v4, v5, 0, v3) = v6) | ~ (elts(v0, % 25.13/4.12 v2) = v5) | ~ (elts(v0, v1) = v4) | ~ (length(v0, v1) = v3) | ~ % 25.13/4.12 ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v7: any] : ? [v8: int] : % 25.13/4.12 (permut_all(v0, v1, v2) = v7 & length(v0, v2) = v8 & ( ~ (v7 = 0) | (v8 = v3 % 25.13/4.12 & v6 = 0)))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 25.13/4.12 int] : ! [v4: uni] : ! [v5: uni] : ( ~ (permut(v0, v4, v5, 0, v3) = 0) | % 25.13/4.12 ~ (elts(v0, v2) = v5) | ~ (elts(v0, v1) = v4) | ~ (length(v0, v1) = v3) | % 25.13/4.12 ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v6: int] : ? [v7: any] : % 25.13/4.12 (permut_all(v0, v1, v2) = v7 & length(v0, v2) = v6 & ( ~ (v6 = v3) | v7 = % 25.13/4.12 0))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : (v3 = % 25.13/4.12 0 | ~ (permut_all(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | % 25.13/4.12 ? [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? [v8: any] : % 25.13/4.12 (permut(v0, v6, v7, 0, v4) = v8 & elts(v0, v2) = v7 & elts(v0, v1) = v6 & % 25.13/4.12 length(v0, v2) = v5 & length(v0, v1) = v4 & uni(v7) & uni(v6) & ( ~ (v8 = % 25.13/4.12 0) | ~ (v5 = v4)))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ % 25.13/4.12 (permut_all(v0, v1, v2) = 0) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v3: % 25.13/4.12 int] : ? [v4: uni] : ? [v5: uni] : (permut(v0, v4, v5, 0, v3) = 0 & % 25.13/4.12 elts(v0, v2) = v5 & elts(v0, v1) = v4 & length(v0, v2) = v3 & length(v0, % 25.13/4.12 v1) = v3 & uni(v5) & uni(v4))) % 25.13/4.12 % 25.13/4.12 (t2tb_sort2) % 25.13/4.12 ty(int) & ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : % 25.13/4.12 ! [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort(v0, v2) = 0)) % 25.13/4.12 % 25.13/4.12 (termination_def) % 25.13/4.13 ty(int) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.13/4.13 int] : ! [v5: array_int] : ! [v6: int] : (v6 = 0 | ~ ($lesseq(1, % 25.13/4.13 $difference(v3, v1))) | ~ ($lesseq(1, $difference(v0, v2))) | ~ % 25.13/4.13 (termination(v0, v1, v2, v3, v4, v5) = v6) | ~ array_int(v5)) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ! [v6: int] : (v6 = 0 | ~ ($lesseq(f, v1)) | ~ ($lesseq(v0, % 25.13/4.13 f)) | ~ (termination(v0, v1, v2, v3, v4, v5) = v6) | ~ array_int(v5) | % 25.13/4.13 ? [v7: uni] : ? [v8: uni] : ? [v9: int] : ( ~ (v9 = v4) & t2tb1(v5) = v7 % 25.13/4.13 & tb2t(v8) = v9 & get1(int, v7, f) = v8 & uni(v8) & uni(v7))) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v3, v1)) | ~ ($lesseq(1, $difference(f, v1))) | % 25.13/4.13 ~ (termination(v0, v1, v2, v3, v4, v5) = 0) | ~ array_int(v5)) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v3, v1)) | ~ ($lesseq(1, $difference(v0, f))) | % 25.13/4.13 ~ (termination(v0, v1, v2, v3, v4, v5) = 0) | ~ array_int(v5)) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v3, v1)) | ~ (termination(v0, v1, v2, v3, v4, v5) % 25.13/4.13 = 0) | ~ array_int(v5) | ? [v6: uni] : ? [v7: uni] : (t2tb1(v5) = v6 & % 25.13/4.13 tb2t(v7) = v4 & get1(int, v6, f) = v7 & uni(v7) & uni(v6))) & ! [v0: int] % 25.13/4.13 : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v0, v2)) | ~ ($lesseq(1, $difference(f, v1))) | % 25.13/4.13 ~ (termination(v0, v1, v2, v3, v4, v5) = 0) | ~ array_int(v5)) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v0, v2)) | ~ ($lesseq(1, $difference(v0, f))) | % 25.13/4.13 ~ (termination(v0, v1, v2, v3, v4, v5) = 0) | ~ array_int(v5)) & ! [v0: % 25.13/4.13 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 25.13/4.13 array_int] : ( ~ ($lesseq(v0, v2)) | ~ (termination(v0, v1, v2, v3, v4, v5) % 25.13/4.13 = 0) | ~ array_int(v5) | ? [v6: uni] : ? [v7: uni] : (t2tb1(v5) = v6 & % 25.13/4.13 tb2t(v7) = v4 & get1(int, v6, f) = v7 & uni(v7) & uni(v6))) % 25.13/4.13 % 25.13/4.13 (wP_parameter_find) % 25.13/4.13 ty(int) & ? [v0: uni] : ? [v1: map_int_int] : ? [v2: uni] : ? [v3: uni] : % 25.13/4.13 ? [v4: int] : ? [v5: int] : ? [v6: map_int_int] : ? [v7: uni] : ? [v8: % 25.13/4.13 uni] : ? [v9: array_int] : ? [v10: uni] : ? [v11: int] : ? [v12: int] : % 25.13/4.13 ? [v13: int] : ? [v14: map_int_int] : ? [v15: uni] : ? [v16: uni] : ? % 25.13/4.13 [v17: array_int] : ? [v18: int] : ? [v19: uni] : ? [v20: uni] : ? [v21: % 25.13/4.13 int] : ? [v22: int] : ? [v23: uni] : ? [v24: uni] : ? [v25: int] : ? % 25.13/4.13 [v26: int] : ( ~ (v26 = 0) & $lesseq(1, $difference(v25, v11)) & $lesseq(v22, % 25.13/4.13 v12) & $lesseq(v22, usN) & $lesseq(v5, v22) & $lesseq(0, v22) & % 25.13/4.13 $lesseq(v11, v21) & $lesseq(v18, v4) & $lesseq(v18, usN) & $lesseq(v13, v18) % 25.13/4.13 & $lesseq(0, v18) & $lesseq(v13, v12) & $lesseq(1, $difference(v4, v5)) & % 25.13/4.13 $lesseq(1, v5) & $lesseq(v4, usN) & $lesseq(f, usN) & $lesseq(0, f) & % 25.13/4.13 t2tb2(v14) = v15 & t2tb2(v6) = v7 & t2tb2(v1) = v2 & termination(v18, % 25.13/4.13 $sum(v22, -1), v5, v4, v11, v17) = v26 & termination(v18, v22, v5, v4, % 25.13/4.13 v11, v17) = 0 & termination(v18, v12, v5, v4, v11, v17) = 0 & % 25.13/4.13 termination(v13, v12, v5, v4, v11, v17) = 0 & j_invariant(v5, v4, v22, v11, % 25.13/4.13 v17) = 0 & j_invariant(v5, v4, v12, v11, v17) = 0 & i_invariant(v5, v4, % 25.13/4.13 v18, v11, v17) = 0 & i_invariant(v5, v4, v13, v11, v17) = 0 & % 25.13/4.13 n_invariant(v4, v17) = 0 & n_invariant(v4, v9) = 0 & m_invariant(v5, v17) = % 25.13/4.13 0 & m_invariant(v5, v9) = 0 & tb2t1(v16) = v17 & tb2t1(v8) = v9 & % 25.13/4.13 permut_all(int, v16, v3) = 0 & permut_all(int, v8, v3) = 0 & tb2t(v24) = v25 % 25.13/4.13 & tb2t(v20) = v21 & tb2t(v10) = v11 & t2tb(v22) = v23 & t2tb(v18) = v19 & % 25.13/4.13 t2tb(f) = v0 & mk_array(int, $sum(usN, 1), v15) = v16 & mk_array(int, % 25.13/4.13 $sum(usN, 1), v7) = v8 & mk_array(int, $sum(usN, 1), v2) = v3 & get(int, % 25.13/4.13 int, v15, v23) = v24 & get(int, int, v15, v19) = v20 & get(int, int, v7, % 25.13/4.13 v0) = v10 & map_int_int(v14) & map_int_int(v6) & map_int_int(v1) & % 25.13/4.13 array_int(v17) & array_int(v9) & uni(v24) & uni(v23) & uni(v20) & uni(v19) & % 25.13/4.13 uni(v16) & uni(v15) & uni(v10) & uni(v8) & uni(v7) & uni(v3) & uni(v2) & % 25.13/4.13 uni(v0)) % 25.13/4.13 % 25.13/4.13 (function-axioms) % 25.20/4.14 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 25.20/4.14 [v3: int] : ! [v4: int] : ! [v5: int] : ! [v6: uni] : ! [v7: uni] : ! % 25.20/4.14 [v8: ty] : (v1 = v0 | ~ (exchange(v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 25.20/4.14 (exchange(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 25.20/4.14 ! [v1: MultipleValueBool] : ! [v2: array_int] : ! [v3: int] : ! [v4: int] : % 25.20/4.14 ! [v5: int] : ! [v6: int] : ! [v7: int] : (v1 = v0 | ~ (termination(v7, % 25.20/4.14 v6, v5, v4, v3, v2) = v1) | ~ (termination(v7, v6, v5, v4, v3, v2) = % 25.20/4.14 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 25.20/4.14 array_int] : ! [v3: int] : ! [v4: int] : ! [v5: int] : ! [v6: int] : (v1 % 25.20/4.14 = v0 | ~ (j_invariant(v6, v5, v4, v3, v2) = v1) | ~ (j_invariant(v6, v5, % 25.20/4.14 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 25.20/4.14 MultipleValueBool] : ! [v2: array_int] : ! [v3: int] : ! [v4: int] : ! % 25.20/4.14 [v5: int] : ! [v6: int] : (v1 = v0 | ~ (i_invariant(v6, v5, v4, v3, v2) = % 25.20/4.14 v1) | ~ (i_invariant(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 25.20/4.14 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 25.20/4.14 int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = v0 | ~ % 25.20/4.14 (permut_sub(v6, v5, v4, v3, v2) = v1) | ~ (permut_sub(v6, v5, v4, v3, v2) = % 25.20/4.14 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 25.20/4.14 int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = v0 | % 25.20/4.14 ~ (permut1(v6, v5, v4, v3, v2) = v1) | ~ (permut1(v6, v5, v4, v3, v2) = % 25.20/4.14 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 25.20/4.14 int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = v0 | % 25.20/4.14 ~ (exchange1(v6, v5, v4, v3, v2) = v1) | ~ (exchange1(v6, v5, v4, v3, v2) % 25.20/4.14 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 25.20/4.14 int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = v0 | % 25.20/4.14 ~ (array_eq_sub(v6, v5, v4, v3, v2) = v1) | ~ (array_eq_sub(v6, v5, v4, % 25.20/4.14 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 25.20/4.14 : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : % 25.20/4.14 (v1 = v0 | ~ (map_eq_sub(v6, v5, v4, v3, v2) = v1) | ~ (map_eq_sub(v6, v5, % 25.20/4.14 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 25.20/4.14 MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! [v5: % 25.20/4.14 uni] : ! [v6: ty] : (v1 = v0 | ~ (permut(v6, v5, v4, v3, v2) = v1) | ~ % 25.20/4.14 (permut(v6, v5, v4, v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 25.20/4.14 int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = v0 | % 25.20/4.14 ~ (occ(v6, v5, v4, v3, v2) = v1) | ~ (occ(v6, v5, v4, v3, v2) = v0)) & ! % 25.20/4.14 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 25.20/4.14 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 25.20/4.14 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 25.20/4.14 : ! [v3: int] : ! [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ (set1(v5, v4, v3, % 25.20/4.14 v2) = v1) | ~ (set1(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 25.20/4.14 uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | % 25.20/4.14 ~ (get(v5, v4, v3, v2) = v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] % 25.20/4.14 : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: bool] : ! [v5: ty] : % 25.20/4.14 (v1 = v0 | ~ (match_bool(v5, v4, v3, v2) = v1) | ~ (match_bool(v5, v4, v3, % 25.20/4.14 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 25.20/4.14 ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (permut_all(v4, v3, % 25.20/4.14 v2) = v1) | ~ (permut_all(v4, v3, v2) = v0)) & ! [v0: % 25.20/4.15 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: % 25.20/4.15 uni] : ! [v4: ty] : (v1 = v0 | ~ (array_eq(v4, v3, v2) = v1) | ~ % 25.20/4.15 (array_eq(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 25.20/4.15 ! [v3: int] : ! [v4: ty] : (v1 = v0 | ~ (make(v4, v3, v2) = v1) | ~ % 25.20/4.15 (make(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! % 25.20/4.15 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (get1(v4, v3, v2) = v1) | ~ (get1(v4, % 25.20/4.15 v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 25.20/4.15 int] : ! [v4: ty] : (v1 = v0 | ~ (mk_array(v4, v3, v2) = v1) | ~ % 25.20/4.15 (mk_array(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 25.20/4.15 ! [v3: ty] : ! [v4: ty] : (v1 = v0 | ~ (const(v4, v3, v2) = v1) | ~ % 25.20/4.15 (const(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 25.20/4.15 MultipleValueBool] : ! [v2: array_int] : ! [v3: int] : (v1 = v0 | ~ % 25.20/4.15 (n_invariant(v3, v2) = v1) | ~ (n_invariant(v3, v2) = v0)) & ! [v0: % 25.20/4.15 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: array_int] : ! % 25.20/4.15 [v3: int] : (v1 = v0 | ~ (m_invariant(v3, v2) = v1) | ~ (m_invariant(v3, v2) % 25.20/4.15 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = % 25.20/4.15 v0 | ~ (elts(v3, v2) = v1) | ~ (elts(v3, v2) = v0)) & ! [v0: int] : ! % 25.20/4.15 [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (length(v3, v2) = v1) | % 25.20/4.15 ~ (length(v3, v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! % 25.20/4.15 [v3: ty] : (v1 = v0 | ~ (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: % 25.20/4.15 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 25.20/4.15 (contents(v3, v2) = v1) | ~ (contents(v3, v2) = v0)) & ! [v0: uni] : ! % 25.20/4.15 [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) | % 25.20/4.15 ~ (mk_ref(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 25.20/4.15 MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (sort(v3, % 25.20/4.15 v2) = v1) | ~ (sort(v3, v2) = v0)) & ! [v0: map_int_int] : ! [v1: % 25.20/4.15 map_int_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | ~ (tb2t2(v2) % 25.20/4.15 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: map_int_int] : (v1 = v0 | % 25.20/4.15 ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 25.20/4.15 [v1: MultipleValueBool] : ! [v2: array_int] : (v1 = v0 | ~ (found(v2) = v1) % 25.20/4.15 | ~ (found(v2) = v0)) & ! [v0: array_int] : ! [v1: array_int] : ! [v2: % 25.20/4.15 uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ (tb2t1(v2) = v0)) & ! [v0: uni] % 25.20/4.15 : ! [v1: uni] : ! [v2: array_int] : (v1 = v0 | ~ (t2tb1(v2) = v1) | ~ % 25.20/4.15 (t2tb1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | % 25.20/4.15 ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 25.20/4.15 [v2: int] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: ty] % 25.20/4.15 : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (array(v2) = v1) | ~ (array(v2) = % 25.20/4.15 v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (ref(v2) = % 25.20/4.15 v1) | ~ (ref(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 % 25.20/4.15 = v0 | ~ (witness(v2) = v1) | ~ (witness(v2) = v0)) % 25.20/4.15 % 25.20/4.15 Further assumptions not needed in the proof: % 25.20/4.15 -------------------------------------------- % 25.20/4.15 array_eq_def, array_eq_sub_def, array_inversion, bool_inversion, bridgeL, % 25.20/4.15 bridgeL1, bridgeL2, bridgeR2, compatOrderMult, const1, const_sort, contents_def, % 25.20/4.15 contents_sort, elts_sort, exchange_def, exchange_def1, exchange_permut_all, % 25.20/4.15 exchange_permut_sub, exchange_set, f_N_range, get_sort, get_sort1, length_def, % 25.20/4.15 make_def, make_sort, map_eq_sub_def, match_bool_False, match_bool_True, % 25.20/4.15 match_bool_sort, mk_array_sort, mk_ref_sort, occ_append, occ_bounds, occ_empty, % 25.20/4.15 occ_eq, occ_exists, occ_neq, occ_pos, occ_right_add, occ_right_no_add, % 25.20/4.15 permut_def, permut_def1, permut_exists, permut_sub_def, permut_sub_weakening, % 25.20/4.15 permut_trans, ref_inversion, select_eq, select_neq, set_def, set_sort, % 25.20/4.15 set_sort1, t2tb_sort, t2tb_sort1, true_False, tuple0_inversion, witness_sort % 25.20/4.15 % 25.20/4.15 Those formulas are unsatisfiable: % 25.20/4.15 --------------------------------- % 25.20/4.15 % 25.20/4.15 Begin of proof % 25.20/4.15 | % 25.20/4.15 | ALPHA: (elts_def) implies: % 25.20/4.15 | (1) ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 25.20/4.15 | (mk_array(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ? [v4: ty] : % 25.20/4.15 | ? [v5: any] : ? [v6: uni] : (elts(v0, v3) = v6 & map(int, v0) = v4 & % 25.20/4.15 | sort(v4, v2) = v5 & ty(v4) & uni(v6) & ( ~ (v5 = 0) | v6 = v2))) % 25.20/4.15 | % 25.20/4.15 | ALPHA: (get_def) implies: % 25.20/4.15 | (2) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: uni] % 25.20/4.15 | : ! [v5: uni] : ( ~ (t2tb(v2) = v4) | ~ (elts(v0, v1) = v3) | ~ % 25.20/4.15 | (get(v0, int, v3, v4) = v5) | ~ ty(v0) | ~ uni(v1) | (get1(v0, v1, % 25.20/4.15 | v2) = v5 & uni(v5))) % 25.20/4.15 | % 25.20/4.15 | ALPHA: (permut_all_def) implies: % 25.20/4.15 | (3) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (permut_all(v0, v1, v2) % 25.20/4.15 | = 0) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v3: int] : ? [v4: % 25.20/4.15 | uni] : ? [v5: uni] : (permut(v0, v4, v5, 0, v3) = 0 & elts(v0, v2) % 25.20/4.15 | = v5 & elts(v0, v1) = v4 & length(v0, v2) = v3 & length(v0, v1) = % 25.20/4.15 | v3 & uni(v5) & uni(v4))) % 25.20/4.15 | % 25.20/4.15 | ALPHA: (found_def) implies: % 25.20/4.16 | (4) ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 25.20/4.16 | array_int(v0) | ? [v2: any] : ? [v3: uni] : ? [v4: int] : % 25.20/4.16 | (found(v0) = v2 & tb2t(v3) = v4 & get1(int, v1, f) = v3 & uni(v3) & ( % 25.20/4.16 | ~ (v2 = 0) | ( ! [v5: int] : ! [v6: int] : ! [v7: uni] : ! % 25.20/4.16 | [v8: int] : ! [v9: uni] : ! [v10: int] : ( ~ ($lesseq(1, % 25.20/4.16 | $difference(v4, v10))) | ~ ($lesseq(v6, usN)) | ~ % 25.20/4.16 | ($lesseq(f, v6)) | ~ ($lesseq(v5, f)) | ~ ($lesseq(1, v5)) % 25.20/4.16 | | ~ (tb2t(v9) = v10) | ~ (tb2t(v7) = v8) | ~ (get1(int, % 25.20/4.16 | v1, v6) = v9) | ~ (get1(int, v1, v5) = v7)) & ! [v5: % 25.20/4.16 | int] : ! [v6: int] : ! [v7: uni] : ! [v8: int] : ! [v9: % 25.20/4.16 | uni] : ! [v10: int] : ( ~ ($lesseq(1, $difference(v8, v4))) % 25.20/4.16 | | ~ ($lesseq(v6, usN)) | ~ ($lesseq(f, v6)) | ~ % 25.20/4.16 | ($lesseq(v5, f)) | ~ ($lesseq(1, v5)) | ~ (tb2t(v9) = v10) % 25.20/4.16 | | ~ (tb2t(v7) = v8) | ~ (get1(int, v1, v6) = v9) | ~ % 25.20/4.16 | (get1(int, v1, v5) = v7)))))) % 25.20/4.16 | (5) ! [v0: array_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 25.20/4.16 | array_int(v0) | ? [v2: uni] : ? [v3: int] : ? [v4: any] : ? [v5: % 25.20/4.16 | int] : ? [v6: int] : ? [v7: uni] : ? [v8: int] : ? [v9: uni] : % 25.20/4.16 | ? [v10: int] : (found(v0) = v4 & tb2t(v2) = v3 & get1(int, v1, f) = % 25.20/4.16 | v2 & uni(v2) & (v4 = 0 | ($lesseq(v6, usN) & $lesseq(f, v6) & % 25.20/4.16 | $lesseq(v5, f) & $lesseq(1, v5) & tb2t(v9) = v10 & tb2t(v7) = % 25.20/4.16 | v8 & get1(int, v1, v6) = v9 & get1(int, v1, v5) = v7 & uni(v9) % 25.20/4.16 | & uni(v7) & ( ~ ($lesseq(v3, v10)) | ~ ($lesseq(v8, v3))))))) % 25.20/4.16 | % 25.20/4.16 | ALPHA: (m_invariant_def) implies: % 25.20/4.16 | (6) ! [v0: int] : ! [v1: array_int] : ( ~ (m_invariant(v0, v1) = 0) | ~ % 25.20/4.16 | array_int(v1) | ? [v2: uni] : (t2tb1(v1) = v2 & uni(v2) & ! [v3: % 25.20/4.16 | int] : ! [v4: int] : ! [v5: uni] : ! [v6: int] : ! [v7: uni] % 25.20/4.16 | : ! [v8: int] : ( ~ ($lesseq(1, $difference(v8, v6))) | ~ % 25.20/4.16 | ($lesseq(v4, usN)) | ~ ($lesseq(v0, v4)) | ~ ($lesseq(1, % 25.20/4.16 | $difference(v0, v3))) | ~ ($lesseq(1, v3)) | ~ (tb2t(v7) = % 25.20/4.16 | v8) | ~ (tb2t(v5) = v6) | ~ (get1(int, v2, v4) = v5) | ~ % 25.20/4.16 | (get1(int, v2, v3) = v7)))) % 25.20/4.16 | (7) ! [v0: int] : ! [v1: array_int] : ( ~ ($lesseq(1, $difference(v0, % 25.20/4.16 | f))) | ~ (m_invariant(v0, v1) = 0) | ~ array_int(v1)) % 25.20/4.16 | % 25.20/4.16 | ALPHA: (n_invariant_def) implies: % 25.20/4.16 | (8) ! [v0: int] : ! [v1: array_int] : ( ~ (n_invariant(v0, v1) = 0) | ~ % 25.20/4.16 | array_int(v1) | ? [v2: uni] : (t2tb1(v1) = v2 & uni(v2) & ! [v3: % 25.20/4.16 | int] : ! [v4: int] : ! [v5: uni] : ! [v6: int] : ! [v7: uni] % 25.20/4.16 | : ! [v8: int] : ( ~ ($lesseq(1, $difference(v8, v6))) | ~ % 25.20/4.16 | ($lesseq(v4, usN)) | ~ ($lesseq(1, $difference(v4, v0))) | ~ % 25.20/4.16 | ($lesseq(v3, v0)) | ~ ($lesseq(1, v3)) | ~ (tb2t(v7) = v8) | ~ % 25.20/4.16 | (tb2t(v5) = v6) | ~ (get1(int, v2, v4) = v5) | ~ (get1(int, v2, % 25.20/4.16 | v3) = v7)))) % 25.20/4.16 | % 25.20/4.16 | ALPHA: (i_invariant_def) implies: % 25.20/4.16 | (9) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.16 | array_int] : ( ~ (i_invariant(v0, v1, v2, v3, v4) = 0) | ~ % 25.20/4.16 | array_int(v4) | ? [v5: uni] : ? [v6: int] : ? [v7: uni] : ? [v8: % 25.20/4.16 | int] : (t2tb1(v4) = v5 & uni(v5) & ! [v9: int] : ! [v10: uni] : ( % 25.20/4.16 | ~ ($lesseq(1, $difference(v2, v9))) | ~ ($lesseq(1, v9)) | ~ % 25.20/4.16 | (get1(int, v5, v9) = v10) | ? [v11: int] : ($lesseq(v11, v3) & % 25.20/4.16 | tb2t(v10) = v11)) & ( ~ ($lesseq(v2, v1)) | ($lesseq(v3, v8) & % 25.20/4.16 | $lesseq(v6, v1) & $lesseq(v2, v6) & tb2t(v7) = v8 & get1(int, % 25.20/4.16 | v5, v6) = v7 & uni(v7))))) % 25.20/4.16 | (10) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.16 | array_int] : ( ~ ($lesseq(1, $difference(v0, v2))) | ~ % 25.20/4.16 | (i_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4)) % 25.20/4.16 | % 25.20/4.16 | ALPHA: (j_invariant_def) implies: % 25.20/4.16 | (11) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.16 | array_int] : ( ~ (j_invariant(v0, v1, v2, v3, v4) = 0) | ~ % 25.20/4.16 | array_int(v4) | ? [v5: uni] : ? [v6: int] : ? [v7: uni] : ? [v8: % 25.20/4.16 | int] : (t2tb1(v4) = v5 & uni(v5) & ! [v9: int] : ! [v10: uni] : % 25.20/4.16 | ( ~ ($lesseq(v9, usN)) | ~ ($lesseq(1, $difference(v9, v2))) | ~ % 25.20/4.16 | (get1(int, v5, v9) = v10) | ? [v11: int] : ($lesseq(v3, v11) & % 25.20/4.16 | tb2t(v10) = v11)) & ( ~ ($lesseq(v0, v2)) | ($lesseq(v8, v3) & % 25.20/4.16 | $lesseq(v6, v2) & $lesseq(v0, v6) & tb2t(v7) = v8 & get1(int, % 25.20/4.16 | v5, v6) = v7 & uni(v7))))) % 25.20/4.16 | (12) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.16 | array_int] : ( ~ ($lesseq(1, $difference(v2, v1))) | ~ % 25.20/4.16 | (j_invariant(v0, v1, v2, v3, v4) = 0) | ~ array_int(v4)) % 25.20/4.16 | % 25.20/4.16 | ALPHA: (termination_def) implies: % 25.20/4.17 | (13) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.17 | int] : ! [v5: array_int] : ( ~ ($lesseq(v0, v2)) | ~ % 25.20/4.17 | (termination(v0, v1, v2, v3, v4, v5) = 0) | ~ array_int(v5) | ? % 25.20/4.17 | [v6: uni] : ? [v7: uni] : (t2tb1(v5) = v6 & tb2t(v7) = v4 & % 25.20/4.17 | get1(int, v6, f) = v7 & uni(v7) & uni(v6))) % 25.20/4.17 | (14) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.17 | int] : ! [v5: array_int] : ( ~ ($lesseq(v0, v2)) | ~ ($lesseq(1, % 25.20/4.17 | $difference(f, v1))) | ~ (termination(v0, v1, v2, v3, v4, v5) = % 25.20/4.17 | 0) | ~ array_int(v5)) % 25.20/4.17 | (15) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.17 | int] : ! [v5: array_int] : ! [v6: int] : (v6 = 0 | ~ ($lesseq(f, % 25.20/4.17 | v1)) | ~ ($lesseq(v0, f)) | ~ (termination(v0, v1, v2, v3, v4, % 25.20/4.17 | v5) = v6) | ~ array_int(v5) | ? [v7: uni] : ? [v8: uni] : ? % 25.20/4.17 | [v9: int] : ( ~ (v9 = v4) & t2tb1(v5) = v7 & tb2t(v8) = v9 & % 25.20/4.17 | get1(int, v7, f) = v8 & uni(v8) & uni(v7))) % 25.20/4.17 | (16) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 25.20/4.17 | int] : ! [v5: array_int] : ! [v6: int] : (v6 = 0 | ~ ($lesseq(1, % 25.20/4.17 | $difference(v3, v1))) | ~ ($lesseq(1, $difference(v0, v2))) | % 25.20/4.17 | ~ (termination(v0, v1, v2, v3, v4, v5) = v6) | ~ array_int(v5)) % 25.20/4.17 | % 25.20/4.17 | ALPHA: (t2tb_sort2) implies: % 25.20/4.17 | (17) ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : ! % 25.20/4.17 | [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort(v0, v2) % 25.20/4.17 | = 0)) % 25.20/4.17 | % 25.20/4.17 | ALPHA: (wP_parameter_find) implies: % 25.20/4.17 | (18) ty(int) % 25.20/4.17 | (19) ? [v0: uni] : ? [v1: map_int_int] : ? [v2: uni] : ? [v3: uni] : ? % 25.20/4.17 | [v4: int] : ? [v5: int] : ? [v6: map_int_int] : ? [v7: uni] : ? % 25.20/4.17 | [v8: uni] : ? [v9: array_int] : ? [v10: uni] : ? [v11: int] : ? % 25.20/4.17 | [v12: int] : ? [v13: int] : ? [v14: map_int_int] : ? [v15: uni] : % 25.20/4.17 | ? [v16: uni] : ? [v17: array_int] : ? [v18: int] : ? [v19: uni] : % 25.20/4.17 | ? [v20: uni] : ? [v21: int] : ? [v22: int] : ? [v23: uni] : ? % 25.20/4.17 | [v24: uni] : ? [v25: int] : ? [v26: int] : ( ~ (v26 = 0) & % 25.20/4.17 | $lesseq(1, $difference(v25, v11)) & $lesseq(v22, v12) & $lesseq(v22, % 25.20/4.17 | usN) & $lesseq(v5, v22) & $lesseq(0, v22) & $lesseq(v11, v21) & % 25.20/4.17 | $lesseq(v18, v4) & $lesseq(v18, usN) & $lesseq(v13, v18) & % 25.20/4.17 | $lesseq(0, v18) & $lesseq(v13, v12) & $lesseq(1, $difference(v4, % 25.20/4.17 | v5)) & $lesseq(1, v5) & $lesseq(v4, usN) & $lesseq(f, usN) & % 25.20/4.17 | $lesseq(0, f) & t2tb2(v14) = v15 & t2tb2(v6) = v7 & t2tb2(v1) = v2 & % 25.20/4.17 | termination(v18, $sum(v22, -1), v5, v4, v11, v17) = v26 & % 25.20/4.17 | termination(v18, v22, v5, v4, v11, v17) = 0 & termination(v18, v12, % 25.20/4.17 | v5, v4, v11, v17) = 0 & termination(v13, v12, v5, v4, v11, v17) = % 25.20/4.17 | 0 & j_invariant(v5, v4, v22, v11, v17) = 0 & j_invariant(v5, v4, % 25.20/4.17 | v12, v11, v17) = 0 & i_invariant(v5, v4, v18, v11, v17) = 0 & % 25.20/4.17 | i_invariant(v5, v4, v13, v11, v17) = 0 & n_invariant(v4, v17) = 0 & % 25.20/4.17 | n_invariant(v4, v9) = 0 & m_invariant(v5, v17) = 0 & m_invariant(v5, % 25.20/4.17 | v9) = 0 & tb2t1(v16) = v17 & tb2t1(v8) = v9 & permut_all(int, v16, % 25.20/4.17 | v3) = 0 & permut_all(int, v8, v3) = 0 & tb2t(v24) = v25 & % 25.20/4.17 | tb2t(v20) = v21 & tb2t(v10) = v11 & t2tb(v22) = v23 & t2tb(v18) = % 25.20/4.17 | v19 & t2tb(f) = v0 & mk_array(int, $sum(usN, 1), v15) = v16 & % 25.20/4.17 | mk_array(int, $sum(usN, 1), v7) = v8 & mk_array(int, $sum(usN, 1), % 25.20/4.17 | v2) = v3 & get(int, int, v15, v23) = v24 & get(int, int, v15, v19) % 25.20/4.17 | = v20 & get(int, int, v7, v0) = v10 & map_int_int(v14) & % 25.20/4.17 | map_int_int(v6) & map_int_int(v1) & array_int(v17) & array_int(v9) & % 25.20/4.17 | uni(v24) & uni(v23) & uni(v20) & uni(v19) & uni(v16) & uni(v15) & % 25.20/4.17 | uni(v10) & uni(v8) & uni(v7) & uni(v3) & uni(v2) & uni(v0)) % 25.20/4.17 | % 25.20/4.17 | ALPHA: (function-axioms) implies: % 25.20/4.17 | (20) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb(v2) = % 25.20/4.17 | v1) | ~ (t2tb(v2) = v0)) % 25.20/4.17 | (21) ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = % 25.20/4.17 | v1) | ~ (tb2t(v2) = v0)) % 25.20/4.17 | (22) ! [v0: uni] : ! [v1: uni] : ! [v2: array_int] : (v1 = v0 | ~ % 25.20/4.17 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 25.20/4.17 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 25.20/4.17 | : ! [v3: ty] : (v1 = v0 | ~ (sort(v3, v2) = v1) | ~ (sort(v3, v2) = % 25.20/4.17 | v0)) % 25.20/4.17 | (24) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ % 25.20/4.17 | (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) % 25.20/4.17 | (25) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 25.20/4.17 | ~ (elts(v3, v2) = v1) | ~ (elts(v3, v2) = v0)) % 25.20/4.17 | (26) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: % 25.20/4.17 | ty] : (v1 = v0 | ~ (get1(v4, v3, v2) = v1) | ~ (get1(v4, v3, v2) = % 25.20/4.17 | v0)) % 25.20/4.17 | % 25.20/4.17 | DELTA: instantiating (17) with fresh symbol all_84_0 gives: % 25.20/4.18 | (27) map(int, int) = all_84_0 & ty(all_84_0) & ! [v0: map_int_int] : ! % 25.20/4.18 | [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ map_int_int(v0) | sort(all_84_0, % 25.20/4.18 | v1) = 0) % 25.20/4.18 | % 25.20/4.18 | ALPHA: (27) implies: % 25.20/4.18 | (28) map(int, int) = all_84_0 % 25.20/4.18 | (29) ! [v0: map_int_int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ % 25.20/4.18 | map_int_int(v0) | sort(all_84_0, v1) = 0) % 25.20/4.18 | % 25.20/4.18 | DELTA: instantiating (19) with fresh symbols all_88_0, all_88_1, all_88_2, % 25.20/4.18 | all_88_3, all_88_4, all_88_5, all_88_6, all_88_7, all_88_8, all_88_9, % 25.20/4.18 | all_88_10, all_88_11, all_88_12, all_88_13, all_88_14, all_88_15, % 25.20/4.18 | all_88_16, all_88_17, all_88_18, all_88_19, all_88_20, all_88_21, % 25.20/4.18 | all_88_22, all_88_23, all_88_24, all_88_25, all_88_26 gives: % 25.20/4.18 | (30) ~ (all_88_0 = 0) & $lesseq(1, $difference(all_88_1, all_88_15)) & % 25.20/4.18 | $lesseq(all_88_4, all_88_14) & $lesseq(all_88_4, usN) & % 25.20/4.18 | $lesseq(all_88_21, all_88_4) & $lesseq(0, all_88_4) & % 25.20/4.18 | $lesseq(all_88_15, all_88_5) & $lesseq(all_88_8, all_88_22) & % 25.20/4.18 | $lesseq(all_88_8, usN) & $lesseq(all_88_13, all_88_8) & $lesseq(0, % 25.20/4.18 | all_88_8) & $lesseq(all_88_13, all_88_14) & $lesseq(1, % 25.20/4.18 | $difference(all_88_22, all_88_21)) & $lesseq(1, all_88_21) & % 25.20/4.18 | $lesseq(all_88_22, usN) & $lesseq(f, usN) & $lesseq(0, f) & % 25.20/4.18 | t2tb2(all_88_12) = all_88_11 & t2tb2(all_88_20) = all_88_19 & % 25.20/4.18 | t2tb2(all_88_25) = all_88_24 & termination(all_88_8, $sum(all_88_4, % 25.20/4.18 | -1), all_88_21, all_88_22, all_88_15, all_88_9) = all_88_0 & % 25.20/4.18 | termination(all_88_8, all_88_4, all_88_21, all_88_22, all_88_15, % 25.20/4.18 | all_88_9) = 0 & termination(all_88_8, all_88_14, all_88_21, % 25.20/4.18 | all_88_22, all_88_15, all_88_9) = 0 & termination(all_88_13, % 25.20/4.18 | all_88_14, all_88_21, all_88_22, all_88_15, all_88_9) = 0 & % 25.20/4.18 | j_invariant(all_88_21, all_88_22, all_88_4, all_88_15, all_88_9) = 0 & % 25.20/4.18 | j_invariant(all_88_21, all_88_22, all_88_14, all_88_15, all_88_9) = 0 % 25.20/4.18 | & i_invariant(all_88_21, all_88_22, all_88_8, all_88_15, all_88_9) = 0 % 25.20/4.18 | & i_invariant(all_88_21, all_88_22, all_88_13, all_88_15, all_88_9) = % 25.20/4.18 | 0 & n_invariant(all_88_22, all_88_9) = 0 & n_invariant(all_88_22, % 25.20/4.18 | all_88_17) = 0 & m_invariant(all_88_21, all_88_9) = 0 & % 25.20/4.18 | m_invariant(all_88_21, all_88_17) = 0 & tb2t1(all_88_10) = all_88_9 & % 25.20/4.18 | tb2t1(all_88_18) = all_88_17 & permut_all(int, all_88_10, all_88_23) = % 25.20/4.18 | 0 & permut_all(int, all_88_18, all_88_23) = 0 & tb2t(all_88_2) = % 25.20/4.18 | all_88_1 & tb2t(all_88_6) = all_88_5 & tb2t(all_88_16) = all_88_15 & % 25.20/4.18 | t2tb(all_88_4) = all_88_3 & t2tb(all_88_8) = all_88_7 & t2tb(f) = % 25.20/4.18 | all_88_26 & mk_array(int, $sum(usN, 1), all_88_11) = all_88_10 & % 25.20/4.18 | mk_array(int, $sum(usN, 1), all_88_19) = all_88_18 & mk_array(int, % 25.20/4.18 | $sum(usN, 1), all_88_24) = all_88_23 & get(int, int, all_88_11, % 25.20/4.18 | all_88_3) = all_88_2 & get(int, int, all_88_11, all_88_7) = all_88_6 % 25.20/4.18 | & get(int, int, all_88_19, all_88_26) = all_88_16 & % 25.20/4.18 | map_int_int(all_88_12) & map_int_int(all_88_20) & % 25.20/4.18 | map_int_int(all_88_25) & array_int(all_88_9) & array_int(all_88_17) & % 25.20/4.18 | uni(all_88_2) & uni(all_88_3) & uni(all_88_6) & uni(all_88_7) & % 25.20/4.18 | uni(all_88_10) & uni(all_88_11) & uni(all_88_16) & uni(all_88_18) & % 25.20/4.18 | uni(all_88_19) & uni(all_88_23) & uni(all_88_24) & uni(all_88_26) % 25.20/4.18 | % 25.20/4.18 | ALPHA: (30) implies: % 25.20/4.18 | (31) ~ (all_88_0 = 0) % 25.20/4.18 | (32) $lesseq(all_88_13, all_88_8) % 25.20/4.18 | (33) $lesseq(1, $difference(all_88_1, all_88_15)) % 25.20/4.18 | (34) uni(all_88_24) % 25.20/4.18 | (35) uni(all_88_23) % 25.20/4.18 | (36) uni(all_88_19) % 25.20/4.18 | (37) uni(all_88_18) % 25.20/4.18 | (38) uni(all_88_16) % 25.20/4.18 | (39) uni(all_88_11) % 25.20/4.18 | (40) uni(all_88_10) % 25.20/4.18 | (41) array_int(all_88_17) % 25.20/4.18 | (42) array_int(all_88_9) % 25.20/4.18 | (43) map_int_int(all_88_20) % 25.20/4.18 | (44) map_int_int(all_88_12) % 25.20/4.18 | (45) get(int, int, all_88_19, all_88_26) = all_88_16 % 25.20/4.18 | (46) get(int, int, all_88_11, all_88_3) = all_88_2 % 25.20/4.18 | (47) mk_array(int, $sum(usN, 1), all_88_24) = all_88_23 % 25.20/4.18 | (48) mk_array(int, $sum(usN, 1), all_88_19) = all_88_18 % 25.20/4.18 | (49) mk_array(int, $sum(usN, 1), all_88_11) = all_88_10 % 25.20/4.18 | (50) t2tb(f) = all_88_26 % 25.20/4.18 | (51) t2tb(all_88_4) = all_88_3 % 25.20/4.18 | (52) tb2t(all_88_16) = all_88_15 % 25.20/4.18 | (53) tb2t(all_88_2) = all_88_1 % 25.20/4.18 | (54) permut_all(int, all_88_18, all_88_23) = 0 % 25.20/4.18 | (55) permut_all(int, all_88_10, all_88_23) = 0 % 25.20/4.18 | (56) tb2t1(all_88_18) = all_88_17 % 25.20/4.18 | (57) tb2t1(all_88_10) = all_88_9 % 25.20/4.18 | (58) m_invariant(all_88_21, all_88_17) = 0 % 25.20/4.18 | (59) m_invariant(all_88_21, all_88_9) = 0 % 25.20/4.18 | (60) n_invariant(all_88_22, all_88_17) = 0 % 25.20/4.18 | (61) n_invariant(all_88_22, all_88_9) = 0 % 25.20/4.18 | (62) i_invariant(all_88_21, all_88_22, all_88_13, all_88_15, all_88_9) = 0 % 25.20/4.18 | (63) i_invariant(all_88_21, all_88_22, all_88_8, all_88_15, all_88_9) = 0 % 25.20/4.18 | (64) j_invariant(all_88_21, all_88_22, all_88_14, all_88_15, all_88_9) = 0 % 25.20/4.18 | (65) j_invariant(all_88_21, all_88_22, all_88_4, all_88_15, all_88_9) = 0 % 25.20/4.18 | (66) termination(all_88_13, all_88_14, all_88_21, all_88_22, all_88_15, % 25.20/4.18 | all_88_9) = 0 % 25.20/4.18 | (67) termination(all_88_8, all_88_4, all_88_21, all_88_22, all_88_15, % 25.20/4.18 | all_88_9) = 0 % 25.20/4.18 | (68) termination(all_88_8, $sum(all_88_4, -1), all_88_21, all_88_22, % 25.20/4.18 | all_88_15, all_88_9) = all_88_0 % 25.20/4.18 | (69) t2tb2(all_88_20) = all_88_19 % 25.20/4.18 | (70) t2tb2(all_88_12) = all_88_11 % 25.20/4.18 | % 25.20/4.18 | GROUND_INST: instantiating (20) with all_88_26, all_88_3, f, simplifying with % 25.20/4.18 | (50) gives: % 25.20/4.18 | (71) all_88_3 = all_88_26 | ~ (t2tb(f) = all_88_3) % 25.20/4.18 | % 25.20/4.18 | GROUND_INST: instantiating (1) with int, $sum(usN, 1), all_88_24, all_88_23, % 25.20/4.18 | simplifying with (18), (34), (47) gives: % 25.20/4.18 | (72) ? [v0: ty] : ? [v1: any] : ? [v2: uni] : (elts(int, all_88_23) = v2 % 25.20/4.18 | & map(int, int) = v0 & sort(v0, all_88_24) = v1 & ty(v0) & uni(v2) & % 25.20/4.19 | ( ~ (v1 = 0) | v2 = all_88_24)) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (1) with int, $sum(usN, 1), all_88_19, all_88_18, % 25.20/4.19 | simplifying with (18), (36), (48) gives: % 25.20/4.19 | (73) ? [v0: ty] : ? [v1: any] : ? [v2: uni] : (elts(int, all_88_18) = v2 % 25.20/4.19 | & map(int, int) = v0 & sort(v0, all_88_19) = v1 & ty(v0) & uni(v2) & % 25.20/4.19 | ( ~ (v1 = 0) | v2 = all_88_19)) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (1) with int, $sum(usN, 1), all_88_11, all_88_10, % 25.20/4.19 | simplifying with (18), (39), (49) gives: % 25.20/4.19 | (74) ? [v0: ty] : ? [v1: any] : ? [v2: uni] : (elts(int, all_88_10) = v2 % 25.20/4.19 | & map(int, int) = v0 & sort(v0, all_88_11) = v1 & ty(v0) & uni(v2) & % 25.20/4.19 | ( ~ (v1 = 0) | v2 = all_88_11)) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (bridgeR) with all_88_16, all_88_15, simplifying % 25.20/4.19 | with (38), (52) gives: % 25.20/4.19 | (75) t2tb(all_88_15) = all_88_16 % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (3) with int, all_88_18, all_88_23, simplifying % 25.20/4.19 | with (18), (35), (37), (54) gives: % 25.20/4.19 | (76) ? [v0: int] : ? [v1: uni] : ? [v2: uni] : (permut(int, v1, v2, 0, % 25.20/4.19 | v0) = 0 & elts(int, all_88_18) = v1 & elts(int, all_88_23) = v2 & % 25.20/4.19 | length(int, all_88_18) = v0 & length(int, all_88_23) = v0 & uni(v2) % 25.20/4.19 | & uni(v1)) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (3) with int, all_88_10, all_88_23, simplifying % 25.20/4.19 | with (18), (35), (40), (55) gives: % 25.20/4.19 | (77) ? [v0: int] : ? [v1: uni] : ? [v2: uni] : (permut(int, v1, v2, 0, % 25.20/4.19 | v0) = 0 & elts(int, all_88_10) = v1 & elts(int, all_88_23) = v2 & % 25.20/4.19 | length(int, all_88_10) = v0 & length(int, all_88_23) = v0 & uni(v2) % 25.20/4.19 | & uni(v1)) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (bridgeR1) with all_88_18, all_88_17, simplifying % 25.20/4.19 | with (37), (56) gives: % 25.20/4.19 | (78) t2tb1(all_88_17) = all_88_18 % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (bridgeR1) with all_88_10, all_88_9, simplifying % 25.20/4.19 | with (40), (57) gives: % 25.20/4.19 | (79) t2tb1(all_88_9) = all_88_10 % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (6) with all_88_21, all_88_17, simplifying with % 25.20/4.19 | (41), (58) gives: % 25.20/4.19 | (80) ? [v0: uni] : (t2tb1(all_88_17) = v0 & uni(v0) & ! [v1: int] : ! % 25.20/4.19 | [v2: int] : ! [v3: uni] : ! [v4: int] : ! [v5: uni] : ! [v6: % 25.20/4.19 | int] : ( ~ ($lesseq(1, $difference(v6, v4))) | ~ ($lesseq(v2, % 25.20/4.19 | usN)) | ~ ($lesseq(all_88_21, v2)) | ~ ($lesseq(1, % 25.20/4.19 | $difference(all_88_21, v1))) | ~ ($lesseq(1, v1)) | ~ % 25.20/4.19 | (tb2t(v5) = v6) | ~ (tb2t(v3) = v4) | ~ (get1(int, v0, v2) = v3) % 25.20/4.19 | | ~ (get1(int, v0, v1) = v5))) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (7) with all_88_21, all_88_9, simplifying with % 25.20/4.19 | (42), (59) gives: % 25.20/4.19 | (81) $lesseq(all_88_21, f) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (6) with all_88_21, all_88_9, simplifying with % 25.20/4.19 | (42), (59) gives: % 25.20/4.19 | (82) ? [v0: uni] : (t2tb1(all_88_9) = v0 & uni(v0) & ! [v1: int] : ! % 25.20/4.19 | [v2: int] : ! [v3: uni] : ! [v4: int] : ! [v5: uni] : ! [v6: % 25.20/4.19 | int] : ( ~ ($lesseq(1, $difference(v6, v4))) | ~ ($lesseq(v2, % 25.20/4.19 | usN)) | ~ ($lesseq(all_88_21, v2)) | ~ ($lesseq(1, % 25.20/4.19 | $difference(all_88_21, v1))) | ~ ($lesseq(1, v1)) | ~ % 25.20/4.19 | (tb2t(v5) = v6) | ~ (tb2t(v3) = v4) | ~ (get1(int, v0, v2) = v3) % 25.20/4.19 | | ~ (get1(int, v0, v1) = v5))) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (8) with all_88_22, all_88_17, simplifying with % 25.20/4.19 | (41), (60) gives: % 25.20/4.19 | (83) ? [v0: uni] : (t2tb1(all_88_17) = v0 & uni(v0) & ! [v1: int] : ! % 25.20/4.19 | [v2: int] : ! [v3: uni] : ! [v4: int] : ! [v5: uni] : ! [v6: % 25.20/4.19 | int] : ( ~ ($lesseq(1, $difference(v6, v4))) | ~ ($lesseq(v2, % 25.20/4.19 | usN)) | ~ ($lesseq(1, $difference(v2, all_88_22))) | ~ % 25.20/4.19 | ($lesseq(v1, all_88_22)) | ~ ($lesseq(1, v1)) | ~ (tb2t(v5) = % 25.20/4.19 | v6) | ~ (tb2t(v3) = v4) | ~ (get1(int, v0, v2) = v3) | ~ % 25.20/4.19 | (get1(int, v0, v1) = v5))) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (8) with all_88_22, all_88_9, simplifying with % 25.20/4.19 | (42), (61) gives: % 25.20/4.19 | (84) ? [v0: uni] : (t2tb1(all_88_9) = v0 & uni(v0) & ! [v1: int] : ! % 25.20/4.19 | [v2: int] : ! [v3: uni] : ! [v4: int] : ! [v5: uni] : ! [v6: % 25.20/4.19 | int] : ( ~ ($lesseq(1, $difference(v6, v4))) | ~ ($lesseq(v2, % 25.20/4.19 | usN)) | ~ ($lesseq(1, $difference(v2, all_88_22))) | ~ % 25.20/4.19 | ($lesseq(v1, all_88_22)) | ~ ($lesseq(1, v1)) | ~ (tb2t(v5) = % 25.20/4.19 | v6) | ~ (tb2t(v3) = v4) | ~ (get1(int, v0, v2) = v3) | ~ % 25.20/4.19 | (get1(int, v0, v1) = v5))) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (10) with all_88_21, all_88_22, all_88_13, % 25.20/4.19 | all_88_15, all_88_9, simplifying with (42), (62) gives: % 25.20/4.19 | (85) $lesseq(all_88_21, all_88_13) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (9) with all_88_21, all_88_22, all_88_13, % 25.20/4.19 | all_88_15, all_88_9, simplifying with (42), (62) gives: % 25.20/4.19 | (86) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 25.20/4.19 | (t2tb1(all_88_9) = v0 & uni(v0) & ! [v4: int] : ! [v5: uni] : ( ~ % 25.20/4.19 | ($lesseq(1, $difference(all_88_13, v4))) | ~ ($lesseq(1, v4)) | % 25.20/4.19 | ~ (get1(int, v0, v4) = v5) | ? [v6: int] : ($lesseq(v6, % 25.20/4.19 | all_88_15) & tb2t(v5) = v6)) & ( ~ ($lesseq(all_88_13, % 25.20/4.19 | all_88_22)) | ($lesseq(all_88_15, v3) & $lesseq(v1, all_88_22) % 25.20/4.19 | & $lesseq(all_88_13, v1) & tb2t(v2) = v3 & get1(int, v0, v1) = % 25.20/4.19 | v2 & uni(v2)))) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (10) with all_88_21, all_88_22, all_88_8, % 25.20/4.19 | all_88_15, all_88_9, simplifying with (42), (63) gives: % 25.20/4.19 | (87) $lesseq(all_88_21, all_88_8) % 25.20/4.19 | % 25.20/4.19 | GROUND_INST: instantiating (9) with all_88_21, all_88_22, all_88_8, all_88_15, % 25.20/4.19 | all_88_9, simplifying with (42), (63) gives: % 25.20/4.20 | (88) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 25.20/4.20 | (t2tb1(all_88_9) = v0 & uni(v0) & ! [v4: int] : ! [v5: uni] : ( ~ % 25.20/4.20 | ($lesseq(1, $difference(all_88_8, v4))) | ~ ($lesseq(1, v4)) | ~ % 25.20/4.20 | (get1(int, v0, v4) = v5) | ? [v6: int] : ($lesseq(v6, all_88_15) % 25.20/4.20 | & tb2t(v5) = v6)) & ( ~ ($lesseq(all_88_8, all_88_22)) | % 25.20/4.20 | ($lesseq(all_88_15, v3) & $lesseq(v1, all_88_22) & % 25.20/4.20 | $lesseq(all_88_8, v1) & tb2t(v2) = v3 & get1(int, v0, v1) = v2 & % 25.20/4.20 | uni(v2)))) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (11) with all_88_21, all_88_22, all_88_14, % 25.20/4.20 | all_88_15, all_88_9, simplifying with (42), (64) gives: % 25.20/4.20 | (89) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 25.20/4.20 | (t2tb1(all_88_9) = v0 & uni(v0) & ! [v4: int] : ! [v5: uni] : ( ~ % 25.20/4.20 | ($lesseq(v4, usN)) | ~ ($lesseq(1, $difference(v4, all_88_14))) | % 25.20/4.20 | ~ (get1(int, v0, v4) = v5) | ? [v6: int] : ($lesseq(all_88_15, % 25.20/4.20 | v6) & tb2t(v5) = v6)) & ( ~ ($lesseq(all_88_21, all_88_14)) | % 25.20/4.20 | ($lesseq(v3, all_88_15) & $lesseq(v1, all_88_14) & % 25.20/4.20 | $lesseq(all_88_21, v1) & tb2t(v2) = v3 & get1(int, v0, v1) = v2 % 25.20/4.20 | & uni(v2)))) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (12) with all_88_21, all_88_22, all_88_4, % 25.20/4.20 | all_88_15, all_88_9, simplifying with (42), (65) gives: % 25.20/4.20 | (90) $lesseq(all_88_4, all_88_22) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (11) with all_88_21, all_88_22, all_88_4, % 25.20/4.20 | all_88_15, all_88_9, simplifying with (42), (65) gives: % 25.20/4.20 | (91) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 25.20/4.20 | (t2tb1(all_88_9) = v0 & uni(v0) & ! [v4: int] : ! [v5: uni] : ( ~ % 25.20/4.20 | ($lesseq(v4, usN)) | ~ ($lesseq(1, $difference(v4, all_88_4))) | % 25.20/4.20 | ~ (get1(int, v0, v4) = v5) | ? [v6: int] : ($lesseq(all_88_15, % 25.20/4.20 | v6) & tb2t(v5) = v6)) & ( ~ ($lesseq(all_88_21, all_88_4)) | % 25.20/4.20 | ($lesseq(v3, all_88_15) & $lesseq(v1, all_88_4) & % 25.20/4.20 | $lesseq(all_88_21, v1) & tb2t(v2) = v3 & get1(int, v0, v1) = v2 % 25.20/4.20 | & uni(v2)))) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (13) with all_88_13, all_88_14, all_88_21, % 25.20/4.20 | all_88_22, all_88_15, all_88_9, simplifying with (42), (66) % 25.20/4.20 | gives: % 25.20/4.20 | (92) ~ ($lesseq(all_88_13, all_88_21)) | ? [v0: uni] : ? [v1: uni] : % 25.20/4.20 | (t2tb1(all_88_9) = v0 & tb2t(v1) = all_88_15 & get1(int, v0, f) = v1 & % 25.20/4.20 | uni(v1) & uni(v0)) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (14) with all_88_8, all_88_4, all_88_21, all_88_22, % 25.20/4.20 | all_88_15, all_88_9, simplifying with (42), (67) gives: % 25.20/4.20 | (93) ~ ($lesseq(1, $difference(f, all_88_4))) | ~ ($lesseq(all_88_8, % 25.20/4.20 | all_88_21)) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (16) with all_88_8, $sum(all_88_4, -1), all_88_21, % 25.20/4.20 | all_88_22, all_88_15, all_88_9, all_88_0, simplifying with (42), % 25.20/4.20 | (68) gives: % 25.20/4.20 | (94) all_88_0 = 0 | ~ ($lesseq(all_88_4, all_88_22)) | ~ ($lesseq(1, % 25.20/4.20 | $difference(all_88_8, all_88_21))) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (15) with all_88_8, $sum(all_88_4, -1), all_88_21, % 25.20/4.20 | all_88_22, all_88_15, all_88_9, all_88_0, simplifying with (42), % 25.20/4.20 | (68) gives: % 25.20/4.20 | (95) all_88_0 = 0 | ~ ($lesseq(1, $difference(all_88_4, f))) | ~ % 25.20/4.20 | ($lesseq(all_88_8, f)) | ? [v0: uni] : ? [v1: uni] : ? [v2: int] : % 25.20/4.20 | ( ~ (v2 = all_88_15) & t2tb1(all_88_9) = v0 & tb2t(v1) = v2 & % 25.20/4.20 | get1(int, v0, f) = v1 & uni(v1) & uni(v0)) % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (29) with all_88_20, all_88_19, simplifying with % 25.20/4.20 | (43), (69) gives: % 25.20/4.20 | (96) sort(all_84_0, all_88_19) = 0 % 25.20/4.20 | % 25.20/4.20 | GROUND_INST: instantiating (29) with all_88_12, all_88_11, simplifying with % 25.20/4.20 | (44), (70) gives: % 25.20/4.20 | (97) sort(all_84_0, all_88_11) = 0 % 25.20/4.20 | % 25.20/4.20 | DELTA: instantiating (76) with fresh symbols all_105_0, all_105_1, all_105_2 % 25.20/4.20 | gives: % 25.20/4.20 | (98) permut(int, all_105_1, all_105_0, 0, all_105_2) = 0 & elts(int, % 25.20/4.20 | all_88_18) = all_105_1 & elts(int, all_88_23) = all_105_0 & % 25.20/4.20 | length(int, all_88_18) = all_105_2 & length(int, all_88_23) = % 25.20/4.20 | all_105_2 & uni(all_105_0) & uni(all_105_1) % 25.20/4.20 | % 25.20/4.20 | ALPHA: (98) implies: % 25.20/4.20 | (99) elts(int, all_88_18) = all_105_1 % 25.20/4.20 | % 25.20/4.20 | DELTA: instantiating (72) with fresh symbols all_107_0, all_107_1, all_107_2 % 25.20/4.20 | gives: % 25.20/4.20 | (100) elts(int, all_88_23) = all_107_0 & map(int, int) = all_107_2 & % 25.20/4.20 | sort(all_107_2, all_88_24) = all_107_1 & ty(all_107_2) & % 25.20/4.20 | uni(all_107_0) & ( ~ (all_107_1 = 0) | all_107_0 = all_88_24) % 25.20/4.20 | % 25.20/4.20 | ALPHA: (100) implies: % 25.20/4.20 | (101) map(int, int) = all_107_2 % 25.20/4.20 | % 25.20/4.20 | DELTA: instantiating (73) with fresh symbols all_109_0, all_109_1, all_109_2 % 25.20/4.20 | gives: % 25.20/4.20 | (102) elts(int, all_88_18) = all_109_0 & map(int, int) = all_109_2 & % 25.20/4.20 | sort(all_109_2, all_88_19) = all_109_1 & ty(all_109_2) & % 25.20/4.20 | uni(all_109_0) & ( ~ (all_109_1 = 0) | all_109_0 = all_88_19) % 25.20/4.20 | % 25.20/4.20 | ALPHA: (102) implies: % 25.20/4.20 | (103) sort(all_109_2, all_88_19) = all_109_1 % 25.20/4.20 | (104) map(int, int) = all_109_2 % 25.20/4.20 | (105) elts(int, all_88_18) = all_109_0 % 25.20/4.20 | (106) ~ (all_109_1 = 0) | all_109_0 = all_88_19 % 25.20/4.20 | % 25.20/4.20 | DELTA: instantiating (77) with fresh symbols all_111_0, all_111_1, all_111_2 % 25.20/4.20 | gives: % 25.20/4.20 | (107) permut(int, all_111_1, all_111_0, 0, all_111_2) = 0 & elts(int, % 25.20/4.20 | all_88_10) = all_111_1 & elts(int, all_88_23) = all_111_0 & % 25.20/4.20 | length(int, all_88_10) = all_111_2 & length(int, all_88_23) = % 25.20/4.20 | all_111_2 & uni(all_111_0) & uni(all_111_1) % 25.20/4.20 | % 25.20/4.20 | ALPHA: (107) implies: % 25.20/4.20 | (108) elts(int, all_88_10) = all_111_1 % 25.20/4.20 | % 25.20/4.20 | DELTA: instantiating (74) with fresh symbols all_113_0, all_113_1, all_113_2 % 25.20/4.20 | gives: % 25.20/4.20 | (109) elts(int, all_88_10) = all_113_0 & map(int, int) = all_113_2 & % 25.20/4.20 | sort(all_113_2, all_88_11) = all_113_1 & ty(all_113_2) & % 25.20/4.20 | uni(all_113_0) & ( ~ (all_113_1 = 0) | all_113_0 = all_88_11) % 25.20/4.20 | % 25.20/4.20 | ALPHA: (109) implies: % 25.20/4.21 | (110) sort(all_113_2, all_88_11) = all_113_1 % 25.20/4.21 | (111) map(int, int) = all_113_2 % 25.20/4.21 | (112) elts(int, all_88_10) = all_113_0 % 25.20/4.21 | (113) ~ (all_113_1 = 0) | all_113_0 = all_88_11 % 25.20/4.21 | % 25.20/4.21 | DELTA: instantiating (82) with fresh symbol all_115_0 gives: % 25.20/4.21 | (114) t2tb1(all_88_9) = all_115_0 & uni(all_115_0) & ! [v0: int] : ! [v1: % 25.20/4.21 | int] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] : % 25.20/4.21 | ( ~ ($lesseq(1, $difference(v5, v3))) | ~ ($lesseq(v1, usN)) | ~ % 25.20/4.21 | ($lesseq(all_88_21, v1)) | ~ ($lesseq(1, $difference(all_88_21, % 25.20/4.21 | v0))) | ~ ($lesseq(1, v0)) | ~ (tb2t(v4) = v5) | ~ % 25.20/4.21 | (tb2t(v2) = v3) | ~ (get1(int, all_115_0, v1) = v2) | ~ % 25.20/4.21 | (get1(int, all_115_0, v0) = v4)) % 25.20/4.21 | % 25.20/4.21 | ALPHA: (114) implies: % 25.20/4.21 | (115) uni(all_115_0) % 25.20/4.21 | (116) t2tb1(all_88_9) = all_115_0 % 25.20/4.21 | % 25.20/4.21 | DELTA: instantiating (80) with fresh symbol all_118_0 gives: % 25.20/4.21 | (117) t2tb1(all_88_17) = all_118_0 & uni(all_118_0) & ! [v0: int] : ! % 25.20/4.21 | [v1: int] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] % 25.20/4.21 | : ( ~ ($lesseq(1, $difference(v5, v3))) | ~ ($lesseq(v1, usN)) | ~ % 25.20/4.21 | ($lesseq(all_88_21, v1)) | ~ ($lesseq(1, $difference(all_88_21, % 25.20/4.21 | v0))) | ~ ($lesseq(1, v0)) | ~ (tb2t(v4) = v5) | ~ % 25.20/4.21 | (tb2t(v2) = v3) | ~ (get1(int, all_118_0, v1) = v2) | ~ % 25.20/4.21 | (get1(int, all_118_0, v0) = v4)) % 25.20/4.21 | % 25.20/4.21 | ALPHA: (117) implies: % 25.20/4.21 | (118) uni(all_118_0) % 25.20/4.21 | (119) t2tb1(all_88_17) = all_118_0 % 25.20/4.21 | % 25.20/4.21 | DELTA: instantiating (83) with fresh symbol all_121_0 gives: % 25.20/4.21 | (120) t2tb1(all_88_17) = all_121_0 & uni(all_121_0) & ! [v0: int] : ! % 25.20/4.21 | [v1: int] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] % 25.20/4.21 | : ( ~ ($lesseq(1, $difference(v5, v3))) | ~ ($lesseq(v1, usN)) | ~ % 25.20/4.21 | ($lesseq(1, $difference(v1, all_88_22))) | ~ ($lesseq(v0, % 25.20/4.21 | all_88_22)) | ~ ($lesseq(1, v0)) | ~ (tb2t(v4) = v5) | ~ % 25.20/4.21 | (tb2t(v2) = v3) | ~ (get1(int, all_121_0, v1) = v2) | ~ % 25.20/4.21 | (get1(int, all_121_0, v0) = v4)) % 25.20/4.21 | % 25.20/4.21 | ALPHA: (120) implies: % 25.20/4.21 | (121) t2tb1(all_88_17) = all_121_0 % 25.20/4.21 | % 25.20/4.21 | DELTA: instantiating (84) with fresh symbol all_124_0 gives: % 25.20/4.21 | (122) t2tb1(all_88_9) = all_124_0 & uni(all_124_0) & ! [v0: int] : ! [v1: % 25.20/4.21 | int] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: int] : % 25.20/4.21 | ( ~ ($lesseq(1, $difference(v5, v3))) | ~ ($lesseq(v1, usN)) | ~ % 25.20/4.21 | ($lesseq(1, $difference(v1, all_88_22))) | ~ ($lesseq(v0, % 25.20/4.21 | all_88_22)) | ~ ($lesseq(1, v0)) | ~ (tb2t(v4) = v5) | ~ % 25.20/4.21 | (tb2t(v2) = v3) | ~ (get1(int, all_124_0, v1) = v2) | ~ % 25.20/4.21 | (get1(int, all_124_0, v0) = v4)) % 25.20/4.21 | % 25.20/4.21 | ALPHA: (122) implies: % 25.20/4.21 | (123) t2tb1(all_88_9) = all_124_0 % 25.20/4.21 | % 25.20/4.21 | DELTA: instantiating (86) with fresh symbols all_127_0, all_127_1, all_127_2, % 25.20/4.21 | all_127_3 gives: % 25.20/4.21 | (124) t2tb1(all_88_9) = all_127_3 & uni(all_127_3) & ! [v0: int] : ! [v1: % 25.20/4.21 | uni] : ( ~ ($lesseq(1, $difference(all_88_13, v0))) | ~ % 25.20/4.21 | ($lesseq(1, v0)) | ~ (get1(int, all_127_3, v0) = v1) | ? [v2: % 25.20/4.21 | int] : ($lesseq(v2, all_88_15) & tb2t(v1) = v2)) & ( ~ % 25.20/4.21 | ($lesseq(all_88_13, all_88_22)) | ($lesseq(all_88_15, all_127_0) & % 25.20/4.21 | $lesseq(all_127_2, all_88_22) & $lesseq(all_88_13, all_127_2) & % 25.20/4.21 | tb2t(all_127_1) = all_127_0 & get1(int, all_127_3, all_127_2) = % 25.20/4.21 | all_127_1 & uni(all_127_1))) % 25.20/4.21 | % 25.20/4.21 | ALPHA: (124) implies: % 25.55/4.21 | (125) t2tb1(all_88_9) = all_127_3 % 25.55/4.21 | % 25.55/4.21 | DELTA: instantiating (91) with fresh symbols all_130_0, all_130_1, all_130_2, % 25.55/4.21 | all_130_3 gives: % 25.55/4.21 | (126) t2tb1(all_88_9) = all_130_3 & uni(all_130_3) & ! [v0: int] : ! [v1: % 25.55/4.21 | uni] : ( ~ ($lesseq(v0, usN)) | ~ ($lesseq(1, $difference(v0, % 25.55/4.21 | all_88_4))) | ~ (get1(int, all_130_3, v0) = v1) | ? [v2: % 25.55/4.21 | int] : ($lesseq(all_88_15, v2) & tb2t(v1) = v2)) & ( ~ % 25.55/4.21 | ($lesseq(all_88_21, all_88_4)) | ($lesseq(all_130_0, all_88_15) & % 25.55/4.21 | $lesseq(all_130_2, all_88_4) & $lesseq(all_88_21, all_130_2) & % 25.55/4.21 | tb2t(all_130_1) = all_130_0 & get1(int, all_130_3, all_130_2) = % 25.55/4.21 | all_130_1 & uni(all_130_1))) % 25.55/4.21 | % 25.55/4.21 | ALPHA: (126) implies: % 25.55/4.21 | (127) t2tb1(all_88_9) = all_130_3 % 25.55/4.21 | % 25.55/4.21 | DELTA: instantiating (89) with fresh symbols all_133_0, all_133_1, all_133_2, % 25.55/4.21 | all_133_3 gives: % 25.55/4.21 | (128) t2tb1(all_88_9) = all_133_3 & uni(all_133_3) & ! [v0: int] : ! [v1: % 25.55/4.21 | uni] : ( ~ ($lesseq(v0, usN)) | ~ ($lesseq(1, $difference(v0, % 25.55/4.21 | all_88_14))) | ~ (get1(int, all_133_3, v0) = v1) | ? [v2: % 25.55/4.21 | int] : ($lesseq(all_88_15, v2) & tb2t(v1) = v2)) & ( ~ % 25.55/4.21 | ($lesseq(all_88_21, all_88_14)) | ($lesseq(all_133_0, all_88_15) & % 25.55/4.21 | $lesseq(all_133_2, all_88_14) & $lesseq(all_88_21, all_133_2) & % 25.55/4.21 | tb2t(all_133_1) = all_133_0 & get1(int, all_133_3, all_133_2) = % 25.55/4.21 | all_133_1 & uni(all_133_1))) % 25.55/4.21 | % 25.55/4.21 | ALPHA: (128) implies: % 25.55/4.21 | (129) t2tb1(all_88_9) = all_133_3 % 25.55/4.21 | % 25.55/4.21 | DELTA: instantiating (88) with fresh symbols all_136_0, all_136_1, all_136_2, % 25.55/4.21 | all_136_3 gives: % 25.55/4.21 | (130) t2tb1(all_88_9) = all_136_3 & uni(all_136_3) & ! [v0: int] : ! [v1: % 25.55/4.21 | uni] : ( ~ ($lesseq(1, $difference(all_88_8, v0))) | ~ ($lesseq(1, % 25.55/4.21 | v0)) | ~ (get1(int, all_136_3, v0) = v1) | ? [v2: int] : % 25.55/4.21 | ($lesseq(v2, all_88_15) & tb2t(v1) = v2)) & ( ~ ($lesseq(all_88_8, % 25.55/4.21 | all_88_22)) | ($lesseq(all_88_15, all_136_0) & % 25.55/4.21 | $lesseq(all_136_2, all_88_22) & $lesseq(all_88_8, all_136_2) & % 25.55/4.21 | tb2t(all_136_1) = all_136_0 & get1(int, all_136_3, all_136_2) = % 25.55/4.21 | all_136_1 & uni(all_136_1))) % 25.55/4.21 | % 25.55/4.21 | ALPHA: (130) implies: % 25.55/4.21 | (131) t2tb1(all_88_9) = all_136_3 % 25.55/4.21 | % 25.55/4.21 | BETA: splitting (94) gives: % 25.55/4.21 | % 25.55/4.21 | Case 1: % 25.55/4.21 | | % 25.55/4.21 | | (132) $lesseq(1, $difference(all_88_4, all_88_22)) % 25.55/4.21 | | % 25.55/4.21 | | COMBINE_INEQS: (90), (132) imply: % 25.55/4.21 | | (133) $false % 25.55/4.22 | | % 25.55/4.22 | | CLOSE: (133) is inconsistent. % 25.55/4.22 | | % 25.55/4.22 | Case 2: % 25.55/4.22 | | % 25.55/4.22 | | (134) all_88_0 = 0 | ~ ($lesseq(1, $difference(all_88_8, all_88_21))) % 25.55/4.22 | | % 25.55/4.22 | | BETA: splitting (134) gives: % 25.55/4.22 | | % 25.55/4.22 | | Case 1: % 25.55/4.22 | | | % 25.55/4.22 | | | (135) $lesseq(all_88_8, all_88_21) % 25.55/4.22 | | | % 25.55/4.22 | | | COMBINE_INEQS: (32), (135) imply: % 25.55/4.22 | | | (136) $lesseq(all_88_13, all_88_21) % 25.55/4.22 | | | % 25.55/4.22 | | | ANTI_SYMM: (87), (135) imply: % 25.55/4.22 | | | (137) all_88_8 = all_88_21 % 25.55/4.22 | | | % 25.55/4.22 | | | ANTI_SYMM: (85), (136) imply: % 25.55/4.22 | | | (138) all_88_13 = all_88_21 % 25.55/4.22 | | | % 25.55/4.22 | | | BETA: splitting (93) gives: % 25.55/4.22 | | | % 25.55/4.22 | | | Case 1: % 25.55/4.22 | | | | % 25.55/4.22 | | | | (139) $lesseq(1, $difference(all_88_8, all_88_21)) % 25.55/4.22 | | | | % 25.55/4.22 | | | | REDUCE: (137), (139) imply: % 25.55/4.22 | | | | (140) $false % 25.55/4.22 | | | | % 25.55/4.22 | | | | CLOSE: (140) is inconsistent. % 25.55/4.22 | | | | % 25.55/4.22 | | | Case 2: % 25.55/4.22 | | | | % 25.55/4.22 | | | | (141) $lesseq(f, all_88_4) % 25.55/4.22 | | | | % 25.55/4.22 | | | | BETA: splitting (92) gives: % 25.55/4.22 | | | | % 25.55/4.22 | | | | Case 1: % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | (142) $lesseq(1, $difference(all_88_13, all_88_21)) % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | REDUCE: (138), (142) imply: % 25.55/4.22 | | | | | (143) $false % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | CLOSE: (143) is inconsistent. % 25.55/4.22 | | | | | % 25.55/4.22 | | | | Case 2: % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | (144) ? [v0: uni] : ? [v1: uni] : (t2tb1(all_88_9) = v0 & % 25.55/4.22 | | | | | tb2t(v1) = all_88_15 & get1(int, v0, f) = v1 & uni(v1) & % 25.55/4.22 | | | | | uni(v0)) % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | DELTA: instantiating (144) with fresh symbols all_181_0, all_181_1 % 25.55/4.22 | | | | | gives: % 25.55/4.22 | | | | | (145) t2tb1(all_88_9) = all_181_1 & tb2t(all_181_0) = all_88_15 & % 25.55/4.22 | | | | | get1(int, all_181_1, f) = all_181_0 & uni(all_181_0) & % 25.55/4.22 | | | | | uni(all_181_1) % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | ALPHA: (145) implies: % 25.55/4.22 | | | | | (146) get1(int, all_181_1, f) = all_181_0 % 25.55/4.22 | | | | | (147) t2tb1(all_88_9) = all_181_1 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | DELTA: instantiating (144) with fresh symbols all_188_0, all_188_1 % 25.55/4.22 | | | | | gives: % 25.55/4.22 | | | | | (148) t2tb1(all_88_9) = all_188_1 & tb2t(all_188_0) = all_88_15 & % 25.55/4.22 | | | | | get1(int, all_188_1, f) = all_188_0 & uni(all_188_0) & % 25.55/4.22 | | | | | uni(all_188_1) % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | ALPHA: (148) implies: % 25.55/4.22 | | | | | (149) uni(all_188_0) % 25.55/4.22 | | | | | (150) get1(int, all_188_1, f) = all_188_0 % 25.55/4.22 | | | | | (151) tb2t(all_188_0) = all_88_15 % 25.55/4.22 | | | | | (152) t2tb1(all_88_9) = all_188_1 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (24) with all_84_0, all_109_2, int, int, % 25.55/4.22 | | | | | simplifying with (28), (104) gives: % 25.55/4.22 | | | | | (153) all_109_2 = all_84_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (24) with all_109_2, all_113_2, int, int, % 25.55/4.22 | | | | | simplifying with (104), (111) gives: % 25.55/4.22 | | | | | (154) all_113_2 = all_109_2 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (24) with all_107_2, all_113_2, int, int, % 25.55/4.22 | | | | | simplifying with (101), (111) gives: % 25.55/4.22 | | | | | (155) all_113_2 = all_107_2 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (25) with all_105_1, all_109_0, all_88_18, % 25.55/4.22 | | | | | int, simplifying with (99), (105) gives: % 25.55/4.22 | | | | | (156) all_109_0 = all_105_1 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (25) with all_111_1, all_113_0, all_88_10, % 25.55/4.22 | | | | | int, simplifying with (108), (112) gives: % 25.55/4.22 | | | | | (157) all_113_0 = all_111_1 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_118_0, all_121_0, all_88_17, % 25.55/4.22 | | | | | simplifying with (119), (121) gives: % 25.55/4.22 | | | | | (158) all_121_0 = all_118_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_88_18, all_121_0, all_88_17, % 25.55/4.22 | | | | | simplifying with (78), (121) gives: % 25.55/4.22 | | | | | (159) all_121_0 = all_88_18 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_124_0, all_127_3, all_88_9, % 25.55/4.22 | | | | | simplifying with (123), (125) gives: % 25.55/4.22 | | | | | (160) all_127_3 = all_124_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_130_3, all_133_3, all_88_9, % 25.55/4.22 | | | | | simplifying with (127), (129) gives: % 25.55/4.22 | | | | | (161) all_133_3 = all_130_3 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_127_3, all_133_3, all_88_9, % 25.55/4.22 | | | | | simplifying with (125), (129) gives: % 25.55/4.22 | | | | | (162) all_133_3 = all_127_3 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_136_3, all_181_1, all_88_9, % 25.55/4.22 | | | | | simplifying with (131), (147) gives: % 25.55/4.22 | | | | | (163) all_181_1 = all_136_3 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_124_0, all_181_1, all_88_9, % 25.55/4.22 | | | | | simplifying with (123), (147) gives: % 25.55/4.22 | | | | | (164) all_181_1 = all_124_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_115_0, all_181_1, all_88_9, % 25.55/4.22 | | | | | simplifying with (116), (147) gives: % 25.55/4.22 | | | | | (165) all_181_1 = all_115_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_133_3, all_188_1, all_88_9, % 25.55/4.22 | | | | | simplifying with (129), (152) gives: % 25.55/4.22 | | | | | (166) all_188_1 = all_133_3 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | GROUND_INST: instantiating (22) with all_88_10, all_188_1, all_88_9, % 25.55/4.22 | | | | | simplifying with (79), (152) gives: % 25.55/4.22 | | | | | (167) all_188_1 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (166), (167) imply: % 25.55/4.22 | | | | | (168) all_133_3 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (168) implies: % 25.55/4.22 | | | | | (169) all_133_3 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (163), (165) imply: % 25.55/4.22 | | | | | (170) all_136_3 = all_115_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (163), (164) imply: % 25.55/4.22 | | | | | (171) all_136_3 = all_124_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (170), (171) imply: % 25.55/4.22 | | | | | (172) all_124_0 = all_115_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (172) implies: % 25.55/4.22 | | | | | (173) all_124_0 = all_115_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (161), (162) imply: % 25.55/4.22 | | | | | (174) all_130_3 = all_127_3 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (161), (169) imply: % 25.55/4.22 | | | | | (175) all_130_3 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (174), (175) imply: % 25.55/4.22 | | | | | (176) all_127_3 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (176) implies: % 25.55/4.22 | | | | | (177) all_127_3 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (160), (177) imply: % 25.55/4.22 | | | | | (178) all_124_0 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (178) implies: % 25.55/4.22 | | | | | (179) all_124_0 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (173), (179) imply: % 25.55/4.22 | | | | | (180) all_115_0 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (180) implies: % 25.55/4.22 | | | | | (181) all_115_0 = all_88_10 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (158), (159) imply: % 25.55/4.22 | | | | | (182) all_118_0 = all_88_18 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (154), (155) imply: % 25.55/4.22 | | | | | (183) all_109_2 = all_107_2 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | SIMP: (183) implies: % 25.55/4.22 | | | | | (184) all_109_2 = all_107_2 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (153), (184) imply: % 25.55/4.22 | | | | | (185) all_107_2 = all_84_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (155), (185) imply: % 25.55/4.22 | | | | | (186) all_113_2 = all_84_0 % 25.55/4.22 | | | | | % 25.55/4.22 | | | | | COMBINE_EQS: (170), (181) imply: % 25.55/4.23 | | | | | (187) all_136_3 = all_88_10 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | COMBINE_EQS: (163), (187) imply: % 25.55/4.23 | | | | | (188) all_181_1 = all_88_10 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | REDUCE: (150), (167) imply: % 25.55/4.23 | | | | | (189) get1(int, all_88_10, f) = all_188_0 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | REDUCE: (146), (188) imply: % 25.55/4.23 | | | | | (190) get1(int, all_88_10, f) = all_181_0 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | REDUCE: (110), (186) imply: % 25.55/4.23 | | | | | (191) sort(all_84_0, all_88_11) = all_113_1 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | REDUCE: (103), (153) imply: % 25.55/4.23 | | | | | (192) sort(all_84_0, all_88_19) = all_109_1 % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | BETA: splitting (95) gives: % 25.55/4.23 | | | | | % 25.55/4.23 | | | | | Case 1: % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | (193) $lesseq(1, $difference(all_88_8, f)) % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | REDUCE: (137), (193) imply: % 25.55/4.23 | | | | | | (194) $lesseq(1, $difference(all_88_21, f)) % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | COMBINE_INEQS: (81), (194) imply: % 25.55/4.23 | | | | | | (195) $false % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | CLOSE: (195) is inconsistent. % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | Case 2: % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | (196) all_88_0 = 0 | ~ ($lesseq(1, $difference(all_88_4, f))) | % 25.55/4.23 | | | | | | ? [v0: uni] : ? [v1: uni] : ? [v2: int] : ( ~ (v2 = % 25.55/4.23 | | | | | | all_88_15) & t2tb1(all_88_9) = v0 & tb2t(v1) = v2 & % 25.55/4.23 | | | | | | get1(int, v0, f) = v1 & uni(v1) & uni(v0)) % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | BETA: splitting (196) gives: % 25.55/4.23 | | | | | | % 25.55/4.23 | | | | | | Case 1: % 25.55/4.23 | | | | | | | % 25.55/4.23 | | | | | | | (197) $lesseq(all_88_4, f) % 25.55/4.23 | | | | | | | % 25.55/4.23 | | | | | | | ANTI_SYMM: (141), (197) imply: % 25.55/4.23 | | | | | | | (198) all_88_4 = f % 25.55/4.23 | | | | | | | % 25.55/4.23 | | | | | | | REDUCE: (51), (198) imply: % 25.55/4.23 | | | | | | | (199) t2tb(f) = all_88_3 % 25.55/4.23 | | | | | | | % 25.55/4.23 | | | | | | | BETA: splitting (71) gives: % 25.55/4.23 | | | | | | | % 25.55/4.23 | | | | | | | Case 1: % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | (200) ~ (t2tb(f) = all_88_3) % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | PRED_UNIFY: (199), (200) imply: % 25.55/4.23 | | | | | | | | (201) $false % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | CLOSE: (201) is inconsistent. % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | Case 2: % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | (202) all_88_3 = all_88_26 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | REDUCE: (46), (202) imply: % 25.55/4.23 | | | | | | | | (203) get(int, int, all_88_11, all_88_26) = all_88_2 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | GROUND_INST: instantiating (23) with 0, all_109_1, all_88_19, % 25.55/4.23 | | | | | | | | all_84_0, simplifying with (96), (192) gives: % 25.55/4.23 | | | | | | | | (204) all_109_1 = 0 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | GROUND_INST: instantiating (23) with 0, all_113_1, all_88_11, % 25.55/4.23 | | | | | | | | all_84_0, simplifying with (97), (191) gives: % 25.55/4.23 | | | | | | | | (205) all_113_1 = 0 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | GROUND_INST: instantiating (26) with all_181_0, all_188_0, f, % 25.55/4.23 | | | | | | | | all_88_10, int, simplifying with (189), (190) % 25.55/4.23 | | | | | | | | gives: % 25.55/4.23 | | | | | | | | (206) all_188_0 = all_181_0 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | REDUCE: (151), (206) imply: % 25.55/4.23 | | | | | | | | (207) tb2t(all_181_0) = all_88_15 % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | REDUCE: (149), (206) imply: % 25.55/4.23 | | | | | | | | (208) uni(all_181_0) % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | BETA: splitting (113) gives: % 25.55/4.23 | | | | | | | | % 25.55/4.23 | | | | | | | | Case 1: % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | (209) ~ (all_113_1 = 0) % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | REDUCE: (205), (209) imply: % 25.55/4.23 | | | | | | | | | (210) $false % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | CLOSE: (210) is inconsistent. % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | Case 2: % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | (211) all_113_0 = all_88_11 % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | COMBINE_EQS: (157), (211) imply: % 25.55/4.23 | | | | | | | | | (212) all_111_1 = all_88_11 % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | SIMP: (212) implies: % 25.55/4.23 | | | | | | | | | (213) all_111_1 = all_88_11 % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | REDUCE: (108), (213) imply: % 25.55/4.23 | | | | | | | | | (214) elts(int, all_88_10) = all_88_11 % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | BETA: splitting (106) gives: % 25.55/4.23 | | | | | | | | | % 25.55/4.23 | | | | | | | | | Case 1: % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | (215) ~ (all_109_1 = 0) % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | REDUCE: (204), (215) imply: % 25.55/4.23 | | | | | | | | | | (216) $false % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | CLOSE: (216) is inconsistent. % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | Case 2: % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | (217) all_109_0 = all_88_19 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | COMBINE_EQS: (156), (217) imply: % 25.55/4.23 | | | | | | | | | | (218) all_105_1 = all_88_19 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | SIMP: (218) implies: % 25.55/4.23 | | | | | | | | | | (219) all_105_1 = all_88_19 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | REDUCE: (99), (219) imply: % 25.55/4.23 | | | | | | | | | | (220) elts(int, all_88_18) = all_88_19 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | GROUND_INST: instantiating (2) with int, all_88_18, f, % 25.55/4.23 | | | | | | | | | | all_88_19, all_88_26, all_88_16, simplifying with % 25.55/4.23 | | | | | | | | | | (18), (37), (45), (50), (220) gives: % 25.55/4.23 | | | | | | | | | | (221) get1(int, all_88_18, f) = all_88_16 & % 25.55/4.23 | | | | | | | | | | uni(all_88_16) % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | ALPHA: (221) implies: % 25.55/4.23 | | | | | | | | | | (222) get1(int, all_88_18, f) = all_88_16 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | GROUND_INST: instantiating (2) with int, all_88_10, f, % 25.55/4.23 | | | | | | | | | | all_88_11, all_88_26, all_88_2, simplifying with % 25.55/4.23 | | | | | | | | | | (18), (40), (50), (203), (214) gives: % 25.55/4.23 | | | | | | | | | | (223) get1(int, all_88_10, f) = all_88_2 & uni(all_88_2) % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | ALPHA: (223) implies: % 25.55/4.23 | | | | | | | | | | (224) get1(int, all_88_10, f) = all_88_2 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_181_0, all_88_15, % 25.55/4.23 | | | | | | | | | | simplifying with (207), (208) gives: % 25.55/4.23 | | | | | | | | | | (225) t2tb(all_88_15) = all_181_0 % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | GROUND_INST: instantiating (5) with all_88_17, all_88_18, % 25.55/4.23 | | | | | | | | | | simplifying with (41), (78) gives: % 25.55/4.23 | | | | | | | | | | (226) ? [v0: uni] : ? [v1: int] : ? [v2: any] : ? % 25.55/4.23 | | | | | | | | | | [v3: int] : ? [v4: int] : ? [v5: uni] : ? [v6: % 25.55/4.23 | | | | | | | | | | int] : ? [v7: uni] : ? [v8: int] : % 25.55/4.23 | | | | | | | | | | (found(all_88_17) = v2 & tb2t(v0) = v1 & get1(int, % 25.55/4.23 | | | | | | | | | | all_88_18, f) = v0 & uni(v0) & (v2 = 0 | % 25.55/4.23 | | | | | | | | | | ($lesseq(v4, usN) & $lesseq(f, v4) & % 25.55/4.23 | | | | | | | | | | $lesseq(v3, f) & $lesseq(1, v3) & tb2t(v7) = % 25.55/4.23 | | | | | | | | | | v8 & tb2t(v5) = v6 & get1(int, all_88_18, v4) % 25.55/4.23 | | | | | | | | | | = v7 & get1(int, all_88_18, v3) = v5 & % 25.55/4.23 | | | | | | | | | | uni(v7) & uni(v5) & ( ~ ($lesseq(v1, v8)) | % 25.55/4.23 | | | | | | | | | | ~ ($lesseq(v6, v1)))))) % 25.55/4.23 | | | | | | | | | | % 25.55/4.23 | | | | | | | | | | GROUND_INST: instantiating (4) with all_88_17, all_88_18, % 25.55/4.23 | | | | | | | | | | simplifying with (41), (78) gives: % 25.55/4.24 | | | | | | | | | | (227) ? [v0: any] : ? [v1: uni] : ? [v2: int] : % 25.55/4.24 | | | | | | | | | | (found(all_88_17) = v0 & tb2t(v1) = v2 & get1(int, % 25.55/4.24 | | | | | | | | | | all_88_18, f) = v1 & uni(v1) & ( ~ (v0 = 0) | ( % 25.55/4.24 | | | | | | | | | | ! [v3: int] : ! [v4: int] : ! [v5: uni] : % 25.55/4.24 | | | | | | | | | | ! [v6: int] : ! [v7: uni] : ! [v8: int] : ( % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(1, $difference(v2, v8))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v4, usN)) | ~ ($lesseq(f, v4)) | % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(v3, f)) | ~ ($lesseq(1, v3)) | % 25.55/4.24 | | | | | | | | | | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v4) = v7) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v3) = v5)) & ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: int] : ! [v5: uni] : ! % 25.55/4.24 | | | | | | | | | | [v6: int] : ! [v7: uni] : ! [v8: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(v6, v2))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v4, usN)) | ~ ($lesseq(f, v4)) | % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(v3, f)) | ~ ($lesseq(1, v3)) | % 25.55/4.24 | | | | | | | | | | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v4) = v7) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v3) = v5))))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (5) with all_88_9, all_88_10, % 25.55/4.24 | | | | | | | | | | simplifying with (42), (79) gives: % 25.55/4.24 | | | | | | | | | | (228) ? [v0: uni] : ? [v1: int] : ? [v2: any] : ? % 25.55/4.24 | | | | | | | | | | [v3: int] : ? [v4: int] : ? [v5: uni] : ? [v6: % 25.55/4.24 | | | | | | | | | | int] : ? [v7: uni] : ? [v8: int] : % 25.55/4.24 | | | | | | | | | | (found(all_88_9) = v2 & tb2t(v0) = v1 & get1(int, % 25.55/4.24 | | | | | | | | | | all_88_10, f) = v0 & uni(v0) & (v2 = 0 | % 25.55/4.24 | | | | | | | | | | ($lesseq(v4, usN) & $lesseq(f, v4) & % 25.55/4.24 | | | | | | | | | | $lesseq(v3, f) & $lesseq(1, v3) & tb2t(v7) = % 25.55/4.24 | | | | | | | | | | v8 & tb2t(v5) = v6 & get1(int, all_88_10, v4) % 25.55/4.24 | | | | | | | | | | = v7 & get1(int, all_88_10, v3) = v5 & % 25.55/4.24 | | | | | | | | | | uni(v7) & uni(v5) & ( ~ ($lesseq(v1, v8)) | % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(v6, v1)))))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (4) with all_88_9, all_88_10, % 25.55/4.24 | | | | | | | | | | simplifying with (42), (79) gives: % 25.55/4.24 | | | | | | | | | | (229) ? [v0: any] : ? [v1: uni] : ? [v2: int] : % 25.55/4.24 | | | | | | | | | | (found(all_88_9) = v0 & tb2t(v1) = v2 & get1(int, % 25.55/4.24 | | | | | | | | | | all_88_10, f) = v1 & uni(v1) & ( ~ (v0 = 0) | ( % 25.55/4.24 | | | | | | | | | | ! [v3: int] : ! [v4: int] : ! [v5: uni] : % 25.55/4.24 | | | | | | | | | | ! [v6: int] : ! [v7: uni] : ! [v8: int] : ( % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(1, $difference(v2, v8))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v4, usN)) | ~ ($lesseq(f, v4)) | % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(v3, f)) | ~ ($lesseq(1, v3)) | % 25.55/4.24 | | | | | | | | | | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v4) = v7) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v3) = v5)) & ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: int] : ! [v5: uni] : ! % 25.55/4.24 | | | | | | | | | | [v6: int] : ! [v7: uni] : ! [v8: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(v6, v2))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v4, usN)) | ~ ($lesseq(f, v4)) | % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(v3, f)) | ~ ($lesseq(1, v3)) | % 25.55/4.24 | | | | | | | | | | ~ (tb2t(v7) = v8) | ~ (tb2t(v5) = v6) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v4) = v7) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v3) = v5))))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | DELTA: instantiating (228) with fresh symbols all_273_0, % 25.55/4.24 | | | | | | | | | | all_273_1, all_273_2, all_273_3, all_273_4, % 25.55/4.24 | | | | | | | | | | all_273_5, all_273_6, all_273_7, all_273_8 gives: % 25.55/4.24 | | | | | | | | | | (230) found(all_88_9) = all_273_6 & tb2t(all_273_8) = % 25.55/4.24 | | | | | | | | | | all_273_7 & get1(int, all_88_10, f) = all_273_8 & % 25.55/4.24 | | | | | | | | | | uni(all_273_8) & (all_273_6 = 0 | % 25.55/4.24 | | | | | | | | | | ($lesseq(all_273_4, usN) & $lesseq(f, all_273_4) % 25.55/4.24 | | | | | | | | | | & $lesseq(all_273_5, f) & $lesseq(1, all_273_5) % 25.55/4.24 | | | | | | | | | | & tb2t(all_273_1) = all_273_0 & tb2t(all_273_3) % 25.55/4.24 | | | | | | | | | | = all_273_2 & get1(int, all_88_10, all_273_4) = % 25.55/4.24 | | | | | | | | | | all_273_1 & get1(int, all_88_10, all_273_5) = % 25.55/4.24 | | | | | | | | | | all_273_3 & uni(all_273_1) & uni(all_273_3) & ( % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(all_273_7, all_273_0)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(all_273_2, all_273_7))))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | ALPHA: (230) implies: % 25.55/4.24 | | | | | | | | | | (231) get1(int, all_88_10, f) = all_273_8 % 25.55/4.24 | | | | | | | | | | (232) tb2t(all_273_8) = all_273_7 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | DELTA: instantiating (226) with fresh symbols all_275_0, % 25.55/4.24 | | | | | | | | | | all_275_1, all_275_2, all_275_3, all_275_4, % 25.55/4.24 | | | | | | | | | | all_275_5, all_275_6, all_275_7, all_275_8 gives: % 25.55/4.24 | | | | | | | | | | (233) found(all_88_17) = all_275_6 & tb2t(all_275_8) = % 25.55/4.24 | | | | | | | | | | all_275_7 & get1(int, all_88_18, f) = all_275_8 & % 25.55/4.24 | | | | | | | | | | uni(all_275_8) & (all_275_6 = 0 | % 25.55/4.24 | | | | | | | | | | ($lesseq(all_275_4, usN) & $lesseq(f, all_275_4) % 25.55/4.24 | | | | | | | | | | & $lesseq(all_275_5, f) & $lesseq(1, all_275_5) % 25.55/4.24 | | | | | | | | | | & tb2t(all_275_1) = all_275_0 & tb2t(all_275_3) % 25.55/4.24 | | | | | | | | | | = all_275_2 & get1(int, all_88_18, all_275_4) = % 25.55/4.24 | | | | | | | | | | all_275_1 & get1(int, all_88_18, all_275_5) = % 25.55/4.24 | | | | | | | | | | all_275_3 & uni(all_275_1) & uni(all_275_3) & ( % 25.55/4.24 | | | | | | | | | | ~ ($lesseq(all_275_7, all_275_0)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(all_275_2, all_275_7))))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | ALPHA: (233) implies: % 25.55/4.24 | | | | | | | | | | (234) get1(int, all_88_18, f) = all_275_8 % 25.55/4.24 | | | | | | | | | | (235) tb2t(all_275_8) = all_275_7 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | DELTA: instantiating (229) with fresh symbols all_277_0, % 25.55/4.24 | | | | | | | | | | all_277_1, all_277_2 gives: % 25.55/4.24 | | | | | | | | | | (236) found(all_88_9) = all_277_2 & tb2t(all_277_1) = % 25.55/4.24 | | | | | | | | | | all_277_0 & get1(int, all_88_10, f) = all_277_1 & % 25.55/4.24 | | | | | | | | | | uni(all_277_1) & ( ~ (all_277_2 = 0) | ( ! [v0: % 25.55/4.24 | | | | | | | | | | int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: uni] : ! [v5: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(all_277_0, v5))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v1, usN)) | ~ ($lesseq(f, v1)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v0, f)) | ~ ($lesseq(1, v0)) | ~ % 25.55/4.24 | | | | | | | | | | (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v1) = v4) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v0) = v2)) & ! [v0: % 25.55/4.24 | | | | | | | | | | int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: uni] : ! [v5: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(v3, all_277_0))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v1, usN)) | ~ ($lesseq(f, v1)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v0, f)) | ~ ($lesseq(1, v0)) | ~ % 25.55/4.24 | | | | | | | | | | (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v1) = v4) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_10, v0) = v2)))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | ALPHA: (236) implies: % 25.55/4.24 | | | | | | | | | | (237) get1(int, all_88_10, f) = all_277_1 % 25.55/4.24 | | | | | | | | | | (238) tb2t(all_277_1) = all_277_0 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | DELTA: instantiating (227) with fresh symbols all_279_0, % 25.55/4.24 | | | | | | | | | | all_279_1, all_279_2 gives: % 25.55/4.24 | | | | | | | | | | (239) found(all_88_17) = all_279_2 & tb2t(all_279_1) = % 25.55/4.24 | | | | | | | | | | all_279_0 & get1(int, all_88_18, f) = all_279_1 & % 25.55/4.24 | | | | | | | | | | uni(all_279_1) & ( ~ (all_279_2 = 0) | ( ! [v0: % 25.55/4.24 | | | | | | | | | | int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: uni] : ! [v5: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(all_279_0, v5))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v1, usN)) | ~ ($lesseq(f, v1)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v0, f)) | ~ ($lesseq(1, v0)) | ~ % 25.55/4.24 | | | | | | | | | | (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v1) = v4) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v0) = v2)) & ! [v0: % 25.55/4.24 | | | | | | | | | | int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 25.55/4.24 | | | | | | | | | | int] : ! [v4: uni] : ! [v5: int] : ( ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(1, $difference(v3, all_279_0))) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v1, usN)) | ~ ($lesseq(f, v1)) | ~ % 25.55/4.24 | | | | | | | | | | ($lesseq(v0, f)) | ~ ($lesseq(1, v0)) | ~ % 25.55/4.24 | | | | | | | | | | (tb2t(v4) = v5) | ~ (tb2t(v2) = v3) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v1) = v4) | ~ % 25.55/4.24 | | | | | | | | | | (get1(int, all_88_18, v0) = v2)))) % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | ALPHA: (239) implies: % 25.55/4.24 | | | | | | | | | | (240) get1(int, all_88_18, f) = all_279_1 % 25.55/4.24 | | | | | | | | | | (241) tb2t(all_279_1) = all_279_0 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (26) with all_275_8, all_279_1, f, % 25.55/4.24 | | | | | | | | | | all_88_18, int, simplifying with (234), (240) % 25.55/4.24 | | | | | | | | | | gives: % 25.55/4.24 | | | | | | | | | | (242) all_279_1 = all_275_8 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (26) with all_88_16, all_279_1, f, % 25.55/4.24 | | | | | | | | | | all_88_18, int, simplifying with (222), (240) % 25.55/4.24 | | | | | | | | | | gives: % 25.55/4.24 | | | | | | | | | | (243) all_279_1 = all_88_16 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (26) with all_181_0, all_273_8, f, % 25.55/4.24 | | | | | | | | | | all_88_10, int, simplifying with (190), (231) % 25.55/4.24 | | | | | | | | | | gives: % 25.55/4.24 | | | | | | | | | | (244) all_273_8 = all_181_0 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (26) with all_273_8, all_277_1, f, % 25.55/4.24 | | | | | | | | | | all_88_10, int, simplifying with (231), (237) % 25.55/4.24 | | | | | | | | | | gives: % 25.55/4.24 | | | | | | | | | | (245) all_277_1 = all_273_8 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (26) with all_88_2, all_277_1, f, % 25.55/4.24 | | | | | | | | | | all_88_10, int, simplifying with (224), (237) % 25.55/4.24 | | | | | | | | | | gives: % 25.55/4.24 | | | | | | | | | | (246) all_277_1 = all_88_2 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | GROUND_INST: instantiating (20) with all_88_16, all_181_0, % 25.55/4.24 | | | | | | | | | | all_88_15, simplifying with (75), (225) gives: % 25.55/4.24 | | | | | | | | | | (247) all_181_0 = all_88_16 % 25.55/4.24 | | | | | | | | | | % 25.55/4.24 | | | | | | | | | | COMBINE_EQS: (242), (243) imply: % 25.55/4.24 | | | | | | | | | | (248) all_275_8 = all_88_16 % 25.55/4.24 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (248) implies: % 25.55/4.25 | | | | | | | | | | (249) all_275_8 = all_88_16 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (245), (246) imply: % 25.55/4.25 | | | | | | | | | | (250) all_273_8 = all_88_2 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (250) implies: % 25.55/4.25 | | | | | | | | | | (251) all_273_8 = all_88_2 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (244), (251) imply: % 25.55/4.25 | | | | | | | | | | (252) all_181_0 = all_88_2 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (247), (252) imply: % 25.55/4.25 | | | | | | | | | | (253) all_88_2 = all_88_16 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (244), (247) imply: % 25.55/4.25 | | | | | | | | | | (254) all_273_8 = all_88_16 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (246), (253) imply: % 25.55/4.25 | | | | | | | | | | (255) all_277_1 = all_88_16 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (241), (243) imply: % 25.55/4.25 | | | | | | | | | | (256) tb2t(all_88_16) = all_279_0 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (238), (255) imply: % 25.55/4.25 | | | | | | | | | | (257) tb2t(all_88_16) = all_277_0 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (235), (249) imply: % 25.55/4.25 | | | | | | | | | | (258) tb2t(all_88_16) = all_275_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (232), (254) imply: % 25.55/4.25 | | | | | | | | | | (259) tb2t(all_88_16) = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (53), (253) imply: % 25.55/4.25 | | | | | | | | | | (260) tb2t(all_88_16) = all_88_1 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | GROUND_INST: instantiating (21) with all_88_1, all_275_7, % 25.55/4.25 | | | | | | | | | | all_88_16, simplifying with (258), (260) gives: % 25.55/4.25 | | | | | | | | | | (261) all_275_7 = all_88_1 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | GROUND_INST: instantiating (21) with all_88_15, all_277_0, % 25.55/4.25 | | | | | | | | | | all_88_16, simplifying with (52), (257) gives: % 25.55/4.25 | | | | | | | | | | (262) all_277_0 = all_88_15 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | GROUND_INST: instantiating (21) with all_275_7, all_277_0, % 25.55/4.25 | | | | | | | | | | all_88_16, simplifying with (257), (258) gives: % 25.55/4.25 | | | | | | | | | | (263) all_277_0 = all_275_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | GROUND_INST: instantiating (21) with all_277_0, all_279_0, % 25.55/4.25 | | | | | | | | | | all_88_16, simplifying with (256), (257) gives: % 25.55/4.25 | | | | | | | | | | (264) all_279_0 = all_277_0 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | GROUND_INST: instantiating (21) with all_273_7, all_279_0, % 25.55/4.25 | | | | | | | | | | all_88_16, simplifying with (256), (259) gives: % 25.55/4.25 | | | | | | | | | | (265) all_279_0 = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (264), (265) imply: % 25.55/4.25 | | | | | | | | | | (266) all_277_0 = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (266) implies: % 25.55/4.25 | | | | | | | | | | (267) all_277_0 = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (263), (267) imply: % 25.55/4.25 | | | | | | | | | | (268) all_275_7 = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (268) implies: % 25.55/4.25 | | | | | | | | | | (269) all_275_7 = all_273_7 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (262), (267) imply: % 25.55/4.25 | | | | | | | | | | (270) all_273_7 = all_88_15 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (261), (269) imply: % 25.55/4.25 | | | | | | | | | | (271) all_273_7 = all_88_1 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (271) implies: % 25.55/4.25 | | | | | | | | | | (272) all_273_7 = all_88_1 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | COMBINE_EQS: (270), (272) imply: % 25.55/4.25 | | | | | | | | | | (273) all_88_1 = all_88_15 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | SIMP: (273) implies: % 25.55/4.25 | | | | | | | | | | (274) all_88_1 = all_88_15 % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | REDUCE: (33), (274) imply: % 25.55/4.25 | | | | | | | | | | (275) $false % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | | CLOSE: (275) is inconsistent. % 25.55/4.25 | | | | | | | | | | % 25.55/4.25 | | | | | | | | | End of split % 25.55/4.25 | | | | | | | | | % 25.55/4.25 | | | | | | | | End of split % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | End of split % 25.55/4.25 | | | | | | | % 25.55/4.25 | | | | | | Case 2: % 25.55/4.25 | | | | | | | % 25.55/4.25 | | | | | | | (276) all_88_0 = 0 | ? [v0: uni] : ? [v1: uni] : ? [v2: int] % 25.55/4.25 | | | | | | | : ( ~ (v2 = all_88_15) & t2tb1(all_88_9) = v0 & tb2t(v1) % 25.55/4.25 | | | | | | | = v2 & get1(int, v0, f) = v1 & uni(v1) & uni(v0)) % 25.55/4.25 | | | | | | | % 25.55/4.25 | | | | | | | BETA: splitting (276) gives: % 25.55/4.25 | | | | | | | % 25.55/4.25 | | | | | | | Case 1: % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | (277) all_88_0 = 0 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | REDUCE: (31), (277) imply: % 25.55/4.25 | | | | | | | | (278) $false % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | CLOSE: (278) is inconsistent. % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | Case 2: % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | (279) ? [v0: uni] : ? [v1: uni] : ? [v2: int] : ( ~ (v2 = % 25.55/4.25 | | | | | | | | all_88_15) & t2tb1(all_88_9) = v0 & tb2t(v1) = v2 & % 25.55/4.25 | | | | | | | | get1(int, v0, f) = v1 & uni(v1) & uni(v0)) % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | DELTA: instantiating (279) with fresh symbols all_210_0, % 25.55/4.25 | | | | | | | | all_210_1, all_210_2 gives: % 25.55/4.25 | | | | | | | | (280) ~ (all_210_0 = all_88_15) & t2tb1(all_88_9) = % 25.55/4.25 | | | | | | | | all_210_2 & tb2t(all_210_1) = all_210_0 & get1(int, % 25.55/4.25 | | | | | | | | all_210_2, f) = all_210_1 & uni(all_210_1) & % 25.55/4.25 | | | | | | | | uni(all_210_2) % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | ALPHA: (280) implies: % 25.55/4.25 | | | | | | | | (281) ~ (all_210_0 = all_88_15) % 25.55/4.25 | | | | | | | | (282) get1(int, all_210_2, f) = all_210_1 % 25.55/4.25 | | | | | | | | (283) tb2t(all_210_1) = all_210_0 % 25.55/4.25 | | | | | | | | (284) t2tb1(all_88_9) = all_210_2 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | GROUND_INST: instantiating (26) with all_181_0, all_188_0, f, % 25.55/4.25 | | | | | | | | all_88_10, int, simplifying with (189), (190) % 25.55/4.25 | | | | | | | | gives: % 25.55/4.25 | | | | | | | | (285) all_188_0 = all_181_0 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | GROUND_INST: instantiating (22) with all_88_10, all_210_2, % 25.55/4.25 | | | | | | | | all_88_9, simplifying with (79), (284) gives: % 25.55/4.25 | | | | | | | | (286) all_210_2 = all_88_10 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | REDUCE: (151), (285) imply: % 25.55/4.25 | | | | | | | | (287) tb2t(all_181_0) = all_88_15 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | REDUCE: (282), (286) imply: % 25.55/4.25 | | | | | | | | (288) get1(int, all_88_10, f) = all_210_1 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | GROUND_INST: instantiating (26) with all_181_0, all_210_1, f, % 25.55/4.25 | | | | | | | | all_88_10, int, simplifying with (190), (288) % 25.55/4.25 | | | | | | | | gives: % 25.55/4.25 | | | | | | | | (289) all_210_1 = all_181_0 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | REDUCE: (283), (289) imply: % 25.55/4.25 | | | | | | | | (290) tb2t(all_181_0) = all_210_0 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | GROUND_INST: instantiating (21) with all_88_15, all_210_0, % 25.55/4.25 | | | | | | | | all_181_0, simplifying with (287), (290) gives: % 25.55/4.25 | | | | | | | | (291) all_210_0 = all_88_15 % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | REDUCE: (281), (291) imply: % 25.55/4.25 | | | | | | | | (292) $false % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | | CLOSE: (292) is inconsistent. % 25.55/4.25 | | | | | | | | % 25.55/4.25 | | | | | | | End of split % 25.55/4.25 | | | | | | | % 25.55/4.25 | | | | | | End of split % 25.55/4.25 | | | | | | % 25.55/4.25 | | | | | End of split % 25.55/4.25 | | | | | % 25.55/4.25 | | | | End of split % 25.55/4.25 | | | | % 25.55/4.25 | | | End of split % 25.55/4.25 | | | % 25.55/4.25 | | Case 2: % 25.55/4.25 | | | % 25.55/4.25 | | | (293) all_88_0 = 0 % 25.55/4.25 | | | % 25.55/4.25 | | | REDUCE: (31), (293) imply: % 25.55/4.25 | | | (294) $false % 25.55/4.25 | | | % 25.55/4.25 | | | CLOSE: (294) is inconsistent. % 25.55/4.25 | | | % 25.55/4.25 | | End of split % 25.55/4.25 | | % 25.55/4.25 | End of split % 25.55/4.25 | % 25.55/4.25 End of proof % 25.55/4.25 % SZS output end Proof for theBenchmark % 25.55/4.25 % 25.55/4.25 3648ms %------------------------------------------------------------------------------