%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW634_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 : n004.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:58 EDT 2023 % Result : Theorem 35.79s 5.61s % Output : Proof 37.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW634_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n004.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 19:15:22 EDT 2023 % 0.13/0.33 % 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.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 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 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 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 % 4.46/1.39 Prover 2: Preprocessing ... % 4.46/1.39 Prover 4: Preprocessing ... % 4.46/1.40 Prover 0: Preprocessing ... % 4.46/1.40 Prover 1: Preprocessing ... % 4.46/1.41 Prover 3: Preprocessing ... % 4.97/1.41 Prover 6: Preprocessing ... % 4.97/1.42 Prover 5: Preprocessing ... % 12.98/2.49 Prover 1: Warning: ignoring some quantifiers % 12.98/2.53 Prover 3: Warning: ignoring some quantifiers % 13.65/2.59 Prover 4: Warning: ignoring some quantifiers % 13.65/2.61 Prover 3: Constructing countermodel ... % 13.65/2.64 Prover 5: Proving ... % 13.65/2.66 Prover 6: Proving ... % 13.65/2.66 Prover 1: Constructing countermodel ... % 14.76/2.74 Prover 0: Proving ... % 14.76/2.75 Prover 4: Constructing countermodel ... % 15.94/2.93 Prover 2: Proving ... % 21.22/3.65 Prover 3: gave up % 21.82/3.67 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 22.28/3.81 Prover 7: Preprocessing ... % 24.96/4.11 Prover 7: Warning: ignoring some quantifiers % 25.04/4.16 Prover 7: Constructing countermodel ... % 28.58/4.61 Prover 1: gave up % 28.58/4.64 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.21/4.75 Prover 8: Preprocessing ... % 31.54/5.03 Prover 8: Warning: ignoring some quantifiers % 32.23/5.07 Prover 8: Constructing countermodel ... % 35.79/5.60 Prover 4: Found proof (size 194) % 35.79/5.60 Prover 4: proved (4970ms) % 35.79/5.60 Prover 6: stopped % 35.79/5.60 Prover 7: stopped % 35.79/5.60 Prover 8: stopped % 35.79/5.60 Prover 2: stopped % 35.79/5.61 Prover 5: stopped % 35.79/5.61 Prover 0: stopped % 35.79/5.61 % 35.79/5.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.79/5.61 % 36.39/5.64 % SZS output start Proof for theBenchmark % 36.39/5.64 Assumptions after simplification: % 36.39/5.64 --------------------------------- % 36.39/5.64 % 36.39/5.64 (below_def) % 36.39/5.66 ty(int) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: set_int] : ! % 36.39/5.66 [v4: uni] : ! [v5: int] : (v5 = 0 | ~ ($lesseq(1, $difference(v1, v0))) | ~ % 36.39/5.66 ($lesseq(0, v0)) | ~ (below1(v1) = v3) | ~ (t2tb1(v0) = v2) | ~ (t2tb(v3) % 36.39/5.66 = v4) | ~ (mem(int, v2, v4) = v5)) & ! [v0: int] : ! [v1: int] : ! % 36.39/5.66 [v2: uni] : ! [v3: set_int] : ! [v4: uni] : ( ~ ($lesseq(v1, v0)) | ~ % 36.39/5.66 (below1(v1) = v3) | ~ (t2tb1(v0) = v2) | ~ (t2tb(v3) = v4) | ~ (mem(int, % 36.39/5.66 v2, v4) = 0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: % 36.39/5.66 set_int] : ! [v4: uni] : ( ~ ($lesseq(v0, -1)) | ~ (below1(v1) = v3) | ~ % 36.39/5.66 (t2tb1(v0) = v2) | ~ (t2tb(v3) = v4) | ~ (mem(int, v2, v4) = 0)) % 36.39/5.66 % 36.39/5.66 (cardinal_empty) % 36.39/5.66 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (cardinal1(v0, v1) = % 36.39/5.66 v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: int] : ( ~ (v3 = 0) & is_empty(v0, % 36.39/5.66 v1) = v3)) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ % 36.39/5.66 (is_empty(v0, v1) = v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: int] : ( ~ (v3 = % 36.39/5.66 0) & cardinal1(v0, v1) = v3)) & ! [v0: ty] : ! [v1: uni] : ( ~ % 36.39/5.66 (cardinal1(v0, v1) = 0) | ~ ty(v0) | ~ uni(v1) | is_empty(v0, v1) = 0) & % 36.39/5.66 ! [v0: ty] : ! [v1: uni] : ( ~ (is_empty(v0, v1) = 0) | ~ ty(v0) | ~ % 36.39/5.66 uni(v1) | cardinal1(v0, v1) = 0) % 36.39/5.66 % 36.39/5.66 (eq_prefix_def) % 36.39/5.67 ty(int) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: % 36.39/5.67 int] : ! [v5: uni] : ( ~ ($lesseq(1, $difference(v3, v4))) | ~ ($lesseq(0, % 36.39/5.67 v4)) | ~ (eq_prefix1(v0, v1, v2, v3) = 0) | ~ (t2tb1(v4) = v5) | ~ % 36.39/5.67 ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v6: uni] : (get(v0, int, v2, v5) = v6 % 36.39/5.67 & get(v0, int, v1, v5) = v6 & uni(v6))) & ! [v0: ty] : ! [v1: uni] : ! % 36.39/5.67 [v2: uni] : ! [v3: int] : ! [v4: int] : (v4 = 0 | ~ (eq_prefix1(v0, v1, v2, % 36.39/5.67 v3) = v4) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v5: int] : ? [v6: % 36.39/5.67 uni] : ? [v7: uni] : ? [v8: uni] : ( ~ (v8 = v7) & $lesseq(1, % 36.39/5.67 $difference(v3, v5)) & $lesseq(0, v5) & get(v0, int, v2, v6) = v8 & % 36.39/5.67 get(v0, int, v1, v6) = v7 & t2tb1(v5) = v6 & uni(v8) & uni(v7) & uni(v6))) % 36.39/5.67 % 36.39/5.67 (max_elt_def1) % 36.39/5.67 ty(int) & ! [v0: set_int] : ! [v1: int] : ( ~ (max_elt1(v0) = v1) | ~ % 36.39/5.67 set_int(v0) | ? [v2: uni] : ? [v3: any] : ? [v4: uni] : ? [v5: any] : % 36.39/5.67 (t2tb1(v1) = v4 & t2tb(v0) = v2 & is_empty(int, v2) = v3 & mem(int, v4, v2) % 36.39/5.67 = v5 & uni(v4) & uni(v2) & (v5 = 0 | v3 = 0))) & ! [v0: set_int] : ! % 36.39/5.67 [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) | ? [v2: any] : ? [v3: int] % 36.39/5.67 : ? [v4: uni] : ? [v5: any] : (max_elt1(v0) = v3 & t2tb1(v3) = v4 & % 36.39/5.67 is_empty(int, v1) = v2 & mem(int, v4, v1) = v5 & uni(v4) & (v5 = 0 | v2 = % 36.39/5.67 0))) % 36.39/5.67 % 36.39/5.67 (max_elt_def2) % 36.39/5.67 ty(int) & ! [v0: set_int] : ! [v1: int] : ( ~ (max_elt1(v0) = v1) | ~ % 36.39/5.67 set_int(v0) | ? [v2: uni] : ? [v3: any] : (t2tb(v0) = v2 & is_empty(int, % 36.39/5.67 v2) = v3 & uni(v2) & (v3 = 0 | ! [v4: int] : ! [v5: uni] : ( ~ % 36.39/5.67 ($lesseq(1, $difference(v4, v1))) | ~ (t2tb1(v4) = v5) | ? [v6: int] % 36.39/5.67 : ( ~ (v6 = 0) & mem(int, v5, v2) = v6))))) & ! [v0: set_int] : ! % 36.39/5.67 [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) | ? [v2: any] : ? [v3: int] % 36.39/5.67 : (max_elt1(v0) = v3 & is_empty(int, v1) = v2 & (v2 = 0 | ! [v4: int] : ! % 36.39/5.67 [v5: uni] : ( ~ ($lesseq(1, $difference(v4, v3))) | ~ (t2tb1(v4) = v5) % 36.39/5.67 | ? [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v1) = v6))))) % 36.39/5.67 % 36.39/5.67 (min_elt_def1) % 36.39/5.68 ty(int) & ! [v0: set_int] : ! [v1: int] : ( ~ (min_elt1(v0) = v1) | ~ % 36.39/5.68 set_int(v0) | ? [v2: uni] : ? [v3: any] : ? [v4: uni] : ? [v5: any] : % 36.39/5.68 (t2tb1(v1) = v4 & t2tb(v0) = v2 & is_empty(int, v2) = v3 & mem(int, v4, v2) % 36.39/5.68 = v5 & uni(v4) & uni(v2) & (v5 = 0 | v3 = 0))) & ! [v0: set_int] : ! % 36.39/5.68 [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) | ? [v2: any] : ? [v3: int] % 36.39/5.68 : ? [v4: uni] : ? [v5: any] : (min_elt1(v0) = v3 & t2tb1(v3) = v4 & % 36.39/5.68 is_empty(int, v1) = v2 & mem(int, v4, v1) = v5 & uni(v4) & (v5 = 0 | v2 = % 36.39/5.68 0))) % 36.39/5.68 % 36.39/5.68 (min_elt_def2) % 36.69/5.68 ty(int) & ! [v0: set_int] : ! [v1: int] : ( ~ (min_elt1(v0) = v1) | ~ % 36.69/5.68 set_int(v0) | ? [v2: uni] : ? [v3: any] : (t2tb(v0) = v2 & is_empty(int, % 36.69/5.68 v2) = v3 & uni(v2) & (v3 = 0 | ! [v4: int] : ! [v5: uni] : ( ~ % 36.69/5.68 ($lesseq(1, $difference(v1, v4))) | ~ (t2tb1(v4) = v5) | ? [v6: int] % 36.69/5.68 : ( ~ (v6 = 0) & mem(int, v5, v2) = v6))))) & ! [v0: set_int] : ! % 36.69/5.68 [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) | ? [v2: any] : ? [v3: int] % 36.69/5.68 : (min_elt1(v0) = v3 & is_empty(int, v1) = v2 & (v2 = 0 | ! [v4: int] : ! % 36.69/5.68 [v5: uni] : ( ~ ($lesseq(1, $difference(v3, v4))) | ~ (t2tb1(v4) = v5) % 36.69/5.68 | ? [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v1) = v6))))) % 36.69/5.68 % 36.69/5.68 (partial_solution_def) % 36.69/5.68 ty(int) & ! [v0: int] : ! [v1: map_int_int] : ! [v2: int] : (v2 = 0 | ~ % 36.69/5.68 (partial_solution1(v0, v1) = v2) | ~ map_int_int(v1) | ? [v3: uni] : ? % 36.69/5.68 [v4: int] : ? [v5: uni] : ? [v6: uni] : ? [v7: int] : ? [v8: int] : ? % 36.69/5.68 [v9: uni] : ? [v10: uni] : ? [v11: int] : ($lesseq(1, $difference(v0, v4)) % 36.69/5.68 & $lesseq(0, v4) & t2tb2(v1) = v3 & get(int, int, v3, v5) = v6 & tb2t1(v6) % 36.69/5.68 = v7 & t2tb1(v4) = v5 & uni(v6) & uni(v5) & uni(v3) & ( ~ ($lesseq(1, % 36.69/5.68 $difference(n1, v7))) | ~ ($lesseq(0, v7)) | ($lesseq(1, % 36.69/5.68 $difference(v4, v8)) & $lesseq(0, v8) & get(int, int, v3, v9) = v10 % 36.69/5.68 & tb2t1(v10) = v11 & t2tb1(v8) = v9 & uni(v10) & uni(v9) & % 36.69/5.68 ($sum($difference($difference(v11, v8), v7), v4) = 0 | % 36.69/5.68 $difference($sum(v11, v8), v7) = v4 | v11 = v7))))) & ! [v0: int] : % 36.69/5.68 ! [v1: map_int_int] : ( ~ (partial_solution1(v0, v1) = 0) | ~ % 36.69/5.68 map_int_int(v1) | ? [v2: uni] : (t2tb2(v1) = v2 & uni(v2) & ! [v3: int] : % 36.69/5.68 ! [v4: uni] : ( ~ ($lesseq(1, $difference(v0, v3))) | ~ ($lesseq(0, v3)) % 36.69/5.68 | ~ (t2tb1(v3) = v4) | ? [v5: uni] : ? [v6: int] : ($lesseq(1, % 36.69/5.68 $difference(n1, v6)) & $lesseq(0, v6) & get(int, int, v2, v4) = v5 & % 36.69/5.68 tb2t1(v5) = v6 & uni(v5) & ! [v7: int] : ! [v8: uni] : ( ~ % 36.69/5.68 ($lesseq(1, $difference(v3, v7))) | ~ ($lesseq(0, v7)) | ~ % 36.69/5.68 (t2tb1(v7) = v8) | ? [v9: uni] : ? [v10: int] : ( ~ % 36.69/5.68 ($sum($difference($difference(v10, v7), v6), v3) = 0) & ~ % 36.69/5.68 ($difference($sum(v10, v7), v6) = v3) & ~ (v10 = v6) & get(int, % 36.69/5.68 int, v2, v8) = v9 & tb2t1(v9) = v10 & uni(v9))))))) % 36.69/5.68 % 36.69/5.68 (t2tb_sort2) % 36.69/5.68 ty(int) & ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : % 36.69/5.68 ! [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort1(v0, v2) = % 36.69/5.68 0)) % 36.69/5.68 % 36.69/5.68 (wP_parameter_queens3) % 36.69/5.69 ty(int) & ? [v0: uni] : ? [v1: ty] : ? [v2: map_int_lpmap_int_intrp] : ? % 36.69/5.69 [v3: map_int_int] : ? [v4: set_int] : ? [v5: uni] : ? [v6: uni] : ? [v7: % 36.69/5.69 uni] : ? [v8: int] : ? [v9: map_int_lpmap_int_intrp] : ? [v10: % 36.69/5.69 map_int_int] : ? [v11: uni] : ? [v12: uni] : ? [v13: map_int_int] : ? % 36.69/5.69 [v14: any] : ? [v15: uni] : ? [v16: int] : ? [v17: uni] : ? [v18: uni] : % 36.69/5.69 ? [v19: int] : ($lesseq(0, v8) & $lesseq(0, n1) & sorted1(v9, 0, v8) = 0 & % 36.69/5.69 t2tb3(v9) = v12 & t2tb3(v2) = v7 & partial_solution1(n1, v13) = v14 & % 36.69/5.69 partial_solution1(0, v3) = 0 & t2tb2(v13) = v15 & t2tb2(v10) = v11 & % 36.69/5.69 t2tb2(v3) = v6 & eq_prefix1(v1, v7, v12, 0) = 0 & eq_prefix1(int, v6, v11, % 36.69/5.69 0) = 0 & map(int, int) = v1 & below1(n1) = v4 & t2tb(v4) = v5 & % 36.69/5.69 cardinal1(int, v5) = n1 & empty(int) = v0 & map_int_lpmap_int_intrp(v9) & % 36.69/5.69 map_int_lpmap_int_intrp(v2) & map_int_int(v13) & map_int_int(v10) & % 36.69/5.69 map_int_int(v3) & set_int(v4) & ty(v1) & uni(v15) & uni(v12) & uni(v11) & % 36.69/5.69 uni(v7) & uni(v6) & uni(v5) & uni(v0) & ! [v20: map_int_int] : ! [v21: % 36.69/5.69 uni] : ! [v22: int] : ! [v23: uni] : ( ~ ($lesseq(1, $difference(v8, % 36.69/5.69 v22))) | ~ ($lesseq(0, v22)) | ~ (t2tb2(v20) = v21) | ~ % 36.69/5.69 (t2tb1(v22) = v23) | ~ map_int_int(v20) | ? [v24: any] : ? [v25: int] : % 36.69/5.69 ((v25 = 0 & v24 = 0 & partial_solution1(n1, v20) = 0 & eq_prefix1(int, % 36.69/5.69 v11, v21, 0) = 0) | ( ~ (v25 = 0) & eq_prefix1(int, v21, v24, n1) = % 36.69/5.69 v25 & get(v1, int, v12, v23) = v24 & uni(v24)))) & ! [v20: int] : ! % 36.69/5.69 [v21: uni] : ( ~ ($lesseq(1, $difference(n1, v20))) | ~ ($lesseq(0, v20)) | % 36.69/5.69 ~ (t2tb1(v20) = v21) | mem(int, v21, v5) = 0) & ! [v20: int] : ! [v21: % 36.69/5.69 uni] : ( ~ ($lesseq(v20, -1)) | ~ (t2tb1(v20) = v21) | ? [v22: int] : ( % 36.69/5.69 ~ (v22 = 0) & mem(int, v21, v5) = v22)) & ! [v20: int] : ! [v21: uni] % 36.69/5.69 : ( ~ ($lesseq(n1, v20)) | ~ (t2tb1(v20) = v21) | ? [v22: int] : ( ~ (v22 % 36.69/5.69 = 0) & mem(int, v21, v5) = v22)) & ! [v20: int] : ! [v21: uni] : ( ~ % 36.69/5.69 ($lesseq(0, v20)) | ~ (t2tb1(v20) = v21) | ? [v22: int] : ( ~ (v22 = 0) % 36.69/5.69 & mem(int, v21, v0) = v22)) & ! [v20: map_int_int] : ! [v21: any] : ( % 36.69/5.69 ~ (partial_solution1(n1, v20) = v21) | ~ map_int_int(v20) | ? [v22: uni] % 36.69/5.69 : ? [v23: any] : (t2tb2(v20) = v22 & eq_prefix1(int, v11, v22, 0) = v23 & % 36.69/5.69 uni(v22) & ( ! [v24: int] : ! [v25: uni] : ( ~ ($lesseq(1, % 36.69/5.69 $difference(v8, v24))) | ~ ($lesseq(0, v24)) | ~ (t2tb1(v24) = % 36.69/5.69 v25) | ? [v26: uni] : ? [v27: int] : ( ~ (v27 = 0) & % 36.69/5.69 eq_prefix1(int, v22, v26, n1) = v27 & get(v1, int, v12, v25) = v26 % 36.69/5.69 & uni(v26))) | (v23 = 0 & v21 = 0)))) & ! [v20: map_int_int] : ! % 36.69/5.69 [v21: uni] : ( ~ (t2tb2(v20) = v21) | ~ map_int_int(v20) | ? [v22: int] : % 36.69/5.69 ? [v23: any] : ? [v24: uni] : ? [v25: int] : ((v25 = 0 & $lesseq(1, % 36.69/5.69 $difference(v8, v22)) & $lesseq(0, v22) & eq_prefix1(int, v21, v24, % 36.69/5.69 n1) = 0 & get(v1, int, v12, v23) = v24 & t2tb1(v22) = v23 & uni(v24) % 36.69/5.69 & uni(v23)) | (partial_solution1(n1, v20) = v22 & eq_prefix1(int, v11, % 36.69/5.69 v21, 0) = v23 & ( ~ (v23 = 0) | ~ (v22 = 0))))) & ! [v20: % 36.69/5.69 map_int_int] : ( ~ (partial_solution1(n1, v20) = 0) | ~ map_int_int(v20) % 36.69/5.69 | ? [v21: uni] : ? [v22: any] : ? [v23: int] : ? [v24: uni] : ? [v25: % 36.69/5.69 uni] : ? [v26: int] : (t2tb2(v20) = v21 & eq_prefix1(int, v11, v21, 0) % 36.69/5.69 = v22 & uni(v21) & ( ~ (v22 = 0) | (v26 = 0 & $lesseq(1, $difference(v8, % 36.69/5.69 v23)) & $lesseq(0, v23) & eq_prefix1(int, v21, v25, n1) = 0 & % 36.69/5.69 get(v1, int, v12, v24) = v25 & t2tb1(v23) = v24 & uni(v25) & % 36.69/5.69 uni(v24))))) & ((v19 = 0 & ~ (v14 = 0) & $lesseq(1, $difference(v8, % 36.69/5.69 v16)) & $lesseq(0, v16) & eq_prefix1(int, v15, v18, n1) = 0 & % 36.69/5.69 get(v1, int, v12, v17) = v18 & t2tb1(v16) = v17 & uni(v18) & uni(v17)) | % 36.69/5.69 (v14 = 0 & ! [v20: int] : ! [v21: uni] : ( ~ ($lesseq(1, $difference(v8, % 36.69/5.69 v20))) | ~ ($lesseq(0, v20)) | ~ (t2tb1(v20) = v21) | ? [v22: % 36.69/5.69 uni] : ? [v23: int] : ( ~ (v23 = 0) & eq_prefix1(int, v15, v22, n1) % 36.69/5.69 = v23 & get(v1, int, v12, v21) = v22 & uni(v22)))))) % 36.69/5.69 % 36.69/5.69 (function-axioms) % 36.69/5.70 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 36.69/5.70 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set1(v6, v5, v4, v3, v2) = v1) | ~ % 36.69/5.70 (set1(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 36.69/5.70 MultipleValueBool] : ! [v2: int] : ! [v3: uni] : ! [v4: uni] : ! [v5: % 36.69/5.70 ty] : (v1 = v0 | ~ (eq_prefix1(v5, v4, v3, v2) = v1) | ~ (eq_prefix1(v5, % 36.69/5.70 v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 36.69/5.70 [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = % 36.69/5.70 v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 36.69/5.70 [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : (v1 = v0 | ~ % 36.69/5.70 (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, v2) = v0)) % 36.69/5.70 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 36.69/5.70 [v3: int] : ! [v4: map_int_lpmap_int_intrp] : (v1 = v0 | ~ (sorted1(v4, v3, % 36.69/5.70 v2) = v1) | ~ (sorted1(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] % 36.69/5.70 : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | ~ (const(v4, v3, v2) % 36.69/5.70 = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 36.69/5.70 [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (diff(v4, v3, v2) = v1) % 36.69/5.70 | ~ (diff(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 36.69/5.70 ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (inter(v4, v3, v2) = v1) | ~ % 36.69/5.70 (inter(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 36.69/5.70 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (union(v4, v3, v2) = v1) | ~ % 36.69/5.70 (union(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 36.69/5.70 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (remove(v4, v3, v2) = v1) | ~ % 36.69/5.70 (remove(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 36.69/5.70 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (add(v4, v3, v2) = v1) | ~ (add(v4, % 36.69/5.70 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 36.69/5.70 : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (subset(v4, v3, % 36.69/5.70 v2) = v1) | ~ (subset(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 36.69/5.70 ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = % 36.69/5.70 v0 | ~ (infix_eqeq(v4, v3, v2) = v1) | ~ (infix_eqeq(v4, v3, v2) = v0)) & % 36.69/5.70 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! % 36.69/5.70 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (mem(v4, v3, v2) = v1) | ~ (mem(v4, % 36.69/5.70 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 36.69/5.70 : ! [v2: map_int_int] : ! [v3: map_int_int] : (v1 = v0 | ~ (lt_sol1(v3, v2) % 36.69/5.70 = v1) | ~ (lt_sol1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 36.69/5.70 MultipleValueBool] : ! [v2: map_int_int] : ! [v3: int] : (v1 = v0 | ~ % 36.69/5.70 (partial_solution1(v3, v2) = v1) | ~ (partial_solution1(v3, v2) = v0)) & ! % 36.69/5.70 [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, % 36.69/5.70 v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 36.69/5.70 [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ % 36.69/5.70 (contents(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 36.69/5.70 [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & % 36.69/5.70 ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 36.69/5.70 (cardinal1(v3, v2) = v1) | ~ (cardinal1(v3, v2) = v0)) & ! [v0: uni] : ! % 36.69/5.70 [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (choose(v3, v2) = v1) | % 36.69/5.70 ~ (choose(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 36.69/5.70 MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 36.69/5.70 (is_empty(v3, v2) = v1) | ~ (is_empty(v3, v2) = v0)) & ! [v0: % 36.69/5.70 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: ty] % 36.69/5.70 : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! [v0: % 36.69/5.70 map_int_lpmap_int_intrp] : ! [v1: map_int_lpmap_int_intrp] : ! [v2: uni] : % 36.69/5.70 (v1 = v0 | ~ (tb2t3(v2) = v1) | ~ (tb2t3(v2) = v0)) & ! [v0: uni] : ! [v1: % 36.69/5.70 uni] : ! [v2: map_int_lpmap_int_intrp] : (v1 = v0 | ~ (t2tb3(v2) = v1) | % 36.69/5.70 ~ (t2tb3(v2) = v0)) & ! [v0: map_int_int] : ! [v1: map_int_int] : ! [v2: % 36.69/5.70 uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) & ! [v0: uni] % 36.69/5.70 : ! [v1: uni] : ! [v2: map_int_int] : (v1 = v0 | ~ (t2tb2(v2) = v1) | ~ % 36.69/5.70 (t2tb2(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ % 36.69/5.70 (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: set_int] : ! [v1: set_int] : % 36.69/5.70 ! [v2: set_int] : (v1 = v0 | ~ (pred1(v2) = v1) | ~ (pred1(v2) = v0)) & ! % 36.69/5.70 [v0: set_int] : ! [v1: set_int] : ! [v2: set_int] : (v1 = v0 | ~ (succ1(v2) % 36.69/5.70 = v1) | ~ (succ1(v2) = v0)) & ! [v0: set_int] : ! [v1: set_int] : ! % 36.69/5.70 [v2: int] : (v1 = v0 | ~ (below1(v2) = v1) | ~ (below1(v2) = v0)) & ! [v0: % 36.69/5.70 int] : ! [v1: int] : ! [v2: set_int] : (v1 = v0 | ~ (max_elt1(v2) = v1) | % 36.69/5.70 ~ (max_elt1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: set_int] : % 36.69/5.70 (v1 = v0 | ~ (min_elt1(v2) = v1) | ~ (min_elt1(v2) = v0)) & ! [v0: int] : % 36.69/5.70 ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ (tb2t1(v2) = % 36.69/5.70 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ % 36.69/5.70 (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: set_int] : ! [v1: % 36.69/5.70 set_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = % 36.69/5.70 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: set_int] : (v1 = v0 | ~ % 36.69/5.70 (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 36.69/5.70 [v2: ty] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0: ty] % 36.69/5.70 : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (set(v2) = v1) | ~ (set(v2) = % 36.69/5.70 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ % 36.69/5.70 (witness1(v2) = v1) | ~ (witness1(v2) = v0)) % 36.69/5.70 % 36.69/5.70 Further assumptions not needed in the proof: % 36.69/5.70 -------------------------------------------- % 36.69/5.70 add_def1, add_remove, add_sort1, bool_inversion, bridgeL, bridgeL1, bridgeL2, % 36.69/5.70 bridgeL3, bridgeR, bridgeR1, bridgeR2, bridgeR3, cardinal1, cardinal_add, % 36.69/5.70 cardinal_below, cardinal_nonneg, cardinal_remove, cardinal_subset, choose_def, % 36.69/5.70 choose_sort1, compatOrderMult, const, const_sort1, contents_def1, % 36.69/5.70 contents_sort1, diff_def1, diff_sort1, empty_def1, empty_sort1, extensionality, % 36.69/5.70 get_sort1, infix_eqeq_def, inter_def1, inter_sort1, is_empty_def, lt_sol_def, % 36.69/5.70 match_bool_False, match_bool_True, match_bool_sort1, mem_empty, mk_ref_sort1, % 36.69/5.70 no_duplicate, partial_solution_eq_prefix, pred_def, ref_inversion1, remove_add, % 36.69/5.70 remove_def1, remove_sort1, select_eq, select_neq, set_sort1, sorted_def, % 36.69/5.70 subset_def, subset_diff, subset_refl, subset_remove, subset_trans, succ_def, % 36.69/5.70 t2tb_sort, t2tb_sort1, t2tb_sort3, true_False, tuple0_inversion, union_def1, % 36.69/5.70 union_sort1, witness_sort1 % 36.69/5.70 % 36.69/5.70 Those formulas are unsatisfiable: % 36.69/5.70 --------------------------------- % 36.69/5.70 % 36.69/5.70 Begin of proof % 36.69/5.70 | % 36.69/5.70 | ALPHA: (cardinal_empty) implies: % 36.69/5.70 | (1) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (cardinal1(v0, % 36.69/5.70 | v1) = v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: int] : ( ~ (v3 = 0) % 36.69/5.70 | & is_empty(v0, v1) = v3)) % 36.69/5.70 | % 36.69/5.70 | ALPHA: (min_elt_def1) implies: % 36.69/5.71 | (2) ! [v0: set_int] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) % 36.69/5.71 | | ? [v2: any] : ? [v3: int] : ? [v4: uni] : ? [v5: any] : % 36.69/5.71 | (min_elt1(v0) = v3 & t2tb1(v3) = v4 & is_empty(int, v1) = v2 & % 36.69/5.71 | mem(int, v4, v1) = v5 & uni(v4) & (v5 = 0 | v2 = 0))) % 36.69/5.71 | (3) ! [v0: set_int] : ! [v1: int] : ( ~ (min_elt1(v0) = v1) | ~ % 36.69/5.71 | set_int(v0) | ? [v2: uni] : ? [v3: any] : ? [v4: uni] : ? [v5: % 36.69/5.71 | any] : (t2tb1(v1) = v4 & t2tb(v0) = v2 & is_empty(int, v2) = v3 & % 36.69/5.71 | mem(int, v4, v2) = v5 & uni(v4) & uni(v2) & (v5 = 0 | v3 = 0))) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (min_elt_def2) implies: % 36.69/5.71 | (4) ! [v0: set_int] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) % 36.69/5.71 | | ? [v2: any] : ? [v3: int] : (min_elt1(v0) = v3 & is_empty(int, % 36.69/5.71 | v1) = v2 & (v2 = 0 | ! [v4: int] : ! [v5: uni] : ( ~ % 36.69/5.71 | ($lesseq(1, $difference(v3, v4))) | ~ (t2tb1(v4) = v5) | ? % 36.69/5.71 | [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v1) = v6))))) % 36.69/5.71 | (5) ! [v0: set_int] : ! [v1: int] : ( ~ (min_elt1(v0) = v1) | ~ % 36.69/5.71 | set_int(v0) | ? [v2: uni] : ? [v3: any] : (t2tb(v0) = v2 & % 36.69/5.71 | is_empty(int, v2) = v3 & uni(v2) & (v3 = 0 | ! [v4: int] : ! [v5: % 36.69/5.71 | uni] : ( ~ ($lesseq(1, $difference(v1, v4))) | ~ (t2tb1(v4) = % 36.69/5.71 | v5) | ? [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v2) = % 36.69/5.71 | v6))))) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (max_elt_def1) implies: % 36.69/5.71 | (6) ! [v0: set_int] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) % 36.69/5.71 | | ? [v2: any] : ? [v3: int] : ? [v4: uni] : ? [v5: any] : % 36.69/5.71 | (max_elt1(v0) = v3 & t2tb1(v3) = v4 & is_empty(int, v1) = v2 & % 36.69/5.71 | mem(int, v4, v1) = v5 & uni(v4) & (v5 = 0 | v2 = 0))) % 36.69/5.71 | (7) ! [v0: set_int] : ! [v1: int] : ( ~ (max_elt1(v0) = v1) | ~ % 36.69/5.71 | set_int(v0) | ? [v2: uni] : ? [v3: any] : ? [v4: uni] : ? [v5: % 36.69/5.71 | any] : (t2tb1(v1) = v4 & t2tb(v0) = v2 & is_empty(int, v2) = v3 & % 36.69/5.71 | mem(int, v4, v2) = v5 & uni(v4) & uni(v2) & (v5 = 0 | v3 = 0))) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (max_elt_def2) implies: % 36.69/5.71 | (8) ! [v0: set_int] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ set_int(v0) % 36.69/5.71 | | ? [v2: any] : ? [v3: int] : (max_elt1(v0) = v3 & is_empty(int, % 36.69/5.71 | v1) = v2 & (v2 = 0 | ! [v4: int] : ! [v5: uni] : ( ~ % 36.69/5.71 | ($lesseq(1, $difference(v4, v3))) | ~ (t2tb1(v4) = v5) | ? % 36.69/5.71 | [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v1) = v6))))) % 36.69/5.71 | (9) ! [v0: set_int] : ! [v1: int] : ( ~ (max_elt1(v0) = v1) | ~ % 36.69/5.71 | set_int(v0) | ? [v2: uni] : ? [v3: any] : (t2tb(v0) = v2 & % 36.69/5.71 | is_empty(int, v2) = v3 & uni(v2) & (v3 = 0 | ! [v4: int] : ! [v5: % 36.69/5.71 | uni] : ( ~ ($lesseq(1, $difference(v4, v1))) | ~ (t2tb1(v4) = % 36.69/5.71 | v5) | ? [v6: int] : ( ~ (v6 = 0) & mem(int, v5, v2) = % 36.69/5.71 | v6))))) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (below_def) implies: % 36.69/5.71 | (10) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: set_int] : ! % 36.69/5.71 | [v4: uni] : ( ~ ($lesseq(v0, -1)) | ~ (below1(v1) = v3) | ~ % 36.69/5.71 | (t2tb1(v0) = v2) | ~ (t2tb(v3) = v4) | ~ (mem(int, v2, v4) = 0)) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (eq_prefix_def) implies: % 36.69/5.71 | (11) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: % 36.69/5.71 | int] : (v4 = 0 | ~ (eq_prefix1(v0, v1, v2, v3) = v4) | ~ ty(v0) | % 36.69/5.71 | ~ uni(v2) | ~ uni(v1) | ? [v5: int] : ? [v6: uni] : ? [v7: uni] % 36.69/5.71 | : ? [v8: uni] : ( ~ (v8 = v7) & $lesseq(1, $difference(v3, v5)) & % 36.69/5.71 | $lesseq(0, v5) & get(v0, int, v2, v6) = v8 & get(v0, int, v1, v6) % 36.69/5.71 | = v7 & t2tb1(v5) = v6 & uni(v8) & uni(v7) & uni(v6))) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (t2tb_sort2) implies: % 36.69/5.71 | (12) ? [v0: ty] : (map(int, int) = v0 & ty(v0) & ! [v1: map_int_int] : ! % 36.69/5.71 | [v2: uni] : ( ~ (t2tb2(v1) = v2) | ~ map_int_int(v1) | sort1(v0, % 36.69/5.71 | v2) = 0)) % 36.69/5.71 | % 36.69/5.71 | ALPHA: (partial_solution_def) implies: % 36.69/5.72 | (13) ! [v0: int] : ! [v1: map_int_int] : ! [v2: int] : (v2 = 0 | ~ % 36.69/5.72 | (partial_solution1(v0, v1) = v2) | ~ map_int_int(v1) | ? [v3: uni] % 36.69/5.72 | : ? [v4: int] : ? [v5: uni] : ? [v6: uni] : ? [v7: int] : ? % 36.69/5.72 | [v8: int] : ? [v9: uni] : ? [v10: uni] : ? [v11: int] : % 36.69/5.72 | ($lesseq(1, $difference(v0, v4)) & $lesseq(0, v4) & t2tb2(v1) = v3 & % 36.69/5.72 | get(int, int, v3, v5) = v6 & tb2t1(v6) = v7 & t2tb1(v4) = v5 & % 36.69/5.72 | uni(v6) & uni(v5) & uni(v3) & ( ~ ($lesseq(1, $difference(n1, % 36.69/5.72 | v7))) | ~ ($lesseq(0, v7)) | ($lesseq(1, $difference(v4, % 36.69/5.72 | v8)) & $lesseq(0, v8) & get(int, int, v3, v9) = v10 & % 36.69/5.72 | tb2t1(v10) = v11 & t2tb1(v8) = v9 & uni(v10) & uni(v9) & % 36.69/5.72 | ($sum($difference($difference(v11, v8), v7), v4) = 0 | % 36.69/5.72 | $difference($sum(v11, v8), v7) = v4 | v11 = v7))))) % 36.69/5.72 | % 36.69/5.72 | ALPHA: (wP_parameter_queens3) implies: % 36.69/5.72 | (14) ty(int) % 36.69/5.72 | (15) ? [v0: uni] : ? [v1: ty] : ? [v2: map_int_lpmap_int_intrp] : ? % 36.69/5.72 | [v3: map_int_int] : ? [v4: set_int] : ? [v5: uni] : ? [v6: uni] : % 36.69/5.72 | ? [v7: uni] : ? [v8: int] : ? [v9: map_int_lpmap_int_intrp] : ? % 36.69/5.72 | [v10: map_int_int] : ? [v11: uni] : ? [v12: uni] : ? [v13: % 36.69/5.72 | map_int_int] : ? [v14: any] : ? [v15: uni] : ? [v16: int] : ? % 36.69/5.72 | [v17: uni] : ? [v18: uni] : ? [v19: int] : ($lesseq(0, v8) & % 36.69/5.72 | $lesseq(0, n1) & sorted1(v9, 0, v8) = 0 & t2tb3(v9) = v12 & % 36.69/5.72 | t2tb3(v2) = v7 & partial_solution1(n1, v13) = v14 & % 36.69/5.72 | partial_solution1(0, v3) = 0 & t2tb2(v13) = v15 & t2tb2(v10) = v11 & % 36.69/5.72 | t2tb2(v3) = v6 & eq_prefix1(v1, v7, v12, 0) = 0 & eq_prefix1(int, % 36.69/5.72 | v6, v11, 0) = 0 & map(int, int) = v1 & below1(n1) = v4 & t2tb(v4) % 36.69/5.72 | = v5 & cardinal1(int, v5) = n1 & empty(int) = v0 & % 36.69/5.72 | map_int_lpmap_int_intrp(v9) & map_int_lpmap_int_intrp(v2) & % 36.69/5.72 | map_int_int(v13) & map_int_int(v10) & map_int_int(v3) & set_int(v4) % 36.69/5.72 | & ty(v1) & uni(v15) & uni(v12) & uni(v11) & uni(v7) & uni(v6) & % 36.69/5.72 | uni(v5) & uni(v0) & ! [v20: map_int_int] : ! [v21: uni] : ! [v22: % 36.69/5.72 | int] : ! [v23: uni] : ( ~ ($lesseq(1, $difference(v8, v22))) | ~ % 36.69/5.72 | ($lesseq(0, v22)) | ~ (t2tb2(v20) = v21) | ~ (t2tb1(v22) = v23) % 36.69/5.72 | | ~ map_int_int(v20) | ? [v24: any] : ? [v25: int] : ((v25 = 0 % 36.69/5.72 | & v24 = 0 & partial_solution1(n1, v20) = 0 & eq_prefix1(int, % 36.69/5.72 | v11, v21, 0) = 0) | ( ~ (v25 = 0) & eq_prefix1(int, v21, % 36.69/5.72 | v24, n1) = v25 & get(v1, int, v12, v23) = v24 & uni(v24)))) % 36.69/5.72 | & ! [v20: int] : ! [v21: uni] : ( ~ ($lesseq(1, $difference(n1, % 36.69/5.72 | v20))) | ~ ($lesseq(0, v20)) | ~ (t2tb1(v20) = v21) | % 36.69/5.72 | mem(int, v21, v5) = 0) & ! [v20: int] : ! [v21: uni] : ( ~ % 36.69/5.72 | ($lesseq(v20, -1)) | ~ (t2tb1(v20) = v21) | ? [v22: int] : ( ~ % 36.69/5.72 | (v22 = 0) & mem(int, v21, v5) = v22)) & ! [v20: int] : ! [v21: % 36.69/5.72 | uni] : ( ~ ($lesseq(n1, v20)) | ~ (t2tb1(v20) = v21) | ? [v22: % 36.69/5.72 | int] : ( ~ (v22 = 0) & mem(int, v21, v5) = v22)) & ! [v20: int] % 36.69/5.72 | : ! [v21: uni] : ( ~ ($lesseq(0, v20)) | ~ (t2tb1(v20) = v21) | ? % 36.69/5.72 | [v22: int] : ( ~ (v22 = 0) & mem(int, v21, v0) = v22)) & ! [v20: % 36.69/5.72 | map_int_int] : ! [v21: any] : ( ~ (partial_solution1(n1, v20) = % 36.69/5.72 | v21) | ~ map_int_int(v20) | ? [v22: uni] : ? [v23: any] : % 36.69/5.72 | (t2tb2(v20) = v22 & eq_prefix1(int, v11, v22, 0) = v23 & uni(v22) % 36.69/5.72 | & ( ! [v24: int] : ! [v25: uni] : ( ~ ($lesseq(1, % 36.69/5.72 | $difference(v8, v24))) | ~ ($lesseq(0, v24)) | ~ % 36.69/5.72 | (t2tb1(v24) = v25) | ? [v26: uni] : ? [v27: int] : ( ~ % 36.69/5.72 | (v27 = 0) & eq_prefix1(int, v22, v26, n1) = v27 & get(v1, % 36.69/5.72 | int, v12, v25) = v26 & uni(v26))) | (v23 = 0 & v21 = % 36.69/5.72 | 0)))) & ! [v20: map_int_int] : ! [v21: uni] : ( ~ % 36.69/5.72 | (t2tb2(v20) = v21) | ~ map_int_int(v20) | ? [v22: int] : ? % 36.69/5.72 | [v23: any] : ? [v24: uni] : ? [v25: int] : ((v25 = 0 & % 36.69/5.72 | $lesseq(1, $difference(v8, v22)) & $lesseq(0, v22) & % 36.69/5.72 | eq_prefix1(int, v21, v24, n1) = 0 & get(v1, int, v12, v23) = % 36.69/5.72 | v24 & t2tb1(v22) = v23 & uni(v24) & uni(v23)) | % 36.69/5.72 | (partial_solution1(n1, v20) = v22 & eq_prefix1(int, v11, v21, 0) % 36.69/5.72 | = v23 & ( ~ (v23 = 0) | ~ (v22 = 0))))) & ! [v20: % 36.69/5.72 | map_int_int] : ( ~ (partial_solution1(n1, v20) = 0) | ~ % 36.69/5.72 | map_int_int(v20) | ? [v21: uni] : ? [v22: any] : ? [v23: int] : % 36.69/5.72 | ? [v24: uni] : ? [v25: uni] : ? [v26: int] : (t2tb2(v20) = v21 % 36.69/5.72 | & eq_prefix1(int, v11, v21, 0) = v22 & uni(v21) & ( ~ (v22 = 0) % 36.69/5.72 | | (v26 = 0 & $lesseq(1, $difference(v8, v23)) & $lesseq(0, % 36.69/5.72 | v23) & eq_prefix1(int, v21, v25, n1) = 0 & get(v1, int, % 36.69/5.72 | v12, v24) = v25 & t2tb1(v23) = v24 & uni(v25) & % 36.69/5.72 | uni(v24))))) & ((v19 = 0 & ~ (v14 = 0) & $lesseq(1, % 36.69/5.72 | $difference(v8, v16)) & $lesseq(0, v16) & eq_prefix1(int, v15, % 36.69/5.72 | v18, n1) = 0 & get(v1, int, v12, v17) = v18 & t2tb1(v16) = v17 % 36.69/5.72 | & uni(v18) & uni(v17)) | (v14 = 0 & ! [v20: int] : ! [v21: % 36.69/5.72 | uni] : ( ~ ($lesseq(1, $difference(v8, v20))) | ~ ($lesseq(0, % 36.69/5.72 | v20)) | ~ (t2tb1(v20) = v21) | ? [v22: uni] : ? [v23: % 36.69/5.72 | int] : ( ~ (v23 = 0) & eq_prefix1(int, v15, v22, n1) = v23 & % 36.69/5.72 | get(v1, int, v12, v21) = v22 & uni(v22)))))) % 36.69/5.72 | % 36.69/5.72 | ALPHA: (function-axioms) implies: % 36.69/5.72 | (16) ! [v0: uni] : ! [v1: uni] : ! [v2: set_int] : (v1 = v0 | ~ % 36.69/5.72 | (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) % 36.69/5.72 | (17) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb1(v2) % 36.69/5.72 | = v1) | ~ (t2tb1(v2) = v0)) % 36.69/5.72 | (18) ! [v0: int] : ! [v1: int] : ! [v2: set_int] : (v1 = v0 | ~ % 36.69/5.72 | (min_elt1(v2) = v1) | ~ (min_elt1(v2) = v0)) % 36.69/5.72 | (19) ! [v0: int] : ! [v1: int] : ! [v2: set_int] : (v1 = v0 | ~ % 36.69/5.72 | (max_elt1(v2) = v1) | ~ (max_elt1(v2) = v0)) % 36.69/5.72 | (20) ! [v0: uni] : ! [v1: uni] : ! [v2: map_int_int] : (v1 = v0 | ~ % 36.69/5.73 | (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) % 36.69/5.73 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 36.69/5.73 | : ! [v3: ty] : (v1 = v0 | ~ (is_empty(v3, v2) = v1) | ~ % 36.69/5.73 | (is_empty(v3, v2) = v0)) % 36.69/5.73 | (22) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ % 36.69/5.73 | (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) % 36.69/5.73 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 36.69/5.73 | map_int_int] : ! [v3: int] : (v1 = v0 | ~ (partial_solution1(v3, % 36.69/5.73 | v2) = v1) | ~ (partial_solution1(v3, v2) = v0)) % 36.69/5.73 | (24) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 36.69/5.73 | : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (mem(v4, v3, v2) = v1) | % 36.69/5.73 | ~ (mem(v4, v3, v2) = v0)) % 36.69/5.73 | (25) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 36.69/5.73 | ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 36.69/5.73 | (get(v5, v4, v3, v2) = v0)) % 36.69/5.73 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] % 36.69/5.73 | : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ % 36.69/5.73 | (eq_prefix1(v5, v4, v3, v2) = v1) | ~ (eq_prefix1(v5, v4, v3, v2) = % 36.69/5.73 | v0)) % 36.69/5.73 | % 36.69/5.73 | DELTA: instantiating (12) with fresh symbol all_87_0 gives: % 36.69/5.73 | (27) map(int, int) = all_87_0 & ty(all_87_0) & ! [v0: map_int_int] : ! % 36.69/5.73 | [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ map_int_int(v0) | % 36.69/5.73 | sort1(all_87_0, v1) = 0) % 36.69/5.73 | % 36.69/5.73 | ALPHA: (27) implies: % 36.69/5.73 | (28) map(int, int) = all_87_0 % 36.69/5.73 | % 36.69/5.73 | DELTA: instantiating (15) with fresh symbols all_102_0, all_102_1, all_102_2, % 36.69/5.73 | all_102_3, all_102_4, all_102_5, all_102_6, all_102_7, all_102_8, % 36.69/5.73 | all_102_9, all_102_10, all_102_11, all_102_12, all_102_13, all_102_14, % 36.69/5.73 | all_102_15, all_102_16, all_102_17, all_102_18, all_102_19 gives: % 36.69/5.73 | (29) $lesseq(0, all_102_11) & $lesseq(0, n1) & sorted1(all_102_10, 0, % 36.69/5.73 | all_102_11) = 0 & t2tb3(all_102_10) = all_102_7 & t2tb3(all_102_17) % 36.69/5.73 | = all_102_12 & partial_solution1(n1, all_102_6) = all_102_5 & % 36.69/5.73 | partial_solution1(0, all_102_16) = 0 & t2tb2(all_102_6) = all_102_4 & % 36.69/5.73 | t2tb2(all_102_9) = all_102_8 & t2tb2(all_102_16) = all_102_13 & % 36.69/5.73 | eq_prefix1(all_102_18, all_102_12, all_102_7, 0) = 0 & eq_prefix1(int, % 36.69/5.73 | all_102_13, all_102_8, 0) = 0 & map(int, int) = all_102_18 & % 36.69/5.73 | below1(n1) = all_102_15 & t2tb(all_102_15) = all_102_14 & % 36.69/5.73 | cardinal1(int, all_102_14) = n1 & empty(int) = all_102_19 & % 36.69/5.73 | map_int_lpmap_int_intrp(all_102_10) & % 36.69/5.73 | map_int_lpmap_int_intrp(all_102_17) & map_int_int(all_102_6) & % 36.69/5.73 | map_int_int(all_102_9) & map_int_int(all_102_16) & set_int(all_102_15) % 36.69/5.73 | & ty(all_102_18) & uni(all_102_4) & uni(all_102_7) & uni(all_102_8) & % 36.69/5.73 | uni(all_102_12) & uni(all_102_13) & uni(all_102_14) & uni(all_102_19) % 36.69/5.73 | & ! [v0: map_int_int] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : % 36.69/5.73 | ( ~ ($lesseq(1, $difference(all_102_11, v2))) | ~ ($lesseq(0, v2)) | % 36.69/5.73 | ~ (t2tb2(v0) = v1) | ~ (t2tb1(v2) = v3) | ~ map_int_int(v0) | ? % 36.69/5.73 | [v4: any] : ? [v5: int] : ((v5 = 0 & v4 = 0 & partial_solution1(n1, % 36.69/5.73 | v0) = 0 & eq_prefix1(int, all_102_8, v1, 0) = 0) | ( ~ (v5 = % 36.69/5.73 | 0) & eq_prefix1(int, v1, v4, n1) = v5 & get(all_102_18, int, % 36.69/5.73 | all_102_7, v3) = v4 & uni(v4)))) & ! [v0: int] : ! [v1: uni] % 36.69/5.73 | : ( ~ ($lesseq(1, $difference(n1, v0))) | ~ ($lesseq(0, v0)) | ~ % 36.69/5.73 | (t2tb1(v0) = v1) | mem(int, v1, all_102_14) = 0) & ! [v0: int] : ! % 36.69/5.73 | [v1: uni] : ( ~ ($lesseq(v0, -1)) | ~ (t2tb1(v0) = v1) | ? [v2: int] % 36.69/5.73 | : ( ~ (v2 = 0) & mem(int, v1, all_102_14) = v2)) & ! [v0: int] : ! % 36.69/5.73 | [v1: uni] : ( ~ ($lesseq(n1, v0)) | ~ (t2tb1(v0) = v1) | ? [v2: int] % 36.69/5.73 | : ( ~ (v2 = 0) & mem(int, v1, all_102_14) = v2)) & ! [v0: int] : ! % 36.69/5.73 | [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (t2tb1(v0) = v1) | ? [v2: int] % 36.69/5.73 | : ( ~ (v2 = 0) & mem(int, v1, all_102_19) = v2)) & ! [v0: % 36.69/5.73 | map_int_int] : ! [v1: any] : ( ~ (partial_solution1(n1, v0) = v1) | % 36.69/5.73 | ~ map_int_int(v0) | ? [v2: uni] : ? [v3: any] : (t2tb2(v0) = v2 & % 36.69/5.73 | eq_prefix1(int, all_102_8, v2, 0) = v3 & uni(v2) & ( ! [v4: int] : % 36.69/5.73 | ! [v5: uni] : ( ~ ($lesseq(1, $difference(all_102_11, v4))) | % 36.69/5.73 | ~ ($lesseq(0, v4)) | ~ (t2tb1(v4) = v5) | ? [v6: uni] : ? % 36.69/5.73 | [v7: int] : ( ~ (v7 = 0) & eq_prefix1(int, v2, v6, n1) = v7 & % 36.69/5.73 | get(all_102_18, int, all_102_7, v5) = v6 & uni(v6))) | (v3 = % 36.69/5.73 | 0 & v1 = 0)))) & ! [v0: map_int_int] : ! [v1: uni] : ( ~ % 36.69/5.74 | (t2tb2(v0) = v1) | ~ map_int_int(v0) | ? [v2: int] : ? [v3: any] % 36.69/5.74 | : ? [v4: uni] : ? [v5: int] : ((v5 = 0 & $lesseq(1, % 36.69/5.74 | $difference(all_102_11, v2)) & $lesseq(0, v2) & % 36.69/5.74 | eq_prefix1(int, v1, v4, n1) = 0 & get(all_102_18, int, % 36.69/5.74 | all_102_7, v3) = v4 & t2tb1(v2) = v3 & uni(v4) & uni(v3)) | % 36.69/5.74 | (partial_solution1(n1, v0) = v2 & eq_prefix1(int, all_102_8, v1, % 36.69/5.74 | 0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0))))) & ! [v0: % 36.69/5.74 | map_int_int] : ( ~ (partial_solution1(n1, v0) = 0) | ~ % 36.69/5.74 | map_int_int(v0) | ? [v1: uni] : ? [v2: any] : ? [v3: int] : ? % 36.69/5.74 | [v4: uni] : ? [v5: uni] : ? [v6: int] : (t2tb2(v0) = v1 & % 36.69/5.74 | eq_prefix1(int, all_102_8, v1, 0) = v2 & uni(v1) & ( ~ (v2 = 0) | % 36.69/5.74 | (v6 = 0 & $lesseq(1, $difference(all_102_11, v3)) & $lesseq(0, % 36.69/5.74 | v3) & eq_prefix1(int, v1, v5, n1) = 0 & get(all_102_18, int, % 36.69/5.74 | all_102_7, v4) = v5 & t2tb1(v3) = v4 & uni(v5) & uni(v4))))) % 36.69/5.74 | & ((all_102_0 = 0 & ~ (all_102_5 = 0) & $lesseq(1, % 36.69/5.74 | $difference(all_102_11, all_102_3)) & $lesseq(0, all_102_3) & % 36.69/5.74 | eq_prefix1(int, all_102_4, all_102_1, n1) = 0 & get(all_102_18, % 36.69/5.74 | int, all_102_7, all_102_2) = all_102_1 & t2tb1(all_102_3) = % 36.69/5.74 | all_102_2 & uni(all_102_1) & uni(all_102_2)) | (all_102_5 = 0 & ! % 36.69/5.74 | [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_102_11, % 36.69/5.74 | v0))) | ~ ($lesseq(0, v0)) | ~ (t2tb1(v0) = v1) | ? % 36.69/5.74 | [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & eq_prefix1(int, % 36.69/5.74 | all_102_4, v2, n1) = v3 & get(all_102_18, int, all_102_7, % 36.69/5.74 | v1) = v2 & uni(v2))))) % 36.69/5.74 | % 36.69/5.74 | ALPHA: (29) implies: % 36.69/5.74 | (30) uni(all_102_14) % 36.69/5.74 | (31) uni(all_102_8) % 36.69/5.74 | (32) set_int(all_102_15) % 36.69/5.74 | (33) map_int_int(all_102_9) % 36.69/5.74 | (34) map_int_int(all_102_6) % 36.69/5.74 | (35) cardinal1(int, all_102_14) = n1 % 36.69/5.74 | (36) t2tb(all_102_15) = all_102_14 % 36.69/5.74 | (37) below1(n1) = all_102_15 % 36.69/5.74 | (38) map(int, int) = all_102_18 % 36.69/5.74 | (39) t2tb2(all_102_9) = all_102_8 % 36.69/5.74 | (40) t2tb2(all_102_6) = all_102_4 % 36.69/5.74 | (41) partial_solution1(n1, all_102_6) = all_102_5 % 36.69/5.74 | (42) (all_102_0 = 0 & ~ (all_102_5 = 0) & $lesseq(1, % 36.69/5.74 | $difference(all_102_11, all_102_3)) & $lesseq(0, all_102_3) & % 36.69/5.74 | eq_prefix1(int, all_102_4, all_102_1, n1) = 0 & get(all_102_18, int, % 36.69/5.74 | all_102_7, all_102_2) = all_102_1 & t2tb1(all_102_3) = all_102_2 & % 36.69/5.74 | uni(all_102_1) & uni(all_102_2)) | (all_102_5 = 0 & ! [v0: int] : % 36.69/5.74 | ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_102_11, v0))) | ~ % 36.69/5.74 | ($lesseq(0, v0)) | ~ (t2tb1(v0) = v1) | ? [v2: uni] : ? [v3: % 36.69/5.74 | int] : ( ~ (v3 = 0) & eq_prefix1(int, all_102_4, v2, n1) = v3 & % 36.69/5.74 | get(all_102_18, int, all_102_7, v1) = v2 & uni(v2)))) % 36.69/5.74 | (43) ! [v0: map_int_int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ % 36.69/5.74 | map_int_int(v0) | ? [v2: int] : ? [v3: any] : ? [v4: uni] : ? % 36.69/5.74 | [v5: int] : ((v5 = 0 & $lesseq(1, $difference(all_102_11, v2)) & % 36.69/5.74 | $lesseq(0, v2) & eq_prefix1(int, v1, v4, n1) = 0 & % 36.69/5.74 | get(all_102_18, int, all_102_7, v3) = v4 & t2tb1(v2) = v3 & % 36.69/5.74 | uni(v4) & uni(v3)) | (partial_solution1(n1, v0) = v2 & % 36.69/5.74 | eq_prefix1(int, all_102_8, v1, 0) = v3 & ( ~ (v3 = 0) | ~ (v2 = % 36.69/5.74 | 0))))) % 36.69/5.74 | (44) ! [v0: map_int_int] : ! [v1: any] : ( ~ (partial_solution1(n1, v0) = % 36.69/5.74 | v1) | ~ map_int_int(v0) | ? [v2: uni] : ? [v3: any] : % 36.69/5.74 | (t2tb2(v0) = v2 & eq_prefix1(int, all_102_8, v2, 0) = v3 & uni(v2) & % 36.69/5.74 | ( ! [v4: int] : ! [v5: uni] : ( ~ ($lesseq(1, % 36.69/5.74 | $difference(all_102_11, v4))) | ~ ($lesseq(0, v4)) | ~ % 36.69/5.74 | (t2tb1(v4) = v5) | ? [v6: uni] : ? [v7: int] : ( ~ (v7 = 0) % 36.69/5.74 | & eq_prefix1(int, v2, v6, n1) = v7 & get(all_102_18, int, % 36.69/5.74 | all_102_7, v5) = v6 & uni(v6))) | (v3 = 0 & v1 = 0)))) % 36.69/5.74 | (45) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (t2tb1(v0) = % 36.69/5.74 | v1) | ? [v2: int] : ( ~ (v2 = 0) & mem(int, v1, all_102_19) = % 36.69/5.74 | v2)) % 36.69/5.74 | (46) ! [v0: map_int_int] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ( % 36.69/5.74 | ~ ($lesseq(1, $difference(all_102_11, v2))) | ~ ($lesseq(0, v2)) | % 36.69/5.74 | ~ (t2tb2(v0) = v1) | ~ (t2tb1(v2) = v3) | ~ map_int_int(v0) | ? % 36.69/5.74 | [v4: any] : ? [v5: int] : ((v5 = 0 & v4 = 0 & partial_solution1(n1, % 36.69/5.74 | v0) = 0 & eq_prefix1(int, all_102_8, v1, 0) = 0) | ( ~ (v5 = % 36.69/5.74 | 0) & eq_prefix1(int, v1, v4, n1) = v5 & get(all_102_18, int, % 36.69/5.74 | all_102_7, v3) = v4 & uni(v4)))) % 36.69/5.74 | % 36.69/5.74 | GROUND_INST: instantiating (22) with all_87_0, all_102_18, int, int, % 36.69/5.74 | simplifying with (28), (38) gives: % 36.69/5.74 | (47) all_102_18 = all_87_0 % 36.69/5.74 | % 36.69/5.74 | GROUND_INST: instantiating (1) with int, all_102_14, n1, simplifying with % 36.69/5.74 | (14), (30), (35) gives: % 36.69/5.74 | (48) n1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & is_empty(int, all_102_14) = v0) % 36.69/5.74 | % 36.69/5.74 | GROUND_INST: instantiating (6) with all_102_15, all_102_14, simplifying with % 36.69/5.74 | (32), (36) gives: % 36.69/5.74 | (49) ? [v0: any] : ? [v1: int] : ? [v2: uni] : ? [v3: any] : % 36.69/5.74 | (max_elt1(all_102_15) = v1 & t2tb1(v1) = v2 & is_empty(int, % 36.69/5.74 | all_102_14) = v0 & mem(int, v2, all_102_14) = v3 & uni(v2) & (v3 = % 36.69/5.74 | 0 | v0 = 0)) % 36.69/5.74 | % 36.69/5.75 | GROUND_INST: instantiating (2) with all_102_15, all_102_14, simplifying with % 36.69/5.75 | (32), (36) gives: % 36.69/5.75 | (50) ? [v0: any] : ? [v1: int] : ? [v2: uni] : ? [v3: any] : % 36.69/5.75 | (min_elt1(all_102_15) = v1 & t2tb1(v1) = v2 & is_empty(int, % 36.69/5.75 | all_102_14) = v0 & mem(int, v2, all_102_14) = v3 & uni(v2) & (v3 = % 36.69/5.75 | 0 | v0 = 0)) % 36.69/5.75 | % 36.69/5.75 | GROUND_INST: instantiating (8) with all_102_15, all_102_14, simplifying with % 36.69/5.75 | (32), (36) gives: % 36.69/5.75 | (51) ? [v0: any] : ? [v1: int] : (max_elt1(all_102_15) = v1 & % 36.69/5.75 | is_empty(int, all_102_14) = v0 & (v0 = 0 | ! [v2: int] : ! [v3: % 36.69/5.75 | uni] : ( ~ ($lesseq(1, $difference(v2, v1))) | ~ (t2tb1(v2) = % 36.69/5.75 | v3) | ? [v4: int] : ( ~ (v4 = 0) & mem(int, v3, all_102_14) = % 36.69/5.75 | v4)))) % 36.69/5.75 | % 36.69/5.75 | GROUND_INST: instantiating (4) with all_102_15, all_102_14, simplifying with % 36.69/5.75 | (32), (36) gives: % 36.69/5.75 | (52) ? [v0: any] : ? [v1: int] : (min_elt1(all_102_15) = v1 & % 36.69/5.75 | is_empty(int, all_102_14) = v0 & (v0 = 0 | ! [v2: int] : ! [v3: % 36.69/5.75 | uni] : ( ~ ($lesseq(1, $difference(v1, v2))) | ~ (t2tb1(v2) = % 36.69/5.75 | v3) | ? [v4: int] : ( ~ (v4 = 0) & mem(int, v3, all_102_14) = % 36.69/5.75 | v4)))) % 36.69/5.75 | % 36.69/5.75 | GROUND_INST: instantiating (43) with all_102_6, all_102_4, simplifying with % 36.69/5.75 | (34), (40) gives: % 36.69/5.75 | (53) ? [v0: int] : ? [v1: any] : ? [v2: uni] : ? [v3: int] : ((v3 = 0 & % 36.69/5.75 | $lesseq(1, $difference(all_102_11, v0)) & $lesseq(0, v0) & % 36.69/5.75 | eq_prefix1(int, all_102_4, v2, n1) = 0 & get(all_102_18, int, % 36.69/5.75 | all_102_7, v1) = v2 & t2tb1(v0) = v1 & uni(v2) & uni(v1)) | % 36.69/5.75 | (partial_solution1(n1, all_102_6) = v0 & eq_prefix1(int, all_102_8, % 36.69/5.75 | all_102_4, 0) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 36.69/5.75 | % 36.69/5.75 | GROUND_INST: instantiating (44) with all_102_6, all_102_5, simplifying with % 36.69/5.75 | (34), (41) gives: % 36.69/5.75 | (54) ? [v0: uni] : ? [v1: any] : (t2tb2(all_102_6) = v0 & eq_prefix1(int, % 36.69/5.75 | all_102_8, v0, 0) = v1 & uni(v0) & ( ! [v2: int] : ! [v3: uni] : % 36.69/5.75 | ( ~ ($lesseq(1, $difference(all_102_11, v2))) | ~ ($lesseq(0, % 36.69/5.75 | v2)) | ~ (t2tb1(v2) = v3) | ? [v4: uni] : ? [v5: int] : ( % 36.69/5.75 | ~ (v5 = 0) & eq_prefix1(int, v0, v4, n1) = v5 & % 36.69/5.75 | get(all_102_18, int, all_102_7, v3) = v4 & uni(v4))) | (v1 = 0 % 36.69/5.75 | & all_102_5 = 0))) % 36.69/5.75 | % 36.69/5.75 | GROUND_INST: instantiating (13) with n1, all_102_6, all_102_5, simplifying % 36.69/5.75 | with (34), (41) gives: % 36.69/5.75 | (55) all_102_5 = 0 | ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: % 36.69/5.75 | uni] : ? [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : % 36.69/5.75 | ? [v8: int] : ($lesseq(1, $difference(n1, v1)) & $lesseq(0, v1) & % 36.69/5.75 | t2tb2(all_102_6) = v0 & get(int, int, v0, v2) = v3 & tb2t1(v3) = v4 % 36.69/5.75 | & t2tb1(v1) = v2 & uni(v3) & uni(v2) & uni(v0) & ( ~ ($lesseq(1, % 36.69/5.75 | $difference(n1, v4))) | ~ ($lesseq(0, v4)) | ($lesseq(1, % 36.69/5.75 | $difference(v1, v5)) & $lesseq(0, v5) & get(int, int, v0, v6) % 36.69/5.75 | = v7 & tb2t1(v7) = v8 & t2tb1(v5) = v6 & uni(v7) & uni(v6) & % 36.69/5.75 | ($sum($difference($difference(v8, v5), v4), v1) = 0 | % 36.69/5.75 | $difference($sum(v8, v5), v4) = v1 | v8 = v4)))) % 36.69/5.75 | % 36.69/5.75 | DELTA: instantiating (52) with fresh symbols all_130_0, all_130_1 gives: % 36.69/5.75 | (56) min_elt1(all_102_15) = all_130_0 & is_empty(int, all_102_14) = % 36.69/5.75 | all_130_1 & (all_130_1 = 0 | ! [v0: int] : ! [v1: uni] : ( ~ % 36.69/5.75 | ($lesseq(1, $difference(all_130_0, v0))) | ~ (t2tb1(v0) = v1) | % 36.69/5.75 | ? [v2: int] : ( ~ (v2 = 0) & mem(int, v1, all_102_14) = v2))) % 36.69/5.75 | % 36.69/5.75 | ALPHA: (56) implies: % 36.69/5.75 | (57) is_empty(int, all_102_14) = all_130_1 % 36.69/5.75 | (58) min_elt1(all_102_15) = all_130_0 % 36.69/5.75 | % 36.69/5.75 | DELTA: instantiating (50) with fresh symbols all_132_0, all_132_1, all_132_2, % 36.69/5.75 | all_132_3 gives: % 36.69/5.75 | (59) min_elt1(all_102_15) = all_132_2 & t2tb1(all_132_2) = all_132_1 & % 36.69/5.75 | is_empty(int, all_102_14) = all_132_3 & mem(int, all_132_1, % 36.69/5.75 | all_102_14) = all_132_0 & uni(all_132_1) & (all_132_0 = 0 | % 36.69/5.75 | all_132_3 = 0) % 36.69/5.75 | % 36.69/5.75 | ALPHA: (59) implies: % 36.69/5.75 | (60) is_empty(int, all_102_14) = all_132_3 % 36.69/5.75 | (61) min_elt1(all_102_15) = all_132_2 % 36.69/5.75 | % 36.69/5.75 | DELTA: instantiating (49) with fresh symbols all_134_0, all_134_1, all_134_2, % 36.69/5.75 | all_134_3 gives: % 36.69/5.75 | (62) max_elt1(all_102_15) = all_134_2 & t2tb1(all_134_2) = all_134_1 & % 36.69/5.75 | is_empty(int, all_102_14) = all_134_3 & mem(int, all_134_1, % 36.69/5.75 | all_102_14) = all_134_0 & uni(all_134_1) & (all_134_0 = 0 | % 36.69/5.75 | all_134_3 = 0) % 36.69/5.75 | % 36.69/5.75 | ALPHA: (62) implies: % 36.69/5.75 | (63) mem(int, all_134_1, all_102_14) = all_134_0 % 36.69/5.75 | (64) is_empty(int, all_102_14) = all_134_3 % 36.69/5.75 | (65) t2tb1(all_134_2) = all_134_1 % 36.69/5.75 | (66) max_elt1(all_102_15) = all_134_2 % 36.69/5.75 | % 36.69/5.75 | DELTA: instantiating (51) with fresh symbols all_136_0, all_136_1 gives: % 36.69/5.76 | (67) max_elt1(all_102_15) = all_136_0 & is_empty(int, all_102_14) = % 36.69/5.76 | all_136_1 & (all_136_1 = 0 | ! [v0: int] : ! [v1: uni] : ( ~ % 36.69/5.76 | ($lesseq(1, $difference(v0, all_136_0))) | ~ (t2tb1(v0) = v1) | % 36.69/5.76 | ? [v2: int] : ( ~ (v2 = 0) & mem(int, v1, all_102_14) = v2))) % 36.69/5.76 | % 36.69/5.76 | ALPHA: (67) implies: % 36.69/5.76 | (68) is_empty(int, all_102_14) = all_136_1 % 36.69/5.76 | (69) max_elt1(all_102_15) = all_136_0 % 36.69/5.76 | % 36.69/5.76 | DELTA: instantiating (53) with fresh symbols all_143_0, all_143_1, all_143_2, % 36.69/5.76 | all_143_3 gives: % 36.69/5.76 | (70) (all_143_0 = 0 & $lesseq(1, $difference(all_102_11, all_143_3)) & % 36.69/5.76 | $lesseq(0, all_143_3) & eq_prefix1(int, all_102_4, all_143_1, n1) = % 36.69/5.76 | 0 & get(all_102_18, int, all_102_7, all_143_2) = all_143_1 & % 36.69/5.76 | t2tb1(all_143_3) = all_143_2 & uni(all_143_1) & uni(all_143_2)) | % 36.69/5.76 | (partial_solution1(n1, all_102_6) = all_143_3 & eq_prefix1(int, % 36.69/5.76 | all_102_8, all_102_4, 0) = all_143_2 & ( ~ (all_143_2 = 0) | ~ % 36.69/5.76 | (all_143_3 = 0))) % 36.69/5.76 | % 36.69/5.76 | DELTA: instantiating (54) with fresh symbols all_144_0, all_144_1 gives: % 36.69/5.76 | (71) t2tb2(all_102_6) = all_144_1 & eq_prefix1(int, all_102_8, all_144_1, % 36.69/5.76 | 0) = all_144_0 & uni(all_144_1) & ( ! [v0: int] : ! [v1: uni] : ( ~ % 36.69/5.76 | ($lesseq(1, $difference(all_102_11, v0))) | ~ ($lesseq(0, v0)) | % 36.69/5.76 | ~ (t2tb1(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & % 36.69/5.76 | eq_prefix1(int, all_144_1, v2, n1) = v3 & get(all_102_18, int, % 36.69/5.76 | all_102_7, v1) = v2 & uni(v2))) | (all_144_0 = 0 & all_102_5 = % 36.69/5.76 | 0)) % 36.69/5.76 | % 36.69/5.76 | ALPHA: (71) implies: % 36.69/5.76 | (72) uni(all_144_1) % 36.69/5.76 | (73) eq_prefix1(int, all_102_8, all_144_1, 0) = all_144_0 % 36.69/5.76 | (74) t2tb2(all_102_6) = all_144_1 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (21) with all_134_3, all_136_1, all_102_14, int, % 36.69/5.76 | simplifying with (64), (68) gives: % 36.69/5.76 | (75) all_136_1 = all_134_3 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (21) with all_132_3, all_136_1, all_102_14, int, % 36.69/5.76 | simplifying with (60), (68) gives: % 36.69/5.76 | (76) all_136_1 = all_132_3 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (21) with all_130_1, all_136_1, all_102_14, int, % 36.69/5.76 | simplifying with (57), (68) gives: % 36.69/5.76 | (77) all_136_1 = all_130_1 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (18) with all_130_0, all_132_2, all_102_15, % 36.69/5.76 | simplifying with (58), (61) gives: % 36.69/5.76 | (78) all_132_2 = all_130_0 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (19) with all_134_2, all_136_0, all_102_15, % 36.69/5.76 | simplifying with (66), (69) gives: % 36.69/5.76 | (79) all_136_0 = all_134_2 % 36.69/5.76 | % 36.69/5.76 | GROUND_INST: instantiating (20) with all_102_4, all_144_1, all_102_6, % 36.69/5.76 | simplifying with (40), (74) gives: % 36.69/5.76 | (80) all_144_1 = all_102_4 % 36.69/5.76 | % 36.69/5.76 | COMBINE_EQS: (75), (77) imply: % 36.69/5.76 | (81) all_134_3 = all_130_1 % 36.69/5.76 | % 36.69/5.76 | COMBINE_EQS: (75), (76) imply: % 36.69/5.76 | (82) all_134_3 = all_132_3 % 36.69/5.76 | % 36.69/5.76 | COMBINE_EQS: (81), (82) imply: % 36.69/5.76 | (83) all_132_3 = all_130_1 % 36.69/5.76 | % 36.69/5.76 | SIMP: (83) implies: % 36.69/5.76 | (84) all_132_3 = all_130_1 % 36.69/5.76 | % 36.69/5.76 | REDUCE: (73), (80) imply: % 36.69/5.76 | (85) eq_prefix1(int, all_102_8, all_102_4, 0) = all_144_0 % 36.69/5.76 | % 36.69/5.76 | REDUCE: (72), (80) imply: % 36.69/5.76 | (86) uni(all_102_4) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (45) with all_134_2, all_134_1, simplifying with % 37.10/5.76 | (65) gives: % 37.10/5.76 | (87) ~ ($lesseq(0, all_134_2)) | ? [v0: int] : ( ~ (v0 = 0) & mem(int, % 37.10/5.76 | all_134_1, all_102_19) = v0) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (3) with all_102_15, all_130_0, simplifying with % 37.10/5.76 | (32), (58) gives: % 37.10/5.76 | (88) ? [v0: uni] : ? [v1: any] : ? [v2: uni] : ? [v3: any] : % 37.10/5.76 | (t2tb1(all_130_0) = v2 & t2tb(all_102_15) = v0 & is_empty(int, v0) = % 37.10/5.76 | v1 & mem(int, v2, v0) = v3 & uni(v2) & uni(v0) & (v3 = 0 | v1 = 0)) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (5) with all_102_15, all_130_0, simplifying with % 37.10/5.76 | (32), (58) gives: % 37.10/5.76 | (89) ? [v0: uni] : ? [v1: any] : (t2tb(all_102_15) = v0 & is_empty(int, % 37.10/5.76 | v0) = v1 & uni(v0) & (v1 = 0 | ! [v2: int] : ! [v3: uni] : ( ~ % 37.10/5.76 | ($lesseq(1, $difference(all_130_0, v2))) | ~ (t2tb1(v2) = v3) | % 37.10/5.76 | ? [v4: int] : ( ~ (v4 = 0) & mem(int, v3, v0) = v4)))) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (7) with all_102_15, all_134_2, simplifying with % 37.10/5.76 | (32), (66) gives: % 37.10/5.76 | (90) ? [v0: uni] : ? [v1: any] : ? [v2: uni] : ? [v3: any] : % 37.10/5.76 | (t2tb1(all_134_2) = v2 & t2tb(all_102_15) = v0 & is_empty(int, v0) = % 37.10/5.76 | v1 & mem(int, v2, v0) = v3 & uni(v2) & uni(v0) & (v3 = 0 | v1 = 0)) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (9) with all_102_15, all_134_2, simplifying with % 37.10/5.76 | (32), (66) gives: % 37.10/5.76 | (91) ? [v0: uni] : ? [v1: any] : (t2tb(all_102_15) = v0 & is_empty(int, % 37.10/5.76 | v0) = v1 & uni(v0) & (v1 = 0 | ! [v2: int] : ! [v3: uni] : ( ~ % 37.10/5.76 | ($lesseq(1, $difference(v2, all_134_2))) | ~ (t2tb1(v2) = v3) | % 37.10/5.76 | ? [v4: int] : ( ~ (v4 = 0) & mem(int, v3, v0) = v4)))) % 37.10/5.76 | % 37.10/5.76 | GROUND_INST: instantiating (11) with int, all_102_8, all_102_4, 0, all_144_0, % 37.10/5.76 | simplifying with (14), (31), (85), (86) gives: % 37.10/5.76 | (92) all_144_0 = 0 % 37.10/5.76 | % 37.10/5.76 | DELTA: instantiating (88) with fresh symbols all_180_0, all_180_1, all_180_2, % 37.10/5.76 | all_180_3 gives: % 37.10/5.76 | (93) t2tb1(all_130_0) = all_180_1 & t2tb(all_102_15) = all_180_3 & % 37.10/5.76 | is_empty(int, all_180_3) = all_180_2 & mem(int, all_180_1, all_180_3) % 37.10/5.76 | = all_180_0 & uni(all_180_1) & uni(all_180_3) & (all_180_0 = 0 | % 37.10/5.76 | all_180_2 = 0) % 37.10/5.76 | % 37.10/5.76 | ALPHA: (93) implies: % 37.10/5.76 | (94) is_empty(int, all_180_3) = all_180_2 % 37.10/5.76 | (95) t2tb(all_102_15) = all_180_3 % 37.10/5.76 | % 37.10/5.76 | DELTA: instantiating (91) with fresh symbols all_182_0, all_182_1 gives: % 37.10/5.76 | (96) t2tb(all_102_15) = all_182_1 & is_empty(int, all_182_1) = all_182_0 & % 37.10/5.76 | uni(all_182_1) & (all_182_0 = 0 | ! [v0: int] : ! [v1: uni] : ( ~ % 37.10/5.76 | ($lesseq(1, $difference(v0, all_134_2))) | ~ (t2tb1(v0) = v1) | % 37.10/5.76 | ? [v2: int] : ( ~ (v2 = 0) & mem(int, v1, all_182_1) = v2))) % 37.10/5.77 | % 37.10/5.77 | ALPHA: (96) implies: % 37.10/5.77 | (97) is_empty(int, all_182_1) = all_182_0 % 37.10/5.77 | (98) t2tb(all_102_15) = all_182_1 % 37.10/5.77 | % 37.10/5.77 | DELTA: instantiating (90) with fresh symbols all_184_0, all_184_1, all_184_2, % 37.10/5.77 | all_184_3 gives: % 37.10/5.77 | (99) t2tb1(all_134_2) = all_184_1 & t2tb(all_102_15) = all_184_3 & % 37.10/5.77 | is_empty(int, all_184_3) = all_184_2 & mem(int, all_184_1, all_184_3) % 37.10/5.77 | = all_184_0 & uni(all_184_1) & uni(all_184_3) & (all_184_0 = 0 | % 37.10/5.77 | all_184_2 = 0) % 37.10/5.77 | % 37.10/5.77 | ALPHA: (99) implies: % 37.10/5.77 | (100) mem(int, all_184_1, all_184_3) = all_184_0 % 37.10/5.77 | (101) is_empty(int, all_184_3) = all_184_2 % 37.10/5.77 | (102) t2tb(all_102_15) = all_184_3 % 37.10/5.77 | (103) t2tb1(all_134_2) = all_184_1 % 37.10/5.77 | (104) all_184_0 = 0 | all_184_2 = 0 % 37.10/5.77 | % 37.10/5.77 | DELTA: instantiating (89) with fresh symbols all_186_0, all_186_1 gives: % 37.10/5.77 | (105) t2tb(all_102_15) = all_186_1 & is_empty(int, all_186_1) = all_186_0 & % 37.10/5.77 | uni(all_186_1) & (all_186_0 = 0 | ! [v0: int] : ! [v1: uni] : ( ~ % 37.10/5.77 | ($lesseq(1, $difference(all_130_0, v0))) | ~ (t2tb1(v0) = v1) | % 37.10/5.77 | ? [v2: int] : ( ~ (v2 = 0) & mem(int, v1, all_186_1) = v2))) % 37.10/5.77 | % 37.10/5.77 | ALPHA: (105) implies: % 37.10/5.77 | (106) is_empty(int, all_186_1) = all_186_0 % 37.10/5.77 | (107) t2tb(all_102_15) = all_186_1 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (85), (92) imply: % 37.10/5.77 | (108) eq_prefix1(int, all_102_8, all_102_4, 0) = 0 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (16) with all_102_14, all_184_3, all_102_15, % 37.10/5.77 | simplifying with (36), (102) gives: % 37.10/5.77 | (109) all_184_3 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (16) with all_182_1, all_184_3, all_102_15, % 37.10/5.77 | simplifying with (98), (102) gives: % 37.10/5.77 | (110) all_184_3 = all_182_1 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (16) with all_182_1, all_186_1, all_102_15, % 37.10/5.77 | simplifying with (98), (107) gives: % 37.10/5.77 | (111) all_186_1 = all_182_1 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (16) with all_180_3, all_186_1, all_102_15, % 37.10/5.77 | simplifying with (95), (107) gives: % 37.10/5.77 | (112) all_186_1 = all_180_3 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (17) with all_134_1, all_184_1, all_134_2, % 37.10/5.77 | simplifying with (65), (103) gives: % 37.10/5.77 | (113) all_184_1 = all_134_1 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (111), (112) imply: % 37.10/5.77 | (114) all_182_1 = all_180_3 % 37.10/5.77 | % 37.10/5.77 | SIMP: (114) implies: % 37.10/5.77 | (115) all_182_1 = all_180_3 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (109), (110) imply: % 37.10/5.77 | (116) all_182_1 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | SIMP: (116) implies: % 37.10/5.77 | (117) all_182_1 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (115), (117) imply: % 37.10/5.77 | (118) all_180_3 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | SIMP: (118) implies: % 37.10/5.77 | (119) all_180_3 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (112), (119) imply: % 37.10/5.77 | (120) all_186_1 = all_102_14 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (106), (120) imply: % 37.10/5.77 | (121) is_empty(int, all_102_14) = all_186_0 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (101), (109) imply: % 37.10/5.77 | (122) is_empty(int, all_102_14) = all_184_2 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (97), (117) imply: % 37.10/5.77 | (123) is_empty(int, all_102_14) = all_182_0 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (94), (119) imply: % 37.10/5.77 | (124) is_empty(int, all_102_14) = all_180_2 % 37.10/5.77 | % 37.10/5.77 | REDUCE: (100), (109), (113) imply: % 37.10/5.77 | (125) mem(int, all_134_1, all_102_14) = all_184_0 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (24) with all_134_0, all_184_0, all_102_14, % 37.10/5.77 | all_134_1, int, simplifying with (63), (125) gives: % 37.10/5.77 | (126) all_184_0 = all_134_0 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (21) with all_130_1, all_182_0, all_102_14, int, % 37.10/5.77 | simplifying with (57), (123) gives: % 37.10/5.77 | (127) all_182_0 = all_130_1 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (21) with all_182_0, all_184_2, all_102_14, int, % 37.10/5.77 | simplifying with (122), (123) gives: % 37.10/5.77 | (128) all_184_2 = all_182_0 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (21) with all_184_2, all_186_0, all_102_14, int, % 37.10/5.77 | simplifying with (121), (122) gives: % 37.10/5.77 | (129) all_186_0 = all_184_2 % 37.10/5.77 | % 37.10/5.77 | GROUND_INST: instantiating (21) with all_180_2, all_186_0, all_102_14, int, % 37.10/5.77 | simplifying with (121), (124) gives: % 37.10/5.77 | (130) all_186_0 = all_180_2 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (129), (130) imply: % 37.10/5.77 | (131) all_184_2 = all_180_2 % 37.10/5.77 | % 37.10/5.77 | SIMP: (131) implies: % 37.10/5.77 | (132) all_184_2 = all_180_2 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (128), (132) imply: % 37.10/5.77 | (133) all_182_0 = all_180_2 % 37.10/5.77 | % 37.10/5.77 | SIMP: (133) implies: % 37.10/5.77 | (134) all_182_0 = all_180_2 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (127), (134) imply: % 37.10/5.77 | (135) all_180_2 = all_130_1 % 37.10/5.77 | % 37.10/5.77 | SIMP: (135) implies: % 37.10/5.77 | (136) all_180_2 = all_130_1 % 37.10/5.77 | % 37.10/5.77 | COMBINE_EQS: (132), (136) imply: % 37.10/5.77 | (137) all_184_2 = all_130_1 % 37.10/5.77 | % 37.10/5.77 | BETA: splitting (42) gives: % 37.10/5.77 | % 37.10/5.77 | Case 1: % 37.10/5.77 | | % 37.10/5.77 | | (138) all_102_0 = 0 & ~ (all_102_5 = 0) & $lesseq(1, % 37.10/5.77 | | $difference(all_102_11, all_102_3)) & $lesseq(0, all_102_3) & % 37.10/5.77 | | eq_prefix1(int, all_102_4, all_102_1, n1) = 0 & get(all_102_18, % 37.10/5.77 | | int, all_102_7, all_102_2) = all_102_1 & t2tb1(all_102_3) = % 37.10/5.77 | | all_102_2 & uni(all_102_1) & uni(all_102_2) % 37.10/5.77 | | % 37.10/5.77 | | ALPHA: (138) implies: % 37.10/5.77 | | (139) ~ (all_102_5 = 0) % 37.10/5.77 | | (140) $lesseq(0, all_102_3) % 37.10/5.77 | | (141) $lesseq(1, $difference(all_102_11, all_102_3)) % 37.10/5.77 | | (142) t2tb1(all_102_3) = all_102_2 % 37.10/5.77 | | (143) get(all_102_18, int, all_102_7, all_102_2) = all_102_1 % 37.10/5.77 | | (144) eq_prefix1(int, all_102_4, all_102_1, n1) = 0 % 37.10/5.77 | | % 37.10/5.77 | | REDUCE: (47), (143) imply: % 37.10/5.77 | | (145) get(all_87_0, int, all_102_7, all_102_2) = all_102_1 % 37.10/5.77 | | % 37.10/5.77 | | BETA: splitting (55) gives: % 37.10/5.77 | | % 37.10/5.77 | | Case 1: % 37.10/5.77 | | | % 37.10/5.77 | | | (146) all_102_5 = 0 % 37.10/5.77 | | | % 37.10/5.77 | | | REDUCE: (139), (146) imply: % 37.10/5.77 | | | (147) $false % 37.10/5.78 | | | % 37.10/5.78 | | | CLOSE: (147) is inconsistent. % 37.10/5.78 | | | % 37.10/5.78 | | Case 2: % 37.10/5.78 | | | % 37.10/5.78 | | | (148) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: uni] : ? % 37.10/5.78 | | | [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 37.10/5.78 | | | int] : ($lesseq(1, $difference(n1, v1)) & $lesseq(0, v1) & % 37.10/5.78 | | | t2tb2(all_102_6) = v0 & get(int, int, v0, v2) = v3 & tb2t1(v3) % 37.10/5.78 | | | = v4 & t2tb1(v1) = v2 & uni(v3) & uni(v2) & uni(v0) & ( ~ % 37.10/5.78 | | | ($lesseq(1, $difference(n1, v4))) | ~ ($lesseq(0, v4)) | % 37.10/5.78 | | | ($lesseq(1, $difference(v1, v5)) & $lesseq(0, v5) & get(int, % 37.10/5.78 | | | int, v0, v6) = v7 & tb2t1(v7) = v8 & t2tb1(v5) = v6 & % 37.10/5.78 | | | uni(v7) & uni(v6) & ($sum($difference($difference(v8, v5), % 37.10/5.78 | | | v4), v1) = 0 | $difference($sum(v8, v5), v4) = v1 | % 37.10/5.78 | | | v8 = v4)))) % 37.10/5.78 | | | % 37.10/5.78 | | | DELTA: instantiating (148) with fresh symbols all_295_0, all_295_1, % 37.10/5.78 | | | all_295_2, all_295_3, all_295_4, all_295_5, all_295_6, all_295_7, % 37.10/5.78 | | | all_295_8 gives: % 37.10/5.78 | | | (149) $lesseq(1, $difference(n1, all_295_7)) & $lesseq(0, all_295_7) & % 37.10/5.78 | | | t2tb2(all_102_6) = all_295_8 & get(int, int, all_295_8, % 37.10/5.78 | | | all_295_6) = all_295_5 & tb2t1(all_295_5) = all_295_4 & % 37.10/5.78 | | | t2tb1(all_295_7) = all_295_6 & uni(all_295_5) & uni(all_295_6) & % 37.10/5.78 | | | uni(all_295_8) & ( ~ ($lesseq(1, $difference(n1, all_295_4))) | % 37.10/5.78 | | | ~ ($lesseq(0, all_295_4)) | ($lesseq(1, $difference(all_295_7, % 37.10/5.78 | | | all_295_3)) & $lesseq(0, all_295_3) & get(int, int, % 37.10/5.78 | | | all_295_8, all_295_2) = all_295_1 & tb2t1(all_295_1) = % 37.10/5.78 | | | all_295_0 & t2tb1(all_295_3) = all_295_2 & uni(all_295_1) & % 37.10/5.78 | | | uni(all_295_2) & ($sum($difference($difference(all_295_0, % 37.10/5.78 | | | all_295_3), all_295_4), all_295_7) = 0 | % 37.10/5.78 | | | $difference($sum(all_295_0, all_295_3), all_295_4) = % 37.10/5.78 | | | all_295_7 | all_295_0 = all_295_4))) % 37.10/5.78 | | | % 37.10/5.78 | | | ALPHA: (149) implies: % 37.10/5.78 | | | (150) $lesseq(0, all_295_7) % 37.10/5.78 | | | (151) $lesseq(1, $difference(n1, all_295_7)) % 37.10/5.78 | | | (152) t2tb2(all_102_6) = all_295_8 % 37.10/5.78 | | | % 37.10/5.78 | | | BETA: splitting (48) gives: % 37.10/5.78 | | | % 37.10/5.78 | | | Case 1: % 37.10/5.78 | | | | % 37.10/5.78 | | | | (153) n1 = 0 % 37.10/5.78 | | | | % 37.10/5.78 | | | | REDUCE: (151), (153) imply: % 37.10/5.78 | | | | (154) $lesseq(all_295_7, -1) % 37.10/5.78 | | | | % 37.10/5.78 | | | | COMBINE_INEQS: (150), (154) imply: % 37.10/5.78 | | | | (155) $false % 37.10/5.78 | | | | % 37.10/5.78 | | | | CLOSE: (155) is inconsistent. % 37.10/5.78 | | | | % 37.10/5.78 | | | Case 2: % 37.10/5.78 | | | | % 37.10/5.78 | | | | (156) ? [v0: int] : ( ~ (v0 = 0) & is_empty(int, all_102_14) = v0) % 37.10/5.78 | | | | % 37.10/5.78 | | | | DELTA: instantiating (156) with fresh symbol all_303_0 gives: % 37.10/5.78 | | | | (157) ~ (all_303_0 = 0) & is_empty(int, all_102_14) = all_303_0 % 37.10/5.78 | | | | % 37.10/5.78 | | | | ALPHA: (157) implies: % 37.10/5.78 | | | | (158) ~ (all_303_0 = 0) % 37.19/5.78 | | | | (159) is_empty(int, all_102_14) = all_303_0 % 37.19/5.78 | | | | % 37.19/5.78 | | | | GROUND_INST: instantiating (21) with all_130_1, all_303_0, all_102_14, % 37.19/5.78 | | | | int, simplifying with (57), (159) gives: % 37.19/5.78 | | | | (160) all_303_0 = all_130_1 % 37.19/5.78 | | | | % 37.19/5.78 | | | | GROUND_INST: instantiating (20) with all_102_4, all_295_8, all_102_6, % 37.19/5.78 | | | | simplifying with (40), (152) gives: % 37.19/5.78 | | | | (161) all_295_8 = all_102_4 % 37.19/5.78 | | | | % 37.19/5.78 | | | | REDUCE: (158), (160) imply: % 37.19/5.78 | | | | (162) ~ (all_130_1 = 0) % 37.19/5.78 | | | | % 37.19/5.78 | | | | BETA: splitting (104) gives: % 37.19/5.78 | | | | % 37.19/5.78 | | | | Case 1: % 37.19/5.78 | | | | | % 37.19/5.78 | | | | | (163) all_184_0 = 0 % 37.19/5.78 | | | | | % 37.19/5.78 | | | | | COMBINE_EQS: (126), (163) imply: % 37.19/5.78 | | | | | (164) all_134_0 = 0 % 37.19/5.78 | | | | | % 37.19/5.78 | | | | | REDUCE: (63), (164) imply: % 37.19/5.78 | | | | | (165) mem(int, all_134_1, all_102_14) = 0 % 37.19/5.78 | | | | | % 37.19/5.78 | | | | | BETA: splitting (87) gives: % 37.19/5.78 | | | | | % 37.19/5.78 | | | | | Case 1: % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | (166) $lesseq(all_134_2, -1) % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | GROUND_INST: instantiating (10) with all_134_2, n1, all_134_1, % 37.19/5.78 | | | | | | all_102_15, all_102_14, simplifying with (36), (37), % 37.19/5.78 | | | | | | (65), (165) gives: % 37.19/5.78 | | | | | | (167) $lesseq(0, all_134_2) % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | COMBINE_INEQS: (166), (167) imply: % 37.19/5.78 | | | | | | (168) $false % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | CLOSE: (168) is inconsistent. % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | Case 2: % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | GROUND_INST: instantiating (46) with all_102_6, all_102_4, % 37.19/5.78 | | | | | | all_102_3, all_102_2, simplifying with (34), (40), % 37.19/5.78 | | | | | | (142) gives: % 37.19/5.78 | | | | | | (169) ~ ($lesseq(1, $difference(all_102_11, all_102_3))) | ~ % 37.19/5.78 | | | | | | ($lesseq(0, all_102_3)) | ? [v0: any] : ? [v1: int] : % 37.19/5.78 | | | | | | ((v1 = 0 & v0 = 0 & partial_solution1(n1, all_102_6) = 0 & % 37.19/5.78 | | | | | | eq_prefix1(int, all_102_8, all_102_4, 0) = 0) | ( ~ (v1 % 37.19/5.78 | | | | | | = 0) & eq_prefix1(int, all_102_4, v0, n1) = v1 & % 37.19/5.78 | | | | | | get(all_102_18, int, all_102_7, all_102_2) = v0 & % 37.19/5.78 | | | | | | uni(v0))) % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | GROUND_INST: instantiating (46) with all_102_9, all_102_8, % 37.19/5.78 | | | | | | all_102_3, all_102_2, simplifying with (33), (39), % 37.19/5.78 | | | | | | (142) gives: % 37.19/5.78 | | | | | | (170) ~ ($lesseq(1, $difference(all_102_11, all_102_3))) | ~ % 37.19/5.78 | | | | | | ($lesseq(0, all_102_3)) | ? [v0: any] : ? [v1: int] : % 37.19/5.78 | | | | | | ((v1 = 0 & v0 = 0 & partial_solution1(n1, all_102_9) = 0 & % 37.19/5.78 | | | | | | eq_prefix1(int, all_102_8, all_102_8, 0) = 0) | ( ~ (v1 % 37.19/5.78 | | | | | | = 0) & eq_prefix1(int, all_102_8, v0, n1) = v1 & % 37.19/5.78 | | | | | | get(all_102_18, int, all_102_7, all_102_2) = v0 & % 37.19/5.78 | | | | | | uni(v0))) % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | BETA: splitting (169) gives: % 37.19/5.78 | | | | | | % 37.19/5.78 | | | | | | Case 1: % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | (171) $lesseq(all_102_3, -1) % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | COMBINE_INEQS: (140), (171) imply: % 37.19/5.78 | | | | | | | (172) $false % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | CLOSE: (172) is inconsistent. % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | Case 2: % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | (173) ~ ($lesseq(1, $difference(all_102_11, all_102_3))) | ? % 37.19/5.78 | | | | | | | [v0: any] : ? [v1: int] : ((v1 = 0 & v0 = 0 & % 37.19/5.78 | | | | | | | partial_solution1(n1, all_102_6) = 0 & % 37.19/5.78 | | | | | | | eq_prefix1(int, all_102_8, all_102_4, 0) = 0) | ( ~ % 37.19/5.78 | | | | | | | (v1 = 0) & eq_prefix1(int, all_102_4, v0, n1) = v1 & % 37.19/5.78 | | | | | | | get(all_102_18, int, all_102_7, all_102_2) = v0 & % 37.19/5.78 | | | | | | | uni(v0))) % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | BETA: splitting (170) gives: % 37.19/5.78 | | | | | | | % 37.19/5.78 | | | | | | | Case 1: % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | (174) $lesseq(all_102_3, -1) % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | COMBINE_INEQS: (140), (174) imply: % 37.19/5.78 | | | | | | | | (175) $false % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | CLOSE: (175) is inconsistent. % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | Case 2: % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | (176) ~ ($lesseq(1, $difference(all_102_11, all_102_3))) | % 37.19/5.78 | | | | | | | | ? [v0: any] : ? [v1: int] : ((v1 = 0 & v0 = 0 & % 37.19/5.78 | | | | | | | | partial_solution1(n1, all_102_9) = 0 & % 37.19/5.78 | | | | | | | | eq_prefix1(int, all_102_8, all_102_8, 0) = 0) | ( ~ % 37.19/5.78 | | | | | | | | (v1 = 0) & eq_prefix1(int, all_102_8, v0, n1) = v1 % 37.19/5.78 | | | | | | | | & get(all_102_18, int, all_102_7, all_102_2) = v0 & % 37.19/5.78 | | | | | | | | uni(v0))) % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | BETA: splitting (173) gives: % 37.19/5.78 | | | | | | | | % 37.19/5.78 | | | | | | | | Case 1: % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | | (177) $lesseq(all_102_11, all_102_3) % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | | COMBINE_INEQS: (141), (177) imply: % 37.19/5.78 | | | | | | | | | (178) $false % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | | CLOSE: (178) is inconsistent. % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | Case 2: % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | | (179) ? [v0: any] : ? [v1: int] : ((v1 = 0 & v0 = 0 & % 37.19/5.78 | | | | | | | | | partial_solution1(n1, all_102_6) = 0 & % 37.19/5.78 | | | | | | | | | eq_prefix1(int, all_102_8, all_102_4, 0) = 0) | ( % 37.19/5.78 | | | | | | | | | ~ (v1 = 0) & eq_prefix1(int, all_102_4, v0, n1) = % 37.19/5.78 | | | | | | | | | v1 & get(all_102_18, int, all_102_7, all_102_2) = % 37.19/5.78 | | | | | | | | | v0 & uni(v0))) % 37.19/5.78 | | | | | | | | | % 37.19/5.78 | | | | | | | | | DELTA: instantiating (179) with fresh symbols all_579_0, % 37.19/5.78 | | | | | | | | | all_579_1 gives: % 37.19/5.78 | | | | | | | | | (180) (all_579_0 = 0 & all_579_1 = 0 & % 37.19/5.78 | | | | | | | | | partial_solution1(n1, all_102_6) = 0 & % 37.19/5.78 | | | | | | | | | eq_prefix1(int, all_102_8, all_102_4, 0) = 0) | ( ~ % 37.19/5.78 | | | | | | | | | (all_579_0 = 0) & eq_prefix1(int, all_102_4, % 37.19/5.78 | | | | | | | | | all_579_1, n1) = all_579_0 & get(all_102_18, int, % 37.19/5.78 | | | | | | | | | all_102_7, all_102_2) = all_579_1 & % 37.19/5.78 | | | | | | | | | uni(all_579_1)) % 37.19/5.78 | | | | | | | | | % 37.19/5.79 | | | | | | | | | BETA: splitting (180) gives: % 37.19/5.79 | | | | | | | | | % 37.19/5.79 | | | | | | | | | Case 1: % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | (181) all_579_0 = 0 & all_579_1 = 0 & % 37.19/5.79 | | | | | | | | | | partial_solution1(n1, all_102_6) = 0 & % 37.19/5.79 | | | | | | | | | | eq_prefix1(int, all_102_8, all_102_4, 0) = 0 % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | ALPHA: (181) implies: % 37.19/5.79 | | | | | | | | | | (182) partial_solution1(n1, all_102_6) = 0 % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | GROUND_INST: instantiating (23) with all_102_5, 0, all_102_6, % 37.19/5.79 | | | | | | | | | | n1, simplifying with (41), (182) gives: % 37.19/5.79 | | | | | | | | | | (183) all_102_5 = 0 % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | REDUCE: (139), (183) imply: % 37.19/5.79 | | | | | | | | | | (184) $false % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | CLOSE: (184) is inconsistent. % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | Case 2: % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | (185) ~ (all_579_0 = 0) & eq_prefix1(int, all_102_4, % 37.19/5.79 | | | | | | | | | | all_579_1, n1) = all_579_0 & get(all_102_18, int, % 37.19/5.79 | | | | | | | | | | all_102_7, all_102_2) = all_579_1 & % 37.19/5.79 | | | | | | | | | | uni(all_579_1) % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | ALPHA: (185) implies: % 37.19/5.79 | | | | | | | | | | (186) ~ (all_579_0 = 0) % 37.19/5.79 | | | | | | | | | | (187) get(all_102_18, int, all_102_7, all_102_2) = % 37.19/5.79 | | | | | | | | | | all_579_1 % 37.19/5.79 | | | | | | | | | | (188) eq_prefix1(int, all_102_4, all_579_1, n1) = % 37.19/5.79 | | | | | | | | | | all_579_0 % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | REDUCE: (47), (187) imply: % 37.19/5.79 | | | | | | | | | | (189) get(all_87_0, int, all_102_7, all_102_2) = % 37.19/5.79 | | | | | | | | | | all_579_1 % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | BETA: splitting (176) gives: % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | Case 1: % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | (190) $lesseq(all_102_11, all_102_3) % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | COMBINE_INEQS: (141), (190) imply: % 37.19/5.79 | | | | | | | | | | | (191) $false % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | CLOSE: (191) is inconsistent. % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | Case 2: % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | GROUND_INST: instantiating (25) with all_102_1, all_579_1, % 37.19/5.79 | | | | | | | | | | | all_102_2, all_102_7, int, all_87_0, simplifying % 37.19/5.79 | | | | | | | | | | | with (145), (189) gives: % 37.19/5.79 | | | | | | | | | | | (192) all_579_1 = all_102_1 % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | REDUCE: (188), (192) imply: % 37.19/5.79 | | | | | | | | | | | (193) eq_prefix1(int, all_102_4, all_102_1, n1) = % 37.19/5.79 | | | | | | | | | | | all_579_0 % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | GROUND_INST: instantiating (26) with 0, all_579_0, n1, % 37.19/5.79 | | | | | | | | | | | all_102_1, all_102_4, int, simplifying with (144), % 37.19/5.79 | | | | | | | | | | | (193) gives: % 37.19/5.79 | | | | | | | | | | | (194) all_579_0 = 0 % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | REDUCE: (186), (194) imply: % 37.19/5.79 | | | | | | | | | | | (195) $false % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | | CLOSE: (195) is inconsistent. % 37.19/5.79 | | | | | | | | | | | % 37.19/5.79 | | | | | | | | | | End of split % 37.19/5.79 | | | | | | | | | | % 37.19/5.79 | | | | | | | | | End of split % 37.19/5.79 | | | | | | | | | % 37.19/5.79 | | | | | | | | End of split % 37.19/5.79 | | | | | | | | % 37.19/5.79 | | | | | | | End of split % 37.19/5.79 | | | | | | | % 37.19/5.79 | | | | | | End of split % 37.19/5.79 | | | | | | % 37.19/5.79 | | | | | End of split % 37.19/5.79 | | | | | % 37.19/5.79 | | | | Case 2: % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | (196) all_184_2 = 0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | COMBINE_EQS: (137), (196) imply: % 37.19/5.79 | | | | | (197) all_130_1 = 0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | SIMP: (197) implies: % 37.19/5.79 | | | | | (198) all_130_1 = 0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | REDUCE: (162), (198) imply: % 37.19/5.79 | | | | | (199) $false % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | CLOSE: (199) is inconsistent. % 37.19/5.79 | | | | | % 37.19/5.79 | | | | End of split % 37.19/5.79 | | | | % 37.19/5.79 | | | End of split % 37.19/5.79 | | | % 37.19/5.79 | | End of split % 37.19/5.79 | | % 37.19/5.79 | Case 2: % 37.19/5.79 | | % 37.19/5.79 | | (200) all_102_5 = 0 & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 37.19/5.79 | | $difference(all_102_11, v0))) | ~ ($lesseq(0, v0)) | ~ % 37.19/5.79 | | (t2tb1(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & % 37.19/5.79 | | eq_prefix1(int, all_102_4, v2, n1) = v3 & get(all_102_18, int, % 37.19/5.79 | | all_102_7, v1) = v2 & uni(v2))) % 37.19/5.79 | | % 37.19/5.79 | | ALPHA: (200) implies: % 37.19/5.79 | | (201) all_102_5 = 0 % 37.19/5.79 | | (202) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 37.19/5.79 | | $difference(all_102_11, v0))) | ~ ($lesseq(0, v0)) | ~ % 37.19/5.79 | | (t2tb1(v0) = v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & % 37.19/5.79 | | eq_prefix1(int, all_102_4, v2, n1) = v3 & get(all_102_18, int, % 37.19/5.79 | | all_102_7, v1) = v2 & uni(v2))) % 37.19/5.79 | | % 37.19/5.79 | | REDUCE: (41), (201) imply: % 37.19/5.79 | | (203) partial_solution1(n1, all_102_6) = 0 % 37.19/5.79 | | % 37.19/5.79 | | BETA: splitting (70) gives: % 37.19/5.79 | | % 37.19/5.79 | | Case 1: % 37.19/5.79 | | | % 37.19/5.79 | | | (204) all_143_0 = 0 & $lesseq(1, $difference(all_102_11, all_143_3)) & % 37.19/5.79 | | | $lesseq(0, all_143_3) & eq_prefix1(int, all_102_4, all_143_1, n1) % 37.19/5.79 | | | = 0 & get(all_102_18, int, all_102_7, all_143_2) = all_143_1 & % 37.19/5.79 | | | t2tb1(all_143_3) = all_143_2 & uni(all_143_1) & uni(all_143_2) % 37.19/5.79 | | | % 37.19/5.79 | | | ALPHA: (204) implies: % 37.19/5.79 | | | (205) $lesseq(0, all_143_3) % 37.19/5.79 | | | (206) $lesseq(1, $difference(all_102_11, all_143_3)) % 37.19/5.79 | | | (207) t2tb1(all_143_3) = all_143_2 % 37.19/5.79 | | | (208) get(all_102_18, int, all_102_7, all_143_2) = all_143_1 % 37.19/5.79 | | | (209) eq_prefix1(int, all_102_4, all_143_1, n1) = 0 % 37.19/5.79 | | | % 37.19/5.79 | | | REDUCE: (47), (208) imply: % 37.19/5.79 | | | (210) get(all_87_0, int, all_102_7, all_143_2) = all_143_1 % 37.19/5.79 | | | % 37.19/5.79 | | | GROUND_INST: instantiating (202) with all_143_3, all_143_2, simplifying % 37.19/5.79 | | | with (207) gives: % 37.19/5.79 | | | (211) ~ ($lesseq(1, $difference(all_102_11, all_143_3))) | ~ % 37.19/5.79 | | | ($lesseq(0, all_143_3)) | ? [v0: uni] : ? [v1: int] : ( ~ (v1 = % 37.19/5.79 | | | 0) & eq_prefix1(int, all_102_4, v0, n1) = v1 & % 37.19/5.79 | | | get(all_102_18, int, all_102_7, all_143_2) = v0 & uni(v0)) % 37.19/5.79 | | | % 37.19/5.79 | | | BETA: splitting (211) gives: % 37.19/5.79 | | | % 37.19/5.79 | | | Case 1: % 37.19/5.79 | | | | % 37.19/5.79 | | | | (212) $lesseq(all_143_3, -1) % 37.19/5.79 | | | | % 37.19/5.79 | | | | COMBINE_INEQS: (205), (212) imply: % 37.19/5.79 | | | | (213) $false % 37.19/5.79 | | | | % 37.19/5.79 | | | | CLOSE: (213) is inconsistent. % 37.19/5.79 | | | | % 37.19/5.79 | | | Case 2: % 37.19/5.79 | | | | % 37.19/5.79 | | | | (214) ~ ($lesseq(1, $difference(all_102_11, all_143_3))) | ? [v0: % 37.19/5.79 | | | | uni] : ? [v1: int] : ( ~ (v1 = 0) & eq_prefix1(int, % 37.19/5.79 | | | | all_102_4, v0, n1) = v1 & get(all_102_18, int, all_102_7, % 37.19/5.79 | | | | all_143_2) = v0 & uni(v0)) % 37.19/5.79 | | | | % 37.19/5.79 | | | | BETA: splitting (214) gives: % 37.19/5.79 | | | | % 37.19/5.79 | | | | Case 1: % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | (215) $lesseq(all_102_11, all_143_3) % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | COMBINE_INEQS: (206), (215) imply: % 37.19/5.79 | | | | | (216) $false % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | CLOSE: (216) is inconsistent. % 37.19/5.79 | | | | | % 37.19/5.79 | | | | Case 2: % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | (217) ? [v0: uni] : ? [v1: int] : ( ~ (v1 = 0) & eq_prefix1(int, % 37.19/5.79 | | | | | all_102_4, v0, n1) = v1 & get(all_102_18, int, all_102_7, % 37.19/5.79 | | | | | all_143_2) = v0 & uni(v0)) % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | DELTA: instantiating (217) with fresh symbols all_376_0, all_376_1 % 37.19/5.79 | | | | | gives: % 37.19/5.79 | | | | | (218) ~ (all_376_0 = 0) & eq_prefix1(int, all_102_4, all_376_1, % 37.19/5.79 | | | | | n1) = all_376_0 & get(all_102_18, int, all_102_7, % 37.19/5.79 | | | | | all_143_2) = all_376_1 & uni(all_376_1) % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | ALPHA: (218) implies: % 37.19/5.79 | | | | | (219) ~ (all_376_0 = 0) % 37.19/5.79 | | | | | (220) get(all_102_18, int, all_102_7, all_143_2) = all_376_1 % 37.19/5.79 | | | | | (221) eq_prefix1(int, all_102_4, all_376_1, n1) = all_376_0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | REDUCE: (47), (220) imply: % 37.19/5.79 | | | | | (222) get(all_87_0, int, all_102_7, all_143_2) = all_376_1 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | GROUND_INST: instantiating (25) with all_143_1, all_376_1, all_143_2, % 37.19/5.79 | | | | | all_102_7, int, all_87_0, simplifying with (210), (222) % 37.19/5.79 | | | | | gives: % 37.19/5.79 | | | | | (223) all_376_1 = all_143_1 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | REDUCE: (221), (223) imply: % 37.19/5.79 | | | | | (224) eq_prefix1(int, all_102_4, all_143_1, n1) = all_376_0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | GROUND_INST: instantiating (26) with 0, all_376_0, n1, all_143_1, % 37.19/5.79 | | | | | all_102_4, int, simplifying with (209), (224) gives: % 37.19/5.79 | | | | | (225) all_376_0 = 0 % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | REDUCE: (219), (225) imply: % 37.19/5.79 | | | | | (226) $false % 37.19/5.79 | | | | | % 37.19/5.79 | | | | | CLOSE: (226) is inconsistent. % 37.19/5.79 | | | | | % 37.19/5.79 | | | | End of split % 37.19/5.79 | | | | % 37.19/5.79 | | | End of split % 37.19/5.79 | | | % 37.19/5.79 | | Case 2: % 37.19/5.79 | | | % 37.19/5.79 | | | (227) partial_solution1(n1, all_102_6) = all_143_3 & eq_prefix1(int, % 37.19/5.79 | | | all_102_8, all_102_4, 0) = all_143_2 & ( ~ (all_143_2 = 0) | ~ % 37.19/5.79 | | | (all_143_3 = 0)) % 37.19/5.79 | | | % 37.19/5.79 | | | ALPHA: (227) implies: % 37.19/5.79 | | | (228) eq_prefix1(int, all_102_8, all_102_4, 0) = all_143_2 % 37.19/5.79 | | | (229) partial_solution1(n1, all_102_6) = all_143_3 % 37.19/5.79 | | | (230) ~ (all_143_2 = 0) | ~ (all_143_3 = 0) % 37.19/5.79 | | | % 37.19/5.80 | | | GROUND_INST: instantiating (26) with 0, all_143_2, 0, all_102_4, % 37.19/5.80 | | | all_102_8, int, simplifying with (108), (228) gives: % 37.19/5.80 | | | (231) all_143_2 = 0 % 37.19/5.80 | | | % 37.19/5.80 | | | GROUND_INST: instantiating (23) with 0, all_143_3, all_102_6, n1, % 37.19/5.80 | | | simplifying with (203), (229) gives: % 37.19/5.80 | | | (232) all_143_3 = 0 % 37.19/5.80 | | | % 37.19/5.80 | | | BETA: splitting (230) gives: % 37.19/5.80 | | | % 37.19/5.80 | | | Case 1: % 37.19/5.80 | | | | % 37.19/5.80 | | | | (233) ~ (all_143_2 = 0) % 37.19/5.80 | | | | % 37.19/5.80 | | | | REDUCE: (231), (233) imply: % 37.19/5.80 | | | | (234) $false % 37.19/5.80 | | | | % 37.19/5.80 | | | | CLOSE: (234) is inconsistent. % 37.19/5.80 | | | | % 37.19/5.80 | | | Case 2: % 37.19/5.80 | | | | % 37.19/5.80 | | | | (235) ~ (all_143_3 = 0) % 37.19/5.80 | | | | % 37.19/5.80 | | | | REDUCE: (232), (235) imply: % 37.19/5.80 | | | | (236) $false % 37.19/5.80 | | | | % 37.19/5.80 | | | | CLOSE: (236) is inconsistent. % 37.19/5.80 | | | | % 37.19/5.80 | | | End of split % 37.19/5.80 | | | % 37.19/5.80 | | End of split % 37.19/5.80 | | % 37.19/5.80 | End of split % 37.19/5.80 | % 37.19/5.80 End of proof % 37.19/5.80 % SZS output end Proof for theBenchmark % 37.19/5.80 % 37.19/5.80 5199ms %------------------------------------------------------------------------------