%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP384_1 : TPTP v8.1.2. Released v8.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:11:57 EDT 2023 % Result : Theorem 66.25s 9.59s % Output : Proof 180.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : ITP384_1 : TPTP v8.1.2. Released v8.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n027.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 12:57:51 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.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 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 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 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 18.46/3.30 Prover 2: Preprocessing ... % 19.17/3.36 Prover 6: Preprocessing ... % 19.17/3.37 Prover 5: Preprocessing ... % 19.17/3.38 Prover 3: Preprocessing ... % 20.25/3.46 Prover 4: Preprocessing ... % 20.25/3.46 Prover 1: Preprocessing ... % 21.50/3.63 Prover 0: Preprocessing ... % 43.70/6.65 Prover 3: Warning: ignoring some quantifiers % 43.70/6.70 Prover 1: Warning: ignoring some quantifiers % 45.06/6.75 Prover 3: Constructing countermodel ... % 46.90/6.97 Prover 1: Constructing countermodel ... % 48.06/7.15 Prover 6: Proving ... % 51.47/7.66 Prover 4: Warning: ignoring some quantifiers % 55.77/8.16 Prover 4: Constructing countermodel ... % 59.15/8.69 Prover 5: Proving ... % 60.87/8.82 Prover 0: Proving ... % 66.25/9.58 Prover 3: proved (8950ms) % 66.25/9.58 % 66.25/9.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 66.25/9.59 % 66.25/9.59 Prover 6: stopped % 66.80/9.60 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 66.80/9.60 Prover 5: stopped % 66.80/9.60 Prover 0: stopped % 66.80/9.62 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 66.80/9.62 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 66.80/9.62 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 69.72/10.04 Prover 2: Proving ... % 69.72/10.04 Prover 2: stopped % 69.72/10.10 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 76.53/10.91 Prover 8: Preprocessing ... % 76.53/10.93 Prover 10: Preprocessing ... % 77.20/10.98 Prover 7: Preprocessing ... % 77.54/11.08 Prover 11: Preprocessing ... % 79.74/11.40 Prover 13: Preprocessing ... % 88.20/12.44 Prover 10: Warning: ignoring some quantifiers % 90.57/12.76 Prover 10: Constructing countermodel ... % 90.57/12.84 Prover 7: Warning: ignoring some quantifiers % 90.57/12.87 Prover 8: Warning: ignoring some quantifiers % 92.96/13.12 Prover 8: Constructing countermodel ... % 94.85/13.29 Prover 7: Constructing countermodel ... % 96.49/13.52 Prover 11: Warning: ignoring some quantifiers % 99.14/13.87 Prover 11: Constructing countermodel ... % 99.59/13.95 Prover 13: Warning: ignoring some quantifiers % 101.52/14.14 Prover 13: Constructing countermodel ... % 103.52/14.42 Prover 13: stopped % 103.52/14.43 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 111.13/15.45 Prover 16: Preprocessing ... % 126.36/17.47 Prover 16: Warning: ignoring some quantifiers % 127.36/17.64 Prover 16: Constructing countermodel ... % 140.97/19.59 Prover 16: stopped % 142.27/19.61 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 149.93/20.51 Prover 19: Preprocessing ... % 165.71/22.63 Prover 19: Warning: ignoring some quantifiers % 167.03/22.90 Prover 19: Constructing countermodel ... % 179.23/24.45 Prover 10: Found proof (size 105) % 179.23/24.45 Prover 10: proved (14830ms) % 179.23/24.45 Prover 19: stopped % 179.23/24.45 Prover 7: stopped % 179.23/24.45 Prover 1: stopped % 179.23/24.45 Prover 4: stopped % 179.23/24.45 Prover 8: stopped % 179.23/24.45 Prover 11: stopped % 179.23/24.45 % 179.23/24.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 179.23/24.46 % 179.23/24.46 % SZS output start Proof for theBenchmark % 180.08/24.48 Assumptions after simplification: % 180.08/24.48 --------------------------------- % 180.08/24.48 % 180.08/24.48 (axiom144) % 180.13/24.51 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$(comp$d) % 180.13/24.51 & % 180.13/24.51 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$(comp$b) % 180.13/24.51 & ! [v0: B_update_c_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.13/24.51 A_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : ! [v4: % 180.13/24.51 C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v5: % 180.13/24.51 C_update_b_update_fun$] : ! [v6: C_update_c_update_fun$] : ! [v7: % 180.13/24.51 C_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v8: % 180.13/24.51 C_update_c_update_fun$] : (v8 = v6 | ~ (comp$(v0, v5) = v6) | ~ % 180.13/24.51 (fun_app$y(comp$b, v1) = v4) | ~ (fun_app$x(v4, v3) = v5) | ~ % 180.13/24.51 (fun_app$af(comp$d, v2) = v7) | ~ (fun_app$ae(v7, v3) = v8) | ~ % 180.13/24.51 C_update_a_update_fun$(v3) | ~ A_update_c_update_fun$(v2) | ~ % 180.13/24.51 B_update_c_update_fun$(v0) | ~ A_update_b_update_fun$(v1) | ? [v9: % 180.13/24.51 A_update_c_update_fun$] : ( ~ (v9 = v2) & comp$aj(v0, v1) = v9 & % 180.13/24.51 A_update_c_update_fun$(v9))) % 180.13/24.51 % 180.13/24.51 (axiom187) % 180.23/24.51 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$(comp$d) % 180.23/24.51 & % 180.23/24.51 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$(comp$b) % 180.23/24.51 & ! [v0: B_update_c_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.23/24.51 C_update_a_update_fun$] : ! [v3: % 180.23/24.51 C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v4: % 180.23/24.51 C_update_b_update_fun$] : ! [v5: C_update_c_update_fun$] : ( ~ (comp$(v0, % 180.23/24.51 v4) = v5) | ~ (fun_app$y(comp$b, v1) = v3) | ~ (fun_app$x(v3, v2) = % 180.23/24.51 v4) | ~ C_update_a_update_fun$(v2) | ~ B_update_c_update_fun$(v0) | ~ % 180.23/24.51 A_update_b_update_fun$(v1) | ? [v6: A_update_c_update_fun$] : ? [v7: % 180.23/24.51 C_update_a_update_fun_c_update_c_update_fun_fun$] : (comp$aj(v0, v1) = v6 % 180.23/24.51 & fun_app$af(comp$d, v6) = v7 & fun_app$ae(v7, v2) = v5 & % 180.23/24.51 C_update_a_update_fun_c_update_c_update_fun_fun$(v7) & % 180.23/24.51 C_update_c_update_fun$(v5) & A_update_c_update_fun$(v6))) % 180.23/24.51 % 180.23/24.51 (axiom231) % 180.23/24.51 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$(comp$a) % 180.23/24.51 & ! [v0: B_update_a_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.23/24.51 B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.23/24.51 B_update_c_update_fun$] : ( ~ (fun_app$w(comp$a, v1) = v2) | ~ % 180.23/24.51 (fun_app$v(v2, v0) = v3) | ~ A_update_c_update_fun$(v1) | ~ % 180.23/24.51 B_update_a_update_fun$(v0) | (fcomp$b(v0, v1) = v3 & % 180.23/24.51 B_update_c_update_fun$(v3))) % 180.23/24.51 % 180.23/24.51 (axiom42) % 180.23/24.51 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$(comp$d) % 180.23/24.51 & C_update_c_update_fun$(id$) & C_update_a_update_fun$(g$a) & % 180.23/24.51 A_update_c_update_fun$(g$) & ? [v0: % 180.23/24.51 C_update_a_update_fun_c_update_c_update_fun_fun$] : (fun_app$af(comp$d, g$) % 180.23/24.51 = v0 & fun_app$ae(v0, g$a) = id$ & % 180.23/24.51 C_update_a_update_fun_c_update_c_update_fun_fun$(v0)) % 180.23/24.51 % 180.23/24.51 (axiom452) % 180.23/24.52 C_update_set$(top$a) & % 180.23/24.52 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$(comp$d) % 180.23/24.52 & C_update_c_update_fun$(id$) & A_update_a_update_fun$(id$b) & ! [v0: % 180.23/24.52 C_update_a_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.23/24.52 C_update_a_update_fun_c_update_c_update_fun_fun$] : ( ~ (fun_app$af(comp$d, % 180.23/24.52 v1) = v2) | ~ (fun_app$ae(v2, v0) = id$) | ~ % 180.23/24.52 C_update_a_update_fun$(v0) | ~ A_update_c_update_fun$(v1) | ? [v3: % 180.23/24.52 A_update_a_update_fun$] : ? [v4: A_update_c_update_fun$] : ((v4 = v1 & % 180.23/24.52 inv_into$a(top$a, v0) = v1) | ( ~ (v3 = id$b) & comp$k(v0, v1) = v3 & % 180.23/24.52 A_update_a_update_fun$(v3)))) % 180.23/24.52 % 180.23/24.52 (axiom455) % 180.23/24.52 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$(comp$c) % 180.23/24.52 & B_update_b_update_fun$(id$a) & % 180.27/24.52 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$(comp$e) % 180.27/24.52 & A_update_a_update_fun$(id$b) & A_update_set$(top$) & ! [v0: % 180.27/24.52 A_update_b_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.27/24.52 B_update_a_update_fun_b_update_b_update_fun_fun$] : ( ~ (fun_app$ak(comp$e, % 180.27/24.52 v0) = v2) | ~ (fun_app$aj(v2, v1) = id$a) | ~ % 180.27/24.52 A_update_b_update_fun$(v0) | ~ B_update_a_update_fun$(v1) | ? [v3: % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v4: % 180.27/24.52 A_update_a_update_fun$] : ? [v5: B_update_a_update_fun$] : ((v5 = v1 & % 180.27/24.52 inv_into$b(top$, v0) = v1) | ( ~ (v4 = id$b) & fun_app$ad(comp$c, v1) = % 180.27/24.52 v3 & fun_app$ac(v3, v0) = v4 & A_update_a_update_fun$(v4) & % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$(v3)))) % 180.27/24.52 % 180.27/24.52 (axiom479) % 180.27/24.52 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$(comp$a) % 180.27/24.52 & A_update_set$(top$) & ! [v0: A_update_b_update_fun$] : ! [v1: % 180.27/24.52 A_update_c_update_fun$] : ! [v2: % 180.27/24.52 B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.27/24.52 B_update_a_update_fun$] : ! [v4: B_update_c_update_fun$] : ! [v5: % 180.27/24.52 A_update_c_update_fun$] : (v5 = v1 | ~ (inv_into$b(top$, v0) = v3) | ~ % 180.27/24.52 (comp$aj(v4, v0) = v5) | ~ (fun_app$w(comp$a, v1) = v2) | ~ (fun_app$v(v2, % 180.27/24.52 v3) = v4) | ~ A_update_c_update_fun$(v1) | ~ % 180.27/24.52 A_update_b_update_fun$(v0) | ~ inj_on$(v0, top$)) % 180.27/24.52 % 180.27/24.52 (axiom575) % 180.27/24.52 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$(comp$c) % 180.27/24.52 & A_update_a_update_fun$(id$b) & A_update_set$(top$) & ! [v0: % 180.27/24.52 A_update_b_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.27/24.52 A_update_a_update_fun$] : (v3 = id$b | ~ (inv_into$b(top$, v0) = v1) | ~ % 180.27/24.52 (fun_app$ad(comp$c, v1) = v2) | ~ (fun_app$ac(v2, v0) = v3) | ~ % 180.27/24.52 A_update_b_update_fun$(v0) | ~ inj_on$(v0, top$)) & ! [v0: % 180.27/24.52 A_update_b_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$] : ( ~ (inv_into$b(top$, % 180.27/24.52 v0) = v1) | ~ (fun_app$ad(comp$c, v1) = v2) | ~ (fun_app$ac(v2, v0) = % 180.27/24.52 id$b) | ~ A_update_b_update_fun$(v0) | inj_on$(v0, top$)) % 180.27/24.52 % 180.27/24.52 (axiom66) % 180.27/24.52 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$(comp$d) % 180.27/24.52 & C_update_c_update_fun$(id$) & % 180.27/24.52 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$(comp$c) % 180.27/24.52 & C_update_a_update_fun$(g$a) & B_update_b_update_fun$(id$a) & % 180.27/24.52 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$(comp$e) % 180.27/24.52 & A_update_b_update_fun$(f$a) & A_update_a_update_fun$(id$b) & ? [v0: % 180.27/24.52 B_update_a_update_fun_b_update_b_update_fun_fun$] : ? [v1: % 180.27/24.52 B_update_a_update_fun$] : ? [v2: A_update_c_update_fun$] : ? [v3: % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v4: % 180.27/24.52 C_update_a_update_fun_c_update_c_update_fun_fun$] : (comp$k(g$a, v2) = id$b % 180.27/24.52 & fun_app$ak(comp$e, f$a) = v0 & fun_app$aj(v0, v1) = id$a & % 180.27/24.52 fun_app$af(comp$d, v2) = v4 & fun_app$ae(v4, g$a) = id$ & fun_app$ad(comp$c, % 180.27/24.52 v1) = v3 & fun_app$ac(v3, f$a) = id$b & % 180.27/24.52 C_update_a_update_fun_c_update_c_update_fun_fun$(v4) & % 180.27/24.52 B_update_a_update_fun_b_update_b_update_fun_fun$(v0) & % 180.27/24.52 A_update_c_update_fun$(v2) & B_update_a_update_fun$(v1) & % 180.27/24.52 A_update_b_update_fun_a_update_a_update_fun_fun$(v3) & register$a(v1) & % 180.27/24.52 register$(v2)) % 180.27/24.52 % 180.27/24.52 (axiom67) % 180.27/24.53 B_update_b_update_fun$(id$a) & % 180.27/24.53 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$(comp$e) % 180.27/24.53 & A_update_b_update_fun$(f$a) & B_update_a_update_fun$(f$) & ? [v0: % 180.27/24.53 B_update_a_update_fun_b_update_b_update_fun_fun$] : (fun_app$ak(comp$e, f$a) % 180.27/24.53 = v0 & fun_app$aj(v0, f$) = id$a & % 180.27/24.53 B_update_a_update_fun_b_update_b_update_fun_fun$(v0)) % 180.27/24.53 % 180.27/24.53 (axiom68) % 180.27/24.53 comp$k(g$a, g$) = id$b & C_update_a_update_fun$(g$a) & % 180.27/24.53 A_update_c_update_fun$(g$) & A_update_a_update_fun$(id$b) % 180.27/24.53 % 180.27/24.53 (axiom69) % 180.27/24.53 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$(comp$c) % 180.27/24.53 & A_update_b_update_fun$(f$a) & A_update_a_update_fun$(id$b) & % 180.27/24.53 B_update_a_update_fun$(f$) & ? [v0: % 180.27/24.53 A_update_b_update_fun_a_update_a_update_fun_fun$] : (fun_app$ad(comp$c, f$) % 180.27/24.53 = v0 & fun_app$ac(v0, f$a) = id$b & % 180.27/24.53 A_update_b_update_fun_a_update_a_update_fun_fun$(v0)) % 180.27/24.53 % 180.27/24.53 (conjecture29) % 180.27/24.53 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$(comp$b) % 180.27/24.53 & C_update_c_update_fun$(id$) & C_update_a_update_fun$(g$a) & % 180.27/24.53 A_update_c_update_fun$(g$) & % 180.27/24.53 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$(comp$a) % 180.27/24.53 & A_update_b_update_fun$(f$a) & B_update_a_update_fun$(f$) & ? [v0: % 180.27/24.53 B_update_a_update_fun_b_update_c_update_fun_fun$] : ? [v1: % 180.27/24.53 B_update_c_update_fun$] : ? [v2: % 180.27/24.53 C_update_a_update_fun_c_update_b_update_fun_fun$] : ? [v3: % 180.27/24.53 C_update_b_update_fun$] : ? [v4: C_update_c_update_fun$] : ( ~ (v4 = id$) & % 180.27/24.53 comp$(v1, v3) = v4 & fun_app$y(comp$b, f$a) = v2 & fun_app$x(v2, g$a) = v3 & % 180.27/24.53 fun_app$w(comp$a, g$) = v0 & fun_app$v(v0, f$) = v1 & % 180.27/24.53 B_update_a_update_fun_b_update_c_update_fun_fun$(v0) & % 180.27/24.53 C_update_c_update_fun$(v4) & C_update_b_update_fun$(v3) & % 180.27/24.53 B_update_c_update_fun$(v1) & % 180.27/24.53 C_update_a_update_fun_c_update_b_update_fun_fun$(v2)) % 180.27/24.53 % 180.27/24.53 (function-axioms) % 180.68/24.61 ! [v0: A_update_a_update_bool_fun_fun$] : ! [v1: % 180.68/24.61 A_update_a_update_bool_fun_fun$] : ! [v2: A_update_a_update_fun$] : ! [v3: % 180.68/24.61 A_update$] : ! [v4: A_update_a_update_fun$] : ! [v5: % 180.68/24.61 A_update_a_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$b(v5, v4, v3, v2) = v1) | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$b(v5, v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 B_update_b_update_bool_fun_fun$] : ! [v1: B_update_b_update_bool_fun_fun$] % 180.68/24.61 : ! [v2: B_update_b_update_fun$] : ! [v3: B_update$] : ! [v4: % 180.68/24.61 B_update_b_update_fun$] : ! [v5: % 180.68/24.61 B_update_b_update_fun_b_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$a(v5, v4, v3, v2) = v1) | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$a(v5, v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 C_update_c_update_bool_fun_fun$] : ! [v1: C_update_c_update_bool_fun_fun$] % 180.68/24.61 : ! [v2: C_update_c_update_fun$] : ! [v3: C_update$] : ! [v4: % 180.68/24.61 C_update_c_update_fun$] : ! [v5: % 180.68/24.61 C_update_c_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$(v5, v4, v3, v2) = v1) | ~ % 180.68/24.61 (iso_tuple_update_accessor_eq_assist$(v5, v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: A_update_b_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$at(v4, v3, v2) = v1) | ~ (map_fun$at(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: A_update_b_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$ar(v4, v3, v2) = v1) | ~ (map_fun$ar(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: A_update_c_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$an(v4, v3, v2) = v1) | ~ (map_fun$an(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: A_update_c_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$al(v4, v3, v2) = v1) | ~ (map_fun$al(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: B_update_a_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$aj(v4, v3, v2) = v1) | ~ (map_fun$aj(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.61 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v1: % 180.68/24.61 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v2: % 180.68/24.61 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.61 : ! [v3: % 180.68/24.61 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.61 : ! [v4: A_update_b_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.61 (map_fun$ah(v4, v3, v2) = v1) | ~ (map_fun$ah(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v4: A_update_b_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$af(v4, v3, v2) = v1) | ~ (map_fun$af(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v4: A_update_c_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ac(v4, v3, v2) = v1) | ~ (map_fun$ac(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v4: A_update_c_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$aa(v4, v3, v2) = v1) | ~ (map_fun$aa(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v4: B_update_a_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$y(v4, v3, v2) = v1) | ~ (map_fun$y(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update$] : ! [v3: A_update_b_update_fun$] : ! [v4: A_update_set$] : (v1 % 180.68/24.62 = v0 | ~ (uut$(v4, v3, v2) = v1) | ~ (uut$(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 B_update$] : ! [v3: B_update_a_update_fun$] : ! [v4: B_update_set$] : (v1 % 180.68/24.62 = v0 | ~ (uuv$(v4, v3, v2) = v1) | ~ (uuv$(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.62 C_update$] : ! [v3: C_update_a_update_fun$] : ! [v4: C_update_set$] : (v1 % 180.68/24.62 = v0 | ~ (uuu$(v4, v3, v2) = v1) | ~ (uuu$(v4, v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_bool_fun$] : ! [v1: A_update_a_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$cf(v3, v2) = v1) | ~ (fun_app$cf(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_bool_fun$] : ! [v1: B_update_b_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$ce(v3, v2) = v1) | ~ (fun_app$ce(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_bool_fun$] : ! [v1: C_update_c_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$cd(v3, v2) = v1) | ~ (fun_app$cd(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_bool_fun$] : ! [v1: B_update_b_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_fun$] : ! [v3: % 180.68/24.62 B_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$cc(v3, v2) = v1) | ~ (fun_app$cc(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_bool_fun$] : ! [v1: A_update_a_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$cb(v3, v2) = v1) | ~ (fun_app$cb(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_bool_fun$] : ! [v1: B_update_b_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bz(v3, v2) = v1) | ~ (fun_app$bz(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_bool_fun$] : ! [v1: C_update_c_update_fun_bool_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bx(v3, v2) = v1) | ~ (fun_app$bx(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v3: B_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bw(v3, v2) = v1) | ~ (rel_fun$bw(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bv(v3, v2) = v1) | ~ (rel_fun$bv(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v3: C_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bt(v3, v2) = v1) | ~ (rel_fun$bt(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bs(v3, v2) = v1) | ~ (rel_fun$bs(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v3: B_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bp(v3, v2) = v1) | ~ (rel_fun$bp(v3, v2) = v0)) & ! % 180.68/24.62 [v0: B_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: B_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bq(v3, v2) = v1) | ~ (rel_fun$bq(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bo(v3, v2) = v1) | ~ (rel_fun$bo(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bm(v3, v2) = v1) | ~ (rel_fun$bm(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bl(v3, v2) = v1) | ~ (rel_fun$bl(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_b_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bj(v3, v2) = v1) | ~ (rel_fun$bj(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bi(v3, v2) = v1) | ~ (rel_fun$bi(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bg(v3, v2) = v1) | ~ (rel_fun$bg(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bf(v3, v2) = v1) | ~ (rel_fun$bf(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bd(v3, v2) = v1) | ~ (rel_fun$bd(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_b_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$bc(v3, v2) = v1) | ~ (rel_fun$bc(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$bb(v3, v2) = v1) | ~ (rel_fun$bb(v3, v2) = v0)) & ! % 180.68/24.62 [v0: B_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$az(v3, v2) = v1) | ~ (rel_fun$az(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$ay(v3, v2) = v1) | ~ (rel_fun$ay(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$aw(v3, v2) = v1) | ~ (rel_fun$aw(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$av(v3, v2) = v1) | ~ (rel_fun$av(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_bool_fun_fun$] : ! [v3: C_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$at(v3, v2) = v1) | ~ (rel_fun$at(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$as(v3, v2) = v1) | ~ (rel_fun$as(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$aq(v3, v2) = v1) | ~ (rel_fun$aq(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$ap(v3, v2) = v1) | ~ (rel_fun$ap(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$ao(v3, v2) = v1) | ~ (rel_fun$ao(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v3: C_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$al(v3, v2) = v1) | ~ (rel_fun$al(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: C_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$am(v3, v2) = v1) | ~ (rel_fun$am(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$ak(v3, v2) = v1) | ~ (rel_fun$ak(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$ah(v3, v2) = v1) | ~ (rel_fun$ah(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$ai(v3, v2) = v1) | ~ (rel_fun$ai(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$ag(v3, v2) = v1) | ~ (rel_fun$ag(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$af(v3, v2) = v1) | ~ (rel_fun$af(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: C_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$ac(v3, v2) = v1) | ~ (rel_fun$ac(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_bool_fun_fun$] : ! [v3: C_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$ad(v3, v2) = v1) | ~ (rel_fun$ad(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$ab(v3, v2) = v1) | ~ (rel_fun$ab(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_bool_fun_fun$] : ! [v3: A_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$aa(v3, v2) = v1) | ~ (rel_fun$aa(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: A_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$y(v3, v2) = v1) | ~ (rel_fun$y(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$x(v3, v2) = v1) | ~ (rel_fun$x(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: A_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$v(v3, v2) = v1) | ~ (rel_fun$v(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$u(v3, v2) = v1) | ~ (rel_fun$u(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: B_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$t(v3, v2) = v1) | ~ (rel_fun$t(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_bool_fun_fun$] : ! [v3: A_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$q(v3, v2) = v1) | ~ (rel_fun$q(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v3: A_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$r(v3, v2) = v1) | ~ (rel_fun$r(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$p(v3, v2) = v1) | ~ (rel_fun$p(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_bool_fun_fun$] : ! [v3: A_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$m(v3, v2) = v1) | ~ (rel_fun$m(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v3: A_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$n(v3, v2) = v1) | ~ (rel_fun$n(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$l(v3, v2) = v1) | ~ (rel_fun$l(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_a_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v3: B_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$k(v3, v2) = v1) | ~ (rel_fun$k(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$h(v3, v2) = v1) | ~ (rel_fun$h(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$i(v3, v2) = v1) | ~ (rel_fun$i(v3, v2) = v0)) & ! % 180.68/24.62 [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (rel_fun$g(v3, v2) = v1) | ~ (rel_fun$g(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$f(v3, v2) = v1) | ~ (rel_fun$f(v3, v2) = v0)) & ! % 180.68/24.62 [v0: B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_set$] : (v1 = v0 | ~ (grp$j(v3, v2) = v1) | ~ % 180.68/24.62 (grp$j(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$d(v3, v2) = v1) | ~ (rel_fun$d(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_set$] : (v1 = v0 | ~ (grp$i(v3, v2) = v1) | ~ % 180.68/24.62 (grp$i(v3, v2) = v0)) & ! [v0: A_update_b_update_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.62 A_update_set$] : (v1 = v0 | ~ (grp$h(v3, v2) = v1) | ~ (grp$h(v3, v2) = % 180.68/24.62 v0)) & ! [v0: C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$c(v3, v2) = v1) | ~ (rel_fun$c(v3, v2) = v0)) & ! % 180.68/24.62 [v0: B_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_set$] : (v1 = v0 | ~ (grp$g(v3, v2) = v1) | ~ % 180.68/24.62 (grp$g(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v3: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$b(v3, v2) = v1) | ~ (rel_fun$b(v3, v2) = v0)) & ! % 180.68/24.62 [v0: C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_set$] : (v1 = v0 | ~ (grp$f(v3, v2) = v1) | ~ % 180.68/24.62 (grp$f(v3, v2) = v0)) & ! [v0: A_update_c_update_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.62 A_update_set$] : (v1 = v0 | ~ (grp$e(v3, v2) = v1) | ~ (grp$e(v3, v2) = % 180.68/24.62 v0)) & ! [v0: C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$a(v3, v2) = v1) | ~ (rel_fun$a(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_b_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_set$] : (v1 = v0 | ~ (grp$d(v3, v2) = v1) | ~ % 180.68/24.62 (grp$d(v3, v2) = v0)) & ! [v0: B_update_a_update_bool_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_bool_fun_fun$] : ! [v2: B_update_a_update_fun$] : ! [v3: % 180.68/24.62 B_update_set$] : (v1 = v0 | ~ (grp$c(v3, v2) = v1) | ~ (grp$c(v3, v2) = % 180.68/24.62 v0)) & ! [v0: A_update_b_update_fun_a_update_a_update_fun_bool_fun_fun$] % 180.68/24.62 : ! [v1: A_update_b_update_fun_a_update_a_update_fun_bool_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_bool_fun_fun$] : ! [v3: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (rel_fun$(v3, v2) = v1) | ~ (rel_fun$(v3, v2) = v0)) & ! % 180.68/24.62 [v0: B_update_c_update_fun$] : ! [v1: B_update_c_update_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: C_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (the_inv_into$g(v3, v2) = v1) | ~ (the_inv_into$g(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_fun$] : ! [v3: B_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (the_inv_into$f(v3, v2) = v1) | ~ (the_inv_into$f(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: A_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (the_inv_into$e(v3, v2) = v1) | ~ (the_inv_into$e(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update$] : ! [v1: A_update$] : ! [v2: A_update_set$] : ! [v3: % 180.68/24.62 A_update_set_a_update_fun$] : (v1 = v0 | ~ (fun_app$bv(v3, v2) = v1) | ~ % 180.68/24.62 (fun_app$bv(v3, v2) = v0)) & ! [v0: B_update$] : ! [v1: B_update$] : ! % 180.68/24.62 [v2: B_update_set$] : ! [v3: B_update_set_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bu(v3, v2) = v1) | ~ (fun_app$bu(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update$] : ! [v1: C_update$] : ! [v2: C_update_set$] : ! [v3: % 180.68/24.62 C_update_set_c_update_fun$] : (v1 = v0 | ~ (fun_app$bt(v3, v2) = v1) | ~ % 180.68/24.62 (fun_app$bt(v3, v2) = v0)) & ! [v0: B_update_set$] : ! [v1: B_update_set$] % 180.68/24.62 : ! [v2: B_update_set$] : ! [v3: B_update_set_b_update_set_fun$] : (v1 = v0 % 180.68/24.62 | ~ (fun_app$bs(v3, v2) = v1) | ~ (fun_app$bs(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_set$] : ! [v1: B_update_set$] : ! [v2: C_update_set$] : ! [v3: % 180.68/24.62 C_update_b_update_fun$] : (v1 = v0 | ~ (image$h(v3, v2) = v1) | ~ % 180.68/24.62 (image$h(v3, v2) = v0)) & ! [v0: C_update_set$] : ! [v1: C_update_set$] : % 180.68/24.62 ! [v2: B_update_set$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (image$g(v3, v2) = v1) | ~ (image$g(v3, v2) = v0)) & ! [v0: C_update_set$] % 180.68/24.62 : ! [v1: C_update_set$] : ! [v2: C_update_set$] : ! [v3: % 180.68/24.62 C_update_set_c_update_set_fun$] : (v1 = v0 | ~ (fun_app$br(v3, v2) = v1) | % 180.68/24.62 ~ (fun_app$br(v3, v2) = v0)) & ! [v0: A_update_set$] : ! [v1: % 180.68/24.62 A_update_set$] : ! [v2: A_update_set$] : ! [v3: % 180.68/24.62 A_update_set_a_update_set_fun$] : (v1 = v0 | ~ (fun_app$bq(v3, v2) = v1) | % 180.68/24.62 ~ (fun_app$bq(v3, v2) = v0)) & ! [v0: C_update_set$] : ! [v1: % 180.68/24.62 C_update_set$] : ! [v2: A_update_set$] : ! [v3: A_update_c_update_fun$] : % 180.68/24.62 (v1 = v0 | ~ (image$c(v3, v2) = v1) | ~ (image$c(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v1: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun$] : ! [v3: A_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (grp$b(v3, v2) = v1) | ~ (grp$b(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v1: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_fun$] : ! [v3: B_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (grp$a(v3, v2) = v1) | ~ (grp$a(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v1: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun$] : ! [v3: C_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (grp$(v3, v2) = v1) | ~ (grp$(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_c_update_fun$] : ! [v1: B_update_c_update_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: C_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$h(v3, v2) = v1) | ~ (inv_into$h(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_fun$] : ! [v3: B_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$g(v3, v2) = v1) | ~ (inv_into$g(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: A_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$c(v3, v2) = v1) | ~ (inv_into$c(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: A_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$b(v3, v2) = v1) | ~ (inv_into$b(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun$] : ! [v3: C_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$a(v3, v2) = v1) | ~ (inv_into$a(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: B_update_set$] : (v1 = v0 | ~ % 180.68/24.62 (inv_into$(v3, v2) = v1) | ~ (inv_into$(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : ! [v1: B_update_b_update_bool_fun_fun$] % 180.68/24.62 : ! [v2: B_update_b_update_bool_fun_fun$] : ! [v3: % 180.68/24.62 B_update_b_update_bool_fun_fun$] : (v1 = v0 | ~ (relcompp$b(v3, v2) = v1) | % 180.68/24.62 ~ (relcompp$b(v3, v2) = v0)) & ! [v0: C_update_c_update_bool_fun_fun$] : % 180.68/24.62 ! [v1: C_update_c_update_bool_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_bool_fun_fun$] : ! [v3: C_update_c_update_bool_fun_fun$] % 180.68/24.62 : (v1 = v0 | ~ (relcompp$a(v3, v2) = v1) | ~ (relcompp$a(v3, v2) = v0)) & ! % 180.68/24.62 [v0: A_update_a_update_bool_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_bool_fun_fun$] : ! [v2: A_update_a_update_bool_fun_fun$] % 180.68/24.62 : ! [v3: A_update_a_update_bool_fun_fun$] : (v1 = v0 | ~ (relcompp$(v3, v2) % 180.68/24.62 = v1) | ~ (relcompp$(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$aw(v3, v2) = v1) | ~ (map_fun$aw(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$av(v3, v2) = v1) | ~ (map_fun$av(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_b_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$au(v3, v2) = v1) | ~ (map_fun$au(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_c_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$as(v3, v2) = v1) | ~ (map_fun$as(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ap(v3, v2) = v1) | ~ (map_fun$ap(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_b_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_b_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$aq(v3, v2) = v1) | ~ (map_fun$aq(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ao(v3, v2) = v1) | ~ (map_fun$ao(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$am(v3, v2) = v1) | ~ (map_fun$am(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: C_update_c_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ak(v3, v2) = v1) | ~ (map_fun$ak(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ai(v3, v2) = v1) | ~ (map_fun$ai(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ag(v3, v2) = v1) | ~ (map_fun$ag(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ae(v3, v2) = v1) | ~ (map_fun$ae(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ad(v3, v2) = v1) | ~ (map_fun$ad(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$ab(v3, v2) = v1) | ~ (map_fun$ab(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.62 : ! [v2: A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$z(v3, v2) = v1) | ~ (map_fun$z(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_bool_fun$] : ! [v1: A_update_bool_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: B_update_bool_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bp(v3, v2) = v1) | ~ (comp$bp(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_bool_fun$] : ! [v1: A_update_bool_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: C_update_bool_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bo(v3, v2) = v1) | ~ (comp$bo(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_bool_fun$] : ! [v1: B_update_bool_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: A_update_bool_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bn(v3, v2) = v1) | ~ (comp$bn(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_b_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$x(v3, v2) = v1) | ~ (map_fun$x(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$w(v3, v2) = v1) | ~ (map_fun$w(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_c_update_fun_b_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_c_update_fun_b_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$v(v3, v2) = v1) | ~ (map_fun$v(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_fun$] : ! [v3: % 180.68/24.62 B_update_b_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bp(v3, v2) = v1) | ~ (fun_app$bp(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun$] : ! [v1: B_update_b_update_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_b_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bo(v3, v2) = v1) | ~ (fun_app$bo(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bn(v3, v2) = v1) | ~ (fun_app$bn(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bm(v3, v2) = v1) | ~ (fun_app$bm(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bl(v3, v2) = v1) | ~ (fun_app$bl(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bk(v3, v2) = v1) | ~ (fun_app$bk(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: % 180.68/24.62 C_update_b_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bj(v3, v2) = v1) | ~ (fun_app$bj(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bi(v3, v2) = v1) | ~ (fun_app$bi(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bh(v3, v2) = v1) | ~ (fun_app$bh(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bg(v3, v2) = v1) | ~ (fun_app$bg(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun$] : ! [v3: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bf(v3, v2) = v1) | ~ (fun_app$bf(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$be(v3, v2) = v1) | ~ (fun_app$be(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bd(v3, v2) = v1) | ~ (fun_app$bd(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bc(v3, v2) = v1) | ~ (fun_app$bc(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$bb(v3, v2) = v1) | ~ (fun_app$bb(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$ba(v3, v2) = v1) | ~ (fun_app$ba(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$az(v3, v2) = v1) | ~ (fun_app$az(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: % 180.68/24.62 A_update_c_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$ay(v3, v2) = v1) | ~ (fun_app$ay(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$ax(v3, v2) = v1) | ~ (fun_app$ax(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$aw(v3, v2) = v1) | ~ (fun_app$aw(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_b_update_fun$] : ! [v1: B_update_b_update_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_b_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$av(v3, v2) = v1) | ~ (fun_app$av(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_fun$] : ! [v3: % 180.68/24.62 B_update_b_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (fun_app$au(v3, v2) = v1) | ~ (fun_app$au(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$u(v3, v2) = v1) | ~ (map_fun$u(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bm(v3, v2) = v1) | ~ (comp$bm(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$t(v3, v2) = v1) | ~ (map_fun$t(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$s(v3, v2) = v1) | ~ (map_fun$s(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bl(v3, v2) = v1) | ~ (comp$bl(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$r(v3, v2) = v1) | ~ (map_fun$r(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$q(v3, v2) = v1) | ~ (map_fun$q(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_b_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bk(v3, v2) = v1) | ~ (comp$bk(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$p(v3, v2) = v1) | ~ (map_fun$p(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$n(v3, v2) = v1) | ~ (map_fun$n(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$o(v3, v2) = v1) | ~ (map_fun$o(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_c_update_fun_a_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_a_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bj(v3, v2) = v1) | ~ (comp$bj(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_a_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$m(v3, v2) = v1) | ~ (map_fun$m(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$k(v3, v2) = v1) | ~ (map_fun$k(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$l(v3, v2) = v1) | ~ (map_fun$l(v3, v2) = v0)) & ! [v0: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 C_update_a_update_fun_c_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_a_update_fun_a_update_b_update_fun_fun$] : ! [v3: % 180.68/24.62 A_update_b_update_fun_c_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bi(v3, v2) = v1) | ~ (comp$bi(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_b_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$j(v3, v2) = v1) | ~ (map_fun$j(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bh(v3, v2) = v1) | ~ (comp$bh(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 C_update_b_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$i(v3, v2) = v1) | ~ (map_fun$i(v3, v2) = v0)) & ! [v0: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_b_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$h(v3, v2) = v1) | ~ (map_fun$h(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_c_update_fun_a_update_b_update_fun_fun$] : ! [v2: % 180.68/24.62 A_update_c_update_fun_b_update_a_update_fun_fun$] : ! [v3: % 180.68/24.62 B_update_a_update_fun_a_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.62 (comp$bg(v3, v2) = v1) | ~ (comp$bg(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_c_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$g(v3, v2) = v1) | ~ (map_fun$g(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_fun$] : ! [v1: % 180.68/24.62 A_update_b_update_fun_b_update_a_update_fun_fun$] : ! [v2: % 180.68/24.62 B_update_a_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.62 (map_fun$f(v3, v2) = v1) | ~ (map_fun$f(v3, v2) = v0)) & ! [v0: % 180.68/24.62 A_update_b_update_fun_a_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_b_update_fun_a_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun_b_update_a_update_fun_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$bf(v3, v2) = v1) | ~ (comp$bf(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun_a_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_c_update_fun_a_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$e(v3, v2) = v1) | ~ (map_fun$e(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun_a_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_a_update_fun_a_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$c(v3, v2) = v1) | ~ (map_fun$c(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun_b_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_c_update_fun_b_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 C_update_a_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$d(v3, v2) = v1) | ~ (map_fun$d(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun_a_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_c_update_fun_a_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun_b_update_a_update_fun_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_a_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$be(v3, v2) = v1) | ~ (comp$be(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$b(v3, v2) = v1) | ~ (map_fun$b(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$(v3, v2) = v1) | ~ (map_fun$(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (map_fun$a(v3, v2) = v1) | ~ (map_fun$a(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v3: % 180.68/24.63 B_update_b_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$bd(v3, v2) = v1) | ~ (comp$bd(v3, v2) = v0)) & ! [v0: A_update$] : % 180.68/24.63 ! [v1: A_update$] : ! [v2: B_b_prod_update$] : ! [v3: % 180.68/24.63 B_b_prod_update_a_update_fun$] : (v1 = v0 | ~ (fun_app$at(v3, v2) = v1) | % 180.68/24.63 ~ (fun_app$at(v3, v2) = v0)) & ! [v0: C_update$] : ! [v1: C_update$] : ! % 180.68/24.63 [v2: A_a_prod_update$] : ! [v3: A_a_prod_update_c_update_fun$] : (v1 = v0 | % 180.68/24.63 ~ (fun_app$as(v3, v2) = v1) | ~ (fun_app$as(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_a_prod_update_a_update_fun$] : ! [v1: A_a_prod_update_a_update_fun$] : ! % 180.68/24.63 [v2: A_a_prod_update_b_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = % 180.68/24.63 v0 | ~ (comp$bc(v3, v2) = v1) | ~ (comp$bc(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_b_prod_update_c_update_fun$] : ! [v1: B_b_prod_update_c_update_fun$] : ! % 180.68/24.63 [v2: B_update_c_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$t(v3, v2) = v1) | ~ (register_pair$t(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_b_prod_update_c_update_fun$] : ! [v1: B_b_prod_update_c_update_fun$] : % 180.68/24.63 ! [v2: B_b_prod_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 % 180.68/24.63 = v0 | ~ (comp$bb(v3, v2) = v1) | ~ (comp$bb(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_c_prod_update_c_update_fun$] : ! [v1: B_c_prod_update_c_update_fun$] : ! % 180.68/24.63 [v2: C_update_c_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$s(v3, v2) = v1) | ~ (register_pair$s(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_c_prod_update_c_update_fun$] : ! [v1: B_c_prod_update_c_update_fun$] : % 180.68/24.63 ! [v2: B_c_prod_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 % 180.68/24.63 = v0 | ~ (comp$ba(v3, v2) = v1) | ~ (comp$ba(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_b_prod_update_c_update_fun$] : ! [v1: C_b_prod_update_c_update_fun$] : ! % 180.68/24.63 [v2: C_b_prod_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = % 180.68/24.63 v0 | ~ (comp$az(v3, v2) = v1) | ~ (comp$az(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_c_update_fun$] : ! [v1: C_c_prod_update_c_update_fun$] : ! % 180.68/24.63 [v2: C_c_prod_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = % 180.68/24.63 v0 | ~ (comp$ay(v3, v2) = v1) | ~ (comp$ay(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_b_prod_update_b_update_fun$] : ! [v1: B_b_prod_update_b_update_fun$] : ! % 180.68/24.63 [v2: B_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$r(v3, v2) = v1) | ~ (register_pair$r(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_b_prod_update_b_update_fun$] : ! [v1: B_b_prod_update_b_update_fun$] : % 180.68/24.63 ! [v2: B_b_prod_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 % 180.68/24.63 = v0 | ~ (comp$ax(v3, v2) = v1) | ~ (comp$ax(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_c_prod_update_b_update_fun$] : ! [v1: B_c_prod_update_b_update_fun$] : ! % 180.68/24.63 [v2: C_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$q(v3, v2) = v1) | ~ (register_pair$q(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_c_prod_update_b_update_fun$] : ! [v1: B_c_prod_update_b_update_fun$] : % 180.68/24.63 ! [v2: B_c_prod_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 % 180.68/24.63 = v0 | ~ (comp$aw(v3, v2) = v1) | ~ (comp$aw(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_b_prod_update_b_update_fun$] : ! [v1: C_b_prod_update_b_update_fun$] : ! % 180.68/24.63 [v2: C_b_prod_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 = % 180.68/24.63 v0 | ~ (comp$av(v3, v2) = v1) | ~ (comp$av(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_a_update_fun$] : ! [v1: C_c_prod_update_a_update_fun$] : ! % 180.68/24.63 [v2: C_update_a_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$p(v3, v2) = v1) | ~ (register_pair$p(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_c_prod_update_b_update_fun$] : ! [v1: C_c_prod_update_b_update_fun$] : % 180.68/24.63 ! [v2: C_c_prod_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 % 180.68/24.63 = v0 | ~ (comp$au(v3, v2) = v1) | ~ (comp$au(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_b_prod_update_a_update_fun$] : ! [v1: C_b_prod_update_a_update_fun$] : ! % 180.68/24.63 [v2: B_update_a_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_pair$o(v3, v2) = v1) | ~ (register_pair$o(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_a_prod_update_c_b_prod_update_fun$] : ! [v1: % 180.68/24.63 A_a_prod_update_c_b_prod_update_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$ac(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$ac(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_a_prod_update_a_update_fun$] : ! [v1: A_a_prod_update_a_update_fun$] : ! % 180.68/24.63 [v2: A_a_prod_update_c_b_prod_update_fun$] : ! [v3: % 180.68/24.63 C_b_prod_update_a_update_fun$] : (v1 = v0 | ~ (comp$at(v3, v2) = v1) | ~ % 180.68/24.63 (comp$at(v3, v2) = v0)) & ! [v0: C_b_prod_update_b_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_b_update_fun$] : ! [v2: B_update_b_update_fun$] : ! [v3: % 180.68/24.63 C_update_b_update_fun$] : (v1 = v0 | ~ (register_pair$n(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$n(v3, v2) = v0)) & ! [v0: C_b_prod_update_b_update_fun$] : % 180.68/24.63 ! [v1: C_b_prod_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_update_fun$] : (v1 = v0 | ~ (comp$as(v3, v2) = v1) | ~ % 180.68/24.63 (comp$as(v3, v2) = v0)) & ! [v0: C_b_prod_update_c_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_c_update_fun$] : ! [v2: B_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_c_update_fun$] : (v1 = v0 | ~ (register_pair$m(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$m(v3, v2) = v0)) & ! [v0: C_b_prod_update_c_update_fun$] : % 180.68/24.63 ! [v1: C_b_prod_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_c_update_fun$] : (v1 = v0 | ~ (comp$ar(v3, v2) = v1) | ~ % 180.68/24.63 (comp$ar(v3, v2) = v0)) & ! [v0: A_b_prod_update_a_update_fun$] : ! [v1: % 180.68/24.63 A_b_prod_update_a_update_fun$] : ! [v2: B_update_a_update_fun$] : ! [v3: % 180.68/24.63 A_update_a_update_fun$] : (v1 = v0 | ~ (register_pair$l(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$l(v3, v2) = v0)) & ! [v0: B_a_prod_update_a_update_fun$] : % 180.68/24.63 ! [v1: B_a_prod_update_a_update_fun$] : ! [v2: A_update_a_update_fun$] : ! % 180.68/24.63 [v3: B_update_a_update_fun$] : (v1 = v0 | ~ (register_pair$k(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$k(v3, v2) = v0)) & ! [v0: A_b_prod_update_a_update_fun$] : % 180.68/24.63 ! [v1: A_b_prod_update_a_update_fun$] : ! [v2: % 180.68/24.63 A_b_prod_update_b_a_prod_update_fun$] : ! [v3: % 180.68/24.63 B_a_prod_update_a_update_fun$] : (v1 = v0 | ~ (comp$aq(v3, v2) = v1) | ~ % 180.68/24.63 (comp$aq(v3, v2) = v0)) & ! [v0: C_a_prod_update_b_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_b_update_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.63 C_update_b_update_fun$] : (v1 = v0 | ~ (register_pair$j(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$j(v3, v2) = v0)) & ! [v0: A_c_prod_update_b_update_fun$] : % 180.68/24.63 ! [v1: A_c_prod_update_b_update_fun$] : ! [v2: C_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (register_pair$i(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$i(v3, v2) = v0)) & ! [v0: C_a_prod_update_b_update_fun$] : % 180.68/24.63 ! [v1: C_a_prod_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_a_prod_update_a_c_prod_update_fun$] : ! [v3: % 180.68/24.63 A_c_prod_update_b_update_fun$] : (v1 = v0 | ~ (comp$ap(v3, v2) = v1) | ~ % 180.68/24.63 (comp$ap(v3, v2) = v0)) & ! [v0: C_a_prod_update_c_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_c_update_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_c_update_fun$] : (v1 = v0 | ~ (register_pair$h(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$h(v3, v2) = v0)) & ! [v0: A_c_prod_update_c_update_fun$] : % 180.68/24.63 ! [v1: A_c_prod_update_c_update_fun$] : ! [v2: C_update_c_update_fun$] : ! % 180.68/24.63 [v3: A_update_c_update_fun$] : (v1 = v0 | ~ (register_pair$g(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$g(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_a_prod_update_a_c_prod_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_a_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : ! % 180.68/24.63 [v3: C_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$ab(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$ab(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_a_prod_update_c_update_fun$] : ! [v1: C_a_prod_update_c_update_fun$] : ! % 180.68/24.63 [v2: C_a_prod_update_a_c_prod_update_fun$] : ! [v3: % 180.68/24.63 A_c_prod_update_c_update_fun$] : (v1 = v0 | ~ (comp$ao(v3, v2) = v1) | ~ % 180.68/24.63 (comp$ao(v3, v2) = v0)) & ! [v0: B_c_prod_update_a_update_fun$] : ! [v1: % 180.68/24.63 B_c_prod_update_a_update_fun$] : ! [v2: C_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun$] : (v1 = v0 | ~ (register_pair$f(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$f(v3, v2) = v0)) & ! [v0: A_a_prod_update_a_update_fun$] : % 180.68/24.63 ! [v1: A_a_prod_update_a_update_fun$] : ! [v2: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : ! [v3: % 180.68/24.63 B_c_prod_update_a_update_fun$] : (v1 = v0 | ~ (comp$an(v3, v2) = v1) | ~ % 180.68/24.63 (comp$an(v3, v2) = v0)) & ! [v0: C_c_prod_update_b_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_b_update_fun$] : ! [v2: C_update_b_update_fun$] : ! [v3: % 180.68/24.63 C_update_b_update_fun$] : (v1 = v0 | ~ (register_pair$e(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$e(v3, v2) = v0)) & ! [v0: A_a_prod_update_b_update_fun$] : % 180.68/24.63 ! [v1: A_a_prod_update_b_update_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (register_pair$d(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$d(v3, v2) = v0)) & ! [v0: C_c_prod_update_b_update_fun$] : % 180.68/24.63 ! [v1: C_c_prod_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_update_fun$] : (v1 = v0 | ~ (comp$am(v3, v2) = v1) | ~ % 180.68/24.63 (comp$am(v3, v2) = v0)) & ! [v0: C_c_prod_update_c_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_c_update_fun$] : ! [v2: C_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_c_update_fun$] : (v1 = v0 | ~ (register_pair$c(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$c(v3, v2) = v0)) & ! [v0: A_a_prod_update_c_update_fun$] : % 180.68/24.63 ! [v1: A_a_prod_update_c_update_fun$] : ! [v2: A_update_c_update_fun$] : ! % 180.68/24.63 [v3: A_update_c_update_fun$] : (v1 = v0 | ~ (register_pair$b(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$b(v3, v2) = v0)) & ! [v0: C_c_prod_update_c_update_fun$] : % 180.68/24.63 ! [v1: C_c_prod_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_c_update_fun$] : (v1 = v0 | ~ (comp$al(v3, v2) = v1) | ~ % 180.68/24.63 (comp$al(v3, v2) = v0)) & ! [v0: A_a_prod_update_a_update_fun$] : ! [v1: % 180.68/24.63 A_a_prod_update_a_update_fun$] : ! [v2: A_update_a_update_fun$] : ! [v3: % 180.68/24.63 A_update_a_update_fun$] : (v1 = v0 | ~ (register_pair$a(v3, v2) = v1) | ~ % 180.68/24.63 (register_pair$a(v3, v2) = v0)) & ! [v0: B_b_prod_update_a_update_fun$] : % 180.68/24.63 ! [v1: B_b_prod_update_a_update_fun$] : ! [v2: B_update_a_update_fun$] : ! % 180.68/24.63 [v3: B_update_a_update_fun$] : (v1 = v0 | ~ (register_pair$(v3, v2) = v1) | % 180.68/24.63 ~ (register_pair$(v3, v2) = v0)) & ! [v0: A_a_prod_update_a_update_fun$] : % 180.68/24.63 ! [v1: A_a_prod_update_a_update_fun$] : ! [v2: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : ! [v3: % 180.68/24.63 B_b_prod_update_a_update_fun$] : (v1 = v0 | ~ (comp$ak(v3, v2) = v1) | ~ % 180.68/24.63 (comp$ak(v3, v2) = v0)) & ! [v0: B_update_b_update_fun$] : ! [v1: % 180.68/24.63 B_update_b_update_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun$] : (v1 = v0 | ~ (fcomp$d(v3, v2) = v1) | ~ % 180.68/24.63 (fcomp$d(v3, v2) = v0)) & ! [v0: C_update_b_update_fun$] : ! [v1: % 180.68/24.63 C_update_b_update_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.63 C_update_a_update_fun$] : (v1 = v0 | ~ (fcomp$c(v3, v2) = v1) | ~ % 180.68/24.63 (fcomp$c(v3, v2) = v0)) & ! [v0: B_update_c_update_fun$] : ! [v1: % 180.68/24.63 B_update_c_update_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun$] : (v1 = v0 | ~ (fcomp$b(v3, v2) = v1) | ~ % 180.68/24.63 (fcomp$b(v3, v2) = v0)) & ! [v0: C_update_c_update_fun$] : ! [v1: % 180.68/24.63 C_update_c_update_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_a_update_fun$] : (v1 = v0 | ~ (fcomp$a(v3, v2) = v1) | ~ % 180.68/24.63 (fcomp$a(v3, v2) = v0)) & ! [v0: A_update_a_update_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun$] : ! [v2: B_update_a_update_fun$] : ! [v3: % 180.68/24.63 A_update_b_update_fun$] : (v1 = v0 | ~ (fcomp$(v3, v2) = v1) | ~ % 180.68/24.63 (fcomp$(v3, v2) = v0)) & ! [v0: B_b_prod_update$] : ! [v1: % 180.68/24.63 B_b_prod_update$] : ! [v2: B_update$] : ! [v3: B_update$] : (v1 = v0 | ~ % 180.68/24.63 (tensor_update$f(v3, v2) = v1) | ~ (tensor_update$f(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_a_prod_update$] : ! [v1: A_a_prod_update$] : ! [v2: B_b_prod_update$] % 180.68/24.63 : ! [v3: B_b_prod_update_a_a_prod_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$ar(v3, v2) = v1) | ~ (fun_app$ar(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_a_prod_update$] : ! [v1: B_a_prod_update$] : ! [v2: A_update$] : ! [v3: % 180.68/24.63 B_update$] : (v1 = v0 | ~ (tensor_update$e(v3, v2) = v1) | ~ % 180.68/24.63 (tensor_update$e(v3, v2) = v0)) & ! [v0: A_c_prod_update$] : ! [v1: % 180.68/24.63 A_c_prod_update$] : ! [v2: B_a_prod_update$] : ! [v3: % 180.68/24.63 B_a_prod_update_a_c_prod_update_fun$] : (v1 = v0 | ~ (fun_app$aq(v3, v2) = % 180.68/24.63 v1) | ~ (fun_app$aq(v3, v2) = v0)) & ! [v0: A_b_prod_update$] : ! [v1: % 180.68/24.63 A_b_prod_update$] : ! [v2: B_update$] : ! [v3: A_update$] : (v1 = v0 | ~ % 180.68/24.63 (tensor_update$d(v3, v2) = v1) | ~ (tensor_update$d(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_a_prod_update$] : ! [v1: C_a_prod_update$] : ! [v2: A_b_prod_update$] % 180.68/24.63 : ! [v3: A_b_prod_update_c_a_prod_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$ap(v3, v2) = v1) | ~ (fun_app$ap(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update$] : ! [v1: C_c_prod_update$] : ! [v2: A_a_prod_update$] : % 180.68/24.63 ! [v3: A_a_prod_update_c_c_prod_update_fun$] : (v1 = v0 | ~ (fun_app$ao(v3, % 180.68/24.63 v2) = v1) | ~ (fun_app$ao(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$aj(v3, v2) = v1) | ~ (comp$aj(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ai(v3, v2) = v1) | ~ (comp$ai(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ah(v3, v2) = v1) | ~ (comp$ah(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ag(v3, v2) = v1) | ~ (comp$ag(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_c_update_fun$] : ! [v1: B_update_c_update_fun$] : ! [v2: % 180.68/24.63 B_update_b_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$af(v3, v2) = v1) | ~ (comp$af(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.63 C_update_b_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ae(v3, v2) = v1) | ~ (comp$ae(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.63 B_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ac(v3, v2) = v1) | ~ (comp$ac(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ad(v3, v2) = v1) | ~ (comp$ad(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.63 C_update_a_update_fun$] : ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$aa(v3, v2) = v1) | ~ (comp$aa(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_a_update_fun$] : ! [v1: C_update_a_update_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$z(v3, v2) = v1) | ~ (comp$z(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : ! [v3: A_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$ab(v3, v2) = v1) | ~ (comp$ab(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$x(v3, v2) = v1) | ~ (comp$x(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$w(v3, v2) = v1) | ~ (comp$w(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! [v2: % 180.68/24.63 B_update_b_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$y(v3, v2) = v1) | ~ (comp$y(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_update_b_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$(v3, v2) = v1) | ~ (comp$(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun$] : ! [v1: B_update_b_update_fun$] : ! [v2: % 180.68/24.63 B_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$v(v3, v2) = v1) | ~ (comp$v(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_a_prod_update_a_b_prod_update_fun$] : ! [v1: % 180.68/24.63 B_a_prod_update_a_b_prod_update_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: B_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$aa(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$aa(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_a_prod_update_b_a_prod_update_fun$] : ! [v1: % 180.68/24.63 B_a_prod_update_b_a_prod_update_fun$] : ! [v2: % 180.68/24.63 B_a_prod_update_a_b_prod_update_fun$] : ! [v3: % 180.68/24.63 A_b_prod_update_b_a_prod_update_fun$] : (v1 = v0 | ~ (comp$u(v3, v2) = v1) % 180.68/24.63 | ~ (comp$u(v3, v2) = v0)) & ! [v0: C_a_prod_update_b_a_prod_update_fun$] % 180.68/24.63 : ! [v1: C_a_prod_update_b_a_prod_update_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$z(v3, v2) = v1) | ~ (register_tensor$z(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_b_prod_update_b_a_prod_update_fun$] : ! [v1: % 180.68/24.63 A_b_prod_update_b_a_prod_update_fun$] : ! [v2: B_update_a_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$x(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$x(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_a_prod_update_a_b_prod_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_a_b_prod_update_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: C_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$y(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$y(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_a_prod_update_b_a_prod_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_b_a_prod_update_fun$] : ! [v2: % 180.68/24.63 C_a_prod_update_a_b_prod_update_fun$] : ! [v3: % 180.68/24.63 A_b_prod_update_b_a_prod_update_fun$] : (v1 = v0 | ~ (comp$t(v3, v2) = v1) % 180.68/24.63 | ~ (comp$t(v3, v2) = v0)) & ! [v0: B_b_prod_update_b_c_prod_update_fun$] % 180.68/24.63 : ! [v1: B_b_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 B_update_c_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$w(v3, v2) = v1) | ~ (register_tensor$w(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_b_prod_update_b_c_prod_update_fun$] : ! [v1: % 180.68/24.63 B_b_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 B_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : (v1 = v0 | ~ (comp$s(v3, v2) = v1) % 180.68/24.63 | ~ (comp$s(v3, v2) = v0)) & ! [v0: B_c_prod_update_b_c_prod_update_fun$] % 180.68/24.63 : ! [v1: B_c_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 B_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : (v1 = v0 | ~ (comp$r(v3, v2) = v1) % 180.68/24.63 | ~ (comp$r(v3, v2) = v0)) & ! [v0: C_b_prod_update_b_c_prod_update_fun$] % 180.68/24.63 : ! [v1: C_b_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 B_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$v(v3, v2) = v1) | ~ (register_tensor$v(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_b_prod_update_b_c_prod_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 C_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : (v1 = v0 | ~ (comp$q(v3, v2) = v1) % 180.68/24.63 | ~ (comp$q(v3, v2) = v0)) & ! [v0: C_c_prod_update_b_c_prod_update_fun$] % 180.68/24.63 : ! [v1: C_c_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$u(v3, v2) = v1) | ~ (register_tensor$u(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_a_prod_update_b_c_prod_update_fun$] : ! [v1: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$t(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$t(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_b_c_prod_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_b_c_prod_update_fun$] : ! [v2: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_c_prod_update_fun$] : (v1 = v0 | ~ (comp$p(v3, v2) = v1) % 180.68/24.63 | ~ (comp$p(v3, v2) = v0)) & ! [v0: B_b_prod_update_b_b_prod_update_fun$] % 180.68/24.63 : ! [v1: B_b_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 B_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : (v1 = v0 | ~ (comp$o(v3, v2) = v1) % 180.68/24.63 | ~ (comp$o(v3, v2) = v0)) & ! [v0: B_c_prod_update_b_b_prod_update_fun$] % 180.68/24.63 : ! [v1: B_c_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 C_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$s(v3, v2) = v1) | ~ (register_tensor$s(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_c_prod_update_a_a_prod_update_fun$] : ! [v1: % 180.68/24.63 B_c_prod_update_a_a_prod_update_fun$] : ! [v2: C_update_a_update_fun$] : ! % 180.68/24.63 [v3: B_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$r(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$r(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_c_prod_update_b_b_prod_update_fun$] : ! [v1: % 180.68/24.63 B_c_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 B_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : (v1 = v0 | ~ (comp$n(v3, v2) = v1) % 180.68/24.63 | ~ (comp$n(v3, v2) = v0)) & ! [v0: C_b_prod_update_b_b_prod_update_fun$] % 180.68/24.63 : ! [v1: C_b_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 B_update_b_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$q(v3, v2) = v1) | ~ (register_tensor$q(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_b_prod_update_a_a_prod_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_a_a_prod_update_fun$] : ! [v2: B_update_a_update_fun$] : ! % 180.68/24.63 [v3: C_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$p(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$p(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_b_prod_update_b_b_prod_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 C_b_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : (v1 = v0 | ~ (comp$m(v3, v2) = v1) % 180.68/24.63 | ~ (comp$m(v3, v2) = v0)) & ! [v0: C_c_prod_update_b_b_prod_update_fun$] % 180.68/24.63 : ! [v1: C_c_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 C_update_b_update_fun$] : ! [v3: C_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$o(v3, v2) = v1) | ~ (register_tensor$o(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_a_prod_update_b_b_prod_update_fun$] : ! [v1: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$m(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$m(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v2: C_update_a_update_fun$] : ! % 180.68/24.63 [v3: C_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$n(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$n(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_b_b_prod_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_b_b_prod_update_fun$] : ! [v2: % 180.68/24.63 C_c_prod_update_a_a_prod_update_fun$] : ! [v3: % 180.68/24.63 A_a_prod_update_b_b_prod_update_fun$] : (v1 = v0 | ~ (comp$l(v3, v2) = v1) % 180.68/24.63 | ~ (comp$l(v3, v2) = v0)) & ! [v0: B_b_prod_update_a_a_prod_update_fun$] % 180.68/24.63 : ! [v1: B_b_prod_update_a_a_prod_update_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (register_tensor$l(v3, v2) = v1) | ~ (register_tensor$l(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_a_prod_update_a_c_prod_update_fun$] : ! [v1: % 180.68/24.63 B_a_prod_update_a_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : ! % 180.68/24.63 [v3: B_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$k(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$k(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_b_prod_update_c_a_prod_update_fun$] : ! [v1: % 180.68/24.63 A_b_prod_update_c_a_prod_update_fun$] : ! [v2: B_update_a_update_fun$] : ! % 180.68/24.63 [v3: A_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$j(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$j(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_a_prod_update_c_c_prod_update_fun$] : ! [v1: % 180.68/24.63 A_a_prod_update_c_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : ! % 180.68/24.63 [v3: A_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$i(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$i(v3, v2) = v0)) & ! [v0: A_update_a_update_fun$] : % 180.68/24.63 ! [v1: A_update_a_update_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_a_update_fun$] : (v1 = v0 | ~ (comp$k(v3, v2) = v1) | ~ % 180.68/24.63 (comp$k(v3, v2) = v0)) & ! [v0: A_a_prod_update_a_a_prod_update_fun$] : ! % 180.68/24.63 [v1: A_a_prod_update_a_a_prod_update_fun$] : ! [v2: A_update_a_update_fun$] : % 180.68/24.63 ! [v3: A_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$h(v3, v2) = % 180.68/24.63 v1) | ~ (register_tensor$h(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_b_prod_update_a_b_prod_update_fun$] : ! [v1: % 180.68/24.63 A_b_prod_update_a_b_prod_update_fun$] : ! [v2: B_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$g(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$g(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_c_prod_update_a_c_prod_update_fun$] : ! [v1: % 180.68/24.63 A_c_prod_update_a_c_prod_update_fun$] : ! [v2: C_update_c_update_fun$] : ! % 180.68/24.63 [v3: A_update_a_update_fun$] : (v1 = v0 | ~ (register_tensor$f(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$f(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_a_prod_update_b_a_prod_update_fun$] : ! [v1: % 180.68/24.63 B_a_prod_update_b_a_prod_update_fun$] : ! [v2: A_update_a_update_fun$] : ! % 180.68/24.63 [v3: B_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$e(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$e(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_b_prod_update_b_b_prod_update_fun$] : ! [v1: % 180.68/24.63 B_b_prod_update_b_b_prod_update_fun$] : ! [v2: B_update_b_update_fun$] : ! % 180.68/24.63 [v3: B_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$d(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$d(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_c_prod_update_b_c_prod_update_fun$] : ! [v1: % 180.68/24.63 B_c_prod_update_b_c_prod_update_fun$] : ! [v2: C_update_c_update_fun$] : ! % 180.68/24.63 [v3: B_update_b_update_fun$] : (v1 = v0 | ~ (register_tensor$c(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$c(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_a_prod_update_c_a_prod_update_fun$] : ! [v1: % 180.68/24.63 C_a_prod_update_c_a_prod_update_fun$] : ! [v2: A_update_a_update_fun$] : ! % 180.68/24.63 [v3: C_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$b(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$b(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_b_prod_update_c_b_prod_update_fun$] : ! [v1: % 180.68/24.63 C_b_prod_update_c_b_prod_update_fun$] : ! [v2: B_update_b_update_fun$] : ! % 180.68/24.63 [v3: C_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$a(v3, v2) = v1) % 180.68/24.63 | ~ (register_tensor$a(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update_c_c_prod_update_fun$] : ! [v1: % 180.68/24.63 C_c_prod_update_c_c_prod_update_fun$] : ! [v2: C_update_c_update_fun$] : ! % 180.68/24.63 [v3: C_update_c_update_fun$] : (v1 = v0 | ~ (register_tensor$(v3, v2) = v1) | % 180.68/24.63 ~ (register_tensor$(v3, v2) = v0)) & ! [v0: B_update_b_update_fun$] : ! % 180.68/24.63 [v1: B_update_b_update_fun$] : ! [v2: B_update_b_update_fun$] : ! [v3: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$an(v3, v2) = v1) | ~ (fun_app$an(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_update_b_update_fun$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$i(v3, v2) = v1) | ~ (comp$i(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_c_update_fun$] : ! [v1: B_update_c_update_fun$] : ! [v2: % 180.68/24.63 B_update_c_update_fun$] : ! [v3: C_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (comp$h(v3, v2) = v1) | ~ (comp$h(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : ! [v3: % 180.68/24.63 C_update_c_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$am(v3, v2) = v1) | ~ (fun_app$am(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : ! [v3: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$al(v3, v2) = v1) | ~ (fun_app$al(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: % 180.68/24.63 A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | ~ (fun_app$ak(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_update_b_update_fun$] : ! [v1: B_update_b_update_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_b_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$aj(v3, v2) = v1) | ~ (fun_app$aj(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: % 180.68/24.63 A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (fun_app$y(v3, v2) = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_update_b_update_fun$] : ! [v1: C_update_b_update_fun$] : ! [v2: % 180.68/24.63 C_update_a_update_fun$] : ! [v3: % 180.68/24.63 C_update_a_update_fun_c_update_b_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$x(v3, v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: B_update$] % 180.68/24.63 : ! [v1: B_update$] : ! [v2: C_update$] : ! [v3: C_update_b_update_fun$] : % 180.68/24.63 (v1 = v0 | ~ (fun_app$ai(v3, v2) = v1) | ~ (fun_app$ai(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun$] : ! [v3: % 180.68/24.63 A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (fun_app$w(v3, v2) = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! % 180.68/24.63 [v0: B_update_c_update_fun$] : ! [v1: B_update_c_update_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_b_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$v(v3, v2) = v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: C_update$] % 180.68/24.63 : ! [v1: C_update$] : ! [v2: B_update$] : ! [v3: B_update_c_update_fun$] : % 180.68/24.63 (v1 = v0 | ~ (fun_app$ah(v3, v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 C_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_c_update_fun$] : ! [v3: % 180.68/24.63 A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (fun_app$af(v3, v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_update_c_update_fun$] : ! [v1: C_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_update_a_update_fun$] : ! [v3: % 180.68/24.63 C_update_a_update_fun_c_update_c_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$ae(v3, v2) = v1) | ~ (fun_app$ae(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update$] : ! [v1: A_update$] : ! [v2: C_update$] : ! [v3: % 180.68/24.63 C_update_a_update_fun$] : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$ag(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 B_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ (fun_app$ad(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! [v2: % 180.68/24.63 A_update_b_update_fun$] : ! [v3: % 180.68/24.63 A_update_b_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update$] : ! [v1: A_update$] : ! [v2: A_update$] : ! [v3: % 180.68/24.63 A_update_a_update_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$ab(v3, v2) = v0)) & ! [v0: B_update$] : ! [v1: B_update$] : ! % 180.68/24.63 [v2: B_update$] : ! [v3: B_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_update$] : ! [v1: C_update$] : ! [v2: C_update$] : ! [v3: % 180.68/24.63 C_update_c_update_fun$] : (v1 = v0 | ~ (fun_app$z(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$z(v3, v2) = v0)) & ! [v0: B_update_a_update_fun$] : ! [v1: % 180.68/24.63 B_update_a_update_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.63 A_update_set$] : (v1 = v0 | ~ (the_inv_into$b(v3, v2) = v1) | ~ % 180.68/24.63 (the_inv_into$b(v3, v2) = v0)) & ! [v0: A_update_b_update_fun$] : ! [v1: % 180.68/24.63 A_update_b_update_fun$] : ! [v2: B_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_set$] : (v1 = v0 | ~ (the_inv_into$a(v3, v2) = v1) | ~ % 180.68/24.63 (the_inv_into$a(v3, v2) = v0)) & ! [v0: A_update_c_update_fun$] : ! [v1: % 180.68/24.63 A_update_c_update_fun$] : ! [v2: C_update_a_update_fun$] : ! [v3: % 180.68/24.63 C_update_set$] : (v1 = v0 | ~ (the_inv_into$(v3, v2) = v1) | ~ % 180.68/24.63 (the_inv_into$(v3, v2) = v0)) & ! [v0: A_update_bool_fun$] : ! [v1: % 180.68/24.63 A_update_bool_fun$] : ! [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.63 A_update_b_update_fun$] : (v1 = v0 | ~ (uup$(v3, v2) = v1) | ~ (uup$(v3, % 180.68/24.63 v2) = v0)) & ! [v0: B_update$] : ! [v1: B_update$] : ! [v2: % 180.68/24.63 A_update$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ (fun_app$u(v3, % 180.68/24.63 v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: A_update_bool_fun$] : % 180.68/24.63 ! [v1: A_update_bool_fun$] : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 A_update_c_update_fun$] : (v1 = v0 | ~ (uun$(v3, v2) = v1) | ~ (uun$(v3, % 180.68/24.63 v2) = v0)) & ! [v0: B_update_bool_fun$] : ! [v1: B_update_bool_fun$] : % 180.68/24.63 ! [v2: B_update_a_update_fun$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | % 180.68/24.63 ~ (uul$(v3, v2) = v1) | ~ (uul$(v3, v2) = v0)) & ! [v0: A_c_prod_update$] % 180.68/24.63 : ! [v1: A_c_prod_update$] : ! [v2: A_update$] : ! [v3: % 180.68/24.63 A_update_a_c_prod_update_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$t(v3, v2) = v0)) & ! [v0: C_a_prod_update$] : ! [v1: % 180.68/24.63 C_a_prod_update$] : ! [v2: B_update$] : ! [v3: % 180.68/24.63 B_update_c_a_prod_update_fun$] : (v1 = v0 | ~ (fun_app$s(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$s(v3, v2) = v0)) & ! [v0: A_update_b_update_fun_bool_fun$] : ! % 180.68/24.63 [v1: A_update_b_update_fun_bool_fun$] : ! [v2: A_update_b_update_fun$] : ! % 180.68/24.63 [v3: A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$] : (v1 = v0 | % 180.68/24.63 ~ (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun_bool_fun$] : ! [v1: A_update_c_update_fun_bool_fun$] % 180.68/24.63 : ! [v2: A_update_c_update_fun$] : ! [v3: % 180.68/24.63 A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$q(v3, v2) = v1) | ~ (fun_app$q(v3, v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun_bool_fun$] : ! [v1: B_update_a_update_fun_bool_fun$] % 180.68/24.63 : ! [v2: B_update_a_update_fun$] : ! [v3: % 180.68/24.63 B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$o(v3, v2) = v1) | ~ (fun_app$o(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_bool_fun$] : ! [v1: A_update_bool_fun$] : ! [v2: A_update$] : ! % 180.68/24.63 [v3: A_update_a_update_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) % 180.68/24.63 | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: B_update_bool_fun$] : ! [v1: % 180.68/24.63 B_update_bool_fun$] : ! [v2: B_update$] : ! [v3: % 180.68/24.63 B_update_b_update_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) | % 180.68/24.63 ~ (fun_app$l(v3, v2) = v0)) & ! [v0: C_update_bool_fun$] : ! [v1: % 180.68/24.63 C_update_bool_fun$] : ! [v2: C_update$] : ! [v3: % 180.68/24.63 C_update_c_update_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | % 180.68/24.63 ~ (fun_app$j(v3, v2) = v0)) & ! [v0: C_a_prod_update$] : ! [v1: % 180.68/24.63 C_a_prod_update$] : ! [v2: A_update$] : ! [v3: % 180.68/24.63 A_update_c_a_prod_update_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$h(v3, v2) = v0)) & ! [v0: C_a_prod_update$] : ! [v1: % 180.68/24.63 C_a_prod_update$] : ! [v2: A_update$] : ! [v3: C_update$] : (v1 = v0 | ~ % 180.68/24.63 (tensor_update$c(v3, v2) = v1) | ~ (tensor_update$c(v3, v2) = v0)) & ! % 180.68/24.63 [v0: C_c_prod_update$] : ! [v1: C_c_prod_update$] : ! [v2: A_update$] : ! % 180.68/24.63 [v3: A_update_c_c_prod_update_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | % 180.68/24.63 ~ (fun_app$f(v3, v2) = v0)) & ! [v0: C_update$] : ! [v1: C_update$] : ! % 180.68/24.63 [v2: A_update$] : ! [v3: A_update_c_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 180.68/24.63 C_c_prod_update$] : ! [v1: C_c_prod_update$] : ! [v2: C_update$] : ! [v3: % 180.68/24.63 C_update$] : (v1 = v0 | ~ (tensor_update$b(v3, v2) = v1) | ~ % 180.68/24.63 (tensor_update$b(v3, v2) = v0)) & ! [v0: A_a_prod_update$] : ! [v1: % 180.68/24.63 A_a_prod_update$] : ! [v2: B_update$] : ! [v3: % 180.68/24.63 B_update_a_a_prod_update_fun$] : (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) | ~ % 180.68/24.63 (fun_app$e(v3, v2) = v0)) & ! [v0: A_a_prod_update$] : ! [v1: % 180.68/24.63 A_a_prod_update$] : ! [v2: A_update$] : ! [v3: A_update$] : (v1 = v0 | ~ % 180.68/24.63 (tensor_update$a(v3, v2) = v1) | ~ (tensor_update$a(v3, v2) = v0)) & ! % 180.68/24.63 [v0: A_c_prod_update$] : ! [v1: A_c_prod_update$] : ! [v2: B_update$] : ! % 180.68/24.63 [v3: B_update_a_c_prod_update_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | % 180.68/24.63 ~ (fun_app$c(v3, v2) = v0)) & ! [v0: A_update$] : ! [v1: A_update$] : ! % 180.68/24.63 [v2: B_update$] : ! [v3: B_update_a_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_c_prod_update$] : ! [v1: A_c_prod_update$] : ! [v2: C_update$] : ! [v3: % 180.68/24.63 A_update$] : (v1 = v0 | ~ (tensor_update$(v3, v2) = v1) | ~ % 180.68/24.63 (tensor_update$(v3, v2) = v0)) & ! [v0: A_update_set$] : ! [v1: % 180.68/24.63 A_update_set$] : ! [v2: B_update_set$] : ! [v3: B_update_a_update_fun$] : % 180.68/24.63 (v1 = v0 | ~ (image$b(v3, v2) = v1) | ~ (image$b(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_set$] : ! [v1: A_update_set$] : ! [v2: C_update_set$] : ! [v3: % 180.68/24.63 C_update_a_update_fun$] : (v1 = v0 | ~ (image$a(v3, v2) = v1) | ~ % 180.68/24.63 (image$a(v3, v2) = v0)) & ! [v0: B_update_set$] : ! [v1: B_update_set$] : % 180.68/24.63 ! [v2: A_update_set$] : ! [v3: A_update_b_update_fun$] : (v1 = v0 | ~ % 180.68/24.63 (image$(v3, v2) = v1) | ~ (image$(v3, v2) = v0)) & ! [v0: % 180.68/24.63 A_update_set_a_update_set_fun$] : ! [v1: A_update_set_a_update_set_fun$] : % 180.68/24.63 ! [v2: A_update_a_update_fun$] : (v1 = v0 | ~ (vimage$b(v2) = v1) | ~ % 180.68/24.63 (vimage$b(v2) = v0)) & ! [v0: B_update_set_b_update_set_fun$] : ! [v1: % 180.68/24.63 B_update_set_b_update_set_fun$] : ! [v2: B_update_b_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (vimage$a(v2) = v1) | ~ (vimage$a(v2) = v0)) & ! [v0: % 180.68/24.63 C_update_set_c_update_set_fun$] : ! [v1: C_update_set_c_update_set_fun$] : % 180.68/24.63 ! [v2: C_update_c_update_fun$] : (v1 = v0 | ~ (vimage$(v2) = v1) | ~ % 180.68/24.63 (vimage$(v2) = v0)) & ! [v0: B_update_a_update_fun_set$] : ! [v1: % 180.68/24.63 B_update_a_update_fun_set$] : ! [v2: B_update_a_update_fun_bool_fun$] : (v1 % 180.68/24.63 = v0 | ~ (collect$b(v2) = v1) | ~ (collect$b(v2) = v0)) & ! [v0: % 180.68/24.63 C_update_a_update_fun_set$] : ! [v1: C_update_a_update_fun_set$] : ! [v2: % 180.68/24.63 C_update_a_update_fun_bool_fun$] : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ % 180.68/24.63 (collect$a(v2) = v0)) & ! [v0: A_update_b_update_fun_set$] : ! [v1: % 180.68/24.63 A_update_b_update_fun_set$] : ! [v2: A_update_b_update_fun_bool_fun$] : (v1 % 180.68/24.63 = v0 | ~ (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v2: B_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (the_inv_into$h(v2) = v1) | ~ (the_inv_into$h(v2) = v0)) & ! % 180.68/24.63 [v0: C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v2: C_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (the_inv_into$d(v2) = v1) | ~ (the_inv_into$d(v2) = v0)) & ! % 180.68/24.63 [v0: A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v2: A_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (the_inv_into$c(v2) = v1) | ~ (the_inv_into$c(v2) = v0)) & ! % 180.68/24.63 [v0: A_update_a_update_bool_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_bool_fun_fun$] : ! [v2: A_update_a_update_bool_fun_fun$] % 180.68/24.63 : (v1 = v0 | ~ (conversep$b(v2) = v1) | ~ (conversep$b(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_bool_fun_fun$] : ! [v1: B_update_b_update_bool_fun_fun$] % 180.68/24.63 : ! [v2: B_update_b_update_bool_fun_fun$] : (v1 = v0 | ~ (conversep$a(v2) = % 180.68/24.63 v1) | ~ (conversep$a(v2) = v0)) & ! [v0: % 180.68/24.63 C_update_c_update_bool_fun_fun$] : ! [v1: C_update_c_update_bool_fun_fun$] % 180.68/24.63 : ! [v2: C_update_c_update_bool_fun_fun$] : (v1 = v0 | ~ (conversep$(v2) = % 180.68/24.63 v1) | ~ (conversep$(v2) = v0)) & ! [v0: A_update_set_a_update_set_fun$] % 180.68/24.63 : ! [v1: A_update_set_a_update_set_fun$] : ! [v2: A_update_a_update_fun$] : % 180.68/24.63 (v1 = v0 | ~ (image$f(v2) = v1) | ~ (image$f(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_set_b_update_set_fun$] : ! [v1: B_update_set_b_update_set_fun$] : % 180.68/24.63 ! [v2: B_update_b_update_fun$] : (v1 = v0 | ~ (image$e(v2) = v1) | ~ % 180.68/24.63 (image$e(v2) = v0)) & ! [v0: C_update_set_c_update_set_fun$] : ! [v1: % 180.68/24.63 C_update_set_c_update_set_fun$] : ! [v2: C_update_c_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (image$d(v2) = v1) | ~ (image$d(v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v2: A_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (inv_into$f(v2) = v1) | ~ (inv_into$f(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v2: B_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (inv_into$e(v2) = v1) | ~ (inv_into$e(v2) = v0)) & ! [v0: % 180.68/24.63 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v2: C_update_set$] : % 180.68/24.63 (v1 = v0 | ~ (inv_into$d(v2) = v1) | ~ (inv_into$d(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun$] : ! [v1: B_update_b_update_fun$] : ! [v2: % 180.68/24.63 B_update$] : (v1 = v0 | ~ (comp_update$b(v2) = v1) | ~ (comp_update$b(v2) % 180.68/24.63 = v0)) & ! [v0: A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] % 180.68/24.63 : ! [v2: A_update$] : (v1 = v0 | ~ (comp_update$a(v2) = v1) | ~ % 180.68/24.63 (comp_update$a(v2) = v0)) & ! [v0: C_update_c_update_fun$] : ! [v1: % 180.68/24.63 C_update_c_update_fun$] : ! [v2: C_update$] : (v1 = v0 | ~ % 180.68/24.63 (comp_update$(v2) = v1) | ~ (comp_update$(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.63 B_update_b_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.63 B_update_b_update_fun$] : (v1 = v0 | ~ (comp$j(v2) = v1) | ~ (comp$j(v2) = % 180.68/24.63 v0)) & ! [v0: C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v1: % 180.68/24.63 C_update_c_update_fun_c_update_c_update_fun_fun$] : ! [v2: % 180.68/24.63 C_update_c_update_fun$] : (v1 = v0 | ~ (comp$g(v2) = v1) | ~ (comp$g(v2) = % 180.68/24.63 v0)) & ! [v0: A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.63 A_update_a_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.63 A_update_a_update_fun$] : (v1 = v0 | ~ (comp$f(v2) = v1) | ~ (comp$f(v2) = % 180.68/24.63 v0)) & ! [v0: B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : % 180.68/24.63 ! [v2: A_update$] : (v1 = v0 | ~ (uu$(v2) = v1) | ~ (uu$(v2) = v0)) & ! % 180.68/24.63 [v0: A_update_b_update_fun$] : ! [v1: A_update_b_update_fun$] : ! [v2: % 180.68/24.63 B_update$] : (v1 = v0 | ~ (uub$(v2) = v1) | ~ (uub$(v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! [v2: % 180.68/24.63 C_update$] : (v1 = v0 | ~ (uua$(v2) = v1) | ~ (uua$(v2) = v0)) & ! [v0: % 180.68/24.63 A_update_a_c_prod_update_fun$] : ! [v1: A_update_a_c_prod_update_fun$] : ! % 180.68/24.63 [v2: A_update_c_update_fun$] : (v1 = v0 | ~ (uue$(v2) = v1) | ~ (uue$(v2) = % 180.68/24.63 v0)) & ! [v0: A_update_c_c_prod_update_fun$] : ! [v1: % 180.68/24.63 A_update_c_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (uuc$(v2) = v1) | ~ (uuc$(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_a_prod_update_fun$] : ! [v1: B_update_a_a_prod_update_fun$] : ! % 180.68/24.63 [v2: B_update_a_update_fun$] : (v1 = v0 | ~ (uui$(v2) = v1) | ~ (uui$(v2) = % 180.68/24.63 v0)) & ! [v0: B_update_c_a_prod_update_fun$] : ! [v1: % 180.68/24.63 B_update_c_a_prod_update_fun$] : ! [v2: B_update_a_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (uug$(v2) = v1) | ~ (uug$(v2) = v0)) & ! [v0: % 180.68/24.63 A_update_c_a_prod_update_fun$] : ! [v1: A_update_c_a_prod_update_fun$] : ! % 180.68/24.63 [v2: A_update_c_update_fun$] : (v1 = v0 | ~ (uuh$(v2) = v1) | ~ (uuh$(v2) = % 180.68/24.63 v0)) & ! [v0: A_update_c_c_prod_update_fun$] : ! [v1: % 180.68/24.63 A_update_c_c_prod_update_fun$] : ! [v2: A_update_c_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (uud$(v2) = v1) | ~ (uud$(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_a_prod_update_fun$] : ! [v1: B_update_a_a_prod_update_fun$] : ! % 180.68/24.63 [v2: B_update_a_update_fun$] : (v1 = v0 | ~ (uuj$(v2) = v1) | ~ (uuj$(v2) = % 180.68/24.63 v0)) & ! [v0: B_update_a_c_prod_update_fun$] : ! [v1: % 180.68/24.63 B_update_a_c_prod_update_fun$] : ! [v2: B_update_a_update_fun$] : (v1 = v0 % 180.68/24.63 | ~ (uuf$(v2) = v1) | ~ (uuf$(v2) = v0)) & ! [v0: % 180.68/24.63 B_update_a_update_fun_bool_fun$] : ! [v1: B_update_a_update_fun_bool_fun$] % 180.68/24.63 : ! [v2: A_update_set$] : (v1 = v0 | ~ (uuy$(v2) = v1) | ~ (uuy$(v2) = v0)) % 180.68/24.63 & ! [v0: C_update_a_update_fun_bool_fun$] : ! [v1: % 180.68/24.63 C_update_a_update_fun_bool_fun$] : ! [v2: A_update_set$] : (v1 = v0 | ~ % 180.68/24.63 (uux$(v2) = v1) | ~ (uux$(v2) = v0)) & ! [v0: % 180.68/24.63 A_update_b_update_fun_bool_fun$] : ! [v1: A_update_b_update_fun_bool_fun$] % 180.68/24.63 : ! [v2: B_update_set$] : (v1 = v0 | ~ (uuw$(v2) = v1) | ~ (uuw$(v2) = v0)) % 180.68/24.63 % 180.68/24.63 Further assumptions not needed in the proof: % 180.68/24.63 -------------------------------------------- % 180.68/24.63 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 180.68/24.63 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 180.68/24.63 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 180.68/24.63 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 180.68/24.63 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 180.68/24.63 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 180.68/24.63 axiom141, axiom142, axiom143, axiom145, axiom146, axiom147, axiom148, axiom149, % 180.68/24.63 axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, % 180.68/24.63 axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, % 180.68/24.63 axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, % 180.68/24.63 axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, % 180.68/24.63 axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, % 180.68/24.63 axiom186, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 180.68/24.63 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 180.68/24.63 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 180.68/24.63 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 180.68/24.63 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 180.68/24.63 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 180.68/24.63 axiom23, axiom230, axiom232, axiom233, axiom234, axiom235, axiom236, axiom237, % 180.68/24.63 axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, axiom244, % 180.68/24.63 axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, axiom251, % 180.68/24.63 axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, % 180.68/24.63 axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, axiom266, % 180.68/24.63 axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, axiom273, % 180.68/24.63 axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, axiom280, % 180.68/24.63 axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, % 180.68/24.63 axiom289, axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, % 180.68/24.63 axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, % 180.68/24.63 axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, % 180.68/24.63 axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, axiom317, % 180.68/24.63 axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, % 180.68/24.63 axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, % 180.68/24.63 axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, % 180.68/24.63 axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, % 180.68/24.63 axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, % 180.68/24.63 axiom354, axiom355, axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, % 180.68/24.63 axiom361, axiom362, axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, % 180.68/24.63 axiom369, axiom37, axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, % 180.68/24.63 axiom376, axiom377, axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, % 180.68/24.63 axiom383, axiom384, axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, % 180.68/24.63 axiom390, axiom391, axiom392, axiom393, axiom394, axiom395, axiom396, axiom397, % 180.68/24.63 axiom398, axiom399, axiom4, axiom40, axiom400, axiom401, axiom402, axiom403, % 180.68/24.63 axiom404, axiom405, axiom406, axiom407, axiom408, axiom409, axiom41, axiom410, % 180.68/24.63 axiom411, axiom412, axiom413, axiom414, axiom415, axiom416, axiom417, axiom418, % 180.68/24.63 axiom419, axiom420, axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, % 180.68/24.63 axiom427, axiom428, axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, % 180.68/24.63 axiom434, axiom435, axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, % 180.68/24.63 axiom441, axiom442, axiom443, axiom444, axiom445, axiom446, axiom447, axiom448, % 180.68/24.63 axiom449, axiom45, axiom450, axiom451, axiom453, axiom454, axiom456, axiom457, % 180.68/24.63 axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, axiom464, % 180.68/24.63 axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, axiom471, % 180.68/24.63 axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, axiom48, % 180.68/24.63 axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, % 180.68/24.63 axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, % 180.68/24.63 axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, % 180.68/24.63 axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, % 180.68/24.63 axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, % 180.68/24.63 axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, % 180.68/24.63 axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, % 180.68/24.63 axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, % 180.68/24.63 axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, % 180.68/24.63 axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, % 180.68/24.63 axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, % 180.68/24.63 axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, % 180.68/24.63 axiom567, axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, % 180.68/24.63 axiom574, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, % 180.68/24.63 axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, % 180.68/24.63 axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, % 180.68/24.63 axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, axiom602, % 180.68/24.63 axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, axiom61, % 180.68/24.63 axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, axiom617, % 180.68/24.63 axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, axiom624, % 180.68/24.63 axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, axiom631, % 180.68/24.63 axiom632, axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, axiom639, % 180.68/24.63 axiom64, axiom640, axiom641, axiom642, axiom643, axiom644, axiom645, axiom646, % 180.68/24.63 axiom647, axiom648, axiom649, axiom65, axiom650, axiom651, axiom652, axiom653, % 180.68/24.63 axiom654, axiom655, axiom656, axiom657, axiom658, axiom659, axiom660, axiom661, % 180.68/24.63 axiom662, axiom663, axiom664, axiom665, axiom666, axiom667, axiom668, axiom7, % 180.68/24.63 axiom70, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, axiom78, % 180.68/24.63 axiom79, axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, % 180.68/24.63 axiom87, axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, % 180.68/24.63 axiom95, axiom96, axiom97, axiom98, axiom99 % 180.68/24.63 % 180.68/24.63 Those formulas are unsatisfiable: % 180.68/24.63 --------------------------------- % 180.68/24.63 % 180.68/24.63 Begin of proof % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom42) implies: % 180.68/24.64 | (1) ? [v0: C_update_a_update_fun_c_update_c_update_fun_fun$] : % 180.68/24.64 | (fun_app$af(comp$d, g$) = v0 & fun_app$ae(v0, g$a) = id$ & % 180.68/24.64 | C_update_a_update_fun_c_update_c_update_fun_fun$(v0)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom66) implies: % 180.68/24.64 | (2) ? [v0: B_update_a_update_fun_b_update_b_update_fun_fun$] : ? [v1: % 180.68/24.64 | B_update_a_update_fun$] : ? [v2: A_update_c_update_fun$] : ? [v3: % 180.68/24.64 | A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v4: % 180.68/24.64 | C_update_a_update_fun_c_update_c_update_fun_fun$] : (comp$k(g$a, v2) % 180.68/24.64 | = id$b & fun_app$ak(comp$e, f$a) = v0 & fun_app$aj(v0, v1) = id$a & % 180.68/24.64 | fun_app$af(comp$d, v2) = v4 & fun_app$ae(v4, g$a) = id$ & % 180.68/24.64 | fun_app$ad(comp$c, v1) = v3 & fun_app$ac(v3, f$a) = id$b & % 180.68/24.64 | C_update_a_update_fun_c_update_c_update_fun_fun$(v4) & % 180.68/24.64 | B_update_a_update_fun_b_update_b_update_fun_fun$(v0) & % 180.68/24.64 | A_update_c_update_fun$(v2) & B_update_a_update_fun$(v1) & % 180.68/24.64 | A_update_b_update_fun_a_update_a_update_fun_fun$(v3) & register$a(v1) % 180.68/24.64 | & register$(v2)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom67) implies: % 180.68/24.64 | (3) ? [v0: B_update_a_update_fun_b_update_b_update_fun_fun$] : % 180.68/24.64 | (fun_app$ak(comp$e, f$a) = v0 & fun_app$aj(v0, f$) = id$a & % 180.68/24.64 | B_update_a_update_fun_b_update_b_update_fun_fun$(v0)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom68) implies: % 180.68/24.64 | (4) comp$k(g$a, g$) = id$b % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom69) implies: % 180.68/24.64 | (5) ? [v0: A_update_b_update_fun_a_update_a_update_fun_fun$] : % 180.68/24.64 | (fun_app$ad(comp$c, f$) = v0 & fun_app$ac(v0, f$a) = id$b & % 180.68/24.64 | A_update_b_update_fun_a_update_a_update_fun_fun$(v0)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom144) implies: % 180.68/24.64 | (6) ! [v0: B_update_c_update_fun$] : ! [v1: A_update_b_update_fun$] : ! % 180.68/24.64 | [v2: A_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : ! % 180.68/24.64 | [v4: C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v5: % 180.68/24.64 | C_update_b_update_fun$] : ! [v6: C_update_c_update_fun$] : ! [v7: % 180.68/24.64 | C_update_a_update_fun_c_update_c_update_fun_fun$] : ! [v8: % 180.68/24.64 | C_update_c_update_fun$] : (v8 = v6 | ~ (comp$(v0, v5) = v6) | ~ % 180.68/24.64 | (fun_app$y(comp$b, v1) = v4) | ~ (fun_app$x(v4, v3) = v5) | ~ % 180.68/24.64 | (fun_app$af(comp$d, v2) = v7) | ~ (fun_app$ae(v7, v3) = v8) | ~ % 180.68/24.64 | C_update_a_update_fun$(v3) | ~ A_update_c_update_fun$(v2) | ~ % 180.68/24.64 | B_update_c_update_fun$(v0) | ~ A_update_b_update_fun$(v1) | ? [v9: % 180.68/24.64 | A_update_c_update_fun$] : ( ~ (v9 = v2) & comp$aj(v0, v1) = v9 & % 180.68/24.64 | A_update_c_update_fun$(v9))) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom187) implies: % 180.68/24.64 | (7) ! [v0: B_update_c_update_fun$] : ! [v1: A_update_b_update_fun$] : ! % 180.68/24.64 | [v2: C_update_a_update_fun$] : ! [v3: % 180.68/24.64 | C_update_a_update_fun_c_update_b_update_fun_fun$] : ! [v4: % 180.68/24.64 | C_update_b_update_fun$] : ! [v5: C_update_c_update_fun$] : ( ~ % 180.68/24.64 | (comp$(v0, v4) = v5) | ~ (fun_app$y(comp$b, v1) = v3) | ~ % 180.68/24.64 | (fun_app$x(v3, v2) = v4) | ~ C_update_a_update_fun$(v2) | ~ % 180.68/24.64 | B_update_c_update_fun$(v0) | ~ A_update_b_update_fun$(v1) | ? [v6: % 180.68/24.64 | A_update_c_update_fun$] : ? [v7: % 180.68/24.64 | C_update_a_update_fun_c_update_c_update_fun_fun$] : (comp$aj(v0, % 180.68/24.64 | v1) = v6 & fun_app$af(comp$d, v6) = v7 & fun_app$ae(v7, v2) = v5 % 180.68/24.64 | & C_update_a_update_fun_c_update_c_update_fun_fun$(v7) & % 180.68/24.64 | C_update_c_update_fun$(v5) & A_update_c_update_fun$(v6))) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom231) implies: % 180.68/24.64 | (8) ! [v0: B_update_a_update_fun$] : ! [v1: A_update_c_update_fun$] : ! % 180.68/24.64 | [v2: B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.68/24.64 | B_update_c_update_fun$] : ( ~ (fun_app$w(comp$a, v1) = v2) | ~ % 180.68/24.64 | (fun_app$v(v2, v0) = v3) | ~ A_update_c_update_fun$(v1) | ~ % 180.68/24.64 | B_update_a_update_fun$(v0) | (fcomp$b(v0, v1) = v3 & % 180.68/24.64 | B_update_c_update_fun$(v3))) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom452) implies: % 180.68/24.64 | (9) ! [v0: C_update_a_update_fun$] : ! [v1: A_update_c_update_fun$] : ! % 180.68/24.64 | [v2: C_update_a_update_fun_c_update_c_update_fun_fun$] : ( ~ % 180.68/24.64 | (fun_app$af(comp$d, v1) = v2) | ~ (fun_app$ae(v2, v0) = id$) | ~ % 180.68/24.64 | C_update_a_update_fun$(v0) | ~ A_update_c_update_fun$(v1) | ? [v3: % 180.68/24.64 | A_update_a_update_fun$] : ? [v4: A_update_c_update_fun$] : ((v4 = % 180.68/24.64 | v1 & inv_into$a(top$a, v0) = v1) | ( ~ (v3 = id$b) & comp$k(v0, % 180.68/24.64 | v1) = v3 & A_update_a_update_fun$(v3)))) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom455) implies: % 180.68/24.64 | (10) ! [v0: A_update_b_update_fun$] : ! [v1: B_update_a_update_fun$] : ! % 180.68/24.64 | [v2: B_update_a_update_fun_b_update_b_update_fun_fun$] : ( ~ % 180.68/24.64 | (fun_app$ak(comp$e, v0) = v2) | ~ (fun_app$aj(v2, v1) = id$a) | ~ % 180.68/24.64 | A_update_b_update_fun$(v0) | ~ B_update_a_update_fun$(v1) | ? [v3: % 180.68/24.64 | A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v4: % 180.68/24.64 | A_update_a_update_fun$] : ? [v5: B_update_a_update_fun$] : ((v5 = % 180.68/24.64 | v1 & inv_into$b(top$, v0) = v1) | ( ~ (v4 = id$b) & % 180.68/24.64 | fun_app$ad(comp$c, v1) = v3 & fun_app$ac(v3, v0) = v4 & % 180.68/24.64 | A_update_a_update_fun$(v4) & % 180.68/24.64 | A_update_b_update_fun_a_update_a_update_fun_fun$(v3)))) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom479) implies: % 180.68/24.64 | (11) ! [v0: A_update_b_update_fun$] : ! [v1: A_update_c_update_fun$] : ! % 180.68/24.64 | [v2: B_update_a_update_fun_b_update_c_update_fun_fun$] : ! [v3: % 180.68/24.64 | B_update_a_update_fun$] : ! [v4: B_update_c_update_fun$] : ! [v5: % 180.68/24.64 | A_update_c_update_fun$] : (v5 = v1 | ~ (inv_into$b(top$, v0) = v3) % 180.68/24.64 | | ~ (comp$aj(v4, v0) = v5) | ~ (fun_app$w(comp$a, v1) = v2) | ~ % 180.68/24.64 | (fun_app$v(v2, v3) = v4) | ~ A_update_c_update_fun$(v1) | ~ % 180.68/24.64 | A_update_b_update_fun$(v0) | ~ inj_on$(v0, top$)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (axiom575) implies: % 180.68/24.64 | (12) ! [v0: A_update_b_update_fun$] : ! [v1: B_update_a_update_fun$] : ! % 180.68/24.64 | [v2: A_update_b_update_fun_a_update_a_update_fun_fun$] : ( ~ % 180.68/24.64 | (inv_into$b(top$, v0) = v1) | ~ (fun_app$ad(comp$c, v1) = v2) | ~ % 180.68/24.64 | (fun_app$ac(v2, v0) = id$b) | ~ A_update_b_update_fun$(v0) | % 180.68/24.64 | inj_on$(v0, top$)) % 180.68/24.64 | % 180.68/24.64 | ALPHA: (conjecture29) implies: % 180.68/24.65 | (13) B_update_a_update_fun$(f$) % 180.68/24.65 | (14) A_update_b_update_fun$(f$a) % 180.68/24.65 | (15) A_update_c_update_fun$(g$) % 180.68/24.65 | (16) C_update_a_update_fun$(g$a) % 180.68/24.65 | (17) ? [v0: B_update_a_update_fun_b_update_c_update_fun_fun$] : ? [v1: % 180.68/24.65 | B_update_c_update_fun$] : ? [v2: % 180.68/24.65 | C_update_a_update_fun_c_update_b_update_fun_fun$] : ? [v3: % 180.68/24.65 | C_update_b_update_fun$] : ? [v4: C_update_c_update_fun$] : ( ~ (v4 % 180.68/24.65 | = id$) & comp$(v1, v3) = v4 & fun_app$y(comp$b, f$a) = v2 & % 180.68/24.65 | fun_app$x(v2, g$a) = v3 & fun_app$w(comp$a, g$) = v0 & fun_app$v(v0, % 180.68/24.65 | f$) = v1 & B_update_a_update_fun_b_update_c_update_fun_fun$(v0) & % 180.68/24.65 | C_update_c_update_fun$(v4) & C_update_b_update_fun$(v3) & % 180.68/24.65 | B_update_c_update_fun$(v1) & % 180.68/24.65 | C_update_a_update_fun_c_update_b_update_fun_fun$(v2)) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (function-axioms) implies: % 180.68/24.65 | (18) ! [v0: A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! % 180.68/24.65 | [v2: A_update_b_update_fun$] : ! [v3: % 180.68/24.65 | A_update_b_update_fun_a_update_a_update_fun_fun$] : (v1 = v0 | ~ % 180.68/24.65 | (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) % 180.68/24.65 | (19) ! [v0: A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v1: % 180.68/24.65 | A_update_b_update_fun_a_update_a_update_fun_fun$] : ! [v2: % 180.68/24.65 | B_update_a_update_fun$] : ! [v3: % 180.68/24.65 | B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$] % 180.68/24.65 | : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ (fun_app$ad(v3, v2) = % 180.68/24.65 | v0)) % 180.68/24.65 | (20) ! [v0: B_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v1: % 180.68/24.65 | B_update_a_update_fun_b_update_b_update_fun_fun$] : ! [v2: % 180.68/24.65 | A_update_b_update_fun$] : ! [v3: % 180.68/24.65 | A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$] % 180.68/24.65 | : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | ~ (fun_app$ak(v3, v2) = % 180.68/24.65 | v0)) % 180.68/24.65 | (21) ! [v0: A_update_a_update_fun$] : ! [v1: A_update_a_update_fun$] : ! % 180.68/24.65 | [v2: A_update_c_update_fun$] : ! [v3: C_update_a_update_fun$] : (v1 = % 180.68/24.65 | v0 | ~ (comp$k(v3, v2) = v1) | ~ (comp$k(v3, v2) = v0)) % 180.68/24.65 | (22) ! [v0: A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! % 180.68/24.65 | [v2: A_update_b_update_fun$] : ! [v3: B_update_c_update_fun$] : (v1 = % 180.68/24.65 | v0 | ~ (comp$aj(v3, v2) = v1) | ~ (comp$aj(v3, v2) = v0)) % 180.68/24.65 | (23) ! [v0: A_update_c_update_fun$] : ! [v1: A_update_c_update_fun$] : ! % 180.68/24.65 | [v2: C_update_a_update_fun$] : ! [v3: C_update_set$] : (v1 = v0 | ~ % 180.68/24.65 | (inv_into$a(v3, v2) = v1) | ~ (inv_into$a(v3, v2) = v0)) % 180.68/24.65 | (24) ! [v0: B_update_a_update_fun$] : ! [v1: B_update_a_update_fun$] : ! % 180.68/24.65 | [v2: A_update_b_update_fun$] : ! [v3: A_update_set$] : (v1 = v0 | ~ % 180.68/24.65 | (inv_into$b(v3, v2) = v1) | ~ (inv_into$b(v3, v2) = v0)) % 180.68/24.65 | % 180.68/24.65 | DELTA: instantiating (5) with fresh symbol all_1020_0 gives: % 180.68/24.65 | (25) fun_app$ad(comp$c, f$) = all_1020_0 & fun_app$ac(all_1020_0, f$a) = % 180.68/24.65 | id$b & A_update_b_update_fun_a_update_a_update_fun_fun$(all_1020_0) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (25) implies: % 180.68/24.65 | (26) fun_app$ac(all_1020_0, f$a) = id$b % 180.68/24.65 | (27) fun_app$ad(comp$c, f$) = all_1020_0 % 180.68/24.65 | % 180.68/24.65 | DELTA: instantiating (1) with fresh symbol all_1030_0 gives: % 180.68/24.65 | (28) fun_app$af(comp$d, g$) = all_1030_0 & fun_app$ae(all_1030_0, g$a) = % 180.68/24.65 | id$ & C_update_a_update_fun_c_update_c_update_fun_fun$(all_1030_0) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (28) implies: % 180.68/24.65 | (29) fun_app$ae(all_1030_0, g$a) = id$ % 180.68/24.65 | (30) fun_app$af(comp$d, g$) = all_1030_0 % 180.68/24.65 | % 180.68/24.65 | DELTA: instantiating (3) with fresh symbol all_1032_0 gives: % 180.68/24.65 | (31) fun_app$ak(comp$e, f$a) = all_1032_0 & fun_app$aj(all_1032_0, f$) = % 180.68/24.65 | id$a & B_update_a_update_fun_b_update_b_update_fun_fun$(all_1032_0) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (31) implies: % 180.68/24.65 | (32) fun_app$aj(all_1032_0, f$) = id$a % 180.68/24.65 | (33) fun_app$ak(comp$e, f$a) = all_1032_0 % 180.68/24.65 | % 180.68/24.65 | DELTA: instantiating (17) with fresh symbols all_1085_0, all_1085_1, % 180.68/24.65 | all_1085_2, all_1085_3, all_1085_4 gives: % 180.68/24.65 | (34) ~ (all_1085_0 = id$) & comp$(all_1085_3, all_1085_1) = all_1085_0 & % 180.68/24.65 | fun_app$y(comp$b, f$a) = all_1085_2 & fun_app$x(all_1085_2, g$a) = % 180.68/24.65 | all_1085_1 & fun_app$w(comp$a, g$) = all_1085_4 & % 180.68/24.65 | fun_app$v(all_1085_4, f$) = all_1085_3 & % 180.68/24.65 | B_update_a_update_fun_b_update_c_update_fun_fun$(all_1085_4) & % 180.68/24.65 | C_update_c_update_fun$(all_1085_0) & % 180.68/24.65 | C_update_b_update_fun$(all_1085_1) & % 180.68/24.65 | B_update_c_update_fun$(all_1085_3) & % 180.68/24.65 | C_update_a_update_fun_c_update_b_update_fun_fun$(all_1085_2) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (34) implies: % 180.68/24.65 | (35) ~ (all_1085_0 = id$) % 180.68/24.65 | (36) fun_app$v(all_1085_4, f$) = all_1085_3 % 180.68/24.65 | (37) fun_app$w(comp$a, g$) = all_1085_4 % 180.68/24.65 | (38) fun_app$x(all_1085_2, g$a) = all_1085_1 % 180.68/24.65 | (39) fun_app$y(comp$b, f$a) = all_1085_2 % 180.68/24.65 | (40) comp$(all_1085_3, all_1085_1) = all_1085_0 % 180.68/24.65 | % 180.68/24.65 | DELTA: instantiating (2) with fresh symbols all_1096_0, all_1096_1, % 180.68/24.65 | all_1096_2, all_1096_3, all_1096_4 gives: % 180.68/24.65 | (41) comp$k(g$a, all_1096_2) = id$b & fun_app$ak(comp$e, f$a) = all_1096_4 % 180.68/24.65 | & fun_app$aj(all_1096_4, all_1096_3) = id$a & fun_app$af(comp$d, % 180.68/24.65 | all_1096_2) = all_1096_0 & fun_app$ae(all_1096_0, g$a) = id$ & % 180.68/24.65 | fun_app$ad(comp$c, all_1096_3) = all_1096_1 & fun_app$ac(all_1096_1, % 180.68/24.65 | f$a) = id$b & % 180.68/24.65 | C_update_a_update_fun_c_update_c_update_fun_fun$(all_1096_0) & % 180.68/24.65 | B_update_a_update_fun_b_update_b_update_fun_fun$(all_1096_4) & % 180.68/24.65 | A_update_c_update_fun$(all_1096_2) & % 180.68/24.65 | B_update_a_update_fun$(all_1096_3) & % 180.68/24.65 | A_update_b_update_fun_a_update_a_update_fun_fun$(all_1096_1) & % 180.68/24.65 | register$a(all_1096_3) & register$(all_1096_2) % 180.68/24.65 | % 180.68/24.65 | ALPHA: (41) implies: % 180.68/24.65 | (42) B_update_a_update_fun$(all_1096_3) % 180.68/24.65 | (43) A_update_c_update_fun$(all_1096_2) % 180.68/24.65 | (44) fun_app$ac(all_1096_1, f$a) = id$b % 180.68/24.65 | (45) fun_app$ad(comp$c, all_1096_3) = all_1096_1 % 180.68/24.65 | (46) fun_app$ae(all_1096_0, g$a) = id$ % 180.68/24.65 | (47) fun_app$af(comp$d, all_1096_2) = all_1096_0 % 180.68/24.65 | (48) fun_app$aj(all_1096_4, all_1096_3) = id$a % 180.68/24.65 | (49) fun_app$ak(comp$e, f$a) = all_1096_4 % 180.68/24.65 | (50) comp$k(g$a, all_1096_2) = id$b % 180.68/24.65 | % 180.68/24.66 | GROUND_INST: instantiating (20) with all_1032_0, all_1096_4, f$a, comp$e, % 180.68/24.66 | simplifying with (33), (49) gives: % 180.68/24.66 | (51) all_1096_4 = all_1032_0 % 180.68/24.66 | % 180.68/24.66 | REDUCE: (48), (51) imply: % 180.68/24.66 | (52) fun_app$aj(all_1032_0, all_1096_3) = id$a % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (9) with g$a, g$, all_1030_0, simplifying with % 180.68/24.66 | (15), (16), (29), (30) gives: % 180.68/24.66 | (53) ? [v0: A_update_a_update_fun$] : ? [v1: A_update_c_update_fun$] : % 180.68/24.66 | ((v1 = g$ & inv_into$a(top$a, g$a) = g$) | ( ~ (v0 = id$b) & % 180.68/24.66 | comp$k(g$a, g$) = v0 & A_update_a_update_fun$(v0))) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (9) with g$a, all_1096_2, all_1096_0, simplifying % 180.68/24.66 | with (16), (43), (46), (47) gives: % 180.68/24.66 | (54) ? [v0: A_update_a_update_fun$] : ? [v1: int] : ((v1 = all_1096_2 & % 180.68/24.66 | inv_into$a(top$a, g$a) = all_1096_2) | ( ~ (v0 = id$b) & % 180.68/24.66 | comp$k(g$a, all_1096_2) = v0 & A_update_a_update_fun$(v0))) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (8) with f$, g$, all_1085_4, all_1085_3, % 180.68/24.66 | simplifying with (13), (15), (36), (37) gives: % 180.68/24.66 | (55) fcomp$b(f$, g$) = all_1085_3 & B_update_c_update_fun$(all_1085_3) % 180.68/24.66 | % 180.68/24.66 | ALPHA: (55) implies: % 180.68/24.66 | (56) B_update_c_update_fun$(all_1085_3) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (10) with f$a, all_1096_3, all_1032_0, simplifying % 180.68/24.66 | with (14), (33), (42), (52) gives: % 180.68/24.66 | (57) ? [v0: A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v1: % 180.68/24.66 | A_update_a_update_fun$] : ? [v2: int] : ((v2 = all_1096_3 & % 180.68/24.66 | inv_into$b(top$, f$a) = all_1096_3) | ( ~ (v1 = id$b) & % 180.68/24.66 | fun_app$ad(comp$c, all_1096_3) = v0 & fun_app$ac(v0, f$a) = v1 & % 180.68/24.66 | A_update_a_update_fun$(v1) & % 180.68/24.66 | A_update_b_update_fun_a_update_a_update_fun_fun$(v0))) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (10) with f$a, f$, all_1032_0, simplifying with % 180.68/24.66 | (13), (14), (32), (33) gives: % 180.68/24.66 | (58) ? [v0: A_update_b_update_fun_a_update_a_update_fun_fun$] : ? [v1: % 180.68/24.66 | A_update_a_update_fun$] : ? [v2: B_update_a_update_fun$] : ((v2 = % 180.68/24.66 | f$ & inv_into$b(top$, f$a) = f$) | ( ~ (v1 = id$b) & % 180.68/24.66 | fun_app$ad(comp$c, f$) = v0 & fun_app$ac(v0, f$a) = v1 & % 180.68/24.66 | A_update_a_update_fun$(v1) & % 180.68/24.66 | A_update_b_update_fun_a_update_a_update_fun_fun$(v0))) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (6) with all_1085_3, f$a, all_1096_2, g$a, % 180.68/24.66 | all_1085_2, all_1085_1, all_1085_0, all_1096_0, id$, simplifying % 180.68/24.66 | with (14), (16), (38), (39), (40), (43), (46), (47), (56) gives: % 180.68/24.66 | (59) all_1085_0 = id$ | ? [v0: any] : ( ~ (v0 = all_1096_2) & % 180.68/24.66 | comp$aj(all_1085_3, f$a) = v0 & A_update_c_update_fun$(v0)) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (6) with all_1085_3, f$a, g$, g$a, all_1085_2, % 180.68/24.66 | all_1085_1, all_1085_0, all_1030_0, id$, simplifying with (14), % 180.68/24.66 | (15), (16), (29), (30), (38), (39), (40), (56) gives: % 180.68/24.66 | (60) all_1085_0 = id$ | ? [v0: A_update_c_update_fun$] : ( ~ (v0 = g$) & % 180.68/24.66 | comp$aj(all_1085_3, f$a) = v0 & A_update_c_update_fun$(v0)) % 180.68/24.66 | % 180.68/24.66 | GROUND_INST: instantiating (7) with all_1085_3, f$a, g$a, all_1085_2, % 180.68/24.66 | all_1085_1, all_1085_0, simplifying with (14), (16), (38), (39), % 180.68/24.66 | (40), (56) gives: % 180.68/24.66 | (61) ? [v0: A_update_c_update_fun$] : ? [v1: % 180.68/24.66 | C_update_a_update_fun_c_update_c_update_fun_fun$] : % 180.68/24.66 | (comp$aj(all_1085_3, f$a) = v0 & fun_app$af(comp$d, v0) = v1 & % 180.68/24.66 | fun_app$ae(v1, g$a) = all_1085_0 & % 180.68/24.66 | C_update_a_update_fun_c_update_c_update_fun_fun$(v1) & % 180.68/24.66 | C_update_c_update_fun$(all_1085_0) & A_update_c_update_fun$(v0)) % 180.68/24.66 | % 180.68/24.66 | DELTA: instantiating (54) with fresh symbols all_1131_0, all_1131_1 gives: % 180.68/24.66 | (62) (all_1131_0 = all_1096_2 & inv_into$a(top$a, g$a) = all_1096_2) | ( ~ % 180.68/24.66 | (all_1131_1 = id$b) & comp$k(g$a, all_1096_2) = all_1131_1 & % 180.68/24.66 | A_update_a_update_fun$(all_1131_1)) % 180.68/24.66 | % 180.68/24.66 | DELTA: instantiating (53) with fresh symbols all_1132_0, all_1132_1 gives: % 180.68/24.66 | (63) (all_1132_0 = g$ & inv_into$a(top$a, g$a) = g$) | ( ~ (all_1132_1 = % 180.68/24.66 | id$b) & comp$k(g$a, g$) = all_1132_1 & % 180.68/24.66 | A_update_a_update_fun$(all_1132_1)) % 180.68/24.66 | % 180.68/24.66 | DELTA: instantiating (61) with fresh symbols all_1175_0, all_1175_1 gives: % 180.68/24.66 | (64) comp$aj(all_1085_3, f$a) = all_1175_1 & fun_app$af(comp$d, all_1175_1) % 180.68/24.66 | = all_1175_0 & fun_app$ae(all_1175_0, g$a) = all_1085_0 & % 180.68/24.66 | C_update_a_update_fun_c_update_c_update_fun_fun$(all_1175_0) & % 180.68/24.66 | C_update_c_update_fun$(all_1085_0) & % 180.68/24.66 | A_update_c_update_fun$(all_1175_1) % 180.68/24.66 | % 180.68/24.66 | ALPHA: (64) implies: % 180.68/24.66 | (65) comp$aj(all_1085_3, f$a) = all_1175_1 % 180.68/24.66 | % 180.68/24.66 | DELTA: instantiating (57) with fresh symbols all_1195_0, all_1195_1, % 180.68/24.66 | all_1195_2 gives: % 180.68/24.66 | (66) (all_1195_0 = all_1096_3 & inv_into$b(top$, f$a) = all_1096_3) | ( ~ % 180.68/24.66 | (all_1195_1 = id$b) & fun_app$ad(comp$c, all_1096_3) = all_1195_2 & % 180.68/24.66 | fun_app$ac(all_1195_2, f$a) = all_1195_1 & % 180.68/24.66 | A_update_a_update_fun$(all_1195_1) & % 180.68/24.66 | A_update_b_update_fun_a_update_a_update_fun_fun$(all_1195_2)) % 180.68/24.66 | % 180.68/24.66 | DELTA: instantiating (58) with fresh symbols all_1197_0, all_1197_1, % 180.68/24.66 | all_1197_2 gives: % 180.68/24.66 | (67) (all_1197_0 = f$ & inv_into$b(top$, f$a) = f$) | ( ~ (all_1197_1 = % 180.68/24.66 | id$b) & fun_app$ad(comp$c, f$) = all_1197_2 & % 180.68/24.67 | fun_app$ac(all_1197_2, f$a) = all_1197_1 & % 180.68/24.67 | A_update_a_update_fun$(all_1197_1) & % 180.68/24.67 | A_update_b_update_fun_a_update_a_update_fun_fun$(all_1197_2)) % 180.68/24.67 | % 180.68/24.67 | BETA: splitting (62) gives: % 180.68/24.67 | % 180.68/24.67 | Case 1: % 180.68/24.67 | | % 180.68/24.67 | | (68) all_1131_0 = all_1096_2 & inv_into$a(top$a, g$a) = all_1096_2 % 180.68/24.67 | | % 180.68/24.67 | | ALPHA: (68) implies: % 180.68/24.67 | | (69) inv_into$a(top$a, g$a) = all_1096_2 % 180.68/24.67 | | % 180.68/24.67 | | BETA: splitting (66) gives: % 180.68/24.67 | | % 180.68/24.67 | | Case 1: % 180.68/24.67 | | | % 180.68/24.67 | | | (70) all_1195_0 = all_1096_3 & inv_into$b(top$, f$a) = all_1096_3 % 180.68/24.67 | | | % 180.68/24.67 | | | ALPHA: (70) implies: % 180.68/24.67 | | | (71) inv_into$b(top$, f$a) = all_1096_3 % 180.68/24.67 | | | % 180.68/24.67 | | | BETA: splitting (63) gives: % 180.68/24.67 | | | % 180.68/24.67 | | | Case 1: % 180.68/24.67 | | | | % 180.68/24.67 | | | | (72) all_1132_0 = g$ & inv_into$a(top$a, g$a) = g$ % 180.68/24.67 | | | | % 180.68/24.67 | | | | ALPHA: (72) implies: % 180.68/24.67 | | | | (73) inv_into$a(top$a, g$a) = g$ % 180.68/24.67 | | | | % 180.68/24.67 | | | | BETA: splitting (60) gives: % 180.68/24.67 | | | | % 180.68/24.67 | | | | Case 1: % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | (74) all_1085_0 = id$ % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | REDUCE: (35), (74) imply: % 180.68/24.67 | | | | | (75) $false % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | CLOSE: (75) is inconsistent. % 180.68/24.67 | | | | | % 180.68/24.67 | | | | Case 2: % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | (76) ? [v0: A_update_c_update_fun$] : ( ~ (v0 = g$) & % 180.68/24.67 | | | | | comp$aj(all_1085_3, f$a) = v0 & A_update_c_update_fun$(v0)) % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | DELTA: instantiating (76) with fresh symbol all_1229_0 gives: % 180.68/24.67 | | | | | (77) ~ (all_1229_0 = g$) & comp$aj(all_1085_3, f$a) = all_1229_0 & % 180.68/24.67 | | | | | A_update_c_update_fun$(all_1229_0) % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | ALPHA: (77) implies: % 180.68/24.67 | | | | | (78) ~ (all_1229_0 = g$) % 180.68/24.67 | | | | | (79) comp$aj(all_1085_3, f$a) = all_1229_0 % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | BETA: splitting (59) gives: % 180.68/24.67 | | | | | % 180.68/24.67 | | | | | Case 1: % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | (80) all_1085_0 = id$ % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | REDUCE: (35), (80) imply: % 180.68/24.67 | | | | | | (81) $false % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | CLOSE: (81) is inconsistent. % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | Case 2: % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | (82) ? [v0: any] : ( ~ (v0 = all_1096_2) & comp$aj(all_1085_3, % 180.68/24.67 | | | | | | f$a) = v0 & A_update_c_update_fun$(v0)) % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | DELTA: instantiating (82) with fresh symbol all_1247_0 gives: % 180.68/24.67 | | | | | | (83) ~ (all_1247_0 = all_1096_2) & comp$aj(all_1085_3, f$a) = % 180.68/24.67 | | | | | | all_1247_0 & A_update_c_update_fun$(all_1247_0) % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | ALPHA: (83) implies: % 180.68/24.67 | | | | | | (84) comp$aj(all_1085_3, f$a) = all_1247_0 % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | BETA: splitting (67) gives: % 180.68/24.67 | | | | | | % 180.68/24.67 | | | | | | Case 1: % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | (85) all_1197_0 = f$ & inv_into$b(top$, f$a) = f$ % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | ALPHA: (85) implies: % 180.68/24.67 | | | | | | | (86) inv_into$b(top$, f$a) = f$ % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (22) with all_1229_0, all_1247_0, f$a, % 180.68/24.67 | | | | | | | all_1085_3, simplifying with (79), (84) gives: % 180.68/24.67 | | | | | | | (87) all_1247_0 = all_1229_0 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (22) with all_1175_1, all_1247_0, f$a, % 180.68/24.67 | | | | | | | all_1085_3, simplifying with (65), (84) gives: % 180.68/24.67 | | | | | | | (88) all_1247_0 = all_1175_1 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (23) with g$, all_1096_2, g$a, top$a, % 180.68/24.67 | | | | | | | simplifying with (69), (73) gives: % 180.68/24.67 | | | | | | | (89) all_1096_2 = g$ % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (24) with f$, all_1096_3, f$a, top$, % 180.68/24.67 | | | | | | | simplifying with (71), (86) gives: % 180.68/24.67 | | | | | | | (90) all_1096_3 = f$ % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | COMBINE_EQS: (87), (88) imply: % 180.68/24.67 | | | | | | | (91) all_1229_0 = all_1175_1 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | SIMP: (91) implies: % 180.68/24.67 | | | | | | | (92) all_1229_0 = all_1175_1 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | REDUCE: (78), (92) imply: % 180.68/24.67 | | | | | | | (93) ~ (all_1175_1 = g$) % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | REDUCE: (45), (90) imply: % 180.68/24.67 | | | | | | | (94) fun_app$ad(comp$c, f$) = all_1096_1 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (19) with all_1020_0, all_1096_1, f$, % 180.68/24.67 | | | | | | | comp$c, simplifying with (27), (94) gives: % 180.68/24.67 | | | | | | | (95) all_1096_1 = all_1020_0 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (12) with f$a, f$, all_1020_0, % 180.68/24.67 | | | | | | | simplifying with (14), (26), (27), (86) gives: % 180.68/24.67 | | | | | | | (96) inj_on$(f$a, top$) % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (11) with f$a, g$, all_1085_4, f$, % 180.68/24.67 | | | | | | | all_1085_3, all_1175_1, simplifying with (14), (15), % 180.68/24.67 | | | | | | | (36), (37), (65), (86), (96) gives: % 180.68/24.67 | | | | | | | (97) all_1175_1 = g$ % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | REDUCE: (93), (97) imply: % 180.68/24.67 | | | | | | | (98) $false % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | CLOSE: (98) is inconsistent. % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | Case 2: % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | (99) ~ (all_1197_1 = id$b) & fun_app$ad(comp$c, f$) = % 180.68/24.67 | | | | | | | all_1197_2 & fun_app$ac(all_1197_2, f$a) = all_1197_1 & % 180.68/24.67 | | | | | | | A_update_a_update_fun$(all_1197_1) & % 180.68/24.67 | | | | | | | A_update_b_update_fun_a_update_a_update_fun_fun$(all_1197_2) % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | ALPHA: (99) implies: % 180.68/24.67 | | | | | | | (100) ~ (all_1197_1 = id$b) % 180.68/24.67 | | | | | | | (101) fun_app$ac(all_1197_2, f$a) = all_1197_1 % 180.68/24.67 | | | | | | | (102) fun_app$ad(comp$c, f$) = all_1197_2 % 180.68/24.67 | | | | | | | % 180.68/24.67 | | | | | | | GROUND_INST: instantiating (19) with all_1020_0, all_1197_2, f$, % 180.68/24.67 | | | | | | | comp$c, simplifying with (27), (102) gives: % 180.68/24.67 | | | | | | | (103) all_1197_2 = all_1020_0 % 180.68/24.67 | | | | | | | % 180.68/24.68 | | | | | | | REDUCE: (101), (103) imply: % 180.68/24.68 | | | | | | | (104) fun_app$ac(all_1020_0, f$a) = all_1197_1 % 180.68/24.68 | | | | | | | % 180.68/24.68 | | | | | | | GROUND_INST: instantiating (18) with id$b, all_1197_1, f$a, % 180.68/24.68 | | | | | | | all_1020_0, simplifying with (26), (104) gives: % 180.68/24.68 | | | | | | | (105) all_1197_1 = id$b % 180.68/24.68 | | | | | | | % 180.68/24.68 | | | | | | | REDUCE: (100), (105) imply: % 180.68/24.68 | | | | | | | (106) $false % 180.68/24.68 | | | | | | | % 180.68/24.68 | | | | | | | CLOSE: (106) is inconsistent. % 180.68/24.68 | | | | | | | % 180.68/24.68 | | | | | | End of split % 180.68/24.68 | | | | | | % 180.68/24.68 | | | | | End of split % 180.68/24.68 | | | | | % 180.68/24.68 | | | | End of split % 180.68/24.68 | | | | % 180.68/24.68 | | | Case 2: % 180.68/24.68 | | | | % 180.68/24.68 | | | | (107) ~ (all_1132_1 = id$b) & comp$k(g$a, g$) = all_1132_1 & % 180.68/24.68 | | | | A_update_a_update_fun$(all_1132_1) % 180.68/24.68 | | | | % 180.68/24.68 | | | | ALPHA: (107) implies: % 180.68/24.68 | | | | (108) ~ (all_1132_1 = id$b) % 180.68/24.68 | | | | (109) comp$k(g$a, g$) = all_1132_1 % 180.68/24.68 | | | | % 180.68/24.68 | | | | GROUND_INST: instantiating (21) with id$b, all_1132_1, g$, g$a, % 180.68/24.68 | | | | simplifying with (4), (109) gives: % 180.68/24.68 | | | | (110) all_1132_1 = id$b % 180.68/24.68 | | | | % 180.68/24.68 | | | | REDUCE: (108), (110) imply: % 180.68/24.68 | | | | (111) $false % 180.68/24.68 | | | | % 180.68/24.68 | | | | CLOSE: (111) is inconsistent. % 180.68/24.68 | | | | % 180.68/24.68 | | | End of split % 180.68/24.68 | | | % 180.68/24.68 | | Case 2: % 180.68/24.68 | | | % 180.68/24.68 | | | (112) ~ (all_1195_1 = id$b) & fun_app$ad(comp$c, all_1096_3) = % 180.68/24.68 | | | all_1195_2 & fun_app$ac(all_1195_2, f$a) = all_1195_1 & % 180.68/24.68 | | | A_update_a_update_fun$(all_1195_1) & % 180.68/24.68 | | | A_update_b_update_fun_a_update_a_update_fun_fun$(all_1195_2) % 180.68/24.68 | | | % 180.68/24.68 | | | ALPHA: (112) implies: % 180.68/24.68 | | | (113) ~ (all_1195_1 = id$b) % 180.68/24.68 | | | (114) fun_app$ac(all_1195_2, f$a) = all_1195_1 % 180.68/24.68 | | | (115) fun_app$ad(comp$c, all_1096_3) = all_1195_2 % 180.68/24.68 | | | % 180.68/24.68 | | | GROUND_INST: instantiating (19) with all_1096_1, all_1195_2, all_1096_3, % 180.68/24.68 | | | comp$c, simplifying with (45), (115) gives: % 180.68/24.68 | | | (116) all_1195_2 = all_1096_1 % 180.68/24.68 | | | % 180.68/24.68 | | | REDUCE: (114), (116) imply: % 180.68/24.68 | | | (117) fun_app$ac(all_1096_1, f$a) = all_1195_1 % 180.68/24.68 | | | % 180.68/24.68 | | | GROUND_INST: instantiating (18) with id$b, all_1195_1, f$a, all_1096_1, % 180.68/24.68 | | | simplifying with (44), (117) gives: % 180.68/24.68 | | | (118) all_1195_1 = id$b % 180.68/24.68 | | | % 180.68/24.68 | | | REDUCE: (113), (118) imply: % 180.68/24.68 | | | (119) $false % 180.68/24.68 | | | % 180.68/24.68 | | | CLOSE: (119) is inconsistent. % 180.68/24.68 | | | % 180.68/24.68 | | End of split % 180.68/24.68 | | % 180.68/24.68 | Case 2: % 180.68/24.68 | | % 180.68/24.68 | | (120) ~ (all_1131_1 = id$b) & comp$k(g$a, all_1096_2) = all_1131_1 & % 180.68/24.68 | | A_update_a_update_fun$(all_1131_1) % 180.68/24.68 | | % 180.68/24.68 | | ALPHA: (120) implies: % 180.68/24.68 | | (121) ~ (all_1131_1 = id$b) % 180.68/24.68 | | (122) comp$k(g$a, all_1096_2) = all_1131_1 % 180.68/24.68 | | % 180.68/24.68 | | GROUND_INST: instantiating (21) with id$b, all_1131_1, all_1096_2, g$a, % 180.68/24.68 | | simplifying with (50), (122) gives: % 180.68/24.68 | | (123) all_1131_1 = id$b % 180.68/24.68 | | % 180.68/24.68 | | REDUCE: (121), (123) imply: % 180.68/24.68 | | (124) $false % 180.68/24.68 | | % 180.68/24.68 | | CLOSE: (124) is inconsistent. % 180.68/24.68 | | % 180.68/24.68 | End of split % 180.68/24.68 | % 180.68/24.68 End of proof % 180.68/24.68 % SZS output end Proof for theBenchmark % 180.68/24.68 % 180.68/24.68 24073ms %------------------------------------------------------------------------------