%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW589_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 : n017.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:49 EDT 2023 % Result : Theorem 41.35s 6.42s % Output : Proof 42.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWW589_2 : TPTP v8.1.2. Released v6.1.0. % 0.06/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.32 % Computer : n017.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Aug 27 19:20:42 EDT 2023 % 0.11/0.32 % CPUTime : % 0.17/0.61 ________ _____ % 0.17/0.61 ___ __ \_________(_)________________________________ % 0.17/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.17/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.17/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.17/0.61 % 0.17/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.17/0.61 (2023-06-19) % 0.17/0.61 % 0.17/0.61 (c) Philipp Rümmer, 2009-2023 % 0.17/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.17/0.61 Amanda Stjerna. % 0.17/0.61 Free software under BSD-3-Clause. % 0.17/0.61 % 0.17/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.17/0.61 % 0.17/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.56/0.63 Running up to 7 provers in parallel. % 0.56/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.56/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.56/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.56/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.56/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.56/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.56/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 5.75/1.62 Prover 4: Preprocessing ... % 5.75/1.62 Prover 5: Preprocessing ... % 5.89/1.62 Prover 6: Preprocessing ... % 5.89/1.63 Prover 1: Preprocessing ... % 5.89/1.63 Prover 3: Preprocessing ... % 5.89/1.63 Prover 0: Preprocessing ... % 5.89/1.64 Prover 2: Preprocessing ... % 17.43/3.22 Prover 1: Warning: ignoring some quantifiers % 17.43/3.24 Prover 3: Warning: ignoring some quantifiers % 17.43/3.26 Prover 6: Proving ... % 17.43/3.27 Prover 5: Proving ... % 17.43/3.32 Prover 4: Warning: ignoring some quantifiers % 17.43/3.36 Prover 1: Constructing countermodel ... % 18.28/3.37 Prover 3: Constructing countermodel ... % 18.77/3.40 Prover 0: Proving ... % 18.77/3.40 Prover 4: Constructing countermodel ... % 20.25/3.59 Prover 2: Proving ... % 24.98/4.28 Prover 3: gave up % 25.55/4.29 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 26.59/4.47 Prover 7: Preprocessing ... % 28.96/4.82 Prover 1: gave up % 29.61/4.84 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.61/4.86 Prover 7: Warning: ignoring some quantifiers % 30.50/4.95 Prover 7: Constructing countermodel ... % 31.25/5.10 Prover 8: Preprocessing ... % 35.65/5.63 Prover 8: Warning: ignoring some quantifiers % 36.05/5.68 Prover 8: Constructing countermodel ... % 41.35/6.40 Prover 7: Found proof (size 128) % 41.35/6.40 Prover 7: proved (2105ms) % 41.35/6.40 Prover 0: stopped % 41.35/6.40 Prover 6: stopped % 41.35/6.40 Prover 2: stopped % 41.35/6.40 Prover 8: stopped % 41.35/6.41 Prover 5: stopped % 41.35/6.42 Prover 4: stopped % 41.35/6.42 % 41.35/6.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 41.35/6.42 % 41.35/6.45 % SZS output start Proof for theBenchmark % 41.35/6.46 Assumptions after simplification: % 41.35/6.46 --------------------------------- % 41.35/6.46 % 41.35/6.46 (bridgeL2) % 41.80/6.48 ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | tb2t2(v1) = v0) % 41.80/6.48 % 41.80/6.48 (bridgeR5) % 41.80/6.48 ! [v0: uni] : ! [v1: map_int_int] : ( ~ (tb2t5(v0) = v1) | ~ uni(v0) | % 41.85/6.48 t2tb5(v1) = v0) % 41.85/6.48 % 41.85/6.48 (but_last_def) % 41.85/6.49 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.85/6.49 & list_char(v1) & uni(v0) & ! [v2: char1] : ! [v3: char1] : ! [v4: % 41.85/6.49 list_char] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 41.85/6.49 list_char] : ! [v9: list_char] : ( ~ (but_last1(v2, v8) = v9) | ~ % 41.85/6.49 (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ (t2tb(v4) = v6) | ~ % 41.85/6.49 (cons(char, v5, v6) = v7) | ~ list_char(v4) | ~ char1(v3) | ~ char1(v2) % 41.85/6.49 | ? [v10: uni] : ? [v11: list_char] : ? [v12: uni] : ? [v13: uni] : % 41.85/6.49 (but_last1(v3, v4) = v11 & t2tb1(v2) = v10 & tb2t(v13) = v9 & t2tb(v11) = % 41.85/6.49 v12 & cons(char, v10, v12) = v13 & list_char(v11) & list_char(v9) & % 41.85/6.49 uni(v13) & uni(v12) & uni(v10))) & ! [v2: char1] : ! [v3: char1] : ! % 41.85/6.49 [v4: list_char] : ! [v5: uni] : ! [v6: list_char] : ! [v7: uni] : ! [v8: % 41.85/6.49 uni] : ( ~ (but_last1(v3, v4) = v6) | ~ (t2tb1(v2) = v5) | ~ (t2tb(v6) = % 41.85/6.49 v7) | ~ (cons(char, v5, v7) = v8) | ~ list_char(v4) | ~ char1(v3) | % 41.85/6.49 ~ char1(v2) | ? [v9: uni] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 41.85/6.49 list_char] : ? [v13: list_char] : (but_last1(v2, v12) = v13 & t2tb1(v3) % 41.85/6.49 = v9 & tb2t(v11) = v12 & tb2t(v8) = v13 & t2tb(v4) = v10 & cons(char, % 41.85/6.49 v9, v10) = v11 & list_char(v13) & list_char(v12) & uni(v11) & uni(v10) % 41.85/6.49 & uni(v9))) & ! [v2: char1] : ! [v3: list_char] : (v3 = v1 | ~ % 41.85/6.49 (but_last1(v2, v1) = v3) | ~ char1(v2))) % 41.85/6.49 % 41.85/6.49 (dist_eps) % 41.85/6.50 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.85/6.50 & list_char(v1) & uni(v0) & dist1(v1, v1, 0)) % 41.85/6.50 % 41.85/6.50 (dist_inversion) % 41.99/6.51 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.99/6.51 & list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: list_char] : ! % 41.99/6.51 [v4: int] : (v4 = 0 | ~ list_char(v3) | ~ list_char(v2) | ~ dist1(v2, v3, % 41.99/6.51 v4) | ? [v5: list_char] : ? [v6: list_char] : ? [v7: int] : ? [v8: % 41.99/6.51 uni] : ? [v9: uni] : ? [v10: char1] : ? [v11: uni] : ? [v12: uni] : % 41.99/6.51 ? [v13: list_char] : ? [v14: uni] : ? [v15: list_char] : ? [v16: % 41.99/6.51 list_char] : ? [v17: list_char] : ? [v18: int] : ? [v19: uni] : ? % 41.99/6.52 [v20: char1] : ? [v21: uni] : ? [v22: uni] : ? [v23: list_char] : ? % 41.99/6.52 [v24: list_char] : ? [v25: list_char] : ? [v26: int] : ? [v27: uni] : % 41.99/6.52 ? [v28: char1] : ? [v29: uni] : ? [v30: uni] : ? [v31: list_char] : % 41.99/6.52 (list_char(v25) & list_char(v24) & list_char(v17) & list_char(v16) & % 41.99/6.52 list_char(v6) & list_char(v5) & char1(v28) & char1(v20) & char1(v10) & % 41.99/6.52 ((v31 = v2 & $difference(v26, v4) = -1 & v25 = v3 & t2tb1(v28) = v29 & % 41.99/6.52 tb2t(v30) = v2 & t2tb(v24) = v27 & cons(char, v29, v27) = v30 & % 41.99/6.52 uni(v30) & uni(v29) & uni(v27) & dist1(v24, v3, $sum(v4, -1))) | % 41.99/6.52 (v23 = v3 & $difference(v18, v4) = -1 & v16 = v2 & t2tb1(v20) = v21 & % 41.99/6.52 tb2t(v22) = v3 & t2tb(v17) = v19 & cons(char, v21, v19) = v22 & % 41.99/6.52 uni(v22) & uni(v21) & uni(v19) & dist1(v2, v17, $sum(v4, -1))) | % 41.99/6.52 (v15 = v3 & v13 = v2 & v7 = v4 & t2tb1(v10) = v11 & tb2t(v14) = v3 & % 41.99/6.52 tb2t(v12) = v2 & t2tb(v6) = v9 & t2tb(v5) = v8 & cons(char, v11, v9) % 41.99/6.52 = v14 & cons(char, v11, v8) = v12 & uni(v14) & uni(v12) & uni(v11) & % 41.99/6.52 uni(v9) & uni(v8) & dist1(v5, v6, v4))))) & ! [v2: list_char] : ! % 41.99/6.52 [v3: list_char] : ! [v4: int] : (v3 = v1 | ~ list_char(v3) | ~ % 41.99/6.52 list_char(v2) | ~ dist1(v2, v3, v4) | ? [v5: list_char] : ? [v6: % 41.99/6.52 list_char] : ? [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: % 41.99/6.52 char1] : ? [v11: uni] : ? [v12: uni] : ? [v13: list_char] : ? [v14: % 41.99/6.52 uni] : ? [v15: list_char] : ? [v16: list_char] : ? [v17: list_char] : % 41.99/6.52 ? [v18: int] : ? [v19: uni] : ? [v20: char1] : ? [v21: uni] : ? [v22: % 41.99/6.52 uni] : ? [v23: list_char] : ? [v24: list_char] : ? [v25: list_char] : % 41.99/6.52 ? [v26: int] : ? [v27: uni] : ? [v28: char1] : ? [v29: uni] : ? [v30: % 41.99/6.52 uni] : ? [v31: list_char] : (list_char(v25) & list_char(v24) & % 41.99/6.52 list_char(v17) & list_char(v16) & list_char(v6) & list_char(v5) & % 41.99/6.52 char1(v28) & char1(v20) & char1(v10) & ((v31 = v2 & $difference(v26, v4) % 41.99/6.52 = -1 & v25 = v3 & t2tb1(v28) = v29 & tb2t(v30) = v2 & t2tb(v24) = % 41.99/6.52 v27 & cons(char, v29, v27) = v30 & uni(v30) & uni(v29) & uni(v27) & % 41.99/6.52 dist1(v24, v3, $sum(v4, -1))) | (v23 = v3 & $difference(v18, v4) = % 41.99/6.52 -1 & v16 = v2 & t2tb1(v20) = v21 & tb2t(v22) = v3 & t2tb(v17) = v19 % 41.99/6.52 & cons(char, v21, v19) = v22 & uni(v22) & uni(v21) & uni(v19) & % 41.99/6.52 dist1(v2, v17, $sum(v4, -1))) | (v15 = v3 & v13 = v2 & v7 = v4 & % 41.99/6.52 t2tb1(v10) = v11 & tb2t(v14) = v3 & tb2t(v12) = v2 & t2tb(v6) = v9 & % 41.99/6.52 t2tb(v5) = v8 & cons(char, v11, v9) = v14 & cons(char, v11, v8) = % 41.99/6.52 v12 & uni(v14) & uni(v12) & uni(v11) & uni(v9) & uni(v8) & dist1(v5, % 41.99/6.52 v6, v4))))) & ! [v2: list_char] : ! [v3: list_char] : ! [v4: % 41.99/6.52 int] : (v2 = v1 | ~ list_char(v3) | ~ list_char(v2) | ~ dist1(v2, v3, % 41.99/6.52 v4) | ? [v5: list_char] : ? [v6: list_char] : ? [v7: int] : ? [v8: % 41.99/6.52 uni] : ? [v9: uni] : ? [v10: char1] : ? [v11: uni] : ? [v12: uni] : % 41.99/6.52 ? [v13: list_char] : ? [v14: uni] : ? [v15: list_char] : ? [v16: % 41.99/6.52 list_char] : ? [v17: list_char] : ? [v18: int] : ? [v19: uni] : ? % 41.99/6.52 [v20: char1] : ? [v21: uni] : ? [v22: uni] : ? [v23: list_char] : ? % 41.99/6.52 [v24: list_char] : ? [v25: list_char] : ? [v26: int] : ? [v27: uni] : % 41.99/6.52 ? [v28: char1] : ? [v29: uni] : ? [v30: uni] : ? [v31: list_char] : % 41.99/6.52 (list_char(v25) & list_char(v24) & list_char(v17) & list_char(v16) & % 41.99/6.52 list_char(v6) & list_char(v5) & char1(v28) & char1(v20) & char1(v10) & % 41.99/6.52 ((v31 = v2 & $difference(v26, v4) = -1 & v25 = v3 & t2tb1(v28) = v29 & % 41.99/6.52 tb2t(v30) = v2 & t2tb(v24) = v27 & cons(char, v29, v27) = v30 & % 41.99/6.52 uni(v30) & uni(v29) & uni(v27) & dist1(v24, v3, $sum(v4, -1))) | % 41.99/6.52 (v23 = v3 & $difference(v18, v4) = -1 & v16 = v2 & t2tb1(v20) = v21 & % 41.99/6.52 tb2t(v22) = v3 & t2tb(v17) = v19 & cons(char, v21, v19) = v22 & % 41.99/6.52 uni(v22) & uni(v21) & uni(v19) & dist1(v2, v17, $sum(v4, -1))) | % 41.99/6.52 (v15 = v3 & v13 = v2 & v7 = v4 & t2tb1(v10) = v11 & tb2t(v14) = v3 & % 41.99/6.52 tb2t(v12) = v2 & t2tb(v6) = v9 & t2tb(v5) = v8 & cons(char, v11, v9) % 41.99/6.52 = v14 & cons(char, v11, v8) = v12 & uni(v14) & uni(v12) & uni(v11) & % 41.99/6.52 uni(v9) & uni(v8) & dist1(v5, v6, v4)))))) % 41.99/6.52 % 41.99/6.52 (first_last) % 41.99/6.52 ty(char) & ? [v0: uni] : (nil(char) = v0 & uni(v0) & ! [v1: char1] : ! [v2: % 41.99/6.52 list_char] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ (t2tb1(v1) = % 41.99/6.52 v3) | ~ (t2tb(v2) = v4) | ~ (cons(char, v3, v4) = v5) | ~ % 41.99/6.52 list_char(v2) | ~ char1(v1) | ? [v6: list_char] : ? [v7: int] : ? [v8: % 41.99/6.52 list_char] : ? [v9: char1] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 41.99/6.52 uni] : ? [v13: uni] : (infix_plpl(char, v10, v12) = v13 & t2tb1(v9) = % 41.99/6.52 v11 & tb2t(v13) = v6 & tb2t(v5) = v6 & t2tb(v8) = v10 & length2(char, % 41.99/6.52 v10) = v7 & length2(char, v4) = v7 & cons(char, v11, v0) = v12 & % 41.99/6.52 list_char(v8) & list_char(v6) & char1(v9) & uni(v13) & uni(v12) & % 41.99/6.52 uni(v11) & uni(v10)))) % 41.99/6.52 % 41.99/6.52 (first_last_explicit) % 41.99/6.53 ty(char) & ? [v0: uni] : (nil(char) = v0 & uni(v0) & ! [v1: list_char] : ! % 41.99/6.53 [v2: char1] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ (t2tb1(v2) = % 41.99/6.53 v3) | ~ (t2tb(v1) = v4) | ~ (cons(char, v3, v4) = v5) | ~ % 41.99/6.53 list_char(v1) | ~ char1(v2) | ? [v6: list_char] : ? [v7: uni] : ? [v8: % 41.99/6.53 char1] : ? [v9: uni] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 41.99/6.53 list_char] : (but_last1(v2, v1) = v6 & last_char1(v2, v1) = v8 & % 41.99/6.53 infix_plpl(char, v7, v10) = v11 & t2tb1(v8) = v9 & tb2t(v11) = v12 & % 41.99/6.53 tb2t(v5) = v12 & t2tb(v6) = v7 & cons(char, v9, v0) = v10 & % 41.99/6.53 list_char(v12) & list_char(v6) & char1(v8) & uni(v11) & uni(v10) & % 41.99/6.53 uni(v9) & uni(v7))) & ! [v1: list_char] : ! [v2: char1] : ! [v3: % 41.99/6.53 list_char] : ( ~ (but_last1(v2, v1) = v3) | ~ list_char(v1) | ~ % 41.99/6.53 char1(v2) | ? [v4: uni] : ? [v5: char1] : ? [v6: uni] : ? [v7: uni] : % 41.99/6.53 ? [v8: uni] : ? [v9: list_char] : ? [v10: uni] : ? [v11: uni] : ? % 41.99/6.53 [v12: uni] : (last_char1(v2, v1) = v5 & infix_plpl(char, v4, v7) = v8 & % 41.99/6.53 t2tb1(v5) = v6 & t2tb1(v2) = v10 & tb2t(v12) = v9 & tb2t(v8) = v9 & % 41.99/6.53 t2tb(v3) = v4 & t2tb(v1) = v11 & cons(char, v10, v11) = v12 & cons(char, % 41.99/6.53 v6, v0) = v7 & list_char(v9) & char1(v5) & uni(v12) & uni(v11) & % 41.99/6.53 uni(v10) & uni(v8) & uni(v7) & uni(v6) & uni(v4))) & ! [v1: list_char] % 41.99/6.53 : ! [v2: char1] : ! [v3: char1] : ( ~ (last_char1(v2, v1) = v3) | ~ % 41.99/6.53 list_char(v1) | ~ char1(v2) | ? [v4: list_char] : ? [v5: uni] : ? [v6: % 41.99/6.53 uni] : ? [v7: uni] : ? [v8: uni] : ? [v9: list_char] : ? [v10: uni] % 41.99/6.53 : ? [v11: uni] : ? [v12: uni] : (but_last1(v2, v1) = v4 & % 41.99/6.53 infix_plpl(char, v5, v7) = v8 & t2tb1(v3) = v6 & t2tb1(v2) = v10 & % 41.99/6.53 tb2t(v12) = v9 & tb2t(v8) = v9 & t2tb(v4) = v5 & t2tb(v1) = v11 & % 41.99/6.53 cons(char, v10, v11) = v12 & cons(char, v6, v0) = v7 & list_char(v9) & % 41.99/6.53 list_char(v4) & uni(v12) & uni(v11) & uni(v10) & uni(v8) & uni(v7) & % 41.99/6.53 uni(v6) & uni(v5)))) % 41.99/6.53 % 41.99/6.53 (last_char_def) % 41.99/6.53 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.99/6.53 & list_char(v1) & uni(v0) & ! [v2: char1] : ! [v3: char1] : ! [v4: % 41.99/6.53 list_char] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 41.99/6.53 list_char] : ! [v9: char1] : ( ~ (last_char1(v2, v8) = v9) | ~ % 41.99/6.53 (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ (t2tb(v4) = v6) | ~ % 41.99/6.53 (cons(char, v5, v6) = v7) | ~ list_char(v4) | ~ char1(v3) | ~ char1(v2) % 41.99/6.53 | (last_char1(v3, v4) = v9 & char1(v9))) & ! [v2: char1] : ! [v3: char1] % 41.99/6.54 : (v3 = v2 | ~ (last_char1(v2, v1) = v3) | ~ char1(v2))) % 41.99/6.54 % 41.99/6.54 (min_dist_eps) % 41.99/6.54 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.99/6.54 & list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: char1] : ! [v4: % 41.99/6.54 int] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: list_char] : ( % 41.99/6.54 ~ (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ (t2tb(v2) = v6) | ~ % 41.99/6.54 (cons(char, v5, v6) = v7) | ~ list_char(v2) | ~ char1(v3) | ~ % 41.99/6.54 min_dist1(v2, v1, v4) | min_dist1(v8, v1, $sum(v4, 1)))) % 41.99/6.54 % 41.99/6.54 (min_dist_eps_length) % 41.99/6.54 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.99/6.54 & list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: uni] : ( ~ % 41.99/6.54 (t2tb(v2) = v3) | ~ list_char(v2) | ? [v4: int] : (length2(char, v3) = % 41.99/6.54 v4 & min_dist1(v1, v2, v4)))) % 41.99/6.54 % 41.99/6.54 (select_eq) % 41.99/6.54 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 41.99/6.54 [v5: uni] : ! [v6: uni] : (v6 = v4 | ~ (set(v1, v0, v2, v3, v4) = v5) | ~ % 41.99/6.54 (get(v1, v0, v5, v3) = v6) | ~ ty(v1) | ~ ty(v0) | ~ uni(v4) | ~ uni(v3) % 41.99/6.54 | ~ uni(v2) | ~ sort1(v1, v4)) % 41.99/6.54 % 41.99/6.54 (select_neq) % 41.99/6.54 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 41.99/6.54 [v5: uni] : ! [v6: uni] : ! [v7: uni] : (v4 = v3 | ~ (set(v1, v0, v2, v3, % 41.99/6.54 v6) = v7) | ~ (get(v1, v0, v2, v4) = v5) | ~ ty(v1) | ~ ty(v0) | ~ % 41.99/6.54 uni(v6) | ~ uni(v4) | ~ uni(v3) | ~ uni(v2) | ~ sort1(v0, v4) | ~ % 41.99/6.54 sort1(v0, v3) | (get(v1, v0, v7, v4) = v5 & uni(v5))) % 41.99/6.54 % 41.99/6.54 (suffix_nil) % 41.99/6.54 ty(char) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 % 41.99/6.54 & list_char(v1) & uni(v0) & ! [v2: array_char] : ! [v3: uni] : ( ~ % 41.99/6.54 (t2tb3(v2) = v3) | ~ array_char(v2) | ? [v4: int] : (suffix1(v2, v4) = % 41.99/6.54 v1 & length3(char, v3) = v4))) % 41.99/6.54 % 41.99/6.54 (t2tb_sort8) % 41.99/6.55 ty(int) & ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | sort1(int, v1)) % 41.99/6.55 % 41.99/6.55 (wP_parameter_distance) % 41.99/6.55 ty(char) & ty(int) & ? [v0: ty] : ? [v1: uni] : ? [v2: int] : ? [v3: uni] % 41.99/6.55 : ? [v4: map_int_int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 41.99/6.55 uni] : ? [v9: uni] : ? [v10: map_int_int] : ? [v11: uni] : ? [v12: int] % 41.99/6.55 : ? [v13: uni] : ? [v14: uni] : ? [v15: int] : ( ~ ($sum(v15, v12) = v2) & % 41.99/6.55 $lesseq(v12, v5) & $lesseq(0, v12) & $lesseq(v5, v2) & tb2t5(v9) = v10 & % 41.99/6.55 t2tb5(v10) = v11 & t2tb5(v4) = v6 & tb2t2(v14) = v15 & t2tb2(v12) = v13 & % 41.99/6.55 t2tb2($difference(v2, v5)) = v8 & t2tb2(v5) = v7 & set(int, int, v6, v7, v8) % 41.99/6.55 = v9 & map(int, char) = v0 & get(int, int, v11, v13) = v14 & % 41.99/6.55 map_int_int(v10) & map_int_int(v4) & ty(v0) & uni(v14) & uni(v13) & uni(v11) % 41.99/6.55 & uni(v9) & uni(v8) & uni(v7) & uni(v6) & uni(v3) & uni(v1) & sort1(v0, v3) % 41.99/6.55 & sort1(v0, v1) & ! [v16: int] : ! [v17: uni] : ( ~ ($lesseq(1, % 41.99/6.55 $difference(v5, v16))) | ~ ($lesseq(0, v16)) | ~ (t2tb2(v16) = v17) % 41.99/6.55 | ? [v18: uni] : (tb2t2(v18) = $difference(v2, v16) & get(int, int, v6, % 41.99/6.55 v17) = v18 & uni(v18)))) % 41.99/6.55 % 41.99/6.55 (function-axioms) % 41.99/6.57 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 41.99/6.57 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 41.99/6.57 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 41.99/6.57 : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ % 41.99/6.57 (match_list1(v6, v5, v4, v3, v2) = v1) | ~ (match_list1(v6, v5, v4, v3, v2) % 41.99/6.57 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! % 41.99/6.57 [v4: uni] : ! [v5: ty] : (v1 = v0 | ~ (set2(v5, v4, v3, v2) = v1) | ~ % 41.99/6.57 (set2(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 41.99/6.57 ! [v3: uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = % 41.99/6.57 v1) | ~ (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 41.99/6.57 [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : (v1 = v0 | ~ % 41.99/6.57 (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, v2) = v0)) % 41.99/6.57 & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : % 41.99/6.57 (v1 = v0 | ~ (make1(v4, v3, v2) = v1) | ~ (make1(v4, v3, v2) = v0)) & ! % 41.99/6.57 [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] : (v1 = % 41.99/6.57 v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) & ! [v0: uni] % 41.99/6.57 : ! [v1: uni] : ! [v2: uni] : ! [v3: int] : ! [v4: ty] : (v1 = v0 | ~ % 41.99/6.57 (mk_array1(v4, v3, v2) = v1) | ~ (mk_array1(v4, v3, v2) = v0)) & ! [v0: % 41.99/6.57 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | % 41.99/6.57 ~ (const(v4, v3, v2) = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: uni] : % 41.99/6.57 ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ % 41.99/6.57 (infix_plpl(v4, v3, v2) = v1) | ~ (infix_plpl(v4, v3, v2) = v0)) & ! [v0: % 41.99/6.57 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | % 41.99/6.57 ~ (cons(v4, v3, v2) = v1) | ~ (cons(v4, v3, v2) = v0)) & ! [v0: % 41.99/6.57 list_char] : ! [v1: list_char] : ! [v2: int] : ! [v3: array_char] : (v1 = % 41.99/6.57 v0 | ~ (suffix1(v3, v2) = v1) | ~ (suffix1(v3, v2) = v0)) & ! [v0: uni] : % 41.99/6.57 ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (elts(v3, v2) = v1) % 41.99/6.57 | ~ (elts(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! % 41.99/6.57 [v3: ty] : (v1 = v0 | ~ (length3(v3, v2) = v1) | ~ (length3(v3, v2) = v0)) & % 41.99/6.57 ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, % 41.99/6.57 v2) = v1) | ~ (map(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 41.99/6.57 [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ % 41.99/6.57 (contents(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 41.99/6.57 [v3: ty] : (v1 = v0 | ~ (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & % 41.99/6.57 ! [v0: list_char] : ! [v1: list_char] : ! [v2: list_char] : ! [v3: char1] : % 41.99/6.57 (v1 = v0 | ~ (but_last1(v3, v2) = v1) | ~ (but_last1(v3, v2) = v0)) & ! % 41.99/6.57 [v0: char1] : ! [v1: char1] : ! [v2: list_char] : ! [v3: char1] : (v1 = v0 % 41.99/6.57 | ~ (last_char1(v3, v2) = v1) | ~ (last_char1(v3, v2) = v0)) & ! [v0: % 41.99/6.57 int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 41.99/6.57 (length2(v3, v2) = v1) | ~ (length2(v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 41.99/6.57 uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (cons_proj_21(v3, v2) = % 41.99/6.57 v1) | ~ (cons_proj_21(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 41.99/6.57 [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (cons_proj_11(v3, v2) = v1) | ~ % 41.99/6.57 (cons_proj_11(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : % 41.99/6.57 ! [v3: int] : (v1 = v0 | ~ (min1(v3, v2) = v1) | ~ (min1(v3, v2) = v0)) & ! % 41.99/6.57 [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ % 41.99/6.57 (max1(v3, v2) = v1) | ~ (max1(v3, v2) = v0)) & ! [v0: map_int_int] : ! % 41.99/6.57 [v1: map_int_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t5(v2) = v1) | ~ % 41.99/6.57 (tb2t5(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: map_int_int] : (v1 % 41.99/6.57 = v0 | ~ (t2tb5(v2) = v1) | ~ (t2tb5(v2) = v0)) & ! [v0: array_char] : ! % 41.99/6.57 [v1: array_char] : ! [v2: uni] : (v1 = v0 | ~ (tb2t3(v2) = v1) | ~ % 41.99/6.57 (tb2t3(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: array_char] : (v1 % 41.99/6.57 = v0 | ~ (t2tb3(v2) = v1) | ~ (t2tb3(v2) = v0)) & ! [v0: int] : ! [v1: % 41.99/6.57 int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) % 41.99/6.57 & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb2(v2) = v1) % 41.99/6.57 | ~ (t2tb2(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 % 41.99/6.57 | ~ (array(v2) = v1) | ~ (array(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : % 41.99/6.57 ! [v2: ty] : (v1 = v0 | ~ (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: % 41.99/6.57 char1] : ! [v1: char1] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ % 41.99/6.57 (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: char1] : (v1 = v0 % 41.99/6.57 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: list_char] : ! [v1: % 41.99/6.57 list_char] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = % 41.99/6.57 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: list_char] : (v1 = v0 | ~ % 41.99/6.57 (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: % 41.99/6.57 ty] : (v1 = v0 | ~ (list(v2) = v1) | ~ (list(v2) = v0)) & ! [v0: uni] : % 41.99/6.57 ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = v1) | ~ (nil(v2) = v0)) % 41.99/6.57 & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (witness1(v2) = % 41.99/6.57 v1) | ~ (witness1(v2) = v0)) % 41.99/6.57 % 41.99/6.57 Further assumptions not needed in the proof: % 41.99/6.57 -------------------------------------------- % 41.99/6.57 append_assoc, append_l_nil, append_length, array_inversion1, bool_inversion, % 41.99/6.57 bridgeL, bridgeL1, bridgeL3, bridgeL5, bridgeR, bridgeR1, bridgeR2, bridgeR3, % 41.99/6.57 compatOrderMult, cons_proj_1_def1, cons_proj_1_sort2, cons_proj_2_def1, % 41.99/6.57 cons_proj_2_sort2, cons_sort2, const, const_sort2, contents_def1, % 41.99/6.57 contents_sort2, dist_add_left, dist_add_right, dist_concat_left, % 41.99/6.57 dist_concat_right, dist_context, dist_symetry, elts_def1, elts_sort2, get_def, % 41.99/6.57 get_sort4, get_sort5, infix_plpl_def, infix_plpl_sort2, key_lemma_left, % 41.99/6.57 key_lemma_right, length_def, length_def2, length_nil, length_nonnegative, % 41.99/6.57 list_inversion1, make_def, make_sort2, match_bool_False, match_bool_True, % 41.99/6.57 match_bool_sort2, match_list_Cons1, match_list_Nil1, match_list_sort2, % 41.99/6.57 max_is_ge, max_is_some, max_sym, max_x, max_y, mem_append, mem_decomp, mem_def, % 41.99/6.57 min_dist_def, min_dist_diff, min_dist_equal, min_is_le, min_is_some, % 41.99/6.57 min_suffix_def, min_sym, min_x, min_y, mk_array_sort2, mk_ref_sort2, nil_Cons1, % 41.99/6.57 nil_sort2, ref_inversion1, set_def, set_sort4, set_sort5, suffix_cons, % 41.99/6.57 suffix_length, t2tb_sort10, t2tb_sort6, t2tb_sort7, t2tb_sort9, true_False, % 41.99/6.57 tuple0_inversion, witness_sort1 % 41.99/6.57 % 41.99/6.57 Those formulas are unsatisfiable: % 41.99/6.57 --------------------------------- % 41.99/6.57 % 41.99/6.57 Begin of proof % 41.99/6.57 | % 41.99/6.58 | ALPHA: (dist_eps) implies: % 41.99/6.58 | (1) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 41.99/6.58 | list_char(v1) & uni(v0) & dist1(v1, v1, 0)) % 41.99/6.58 | % 41.99/6.58 | ALPHA: (dist_inversion) implies: % 41.99/6.59 | (2) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 41.99/6.59 | list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: list_char] : % 41.99/6.59 | ! [v4: int] : (v4 = 0 | ~ list_char(v3) | ~ list_char(v2) | ~ % 41.99/6.59 | dist1(v2, v3, v4) | ? [v5: list_char] : ? [v6: list_char] : ? % 41.99/6.59 | [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: char1] : ? % 41.99/6.59 | [v11: uni] : ? [v12: uni] : ? [v13: list_char] : ? [v14: uni] : % 41.99/6.59 | ? [v15: list_char] : ? [v16: list_char] : ? [v17: list_char] : ? % 41.99/6.59 | [v18: int] : ? [v19: uni] : ? [v20: char1] : ? [v21: uni] : ? % 41.99/6.59 | [v22: uni] : ? [v23: list_char] : ? [v24: list_char] : ? [v25: % 41.99/6.59 | list_char] : ? [v26: int] : ? [v27: uni] : ? [v28: char1] : ? % 41.99/6.59 | [v29: uni] : ? [v30: uni] : ? [v31: list_char] : (list_char(v25) % 41.99/6.59 | & list_char(v24) & list_char(v17) & list_char(v16) & % 41.99/6.59 | list_char(v6) & list_char(v5) & char1(v28) & char1(v20) & % 41.99/6.59 | char1(v10) & ((v31 = v2 & $difference(v26, v4) = -1 & v25 = v3 & % 41.99/6.59 | t2tb1(v28) = v29 & tb2t(v30) = v2 & t2tb(v24) = v27 & % 41.99/6.59 | cons(char, v29, v27) = v30 & uni(v30) & uni(v29) & uni(v27) & % 41.99/6.59 | dist1(v24, v3, $sum(v4, -1))) | (v23 = v3 & $difference(v18, % 41.99/6.59 | v4) = -1 & v16 = v2 & t2tb1(v20) = v21 & tb2t(v22) = v3 & % 41.99/6.59 | t2tb(v17) = v19 & cons(char, v21, v19) = v22 & uni(v22) & % 41.99/6.59 | uni(v21) & uni(v19) & dist1(v2, v17, $sum(v4, -1))) | (v15 = % 41.99/6.59 | v3 & v13 = v2 & v7 = v4 & t2tb1(v10) = v11 & tb2t(v14) = v3 & % 41.99/6.59 | tb2t(v12) = v2 & t2tb(v6) = v9 & t2tb(v5) = v8 & cons(char, % 41.99/6.59 | v11, v9) = v14 & cons(char, v11, v8) = v12 & uni(v14) & % 41.99/6.59 | uni(v12) & uni(v11) & uni(v9) & uni(v8) & dist1(v5, v6, % 41.99/6.59 | v4))))) & ! [v2: list_char] : ! [v3: list_char] : ! [v4: % 41.99/6.59 | int] : (v3 = v1 | ~ list_char(v3) | ~ list_char(v2) | ~ % 41.99/6.59 | dist1(v2, v3, v4) | ? [v5: list_char] : ? [v6: list_char] : ? % 41.99/6.59 | [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: char1] : ? % 41.99/6.59 | [v11: uni] : ? [v12: uni] : ? [v13: list_char] : ? [v14: uni] : % 41.99/6.59 | ? [v15: list_char] : ? [v16: list_char] : ? [v17: list_char] : ? % 41.99/6.59 | [v18: int] : ? [v19: uni] : ? [v20: char1] : ? [v21: uni] : ? % 41.99/6.59 | [v22: uni] : ? [v23: list_char] : ? [v24: list_char] : ? [v25: % 41.99/6.59 | list_char] : ? [v26: int] : ? [v27: uni] : ? [v28: char1] : ? % 41.99/6.59 | [v29: uni] : ? [v30: uni] : ? [v31: list_char] : (list_char(v25) % 41.99/6.59 | & list_char(v24) & list_char(v17) & list_char(v16) & % 41.99/6.60 | list_char(v6) & list_char(v5) & char1(v28) & char1(v20) & % 41.99/6.60 | char1(v10) & ((v31 = v2 & $difference(v26, v4) = -1 & v25 = v3 & % 41.99/6.60 | t2tb1(v28) = v29 & tb2t(v30) = v2 & t2tb(v24) = v27 & % 41.99/6.60 | cons(char, v29, v27) = v30 & uni(v30) & uni(v29) & uni(v27) & % 41.99/6.60 | dist1(v24, v3, $sum(v4, -1))) | (v23 = v3 & $difference(v18, % 41.99/6.60 | v4) = -1 & v16 = v2 & t2tb1(v20) = v21 & tb2t(v22) = v3 & % 41.99/6.60 | t2tb(v17) = v19 & cons(char, v21, v19) = v22 & uni(v22) & % 41.99/6.60 | uni(v21) & uni(v19) & dist1(v2, v17, $sum(v4, -1))) | (v15 = % 41.99/6.60 | v3 & v13 = v2 & v7 = v4 & t2tb1(v10) = v11 & tb2t(v14) = v3 & % 41.99/6.60 | tb2t(v12) = v2 & t2tb(v6) = v9 & t2tb(v5) = v8 & cons(char, % 41.99/6.60 | v11, v9) = v14 & cons(char, v11, v8) = v12 & uni(v14) & % 41.99/6.60 | uni(v12) & uni(v11) & uni(v9) & uni(v8) & dist1(v5, v6, % 41.99/6.60 | v4))))) & ! [v2: list_char] : ! [v3: list_char] : ! [v4: % 41.99/6.60 | int] : (v2 = v1 | ~ list_char(v3) | ~ list_char(v2) | ~ % 41.99/6.60 | dist1(v2, v3, v4) | ? [v5: list_char] : ? [v6: list_char] : ? % 41.99/6.60 | [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: char1] : ? % 41.99/6.60 | [v11: uni] : ? [v12: uni] : ? [v13: list_char] : ? [v14: uni] : % 41.99/6.60 | ? [v15: list_char] : ? [v16: list_char] : ? [v17: list_char] : ? % 41.99/6.60 | [v18: int] : ? [v19: uni] : ? [v20: char1] : ? [v21: uni] : ? % 41.99/6.60 | [v22: uni] : ? [v23: list_char] : ? [v24: list_char] : ? [v25: % 41.99/6.60 | list_char] : ? [v26: int] : ? [v27: uni] : ? [v28: char1] : ? % 41.99/6.60 | [v29: uni] : ? [v30: uni] : ? [v31: list_char] : (list_char(v25) % 41.99/6.60 | & list_char(v24) & list_char(v17) & list_char(v16) & % 41.99/6.60 | list_char(v6) & list_char(v5) & char1(v28) & char1(v20) & % 41.99/6.60 | char1(v10) & ((v31 = v2 & $difference(v26, v4) = -1 & v25 = v3 & % 41.99/6.60 | t2tb1(v28) = v29 & tb2t(v30) = v2 & t2tb(v24) = v27 & % 41.99/6.60 | cons(char, v29, v27) = v30 & uni(v30) & uni(v29) & uni(v27) & % 41.99/6.60 | dist1(v24, v3, $sum(v4, -1))) | (v23 = v3 & $difference(v18, % 41.99/6.60 | v4) = -1 & v16 = v2 & t2tb1(v20) = v21 & tb2t(v22) = v3 & % 41.99/6.60 | t2tb(v17) = v19 & cons(char, v21, v19) = v22 & uni(v22) & % 41.99/6.60 | uni(v21) & uni(v19) & dist1(v2, v17, $sum(v4, -1))) | (v15 = % 41.99/6.60 | v3 & v13 = v2 & v7 = v4 & t2tb1(v10) = v11 & tb2t(v14) = v3 & % 41.99/6.60 | tb2t(v12) = v2 & t2tb(v6) = v9 & t2tb(v5) = v8 & cons(char, % 41.99/6.60 | v11, v9) = v14 & cons(char, v11, v8) = v12 & uni(v14) & % 41.99/6.60 | uni(v12) & uni(v11) & uni(v9) & uni(v8) & dist1(v5, v6, % 41.99/6.60 | v4)))))) % 41.99/6.60 | % 41.99/6.60 | ALPHA: (last_char_def) implies: % 41.99/6.60 | (3) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 41.99/6.60 | list_char(v1) & uni(v0) & ! [v2: char1] : ! [v3: char1] : ! [v4: % 41.99/6.60 | list_char] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 41.99/6.60 | list_char] : ! [v9: char1] : ( ~ (last_char1(v2, v8) = v9) | ~ % 41.99/6.60 | (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ (t2tb(v4) = v6) | ~ % 41.99/6.60 | (cons(char, v5, v6) = v7) | ~ list_char(v4) | ~ char1(v3) | ~ % 41.99/6.60 | char1(v2) | (last_char1(v3, v4) = v9 & char1(v9))) & ! [v2: char1] % 41.99/6.60 | : ! [v3: char1] : (v3 = v2 | ~ (last_char1(v2, v1) = v3) | ~ % 41.99/6.60 | char1(v2))) % 41.99/6.60 | % 41.99/6.60 | ALPHA: (but_last_def) implies: % 41.99/6.61 | (4) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 41.99/6.61 | list_char(v1) & uni(v0) & ! [v2: char1] : ! [v3: char1] : ! [v4: % 41.99/6.61 | list_char] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 41.99/6.61 | list_char] : ! [v9: list_char] : ( ~ (but_last1(v2, v8) = v9) | ~ % 41.99/6.61 | (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ (t2tb(v4) = v6) | ~ % 41.99/6.61 | (cons(char, v5, v6) = v7) | ~ list_char(v4) | ~ char1(v3) | ~ % 41.99/6.61 | char1(v2) | ? [v10: uni] : ? [v11: list_char] : ? [v12: uni] : % 41.99/6.61 | ? [v13: uni] : (but_last1(v3, v4) = v11 & t2tb1(v2) = v10 & % 41.99/6.61 | tb2t(v13) = v9 & t2tb(v11) = v12 & cons(char, v10, v12) = v13 & % 41.99/6.61 | list_char(v11) & list_char(v9) & uni(v13) & uni(v12) & uni(v10))) % 41.99/6.61 | & ! [v2: char1] : ! [v3: char1] : ! [v4: list_char] : ! [v5: uni] % 41.99/6.61 | : ! [v6: list_char] : ! [v7: uni] : ! [v8: uni] : ( ~ % 41.99/6.61 | (but_last1(v3, v4) = v6) | ~ (t2tb1(v2) = v5) | ~ (t2tb(v6) = v7) % 41.99/6.61 | | ~ (cons(char, v5, v7) = v8) | ~ list_char(v4) | ~ char1(v3) | % 41.99/6.61 | ~ char1(v2) | ? [v9: uni] : ? [v10: uni] : ? [v11: uni] : ? % 41.99/6.61 | [v12: list_char] : ? [v13: list_char] : (but_last1(v2, v12) = v13 % 41.99/6.61 | & t2tb1(v3) = v9 & tb2t(v11) = v12 & tb2t(v8) = v13 & t2tb(v4) = % 41.99/6.61 | v10 & cons(char, v9, v10) = v11 & list_char(v13) & list_char(v12) % 41.99/6.61 | & uni(v11) & uni(v10) & uni(v9))) & ! [v2: char1] : ! [v3: % 41.99/6.61 | list_char] : (v3 = v1 | ~ (but_last1(v2, v1) = v3) | ~ % 41.99/6.61 | char1(v2))) % 41.99/6.61 | % 41.99/6.61 | ALPHA: (first_last_explicit) implies: % 41.99/6.61 | (5) ? [v0: uni] : (nil(char) = v0 & uni(v0) & ! [v1: list_char] : ! [v2: % 41.99/6.61 | char1] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ % 41.99/6.61 | (t2tb1(v2) = v3) | ~ (t2tb(v1) = v4) | ~ (cons(char, v3, v4) = % 41.99/6.61 | v5) | ~ list_char(v1) | ~ char1(v2) | ? [v6: list_char] : ? % 41.99/6.61 | [v7: uni] : ? [v8: char1] : ? [v9: uni] : ? [v10: uni] : ? % 41.99/6.61 | [v11: uni] : ? [v12: list_char] : (but_last1(v2, v1) = v6 & % 41.99/6.61 | last_char1(v2, v1) = v8 & infix_plpl(char, v7, v10) = v11 & % 41.99/6.61 | t2tb1(v8) = v9 & tb2t(v11) = v12 & tb2t(v5) = v12 & t2tb(v6) = v7 % 41.99/6.61 | & cons(char, v9, v0) = v10 & list_char(v12) & list_char(v6) & % 41.99/6.61 | char1(v8) & uni(v11) & uni(v10) & uni(v9) & uni(v7))) & ! [v1: % 41.99/6.61 | list_char] : ! [v2: char1] : ! [v3: list_char] : ( ~ % 41.99/6.61 | (but_last1(v2, v1) = v3) | ~ list_char(v1) | ~ char1(v2) | ? % 41.99/6.61 | [v4: uni] : ? [v5: char1] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 41.99/6.61 | uni] : ? [v9: list_char] : ? [v10: uni] : ? [v11: uni] : ? % 41.99/6.61 | [v12: uni] : (last_char1(v2, v1) = v5 & infix_plpl(char, v4, v7) = % 41.99/6.61 | v8 & t2tb1(v5) = v6 & t2tb1(v2) = v10 & tb2t(v12) = v9 & tb2t(v8) % 41.99/6.61 | = v9 & t2tb(v3) = v4 & t2tb(v1) = v11 & cons(char, v10, v11) = % 41.99/6.61 | v12 & cons(char, v6, v0) = v7 & list_char(v9) & char1(v5) & % 41.99/6.61 | uni(v12) & uni(v11) & uni(v10) & uni(v8) & uni(v7) & uni(v6) & % 41.99/6.61 | uni(v4))) & ! [v1: list_char] : ! [v2: char1] : ! [v3: char1] % 41.99/6.61 | : ( ~ (last_char1(v2, v1) = v3) | ~ list_char(v1) | ~ char1(v2) | % 41.99/6.61 | ? [v4: list_char] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? % 41.99/6.62 | [v8: uni] : ? [v9: list_char] : ? [v10: uni] : ? [v11: uni] : ? % 41.99/6.62 | [v12: uni] : (but_last1(v2, v1) = v4 & infix_plpl(char, v5, v7) = % 41.99/6.62 | v8 & t2tb1(v3) = v6 & t2tb1(v2) = v10 & tb2t(v12) = v9 & tb2t(v8) % 41.99/6.62 | = v9 & t2tb(v4) = v5 & t2tb(v1) = v11 & cons(char, v10, v11) = % 42.24/6.62 | v12 & cons(char, v6, v0) = v7 & list_char(v9) & list_char(v4) & % 42.24/6.62 | uni(v12) & uni(v11) & uni(v10) & uni(v8) & uni(v7) & uni(v6) & % 42.24/6.62 | uni(v5)))) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (first_last) implies: % 42.24/6.62 | (6) ? [v0: uni] : (nil(char) = v0 & uni(v0) & ! [v1: char1] : ! [v2: % 42.24/6.62 | list_char] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ % 42.24/6.62 | (t2tb1(v1) = v3) | ~ (t2tb(v2) = v4) | ~ (cons(char, v3, v4) = % 42.24/6.62 | v5) | ~ list_char(v2) | ~ char1(v1) | ? [v6: list_char] : ? % 42.24/6.62 | [v7: int] : ? [v8: list_char] : ? [v9: char1] : ? [v10: uni] : % 42.24/6.62 | ? [v11: uni] : ? [v12: uni] : ? [v13: uni] : (infix_plpl(char, % 42.24/6.62 | v10, v12) = v13 & t2tb1(v9) = v11 & tb2t(v13) = v6 & tb2t(v5) = % 42.24/6.62 | v6 & t2tb(v8) = v10 & length2(char, v10) = v7 & length2(char, v4) % 42.24/6.62 | = v7 & cons(char, v11, v0) = v12 & list_char(v8) & list_char(v6) % 42.24/6.62 | & char1(v9) & uni(v13) & uni(v12) & uni(v11) & uni(v10)))) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (min_dist_eps) implies: % 42.24/6.62 | (7) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 42.24/6.62 | list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: char1] : ! % 42.24/6.62 | [v4: int] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 42.24/6.62 | list_char] : ( ~ (t2tb1(v3) = v5) | ~ (tb2t(v7) = v8) | ~ % 42.24/6.62 | (t2tb(v2) = v6) | ~ (cons(char, v5, v6) = v7) | ~ list_char(v2) | % 42.24/6.62 | ~ char1(v3) | ~ min_dist1(v2, v1, v4) | min_dist1(v8, v1, % 42.24/6.62 | $sum(v4, 1)))) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (min_dist_eps_length) implies: % 42.24/6.62 | (8) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 42.24/6.62 | list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: uni] : ( ~ % 42.24/6.62 | (t2tb(v2) = v3) | ~ list_char(v2) | ? [v4: int] : (length2(char, % 42.24/6.62 | v3) = v4 & min_dist1(v1, v2, v4)))) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (t2tb_sort8) implies: % 42.24/6.62 | (9) ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | sort1(int, v1)) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (suffix_nil) implies: % 42.24/6.62 | (10) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char) = v0 & % 42.24/6.62 | list_char(v1) & uni(v0) & ! [v2: array_char] : ! [v3: uni] : ( ~ % 42.24/6.62 | (t2tb3(v2) = v3) | ~ array_char(v2) | ? [v4: int] : (suffix1(v2, % 42.24/6.62 | v4) = v1 & length3(char, v3) = v4))) % 42.24/6.62 | % 42.24/6.62 | ALPHA: (wP_parameter_distance) implies: % 42.24/6.63 | (11) ty(int) % 42.24/6.63 | (12) ? [v0: ty] : ? [v1: uni] : ? [v2: int] : ? [v3: uni] : ? [v4: % 42.24/6.63 | map_int_int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 42.24/6.63 | uni] : ? [v9: uni] : ? [v10: map_int_int] : ? [v11: uni] : ? % 42.24/6.63 | [v12: int] : ? [v13: uni] : ? [v14: uni] : ? [v15: int] : ( ~ % 42.24/6.63 | ($sum(v15, v12) = v2) & $lesseq(v12, v5) & $lesseq(0, v12) & % 42.24/6.63 | $lesseq(v5, v2) & tb2t5(v9) = v10 & t2tb5(v10) = v11 & t2tb5(v4) = % 42.24/6.63 | v6 & tb2t2(v14) = v15 & t2tb2(v12) = v13 & t2tb2($difference(v2, % 42.24/6.63 | v5)) = v8 & t2tb2(v5) = v7 & set(int, int, v6, v7, v8) = v9 & % 42.24/6.63 | map(int, char) = v0 & get(int, int, v11, v13) = v14 & % 42.24/6.63 | map_int_int(v10) & map_int_int(v4) & ty(v0) & uni(v14) & uni(v13) & % 42.24/6.63 | uni(v11) & uni(v9) & uni(v8) & uni(v7) & uni(v6) & uni(v3) & uni(v1) % 42.24/6.63 | & sort1(v0, v3) & sort1(v0, v1) & ! [v16: int] : ! [v17: uni] : ( % 42.24/6.63 | ~ ($lesseq(1, $difference(v5, v16))) | ~ ($lesseq(0, v16)) | ~ % 42.24/6.63 | (t2tb2(v16) = v17) | ? [v18: uni] : (tb2t2(v18) = $difference(v2, % 42.24/6.63 | v16) & get(int, int, v6, v17) = v18 & uni(v18)))) % 42.24/6.63 | % 42.24/6.63 | ALPHA: (function-axioms) implies: % 42.24/6.63 | (13) ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = % 42.24/6.63 | v1) | ~ (nil(v2) = v0)) % 42.24/6.63 | (14) ! [v0: list_char] : ! [v1: list_char] : ! [v2: uni] : (v1 = v0 | ~ % 42.24/6.63 | (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 42.24/6.63 | (15) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb2(v2) % 42.24/6.63 | = v1) | ~ (t2tb2(v2) = v0)) % 42.24/6.63 | (16) ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) % 42.24/6.63 | = v1) | ~ (tb2t2(v2) = v0)) % 42.24/6.63 | (17) ! [v0: uni] : ! [v1: uni] : ! [v2: map_int_int] : (v1 = v0 | ~ % 42.24/6.63 | (t2tb5(v2) = v1) | ~ (t2tb5(v2) = v0)) % 42.24/6.63 | (18) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 42.24/6.63 | ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 42.24/6.63 | (get(v5, v4, v3, v2) = v0)) % 42.24/6.63 | % 42.24/6.63 | DELTA: instantiating (1) with fresh symbols all_115_0, all_115_1 gives: % 42.24/6.64 | (19) tb2t(all_115_1) = all_115_0 & nil(char) = all_115_1 & % 42.24/6.64 | list_char(all_115_0) & uni(all_115_1) & dist1(all_115_0, all_115_0, 0) % 42.24/6.64 | % 42.24/6.64 | ALPHA: (19) implies: % 42.24/6.64 | (20) nil(char) = all_115_1 % 42.24/6.64 | % 42.24/6.64 | DELTA: instantiating (8) with fresh symbols all_117_0, all_117_1 gives: % 42.24/6.64 | (21) tb2t(all_117_1) = all_117_0 & nil(char) = all_117_1 & % 42.24/6.64 | list_char(all_117_0) & uni(all_117_1) & ! [v0: list_char] : ! [v1: % 42.24/6.64 | uni] : ( ~ (t2tb(v0) = v1) | ~ list_char(v0) | ? [v2: int] : % 42.24/6.64 | (length2(char, v1) = v2 & min_dist1(all_117_0, v0, v2))) % 42.24/6.64 | % 42.24/6.64 | ALPHA: (21) implies: % 42.24/6.64 | (22) nil(char) = all_117_1 % 42.24/6.64 | (23) tb2t(all_117_1) = all_117_0 % 42.24/6.64 | % 42.24/6.64 | DELTA: instantiating (10) with fresh symbols all_120_0, all_120_1 gives: % 42.24/6.64 | (24) tb2t(all_120_1) = all_120_0 & nil(char) = all_120_1 & % 42.24/6.64 | list_char(all_120_0) & uni(all_120_1) & ! [v0: array_char] : ! [v1: % 42.24/6.64 | uni] : ( ~ (t2tb3(v0) = v1) | ~ array_char(v0) | ? [v2: int] : % 42.24/6.64 | (suffix1(v0, v2) = all_120_0 & length3(char, v1) = v2)) % 42.24/6.64 | % 42.24/6.64 | ALPHA: (24) implies: % 42.24/6.64 | (25) nil(char) = all_120_1 % 42.24/6.64 | (26) tb2t(all_120_1) = all_120_0 % 42.24/6.64 | % 42.24/6.64 | DELTA: instantiating (7) with fresh symbols all_123_0, all_123_1 gives: % 42.24/6.64 | (27) tb2t(all_123_1) = all_123_0 & nil(char) = all_123_1 & % 42.24/6.64 | list_char(all_123_0) & uni(all_123_1) & ! [v0: list_char] : ! [v1: % 42.24/6.64 | char1] : ! [v2: int] : ! [v3: uni] : ! [v4: uni] : ! [v5: uni] : % 42.24/6.64 | ! [v6: list_char] : ( ~ (t2tb1(v1) = v3) | ~ (tb2t(v5) = v6) | ~ % 42.24/6.64 | (t2tb(v0) = v4) | ~ (cons(char, v3, v4) = v5) | ~ list_char(v0) | % 42.24/6.64 | ~ char1(v1) | ~ min_dist1(v0, all_123_0, v2) | min_dist1(v6, % 42.24/6.64 | all_123_0, $sum(v2, 1))) % 42.24/6.64 | % 42.24/6.64 | ALPHA: (27) implies: % 42.24/6.64 | (28) nil(char) = all_123_1 % 42.24/6.64 | % 42.24/6.64 | DELTA: instantiating (3) with fresh symbols all_126_0, all_126_1 gives: % 42.24/6.64 | (29) tb2t(all_126_1) = all_126_0 & nil(char) = all_126_1 & % 42.24/6.64 | list_char(all_126_0) & uni(all_126_1) & ! [v0: char1] : ! [v1: % 42.24/6.64 | char1] : ! [v2: list_char] : ! [v3: uni] : ! [v4: uni] : ! [v5: % 42.24/6.64 | uni] : ! [v6: list_char] : ! [v7: char1] : ( ~ (last_char1(v0, v6) % 42.24/6.64 | = v7) | ~ (t2tb1(v1) = v3) | ~ (tb2t(v5) = v6) | ~ (t2tb(v2) = % 42.24/6.64 | v4) | ~ (cons(char, v3, v4) = v5) | ~ list_char(v2) | ~ % 42.24/6.64 | char1(v1) | ~ char1(v0) | (last_char1(v1, v2) = v7 & char1(v7))) & % 42.24/6.64 | ! [v0: char1] : ! [v1: char1] : (v1 = v0 | ~ (last_char1(v0, % 42.24/6.64 | all_126_0) = v1) | ~ char1(v0)) % 42.24/6.64 | % 42.24/6.64 | ALPHA: (29) implies: % 42.24/6.64 | (30) nil(char) = all_126_1 % 42.24/6.64 | % 42.24/6.64 | DELTA: instantiating (6) with fresh symbol all_129_0 gives: % 42.24/6.65 | (31) nil(char) = all_129_0 & uni(all_129_0) & ! [v0: char1] : ! [v1: % 42.24/6.65 | list_char] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ % 42.24/6.65 | (t2tb1(v0) = v2) | ~ (t2tb(v1) = v3) | ~ (cons(char, v2, v3) = v4) % 42.24/6.65 | | ~ list_char(v1) | ~ char1(v0) | ? [v5: list_char] : ? [v6: % 42.24/6.65 | int] : ? [v7: list_char] : ? [v8: char1] : ? [v9: uni] : ? % 42.24/6.65 | [v10: uni] : ? [v11: uni] : ? [v12: uni] : (infix_plpl(char, v9, % 42.24/6.65 | v11) = v12 & t2tb1(v8) = v10 & tb2t(v12) = v5 & tb2t(v4) = v5 & % 42.24/6.65 | t2tb(v7) = v9 & length2(char, v9) = v6 & length2(char, v3) = v6 & % 42.24/6.65 | cons(char, v10, all_129_0) = v11 & list_char(v7) & list_char(v5) & % 42.24/6.65 | char1(v8) & uni(v12) & uni(v11) & uni(v10) & uni(v9))) % 42.24/6.65 | % 42.24/6.65 | ALPHA: (31) implies: % 42.24/6.65 | (32) nil(char) = all_129_0 % 42.24/6.65 | % 42.24/6.65 | DELTA: instantiating (12) with fresh symbols all_132_0, all_132_1, all_132_2, % 42.24/6.65 | all_132_3, all_132_4, all_132_5, all_132_6, all_132_7, all_132_8, % 42.24/6.65 | all_132_9, all_132_10, all_132_11, all_132_12, all_132_13, all_132_14, % 42.24/6.65 | all_132_15 gives: % 42.24/6.65 | (33) ~ ($sum(all_132_0, all_132_3) = all_132_13) & $lesseq(all_132_3, % 42.24/6.65 | all_132_10) & $lesseq(0, all_132_3) & $lesseq(all_132_10, % 42.24/6.65 | all_132_13) & tb2t5(all_132_6) = all_132_5 & t2tb5(all_132_5) = % 42.24/6.65 | all_132_4 & t2tb5(all_132_11) = all_132_9 & tb2t2(all_132_1) = % 42.24/6.65 | all_132_0 & t2tb2(all_132_3) = all_132_2 & % 42.24/6.65 | t2tb2($difference(all_132_13, all_132_10)) = all_132_7 & % 42.24/6.65 | t2tb2(all_132_10) = all_132_8 & set(int, int, all_132_9, all_132_8, % 42.24/6.65 | all_132_7) = all_132_6 & map(int, char) = all_132_15 & get(int, int, % 42.24/6.65 | all_132_4, all_132_2) = all_132_1 & map_int_int(all_132_5) & % 42.24/6.65 | map_int_int(all_132_11) & ty(all_132_15) & uni(all_132_1) & % 42.24/6.65 | uni(all_132_2) & uni(all_132_4) & uni(all_132_6) & uni(all_132_7) & % 42.24/6.65 | uni(all_132_8) & uni(all_132_9) & uni(all_132_12) & uni(all_132_14) & % 42.24/6.65 | sort1(all_132_15, all_132_12) & sort1(all_132_15, all_132_14) & ! % 42.24/6.65 | [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_132_10, % 42.24/6.65 | v0))) | ~ ($lesseq(0, v0)) | ~ (t2tb2(v0) = v1) | ? [v2: % 42.24/6.65 | uni] : (tb2t2(v2) = $difference(all_132_13, v0) & get(int, int, % 42.24/6.65 | all_132_9, v1) = v2 & uni(v2))) % 42.24/6.65 | % 42.24/6.65 | ALPHA: (33) implies: % 42.24/6.65 | (34) ~ ($sum(all_132_0, all_132_3) = all_132_13) % 42.24/6.65 | (35) $lesseq(0, all_132_3) % 42.24/6.65 | (36) $lesseq(all_132_3, all_132_10) % 42.24/6.65 | (37) uni(all_132_9) % 42.24/6.65 | (38) uni(all_132_8) % 42.24/6.65 | (39) uni(all_132_7) % 42.24/6.65 | (40) uni(all_132_6) % 42.24/6.65 | (41) uni(all_132_2) % 42.24/6.65 | (42) get(int, int, all_132_4, all_132_2) = all_132_1 % 42.24/6.65 | (43) set(int, int, all_132_9, all_132_8, all_132_7) = all_132_6 % 42.24/6.65 | (44) t2tb2(all_132_10) = all_132_8 % 42.24/6.65 | (45) t2tb2($difference(all_132_13, all_132_10)) = all_132_7 % 42.24/6.65 | (46) t2tb2(all_132_3) = all_132_2 % 42.24/6.65 | (47) tb2t2(all_132_1) = all_132_0 % 42.24/6.65 | (48) t2tb5(all_132_5) = all_132_4 % 42.24/6.65 | (49) tb2t5(all_132_6) = all_132_5 % 42.24/6.65 | (50) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_132_10, % 42.24/6.65 | v0))) | ~ ($lesseq(0, v0)) | ~ (t2tb2(v0) = v1) | ? [v2: % 42.24/6.65 | uni] : (tb2t2(v2) = $difference(all_132_13, v0) & get(int, int, % 42.24/6.65 | all_132_9, v1) = v2 & uni(v2))) % 42.24/6.65 | % 42.24/6.65 | DELTA: instantiating (4) with fresh symbols all_136_0, all_136_1 gives: % 42.24/6.65 | (51) tb2t(all_136_1) = all_136_0 & nil(char) = all_136_1 & % 42.24/6.65 | list_char(all_136_0) & uni(all_136_1) & ! [v0: char1] : ! [v1: % 42.24/6.65 | char1] : ! [v2: list_char] : ! [v3: uni] : ! [v4: uni] : ! [v5: % 42.24/6.65 | uni] : ! [v6: list_char] : ! [v7: list_char] : ( ~ (but_last1(v0, % 42.24/6.65 | v6) = v7) | ~ (t2tb1(v1) = v3) | ~ (tb2t(v5) = v6) | ~ % 42.24/6.65 | (t2tb(v2) = v4) | ~ (cons(char, v3, v4) = v5) | ~ list_char(v2) | % 42.24/6.65 | ~ char1(v1) | ~ char1(v0) | ? [v8: uni] : ? [v9: list_char] : ? % 42.24/6.65 | [v10: uni] : ? [v11: uni] : (but_last1(v1, v2) = v9 & t2tb1(v0) = % 42.24/6.65 | v8 & tb2t(v11) = v7 & t2tb(v9) = v10 & cons(char, v8, v10) = v11 & % 42.24/6.65 | list_char(v9) & list_char(v7) & uni(v11) & uni(v10) & uni(v8))) & % 42.24/6.65 | ! [v0: char1] : ! [v1: char1] : ! [v2: list_char] : ! [v3: uni] : % 42.24/6.65 | ! [v4: list_char] : ! [v5: uni] : ! [v6: uni] : ( ~ (but_last1(v1, % 42.24/6.65 | v2) = v4) | ~ (t2tb1(v0) = v3) | ~ (t2tb(v4) = v5) | ~ % 42.24/6.65 | (cons(char, v3, v5) = v6) | ~ list_char(v2) | ~ char1(v1) | ~ % 42.24/6.65 | char1(v0) | ? [v7: uni] : ? [v8: uni] : ? [v9: uni] : ? [v10: % 42.24/6.65 | list_char] : ? [v11: list_char] : (but_last1(v0, v10) = v11 & % 42.24/6.65 | t2tb1(v1) = v7 & tb2t(v9) = v10 & tb2t(v6) = v11 & t2tb(v2) = v8 & % 42.24/6.65 | cons(char, v7, v8) = v9 & list_char(v11) & list_char(v10) & % 42.24/6.65 | uni(v9) & uni(v8) & uni(v7))) & ! [v0: char1] : ! [v1: int] : % 42.24/6.65 | (v1 = all_136_0 | ~ (but_last1(v0, all_136_0) = v1) | ~ char1(v0)) % 42.24/6.65 | % 42.24/6.66 | ALPHA: (51) implies: % 42.24/6.66 | (52) nil(char) = all_136_1 % 42.24/6.66 | % 42.24/6.66 | DELTA: instantiating (5) with fresh symbol all_139_0 gives: % 42.24/6.66 | (53) nil(char) = all_139_0 & uni(all_139_0) & ! [v0: list_char] : ! [v1: % 42.24/6.66 | char1] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ( ~ (t2tb1(v1) % 42.24/6.66 | = v2) | ~ (t2tb(v0) = v3) | ~ (cons(char, v2, v3) = v4) | ~ % 42.24/6.66 | list_char(v0) | ~ char1(v1) | ? [v5: list_char] : ? [v6: uni] : % 42.24/6.66 | ? [v7: char1] : ? [v8: uni] : ? [v9: uni] : ? [v10: uni] : ? % 42.24/6.66 | [v11: list_char] : (but_last1(v1, v0) = v5 & last_char1(v1, v0) = v7 % 42.24/6.66 | & infix_plpl(char, v6, v9) = v10 & t2tb1(v7) = v8 & tb2t(v10) = % 42.24/6.66 | v11 & tb2t(v4) = v11 & t2tb(v5) = v6 & cons(char, v8, all_139_0) = % 42.24/6.66 | v9 & list_char(v11) & list_char(v5) & char1(v7) & uni(v10) & % 42.24/6.66 | uni(v9) & uni(v8) & uni(v6))) & ! [v0: list_char] : ! [v1: % 42.24/6.66 | char1] : ! [v2: list_char] : ( ~ (but_last1(v1, v0) = v2) | ~ % 42.24/6.66 | list_char(v0) | ~ char1(v1) | ? [v3: uni] : ? [v4: char1] : ? % 42.24/6.66 | [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? [v8: list_char] : ? % 42.24/6.66 | [v9: uni] : ? [v10: uni] : ? [v11: uni] : (last_char1(v1, v0) = v4 % 42.24/6.66 | & infix_plpl(char, v3, v6) = v7 & t2tb1(v4) = v5 & t2tb1(v1) = v9 % 42.24/6.66 | & tb2t(v11) = v8 & tb2t(v7) = v8 & t2tb(v2) = v3 & t2tb(v0) = v10 % 42.24/6.66 | & cons(char, v9, v10) = v11 & cons(char, v5, all_139_0) = v6 & % 42.24/6.66 | list_char(v8) & char1(v4) & uni(v11) & uni(v10) & uni(v9) & % 42.24/6.66 | uni(v7) & uni(v6) & uni(v5) & uni(v3))) & ! [v0: list_char] : ! % 42.24/6.66 | [v1: char1] : ! [v2: char1] : ( ~ (last_char1(v1, v0) = v2) | ~ % 42.24/6.66 | list_char(v0) | ~ char1(v1) | ? [v3: list_char] : ? [v4: uni] : % 42.24/6.66 | ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? [v8: list_char] : ? % 42.24/6.66 | [v9: uni] : ? [v10: uni] : ? [v11: uni] : (but_last1(v1, v0) = v3 % 42.24/6.66 | & infix_plpl(char, v4, v6) = v7 & t2tb1(v2) = v5 & t2tb1(v1) = v9 % 42.24/6.66 | & tb2t(v11) = v8 & tb2t(v7) = v8 & t2tb(v3) = v4 & t2tb(v0) = v10 % 42.24/6.66 | & cons(char, v9, v10) = v11 & cons(char, v5, all_139_0) = v6 & % 42.24/6.66 | list_char(v8) & list_char(v3) & uni(v11) & uni(v10) & uni(v9) & % 42.24/6.66 | uni(v7) & uni(v6) & uni(v5) & uni(v4))) % 42.24/6.66 | % 42.24/6.66 | ALPHA: (53) implies: % 42.24/6.66 | (54) nil(char) = all_139_0 % 42.24/6.66 | % 42.24/6.66 | DELTA: instantiating (2) with fresh symbols all_142_0, all_142_1 gives: % 42.24/6.67 | (55) tb2t(all_142_1) = all_142_0 & nil(char) = all_142_1 & % 42.24/6.67 | list_char(all_142_0) & uni(all_142_1) & ! [v0: list_char] : ! [v1: % 42.24/6.67 | list_char] : ! [v2: int] : (v2 = 0 | ~ list_char(v1) | ~ % 42.24/6.67 | list_char(v0) | ~ dist1(v0, v1, v2) | ? [v3: list_char] : ? [v4: % 42.24/6.67 | list_char] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? [v8: % 42.24/6.67 | char1] : ? [v9: uni] : ? [v10: uni] : ? [v11: list_char] : ? % 42.24/6.67 | [v12: uni] : ? [v13: list_char] : ? [v14: list_char] : ? [v15: % 42.24/6.67 | list_char] : ? [v16: int] : ? [v17: uni] : ? [v18: char1] : ? % 42.24/6.67 | [v19: uni] : ? [v20: uni] : ? [v21: list_char] : ? [v22: % 42.24/6.67 | list_char] : ? [v23: list_char] : ? [v24: int] : ? [v25: uni] : % 42.24/6.67 | ? [v26: char1] : ? [v27: uni] : ? [v28: uni] : ? [v29: % 42.24/6.67 | list_char] : (list_char(v23) & list_char(v22) & list_char(v15) & % 42.24/6.67 | list_char(v14) & list_char(v4) & list_char(v3) & char1(v26) & % 42.24/6.67 | char1(v18) & char1(v8) & ((v29 = v0 & $difference(v24, v2) = -1 & % 42.24/6.67 | v23 = v1 & t2tb1(v26) = v27 & tb2t(v28) = v0 & t2tb(v22) = v25 % 42.24/6.67 | & cons(char, v27, v25) = v28 & uni(v28) & uni(v27) & uni(v25) % 42.24/6.67 | & dist1(v22, v1, $sum(v2, -1))) | (v21 = v1 & $difference(v16, % 42.24/6.67 | v2) = -1 & v14 = v0 & t2tb1(v18) = v19 & tb2t(v20) = v1 & % 42.24/6.67 | t2tb(v15) = v17 & cons(char, v19, v17) = v20 & uni(v20) & % 42.24/6.67 | uni(v19) & uni(v17) & dist1(v0, v15, $sum(v2, -1))) | (v13 = % 42.24/6.67 | v1 & v11 = v0 & v5 = v2 & t2tb1(v8) = v9 & tb2t(v12) = v1 & % 42.24/6.67 | tb2t(v10) = v0 & t2tb(v4) = v7 & t2tb(v3) = v6 & cons(char, % 42.24/6.67 | v9, v7) = v12 & cons(char, v9, v6) = v10 & uni(v12) & % 42.24/6.67 | uni(v10) & uni(v9) & uni(v7) & uni(v6) & dist1(v3, v4, v2))))) % 42.24/6.67 | & ! [v0: list_char] : ! [v1: any] : ! [v2: int] : (v1 = all_142_0 | % 42.24/6.67 | ~ list_char(v1) | ~ list_char(v0) | ~ dist1(v0, v1, v2) | ? [v3: % 42.24/6.67 | list_char] : ? [v4: list_char] : ? [v5: int] : ? [v6: uni] : ? % 42.24/6.67 | [v7: uni] : ? [v8: char1] : ? [v9: uni] : ? [v10: uni] : ? [v11: % 42.24/6.67 | list_char] : ? [v12: uni] : ? [v13: any] : ? [v14: list_char] : % 42.24/6.67 | ? [v15: list_char] : ? [v16: int] : ? [v17: uni] : ? [v18: % 42.24/6.67 | char1] : ? [v19: uni] : ? [v20: uni] : ? [v21: any] : ? [v22: % 42.24/6.67 | list_char] : ? [v23: list_char] : ? [v24: int] : ? [v25: uni] : % 42.24/6.67 | ? [v26: char1] : ? [v27: uni] : ? [v28: uni] : ? [v29: % 42.24/6.67 | list_char] : (list_char(v23) & list_char(v22) & list_char(v15) & % 42.24/6.67 | list_char(v14) & list_char(v4) & list_char(v3) & char1(v26) & % 42.24/6.67 | char1(v18) & char1(v8) & ((v29 = v0 & $difference(v24, v2) = -1 & % 42.24/6.67 | v23 = v1 & t2tb1(v26) = v27 & tb2t(v28) = v0 & t2tb(v22) = v25 % 42.24/6.67 | & cons(char, v27, v25) = v28 & uni(v28) & uni(v27) & uni(v25) % 42.24/6.67 | & dist1(v22, v1, $sum(v2, -1))) | (v21 = v1 & $difference(v16, % 42.24/6.67 | v2) = -1 & v14 = v0 & t2tb1(v18) = v19 & tb2t(v20) = v1 & % 42.24/6.67 | t2tb(v15) = v17 & cons(char, v19, v17) = v20 & uni(v20) & % 42.24/6.67 | uni(v19) & uni(v17) & dist1(v0, v15, $sum(v2, -1))) | (v13 = % 42.24/6.67 | v1 & v11 = v0 & v5 = v2 & t2tb1(v8) = v9 & tb2t(v12) = v1 & % 42.24/6.67 | tb2t(v10) = v0 & t2tb(v4) = v7 & t2tb(v3) = v6 & cons(char, % 42.24/6.67 | v9, v7) = v12 & cons(char, v9, v6) = v10 & uni(v12) & % 42.24/6.67 | uni(v10) & uni(v9) & uni(v7) & uni(v6) & dist1(v3, v4, v2))))) % 42.24/6.67 | & ! [v0: any] : ! [v1: list_char] : ! [v2: int] : (v0 = all_142_0 | % 42.24/6.67 | ~ list_char(v1) | ~ list_char(v0) | ~ dist1(v0, v1, v2) | ? [v3: % 42.24/6.67 | list_char] : ? [v4: list_char] : ? [v5: int] : ? [v6: uni] : ? % 42.24/6.67 | [v7: uni] : ? [v8: char1] : ? [v9: uni] : ? [v10: uni] : ? [v11: % 42.24/6.67 | any] : ? [v12: uni] : ? [v13: list_char] : ? [v14: list_char] : % 42.24/6.67 | ? [v15: list_char] : ? [v16: int] : ? [v17: uni] : ? [v18: % 42.24/6.67 | char1] : ? [v19: uni] : ? [v20: uni] : ? [v21: list_char] : ? % 42.24/6.67 | [v22: list_char] : ? [v23: list_char] : ? [v24: int] : ? [v25: % 42.24/6.67 | uni] : ? [v26: char1] : ? [v27: uni] : ? [v28: uni] : ? [v29: % 42.24/6.67 | any] : (list_char(v23) & list_char(v22) & list_char(v15) & % 42.24/6.67 | list_char(v14) & list_char(v4) & list_char(v3) & char1(v26) & % 42.24/6.67 | char1(v18) & char1(v8) & ((v29 = v0 & $difference(v24, v2) = -1 & % 42.24/6.67 | v23 = v1 & t2tb1(v26) = v27 & tb2t(v28) = v0 & t2tb(v22) = v25 % 42.24/6.67 | & cons(char, v27, v25) = v28 & uni(v28) & uni(v27) & uni(v25) % 42.24/6.67 | & dist1(v22, v1, $sum(v2, -1))) | (v21 = v1 & $difference(v16, % 42.24/6.67 | v2) = -1 & v14 = v0 & t2tb1(v18) = v19 & tb2t(v20) = v1 & % 42.24/6.67 | t2tb(v15) = v17 & cons(char, v19, v17) = v20 & uni(v20) & % 42.24/6.67 | uni(v19) & uni(v17) & dist1(v0, v15, $sum(v2, -1))) | (v13 = % 42.24/6.67 | v1 & v11 = v0 & v5 = v2 & t2tb1(v8) = v9 & tb2t(v12) = v1 & % 42.24/6.67 | tb2t(v10) = v0 & t2tb(v4) = v7 & t2tb(v3) = v6 & cons(char, % 42.24/6.67 | v9, v7) = v12 & cons(char, v9, v6) = v10 & uni(v12) & % 42.24/6.67 | uni(v10) & uni(v9) & uni(v7) & uni(v6) & dist1(v3, v4, v2))))) % 42.24/6.67 | % 42.24/6.67 | ALPHA: (55) implies: % 42.24/6.67 | (56) nil(char) = all_142_1 % 42.24/6.67 | (57) tb2t(all_142_1) = all_142_0 % 42.24/6.67 | % 42.24/6.67 | GROUND_INST: instantiating (13) with all_117_1, all_120_1, char, simplifying % 42.24/6.67 | with (22), (25) gives: % 42.24/6.67 | (58) all_120_1 = all_117_1 % 42.24/6.67 | % 42.24/6.67 | GROUND_INST: instantiating (13) with all_120_1, all_126_1, char, simplifying % 42.24/6.67 | with (25), (30) gives: % 42.24/6.67 | (59) all_126_1 = all_120_1 % 42.24/6.67 | % 42.24/6.67 | GROUND_INST: instantiating (13) with all_129_0, all_136_1, char, simplifying % 42.24/6.67 | with (32), (52) gives: % 42.24/6.67 | (60) all_136_1 = all_129_0 % 42.24/6.67 | % 42.24/6.68 | GROUND_INST: instantiating (13) with all_126_1, all_136_1, char, simplifying % 42.24/6.68 | with (30), (52) gives: % 42.24/6.68 | (61) all_136_1 = all_126_1 % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (13) with all_136_1, all_139_0, char, simplifying % 42.24/6.68 | with (52), (54) gives: % 42.24/6.68 | (62) all_139_0 = all_136_1 % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (13) with all_123_1, all_139_0, char, simplifying % 42.24/6.68 | with (28), (54) gives: % 42.24/6.68 | (63) all_139_0 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (13) with all_126_1, all_142_1, char, simplifying % 42.24/6.68 | with (30), (56) gives: % 42.24/6.68 | (64) all_142_1 = all_126_1 % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (13) with all_115_1, all_142_1, char, simplifying % 42.24/6.68 | with (20), (56) gives: % 42.24/6.68 | (65) all_142_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (14) with all_120_0, all_142_0, all_120_1, % 42.24/6.68 | simplifying with (26) gives: % 42.24/6.68 | (66) all_142_0 = all_120_0 | ~ (tb2t(all_120_1) = all_142_0) % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (14) with all_117_0, all_142_0, all_117_1, % 42.24/6.68 | simplifying with (23) gives: % 42.24/6.68 | (67) all_142_0 = all_117_0 | ~ (tb2t(all_117_1) = all_142_0) % 42.24/6.68 | % 42.24/6.68 | GROUND_INST: instantiating (15) with all_132_8, all_132_2, all_132_10, % 42.24/6.68 | simplifying with (44) gives: % 42.24/6.68 | (68) all_132_2 = all_132_8 | ~ (t2tb2(all_132_10) = all_132_2) % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (64), (65) imply: % 42.24/6.68 | (69) all_126_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | SIMP: (69) implies: % 42.24/6.68 | (70) all_126_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (62), (63) imply: % 42.24/6.68 | (71) all_136_1 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | SIMP: (71) implies: % 42.24/6.68 | (72) all_136_1 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (60), (61) imply: % 42.24/6.68 | (73) all_129_0 = all_126_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (60), (72) imply: % 42.24/6.68 | (74) all_129_0 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (73), (74) imply: % 42.24/6.68 | (75) all_126_1 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | SIMP: (75) implies: % 42.24/6.68 | (76) all_126_1 = all_123_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (70), (76) imply: % 42.24/6.68 | (77) all_123_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (59), (76) imply: % 42.24/6.68 | (78) all_123_1 = all_120_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (77), (78) imply: % 42.24/6.68 | (79) all_120_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | SIMP: (79) implies: % 42.24/6.68 | (80) all_120_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | COMBINE_EQS: (58), (80) imply: % 42.24/6.68 | (81) all_117_1 = all_115_1 % 42.24/6.68 | % 42.24/6.68 | REDUCE: (57), (65) imply: % 42.24/6.68 | (82) tb2t(all_115_1) = all_142_0 % 42.24/6.68 | % 42.24/6.68 | BETA: splitting (67) gives: % 42.24/6.68 | % 42.24/6.68 | Case 1: % 42.24/6.68 | | % 42.24/6.68 | | (83) ~ (tb2t(all_117_1) = all_142_0) % 42.24/6.68 | | % 42.24/6.68 | | REDUCE: (81), (83) imply: % 42.24/6.68 | | (84) ~ (tb2t(all_115_1) = all_142_0) % 42.24/6.68 | | % 42.24/6.68 | | PRED_UNIFY: (82), (84) imply: % 42.24/6.68 | | (85) $false % 42.24/6.68 | | % 42.24/6.68 | | CLOSE: (85) is inconsistent. % 42.24/6.68 | | % 42.24/6.68 | Case 2: % 42.24/6.68 | | % 42.24/6.68 | | (86) all_142_0 = all_117_0 % 42.24/6.68 | | % 42.24/6.68 | | REDUCE: (82), (86) imply: % 42.24/6.69 | | (87) tb2t(all_115_1) = all_117_0 % 42.24/6.69 | | % 42.24/6.69 | | BETA: splitting (66) gives: % 42.24/6.69 | | % 42.24/6.69 | | Case 1: % 42.24/6.69 | | | % 42.24/6.69 | | | (88) ~ (tb2t(all_120_1) = all_142_0) % 42.24/6.69 | | | % 42.24/6.69 | | | REDUCE: (80), (86), (88) imply: % 42.24/6.69 | | | (89) ~ (tb2t(all_115_1) = all_117_0) % 42.24/6.69 | | | % 42.24/6.69 | | | PRED_UNIFY: (87), (89) imply: % 42.24/6.69 | | | (90) $false % 42.24/6.69 | | | % 42.24/6.69 | | | CLOSE: (90) is inconsistent. % 42.24/6.69 | | | % 42.24/6.69 | | Case 2: % 42.24/6.69 | | | % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (bridgeL2) with all_132_10, all_132_8, % 42.24/6.69 | | | simplifying with (44) gives: % 42.24/6.69 | | | (91) tb2t2(all_132_8) = all_132_10 % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (9) with all_132_10, all_132_8, simplifying % 42.24/6.69 | | | with (44) gives: % 42.24/6.69 | | | (92) sort1(int, all_132_8) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (bridgeL2) with $difference(all_132_13, % 42.24/6.69 | | | all_132_10), all_132_7, simplifying with (45) gives: % 42.24/6.69 | | | (93) tb2t2(all_132_7) = $difference(all_132_13, all_132_10) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (9) with $difference(all_132_13, all_132_10), % 42.24/6.69 | | | all_132_7, simplifying with (45) gives: % 42.24/6.69 | | | (94) sort1(int, all_132_7) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (50) with all_132_3, all_132_2, simplifying % 42.24/6.69 | | | with (46) gives: % 42.24/6.69 | | | (95) ~ ($lesseq(1, $difference(all_132_10, all_132_3))) | ~ % 42.24/6.69 | | | ($lesseq(0, all_132_3)) | ? [v0: uni] : (tb2t2(v0) = % 42.24/6.69 | | | $difference(all_132_13, all_132_3) & get(int, int, all_132_9, % 42.24/6.69 | | | all_132_2) = v0 & uni(v0)) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (bridgeL2) with all_132_3, all_132_2, % 42.24/6.69 | | | simplifying with (46) gives: % 42.24/6.69 | | | (96) tb2t2(all_132_2) = all_132_3 % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (9) with all_132_3, all_132_2, simplifying with % 42.24/6.69 | | | (46) gives: % 42.24/6.69 | | | (97) sort1(int, all_132_2) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (bridgeR5) with all_132_6, all_132_5, % 42.24/6.69 | | | simplifying with (40), (49) gives: % 42.24/6.69 | | | (98) t2tb5(all_132_5) = all_132_6 % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (16) with all_132_0, $difference(all_132_13, % 42.24/6.69 | | | all_132_10), all_132_7, simplifying with (93) gives: % 42.24/6.69 | | | (99) $sum(all_132_0, all_132_10) = all_132_13 | ~ (tb2t2(all_132_7) = % 42.24/6.69 | | | all_132_0) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (16) with all_132_10, all_132_3, all_132_8, % 42.24/6.69 | | | simplifying with (91) gives: % 42.24/6.69 | | | (100) all_132_3 = all_132_10 | ~ (tb2t2(all_132_8) = all_132_3) % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (17) with all_132_4, all_132_6, all_132_5, % 42.24/6.69 | | | simplifying with (48), (98) gives: % 42.24/6.69 | | | (101) all_132_4 = all_132_6 % 42.24/6.69 | | | % 42.24/6.69 | | | REDUCE: (42), (101) imply: % 42.24/6.69 | | | (102) get(int, int, all_132_6, all_132_2) = all_132_1 % 42.24/6.69 | | | % 42.24/6.69 | | | GROUND_INST: instantiating (select_eq) with int, int, all_132_9, % 42.24/6.69 | | | all_132_8, all_132_7, all_132_6, all_132_1, simplifying with % 42.24/6.69 | | | (11), (37), (38), (39), (43), (94) gives: % 42.24/6.69 | | | (103) all_132_1 = all_132_7 | ~ (get(int, int, all_132_6, all_132_8) = % 42.24/6.69 | | | all_132_1) % 42.24/6.69 | | | % 42.24/6.69 | | | BETA: splitting (68) gives: % 42.24/6.69 | | | % 42.24/6.69 | | | Case 1: % 42.24/6.69 | | | | % 42.24/6.69 | | | | (104) ~ (t2tb2(all_132_10) = all_132_2) % 42.24/6.69 | | | | % 42.24/6.69 | | | | PRED_UNIFY: (46), (104) imply: % 42.24/6.69 | | | | (105) ~ (all_132_3 = all_132_10) % 42.24/6.69 | | | | % 42.24/6.69 | | | | PRED_UNIFY: (44), (104) imply: % 42.24/6.69 | | | | (106) ~ (all_132_2 = all_132_8) % 42.24/6.69 | | | | % 42.24/6.69 | | | | STRENGTHEN: (36), (105) imply: % 42.24/6.69 | | | | (107) $lesseq(1, $difference(all_132_10, all_132_3)) % 42.24/6.69 | | | | % 42.24/6.69 | | | | BETA: splitting (95) gives: % 42.24/6.69 | | | | % 42.24/6.69 | | | | Case 1: % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | (108) $lesseq(all_132_3, -1) % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | COMBINE_INEQS: (35), (108) imply: % 42.24/6.69 | | | | | (109) $false % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | CLOSE: (109) is inconsistent. % 42.24/6.69 | | | | | % 42.24/6.69 | | | | Case 2: % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | (110) ~ ($lesseq(1, $difference(all_132_10, all_132_3))) | ? [v0: % 42.24/6.69 | | | | | uni] : (tb2t2(v0) = $difference(all_132_13, all_132_3) & % 42.24/6.69 | | | | | get(int, int, all_132_9, all_132_2) = v0 & uni(v0)) % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | BETA: splitting (110) gives: % 42.24/6.69 | | | | | % 42.24/6.69 | | | | | Case 1: % 42.24/6.69 | | | | | | % 42.24/6.69 | | | | | | (111) $lesseq(all_132_10, all_132_3) % 42.24/6.69 | | | | | | % 42.24/6.69 | | | | | | COMBINE_INEQS: (107), (111) imply: % 42.24/6.69 | | | | | | (112) $false % 42.24/6.69 | | | | | | % 42.24/6.69 | | | | | | CLOSE: (112) is inconsistent. % 42.24/6.69 | | | | | | % 42.24/6.70 | | | | | Case 2: % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | (113) ? [v0: uni] : (tb2t2(v0) = $difference(all_132_13, % 42.24/6.70 | | | | | | all_132_3) & get(int, int, all_132_9, all_132_2) = v0 & % 42.24/6.70 | | | | | | uni(v0)) % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | DELTA: instantiating (113) with fresh symbol all_356_0 gives: % 42.24/6.70 | | | | | | (114) tb2t2(all_356_0) = $difference(all_132_13, all_132_3) & % 42.24/6.70 | | | | | | get(int, int, all_132_9, all_132_2) = all_356_0 & % 42.24/6.70 | | | | | | uni(all_356_0) % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | ALPHA: (114) implies: % 42.24/6.70 | | | | | | (115) get(int, int, all_132_9, all_132_2) = all_356_0 % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | GROUND_INST: instantiating (select_neq) with int, int, all_132_9, % 42.24/6.70 | | | | | | all_132_8, all_132_2, all_356_0, all_132_7, all_132_6, % 42.24/6.70 | | | | | | simplifying with (11), (37), (38), (39), (41), (43), % 42.24/6.70 | | | | | | (92), (97), (115) gives: % 42.24/6.70 | | | | | | (116) all_132_2 = all_132_8 | (get(int, int, all_132_6, % 42.24/6.70 | | | | | | all_132_2) = all_356_0 & uni(all_356_0)) % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | BETA: splitting (116) gives: % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | | Case 1: % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | (117) all_132_2 = all_132_8 % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | REDUCE: (106), (117) imply: % 42.24/6.70 | | | | | | | (118) $false % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | CLOSE: (118) is inconsistent. % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | Case 2: % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | (119) get(int, int, all_132_6, all_132_2) = all_356_0 & % 42.24/6.70 | | | | | | | uni(all_356_0) % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | ALPHA: (119) implies: % 42.24/6.70 | | | | | | | (120) get(int, int, all_132_6, all_132_2) = all_356_0 % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | GROUND_INST: instantiating (18) with all_132_1, all_356_0, % 42.24/6.70 | | | | | | | all_132_2, all_132_6, int, int, simplifying with % 42.24/6.70 | | | | | | | (102), (120) gives: % 42.24/6.70 | | | | | | | (121) all_356_0 = all_132_1 % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | REDUCE: (115), (121) imply: % 42.24/6.70 | | | | | | | (122) get(int, int, all_132_9, all_132_2) = all_132_1 % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | DELTA: instantiating (113) with fresh symbol all_344_0 gives: % 42.24/6.70 | | | | | | | (123) tb2t2(all_344_0) = $difference(all_132_13, all_132_3) & % 42.24/6.70 | | | | | | | get(int, int, all_132_9, all_132_2) = all_344_0 & % 42.24/6.70 | | | | | | | uni(all_344_0) % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | ALPHA: (123) implies: % 42.24/6.70 | | | | | | | (124) get(int, int, all_132_9, all_132_2) = all_344_0 % 42.24/6.70 | | | | | | | (125) tb2t2(all_344_0) = $difference(all_132_13, all_132_3) % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | GROUND_INST: instantiating (18) with all_132_1, all_344_0, % 42.24/6.70 | | | | | | | all_132_2, all_132_9, int, int, simplifying with % 42.24/6.70 | | | | | | | (122), (124) gives: % 42.24/6.70 | | | | | | | (126) all_344_0 = all_132_1 % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | GROUND_INST: instantiating (16) with all_132_0, % 42.24/6.70 | | | | | | | $difference(all_132_13, all_132_3), all_132_1, % 42.24/6.70 | | | | | | | simplifying with (47) gives: % 42.24/6.70 | | | | | | | (127) $sum(all_132_0, all_132_3) = all_132_13 | ~ % 42.24/6.70 | | | | | | | (tb2t2(all_132_1) = $difference(all_132_13, all_132_3)) % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | REDUCE: (125), (126) imply: % 42.24/6.70 | | | | | | | (128) tb2t2(all_132_1) = $difference(all_132_13, all_132_3) % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | BETA: splitting (127) gives: % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | | Case 1: % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | (129) ~ (tb2t2(all_132_1) = $difference(all_132_13, % 42.24/6.70 | | | | | | | | all_132_3)) % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | PRED_UNIFY: (128), (129) imply: % 42.24/6.70 | | | | | | | | (130) $false % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | CLOSE: (130) is inconsistent. % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | Case 2: % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | (131) $sum(all_132_0, all_132_3) = all_132_13 % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | REDUCE: (34), (131) imply: % 42.24/6.70 | | | | | | | | (132) $false % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | | CLOSE: (132) is inconsistent. % 42.24/6.70 | | | | | | | | % 42.24/6.70 | | | | | | | End of split % 42.24/6.70 | | | | | | | % 42.24/6.70 | | | | | | End of split % 42.24/6.70 | | | | | | % 42.24/6.70 | | | | | End of split % 42.24/6.70 | | | | | % 42.24/6.70 | | | | End of split % 42.24/6.70 | | | | % 42.24/6.70 | | | Case 2: % 42.24/6.70 | | | | % 42.24/6.70 | | | | (133) all_132_2 = all_132_8 % 42.24/6.70 | | | | % 42.24/6.70 | | | | REDUCE: (96), (133) imply: % 42.24/6.70 | | | | (134) tb2t2(all_132_8) = all_132_3 % 42.24/6.70 | | | | % 42.24/6.70 | | | | REDUCE: (102), (133) imply: % 42.24/6.70 | | | | (135) get(int, int, all_132_6, all_132_8) = all_132_1 % 42.24/6.70 | | | | % 42.24/6.70 | | | | BETA: splitting (100) gives: % 42.24/6.70 | | | | % 42.24/6.70 | | | | Case 1: % 42.24/6.70 | | | | | % 42.24/6.70 | | | | | (136) ~ (tb2t2(all_132_8) = all_132_3) % 42.24/6.70 | | | | | % 42.24/6.70 | | | | | PRED_UNIFY: (134), (136) imply: % 42.24/6.70 | | | | | (137) $false % 42.24/6.70 | | | | | % 42.24/6.70 | | | | | CLOSE: (137) is inconsistent. % 42.24/6.70 | | | | | % 42.24/6.70 | | | | Case 2: % 42.24/6.70 | | | | | % 42.88/6.70 | | | | | (138) all_132_3 = all_132_10 % 42.88/6.70 | | | | | % 42.88/6.70 | | | | | REDUCE: (34), (138) imply: % 42.88/6.70 | | | | | (139) ~ ($sum(all_132_0, all_132_10) = all_132_13) % 42.88/6.70 | | | | | % 42.88/6.70 | | | | | BETA: splitting (103) gives: % 42.88/6.70 | | | | | % 42.88/6.70 | | | | | Case 1: % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | (140) ~ (get(int, int, all_132_6, all_132_8) = all_132_1) % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | PRED_UNIFY: (135), (140) imply: % 42.88/6.70 | | | | | | (141) $false % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | CLOSE: (141) is inconsistent. % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | Case 2: % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | (142) all_132_1 = all_132_7 % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | REDUCE: (47), (142) imply: % 42.88/6.70 | | | | | | (143) tb2t2(all_132_7) = all_132_0 % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | BETA: splitting (99) gives: % 42.88/6.70 | | | | | | % 42.88/6.70 | | | | | | Case 1: % 42.88/6.70 | | | | | | | % 42.88/6.71 | | | | | | | (144) ~ (tb2t2(all_132_7) = all_132_0) % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | | PRED_UNIFY: (143), (144) imply: % 42.88/6.71 | | | | | | | (145) $false % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | | CLOSE: (145) is inconsistent. % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | Case 2: % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | | (146) $sum(all_132_0, all_132_10) = all_132_13 % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | | REDUCE: (139), (146) imply: % 42.88/6.71 | | | | | | | (147) $false % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | | CLOSE: (147) is inconsistent. % 42.88/6.71 | | | | | | | % 42.88/6.71 | | | | | | End of split % 42.88/6.71 | | | | | | % 42.88/6.71 | | | | | End of split % 42.88/6.71 | | | | | % 42.88/6.71 | | | | End of split % 42.88/6.71 | | | | % 42.88/6.71 | | | End of split % 42.88/6.71 | | | % 42.88/6.71 | | End of split % 42.88/6.71 | | % 42.88/6.71 | End of split % 42.88/6.71 | % 42.88/6.71 End of proof % 42.88/6.71 % SZS output end Proof for theBenchmark % 42.88/6.71 % 42.88/6.71 6091ms %------------------------------------------------------------------------------