%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW610_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 : n011.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:53 EDT 2023 % Result : Theorem 14.81s 2.81s % Output : Proof 30.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : SWW610_2 : TPTP v8.1.2. Released v6.1.0. % 0.06/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 19:09:10 EDT 2023 % 0.12/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.62 (2023-06-19) % 0.19/0.62 % 0.19/0.62 (c) Philipp Rümmer, 2009-2023 % 0.19/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.62 Amanda Stjerna. % 0.19/0.62 Free software under BSD-3-Clause. % 0.19/0.62 % 0.19/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.62 % 0.19/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.63 Running up to 7 provers in parallel. % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 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 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 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 % 3.55/1.23 Prover 2: Preprocessing ... % 3.55/1.23 Prover 1: Preprocessing ... % 3.55/1.23 Prover 4: Preprocessing ... % 3.55/1.23 Prover 5: Preprocessing ... % 3.55/1.23 Prover 3: Preprocessing ... % 3.55/1.24 Prover 0: Preprocessing ... % 3.55/1.24 Prover 6: Preprocessing ... % 7.62/1.85 Prover 1: Warning: ignoring some quantifiers % 7.62/1.87 Prover 3: Warning: ignoring some quantifiers % 8.02/1.88 Prover 4: Warning: ignoring some quantifiers % 8.02/1.90 Prover 5: Proving ... % 8.02/1.91 Prover 6: Proving ... % 8.02/1.92 Prover 1: Constructing countermodel ... % 8.02/1.92 Prover 4: Constructing countermodel ... % 8.02/1.92 Prover 3: Constructing countermodel ... % 8.02/1.96 Prover 0: Proving ... % 9.24/2.06 Prover 2: Proving ... % 14.81/2.80 Prover 6: proved (2160ms) % 14.81/2.81 % 14.81/2.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.81/2.81 % 14.81/2.81 Prover 0: stopped % 14.81/2.81 Prover 3: stopped % 14.81/2.82 Prover 5: stopped % 14.81/2.82 Prover 2: stopped % 14.81/2.82 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.81/2.82 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 14.81/2.82 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.81/2.82 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.81/2.83 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 15.74/2.95 Prover 8: Preprocessing ... % 15.74/2.97 Prover 7: Preprocessing ... % 15.74/2.97 Prover 11: Preprocessing ... % 15.74/2.97 Prover 10: Preprocessing ... % 15.74/2.97 Prover 13: Preprocessing ... % 17.06/3.09 Prover 11: Warning: ignoring some quantifiers % 17.06/3.11 Prover 11: Constructing countermodel ... % 17.06/3.13 Prover 10: Warning: ignoring some quantifiers % 17.06/3.14 Prover 10: Constructing countermodel ... % 17.06/3.16 Prover 8: Warning: ignoring some quantifiers % 17.70/3.18 Prover 8: Constructing countermodel ... % 17.70/3.21 Prover 13: Warning: ignoring some quantifiers % 17.70/3.21 Prover 7: Warning: ignoring some quantifiers % 17.70/3.22 Prover 10: gave up % 17.70/3.24 Prover 7: Constructing countermodel ... % 17.70/3.24 Prover 13: Constructing countermodel ... % 17.70/3.24 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 18.46/3.29 Prover 16: Preprocessing ... % 18.68/3.39 Prover 16: Warning: ignoring some quantifiers % 18.68/3.41 Prover 16: Constructing countermodel ... % 20.06/3.51 Prover 7: gave up % 20.06/3.52 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 20.06/3.55 Prover 19: Preprocessing ... % 20.99/3.68 Prover 19: Warning: ignoring some quantifiers % 20.99/3.71 Prover 19: Constructing countermodel ... % 23.94/4.02 Prover 16: gave up % 29.62/4.80 Prover 1: Found proof (size 235) % 29.62/4.80 Prover 1: proved (4166ms) % 29.93/4.80 Prover 8: stopped % 29.93/4.80 Prover 19: stopped % 29.93/4.80 Prover 11: stopped % 29.93/4.80 Prover 4: stopped % 29.93/4.80 Prover 13: stopped % 29.93/4.80 % 29.93/4.80 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.93/4.80 % 29.93/4.83 % SZS output start Proof for theBenchmark % 29.93/4.83 Assumptions after simplification: % 29.93/4.83 --------------------------------- % 29.93/4.83 % 29.93/4.83 (matches_contradiction_at_first) % 30.08/4.85 ty(char) & ! [v0: array_char] : ! [v1: array_char] : ! [v2: int] : ! [v3: % 30.08/4.85 int] : ! [v4: int] : ( ~ ($lesseq(1, v4)) | ~ (matches1(v0, v2, v1, v3, % 30.08/4.85 v4) = 0) | ~ array_char(v1) | ~ array_char(v0) | ? [v5: uni] : ? % 30.08/4.85 [v6: uni] : ? [v7: char1] : ? [v8: uni] : ? [v9: uni] : (tb2t2(v9) = v7 & % 30.08/4.85 tb2t2(v6) = v7 & t2tb1(v1) = v8 & t2tb1(v0) = v5 & get2(char, v8, v3) = v9 % 30.08/4.85 & get2(char, v5, v2) = v6 & char1(v7) & uni(v9) & uni(v8) & uni(v6) & % 30.08/4.85 uni(v5))) % 30.08/4.85 % 30.08/4.85 (matches_contradiction_at_i) % 30.08/4.85 ty(char) & ! [v0: array_char] : ! [v1: array_char] : ! [v2: int] : ! [v3: % 30.08/4.85 int] : ! [v4: int] : ! [v5: int] : ! [v6: uni] : ! [v7: uni] : ( ~ % 30.08/4.85 ($lesseq(1, $difference(v5, v4))) | ~ ($lesseq(1, v5)) | ~ ($lesseq(0, % 30.08/4.85 v4)) | ~ (matches1(v0, v2, v1, v3, v5) = 0) | ~ (t2tb1(v0) = v6) | ~ % 30.08/4.85 (get2(char, v6, $sum(v4, v2)) = v7) | ~ array_char(v1) | ~ array_char(v0) % 30.08/4.85 | ? [v8: char1] : ? [v9: uni] : ? [v10: uni] : (tb2t2(v10) = v8 & % 30.08/4.85 tb2t2(v7) = v8 & t2tb1(v1) = v9 & get2(char, v9, $sum(v4, v3)) = v10 & % 30.08/4.85 char1(v8) & uni(v10) & uni(v9))) % 30.08/4.85 % 30.08/4.85 (matches_def) % 30.08/4.86 ty(char) & ! [v0: array_char] : ! [v1: int] : ! [v2: array_char] : ! [v3: % 30.08/4.86 int] : ! [v4: int] : ! [v5: int] : (v5 = 0 | ~ ($lesseq(0, v3)) | ~ % 30.08/4.86 ($lesseq(0, v1)) | ~ (matches1(v0, v1, v2, v3, v4) = v5) | ~ % 30.08/4.86 array_char(v2) | ~ array_char(v0) | ? [v6: uni] : ? [v7: int] : ? [v8: % 30.08/4.86 uni] : ? [v9: int] : (t2tb1(v2) = v8 & t2tb1(v0) = v6 & length1(char, v8) % 30.08/4.86 = v9 & length1(char, v6) = v7 & uni(v8) & uni(v6) & ( ~ ($lesseq(v3, % 30.08/4.86 $difference(v9, v4))) | ~ ($lesseq(v1, $difference(v7, v4))) | ? % 30.08/4.86 [v10: int] : ? [v11: uni] : ? [v12: char1] : ? [v13: uni] : ? [v14: % 30.08/4.86 char1] : ( ~ (v14 = v12) & $lesseq(1, $difference(v4, v10)) & % 30.08/4.86 $lesseq(0, v10) & tb2t2(v13) = v14 & tb2t2(v11) = v12 & get2(char, v8, % 30.08/4.86 $sum(v10, v3)) = v13 & get2(char, v6, $sum(v10, v1)) = v11 & % 30.08/4.86 char1(v14) & char1(v12) & uni(v13) & uni(v11))))) & ! [v0: % 30.08/4.86 array_char] : ! [v1: int] : ! [v2: array_char] : ! [v3: int] : ! [v4: % 30.08/4.86 int] : ( ~ (matches1(v0, v1, v2, v3, v4) = 0) | ~ array_char(v2) | ~ % 30.08/4.86 array_char(v0) | ($lesseq(0, v3) & $lesseq(0, v1) & ? [v5: uni] : ? [v6: % 30.08/4.86 int] : ? [v7: uni] : ? [v8: int] : ($lesseq(v3, $difference(v8, v4)) & % 30.08/4.86 $lesseq(v1, $difference(v6, v4)) & t2tb1(v2) = v7 & t2tb1(v0) = v5 & % 30.08/4.86 length1(char, v7) = v8 & length1(char, v5) = v6 & uni(v7) & uni(v5) & ! % 30.08/4.86 [v9: int] : ! [v10: uni] : ( ~ ($lesseq(1, $difference(v4, v9))) | ~ % 30.08/4.86 ($lesseq(0, v9)) | ~ (get2(char, v5, $sum(v9, v1)) = v10) | ? [v11: % 30.08/4.86 char1] : ? [v12: uni] : (tb2t2(v12) = v11 & tb2t2(v10) = v11 & % 30.08/4.86 get2(char, v7, $sum(v9, v3)) = v12 & char1(v11) & uni(v12)))))) % 30.08/4.86 % 30.08/4.86 (matches_right_extension) % 30.08/4.86 ty(char) & ? [v0: int] : ! [v1: array_char] : ! [v2: array_char] : ! [v3: % 30.08/4.86 int] : ! [v4: int] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 30.08/4.86 uni] : ( ~ (t2tb1(v2) = v6) | ~ (t2tb1(v1) = v5) | ~ (get2(char, v6, % 30.08/4.86 $sum(v4, v3)) = v8) | ~ (get2(char, v5, $sum(v4, v0)) = v7) | ~ % 30.08/4.86 array_char(v2) | ~ array_char(v1) | ? [v9: any] : ? [v10: int] : ? [v11: % 30.08/4.86 int] : ? [v12: char1] : ? [v13: char1] : ? [v14: any] : (matches1(v1, % 30.08/4.86 v0, v2, v3, $sum(v4, 1)) = v14 & matches1(v1, v0, v2, v3, v4) = v9 & % 30.08/4.86 tb2t2(v8) = v13 & tb2t2(v7) = v12 & length1(char, v6) = v11 & % 30.08/4.87 length1(char, v5) = v10 & char1(v13) & char1(v12) & ( ~ (v13 = v12) | ~ % 30.08/4.87 (v9 = 0) | v14 = 0 | ~ ($lesseq(1, $difference($difference(v11, v4), % 30.08/4.87 v3))) | ~ ($lesseq(1, $difference($difference(v10, v4), v0)))))) % 30.08/4.87 % 30.08/4.87 (matches_right_weakening) % 30.08/4.87 ? [v0: array_char] : ? [v1: array_char] : ? [v2: int] : ? [v3: int] : ? % 30.08/4.87 [v4: int] : ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & $lesseq(1, % 30.08/4.87 $difference(v4, v5)) & matches1(v0, v2, v1, v3, v5) = v6 & matches1(v0, % 30.08/4.87 v2, v1, v3, v4) = 0 & array_char(v1) & array_char(v0)) % 30.08/4.87 % 30.08/4.87 (function-axioms) % 30.08/4.87 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 30.08/4.87 [v3: int] : ! [v4: array_char] : ! [v5: int] : ! [v6: array_char] : (v1 = % 30.08/4.87 v0 | ~ (matches1(v6, v5, v4, v3, v2) = v1) | ~ (matches1(v6, v5, v4, v3, % 30.08/4.87 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : % 30.08/4.87 ! [v4: uni] : ! [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, % 30.08/4.87 v2) = v1) | ~ (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 30.08/4.87 uni] : ! [v2: uni] : ! [v3: int] : ! [v4: uni] : ! [v5: ty] : (v1 = v0 | % 30.08/4.87 ~ (set2(v5, v4, v3, v2) = v1) | ~ (set2(v5, v4, v3, v2) = v0)) & ! [v0: % 30.08/4.87 uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: ty] : ! [v5: % 30.08/4.87 ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ (get(v5, v4, v3, v2) = % 30.08/4.87 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 30.08/4.87 bool1] : ! [v5: ty] : (v1 = v0 | ~ (match_bool1(v5, v4, v3, v2) = v1) | ~ % 30.08/4.87 (match_bool1(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 30.08/4.87 uni] : ! [v3: int] : ! [v4: ty] : (v1 = v0 | ~ (make1(v4, v3, v2) = v1) | % 30.08/4.87 ~ (make1(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: int] : % 30.08/4.87 ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ % 30.08/4.87 (get2(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 30.08/4.87 [v3: int] : ! [v4: ty] : (v1 = v0 | ~ (mk_array1(v4, v3, v2) = v1) | ~ % 30.08/4.87 (mk_array1(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 30.08/4.87 ! [v3: ty] : ! [v4: ty] : (v1 = v0 | ~ (const(v4, v3, v2) = v1) | ~ % 30.08/4.87 (const(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 30.08/4.87 [v3: ty] : (v1 = v0 | ~ (elts(v3, v2) = v1) | ~ (elts(v3, v2) = v0)) & ! % 30.08/4.87 [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 30.08/4.87 (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) & ! [v0: ty] : ! [v1: % 30.08/4.87 ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, v2) = v1) | ~ % 30.08/4.87 (map(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 30.08/4.87 ty] : (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ (contents(v3, v2) = v0)) & % 30.08/4.87 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 30.08/4.87 (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & ! [v0: % 30.08/4.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: ty] % 30.08/4.87 : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! [v0: % 30.08/4.87 char1] : ! [v1: char1] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | ~ % 30.08/4.87 (tb2t2(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: char1] : (v1 = v0 % 30.08/4.87 | ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! [v0: array_char] : ! [v1: % 30.08/4.87 array_char] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ (tb2t1(v2) % 30.08/4.87 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: array_char] : (v1 = v0 | ~ % 30.08/4.87 (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 30.08/4.87 [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & ! [v0: uni] % 30.08/4.87 : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = % 30.08/4.87 v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (array(v2) % 30.08/4.87 = v1) | ~ (array(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : % 30.08/4.87 (v1 = v0 | ~ (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: uni] : ! [v1: % 30.08/4.87 uni] : ! [v2: ty] : (v1 = v0 | ~ (witness1(v2) = v1) | ~ (witness1(v2) = % 30.08/4.87 v0)) % 30.08/4.87 % 30.08/4.87 Further assumptions not needed in the proof: % 30.08/4.87 -------------------------------------------- % 30.08/4.88 array_inversion2, bool_inversion, bridgeL, bridgeL1, bridgeL2, bridgeR, % 30.08/4.88 bridgeR1, bridgeR2, compatOrderMult, const, const_sort2, contents_def1, % 30.08/4.88 contents_sort1, elts_def2, elts_sort2, get_def, get_sort4, get_sort5, % 30.08/4.88 length_def2, make_def, make_sort1, match_bool_False, match_bool_True, % 30.08/4.88 match_bool_sort1, matches_empty, mk_array_sort2, mk_ref_sort1, ref_inversion1, % 30.08/4.88 select_eq, select_neq, set_def, set_sort3, set_sort4, t2tb_sort, t2tb_sort1, % 30.08/4.88 t2tb_sort2, true_False, tuple0_inversion, witness_sort1 % 30.08/4.88 % 30.08/4.88 Those formulas are unsatisfiable: % 30.08/4.88 --------------------------------- % 30.08/4.88 % 30.08/4.88 Begin of proof % 30.08/4.88 | % 30.08/4.88 | ALPHA: (matches_def) implies: % 30.08/4.88 | (1) ! [v0: array_char] : ! [v1: int] : ! [v2: array_char] : ! [v3: int] % 30.08/4.88 | : ! [v4: int] : ( ~ (matches1(v0, v1, v2, v3, v4) = 0) | ~ % 30.08/4.88 | array_char(v2) | ~ array_char(v0) | ($lesseq(0, v3) & $lesseq(0, v1) % 30.08/4.88 | & ? [v5: uni] : ? [v6: int] : ? [v7: uni] : ? [v8: int] : % 30.08/4.88 | ($lesseq(v3, $difference(v8, v4)) & $lesseq(v1, $difference(v6, % 30.08/4.88 | v4)) & t2tb1(v2) = v7 & t2tb1(v0) = v5 & length1(char, v7) = % 30.08/4.88 | v8 & length1(char, v5) = v6 & uni(v7) & uni(v5) & ! [v9: int] : % 30.08/4.88 | ! [v10: uni] : ( ~ ($lesseq(1, $difference(v4, v9))) | ~ % 30.08/4.88 | ($lesseq(0, v9)) | ~ (get2(char, v5, $sum(v9, v1)) = v10) | ? % 30.08/4.88 | [v11: char1] : ? [v12: uni] : (tb2t2(v12) = v11 & tb2t2(v10) = % 30.08/4.88 | v11 & get2(char, v7, $sum(v9, v3)) = v12 & char1(v11) & % 30.08/4.88 | uni(v12)))))) % 30.08/4.88 | (2) ! [v0: array_char] : ! [v1: int] : ! [v2: array_char] : ! [v3: int] % 30.08/4.88 | : ! [v4: int] : ! [v5: int] : (v5 = 0 | ~ ($lesseq(0, v3)) | ~ % 30.08/4.88 | ($lesseq(0, v1)) | ~ (matches1(v0, v1, v2, v3, v4) = v5) | ~ % 30.08/4.88 | array_char(v2) | ~ array_char(v0) | ? [v6: uni] : ? [v7: int] : ? % 30.08/4.88 | [v8: uni] : ? [v9: int] : (t2tb1(v2) = v8 & t2tb1(v0) = v6 & % 30.08/4.88 | length1(char, v8) = v9 & length1(char, v6) = v7 & uni(v8) & uni(v6) % 30.08/4.88 | & ( ~ ($lesseq(v3, $difference(v9, v4))) | ~ ($lesseq(v1, % 30.08/4.88 | $difference(v7, v4))) | ? [v10: int] : ? [v11: uni] : ? % 30.08/4.88 | [v12: char1] : ? [v13: uni] : ? [v14: char1] : ( ~ (v14 = v12) % 30.08/4.88 | & $lesseq(1, $difference(v4, v10)) & $lesseq(0, v10) & % 30.08/4.88 | tb2t2(v13) = v14 & tb2t2(v11) = v12 & get2(char, v8, $sum(v10, % 30.08/4.88 | v3)) = v13 & get2(char, v6, $sum(v10, v1)) = v11 & % 30.08/4.88 | char1(v14) & char1(v12) & uni(v13) & uni(v11))))) % 30.08/4.88 | % 30.08/4.88 | ALPHA: (matches_right_extension) implies: % 30.08/4.88 | (3) ? [v0: int] : ! [v1: array_char] : ! [v2: array_char] : ! [v3: int] % 30.08/4.88 | : ! [v4: int] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: % 30.08/4.88 | uni] : ( ~ (t2tb1(v2) = v6) | ~ (t2tb1(v1) = v5) | ~ (get2(char, % 30.08/4.88 | v6, $sum(v4, v3)) = v8) | ~ (get2(char, v5, $sum(v4, v0)) = v7) % 30.08/4.88 | | ~ array_char(v2) | ~ array_char(v1) | ? [v9: any] : ? [v10: % 30.08/4.88 | int] : ? [v11: int] : ? [v12: char1] : ? [v13: char1] : ? [v14: % 30.08/4.88 | any] : (matches1(v1, v0, v2, v3, $sum(v4, 1)) = v14 & matches1(v1, % 30.08/4.88 | v0, v2, v3, v4) = v9 & tb2t2(v8) = v13 & tb2t2(v7) = v12 & % 30.08/4.88 | length1(char, v6) = v11 & length1(char, v5) = v10 & char1(v13) & % 30.08/4.88 | char1(v12) & ( ~ (v13 = v12) | ~ (v9 = 0) | v14 = 0 | ~ % 30.08/4.88 | ($lesseq(1, $difference($difference(v11, v4), v3))) | ~ % 30.08/4.88 | ($lesseq(1, $difference($difference(v10, v4), v0)))))) % 30.08/4.88 | % 30.08/4.88 | ALPHA: (matches_contradiction_at_first) implies: % 30.08/4.88 | (4) ! [v0: array_char] : ! [v1: array_char] : ! [v2: int] : ! [v3: int] % 30.08/4.88 | : ! [v4: int] : ( ~ ($lesseq(1, v4)) | ~ (matches1(v0, v2, v1, v3, % 30.08/4.88 | v4) = 0) | ~ array_char(v1) | ~ array_char(v0) | ? [v5: uni] : % 30.08/4.88 | ? [v6: uni] : ? [v7: char1] : ? [v8: uni] : ? [v9: uni] : % 30.08/4.88 | (tb2t2(v9) = v7 & tb2t2(v6) = v7 & t2tb1(v1) = v8 & t2tb1(v0) = v5 & % 30.08/4.88 | get2(char, v8, v3) = v9 & get2(char, v5, v2) = v6 & char1(v7) & % 30.08/4.88 | uni(v9) & uni(v8) & uni(v6) & uni(v5))) % 30.08/4.89 | % 30.08/4.89 | ALPHA: (matches_contradiction_at_i) implies: % 30.08/4.89 | (5) ! [v0: array_char] : ! [v1: array_char] : ! [v2: int] : ! [v3: int] % 30.08/4.89 | : ! [v4: int] : ! [v5: int] : ! [v6: uni] : ! [v7: uni] : ( ~ % 30.08/4.89 | ($lesseq(1, $difference(v5, v4))) | ~ ($lesseq(1, v5)) | ~ % 30.08/4.89 | ($lesseq(0, v4)) | ~ (matches1(v0, v2, v1, v3, v5) = 0) | ~ % 30.08/4.89 | (t2tb1(v0) = v6) | ~ (get2(char, v6, $sum(v4, v2)) = v7) | ~ % 30.08/4.89 | array_char(v1) | ~ array_char(v0) | ? [v8: char1] : ? [v9: uni] : % 30.08/4.89 | ? [v10: uni] : (tb2t2(v10) = v8 & tb2t2(v7) = v8 & t2tb1(v1) = v9 & % 30.08/4.89 | get2(char, v9, $sum(v4, v3)) = v10 & char1(v8) & uni(v10) & % 30.08/4.89 | uni(v9))) % 30.08/4.89 | % 30.08/4.89 | ALPHA: (function-axioms) implies: % 30.08/4.89 | (6) ! [v0: uni] : ! [v1: uni] : ! [v2: array_char] : (v1 = v0 | ~ % 30.08/4.89 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 30.08/4.89 | (7) ! [v0: char1] : ! [v1: char1] : ! [v2: uni] : (v1 = v0 | ~ % 30.08/4.89 | (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) % 30.08/4.89 | (8) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 30.08/4.89 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) % 30.08/4.89 | (9) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] % 30.08/4.89 | : (v1 = v0 | ~ (get2(v4, v3, v2) = v1) | ~ (get2(v4, v3, v2) = v0)) % 30.08/4.89 | % 30.08/4.89 | DELTA: instantiating (matches_right_weakening) with fresh symbols all_59_0, % 30.08/4.89 | all_59_1, all_59_2, all_59_3, all_59_4, all_59_5, all_59_6 gives: % 30.08/4.89 | (10) ~ (all_59_0 = 0) & $lesseq(1, $difference(all_59_2, all_59_1)) & % 30.08/4.89 | matches1(all_59_6, all_59_4, all_59_5, all_59_3, all_59_1) = all_59_0 % 30.08/4.89 | & matches1(all_59_6, all_59_4, all_59_5, all_59_3, all_59_2) = 0 & % 30.08/4.89 | array_char(all_59_5) & array_char(all_59_6) % 30.08/4.89 | % 30.08/4.89 | ALPHA: (10) implies: % 30.08/4.89 | (11) ~ (all_59_0 = 0) % 30.08/4.89 | (12) $lesseq(1, $difference(all_59_2, all_59_1)) % 30.08/4.89 | (13) array_char(all_59_6) % 30.08/4.89 | (14) array_char(all_59_5) % 30.08/4.89 | (15) matches1(all_59_6, all_59_4, all_59_5, all_59_3, all_59_2) = 0 % 30.08/4.89 | (16) matches1(all_59_6, all_59_4, all_59_5, all_59_3, all_59_1) = all_59_0 % 30.08/4.89 | % 30.08/4.89 | DELTA: instantiating (3) with fresh symbol all_62_0 gives: % 30.08/4.89 | (17) ! [v0: array_char] : ! [v1: array_char] : ! [v2: int] : ! [v3: % 30.08/4.89 | int] : ! [v4: uni] : ! [v5: uni] : ! [v6: uni] : ! [v7: uni] : ( % 30.08/4.89 | ~ (t2tb1(v1) = v5) | ~ (t2tb1(v0) = v4) | ~ (get2(char, v5, % 30.08/4.89 | $sum(v3, v2)) = v7) | ~ (get2(char, v4, $sum(v3, all_62_0)) = % 30.08/4.89 | v6) | ~ array_char(v1) | ~ array_char(v0) | ? [v8: any] : ? % 30.08/4.89 | [v9: int] : ? [v10: int] : ? [v11: char1] : ? [v12: char1] : ? % 30.08/4.89 | [v13: any] : (matches1(v0, all_62_0, v1, v2, $sum(v3, 1)) = v13 & % 30.08/4.89 | matches1(v0, all_62_0, v1, v2, v3) = v8 & tb2t2(v7) = v12 & % 30.08/4.89 | tb2t2(v6) = v11 & length1(char, v5) = v10 & length1(char, v4) = v9 % 30.08/4.89 | & char1(v12) & char1(v11) & ( ~ (v12 = v11) | ~ (v8 = 0) | v13 = % 30.08/4.89 | 0 | ~ ($lesseq(1, $difference($difference(v10, v3), v2))) | ~ % 30.08/4.89 | ($lesseq(1, $difference($difference(v9, v3), all_62_0)))))) % 30.08/4.89 | % 30.08/4.89 | GROUND_INST: instantiating (4) with all_59_6, all_59_5, all_59_4, all_59_3, % 30.08/4.89 | all_59_2, simplifying with (13), (14), (15) gives: % 30.08/4.89 | (18) ~ ($lesseq(1, all_59_2)) | ? [v0: uni] : ? [v1: uni] : ? [v2: % 30.08/4.89 | char1] : ? [v3: uni] : ? [v4: uni] : (tb2t2(v4) = v2 & tb2t2(v1) = % 30.08/4.89 | v2 & t2tb1(all_59_5) = v3 & t2tb1(all_59_6) = v0 & get2(char, v3, % 30.08/4.89 | all_59_3) = v4 & get2(char, v0, all_59_4) = v1 & char1(v2) & % 30.08/4.89 | uni(v4) & uni(v3) & uni(v1) & uni(v0)) % 30.08/4.89 | % 30.08/4.89 | GROUND_INST: instantiating (1) with all_59_6, all_59_4, all_59_5, all_59_3, % 30.08/4.89 | all_59_2, simplifying with (13), (14), (15) gives: % 30.08/4.90 | (19) $lesseq(0, all_59_3) & $lesseq(0, all_59_4) & ? [v0: uni] : ? [v1: % 30.08/4.90 | int] : ? [v2: uni] : ? [v3: int] : ($lesseq(all_59_3, % 30.08/4.90 | $difference(v3, all_59_2)) & $lesseq(all_59_4, $difference(v1, % 30.08/4.90 | all_59_2)) & t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & % 30.08/4.90 | length1(char, v2) = v3 & length1(char, v0) = v1 & uni(v2) & uni(v0) % 30.08/4.90 | & ! [v4: int] : ! [v5: uni] : ( ~ ($lesseq(1, % 30.08/4.90 | $difference(all_59_2, v4))) | ~ ($lesseq(0, v4)) | ~ % 30.08/4.90 | (get2(char, v0, $sum(v4, all_59_4)) = v5) | ? [v6: char1] : ? % 30.08/4.90 | [v7: uni] : (tb2t2(v7) = v6 & tb2t2(v5) = v6 & get2(char, v2, % 30.08/4.90 | $sum(v4, all_59_3)) = v7 & char1(v6) & uni(v7)))) % 30.08/4.90 | % 30.08/4.90 | ALPHA: (19) implies: % 30.08/4.90 | (20) $lesseq(0, all_59_4) % 30.08/4.90 | (21) $lesseq(0, all_59_3) % 30.08/4.90 | (22) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 30.08/4.90 | ($lesseq(all_59_3, $difference(v3, all_59_2)) & $lesseq(all_59_4, % 30.08/4.90 | $difference(v1, all_59_2)) & t2tb1(all_59_5) = v2 & % 30.08/4.90 | t2tb1(all_59_6) = v0 & length1(char, v2) = v3 & length1(char, v0) = % 30.08/4.90 | v1 & uni(v2) & uni(v0) & ! [v4: int] : ! [v5: uni] : ( ~ % 30.08/4.90 | ($lesseq(1, $difference(all_59_2, v4))) | ~ ($lesseq(0, v4)) | ~ % 30.08/4.90 | (get2(char, v0, $sum(v4, all_59_4)) = v5) | ? [v6: char1] : ? % 30.08/4.90 | [v7: uni] : (tb2t2(v7) = v6 & tb2t2(v5) = v6 & get2(char, v2, % 30.08/4.90 | $sum(v4, all_59_3)) = v7 & char1(v6) & uni(v7)))) % 30.08/4.90 | % 30.08/4.90 | GROUND_INST: instantiating (2) with all_59_6, all_59_4, all_59_5, all_59_3, % 30.08/4.90 | all_59_1, all_59_0, simplifying with (13), (14), (16) gives: % 30.08/4.90 | (23) all_59_0 = 0 | ~ ($lesseq(0, all_59_3)) | ~ ($lesseq(0, all_59_4)) | % 30.08/4.90 | ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 30.08/4.90 | (t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & length1(char, v2) = v3 % 30.08/4.90 | & length1(char, v0) = v1 & uni(v2) & uni(v0) & ( ~ % 30.08/4.90 | ($lesseq(all_59_3, $difference(v3, all_59_1))) | ~ % 30.08/4.90 | ($lesseq(all_59_4, $difference(v1, all_59_1))) | ? [v4: int] : ? % 30.08/4.90 | [v5: uni] : ? [v6: char1] : ? [v7: uni] : ? [v8: char1] : ( ~ % 30.08/4.90 | (v8 = v6) & $lesseq(1, $difference(all_59_1, v4)) & $lesseq(0, % 30.08/4.90 | v4) & tb2t2(v7) = v8 & tb2t2(v5) = v6 & get2(char, v2, % 30.08/4.90 | $sum(v4, all_59_3)) = v7 & get2(char, v0, $sum(v4, all_59_4)) % 30.08/4.90 | = v5 & char1(v8) & char1(v6) & uni(v7) & uni(v5)))) % 30.08/4.90 | % 30.08/4.90 | DELTA: instantiating (22) with fresh symbols all_73_0, all_73_1, all_73_2, % 30.08/4.90 | all_73_3 gives: % 30.08/4.90 | (24) $lesseq(all_59_3, $difference(all_73_0, all_59_2)) & $lesseq(all_59_4, % 30.08/4.90 | $difference(all_73_2, all_59_2)) & t2tb1(all_59_5) = all_73_1 & % 30.08/4.90 | t2tb1(all_59_6) = all_73_3 & length1(char, all_73_1) = all_73_0 & % 30.08/4.90 | length1(char, all_73_3) = all_73_2 & uni(all_73_1) & uni(all_73_3) & % 30.08/4.90 | ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_59_2, % 30.08/4.90 | v0))) | ~ ($lesseq(0, v0)) | ~ (get2(char, all_73_3, % 30.08/4.90 | $sum(v0, all_59_4)) = v1) | ? [v2: char1] : ? [v3: uni] : % 30.08/4.90 | (tb2t2(v3) = v2 & tb2t2(v1) = v2 & get2(char, all_73_1, $sum(v0, % 30.08/4.90 | all_59_3)) = v3 & char1(v2) & uni(v3))) % 30.08/4.90 | % 30.08/4.90 | ALPHA: (24) implies: % 30.08/4.90 | (25) $lesseq(all_59_4, $difference(all_73_2, all_59_2)) % 30.08/4.90 | (26) $lesseq(all_59_3, $difference(all_73_0, all_59_2)) % 30.08/4.90 | (27) length1(char, all_73_3) = all_73_2 % 30.08/4.90 | (28) length1(char, all_73_1) = all_73_0 % 30.08/4.90 | (29) t2tb1(all_59_6) = all_73_3 % 30.08/4.90 | (30) t2tb1(all_59_5) = all_73_1 % 30.08/4.90 | (31) ! [v0: int] : ! [v1: uni] : ( ~ ($lesseq(1, $difference(all_59_2, % 30.08/4.90 | v0))) | ~ ($lesseq(0, v0)) | ~ (get2(char, all_73_3, % 30.08/4.90 | $sum(v0, all_59_4)) = v1) | ? [v2: char1] : ? [v3: uni] : % 30.08/4.90 | (tb2t2(v3) = v2 & tb2t2(v1) = v2 & get2(char, all_73_1, $sum(v0, % 30.08/4.90 | all_59_3)) = v3 & char1(v2) & uni(v3))) % 30.08/4.90 | % 30.08/4.90 | BETA: splitting (18) gives: % 30.08/4.90 | % 30.08/4.90 | Case 1: % 30.08/4.90 | | % 30.08/4.90 | | (32) $lesseq(all_59_2, 0) % 30.08/4.90 | | % 30.08/4.90 | | BETA: splitting (23) gives: % 30.08/4.90 | | % 30.08/4.90 | | Case 1: % 30.08/4.90 | | | % 30.08/4.90 | | | (33) $lesseq(all_59_3, -1) % 30.08/4.90 | | | % 30.08/4.90 | | | COMBINE_INEQS: (21), (33) imply: % 30.08/4.90 | | | (34) $false % 30.08/4.91 | | | % 30.08/4.91 | | | CLOSE: (34) is inconsistent. % 30.08/4.91 | | | % 30.08/4.91 | | Case 2: % 30.08/4.91 | | | % 30.08/4.91 | | | (35) all_59_0 = 0 | ~ ($lesseq(0, all_59_4)) | ? [v0: uni] : ? [v1: % 30.08/4.91 | | | int] : ? [v2: uni] : ? [v3: int] : (t2tb1(all_59_5) = v2 & % 30.08/4.91 | | | t2tb1(all_59_6) = v0 & length1(char, v2) = v3 & length1(char, % 30.08/4.91 | | | v0) = v1 & uni(v2) & uni(v0) & ( ~ ($lesseq(all_59_3, % 30.08/4.91 | | | $difference(v3, all_59_1))) | ~ ($lesseq(all_59_4, % 30.08/4.91 | | | $difference(v1, all_59_1))) | ? [v4: int] : ? [v5: uni] % 30.08/4.91 | | | : ? [v6: char1] : ? [v7: uni] : ? [v8: char1] : ( ~ (v8 = % 30.08/4.91 | | | v6) & $lesseq(1, $difference(all_59_1, v4)) & $lesseq(0, % 30.08/4.91 | | | v4) & tb2t2(v7) = v8 & tb2t2(v5) = v6 & get2(char, v2, % 30.08/4.91 | | | $sum(v4, all_59_3)) = v7 & get2(char, v0, $sum(v4, % 30.08/4.91 | | | all_59_4)) = v5 & char1(v8) & char1(v6) & uni(v7) & % 30.08/4.91 | | | uni(v5)))) % 30.08/4.91 | | | % 30.08/4.91 | | | BETA: splitting (35) gives: % 30.08/4.91 | | | % 30.08/4.91 | | | Case 1: % 30.08/4.91 | | | | % 30.08/4.91 | | | | (36) $lesseq(all_59_4, -1) % 30.08/4.91 | | | | % 30.08/4.91 | | | | COMBINE_INEQS: (20), (36) imply: % 30.08/4.91 | | | | (37) $false % 30.08/4.91 | | | | % 30.08/4.91 | | | | CLOSE: (37) is inconsistent. % 30.08/4.91 | | | | % 30.08/4.91 | | | Case 2: % 30.08/4.91 | | | | % 30.08/4.91 | | | | (38) all_59_0 = 0 | ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? % 30.08/4.91 | | | | [v3: int] : (t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & % 30.08/4.91 | | | | length1(char, v2) = v3 & length1(char, v0) = v1 & uni(v2) & % 30.08/4.91 | | | | uni(v0) & ( ~ ($lesseq(all_59_3, $difference(v3, all_59_1))) | % 30.08/4.91 | | | | ~ ($lesseq(all_59_4, $difference(v1, all_59_1))) | ? [v4: % 30.08/4.91 | | | | int] : ? [v5: uni] : ? [v6: char1] : ? [v7: uni] : ? % 30.08/4.91 | | | | [v8: char1] : ( ~ (v8 = v6) & $lesseq(1, % 30.08/4.91 | | | | $difference(all_59_1, v4)) & $lesseq(0, v4) & tb2t2(v7) % 30.08/4.91 | | | | = v8 & tb2t2(v5) = v6 & get2(char, v2, $sum(v4, all_59_3)) % 30.08/4.91 | | | | = v7 & get2(char, v0, $sum(v4, all_59_4)) = v5 & char1(v8) % 30.08/4.91 | | | | & char1(v6) & uni(v7) & uni(v5)))) % 30.08/4.91 | | | | % 30.08/4.91 | | | | BETA: splitting (38) gives: % 30.08/4.91 | | | | % 30.08/4.91 | | | | Case 1: % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | (39) all_59_0 = 0 % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | REDUCE: (11), (39) imply: % 30.08/4.91 | | | | | (40) $false % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | CLOSE: (40) is inconsistent. % 30.08/4.91 | | | | | % 30.08/4.91 | | | | Case 2: % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | (41) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 30.08/4.91 | | | | | (t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & length1(char, % 30.08/4.91 | | | | | v2) = v3 & length1(char, v0) = v1 & uni(v2) & uni(v0) & ( % 30.08/4.91 | | | | | ~ ($lesseq(all_59_3, $difference(v3, all_59_1))) | ~ % 30.08/4.91 | | | | | ($lesseq(all_59_4, $difference(v1, all_59_1))) | ? [v4: % 30.08/4.91 | | | | | int] : ? [v5: uni] : ? [v6: char1] : ? [v7: uni] : ? % 30.08/4.91 | | | | | [v8: char1] : ( ~ (v8 = v6) & $lesseq(1, % 30.08/4.91 | | | | | $difference(all_59_1, v4)) & $lesseq(0, v4) & % 30.08/4.91 | | | | | tb2t2(v7) = v8 & tb2t2(v5) = v6 & get2(char, v2, % 30.08/4.91 | | | | | $sum(v4, all_59_3)) = v7 & get2(char, v0, $sum(v4, % 30.08/4.91 | | | | | all_59_4)) = v5 & char1(v8) & char1(v6) & uni(v7) & % 30.08/4.91 | | | | | uni(v5)))) % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | DELTA: instantiating (41) with fresh symbols all_171_0, all_171_1, % 30.08/4.91 | | | | | all_171_2, all_171_3 gives: % 30.08/4.91 | | | | | (42) t2tb1(all_59_5) = all_171_1 & t2tb1(all_59_6) = all_171_3 & % 30.08/4.91 | | | | | length1(char, all_171_1) = all_171_0 & length1(char, % 30.08/4.91 | | | | | all_171_3) = all_171_2 & uni(all_171_1) & uni(all_171_3) & ( % 30.08/4.91 | | | | | ~ ($lesseq(all_59_3, $difference(all_171_0, all_59_1))) | ~ % 30.08/4.91 | | | | | ($lesseq(all_59_4, $difference(all_171_2, all_59_1))) | ? % 30.08/4.91 | | | | | [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] : % 30.08/4.91 | | | | | ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.08/4.91 | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & tb2t2(v3) % 30.08/4.91 | | | | | = v4 & tb2t2(v1) = v2 & get2(char, all_171_1, $sum(v0, % 30.08/4.91 | | | | | all_59_3)) = v3 & get2(char, all_171_3, $sum(v0, % 30.08/4.91 | | | | | all_59_4)) = v1 & char1(v4) & char1(v2) & uni(v3) & % 30.08/4.91 | | | | | uni(v1))) % 30.08/4.91 | | | | | % 30.08/4.91 | | | | | ALPHA: (42) implies: % 30.08/4.91 | | | | | (43) length1(char, all_171_3) = all_171_2 % 30.08/4.91 | | | | | (44) length1(char, all_171_1) = all_171_0 % 30.08/4.91 | | | | | (45) t2tb1(all_59_6) = all_171_3 % 30.08/4.91 | | | | | (46) t2tb1(all_59_5) = all_171_1 % 30.08/4.92 | | | | | (47) ~ ($lesseq(all_59_3, $difference(all_171_0, all_59_1))) | ~ % 30.08/4.92 | | | | | ($lesseq(all_59_4, $difference(all_171_2, all_59_1))) | ? % 30.08/4.92 | | | | | [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] : ? % 30.08/4.92 | | | | | [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, $difference(all_59_1, % 30.08/4.92 | | | | | v0)) & $lesseq(0, v0) & tb2t2(v3) = v4 & tb2t2(v1) = v2 % 30.08/4.92 | | | | | & get2(char, all_171_1, $sum(v0, all_59_3)) = v3 & % 30.08/4.92 | | | | | get2(char, all_171_3, $sum(v0, all_59_4)) = v1 & char1(v4) & % 30.08/4.92 | | | | | char1(v2) & uni(v3) & uni(v1)) % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | GROUND_INST: instantiating (6) with all_73_3, all_171_3, all_59_6, % 30.08/4.92 | | | | | simplifying with (29), (45) gives: % 30.08/4.92 | | | | | (48) all_171_3 = all_73_3 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | GROUND_INST: instantiating (6) with all_73_1, all_171_1, all_59_5, % 30.08/4.92 | | | | | simplifying with (30), (46) gives: % 30.08/4.92 | | | | | (49) all_171_1 = all_73_1 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | REDUCE: (44), (49) imply: % 30.08/4.92 | | | | | (50) length1(char, all_73_1) = all_171_0 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | REDUCE: (43), (48) imply: % 30.08/4.92 | | | | | (51) length1(char, all_73_3) = all_171_2 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | GROUND_INST: instantiating (8) with all_73_2, all_171_2, all_73_3, % 30.08/4.92 | | | | | char, simplifying with (27), (51) gives: % 30.08/4.92 | | | | | (52) all_171_2 = all_73_2 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | GROUND_INST: instantiating (8) with all_73_0, all_171_0, all_73_1, % 30.08/4.92 | | | | | char, simplifying with (28), (50) gives: % 30.08/4.92 | | | | | (53) all_171_0 = all_73_0 % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | BETA: splitting (47) gives: % 30.08/4.92 | | | | | % 30.08/4.92 | | | | | Case 1: % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | (54) $lesseq(1, $sum($difference(all_59_1, all_171_0), all_59_3)) % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | REDUCE: (53), (54) imply: % 30.08/4.92 | | | | | | (55) $lesseq(1, $sum($difference(all_59_1, all_73_0), all_59_3)) % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | COMBINE_INEQS: (26), (55) imply: % 30.08/4.92 | | | | | | (56) $lesseq(1, $difference(all_59_1, all_59_2)) % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | COMBINE_INEQS: (12), (56) imply: % 30.08/4.92 | | | | | | (57) $false % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | CLOSE: (57) is inconsistent. % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | Case 2: % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | (58) ~ ($lesseq(all_59_4, $difference(all_171_2, all_59_1))) | % 30.08/4.92 | | | | | | ? [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] : % 30.08/4.92 | | | | | | ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.08/4.92 | | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & tb2t2(v3) % 30.08/4.92 | | | | | | = v4 & tb2t2(v1) = v2 & get2(char, all_171_1, $sum(v0, % 30.08/4.92 | | | | | | all_59_3)) = v3 & get2(char, all_171_3, $sum(v0, % 30.08/4.92 | | | | | | all_59_4)) = v1 & char1(v4) & char1(v2) & uni(v3) & % 30.08/4.92 | | | | | | uni(v1)) % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | BETA: splitting (58) gives: % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | | Case 1: % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | (59) $lesseq(1, $sum($difference(all_59_1, all_171_2), % 30.08/4.92 | | | | | | | all_59_4)) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | REDUCE: (52), (59) imply: % 30.08/4.92 | | | | | | | (60) $lesseq(1, $sum($difference(all_59_1, all_73_2), % 30.08/4.92 | | | | | | | all_59_4)) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | COMBINE_INEQS: (25), (60) imply: % 30.08/4.92 | | | | | | | (61) $lesseq(1, $difference(all_59_1, all_59_2)) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | COMBINE_INEQS: (12), (61) imply: % 30.08/4.92 | | | | | | | (62) $false % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | CLOSE: (62) is inconsistent. % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | Case 2: % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | (63) ? [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: % 30.08/4.92 | | | | | | | uni] : ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.08/4.92 | | | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & % 30.08/4.92 | | | | | | | tb2t2(v3) = v4 & tb2t2(v1) = v2 & get2(char, all_171_1, % 30.08/4.92 | | | | | | | $sum(v0, all_59_3)) = v3 & get2(char, all_171_3, % 30.08/4.92 | | | | | | | $sum(v0, all_59_4)) = v1 & char1(v4) & char1(v2) & % 30.08/4.92 | | | | | | | uni(v3) & uni(v1)) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | DELTA: instantiating (63) with fresh symbols all_202_0, all_202_1, % 30.08/4.92 | | | | | | | all_202_2, all_202_3, all_202_4 gives: % 30.08/4.92 | | | | | | | (64) ~ (all_202_0 = all_202_2) & $lesseq(1, % 30.08/4.92 | | | | | | | $difference(all_59_1, all_202_4)) & $lesseq(0, % 30.08/4.92 | | | | | | | all_202_4) & tb2t2(all_202_1) = all_202_0 & % 30.08/4.92 | | | | | | | tb2t2(all_202_3) = all_202_2 & get2(char, all_171_1, % 30.08/4.92 | | | | | | | $sum(all_202_4, all_59_3)) = all_202_1 & get2(char, % 30.08/4.92 | | | | | | | all_171_3, $sum(all_202_4, all_59_4)) = all_202_3 & % 30.08/4.92 | | | | | | | char1(all_202_0) & char1(all_202_2) & uni(all_202_1) & % 30.08/4.92 | | | | | | | uni(all_202_3) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | ALPHA: (64) implies: % 30.08/4.92 | | | | | | | (65) $lesseq(0, all_202_4) % 30.08/4.92 | | | | | | | (66) $lesseq(1, $difference(all_59_1, all_202_4)) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | COMBINE_INEQS: (65), (66) imply: % 30.08/4.92 | | | | | | | (67) $lesseq(1, all_59_1) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | COMBINE_INEQS: (12), (67) imply: % 30.08/4.92 | | | | | | | (68) $lesseq(2, all_59_2) % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | COMBINE_INEQS: (32), (68) imply: % 30.08/4.92 | | | | | | | (69) $false % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | | CLOSE: (69) is inconsistent. % 30.08/4.92 | | | | | | | % 30.08/4.92 | | | | | | End of split % 30.08/4.92 | | | | | | % 30.08/4.92 | | | | | End of split % 30.08/4.92 | | | | | % 30.08/4.92 | | | | End of split % 30.08/4.92 | | | | % 30.08/4.92 | | | End of split % 30.08/4.92 | | | % 30.08/4.92 | | End of split % 30.08/4.92 | | % 30.08/4.92 | Case 2: % 30.08/4.92 | | % 30.08/4.92 | | (70) ? [v0: uni] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] : ? % 30.08/4.92 | | [v4: uni] : (tb2t2(v4) = v2 & tb2t2(v1) = v2 & t2tb1(all_59_5) = v3 % 30.08/4.92 | | & t2tb1(all_59_6) = v0 & get2(char, v3, all_59_3) = v4 & % 30.08/4.92 | | get2(char, v0, all_59_4) = v1 & char1(v2) & uni(v4) & uni(v3) & % 30.08/4.92 | | uni(v1) & uni(v0)) % 30.08/4.92 | | % 30.08/4.92 | | DELTA: instantiating (70) with fresh symbols all_122_0, all_122_1, % 30.08/4.92 | | all_122_2, all_122_3, all_122_4 gives: % 30.08/4.92 | | (71) tb2t2(all_122_0) = all_122_2 & tb2t2(all_122_3) = all_122_2 & % 30.08/4.92 | | t2tb1(all_59_5) = all_122_1 & t2tb1(all_59_6) = all_122_4 & % 30.08/4.92 | | get2(char, all_122_1, all_59_3) = all_122_0 & get2(char, all_122_4, % 30.08/4.92 | | all_59_4) = all_122_3 & char1(all_122_2) & uni(all_122_0) & % 30.08/4.92 | | uni(all_122_1) & uni(all_122_3) & uni(all_122_4) % 30.08/4.92 | | % 30.08/4.92 | | ALPHA: (71) implies: % 30.08/4.93 | | (72) get2(char, all_122_4, all_59_4) = all_122_3 % 30.08/4.93 | | (73) get2(char, all_122_1, all_59_3) = all_122_0 % 30.08/4.93 | | (74) t2tb1(all_59_6) = all_122_4 % 30.08/4.93 | | (75) t2tb1(all_59_5) = all_122_1 % 30.08/4.93 | | % 30.08/4.93 | | GROUND_INST: instantiating (6) with all_73_3, all_122_4, all_59_6, % 30.08/4.93 | | simplifying with (29), (74) gives: % 30.08/4.93 | | (76) all_122_4 = all_73_3 % 30.08/4.93 | | % 30.08/4.93 | | GROUND_INST: instantiating (6) with all_73_1, all_122_1, all_59_5, % 30.08/4.93 | | simplifying with (30), (75) gives: % 30.08/4.93 | | (77) all_122_1 = all_73_1 % 30.08/4.93 | | % 30.08/4.93 | | REDUCE: (73), (77) imply: % 30.08/4.93 | | (78) get2(char, all_73_1, all_59_3) = all_122_0 % 30.08/4.93 | | % 30.08/4.93 | | REDUCE: (72), (76) imply: % 30.08/4.93 | | (79) get2(char, all_73_3, all_59_4) = all_122_3 % 30.08/4.93 | | % 30.08/4.93 | | GROUND_INST: instantiating (17) with all_59_6, all_59_6, all_62_0, % 30.08/4.93 | | $difference(all_59_4, all_62_0), all_73_3, all_73_3, all_122_3, % 30.08/4.93 | | all_122_3, simplifying with (13), (29), (79) gives: % 30.08/4.93 | | (80) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: char1] : ? % 30.08/4.93 | | [v4: char1] : ? [v5: any] : (matches1(all_59_6, all_62_0, all_59_6, % 30.08/4.93 | | all_62_0, $sum($difference(all_59_4, all_62_0), 1)) = v5 & % 30.08/4.93 | | matches1(all_59_6, all_62_0, all_59_6, all_62_0, % 30.08/4.93 | | $difference(all_59_4, all_62_0)) = v0 & tb2t2(all_122_3) = v4 & % 30.08/4.93 | | tb2t2(all_122_3) = v3 & length1(char, all_73_3) = v2 & % 30.08/4.93 | | length1(char, all_73_3) = v1 & char1(v4) & char1(v3) & ( ~ (v4 = % 30.08/4.93 | | v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, $difference(v2, % 30.08/4.93 | | all_59_4))) | ~ ($lesseq(1, $difference(v1, all_59_4))))) % 30.08/4.93 | | % 30.08/4.93 | | GROUND_INST: instantiating (17) with all_59_5, all_59_5, all_62_0, % 30.08/4.93 | | $difference(all_59_3, all_62_0), all_73_1, all_73_1, all_122_0, % 30.08/4.93 | | all_122_0, simplifying with (14), (30), (78) gives: % 30.08/4.93 | | (81) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: char1] : ? % 30.08/4.93 | | [v4: char1] : ? [v5: any] : (matches1(all_59_5, all_62_0, all_59_5, % 30.08/4.93 | | all_62_0, $sum($difference(all_59_3, all_62_0), 1)) = v5 & % 30.08/4.93 | | matches1(all_59_5, all_62_0, all_59_5, all_62_0, % 30.08/4.93 | | $difference(all_59_3, all_62_0)) = v0 & tb2t2(all_122_0) = v4 & % 30.08/4.93 | | tb2t2(all_122_0) = v3 & length1(char, all_73_1) = v2 & % 30.08/4.93 | | length1(char, all_73_1) = v1 & char1(v4) & char1(v3) & ( ~ (v4 = % 30.08/4.93 | | v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, $difference(v2, % 30.08/4.93 | | all_59_3))) | ~ ($lesseq(1, $difference(v1, all_59_3))))) % 30.08/4.93 | | % 30.08/4.93 | | GROUND_INST: instantiating (17) with all_59_6, all_59_5, % 30.08/4.93 | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.08/4.93 | | $difference(all_59_4, all_62_0), all_73_3, all_73_1, all_122_3, % 30.08/4.93 | | all_122_0, simplifying with (13), (14), (29), (30), (78), (79) % 30.08/4.93 | | gives: % 30.08/4.93 | | (82) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: char1] : ? % 30.08/4.93 | | [v4: char1] : ? [v5: any] : (matches1(all_59_6, all_62_0, all_59_5, % 30.08/4.93 | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.08/4.93 | | $sum($difference(all_59_4, all_62_0), 1)) = v5 & % 30.08/4.93 | | matches1(all_59_6, all_62_0, all_59_5, $difference($sum(all_62_0, % 30.08/4.93 | | all_59_3), all_59_4), $difference(all_59_4, all_62_0)) = v0 % 30.55/4.93 | | & tb2t2(all_122_0) = v4 & tb2t2(all_122_3) = v3 & length1(char, % 30.55/4.93 | | all_73_1) = v2 & length1(char, all_73_3) = v1 & char1(v4) & % 30.55/4.93 | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.93 | | $difference(v2, all_59_3))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.93 | | all_59_4))))) % 30.55/4.93 | | % 30.55/4.93 | | GROUND_INST: instantiating (17) with all_59_5, all_59_6, % 30.55/4.93 | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.93 | | $difference(all_59_3, all_62_0), all_73_1, all_73_3, all_122_0, % 30.55/4.93 | | all_122_3, simplifying with (13), (14), (29), (30), (78), (79) % 30.55/4.93 | | gives: % 30.55/4.93 | | (83) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: char1] : ? % 30.55/4.93 | | [v4: char1] : ? [v5: any] : (matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.93 | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.93 | | $sum($difference(all_59_3, all_62_0), 1)) = v5 & % 30.55/4.93 | | matches1(all_59_5, all_62_0, all_59_6, $sum($difference(all_62_0, % 30.55/4.93 | | all_59_3), all_59_4), $difference(all_59_3, all_62_0)) = v0 % 30.55/4.93 | | & tb2t2(all_122_0) = v3 & tb2t2(all_122_3) = v4 & length1(char, % 30.55/4.93 | | all_73_1) = v1 & length1(char, all_73_3) = v2 & char1(v4) & % 30.55/4.93 | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.93 | | $difference(v2, all_59_4))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.93 | | all_59_3))))) % 30.55/4.93 | | % 30.55/4.93 | | DELTA: instantiating (83) with fresh symbols all_136_0, all_136_1, % 30.55/4.93 | | all_136_2, all_136_3, all_136_4, all_136_5 gives: % 30.55/4.93 | | (84) matches1(all_59_5, all_62_0, all_59_6, $sum($difference(all_62_0, % 30.55/4.93 | | all_59_3), all_59_4), $sum($difference(all_59_3, all_62_0), % 30.55/4.93 | | 1)) = all_136_0 & matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.93 | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.93 | | $difference(all_59_3, all_62_0)) = all_136_5 & tb2t2(all_122_0) = % 30.55/4.93 | | all_136_2 & tb2t2(all_122_3) = all_136_1 & length1(char, all_73_1) = % 30.55/4.93 | | all_136_4 & length1(char, all_73_3) = all_136_3 & char1(all_136_1) & % 30.55/4.93 | | char1(all_136_2) & ( ~ (all_136_1 = all_136_2) | ~ (all_136_5 = 0) % 30.55/4.93 | | | all_136_0 = 0 | ~ ($lesseq(1, $difference(all_136_3, % 30.55/4.93 | | all_59_4))) | ~ ($lesseq(1, $difference(all_136_4, % 30.55/4.93 | | all_59_3)))) % 30.55/4.93 | | % 30.55/4.93 | | ALPHA: (84) implies: % 30.55/4.93 | | (85) length1(char, all_73_3) = all_136_3 % 30.55/4.93 | | (86) length1(char, all_73_1) = all_136_4 % 30.55/4.93 | | % 30.55/4.93 | | DELTA: instantiating (82) with fresh symbols all_138_0, all_138_1, % 30.55/4.93 | | all_138_2, all_138_3, all_138_4, all_138_5 gives: % 30.55/4.93 | | (87) matches1(all_59_6, all_62_0, all_59_5, $difference($sum(all_62_0, % 30.55/4.93 | | all_59_3), all_59_4), $sum($difference(all_59_4, all_62_0), % 30.55/4.93 | | 1)) = all_138_0 & matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.93 | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.55/4.93 | | $difference(all_59_4, all_62_0)) = all_138_5 & tb2t2(all_122_0) = % 30.55/4.93 | | all_138_1 & tb2t2(all_122_3) = all_138_2 & length1(char, all_73_1) = % 30.55/4.93 | | all_138_3 & length1(char, all_73_3) = all_138_4 & char1(all_138_1) & % 30.55/4.93 | | char1(all_138_2) & ( ~ (all_138_1 = all_138_2) | ~ (all_138_5 = 0) % 30.55/4.93 | | | all_138_0 = 0 | ~ ($lesseq(1, $difference(all_138_3, % 30.55/4.93 | | all_59_3))) | ~ ($lesseq(1, $difference(all_138_4, % 30.55/4.93 | | all_59_4)))) % 30.55/4.93 | | % 30.55/4.93 | | ALPHA: (87) implies: % 30.55/4.93 | | (88) length1(char, all_73_3) = all_138_4 % 30.55/4.93 | | (89) length1(char, all_73_1) = all_138_3 % 30.55/4.93 | | % 30.55/4.93 | | DELTA: instantiating (81) with fresh symbols all_140_0, all_140_1, % 30.55/4.93 | | all_140_2, all_140_3, all_140_4, all_140_5 gives: % 30.55/4.93 | | (90) matches1(all_59_5, all_62_0, all_59_5, all_62_0, % 30.55/4.93 | | $sum($difference(all_59_3, all_62_0), 1)) = all_140_0 & % 30.55/4.93 | | matches1(all_59_5, all_62_0, all_59_5, all_62_0, % 30.55/4.93 | | $difference(all_59_3, all_62_0)) = all_140_5 & tb2t2(all_122_0) = % 30.55/4.93 | | all_140_1 & tb2t2(all_122_0) = all_140_2 & length1(char, all_73_1) = % 30.55/4.93 | | all_140_3 & length1(char, all_73_1) = all_140_4 & char1(all_140_1) & % 30.55/4.93 | | char1(all_140_2) & ( ~ (all_140_1 = all_140_2) | ~ (all_140_5 = 0) % 30.55/4.93 | | | all_140_0 = 0 | ~ ($lesseq(1, $difference(all_140_3, % 30.55/4.93 | | all_59_3))) | ~ ($lesseq(1, $difference(all_140_4, % 30.55/4.93 | | all_59_3)))) % 30.55/4.93 | | % 30.55/4.93 | | ALPHA: (90) implies: % 30.55/4.93 | | (91) length1(char, all_73_1) = all_140_4 % 30.55/4.93 | | (92) length1(char, all_73_1) = all_140_3 % 30.55/4.93 | | % 30.55/4.93 | | DELTA: instantiating (80) with fresh symbols all_142_0, all_142_1, % 30.55/4.93 | | all_142_2, all_142_3, all_142_4, all_142_5 gives: % 30.55/4.94 | | (93) matches1(all_59_6, all_62_0, all_59_6, all_62_0, % 30.55/4.94 | | $sum($difference(all_59_4, all_62_0), 1)) = all_142_0 & % 30.55/4.94 | | matches1(all_59_6, all_62_0, all_59_6, all_62_0, % 30.55/4.94 | | $difference(all_59_4, all_62_0)) = all_142_5 & tb2t2(all_122_3) = % 30.55/4.94 | | all_142_1 & tb2t2(all_122_3) = all_142_2 & length1(char, all_73_3) = % 30.55/4.94 | | all_142_3 & length1(char, all_73_3) = all_142_4 & char1(all_142_1) & % 30.55/4.94 | | char1(all_142_2) & ( ~ (all_142_1 = all_142_2) | ~ (all_142_5 = 0) % 30.55/4.94 | | | all_142_0 = 0 | ~ ($lesseq(1, $difference(all_142_3, % 30.55/4.94 | | all_59_4))) | ~ ($lesseq(1, $difference(all_142_4, % 30.55/4.94 | | all_59_4)))) % 30.55/4.94 | | % 30.55/4.94 | | ALPHA: (93) implies: % 30.55/4.94 | | (94) length1(char, all_73_3) = all_142_4 % 30.55/4.94 | | (95) length1(char, all_73_3) = all_142_3 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_73_2, all_138_4, all_73_3, char, % 30.55/4.94 | | simplifying with (27), (88) gives: % 30.55/4.94 | | (96) all_138_4 = all_73_2 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_138_4, all_142_4, all_73_3, char, % 30.55/4.94 | | simplifying with (88), (94) gives: % 30.55/4.94 | | (97) all_142_4 = all_138_4 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_142_4, all_142_3, all_73_3, char, % 30.55/4.94 | | simplifying with (94), (95) gives: % 30.55/4.94 | | (98) all_142_3 = all_142_4 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_136_3, all_142_3, all_73_3, char, % 30.55/4.94 | | simplifying with (85), (95) gives: % 30.55/4.94 | | (99) all_142_3 = all_136_3 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_73_0, all_140_4, all_73_1, char, % 30.55/4.94 | | simplifying with (28), (91) gives: % 30.55/4.94 | | (100) all_140_4 = all_73_0 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_138_3, all_140_4, all_73_1, char, % 30.55/4.94 | | simplifying with (89), (91) gives: % 30.55/4.94 | | (101) all_140_4 = all_138_3 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_140_4, all_140_3, all_73_1, char, % 30.55/4.94 | | simplifying with (91), (92) gives: % 30.55/4.94 | | (102) all_140_3 = all_140_4 % 30.55/4.94 | | % 30.55/4.94 | | GROUND_INST: instantiating (8) with all_136_4, all_140_3, all_73_1, char, % 30.55/4.94 | | simplifying with (86), (92) gives: % 30.55/4.94 | | (103) all_140_3 = all_136_4 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (98), (99) imply: % 30.55/4.94 | | (104) all_142_4 = all_136_3 % 30.55/4.94 | | % 30.55/4.94 | | SIMP: (104) implies: % 30.55/4.94 | | (105) all_142_4 = all_136_3 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (97), (105) imply: % 30.55/4.94 | | (106) all_138_4 = all_136_3 % 30.55/4.94 | | % 30.55/4.94 | | SIMP: (106) implies: % 30.55/4.94 | | (107) all_138_4 = all_136_3 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (102), (103) imply: % 30.55/4.94 | | (108) all_140_4 = all_136_4 % 30.55/4.94 | | % 30.55/4.94 | | SIMP: (108) implies: % 30.55/4.94 | | (109) all_140_4 = all_136_4 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (100), (101) imply: % 30.55/4.94 | | (110) all_138_3 = all_73_0 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (101), (109) imply: % 30.55/4.94 | | (111) all_138_3 = all_136_4 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (110), (111) imply: % 30.55/4.94 | | (112) all_136_4 = all_73_0 % 30.55/4.94 | | % 30.55/4.94 | | SIMP: (112) implies: % 30.55/4.94 | | (113) all_136_4 = all_73_0 % 30.55/4.94 | | % 30.55/4.94 | | COMBINE_EQS: (96), (107) imply: % 30.55/4.94 | | (114) all_136_3 = all_73_2 % 30.55/4.94 | | % 30.55/4.94 | | SIMP: (114) implies: % 30.55/4.94 | | (115) all_136_3 = all_73_2 % 30.55/4.94 | | % 30.55/4.94 | | BETA: splitting (23) gives: % 30.55/4.94 | | % 30.55/4.94 | | Case 1: % 30.55/4.94 | | | % 30.55/4.94 | | | (116) $lesseq(all_59_3, -1) % 30.55/4.94 | | | % 30.55/4.94 | | | COMBINE_INEQS: (21), (116) imply: % 30.55/4.94 | | | (117) $false % 30.55/4.94 | | | % 30.55/4.94 | | | CLOSE: (117) is inconsistent. % 30.55/4.94 | | | % 30.55/4.94 | | Case 2: % 30.55/4.94 | | | % 30.55/4.94 | | | (118) all_59_0 = 0 | ~ ($lesseq(0, all_59_4)) | ? [v0: uni] : ? [v1: % 30.55/4.94 | | | int] : ? [v2: uni] : ? [v3: int] : (t2tb1(all_59_5) = v2 & % 30.55/4.94 | | | t2tb1(all_59_6) = v0 & length1(char, v2) = v3 & length1(char, % 30.55/4.94 | | | v0) = v1 & uni(v2) & uni(v0) & ( ~ ($lesseq(all_59_3, % 30.55/4.94 | | | $difference(v3, all_59_1))) | ~ ($lesseq(all_59_4, % 30.55/4.94 | | | $difference(v1, all_59_1))) | ? [v4: int] : ? [v5: uni] % 30.55/4.94 | | | : ? [v6: char1] : ? [v7: uni] : ? [v8: char1] : ( ~ (v8 = % 30.55/4.94 | | | v6) & $lesseq(1, $difference(all_59_1, v4)) & $lesseq(0, % 30.55/4.94 | | | v4) & tb2t2(v7) = v8 & tb2t2(v5) = v6 & get2(char, v2, % 30.55/4.94 | | | $sum(v4, all_59_3)) = v7 & get2(char, v0, $sum(v4, % 30.55/4.94 | | | all_59_4)) = v5 & char1(v8) & char1(v6) & uni(v7) & % 30.55/4.94 | | | uni(v5)))) % 30.55/4.94 | | | % 30.55/4.94 | | | BETA: splitting (118) gives: % 30.55/4.94 | | | % 30.55/4.94 | | | Case 1: % 30.55/4.94 | | | | % 30.55/4.94 | | | | (119) $lesseq(all_59_4, -1) % 30.55/4.94 | | | | % 30.55/4.94 | | | | COMBINE_INEQS: (20), (119) imply: % 30.55/4.94 | | | | (120) $false % 30.55/4.94 | | | | % 30.55/4.94 | | | | CLOSE: (120) is inconsistent. % 30.55/4.94 | | | | % 30.55/4.94 | | | Case 2: % 30.55/4.94 | | | | % 30.55/4.94 | | | | (121) all_59_0 = 0 | ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? % 30.55/4.94 | | | | [v3: int] : (t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & % 30.55/4.94 | | | | length1(char, v2) = v3 & length1(char, v0) = v1 & uni(v2) & % 30.55/4.94 | | | | uni(v0) & ( ~ ($lesseq(all_59_3, $difference(v3, all_59_1))) % 30.55/4.94 | | | | | ~ ($lesseq(all_59_4, $difference(v1, all_59_1))) | ? % 30.55/4.94 | | | | [v4: int] : ? [v5: uni] : ? [v6: char1] : ? [v7: uni] : % 30.55/4.94 | | | | ? [v8: char1] : ( ~ (v8 = v6) & $lesseq(1, % 30.55/4.94 | | | | $difference(all_59_1, v4)) & $lesseq(0, v4) & tb2t2(v7) % 30.55/4.94 | | | | = v8 & tb2t2(v5) = v6 & get2(char, v2, $sum(v4, % 30.55/4.94 | | | | all_59_3)) = v7 & get2(char, v0, $sum(v4, all_59_4)) % 30.55/4.94 | | | | = v5 & char1(v8) & char1(v6) & uni(v7) & uni(v5)))) % 30.55/4.94 | | | | % 30.55/4.94 | | | | BETA: splitting (121) gives: % 30.55/4.94 | | | | % 30.55/4.94 | | | | Case 1: % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | (122) all_59_0 = 0 % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | REDUCE: (11), (122) imply: % 30.55/4.94 | | | | | (123) $false % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | CLOSE: (123) is inconsistent. % 30.55/4.94 | | | | | % 30.55/4.94 | | | | Case 2: % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | (124) ? [v0: uni] : ? [v1: int] : ? [v2: uni] : ? [v3: int] : % 30.55/4.94 | | | | | (t2tb1(all_59_5) = v2 & t2tb1(all_59_6) = v0 & length1(char, % 30.55/4.94 | | | | | v2) = v3 & length1(char, v0) = v1 & uni(v2) & uni(v0) & ( % 30.55/4.94 | | | | | ~ ($lesseq(all_59_3, $difference(v3, all_59_1))) | ~ % 30.55/4.94 | | | | | ($lesseq(all_59_4, $difference(v1, all_59_1))) | ? [v4: % 30.55/4.94 | | | | | int] : ? [v5: uni] : ? [v6: char1] : ? [v7: uni] : % 30.55/4.94 | | | | | ? [v8: char1] : ( ~ (v8 = v6) & $lesseq(1, % 30.55/4.94 | | | | | $difference(all_59_1, v4)) & $lesseq(0, v4) & % 30.55/4.94 | | | | | tb2t2(v7) = v8 & tb2t2(v5) = v6 & get2(char, v2, % 30.55/4.94 | | | | | $sum(v4, all_59_3)) = v7 & get2(char, v0, $sum(v4, % 30.55/4.94 | | | | | all_59_4)) = v5 & char1(v8) & char1(v6) & uni(v7) & % 30.55/4.94 | | | | | uni(v5)))) % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | DELTA: instantiating (124) with fresh symbols all_247_0, all_247_1, % 30.55/4.94 | | | | | all_247_2, all_247_3 gives: % 30.55/4.94 | | | | | (125) t2tb1(all_59_5) = all_247_1 & t2tb1(all_59_6) = all_247_3 & % 30.55/4.94 | | | | | length1(char, all_247_1) = all_247_0 & length1(char, % 30.55/4.94 | | | | | all_247_3) = all_247_2 & uni(all_247_1) & uni(all_247_3) & % 30.55/4.94 | | | | | ( ~ ($lesseq(all_59_3, $difference(all_247_0, all_59_1))) | % 30.55/4.94 | | | | | ~ ($lesseq(all_59_4, $difference(all_247_2, all_59_1))) | % 30.55/4.94 | | | | | ? [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] % 30.55/4.94 | | | | | : ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.55/4.94 | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & tb2t2(v3) % 30.55/4.94 | | | | | = v4 & tb2t2(v1) = v2 & get2(char, all_247_1, $sum(v0, % 30.55/4.94 | | | | | all_59_3)) = v3 & get2(char, all_247_3, $sum(v0, % 30.55/4.94 | | | | | all_59_4)) = v1 & char1(v4) & char1(v2) & uni(v3) & % 30.55/4.94 | | | | | uni(v1))) % 30.55/4.94 | | | | | % 30.55/4.94 | | | | | ALPHA: (125) implies: % 30.55/4.94 | | | | | (126) length1(char, all_247_3) = all_247_2 % 30.55/4.94 | | | | | (127) length1(char, all_247_1) = all_247_0 % 30.55/4.94 | | | | | (128) t2tb1(all_59_6) = all_247_3 % 30.55/4.94 | | | | | (129) t2tb1(all_59_5) = all_247_1 % 30.55/4.95 | | | | | (130) ~ ($lesseq(all_59_3, $difference(all_247_0, all_59_1))) | ~ % 30.55/4.95 | | | | | ($lesseq(all_59_4, $difference(all_247_2, all_59_1))) | ? % 30.55/4.95 | | | | | [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] : ? % 30.55/4.95 | | | | | [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.55/4.95 | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & tb2t2(v3) = % 30.55/4.95 | | | | | v4 & tb2t2(v1) = v2 & get2(char, all_247_1, $sum(v0, % 30.55/4.95 | | | | | all_59_3)) = v3 & get2(char, all_247_3, $sum(v0, % 30.55/4.95 | | | | | all_59_4)) = v1 & char1(v4) & char1(v2) & uni(v3) & % 30.55/4.95 | | | | | uni(v1)) % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | GROUND_INST: instantiating (6) with all_73_3, all_247_3, all_59_6, % 30.55/4.95 | | | | | simplifying with (29), (128) gives: % 30.55/4.95 | | | | | (131) all_247_3 = all_73_3 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | GROUND_INST: instantiating (6) with all_73_1, all_247_1, all_59_5, % 30.55/4.95 | | | | | simplifying with (30), (129) gives: % 30.55/4.95 | | | | | (132) all_247_1 = all_73_1 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | REDUCE: (127), (132) imply: % 30.55/4.95 | | | | | (133) length1(char, all_73_1) = all_247_0 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | REDUCE: (126), (131) imply: % 30.55/4.95 | | | | | (134) length1(char, all_73_3) = all_247_2 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | GROUND_INST: instantiating (8) with all_73_2, all_247_2, all_73_3, % 30.55/4.95 | | | | | char, simplifying with (27), (134) gives: % 30.55/4.95 | | | | | (135) all_247_2 = all_73_2 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | GROUND_INST: instantiating (8) with all_73_0, all_247_0, all_73_1, % 30.55/4.95 | | | | | char, simplifying with (28), (133) gives: % 30.55/4.95 | | | | | (136) all_247_0 = all_73_0 % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | BETA: splitting (130) gives: % 30.55/4.95 | | | | | % 30.55/4.95 | | | | | Case 1: % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | (137) $lesseq(1, $sum($difference(all_59_1, all_247_0), % 30.55/4.95 | | | | | | all_59_3)) % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | REDUCE: (136), (137) imply: % 30.55/4.95 | | | | | | (138) $lesseq(1, $sum($difference(all_59_1, all_73_0), all_59_3)) % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | COMBINE_INEQS: (26), (138) imply: % 30.55/4.95 | | | | | | (139) $lesseq(1, $difference(all_59_1, all_59_2)) % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | COMBINE_INEQS: (12), (139) imply: % 30.55/4.95 | | | | | | (140) $false % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | CLOSE: (140) is inconsistent. % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | Case 2: % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | (141) ~ ($lesseq(all_59_4, $difference(all_247_2, all_59_1))) | % 30.55/4.95 | | | | | | ? [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: uni] % 30.55/4.95 | | | | | | : ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.55/4.95 | | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & tb2t2(v3) % 30.55/4.95 | | | | | | = v4 & tb2t2(v1) = v2 & get2(char, all_247_1, $sum(v0, % 30.55/4.95 | | | | | | all_59_3)) = v3 & get2(char, all_247_3, $sum(v0, % 30.55/4.95 | | | | | | all_59_4)) = v1 & char1(v4) & char1(v2) & uni(v3) & % 30.55/4.95 | | | | | | uni(v1)) % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | BETA: splitting (141) gives: % 30.55/4.95 | | | | | | % 30.55/4.95 | | | | | | Case 1: % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | (142) $lesseq(1, $sum($difference(all_59_1, all_247_2), % 30.55/4.95 | | | | | | | all_59_4)) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | REDUCE: (135), (142) imply: % 30.55/4.95 | | | | | | | (143) $lesseq(1, $sum($difference(all_59_1, all_73_2), % 30.55/4.95 | | | | | | | all_59_4)) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | COMBINE_INEQS: (25), (143) imply: % 30.55/4.95 | | | | | | | (144) $lesseq(1, $difference(all_59_1, all_59_2)) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | COMBINE_INEQS: (12), (144) imply: % 30.55/4.95 | | | | | | | (145) $false % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | CLOSE: (145) is inconsistent. % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | Case 2: % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | (146) ? [v0: int] : ? [v1: uni] : ? [v2: char1] : ? [v3: % 30.55/4.95 | | | | | | | uni] : ? [v4: char1] : ( ~ (v4 = v2) & $lesseq(1, % 30.55/4.95 | | | | | | | $difference(all_59_1, v0)) & $lesseq(0, v0) & % 30.55/4.95 | | | | | | | tb2t2(v3) = v4 & tb2t2(v1) = v2 & get2(char, all_247_1, % 30.55/4.95 | | | | | | | $sum(v0, all_59_3)) = v3 & get2(char, all_247_3, % 30.55/4.95 | | | | | | | $sum(v0, all_59_4)) = v1 & char1(v4) & char1(v2) & % 30.55/4.95 | | | | | | | uni(v3) & uni(v1)) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | DELTA: instantiating (146) with fresh symbols all_278_0, % 30.55/4.95 | | | | | | | all_278_1, all_278_2, all_278_3, all_278_4 gives: % 30.55/4.95 | | | | | | | (147) ~ (all_278_0 = all_278_2) & $lesseq(1, % 30.55/4.95 | | | | | | | $difference(all_59_1, all_278_4)) & $lesseq(0, % 30.55/4.95 | | | | | | | all_278_4) & tb2t2(all_278_1) = all_278_0 & % 30.55/4.95 | | | | | | | tb2t2(all_278_3) = all_278_2 & get2(char, all_247_1, % 30.55/4.95 | | | | | | | $sum(all_278_4, all_59_3)) = all_278_1 & get2(char, % 30.55/4.95 | | | | | | | all_247_3, $sum(all_278_4, all_59_4)) = all_278_3 & % 30.55/4.95 | | | | | | | char1(all_278_0) & char1(all_278_2) & uni(all_278_1) & % 30.55/4.95 | | | | | | | uni(all_278_3) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | ALPHA: (147) implies: % 30.55/4.95 | | | | | | | (148) ~ (all_278_0 = all_278_2) % 30.55/4.95 | | | | | | | (149) $lesseq(0, all_278_4) % 30.55/4.95 | | | | | | | (150) $lesseq(1, $difference(all_59_1, all_278_4)) % 30.55/4.95 | | | | | | | (151) get2(char, all_247_3, $sum(all_278_4, all_59_4)) = % 30.55/4.95 | | | | | | | all_278_3 % 30.55/4.95 | | | | | | | (152) get2(char, all_247_1, $sum(all_278_4, all_59_3)) = % 30.55/4.95 | | | | | | | all_278_1 % 30.55/4.95 | | | | | | | (153) tb2t2(all_278_3) = all_278_2 % 30.55/4.95 | | | | | | | (154) tb2t2(all_278_1) = all_278_0 % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | REDUCE: (132), (152) imply: % 30.55/4.95 | | | | | | | (155) get2(char, all_73_1, $sum(all_278_4, all_59_3)) = % 30.55/4.95 | | | | | | | all_278_1 % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | REDUCE: (131), (151) imply: % 30.55/4.95 | | | | | | | (156) get2(char, all_73_3, $sum(all_278_4, all_59_4)) = % 30.55/4.95 | | | | | | | all_278_3 % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | GROUND_INST: instantiating (5) with all_59_6, all_59_5, all_59_4, % 30.55/4.95 | | | | | | | all_59_3, all_278_4, all_59_2, all_73_3, all_278_3, % 30.55/4.95 | | | | | | | simplifying with (13), (14), (15), (29), (156) gives: % 30.55/4.95 | | | | | | | (157) ~ ($lesseq(1, $difference(all_59_2, all_278_4))) | ~ % 30.55/4.95 | | | | | | | ($lesseq(0, all_278_4)) | ? [v0: char1] : ? [v1: uni] : % 30.55/4.95 | | | | | | | ? [v2: uni] : (tb2t2(v2) = v0 & tb2t2(all_278_3) = v0 & % 30.55/4.95 | | | | | | | t2tb1(all_59_5) = v1 & get2(char, v1, $sum(all_278_4, % 30.55/4.95 | | | | | | | all_59_3)) = v2 & char1(v0) & uni(v2) & uni(v1)) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_5, % 30.55/4.95 | | | | | | | $difference($sum($difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.95 | | | | | | | all_62_0), all_59_4), all_73_3, all_73_1, % 30.55/4.95 | | | | | | | all_278_3, all_122_0, simplifying with (13), (14), % 30.55/4.95 | | | | | | | (29), (30), (78), (156) gives: % 30.55/4.95 | | | | | | | (158) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.95 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.95 | | | | | | | (matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.95 | | | | | | | $difference($sum($difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | all_59_3), all_59_4), % 30.55/4.95 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.95 | | | | | | | all_59_4), 1)) = v5 & matches1(all_59_6, % 30.55/4.95 | | | | | | | all_62_0, all_59_5, % 30.55/4.95 | | | | | | | $difference($sum($difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.95 | | | | | | | all_62_0), all_59_4)) = v0 & tb2t2(all_278_3) = % 30.55/4.95 | | | | | | | v3 & tb2t2(all_122_0) = v4 & length1(char, all_73_1) = % 30.55/4.95 | | | | | | | v2 & length1(char, all_73_3) = v1 & char1(v4) & % 30.55/4.95 | | | | | | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ % 30.55/4.95 | | | | | | | ($lesseq(1, $difference(v2, all_59_3))) | ~ % 30.55/4.95 | | | | | | | ($lesseq(1, $difference($difference(v1, all_278_4), % 30.55/4.95 | | | | | | | all_59_4))))) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_6, % 30.55/4.95 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.95 | | | | | | | all_73_3, all_73_3, all_278_3, all_122_3, simplifying % 30.55/4.95 | | | | | | | with (13), (29), (79), (156) gives: % 30.55/4.95 | | | | | | | (159) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.95 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.95 | | | | | | | (matches1(all_59_6, all_62_0, all_59_6, % 30.55/4.95 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.95 | | | | | | | all_59_4), 1)) = v5 & matches1(all_59_6, % 30.55/4.95 | | | | | | | all_62_0, all_59_6, $difference(all_62_0, all_278_4), % 30.55/4.95 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4)) = % 30.55/4.95 | | | | | | | v0 & tb2t2(all_278_3) = v3 & tb2t2(all_122_3) = v4 & % 30.55/4.95 | | | | | | | length1(char, all_73_3) = v2 & length1(char, all_73_3) % 30.55/4.95 | | | | | | | = v1 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.95 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, $difference(v2, % 30.55/4.95 | | | | | | | all_59_4))) | ~ ($lesseq(1, % 30.55/4.95 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.95 | | | | | | | all_59_4))))) % 30.55/4.95 | | | | | | | % 30.55/4.95 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_6, all_62_0, % 30.55/4.95 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.95 | | | | | | | all_73_3, all_73_3, all_278_3, all_278_3, simplifying % 30.55/4.95 | | | | | | | with (13), (29), (156) gives: % 30.55/4.96 | | | | | | | (160) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_6, all_62_0, all_59_6, all_62_0, % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_4), 1)) = v5 & matches1(all_59_6, % 30.55/4.96 | | | | | | | all_62_0, all_59_6, all_62_0, % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4)) = % 30.55/4.96 | | | | | | | v0 & tb2t2(all_278_3) = v4 & tb2t2(all_278_3) = v3 & % 30.55/4.96 | | | | | | | length1(char, all_73_3) = v2 & length1(char, all_73_3) % 30.55/4.96 | | | | | | | = v1 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.96 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))) | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference($sum(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $difference(all_59_3, % 30.55/4.96 | | | | | | | all_62_0), all_73_1, all_73_3, all_122_0, % 30.55/4.96 | | | | | | | all_278_3, simplifying with (13), (14), (29), (30), % 30.55/4.96 | | | | | | | (78), (156) gives: % 30.55/4.96 | | | | | | | (161) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference($sum(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_59_3, % 30.55/4.96 | | | | | | | all_62_0), 1)) = v5 & matches1(all_59_5, % 30.55/4.96 | | | | | | | all_62_0, all_59_6, $sum($difference($sum(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $difference(all_59_3, all_62_0)) = v0 & % 30.55/4.96 | | | | | | | tb2t2(all_278_3) = v4 & tb2t2(all_122_0) = v3 & % 30.55/4.96 | | | | | | | length1(char, all_73_1) = v1 & length1(char, all_73_3) % 30.55/4.96 | | | | | | | = v2 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.96 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_6, % 30.55/4.96 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_4, % 30.55/4.96 | | | | | | | all_62_0), all_73_3, all_73_3, all_122_3, % 30.55/4.96 | | | | | | | all_278_3, simplifying with (13), (29), (79), (156) % 30.55/4.96 | | | | | | | gives: % 30.55/4.96 | | | | | | | (162) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_6, all_62_0, all_59_6, $sum(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), $sum($difference(all_59_4, all_62_0), % 30.55/4.96 | | | | | | | 1)) = v5 & matches1(all_59_6, all_62_0, all_59_6, % 30.55/4.96 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_4, % 30.55/4.96 | | | | | | | all_62_0)) = v0 & tb2t2(all_278_3) = v4 & % 30.55/4.96 | | | | | | | tb2t2(all_122_3) = v3 & length1(char, all_73_3) = v2 & % 30.55/4.96 | | | | | | | length1(char, all_73_3) = v1 & char1(v4) & char1(v3) & % 30.55/4.96 | | | | | | | ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.96 | | | | | | | all_59_4))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (31) with all_278_4, all_278_3, % 30.55/4.96 | | | | | | | simplifying with (156) gives: % 30.55/4.96 | | | | | | | (163) ~ ($lesseq(1, $difference(all_59_2, all_278_4))) | ~ % 30.55/4.96 | | | | | | | ($lesseq(0, all_278_4)) | ? [v0: char1] : ? [v1: uni] : % 30.55/4.96 | | | | | | | (tb2t2(v1) = v0 & tb2t2(all_278_3) = v0 & get2(char, % 30.55/4.96 | | | | | | | all_73_1, $sum(all_278_4, all_59_3)) = v1 & char1(v0) % 30.55/4.96 | | | | | | | & uni(v1)) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_5, % 30.55/4.96 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.96 | | | | | | | all_73_1, all_73_1, all_278_1, all_122_0, simplifying % 30.55/4.96 | | | | | | | with (14), (30), (78), (155) gives: % 30.55/4.96 | | | | | | | (164) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_5, % 30.55/4.96 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), 1)) = v5 & matches1(all_59_5, % 30.55/4.96 | | | | | | | all_62_0, all_59_5, $difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3)) = % 30.55/4.96 | | | | | | | v0 & tb2t2(all_278_1) = v3 & tb2t2(all_122_0) = v4 & % 30.55/4.96 | | | | | | | length1(char, all_73_1) = v2 & length1(char, all_73_1) % 30.55/4.96 | | | | | | | = v1 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.96 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, $difference(v2, % 30.55/4.96 | | | | | | | all_59_3))) | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_5, all_62_0, % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.96 | | | | | | | all_73_1, all_73_1, all_278_1, all_278_1, simplifying % 30.55/4.96 | | | | | | | with (14), (30), (155) gives: % 30.55/4.96 | | | | | | | (165) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_5, all_62_0, % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), 1)) = v5 & matches1(all_59_5, % 30.55/4.96 | | | | | | | all_62_0, all_59_5, all_62_0, % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3)) = % 30.55/4.96 | | | | | | | v0 & tb2t2(all_278_1) = v4 & tb2t2(all_278_1) = v3 & % 30.55/4.96 | | | | | | | length1(char, all_73_1) = v2 & length1(char, all_73_1) % 30.55/4.96 | | | | | | | = v1 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.96 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))) | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_5, % 30.55/4.96 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_3, % 30.55/4.96 | | | | | | | all_62_0), all_73_1, all_73_1, all_122_0, % 30.55/4.96 | | | | | | | all_278_1, simplifying with (14), (30), (78), (155) % 30.55/4.96 | | | | | | | gives: % 30.55/4.96 | | | | | | | (166) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_5, $sum(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), $sum($difference(all_59_3, all_62_0), % 30.55/4.96 | | | | | | | 1)) = v5 & matches1(all_59_5, all_62_0, all_59_5, % 30.55/4.96 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_3, % 30.55/4.96 | | | | | | | all_62_0)) = v0 & tb2t2(all_278_1) = v4 & % 30.55/4.96 | | | | | | | tb2t2(all_122_0) = v3 & length1(char, all_73_1) = v2 & % 30.55/4.96 | | | | | | | length1(char, all_73_1) = v1 & char1(v4) & char1(v3) & % 30.55/4.96 | | | | | | | ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_5, % 30.55/4.96 | | | | | | | $difference($sum($sum(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $difference(all_59_4, % 30.55/4.96 | | | | | | | all_62_0), all_73_3, all_73_1, all_122_3, % 30.55/4.96 | | | | | | | all_278_1, simplifying with (13), (14), (29), (30), % 30.55/4.96 | | | | | | | (79), (155) gives: % 30.55/4.96 | | | | | | | (167) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.96 | | | | | | | $difference($sum($sum(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_59_4, % 30.55/4.96 | | | | | | | all_62_0), 1)) = v5 & matches1(all_59_6, % 30.55/4.96 | | | | | | | all_62_0, all_59_5, $difference($sum($sum(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $difference(all_59_4, all_62_0)) = v0 & % 30.55/4.96 | | | | | | | tb2t2(all_278_1) = v4 & tb2t2(all_122_3) = v3 & % 30.55/4.96 | | | | | | | length1(char, all_73_1) = v2 & length1(char, all_73_3) % 30.55/4.96 | | | | | | | = v1 & char1(v4) & char1(v3) & ( ~ (v4 = v3) | ~ (v0 = % 30.55/4.96 | | | | | | | 0) | v5 = 0 | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))) | ~ ($lesseq(1, $difference(v1, % 30.55/4.96 | | | | | | | all_59_4))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_6, all_59_5, % 30.55/4.96 | | | | | | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.96 | | | | | | | all_73_3, all_73_1, all_278_3, all_278_1, simplifying % 30.55/4.96 | | | | | | | with (13), (14), (29), (30), (155), (156) gives: % 30.55/4.96 | | | | | | | (168) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.96 | | | | | | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_4), 1)) = v5 & matches1(all_59_6, % 30.55/4.96 | | | | | | | all_62_0, all_59_5, $difference($sum(all_62_0, % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_4)) = v0 & tb2t2(all_278_1) = % 30.55/4.96 | | | | | | | v4 & tb2t2(all_278_3) = v3 & length1(char, all_73_1) = % 30.55/4.96 | | | | | | | v2 & length1(char, all_73_3) = v1 & char1(v4) & % 30.55/4.96 | | | | | | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ % 30.55/4.96 | | | | | | | ($lesseq(1, $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))) | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference($difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_3), all_73_1, all_73_3, % 30.55/4.96 | | | | | | | all_278_1, all_122_3, simplifying with (13), (14), % 30.55/4.96 | | | | | | | (29), (30), (79), (155) gives: % 30.55/4.96 | | | | | | | (169) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference($difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), 1)) = v5 & matches1(all_59_5, % 30.55/4.96 | | | | | | | all_62_0, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference($difference(all_62_0, all_278_4), % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_3)) = v0 & tb2t2(all_278_1) = % 30.55/4.96 | | | | | | | v3 & tb2t2(all_122_3) = v4 & length1(char, all_73_1) = % 30.55/4.96 | | | | | | | v1 & length1(char, all_73_3) = v2 & char1(v4) & % 30.55/4.96 | | | | | | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ % 30.55/4.96 | | | | | | | ($lesseq(1, $difference(v2, all_59_4))) | ~ % 30.55/4.96 | | | | | | | ($lesseq(1, $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | GROUND_INST: instantiating (17) with all_59_5, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.96 | | | | | | | all_73_1, all_73_3, all_278_1, all_278_3, simplifying % 30.55/4.96 | | | | | | | with (13), (14), (29), (30), (155), (156) gives: % 30.55/4.96 | | | | | | | (170) ? [v0: any] : ? [v1: int] : ? [v2: int] : ? [v3: % 30.55/4.96 | | | | | | | char1] : ? [v4: char1] : ? [v5: any] : % 30.55/4.96 | | | | | | | (matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.96 | | | | | | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.96 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), % 30.55/4.96 | | | | | | | all_59_3), 1)) = v5 & matches1(all_59_5, % 30.55/4.96 | | | | | | | all_62_0, all_59_6, $sum($difference(all_62_0, % 30.55/4.96 | | | | | | | all_59_3), all_59_4), $sum($difference(all_278_4, % 30.55/4.96 | | | | | | | all_62_0), all_59_3)) = v0 & tb2t2(all_278_1) = % 30.55/4.96 | | | | | | | v3 & tb2t2(all_278_3) = v4 & length1(char, all_73_1) = % 30.55/4.96 | | | | | | | v1 & length1(char, all_73_3) = v2 & char1(v4) & % 30.55/4.96 | | | | | | | char1(v3) & ( ~ (v4 = v3) | ~ (v0 = 0) | v5 = 0 | ~ % 30.55/4.96 | | | | | | | ($lesseq(1, $difference($difference(v2, all_278_4), % 30.55/4.96 | | | | | | | all_59_4))) | ~ ($lesseq(1, % 30.55/4.96 | | | | | | | $difference($difference(v1, all_278_4), % 30.55/4.96 | | | | | | | all_59_3))))) % 30.55/4.96 | | | | | | | % 30.55/4.96 | | | | | | | DELTA: instantiating (170) with fresh symbols all_288_0, % 30.55/4.96 | | | | | | | all_288_1, all_288_2, all_288_3, all_288_4, all_288_5 % 30.55/4.96 | | | | | | | gives: % 30.55/4.97 | | | | | | | (171) matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $sum($difference(all_62_0, all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | 1)) = all_288_0 & matches1(all_59_5, all_62_0, % 30.55/4.97 | | | | | | | all_59_6, $sum($difference(all_62_0, all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $sum($difference(all_278_4, all_62_0), % 30.55/4.97 | | | | | | | all_59_3)) = all_288_5 & tb2t2(all_278_1) = all_288_2 % 30.55/4.97 | | | | | | | & tb2t2(all_278_3) = all_288_1 & length1(char, all_73_1) % 30.55/4.97 | | | | | | | = all_288_4 & length1(char, all_73_3) = all_288_3 & % 30.55/4.97 | | | | | | | char1(all_288_1) & char1(all_288_2) & ( ~ (all_288_1 = % 30.55/4.97 | | | | | | | all_288_2) | ~ (all_288_5 = 0) | all_288_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_288_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_4))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_288_4, all_278_4), % 30.55/4.97 | | | | | | | all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (171) implies: % 30.55/4.97 | | | | | | | (172) tb2t2(all_278_3) = all_288_1 % 30.55/4.97 | | | | | | | (173) tb2t2(all_278_1) = all_288_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (168) with fresh symbols all_290_0, % 30.55/4.97 | | | | | | | all_290_1, all_290_2, all_290_3, all_290_4, all_290_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (174) matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $difference($sum(all_62_0, all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.97 | | | | | | | 1)) = all_290_0 & matches1(all_59_6, all_62_0, % 30.55/4.97 | | | | | | | all_59_5, $difference($sum(all_62_0, all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $sum($difference(all_278_4, all_62_0), % 30.55/4.97 | | | | | | | all_59_4)) = all_290_5 & tb2t2(all_278_1) = all_290_1 % 30.55/4.97 | | | | | | | & tb2t2(all_278_3) = all_290_2 & length1(char, all_73_1) % 30.55/4.97 | | | | | | | = all_290_3 & length1(char, all_73_3) = all_290_4 & % 30.55/4.97 | | | | | | | char1(all_290_1) & char1(all_290_2) & ( ~ (all_290_1 = % 30.55/4.97 | | | | | | | all_290_2) | ~ (all_290_5 = 0) | all_290_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_290_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_3))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_290_4, all_278_4), % 30.55/4.97 | | | | | | | all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (174) implies: % 30.55/4.97 | | | | | | | (175) tb2t2(all_278_3) = all_290_2 % 30.55/4.97 | | | | | | | (176) tb2t2(all_278_1) = all_290_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (162) with fresh symbols all_292_0, % 30.55/4.97 | | | | | | | all_292_1, all_292_2, all_292_3, all_292_4, all_292_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (177) matches1(all_59_6, all_62_0, all_59_6, $sum(all_278_4, % 30.55/4.97 | | | | | | | all_62_0), $sum($difference(all_59_4, all_62_0), 1)) % 30.55/4.97 | | | | | | | = all_292_0 & matches1(all_59_6, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_4, % 30.55/4.97 | | | | | | | all_62_0)) = all_292_5 & tb2t2(all_278_3) = all_292_1 % 30.55/4.97 | | | | | | | & tb2t2(all_122_3) = all_292_2 & length1(char, all_73_3) % 30.55/4.97 | | | | | | | = all_292_3 & length1(char, all_73_3) = all_292_4 & % 30.55/4.97 | | | | | | | char1(all_292_1) & char1(all_292_2) & ( ~ (all_292_1 = % 30.55/4.97 | | | | | | | all_292_2) | ~ (all_292_5 = 0) | all_292_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_292_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_4))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference(all_292_4, all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (177) implies: % 30.55/4.97 | | | | | | | (178) tb2t2(all_278_3) = all_292_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (161) with fresh symbols all_294_0, % 30.55/4.97 | | | | | | | all_294_1, all_294_2, all_294_3, all_294_4, all_294_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (179) matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $sum($difference($sum(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $sum($difference(all_59_3, all_62_0), 1)) % 30.55/4.97 | | | | | | | = all_294_0 & matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $sum($difference($sum(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $difference(all_59_3, all_62_0)) = % 30.55/4.97 | | | | | | | all_294_5 & tb2t2(all_278_3) = all_294_1 & % 30.55/4.97 | | | | | | | tb2t2(all_122_0) = all_294_2 & length1(char, all_73_1) = % 30.55/4.97 | | | | | | | all_294_4 & length1(char, all_73_3) = all_294_3 & % 30.55/4.97 | | | | | | | char1(all_294_1) & char1(all_294_2) & ( ~ (all_294_1 = % 30.55/4.97 | | | | | | | all_294_2) | ~ (all_294_5 = 0) | all_294_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_294_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_4))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference(all_294_4, all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (179) implies: % 30.55/4.97 | | | | | | | (180) tb2t2(all_278_3) = all_294_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (167) with fresh symbols all_296_0, % 30.55/4.97 | | | | | | | all_296_1, all_296_2, all_296_3, all_296_4, all_296_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (181) matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $difference($sum($sum(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $sum($difference(all_59_4, all_62_0), 1)) % 30.55/4.97 | | | | | | | = all_296_0 & matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $difference($sum($sum(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | all_59_4), $difference(all_59_4, all_62_0)) = % 30.55/4.97 | | | | | | | all_296_5 & tb2t2(all_278_1) = all_296_1 & % 30.55/4.97 | | | | | | | tb2t2(all_122_3) = all_296_2 & length1(char, all_73_1) = % 30.55/4.97 | | | | | | | all_296_3 & length1(char, all_73_3) = all_296_4 & % 30.55/4.97 | | | | | | | char1(all_296_1) & char1(all_296_2) & ( ~ (all_296_1 = % 30.55/4.97 | | | | | | | all_296_2) | ~ (all_296_5 = 0) | all_296_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_296_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_3))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference(all_296_4, all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (181) implies: % 30.55/4.97 | | | | | | | (182) tb2t2(all_278_1) = all_296_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (158) with fresh symbols all_298_0, % 30.55/4.97 | | | | | | | all_298_1, all_298_2, all_298_3, all_298_4, all_298_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (183) matches1(all_59_6, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $difference($sum($difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.97 | | | | | | | 1)) = all_298_0 & matches1(all_59_6, all_62_0, % 30.55/4.97 | | | | | | | all_59_5, $difference($sum($difference(all_62_0, % 30.55/4.97 | | | | | | | all_278_4), all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4)) = % 30.55/4.97 | | | | | | | all_298_5 & tb2t2(all_278_3) = all_298_2 & % 30.55/4.97 | | | | | | | tb2t2(all_122_0) = all_298_1 & length1(char, all_73_1) = % 30.55/4.97 | | | | | | | all_298_3 & length1(char, all_73_3) = all_298_4 & % 30.55/4.97 | | | | | | | char1(all_298_1) & char1(all_298_2) & ( ~ (all_298_1 = % 30.55/4.97 | | | | | | | all_298_2) | ~ (all_298_5 = 0) | all_298_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference(all_298_3, all_59_3))) | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_298_4, % 30.55/4.97 | | | | | | | all_278_4), all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (183) implies: % 30.55/4.97 | | | | | | | (184) tb2t2(all_278_3) = all_298_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (160) with fresh symbols all_300_0, % 30.55/4.97 | | | | | | | all_300_1, all_300_2, all_300_3, all_300_4, all_300_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (185) matches1(all_59_6, all_62_0, all_59_6, all_62_0, % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.97 | | | | | | | 1)) = all_300_0 & matches1(all_59_6, all_62_0, % 30.55/4.97 | | | | | | | all_59_6, all_62_0, $sum($difference(all_278_4, % 30.55/4.97 | | | | | | | all_62_0), all_59_4)) = all_300_5 & % 30.55/4.97 | | | | | | | tb2t2(all_278_3) = all_300_1 & tb2t2(all_278_3) = % 30.55/4.97 | | | | | | | all_300_2 & length1(char, all_73_3) = all_300_3 & % 30.55/4.97 | | | | | | | length1(char, all_73_3) = all_300_4 & char1(all_300_1) & % 30.55/4.97 | | | | | | | char1(all_300_2) & ( ~ (all_300_1 = all_300_2) | ~ % 30.55/4.97 | | | | | | | (all_300_5 = 0) | all_300_0 = 0 | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_300_3, all_278_4), % 30.55/4.97 | | | | | | | all_59_4))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_300_4, all_278_4), % 30.55/4.97 | | | | | | | all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (185) implies: % 30.55/4.97 | | | | | | | (186) tb2t2(all_278_3) = all_300_2 % 30.55/4.97 | | | | | | | (187) tb2t2(all_278_3) = all_300_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (159) with fresh symbols all_302_0, % 30.55/4.97 | | | | | | | all_302_1, all_302_2, all_302_3, all_302_4, all_302_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (188) matches1(all_59_6, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_4), % 30.55/4.97 | | | | | | | 1)) = all_302_0 & matches1(all_59_6, all_62_0, % 30.55/4.97 | | | | | | | all_59_6, $difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_4)) = % 30.55/4.97 | | | | | | | all_302_5 & tb2t2(all_278_3) = all_302_2 & % 30.55/4.97 | | | | | | | tb2t2(all_122_3) = all_302_1 & length1(char, all_73_3) = % 30.55/4.97 | | | | | | | all_302_3 & length1(char, all_73_3) = all_302_4 & % 30.55/4.97 | | | | | | | char1(all_302_1) & char1(all_302_2) & ( ~ (all_302_1 = % 30.55/4.97 | | | | | | | all_302_2) | ~ (all_302_5 = 0) | all_302_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference(all_302_3, all_59_4))) | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_302_4, % 30.55/4.97 | | | | | | | all_278_4), all_59_4)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (188) implies: % 30.55/4.97 | | | | | | | (189) tb2t2(all_278_3) = all_302_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (169) with fresh symbols all_304_0, % 30.55/4.97 | | | | | | | all_304_1, all_304_2, all_304_3, all_304_4, all_304_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (190) matches1(all_59_5, all_62_0, all_59_6, % 30.55/4.97 | | | | | | | $sum($difference($difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | 1)) = all_304_0 & matches1(all_59_5, all_62_0, % 30.55/4.97 | | | | | | | all_59_6, $sum($difference($difference(all_62_0, % 30.55/4.97 | | | | | | | all_278_4), all_59_3), all_59_4), % 30.55/4.97 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3)) = % 30.55/4.97 | | | | | | | all_304_5 & tb2t2(all_278_1) = all_304_2 & % 30.55/4.97 | | | | | | | tb2t2(all_122_3) = all_304_1 & length1(char, all_73_1) = % 30.55/4.97 | | | | | | | all_304_4 & length1(char, all_73_3) = all_304_3 & % 30.55/4.97 | | | | | | | char1(all_304_1) & char1(all_304_2) & ( ~ (all_304_1 = % 30.55/4.97 | | | | | | | all_304_2) | ~ (all_304_5 = 0) | all_304_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference(all_304_3, all_59_4))) | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_304_4, % 30.55/4.97 | | | | | | | all_278_4), all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (190) implies: % 30.55/4.97 | | | | | | | (191) tb2t2(all_278_1) = all_304_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (166) with fresh symbols all_306_0, % 30.55/4.97 | | | | | | | all_306_1, all_306_2, all_306_3, all_306_4, all_306_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (192) matches1(all_59_5, all_62_0, all_59_5, $sum(all_278_4, % 30.55/4.97 | | | | | | | all_62_0), $sum($difference(all_59_3, all_62_0), 1)) % 30.55/4.97 | | | | | | | = all_306_0 & matches1(all_59_5, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $sum(all_278_4, all_62_0), $difference(all_59_3, % 30.55/4.97 | | | | | | | all_62_0)) = all_306_5 & tb2t2(all_278_1) = all_306_1 % 30.55/4.97 | | | | | | | & tb2t2(all_122_0) = all_306_2 & length1(char, all_73_1) % 30.55/4.97 | | | | | | | = all_306_3 & length1(char, all_73_1) = all_306_4 & % 30.55/4.97 | | | | | | | char1(all_306_1) & char1(all_306_2) & ( ~ (all_306_1 = % 30.55/4.97 | | | | | | | all_306_2) | ~ (all_306_5 = 0) | all_306_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_306_3, % 30.55/4.97 | | | | | | | all_278_4), all_59_3))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference(all_306_4, all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (192) implies: % 30.55/4.97 | | | | | | | (193) tb2t2(all_278_1) = all_306_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (165) with fresh symbols all_308_0, % 30.55/4.97 | | | | | | | all_308_1, all_308_2, all_308_3, all_308_4, all_308_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (194) matches1(all_59_5, all_62_0, all_59_5, all_62_0, % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | 1)) = all_308_0 & matches1(all_59_5, all_62_0, % 30.55/4.97 | | | | | | | all_59_5, all_62_0, $sum($difference(all_278_4, % 30.55/4.97 | | | | | | | all_62_0), all_59_3)) = all_308_5 & % 30.55/4.97 | | | | | | | tb2t2(all_278_1) = all_308_1 & tb2t2(all_278_1) = % 30.55/4.97 | | | | | | | all_308_2 & length1(char, all_73_1) = all_308_3 & % 30.55/4.97 | | | | | | | length1(char, all_73_1) = all_308_4 & char1(all_308_1) & % 30.55/4.97 | | | | | | | char1(all_308_2) & ( ~ (all_308_1 = all_308_2) | ~ % 30.55/4.97 | | | | | | | (all_308_5 = 0) | all_308_0 = 0 | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_308_3, all_278_4), % 30.55/4.97 | | | | | | | all_59_3))) | ~ ($lesseq(1, % 30.55/4.97 | | | | | | | $difference($difference(all_308_4, all_278_4), % 30.55/4.97 | | | | | | | all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (194) implies: % 30.55/4.97 | | | | | | | (195) tb2t2(all_278_1) = all_308_2 % 30.55/4.97 | | | | | | | (196) tb2t2(all_278_1) = all_308_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | DELTA: instantiating (164) with fresh symbols all_310_0, % 30.55/4.97 | | | | | | | all_310_1, all_310_2, all_310_3, all_310_4, all_310_5 % 30.55/4.97 | | | | | | | gives: % 30.55/4.97 | | | | | | | (197) matches1(all_59_5, all_62_0, all_59_5, % 30.55/4.97 | | | | | | | $difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | $sum($sum($difference(all_278_4, all_62_0), all_59_3), % 30.55/4.97 | | | | | | | 1)) = all_310_0 & matches1(all_59_5, all_62_0, % 30.55/4.97 | | | | | | | all_59_5, $difference(all_62_0, all_278_4), % 30.55/4.97 | | | | | | | $sum($difference(all_278_4, all_62_0), all_59_3)) = % 30.55/4.97 | | | | | | | all_310_5 & tb2t2(all_278_1) = all_310_2 & % 30.55/4.97 | | | | | | | tb2t2(all_122_0) = all_310_1 & length1(char, all_73_1) = % 30.55/4.97 | | | | | | | all_310_3 & length1(char, all_73_1) = all_310_4 & % 30.55/4.97 | | | | | | | char1(all_310_1) & char1(all_310_2) & ( ~ (all_310_1 = % 30.55/4.97 | | | | | | | all_310_2) | ~ (all_310_5 = 0) | all_310_0 = 0 | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference(all_310_3, all_59_3))) | ~ % 30.55/4.97 | | | | | | | ($lesseq(1, $difference($difference(all_310_4, % 30.55/4.97 | | | | | | | all_278_4), all_59_3)))) % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | ALPHA: (197) implies: % 30.55/4.97 | | | | | | | (198) tb2t2(all_278_1) = all_310_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_278_2, all_294_1, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (153), (180) gives: % 30.55/4.97 | | | | | | | (199) all_294_1 = all_278_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_292_1, all_294_1, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (178), (180) gives: % 30.55/4.97 | | | | | | | (200) all_294_1 = all_292_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_292_1, all_298_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (178), (184) gives: % 30.55/4.97 | | | | | | | (201) all_298_2 = all_292_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_288_1, all_298_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (172), (184) gives: % 30.55/4.97 | | | | | | | (202) all_298_2 = all_288_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_294_1, all_300_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (180), (186) gives: % 30.55/4.97 | | | | | | | (203) all_300_2 = all_294_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_300_1, all_302_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (187), (189) gives: % 30.55/4.97 | | | | | | | (204) all_302_2 = all_300_1 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_300_2, all_302_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (186), (189) gives: % 30.55/4.97 | | | | | | | (205) all_302_2 = all_300_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_290_2, all_302_2, % 30.55/4.97 | | | | | | | all_278_3, simplifying with (175), (189) gives: % 30.55/4.97 | | | | | | | (206) all_302_2 = all_290_2 % 30.55/4.97 | | | | | | | % 30.55/4.97 | | | | | | | GROUND_INST: instantiating (7) with all_278_0, all_296_1, % 30.55/4.97 | | | | | | | all_278_1, simplifying with (154), (182) gives: % 30.55/4.98 | | | | | | | (207) all_296_1 = all_278_0 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_296_1, all_304_2, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (182), (191) gives: % 30.55/4.98 | | | | | | | (208) all_304_2 = all_296_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_296_1, all_306_1, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (182), (193) gives: % 30.55/4.98 | | | | | | | (209) all_306_1 = all_296_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_306_1, all_308_2, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (193), (195) gives: % 30.55/4.98 | | | | | | | (210) all_308_2 = all_306_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_290_1, all_308_2, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (176), (195) gives: % 30.55/4.98 | | | | | | | (211) all_308_2 = all_290_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_304_2, all_308_1, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (191), (196) gives: % 30.55/4.98 | | | | | | | (212) all_308_1 = all_304_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_308_1, all_310_2, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (196), (198) gives: % 30.55/4.98 | | | | | | | (213) all_310_2 = all_308_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | GROUND_INST: instantiating (7) with all_288_2, all_310_2, % 30.55/4.98 | | | | | | | all_278_1, simplifying with (173), (198) gives: % 30.55/4.98 | | | | | | | (214) all_310_2 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (213), (214) imply: % 30.55/4.98 | | | | | | | (215) all_308_1 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (215) implies: % 30.55/4.98 | | | | | | | (216) all_308_1 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (212), (216) imply: % 30.55/4.98 | | | | | | | (217) all_304_2 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (217) implies: % 30.55/4.98 | | | | | | | (218) all_304_2 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (210), (211) imply: % 30.55/4.98 | | | | | | | (219) all_306_1 = all_290_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (219) implies: % 30.55/4.98 | | | | | | | (220) all_306_1 = all_290_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (209), (220) imply: % 30.55/4.98 | | | | | | | (221) all_296_1 = all_290_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (221) implies: % 30.55/4.98 | | | | | | | (222) all_296_1 = all_290_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (208), (218) imply: % 30.55/4.98 | | | | | | | (223) all_296_1 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (223) implies: % 30.55/4.98 | | | | | | | (224) all_296_1 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (204), (205) imply: % 30.55/4.98 | | | | | | | (225) all_300_1 = all_300_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (204), (206) imply: % 30.55/4.98 | | | | | | | (226) all_300_1 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (225), (226) imply: % 30.55/4.98 | | | | | | | (227) all_300_2 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (227) implies: % 30.55/4.98 | | | | | | | (228) all_300_2 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (203), (228) imply: % 30.55/4.98 | | | | | | | (229) all_294_1 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (229) implies: % 30.55/4.98 | | | | | | | (230) all_294_1 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (201), (202) imply: % 30.55/4.98 | | | | | | | (231) all_292_1 = all_288_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (231) implies: % 30.55/4.98 | | | | | | | (232) all_292_1 = all_288_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (207), (222) imply: % 30.55/4.98 | | | | | | | (233) all_290_1 = all_278_0 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (222), (224) imply: % 30.55/4.98 | | | | | | | (234) all_290_1 = all_288_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (199), (230) imply: % 30.55/4.98 | | | | | | | (235) all_290_2 = all_278_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (200), (230) imply: % 30.55/4.98 | | | | | | | (236) all_292_1 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (236) implies: % 30.55/4.98 | | | | | | | (237) all_292_1 = all_290_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (232), (237) imply: % 30.55/4.98 | | | | | | | (238) all_290_2 = all_288_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | SIMP: (238) implies: % 30.55/4.98 | | | | | | | (239) all_290_2 = all_288_1 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (233), (234) imply: % 30.55/4.98 | | | | | | | (240) all_288_2 = all_278_0 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | COMBINE_EQS: (235), (239) imply: % 30.55/4.98 | | | | | | | (241) all_288_1 = all_278_2 % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | BETA: splitting (157) gives: % 30.55/4.98 | | | | | | | % 30.55/4.98 | | | | | | | Case 1: % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | (242) $lesseq(all_278_4, -1) % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | COMBINE_INEQS: (149), (242) imply: % 30.55/4.98 | | | | | | | | (243) $false % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | CLOSE: (243) is inconsistent. % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | Case 2: % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | (244) ~ ($lesseq(1, $difference(all_59_2, all_278_4))) | ? % 30.55/4.98 | | | | | | | | [v0: char1] : ? [v1: uni] : ? [v2: uni] : (tb2t2(v2) % 30.55/4.98 | | | | | | | | = v0 & tb2t2(all_278_3) = v0 & t2tb1(all_59_5) = v1 & % 30.55/4.98 | | | | | | | | get2(char, v1, $sum(all_278_4, all_59_3)) = v2 & % 30.55/4.98 | | | | | | | | char1(v0) & uni(v2) & uni(v1)) % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | BETA: splitting (244) gives: % 30.55/4.98 | | | | | | | | % 30.55/4.98 | | | | | | | | Case 1: % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | (245) $lesseq(all_59_2, all_278_4) % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | COMBINE_INEQS: (150), (245) imply: % 30.55/4.98 | | | | | | | | | (246) $lesseq(1, $difference(all_59_1, all_59_2)) % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | COMBINE_INEQS: (12), (246) imply: % 30.55/4.98 | | | | | | | | | (247) $false % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | CLOSE: (247) is inconsistent. % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | Case 2: % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | (248) $lesseq(1, $difference(all_59_2, all_278_4)) % 30.55/4.98 | | | | | | | | | (249) ? [v0: char1] : ? [v1: uni] : ? [v2: uni] : % 30.55/4.98 | | | | | | | | | (tb2t2(v2) = v0 & tb2t2(all_278_3) = v0 & % 30.55/4.98 | | | | | | | | | t2tb1(all_59_5) = v1 & get2(char, v1, % 30.55/4.98 | | | | | | | | | $sum(all_278_4, all_59_3)) = v2 & char1(v0) & % 30.55/4.98 | | | | | | | | | uni(v2) & uni(v1)) % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | DELTA: instantiating (249) with fresh symbols all_327_0, % 30.55/4.98 | | | | | | | | | all_327_1, all_327_2 gives: % 30.55/4.98 | | | | | | | | | (250) tb2t2(all_327_0) = all_327_2 & tb2t2(all_278_3) = % 30.55/4.98 | | | | | | | | | all_327_2 & t2tb1(all_59_5) = all_327_1 & get2(char, % 30.55/4.98 | | | | | | | | | all_327_1, $sum(all_278_4, all_59_3)) = all_327_0 & % 30.55/4.98 | | | | | | | | | char1(all_327_2) & uni(all_327_0) & uni(all_327_1) % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | ALPHA: (250) implies: % 30.55/4.98 | | | | | | | | | (251) tb2t2(all_278_3) = all_327_2 % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | BETA: splitting (163) gives: % 30.55/4.98 | | | | | | | | | % 30.55/4.98 | | | | | | | | | Case 1: % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | (252) $lesseq(all_278_4, -1) % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | COMBINE_INEQS: (149), (252) imply: % 30.55/4.98 | | | | | | | | | | (253) $false % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | CLOSE: (253) is inconsistent. % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | Case 2: % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | (254) ~ ($lesseq(1, $difference(all_59_2, all_278_4))) | % 30.55/4.98 | | | | | | | | | | ? [v0: char1] : ? [v1: uni] : (tb2t2(v1) = v0 & % 30.55/4.98 | | | | | | | | | | tb2t2(all_278_3) = v0 & get2(char, all_73_1, % 30.55/4.98 | | | | | | | | | | $sum(all_278_4, all_59_3)) = v1 & char1(v0) & % 30.55/4.98 | | | | | | | | | | uni(v1)) % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | BETA: splitting (254) gives: % 30.55/4.98 | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | Case 1: % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | (255) $lesseq(all_59_2, all_278_4) % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | COMBINE_INEQS: (248), (255) imply: % 30.55/4.98 | | | | | | | | | | | (256) $false % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | CLOSE: (256) is inconsistent. % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | Case 2: % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | (257) ? [v0: char1] : ? [v1: uni] : (tb2t2(v1) = v0 & % 30.55/4.98 | | | | | | | | | | | tb2t2(all_278_3) = v0 & get2(char, all_73_1, % 30.55/4.98 | | | | | | | | | | | $sum(all_278_4, all_59_3)) = v1 & char1(v0) & % 30.55/4.98 | | | | | | | | | | | uni(v1)) % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | DELTA: instantiating (257) with fresh symbols all_339_0, % 30.55/4.98 | | | | | | | | | | | all_339_1 gives: % 30.55/4.98 | | | | | | | | | | | (258) tb2t2(all_339_0) = all_339_1 & tb2t2(all_278_3) = % 30.55/4.98 | | | | | | | | | | | all_339_1 & get2(char, all_73_1, $sum(all_278_4, % 30.55/4.98 | | | | | | | | | | | all_59_3)) = all_339_0 & char1(all_339_1) & % 30.55/4.98 | | | | | | | | | | | uni(all_339_0) % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | ALPHA: (258) implies: % 30.55/4.98 | | | | | | | | | | | (259) get2(char, all_73_1, $sum(all_278_4, all_59_3)) = % 30.55/4.98 | | | | | | | | | | | all_339_0 % 30.55/4.98 | | | | | | | | | | | (260) tb2t2(all_278_3) = all_339_1 % 30.55/4.98 | | | | | | | | | | | (261) tb2t2(all_339_0) = all_339_1 % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | GROUND_INST: instantiating (9) with all_278_1, all_339_0, % 30.55/4.98 | | | | | | | | | | | $sum(all_278_4, all_59_3), all_73_1, char, % 30.55/4.98 | | | | | | | | | | | simplifying with (155), (259) gives: % 30.55/4.98 | | | | | | | | | | | (262) all_339_0 = all_278_1 % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_278_2, all_339_1, % 30.55/4.98 | | | | | | | | | | | all_278_3, simplifying with (153), (260) gives: % 30.55/4.98 | | | | | | | | | | | (263) all_339_1 = all_278_2 % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_327_2, all_339_1, % 30.55/4.98 | | | | | | | | | | | all_278_3, simplifying with (251), (260) gives: % 30.55/4.98 | | | | | | | | | | | (264) all_339_1 = all_327_2 % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | COMBINE_EQS: (263), (264) imply: % 30.55/4.98 | | | | | | | | | | | (265) all_327_2 = all_278_2 % 30.55/4.98 | | | | | | | | | | | % 30.55/4.98 | | | | | | | | | | | REDUCE: (261), (262), (263) imply: % 30.55/4.98 | | | | | | | | | | | (266) tb2t2(all_278_1) = all_278_2 % 30.55/4.99 | | | | | | | | | | | % 30.55/4.99 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_278_0, all_278_2, % 30.55/4.99 | | | | | | | | | | | all_278_1, simplifying with (154), (266) gives: % 30.55/4.99 | | | | | | | | | | | (267) all_278_0 = all_278_2 % 30.55/4.99 | | | | | | | | | | | % 30.55/4.99 | | | | | | | | | | | REDUCE: (148), (267) imply: % 30.55/4.99 | | | | | | | | | | | (268) $false % 30.55/4.99 | | | | | | | | | | | % 30.55/4.99 | | | | | | | | | | | CLOSE: (268) is inconsistent. % 30.55/4.99 | | | | | | | | | | | % 30.55/4.99 | | | | | | | | | | End of split % 30.55/4.99 | | | | | | | | | | % 30.55/4.99 | | | | | | | | | End of split % 30.55/4.99 | | | | | | | | | % 30.55/4.99 | | | | | | | | End of split % 30.55/4.99 | | | | | | | | % 30.55/4.99 | | | | | | | End of split % 30.55/4.99 | | | | | | | % 30.55/4.99 | | | | | | End of split % 30.55/4.99 | | | | | | % 30.55/4.99 | | | | | End of split % 30.55/4.99 | | | | | % 30.55/4.99 | | | | End of split % 30.55/4.99 | | | | % 30.55/4.99 | | | End of split % 30.55/4.99 | | | % 30.55/4.99 | | End of split % 30.55/4.99 | | % 30.55/4.99 | End of split % 30.55/4.99 | % 30.55/4.99 End of proof % 30.55/4.99 % SZS output end Proof for theBenchmark % 30.55/4.99 % 30.55/4.99 4371ms %------------------------------------------------------------------------------