%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW820_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 : Fri Sep 1 00:51:28 EDT 2023 % Result : Unsatisfiable 47.92s 7.59s % Output : Proof 81.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWW820_1 : TPTP v8.1.2. Released v7.0.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n028.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sun Aug 27 17:55:39 EDT 2023 % 0.14/0.35 % CPUTime : % 0.21/0.72 ________ _____ % 0.21/0.72 ___ __ \_________(_)________________________________ % 0.21/0.72 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.72 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.72 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.72 % 0.21/0.72 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.72 (2023-06-19) % 0.21/0.72 % 0.21/0.72 (c) Philipp Rümmer, 2009-2023 % 0.21/0.72 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.72 Amanda Stjerna. % 0.21/0.72 Free software under BSD-3-Clause. % 0.21/0.72 % 0.21/0.72 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.72 % 0.21/0.72 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.73 Running up to 7 provers in parallel. % 0.21/0.76 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.76 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.76 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.76 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.76 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.76 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.76 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.69/1.12 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 1.69/1.12 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 2.09/1.12 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 2.09/1.12 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 2.09/1.13 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 2.09/1.13 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 2.09/1.15 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 10.81/2.46 Prover 3: Preprocessing ... % 10.81/2.46 Prover 1: Preprocessing ... % 10.81/2.46 Prover 2: Preprocessing ... % 10.81/2.46 Prover 0: Preprocessing ... % 10.81/2.46 Prover 4: Preprocessing ... % 10.81/2.46 Prover 5: Preprocessing ... % 10.94/2.47 Prover 6: Preprocessing ... % 28.89/4.95 Prover 1: Warning: ignoring some quantifiers % 29.42/5.15 Prover 4: Warning: ignoring some quantifiers % 29.42/5.25 Prover 1: Constructing countermodel ... % 29.42/5.27 Prover 4: Constructing countermodel ... % 31.85/5.33 Prover 6: Proving ... % 31.85/5.34 Prover 3: Warning: ignoring some quantifiers % 31.85/5.37 Prover 3: Constructing countermodel ... % 33.91/5.62 Prover 0: Proving ... % 38.08/6.20 Prover 5: Proving ... % 47.92/7.57 Prover 0: proved (6825ms) % 47.92/7.57 % 47.92/7.59 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.92/7.59 % 48.60/7.60 Prover 2: Proving ... % 48.60/7.60 Prover 5: stopped % 48.60/7.60 Prover 2: stopped % 48.60/7.62 Prover 6: stopped % 48.60/7.62 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 48.60/7.62 Prover 3: stopped % 48.60/7.62 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 48.60/7.63 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 48.60/7.63 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 48.60/7.63 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 48.60/7.66 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 48.60/7.66 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 48.60/7.66 Prover 13: Warning: Problem contains reals, using incomplete axiomatisation % 48.60/7.66 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 48.60/7.67 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 52.31/8.25 Prover 8: Preprocessing ... % 52.31/8.33 Prover 13: Preprocessing ... % 52.31/8.37 Prover 10: Preprocessing ... % 52.31/8.37 Prover 11: Preprocessing ... % 52.31/8.38 Prover 7: Preprocessing ... % 57.86/9.14 Prover 10: Warning: ignoring some quantifiers % 57.86/9.18 Prover 8: Warning: ignoring some quantifiers % 59.78/9.25 Prover 8: Constructing countermodel ... % 59.78/9.27 Prover 10: Constructing countermodel ... % 61.90/9.44 Prover 11: Warning: ignoring some quantifiers % 62.25/9.50 Prover 7: Warning: ignoring some quantifiers % 63.46/9.61 Prover 11: Constructing countermodel ... % 63.46/9.64 Prover 7: Constructing countermodel ... % 64.29/9.81 Prover 13: Warning: ignoring some quantifiers % 64.29/9.97 Prover 13: Constructing countermodel ... % 79.97/11.78 Prover 13: Found proof (size 67) % 79.97/11.78 Prover 13: proved (4128ms) % 79.97/11.78 Prover 11: stopped % 79.97/11.78 Prover 1: stopped % 79.97/11.78 Prover 4: stopped % 79.97/11.79 Prover 7: stopped % 79.97/11.79 Prover 8: stopped % 79.97/11.80 Prover 10: stopped % 79.97/11.80 % 79.97/11.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 79.97/11.80 % 79.97/11.81 % SZS output start Proof for theBenchmark % 80.29/11.82 Assumptions after simplification: % 80.29/11.82 --------------------------------- % 80.29/11.82 % 80.29/11.82 (formula_101) % 80.46/11.86 c_type(type_global) & c_type(c_int) & c_type(type_alloc_table) & ? [v0: % 80.46/11.86 c_type] : ? [v1: c_type] : ? [v2: c_unique] : ? [v3: c_unique] : ? [v4: % 80.46/11.86 c_ssorted] : ? [v5: c_ssorted] : ? [v6: c_unique] : ? [v7: c_ssorted] : % 80.46/11.86 ? [v8: int] : ? [v9: int] : ? [v10: int] : ? [v11: c_unique] : ? [v12: % 80.46/11.86 c_ssorted] : ? [v13: c_unique] : ? [v14: c_unique] : ? [v15: c_unique] : % 80.46/11.86 ? [v16: c_ssorted] : ? [v17: c_ssorted] : ? [v18: c_unique] : ? [v19: % 80.46/11.86 c_ssorted] : ? [v20: int] : ? [v21: int] : ? [v22: int] : ? [v23: % 80.46/11.86 c_unique] : ? [v24: c_ssorted] : ? [v25: c_unique] : ($lesseq(v21, v20) & % 80.46/11.87 $lesseq(1, v21) & $lesseq(v20, 2800) & $lesseq(v9, v8) & $lesseq(1, v9) & % 80.46/11.87 $lesseq(v8, 2800) & %(v20, 14) = 0 & %(v8, 14) = 0 & type_memory(c_int, % 80.46/11.87 type_global) = v1 & type_pointer(type_global) = v0 & c_sort(v1, v23) = v24 % 80.46/11.87 & c_sort(v1, v18) = v19 & c_sort(v1, v11) = v12 & c_sort(v1, v6) = v7 & % 80.46/11.87 c_sort(v0, v15) = v17 & c_sort(v0, v3) = v5 & c_sort(type_alloc_table, v14) % 80.46/11.87 = v16 & c_sort(type_alloc_table, v2) = v4 & c_unique(v25) & c_unique(v23) & % 80.46/11.87 c_unique(v18) & c_unique(v15) & c_unique(v14) & c_unique(v13) & % 80.46/11.87 c_unique(v11) & c_unique(v6) & c_unique(v3) & c_unique(v2) & c_type(v1) & % 80.46/11.87 c_type(v0) & c_ssorted(v24) & c_ssorted(v19) & c_ssorted(v17) & % 80.46/11.87 c_ssorted(v16) & c_ssorted(v12) & c_ssorted(v7) & c_ssorted(v5) & % 80.46/11.87 c_ssorted(v4) & valid_range(v16, v17, 0, 2800) & valid_range(v4, v5, 0, % 80.46/11.87 2800) & ! [v26: c_ssorted] : ! [v27: c_unique] : ( ~ (acc(v24, v26) = % 80.46/11.87 v27) | ~ (c_sort(v0, v25) = v26) | valid(v16, v26)) & ! [v26: % 80.46/11.87 c_ssorted] : ! [v27: c_unique] : ( ~ (acc(v24, v26) = v27) | ~ % 80.46/11.87 (c_sort(v0, v25) = v26) | ? [v28: c_ssorted] : ? [v29: int] : ? [v30: % 80.46/11.87 int] : ? [v31: int] : (%($sum($product(10000, v29), v22), % 80.46/11.87 $sum($product(2, v21), -1)) = v30 & shift(v17, v21) = v25 & % 80.46/11.87 ss2Int(v28) = v29 & c_sort(c_int, v27) = v28 & c_unique(v27) & % 80.46/11.87 c_ssorted(v28) & ! [v32: int] : ( ~ (block_length(v16, v26) = v32) | ~ % 80.46/11.87 c_ssorted(v26) | ? [v33: int] : (v31 = v30 & offset(v26) = v33 & ( ~ % 80.46/11.87 ($lesseq(1, $difference(v32, v33))) | ~ ($lesseq(0, v33))))))) & % 80.46/11.87 ? [v26: c_ssorted] : ? [v27: c_unique] : ? [v28: c_ssorted] : ? [v29: % 80.46/11.87 int] : ? [v30: int] : ? [v31: int] : (%($sum($product(10000, v29), v10), % 80.46/11.87 $sum($product(2, v9), -1)) = v30 & acc(v12, v26) = v27 & shift(v5, v9) = % 80.46/11.87 v13 & ss2Int(v28) = v29 & c_sort(v0, v13) = v26 & c_sort(c_int, v27) = v28 % 80.46/11.87 & c_unique(v27) & c_ssorted(v28) & c_ssorted(v26) & valid(v4, v26) & ? % 80.46/11.87 [v32: int] : ? [v33: int] : (v31 = v30 & block_length(v4, v26) = v33 & % 80.46/11.87 offset(v26) = v32 & ( ~ ($lesseq(1, $difference(v33, v32))) | ~ % 80.46/11.87 ($lesseq(0, v32))))) & ? [v26: int] : ? [v27: c_unique] : ? [v28: % 80.46/11.87 c_ssorted] : ? [v29: c_unique] : ? [v30: c_ssorted] : ? [v31: int] : % 80.46/11.87 (acc(v19, v28) = v29 & shift(v17, v26) = v27 & ss2Int(v30) = v31 & % 80.46/11.87 c_sort(v0, v27) = v28 & c_sort(c_int, v29) = v30 & c_unique(v29) & % 80.46/11.87 c_unique(v27) & c_ssorted(v30) & c_ssorted(v28) & (v31 = 2000 | ~ % 80.46/11.87 ($lesseq(v26, 2799)) | ~ ($lesseq(0, v26)))) & ? [v26: int] : ? [v27: % 80.46/11.87 c_unique] : ? [v28: c_ssorted] : ? [v29: c_unique] : ? [v30: c_ssorted] % 80.46/11.87 : ? [v31: int] : (acc(v7, v28) = v29 & shift(v5, v26) = v27 & ss2Int(v30) = % 80.46/11.87 v31 & c_sort(v0, v27) = v28 & c_sort(c_int, v29) = v30 & c_unique(v29) & % 80.46/11.87 c_unique(v27) & c_ssorted(v30) & c_ssorted(v28) & (v31 = 2000 | ~ % 80.46/11.87 ($lesseq(v26, 2799)) | ~ ($lesseq(0, v26))))) % 80.46/11.87 % 80.46/11.87 (formula_28) % 80.46/11.87 c_type(type_alloc_table) & ! [v0: c_type] : ! [v1: c_unique] : ! [v2: % 80.46/11.88 c_unique] : ! [v3: c_ssorted] : ! [v4: c_type] : ! [v5: c_ssorted] : ( ~ % 80.46/11.88 (type_pointer(v0) = v4) | ~ (c_sort(v4, v2) = v5) | ~ % 80.46/11.88 (c_sort(type_alloc_table, v1) = v3) | ~ c_unique(v2) | ~ c_unique(v1) | ~ % 80.46/11.88 c_type(v0) | ? [v6: int] : ? [v7: int] : (block_length(v3, v5) = v7 & % 80.46/11.88 offset(v5) = v6 & c_ssorted(v5) & c_ssorted(v3) & ( ~ ($lesseq(1, % 80.46/11.88 $difference(v7, v6))) | ~ ($lesseq(0, v6)) | valid(v3, v5)) & ( ~ % 80.46/11.88 valid(v3, v5) | ($lesseq(1, $difference(v7, v6)) & $lesseq(0, v6))))) & % 80.46/11.88 ? [v0: c_type] : ? [v1: c_unique] : ? [v2: c_unique] : ( ~ c_unique(v2) | ~ % 80.46/11.88 c_unique(v1) | ~ c_type(v0) | ? [v3: c_ssorted] : ? [v4: c_type] : ? % 80.46/11.88 [v5: c_ssorted] : ? [v6: int] : ? [v7: int] : (block_length(v3, v5) = v7 & % 80.46/11.88 type_pointer(v0) = v4 & offset(v5) = v6 & c_sort(v4, v2) = v5 & % 80.46/11.88 c_sort(type_alloc_table, v1) = v3 & c_type(v4) & c_ssorted(v5) & % 80.46/11.88 c_ssorted(v3) & ( ~ ($lesseq(1, $difference(v7, v6))) | ~ ($lesseq(0, % 80.46/11.88 v6)) | valid(v3, v5)) & ( ~ valid(v3, v5) | ($lesseq(1, % 80.46/11.88 $difference(v7, v6)) & $lesseq(0, v6))))) % 80.46/11.88 % 80.46/11.88 (formula_29) % 80.46/11.88 c_type(type_alloc_table) & ? [v0: int] : ! [v1: c_type] : ! [v2: c_unique] % 80.46/11.88 : ! [v3: c_unique] : ! [v4: c_ssorted] : ! [v5: c_type] : ! [v6: % 80.46/11.88 c_ssorted] : ( ~ (type_pointer(v1) = v5) | ~ (c_sort(v5, v3) = v6) | ~ % 80.46/11.88 (c_sort(type_alloc_table, v2) = v4) | ~ c_unique(v3) | ~ c_unique(v2) | ~ % 80.46/11.88 c_type(v1) | ? [v7: int] : ? [v8: int] : (block_length(v4, v6) = v8 & % 80.46/11.88 offset(v6) = v7 & c_ssorted(v6) & c_ssorted(v4) & ( ~ ($lesseq(1, % 80.46/11.88 $difference($difference(v8, v7), v0))) | ~ ($lesseq(0, $sum(v7, % 80.46/11.88 v0))) | valid_index(v4, v6, v0)) & ( ~ valid_index(v4, v6, v0) | % 80.46/11.88 ($lesseq(1, $difference($difference(v8, v7), v0)) & $lesseq(0, $sum(v7, % 80.46/11.88 v0)))))) & ? [v0: c_type] : ? [v1: c_unique] : ? [v2: c_unique] % 80.46/11.88 : ? [v3: int] : ( ~ c_unique(v2) | ~ c_unique(v1) | ~ c_type(v0) | ? [v4: % 80.46/11.88 c_ssorted] : ? [v5: c_type] : ? [v6: c_ssorted] : ? [v7: int] : ? [v8: % 80.46/11.88 int] : (block_length(v4, v6) = v8 & type_pointer(v0) = v5 & offset(v6) = % 80.46/11.88 v7 & c_sort(v5, v2) = v6 & c_sort(type_alloc_table, v1) = v4 & c_type(v5) % 80.46/11.88 & c_ssorted(v6) & c_ssorted(v4) & ( ~ ($lesseq(1, % 80.46/11.88 $difference($difference(v8, v7), v3))) | ~ ($lesseq(0, $sum(v7, % 80.46/11.88 v3))) | valid_index(v4, v6, v3)) & ( ~ valid_index(v4, v6, v3) | % 80.46/11.88 ($lesseq(1, $difference($difference(v8, v7), v3)) & $lesseq(0, $sum(v7, % 80.46/11.88 v3)))))) % 80.46/11.88 % 80.46/11.88 (formula_30) % 80.46/11.89 c_type(type_alloc_table) & ? [v0: int] : ? [v1: int] : ! [v2: c_type] : ! % 80.46/11.89 [v3: c_unique] : ! [v4: c_unique] : ! [v5: c_ssorted] : ! [v6: c_type] : ! % 80.46/11.89 [v7: c_ssorted] : ( ~ (type_pointer(v2) = v6) | ~ (c_sort(v6, v4) = v7) | ~ % 80.46/11.89 (c_sort(type_alloc_table, v3) = v5) | ~ c_unique(v4) | ~ c_unique(v3) | ~ % 80.46/11.89 c_type(v2) | ? [v8: int] : ? [v9: int] : (block_length(v5, v7) = v9 & % 80.46/11.89 offset(v7) = v8 & c_ssorted(v7) & c_ssorted(v5) & ( ~ ($lesseq(1, % 80.46/11.89 $difference($difference(v9, v8), v1))) | ~ ($lesseq(0, $sum(v8, % 80.46/11.89 v0))) | valid_range(v5, v7, v0, v1)) & ( ~ valid_range(v5, v7, v0, % 80.46/11.89 v1) | ($lesseq(1, $difference($difference(v9, v8), v1)) & $lesseq(0, % 80.46/11.89 $sum(v8, v0)))))) & ? [v0: c_type] : ? [v1: c_unique] : ? [v2: % 80.46/11.89 c_unique] : ? [v3: int] : ? [v4: int] : ( ~ c_unique(v2) | ~ c_unique(v1) % 80.46/11.89 | ~ c_type(v0) | ? [v5: c_ssorted] : ? [v6: c_type] : ? [v7: c_ssorted] % 80.46/11.89 : ? [v8: int] : ? [v9: int] : (block_length(v5, v7) = v9 & % 80.46/11.89 type_pointer(v0) = v6 & offset(v7) = v8 & c_sort(v6, v2) = v7 & % 80.46/11.89 c_sort(type_alloc_table, v1) = v5 & c_type(v6) & c_ssorted(v7) & % 80.46/11.89 c_ssorted(v5) & ( ~ ($lesseq(1, $difference($difference(v9, v8), v4))) | % 80.46/11.89 ~ ($lesseq(0, $sum(v8, v3))) | valid_range(v5, v7, v3, v4)) & ( ~ % 80.46/11.89 valid_range(v5, v7, v3, v4) | ($lesseq(1, $difference($difference(v9, % 80.46/11.89 v8), v4)) & $lesseq(0, $sum(v8, v3)))))) % 80.46/11.89 % 80.46/11.89 (function-axioms) % 80.46/11.91 ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: int] : ! [v4: % 80.46/11.91 c_ssorted] : ! [v5: c_ssorted] : (v1 = v0 | ~ (pset_acc_range(v5, v4, v3, % 80.46/11.91 v2) = v1) | ~ (pset_acc_range(v5, v4, v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: c_ssorted] : ! [v4: % 80.46/11.91 c_ssorted] : (v1 = v0 | ~ (pset_acc_range_right(v4, v3, v2) = v1) | ~ % 80.46/11.91 (pset_acc_range_right(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: % 80.46/11.91 c_unique] : ! [v2: int] : ! [v3: c_ssorted] : ! [v4: c_ssorted] : (v1 = % 80.46/11.91 v0 | ~ (pset_acc_range_left(v4, v3, v2) = v1) | ~ (pset_acc_range_left(v4, % 80.46/11.91 v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: int] : % 80.46/11.91 ! [v3: int] : ! [v4: c_ssorted] : (v1 = v0 | ~ (pset_range(v4, v3, v2) = v1) % 80.46/11.91 | ~ (pset_range(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] % 80.46/11.91 : ! [v2: c_ssorted] : ! [v3: c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (upd(v4, v3, v2) = v1) | ~ (upd(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! % 80.46/11.91 [v1: c_unique] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : ! [v4: c_Boolean] % 80.46/11.91 : (v1 = v0 | ~ (smtlib__ite(v4, v3, v2) = v1) | ~ (smtlib__ite(v4, v3, v2) = % 80.46/11.91 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = % 80.46/11.91 v0 | ~ (whydivide(v3, v2) = v1) | ~ (whydivide(v3, v2) = v0)) & ! [v0: % 80.46/11.91 $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$quotient(v3, v2) = v1) | ~ (real_$quotient(v3, v2) = v0)) & ! [v0: % 80.46/11.91 $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$product(v3, v2) = v1) | ~ (real_$product(v3, v2) = v0)) & ! [v0: % 80.46/11.91 $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$difference(v3, v2) = v1) | ~ (real_$difference(v3, v2) = v0)) & ! % 80.46/11.91 [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$sum(v3, v2) = v1) | ~ (real_$sum(v3, v2) = v0)) & ! [v0: int] : ! % 80.46/11.91 [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (%(v3, v2) = v1) | ~ % 80.46/11.91 (%(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: % 80.46/11.91 c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (pset_acc_all(v3, v2) = v1) % 80.46/11.91 | ~ (pset_acc_all(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : % 80.46/11.91 ! [v2: int] : ! [v3: c_ssorted] : (v1 = v0 | ~ (pset_range_right(v3, v2) = % 80.46/11.91 v1) | ~ (pset_range_right(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: % 80.46/11.91 c_unique] : ! [v2: int] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (pset_range_left(v3, v2) = v1) | ~ (pset_range_left(v3, v2) = v0)) & ! % 80.46/11.91 [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : % 80.46/11.91 (v1 = v0 | ~ (pset_star(v3, v2) = v1) | ~ (pset_star(v3, v2) = v0)) & ! % 80.46/11.91 [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : % 80.46/11.91 (v1 = v0 | ~ (pset_union(v3, v2) = v1) | ~ (pset_union(v3, v2) = v0)) & ! % 80.46/11.91 [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] : ! [v3: c_type] : (v1 = v0 % 80.46/11.91 | ~ (type_memory(v3, v2) = v1) | ~ (type_memory(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : % 80.46/11.91 (v1 = v0 | ~ (acc(v3, v2) = v1) | ~ (acc(v3, v2) = v0)) & ! [v0: int] : ! % 80.46/11.91 [v1: int] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (sub_pointer(v3, v2) = v1) | ~ (sub_pointer(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: c_ssorted] : (v1 = v0 % 80.46/11.91 | ~ (shift(v3, v2) = v1) | ~ (shift(v3, v2) = v0)) & ! [v0: int] : ! % 80.46/11.91 [v1: int] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (block_length(v3, v2) = v1) | ~ (block_length(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (neq_int_bool(v3, v2) = v1) | ~ (neq_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (eq_int_bool(v3, v2) = v1) | ~ (eq_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (ge_int_bool(v3, v2) = v1) | ~ (ge_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (gt_int_bool(v3, v2) = v1) | ~ (gt_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (le_int_bool(v3, v2) = v1) | ~ (le_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 80.46/11.91 ~ (lt_int_bool(v3, v2) = v1) | ~ (lt_int_bool(v3, v2) = v0)) & ! [v0: % 80.46/11.91 c_ssorted] : ! [v1: c_ssorted] : ! [v2: c_unique] : ! [v3: c_type] : (v1 % 80.46/11.91 = v0 | ~ (c_sort(v3, v2) = v1) | ~ (c_sort(v3, v2) = v0)) & ! [v0: $real] % 80.46/11.91 : ! [v1: $real] : ! [v2: int] : (v1 = v0 | ~ (int_$to_real(v2) = v1) | ~ % 80.46/11.91 (int_$to_real(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] % 80.46/11.91 : (v1 = v0 | ~ (real_$to_real(v2) = v1) | ~ (real_$to_real(v2) = v0)) & ! % 80.46/11.91 [v0: $rat] : ! [v1: $rat] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_rat(v2) % 80.46/11.91 = v1) | ~ (real_$to_rat(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 80.46/11.91 [v2: $real] : (v1 = v0 | ~ (real_$to_int(v2) = v1) | ~ (real_$to_int(v2) = % 80.46/11.91 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$round(v2) = v1) | ~ (real_$round(v2) = v0)) & ! [v0: $real] : ! % 80.46/11.91 [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$truncate(v2) = v1) | ~ % 80.46/11.91 (real_$truncate(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 80.46/11.91 $real] : (v1 = v0 | ~ (real_$ceiling(v2) = v1) | ~ (real_$ceiling(v2) = % 80.46/11.91 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 80.46/11.91 (real_$floor(v2) = v1) | ~ (real_$floor(v2) = v0)) & ! [v0: $real] : ! % 80.46/11.91 [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$uminus(v2) = v1) | ~ % 80.46/11.91 (real_$uminus(v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: % 80.46/11.91 c_ssorted] : (v1 = v0 | ~ (pset_all(v2) = v1) | ~ (pset_all(v2) = v0)) & % 80.46/11.91 ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (pset_singleton(v2) = v1) | ~ (pset_singleton(v2) = v0)) & ! [v0: c_type] % 80.46/11.91 : ! [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ (type_pset(v2) = v1) | ~ % 80.46/11.91 (type_pset(v2) = v0)) & ! [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] % 80.46/11.91 : (v1 = v0 | ~ (type_pointer(v2) = v1) | ~ (type_pointer(v2) = v0)) & ! % 80.46/11.91 [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (base_addr(v2) = v1) | ~ (base_addr(v2) = v0)) & ! [v0: int] : ! [v1: % 80.46/11.91 int] : ! [v2: c_ssorted] : (v1 = v0 | ~ (offset(v2) = v1) | ~ (offset(v2) % 80.46/11.91 = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_ssorted] : % 80.46/11.91 (v1 = v0 | ~ (ss2Bool(v2) = v1) | ~ (ss2Bool(v2) = v0)) & ! [v0: $real] : % 80.46/11.91 ! [v1: $real] : ! [v2: c_ssorted] : (v1 = v0 | ~ (ss2Real(v2) = v1) | ~ % 80.46/11.91 (ss2Real(v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: % 80.46/11.91 c_Boolean] : (v1 = v0 | ~ (bool2U(v2) = v1) | ~ (bool2U(v2) = v0)) & ! % 80.46/11.91 [v0: c_unique] : ! [v1: c_unique] : ! [v2: $real] : (v1 = v0 | ~ % 80.46/11.91 (real2U(v2) = v1) | ~ (real2U(v2) = v0)) & ! [v0: c_unique] : ! [v1: % 80.46/11.91 c_unique] : ! [v2: int] : (v1 = v0 | ~ (int2U(v2) = v1) | ~ (int2U(v2) = % 80.46/11.91 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 80.46/11.91 (ss2Int(v2) = v1) | ~ (ss2Int(v2) = v0)) % 80.46/11.91 % 80.46/11.91 Further assumptions not needed in the proof: % 80.46/11.91 -------------------------------------------- % 80.46/11.91 formula_1, formula_10, formula_100, formula_11, formula_12, formula_13, % 80.46/11.91 formula_14, formula_15, formula_16, formula_17, formula_18, formula_19, % 80.46/11.91 formula_2, formula_20, formula_21, formula_22, formula_23, formula_24, % 80.46/11.91 formula_25, formula_26, formula_27, formula_3, formula_31, formula_32, % 80.46/11.91 formula_33, formula_34, formula_35, formula_36, formula_37, formula_38, % 80.46/11.91 formula_39, formula_4, formula_40, formula_41, formula_42, formula_43, % 80.46/11.91 formula_44, formula_45, formula_46, formula_47, formula_48, formula_49, % 80.46/11.91 formula_5, formula_50, formula_51, formula_52, formula_53, formula_54, % 80.46/11.91 formula_55, formula_56, formula_57, formula_58, formula_59, formula_6, % 80.46/11.91 formula_60, formula_61, formula_62, formula_63, formula_64, formula_65, % 80.46/11.91 formula_66, formula_67, formula_68, formula_69, formula_7, formula_70, % 80.46/11.91 formula_71, formula_72, formula_73, formula_74, formula_75, formula_76, % 80.46/11.91 formula_77, formula_78, formula_79, formula_8, formula_80, formula_81, % 80.46/11.91 formula_82, formula_83, formula_84, formula_85, formula_86, formula_87, % 80.46/11.91 formula_88, formula_89, formula_9, formula_90, formula_91, formula_92, % 80.46/11.91 formula_93, formula_94, formula_95, formula_96, formula_97, formula_98, % 80.46/11.91 formula_99 % 80.46/11.91 % 80.46/11.91 Those formulas are unsatisfiable: % 80.46/11.91 --------------------------------- % 80.46/11.91 % 80.46/11.91 Begin of proof % 80.46/11.91 | % 80.46/11.91 | ALPHA: (formula_28) implies: % 80.46/11.92 | (1) ! [v0: c_type] : ! [v1: c_unique] : ! [v2: c_unique] : ! [v3: % 80.46/11.92 | c_ssorted] : ! [v4: c_type] : ! [v5: c_ssorted] : ( ~ % 80.46/11.92 | (type_pointer(v0) = v4) | ~ (c_sort(v4, v2) = v5) | ~ % 80.46/11.92 | (c_sort(type_alloc_table, v1) = v3) | ~ c_unique(v2) | ~ % 80.46/11.92 | c_unique(v1) | ~ c_type(v0) | ? [v6: int] : ? [v7: int] : % 80.46/11.92 | (block_length(v3, v5) = v7 & offset(v5) = v6 & c_ssorted(v5) & % 80.46/11.92 | c_ssorted(v3) & ( ~ ($lesseq(1, $difference(v7, v6))) | ~ % 80.46/11.92 | ($lesseq(0, v6)) | valid(v3, v5)) & ( ~ valid(v3, v5) | % 80.46/11.92 | ($lesseq(1, $difference(v7, v6)) & $lesseq(0, v6))))) % 80.46/11.92 | % 80.46/11.92 | ALPHA: (formula_29) implies: % 80.46/11.92 | (2) ? [v0: int] : ! [v1: c_type] : ! [v2: c_unique] : ! [v3: c_unique] % 80.46/11.92 | : ! [v4: c_ssorted] : ! [v5: c_type] : ! [v6: c_ssorted] : ( ~ % 80.46/11.92 | (type_pointer(v1) = v5) | ~ (c_sort(v5, v3) = v6) | ~ % 80.46/11.92 | (c_sort(type_alloc_table, v2) = v4) | ~ c_unique(v3) | ~ % 80.46/11.92 | c_unique(v2) | ~ c_type(v1) | ? [v7: int] : ? [v8: int] : % 80.46/11.92 | (block_length(v4, v6) = v8 & offset(v6) = v7 & c_ssorted(v6) & % 80.46/11.92 | c_ssorted(v4) & ( ~ ($lesseq(1, $difference($difference(v8, v7), % 80.46/11.92 | v0))) | ~ ($lesseq(0, $sum(v7, v0))) | valid_index(v4, v6, % 80.46/11.92 | v0)) & ( ~ valid_index(v4, v6, v0) | ($lesseq(1, % 80.46/11.92 | $difference($difference(v8, v7), v0)) & $lesseq(0, $sum(v7, % 80.46/11.92 | v0)))))) % 80.46/11.92 | % 80.46/11.92 | ALPHA: (formula_30) implies: % 80.46/11.92 | (3) ? [v0: int] : ? [v1: int] : ! [v2: c_type] : ! [v3: c_unique] : ! % 80.46/11.92 | [v4: c_unique] : ! [v5: c_ssorted] : ! [v6: c_type] : ! [v7: % 80.46/11.92 | c_ssorted] : ( ~ (type_pointer(v2) = v6) | ~ (c_sort(v6, v4) = v7) | % 80.46/11.92 | ~ (c_sort(type_alloc_table, v3) = v5) | ~ c_unique(v4) | ~ % 80.46/11.92 | c_unique(v3) | ~ c_type(v2) | ? [v8: int] : ? [v9: int] : % 80.46/11.92 | (block_length(v5, v7) = v9 & offset(v7) = v8 & c_ssorted(v7) & % 80.46/11.92 | c_ssorted(v5) & ( ~ ($lesseq(1, $difference($difference(v9, v8), % 80.46/11.92 | v1))) | ~ ($lesseq(0, $sum(v8, v0))) | valid_range(v5, v7, % 80.46/11.92 | v0, v1)) & ( ~ valid_range(v5, v7, v0, v1) | ($lesseq(1, % 80.46/11.92 | $difference($difference(v9, v8), v1)) & $lesseq(0, $sum(v8, % 80.46/11.92 | v0)))))) % 80.46/11.92 | % 80.46/11.92 | ALPHA: (formula_101) implies: % 80.46/11.92 | (4) c_type(type_global) % 80.84/11.93 | (5) ? [v0: c_type] : ? [v1: c_type] : ? [v2: c_unique] : ? [v3: % 80.84/11.93 | c_unique] : ? [v4: c_ssorted] : ? [v5: c_ssorted] : ? [v6: % 80.84/11.93 | c_unique] : ? [v7: c_ssorted] : ? [v8: int] : ? [v9: int] : ? % 80.84/11.93 | [v10: int] : ? [v11: c_unique] : ? [v12: c_ssorted] : ? [v13: % 80.84/11.93 | c_unique] : ? [v14: c_unique] : ? [v15: c_unique] : ? [v16: % 80.84/11.93 | c_ssorted] : ? [v17: c_ssorted] : ? [v18: c_unique] : ? [v19: % 80.84/11.93 | c_ssorted] : ? [v20: int] : ? [v21: int] : ? [v22: int] : ? [v23: % 80.84/11.93 | c_unique] : ? [v24: c_ssorted] : ? [v25: c_unique] : ($lesseq(v21, % 80.84/11.93 | v20) & $lesseq(1, v21) & $lesseq(v20, 2800) & $lesseq(v9, v8) & % 80.84/11.93 | $lesseq(1, v9) & $lesseq(v8, 2800) & %(v20, 14) = 0 & %(v8, 14) = 0 & % 80.84/11.93 | type_memory(c_int, type_global) = v1 & type_pointer(type_global) = v0 % 80.84/11.93 | & c_sort(v1, v23) = v24 & c_sort(v1, v18) = v19 & c_sort(v1, v11) = % 80.84/11.93 | v12 & c_sort(v1, v6) = v7 & c_sort(v0, v15) = v17 & c_sort(v0, v3) = % 80.84/11.93 | v5 & c_sort(type_alloc_table, v14) = v16 & c_sort(type_alloc_table, % 80.84/11.93 | v2) = v4 & c_unique(v25) & c_unique(v23) & c_unique(v18) & % 80.84/11.93 | c_unique(v15) & c_unique(v14) & c_unique(v13) & c_unique(v11) & % 80.84/11.93 | c_unique(v6) & c_unique(v3) & c_unique(v2) & c_type(v1) & c_type(v0) % 80.84/11.93 | & c_ssorted(v24) & c_ssorted(v19) & c_ssorted(v17) & c_ssorted(v16) & % 80.84/11.93 | c_ssorted(v12) & c_ssorted(v7) & c_ssorted(v5) & c_ssorted(v4) & % 80.84/11.93 | valid_range(v16, v17, 0, 2800) & valid_range(v4, v5, 0, 2800) & ! % 80.84/11.93 | [v26: c_ssorted] : ! [v27: c_unique] : ( ~ (acc(v24, v26) = v27) | % 80.84/11.93 | ~ (c_sort(v0, v25) = v26) | valid(v16, v26)) & ! [v26: c_ssorted] % 80.84/11.93 | : ! [v27: c_unique] : ( ~ (acc(v24, v26) = v27) | ~ (c_sort(v0, % 80.84/11.93 | v25) = v26) | ? [v28: c_ssorted] : ? [v29: int] : ? [v30: % 80.84/11.93 | int] : ? [v31: int] : (%($sum($product(10000, v29), v22), % 80.84/11.93 | $sum($product(2, v21), -1)) = v30 & shift(v17, v21) = v25 & % 80.84/11.93 | ss2Int(v28) = v29 & c_sort(c_int, v27) = v28 & c_unique(v27) & % 80.84/11.93 | c_ssorted(v28) & ! [v32: int] : ( ~ (block_length(v16, v26) = % 80.84/11.93 | v32) | ~ c_ssorted(v26) | ? [v33: int] : (v31 = v30 & % 80.84/11.93 | offset(v26) = v33 & ( ~ ($lesseq(1, $difference(v32, v33))) | % 80.84/11.93 | ~ ($lesseq(0, v33))))))) & ? [v26: c_ssorted] : ? [v27: % 80.84/11.93 | c_unique] : ? [v28: c_ssorted] : ? [v29: int] : ? [v30: int] : % 80.84/11.93 | ? [v31: int] : (%($sum($product(10000, v29), v10), $sum($product(2, % 80.84/11.93 | v9), -1)) = v30 & acc(v12, v26) = v27 & shift(v5, v9) = v13 & % 80.84/11.93 | ss2Int(v28) = v29 & c_sort(v0, v13) = v26 & c_sort(c_int, v27) = % 80.84/11.93 | v28 & c_unique(v27) & c_ssorted(v28) & c_ssorted(v26) & valid(v4, % 80.84/11.93 | v26) & ? [v32: int] : ? [v33: int] : (v31 = v30 & % 80.84/11.93 | block_length(v4, v26) = v33 & offset(v26) = v32 & ( ~ ($lesseq(1, % 80.84/11.93 | $difference(v33, v32))) | ~ ($lesseq(0, v32))))) & ? % 80.84/11.93 | [v26: int] : ? [v27: c_unique] : ? [v28: c_ssorted] : ? [v29: % 80.84/11.93 | c_unique] : ? [v30: c_ssorted] : ? [v31: int] : (acc(v19, v28) = % 80.84/11.93 | v29 & shift(v17, v26) = v27 & ss2Int(v30) = v31 & c_sort(v0, v27) = % 80.84/11.93 | v28 & c_sort(c_int, v29) = v30 & c_unique(v29) & c_unique(v27) & % 80.84/11.93 | c_ssorted(v30) & c_ssorted(v28) & (v31 = 2000 | ~ ($lesseq(v26, % 80.84/11.93 | 2799)) | ~ ($lesseq(0, v26)))) & ? [v26: int] : ? [v27: % 80.84/11.93 | c_unique] : ? [v28: c_ssorted] : ? [v29: c_unique] : ? [v30: % 80.84/11.93 | c_ssorted] : ? [v31: int] : (acc(v7, v28) = v29 & shift(v5, v26) = % 80.84/11.93 | v27 & ss2Int(v30) = v31 & c_sort(v0, v27) = v28 & c_sort(c_int, % 80.84/11.93 | v29) = v30 & c_unique(v29) & c_unique(v27) & c_ssorted(v30) & % 80.84/11.93 | c_ssorted(v28) & (v31 = 2000 | ~ ($lesseq(v26, 2799)) | ~ % 80.84/11.93 | ($lesseq(0, v26))))) % 80.84/11.93 | % 80.84/11.93 | ALPHA: (function-axioms) implies: % 80.84/11.94 | (6) ! [v0: int] : ! [v1: int] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 80.84/11.94 | (offset(v2) = v1) | ~ (offset(v2) = v0)) % 80.84/11.94 | (7) ! [v0: int] : ! [v1: int] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : % 80.84/11.94 | (v1 = v0 | ~ (block_length(v3, v2) = v1) | ~ (block_length(v3, v2) = % 80.84/11.94 | v0)) % 80.84/11.94 | % 80.84/11.94 | DELTA: instantiating (2) with fresh symbol all_119_0 gives: % 80.84/11.94 | (8) ! [v0: c_type] : ! [v1: c_unique] : ! [v2: c_unique] : ! [v3: % 80.84/11.94 | c_ssorted] : ! [v4: c_type] : ! [v5: c_ssorted] : ( ~ % 80.84/11.94 | (type_pointer(v0) = v4) | ~ (c_sort(v4, v2) = v5) | ~ % 80.84/11.94 | (c_sort(type_alloc_table, v1) = v3) | ~ c_unique(v2) | ~ % 80.84/11.94 | c_unique(v1) | ~ c_type(v0) | ? [v6: int] : ? [v7: int] : % 80.84/11.94 | (block_length(v3, v5) = v7 & offset(v5) = v6 & c_ssorted(v5) & % 80.84/11.94 | c_ssorted(v3) & ( ~ ($lesseq(1, $difference($difference(v7, v6), % 80.84/11.94 | all_119_0))) | ~ ($lesseq(0, $sum(v6, all_119_0))) | % 80.84/11.94 | valid_index(v3, v5, all_119_0)) & ( ~ valid_index(v3, v5, % 80.84/11.94 | all_119_0) | ($lesseq(1, $difference($difference(v7, v6), % 80.84/11.94 | all_119_0)) & $lesseq(0, $sum(v6, all_119_0)))))) % 80.84/11.94 | % 80.84/11.94 | DELTA: instantiating (3) with fresh symbols all_125_0, all_125_1 gives: % 80.84/11.94 | (9) ! [v0: c_type] : ! [v1: c_unique] : ! [v2: c_unique] : ! [v3: % 80.84/11.94 | c_ssorted] : ! [v4: c_type] : ! [v5: c_ssorted] : ( ~ % 80.84/11.94 | (type_pointer(v0) = v4) | ~ (c_sort(v4, v2) = v5) | ~ % 80.84/11.94 | (c_sort(type_alloc_table, v1) = v3) | ~ c_unique(v2) | ~ % 80.84/11.94 | c_unique(v1) | ~ c_type(v0) | ? [v6: int] : ? [v7: int] : % 80.84/11.94 | (block_length(v3, v5) = v7 & offset(v5) = v6 & c_ssorted(v5) & % 80.84/11.94 | c_ssorted(v3) & ( ~ ($lesseq(1, $difference($difference(v7, v6), % 80.84/11.94 | all_125_0))) | ~ ($lesseq(0, $sum(v6, all_125_1))) | % 80.84/11.94 | valid_range(v3, v5, all_125_1, all_125_0)) & ( ~ valid_range(v3, % 80.84/11.94 | v5, all_125_1, all_125_0) | ($lesseq(1, % 80.84/11.94 | $difference($difference(v7, v6), all_125_0)) & $lesseq(0, % 80.84/11.94 | $sum(v6, all_125_1)))))) % 80.84/11.94 | % 80.84/11.94 | DELTA: instantiating (5) with fresh symbols all_267_0, all_267_1, all_267_2, % 80.84/11.94 | all_267_3, all_267_4, all_267_5, all_267_6, all_267_7, all_267_8, % 80.84/11.94 | all_267_9, all_267_10, all_267_11, all_267_12, all_267_13, all_267_14, % 80.84/11.94 | all_267_15, all_267_16, all_267_17, all_267_18, all_267_19, all_267_20, % 80.84/11.94 | all_267_21, all_267_22, all_267_23, all_267_24, all_267_25 gives: % 80.84/11.95 | (10) $lesseq(all_267_4, all_267_5) & $lesseq(1, all_267_4) & % 80.84/11.95 | $lesseq(all_267_5, 2800) & $lesseq(all_267_16, all_267_17) & % 80.84/11.95 | $lesseq(1, all_267_16) & $lesseq(all_267_17, 2800) & %(all_267_5, 14) % 80.84/11.95 | = 0 & %(all_267_17, 14) = 0 & type_memory(c_int, type_global) = % 80.84/11.95 | all_267_24 & type_pointer(type_global) = all_267_25 & % 80.84/11.95 | c_sort(all_267_24, all_267_2) = all_267_1 & c_sort(all_267_24, % 80.84/11.95 | all_267_7) = all_267_6 & c_sort(all_267_24, all_267_14) = all_267_13 % 80.84/11.95 | & c_sort(all_267_24, all_267_19) = all_267_18 & c_sort(all_267_25, % 80.84/11.95 | all_267_10) = all_267_8 & c_sort(all_267_25, all_267_22) = % 80.84/11.95 | all_267_20 & c_sort(type_alloc_table, all_267_11) = all_267_9 & % 80.84/11.95 | c_sort(type_alloc_table, all_267_23) = all_267_21 & % 80.84/11.95 | c_unique(all_267_0) & c_unique(all_267_2) & c_unique(all_267_7) & % 80.84/11.95 | c_unique(all_267_10) & c_unique(all_267_11) & c_unique(all_267_12) & % 80.84/11.95 | c_unique(all_267_14) & c_unique(all_267_19) & c_unique(all_267_22) & % 80.84/11.95 | c_unique(all_267_23) & c_type(all_267_24) & c_type(all_267_25) & % 80.84/11.95 | c_ssorted(all_267_1) & c_ssorted(all_267_6) & c_ssorted(all_267_8) & % 80.84/11.95 | c_ssorted(all_267_9) & c_ssorted(all_267_13) & c_ssorted(all_267_18) & % 80.84/11.95 | c_ssorted(all_267_20) & c_ssorted(all_267_21) & valid_range(all_267_9, % 80.84/11.95 | all_267_8, 0, 2800) & valid_range(all_267_21, all_267_20, 0, 2800) & % 80.84/11.95 | ! [v0: c_ssorted] : ! [v1: c_unique] : ( ~ (acc(all_267_1, v0) = v1) % 80.84/11.95 | | ~ (c_sort(all_267_25, all_267_0) = v0) | valid(all_267_9, v0)) & % 80.84/11.95 | ! [v0: c_ssorted] : ! [v1: c_unique] : ( ~ (acc(all_267_1, v0) = v1) % 80.84/11.95 | | ~ (c_sort(all_267_25, all_267_0) = v0) | ? [v2: c_ssorted] : ? % 80.84/11.95 | [v3: int] : ? [v4: int] : ? [v5: int] : (%($sum($product(10000, % 80.84/11.95 | v3), all_267_3), $sum($product(2, all_267_4), -1)) = v4 & % 80.84/11.95 | shift(all_267_8, all_267_4) = all_267_0 & ss2Int(v2) = v3 & % 80.84/11.95 | c_sort(c_int, v1) = v2 & c_unique(v1) & c_ssorted(v2) & ! [v6: % 80.84/11.95 | int] : ( ~ (block_length(all_267_9, v0) = v6) | ~ c_ssorted(v0) % 80.84/11.95 | | ? [v7: int] : (v5 = v4 & offset(v0) = v7 & ( ~ ($lesseq(1, % 80.84/11.95 | $difference(v6, v7))) | ~ ($lesseq(0, v7))))))) & ? % 80.84/11.95 | [v0: c_ssorted] : ? [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: % 80.84/11.95 | int] : ? [v4: int] : ? [v5: int] : (%($sum($product(10000, v3), % 80.84/11.95 | all_267_15), $sum($product(2, all_267_16), -1)) = v4 & % 80.84/11.95 | acc(all_267_13, v0) = v1 & shift(all_267_20, all_267_16) = % 80.84/11.95 | all_267_12 & ss2Int(v2) = v3 & c_sort(all_267_25, all_267_12) = v0 & % 80.84/11.95 | c_sort(c_int, v1) = v2 & c_unique(v1) & c_ssorted(v2) & % 80.84/11.95 | c_ssorted(v0) & valid(all_267_21, v0) & ? [v6: int] : ? [v7: int] % 80.84/11.95 | : (v5 = v4 & block_length(all_267_21, v0) = v7 & offset(v0) = v6 & ( % 80.84/11.95 | ~ ($lesseq(1, $difference(v7, v6))) | ~ ($lesseq(0, v6))))) & % 80.84/11.95 | ? [v0: int] : ? [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: % 80.84/11.95 | c_unique] : ? [v4: c_ssorted] : ? [v5: int] : (acc(all_267_6, v2) % 80.84/11.95 | = v3 & shift(all_267_8, v0) = v1 & ss2Int(v4) = v5 & % 80.84/11.95 | c_sort(all_267_25, v1) = v2 & c_sort(c_int, v3) = v4 & c_unique(v3) % 80.84/11.95 | & c_unique(v1) & c_ssorted(v4) & c_ssorted(v2) & (v5 = 2000 | ~ % 80.84/11.95 | ($lesseq(v0, 2799)) | ~ ($lesseq(0, v0)))) & ? [v0: int] : ? % 80.84/11.95 | [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: c_unique] : ? [v4: % 80.84/11.95 | c_ssorted] : ? [v5: int] : (acc(all_267_18, v2) = v3 & % 80.84/11.95 | shift(all_267_20, v0) = v1 & ss2Int(v4) = v5 & c_sort(all_267_25, % 80.84/11.95 | v1) = v2 & c_sort(c_int, v3) = v4 & c_unique(v3) & c_unique(v1) & % 80.84/11.95 | c_ssorted(v4) & c_ssorted(v2) & (v5 = 2000 | ~ ($lesseq(v0, 2799)) % 80.84/11.95 | | ~ ($lesseq(0, v0)))) % 80.84/11.95 | % 80.84/11.95 | ALPHA: (10) implies: % 80.84/11.95 | (11) c_unique(all_267_23) % 80.84/11.95 | (12) c_unique(all_267_12) % 80.84/11.95 | (13) c_unique(all_267_11) % 80.84/11.95 | (14) c_sort(type_alloc_table, all_267_23) = all_267_21 % 80.84/11.95 | (15) c_sort(type_alloc_table, all_267_11) = all_267_9 % 80.84/11.95 | (16) type_pointer(type_global) = all_267_25 % 80.84/11.96 | (17) ? [v0: c_ssorted] : ? [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: % 80.84/11.96 | int] : ? [v4: int] : ? [v5: int] : (%($sum($product(10000, v3), % 80.84/11.96 | all_267_15), $sum($product(2, all_267_16), -1)) = v4 & % 80.84/11.96 | acc(all_267_13, v0) = v1 & shift(all_267_20, all_267_16) = % 80.84/11.96 | all_267_12 & ss2Int(v2) = v3 & c_sort(all_267_25, all_267_12) = v0 & % 80.84/11.96 | c_sort(c_int, v1) = v2 & c_unique(v1) & c_ssorted(v2) & % 80.84/11.96 | c_ssorted(v0) & valid(all_267_21, v0) & ? [v6: int] : ? [v7: int] % 80.84/11.96 | : (v5 = v4 & block_length(all_267_21, v0) = v7 & offset(v0) = v6 & ( % 80.84/11.96 | ~ ($lesseq(1, $difference(v7, v6))) | ~ ($lesseq(0, v6))))) % 80.84/11.96 | % 80.84/11.96 | DELTA: instantiating (17) with fresh symbols all_275_0, all_275_1, all_275_2, % 80.84/11.96 | all_275_3, all_275_4, all_275_5 gives: % 80.84/11.96 | (18) %($sum($product(10000, all_275_2), all_267_15), $sum($product(2, % 80.84/11.96 | all_267_16), -1)) = all_275_1 & acc(all_267_13, all_275_5) = % 80.84/11.96 | all_275_4 & shift(all_267_20, all_267_16) = all_267_12 & % 80.84/11.96 | ss2Int(all_275_3) = all_275_2 & c_sort(all_267_25, all_267_12) = % 80.84/11.96 | all_275_5 & c_sort(c_int, all_275_4) = all_275_3 & c_unique(all_275_4) % 80.84/11.96 | & c_ssorted(all_275_3) & c_ssorted(all_275_5) & valid(all_267_21, % 80.84/11.96 | all_275_5) & ? [v0: int] : ? [v1: int] : (all_275_0 = all_275_1 & % 80.84/11.96 | block_length(all_267_21, all_275_5) = v1 & offset(all_275_5) = v0 & % 80.84/11.96 | ( ~ ($lesseq(1, $difference(v1, v0))) | ~ ($lesseq(0, v0)))) % 80.84/11.96 | % 80.84/11.96 | ALPHA: (18) implies: % 80.84/11.96 | (19) valid(all_267_21, all_275_5) % 80.84/11.96 | (20) c_sort(all_267_25, all_267_12) = all_275_5 % 80.84/11.96 | (21) ? [v0: int] : ? [v1: int] : (all_275_0 = all_275_1 & % 80.84/11.96 | block_length(all_267_21, all_275_5) = v1 & offset(all_275_5) = v0 & % 80.84/11.96 | ( ~ ($lesseq(1, $difference(v1, v0))) | ~ ($lesseq(0, v0)))) % 80.84/11.96 | % 80.84/11.96 | DELTA: instantiating (21) with fresh symbols all_277_0, all_277_1 gives: % 80.84/11.96 | (22) all_275_0 = all_275_1 & block_length(all_267_21, all_275_5) = % 80.84/11.96 | all_277_0 & offset(all_275_5) = all_277_1 & ( ~ ($lesseq(1, % 80.84/11.96 | $difference(all_277_0, all_277_1))) | ~ ($lesseq(0, % 80.84/11.96 | all_277_1))) % 80.84/11.96 | % 80.84/11.96 | ALPHA: (22) implies: % 80.84/11.96 | (23) offset(all_275_5) = all_277_1 % 80.84/11.96 | (24) block_length(all_267_21, all_275_5) = all_277_0 % 80.84/11.96 | (25) ~ ($lesseq(1, $difference(all_277_0, all_277_1))) | ~ ($lesseq(0, % 80.84/11.96 | all_277_1)) % 80.84/11.96 | % 80.84/11.97 | GROUND_INST: instantiating (9) with type_global, all_267_11, all_267_12, % 80.84/11.97 | all_267_9, all_267_25, all_275_5, simplifying with (4), (12), % 80.84/11.97 | (13), (15), (16), (20) gives: % 80.84/11.97 | (26) ? [v0: int] : ? [v1: int] : (block_length(all_267_9, all_275_5) = v1 % 80.84/11.97 | & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 80.84/11.97 | c_ssorted(all_267_9) & ( ~ ($lesseq(1, $difference($difference(v1, % 80.84/11.97 | v0), all_125_0))) | ~ ($lesseq(0, $sum(v0, all_125_1))) | % 80.84/11.97 | valid_range(all_267_9, all_275_5, all_125_1, all_125_0)) & ( ~ % 80.84/11.97 | valid_range(all_267_9, all_275_5, all_125_1, all_125_0) | % 80.84/11.97 | ($lesseq(1, $difference($difference(v1, v0), all_125_0)) & % 80.84/11.97 | $lesseq(0, $sum(v0, all_125_1))))) % 80.84/11.97 | % 80.84/11.97 | GROUND_INST: instantiating (8) with type_global, all_267_11, all_267_12, % 80.84/11.97 | all_267_9, all_267_25, all_275_5, simplifying with (4), (12), % 80.84/11.97 | (13), (15), (16), (20) gives: % 80.84/11.97 | (27) ? [v0: int] : ? [v1: int] : (block_length(all_267_9, all_275_5) = v1 % 80.84/11.97 | & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 80.84/11.97 | c_ssorted(all_267_9) & ( ~ ($lesseq(1, $difference($difference(v1, % 80.84/11.97 | v0), all_119_0))) | ~ ($lesseq(0, $sum(v0, all_119_0))) | % 80.84/11.97 | valid_index(all_267_9, all_275_5, all_119_0)) & ( ~ % 80.84/11.97 | valid_index(all_267_9, all_275_5, all_119_0) | ($lesseq(1, % 80.84/11.97 | $difference($difference(v1, v0), all_119_0)) & $lesseq(0, % 80.84/11.97 | $sum(v0, all_119_0))))) % 80.84/11.97 | % 80.84/11.97 | GROUND_INST: instantiating (1) with type_global, all_267_11, all_267_12, % 80.84/11.97 | all_267_9, all_267_25, all_275_5, simplifying with (4), (12), % 80.84/11.97 | (13), (15), (16), (20) gives: % 80.84/11.97 | (28) ? [v0: int] : ? [v1: int] : (block_length(all_267_9, all_275_5) = v1 % 80.84/11.97 | & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 80.84/11.97 | c_ssorted(all_267_9) & ( ~ ($lesseq(1, $difference(v1, v0))) | ~ % 80.84/11.97 | ($lesseq(0, v0)) | valid(all_267_9, all_275_5)) & ( ~ % 80.84/11.97 | valid(all_267_9, all_275_5) | ($lesseq(1, $difference(v1, v0)) & % 80.84/11.97 | $lesseq(0, v0)))) % 80.84/11.97 | % 80.84/11.97 | GROUND_INST: instantiating (9) with type_global, all_267_23, all_267_12, % 80.84/11.97 | all_267_21, all_267_25, all_275_5, simplifying with (4), (11), % 80.84/11.97 | (12), (14), (16), (20) gives: % 80.84/11.97 | (29) ? [v0: int] : ? [v1: int] : (block_length(all_267_21, all_275_5) = % 80.84/11.97 | v1 & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 80.84/11.97 | c_ssorted(all_267_21) & ( ~ ($lesseq(1, $difference($difference(v1, % 80.84/11.97 | v0), all_125_0))) | ~ ($lesseq(0, $sum(v0, all_125_1))) | % 80.84/11.97 | valid_range(all_267_21, all_275_5, all_125_1, all_125_0)) & ( ~ % 80.84/11.97 | valid_range(all_267_21, all_275_5, all_125_1, all_125_0) | % 80.84/11.97 | ($lesseq(1, $difference($difference(v1, v0), all_125_0)) & % 80.84/11.97 | $lesseq(0, $sum(v0, all_125_1))))) % 80.84/11.97 | % 81.06/11.98 | GROUND_INST: instantiating (8) with type_global, all_267_23, all_267_12, % 81.06/11.98 | all_267_21, all_267_25, all_275_5, simplifying with (4), (11), % 81.06/11.98 | (12), (14), (16), (20) gives: % 81.06/11.98 | (30) ? [v0: int] : ? [v1: int] : (block_length(all_267_21, all_275_5) = % 81.06/11.98 | v1 & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 81.06/11.98 | c_ssorted(all_267_21) & ( ~ ($lesseq(1, $difference($difference(v1, % 81.06/11.98 | v0), all_119_0))) | ~ ($lesseq(0, $sum(v0, all_119_0))) | % 81.06/11.98 | valid_index(all_267_21, all_275_5, all_119_0)) & ( ~ % 81.06/11.98 | valid_index(all_267_21, all_275_5, all_119_0) | ($lesseq(1, % 81.06/11.98 | $difference($difference(v1, v0), all_119_0)) & $lesseq(0, % 81.06/11.98 | $sum(v0, all_119_0))))) % 81.06/11.98 | % 81.06/11.98 | GROUND_INST: instantiating (1) with type_global, all_267_23, all_267_12, % 81.06/11.98 | all_267_21, all_267_25, all_275_5, simplifying with (4), (11), % 81.06/11.98 | (12), (14), (16), (20) gives: % 81.06/11.98 | (31) ? [v0: int] : ? [v1: int] : (block_length(all_267_21, all_275_5) = % 81.06/11.98 | v1 & offset(all_275_5) = v0 & c_ssorted(all_275_5) & % 81.06/11.98 | c_ssorted(all_267_21) & ( ~ ($lesseq(1, $difference(v1, v0))) | ~ % 81.06/11.98 | ($lesseq(0, v0)) | valid(all_267_21, all_275_5)) & ( ~ % 81.06/11.98 | valid(all_267_21, all_275_5) | ($lesseq(1, $difference(v1, v0)) & % 81.06/11.98 | $lesseq(0, v0)))) % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (31) with fresh symbols all_317_0, all_317_1 gives: % 81.06/11.98 | (32) block_length(all_267_21, all_275_5) = all_317_0 & offset(all_275_5) = % 81.06/11.98 | all_317_1 & c_ssorted(all_275_5) & c_ssorted(all_267_21) & ( ~ % 81.06/11.98 | ($lesseq(1, $difference(all_317_0, all_317_1))) | ~ ($lesseq(0, % 81.06/11.98 | all_317_1)) | valid(all_267_21, all_275_5)) & ( ~ % 81.06/11.98 | valid(all_267_21, all_275_5) | ($lesseq(1, $difference(all_317_0, % 81.06/11.98 | all_317_1)) & $lesseq(0, all_317_1))) % 81.06/11.98 | % 81.06/11.98 | ALPHA: (32) implies: % 81.06/11.98 | (33) offset(all_275_5) = all_317_1 % 81.06/11.98 | (34) block_length(all_267_21, all_275_5) = all_317_0 % 81.06/11.98 | (35) ~ valid(all_267_21, all_275_5) | ($lesseq(1, $difference(all_317_0, % 81.06/11.98 | all_317_1)) & $lesseq(0, all_317_1)) % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (30) with fresh symbols all_319_0, all_319_1 gives: % 81.06/11.98 | (36) block_length(all_267_21, all_275_5) = all_319_0 & offset(all_275_5) = % 81.06/11.98 | all_319_1 & c_ssorted(all_275_5) & c_ssorted(all_267_21) & ( ~ % 81.06/11.98 | ($lesseq(1, $difference($difference(all_319_0, all_319_1), % 81.06/11.98 | all_119_0))) | ~ ($lesseq(0, $sum(all_319_1, all_119_0))) | % 81.06/11.98 | valid_index(all_267_21, all_275_5, all_119_0)) & ( ~ % 81.06/11.98 | valid_index(all_267_21, all_275_5, all_119_0) | ($lesseq(1, % 81.06/11.98 | $difference($difference(all_319_0, all_319_1), all_119_0)) & % 81.06/11.98 | $lesseq(0, $sum(all_319_1, all_119_0)))) % 81.06/11.98 | % 81.06/11.98 | ALPHA: (36) implies: % 81.06/11.98 | (37) offset(all_275_5) = all_319_1 % 81.06/11.98 | (38) block_length(all_267_21, all_275_5) = all_319_0 % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (29) with fresh symbols all_331_0, all_331_1 gives: % 81.06/11.98 | (39) block_length(all_267_21, all_275_5) = all_331_0 & offset(all_275_5) = % 81.06/11.98 | all_331_1 & c_ssorted(all_275_5) & c_ssorted(all_267_21) & ( ~ % 81.06/11.98 | ($lesseq(1, $difference($difference(all_331_0, all_331_1), % 81.06/11.98 | all_125_0))) | ~ ($lesseq(0, $sum(all_331_1, all_125_1))) | % 81.06/11.98 | valid_range(all_267_21, all_275_5, all_125_1, all_125_0)) & ( ~ % 81.06/11.98 | valid_range(all_267_21, all_275_5, all_125_1, all_125_0) | % 81.06/11.98 | ($lesseq(1, $difference($difference(all_331_0, all_331_1), % 81.06/11.98 | all_125_0)) & $lesseq(0, $sum(all_331_1, all_125_1)))) % 81.06/11.98 | % 81.06/11.98 | ALPHA: (39) implies: % 81.06/11.98 | (40) offset(all_275_5) = all_331_1 % 81.06/11.98 | (41) block_length(all_267_21, all_275_5) = all_331_0 % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (28) with fresh symbols all_351_0, all_351_1 gives: % 81.06/11.98 | (42) block_length(all_267_9, all_275_5) = all_351_0 & offset(all_275_5) = % 81.06/11.98 | all_351_1 & c_ssorted(all_275_5) & c_ssorted(all_267_9) & ( ~ % 81.06/11.98 | ($lesseq(1, $difference(all_351_0, all_351_1))) | ~ ($lesseq(0, % 81.06/11.98 | all_351_1)) | valid(all_267_9, all_275_5)) & ( ~ % 81.06/11.98 | valid(all_267_9, all_275_5) | ($lesseq(1, $difference(all_351_0, % 81.06/11.98 | all_351_1)) & $lesseq(0, all_351_1))) % 81.06/11.98 | % 81.06/11.98 | ALPHA: (42) implies: % 81.06/11.98 | (43) offset(all_275_5) = all_351_1 % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (27) with fresh symbols all_363_0, all_363_1 gives: % 81.06/11.98 | (44) block_length(all_267_9, all_275_5) = all_363_0 & offset(all_275_5) = % 81.06/11.98 | all_363_1 & c_ssorted(all_275_5) & c_ssorted(all_267_9) & ( ~ % 81.06/11.98 | ($lesseq(1, $difference($difference(all_363_0, all_363_1), % 81.06/11.98 | all_119_0))) | ~ ($lesseq(0, $sum(all_363_1, all_119_0))) | % 81.06/11.98 | valid_index(all_267_9, all_275_5, all_119_0)) & ( ~ % 81.06/11.98 | valid_index(all_267_9, all_275_5, all_119_0) | ($lesseq(1, % 81.06/11.98 | $difference($difference(all_363_0, all_363_1), all_119_0)) & % 81.06/11.98 | $lesseq(0, $sum(all_363_1, all_119_0)))) % 81.06/11.98 | % 81.06/11.98 | ALPHA: (44) implies: % 81.06/11.98 | (45) offset(all_275_5) = all_363_1 % 81.06/11.98 | % 81.06/11.98 | DELTA: instantiating (26) with fresh symbols all_365_0, all_365_1 gives: % 81.06/11.99 | (46) block_length(all_267_9, all_275_5) = all_365_0 & offset(all_275_5) = % 81.06/11.99 | all_365_1 & c_ssorted(all_275_5) & c_ssorted(all_267_9) & ( ~ % 81.06/11.99 | ($lesseq(1, $difference($difference(all_365_0, all_365_1), % 81.06/11.99 | all_125_0))) | ~ ($lesseq(0, $sum(all_365_1, all_125_1))) | % 81.06/11.99 | valid_range(all_267_9, all_275_5, all_125_1, all_125_0)) & ( ~ % 81.06/11.99 | valid_range(all_267_9, all_275_5, all_125_1, all_125_0) | % 81.06/11.99 | ($lesseq(1, $difference($difference(all_365_0, all_365_1), % 81.06/11.99 | all_125_0)) & $lesseq(0, $sum(all_365_1, all_125_1)))) % 81.06/11.99 | % 81.06/11.99 | ALPHA: (46) implies: % 81.06/11.99 | (47) offset(all_275_5) = all_365_1 % 81.06/11.99 | % 81.06/11.99 | BETA: splitting (35) gives: % 81.06/11.99 | % 81.06/11.99 | Case 1: % 81.06/11.99 | | % 81.06/11.99 | | (48) ~ valid(all_267_21, all_275_5) % 81.06/11.99 | | % 81.06/11.99 | | PRED_UNIFY: (19), (48) imply: % 81.06/11.99 | | (49) $false % 81.06/11.99 | | % 81.06/11.99 | | CLOSE: (49) is inconsistent. % 81.06/11.99 | | % 81.06/11.99 | Case 2: % 81.06/11.99 | | % 81.06/11.99 | | (50) $lesseq(1, $difference(all_317_0, all_317_1)) & $lesseq(0, % 81.06/11.99 | | all_317_1) % 81.06/11.99 | | % 81.06/11.99 | | ALPHA: (50) implies: % 81.06/11.99 | | (51) $lesseq(0, all_317_1) % 81.06/11.99 | | (52) $lesseq(1, $difference(all_317_0, all_317_1)) % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_317_1, all_319_1, all_275_5, % 81.06/11.99 | | simplifying with (33), (37) gives: % 81.06/11.99 | | (53) all_319_1 = all_317_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_331_1, all_351_1, all_275_5, % 81.06/11.99 | | simplifying with (40), (43) gives: % 81.06/11.99 | | (54) all_351_1 = all_331_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_319_1, all_351_1, all_275_5, % 81.06/11.99 | | simplifying with (37), (43) gives: % 81.06/11.99 | | (55) all_351_1 = all_319_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_277_1, all_365_1, all_275_5, % 81.06/11.99 | | simplifying with (23), (47) gives: % 81.06/11.99 | | (56) all_365_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_363_1, all_365_1, all_275_5, % 81.06/11.99 | | simplifying with (45), (47) gives: % 81.06/11.99 | | (57) all_365_1 = all_363_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (6) with all_351_1, all_365_1, all_275_5, % 81.06/11.99 | | simplifying with (43), (47) gives: % 81.06/11.99 | | (58) all_365_1 = all_351_1 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (7) with all_317_0, all_319_0, all_275_5, % 81.06/11.99 | | all_267_21, simplifying with (34), (38) gives: % 81.06/11.99 | | (59) all_319_0 = all_317_0 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (7) with all_277_0, all_331_0, all_275_5, % 81.06/11.99 | | all_267_21, simplifying with (24), (41) gives: % 81.06/11.99 | | (60) all_331_0 = all_277_0 % 81.06/11.99 | | % 81.06/11.99 | | GROUND_INST: instantiating (7) with all_319_0, all_331_0, all_275_5, % 81.06/11.99 | | all_267_21, simplifying with (38), (41) gives: % 81.06/11.99 | | (61) all_331_0 = all_319_0 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (56), (57) imply: % 81.06/11.99 | | (62) all_363_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (57), (58) imply: % 81.06/11.99 | | (63) all_363_1 = all_351_1 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (62), (63) imply: % 81.06/11.99 | | (64) all_351_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | SIMP: (64) implies: % 81.06/11.99 | | (65) all_351_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (54), (55) imply: % 81.06/11.99 | | (66) all_331_1 = all_319_1 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (54), (65) imply: % 81.06/11.99 | | (67) all_331_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (60), (61) imply: % 81.06/11.99 | | (68) all_319_0 = all_277_0 % 81.06/11.99 | | % 81.06/11.99 | | SIMP: (68) implies: % 81.06/11.99 | | (69) all_319_0 = all_277_0 % 81.06/11.99 | | % 81.06/11.99 | | COMBINE_EQS: (66), (67) imply: % 81.06/11.99 | | (70) all_319_1 = all_277_1 % 81.06/11.99 | | % 81.06/11.99 | | SIMP: (70) implies: % 81.06/11.99 | | (71) all_319_1 = all_277_1 % 81.06/11.99 | | % 81.06/12.00 | | COMBINE_EQS: (59), (69) imply: % 81.06/12.00 | | (72) all_317_0 = all_277_0 % 81.06/12.00 | | % 81.06/12.00 | | SIMP: (72) implies: % 81.06/12.00 | | (73) all_317_0 = all_277_0 % 81.06/12.00 | | % 81.06/12.00 | | COMBINE_EQS: (53), (71) imply: % 81.06/12.00 | | (74) all_317_1 = all_277_1 % 81.06/12.00 | | % 81.06/12.00 | | SIMP: (74) implies: % 81.06/12.00 | | (75) all_317_1 = all_277_1 % 81.06/12.00 | | % 81.06/12.00 | | REDUCE: (52), (73), (75) imply: % 81.06/12.00 | | (76) $lesseq(1, $difference(all_277_0, all_277_1)) % 81.06/12.00 | | % 81.06/12.00 | | REDUCE: (51), (75) imply: % 81.06/12.00 | | (77) $lesseq(0, all_277_1) % 81.06/12.00 | | % 81.06/12.00 | | BETA: splitting (25) gives: % 81.06/12.00 | | % 81.06/12.00 | | Case 1: % 81.06/12.00 | | | % 81.06/12.00 | | | (78) $lesseq(all_277_1, -1) % 81.06/12.00 | | | % 81.06/12.00 | | | COMBINE_INEQS: (77), (78) imply: % 81.06/12.00 | | | (79) $false % 81.06/12.00 | | | % 81.06/12.00 | | | CLOSE: (79) is inconsistent. % 81.06/12.00 | | | % 81.06/12.00 | | Case 2: % 81.06/12.00 | | | % 81.06/12.00 | | | (80) $lesseq(all_277_0, all_277_1) % 81.06/12.00 | | | % 81.06/12.00 | | | COMBINE_INEQS: (76), (80) imply: % 81.06/12.00 | | | (81) $false % 81.06/12.00 | | | % 81.06/12.00 | | | CLOSE: (81) is inconsistent. % 81.06/12.00 | | | % 81.06/12.00 | | End of split % 81.06/12.00 | | % 81.06/12.00 | End of split % 81.06/12.00 | % 81.06/12.00 End of proof % 81.06/12.00 % SZS output end Proof for theBenchmark % 81.06/12.00 % 81.06/12.00 11279ms %------------------------------------------------------------------------------