%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW625_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 : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:56 EDT 2023 % Result : Theorem 21.91s 3.71s % Output : Proof 43.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW625_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 21:40:28 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.60 ___ __ \_________(_)________________________________ % 0.20/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.60 (2023-06-19) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2023 % 0.20/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.60 Amanda Stjerna. % 0.20/0.60 Free software under BSD-3-Clause. % 0.20/0.60 % 0.20/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.60 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 0.20/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.20/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 4.38/1.32 Prover 3: Preprocessing ... % 4.38/1.32 Prover 6: Preprocessing ... % 4.38/1.32 Prover 1: Preprocessing ... % 4.38/1.32 Prover 5: Preprocessing ... % 4.38/1.33 Prover 2: Preprocessing ... % 4.38/1.33 Prover 4: Preprocessing ... % 4.38/1.33 Prover 0: Preprocessing ... % 10.53/2.29 Prover 1: Warning: ignoring some quantifiers % 11.62/2.33 Prover 4: Warning: ignoring some quantifiers % 11.62/2.34 Prover 5: Proving ... % 11.62/2.37 Prover 6: Proving ... % 11.62/2.38 Prover 3: Warning: ignoring some quantifiers % 12.12/2.39 Prover 1: Constructing countermodel ... % 12.12/2.42 Prover 3: Constructing countermodel ... % 12.12/2.44 Prover 4: Constructing countermodel ... % 13.03/2.52 Prover 2: Proving ... % 13.03/2.53 Prover 0: Proving ... % 21.91/3.71 Prover 0: proved (3089ms) % 21.91/3.71 % 21.91/3.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.91/3.71 % 21.91/3.72 Prover 5: stopped % 21.91/3.73 Prover 6: stopped % 21.91/3.73 Prover 2: stopped % 21.91/3.74 Prover 3: stopped % 21.91/3.75 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 21.91/3.75 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 21.91/3.75 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 21.91/3.75 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 21.91/3.75 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 23.74/3.95 Prover 13: Preprocessing ... % 23.74/3.98 Prover 7: Preprocessing ... % 24.21/3.99 Prover 8: Preprocessing ... % 24.21/4.03 Prover 10: Preprocessing ... % 24.21/4.03 Prover 11: Preprocessing ... % 24.79/4.16 Prover 7: Warning: ignoring some quantifiers % 24.79/4.18 Prover 7: Constructing countermodel ... % 25.55/4.27 Prover 10: Warning: ignoring some quantifiers % 25.55/4.28 Prover 11: Warning: ignoring some quantifiers % 25.55/4.29 Prover 11: Constructing countermodel ... % 26.48/4.30 Prover 10: Constructing countermodel ... % 26.48/4.31 Prover 8: Warning: ignoring some quantifiers % 26.48/4.32 Prover 13: Warning: ignoring some quantifiers % 26.48/4.34 Prover 13: Constructing countermodel ... % 26.48/4.35 Prover 8: Constructing countermodel ... % 41.48/6.33 Prover 4: Found proof (size 364) % 41.48/6.33 Prover 4: proved (5705ms) % 41.48/6.33 Prover 8: stopped % 41.48/6.33 Prover 7: stopped % 41.48/6.33 Prover 10: stopped % 41.48/6.33 Prover 13: stopped % 41.48/6.34 Prover 11: stopped % 41.48/6.34 Prover 1: stopped % 41.48/6.34 % 41.48/6.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 41.48/6.34 % 42.21/6.40 % SZS output start Proof for theBenchmark % 42.21/6.41 Assumptions after simplification: % 42.21/6.41 --------------------------------- % 42.21/6.41 % 42.21/6.41 (bridgeL) % 42.32/6.42 ! [v0: list_elt] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ list_elt(v0) | % 42.32/6.42 tb2t(v1) = v0) % 42.32/6.42 % 42.32/6.42 (bridgeR) % 42.33/6.42 ! [v0: uni] : ! [v1: list_elt] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | t2tb(v1) % 42.33/6.42 = v0) % 42.33/6.42 % 42.33/6.42 (cons_proj_1_def) % 42.33/6.43 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 42.33/6.43 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: any] : ? [v5: % 42.33/6.43 uni] : (cons_proj_1(v0, v3) = v5 & sort(v0, v1) = v4 & uni(v5) & ( ~ (v4 = % 42.33/6.43 0) | v5 = v1))) % 42.33/6.43 % 42.33/6.43 (length_def) % 42.33/6.43 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 42.33/6.43 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: int] : % 42.33/6.43 (length(v0, v3) = v4 & length(v0, v2) = $sum(v4, -1))) & ! [v0: ty] : ! % 42.33/6.43 [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | length(v0, v1) = 0) % 42.33/6.43 % 42.33/6.43 (length_nil) % 42.33/6.43 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (length(v0, v1) = v2) % 42.33/6.43 | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : ( ~ (v3 = v1) & nil(v0) = v3 & % 42.33/6.43 uni(v3))) & ! [v0: ty] : ! [v1: uni] : ( ~ (length(v0, v1) = 0) | ~ % 42.33/6.43 ty(v0) | ~ uni(v1) | nil(v0) = v1) % 42.33/6.43 % 42.33/6.43 (length_nonnegative) % 42.33/6.43 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ( ~ ($lesseq(v2, -1)) | ~ % 42.33/6.43 (length(v0, v1) = v2) | ~ ty(v0) | ~ uni(v1)) % 42.33/6.43 % 42.33/6.43 (mem_def) % 42.33/6.44 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: MultipleValueBool] : ! % 42.33/6.44 [v4: uni] : ! [v5: uni] : ! [v6: uni] : ( ~ (mem(v0, v1, v2) = v3) | ~ % 42.33/6.44 (cons(v0, v4, v5) = v6) | ~ (nil(v0) = v2) | ~ ty(v0) | ~ uni(v5) | ~ % 42.33/6.44 uni(v4) | ~ uni(v1) | ? [v7: int] : ? [v8: any] : ? [v9: any] : (( ~ (v7 % 42.33/6.44 = 0) & sort(v0, v1) = v7) | (mem(v0, v1, v6) = v8 & mem(v0, v1, v5) = % 42.33/6.44 v9 & sort(v0, v4) = v7 & ( ~ (v7 = 0) | (( ~ (v8 = 0) | v9 = 0 | v4 = % 42.33/6.44 v1) & (v8 = 0 | ( ~ (v9 = 0) & ~ (v4 = v1)))))))) & ! [v0: ty] : % 42.33/6.44 ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ (cons(v0, v2, % 42.33/6.44 v3) = v4) | ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) % 42.33/6.44 | ~ uni(v1) | ? [v5: any] : ? [v6: any] : ? [v7: any] : (mem(v0, v1, v4) % 42.33/6.44 = v6 & mem(v0, v1, v3) = v7 & sort(v0, v2) = v5 & ( ~ (v5 = 0) | (( ~ (v6 % 42.33/6.44 = 0) | v7 = 0 | v2 = v1) & (v6 = 0 | ( ~ (v7 = 0) & ~ (v2 = % 42.33/6.44 v1))))))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ % 42.33/6.44 (mem(v0, v1, v2) = 0) | ~ (nil(v0) = v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: % 42.33/6.44 int] : ( ~ (v3 = 0) & sort(v0, v1) = v3)) & ! [v0: ty] : ! [v1: uni] : ( % 42.33/6.44 ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ uni(v1) | ? [v2: uni] : ? [v3: int] % 42.33/6.44 : ( ~ (v3 = 0) & mem(v0, v1, v2) = v3 & nil(v0) = v2 & uni(v2))) % 42.33/6.44 % 42.33/6.44 (nil_Cons) % 42.33/6.44 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 42.33/6.44 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : ( ~ (v4 % 42.33/6.44 = v3) & nil(v0) = v4 & uni(v4))) % 42.33/6.44 % 42.33/6.44 (nil_sort) % 42.33/6.44 ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | ? [v2: ty] : % 42.33/6.44 (list(v0) = v2 & sort(v2, v1) = 0 & ty(v2))) & ! [v0: ty] : ! [v1: ty] : ( % 42.33/6.44 ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: uni] : (nil(v0) = v2 & sort(v1, v2) % 42.33/6.44 = 0 & uni(v2))) % 42.33/6.44 % 42.33/6.44 (num_occ_def) % 42.33/6.44 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! % 42.33/6.44 [v5: uni] : ! [v6: uni] : ( ~ (num_occ(v0, v1, v2) = v3) | ~ (cons(v0, v4, % 42.33/6.44 v5) = v6) | ~ (nil(v0) = v2) | ~ ty(v0) | ~ uni(v5) | ~ uni(v4) | ~ % 42.33/6.44 uni(v1) | ? [v7: int] : ? [v8: int] : ? [v9: int] : (( ~ (v7 = 0) & % 42.33/6.44 sort(v0, v1) = v7) | (num_occ(v0, v1, v6) = v8 & num_occ(v0, v1, v5) = % 42.33/6.44 v9 & sort(v0, v4) = v7 & ( ~ (v7 = 0) | (( ~ (v4 = v1) | $difference(v9, % 42.33/6.44 v8) = -1) & (v9 = v8 | v4 = v1)))))) & ! [v0: ty] : ! [v1: % 42.33/6.44 uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ (cons(v0, v2, v3) = % 42.33/6.44 v4) | ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ % 42.33/6.44 uni(v1) | ? [v5: any] : ? [v6: int] : ? [v7: int] : (num_occ(v0, v1, v4) % 42.33/6.44 = v6 & num_occ(v0, v1, v3) = v7 & sort(v0, v2) = v5 & ( ~ (v5 = 0) | (( ~ % 42.33/6.44 (v2 = v1) | $difference(v7, v6) = -1) & (v7 = v6 | v2 = v1))))) & ! % 42.33/6.44 [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : (v3 = 0 | ~ % 42.33/6.44 (num_occ(v0, v1, v2) = v3) | ~ (nil(v0) = v2) | ~ ty(v0) | ~ uni(v1) | ? % 42.33/6.44 [v4: int] : ( ~ (v4 = 0) & sort(v0, v1) = v4)) & ! [v0: ty] : ! [v1: uni] % 42.33/6.44 : ( ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ uni(v1) | ? [v2: uni] : % 42.33/6.44 (num_occ(v0, v1, v2) = 0 & nil(v0) = v2 & uni(v2))) % 42.33/6.44 % 42.33/6.44 (permut_cons_append) % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.45 [v5: uni] : ( ~ (infix_plpl(v0, v4, v3) = v5) | ~ (cons(v0, v1, v2) = v4) | % 42.33/6.45 ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v6: uni] : ? [v7: % 42.33/6.45 uni] : (permut(v0, v5, v7) = 0 & infix_plpl(v0, v2, v6) = v7 & cons(v0, % 42.33/6.45 v1, v3) = v6 & uni(v7) & uni(v6))) & ! [v0: ty] : ! [v1: uni] : ! % 42.33/6.45 [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ (infix_plpl(v0, % 42.33/6.45 v2, v4) = v5) | ~ (cons(v0, v1, v3) = v4) | ~ ty(v0) | ~ uni(v3) | ~ % 42.33/6.45 uni(v2) | ~ uni(v1) | ? [v6: uni] : ? [v7: uni] : (permut(v0, v7, v5) = 0 % 42.33/6.45 & infix_plpl(v0, v6, v3) = v7 & cons(v0, v1, v2) = v6 & uni(v7) & % 42.33/6.45 uni(v6))) % 42.33/6.45 % 42.33/6.45 (rev_append_def) % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.45 [v5: uni] : ( ~ (rev_append(v0, v4, v1) = v5) | ~ (cons(v0, v2, v3) = v4) | % 42.33/6.45 ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v6: uni] : % 42.33/6.45 (rev_append(v0, v3, v6) = v5 & cons(v0, v2, v1) = v6 & uni(v6) & uni(v5))) & % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.45 [v5: uni] : ( ~ (rev_append(v0, v3, v4) = v5) | ~ (cons(v0, v2, v1) = v4) | % 42.33/6.45 ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v6: uni] : % 42.33/6.45 (rev_append(v0, v6, v1) = v5 & cons(v0, v2, v3) = v6 & uni(v6) & uni(v5))) & % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : (v3 = v1 | ~ % 42.33/6.45 (rev_append(v0, v2, v1) = v3) | ~ (nil(v0) = v2) | ~ ty(v0) | ~ uni(v1)) % 42.33/6.45 % 42.33/6.45 (rev_append_def1) % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ % 42.33/6.45 (reverse(v0, v1) = v3) | ~ (infix_plpl(v0, v3, v2) = v4) | ~ ty(v0) | ~ % 42.33/6.45 uni(v2) | ~ uni(v1) | (rev_append(v0, v1, v2) = v4 & uni(v4))) & ! [v0: % 42.33/6.45 ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (rev_append(v0, v1, % 42.33/6.45 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : % 42.33/6.45 (reverse(v0, v1) = v4 & infix_plpl(v0, v4, v2) = v3 & uni(v4) & uni(v3))) % 42.33/6.45 % 42.33/6.45 (rev_append_length) % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (rev_append(v0, % 42.33/6.45 v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: int] : ? % 42.33/6.45 [v5: int] : (length(v0, v3) = v4 & length(v0, v2) = $difference(v4, v5) & % 42.33/6.45 length(v0, v1) = v5)) % 42.33/6.45 % 42.33/6.45 (reverse_append) % 42.33/6.45 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.45 [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v4) = v5) | ~ (infix_plpl(v0, v5, % 42.33/6.45 v2) = v6) | ~ (cons(v0, v3, v1) = v4) | ~ ty(v0) | ~ uni(v3) | ~ % 42.33/6.45 uni(v2) | ~ uni(v1) | ? [v7: uni] : ? [v8: uni] : (reverse(v0, v1) = v7 & % 42.33/6.45 infix_plpl(v0, v7, v8) = v6 & cons(v0, v3, v2) = v8 & uni(v8) & uni(v7) & % 42.33/6.45 uni(v6))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! % 42.33/6.45 [v4: uni] : ! [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v1) = v4) | ~ % 42.33/6.45 (infix_plpl(v0, v4, v5) = v6) | ~ (cons(v0, v3, v2) = v5) | ~ ty(v0) | ~ % 42.33/6.45 uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v7: uni] : ? [v8: uni] : % 42.33/6.45 (reverse(v0, v7) = v8 & infix_plpl(v0, v8, v2) = v6 & cons(v0, v3, v1) = v7 % 42.33/6.45 & uni(v8) & uni(v7) & uni(v6))) % 42.33/6.45 % 42.33/6.45 (reverse_cons) % 42.33/6.46 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.46 [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v1) = v3) | ~ (infix_plpl(v0, v3, % 42.33/6.46 v5) = v6) | ~ (cons(v0, v2, v4) = v5) | ~ (nil(v0) = v4) | ~ ty(v0) | % 42.33/6.46 ~ uni(v2) | ~ uni(v1) | ? [v7: uni] : (reverse(v0, v7) = v6 & cons(v0, % 42.33/6.46 v2, v1) = v7 & uni(v7) & uni(v6))) & ! [v0: ty] : ! [v1: uni] : ! % 42.33/6.46 [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v2, v1) = v3) | ~ ty(v0) | ~ % 42.33/6.46 uni(v2) | ~ uni(v1) | ? [v4: uni] : ? [v5: uni] : ? [v6: uni] : ? [v7: % 42.33/6.46 uni] : (reverse(v0, v3) = v4 & reverse(v0, v1) = v5 & infix_plpl(v0, v5, % 42.33/6.46 v7) = v4 & cons(v0, v2, v6) = v7 & nil(v0) = v6 & uni(v7) & uni(v6) & % 42.33/6.46 uni(v5) & uni(v4))) % 42.33/6.46 % 42.33/6.46 (reverse_def) % 42.33/6.46 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.46 [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v2) = v3) | ~ (infix_plpl(v0, v3, % 42.33/6.46 v5) = v6) | ~ (cons(v0, v1, v4) = v5) | ~ (nil(v0) = v4) | ~ ty(v0) | % 42.33/6.46 ~ uni(v2) | ~ uni(v1) | ? [v7: uni] : (reverse(v0, v7) = v6 & cons(v0, % 42.33/6.46 v1, v2) = v7 & uni(v7) & uni(v6))) & ! [v0: ty] : ! [v1: uni] : ! % 42.33/6.46 [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ % 42.33/6.46 uni(v2) | ~ uni(v1) | ? [v4: uni] : ? [v5: uni] : ? [v6: uni] : ? [v7: % 42.33/6.46 uni] : (reverse(v0, v3) = v4 & reverse(v0, v2) = v5 & infix_plpl(v0, v5, % 42.33/6.46 v7) = v4 & cons(v0, v1, v6) = v7 & nil(v0) = v6 & uni(v7) & uni(v6) & % 42.33/6.46 uni(v5) & uni(v4))) & ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ % 42.33/6.46 ty(v0) | (reverse(v0, v1) = v1 & uni(v1))) % 42.33/6.46 % 42.33/6.46 (reverse_length) % 42.33/6.46 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (reverse(v0, v1) = v2) | ~ % 42.33/6.46 ty(v0) | ~ uni(v1) | ? [v3: int] : (length(v0, v2) = v3 & length(v0, v1) = % 42.33/6.46 v3)) & ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ( ~ (length(v0, v1) = % 42.33/6.46 v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : (reverse(v0, v1) = v3 & % 42.33/6.46 length(v0, v3) = v2 & uni(v3))) % 42.33/6.46 % 42.33/6.46 (reverse_mem) % 42.33/6.46 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: int] : (v4 % 42.33/6.46 = 0 | ~ (reverse(v0, v1) = v3) | ~ (mem(v0, v2, v3) = v4) | ~ ty(v0) | ~ % 42.33/6.46 uni(v2) | ~ uni(v1) | ? [v5: int] : ( ~ (v5 = 0) & mem(v0, v2, v1) = v5)) % 42.33/6.46 & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : (v3 = 0 | ~ % 42.33/6.46 (mem(v0, v2, v1) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] % 42.33/6.46 : ? [v5: int] : ( ~ (v5 = 0) & reverse(v0, v1) = v4 & mem(v0, v2, v4) = v5 % 42.33/6.46 & uni(v4))) & ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( % 42.33/6.46 ~ (reverse(v0, v1) = v3) | ~ (mem(v0, v2, v3) = 0) | ~ ty(v0) | ~ uni(v2) % 42.33/6.46 | ~ uni(v1) | mem(v0, v2, v1) = 0) & ! [v0: ty] : ! [v1: uni] : ! [v2: % 42.33/6.46 uni] : ( ~ (mem(v0, v2, v1) = 0) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 42.33/6.46 [v3: uni] : (reverse(v0, v1) = v3 & mem(v0, v2, v3) = 0 & uni(v3))) % 42.33/6.46 % 42.33/6.46 (reverse_reverse) % 42.33/6.46 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (reverse(v0, v1) = v2) | ~ % 42.33/6.46 ty(v0) | ~ uni(v1) | reverse(v0, v2) = v1) % 42.33/6.46 % 42.33/6.46 (sorted_Nil) % 42.33/6.46 ty(elt1) & ? [v0: uni] : ? [v1: list_elt] : (sorted(v1) = 0 & tb2t(v0) = v1 % 42.33/6.46 & nil(elt1) = v0 & list_elt(v1) & uni(v0)) % 42.33/6.46 % 42.33/6.46 (sorted_One) % 42.33/6.47 ty(elt1) & ? [v0: uni] : (nil(elt1) = v0 & uni(v0) & ! [v1: elt] : ! [v2: % 42.33/6.47 uni] : ( ~ (t2tb1(v1) = v2) | ~ elt(v1) | ? [v3: uni] : ? [v4: % 42.33/6.47 list_elt] : (sorted(v4) = 0 & tb2t(v3) = v4 & cons(elt1, v2, v0) = v3 & % 42.33/6.47 list_elt(v4) & uni(v3)))) % 42.33/6.47 % 42.33/6.47 (sorted_append) % 42.33/6.47 ty(elt1) & ! [v0: list_elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] % 42.33/6.47 : ! [v4: uni] : ( ~ (t2tb(v1) = v3) | ~ (t2tb(v0) = v2) | ~ % 42.33/6.47 (infix_plpl(elt1, v2, v3) = v4) | ~ list_elt(v1) | ~ list_elt(v0) | ? % 42.33/6.47 [v5: any] : ? [v6: any] : ? [v7: list_elt] : ? [v8: any] : ? [v9: elt] : % 42.33/6.47 ? [v10: elt] : ? [v11: uni] : ? [v12: int] : ? [v13: uni] : ? [v14: % 42.33/6.47 int] : ? [v15: int] : (elt(v10) & elt(v9) & ((v14 = 0 & v12 = 0 & ~ (v15 % 42.33/6.47 = 0) & t2tb1(v10) = v13 & t2tb1(v9) = v11 & le(v9, v10) = v15 & % 42.33/6.47 mem(elt1, v13, v3) = 0 & mem(elt1, v11, v2) = 0 & uni(v13) & uni(v11)) % 42.33/6.47 | (sorted(v7) = v8 & sorted(v1) = v6 & sorted(v0) = v5 & tb2t(v4) = v7 & % 42.33/6.47 list_elt(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | v8 = 0))))) & ! [v0: % 42.33/6.47 list_elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : % 42.33/6.47 ( ~ (t2tb(v1) = v3) | ~ (t2tb(v0) = v2) | ~ (infix_plpl(elt1, v2, v3) = v4) % 42.33/6.47 | ~ list_elt(v1) | ~ list_elt(v0) | ? [v5: list_elt] : ? [v6: any] : ? % 42.33/6.47 [v7: any] : ? [v8: any] : (sorted(v5) = v6 & sorted(v1) = v8 & sorted(v0) = % 42.33/6.47 v7 & tb2t(v4) = v5 & list_elt(v5) & ( ~ (v6 = 0) | (v8 = 0 & v7 = 0 & ! % 42.33/6.47 [v9: elt] : ! [v10: elt] : ! [v11: int] : (v11 = 0 | ~ (le(v9, v10) % 42.33/6.47 = v11) | ~ elt(v10) | ~ elt(v9) | ? [v12: uni] : ? [v13: any] % 42.33/6.47 : ? [v14: uni] : ? [v15: any] : (t2tb1(v10) = v14 & t2tb1(v9) = % 42.33/6.47 v12 & mem(elt1, v14, v3) = v15 & mem(elt1, v12, v2) = v13 & % 42.33/6.47 uni(v14) & uni(v12) & ( ~ (v15 = 0) | ~ (v13 = 0)))))))) % 42.33/6.47 % 42.33/6.47 (sorted_inversion) % 42.33/6.47 ty(elt1) & ? [v0: uni] : ? [v1: list_elt] : (tb2t(v0) = v1 & nil(elt1) = v0 % 42.33/6.47 & list_elt(v1) & uni(v0) & ! [v2: list_elt] : (v2 = v1 | ~ (sorted(v2) = % 42.33/6.47 0) | ~ list_elt(v2) | ? [v3: elt] : ? [v4: elt] : ? [v5: list_elt] : % 42.33/6.47 ? [v6: int] : ? [v7: uni] : ? [v8: uni] : ? [v9: uni] : ? [v10: % 42.33/6.47 list_elt] : ? [v11: int] : ? [v12: uni] : ? [v13: uni] : ? [v14: % 42.33/6.47 list_elt] : ? [v15: elt] : ? [v16: uni] : ? [v17: uni] : ? [v18: % 42.33/6.47 list_elt] : (list_elt(v5) & elt(v15) & elt(v4) & elt(v3) & ((v18 = v2 & % 42.33/6.47 t2tb1(v15) = v16 & tb2t(v17) = v2 & cons(elt1, v16, v0) = v17 & % 42.33/6.47 uni(v17) & uni(v16)) | (v14 = v2 & v11 = 0 & v6 = 0 & t2tb1(v4) = v7 % 42.33/6.47 & t2tb1(v3) = v12 & sorted(v10) = 0 & tb2t(v13) = v2 & tb2t(v9) = % 42.33/6.47 v10 & t2tb(v5) = v8 & le(v3, v4) = 0 & cons(elt1, v12, v9) = v13 & % 42.33/6.47 cons(elt1, v7, v8) = v9 & list_elt(v10) & uni(v13) & uni(v12) & % 42.33/6.47 uni(v9) & uni(v8) & uni(v7)))))) % 42.33/6.47 % 42.33/6.47 (sorted_mem) % 42.33/6.48 ty(elt1) & ! [v0: elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! % 42.33/6.48 [v4: uni] : ( ~ (t2tb1(v0) = v3) | ~ (t2tb(v1) = v2) | ~ (cons(elt1, v3, v2) % 42.33/6.48 = v4) | ~ list_elt(v1) | ~ elt(v0) | ? [v5: any] : ? [v6: list_elt] : % 42.33/6.48 ? [v7: any] : ? [v8: elt] : ? [v9: uni] : ? [v10: int] : ? [v11: int] : % 42.33/6.48 (elt(v8) & ((v10 = 0 & ~ (v11 = 0) & t2tb1(v8) = v9 & le(v0, v8) = v11 & % 42.33/6.48 mem(elt1, v9, v2) = 0 & uni(v9)) | (sorted(v6) = v7 & sorted(v1) = v5 % 42.33/6.48 & tb2t(v4) = v6 & list_elt(v6) & ( ~ (v5 = 0) | v7 = 0))))) & ! [v0: % 42.33/6.48 elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ % 42.33/6.48 (t2tb1(v0) = v2) | ~ (t2tb(v1) = v3) | ~ (cons(elt1, v2, v3) = v4) | ~ % 42.33/6.48 list_elt(v1) | ~ elt(v0) | ? [v5: list_elt] : ? [v6: any] : ? [v7: any] % 42.33/6.48 : (sorted(v5) = v6 & sorted(v1) = v7 & tb2t(v4) = v5 & list_elt(v5) & ( ~ % 42.33/6.48 (v6 = 0) | (v7 = 0 & ! [v8: elt] : ! [v9: int] : (v9 = 0 | ~ (le(v0, % 42.33/6.48 v8) = v9) | ~ elt(v8) | ? [v10: uni] : ? [v11: int] : ( ~ % 42.33/6.48 (v11 = 0) & t2tb1(v8) = v10 & mem(elt1, v10, v3) = v11 & % 42.33/6.48 uni(v10))) & ! [v8: elt] : ! [v9: uni] : ( ~ (t2tb1(v8) = v9) | % 42.33/6.48 ~ elt(v8) | ? [v10: any] : ? [v11: any] : (le(v0, v8) = v11 & % 42.33/6.48 mem(elt1, v9, v3) = v10 & ( ~ (v10 = 0) | v11 = 0))))))) % 42.33/6.48 % 42.33/6.48 (sorted_reverse_cons2) % 42.33/6.48 ty(elt1) & ! [v0: elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! % 42.33/6.48 [v4: uni] : ( ~ (t2tb1(v0) = v2) | ~ (t2tb(v1) = v3) | ~ (cons(elt1, v2, v3) % 42.33/6.48 = v4) | ~ list_elt(v1) | ~ elt(v0) | ? [v5: uni] : ? [v6: list_elt] : % 42.33/6.48 ? [v7: any] : ? [v8: uni] : ? [v9: list_elt] : ? [v10: any] : (sorted(v9) % 42.33/6.48 = v10 & sorted(v6) = v7 & tb2t(v8) = v9 & tb2t(v5) = v6 & reverse(elt1, % 42.33/6.48 v4) = v5 & reverse(elt1, v3) = v8 & list_elt(v9) & list_elt(v6) & % 42.33/6.48 uni(v8) & uni(v5) & ( ~ (v7 = 0) | v10 = 0))) % 42.33/6.48 % 42.33/6.48 (t2tb_sort) % 42.33/6.48 ty(elt1) & ? [v0: ty] : (list(elt1) = v0 & ty(v0) & ! [v1: list_elt] : ! % 42.33/6.48 [v2: uni] : ( ~ (t2tb(v1) = v2) | ~ list_elt(v1) | sort(v0, v2) = 0)) % 42.33/6.48 % 42.33/6.48 (t2tb_sort1) % 42.33/6.48 ty(elt1) & ! [v0: elt] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ elt(v0) | % 42.33/6.48 sort(elt1, v1) = 0) % 42.33/6.48 % 42.33/6.48 (wP_parameter_rev_merge_rev) % 42.33/6.48 ty(elt1) & ? [v0: uni] : ? [v1: list_elt] : ? [v2: list_elt] : ? [v3: % 42.33/6.48 list_elt] : ? [v4: uni] : ? [v5: uni] : ? [v6: list_elt] : ? [v7: uni] : % 42.33/6.48 ? [v8: uni] : ? [v9: list_elt] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 42.33/6.48 list_elt] : ? [v13: int] : ? [v14: elt] : ? [v15: list_elt] : ? [v16: % 42.33/6.49 uni] : ? [v17: uni] : ? [v18: uni] : ( ~ (v13 = 0) & rev_append(elt1, v7, % 42.33/6.49 v10) = v11 & t2tb1(v14) = v16 & sorted(v12) = v13 & sorted(v9) = 0 & % 42.33/6.49 sorted(v6) = 0 & sorted(v3) = 0 & tb2t(v18) = v2 & tb2t(v11) = v12 & % 42.33/6.49 tb2t(v8) = v9 & tb2t(v5) = v6 & tb2t(v0) = v1 & t2tb(v15) = v17 & t2tb(v3) = % 42.33/6.49 v10 & t2tb(v2) = v7 & t2tb(v1) = v4 & reverse(elt1, v7) = v8 & reverse(elt1, % 42.33/6.49 v4) = v5 & cons(elt1, v16, v17) = v18 & nil(elt1) = v0 & list_elt(v15) & % 42.33/6.49 list_elt(v12) & list_elt(v9) & list_elt(v6) & list_elt(v3) & list_elt(v2) & % 42.33/6.49 list_elt(v1) & elt(v14) & uni(v18) & uni(v17) & uni(v16) & uni(v11) & % 42.33/6.49 uni(v10) & uni(v8) & uni(v7) & uni(v5) & uni(v4) & uni(v0) & ! [v19: elt] : % 42.33/6.49 ! [v20: elt] : ! [v21: int] : (v21 = 0 | ~ (le(v20, v19) = v21) | ~ % 42.33/6.49 elt(v20) | ~ elt(v19) | ? [v22: uni] : ? [v23: any] : ? [v24: uni] : % 42.33/6.49 ? [v25: any] : (t2tb1(v20) = v24 & t2tb1(v19) = v22 & mem(elt1, v24, v7) = % 42.33/6.49 v25 & mem(elt1, v22, v10) = v23 & uni(v24) & uni(v22) & ( ~ (v25 = 0) | % 42.33/6.49 ~ (v23 = 0)))) & ! [v19: elt] : ! [v20: elt] : ! [v21: int] : (v21 % 42.33/6.49 = 0 | ~ (le(v20, v19) = v21) | ~ elt(v20) | ~ elt(v19) | ? [v22: uni] % 42.33/6.49 : ? [v23: any] : ? [v24: uni] : ? [v25: any] : (t2tb1(v20) = v24 & % 42.33/6.49 t2tb1(v19) = v22 & mem(elt1, v24, v4) = v25 & mem(elt1, v22, v10) = v23 % 42.33/6.49 & uni(v24) & uni(v22) & ( ~ (v25 = 0) | ~ (v23 = 0))))) % 42.33/6.49 % 42.33/6.49 (function-axioms) % 42.33/6.49 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 42.33/6.49 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (match_list(v6, v5, v4, v3, v2) = v1) | % 42.33/6.49 ~ (match_list(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 42.33/6.49 [v2: uni] : ! [v3: uni] : ! [v4: bool] : ! [v5: ty] : (v1 = v0 | ~ % 42.33/6.49 (match_bool(v5, v4, v3, v2) = v1) | ~ (match_bool(v5, v4, v3, v2) = v0)) & % 42.33/6.49 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = % 42.33/6.49 v0 | ~ (rev_append(v4, v3, v2) = v1) | ~ (rev_append(v4, v3, v2) = v0)) & % 42.33/6.49 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! % 42.33/6.49 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (permut(v4, v3, v2) = v1) | ~ % 42.33/6.49 (permut(v4, v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! % 42.33/6.49 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (num_occ(v4, v3, v2) = v1) | ~ % 42.33/6.49 (num_occ(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 42.33/6.49 MultipleValueBool] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 42.33/6.49 ~ (mem(v4, v3, v2) = v1) | ~ (mem(v4, v3, v2) = v0)) & ! [v0: uni] : ! % 42.33/6.49 [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ % 42.33/6.49 (infix_plpl(v4, v3, v2) = v1) | ~ (infix_plpl(v4, v3, v2) = v0)) & ! [v0: % 42.33/6.49 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 42.33/6.49 ~ (cons(v4, v3, v2) = v1) | ~ (cons(v4, v3, v2) = v0)) & ! [v0: % 42.33/6.49 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: elt] : ! [v3: % 42.33/6.49 elt] : (v1 = v0 | ~ (le(v3, v2) = v1) | ~ (le(v3, v2) = v0)) & ! [v0: % 42.33/6.49 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 42.33/6.49 (reverse(v3, v2) = v1) | ~ (reverse(v3, v2) = v0)) & ! [v0: int] : ! [v1: % 42.33/6.49 int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (length(v3, v2) = v1) | ~ % 42.33/6.49 (length(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 42.33/6.49 [v3: ty] : (v1 = v0 | ~ (cons_proj_2(v3, v2) = v1) | ~ (cons_proj_2(v3, v2) % 42.33/6.49 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = % 42.33/6.49 v0 | ~ (cons_proj_1(v3, v2) = v1) | ~ (cons_proj_1(v3, v2) = v0)) & ! % 42.33/6.49 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: % 42.33/6.49 ty] : (v1 = v0 | ~ (sort(v3, v2) = v1) | ~ (sort(v3, v2) = v0)) & ! [v0: % 42.33/6.49 elt] : ! [v1: elt] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ % 42.33/6.49 (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: elt] : (v1 = v0 | % 42.33/6.49 ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 42.33/6.49 [v1: MultipleValueBool] : ! [v2: list_elt] : (v1 = v0 | ~ (sorted(v2) = v1) % 42.33/6.49 | ~ (sorted(v2) = v0)) & ! [v0: list_elt] : ! [v1: list_elt] : ! [v2: % 42.33/6.49 uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & ! [v0: uni] : % 42.33/6.49 ! [v1: uni] : ! [v2: list_elt] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ (t2tb(v2) % 42.33/6.49 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ % 42.33/6.49 (nil(v2) = v1) | ~ (nil(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: % 42.33/6.49 ty] : (v1 = v0 | ~ (list(v2) = v1) | ~ (list(v2) = v0)) & ! [v0: uni] : % 42.33/6.49 ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (witness(v2) = v1) | ~ (witness(v2) % 42.33/6.49 = v0)) % 42.33/6.49 % 42.33/6.49 Further assumptions not needed in the proof: % 42.33/6.49 -------------------------------------------- % 42.33/6.49 append_Num_Occ, append_assoc, append_l_nil, append_length, bool_inversion, % 42.33/6.49 bridgeL1, bridgeR1, compatOrderMult, cons_proj_1_sort, cons_proj_2_def, % 42.33/6.49 cons_proj_2_sort, cons_sort, infix_plpl_def, infix_plpl_sort, list_inversion, % 42.33/6.49 match_bool_False, match_bool_True, match_bool_sort, match_list_Cons, % 42.33/6.49 match_list_Nil, match_list_sort, mem_Num_Occ, mem_append, mem_decomp, % 42.33/6.49 permut_append, permut_append_swap, permut_assoc, permut_cons, permut_def, % 42.33/6.49 permut_length, permut_mem, permut_refl, permut_swap, permut_sym, permut_trans, % 42.33/6.49 refl, rev_append_append_l, rev_append_append_r, rev_append_sort, % 42.33/6.49 reverse_num_occ, reverse_sort, sorted_Two, sorted_rev_append, % 42.33/6.49 sorted_reverse_cons, sorted_reverse_mem, total, trans, true_False, % 42.33/6.49 tuple0_inversion, witness_sort % 42.33/6.49 % 42.33/6.49 Those formulas are unsatisfiable: % 42.33/6.49 --------------------------------- % 42.33/6.49 % 42.33/6.49 Begin of proof % 42.33/6.49 | % 42.33/6.49 | ALPHA: (nil_sort) implies: % 42.33/6.49 | (1) ! [v0: ty] : ! [v1: ty] : ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: % 42.33/6.49 | uni] : (nil(v0) = v2 & sort(v1, v2) = 0 & uni(v2))) % 42.33/6.49 | % 42.33/6.49 | ALPHA: (length_def) implies: % 42.33/6.50 | (2) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 42.33/6.50 | (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 42.33/6.50 | [v4: int] : (length(v0, v3) = v4 & length(v0, v2) = $sum(v4, -1))) % 42.33/6.50 | % 42.33/6.50 | ALPHA: (length_nil) implies: % 42.33/6.50 | (3) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (length(v0, % 42.33/6.50 | v1) = v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : ( ~ (v3 = v1) % 42.33/6.50 | & nil(v0) = v3 & uni(v3))) % 42.33/6.50 | % 42.33/6.50 | ALPHA: (mem_def) implies: % 42.33/6.50 | (4) ! [v0: ty] : ! [v1: uni] : ( ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ % 42.33/6.50 | uni(v1) | ? [v2: uni] : ? [v3: int] : ( ~ (v3 = 0) & mem(v0, v1, % 42.33/6.50 | v2) = v3 & nil(v0) = v2 & uni(v2))) % 42.33/6.50 | (5) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] % 42.70/6.50 | : ( ~ (cons(v0, v2, v3) = v4) | ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ % 42.70/6.50 | uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v5: any] : ? [v6: any] : ? % 42.70/6.50 | [v7: any] : (mem(v0, v1, v4) = v6 & mem(v0, v1, v3) = v7 & sort(v0, % 42.70/6.50 | v2) = v5 & ( ~ (v5 = 0) | (( ~ (v6 = 0) | v7 = 0 | v2 = v1) & (v6 % 42.70/6.50 | = 0 | ( ~ (v7 = 0) & ~ (v2 = v1))))))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (num_occ_def) implies: % 42.70/6.50 | (6) ! [v0: ty] : ! [v1: uni] : ( ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ % 42.70/6.50 | uni(v1) | ? [v2: uni] : (num_occ(v0, v1, v2) = 0 & nil(v0) = v2 & % 42.70/6.50 | uni(v2))) % 42.70/6.50 | (7) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] % 42.70/6.50 | : ( ~ (cons(v0, v2, v3) = v4) | ~ (sort(v0, v1) = 0) | ~ ty(v0) | ~ % 42.70/6.50 | uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v5: any] : ? [v6: int] : ? % 42.70/6.50 | [v7: int] : (num_occ(v0, v1, v4) = v6 & num_occ(v0, v1, v3) = v7 & % 42.70/6.50 | sort(v0, v2) = v5 & ( ~ (v5 = 0) | (( ~ (v2 = v1) | $difference(v7, % 42.70/6.50 | v6) = -1) & (v7 = v6 | v2 = v1))))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (reverse_def) implies: % 42.70/6.50 | (8) ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | % 42.70/6.50 | (reverse(v0, v1) = v1 & uni(v1))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (reverse_append) implies: % 42.70/6.50 | (9) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] % 42.70/6.50 | : ! [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v1) = v4) | ~ % 42.70/6.50 | (infix_plpl(v0, v4, v5) = v6) | ~ (cons(v0, v3, v2) = v5) | ~ % 42.70/6.50 | ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v7: uni] : ? % 42.70/6.50 | [v8: uni] : (reverse(v0, v7) = v8 & infix_plpl(v0, v8, v2) = v6 & % 42.70/6.50 | cons(v0, v3, v1) = v7 & uni(v8) & uni(v7) & uni(v6))) % 42.70/6.50 | (10) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.70/6.50 | uni] : ! [v5: uni] : ! [v6: uni] : ( ~ (reverse(v0, v4) = v5) | ~ % 42.70/6.50 | (infix_plpl(v0, v5, v2) = v6) | ~ (cons(v0, v3, v1) = v4) | ~ % 42.70/6.50 | ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ uni(v1) | ? [v7: uni] : ? % 42.70/6.50 | [v8: uni] : (reverse(v0, v1) = v7 & infix_plpl(v0, v7, v8) = v6 & % 42.70/6.50 | cons(v0, v3, v2) = v8 & uni(v8) & uni(v7) & uni(v6))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (reverse_cons) implies: % 42.70/6.50 | (11) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 42.70/6.50 | (cons(v0, v2, v1) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? % 42.70/6.50 | [v4: uni] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : % 42.70/6.50 | (reverse(v0, v3) = v4 & reverse(v0, v1) = v5 & infix_plpl(v0, v5, % 42.70/6.50 | v7) = v4 & cons(v0, v2, v6) = v7 & nil(v0) = v6 & uni(v7) & % 42.70/6.50 | uni(v6) & uni(v5) & uni(v4))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (reverse_mem) implies: % 42.70/6.50 | (12) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (mem(v0, v2, v1) = 0) % 42.70/6.50 | | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v3: uni] : (reverse(v0, % 42.70/6.50 | v1) = v3 & mem(v0, v2, v3) = 0 & uni(v3))) % 42.70/6.50 | % 42.70/6.50 | ALPHA: (reverse_length) implies: % 42.70/6.51 | (13) ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ( ~ (length(v0, v1) = v2) % 42.70/6.51 | | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : (reverse(v0, v1) = v3 & % 42.70/6.51 | length(v0, v3) = v2 & uni(v3))) % 42.70/6.51 | (14) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (reverse(v0, v1) = v2) % 42.70/6.51 | | ~ ty(v0) | ~ uni(v1) | ? [v3: int] : (length(v0, v2) = v3 & % 42.70/6.51 | length(v0, v1) = v3)) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (permut_cons_append) implies: % 42.70/6.51 | (15) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.70/6.51 | uni] : ! [v5: uni] : ( ~ (infix_plpl(v0, v2, v4) = v5) | ~ % 42.70/6.51 | (cons(v0, v1, v3) = v4) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ % 42.70/6.51 | uni(v1) | ? [v6: uni] : ? [v7: uni] : (permut(v0, v7, v5) = 0 & % 42.70/6.51 | infix_plpl(v0, v6, v3) = v7 & cons(v0, v1, v2) = v6 & uni(v7) & % 42.70/6.51 | uni(v6))) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (t2tb_sort) implies: % 42.70/6.51 | (16) ? [v0: ty] : (list(elt1) = v0 & ty(v0) & ! [v1: list_elt] : ! [v2: % 42.70/6.51 | uni] : ( ~ (t2tb(v1) = v2) | ~ list_elt(v1) | sort(v0, v2) = 0)) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (sorted_Nil) implies: % 42.70/6.51 | (17) ? [v0: uni] : ? [v1: list_elt] : (sorted(v1) = 0 & tb2t(v0) = v1 & % 42.70/6.51 | nil(elt1) = v0 & list_elt(v1) & uni(v0)) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (t2tb_sort1) implies: % 42.70/6.51 | (18) ! [v0: elt] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ elt(v0) | % 42.70/6.51 | sort(elt1, v1) = 0) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (sorted_One) implies: % 42.70/6.51 | (19) ? [v0: uni] : (nil(elt1) = v0 & uni(v0) & ! [v1: elt] : ! [v2: uni] % 42.70/6.51 | : ( ~ (t2tb1(v1) = v2) | ~ elt(v1) | ? [v3: uni] : ? [v4: % 42.70/6.51 | list_elt] : (sorted(v4) = 0 & tb2t(v3) = v4 & cons(elt1, v2, v0) % 42.70/6.51 | = v3 & list_elt(v4) & uni(v3)))) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (sorted_inversion) implies: % 42.70/6.51 | (20) ? [v0: uni] : ? [v1: list_elt] : (tb2t(v0) = v1 & nil(elt1) = v0 & % 42.70/6.51 | list_elt(v1) & uni(v0) & ! [v2: list_elt] : (v2 = v1 | ~ % 42.70/6.51 | (sorted(v2) = 0) | ~ list_elt(v2) | ? [v3: elt] : ? [v4: elt] : % 42.70/6.51 | ? [v5: list_elt] : ? [v6: int] : ? [v7: uni] : ? [v8: uni] : % 42.70/6.51 | ? [v9: uni] : ? [v10: list_elt] : ? [v11: int] : ? [v12: uni] : % 42.70/6.51 | ? [v13: uni] : ? [v14: list_elt] : ? [v15: elt] : ? [v16: uni] % 42.70/6.51 | : ? [v17: uni] : ? [v18: list_elt] : (list_elt(v5) & elt(v15) & % 42.70/6.51 | elt(v4) & elt(v3) & ((v18 = v2 & t2tb1(v15) = v16 & tb2t(v17) = % 42.70/6.51 | v2 & cons(elt1, v16, v0) = v17 & uni(v17) & uni(v16)) | (v14 % 42.70/6.51 | = v2 & v11 = 0 & v6 = 0 & t2tb1(v4) = v7 & t2tb1(v3) = v12 & % 42.70/6.51 | sorted(v10) = 0 & tb2t(v13) = v2 & tb2t(v9) = v10 & t2tb(v5) % 42.70/6.51 | = v8 & le(v3, v4) = 0 & cons(elt1, v12, v9) = v13 & % 42.70/6.51 | cons(elt1, v7, v8) = v9 & list_elt(v10) & uni(v13) & % 42.70/6.51 | uni(v12) & uni(v9) & uni(v8) & uni(v7)))))) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (sorted_mem) implies: % 42.70/6.51 | (21) ! [v0: elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! % 42.70/6.51 | [v4: uni] : ( ~ (t2tb1(v0) = v2) | ~ (t2tb(v1) = v3) | ~ (cons(elt1, % 42.70/6.51 | v2, v3) = v4) | ~ list_elt(v1) | ~ elt(v0) | ? [v5: list_elt] % 42.70/6.51 | : ? [v6: any] : ? [v7: any] : (sorted(v5) = v6 & sorted(v1) = v7 & % 42.70/6.51 | tb2t(v4) = v5 & list_elt(v5) & ( ~ (v6 = 0) | (v7 = 0 & ! [v8: % 42.70/6.51 | elt] : ! [v9: int] : (v9 = 0 | ~ (le(v0, v8) = v9) | ~ % 42.70/6.51 | elt(v8) | ? [v10: uni] : ? [v11: int] : ( ~ (v11 = 0) & % 42.70/6.51 | t2tb1(v8) = v10 & mem(elt1, v10, v3) = v11 & uni(v10))) & % 42.70/6.51 | ! [v8: elt] : ! [v9: uni] : ( ~ (t2tb1(v8) = v9) | ~ elt(v8) % 42.70/6.51 | | ? [v10: any] : ? [v11: any] : (le(v0, v8) = v11 & % 42.70/6.51 | mem(elt1, v9, v3) = v10 & ( ~ (v10 = 0) | v11 = 0))))))) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (sorted_append) implies: % 42.70/6.51 | (22) ! [v0: list_elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : % 42.70/6.51 | ! [v4: uni] : ( ~ (t2tb(v1) = v3) | ~ (t2tb(v0) = v2) | ~ % 42.70/6.51 | (infix_plpl(elt1, v2, v3) = v4) | ~ list_elt(v1) | ~ list_elt(v0) % 42.70/6.51 | | ? [v5: any] : ? [v6: any] : ? [v7: list_elt] : ? [v8: any] : % 42.70/6.51 | ? [v9: elt] : ? [v10: elt] : ? [v11: uni] : ? [v12: int] : ? % 42.70/6.51 | [v13: uni] : ? [v14: int] : ? [v15: int] : (elt(v10) & elt(v9) & % 42.70/6.51 | ((v14 = 0 & v12 = 0 & ~ (v15 = 0) & t2tb1(v10) = v13 & t2tb1(v9) % 42.70/6.51 | = v11 & le(v9, v10) = v15 & mem(elt1, v13, v3) = 0 & mem(elt1, % 42.70/6.51 | v11, v2) = 0 & uni(v13) & uni(v11)) | (sorted(v7) = v8 & % 42.70/6.51 | sorted(v1) = v6 & sorted(v0) = v5 & tb2t(v4) = v7 & % 42.70/6.51 | list_elt(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | v8 = 0))))) % 42.70/6.51 | % 42.70/6.51 | ALPHA: (rev_append_def) implies: % 42.70/6.52 | (23) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.70/6.52 | uni] : ! [v5: uni] : ( ~ (rev_append(v0, v4, v1) = v5) | ~ % 42.70/6.52 | (cons(v0, v2, v3) = v4) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ~ % 42.70/6.52 | uni(v1) | ? [v6: uni] : (rev_append(v0, v3, v6) = v5 & cons(v0, v2, % 42.70/6.52 | v1) = v6 & uni(v6) & uni(v5))) % 42.70/6.52 | % 42.70/6.52 | ALPHA: (rev_append_def1) implies: % 42.70/6.52 | (24) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ % 42.70/6.52 | (rev_append(v0, v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) % 42.70/6.52 | | ? [v4: uni] : (reverse(v0, v1) = v4 & infix_plpl(v0, v4, v2) = v3 % 42.70/6.52 | & uni(v4) & uni(v3))) % 42.70/6.52 | (25) ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.70/6.52 | uni] : ( ~ (reverse(v0, v1) = v3) | ~ (infix_plpl(v0, v3, v2) = v4) % 42.70/6.52 | | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | (rev_append(v0, v1, v2) = v4 % 42.70/6.52 | & uni(v4))) % 42.70/6.52 | % 42.70/6.52 | ALPHA: (sorted_reverse_cons2) implies: % 42.70/6.52 | (26) ! [v0: elt] : ! [v1: list_elt] : ! [v2: uni] : ! [v3: uni] : ! % 42.70/6.52 | [v4: uni] : ( ~ (t2tb1(v0) = v2) | ~ (t2tb(v1) = v3) | ~ (cons(elt1, % 42.70/6.52 | v2, v3) = v4) | ~ list_elt(v1) | ~ elt(v0) | ? [v5: uni] : ? % 42.70/6.52 | [v6: list_elt] : ? [v7: any] : ? [v8: uni] : ? [v9: list_elt] : % 42.70/6.52 | ? [v10: any] : (sorted(v9) = v10 & sorted(v6) = v7 & tb2t(v8) = v9 & % 42.70/6.52 | tb2t(v5) = v6 & reverse(elt1, v4) = v5 & reverse(elt1, v3) = v8 & % 42.70/6.52 | list_elt(v9) & list_elt(v6) & uni(v8) & uni(v5) & ( ~ (v7 = 0) | % 42.70/6.52 | v10 = 0))) % 42.70/6.52 | % 42.70/6.52 | ALPHA: (wP_parameter_rev_merge_rev) implies: % 42.70/6.52 | (27) ty(elt1) % 42.70/6.52 | (28) ? [v0: uni] : ? [v1: list_elt] : ? [v2: list_elt] : ? [v3: % 42.70/6.52 | list_elt] : ? [v4: uni] : ? [v5: uni] : ? [v6: list_elt] : ? % 42.70/6.52 | [v7: uni] : ? [v8: uni] : ? [v9: list_elt] : ? [v10: uni] : ? % 42.70/6.52 | [v11: uni] : ? [v12: list_elt] : ? [v13: int] : ? [v14: elt] : ? % 42.70/6.52 | [v15: list_elt] : ? [v16: uni] : ? [v17: uni] : ? [v18: uni] : ( ~ % 42.70/6.52 | (v13 = 0) & rev_append(elt1, v7, v10) = v11 & t2tb1(v14) = v16 & % 42.70/6.52 | sorted(v12) = v13 & sorted(v9) = 0 & sorted(v6) = 0 & sorted(v3) = 0 % 42.70/6.52 | & tb2t(v18) = v2 & tb2t(v11) = v12 & tb2t(v8) = v9 & tb2t(v5) = v6 & % 42.70/6.52 | tb2t(v0) = v1 & t2tb(v15) = v17 & t2tb(v3) = v10 & t2tb(v2) = v7 & % 42.70/6.52 | t2tb(v1) = v4 & reverse(elt1, v7) = v8 & reverse(elt1, v4) = v5 & % 42.70/6.52 | cons(elt1, v16, v17) = v18 & nil(elt1) = v0 & list_elt(v15) & % 42.70/6.52 | list_elt(v12) & list_elt(v9) & list_elt(v6) & list_elt(v3) & % 42.70/6.52 | list_elt(v2) & list_elt(v1) & elt(v14) & uni(v18) & uni(v17) & % 42.70/6.52 | uni(v16) & uni(v11) & uni(v10) & uni(v8) & uni(v7) & uni(v5) & % 42.70/6.52 | uni(v4) & uni(v0) & ! [v19: elt] : ! [v20: elt] : ! [v21: int] : % 42.70/6.52 | (v21 = 0 | ~ (le(v20, v19) = v21) | ~ elt(v20) | ~ elt(v19) | ? % 42.70/6.52 | [v22: uni] : ? [v23: any] : ? [v24: uni] : ? [v25: any] : % 42.70/6.52 | (t2tb1(v20) = v24 & t2tb1(v19) = v22 & mem(elt1, v24, v7) = v25 & % 42.70/6.52 | mem(elt1, v22, v10) = v23 & uni(v24) & uni(v22) & ( ~ (v25 = 0) % 42.70/6.52 | | ~ (v23 = 0)))) & ! [v19: elt] : ! [v20: elt] : ! [v21: % 42.70/6.52 | int] : (v21 = 0 | ~ (le(v20, v19) = v21) | ~ elt(v20) | ~ % 42.70/6.52 | elt(v19) | ? [v22: uni] : ? [v23: any] : ? [v24: uni] : ? % 42.70/6.52 | [v25: any] : (t2tb1(v20) = v24 & t2tb1(v19) = v22 & mem(elt1, v24, % 42.70/6.52 | v4) = v25 & mem(elt1, v22, v10) = v23 & uni(v24) & uni(v22) & % 42.70/6.52 | ( ~ (v25 = 0) | ~ (v23 = 0))))) % 42.70/6.52 | % 42.70/6.52 | ALPHA: (function-axioms) implies: % 42.70/6.52 | (29) ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = % 42.70/6.52 | v1) | ~ (nil(v2) = v0)) % 42.70/6.52 | (30) ! [v0: uni] : ! [v1: uni] : ! [v2: list_elt] : (v1 = v0 | ~ % 42.70/6.52 | (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) % 42.70/6.52 | (31) ! [v0: list_elt] : ! [v1: list_elt] : ! [v2: uni] : (v1 = v0 | ~ % 42.70/6.52 | (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 42.70/6.52 | (32) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 42.70/6.52 | list_elt] : (v1 = v0 | ~ (sorted(v2) = v1) | ~ (sorted(v2) = v0)) % 42.70/6.52 | (33) ! [v0: uni] : ! [v1: uni] : ! [v2: elt] : (v1 = v0 | ~ (t2tb1(v2) % 42.70/6.52 | = v1) | ~ (t2tb1(v2) = v0)) % 42.70/6.52 | (34) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 42.70/6.52 | : ! [v3: ty] : (v1 = v0 | ~ (sort(v3, v2) = v1) | ~ (sort(v3, v2) = % 42.70/6.52 | v0)) % 42.70/6.52 | (35) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 42.70/6.52 | ~ (length(v3, v2) = v1) | ~ (length(v3, v2) = v0)) % 42.70/6.52 | (36) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 42.70/6.52 | ~ (reverse(v3, v2) = v1) | ~ (reverse(v3, v2) = v0)) % 42.70/6.52 | (37) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.70/6.52 | ty] : (v1 = v0 | ~ (cons(v4, v3, v2) = v1) | ~ (cons(v4, v3, v2) = % 42.70/6.52 | v0)) % 42.70/6.52 | (38) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 42.70/6.52 | : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (mem(v4, v3, v2) = v1) | % 42.70/6.52 | ~ (mem(v4, v3, v2) = v0)) % 42.70/6.52 | % 42.70/6.52 | DELTA: instantiating (17) with fresh symbols all_89_0, all_89_1 gives: % 42.70/6.53 | (39) sorted(all_89_0) = 0 & tb2t(all_89_1) = all_89_0 & nil(elt1) = % 42.70/6.53 | all_89_1 & list_elt(all_89_0) & uni(all_89_1) % 42.70/6.53 | % 42.70/6.53 | ALPHA: (39) implies: % 42.70/6.53 | (40) nil(elt1) = all_89_1 % 42.70/6.53 | (41) tb2t(all_89_1) = all_89_0 % 42.70/6.53 | % 42.70/6.53 | DELTA: instantiating (16) with fresh symbol all_91_0 gives: % 42.70/6.53 | (42) list(elt1) = all_91_0 & ty(all_91_0) & ! [v0: list_elt] : ! [v1: % 42.70/6.53 | uni] : ( ~ (t2tb(v0) = v1) | ~ list_elt(v0) | sort(all_91_0, v1) = % 42.70/6.53 | 0) % 42.70/6.53 | % 42.70/6.53 | ALPHA: (42) implies: % 42.70/6.53 | (43) list(elt1) = all_91_0 % 42.70/6.53 | % 42.70/6.53 | DELTA: instantiating (19) with fresh symbol all_94_0 gives: % 42.70/6.53 | (44) nil(elt1) = all_94_0 & uni(all_94_0) & ! [v0: elt] : ! [v1: uni] : ( % 42.70/6.53 | ~ (t2tb1(v0) = v1) | ~ elt(v0) | ? [v2: uni] : ? [v3: list_elt] : % 42.70/6.53 | (sorted(v3) = 0 & tb2t(v2) = v3 & cons(elt1, v1, all_94_0) = v2 & % 42.70/6.53 | list_elt(v3) & uni(v2))) % 42.70/6.53 | % 42.70/6.53 | ALPHA: (44) implies: % 42.70/6.53 | (45) nil(elt1) = all_94_0 % 42.70/6.53 | (46) ! [v0: elt] : ! [v1: uni] : ( ~ (t2tb1(v0) = v1) | ~ elt(v0) | ? % 42.70/6.53 | [v2: uni] : ? [v3: list_elt] : (sorted(v3) = 0 & tb2t(v2) = v3 & % 42.70/6.53 | cons(elt1, v1, all_94_0) = v2 & list_elt(v3) & uni(v2))) % 42.70/6.53 | % 42.70/6.53 | DELTA: instantiating (20) with fresh symbols all_97_0, all_97_1 gives: % 42.70/6.53 | (47) tb2t(all_97_1) = all_97_0 & nil(elt1) = all_97_1 & list_elt(all_97_0) % 42.70/6.53 | & uni(all_97_1) & ! [v0: any] : (v0 = all_97_0 | ~ (sorted(v0) = 0) % 42.70/6.53 | | ~ list_elt(v0) | ? [v1: elt] : ? [v2: elt] : ? [v3: list_elt] % 42.70/6.53 | : ? [v4: int] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? % 42.70/6.53 | [v8: list_elt] : ? [v9: int] : ? [v10: uni] : ? [v11: uni] : ? % 42.70/6.53 | [v12: any] : ? [v13: elt] : ? [v14: uni] : ? [v15: uni] : ? % 42.70/6.53 | [v16: any] : (list_elt(v3) & elt(v13) & elt(v2) & elt(v1) & ((v16 = % 42.70/6.53 | v0 & t2tb1(v13) = v14 & tb2t(v15) = v0 & cons(elt1, v14, % 42.70/6.53 | all_97_1) = v15 & uni(v15) & uni(v14)) | (v12 = v0 & v9 = 0 % 42.70/6.53 | & v4 = 0 & t2tb1(v2) = v5 & t2tb1(v1) = v10 & sorted(v8) = 0 & % 42.70/6.53 | tb2t(v11) = v0 & tb2t(v7) = v8 & t2tb(v3) = v6 & le(v1, v2) = % 42.70/6.53 | 0 & cons(elt1, v10, v7) = v11 & cons(elt1, v5, v6) = v7 & % 42.70/6.53 | list_elt(v8) & uni(v11) & uni(v10) & uni(v7) & uni(v6) & % 42.70/6.53 | uni(v5))))) % 42.70/6.53 | % 42.70/6.53 | ALPHA: (47) implies: % 42.70/6.53 | (48) list_elt(all_97_0) % 42.70/6.53 | (49) nil(elt1) = all_97_1 % 42.70/6.53 | (50) tb2t(all_97_1) = all_97_0 % 42.70/6.53 | % 42.70/6.53 | DELTA: instantiating (28) with fresh symbols all_100_0, all_100_1, all_100_2, % 42.70/6.53 | all_100_3, all_100_4, all_100_5, all_100_6, all_100_7, all_100_8, % 42.70/6.53 | all_100_9, all_100_10, all_100_11, all_100_12, all_100_13, all_100_14, % 42.70/6.53 | all_100_15, all_100_16, all_100_17, all_100_18 gives: % 42.70/6.53 | (51) ~ (all_100_5 = 0) & rev_append(elt1, all_100_11, all_100_8) = % 42.70/6.53 | all_100_7 & t2tb1(all_100_4) = all_100_2 & sorted(all_100_6) = % 42.70/6.53 | all_100_5 & sorted(all_100_9) = 0 & sorted(all_100_12) = 0 & % 42.70/6.53 | sorted(all_100_15) = 0 & tb2t(all_100_0) = all_100_16 & % 42.70/6.53 | tb2t(all_100_7) = all_100_6 & tb2t(all_100_10) = all_100_9 & % 42.70/6.53 | tb2t(all_100_13) = all_100_12 & tb2t(all_100_18) = all_100_17 & % 42.70/6.53 | t2tb(all_100_3) = all_100_1 & t2tb(all_100_15) = all_100_8 & % 42.70/6.53 | t2tb(all_100_16) = all_100_11 & t2tb(all_100_17) = all_100_14 & % 42.70/6.53 | reverse(elt1, all_100_11) = all_100_10 & reverse(elt1, all_100_14) = % 42.70/6.53 | all_100_13 & cons(elt1, all_100_2, all_100_1) = all_100_0 & nil(elt1) % 42.70/6.53 | = all_100_18 & list_elt(all_100_3) & list_elt(all_100_6) & % 42.70/6.53 | list_elt(all_100_9) & list_elt(all_100_12) & list_elt(all_100_15) & % 42.70/6.53 | list_elt(all_100_16) & list_elt(all_100_17) & elt(all_100_4) & % 42.70/6.53 | uni(all_100_0) & uni(all_100_1) & uni(all_100_2) & uni(all_100_7) & % 42.70/6.53 | uni(all_100_8) & uni(all_100_10) & uni(all_100_11) & uni(all_100_13) & % 42.70/6.53 | uni(all_100_14) & uni(all_100_18) & ! [v0: elt] : ! [v1: elt] : ! % 42.70/6.53 | [v2: int] : (v2 = 0 | ~ (le(v1, v0) = v2) | ~ elt(v1) | ~ elt(v0) | % 42.70/6.53 | ? [v3: uni] : ? [v4: any] : ? [v5: uni] : ? [v6: any] : % 42.70/6.53 | (t2tb1(v1) = v5 & t2tb1(v0) = v3 & mem(elt1, v5, all_100_11) = v6 & % 42.70/6.53 | mem(elt1, v3, all_100_8) = v4 & uni(v5) & uni(v3) & ( ~ (v6 = 0) | % 42.70/6.53 | ~ (v4 = 0)))) & ! [v0: elt] : ! [v1: elt] : ! [v2: int] : % 42.70/6.53 | (v2 = 0 | ~ (le(v1, v0) = v2) | ~ elt(v1) | ~ elt(v0) | ? [v3: % 42.70/6.53 | uni] : ? [v4: any] : ? [v5: uni] : ? [v6: any] : (t2tb1(v1) = % 42.70/6.53 | v5 & t2tb1(v0) = v3 & mem(elt1, v5, all_100_14) = v6 & mem(elt1, % 42.70/6.53 | v3, all_100_8) = v4 & uni(v5) & uni(v3) & ( ~ (v6 = 0) | ~ (v4 % 42.70/6.53 | = 0)))) % 42.70/6.53 | % 42.70/6.53 | ALPHA: (51) implies: % 42.70/6.53 | (52) ~ (all_100_5 = 0) % 42.70/6.53 | (53) uni(all_100_13) % 42.70/6.53 | (54) uni(all_100_11) % 42.70/6.53 | (55) uni(all_100_10) % 42.70/6.53 | (56) uni(all_100_8) % 42.70/6.53 | (57) uni(all_100_2) % 42.70/6.53 | (58) uni(all_100_1) % 42.70/6.53 | (59) uni(all_100_0) % 42.70/6.53 | (60) elt(all_100_4) % 42.70/6.53 | (61) list_elt(all_100_15) % 42.70/6.53 | (62) list_elt(all_100_12) % 42.70/6.53 | (63) list_elt(all_100_3) % 42.70/6.53 | (64) nil(elt1) = all_100_18 % 42.70/6.53 | (65) cons(elt1, all_100_2, all_100_1) = all_100_0 % 42.70/6.53 | (66) reverse(elt1, all_100_14) = all_100_13 % 42.70/6.53 | (67) reverse(elt1, all_100_11) = all_100_10 % 42.70/6.53 | (68) t2tb(all_100_17) = all_100_14 % 42.70/6.54 | (69) t2tb(all_100_16) = all_100_11 % 42.70/6.54 | (70) t2tb(all_100_15) = all_100_8 % 42.70/6.54 | (71) t2tb(all_100_3) = all_100_1 % 42.70/6.54 | (72) tb2t(all_100_18) = all_100_17 % 42.70/6.54 | (73) tb2t(all_100_13) = all_100_12 % 42.70/6.54 | (74) tb2t(all_100_10) = all_100_9 % 42.70/6.54 | (75) tb2t(all_100_7) = all_100_6 % 42.70/6.54 | (76) tb2t(all_100_0) = all_100_16 % 42.70/6.54 | (77) sorted(all_100_15) = 0 % 42.70/6.54 | (78) sorted(all_100_9) = 0 % 42.70/6.54 | (79) sorted(all_100_6) = all_100_5 % 42.70/6.54 | (80) t2tb1(all_100_4) = all_100_2 % 42.70/6.54 | (81) rev_append(elt1, all_100_11, all_100_8) = all_100_7 % 42.70/6.54 | (82) ! [v0: elt] : ! [v1: elt] : ! [v2: int] : (v2 = 0 | ~ (le(v1, v0) % 42.70/6.54 | = v2) | ~ elt(v1) | ~ elt(v0) | ? [v3: uni] : ? [v4: any] : ? % 42.70/6.54 | [v5: uni] : ? [v6: any] : (t2tb1(v1) = v5 & t2tb1(v0) = v3 & % 42.70/6.54 | mem(elt1, v5, all_100_14) = v6 & mem(elt1, v3, all_100_8) = v4 & % 42.70/6.54 | uni(v5) & uni(v3) & ( ~ (v6 = 0) | ~ (v4 = 0)))) % 42.70/6.54 | (83) ! [v0: elt] : ! [v1: elt] : ! [v2: int] : (v2 = 0 | ~ (le(v1, v0) % 42.70/6.54 | = v2) | ~ elt(v1) | ~ elt(v0) | ? [v3: uni] : ? [v4: any] : ? % 42.70/6.54 | [v5: uni] : ? [v6: any] : (t2tb1(v1) = v5 & t2tb1(v0) = v3 & % 42.70/6.54 | mem(elt1, v5, all_100_11) = v6 & mem(elt1, v3, all_100_8) = v4 & % 42.70/6.54 | uni(v5) & uni(v3) & ( ~ (v6 = 0) | ~ (v4 = 0)))) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (29) with all_94_0, all_97_1, elt1, simplifying % 42.70/6.54 | with (45), (49) gives: % 42.70/6.54 | (84) all_97_1 = all_94_0 % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (29) with all_97_1, all_100_18, elt1, simplifying % 42.70/6.54 | with (49), (64) gives: % 42.70/6.54 | (85) all_100_18 = all_97_1 % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (29) with all_89_1, all_100_18, elt1, simplifying % 42.70/6.54 | with (40), (64) gives: % 42.70/6.54 | (86) all_100_18 = all_89_1 % 42.70/6.54 | % 42.70/6.54 | COMBINE_EQS: (85), (86) imply: % 42.70/6.54 | (87) all_97_1 = all_89_1 % 42.70/6.54 | % 42.70/6.54 | SIMP: (87) implies: % 42.70/6.54 | (88) all_97_1 = all_89_1 % 42.70/6.54 | % 42.70/6.54 | COMBINE_EQS: (84), (88) imply: % 42.70/6.54 | (89) all_94_0 = all_89_1 % 42.70/6.54 | % 42.70/6.54 | REDUCE: (72), (86) imply: % 42.70/6.54 | (90) tb2t(all_89_1) = all_100_17 % 42.70/6.54 | % 42.70/6.54 | REDUCE: (50), (88) imply: % 42.70/6.54 | (91) tb2t(all_89_1) = all_97_0 % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (31) with all_89_0, all_100_17, all_89_1, % 42.70/6.54 | simplifying with (41), (90) gives: % 42.70/6.54 | (92) all_100_17 = all_89_0 % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (31) with all_97_0, all_100_17, all_89_1, % 42.70/6.54 | simplifying with (90), (91) gives: % 42.70/6.54 | (93) all_100_17 = all_97_0 % 42.70/6.54 | % 42.70/6.54 | COMBINE_EQS: (92), (93) imply: % 42.70/6.54 | (94) all_97_0 = all_89_0 % 42.70/6.54 | % 42.70/6.54 | REDUCE: (68), (92) imply: % 42.70/6.54 | (95) t2tb(all_89_0) = all_100_14 % 42.70/6.54 | % 42.70/6.54 | REDUCE: (48), (94) imply: % 42.70/6.54 | (96) list_elt(all_89_0) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (1) with elt1, all_91_0, simplifying with (27), % 42.70/6.54 | (43) gives: % 42.70/6.54 | (97) ? [v0: uni] : (nil(elt1) = v0 & sort(all_91_0, v0) = 0 & uni(v0)) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (8) with elt1, all_89_1, simplifying with (27), % 42.70/6.54 | (40) gives: % 42.70/6.54 | (98) reverse(elt1, all_89_1) = all_89_1 & uni(all_89_1) % 42.70/6.54 | % 42.70/6.54 | ALPHA: (98) implies: % 42.70/6.54 | (99) uni(all_89_1) % 42.70/6.54 | (100) reverse(elt1, all_89_1) = all_89_1 % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (11) with elt1, all_100_1, all_100_2, all_100_0, % 42.70/6.54 | simplifying with (27), (57), (58), (65) gives: % 42.70/6.54 | (101) ? [v0: uni] : ? [v1: uni] : ? [v2: uni] : ? [v3: uni] : % 42.70/6.54 | (reverse(elt1, all_100_0) = v0 & reverse(elt1, all_100_1) = v1 & % 42.70/6.54 | infix_plpl(elt1, v1, v3) = v0 & cons(elt1, all_100_2, v2) = v3 & % 42.70/6.54 | nil(elt1) = v2 & uni(v3) & uni(v2) & uni(v1) & uni(v0)) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (cons_proj_1_def) with elt1, all_100_2, all_100_1, % 42.70/6.54 | all_100_0, simplifying with (27), (57), (58), (65) gives: % 42.70/6.54 | (102) ? [v0: any] : ? [v1: uni] : (cons_proj_1(elt1, all_100_0) = v1 & % 42.70/6.54 | sort(elt1, all_100_2) = v0 & uni(v1) & ( ~ (v0 = 0) | v1 = % 42.70/6.54 | all_100_2)) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (nil_Cons) with elt1, all_100_2, all_100_1, % 42.70/6.54 | all_100_0, simplifying with (27), (57), (58), (65) gives: % 42.70/6.54 | (103) ? [v0: any] : ( ~ (v0 = all_100_0) & nil(elt1) = v0 & uni(v0)) % 42.70/6.54 | % 42.70/6.54 | GROUND_INST: instantiating (2) with elt1, all_100_2, all_100_1, all_100_0, % 42.70/6.54 | simplifying with (27), (57), (58), (65) gives: % 42.70/6.54 | (104) ? [v0: int] : (length(elt1, all_100_0) = v0 & length(elt1, % 42.70/6.54 | all_100_1) = $sum(v0, -1)) % 42.70/6.54 | % 42.70/6.55 | GROUND_INST: instantiating (reverse_reverse) with elt1, all_100_11, % 42.70/6.55 | all_100_10, simplifying with (27), (54), (67) gives: % 42.70/6.55 | (105) reverse(elt1, all_100_10) = all_100_11 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (14) with elt1, all_100_11, all_100_10, simplifying % 42.70/6.55 | with (27), (54), (67) gives: % 42.70/6.55 | (106) ? [v0: int] : (length(elt1, all_100_10) = v0 & length(elt1, % 42.70/6.55 | all_100_11) = v0) % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (bridgeL) with all_89_0, all_100_14, simplifying % 42.70/6.55 | with (95), (96) gives: % 42.70/6.55 | (107) tb2t(all_100_14) = all_89_0 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (bridgeR) with all_89_1, all_89_0, simplifying with % 42.70/6.55 | (41), (99) gives: % 42.70/6.55 | (108) t2tb(all_89_0) = all_89_1 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (bridgeR) with all_100_13, all_100_12, simplifying % 42.70/6.55 | with (53), (73) gives: % 42.70/6.55 | (109) t2tb(all_100_12) = all_100_13 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (bridgeR) with all_100_10, all_100_9, simplifying % 42.70/6.55 | with (55), (74) gives: % 42.70/6.55 | (110) t2tb(all_100_9) = all_100_10 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (bridgeR) with all_100_0, all_100_16, simplifying % 42.70/6.55 | with (59), (76) gives: % 42.70/6.55 | (111) t2tb(all_100_16) = all_100_0 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (26) with all_100_4, all_100_3, all_100_2, % 42.70/6.55 | all_100_1, all_100_0, simplifying with (60), (63), (65), (71), % 42.70/6.55 | (80) gives: % 42.70/6.55 | (112) ? [v0: uni] : ? [v1: list_elt] : ? [v2: any] : ? [v3: uni] : ? % 42.70/6.55 | [v4: list_elt] : ? [v5: any] : (sorted(v4) = v5 & sorted(v1) = v2 & % 42.70/6.55 | tb2t(v3) = v4 & tb2t(v0) = v1 & reverse(elt1, all_100_0) = v0 & % 42.70/6.55 | reverse(elt1, all_100_1) = v3 & list_elt(v4) & list_elt(v1) & % 42.70/6.55 | uni(v3) & uni(v0) & ( ~ (v2 = 0) | v5 = 0)) % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (18) with all_100_4, all_100_2, simplifying with % 42.70/6.55 | (60), (80) gives: % 42.70/6.55 | (113) sort(elt1, all_100_2) = 0 % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (46) with all_100_4, all_100_2, simplifying with % 42.70/6.55 | (60), (80) gives: % 42.70/6.55 | (114) ? [v0: uni] : ? [v1: list_elt] : (sorted(v1) = 0 & tb2t(v0) = v1 & % 42.70/6.55 | cons(elt1, all_100_2, all_94_0) = v0 & list_elt(v1) & uni(v0)) % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (rev_append_length) with elt1, all_100_11, % 42.70/6.55 | all_100_8, all_100_7, simplifying with (27), (54), (56), (81) % 42.70/6.55 | gives: % 42.70/6.55 | (115) ? [v0: int] : ? [v1: int] : (length(elt1, all_100_7) = v0 & % 42.70/6.55 | length(elt1, all_100_8) = $difference(v0, v1) & length(elt1, % 42.70/6.55 | all_100_11) = v1) % 42.70/6.55 | % 42.70/6.55 | GROUND_INST: instantiating (24) with elt1, all_100_11, all_100_8, all_100_7, % 42.70/6.55 | simplifying with (27), (54), (56), (81) gives: % 42.70/6.55 | (116) ? [v0: uni] : (reverse(elt1, all_100_11) = v0 & infix_plpl(elt1, v0, % 42.70/6.55 | all_100_8) = all_100_7 & uni(v0) & uni(all_100_7)) % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (106) with fresh symbol all_121_0 gives: % 42.70/6.55 | (117) length(elt1, all_100_10) = all_121_0 & length(elt1, all_100_11) = % 42.70/6.55 | all_121_0 % 42.70/6.55 | % 42.70/6.55 | ALPHA: (117) implies: % 42.70/6.55 | (118) length(elt1, all_100_11) = all_121_0 % 42.70/6.55 | (119) length(elt1, all_100_10) = all_121_0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (104) with fresh symbol all_123_0 gives: % 42.70/6.55 | (120) length(elt1, all_100_0) = all_123_0 & length(elt1, all_100_1) = % 42.70/6.55 | $sum(all_123_0, -1) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (120) implies: % 42.70/6.55 | (121) length(elt1, all_100_1) = $sum(all_123_0, -1) % 42.70/6.55 | (122) length(elt1, all_100_0) = all_123_0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (97) with fresh symbol all_129_0 gives: % 42.70/6.55 | (123) nil(elt1) = all_129_0 & sort(all_91_0, all_129_0) = 0 & % 42.70/6.55 | uni(all_129_0) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (123) implies: % 42.70/6.55 | (124) nil(elt1) = all_129_0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (115) with fresh symbols all_133_0, all_133_1 gives: % 42.70/6.55 | (125) length(elt1, all_100_7) = all_133_1 & length(elt1, all_100_8) = % 42.70/6.55 | $difference(all_133_1, all_133_0) & length(elt1, all_100_11) = % 42.70/6.55 | all_133_0 % 42.70/6.55 | % 42.70/6.55 | ALPHA: (125) implies: % 42.70/6.55 | (126) length(elt1, all_100_11) = all_133_0 % 42.70/6.55 | (127) length(elt1, all_100_8) = $difference(all_133_1, all_133_0) % 42.70/6.55 | (128) length(elt1, all_100_7) = all_133_1 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (103) with fresh symbol all_139_0 gives: % 42.70/6.55 | (129) ~ (all_139_0 = all_100_0) & nil(elt1) = all_139_0 & uni(all_139_0) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (129) implies: % 42.70/6.55 | (130) nil(elt1) = all_139_0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (116) with fresh symbol all_143_0 gives: % 42.70/6.55 | (131) reverse(elt1, all_100_11) = all_143_0 & infix_plpl(elt1, all_143_0, % 42.70/6.55 | all_100_8) = all_100_7 & uni(all_143_0) & uni(all_100_7) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (131) implies: % 42.70/6.55 | (132) uni(all_100_7) % 42.70/6.55 | (133) infix_plpl(elt1, all_143_0, all_100_8) = all_100_7 % 42.70/6.55 | (134) reverse(elt1, all_100_11) = all_143_0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (114) with fresh symbols all_145_0, all_145_1 gives: % 42.70/6.55 | (135) sorted(all_145_0) = 0 & tb2t(all_145_1) = all_145_0 & cons(elt1, % 42.70/6.55 | all_100_2, all_94_0) = all_145_1 & list_elt(all_145_0) & % 42.70/6.55 | uni(all_145_1) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (135) implies: % 42.70/6.55 | (136) cons(elt1, all_100_2, all_94_0) = all_145_1 % 42.70/6.55 | (137) tb2t(all_145_1) = all_145_0 % 42.70/6.55 | (138) sorted(all_145_0) = 0 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (102) with fresh symbols all_147_0, all_147_1 gives: % 42.70/6.55 | (139) cons_proj_1(elt1, all_100_0) = all_147_0 & sort(elt1, all_100_2) = % 42.70/6.55 | all_147_1 & uni(all_147_0) & ( ~ (all_147_1 = 0) | all_147_0 = % 42.70/6.55 | all_100_2) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (139) implies: % 42.70/6.55 | (140) uni(all_147_0) % 42.70/6.55 | (141) sort(elt1, all_100_2) = all_147_1 % 42.70/6.55 | (142) ~ (all_147_1 = 0) | all_147_0 = all_100_2 % 42.70/6.55 | % 42.70/6.55 | DELTA: instantiating (101) with fresh symbols all_149_0, all_149_1, all_149_2, % 42.70/6.55 | all_149_3 gives: % 42.70/6.55 | (143) reverse(elt1, all_100_0) = all_149_3 & reverse(elt1, all_100_1) = % 42.70/6.55 | all_149_2 & infix_plpl(elt1, all_149_2, all_149_0) = all_149_3 & % 42.70/6.55 | cons(elt1, all_100_2, all_149_1) = all_149_0 & nil(elt1) = all_149_1 % 42.70/6.55 | & uni(all_149_0) & uni(all_149_1) & uni(all_149_2) & uni(all_149_3) % 42.70/6.55 | % 42.70/6.55 | ALPHA: (143) implies: % 42.70/6.55 | (144) nil(elt1) = all_149_1 % 42.70/6.55 | (145) cons(elt1, all_100_2, all_149_1) = all_149_0 % 42.70/6.55 | (146) infix_plpl(elt1, all_149_2, all_149_0) = all_149_3 % 42.70/6.55 | (147) reverse(elt1, all_100_1) = all_149_2 % 42.70/6.55 | (148) reverse(elt1, all_100_0) = all_149_3 % 42.70/6.55 | % 42.70/6.56 | DELTA: instantiating (112) with fresh symbols all_152_0, all_152_1, all_152_2, % 42.70/6.56 | all_152_3, all_152_4, all_152_5 gives: % 42.70/6.56 | (149) sorted(all_152_1) = all_152_0 & sorted(all_152_4) = all_152_3 & % 42.70/6.56 | tb2t(all_152_2) = all_152_1 & tb2t(all_152_5) = all_152_4 & % 42.70/6.56 | reverse(elt1, all_100_0) = all_152_5 & reverse(elt1, all_100_1) = % 42.70/6.56 | all_152_2 & list_elt(all_152_1) & list_elt(all_152_4) & % 42.70/6.56 | uni(all_152_2) & uni(all_152_5) & ( ~ (all_152_3 = 0) | all_152_0 = % 42.70/6.56 | 0) % 42.70/6.56 | % 42.70/6.56 | ALPHA: (149) implies: % 42.70/6.56 | (150) uni(all_152_5) % 42.70/6.56 | (151) uni(all_152_2) % 42.70/6.56 | (152) list_elt(all_152_4) % 42.70/6.56 | (153) reverse(elt1, all_100_1) = all_152_2 % 42.70/6.56 | (154) reverse(elt1, all_100_0) = all_152_5 % 42.70/6.56 | (155) tb2t(all_152_5) = all_152_4 % 42.70/6.56 | (156) sorted(all_152_4) = all_152_3 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (89), (136) imply: % 42.70/6.56 | (157) cons(elt1, all_100_2, all_89_1) = all_145_1 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (34) with 0, all_147_1, all_100_2, elt1, % 42.70/6.56 | simplifying with (113), (141) gives: % 42.70/6.56 | (158) all_147_1 = 0 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (29) with all_89_1, all_149_1, elt1, simplifying % 42.70/6.56 | with (40), (144) gives: % 42.70/6.56 | (159) all_149_1 = all_89_1 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (29) with all_139_0, all_149_1, elt1, simplifying % 42.70/6.56 | with (130), (144) gives: % 42.70/6.56 | (160) all_149_1 = all_139_0 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (29) with all_129_0, all_149_1, elt1, simplifying % 42.70/6.56 | with (124), (144) gives: % 42.70/6.56 | (161) all_149_1 = all_129_0 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (35) with all_121_0, all_133_0, all_100_11, elt1, % 42.70/6.56 | simplifying with (118), (126) gives: % 42.70/6.56 | (162) all_133_0 = all_121_0 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (36) with all_100_10, all_143_0, all_100_11, elt1, % 42.70/6.56 | simplifying with (67), (134) gives: % 42.70/6.56 | (163) all_143_0 = all_100_10 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (36) with all_149_2, all_152_2, all_100_1, elt1, % 42.70/6.56 | simplifying with (147), (153) gives: % 42.70/6.56 | (164) all_152_2 = all_149_2 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (36) with all_149_3, all_152_5, all_100_0, elt1, % 42.70/6.56 | simplifying with (148), (154) gives: % 42.70/6.56 | (165) all_152_5 = all_149_3 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (30) with all_100_14, all_89_1, all_89_0, % 42.70/6.56 | simplifying with (95), (108) gives: % 42.70/6.56 | (166) all_100_14 = all_89_1 % 42.70/6.56 | % 42.70/6.56 | GROUND_INST: instantiating (30) with all_100_11, all_100_0, all_100_16, % 42.70/6.56 | simplifying with (69), (111) gives: % 42.70/6.56 | (167) all_100_0 = all_100_11 % 42.70/6.56 | % 42.70/6.56 | COMBINE_EQS: (160), (161) imply: % 42.70/6.56 | (168) all_139_0 = all_129_0 % 42.70/6.56 | % 42.70/6.56 | COMBINE_EQS: (159), (160) imply: % 42.70/6.56 | (169) all_139_0 = all_89_1 % 42.70/6.56 | % 42.70/6.56 | COMBINE_EQS: (168), (169) imply: % 42.70/6.56 | (170) all_129_0 = all_89_1 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (155), (165) imply: % 42.70/6.56 | (171) tb2t(all_149_3) = all_152_4 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (148), (167) imply: % 42.70/6.56 | (172) reverse(elt1, all_100_11) = all_149_3 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (66), (166) imply: % 42.70/6.56 | (173) reverse(elt1, all_89_1) = all_100_13 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (133), (163) imply: % 42.70/6.56 | (174) infix_plpl(elt1, all_100_10, all_100_8) = all_100_7 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (122), (167) imply: % 42.70/6.56 | (175) length(elt1, all_100_11) = all_123_0 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (127), (162) imply: % 42.70/6.56 | (176) length(elt1, all_100_8) = $difference(all_133_1, all_121_0) % 42.70/6.56 | % 42.70/6.56 | REDUCE: (145), (159) imply: % 42.70/6.56 | (177) cons(elt1, all_100_2, all_89_1) = all_149_0 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (65), (167) imply: % 42.70/6.56 | (178) cons(elt1, all_100_2, all_100_1) = all_100_11 % 42.70/6.56 | % 42.70/6.56 | REDUCE: (151), (164) imply: % 42.70/6.56 | (179) uni(all_149_2) % 42.70/6.56 | % 42.70/6.56 | REDUCE: (150), (165) imply: % 42.70/6.56 | (180) uni(all_149_3) % 42.70/6.56 | % 42.70/6.56 | BETA: splitting (142) gives: % 42.70/6.56 | % 42.70/6.56 | Case 1: % 42.70/6.56 | | % 42.70/6.56 | | (181) ~ (all_147_1 = 0) % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (158), (181) imply: % 42.70/6.56 | | (182) $false % 42.70/6.56 | | % 42.70/6.56 | | CLOSE: (182) is inconsistent. % 42.70/6.56 | | % 42.70/6.56 | Case 2: % 42.70/6.56 | | % 42.70/6.56 | | (183) all_147_0 = all_100_2 % 42.70/6.56 | | % 42.70/6.56 | | GROUND_INST: instantiating (37) with all_145_1, all_149_0, all_89_1, % 42.70/6.56 | | all_100_2, elt1, simplifying with (157), (177) gives: % 42.70/6.56 | | (184) all_149_0 = all_145_1 % 42.70/6.56 | | % 42.70/6.56 | | GROUND_INST: instantiating (35) with all_121_0, all_123_0, all_100_11, elt1, % 42.70/6.56 | | simplifying with (118), (175) gives: % 42.70/6.56 | | (185) all_123_0 = all_121_0 % 42.70/6.56 | | % 42.70/6.56 | | GROUND_INST: instantiating (36) with all_89_1, all_100_13, all_89_1, elt1, % 42.70/6.56 | | simplifying with (100), (173) gives: % 42.70/6.56 | | (186) all_100_13 = all_89_1 % 42.70/6.56 | | % 42.70/6.56 | | GROUND_INST: instantiating (36) with all_100_10, all_149_3, all_100_11, % 42.70/6.56 | | elt1, simplifying with (67), (172) gives: % 42.70/6.56 | | (187) all_149_3 = all_100_10 % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (171), (187) imply: % 42.70/6.56 | | (188) tb2t(all_100_10) = all_152_4 % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (73), (186) imply: % 42.70/6.56 | | (189) tb2t(all_89_1) = all_100_12 % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (109), (186) imply: % 42.70/6.56 | | (190) t2tb(all_100_12) = all_89_1 % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (146), (184), (187) imply: % 42.70/6.56 | | (191) infix_plpl(elt1, all_149_2, all_145_1) = all_100_10 % 42.70/6.56 | | % 42.70/6.56 | | REDUCE: (121), (185) imply: % 42.70/6.56 | | (192) length(elt1, all_100_1) = $sum(all_121_0, -1) % 42.70/6.56 | | % 42.70/6.57 | | GROUND_INST: instantiating (31) with all_89_0, all_100_12, all_89_1, % 42.70/6.57 | | simplifying with (41), (189) gives: % 42.70/6.57 | | (193) all_100_12 = all_89_0 % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (31) with all_100_9, all_152_4, all_100_10, % 42.70/6.57 | | simplifying with (74), (188) gives: % 42.70/6.57 | | (194) all_152_4 = all_100_9 % 42.70/6.57 | | % 42.70/6.57 | | REDUCE: (156), (194) imply: % 42.70/6.57 | | (195) sorted(all_100_9) = all_152_3 % 42.70/6.57 | | % 42.70/6.57 | | REDUCE: (152), (194) imply: % 42.70/6.57 | | (196) list_elt(all_100_9) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (32) with 0, all_152_3, all_100_9, simplifying % 42.70/6.57 | | with (78), (195) gives: % 42.70/6.57 | | (197) all_152_3 = 0 % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (4) with elt1, all_100_2, simplifying with (27), % 42.70/6.57 | | (57), (113) gives: % 42.70/6.57 | | (198) ? [v0: uni] : ? [v1: int] : ( ~ (v1 = 0) & mem(elt1, all_100_2, % 42.70/6.57 | | v0) = v1 & nil(elt1) = v0 & uni(v0)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (6) with elt1, all_100_2, simplifying with (27), % 42.70/6.57 | | (57), (113) gives: % 42.70/6.57 | | (199) ? [v0: uni] : (num_occ(elt1, all_100_2, v0) = 0 & nil(elt1) = v0 & % 42.70/6.57 | | uni(v0)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (7) with elt1, all_100_2, all_100_2, all_89_1, % 42.70/6.57 | | all_145_1, simplifying with (27), (57), (99), (113), (157) % 42.70/6.57 | | gives: % 42.70/6.57 | | (200) ? [v0: any] : ? [v1: int] : ? [v2: int] : (num_occ(elt1, % 42.70/6.57 | | all_100_2, all_145_1) = v1 & num_occ(elt1, all_100_2, all_89_1) % 42.70/6.57 | | = v2 & sort(elt1, all_100_2) = v0 & ( ~ (v0 = 0) | % 42.70/6.57 | | $difference(v2, v1) = -1)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (5) with elt1, all_100_2, all_100_2, all_89_1, % 42.70/6.57 | | all_145_1, simplifying with (27), (57), (99), (113), (157) % 42.70/6.57 | | gives: % 42.70/6.57 | | (201) ? [v0: any] : ? [v1: any] : ? [v2: MultipleValueBool] : % 42.70/6.57 | | (mem(elt1, all_100_2, all_145_1) = v1 & mem(elt1, all_100_2, % 42.70/6.57 | | all_89_1) = v2 & sort(elt1, all_100_2) = v0 & ( ~ (v0 = 0) | v1 % 42.70/6.57 | | = 0)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (11) with elt1, all_89_1, all_100_2, all_145_1, % 42.70/6.57 | | simplifying with (27), (57), (99), (157) gives: % 42.70/6.57 | | (202) ? [v0: uni] : ? [v1: uni] : ? [v2: uni] : ? [v3: uni] : % 42.70/6.57 | | (reverse(elt1, all_145_1) = v0 & reverse(elt1, all_89_1) = v1 & % 42.70/6.57 | | infix_plpl(elt1, v1, v3) = v0 & cons(elt1, all_100_2, v2) = v3 & % 42.70/6.57 | | nil(elt1) = v2 & uni(v3) & uni(v2) & uni(v1) & uni(v0)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (cons_proj_1_def) with elt1, all_100_2, all_89_1, % 42.70/6.57 | | all_145_1, simplifying with (27), (57), (99), (157) gives: % 42.70/6.57 | | (203) ? [v0: any] : ? [v1: uni] : (cons_proj_1(elt1, all_145_1) = v1 & % 42.70/6.57 | | sort(elt1, all_100_2) = v0 & uni(v1) & ( ~ (v0 = 0) | v1 = % 42.70/6.57 | | all_100_2)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (nil_Cons) with elt1, all_100_2, all_89_1, % 42.70/6.57 | | all_145_1, simplifying with (27), (57), (99), (157) gives: % 42.70/6.57 | | (204) ? [v0: any] : ( ~ (v0 = all_145_1) & nil(elt1) = v0 & uni(v0)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (23) with elt1, all_100_8, all_100_2, all_100_1, % 42.70/6.57 | | all_100_11, all_100_7, simplifying with (27), (56), (57), (58), % 42.70/6.57 | | (81), (178) gives: % 42.70/6.57 | | (205) ? [v0: uni] : (rev_append(elt1, all_100_1, v0) = all_100_7 & % 42.70/6.57 | | cons(elt1, all_100_2, all_100_8) = v0 & uni(v0) & uni(all_100_7)) % 42.70/6.57 | | % 42.70/6.57 | | GROUND_INST: instantiating (7) with elt1, all_100_2, all_100_2, all_100_1, % 42.70/6.57 | | all_100_11, simplifying with (27), (57), (58), (113), (178) % 42.70/6.57 | | gives: % 43.03/6.57 | | (206) ? [v0: any] : ? [v1: int] : ? [v2: int] : (num_occ(elt1, % 43.03/6.57 | | all_100_2, all_100_1) = v2 & num_occ(elt1, all_100_2, % 43.03/6.57 | | all_100_11) = v1 & sort(elt1, all_100_2) = v0 & ( ~ (v0 = 0) | % 43.03/6.57 | | $difference(v2, v1) = -1)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (5) with elt1, all_100_2, all_100_2, all_100_1, % 43.03/6.57 | | all_100_11, simplifying with (27), (57), (58), (113), (178) % 43.03/6.57 | | gives: % 43.03/6.57 | | (207) ? [v0: any] : ? [v1: any] : ? [v2: MultipleValueBool] : % 43.03/6.57 | | (mem(elt1, all_100_2, all_100_1) = v2 & mem(elt1, all_100_2, % 43.03/6.57 | | all_100_11) = v1 & sort(elt1, all_100_2) = v0 & ( ~ (v0 = 0) | % 43.03/6.57 | | v1 = 0)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (3) with elt1, all_100_10, all_121_0, simplifying % 43.03/6.57 | | with (27), (55), (119) gives: % 43.03/6.57 | | (208) all_121_0 = 0 | ? [v0: any] : ( ~ (v0 = all_100_10) & nil(elt1) = % 43.03/6.57 | | v0 & uni(v0)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (length_nonnegative) with elt1, all_100_8, % 43.03/6.57 | | $difference(all_133_1, all_121_0), simplifying with (27), (56), % 43.03/6.57 | | (176) gives: % 43.03/6.57 | | (209) $lesseq(all_121_0, all_133_1) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (3) with elt1, all_100_7, all_133_1, simplifying % 43.03/6.57 | | with (27), (128), (132) gives: % 43.03/6.57 | | (210) all_133_1 = 0 | ? [v0: any] : ( ~ (v0 = all_100_7) & nil(elt1) = % 43.03/6.57 | | v0 & uni(v0)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (length_nonnegative) with elt1, all_100_1, % 43.03/6.57 | | $sum(all_121_0, -1), simplifying with (27), (58), (192) gives: % 43.03/6.57 | | (211) $lesseq(1, all_121_0) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (13) with elt1, all_100_1, $sum(all_121_0, -1), % 43.03/6.57 | | simplifying with (27), (58), (192) gives: % 43.03/6.57 | | (212) ? [v0: uni] : (reverse(elt1, all_100_1) = v0 & length(elt1, v0) = % 43.03/6.57 | | $sum(all_121_0, -1) & uni(v0)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (10) with elt1, all_100_1, all_100_8, all_100_2, % 43.03/6.57 | | all_100_11, all_100_10, all_100_7, simplifying with (27), (56), % 43.03/6.57 | | (57), (58), (67), (174), (178) gives: % 43.03/6.57 | | (213) ? [v0: uni] : ? [v1: uni] : (reverse(elt1, all_100_1) = v0 & % 43.03/6.57 | | infix_plpl(elt1, v0, v1) = all_100_7 & cons(elt1, all_100_2, % 43.03/6.57 | | all_100_8) = v1 & uni(v1) & uni(v0) & uni(all_100_7)) % 43.03/6.57 | | % 43.03/6.57 | | GROUND_INST: instantiating (15) with elt1, all_100_2, all_149_2, all_89_1, % 43.03/6.57 | | all_145_1, all_100_10, simplifying with (27), (57), (99), % 43.03/6.57 | | (157), (179), (191) gives: % 43.03/6.58 | | (214) ? [v0: uni] : ? [v1: uni] : (permut(elt1, v1, all_100_10) = 0 & % 43.03/6.58 | | infix_plpl(elt1, v0, all_89_1) = v1 & cons(elt1, all_100_2, % 43.03/6.58 | | all_149_2) = v0 & uni(v1) & uni(v0)) % 43.03/6.58 | | % 43.03/6.58 | | GROUND_INST: instantiating (9) with elt1, all_100_1, all_89_1, all_100_2, % 43.03/6.58 | | all_149_2, all_145_1, all_100_10, simplifying with (27), (57), % 43.03/6.58 | | (58), (99), (147), (157), (191) gives: % 43.03/6.58 | | (215) ? [v0: uni] : ? [v1: uni] : (reverse(elt1, v0) = v1 & % 43.03/6.58 | | infix_plpl(elt1, v1, all_89_1) = all_100_10 & cons(elt1, % 43.03/6.58 | | all_100_2, all_100_1) = v0 & uni(v1) & uni(v0) & % 43.03/6.58 | | uni(all_100_10)) % 43.03/6.58 | | % 43.03/6.58 | | GROUND_INST: instantiating (21) with all_100_4, all_89_0, all_100_2, % 43.03/6.58 | | all_89_1, all_145_1, simplifying with (60), (80), (96), (108), % 43.03/6.58 | | (157) gives: % 43.03/6.58 | | (216) ? [v0: list_elt] : ? [v1: any] : ? [v2: any] : (sorted(v0) = v1 % 43.03/6.58 | | & sorted(all_89_0) = v2 & tb2t(all_145_1) = v0 & list_elt(v0) & ( % 43.03/6.58 | | ~ (v1 = 0) | (v2 = 0 & ! [v3: elt] : ! [v4: int] : (v4 = 0 | % 43.03/6.58 | | ~ (le(all_100_4, v3) = v4) | ~ elt(v3) | ? [v5: uni] : ? % 43.03/6.58 | | [v6: int] : ( ~ (v6 = 0) & t2tb1(v3) = v5 & mem(elt1, v5, % 43.03/6.58 | | all_89_1) = v6 & uni(v5))) & ! [v3: elt] : ! [v4: % 43.03/6.58 | | uni] : ( ~ (t2tb1(v3) = v4) | ~ elt(v3) | ? [v5: any] : % 43.03/6.58 | | ? [v6: any] : (le(all_100_4, v3) = v6 & mem(elt1, v4, % 43.03/6.58 | | all_89_1) = v5 & ( ~ (v5 = 0) | v6 = 0)))))) % 43.03/6.58 | | % 43.03/6.58 | | GROUND_INST: instantiating (22) with all_100_9, all_100_15, all_100_10, % 43.03/6.58 | | all_100_8, all_100_7, simplifying with (61), (70), (110), % 43.03/6.58 | | (174), (196) gives: % 43.03/6.58 | | (217) ? [v0: any] : ? [v1: any] : ? [v2: list_elt] : ? [v3: any] : ? % 43.03/6.58 | | [v4: elt] : ? [v5: elt] : ? [v6: uni] : ? [v7: int] : ? [v8: % 43.03/6.58 | | uni] : ? [v9: int] : ? [v10: int] : (elt(v5) & elt(v4) & ((v9 = % 43.03/6.58 | | 0 & v7 = 0 & ~ (v10 = 0) & t2tb1(v5) = v8 & t2tb1(v4) = v6 & % 43.03/6.58 | | le(v4, v5) = v10 & mem(elt1, v8, all_100_8) = 0 & mem(elt1, % 43.03/6.58 | | v6, all_100_10) = 0 & uni(v8) & uni(v6)) | (sorted(v2) = v3 % 43.03/6.58 | | & sorted(all_100_9) = v0 & sorted(all_100_15) = v1 & % 43.03/6.58 | | tb2t(all_100_7) = v2 & list_elt(v2) & ( ~ (v1 = 0) | ~ (v0 = % 43.03/6.58 | | 0) | v3 = 0)))) % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (199) with fresh symbol all_221_0 gives: % 43.03/6.58 | | (218) num_occ(elt1, all_100_2, all_221_0) = 0 & nil(elt1) = all_221_0 & % 43.03/6.58 | | uni(all_221_0) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (218) implies: % 43.03/6.58 | | (219) uni(all_221_0) % 43.03/6.58 | | (220) nil(elt1) = all_221_0 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (212) with fresh symbol all_231_0 gives: % 43.03/6.58 | | (221) reverse(elt1, all_100_1) = all_231_0 & length(elt1, all_231_0) = % 43.03/6.58 | | $sum(all_121_0, -1) & uni(all_231_0) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (221) implies: % 43.03/6.58 | | (222) uni(all_231_0) % 43.03/6.58 | | (223) reverse(elt1, all_100_1) = all_231_0 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (204) with fresh symbol all_243_0 gives: % 43.03/6.58 | | (224) ~ (all_243_0 = all_145_1) & nil(elt1) = all_243_0 & uni(all_243_0) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (224) implies: % 43.03/6.58 | | (225) nil(elt1) = all_243_0 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (205) with fresh symbol all_245_0 gives: % 43.03/6.58 | | (226) rev_append(elt1, all_100_1, all_245_0) = all_100_7 & cons(elt1, % 43.03/6.58 | | all_100_2, all_100_8) = all_245_0 & uni(all_245_0) & % 43.03/6.58 | | uni(all_100_7) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (226) implies: % 43.03/6.58 | | (227) cons(elt1, all_100_2, all_100_8) = all_245_0 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (198) with fresh symbols all_247_0, all_247_1 gives: % 43.03/6.58 | | (228) ~ (all_247_0 = 0) & mem(elt1, all_100_2, all_247_1) = all_247_0 & % 43.03/6.58 | | nil(elt1) = all_247_1 & uni(all_247_1) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (228) implies: % 43.03/6.58 | | (229) nil(elt1) = all_247_1 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (201) with fresh symbols all_263_0, all_263_1, % 43.03/6.58 | | all_263_2 gives: % 43.03/6.58 | | (230) mem(elt1, all_100_2, all_145_1) = all_263_1 & mem(elt1, all_100_2, % 43.03/6.58 | | all_89_1) = all_263_0 & sort(elt1, all_100_2) = all_263_2 & ( ~ % 43.03/6.58 | | (all_263_2 = 0) | all_263_1 = 0) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (230) implies: % 43.03/6.58 | | (231) sort(elt1, all_100_2) = all_263_2 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (200) with fresh symbols all_265_0, all_265_1, % 43.03/6.58 | | all_265_2 gives: % 43.03/6.58 | | (232) num_occ(elt1, all_100_2, all_145_1) = all_265_1 & num_occ(elt1, % 43.03/6.58 | | all_100_2, all_89_1) = all_265_0 & sort(elt1, all_100_2) = % 43.03/6.58 | | all_265_2 & ( ~ (all_265_2 = 0) | $difference(all_265_0, all_265_1) % 43.03/6.58 | | = -1) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (232) implies: % 43.03/6.58 | | (233) sort(elt1, all_100_2) = all_265_2 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (214) with fresh symbols all_269_0, all_269_1 gives: % 43.03/6.58 | | (234) permut(elt1, all_269_0, all_100_10) = 0 & infix_plpl(elt1, % 43.03/6.58 | | all_269_1, all_89_1) = all_269_0 & cons(elt1, all_100_2, % 43.03/6.58 | | all_149_2) = all_269_1 & uni(all_269_0) & uni(all_269_1) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (234) implies: % 43.03/6.58 | | (235) cons(elt1, all_100_2, all_149_2) = all_269_1 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (207) with fresh symbols all_271_0, all_271_1, % 43.03/6.58 | | all_271_2 gives: % 43.03/6.58 | | (236) mem(elt1, all_100_2, all_100_1) = all_271_0 & mem(elt1, all_100_2, % 43.03/6.58 | | all_100_11) = all_271_1 & sort(elt1, all_100_2) = all_271_2 & ( ~ % 43.03/6.58 | | (all_271_2 = 0) | all_271_1 = 0) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (236) implies: % 43.03/6.58 | | (237) sort(elt1, all_100_2) = all_271_2 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (203) with fresh symbols all_273_0, all_273_1 gives: % 43.03/6.58 | | (238) cons_proj_1(elt1, all_145_1) = all_273_0 & sort(elt1, all_100_2) = % 43.03/6.58 | | all_273_1 & uni(all_273_0) & ( ~ (all_273_1 = 0) | all_273_0 = % 43.03/6.58 | | all_100_2) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (238) implies: % 43.03/6.58 | | (239) sort(elt1, all_100_2) = all_273_1 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (206) with fresh symbols all_275_0, all_275_1, % 43.03/6.58 | | all_275_2 gives: % 43.03/6.58 | | (240) num_occ(elt1, all_100_2, all_100_1) = all_275_0 & num_occ(elt1, % 43.03/6.58 | | all_100_2, all_100_11) = all_275_1 & sort(elt1, all_100_2) = % 43.03/6.58 | | all_275_2 & ( ~ (all_275_2 = 0) | $difference(all_275_0, all_275_1) % 43.03/6.58 | | = -1) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (240) implies: % 43.03/6.58 | | (241) sort(elt1, all_100_2) = all_275_2 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (215) with fresh symbols all_277_0, all_277_1 gives: % 43.03/6.58 | | (242) reverse(elt1, all_277_1) = all_277_0 & infix_plpl(elt1, all_277_0, % 43.03/6.58 | | all_89_1) = all_100_10 & cons(elt1, all_100_2, all_100_1) = % 43.03/6.58 | | all_277_1 & uni(all_277_0) & uni(all_277_1) & uni(all_100_10) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (242) implies: % 43.03/6.58 | | (243) uni(all_277_1) % 43.03/6.58 | | (244) cons(elt1, all_100_2, all_100_1) = all_277_1 % 43.03/6.58 | | (245) infix_plpl(elt1, all_277_0, all_89_1) = all_100_10 % 43.03/6.58 | | (246) reverse(elt1, all_277_1) = all_277_0 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (213) with fresh symbols all_279_0, all_279_1 gives: % 43.03/6.58 | | (247) reverse(elt1, all_100_1) = all_279_1 & infix_plpl(elt1, all_279_1, % 43.03/6.58 | | all_279_0) = all_100_7 & cons(elt1, all_100_2, all_100_8) = % 43.03/6.58 | | all_279_0 & uni(all_279_0) & uni(all_279_1) & uni(all_100_7) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (247) implies: % 43.03/6.58 | | (248) cons(elt1, all_100_2, all_100_8) = all_279_0 % 43.03/6.58 | | (249) reverse(elt1, all_100_1) = all_279_1 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (202) with fresh symbols all_281_0, all_281_1, % 43.03/6.58 | | all_281_2, all_281_3 gives: % 43.03/6.58 | | (250) reverse(elt1, all_145_1) = all_281_3 & reverse(elt1, all_89_1) = % 43.03/6.58 | | all_281_2 & infix_plpl(elt1, all_281_2, all_281_0) = all_281_3 & % 43.03/6.58 | | cons(elt1, all_100_2, all_281_1) = all_281_0 & nil(elt1) = % 43.03/6.58 | | all_281_1 & uni(all_281_0) & uni(all_281_1) & uni(all_281_2) & % 43.03/6.58 | | uni(all_281_3) % 43.03/6.58 | | % 43.03/6.58 | | ALPHA: (250) implies: % 43.03/6.58 | | (251) nil(elt1) = all_281_1 % 43.03/6.58 | | % 43.03/6.58 | | DELTA: instantiating (216) with fresh symbols all_290_0, all_290_1, % 43.03/6.58 | | all_290_2 gives: % 43.03/6.59 | | (252) sorted(all_290_2) = all_290_1 & sorted(all_89_0) = all_290_0 & % 43.03/6.59 | | tb2t(all_145_1) = all_290_2 & list_elt(all_290_2) & ( ~ (all_290_1 % 43.03/6.59 | | = 0) | (all_290_0 = 0 & ! [v0: elt] : ! [v1: int] : (v1 = 0 | % 43.03/6.59 | | ~ (le(all_100_4, v0) = v1) | ~ elt(v0) | ? [v2: uni] : ? % 43.03/6.59 | | [v3: int] : ( ~ (v3 = 0) & t2tb1(v0) = v2 & mem(elt1, v2, % 43.03/6.59 | | all_89_1) = v3 & uni(v2))) & ! [v0: elt] : ! [v1: uni] % 43.03/6.59 | | : ( ~ (t2tb1(v0) = v1) | ~ elt(v0) | ? [v2: any] : ? [v3: % 43.03/6.59 | | any] : (le(all_100_4, v0) = v3 & mem(elt1, v1, all_89_1) = % 43.03/6.59 | | v2 & ( ~ (v2 = 0) | v3 = 0))))) % 43.03/6.59 | | % 43.03/6.59 | | ALPHA: (252) implies: % 43.03/6.59 | | (253) tb2t(all_145_1) = all_290_2 % 43.03/6.59 | | (254) sorted(all_290_2) = all_290_1 % 43.03/6.59 | | (255) ~ (all_290_1 = 0) | (all_290_0 = 0 & ! [v0: elt] : ! [v1: int] : % 43.03/6.59 | | (v1 = 0 | ~ (le(all_100_4, v0) = v1) | ~ elt(v0) | ? [v2: uni] % 43.03/6.59 | | : ? [v3: int] : ( ~ (v3 = 0) & t2tb1(v0) = v2 & mem(elt1, v2, % 43.03/6.59 | | all_89_1) = v3 & uni(v2))) & ! [v0: elt] : ! [v1: uni] : % 43.03/6.59 | | ( ~ (t2tb1(v0) = v1) | ~ elt(v0) | ? [v2: any] : ? [v3: any] : % 43.03/6.59 | | (le(all_100_4, v0) = v3 & mem(elt1, v1, all_89_1) = v2 & ( ~ % 43.03/6.59 | | (v2 = 0) | v3 = 0)))) % 43.03/6.59 | | % 43.03/6.59 | | DELTA: instantiating (217) with fresh symbols all_292_0, all_292_1, % 43.03/6.59 | | all_292_2, all_292_3, all_292_4, all_292_5, all_292_6, all_292_7, % 43.03/6.59 | | all_292_8, all_292_9, all_292_10 gives: % 43.03/6.59 | | (256) elt(all_292_5) & elt(all_292_6) & ((all_292_1 = 0 & all_292_3 = 0 & % 43.03/6.59 | | ~ (all_292_0 = 0) & t2tb1(all_292_5) = all_292_2 & % 43.03/6.59 | | t2tb1(all_292_6) = all_292_4 & le(all_292_6, all_292_5) = % 43.03/6.59 | | all_292_0 & mem(elt1, all_292_2, all_100_8) = 0 & mem(elt1, % 43.03/6.59 | | all_292_4, all_100_10) = 0 & uni(all_292_2) & uni(all_292_4)) % 43.03/6.59 | | | (sorted(all_292_8) = all_292_7 & sorted(all_100_9) = all_292_10 % 43.03/6.59 | | & sorted(all_100_15) = all_292_9 & tb2t(all_100_7) = all_292_8 % 43.03/6.59 | | & list_elt(all_292_8) & ( ~ (all_292_9 = 0) | ~ (all_292_10 = % 43.03/6.59 | | 0) | all_292_7 = 0))) % 43.03/6.59 | | % 43.03/6.59 | | ALPHA: (256) implies: % 43.03/6.59 | | (257) elt(all_292_6) % 43.03/6.59 | | (258) elt(all_292_5) % 43.03/6.59 | | (259) (all_292_1 = 0 & all_292_3 = 0 & ~ (all_292_0 = 0) & % 43.03/6.59 | | t2tb1(all_292_5) = all_292_2 & t2tb1(all_292_6) = all_292_4 & % 43.03/6.59 | | le(all_292_6, all_292_5) = all_292_0 & mem(elt1, all_292_2, % 43.03/6.59 | | all_100_8) = 0 & mem(elt1, all_292_4, all_100_10) = 0 & % 43.03/6.59 | | uni(all_292_2) & uni(all_292_4)) | (sorted(all_292_8) = all_292_7 % 43.03/6.59 | | & sorted(all_100_9) = all_292_10 & sorted(all_100_15) = all_292_9 % 43.03/6.59 | | & tb2t(all_100_7) = all_292_8 & list_elt(all_292_8) & ( ~ % 43.03/6.59 | | (all_292_9 = 0) | ~ (all_292_10 = 0) | all_292_7 = 0)) % 43.03/6.59 | | % 43.03/6.59 | | BETA: splitting (259) gives: % 43.03/6.59 | | % 43.03/6.59 | | Case 1: % 43.03/6.59 | | | % 43.03/6.59 | | | (260) all_292_1 = 0 & all_292_3 = 0 & ~ (all_292_0 = 0) & % 43.03/6.59 | | | t2tb1(all_292_5) = all_292_2 & t2tb1(all_292_6) = all_292_4 & % 43.03/6.59 | | | le(all_292_6, all_292_5) = all_292_0 & mem(elt1, all_292_2, % 43.03/6.59 | | | all_100_8) = 0 & mem(elt1, all_292_4, all_100_10) = 0 & % 43.03/6.59 | | | uni(all_292_2) & uni(all_292_4) % 43.03/6.59 | | | % 43.03/6.59 | | | ALPHA: (260) implies: % 43.03/6.59 | | | (261) ~ (all_292_0 = 0) % 43.03/6.59 | | | (262) uni(all_292_4) % 43.03/6.59 | | | (263) mem(elt1, all_292_4, all_100_10) = 0 % 43.03/6.59 | | | (264) mem(elt1, all_292_2, all_100_8) = 0 % 43.03/6.59 | | | (265) le(all_292_6, all_292_5) = all_292_0 % 43.03/6.59 | | | (266) t2tb1(all_292_6) = all_292_4 % 43.03/6.59 | | | (267) t2tb1(all_292_5) = all_292_2 % 43.03/6.59 | | | % 43.03/6.59 | | | BETA: splitting (210) gives: % 43.03/6.59 | | | % 43.03/6.59 | | | Case 1: % 43.03/6.59 | | | | % 43.03/6.59 | | | | (268) all_133_1 = 0 % 43.03/6.59 | | | | % 43.03/6.59 | | | | REDUCE: (209), (268) imply: % 43.03/6.59 | | | | (269) $lesseq(all_121_0, 0) % 43.03/6.59 | | | | % 43.03/6.59 | | | | COMBINE_INEQS: (211), (269) imply: % 43.03/6.59 | | | | (270) $false % 43.03/6.59 | | | | % 43.03/6.59 | | | | CLOSE: (270) is inconsistent. % 43.03/6.59 | | | | % 43.03/6.59 | | | Case 2: % 43.03/6.59 | | | | % 43.03/6.59 | | | | (271) ? [v0: any] : ( ~ (v0 = all_100_7) & nil(elt1) = v0 & uni(v0)) % 43.03/6.59 | | | | % 43.03/6.59 | | | | DELTA: instantiating (271) with fresh symbol all_304_0 gives: % 43.03/6.59 | | | | (272) ~ (all_304_0 = all_100_7) & nil(elt1) = all_304_0 & % 43.03/6.59 | | | | uni(all_304_0) % 43.03/6.59 | | | | % 43.03/6.59 | | | | ALPHA: (272) implies: % 43.03/6.59 | | | | (273) nil(elt1) = all_304_0 % 43.03/6.59 | | | | % 43.03/6.59 | | | | BETA: splitting (208) gives: % 43.03/6.59 | | | | % 43.03/6.59 | | | | Case 1: % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | (274) all_121_0 = 0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | REDUCE: (211), (274) imply: % 43.03/6.59 | | | | | (275) $false % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | CLOSE: (275) is inconsistent. % 43.03/6.59 | | | | | % 43.03/6.59 | | | | Case 2: % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | (276) ? [v0: any] : ( ~ (v0 = all_100_10) & nil(elt1) = v0 & % 43.03/6.59 | | | | | uni(v0)) % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | DELTA: instantiating (276) with fresh symbol all_311_0 gives: % 43.03/6.59 | | | | | (277) ~ (all_311_0 = all_100_10) & nil(elt1) = all_311_0 & % 43.03/6.59 | | | | | uni(all_311_0) % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | ALPHA: (277) implies: % 43.03/6.59 | | | | | (278) nil(elt1) = all_311_0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (34) with 0, all_273_1, all_100_2, elt1, % 43.03/6.59 | | | | | simplifying with (113), (239) gives: % 43.03/6.59 | | | | | (279) all_273_1 = 0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (34) with all_273_1, all_275_2, all_100_2, % 43.03/6.59 | | | | | elt1, simplifying with (239), (241) gives: % 43.03/6.59 | | | | | (280) all_275_2 = all_273_1 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (34) with all_271_2, all_275_2, all_100_2, % 43.03/6.59 | | | | | elt1, simplifying with (237), (241) gives: % 43.03/6.59 | | | | | (281) all_275_2 = all_271_2 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (34) with all_265_2, all_275_2, all_100_2, % 43.03/6.59 | | | | | elt1, simplifying with (233), (241) gives: % 43.03/6.59 | | | | | (282) all_275_2 = all_265_2 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (34) with all_263_2, all_275_2, all_100_2, % 43.03/6.59 | | | | | elt1, simplifying with (231), (241) gives: % 43.03/6.59 | | | | | (283) all_275_2 = all_263_2 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_89_1, all_247_1, elt1, % 43.03/6.59 | | | | | simplifying with (40), (229) gives: % 43.03/6.59 | | | | | (284) all_247_1 = all_89_1 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_221_0, all_247_1, elt1, % 43.03/6.59 | | | | | simplifying with (220), (229) gives: % 43.03/6.59 | | | | | (285) all_247_1 = all_221_0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_281_1, all_304_0, elt1, % 43.03/6.59 | | | | | simplifying with (251), (273) gives: % 43.03/6.59 | | | | | (286) all_304_0 = all_281_1 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_247_1, all_304_0, elt1, % 43.03/6.59 | | | | | simplifying with (229), (273) gives: % 43.03/6.59 | | | | | (287) all_304_0 = all_247_1 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_304_0, all_311_0, elt1, % 43.03/6.59 | | | | | simplifying with (273), (278) gives: % 43.03/6.59 | | | | | (288) all_311_0 = all_304_0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (29) with all_243_0, all_311_0, elt1, % 43.03/6.59 | | | | | simplifying with (225), (278) gives: % 43.03/6.59 | | | | | (289) all_311_0 = all_243_0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (37) with all_245_0, all_279_0, all_100_8, % 43.03/6.59 | | | | | all_100_2, elt1, simplifying with (227), (248) gives: % 43.03/6.59 | | | | | (290) all_279_0 = all_245_0 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (37) with all_100_11, all_277_1, all_100_1, % 43.03/6.59 | | | | | all_100_2, elt1, simplifying with (178), (244) gives: % 43.03/6.59 | | | | | (291) all_277_1 = all_100_11 % 43.03/6.59 | | | | | % 43.03/6.59 | | | | | GROUND_INST: instantiating (36) with all_149_2, all_279_1, all_100_1, % 43.03/6.59 | | | | | elt1, simplifying with (147), (249) gives: % 43.03/6.59 | | | | | (292) all_279_1 = all_149_2 % 43.03/6.59 | | | | | % 43.03/6.60 | | | | | GROUND_INST: instantiating (36) with all_231_0, all_279_1, all_100_1, % 43.03/6.60 | | | | | elt1, simplifying with (223), (249) gives: % 43.03/6.60 | | | | | (293) all_279_1 = all_231_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | GROUND_INST: instantiating (31) with all_145_0, all_290_2, all_145_1, % 43.03/6.60 | | | | | simplifying with (137), (253) gives: % 43.03/6.60 | | | | | (294) all_290_2 = all_145_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (288), (289) imply: % 43.03/6.60 | | | | | (295) all_304_0 = all_243_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (295) implies: % 43.03/6.60 | | | | | (296) all_304_0 = all_243_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (286), (287) imply: % 43.03/6.60 | | | | | (297) all_281_1 = all_247_1 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (286), (296) imply: % 43.03/6.60 | | | | | (298) all_281_1 = all_243_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (297), (298) imply: % 43.03/6.60 | | | | | (299) all_247_1 = all_243_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (299) implies: % 43.03/6.60 | | | | | (300) all_247_1 = all_243_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (292), (293) imply: % 43.03/6.60 | | | | | (301) all_231_0 = all_149_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (301) implies: % 43.03/6.60 | | | | | (302) all_231_0 = all_149_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (280), (281) imply: % 43.03/6.60 | | | | | (303) all_273_1 = all_271_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (303) implies: % 43.03/6.60 | | | | | (304) all_273_1 = all_271_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (281), (283) imply: % 43.03/6.60 | | | | | (305) all_271_2 = all_263_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (281), (282) imply: % 43.03/6.60 | | | | | (306) all_271_2 = all_265_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (279), (304) imply: % 43.03/6.60 | | | | | (307) all_271_2 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (307) implies: % 43.03/6.60 | | | | | (308) all_271_2 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (305), (306) imply: % 43.03/6.60 | | | | | (309) all_265_2 = all_263_2 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (306), (308) imply: % 43.03/6.60 | | | | | (310) all_265_2 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (309), (310) imply: % 43.03/6.60 | | | | | (311) all_263_2 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (311) implies: % 43.03/6.60 | | | | | (312) all_263_2 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (285), (300) imply: % 43.03/6.60 | | | | | (313) all_243_0 = all_221_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (284), (300) imply: % 43.03/6.60 | | | | | (314) all_243_0 = all_89_1 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | COMBINE_EQS: (313), (314) imply: % 43.03/6.60 | | | | | (315) all_221_0 = all_89_1 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | SIMP: (315) implies: % 43.03/6.60 | | | | | (316) all_221_0 = all_89_1 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | REDUCE: (254), (294) imply: % 43.03/6.60 | | | | | (317) sorted(all_145_0) = all_290_1 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | REDUCE: (246), (291) imply: % 43.03/6.60 | | | | | (318) reverse(elt1, all_100_11) = all_277_0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | GROUND_INST: instantiating (36) with all_100_10, all_277_0, % 43.03/6.60 | | | | | all_100_11, elt1, simplifying with (67), (318) gives: % 43.03/6.60 | | | | | (319) all_277_0 = all_100_10 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | GROUND_INST: instantiating (32) with 0, all_290_1, all_145_0, % 43.03/6.60 | | | | | simplifying with (138), (317) gives: % 43.03/6.60 | | | | | (320) all_290_1 = 0 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | REDUCE: (245), (319) imply: % 43.03/6.60 | | | | | (321) infix_plpl(elt1, all_100_10, all_89_1) = all_100_10 % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | BETA: splitting (255) gives: % 43.03/6.60 | | | | | % 43.03/6.60 | | | | | Case 1: % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | (322) ~ (all_290_1 = 0) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | REDUCE: (320), (322) imply: % 43.03/6.60 | | | | | | (323) $false % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | CLOSE: (323) is inconsistent. % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | Case 2: % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (7) with elt1, all_100_2, all_100_2, % 43.03/6.60 | | | | | | all_100_8, all_245_0, simplifying with (27), (56), % 43.03/6.60 | | | | | | (57), (113), (227) gives: % 43.03/6.60 | | | | | | (324) ? [v0: any] : ? [v1: int] : ? [v2: int] : (num_occ(elt1, % 43.03/6.60 | | | | | | all_100_2, all_245_0) = v1 & num_occ(elt1, all_100_2, % 43.03/6.60 | | | | | | all_100_8) = v2 & sort(elt1, all_100_2) = v0 & ( ~ (v0 % 43.03/6.60 | | | | | | = 0) | $difference(v2, v1) = -1)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (5) with elt1, all_100_2, all_100_2, % 43.03/6.60 | | | | | | all_100_8, all_245_0, simplifying with (27), (56), % 43.03/6.60 | | | | | | (57), (113), (227) gives: % 43.03/6.60 | | | | | | (325) ? [v0: any] : ? [v1: any] : ? [v2: MultipleValueBool] : % 43.03/6.60 | | | | | | (mem(elt1, all_100_2, all_245_0) = v1 & mem(elt1, % 43.03/6.60 | | | | | | all_100_2, all_100_8) = v2 & sort(elt1, all_100_2) = v0 % 43.03/6.60 | | | | | | & ( ~ (v0 = 0) | v1 = 0)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (cons_proj_1_def) with elt1, all_100_2, % 43.03/6.60 | | | | | | all_100_8, all_245_0, simplifying with (27), (56), % 43.03/6.60 | | | | | | (57), (227) gives: % 43.03/6.60 | | | | | | (326) ? [v0: any] : ? [v1: uni] : (cons_proj_1(elt1, all_245_0) % 43.03/6.60 | | | | | | = v1 & sort(elt1, all_100_2) = v0 & uni(v1) & ( ~ (v0 = % 43.03/6.60 | | | | | | 0) | v1 = all_100_2)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (7) with elt1, all_100_2, all_100_2, % 43.03/6.60 | | | | | | all_149_2, all_269_1, simplifying with (27), (57), % 43.03/6.60 | | | | | | (113), (179), (235) gives: % 43.03/6.60 | | | | | | (327) ? [v0: any] : ? [v1: int] : ? [v2: int] : (num_occ(elt1, % 43.03/6.60 | | | | | | all_100_2, all_269_1) = v1 & num_occ(elt1, all_100_2, % 43.03/6.60 | | | | | | all_149_2) = v2 & sort(elt1, all_100_2) = v0 & ( ~ (v0 % 43.03/6.60 | | | | | | = 0) | $difference(v2, v1) = -1)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (5) with elt1, all_100_2, all_100_2, % 43.03/6.60 | | | | | | all_149_2, all_269_1, simplifying with (27), (57), % 43.03/6.60 | | | | | | (113), (179), (235) gives: % 43.03/6.60 | | | | | | (328) ? [v0: any] : ? [v1: any] : ? [v2: MultipleValueBool] : % 43.03/6.60 | | | | | | (mem(elt1, all_100_2, all_269_1) = v1 & mem(elt1, % 43.03/6.60 | | | | | | all_100_2, all_149_2) = v2 & sort(elt1, all_100_2) = v0 % 43.03/6.60 | | | | | | & ( ~ (v0 = 0) | v1 = 0)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (cons_proj_1_def) with elt1, all_100_2, % 43.03/6.60 | | | | | | all_149_2, all_269_1, simplifying with (27), (57), % 43.03/6.60 | | | | | | (179), (235) gives: % 43.03/6.60 | | | | | | (329) ? [v0: any] : ? [v1: uni] : (cons_proj_1(elt1, all_269_1) % 43.03/6.60 | | | | | | = v1 & sort(elt1, all_100_2) = v0 & uni(v1) & ( ~ (v0 = % 43.03/6.60 | | | | | | 0) | v1 = all_100_2)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (25) with elt1, all_100_11, all_89_1, % 43.03/6.60 | | | | | | all_100_10, all_100_10, simplifying with (27), (54), % 43.03/6.60 | | | | | | (67), (99), (321) gives: % 43.03/6.60 | | | | | | (330) rev_append(elt1, all_100_11, all_89_1) = all_100_10 & % 43.03/6.60 | | | | | | uni(all_100_10) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (12) with elt1, all_100_10, all_292_4, % 43.03/6.60 | | | | | | simplifying with (27), (55), (262), (263) gives: % 43.03/6.60 | | | | | | (331) ? [v0: uni] : (reverse(elt1, all_100_10) = v0 & mem(elt1, % 43.03/6.60 | | | | | | all_292_4, v0) = 0 & uni(v0)) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (83) with all_292_5, all_292_6, % 43.03/6.60 | | | | | | all_292_0, simplifying with (257), (258), (265) gives: % 43.03/6.60 | | | | | | (332) all_292_0 = 0 | ? [v0: uni] : ? [v1: any] : ? [v2: uni] % 43.03/6.60 | | | | | | : ? [v3: any] : (t2tb1(all_292_5) = v0 & t2tb1(all_292_6) % 43.03/6.60 | | | | | | = v2 & mem(elt1, v2, all_100_11) = v3 & mem(elt1, v0, % 43.03/6.60 | | | | | | all_100_8) = v1 & uni(v2) & uni(v0) & ( ~ (v3 = 0) | ~ % 43.03/6.60 | | | | | | (v1 = 0))) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | GROUND_INST: instantiating (82) with all_292_5, all_292_6, % 43.03/6.60 | | | | | | all_292_0, simplifying with (257), (258), (265) gives: % 43.03/6.60 | | | | | | (333) all_292_0 = 0 | ? [v0: uni] : ? [v1: any] : ? [v2: uni] % 43.03/6.60 | | | | | | : ? [v3: any] : (t2tb1(all_292_5) = v0 & t2tb1(all_292_6) % 43.03/6.60 | | | | | | = v2 & mem(elt1, v2, all_100_14) = v3 & mem(elt1, v0, % 43.03/6.60 | | | | | | all_100_8) = v1 & uni(v2) & uni(v0) & ( ~ (v3 = 0) | ~ % 43.03/6.60 | | | | | | (v1 = 0))) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | DELTA: instantiating (331) with fresh symbol all_450_0 gives: % 43.03/6.60 | | | | | | (334) reverse(elt1, all_100_10) = all_450_0 & mem(elt1, % 43.03/6.60 | | | | | | all_292_4, all_450_0) = 0 & uni(all_450_0) % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | ALPHA: (334) implies: % 43.03/6.60 | | | | | | (335) mem(elt1, all_292_4, all_450_0) = 0 % 43.03/6.60 | | | | | | (336) reverse(elt1, all_100_10) = all_450_0 % 43.03/6.60 | | | | | | % 43.03/6.60 | | | | | | DELTA: instantiating (329) with fresh symbols all_542_0, all_542_1 % 43.03/6.60 | | | | | | gives: % 43.03/6.60 | | | | | | (337) cons_proj_1(elt1, all_269_1) = all_542_0 & sort(elt1, % 43.03/6.60 | | | | | | all_100_2) = all_542_1 & uni(all_542_0) & ( ~ (all_542_1 % 43.03/6.61 | | | | | | = 0) | all_542_0 = all_100_2) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (337) implies: % 43.03/6.61 | | | | | | (338) sort(elt1, all_100_2) = all_542_1 % 43.03/6.61 | | | | | | (339) ~ (all_542_1 = 0) | all_542_0 = all_100_2 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | DELTA: instantiating (326) with fresh symbols all_546_0, all_546_1 % 43.03/6.61 | | | | | | gives: % 43.03/6.61 | | | | | | (340) cons_proj_1(elt1, all_245_0) = all_546_0 & sort(elt1, % 43.03/6.61 | | | | | | all_100_2) = all_546_1 & uni(all_546_0) & ( ~ (all_546_1 % 43.03/6.61 | | | | | | = 0) | all_546_0 = all_100_2) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (340) implies: % 43.03/6.61 | | | | | | (341) sort(elt1, all_100_2) = all_546_1 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | DELTA: instantiating (325) with fresh symbols all_548_0, all_548_1, % 43.03/6.61 | | | | | | all_548_2 gives: % 43.03/6.61 | | | | | | (342) mem(elt1, all_100_2, all_245_0) = all_548_1 & mem(elt1, % 43.03/6.61 | | | | | | all_100_2, all_100_8) = all_548_0 & sort(elt1, all_100_2) % 43.03/6.61 | | | | | | = all_548_2 & ( ~ (all_548_2 = 0) | all_548_1 = 0) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (342) implies: % 43.03/6.61 | | | | | | (343) sort(elt1, all_100_2) = all_548_2 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | DELTA: instantiating (328) with fresh symbols all_554_0, all_554_1, % 43.03/6.61 | | | | | | all_554_2 gives: % 43.03/6.61 | | | | | | (344) mem(elt1, all_100_2, all_269_1) = all_554_1 & mem(elt1, % 43.03/6.61 | | | | | | all_100_2, all_149_2) = all_554_0 & sort(elt1, all_100_2) % 43.03/6.61 | | | | | | = all_554_2 & ( ~ (all_554_2 = 0) | all_554_1 = 0) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (344) implies: % 43.03/6.61 | | | | | | (345) sort(elt1, all_100_2) = all_554_2 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | DELTA: instantiating (327) with fresh symbols all_556_0, all_556_1, % 43.03/6.61 | | | | | | all_556_2 gives: % 43.03/6.61 | | | | | | (346) num_occ(elt1, all_100_2, all_269_1) = all_556_1 & % 43.03/6.61 | | | | | | num_occ(elt1, all_100_2, all_149_2) = all_556_0 & % 43.03/6.61 | | | | | | sort(elt1, all_100_2) = all_556_2 & ( ~ (all_556_2 = 0) | % 43.03/6.61 | | | | | | $difference(all_556_0, all_556_1) = -1) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (346) implies: % 43.03/6.61 | | | | | | (347) sort(elt1, all_100_2) = all_556_2 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | DELTA: instantiating (324) with fresh symbols all_562_0, all_562_1, % 43.03/6.61 | | | | | | all_562_2 gives: % 43.03/6.61 | | | | | | (348) num_occ(elt1, all_100_2, all_245_0) = all_562_1 & % 43.03/6.61 | | | | | | num_occ(elt1, all_100_2, all_100_8) = all_562_0 & % 43.03/6.61 | | | | | | sort(elt1, all_100_2) = all_562_2 & ( ~ (all_562_2 = 0) | % 43.03/6.61 | | | | | | $difference(all_562_0, all_562_1) = -1) % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | ALPHA: (348) implies: % 43.03/6.61 | | | | | | (349) sort(elt1, all_100_2) = all_562_2 % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | BETA: splitting (333) gives: % 43.03/6.61 | | | | | | % 43.03/6.61 | | | | | | Case 1: % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | (350) all_292_0 = 0 % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | REDUCE: (261), (350) imply: % 43.03/6.61 | | | | | | | (351) $false % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | CLOSE: (351) is inconsistent. % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | Case 2: % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | (352) ? [v0: uni] : ? [v1: any] : ? [v2: uni] : ? [v3: any] % 43.03/6.61 | | | | | | | : (t2tb1(all_292_5) = v0 & t2tb1(all_292_6) = v2 & % 43.03/6.61 | | | | | | | mem(elt1, v2, all_100_14) = v3 & mem(elt1, v0, % 43.03/6.61 | | | | | | | all_100_8) = v1 & uni(v2) & uni(v0) & ( ~ (v3 = 0) | % 43.03/6.61 | | | | | | | ~ (v1 = 0))) % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | DELTA: instantiating (352) with fresh symbols all_672_0, % 43.03/6.61 | | | | | | | all_672_1, all_672_2, all_672_3 gives: % 43.03/6.61 | | | | | | | (353) t2tb1(all_292_5) = all_672_3 & t2tb1(all_292_6) = % 43.03/6.61 | | | | | | | all_672_1 & mem(elt1, all_672_1, all_100_14) = all_672_0 % 43.03/6.61 | | | | | | | & mem(elt1, all_672_3, all_100_8) = all_672_2 & % 43.03/6.61 | | | | | | | uni(all_672_1) & uni(all_672_3) & ( ~ (all_672_0 = 0) | % 43.03/6.61 | | | | | | | ~ (all_672_2 = 0)) % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | ALPHA: (353) implies: % 43.03/6.61 | | | | | | | (354) t2tb1(all_292_6) = all_672_1 % 43.03/6.61 | | | | | | | (355) t2tb1(all_292_5) = all_672_3 % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | BETA: splitting (332) gives: % 43.03/6.61 | | | | | | | % 43.03/6.61 | | | | | | | Case 1: % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | (356) all_292_0 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | REDUCE: (261), (356) imply: % 43.03/6.61 | | | | | | | | (357) $false % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | CLOSE: (357) is inconsistent. % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | Case 2: % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | (358) ? [v0: uni] : ? [v1: any] : ? [v2: uni] : ? [v3: % 43.03/6.61 | | | | | | | | any] : (t2tb1(all_292_5) = v0 & t2tb1(all_292_6) = v2 % 43.03/6.61 | | | | | | | | & mem(elt1, v2, all_100_11) = v3 & mem(elt1, v0, % 43.03/6.61 | | | | | | | | all_100_8) = v1 & uni(v2) & uni(v0) & ( ~ (v3 = 0) % 43.03/6.61 | | | | | | | | | ~ (v1 = 0))) % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | DELTA: instantiating (358) with fresh symbols all_712_0, % 43.03/6.61 | | | | | | | | all_712_1, all_712_2, all_712_3 gives: % 43.03/6.61 | | | | | | | | (359) t2tb1(all_292_5) = all_712_3 & t2tb1(all_292_6) = % 43.03/6.61 | | | | | | | | all_712_1 & mem(elt1, all_712_1, all_100_11) = % 43.03/6.61 | | | | | | | | all_712_0 & mem(elt1, all_712_3, all_100_8) = all_712_2 % 43.03/6.61 | | | | | | | | & uni(all_712_1) & uni(all_712_3) & ( ~ (all_712_0 = 0) % 43.03/6.61 | | | | | | | | | ~ (all_712_2 = 0)) % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | ALPHA: (359) implies: % 43.03/6.61 | | | | | | | | (360) mem(elt1, all_712_3, all_100_8) = all_712_2 % 43.03/6.61 | | | | | | | | (361) mem(elt1, all_712_1, all_100_11) = all_712_0 % 43.03/6.61 | | | | | | | | (362) t2tb1(all_292_6) = all_712_1 % 43.03/6.61 | | | | | | | | (363) t2tb1(all_292_5) = all_712_3 % 43.03/6.61 | | | | | | | | (364) ~ (all_712_0 = 0) | ~ (all_712_2 = 0) % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with all_542_1, all_548_2, % 43.03/6.61 | | | | | | | | all_100_2, elt1, simplifying with (338), (343) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (365) all_548_2 = all_542_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with all_554_2, all_556_2, % 43.03/6.61 | | | | | | | | all_100_2, elt1, simplifying with (345), (347) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (366) all_556_2 = all_554_2 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with all_548_2, all_556_2, % 43.03/6.61 | | | | | | | | all_100_2, elt1, simplifying with (343), (347) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (367) all_556_2 = all_548_2 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with all_546_1, all_556_2, % 43.03/6.61 | | | | | | | | all_100_2, elt1, simplifying with (341), (347) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (368) all_556_2 = all_546_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with 0, all_562_2, all_100_2, % 43.03/6.61 | | | | | | | | elt1, simplifying with (113), (349) gives: % 43.03/6.61 | | | | | | | | (369) all_562_2 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (34) with all_554_2, all_562_2, % 43.03/6.61 | | | | | | | | all_100_2, elt1, simplifying with (345), (349) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (370) all_562_2 = all_554_2 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (36) with all_100_11, all_450_0, % 43.03/6.61 | | | | | | | | all_100_10, elt1, simplifying with (105), (336) % 43.03/6.61 | | | | | | | | gives: % 43.03/6.61 | | | | | | | | (371) all_450_0 = all_100_11 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (33) with all_292_4, all_712_1, % 43.03/6.61 | | | | | | | | all_292_6, simplifying with (266), (362) gives: % 43.03/6.61 | | | | | | | | (372) all_712_1 = all_292_4 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (33) with all_672_1, all_712_1, % 43.03/6.61 | | | | | | | | all_292_6, simplifying with (354), (362) gives: % 43.03/6.61 | | | | | | | | (373) all_712_1 = all_672_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (33) with all_292_2, all_712_3, % 43.03/6.61 | | | | | | | | all_292_5, simplifying with (267), (363) gives: % 43.03/6.61 | | | | | | | | (374) all_712_3 = all_292_2 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | GROUND_INST: instantiating (33) with all_672_3, all_712_3, % 43.03/6.61 | | | | | | | | all_292_5, simplifying with (355), (363) gives: % 43.03/6.61 | | | | | | | | (375) all_712_3 = all_672_3 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (372), (373) imply: % 43.03/6.61 | | | | | | | | (376) all_672_1 = all_292_4 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (374), (375) imply: % 43.03/6.61 | | | | | | | | (377) all_672_3 = all_292_2 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (369), (370) imply: % 43.03/6.61 | | | | | | | | (378) all_554_2 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | SIMP: (378) implies: % 43.03/6.61 | | | | | | | | (379) all_554_2 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (366), (368) imply: % 43.03/6.61 | | | | | | | | (380) all_554_2 = all_546_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | SIMP: (380) implies: % 43.03/6.61 | | | | | | | | (381) all_554_2 = all_546_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (367), (368) imply: % 43.03/6.61 | | | | | | | | (382) all_548_2 = all_546_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | SIMP: (382) implies: % 43.03/6.61 | | | | | | | | (383) all_548_2 = all_546_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (379), (381) imply: % 43.03/6.61 | | | | | | | | (384) all_546_1 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | SIMP: (384) implies: % 43.03/6.61 | | | | | | | | (385) all_546_1 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (365), (383) imply: % 43.03/6.61 | | | | | | | | (386) all_546_1 = all_542_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | SIMP: (386) implies: % 43.03/6.61 | | | | | | | | (387) all_546_1 = all_542_1 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | COMBINE_EQS: (385), (387) imply: % 43.03/6.61 | | | | | | | | (388) all_542_1 = 0 % 43.03/6.61 | | | | | | | | % 43.03/6.61 | | | | | | | | REDUCE: (361), (372) imply: % 43.03/6.61 | | | | | | | | (389) mem(elt1, all_292_4, all_100_11) = all_712_0 % 43.03/6.61 | | | | | | | | % 43.03/6.62 | | | | | | | | REDUCE: (360), (374) imply: % 43.03/6.62 | | | | | | | | (390) mem(elt1, all_292_2, all_100_8) = all_712_2 % 43.03/6.62 | | | | | | | | % 43.03/6.62 | | | | | | | | REDUCE: (335), (371) imply: % 43.03/6.62 | | | | | | | | (391) mem(elt1, all_292_4, all_100_11) = 0 % 43.03/6.62 | | | | | | | | % 43.03/6.62 | | | | | | | | BETA: splitting (339) gives: % 43.03/6.62 | | | | | | | | % 43.03/6.62 | | | | | | | | Case 1: % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | (392) ~ (all_542_1 = 0) % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | REDUCE: (388), (392) imply: % 43.03/6.62 | | | | | | | | | (393) $false % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | CLOSE: (393) is inconsistent. % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | Case 2: % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | GROUND_INST: instantiating (38) with 0, all_712_0, all_100_11, % 43.03/6.62 | | | | | | | | | all_292_4, elt1, simplifying with (389), (391) % 43.03/6.62 | | | | | | | | | gives: % 43.03/6.62 | | | | | | | | | (394) all_712_0 = 0 % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | GROUND_INST: instantiating (38) with 0, all_712_2, all_100_8, % 43.03/6.62 | | | | | | | | | all_292_2, elt1, simplifying with (264), (390) % 43.03/6.62 | | | | | | | | | gives: % 43.03/6.62 | | | | | | | | | (395) all_712_2 = 0 % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | BETA: splitting (364) gives: % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | | Case 1: % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | (396) ~ (all_712_0 = 0) % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | REDUCE: (394), (396) imply: % 43.03/6.62 | | | | | | | | | | (397) $false % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | CLOSE: (397) is inconsistent. % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | Case 2: % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | (398) ~ (all_712_2 = 0) % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | REDUCE: (395), (398) imply: % 43.03/6.62 | | | | | | | | | | (399) $false % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | | CLOSE: (399) is inconsistent. % 43.03/6.62 | | | | | | | | | | % 43.03/6.62 | | | | | | | | | End of split % 43.03/6.62 | | | | | | | | | % 43.03/6.62 | | | | | | | | End of split % 43.03/6.62 | | | | | | | | % 43.03/6.62 | | | | | | | End of split % 43.03/6.62 | | | | | | | % 43.03/6.62 | | | | | | End of split % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | End of split % 43.03/6.62 | | | | | % 43.03/6.62 | | | | End of split % 43.03/6.62 | | | | % 43.03/6.62 | | | End of split % 43.03/6.62 | | | % 43.03/6.62 | | Case 2: % 43.03/6.62 | | | % 43.03/6.62 | | | (400) sorted(all_292_8) = all_292_7 & sorted(all_100_9) = all_292_10 & % 43.03/6.62 | | | sorted(all_100_15) = all_292_9 & tb2t(all_100_7) = all_292_8 & % 43.03/6.62 | | | list_elt(all_292_8) & ( ~ (all_292_9 = 0) | ~ (all_292_10 = 0) | % 43.03/6.62 | | | all_292_7 = 0) % 43.03/6.62 | | | % 43.03/6.62 | | | ALPHA: (400) implies: % 43.03/6.62 | | | (401) tb2t(all_100_7) = all_292_8 % 43.03/6.62 | | | (402) sorted(all_100_15) = all_292_9 % 43.03/6.62 | | | (403) sorted(all_100_9) = all_292_10 % 43.03/6.62 | | | (404) sorted(all_292_8) = all_292_7 % 43.03/6.62 | | | (405) ~ (all_292_9 = 0) | ~ (all_292_10 = 0) | all_292_7 = 0 % 43.03/6.62 | | | % 43.03/6.62 | | | BETA: splitting (208) gives: % 43.03/6.62 | | | % 43.03/6.62 | | | Case 1: % 43.03/6.62 | | | | % 43.03/6.62 | | | | (406) all_121_0 = 0 % 43.03/6.62 | | | | % 43.03/6.62 | | | | REDUCE: (211), (406) imply: % 43.03/6.62 | | | | (407) $false % 43.03/6.62 | | | | % 43.03/6.62 | | | | CLOSE: (407) is inconsistent. % 43.03/6.62 | | | | % 43.03/6.62 | | | Case 2: % 43.03/6.62 | | | | % 43.03/6.62 | | | | % 43.03/6.62 | | | | GROUND_INST: instantiating (31) with all_100_6, all_292_8, all_100_7, % 43.03/6.62 | | | | simplifying with (75), (401) gives: % 43.03/6.62 | | | | (408) all_292_8 = all_100_6 % 43.03/6.62 | | | | % 43.03/6.62 | | | | GROUND_INST: instantiating (32) with 0, all_292_9, all_100_15, % 43.03/6.62 | | | | simplifying with (77), (402) gives: % 43.03/6.62 | | | | (409) all_292_9 = 0 % 43.03/6.62 | | | | % 43.03/6.62 | | | | GROUND_INST: instantiating (32) with 0, all_292_10, all_100_9, % 43.03/6.62 | | | | simplifying with (78), (403) gives: % 43.03/6.62 | | | | (410) all_292_10 = 0 % 43.03/6.62 | | | | % 43.03/6.62 | | | | REDUCE: (404), (408) imply: % 43.03/6.62 | | | | (411) sorted(all_100_6) = all_292_7 % 43.03/6.62 | | | | % 43.03/6.62 | | | | BETA: splitting (405) gives: % 43.03/6.62 | | | | % 43.03/6.62 | | | | Case 1: % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | (412) ~ (all_292_9 = 0) % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | REDUCE: (409), (412) imply: % 43.03/6.62 | | | | | (413) $false % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | CLOSE: (413) is inconsistent. % 43.03/6.62 | | | | | % 43.03/6.62 | | | | Case 2: % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | (414) ~ (all_292_10 = 0) | all_292_7 = 0 % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | BETA: splitting (414) gives: % 43.03/6.62 | | | | | % 43.03/6.62 | | | | | Case 1: % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | (415) ~ (all_292_10 = 0) % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | REDUCE: (410), (415) imply: % 43.03/6.62 | | | | | | (416) $false % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | CLOSE: (416) is inconsistent. % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | Case 2: % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | (417) all_292_7 = 0 % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | REDUCE: (411), (417) imply: % 43.03/6.62 | | | | | | (418) sorted(all_100_6) = 0 % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | GROUND_INST: instantiating (32) with all_100_5, 0, all_100_6, % 43.03/6.62 | | | | | | simplifying with (79), (418) gives: % 43.03/6.62 | | | | | | (419) all_100_5 = 0 % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | REDUCE: (52), (419) imply: % 43.03/6.62 | | | | | | (420) $false % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | | CLOSE: (420) is inconsistent. % 43.03/6.62 | | | | | | % 43.03/6.62 | | | | | End of split % 43.03/6.62 | | | | | % 43.03/6.62 | | | | End of split % 43.03/6.62 | | | | % 43.03/6.62 | | | End of split % 43.03/6.62 | | | % 43.03/6.62 | | End of split % 43.03/6.62 | | % 43.03/6.62 | End of split % 43.03/6.62 | % 43.03/6.62 End of proof % 43.03/6.62 % SZS output end Proof for theBenchmark % 43.03/6.62 % 43.03/6.62 6021ms %------------------------------------------------------------------------------