%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW615_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 : n003.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:54 EDT 2023 % Result : Theorem 15.39s 2.90s % Output : Proof 26.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW615_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 : n003.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 17:53:25 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.06/1.32 Prover 3: Preprocessing ... % 4.06/1.32 Prover 4: Preprocessing ... % 4.06/1.32 Prover 6: Preprocessing ... % 4.06/1.32 Prover 5: Preprocessing ... % 4.06/1.32 Prover 1: Preprocessing ... % 4.06/1.32 Prover 2: Preprocessing ... % 4.06/1.32 Prover 0: Preprocessing ... % 10.32/2.21 Prover 1: Warning: ignoring some quantifiers % 10.83/2.23 Prover 4: Warning: ignoring some quantifiers % 10.83/2.27 Prover 5: Proving ... % 11.20/2.30 Prover 3: Warning: ignoring some quantifiers % 11.20/2.31 Prover 6: Proving ... % 11.20/2.33 Prover 1: Constructing countermodel ... % 11.75/2.37 Prover 4: Constructing countermodel ... % 11.93/2.38 Prover 3: Constructing countermodel ... % 11.93/2.39 Prover 0: Proving ... % 12.47/2.48 Prover 2: Proving ... % 15.39/2.89 Prover 3: proved (2262ms) % 15.39/2.90 % 15.39/2.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.39/2.90 % 15.39/2.90 Prover 2: stopped % 15.39/2.91 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.39/2.91 Prover 0: stopped % 15.39/2.92 Prover 5: stopped % 16.03/2.93 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.03/2.93 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.03/2.93 Prover 6: stopped % 16.03/2.93 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.03/2.93 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 17.15/3.08 Prover 10: Preprocessing ... % 17.15/3.09 Prover 8: Preprocessing ... % 17.47/3.12 Prover 7: Preprocessing ... % 17.47/3.14 Prover 13: Preprocessing ... % 17.66/3.14 Prover 11: Preprocessing ... % 18.31/3.34 Prover 10: Warning: ignoring some quantifiers % 18.31/3.36 Prover 10: Constructing countermodel ... % 18.31/3.37 Prover 7: Warning: ignoring some quantifiers % 18.31/3.38 Prover 13: Warning: ignoring some quantifiers % 19.28/3.41 Prover 13: Constructing countermodel ... % 19.28/3.42 Prover 8: Warning: ignoring some quantifiers % 19.28/3.42 Prover 7: Constructing countermodel ... % 19.28/3.43 Prover 8: Constructing countermodel ... % 19.28/3.44 Prover 11: Warning: ignoring some quantifiers % 19.28/3.47 Prover 11: Constructing countermodel ... % 25.99/4.29 Prover 8: Found proof (size 110) % 25.99/4.29 Prover 8: proved (1370ms) % 25.99/4.29 Prover 7: stopped % 25.99/4.29 Prover 4: stopped % 25.99/4.29 Prover 11: stopped % 25.99/4.29 Prover 1: stopped % 25.99/4.29 Prover 13: stopped % 25.99/4.29 Prover 10: stopped % 25.99/4.29 % 25.99/4.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.99/4.29 % 25.99/4.31 % SZS output start Proof for theBenchmark % 25.99/4.31 Assumptions after simplification: % 25.99/4.31 --------------------------------- % 25.99/4.31 % 25.99/4.31 (bridgeL) % 25.99/4.33 ! [v0: list_loc] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ list_loc(v0) | % 25.99/4.33 tb2t(v1) = v0) % 25.99/4.33 % 25.99/4.33 (bridgeR) % 25.99/4.33 ! [v0: uni] : ! [v1: list_loc] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | t2tb(v1) % 25.99/4.33 = v0) % 25.99/4.33 % 25.99/4.33 (list_seg_inversion) % 25.99/4.33 loc(null) & ty(loc1) & ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & % 25.99/4.33 nil(loc1) = v0 & list_loc(v1) & uni(v0) & ! [v2: loc] : ! [v3: % 25.99/4.33 map_loc_loc] : ! [v4: list_loc] : ! [v5: loc] : ( ~ (list_seg(v2, v3, % 25.99/4.33 v4, v5) = 0) | ~ map_loc_loc(v3) | ~ list_loc(v4) | ~ loc(v5) | ~ % 25.99/4.33 loc(v2) | ? [v6: list_loc] : ? [v7: uni] : ? [v8: uni] : ? [v9: uni] : % 25.99/4.33 ? [v10: loc] : ? [v11: uni] : ? [v12: uni] : ( ~ (v2 = null) & % 25.99/4.33 tb2t2(v9) = v10 & t2tb2(v2) = v8 & t2tb1(v3) = v7 & list_seg(v10, v3, % 25.99/4.33 v6, v5) = 0 & tb2t(v12) = v4 & t2tb(v6) = v11 & get(loc1, loc1, v7, % 25.99/4.33 v8) = v9 & cons(loc1, v8, v11) = v12 & list_loc(v6) & loc(v10) & % 25.99/4.33 uni(v12) & uni(v11) & uni(v9) & uni(v8) & uni(v7)) | (v5 = v2 & v4 = % 25.99/4.33 v1))) % 25.99/4.33 % 25.99/4.33 (list_seg_nil) % 26.62/4.34 ty(loc1) & ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & nil(loc1) = v0 % 26.62/4.34 & list_loc(v1) & uni(v0) & ! [v2: loc] : ! [v3: map_loc_loc] : ! [v4: % 26.62/4.34 int] : (v4 = 0 | ~ (list_seg(v2, v3, v1, v2) = v4) | ~ map_loc_loc(v3) | % 26.62/4.34 ~ loc(v2))) % 26.62/4.34 % 26.62/4.34 (list_seg_no_repet) % 26.62/4.34 loc(null) & ty(loc1) & ! [v0: map_loc_loc] : ! [v1: list_loc] : ! [v2: loc] % 26.62/4.34 : ( ~ (list_seg(v2, v0, v1, null) = 0) | ~ map_loc_loc(v0) | ~ list_loc(v1) % 26.62/4.34 | ~ loc(v2) | ? [v3: uni] : (t2tb(v1) = v3 & no_repet(loc1, v3) = 0 & % 26.62/4.34 uni(v3))) % 26.62/4.34 % 26.62/4.34 (nil_Cons) % 26.62/4.34 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 26.62/4.34 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : ( ~ (v4 % 26.62/4.34 = v3) & nil(v0) = v4 & uni(v4))) % 26.62/4.34 % 26.62/4.34 (select_neq) % 26.62/4.34 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 26.62/4.34 [v5: uni] : ( ~ (get(v1, v0, v2, v4) = v5) | ~ (sort(v0, v3) = 0) | ~ ty(v1) % 26.62/4.34 | ~ ty(v0) | ~ uni(v4) | ~ uni(v3) | ~ uni(v2) | ? [v6: int] : ( ~ (v6 % 26.62/4.34 = 0) & sort(v0, v4) = v6) | ! [v6: uni] : ! [v7: uni] : ! [v8: uni] : % 26.62/4.34 (v8 = v5 | v4 = v3 | ~ (set(v1, v0, v2, v3, v6) = v7) | ~ (get(v1, v0, v7, % 26.62/4.34 v4) = v8) | ~ uni(v6))) % 26.62/4.34 % 26.62/4.34 (t2tb_sort) % 26.62/4.34 ty(loc1) & ? [v0: ty] : (list(loc1) = v0 & ty(v0) & ! [v1: list_loc] : ! % 26.62/4.34 [v2: uni] : ( ~ (t2tb(v1) = v2) | ~ list_loc(v1) | sort(v0, v2) = 0)) % 26.62/4.34 % 26.62/4.34 (t2tb_sort2) % 26.62/4.34 ty(loc1) & ! [v0: loc] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ loc(v0) | % 26.62/4.34 sort(loc1, v1) = 0) % 26.62/4.34 % 26.62/4.34 (tail_cons) % 26.62/4.34 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : (v4 % 26.62/4.34 = v2 | ~ (tail(v0, v3) = v4) | ~ (cons(v0, v1, v2) = v3) | ~ ty(v0) | ~ % 26.62/4.34 uni(v2) | ~ uni(v1)) % 26.62/4.34 % 26.62/4.34 (wP_parameter_in_place_reverse) % 26.62/4.35 loc(null) & ty(loc1) & ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & % 26.62/4.35 nil(loc1) = v0 & list_loc(v1) & uni(v0) & ? [v2: loc] : ? [v3: list_loc] : % 26.62/4.35 ? [v4: map_loc_loc] : ? [v5: uni] : ? [v6: uni] : ? [v7: list_loc] : % 26.62/4.35 (list_seg(v2, v4, v3, null) = 0 & tb2t(v6) = v7 & t2tb(v3) = v5 & % 26.62/4.35 reverse(loc1, v5) = v6 & map_loc_loc(v4) & list_loc(v7) & list_loc(v3) & % 26.62/4.35 loc(v2) & uni(v6) & uni(v5) & ? [v8: list_loc] : ? [v9: loc] : ? [v10: % 26.62/4.35 list_loc] : ? [v11: loc] : ? [v12: map_loc_loc] : ? [v13: uni] : ? % 26.62/4.35 [v14: uni] : ? [v15: uni] : ? [v16: uni] : ? [v17: uni] : ? [v18: uni] % 26.62/4.35 : ? [v19: uni] : ? [v20: uni] : ? [v21: map_loc_loc] : ? [v22: uni] : % 26.62/4.35 ? [v23: loc] : ? [v24: uni] : ? [v25: uni] : ? [v26: list_loc] : ? % 26.62/4.35 [v27: uni] : ? [v28: list_loc] : ( ~ (v11 = null) & tb2t2(v22) = v23 & % 26.62/4.35 t2tb2(v11) = v18 & t2tb2(v9) = v19 & tb2t1(v20) = v21 & t2tb1(v12) = v17 % 26.62/4.35 & list_seg(v11, v12, v10, null) = 0 & list_seg(v9, v21, v8, null) = 0 & % 26.62/4.35 list_seg(v9, v12, v8, null) = 0 & tb2t(v27) = v28 & tb2t(v25) = v26 & % 26.62/4.35 tb2t(v16) = v7 & t2tb(v10) = v13 & t2tb(v8) = v14 & set(loc1, loc1, v17, % 26.62/4.35 v18, v19) = v20 & get(loc1, loc1, v17, v18) = v22 & reverse(loc1, v13) % 26.62/4.35 = v15 & infix_plpl(loc1, v15, v14) = v16 & disjoint(loc1, v13, v14) = 0 % 26.62/4.35 & tail(loc1, v13) = v27 & head(loc1, v13) = v24 & cons(loc1, v24, v14) = % 26.62/4.35 v25 & map_loc_loc(v21) & map_loc_loc(v12) & list_loc(v28) & % 26.62/4.35 list_loc(v26) & list_loc(v10) & list_loc(v8) & loc(v23) & loc(v11) & % 26.62/4.35 loc(v9) & uni(v27) & uni(v25) & uni(v24) & uni(v22) & uni(v20) & % 26.62/4.35 uni(v19) & uni(v18) & uni(v17) & uni(v16) & uni(v15) & uni(v14) & % 26.62/4.35 uni(v13) & (v10 = v1 | ? [v29: loc] : ? [v30: list_loc] : ? [v31: % 26.62/4.35 uni] : ? [v32: uni] : ? [v33: uni] : ( ~ (v30 = v28) & t2tb2(v29) % 26.62/4.35 = v31 & tb2t(v33) = v10 & t2tb(v30) = v32 & cons(loc1, v31, v32) = % 26.62/4.35 v33 & list_loc(v30) & loc(v29) & uni(v33) & uni(v32) & uni(v31)))))) % 26.62/4.35 % 26.62/4.35 (function-axioms) % 26.62/4.36 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 26.62/4.36 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 26.62/4.36 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 26.62/4.36 : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ % 26.62/4.36 (match_list(v6, v5, v4, v3, v2) = v1) | ~ (match_list(v6, v5, v4, v3, v2) = % 26.62/4.36 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 26.62/4.36 loc] : ! [v3: list_loc] : ! [v4: map_loc_loc] : ! [v5: loc] : (v1 = v0 | % 26.62/4.36 ~ (list_seg(v5, v4, v3, v2) = v1) | ~ (list_seg(v5, v4, v3, v2) = v0)) & ! % 26.62/4.36 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : ! [v5: % 26.62/4.36 ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ (get(v5, v4, v3, v2) = % 26.62/4.36 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 26.62/4.36 bool] : ! [v5: ty] : (v1 = v0 | ~ (match_bool(v5, v4, v3, v2) = v1) | ~ % 26.62/4.36 (match_bool(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 26.62/4.36 uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | ~ (const(v4, v3, v2) = v1) | % 26.62/4.36 ~ (const(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 26.62/4.36 ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (infix_plpl(v4, v3, v2) = v1) | ~ % 26.62/4.36 (infix_plpl(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 26.62/4.36 MultipleValueBool] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 26.62/4.36 ~ (disjoint(v4, v3, v2) = v1) | ~ (disjoint(v4, v3, v2) = v0)) & ! [v0: % 26.62/4.36 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: % 26.62/4.36 uni] : ! [v4: ty] : (v1 = v0 | ~ (mem(v4, v3, v2) = v1) | ~ (mem(v4, v3, % 26.62/4.36 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : % 26.62/4.36 ! [v4: ty] : (v1 = v0 | ~ (cons(v4, v3, v2) = v1) | ~ (cons(v4, v3, v2) = % 26.62/4.36 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 % 26.62/4.36 | ~ (contents(v3, v2) = v1) | ~ (contents(v3, v2) = v0)) & ! [v0: uni] : % 26.62/4.36 ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) % 26.62/4.36 | ~ (mk_ref(v3, v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! % 26.62/4.36 [v3: ty] : (v1 = v0 | ~ (map(v3, v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: % 26.62/4.36 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 26.62/4.36 (reverse(v3, v2) = v1) | ~ (reverse(v3, v2) = v0)) & ! [v0: int] : ! [v1: % 26.62/4.36 int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (length(v3, v2) = v1) | ~ % 26.62/4.36 (length(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 26.62/4.36 MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 26.62/4.36 (no_repet(v3, v2) = v1) | ~ (no_repet(v3, v2) = v0)) & ! [v0: uni] : ! % 26.62/4.36 [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (tail(v3, v2) = v1) | % 26.62/4.36 ~ (tail(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 26.62/4.36 [v3: ty] : (v1 = v0 | ~ (head(v3, v2) = v1) | ~ (head(v3, v2) = v0)) & ! % 26.62/4.36 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 26.62/4.36 (cons_proj_2(v3, v2) = v1) | ~ (cons_proj_2(v3, v2) = v0)) & ! [v0: uni] : % 26.62/4.36 ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (cons_proj_1(v3, v2) % 26.62/4.36 = v1) | ~ (cons_proj_1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 26.62/4.36 [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (sort(v3, % 26.62/4.36 v2) = v1) | ~ (sort(v3, v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! % 26.62/4.37 [v2: ty] : (v1 = v0 | ~ (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: loc] : % 26.62/4.37 ! [v1: loc] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | ~ (tb2t2(v2) = % 26.62/4.37 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: loc] : (v1 = v0 | ~ % 26.62/4.37 (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! [v0: map_loc_loc] : ! [v1: % 26.62/4.37 map_loc_loc] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ (tb2t1(v2) % 26.62/4.37 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: map_loc_loc] : (v1 = v0 | % 26.62/4.37 ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: list_loc] : ! [v1: % 26.62/4.37 list_loc] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = % 26.62/4.37 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: list_loc] : (v1 = v0 | ~ % 26.62/4.37 (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: % 26.62/4.37 ty] : (v1 = v0 | ~ (list(v2) = v1) | ~ (list(v2) = v0)) & ! [v0: uni] : % 26.62/4.37 ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = v1) | ~ (nil(v2) = v0)) % 26.62/4.37 & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (witness(v2) = v1) % 26.62/4.37 | ~ (witness(v2) = v0)) & ? [v0: uni] : ? [v1: uni] : ? [v2: uni] : ? % 26.62/4.37 [v3: ty] : ? [v4: ty] : ? [v5: uni] : (set(v4, v3, v2, v1, v0) = v5 & % 26.62/4.37 uni(v5)) & ? [v0: uni] : ? [v1: uni] : ? [v2: uni] : ? [v3: ty] : ? % 26.62/4.37 [v4: ty] : ? [v5: uni] : (match_list(v4, v3, v2, v1, v0) = v5 & uni(v5)) & ? % 26.62/4.37 [v0: loc] : ? [v1: list_loc] : ? [v2: map_loc_loc] : ? [v3: loc] : ? [v4: % 26.62/4.37 MultipleValueBool] : (list_seg(v3, v2, v1, v0) = v4) & ? [v0: uni] : ? % 26.62/4.37 [v1: uni] : ? [v2: ty] : ? [v3: ty] : ? [v4: uni] : (get(v3, v2, v1, v0) = % 26.62/4.37 v4 & uni(v4)) & ? [v0: uni] : ? [v1: uni] : ? [v2: bool] : ? [v3: ty] : % 26.62/4.37 ? [v4: uni] : (match_bool(v3, v2, v1, v0) = v4 & uni(v4)) & ? [v0: uni] : ? % 26.62/4.37 [v1: uni] : ? [v2: ty] : ? [v3: MultipleValueBool] : (disjoint(v2, v1, v0) = % 26.62/4.37 v3) & ? [v0: uni] : ? [v1: uni] : ? [v2: ty] : ? [v3: MultipleValueBool] % 26.62/4.37 : (mem(v2, v1, v0) = v3) & ? [v0: uni] : ? [v1: ty] : ? [v2: ty] : ? [v3: % 26.62/4.37 uni] : (const(v2, v1, v0) = v3 & uni(v3)) & ? [v0: uni] : ? [v1: uni] : ? % 26.62/4.37 [v2: ty] : ? [v3: uni] : (infix_plpl(v2, v1, v0) = v3 & uni(v3)) & ? [v0: % 26.62/4.37 uni] : ? [v1: uni] : ? [v2: ty] : ? [v3: uni] : (cons(v2, v1, v0) = v3 & % 26.62/4.37 uni(v3)) & ? [v0: uni] : ? [v1: ty] : ? [v2: int] : (length(v1, v0) = v2) % 26.62/4.37 & ? [v0: uni] : ? [v1: ty] : ? [v2: MultipleValueBool] : (no_repet(v1, v0) % 26.62/4.37 = v2) & ? [v0: uni] : ? [v1: ty] : ? [v2: MultipleValueBool] : (sort(v1, % 26.62/4.37 v0) = v2) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : (contents(v1, v0) % 26.62/4.37 = v2 & uni(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : (mk_ref(v1, % 26.62/4.37 v0) = v2 & uni(v2)) & ? [v0: ty] : ? [v1: ty] : ? [v2: ty] : (map(v1, % 26.62/4.37 v0) = v2 & ty(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : % 26.62/4.37 (reverse(v1, v0) = v2 & uni(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : % 26.62/4.37 (tail(v1, v0) = v2 & uni(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : % 26.62/4.37 (head(v1, v0) = v2 & uni(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: uni] : % 26.62/4.37 (cons_proj_2(v1, v0) = v2 & uni(v2)) & ? [v0: uni] : ? [v1: ty] : ? [v2: % 26.62/4.37 uni] : (cons_proj_1(v1, v0) = v2 & uni(v2)) & ? [v0: ty] : ? [v1: ty] : % 26.62/4.37 (ref(v0) = v1 & ty(v1)) & ? [v0: uni] : ? [v1: loc] : (tb2t2(v0) = v1 & % 26.62/4.37 loc(v1)) & ? [v0: loc] : ? [v1: uni] : (t2tb2(v0) = v1 & uni(v1)) & ? % 26.62/4.37 [v0: uni] : ? [v1: map_loc_loc] : (tb2t1(v0) = v1 & map_loc_loc(v1)) & ? % 26.62/4.37 [v0: map_loc_loc] : ? [v1: uni] : (t2tb1(v0) = v1 & uni(v1)) & ? [v0: uni] : % 26.62/4.37 ? [v1: list_loc] : (tb2t(v0) = v1 & list_loc(v1)) & ? [v0: list_loc] : ? % 26.62/4.37 [v1: uni] : (t2tb(v0) = v1 & uni(v1)) & ? [v0: ty] : ? [v1: ty] : (list(v0) % 26.62/4.37 = v1 & ty(v1)) & ? [v0: ty] : ? [v1: uni] : (nil(v0) = v1 & uni(v1)) & ? % 26.62/4.37 [v0: ty] : ? [v1: uni] : (witness(v0) = v1 & uni(v1)) % 26.62/4.37 % 26.62/4.37 Further assumptions not needed in the proof: % 26.62/4.37 -------------------------------------------- % 26.62/4.37 append_assoc, append_l_nil, append_length, bool_inversion, bridgeL1, bridgeL2, % 26.62/4.37 bridgeR1, bridgeR2, compatOrderMult, cons_proj_1_def, cons_proj_1_sort, % 26.62/4.37 cons_proj_2_def, cons_proj_2_sort, cons_sort, const1, const_sort, contents_def, % 26.62/4.37 contents_sort, disjoint_def, get_sort, head_cons, head_sort, infix_plpl_def, % 26.62/4.37 infix_plpl_sort, length_def, length_nil, length_nonnegative, list_inversion, % 26.62/4.37 list_seg_cons, list_seg_frame, list_seg_functional, list_seg_sublistl, % 26.62/4.37 match_bool_False, match_bool_True, match_bool_sort, match_list_Cons, % 26.62/4.37 match_list_Nil, match_list_sort, mem_append, mem_decomp, mem_def, mk_ref_sort, % 26.62/4.37 nil_sort, no_repet_def, ref_inversion, reverse_append, reverse_cons, % 26.62/4.37 reverse_def, reverse_length, reverse_mem, reverse_reverse, reverse_sort, % 26.62/4.37 select_eq, set_sort, t2tb_sort1, tail_sort, true_False, tuple0_inversion, % 26.62/4.37 witness_sort % 26.62/4.37 % 26.62/4.37 Those formulas are unsatisfiable: % 26.62/4.37 --------------------------------- % 26.62/4.37 % 26.62/4.37 Begin of proof % 26.62/4.37 | % 26.62/4.37 | ALPHA: (t2tb_sort) implies: % 26.62/4.37 | (1) ? [v0: ty] : (list(loc1) = v0 & ty(v0) & ! [v1: list_loc] : ! [v2: % 26.62/4.37 | uni] : ( ~ (t2tb(v1) = v2) | ~ list_loc(v1) | sort(v0, v2) = 0)) % 26.62/4.37 | % 26.62/4.37 | ALPHA: (list_seg_nil) implies: % 26.62/4.37 | (2) ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & nil(loc1) = v0 & % 26.62/4.37 | list_loc(v1) & uni(v0) & ! [v2: loc] : ! [v3: map_loc_loc] : ! % 26.62/4.37 | [v4: int] : (v4 = 0 | ~ (list_seg(v2, v3, v1, v2) = v4) | ~ % 26.62/4.37 | map_loc_loc(v3) | ~ loc(v2))) % 26.62/4.37 | % 26.62/4.37 | ALPHA: (t2tb_sort2) implies: % 26.62/4.37 | (3) ! [v0: loc] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | ~ loc(v0) | % 26.62/4.37 | sort(loc1, v1) = 0) % 26.62/4.37 | % 26.62/4.37 | ALPHA: (list_seg_inversion) implies: % 26.62/4.37 | (4) ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & nil(loc1) = v0 & % 26.62/4.37 | list_loc(v1) & uni(v0) & ! [v2: loc] : ! [v3: map_loc_loc] : ! % 26.62/4.37 | [v4: list_loc] : ! [v5: loc] : ( ~ (list_seg(v2, v3, v4, v5) = 0) | % 26.62/4.37 | ~ map_loc_loc(v3) | ~ list_loc(v4) | ~ loc(v5) | ~ loc(v2) | ? % 26.62/4.37 | [v6: list_loc] : ? [v7: uni] : ? [v8: uni] : ? [v9: uni] : ? % 26.62/4.37 | [v10: loc] : ? [v11: uni] : ? [v12: uni] : ( ~ (v2 = null) & % 26.62/4.37 | tb2t2(v9) = v10 & t2tb2(v2) = v8 & t2tb1(v3) = v7 & list_seg(v10, % 26.62/4.37 | v3, v6, v5) = 0 & tb2t(v12) = v4 & t2tb(v6) = v11 & get(loc1, % 26.62/4.37 | loc1, v7, v8) = v9 & cons(loc1, v8, v11) = v12 & list_loc(v6) & % 26.62/4.37 | loc(v10) & uni(v12) & uni(v11) & uni(v9) & uni(v8) & uni(v7)) | % 26.62/4.37 | (v5 = v2 & v4 = v1))) % 26.62/4.37 | % 26.62/4.37 | ALPHA: (list_seg_no_repet) implies: % 26.62/4.37 | (5) ! [v0: map_loc_loc] : ! [v1: list_loc] : ! [v2: loc] : ( ~ % 26.62/4.37 | (list_seg(v2, v0, v1, null) = 0) | ~ map_loc_loc(v0) | ~ % 26.62/4.37 | list_loc(v1) | ~ loc(v2) | ? [v3: uni] : (t2tb(v1) = v3 & % 26.62/4.37 | no_repet(loc1, v3) = 0 & uni(v3))) % 26.62/4.37 | % 26.62/4.37 | ALPHA: (wP_parameter_in_place_reverse) implies: % 26.62/4.38 | (6) ty(loc1) % 26.62/4.38 | (7) loc(null) % 26.62/4.38 | (8) ? [v0: uni] : ? [v1: list_loc] : (tb2t(v0) = v1 & nil(loc1) = v0 & % 26.62/4.38 | list_loc(v1) & uni(v0) & ? [v2: loc] : ? [v3: list_loc] : ? [v4: % 26.62/4.38 | map_loc_loc] : ? [v5: uni] : ? [v6: uni] : ? [v7: list_loc] : % 26.62/4.38 | (list_seg(v2, v4, v3, null) = 0 & tb2t(v6) = v7 & t2tb(v3) = v5 & % 26.62/4.38 | reverse(loc1, v5) = v6 & map_loc_loc(v4) & list_loc(v7) & % 26.62/4.38 | list_loc(v3) & loc(v2) & uni(v6) & uni(v5) & ? [v8: list_loc] : ? % 26.62/4.38 | [v9: loc] : ? [v10: list_loc] : ? [v11: loc] : ? [v12: % 26.62/4.38 | map_loc_loc] : ? [v13: uni] : ? [v14: uni] : ? [v15: uni] : ? % 26.62/4.38 | [v16: uni] : ? [v17: uni] : ? [v18: uni] : ? [v19: uni] : ? % 26.62/4.38 | [v20: uni] : ? [v21: map_loc_loc] : ? [v22: uni] : ? [v23: loc] % 26.62/4.38 | : ? [v24: uni] : ? [v25: uni] : ? [v26: list_loc] : ? [v27: % 26.62/4.38 | uni] : ? [v28: list_loc] : ( ~ (v11 = null) & tb2t2(v22) = v23 & % 26.62/4.38 | t2tb2(v11) = v18 & t2tb2(v9) = v19 & tb2t1(v20) = v21 & % 26.62/4.38 | t2tb1(v12) = v17 & list_seg(v11, v12, v10, null) = 0 & % 26.62/4.38 | list_seg(v9, v21, v8, null) = 0 & list_seg(v9, v12, v8, null) = 0 % 26.62/4.38 | & tb2t(v27) = v28 & tb2t(v25) = v26 & tb2t(v16) = v7 & t2tb(v10) % 26.62/4.38 | = v13 & t2tb(v8) = v14 & set(loc1, loc1, v17, v18, v19) = v20 & % 26.62/4.38 | get(loc1, loc1, v17, v18) = v22 & reverse(loc1, v13) = v15 & % 26.62/4.38 | infix_plpl(loc1, v15, v14) = v16 & disjoint(loc1, v13, v14) = 0 & % 26.62/4.38 | tail(loc1, v13) = v27 & head(loc1, v13) = v24 & cons(loc1, v24, % 26.62/4.38 | v14) = v25 & map_loc_loc(v21) & map_loc_loc(v12) & % 26.62/4.38 | list_loc(v28) & list_loc(v26) & list_loc(v10) & list_loc(v8) & % 26.62/4.38 | loc(v23) & loc(v11) & loc(v9) & uni(v27) & uni(v25) & uni(v24) & % 26.62/4.38 | uni(v22) & uni(v20) & uni(v19) & uni(v18) & uni(v17) & uni(v16) & % 26.62/4.38 | uni(v15) & uni(v14) & uni(v13) & (v10 = v1 | ? [v29: loc] : ? % 26.62/4.38 | [v30: list_loc] : ? [v31: uni] : ? [v32: uni] : ? [v33: uni] % 26.62/4.38 | : ( ~ (v30 = v28) & t2tb2(v29) = v31 & tb2t(v33) = v10 & % 26.62/4.38 | t2tb(v30) = v32 & cons(loc1, v31, v32) = v33 & list_loc(v30) % 26.62/4.38 | & loc(v29) & uni(v33) & uni(v32) & uni(v31)))))) % 26.62/4.38 | % 26.62/4.38 | ALPHA: (function-axioms) implies: % 26.62/4.38 | (9) ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = % 26.62/4.38 | v1) | ~ (nil(v2) = v0)) % 26.62/4.38 | (10) ! [v0: uni] : ! [v1: uni] : ! [v2: list_loc] : (v1 = v0 | ~ % 26.62/4.38 | (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) % 26.62/4.38 | (11) ! [v0: list_loc] : ! [v1: list_loc] : ! [v2: uni] : (v1 = v0 | ~ % 26.62/4.38 | (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 26.62/4.38 | (12) ! [v0: uni] : ! [v1: uni] : ! [v2: map_loc_loc] : (v1 = v0 | ~ % 26.62/4.38 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 26.62/4.38 | (13) ! [v0: uni] : ! [v1: uni] : ! [v2: loc] : (v1 = v0 | ~ (t2tb2(v2) % 26.62/4.38 | = v1) | ~ (t2tb2(v2) = v0)) % 26.62/4.39 | (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] % 26.62/4.39 | : ! [v3: ty] : (v1 = v0 | ~ (sort(v3, v2) = v1) | ~ (sort(v3, v2) = % 26.62/4.39 | v0)) % 26.62/4.39 | (15) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 26.62/4.39 | ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 26.62/4.39 | (get(v5, v4, v3, v2) = v0)) % 26.62/4.39 | (16) ? [v0: list_loc] : ? [v1: uni] : (t2tb(v0) = v1 & uni(v1)) % 26.62/4.39 | % 26.62/4.39 | DELTA: instantiating (16) with fresh symbols all_92_0, all_92_1 gives: % 26.62/4.39 | (17) t2tb(all_92_1) = all_92_0 & uni(all_92_0) % 26.62/4.39 | % 26.62/4.39 | ALPHA: (17) implies: % 26.62/4.39 | (18) t2tb(all_92_1) = all_92_0 % 26.62/4.39 | % 26.62/4.39 | DELTA: instantiating (1) with fresh symbol all_143_0 gives: % 26.62/4.39 | (19) list(loc1) = all_143_0 & ty(all_143_0) & ! [v0: list_loc] : ! [v1: % 26.62/4.39 | uni] : ( ~ (t2tb(v0) = v1) | ~ list_loc(v0) | sort(all_143_0, v1) = % 26.62/4.39 | 0) % 26.62/4.39 | % 26.62/4.39 | ALPHA: (19) implies: % 26.62/4.39 | (20) ! [v0: list_loc] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ % 26.62/4.39 | list_loc(v0) | sort(all_143_0, v1) = 0) % 26.62/4.39 | % 26.62/4.39 | DELTA: instantiating (2) with fresh symbols all_152_0, all_152_1 gives: % 26.62/4.39 | (21) tb2t(all_152_1) = all_152_0 & nil(loc1) = all_152_1 & % 26.62/4.39 | list_loc(all_152_0) & uni(all_152_1) & ! [v0: loc] : ! [v1: % 26.62/4.39 | map_loc_loc] : ! [v2: int] : (v2 = 0 | ~ (list_seg(v0, v1, % 26.62/4.39 | all_152_0, v0) = v2) | ~ map_loc_loc(v1) | ~ loc(v0)) % 26.62/4.39 | % 26.62/4.39 | ALPHA: (21) implies: % 26.62/4.39 | (22) nil(loc1) = all_152_1 % 26.62/4.39 | (23) tb2t(all_152_1) = all_152_0 % 26.62/4.39 | % 26.62/4.39 | DELTA: instantiating (4) with fresh symbols all_155_0, all_155_1 gives: % 26.62/4.39 | (24) tb2t(all_155_1) = all_155_0 & nil(loc1) = all_155_1 & % 26.62/4.39 | list_loc(all_155_0) & uni(all_155_1) & ! [v0: loc] : ! [v1: % 26.62/4.39 | map_loc_loc] : ! [v2: list_loc] : ! [v3: loc] : ( ~ (list_seg(v0, % 26.62/4.39 | v1, v2, v3) = 0) | ~ map_loc_loc(v1) | ~ list_loc(v2) | ~ % 26.62/4.39 | loc(v3) | ~ loc(v0) | ? [v4: list_loc] : ? [v5: uni] : ? [v6: % 26.62/4.39 | uni] : ? [v7: uni] : ? [v8: loc] : ? [v9: uni] : ? [v10: uni] % 26.62/4.39 | : ( ~ (v0 = null) & tb2t2(v7) = v8 & t2tb2(v0) = v6 & t2tb1(v1) = v5 % 26.62/4.39 | & list_seg(v8, v1, v4, v3) = 0 & tb2t(v10) = v2 & t2tb(v4) = v9 & % 26.62/4.39 | get(loc1, loc1, v5, v6) = v7 & cons(loc1, v6, v9) = v10 & % 26.62/4.39 | list_loc(v4) & loc(v8) & uni(v10) & uni(v9) & uni(v7) & uni(v6) & % 26.62/4.39 | uni(v5)) | (v3 = v0 & v2 = all_155_0)) % 26.62/4.39 | % 26.62/4.39 | ALPHA: (24) implies: % 26.62/4.39 | (25) uni(all_155_1) % 26.62/4.39 | (26) nil(loc1) = all_155_1 % 26.62/4.39 | (27) tb2t(all_155_1) = all_155_0 % 26.62/4.39 | (28) ! [v0: loc] : ! [v1: map_loc_loc] : ! [v2: list_loc] : ! [v3: loc] % 26.62/4.39 | : ( ~ (list_seg(v0, v1, v2, v3) = 0) | ~ map_loc_loc(v1) | ~ % 26.62/4.39 | list_loc(v2) | ~ loc(v3) | ~ loc(v0) | ? [v4: list_loc] : ? [v5: % 26.62/4.39 | uni] : ? [v6: uni] : ? [v7: uni] : ? [v8: loc] : ? [v9: uni] : % 26.62/4.39 | ? [v10: uni] : ( ~ (v0 = null) & tb2t2(v7) = v8 & t2tb2(v0) = v6 & % 26.62/4.39 | t2tb1(v1) = v5 & list_seg(v8, v1, v4, v3) = 0 & tb2t(v10) = v2 & % 26.62/4.39 | t2tb(v4) = v9 & get(loc1, loc1, v5, v6) = v7 & cons(loc1, v6, v9) % 26.62/4.39 | = v10 & list_loc(v4) & loc(v8) & uni(v10) & uni(v9) & uni(v7) & % 26.62/4.39 | uni(v6) & uni(v5)) | (v3 = v0 & v2 = all_155_0)) % 26.62/4.39 | % 26.62/4.39 | DELTA: instantiating (8) with fresh symbols all_158_0, all_158_1 gives: % 26.92/4.40 | (29) tb2t(all_158_1) = all_158_0 & nil(loc1) = all_158_1 & % 26.92/4.40 | list_loc(all_158_0) & uni(all_158_1) & ? [v0: loc] : ? [v1: % 26.92/4.40 | list_loc] : ? [v2: map_loc_loc] : ? [v3: uni] : ? [v4: uni] : ? % 26.92/4.40 | [v5: list_loc] : (list_seg(v0, v2, v1, null) = 0 & tb2t(v4) = v5 & % 26.92/4.40 | t2tb(v1) = v3 & reverse(loc1, v3) = v4 & map_loc_loc(v2) & % 26.92/4.40 | list_loc(v5) & list_loc(v1) & loc(v0) & uni(v4) & uni(v3) & ? [v6: % 26.92/4.40 | list_loc] : ? [v7: loc] : ? [v8: list_loc] : ? [v9: loc] : ? % 26.92/4.40 | [v10: map_loc_loc] : ? [v11: uni] : ? [v12: uni] : ? [v13: uni] : % 26.92/4.40 | ? [v14: uni] : ? [v15: uni] : ? [v16: uni] : ? [v17: uni] : ? % 26.92/4.40 | [v18: uni] : ? [v19: map_loc_loc] : ? [v20: uni] : ? [v21: loc] : % 26.92/4.40 | ? [v22: uni] : ? [v23: uni] : ? [v24: list_loc] : ? [v25: uni] : % 26.92/4.40 | ? [v26: list_loc] : ( ~ (v9 = null) & tb2t2(v20) = v21 & t2tb2(v9) % 26.92/4.40 | = v16 & t2tb2(v7) = v17 & tb2t1(v18) = v19 & t2tb1(v10) = v15 & % 26.92/4.40 | list_seg(v9, v10, v8, null) = 0 & list_seg(v7, v19, v6, null) = 0 % 26.92/4.40 | & list_seg(v7, v10, v6, null) = 0 & tb2t(v25) = v26 & tb2t(v23) = % 26.92/4.40 | v24 & tb2t(v14) = v5 & t2tb(v8) = v11 & t2tb(v6) = v12 & set(loc1, % 26.92/4.40 | loc1, v15, v16, v17) = v18 & get(loc1, loc1, v15, v16) = v20 & % 26.92/4.40 | reverse(loc1, v11) = v13 & infix_plpl(loc1, v13, v12) = v14 & % 26.92/4.40 | disjoint(loc1, v11, v12) = 0 & tail(loc1, v11) = v25 & head(loc1, % 26.92/4.40 | v11) = v22 & cons(loc1, v22, v12) = v23 & map_loc_loc(v19) & % 26.92/4.40 | map_loc_loc(v10) & list_loc(v26) & list_loc(v24) & list_loc(v8) & % 26.92/4.40 | list_loc(v6) & loc(v21) & loc(v9) & loc(v7) & uni(v25) & uni(v23) % 26.92/4.40 | & uni(v22) & uni(v20) & uni(v18) & uni(v17) & uni(v16) & uni(v15) % 26.92/4.40 | & uni(v14) & uni(v13) & uni(v12) & uni(v11) & (v8 = all_158_0 | ? % 26.92/4.40 | [v27: loc] : ? [v28: list_loc] : ? [v29: uni] : ? [v30: uni] % 26.92/4.40 | : ? [v31: uni] : ( ~ (v28 = v26) & t2tb2(v27) = v29 & tb2t(v31) % 26.92/4.40 | = v8 & t2tb(v28) = v30 & cons(loc1, v29, v30) = v31 & % 26.92/4.40 | list_loc(v28) & loc(v27) & uni(v31) & uni(v30) & uni(v29))))) % 26.92/4.40 | % 26.92/4.40 | ALPHA: (29) implies: % 26.92/4.40 | (30) nil(loc1) = all_158_1 % 26.92/4.40 | (31) tb2t(all_158_1) = all_158_0 % 26.92/4.40 | (32) ? [v0: loc] : ? [v1: list_loc] : ? [v2: map_loc_loc] : ? [v3: uni] % 26.92/4.40 | : ? [v4: uni] : ? [v5: list_loc] : (list_seg(v0, v2, v1, null) = 0 & % 26.92/4.40 | tb2t(v4) = v5 & t2tb(v1) = v3 & reverse(loc1, v3) = v4 & % 26.92/4.40 | map_loc_loc(v2) & list_loc(v5) & list_loc(v1) & loc(v0) & uni(v4) & % 26.92/4.40 | uni(v3) & ? [v6: list_loc] : ? [v7: loc] : ? [v8: list_loc] : ? % 26.92/4.40 | [v9: loc] : ? [v10: map_loc_loc] : ? [v11: uni] : ? [v12: uni] : % 26.92/4.40 | ? [v13: uni] : ? [v14: uni] : ? [v15: uni] : ? [v16: uni] : ? % 26.92/4.40 | [v17: uni] : ? [v18: uni] : ? [v19: map_loc_loc] : ? [v20: uni] : % 26.92/4.40 | ? [v21: loc] : ? [v22: uni] : ? [v23: uni] : ? [v24: list_loc] : % 26.92/4.40 | ? [v25: uni] : ? [v26: list_loc] : ( ~ (v9 = null) & tb2t2(v20) = % 26.92/4.40 | v21 & t2tb2(v9) = v16 & t2tb2(v7) = v17 & tb2t1(v18) = v19 & % 26.92/4.40 | t2tb1(v10) = v15 & list_seg(v9, v10, v8, null) = 0 & list_seg(v7, % 26.92/4.40 | v19, v6, null) = 0 & list_seg(v7, v10, v6, null) = 0 & tb2t(v25) % 26.92/4.40 | = v26 & tb2t(v23) = v24 & tb2t(v14) = v5 & t2tb(v8) = v11 & % 26.92/4.40 | t2tb(v6) = v12 & set(loc1, loc1, v15, v16, v17) = v18 & get(loc1, % 26.92/4.40 | loc1, v15, v16) = v20 & reverse(loc1, v11) = v13 & % 26.92/4.40 | infix_plpl(loc1, v13, v12) = v14 & disjoint(loc1, v11, v12) = 0 & % 26.92/4.40 | tail(loc1, v11) = v25 & head(loc1, v11) = v22 & cons(loc1, v22, % 26.92/4.40 | v12) = v23 & map_loc_loc(v19) & map_loc_loc(v10) & list_loc(v26) % 26.92/4.40 | & list_loc(v24) & list_loc(v8) & list_loc(v6) & loc(v21) & loc(v9) % 26.92/4.40 | & loc(v7) & uni(v25) & uni(v23) & uni(v22) & uni(v20) & uni(v18) & % 26.92/4.40 | uni(v17) & uni(v16) & uni(v15) & uni(v14) & uni(v13) & uni(v12) & % 26.92/4.40 | uni(v11) & (v8 = all_158_0 | ? [v27: loc] : ? [v28: list_loc] : % 26.92/4.40 | ? [v29: uni] : ? [v30: uni] : ? [v31: uni] : ( ~ (v28 = v26) & % 26.92/4.40 | t2tb2(v27) = v29 & tb2t(v31) = v8 & t2tb(v28) = v30 & % 26.92/4.40 | cons(loc1, v29, v30) = v31 & list_loc(v28) & loc(v27) & % 26.92/4.40 | uni(v31) & uni(v30) & uni(v29))))) % 26.92/4.40 | % 26.92/4.40 | DELTA: instantiating (32) with fresh symbols all_160_0, all_160_1, all_160_2, % 26.92/4.40 | all_160_3, all_160_4, all_160_5 gives: % 26.92/4.41 | (33) list_seg(all_160_5, all_160_3, all_160_4, null) = 0 & tb2t(all_160_1) % 26.92/4.41 | = all_160_0 & t2tb(all_160_4) = all_160_2 & reverse(loc1, all_160_2) = % 26.92/4.41 | all_160_1 & map_loc_loc(all_160_3) & list_loc(all_160_0) & % 26.92/4.41 | list_loc(all_160_4) & loc(all_160_5) & uni(all_160_1) & uni(all_160_2) % 26.92/4.41 | & ? [v0: list_loc] : ? [v1: loc] : ? [v2: list_loc] : ? [v3: loc] % 26.92/4.41 | : ? [v4: map_loc_loc] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : % 26.92/4.41 | ? [v8: uni] : ? [v9: uni] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 26.92/4.41 | uni] : ? [v13: map_loc_loc] : ? [v14: uni] : ? [v15: loc] : ? % 26.92/4.41 | [v16: uni] : ? [v17: uni] : ? [v18: list_loc] : ? [v19: uni] : ? % 26.92/4.41 | [v20: list_loc] : ( ~ (v3 = null) & tb2t2(v14) = v15 & t2tb2(v3) = v10 % 26.92/4.41 | & t2tb2(v1) = v11 & tb2t1(v12) = v13 & t2tb1(v4) = v9 & list_seg(v3, % 26.92/4.41 | v4, v2, null) = 0 & list_seg(v1, v13, v0, null) = 0 & list_seg(v1, % 26.92/4.41 | v4, v0, null) = 0 & tb2t(v19) = v20 & tb2t(v17) = v18 & tb2t(v8) = % 26.92/4.41 | all_160_0 & t2tb(v2) = v5 & t2tb(v0) = v6 & set(loc1, loc1, v9, v10, % 26.92/4.41 | v11) = v12 & get(loc1, loc1, v9, v10) = v14 & reverse(loc1, v5) = % 26.92/4.41 | v7 & infix_plpl(loc1, v7, v6) = v8 & disjoint(loc1, v5, v6) = 0 & % 26.92/4.41 | tail(loc1, v5) = v19 & head(loc1, v5) = v16 & cons(loc1, v16, v6) = % 26.92/4.41 | v17 & map_loc_loc(v13) & map_loc_loc(v4) & list_loc(v20) & % 26.92/4.41 | list_loc(v18) & list_loc(v2) & list_loc(v0) & loc(v15) & loc(v3) & % 26.92/4.41 | loc(v1) & uni(v19) & uni(v17) & uni(v16) & uni(v14) & uni(v12) & % 26.92/4.41 | uni(v11) & uni(v10) & uni(v9) & uni(v8) & uni(v7) & uni(v6) & % 26.92/4.41 | uni(v5) & (v2 = all_158_0 | ? [v21: loc] : ? [v22: list_loc] : ? % 26.92/4.41 | [v23: uni] : ? [v24: uni] : ? [v25: uni] : ( ~ (v22 = v20) & % 26.92/4.41 | t2tb2(v21) = v23 & tb2t(v25) = v2 & t2tb(v22) = v24 & cons(loc1, % 26.92/4.41 | v23, v24) = v25 & list_loc(v22) & loc(v21) & uni(v25) & % 26.92/4.41 | uni(v24) & uni(v23)))) % 26.92/4.41 | % 26.92/4.41 | ALPHA: (33) implies: % 26.92/4.41 | (34) ? [v0: list_loc] : ? [v1: loc] : ? [v2: list_loc] : ? [v3: loc] : % 26.92/4.41 | ? [v4: map_loc_loc] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? % 26.92/4.41 | [v8: uni] : ? [v9: uni] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 26.92/4.41 | uni] : ? [v13: map_loc_loc] : ? [v14: uni] : ? [v15: loc] : ? % 26.92/4.41 | [v16: uni] : ? [v17: uni] : ? [v18: list_loc] : ? [v19: uni] : ? % 26.92/4.41 | [v20: list_loc] : ( ~ (v3 = null) & tb2t2(v14) = v15 & t2tb2(v3) = v10 % 26.92/4.41 | & t2tb2(v1) = v11 & tb2t1(v12) = v13 & t2tb1(v4) = v9 & list_seg(v3, % 26.92/4.41 | v4, v2, null) = 0 & list_seg(v1, v13, v0, null) = 0 & list_seg(v1, % 26.92/4.41 | v4, v0, null) = 0 & tb2t(v19) = v20 & tb2t(v17) = v18 & tb2t(v8) = % 26.92/4.41 | all_160_0 & t2tb(v2) = v5 & t2tb(v0) = v6 & set(loc1, loc1, v9, v10, % 26.92/4.41 | v11) = v12 & get(loc1, loc1, v9, v10) = v14 & reverse(loc1, v5) = % 26.92/4.41 | v7 & infix_plpl(loc1, v7, v6) = v8 & disjoint(loc1, v5, v6) = 0 & % 26.92/4.41 | tail(loc1, v5) = v19 & head(loc1, v5) = v16 & cons(loc1, v16, v6) = % 26.92/4.41 | v17 & map_loc_loc(v13) & map_loc_loc(v4) & list_loc(v20) & % 26.92/4.41 | list_loc(v18) & list_loc(v2) & list_loc(v0) & loc(v15) & loc(v3) & % 26.92/4.41 | loc(v1) & uni(v19) & uni(v17) & uni(v16) & uni(v14) & uni(v12) & % 26.92/4.41 | uni(v11) & uni(v10) & uni(v9) & uni(v8) & uni(v7) & uni(v6) & % 26.92/4.41 | uni(v5) & (v2 = all_158_0 | ? [v21: loc] : ? [v22: list_loc] : ? % 26.92/4.41 | [v23: uni] : ? [v24: uni] : ? [v25: uni] : ( ~ (v22 = v20) & % 26.92/4.41 | t2tb2(v21) = v23 & tb2t(v25) = v2 & t2tb(v22) = v24 & cons(loc1, % 26.92/4.41 | v23, v24) = v25 & list_loc(v22) & loc(v21) & uni(v25) & % 26.92/4.41 | uni(v24) & uni(v23)))) % 26.92/4.41 | % 26.92/4.41 | DELTA: instantiating (34) with fresh symbols all_162_0, all_162_1, all_162_2, % 26.92/4.41 | all_162_3, all_162_4, all_162_5, all_162_6, all_162_7, all_162_8, % 26.92/4.41 | all_162_9, all_162_10, all_162_11, all_162_12, all_162_13, all_162_14, % 26.92/4.41 | all_162_15, all_162_16, all_162_17, all_162_18, all_162_19, all_162_20 % 26.92/4.41 | gives: % 26.92/4.41 | (35) ~ (all_162_17 = null) & tb2t2(all_162_6) = all_162_5 & % 26.92/4.41 | t2tb2(all_162_17) = all_162_10 & t2tb2(all_162_19) = all_162_9 & % 26.92/4.41 | tb2t1(all_162_8) = all_162_7 & t2tb1(all_162_16) = all_162_11 & % 26.92/4.41 | list_seg(all_162_17, all_162_16, all_162_18, null) = 0 & % 26.92/4.41 | list_seg(all_162_19, all_162_7, all_162_20, null) = 0 & % 26.92/4.41 | list_seg(all_162_19, all_162_16, all_162_20, null) = 0 & % 26.92/4.41 | tb2t(all_162_1) = all_162_0 & tb2t(all_162_3) = all_162_2 & % 26.92/4.41 | tb2t(all_162_12) = all_160_0 & t2tb(all_162_18) = all_162_15 & % 26.92/4.41 | t2tb(all_162_20) = all_162_14 & set(loc1, loc1, all_162_11, % 26.92/4.41 | all_162_10, all_162_9) = all_162_8 & get(loc1, loc1, all_162_11, % 26.92/4.41 | all_162_10) = all_162_6 & reverse(loc1, all_162_15) = all_162_13 & % 26.92/4.41 | infix_plpl(loc1, all_162_13, all_162_14) = all_162_12 & disjoint(loc1, % 26.92/4.41 | all_162_15, all_162_14) = 0 & tail(loc1, all_162_15) = all_162_1 & % 26.92/4.41 | head(loc1, all_162_15) = all_162_4 & cons(loc1, all_162_4, all_162_14) % 26.92/4.41 | = all_162_3 & map_loc_loc(all_162_7) & map_loc_loc(all_162_16) & % 26.92/4.41 | list_loc(all_162_0) & list_loc(all_162_2) & list_loc(all_162_18) & % 26.92/4.41 | list_loc(all_162_20) & loc(all_162_5) & loc(all_162_17) & % 26.92/4.41 | loc(all_162_19) & uni(all_162_1) & uni(all_162_3) & uni(all_162_4) & % 26.92/4.41 | uni(all_162_6) & uni(all_162_8) & uni(all_162_9) & uni(all_162_10) & % 26.92/4.41 | uni(all_162_11) & uni(all_162_12) & uni(all_162_13) & uni(all_162_14) % 26.92/4.41 | & uni(all_162_15) & (all_162_18 = all_158_0 | ? [v0: loc] : ? [v1: % 26.92/4.41 | any] : ? [v2: uni] : ? [v3: uni] : ? [v4: uni] : ( ~ (v1 = % 26.92/4.41 | all_162_0) & t2tb2(v0) = v2 & tb2t(v4) = all_162_18 & t2tb(v1) = % 26.92/4.41 | v3 & cons(loc1, v2, v3) = v4 & list_loc(v1) & loc(v0) & uni(v4) & % 26.92/4.41 | uni(v3) & uni(v2))) % 26.92/4.41 | % 26.92/4.41 | ALPHA: (35) implies: % 26.92/4.41 | (36) ~ (all_162_17 = null) % 26.92/4.41 | (37) uni(all_162_14) % 26.92/4.41 | (38) uni(all_162_9) % 26.92/4.41 | (39) uni(all_162_4) % 26.92/4.41 | (40) loc(all_162_19) % 26.92/4.42 | (41) loc(all_162_17) % 26.92/4.42 | (42) list_loc(all_162_18) % 26.92/4.42 | (43) map_loc_loc(all_162_16) % 26.92/4.42 | (44) cons(loc1, all_162_4, all_162_14) = all_162_3 % 26.92/4.42 | (45) tail(loc1, all_162_15) = all_162_1 % 26.92/4.42 | (46) get(loc1, loc1, all_162_11, all_162_10) = all_162_6 % 26.92/4.42 | (47) t2tb(all_162_18) = all_162_15 % 26.92/4.42 | (48) tb2t(all_162_1) = all_162_0 % 26.92/4.42 | (49) list_seg(all_162_17, all_162_16, all_162_18, null) = 0 % 26.92/4.42 | (50) t2tb1(all_162_16) = all_162_11 % 26.92/4.42 | (51) t2tb2(all_162_19) = all_162_9 % 26.92/4.42 | (52) t2tb2(all_162_17) = all_162_10 % 26.92/4.42 | (53) all_162_18 = all_158_0 | ? [v0: loc] : ? [v1: any] : ? [v2: uni] : % 26.92/4.42 | ? [v3: uni] : ? [v4: uni] : ( ~ (v1 = all_162_0) & t2tb2(v0) = v2 & % 26.92/4.42 | tb2t(v4) = all_162_18 & t2tb(v1) = v3 & cons(loc1, v2, v3) = v4 & % 26.92/4.42 | list_loc(v1) & loc(v0) & uni(v4) & uni(v3) & uni(v2)) % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (9) with all_155_1, all_158_1, loc1, simplifying % 26.92/4.42 | with (26), (30) gives: % 26.92/4.42 | (54) all_158_1 = all_155_1 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (9) with all_152_1, all_158_1, loc1, simplifying % 26.92/4.42 | with (22), (30) gives: % 26.92/4.42 | (55) all_158_1 = all_152_1 % 26.92/4.42 | % 26.92/4.42 | COMBINE_EQS: (54), (55) imply: % 26.92/4.42 | (56) all_155_1 = all_152_1 % 26.92/4.42 | % 26.92/4.42 | SIMP: (56) implies: % 26.92/4.42 | (57) all_155_1 = all_152_1 % 26.92/4.42 | % 26.92/4.42 | REDUCE: (31), (55) imply: % 26.92/4.42 | (58) tb2t(all_152_1) = all_158_0 % 26.92/4.42 | % 26.92/4.42 | REDUCE: (27), (57) imply: % 26.92/4.42 | (59) tb2t(all_152_1) = all_155_0 % 26.92/4.42 | % 26.92/4.42 | REDUCE: (25), (57) imply: % 26.92/4.42 | (60) uni(all_152_1) % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (11) with all_152_0, all_158_0, all_152_1, % 26.92/4.42 | simplifying with (23), (58) gives: % 26.92/4.42 | (61) all_158_0 = all_152_0 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (11) with all_155_0, all_158_0, all_152_1, % 26.92/4.42 | simplifying with (58), (59) gives: % 26.92/4.42 | (62) all_158_0 = all_155_0 % 26.92/4.42 | % 26.92/4.42 | COMBINE_EQS: (61), (62) imply: % 26.92/4.42 | (63) all_155_0 = all_152_0 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (nil_Cons) with loc1, all_162_4, all_162_14, % 26.92/4.42 | all_162_3, simplifying with (6), (37), (39), (44) gives: % 26.92/4.42 | (64) ? [v0: any] : ( ~ (v0 = all_162_3) & nil(loc1) = v0 & uni(v0)) % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (bridgeL) with all_92_1, all_92_0, simplifying with % 26.92/4.42 | (18) gives: % 26.92/4.42 | (65) ~ list_loc(all_92_1) | tb2t(all_92_0) = all_92_1 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (20) with all_92_1, all_92_0, simplifying with (18) % 26.92/4.42 | gives: % 26.92/4.42 | (66) ~ list_loc(all_92_1) | sort(all_143_0, all_92_0) = 0 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (bridgeR) with all_152_1, all_152_0, simplifying % 26.92/4.42 | with (23), (60) gives: % 26.92/4.42 | (67) t2tb(all_152_0) = all_152_1 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (5) with all_162_16, all_162_18, all_162_17, % 26.92/4.42 | simplifying with (41), (42), (43), (49) gives: % 26.92/4.42 | (68) ? [v0: uni] : (t2tb(all_162_18) = v0 & no_repet(loc1, v0) = 0 & % 26.92/4.42 | uni(v0)) % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (28) with all_162_17, all_162_16, all_162_18, null, % 26.92/4.42 | simplifying with (7), (41), (42), (43), (49) gives: % 26.92/4.42 | (69) ? [v0: list_loc] : ? [v1: uni] : ? [v2: uni] : ? [v3: uni] : ? % 26.92/4.42 | [v4: loc] : ? [v5: uni] : ? [v6: uni] : ( ~ (all_162_17 = null) & % 26.92/4.42 | tb2t2(v3) = v4 & t2tb2(all_162_17) = v2 & t2tb1(all_162_16) = v1 & % 26.92/4.42 | list_seg(v4, all_162_16, v0, null) = 0 & tb2t(v6) = all_162_18 & % 26.92/4.42 | t2tb(v0) = v5 & get(loc1, loc1, v1, v2) = v3 & cons(loc1, v2, v5) = % 26.92/4.42 | v6 & list_loc(v0) & loc(v4) & uni(v6) & uni(v5) & uni(v3) & uni(v2) % 26.92/4.42 | & uni(v1)) | (all_162_17 = null & all_162_18 = all_155_0) % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (3) with all_162_19, all_162_9, simplifying with % 26.92/4.42 | (40), (51) gives: % 26.92/4.42 | (70) sort(loc1, all_162_9) = 0 % 26.92/4.42 | % 26.92/4.42 | GROUND_INST: instantiating (3) with all_162_17, all_162_10, simplifying with % 26.92/4.42 | (41), (52) gives: % 26.92/4.42 | (71) sort(loc1, all_162_10) = 0 % 26.92/4.42 | % 26.92/4.42 | DELTA: instantiating (64) with fresh symbol all_187_0 gives: % 26.92/4.42 | (72) ~ (all_187_0 = all_162_3) & nil(loc1) = all_187_0 & uni(all_187_0) % 26.92/4.42 | % 26.92/4.42 | ALPHA: (72) implies: % 26.92/4.42 | (73) nil(loc1) = all_187_0 % 26.92/4.42 | % 26.92/4.42 | DELTA: instantiating (68) with fresh symbol all_189_0 gives: % 26.92/4.42 | (74) t2tb(all_162_18) = all_189_0 & no_repet(loc1, all_189_0) = 0 & % 26.92/4.42 | uni(all_189_0) % 26.92/4.42 | % 26.92/4.42 | ALPHA: (74) implies: % 26.92/4.42 | (75) t2tb(all_162_18) = all_189_0 % 26.92/4.42 | % 26.92/4.42 | BETA: splitting (69) gives: % 26.92/4.42 | % 26.92/4.42 | Case 1: % 26.92/4.42 | | % 26.92/4.43 | | (76) ? [v0: list_loc] : ? [v1: uni] : ? [v2: uni] : ? [v3: uni] : ? % 26.92/4.43 | | [v4: loc] : ? [v5: uni] : ? [v6: uni] : ( ~ (all_162_17 = null) & % 26.92/4.43 | | tb2t2(v3) = v4 & t2tb2(all_162_17) = v2 & t2tb1(all_162_16) = v1 & % 26.92/4.43 | | list_seg(v4, all_162_16, v0, null) = 0 & tb2t(v6) = all_162_18 & % 26.92/4.43 | | t2tb(v0) = v5 & get(loc1, loc1, v1, v2) = v3 & cons(loc1, v2, v5) % 26.92/4.43 | | = v6 & list_loc(v0) & loc(v4) & uni(v6) & uni(v5) & uni(v3) & % 26.92/4.43 | | uni(v2) & uni(v1)) % 26.92/4.43 | | % 26.92/4.43 | | DELTA: instantiating (76) with fresh symbols all_195_0, all_195_1, % 26.92/4.43 | | all_195_2, all_195_3, all_195_4, all_195_5, all_195_6 gives: % 26.92/4.43 | | (77) ~ (all_162_17 = null) & tb2t2(all_195_3) = all_195_2 & % 26.92/4.43 | | t2tb2(all_162_17) = all_195_4 & t2tb1(all_162_16) = all_195_5 & % 26.92/4.43 | | list_seg(all_195_2, all_162_16, all_195_6, null) = 0 & % 26.92/4.43 | | tb2t(all_195_0) = all_162_18 & t2tb(all_195_6) = all_195_1 & % 26.92/4.43 | | get(loc1, loc1, all_195_5, all_195_4) = all_195_3 & cons(loc1, % 26.92/4.43 | | all_195_4, all_195_1) = all_195_0 & list_loc(all_195_6) & % 26.92/4.43 | | loc(all_195_2) & uni(all_195_0) & uni(all_195_1) & uni(all_195_3) & % 26.92/4.43 | | uni(all_195_4) & uni(all_195_5) % 26.92/4.43 | | % 26.92/4.43 | | ALPHA: (77) implies: % 26.92/4.43 | | (78) uni(all_195_5) % 26.92/4.43 | | (79) uni(all_195_4) % 26.92/4.43 | | (80) uni(all_195_1) % 26.92/4.43 | | (81) uni(all_195_0) % 26.92/4.43 | | (82) cons(loc1, all_195_4, all_195_1) = all_195_0 % 26.92/4.43 | | (83) get(loc1, loc1, all_195_5, all_195_4) = all_195_3 % 26.92/4.43 | | (84) tb2t(all_195_0) = all_162_18 % 26.92/4.43 | | (85) t2tb1(all_162_16) = all_195_5 % 26.92/4.43 | | (86) t2tb2(all_162_17) = all_195_4 % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (9) with all_152_1, all_187_0, loc1, simplifying % 26.92/4.43 | | with (22), (73) gives: % 26.92/4.43 | | (87) all_187_0 = all_152_1 % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (10) with all_162_15, all_189_0, all_162_18, % 26.92/4.43 | | simplifying with (47), (75) gives: % 26.92/4.43 | | (88) all_189_0 = all_162_15 % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (12) with all_162_11, all_195_5, all_162_16, % 26.92/4.43 | | simplifying with (50), (85) gives: % 26.92/4.43 | | (89) all_195_5 = all_162_11 % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (13) with all_162_10, all_195_4, all_162_17, % 26.92/4.43 | | simplifying with (52), (86) gives: % 26.92/4.43 | | (90) all_195_4 = all_162_10 % 26.92/4.43 | | % 26.92/4.43 | | REDUCE: (83), (89), (90) imply: % 26.92/4.43 | | (91) get(loc1, loc1, all_162_11, all_162_10) = all_195_3 % 26.92/4.43 | | % 26.92/4.43 | | REDUCE: (82), (90) imply: % 26.92/4.43 | | (92) cons(loc1, all_162_10, all_195_1) = all_195_0 % 26.92/4.43 | | % 26.92/4.43 | | REDUCE: (79), (90) imply: % 26.92/4.43 | | (93) uni(all_162_10) % 26.92/4.43 | | % 26.92/4.43 | | REDUCE: (78), (89) imply: % 26.92/4.43 | | (94) uni(all_162_11) % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (15) with all_162_6, all_195_3, all_162_10, % 26.92/4.43 | | all_162_11, loc1, loc1, simplifying with (46), (91) gives: % 26.92/4.43 | | (95) all_195_3 = all_162_6 % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (select_neq) with loc1, loc1, all_162_11, % 26.92/4.43 | | all_162_9, all_162_10, all_162_6, simplifying with (6), (38), % 26.92/4.43 | | (46), (70), (93), (94) gives: % 26.92/4.43 | | (96) ? [v0: int] : ( ~ (v0 = 0) & sort(loc1, all_162_10) = v0) | ! [v0: % 26.92/4.43 | | uni] : ! [v1: uni] : ! [v2: int] : (v2 = all_162_6 | all_162_9 = % 26.92/4.43 | | all_162_10 | ~ (set(loc1, loc1, all_162_11, all_162_9, v0) = v1) % 26.92/4.43 | | | ~ (get(loc1, loc1, v1, all_162_10) = v2) | ~ uni(v0)) % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (nil_Cons) with loc1, all_162_10, all_195_1, % 26.92/4.43 | | all_195_0, simplifying with (6), (80), (92), (93) gives: % 26.92/4.43 | | (97) ? [v0: any] : ( ~ (v0 = all_195_0) & nil(loc1) = v0 & uni(v0)) % 26.92/4.43 | | % 26.92/4.43 | | GROUND_INST: instantiating (bridgeR) with all_195_0, all_162_18, simplifying % 26.92/4.43 | | with (81), (84) gives: % 26.92/4.43 | | (98) t2tb(all_162_18) = all_195_0 % 26.92/4.43 | | % 26.92/4.43 | | DELTA: instantiating (97) with fresh symbol all_220_0 gives: % 26.92/4.43 | | (99) ~ (all_220_0 = all_195_0) & nil(loc1) = all_220_0 & uni(all_220_0) % 26.92/4.43 | | % 26.92/4.43 | | ALPHA: (99) implies: % 26.92/4.43 | | (100) ~ (all_220_0 = all_195_0) % 26.92/4.43 | | (101) nil(loc1) = all_220_0 % 26.92/4.43 | | % 26.92/4.43 | | BETA: splitting (96) gives: % 26.92/4.43 | | % 26.92/4.43 | | Case 1: % 26.92/4.43 | | | % 26.92/4.43 | | | (102) ? [v0: int] : ( ~ (v0 = 0) & sort(loc1, all_162_10) = v0) % 26.92/4.43 | | | % 26.92/4.43 | | | DELTA: instantiating (102) with fresh symbol all_228_0 gives: % 26.92/4.43 | | | (103) ~ (all_228_0 = 0) & sort(loc1, all_162_10) = all_228_0 % 26.92/4.43 | | | % 26.92/4.43 | | | ALPHA: (103) implies: % 26.92/4.43 | | | (104) ~ (all_228_0 = 0) % 26.92/4.43 | | | (105) sort(loc1, all_162_10) = all_228_0 % 26.92/4.43 | | | % 26.92/4.43 | | | GROUND_INST: instantiating (14) with 0, all_228_0, all_162_10, loc1, % 26.92/4.43 | | | simplifying with (71), (105) gives: % 26.92/4.43 | | | (106) all_228_0 = 0 % 26.92/4.43 | | | % 26.92/4.43 | | | REDUCE: (104), (106) imply: % 26.92/4.43 | | | (107) $false % 26.92/4.43 | | | % 26.92/4.43 | | | CLOSE: (107) is inconsistent. % 26.92/4.43 | | | % 26.92/4.43 | | Case 2: % 26.92/4.43 | | | % 26.92/4.43 | | | % 26.92/4.43 | | | GROUND_INST: instantiating (9) with all_152_1, all_220_0, loc1, % 26.92/4.43 | | | simplifying with (22), (101) gives: % 26.92/4.43 | | | (108) all_220_0 = all_152_1 % 26.92/4.43 | | | % 26.92/4.43 | | | GROUND_INST: instantiating (10) with all_162_15, all_195_0, all_162_18, % 26.92/4.43 | | | simplifying with (47), (98) gives: % 26.92/4.43 | | | (109) all_195_0 = all_162_15 % 26.92/4.43 | | | % 26.92/4.43 | | | REDUCE: (100), (108), (109) imply: % 26.92/4.43 | | | (110) ~ (all_162_15 = all_152_1) % 26.92/4.43 | | | % 26.92/4.43 | | | SIMP: (110) implies: % 26.92/4.43 | | | (111) ~ (all_162_15 = all_152_1) % 26.92/4.43 | | | % 26.92/4.43 | | | BETA: splitting (53) gives: % 26.92/4.43 | | | % 26.92/4.43 | | | Case 1: % 26.92/4.43 | | | | % 26.92/4.44 | | | | (112) all_162_18 = all_158_0 % 26.92/4.44 | | | | % 26.92/4.44 | | | | COMBINE_EQS: (61), (112) imply: % 26.92/4.44 | | | | (113) all_162_18 = all_152_0 % 26.92/4.44 | | | | % 26.92/4.44 | | | | REDUCE: (47), (113) imply: % 26.92/4.44 | | | | (114) t2tb(all_152_0) = all_162_15 % 26.92/4.44 | | | | % 26.92/4.44 | | | | GROUND_INST: instantiating (10) with all_152_1, all_162_15, all_152_0, % 26.92/4.44 | | | | simplifying with (67), (114) gives: % 26.92/4.44 | | | | (115) all_162_15 = all_152_1 % 26.92/4.44 | | | | % 26.92/4.44 | | | | REDUCE: (111), (115) imply: % 26.92/4.44 | | | | (116) $false % 26.92/4.44 | | | | % 26.92/4.44 | | | | CLOSE: (116) is inconsistent. % 26.92/4.44 | | | | % 26.92/4.44 | | | Case 2: % 26.92/4.44 | | | | % 26.92/4.44 | | | | (117) ? [v0: loc] : ? [v1: any] : ? [v2: uni] : ? [v3: uni] : ? % 26.92/4.44 | | | | [v4: uni] : ( ~ (v1 = all_162_0) & t2tb2(v0) = v2 & tb2t(v4) = % 26.92/4.44 | | | | all_162_18 & t2tb(v1) = v3 & cons(loc1, v2, v3) = v4 & % 26.92/4.44 | | | | list_loc(v1) & loc(v0) & uni(v4) & uni(v3) & uni(v2)) % 26.92/4.44 | | | | % 26.92/4.44 | | | | DELTA: instantiating (117) with fresh symbols all_285_0, all_285_1, % 26.92/4.44 | | | | all_285_2, all_285_3, all_285_4 gives: % 26.92/4.44 | | | | (118) ~ (all_285_3 = all_162_0) & t2tb2(all_285_4) = all_285_2 & % 26.92/4.44 | | | | tb2t(all_285_0) = all_162_18 & t2tb(all_285_3) = all_285_1 & % 26.92/4.44 | | | | cons(loc1, all_285_2, all_285_1) = all_285_0 & % 26.92/4.44 | | | | list_loc(all_285_3) & loc(all_285_4) & uni(all_285_0) & % 26.92/4.44 | | | | uni(all_285_1) & uni(all_285_2) % 26.92/4.44 | | | | % 26.92/4.44 | | | | ALPHA: (118) implies: % 26.92/4.44 | | | | (119) ~ (all_285_3 = all_162_0) % 26.92/4.44 | | | | (120) uni(all_285_2) % 26.92/4.44 | | | | (121) uni(all_285_1) % 26.92/4.44 | | | | (122) uni(all_285_0) % 26.92/4.44 | | | | (123) list_loc(all_285_3) % 26.92/4.44 | | | | (124) cons(loc1, all_285_2, all_285_1) = all_285_0 % 26.92/4.44 | | | | (125) t2tb(all_285_3) = all_285_1 % 26.92/4.44 | | | | (126) tb2t(all_285_0) = all_162_18 % 26.92/4.44 | | | | % 26.92/4.44 | | | | GROUND_INST: instantiating (bridgeL) with all_285_3, all_285_1, % 26.92/4.44 | | | | simplifying with (123), (125) gives: % 26.92/4.44 | | | | (127) tb2t(all_285_1) = all_285_3 % 26.92/4.44 | | | | % 26.92/4.44 | | | | GROUND_INST: instantiating (bridgeR) with all_285_0, all_162_18, % 26.92/4.44 | | | | simplifying with (122), (126) gives: % 26.92/4.44 | | | | (128) t2tb(all_162_18) = all_285_0 % 26.92/4.44 | | | | % 26.92/4.44 | | | | GROUND_INST: instantiating (10) with all_162_15, all_285_0, all_162_18, % 26.92/4.44 | | | | simplifying with (47), (128) gives: % 26.92/4.44 | | | | (129) all_285_0 = all_162_15 % 26.92/4.44 | | | | % 26.92/4.44 | | | | REDUCE: (124), (129) imply: % 26.92/4.44 | | | | (130) cons(loc1, all_285_2, all_285_1) = all_162_15 % 26.92/4.44 | | | | % 26.92/4.44 | | | | BETA: splitting (65) gives: % 26.92/4.44 | | | | % 26.92/4.44 | | | | Case 1: % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | GROUND_INST: instantiating (tail_cons) with loc1, all_285_2, % 26.92/4.44 | | | | | all_285_1, all_162_15, all_162_1, simplifying with (6), % 26.92/4.44 | | | | | (45), (120), (121), (130) gives: % 26.92/4.44 | | | | | (131) all_285_1 = all_162_1 % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | REDUCE: (127), (131) imply: % 26.92/4.44 | | | | | (132) tb2t(all_162_1) = all_285_3 % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | REF_CLOSE: (11), (48), (119), (132) are inconsistent by sub-proof #1. % 26.92/4.44 | | | | | % 26.92/4.44 | | | | Case 2: % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | (133) list_loc(all_92_1) % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | BETA: splitting (66) gives: % 26.92/4.44 | | | | | % 26.92/4.44 | | | | | Case 1: % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | (134) ~ list_loc(all_92_1) % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | PRED_UNIFY: (133), (134) imply: % 26.92/4.44 | | | | | | (135) $false % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | CLOSE: (135) is inconsistent. % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | Case 2: % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | GROUND_INST: instantiating (tail_cons) with loc1, all_285_2, % 26.92/4.44 | | | | | | all_285_1, all_162_15, all_162_1, simplifying with (6), % 26.92/4.44 | | | | | | (45), (120), (121), (130) gives: % 26.92/4.44 | | | | | | (136) all_285_1 = all_162_1 % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | REDUCE: (127), (136) imply: % 26.92/4.44 | | | | | | (137) tb2t(all_162_1) = all_285_3 % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | | REF_CLOSE: (11), (48), (119), (137) are inconsistent by sub-proof % 26.92/4.44 | | | | | | #1. % 26.92/4.44 | | | | | | % 26.92/4.44 | | | | | End of split % 26.92/4.44 | | | | | % 26.92/4.44 | | | | End of split % 26.92/4.44 | | | | % 26.92/4.44 | | | End of split % 26.92/4.44 | | | % 26.92/4.44 | | End of split % 26.92/4.44 | | % 26.92/4.44 | Case 2: % 26.92/4.44 | | % 26.92/4.44 | | (138) all_162_17 = null & all_162_18 = all_155_0 % 26.92/4.44 | | % 26.92/4.44 | | ALPHA: (138) implies: % 26.92/4.44 | | (139) all_162_17 = null % 26.92/4.44 | | % 26.92/4.44 | | REDUCE: (36), (139) imply: % 26.92/4.44 | | (140) $false % 26.92/4.44 | | % 26.92/4.44 | | CLOSE: (140) is inconsistent. % 26.92/4.44 | | % 26.92/4.44 | End of split % 26.92/4.44 | % 26.92/4.44 End of proof % 26.92/4.44 % 26.92/4.44 Sub-proof #1 shows that the following formulas are inconsistent: % 26.92/4.44 ---------------------------------------------------------------- % 26.92/4.44 (1) ! [v0: list_loc] : ! [v1: list_loc] : ! [v2: uni] : (v1 = v0 | ~ % 26.92/4.44 (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 26.92/4.44 (2) tb2t(all_162_1) = all_285_3 % 26.92/4.44 (3) tb2t(all_162_1) = all_162_0 % 26.92/4.44 (4) ~ (all_285_3 = all_162_0) % 26.92/4.44 % 26.92/4.44 Begin of proof % 26.92/4.44 | % 26.92/4.44 | GROUND_INST: instantiating (1) with all_162_0, all_285_3, all_162_1, % 26.92/4.44 | simplifying with (2), (3) gives: % 26.92/4.44 | (5) all_285_3 = all_162_0 % 26.92/4.44 | % 26.92/4.44 | REDUCE: (4), (5) imply: % 26.92/4.44 | (6) $false % 26.92/4.44 | % 26.92/4.44 | CLOSE: (6) is inconsistent. % 26.92/4.44 | % 26.92/4.44 End of proof % 26.92/4.44 % SZS output end Proof for theBenchmark % 26.92/4.44 % 26.92/4.44 3836ms %------------------------------------------------------------------------------