%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW670_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 : n025.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:05 EDT 2023 % Result : Theorem 67.72s 9.88s % Output : Proof 68.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.19 % Problem : SWW670_2 : TPTP v8.1.2. Released v6.1.0. % 0.10/0.19 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.39 % Computer : n025.cluster.edu % 0.14/0.39 % Model : x86_64 x86_64 % 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.39 % Memory : 8042.1875MB % 0.14/0.39 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.39 % CPULimit : 300 % 0.14/0.39 % WCLimit : 300 % 0.14/0.39 % DateTime : Sun Aug 27 20:34:09 EDT 2023 % 0.14/0.39 % CPUTime : % 0.19/0.64 ________ _____ % 0.19/0.64 ___ __ \_________(_)________________________________ % 0.19/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.64 % 0.19/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.64 (2023-06-19) % 0.19/0.64 % 0.19/0.64 (c) Philipp Rümmer, 2009-2023 % 0.19/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.64 Amanda Stjerna. % 0.19/0.64 Free software under BSD-3-Clause. % 0.19/0.64 % 0.19/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.64 % 0.19/0.64 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.65 Running up to 7 provers in parallel. % 0.19/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.83/1.31 Prover 4: Preprocessing ... % 3.83/1.31 Prover 1: Preprocessing ... % 3.83/1.31 Prover 3: Preprocessing ... % 3.83/1.31 Prover 5: Preprocessing ... % 3.83/1.31 Prover 0: Preprocessing ... % 3.83/1.31 Prover 6: Preprocessing ... % 3.83/1.32 Prover 2: Preprocessing ... % 9.72/2.30 Prover 1: Warning: ignoring some quantifiers % 9.72/2.36 Prover 3: Warning: ignoring some quantifiers % 9.72/2.39 Prover 1: Constructing countermodel ... % 9.72/2.40 Prover 3: Constructing countermodel ... % 10.35/2.40 Prover 6: Proving ... % 10.35/2.41 Prover 4: Warning: ignoring some quantifiers % 10.35/2.44 Prover 5: Proving ... % 10.35/2.47 Prover 4: Constructing countermodel ... % 12.84/2.55 Prover 0: Proving ... % 14.04/2.72 Prover 2: Proving ... % 16.27/3.20 Prover 3: gave up % 16.27/3.21 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 16.91/3.33 Prover 7: Preprocessing ... % 20.27/3.62 Prover 7: Warning: ignoring some quantifiers % 21.13/3.68 Prover 7: Constructing countermodel ... % 24.30/4.15 Prover 1: gave up % 24.30/4.15 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 24.79/4.23 Prover 8: Preprocessing ... % 25.98/4.40 Prover 8: Warning: ignoring some quantifiers % 26.63/4.44 Prover 8: Constructing countermodel ... % 33.09/5.47 Prover 8: gave up % 33.09/5.49 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 34.86/5.56 Prover 9: Preprocessing ... % 36.47/5.81 Prover 9: Warning: ignoring some quantifiers % 37.09/5.82 Prover 9: Constructing countermodel ... % 44.15/6.90 Prover 7: gave up % 44.15/6.92 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 46.42/7.07 Prover 10: Preprocessing ... % 47.90/7.28 Prover 10: Warning: ignoring some quantifiers % 48.28/7.32 Prover 10: Constructing countermodel ... % 55.55/8.54 Prover 2: stopped % 55.55/8.56 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 58.62/8.69 Prover 11: Preprocessing ... % 60.80/8.93 Prover 11: Warning: ignoring some quantifiers % 60.89/8.95 Prover 11: Constructing countermodel ... % 67.72/9.87 Prover 4: Found proof (size 460) % 67.72/9.87 Prover 4: proved (9205ms) % 67.72/9.87 Prover 0: stopped % 67.72/9.87 Prover 6: stopped % 67.72/9.87 Prover 5: stopped % 67.72/9.87 Prover 9: stopped % 67.72/9.87 Prover 10: stopped % 67.72/9.88 Prover 11: stopped % 67.72/9.88 % 67.72/9.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.72/9.88 % 68.35/9.99 % SZS output start Proof for theBenchmark % 68.35/9.99 Assumptions after simplification: % 68.35/9.99 --------------------------------- % 68.35/10.00 % 68.35/10.00 (bridgeR) % 68.35/10.01 ! [v0: uni] : ! [v1: option_int] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | % 68.35/10.02 t2tb(v1) = v0) % 68.35/10.02 % 68.35/10.02 (bridgeR1) % 68.35/10.02 ! [v0: uni] : ! [v1: list_int] : ( ~ (tb2t1(v0) = v1) | ~ uni(v0) | % 68.35/10.02 t2tb1(v1) = v0) % 68.35/10.02 % 68.35/10.02 (cons_sort3) % 68.35/10.02 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 68.35/10.02 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: ty] : % 68.35/10.02 (list(v0) = v4 & sort1(v4, v3) = 0 & ty(v4))) % 68.35/10.02 % 68.35/10.02 (hd_def) % 68.35/10.02 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 68.35/10.02 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : (hd(v0, % 68.35/10.02 v3) = v4 & some(v0, v1) = v4 & uni(v4))) & ! [v0: ty] : ! [v1: uni] : % 68.35/10.02 ( ~ (none(v0) = v1) | ~ ty(v0) | ? [v2: uni] : (hd(v0, v2) = v1 & nil(v0) = % 68.35/10.02 v2 & uni(v2) & uni(v1))) & ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) % 68.35/10.02 | ~ ty(v0) | ? [v2: uni] : (hd(v0, v1) = v2 & none(v0) = v2 & uni(v2))) % 68.35/10.02 % 68.35/10.02 (length_def) % 68.35/10.03 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 68.35/10.03 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: int] : % 68.35/10.03 (length1(v0, v3) = v4 & length1(v0, v2) = $sum(v4, -1))) & ! [v0: ty] : ! % 68.35/10.03 [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | length1(v0, v1) = 0) % 68.35/10.03 % 68.35/10.03 (length_nil) % 68.35/10.03 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (length1(v0, v1) = % 68.35/10.03 v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : ( ~ (v3 = v1) & nil(v0) = v3 % 68.35/10.03 & uni(v3))) & ! [v0: ty] : ! [v1: uni] : ( ~ (length1(v0, v1) = 0) | ~ % 68.35/10.03 ty(v0) | ~ uni(v1) | nil(v0) = v1) % 68.35/10.03 % 68.35/10.03 (length_nonnegative) % 68.35/10.03 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ( ~ ($lesseq(v2, -1)) | ~ % 68.35/10.03 (length1(v0, v1) = v2) | ~ ty(v0) | ~ uni(v1)) % 68.35/10.03 % 68.35/10.03 (nil_Cons1) % 68.35/10.03 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 68.35/10.03 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : ( ~ (v4 % 68.35/10.03 = v3) & nil(v0) = v4 & uni(v4))) % 68.35/10.03 % 68.35/10.03 (nil_sort3) % 68.35/10.03 ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | ? [v2: ty] : % 68.35/10.03 (list(v0) = v2 & sort1(v2, v1) = 0 & ty(v2))) & ! [v0: ty] : ! [v1: ty] : % 68.35/10.03 ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: uni] : (nil(v0) = v2 & sort1(v1, v2) % 68.35/10.03 = 0 & uni(v2))) % 68.35/10.03 % 68.35/10.03 (no_zero_def) % 68.35/10.04 ty(int) & ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : (t2tb2(0) = v0 & % 68.35/10.04 tb2t(v1) = v2 & some(int, v0) = v1 & option_int(v2) & uni(v1) & uni(v0) & ! % 68.35/10.04 [v3: list_int] : ! [v4: int] : (v4 = 0 | ~ (no_zero1(v3) = v4) | ~ % 68.35/10.04 list_int(v3) | ? [v5: uni] : ? [v6: int] : ? [v7: int] : ? [v8: uni] : % 68.35/10.04 ($lesseq(1, $difference(v6, v7)) & $lesseq(0, v7) & t2tb1(v3) = v5 & % 68.35/10.04 tb2t(v8) = v2 & nth1(int, v7, v5) = v8 & length1(int, v5) = v6 & uni(v8) % 68.35/10.04 & uni(v5))) & ! [v3: list_int] : ! [v4: uni] : ( ~ (t2tb1(v3) = v4) | % 68.35/10.04 ~ list_int(v3) | ? [v5: int] : ? [v6: any] : ? [v7: int] : ? [v8: uni] % 68.35/10.04 : ? [v9: option_int] : (no_zero1(v3) = v6 & length1(int, v4) = v5 & (v6 = % 68.35/10.04 0 | (v9 = v2 & $lesseq(1, $difference(v5, v7)) & $lesseq(0, v7) & % 68.35/10.04 tb2t(v8) = v2 & nth1(int, v7, v4) = v8 & uni(v8))))) & ! [v3: % 68.35/10.04 list_int] : ! [v4: uni] : ( ~ (t2tb1(v3) = v4) | ~ list_int(v3) | ? % 68.35/10.04 [v5: any] : ? [v6: int] : (no_zero1(v3) = v5 & length1(int, v4) = v6 & ( % 68.35/10.04 ~ (v5 = 0) | ! [v7: int] : ! [v8: uni] : ( ~ ($lesseq(1, % 68.35/10.04 $difference(v6, v7))) | ~ ($lesseq(0, v7)) | ~ (nth1(int, v7, % 68.35/10.04 v4) = v8) | ? [v9: option_int] : ( ~ (v9 = v2) & tb2t(v8) = v9 % 68.35/10.04 & option_int(v9)))))) & ! [v3: list_int] : ( ~ (no_zero1(v3) = 0) % 68.35/10.04 | ~ list_int(v3) | ? [v4: uni] : ? [v5: int] : (t2tb1(v3) = v4 & % 68.35/10.04 length1(int, v4) = v5 & uni(v4) & ! [v6: int] : ! [v7: uni] : ( ~ % 68.35/10.04 ($lesseq(1, $difference(v5, v6))) | ~ ($lesseq(0, v6)) | ~ % 68.35/10.04 (nth1(int, v6, v4) = v7) | ? [v8: option_int] : ( ~ (v8 = v2) & % 68.35/10.04 tb2t(v7) = v8 & option_int(v8)))))) % 68.35/10.04 % 68.35/10.04 (nth_def) % 68.35/10.05 ! [v0: ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 68.35/10.05 [v5: uni] : (v1 = 0 | ~ (nth1(v0, v1, v4) = v5) | ~ (cons(v0, v2, v3) = v4) % 68.35/10.05 | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | (nth1(v0, $sum(v1, -1), v3) = v5 & % 68.35/10.05 uni(v5))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! % 68.35/10.05 [v4: uni] : ( ~ (nth1(v0, 0, v3) = v4) | ~ (cons(v0, v1, v2) = v3) | ~ % 68.35/10.05 ty(v0) | ~ uni(v2) | ~ uni(v1) | (some(v0, v1) = v4 & uni(v4))) & ! [v0: % 68.35/10.05 ty] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ (nth1(v0, v1, v2) = % 68.35/10.05 v3) | ~ (nil(v0) = v2) | ~ ty(v0) | (none(v0) = v3 & uni(v3))) % 68.35/10.05 % 68.35/10.05 (some_proj_1_def1) % 68.35/10.05 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (some(v0, v1) = v2) | ~ % 68.35/10.05 ty(v0) | ~ uni(v1) | ? [v3: any] : ? [v4: uni] : (some_proj_11(v0, v2) = % 68.35/10.05 v4 & sort1(v0, v1) = v3 & uni(v4) & ( ~ (v3 = 0) | v4 = v1))) & ! [v0: % 68.35/10.05 ty] : ! [v1: uni] : ( ~ (sort1(v0, v1) = 0) | ~ ty(v0) | ~ uni(v1) | ? % 68.35/10.05 [v2: uni] : (some_proj_11(v0, v2) = v1 & some(v0, v1) = v2 & uni(v2))) % 68.35/10.05 % 68.35/10.05 (t2tb_sort4) % 68.35/10.05 ty(int) & ? [v0: ty] : (list(int) = v0 & ty(v0) & ! [v1: list_int] : ! [v2: % 68.35/10.05 uni] : ( ~ (t2tb1(v1) = v2) | ~ list_int(v1) | sort1(v0, v2) = 0)) % 68.35/10.05 % 68.35/10.05 (tl_def) % 68.35/10.05 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 68.35/10.05 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : ? [v5: % 68.35/10.05 ty] : (tl(v0, v3) = v4 & some(v5, v2) = v4 & list(v0) = v5 & ty(v5) & % 68.35/10.05 uni(v4))) & ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | % 68.35/10.05 ? [v2: uni] : ? [v3: ty] : (tl(v0, v1) = v2 & none(v3) = v2 & list(v0) = v3 % 68.35/10.05 & ty(v3) & uni(v2))) & ! [v0: ty] : ! [v1: ty] : ( ~ (list(v0) = v1) | % 68.35/10.05 ~ ty(v0) | ? [v2: uni] : ? [v3: uni] : (tl(v0, v2) = v3 & none(v1) = v3 & % 68.35/10.05 nil(v0) = v2 & uni(v3) & uni(v2))) % 68.35/10.05 % 68.35/10.05 (wP_parameter_search_loop) % 68.35/10.06 ty(int) & ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : ? [v3: uni] : % 68.35/10.06 ? [v4: list_int] : ? [v5: list_int] : ? [v6: list_int] : ? [v7: int] : ? % 68.35/10.06 [v8: uni] : ? [v9: int] : ? [v10: uni] : ? [v11: any] : ? [v12: any] : ? % 68.35/10.06 [v13: list_int] : ? [v14: uni] : ? [v15: uni] : ( ~ (v6 = v4) & $lesseq(0, % 68.35/10.06 v7) & no_zero1(v5) = v12 & zero_at1(v5, v7) = v11 & t2tb2(0) = v0 & % 68.35/10.06 tb2t1(v15) = v6 & tb2t1(v3) = v4 & t2tb1(v13) = v14 & t2tb1(v6) = v8 & % 68.35/10.06 t2tb1(v5) = v10 & tb2t(v1) = v2 & some(int, v0) = v1 & length1(int, v10) = % 68.35/10.06 $sum(v9, v7) & length1(int, v8) = v9 & cons(int, v0, v14) = v15 & nil(int) = % 68.35/10.06 v3 & option_int(v2) & list_int(v13) & list_int(v6) & list_int(v5) & % 68.35/10.06 list_int(v4) & uni(v15) & uni(v14) & uni(v10) & uni(v8) & uni(v3) & uni(v1) % 68.35/10.06 & uni(v0) & ! [v16: int] : ! [v17: uni] : ( ~ ($lesseq(1, $difference(v7, % 68.35/10.06 v16))) | ~ ($lesseq(0, v16)) | ~ (nth1(int, v16, v10) = v17) | ? % 68.35/10.06 [v18: option_int] : ( ~ (v18 = v2) & tb2t(v17) = v18 & option_int(v18))) & % 68.35/10.06 ! [v16: int] : ! [v17: uni] : ( ~ ($lesseq(0, v16)) | ~ (nth1(int, % 68.35/10.06 $sum(v16, v7), v10) = v17) | ? [v18: uni] : ? [v19: option_int] : % 68.35/10.06 (tb2t(v18) = v19 & tb2t(v17) = v19 & nth1(int, v16, v8) = v18 & % 68.35/10.06 option_int(v19) & uni(v18))) & ! [v16: int] : ! [v17: uni] : ( ~ % 68.35/10.06 ($lesseq(0, v16)) | ~ (nth1(int, v16, v8) = v17) | ? [v18: option_int] : % 68.35/10.06 ? [v19: uni] : (tb2t(v19) = v18 & tb2t(v17) = v18 & nth1(int, $sum(v16, % 68.35/10.06 v7), v10) = v19 & option_int(v18) & uni(v19))) & ( ~ (v12 = 0) | ~ % 68.35/10.06 (v9 = 0)) & ( ~ (v11 = 0) | ~ ($lesseq(1, v9)))) % 68.35/10.06 % 68.35/10.06 (zero_at_def) % 68.35/10.06 ty(int) & ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : (t2tb2(0) = v0 & % 68.35/10.06 tb2t(v1) = v2 & some(int, v0) = v1 & option_int(v2) & uni(v1) & uni(v0) & ! % 68.35/10.06 [v3: list_int] : ! [v4: int] : ! [v5: uni] : ! [v6: uni] : ( ~ (t2tb1(v3) % 68.35/10.06 = v5) | ~ (nth1(int, v4, v5) = v6) | ~ list_int(v3) | ? [v7: any] : % 68.35/10.06 ? [v8: any] : ? [v9: option_int] : ((v9 = v2 & $lesseq(1, $difference(v4, % 68.35/10.06 v7)) & $lesseq(0, v7) & tb2t(v8) = v2 & nth1(int, v7, v5) = v8 & % 68.35/10.06 uni(v8)) | (zero_at1(v3, v4) = v8 & tb2t(v6) = v7 & option_int(v7) & ( % 68.35/10.06 ~ (v7 = v2) | v8 = 0)))) & ! [v3: list_int] : ! [v4: int] : ! % 68.35/10.06 [v5: uni] : ! [v6: uni] : ( ~ (t2tb1(v3) = v5) | ~ (nth1(int, v4, v5) = % 68.35/10.06 v6) | ~ list_int(v3) | ? [v7: any] : ? [v8: option_int] : % 68.35/10.06 (zero_at1(v3, v4) = v7 & tb2t(v6) = v8 & option_int(v8) & ( ~ (v7 = 0) | % 68.35/10.06 (v8 = v2 & ! [v9: int] : ! [v10: uni] : ( ~ ($lesseq(1, % 68.35/10.06 $difference(v4, v9))) | ~ ($lesseq(0, v9)) | ~ (nth1(int, % 68.35/10.06 v9, v5) = v10) | ? [v11: option_int] : ( ~ (v11 = v2) & % 68.35/10.06 tb2t(v10) = v11 & option_int(v11))))))) & ! [v3: list_int] : ! % 68.35/10.06 [v4: int] : ! [v5: int] : (v5 = 0 | ~ (zero_at1(v3, v4) = v5) | ~ % 68.35/10.06 list_int(v3) | ? [v6: uni] : ? [v7: uni] : ? [v8: option_int] : ? [v9: % 68.35/10.06 int] : ? [v10: uni] : ? [v11: option_int] : (t2tb1(v3) = v6 & tb2t(v7) % 68.35/10.06 = v8 & nth1(int, v4, v6) = v7 & option_int(v8) & uni(v7) & uni(v6) & ( ~ % 68.35/10.06 (v8 = v2) | (v11 = v2 & $lesseq(1, $difference(v4, v9)) & $lesseq(0, % 68.35/10.06 v9) & tb2t(v10) = v2 & nth1(int, v9, v6) = v10 & uni(v10))))) & ! % 68.35/10.06 [v3: list_int] : ! [v4: int] : ( ~ (zero_at1(v3, v4) = 0) | ~ list_int(v3) % 68.35/10.06 | ? [v5: uni] : ? [v6: uni] : (t2tb1(v3) = v5 & tb2t(v6) = v2 & % 68.35/10.06 nth1(int, v4, v5) = v6 & uni(v6) & uni(v5) & ! [v7: int] : ! [v8: uni] % 68.35/10.06 : ( ~ ($lesseq(1, $difference(v4, v7))) | ~ ($lesseq(0, v7)) | ~ % 68.35/10.06 (nth1(int, v7, v5) = v8) | ? [v9: option_int] : ( ~ (v9 = v2) & % 68.35/10.06 tb2t(v8) = v9 & option_int(v9)))))) % 68.35/10.06 % 68.35/10.07 (function-axioms) % 68.35/10.07 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 68.35/10.07 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (match_option1(v6, v5, v4, v3, v2) = % 68.35/10.07 v1) | ~ (match_option1(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! % 68.35/10.07 [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : ! [v6: % 68.35/10.07 ty] : (v1 = v0 | ~ (match_list1(v6, v5, v4, v3, v2) = v1) | ~ % 68.35/10.07 (match_list1(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.35/10.07 [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : (v1 = v0 | ~ % 68.35/10.07 (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, v2) = v0)) % 68.35/10.07 & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : % 68.35/10.07 (v1 = v0 | ~ (nth1(v4, v3, v2) = v1) | ~ (nth1(v4, v3, v2) = v0)) & ! [v0: % 68.35/10.07 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 68.35/10.07 ~ (cons(v4, v3, v2) = v1) | ~ (cons(v4, v3, v2) = v0)) & ! [v0: uni] : ! % 68.35/10.07 [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (tl(v3, v2) = v1) | ~ % 68.35/10.08 (tl(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 68.35/10.08 ty] : (v1 = v0 | ~ (hd(v3, v2) = v1) | ~ (hd(v3, v2) = v0)) & ! [v0: uni] % 68.35/10.08 : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (contents(v3, v2) % 68.35/10.08 = v1) | ~ (contents(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.35/10.08 [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, % 68.35/10.08 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 68.35/10.08 ! [v2: int] : ! [v3: list_int] : (v1 = v0 | ~ (zero_at1(v3, v2) = v1) | ~ % 68.35/10.08 (zero_at1(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 68.35/10.08 [v3: ty] : (v1 = v0 | ~ (some_proj_11(v3, v2) = v1) | ~ (some_proj_11(v3, % 68.35/10.08 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : % 68.35/10.08 (v1 = v0 | ~ (some(v3, v2) = v1) | ~ (some(v3, v2) = v0)) & ! [v0: int] : % 68.35/10.08 ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (length1(v3, v2) = % 68.35/10.08 v1) | ~ (length1(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 68.35/10.08 uni] : ! [v3: ty] : (v1 = v0 | ~ (cons_proj_21(v3, v2) = v1) | ~ % 68.35/10.08 (cons_proj_21(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 68.35/10.08 ! [v3: ty] : (v1 = v0 | ~ (cons_proj_11(v3, v2) = v1) | ~ (cons_proj_11(v3, % 68.35/10.08 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 68.35/10.08 ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, % 68.35/10.08 v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ % 68.35/10.08 (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.35/10.08 MultipleValueBool] : ! [v2: list_int] : (v1 = v0 | ~ (no_zero1(v2) = v1) | % 68.35/10.08 ~ (no_zero1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = % 68.35/10.08 v0 | ~ (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) & ! [v0: uni] : ! [v1: % 68.35/10.08 uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) % 68.35/10.08 & ! [v0: list_int] : ! [v1: list_int] : ! [v2: uni] : (v1 = v0 | ~ % 68.35/10.08 (tb2t1(v2) = v1) | ~ (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.35/10.08 [v2: list_int] : (v1 = v0 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! % 68.35/10.08 [v0: option_int] : ! [v1: option_int] : ! [v2: uni] : (v1 = v0 | ~ % 68.35/10.08 (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.35/10.08 [v2: option_int] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! % 68.35/10.08 [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (none(v2) = v1) | ~ % 68.35/10.08 (none(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ % 68.35/10.08 (option(v2) = v1) | ~ (option(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.35/10.08 [v2: ty] : (v1 = v0 | ~ (nil(v2) = v1) | ~ (nil(v2) = v0)) & ! [v0: ty] : % 68.35/10.08 ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (list(v2) = v1) | ~ (list(v2) = v0)) % 68.35/10.08 & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (witness1(v2) = % 68.35/10.08 v1) | ~ (witness1(v2) = v0)) % 68.35/10.08 % 68.35/10.08 Further assumptions not needed in the proof: % 68.35/10.08 -------------------------------------------- % 68.35/10.08 bool_inversion, bridgeL, bridgeL1, bridgeL2, bridgeR2, compatOrderMult, % 68.35/10.08 cons_proj_1_def1, cons_proj_1_sort3, cons_proj_2_def1, cons_proj_2_sort3, % 68.35/10.08 contents_def1, contents_sort1, hd_sort1, list_inversion1, match_bool_False, % 68.35/10.08 match_bool_True, match_bool_sort3, match_list_Cons1, match_list_Nil1, % 68.35/10.08 match_list_sort3, match_option_None1, match_option_Some1, match_option_sort3, % 68.35/10.08 mk_ref_sort1, none_Some1, none_sort3, nth_sort3, option_inversion1, % 68.35/10.08 ref_inversion1, some_proj_1_sort3, some_sort3, t2tb_sort3, t2tb_sort5, tl_sort1, % 68.35/10.08 true_False, tuple0_inversion, witness_sort1 % 68.35/10.08 % 68.35/10.08 Those formulas are unsatisfiable: % 68.35/10.08 --------------------------------- % 68.35/10.08 % 68.35/10.08 Begin of proof % 68.35/10.08 | % 68.35/10.08 | ALPHA: (nil_sort3) implies: % 68.35/10.08 | (1) ! [v0: ty] : ! [v1: ty] : ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: % 68.35/10.08 | uni] : (nil(v0) = v2 & sort1(v1, v2) = 0 & uni(v2))) % 68.35/10.08 | (2) ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | ? [v2: % 68.35/10.08 | ty] : (list(v0) = v2 & sort1(v2, v1) = 0 & ty(v2))) % 68.35/10.08 | % 68.35/10.08 | ALPHA: (length_def) implies: % 68.35/10.08 | (3) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.35/10.08 | (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 68.35/10.08 | [v4: int] : (length1(v0, v3) = v4 & length1(v0, v2) = $sum(v4, -1))) % 68.35/10.08 | % 68.35/10.08 | ALPHA: (length_nil) implies: % 68.35/10.08 | (4) ! [v0: ty] : ! [v1: uni] : ( ~ (length1(v0, v1) = 0) | ~ ty(v0) | ~ % 68.35/10.08 | uni(v1) | nil(v0) = v1) % 68.35/10.09 | (5) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (length1(v0, % 68.35/10.09 | v1) = v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : ( ~ (v3 = v1) % 68.35/10.09 | & nil(v0) = v3 & uni(v3))) % 68.35/10.09 | % 68.35/10.09 | ALPHA: (some_proj_1_def1) implies: % 68.35/10.09 | (6) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (some(v0, v1) = v2) | % 68.35/10.09 | ~ ty(v0) | ~ uni(v1) | ? [v3: any] : ? [v4: uni] : % 68.35/10.09 | (some_proj_11(v0, v2) = v4 & sort1(v0, v1) = v3 & uni(v4) & ( ~ (v3 = % 68.35/10.09 | 0) | v4 = v1))) % 68.35/10.09 | % 68.35/10.09 | ALPHA: (nth_def) implies: % 68.35/10.09 | (7) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] % 68.35/10.09 | : ( ~ (nth1(v0, 0, v3) = v4) | ~ (cons(v0, v1, v2) = v3) | ~ ty(v0) | % 68.35/10.09 | ~ uni(v2) | ~ uni(v1) | (some(v0, v1) = v4 & uni(v4))) % 68.35/10.09 | % 68.35/10.09 | ALPHA: (t2tb_sort4) implies: % 68.35/10.09 | (8) ? [v0: ty] : (list(int) = v0 & ty(v0) & ! [v1: list_int] : ! [v2: % 68.35/10.09 | uni] : ( ~ (t2tb1(v1) = v2) | ~ list_int(v1) | sort1(v0, v2) = 0)) % 68.35/10.09 | % 68.35/10.09 | ALPHA: (zero_at_def) implies: % 68.35/10.09 | (9) ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : (t2tb2(0) = v0 & % 68.35/10.09 | tb2t(v1) = v2 & some(int, v0) = v1 & option_int(v2) & uni(v1) & % 68.35/10.09 | uni(v0) & ! [v3: list_int] : ! [v4: int] : ! [v5: uni] : ! [v6: % 68.35/10.09 | uni] : ( ~ (t2tb1(v3) = v5) | ~ (nth1(int, v4, v5) = v6) | ~ % 68.35/10.09 | list_int(v3) | ? [v7: any] : ? [v8: any] : ? [v9: option_int] : % 68.35/10.09 | ((v9 = v2 & $lesseq(1, $difference(v4, v7)) & $lesseq(0, v7) & % 68.35/10.09 | tb2t(v8) = v2 & nth1(int, v7, v5) = v8 & uni(v8)) | % 68.35/10.09 | (zero_at1(v3, v4) = v8 & tb2t(v6) = v7 & option_int(v7) & ( ~ (v7 % 68.35/10.09 | = v2) | v8 = 0)))) & ! [v3: list_int] : ! [v4: int] : ! % 68.35/10.09 | [v5: uni] : ! [v6: uni] : ( ~ (t2tb1(v3) = v5) | ~ (nth1(int, v4, % 68.35/10.09 | v5) = v6) | ~ list_int(v3) | ? [v7: any] : ? [v8: % 68.35/10.09 | option_int] : (zero_at1(v3, v4) = v7 & tb2t(v6) = v8 & % 68.35/10.09 | option_int(v8) & ( ~ (v7 = 0) | (v8 = v2 & ! [v9: int] : ! % 68.35/10.09 | [v10: uni] : ( ~ ($lesseq(1, $difference(v4, v9))) | ~ % 68.35/10.09 | ($lesseq(0, v9)) | ~ (nth1(int, v9, v5) = v10) | ? [v11: % 68.35/10.09 | option_int] : ( ~ (v11 = v2) & tb2t(v10) = v11 & % 68.35/10.09 | option_int(v11))))))) & ! [v3: list_int] : ! [v4: int] % 68.35/10.09 | : ! [v5: int] : (v5 = 0 | ~ (zero_at1(v3, v4) = v5) | ~ % 68.35/10.09 | list_int(v3) | ? [v6: uni] : ? [v7: uni] : ? [v8: option_int] : % 68.35/10.09 | ? [v9: int] : ? [v10: uni] : ? [v11: option_int] : (t2tb1(v3) = % 68.35/10.09 | v6 & tb2t(v7) = v8 & nth1(int, v4, v6) = v7 & option_int(v8) & % 68.35/10.09 | uni(v7) & uni(v6) & ( ~ (v8 = v2) | (v11 = v2 & $lesseq(1, % 68.35/10.09 | $difference(v4, v9)) & $lesseq(0, v9) & tb2t(v10) = v2 & % 68.35/10.09 | nth1(int, v9, v6) = v10 & uni(v10))))) & ! [v3: list_int] : % 68.35/10.09 | ! [v4: int] : ( ~ (zero_at1(v3, v4) = 0) | ~ list_int(v3) | ? [v5: % 68.35/10.09 | uni] : ? [v6: uni] : (t2tb1(v3) = v5 & tb2t(v6) = v2 & nth1(int, % 68.35/10.09 | v4, v5) = v6 & uni(v6) & uni(v5) & ! [v7: int] : ! [v8: uni] % 68.35/10.10 | : ( ~ ($lesseq(1, $difference(v4, v7))) | ~ ($lesseq(0, v7)) | % 68.35/10.10 | ~ (nth1(int, v7, v5) = v8) | ? [v9: option_int] : ( ~ (v9 = % 68.35/10.10 | v2) & tb2t(v8) = v9 & option_int(v9)))))) % 68.35/10.10 | % 68.35/10.10 | ALPHA: (no_zero_def) implies: % 68.35/10.10 | (10) ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : (t2tb2(0) = v0 & % 68.35/10.10 | tb2t(v1) = v2 & some(int, v0) = v1 & option_int(v2) & uni(v1) & % 68.35/10.10 | uni(v0) & ! [v3: list_int] : ! [v4: int] : (v4 = 0 | ~ % 68.35/10.10 | (no_zero1(v3) = v4) | ~ list_int(v3) | ? [v5: uni] : ? [v6: % 68.35/10.10 | int] : ? [v7: int] : ? [v8: uni] : ($lesseq(1, $difference(v6, % 68.35/10.10 | v7)) & $lesseq(0, v7) & t2tb1(v3) = v5 & tb2t(v8) = v2 & % 68.35/10.10 | nth1(int, v7, v5) = v8 & length1(int, v5) = v6 & uni(v8) & % 68.35/10.10 | uni(v5))) & ! [v3: list_int] : ! [v4: uni] : ( ~ (t2tb1(v3) = % 68.35/10.10 | v4) | ~ list_int(v3) | ? [v5: int] : ? [v6: any] : ? [v7: % 68.35/10.10 | int] : ? [v8: uni] : ? [v9: option_int] : (no_zero1(v3) = v6 & % 68.35/10.10 | length1(int, v4) = v5 & (v6 = 0 | (v9 = v2 & $lesseq(1, % 68.35/10.10 | $difference(v5, v7)) & $lesseq(0, v7) & tb2t(v8) = v2 & % 68.35/10.10 | nth1(int, v7, v4) = v8 & uni(v8))))) & ! [v3: list_int] : % 68.35/10.10 | ! [v4: uni] : ( ~ (t2tb1(v3) = v4) | ~ list_int(v3) | ? [v5: any] % 68.35/10.10 | : ? [v6: int] : (no_zero1(v3) = v5 & length1(int, v4) = v6 & ( ~ % 68.35/10.10 | (v5 = 0) | ! [v7: int] : ! [v8: uni] : ( ~ ($lesseq(1, % 68.35/10.10 | $difference(v6, v7))) | ~ ($lesseq(0, v7)) | ~ % 68.35/10.10 | (nth1(int, v7, v4) = v8) | ? [v9: option_int] : ( ~ (v9 = % 68.35/10.10 | v2) & tb2t(v8) = v9 & option_int(v9)))))) & ! [v3: % 68.35/10.10 | list_int] : ( ~ (no_zero1(v3) = 0) | ~ list_int(v3) | ? [v4: % 68.35/10.10 | uni] : ? [v5: int] : (t2tb1(v3) = v4 & length1(int, v4) = v5 & % 68.35/10.10 | uni(v4) & ! [v6: int] : ! [v7: uni] : ( ~ ($lesseq(1, % 68.35/10.10 | $difference(v5, v6))) | ~ ($lesseq(0, v6)) | ~ % 68.35/10.10 | (nth1(int, v6, v4) = v7) | ? [v8: option_int] : ( ~ (v8 = v2) % 68.35/10.10 | & tb2t(v7) = v8 & option_int(v8)))))) % 68.35/10.10 | % 68.35/10.10 | ALPHA: (hd_def) implies: % 68.35/10.10 | (11) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.35/10.10 | (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 68.35/10.10 | [v4: uni] : (hd(v0, v3) = v4 & some(v0, v1) = v4 & uni(v4))) % 68.35/10.10 | % 68.35/10.10 | ALPHA: (tl_def) implies: % 68.35/10.10 | (12) ! [v0: ty] : ! [v1: ty] : ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: % 68.35/10.10 | uni] : ? [v3: uni] : (tl(v0, v2) = v3 & none(v1) = v3 & nil(v0) = % 68.35/10.10 | v2 & uni(v3) & uni(v2))) % 68.35/10.10 | (13) ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | ? [v2: % 68.35/10.10 | uni] : ? [v3: ty] : (tl(v0, v1) = v2 & none(v3) = v2 & list(v0) = % 68.35/10.10 | v3 & ty(v3) & uni(v2))) % 68.35/10.11 | (14) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.35/10.11 | (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 68.35/10.11 | [v4: uni] : ? [v5: ty] : (tl(v0, v3) = v4 & some(v5, v2) = v4 & % 68.35/10.11 | list(v0) = v5 & ty(v5) & uni(v4))) % 68.35/10.11 | % 68.35/10.11 | ALPHA: (wP_parameter_search_loop) implies: % 68.35/10.11 | (15) ty(int) % 68.35/10.11 | (16) ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : ? [v3: uni] : ? % 68.35/10.11 | [v4: list_int] : ? [v5: list_int] : ? [v6: list_int] : ? [v7: int] % 68.35/10.11 | : ? [v8: uni] : ? [v9: int] : ? [v10: uni] : ? [v11: any] : ? % 68.35/10.11 | [v12: any] : ? [v13: list_int] : ? [v14: uni] : ? [v15: uni] : ( ~ % 68.35/10.11 | (v6 = v4) & $lesseq(0, v7) & no_zero1(v5) = v12 & zero_at1(v5, v7) = % 68.35/10.11 | v11 & t2tb2(0) = v0 & tb2t1(v15) = v6 & tb2t1(v3) = v4 & t2tb1(v13) % 68.35/10.11 | = v14 & t2tb1(v6) = v8 & t2tb1(v5) = v10 & tb2t(v1) = v2 & some(int, % 68.35/10.11 | v0) = v1 & length1(int, v10) = $sum(v9, v7) & length1(int, v8) = % 68.35/10.11 | v9 & cons(int, v0, v14) = v15 & nil(int) = v3 & option_int(v2) & % 68.35/10.11 | list_int(v13) & list_int(v6) & list_int(v5) & list_int(v4) & % 68.35/10.11 | uni(v15) & uni(v14) & uni(v10) & uni(v8) & uni(v3) & uni(v1) & % 68.35/10.11 | uni(v0) & ! [v16: int] : ! [v17: uni] : ( ~ ($lesseq(1, % 68.35/10.11 | $difference(v7, v16))) | ~ ($lesseq(0, v16)) | ~ (nth1(int, % 68.35/10.11 | v16, v10) = v17) | ? [v18: option_int] : ( ~ (v18 = v2) & % 68.35/10.11 | tb2t(v17) = v18 & option_int(v18))) & ! [v16: int] : ! [v17: % 68.35/10.11 | uni] : ( ~ ($lesseq(0, v16)) | ~ (nth1(int, $sum(v16, v7), v10) = % 68.35/10.11 | v17) | ? [v18: uni] : ? [v19: option_int] : (tb2t(v18) = v19 & % 68.35/10.11 | tb2t(v17) = v19 & nth1(int, v16, v8) = v18 & option_int(v19) & % 68.35/10.11 | uni(v18))) & ! [v16: int] : ! [v17: uni] : ( ~ ($lesseq(0, % 68.35/10.11 | v16)) | ~ (nth1(int, v16, v8) = v17) | ? [v18: option_int] : % 68.35/10.11 | ? [v19: uni] : (tb2t(v19) = v18 & tb2t(v17) = v18 & nth1(int, % 68.35/10.11 | $sum(v16, v7), v10) = v19 & option_int(v18) & uni(v19))) & ( ~ % 68.35/10.11 | (v12 = 0) | ~ (v9 = 0)) & ( ~ (v11 = 0) | ~ ($lesseq(1, v9)))) % 68.35/10.11 | % 68.35/10.11 | ALPHA: (function-axioms) implies: % 68.35/10.11 | (17) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (list(v2) = % 68.35/10.11 | v1) | ~ (list(v2) = v0)) % 68.35/10.11 | (18) ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = % 68.35/10.11 | v1) | ~ (nil(v2) = v0)) % 68.35/10.11 | (19) ! [v0: uni] : ! [v1: uni] : ! [v2: option_int] : (v1 = v0 | ~ % 68.35/10.11 | (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) % 68.35/10.11 | (20) ! [v0: option_int] : ! [v1: option_int] : ! [v2: uni] : (v1 = v0 | % 68.35/10.11 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 68.35/10.11 | (21) ! [v0: uni] : ! [v1: uni] : ! [v2: list_int] : (v1 = v0 | ~ % 68.35/10.11 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 68.35/10.11 | (22) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb2(v2) % 68.35/10.11 | = v1) | ~ (t2tb2(v2) = v0)) % 68.35/10.12 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 68.35/10.12 | list_int] : (v1 = v0 | ~ (no_zero1(v2) = v1) | ~ (no_zero1(v2) = % 68.35/10.12 | v0)) % 68.35/10.12 | (24) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 68.35/10.12 | : ! [v3: ty] : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) % 68.35/10.12 | = v0)) % 68.35/10.12 | (25) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 68.35/10.12 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) % 68.35/10.12 | (26) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 68.35/10.12 | ~ (some(v3, v2) = v1) | ~ (some(v3, v2) = v0)) % 68.35/10.12 | % 68.35/10.12 | DELTA: instantiating (8) with fresh symbol all_66_0 gives: % 68.35/10.12 | (27) list(int) = all_66_0 & ty(all_66_0) & ! [v0: list_int] : ! [v1: uni] % 68.35/10.12 | : ( ~ (t2tb1(v0) = v1) | ~ list_int(v0) | sort1(all_66_0, v1) = 0) % 68.35/10.12 | % 68.35/10.12 | ALPHA: (27) implies: % 68.35/10.12 | (28) list(int) = all_66_0 % 68.35/10.12 | (29) ! [v0: list_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 68.35/10.12 | list_int(v0) | sort1(all_66_0, v1) = 0) % 68.35/10.12 | % 68.35/10.12 | DELTA: instantiating (10) with fresh symbols all_69_0, all_69_1, all_69_2 % 68.35/10.12 | gives: % 68.35/10.12 | (30) t2tb2(0) = all_69_2 & tb2t(all_69_1) = all_69_0 & some(int, all_69_2) % 68.35/10.12 | = all_69_1 & option_int(all_69_0) & uni(all_69_1) & uni(all_69_2) & ! % 68.35/10.12 | [v0: list_int] : ! [v1: int] : (v1 = 0 | ~ (no_zero1(v0) = v1) | ~ % 68.35/10.12 | list_int(v0) | ? [v2: uni] : ? [v3: int] : ? [v4: int] : ? [v5: % 68.35/10.12 | uni] : ($lesseq(1, $difference(v3, v4)) & $lesseq(0, v4) & % 68.35/10.12 | t2tb1(v0) = v2 & tb2t(v5) = all_69_0 & nth1(int, v4, v2) = v5 & % 68.35/10.12 | length1(int, v2) = v3 & uni(v5) & uni(v2))) & ! [v0: list_int] : % 68.35/10.12 | ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ list_int(v0) | ? [v2: int] : % 68.35/10.12 | ? [v3: any] : ? [v4: int] : ? [v5: uni] : ? [v6: int] : % 68.35/10.12 | (no_zero1(v0) = v3 & length1(int, v1) = v2 & (v3 = 0 | (v6 = % 68.35/10.12 | all_69_0 & $lesseq(1, $difference(v2, v4)) & $lesseq(0, v4) & % 68.35/10.12 | tb2t(v5) = all_69_0 & nth1(int, v4, v1) = v5 & uni(v5))))) & % 68.35/10.12 | ! [v0: list_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 68.35/10.12 | list_int(v0) | ? [v2: any] : ? [v3: int] : (no_zero1(v0) = v2 & % 68.35/10.12 | length1(int, v1) = v3 & ( ~ (v2 = 0) | ! [v4: int] : ! [v5: uni] % 68.35/10.12 | : ( ~ ($lesseq(1, $difference(v3, v4))) | ~ ($lesseq(0, v4)) | % 68.35/10.12 | ~ (nth1(int, v4, v1) = v5) | ? [v6: any] : ( ~ (v6 = % 68.35/10.12 | all_69_0) & tb2t(v5) = v6 & option_int(v6)))))) & ! [v0: % 68.35/10.12 | list_int] : ( ~ (no_zero1(v0) = 0) | ~ list_int(v0) | ? [v1: uni] % 68.35/10.12 | : ? [v2: int] : (t2tb1(v0) = v1 & length1(int, v1) = v2 & uni(v1) & % 68.35/10.12 | ! [v3: int] : ! [v4: uni] : ( ~ ($lesseq(1, $difference(v2, % 68.35/10.12 | v3))) | ~ ($lesseq(0, v3)) | ~ (nth1(int, v3, v1) = v4) % 68.35/10.13 | | ? [v5: any] : ( ~ (v5 = all_69_0) & tb2t(v4) = v5 & % 68.35/10.13 | option_int(v5))))) % 68.35/10.13 | % 68.35/10.13 | ALPHA: (30) implies: % 68.35/10.13 | (31) some(int, all_69_2) = all_69_1 % 68.35/10.13 | (32) tb2t(all_69_1) = all_69_0 % 68.35/10.13 | (33) t2tb2(0) = all_69_2 % 68.35/10.13 | (34) ! [v0: list_int] : ( ~ (no_zero1(v0) = 0) | ~ list_int(v0) | ? [v1: % 68.35/10.13 | uni] : ? [v2: int] : (t2tb1(v0) = v1 & length1(int, v1) = v2 & % 68.35/10.13 | uni(v1) & ! [v3: int] : ! [v4: uni] : ( ~ ($lesseq(1, % 68.35/10.13 | $difference(v2, v3))) | ~ ($lesseq(0, v3)) | ~ (nth1(int, % 68.35/10.13 | v3, v1) = v4) | ? [v5: any] : ( ~ (v5 = all_69_0) & % 68.35/10.13 | tb2t(v4) = v5 & option_int(v5))))) % 68.35/10.13 | (35) ! [v0: list_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 68.35/10.13 | list_int(v0) | ? [v2: any] : ? [v3: int] : (no_zero1(v0) = v2 & % 68.35/10.13 | length1(int, v1) = v3 & ( ~ (v2 = 0) | ! [v4: int] : ! [v5: uni] % 68.35/10.13 | : ( ~ ($lesseq(1, $difference(v3, v4))) | ~ ($lesseq(0, v4)) | % 68.35/10.13 | ~ (nth1(int, v4, v1) = v5) | ? [v6: any] : ( ~ (v6 = % 68.35/10.13 | all_69_0) & tb2t(v5) = v6 & option_int(v6)))))) % 68.35/10.13 | (36) ! [v0: list_int] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ % 68.35/10.13 | list_int(v0) | ? [v2: int] : ? [v3: any] : ? [v4: int] : ? [v5: % 68.35/10.13 | uni] : ? [v6: int] : (no_zero1(v0) = v3 & length1(int, v1) = v2 & % 68.35/10.13 | (v3 = 0 | (v6 = all_69_0 & $lesseq(1, $difference(v2, v4)) & % 68.35/10.13 | $lesseq(0, v4) & tb2t(v5) = all_69_0 & nth1(int, v4, v1) = v5 % 68.35/10.13 | & uni(v5))))) % 68.35/10.13 | (37) ! [v0: list_int] : ! [v1: int] : (v1 = 0 | ~ (no_zero1(v0) = v1) | % 68.35/10.13 | ~ list_int(v0) | ? [v2: uni] : ? [v3: int] : ? [v4: int] : ? % 68.35/10.13 | [v5: uni] : ($lesseq(1, $difference(v3, v4)) & $lesseq(0, v4) & % 68.35/10.13 | t2tb1(v0) = v2 & tb2t(v5) = all_69_0 & nth1(int, v4, v2) = v5 & % 68.35/10.13 | length1(int, v2) = v3 & uni(v5) & uni(v2))) % 68.35/10.13 | % 68.35/10.13 | DELTA: instantiating (16) with fresh symbols all_72_0, all_72_1, all_72_2, % 68.35/10.13 | all_72_3, all_72_4, all_72_5, all_72_6, all_72_7, all_72_8, all_72_9, % 68.35/10.13 | all_72_10, all_72_11, all_72_12, all_72_13, all_72_14, all_72_15 gives: % 68.35/10.13 | (38) ~ (all_72_9 = all_72_11) & $lesseq(0, all_72_8) & no_zero1(all_72_10) % 68.35/10.13 | = all_72_3 & zero_at1(all_72_10, all_72_8) = all_72_4 & t2tb2(0) = % 68.35/10.13 | all_72_15 & tb2t1(all_72_0) = all_72_9 & tb2t1(all_72_12) = all_72_11 % 68.35/10.13 | & t2tb1(all_72_2) = all_72_1 & t2tb1(all_72_9) = all_72_7 & % 68.35/10.13 | t2tb1(all_72_10) = all_72_5 & tb2t(all_72_14) = all_72_13 & some(int, % 68.35/10.13 | all_72_15) = all_72_14 & length1(int, all_72_5) = $sum(all_72_6, % 68.35/10.13 | all_72_8) & length1(int, all_72_7) = all_72_6 & cons(int, all_72_15, % 68.35/10.13 | all_72_1) = all_72_0 & nil(int) = all_72_12 & option_int(all_72_13) % 68.35/10.13 | & list_int(all_72_2) & list_int(all_72_9) & list_int(all_72_10) & % 68.35/10.13 | list_int(all_72_11) & uni(all_72_0) & uni(all_72_1) & uni(all_72_5) & % 68.35/10.13 | uni(all_72_7) & uni(all_72_12) & uni(all_72_14) & uni(all_72_15) & ! % 68.35/10.13 | [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_72_8, v0))) % 68.35/10.13 | | ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, all_72_5) = v1) | ? [v2: % 68.35/10.14 | any] : ( ~ (v2 = all_72_13) & tb2t(v1) = v2 & option_int(v2))) & % 68.35/10.14 | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (nth1(int, % 68.35/10.14 | $sum(v0, all_72_8), all_72_5) = v1) | ? [v2: uni] : ? [v3: % 68.35/10.14 | option_int] : (tb2t(v2) = v3 & tb2t(v1) = v3 & nth1(int, v0, % 68.35/10.14 | all_72_7) = v2 & option_int(v3) & uni(v2))) & ! [v0: int] : ! % 68.35/10.14 | [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, all_72_7) = v1) | % 68.35/10.14 | ? [v2: option_int] : ? [v3: uni] : (tb2t(v3) = v2 & tb2t(v1) = v2 % 68.35/10.14 | & nth1(int, $sum(v0, all_72_8), all_72_5) = v3 & option_int(v2) & % 68.35/10.14 | uni(v3))) & ( ~ (all_72_3 = 0) | ~ (all_72_6 = 0)) & ( ~ % 68.35/10.14 | (all_72_4 = 0) | ~ ($lesseq(1, all_72_6))) % 68.35/10.14 | % 68.35/10.14 | ALPHA: (38) implies: % 68.35/10.14 | (39) $lesseq(0, all_72_8) % 68.35/10.14 | (40) uni(all_72_15) % 68.35/10.14 | (41) uni(all_72_14) % 68.35/10.14 | (42) uni(all_72_5) % 68.35/10.14 | (43) uni(all_72_1) % 68.35/10.14 | (44) uni(all_72_0) % 68.35/10.14 | (45) list_int(all_72_10) % 68.35/10.14 | (46) list_int(all_72_9) % 68.35/10.14 | (47) list_int(all_72_2) % 68.35/10.14 | (48) nil(int) = all_72_12 % 68.35/10.14 | (49) cons(int, all_72_15, all_72_1) = all_72_0 % 68.35/10.14 | (50) length1(int, all_72_7) = all_72_6 % 68.35/10.14 | (51) length1(int, all_72_5) = $sum(all_72_6, all_72_8) % 68.35/10.14 | (52) some(int, all_72_15) = all_72_14 % 68.35/10.14 | (53) tb2t(all_72_14) = all_72_13 % 68.35/10.14 | (54) t2tb1(all_72_10) = all_72_5 % 68.35/10.14 | (55) t2tb1(all_72_9) = all_72_7 % 68.35/10.14 | (56) t2tb1(all_72_2) = all_72_1 % 68.35/10.14 | (57) tb2t1(all_72_0) = all_72_9 % 68.35/10.14 | (58) t2tb2(0) = all_72_15 % 68.35/10.14 | (59) zero_at1(all_72_10, all_72_8) = all_72_4 % 68.35/10.14 | (60) no_zero1(all_72_10) = all_72_3 % 68.35/10.14 | (61) ~ (all_72_4 = 0) | ~ ($lesseq(1, all_72_6)) % 68.35/10.14 | (62) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, % 68.35/10.14 | all_72_7) = v1) | ? [v2: option_int] : ? [v3: uni] : (tb2t(v3) % 68.35/10.14 | = v2 & tb2t(v1) = v2 & nth1(int, $sum(v0, all_72_8), all_72_5) = % 68.35/10.14 | v3 & option_int(v2) & uni(v3))) % 68.35/10.14 | (63) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(0, v0)) | ~ (nth1(int, % 68.35/10.14 | $sum(v0, all_72_8), all_72_5) = v1) | ? [v2: uni] : ? [v3: % 68.35/10.14 | option_int] : (tb2t(v2) = v3 & tb2t(v1) = v3 & nth1(int, v0, % 68.35/10.14 | all_72_7) = v2 & option_int(v3) & uni(v2))) % 68.35/10.14 | (64) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_72_8, % 68.35/10.14 | v0))) | ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, all_72_5) = % 68.35/10.14 | v1) | ? [v2: any] : ( ~ (v2 = all_72_13) & tb2t(v1) = v2 & % 68.35/10.14 | option_int(v2))) % 68.35/10.14 | % 68.35/10.14 | DELTA: instantiating (9) with fresh symbols all_76_0, all_76_1, all_76_2 % 68.35/10.14 | gives: % 68.89/10.14 | (65) t2tb2(0) = all_76_2 & tb2t(all_76_1) = all_76_0 & some(int, all_76_2) % 68.89/10.14 | = all_76_1 & option_int(all_76_0) & uni(all_76_1) & uni(all_76_2) & ! % 68.89/10.14 | [v0: list_int] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.89/10.14 | (t2tb1(v0) = v2) | ~ (nth1(int, v1, v2) = v3) | ~ list_int(v0) | % 68.89/10.14 | ? [v4: any] : ? [v5: any] : ? [v6: int] : ((v6 = all_76_0 & % 68.89/10.14 | $lesseq(1, $difference(v1, v4)) & $lesseq(0, v4) & tb2t(v5) = % 68.89/10.14 | all_76_0 & nth1(int, v4, v2) = v5 & uni(v5)) | (zero_at1(v0, v1) % 68.89/10.14 | = v5 & tb2t(v3) = v4 & option_int(v4) & ( ~ (v4 = all_76_0) | v5 % 68.89/10.14 | = 0)))) & ! [v0: list_int] : ! [v1: int] : ! [v2: uni] : ! % 68.89/10.14 | [v3: uni] : ( ~ (t2tb1(v0) = v2) | ~ (nth1(int, v1, v2) = v3) | ~ % 68.89/10.14 | list_int(v0) | ? [v4: any] : ? [v5: option_int] : (zero_at1(v0, % 68.89/10.14 | v1) = v4 & tb2t(v3) = v5 & option_int(v5) & ( ~ (v4 = 0) | (v5 = % 68.89/10.14 | all_76_0 & ! [v6: int] : ! [v7: uni] : ( ~ ($lesseq(1, % 68.89/10.14 | $difference(v1, v6))) | ~ ($lesseq(0, v6)) | ~ % 68.89/10.14 | (nth1(int, v6, v2) = v7) | ? [v8: any] : ( ~ (v8 = % 68.89/10.14 | all_76_0) & tb2t(v7) = v8 & option_int(v8))))))) & ! % 68.89/10.14 | [v0: list_int] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ % 68.89/10.14 | (zero_at1(v0, v1) = v2) | ~ list_int(v0) | ? [v3: uni] : ? [v4: % 68.89/10.14 | uni] : ? [v5: option_int] : ? [v6: int] : ? [v7: uni] : ? [v8: % 68.89/10.14 | int] : (t2tb1(v0) = v3 & tb2t(v4) = v5 & nth1(int, v1, v3) = v4 & % 68.89/10.14 | option_int(v5) & uni(v4) & uni(v3) & ( ~ (v5 = all_76_0) | (v8 = % 68.89/10.14 | all_76_0 & $lesseq(1, $difference(v1, v6)) & $lesseq(0, v6) & % 68.89/10.14 | tb2t(v7) = all_76_0 & nth1(int, v6, v3) = v7 & uni(v7))))) & % 68.89/10.14 | ! [v0: list_int] : ! [v1: int] : ( ~ (zero_at1(v0, v1) = 0) | ~ % 68.89/10.14 | list_int(v0) | ? [v2: uni] : ? [v3: uni] : (t2tb1(v0) = v2 & % 68.89/10.14 | tb2t(v3) = all_76_0 & nth1(int, v1, v2) = v3 & uni(v3) & uni(v2) & % 68.89/10.14 | ! [v4: int] : ! [v5: uni] : ( ~ ($lesseq(1, $difference(v1, % 68.89/10.14 | v4))) | ~ ($lesseq(0, v4)) | ~ (nth1(int, v4, v2) = v5) % 68.89/10.15 | | ? [v6: any] : ( ~ (v6 = all_76_0) & tb2t(v5) = v6 & % 68.89/10.15 | option_int(v6))))) % 68.89/10.15 | % 68.89/10.15 | ALPHA: (65) implies: % 68.89/10.15 | (66) some(int, all_76_2) = all_76_1 % 68.89/10.15 | (67) tb2t(all_76_1) = all_76_0 % 68.89/10.15 | (68) t2tb2(0) = all_76_2 % 68.89/10.15 | (69) ! [v0: list_int] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ % 68.89/10.15 | (zero_at1(v0, v1) = v2) | ~ list_int(v0) | ? [v3: uni] : ? [v4: % 68.89/10.15 | uni] : ? [v5: option_int] : ? [v6: int] : ? [v7: uni] : ? [v8: % 68.89/10.15 | int] : (t2tb1(v0) = v3 & tb2t(v4) = v5 & nth1(int, v1, v3) = v4 & % 68.89/10.15 | option_int(v5) & uni(v4) & uni(v3) & ( ~ (v5 = all_76_0) | (v8 = % 68.89/10.15 | all_76_0 & $lesseq(1, $difference(v1, v6)) & $lesseq(0, v6) & % 68.89/10.15 | tb2t(v7) = all_76_0 & nth1(int, v6, v3) = v7 & uni(v7))))) % 68.89/10.15 | (70) ! [v0: list_int] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.89/10.15 | (t2tb1(v0) = v2) | ~ (nth1(int, v1, v2) = v3) | ~ list_int(v0) | % 68.89/10.15 | ? [v4: any] : ? [v5: option_int] : (zero_at1(v0, v1) = v4 & % 68.89/10.15 | tb2t(v3) = v5 & option_int(v5) & ( ~ (v4 = 0) | (v5 = all_76_0 & % 68.89/10.15 | ! [v6: int] : ! [v7: uni] : ( ~ ($lesseq(1, $difference(v1, % 68.89/10.15 | v6))) | ~ ($lesseq(0, v6)) | ~ (nth1(int, v6, v2) = % 68.89/10.15 | v7) | ? [v8: any] : ( ~ (v8 = all_76_0) & tb2t(v7) = v8 & % 68.89/10.15 | option_int(v8))))))) % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (22) with all_72_15, all_76_2, 0, simplifying with % 68.89/10.15 | (58), (68) gives: % 68.89/10.15 | (71) all_76_2 = all_72_15 % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (22) with all_69_2, all_76_2, 0, simplifying with % 68.89/10.15 | (33), (68) gives: % 68.89/10.15 | (72) all_76_2 = all_69_2 % 68.89/10.15 | % 68.89/10.15 | COMBINE_EQS: (71), (72) imply: % 68.89/10.15 | (73) all_72_15 = all_69_2 % 68.89/10.15 | % 68.89/10.15 | SIMP: (73) implies: % 68.89/10.15 | (74) all_72_15 = all_69_2 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (66), (72) imply: % 68.89/10.15 | (75) some(int, all_69_2) = all_76_1 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (52), (74) imply: % 68.89/10.15 | (76) some(int, all_69_2) = all_72_14 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (49), (74) imply: % 68.89/10.15 | (77) cons(int, all_69_2, all_72_1) = all_72_0 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (40), (74) imply: % 68.89/10.15 | (78) uni(all_69_2) % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (26) with all_69_1, all_76_1, all_69_2, int, % 68.89/10.15 | simplifying with (31), (75) gives: % 68.89/10.15 | (79) all_76_1 = all_69_1 % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (26) with all_72_14, all_76_1, all_69_2, int, % 68.89/10.15 | simplifying with (75), (76) gives: % 68.89/10.15 | (80) all_76_1 = all_72_14 % 68.89/10.15 | % 68.89/10.15 | COMBINE_EQS: (79), (80) imply: % 68.89/10.15 | (81) all_72_14 = all_69_1 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (67), (79) imply: % 68.89/10.15 | (82) tb2t(all_69_1) = all_76_0 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (53), (81) imply: % 68.89/10.15 | (83) tb2t(all_69_1) = all_72_13 % 68.89/10.15 | % 68.89/10.15 | REDUCE: (41), (81) imply: % 68.89/10.15 | (84) uni(all_69_1) % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (20) with all_69_0, all_76_0, all_69_1, simplifying % 68.89/10.15 | with (32), (82) gives: % 68.89/10.15 | (85) all_76_0 = all_69_0 % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (20) with all_72_13, all_76_0, all_69_1, % 68.89/10.15 | simplifying with (82), (83) gives: % 68.89/10.15 | (86) all_76_0 = all_72_13 % 68.89/10.15 | % 68.89/10.15 | COMBINE_EQS: (85), (86) imply: % 68.89/10.15 | (87) all_72_13 = all_69_0 % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (12) with int, all_66_0, simplifying with (15), % 68.89/10.15 | (28) gives: % 68.89/10.15 | (88) ? [v0: uni] : ? [v1: uni] : (tl(int, v0) = v1 & none(all_66_0) = v1 % 68.89/10.15 | & nil(int) = v0 & uni(v1) & uni(v0)) % 68.89/10.15 | % 68.89/10.15 | GROUND_INST: instantiating (1) with int, all_66_0, simplifying with (15), (28) % 68.89/10.15 | gives: % 68.89/10.16 | (89) ? [v0: uni] : (nil(int) = v0 & sort1(all_66_0, v0) = 0 & uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (13) with int, all_72_12, simplifying with (15), % 68.89/10.16 | (48) gives: % 68.89/10.16 | (90) ? [v0: uni] : ? [v1: ty] : (tl(int, all_72_12) = v0 & none(v1) = v0 % 68.89/10.16 | & list(int) = v1 & ty(v1) & uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (2) with int, all_72_12, simplifying with (15), % 68.89/10.16 | (48) gives: % 68.89/10.16 | (91) ? [v0: ty] : (list(int) = v0 & sort1(v0, all_72_12) = 0 & ty(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (14) with int, all_69_2, all_72_1, all_72_0, % 68.89/10.16 | simplifying with (15), (43), (77), (78) gives: % 68.89/10.16 | (92) ? [v0: uni] : ? [v1: ty] : (tl(int, all_72_0) = v0 & some(v1, % 68.89/10.16 | all_72_1) = v0 & list(int) = v1 & ty(v1) & uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (nil_Cons1) with int, all_69_2, all_72_1, all_72_0, % 68.89/10.16 | simplifying with (15), (43), (77), (78) gives: % 68.89/10.16 | (93) ? [v0: any] : ( ~ (v0 = all_72_0) & nil(int) = v0 & uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (11) with int, all_69_2, all_72_1, all_72_0, % 68.89/10.16 | simplifying with (15), (43), (77), (78) gives: % 68.89/10.16 | (94) ? [v0: uni] : (hd(int, all_72_0) = v0 & some(int, all_69_2) = v0 & % 68.89/10.16 | uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (3) with int, all_69_2, all_72_1, all_72_0, % 68.89/10.16 | simplifying with (15), (43), (77), (78) gives: % 68.89/10.16 | (95) ? [v0: int] : (length1(int, all_72_0) = v0 & length1(int, all_72_1) = % 68.89/10.16 | $sum(v0, -1)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (cons_sort3) with int, all_69_2, all_72_1, % 68.89/10.16 | all_72_0, simplifying with (15), (43), (77), (78) gives: % 68.89/10.16 | (96) ? [v0: ty] : (list(int) = v0 & sort1(v0, all_72_0) = 0 & ty(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (5) with int, all_72_5, $sum(all_72_6, all_72_8), % 68.89/10.16 | simplifying with (15), (42), (51) gives: % 68.89/10.16 | (97) $sum(all_72_6, all_72_8) = 0 | ? [v0: any] : ( ~ (v0 = all_72_5) & % 68.89/10.16 | nil(int) = v0 & uni(v0)) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (bridgeR) with all_69_1, all_69_0, simplifying with % 68.89/10.16 | (32), (84) gives: % 68.89/10.16 | (98) t2tb(all_69_0) = all_69_1 % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (36) with all_72_10, all_72_5, simplifying with % 68.89/10.16 | (45), (54) gives: % 68.89/10.16 | (99) ? [v0: int] : ? [v1: any] : ? [v2: int] : ? [v3: uni] : ? [v4: % 68.89/10.16 | int] : (no_zero1(all_72_10) = v1 & length1(int, all_72_5) = v0 & (v1 % 68.89/10.16 | = 0 | (v4 = all_69_0 & $lesseq(1, $difference(v0, v2)) & % 68.89/10.16 | $lesseq(0, v2) & tb2t(v3) = all_69_0 & nth1(int, v2, all_72_5) = % 68.89/10.16 | v3 & uni(v3)))) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (35) with all_72_10, all_72_5, simplifying with % 68.89/10.16 | (45), (54) gives: % 68.89/10.16 | (100) ? [v0: any] : ? [v1: int] : (no_zero1(all_72_10) = v0 & % 68.89/10.16 | length1(int, all_72_5) = v1 & ( ~ (v0 = 0) | ! [v2: int] : ! [v3: % 68.89/10.16 | uni] : ( ~ ($lesseq(1, $difference(v1, v2))) | ~ ($lesseq(0, % 68.89/10.16 | v2)) | ~ (nth1(int, v2, all_72_5) = v3) | ? [v4: any] : ( % 68.89/10.16 | ~ (v4 = all_69_0) & tb2t(v3) = v4 & option_int(v4))))) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (36) with all_72_9, all_72_7, simplifying with % 68.89/10.16 | (46), (55) gives: % 68.89/10.16 | (101) ? [v0: int] : ? [v1: any] : ? [v2: int] : ? [v3: uni] : ? [v4: % 68.89/10.16 | int] : (no_zero1(all_72_9) = v1 & length1(int, all_72_7) = v0 & (v1 % 68.89/10.16 | = 0 | (v4 = all_69_0 & $lesseq(1, $difference(v0, v2)) & % 68.89/10.16 | $lesseq(0, v2) & tb2t(v3) = all_69_0 & nth1(int, v2, all_72_7) % 68.89/10.16 | = v3 & uni(v3)))) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (35) with all_72_9, all_72_7, simplifying with % 68.89/10.16 | (46), (55) gives: % 68.89/10.16 | (102) ? [v0: any] : ? [v1: int] : (no_zero1(all_72_9) = v0 & length1(int, % 68.89/10.16 | all_72_7) = v1 & ( ~ (v0 = 0) | ! [v2: int] : ! [v3: uni] : ( ~ % 68.89/10.16 | ($lesseq(1, $difference(v1, v2))) | ~ ($lesseq(0, v2)) | ~ % 68.89/10.16 | (nth1(int, v2, all_72_7) = v3) | ? [v4: any] : ( ~ (v4 = % 68.89/10.16 | all_69_0) & tb2t(v3) = v4 & option_int(v4))))) % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (29) with all_72_2, all_72_1, simplifying with % 68.89/10.16 | (47), (56) gives: % 68.89/10.16 | (103) sort1(all_66_0, all_72_1) = 0 % 68.89/10.16 | % 68.89/10.16 | GROUND_INST: instantiating (36) with all_72_2, all_72_1, simplifying with % 68.89/10.16 | (47), (56) gives: % 68.89/10.17 | (104) ? [v0: int] : ? [v1: any] : ? [v2: int] : ? [v3: uni] : ? [v4: % 68.89/10.17 | int] : (no_zero1(all_72_2) = v1 & length1(int, all_72_1) = v0 & (v1 % 68.89/10.17 | = 0 | (v4 = all_69_0 & $lesseq(1, $difference(v0, v2)) & % 68.89/10.17 | $lesseq(0, v2) & tb2t(v3) = all_69_0 & nth1(int, v2, all_72_1) % 68.89/10.17 | = v3 & uni(v3)))) % 68.89/10.17 | % 68.89/10.17 | GROUND_INST: instantiating (35) with all_72_2, all_72_1, simplifying with % 68.89/10.17 | (47), (56) gives: % 68.89/10.17 | (105) ? [v0: any] : ? [v1: int] : (no_zero1(all_72_2) = v0 & length1(int, % 68.89/10.17 | all_72_1) = v1 & ( ~ (v0 = 0) | ! [v2: int] : ! [v3: uni] : ( ~ % 68.89/10.17 | ($lesseq(1, $difference(v1, v2))) | ~ ($lesseq(0, v2)) | ~ % 68.89/10.17 | (nth1(int, v2, all_72_1) = v3) | ? [v4: any] : ( ~ (v4 = % 68.89/10.17 | all_69_0) & tb2t(v3) = v4 & option_int(v4))))) % 68.89/10.17 | % 68.89/10.17 | GROUND_INST: instantiating (bridgeR1) with all_72_0, all_72_9, simplifying % 68.89/10.17 | with (44), (57) gives: % 68.89/10.17 | (106) t2tb1(all_72_9) = all_72_0 % 68.89/10.17 | % 68.89/10.17 | GROUND_INST: instantiating (69) with all_72_10, all_72_8, all_72_4, % 68.89/10.17 | simplifying with (45), (59) gives: % 68.89/10.17 | (107) all_72_4 = 0 | ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : ? % 68.89/10.17 | [v3: int] : ? [v4: uni] : ? [v5: int] : (t2tb1(all_72_10) = v0 & % 68.89/10.17 | tb2t(v1) = v2 & nth1(int, all_72_8, v0) = v1 & option_int(v2) & % 68.89/10.17 | uni(v1) & uni(v0) & ( ~ (v2 = all_76_0) | (v5 = all_76_0 & % 68.89/10.17 | $lesseq(1, $difference(all_72_8, v3)) & $lesseq(0, v3) & % 68.89/10.17 | tb2t(v4) = all_76_0 & nth1(int, v3, v0) = v4 & uni(v4)))) % 68.89/10.17 | % 68.89/10.17 | GROUND_INST: instantiating (37) with all_72_10, all_72_3, simplifying with % 68.89/10.17 | (45), (60) gives: % 68.89/10.17 | (108) all_72_3 = 0 | ? [v0: uni] : ? [v1: int] : ? [v2: int] : ? [v3: % 68.89/10.17 | uni] : ($lesseq(1, $difference(v1, v2)) & $lesseq(0, v2) & % 68.89/10.17 | t2tb1(all_72_10) = v0 & tb2t(v3) = all_69_0 & nth1(int, v2, v0) = % 68.89/10.17 | v3 & length1(int, v0) = v1 & uni(v3) & uni(v0)) % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (95) with fresh symbol all_103_0 gives: % 68.89/10.17 | (109) length1(int, all_72_0) = all_103_0 & length1(int, all_72_1) = % 68.89/10.17 | $sum(all_103_0, -1) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (109) implies: % 68.89/10.17 | (110) length1(int, all_72_1) = $sum(all_103_0, -1) % 68.89/10.17 | (111) length1(int, all_72_0) = all_103_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (93) with fresh symbol all_105_0 gives: % 68.89/10.17 | (112) ~ (all_105_0 = all_72_0) & nil(int) = all_105_0 & uni(all_105_0) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (112) implies: % 68.89/10.17 | (113) nil(int) = all_105_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (91) with fresh symbol all_107_0 gives: % 68.89/10.17 | (114) list(int) = all_107_0 & sort1(all_107_0, all_72_12) = 0 & % 68.89/10.17 | ty(all_107_0) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (114) implies: % 68.89/10.17 | (115) ty(all_107_0) % 68.89/10.17 | (116) list(int) = all_107_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (96) with fresh symbol all_111_0 gives: % 68.89/10.17 | (117) list(int) = all_111_0 & sort1(all_111_0, all_72_0) = 0 & % 68.89/10.17 | ty(all_111_0) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (117) implies: % 68.89/10.17 | (118) list(int) = all_111_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (94) with fresh symbol all_117_0 gives: % 68.89/10.17 | (119) hd(int, all_72_0) = all_117_0 & some(int, all_69_2) = all_117_0 & % 68.89/10.17 | uni(all_117_0) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (119) implies: % 68.89/10.17 | (120) some(int, all_69_2) = all_117_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (89) with fresh symbol all_119_0 gives: % 68.89/10.17 | (121) nil(int) = all_119_0 & sort1(all_66_0, all_119_0) = 0 & % 68.89/10.17 | uni(all_119_0) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (121) implies: % 68.89/10.17 | (122) nil(int) = all_119_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (92) with fresh symbols all_125_0, all_125_1 gives: % 68.89/10.17 | (123) tl(int, all_72_0) = all_125_1 & some(all_125_0, all_72_1) = all_125_1 % 68.89/10.17 | & list(int) = all_125_0 & ty(all_125_0) & uni(all_125_1) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (123) implies: % 68.89/10.17 | (124) list(int) = all_125_0 % 68.89/10.17 | (125) some(all_125_0, all_72_1) = all_125_1 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (88) with fresh symbols all_127_0, all_127_1 gives: % 68.89/10.17 | (126) tl(int, all_127_1) = all_127_0 & none(all_66_0) = all_127_0 & % 68.89/10.17 | nil(int) = all_127_1 & uni(all_127_0) & uni(all_127_1) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (126) implies: % 68.89/10.17 | (127) nil(int) = all_127_1 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (90) with fresh symbols all_129_0, all_129_1 gives: % 68.89/10.17 | (128) tl(int, all_72_12) = all_129_1 & none(all_129_0) = all_129_1 & % 68.89/10.17 | list(int) = all_129_0 & ty(all_129_0) & uni(all_129_1) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (128) implies: % 68.89/10.17 | (129) list(int) = all_129_0 % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (102) with fresh symbols all_133_0, all_133_1 gives: % 68.89/10.17 | (130) no_zero1(all_72_9) = all_133_1 & length1(int, all_72_7) = all_133_0 & % 68.89/10.17 | ( ~ (all_133_1 = 0) | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.17 | $difference(all_133_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 68.89/10.17 | (nth1(int, v0, all_72_7) = v1) | ? [v2: any] : ( ~ (v2 = % 68.89/10.17 | all_69_0) & tb2t(v1) = v2 & option_int(v2)))) % 68.89/10.17 | % 68.89/10.17 | ALPHA: (130) implies: % 68.89/10.17 | (131) length1(int, all_72_7) = all_133_0 % 68.89/10.17 | (132) no_zero1(all_72_9) = all_133_1 % 68.89/10.17 | (133) ~ (all_133_1 = 0) | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.17 | $difference(all_133_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 68.89/10.17 | (nth1(int, v0, all_72_7) = v1) | ? [v2: any] : ( ~ (v2 = all_69_0) % 68.89/10.17 | & tb2t(v1) = v2 & option_int(v2))) % 68.89/10.17 | % 68.89/10.17 | DELTA: instantiating (101) with fresh symbols all_135_0, all_135_1, all_135_2, % 68.89/10.17 | all_135_3, all_135_4 gives: % 68.89/10.18 | (134) no_zero1(all_72_9) = all_135_3 & length1(int, all_72_7) = all_135_4 & % 68.89/10.18 | (all_135_3 = 0 | (all_135_0 = all_69_0 & $lesseq(1, % 68.89/10.18 | $difference(all_135_4, all_135_2)) & $lesseq(0, all_135_2) & % 68.89/10.18 | tb2t(all_135_1) = all_69_0 & nth1(int, all_135_2, all_72_7) = % 68.89/10.18 | all_135_1 & uni(all_135_1))) % 68.89/10.18 | % 68.89/10.18 | ALPHA: (134) implies: % 68.89/10.18 | (135) length1(int, all_72_7) = all_135_4 % 68.89/10.18 | (136) no_zero1(all_72_9) = all_135_3 % 68.89/10.18 | (137) all_135_3 = 0 | (all_135_0 = all_69_0 & $lesseq(1, % 68.89/10.18 | $difference(all_135_4, all_135_2)) & $lesseq(0, all_135_2) & % 68.89/10.18 | tb2t(all_135_1) = all_69_0 & nth1(int, all_135_2, all_72_7) = % 68.89/10.18 | all_135_1 & uni(all_135_1)) % 68.89/10.18 | % 68.89/10.18 | DELTA: instantiating (105) with fresh symbols all_137_0, all_137_1 gives: % 68.89/10.18 | (138) no_zero1(all_72_2) = all_137_1 & length1(int, all_72_1) = all_137_0 & % 68.89/10.18 | ( ~ (all_137_1 = 0) | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.18 | $difference(all_137_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 68.89/10.18 | (nth1(int, v0, all_72_1) = v1) | ? [v2: any] : ( ~ (v2 = % 68.89/10.18 | all_69_0) & tb2t(v1) = v2 & option_int(v2)))) % 68.89/10.18 | % 68.89/10.18 | ALPHA: (138) implies: % 68.89/10.18 | (139) length1(int, all_72_1) = all_137_0 % 68.89/10.18 | % 68.89/10.18 | DELTA: instantiating (100) with fresh symbols all_139_0, all_139_1 gives: % 68.89/10.18 | (140) no_zero1(all_72_10) = all_139_1 & length1(int, all_72_5) = all_139_0 % 68.89/10.18 | & ( ~ (all_139_1 = 0) | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.18 | $difference(all_139_0, v0))) | ~ ($lesseq(0, v0)) | ~ % 68.89/10.18 | (nth1(int, v0, all_72_5) = v1) | ? [v2: any] : ( ~ (v2 = % 68.89/10.18 | all_69_0) & tb2t(v1) = v2 & option_int(v2)))) % 68.89/10.18 | % 68.89/10.18 | ALPHA: (140) implies: % 68.89/10.18 | (141) no_zero1(all_72_10) = all_139_1 % 68.89/10.18 | % 68.89/10.18 | DELTA: instantiating (104) with fresh symbols all_141_0, all_141_1, all_141_2, % 68.89/10.18 | all_141_3, all_141_4 gives: % 68.89/10.18 | (142) no_zero1(all_72_2) = all_141_3 & length1(int, all_72_1) = all_141_4 & % 68.89/10.18 | (all_141_3 = 0 | (all_141_0 = all_69_0 & $lesseq(1, % 68.89/10.18 | $difference(all_141_4, all_141_2)) & $lesseq(0, all_141_2) & % 68.89/10.18 | tb2t(all_141_1) = all_69_0 & nth1(int, all_141_2, all_72_1) = % 68.89/10.18 | all_141_1 & uni(all_141_1))) % 68.89/10.18 | % 68.89/10.18 | ALPHA: (142) implies: % 68.89/10.18 | (143) length1(int, all_72_1) = all_141_4 % 68.89/10.18 | % 68.89/10.18 | DELTA: instantiating (99) with fresh symbols all_143_0, all_143_1, all_143_2, % 68.89/10.18 | all_143_3, all_143_4 gives: % 68.89/10.18 | (144) no_zero1(all_72_10) = all_143_3 & length1(int, all_72_5) = all_143_4 % 68.89/10.18 | & (all_143_3 = 0 | (all_143_0 = all_69_0 & $lesseq(1, % 68.89/10.18 | $difference(all_143_4, all_143_2)) & $lesseq(0, all_143_2) & % 68.89/10.18 | tb2t(all_143_1) = all_69_0 & nth1(int, all_143_2, all_72_5) = % 68.89/10.18 | all_143_1 & uni(all_143_1))) % 68.89/10.18 | % 68.89/10.18 | ALPHA: (144) implies: % 68.89/10.18 | (145) no_zero1(all_72_10) = all_143_3 % 68.89/10.18 | (146) all_143_3 = 0 | (all_143_0 = all_69_0 & $lesseq(1, % 68.89/10.18 | $difference(all_143_4, all_143_2)) & $lesseq(0, all_143_2) & % 68.89/10.18 | tb2t(all_143_1) = all_69_0 & nth1(int, all_143_2, all_72_5) = % 68.89/10.18 | all_143_1 & uni(all_143_1)) % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (17) with all_107_0, all_125_0, int, simplifying % 68.89/10.18 | with (116), (124) gives: % 68.89/10.18 | (147) all_125_0 = all_107_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (17) with all_66_0, all_129_0, int, simplifying % 68.89/10.18 | with (28), (129) gives: % 68.89/10.18 | (148) all_129_0 = all_66_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (17) with all_125_0, all_129_0, int, simplifying % 68.89/10.18 | with (124), (129) gives: % 68.89/10.18 | (149) all_129_0 = all_125_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (17) with all_111_0, all_129_0, int, simplifying % 68.89/10.18 | with (118), (129) gives: % 68.89/10.18 | (150) all_129_0 = all_111_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (18) with all_72_12, all_127_1, int, simplifying % 68.89/10.18 | with (48), (127) gives: % 68.89/10.18 | (151) all_127_1 = all_72_12 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (18) with all_119_0, all_127_1, int, simplifying % 68.89/10.18 | with (122), (127) gives: % 68.89/10.18 | (152) all_127_1 = all_119_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (18) with all_105_0, all_127_1, int, simplifying % 68.89/10.18 | with (113), (127) gives: % 68.89/10.18 | (153) all_127_1 = all_105_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (25) with all_133_0, all_135_4, all_72_7, int, % 68.89/10.18 | simplifying with (131), (135) gives: % 68.89/10.18 | (154) all_135_4 = all_133_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (25) with all_72_6, all_135_4, all_72_7, int, % 68.89/10.18 | simplifying with (50), (135) gives: % 68.89/10.18 | (155) all_135_4 = all_72_6 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (25) with all_137_0, all_141_4, all_72_1, int, % 68.89/10.18 | simplifying with (139), (143) gives: % 68.89/10.18 | (156) all_141_4 = all_137_0 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (25) with $sum(all_103_0, -1), all_141_4, all_72_1, % 68.89/10.18 | int, simplifying with (110), (143) gives: % 68.89/10.18 | (157) $difference(all_141_4, all_103_0) = -1 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (26) with all_69_1, all_117_0, all_69_2, int, % 68.89/10.18 | simplifying with (31), (120) gives: % 68.89/10.18 | (158) all_117_0 = all_69_1 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (21) with all_72_7, all_72_0, all_72_9, simplifying % 68.89/10.18 | with (55), (106) gives: % 68.89/10.18 | (159) all_72_0 = all_72_7 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (23) with all_72_3, all_143_3, all_72_10, % 68.89/10.18 | simplifying with (60), (145) gives: % 68.89/10.18 | (160) all_143_3 = all_72_3 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (23) with all_139_1, all_143_3, all_72_10, % 68.89/10.18 | simplifying with (141), (145) gives: % 68.89/10.18 | (161) all_143_3 = all_139_1 % 68.89/10.18 | % 68.89/10.18 | GROUND_INST: instantiating (23) with all_133_1, all_135_3, all_72_9, % 68.89/10.18 | simplifying with (132), (136) gives: % 68.89/10.18 | (162) all_135_3 = all_133_1 % 68.89/10.18 | % 68.89/10.18 | COMBINE_EQS: (160), (161) imply: % 68.89/10.18 | (163) all_139_1 = all_72_3 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (156), (157) imply: % 68.89/10.19 | (164) $difference(all_137_0, all_103_0) = -1 % 68.89/10.19 | % 68.89/10.19 | SIMP: (164) implies: % 68.89/10.19 | (165) $difference(all_137_0, all_103_0) = -1 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (154), (155) imply: % 68.89/10.19 | (166) all_133_0 = all_72_6 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (148), (150) imply: % 68.89/10.19 | (167) all_111_0 = all_66_0 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (149), (150) imply: % 68.89/10.19 | (168) all_125_0 = all_111_0 % 68.89/10.19 | % 68.89/10.19 | SIMP: (168) implies: % 68.89/10.19 | (169) all_125_0 = all_111_0 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (151), (152) imply: % 68.89/10.19 | (170) all_119_0 = all_72_12 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (152), (153) imply: % 68.89/10.19 | (171) all_119_0 = all_105_0 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (147), (169) imply: % 68.89/10.19 | (172) all_111_0 = all_107_0 % 68.89/10.19 | % 68.89/10.19 | SIMP: (172) implies: % 68.89/10.19 | (173) all_111_0 = all_107_0 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (170), (171) imply: % 68.89/10.19 | (174) all_105_0 = all_72_12 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (167), (173) imply: % 68.89/10.19 | (175) all_107_0 = all_66_0 % 68.89/10.19 | % 68.89/10.19 | SIMP: (175) implies: % 68.89/10.19 | (176) all_107_0 = all_66_0 % 68.89/10.19 | % 68.89/10.19 | COMBINE_EQS: (147), (176) imply: % 68.89/10.19 | (177) all_125_0 = all_66_0 % 68.89/10.19 | % 68.89/10.19 | REDUCE: (125), (177) imply: % 68.89/10.19 | (178) some(all_66_0, all_72_1) = all_125_1 % 68.89/10.19 | % 68.89/10.19 | REDUCE: (111), (159) imply: % 68.89/10.19 | (179) length1(int, all_72_7) = all_103_0 % 68.89/10.19 | % 68.89/10.19 | REDUCE: (77), (159) imply: % 68.89/10.19 | (180) cons(int, all_69_2, all_72_1) = all_72_7 % 68.89/10.19 | % 68.89/10.19 | REDUCE: (115), (176) imply: % 68.89/10.19 | (181) ty(all_66_0) % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (25) with all_72_6, all_103_0, all_72_7, int, % 68.89/10.19 | simplifying with (50), (179) gives: % 68.89/10.19 | (182) all_103_0 = all_72_6 % 68.89/10.19 | % 68.89/10.19 | REDUCE: (110), (182) imply: % 68.89/10.19 | (183) length1(int, all_72_1) = $sum(all_72_6, -1) % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (4) with int, all_72_1, simplifying with (15), (43) % 68.89/10.19 | gives: % 68.89/10.19 | (184) ~ (length1(int, all_72_1) = 0) | nil(int) = all_72_1 % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (5) with int, all_72_1, $sum(all_72_6, -1), % 68.89/10.19 | simplifying with (15), (43), (183) gives: % 68.89/10.19 | (185) all_72_6 = 1 | ? [v0: any] : ( ~ (v0 = all_72_1) & nil(int) = v0 & % 68.89/10.19 | uni(v0)) % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (length_nonnegative) with int, all_72_1, % 68.89/10.19 | $sum(all_72_6, -1), simplifying with (15), (43), (183) gives: % 68.89/10.19 | (186) $lesseq(1, all_72_6) % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (6) with all_66_0, all_72_1, all_125_1, simplifying % 68.89/10.19 | with (43), (178), (181) gives: % 68.89/10.19 | (187) ? [v0: any] : ? [v1: uni] : (some_proj_11(all_66_0, all_125_1) = v1 % 68.89/10.19 | & sort1(all_66_0, all_72_1) = v0 & uni(v1) & ( ~ (v0 = 0) | v1 = % 68.89/10.19 | all_72_1)) % 68.89/10.19 | % 68.89/10.19 | GROUND_INST: instantiating (37) with all_72_9, all_133_1, simplifying with % 68.89/10.19 | (46), (132) gives: % 68.89/10.19 | (188) all_133_1 = 0 | ? [v0: uni] : ? [v1: int] : ? [v2: int] : ? [v3: % 68.89/10.19 | uni] : ($lesseq(1, $difference(v1, v2)) & $lesseq(0, v2) & % 68.89/10.19 | t2tb1(all_72_9) = v0 & tb2t(v3) = all_69_0 & nth1(int, v2, v0) = v3 % 68.89/10.19 | & length1(int, v0) = v1 & uni(v3) & uni(v0)) % 68.89/10.19 | % 68.89/10.19 | DELTA: instantiating (187) with fresh symbols all_206_0, all_206_1 gives: % 68.89/10.19 | (189) some_proj_11(all_66_0, all_125_1) = all_206_0 & sort1(all_66_0, % 68.89/10.19 | all_72_1) = all_206_1 & uni(all_206_0) & ( ~ (all_206_1 = 0) | % 68.89/10.19 | all_206_0 = all_72_1) % 68.89/10.19 | % 68.89/10.19 | ALPHA: (189) implies: % 68.89/10.19 | (190) uni(all_206_0) % 68.89/10.19 | (191) sort1(all_66_0, all_72_1) = all_206_1 % 68.89/10.19 | (192) ~ (all_206_1 = 0) | all_206_0 = all_72_1 % 68.89/10.19 | % 68.89/10.19 | BETA: splitting (61) gives: % 68.89/10.19 | % 68.89/10.19 | Case 1: % 68.89/10.19 | | % 68.89/10.19 | | (193) ~ (all_72_4 = 0) % 68.89/10.19 | | % 68.89/10.19 | | BETA: splitting (97) gives: % 68.89/10.19 | | % 68.89/10.19 | | Case 1: % 68.89/10.19 | | | % 68.89/10.19 | | | (194) $sum(all_72_6, all_72_8) = 0 % 68.89/10.19 | | | % 68.89/10.19 | | | REDUCE: (186), (194) imply: % 68.89/10.19 | | | (195) $lesseq(all_72_8, -1) % 68.89/10.19 | | | % 68.89/10.19 | | | COMBINE_INEQS: (39), (195) imply: % 68.89/10.19 | | | (196) $false % 68.89/10.20 | | | % 68.89/10.20 | | | CLOSE: (196) is inconsistent. % 68.89/10.20 | | | % 68.89/10.20 | | Case 2: % 68.89/10.20 | | | % 68.89/10.20 | | | (197) ? [v0: any] : ( ~ (v0 = all_72_5) & nil(int) = v0 & uni(v0)) % 68.89/10.20 | | | % 68.89/10.20 | | | DELTA: instantiating (197) with fresh symbol all_228_0 gives: % 68.89/10.20 | | | (198) ~ (all_228_0 = all_72_5) & nil(int) = all_228_0 & uni(all_228_0) % 68.89/10.20 | | | % 68.89/10.20 | | | ALPHA: (198) implies: % 68.89/10.20 | | | (199) nil(int) = all_228_0 % 68.89/10.20 | | | % 68.89/10.20 | | | BETA: splitting (107) gives: % 68.89/10.20 | | | % 68.89/10.20 | | | Case 1: % 68.89/10.20 | | | | % 68.89/10.20 | | | | (200) all_72_4 = 0 % 68.89/10.20 | | | | % 68.89/10.20 | | | | REDUCE: (193), (200) imply: % 68.89/10.20 | | | | (201) $false % 68.89/10.20 | | | | % 68.89/10.20 | | | | CLOSE: (201) is inconsistent. % 68.89/10.20 | | | | % 68.89/10.20 | | | Case 2: % 68.89/10.20 | | | | % 68.89/10.20 | | | | (202) ? [v0: uni] : ? [v1: uni] : ? [v2: option_int] : ? [v3: % 68.89/10.20 | | | | int] : ? [v4: uni] : ? [v5: int] : (t2tb1(all_72_10) = v0 & % 68.89/10.20 | | | | tb2t(v1) = v2 & nth1(int, all_72_8, v0) = v1 & option_int(v2) % 68.89/10.20 | | | | & uni(v1) & uni(v0) & ( ~ (v2 = all_76_0) | (v5 = all_76_0 & % 68.89/10.20 | | | | $lesseq(1, $difference(all_72_8, v3)) & $lesseq(0, v3) & % 68.89/10.20 | | | | tb2t(v4) = all_76_0 & nth1(int, v3, v0) = v4 & uni(v4)))) % 68.89/10.20 | | | | % 68.89/10.20 | | | | DELTA: instantiating (202) with fresh symbols all_235_0, all_235_1, % 68.89/10.20 | | | | all_235_2, all_235_3, all_235_4, all_235_5 gives: % 68.89/10.20 | | | | (203) t2tb1(all_72_10) = all_235_5 & tb2t(all_235_4) = all_235_3 & % 68.89/10.20 | | | | nth1(int, all_72_8, all_235_5) = all_235_4 & % 68.89/10.20 | | | | option_int(all_235_3) & uni(all_235_4) & uni(all_235_5) & ( ~ % 68.89/10.20 | | | | (all_235_3 = all_76_0) | (all_235_0 = all_76_0 & $lesseq(1, % 68.89/10.20 | | | | $difference(all_72_8, all_235_2)) & $lesseq(0, all_235_2) % 68.89/10.20 | | | | & tb2t(all_235_1) = all_76_0 & nth1(int, all_235_2, % 68.89/10.20 | | | | all_235_5) = all_235_1 & uni(all_235_1))) % 68.89/10.20 | | | | % 68.89/10.20 | | | | ALPHA: (203) implies: % 68.89/10.20 | | | | (204) uni(all_235_4) % 68.89/10.20 | | | | (205) nth1(int, all_72_8, all_235_5) = all_235_4 % 68.89/10.20 | | | | (206) tb2t(all_235_4) = all_235_3 % 68.89/10.20 | | | | (207) t2tb1(all_72_10) = all_235_5 % 68.89/10.20 | | | | (208) ~ (all_235_3 = all_76_0) | (all_235_0 = all_76_0 & $lesseq(1, % 68.89/10.20 | | | | $difference(all_72_8, all_235_2)) & $lesseq(0, all_235_2) & % 68.89/10.20 | | | | tb2t(all_235_1) = all_76_0 & nth1(int, all_235_2, all_235_5) % 68.89/10.20 | | | | = all_235_1 & uni(all_235_1)) % 68.89/10.20 | | | | % 68.89/10.20 | | | | GROUND_INST: instantiating (24) with 0, all_206_1, all_72_1, all_66_0, % 68.89/10.20 | | | | simplifying with (103), (191) gives: % 68.89/10.20 | | | | (209) all_206_1 = 0 % 68.89/10.20 | | | | % 68.89/10.20 | | | | GROUND_INST: instantiating (18) with all_72_12, all_228_0, int, % 68.89/10.20 | | | | simplifying with (48), (199) gives: % 68.89/10.20 | | | | (210) all_228_0 = all_72_12 % 68.89/10.20 | | | | % 68.89/10.20 | | | | GROUND_INST: instantiating (21) with all_72_5, all_235_5, all_72_10, % 68.89/10.20 | | | | simplifying with (54), (207) gives: % 68.89/10.20 | | | | (211) all_235_5 = all_72_5 % 68.89/10.20 | | | | % 68.89/10.20 | | | | REDUCE: (205), (211) imply: % 68.89/10.20 | | | | (212) nth1(int, all_72_8, all_72_5) = all_235_4 % 68.89/10.20 | | | | % 68.89/10.20 | | | | BETA: splitting (192) gives: % 68.89/10.20 | | | | % 68.89/10.20 | | | | Case 1: % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | (213) ~ (all_206_1 = 0) % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | REDUCE: (209), (213) imply: % 68.89/10.20 | | | | | (214) $false % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | CLOSE: (214) is inconsistent. % 68.89/10.20 | | | | | % 68.89/10.20 | | | | Case 2: % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | (215) all_206_0 = all_72_1 % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | GROUND_INST: instantiating (63) with 0, all_235_4, simplifying with % 68.89/10.20 | | | | | (212) gives: % 68.89/10.20 | | | | | (216) ? [v0: uni] : ? [v1: option_int] : (tb2t(v0) = v1 & % 68.89/10.20 | | | | | tb2t(all_235_4) = v1 & nth1(int, 0, all_72_7) = v0 & % 68.89/10.20 | | | | | option_int(v1) & uni(v0)) % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | GROUND_INST: instantiating (bridgeR) with all_235_4, all_235_3, % 68.89/10.20 | | | | | simplifying with (204), (206) gives: % 68.89/10.20 | | | | | (217) t2tb(all_235_3) = all_235_4 % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | DELTA: instantiating (216) with fresh symbols all_329_0, all_329_1 % 68.89/10.20 | | | | | gives: % 68.89/10.20 | | | | | (218) tb2t(all_329_1) = all_329_0 & tb2t(all_235_4) = all_329_0 & % 68.89/10.20 | | | | | nth1(int, 0, all_72_7) = all_329_1 & option_int(all_329_0) & % 68.89/10.20 | | | | | uni(all_329_1) % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | ALPHA: (218) implies: % 68.89/10.20 | | | | | (219) nth1(int, 0, all_72_7) = all_329_1 % 68.89/10.20 | | | | | (220) tb2t(all_235_4) = all_329_0 % 68.89/10.20 | | | | | (221) tb2t(all_329_1) = all_329_0 % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | GROUND_INST: instantiating (20) with all_235_3, all_329_0, all_235_4, % 68.89/10.20 | | | | | simplifying with (206), (220) gives: % 68.89/10.20 | | | | | (222) all_329_0 = all_235_3 % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | REDUCE: (221), (222) imply: % 68.89/10.20 | | | | | (223) tb2t(all_329_1) = all_235_3 % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | BETA: splitting (108) gives: % 68.89/10.20 | | | | | % 68.89/10.20 | | | | | Case 1: % 68.89/10.20 | | | | | | % 68.89/10.20 | | | | | | (224) all_72_3 = 0 % 68.89/10.20 | | | | | | % 68.89/10.20 | | | | | | REDUCE: (60), (224) imply: % 68.89/10.20 | | | | | | (225) no_zero1(all_72_10) = 0 % 68.89/10.20 | | | | | | % 68.89/10.20 | | | | | | BETA: splitting (184) gives: % 68.89/10.20 | | | | | | % 68.89/10.20 | | | | | | Case 1: % 68.89/10.20 | | | | | | | % 68.89/10.20 | | | | | | | (226) ~ (length1(int, all_72_1) = 0) % 68.89/10.20 | | | | | | | % 68.89/10.20 | | | | | | | PRED_UNIFY: (183), (226) imply: % 68.89/10.20 | | | | | | | (227) ~ (all_72_6 = 1) % 68.89/10.20 | | | | | | | % 68.89/10.20 | | | | | | | STRENGTHEN: (186), (227) imply: % 68.89/10.20 | | | | | | | (228) $lesseq(2, all_72_6) % 68.89/10.20 | | | | | | | % 68.89/10.20 | | | | | | | BETA: splitting (185) gives: % 68.89/10.20 | | | | | | | % 68.89/10.20 | | | | | | | Case 1: % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | (229) all_72_6 = 1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | REDUCE: (228), (229) imply: % 68.89/10.20 | | | | | | | | (230) $false % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | CLOSE: (230) is inconsistent. % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | Case 2: % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (7) with int, all_69_2, all_72_1, % 68.89/10.20 | | | | | | | | all_72_7, all_329_1, simplifying with (15), (43), % 68.89/10.20 | | | | | | | | (78), (180), (219) gives: % 68.89/10.20 | | | | | | | | (231) some(int, all_69_2) = all_329_1 & uni(all_329_1) % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | ALPHA: (231) implies: % 68.89/10.20 | | | | | | | | (232) uni(all_329_1) % 68.89/10.20 | | | | | | | | (233) some(int, all_69_2) = all_329_1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_329_1, all_235_3, % 68.89/10.20 | | | | | | | | simplifying with (223), (232) gives: % 68.89/10.20 | | | | | | | | (234) t2tb(all_235_3) = all_329_1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (34) with all_72_10, simplifying with % 68.89/10.20 | | | | | | | | (45), (225) gives: % 68.89/10.20 | | | | | | | | (235) ? [v0: uni] : ? [v1: int] : (t2tb1(all_72_10) = v0 & % 68.89/10.20 | | | | | | | | length1(int, v0) = v1 & uni(v0) & ! [v2: int] : ! % 68.89/10.20 | | | | | | | | [v3: uni] : ( ~ ($lesseq(1, $difference(v1, v2))) | % 68.89/10.20 | | | | | | | | ~ ($lesseq(0, v2)) | ~ (nth1(int, v2, v0) = v3) | % 68.89/10.20 | | | | | | | | ? [v4: any] : ( ~ (v4 = all_69_0) & tb2t(v3) = v4 & % 68.89/10.20 | | | | | | | | option_int(v4)))) % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | DELTA: instantiating (235) with fresh symbols all_575_0, % 68.89/10.20 | | | | | | | | all_575_1 gives: % 68.89/10.20 | | | | | | | | (236) t2tb1(all_72_10) = all_575_1 & length1(int, all_575_1) % 68.89/10.20 | | | | | | | | = all_575_0 & uni(all_575_1) & ! [v0: int] : ! [v1: % 68.89/10.20 | | | | | | | | uni] : ( ~ ($lesseq(1, $difference(all_575_0, v0))) | % 68.89/10.20 | | | | | | | | ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, all_575_1) = % 68.89/10.20 | | | | | | | | v1) | ? [v2: any] : ( ~ (v2 = all_69_0) & tb2t(v1) % 68.89/10.20 | | | | | | | | = v2 & option_int(v2))) % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | ALPHA: (236) implies: % 68.89/10.20 | | | | | | | | (237) t2tb1(all_72_10) = all_575_1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (26) with all_69_1, all_329_1, % 68.89/10.20 | | | | | | | | all_69_2, int, simplifying with (31), (233) gives: % 68.89/10.20 | | | | | | | | (238) all_329_1 = all_69_1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (19) with all_235_4, all_329_1, % 68.89/10.20 | | | | | | | | all_235_3, simplifying with (217), (234) gives: % 68.89/10.20 | | | | | | | | (239) all_329_1 = all_235_4 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | GROUND_INST: instantiating (21) with all_72_5, all_575_1, % 68.89/10.20 | | | | | | | | all_72_10, simplifying with (54), (237) gives: % 68.89/10.20 | | | | | | | | (240) all_575_1 = all_72_5 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | COMBINE_EQS: (238), (239) imply: % 68.89/10.20 | | | | | | | | (241) all_235_4 = all_69_1 % 68.89/10.20 | | | | | | | | % 68.89/10.20 | | | | | | | | REDUCE: (206), (241) imply: % 68.89/10.20 | | | | | | | | (242) tb2t(all_69_1) = all_235_3 % 68.89/10.20 | | | | | | | | % 68.89/10.21 | | | | | | | | REF_CLOSE: (20), (32), (45), (54), (64), (70), (85), (87), % 68.89/10.21 | | | | | | | | (208), (211), (242) are inconsistent by sub-proof #1. % 68.89/10.21 | | | | | | | | % 68.89/10.21 | | | | | | | End of split % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | Case 2: % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | (243) nil(int) = all_72_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (18) with all_72_12, all_72_1, int, % 68.89/10.21 | | | | | | | simplifying with (48), (243) gives: % 68.89/10.21 | | | | | | | (244) all_72_1 = all_72_12 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | REDUCE: (180), (244) imply: % 68.89/10.21 | | | | | | | (245) cons(int, all_69_2, all_72_12) = all_72_7 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | REDUCE: (43), (244) imply: % 68.89/10.21 | | | | | | | (246) uni(all_72_12) % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (7) with int, all_69_2, all_72_12, % 68.89/10.21 | | | | | | | all_72_7, all_329_1, simplifying with (15), (78), % 68.89/10.21 | | | | | | | (219), (245), (246) gives: % 68.89/10.21 | | | | | | | (247) some(int, all_69_2) = all_329_1 & uni(all_329_1) % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | ALPHA: (247) implies: % 68.89/10.21 | | | | | | | (248) uni(all_329_1) % 68.89/10.21 | | | | | | | (249) some(int, all_69_2) = all_329_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (bridgeR) with all_329_1, all_235_3, % 68.89/10.21 | | | | | | | simplifying with (223), (248) gives: % 68.89/10.21 | | | | | | | (250) t2tb(all_235_3) = all_329_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (34) with all_72_10, simplifying with % 68.89/10.21 | | | | | | | (45), (225) gives: % 68.89/10.21 | | | | | | | (251) ? [v0: uni] : ? [v1: int] : (t2tb1(all_72_10) = v0 & % 68.89/10.21 | | | | | | | length1(int, v0) = v1 & uni(v0) & ! [v2: int] : ! % 68.89/10.21 | | | | | | | [v3: uni] : ( ~ ($lesseq(1, $difference(v1, v2))) | ~ % 68.89/10.21 | | | | | | | ($lesseq(0, v2)) | ~ (nth1(int, v2, v0) = v3) | ? % 68.89/10.21 | | | | | | | [v4: any] : ( ~ (v4 = all_69_0) & tb2t(v3) = v4 & % 68.89/10.21 | | | | | | | option_int(v4)))) % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | DELTA: instantiating (251) with fresh symbols all_554_0, all_554_1 % 68.89/10.21 | | | | | | | gives: % 68.89/10.21 | | | | | | | (252) t2tb1(all_72_10) = all_554_1 & length1(int, all_554_1) = % 68.89/10.21 | | | | | | | all_554_0 & uni(all_554_1) & ! [v0: int] : ! [v1: uni] % 68.89/10.21 | | | | | | | : ( ~ ($lesseq(1, $difference(all_554_0, v0))) | ~ % 68.89/10.21 | | | | | | | ($lesseq(0, v0)) | ~ (nth1(int, v0, all_554_1) = v1) | % 68.89/10.21 | | | | | | | ? [v2: any] : ( ~ (v2 = all_69_0) & tb2t(v1) = v2 & % 68.89/10.21 | | | | | | | option_int(v2))) % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | ALPHA: (252) implies: % 68.89/10.21 | | | | | | | (253) t2tb1(all_72_10) = all_554_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (26) with all_69_1, all_329_1, % 68.89/10.21 | | | | | | | all_69_2, int, simplifying with (31), (249) gives: % 68.89/10.21 | | | | | | | (254) all_329_1 = all_69_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (19) with all_235_4, all_329_1, % 68.89/10.21 | | | | | | | all_235_3, simplifying with (217), (250) gives: % 68.89/10.21 | | | | | | | (255) all_329_1 = all_235_4 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (21) with all_72_5, all_554_1, % 68.89/10.21 | | | | | | | all_72_10, simplifying with (54), (253) gives: % 68.89/10.21 | | | | | | | (256) all_554_1 = all_72_5 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | COMBINE_EQS: (254), (255) imply: % 68.89/10.21 | | | | | | | (257) all_235_4 = all_69_1 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | REDUCE: (206), (257) imply: % 68.89/10.21 | | | | | | | (258) tb2t(all_69_1) = all_235_3 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | REF_CLOSE: (20), (32), (45), (54), (64), (70), (85), (87), (208), % 68.89/10.21 | | | | | | | (211), (258) are inconsistent by sub-proof #1. % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | End of split % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | Case 2: % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | | (259) ~ (all_72_3 = 0) % 68.89/10.21 | | | | | | (260) ? [v0: uni] : ? [v1: int] : ? [v2: int] : ? [v3: uni] : % 68.89/10.21 | | | | | | ($lesseq(1, $difference(v1, v2)) & $lesseq(0, v2) & % 68.89/10.21 | | | | | | t2tb1(all_72_10) = v0 & tb2t(v3) = all_69_0 & nth1(int, % 68.89/10.21 | | | | | | v2, v0) = v3 & length1(int, v0) = v1 & uni(v3) & % 68.89/10.21 | | | | | | uni(v0)) % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | | DELTA: instantiating (260) with fresh symbols all_392_0, all_392_1, % 68.89/10.21 | | | | | | all_392_2, all_392_3 gives: % 68.89/10.21 | | | | | | (261) $lesseq(1, $difference(all_392_2, all_392_1)) & $lesseq(0, % 68.89/10.21 | | | | | | all_392_1) & t2tb1(all_72_10) = all_392_3 & % 68.89/10.21 | | | | | | tb2t(all_392_0) = all_69_0 & nth1(int, all_392_1, % 68.89/10.21 | | | | | | all_392_3) = all_392_0 & length1(int, all_392_3) = % 68.89/10.21 | | | | | | all_392_2 & uni(all_392_0) & uni(all_392_3) % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | | ALPHA: (261) implies: % 68.89/10.21 | | | | | | (262) uni(all_392_0) % 68.89/10.21 | | | | | | (263) tb2t(all_392_0) = all_69_0 % 68.89/10.21 | | | | | | (264) t2tb1(all_72_10) = all_392_3 % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | | BETA: splitting (146) gives: % 68.89/10.21 | | | | | | % 68.89/10.21 | | | | | | Case 1: % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | (265) all_143_3 = 0 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | COMBINE_EQS: (160), (265) imply: % 68.89/10.21 | | | | | | | (266) all_72_3 = 0 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | REDUCE: (259), (266) imply: % 68.89/10.21 | | | | | | | (267) $false % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | CLOSE: (267) is inconsistent. % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | Case 2: % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | (268) all_143_0 = all_69_0 & $lesseq(1, $difference(all_143_4, % 68.89/10.21 | | | | | | | all_143_2)) & $lesseq(0, all_143_2) & tb2t(all_143_1) % 68.89/10.21 | | | | | | | = all_69_0 & nth1(int, all_143_2, all_72_5) = all_143_1 & % 68.89/10.21 | | | | | | | uni(all_143_1) % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | ALPHA: (268) implies: % 68.89/10.21 | | | | | | | (269) uni(all_143_1) % 68.89/10.21 | | | | | | | (270) tb2t(all_143_1) = all_69_0 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | GROUND_INST: instantiating (21) with all_72_5, all_392_3, % 68.89/10.21 | | | | | | | all_72_10, simplifying with (54), (264) gives: % 68.89/10.21 | | | | | | | (271) all_392_3 = all_72_5 % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | BETA: splitting (133) gives: % 68.89/10.21 | | | | | | | % 68.89/10.21 | | | | | | | Case 1: % 68.89/10.21 | | | | | | | | % 68.89/10.21 | | | | | | | | (272) ~ (all_133_1 = 0) % 68.89/10.21 | | | | | | | | % 68.89/10.21 | | | | | | | | BETA: splitting (137) gives: % 68.89/10.21 | | | | | | | | % 68.89/10.21 | | | | | | | | Case 1: % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | (273) all_135_3 = 0 % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | COMBINE_EQS: (162), (273) imply: % 68.89/10.21 | | | | | | | | | (274) all_133_1 = 0 % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | SIMP: (274) implies: % 68.89/10.21 | | | | | | | | | (275) all_133_1 = 0 % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | REDUCE: (272), (275) imply: % 68.89/10.21 | | | | | | | | | (276) $false % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | CLOSE: (276) is inconsistent. % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | Case 2: % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | (277) ~ (all_135_3 = 0) % 68.89/10.21 | | | | | | | | | (278) all_135_0 = all_69_0 & $lesseq(1, % 68.89/10.21 | | | | | | | | | $difference(all_135_4, all_135_2)) & $lesseq(0, % 68.89/10.21 | | | | | | | | | all_135_2) & tb2t(all_135_1) = all_69_0 & nth1(int, % 68.89/10.21 | | | | | | | | | all_135_2, all_72_7) = all_135_1 & uni(all_135_1) % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | ALPHA: (278) implies: % 68.89/10.21 | | | | | | | | | (279) uni(all_135_1) % 68.89/10.21 | | | | | | | | | (280) tb2t(all_135_1) = all_69_0 % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | BETA: splitting (188) gives: % 68.89/10.21 | | | | | | | | | % 68.89/10.21 | | | | | | | | | Case 1: % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | (281) all_133_1 = 0 % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | REDUCE: (272), (281) imply: % 68.89/10.21 | | | | | | | | | | (282) $false % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | CLOSE: (282) is inconsistent. % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | Case 2: % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | (283) ? [v0: uni] : ? [v1: int] : ? [v2: int] : ? % 68.89/10.21 | | | | | | | | | | [v3: uni] : ($lesseq(1, $difference(v1, v2)) & % 68.89/10.21 | | | | | | | | | | $lesseq(0, v2) & t2tb1(all_72_9) = v0 & tb2t(v3) % 68.89/10.21 | | | | | | | | | | = all_69_0 & nth1(int, v2, v0) = v3 & % 68.89/10.21 | | | | | | | | | | length1(int, v0) = v1 & uni(v3) & uni(v0)) % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | DELTA: instantiating (283) with fresh symbols all_429_0, % 68.89/10.21 | | | | | | | | | | all_429_1, all_429_2, all_429_3 gives: % 68.89/10.21 | | | | | | | | | | (284) $lesseq(1, $difference(all_429_2, all_429_1)) & % 68.89/10.21 | | | | | | | | | | $lesseq(0, all_429_1) & t2tb1(all_72_9) = all_429_3 % 68.89/10.21 | | | | | | | | | | & tb2t(all_429_0) = all_69_0 & nth1(int, all_429_1, % 68.89/10.21 | | | | | | | | | | all_429_3) = all_429_0 & length1(int, all_429_3) % 68.89/10.21 | | | | | | | | | | = all_429_2 & uni(all_429_0) & uni(all_429_3) % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | ALPHA: (284) implies: % 68.89/10.21 | | | | | | | | | | (285) $lesseq(0, all_429_1) % 68.89/10.21 | | | | | | | | | | (286) uni(all_429_0) % 68.89/10.21 | | | | | | | | | | (287) nth1(int, all_429_1, all_429_3) = all_429_0 % 68.89/10.21 | | | | | | | | | | (288) tb2t(all_429_0) = all_69_0 % 68.89/10.21 | | | | | | | | | | (289) t2tb1(all_72_9) = all_429_3 % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | GROUND_INST: instantiating (21) with all_72_7, all_429_3, % 68.89/10.21 | | | | | | | | | | all_72_9, simplifying with (55), (289) gives: % 68.89/10.21 | | | | | | | | | | (290) all_429_3 = all_72_7 % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | REDUCE: (287), (290) imply: % 68.89/10.21 | | | | | | | | | | (291) nth1(int, all_429_1, all_72_7) = all_429_0 % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | GROUND_INST: instantiating (7) with int, all_69_2, all_72_1, % 68.89/10.21 | | | | | | | | | | all_72_7, all_329_1, simplifying with (15), (43), % 68.89/10.21 | | | | | | | | | | (78), (180), (219) gives: % 68.89/10.21 | | | | | | | | | | (292) some(int, all_69_2) = all_329_1 & uni(all_329_1) % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | ALPHA: (292) implies: % 68.89/10.21 | | | | | | | | | | (293) uni(all_329_1) % 68.89/10.21 | | | | | | | | | | (294) some(int, all_69_2) = all_329_1 % 68.89/10.21 | | | | | | | | | | % 68.89/10.21 | | | | | | | | | | GROUND_INST: instantiating (62) with all_429_1, all_429_0, % 68.89/10.21 | | | | | | | | | | simplifying with (291) gives: % 68.89/10.21 | | | | | | | | | | (295) ~ ($lesseq(0, all_429_1)) | ? [v0: option_int] : % 68.89/10.21 | | | | | | | | | | ? [v1: uni] : (tb2t(v1) = v0 & tb2t(all_429_0) = v0 % 68.89/10.21 | | | | | | | | | | & nth1(int, $sum(all_429_1, all_72_8), all_72_5) % 68.89/10.21 | | | | | | | | | | = v1 & option_int(v0) & uni(v1)) % 68.89/10.21 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_135_1, all_69_0, % 68.89/10.22 | | | | | | | | | | simplifying with (279), (280) gives: % 68.89/10.22 | | | | | | | | | | (296) t2tb(all_69_0) = all_135_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_143_1, all_69_0, % 68.89/10.22 | | | | | | | | | | simplifying with (269), (270) gives: % 68.89/10.22 | | | | | | | | | | (297) t2tb(all_69_0) = all_143_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_329_1, all_235_3, % 68.89/10.22 | | | | | | | | | | simplifying with (223), (293) gives: % 68.89/10.22 | | | | | | | | | | (298) t2tb(all_235_3) = all_329_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_392_0, all_69_0, % 68.89/10.22 | | | | | | | | | | simplifying with (262), (263) gives: % 68.89/10.22 | | | | | | | | | | (299) t2tb(all_69_0) = all_392_0 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_429_0, all_69_0, % 68.89/10.22 | | | | | | | | | | simplifying with (286), (288) gives: % 68.89/10.22 | | | | | | | | | | (300) t2tb(all_69_0) = all_429_0 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | BETA: splitting (295) gives: % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | Case 1: % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | (301) $lesseq(all_429_1, -1) % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_INEQS: (285), (301) imply: % 68.89/10.22 | | | | | | | | | | | (302) $false % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | CLOSE: (302) is inconsistent. % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | Case 2: % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (26) with all_69_1, all_329_1, % 68.89/10.22 | | | | | | | | | | | all_69_2, int, simplifying with (31), (294) gives: % 68.89/10.22 | | | | | | | | | | | (303) all_329_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_69_1, all_429_0, % 68.89/10.22 | | | | | | | | | | | all_69_0, simplifying with (98), (300) gives: % 68.89/10.22 | | | | | | | | | | | (304) all_429_0 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_392_0, all_429_0, % 68.89/10.22 | | | | | | | | | | | all_69_0, simplifying with (299), (300) gives: % 68.89/10.22 | | | | | | | | | | | (305) all_429_0 = all_392_0 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_143_1, all_429_0, % 68.89/10.22 | | | | | | | | | | | all_69_0, simplifying with (297), (300) gives: % 68.89/10.22 | | | | | | | | | | | (306) all_429_0 = all_143_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_135_1, all_429_0, % 68.89/10.22 | | | | | | | | | | | all_69_0, simplifying with (296), (300) gives: % 68.89/10.22 | | | | | | | | | | | (307) all_429_0 = all_135_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_235_4, all_329_1, % 68.89/10.22 | | | | | | | | | | | all_235_3, simplifying with (217), (298) gives: % 68.89/10.22 | | | | | | | | | | | (308) all_329_1 = all_235_4 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (304), (305) imply: % 68.89/10.22 | | | | | | | | | | | (309) all_392_0 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (305), (307) imply: % 68.89/10.22 | | | | | | | | | | | (310) all_392_0 = all_135_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (305), (306) imply: % 68.89/10.22 | | | | | | | | | | | (311) all_392_0 = all_143_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (309), (311) imply: % 68.89/10.22 | | | | | | | | | | | (312) all_143_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (310), (311) imply: % 68.89/10.22 | | | | | | | | | | | (313) all_143_1 = all_135_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (303), (308) imply: % 68.89/10.22 | | | | | | | | | | | (314) all_235_4 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | COMBINE_EQS: (312), (313) imply: % 68.89/10.22 | | | | | | | | | | | (315) all_135_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | REDUCE: (206), (314) imply: % 68.89/10.22 | | | | | | | | | | | (316) tb2t(all_69_1) = all_235_3 % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | | REF_CLOSE: (20), (32), (45), (54), (64), (70), (85), (87), % 68.89/10.22 | | | | | | | | | | | (208), (211), (316) are inconsistent by sub-proof % 68.89/10.22 | | | | | | | | | | | #1. % 68.89/10.22 | | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | End of split % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | End of split % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | End of split % 68.89/10.22 | | | | | | | | % 68.89/10.22 | | | | | | | Case 2: % 68.89/10.22 | | | | | | | | % 68.89/10.22 | | | | | | | | (317) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.22 | | | | | | | | $difference(all_133_0, v0))) | ~ ($lesseq(0, % 68.89/10.22 | | | | | | | | v0)) | ~ (nth1(int, v0, all_72_7) = v1) | ? % 68.89/10.22 | | | | | | | | [v2: any] : ( ~ (v2 = all_69_0) & tb2t(v1) = v2 & % 68.89/10.22 | | | | | | | | option_int(v2))) % 68.89/10.22 | | | | | | | | % 68.89/10.22 | | | | | | | | BETA: splitting (184) gives: % 68.89/10.22 | | | | | | | | % 68.89/10.22 | | | | | | | | Case 1: % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | (318) ~ (length1(int, all_72_1) = 0) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | PRED_UNIFY: (183), (318) imply: % 68.89/10.22 | | | | | | | | | (319) ~ (all_72_6 = 1) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | STRENGTHEN: (186), (319) imply: % 68.89/10.22 | | | | | | | | | (320) $lesseq(2, all_72_6) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (317) with 0, all_329_1, simplifying % 68.89/10.22 | | | | | | | | | with (219) gives: % 68.89/10.22 | | | | | | | | | (321) ~ ($lesseq(1, all_133_0)) | ? [v0: any] : ( ~ (v0 = % 68.89/10.22 | | | | | | | | | all_69_0) & tb2t(all_329_1) = v0 & % 68.89/10.22 | | | | | | | | | option_int(v0)) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (7) with int, all_69_2, all_72_1, % 68.89/10.22 | | | | | | | | | all_72_7, all_329_1, simplifying with (15), (43), % 68.89/10.22 | | | | | | | | | (78), (180), (219) gives: % 68.89/10.22 | | | | | | | | | (322) some(int, all_69_2) = all_329_1 & uni(all_329_1) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | ALPHA: (322) implies: % 68.89/10.22 | | | | | | | | | (323) uni(all_329_1) % 68.89/10.22 | | | | | | | | | (324) some(int, all_69_2) = all_329_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_143_1, all_69_0, % 68.89/10.22 | | | | | | | | | simplifying with (269), (270) gives: % 68.89/10.22 | | | | | | | | | (325) t2tb(all_69_0) = all_143_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_329_1, all_235_3, % 68.89/10.22 | | | | | | | | | simplifying with (223), (323) gives: % 68.89/10.22 | | | | | | | | | (326) t2tb(all_235_3) = all_329_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_392_0, all_69_0, % 68.89/10.22 | | | | | | | | | simplifying with (262), (263) gives: % 68.89/10.22 | | | | | | | | | (327) t2tb(all_69_0) = all_392_0 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | BETA: splitting (321) gives: % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | Case 1: % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | (328) $lesseq(all_133_0, 0) % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | REDUCE: (166), (328) imply: % 68.89/10.22 | | | | | | | | | | (329) $lesseq(all_72_6, 0) % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | COMBINE_INEQS: (320), (329) imply: % 68.89/10.22 | | | | | | | | | | (330) $false % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | CLOSE: (330) is inconsistent. % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | Case 2: % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (26) with all_69_1, all_329_1, % 68.89/10.22 | | | | | | | | | | all_69_2, int, simplifying with (31), (324) gives: % 68.89/10.22 | | | | | | | | | | (331) all_329_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_69_1, all_392_0, % 68.89/10.22 | | | | | | | | | | all_69_0, simplifying with (98), (327) gives: % 68.89/10.22 | | | | | | | | | | (332) all_392_0 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_143_1, all_392_0, % 68.89/10.22 | | | | | | | | | | all_69_0, simplifying with (325), (327) gives: % 68.89/10.22 | | | | | | | | | | (333) all_392_0 = all_143_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_235_4, all_329_1, % 68.89/10.22 | | | | | | | | | | all_235_3, simplifying with (217), (326) gives: % 68.89/10.22 | | | | | | | | | | (334) all_329_1 = all_235_4 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | COMBINE_EQS: (332), (333) imply: % 68.89/10.22 | | | | | | | | | | (335) all_143_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | COMBINE_EQS: (331), (334) imply: % 68.89/10.22 | | | | | | | | | | (336) all_235_4 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | REDUCE: (206), (336) imply: % 68.89/10.22 | | | | | | | | | | (337) tb2t(all_69_1) = all_235_3 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | REF_CLOSE: (20), (32), (45), (54), (64), (70), (85), (87), % 68.89/10.22 | | | | | | | | | | (208), (211), (337) are inconsistent by sub-proof % 68.89/10.22 | | | | | | | | | | #1. % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | End of split % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | Case 2: % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | (338) nil(int) = all_72_1 % 68.89/10.22 | | | | | | | | | (339) length1(int, all_72_1) = 0 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (18) with all_72_12, all_72_1, int, % 68.89/10.22 | | | | | | | | | simplifying with (48), (338) gives: % 68.89/10.22 | | | | | | | | | (340) all_72_1 = all_72_12 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (25) with $sum(all_72_6, -1), 0, % 68.89/10.22 | | | | | | | | | all_72_1, int, simplifying with (183), (339) % 68.89/10.22 | | | | | | | | | gives: % 68.89/10.22 | | | | | | | | | (341) all_72_6 = 1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | COMBINE_EQS: (166), (341) imply: % 68.89/10.22 | | | | | | | | | (342) all_133_0 = 1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | REDUCE: (180), (340) imply: % 68.89/10.22 | | | | | | | | | (343) cons(int, all_69_2, all_72_12) = all_72_7 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | REDUCE: (43), (340) imply: % 68.89/10.22 | | | | | | | | | (344) uni(all_72_12) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (317) with 0, all_329_1, simplifying % 68.89/10.22 | | | | | | | | | with (219) gives: % 68.89/10.22 | | | | | | | | | (345) ~ ($lesseq(1, all_133_0)) | ? [v0: any] : ( ~ (v0 = % 68.89/10.22 | | | | | | | | | all_69_0) & tb2t(all_329_1) = v0 & % 68.89/10.22 | | | | | | | | | option_int(v0)) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (7) with int, all_69_2, all_72_12, % 68.89/10.22 | | | | | | | | | all_72_7, all_329_1, simplifying with (15), (78), % 68.89/10.22 | | | | | | | | | (219), (343), (344) gives: % 68.89/10.22 | | | | | | | | | (346) some(int, all_69_2) = all_329_1 & uni(all_329_1) % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | ALPHA: (346) implies: % 68.89/10.22 | | | | | | | | | (347) uni(all_329_1) % 68.89/10.22 | | | | | | | | | (348) some(int, all_69_2) = all_329_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_143_1, all_69_0, % 68.89/10.22 | | | | | | | | | simplifying with (269), (270) gives: % 68.89/10.22 | | | | | | | | | (349) t2tb(all_69_0) = all_143_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_329_1, all_235_3, % 68.89/10.22 | | | | | | | | | simplifying with (223), (347) gives: % 68.89/10.22 | | | | | | | | | (350) t2tb(all_235_3) = all_329_1 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | GROUND_INST: instantiating (bridgeR) with all_392_0, all_69_0, % 68.89/10.22 | | | | | | | | | simplifying with (262), (263) gives: % 68.89/10.22 | | | | | | | | | (351) t2tb(all_69_0) = all_392_0 % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | BETA: splitting (345) gives: % 68.89/10.22 | | | | | | | | | % 68.89/10.22 | | | | | | | | | Case 1: % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | (352) $lesseq(all_133_0, 0) % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | REDUCE: (342), (352) imply: % 68.89/10.22 | | | | | | | | | | (353) $false % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | CLOSE: (353) is inconsistent. % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | Case 2: % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (26) with all_69_1, all_329_1, % 68.89/10.22 | | | | | | | | | | all_69_2, int, simplifying with (31), (348) gives: % 68.89/10.22 | | | | | | | | | | (354) all_329_1 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_69_1, all_392_0, % 68.89/10.22 | | | | | | | | | | all_69_0, simplifying with (98), (351) gives: % 68.89/10.22 | | | | | | | | | | (355) all_392_0 = all_69_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_143_1, all_392_0, % 68.89/10.22 | | | | | | | | | | all_69_0, simplifying with (349), (351) gives: % 68.89/10.22 | | | | | | | | | | (356) all_392_0 = all_143_1 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | GROUND_INST: instantiating (19) with all_235_4, all_329_1, % 68.89/10.22 | | | | | | | | | | all_235_3, simplifying with (217), (350) gives: % 68.89/10.22 | | | | | | | | | | (357) all_329_1 = all_235_4 % 68.89/10.22 | | | | | | | | | | % 68.89/10.22 | | | | | | | | | | COMBINE_EQS: (355), (356) imply: % 68.89/10.23 | | | | | | | | | | (358) all_143_1 = all_69_1 % 68.89/10.23 | | | | | | | | | | % 68.89/10.23 | | | | | | | | | | COMBINE_EQS: (354), (357) imply: % 68.89/10.23 | | | | | | | | | | (359) all_235_4 = all_69_1 % 68.89/10.23 | | | | | | | | | | % 68.89/10.23 | | | | | | | | | | REDUCE: (206), (359) imply: % 68.89/10.23 | | | | | | | | | | (360) tb2t(all_69_1) = all_235_3 % 68.89/10.23 | | | | | | | | | | % 68.89/10.23 | | | | | | | | | | REF_CLOSE: (20), (32), (45), (54), (64), (70), (85), (87), % 68.89/10.23 | | | | | | | | | | (208), (211), (360) are inconsistent by sub-proof % 68.89/10.23 | | | | | | | | | | #1. % 68.89/10.23 | | | | | | | | | | % 68.89/10.23 | | | | | | | | | End of split % 68.89/10.23 | | | | | | | | | % 68.89/10.23 | | | | | | | | End of split % 68.89/10.23 | | | | | | | | % 68.89/10.23 | | | | | | | End of split % 68.89/10.23 | | | | | | | % 68.89/10.23 | | | | | | End of split % 68.89/10.23 | | | | | | % 68.89/10.23 | | | | | End of split % 68.89/10.23 | | | | | % 68.89/10.23 | | | | End of split % 68.89/10.23 | | | | % 68.89/10.23 | | | End of split % 68.89/10.23 | | | % 68.89/10.23 | | End of split % 68.89/10.23 | | % 68.89/10.23 | Case 2: % 68.89/10.23 | | % 68.89/10.23 | | (361) $lesseq(all_72_6, 0) % 68.89/10.23 | | % 68.89/10.23 | | COMBINE_INEQS: (186), (361) imply: % 68.89/10.23 | | (362) $false % 68.89/10.23 | | % 68.89/10.23 | | CLOSE: (362) is inconsistent. % 68.89/10.23 | | % 68.89/10.23 | End of split % 68.89/10.23 | % 68.89/10.23 End of proof % 68.89/10.23 % 68.89/10.23 Sub-proof #1 shows that the following formulas are inconsistent: % 68.89/10.23 ---------------------------------------------------------------- % 68.89/10.23 (1) ~ (all_235_3 = all_76_0) | (all_235_0 = all_76_0 & $lesseq(1, % 68.89/10.23 $difference(all_72_8, all_235_2)) & $lesseq(0, all_235_2) & % 68.89/10.23 tb2t(all_235_1) = all_76_0 & nth1(int, all_235_2, all_235_5) = % 68.89/10.23 all_235_1 & uni(all_235_1)) % 68.89/10.23 (2) tb2t(all_69_1) = all_235_3 % 68.89/10.23 (3) ! [v0: list_int] : ! [v1: int] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.89/10.23 (t2tb1(v0) = v2) | ~ (nth1(int, v1, v2) = v3) | ~ list_int(v0) | ? % 68.89/10.23 [v4: any] : ? [v5: option_int] : (zero_at1(v0, v1) = v4 & tb2t(v3) = % 68.89/10.23 v5 & option_int(v5) & ( ~ (v4 = 0) | (v5 = all_76_0 & ! [v6: int] : % 68.89/10.23 ! [v7: uni] : ( ~ ($lesseq(1, $difference(v1, v6))) | ~ % 68.89/10.23 ($lesseq(0, v6)) | ~ (nth1(int, v6, v2) = v7) | ? [v8: any] : % 68.89/10.23 ( ~ (v8 = all_76_0) & tb2t(v7) = v8 & option_int(v8))))))) % 68.89/10.23 (4) t2tb1(all_72_10) = all_72_5 % 68.89/10.23 (5) all_235_5 = all_72_5 % 68.89/10.23 (6) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_72_8, v0))) % 68.89/10.23 | ~ ($lesseq(0, v0)) | ~ (nth1(int, v0, all_72_5) = v1) | ? [v2: % 68.89/10.23 any] : ( ~ (v2 = all_72_13) & tb2t(v1) = v2 & option_int(v2))) % 68.89/10.23 (7) all_76_0 = all_69_0 % 68.89/10.23 (8) list_int(all_72_10) % 68.89/10.23 (9) ! [v0: option_int] : ! [v1: option_int] : ! [v2: uni] : (v1 = v0 | ~ % 68.89/10.23 (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 68.89/10.23 (10) all_72_13 = all_69_0 % 68.89/10.23 (11) tb2t(all_69_1) = all_69_0 % 68.89/10.23 % 68.89/10.23 Begin of proof % 68.89/10.23 | % 68.89/10.23 | GROUND_INST: instantiating (9) with all_69_0, all_235_3, all_69_1, simplifying % 68.89/10.23 | with (2), (11) gives: % 68.89/10.23 | (12) all_235_3 = all_69_0 % 68.89/10.23 | % 68.89/10.23 | BETA: splitting (1) gives: % 68.89/10.23 | % 68.89/10.23 | Case 1: % 68.89/10.23 | | % 68.89/10.23 | | (13) ~ (all_235_3 = all_76_0) % 68.89/10.23 | | % 68.89/10.23 | | REDUCE: (7), (12), (13) imply: % 68.89/10.23 | | (14) $false % 68.89/10.23 | | % 68.89/10.23 | | CLOSE: (14) is inconsistent. % 68.89/10.23 | | % 68.89/10.23 | Case 2: % 68.89/10.23 | | % 68.89/10.23 | | (15) all_235_3 = all_76_0 % 68.89/10.23 | | (16) all_235_0 = all_76_0 & $lesseq(1, $difference(all_72_8, all_235_2)) % 68.89/10.23 | | & $lesseq(0, all_235_2) & tb2t(all_235_1) = all_76_0 & nth1(int, % 68.89/10.23 | | all_235_2, all_235_5) = all_235_1 & uni(all_235_1) % 68.89/10.23 | | % 68.89/10.23 | | ALPHA: (16) implies: % 68.89/10.23 | | (17) $lesseq(0, all_235_2) % 68.89/10.23 | | (18) $lesseq(1, $difference(all_72_8, all_235_2)) % 68.89/10.23 | | (19) nth1(int, all_235_2, all_235_5) = all_235_1 % 68.89/10.23 | | (20) tb2t(all_235_1) = all_76_0 % 68.89/10.23 | | % 68.89/10.23 | | REDUCE: (7), (20) imply: % 68.89/10.23 | | (21) tb2t(all_235_1) = all_69_0 % 68.89/10.23 | | % 68.89/10.23 | | REDUCE: (5), (19) imply: % 68.89/10.23 | | (22) nth1(int, all_235_2, all_72_5) = all_235_1 % 68.89/10.23 | | % 68.89/10.23 | | GROUND_INST: instantiating (3) with all_72_10, all_235_2, all_72_5, % 68.89/10.23 | | all_235_1, simplifying with (4), (8), (22) gives: % 68.89/10.23 | | (23) ? [v0: any] : ? [v1: option_int] : (zero_at1(all_72_10, all_235_2) % 68.89/10.23 | | = v0 & tb2t(all_235_1) = v1 & option_int(v1) & ( ~ (v0 = 0) | (v1 % 68.89/10.23 | | = all_76_0 & ! [v2: int] : ! [v3: uni] : ( ~ ($lesseq(1, % 68.89/10.23 | | $difference(all_235_2, v2))) | ~ ($lesseq(0, v2)) | ~ % 68.89/10.23 | | (nth1(int, v2, all_72_5) = v3) | ? [v4: any] : ( ~ (v4 = % 68.89/10.23 | | all_76_0) & tb2t(v3) = v4 & option_int(v4)))))) % 68.89/10.23 | | % 68.89/10.23 | | GROUND_INST: instantiating (6) with all_235_2, all_235_1, simplifying with % 68.89/10.23 | | (22) gives: % 68.89/10.23 | | (24) ~ ($lesseq(1, $difference(all_72_8, all_235_2))) | ~ ($lesseq(0, % 68.89/10.23 | | all_235_2)) | ? [v0: any] : ( ~ (v0 = all_72_13) & % 68.89/10.23 | | tb2t(all_235_1) = v0 & option_int(v0)) % 68.89/10.23 | | % 68.89/10.23 | | DELTA: instantiating (23) with fresh symbols all_931_0, all_931_1 gives: % 68.89/10.23 | | (25) zero_at1(all_72_10, all_235_2) = all_931_1 & tb2t(all_235_1) = % 68.89/10.23 | | all_931_0 & option_int(all_931_0) & ( ~ (all_931_1 = 0) | (all_931_0 % 68.89/10.23 | | = all_76_0 & ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, % 68.89/10.23 | | $difference(all_235_2, v0))) | ~ ($lesseq(0, v0)) | ~ % 68.89/10.23 | | (nth1(int, v0, all_72_5) = v1) | ? [v2: any] : ( ~ (v2 = % 68.89/10.23 | | all_76_0) & tb2t(v1) = v2 & option_int(v2))))) % 68.89/10.23 | | % 68.89/10.23 | | ALPHA: (25) implies: % 68.89/10.23 | | (26) tb2t(all_235_1) = all_931_0 % 68.89/10.23 | | % 68.89/10.23 | | BETA: splitting (24) gives: % 68.89/10.23 | | % 68.89/10.23 | | Case 1: % 68.89/10.23 | | | % 68.89/10.23 | | | (27) $lesseq(all_235_2, -1) % 68.89/10.23 | | | % 68.89/10.23 | | | COMBINE_INEQS: (17), (27) imply: % 68.89/10.23 | | | (28) $false % 68.89/10.23 | | | % 68.89/10.23 | | | CLOSE: (28) is inconsistent. % 68.89/10.23 | | | % 68.89/10.23 | | Case 2: % 68.89/10.23 | | | % 68.89/10.23 | | | (29) ~ ($lesseq(1, $difference(all_72_8, all_235_2))) | ? [v0: any] : % 68.89/10.23 | | | ( ~ (v0 = all_72_13) & tb2t(all_235_1) = v0 & option_int(v0)) % 68.89/10.23 | | | % 68.89/10.23 | | | BETA: splitting (29) gives: % 68.89/10.23 | | | % 68.89/10.23 | | | Case 1: % 68.89/10.23 | | | | % 68.89/10.23 | | | | (30) $lesseq(all_72_8, all_235_2) % 68.89/10.23 | | | | % 68.89/10.23 | | | | COMBINE_INEQS: (18), (30) imply: % 68.89/10.23 | | | | (31) $false % 68.89/10.23 | | | | % 68.89/10.23 | | | | CLOSE: (31) is inconsistent. % 68.89/10.23 | | | | % 68.89/10.23 | | | Case 2: % 68.89/10.23 | | | | % 68.89/10.23 | | | | (32) ? [v0: any] : ( ~ (v0 = all_72_13) & tb2t(all_235_1) = v0 & % 68.89/10.23 | | | | option_int(v0)) % 68.89/10.23 | | | | % 68.89/10.23 | | | | DELTA: instantiating (32) with fresh symbol all_959_0 gives: % 68.89/10.23 | | | | (33) ~ (all_959_0 = all_72_13) & tb2t(all_235_1) = all_959_0 & % 68.89/10.23 | | | | option_int(all_959_0) % 68.89/10.23 | | | | % 68.89/10.23 | | | | ALPHA: (33) implies: % 68.89/10.23 | | | | (34) ~ (all_959_0 = all_72_13) % 68.89/10.23 | | | | (35) tb2t(all_235_1) = all_959_0 % 68.89/10.23 | | | | % 68.89/10.23 | | | | REDUCE: (10), (34) imply: % 68.89/10.23 | | | | (36) ~ (all_959_0 = all_69_0) % 68.89/10.23 | | | | % 68.89/10.23 | | | | GROUND_INST: instantiating (9) with all_69_0, all_959_0, all_235_1, % 68.89/10.23 | | | | simplifying with (21), (35) gives: % 68.89/10.23 | | | | (37) all_959_0 = all_69_0 % 68.89/10.23 | | | | % 68.89/10.23 | | | | GROUND_INST: instantiating (9) with all_931_0, all_959_0, all_235_1, % 68.89/10.23 | | | | simplifying with (26), (35) gives: % 68.89/10.23 | | | | (38) all_959_0 = all_931_0 % 68.89/10.23 | | | | % 68.89/10.23 | | | | COMBINE_EQS: (37), (38) imply: % 68.89/10.23 | | | | (39) all_931_0 = all_69_0 % 68.89/10.23 | | | | % 68.89/10.23 | | | | REDUCE: (36), (37) imply: % 68.89/10.23 | | | | (40) $false % 68.89/10.23 | | | | % 68.89/10.23 | | | | CLOSE: (40) is inconsistent. % 68.89/10.23 | | | | % 68.89/10.23 | | | End of split % 68.89/10.23 | | | % 68.89/10.23 | | End of split % 68.89/10.23 | | % 68.89/10.23 | End of split % 68.89/10.23 | % 68.89/10.23 End of proof % 68.89/10.23 % SZS output end Proof for theBenchmark % 68.89/10.23 % 68.89/10.23 9596ms %------------------------------------------------------------------------------