%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW620_2 : TPTP v8.1.2. Released v6.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:55 EDT 2023 % Result : Theorem 14.65s 2.69s % Output : Proof 19.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWW620_2 : TPTP v8.1.2. Released v6.1.0. % 0.10/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Aug 27 21:17:55 EDT 2023 % 0.13/0.33 % CPUTime : % 0.60/0.60 ________ _____ % 0.60/0.60 ___ __ \_________(_)________________________________ % 0.60/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.60/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.60/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.60/0.60 % 0.60/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.60/0.60 (2023-06-19) % 0.60/0.60 % 0.60/0.60 (c) Philipp Rümmer, 2009-2023 % 0.60/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.60/0.60 Amanda Stjerna. % 0.60/0.60 Free software under BSD-3-Clause. % 0.60/0.60 % 0.60/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.60/0.60 % 0.60/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.65/0.61 Running up to 7 provers in parallel. % 0.65/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.65/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.65/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.65/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.65/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.65/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.65/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.38/1.47 Prover 0: Preprocessing ... % 5.38/1.47 Prover 5: Preprocessing ... % 5.38/1.47 Prover 4: Preprocessing ... % 5.38/1.47 Prover 3: Preprocessing ... % 5.38/1.47 Prover 6: Preprocessing ... % 5.56/1.49 Prover 2: Preprocessing ... % 5.56/1.51 Prover 1: Preprocessing ... % 12.30/2.38 Prover 1: Warning: ignoring some quantifiers % 12.54/2.46 Prover 3: Warning: ignoring some quantifiers % 12.54/2.47 Prover 1: Constructing countermodel ... % 12.54/2.49 Prover 3: Constructing countermodel ... % 13.22/2.53 Prover 4: Warning: ignoring some quantifiers % 13.22/2.56 Prover 6: Proving ... % 13.22/2.57 Prover 4: Constructing countermodel ... % 13.87/2.64 Prover 0: Proving ... % 13.87/2.68 Prover 5: Proving ... % 14.65/2.69 Prover 3: proved (2071ms) % 14.65/2.69 % 14.65/2.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.65/2.69 % 14.65/2.69 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.74/2.70 Prover 0: stopped % 14.74/2.70 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 14.74/2.70 Prover 5: stopped % 14.74/2.71 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.86/2.71 Prover 6: stopped % 14.94/2.73 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.94/2.78 Prover 2: Proving ... % 14.94/2.78 Prover 2: stopped % 14.94/2.79 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.94/2.80 Prover 1: Found proof (size 21) % 14.94/2.80 Prover 1: proved (2182ms) % 14.94/2.80 Prover 4: stopped % 16.28/2.92 Prover 10: Preprocessing ... % 16.28/2.94 Prover 7: Preprocessing ... % 16.28/2.97 Prover 11: Preprocessing ... % 16.28/2.97 Prover 8: Preprocessing ... % 16.99/2.99 Prover 13: Preprocessing ... % 16.99/2.99 Prover 10: stopped % 17.10/3.01 Prover 7: stopped % 17.20/3.04 Prover 11: stopped % 17.20/3.07 Prover 13: stopped % 18.20/3.26 Prover 8: Warning: ignoring some quantifiers % 18.64/3.29 Prover 8: Constructing countermodel ... % 18.76/3.31 Prover 8: stopped % 18.76/3.31 % 18.76/3.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.76/3.31 % 18.76/3.31 % SZS output start Proof for theBenchmark % 18.82/3.33 Assumptions after simplification: % 18.82/3.33 --------------------------------- % 18.82/3.33 % 18.82/3.33 (refl4) % 18.82/3.36 ! [v0: elt6] : ! [v1: int] : (v1 = 0 | ~ (le4(v0, v0) = v1) | ~ elt6(v0)) % 18.82/3.36 % 18.82/3.36 (sorted_sub_def3) % 18.82/3.37 ty(elt7) & ! [v0: array_elt3] : ! [v1: int] : ! [v2: int] : ! [v3: int] : % 18.82/3.37 (v3 = 0 | ~ (sorted_sub4(v0, v1, v2) = v3) | ~ array_elt3(v0) | ? [v4: uni] % 18.82/3.37 : (t2tb10(v0) = v4 & uni(v4) & ? [v5: int] : ? [v6: int] : ? [v7: uni] : % 18.82/3.37 ? [v8: elt6] : ? [v9: uni] : ? [v10: elt6] : ? [v11: int] : ( ~ (v11 = % 18.82/3.37 0) & $lesseq(1, $difference(v2, v6)) & $lesseq(v5, v6) & $lesseq(v1, % 18.82/3.37 v5) & tb2t11(v9) = v10 & tb2t11(v7) = v8 & le4(v8, v10) = v11 & % 18.82/3.37 get2(elt7, v4, v6) = v9 & get2(elt7, v4, v5) = v7 & elt6(v10) & elt6(v8) % 18.82/3.37 & uni(v9) & uni(v7)))) & ! [v0: array_elt3] : ! [v1: int] : ! [v2: % 18.82/3.37 int] : ( ~ (sorted_sub4(v0, v1, v2) = 0) | ~ array_elt3(v0) | ? [v3: uni] % 18.82/3.37 : (t2tb10(v0) = v3 & uni(v3) & ! [v4: int] : ! [v5: int] : ! [v6: uni] : % 18.82/3.37 ! [v7: elt6] : ! [v8: uni] : ! [v9: elt6] : ! [v10: int] : (v10 = 0 | % 18.82/3.37 ~ ($lesseq(1, $difference(v2, v5))) | ~ ($lesseq(v4, v5)) | ~ % 18.82/3.37 ($lesseq(v1, v4)) | ~ (tb2t11(v8) = v9) | ~ (tb2t11(v6) = v7) | ~ % 18.82/3.37 (le4(v7, v9) = v10) | ~ (get2(elt7, v3, v5) = v8) | ~ (get2(elt7, v3, % 18.82/3.37 v4) = v6)))) % 18.82/3.37 % 18.82/3.37 (wP_parameter_find_run) % 18.82/3.38 ty(elt7) & ? [v0: int] : ? [v1: map_int_elt3] : ? [v2: int] : ? [v3: uni] % 18.82/3.38 : ? [v4: uni] : ? [v5: array_elt3] : ? [v6: int] : ( ~ (v6 = 0) & % 18.82/3.38 $lesseq(1, $difference(v0, v2)) & $lesseq(0, v2) & t2tb12(v1) = v3 & % 18.82/3.38 sorted_sub4(v5, v2, $sum(v2, 1)) = v6 & tb2t10(v4) = v5 & mk_array1(elt7, % 18.82/3.38 v0, v3) = v4 & map_int_elt3(v1) & array_elt3(v5) & uni(v4) & uni(v3)) % 18.82/3.38 % 18.82/3.38 (function-axioms) % 18.82/3.40 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 18.82/3.40 [v3: int] : ! [v4: int] : ! [v5: int] : ! [v6: uni] : ! [v7: uni] : ! % 18.82/3.40 [v8: ty] : (v1 = v0 | ~ (exchange2(v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 18.82/3.40 (exchange2(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 18.82/3.40 ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! % 18.82/3.40 [v5: uni] : ! [v6: ty] : (v1 = v0 | ~ (permut_sub1(v6, v5, v4, v3, v2) = v1) % 18.82/3.40 | ~ (permut_sub1(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 18.82/3.40 ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! % 18.82/3.40 [v5: uni] : ! [v6: ty] : (v1 = v0 | ~ (permut3(v6, v5, v4, v3, v2) = v1) | % 18.82/3.40 ~ (permut3(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.82/3.40 MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! [v5: % 18.82/3.40 uni] : ! [v6: ty] : (v1 = v0 | ~ (exchange3(v6, v5, v4, v3, v2) = v1) | ~ % 18.82/3.40 (exchange3(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.82/3.40 MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! [v5: % 18.82/3.40 uni] : ! [v6: ty] : (v1 = v0 | ~ (array_eq_sub1(v6, v5, v4, v3, v2) = v1) % 18.82/3.40 | ~ (array_eq_sub1(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 18.82/3.40 : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! % 18.82/3.40 [v5: uni] : ! [v6: ty] : (v1 = v0 | ~ (map_eq_sub1(v6, v5, v4, v3, v2) = v1) % 18.82/3.40 | ~ (map_eq_sub1(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 18.82/3.40 ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: uni] : ! % 18.82/3.40 [v5: uni] : ! [v6: ty] : (v1 = v0 | ~ (permut2(v6, v5, v4, v3, v2) = v1) | % 18.82/3.40 ~ (permut2(v6, v5, v4, v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 18.82/3.40 [v2: int] : ! [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: ty] : (v1 = % 18.82/3.40 v0 | ~ (occ1(v6, v5, v4, v3, v2) = v1) | ~ (occ1(v6, v5, v4, v3, v2) = % 18.82/3.40 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 18.82/3.40 uni] : ! [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = % 18.82/3.40 v1) | ~ (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : % 18.82/3.40 ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ % 18.82/3.40 (set2(v5, v4, v3, v2) = v1) | ~ (set2(v5, v4, v3, v2) = v0)) & ! [v0: uni] % 18.82/3.40 : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 % 18.82/3.40 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! % 18.82/3.40 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! % 18.82/3.40 [v5: ty] : (v1 = v0 | ~ (match_bool1(v5, v4, v3, v2) = v1) | ~ % 18.82/3.40 (match_bool1(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.82/3.40 MultipleValueBool] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 18.82/3.40 ~ (permut_all(v4, v3, v2) = v1) | ~ (permut_all(v4, v3, v2) = v0)) & ! % 18.82/3.40 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: % 18.82/3.40 uni] : ! [v4: ty] : (v1 = v0 | ~ (array_eq(v4, v3, v2) = v1) | ~ % 18.82/3.40 (array_eq(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.82/3.40 MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: array_elt3] : (v1 % 18.82/3.40 = v0 | ~ (sorted_sub4(v4, v3, v2) = v1) | ~ (sorted_sub4(v4, v3, v2) = % 18.82/3.40 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: % 18.82/3.40 ty] : (v1 = v0 | ~ (make1(v4, v3, v2) = v1) | ~ (make1(v4, v3, v2) = v0)) % 18.82/3.40 & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] : % 18.82/3.40 (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) & ! [v0: % 18.82/3.40 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : (v1 = v0 | % 18.82/3.40 ~ (mk_array1(v4, v3, v2) = v1) | ~ (mk_array1(v4, v3, v2) = v0)) & ! [v0: % 18.82/3.40 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | % 18.82/3.40 ~ (const(v4, v3, v2) = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: int] : % 18.82/3.40 ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (min(v3, v2) = v1) | % 18.82/3.40 ~ (min(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 18.82/3.40 [v3: int] : (v1 = v0 | ~ (max(v3, v2) = v1) | ~ (max(v3, v2) = v0)) & ! % 18.82/3.40 [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ % 18.82/3.40 (mod(v3, v2) = v1) | ~ (mod(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : % 18.82/3.40 ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (div(v3, v2) = v1) | ~ (div(v3, % 18.82/3.40 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : % 18.82/3.40 (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ (contents(v3, v2) = v0)) & ! [v0: % 18.82/3.40 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, % 18.82/3.40 v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 18.82/3.40 [v1: MultipleValueBool] : ! [v2: elt6] : ! [v3: elt6] : (v1 = v0 | ~ % 18.82/3.40 (le4(v3, v2) = v1) | ~ (le4(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : % 18.82/3.40 ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (elts(v3, v2) = v1) | ~ (elts(v3, % 18.82/3.40 v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : % 18.82/3.40 (v1 = v0 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) & ! [v0: % 18.82/3.40 ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, v2) = % 18.82/3.40 v1) | ~ (map(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.82/3.40 MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (sort1(v3, % 18.82/3.40 v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! [v0: map_int_elt3] : ! [v1: % 18.82/3.40 map_int_elt3] : ! [v2: uni] : (v1 = v0 | ~ (tb2t12(v2) = v1) | ~ % 18.82/3.40 (tb2t12(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: map_int_elt3] : % 18.82/3.40 (v1 = v0 | ~ (t2tb12(v2) = v1) | ~ (t2tb12(v2) = v0)) & ! [v0: int] : ! % 18.82/3.40 [v1: int] : ! [v2: int] : (v1 = v0 | ~ (abs(v2) = v1) | ~ (abs(v2) = v0)) & % 18.82/3.40 ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (ref(v2) = v1) | ~ % 18.82/3.40 (ref(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 18.82/3.40 ! [v2: array_elt3] : (v1 = v0 | ~ (sorted4(v2) = v1) | ~ (sorted4(v2) = v0)) % 18.82/3.40 & ! [v0: elt6] : ! [v1: elt6] : ! [v2: uni] : (v1 = v0 | ~ (tb2t11(v2) = % 18.82/3.40 v1) | ~ (tb2t11(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: elt6] % 18.82/3.40 : (v1 = v0 | ~ (t2tb11(v2) = v1) | ~ (t2tb11(v2) = v0)) & ! [v0: % 18.82/3.40 array_elt3] : ! [v1: array_elt3] : ! [v2: uni] : (v1 = v0 | ~ (tb2t10(v2) % 18.82/3.40 = v1) | ~ (tb2t10(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 18.82/3.40 array_elt3] : (v1 = v0 | ~ (t2tb10(v2) = v1) | ~ (t2tb10(v2) = v0)) & ! % 18.82/3.40 [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ % 18.82/3.40 (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | % 18.82/3.40 ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! % 18.82/3.40 [v2: ty] : (v1 = v0 | ~ (array(v2) = v1) | ~ (array(v2) = v0)) & ! [v0: % 18.82/3.40 uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (witness1(v2) = v1) | ~ % 18.82/3.40 (witness1(v2) = v0)) % 18.82/3.40 % 18.82/3.40 Further assumptions not needed in the proof: % 18.82/3.40 -------------------------------------------- % 18.82/3.40 abs_def, abs_le, abs_pos, array_eq_def, array_eq_sub_def, array_inversion1, % 18.82/3.40 bool_inversion, bridgeL, bridgeL10, bridgeL11, bridgeL12, bridgeR, bridgeR10, % 18.82/3.40 bridgeR11, bridgeR12, compatOrderMult, const, const_sort4, contents_def4, % 18.82/3.40 contents_sort4, div_1, div_bound, div_inf, div_mod, div_mult, div_sign_neg, % 18.82/3.40 div_sign_pos, elts_def1, elts_sort4, exchange_def, exchange_def1, % 18.82/3.40 exchange_permut_all, exchange_permut_sub, exchange_set, get_def, get_sort8, % 18.82/3.40 get_sort9, length_def1, make_def, make_sort4, map_eq_sub_def, match_bool_False, % 18.82/3.40 match_bool_True, match_bool_sort4, max_is_ge, max_is_some, max_sym, max_x, % 18.82/3.40 max_y, min_is_le, min_is_some, min_sym, min_x, min_y, mk_array_sort4, % 18.82/3.40 mk_ref_sort4, mod_1, mod_bound, mod_inf, mod_mult, mod_sign_neg, mod_sign_pos, % 18.82/3.40 occ_append, occ_bounds, occ_empty, occ_eq, occ_exists, occ_neq, occ_pos, % 18.82/3.40 occ_right_add, occ_right_no_add, permut_all_def, permut_def, permut_def1, % 18.82/3.40 permut_exists, permut_sub_def, permut_sub_weakening, permut_trans, % 18.82/3.40 ref_inversion4, rounds_toward_zero, select_eq, select_neq, set_def, set_sort8, % 18.82/3.40 set_sort9, sorted_def3, t2tb_sort12, t2tb_sort13, t2tb_sort14, t2tb_sort15, % 18.82/3.40 total4, trans4, true_False, tuple0_inversion, witness_sort1 % 18.82/3.40 % 18.82/3.40 Those formulas are unsatisfiable: % 18.82/3.40 --------------------------------- % 18.82/3.40 % 18.82/3.40 Begin of proof % 18.82/3.40 | % 18.82/3.40 | ALPHA: (sorted_sub_def3) implies: % 18.82/3.41 | (1) ! [v0: array_elt3] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v3 % 18.82/3.41 | = 0 | ~ (sorted_sub4(v0, v1, v2) = v3) | ~ array_elt3(v0) | ? [v4: % 18.82/3.41 | uni] : (t2tb10(v0) = v4 & uni(v4) & ? [v5: int] : ? [v6: int] : % 18.82/3.41 | ? [v7: uni] : ? [v8: elt6] : ? [v9: uni] : ? [v10: elt6] : ? % 18.82/3.41 | [v11: int] : ( ~ (v11 = 0) & $lesseq(1, $difference(v2, v6)) & % 18.82/3.41 | $lesseq(v5, v6) & $lesseq(v1, v5) & tb2t11(v9) = v10 & tb2t11(v7) % 18.82/3.41 | = v8 & le4(v8, v10) = v11 & get2(elt7, v4, v6) = v9 & get2(elt7, % 18.82/3.41 | v4, v5) = v7 & elt6(v10) & elt6(v8) & uni(v9) & uni(v7)))) % 18.82/3.41 | % 18.82/3.41 | ALPHA: (wP_parameter_find_run) implies: % 18.82/3.41 | (2) ? [v0: int] : ? [v1: map_int_elt3] : ? [v2: int] : ? [v3: uni] : ? % 18.82/3.41 | [v4: uni] : ? [v5: array_elt3] : ? [v6: int] : ( ~ (v6 = 0) & % 18.82/3.41 | $lesseq(1, $difference(v0, v2)) & $lesseq(0, v2) & t2tb12(v1) = v3 & % 18.82/3.41 | sorted_sub4(v5, v2, $sum(v2, 1)) = v6 & tb2t10(v4) = v5 & % 18.82/3.41 | mk_array1(elt7, v0, v3) = v4 & map_int_elt3(v1) & array_elt3(v5) & % 18.82/3.41 | uni(v4) & uni(v3)) % 18.82/3.41 | % 18.82/3.41 | ALPHA: (function-axioms) implies: % 18.82/3.41 | (3) ! [v0: elt6] : ! [v1: elt6] : ! [v2: uni] : (v1 = v0 | ~ % 18.82/3.41 | (tb2t11(v2) = v1) | ~ (tb2t11(v2) = v0)) % 18.82/3.41 | (4) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] % 18.82/3.41 | : (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) % 18.82/3.41 | % 18.82/3.41 | DELTA: instantiating (2) with fresh symbols all_124_0, all_124_1, all_124_2, % 18.82/3.41 | all_124_3, all_124_4, all_124_5, all_124_6 gives: % 18.82/3.41 | (5) ~ (all_124_0 = 0) & $lesseq(1, $difference(all_124_6, all_124_4)) & % 18.82/3.41 | $lesseq(0, all_124_4) & t2tb12(all_124_5) = all_124_3 & % 18.82/3.41 | sorted_sub4(all_124_1, all_124_4, $sum(all_124_4, 1)) = all_124_0 & % 18.82/3.41 | tb2t10(all_124_2) = all_124_1 & mk_array1(elt7, all_124_6, all_124_3) = % 18.82/3.41 | all_124_2 & map_int_elt3(all_124_5) & array_elt3(all_124_1) & % 18.82/3.41 | uni(all_124_2) & uni(all_124_3) % 18.82/3.41 | % 18.82/3.41 | ALPHA: (5) implies: % 18.82/3.41 | (6) ~ (all_124_0 = 0) % 18.82/3.41 | (7) array_elt3(all_124_1) % 18.82/3.41 | (8) sorted_sub4(all_124_1, all_124_4, $sum(all_124_4, 1)) = all_124_0 % 18.82/3.41 | % 18.82/3.41 | GROUND_INST: instantiating (1) with all_124_1, all_124_4, $sum(all_124_4, 1), % 18.82/3.41 | all_124_0, simplifying with (7), (8) gives: % 18.82/3.41 | (9) all_124_0 = 0 | ? [v0: uni] : (t2tb10(all_124_1) = v0 & uni(v0) & ? % 18.82/3.41 | [v1: uni] : ? [v2: elt6] : ? [v3: uni] : ? [v4: elt6] : ? [v5: % 18.82/3.41 | int] : ( ~ (v5 = 0) & tb2t11(v3) = v4 & tb2t11(v1) = v2 & le4(v2, % 18.82/3.41 | v4) = v5 & get2(elt7, v0, all_124_4) = v3 & get2(elt7, v0, % 18.82/3.41 | all_124_4) = v1 & elt6(v4) & elt6(v2) & uni(v3) & uni(v1))) % 18.82/3.41 | % 18.82/3.41 | BETA: splitting (9) gives: % 18.82/3.41 | % 18.82/3.41 | Case 1: % 18.82/3.41 | | % 18.82/3.42 | | (10) all_124_0 = 0 % 18.82/3.42 | | % 18.82/3.42 | | REDUCE: (6), (10) imply: % 18.82/3.42 | | (11) $false % 18.82/3.42 | | % 18.82/3.42 | | CLOSE: (11) is inconsistent. % 18.82/3.42 | | % 18.82/3.42 | Case 2: % 18.82/3.42 | | % 18.82/3.42 | | (12) ? [v0: uni] : (t2tb10(all_124_1) = v0 & uni(v0) & ? [v1: uni] : ? % 18.82/3.42 | | [v2: elt6] : ? [v3: uni] : ? [v4: elt6] : ? [v5: int] : ( ~ (v5 % 18.82/3.42 | | = 0) & tb2t11(v3) = v4 & tb2t11(v1) = v2 & le4(v2, v4) = v5 & % 18.82/3.42 | | get2(elt7, v0, all_124_4) = v3 & get2(elt7, v0, all_124_4) = v1 % 18.82/3.42 | | & elt6(v4) & elt6(v2) & uni(v3) & uni(v1))) % 18.82/3.42 | | % 18.82/3.42 | | DELTA: instantiating (12) with fresh symbol all_145_0 gives: % 18.82/3.42 | | (13) t2tb10(all_124_1) = all_145_0 & uni(all_145_0) & ? [v0: uni] : ? % 18.82/3.42 | | [v1: elt6] : ? [v2: uni] : ? [v3: elt6] : ? [v4: int] : ( ~ (v4 = % 18.82/3.42 | | 0) & tb2t11(v2) = v3 & tb2t11(v0) = v1 & le4(v1, v3) = v4 & % 18.82/3.42 | | get2(elt7, all_145_0, all_124_4) = v2 & get2(elt7, all_145_0, % 18.82/3.42 | | all_124_4) = v0 & elt6(v3) & elt6(v1) & uni(v2) & uni(v0)) % 18.82/3.42 | | % 18.82/3.42 | | ALPHA: (13) implies: % 18.82/3.42 | | (14) ? [v0: uni] : ? [v1: elt6] : ? [v2: uni] : ? [v3: elt6] : ? % 18.82/3.42 | | [v4: int] : ( ~ (v4 = 0) & tb2t11(v2) = v3 & tb2t11(v0) = v1 & % 18.82/3.42 | | le4(v1, v3) = v4 & get2(elt7, all_145_0, all_124_4) = v2 & % 18.82/3.42 | | get2(elt7, all_145_0, all_124_4) = v0 & elt6(v3) & elt6(v1) & % 18.82/3.42 | | uni(v2) & uni(v0)) % 18.82/3.42 | | % 19.30/3.42 | | DELTA: instantiating (14) with fresh symbols all_147_0, all_147_1, % 19.30/3.42 | | all_147_2, all_147_3, all_147_4 gives: % 19.30/3.42 | | (15) ~ (all_147_0 = 0) & tb2t11(all_147_2) = all_147_1 & % 19.30/3.42 | | tb2t11(all_147_4) = all_147_3 & le4(all_147_3, all_147_1) = % 19.30/3.42 | | all_147_0 & get2(elt7, all_145_0, all_124_4) = all_147_2 & % 19.30/3.42 | | get2(elt7, all_145_0, all_124_4) = all_147_4 & elt6(all_147_1) & % 19.30/3.42 | | elt6(all_147_3) & uni(all_147_2) & uni(all_147_4) % 19.30/3.42 | | % 19.30/3.42 | | ALPHA: (15) implies: % 19.30/3.42 | | (16) ~ (all_147_0 = 0) % 19.30/3.42 | | (17) elt6(all_147_1) % 19.30/3.42 | | (18) get2(elt7, all_145_0, all_124_4) = all_147_4 % 19.30/3.42 | | (19) get2(elt7, all_145_0, all_124_4) = all_147_2 % 19.30/3.42 | | (20) le4(all_147_3, all_147_1) = all_147_0 % 19.30/3.42 | | (21) tb2t11(all_147_4) = all_147_3 % 19.30/3.42 | | (22) tb2t11(all_147_2) = all_147_1 % 19.30/3.42 | | % 19.30/3.42 | | GROUND_INST: instantiating (4) with all_147_4, all_147_2, all_124_4, % 19.30/3.42 | | all_145_0, elt7, simplifying with (18), (19) gives: % 19.30/3.42 | | (23) all_147_2 = all_147_4 % 19.30/3.42 | | % 19.30/3.42 | | REDUCE: (22), (23) imply: % 19.30/3.42 | | (24) tb2t11(all_147_4) = all_147_1 % 19.30/3.42 | | % 19.30/3.42 | | GROUND_INST: instantiating (3) with all_147_3, all_147_1, all_147_4, % 19.30/3.42 | | simplifying with (21), (24) gives: % 19.30/3.42 | | (25) all_147_1 = all_147_3 % 19.30/3.42 | | % 19.30/3.42 | | REDUCE: (20), (25) imply: % 19.30/3.42 | | (26) le4(all_147_3, all_147_3) = all_147_0 % 19.30/3.42 | | % 19.30/3.42 | | REDUCE: (17), (25) imply: % 19.30/3.43 | | (27) elt6(all_147_3) % 19.30/3.43 | | % 19.30/3.43 | | GROUND_INST: instantiating (refl4) with all_147_3, all_147_0, simplifying % 19.30/3.43 | | with (26), (27) gives: % 19.30/3.43 | | (28) all_147_0 = 0 % 19.30/3.43 | | % 19.30/3.43 | | REDUCE: (16), (28) imply: % 19.30/3.43 | | (29) $false % 19.30/3.43 | | % 19.30/3.43 | | CLOSE: (29) is inconsistent. % 19.30/3.43 | | % 19.30/3.43 | End of split % 19.30/3.43 | % 19.30/3.43 End of proof % 19.30/3.43 % SZS output end Proof for theBenchmark % 19.30/3.43 % 19.30/3.43 2827ms %------------------------------------------------------------------------------