%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW813_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 : n013.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:27 EDT 2023 % Result : Unsatisfiable 28.20s 4.57s % Output : Proof 35.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWW813_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.13/0.35 % Computer : n013.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Aug 27 20:02:32 EDT 2023 % 0.13/0.35 % CPUTime : % 0.21/0.61 ________ _____ % 0.21/0.61 ___ __ \_________(_)________________________________ % 0.21/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.61 % 0.21/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.61 (2023-06-19) % 0.21/0.61 % 0.21/0.61 (c) Philipp Rümmer, 2009-2023 % 0.21/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.61 Amanda Stjerna. % 0.21/0.61 Free software under BSD-3-Clause. % 0.21/0.61 % 0.21/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.61 % 0.21/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.62 Running up to 7 provers in parallel. % 0.21/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.32/0.91 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 1.32/0.91 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 1.32/0.91 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 1.32/0.91 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 1.32/0.91 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 1.91/0.92 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 1.91/0.93 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 8.44/1.88 Prover 1: Preprocessing ... % 8.44/1.88 Prover 3: Preprocessing ... % 8.59/1.88 Prover 5: Preprocessing ... % 8.59/1.89 Prover 4: Preprocessing ... % 8.59/1.89 Prover 0: Preprocessing ... % 8.59/1.89 Prover 6: Preprocessing ... % 8.59/1.90 Prover 2: Preprocessing ... % 21.52/3.66 Prover 1: Warning: ignoring some quantifiers % 22.58/3.78 Prover 1: Constructing countermodel ... % 22.58/3.79 Prover 4: Warning: ignoring some quantifiers % 22.58/3.79 Prover 3: Warning: ignoring some quantifiers % 22.58/3.79 Prover 6: Proving ... % 22.58/3.81 Prover 3: Constructing countermodel ... % 23.49/3.91 Prover 4: Constructing countermodel ... % 23.81/4.01 Prover 0: Proving ... % 28.20/4.57 Prover 0: proved (3938ms) % 28.20/4.57 % 28.20/4.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.20/4.57 % 28.57/4.58 Prover 6: stopped % 28.57/4.59 Prover 3: stopped % 28.57/4.59 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 28.57/4.59 Prover 5: Proving ... % 28.57/4.59 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 28.57/4.59 Prover 5: stopped % 28.57/4.60 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 28.57/4.60 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 28.57/4.61 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 28.57/4.61 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 28.57/4.62 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 28.57/4.62 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 31.77/5.04 Prover 10: Preprocessing ... % 31.77/5.07 Prover 8: Preprocessing ... % 31.77/5.07 Prover 7: Preprocessing ... % 31.77/5.08 Prover 11: Preprocessing ... % 33.27/5.24 Prover 4: Found proof (size 18) % 33.27/5.24 Prover 4: proved (4609ms) % 33.27/5.24 Prover 10: stopped % 33.27/5.25 Prover 7: stopped % 33.27/5.25 Prover 11: stopped % 33.27/5.25 Prover 1: stopped % 33.27/5.31 Prover 2: Proving ... % 33.27/5.31 Prover 2: stopped % 34.37/5.58 Prover 8: Warning: ignoring some quantifiers % 34.61/5.63 Prover 8: Constructing countermodel ... % 35.07/5.63 Prover 8: stopped % 35.07/5.64 % 35.07/5.64 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.07/5.64 % 35.07/5.64 % SZS output start Proof for theBenchmark % 35.07/5.65 Assumptions after simplification: % 35.07/5.65 --------------------------------- % 35.07/5.65 % 35.07/5.65 (formula_101) % 35.07/5.70 c_type(type_global) & c_type(c_int) & c_type(type_alloc_table) & ? [v0: % 35.07/5.70 c_type] : ? [v1: c_type] : ? [v2: c_unique] : ? [v3: c_unique] : ? [v4: % 35.07/5.70 c_ssorted] : ? [v5: c_ssorted] : ? [v6: c_unique] : ? [v7: c_ssorted] : % 35.07/5.70 ? [v8: int] : ? [v9: int] : ? [v10: int] : ? [v11: c_unique] : ? [v12: % 35.07/5.70 c_ssorted] : ? [v13: c_unique] : ($lesseq(v9, v8) & $lesseq(1, v9) & % 35.07/5.70 $lesseq(v8, 2800) & %(v8, 14) = 0 & type_memory(c_int, type_global) = v1 & % 35.07/5.70 valid_range(v4, v5, 0, 2800) = 0 & type_pointer(type_global) = v0 & % 35.07/5.70 c_sort(v1, v11) = v12 & c_sort(v1, v6) = v7 & c_sort(v0, v3) = v5 & % 35.07/5.70 c_sort(type_alloc_table, v2) = v4 & c_unique(v13) & c_unique(v11) & % 35.07/5.70 c_unique(v6) & c_unique(v3) & c_unique(v2) & c_type(v1) & c_type(v0) & % 35.07/5.70 c_ssorted(v12) & c_ssorted(v7) & c_ssorted(v5) & c_ssorted(v4) & ! [v14: % 35.07/5.70 c_ssorted] : ( ~ (c_sort(v0, v13) = v14) | ? [v15: c_unique] : ? [v16: % 35.07/5.70 c_ssorted] : ? [v17: int] : ? [v18: int] : ? [v19: int] : ? [v20: % 35.07/5.70 c_unique] : ? [v21: c_ssorted] : ? [v22: c_unique] : ? [v23: int] : % 35.07/5.70 ? [v24: int] : ? [v25: int] : (v9 = 1 & ~ (v25 = 0) & whydivide(v19, % 35.07/5.70 10000) = v23 & whydivide($sum($product(10000, v17), v10), 1) = v19 & % 35.07/5.70 %(v19, 10000) = v24 & %($sum($product(10000, v17), v10), 1) = v18 & % 35.07/5.70 %($sum(v8, -14), 14) = v25 & upd(v12, v14, v21) = v22 & acc(v12, v14) = % 35.07/5.70 v15 & shift(v5, 1) = v13 & valid(v4, v14) = 0 & int2U(v18) = v20 & % 35.07/5.70 ss2Int(v16) = v17 & c_sort(c_int, v20) = v21 & c_sort(c_int, v15) = v16 % 35.07/5.70 & c_unique(v22) & c_unique(v20) & c_unique(v15) & c_ssorted(v21) & % 35.07/5.70 c_ssorted(v16))) & ? [v14: c_ssorted] : ? [v15: c_unique] : ? [v16: % 35.07/5.70 c_ssorted] : ? [v17: int] : ? [v18: int] : ? [v19: int] : ? [v20: % 35.07/5.70 c_unique] : ? [v21: c_ssorted] : ? [v22: c_unique] : ? [v23: int] : ? % 35.07/5.70 [v24: int] : ? [v25: int] : (v9 = 1 & ~ (v25 = 0) & whydivide(v19, 10000) % 35.07/5.70 = v23 & whydivide($sum($product(10000, v17), v10), 1) = v19 & %(v19, % 35.07/5.70 10000) = v24 & %($sum($product(10000, v17), v10), 1) = v18 & %($sum(v8, % 35.07/5.70 -14), 14) = v25 & upd(v12, v14, v21) = v22 & acc(v12, v14) = v15 & % 35.07/5.70 shift(v5, 1) = v13 & valid(v4, v14) = 0 & int2U(v18) = v20 & ss2Int(v16) = % 35.07/5.70 v17 & c_sort(v0, v13) = v14 & c_sort(c_int, v20) = v21 & c_sort(c_int, % 35.07/5.70 v15) = v16 & c_unique(v22) & c_unique(v20) & c_unique(v15) & % 35.07/5.70 c_ssorted(v21) & c_ssorted(v16) & c_ssorted(v14)) & ? [v14: int] : ? % 35.07/5.70 [v15: c_unique] : ? [v16: c_ssorted] : ? [v17: c_unique] : ? [v18: % 35.07/5.70 c_ssorted] : ? [v19: int] : (acc(v7, v16) = v17 & shift(v5, v14) = v15 & % 35.07/5.70 ss2Int(v18) = v19 & c_sort(v0, v15) = v16 & c_sort(c_int, v17) = v18 & % 35.07/5.70 c_unique(v17) & c_unique(v15) & c_ssorted(v18) & c_ssorted(v16) & (v19 = % 35.07/5.70 2000 | ~ ($lesseq(v14, 2799)) | ~ ($lesseq(0, v14))))) % 35.07/5.70 % 35.07/5.70 (formula_98) % 35.07/5.71 ! [v0: int] : ! [v1: int] : (v1 = 0 | ~ (%($sum(v0, -14), 14) = v1) | ? % 35.07/5.71 [v2: int] : ( ~ (v2 = 0) & %(v0, 14) = v2)) & ! [v0: int] : ( ~ (%(v0, 14) % 35.07/5.71 = 0) | %($sum(v0, -14), 14) = 0) % 35.07/5.71 % 35.07/5.71 (function-axioms) % 35.52/5.73 ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: int] : ! [v4: % 35.52/5.73 c_ssorted] : ! [v5: c_ssorted] : (v1 = v0 | ~ (pset_acc_range(v5, v4, v3, % 35.52/5.73 v2) = v1) | ~ (pset_acc_range(v5, v4, v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : ! [v4: c_ssorted] : ! [v5: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (not_assigns(v5, v4, v3, v2) = v1) | ~ (not_assigns(v5, v4, v3, v2) = v0)) % 35.52/5.73 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 35.52/5.73 [v3: int] : ! [v4: c_ssorted] : ! [v5: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (valid_range(v5, v4, v3, v2) = v1) | ~ (valid_range(v5, v4, v3, v2) = v0)) % 35.52/5.73 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] % 35.52/5.73 : ! [v3: c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ (free_stack(v4, v3, % 35.52/5.73 v2) = v1) | ~ (free_stack(v4, v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 35.52/5.73 c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ (separation2_range1(v4, v3, % 35.52/5.73 v2) = v1) | ~ (separation2_range1(v4, v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 35.52/5.73 c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ (separation1_range1(v4, v3, % 35.52/5.73 v2) = v1) | ~ (separation1_range1(v4, v3, v2) = v0)) & ! [v0: % 35.52/5.73 c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: c_ssorted] : ! [v4: % 35.52/5.73 c_ssorted] : (v1 = v0 | ~ (pset_acc_range_right(v4, v3, v2) = v1) | ~ % 35.52/5.73 (pset_acc_range_right(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: % 35.52/5.73 c_unique] : ! [v2: int] : ! [v3: c_ssorted] : ! [v4: c_ssorted] : (v1 = % 35.52/5.73 v0 | ~ (pset_acc_range_left(v4, v3, v2) = v1) | ~ (pset_acc_range_left(v4, % 35.52/5.73 v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: int] : % 35.52/5.73 ! [v3: int] : ! [v4: c_ssorted] : (v1 = v0 | ~ (pset_range(v4, v3, v2) = v1) % 35.52/5.73 | ~ (pset_range(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] % 35.52/5.73 : ! [v2: c_ssorted] : ! [v3: c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (upd(v4, v3, v2) = v1) | ~ (upd(v4, v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 35.52/5.73 c_ssorted] : ! [v4: c_ssorted] : (v1 = v0 | ~ (valid_index(v4, v3, v2) = % 35.52/5.73 v1) | ~ (valid_index(v4, v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: % 35.52/5.73 c_unique] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : ! [v4: c_Boolean] : % 35.52/5.73 (v1 = v0 | ~ (smtlib__ite(v4, v3, v2) = v1) | ~ (smtlib__ite(v4, v3, v2) = % 35.52/5.73 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : % 35.52/5.73 (v1 = v0 | ~ (real_$quotient(v3, v2) = v1) | ~ (real_$quotient(v3, v2) = % 35.52/5.73 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : % 35.52/5.73 (v1 = v0 | ~ (real_$product(v3, v2) = v1) | ~ (real_$product(v3, v2) = v0)) % 35.52/5.73 & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 35.52/5.73 | ~ (real_$difference(v3, v2) = v1) | ~ (real_$difference(v3, v2) = v0)) & % 35.52/5.73 ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | % 35.52/5.73 ~ (real_$sum(v3, v2) = v1) | ~ (real_$sum(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 35.52/5.73 $real] : (v1 = v0 | ~ (real_$greatereq(v3, v2) = v1) | ~ % 35.52/5.73 (real_$greatereq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 35.52/5.73 (real_$lesseq(v3, v2) = v1) | ~ (real_$lesseq(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 35.52/5.73 $real] : (v1 = v0 | ~ (real_$greater(v3, v2) = v1) | ~ (real_$greater(v3, % 35.52/5.73 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 35.52/5.73 ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ (real_$less(v3, v2) = v1) | ~ % 35.52/5.73 (real_$less(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 35.52/5.73 [v3: int] : (v1 = v0 | ~ (whydivide(v3, v2) = v1) | ~ (whydivide(v3, v2) = % 35.52/5.73 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = % 35.52/5.73 v0 | ~ (%(v3, v2) = v1) | ~ (%(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 35.52/5.73 : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = % 35.52/5.73 v0 | ~ (on_stack(v3, v2) = v1) | ~ (on_stack(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : (v1 = v0 | ~ (on_heap(v3, v2) = v1) | ~ (on_heap(v3, v2) = % 35.52/5.73 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 35.52/5.73 c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (alloc_extends(v3, v2) = v1) % 35.52/5.73 | ~ (alloc_extends(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (fresh(v3, v2) = v1) | ~ (fresh(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 35.52/5.73 : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = % 35.52/5.73 v0 | ~ (separation2(v3, v2) = v1) | ~ (separation2(v3, v2) = v0)) & ! % 35.52/5.73 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 35.52/5.73 c_ssorted] : (v1 = v0 | ~ (separation1_range(v3, v2) = v1) | ~ % 35.52/5.73 (separation1_range(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (separation1(v3, v2) = v1) | ~ (separation1(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 35.52/5.73 c_ssorted] : (v1 = v0 | ~ (valid_acc_range(v3, v2) = v1) | ~ % 35.52/5.73 (valid_acc_range(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! % 35.52/5.73 [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (pset_acc_all(v3, v2) = % 35.52/5.73 v1) | ~ (pset_acc_all(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: % 35.52/5.73 c_unique] : ! [v2: int] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (pset_range_right(v3, v2) = v1) | ~ (pset_range_right(v3, v2) = v0)) & ! % 35.52/5.73 [v0: c_unique] : ! [v1: c_unique] : ! [v2: int] : ! [v3: c_ssorted] : (v1 = % 35.52/5.73 v0 | ~ (pset_range_left(v3, v2) = v1) | ~ (pset_range_left(v3, v2) = v0)) % 35.52/5.73 & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : ! [v3: % 35.52/5.73 c_ssorted] : (v1 = v0 | ~ (pset_star(v3, v2) = v1) | ~ (pset_star(v3, v2) % 35.52/5.73 = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : (v1 = v0 | ~ (pset_union(v3, v2) = v1) | ~ (pset_union(v3, % 35.52/5.73 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 35.52/5.73 ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (not_in_pset(v3, v2) = % 35.52/5.73 v1) | ~ (not_in_pset(v3, v2) = v0)) & ! [v0: c_type] : ! [v1: c_type] : % 35.52/5.73 ! [v2: c_type] : ! [v3: c_type] : (v1 = v0 | ~ (type_memory(v3, v2) = v1) | % 35.52/5.73 ~ (type_memory(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! % 35.52/5.73 [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (acc(v3, v2) = v1) | ~ % 35.52/5.73 (acc(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : (v1 = v0 | ~ (sub_pointer(v3, v2) = v1) | ~ % 35.52/5.73 (sub_pointer(v3, v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! % 35.52/5.73 [v2: int] : ! [v3: c_ssorted] : (v1 = v0 | ~ (shift(v3, v2) = v1) | ~ % 35.52/5.73 (shift(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (valid(v3, v2) = v1) | ~ (valid(v3, v2) = v0)) & ! [v0: int] : ! [v1: % 35.52/5.73 int] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (block_length(v3, v2) = v1) | ~ (block_length(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : (v1 = v0 | ~ (ge_pointer(v3, v2) = v1) | ~ (ge_pointer(v3, % 35.52/5.73 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 35.52/5.73 ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ (gt_pointer(v3, v2) = % 35.52/5.73 v1) | ~ (gt_pointer(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: c_ssorted] : ! [v3: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (le_pointer(v3, v2) = v1) | ~ (le_pointer(v3, v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: c_ssorted] : ! % 35.52/5.73 [v3: c_ssorted] : (v1 = v0 | ~ (lt_pointer(v3, v2) = v1) | ~ (lt_pointer(v3, % 35.52/5.73 v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! % 35.52/5.73 [v3: int] : (v1 = v0 | ~ (neq_int_bool(v3, v2) = v1) | ~ (neq_int_bool(v3, % 35.52/5.73 v2) = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! % 35.52/5.73 [v3: int] : (v1 = v0 | ~ (eq_int_bool(v3, v2) = v1) | ~ (eq_int_bool(v3, v2) % 35.52/5.73 = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 35.52/5.73 int] : (v1 = v0 | ~ (ge_int_bool(v3, v2) = v1) | ~ (ge_int_bool(v3, v2) = % 35.52/5.73 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 35.52/5.73 int] : (v1 = v0 | ~ (gt_int_bool(v3, v2) = v1) | ~ (gt_int_bool(v3, v2) = % 35.52/5.73 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 35.52/5.73 int] : (v1 = v0 | ~ (le_int_bool(v3, v2) = v1) | ~ (le_int_bool(v3, v2) = % 35.52/5.73 v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: int] : ! [v3: % 35.52/5.73 int] : (v1 = v0 | ~ (lt_int_bool(v3, v2) = v1) | ~ (lt_int_bool(v3, v2) = % 35.52/5.73 v0)) & ! [v0: c_ssorted] : ! [v1: c_ssorted] : ! [v2: c_unique] : ! % 35.52/5.73 [v3: c_type] : (v1 = v0 | ~ (c_sort(v3, v2) = v1) | ~ (c_sort(v3, v2) = v0)) % 35.52/5.73 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : % 35.52/5.73 (v1 = v0 | ~ (real_$is_int(v2) = v1) | ~ (real_$is_int(v2) = v0)) & ! [v0: % 35.52/5.73 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : (v1 = v0 % 35.52/5.73 | ~ (real_$is_rat(v2) = v1) | ~ (real_$is_rat(v2) = v0)) & ! [v0: $real] % 35.52/5.73 : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$floor(v2) = v1) | ~ % 35.52/5.73 (real_$floor(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : % 35.52/5.73 (v1 = v0 | ~ (real_$ceiling(v2) = v1) | ~ (real_$ceiling(v2) = v0)) & ! % 35.52/5.73 [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 35.52/5.73 (real_$truncate(v2) = v1) | ~ (real_$truncate(v2) = v0)) & ! [v0: $real] : % 35.52/5.73 ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$round(v2) = v1) | ~ % 35.52/5.73 (real_$round(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: $real] : (v1 % 35.52/5.73 = v0 | ~ (real_$to_int(v2) = v1) | ~ (real_$to_int(v2) = v0)) & ! [v0: % 35.52/5.73 $rat] : ! [v1: $rat] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_rat(v2) = % 35.52/5.73 v1) | ~ (real_$to_rat(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 35.52/5.73 [v2: $real] : (v1 = v0 | ~ (real_$to_real(v2) = v1) | ~ (real_$to_real(v2) = % 35.52/5.73 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: int] : (v1 = v0 | ~ % 35.52/5.73 (int_$to_real(v2) = v1) | ~ (int_$to_real(v2) = v0)) & ! [v0: $real] : ! % 35.52/5.73 [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$uminus(v2) = v1) | ~ % 35.52/5.73 (real_$uminus(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 35.52/5.73 MultipleValueBool] : ! [v2: c_ssorted] : (v1 = v0 | ~ (valid_acc(v2) = v1) % 35.52/5.73 | ~ (valid_acc(v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: % 35.52/5.73 c_ssorted] : (v1 = v0 | ~ (pset_all(v2) = v1) | ~ (pset_all(v2) = v0)) & % 35.52/5.73 ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (pset_singleton(v2) = v1) | ~ (pset_singleton(v2) = v0)) & ! [v0: c_type] % 35.52/5.73 : ! [v1: c_type] : ! [v2: c_type] : (v1 = v0 | ~ (type_pset(v2) = v1) | ~ % 35.52/5.73 (type_pset(v2) = v0)) & ! [v0: c_type] : ! [v1: c_type] : ! [v2: c_type] % 35.52/5.73 : (v1 = v0 | ~ (type_pointer(v2) = v1) | ~ (type_pointer(v2) = v0)) & ! % 35.52/5.73 [v0: c_unique] : ! [v1: c_unique] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (base_addr(v2) = v1) | ~ (base_addr(v2) = v0)) & ! [v0: int] : ! [v1: % 35.52/5.73 int] : ! [v2: c_ssorted] : (v1 = v0 | ~ (offset(v2) = v1) | ~ (offset(v2) % 35.52/5.73 = v0)) & ! [v0: c_Boolean] : ! [v1: c_Boolean] : ! [v2: c_ssorted] : % 35.52/5.73 (v1 = v0 | ~ (ss2Bool(v2) = v1) | ~ (ss2Bool(v2) = v0)) & ! [v0: $real] : % 35.52/5.73 ! [v1: $real] : ! [v2: c_ssorted] : (v1 = v0 | ~ (ss2Real(v2) = v1) | ~ % 35.52/5.73 (ss2Real(v2) = v0)) & ! [v0: c_unique] : ! [v1: c_unique] : ! [v2: % 35.52/5.73 c_Boolean] : (v1 = v0 | ~ (bool2U(v2) = v1) | ~ (bool2U(v2) = v0)) & ! % 35.52/5.73 [v0: c_unique] : ! [v1: c_unique] : ! [v2: $real] : (v1 = v0 | ~ % 35.52/5.73 (real2U(v2) = v1) | ~ (real2U(v2) = v0)) & ! [v0: c_unique] : ! [v1: % 35.52/5.73 c_unique] : ! [v2: int] : (v1 = v0 | ~ (int2U(v2) = v1) | ~ (int2U(v2) = % 35.52/5.73 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: c_ssorted] : (v1 = v0 | ~ % 35.52/5.73 (ss2Int(v2) = v1) | ~ (ss2Int(v2) = v0)) % 35.52/5.73 % 35.52/5.73 Further assumptions not needed in the proof: % 35.52/5.73 -------------------------------------------- % 35.52/5.73 formula_1, formula_10, formula_100, formula_11, formula_12, formula_13, % 35.52/5.73 formula_14, formula_15, formula_16, formula_17, formula_18, formula_19, % 35.52/5.73 formula_2, formula_20, formula_21, formula_22, formula_23, formula_24, % 35.52/5.73 formula_25, formula_26, formula_27, formula_28, formula_29, formula_3, % 35.52/5.73 formula_30, formula_31, formula_32, formula_33, formula_34, formula_35, % 35.52/5.73 formula_36, formula_37, formula_38, formula_39, formula_4, formula_40, % 35.52/5.73 formula_41, formula_42, formula_43, formula_44, formula_45, formula_46, % 35.52/5.73 formula_47, formula_48, formula_49, formula_5, formula_50, formula_51, % 35.52/5.73 formula_52, formula_53, formula_54, formula_55, formula_56, formula_57, % 35.52/5.73 formula_58, formula_59, formula_6, formula_60, formula_61, formula_62, % 35.52/5.73 formula_63, formula_64, formula_65, formula_66, formula_67, formula_68, % 35.52/5.73 formula_69, formula_7, formula_70, formula_71, formula_72, formula_73, % 35.52/5.73 formula_74, formula_75, formula_76, formula_77, formula_78, formula_79, % 35.52/5.73 formula_8, formula_80, formula_81, formula_82, formula_83, formula_84, % 35.52/5.74 formula_85, formula_86, formula_87, formula_88, formula_89, formula_9, % 35.52/5.74 formula_90, formula_91, formula_92, formula_93, formula_94, formula_95, % 35.52/5.74 formula_96, formula_97, formula_99 % 35.52/5.74 % 35.52/5.74 Those formulas are unsatisfiable: % 35.52/5.74 --------------------------------- % 35.52/5.74 % 35.52/5.74 Begin of proof % 35.52/5.74 | % 35.52/5.74 | ALPHA: (formula_98) implies: % 35.52/5.74 | (1) ! [v0: int] : ( ~ (%(v0, 14) = 0) | %($sum(v0, -14), 14) = 0) % 35.52/5.74 | % 35.52/5.74 | ALPHA: (formula_101) implies: % 35.52/5.74 | (2) ? [v0: c_type] : ? [v1: c_type] : ? [v2: c_unique] : ? [v3: % 35.52/5.74 | c_unique] : ? [v4: c_ssorted] : ? [v5: c_ssorted] : ? [v6: % 35.52/5.74 | c_unique] : ? [v7: c_ssorted] : ? [v8: int] : ? [v9: int] : ? % 35.52/5.74 | [v10: int] : ? [v11: c_unique] : ? [v12: c_ssorted] : ? [v13: % 35.52/5.74 | c_unique] : ($lesseq(v9, v8) & $lesseq(1, v9) & $lesseq(v8, 2800) & % 35.52/5.74 | %(v8, 14) = 0 & type_memory(c_int, type_global) = v1 & % 35.52/5.74 | valid_range(v4, v5, 0, 2800) = 0 & type_pointer(type_global) = v0 & % 35.52/5.74 | c_sort(v1, v11) = v12 & c_sort(v1, v6) = v7 & c_sort(v0, v3) = v5 & % 35.52/5.74 | c_sort(type_alloc_table, v2) = v4 & c_unique(v13) & c_unique(v11) & % 35.52/5.74 | c_unique(v6) & c_unique(v3) & c_unique(v2) & c_type(v1) & c_type(v0) % 35.52/5.74 | & c_ssorted(v12) & c_ssorted(v7) & c_ssorted(v5) & c_ssorted(v4) & ! % 35.52/5.74 | [v14: c_ssorted] : ( ~ (c_sort(v0, v13) = v14) | ? [v15: c_unique] : % 35.52/5.74 | ? [v16: c_ssorted] : ? [v17: int] : ? [v18: int] : ? [v19: int] % 35.52/5.74 | : ? [v20: c_unique] : ? [v21: c_ssorted] : ? [v22: c_unique] : % 35.52/5.74 | ? [v23: int] : ? [v24: int] : ? [v25: int] : (v9 = 1 & ~ (v25 = % 35.52/5.74 | 0) & whydivide(v19, 10000) = v23 & % 35.52/5.74 | whydivide($sum($product(10000, v17), v10), 1) = v19 & %(v19, % 35.52/5.74 | 10000) = v24 & %($sum($product(10000, v17), v10), 1) = v18 & % 35.52/5.74 | %($sum(v8, -14), 14) = v25 & upd(v12, v14, v21) = v22 & acc(v12, % 35.52/5.74 | v14) = v15 & shift(v5, 1) = v13 & valid(v4, v14) = 0 & % 35.52/5.74 | int2U(v18) = v20 & ss2Int(v16) = v17 & c_sort(c_int, v20) = v21 & % 35.52/5.74 | c_sort(c_int, v15) = v16 & c_unique(v22) & c_unique(v20) & % 35.52/5.74 | c_unique(v15) & c_ssorted(v21) & c_ssorted(v16))) & ? [v14: % 35.52/5.74 | c_ssorted] : ? [v15: c_unique] : ? [v16: c_ssorted] : ? [v17: % 35.52/5.74 | int] : ? [v18: int] : ? [v19: int] : ? [v20: c_unique] : ? % 35.52/5.74 | [v21: c_ssorted] : ? [v22: c_unique] : ? [v23: int] : ? [v24: int] % 35.52/5.74 | : ? [v25: int] : (v9 = 1 & ~ (v25 = 0) & whydivide(v19, 10000) = % 35.52/5.74 | v23 & whydivide($sum($product(10000, v17), v10), 1) = v19 & %(v19, % 35.52/5.74 | 10000) = v24 & %($sum($product(10000, v17), v10), 1) = v18 & % 35.52/5.74 | %($sum(v8, -14), 14) = v25 & upd(v12, v14, v21) = v22 & acc(v12, % 35.52/5.74 | v14) = v15 & shift(v5, 1) = v13 & valid(v4, v14) = 0 & int2U(v18) % 35.52/5.74 | = v20 & ss2Int(v16) = v17 & c_sort(v0, v13) = v14 & c_sort(c_int, % 35.52/5.74 | v20) = v21 & c_sort(c_int, v15) = v16 & c_unique(v22) & % 35.52/5.74 | c_unique(v20) & c_unique(v15) & c_ssorted(v21) & c_ssorted(v16) & % 35.52/5.74 | c_ssorted(v14)) & ? [v14: int] : ? [v15: c_unique] : ? [v16: % 35.52/5.74 | c_ssorted] : ? [v17: c_unique] : ? [v18: c_ssorted] : ? [v19: % 35.52/5.74 | int] : (acc(v7, v16) = v17 & shift(v5, v14) = v15 & ss2Int(v18) = % 35.52/5.74 | v19 & c_sort(v0, v15) = v16 & c_sort(c_int, v17) = v18 & % 35.52/5.74 | c_unique(v17) & c_unique(v15) & c_ssorted(v18) & c_ssorted(v16) & % 35.52/5.74 | (v19 = 2000 | ~ ($lesseq(v14, 2799)) | ~ ($lesseq(0, v14))))) % 35.52/5.74 | % 35.52/5.74 | ALPHA: (function-axioms) implies: % 35.52/5.74 | (3) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | % 35.52/5.74 | ~ (%(v3, v2) = v1) | ~ (%(v3, v2) = v0)) % 35.52/5.74 | % 35.52/5.74 | DELTA: instantiating (2) with fresh symbols all_190_0, all_190_1, all_190_2, % 35.52/5.74 | all_190_3, all_190_4, all_190_5, all_190_6, all_190_7, all_190_8, % 35.52/5.74 | all_190_9, all_190_10, all_190_11, all_190_12, all_190_13 gives: % 35.52/5.75 | (4) $lesseq(all_190_4, all_190_5) & $lesseq(1, all_190_4) & % 35.52/5.75 | $lesseq(all_190_5, 2800) & %(all_190_5, 14) = 0 & type_memory(c_int, % 35.52/5.75 | type_global) = all_190_12 & valid_range(all_190_9, all_190_8, 0, % 35.52/5.75 | 2800) = 0 & type_pointer(type_global) = all_190_13 & % 35.52/5.75 | c_sort(all_190_12, all_190_2) = all_190_1 & c_sort(all_190_12, % 35.52/5.75 | all_190_7) = all_190_6 & c_sort(all_190_13, all_190_10) = all_190_8 & % 35.52/5.75 | c_sort(type_alloc_table, all_190_11) = all_190_9 & c_unique(all_190_0) % 35.52/5.75 | & c_unique(all_190_2) & c_unique(all_190_7) & c_unique(all_190_10) & % 35.52/5.75 | c_unique(all_190_11) & c_type(all_190_12) & c_type(all_190_13) & % 35.52/5.75 | c_ssorted(all_190_1) & c_ssorted(all_190_6) & c_ssorted(all_190_8) & % 35.52/5.75 | c_ssorted(all_190_9) & ! [v0: c_ssorted] : ( ~ (c_sort(all_190_13, % 35.52/5.75 | all_190_0) = v0) | ? [v1: c_unique] : ? [v2: c_ssorted] : ? % 35.52/5.75 | [v3: int] : ? [v4: int] : ? [v5: int] : ? [v6: c_unique] : ? [v7: % 35.52/5.75 | c_ssorted] : ? [v8: c_unique] : ? [v9: int] : ? [v10: int] : ? % 35.52/5.75 | [v11: int] : (all_190_4 = 1 & ~ (v11 = 0) & whydivide(v5, 10000) = % 35.52/5.75 | v9 & whydivide($sum($product(10000, v3), all_190_3), 1) = v5 & % 35.52/5.75 | %(v5, 10000) = v10 & %($sum($product(10000, v3), all_190_3), 1) = % 35.52/5.75 | v4 & %($sum(all_190_5, -14), 14) = v11 & upd(all_190_1, v0, v7) = % 35.52/5.75 | v8 & acc(all_190_1, v0) = v1 & shift(all_190_8, 1) = all_190_0 & % 35.52/5.75 | valid(all_190_9, v0) = 0 & int2U(v4) = v6 & ss2Int(v2) = v3 & % 35.52/5.75 | c_sort(c_int, v6) = v7 & c_sort(c_int, v1) = v2 & c_unique(v8) & % 35.52/5.75 | c_unique(v6) & c_unique(v1) & c_ssorted(v7) & c_ssorted(v2))) & ? % 35.52/5.75 | [v0: c_ssorted] : ? [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: int] % 35.52/5.75 | : ? [v4: int] : ? [v5: int] : ? [v6: c_unique] : ? [v7: c_ssorted] % 35.52/5.75 | : ? [v8: c_unique] : ? [v9: int] : ? [v10: int] : ? [v11: int] : % 35.52/5.75 | (all_190_4 = 1 & ~ (v11 = 0) & whydivide(v5, 10000) = v9 & % 35.52/5.75 | whydivide($sum($product(10000, v3), all_190_3), 1) = v5 & %(v5, % 35.52/5.75 | 10000) = v10 & %($sum($product(10000, v3), all_190_3), 1) = v4 & % 35.52/5.75 | %($sum(all_190_5, -14), 14) = v11 & upd(all_190_1, v0, v7) = v8 & % 35.52/5.75 | acc(all_190_1, v0) = v1 & shift(all_190_8, 1) = all_190_0 & % 35.52/5.75 | valid(all_190_9, v0) = 0 & int2U(v4) = v6 & ss2Int(v2) = v3 & % 35.52/5.75 | c_sort(all_190_13, all_190_0) = v0 & c_sort(c_int, v6) = v7 & % 35.52/5.75 | c_sort(c_int, v1) = v2 & c_unique(v8) & c_unique(v6) & c_unique(v1) & % 35.52/5.75 | c_ssorted(v7) & c_ssorted(v2) & c_ssorted(v0)) & ? [v0: int] : ? % 35.52/5.75 | [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: c_unique] : ? [v4: % 35.52/5.75 | c_ssorted] : ? [v5: int] : (acc(all_190_6, v2) = v3 & % 35.52/5.75 | shift(all_190_8, v0) = v1 & ss2Int(v4) = v5 & c_sort(all_190_13, v1) % 35.52/5.75 | = v2 & c_sort(c_int, v3) = v4 & c_unique(v3) & c_unique(v1) & % 35.52/5.75 | c_ssorted(v4) & c_ssorted(v2) & (v5 = 2000 | ~ ($lesseq(v0, 2799)) | % 35.52/5.75 | ~ ($lesseq(0, v0)))) % 35.52/5.75 | % 35.52/5.75 | ALPHA: (4) implies: % 35.52/5.75 | (5) %(all_190_5, 14) = 0 % 35.52/5.75 | (6) ! [v0: c_ssorted] : ( ~ (c_sort(all_190_13, all_190_0) = v0) | ? [v1: % 35.52/5.75 | c_unique] : ? [v2: c_ssorted] : ? [v3: int] : ? [v4: int] : ? % 35.52/5.75 | [v5: int] : ? [v6: c_unique] : ? [v7: c_ssorted] : ? [v8: % 35.52/5.75 | c_unique] : ? [v9: int] : ? [v10: int] : ? [v11: int] : % 35.52/5.75 | (all_190_4 = 1 & ~ (v11 = 0) & whydivide(v5, 10000) = v9 & % 35.52/5.75 | whydivide($sum($product(10000, v3), all_190_3), 1) = v5 & %(v5, % 35.52/5.75 | 10000) = v10 & %($sum($product(10000, v3), all_190_3), 1) = v4 & % 35.52/5.75 | %($sum(all_190_5, -14), 14) = v11 & upd(all_190_1, v0, v7) = v8 & % 35.52/5.75 | acc(all_190_1, v0) = v1 & shift(all_190_8, 1) = all_190_0 & % 35.52/5.75 | valid(all_190_9, v0) = 0 & int2U(v4) = v6 & ss2Int(v2) = v3 & % 35.52/5.75 | c_sort(c_int, v6) = v7 & c_sort(c_int, v1) = v2 & c_unique(v8) & % 35.52/5.75 | c_unique(v6) & c_unique(v1) & c_ssorted(v7) & c_ssorted(v2))) % 35.52/5.75 | (7) ? [v0: c_ssorted] : ? [v1: c_unique] : ? [v2: c_ssorted] : ? [v3: % 35.52/5.75 | int] : ? [v4: int] : ? [v5: int] : ? [v6: c_unique] : ? [v7: % 35.52/5.75 | c_ssorted] : ? [v8: c_unique] : ? [v9: int] : ? [v10: int] : ? % 35.52/5.75 | [v11: int] : (all_190_4 = 1 & ~ (v11 = 0) & whydivide(v5, 10000) = v9 % 35.52/5.75 | & whydivide($sum($product(10000, v3), all_190_3), 1) = v5 & %(v5, % 35.52/5.75 | 10000) = v10 & %($sum($product(10000, v3), all_190_3), 1) = v4 & % 35.52/5.75 | %($sum(all_190_5, -14), 14) = v11 & upd(all_190_1, v0, v7) = v8 & % 35.52/5.75 | acc(all_190_1, v0) = v1 & shift(all_190_8, 1) = all_190_0 & % 35.52/5.75 | valid(all_190_9, v0) = 0 & int2U(v4) = v6 & ss2Int(v2) = v3 & % 35.52/5.75 | c_sort(all_190_13, all_190_0) = v0 & c_sort(c_int, v6) = v7 & % 35.52/5.75 | c_sort(c_int, v1) = v2 & c_unique(v8) & c_unique(v6) & c_unique(v1) & % 35.52/5.75 | c_ssorted(v7) & c_ssorted(v2) & c_ssorted(v0)) % 35.52/5.75 | % 35.52/5.75 | DELTA: instantiating (7) with fresh symbols all_200_0, all_200_1, all_200_2, % 35.52/5.75 | all_200_3, all_200_4, all_200_5, all_200_6, all_200_7, all_200_8, % 35.52/5.75 | all_200_9, all_200_10, all_200_11 gives: % 35.52/5.76 | (8) all_190_4 = 1 & ~ (all_200_0 = 0) & whydivide(all_200_6, 10000) = % 35.52/5.76 | all_200_2 & whydivide($sum($product(10000, all_200_8), all_190_3), 1) = % 35.52/5.76 | all_200_6 & %(all_200_6, 10000) = all_200_1 & %($sum($product(10000, % 35.52/5.76 | all_200_8), all_190_3), 1) = all_200_7 & %($sum(all_190_5, -14), % 35.52/5.76 | 14) = all_200_0 & upd(all_190_1, all_200_11, all_200_4) = all_200_3 & % 35.52/5.76 | acc(all_190_1, all_200_11) = all_200_10 & shift(all_190_8, 1) = % 35.52/5.76 | all_190_0 & valid(all_190_9, all_200_11) = 0 & int2U(all_200_7) = % 35.52/5.76 | all_200_5 & ss2Int(all_200_9) = all_200_8 & c_sort(all_190_13, % 35.52/5.76 | all_190_0) = all_200_11 & c_sort(c_int, all_200_5) = all_200_4 & % 35.52/5.76 | c_sort(c_int, all_200_10) = all_200_9 & c_unique(all_200_3) & % 35.52/5.76 | c_unique(all_200_5) & c_unique(all_200_10) & c_ssorted(all_200_4) & % 35.52/5.76 | c_ssorted(all_200_9) & c_ssorted(all_200_11) % 35.52/5.76 | % 35.52/5.76 | ALPHA: (8) implies: % 35.52/5.76 | (9) ~ (all_200_0 = 0) % 35.52/5.76 | (10) c_sort(all_190_13, all_190_0) = all_200_11 % 35.52/5.76 | (11) %($sum(all_190_5, -14), 14) = all_200_0 % 35.52/5.76 | % 35.52/5.76 | GROUND_INST: instantiating (6) with all_200_11, simplifying with (10) gives: % 35.52/5.76 | (12) ? [v0: c_unique] : ? [v1: c_ssorted] : ? [v2: int] : ? [v3: int] : % 35.52/5.76 | ? [v4: int] : ? [v5: c_unique] : ? [v6: c_ssorted] : ? [v7: % 35.52/5.76 | c_unique] : ? [v8: int] : ? [v9: int] : ? [v10: int] : (all_190_4 % 35.52/5.76 | = 1 & ~ (v10 = 0) & whydivide(v4, 10000) = v8 & % 35.52/5.76 | whydivide($sum($product(10000, v2), all_190_3), 1) = v4 & %(v4, % 35.52/5.76 | 10000) = v9 & %($sum($product(10000, v2), all_190_3), 1) = v3 & % 35.52/5.76 | %($sum(all_190_5, -14), 14) = v10 & upd(all_190_1, all_200_11, v6) = % 35.52/5.76 | v7 & acc(all_190_1, all_200_11) = v0 & shift(all_190_8, 1) = % 35.52/5.76 | all_190_0 & valid(all_190_9, all_200_11) = 0 & int2U(v3) = v5 & % 35.52/5.76 | ss2Int(v1) = v2 & c_sort(c_int, v5) = v6 & c_sort(c_int, v0) = v1 & % 35.52/5.76 | c_unique(v7) & c_unique(v5) & c_unique(v0) & c_ssorted(v6) & % 35.52/5.76 | c_ssorted(v1)) % 35.52/5.76 | % 35.52/5.76 | GROUND_INST: instantiating (1) with all_190_5, simplifying with (5) gives: % 35.52/5.76 | (13) %($sum(all_190_5, -14), 14) = 0 % 35.52/5.76 | % 35.52/5.76 | DELTA: instantiating (12) with fresh symbols all_294_0, all_294_1, all_294_2, % 35.52/5.76 | all_294_3, all_294_4, all_294_5, all_294_6, all_294_7, all_294_8, % 35.52/5.76 | all_294_9, all_294_10 gives: % 35.52/5.76 | (14) all_190_4 = 1 & ~ (all_294_0 = 0) & whydivide(all_294_6, 10000) = % 35.52/5.76 | all_294_2 & whydivide($sum($product(10000, all_294_8), all_190_3), 1) % 35.52/5.76 | = all_294_6 & %(all_294_6, 10000) = all_294_1 & %($sum($product(10000, % 35.52/5.76 | all_294_8), all_190_3), 1) = all_294_7 & %($sum(all_190_5, -14), % 35.52/5.76 | 14) = all_294_0 & upd(all_190_1, all_200_11, all_294_4) = all_294_3 % 35.52/5.76 | & acc(all_190_1, all_200_11) = all_294_10 & shift(all_190_8, 1) = % 35.52/5.76 | all_190_0 & valid(all_190_9, all_200_11) = 0 & int2U(all_294_7) = % 35.52/5.76 | all_294_5 & ss2Int(all_294_9) = all_294_8 & c_sort(c_int, all_294_5) = % 35.52/5.76 | all_294_4 & c_sort(c_int, all_294_10) = all_294_9 & % 35.52/5.76 | c_unique(all_294_3) & c_unique(all_294_5) & c_unique(all_294_10) & % 35.52/5.76 | c_ssorted(all_294_4) & c_ssorted(all_294_9) % 35.52/5.76 | % 35.52/5.76 | ALPHA: (14) implies: % 35.52/5.76 | (15) %($sum(all_190_5, -14), 14) = all_294_0 % 35.52/5.76 | % 35.52/5.76 | GROUND_INST: instantiating (3) with all_200_0, all_294_0, 14, $sum(all_190_5, % 35.52/5.76 | -14), simplifying with (11), (15) gives: % 35.52/5.76 | (16) all_294_0 = all_200_0 % 35.52/5.76 | % 35.52/5.76 | GROUND_INST: instantiating (3) with 0, all_294_0, 14, $sum(all_190_5, -14), % 35.52/5.76 | simplifying with (13), (15) gives: % 35.52/5.76 | (17) all_294_0 = 0 % 35.52/5.76 | % 35.52/5.76 | COMBINE_EQS: (16), (17) imply: % 35.52/5.76 | (18) all_200_0 = 0 % 35.52/5.76 | % 35.52/5.76 | SIMP: (18) implies: % 35.52/5.76 | (19) all_200_0 = 0 % 35.52/5.76 | % 35.52/5.76 | REDUCE: (9), (19) imply: % 35.52/5.76 | (20) $false % 35.52/5.76 | % 35.52/5.77 | CLOSE: (20) is inconsistent. % 35.52/5.77 | % 35.52/5.77 End of proof % 35.52/5.77 % SZS output end Proof for theBenchmark % 35.52/5.77 % 35.52/5.77 5155ms %------------------------------------------------------------------------------