%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ARI750_1 : TPTP v8.1.2. Released v7.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 17:49:01 EDT 2023 % Result : Unsatisfiable 29.22s 4.56s % Output : Proof 42.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ARI750_1 : TPTP v8.1.2. Released v7.0.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Aug 29 19:07:11 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.48/0.62 Running up to 7 provers in parallel. % 0.48/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.48/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.48/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.48/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.48/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.48/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.48/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.29/1.02 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.02 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.02 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.03 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.03 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.04 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 2.29/1.04 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 7.96/1.85 Prover 3: Preprocessing ... % 8.87/1.94 Prover 5: Preprocessing ... % 8.87/1.95 Prover 6: Preprocessing ... % 8.87/1.97 Prover 4: Preprocessing ... % 8.87/1.98 Prover 0: Preprocessing ... % 9.49/2.00 Prover 1: Preprocessing ... % 9.49/2.01 Prover 2: Preprocessing ... % 24.10/3.96 Prover 1: Warning: ignoring some quantifiers % 25.27/4.03 Prover 4: Warning: ignoring some quantifiers % 25.27/4.08 Prover 1: Constructing countermodel ... % 25.88/4.11 Prover 6: Proving ... % 25.88/4.13 Prover 3: Warning: ignoring some quantifiers % 25.88/4.14 Prover 4: Constructing countermodel ... % 25.88/4.16 Prover 3: Constructing countermodel ... % 25.88/4.23 Prover 0: Proving ... % 29.22/4.55 Prover 2: Constructing countermodel ... % 29.22/4.56 Prover 2: proved (3925ms) % 29.22/4.56 % 29.22/4.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.22/4.56 % 29.22/4.56 Prover 6: stopped % 29.22/4.57 Prover 3: stopped % 29.22/4.58 Prover 0: stopped % 29.53/4.59 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.53/4.59 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.53/4.59 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.53/4.59 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 29.53/4.59 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 29.53/4.59 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 29.53/4.59 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 29.53/4.60 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 29.92/4.64 Prover 5: Constructing countermodel ... % 29.92/4.64 Prover 5: stopped % 29.99/4.65 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 29.99/4.66 Prover 13: Warning: Problem contains reals, using incomplete axiomatisation % 33.78/5.14 Prover 8: Preprocessing ... % 34.17/5.21 Prover 7: Preprocessing ... % 34.17/5.22 Prover 10: Preprocessing ... % 34.17/5.23 Prover 13: Preprocessing ... % 34.69/5.27 Prover 11: Preprocessing ... % 38.93/5.85 Prover 1: Found proof (size 92) % 38.93/5.85 Prover 1: proved (5219ms) % 38.93/5.85 Prover 11: stopped % 38.93/5.85 Prover 4: stopped % 39.75/5.93 Prover 13: stopped % 40.38/6.08 Prover 10: Warning: ignoring some quantifiers % 40.96/6.10 Prover 8: Warning: ignoring some quantifiers % 40.96/6.14 Prover 7: Warning: ignoring some quantifiers % 40.96/6.15 Prover 10: Constructing countermodel ... % 40.96/6.15 Prover 10: stopped % 40.96/6.17 Prover 8: Constructing countermodel ... % 40.96/6.18 Prover 8: stopped % 40.96/6.19 Prover 7: Constructing countermodel ... % 40.96/6.19 Prover 7: stopped % 40.96/6.19 % 40.96/6.20 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.96/6.20 % 40.96/6.21 % SZS output start Proof for theBenchmark % 40.96/6.22 Assumptions after simplification: % 40.96/6.22 --------------------------------- % 40.96/6.22 % 40.96/6.22 (formula_133) % 40.96/6.23 c_type(bitvector) & c_type(T) & ? [v0: c_type] : (pointer(T) = v0 & % 40.96/6.23 c_type(v0) & ? [v1: c_unsorted] : ( ~ c_unsorted(v1) | ? [v2: c_sorted] : % 40.96/6.23 (c_sort(v0, v1) = v2 & c_sorted(v2) & ? [v3: c_unsorted] : ? [v4: % 40.96/6.23 c_sorted] : ? [v5: c_unsorted] : (bitvector_of_T(v2) = v3 & % 40.96/6.23 T_of_bitvector(v4) = v5 & c_sort(v0, v5) = v2 & c_sort(bitvector, v3) % 40.96/6.23 = v4 & c_unsorted(v5) & c_unsorted(v3) & c_sorted(v4))))) % 40.96/6.23 % 40.96/6.23 (formula_134) % 40.96/6.24 c_type(T) & c_type(c_unit) & ? [v0: c_type] : ? [v1: c_type] : (pointer(T) = % 40.96/6.24 v0 & pointer(c_unit) = v1 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : % 40.96/6.24 ( ~ c_unsorted(v2) | ? [v3: c_sorted] : (c_sort(v0, v2) = v3 & c_sorted(v3) % 40.96/6.24 & ? [v4: c_unsorted] : ? [v5: c_sorted] : ? [v6: c_unsorted] : % 40.96/6.24 (pointer_address(v3) = v4 & T_of_pointer_address(v5) = v6 & c_sort(v1, % 40.96/6.24 v4) = v5 & c_sort(v0, v6) = v3 & c_unsorted(v6) & c_unsorted(v4) & % 40.96/6.24 c_sorted(v5))))) % 40.96/6.24 % 40.96/6.24 (formula_136) % 41.72/6.24 c_type(T) & c_unsorted(T_tag) & ? [v0: c_type] : ? [v1: c_type] : ? [v2: % 41.72/6.24 c_type] : ? [v3: c_sorted] : (tag_table(T) = v0 & tag_id(T) = v2 & % 41.72/6.24 pointer(T) = v1 & c_sort(v2, T_tag) = v3 & c_type(v2) & c_type(v1) & % 41.72/6.24 c_type(v0) & c_sorted(v3) & ! [v4: c_unsorted] : ! [v5: c_unsorted] : ! % 41.72/6.24 [v6: c_sorted] : ! [v7: c_sorted] : ! [v8: int] : (v8 = 0 | ~ % 41.72/6.24 (instanceof(v6, v7, v3) = v8) | ~ (c_sort(v1, v4) = v7) | ~ (c_sort(v0, % 41.72/6.24 v5) = v6) | ~ c_unsorted(v5) | ~ c_unsorted(v4))) % 41.72/6.24 % 41.72/6.24 (formula_137) % 41.72/6.24 c_type(bitvector) & c_type(T) & ? [v0: c_type] : (pointer(T) = v0 & % 41.72/6.24 c_type(v0) & ! [v1: c_unsorted] : ! [v2: c_sorted] : ( ~ % 41.72/6.24 (c_sort(bitvector, v1) = v2) | ~ c_unsorted(v1) | ? [v3: c_unsorted] : % 41.72/6.24 ? [v4: c_sorted] : ? [v5: c_unsorted] : (bitvector_of_T(v4) = v5 & % 41.72/6.24 T_of_bitvector(v2) = v3 & c_sort(v0, v3) = v4 & c_sort(bitvector, v5) = % 41.72/6.24 v2 & c_unsorted(v5) & c_unsorted(v3) & c_sorted(v4) & c_sorted(v2)))) % 41.72/6.24 % 41.72/6.24 (formula_155) % 41.72/6.24 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.72/6.24 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ! [v3: % 41.72/6.24 c_unsorted] : ! [v4: c_unsorted] : ! [v5: c_sorted] : ! [v6: c_sorted] % 41.72/6.24 : ( ~ (c_sort(v1, v4) = v6) | ~ (c_sort(v0, v3) = v5) | ~ c_unsorted(v4) | % 41.72/6.24 ~ c_unsorted(v3) | ? [v7: any] : ? [v8: int] : (left_valid_struct_T(v5, % 41.72/6.24 v2, v6) = v7 & offset_min(v6, v5) = v8 & c_sorted(v6) & c_sorted(v5) & % 41.72/6.24 ( ~ (v7 = 0) | ~ ($lesseq(1, $difference(v8, v2)))) & (v7 = 0 | ~ % 41.72/6.24 ($lesseq(v8, v2)))))) % 41.72/6.24 % 41.72/6.24 (formula_158) % 41.72/6.25 c_type(T) & c_type(c_unit) & ? [v0: c_type] : ? [v1: c_type] : (pointer(T) = % 41.72/6.25 v1 & pointer(c_unit) = v0 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : % 41.72/6.25 ( ~ c_unsorted(v2) | ? [v3: c_sorted] : (c_sort(v0, v2) = v3 & c_sorted(v3) % 41.72/6.25 & ? [v4: c_unsorted] : ? [v5: c_sorted] : ? [v6: c_unsorted] : % 41.72/6.25 (pointer_address(v5) = v6 & T_of_pointer_address(v3) = v4 & c_sort(v1, % 41.72/6.25 v4) = v5 & c_sort(v0, v6) = v3 & c_unsorted(v6) & c_unsorted(v4) & % 41.72/6.25 c_sorted(v5))))) % 41.72/6.25 % 41.72/6.25 (formula_161) % 41.76/6.25 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.76/6.25 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ! [v3: % 41.76/6.25 c_unsorted] : ! [v4: c_unsorted] : ! [v5: c_sorted] : ! [v6: c_sorted] % 41.76/6.25 : ( ~ (c_sort(v1, v4) = v6) | ~ (c_sort(v0, v3) = v5) | ~ c_unsorted(v4) | % 41.76/6.25 ~ c_unsorted(v3) | ? [v7: any] : ? [v8: int] : % 41.76/6.25 (right_valid_struct_T(v5, v2, v6) = v7 & offset_max(v6, v5) = v8 & % 41.76/6.25 c_sorted(v6) & c_sorted(v5) & ( ~ (v7 = 0) | ~ ($lesseq(1, % 41.76/6.25 $difference(v2, v8)))) & (v7 = 0 | ~ ($lesseq(v2, v8)))))) % 41.76/6.25 % 41.76/6.25 (formula_164) % 41.76/6.25 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.76/6.25 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 41.76/6.25 [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 41.76/6.25 c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | ~ % 41.76/6.25 c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] : ? % 41.76/6.25 [v10: int] : (strict_valid_root_T(v6, v2, v3, v7) = v8 & offset_min(v7, % 41.76/6.25 v6) = v9 & offset_max(v7, v6) = v10 & c_sorted(v7) & c_sorted(v6) & ( % 41.76/6.25 ~ (v10 = v3) | ~ (v9 = v2) | v8 = 0) & ( ~ (v8 = 0) | (v10 = v3 & v9 % 41.76/6.25 = v2))))) % 41.76/6.25 % 41.76/6.25 (formula_167) % 41.76/6.25 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.76/6.25 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 41.76/6.25 [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 41.76/6.25 c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | ~ % 41.76/6.25 c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] : ? % 41.76/6.25 [v10: int] : (strict_valid_struct_T(v6, v2, v3, v7) = v8 & offset_min(v7, % 41.76/6.25 v6) = v9 & offset_max(v7, v6) = v10 & c_sorted(v7) & c_sorted(v6) & ( % 41.76/6.25 ~ (v10 = v3) | ~ (v9 = v2) | v8 = 0) & ( ~ (v8 = 0) | (v10 = v3 & v9 % 41.76/6.25 = v2))))) % 41.76/6.25 % 41.76/6.25 (formula_173) % 41.76/6.25 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.76/6.25 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 41.76/6.25 [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 41.76/6.25 c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | ~ % 41.76/6.25 c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] : ? % 41.76/6.25 [v10: int] : (valid_root_T(v6, v2, v3, v7) = v8 & offset_min(v7, v6) = v9 % 41.76/6.25 & offset_max(v7, v6) = v10 & c_sorted(v7) & c_sorted(v6) & ( ~ (v8 = 0) % 41.76/6.25 | ($lesseq(v3, v10) & $lesseq(v9, v2))) & (v8 = 0 | ~ ($lesseq(v3, % 41.76/6.25 v10)) | ~ ($lesseq(v9, v2)))))) % 41.76/6.25 % 41.76/6.25 (formula_176) % 41.76/6.26 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & % 41.76/6.26 pointer(T) = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 41.76/6.26 [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 41.76/6.26 c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | ~ % 41.76/6.26 c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] : ? % 41.76/6.26 [v10: int] : (valid_struct_T(v6, v2, v3, v7) = v8 & offset_min(v7, v6) = % 41.76/6.26 v9 & offset_max(v7, v6) = v10 & c_sorted(v7) & c_sorted(v6) & ( ~ (v8 = % 41.76/6.26 0) | ($lesseq(v3, v10) & $lesseq(v9, v2))) & (v8 = 0 | ~ % 41.76/6.26 ($lesseq(v3, v10)) | ~ ($lesseq(v9, v2)))))) % 41.76/6.26 % 41.76/6.26 (formula_184) % 41.76/6.26 c_type(T) & ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v0 & % 41.76/6.26 pointer(T) = v1 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : ? [v3: % 41.76/6.26 c_unsorted] : ? [v4: c_sorted] : ? [v5: c_sorted] : (c_sort(v1, v2) = v5 % 41.76/6.26 & c_sort(v0, v3) = v4 & c_unsorted(v3) & c_unsorted(v2) & c_sorted(v5) & % 41.76/6.26 c_sorted(v4) & ! [v6: int] : ~ (offset_min(v4, v5) = v6))) % 41.76/6.26 % 41.76/6.26 (formula_43) % 41.76/6.26 ! [v0: c_type] : ! [v1: c_unsorted] : ! [v2: c_unsorted] : ! [v3: c_type] % 41.76/6.26 : ! [v4: c_sorted] : ! [v5: c_type] : ! [v6: c_sorted] : ( ~ % 41.76/6.26 (alloc_table(v0) = v3) | ~ (pointer(v0) = v5) | ~ (c_sort(v5, v2) = v6) | % 41.76/6.26 ~ (c_sort(v3, v1) = v4) | ~ c_type(v0) | ~ c_unsorted(v2) | ~ % 41.76/6.26 c_unsorted(v1) | ? [v7: any] : ? [v8: int] : ? [v9: int] : (valid(v4, v6) % 41.76/6.26 = v7 & offset_min(v4, v6) = v8 & offset_max(v4, v6) = v9 & c_sorted(v6) & % 41.76/6.26 c_sorted(v4) & ( ~ (v7 = 0) | ($lesseq(0, v9) & $lesseq(v8, 0))) & (v7 = 0 % 41.76/6.26 | ~ ($lesseq(0, v9)) | ~ ($lesseq(v8, 0)))) % 41.76/6.26 % 41.76/6.26 (function-axioms) % 41.76/6.30 ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : ! [v3: int] : % 41.76/6.30 ! [v4: int] : ! [v5: c_sorted] : ! [v6: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (store_bytes(v6, v5, v4, v3, v2) = v1) | ~ (store_bytes(v6, v5, v4, v3, v2) % 41.76/6.30 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.76/6.30 c_sorted] : ! [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (valid_struct_void_P(v5, v4, v3, v2) = v1) | ~ (valid_struct_void_P(v5, v4, % 41.76/6.30 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 41.76/6.30 : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = % 41.76/6.30 v0 | ~ (valid_struct_char_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_struct_char_P(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : % 41.76/6.30 ! [v5: c_sorted] : (v1 = v0 | ~ (valid_struct_T(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_struct_T(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 41.76/6.30 [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! % 41.76/6.30 [v5: c_sorted] : (v1 = v0 | ~ (valid_root_void_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_root_void_P(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 41.76/6.30 [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! % 41.76/6.30 [v5: c_sorted] : (v1 = v0 | ~ (valid_root_char_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_root_char_P(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 41.76/6.30 [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! % 41.76/6.30 [v5: c_sorted] : (v1 = v0 | ~ (valid_root_T(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_root_T(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! % 41.76/6.30 [v5: c_sorted] : (v1 = v0 | ~ (valid_bitvector_struct_void_P(v5, v4, v3, v2) % 41.76/6.30 = v1) | ~ (valid_bitvector_struct_void_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (valid_bitvector_struct_char_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_bitvector_struct_char_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (valid_bitvector_struct_T(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (valid_bitvector_struct_T(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (strict_valid_struct_void_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (strict_valid_struct_void_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (strict_valid_struct_char_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (strict_valid_struct_char_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (strict_valid_struct_T(v5, v4, v3, v2) = v1) | ~ (strict_valid_struct_T(v5, % 41.76/6.30 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: int] : ! % 41.76/6.30 [v5: c_sorted] : (v1 = v0 | ~ (strict_valid_root_void_P(v5, v4, v3, v2) = v1) % 41.76/6.30 | ~ (strict_valid_root_void_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (strict_valid_root_char_P(v5, v4, v3, v2) = v1) | ~ % 41.76/6.30 (strict_valid_root_char_P(v5, v4, v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (strict_valid_root_T(v5, v4, v3, v2) = v1) | ~ (strict_valid_root_T(v5, v4, % 41.76/6.30 v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: % 41.76/6.30 int] : ! [v3: int] : ! [v4: c_sorted] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (select_bytes(v5, v4, v3, v2) = v1) | ~ (select_bytes(v5, v4, v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: int] : ! [v4: int] : ! [v5: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (replace_bytes(v5, v4, v3, v2) = v1) | ~ (replace_bytes(v5, v4, v3, v2) = % 41.76/6.30 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.76/6.30 c_sorted] : ! [v3: c_sorted] : ! [v4: c_sorted] : ! [v5: c_sorted] : (v1 % 41.76/6.30 = v0 | ~ (not_assigns(v5, v4, v3, v2) = v1) | ~ (not_assigns(v5, v4, v3, % 41.76/6.30 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 41.76/6.30 ! [v2: c_sorted] : ! [v3: int] : ! [v4: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (right_valid_struct_void_P(v4, v3, v2) = v1) | ~ % 41.76/6.30 (right_valid_struct_void_P(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (right_valid_struct_char_P(v4, v3, v2) = v1) | ~ % 41.76/6.30 (right_valid_struct_char_P(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (right_valid_struct_T(v4, v3, v2) = v1) | ~ % 41.76/6.30 (right_valid_struct_T(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 41.76/6.30 [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: c_sorted] % 41.76/6.30 : (v1 = v0 | ~ (left_valid_struct_void_P(v4, v3, v2) = v1) | ~ % 41.76/6.30 (left_valid_struct_void_P(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (left_valid_struct_char_P(v4, v3, v2) = v1) | ~ % 41.76/6.30 (left_valid_struct_char_P(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: int] : ! [v4: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (left_valid_struct_T(v4, v3, v2) = v1) | ~ % 41.76/6.30 (left_valid_struct_T(v4, v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: int] : ! [v3: int] : ! [v4: c_sorted] : (v1 = v0 | % 41.76/6.30 ~ (extract_bytes(v4, v3, v2) = v1) | ~ (extract_bytes(v4, v3, v2) = v0)) & % 41.76/6.30 ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: c_sorted] : ! [v4: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (offset_max_bytes(v4, v3, v2) = v1) | ~ % 41.76/6.30 (offset_max_bytes(v4, v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 41.76/6.30 int] : ! [v3: c_sorted] : ! [v4: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (offset_min_bytes(v4, v3, v2) = v1) | ~ (offset_min_bytes(v4, v3, v2) = % 41.76/6.30 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.76/6.30 c_sorted] : ! [v3: c_sorted] : ! [v4: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (alloc_extends_except(v4, v3, v2) = v1) | ~ (alloc_extends_except(v4, v3, % 41.76/6.30 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 41.76/6.30 ! [v2: int] : ! [v3: c_sorted] : ! [v4: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (alloc_fresh(v4, v3, v2) = v1) | ~ (alloc_fresh(v4, v3, v2) = v0)) & ! % 41.76/6.30 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : ! [v4: c_sorted] : (v1 = v0 | ~ (fully_packed(v4, v3, v2) = % 41.76/6.30 v1) | ~ (fully_packed(v4, v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : ! [v3: c_sorted] : ! [v4: c_sorted] : % 41.76/6.30 (v1 = v0 | ~ (downcast(v4, v3, v2) = v1) | ~ (downcast(v4, v3, v2) = v0)) & % 41.76/6.30 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : % 41.76/6.30 ! [v3: c_sorted] : ! [v4: c_sorted] : (v1 = v0 | ~ (instanceof(v4, v3, v2) = % 41.76/6.30 v1) | ~ (instanceof(v4, v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: int] : ! [v3: int] : ! [v4: c_sorted] : (v1 = v0 | % 41.76/6.30 ~ (pset_range(v4, v3, v2) = v1) | ~ (pset_range(v4, v3, v2) = v0)) & ! % 41.76/6.30 [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : ! [v3: c_sorted] % 41.76/6.30 : ! [v4: c_sorted] : (v1 = v0 | ~ (smtlib__store(v4, v3, v2) = v1) | ~ % 41.76/6.30 (smtlib__store(v4, v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : ! [v3: c_sorted] : ! [v4: c_Boolean] : % 41.76/6.30 (v1 = v0 | ~ (smtlib__ite(v4, v3, v2) = v1) | ~ (smtlib__ite(v4, v3, v2) = % 41.76/6.30 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : % 41.76/6.30 (v1 = v0 | ~ (real_$quotient(v3, v2) = v1) | ~ (real_$quotient(v3, v2) = % 41.76/6.30 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : % 41.76/6.30 (v1 = v0 | ~ (real_$product(v3, v2) = v1) | ~ (real_$product(v3, v2) = v0)) % 41.76/6.30 & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 41.76/6.30 | ~ (real_$difference(v3, v2) = v1) | ~ (real_$difference(v3, v2) = v0)) & % 41.76/6.30 ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | % 41.76/6.30 ~ (real_$sum(v3, v2) = v1) | ~ (real_$sum(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : (v1 = v0 | ~ (eq_int8(v3, v2) = v1) | ~ (eq_int8(v3, v2) = % 41.76/6.30 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.76/6.30 c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ (eq_int32(v3, v2) = v1) | ~ % 41.76/6.30 (eq_int32(v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! % 41.76/6.30 [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ (concat_bitvector(v3, v2) = % 41.76/6.30 v1) | ~ (concat_bitvector(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 41.76/6.30 ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | % 41.76/6.30 ~ (alloc_extends(v3, v2) = v1) | ~ (alloc_extends(v3, v2) = v0)) & ! [v0: % 41.76/6.30 int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (asr(v3, % 41.76/6.30 v2) = v1) | ~ (asr(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 41.76/6.30 [v2: int] : ! [v3: int] : (v1 = v0 | ~ (lsr(v3, v2) = v1) | ~ (lsr(v3, v2) % 41.76/6.30 = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = % 41.76/6.30 v0 | ~ (lsl(v3, v2) = v1) | ~ (lsl(v3, v2) = v0)) & ! [v0: int] : ! [v1: % 41.76/6.30 int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (bw_and(v3, v2) = v1) | % 41.76/6.30 ~ (bw_and(v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! % 41.76/6.30 [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ (typeof(v3, v2) = v1) | ~ % 41.76/6.30 (typeof(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (parenttag(v3, v2) = v1) | ~ (parenttag(v3, v2) = v0)) & ! [v0: c_Boolean] % 41.76/6.30 : ! [v1: c_Boolean] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (subtag_bool(v3, v2) = v1) | ~ (subtag_bool(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : (v1 = v0 | ~ (subtag(v3, v2) = v1) | ~ (subtag(v3, v2) = % 41.76/6.30 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.76/6.30 c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ (full_separated(v3, v2) = v1) % 41.76/6.30 | ~ (full_separated(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (valid_pset(v3, v2) = v1) | ~ (valid_pset(v3, v2) = v0)) & ! [v0: % 41.76/6.30 c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : ! [v3: c_sorted] : % 41.76/6.30 (v1 = v0 | ~ (pset_union(v3, v2) = v1) | ~ (pset_union(v3, v2) = v0)) & ! % 41.76/6.30 [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: int] : ! [v3: c_sorted] : % 41.76/6.30 (v1 = v0 | ~ (pset_range_right(v3, v2) = v1) | ~ (pset_range_right(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: int] : ! [v3: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (pset_range_left(v3, v2) = v1) | ~ % 41.76/6.30 (pset_range_left(v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] % 41.76/6.30 : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ (pset_deref(v3, v2) = % 41.76/6.30 v1) | ~ (pset_deref(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (pset_included(v3, v2) = v1) | ~ (pset_included(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : (v1 = v0 | ~ (pset_disjoint(v3, v2) = v1) | ~ % 41.76/6.30 (pset_disjoint(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (in_pset(v3, v2) = v1) | ~ (in_pset(v3, v2) = v0)) & ! [v0: c_type] : ! % 41.76/6.30 [v1: c_type] : ! [v2: c_type] : ! [v3: c_type] : (v1 = v0 | ~ (memory(v3, % 41.76/6.30 v2) = v1) | ~ (memory(v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (smtlib__select(v3, v2) = v1) | ~ (smtlib__select(v3, v2) = v0)) & ! [v0: % 41.76/6.30 int] : ! [v1: int] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (sub_pointer(v3, v2) = v1) | ~ (sub_pointer(v3, v2) = v0)) & ! [v0: % 41.76/6.30 c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_sorted] : ! [v3: c_sorted] : % 41.76/6.30 (v1 = v0 | ~ (neq_pointer_bool(v3, v2) = v1) | ~ (neq_pointer_bool(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : (v1 = v0 | ~ (eq_pointer_bool(v3, v2) = v1) | ~ % 41.76/6.30 (eq_pointer_bool(v3, v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] % 41.76/6.30 : ! [v2: int] : ! [v3: c_sorted] : (v1 = v0 | ~ (shift(v3, v2) = v1) | ~ % 41.76/6.30 (shift(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (same_block(v3, v2) = v1) | ~ (same_block(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : ! % 41.76/6.30 [v3: c_sorted] : (v1 = v0 | ~ (valid(v3, v2) = v1) | ~ (valid(v3, v2) = v0)) % 41.76/6.30 & ! [v0: int] : ! [v1: int] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = % 41.76/6.30 v0 | ~ (offset_min(v3, v2) = v1) | ~ (offset_min(v3, v2) = v0)) & ! [v0: % 41.76/6.30 int] : ! [v1: int] : ! [v2: c_sorted] : ! [v3: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (offset_max(v3, v2) = v1) | ~ (offset_max(v3, v2) = v0)) & ! [v0: $real] : % 41.76/6.30 ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ (real_min(v3, % 41.76/6.30 v2) = v1) | ~ (real_min(v3, v2) = v0)) & ! [v0: $real] : ! [v1: % 41.76/6.30 $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ (real_max(v3, v2) = % 41.76/6.30 v1) | ~ (real_max(v3, v2) = v0)) & ! [v0: c_Boolean] : ! [v1: % 41.76/6.30 c_Boolean] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 41.76/6.30 (neq_real_bool(v3, v2) = v1) | ~ (neq_real_bool(v3, v2) = v0)) & ! [v0: % 41.76/6.30 c_Boolean] : ! [v1: c_Boolean] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 41.76/6.30 | ~ (eq_real_bool(v3, v2) = v1) | ~ (eq_real_bool(v3, v2) = v0)) & ! [v0: % 41.76/6.30 c_Boolean] : ! [v1: c_Boolean] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 41.76/6.30 | ~ (ge_real_bool(v3, v2) = v1) | ~ (ge_real_bool(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 41.76/6.30 $real] : (v1 = v0 | ~ (real_$greatereq(v3, v2) = v1) | ~ % 41.76/6.30 (real_$greatereq(v3, v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : % 41.76/6.30 ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ (gt_real_bool(v3, v2) = v1) | % 41.76/6.30 ~ (gt_real_bool(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 41.76/6.30 (real_$greater(v3, v2) = v1) | ~ (real_$greater(v3, v2) = v0)) & ! [v0: % 41.76/6.30 c_Boolean] : ! [v1: c_Boolean] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 41.76/6.30 | ~ (le_real_bool(v3, v2) = v1) | ~ (le_real_bool(v3, v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 41.76/6.30 $real] : (v1 = v0 | ~ (real_$lesseq(v3, v2) = v1) | ~ (real_$lesseq(v3, % 41.76/6.30 v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: $real] : % 41.76/6.30 ! [v3: $real] : (v1 = v0 | ~ (lt_real_bool(v3, v2) = v1) | ~ % 41.76/6.30 (lt_real_bool(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.76/6.30 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 41.76/6.30 (real_$less(v3, v2) = v1) | ~ (real_$less(v3, v2) = v0)) & ! [v0: int] : % 41.76/6.30 ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (int_min(v3, v2) = % 41.76/6.30 v1) | ~ (int_min(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 41.76/6.30 int] : ! [v3: int] : (v1 = v0 | ~ (int_max(v3, v2) = v1) | ~ (int_max(v3, % 41.76/6.30 v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! % 41.76/6.30 [v3: int] : (v1 = v0 | ~ (neq_int_bool(v3, v2) = v1) | ~ (neq_int_bool(v3, % 41.76/6.30 v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! % 41.76/6.30 [v3: int] : (v1 = v0 | ~ (eq_int_bool(v3, v2) = v1) | ~ (eq_int_bool(v3, v2) % 41.76/6.30 = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 41.76/6.30 int] : (v1 = v0 | ~ (ge_int_bool(v3, v2) = v1) | ~ (ge_int_bool(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 41.76/6.30 int] : (v1 = v0 | ~ (gt_int_bool(v3, v2) = v1) | ~ (gt_int_bool(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 41.76/6.30 int] : (v1 = v0 | ~ (le_int_bool(v3, v2) = v1) | ~ (le_int_bool(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 41.76/6.30 int] : (v1 = v0 | ~ (lt_int_bool(v3, v2) = v1) | ~ (lt_int_bool(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_Boolean] : ! % 41.76/6.30 [v3: c_Boolean] : (v1 = v0 | ~ (bool_xor(v3, v2) = v1) | ~ (bool_xor(v3, v2) % 41.76/6.30 = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_Boolean] : ! % 41.76/6.30 [v3: c_Boolean] : (v1 = v0 | ~ (bool_or(v3, v2) = v1) | ~ (bool_or(v3, v2) = % 41.76/6.30 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_Boolean] : ! % 41.76/6.30 [v3: c_Boolean] : (v1 = v0 | ~ (bool_and(v3, v2) = v1) | ~ (bool_and(v3, v2) % 41.76/6.30 = v0)) & ! [v0: c_sorted] : ! [v1: c_sorted] : ! [v2: c_unsorted] : ! % 41.76/6.30 [v3: c_type] : (v1 = v0 | ~ (c_sort(v3, v2) = v1) | ~ (c_sort(v3, v2) = v0)) % 41.76/6.30 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : % 41.76/6.30 (v1 = v0 | ~ (real_$is_int(v2) = v1) | ~ (real_$is_int(v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : (v1 = v0 % 41.76/6.30 | ~ (real_$is_rat(v2) = v1) | ~ (real_$is_rat(v2) = v0)) & ! [v0: $real] % 41.76/6.30 : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$floor(v2) = v1) | ~ % 41.76/6.30 (real_$floor(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : % 41.76/6.30 (v1 = v0 | ~ (real_$ceiling(v2) = v1) | ~ (real_$ceiling(v2) = v0)) & ! % 41.76/6.30 [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 41.76/6.30 (real_$truncate(v2) = v1) | ~ (real_$truncate(v2) = v0)) & ! [v0: $real] : % 41.76/6.30 ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$round(v2) = v1) | ~ % 41.76/6.30 (real_$round(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: $real] : (v1 % 41.76/6.30 = v0 | ~ (real_$to_int(v2) = v1) | ~ (real_$to_int(v2) = v0)) & ! [v0: % 41.76/6.30 $rat] : ! [v1: $rat] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_rat(v2) = % 41.76/6.30 v1) | ~ (real_$to_rat(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 41.76/6.30 [v2: $real] : (v1 = v0 | ~ (real_$to_real(v2) = v1) | ~ (real_$to_real(v2) = % 41.76/6.30 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: int] : (v1 = v0 | ~ % 41.76/6.30 (int_$to_real(v2) = v1) | ~ (int_$to_real(v2) = v0)) & ! [v0: c_unsorted] % 41.76/6.30 : ! [v1: c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (void_P_of_pointer_address(v2) = v1) | ~ (void_P_of_pointer_address(v2) = % 41.76/6.30 v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: int] : (v1 = v0 % 41.76/6.30 | ~ (int8_of_integer(v2) = v1) | ~ (int8_of_integer(v2) = v0)) & ! [v0: % 41.76/6.30 c_unsorted] : ! [v1: c_unsorted] : ! [v2: int] : (v1 = v0 | ~ % 41.76/6.30 (int32_of_integer(v2) = v1) | ~ (int32_of_integer(v2) = v0)) & ! [v0: int] % 41.76/6.30 : ! [v1: int] : ! [v2: c_sorted] : (v1 = v0 | ~ (integer_of_int8(v2) = v1) % 41.76/6.30 | ~ (integer_of_int8(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 41.76/6.30 c_sorted] : (v1 = v0 | ~ (integer_of_int32(v2) = v1) | ~ % 41.76/6.30 (integer_of_int32(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : % 41.76/6.30 ! [v2: c_sorted] : (v1 = v0 | ~ (char_P_of_pointer_address(v2) = v1) | ~ % 41.76/6.30 (char_P_of_pointer_address(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (void_P_of_bitvector(v2) = % 41.76/6.30 v1) | ~ (void_P_of_bitvector(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (bitvector_of_void_P(v2) = % 41.76/6.30 v1) | ~ (bitvector_of_void_P(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (int8_of_bitvector(v2) = v1) % 41.76/6.30 | ~ (int8_of_bitvector(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (bitvector_of_int8(v2) = v1) % 41.76/6.30 | ~ (bitvector_of_int8(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (int32_of_bitvector(v2) = % 41.76/6.30 v1) | ~ (int32_of_bitvector(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (bitvector_of_int32(v2) = % 41.76/6.30 v1) | ~ (bitvector_of_int32(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (char_P_of_bitvector(v2) = % 41.76/6.30 v1) | ~ (char_P_of_bitvector(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (bitvector_of_char_P(v2) = % 41.76/6.30 v1) | ~ (bitvector_of_char_P(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: % 41.76/6.30 c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ (pointer_address(v2) = v1) | % 41.76/6.30 ~ (pointer_address(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : % 41.76/6.30 ! [v2: c_sorted] : (v1 = v0 | ~ (T_of_pointer_address(v2) = v1) | ~ % 41.76/6.30 (T_of_pointer_address(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] % 41.76/6.30 : ! [v2: c_sorted] : (v1 = v0 | ~ (bitvector_of_T(v2) = v1) | ~ % 41.76/6.30 (bitvector_of_T(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! % 41.76/6.30 [v2: c_sorted] : (v1 = v0 | ~ (T_of_bitvector(v2) = v1) | ~ % 41.76/6.30 (T_of_bitvector(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: c_sorted] % 41.76/6.30 : (v1 = v0 | ~ (int_of_tag(v2) = v1) | ~ (int_of_tag(v2) = v0)) & ! [v0: % 41.76/6.30 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_sorted] : (v1 = % 41.76/6.30 v0 | ~ (root_tag(v2) = v1) | ~ (root_tag(v2) = v0)) & ! [v0: c_type] : ! % 41.76/6.30 [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ (tag_table(v2) = v1) | ~ % 41.76/6.30 (tag_table(v2) = v0)) & ! [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] % 41.76/6.30 : (v1 = v0 | ~ (tag_id(v2) = v1) | ~ (tag_id(v2) = v0)) & ! [v0: % 41.76/6.30 c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (pset_singleton(v2) = v1) | ~ (pset_singleton(v2) = v0)) & ! [v0: % 41.76/6.30 c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (pset_all(v2) = v1) | ~ (pset_all(v2) = v0)) & ! [v0: c_type] : ! [v1: % 41.76/6.30 c_type] : ! [v2: c_type] : (v1 = v0 | ~ (pset(v2) = v1) | ~ (pset(v2) = % 41.76/6.30 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: c_sorted] : (v1 = v0 | ~ % 41.76/6.30 (address(v2) = v1) | ~ (address(v2) = v0)) & ! [v0: c_type] : ! [v1: % 41.76/6.30 c_type] : ! [v2: c_type] : (v1 = v0 | ~ (block(v2) = v1) | ~ (block(v2) = % 41.76/6.30 v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : (v1 % 41.76/6.30 = v0 | ~ (base_block(v2) = v1) | ~ (base_block(v2) = v0)) & ! [v0: % 41.76/6.30 c_type] : ! [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ (alloc_table(v2) % 41.76/6.30 = v1) | ~ (alloc_table(v2) = v0)) & ! [v0: c_type] : ! [v1: c_type] : % 41.76/6.30 ! [v2: c_type] : (v1 = v0 | ~ (pointer(v2) = v1) | ~ (pointer(v2) = v0)) & % 41.76/6.30 ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (exp(v2) = v1) % 41.76/6.30 | ~ (exp(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : % 41.76/6.30 (v1 = v0 | ~ (log(v2) = v1) | ~ (log(v2) = v0)) & ! [v0: $real] : ! [v1: % 41.76/6.30 $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$uminus(v2) = v1) | ~ % 41.76/6.30 (real_$uminus(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] % 41.76/6.30 : (v1 = v0 | ~ (abs_real(v2) = v1) | ~ (abs_real(v2) = v0)) & ! [v0: int] : % 41.76/6.30 ! [v1: int] : ! [v2: int] : (v1 = v0 | ~ (abs_int(v2) = v1) | ~ % 41.76/6.30 (abs_int(v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: % 41.76/6.30 c_Boolean] : (v1 = v0 | ~ (bool_not(v2) = v1) | ~ (bool_not(v2) = v0)) & % 41.76/6.30 ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: Unit] : (v1 = v0 | ~ % 41.76/6.30 (unit2u(v2) = v1) | ~ (unit2u(v2) = v0)) & ! [v0: Unit] : ! [v1: Unit] : % 41.76/6.30 ! [v2: c_sorted] : (v1 = v0 | ~ (s2unit(v2) = v1) | ~ (s2unit(v2) = v0)) & % 41.76/6.30 ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: $real] : (v1 = v0 | ~ % 41.76/6.30 (real2u(v2) = v1) | ~ (real2u(v2) = v0)) & ! [v0: $real] : ! [v1: $real] % 41.76/6.30 : ! [v2: c_sorted] : (v1 = v0 | ~ (s2real(v2) = v1) | ~ (s2real(v2) = v0)) % 41.76/6.30 & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_Boolean] : (v1 = v0 | % 41.76/6.30 ~ (bool2u(v2) = v1) | ~ (bool2u(v2) = v0)) & ! [v0: c_Boolean] : ! [v1: % 41.76/6.30 c_Boolean] : ! [v2: c_sorted] : (v1 = v0 | ~ (s2bool(v2) = v1) | ~ % 41.76/6.30 (s2bool(v2) = v0)) & ! [v0: c_unsorted] : ! [v1: c_unsorted] : ! [v2: % 41.76/6.30 int] : (v1 = v0 | ~ (int2u(v2) = v1) | ~ (int2u(v2) = v0)) & ! [v0: int] % 41.76/6.30 : ! [v1: int] : ! [v2: c_sorted] : (v1 = v0 | ~ (s2int(v2) = v1) | ~ % 41.76/6.30 (s2int(v2) = v0)) % 41.76/6.30 % 41.76/6.30 Further assumptions not needed in the proof: % 41.76/6.30 -------------------------------------------- % 42.05/6.31 formula_1, formula_10, formula_100, formula_101, formula_102, formula_103, % 42.05/6.31 formula_104, formula_105, formula_106, formula_107, formula_108, formula_109, % 42.05/6.31 formula_11, formula_110, formula_111, formula_112, formula_113, formula_114, % 42.05/6.31 formula_115, formula_116, formula_117, formula_118, formula_119, formula_12, % 42.05/6.31 formula_120, formula_121, formula_122, formula_123, formula_124, formula_125, % 42.05/6.31 formula_126, formula_127, formula_128, formula_129, formula_13, formula_130, % 42.05/6.31 formula_131, formula_132, formula_135, formula_138, formula_139, formula_14, % 42.05/6.31 formula_140, formula_141, formula_142, formula_143, formula_144, formula_145, % 42.05/6.31 formula_146, formula_147, formula_148, formula_149, formula_15, formula_150, % 42.05/6.31 formula_151, formula_152, formula_153, formula_154, formula_156, formula_157, % 42.05/6.31 formula_159, formula_16, formula_160, formula_162, formula_163, formula_165, % 42.05/6.31 formula_166, formula_168, formula_169, formula_17, formula_170, formula_171, % 42.05/6.31 formula_172, formula_174, formula_175, formula_177, formula_178, formula_179, % 42.05/6.31 formula_18, formula_180, formula_181, formula_182, formula_183, formula_19, % 42.05/6.31 formula_2, formula_20, formula_21, formula_22, formula_23, formula_24, % 42.05/6.31 formula_25, formula_26, formula_27, formula_28, formula_29, formula_3, % 42.05/6.31 formula_30, formula_31, formula_32, formula_33, formula_34, formula_35, % 42.05/6.31 formula_36, formula_37, formula_38, formula_39, formula_4, formula_40, % 42.05/6.31 formula_41, formula_42, formula_44, formula_45, formula_46, formula_47, % 42.05/6.31 formula_48, formula_49, formula_5, formula_50, formula_51, formula_52, % 42.05/6.31 formula_53, formula_54, formula_55, formula_56, formula_57, formula_58, % 42.05/6.31 formula_59, formula_6, formula_60, formula_61, formula_62, formula_63, % 42.05/6.31 formula_64, formula_65, formula_66, formula_67, formula_68, formula_69, % 42.05/6.31 formula_7, formula_70, formula_71, formula_72, formula_73, formula_74, % 42.05/6.31 formula_75, formula_76, formula_77, formula_78, formula_79, formula_8, % 42.05/6.31 formula_80, formula_81, formula_82, formula_83, formula_84, formula_85, % 42.05/6.31 formula_86, formula_87, formula_88, formula_89, formula_9, formula_90, % 42.05/6.31 formula_91, formula_92, formula_93, formula_94, formula_95, formula_96, % 42.05/6.31 formula_97, formula_98, formula_99 % 42.05/6.31 % 42.05/6.31 Those formulas are unsatisfiable: % 42.05/6.31 --------------------------------- % 42.05/6.31 % 42.05/6.31 Begin of proof % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_133) implies: % 42.05/6.31 | (1) ? [v0: c_type] : (pointer(T) = v0 & c_type(v0) & ? [v1: c_unsorted] : % 42.05/6.31 | ( ~ c_unsorted(v1) | ? [v2: c_sorted] : (c_sort(v0, v1) = v2 & % 42.05/6.31 | c_sorted(v2) & ? [v3: c_unsorted] : ? [v4: c_sorted] : ? [v5: % 42.05/6.31 | c_unsorted] : (bitvector_of_T(v2) = v3 & T_of_bitvector(v4) = % 42.05/6.31 | v5 & c_sort(v0, v5) = v2 & c_sort(bitvector, v3) = v4 & % 42.05/6.31 | c_unsorted(v5) & c_unsorted(v3) & c_sorted(v4))))) % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_134) implies: % 42.05/6.31 | (2) ? [v0: c_type] : ? [v1: c_type] : (pointer(T) = v0 & pointer(c_unit) % 42.05/6.31 | = v1 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : ( ~ % 42.05/6.31 | c_unsorted(v2) | ? [v3: c_sorted] : (c_sort(v0, v2) = v3 & % 42.05/6.31 | c_sorted(v3) & ? [v4: c_unsorted] : ? [v5: c_sorted] : ? [v6: % 42.05/6.31 | c_unsorted] : (pointer_address(v3) = v4 & % 42.05/6.31 | T_of_pointer_address(v5) = v6 & c_sort(v1, v4) = v5 & % 42.05/6.31 | c_sort(v0, v6) = v3 & c_unsorted(v6) & c_unsorted(v4) & % 42.05/6.31 | c_sorted(v5))))) % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_136) implies: % 42.05/6.31 | (3) ? [v0: c_type] : ? [v1: c_type] : ? [v2: c_type] : ? [v3: c_sorted] % 42.05/6.31 | : (tag_table(T) = v0 & tag_id(T) = v2 & pointer(T) = v1 & c_sort(v2, % 42.05/6.31 | T_tag) = v3 & c_type(v2) & c_type(v1) & c_type(v0) & c_sorted(v3) & % 42.05/6.31 | ! [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! % 42.05/6.31 | [v7: c_sorted] : ! [v8: int] : (v8 = 0 | ~ (instanceof(v6, v7, v3) % 42.05/6.31 | = v8) | ~ (c_sort(v1, v4) = v7) | ~ (c_sort(v0, v5) = v6) | ~ % 42.05/6.31 | c_unsorted(v5) | ~ c_unsorted(v4))) % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_137) implies: % 42.05/6.31 | (4) ? [v0: c_type] : (pointer(T) = v0 & c_type(v0) & ! [v1: c_unsorted] : % 42.05/6.31 | ! [v2: c_sorted] : ( ~ (c_sort(bitvector, v1) = v2) | ~ % 42.05/6.31 | c_unsorted(v1) | ? [v3: c_unsorted] : ? [v4: c_sorted] : ? [v5: % 42.05/6.31 | c_unsorted] : (bitvector_of_T(v4) = v5 & T_of_bitvector(v2) = v3 % 42.05/6.31 | & c_sort(v0, v3) = v4 & c_sort(bitvector, v5) = v2 & % 42.05/6.31 | c_unsorted(v5) & c_unsorted(v3) & c_sorted(v4) & c_sorted(v2)))) % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_155) implies: % 42.05/6.31 | (5) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) = % 42.05/6.31 | v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ! [v3: c_unsorted] : % 42.05/6.31 | ! [v4: c_unsorted] : ! [v5: c_sorted] : ! [v6: c_sorted] : ( ~ % 42.05/6.31 | (c_sort(v1, v4) = v6) | ~ (c_sort(v0, v3) = v5) | ~ % 42.05/6.31 | c_unsorted(v4) | ~ c_unsorted(v3) | ? [v7: any] : ? [v8: int] : % 42.05/6.31 | (left_valid_struct_T(v5, v2, v6) = v7 & offset_min(v6, v5) = v8 & % 42.05/6.31 | c_sorted(v6) & c_sorted(v5) & ( ~ (v7 = 0) | ~ ($lesseq(1, % 42.05/6.31 | $difference(v8, v2)))) & (v7 = 0 | ~ ($lesseq(v8, v2)))))) % 42.05/6.31 | % 42.05/6.31 | ALPHA: (formula_158) implies: % 42.05/6.32 | (6) ? [v0: c_type] : ? [v1: c_type] : (pointer(T) = v1 & pointer(c_unit) % 42.05/6.32 | = v0 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : ( ~ % 42.05/6.32 | c_unsorted(v2) | ? [v3: c_sorted] : (c_sort(v0, v2) = v3 & % 42.05/6.32 | c_sorted(v3) & ? [v4: c_unsorted] : ? [v5: c_sorted] : ? [v6: % 42.05/6.32 | c_unsorted] : (pointer_address(v5) = v6 & % 42.05/6.32 | T_of_pointer_address(v3) = v4 & c_sort(v1, v4) = v5 & % 42.05/6.32 | c_sort(v0, v6) = v3 & c_unsorted(v6) & c_unsorted(v4) & % 42.05/6.32 | c_sorted(v5))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_161) implies: % 42.05/6.32 | (7) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) = % 42.05/6.32 | v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ! [v3: c_unsorted] : % 42.05/6.32 | ! [v4: c_unsorted] : ! [v5: c_sorted] : ! [v6: c_sorted] : ( ~ % 42.05/6.32 | (c_sort(v1, v4) = v6) | ~ (c_sort(v0, v3) = v5) | ~ % 42.05/6.32 | c_unsorted(v4) | ~ c_unsorted(v3) | ? [v7: any] : ? [v8: int] : % 42.05/6.32 | (right_valid_struct_T(v5, v2, v6) = v7 & offset_max(v6, v5) = v8 & % 42.05/6.32 | c_sorted(v6) & c_sorted(v5) & ( ~ (v7 = 0) | ~ ($lesseq(1, % 42.05/6.32 | $difference(v2, v8)))) & (v7 = 0 | ~ ($lesseq(v2, v8)))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_164) implies: % 42.05/6.32 | (8) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) = % 42.05/6.32 | v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! [v4: % 42.05/6.32 | c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 42.05/6.32 | c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | % 42.05/6.32 | ~ c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] % 42.05/6.32 | : ? [v10: int] : (strict_valid_root_T(v6, v2, v3, v7) = v8 & % 42.05/6.32 | offset_min(v7, v6) = v9 & offset_max(v7, v6) = v10 & c_sorted(v7) % 42.05/6.32 | & c_sorted(v6) & ( ~ (v10 = v3) | ~ (v9 = v2) | v8 = 0) & ( ~ % 42.05/6.32 | (v8 = 0) | (v10 = v3 & v9 = v2))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_167) implies: % 42.05/6.32 | (9) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) = % 42.05/6.32 | v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! [v4: % 42.05/6.32 | c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 42.05/6.32 | c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | % 42.05/6.32 | ~ c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: int] % 42.05/6.32 | : ? [v10: int] : (strict_valid_struct_T(v6, v2, v3, v7) = v8 & % 42.05/6.32 | offset_min(v7, v6) = v9 & offset_max(v7, v6) = v10 & c_sorted(v7) % 42.05/6.32 | & c_sorted(v6) & ( ~ (v10 = v3) | ~ (v9 = v2) | v8 = 0) & ( ~ % 42.05/6.32 | (v8 = 0) | (v10 = v3 & v9 = v2))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_173) implies: % 42.05/6.32 | (10) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) % 42.05/6.32 | = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 42.05/6.32 | [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 42.05/6.32 | c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | % 42.05/6.32 | ~ c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: % 42.05/6.32 | int] : ? [v10: int] : (valid_root_T(v6, v2, v3, v7) = v8 & % 42.05/6.32 | offset_min(v7, v6) = v9 & offset_max(v7, v6) = v10 & % 42.05/6.32 | c_sorted(v7) & c_sorted(v6) & ( ~ (v8 = 0) | ($lesseq(v3, v10) & % 42.05/6.32 | $lesseq(v9, v2))) & (v8 = 0 | ~ ($lesseq(v3, v10)) | ~ % 42.05/6.32 | ($lesseq(v9, v2)))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_176) implies: % 42.05/6.32 | (11) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v1 & pointer(T) % 42.05/6.32 | = v0 & c_type(v1) & c_type(v0) & ? [v2: int] : ? [v3: int] : ! % 42.05/6.32 | [v4: c_unsorted] : ! [v5: c_unsorted] : ! [v6: c_sorted] : ! [v7: % 42.05/6.32 | c_sorted] : ( ~ (c_sort(v1, v5) = v7) | ~ (c_sort(v0, v4) = v6) | % 42.05/6.32 | ~ c_unsorted(v5) | ~ c_unsorted(v4) | ? [v8: any] : ? [v9: % 42.05/6.32 | int] : ? [v10: int] : (valid_struct_T(v6, v2, v3, v7) = v8 & % 42.05/6.32 | offset_min(v7, v6) = v9 & offset_max(v7, v6) = v10 & % 42.05/6.32 | c_sorted(v7) & c_sorted(v6) & ( ~ (v8 = 0) | ($lesseq(v3, v10) & % 42.05/6.32 | $lesseq(v9, v2))) & (v8 = 0 | ~ ($lesseq(v3, v10)) | ~ % 42.05/6.32 | ($lesseq(v9, v2)))))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (formula_184) implies: % 42.05/6.32 | (12) c_type(T) % 42.05/6.32 | (13) ? [v0: c_type] : ? [v1: c_type] : (alloc_table(T) = v0 & pointer(T) % 42.05/6.32 | = v1 & c_type(v1) & c_type(v0) & ? [v2: c_unsorted] : ? [v3: % 42.05/6.32 | c_unsorted] : ? [v4: c_sorted] : ? [v5: c_sorted] : (c_sort(v1, % 42.05/6.32 | v2) = v5 & c_sort(v0, v3) = v4 & c_unsorted(v3) & c_unsorted(v2) % 42.05/6.32 | & c_sorted(v5) & c_sorted(v4) & ! [v6: int] : ~ (offset_min(v4, % 42.05/6.32 | v5) = v6))) % 42.05/6.32 | % 42.05/6.32 | ALPHA: (function-axioms) implies: % 42.05/6.32 | (14) ! [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ % 42.05/6.32 | (pointer(v2) = v1) | ~ (pointer(v2) = v0)) % 42.05/6.32 | (15) ! [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ % 42.05/6.32 | (alloc_table(v2) = v1) | ~ (alloc_table(v2) = v0)) % 42.05/6.32 | % 42.05/6.33 | DELTA: instantiating (13) with fresh symbols all_105_0, all_105_1 gives: % 42.05/6.33 | (16) alloc_table(T) = all_105_1 & pointer(T) = all_105_0 & % 42.05/6.33 | c_type(all_105_0) & c_type(all_105_1) & ? [v0: c_unsorted] : ? [v1: % 42.05/6.33 | c_unsorted] : ? [v2: c_sorted] : ? [v3: c_sorted] : % 42.05/6.33 | (c_sort(all_105_0, v0) = v3 & c_sort(all_105_1, v1) = v2 & % 42.05/6.33 | c_unsorted(v1) & c_unsorted(v0) & c_sorted(v3) & c_sorted(v2) & ! % 42.05/6.33 | [v4: int] : ~ (offset_min(v2, v3) = v4)) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (16) implies: % 42.05/6.33 | (17) pointer(T) = all_105_0 % 42.05/6.33 | (18) alloc_table(T) = all_105_1 % 42.05/6.33 | (19) ? [v0: c_unsorted] : ? [v1: c_unsorted] : ? [v2: c_sorted] : ? % 42.05/6.33 | [v3: c_sorted] : (c_sort(all_105_0, v0) = v3 & c_sort(all_105_1, v1) = % 42.05/6.33 | v2 & c_unsorted(v1) & c_unsorted(v0) & c_sorted(v3) & c_sorted(v2) & % 42.05/6.33 | ! [v4: int] : ~ (offset_min(v2, v3) = v4)) % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (4) with fresh symbol all_110_0 gives: % 42.05/6.33 | (20) pointer(T) = all_110_0 & c_type(all_110_0) & ! [v0: c_unsorted] : ! % 42.05/6.33 | [v1: c_sorted] : ( ~ (c_sort(bitvector, v0) = v1) | ~ c_unsorted(v0) % 42.05/6.33 | | ? [v2: c_unsorted] : ? [v3: c_sorted] : ? [v4: c_unsorted] : % 42.05/6.33 | (bitvector_of_T(v3) = v4 & T_of_bitvector(v1) = v2 & % 42.05/6.33 | c_sort(all_110_0, v2) = v3 & c_sort(bitvector, v4) = v1 & % 42.05/6.33 | c_unsorted(v4) & c_unsorted(v2) & c_sorted(v3) & c_sorted(v1))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (20) implies: % 42.05/6.33 | (21) pointer(T) = all_110_0 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (1) with fresh symbol all_118_0 gives: % 42.05/6.33 | (22) pointer(T) = all_118_0 & c_type(all_118_0) & ? [v0: c_unsorted] : ( ~ % 42.05/6.33 | c_unsorted(v0) | ? [v1: c_sorted] : (c_sort(all_118_0, v0) = v1 & % 42.05/6.33 | c_sorted(v1) & ? [v2: c_unsorted] : ? [v3: c_sorted] : ? [v4: % 42.05/6.33 | c_unsorted] : (bitvector_of_T(v1) = v2 & T_of_bitvector(v3) = v4 % 42.05/6.33 | & c_sort(all_118_0, v4) = v1 & c_sort(bitvector, v2) = v3 & % 42.05/6.33 | c_unsorted(v4) & c_unsorted(v2) & c_sorted(v3)))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (22) implies: % 42.05/6.33 | (23) pointer(T) = all_118_0 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (2) with fresh symbols all_126_0, all_126_1 gives: % 42.05/6.33 | (24) pointer(T) = all_126_1 & pointer(c_unit) = all_126_0 & % 42.05/6.33 | c_type(all_126_0) & c_type(all_126_1) & ? [v0: c_unsorted] : ( ~ % 42.05/6.33 | c_unsorted(v0) | ? [v1: c_sorted] : (c_sort(all_126_1, v0) = v1 & % 42.05/6.33 | c_sorted(v1) & ? [v2: c_unsorted] : ? [v3: c_sorted] : ? [v4: % 42.05/6.33 | c_unsorted] : (pointer_address(v1) = v2 & % 42.05/6.33 | T_of_pointer_address(v3) = v4 & c_sort(all_126_0, v2) = v3 & % 42.05/6.33 | c_sort(all_126_1, v4) = v1 & c_unsorted(v4) & c_unsorted(v2) & % 42.05/6.33 | c_sorted(v3)))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (24) implies: % 42.05/6.33 | (25) pointer(T) = all_126_1 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (6) with fresh symbols all_130_0, all_130_1 gives: % 42.05/6.33 | (26) pointer(T) = all_130_0 & pointer(c_unit) = all_130_1 & % 42.05/6.33 | c_type(all_130_0) & c_type(all_130_1) & ? [v0: c_unsorted] : ( ~ % 42.05/6.33 | c_unsorted(v0) | ? [v1: c_sorted] : (c_sort(all_130_1, v0) = v1 & % 42.05/6.33 | c_sorted(v1) & ? [v2: c_unsorted] : ? [v3: c_sorted] : ? [v4: % 42.05/6.33 | c_unsorted] : (pointer_address(v3) = v4 & % 42.05/6.33 | T_of_pointer_address(v1) = v2 & c_sort(all_130_0, v2) = v3 & % 42.05/6.33 | c_sort(all_130_1, v4) = v1 & c_unsorted(v4) & c_unsorted(v2) & % 42.05/6.33 | c_sorted(v3)))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (26) implies: % 42.05/6.33 | (27) pointer(T) = all_130_0 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (3) with fresh symbols all_132_0, all_132_1, all_132_2, % 42.05/6.33 | all_132_3 gives: % 42.05/6.33 | (28) tag_table(T) = all_132_3 & tag_id(T) = all_132_1 & pointer(T) = % 42.05/6.33 | all_132_2 & c_sort(all_132_1, T_tag) = all_132_0 & c_type(all_132_1) & % 42.05/6.33 | c_type(all_132_2) & c_type(all_132_3) & c_sorted(all_132_0) & ! [v0: % 42.05/6.33 | c_unsorted] : ! [v1: c_unsorted] : ! [v2: c_sorted] : ! [v3: % 42.05/6.33 | c_sorted] : ! [v4: int] : (v4 = 0 | ~ (instanceof(v2, v3, % 42.05/6.33 | all_132_0) = v4) | ~ (c_sort(all_132_2, v0) = v3) | ~ % 42.05/6.33 | (c_sort(all_132_3, v1) = v2) | ~ c_unsorted(v1) | ~ % 42.05/6.33 | c_unsorted(v0)) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (28) implies: % 42.05/6.33 | (29) pointer(T) = all_132_2 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (7) with fresh symbols all_175_0, all_175_1 gives: % 42.05/6.33 | (30) alloc_table(T) = all_175_0 & pointer(T) = all_175_1 & % 42.05/6.33 | c_type(all_175_0) & c_type(all_175_1) & ? [v0: int] : ! [v1: % 42.05/6.33 | c_unsorted] : ! [v2: c_unsorted] : ! [v3: c_sorted] : ! [v4: % 42.05/6.33 | c_sorted] : ( ~ (c_sort(all_175_0, v2) = v4) | ~ (c_sort(all_175_1, % 42.05/6.33 | v1) = v3) | ~ c_unsorted(v2) | ~ c_unsorted(v1) | ? [v5: any] % 42.05/6.33 | : ? [v6: int] : (right_valid_struct_T(v3, v0, v4) = v5 & % 42.05/6.33 | offset_max(v4, v3) = v6 & c_sorted(v4) & c_sorted(v3) & ( ~ (v5 = % 42.05/6.33 | 0) | ~ ($lesseq(1, $difference(v0, v6)))) & (v5 = 0 | ~ % 42.05/6.33 | ($lesseq(v0, v6))))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (30) implies: % 42.05/6.33 | (31) pointer(T) = all_175_1 % 42.05/6.33 | (32) alloc_table(T) = all_175_0 % 42.05/6.33 | % 42.05/6.33 | DELTA: instantiating (5) with fresh symbols all_179_0, all_179_1 gives: % 42.05/6.33 | (33) alloc_table(T) = all_179_0 & pointer(T) = all_179_1 & % 42.05/6.33 | c_type(all_179_0) & c_type(all_179_1) & ? [v0: int] : ! [v1: % 42.05/6.33 | c_unsorted] : ! [v2: c_unsorted] : ! [v3: c_sorted] : ! [v4: % 42.05/6.33 | c_sorted] : ( ~ (c_sort(all_179_0, v2) = v4) | ~ (c_sort(all_179_1, % 42.05/6.33 | v1) = v3) | ~ c_unsorted(v2) | ~ c_unsorted(v1) | ? [v5: any] % 42.05/6.33 | : ? [v6: int] : (left_valid_struct_T(v3, v0, v4) = v5 & % 42.05/6.33 | offset_min(v4, v3) = v6 & c_sorted(v4) & c_sorted(v3) & ( ~ (v5 = % 42.05/6.33 | 0) | ~ ($lesseq(1, $difference(v6, v0)))) & (v5 = 0 | ~ % 42.05/6.33 | ($lesseq(v6, v0))))) % 42.05/6.33 | % 42.05/6.33 | ALPHA: (33) implies: % 42.05/6.34 | (34) pointer(T) = all_179_1 % 42.05/6.34 | (35) alloc_table(T) = all_179_0 % 42.05/6.34 | % 42.05/6.34 | DELTA: instantiating (8) with fresh symbols all_209_0, all_209_1 gives: % 42.05/6.34 | (36) alloc_table(T) = all_209_0 & pointer(T) = all_209_1 & % 42.05/6.34 | c_type(all_209_0) & c_type(all_209_1) & ? [v0: int] : ? [v1: int] : % 42.05/6.34 | ! [v2: c_unsorted] : ! [v3: c_unsorted] : ! [v4: c_sorted] : ! [v5: % 42.05/6.34 | c_sorted] : ( ~ (c_sort(all_209_0, v3) = v5) | ~ (c_sort(all_209_1, % 42.05/6.34 | v2) = v4) | ~ c_unsorted(v3) | ~ c_unsorted(v2) | ? [v6: any] % 42.05/6.34 | : ? [v7: int] : ? [v8: int] : (strict_valid_root_T(v4, v0, v1, v5) % 42.05/6.34 | = v6 & offset_min(v5, v4) = v7 & offset_max(v5, v4) = v8 & % 42.05/6.34 | c_sorted(v5) & c_sorted(v4) & ( ~ (v8 = v1) | ~ (v7 = v0) | v6 = % 42.05/6.34 | 0) & ( ~ (v6 = 0) | (v8 = v1 & v7 = v0)))) % 42.05/6.34 | % 42.05/6.34 | ALPHA: (36) implies: % 42.05/6.34 | (37) pointer(T) = all_209_1 % 42.05/6.34 | (38) alloc_table(T) = all_209_0 % 42.05/6.34 | % 42.05/6.34 | DELTA: instantiating (11) with fresh symbols all_219_0, all_219_1 gives: % 42.05/6.34 | (39) alloc_table(T) = all_219_0 & pointer(T) = all_219_1 & % 42.05/6.34 | c_type(all_219_0) & c_type(all_219_1) & ? [v0: int] : ? [v1: int] : % 42.05/6.34 | ! [v2: c_unsorted] : ! [v3: c_unsorted] : ! [v4: c_sorted] : ! [v5: % 42.05/6.34 | c_sorted] : ( ~ (c_sort(all_219_0, v3) = v5) | ~ (c_sort(all_219_1, % 42.05/6.34 | v2) = v4) | ~ c_unsorted(v3) | ~ c_unsorted(v2) | ? [v6: any] % 42.05/6.34 | : ? [v7: int] : ? [v8: int] : (valid_struct_T(v4, v0, v1, v5) = v6 % 42.05/6.34 | & offset_min(v5, v4) = v7 & offset_max(v5, v4) = v8 & c_sorted(v5) % 42.05/6.34 | & c_sorted(v4) & ( ~ (v6 = 0) | ($lesseq(v1, v8) & $lesseq(v7, % 42.05/6.34 | v0))) & (v6 = 0 | ~ ($lesseq(v1, v8)) | ~ ($lesseq(v7, % 42.05/6.34 | v0))))) % 42.05/6.34 | % 42.05/6.34 | ALPHA: (39) implies: % 42.05/6.34 | (40) pointer(T) = all_219_1 % 42.05/6.34 | (41) alloc_table(T) = all_219_0 % 42.05/6.34 | % 42.05/6.34 | DELTA: instantiating (10) with fresh symbols all_221_0, all_221_1 gives: % 42.05/6.34 | (42) alloc_table(T) = all_221_0 & pointer(T) = all_221_1 & % 42.05/6.34 | c_type(all_221_0) & c_type(all_221_1) & ? [v0: int] : ? [v1: int] : % 42.05/6.34 | ! [v2: c_unsorted] : ! [v3: c_unsorted] : ! [v4: c_sorted] : ! [v5: % 42.05/6.34 | c_sorted] : ( ~ (c_sort(all_221_0, v3) = v5) | ~ (c_sort(all_221_1, % 42.05/6.34 | v2) = v4) | ~ c_unsorted(v3) | ~ c_unsorted(v2) | ? [v6: any] % 42.05/6.34 | : ? [v7: int] : ? [v8: int] : (valid_root_T(v4, v0, v1, v5) = v6 & % 42.05/6.34 | offset_min(v5, v4) = v7 & offset_max(v5, v4) = v8 & c_sorted(v5) & % 42.05/6.34 | c_sorted(v4) & ( ~ (v6 = 0) | ($lesseq(v1, v8) & $lesseq(v7, v0))) % 42.05/6.34 | & (v6 = 0 | ~ ($lesseq(v1, v8)) | ~ ($lesseq(v7, v0))))) % 42.05/6.34 | % 42.05/6.34 | ALPHA: (42) implies: % 42.05/6.34 | (43) pointer(T) = all_221_1 % 42.05/6.34 | (44) alloc_table(T) = all_221_0 % 42.05/6.34 | % 42.05/6.34 | DELTA: instantiating (9) with fresh symbols all_225_0, all_225_1 gives: % 42.05/6.34 | (45) alloc_table(T) = all_225_0 & pointer(T) = all_225_1 & % 42.05/6.34 | c_type(all_225_0) & c_type(all_225_1) & ? [v0: int] : ? [v1: int] : % 42.05/6.34 | ! [v2: c_unsorted] : ! [v3: c_unsorted] : ! [v4: c_sorted] : ! [v5: % 42.05/6.34 | c_sorted] : ( ~ (c_sort(all_225_0, v3) = v5) | ~ (c_sort(all_225_1, % 42.05/6.34 | v2) = v4) | ~ c_unsorted(v3) | ~ c_unsorted(v2) | ? [v6: any] % 42.05/6.34 | : ? [v7: int] : ? [v8: int] : (strict_valid_struct_T(v4, v0, v1, % 42.05/6.34 | v5) = v6 & offset_min(v5, v4) = v7 & offset_max(v5, v4) = v8 & % 42.05/6.34 | c_sorted(v5) & c_sorted(v4) & ( ~ (v8 = v1) | ~ (v7 = v0) | v6 = % 42.05/6.34 | 0) & ( ~ (v6 = 0) | (v8 = v1 & v7 = v0)))) % 42.05/6.34 | % 42.05/6.34 | ALPHA: (45) implies: % 42.05/6.34 | (46) pointer(T) = all_225_1 % 42.05/6.34 | (47) alloc_table(T) = all_225_0 % 42.05/6.34 | % 42.05/6.34 | DELTA: instantiating (19) with fresh symbols all_317_0, all_317_1, all_317_2, % 42.05/6.34 | all_317_3 gives: % 42.05/6.34 | (48) c_sort(all_105_0, all_317_3) = all_317_0 & c_sort(all_105_1, % 42.05/6.34 | all_317_2) = all_317_1 & c_unsorted(all_317_2) & % 42.05/6.34 | c_unsorted(all_317_3) & c_sorted(all_317_0) & c_sorted(all_317_1) & ! % 42.05/6.34 | [v0: int] : ~ (offset_min(all_317_1, all_317_0) = v0) % 42.05/6.34 | % 42.05/6.34 | ALPHA: (48) implies: % 42.05/6.34 | (49) c_unsorted(all_317_3) % 42.05/6.34 | (50) c_unsorted(all_317_2) % 42.05/6.34 | (51) c_sort(all_105_1, all_317_2) = all_317_1 % 42.05/6.34 | (52) c_sort(all_105_0, all_317_3) = all_317_0 % 42.05/6.34 | (53) ! [v0: int] : ~ (offset_min(all_317_1, all_317_0) = v0) % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_110_0, all_118_0, T, simplifying with % 42.05/6.34 | (21), (23) gives: % 42.05/6.34 | (54) all_118_0 = all_110_0 % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_118_0, all_130_0, T, simplifying with % 42.05/6.34 | (23), (27) gives: % 42.05/6.34 | (55) all_130_0 = all_118_0 % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_130_0, all_132_2, T, simplifying with % 42.05/6.34 | (27), (29) gives: % 42.05/6.34 | (56) all_132_2 = all_130_0 % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_132_2, all_175_1, T, simplifying with % 42.05/6.34 | (29), (31) gives: % 42.05/6.34 | (57) all_175_1 = all_132_2 % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_130_0, all_179_1, T, simplifying with % 42.05/6.34 | (27), (34) gives: % 42.05/6.34 | (58) all_179_1 = all_130_0 % 42.05/6.34 | % 42.05/6.34 | GROUND_INST: instantiating (14) with all_175_1, all_209_1, T, simplifying with % 42.05/6.34 | (31), (37) gives: % 42.05/6.34 | (59) all_209_1 = all_175_1 % 42.05/6.34 | % 42.05/6.35 | GROUND_INST: instantiating (14) with all_126_1, all_209_1, T, simplifying with % 42.05/6.35 | (25), (37) gives: % 42.05/6.35 | (60) all_209_1 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (14) with all_179_1, all_219_1, T, simplifying with % 42.05/6.35 | (34), (40) gives: % 42.05/6.35 | (61) all_219_1 = all_179_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (14) with all_221_1, all_225_1, T, simplifying with % 42.05/6.35 | (43), (46) gives: % 42.05/6.35 | (62) all_225_1 = all_221_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (14) with all_219_1, all_225_1, T, simplifying with % 42.05/6.35 | (40), (46) gives: % 42.05/6.35 | (63) all_225_1 = all_219_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (14) with all_105_0, all_225_1, T, simplifying with % 42.05/6.35 | (17), (46) gives: % 42.05/6.35 | (64) all_225_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_179_0, all_209_0, T, simplifying with % 42.05/6.35 | (35), (38) gives: % 42.05/6.35 | (65) all_209_0 = all_179_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_105_1, all_209_0, T, simplifying with % 42.05/6.35 | (18), (38) gives: % 42.05/6.35 | (66) all_209_0 = all_105_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_209_0, all_221_0, T, simplifying with % 42.05/6.35 | (38), (44) gives: % 42.05/6.35 | (67) all_221_0 = all_209_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_175_0, all_221_0, T, simplifying with % 42.05/6.35 | (32), (44) gives: % 42.05/6.35 | (68) all_221_0 = all_175_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_221_0, all_225_0, T, simplifying with % 42.05/6.35 | (44), (47) gives: % 42.05/6.35 | (69) all_225_0 = all_221_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (15) with all_219_0, all_225_0, T, simplifying with % 42.05/6.35 | (41), (47) gives: % 42.05/6.35 | (70) all_225_0 = all_219_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (69), (70) imply: % 42.05/6.35 | (71) all_221_0 = all_219_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (71) implies: % 42.05/6.35 | (72) all_221_0 = all_219_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (62), (63) imply: % 42.05/6.35 | (73) all_221_1 = all_219_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (62), (64) imply: % 42.05/6.35 | (74) all_221_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (67), (72) imply: % 42.05/6.35 | (75) all_219_0 = all_209_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (68), (72) imply: % 42.05/6.35 | (76) all_219_0 = all_175_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (73), (74) imply: % 42.05/6.35 | (77) all_219_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (77) implies: % 42.05/6.35 | (78) all_219_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (75), (76) imply: % 42.05/6.35 | (79) all_209_0 = all_175_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (79) implies: % 42.05/6.35 | (80) all_209_0 = all_175_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (61), (78) imply: % 42.05/6.35 | (81) all_179_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (81) implies: % 42.05/6.35 | (82) all_179_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (65), (66) imply: % 42.05/6.35 | (83) all_179_0 = all_105_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (65), (80) imply: % 42.05/6.35 | (84) all_179_0 = all_175_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (59), (60) imply: % 42.05/6.35 | (85) all_175_1 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | SIMP: (85) implies: % 42.05/6.35 | (86) all_175_1 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (83), (84) imply: % 42.05/6.35 | (87) all_175_0 = all_105_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (58), (82) imply: % 42.05/6.35 | (88) all_130_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (88) implies: % 42.05/6.35 | (89) all_130_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (57), (86) imply: % 42.05/6.35 | (90) all_132_2 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | SIMP: (90) implies: % 42.05/6.35 | (91) all_132_2 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (56), (91) imply: % 42.05/6.35 | (92) all_130_0 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | SIMP: (92) implies: % 42.05/6.35 | (93) all_130_0 = all_126_1 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (55), (93) imply: % 42.05/6.35 | (94) all_126_1 = all_118_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (89), (93) imply: % 42.05/6.35 | (95) all_126_1 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (94), (95) imply: % 42.05/6.35 | (96) all_118_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (96) implies: % 42.05/6.35 | (97) all_118_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | COMBINE_EQS: (54), (97) imply: % 42.05/6.35 | (98) all_110_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | SIMP: (98) implies: % 42.05/6.35 | (99) all_110_0 = all_105_0 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (formula_43) with T, all_317_2, all_317_3, % 42.05/6.35 | all_105_1, all_317_1, all_105_0, all_317_0, simplifying with % 42.05/6.35 | (12), (17), (18), (49), (50), (51), (52) gives: % 42.05/6.35 | (100) ? [v0: any] : ? [v1: int] : ? [v2: int] : (valid(all_317_1, % 42.05/6.35 | all_317_0) = v0 & offset_min(all_317_1, all_317_0) = v1 & % 42.05/6.35 | offset_max(all_317_1, all_317_0) = v2 & c_sorted(all_317_0) & % 42.05/6.35 | c_sorted(all_317_1) & ( ~ (v0 = 0) | ($lesseq(0, v2) & $lesseq(v1, % 42.05/6.35 | 0))) & (v0 = 0 | ~ ($lesseq(0, v2)) | ~ ($lesseq(v1, 0))) % 42.05/6.35 | % 42.05/6.35 | DELTA: instantiating (100) with fresh symbols all_472_0, all_472_1, all_472_2 % 42.05/6.35 | gives: % 42.05/6.35 | (101) valid(all_317_1, all_317_0) = all_472_2 & offset_min(all_317_1, % 42.05/6.35 | all_317_0) = all_472_1 & offset_max(all_317_1, all_317_0) = % 42.05/6.35 | all_472_0 & c_sorted(all_317_0) & c_sorted(all_317_1) & ( ~ % 42.05/6.35 | (all_472_2 = 0) | ($lesseq(0, all_472_0) & $lesseq(all_472_1, 0))) % 42.05/6.35 | & (all_472_2 = 0 | ~ ($lesseq(0, all_472_0)) | ~ % 42.05/6.35 | ($lesseq(all_472_1, 0)) % 42.05/6.35 | % 42.05/6.35 | ALPHA: (101) implies: % 42.05/6.35 | (102) offset_min(all_317_1, all_317_0) = all_472_1 % 42.05/6.35 | % 42.05/6.35 | GROUND_INST: instantiating (53) with all_472_1, simplifying with (102) gives: % 42.05/6.35 | (103) $false % 42.26/6.36 | % 42.26/6.36 | CLOSE: (103) is inconsistent. % 42.26/6.36 | % 42.26/6.36 End of proof % 42.26/6.36 % SZS output end Proof for theBenchmark % 42.26/6.36 % 42.26/6.36 5744ms %------------------------------------------------------------------------------