%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW478_1 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:30 EDT 2023 % Result : Theorem 26.60s 4.23s % Output : Proof 34.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWW478_1 : TPTP v8.1.2. Released v5.3.0. % 0.10/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 17:58:12 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.62 Amanda Stjerna. % 0.19/0.62 Free software under BSD-3-Clause. % 0.19/0.62 % 0.19/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.62 % 0.19/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.63 Running up to 7 provers in parallel. % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 7.84/1.79 Prover 1: Preprocessing ... % 7.84/1.79 Prover 4: Preprocessing ... % 7.84/1.81 Prover 6: Preprocessing ... % 7.84/1.81 Prover 5: Preprocessing ... % 7.84/1.81 Prover 0: Preprocessing ... % 7.84/1.81 Prover 3: Preprocessing ... % 7.84/1.82 Prover 2: Preprocessing ... % 22.14/3.64 Prover 1: Warning: ignoring some quantifiers % 22.61/3.76 Prover 4: Warning: ignoring some quantifiers % 23.31/3.77 Prover 3: Warning: ignoring some quantifiers % 23.31/3.82 Prover 1: Constructing countermodel ... % 23.31/3.83 Prover 3: Constructing countermodel ... % 23.83/3.86 Prover 4: Constructing countermodel ... % 24.17/3.89 Prover 6: Proving ... % 24.33/3.97 Prover 5: Proving ... % 25.05/4.01 Prover 0: Proving ... % 26.60/4.22 Prover 3: proved (3588ms) % 26.60/4.23 % 26.60/4.23 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 26.60/4.23 % 26.60/4.23 Prover 5: stopped % 26.60/4.23 Prover 6: stopped % 26.60/4.23 Prover 0: stopped % 26.60/4.23 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 26.60/4.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 26.60/4.23 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 26.60/4.24 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.17/4.81 Prover 1: Found proof (size 64) % 31.17/4.81 Prover 1: proved (4175ms) % 31.17/4.81 Prover 4: stopped % 31.17/4.82 Prover 7: Preprocessing ... % 31.17/4.82 Prover 10: Preprocessing ... % 31.17/4.84 Prover 8: Preprocessing ... % 31.17/4.85 Prover 11: Preprocessing ... % 32.28/5.00 Prover 10: stopped % 32.28/5.01 Prover 7: stopped % 32.28/5.01 Prover 11: stopped % 32.28/5.02 Prover 2: Proving ... % 32.28/5.02 Prover 2: stopped % 33.68/5.24 Prover 8: Warning: ignoring some quantifiers % 33.87/5.29 Prover 8: Constructing countermodel ... % 33.87/5.30 Prover 8: stopped % 33.87/5.30 % 33.87/5.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.87/5.30 % 33.87/5.32 % SZS output start Proof for theBenchmark % 34.25/5.34 Assumptions after simplification: % 34.25/5.34 --------------------------------- % 34.25/5.34 % 34.25/5.34 (conj_0) % 34.43/5.40 fun_Pr1391347915on_val(produc1441475159on_val) & % 34.43/5.40 fun_fu1639641777on_val(produc899768717on_val) & fun_na939144002on_val(ha) & % 34.43/5.40 fun_na939144002on_val(h_a) & fun_li1432931796on_val(la) & % 34.43/5.40 fun_li1432931796on_val(l_a) & fun_ex977868519on_val(produc1259058957on_val) & % 34.43/5.40 val(v) & list_P1999446415t_char(p) & list_char(v_1) & exp_list_char(ea) & % 34.43/5.40 exp_list_char(e_a) & ? [v0: fun_Pr231134077on_val] : ? [v1: % 34.43/5.40 fun_fu1690035458on_val] : ? [v2: option_val] : ? [v3: % 34.43/5.40 fun_li1432931796on_val] : ? [v4: produc12694297on_val] : ? [v5: % 34.43/5.40 produc124828825on_val] : ? [v6: fun_Pr714818201on_val] : ? [v7: % 34.43/5.40 fun_Pr231134077on_val] : ? [v8: fun_fu1690035458on_val] : ? [v9: % 34.43/5.40 produc12694297on_val] : ? [v10: produc124828825on_val] : ? [v11: % 34.43/5.40 produc1102272487on_val] : ? [v12: fun_Pr691271849l_bool] : ? [v13: bool] : % 34.43/5.40 ? [v14: int] : ( ~ (v14 = 0) & fun_up1149430426on_val(la, v_1, v2) = v3 & % 34.43/5.40 hAPP_P1870962205on_val(produc1441475159on_val, v5) = v6 & % 34.43/5.40 hAPP_e1659493427on_val(produc1259058957on_val, ea) = v0 & % 34.43/5.40 hAPP_e1659493427on_val(produc1259058957on_val, e_a) = v7 & % 34.43/5.40 hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.43/5.40 hAPP_f1849790461on_val(produc899768717on_val, h_a) = v8 & % 34.43/5.40 hAPP_f1727192346on_val(v8, l_a) = v9 & hAPP_f1727192346on_val(v1, v3) = v4 & % 34.43/5.40 hAPP_P604205461on_val(v7, v9) = v10 & hAPP_P604205461on_val(v0, v4) = v5 & % 34.43/5.40 hAPP_P1886180715on_val(v6, v10) = v11 & red(p) = v12 & % 34.43/5.40 member773094996on_val(v11, v12) = v13 & hBOOL(v13) = v14 & some_val(v) = v2 % 34.43/5.40 & produc1102272487on_val(v11) & produc12694297on_val(v9) & % 34.43/5.40 produc12694297on_val(v4) & produc124828825on_val(v10) & % 34.43/5.40 produc124828825on_val(v5) & fun_Pr691271849l_bool(v12) & % 34.43/5.40 fun_Pr231134077on_val(v7) & fun_Pr231134077on_val(v0) & % 34.43/5.40 fun_Pr714818201on_val(v6) & fun_fu1690035458on_val(v8) & % 34.43/5.40 fun_fu1690035458on_val(v1) & fun_li1432931796on_val(v3) & option_val(v2) & % 34.43/5.40 bool(v13)) % 34.43/5.40 % 34.43/5.40 (fact_11_InitBlockRed_I2_J) % 34.43/5.40 fun_fu1639641777on_val(produc899768717on_val) & fun_na939144002on_val(ha) & % 34.43/5.40 fun_na939144002on_val(h_a) & fun_li1432931796on_val(la) & val(v) & % 34.43/5.40 list_P1999446415t_char(p) & list_char(v_1) & exp_list_char(ea) & % 34.43/5.40 exp_list_char(e_a) & ? [v0: fun_fu1690035458on_val] : ? [v1: option_val] : % 34.43/5.40 ? [v2: fun_li1432931796on_val] : ? [v3: produc12694297on_val] : % 34.43/5.40 (fun_up1149430426on_val(la, v_1, v1) = v2 & % 34.43/5.40 hAPP_f1849790461on_val(produc899768717on_val, ha) = v0 & % 34.43/5.40 hAPP_f1727192346on_val(v0, v2) = v3 & some_val(v) = v1 & % 34.43/5.40 produc12694297on_val(v3) & fun_fu1690035458on_val(v0) & % 34.43/5.40 fun_li1432931796on_val(v2) & option_val(v1) & ! [v4: ty] : ! [v5: % 34.43/5.40 fun_li688206603ion_ty] : ! [v6: bool] : ( ~ (wTrt(p, ha, v5, ea, v4) = % 34.43/5.40 v6) | ~ fun_li688206603ion_ty(v5) | ~ ty(v4) | ? [v7: % 34.43/5.40 fun_Pr1696029455l_bool] : ? [v8: bool] : ? [v9: any] : ? [v10: any] : % 34.43/5.40 (typeSa1844245082_sconf(p, v5) = v7 & hAPP_P159683425l_bool(v7, v3) = v8 & % 34.43/5.40 hBOOL(v8) = v9 & hBOOL(v6) = v10 & fun_Pr1696029455l_bool(v7) & bool(v8) % 34.43/5.40 & ( ~ (v10 = 0) | ~ (v9 = 0))) | ? [v7: ty] : ? [v8: bool] : ? [v9: % 34.43/5.40 bool] : (wTrt(p, h_a, v5, e_a, v7) = v8 & widen_2090681816t_char(p, v7, % 34.43/5.40 v4) = v9 & hBOOL(v9) = 0 & hBOOL(v8) = 0 & ty(v7) & bool(v9) & % 34.43/5.40 bool(v8)))) % 34.43/5.40 % 34.43/5.40 (fact_14_InitBlockRed_I4_J) % 34.43/5.41 fun_fu1639641777on_val(produc899768717on_val) & fun_na939144002on_val(ha) & % 34.43/5.41 fun_li1432931796on_val(la) & fun_li688206603ion_ty(e) & % 34.43/5.41 list_P1999446415t_char(p) & ? [v0: fun_Pr1696029455l_bool] : ? [v1: % 34.43/5.41 fun_fu1690035458on_val] : ? [v2: produc12694297on_val] : ? [v3: bool] : % 34.43/5.41 (typeSa1844245082_sconf(p, e) = v0 & hAPP_P159683425l_bool(v0, v2) = v3 & % 34.43/5.41 hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.43/5.41 hAPP_f1727192346on_val(v1, la) = v2 & hBOOL(v3) = 0 & % 34.43/5.41 produc12694297on_val(v2) & fun_Pr1696029455l_bool(v0) & % 34.43/5.41 fun_fu1690035458on_val(v1) & bool(v3)) % 34.43/5.41 % 34.43/5.41 (fact_1_InitBlockRed_I1_J) % 34.43/5.41 fun_Pr1391347915on_val(produc1441475159on_val) & % 34.43/5.41 fun_fu1639641777on_val(produc899768717on_val) & fun_na939144002on_val(ha) & % 34.43/5.41 fun_na939144002on_val(h_a) & fun_li1432931796on_val(la) & % 34.43/5.41 fun_li1432931796on_val(l_a) & fun_ex977868519on_val(produc1259058957on_val) & % 34.43/5.41 val(v) & list_P1999446415t_char(p) & list_char(v_1) & exp_list_char(ea) & % 34.43/5.41 exp_list_char(e_a) & ? [v0: fun_Pr231134077on_val] : ? [v1: % 34.43/5.41 fun_fu1690035458on_val] : ? [v2: option_val] : ? [v3: % 34.43/5.41 fun_li1432931796on_val] : ? [v4: produc12694297on_val] : ? [v5: % 34.43/5.41 produc124828825on_val] : ? [v6: fun_Pr714818201on_val] : ? [v7: % 34.43/5.41 fun_Pr231134077on_val] : ? [v8: fun_fu1690035458on_val] : ? [v9: % 34.43/5.41 produc12694297on_val] : ? [v10: produc124828825on_val] : ? [v11: % 34.43/5.41 produc1102272487on_val] : ? [v12: fun_Pr691271849l_bool] : ? [v13: bool] : % 34.43/5.41 (fun_up1149430426on_val(la, v_1, v2) = v3 & % 34.43/5.41 hAPP_P1870962205on_val(produc1441475159on_val, v5) = v6 & % 34.43/5.41 hAPP_e1659493427on_val(produc1259058957on_val, ea) = v0 & % 34.43/5.41 hAPP_e1659493427on_val(produc1259058957on_val, e_a) = v7 & % 34.43/5.41 hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.43/5.41 hAPP_f1849790461on_val(produc899768717on_val, h_a) = v8 & % 34.43/5.41 hAPP_f1727192346on_val(v8, l_a) = v9 & hAPP_f1727192346on_val(v1, v3) = v4 & % 34.43/5.41 hAPP_P604205461on_val(v7, v9) = v10 & hAPP_P604205461on_val(v0, v4) = v5 & % 34.43/5.41 hAPP_P1886180715on_val(v6, v10) = v11 & red(p) = v12 & % 34.43/5.41 member773094996on_val(v11, v12) = v13 & hBOOL(v13) = 0 & some_val(v) = v2 & % 34.43/5.41 produc1102272487on_val(v11) & produc12694297on_val(v9) & % 34.43/5.41 produc12694297on_val(v4) & produc124828825on_val(v10) & % 34.43/5.41 produc124828825on_val(v5) & fun_Pr691271849l_bool(v12) & % 34.43/5.41 fun_Pr231134077on_val(v7) & fun_Pr231134077on_val(v0) & % 34.43/5.41 fun_Pr714818201on_val(v6) & fun_fu1690035458on_val(v8) & % 34.43/5.41 fun_fu1690035458on_val(v1) & fun_li1432931796on_val(v3) & option_val(v2) & % 34.43/5.41 bool(v13)) % 34.43/5.41 % 34.43/5.41 (function-axioms) % 34.70/5.45 ! [v0: bool] : ! [v1: bool] : ! [v2: ty] : ! [v3: exp_list_char] : ! [v4: % 34.70/5.45 fun_li688206603ion_ty] : ! [v5: fun_na939144002on_val] : ! [v6: % 34.70/5.45 list_P1999446415t_char] : (v1 = v0 | ~ (wTrt(v6, v5, v4, v3, v2) = v1) | ~ % 34.70/5.45 (wTrt(v6, v5, v4, v3, v2) = v0)) & ! [v0: fun_ex1201926843l_bool] : ! [v1: % 34.70/5.45 fun_ex1201926843l_bool] : ! [v2: produc12694297on_val] : ! [v3: % 34.70/5.45 exp_list_char] : ! [v4: list_P1999446415t_char] : (v1 = v0 | ~ (redp(v4, % 34.70/5.45 v3, v2) = v1) | ~ (redp(v4, v3, v2) = v0)) & ! [v0: exp_list_char] : % 34.70/5.45 ! [v1: exp_list_char] : ! [v2: exp_list_char] : ! [v3: ty] : ! [v4: % 34.70/5.45 list_char] : (v1 = v0 | ~ (block_list_char(v4, v3, v2) = v1) | ~ % 34.70/5.45 (block_list_char(v4, v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! % 34.70/5.45 [v2: ty] : ! [v3: ty] : ! [v4: list_P1999446415t_char] : (v1 = v0 | ~ % 34.70/5.45 (widen_2090681816t_char(v4, v3, v2) = v1) | ~ (widen_2090681816t_char(v4, % 34.70/5.45 v3, v2) = v0)) & ! [v0: fun_li688206603ion_ty] : ! [v1: % 34.70/5.45 fun_li688206603ion_ty] : ! [v2: option_ty] : ! [v3: list_char] : ! [v4: % 34.70/5.45 fun_li688206603ion_ty] : (v1 = v0 | ~ (fun_up424764369ion_ty(v4, v3, v2) = % 34.70/5.45 v1) | ~ (fun_up424764369ion_ty(v4, v3, v2) = v0)) & ! [v0: % 34.70/5.45 fun_li1432931796on_val] : ! [v1: fun_li1432931796on_val] : ! [v2: % 34.70/5.45 option_val] : ! [v3: list_char] : ! [v4: fun_li1432931796on_val] : (v1 = % 34.70/5.45 v0 | ~ (fun_up1149430426on_val(v4, v3, v2) = v1) | ~ % 34.70/5.45 (fun_up1149430426on_val(v4, v3, v2) = v0)) & ! [v0: fun_Pr2087158653on_val] % 34.70/5.45 : ! [v1: fun_Pr2087158653on_val] : ! [v2: produc124828825on_val] : ! [v3: % 34.70/5.45 fun_Pr1719283041on_val] : (v1 = v0 | ~ (hAPP_P2083594489on_val(v3, v2) = % 34.70/5.45 v1) | ~ (hAPP_P2083594489on_val(v3, v2) = v0)) & ! [v0: % 34.70/5.45 fun_fu1622757844on_val] : ! [v1: fun_fu1622757844on_val] : ! [v2: % 34.70/5.45 fun_na939144002on_val] : ! [v3: fun_fu1133203323on_val] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_f600512025on_val(v3, v2) = v1) | ~ (hAPP_f600512025on_val(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.70/5.45 ! [v2: fun_Pr714818201on_val] : ! [v3: fun_fu1587641869l_bool] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f204771371l_bool(v3, v2) = v1) | ~ (hAPP_f204771371l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_Pr1833267965on_val] : ! [v1: fun_Pr1833267965on_val] : % 34.70/5.45 ! [v2: exp_list_char] : ! [v3: fun_ex1005552999on_val] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_e108155315on_val(v3, v2) = v1) | ~ (hAPP_e108155315on_val(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_fu1693644106l_bool] : ! [v1: fun_fu1693644106l_bool] : % 34.70/5.45 ! [v2: fun_fu1622757844on_val] : ! [v3: fun_fu964448643l_bool] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f524589473l_bool(v3, v2) = v1) | ~ (hAPP_f524589473l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: produc1102272487on_val] : ! [v1: produc1102272487on_val] : % 34.70/5.45 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu1622757844on_val] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f602593190on_val(v3, v2) = v1) | ~ (hAPP_f602593190on_val(v3, v2) % 34.70/5.45 = v0)) & ! [v0: fun_fu277794946on_val] : ! [v1: fun_fu277794946on_val] : % 34.70/5.45 ! [v2: fun_na939144002on_val] : ! [v3: fun_fu2073188913on_val] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f1840640125on_val(v3, v2) = v1) | ~ (hAPP_f1840640125on_val(v3, v2) % 34.70/5.45 = v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.70/5.45 ! [v2: fun_Pr2087158653on_val] : ! [v3: fun_fu2085256997l_bool] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f1712766199l_bool(v3, v2) = v1) | ~ (hAPP_f1712766199l_bool(v3, % 34.70/5.45 v2) = v0)) & ! [v0: fun_Pr1696029455l_bool] : ! [v1: % 34.70/5.45 fun_Pr1696029455l_bool] : ! [v2: fun_Pr231134077on_val] : ! [v3: % 34.70/5.45 fun_fu1929378469l_bool] : (v1 = v0 | ~ (hAPP_f489055607l_bool(v3, v2) = v1) % 34.70/5.45 | ~ (hAPP_f489055607l_bool(v3, v2) = v0)) & ! [v0: fun_Pr1696029455l_bool] % 34.70/5.45 : ! [v1: fun_Pr1696029455l_bool] : ! [v2: fun_Pr1833267965on_val] : ! [v3: % 34.70/5.45 fun_fu225006629l_bool] : (v1 = v0 | ~ (hAPP_f1301559543l_bool(v3, v2) = v1) % 34.70/5.45 | ~ (hAPP_f1301559543l_bool(v3, v2) = v0)) & ! [v0: produc12694297on_val] % 34.70/5.45 : ! [v1: produc12694297on_val] : ! [v2: produc12694297on_val] : ! [v3: % 34.70/5.45 fun_Pr1833267965on_val] : (v1 = v0 | ~ (hAPP_P1776198677on_val(v3, v2) = % 34.70/5.45 v1) | ~ (hAPP_P1776198677on_val(v3, v2) = v0)) & ! [v0: % 34.70/5.45 fun_fu1693644106l_bool] : ! [v1: fun_fu1693644106l_bool] : ! [v2: % 34.70/5.45 fun_fu277794946on_val] : ! [v3: fun_fu1640122725l_bool] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_f318082871l_bool(v3, v2) = v1) | ~ (hAPP_f318082871l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: produc124828825on_val] : ! [v1: produc124828825on_val] : % 34.70/5.45 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu277794946on_val] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f1926378906on_val(v3, v2) = v1) | ~ (hAPP_f1926378906on_val(v3, v2) % 34.70/5.45 = v0)) & ! [v0: fun_fu1590192889l_bool] : ! [v1: fun_fu1590192889l_bool] % 34.70/5.45 : ! [v2: fun_na939144002on_val] : ! [v3: fun_fu1806184744l_bool] : (v1 = v0 % 34.70/5.45 | ~ (hAPP_f1492320500l_bool(v3, v2) = v1) | ~ (hAPP_f1492320500l_bool(v3, % 34.70/5.45 v2) = v0)) & ! [v0: fun_fu1693644106l_bool] : ! [v1: % 34.70/5.45 fun_fu1693644106l_bool] : ! [v2: fun_fu1690035458on_val] : ! [v3: % 34.70/5.45 fun_fu1176066021l_bool] : (v1 = v0 | ~ (hAPP_f1008932791l_bool(v3, v2) = % 34.70/5.45 v1) | ~ (hAPP_f1008932791l_bool(v3, v2) = v0)) & ! [v0: % 34.70/5.45 fun_fu2075294830l_bool] : ! [v1: fun_fu2075294830l_bool] : ! [v2: % 34.70/5.45 fun_na939144002on_val] : ! [v3: fun_fu570492181l_bool] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_f1617787571l_bool(v3, v2) = v1) | ~ (hAPP_f1617787571l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.70/5.45 ! [v2: fun_Pr680585871l_bool] : ! [v3: fun_fu983865091l_bool] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_f926562337l_bool(v3, v2) = v1) | ~ (hAPP_f926562337l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : % 34.70/5.45 ! [v2: fun_Pr1696029455l_bool] : ! [v3: fun_fu1319073539l_bool] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f2134824737l_bool(v3, v2) = v1) | ~ (hAPP_f2134824737l_bool(v3, % 34.70/5.45 v2) = v0)) & ! [v0: fun_bool_bool] : ! [v1: fun_bool_bool] : ! [v2: % 34.70/5.45 fun_na939144002on_val] : ! [v3: fun_fu250820942l_bool] : (v1 = v0 | ~ % 34.70/5.45 (hAPP_f1145256474l_bool(v3, v2) = v1) | ~ (hAPP_f1145256474l_bool(v3, v2) = % 34.70/5.45 v0)) & ! [v0: fun_fu2075294830l_bool] : ! [v1: fun_fu2075294830l_bool] : % 34.70/5.45 ! [v2: fun_fu1670877422y_bool] : ! [v3: fun_fu2083094209l_bool] : (v1 = v0 | % 34.70/5.45 ~ (hAPP_f181262431l_bool(v3, v2) = v1) | ~ (hAPP_f181262431l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_fu1693644106l_bool] : ! [v1: fun_fu1693644106l_bool] % 34.77/5.45 : ! [v2: fun_li688206603ion_ty] : ! [v3: fun_fu2075294830l_bool] : (v1 = v0 % 34.77/5.45 | ~ (hAPP_f603925568l_bool(v3, v2) = v1) | ~ (hAPP_f603925568l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_fu1693644106l_bool] : ! [v1: % 34.77/5.45 fun_fu1693644106l_bool] : ! [v2: fun_fu1693644106l_bool] : ! [v3: % 34.77/5.45 fun_fu1590192889l_bool] : (v1 = v0 | ~ (hAPP_f1074020887l_bool(v3, v2) = % 34.77/5.45 v1) | ~ (hAPP_f1074020887l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 34.77/5.45 bool] : ! [v2: exp_list_char] : ! [v3: list_char] : (v1 = v0 | ~ % 34.77/5.45 (assigned(v3, v2) = v1) | ~ (assigned(v3, v2) = v0)) & ! [v0: bool] : ! % 34.77/5.45 [v1: bool] : ! [v2: bool] : ! [v3: fun_bool_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_bool_bool(v3, v2) = v1) | ~ (hAPP_bool_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_Pr1793564609l_bool] : ! [v1: fun_Pr1793564609l_bool] : ! [v2: % 34.77/5.45 fun_fu606696995l_bool] : ! [v3: fun_fu1343174525l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f833559503l_bool(v3, v2) = v1) | ~ (hAPP_f833559503l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1677251708l_bool] : ! [v1: fun_fu1677251708l_bool] : % 34.77/5.45 ! [v2: fun_na939144002on_val] : ! [v3: fun_fu606696995l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f2144092865l_bool(v3, v2) = v1) | ~ (hAPP_f2144092865l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.77/5.45 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu1677251708l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f2011777102l_bool(v3, v2) = v1) | ~ (hAPP_f2011777102l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_Pr598845249l_bool] : ! [v1: % 34.77/5.45 fun_Pr598845249l_bool] : ! [v2: fun_fu110544035l_bool] : ! [v3: % 34.77/5.45 fun_fu1871906941l_bool] : (v1 = v0 | ~ (hAPP_f1276548047l_bool(v3, v2) = % 34.77/5.45 v1) | ~ (hAPP_f1276548047l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu905586428l_bool] : ! [v1: fun_fu905586428l_bool] : ! [v2: % 34.77/5.45 fun_na939144002on_val] : ! [v3: fun_fu110544035l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f2135509569l_bool(v3, v2) = v1) | ~ (hAPP_f2135509569l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : % 34.77/5.45 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu905586428l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f396019662l_bool(v3, v2) = v1) | ~ (hAPP_f396019662l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr633696065l_bool] : ! [v1: fun_Pr633696065l_bool] : % 34.77/5.45 ! [v2: fun_ex1732109805l_bool] : ! [v3: fun_fu1162814663l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1760682521l_bool(v3, v2) = v1) | ~ (hAPP_f1760682521l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_Pr1793564609l_bool] : ! [v1: fun_Pr1793564609l_bool] % 34.77/5.45 : ! [v2: exp_list_char] : ! [v3: fun_ex1732109805l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_e592495499l_bool(v3, v2) = v1) | ~ (hAPP_e592495499l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.77/5.45 ! [v2: produc12694297on_val] : ! [v3: fun_Pr1793564609l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P1638898323l_bool(v3, v2) = v1) | ~ (hAPP_P1638898323l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr134674113l_bool] : ! [v1: fun_Pr134674113l_bool] : % 34.77/5.45 ! [v2: fun_ex1123147373l_bool] : ! [v3: fun_fu1913539015l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f468299289l_bool(v3, v2) = v1) | ~ (hAPP_f468299289l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr598845249l_bool] : ! [v1: fun_Pr598845249l_bool] : % 34.77/5.45 ! [v2: exp_list_char] : ! [v3: fun_ex1123147373l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_e500528395l_bool(v3, v2) = v1) | ~ (hAPP_e500528395l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : % 34.77/5.45 ! [v2: produc12694297on_val] : ! [v3: fun_Pr598845249l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P1988153107l_bool(v3, v2) = v1) | ~ (hAPP_P1988153107l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr650805339l_bool] : ! [v1: fun_Pr650805339l_bool] : % 34.77/5.45 ! [v2: fun_Pr741412723l_bool] : ! [v3: fun_fu1562135449l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1591648613l_bool(v3, v2) = v1) | ~ (hAPP_f1591648613l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.77/5.45 ! [v2: produc1102272487on_val] : ! [v3: fun_Pr650805339l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_P678729081l_bool(v3, v2) = v1) | ~ (hAPP_P678729081l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr633696065l_bool] : ! [v1: fun_Pr633696065l_bool] : % 34.77/5.45 ! [v2: produc124828825on_val] : ! [v3: fun_Pr741412723l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P1953518277l_bool(v3, v2) = v1) | ~ (hAPP_P1953518277l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr1404764635l_bool] : ! [v1: fun_Pr1404764635l_bool] : % 34.77/5.45 ! [v2: fun_Pr293514739l_bool] : ! [v3: fun_fu2138074009l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f444383845l_bool(v3, v2) = v1) | ~ (hAPP_f444383845l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : % 34.77/5.45 ! [v2: produc1102272487on_val] : ! [v3: fun_Pr1404764635l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_P1826803705l_bool(v3, v2) = v1) | ~ (hAPP_P1826803705l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_Pr134674113l_bool] : ! [v1: % 34.77/5.45 fun_Pr134674113l_bool] : ! [v2: produc124828825on_val] : ! [v3: % 34.77/5.45 fun_Pr293514739l_bool] : (v1 = v0 | ~ (hAPP_P1134042693l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_P1134042693l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : ! [v2: % 34.77/5.45 produc124828825on_val] : ! [v3: fun_Pr134674113l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P595502227l_bool(v3, v2) = v1) | ~ (hAPP_P595502227l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1929378469l_bool] : ! [v1: fun_fu1929378469l_bool] : % 34.77/5.45 ! [v2: fun_Pr680585871l_bool] : ! [v3: fun_fu1002878233l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f10074679l_bool(v3, v2) = v1) | ~ (hAPP_f10074679l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1241242885l_bool] : ! [v1: fun_fu1241242885l_bool] : % 34.77/5.45 ! [v2: fun_fu1929378469l_bool] : ! [v3: fun_fu610694927l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1725502637l_bool(v3, v2) = v1) | ~ (hAPP_f1725502637l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_ex1201926843l_bool] : ! [v1: fun_ex1201926843l_bool] % 34.77/5.45 : ! [v2: fun_ex977868519on_val] : ! [v3: fun_fu1241242885l_bool] : (v1 = v0 % 34.77/5.45 | ~ (hAPP_f439412817l_bool(v3, v2) = v1) | ~ (hAPP_f439412817l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_fu1587641869l_bool] : ! [v1: % 34.77/5.45 fun_fu1587641869l_bool] : ! [v2: fun_Pr691271849l_bool] : ! [v3: % 34.77/5.45 fun_fu1003774433l_bool] : (v1 = v0 | ~ (hAPP_f365540729l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f365540729l_bool(v3, v2) = v0)) & ! [v0: fun_fu151382129l_bool] % 34.77/5.45 : ! [v1: fun_fu151382129l_bool] : ! [v2: fun_fu1587641869l_bool] : ! [v3: % 34.77/5.45 fun_fu470662369l_bool] : (v1 = v0 | ~ (hAPP_f639265145l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f639265145l_bool(v3, v2) = v0)) & ! [v0: fun_Pr633696065l_bool] % 34.77/5.45 : ! [v1: fun_Pr633696065l_bool] : ! [v2: fun_Pr1391347915on_val] : ! [v3: % 34.77/5.45 fun_fu151382129l_bool] : (v1 = v0 | ~ (hAPP_f1342895119l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f1342895119l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu1176066021l_bool] : ! [v1: fun_fu1176066021l_bool] : ! [v2: % 34.77/5.45 fun_Pr1696029455l_bool] : ! [v3: fun_fu121169625l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f2057883639l_bool(v3, v2) = v1) | ~ (hAPP_f2057883639l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1722968561l_bool] : ! [v1: fun_fu1722968561l_bool] : % 34.77/5.45 ! [v2: fun_fu1176066021l_bool] : ! [v3: fun_fu698854459l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1050935001l_bool(v3, v2) = v1) | ~ (hAPP_f1050935001l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_fu100249073l_bool] : ! [v1: fun_fu100249073l_bool] : % 34.77/5.45 ! [v2: fun_fu1639641777on_val] : ! [v3: fun_fu1722968561l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1363667773l_bool(v3, v2) = v1) | ~ (hAPP_f1363667773l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_fu1590192889l_bool] : ! [v1: % 34.77/5.45 fun_fu1590192889l_bool] : ! [v2: fun_bool_bool] : ! [v3: % 34.77/5.45 fun_fu114905943l_bool] : (v1 = v0 | ~ (hAPP_f1863694447l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f1863694447l_bool(v3, v2) = v0)) & ! [v0: fun_fu459093885l_bool] % 34.77/5.45 : ! [v1: fun_fu459093885l_bool] : ! [v2: fun_fu1590192889l_bool] : ! [v3: % 34.77/5.45 fun_fu816125185l_bool] : (v1 = v0 | ~ (hAPP_f1734879897l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f1734879897l_bool(v3, v2) = v0)) & ! [v0: fun_fu100249073l_bool] % 34.77/5.45 : ! [v1: fun_fu100249073l_bool] : ! [v2: fun_fu100249073l_bool] : ! [v3: % 34.77/5.45 fun_fu459093885l_bool] : (v1 = v0 | ~ (hAPP_f555424277l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f555424277l_bool(v3, v2) = v0)) & ! [v0: fun_fu983865091l_bool] % 34.77/5.45 : ! [v1: fun_fu983865091l_bool] : ! [v2: fun_bool_bool] : ! [v3: % 34.77/5.45 fun_fu2003389793l_bool] : (v1 = v0 | ~ (hAPP_f1560238713l_bool(v3, v2) = % 34.77/5.45 v1) | ~ (hAPP_f1560238713l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu1934636263l_bool] : ! [v1: fun_fu1934636263l_bool] : ! [v2: % 34.77/5.45 fun_fu983865091l_bool] : ! [v3: fun_fu1506313313l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f2032347769l_bool(v3, v2) = v1) | ~ (hAPP_f2032347769l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr633696065l_bool] : ! [v1: fun_Pr633696065l_bool] : % 34.77/5.45 ! [v2: fun_Pr633696065l_bool] : ! [v3: fun_fu1934636263l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f641257349l_bool(v3, v2) = v1) | ~ (hAPP_f641257349l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_bool_bool] : ! [v1: fun_bool_bool] : ! [v2: bool] : % 34.77/5.45 ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | ~ (hAPP_b589554111l_bool(v3, v2) % 34.77/5.45 = v1) | ~ (hAPP_b589554111l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu1319073539l_bool] : ! [v1: fun_fu1319073539l_bool] : ! [v2: % 34.77/5.45 fun_bool_bool] : ! [v3: fun_fu1485943649l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f1308714617l_bool(v3, v2) = v1) | ~ (hAPP_f1308714617l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu2122484477l_bool] : ! [v1: fun_fu2122484477l_bool] : % 34.77/5.45 ! [v2: fun_fu1319073539l_bool] : ! [v3: fun_fu2023535095l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f917296015l_bool(v3, v2) = v1) | ~ (hAPP_f917296015l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_ex1201926843l_bool] : ! [v1: fun_ex1201926843l_bool] % 34.77/5.45 : ! [v2: fun_ex1201926843l_bool] : ! [v3: fun_fu2122484477l_bool] : (v1 = v0 % 34.77/5.45 | ~ (hAPP_f546724245l_bool(v3, v2) = v1) | ~ (hAPP_f546724245l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_fu964448643l_bool] : ! [v1: % 34.77/5.45 fun_fu964448643l_bool] : ! [v2: fun_Pr691271849l_bool] : ! [v3: % 34.77/5.45 fun_fu169292119l_bool] : (v1 = v0 | ~ (hAPP_f2052660463l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f2052660463l_bool(v3, v2) = v0)) & ! [v0: fun_fu911981683l_bool] % 34.77/5.45 : ! [v1: fun_fu911981683l_bool] : ! [v2: fun_fu964448643l_bool] : ! [v3: % 34.77/5.45 fun_fu1755700589l_bool] : (v1 = v0 | ~ (hAPP_f1043869573l_bool(v3, v2) = % 34.77/5.45 v1) | ~ (hAPP_f1043869573l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu100249073l_bool] : ! [v1: fun_fu100249073l_bool] : ! [v2: % 34.77/5.45 fun_fu1133203323on_val] : ! [v3: fun_fu911981683l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f927043595l_bool(v3, v2) = v1) | ~ (hAPP_f927043595l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_Pr336360217on_val] : ! [v1: fun_Pr336360217on_val] : % 34.77/5.45 ! [v2: fun_fu1133203323on_val] : ! [v3: fun_fu442091053on_val] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f204556415on_val(v3, v2) = v1) | ~ (hAPP_f204556415on_val(v3, v2) = % 34.77/5.45 v0)) & ! [v0: produc1102272487on_val] : ! [v1: produc1102272487on_val] : % 34.77/5.45 ! [v2: produc12694297on_val] : ! [v3: fun_Pr336360217on_val] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P2024243179on_val(v3, v2) = v1) | ~ (hAPP_P2024243179on_val(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1640122725l_bool] : ! [v1: fun_fu1640122725l_bool] : % 34.77/5.45 ! [v2: fun_Pr680585871l_bool] : ! [v3: fun_fu369322201l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1233687287l_bool(v3, v2) = v1) | ~ (hAPP_f1233687287l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_fu1262577777l_bool] : ! [v1: fun_fu1262577777l_bool] % 34.77/5.45 : ! [v2: fun_fu1640122725l_bool] : ! [v3: fun_fu626845499l_bool] : (v1 = v0 % 34.77/5.45 | ~ (hAPP_f399538905l_bool(v3, v2) = v1) | ~ (hAPP_f399538905l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_fu100249073l_bool] : ! [v1: % 34.77/5.45 fun_fu100249073l_bool] : ! [v2: fun_fu2073188913on_val] : ! [v3: % 34.77/5.45 fun_fu1262577777l_bool] : (v1 = v0 | ~ (hAPP_f850751421l_bool(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f850751421l_bool(v3, v2) = v0)) & ! [v0: fun_Pr231134077on_val] % 34.77/5.45 : ! [v1: fun_Pr231134077on_val] : ! [v2: fun_fu2073188913on_val] : ! [v3: % 34.77/5.45 fun_fu192331261on_val] : (v1 = v0 | ~ (hAPP_f1309113673on_val(v3, v2) = v1) % 34.77/5.45 | ~ (hAPP_f1309113673on_val(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_fu2085256997l_bool] : ! [v1: fun_fu2085256997l_bool] : ! [v2: % 34.77/5.45 fun_Pr1696029455l_bool] : ! [v3: fun_fu1929656089l_bool] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f881985847l_bool(v3, v2) = v1) | ~ (hAPP_f881985847l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu1176482875l_bool] : ! [v1: fun_fu1176482875l_bool] : % 34.77/5.45 ! [v2: fun_fu2085256997l_bool] : ! [v3: fun_fu1452544581l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1438732387l_bool(v3, v2) = v1) | ~ (hAPP_f1438732387l_bool(v3, % 34.77/5.45 v2) = v0)) & ! [v0: fun_Pr633696065l_bool] : ! [v1: % 34.77/5.45 fun_Pr633696065l_bool] : ! [v2: fun_Pr1719283041on_val] : ! [v3: % 34.77/5.45 fun_fu1176482875l_bool] : (v1 = v0 | ~ (hAPP_f1241216909l_bool(v3, v2) = % 34.77/5.45 v1) | ~ (hAPP_f1241216909l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.45 fun_Pr1727285475on_val] : ! [v1: fun_Pr1727285475on_val] : ! [v2: % 34.77/5.45 fun_Pr1719283041on_val] : ! [v3: fun_fu1753546205on_val] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_f394183983on_val(v3, v2) = v1) | ~ (hAPP_f394183983on_val(v3, v2) = % 34.77/5.45 v0)) & ! [v0: produc12694297on_val] : ! [v1: produc12694297on_val] : ! % 34.77/5.45 [v2: produc1102272487on_val] : ! [v3: fun_Pr1727285475on_val] : (v1 = v0 | ~ % 34.77/5.45 (hAPP_P1760219823on_val(v3, v2) = v1) | ~ (hAPP_P1760219823on_val(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_fu225006629l_bool] : ! [v1: fun_fu225006629l_bool] : % 34.77/5.45 ! [v2: fun_Pr1696029455l_bool] : ! [v3: fun_fu1802993177l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f1825030711l_bool(v3, v2) = v1) | ~ (hAPP_f1825030711l_bool(v3, v2) % 34.77/5.45 = v0)) & ! [v0: fun_fu676595845l_bool] : ! [v1: fun_fu676595845l_bool] : % 34.77/5.45 ! [v2: fun_fu225006629l_bool] : ! [v3: fun_fu1104572687l_bool] : (v1 = v0 | % 34.77/5.45 ~ (hAPP_f516738477l_bool(v3, v2) = v1) | ~ (hAPP_f516738477l_bool(v3, v2) = % 34.77/5.45 v0)) & ! [v0: fun_ex1201926843l_bool] : ! [v1: fun_ex1201926843l_bool] : % 34.77/5.45 ! [v2: fun_ex1005552999on_val] : ! [v3: fun_fu676595845l_bool] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f653692369l_bool(v3, v2) = v1) | ~ (hAPP_f653692369l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_Pr2087158653on_val] : ! [v1: fun_Pr2087158653on_val] : % 34.77/5.46 ! [v2: fun_ex1005552999on_val] : ! [v3: fun_fu1924376903on_val] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f1520199827on_val(v3, v2) = v1) | ~ (hAPP_f1520199827on_val(v3, % 34.77/5.46 v2) = v0)) & ! [v0: produc12694297on_val] : ! [v1: % 34.77/5.46 produc12694297on_val] : ! [v2: produc124828825on_val] : ! [v3: % 34.77/5.46 fun_Pr2087158653on_val] : (v1 = v0 | ~ (hAPP_P789556885on_val(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_P789556885on_val(v3, v2) = v0)) & ! [v0: fun_Pr680585871l_bool] % 34.77/5.46 : ! [v1: fun_Pr680585871l_bool] : ! [v2: fun_ex1201926843l_bool] : ! [v3: % 34.77/5.46 fun_fu254083683l_bool] : (v1 = v0 | ~ (hAPP_f1930574389l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_f1930574389l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.46 fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : ! [v2: % 34.77/5.46 exp_list_char] : ! [v3: fun_ex1201926843l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_e1833980889l_bool(v3, v2) = v1) | ~ (hAPP_e1833980889l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_Pr691271849l_bool] : ! [v1: fun_Pr691271849l_bool] : % 34.77/5.46 ! [v2: fun_Pr633696065l_bool] : ! [v3: fun_fu371764249l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_f635218277l_bool(v3, v2) = v1) | ~ (hAPP_f635218277l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_Pr680585871l_bool] : ! [v1: fun_Pr680585871l_bool] : % 34.77/5.46 ! [v2: produc124828825on_val] : ! [v3: fun_Pr633696065l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_P1116729363l_bool(v3, v2) = v1) | ~ (hAPP_P1116729363l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_fu1989717467l_bool] : ! [v1: fun_fu1989717467l_bool] : % 34.77/5.46 ! [v2: fun_fu114905943l_bool] : ! [v3: fun_fu48585473l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_f592397849l_bool(v3, v2) = v1) | ~ (hAPP_f592397849l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_fu1457514859l_bool] : ! [v1: fun_fu1457514859l_bool] : % 34.77/5.46 ! [v2: fun_bo1549164019l_bool] : ! [v3: fun_fu781882819l_bool] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f1977633121l_bool(v3, v2) = v1) | ~ (hAPP_f1977633121l_bool(v3, v2) % 34.77/5.46 = v0)) & ! [v0: fun_fu712248957l_bool] : ! [v1: fun_fu712248957l_bool] : % 34.77/5.46 ! [v2: fun_fu2083094209l_bool] : ! [v3: fun_fu938561337l_bool] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f348318673l_bool(v3, v2) = v1) | ~ (hAPP_f348318673l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_fu250820942l_bool] : ! [v1: fun_fu250820942l_bool] : % 34.77/5.46 ! [v2: fun_fu1246919812l_bool] : ! [v3: fun_fu1457514859l_bool] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f1452292669l_bool(v3, v2) = v1) | ~ (hAPP_f1452292669l_bool(v3, v2) % 34.77/5.46 = v0)) & ! [v0: fun_fu1806184744l_bool] : ! [v1: fun_fu1806184744l_bool] % 34.77/5.46 : ! [v2: fun_fu250820942l_bool] : ! [v3: fun_fu1989717467l_bool] : (v1 = v0 % 34.77/5.46 | ~ (hAPP_f1523875321l_bool(v3, v2) = v1) | ~ (hAPP_f1523875321l_bool(v3, % 34.77/5.46 v2) = v0)) & ! [v0: fun_fu570492181l_bool] : ! [v1: % 34.77/5.46 fun_fu570492181l_bool] : ! [v2: fun_fu2141444501y_bool] : ! [v3: % 34.77/5.46 fun_fu712248957l_bool] : (v1 = v0 | ~ (hAPP_f857351829l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_f857351829l_bool(v3, v2) = v0)) & ! [v0: fun_fu863769827l_bool] % 34.77/5.46 : ! [v1: fun_fu863769827l_bool] : ! [v2: fun_fu570492181l_bool] : ! [v3: % 34.77/5.46 fun_fu1680591819l_bool] : (v1 = v0 | ~ (hAPP_f838396643l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_f838396643l_bool(v3, v2) = v0)) & ! [v0: fun_fu100249073l_bool] % 34.77/5.46 : ! [v1: fun_fu100249073l_bool] : ! [v2: fun_li688206603ion_ty] : ! [v3: % 34.77/5.46 fun_fu863769827l_bool] : (v1 = v0 | ~ (hAPP_f550652027l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_f550652027l_bool(v3, v2) = v0)) & ! [v0: fun_fu100249073l_bool] % 34.77/5.46 : ! [v1: fun_fu100249073l_bool] : ! [v2: fun_fu100249073l_bool] : ! [v3: % 34.77/5.46 fun_fu1806184744l_bool] : (v1 = v0 | ~ (cOMBS_570216337l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (cOMBS_570216337l_bool(v3, v2) = v0)) & ! [v0: fun_Pr1696029455l_bool] % 34.77/5.46 : ! [v1: fun_Pr1696029455l_bool] : ! [v2: fun_fu100249073l_bool] : ! [v3: % 34.77/5.46 fun_fu947198233l_bool] : (v1 = v0 | ~ (hAPP_f2121594859l_bool(v3, v2) = v1) % 34.77/5.46 | ~ (hAPP_f2121594859l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.46 fun_fu1693644106l_bool] : ! [v1: fun_fu1693644106l_bool] : ! [v2: % 34.77/5.46 fun_na939144002on_val] : ! [v3: fun_fu100249073l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_f1175813647l_bool(v3, v2) = v1) | ~ (hAPP_f1175813647l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_li1432931796on_val] : % 34.77/5.46 ! [v3: fun_fu1693644106l_bool] : (v1 = v0 | ~ (hAPP_f1033709212l_bool(v3, v2) % 34.77/5.46 = v1) | ~ (hAPP_f1033709212l_bool(v3, v2) = v0)) & ! [v0: exp_list_char] % 34.77/5.46 : ! [v1: exp_list_char] : ! [v2: exp_list_char] : ! [v3: list_char] : (v1 = % 34.77/5.46 v0 | ~ (lAss_list_char(v3, v2) = v1) | ~ (lAss_list_char(v3, v2) = v0)) & % 34.77/5.46 ! [v0: exp_list_char] : ! [v1: exp_list_char] : ! [v2: exp_list_char] : ! % 34.77/5.46 [v3: exp_list_char] : (v1 = v0 | ~ (seq_list_char(v3, v2) = v1) | ~ % 34.77/5.46 (seq_list_char(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: % 34.77/5.46 fun_Pr1696029455l_bool] : ! [v3: produc12694297on_val] : (v1 = v0 | ~ % 34.77/5.46 (member763590124on_val(v3, v2) = v1) | ~ (member763590124on_val(v3, v2) = % 34.77/5.46 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_Pr680585871l_bool] : ! % 34.77/5.46 [v3: produc124828825on_val] : (v1 = v0 | ~ (member840932460on_val(v3, v2) = % 34.77/5.46 v1) | ~ (member840932460on_val(v3, v2) = v0)) & ! [v0: % 34.77/5.46 fun_fu1670877422y_bool] : ! [v1: fun_fu1670877422y_bool] : ! [v2: % 34.77/5.46 fun_na939144002on_val] : ! [v3: fun_fu2141444501y_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_f1213370163y_bool(v3, v2) = v1) | ~ (hAPP_f1213370163y_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_fu964075521y_bool] : ! [v1: fun_fu964075521y_bool] : % 34.77/5.46 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu1670877422y_bool] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f2060496320y_bool(v3, v2) = v1) | ~ (hAPP_f2060496320y_bool(v3, v2) % 34.77/5.46 = v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_li688206603ion_ty] : % 34.77/5.46 ! [v3: fun_fu964075521y_bool] : (v1 = v0 | ~ (hAPP_f1001225811y_bool(v3, v2) % 34.77/5.46 = v1) | ~ (hAPP_f1001225811y_bool(v3, v2) = v0)) & ! [v0: bool] : ! % 34.77/5.46 [v1: bool] : ! [v2: fun_na939144002on_val] : ! [v3: fun_fu1246919812l_bool] % 34.77/5.46 : (v1 = v0 | ~ (hAPP_f61040418l_bool(v3, v2) = v1) | ~ % 34.77/5.46 (hAPP_f61040418l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! % 34.77/5.46 [v2: produc124828825on_val] : ! [v3: fun_Pr680585871l_bool] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_P1708370145l_bool(v3, v2) = v1) | ~ (hAPP_P1708370145l_bool(v3, v2) = % 34.77/5.46 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: produc1102272487on_val] : % 34.77/5.46 ! [v3: fun_Pr691271849l_bool] : (v1 = v0 | ~ (hAPP_P282169671l_bool(v3, v2) = % 34.77/5.46 v1) | ~ (hAPP_P282169671l_bool(v3, v2) = v0)) & ! [v0: % 34.77/5.46 fun_Pr1696029455l_bool] : ! [v1: fun_Pr1696029455l_bool] : ! [v2: % 34.77/5.46 fun_li688206603ion_ty] : ! [v3: list_P1999446415t_char] : (v1 = v0 | ~ % 34.77/5.46 (typeSa1844245082_sconf(v3, v2) = v1) | ~ (typeSa1844245082_sconf(v3, v2) = % 34.77/5.46 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: produc12694297on_val] : ! % 34.77/5.46 [v3: fun_Pr1696029455l_bool] : (v1 = v0 | ~ (hAPP_P159683425l_bool(v3, v2) = % 34.77/5.46 v1) | ~ (hAPP_P159683425l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 34.77/5.46 bool] : ! [v2: list_P1999446415t_char] : ! [v3: fun_li318226104r_bool] : % 34.77/5.46 (v1 = v0 | ~ (wf_pro755087577t_char(v3, v2) = v1) | ~ % 34.77/5.46 (wf_pro755087577t_char(v3, v2) = v0)) & ! [v0: option_ty] : ! [v1: % 34.77/5.46 option_ty] : ! [v2: list_char] : ! [v3: fun_li688206603ion_ty] : (v1 = v0 % 34.77/5.46 | ~ (hAPP_l512744617ion_ty(v3, v2) = v1) | ~ (hAPP_l512744617ion_ty(v3, % 34.77/5.46 v2) = v0)) & ! [v0: fun_Pr714818201on_val] : ! [v1: % 34.77/5.46 fun_Pr714818201on_val] : ! [v2: produc124828825on_val] : ! [v3: % 34.77/5.46 fun_Pr1391347915on_val] : (v1 = v0 | ~ (hAPP_P1870962205on_val(v3, v2) = % 34.77/5.46 v1) | ~ (hAPP_P1870962205on_val(v3, v2) = v0)) & ! [v0: % 34.77/5.46 fun_Pr231134077on_val] : ! [v1: fun_Pr231134077on_val] : ! [v2: % 34.77/5.46 exp_list_char] : ! [v3: fun_ex977868519on_val] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_e1659493427on_val(v3, v2) = v1) | ~ (hAPP_e1659493427on_val(v3, v2) = % 34.77/5.46 v0)) & ! [v0: fun_fu1690035458on_val] : ! [v1: fun_fu1690035458on_val] : % 34.77/5.46 ! [v2: fun_na939144002on_val] : ! [v3: fun_fu1639641777on_val] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f1849790461on_val(v3, v2) = v1) | ~ (hAPP_f1849790461on_val(v3, v2) % 34.77/5.46 = v0)) & ! [v0: produc12694297on_val] : ! [v1: produc12694297on_val] : % 34.77/5.46 ! [v2: fun_li1432931796on_val] : ! [v3: fun_fu1690035458on_val] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_f1727192346on_val(v3, v2) = v1) | ~ (hAPP_f1727192346on_val(v3, v2) % 34.77/5.46 = v0)) & ! [v0: produc124828825on_val] : ! [v1: produc124828825on_val] : % 34.77/5.46 ! [v2: produc12694297on_val] : ! [v3: fun_Pr231134077on_val] : (v1 = v0 | ~ % 34.77/5.46 (hAPP_P604205461on_val(v3, v2) = v1) | ~ (hAPP_P604205461on_val(v3, v2) = % 34.77/5.46 v0)) & ! [v0: produc1102272487on_val] : ! [v1: produc1102272487on_val] : % 34.77/5.46 ! [v2: produc124828825on_val] : ! [v3: fun_Pr714818201on_val] : (v1 = v0 | % 34.77/5.46 ~ (hAPP_P1886180715on_val(v3, v2) = v1) | ~ (hAPP_P1886180715on_val(v3, v2) % 34.77/5.46 = v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_Pr691271849l_bool] : % 34.77/5.46 ! [v3: produc1102272487on_val] : (v1 = v0 | ~ (member773094996on_val(v3, v2) % 34.77/5.46 = v1) | ~ (member773094996on_val(v3, v2) = v0)) & ! [v0: option_val] : % 34.77/5.46 ! [v1: option_val] : ! [v2: list_char] : ! [v3: fun_li1432931796on_val] : % 34.77/5.46 (v1 = v0 | ~ (hAPP_l207779698on_val(v3, v2) = v1) | ~ % 34.77/5.46 (hAPP_l207779698on_val(v3, v2) = v0)) & ! [v0: fun_li688206603ion_ty] : ! % 34.77/5.46 [v1: fun_li688206603ion_ty] : ! [v2: option_ty] : (v1 = v0 | ~ % 34.77/5.46 (cOMBK_1294242658t_char(v2) = v1) | ~ (cOMBK_1294242658t_char(v2) = v0)) & % 34.77/5.46 ! [v0: fun_li1432931796on_val] : ! [v1: fun_li1432931796on_val] : ! [v2: % 34.77/5.46 option_val] : (v1 = v0 | ~ (cOMBK_1097134891t_char(v2) = v1) | ~ % 34.77/5.46 (cOMBK_1097134891t_char(v2) = v0)) & ! [v0: exp_list_char] : ! [v1: % 34.77/5.46 exp_list_char] : ! [v2: val] : (v1 = v0 | ~ (val_list_char(v2) = v1) | ~ % 34.77/5.46 (val_list_char(v2) = v0)) & ! [v0: fun_na939144002on_val] : ! [v1: % 34.77/5.46 fun_na939144002on_val] : ! [v2: produc12694297on_val] : (v1 = v0 | ~ % 34.77/5.46 (hp(v2) = v1) | ~ (hp(v2) = v0)) & ! [v0: fun_fu2141444501y_bool] : ! % 34.77/5.46 [v1: fun_fu2141444501y_bool] : ! [v2: list_P1999446415t_char] : (v1 = v0 | ~ % 34.77/5.46 (lconf_496643946t_char(v2) = v1) | ~ (lconf_496643946t_char(v2) = v0)) & ! % 34.77/5.46 [v0: fun_fu1246919812l_bool] : ! [v1: fun_fu1246919812l_bool] : ! [v2: % 34.77/5.46 list_P1999446415t_char] : (v1 = v0 | ~ (hconf_97414254t_char(v2) = v1) | ~ % 34.77/5.46 (hconf_97414254t_char(v2) = v0)) & ! [v0: option_ty] : ! [v1: option_ty] : % 34.77/5.46 ! [v2: ty] : (v1 = v0 | ~ (some_ty(v2) = v1) | ~ (some_ty(v2) = v0)) & ! % 34.77/5.46 [v0: fun_Pr691271849l_bool] : ! [v1: fun_Pr691271849l_bool] : ! [v2: % 34.77/5.46 list_P1999446415t_char] : (v1 = v0 | ~ (red(v2) = v1) | ~ (red(v2) = v0)) % 34.77/5.46 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: bool] : % 34.77/5.46 (v1 = v0 | ~ (hBOOL(v2) = v1) | ~ (hBOOL(v2) = v0)) & ! [v0: option_val] : % 34.77/5.46 ! [v1: option_val] : ! [v2: val] : (v1 = v0 | ~ (some_val(v2) = v1) | ~ % 34.77/5.46 (some_val(v2) = v0)) % 34.77/5.46 % 34.77/5.46 Further assumptions not needed in the proof: % 34.77/5.46 -------------------------------------------- % 34.77/5.46 fact_0_InitBlockRed_I3_J, fact_100_splitE, fact_101_splitE, fact_102_splitE, % 34.77/5.46 fact_103_WTrtBlock, fact_104_mem__splitI, fact_105_mem__splitI, % 34.77/5.46 fact_106_mem__splitI, fact_107_mem__splitI, fact_108_mem__splitI, % 34.77/5.46 fact_109_mem__splitI, fact_10_map__upd__eqD1, fact_110_WTrtSeq, % 34.77/5.46 fact_111_red__reds_OSeqRed, fact_112_red__reds_OLAssRed, % 34.77/5.46 fact_113_red__reds_ORedSeq, fact_114_red__reds_ORedBlock, fact_115_mem__splitE, % 34.77/5.46 fact_116_mem__splitE, fact_117_mem__splitE, fact_118_mem__splitE, % 34.77/5.46 fact_119_mem__splitE, fact_120_mem__splitE, fact_121_mem__splitI2, % 34.77/5.46 fact_122_mem__splitI2, fact_123_mem__splitI2, fact_124_mem__splitI2, % 34.77/5.46 fact_125_mem__splitI2, fact_126_mem__splitI2, fact_127_red__reds_ORedLAss, % 34.77/5.46 fact_128_cond__split__eta, fact_129_cond__split__eta, fact_12_prod__induct4, % 34.77/5.46 fact_130_cond__split__eta, fact_131_splitE2, fact_132_splitE2, fact_133_splitE2, % 34.77/5.46 fact_134_exp_Osimps_I143_J, fact_135_exp_Osimps_I196_J, % 34.77/5.46 fact_136_exp_Osimps_I3_J, fact_137_exp_Osimps_I11_J, fact_138_exp_Osimps_I6_J, % 34.77/5.46 fact_139_mem__def, fact_13_prod__cases4, fact_140_mem__def, fact_141_mem__def, % 34.77/5.46 fact_142_exp_Osimps_I10_J, fact_143_exp_Osimps_I84_J, fact_144_exp_Osimps_I74_J, % 34.77/5.46 fact_145_exp_Osimps_I85_J, fact_146_exp_Osimps_I75_J, fact_147_exp_Osimps_I82_J, % 34.77/5.46 fact_148_exp_Osimps_I83_J, fact_149_exp_Osimps_I145_J, % 34.77/5.46 fact_150_exp_Osimps_I144_J, fact_151_exp_Osimps_I197_J, % 34.77/5.46 fact_152_exp_Osimps_I142_J, fact_153_redp__redsp_OInitBlockRed, % 34.77/5.46 fact_154_red__reds_OBlockRedSome, fact_155_redp__redsp_OSeqRed, % 34.77/5.46 fact_156_redp__redsp_OLAssRed, fact_157_redp__redsp_OBlockRedNone, % 34.77/5.46 fact_158_redp__redsp_ORedSeq, fact_159_map__upd__nonempty, fact_15_Pair__inject, % 34.77/5.46 fact_160_map__upd__nonempty, fact_161_redp__redsp_ORedBlock, % 34.77/5.46 fact_162_empty__upd__none, fact_163_empty__upd__none, % 34.77/5.46 fact_164_redp__redsp_OBlockRedSome, fact_165_redp__red__eq, % 34.77/5.46 fact_166_redp__redsp_ORedInitBlock, fact_16_Pair__inject, fact_17_Pair__inject, % 34.77/5.46 fact_18_Pair__eq, fact_19_Pair__eq, fact_20_Pair__eq, % 34.77/5.46 fact_21_split__paired__All, fact_22_split__paired__All, % 34.77/5.46 fact_23_split__paired__All, fact_24_fun__upd__def, fact_25_fun__upd__def, % 34.77/5.46 fact_26_fun__upd__idem, fact_27_fun__upd__idem, fact_28_fun__upd__other, % 34.77/5.46 fact_29_fun__upd__other, fact_2_fun__upd__triv, fact_30_fun__upd__twist, % 34.77/5.46 fact_31_fun__upd__twist, fact_32_fun__upd__apply, fact_33_fun__upd__apply, % 34.77/5.46 fact_34_fun__upd__same, fact_35_fun__upd__same, fact_36_fun__upd__upd, % 34.77/5.46 fact_37_fun__upd__upd, fact_38_fun__upd__idem__iff, fact_39_fun__upd__idem__iff, % 34.77/5.46 fact_3_fun__upd__triv, fact_40_widen__refl, fact_41_red__preserves__hconf, % 34.77/5.46 fact_42_red__preserves__lconf, fact_43_prod__cases3, fact_44_prod__cases3, % 34.77/5.46 fact_45_prod__induct3, fact_46_prod__induct3, fact_47_red__preserves__sconf, % 34.77/5.46 fact_48_pred__equals__eq2, fact_49_pred__equals__eq2, fact_4_assms, % 34.77/5.46 fact_50_pred__equals__eq2, fact_51_prod_Oexhaust, fact_52_prod_Oexhaust, % 34.77/5.46 fact_53_prod_Oexhaust, fact_54_widen__trans, fact_55_InitBlockRed_I5_J, % 34.77/5.46 fact_56_split__paired__Ex, fact_57_split__paired__Ex, fact_58_split__paired__Ex, % 34.77/5.46 fact_59_PairE, fact_5_map__upd__Some__unfold, fact_60_PairE, fact_61_PairE, % 34.77/5.46 fact_62_internal__split__conv, fact_63_sconf__def, fact_64_prod__caseI, % 34.77/5.46 fact_65_prod__caseI, fact_66_prod__caseI, fact_67_splitI, fact_68_splitI, % 34.77/5.46 fact_69_splitI, fact_6_map__upd__Some__unfold, fact_70_splitD, fact_71_splitD, % 34.77/5.46 fact_72_splitD, fact_73_split__weak__cong, fact_74_split__weak__cong, % 34.77/5.46 fact_75_split__weak__cong, fact_76_internal__split__def, % 34.77/5.46 fact_77_internal__split__def, fact_78_internal__split__def, % 34.77/5.46 fact_79_split__twice, fact_7_map__upd__triv, fact_80_split__twice, % 34.77/5.46 fact_81_split__twice, fact_82_split__twice, fact_83_split__part, % 34.77/5.46 fact_84_split__part, fact_85_split__part, fact_86_prod_Osimps_I2_J, % 34.77/5.46 fact_87_prod_Osimps_I2_J, fact_88_prod_Osimps_I2_J, fact_89_split__conv, % 34.77/5.46 fact_8_map__upd__triv, fact_90_split__conv, fact_91_split__conv, % 34.77/5.46 fact_92_split__eta, fact_93_split__eta, fact_94_split__eta, % 34.77/5.46 fact_95_red__reds_OInitBlockRed, fact_96_red__reds_ORedInitBlock, % 34.77/5.46 fact_97_splitI2, fact_98_splitI2, fact_99_splitI2, fact_9_map__upd__eqD1, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__List__O, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__prod_Itc__Expr__, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__prod_Itc__fun_It, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Obool_J_000tc__fun_Itc, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_200, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_204, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_205, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_209, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc___210, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc___211, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O_206, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O_207, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O_202, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It_201, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It_203, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc_, % 34.77/5.46 help_COMBB_1_1_COMBB_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__208, % 34.77/5.46 help_COMBC_1_1_COMBC_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Optio, % 34.77/5.46 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It, % 34.77/5.46 help_COMBK_1_1_COMBK_000tc__Option__Ooption_Itc__Type__Oty_J_000tc__List__Olist_, % 34.77/5.46 help_COMBK_1_1_COMBK_000tc__Option__Ooption_Itc__Value__Oval_J_000tc__List__Olis, % 34.77/5.46 help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It, % 34.77/5.46 help_fconj_1_1_U, help_fconj_2_1_U, help_fconj_3_1_U % 34.77/5.46 % 34.77/5.46 Those formulas are unsatisfiable: % 34.77/5.46 --------------------------------- % 34.77/5.46 % 34.77/5.46 Begin of proof % 34.77/5.46 | % 34.77/5.46 | ALPHA: (fact_1_InitBlockRed_I1_J) implies: % 34.77/5.46 | (1) ? [v0: fun_Pr231134077on_val] : ? [v1: fun_fu1690035458on_val] : ? % 34.77/5.46 | [v2: option_val] : ? [v3: fun_li1432931796on_val] : ? [v4: % 34.77/5.46 | produc12694297on_val] : ? [v5: produc124828825on_val] : ? [v6: % 34.77/5.46 | fun_Pr714818201on_val] : ? [v7: fun_Pr231134077on_val] : ? [v8: % 34.77/5.46 | fun_fu1690035458on_val] : ? [v9: produc12694297on_val] : ? [v10: % 34.77/5.46 | produc124828825on_val] : ? [v11: produc1102272487on_val] : ? [v12: % 34.77/5.46 | fun_Pr691271849l_bool] : ? [v13: bool] : (fun_up1149430426on_val(la, % 34.77/5.46 | v_1, v2) = v3 & hAPP_P1870962205on_val(produc1441475159on_val, v5) % 34.77/5.46 | = v6 & hAPP_e1659493427on_val(produc1259058957on_val, ea) = v0 & % 34.77/5.46 | hAPP_e1659493427on_val(produc1259058957on_val, e_a) = v7 & % 34.77/5.46 | hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.77/5.46 | hAPP_f1849790461on_val(produc899768717on_val, h_a) = v8 & % 34.77/5.46 | hAPP_f1727192346on_val(v8, l_a) = v9 & hAPP_f1727192346on_val(v1, v3) % 34.77/5.46 | = v4 & hAPP_P604205461on_val(v7, v9) = v10 & % 34.77/5.46 | hAPP_P604205461on_val(v0, v4) = v5 & hAPP_P1886180715on_val(v6, v10) % 34.77/5.46 | = v11 & red(p) = v12 & member773094996on_val(v11, v12) = v13 & % 34.77/5.46 | hBOOL(v13) = 0 & some_val(v) = v2 & produc1102272487on_val(v11) & % 34.77/5.46 | produc12694297on_val(v9) & produc12694297on_val(v4) & % 34.77/5.46 | produc124828825on_val(v10) & produc124828825on_val(v5) & % 34.77/5.46 | fun_Pr691271849l_bool(v12) & fun_Pr231134077on_val(v7) & % 34.77/5.46 | fun_Pr231134077on_val(v0) & fun_Pr714818201on_val(v6) & % 34.77/5.46 | fun_fu1690035458on_val(v8) & fun_fu1690035458on_val(v1) & % 34.77/5.46 | fun_li1432931796on_val(v3) & option_val(v2) & bool(v13)) % 34.77/5.46 | % 34.77/5.46 | ALPHA: (fact_11_InitBlockRed_I2_J) implies: % 34.77/5.47 | (2) ? [v0: fun_fu1690035458on_val] : ? [v1: option_val] : ? [v2: % 34.77/5.47 | fun_li1432931796on_val] : ? [v3: produc12694297on_val] : % 34.77/5.47 | (fun_up1149430426on_val(la, v_1, v1) = v2 & % 34.77/5.47 | hAPP_f1849790461on_val(produc899768717on_val, ha) = v0 & % 34.77/5.47 | hAPP_f1727192346on_val(v0, v2) = v3 & some_val(v) = v1 & % 34.77/5.47 | produc12694297on_val(v3) & fun_fu1690035458on_val(v0) & % 34.77/5.47 | fun_li1432931796on_val(v2) & option_val(v1) & ! [v4: ty] : ! [v5: % 34.77/5.47 | fun_li688206603ion_ty] : ! [v6: bool] : ( ~ (wTrt(p, ha, v5, ea, % 34.77/5.47 | v4) = v6) | ~ fun_li688206603ion_ty(v5) | ~ ty(v4) | ? [v7: % 34.77/5.47 | fun_Pr1696029455l_bool] : ? [v8: bool] : ? [v9: any] : ? [v10: % 34.77/5.47 | any] : (typeSa1844245082_sconf(p, v5) = v7 & % 34.77/5.47 | hAPP_P159683425l_bool(v7, v3) = v8 & hBOOL(v8) = v9 & hBOOL(v6) = % 34.77/5.47 | v10 & fun_Pr1696029455l_bool(v7) & bool(v8) & ( ~ (v10 = 0) | ~ % 34.77/5.47 | (v9 = 0))) | ? [v7: ty] : ? [v8: bool] : ? [v9: bool] : % 34.77/5.47 | (wTrt(p, h_a, v5, e_a, v7) = v8 & widen_2090681816t_char(p, v7, v4) % 34.77/5.47 | = v9 & hBOOL(v9) = 0 & hBOOL(v8) = 0 & ty(v7) & bool(v9) & % 34.77/5.47 | bool(v8)))) % 34.77/5.47 | % 34.77/5.47 | ALPHA: (fact_14_InitBlockRed_I4_J) implies: % 34.77/5.47 | (3) ? [v0: fun_Pr1696029455l_bool] : ? [v1: fun_fu1690035458on_val] : ? % 34.77/5.47 | [v2: produc12694297on_val] : ? [v3: bool] : (typeSa1844245082_sconf(p, % 34.77/5.47 | e) = v0 & hAPP_P159683425l_bool(v0, v2) = v3 & % 34.77/5.47 | hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.77/5.47 | hAPP_f1727192346on_val(v1, la) = v2 & hBOOL(v3) = 0 & % 34.77/5.47 | produc12694297on_val(v2) & fun_Pr1696029455l_bool(v0) & % 34.77/5.47 | fun_fu1690035458on_val(v1) & bool(v3)) % 34.77/5.47 | % 34.77/5.47 | ALPHA: (conj_0) implies: % 34.77/5.47 | (4) ? [v0: fun_Pr231134077on_val] : ? [v1: fun_fu1690035458on_val] : ? % 34.77/5.47 | [v2: option_val] : ? [v3: fun_li1432931796on_val] : ? [v4: % 34.77/5.47 | produc12694297on_val] : ? [v5: produc124828825on_val] : ? [v6: % 34.77/5.47 | fun_Pr714818201on_val] : ? [v7: fun_Pr231134077on_val] : ? [v8: % 34.77/5.47 | fun_fu1690035458on_val] : ? [v9: produc12694297on_val] : ? [v10: % 34.77/5.47 | produc124828825on_val] : ? [v11: produc1102272487on_val] : ? [v12: % 34.77/5.47 | fun_Pr691271849l_bool] : ? [v13: bool] : ? [v14: int] : ( ~ (v14 = % 34.77/5.47 | 0) & fun_up1149430426on_val(la, v_1, v2) = v3 & % 34.77/5.47 | hAPP_P1870962205on_val(produc1441475159on_val, v5) = v6 & % 34.77/5.47 | hAPP_e1659493427on_val(produc1259058957on_val, ea) = v0 & % 34.77/5.47 | hAPP_e1659493427on_val(produc1259058957on_val, e_a) = v7 & % 34.77/5.47 | hAPP_f1849790461on_val(produc899768717on_val, ha) = v1 & % 34.77/5.47 | hAPP_f1849790461on_val(produc899768717on_val, h_a) = v8 & % 34.77/5.47 | hAPP_f1727192346on_val(v8, l_a) = v9 & hAPP_f1727192346on_val(v1, v3) % 34.77/5.47 | = v4 & hAPP_P604205461on_val(v7, v9) = v10 & % 34.77/5.47 | hAPP_P604205461on_val(v0, v4) = v5 & hAPP_P1886180715on_val(v6, v10) % 34.77/5.47 | = v11 & red(p) = v12 & member773094996on_val(v11, v12) = v13 & % 34.77/5.47 | hBOOL(v13) = v14 & some_val(v) = v2 & produc1102272487on_val(v11) & % 34.77/5.47 | produc12694297on_val(v9) & produc12694297on_val(v4) & % 34.77/5.47 | produc124828825on_val(v10) & produc124828825on_val(v5) & % 34.77/5.47 | fun_Pr691271849l_bool(v12) & fun_Pr231134077on_val(v7) & % 34.77/5.47 | fun_Pr231134077on_val(v0) & fun_Pr714818201on_val(v6) & % 34.77/5.47 | fun_fu1690035458on_val(v8) & fun_fu1690035458on_val(v1) & % 34.77/5.47 | fun_li1432931796on_val(v3) & option_val(v2) & bool(v13)) % 34.77/5.47 | % 34.77/5.47 | ALPHA: (function-axioms) implies: % 34.77/5.47 | (5) ! [v0: option_val] : ! [v1: option_val] : ! [v2: val] : (v1 = v0 | % 34.77/5.47 | ~ (some_val(v2) = v1) | ~ (some_val(v2) = v0)) % 34.77/5.47 | (6) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: bool] % 34.77/5.47 | : (v1 = v0 | ~ (hBOOL(v2) = v1) | ~ (hBOOL(v2) = v0)) % 34.77/5.47 | (7) ! [v0: fun_Pr691271849l_bool] : ! [v1: fun_Pr691271849l_bool] : ! % 34.77/5.47 | [v2: list_P1999446415t_char] : (v1 = v0 | ~ (red(v2) = v1) | ~ % 34.77/5.47 | (red(v2) = v0)) % 34.77/5.47 | (8) ! [v0: bool] : ! [v1: bool] : ! [v2: fun_Pr691271849l_bool] : ! % 34.77/5.47 | [v3: produc1102272487on_val] : (v1 = v0 | ~ (member773094996on_val(v3, % 34.77/5.47 | v2) = v1) | ~ (member773094996on_val(v3, v2) = v0)) % 34.77/5.47 | (9) ! [v0: produc1102272487on_val] : ! [v1: produc1102272487on_val] : ! % 34.77/5.47 | [v2: produc124828825on_val] : ! [v3: fun_Pr714818201on_val] : (v1 = v0 % 34.77/5.47 | | ~ (hAPP_P1886180715on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_P1886180715on_val(v3, v2) = v0)) % 34.77/5.47 | (10) ! [v0: produc124828825on_val] : ! [v1: produc124828825on_val] : ! % 34.77/5.47 | [v2: produc12694297on_val] : ! [v3: fun_Pr231134077on_val] : (v1 = v0 % 34.77/5.47 | | ~ (hAPP_P604205461on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_P604205461on_val(v3, v2) = v0)) % 34.77/5.47 | (11) ! [v0: produc12694297on_val] : ! [v1: produc12694297on_val] : ! % 34.77/5.47 | [v2: fun_li1432931796on_val] : ! [v3: fun_fu1690035458on_val] : (v1 = % 34.77/5.47 | v0 | ~ (hAPP_f1727192346on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_f1727192346on_val(v3, v2) = v0)) % 34.77/5.47 | (12) ! [v0: fun_fu1690035458on_val] : ! [v1: fun_fu1690035458on_val] : ! % 34.77/5.47 | [v2: fun_na939144002on_val] : ! [v3: fun_fu1639641777on_val] : (v1 = % 34.77/5.47 | v0 | ~ (hAPP_f1849790461on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_f1849790461on_val(v3, v2) = v0)) % 34.77/5.47 | (13) ! [v0: fun_Pr231134077on_val] : ! [v1: fun_Pr231134077on_val] : ! % 34.77/5.47 | [v2: exp_list_char] : ! [v3: fun_ex977868519on_val] : (v1 = v0 | ~ % 34.77/5.47 | (hAPP_e1659493427on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_e1659493427on_val(v3, v2) = v0)) % 34.77/5.47 | (14) ! [v0: fun_Pr714818201on_val] : ! [v1: fun_Pr714818201on_val] : ! % 34.77/5.47 | [v2: produc124828825on_val] : ! [v3: fun_Pr1391347915on_val] : (v1 = % 34.77/5.47 | v0 | ~ (hAPP_P1870962205on_val(v3, v2) = v1) | ~ % 34.77/5.47 | (hAPP_P1870962205on_val(v3, v2) = v0)) % 34.77/5.47 | (15) ! [v0: fun_li1432931796on_val] : ! [v1: fun_li1432931796on_val] : ! % 34.77/5.47 | [v2: option_val] : ! [v3: list_char] : ! [v4: % 34.77/5.47 | fun_li1432931796on_val] : (v1 = v0 | ~ (fun_up1149430426on_val(v4, % 34.77/5.47 | v3, v2) = v1) | ~ (fun_up1149430426on_val(v4, v3, v2) = v0)) % 34.77/5.47 | % 34.77/5.48 | DELTA: instantiating (3) with fresh symbols all_430_0, all_430_1, all_430_2, % 34.77/5.48 | all_430_3 gives: % 34.77/5.48 | (16) typeSa1844245082_sconf(p, e) = all_430_3 & % 34.77/5.48 | hAPP_P159683425l_bool(all_430_3, all_430_1) = all_430_0 & % 34.77/5.48 | hAPP_f1849790461on_val(produc899768717on_val, ha) = all_430_2 & % 34.77/5.48 | hAPP_f1727192346on_val(all_430_2, la) = all_430_1 & hBOOL(all_430_0) = % 34.77/5.48 | 0 & produc12694297on_val(all_430_1) & % 34.77/5.48 | fun_Pr1696029455l_bool(all_430_3) & fun_fu1690035458on_val(all_430_2) % 34.77/5.48 | & bool(all_430_0) % 34.77/5.48 | % 34.77/5.48 | ALPHA: (16) implies: % 34.77/5.48 | (17) hAPP_f1849790461on_val(produc899768717on_val, ha) = all_430_2 % 34.77/5.48 | % 34.77/5.48 | DELTA: instantiating (2) with fresh symbols all_464_0, all_464_1, all_464_2, % 34.77/5.48 | all_464_3 gives: % 34.77/5.48 | (18) fun_up1149430426on_val(la, v_1, all_464_2) = all_464_1 & % 34.77/5.48 | hAPP_f1849790461on_val(produc899768717on_val, ha) = all_464_3 & % 34.77/5.48 | hAPP_f1727192346on_val(all_464_3, all_464_1) = all_464_0 & some_val(v) % 34.77/5.48 | = all_464_2 & produc12694297on_val(all_464_0) & % 34.77/5.48 | fun_fu1690035458on_val(all_464_3) & fun_li1432931796on_val(all_464_1) % 34.77/5.48 | & option_val(all_464_2) & ! [v0: ty] : ! [v1: fun_li688206603ion_ty] % 34.77/5.48 | : ! [v2: bool] : ( ~ (wTrt(p, ha, v1, ea, v0) = v2) | ~ % 34.77/5.48 | fun_li688206603ion_ty(v1) | ~ ty(v0) | ? [v3: % 34.77/5.48 | fun_Pr1696029455l_bool] : ? [v4: bool] : ? [v5: any] : ? [v6: % 34.77/5.48 | any] : (typeSa1844245082_sconf(p, v1) = v3 & % 34.77/5.48 | hAPP_P159683425l_bool(v3, all_464_0) = v4 & hBOOL(v4) = v5 & % 34.77/5.48 | hBOOL(v2) = v6 & fun_Pr1696029455l_bool(v3) & bool(v4) & ( ~ (v6 = % 34.77/5.48 | 0) | ~ (v5 = 0))) | ? [v3: ty] : ? [v4: bool] : ? [v5: % 34.77/5.48 | bool] : (wTrt(p, h_a, v1, e_a, v3) = v4 & % 34.77/5.48 | widen_2090681816t_char(p, v3, v0) = v5 & hBOOL(v5) = 0 & hBOOL(v4) % 34.77/5.48 | = 0 & ty(v3) & bool(v5) & bool(v4))) % 34.77/5.48 | % 34.77/5.48 | ALPHA: (18) implies: % 34.77/5.48 | (19) some_val(v) = all_464_2 % 34.77/5.48 | (20) hAPP_f1727192346on_val(all_464_3, all_464_1) = all_464_0 % 34.77/5.48 | (21) hAPP_f1849790461on_val(produc899768717on_val, ha) = all_464_3 % 34.77/5.48 | (22) fun_up1149430426on_val(la, v_1, all_464_2) = all_464_1 % 34.77/5.48 | % 34.77/5.48 | DELTA: instantiating (1) with fresh symbols all_467_0, all_467_1, all_467_2, % 34.77/5.48 | all_467_3, all_467_4, all_467_5, all_467_6, all_467_7, all_467_8, % 34.77/5.48 | all_467_9, all_467_10, all_467_11, all_467_12, all_467_13 gives: % 34.77/5.48 | (23) fun_up1149430426on_val(la, v_1, all_467_11) = all_467_10 & % 34.77/5.48 | hAPP_P1870962205on_val(produc1441475159on_val, all_467_8) = all_467_7 % 34.77/5.48 | & hAPP_e1659493427on_val(produc1259058957on_val, ea) = all_467_13 & % 34.77/5.48 | hAPP_e1659493427on_val(produc1259058957on_val, e_a) = all_467_6 & % 34.77/5.48 | hAPP_f1849790461on_val(produc899768717on_val, ha) = all_467_12 & % 34.77/5.48 | hAPP_f1849790461on_val(produc899768717on_val, h_a) = all_467_5 & % 34.77/5.48 | hAPP_f1727192346on_val(all_467_5, l_a) = all_467_4 & % 34.77/5.48 | hAPP_f1727192346on_val(all_467_12, all_467_10) = all_467_9 & % 34.77/5.48 | hAPP_P604205461on_val(all_467_6, all_467_4) = all_467_3 & % 34.77/5.48 | hAPP_P604205461on_val(all_467_13, all_467_9) = all_467_8 & % 34.77/5.48 | hAPP_P1886180715on_val(all_467_7, all_467_3) = all_467_2 & red(p) = % 34.77/5.48 | all_467_1 & member773094996on_val(all_467_2, all_467_1) = all_467_0 & % 34.77/5.48 | hBOOL(all_467_0) = 0 & some_val(v) = all_467_11 & % 34.77/5.48 | produc1102272487on_val(all_467_2) & produc12694297on_val(all_467_4) & % 34.77/5.48 | produc12694297on_val(all_467_9) & produc124828825on_val(all_467_3) & % 34.77/5.48 | produc124828825on_val(all_467_8) & fun_Pr691271849l_bool(all_467_1) & % 34.77/5.48 | fun_Pr231134077on_val(all_467_6) & fun_Pr231134077on_val(all_467_13) & % 34.77/5.48 | fun_Pr714818201on_val(all_467_7) & fun_fu1690035458on_val(all_467_5) & % 34.77/5.48 | fun_fu1690035458on_val(all_467_12) & % 34.77/5.48 | fun_li1432931796on_val(all_467_10) & option_val(all_467_11) & % 34.77/5.48 | bool(all_467_0) % 34.77/5.48 | % 34.77/5.48 | ALPHA: (23) implies: % 34.77/5.48 | (24) some_val(v) = all_467_11 % 34.77/5.48 | (25) hBOOL(all_467_0) = 0 % 34.77/5.48 | (26) member773094996on_val(all_467_2, all_467_1) = all_467_0 % 34.77/5.48 | (27) red(p) = all_467_1 % 34.77/5.48 | (28) hAPP_P1886180715on_val(all_467_7, all_467_3) = all_467_2 % 34.77/5.48 | (29) hAPP_P604205461on_val(all_467_13, all_467_9) = all_467_8 % 34.77/5.48 | (30) hAPP_P604205461on_val(all_467_6, all_467_4) = all_467_3 % 34.77/5.48 | (31) hAPP_f1727192346on_val(all_467_12, all_467_10) = all_467_9 % 34.77/5.48 | (32) hAPP_f1727192346on_val(all_467_5, l_a) = all_467_4 % 34.77/5.48 | (33) hAPP_f1849790461on_val(produc899768717on_val, h_a) = all_467_5 % 34.77/5.48 | (34) hAPP_f1849790461on_val(produc899768717on_val, ha) = all_467_12 % 34.77/5.48 | (35) hAPP_e1659493427on_val(produc1259058957on_val, e_a) = all_467_6 % 34.77/5.48 | (36) hAPP_e1659493427on_val(produc1259058957on_val, ea) = all_467_13 % 34.77/5.48 | (37) hAPP_P1870962205on_val(produc1441475159on_val, all_467_8) = all_467_7 % 34.77/5.48 | (38) fun_up1149430426on_val(la, v_1, all_467_11) = all_467_10 % 34.77/5.48 | % 34.77/5.48 | DELTA: instantiating (4) with fresh symbols all_469_0, all_469_1, all_469_2, % 34.77/5.48 | all_469_3, all_469_4, all_469_5, all_469_6, all_469_7, all_469_8, % 34.77/5.48 | all_469_9, all_469_10, all_469_11, all_469_12, all_469_13, all_469_14 % 34.77/5.48 | gives: % 34.77/5.48 | (39) ~ (all_469_0 = 0) & fun_up1149430426on_val(la, v_1, all_469_12) = % 34.77/5.48 | all_469_11 & hAPP_P1870962205on_val(produc1441475159on_val, all_469_9) % 34.77/5.48 | = all_469_8 & hAPP_e1659493427on_val(produc1259058957on_val, ea) = % 34.77/5.48 | all_469_14 & hAPP_e1659493427on_val(produc1259058957on_val, e_a) = % 34.77/5.48 | all_469_7 & hAPP_f1849790461on_val(produc899768717on_val, ha) = % 34.77/5.48 | all_469_13 & hAPP_f1849790461on_val(produc899768717on_val, h_a) = % 34.77/5.48 | all_469_6 & hAPP_f1727192346on_val(all_469_6, l_a) = all_469_5 & % 34.77/5.48 | hAPP_f1727192346on_val(all_469_13, all_469_11) = all_469_10 & % 34.77/5.48 | hAPP_P604205461on_val(all_469_7, all_469_5) = all_469_4 & % 34.77/5.48 | hAPP_P604205461on_val(all_469_14, all_469_10) = all_469_9 & % 34.77/5.48 | hAPP_P1886180715on_val(all_469_8, all_469_4) = all_469_3 & red(p) = % 34.77/5.48 | all_469_2 & member773094996on_val(all_469_3, all_469_2) = all_469_1 & % 34.77/5.48 | hBOOL(all_469_1) = all_469_0 & some_val(v) = all_469_12 & % 34.77/5.48 | produc1102272487on_val(all_469_3) & produc12694297on_val(all_469_5) & % 34.77/5.48 | produc12694297on_val(all_469_10) & produc124828825on_val(all_469_4) & % 34.77/5.48 | produc124828825on_val(all_469_9) & fun_Pr691271849l_bool(all_469_2) & % 34.77/5.48 | fun_Pr231134077on_val(all_469_7) & fun_Pr231134077on_val(all_469_14) & % 34.77/5.48 | fun_Pr714818201on_val(all_469_8) & fun_fu1690035458on_val(all_469_6) & % 34.77/5.48 | fun_fu1690035458on_val(all_469_13) & % 34.77/5.48 | fun_li1432931796on_val(all_469_11) & option_val(all_469_12) & % 34.77/5.48 | bool(all_469_1) % 34.77/5.48 | % 34.77/5.48 | ALPHA: (39) implies: % 34.77/5.48 | (40) ~ (all_469_0 = 0) % 34.77/5.48 | (41) some_val(v) = all_469_12 % 34.77/5.48 | (42) hBOOL(all_469_1) = all_469_0 % 34.77/5.48 | (43) member773094996on_val(all_469_3, all_469_2) = all_469_1 % 34.77/5.48 | (44) red(p) = all_469_2 % 34.77/5.48 | (45) hAPP_P1886180715on_val(all_469_8, all_469_4) = all_469_3 % 34.77/5.48 | (46) hAPP_P604205461on_val(all_469_14, all_469_10) = all_469_9 % 34.77/5.48 | (47) hAPP_P604205461on_val(all_469_7, all_469_5) = all_469_4 % 34.77/5.48 | (48) hAPP_f1727192346on_val(all_469_13, all_469_11) = all_469_10 % 34.77/5.48 | (49) hAPP_f1727192346on_val(all_469_6, l_a) = all_469_5 % 34.77/5.48 | (50) hAPP_f1849790461on_val(produc899768717on_val, h_a) = all_469_6 % 34.77/5.48 | (51) hAPP_f1849790461on_val(produc899768717on_val, ha) = all_469_13 % 34.77/5.48 | (52) hAPP_e1659493427on_val(produc1259058957on_val, e_a) = all_469_7 % 34.77/5.49 | (53) hAPP_e1659493427on_val(produc1259058957on_val, ea) = all_469_14 % 34.77/5.49 | (54) hAPP_P1870962205on_val(produc1441475159on_val, all_469_9) = all_469_8 % 34.77/5.49 | (55) fun_up1149430426on_val(la, v_1, all_469_12) = all_469_11 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (5) with all_467_11, all_469_12, v, simplifying % 34.77/5.49 | with (24), (41) gives: % 34.77/5.49 | (56) all_469_12 = all_467_11 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (5) with all_464_2, all_469_12, v, simplifying with % 34.77/5.49 | (19), (41) gives: % 34.77/5.49 | (57) all_469_12 = all_464_2 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (7) with all_467_1, all_469_2, p, simplifying with % 34.77/5.49 | (27), (44) gives: % 34.77/5.49 | (58) all_469_2 = all_467_1 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (12) with all_467_5, all_469_6, h_a, % 34.77/5.49 | produc899768717on_val, simplifying with (33), (50) gives: % 34.77/5.49 | (59) all_469_6 = all_467_5 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (12) with all_464_3, all_467_12, ha, % 34.77/5.49 | produc899768717on_val, simplifying with (21), (34) gives: % 34.77/5.49 | (60) all_467_12 = all_464_3 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (12) with all_467_12, all_469_13, ha, % 34.77/5.49 | produc899768717on_val, simplifying with (34), (51) gives: % 34.77/5.49 | (61) all_469_13 = all_467_12 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (12) with all_430_2, all_469_13, ha, % 34.77/5.49 | produc899768717on_val, simplifying with (17), (51) gives: % 34.77/5.49 | (62) all_469_13 = all_430_2 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (13) with all_467_6, all_469_7, e_a, % 34.77/5.49 | produc1259058957on_val, simplifying with (35), (52) gives: % 34.77/5.49 | (63) all_469_7 = all_467_6 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (13) with all_467_13, all_469_14, ea, % 34.77/5.49 | produc1259058957on_val, simplifying with (36), (53) gives: % 34.77/5.49 | (64) all_469_14 = all_467_13 % 34.77/5.49 | % 34.77/5.49 | COMBINE_EQS: (56), (57) imply: % 34.77/5.49 | (65) all_467_11 = all_464_2 % 34.77/5.49 | % 34.77/5.49 | SIMP: (65) implies: % 34.77/5.49 | (66) all_467_11 = all_464_2 % 34.77/5.49 | % 34.77/5.49 | COMBINE_EQS: (61), (62) imply: % 34.77/5.49 | (67) all_467_12 = all_430_2 % 34.77/5.49 | % 34.77/5.49 | SIMP: (67) implies: % 34.77/5.49 | (68) all_467_12 = all_430_2 % 34.77/5.49 | % 34.77/5.49 | COMBINE_EQS: (60), (68) imply: % 34.77/5.49 | (69) all_464_3 = all_430_2 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (55), (57) imply: % 34.77/5.49 | (70) fun_up1149430426on_val(la, v_1, all_464_2) = all_469_11 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (38), (66) imply: % 34.77/5.49 | (71) fun_up1149430426on_val(la, v_1, all_464_2) = all_467_10 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (49), (59) imply: % 34.77/5.49 | (72) hAPP_f1727192346on_val(all_467_5, l_a) = all_469_5 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (48), (62) imply: % 34.77/5.49 | (73) hAPP_f1727192346on_val(all_430_2, all_469_11) = all_469_10 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (31), (68) imply: % 34.77/5.49 | (74) hAPP_f1727192346on_val(all_430_2, all_467_10) = all_467_9 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (20), (69) imply: % 34.77/5.49 | (75) hAPP_f1727192346on_val(all_430_2, all_464_1) = all_464_0 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (47), (63) imply: % 34.77/5.49 | (76) hAPP_P604205461on_val(all_467_6, all_469_5) = all_469_4 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (46), (64) imply: % 34.77/5.49 | (77) hAPP_P604205461on_val(all_467_13, all_469_10) = all_469_9 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (43), (58) imply: % 34.77/5.49 | (78) member773094996on_val(all_469_3, all_467_1) = all_469_1 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (11) with all_467_4, all_469_5, l_a, all_467_5, % 34.77/5.49 | simplifying with (32), (72) gives: % 34.77/5.49 | (79) all_469_5 = all_467_4 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (15) with all_464_1, all_469_11, all_464_2, v_1, % 34.77/5.49 | la, simplifying with (22), (70) gives: % 34.77/5.49 | (80) all_469_11 = all_464_1 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (15) with all_467_10, all_469_11, all_464_2, v_1, % 34.77/5.49 | la, simplifying with (70), (71) gives: % 34.77/5.49 | (81) all_469_11 = all_467_10 % 34.77/5.49 | % 34.77/5.49 | COMBINE_EQS: (80), (81) imply: % 34.77/5.49 | (82) all_467_10 = all_464_1 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (73), (80) imply: % 34.77/5.49 | (83) hAPP_f1727192346on_val(all_430_2, all_464_1) = all_469_10 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (74), (82) imply: % 34.77/5.49 | (84) hAPP_f1727192346on_val(all_430_2, all_464_1) = all_467_9 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (76), (79) imply: % 34.77/5.49 | (85) hAPP_P604205461on_val(all_467_6, all_467_4) = all_469_4 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (10) with all_467_3, all_469_4, all_467_4, % 34.77/5.49 | all_467_6, simplifying with (30), (85) gives: % 34.77/5.49 | (86) all_469_4 = all_467_3 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (11) with all_464_0, all_469_10, all_464_1, % 34.77/5.49 | all_430_2, simplifying with (75), (83) gives: % 34.77/5.49 | (87) all_469_10 = all_464_0 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (11) with all_467_9, all_469_10, all_464_1, % 34.77/5.49 | all_430_2, simplifying with (83), (84) gives: % 34.77/5.49 | (88) all_469_10 = all_467_9 % 34.77/5.49 | % 34.77/5.49 | COMBINE_EQS: (87), (88) imply: % 34.77/5.49 | (89) all_467_9 = all_464_0 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (77), (87) imply: % 34.77/5.49 | (90) hAPP_P604205461on_val(all_467_13, all_464_0) = all_469_9 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (29), (89) imply: % 34.77/5.49 | (91) hAPP_P604205461on_val(all_467_13, all_464_0) = all_467_8 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (45), (86) imply: % 34.77/5.49 | (92) hAPP_P1886180715on_val(all_469_8, all_467_3) = all_469_3 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (10) with all_467_8, all_469_9, all_464_0, % 34.77/5.49 | all_467_13, simplifying with (90), (91) gives: % 34.77/5.49 | (93) all_469_9 = all_467_8 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (54), (93) imply: % 34.77/5.49 | (94) hAPP_P1870962205on_val(produc1441475159on_val, all_467_8) = all_469_8 % 34.77/5.49 | % 34.77/5.49 | GROUND_INST: instantiating (14) with all_467_7, all_469_8, all_467_8, % 34.77/5.49 | produc1441475159on_val, simplifying with (37), (94) gives: % 34.77/5.49 | (95) all_469_8 = all_467_7 % 34.77/5.49 | % 34.77/5.49 | REDUCE: (92), (95) imply: % 34.77/5.50 | (96) hAPP_P1886180715on_val(all_467_7, all_467_3) = all_469_3 % 34.77/5.50 | % 34.77/5.50 | GROUND_INST: instantiating (9) with all_467_2, all_469_3, all_467_3, % 34.77/5.50 | all_467_7, simplifying with (28), (96) gives: % 34.77/5.50 | (97) all_469_3 = all_467_2 % 34.77/5.50 | % 34.77/5.50 | REDUCE: (78), (97) imply: % 34.77/5.50 | (98) member773094996on_val(all_467_2, all_467_1) = all_469_1 % 34.77/5.50 | % 34.77/5.50 | GROUND_INST: instantiating (8) with all_467_0, all_469_1, all_467_1, % 34.77/5.50 | all_467_2, simplifying with (26), (98) gives: % 34.77/5.50 | (99) all_469_1 = all_467_0 % 34.77/5.50 | % 34.77/5.50 | REDUCE: (42), (99) imply: % 34.77/5.50 | (100) hBOOL(all_467_0) = all_469_0 % 34.77/5.50 | % 34.77/5.50 | GROUND_INST: instantiating (6) with 0, all_469_0, all_467_0, simplifying with % 34.77/5.50 | (25), (100) gives: % 34.77/5.50 | (101) all_469_0 = 0 % 34.77/5.50 | % 34.77/5.50 | REDUCE: (40), (101) imply: % 34.77/5.50 | (102) $false % 34.77/5.50 | % 34.77/5.50 | CLOSE: (102) is inconsistent. % 34.77/5.50 | % 34.77/5.50 End of proof % 34.77/5.50 % SZS output end Proof for theBenchmark % 34.77/5.50 % 34.77/5.50 4881ms %------------------------------------------------------------------------------