%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW657_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 : n014.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:02 EDT 2023 % Result : Theorem 11.22s 2.24s % Output : Proof 22.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW657_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 22:22:16 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.60 ___ __ \_________(_)________________________________ % 0.20/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.60 (2023-06-19) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2023 % 0.20/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.60 Amanda Stjerna. % 0.20/0.60 Free software under BSD-3-Clause. % 0.20/0.60 % 0.20/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.60 % 0.20/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.62 Running up to 7 provers in parallel. % 0.20/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.07/1.13 Prover 6: Preprocessing ... % 3.07/1.13 Prover 3: Preprocessing ... % 3.07/1.13 Prover 1: Preprocessing ... % 3.07/1.14 Prover 0: Preprocessing ... % 3.07/1.14 Prover 2: Preprocessing ... % 3.07/1.14 Prover 5: Preprocessing ... % 3.07/1.14 Prover 4: Preprocessing ... % 5.70/1.63 Prover 1: Warning: ignoring some quantifiers % 6.77/1.68 Prover 4: Warning: ignoring some quantifiers % 6.77/1.68 Prover 3: Warning: ignoring some quantifiers % 6.77/1.69 Prover 6: Proving ... % 7.47/1.71 Prover 3: Constructing countermodel ... % 7.47/1.71 Prover 5: Proving ... % 7.47/1.73 Prover 1: Constructing countermodel ... % 7.47/1.75 Prover 4: Constructing countermodel ... % 7.47/1.76 Prover 0: Proving ... % 7.47/1.80 Prover 2: Proving ... % 11.22/2.24 Prover 0: proved (1613ms) % 11.22/2.24 % 11.22/2.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.22/2.24 % 11.22/2.24 Prover 5: stopped % 11.22/2.24 Prover 2: stopped % 11.22/2.24 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.22/2.24 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.22/2.24 Prover 3: stopped % 11.22/2.24 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 11.22/2.24 Prover 6: stopped % 11.22/2.25 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 11.22/2.26 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 11.90/2.32 Prover 8: Preprocessing ... % 11.90/2.32 Prover 7: Preprocessing ... % 11.90/2.33 Prover 11: Preprocessing ... % 11.90/2.36 Prover 13: Preprocessing ... % 11.90/2.36 Prover 10: Preprocessing ... % 12.65/2.47 Prover 8: Warning: ignoring some quantifiers % 12.65/2.48 Prover 7: Warning: ignoring some quantifiers % 12.65/2.49 Prover 8: Constructing countermodel ... % 13.17/2.51 Prover 7: Constructing countermodel ... % 13.48/2.51 Prover 10: Warning: ignoring some quantifiers % 13.48/2.52 Prover 11: Warning: ignoring some quantifiers % 13.48/2.53 Prover 11: Constructing countermodel ... % 13.48/2.54 Prover 10: Constructing countermodel ... % 13.48/2.56 Prover 13: Warning: ignoring some quantifiers % 13.48/2.58 Prover 13: Constructing countermodel ... % 14.25/2.64 Prover 10: gave up % 14.25/2.64 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.25/2.67 Prover 16: Preprocessing ... % 15.70/2.80 Prover 16: Warning: ignoring some quantifiers % 15.77/2.81 Prover 16: Constructing countermodel ... % 16.54/2.93 Prover 13: gave up % 16.54/2.93 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 16.54/2.96 Prover 19: Preprocessing ... % 17.26/3.02 Prover 7: gave up % 18.02/3.12 Prover 19: Warning: ignoring some quantifiers % 18.02/3.13 Prover 19: Constructing countermodel ... % 21.20/3.57 Prover 16: gave up % 21.88/3.62 Prover 19: Found proof (size 105) % 21.88/3.62 Prover 19: proved (691ms) % 21.88/3.62 Prover 11: stopped % 21.88/3.62 Prover 4: stopped % 21.88/3.62 Prover 8: stopped % 21.88/3.62 Prover 1: stopped % 21.88/3.62 % 21.88/3.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.88/3.62 % 21.88/3.63 % SZS output start Proof for theBenchmark % 21.88/3.64 Assumptions after simplification: % 21.88/3.64 --------------------------------- % 21.88/3.64 % 21.88/3.64 (is_common_prefix_def) % 21.88/3.66 ty(int) & ! [v0: array_int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! % 21.88/3.66 [v4: int] : (v4 = 0 | ~ ($lesseq(0, v3)) | ~ (is_common_prefix1(v0, v1, v2, % 21.88/3.66 v3) = v4) | ~ array_int(v0) | ? [v5: uni] : ? [v6: int] : (t2tb1(v0) % 21.88/3.66 = v5 & length1(int, v5) = v6 & uni(v5) & ( ~ ($lesseq(v2, $difference(v6, % 21.88/3.66 v3))) | ~ ($lesseq(v1, $difference(v6, v3))) | ? [v7: int] : ? % 21.88/3.66 [v8: uni] : ? [v9: int] : ? [v10: uni] : ? [v11: int] : ( ~ (v11 = % 21.88/3.66 v9) & $lesseq(1, $difference(v3, v7)) & $lesseq(0, v7) & tb2t(v10) = % 21.88/3.66 v11 & tb2t(v8) = v9 & get2(int, v5, $sum(v7, v2)) = v10 & get2(int, % 21.88/3.66 v5, $sum(v7, v1)) = v8 & uni(v10) & uni(v8))))) & ! [v0: array_int] % 21.88/3.66 : ! [v1: int] : ! [v2: int] : ! [v3: int] : ( ~ (is_common_prefix1(v0, v1, % 21.88/3.66 v2, v3) = 0) | ~ array_int(v0) | ($lesseq(0, v3) & ? [v4: uni] : ? % 21.88/3.66 [v5: int] : ($lesseq(v2, $difference(v5, v3)) & $lesseq(v1, % 21.88/3.66 $difference(v5, v3)) & t2tb1(v0) = v4 & length1(int, v4) = v5 & % 21.88/3.66 uni(v4) & ! [v6: int] : ! [v7: uni] : ( ~ ($lesseq(1, $difference(v3, % 21.88/3.66 v6))) | ~ ($lesseq(0, v6)) | ~ (get2(int, v4, $sum(v6, v1)) = % 21.88/3.66 v7) | ? [v8: int] : ? [v9: uni] : (tb2t(v9) = v8 & tb2t(v7) = v8 & % 21.88/3.66 get2(int, v4, $sum(v6, v2)) = v9 & uni(v9)))))) & ? [v0: array_int] % 21.88/3.66 : ? [v1: int] : ? [v2: int] : ? [v3: int] : ( ~ array_int(v0) | ? [v4: % 21.88/3.66 any] : ? [v5: uni] : ? [v6: int] : (is_common_prefix1(v0, v1, v2, v3) = % 21.88/3.66 v4 & t2tb1(v0) = v5 & length1(int, v5) = v6 & uni(v5) & ( ~ (v4 = 0) | % 21.88/3.66 ($lesseq(v2, $difference(v6, v3)) & $lesseq(v1, $difference(v6, v3)) & % 21.88/3.66 $lesseq(0, v3) & ? [v7: int] : ( ~ ($lesseq(1, $difference(v3, v7))) % 21.88/3.66 | ~ ($lesseq(0, v7)) | ? [v8: uni] : ? [v9: int] : ? [v10: uni] % 21.88/3.66 : (tb2t(v10) = v9 & tb2t(v8) = v9 & get2(int, v5, $sum(v7, v2)) = % 21.88/3.66 v10 & get2(int, v5, $sum(v7, v1)) = v8 & uni(v10) & uni(v8))))))) % 21.88/3.66 % 21.88/3.66 (is_longest_common_prefix_def) % 21.88/3.66 ! [v0: array_int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] % 21.88/3.66 : (v4 = 0 | ~ (is_longest_common_prefix1(v0, v1, v2, v3) = v4) | ~ % 21.88/3.66 array_int(v0) | ? [v5: int] : ( ~ (v5 = 0) & is_common_prefix1(v0, v1, v2, % 21.88/3.66 v3) = v5) | ? [v5: int] : ($lesseq(1, $difference(v5, v3)) & % 21.88/3.66 is_common_prefix1(v0, v1, v2, v5) = 0)) & ! [v0: array_int] : ! [v1: % 21.88/3.66 int] : ! [v2: int] : ! [v3: int] : ( ~ (is_longest_common_prefix1(v0, v1, % 21.88/3.66 v2, v3) = 0) | ~ array_int(v0) | (is_common_prefix1(v0, v1, v2, v3) = 0 % 21.88/3.66 & ! [v4: int] : ( ~ ($lesseq(1, $difference(v4, v3))) | ~ % 21.88/3.66 (is_common_prefix1(v0, v1, v2, v4) = 0)))) & ? [v0: array_int] : ? % 21.88/3.66 [v1: int] : ? [v2: int] : ? [v3: int] : ( ~ array_int(v0) | ? [v4: any] : % 21.88/3.66 ? [v5: any] : (is_longest_common_prefix1(v0, v1, v2, v3) = v4 & % 21.88/3.66 is_common_prefix1(v0, v1, v2, v3) = v5 & ( ~ (v4 = 0) | (v5 = 0 & ? [v6: % 21.88/3.66 int] : ( ~ ($lesseq(1, $difference(v6, v3))) | ? [v7: int] : ( ~ % 21.88/3.66 (v7 = 0) & is_common_prefix1(v0, v1, v2, v6) = v7)))))) % 21.88/3.66 % 21.88/3.66 (longest_common_prefix_succ) % 21.88/3.67 ? [v0: array_int] : ? [v1: int] : ? [v2: int] : ? [v3: int] : ? [v4: int] % 21.88/3.67 : ? [v5: int] : ( ~ (v5 = 0) & ~ (v4 = 0) & is_longest_common_prefix1(v0, % 21.88/3.67 v1, v2, v3) = v5 & is_common_prefix1(v0, v1, v2, $sum(v3, 1)) = v4 & % 21.88/3.67 is_common_prefix1(v0, v1, v2, v3) = 0 & array_int(v0)) % 21.88/3.67 % 21.88/3.67 (function-axioms) % 21.88/3.67 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 21.88/3.67 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 21.88/3.67 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.88/3.67 MultipleValueBool] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ! [v5: % 21.88/3.67 array_int] : (v1 = v0 | ~ (is_longest_common_prefix1(v5, v4, v3, v2) = v1) % 21.88/3.67 | ~ (is_longest_common_prefix1(v5, v4, v3, v2) = v0)) & ! [v0: % 21.88/3.67 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 21.88/3.67 int] : ! [v4: int] : ! [v5: array_int] : (v1 = v0 | ~ % 21.88/3.67 (is_common_prefix1(v5, v4, v3, v2) = v1) | ~ (is_common_prefix1(v5, v4, v3, % 21.88/3.67 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : % 21.88/3.67 ! [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ (set2(v5, v4, v3, v2) = v1) | ~ % 21.88/3.67 (set2(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 21.88/3.67 ! [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = % 21.88/3.67 v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 21.88/3.67 [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : (v1 = v0 | ~ % 21.88/3.67 (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, v2) = v0)) % 21.88/3.67 & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : % 21.88/3.67 (v1 = v0 | ~ (make1(v4, v3, v2) = v1) | ~ (make1(v4, v3, v2) = v0)) & ! % 21.88/3.67 [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] : (v1 = % 21.88/3.67 v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) & ! [v0: uni] % 21.88/3.68 : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : (v1 = v0 | ~ % 21.88/3.68 (mk_array1(v4, v3, v2) = v1) | ~ (mk_array1(v4, v3, v2) = v0)) & ! [v0: % 21.88/3.68 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | % 21.88/3.68 ~ (const(v4, v3, v2) = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: uni] : % 21.88/3.68 ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (elts(v3, v2) = v1) | % 21.88/3.68 ~ (elts(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! % 21.88/3.68 [v3: ty] : (v1 = v0 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) & % 21.88/3.68 ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, % 21.88/3.68 v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 21.88/3.68 [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 21.88/3.68 (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! [v0: array_int] : ! % 21.88/3.68 [v1: array_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ % 21.88/3.68 (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: array_int] : (v1 = % 21.88/3.68 v0 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: int] : ! [v1: % 21.88/3.68 int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & % 21.88/3.68 ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ % 21.88/3.68 (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ % 21.88/3.68 (array(v2) = v1) | ~ (array(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 21.88/3.68 [v2: ty] : (v1 = v0 | ~ (witness1(v2) = v1) | ~ (witness1(v2) = v0)) % 21.88/3.68 % 21.88/3.68 Further assumptions not needed in the proof: % 21.88/3.68 -------------------------------------------- % 21.88/3.68 array_inversion1, bool_inversion, bridgeL, bridgeL1, bridgeR, bridgeR1, % 21.88/3.68 compatOrderMult, const, const_sort1, elts_def1, elts_sort1, get_def, get_sort2, % 21.88/3.68 get_sort3, length_def1, make_def, make_sort1, match_bool_False, match_bool_True, % 21.88/3.68 match_bool_sort1, mk_array_sort1, not_common_prefix_if_last_char_are_different, % 21.88/3.68 select_eq, select_neq, set_def, set_sort2, set_sort3, t2tb_sort, t2tb_sort1, % 21.88/3.68 true_False, tuple0_inversion, witness_sort1 % 21.88/3.68 % 21.88/3.68 Those formulas are unsatisfiable: % 21.88/3.68 --------------------------------- % 21.88/3.68 % 21.88/3.68 Begin of proof % 21.88/3.68 | % 21.88/3.68 | ALPHA: (is_common_prefix_def) implies: % 21.88/3.68 | (1) ! [v0: array_int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ( ~ % 21.88/3.68 | (is_common_prefix1(v0, v1, v2, v3) = 0) | ~ array_int(v0) | % 21.88/3.68 | ($lesseq(0, v3) & ? [v4: uni] : ? [v5: int] : ($lesseq(v2, % 21.88/3.68 | $difference(v5, v3)) & $lesseq(v1, $difference(v5, v3)) & % 21.88/3.68 | t2tb1(v0) = v4 & length1(int, v4) = v5 & uni(v4) & ! [v6: int] : % 21.88/3.68 | ! [v7: uni] : ( ~ ($lesseq(1, $difference(v3, v6))) | ~ % 21.88/3.68 | ($lesseq(0, v6)) | ~ (get2(int, v4, $sum(v6, v1)) = v7) | ? % 21.88/3.68 | [v8: int] : ? [v9: uni] : (tb2t(v9) = v8 & tb2t(v7) = v8 & % 21.88/3.68 | get2(int, v4, $sum(v6, v2)) = v9 & uni(v9)))))) % 21.88/3.68 | (2) ! [v0: array_int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! % 21.88/3.68 | [v4: int] : (v4 = 0 | ~ ($lesseq(0, v3)) | ~ (is_common_prefix1(v0, % 21.88/3.68 | v1, v2, v3) = v4) | ~ array_int(v0) | ? [v5: uni] : ? [v6: % 21.88/3.68 | int] : (t2tb1(v0) = v5 & length1(int, v5) = v6 & uni(v5) & ( ~ % 21.88/3.68 | ($lesseq(v2, $difference(v6, v3))) | ~ ($lesseq(v1, % 21.88/3.68 | $difference(v6, v3))) | ? [v7: int] : ? [v8: uni] : ? [v9: % 21.88/3.68 | int] : ? [v10: uni] : ? [v11: int] : ( ~ (v11 = v9) & % 21.88/3.68 | $lesseq(1, $difference(v3, v7)) & $lesseq(0, v7) & tb2t(v10) = % 21.88/3.68 | v11 & tb2t(v8) = v9 & get2(int, v5, $sum(v7, v2)) = v10 & % 21.88/3.68 | get2(int, v5, $sum(v7, v1)) = v8 & uni(v10) & uni(v8))))) % 21.88/3.68 | % 21.88/3.68 | ALPHA: (is_longest_common_prefix_def) implies: % 21.88/3.68 | (3) ! [v0: array_int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! % 21.88/3.68 | [v4: int] : (v4 = 0 | ~ (is_longest_common_prefix1(v0, v1, v2, v3) = % 21.88/3.68 | v4) | ~ array_int(v0) | ? [v5: int] : ( ~ (v5 = 0) & % 21.88/3.68 | is_common_prefix1(v0, v1, v2, v3) = v5) | ? [v5: int] : % 21.88/3.68 | ($lesseq(1, $difference(v5, v3)) & is_common_prefix1(v0, v1, v2, v5) % 21.88/3.68 | = 0)) % 21.88/3.68 | % 21.88/3.68 | ALPHA: (function-axioms) implies: % 21.88/3.68 | (4) ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = % 21.88/3.68 | v1) | ~ (tb2t(v2) = v0)) % 21.88/3.68 | (5) ! [v0: uni] : ! [v1: uni] : ! [v2: array_int] : (v1 = v0 | ~ % 21.88/3.68 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 21.88/3.68 | (6) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 21.88/3.68 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) % 22.35/3.68 | (7) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] % 22.35/3.68 | : (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) % 22.35/3.69 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] % 22.35/3.69 | : ! [v3: int] : ! [v4: int] : ! [v5: array_int] : (v1 = v0 | ~ % 22.35/3.69 | (is_common_prefix1(v5, v4, v3, v2) = v1) | ~ (is_common_prefix1(v5, % 22.35/3.69 | v4, v3, v2) = v0)) % 22.35/3.69 | % 22.35/3.69 | DELTA: instantiating (longest_common_prefix_succ) with fresh symbols all_51_0, % 22.35/3.69 | all_51_1, all_51_2, all_51_3, all_51_4, all_51_5 gives: % 22.35/3.69 | (9) ~ (all_51_0 = 0) & ~ (all_51_1 = 0) & % 22.35/3.69 | is_longest_common_prefix1(all_51_5, all_51_4, all_51_3, all_51_2) = % 22.35/3.69 | all_51_0 & is_common_prefix1(all_51_5, all_51_4, all_51_3, % 22.35/3.69 | $sum(all_51_2, 1)) = all_51_1 & is_common_prefix1(all_51_5, all_51_4, % 22.35/3.69 | all_51_3, all_51_2) = 0 & array_int(all_51_5) % 22.35/3.69 | % 22.35/3.69 | ALPHA: (9) implies: % 22.35/3.69 | (10) ~ (all_51_1 = 0) % 22.35/3.69 | (11) ~ (all_51_0 = 0) % 22.35/3.69 | (12) array_int(all_51_5) % 22.35/3.69 | (13) is_common_prefix1(all_51_5, all_51_4, all_51_3, all_51_2) = 0 % 22.35/3.69 | (14) is_common_prefix1(all_51_5, all_51_4, all_51_3, $sum(all_51_2, 1)) = % 22.35/3.69 | all_51_1 % 22.35/3.69 | (15) is_longest_common_prefix1(all_51_5, all_51_4, all_51_3, all_51_2) = % 22.35/3.69 | all_51_0 % 22.35/3.69 | % 22.35/3.69 | GROUND_INST: instantiating (1) with all_51_5, all_51_4, all_51_3, all_51_2, % 22.35/3.69 | simplifying with (12), (13) gives: % 22.35/3.69 | (16) $lesseq(0, all_51_2) & ? [v0: uni] : ? [v1: int] : % 22.35/3.69 | ($lesseq(all_51_3, $difference(v1, all_51_2)) & $lesseq(all_51_4, % 22.35/3.69 | $difference(v1, all_51_2)) & t2tb1(all_51_5) = v0 & length1(int, % 22.35/3.69 | v0) = v1 & uni(v0) & ! [v2: int] : ! [v3: uni] : ( ~ ($lesseq(1, % 22.35/3.69 | $difference(all_51_2, v2))) | ~ ($lesseq(0, v2)) | ~ % 22.35/3.69 | (get2(int, v0, $sum(v2, all_51_4)) = v3) | ? [v4: int] : ? [v5: % 22.35/3.69 | uni] : (tb2t(v5) = v4 & tb2t(v3) = v4 & get2(int, v0, $sum(v2, % 22.35/3.69 | all_51_3)) = v5 & uni(v5)))) % 22.35/3.69 | % 22.35/3.69 | ALPHA: (16) implies: % 22.35/3.69 | (17) $lesseq(0, all_51_2) % 22.35/3.69 | (18) ? [v0: uni] : ? [v1: int] : ($lesseq(all_51_3, $difference(v1, % 22.35/3.69 | all_51_2)) & $lesseq(all_51_4, $difference(v1, all_51_2)) & % 22.35/3.69 | t2tb1(all_51_5) = v0 & length1(int, v0) = v1 & uni(v0) & ! [v2: % 22.35/3.69 | int] : ! [v3: uni] : ( ~ ($lesseq(1, $difference(all_51_2, v2))) % 22.35/3.69 | | ~ ($lesseq(0, v2)) | ~ (get2(int, v0, $sum(v2, all_51_4)) = % 22.35/3.69 | v3) | ? [v4: int] : ? [v5: uni] : (tb2t(v5) = v4 & tb2t(v3) = % 22.35/3.69 | v4 & get2(int, v0, $sum(v2, all_51_3)) = v5 & uni(v5)))) % 22.35/3.69 | % 22.35/3.69 | GROUND_INST: instantiating (2) with all_51_5, all_51_4, all_51_3, % 22.35/3.69 | $sum(all_51_2, 1), all_51_1, simplifying with (12), (14) gives: % 22.35/3.69 | (19) all_51_1 = 0 | ~ ($lesseq(-1, all_51_2)) | ? [v0: uni] : ? [v1: % 22.35/3.69 | int] : (t2tb1(all_51_5) = v0 & length1(int, v0) = v1 & uni(v0) & ( ~ % 22.35/3.69 | ($lesseq(1, $difference($difference(v1, all_51_2), all_51_3))) | % 22.35/3.69 | ~ ($lesseq(1, $difference($difference(v1, all_51_2), all_51_4))) | % 22.35/3.69 | ? [v2: int] : ? [v3: uni] : ? [v4: int] : ? [v5: uni] : ? % 22.35/3.69 | [v6: int] : ( ~ (v6 = v4) & $lesseq(v2, all_51_2) & $lesseq(0, v2) % 22.35/3.69 | & tb2t(v5) = v6 & tb2t(v3) = v4 & get2(int, v0, $sum(v2, % 22.35/3.69 | all_51_3)) = v5 & get2(int, v0, $sum(v2, all_51_4)) = v3 & % 22.35/3.69 | uni(v5) & uni(v3)))) % 22.35/3.69 | % 22.35/3.69 | GROUND_INST: instantiating (3) with all_51_5, all_51_4, all_51_3, all_51_2, % 22.35/3.69 | all_51_0, simplifying with (12), (15) gives: % 22.35/3.69 | (20) all_51_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 22.35/3.69 | is_common_prefix1(all_51_5, all_51_4, all_51_3, all_51_2) = v0) | ? % 22.35/3.69 | [v0: int] : ($lesseq(1, $difference(v0, all_51_2)) & % 22.35/3.69 | is_common_prefix1(all_51_5, all_51_4, all_51_3, v0) = 0) % 22.35/3.69 | % 22.35/3.69 | DELTA: instantiating (18) with fresh symbols all_74_0, all_74_1 gives: % 22.35/3.69 | (21) $lesseq(all_51_3, $difference(all_74_0, all_51_2)) & $lesseq(all_51_4, % 22.35/3.69 | $difference(all_74_0, all_51_2)) & t2tb1(all_51_5) = all_74_1 & % 22.35/3.69 | length1(int, all_74_1) = all_74_0 & uni(all_74_1) & ! [v0: int] : ! % 22.35/3.69 | [v1: uni] : ( ~ ($lesseq(1, $difference(all_51_2, v0))) | ~ % 22.35/3.69 | ($lesseq(0, v0)) | ~ (get2(int, all_74_1, $sum(v0, all_51_4)) = v1) % 22.35/3.69 | | ? [v2: int] : ? [v3: uni] : (tb2t(v3) = v2 & tb2t(v1) = v2 & % 22.35/3.69 | get2(int, all_74_1, $sum(v0, all_51_3)) = v3 & uni(v3))) % 22.35/3.70 | % 22.35/3.70 | ALPHA: (21) implies: % 22.35/3.70 | (22) length1(int, all_74_1) = all_74_0 % 22.35/3.70 | (23) t2tb1(all_51_5) = all_74_1 % 22.35/3.70 | (24) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_51_2, % 22.35/3.70 | v0))) | ~ ($lesseq(0, v0)) | ~ (get2(int, all_74_1, $sum(v0, % 22.35/3.70 | all_51_4)) = v1) | ? [v2: int] : ? [v3: uni] : (tb2t(v3) = % 22.35/3.70 | v2 & tb2t(v1) = v2 & get2(int, all_74_1, $sum(v0, all_51_3)) = v3 % 22.35/3.70 | & uni(v3))) % 22.35/3.70 | % 22.35/3.70 | BETA: splitting (20) gives: % 22.35/3.70 | % 22.35/3.70 | Case 1: % 22.35/3.70 | | % 22.35/3.70 | | (25) all_51_0 = 0 % 22.35/3.70 | | % 22.35/3.70 | | REDUCE: (11), (25) imply: % 22.35/3.70 | | (26) $false % 22.35/3.70 | | % 22.35/3.70 | | CLOSE: (26) is inconsistent. % 22.35/3.70 | | % 22.35/3.70 | Case 2: % 22.35/3.70 | | % 22.35/3.70 | | (27) ? [v0: int] : ( ~ (v0 = 0) & is_common_prefix1(all_51_5, all_51_4, % 22.35/3.70 | | all_51_3, all_51_2) = v0) | ? [v0: int] : ($lesseq(1, % 22.35/3.70 | | $difference(v0, all_51_2)) & is_common_prefix1(all_51_5, % 22.35/3.70 | | all_51_4, all_51_3, v0) = 0) % 22.35/3.70 | | % 22.35/3.70 | | BETA: splitting (27) gives: % 22.35/3.70 | | % 22.35/3.70 | | Case 1: % 22.35/3.70 | | | % 22.35/3.70 | | | (28) ? [v0: int] : ( ~ (v0 = 0) & is_common_prefix1(all_51_5, % 22.35/3.70 | | | all_51_4, all_51_3, all_51_2) = v0) % 22.35/3.70 | | | % 22.35/3.70 | | | DELTA: instantiating (28) with fresh symbol all_87_0 gives: % 22.35/3.70 | | | (29) ~ (all_87_0 = 0) & is_common_prefix1(all_51_5, all_51_4, % 22.35/3.70 | | | all_51_3, all_51_2) = all_87_0 % 22.35/3.70 | | | % 22.35/3.70 | | | ALPHA: (29) implies: % 22.35/3.70 | | | (30) ~ (all_87_0 = 0) % 22.35/3.70 | | | (31) is_common_prefix1(all_51_5, all_51_4, all_51_3, all_51_2) = % 22.35/3.70 | | | all_87_0 % 22.35/3.70 | | | % 22.35/3.70 | | | GROUND_INST: instantiating (8) with 0, all_87_0, all_51_2, all_51_3, % 22.35/3.70 | | | all_51_4, all_51_5, simplifying with (13), (31) gives: % 22.35/3.70 | | | (32) all_87_0 = 0 % 22.35/3.70 | | | % 22.35/3.70 | | | REDUCE: (30), (32) imply: % 22.35/3.70 | | | (33) $false % 22.35/3.70 | | | % 22.35/3.70 | | | CLOSE: (33) is inconsistent. % 22.35/3.70 | | | % 22.35/3.70 | | Case 2: % 22.35/3.70 | | | % 22.35/3.70 | | | (34) ? [v0: int] : ($lesseq(1, $difference(v0, all_51_2)) & % 22.35/3.70 | | | is_common_prefix1(all_51_5, all_51_4, all_51_3, v0) = 0) % 22.35/3.70 | | | % 22.35/3.70 | | | DELTA: instantiating (34) with fresh symbol all_87_0 gives: % 22.35/3.70 | | | (35) $lesseq(1, $difference(all_87_0, all_51_2)) & % 22.35/3.70 | | | is_common_prefix1(all_51_5, all_51_4, all_51_3, all_87_0) = 0 % 22.35/3.70 | | | % 22.35/3.70 | | | ALPHA: (35) implies: % 22.35/3.70 | | | (36) $lesseq(1, $difference(all_87_0, all_51_2)) % 22.35/3.70 | | | (37) is_common_prefix1(all_51_5, all_51_4, all_51_3, all_87_0) = 0 % 22.35/3.70 | | | % 22.35/3.70 | | | GROUND_INST: instantiating (8) with all_51_1, 0, $sum(all_51_2, 1), % 22.35/3.70 | | | all_51_3, all_51_4, all_51_5, simplifying with (14) gives: % 22.35/3.70 | | | (38) all_51_1 = 0 | ~ (is_common_prefix1(all_51_5, all_51_4, all_51_3, % 22.35/3.70 | | | $sum(all_51_2, 1)) = 0) % 22.35/3.70 | | | % 22.35/3.70 | | | GROUND_INST: instantiating (1) with all_51_5, all_51_4, all_51_3, % 22.35/3.70 | | | all_87_0, simplifying with (12), (37) gives: % 22.35/3.70 | | | (39) $lesseq(0, all_87_0) & ? [v0: uni] : ? [v1: int] : % 22.35/3.70 | | | ($lesseq(all_51_3, $difference(v1, all_87_0)) & $lesseq(all_51_4, % 22.35/3.70 | | | $difference(v1, all_87_0)) & t2tb1(all_51_5) = v0 & % 22.35/3.70 | | | length1(int, v0) = v1 & uni(v0) & ! [v2: int] : ! [v3: uni] : % 22.35/3.70 | | | ( ~ ($lesseq(1, $difference(all_87_0, v2))) | ~ ($lesseq(0, % 22.35/3.70 | | | v2)) | ~ (get2(int, v0, $sum(v2, all_51_4)) = v3) | ? % 22.35/3.70 | | | [v4: int] : ? [v5: uni] : (tb2t(v5) = v4 & tb2t(v3) = v4 & % 22.35/3.70 | | | get2(int, v0, $sum(v2, all_51_3)) = v5 & uni(v5)))) % 22.35/3.70 | | | % 22.35/3.70 | | | ALPHA: (39) implies: % 22.35/3.70 | | | (40) ? [v0: uni] : ? [v1: int] : ($lesseq(all_51_3, $difference(v1, % 22.35/3.71 | | | all_87_0)) & $lesseq(all_51_4, $difference(v1, all_87_0)) & % 22.35/3.71 | | | t2tb1(all_51_5) = v0 & length1(int, v0) = v1 & uni(v0) & ! [v2: % 22.35/3.71 | | | int] : ! [v3: uni] : ( ~ ($lesseq(1, $difference(all_87_0, % 22.35/3.71 | | | v2))) | ~ ($lesseq(0, v2)) | ~ (get2(int, v0, $sum(v2, % 22.35/3.71 | | | all_51_4)) = v3) | ? [v4: int] : ? [v5: uni] : % 22.35/3.71 | | | (tb2t(v5) = v4 & tb2t(v3) = v4 & get2(int, v0, $sum(v2, % 22.35/3.71 | | | all_51_3)) = v5 & uni(v5)))) % 22.35/3.71 | | | % 22.35/3.71 | | | DELTA: instantiating (40) with fresh symbols all_98_0, all_98_1 gives: % 22.35/3.71 | | | (41) $lesseq(all_51_3, $difference(all_98_0, all_87_0)) & % 22.35/3.71 | | | $lesseq(all_51_4, $difference(all_98_0, all_87_0)) & % 22.35/3.71 | | | t2tb1(all_51_5) = all_98_1 & length1(int, all_98_1) = all_98_0 & % 22.35/3.71 | | | uni(all_98_1) & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 22.35/3.71 | | | $difference(all_87_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 22.35/3.71 | | | (get2(int, all_98_1, $sum(v0, all_51_4)) = v1) | ? [v2: int] : % 22.35/3.71 | | | ? [v3: uni] : (tb2t(v3) = v2 & tb2t(v1) = v2 & get2(int, % 22.35/3.71 | | | all_98_1, $sum(v0, all_51_3)) = v3 & uni(v3))) % 22.35/3.71 | | | % 22.35/3.71 | | | ALPHA: (41) implies: % 22.35/3.71 | | | (42) $lesseq(all_51_4, $difference(all_98_0, all_87_0)) % 22.35/3.71 | | | (43) $lesseq(all_51_3, $difference(all_98_0, all_87_0)) % 22.35/3.71 | | | (44) length1(int, all_98_1) = all_98_0 % 22.35/3.71 | | | (45) t2tb1(all_51_5) = all_98_1 % 22.35/3.71 | | | (46) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 22.35/3.71 | | | $difference(all_87_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 22.35/3.71 | | | (get2(int, all_98_1, $sum(v0, all_51_4)) = v1) | ? [v2: int] : % 22.35/3.71 | | | ? [v3: uni] : (tb2t(v3) = v2 & tb2t(v1) = v2 & get2(int, % 22.35/3.71 | | | all_98_1, $sum(v0, all_51_3)) = v3 & uni(v3))) % 22.35/3.71 | | | % 22.35/3.71 | | | GROUND_INST: instantiating (5) with all_74_1, all_98_1, all_51_5, % 22.35/3.71 | | | simplifying with (23), (45) gives: % 22.35/3.71 | | | (47) all_98_1 = all_74_1 % 22.35/3.71 | | | % 22.35/3.71 | | | REDUCE: (44), (47) imply: % 22.35/3.71 | | | (48) length1(int, all_74_1) = all_98_0 % 22.35/3.71 | | | % 22.35/3.71 | | | GROUND_INST: instantiating (6) with all_74_0, all_98_0, all_74_1, int, % 22.35/3.71 | | | simplifying with (22), (48) gives: % 22.35/3.71 | | | (49) all_98_0 = all_74_0 % 22.35/3.71 | | | % 22.35/3.71 | | | REDUCE: (43), (49) imply: % 22.35/3.71 | | | (50) $lesseq(all_51_3, $difference(all_74_0, all_87_0)) % 22.35/3.71 | | | % 22.35/3.71 | | | REDUCE: (42), (49) imply: % 22.35/3.71 | | | (51) $lesseq(all_51_4, $difference(all_74_0, all_87_0)) % 22.35/3.71 | | | % 22.35/3.71 | | | BETA: splitting (19) gives: % 22.35/3.71 | | | % 22.35/3.71 | | | Case 1: % 22.35/3.71 | | | | % 22.35/3.71 | | | | (52) $lesseq(all_51_2, -2) % 22.35/3.71 | | | | % 22.35/3.71 | | | | COMBINE_INEQS: (17), (52) imply: % 22.35/3.71 | | | | (53) $false % 22.35/3.71 | | | | % 22.35/3.71 | | | | CLOSE: (53) is inconsistent. % 22.35/3.71 | | | | % 22.35/3.71 | | | Case 2: % 22.35/3.71 | | | | % 22.35/3.71 | | | | (54) all_51_1 = 0 | ? [v0: uni] : ? [v1: int] : (t2tb1(all_51_5) = % 22.35/3.71 | | | | v0 & length1(int, v0) = v1 & uni(v0) & ( ~ ($lesseq(1, % 22.35/3.71 | | | | $difference($difference(v1, all_51_2), all_51_3))) | ~ % 22.35/3.71 | | | | ($lesseq(1, $difference($difference(v1, all_51_2), % 22.35/3.71 | | | | all_51_4))) | ? [v2: int] : ? [v3: uni] : ? [v4: % 22.35/3.71 | | | | int] : ? [v5: uni] : ? [v6: int] : ( ~ (v6 = v4) & % 22.35/3.71 | | | | $lesseq(v2, all_51_2) & $lesseq(0, v2) & tb2t(v5) = v6 & % 22.35/3.71 | | | | tb2t(v3) = v4 & get2(int, v0, $sum(v2, all_51_3)) = v5 & % 22.35/3.71 | | | | get2(int, v0, $sum(v2, all_51_4)) = v3 & uni(v5) & % 22.35/3.71 | | | | uni(v3)))) % 22.35/3.71 | | | | % 22.35/3.71 | | | | BETA: splitting (54) gives: % 22.35/3.71 | | | | % 22.35/3.71 | | | | Case 1: % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | (55) all_51_1 = 0 % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | REDUCE: (10), (55) imply: % 22.35/3.71 | | | | | (56) $false % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | CLOSE: (56) is inconsistent. % 22.35/3.71 | | | | | % 22.35/3.71 | | | | Case 2: % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | (57) ? [v0: uni] : ? [v1: int] : (t2tb1(all_51_5) = v0 & % 22.35/3.71 | | | | | length1(int, v0) = v1 & uni(v0) & ( ~ ($lesseq(1, % 22.35/3.71 | | | | | $difference($difference(v1, all_51_2), all_51_3))) | % 22.35/3.71 | | | | | ~ ($lesseq(1, $difference($difference(v1, all_51_2), % 22.35/3.71 | | | | | all_51_4))) | ? [v2: int] : ? [v3: uni] : ? [v4: % 22.35/3.71 | | | | | int] : ? [v5: uni] : ? [v6: int] : ( ~ (v6 = v4) & % 22.35/3.71 | | | | | $lesseq(v2, all_51_2) & $lesseq(0, v2) & tb2t(v5) = v6 & % 22.35/3.71 | | | | | tb2t(v3) = v4 & get2(int, v0, $sum(v2, all_51_3)) = v5 & % 22.35/3.71 | | | | | get2(int, v0, $sum(v2, all_51_4)) = v3 & uni(v5) & % 22.35/3.71 | | | | | uni(v3)))) % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | DELTA: instantiating (57) with fresh symbols all_122_0, all_122_1 % 22.35/3.71 | | | | | gives: % 22.35/3.71 | | | | | (58) t2tb1(all_51_5) = all_122_1 & length1(int, all_122_1) = % 22.35/3.71 | | | | | all_122_0 & uni(all_122_1) & ( ~ ($lesseq(1, % 22.35/3.71 | | | | | $difference($difference(all_122_0, all_51_2), % 22.35/3.71 | | | | | all_51_3))) | ~ ($lesseq(1, % 22.35/3.71 | | | | | $difference($difference(all_122_0, all_51_2), % 22.35/3.71 | | | | | all_51_4))) | ? [v0: int] : ? [v1: uni] : ? [v2: % 22.35/3.71 | | | | | int] : ? [v3: uni] : ? [v4: int] : ( ~ (v4 = v2) & % 22.35/3.71 | | | | | $lesseq(v0, all_51_2) & $lesseq(0, v0) & tb2t(v3) = v4 & % 22.35/3.71 | | | | | tb2t(v1) = v2 & get2(int, all_122_1, $sum(v0, all_51_3)) = % 22.35/3.71 | | | | | v3 & get2(int, all_122_1, $sum(v0, all_51_4)) = v1 & % 22.35/3.71 | | | | | uni(v3) & uni(v1))) % 22.35/3.71 | | | | | % 22.35/3.71 | | | | | ALPHA: (58) implies: % 22.35/3.72 | | | | | (59) length1(int, all_122_1) = all_122_0 % 22.35/3.72 | | | | | (60) t2tb1(all_51_5) = all_122_1 % 22.35/3.72 | | | | | (61) ~ ($lesseq(1, $difference($difference(all_122_0, all_51_2), % 22.35/3.72 | | | | | all_51_3))) | ~ ($lesseq(1, % 22.35/3.72 | | | | | $difference($difference(all_122_0, all_51_2), all_51_4))) % 22.35/3.72 | | | | | | ? [v0: int] : ? [v1: uni] : ? [v2: int] : ? [v3: uni] : % 22.35/3.72 | | | | | ? [v4: int] : ( ~ (v4 = v2) & $lesseq(v0, all_51_2) & % 22.35/3.72 | | | | | $lesseq(0, v0) & tb2t(v3) = v4 & tb2t(v1) = v2 & get2(int, % 22.35/3.72 | | | | | all_122_1, $sum(v0, all_51_3)) = v3 & get2(int, all_122_1, % 22.35/3.72 | | | | | $sum(v0, all_51_4)) = v1 & uni(v3) & uni(v1)) % 22.35/3.72 | | | | | % 22.35/3.72 | | | | | GROUND_INST: instantiating (5) with all_74_1, all_122_1, all_51_5, % 22.35/3.72 | | | | | simplifying with (23), (60) gives: % 22.35/3.72 | | | | | (62) all_122_1 = all_74_1 % 22.35/3.72 | | | | | % 22.35/3.72 | | | | | REDUCE: (59), (62) imply: % 22.35/3.72 | | | | | (63) length1(int, all_74_1) = all_122_0 % 22.35/3.72 | | | | | % 22.35/3.72 | | | | | GROUND_INST: instantiating (6) with all_74_0, all_122_0, all_74_1, % 22.35/3.72 | | | | | int, simplifying with (22), (63) gives: % 22.35/3.72 | | | | | (64) all_122_0 = all_74_0 % 22.35/3.72 | | | | | % 22.35/3.72 | | | | | BETA: splitting (61) gives: % 22.35/3.72 | | | | | % 22.35/3.72 | | | | | Case 1: % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | (65) $lesseq(0, $sum($difference(all_51_2, all_122_0), all_51_3)) % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | REDUCE: (64), (65) imply: % 22.35/3.72 | | | | | | (66) $lesseq(0, $sum($difference(all_51_2, all_74_0), all_51_3)) % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | COMBINE_INEQS: (36), (50) imply: % 22.35/3.72 | | | | | | (67) $lesseq(1, $difference($difference(all_74_0, all_51_2), % 22.35/3.72 | | | | | | all_51_3)) % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | COMBINE_INEQS: (66), (67) imply: % 22.35/3.72 | | | | | | (68) $false % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | CLOSE: (68) is inconsistent. % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | Case 2: % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | (69) ~ ($lesseq(1, $difference($difference(all_122_0, all_51_2), % 22.35/3.72 | | | | | | all_51_4))) | ? [v0: int] : ? [v1: uni] : ? [v2: % 22.35/3.72 | | | | | | int] : ? [v3: uni] : ? [v4: int] : ( ~ (v4 = v2) & % 22.35/3.72 | | | | | | $lesseq(v0, all_51_2) & $lesseq(0, v0) & tb2t(v3) = v4 & % 22.35/3.72 | | | | | | tb2t(v1) = v2 & get2(int, all_122_1, $sum(v0, all_51_3)) = % 22.35/3.72 | | | | | | v3 & get2(int, all_122_1, $sum(v0, all_51_4)) = v1 & % 22.35/3.72 | | | | | | uni(v3) & uni(v1)) % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | BETA: splitting (69) gives: % 22.35/3.72 | | | | | | % 22.35/3.72 | | | | | | Case 1: % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | (70) $lesseq(0, $sum($difference(all_51_2, all_122_0), % 22.35/3.72 | | | | | | | all_51_4)) % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | REDUCE: (64), (70) imply: % 22.35/3.72 | | | | | | | (71) $lesseq(0, $sum($difference(all_51_2, all_74_0), % 22.35/3.72 | | | | | | | all_51_4)) % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | COMBINE_INEQS: (36), (51) imply: % 22.35/3.72 | | | | | | | (72) $lesseq(1, $difference($difference(all_74_0, all_51_2), % 22.35/3.72 | | | | | | | all_51_4)) % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | COMBINE_INEQS: (71), (72) imply: % 22.35/3.72 | | | | | | | (73) $false % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | CLOSE: (73) is inconsistent. % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | Case 2: % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | (74) ? [v0: int] : ? [v1: uni] : ? [v2: int] : ? [v3: uni] % 22.35/3.72 | | | | | | | : ? [v4: int] : ( ~ (v4 = v2) & $lesseq(v0, all_51_2) & % 22.35/3.72 | | | | | | | $lesseq(0, v0) & tb2t(v3) = v4 & tb2t(v1) = v2 & % 22.35/3.72 | | | | | | | get2(int, all_122_1, $sum(v0, all_51_3)) = v3 & % 22.35/3.72 | | | | | | | get2(int, all_122_1, $sum(v0, all_51_4)) = v1 & uni(v3) % 22.35/3.72 | | | | | | | & uni(v1)) % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | DELTA: instantiating (74) with fresh symbols all_145_0, all_145_1, % 22.35/3.72 | | | | | | | all_145_2, all_145_3, all_145_4 gives: % 22.35/3.72 | | | | | | | (75) ~ (all_145_0 = all_145_2) & $lesseq(all_145_4, all_51_2) % 22.35/3.72 | | | | | | | & $lesseq(0, all_145_4) & tb2t(all_145_1) = all_145_0 & % 22.35/3.72 | | | | | | | tb2t(all_145_3) = all_145_2 & get2(int, all_122_1, % 22.35/3.72 | | | | | | | $sum(all_145_4, all_51_3)) = all_145_1 & get2(int, % 22.35/3.72 | | | | | | | all_122_1, $sum(all_145_4, all_51_4)) = all_145_3 & % 22.35/3.72 | | | | | | | uni(all_145_1) & uni(all_145_3) % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | ALPHA: (75) implies: % 22.35/3.72 | | | | | | | (76) ~ (all_145_0 = all_145_2) % 22.35/3.72 | | | | | | | (77) $lesseq(0, all_145_4) % 22.35/3.72 | | | | | | | (78) $lesseq(all_145_4, all_51_2) % 22.35/3.72 | | | | | | | (79) get2(int, all_122_1, $sum(all_145_4, all_51_4)) = % 22.35/3.72 | | | | | | | all_145_3 % 22.35/3.72 | | | | | | | (80) get2(int, all_122_1, $sum(all_145_4, all_51_3)) = % 22.35/3.72 | | | | | | | all_145_1 % 22.35/3.72 | | | | | | | (81) tb2t(all_145_3) = all_145_2 % 22.35/3.72 | | | | | | | (82) tb2t(all_145_1) = all_145_0 % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | REDUCE: (62), (80) imply: % 22.35/3.72 | | | | | | | (83) get2(int, all_74_1, $sum(all_145_4, all_51_3)) = all_145_1 % 22.35/3.72 | | | | | | | % 22.35/3.72 | | | | | | | REDUCE: (62), (79) imply: % 22.35/3.72 | | | | | | | (84) get2(int, all_74_1, $sum(all_145_4, all_51_4)) = all_145_3 % 22.35/3.72 | | | | | | | % 22.35/3.73 | | | | | | | GROUND_INST: instantiating (24) with all_145_4, all_145_3, % 22.35/3.73 | | | | | | | simplifying with (84) gives: % 22.35/3.73 | | | | | | | (85) ~ ($lesseq(1, $difference(all_51_2, all_145_4))) | ~ % 22.35/3.73 | | | | | | | ($lesseq(0, all_145_4)) | ? [v0: int] : ? [v1: uni] : % 22.35/3.73 | | | | | | | (tb2t(v1) = v0 & tb2t(all_145_3) = v0 & get2(int, % 22.35/3.73 | | | | | | | all_74_1, $sum(all_145_4, all_51_3)) = v1 & uni(v1)) % 22.35/3.73 | | | | | | | % 22.35/3.73 | | | | | | | BETA: splitting (85) gives: % 22.35/3.73 | | | | | | | % 22.35/3.73 | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | (86) $lesseq(all_145_4, -1) % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | COMBINE_INEQS: (77), (86) imply: % 22.35/3.73 | | | | | | | | (87) $false % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | CLOSE: (87) is inconsistent. % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | Case 2: % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | (88) ~ ($lesseq(1, $difference(all_51_2, all_145_4))) | ? % 22.35/3.73 | | | | | | | | [v0: int] : ? [v1: uni] : (tb2t(v1) = v0 & % 22.35/3.73 | | | | | | | | tb2t(all_145_3) = v0 & get2(int, all_74_1, % 22.35/3.73 | | | | | | | | $sum(all_145_4, all_51_3)) = v1 & uni(v1)) % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | BETA: splitting (88) gives: % 22.35/3.73 | | | | | | | | % 22.35/3.73 | | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | (89) $lesseq(all_51_2, all_145_4) % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | ANTI_SYMM: (78), (89) imply: % 22.35/3.73 | | | | | | | | | (90) all_145_4 = all_51_2 % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | REDUCE: (83), (90) imply: % 22.35/3.73 | | | | | | | | | (91) get2(int, all_74_1, $sum(all_51_2, all_51_3)) = % 22.35/3.73 | | | | | | | | | all_145_1 % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | REDUCE: (84), (90) imply: % 22.35/3.73 | | | | | | | | | (92) get2(int, all_74_1, $sum(all_51_2, all_51_4)) = % 22.35/3.73 | | | | | | | | | all_145_3 % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | BETA: splitting (38) gives: % 22.35/3.73 | | | | | | | | | % 22.35/3.73 | | | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | (93) ~ (is_common_prefix1(all_51_5, all_51_4, all_51_3, % 22.35/3.73 | | | | | | | | | | $sum(all_51_2, 1)) = 0) % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | PRED_UNIFY: (37), (93) imply: % 22.35/3.73 | | | | | | | | | | (94) ~ ($difference(all_87_0, all_51_2) = 1) % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | STRENGTHEN: (36), (94) imply: % 22.35/3.73 | | | | | | | | | | (95) $lesseq(2, $difference(all_87_0, all_51_2)) % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | GROUND_INST: instantiating (46) with all_51_2, all_145_3 gives: % 22.35/3.73 | | | | | | | | | | (96) ~ ($lesseq(1, $difference(all_87_0, all_51_2))) | % 22.35/3.73 | | | | | | | | | | ~ ($lesseq(0, all_51_2)) | ~ (get2(int, all_98_1, % 22.35/3.73 | | | | | | | | | | $sum(all_51_2, all_51_4)) = all_145_3) | ? [v0: % 22.35/3.73 | | | | | | | | | | int] : ? [v1: uni] : (tb2t(v1) = v0 & % 22.35/3.73 | | | | | | | | | | tb2t(all_145_3) = v0 & get2(int, all_98_1, % 22.35/3.73 | | | | | | | | | | $sum(all_51_2, all_51_3)) = v1 & uni(v1)) % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | BETA: splitting (96) gives: % 22.35/3.73 | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | (97) ~ (get2(int, all_98_1, $sum(all_51_2, all_51_4)) % 22.35/3.73 | | | | | | | | | | | = all_145_3) % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | REDUCE: (47), (97) imply: % 22.35/3.73 | | | | | | | | | | | (98) ~ (get2(int, all_74_1, $sum(all_51_2, all_51_4)) % 22.35/3.73 | | | | | | | | | | | = all_145_3) % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | PRED_UNIFY: (92), (98) imply: % 22.35/3.73 | | | | | | | | | | | (99) $false % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | CLOSE: (99) is inconsistent. % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | Case 2: % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | (100) ~ ($lesseq(1, $difference(all_87_0, all_51_2))) | % 22.35/3.73 | | | | | | | | | | | ~ ($lesseq(0, all_51_2)) | ? [v0: int] : ? [v1: % 22.35/3.73 | | | | | | | | | | | uni] : (tb2t(v1) = v0 & tb2t(all_145_3) = v0 & % 22.35/3.73 | | | | | | | | | | | get2(int, all_98_1, $sum(all_51_2, all_51_3)) = % 22.35/3.73 | | | | | | | | | | | v1 & uni(v1)) % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | BETA: splitting (100) gives: % 22.35/3.73 | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | (101) $lesseq(all_51_2, -1) % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | COMBINE_INEQS: (17), (101) imply: % 22.35/3.73 | | | | | | | | | | | | (102) $false % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | CLOSE: (102) is inconsistent. % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | Case 2: % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | (103) ~ ($lesseq(1, $difference(all_87_0, all_51_2))) | % 22.35/3.73 | | | | | | | | | | | | ? [v0: int] : ? [v1: uni] : (tb2t(v1) = v0 & % 22.35/3.73 | | | | | | | | | | | | tb2t(all_145_3) = v0 & get2(int, all_98_1, % 22.35/3.73 | | | | | | | | | | | | $sum(all_51_2, all_51_3)) = v1 & uni(v1)) % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | BETA: splitting (103) gives: % 22.35/3.73 | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | Case 1: % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | (104) $lesseq(all_87_0, all_51_2) % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | COMBINE_INEQS: (95), (104) imply: % 22.35/3.73 | | | | | | | | | | | | | (105) $false % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | CLOSE: (105) is inconsistent. % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | Case 2: % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | (106) ? [v0: int] : ? [v1: uni] : (tb2t(v1) = v0 & % 22.35/3.73 | | | | | | | | | | | | | tb2t(all_145_3) = v0 & get2(int, all_98_1, % 22.35/3.73 | | | | | | | | | | | | | $sum(all_51_2, all_51_3)) = v1 & uni(v1)) % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | DELTA: instantiating (106) with fresh symbols all_505_0, % 22.35/3.73 | | | | | | | | | | | | | all_505_1 gives: % 22.35/3.73 | | | | | | | | | | | | | (107) tb2t(all_505_0) = all_505_1 & tb2t(all_145_3) = % 22.35/3.73 | | | | | | | | | | | | | all_505_1 & get2(int, all_98_1, $sum(all_51_2, % 22.35/3.73 | | | | | | | | | | | | | all_51_3)) = all_505_0 & uni(all_505_0) % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | ALPHA: (107) implies: % 22.35/3.73 | | | | | | | | | | | | | (108) get2(int, all_98_1, $sum(all_51_2, all_51_3)) = % 22.35/3.73 | | | | | | | | | | | | | all_505_0 % 22.35/3.73 | | | | | | | | | | | | | (109) tb2t(all_145_3) = all_505_1 % 22.35/3.73 | | | | | | | | | | | | | (110) tb2t(all_505_0) = all_505_1 % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | REDUCE: (47), (108) imply: % 22.35/3.73 | | | | | | | | | | | | | (111) get2(int, all_74_1, $sum(all_51_2, all_51_3)) = % 22.35/3.73 | | | | | | | | | | | | | all_505_0 % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | GROUND_INST: instantiating (7) with all_145_1, all_505_0, % 22.35/3.73 | | | | | | | | | | | | | $sum(all_51_2, all_51_3), all_74_1, int, % 22.35/3.73 | | | | | | | | | | | | | simplifying with (91), (111) gives: % 22.35/3.73 | | | | | | | | | | | | | (112) all_505_0 = all_145_1 % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_145_2, all_505_1, % 22.35/3.73 | | | | | | | | | | | | | all_145_3, simplifying with (81), (109) gives: % 22.35/3.73 | | | | | | | | | | | | | (113) all_505_1 = all_145_2 % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | REDUCE: (110), (112), (113) imply: % 22.35/3.73 | | | | | | | | | | | | | (114) tb2t(all_145_1) = all_145_2 % 22.35/3.73 | | | | | | | | | | | | | % 22.35/3.73 | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_145_0, all_145_2, % 22.35/3.73 | | | | | | | | | | | | | all_145_1, simplifying with (82), (114) gives: % 22.35/3.74 | | | | | | | | | | | | | (115) all_145_0 = all_145_2 % 22.35/3.74 | | | | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | | | | REDUCE: (76), (115) imply: % 22.35/3.74 | | | | | | | | | | | | | (116) $false % 22.35/3.74 | | | | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | | | | CLOSE: (116) is inconsistent. % 22.35/3.74 | | | | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | | | End of split % 22.35/3.74 | | | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | | End of split % 22.35/3.74 | | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | End of split % 22.35/3.74 | | | | | | | | | | % 22.35/3.74 | | | | | | | | | Case 2: % 22.35/3.74 | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | (117) all_51_1 = 0 % 22.35/3.74 | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | REDUCE: (10), (117) imply: % 22.35/3.74 | | | | | | | | | | (118) $false % 22.35/3.74 | | | | | | | | | | % 22.35/3.74 | | | | | | | | | | CLOSE: (118) is inconsistent. % 22.35/3.74 | | | | | | | | | | % 22.35/3.74 | | | | | | | | | End of split % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | Case 2: % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | (119) ? [v0: int] : ? [v1: uni] : (tb2t(v1) = v0 & % 22.35/3.74 | | | | | | | | | tb2t(all_145_3) = v0 & get2(int, all_74_1, % 22.35/3.74 | | | | | | | | | $sum(all_145_4, all_51_3)) = v1 & uni(v1)) % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | DELTA: instantiating (119) with fresh symbols all_166_0, % 22.35/3.74 | | | | | | | | | all_166_1 gives: % 22.35/3.74 | | | | | | | | | (120) tb2t(all_166_0) = all_166_1 & tb2t(all_145_3) = % 22.35/3.74 | | | | | | | | | all_166_1 & get2(int, all_74_1, $sum(all_145_4, % 22.35/3.74 | | | | | | | | | all_51_3)) = all_166_0 & uni(all_166_0) % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | ALPHA: (120) implies: % 22.35/3.74 | | | | | | | | | (121) get2(int, all_74_1, $sum(all_145_4, all_51_3)) = % 22.35/3.74 | | | | | | | | | all_166_0 % 22.35/3.74 | | | | | | | | | (122) tb2t(all_145_3) = all_166_1 % 22.35/3.74 | | | | | | | | | (123) tb2t(all_166_0) = all_166_1 % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | GROUND_INST: instantiating (7) with all_145_1, all_166_0, % 22.35/3.74 | | | | | | | | | $sum(all_145_4, all_51_3), all_74_1, int, % 22.35/3.74 | | | | | | | | | simplifying with (83), (121) gives: % 22.35/3.74 | | | | | | | | | (124) all_166_0 = all_145_1 % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | GROUND_INST: instantiating (4) with all_145_2, all_166_1, % 22.35/3.74 | | | | | | | | | all_145_3, simplifying with (81), (122) gives: % 22.35/3.74 | | | | | | | | | (125) all_166_1 = all_145_2 % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | REDUCE: (123), (124), (125) imply: % 22.35/3.74 | | | | | | | | | (126) tb2t(all_145_1) = all_145_2 % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | GROUND_INST: instantiating (4) with all_145_0, all_145_2, % 22.35/3.74 | | | | | | | | | all_145_1, simplifying with (82), (126) gives: % 22.35/3.74 | | | | | | | | | (127) all_145_0 = all_145_2 % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | REDUCE: (76), (127) imply: % 22.35/3.74 | | | | | | | | | (128) $false % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | | CLOSE: (128) is inconsistent. % 22.35/3.74 | | | | | | | | | % 22.35/3.74 | | | | | | | | End of split % 22.35/3.74 | | | | | | | | % 22.35/3.74 | | | | | | | End of split % 22.35/3.74 | | | | | | | % 22.35/3.74 | | | | | | End of split % 22.35/3.74 | | | | | | % 22.35/3.74 | | | | | End of split % 22.35/3.74 | | | | | % 22.35/3.74 | | | | End of split % 22.35/3.74 | | | | % 22.35/3.74 | | | End of split % 22.35/3.74 | | | % 22.35/3.74 | | End of split % 22.35/3.74 | | % 22.35/3.74 | End of split % 22.35/3.74 | % 22.35/3.74 End of proof % 22.35/3.74 % SZS output end Proof for theBenchmark % 22.35/3.74 % 22.35/3.74 3134ms %------------------------------------------------------------------------------