%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW591_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 : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:49 EDT 2023 % Result : Theorem 61.57s 8.71s % Output : Proof 79.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWW591_2 : TPTP v8.1.2. Released v6.1.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 21:27:11 EDT 2023 % 0.13/0.35 % CPUTime : % 0.61/0.61 ________ _____ % 0.61/0.61 ___ __ \_________(_)________________________________ % 0.61/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.61/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.61/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.61/0.61 % 0.61/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.61/0.61 (2023-06-19) % 0.61/0.61 % 0.61/0.61 (c) Philipp Rümmer, 2009-2023 % 0.61/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.61/0.61 Amanda Stjerna. % 0.61/0.61 Free software under BSD-3-Clause. % 0.61/0.61 % 0.61/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.61/0.61 % 0.61/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.61/0.62 Running up to 7 provers in parallel. % 0.61/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.61/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.61/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.61/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.61/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.61/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.61/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.91/1.15 Prover 3: Preprocessing ... % 2.91/1.15 Prover 1: Preprocessing ... % 2.91/1.15 Prover 2: Preprocessing ... % 2.91/1.15 Prover 5: Preprocessing ... % 2.91/1.15 Prover 0: Preprocessing ... % 2.91/1.15 Prover 4: Preprocessing ... % 2.91/1.15 Prover 6: Preprocessing ... % 7.51/1.72 Prover 1: Warning: ignoring some quantifiers % 7.51/1.74 Prover 3: Warning: ignoring some quantifiers % 7.51/1.74 Prover 4: Warning: ignoring some quantifiers % 7.51/1.75 Prover 6: Proving ... % 7.51/1.76 Prover 1: Constructing countermodel ... % 7.51/1.77 Prover 5: Proving ... % 7.98/1.78 Prover 4: Constructing countermodel ... % 7.98/1.78 Prover 3: Constructing countermodel ... % 7.98/1.79 Prover 0: Proving ... % 7.98/1.83 Prover 2: Proving ... % 61.57/8.70 Prover 2: proved (8047ms) % 61.57/8.71 % 61.57/8.71 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.57/8.71 % 61.57/8.72 Prover 3: stopped % 61.57/8.72 Prover 0: stopped % 61.57/8.72 Prover 5: stopped % 62.27/8.73 Prover 6: stopped % 62.27/8.74 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 62.27/8.74 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 62.27/8.74 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 62.27/8.74 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 62.27/8.75 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 62.77/8.79 Prover 11: Preprocessing ... % 62.77/8.79 Prover 10: Preprocessing ... % 62.77/8.81 Prover 8: Preprocessing ... % 62.77/8.82 Prover 7: Preprocessing ... % 62.77/8.83 Prover 13: Preprocessing ... % 63.36/8.89 Prover 7: Warning: ignoring some quantifiers % 63.36/8.90 Prover 7: Constructing countermodel ... % 63.36/8.90 Prover 10: Warning: ignoring some quantifiers % 63.63/8.91 Prover 10: Constructing countermodel ... % 63.63/8.92 Prover 8: Warning: ignoring some quantifiers % 63.63/8.92 Prover 11: Warning: ignoring some quantifiers % 63.63/8.93 Prover 8: Constructing countermodel ... % 63.86/8.94 Prover 11: Constructing countermodel ... % 63.86/9.01 Prover 13: Warning: ignoring some quantifiers % 63.86/9.02 Prover 13: Constructing countermodel ... % 78.41/10.81 Prover 7: Found proof (size 131) % 78.41/10.81 Prover 7: proved (2092ms) % 78.41/10.81 Prover 11: stopped % 78.41/10.81 Prover 8: stopped % 78.41/10.81 Prover 10: stopped % 78.41/10.81 Prover 13: stopped % 78.41/10.82 Prover 4: stopped % 78.41/10.82 Prover 1: stopped % 78.41/10.82 % 78.41/10.82 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 78.41/10.82 % 78.41/10.83 % SZS output start Proof for theBenchmark % 78.41/10.83 Assumptions after simplification: % 78.41/10.83 --------------------------------- % 78.41/10.83 % 78.41/10.83 (bridgeL2) % 78.72/10.85 ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | tb2t2(v1) = v0) % 78.72/10.85 % 78.72/10.85 (bridgeR) % 78.72/10.85 ! [v0: uni] : ! [v1: map_int_lpoption_intrp] : ( ~ (tb2t(v0) = v1) | ~ % 78.72/10.85 uni(v0) | t2tb(v1) = v0) % 78.72/10.85 % 78.72/10.85 (bridgeR1) % 78.72/10.85 ! [v0: uni] : ! [v1: option_int] : ( ~ (tb2t1(v0) = v1) | ~ uni(v0) | % 78.72/10.85 t2tb1(v1) = v0) % 78.74/10.85 % 78.74/10.85 (fibn) % 78.74/10.85 ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(2, v0)) | ~ (fib($sum(v0, -2)) = % 78.74/10.85 v1) | ? [v2: int] : (fib($sum(v0, -1)) = $difference(v2, v1) & fib(v0) = % 78.74/10.85 v2)) & ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(2, v0)) | ~ % 78.74/10.85 (fib($sum(v0, -1)) = v1) | ? [v2: int] : (fib($sum(v0, -2)) = % 78.74/10.85 $difference(v2, v1) & fib(v0) = v2)) & ! [v0: int] : ! [v1: int] : ( ~ % 78.74/10.85 ($lesseq(2, v0)) | ~ (fib(v0) = v1) | ? [v2: int] : (fib($sum(v0, -2)) = % 78.74/10.85 $difference(v1, v2) & fib($sum(v0, -1)) = v2)) % 78.74/10.85 % 78.74/10.85 (inv_def) % 78.74/10.86 ty(int) & ? [v0: ty] : (option(int) = v0 & ty(v0) & ! [v1: % 78.74/10.86 map_int_lpoption_intrp] : ! [v2: uni] : ! [v3: int] : ! [v4: int] : ! % 78.74/10.86 [v5: uni] : ! [v6: uni] : ! [v7: option_int] : ! [v8: uni] : ! [v9: uni] % 78.74/10.86 : ( ~ (t2tb2(v4) = v8) | ~ (t2tb2(v3) = v5) | ~ (tb2t1(v9) = v7) | ~ % 78.74/10.86 (tb2t1(v6) = v7) | ~ (t2tb(v1) = v2) | ~ (get(v0, int, v2, v5) = v6) | % 78.74/10.86 ~ (some(int, v8) = v9) | ~ map_int_lpoption_intrp(v1) | ~ inv(v1) | % 78.74/10.86 fib(v3) = v4) & ! [v1: map_int_lpoption_intrp] : ! [v2: uni] : ! [v3: % 78.74/10.86 int] : ! [v4: int] : ! [v5: uni] : ! [v6: uni] : ! [v7: option_int] : % 78.74/10.86 ! [v8: int] : (v8 = v4 | ~ (t2tb2(v4) = v5) | ~ (tb2t1(v6) = v7) | ~ % 78.74/10.86 (t2tb(v1) = v2) | ~ (fib(v3) = v8) | ~ (some(int, v5) = v6) | ~ % 78.74/10.86 map_int_lpoption_intrp(v1) | ~ inv(v1) | ? [v9: uni] : ? [v10: uni] : % 78.74/10.86 ? [v11: option_int] : ( ~ (v11 = v7) & t2tb2(v3) = v9 & tb2t1(v10) = v11 & % 78.74/10.86 get(v0, int, v2, v9) = v10 & option_int(v11) & uni(v10) & uni(v9))) & ! % 78.74/10.86 [v1: map_int_lpoption_intrp] : ! [v2: uni] : ( ~ (t2tb(v1) = v2) | ~ % 78.74/10.86 map_int_lpoption_intrp(v1) | inv(v1) | ? [v3: int] : ? [v4: int] : ? % 78.74/10.86 [v5: uni] : ? [v6: uni] : ? [v7: option_int] : ? [v8: uni] : ? [v9: % 78.74/10.86 uni] : ? [v10: int] : ( ~ (v10 = v4) & t2tb2(v4) = v8 & t2tb2(v3) = v5 % 78.74/10.86 & tb2t1(v9) = v7 & tb2t1(v6) = v7 & get(v0, int, v2, v5) = v6 & fib(v3) % 78.74/10.86 = v10 & some(int, v8) = v9 & option_int(v7) & uni(v9) & uni(v8) & % 78.74/10.86 uni(v6) & uni(v5)))) % 78.74/10.86 % 78.74/10.86 (none_sort) % 78.74/10.86 ! [v0: ty] : ! [v1: ty] : ( ~ (option(v0) = v1) | ~ ty(v0) | ? [v2: uni] : % 78.74/10.86 (none(v0) = v2 & uni(v2) & sort(v1, v2))) & ! [v0: ty] : ! [v1: uni] : ( ~ % 78.74/10.86 (none(v0) = v1) | ~ ty(v0) | ? [v2: ty] : (option(v0) = v2 & ty(v2) & % 78.74/10.86 sort(v2, v1))) % 78.74/10.86 % 78.74/10.86 (select_eq) % 78.74/10.86 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 78.74/10.86 [v5: uni] : ! [v6: uni] : (v6 = v4 | ~ (set(v1, v0, v2, v3, v4) = v5) | ~ % 78.74/10.86 (get(v1, v0, v5, v3) = v6) | ~ ty(v1) | ~ ty(v0) | ~ uni(v4) | ~ uni(v3) % 78.74/10.86 | ~ uni(v2) | ~ sort(v1, v4)) % 78.74/10.86 % 78.74/10.86 (select_neq) % 78.74/10.86 ! [v0: ty] : ! [v1: ty] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 78.74/10.86 [v5: uni] : ! [v6: uni] : ! [v7: uni] : (v4 = v3 | ~ (set(v1, v0, v2, v3, % 78.74/10.86 v6) = v7) | ~ (get(v1, v0, v2, v4) = v5) | ~ ty(v1) | ~ ty(v0) | ~ % 78.74/10.86 uni(v6) | ~ uni(v4) | ~ uni(v3) | ~ uni(v2) | ~ sort(v0, v4) | ~ % 78.74/10.86 sort(v0, v3) | (get(v1, v0, v7, v4) = v5 & uni(v5))) % 78.74/10.86 % 78.74/10.86 (some_proj_1_def) % 78.74/10.87 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (some(v0, v1) = v2) | ~ % 78.74/10.87 ty(v0) | ~ uni(v1) | ~ sort(v0, v1) | some_proj_1(v0, v2) = v1) % 78.74/10.87 % 78.74/10.87 (some_sort) % 78.74/10.87 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ( ~ (some(v0, v1) = v2) | ~ % 78.74/10.87 ty(v0) | ~ uni(v1) | ? [v3: ty] : (option(v0) = v3 & ty(v3) & sort(v3, % 78.74/10.87 v2))) % 78.74/10.87 % 78.74/10.87 (t2tb_sort) % 78.74/10.87 ty(int) & ? [v0: ty] : ? [v1: ty] : (map(int, v0) = v1 & option(int) = v0 & % 78.74/10.87 ty(v1) & ty(v0) & ! [v2: map_int_lpoption_intrp] : ! [v3: uni] : ( ~ % 78.74/10.87 (t2tb(v2) = v3) | ~ map_int_lpoption_intrp(v2) | sort(v1, v3))) % 78.74/10.87 % 78.74/10.87 (t2tb_sort1) % 78.74/10.87 ty(int) & ? [v0: ty] : (option(int) = v0 & ty(v0) & ! [v1: option_int] : ! % 78.74/10.87 [v2: uni] : ( ~ (t2tb1(v1) = v2) | ~ option_int(v1) | sort(v0, v2))) % 78.74/10.87 % 78.74/10.87 (t2tb_sort2) % 78.74/10.87 ty(int) & ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | sort(int, v1)) % 78.74/10.87 % 78.74/10.87 (wP_parameter_memo_fibo) % 78.74/10.87 ty(int) & ? [v0: ty] : ? [v1: uni] : ? [v2: option_int] : ? [v3: int] : ? % 78.74/10.87 [v4: map_int_lpoption_intrp] : ? [v5: uni] : ? [v6: uni] : ? [v7: uni] : ? % 78.74/10.87 [v8: int] : ? [v9: uni] : ? [v10: uni] : ? [v11: map_int_lpoption_intrp] : % 78.74/10.87 ? [v12: uni] : ? [v13: uni] : ? [v14: map_int_lpoption_intrp] : ($lesseq(0, % 78.74/10.87 v3) & t2tb2(v8) = v9 & t2tb2(v3) = v6 & tb2t1(v7) = v2 & tb2t1(v1) = v2 & % 78.74/10.87 tb2t(v13) = v14 & t2tb(v11) = v12 & t2tb(v4) = v5 & set(v0, int, v12, v6, % 78.74/10.87 v10) = v13 & get(v0, int, v5, v6) = v7 & fib(v3) = v8 & some(int, v9) = % 78.74/10.87 v10 & option(int) = v0 & none(int) = v1 & option_int(v2) & % 78.74/10.87 map_int_lpoption_intrp(v14) & map_int_lpoption_intrp(v11) & % 78.74/10.87 map_int_lpoption_intrp(v4) & ty(v0) & uni(v13) & uni(v12) & uni(v10) & % 78.74/10.87 uni(v9) & uni(v7) & uni(v6) & uni(v5) & uni(v1) & inv(v11) & inv(v4) & ~ % 78.74/10.87 inv(v14)) % 78.74/10.87 % 78.74/10.87 (function-axioms) % 78.74/10.88 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 78.74/10.88 [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ (set(v6, v5, v4, v3, v2) = v1) | ~ % 78.74/10.88 (set(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 78.74/10.88 : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : ! [v6: ty] : (v1 = v0 | ~ % 78.74/10.88 (match_option(v6, v5, v4, v3, v2) = v1) | ~ (match_option(v6, v5, v4, v3, % 78.74/10.88 v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : % 78.74/10.88 ! [v4: ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 78.74/10.88 (get(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : % 78.74/10.88 ! [v3: uni] : ! [v4: bool] : ! [v5: ty] : (v1 = v0 | ~ (match_bool(v5, v4, % 78.74/10.88 v3, v2) = v1) | ~ (match_bool(v5, v4, v3, v2) = v0)) & ! [v0: uni] : % 78.74/10.88 ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : ! [v4: ty] : (v1 = v0 | ~ % 78.74/10.88 (const(v4, v3, v2) = v1) | ~ (const(v4, v3, v2) = v0)) & ! [v0: ty] : ! % 78.74/10.88 [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (map(v3, v2) = v1) | ~ % 78.74/10.88 (map(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 78.74/10.88 ty] : (v1 = v0 | ~ (contents(v3, v2) = v1) | ~ (contents(v3, v2) = v0)) & % 78.74/10.88 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ % 78.74/10.88 (mk_ref(v3, v2) = v1) | ~ (mk_ref(v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 78.74/10.88 uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (some_proj_1(v3, v2) = v1) % 78.74/10.88 | ~ (some_proj_1(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 78.74/10.88 uni] : ! [v3: ty] : (v1 = v0 | ~ (some(v3, v2) = v1) | ~ (some(v3, v2) = % 78.74/10.88 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ % 78.74/10.88 (tb2t2(v2) = v1) | ~ (tb2t2(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 78.74/10.88 [v2: int] : (v1 = v0 | ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! [v0: % 78.74/10.88 option_int] : ! [v1: option_int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) % 78.74/10.88 = v1) | ~ (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 78.74/10.88 option_int] : (v1 = v0 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! % 78.74/10.88 [v0: map_int_lpoption_intrp] : ! [v1: map_int_lpoption_intrp] : ! [v2: uni] % 78.74/10.88 : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: % 78.74/10.88 uni] : ! [v2: map_int_lpoption_intrp] : (v1 = v0 | ~ (t2tb(v2) = v1) | ~ % 78.74/10.88 (t2tb(v2) = v0)) & ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ % 78.74/10.88 (ref(v2) = v1) | ~ (ref(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 78.74/10.88 int] : (v1 = v0 | ~ (fib(v2) = v1) | ~ (fib(v2) = v0)) & ! [v0: ty] : ! % 78.74/10.88 [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (option(v2) = v1) | ~ (option(v2) = % 78.74/10.88 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (none(v2) % 78.74/10.88 = v1) | ~ (none(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : % 78.74/10.88 (v1 = v0 | ~ (witness(v2) = v1) | ~ (witness(v2) = v0)) % 78.74/10.88 % 78.74/10.88 Further assumptions not needed in the proof: % 78.74/10.88 -------------------------------------------- % 78.74/10.88 bool_inversion, bridgeL, bridgeL1, bridgeR2, compatOrderMult, const1, % 78.74/10.88 const_sort, contents_def, contents_sort, fib0, fib1, get_sort, match_bool_False, % 78.74/10.88 match_bool_True, match_bool_sort, match_option_None, match_option_Some, % 78.74/10.88 match_option_sort, mk_ref_sort, none_Some, option_inversion, ref_inversion, % 78.74/10.88 set_sort, some_proj_1_sort, true_False, tuple0_inversion, witness_sort % 78.74/10.88 % 78.74/10.88 Those formulas are unsatisfiable: % 78.74/10.88 --------------------------------- % 78.74/10.88 % 78.74/10.88 Begin of proof % 78.74/10.88 | % 78.74/10.88 | ALPHA: (none_sort) implies: % 78.74/10.88 | (1) ! [v0: ty] : ! [v1: uni] : ( ~ (none(v0) = v1) | ~ ty(v0) | ? [v2: % 78.74/10.88 | ty] : (option(v0) = v2 & ty(v2) & sort(v2, v1))) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (fibn) implies: % 78.74/10.89 | (2) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(2, v0)) | ~ (fib($sum(v0, % 78.74/10.89 | -2)) = v1) | ? [v2: int] : (fib($sum(v0, -1)) = % 78.74/10.89 | $difference(v2, v1) & fib(v0) = v2)) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (t2tb_sort) implies: % 78.74/10.89 | (3) ? [v0: ty] : ? [v1: ty] : (map(int, v0) = v1 & option(int) = v0 & % 78.74/10.89 | ty(v1) & ty(v0) & ! [v2: map_int_lpoption_intrp] : ! [v3: uni] : ( % 78.74/10.89 | ~ (t2tb(v2) = v3) | ~ map_int_lpoption_intrp(v2) | sort(v1, v3))) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (t2tb_sort1) implies: % 78.74/10.89 | (4) ? [v0: ty] : (option(int) = v0 & ty(v0) & ! [v1: option_int] : ! % 78.74/10.89 | [v2: uni] : ( ~ (t2tb1(v1) = v2) | ~ option_int(v1) | sort(v0, v2))) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (t2tb_sort2) implies: % 78.74/10.89 | (5) ! [v0: int] : ! [v1: uni] : ( ~ (t2tb2(v0) = v1) | sort(int, v1)) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (inv_def) implies: % 78.74/10.89 | (6) ? [v0: ty] : (option(int) = v0 & ty(v0) & ! [v1: % 78.74/10.89 | map_int_lpoption_intrp] : ! [v2: uni] : ! [v3: int] : ! [v4: % 78.74/10.89 | int] : ! [v5: uni] : ! [v6: uni] : ! [v7: option_int] : ! [v8: % 78.74/10.89 | uni] : ! [v9: uni] : ( ~ (t2tb2(v4) = v8) | ~ (t2tb2(v3) = v5) | % 78.74/10.89 | ~ (tb2t1(v9) = v7) | ~ (tb2t1(v6) = v7) | ~ (t2tb(v1) = v2) | ~ % 78.74/10.89 | (get(v0, int, v2, v5) = v6) | ~ (some(int, v8) = v9) | ~ % 78.74/10.89 | map_int_lpoption_intrp(v1) | ~ inv(v1) | fib(v3) = v4) & ! [v1: % 78.74/10.89 | map_int_lpoption_intrp] : ! [v2: uni] : ! [v3: int] : ! [v4: % 78.74/10.89 | int] : ! [v5: uni] : ! [v6: uni] : ! [v7: option_int] : ! [v8: % 78.74/10.89 | int] : (v8 = v4 | ~ (t2tb2(v4) = v5) | ~ (tb2t1(v6) = v7) | ~ % 78.74/10.89 | (t2tb(v1) = v2) | ~ (fib(v3) = v8) | ~ (some(int, v5) = v6) | ~ % 78.74/10.89 | map_int_lpoption_intrp(v1) | ~ inv(v1) | ? [v9: uni] : ? [v10: % 78.74/10.89 | uni] : ? [v11: option_int] : ( ~ (v11 = v7) & t2tb2(v3) = v9 & % 78.74/10.89 | tb2t1(v10) = v11 & get(v0, int, v2, v9) = v10 & option_int(v11) & % 78.74/10.89 | uni(v10) & uni(v9))) & ! [v1: map_int_lpoption_intrp] : ! [v2: % 78.74/10.89 | uni] : ( ~ (t2tb(v1) = v2) | ~ map_int_lpoption_intrp(v1) | % 78.74/10.89 | inv(v1) | ? [v3: int] : ? [v4: int] : ? [v5: uni] : ? [v6: uni] % 78.74/10.89 | : ? [v7: option_int] : ? [v8: uni] : ? [v9: uni] : ? [v10: int] % 78.74/10.89 | : ( ~ (v10 = v4) & t2tb2(v4) = v8 & t2tb2(v3) = v5 & tb2t1(v9) = v7 % 78.74/10.89 | & tb2t1(v6) = v7 & get(v0, int, v2, v5) = v6 & fib(v3) = v10 & % 78.74/10.89 | some(int, v8) = v9 & option_int(v7) & uni(v9) & uni(v8) & uni(v6) % 78.74/10.89 | & uni(v5)))) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (wP_parameter_memo_fibo) implies: % 78.74/10.89 | (7) ty(int) % 78.74/10.89 | (8) ? [v0: ty] : ? [v1: uni] : ? [v2: option_int] : ? [v3: int] : ? % 78.74/10.89 | [v4: map_int_lpoption_intrp] : ? [v5: uni] : ? [v6: uni] : ? [v7: % 78.74/10.89 | uni] : ? [v8: int] : ? [v9: uni] : ? [v10: uni] : ? [v11: % 78.74/10.89 | map_int_lpoption_intrp] : ? [v12: uni] : ? [v13: uni] : ? [v14: % 78.74/10.89 | map_int_lpoption_intrp] : ($lesseq(0, v3) & t2tb2(v8) = v9 & % 78.74/10.89 | t2tb2(v3) = v6 & tb2t1(v7) = v2 & tb2t1(v1) = v2 & tb2t(v13) = v14 & % 78.74/10.89 | t2tb(v11) = v12 & t2tb(v4) = v5 & set(v0, int, v12, v6, v10) = v13 & % 78.74/10.89 | get(v0, int, v5, v6) = v7 & fib(v3) = v8 & some(int, v9) = v10 & % 78.74/10.89 | option(int) = v0 & none(int) = v1 & option_int(v2) & % 78.74/10.89 | map_int_lpoption_intrp(v14) & map_int_lpoption_intrp(v11) & % 78.74/10.89 | map_int_lpoption_intrp(v4) & ty(v0) & uni(v13) & uni(v12) & uni(v10) % 78.74/10.89 | & uni(v9) & uni(v7) & uni(v6) & uni(v5) & uni(v1) & inv(v11) & % 78.74/10.89 | inv(v4) & ~ inv(v14)) % 78.74/10.89 | % 78.74/10.89 | ALPHA: (function-axioms) implies: % 78.74/10.89 | (9) ! [v0: ty] : ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (option(v2) = % 78.74/10.89 | v1) | ~ (option(v2) = v0)) % 78.74/10.89 | (10) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v1 = v0 | ~ (fib(v2) = % 78.74/10.89 | v1) | ~ (fib(v2) = v0)) % 78.74/10.89 | (11) ! [v0: uni] : ! [v1: uni] : ! [v2: option_int] : (v1 = v0 | ~ % 78.74/10.89 | (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 78.74/10.89 | (12) ! [v0: uni] : ! [v1: uni] : ! [v2: int] : (v1 = v0 | ~ (t2tb2(v2) % 78.74/10.89 | = v1) | ~ (t2tb2(v2) = v0)) % 78.74/10.89 | (13) ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) % 78.74/10.89 | = v1) | ~ (tb2t2(v2) = v0)) % 78.74/10.90 | (14) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 78.74/10.90 | ~ (some_proj_1(v3, v2) = v1) | ~ (some_proj_1(v3, v2) = v0)) % 78.74/10.90 | (15) ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 78.74/10.90 | ty] : ! [v5: ty] : (v1 = v0 | ~ (get(v5, v4, v3, v2) = v1) | ~ % 78.74/10.90 | (get(v5, v4, v3, v2) = v0)) % 78.74/10.90 | % 78.74/10.90 | DELTA: instantiating (4) with fresh symbol all_50_0 gives: % 78.74/10.90 | (16) option(int) = all_50_0 & ty(all_50_0) & ! [v0: option_int] : ! [v1: % 78.74/10.90 | uni] : ( ~ (t2tb1(v0) = v1) | ~ option_int(v0) | sort(all_50_0, % 78.74/10.90 | v1)) % 78.74/10.90 | % 78.74/10.90 | ALPHA: (16) implies: % 78.74/10.90 | (17) option(int) = all_50_0 % 78.74/10.90 | % 78.74/10.90 | DELTA: instantiating (3) with fresh symbols all_53_0, all_53_1 gives: % 78.74/10.90 | (18) map(int, all_53_1) = all_53_0 & option(int) = all_53_1 & ty(all_53_0) % 78.74/10.90 | & ty(all_53_1) & ! [v0: map_int_lpoption_intrp] : ! [v1: uni] : ( ~ % 78.74/10.90 | (t2tb(v0) = v1) | ~ map_int_lpoption_intrp(v0) | sort(all_53_0, % 78.74/10.90 | v1)) % 78.74/10.90 | % 78.74/10.90 | ALPHA: (18) implies: % 78.74/10.90 | (19) option(int) = all_53_1 % 78.74/10.90 | % 78.74/10.90 | DELTA: instantiating (8) with fresh symbols all_56_0, all_56_1, all_56_2, % 78.74/10.90 | all_56_3, all_56_4, all_56_5, all_56_6, all_56_7, all_56_8, all_56_9, % 78.74/10.90 | all_56_10, all_56_11, all_56_12, all_56_13, all_56_14 gives: % 78.74/10.90 | (20) $lesseq(0, all_56_11) & t2tb2(all_56_6) = all_56_5 & t2tb2(all_56_11) % 78.74/10.90 | = all_56_8 & tb2t1(all_56_7) = all_56_12 & tb2t1(all_56_13) = % 78.74/10.90 | all_56_12 & tb2t(all_56_1) = all_56_0 & t2tb(all_56_3) = all_56_2 & % 78.74/10.90 | t2tb(all_56_10) = all_56_9 & set(all_56_14, int, all_56_2, all_56_8, % 78.74/10.90 | all_56_4) = all_56_1 & get(all_56_14, int, all_56_9, all_56_8) = % 78.74/10.90 | all_56_7 & fib(all_56_11) = all_56_6 & some(int, all_56_5) = all_56_4 % 78.74/10.90 | & option(int) = all_56_14 & none(int) = all_56_13 & % 78.74/10.90 | option_int(all_56_12) & map_int_lpoption_intrp(all_56_0) & % 78.74/10.90 | map_int_lpoption_intrp(all_56_3) & map_int_lpoption_intrp(all_56_10) & % 78.74/10.90 | ty(all_56_14) & uni(all_56_1) & uni(all_56_2) & uni(all_56_4) & % 78.74/10.90 | uni(all_56_5) & uni(all_56_7) & uni(all_56_8) & uni(all_56_9) & % 78.74/10.90 | uni(all_56_13) & inv(all_56_3) & inv(all_56_10) & ~ inv(all_56_0) % 78.74/10.90 | % 78.74/10.90 | ALPHA: (20) implies: % 78.74/10.90 | (21) $lesseq(0, all_56_11) % 78.74/10.90 | (22) ~ inv(all_56_0) % 78.74/10.90 | (23) inv(all_56_10) % 78.74/10.90 | (24) inv(all_56_3) % 78.74/10.90 | (25) uni(all_56_8) % 78.74/10.90 | (26) uni(all_56_5) % 78.74/10.90 | (27) uni(all_56_4) % 78.74/10.90 | (28) uni(all_56_2) % 78.74/10.90 | (29) uni(all_56_1) % 78.74/10.90 | (30) map_int_lpoption_intrp(all_56_10) % 79.00/10.90 | (31) map_int_lpoption_intrp(all_56_3) % 79.00/10.90 | (32) map_int_lpoption_intrp(all_56_0) % 79.00/10.90 | (33) none(int) = all_56_13 % 79.00/10.90 | (34) option(int) = all_56_14 % 79.00/10.90 | (35) some(int, all_56_5) = all_56_4 % 79.00/10.90 | (36) fib(all_56_11) = all_56_6 % 79.00/10.90 | (37) set(all_56_14, int, all_56_2, all_56_8, all_56_4) = all_56_1 % 79.00/10.90 | (38) t2tb(all_56_10) = all_56_9 % 79.00/10.90 | (39) t2tb(all_56_3) = all_56_2 % 79.00/10.90 | (40) tb2t(all_56_1) = all_56_0 % 79.00/10.90 | (41) t2tb2(all_56_11) = all_56_8 % 79.00/10.90 | (42) t2tb2(all_56_6) = all_56_5 % 79.00/10.90 | % 79.00/10.90 | DELTA: instantiating (6) with fresh symbol all_59_0 gives: % 79.00/10.90 | (43) option(int) = all_59_0 & ty(all_59_0) & ! [v0: % 79.00/10.90 | map_int_lpoption_intrp] : ! [v1: uni] : ! [v2: int] : ! [v3: int] % 79.00/10.90 | : ! [v4: uni] : ! [v5: uni] : ! [v6: option_int] : ! [v7: uni] : % 79.00/10.90 | ! [v8: uni] : ( ~ (t2tb2(v3) = v7) | ~ (t2tb2(v2) = v4) | ~ % 79.00/10.90 | (tb2t1(v8) = v6) | ~ (tb2t1(v5) = v6) | ~ (t2tb(v0) = v1) | ~ % 79.00/10.90 | (get(all_59_0, int, v1, v4) = v5) | ~ (some(int, v7) = v8) | ~ % 79.00/10.90 | map_int_lpoption_intrp(v0) | ~ inv(v0) | fib(v2) = v3) & ! [v0: % 79.00/10.90 | map_int_lpoption_intrp] : ! [v1: uni] : ! [v2: int] : ! [v3: int] % 79.00/10.90 | : ! [v4: uni] : ! [v5: uni] : ! [v6: option_int] : ! [v7: int] : % 79.00/10.90 | (v7 = v3 | ~ (t2tb2(v3) = v4) | ~ (tb2t1(v5) = v6) | ~ (t2tb(v0) = % 79.00/10.90 | v1) | ~ (fib(v2) = v7) | ~ (some(int, v4) = v5) | ~ % 79.00/10.90 | map_int_lpoption_intrp(v0) | ~ inv(v0) | ? [v8: uni] : ? [v9: % 79.00/10.90 | uni] : ? [v10: option_int] : ( ~ (v10 = v6) & t2tb2(v2) = v8 & % 79.00/10.90 | tb2t1(v9) = v10 & get(all_59_0, int, v1, v8) = v9 & % 79.00/10.90 | option_int(v10) & uni(v9) & uni(v8))) & ! [v0: % 79.00/10.90 | map_int_lpoption_intrp] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ % 79.00/10.90 | map_int_lpoption_intrp(v0) | inv(v0) | ? [v2: int] : ? [v3: int] : % 79.00/10.90 | ? [v4: uni] : ? [v5: uni] : ? [v6: option_int] : ? [v7: uni] : % 79.00/10.90 | ? [v8: uni] : ? [v9: int] : ( ~ (v9 = v3) & t2tb2(v3) = v7 & % 79.00/10.90 | t2tb2(v2) = v4 & tb2t1(v8) = v6 & tb2t1(v5) = v6 & get(all_59_0, % 79.00/10.90 | int, v1, v4) = v5 & fib(v2) = v9 & some(int, v7) = v8 & % 79.00/10.90 | option_int(v6) & uni(v8) & uni(v7) & uni(v5) & uni(v4))) % 79.00/10.91 | % 79.00/10.91 | ALPHA: (43) implies: % 79.00/10.91 | (44) option(int) = all_59_0 % 79.00/10.91 | (45) ! [v0: map_int_lpoption_intrp] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | % 79.00/10.91 | ~ map_int_lpoption_intrp(v0) | inv(v0) | ? [v2: int] : ? [v3: % 79.00/10.91 | int] : ? [v4: uni] : ? [v5: uni] : ? [v6: option_int] : ? [v7: % 79.00/10.91 | uni] : ? [v8: uni] : ? [v9: int] : ( ~ (v9 = v3) & t2tb2(v3) = % 79.00/10.91 | v7 & t2tb2(v2) = v4 & tb2t1(v8) = v6 & tb2t1(v5) = v6 & % 79.00/10.91 | get(all_59_0, int, v1, v4) = v5 & fib(v2) = v9 & some(int, v7) = % 79.00/10.91 | v8 & option_int(v6) & uni(v8) & uni(v7) & uni(v5) & uni(v4))) % 79.00/10.91 | (46) ! [v0: map_int_lpoption_intrp] : ! [v1: uni] : ! [v2: int] : ! % 79.00/10.91 | [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: option_int] : ! % 79.00/10.91 | [v7: int] : (v7 = v3 | ~ (t2tb2(v3) = v4) | ~ (tb2t1(v5) = v6) | ~ % 79.00/10.91 | (t2tb(v0) = v1) | ~ (fib(v2) = v7) | ~ (some(int, v4) = v5) | ~ % 79.00/10.91 | map_int_lpoption_intrp(v0) | ~ inv(v0) | ? [v8: uni] : ? [v9: % 79.00/10.91 | uni] : ? [v10: option_int] : ( ~ (v10 = v6) & t2tb2(v2) = v8 & % 79.00/10.91 | tb2t1(v9) = v10 & get(all_59_0, int, v1, v8) = v9 & % 79.00/10.91 | option_int(v10) & uni(v9) & uni(v8))) % 79.00/10.91 | (47) ! [v0: map_int_lpoption_intrp] : ! [v1: uni] : ! [v2: int] : ! % 79.00/10.91 | [v3: int] : ! [v4: uni] : ! [v5: uni] : ! [v6: option_int] : ! % 79.00/10.91 | [v7: uni] : ! [v8: uni] : ( ~ (t2tb2(v3) = v7) | ~ (t2tb2(v2) = v4) % 79.00/10.91 | | ~ (tb2t1(v8) = v6) | ~ (tb2t1(v5) = v6) | ~ (t2tb(v0) = v1) | % 79.00/10.91 | ~ (get(all_59_0, int, v1, v4) = v5) | ~ (some(int, v7) = v8) | ~ % 79.00/10.91 | map_int_lpoption_intrp(v0) | ~ inv(v0) | fib(v2) = v3) % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (9) with all_53_1, all_56_14, int, simplifying with % 79.00/10.91 | (19), (34) gives: % 79.00/10.91 | (48) all_56_14 = all_53_1 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (9) with all_56_14, all_59_0, int, simplifying with % 79.00/10.91 | (34), (44) gives: % 79.00/10.91 | (49) all_59_0 = all_56_14 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (9) with all_50_0, all_59_0, int, simplifying with % 79.00/10.91 | (17), (44) gives: % 79.00/10.91 | (50) all_59_0 = all_50_0 % 79.00/10.91 | % 79.00/10.91 | COMBINE_EQS: (49), (50) imply: % 79.00/10.91 | (51) all_56_14 = all_50_0 % 79.00/10.91 | % 79.00/10.91 | SIMP: (51) implies: % 79.00/10.91 | (52) all_56_14 = all_50_0 % 79.00/10.91 | % 79.00/10.91 | COMBINE_EQS: (48), (52) imply: % 79.00/10.91 | (53) all_53_1 = all_50_0 % 79.00/10.91 | % 79.00/10.91 | SIMP: (53) implies: % 79.00/10.91 | (54) all_53_1 = all_50_0 % 79.00/10.91 | % 79.00/10.91 | REDUCE: (37), (52) imply: % 79.00/10.91 | (55) set(all_50_0, int, all_56_2, all_56_8, all_56_4) = all_56_1 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (1) with int, all_56_13, simplifying with (7), (33) % 79.00/10.91 | gives: % 79.00/10.91 | (56) ? [v0: ty] : (option(int) = v0 & ty(v0) & sort(v0, all_56_13)) % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (some_sort) with int, all_56_5, all_56_4, % 79.00/10.91 | simplifying with (7), (26), (35) gives: % 79.00/10.91 | (57) ? [v0: ty] : (option(int) = v0 & ty(v0) & sort(v0, all_56_4)) % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (2) with $sum(all_56_11, 2), all_56_6, simplifying % 79.00/10.91 | with (36) gives: % 79.00/10.91 | (58) ~ ($lesseq(0, all_56_11)) | ? [v0: int] : (fib($sum(all_56_11, 2)) = % 79.00/10.91 | v0 & fib($sum(all_56_11, 1)) = $difference(v0, all_56_6)) % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (bridgeR) with all_56_1, all_56_0, simplifying with % 79.00/10.91 | (29), (40) gives: % 79.00/10.91 | (59) t2tb(all_56_0) = all_56_1 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (bridgeL2) with all_56_11, all_56_8, simplifying % 79.00/10.91 | with (41) gives: % 79.00/10.91 | (60) tb2t2(all_56_8) = all_56_11 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (5) with all_56_11, all_56_8, simplifying with (41) % 79.00/10.91 | gives: % 79.00/10.91 | (61) sort(int, all_56_8) % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (bridgeL2) with all_56_6, all_56_5, simplifying % 79.00/10.91 | with (42) gives: % 79.00/10.91 | (62) tb2t2(all_56_5) = all_56_6 % 79.00/10.91 | % 79.00/10.91 | GROUND_INST: instantiating (5) with all_56_6, all_56_5, simplifying with (42) % 79.00/10.91 | gives: % 79.00/10.91 | (63) sort(int, all_56_5) % 79.00/10.91 | % 79.00/10.91 | DELTA: instantiating (57) with fresh symbol all_83_0 gives: % 79.00/10.92 | (64) option(int) = all_83_0 & ty(all_83_0) & sort(all_83_0, all_56_4) % 79.00/10.92 | % 79.00/10.92 | ALPHA: (64) implies: % 79.00/10.92 | (65) sort(all_83_0, all_56_4) % 79.00/10.92 | (66) ty(all_83_0) % 79.00/10.92 | (67) option(int) = all_83_0 % 79.00/10.92 | % 79.00/10.92 | DELTA: instantiating (56) with fresh symbol all_89_0 gives: % 79.00/10.92 | (68) option(int) = all_89_0 & ty(all_89_0) & sort(all_89_0, all_56_13) % 79.00/10.92 | % 79.00/10.92 | ALPHA: (68) implies: % 79.00/10.92 | (69) option(int) = all_89_0 % 79.00/10.92 | % 79.00/10.92 | BETA: splitting (58) gives: % 79.00/10.92 | % 79.00/10.92 | Case 1: % 79.00/10.92 | | % 79.00/10.92 | | (70) $lesseq(all_56_11, -1) % 79.00/10.92 | | % 79.00/10.92 | | COMBINE_INEQS: (21), (70) imply: % 79.00/10.92 | | (71) $false % 79.00/10.92 | | % 79.00/10.92 | | CLOSE: (71) is inconsistent. % 79.00/10.92 | | % 79.00/10.92 | Case 2: % 79.00/10.92 | | % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (9) with all_50_0, all_89_0, int, simplifying % 79.00/10.92 | | with (17), (69) gives: % 79.00/10.92 | | (72) all_89_0 = all_50_0 % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (9) with all_83_0, all_89_0, int, simplifying % 79.00/10.92 | | with (67), (69) gives: % 79.00/10.92 | | (73) all_89_0 = all_83_0 % 79.00/10.92 | | % 79.00/10.92 | | COMBINE_EQS: (72), (73) imply: % 79.00/10.92 | | (74) all_83_0 = all_50_0 % 79.00/10.92 | | % 79.00/10.92 | | REDUCE: (66), (74) imply: % 79.00/10.92 | | (75) ty(all_50_0) % 79.00/10.92 | | % 79.00/10.92 | | REDUCE: (65), (74) imply: % 79.00/10.92 | | (76) sort(all_50_0, all_56_4) % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (some_proj_1_def) with int, all_56_5, all_56_4, % 79.00/10.92 | | simplifying with (7), (26), (35), (63) gives: % 79.00/10.92 | | (77) some_proj_1(int, all_56_4) = all_56_5 % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (45) with all_56_0, all_56_1, simplifying with % 79.00/10.92 | | (22), (32), (59) gives: % 79.00/10.92 | | (78) ? [v0: int] : ? [v1: int] : ? [v2: uni] : ? [v3: uni] : ? [v4: % 79.00/10.92 | | option_int] : ? [v5: uni] : ? [v6: uni] : ? [v7: int] : ( ~ (v7 % 79.00/10.92 | | = v1) & t2tb2(v1) = v5 & t2tb2(v0) = v2 & tb2t1(v6) = v4 & % 79.00/10.92 | | tb2t1(v3) = v4 & get(all_59_0, int, all_56_1, v2) = v3 & fib(v0) = % 79.00/10.92 | | v7 & some(int, v5) = v6 & option_int(v4) & uni(v6) & uni(v5) & % 79.00/10.92 | | uni(v3) & uni(v2)) % 79.00/10.92 | | % 79.00/10.92 | | DELTA: instantiating (78) with fresh symbols all_116_0, all_116_1, % 79.00/10.92 | | all_116_2, all_116_3, all_116_4, all_116_5, all_116_6, all_116_7 % 79.00/10.92 | | gives: % 79.00/10.92 | | (79) ~ (all_116_0 = all_116_6) & t2tb2(all_116_6) = all_116_2 & % 79.00/10.92 | | t2tb2(all_116_7) = all_116_5 & tb2t1(all_116_1) = all_116_3 & % 79.00/10.92 | | tb2t1(all_116_4) = all_116_3 & get(all_59_0, int, all_56_1, % 79.00/10.92 | | all_116_5) = all_116_4 & fib(all_116_7) = all_116_0 & some(int, % 79.00/10.92 | | all_116_2) = all_116_1 & option_int(all_116_3) & uni(all_116_1) & % 79.00/10.92 | | uni(all_116_2) & uni(all_116_4) & uni(all_116_5) % 79.00/10.92 | | % 79.00/10.92 | | ALPHA: (79) implies: % 79.00/10.92 | | (80) ~ (all_116_0 = all_116_6) % 79.00/10.92 | | (81) uni(all_116_4) % 79.00/10.92 | | (82) uni(all_116_2) % 79.00/10.92 | | (83) uni(all_116_1) % 79.00/10.92 | | (84) some(int, all_116_2) = all_116_1 % 79.00/10.92 | | (85) fib(all_116_7) = all_116_0 % 79.00/10.92 | | (86) get(all_59_0, int, all_56_1, all_116_5) = all_116_4 % 79.00/10.92 | | (87) tb2t1(all_116_4) = all_116_3 % 79.00/10.92 | | (88) tb2t1(all_116_1) = all_116_3 % 79.00/10.92 | | (89) t2tb2(all_116_7) = all_116_5 % 79.00/10.92 | | (90) t2tb2(all_116_6) = all_116_2 % 79.00/10.92 | | % 79.00/10.92 | | REDUCE: (50), (86) imply: % 79.00/10.92 | | (91) get(all_50_0, int, all_56_1, all_116_5) = all_116_4 % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (10) with all_56_6, all_116_0, all_56_11, % 79.00/10.92 | | simplifying with (36) gives: % 79.00/10.92 | | (92) all_116_0 = all_56_6 | ~ (fib(all_56_11) = all_116_0) % 79.00/10.92 | | % 79.00/10.92 | | GROUND_INST: instantiating (some_sort) with int, all_116_2, all_116_1, % 79.00/10.92 | | simplifying with (7), (82), (84) gives: % 79.00/10.92 | | (93) ? [v0: ty] : (option(int) = v0 & ty(v0) & sort(v0, all_116_1)) % 79.00/10.92 | | % 79.00/10.93 | | GROUND_INST: instantiating (select_eq) with int, all_50_0, all_56_2, % 79.00/10.93 | | all_56_8, all_56_4, all_56_1, all_116_4, simplifying with (7), % 79.00/10.93 | | (25), (27), (28), (55), (75), (76) gives: % 79.00/10.93 | | (94) all_116_4 = all_56_4 | ~ (get(all_50_0, int, all_56_1, all_56_8) = % 79.00/10.93 | | all_116_4) % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (bridgeR1) with all_116_4, all_116_3, simplifying % 79.00/10.93 | | with (81), (87) gives: % 79.00/10.93 | | (95) t2tb1(all_116_3) = all_116_4 % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (bridgeR1) with all_116_1, all_116_3, simplifying % 79.00/10.93 | | with (83), (88) gives: % 79.00/10.93 | | (96) t2tb1(all_116_3) = all_116_1 % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (bridgeL2) with all_116_7, all_116_5, simplifying % 79.00/10.93 | | with (89) gives: % 79.00/10.93 | | (97) tb2t2(all_116_5) = all_116_7 % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (5) with all_116_7, all_116_5, simplifying with % 79.00/10.93 | | (89) gives: % 79.00/10.93 | | (98) sort(int, all_116_5) % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (47) with all_56_3, all_56_2, all_116_7, % 79.00/10.93 | | all_116_6, all_116_5, all_116_4, all_116_3, all_116_2, % 79.00/10.93 | | all_116_1, simplifying with (24), (31), (39), (84), (87), (88), % 79.00/10.93 | | (89), (90) gives: % 79.00/10.93 | | (99) ~ (get(all_59_0, int, all_56_2, all_116_5) = all_116_4) | % 79.00/10.93 | | fib(all_116_7) = all_116_6 % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (46) with all_56_3, all_56_2, all_116_7, % 79.00/10.93 | | all_116_6, all_116_2, all_116_1, all_116_3, all_116_0, % 79.00/10.93 | | simplifying with (24), (31), (39), (84), (85), (88), (90) % 79.00/10.93 | | gives: % 79.00/10.93 | | (100) all_116_0 = all_116_6 | ? [v0: uni] : ? [v1: uni] : ? [v2: any] % 79.00/10.93 | | : ( ~ (v2 = all_116_3) & t2tb2(all_116_7) = v0 & tb2t1(v1) = v2 & % 79.00/10.93 | | get(all_59_0, int, all_56_2, v0) = v1 & option_int(v2) & uni(v1) % 79.00/10.93 | | & uni(v0)) % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (46) with all_56_10, all_56_9, all_116_7, % 79.00/10.93 | | all_116_6, all_116_2, all_116_1, all_116_3, all_116_0, % 79.00/10.93 | | simplifying with (23), (30), (38), (84), (85), (88), (90) % 79.00/10.93 | | gives: % 79.00/10.93 | | (101) all_116_0 = all_116_6 | ? [v0: uni] : ? [v1: uni] : ? [v2: any] % 79.00/10.93 | | : ( ~ (v2 = all_116_3) & t2tb2(all_116_7) = v0 & tb2t1(v1) = v2 & % 79.00/10.93 | | get(all_59_0, int, all_56_9, v0) = v1 & option_int(v2) & uni(v1) % 79.00/10.93 | | & uni(v0)) % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (bridgeL2) with all_116_6, all_116_2, simplifying % 79.00/10.93 | | with (90) gives: % 79.00/10.93 | | (102) tb2t2(all_116_2) = all_116_6 % 79.00/10.93 | | % 79.00/10.93 | | GROUND_INST: instantiating (5) with all_116_6, all_116_2, simplifying with % 79.00/10.93 | | (90) gives: % 79.00/10.93 | | (103) sort(int, all_116_2) % 79.00/10.93 | | % 79.00/10.93 | | DELTA: instantiating (93) with fresh symbol all_161_0 gives: % 79.00/10.93 | | (104) option(int) = all_161_0 & ty(all_161_0) & sort(all_161_0, % 79.00/10.93 | | all_116_1) % 79.00/10.93 | | % 79.00/10.93 | | ALPHA: (104) implies: % 79.00/10.93 | | (105) ty(all_161_0) % 79.00/10.93 | | (106) option(int) = all_161_0 % 79.00/10.93 | | % 79.00/10.93 | | BETA: splitting (99) gives: % 79.00/10.93 | | % 79.00/10.93 | | Case 1: % 79.00/10.93 | | | % 79.00/10.93 | | | (107) ~ (get(all_59_0, int, all_56_2, all_116_5) = all_116_4) % 79.00/10.93 | | | % 79.00/10.93 | | | REDUCE: (50), (107) imply: % 79.00/10.93 | | | (108) ~ (get(all_50_0, int, all_56_2, all_116_5) = all_116_4) % 79.00/10.93 | | | % 79.00/10.93 | | | BETA: splitting (101) gives: % 79.00/10.93 | | | % 79.00/10.93 | | | Case 1: % 79.00/10.93 | | | | % 79.00/10.93 | | | | (109) all_116_0 = all_116_6 % 79.00/10.93 | | | | % 79.00/10.93 | | | | REDUCE: (80), (109) imply: % 79.00/10.93 | | | | (110) $false % 79.00/10.93 | | | | % 79.00/10.93 | | | | CLOSE: (110) is inconsistent. % 79.00/10.93 | | | | % 79.00/10.93 | | | Case 2: % 79.00/10.93 | | | | % 79.00/10.93 | | | | (111) ? [v0: uni] : ? [v1: uni] : ? [v2: any] : ( ~ (v2 = % 79.00/10.93 | | | | all_116_3) & t2tb2(all_116_7) = v0 & tb2t1(v1) = v2 & % 79.00/10.93 | | | | get(all_59_0, int, all_56_9, v0) = v1 & option_int(v2) & % 79.00/10.93 | | | | uni(v1) & uni(v0)) % 79.00/10.93 | | | | % 79.00/10.93 | | | | DELTA: instantiating (111) with fresh symbols all_196_0, all_196_1, % 79.00/10.93 | | | | all_196_2 gives: % 79.00/10.93 | | | | (112) ~ (all_196_0 = all_116_3) & t2tb2(all_116_7) = all_196_2 & % 79.00/10.93 | | | | tb2t1(all_196_1) = all_196_0 & get(all_59_0, int, all_56_9, % 79.00/10.93 | | | | all_196_2) = all_196_1 & option_int(all_196_0) & % 79.00/10.93 | | | | uni(all_196_1) & uni(all_196_2) % 79.00/10.93 | | | | % 79.00/10.93 | | | | ALPHA: (112) implies: % 79.00/10.93 | | | | (113) uni(all_196_2) % 79.00/10.93 | | | | (114) t2tb2(all_116_7) = all_196_2 % 79.00/10.93 | | | | % 79.00/10.93 | | | | BETA: splitting (100) gives: % 79.00/10.93 | | | | % 79.00/10.93 | | | | Case 1: % 79.00/10.93 | | | | | % 79.00/10.93 | | | | | (115) all_116_0 = all_116_6 % 79.00/10.93 | | | | | % 79.00/10.93 | | | | | REDUCE: (80), (115) imply: % 79.00/10.93 | | | | | (116) $false % 79.00/10.93 | | | | | % 79.00/10.93 | | | | | CLOSE: (116) is inconsistent. % 79.00/10.93 | | | | | % 79.00/10.93 | | | | Case 2: % 79.00/10.93 | | | | | % 79.00/10.93 | | | | | (117) ? [v0: uni] : ? [v1: uni] : ? [v2: any] : ( ~ (v2 = % 79.00/10.93 | | | | | all_116_3) & t2tb2(all_116_7) = v0 & tb2t1(v1) = v2 & % 79.00/10.93 | | | | | get(all_59_0, int, all_56_2, v0) = v1 & option_int(v2) & % 79.00/10.93 | | | | | uni(v1) & uni(v0)) % 79.00/10.93 | | | | | % 79.00/10.93 | | | | | DELTA: instantiating (117) with fresh symbols all_201_0, all_201_1, % 79.00/10.93 | | | | | all_201_2 gives: % 79.00/10.94 | | | | | (118) ~ (all_201_0 = all_116_3) & t2tb2(all_116_7) = all_201_2 & % 79.00/10.94 | | | | | tb2t1(all_201_1) = all_201_0 & get(all_59_0, int, all_56_2, % 79.00/10.94 | | | | | all_201_2) = all_201_1 & option_int(all_201_0) & % 79.00/10.94 | | | | | uni(all_201_1) & uni(all_201_2) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | ALPHA: (118) implies: % 79.00/10.94 | | | | | (119) get(all_59_0, int, all_56_2, all_201_2) = all_201_1 % 79.00/10.94 | | | | | (120) t2tb2(all_116_7) = all_201_2 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | REDUCE: (50), (119) imply: % 79.00/10.94 | | | | | (121) get(all_50_0, int, all_56_2, all_201_2) = all_201_1 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (9) with all_50_0, all_161_0, int, % 79.00/10.94 | | | | | simplifying with (17), (106) gives: % 79.00/10.94 | | | | | (122) all_161_0 = all_50_0 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (11) with all_116_4, all_116_1, all_116_3, % 79.00/10.94 | | | | | simplifying with (95), (96) gives: % 79.00/10.94 | | | | | (123) all_116_1 = all_116_4 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (12) with all_116_5, all_201_2, all_116_7, % 79.00/10.94 | | | | | simplifying with (89), (120) gives: % 79.00/10.94 | | | | | (124) all_201_2 = all_116_5 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (12) with all_196_2, all_201_2, all_116_7, % 79.00/10.94 | | | | | simplifying with (114), (120) gives: % 79.00/10.94 | | | | | (125) all_201_2 = all_196_2 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (13) with all_56_11, all_116_7, all_56_8, % 79.00/10.94 | | | | | simplifying with (60) gives: % 79.00/10.94 | | | | | (126) all_116_7 = all_56_11 | ~ (tb2t2(all_56_8) = all_116_7) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (13) with all_56_6, all_116_6, all_56_5, % 79.00/10.94 | | | | | simplifying with (62) gives: % 79.00/10.94 | | | | | (127) all_116_6 = all_56_6 | ~ (tb2t2(all_56_5) = all_116_6) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | COMBINE_EQS: (124), (125) imply: % 79.00/10.94 | | | | | (128) all_196_2 = all_116_5 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | SIMP: (128) implies: % 79.00/10.94 | | | | | (129) all_196_2 = all_116_5 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | REDUCE: (121), (124) imply: % 79.00/10.94 | | | | | (130) get(all_50_0, int, all_56_2, all_116_5) = all_201_1 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | REDUCE: (84), (123) imply: % 79.00/10.94 | | | | | (131) some(int, all_116_2) = all_116_4 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | REDUCE: (113), (129) imply: % 79.00/10.94 | | | | | (132) uni(all_116_5) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | PRED_UNIFY: (108), (130) imply: % 79.00/10.94 | | | | | (133) ~ (all_201_1 = all_116_4) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (some_proj_1_def) with int, all_116_2, % 79.00/10.94 | | | | | all_116_4, simplifying with (7), (82), (103), (131) % 79.00/10.94 | | | | | gives: % 79.00/10.94 | | | | | (134) some_proj_1(int, all_116_4) = all_116_2 % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | GROUND_INST: instantiating (select_neq) with int, all_50_0, all_56_2, % 79.00/10.94 | | | | | all_56_8, all_116_5, all_201_1, all_56_4, all_56_1, % 79.00/10.94 | | | | | simplifying with (7), (25), (27), (28), (55), (61), (75), % 79.00/10.94 | | | | | (98), (130), (132) gives: % 79.00/10.94 | | | | | (135) all_116_5 = all_56_8 | (get(all_50_0, int, all_56_1, % 79.00/10.94 | | | | | all_116_5) = all_201_1 & uni(all_201_1)) % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | BETA: splitting (135) gives: % 79.00/10.94 | | | | | % 79.00/10.94 | | | | | Case 1: % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | (136) all_116_5 = all_56_8 % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | REDUCE: (97), (136) imply: % 79.00/10.94 | | | | | | (137) tb2t2(all_56_8) = all_116_7 % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | REDUCE: (91), (136) imply: % 79.00/10.94 | | | | | | (138) get(all_50_0, int, all_56_1, all_56_8) = all_116_4 % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | BETA: splitting (94) gives: % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | Case 1: % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | (139) ~ (get(all_50_0, int, all_56_1, all_56_8) = all_116_4) % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | PRED_UNIFY: (138), (139) imply: % 79.00/10.94 | | | | | | | (140) $false % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | CLOSE: (140) is inconsistent. % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | Case 2: % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | (141) all_116_4 = all_56_4 % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | REDUCE: (134), (141) imply: % 79.00/10.94 | | | | | | | (142) some_proj_1(int, all_56_4) = all_116_2 % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | BETA: splitting (126) gives: % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | | Case 1: % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | (143) ~ (tb2t2(all_56_8) = all_116_7) % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | PRED_UNIFY: (137), (143) imply: % 79.00/10.94 | | | | | | | | (144) $false % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | CLOSE: (144) is inconsistent. % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | Case 2: % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | (145) all_116_7 = all_56_11 % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | REDUCE: (85), (145) imply: % 79.00/10.94 | | | | | | | | (146) fib(all_56_11) = all_116_0 % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | BETA: splitting (92) gives: % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | | Case 1: % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | (147) ~ (fib(all_56_11) = all_116_0) % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | PRED_UNIFY: (146), (147) imply: % 79.00/10.94 | | | | | | | | | (148) $false % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | CLOSE: (148) is inconsistent. % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | Case 2: % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | (149) all_116_0 = all_56_6 % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | REDUCE: (80), (149) imply: % 79.00/10.94 | | | | | | | | | (150) ~ (all_116_6 = all_56_6) % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | SIMP: (150) implies: % 79.00/10.94 | | | | | | | | | (151) ~ (all_116_6 = all_56_6) % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | GROUND_INST: instantiating (14) with all_56_5, all_116_2, % 79.00/10.94 | | | | | | | | | all_56_4, int, simplifying with (77), (142) gives: % 79.00/10.94 | | | | | | | | | (152) all_116_2 = all_56_5 % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | REDUCE: (102), (152) imply: % 79.00/10.94 | | | | | | | | | (153) tb2t2(all_56_5) = all_116_6 % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | BETA: splitting (127) gives: % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | | Case 1: % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | (154) ~ (tb2t2(all_56_5) = all_116_6) % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | PRED_UNIFY: (153), (154) imply: % 79.00/10.94 | | | | | | | | | | (155) $false % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | CLOSE: (155) is inconsistent. % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | Case 2: % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | (156) all_116_6 = all_56_6 % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | REDUCE: (151), (156) imply: % 79.00/10.94 | | | | | | | | | | (157) $false % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | | CLOSE: (157) is inconsistent. % 79.00/10.94 | | | | | | | | | | % 79.00/10.94 | | | | | | | | | End of split % 79.00/10.94 | | | | | | | | | % 79.00/10.94 | | | | | | | | End of split % 79.00/10.94 | | | | | | | | % 79.00/10.94 | | | | | | | End of split % 79.00/10.94 | | | | | | | % 79.00/10.94 | | | | | | End of split % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | Case 2: % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | (158) get(all_50_0, int, all_56_1, all_116_5) = all_201_1 & % 79.00/10.94 | | | | | | uni(all_201_1) % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | ALPHA: (158) implies: % 79.00/10.94 | | | | | | (159) get(all_50_0, int, all_56_1, all_116_5) = all_201_1 % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | GROUND_INST: instantiating (15) with all_116_4, all_201_1, % 79.00/10.94 | | | | | | all_116_5, all_56_1, int, all_50_0, simplifying with % 79.00/10.94 | | | | | | (91), (159) gives: % 79.00/10.94 | | | | | | (160) all_201_1 = all_116_4 % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | REDUCE: (133), (160) imply: % 79.00/10.94 | | | | | | (161) $false % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | | CLOSE: (161) is inconsistent. % 79.00/10.94 | | | | | | % 79.00/10.94 | | | | | End of split % 79.00/10.94 | | | | | % 79.00/10.94 | | | | End of split % 79.00/10.94 | | | | % 79.00/10.94 | | | End of split % 79.00/10.94 | | | % 79.00/10.94 | | Case 2: % 79.00/10.94 | | | % 79.00/10.94 | | | (162) fib(all_116_7) = all_116_6 % 79.00/10.94 | | | % 79.00/10.94 | | | GROUND_INST: instantiating (10) with all_116_0, all_116_6, all_116_7, % 79.00/10.94 | | | simplifying with (85), (162) gives: % 79.00/10.94 | | | (163) all_116_0 = all_116_6 % 79.00/10.94 | | | % 79.00/10.94 | | | REDUCE: (80), (163) imply: % 79.00/10.94 | | | (164) $false % 79.00/10.94 | | | % 79.00/10.94 | | | CLOSE: (164) is inconsistent. % 79.00/10.94 | | | % 79.00/10.94 | | End of split % 79.00/10.94 | | % 79.00/10.94 | End of split % 79.00/10.94 | % 79.00/10.94 End of proof % 79.00/10.94 % SZS output end Proof for theBenchmark % 79.00/10.94 % 79.00/10.94 10335ms %------------------------------------------------------------------------------