%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ITP018+2 : TPTP v8.1.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%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 : 600s % DateTime : Sat Jul 16 22:36:29 EDT 2022 % Result : Theorem 4.00s 1.57s % Output : Proof 6.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ITP018+2 : TPTP v8.1.0. Bugfixed v7.5.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 2 13:15:40 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.58 ____ _ % 0.20/0.58 ___ / __ \_____(_)___ ________ __________ % 0.20/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.20/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.20/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.20/0.58 % 0.20/0.58 A Theorem Prover for First-Order Logic % 0.20/0.58 (ePrincess v.1.0) % 0.20/0.58 % 0.20/0.58 (c) Philipp Rümmer, 2009-2015 % 0.20/0.58 (c) Peter Backeman, 2014-2015 % 0.20/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.20/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.20/0.58 Bug reports to peter@backeman.se % 0.20/0.58 % 0.20/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.20/0.58 % 0.20/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.70/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.72/0.97 Prover 0: Preprocessing ... % 2.98/1.31 Prover 0: Constructing countermodel ... % 4.00/1.57 Prover 0: proved (917ms) % 4.00/1.57 % 4.00/1.57 No countermodel exists, formula is valid % 4.00/1.57 % SZS status Theorem for theBenchmark % 4.00/1.57 % 4.00/1.57 Generating proof ... found it (size 94) % 6.11/2.06 % 6.11/2.06 % SZS output start Proof for theBenchmark % 6.11/2.06 Assumed formulas after preprocessing and simplification: % 6.11/2.06 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v13 = v7) & c_2Ebinary__ieee_2Eulp(v1, v2) = v3 & c_2Ebool_2Ethe__value(v4) = v5 & c_2Ebinary__ieee_2Efloat__to__real(v1, v2) = v8 & c_2Ebinary__ieee_2Efloat__plus__min(v1, v2) = v10 & ty_2Epair_2Eprod(v1, v2) = v4 & c_2Ebinary__ieee_2Efloat__negate(v1, v2) = v9 & ap(v10, v5) = v11 & ap(v9, v11) = v12 & ap(v8, v12) = v13 & ap(v3, v5) = v6 & ap(c_2Erealax_2Ereal__neg, v6) = v7 & arr(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal) = v0 & p(c_2Ebool_2ET) & mem(c_2Ebool_2ET, bool) & mem(c_2Erealax_2Ereal__neg, v0) & ne(v2) & ne(v1) & ne(ty_2Erealax_2Ereal) & ne(ind) & ne(bool) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (c_2Ebool_2Ethe__value(v16) = v17) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v18) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v14, v15) = v19) | ~ (ty_2Epair_2Eprod(v14, v15) = v16) | ~ (ap(v19, v17) = v20) | ~ (ap(v18, v20) = v21) | ~ ne(v15) | ~ ne(v14) | ? [v22] : (c_2Ebinary__ieee_2Eulp(v14, v15) = v22 & ap(v22, v17) = v21)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v18 = v16 | ~ (c_2Emin_2E_3D(v14) = v15) | ~ (ap(v17, v18) = v19) | ~ (ap(v15, v16) = v17) | ~ p(v19) | ~ mem(v18, v14) | ~ mem(v16, v14) | ~ ne(v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (c_2Ebinary__ieee_2Eulp(v14, v15) = v16) | ~ (c_2Ebool_2Ethe__value(v17) = v18) | ~ (ty_2Epair_2Eprod(v14, v15) = v17) | ~ (ap(v16, v18) = v19) | ~ ne(v15) | ~ ne(v14) | ? [v20] : ? [v21] : ? [v22] : (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v20 & c_2Ebinary__ieee_2Efloat__plus__min(v14, v15) = v21 & ap(v21, v18) = v22 & ap(v20, v22) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (ty_2Ebool_2Eitself(v16) = v17) | ~ (ty_2Epair_2Eprod(v14, v15) = v16) | ~ (ty_2Ebinary__ieee_2Efloat(v14, v15) = v18) | ~ (arr(v17, v18) = v19) | ~ ne(v15) | ~ ne(v14) | ? [v20] : (c_2Ebinary__ieee_2Efloat__plus__min(v14, v15) = v20 & mem(v20, v19))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (ap(v16, v18) = v19) | ~ (arr(v14, v15) = v17) | ~ mem(v18, v14) | ~ mem(v16, v17) | mem(v19, v15)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = v16 | ~ (arr(v14, v15) = v17) | ~ mem(v18, v17) | ~ mem(v16, v17) | ? [v19] : ? [v20] : ? [v21] : ( ~ (v21 = v20) & ap(v18, v19) = v21 & ap(v16, v19) = v20 & mem(v19, v14))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = v15 | ~ (k(v14, v15) = v17) | ~ (ap(v17, v16) = v18) | ~ mem(v16, v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (c_2Emin_2E_3D(v14) = v15) | ~ (ap(v17, v16) = v18) | ~ (ap(v15, v16) = v17) | ~ mem(v16, v14) | ~ ne(v14) | p(v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = v15 | ~ (i(v14) = v16) | ~ (ap(v16, v15) = v17) | ~ mem(v15, v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (c_2Ebinary__ieee_2Eulp(v17, v16) = v15) | ~ (c_2Ebinary__ieee_2Eulp(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (c_2Ebinary__ieee_2Efloat__to__real(v17, v16) = v15) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v17, v16) = v15) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ty_2Epair_2Eprod(v17, v16) = v15) | ~ (ty_2Epair_2Eprod(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (c_2Ebinary__ieee_2Efloat__negate(v17, v16) = v15) | ~ (c_2Ebinary__ieee_2Efloat__negate(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ty_2Ebinary__ieee_2Efloat(v17, v16) = v15) | ~ (ty_2Ebinary__ieee_2Efloat(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (k(v17, v16) = v15) | ~ (k(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ap(v17, v16) = v15) | ~ (ap(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (arr(v17, v16) = v15) | ~ (arr(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (ty_2Ebinary__ieee_2Efloat(v14, v15) = v16) | ~ (arr(v16, v16) = v17) | ~ ne(v15) | ~ ne(v14) | ? [v18] : (c_2Ebinary__ieee_2Efloat__negate(v14, v15) = v18 & mem(v18, v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (c_2Ebool_2E_21(v16) = v15) | ~ (c_2Ebool_2E_21(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (c_2Emin_2E_3D(v16) = v15) | ~ (c_2Emin_2E_3D(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (c_2Ebool_2Ethe__value(v16) = v15) | ~ (c_2Ebool_2Ethe__value(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (ty_2Ebool_2Eitself(v16) = v15) | ~ (ty_2Ebool_2Eitself(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (i(v16) = v15) | ~ (i(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Eulp(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : ? [v19] : (ty_2Ebool_2Eitself(v17) = v18 & ty_2Epair_2Eprod(v14, v15) = v17 & arr(v18, ty_2Erealax_2Ereal) = v19 & mem(v16, v19))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (c_2Ebinary__ieee_2Efloat__negate(v14, v15) = v18 & ty_2Ebinary__ieee_2Efloat(v14, v15) = v17 & ! [v19] : ! [v20] : ! [v21] : ( ~ (ap(v18, v19) = v20) | ~ (ap(v16, v20) = v21) | ~ mem(v19, v17) | ? [v22] : (ap(v16, v19) = v22 & ap(c_2Erealax_2Ereal__neg, v22) = v21)) & ! [v19] : ! [v20] : ( ~ (ap(v16, v19) = v20) | ~ mem(v19, v17) | ? [v21] : ? [v22] : (ap(v18, v19) = v21 & ap(v16, v21) = v22 & ap(c_2Erealax_2Ereal__neg, v20) = v22)))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (ty_2Ebinary__ieee_2Efloat(v14, v15) = v17 & arr(v17, ty_2Erealax_2Ereal) = v18 & mem(v16, v18))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Efloat__plus__min(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : (ty_2Ebool_2Eitself(v17) = v18 & ty_2Epair_2Eprod(v14, v15) = v17 & ty_2Ebinary__ieee_2Efloat(v14, v15) = v19 & arr(v18, v19) = v20 & mem(v16, v20))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ty_2Epair_2Eprod(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ne(v16)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ty_2Epair_2Eprod(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : ? [v19] : (c_2Ebinary__ieee_2Eulp(v14, v15) = v17 & ty_2Ebool_2Eitself(v16) = v18 & arr(v18, ty_2Erealax_2Ereal) = v19 & mem(v17, v19))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v18 & ty_2Ebinary__ieee_2Efloat(v14, v15) = v17 & ! [v19] : ! [v20] : ! [v21] : ( ~ (ap(v18, v20) = v21) | ~ (ap(v16, v19) = v20) | ~ mem(v19, v17) | ? [v22] : (ap(v18, v19) = v22 & ap(c_2Erealax_2Ereal__neg, v22) = v21)) & ! [v19] : ! [v20] : ( ~ (ap(v18, v19) = v20) | ~ mem(v19, v17) | ? [v21] : ? [v22] : (ap(v18, v21) = v22 & ap(v16, v19) = v21 & ap(c_2Erealax_2Ereal__neg, v20) = v22)))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (ty_2Ebinary__ieee_2Efloat(v14, v15) = v17 & arr(v17, v17) = v18 & mem(v16, v18))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ty_2Ebinary__ieee_2Efloat(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ne(v16)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ty_2Ebinary__ieee_2Efloat(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v17 & c_2Ebinary__ieee_2Efloat__negate(v14, v15) = v18 & ! [v19] : ! [v20] : ! [v21] : ( ~ (ap(v18, v19) = v20) | ~ (ap(v17, v20) = v21) | ~ mem(v19, v16) | ? [v22] : (ap(v17, v19) = v22 & ap(c_2Erealax_2Ereal__neg, v22) = v21)) & ! [v19] : ! [v20] : ( ~ (ap(v17, v19) = v20) | ~ mem(v19, v16) | ? [v21] : ? [v22] : (ap(v18, v19) = v21 & ap(v17, v21) = v22 & ap(c_2Erealax_2Ereal__neg, v20) = v22)))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ty_2Ebinary__ieee_2Efloat(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ? [v17] : ? [v18] : (c_2Ebinary__ieee_2Efloat__to__real(v14, v15) = v17 & arr(v16, ty_2Erealax_2Ereal) = v18 & mem(v17, v18))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (arr(v14, v15) = v16) | ~ (arr(v14, bool) = v15) | ~ ne(v14) | ? [v17] : (c_2Emin_2E_3D(v14) = v17 & mem(v17, v16))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (arr(v14, v15) = v16) | ~ ne(v15) | ~ ne(v14) | ne(v16)) & ! [v14] : ! [v15] : (v15 = v14 | ~ p(v15) | ~ p(v14) | ~ mem(v15, bool) | ~ mem(v14, bool)) & ! [v14] : ! [v15] : (v15 = v14 | ~ mem(v15, bool) | ~ mem(v14, bool) | p(v15) | p(v14)) & ! [v14] : ! [v15] : ( ~ (c_2Ebool_2E_21(v14) = v15) | ~ ne(v14) | ? [v16] : ? [v17] : (arr(v16, bool) = v17 & arr(v14, bool) = v16 & mem(v15, v17))) & ! [v14] : ! [v15] : ( ~ (c_2Ebool_2E_21(v14) = v15) | ~ ne(v14) | ? [v16] : (arr(v14, bool) = v16 & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (ap(v17, v19) = v20) | ~ (ap(v15, v17) = v18) | ~ p(v18) | ~ mem(v19, v14) | ~ mem(v17, v16) | p(v20)) & ! [v17] : ! [v18] : ( ~ (ap(v15, v17) = v18) | ~ mem(v17, v16) | p(v18) | ? [v19] : ? [v20] : (ap(v17, v19) = v20 & mem(v19, v14) & ~ p(v20))))) & ! [v14] : ! [v15] : ( ~ (c_2Emin_2E_3D(v14) = v15) | ~ ne(v14) | ? [v16] : ? [v17] : (arr(v14, v16) = v17 & arr(v14, bool) = v16 & mem(v15, v17))) & ! [v14] : ! [v15] : ( ~ (c_2Ebool_2Ethe__value(v14) = v15) | ~ ne(v14) | ? [v16] : (ty_2Ebool_2Eitself(v14) = v16 & mem(v15, v16))) & ! [v14] : ! [v15] : ( ~ (ty_2Ebool_2Eitself(v14) = v15) | ~ ne(v14) | ne(v15)) & ! [v14] : ! [v15] : ( ~ (ty_2Ebool_2Eitself(v14) = v15) | ~ ne(v14) | ? [v16] : (c_2Ebool_2Ethe__value(v14) = v16 & mem(v16, v15))) & ! [v14] : ! [v15] : ( ~ (arr(v14, bool) = v15) | ~ ne(v14) | ? [v16] : ? [v17] : (c_2Ebool_2E_21(v14) = v16 & arr(v15, bool) = v17 & mem(v16, v17))) & ! [v14] : ! [v15] : ( ~ (arr(v14, bool) = v15) | ~ ne(v14) | ? [v16] : (c_2Ebool_2E_21(v14) = v16 & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (ap(v17, v19) = v20) | ~ (ap(v16, v17) = v18) | ~ p(v18) | ~ mem(v19, v14) | ~ mem(v17, v15) | p(v20)) & ! [v17] : ! [v18] : ( ~ (ap(v16, v17) = v18) | ~ mem(v17, v15) | p(v18) | ? [v19] : ? [v20] : (ap(v17, v19) = v20 & mem(v19, v14) & ~ p(v20)))))) % 6.65/2.11 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 6.65/2.11 | (1) ~ (all_0_0_0 = all_0_6_6) & c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_0_10_10 & c_2Ebool_2Ethe__value(all_0_9_9) = all_0_8_8 & c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5 & c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_0_3_3 & ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9 & c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_0_4_4 & ap(all_0_3_3, all_0_8_8) = all_0_2_2 & ap(all_0_4_4, all_0_2_2) = all_0_1_1 & ap(all_0_5_5, all_0_1_1) = all_0_0_0 & ap(all_0_10_10, all_0_8_8) = all_0_7_7 & ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_6_6 & arr(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal) = all_0_13_13 & p(c_2Ebool_2ET) & mem(c_2Ebool_2ET, bool) & mem(c_2Erealax_2Ereal__neg, all_0_13_13) & ne(all_0_11_11) & ne(all_0_12_12) & ne(ty_2Erealax_2Ereal) & ne(ind) & ne(bool) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (c_2Ebool_2Ethe__value(v2) = v3) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v5) | ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ (ap(v5, v3) = v6) | ~ (ap(v4, v6) = v7) | ~ ne(v1) | ~ ne(v0) | ? [v8] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v8 & ap(v8, v3) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v2 | ~ (c_2Emin_2E_3D(v0) = v1) | ~ (ap(v3, v4) = v5) | ~ (ap(v1, v2) = v3) | ~ p(v5) | ~ mem(v4, v0) | ~ mem(v2, v0) | ~ ne(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ (c_2Ebool_2Ethe__value(v3) = v4) | ~ (ty_2Epair_2Eprod(v0, v1) = v3) | ~ (ap(v2, v4) = v5) | ~ ne(v1) | ~ ne(v0) | ? [v6] : ? [v7] : ? [v8] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v6 & c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & ap(v7, v4) = v8 & ap(v6, v8) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ty_2Ebool_2Eitself(v2) = v3) | ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v4) | ~ (arr(v3, v4) = v5) | ~ ne(v1) | ~ ne(v0) | ? [v6] : (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v6 & mem(v6, v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ap(v2, v4) = v5) | ~ (arr(v0, v1) = v3) | ~ mem(v4, v0) | ~ mem(v2, v3) | mem(v5, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (arr(v0, v1) = v3) | ~ mem(v4, v3) | ~ mem(v2, v3) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & ap(v4, v5) = v7 & ap(v2, v5) = v6 & mem(v5, v0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (k(v0, v1) = v3) | ~ (ap(v3, v2) = v4) | ~ mem(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (c_2Emin_2E_3D(v0) = v1) | ~ (ap(v3, v2) = v4) | ~ (ap(v1, v2) = v3) | ~ mem(v2, v0) | ~ ne(v0) | p(v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (i(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ mem(v1, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Eulp(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Eulp(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ty_2Epair_2Eprod(v3, v2) = v1) | ~ (ty_2Epair_2Eprod(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ty_2Ebinary__ieee_2Efloat(v3, v2) = v1) | ~ (ty_2Ebinary__ieee_2Efloat(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k(v3, v2) = v1) | ~ (k(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ap(v3, v2) = v1) | ~ (ap(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ (arr(v2, v2) = v3) | ~ ne(v1) | ~ ne(v0) | ? [v4] : (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & mem(v4, v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Ebool_2E_21(v2) = v1) | ~ (c_2Ebool_2E_21(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Emin_2E_3D(v2) = v1) | ~ (c_2Emin_2E_3D(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Ebool_2Ethe__value(v2) = v1) | ~ (c_2Ebool_2Ethe__value(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ty_2Ebool_2Eitself(v2) = v1) | ~ (ty_2Ebool_2Eitself(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (i(v2) = v1) | ~ (i(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & arr(v4, ty_2Erealax_2Ereal) = v5 & mem(v2, v5))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v5) = v6) | ~ (ap(v2, v6) = v7) | ~ mem(v5, v3) | ? [v8] : (ap(v2, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v2, v5) = v6) | ~ mem(v5, v3) | ? [v7] : ? [v8] : (ap(v4, v5) = v7 & ap(v2, v7) = v8 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, ty_2Erealax_2Ereal) = v4 & mem(v2, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v5 & arr(v4, v5) = v6 & mem(v2, v6))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & ty_2Ebool_2Eitself(v2) = v4 & arr(v4, ty_2Erealax_2Ereal) = v5 & mem(v3, v5))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v6) = v7) | ~ (ap(v2, v5) = v6) | ~ mem(v5, v3) | ? [v8] : (ap(v4, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v4, v5) = v6) | ~ mem(v5, v3) | ? [v7] : ? [v8] : (ap(v4, v7) = v8 & ap(v2, v5) = v7 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, v3) = v4 & mem(v2, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v5) = v6) | ~ (ap(v3, v6) = v7) | ~ mem(v5, v2) | ? [v8] : (ap(v3, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ mem(v5, v2) | ? [v7] : ? [v8] : (ap(v4, v5) = v7 & ap(v3, v7) = v8 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & arr(v2, ty_2Erealax_2Ereal) = v4 & mem(v3, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (arr(v0, v1) = v2) | ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v3] : (c_2Emin_2E_3D(v0) = v3 & mem(v3, v2))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (arr(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ p(v1) | ~ p(v0) | ~ mem(v1, bool) | ~ mem(v0, bool)) & ! [v0] : ! [v1] : (v1 = v0 | ~ mem(v1, bool) | ~ mem(v0, bool) | p(v1) | p(v0)) & ! [v0] : ! [v1] : ( ~ (c_2Ebool_2E_21(v0) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (arr(v2, bool) = v3 & arr(v0, bool) = v2 & mem(v1, v3))) & ! [v0] : ! [v1] : ( ~ (c_2Ebool_2E_21(v0) = v1) | ~ ne(v0) | ? [v2] : (arr(v0, bool) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ (ap(v1, v3) = v4) | ~ p(v4) | ~ mem(v5, v0) | ~ mem(v3, v2) | p(v6)) & ! [v3] : ! [v4] : ( ~ (ap(v1, v3) = v4) | ~ mem(v3, v2) | p(v4) | ? [v5] : ? [v6] : (ap(v3, v5) = v6 & mem(v5, v0) & ~ p(v6))))) & ! [v0] : ! [v1] : ( ~ (c_2Emin_2E_3D(v0) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (arr(v0, v2) = v3 & arr(v0, bool) = v2 & mem(v1, v3))) & ! [v0] : ! [v1] : ( ~ (c_2Ebool_2Ethe__value(v0) = v1) | ~ ne(v0) | ? [v2] : (ty_2Ebool_2Eitself(v0) = v2 & mem(v1, v2))) & ! [v0] : ! [v1] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | ~ ne(v0) | ne(v1)) & ! [v0] : ! [v1] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | ~ ne(v0) | ? [v2] : (c_2Ebool_2Ethe__value(v0) = v2 & mem(v2, v1))) & ! [v0] : ! [v1] : ( ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (c_2Ebool_2E_21(v0) = v2 & arr(v1, bool) = v3 & mem(v2, v3))) & ! [v0] : ! [v1] : ( ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v2] : (c_2Ebool_2E_21(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ (ap(v2, v3) = v4) | ~ p(v4) | ~ mem(v5, v0) | ~ mem(v3, v1) | p(v6)) & ! [v3] : ! [v4] : ( ~ (ap(v2, v3) = v4) | ~ mem(v3, v1) | p(v4) | ? [v5] : ? [v6] : (ap(v3, v5) = v6 & mem(v5, v0) & ~ p(v6))))) % 6.72/2.14 | % 6.72/2.14 | Applying alpha-rule on (1) yields: % 6.72/2.14 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v6) = v7) | ~ (ap(v2, v5) = v6) | ~ mem(v5, v3) | ? [v8] : (ap(v4, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v4, v5) = v6) | ~ mem(v5, v3) | ? [v7] : ? [v8] : (ap(v4, v7) = v8 & ap(v2, v5) = v7 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) % 6.72/2.14 | (3) c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_0_3_3 % 6.72/2.14 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v2 | ~ (c_2Emin_2E_3D(v0) = v1) | ~ (ap(v3, v4) = v5) | ~ (ap(v1, v2) = v3) | ~ p(v5) | ~ mem(v4, v0) | ~ mem(v2, v0) | ~ ne(v0)) % 6.72/2.14 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (c_2Ebool_2Ethe__value(v2) = v3) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v4) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v5) | ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ (ap(v5, v3) = v6) | ~ (ap(v4, v6) = v7) | ~ ne(v1) | ~ ne(v0) | ? [v8] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v8 & ap(v8, v3) = v7)) % 6.72/2.14 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (arr(v0, v1) = v2) | ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v3] : (c_2Emin_2E_3D(v0) = v3 & mem(v3, v2))) % 6.72/2.14 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ty_2Ebool_2Eitself(v2) = v3) | ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v4) | ~ (arr(v3, v4) = v5) | ~ ne(v1) | ~ ne(v0) | ? [v6] : (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v6 & mem(v6, v5))) % 6.72/2.14 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v5 & arr(v4, v5) = v6 & mem(v2, v6))) % 6.72/2.15 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k(v3, v2) = v1) | ~ (k(v3, v2) = v0)) % 6.72/2.15 | (10) c_2Ebool_2Ethe__value(all_0_9_9) = all_0_8_8 % 6.72/2.15 | (11) ! [v0] : ! [v1] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | ~ ne(v0) | ne(v1)) % 6.72/2.15 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ap(v2, v4) = v5) | ~ (arr(v0, v1) = v3) | ~ mem(v4, v0) | ~ mem(v2, v3) | mem(v5, v1)) % 6.72/2.15 | (13) ap(all_0_5_5, all_0_1_1) = all_0_0_0 % 6.72/2.15 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : (ty_2Ebool_2Eitself(v3) = v4 & ty_2Epair_2Eprod(v0, v1) = v3 & arr(v4, ty_2Erealax_2Ereal) = v5 & mem(v2, v5))) % 6.72/2.15 | (15) ! [v0] : ! [v1] : ( ~ (c_2Ebool_2E_21(v0) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (arr(v2, bool) = v3 & arr(v0, bool) = v2 & mem(v1, v3))) % 6.72/2.15 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__plus__min(v3, v2) = v0)) % 6.72/2.15 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (i(v2) = v1) | ~ (i(v2) = v0)) % 6.72/2.15 | (18) ne(all_0_11_11) % 6.72/2.15 | (19) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, v3) = v4 & mem(v2, v4))) % 6.72/2.15 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__negate(v3, v2) = v0)) % 6.72/2.15 | (21) ap(all_0_3_3, all_0_8_8) = all_0_2_2 % 6.72/2.15 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ (arr(v2, v2) = v3) | ~ ne(v1) | ~ ne(v0) | ? [v4] : (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & mem(v4, v3))) % 6.72/2.15 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ty_2Epair_2Eprod(v3, v2) = v1) | ~ (ty_2Epair_2Eprod(v3, v2) = v0)) % 6.72/2.15 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ap(v3, v2) = v1) | ~ (ap(v3, v2) = v0)) % 6.72/2.15 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) % 6.72/2.15 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Emin_2E_3D(v2) = v1) | ~ (c_2Emin_2E_3D(v2) = v0)) % 6.72/2.15 | (27) ap(all_0_4_4, all_0_2_2) = all_0_1_1 % 6.72/2.15 | (28) c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_0_10_10 % 6.72/2.15 | (29) ~ (all_0_0_0 = all_0_6_6) % 6.72/2.15 | (30) ne(ind) % 6.72/2.15 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (i(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ mem(v1, v0)) % 6.72/2.15 | (32) mem(c_2Erealax_2Ereal__neg, all_0_13_13) % 6.72/2.15 | (33) ! [v0] : ! [v1] : ( ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (c_2Ebool_2E_21(v0) = v2 & arr(v1, bool) = v3 & mem(v2, v3))) % 6.72/2.15 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & arr(v2, ty_2Erealax_2Ereal) = v4 & mem(v3, v4))) % 6.72/2.15 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) % 6.72/2.16 | (36) ! [v0] : ! [v1] : ( ~ (arr(v0, bool) = v1) | ~ ne(v0) | ? [v2] : (c_2Ebool_2E_21(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ (ap(v2, v3) = v4) | ~ p(v4) | ~ mem(v5, v0) | ~ mem(v3, v1) | p(v6)) & ! [v3] : ! [v4] : ( ~ (ap(v2, v3) = v4) | ~ mem(v3, v1) | p(v4) | ? [v5] : ? [v6] : (ap(v3, v5) = v6 & mem(v5, v0) & ~ p(v6))))) % 6.72/2.16 | (37) ! [v0] : ! [v1] : (v1 = v0 | ~ mem(v1, bool) | ~ mem(v0, bool) | p(v1) | p(v0)) % 6.72/2.16 | (38) c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_0_4_4 % 6.72/2.16 | (39) ne(bool) % 6.72/2.16 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ty_2Ebinary__ieee_2Efloat(v3, v2) = v1) | ~ (ty_2Ebinary__ieee_2Efloat(v3, v2) = v0)) % 6.72/2.16 | (41) ! [v0] : ! [v1] : ! [v2] : ( ~ (arr(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ne(v2)) % 6.72/2.16 | (42) ! [v0] : ! [v1] : ( ~ (c_2Ebool_2E_21(v0) = v1) | ~ ne(v0) | ? [v2] : (arr(v0, bool) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ (ap(v1, v3) = v4) | ~ p(v4) | ~ mem(v5, v0) | ~ mem(v3, v2) | p(v6)) & ! [v3] : ! [v4] : ( ~ (ap(v1, v3) = v4) | ~ mem(v3, v2) | p(v4) | ? [v5] : ? [v6] : (ap(v3, v5) = v6 & mem(v5, v0) & ~ p(v6))))) % 6.72/2.16 | (43) ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9 % 6.72/2.16 | (44) p(c_2Ebool_2ET) % 6.72/2.16 | (45) ! [v0] : ! [v1] : (v1 = v0 | ~ p(v1) | ~ p(v0) | ~ mem(v1, bool) | ~ mem(v0, bool)) % 6.72/2.16 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (arr(v0, v1) = v3) | ~ mem(v4, v3) | ~ mem(v2, v3) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & ap(v4, v5) = v7 & ap(v2, v5) = v6 & mem(v5, v0))) % 6.72/2.16 | (47) ap(all_0_10_10, all_0_8_8) = all_0_7_7 % 6.72/2.16 | (48) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ty_2Ebool_2Eitself(v2) = v1) | ~ (ty_2Ebool_2Eitself(v2) = v0)) % 6.72/2.16 | (49) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5 % 6.72/2.16 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (k(v0, v1) = v3) | ~ (ap(v3, v2) = v4) | ~ mem(v2, v0)) % 6.72/2.16 | (51) ! [v0] : ! [v1] : ( ~ (c_2Emin_2E_3D(v0) = v1) | ~ ne(v0) | ? [v2] : ? [v3] : (arr(v0, v2) = v3 & arr(v0, bool) = v2 & mem(v1, v3))) % 6.72/2.16 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Ebool_2E_21(v2) = v1) | ~ (c_2Ebool_2E_21(v2) = v0)) % 6.72/2.16 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (c_2Emin_2E_3D(v0) = v1) | ~ (ap(v3, v2) = v4) | ~ (ap(v1, v2) = v3) | ~ mem(v2, v0) | ~ ne(v0) | p(v4)) % 6.72/2.16 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Efloat__to__real(v3, v2) = v0)) % 6.72/2.16 | (55) ne(all_0_12_12) % 6.72/2.16 | (56) mem(c_2Ebool_2ET, bool) % 6.72/2.16 | (57) ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_6_6 % 6.72/2.16 | (58) arr(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal) = all_0_13_13 % 6.72/2.16 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & arr(v3, ty_2Erealax_2Ereal) = v4 & mem(v2, v4))) % 6.72/2.17 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (c_2Ebool_2Ethe__value(v2) = v1) | ~ (c_2Ebool_2Ethe__value(v2) = v0)) % 6.72/2.17 | (61) ! [v0] : ! [v1] : ! [v2] : ( ~ (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & ty_2Ebinary__ieee_2Efloat(v0, v1) = v3 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v5) = v6) | ~ (ap(v2, v6) = v7) | ~ mem(v5, v3) | ? [v8] : (ap(v2, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v2, v5) = v6) | ~ mem(v5, v3) | ? [v7] : ? [v8] : (ap(v4, v5) = v7 & ap(v2, v7) = v8 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) % 6.72/2.17 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) % 6.72/2.17 | (63) ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Epair_2Eprod(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : ? [v5] : (c_2Ebinary__ieee_2Eulp(v0, v1) = v3 & ty_2Ebool_2Eitself(v2) = v4 & arr(v4, ty_2Erealax_2Ereal) = v5 & mem(v3, v5))) % 6.72/2.17 | (64) ne(ty_2Erealax_2Ereal) % 6.72/2.17 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (c_2Ebinary__ieee_2Eulp(v3, v2) = v1) | ~ (c_2Ebinary__ieee_2Eulp(v3, v2) = v0)) % 6.72/2.17 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ (ty_2Ebinary__ieee_2Efloat(v0, v1) = v2) | ~ ne(v1) | ~ ne(v0) | ? [v3] : ? [v4] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v3 & c_2Ebinary__ieee_2Efloat__negate(v0, v1) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (ap(v4, v5) = v6) | ~ (ap(v3, v6) = v7) | ~ mem(v5, v2) | ? [v8] : (ap(v3, v5) = v8 & ap(c_2Erealax_2Ereal__neg, v8) = v7)) & ! [v5] : ! [v6] : ( ~ (ap(v3, v5) = v6) | ~ mem(v5, v2) | ? [v7] : ? [v8] : (ap(v4, v5) = v7 & ap(v3, v7) = v8 & ap(c_2Erealax_2Ereal__neg, v6) = v8)))) % 6.72/2.17 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (c_2Ebinary__ieee_2Eulp(v0, v1) = v2) | ~ (c_2Ebool_2Ethe__value(v3) = v4) | ~ (ty_2Epair_2Eprod(v0, v1) = v3) | ~ (ap(v2, v4) = v5) | ~ ne(v1) | ~ ne(v0) | ? [v6] : ? [v7] : ? [v8] : (c_2Ebinary__ieee_2Efloat__to__real(v0, v1) = v6 & c_2Ebinary__ieee_2Efloat__plus__min(v0, v1) = v7 & ap(v7, v4) = v8 & ap(v6, v8) = v5)) % 6.72/2.17 | (68) ! [v0] : ! [v1] : ( ~ (c_2Ebool_2Ethe__value(v0) = v1) | ~ ne(v0) | ? [v2] : (ty_2Ebool_2Eitself(v0) = v2 & mem(v1, v2))) % 6.72/2.17 | (69) ! [v0] : ! [v1] : ( ~ (ty_2Ebool_2Eitself(v0) = v1) | ~ ne(v0) | ? [v2] : (c_2Ebool_2Ethe__value(v0) = v2 & mem(v2, v1))) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (67) with all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_0_10_10, c_2Ebool_2Ethe__value(all_0_9_9) = all_0_8_8, ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9, ap(all_0_10_10, all_0_8_8) = all_0_7_7, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (70) ? [v0] : ? [v1] : ? [v2] : (c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = v0 & c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = v1 & ap(v1, all_0_8_8) = v2 & ap(v0, v2) = all_0_7_7) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (14) with all_0_10_10, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_0_10_10, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (71) ? [v0] : ? [v1] : ? [v2] : (ty_2Ebool_2Eitself(v0) = v1 & ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = v0 & arr(v1, ty_2Erealax_2Ereal) = v2 & mem(all_0_10_10, v2)) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (61) with all_0_5_5, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (72) ? [v0] : ? [v1] : (c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = v1 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = v0 & ! [v2] : ! [v3] : ! [v4] : ( ~ (ap(v1, v2) = v3) | ~ (ap(all_0_5_5, v3) = v4) | ~ mem(v2, v0) | ? [v5] : (ap(all_0_5_5, v2) = v5 & ap(c_2Erealax_2Ereal__neg, v5) = v4)) & ! [v2] : ! [v3] : ( ~ (ap(all_0_5_5, v2) = v3) | ~ mem(v2, v0) | ? [v4] : ? [v5] : (ap(v1, v2) = v4 & ap(all_0_5_5, v4) = v5 & ap(c_2Erealax_2Ereal__neg, v3) = v5))) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (59) with all_0_5_5, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (73) ? [v0] : ? [v1] : (ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = v0 & arr(v0, ty_2Erealax_2Ereal) = v1 & mem(all_0_5_5, v1)) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (8) with all_0_3_3, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_0_3_3, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (74) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (ty_2Ebool_2Eitself(v0) = v1 & ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = v0 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = v2 & arr(v1, v2) = v3 & mem(all_0_3_3, v3)) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (25) with all_0_9_9, all_0_11_11, all_0_12_12 and discharging atoms ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (75) ne(all_0_9_9) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (63) with all_0_9_9, all_0_11_11, all_0_12_12 and discharging atoms ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.17 | (76) ? [v0] : ? [v1] : ? [v2] : (c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = v0 & ty_2Ebool_2Eitself(all_0_9_9) = v1 & arr(v1, ty_2Erealax_2Ereal) = v2 & mem(v0, v2)) % 6.72/2.17 | % 6.72/2.17 | Instantiating formula (2) with all_0_4_4, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_0_4_4, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.18 | (77) ? [v0] : ? [v1] : (c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = v1 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = v0 & ! [v2] : ! [v3] : ! [v4] : ( ~ (ap(v1, v3) = v4) | ~ (ap(all_0_4_4, v2) = v3) | ~ mem(v2, v0) | ? [v5] : (ap(v1, v2) = v5 & ap(c_2Erealax_2Ereal__neg, v5) = v4)) & ! [v2] : ! [v3] : ( ~ (ap(v1, v2) = v3) | ~ mem(v2, v0) | ? [v4] : ? [v5] : (ap(v1, v4) = v5 & ap(all_0_4_4, v2) = v4 & ap(c_2Erealax_2Ereal__neg, v3) = v5))) % 6.72/2.18 | % 6.72/2.18 | Instantiating formula (19) with all_0_4_4, all_0_11_11, all_0_12_12 and discharging atoms c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_0_4_4, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.18 | (78) ? [v0] : ? [v1] : (ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = v0 & arr(v0, v0) = v1 & mem(all_0_4_4, v1)) % 6.72/2.18 | % 6.72/2.18 | Instantiating (77) with all_9_0_14, all_9_1_15 yields: % 6.72/2.18 | (79) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_9_0_14 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_9_1_15 & ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_9_0_14, v1) = v2) | ~ (ap(all_0_4_4, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v3] : (ap(all_9_0_14, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) & ! [v0] : ! [v1] : ( ~ (ap(all_9_0_14, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v2] : ? [v3] : (ap(all_9_0_14, v2) = v3 & ap(all_0_4_4, v0) = v2 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (79) yields: % 6.72/2.18 | (80) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_9_0_14 % 6.72/2.18 | (81) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_9_1_15 % 6.72/2.18 | (82) ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_9_0_14, v1) = v2) | ~ (ap(all_0_4_4, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v3] : (ap(all_9_0_14, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) % 6.72/2.18 | (83) ! [v0] : ! [v1] : ( ~ (ap(all_9_0_14, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v2] : ? [v3] : (ap(all_9_0_14, v2) = v3 & ap(all_0_4_4, v0) = v2 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.18 | % 6.72/2.18 | Instantiating (78) with all_12_0_16, all_12_1_17 yields: % 6.72/2.18 | (84) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_12_1_17 & arr(all_12_1_17, all_12_1_17) = all_12_0_16 & mem(all_0_4_4, all_12_0_16) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (84) yields: % 6.72/2.18 | (85) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_12_1_17 % 6.72/2.18 | (86) arr(all_12_1_17, all_12_1_17) = all_12_0_16 % 6.72/2.18 | (87) mem(all_0_4_4, all_12_0_16) % 6.72/2.18 | % 6.72/2.18 | Instantiating (76) with all_14_0_18, all_14_1_19, all_14_2_20 yields: % 6.72/2.18 | (88) c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_14_2_20 & ty_2Ebool_2Eitself(all_0_9_9) = all_14_1_19 & arr(all_14_1_19, ty_2Erealax_2Ereal) = all_14_0_18 & mem(all_14_2_20, all_14_0_18) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (88) yields: % 6.72/2.18 | (89) c_2Ebinary__ieee_2Eulp(all_0_12_12, all_0_11_11) = all_14_2_20 % 6.72/2.18 | (90) ty_2Ebool_2Eitself(all_0_9_9) = all_14_1_19 % 6.72/2.18 | (91) arr(all_14_1_19, ty_2Erealax_2Ereal) = all_14_0_18 % 6.72/2.18 | (92) mem(all_14_2_20, all_14_0_18) % 6.72/2.18 | % 6.72/2.18 | Instantiating (74) with all_16_0_21, all_16_1_22, all_16_2_23, all_16_3_24 yields: % 6.72/2.18 | (93) ty_2Ebool_2Eitself(all_16_3_24) = all_16_2_23 & ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_16_3_24 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_16_1_22 & arr(all_16_2_23, all_16_1_22) = all_16_0_21 & mem(all_0_3_3, all_16_0_21) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (93) yields: % 6.72/2.18 | (94) arr(all_16_2_23, all_16_1_22) = all_16_0_21 % 6.72/2.18 | (95) mem(all_0_3_3, all_16_0_21) % 6.72/2.18 | (96) ty_2Ebool_2Eitself(all_16_3_24) = all_16_2_23 % 6.72/2.18 | (97) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_16_1_22 % 6.72/2.18 | (98) ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_16_3_24 % 6.72/2.18 | % 6.72/2.18 | Instantiating (73) with all_18_0_25, all_18_1_26 yields: % 6.72/2.18 | (99) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_18_1_26 & arr(all_18_1_26, ty_2Erealax_2Ereal) = all_18_0_25 & mem(all_0_5_5, all_18_0_25) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (99) yields: % 6.72/2.18 | (100) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_18_1_26 % 6.72/2.18 | (101) arr(all_18_1_26, ty_2Erealax_2Ereal) = all_18_0_25 % 6.72/2.18 | (102) mem(all_0_5_5, all_18_0_25) % 6.72/2.18 | % 6.72/2.18 | Instantiating (72) with all_20_0_27, all_20_1_28 yields: % 6.72/2.18 | (103) c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_20_0_27 & ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_20_1_28 & ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_20_0_27, v0) = v1) | ~ (ap(all_0_5_5, v1) = v2) | ~ mem(v0, all_20_1_28) | ? [v3] : (ap(all_0_5_5, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) & ! [v0] : ! [v1] : ( ~ (ap(all_0_5_5, v0) = v1) | ~ mem(v0, all_20_1_28) | ? [v2] : ? [v3] : (ap(all_20_0_27, v0) = v2 & ap(all_0_5_5, v2) = v3 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (103) yields: % 6.72/2.18 | (104) c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_20_0_27 % 6.72/2.18 | (105) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_20_1_28 % 6.72/2.18 | (106) ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_20_0_27, v0) = v1) | ~ (ap(all_0_5_5, v1) = v2) | ~ mem(v0, all_20_1_28) | ? [v3] : (ap(all_0_5_5, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) % 6.72/2.18 | (107) ! [v0] : ! [v1] : ( ~ (ap(all_0_5_5, v0) = v1) | ~ mem(v0, all_20_1_28) | ? [v2] : ? [v3] : (ap(all_20_0_27, v0) = v2 & ap(all_0_5_5, v2) = v3 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.18 | % 6.72/2.18 | Instantiating (71) with all_23_0_29, all_23_1_30, all_23_2_31 yields: % 6.72/2.18 | (108) ty_2Ebool_2Eitself(all_23_2_31) = all_23_1_30 & ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_23_2_31 & arr(all_23_1_30, ty_2Erealax_2Ereal) = all_23_0_29 & mem(all_0_10_10, all_23_0_29) % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (108) yields: % 6.72/2.18 | (109) ty_2Ebool_2Eitself(all_23_2_31) = all_23_1_30 % 6.72/2.18 | (110) ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_23_2_31 % 6.72/2.18 | (111) arr(all_23_1_30, ty_2Erealax_2Ereal) = all_23_0_29 % 6.72/2.18 | (112) mem(all_0_10_10, all_23_0_29) % 6.72/2.18 | % 6.72/2.18 | Instantiating (70) with all_25_0_32, all_25_1_33, all_25_2_34 yields: % 6.72/2.18 | (113) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_25_2_34 & c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_25_1_33 & ap(all_25_1_33, all_0_8_8) = all_25_0_32 & ap(all_25_2_34, all_25_0_32) = all_0_7_7 % 6.72/2.18 | % 6.72/2.18 | Applying alpha-rule on (113) yields: % 6.72/2.18 | (114) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_25_2_34 % 6.72/2.18 | (115) c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_25_1_33 % 6.72/2.18 | (116) ap(all_25_1_33, all_0_8_8) = all_25_0_32 % 6.72/2.18 | (117) ap(all_25_2_34, all_25_0_32) = all_0_7_7 % 6.72/2.18 | % 6.72/2.18 | Instantiating formula (54) with all_0_12_12, all_0_11_11, all_25_2_34, all_0_5_5 and discharging atoms c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_25_2_34, c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5, yields: % 6.72/2.18 | (118) all_25_2_34 = all_0_5_5 % 6.72/2.18 | % 6.72/2.18 | Instantiating formula (54) with all_0_12_12, all_0_11_11, all_9_0_14, all_25_2_34 and discharging atoms c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_25_2_34, c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_9_0_14, yields: % 6.72/2.18 | (119) all_25_2_34 = all_9_0_14 % 6.72/2.18 | % 6.72/2.18 | Instantiating formula (16) with all_0_12_12, all_0_11_11, all_25_1_33, all_0_3_3 and discharging atoms c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_25_1_33, c_2Ebinary__ieee_2Efloat__plus__min(all_0_12_12, all_0_11_11) = all_0_3_3, yields: % 6.72/2.18 | (120) all_25_1_33 = all_0_3_3 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (23) with all_0_12_12, all_0_11_11, all_23_2_31, all_0_9_9 and discharging atoms ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_23_2_31, ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_0_9_9, yields: % 6.72/2.19 | (121) all_23_2_31 = all_0_9_9 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (23) with all_0_12_12, all_0_11_11, all_16_3_24, all_23_2_31 and discharging atoms ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_23_2_31, ty_2Epair_2Eprod(all_0_12_12, all_0_11_11) = all_16_3_24, yields: % 6.72/2.19 | (122) all_23_2_31 = all_16_3_24 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (40) with all_0_12_12, all_0_11_11, all_18_1_26, all_20_1_28 and discharging atoms ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_20_1_28, ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_18_1_26, yields: % 6.72/2.19 | (123) all_20_1_28 = all_18_1_26 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (40) with all_0_12_12, all_0_11_11, all_16_1_22, all_20_1_28 and discharging atoms ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_20_1_28, ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_16_1_22, yields: % 6.72/2.19 | (124) all_20_1_28 = all_16_1_22 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (40) with all_0_12_12, all_0_11_11, all_12_1_17, all_18_1_26 and discharging atoms ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_18_1_26, ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_12_1_17, yields: % 6.72/2.19 | (125) all_18_1_26 = all_12_1_17 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (40) with all_0_12_12, all_0_11_11, all_9_1_15, all_18_1_26 and discharging atoms ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_18_1_26, ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_9_1_15, yields: % 6.72/2.19 | (126) all_18_1_26 = all_9_1_15 % 6.72/2.19 | % 6.72/2.19 | Combining equations (118,119) yields a new equation: % 6.72/2.19 | (127) all_9_0_14 = all_0_5_5 % 6.72/2.19 | % 6.72/2.19 | Combining equations (121,122) yields a new equation: % 6.72/2.19 | (128) all_16_3_24 = all_0_9_9 % 6.72/2.19 | % 6.72/2.19 | Combining equations (123,124) yields a new equation: % 6.72/2.19 | (129) all_18_1_26 = all_16_1_22 % 6.72/2.19 | % 6.72/2.19 | Simplifying 129 yields: % 6.72/2.19 | (130) all_18_1_26 = all_16_1_22 % 6.72/2.19 | % 6.72/2.19 | Combining equations (125,130) yields a new equation: % 6.72/2.19 | (131) all_16_1_22 = all_12_1_17 % 6.72/2.19 | % 6.72/2.19 | Combining equations (126,130) yields a new equation: % 6.72/2.19 | (132) all_16_1_22 = all_9_1_15 % 6.72/2.19 | % 6.72/2.19 | Combining equations (131,132) yields a new equation: % 6.72/2.19 | (133) all_12_1_17 = all_9_1_15 % 6.72/2.19 | % 6.72/2.19 | Simplifying 133 yields: % 6.72/2.19 | (134) all_12_1_17 = all_9_1_15 % 6.72/2.19 | % 6.72/2.19 | Combining equations (128,122) yields a new equation: % 6.72/2.19 | (121) all_23_2_31 = all_0_9_9 % 6.72/2.19 | % 6.72/2.19 | Combining equations (127,119) yields a new equation: % 6.72/2.19 | (118) all_25_2_34 = all_0_5_5 % 6.72/2.19 | % 6.72/2.19 | From (127) and (80) follows: % 6.72/2.19 | (49) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5 % 6.72/2.19 | % 6.72/2.19 | From (121) and (109) follows: % 6.72/2.19 | (138) ty_2Ebool_2Eitself(all_0_9_9) = all_23_1_30 % 6.72/2.19 | % 6.72/2.19 | From (128) and (96) follows: % 6.72/2.19 | (139) ty_2Ebool_2Eitself(all_0_9_9) = all_16_2_23 % 6.72/2.19 | % 6.72/2.19 | From (134) and (85) follows: % 6.72/2.19 | (81) ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_9_1_15 % 6.72/2.19 | % 6.72/2.19 | From (120) and (116) follows: % 6.72/2.19 | (141) ap(all_0_3_3, all_0_8_8) = all_25_0_32 % 6.72/2.19 | % 6.72/2.19 | From (118) and (117) follows: % 6.72/2.19 | (142) ap(all_0_5_5, all_25_0_32) = all_0_7_7 % 6.72/2.19 | % 6.72/2.19 | From (132) and (94) follows: % 6.72/2.19 | (143) arr(all_16_2_23, all_9_1_15) = all_16_0_21 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (48) with all_0_9_9, all_23_1_30, all_14_1_19 and discharging atoms ty_2Ebool_2Eitself(all_0_9_9) = all_23_1_30, ty_2Ebool_2Eitself(all_0_9_9) = all_14_1_19, yields: % 6.72/2.19 | (144) all_23_1_30 = all_14_1_19 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (48) with all_0_9_9, all_16_2_23, all_23_1_30 and discharging atoms ty_2Ebool_2Eitself(all_0_9_9) = all_23_1_30, ty_2Ebool_2Eitself(all_0_9_9) = all_16_2_23, yields: % 6.72/2.19 | (145) all_23_1_30 = all_16_2_23 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (24) with all_0_3_3, all_0_8_8, all_25_0_32, all_0_2_2 and discharging atoms ap(all_0_3_3, all_0_8_8) = all_25_0_32, ap(all_0_3_3, all_0_8_8) = all_0_2_2, yields: % 6.72/2.19 | (146) all_25_0_32 = all_0_2_2 % 6.72/2.19 | % 6.72/2.19 | Combining equations (144,145) yields a new equation: % 6.72/2.19 | (147) all_16_2_23 = all_14_1_19 % 6.72/2.19 | % 6.72/2.19 | From (147) and (139) follows: % 6.72/2.19 | (90) ty_2Ebool_2Eitself(all_0_9_9) = all_14_1_19 % 6.72/2.19 | % 6.72/2.19 | From (146) and (141) follows: % 6.72/2.19 | (21) ap(all_0_3_3, all_0_8_8) = all_0_2_2 % 6.72/2.19 | % 6.72/2.19 | From (146) and (142) follows: % 6.72/2.19 | (150) ap(all_0_5_5, all_0_2_2) = all_0_7_7 % 6.72/2.19 | % 6.72/2.19 | From (147) and (143) follows: % 6.72/2.19 | (151) arr(all_14_1_19, all_9_1_15) = all_16_0_21 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (66) with all_9_1_15, all_0_11_11, all_0_12_12 and discharging atoms ty_2Ebinary__ieee_2Efloat(all_0_12_12, all_0_11_11) = all_9_1_15, ne(all_0_11_11), ne(all_0_12_12), yields: % 6.72/2.19 | (152) ? [v0] : ? [v1] : (c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = v0 & c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = v1 & ! [v2] : ! [v3] : ! [v4] : ( ~ (ap(v1, v2) = v3) | ~ (ap(v0, v3) = v4) | ~ mem(v2, all_9_1_15) | ? [v5] : (ap(v0, v2) = v5 & ap(c_2Erealax_2Ereal__neg, v5) = v4)) & ! [v2] : ! [v3] : ( ~ (ap(v0, v2) = v3) | ~ mem(v2, all_9_1_15) | ? [v4] : ? [v5] : (ap(v1, v2) = v4 & ap(v0, v4) = v5 & ap(c_2Erealax_2Ereal__neg, v3) = v5))) % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (68) with all_0_8_8, all_0_9_9 and discharging atoms c_2Ebool_2Ethe__value(all_0_9_9) = all_0_8_8, ne(all_0_9_9), yields: % 6.72/2.19 | (153) ? [v0] : (ty_2Ebool_2Eitself(all_0_9_9) = v0 & mem(all_0_8_8, v0)) % 6.72/2.19 | % 6.72/2.19 | Instantiating (153) with all_47_0_36 yields: % 6.72/2.19 | (154) ty_2Ebool_2Eitself(all_0_9_9) = all_47_0_36 & mem(all_0_8_8, all_47_0_36) % 6.72/2.19 | % 6.72/2.19 | Applying alpha-rule on (154) yields: % 6.72/2.19 | (155) ty_2Ebool_2Eitself(all_0_9_9) = all_47_0_36 % 6.72/2.19 | (156) mem(all_0_8_8, all_47_0_36) % 6.72/2.19 | % 6.72/2.19 | Instantiating (152) with all_49_0_37, all_49_1_38 yields: % 6.72/2.19 | (157) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_49_1_38 & c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_49_0_37 & ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_49_0_37, v0) = v1) | ~ (ap(all_49_1_38, v1) = v2) | ~ mem(v0, all_9_1_15) | ? [v3] : (ap(all_49_1_38, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) & ! [v0] : ! [v1] : ( ~ (ap(all_49_1_38, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v2] : ? [v3] : (ap(all_49_0_37, v0) = v2 & ap(all_49_1_38, v2) = v3 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.19 | % 6.72/2.19 | Applying alpha-rule on (157) yields: % 6.72/2.19 | (158) c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_49_1_38 % 6.72/2.19 | (159) c_2Ebinary__ieee_2Efloat__negate(all_0_12_12, all_0_11_11) = all_49_0_37 % 6.72/2.19 | (160) ! [v0] : ! [v1] : ! [v2] : ( ~ (ap(all_49_0_37, v0) = v1) | ~ (ap(all_49_1_38, v1) = v2) | ~ mem(v0, all_9_1_15) | ? [v3] : (ap(all_49_1_38, v0) = v3 & ap(c_2Erealax_2Ereal__neg, v3) = v2)) % 6.72/2.19 | (161) ! [v0] : ! [v1] : ( ~ (ap(all_49_1_38, v0) = v1) | ~ mem(v0, all_9_1_15) | ? [v2] : ? [v3] : (ap(all_49_0_37, v0) = v2 & ap(all_49_1_38, v2) = v3 & ap(c_2Erealax_2Ereal__neg, v1) = v3)) % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (54) with all_0_12_12, all_0_11_11, all_49_1_38, all_0_5_5 and discharging atoms c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_49_1_38, c_2Ebinary__ieee_2Efloat__to__real(all_0_12_12, all_0_11_11) = all_0_5_5, yields: % 6.72/2.19 | (162) all_49_1_38 = all_0_5_5 % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (48) with all_0_9_9, all_47_0_36, all_14_1_19 and discharging atoms ty_2Ebool_2Eitself(all_0_9_9) = all_47_0_36, ty_2Ebool_2Eitself(all_0_9_9) = all_14_1_19, yields: % 6.72/2.19 | (163) all_47_0_36 = all_14_1_19 % 6.72/2.19 | % 6.72/2.19 | From (163) and (156) follows: % 6.72/2.19 | (164) mem(all_0_8_8, all_14_1_19) % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (12) with all_0_2_2, all_0_8_8, all_16_0_21, all_0_3_3, all_9_1_15, all_14_1_19 and discharging atoms ap(all_0_3_3, all_0_8_8) = all_0_2_2, arr(all_14_1_19, all_9_1_15) = all_16_0_21, mem(all_0_3_3, all_16_0_21), mem(all_0_8_8, all_14_1_19), yields: % 6.72/2.19 | (165) mem(all_0_2_2, all_9_1_15) % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (82) with all_0_0_0, all_0_1_1, all_0_2_2 and discharging atoms ap(all_0_4_4, all_0_2_2) = all_0_1_1, mem(all_0_2_2, all_9_1_15), yields: % 6.72/2.19 | (166) ~ (ap(all_9_0_14, all_0_1_1) = all_0_0_0) | ? [v0] : (ap(all_9_0_14, all_0_2_2) = v0 & ap(c_2Erealax_2Ereal__neg, v0) = all_0_0_0) % 6.72/2.19 | % 6.72/2.19 | Instantiating formula (161) with all_0_7_7, all_0_2_2 and discharging atoms mem(all_0_2_2, all_9_1_15), yields: % 6.72/2.19 | (167) ~ (ap(all_49_1_38, all_0_2_2) = all_0_7_7) | ? [v0] : ? [v1] : (ap(all_49_0_37, all_0_2_2) = v0 & ap(all_49_1_38, v0) = v1 & ap(c_2Erealax_2Ereal__neg, all_0_7_7) = v1) % 6.72/2.19 | % 6.72/2.19 +-Applying beta-rule and splitting (167), into two cases. % 6.72/2.19 |-Branch one: % 6.72/2.19 | (168) ~ (ap(all_49_1_38, all_0_2_2) = all_0_7_7) % 6.72/2.19 | % 6.72/2.19 | From (162) and (168) follows: % 6.72/2.19 | (169) ~ (ap(all_0_5_5, all_0_2_2) = all_0_7_7) % 6.72/2.20 | % 6.72/2.20 | Using (150) and (169) yields: % 6.72/2.20 | (170) $false % 6.72/2.20 | % 6.72/2.20 |-The branch is then unsatisfiable % 6.72/2.20 |-Branch two: % 6.72/2.20 | (171) ap(all_49_1_38, all_0_2_2) = all_0_7_7 % 6.72/2.20 | (172) ? [v0] : ? [v1] : (ap(all_49_0_37, all_0_2_2) = v0 & ap(all_49_1_38, v0) = v1 & ap(c_2Erealax_2Ereal__neg, all_0_7_7) = v1) % 6.72/2.20 | % 6.72/2.20 | Instantiating (172) with all_72_0_39, all_72_1_40 yields: % 6.72/2.20 | (173) ap(all_49_0_37, all_0_2_2) = all_72_1_40 & ap(all_49_1_38, all_72_1_40) = all_72_0_39 & ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_72_0_39 % 6.72/2.20 | % 6.72/2.20 | Applying alpha-rule on (173) yields: % 6.72/2.20 | (174) ap(all_49_0_37, all_0_2_2) = all_72_1_40 % 6.72/2.20 | (175) ap(all_49_1_38, all_72_1_40) = all_72_0_39 % 6.72/2.20 | (176) ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_72_0_39 % 6.72/2.20 | % 6.72/2.20 | From (162) and (171) follows: % 6.72/2.20 | (150) ap(all_0_5_5, all_0_2_2) = all_0_7_7 % 6.72/2.20 | % 6.72/2.20 +-Applying beta-rule and splitting (166), into two cases. % 6.72/2.20 |-Branch one: % 6.72/2.20 | (178) ~ (ap(all_9_0_14, all_0_1_1) = all_0_0_0) % 6.72/2.20 | % 6.72/2.20 | From (127) and (178) follows: % 6.72/2.20 | (179) ~ (ap(all_0_5_5, all_0_1_1) = all_0_0_0) % 6.72/2.20 | % 6.72/2.20 | Using (13) and (179) yields: % 6.72/2.20 | (170) $false % 6.72/2.20 | % 6.72/2.20 |-The branch is then unsatisfiable % 6.72/2.20 |-Branch two: % 6.72/2.20 | (181) ap(all_9_0_14, all_0_1_1) = all_0_0_0 % 6.72/2.20 | (182) ? [v0] : (ap(all_9_0_14, all_0_2_2) = v0 & ap(c_2Erealax_2Ereal__neg, v0) = all_0_0_0) % 6.72/2.20 | % 6.72/2.20 | Instantiating (182) with all_78_0_41 yields: % 6.72/2.20 | (183) ap(all_9_0_14, all_0_2_2) = all_78_0_41 & ap(c_2Erealax_2Ereal__neg, all_78_0_41) = all_0_0_0 % 6.72/2.20 | % 6.72/2.20 | Applying alpha-rule on (183) yields: % 6.72/2.20 | (184) ap(all_9_0_14, all_0_2_2) = all_78_0_41 % 6.72/2.20 | (185) ap(c_2Erealax_2Ereal__neg, all_78_0_41) = all_0_0_0 % 6.72/2.20 | % 6.72/2.20 | From (127) and (184) follows: % 6.72/2.20 | (186) ap(all_0_5_5, all_0_2_2) = all_78_0_41 % 6.72/2.20 | % 6.72/2.20 | Instantiating formula (24) with all_0_5_5, all_0_2_2, all_78_0_41, all_0_7_7 and discharging atoms ap(all_0_5_5, all_0_2_2) = all_78_0_41, ap(all_0_5_5, all_0_2_2) = all_0_7_7, yields: % 6.72/2.20 | (187) all_78_0_41 = all_0_7_7 % 6.72/2.20 | % 6.72/2.20 | Instantiating formula (24) with c_2Erealax_2Ereal__neg, all_0_7_7, all_72_0_39, all_0_6_6 and discharging atoms ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_72_0_39, ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_6_6, yields: % 6.72/2.20 | (188) all_72_0_39 = all_0_6_6 % 6.72/2.20 | % 6.72/2.20 | From (187) and (185) follows: % 6.72/2.20 | (189) ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_0_0 % 6.72/2.20 | % 6.72/2.20 | From (188) and (176) follows: % 6.72/2.20 | (57) ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_6_6 % 6.72/2.20 | % 6.72/2.20 | Instantiating formula (24) with c_2Erealax_2Ereal__neg, all_0_7_7, all_0_0_0, all_0_6_6 and discharging atoms ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_0_0, ap(c_2Erealax_2Ereal__neg, all_0_7_7) = all_0_6_6, yields: % 6.72/2.20 | (191) all_0_0_0 = all_0_6_6 % 6.72/2.20 | % 6.72/2.20 | Equations (191) can reduce 29 to: % 6.72/2.20 | (192) $false % 6.72/2.20 | % 6.72/2.20 |-The branch is then unsatisfiable % 6.72/2.20 % SZS output end Proof for theBenchmark % 6.72/2.20 % 6.72/2.20 1603ms %------------------------------------------------------------------------------