%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP018+2 : TPTP v8.1.2. Bugfixed v7.5.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n022.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 : Thu Aug 31 04:08:53 EDT 2023 % Result : Theorem 25.66s 4.14s % Output : Proof 26.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ITP018+2 : TPTP v8.1.2. Bugfixed v7.5.0. % 0.11/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.33 % CPULimit : 300 % 0.19/0.33 % WCLimit : 300 % 0.19/0.33 % DateTime : Sun Aug 27 10:21:09 EDT 2023 % 0.19/0.34 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.98/1.14 Prover 1: Preprocessing ... % 2.98/1.14 Prover 4: Preprocessing ... % 3.55/1.18 Prover 6: Preprocessing ... % 3.55/1.18 Prover 2: Preprocessing ... % 3.55/1.18 Prover 0: Preprocessing ... % 3.55/1.18 Prover 3: Preprocessing ... % 3.55/1.18 Prover 5: Preprocessing ... % 6.43/1.66 Prover 1: Constructing countermodel ... % 7.18/1.69 Prover 6: Proving ... % 7.18/1.70 Prover 3: Constructing countermodel ... % 7.64/1.74 Prover 5: Proving ... % 8.36/1.85 Prover 2: Proving ... % 8.85/1.96 Prover 4: Constructing countermodel ... % 9.38/2.02 Prover 0: Proving ... % 12.13/2.36 Prover 3: gave up % 12.13/2.36 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.60/2.41 Prover 7: Preprocessing ... % 14.09/2.60 Prover 7: Constructing countermodel ... % 14.09/2.62 Prover 1: gave up % 14.09/2.63 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 14.43/2.69 Prover 8: Preprocessing ... % 15.31/2.83 Prover 8: Warning: ignoring some quantifiers % 15.31/2.84 Prover 8: Constructing countermodel ... % 19.03/3.28 Prover 8: gave up % 19.03/3.29 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 19.03/3.32 Prover 9: Preprocessing ... % 21.45/3.62 Prover 9: Constructing countermodel ... % 25.66/4.14 Prover 7: Found proof (size 233) % 25.66/4.14 Prover 7: proved (1776ms) % 25.66/4.14 Prover 9: stopped % 25.66/4.14 Prover 6: stopped % 25.66/4.14 Prover 2: stopped % 25.66/4.14 Prover 5: stopped % 25.66/4.14 Prover 4: stopped % 25.66/4.14 Prover 0: stopped % 25.66/4.14 % 25.66/4.14 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 25.66/4.14 % 25.66/4.20 % SZS output start Proof for theBenchmark % 25.66/4.20 Assumptions after simplification: % 25.66/4.20 --------------------------------- % 25.66/4.20 % 25.66/4.20 (ap_tp) % 25.66/4.23 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 25.66/4.23 $i] : ( ~ (ap(v2, v4) = v5) | ~ (arr(v0, v1) = v3) | ~ $i(v4) | ~ $i(v2) % 25.66/4.23 | ~ $i(v1) | ~ $i(v0) | ~ mem(v4, v0) | ~ mem(v2, v3) | mem(v5, v1)) % 25.66/4.23 % 25.66/4.23 (conj_thm_2Ebinary__ieee_2Efloat__to__real__negate) % 25.66/4.24 $i(c_2Erealax_2Ereal__neg) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 25.66/4.24 (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 25.66/4.24 ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 25.66/4.24 (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & % 25.66/4.24 ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & $i(v4) & $i(v3) & ! [v5: $i] : % 25.66/4.24 ! [v6: $i] : ( ~ (ap(v4, v5) = v6) | ~ $i(v5) | ~ mem(v5, v3) | ? [v7: % 25.66/4.24 $i] : ? [v8: $i] : (ap(v2, v6) = v7 & ap(v2, v5) = v8 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v8) = v7 & $i(v8) & $i(v7))) & ! [v5: $i] % 25.66/4.24 : ! [v6: $i] : ( ~ (ap(v2, v5) = v6) | ~ $i(v5) | ~ mem(v5, v3) | ? % 25.66/4.24 [v7: $i] : ? [v8: $i] : (ap(v4, v5) = v7 & ap(v2, v7) = v8 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v6) = v8 & $i(v8) & $i(v7))))) & ! [v0: % 25.66/4.24 $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v0, % 25.66/4.24 v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] % 25.66/4.24 : ? [v4: $i] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4 & % 25.66/4.24 ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & $i(v4) & $i(v3) & ! [v5: $i] : % 25.66/4.24 ! [v6: $i] : ( ~ (ap(v4, v5) = v6) | ~ $i(v5) | ~ mem(v5, v3) | ? [v7: % 25.66/4.24 $i] : ? [v8: $i] : (ap(v4, v7) = v8 & ap(v2, v5) = v7 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v6) = v8 & $i(v8) & $i(v7))) & ! [v5: $i] % 25.66/4.24 : ! [v6: $i] : ( ~ (ap(v2, v5) = v6) | ~ $i(v5) | ~ mem(v5, v3) | ? % 25.66/4.24 [v7: $i] : ? [v8: $i] : (ap(v4, v6) = v7 & ap(v4, v5) = v8 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v8) = v7 & $i(v8) & $i(v7))))) & ! [v0: % 25.66/4.24 $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = % 25.66/4.24 v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? % 25.66/4.24 [v4: $i] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & % 25.66/4.24 c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & $i(v4) & $i(v3) & ! [v5: % 25.66/4.24 $i] : ! [v6: $i] : ( ~ (ap(v4, v5) = v6) | ~ $i(v5) | ~ mem(v5, v2) | % 25.66/4.24 ? [v7: $i] : ? [v8: $i] : (ap(v3, v6) = v7 & ap(v3, v5) = v8 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v8) = v7 & $i(v8) & $i(v7))) & ! [v5: $i] % 25.66/4.24 : ! [v6: $i] : ( ~ (ap(v3, v5) = v6) | ~ $i(v5) | ~ mem(v5, v2) | ? % 25.66/4.24 [v7: $i] : ? [v8: $i] : (ap(v4, v5) = v7 & ap(v3, v7) = v8 & % 25.66/4.24 ap(c_2Erealax_2Ereal__neg, v6) = v8 & $i(v8) & $i(v7))))) % 25.66/4.24 % 25.66/4.24 (conj_thm_2Ebinary__ieee_2Eneg__ulp) % 26.02/4.24 $i(c_2Erealax_2Ereal__neg) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 26.02/4.24 $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 26.02/4.24 ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ( ~ (v12 = v6) & % 26.02/4.24 c_2Ebinary__ieee_2Eulp(v0, v1) = v2 & c_2Ebool_2Ethe__value(v3) = v4 & % 26.02/4.24 c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v7 & % 26.02/4.24 c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v9 & ty_2Epair_2Eprod(v0, v1) % 26.02/4.24 = v3 & c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v8 & ap(v9, v4) = v10 & % 26.02/4.24 ap(v8, v10) = v11 & ap(v7, v11) = v12 & ap(v2, v4) = v5 & % 26.02/4.24 ap(c_2Erealax_2Ereal__neg, v5) = v6 & $i(v12) & $i(v11) & $i(v10) & $i(v9) & % 26.02/4.24 $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 26.02/4.24 $i(v0) & ne(v1) & ne(v0)) % 26.02/4.24 % 26.02/4.24 (conj_thm_2Ebinary__ieee_2Eulp) % 26.02/4.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (c_2Ebinary__ieee_2Eulp(v0, v1) % 26.02/4.25 = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? % 26.02/4.25 [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 26.02/4.25 (c_2Ebool_2Ethe__value(v3) = v4 & c_2Ebinary__ieee_2Efloat__to__real(v0, v1) % 26.02/4.25 = v6 & c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & % 26.02/4.25 ty_2Epair_2Eprod(v0, v1) = v3 & ap(v7, v4) = v8 & ap(v6, v8) = v5 & ap(v2, % 26.02/4.25 v4) = v5 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3))) & ! % 26.02/4.25 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 26.02/4.25 ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 26.02/4.25 : ? [v7: $i] : ? [v8: $i] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & % 26.02/4.25 c_2Ebool_2Ethe__value(v4) = v5 & c_2Ebinary__ieee_2Efloat__plus__min(v0, % 26.02/4.25 v1) = v7 & ty_2Epair_2Eprod(v0, v1) = v4 & ap(v7, v5) = v8 & ap(v3, v5) % 26.02/4.25 = v6 & ap(v2, v8) = v6 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 26.02/4.25 $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 26.02/4.25 ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: % 26.02/4.25 $i] : ? [v7: $i] : ? [v8: $i] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & % 26.02/4.25 c_2Ebool_2Ethe__value(v4) = v5 & c_2Ebinary__ieee_2Efloat__to__real(v0, % 26.02/4.25 v1) = v7 & ty_2Epair_2Eprod(v0, v1) = v4 & ap(v7, v8) = v6 & ap(v3, v5) % 26.02/4.25 = v6 & ap(v2, v5) = v8 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 26.02/4.25 $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (ty_2Epair_2Eprod(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ % 26.02/4.25 ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 26.02/4.25 : ? [v8: $i] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & % 26.02/4.25 c_2Ebool_2Ethe__value(v2) = v4 & c_2Ebinary__ieee_2Efloat__to__real(v0, % 26.02/4.25 v1) = v6 & c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & ap(v7, v4) % 26.02/4.25 = v8 & ap(v6, v8) = v5 & ap(v3, v4) = v5 & $i(v8) & $i(v7) & $i(v6) & % 26.02/4.25 $i(v5) & $i(v4) & $i(v3))) % 26.02/4.25 % 26.02/4.25 (mem_c_2Ebinary__ieee_2Efloat__negate) % 26.02/4.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.25 ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.25 (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, v3) = v4 & $i(v4) & $i(v3) % 26.02/4.25 & mem(v2, v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) % 26.02/4.25 | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v3 & arr(v2, v2) = v4 & $i(v4) & % 26.02/4.25 $i(v3) & mem(v3, v4))) % 26.02/4.25 % 26.02/4.25 (mem_c_2Ebinary__ieee_2Efloat__plus__min) % 26.02/4.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 26.02/4.25 ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: % 26.02/4.25 $i] : (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & % 26.02/4.25 ty_2Ebinary__ieee_2Efloat(v0, v1) = v5 & arr(v4, v5) = v6 & $i(v6) & % 26.02/4.25 $i(v5) & $i(v4) & $i(v3) & mem(v2, v6))) & ! [v0: $i] : ! [v1: $i] : ! % 26.02/4.25 [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.25 ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v3 & ty_2Ebool_2Eitself(v2) = % 26.02/4.25 v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v5 & arr(v4, v5) = v6 & $i(v6) & % 26.02/4.25 $i(v5) & $i(v4) & $i(v3) & mem(v3, v6))) & ! [v0: $i] : ! [v1: $i] : ! % 26.02/4.25 [v2: $i] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.25 $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 26.02/4.25 ? [v6: $i] : (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v3 & % 26.02/4.25 ty_2Ebool_2Eitself(v4) = v5 & ty_2Epair_2Eprod(v0, v1) = v4 & arr(v5, v2) % 26.02/4.25 = v6 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & mem(v3, v6))) % 26.02/4.25 % 26.02/4.25 (mem_c_2Ebinary__ieee_2Efloat__to__real) % 26.02/4.25 $i(ty_2Erealax_2Ereal) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 26.02/4.25 ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.25 (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, ty_2Erealax_2Ereal) = v4 & % 26.02/4.25 $i(v4) & $i(v3) & mem(v2, v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 26.02/4.25 : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.25 ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.25 (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & arr(v2, % 26.02/4.25 ty_2Erealax_2Ereal) = v4 & $i(v4) & $i(v3) & mem(v3, v4))) % 26.02/4.25 % 26.02/4.25 (mem_c_2Ebinary__ieee_2Eulp) % 26.02/4.25 $i(ty_2Erealax_2Ereal) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.25 (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | % 26.02/4.25 ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (ty_2Ebool_2Eitself(v3) % 26.02/4.25 = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & arr(v4, ty_2Erealax_2Ereal) = v5 & % 26.02/4.25 $i(v5) & $i(v4) & $i(v3) & mem(v2, v5))) & ! [v0: $i] : ! [v1: $i] : ! % 26.02/4.25 [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.25 ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 26.02/4.25 (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & ty_2Ebool_2Eitself(v2) = v4 & arr(v4, % 26.02/4.25 ty_2Erealax_2Ereal) = v5 & $i(v5) & $i(v4) & $i(v3) & mem(v3, v5))) % 26.02/4.25 % 26.02/4.25 (mem_c_2Ebool_2Ethe__value) % 26.02/4.25 ! [v0: $i] : ! [v1: $i] : ( ~ (c_2Ebool_2Ethe__value(v0) = v1) | ~ $i(v0) | % 26.02/4.25 ~ ne(v0) | ? [v2: $i] : (ty_2Ebool_2Eitself(v0) = v2 & $i(v2) & mem(v1, % 26.02/4.25 v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | % 26.02/4.25 ~ $i(v0) | ~ ne(v0) | ? [v2: $i] : (c_2Ebool_2Ethe__value(v0) = v2 & % 26.02/4.25 $i(v2) & mem(v2, v1))) % 26.02/4.25 % 26.02/4.25 (ne_ty_2Epair_2Eprod) % 26.02/4.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) % 26.02/4.25 | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ne(v2)) % 26.02/4.25 % 26.02/4.25 (function-axioms) % 26.02/4.26 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.26 (c_2Ebinary__ieee_2Eulp(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Eulp(v3, v2) = % 26.02/4.26 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 26.02/4.26 ~ (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v1) | ~ % 26.02/4.26 (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 26.02/4.26 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.26 (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v1) | ~ % 26.02/4.26 (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 26.02/4.26 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (ty_2Epair_2Eprod(v3, v2) = % 26.02/4.26 v1) | ~ (ty_2Epair_2Eprod(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 26.02/4.26 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, % 26.02/4.26 v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, v2) = v0)) & ! % 26.02/4.26 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.26 (ty_2Ebinary__ieee_2Efloat(v3, v2) = v1) | ~ (ty_2Ebinary__ieee_2Efloat(v3, % 26.02/4.26 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 26.02/4.26 = v0 | ~ (k(v3, v2) = v1) | ~ (k(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 26.02/4.26 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (ap(v3, v2) = v1) | ~ % 26.02/4.26 (ap(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 26.02/4.26 (v1 = v0 | ~ (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) & ! [v0: $i] : ! % 26.02/4.26 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (c_2Ebool_2E_21(v2) = v1) | ~ % 26.02/4.26 (c_2Ebool_2E_21(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 26.02/4.26 v0 | ~ (c_2Emin_2E_3D(v2) = v1) | ~ (c_2Emin_2E_3D(v2) = v0)) & ! [v0: % 26.02/4.26 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (c_2Ebool_2Ethe__value(v2) = % 26.02/4.26 v1) | ~ (c_2Ebool_2Ethe__value(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 26.02/4.26 ! [v2: $i] : (v1 = v0 | ~ (ty_2Ebool_2Eitself(v2) = v1) | ~ % 26.02/4.26 (ty_2Ebool_2Eitself(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 26.02/4.26 (v1 = v0 | ~ (i(v2) = v1) | ~ (i(v2) = v0)) % 26.02/4.26 % 26.02/4.26 Further assumptions not needed in the proof: % 26.02/4.26 -------------------------------------------- % 26.02/4.26 arr_ne, ax_all_p, ax_eq_p, ax_true_p, bool_ne, boolext, % 26.02/4.26 conj_thm_2Ebool_2EREFL__CLAUSE, conj_thm_2Ebool_2ETRUTH, funcext, ibeta, ind_ne, % 26.02/4.26 kbeta, mem_c_2Ebool_2ET, mem_c_2Ebool_2E_21, mem_c_2Emin_2E_3D, % 26.02/4.26 mem_c_2Erealax_2Ereal__neg, ne_ty_2Ebinary__ieee_2Efloat, ne_ty_2Ebool_2Eitself, % 26.02/4.26 ne_ty_2Erealax_2Ereal % 26.02/4.26 % 26.02/4.26 Those formulas are unsatisfiable: % 26.02/4.26 --------------------------------- % 26.02/4.26 % 26.02/4.26 Begin of proof % 26.02/4.26 | % 26.02/4.26 | ALPHA: (mem_c_2Ebinary__ieee_2Efloat__negate) implies: % 26.02/4.26 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.26 | (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.26 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.26 | (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, v3) = v4 & $i(v4) & % 26.02/4.26 | $i(v3) & mem(v2, v4))) % 26.02/4.26 | % 26.02/4.26 | ALPHA: (mem_c_2Ebinary__ieee_2Efloat__plus__min) implies: % 26.02/4.26 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.26 | (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.26 | ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? % 26.02/4.26 | [v6: $i] : (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v3 & % 26.02/4.26 | ty_2Ebool_2Eitself(v4) = v5 & ty_2Epair_2Eprod(v0, v1) = v4 & % 26.02/4.26 | arr(v5, v2) = v6 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & mem(v3, % 26.02/4.26 | v6))) % 26.02/4.26 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, v1) % 26.02/4.26 | = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] % 26.02/4.26 | : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 26.02/4.26 | (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v3 & % 26.02/4.26 | ty_2Ebool_2Eitself(v2) = v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = % 26.02/4.26 | v5 & arr(v4, v5) = v6 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & mem(v3, % 26.02/4.26 | v6))) % 26.02/4.26 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.26 | (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.26 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 26.02/4.26 | $i] : ? [v6: $i] : (ty_2Ebool_2Eitself(v3) = v4 & % 26.02/4.26 | ty_2Epair_2Eprod(v0, v1) = v3 & ty_2Ebinary__ieee_2Efloat(v0, v1) = % 26.02/4.26 | v5 & arr(v4, v5) = v6 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & mem(v2, % 26.02/4.26 | v6))) % 26.02/4.26 | % 26.02/4.26 | ALPHA: (mem_c_2Ebinary__ieee_2Efloat__to__real) implies: % 26.02/4.27 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.27 | (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, ty_2Erealax_2Ereal) % 26.02/4.27 | = v4 & $i(v4) & $i(v3) & mem(v2, v4))) % 26.02/4.27 | % 26.02/4.27 | ALPHA: (mem_c_2Ebool_2Ethe__value) implies: % 26.02/4.27 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v0) | ? [v2: $i] : (c_2Ebool_2Ethe__value(v0) = v2 & % 26.02/4.27 | $i(v2) & mem(v2, v1))) % 26.02/4.27 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (c_2Ebool_2Ethe__value(v0) = v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v0) | ? [v2: $i] : (ty_2Ebool_2Eitself(v0) = v2 & % 26.02/4.27 | $i(v2) & mem(v1, v2))) % 26.02/4.27 | % 26.02/4.27 | ALPHA: (mem_c_2Ebinary__ieee_2Eulp) implies: % 26.02/4.27 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, v1) % 26.02/4.27 | = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] % 26.02/4.27 | : ? [v4: $i] : ? [v5: $i] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & % 26.02/4.27 | ty_2Ebool_2Eitself(v2) = v4 & arr(v4, ty_2Erealax_2Ereal) = v5 & % 26.02/4.27 | $i(v5) & $i(v4) & $i(v3) & mem(v3, v5))) % 26.02/4.27 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.27 | ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 26.02/4.27 | (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & % 26.02/4.27 | arr(v4, ty_2Erealax_2Ereal) = v5 & $i(v5) & $i(v4) & $i(v3) & % 26.02/4.27 | mem(v2, v5))) % 26.02/4.27 | % 26.02/4.27 | ALPHA: (conj_thm_2Ebinary__ieee_2Efloat__to__real__negate) implies: % 26.02/4.27 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4 & % 26.02/4.27 | ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & $i(v4) & $i(v3) & ! [v5: % 26.02/4.27 | $i] : ! [v6: $i] : ( ~ (ap(v4, v5) = v6) | ~ $i(v5) | ~ % 26.02/4.27 | mem(v5, v3) | ? [v7: $i] : ? [v8: $i] : (ap(v4, v7) = v8 & % 26.02/4.27 | ap(v2, v5) = v7 & ap(c_2Erealax_2Ereal__neg, v6) = v8 & $i(v8) % 26.02/4.27 | & $i(v7))) & ! [v5: $i] : ! [v6: $i] : ( ~ (ap(v2, v5) = v6) % 26.02/4.27 | | ~ $i(v5) | ~ mem(v5, v3) | ? [v7: $i] : ? [v8: $i] : % 26.02/4.27 | (ap(v4, v6) = v7 & ap(v4, v5) = v8 & ap(c_2Erealax_2Ereal__neg, % 26.02/4.27 | v8) = v7 & $i(v8) & $i(v7))))) % 26.02/4.27 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & % 26.02/4.27 | ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & $i(v4) & $i(v3) & ! [v5: % 26.02/4.27 | $i] : ! [v6: $i] : ( ~ (ap(v4, v5) = v6) | ~ $i(v5) | ~ % 26.02/4.27 | mem(v5, v3) | ? [v7: $i] : ? [v8: $i] : (ap(v2, v6) = v7 & % 26.02/4.27 | ap(v2, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7 & $i(v8) % 26.02/4.27 | & $i(v7))) & ! [v5: $i] : ! [v6: $i] : ( ~ (ap(v2, v5) = v6) % 26.02/4.27 | | ~ $i(v5) | ~ mem(v5, v3) | ? [v7: $i] : ? [v8: $i] : % 26.02/4.27 | (ap(v4, v5) = v7 & ap(v2, v7) = v8 & ap(c_2Erealax_2Ereal__neg, % 26.02/4.27 | v6) = v8 & $i(v8) & $i(v7))))) % 26.02/4.27 | % 26.02/4.27 | ALPHA: (conj_thm_2Ebinary__ieee_2Eulp) implies: % 26.02/4.27 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ty_2Epair_2Eprod(v0, % 26.02/4.27 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ ne(v1) | ~ ne(v0) | ? % 26.02/4.27 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 26.02/4.27 | ? [v8: $i] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & % 26.02/4.27 | c_2Ebool_2Ethe__value(v2) = v4 & % 26.02/4.27 | c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v6 & % 26.02/4.27 | c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & ap(v7, v4) = v8 % 26.02/4.27 | & ap(v6, v8) = v5 & ap(v3, v4) = v5 & $i(v8) & $i(v7) & $i(v6) & % 26.02/4.27 | $i(v5) & $i(v4) & $i(v3))) % 26.02/4.27 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 26.02/4.27 | $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 26.02/4.27 | (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & c_2Ebool_2Ethe__value(v4) = % 26.02/4.27 | v5 & c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v7 & % 26.02/4.27 | ty_2Epair_2Eprod(v0, v1) = v4 & ap(v7, v8) = v6 & ap(v3, v5) = v6 % 26.02/4.27 | & ap(v2, v5) = v8 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 26.02/4.27 | $i(v3))) % 26.02/4.27 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.27 | (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ $i(v1) | ~ % 26.02/4.27 | $i(v0) | ~ ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 26.02/4.27 | $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 26.02/4.27 | (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & c_2Ebool_2Ethe__value(v4) = % 26.02/4.27 | v5 & c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & % 26.02/4.27 | ty_2Epair_2Eprod(v0, v1) = v4 & ap(v7, v5) = v8 & ap(v3, v5) = v6 % 26.02/4.27 | & ap(v2, v8) = v6 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 26.02/4.27 | $i(v3))) % 26.02/4.28 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 26.02/4.28 | ne(v1) | ~ ne(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? % 26.02/4.28 | [v6: $i] : ? [v7: $i] : ? [v8: $i] : (c_2Ebool_2Ethe__value(v3) = % 26.02/4.28 | v4 & c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v6 & % 26.02/4.28 | c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & % 26.02/4.28 | ty_2Epair_2Eprod(v0, v1) = v3 & ap(v7, v4) = v8 & ap(v6, v8) = v5 % 26.02/4.28 | & ap(v2, v4) = v5 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 26.02/4.28 | $i(v3))) % 26.02/4.28 | % 26.02/4.28 | ALPHA: (conj_thm_2Ebinary__ieee_2Eneg__ulp) implies: % 26.02/4.28 | (16) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 26.02/4.28 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 26.02/4.28 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ( ~ (v12 = v6) & % 26.02/4.28 | c_2Ebinary__ieee_2Eulp(v0, v1) = v2 & c_2Ebool_2Ethe__value(v3) = v4 % 26.02/4.28 | & c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v7 & % 26.02/4.28 | c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v9 & % 26.02/4.28 | ty_2Epair_2Eprod(v0, v1) = v3 & c_2Ebinary__ieee_2Efloat__negate(v0, % 26.02/4.28 | v1) = v8 & ap(v9, v4) = v10 & ap(v8, v10) = v11 & ap(v7, v11) = % 26.02/4.28 | v12 & ap(v2, v4) = v5 & ap(c_2Erealax_2Ereal__neg, v5) = v6 & % 26.02/4.28 | $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 26.02/4.28 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ne(v1) & % 26.02/4.28 | ne(v0)) % 26.02/4.28 | % 26.02/4.28 | ALPHA: (function-axioms) implies: % 26.02/4.28 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 26.02/4.28 | (ty_2Ebool_2Eitself(v2) = v1) | ~ (ty_2Ebool_2Eitself(v2) = v0)) % 26.02/4.28 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 26.02/4.28 | (c_2Ebool_2Ethe__value(v2) = v1) | ~ (c_2Ebool_2Ethe__value(v2) = % 26.02/4.28 | v0)) % 26.02/4.28 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) % 26.02/4.28 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (ap(v3, v2) = v1) | ~ (ap(v3, v2) = v0)) % 26.02/4.28 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (ty_2Ebinary__ieee_2Efloat(v3, v2) = v1) | ~ % 26.02/4.28 | (ty_2Ebinary__ieee_2Efloat(v3, v2) = v0)) % 26.02/4.28 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (ty_2Epair_2Eprod(v3, v2) = v1) | ~ (ty_2Epair_2Eprod(v3, v2) = % 26.02/4.28 | v0)) % 26.02/4.28 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v1) | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v0)) % 26.02/4.28 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v1) | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v0)) % 26.02/4.28 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Eulp(v3, v2) = v1) | ~ % 26.02/4.28 | (c_2Ebinary__ieee_2Eulp(v3, v2) = v0)) % 26.02/4.28 | % 26.02/4.28 | DELTA: instantiating (16) with fresh symbols all_26_0, all_26_1, all_26_2, % 26.02/4.28 | all_26_3, all_26_4, all_26_5, all_26_6, all_26_7, all_26_8, all_26_9, % 26.02/4.28 | all_26_10, all_26_11, all_26_12 gives: % 26.02/4.28 | (26) ~ (all_26_0 = all_26_6) & c_2Ebinary__ieee_2Eulp(all_26_12, % 26.02/4.28 | all_26_11) = all_26_10 & c_2Ebool_2Ethe__value(all_26_9) = all_26_8 % 26.02/4.28 | & c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_26_5 % 26.02/4.28 | & c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_26_3 % 26.02/4.28 | & ty_2Epair_2Eprod(all_26_12, all_26_11) = all_26_9 & % 26.02/4.28 | c_2Ebinary__ieee_2Efloat__negate(all_26_12, all_26_11) = all_26_4 & % 26.02/4.28 | ap(all_26_3, all_26_8) = all_26_2 & ap(all_26_4, all_26_2) = all_26_1 % 26.02/4.28 | & ap(all_26_5, all_26_1) = all_26_0 & ap(all_26_10, all_26_8) = % 26.02/4.28 | all_26_7 & ap(c_2Erealax_2Ereal__neg, all_26_7) = all_26_6 & % 26.02/4.28 | $i(all_26_0) & $i(all_26_1) & $i(all_26_2) & $i(all_26_3) & % 26.02/4.28 | $i(all_26_4) & $i(all_26_5) & $i(all_26_6) & $i(all_26_7) & % 26.02/4.28 | $i(all_26_8) & $i(all_26_9) & $i(all_26_10) & $i(all_26_11) & % 26.02/4.28 | $i(all_26_12) & ne(all_26_11) & ne(all_26_12) % 26.02/4.28 | % 26.02/4.28 | ALPHA: (26) implies: % 26.02/4.28 | (27) ~ (all_26_0 = all_26_6) % 26.02/4.28 | (28) ne(all_26_12) % 26.02/4.28 | (29) ne(all_26_11) % 26.02/4.28 | (30) $i(all_26_12) % 26.02/4.28 | (31) $i(all_26_11) % 26.02/4.28 | (32) ap(c_2Erealax_2Ereal__neg, all_26_7) = all_26_6 % 26.02/4.29 | (33) ap(all_26_10, all_26_8) = all_26_7 % 26.02/4.29 | (34) ap(all_26_5, all_26_1) = all_26_0 % 26.02/4.29 | (35) ap(all_26_4, all_26_2) = all_26_1 % 26.02/4.29 | (36) ap(all_26_3, all_26_8) = all_26_2 % 26.02/4.29 | (37) c_2Ebinary__ieee_2Efloat__negate(all_26_12, all_26_11) = all_26_4 % 26.02/4.29 | (38) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_26_9 % 26.02/4.29 | (39) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_26_3 % 26.02/4.29 | (40) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_26_5 % 26.02/4.29 | (41) c_2Ebool_2Ethe__value(all_26_9) = all_26_8 % 26.02/4.29 | (42) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_26_10 % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (10) with all_26_12, all_26_11, all_26_4, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (37) gives: % 26.02/4.29 | (43) ? [v0: $i] : ? [v1: $i] : % 26.02/4.29 | (c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = v1 & % 26.02/4.29 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = v0 & $i(v1) & % 26.02/4.29 | $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ (ap(v1, v2) = v3) | ~ % 26.02/4.29 | $i(v2) | ~ mem(v2, v0) | ? [v4: $i] : ? [v5: $i] : (ap(v1, v4) % 26.02/4.29 | = v5 & ap(all_26_4, v2) = v4 & ap(c_2Erealax_2Ereal__neg, v3) = % 26.02/4.29 | v5 & $i(v5) & $i(v4))) & ! [v2: $i] : ! [v3: $i] : ( ~ % 26.02/4.29 | (ap(all_26_4, v2) = v3) | ~ $i(v2) | ~ mem(v2, v0) | ? [v4: $i] % 26.02/4.29 | : ? [v5: $i] : (ap(v1, v3) = v4 & ap(v1, v2) = v5 & % 26.02/4.29 | ap(c_2Erealax_2Ereal__neg, v5) = v4 & $i(v5) & $i(v4)))) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (1) with all_26_12, all_26_11, all_26_4, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (37) gives: % 26.02/4.29 | (44) ? [v0: $i] : ? [v1: $i] : (ty_2Ebinary__ieee_2Efloat(all_26_12, % 26.02/4.29 | all_26_11) = v0 & arr(v0, v0) = v1 & $i(v1) & $i(v0) & % 26.02/4.29 | mem(all_26_4, v1)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (ne_ty_2Epair_2Eprod) with all_26_12, all_26_11, % 26.02/4.29 | all_26_9, simplifying with (28), (29), (30), (31), (38) gives: % 26.02/4.29 | (45) ne(all_26_9) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (12) with all_26_12, all_26_11, all_26_9, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (38) gives: % 26.02/4.29 | (46) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 26.02/4.29 | ? [v5: $i] : (c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = v0 & % 26.02/4.29 | c_2Ebool_2Ethe__value(all_26_9) = v1 & % 26.02/4.29 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = v3 & % 26.02/4.29 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = v4 & % 26.02/4.29 | ap(v4, v1) = v5 & ap(v3, v5) = v2 & ap(v0, v1) = v2 & $i(v5) & % 26.02/4.29 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (3) with all_26_12, all_26_11, all_26_9, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (38) gives: % 26.02/4.29 | (47) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 26.02/4.29 | (c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = v0 & % 26.02/4.29 | ty_2Ebool_2Eitself(all_26_9) = v1 & % 26.02/4.29 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = v2 & arr(v1, v2) = % 26.02/4.29 | v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & mem(v0, v3)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (8) with all_26_12, all_26_11, all_26_9, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (38) gives: % 26.02/4.29 | (48) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 26.02/4.29 | (c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = v0 & % 26.02/4.29 | ty_2Ebool_2Eitself(all_26_9) = v1 & arr(v1, ty_2Erealax_2Ereal) = v2 % 26.02/4.29 | & $i(v2) & $i(v1) & $i(v0) & mem(v0, v2)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (13) with all_26_12, all_26_11, all_26_3, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (39) gives: % 26.02/4.29 | (49) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 26.02/4.29 | ? [v5: $i] : (c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = v0 & % 26.02/4.29 | c_2Ebool_2Ethe__value(v1) = v2 & % 26.02/4.29 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = v4 & % 26.02/4.29 | ty_2Epair_2Eprod(all_26_12, all_26_11) = v1 & ap(v4, v5) = v3 & % 26.02/4.29 | ap(v0, v2) = v3 & ap(all_26_3, v2) = v5 & $i(v5) & $i(v4) & $i(v3) & % 26.02/4.29 | $i(v2) & $i(v1) & $i(v0)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (4) with all_26_12, all_26_11, all_26_3, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (39) gives: % 26.02/4.29 | (50) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 26.02/4.29 | (ty_2Ebool_2Eitself(v0) = v1 & ty_2Epair_2Eprod(all_26_12, all_26_11) % 26.02/4.29 | = v0 & ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = v2 & % 26.02/4.29 | arr(v1, v2) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & mem(all_26_3, % 26.02/4.29 | v3)) % 26.02/4.29 | % 26.02/4.29 | GROUND_INST: instantiating (14) with all_26_12, all_26_11, all_26_5, % 26.02/4.29 | simplifying with (28), (29), (30), (31), (40) gives: % 26.02/4.30 | (51) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 26.02/4.30 | ? [v5: $i] : (c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = v0 & % 26.02/4.30 | c_2Ebool_2Ethe__value(v1) = v2 & % 26.02/4.30 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = v4 & % 26.02/4.30 | ty_2Epair_2Eprod(all_26_12, all_26_11) = v1 & ap(v4, v2) = v5 & % 26.02/4.30 | ap(v0, v2) = v3 & ap(all_26_5, v5) = v3 & $i(v5) & $i(v4) & $i(v3) & % 26.02/4.30 | $i(v2) & $i(v1) & $i(v0)) % 26.02/4.30 | % 26.02/4.30 | GROUND_INST: instantiating (11) with all_26_12, all_26_11, all_26_5, % 26.02/4.30 | simplifying with (28), (29), (30), (31), (40) gives: % 26.02/4.30 | (52) ? [v0: $i] : ? [v1: $i] : % 26.02/4.30 | (c_2Ebinary__ieee_2Efloat__negate(all_26_12, all_26_11) = v1 & % 26.02/4.30 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = v0 & $i(v1) & % 26.02/4.30 | $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ (ap(v1, v2) = v3) | ~ % 26.02/4.30 | $i(v2) | ~ mem(v2, v0) | ? [v4: $i] : ? [v5: $i] : % 26.02/4.30 | (ap(all_26_5, v3) = v4 & ap(all_26_5, v2) = v5 & % 26.02/4.30 | ap(c_2Erealax_2Ereal__neg, v5) = v4 & $i(v5) & $i(v4))) & ! % 26.02/4.30 | [v2: $i] : ! [v3: $i] : ( ~ (ap(all_26_5, v2) = v3) | ~ $i(v2) | % 26.02/4.30 | ~ mem(v2, v0) | ? [v4: $i] : ? [v5: $i] : (ap(v1, v2) = v4 & % 26.02/4.30 | ap(all_26_5, v4) = v5 & ap(c_2Erealax_2Ereal__neg, v3) = v5 & % 26.02/4.30 | $i(v5) & $i(v4)))) % 26.02/4.30 | % 26.02/4.30 | GROUND_INST: instantiating (5) with all_26_12, all_26_11, all_26_5, % 26.02/4.30 | simplifying with (28), (29), (30), (31), (40) gives: % 26.02/4.30 | (53) ? [v0: $i] : ? [v1: $i] : (ty_2Ebinary__ieee_2Efloat(all_26_12, % 26.02/4.30 | all_26_11) = v0 & arr(v0, ty_2Erealax_2Ereal) = v1 & $i(v1) & % 26.02/4.30 | $i(v0) & mem(all_26_5, v1)) % 26.02/4.30 | % 26.02/4.30 | GROUND_INST: instantiating (15) with all_26_12, all_26_11, all_26_10, % 26.02/4.30 | simplifying with (28), (29), (30), (31), (42) gives: % 26.02/4.30 | (54) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 26.02/4.30 | ? [v5: $i] : (c_2Ebool_2Ethe__value(v0) = v1 & % 26.02/4.30 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = v3 & % 26.02/4.30 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = v4 & % 26.02/4.30 | ty_2Epair_2Eprod(all_26_12, all_26_11) = v0 & ap(v4, v1) = v5 & % 26.02/4.30 | ap(v3, v5) = v2 & ap(all_26_10, v1) = v2 & $i(v5) & $i(v4) & $i(v3) % 26.02/4.30 | & $i(v2) & $i(v1) & $i(v0)) % 26.02/4.30 | % 26.02/4.30 | GROUND_INST: instantiating (9) with all_26_12, all_26_11, all_26_10, % 26.02/4.30 | simplifying with (28), (29), (30), (31), (42) gives: % 26.02/4.30 | (55) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (ty_2Ebool_2Eitself(v0) = v1 % 26.02/4.30 | & ty_2Epair_2Eprod(all_26_12, all_26_11) = v0 & arr(v1, % 26.02/4.30 | ty_2Erealax_2Ereal) = v2 & $i(v2) & $i(v1) & $i(v0) & % 26.02/4.30 | mem(all_26_10, v2)) % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (53) with fresh symbols all_34_0, all_34_1 gives: % 26.02/4.30 | (56) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_34_1 & % 26.02/4.30 | arr(all_34_1, ty_2Erealax_2Ereal) = all_34_0 & $i(all_34_0) & % 26.02/4.30 | $i(all_34_1) & mem(all_26_5, all_34_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (56) implies: % 26.02/4.30 | (57) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_34_1 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (44) with fresh symbols all_36_0, all_36_1 gives: % 26.02/4.30 | (58) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_36_1 & % 26.02/4.30 | arr(all_36_1, all_36_1) = all_36_0 & $i(all_36_0) & $i(all_36_1) & % 26.02/4.30 | mem(all_26_4, all_36_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (58) implies: % 26.02/4.30 | (59) $i(all_36_1) % 26.02/4.30 | (60) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_36_1 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (48) with fresh symbols all_38_0, all_38_1, all_38_2 % 26.02/4.30 | gives: % 26.02/4.30 | (61) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_38_2 & % 26.02/4.30 | ty_2Ebool_2Eitself(all_26_9) = all_38_1 & arr(all_38_1, % 26.02/4.30 | ty_2Erealax_2Ereal) = all_38_0 & $i(all_38_0) & $i(all_38_1) & % 26.02/4.30 | $i(all_38_2) & mem(all_38_2, all_38_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (61) implies: % 26.02/4.30 | (62) ty_2Ebool_2Eitself(all_26_9) = all_38_1 % 26.02/4.30 | (63) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_38_2 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (55) with fresh symbols all_40_0, all_40_1, all_40_2 % 26.02/4.30 | gives: % 26.02/4.30 | (64) ty_2Ebool_2Eitself(all_40_2) = all_40_1 & ty_2Epair_2Eprod(all_26_12, % 26.02/4.30 | all_26_11) = all_40_2 & arr(all_40_1, ty_2Erealax_2Ereal) = all_40_0 % 26.02/4.30 | & $i(all_40_0) & $i(all_40_1) & $i(all_40_2) & mem(all_26_10, % 26.02/4.30 | all_40_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (64) implies: % 26.02/4.30 | (65) $i(all_40_2) % 26.02/4.30 | (66) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_40_2 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (50) with fresh symbols all_42_0, all_42_1, all_42_2, % 26.02/4.30 | all_42_3 gives: % 26.02/4.30 | (67) ty_2Ebool_2Eitself(all_42_3) = all_42_2 & ty_2Epair_2Eprod(all_26_12, % 26.02/4.30 | all_26_11) = all_42_3 & ty_2Ebinary__ieee_2Efloat(all_26_12, % 26.02/4.30 | all_26_11) = all_42_1 & arr(all_42_2, all_42_1) = all_42_0 & % 26.02/4.30 | $i(all_42_0) & $i(all_42_1) & $i(all_42_2) & $i(all_42_3) & % 26.02/4.30 | mem(all_26_3, all_42_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (67) implies: % 26.02/4.30 | (68) arr(all_42_2, all_42_1) = all_42_0 % 26.02/4.30 | (69) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_42_1 % 26.02/4.30 | (70) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_42_3 % 26.02/4.30 | (71) ty_2Ebool_2Eitself(all_42_3) = all_42_2 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (47) with fresh symbols all_44_0, all_44_1, all_44_2, % 26.02/4.30 | all_44_3 gives: % 26.02/4.30 | (72) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_44_3 & % 26.02/4.30 | ty_2Ebool_2Eitself(all_26_9) = all_44_2 & % 26.02/4.30 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_44_1 & % 26.02/4.30 | arr(all_44_2, all_44_1) = all_44_0 & $i(all_44_0) & $i(all_44_1) & % 26.02/4.30 | $i(all_44_2) & $i(all_44_3) & mem(all_44_3, all_44_0) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (72) implies: % 26.02/4.30 | (73) mem(all_44_3, all_44_0) % 26.02/4.30 | (74) arr(all_44_2, all_44_1) = all_44_0 % 26.02/4.30 | (75) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_44_1 % 26.02/4.30 | (76) ty_2Ebool_2Eitself(all_26_9) = all_44_2 % 26.02/4.30 | (77) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_44_3 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (46) with fresh symbols all_46_0, all_46_1, all_46_2, % 26.02/4.30 | all_46_3, all_46_4, all_46_5 gives: % 26.02/4.30 | (78) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_46_5 & % 26.02/4.30 | c_2Ebool_2Ethe__value(all_26_9) = all_46_4 & % 26.02/4.30 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_46_2 & % 26.02/4.30 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_46_1 & % 26.02/4.30 | ap(all_46_1, all_46_4) = all_46_0 & ap(all_46_2, all_46_0) = all_46_3 % 26.02/4.30 | & ap(all_46_5, all_46_4) = all_46_3 & $i(all_46_0) & $i(all_46_1) & % 26.02/4.30 | $i(all_46_2) & $i(all_46_3) & $i(all_46_4) & $i(all_46_5) % 26.02/4.30 | % 26.02/4.30 | ALPHA: (78) implies: % 26.02/4.30 | (79) $i(all_46_0) % 26.02/4.30 | (80) ap(all_46_5, all_46_4) = all_46_3 % 26.02/4.30 | (81) ap(all_46_1, all_46_4) = all_46_0 % 26.02/4.30 | (82) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_46_1 % 26.02/4.30 | (83) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_46_2 % 26.02/4.30 | (84) c_2Ebool_2Ethe__value(all_26_9) = all_46_4 % 26.02/4.30 | (85) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_46_5 % 26.02/4.30 | % 26.02/4.30 | DELTA: instantiating (49) with fresh symbols all_48_0, all_48_1, all_48_2, % 26.02/4.30 | all_48_3, all_48_4, all_48_5 gives: % 26.02/4.30 | (86) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_48_5 & % 26.02/4.30 | c_2Ebool_2Ethe__value(all_48_4) = all_48_3 & % 26.02/4.31 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_48_1 & % 26.02/4.31 | ty_2Epair_2Eprod(all_26_12, all_26_11) = all_48_4 & ap(all_48_1, % 26.02/4.31 | all_48_0) = all_48_2 & ap(all_48_5, all_48_3) = all_48_2 & % 26.02/4.31 | ap(all_26_3, all_48_3) = all_48_0 & $i(all_48_0) & $i(all_48_1) & % 26.02/4.31 | $i(all_48_2) & $i(all_48_3) & $i(all_48_4) & $i(all_48_5) % 26.02/4.31 | % 26.02/4.31 | ALPHA: (86) implies: % 26.02/4.31 | (87) ap(all_26_3, all_48_3) = all_48_0 % 26.02/4.31 | (88) ap(all_48_5, all_48_3) = all_48_2 % 26.02/4.31 | (89) ap(all_48_1, all_48_0) = all_48_2 % 26.02/4.31 | (90) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_48_4 % 26.02/4.31 | (91) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_48_1 % 26.02/4.31 | (92) c_2Ebool_2Ethe__value(all_48_4) = all_48_3 % 26.02/4.31 | (93) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_48_5 % 26.02/4.31 | % 26.02/4.31 | DELTA: instantiating (54) with fresh symbols all_50_0, all_50_1, all_50_2, % 26.02/4.31 | all_50_3, all_50_4, all_50_5 gives: % 26.02/4.31 | (94) c_2Ebool_2Ethe__value(all_50_5) = all_50_4 & % 26.02/4.31 | c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_50_2 & % 26.02/4.31 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_50_1 & % 26.02/4.31 | ty_2Epair_2Eprod(all_26_12, all_26_11) = all_50_5 & ap(all_50_1, % 26.02/4.31 | all_50_4) = all_50_0 & ap(all_50_2, all_50_0) = all_50_3 & % 26.02/4.31 | ap(all_26_10, all_50_4) = all_50_3 & $i(all_50_0) & $i(all_50_1) & % 26.02/4.31 | $i(all_50_2) & $i(all_50_3) & $i(all_50_4) & $i(all_50_5) % 26.02/4.31 | % 26.02/4.31 | ALPHA: (94) implies: % 26.02/4.31 | (95) ap(all_26_10, all_50_4) = all_50_3 % 26.02/4.31 | (96) ap(all_50_1, all_50_4) = all_50_0 % 26.49/4.31 | (97) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_50_5 % 26.49/4.31 | (98) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_50_1 % 26.49/4.31 | (99) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_50_2 % 26.49/4.31 | (100) c_2Ebool_2Ethe__value(all_50_5) = all_50_4 % 26.49/4.31 | % 26.49/4.31 | DELTA: instantiating (51) with fresh symbols all_52_0, all_52_1, all_52_2, % 26.49/4.31 | all_52_3, all_52_4, all_52_5 gives: % 26.49/4.31 | (101) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_52_5 & % 26.49/4.31 | c_2Ebool_2Ethe__value(all_52_4) = all_52_3 & % 26.49/4.31 | c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_52_1 % 26.49/4.31 | & ty_2Epair_2Eprod(all_26_12, all_26_11) = all_52_4 & ap(all_52_1, % 26.49/4.31 | all_52_3) = all_52_0 & ap(all_52_5, all_52_3) = all_52_2 & % 26.49/4.31 | ap(all_26_5, all_52_0) = all_52_2 & $i(all_52_0) & $i(all_52_1) & % 26.49/4.31 | $i(all_52_2) & $i(all_52_3) & $i(all_52_4) & $i(all_52_5) % 26.49/4.31 | % 26.49/4.31 | ALPHA: (101) implies: % 26.49/4.31 | (102) ap(all_52_5, all_52_3) = all_52_2 % 26.49/4.31 | (103) ap(all_52_1, all_52_3) = all_52_0 % 26.49/4.31 | (104) ty_2Epair_2Eprod(all_26_12, all_26_11) = all_52_4 % 26.49/4.31 | (105) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = all_52_1 % 26.49/4.31 | (106) c_2Ebool_2Ethe__value(all_52_4) = all_52_3 % 26.49/4.31 | (107) c_2Ebinary__ieee_2Eulp(all_26_12, all_26_11) = all_52_5 % 26.49/4.31 | % 26.49/4.31 | DELTA: instantiating (52) with fresh symbols all_54_0, all_54_1 gives: % 26.49/4.31 | (108) c_2Ebinary__ieee_2Efloat__negate(all_26_12, all_26_11) = all_54_0 & % 26.49/4.31 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_54_1 & % 26.49/4.31 | $i(all_54_0) & $i(all_54_1) & ! [v0: $i] : ! [v1: $i] : ( ~ % 26.49/4.31 | (ap(all_54_0, v0) = v1) | ~ $i(v0) | ~ mem(v0, all_54_1) | ? % 26.49/4.31 | [v2: $i] : ? [v3: $i] : (ap(all_26_5, v1) = v2 & ap(all_26_5, v0) % 26.49/4.31 | = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2 & $i(v3) & $i(v2))) & % 26.49/4.31 | ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_26_5, v0) = v1) | ~ $i(v0) | % 26.49/4.31 | ~ mem(v0, all_54_1) | ? [v2: $i] : ? [v3: $i] : (ap(all_54_0, v0) % 26.49/4.31 | = v2 & ap(all_26_5, v2) = v3 & ap(c_2Erealax_2Ereal__neg, v1) = % 26.49/4.31 | v3 & $i(v3) & $i(v2))) % 26.49/4.31 | % 26.49/4.31 | ALPHA: (108) implies: % 26.49/4.31 | (109) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_54_1 % 26.49/4.31 | % 26.49/4.31 | DELTA: instantiating (43) with fresh symbols all_57_0, all_57_1 gives: % 26.49/4.31 | (110) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_57_0 & % 26.49/4.31 | ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_57_1 & % 26.49/4.31 | $i(all_57_0) & $i(all_57_1) & ! [v0: $i] : ! [v1: $i] : ( ~ % 26.49/4.31 | (ap(all_57_0, v0) = v1) | ~ $i(v0) | ~ mem(v0, all_57_1) | ? % 26.49/4.31 | [v2: $i] : ? [v3: $i] : (ap(all_57_0, v2) = v3 & ap(all_26_4, v0) % 26.49/4.31 | = v2 & ap(c_2Erealax_2Ereal__neg, v1) = v3 & $i(v3) & $i(v2))) & % 26.49/4.31 | ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_26_4, v0) = v1) | ~ $i(v0) | % 26.49/4.31 | ~ mem(v0, all_57_1) | ? [v2: $i] : ? [v3: $i] : (ap(all_57_0, v1) % 26.49/4.31 | = v2 & ap(all_57_0, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = % 26.49/4.31 | v2 & $i(v3) & $i(v2))) % 26.49/4.31 | % 26.49/4.31 | ALPHA: (110) implies: % 26.49/4.31 | (111) ty_2Ebinary__ieee_2Efloat(all_26_12, all_26_11) = all_57_1 % 26.49/4.31 | (112) c_2Ebinary__ieee_2Efloat__to__real(all_26_12, all_26_11) = all_57_0 % 26.49/4.31 | (113) ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_26_4, v0) = v1) | ~ $i(v0) | % 26.49/4.31 | ~ mem(v0, all_57_1) | ? [v2: $i] : ? [v3: $i] : (ap(all_57_0, % 26.49/4.31 | v1) = v2 & ap(all_57_0, v0) = v3 & ap(c_2Erealax_2Ereal__neg, % 26.49/4.31 | v3) = v2 & $i(v3) & $i(v2))) % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (20) with all_26_2, all_48_0, all_26_8, all_26_3, % 26.49/4.31 | simplifying with (36) gives: % 26.49/4.31 | (114) all_48_0 = all_26_2 | ~ (ap(all_26_3, all_26_8) = all_48_0) % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (21) with all_42_1, all_44_1, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (69), (75) gives: % 26.49/4.31 | (115) all_44_1 = all_42_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (21) with all_44_1, all_54_1, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (75), (109) gives: % 26.49/4.31 | (116) all_54_1 = all_44_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (21) with all_36_1, all_54_1, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (60), (109) gives: % 26.49/4.31 | (117) all_54_1 = all_36_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (21) with all_42_1, all_57_1, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (69), (111) gives: % 26.49/4.31 | (118) all_57_1 = all_42_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (21) with all_34_1, all_57_1, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (57), (111) gives: % 26.49/4.31 | (119) all_57_1 = all_34_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (22) with all_40_2, all_48_4, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (66), (90) gives: % 26.49/4.31 | (120) all_48_4 = all_40_2 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (22) with all_26_9, all_52_4, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (38), (104) gives: % 26.49/4.31 | (121) all_52_4 = all_26_9 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (22) with all_50_5, all_52_4, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (97), (104) gives: % 26.49/4.31 | (122) all_52_4 = all_50_5 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (22) with all_48_4, all_52_4, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (90), (104) gives: % 26.49/4.31 | (123) all_52_4 = all_48_4 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (22) with all_42_3, all_52_4, all_26_11, all_26_12, % 26.49/4.31 | simplifying with (70), (104) gives: % 26.49/4.31 | (124) all_52_4 = all_42_3 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (17) with all_38_1, all_44_2, all_26_9, simplifying % 26.49/4.31 | with (62), (76) gives: % 26.49/4.31 | (125) all_44_2 = all_38_1 % 26.49/4.31 | % 26.49/4.31 | GROUND_INST: instantiating (17) with all_38_1, all_42_2, all_26_9, simplifying % 26.49/4.31 | with (62) gives: % 26.49/4.32 | (126) all_42_2 = all_38_1 | ~ (ty_2Ebool_2Eitself(all_26_9) = all_42_2) % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (23) with all_26_3, all_46_1, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (39), (82) gives: % 26.49/4.32 | (127) all_46_1 = all_26_3 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (23) with all_46_1, all_50_1, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (82), (98) gives: % 26.49/4.32 | (128) all_50_1 = all_46_1 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (23) with all_50_1, all_52_1, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (98), (105) gives: % 26.49/4.32 | (129) all_52_1 = all_50_1 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (23) with all_44_3, all_52_1, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (77), (105) gives: % 26.49/4.32 | (130) all_52_1 = all_44_3 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (24) with all_26_5, all_50_2, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (40), (99) gives: % 26.49/4.32 | (131) all_50_2 = all_26_5 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (24) with all_48_1, all_50_2, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (91), (99) gives: % 26.49/4.32 | (132) all_50_2 = all_48_1 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (24) with all_50_2, all_57_0, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (99), (112) gives: % 26.49/4.32 | (133) all_57_0 = all_50_2 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (24) with all_46_2, all_57_0, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (83), (112) gives: % 26.49/4.32 | (134) all_57_0 = all_46_2 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (18) with all_26_8, all_46_4, all_26_9, simplifying % 26.49/4.32 | with (41), (84) gives: % 26.49/4.32 | (135) all_46_4 = all_26_8 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (18) with all_26_8, all_48_3, all_26_9, simplifying % 26.49/4.32 | with (41) gives: % 26.49/4.32 | (136) all_48_3 = all_26_8 | ~ (c_2Ebool_2Ethe__value(all_26_9) = all_48_3) % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (18) with all_50_4, all_52_3, all_50_5, simplifying % 26.49/4.32 | with (100) gives: % 26.49/4.32 | (137) all_52_3 = all_50_4 | ~ (c_2Ebool_2Ethe__value(all_50_5) = all_52_3) % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (18) with all_46_4, all_52_3, all_26_9, simplifying % 26.49/4.32 | with (84) gives: % 26.49/4.32 | (138) all_52_3 = all_46_4 | ~ (c_2Ebool_2Ethe__value(all_26_9) = all_52_3) % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (25) with all_26_10, all_48_5, all_26_11, % 26.49/4.32 | all_26_12, simplifying with (42), (93) gives: % 26.49/4.32 | (139) all_48_5 = all_26_10 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (25) with all_38_2, all_48_5, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (63), (93) gives: % 26.49/4.32 | (140) all_48_5 = all_38_2 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (25) with all_48_5, all_52_5, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (93), (107) gives: % 26.49/4.32 | (141) all_52_5 = all_48_5 % 26.49/4.32 | % 26.49/4.32 | GROUND_INST: instantiating (25) with all_46_5, all_52_5, all_26_11, all_26_12, % 26.49/4.32 | simplifying with (85), (107) gives: % 26.49/4.32 | (142) all_52_5 = all_46_5 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (133), (134) imply: % 26.49/4.32 | (143) all_50_2 = all_46_2 % 26.49/4.32 | % 26.49/4.32 | SIMP: (143) implies: % 26.49/4.32 | (144) all_50_2 = all_46_2 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (118), (119) imply: % 26.49/4.32 | (145) all_42_1 = all_34_1 % 26.49/4.32 | % 26.49/4.32 | SIMP: (145) implies: % 26.49/4.32 | (146) all_42_1 = all_34_1 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (116), (117) imply: % 26.49/4.32 | (147) all_44_1 = all_36_1 % 26.49/4.32 | % 26.49/4.32 | SIMP: (147) implies: % 26.49/4.32 | (148) all_44_1 = all_36_1 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (129), (130) imply: % 26.49/4.32 | (149) all_50_1 = all_44_3 % 26.49/4.32 | % 26.49/4.32 | SIMP: (149) implies: % 26.49/4.32 | (150) all_50_1 = all_44_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (121), (122) imply: % 26.49/4.32 | (151) all_50_5 = all_26_9 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (122), (123) imply: % 26.49/4.32 | (152) all_50_5 = all_48_4 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (122), (124) imply: % 26.49/4.32 | (153) all_50_5 = all_42_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (141), (142) imply: % 26.49/4.32 | (154) all_48_5 = all_46_5 % 26.49/4.32 | % 26.49/4.32 | SIMP: (154) implies: % 26.49/4.32 | (155) all_48_5 = all_46_5 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (128), (150) imply: % 26.49/4.32 | (156) all_46_1 = all_44_3 % 26.49/4.32 | % 26.49/4.32 | SIMP: (156) implies: % 26.49/4.32 | (157) all_46_1 = all_44_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (131), (132) imply: % 26.49/4.32 | (158) all_48_1 = all_26_5 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (132), (144) imply: % 26.49/4.32 | (159) all_48_1 = all_46_2 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (151), (153) imply: % 26.49/4.32 | (160) all_42_3 = all_26_9 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (152), (153) imply: % 26.49/4.32 | (161) all_48_4 = all_42_3 % 26.49/4.32 | % 26.49/4.32 | SIMP: (161) implies: % 26.49/4.32 | (162) all_48_4 = all_42_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (158), (159) imply: % 26.49/4.32 | (163) all_46_2 = all_26_5 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (120), (162) imply: % 26.49/4.32 | (164) all_42_3 = all_40_2 % 26.49/4.32 | % 26.49/4.32 | SIMP: (164) implies: % 26.49/4.32 | (165) all_42_3 = all_40_2 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (139), (155) imply: % 26.49/4.32 | (166) all_46_5 = all_26_10 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (140), (155) imply: % 26.49/4.32 | (167) all_46_5 = all_38_2 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (127), (157) imply: % 26.49/4.32 | (168) all_44_3 = all_26_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (166), (167) imply: % 26.49/4.32 | (169) all_38_2 = all_26_10 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (115), (148) imply: % 26.49/4.32 | (170) all_42_1 = all_36_1 % 26.49/4.32 | % 26.49/4.32 | SIMP: (170) implies: % 26.49/4.32 | (171) all_42_1 = all_36_1 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (146), (171) imply: % 26.49/4.32 | (172) all_36_1 = all_34_1 % 26.49/4.32 | % 26.49/4.32 | SIMP: (172) implies: % 26.49/4.32 | (173) all_36_1 = all_34_1 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (160), (165) imply: % 26.49/4.32 | (174) all_40_2 = all_26_9 % 26.49/4.32 | % 26.49/4.32 | SIMP: (174) implies: % 26.49/4.32 | (175) all_40_2 = all_26_9 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (148), (173) imply: % 26.49/4.32 | (176) all_44_1 = all_34_1 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (120), (175) imply: % 26.49/4.32 | (177) all_48_4 = all_26_9 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (150), (168) imply: % 26.49/4.32 | (178) all_50_1 = all_26_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (142), (166) imply: % 26.49/4.32 | (179) all_52_5 = all_26_10 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (130), (168) imply: % 26.49/4.32 | (180) all_52_1 = all_26_3 % 26.49/4.32 | % 26.49/4.32 | COMBINE_EQS: (134), (163) imply: % 26.49/4.32 | (181) all_57_0 = all_26_5 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (106), (121) imply: % 26.49/4.32 | (182) c_2Ebool_2Ethe__value(all_26_9) = all_52_3 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (100), (151) imply: % 26.49/4.32 | (183) c_2Ebool_2Ethe__value(all_26_9) = all_50_4 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (92), (177) imply: % 26.49/4.32 | (184) c_2Ebool_2Ethe__value(all_26_9) = all_48_3 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (71), (160) imply: % 26.49/4.32 | (185) ty_2Ebool_2Eitself(all_26_9) = all_42_2 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (103), (180) imply: % 26.49/4.32 | (186) ap(all_26_3, all_52_3) = all_52_0 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (102), (179) imply: % 26.49/4.32 | (187) ap(all_26_10, all_52_3) = all_52_2 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (96), (178) imply: % 26.49/4.32 | (188) ap(all_26_3, all_50_4) = all_50_0 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (89), (158) imply: % 26.49/4.32 | (189) ap(all_26_5, all_48_0) = all_48_2 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (88), (139) imply: % 26.49/4.32 | (190) ap(all_26_10, all_48_3) = all_48_2 % 26.49/4.32 | % 26.49/4.32 | REDUCE: (81), (127), (135) imply: % 26.49/4.32 | (191) ap(all_26_3, all_26_8) = all_46_0 % 26.49/4.33 | % 26.49/4.33 | REDUCE: (80), (135), (166) imply: % 26.49/4.33 | (192) ap(all_26_10, all_26_8) = all_46_3 % 26.49/4.33 | % 26.49/4.33 | REDUCE: (74), (125), (176) imply: % 26.49/4.33 | (193) arr(all_38_1, all_34_1) = all_44_0 % 26.49/4.33 | % 26.49/4.33 | REDUCE: (68), (146) imply: % 26.49/4.33 | (194) arr(all_42_2, all_34_1) = all_42_0 % 26.49/4.33 | % 26.49/4.33 | REDUCE: (65), (175) imply: % 26.49/4.33 | (195) $i(all_26_9) % 26.49/4.33 | % 26.49/4.33 | REDUCE: (59), (173) imply: % 26.49/4.33 | (196) $i(all_34_1) % 26.49/4.33 | % 26.49/4.33 | REDUCE: (73), (168) imply: % 26.49/4.33 | (197) mem(all_26_3, all_44_0) % 26.49/4.33 | % 26.49/4.33 | BETA: splitting (126) gives: % 26.49/4.33 | % 26.49/4.33 | Case 1: % 26.49/4.33 | | % 26.49/4.33 | | (198) ~ (ty_2Ebool_2Eitself(all_26_9) = all_42_2) % 26.49/4.33 | | % 26.49/4.33 | | PRED_UNIFY: (185), (198) imply: % 26.49/4.33 | | (199) $false % 26.49/4.33 | | % 26.49/4.33 | | CLOSE: (199) is inconsistent. % 26.49/4.33 | | % 26.49/4.33 | Case 2: % 26.49/4.33 | | % 26.49/4.33 | | (200) all_42_2 = all_38_1 % 26.49/4.33 | | % 26.49/4.33 | | REDUCE: (194), (200) imply: % 26.49/4.33 | | (201) arr(all_38_1, all_34_1) = all_42_0 % 26.49/4.33 | | % 26.49/4.33 | | BETA: splitting (136) gives: % 26.49/4.33 | | % 26.49/4.33 | | Case 1: % 26.49/4.33 | | | % 26.49/4.33 | | | (202) ~ (c_2Ebool_2Ethe__value(all_26_9) = all_48_3) % 26.49/4.33 | | | % 26.49/4.33 | | | PRED_UNIFY: (184), (202) imply: % 26.49/4.33 | | | (203) $false % 26.49/4.33 | | | % 26.49/4.33 | | | CLOSE: (203) is inconsistent. % 26.49/4.33 | | | % 26.49/4.33 | | Case 2: % 26.49/4.33 | | | % 26.49/4.33 | | | (204) all_48_3 = all_26_8 % 26.49/4.33 | | | % 26.49/4.33 | | | REDUCE: (87), (204) imply: % 26.49/4.33 | | | (205) ap(all_26_3, all_26_8) = all_48_0 % 26.49/4.33 | | | % 26.49/4.33 | | | REDUCE: (190), (204) imply: % 26.49/4.33 | | | (206) ap(all_26_10, all_26_8) = all_48_2 % 26.49/4.33 | | | % 26.49/4.33 | | | BETA: splitting (114) gives: % 26.49/4.33 | | | % 26.49/4.33 | | | Case 1: % 26.49/4.33 | | | | % 26.49/4.33 | | | | (207) ~ (ap(all_26_3, all_26_8) = all_48_0) % 26.49/4.33 | | | | % 26.49/4.33 | | | | PRED_UNIFY: (205), (207) imply: % 26.49/4.33 | | | | (208) $false % 26.49/4.33 | | | | % 26.49/4.33 | | | | CLOSE: (208) is inconsistent. % 26.49/4.33 | | | | % 26.49/4.33 | | | Case 2: % 26.49/4.33 | | | | % 26.49/4.33 | | | | (209) all_48_0 = all_26_2 % 26.49/4.33 | | | | % 26.49/4.33 | | | | REDUCE: (189), (209) imply: % 26.49/4.33 | | | | (210) ap(all_26_5, all_26_2) = all_48_2 % 26.49/4.33 | | | | % 26.49/4.33 | | | | BETA: splitting (138) gives: % 26.49/4.33 | | | | % 26.49/4.33 | | | | Case 1: % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | (211) ~ (c_2Ebool_2Ethe__value(all_26_9) = all_52_3) % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | PRED_UNIFY: (182), (211) imply: % 26.49/4.33 | | | | | (212) $false % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | CLOSE: (212) is inconsistent. % 26.49/4.33 | | | | | % 26.49/4.33 | | | | Case 2: % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | (213) all_52_3 = all_46_4 % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | COMBINE_EQS: (135), (213) imply: % 26.49/4.33 | | | | | (214) all_52_3 = all_26_8 % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | REDUCE: (186), (214) imply: % 26.49/4.33 | | | | | (215) ap(all_26_3, all_26_8) = all_52_0 % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | REDUCE: (187), (214) imply: % 26.49/4.33 | | | | | (216) ap(all_26_10, all_26_8) = all_52_2 % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | BETA: splitting (137) gives: % 26.49/4.33 | | | | | % 26.49/4.33 | | | | | Case 1: % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | (217) ~ (c_2Ebool_2Ethe__value(all_50_5) = all_52_3) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (151), (214), (217) imply: % 26.49/4.33 | | | | | | (218) ~ (c_2Ebool_2Ethe__value(all_26_9) = all_26_8) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | PRED_UNIFY: (41), (218) imply: % 26.49/4.33 | | | | | | (219) $false % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | CLOSE: (219) is inconsistent. % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | Case 2: % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | (220) all_52_3 = all_50_4 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (214), (220) imply: % 26.49/4.33 | | | | | | (221) all_50_4 = all_26_8 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (188), (221) imply: % 26.49/4.33 | | | | | | (222) ap(all_26_3, all_26_8) = all_50_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (95), (221) imply: % 26.49/4.33 | | | | | | (223) ap(all_26_10, all_26_8) = all_50_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (19) with all_42_0, all_44_0, all_34_1, % 26.49/4.33 | | | | | | all_38_1, simplifying with (193), (201) gives: % 26.49/4.33 | | | | | | (224) all_44_0 = all_42_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_26_7, all_48_2, all_26_8, % 26.49/4.33 | | | | | | all_26_10, simplifying with (33), (206) gives: % 26.49/4.33 | | | | | | (225) all_48_2 = all_26_7 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_48_2, all_50_3, all_26_8, % 26.49/4.33 | | | | | | all_26_10, simplifying with (206), (223) gives: % 26.49/4.33 | | | | | | (226) all_50_3 = all_48_2 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_50_3, all_52_2, all_26_8, % 26.49/4.33 | | | | | | all_26_10, simplifying with (216), (223) gives: % 26.49/4.33 | | | | | | (227) all_52_2 = all_50_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_46_3, all_52_2, all_26_8, % 26.49/4.33 | | | | | | all_26_10, simplifying with (192), (216) gives: % 26.49/4.33 | | | | | | (228) all_52_2 = all_46_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_26_2, all_50_0, all_26_8, % 26.49/4.33 | | | | | | all_26_3, simplifying with (36), (222) gives: % 26.49/4.33 | | | | | | (229) all_50_0 = all_26_2 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_50_0, all_52_0, all_26_8, % 26.49/4.33 | | | | | | all_26_3, simplifying with (215), (222) gives: % 26.49/4.33 | | | | | | (230) all_52_0 = all_50_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (20) with all_46_0, all_52_0, all_26_8, % 26.49/4.33 | | | | | | all_26_3, simplifying with (191), (215) gives: % 26.49/4.33 | | | | | | (231) all_52_0 = all_46_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (230), (231) imply: % 26.49/4.33 | | | | | | (232) all_50_0 = all_46_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | SIMP: (232) implies: % 26.49/4.33 | | | | | | (233) all_50_0 = all_46_0 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (227), (228) imply: % 26.49/4.33 | | | | | | (234) all_50_3 = all_46_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | SIMP: (234) implies: % 26.49/4.33 | | | | | | (235) all_50_3 = all_46_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (229), (233) imply: % 26.49/4.33 | | | | | | (236) all_46_0 = all_26_2 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (226), (235) imply: % 26.49/4.33 | | | | | | (237) all_48_2 = all_46_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | SIMP: (237) implies: % 26.49/4.33 | | | | | | (238) all_48_2 = all_46_3 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | COMBINE_EQS: (225), (238) imply: % 26.49/4.33 | | | | | | (239) all_46_3 = all_26_7 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (210), (225) imply: % 26.49/4.33 | | | | | | (240) ap(all_26_5, all_26_2) = all_26_7 % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (79), (236) imply: % 26.49/4.33 | | | | | | (241) $i(all_26_2) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | REDUCE: (197), (224) imply: % 26.49/4.33 | | | | | | (242) mem(all_26_3, all_42_0) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (7) with all_26_9, all_26_8, simplifying % 26.49/4.33 | | | | | | with (41), (45), (195) gives: % 26.49/4.33 | | | | | | (243) ? [v0: $i] : (ty_2Ebool_2Eitself(all_26_9) = v0 & $i(v0) & % 26.49/4.33 | | | | | | mem(all_26_8, v0)) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (2) with all_26_12, all_26_11, all_34_1, % 26.49/4.33 | | | | | | simplifying with (28), (29), (30), (31), (57) gives: % 26.49/4.33 | | | | | | (244) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 26.49/4.33 | | | | | | (c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) % 26.49/4.33 | | | | | | = v0 & ty_2Ebool_2Eitself(v1) = v2 & % 26.49/4.33 | | | | | | ty_2Epair_2Eprod(all_26_12, all_26_11) = v1 & arr(v2, % 26.49/4.33 | | | | | | all_34_1) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 26.49/4.33 | | | | | | mem(v0, v3)) % 26.49/4.33 | | | | | | % 26.49/4.33 | | | | | | GROUND_INST: instantiating (6) with all_26_9, all_38_1, simplifying % 26.49/4.33 | | | | | | with (45), (62), (195) gives: % 26.49/4.33 | | | | | | (245) ? [v0: $i] : (c_2Ebool_2Ethe__value(all_26_9) = v0 & % 26.49/4.33 | | | | | | $i(v0) & mem(v0, all_38_1)) % 26.49/4.33 | | | | | | % 26.49/4.34 | | | | | | DELTA: instantiating (245) with fresh symbol all_102_0 gives: % 26.49/4.34 | | | | | | (246) c_2Ebool_2Ethe__value(all_26_9) = all_102_0 & $i(all_102_0) % 26.49/4.34 | | | | | | & mem(all_102_0, all_38_1) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | ALPHA: (246) implies: % 26.49/4.34 | | | | | | (247) $i(all_102_0) % 26.49/4.34 | | | | | | (248) c_2Ebool_2Ethe__value(all_26_9) = all_102_0 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | DELTA: instantiating (243) with fresh symbol all_104_0 gives: % 26.49/4.34 | | | | | | (249) ty_2Ebool_2Eitself(all_26_9) = all_104_0 & $i(all_104_0) & % 26.49/4.34 | | | | | | mem(all_26_8, all_104_0) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | ALPHA: (249) implies: % 26.49/4.34 | | | | | | (250) mem(all_26_8, all_104_0) % 26.49/4.34 | | | | | | (251) $i(all_104_0) % 26.49/4.34 | | | | | | (252) ty_2Ebool_2Eitself(all_26_9) = all_104_0 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | DELTA: instantiating (244) with fresh symbols all_106_0, all_106_1, % 26.49/4.34 | | | | | | all_106_2, all_106_3 gives: % 26.49/4.34 | | | | | | (253) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = % 26.49/4.34 | | | | | | all_106_3 & ty_2Ebool_2Eitself(all_106_2) = all_106_1 & % 26.49/4.34 | | | | | | ty_2Epair_2Eprod(all_26_12, all_26_11) = all_106_2 & % 26.49/4.34 | | | | | | arr(all_106_1, all_34_1) = all_106_0 & $i(all_106_0) & % 26.49/4.34 | | | | | | $i(all_106_1) & $i(all_106_2) & $i(all_106_3) & % 26.49/4.34 | | | | | | mem(all_106_3, all_106_0) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | ALPHA: (253) implies: % 26.49/4.34 | | | | | | (254) $i(all_106_3) % 26.49/4.34 | | | | | | (255) c_2Ebinary__ieee_2Efloat__plus__min(all_26_12, all_26_11) = % 26.49/4.34 | | | | | | all_106_3 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | GROUND_INST: instantiating (17) with all_38_1, all_104_0, all_26_9, % 26.49/4.34 | | | | | | simplifying with (62), (252) gives: % 26.49/4.34 | | | | | | (256) all_104_0 = all_38_1 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | GROUND_INST: instantiating (23) with all_26_3, all_106_3, all_26_11, % 26.49/4.34 | | | | | | all_26_12, simplifying with (39), (255) gives: % 26.49/4.34 | | | | | | (257) all_106_3 = all_26_3 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | GROUND_INST: instantiating (18) with all_26_8, all_102_0, all_26_9, % 26.49/4.34 | | | | | | simplifying with (41), (248) gives: % 26.49/4.34 | | | | | | (258) all_102_0 = all_26_8 % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | REDUCE: (254), (257) imply: % 26.49/4.34 | | | | | | (259) $i(all_26_3) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | REDUCE: (251), (256) imply: % 26.49/4.34 | | | | | | (260) $i(all_38_1) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | REDUCE: (247), (258) imply: % 26.49/4.34 | | | | | | (261) $i(all_26_8) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | REDUCE: (250), (256) imply: % 26.49/4.34 | | | | | | (262) mem(all_26_8, all_38_1) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | GROUND_INST: instantiating (ap_tp) with all_38_1, all_34_1, % 26.49/4.34 | | | | | | all_26_3, all_42_0, all_26_8, all_26_2, simplifying % 26.49/4.34 | | | | | | with (36), (196), (201), (242), (259), (260), (261), % 26.49/4.34 | | | | | | (262) gives: % 26.49/4.34 | | | | | | (263) mem(all_26_2, all_34_1) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | GROUND_INST: instantiating (113) with all_26_2, all_26_1, % 26.49/4.34 | | | | | | simplifying with (35), (241) gives: % 26.49/4.34 | | | | | | (264) ~ mem(all_26_2, all_57_1) | ? [v0: $i] : ? [v1: $i] : % 26.49/4.34 | | | | | | (ap(all_57_0, all_26_1) = v0 & ap(all_57_0, all_26_2) = v1 % 26.49/4.34 | | | | | | & ap(c_2Erealax_2Ereal__neg, v1) = v0 & $i(v1) & $i(v0)) % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | BETA: splitting (264) gives: % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | | Case 1: % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | (265) ~ mem(all_26_2, all_57_1) % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | REDUCE: (119), (265) imply: % 26.49/4.34 | | | | | | | (266) ~ mem(all_26_2, all_34_1) % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | PRED_UNIFY: (263), (266) imply: % 26.49/4.34 | | | | | | | (267) $false % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | CLOSE: (267) is inconsistent. % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | Case 2: % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | (268) ? [v0: $i] : ? [v1: $i] : (ap(all_57_0, all_26_1) = v0 % 26.49/4.34 | | | | | | | & ap(all_57_0, all_26_2) = v1 & % 26.49/4.34 | | | | | | | ap(c_2Erealax_2Ereal__neg, v1) = v0 & $i(v1) & $i(v0)) % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | DELTA: instantiating (268) with fresh symbols all_143_0, all_143_1 % 26.49/4.34 | | | | | | | gives: % 26.49/4.34 | | | | | | | (269) ap(all_57_0, all_26_1) = all_143_1 & ap(all_57_0, % 26.49/4.34 | | | | | | | all_26_2) = all_143_0 & ap(c_2Erealax_2Ereal__neg, % 26.49/4.34 | | | | | | | all_143_0) = all_143_1 & $i(all_143_0) & $i(all_143_1) % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | ALPHA: (269) implies: % 26.49/4.34 | | | | | | | (270) ap(c_2Erealax_2Ereal__neg, all_143_0) = all_143_1 % 26.49/4.34 | | | | | | | (271) ap(all_57_0, all_26_2) = all_143_0 % 26.49/4.34 | | | | | | | (272) ap(all_57_0, all_26_1) = all_143_1 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | REDUCE: (181), (272) imply: % 26.49/4.34 | | | | | | | (273) ap(all_26_5, all_26_1) = all_143_1 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | REDUCE: (181), (271) imply: % 26.49/4.34 | | | | | | | (274) ap(all_26_5, all_26_2) = all_143_0 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | GROUND_INST: instantiating (20) with all_26_6, all_143_1, % 26.49/4.34 | | | | | | | all_26_7, c_2Erealax_2Ereal__neg, simplifying with % 26.49/4.34 | | | | | | | (32) gives: % 26.49/4.34 | | | | | | | (275) all_143_1 = all_26_6 | ~ (ap(c_2Erealax_2Ereal__neg, % 26.49/4.34 | | | | | | | all_26_7) = all_143_1) % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | GROUND_INST: instantiating (20) with all_26_7, all_143_0, % 26.49/4.34 | | | | | | | all_26_2, all_26_5, simplifying with (240), (274) % 26.49/4.34 | | | | | | | gives: % 26.49/4.34 | | | | | | | (276) all_143_0 = all_26_7 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | GROUND_INST: instantiating (20) with all_26_0, all_143_1, % 26.49/4.34 | | | | | | | all_26_1, all_26_5, simplifying with (34), (273) % 26.49/4.34 | | | | | | | gives: % 26.49/4.34 | | | | | | | (277) all_143_1 = all_26_0 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | REDUCE: (270), (276), (277) imply: % 26.49/4.34 | | | | | | | (278) ap(c_2Erealax_2Ereal__neg, all_26_7) = all_26_0 % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | BETA: splitting (275) gives: % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | | Case 1: % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | (279) ~ (ap(c_2Erealax_2Ereal__neg, all_26_7) = all_143_1) % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | REDUCE: (277), (279) imply: % 26.49/4.34 | | | | | | | | (280) ~ (ap(c_2Erealax_2Ereal__neg, all_26_7) = all_26_0) % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | PRED_UNIFY: (278), (280) imply: % 26.49/4.34 | | | | | | | | (281) $false % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | CLOSE: (281) is inconsistent. % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | Case 2: % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | (282) all_143_1 = all_26_6 % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | COMBINE_EQS: (277), (282) imply: % 26.49/4.34 | | | | | | | | (283) all_26_0 = all_26_6 % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | REDUCE: (27), (283) imply: % 26.49/4.34 | | | | | | | | (284) $false % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | | CLOSE: (284) is inconsistent. % 26.49/4.34 | | | | | | | | % 26.49/4.34 | | | | | | | End of split % 26.49/4.34 | | | | | | | % 26.49/4.34 | | | | | | End of split % 26.49/4.34 | | | | | | % 26.49/4.34 | | | | | End of split % 26.49/4.34 | | | | | % 26.49/4.34 | | | | End of split % 26.49/4.34 | | | | % 26.49/4.34 | | | End of split % 26.49/4.34 | | | % 26.49/4.34 | | End of split % 26.49/4.34 | | % 26.49/4.34 | End of split % 26.49/4.34 | % 26.49/4.34 End of proof % 26.49/4.34 % SZS output end Proof for theBenchmark % 26.49/4.34 % 26.49/4.34 3744ms %------------------------------------------------------------------------------