%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW473_1 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:17 EDT 2023 % Result : Theorem 34.30s 5.41s % Output : Proof 62.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW473_1 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 20:38:11 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.65 ________ _____ % 0.19/0.65 ___ __ \_________(_)________________________________ % 0.19/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.65 % 0.19/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.65 (2023-06-19) % 0.19/0.65 % 0.19/0.65 (c) Philipp Rümmer, 2009-2023 % 0.19/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.65 Amanda Stjerna. % 0.19/0.65 Free software under BSD-3-Clause. % 0.19/0.65 % 0.19/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.65 % 0.19/0.65 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.67 Running up to 7 provers in parallel. % 0.19/0.71 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.71 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.71 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.71 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.71 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.71 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.71 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.35/2.02 Prover 4: Preprocessing ... % 9.35/2.03 Prover 1: Preprocessing ... % 9.81/2.10 Prover 5: Preprocessing ... % 9.81/2.10 Prover 6: Preprocessing ... % 9.81/2.10 Prover 3: Preprocessing ... % 9.81/2.10 Prover 2: Preprocessing ... % 9.81/2.10 Prover 0: Preprocessing ... % 25.98/4.42 Prover 3: Warning: ignoring some quantifiers % 25.98/4.43 Prover 1: Warning: ignoring some quantifiers % 26.54/4.46 Prover 3: Constructing countermodel ... % 26.54/4.49 Prover 1: Constructing countermodel ... % 26.54/4.50 Prover 6: Proving ... % 29.28/4.70 Prover 4: Warning: ignoring some quantifiers % 30.18/4.83 Prover 4: Constructing countermodel ... % 31.52/5.04 Prover 0: Proving ... % 31.52/5.19 Prover 5: Proving ... % 34.30/5.41 Prover 3: proved (4713ms) % 34.30/5.41 % 34.30/5.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.30/5.41 % 34.73/5.43 Prover 0: stopped % 34.96/5.46 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 34.96/5.46 Prover 5: stopped % 34.96/5.47 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 34.96/5.47 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 34.96/5.47 Prover 6: stopped % 34.96/5.48 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 38.39/5.95 Prover 7: Preprocessing ... % 39.50/6.08 Prover 10: Preprocessing ... % 39.50/6.10 Prover 8: Preprocessing ... % 39.50/6.12 Prover 11: Preprocessing ... % 40.68/6.25 Prover 2: Proving ... % 40.68/6.25 Prover 2: stopped % 40.68/6.26 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 43.82/6.66 Prover 13: Preprocessing ... % 45.67/6.92 Prover 10: Warning: ignoring some quantifiers % 46.10/6.95 Prover 8: Warning: ignoring some quantifiers % 46.67/7.05 Prover 8: Constructing countermodel ... % 47.04/7.06 Prover 10: Constructing countermodel ... % 47.04/7.26 Prover 7: Warning: ignoring some quantifiers % 49.03/7.37 Prover 7: Constructing countermodel ... % 50.65/7.58 Prover 11: Warning: ignoring some quantifiers % 50.65/7.62 Prover 13: Warning: ignoring some quantifiers % 51.68/7.71 Prover 11: Constructing countermodel ... % 52.17/7.83 Prover 13: Constructing countermodel ... % 61.79/9.03 Prover 10: Found proof (size 114) % 61.79/9.03 Prover 10: proved (3566ms) % 61.79/9.04 Prover 8: stopped % 61.79/9.04 Prover 4: stopped % 61.79/9.04 Prover 13: stopped % 61.79/9.04 Prover 11: stopped % 61.79/9.04 Prover 1: stopped % 61.79/9.04 Prover 7: stopped % 61.79/9.04 % 61.79/9.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.79/9.04 % 61.79/9.08 % SZS output start Proof for theBenchmark % 62.06/9.10 Assumptions after simplification: % 62.06/9.10 --------------------------------- % 62.06/9.10 % 62.06/9.10 (conj_0) % 62.06/9.12 fun_fu1430349052l_bool(finite_finite_pname) & fun_pname_bool(u) & ? [v0: % 62.06/9.12 bool] : (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & bool(v0) & % 62.06/9.12 hBOOL(v0)) % 62.06/9.12 % 62.06/9.12 (conj_1) % 62.06/9.13 fun_fu1471507361l_bool(ord_le1311769555a_bool) & fun_pname_bool(u) & % 62.06/9.13 fun_pname_a(mgt_call) & fun_a_bool(g) & ? [v0: fun_fun_a_bool_bool] : ? [v1: % 62.06/9.13 fun_a_bool] : ? [v2: bool] : (image_pname_a(mgt_call, u) = v1 & % 62.06/9.13 hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v0 & % 62.06/9.13 hAPP_fun_a_bool_bool(v0, v1) = v2 & fun_fun_a_bool_bool(v0) & fun_a_bool(v1) % 62.06/9.13 & bool(v2) & hBOOL(v2)) % 62.06/9.13 % 62.06/9.13 (conj_2) % 62.06/9.13 fun_fun_a_bool_nat(finite_card_a) & fun_nat_fun_nat_bool(ord_less_eq_nat) & % 62.06/9.13 fun_nat_nat(suc) & fun_pname_bool(u) & fun_pname_a(mgt_call) & nat(na) & ? % 62.06/9.13 [v0: nat] : ? [v1: fun_nat_bool] : ? [v2: fun_a_bool] : ? [v3: nat] : ? % 62.06/9.13 [v4: bool] : (hAPP_nat_nat(suc, na) = v0 & hAPP_fun_a_bool_nat(finite_card_a, % 62.06/9.13 v2) = v3 & hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & % 62.06/9.13 hAPP_nat_bool(v1, v3) = v4 & image_pname_a(mgt_call, u) = v2 & % 62.06/9.13 fun_nat_bool(v1) & fun_a_bool(v2) & nat(v3) & nat(v0) & bool(v4) & % 62.06/9.13 hBOOL(v4)) % 62.06/9.13 % 62.06/9.13 (conj_3) % 62.06/9.13 fun_fun_a_bool_nat(finite_card_a) & fun_nat_nat(suc) & fun_pname_bool(u) & % 62.06/9.13 fun_pname_a(mgt_call) & fun_a_bool(g) & nat(na) & ? [v0: nat] : ? [v1: % 62.06/9.13 fun_a_bool] : ? [v2: nat] : ? [v3: fun_nat_nat] : ? [v4: nat] : % 62.06/9.13 (minus_minus_nat(v2) = v3 & hAPP_nat_nat(v3, v4) = v0 & hAPP_nat_nat(suc, na) % 62.06/9.13 = v4 & hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 62.06/9.13 hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & image_pname_a(mgt_call, u) = v1 % 62.06/9.13 & fun_nat_nat(v3) & fun_a_bool(v1) & nat(v4) & nat(v2) & nat(v0)) % 62.06/9.13 % 62.06/9.13 (conj_4) % 62.06/9.13 fun_pn422929397l_bool(member_pname) & fun_pname_bool(u) & pname(pn) & ? [v0: % 62.06/9.13 fun_fu1430349052l_bool] : ? [v1: bool] : % 62.06/9.13 (hAPP_p338031245l_bool(member_pname, pn) = v0 & hAPP_f1664156314l_bool(v0, u) % 62.06/9.13 = v1 & fun_fu1430349052l_bool(v0) & bool(v1) & hBOOL(v1)) % 62.06/9.13 % 62.06/9.13 (conj_5) % 62.06/9.13 fun_pname_a(mgt_call) & fun_a_1255737515l_bool(member_a) & fun_a_bool(g) & % 62.06/9.13 pname(pn) & ? [v0: x_a] : ? [v1: fun_fun_a_bool_bool] : ? [v2: bool] : % 62.06/9.13 (hAPP_pname_a(mgt_call, pn) = v0 & hAPP_a85458249l_bool(member_a, v0) = v1 & % 62.06/9.13 hAPP_fun_a_bool_bool(v1, g) = v2 & fun_fun_a_bool_bool(v1) & bool(v2) & % 62.06/9.13 x_a(v0) & ~ hBOOL(v2)) % 62.06/9.13 % 62.06/9.13 (conj_6) % 62.06/9.13 fun_fu1471507361l_bool(ord_le1311769555a_bool) & fun_pname_bool(u) & % 62.06/9.13 fun_pname_a(mgt_call) & fun_a_bool(g) & pname(pn) & ? [v0: x_a] : ? [v1: % 62.06/9.13 fun_a_bool] : ? [v2: fun_fun_a_bool_bool] : ? [v3: fun_a_bool] : ? [v4: % 62.06/9.13 bool] : (hAPP_pname_a(mgt_call, pn) = v0 & insert_a(v0, g) = v1 & % 62.06/9.13 image_pname_a(mgt_call, u) = v3 & % 62.06/9.13 hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 62.06/9.13 hAPP_fun_a_bool_bool(v2, v3) = v4 & fun_fun_a_bool_bool(v2) & fun_a_bool(v3) % 62.06/9.13 & fun_a_bool(v1) & bool(v4) & x_a(v0) & ~ hBOOL(v4)) % 62.06/9.13 % 62.06/9.13 (fact_102_card__insert__if) % 62.06/9.14 fun_fu1668467777ol_nat(finite_card_pname) & % 62.06/9.14 fun_fu1430349052l_bool(finite_finite_pname) & fun_nat_nat(suc) & % 62.06/9.14 fun_pn422929397l_bool(member_pname) & ! [v0: pname] : ! [v1: fun_pname_bool] % 62.06/9.14 : ! [v2: fun_fu1430349052l_bool] : ! [v3: bool] : ( ~ % 62.06/9.14 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ % 62.06/9.14 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ fun_pname_bool(v1) | ~ pname(v0) % 62.06/9.14 | ? [v4: bool] : ? [v5: fun_pname_bool] : ? [v6: nat] : ? [v7: nat] : ? % 62.06/9.14 [v8: nat] : ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & % 62.06/9.14 bool(v4) & ~ hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 62.06/9.14 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 62.06/9.14 hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & insert_pname(v0, % 62.06/9.14 v1) = v5 & fun_pname_bool(v5) & nat(v6))) & (hBOOL(v3) | (v8 = v6 % 62.06/9.14 & hAPP_nat_nat(suc, v7) = v6 & % 62.06/9.14 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 62.06/9.14 hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & insert_pname(v0, % 62.06/9.14 v1) = v5 & fun_pname_bool(v5) & nat(v7) & nat(v6)))))) % 62.06/9.14 % 62.06/9.14 (fact_169_finite__surj) % 62.06/9.14 fun_fu1430349052l_bool(finite_finite_pname) & % 62.06/9.14 fun_fu1471507361l_bool(ord_le1311769555a_bool) & % 62.06/9.14 fun_fun_a_bool_bool(finite_finite_a) & ! [v0: fun_a_bool] : ! [v1: % 62.06/9.14 fun_pname_a] : ! [v2: fun_pname_bool] : ! [v3: fun_fun_a_bool_bool] : ! % 62.06/9.14 [v4: fun_a_bool] : ! [v5: bool] : ( ~ (image_pname_a(v1, v2) = v4) | ~ % 62.06/9.14 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = v3) | ~ % 62.06/9.14 (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ fun_pname_bool(v2) | ~ % 62.06/9.14 fun_pname_a(v1) | ~ fun_a_bool(v0) | ~ hBOOL(v5) | ? [v6: bool] : ? [v7: % 62.06/9.14 bool] : ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 & bool(v6) % 62.06/9.14 & ~ hBOOL(v6)) | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & % 62.06/9.14 bool(v7) & hBOOL(v7)))) % 62.06/9.14 % 62.06/9.14 (fact_170_finite__subset__image) % 62.06/9.14 fun_fu802393907l_bool(ord_le313189616e_bool) & % 62.06/9.14 fun_fu1430349052l_bool(finite_finite_pname) & % 62.06/9.14 fun_fu1471507361l_bool(ord_le1311769555a_bool) & % 62.06/9.14 fun_fun_a_bool_bool(finite_finite_a) & ! [v0: fun_pname_a] : ! [v1: % 62.06/9.14 fun_pname_bool] : ! [v2: fun_a_bool] : ! [v3: fun_fun_a_bool_bool] : ! % 62.06/9.14 [v4: fun_a_bool] : ! [v5: bool] : ( ~ (image_pname_a(v0, v1) = v4) | ~ % 62.06/9.14 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v2) = v3) | ~ % 62.06/9.14 (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ fun_pname_bool(v1) | ~ % 62.06/9.14 fun_pname_a(v0) | ~ fun_a_bool(v2) | ~ hBOOL(v5) | ? [v6: bool] : ? [v7: % 62.06/9.14 fun_pname_bool] : ? [v8: fun_fu1430349052l_bool] : ? [v9: bool] : ? % 62.06/9.14 [v10: bool] : ? [v11: fun_a_bool] : (fun_pname_bool(v7) & ((v11 = v2 & % 62.06/9.14 image_pname_a(v0, v7) = v2 & % 62.06/9.14 hAPP_f434788991l_bool(ord_le313189616e_bool, v7) = v8 & % 62.06/9.14 hAPP_f1664156314l_bool(v8, v1) = v9 & % 62.06/9.14 hAPP_f1664156314l_bool(finite_finite_pname, v7) = v10 & % 62.06/9.14 fun_fu1430349052l_bool(v8) & bool(v10) & bool(v9) & hBOOL(v10) & % 62.06/9.14 hBOOL(v9)) | (hAPP_fun_a_bool_bool(finite_finite_a, v2) = v6 & % 62.06/9.14 bool(v6) & ~ hBOOL(v6))))) % 62.06/9.14 % 62.06/9.14 (fact_176_image__eqI) % 62.06/9.14 fun_pn422929397l_bool(member_pname) & fun_a_1255737515l_bool(member_a) & ! % 62.06/9.14 [v0: fun_pname_bool] : ! [v1: x_a] : ! [v2: fun_pname_a] : ! [v3: pname] : % 62.06/9.14 ! [v4: fun_fu1430349052l_bool] : ! [v5: bool] : ! [v6: fun_fun_a_bool_bool] % 62.06/9.14 : ! [v7: fun_a_bool] : ! [v8: bool] : ( ~ (hAPP_a85458249l_bool(member_a, % 62.06/9.14 v1) = v6) | ~ (hAPP_p338031245l_bool(member_pname, v3) = v4) | ~ % 62.06/9.14 (image_pname_a(v2, v0) = v7) | ~ (hAPP_f1664156314l_bool(v4, v0) = v5) | ~ % 62.06/9.14 (hAPP_fun_a_bool_bool(v6, v7) = v8) | ~ fun_pname_bool(v0) | ~ % 62.06/9.14 fun_pname_a(v2) | ~ pname(v3) | ~ x_a(v1) | ~ hBOOL(v5) | hBOOL(v8) | ? % 62.06/9.14 [v9: x_a] : ( ~ (v9 = v1) & hAPP_pname_a(v2, v3) = v9 & x_a(v9))) % 62.06/9.14 % 62.06/9.14 (fact_223_insert__absorb) % 62.06/9.14 fun_pn422929397l_bool(member_pname) & ! [v0: pname] : ! [v1: fun_pname_bool] % 62.06/9.14 : ! [v2: fun_fu1430349052l_bool] : ! [v3: bool] : ( ~ % 62.06/9.14 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ % 62.06/9.14 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ fun_pname_bool(v1) | ~ pname(v0) % 62.06/9.14 | ~ hBOOL(v3) | insert_pname(v0, v1) = v1) % 62.06/9.14 % 62.06/9.14 (fact_274_insert__subset) % 62.06/9.15 fun_fu1471507361l_bool(ord_le1311769555a_bool) & % 62.06/9.15 fun_a_1255737515l_bool(member_a) & ! [v0: x_a] : ! [v1: fun_a_bool] : ! % 62.06/9.15 [v2: fun_a_bool] : ! [v3: fun_a_bool] : ! [v4: fun_fun_a_bool_bool] : ! % 62.06/9.15 [v5: bool] : ( ~ (insert_a(v0, v1) = v3) | ~ % 62.06/9.15 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 62.06/9.15 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ fun_a_bool(v2) | ~ fun_a_bool(v1) % 62.06/9.15 | ~ x_a(v0) | ~ hBOOL(v5) | ? [v6: fun_fun_a_bool_bool] : ? [v7: bool] : % 62.06/9.15 ? [v8: fun_fun_a_bool_bool] : ? [v9: bool] : % 62.06/9.15 (hAPP_a85458249l_bool(member_a, v0) = v6 & % 62.06/9.15 hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v8 & % 62.06/9.15 hAPP_fun_a_bool_bool(v8, v2) = v9 & hAPP_fun_a_bool_bool(v6, v2) = v7 & % 62.06/9.15 fun_fun_a_bool_bool(v8) & fun_fun_a_bool_bool(v6) & bool(v9) & bool(v7) & % 62.06/9.15 hBOOL(v9) & hBOOL(v7))) & ! [v0: x_a] : ! [v1: fun_a_bool] : ! [v2: % 62.06/9.15 fun_a_bool] : ! [v3: fun_a_bool] : ! [v4: fun_fun_a_bool_bool] : ! [v5: % 62.06/9.15 bool] : ( ~ (insert_a(v0, v1) = v3) | ~ % 62.06/9.15 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 62.06/9.15 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ fun_a_bool(v2) | ~ fun_a_bool(v1) % 62.06/9.15 | ~ x_a(v0) | hBOOL(v5) | ? [v6: fun_fun_a_bool_bool] : ? [v7: bool] : ? % 62.06/9.15 [v8: fun_fun_a_bool_bool] : ? [v9: bool] : ((hAPP_a85458249l_bool(member_a, % 62.06/9.15 v0) = v6 & hAPP_fun_a_bool_bool(v6, v2) = v7 & fun_fun_a_bool_bool(v6) % 62.06/9.15 & bool(v7) & ~ hBOOL(v7)) | % 62.06/9.15 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v8 & % 62.06/9.15 hAPP_fun_a_bool_bool(v8, v2) = v9 & fun_fun_a_bool_bool(v8) & bool(v9) & % 62.06/9.15 ~ hBOOL(v9)))) % 62.06/9.15 % 62.06/9.15 (fact_290_subsetI) % 62.37/9.15 fun_fu1471507361l_bool(ord_le1311769555a_bool) & % 62.37/9.15 fun_a_1255737515l_bool(member_a) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : % 62.37/9.15 ! [v2: fun_fun_a_bool_bool] : ! [v3: bool] : ( ~ % 62.37/9.15 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2) | ~ % 62.37/9.15 (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ fun_a_bool(v1) | ~ fun_a_bool(v0) % 62.37/9.15 | hBOOL(v3) | ? [v4: x_a] : ? [v5: fun_fun_a_bool_bool] : ? [v6: bool] : % 62.37/9.15 ? [v7: bool] : (hAPP_a85458249l_bool(member_a, v4) = v5 & % 62.37/9.15 hAPP_fun_a_bool_bool(v5, v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = v7 & % 62.37/9.15 fun_fun_a_bool_bool(v5) & bool(v7) & bool(v6) & x_a(v4) & hBOOL(v6) & ~ % 62.37/9.15 hBOOL(v7))) % 62.37/9.15 % 62.37/9.15 (function-axioms) % 62.44/9.19 ! [v0: fun_bool_bool] : ! [v1: fun_bool_bool] : ! [v2: fun_pname_bool] : ! % 62.44/9.19 [v3: fun_fu31783638l_bool] : (v1 = v0 | ~ (hAPP_f1476298914l_bool(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_f1476298914l_bool(v3, v2) = v0)) & ! [v0: fun_bool_bool] : % 62.44/9.19 ! [v1: fun_bool_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_fu1016514960l_bool] : (v1 = v0 | ~ (hAPP_f1748468828l_bool(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_f1748468828l_bool(v3, v2) = v0)) & ! [v0: fun_bool_bool] : % 62.44/9.19 ! [v1: fun_bool_bool] : ! [v2: fun_a_bool] : ! [v3: fun_fu554186387l_bool] % 62.44/9.19 : (v1 = v0 | ~ (hAPP_f198738859l_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_f198738859l_bool(v3, v2) = v0)) & ! [v0: fun_bool_bool] : ! [v1: % 62.44/9.19 fun_bool_bool] : ! [v2: pname] : ! [v3: fun_pn250273176l_bool] : (v1 = v0 % 62.44/9.19 | ~ (hAPP_p393069232l_bool(v3, v2) = v1) | ~ (hAPP_p393069232l_bool(v3, % 62.44/9.19 v2) = v0)) & ! [v0: fun_bool_bool] : ! [v1: fun_bool_bool] : ! [v2: % 62.44/9.19 nat] : ! [v3: fun_na1469252690l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_n1006566506l_bool(v3, v2) = v1) | ~ (hAPP_n1006566506l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: pname] : ! % 62.44/9.19 [v3: fun_pname_fun_a_bool] : (v1 = v0 | ~ (hAPP_p1534023578a_bool(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_p1534023578a_bool(v3, v2) = v0)) & ! [v0: fun_bool_bool] : % 62.44/9.19 ! [v1: fun_bool_bool] : ! [v2: x_a] : ! [v3: fun_a_fun_bool_bool] : (v1 = % 62.44/9.19 v0 | ~ (hAPP_a_fun_bool_bool(v3, v2) = v1) | ~ (hAPP_a_fun_bool_bool(v3, % 62.44/9.19 v2) = v0)) & ! [v0: fun_bool_bool] : ! [v1: fun_bool_bool] : ! [v2: % 62.44/9.19 bool] : ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_b589554111l_bool(v3, v2) = v1) | ~ (hAPP_b589554111l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: bool] : ! [v3: % 62.44/9.19 fun_bool_bool] : (v1 = v0 | ~ (hAPP_bool_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_bool_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: % 62.44/9.19 x_a] : ! [v3: fun_a_bool] : (v1 = v0 | ~ (hAPP_a_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_a_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: pname] % 62.44/9.19 : ! [v3: fun_pname_bool] : (v1 = v0 | ~ (hAPP_pname_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_pname_bool(v3, v2) = v0)) & ! [v0: fun_fun_a_bool_bool] : ! [v1: % 62.44/9.19 fun_fun_a_bool_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: fun_bool_bool] % 62.44/9.19 : (v1 = v0 | ~ (cOMBB_2140588453a_bool(v3, v2) = v1) | ~ % 62.44/9.19 (cOMBB_2140588453a_bool(v3, v2) = v0)) & ! [v0: fun_fu1430349052l_bool] : % 62.44/9.19 ! [v1: fun_fu1430349052l_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.19 fun_bool_bool] : (v1 = v0 | ~ (cOMBB_307249310e_bool(v3, v2) = v1) | ~ % 62.44/9.19 (cOMBB_307249310e_bool(v3, v2) = v0)) & ! [v0: fun_fu425979586l_bool] : ! % 62.44/9.19 [v1: fun_fu425979586l_bool] : ! [v2: fun_fu425979586l_bool] : ! [v3: % 62.44/9.19 fun_bool_bool] : (v1 = v0 | ~ (cOMBB_238756964t_bool(v3, v2) = v1) | ~ % 62.44/9.19 (cOMBB_238756964t_bool(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_a_bool] : ! [v3: fun_bool_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBB_bool_bool_a(v3, v2) = v1) | ~ (cOMBB_bool_bool_a(v3, v2) = v0)) & ! % 62.44/9.19 [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: fun_pname_bool] : ! % 62.44/9.19 [v3: fun_bool_bool] : (v1 = v0 | ~ (cOMBB_647938656_pname(v3, v2) = v1) | ~ % 62.44/9.19 (cOMBB_647938656_pname(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: % 62.44/9.19 fun_nat_bool] : ! [v2: fun_nat_bool] : ! [v3: fun_bool_bool] : (v1 = v0 | % 62.44/9.19 ~ (cOMBB_bool_bool_nat(v3, v2) = v1) | ~ (cOMBB_bool_bool_nat(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! % 62.44/9.19 [v2: fun_fun_a_bool_bool] : ! [v3: fun_fu911136611l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f2117159681l_bool(v3, v2) = v1) | ~ (hAPP_f2117159681l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu1430349052l_bool] : ! [v1: fun_fu1430349052l_bool] : % 62.44/9.19 ! [v2: fun_fu1430349052l_bool] : ! [v3: fun_fu2087345469l_bool] : (v1 = v0 | % 62.44/9.19 ~ (hAPP_f559147733l_bool(v3, v2) = v1) | ~ (hAPP_f559147733l_bool(v3, v2) % 62.44/9.19 = v0)) & ! [v0: fun_fu425979586l_bool] : ! [v1: fun_fu425979586l_bool] : % 62.44/9.19 ! [v2: fun_fu425979586l_bool] : ! [v3: fun_fu616551101l_bool] : (v1 = v0 | % 62.44/9.19 ~ (hAPP_f1246832597l_bool(v3, v2) = v1) | ~ (hAPP_f1246832597l_bool(v3, v2) % 62.44/9.19 = v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: x_a] : ! % 62.44/9.19 [v3: fun_a_fun_a_bool] : (v1 = v0 | ~ (hAPP_a_fun_a_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_a_fun_a_bool(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_a_bool] : ! [v3: fun_fu1731003005a_bool] : (v1 = % 62.44/9.19 v0 | ~ (hAPP_f2050579477a_bool(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_f2050579477a_bool(v3, v2) = v0)) & ! [v0: fun_pname_bool] : ! [v1: % 62.44/9.19 fun_pname_bool] : ! [v2: pname] : ! [v3: fun_pn800050071e_bool] : (v1 = v0 % 62.44/9.19 | ~ (hAPP_p61793385e_bool(v3, v2) = v1) | ~ (hAPP_p61793385e_bool(v3, v2) % 62.44/9.19 = v0)) & ! [v0: fun_nat_bool] : ! [v1: fun_nat_bool] : ! [v2: % 62.44/9.19 fun_nat_bool] : ! [v3: fun_fu821463397t_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f800510211t_bool(v3, v2) = v1) | ~ (hAPP_f800510211t_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: % 62.44/9.19 fun_pname_bool] : ! [v3: fun_fu410713561e_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f759274231e_bool(v3, v2) = v1) | ~ (hAPP_f759274231e_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_pname_fun_a_bool] : ! [v1: fun_pname_fun_a_bool] : ! % 62.44/9.19 [v2: fun_pname_a] : ! [v3: fun_a_fun_a_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBB_1897541054_pname(v3, v2) = v1) | ~ (cOMBB_1897541054_pname(v3, v2) = % 62.44/9.19 v0)) & ! [v0: x_a] : ! [v1: x_a] : ! [v2: pname] : ! [v3: fun_pname_a] % 62.44/9.19 : (v1 = v0 | ~ (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, v2) = v0)) % 62.44/9.19 & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: x_a] : ! [v3: % 62.44/9.19 fun_a_fun_pname_bool] : (v1 = v0 | ~ (hAPP_a93125764e_bool(v3, v2) = v1) | % 62.44/9.19 ~ (hAPP_a93125764e_bool(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: nat] : ! [v3: fun_nat_fun_a_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_nat_fun_a_bool(v3, v2) = v1) | ~ (hAPP_nat_fun_a_bool(v3, v2) = v0)) % 62.44/9.19 & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: nat] : ! [v3: % 62.44/9.19 fun_na936072029e_bool] : (v1 = v0 | ~ (hAPP_n1025906991e_bool(v3, v2) = v1) % 62.44/9.19 | ~ (hAPP_n1025906991e_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_na1469252690l_bool] : ! [v1: fun_na1469252690l_bool] : ! [v2: % 62.44/9.19 fun_nat_bool] : ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBB_1015721476ol_nat(v3, v2) = v1) | ~ (cOMBB_1015721476ol_nat(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_nat_bool] : ! [v1: fun_nat_bool] : ! [v2: % 62.44/9.19 fun_nat_bool] : ! [v3: fun_na1469252690l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBS_nat_bool_bool(v3, v2) = v1) | ~ (cOMBS_nat_bool_bool(v3, v2) = v0)) % 62.44/9.19 & ! [v0: fun_pn250273176l_bool] : ! [v1: fun_pn250273176l_bool] : ! [v2: % 62.44/9.19 fun_pname_bool] : ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBB_675860798_pname(v3, v2) = v1) | ~ (cOMBB_675860798_pname(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: % 62.44/9.19 fun_pname_bool] : ! [v3: fun_pn250273176l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBS_568398431l_bool(v3, v2) = v1) | ~ (cOMBS_568398431l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_a_fun_bool_bool] : ! [v1: fun_a_fun_bool_bool] : ! % 62.44/9.19 [v2: fun_a_bool] : ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBB_1972296269bool_a(v3, v2) = v1) | ~ (cOMBB_1972296269bool_a(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_a_bool] : % 62.44/9.19 ! [v3: fun_a_fun_bool_bool] : (v1 = v0 | ~ (cOMBS_a_bool_bool(v3, v2) = v1) | % 62.44/9.19 ~ (cOMBS_a_bool_bool(v3, v2) = v0)) & ! [v0: fun_fu554186387l_bool] : ! % 62.44/9.19 [v1: fun_fu554186387l_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: % 62.44/9.19 fun_bo1549164019l_bool] : (v1 = v0 | ~ (cOMBB_338059395a_bool(v3, v2) = v1) % 62.44/9.19 | ~ (cOMBB_338059395a_bool(v3, v2) = v0)) & ! [v0: fun_fun_a_bool_bool] : % 62.44/9.19 ! [v1: fun_fun_a_bool_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: % 62.44/9.19 fun_fu554186387l_bool] : (v1 = v0 | ~ (cOMBS_1035972772l_bool(v3, v2) = v1) % 62.44/9.19 | ~ (cOMBS_1035972772l_bool(v3, v2) = v0)) & ! [v0: fun_fu31783638l_bool] % 62.44/9.19 : ! [v1: fun_fu31783638l_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.19 fun_bo1549164019l_bool] : (v1 = v0 | ~ (cOMBB_2095475776e_bool(v3, v2) = % 62.44/9.19 v1) | ~ (cOMBB_2095475776e_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_fu1430349052l_bool] : ! [v1: fun_fu1430349052l_bool] : ! [v2: % 62.44/9.19 fun_fu1430349052l_bool] : ! [v3: fun_fu31783638l_bool] : (v1 = v0 | ~ % 62.44/9.19 (cOMBS_350070575l_bool(v3, v2) = v1) | ~ (cOMBS_350070575l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu1016514960l_bool] : ! [v1: fun_fu1016514960l_bool] : % 62.44/9.19 ! [v2: fun_fu425979586l_bool] : ! [v3: fun_bo1549164019l_bool] : (v1 = v0 | % 62.44/9.19 ~ (cOMBB_444170502t_bool(v3, v2) = v1) | ~ (cOMBB_444170502t_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu425979586l_bool] : ! [v1: fun_fu425979586l_bool] : % 62.44/9.19 ! [v2: fun_fu425979586l_bool] : ! [v3: fun_fu1016514960l_bool] : (v1 = v0 | % 62.44/9.19 ~ (cOMBS_1187019125l_bool(v3, v2) = v1) | ~ (cOMBS_1187019125l_bool(v3, v2) % 62.44/9.19 = v0)) & ! [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! % 62.44/9.19 [v2: x_a] : ! [v3: fun_a_1255737515l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu1430349052l_bool] : ! [v1: fun_fu1430349052l_bool] : % 62.44/9.19 ! [v2: pname] : ! [v3: fun_pn422929397l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_p338031245l_bool(v3, v2) = v1) | ~ (hAPP_p338031245l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu425979586l_bool] : ! [v1: fun_fu425979586l_bool] : % 62.44/9.19 ! [v2: nat] : ! [v3: fun_na1436237685l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_n215258509l_bool(v3, v2) = v1) | ~ (hAPP_n215258509l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu885608257l_bool] : ! [v1: fun_fu885608257l_bool] : % 62.44/9.19 ! [v2: fun_a_bool] : ! [v3: fun_fu386216885l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f285962445l_bool(v3, v2) = v1) | ~ (hAPP_f285962445l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu399576434l_bool] : ! [v1: fun_fu399576434l_bool] : % 62.44/9.19 ! [v2: fun_pname_bool] : ! [v3: fun_fu931343505l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f556039215l_bool(v3, v2) = v1) | ~ (hAPP_f556039215l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu814369080l_bool] : ! [v1: fun_fu814369080l_bool] : % 62.44/9.19 ! [v2: fun_nat_bool] : ! [v3: fun_fu1436348701l_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f1951378235l_bool(v3, v2) = v1) | ~ (hAPP_f1951378235l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: nat] : ! [v1: nat] : ! [v2: nat] : ! [v3: fun_nat_nat] : % 62.44/9.19 (v1 = v0 | ~ (hAPP_nat_nat(v3, v2) = v1) | ~ (hAPP_nat_nat(v3, v2) = v0)) & % 62.44/9.19 ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_fu885608257l_bool] : ! % 62.44/9.19 [v3: fun_fu1373417771bool_a] : (v1 = v0 | ~ (image_573985017bool_a(v3, v2) = % 62.44/9.19 v1) | ~ (image_573985017bool_a(v3, v2) = v0)) & ! [v0: nat] : ! [v1: % 62.44/9.19 nat] : ! [v2: fun_fu885608257l_bool] : ! [v3: fun_fu48515398ol_nat] : (v1 % 62.44/9.19 = v0 | ~ (hAPP_f1253658590ol_nat(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_f1253658590ol_nat(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: % 62.44/9.19 fun_fu2061654492bool_a] : (v1 = v0 | ~ (image_349102846bool_a(v3, v2) = v1) % 62.44/9.19 | ~ (image_349102846bool_a(v3, v2) = v0)) & ! [v0: nat] : ! [v1: nat] : % 62.44/9.19 ! [v2: fun_fu399576434l_bool] : ! [v3: fun_fu1701008009ol_nat] : (v1 = v0 | % 62.44/9.19 ~ (hAPP_f98387925ol_nat(v3, v2) = v1) | ~ (hAPP_f98387925ol_nat(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: % 62.44/9.19 fun_fu814369080l_bool] : ! [v3: fun_fu897950882bool_a] : (v1 = v0 | ~ % 62.44/9.19 (image_526090948bool_a(v3, v2) = v1) | ~ (image_526090948bool_a(v3, v2) = % 62.44/9.19 v0)) & ! [v0: nat] : ! [v1: nat] : ! [v2: fun_fu814369080l_bool] : ! % 62.44/9.19 [v3: fun_fu1297083715ol_nat] : (v1 = v0 | ~ (hAPP_f1690079119ol_nat(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_f1690079119ol_nat(v3, v2) = v0)) & ! [v0: nat] : ! [v1: % 62.44/9.19 nat] : ! [v2: fun_fun_a_bool_bool] : ! [v3: fun_fu2020802748ol_nat] : (v1 % 62.44/9.19 = v0 | ~ (hAPP_f2009550088ol_nat(v3, v2) = v1) | ~ % 62.44/9.19 (hAPP_f2009550088ol_nat(v3, v2) = v0)) & ! [v0: nat] : ! [v1: nat] : ! % 62.44/9.19 [v2: fun_fu1430349052l_bool] : ! [v3: fun_fu1730389579ol_nat] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_f55526627ol_nat(v3, v2) = v1) | ~ (hAPP_f55526627ol_nat(v3, v2) = % 62.44/9.19 v0)) & ! [v0: nat] : ! [v1: nat] : ! [v2: fun_fu425979586l_bool] : ! % 62.44/9.19 [v3: fun_fu411113733ol_nat] : (v1 = v0 | ~ (hAPP_f696928925ol_nat(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_f696928925ol_nat(v3, v2) = v0)) & ! [v0: nat] : ! [v1: % 62.44/9.19 nat] : ! [v2: fun_a_bool] : ! [v3: fun_fun_a_bool_nat] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_fun_a_bool_nat(v3, v2) = v1) | ~ (hAPP_fun_a_bool_nat(v3, v2) = v0)) % 62.44/9.19 & ! [v0: nat] : ! [v1: nat] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_fun_nat_bool_nat] : (v1 = v0 | ~ (hAPP_f22106695ol_nat(v3, v2) = v1) | % 62.44/9.19 ~ (hAPP_f22106695ol_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: % 62.44/9.19 fun_nat_bool] : ! [v2: nat] : ! [v3: fun_nat_fun_nat_bool] : (v1 = v0 | ~ % 62.44/9.19 (hAPP_n1699378549t_bool(v3, v2) = v1) | ~ (hAPP_n1699378549t_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: nat] : ! [v1: nat] : ! [v2: fun_pname_bool] : ! [v3: % 62.44/9.19 fun_fu1668467777ol_nat] : (v1 = v0 | ~ (hAPP_f921600141ol_nat(v3, v2) = v1) % 62.44/9.19 | ~ (hAPP_f921600141ol_nat(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : % 62.44/9.19 ! [v2: nat] : ! [v3: fun_nat_bool] : (v1 = v0 | ~ (hAPP_nat_bool(v3, v2) = % 62.44/9.19 v1) | ~ (hAPP_nat_bool(v3, v2) = v0)) & ! [v0: fun_fu425979586l_bool] : % 62.44/9.19 ! [v1: fun_fu425979586l_bool] : ! [v2: fun_fu425979586l_bool] : ! [v3: % 62.44/9.19 fun_nat_bool] : (v1 = v0 | ~ (insert_fun_nat_bool(v3, v2) = v1) | ~ % 62.44/9.19 (insert_fun_nat_bool(v3, v2) = v0)) & ! [v0: fun_fu1430349052l_bool] : ! % 62.44/9.19 [v1: fun_fu1430349052l_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.19 fun_pname_bool] : (v1 = v0 | ~ (insert1325755072e_bool(v3, v2) = v1) | ~ % 62.44/9.19 (insert1325755072e_bool(v3, v2) = v0)) & ! [v0: fun_fun_a_bool_bool] : ! % 62.44/9.19 [v1: fun_fun_a_bool_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: fun_a_bool] % 62.44/9.19 : (v1 = v0 | ~ (insert_fun_a_bool(v3, v2) = v1) | ~ (insert_fun_a_bool(v3, % 62.44/9.19 v2) = v0)) & ! [v0: fun_fu885608257l_bool] : ! [v1: % 62.44/9.19 fun_fu885608257l_bool] : ! [v2: fun_fu885608257l_bool] : ! [v3: % 62.44/9.19 fun_fun_a_bool_bool] : (v1 = v0 | ~ (insert1457093509l_bool(v3, v2) = v1) | % 62.44/9.19 ~ (insert1457093509l_bool(v3, v2) = v0)) & ! [v0: fun_fu399576434l_bool] : % 62.44/9.19 ! [v1: fun_fu399576434l_bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: % 62.44/9.19 fun_fu1430349052l_bool] : (v1 = v0 | ~ (insert1117693814l_bool(v3, v2) = % 62.44/9.19 v1) | ~ (insert1117693814l_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_fu814369080l_bool] : ! [v1: fun_fu814369080l_bool] : ! [v2: % 62.44/9.19 fun_fu814369080l_bool] : ! [v3: fun_fu425979586l_bool] : (v1 = v0 | ~ % 62.44/9.19 (insert2003652156l_bool(v3, v2) = v1) | ~ (insert2003652156l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: % 62.44/9.19 fun_pname_bool] : ! [v3: pname] : (v1 = v0 | ~ (insert_pname(v3, v2) = v1) % 62.44/9.19 | ~ (insert_pname(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: % 62.44/9.19 fun_nat_bool] : ! [v2: fun_nat_bool] : ! [v3: nat] : (v1 = v0 | ~ % 62.44/9.19 (insert_nat(v3, v2) = v1) | ~ (insert_nat(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_a_bool] : ! [v3: x_a] : (v1 % 62.44/9.19 = v0 | ~ (insert_a(v3, v2) = v1) | ~ (insert_a(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_nat_pname] : (v1 = v0 | ~ (image_nat_pname(v3, v2) = v1) | ~ % 62.44/9.19 (image_nat_pname(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: % 62.44/9.19 fun_nat_bool] : ! [v2: fun_pname_bool] : ! [v3: fun_pname_nat] : (v1 = v0 % 62.44/9.19 | ~ (image_pname_nat(v3, v2) = v1) | ~ (image_pname_nat(v3, v2) = v0)) & % 62.44/9.19 ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_fun_a_bool_bool] : ! % 62.44/9.19 [v3: fun_fun_a_bool_a] : (v1 = v0 | ~ (image_fun_a_bool_a(v3, v2) = v1) | ~ % 62.44/9.19 (image_fun_a_bool_a(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.19 fun_fun_pname_bool_a] : (v1 = v0 | ~ (image_876012084bool_a(v3, v2) = v1) | % 62.44/9.19 ~ (image_876012084bool_a(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_fu425979586l_bool] : ! [v3: fun_fun_nat_bool_a] : % 62.44/9.19 (v1 = v0 | ~ (image_fun_nat_bool_a(v3, v2) = v1) | ~ % 62.44/9.19 (image_fun_nat_bool_a(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.19 fun_a_bool] : ! [v2: fun_a_bool] : ! [v3: fun_a_a] : (v1 = v0 | ~ % 62.44/9.19 (image_a_a(v3, v2) = v1) | ~ (image_a_a(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: fun_pname_bool] : ! % 62.44/9.19 [v3: fun_pname_pname] : (v1 = v0 | ~ (image_pname_pname(v3, v2) = v1) | ~ % 62.44/9.19 (image_pname_pname(v3, v2) = v0)) & ! [v0: fun_fu425979586l_bool] : ! [v1: % 62.44/9.19 fun_fu425979586l_bool] : ! [v2: fun_pname_bool] : ! [v3: % 62.44/9.19 fun_pn406123357t_bool] : (v1 = v0 | ~ (image_2129980159t_bool(v3, v2) = v1) % 62.44/9.19 | ~ (image_2129980159t_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_fu1430349052l_bool] : ! [v1: fun_fu1430349052l_bool] : ! [v2: % 62.44/9.19 fun_pname_bool] : ! [v3: fun_pn800050071e_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_47868345e_bool(v3, v2) = v1) | ~ (image_47868345e_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! % 62.44/9.19 [v2: fun_pname_bool] : ! [v3: fun_pname_fun_a_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_112932426a_bool(v3, v2) = v1) | ~ (image_112932426a_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu885608257l_bool] : ! [v1: fun_fu885608257l_bool] : % 62.44/9.19 ! [v2: fun_pname_bool] : ! [v3: fun_pn1038293468l_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_1420695166l_bool(v3, v2) = v1) | ~ (image_1420695166l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu399576434l_bool] : ! [v1: fun_fu399576434l_bool] : % 62.44/9.19 ! [v2: fun_pname_bool] : ! [v3: fun_pn422929397l_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_1642285373l_bool(v3, v2) = v1) | ~ (image_1642285373l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu814369080l_bool] : ! [v1: fun_fu814369080l_bool] : % 62.44/9.19 ! [v2: fun_pname_bool] : ! [v3: fun_pn1165013435l_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_1154884483l_bool(v3, v2) = v1) | ~ (image_1154884483l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_nat_bool] : % 62.44/9.19 ! [v3: fun_nat_a] : (v1 = v0 | ~ (image_nat_a(v3, v2) = v1) | ~ % 62.44/9.19 (image_nat_a(v3, v2) = v0)) & ! [v0: fun_fu425979586l_bool] : ! [v1: % 62.44/9.19 fun_fu425979586l_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_nat_fun_nat_bool] : (v1 = v0 | ~ (image_26036933t_bool(v3, v2) = v1) | % 62.44/9.19 ~ (image_26036933t_bool(v3, v2) = v0)) & ! [v0: fun_fu1430349052l_bool] : % 62.44/9.19 ! [v1: fun_fu1430349052l_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_na936072029e_bool] : (v1 = v0 | ~ (image_1655916159e_bool(v3, v2) = v1) % 62.44/9.19 | ~ (image_1655916159e_bool(v3, v2) = v0)) & ! [v0: fun_fun_a_bool_bool] : % 62.44/9.19 ! [v1: fun_fun_a_bool_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_nat_fun_a_bool] : (v1 = v0 | ~ (image_nat_fun_a_bool(v3, v2) = v1) | ~ % 62.44/9.19 (image_nat_fun_a_bool(v3, v2) = v0)) & ! [v0: fun_fu885608257l_bool] : ! % 62.44/9.19 [v1: fun_fu885608257l_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.19 fun_na1632405922l_bool] : (v1 = v0 | ~ (image_1208015684l_bool(v3, v2) = % 62.44/9.19 v1) | ~ (image_1208015684l_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.19 fun_fu399576434l_bool] : ! [v1: fun_fu399576434l_bool] : ! [v2: % 62.44/9.19 fun_nat_bool] : ! [v3: fun_na2122364079l_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_1874789623l_bool(v3, v2) = v1) | ~ (image_1874789623l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_fu814369080l_bool] : ! [v1: fun_fu814369080l_bool] : % 62.44/9.19 ! [v2: fun_nat_bool] : ! [v3: fun_na1436237685l_bool] : (v1 = v0 | ~ % 62.44/9.19 (image_1607900221l_bool(v3, v2) = v1) | ~ (image_1607900221l_bool(v3, v2) = % 62.44/9.19 v0)) & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: % 62.44/9.19 fun_a_bool] : ! [v3: fun_a_pname] : (v1 = v0 | ~ (image_a_pname(v3, v2) = % 62.44/9.20 v1) | ~ (image_a_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] : ! [v1: % 62.44/9.20 fun_pname_bool] : ! [v2: fun_fu425979586l_bool] : ! [v3: % 62.44/9.20 fun_fu665170229_pname] : (v1 = v0 | ~ (image_1921560913_pname(v3, v2) = v1) % 62.44/9.20 | ~ (image_1921560913_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] : ! % 62.44/9.20 [v1: fun_pname_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.20 fun_fu1499449723_pname] : (v1 = v0 | ~ (image_1283814551_pname(v3, v2) = % 62.44/9.20 v1) | ~ (image_1283814551_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] % 62.44/9.20 : ! [v1: fun_pname_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: % 62.44/9.20 fun_fun_a_bool_pname] : (v1 = v0 | ~ (image_1854862208_pname(v3, v2) = v1) % 62.44/9.20 | ~ (image_1854862208_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] : ! % 62.44/9.20 [v1: fun_pname_bool] : ! [v2: fun_fu885608257l_bool] : ! [v3: % 62.44/9.20 fun_fu1175941238_pname] : (v1 = v0 | ~ (image_990671762_pname(v3, v2) = v1) % 62.44/9.20 | ~ (image_990671762_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] : ! % 62.44/9.20 [v1: fun_pname_bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: % 62.44/9.20 fun_fu1664106117_pname] : (v1 = v0 | ~ (image_1705983821_pname(v3, v2) = % 62.44/9.20 v1) | ~ (image_1705983821_pname(v3, v2) = v0)) & ! [v0: fun_pname_bool] % 62.44/9.20 : ! [v1: fun_pname_bool] : ! [v2: fun_fu814369080l_bool] : ! [v3: % 62.44/9.20 fun_fu881587263_pname] : (v1 = v0 | ~ (image_1604018183_pname(v3, v2) = v1) % 62.44/9.20 | ~ (image_1604018183_pname(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! % 62.44/9.20 [v1: fun_nat_bool] : ! [v2: fun_a_bool] : ! [v3: fun_a_nat] : (v1 = v0 | ~ % 62.44/9.20 (image_a_nat(v3, v2) = v1) | ~ (image_a_nat(v3, v2) = v0)) & ! [v0: % 62.44/9.20 fun_nat_bool] : ! [v1: fun_nat_bool] : ! [v2: fun_fu425979586l_bool] : ! % 62.44/9.20 [v3: fun_fun_nat_bool_nat] : (v1 = v0 | ~ (image_496248727ol_nat(v3, v2) = % 62.44/9.20 v1) | ~ (image_496248727ol_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : % 62.44/9.20 ! [v1: fun_nat_bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: % 62.44/9.20 fun_fu1668467777ol_nat] : (v1 = v0 | ~ (image_1551609309ol_nat(v3, v2) = % 62.44/9.20 v1) | ~ (image_1551609309ol_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : % 62.44/9.20 ! [v1: fun_nat_bool] : ! [v2: fun_fun_a_bool_bool] : ! [v3: % 62.44/9.20 fun_fun_a_bool_nat] : (v1 = v0 | ~ (image_fun_a_bool_nat(v3, v2) = v1) | ~ % 62.44/9.20 (image_fun_a_bool_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: % 62.44/9.20 fun_nat_bool] : ! [v2: fun_fu885608257l_bool] : ! [v3: % 62.44/9.20 fun_fu2020802748ol_nat] : (v1 = v0 | ~ (image_1802975832ol_nat(v3, v2) = % 62.44/9.20 v1) | ~ (image_1802975832ol_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : % 62.44/9.20 ! [v1: fun_nat_bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: % 62.44/9.20 fun_fu1730389579ol_nat] : (v1 = v0 | ~ (image_1079571347ol_nat(v3, v2) = % 62.44/9.20 v1) | ~ (image_1079571347ol_nat(v3, v2) = v0)) & ! [v0: fun_nat_bool] : % 62.44/9.20 ! [v1: fun_nat_bool] : ! [v2: fun_fu814369080l_bool] : ! [v3: % 62.44/9.20 fun_fu411113733ol_nat] : (v1 = v0 | ~ (image_2089570637ol_nat(v3, v2) = v1) % 62.44/9.20 | ~ (image_2089570637ol_nat(v3, v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: % 62.44/9.20 fun_a_bool] : ! [v2: fun_pname_bool] : ! [v3: fun_pname_a] : (v1 = v0 | ~ % 62.44/9.20 (image_pname_a(v3, v2) = v1) | ~ (image_pname_a(v3, v2) = v0)) & ! [v0: % 62.44/9.20 fun_fu814369080l_bool] : ! [v1: fun_fu814369080l_bool] : ! [v2: % 62.44/9.20 fun_fu425979586l_bool] : ! [v3: fun_fu140186515l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f1772781669l_bool(v3, v2) = v1) | ~ (hAPP_f1772781669l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu399576434l_bool] : ! [v1: fun_fu399576434l_bool] : % 62.44/9.20 ! [v2: fun_fu1430349052l_bool] : ! [v3: fun_fu1911931399l_bool] : (v1 = v0 | % 62.44/9.20 ~ (hAPP_f510955609l_bool(v3, v2) = v1) | ~ (hAPP_f510955609l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu885608257l_bool] : ! [v1: fun_fu885608257l_bool] : % 62.44/9.20 ! [v2: fun_fun_a_bool_bool] : ! [v3: fun_fu418465139l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f1434722111l_bool(v3, v2) = v1) | ~ (hAPP_f1434722111l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu255076663l_bool] : ! [v1: fun_fu255076663l_bool] : % 62.44/9.20 ! [v2: fun_fu885608257l_bool] : ! [v3: fun_fu821736593l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f1050622307l_bool(v3, v2) = v1) | ~ (hAPP_f1050622307l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_fu885608257l_bool] : ! % 62.44/9.20 [v3: fun_fu255076663l_bool] : (v1 = v0 | ~ (hAPP_f292226953l_bool(v3, v2) = % 62.44/9.20 v1) | ~ (hAPP_f292226953l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 62.44/9.20 bool] : ! [v2: fun_fu255076663l_bool] : ! [v3: fun_fu754241017l_bool] : % 62.44/9.20 (v1 = v0 | ~ (hAPP_f1363661463l_bool(v3, v2) = v1) | ~ % 62.44/9.20 (hAPP_f1363661463l_bool(v3, v2) = v0)) & ! [v0: fun_fu1438281908l_bool] : % 62.44/9.20 ! [v1: fun_fu1438281908l_bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: % 62.44/9.20 fun_fu1086940979l_bool] : (v1 = v0 | ~ (hAPP_f1759205631l_bool(v3, v2) = % 62.44/9.20 v1) | ~ (hAPP_f1759205631l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 62.44/9.20 bool] : ! [v2: fun_fu399576434l_bool] : ! [v3: fun_fu1438281908l_bool] : % 62.44/9.20 (v1 = v0 | ~ (hAPP_f389811538l_bool(v3, v2) = v1) | ~ % 62.44/9.20 (hAPP_f389811538l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! % 62.44/9.20 [v2: fun_fu1438281908l_bool] : ! [v3: fun_fu2065874474l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f595608956l_bool(v3, v2) = v1) | ~ (hAPP_f595608956l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu61768826l_bool] : ! [v1: fun_fu61768826l_bool] : ! % 62.44/9.20 [v2: fun_fu814369080l_bool] : ! [v3: fun_fu1137991347l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f760187903l_bool(v3, v2) = v1) | ~ (hAPP_f760187903l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_fu814369080l_bool] : ! % 62.44/9.20 [v3: fun_fu61768826l_bool] : (v1 = v0 | ~ (hAPP_f937997336l_bool(v3, v2) = % 62.44/9.20 v1) | ~ (hAPP_f937997336l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 62.44/9.20 bool] : ! [v2: fun_fu61768826l_bool] : ! [v3: fun_fu1971389424l_bool] : % 62.44/9.20 (v1 = v0 | ~ (hAPP_f1295398978l_bool(v3, v2) = v1) | ~ % 62.44/9.20 (hAPP_f1295398978l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : ! % 62.44/9.20 [v2: fun_fun_a_bool_bool] : ! [v3: fun_fu885608257l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f621171935l_bool(v3, v2) = v1) | ~ (hAPP_f621171935l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu1430349052l_bool] : ! [v1: fun_fu1430349052l_bool] : % 62.44/9.20 ! [v2: fun_pname_bool] : ! [v3: fun_fu802393907l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f434788991l_bool(v3, v2) = v1) | ~ (hAPP_f434788991l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_pname_bool] : ! [v3: % 62.44/9.20 fun_fu1430349052l_bool] : (v1 = v0 | ~ (hAPP_f1664156314l_bool(v3, v2) = % 62.44/9.20 v1) | ~ (hAPP_f1664156314l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: % 62.44/9.20 bool] : ! [v2: fun_fu1430349052l_bool] : ! [v3: fun_fu399576434l_bool] : % 62.44/9.20 (v1 = v0 | ~ (hAPP_f1935102916l_bool(v3, v2) = v1) | ~ % 62.44/9.20 (hAPP_f1935102916l_bool(v3, v2) = v0)) & ! [v0: fun_fu425979586l_bool] : ! % 62.44/9.20 [v1: fun_fu425979586l_bool] : ! [v2: fun_nat_bool] : ! [v3: % 62.44/9.20 fun_fu1217155507l_bool] : (v1 = v0 | ~ (hAPP_f103356543l_bool(v3, v2) = v1) % 62.44/9.20 | ~ (hAPP_f103356543l_bool(v3, v2) = v0)) & ! [v0: bool] : ! [v1: bool] : % 62.44/9.20 ! [v2: fun_nat_bool] : ! [v3: fun_fu425979586l_bool] : (v1 = v0 | ~ % 62.44/9.20 (hAPP_f54304608l_bool(v3, v2) = v1) | ~ (hAPP_f54304608l_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: bool] : ! [v1: bool] : ! [v2: fun_fu425979586l_bool] : ! % 62.44/9.20 [v3: fun_fu814369080l_bool] : (v1 = v0 | ~ (hAPP_f1637334154l_bool(v3, v2) = % 62.44/9.20 v1) | ~ (hAPP_f1637334154l_bool(v3, v2) = v0)) & ! [v0: % 62.44/9.20 fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! [v2: fun_a_bool] : % 62.44/9.20 ! [v3: fun_fu1471507361l_bool] : (v1 = v0 | ~ (hAPP_f1631501043l_bool(v3, v2) % 62.44/9.20 = v1) | ~ (hAPP_f1631501043l_bool(v3, v2) = v0)) & ! [v0: bool] : ! % 62.44/9.20 [v1: bool] : ! [v2: fun_a_bool] : ! [v3: fun_fun_a_bool_bool] : (v1 = v0 | % 62.44/9.20 ~ (hAPP_fun_a_bool_bool(v3, v2) = v1) | ~ (hAPP_fun_a_bool_bool(v3, v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu911136611l_bool] : ! [v1: fun_fu911136611l_bool] : % 62.44/9.20 ! [v2: fun_fu386216885l_bool] : (v1 = v0 | ~ (cOMBC_1880041174l_bool(v2) = % 62.44/9.20 v1) | ~ (cOMBC_1880041174l_bool(v2) = v0)) & ! [v0: % 62.44/9.20 fun_fu2087345469l_bool] : ! [v1: fun_fu2087345469l_bool] : ! [v2: % 62.44/9.20 fun_fu931343505l_bool] : (v1 = v0 | ~ (cOMBC_1988546018l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1988546018l_bool(v2) = v0)) & ! [v0: fun_fu616551101l_bool] : ! % 62.44/9.20 [v1: fun_fu616551101l_bool] : ! [v2: fun_fu1436348701l_bool] : (v1 = v0 | ~ % 62.44/9.20 (cOMBC_1245412066l_bool(v2) = v1) | ~ (cOMBC_1245412066l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_a_fun_a_bool] : ! [v1: fun_a_fun_a_bool] : ! [v2: % 62.44/9.20 fun_a_fun_a_bool] : (v1 = v0 | ~ (cOMBC_a_a_bool(v2) = v1) | ~ % 62.44/9.20 (cOMBC_a_a_bool(v2) = v0)) & ! [v0: fun_fu1731003005a_bool] : ! [v1: % 62.44/9.20 fun_fu1731003005a_bool] : ! [v2: fun_a_1255737515l_bool] : (v1 = v0 | ~ % 62.44/9.20 (cOMBC_1355376034l_bool(v2) = v1) | ~ (cOMBC_1355376034l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_pn800050071e_bool] : ! [v1: fun_pn800050071e_bool] : ! [v2: % 62.44/9.20 fun_pn800050071e_bool] : (v1 = v0 | ~ (cOMBC_1149511130e_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1149511130e_bool(v2) = v0)) & ! [v0: fun_fu821463397t_bool] : ! % 62.44/9.20 [v1: fun_fu821463397t_bool] : ! [v2: fun_na1436237685l_bool] : (v1 = v0 | ~ % 62.44/9.20 (cOMBC_226598744l_bool(v2) = v1) | ~ (cOMBC_226598744l_bool(v2) = v0)) & ! % 62.44/9.20 [v0: fun_fu410713561e_bool] : ! [v1: fun_fu410713561e_bool] : ! [v2: % 62.44/9.20 fun_pn422929397l_bool] : (v1 = v0 | ~ (cOMBC_1058051404l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1058051404l_bool(v2) = v0)) & ! [v0: fun_a_fun_pname_bool] : ! % 62.44/9.20 [v1: fun_a_fun_pname_bool] : ! [v2: fun_pname_fun_a_bool] : (v1 = v0 | ~ % 62.44/9.20 (cOMBC_pname_a_bool(v2) = v1) | ~ (cOMBC_pname_a_bool(v2) = v0)) & ! [v0: % 62.44/9.20 fun_nat_fun_nat_bool] : ! [v1: fun_nat_fun_nat_bool] : ! [v2: % 62.44/9.20 fun_nat_fun_nat_bool] : (v1 = v0 | ~ (cOMBC_nat_nat_bool(v2) = v1) | ~ % 62.44/9.20 (cOMBC_nat_nat_bool(v2) = v0)) & ! [v0: fun_nat_nat] : ! [v1: fun_nat_nat] % 62.44/9.20 : ! [v2: nat] : (v1 = v0 | ~ (minus_minus_nat(v2) = v1) | ~ % 62.44/9.20 (minus_minus_nat(v2) = v0)) & ! [v0: fun_nat_bool] : ! [v1: fun_nat_bool] % 62.44/9.20 : ! [v2: fun_nat_bool] : (v1 = v0 | ~ (collect_nat(v2) = v1) | ~ % 62.44/9.20 (collect_nat(v2) = v0)) & ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] % 62.44/9.20 : ! [v2: fun_pname_bool] : (v1 = v0 | ~ (collect_pname(v2) = v1) | ~ % 62.44/9.20 (collect_pname(v2) = v0)) & ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! % 62.44/9.20 [v2: fun_a_bool] : (v1 = v0 | ~ (collect_a(v2) = v1) | ~ (collect_a(v2) = % 62.44/9.20 v0)) & ! [v0: fun_fu140186515l_bool] : ! [v1: fun_fu140186515l_bool] : % 62.44/9.20 ! [v2: fun_fu140186515l_bool] : (v1 = v0 | ~ (cOMBC_595898202l_bool(v2) = v1) % 62.44/9.20 | ~ (cOMBC_595898202l_bool(v2) = v0)) & ! [v0: fun_fu814369080l_bool] : ! % 62.44/9.20 [v1: fun_fu814369080l_bool] : ! [v2: fun_fu814369080l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec1015864663l_bool(v2) = v1) | ~ (collec1015864663l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_fu1911931399l_bool] : ! [v1: fun_fu1911931399l_bool] : ! [v2: % 62.44/9.20 fun_fu1911931399l_bool] : (v1 = v0 | ~ (cOMBC_7971162l_bool(v2) = v1) | ~ % 62.44/9.20 (cOMBC_7971162l_bool(v2) = v0)) & ! [v0: fun_fu399576434l_bool] : ! [v1: % 62.44/9.20 fun_fu399576434l_bool] : ! [v2: fun_fu399576434l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec1613912337l_bool(v2) = v1) | ~ (collec1613912337l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_fu418465139l_bool] : ! [v1: fun_fu418465139l_bool] : ! [v2: % 62.44/9.20 fun_fu418465139l_bool] : (v1 = v0 | ~ (cOMBC_331553030l_bool(v2) = v1) | ~ % 62.44/9.20 (cOMBC_331553030l_bool(v2) = v0)) & ! [v0: fun_fu885608257l_bool] : ! [v1: % 62.44/9.20 fun_fu885608257l_bool] : ! [v2: fun_fu885608257l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec707592106l_bool(v2) = v1) | ~ (collec707592106l_bool(v2) = v0)) & ! % 62.44/9.20 [v0: fun_fu821736593l_bool] : ! [v1: fun_fu821736593l_bool] : ! [v2: % 62.44/9.20 fun_fu821736593l_bool] : (v1 = v0 | ~ (cOMBC_636888218l_bool(v2) = v1) | ~ % 62.44/9.20 (cOMBC_636888218l_bool(v2) = v0)) & ! [v0: fun_fu255076663l_bool] : ! [v1: % 62.44/9.20 fun_fu255076663l_bool] : ! [v2: fun_fu255076663l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec1635217238l_bool(v2) = v1) | ~ (collec1635217238l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_fu1086940979l_bool] : ! [v1: fun_fu1086940979l_bool] : ! [v2: % 62.44/9.20 fun_fu1086940979l_bool] : (v1 = v0 | ~ (cOMBC_336095980l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_336095980l_bool(v2) = v0)) & ! [v0: fun_fu1438281908l_bool] : ! % 62.44/9.20 [v1: fun_fu1438281908l_bool] : ! [v2: fun_fu1438281908l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec792590109l_bool(v2) = v1) | ~ (collec792590109l_bool(v2) = v0)) & ! % 62.44/9.20 [v0: fun_fu1137991347l_bool] : ! [v1: fun_fu1137991347l_bool] : ! [v2: % 62.44/9.20 fun_fu1137991347l_bool] : (v1 = v0 | ~ (cOMBC_1269652216l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1269652216l_bool(v2) = v0)) & ! [v0: fun_fu61768826l_bool] : ! % 62.44/9.20 [v1: fun_fu61768826l_bool] : ! [v2: fun_fu61768826l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec1874991203l_bool(v2) = v1) | ~ (collec1874991203l_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_fu1471507361l_bool] : ! [v1: fun_fu1471507361l_bool] : ! [v2: % 62.44/9.20 fun_fu1471507361l_bool] : (v1 = v0 | ~ (cOMBC_1732670874l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1732670874l_bool(v2) = v0)) & ! [v0: fun_fun_a_bool_bool] : ! % 62.44/9.20 [v1: fun_fun_a_bool_bool] : ! [v2: fun_fun_a_bool_bool] : (v1 = v0 | ~ % 62.44/9.20 (collect_fun_a_bool(v2) = v1) | ~ (collect_fun_a_bool(v2) = v0)) & ! [v0: % 62.44/9.20 fun_fu802393907l_bool] : ! [v1: fun_fu802393907l_bool] : ! [v2: % 62.44/9.20 fun_fu802393907l_bool] : (v1 = v0 | ~ (cOMBC_1284144636l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1284144636l_bool(v2) = v0)) & ! [v0: fun_fu1430349052l_bool] : ! % 62.44/9.20 [v1: fun_fu1430349052l_bool] : ! [v2: fun_fu1430349052l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collec1974731493e_bool(v2) = v1) | ~ (collec1974731493e_bool(v2) = v0)) & % 62.44/9.20 ! [v0: fun_fu1217155507l_bool] : ! [v1: fun_fu1217155507l_bool] : ! [v2: % 62.44/9.20 fun_fu1217155507l_bool] : (v1 = v0 | ~ (cOMBC_1693257480l_bool(v2) = v1) | % 62.44/9.20 ~ (cOMBC_1693257480l_bool(v2) = v0)) & ! [v0: fun_fu425979586l_bool] : ! % 62.44/9.20 [v1: fun_fu425979586l_bool] : ! [v2: fun_fu425979586l_bool] : (v1 = v0 | ~ % 62.44/9.20 (collect_fun_nat_bool(v2) = v1) | ~ (collect_fun_nat_bool(v2) = v0)) & ! % 62.44/9.20 [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! [v2: fun_a_bool] % 62.44/9.20 : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 62.44/9.20 % 62.44/9.20 Further assumptions not needed in the proof: % 62.44/9.20 -------------------------------------------- % 62.44/9.20 fact_0_assms_I1_J, fact_100_card__insert__if, fact_101_card__insert__if, % 62.44/9.20 fact_103_card__insert__if, fact_104_card__insert__disjoint, % 62.44/9.20 fact_105_card__insert__disjoint, fact_106_card__insert__disjoint, % 62.44/9.20 fact_107_card__insert__disjoint, fact_108_card__insert__disjoint, % 62.44/9.20 fact_109_card__insert__disjoint, fact_10_finite__imageI, % 62.44/9.20 fact_110_finite__Collect__conjI, fact_111_finite__Collect__conjI, % 62.44/9.20 fact_112_finite__Collect__conjI, fact_113_finite__Collect__conjI, % 62.44/9.20 fact_114_finite__Collect__conjI, fact_115_finite__Collect__conjI, % 62.44/9.20 fact_116_Suc__diff__le, fact_117_finite__Collect__le__nat, % 62.44/9.20 fact_118_card__Collect__le__nat, fact_119_Suc__inject, fact_11_finite__imageI, % 62.44/9.20 fact_120_nat_Oinject, fact_121_Suc__n__not__n, fact_122_n__not__Suc__n, % 62.44/9.20 fact_123_le__antisym, fact_124_le__trans, fact_125_eq__imp__le, % 62.44/9.20 fact_126_nat__le__linear, fact_127_le__refl, fact_128_diff__commute, % 62.44/9.20 fact_129_finite__Collect__disjI, fact_12_finite__imageI, % 62.44/9.20 fact_130_finite__Collect__disjI, fact_131_finite__Collect__disjI, % 62.44/9.20 fact_132_finite__Collect__disjI, fact_133_finite__Collect__disjI, % 62.44/9.20 fact_134_finite__Collect__disjI, fact_135_finite__insert, % 62.44/9.20 fact_136_finite__insert, fact_137_finite__insert, fact_138_finite__insert, % 62.44/9.20 fact_139_finite__insert, fact_13_finite__imageI, fact_140_finite__insert, % 62.44/9.20 fact_141_finite__subset, fact_142_finite__subset, fact_143_finite__subset, % 62.44/9.20 fact_144_finite__subset, fact_145_finite__subset, fact_146_finite__subset, % 62.44/9.20 fact_147_rev__finite__subset, fact_148_rev__finite__subset, % 62.44/9.20 fact_149_rev__finite__subset, fact_14_finite__imageI, % 62.44/9.20 fact_150_rev__finite__subset, fact_151_rev__finite__subset, % 62.44/9.20 fact_152_rev__finite__subset, fact_153_Suc__leD, fact_154_le__SucE, % 62.44/9.20 fact_155_le__SucI, fact_156_Suc__le__mono, fact_157_le__Suc__eq, % 62.44/9.20 fact_158_not__less__eq__eq, fact_159_Suc__n__not__le__n, fact_15_finite__imageI, % 62.44/9.20 fact_160_Suc__diff__diff, fact_161_diff__Suc__Suc, fact_162_le__diff__iff, % 62.44/9.20 fact_163_Nat_Odiff__diff__eq, fact_164_eq__diff__iff, % 62.44/9.20 fact_165_diff__diff__cancel, fact_166_diff__le__mono, fact_167_diff__le__mono2, % 62.44/9.20 fact_168_diff__le__self, fact_16_finite__imageI, fact_171_lift__Suc__mono__le, % 62.44/9.20 fact_172_lift__Suc__mono__le, fact_173_lift__Suc__mono__le, % 62.44/9.20 fact_174_lift__Suc__mono__le, fact_175_pigeonhole__infinite, fact_177_equalityI, % 62.44/9.20 fact_178_equalityI, fact_179_equalityI, fact_17_finite__imageI, % 62.44/9.20 fact_180_subsetD, fact_181_subsetD, fact_182_subsetD, fact_183_insertCI, % 62.44/9.20 fact_184_insertCI, fact_185_insertCI, fact_186_insertE, fact_187_insertE, % 62.44/9.20 fact_188_insertE, fact_189_insertI1, fact_18_finite__imageI, fact_190_insertI1, % 62.44/9.20 fact_191_insertI1, fact_192_insert__compr, fact_193_insert__compr, % 62.44/9.20 fact_194_insert__compr, fact_195_insert__compr, fact_196_insert__compr, % 62.44/9.20 fact_197_insert__compr, fact_198_insert__Collect, fact_199_insert__Collect, % 62.44/9.20 fact_19_finite__imageI, fact_1_finite__Collect__subsets, % 62.44/9.20 fact_200_insert__Collect, fact_201_insert__Collect, fact_202_insert__Collect, % 62.44/9.20 fact_203_insert__Collect, fact_204_insert__absorb2, fact_205_insert__absorb2, % 62.44/9.20 fact_206_insert__absorb2, fact_207_insert__commute, fact_208_insert__commute, % 62.44/9.20 fact_209_insert__commute, fact_20_finite__imageI, fact_210_insert__iff, % 62.44/9.20 fact_211_insert__iff, fact_212_insert__iff, fact_213_insert__code, % 62.44/9.20 fact_214_insert__code, fact_215_insert__code, fact_216_insert__ident, % 62.44/9.20 fact_217_insert__ident, fact_218_insert__ident, fact_219_insertI2, % 62.44/9.20 fact_21_finite__imageI, fact_220_insertI2, fact_221_insertI2, % 62.44/9.20 fact_222_insert__absorb, fact_224_insert__absorb, fact_225_subset__refl, % 62.44/9.20 fact_226_subset__refl, fact_227_subset__refl, fact_228_set__eq__subset, % 62.44/9.20 fact_229_set__eq__subset, fact_22_finite__imageI, fact_230_set__eq__subset, % 62.44/9.20 fact_231_equalityD1, fact_232_equalityD1, fact_233_equalityD1, % 62.44/9.20 fact_234_equalityD2, fact_235_equalityD2, fact_236_equalityD2, % 62.44/9.20 fact_237_in__mono, fact_238_in__mono, fact_239_in__mono, fact_23_finite__imageI, % 62.44/9.20 fact_240_set__rev__mp, fact_241_set__rev__mp, fact_242_set__rev__mp, % 62.44/9.20 fact_243_set__mp, fact_244_set__mp, fact_245_set__mp, fact_246_subset__trans, % 62.44/9.20 fact_247_subset__trans, fact_248_subset__trans, fact_249_equalityE, % 62.44/9.20 fact_24_finite__imageI, fact_250_equalityE, fact_251_equalityE, % 62.44/9.20 fact_252_mem__def, fact_253_mem__def, fact_254_mem__def, fact_255_Collect__def, % 62.44/9.20 fact_256_Collect__def, fact_257_Collect__def, fact_258_Collect__def, % 62.44/9.20 fact_259_Collect__def, fact_25_finite__imageI, fact_260_image__iff, % 62.44/9.20 fact_261_imageI, fact_262_rev__image__eqI, fact_263_insert__compr__raw, % 62.44/9.20 fact_264_insert__compr__raw, fact_265_insert__compr__raw, % 62.44/9.20 fact_266_insert__compr__raw, fact_267_insert__compr__raw, % 62.44/9.20 fact_268_insert__compr__raw, fact_269_subset__insertI, fact_26_finite__imageI, % 62.44/9.20 fact_270_subset__insertI, fact_271_subset__insertI, fact_272_insert__subset, % 62.44/9.20 fact_273_insert__subset, fact_275_subset__insert, fact_276_subset__insert, % 62.44/9.20 fact_277_subset__insert, fact_278_subset__insertI2, fact_279_subset__insertI2, % 62.44/9.20 fact_27_finite__imageI, fact_280_subset__insertI2, fact_281_insert__mono, % 62.44/9.20 fact_282_insert__mono, fact_283_insert__mono, fact_284_image__insert, % 62.44/9.20 fact_285_insert__image, fact_286_subset__image__iff, fact_287_image__mono, % 62.44/9.20 fact_288_imageE, fact_289_subsetI, fact_28_finite__imageI, fact_291_subsetI, % 62.44/9.20 fact_292_zero__induct__lemma, fact_293_Suc__le__D, fact_294_image__subsetI, % 62.44/9.20 fact_295_order__refl, fact_296_order__refl, fact_297_order__refl, % 62.44/9.20 fact_298_order__refl, fact_299_finite__nat__set__iff__bounded__le, % 62.44/9.20 fact_29_finite__imageI, fact_2_finite__Collect__subsets, fact_30_finite__imageI, % 62.44/9.20 fact_31_finite__imageI, fact_32_finite__imageI, fact_33_finite__imageI, % 62.44/9.20 fact_34_finite__imageI, fact_35_finite__imageI, fact_36_finite__imageI, % 62.44/9.20 fact_37_finite__imageI, fact_38_finite__imageI, fact_39_finite__imageI, % 62.44/9.20 fact_3_finite__Collect__subsets, fact_40_finite__imageI, fact_41_finite__imageI, % 62.44/9.20 fact_42_finite__imageI, fact_43_finite__imageI, fact_44_finite__imageI, % 62.44/9.20 fact_45_finite_OinsertI, fact_46_finite_OinsertI, fact_47_finite_OinsertI, % 62.44/9.20 fact_48_finite_OinsertI, fact_49_finite_OinsertI, % 62.44/9.20 fact_4_finite__Collect__subsets, fact_50_finite_OinsertI, % 62.44/9.20 fact_51_finite_OinsertI, fact_52_finite_OinsertI, fact_53_finite_OinsertI, % 62.44/9.20 fact_54_card__image__le, fact_55_card__image__le, fact_56_card__image__le, % 62.44/9.20 fact_57_card__image__le, fact_58_card__image__le, fact_59_card__image__le, % 62.44/9.20 fact_5_finite__Collect__subsets, fact_60_card__image__le, % 62.44/9.20 fact_61_card__image__le, fact_62_card__image__le, fact_63_card__image__le, % 62.44/9.20 fact_64_card__image__le, fact_65_card__image__le, fact_66_card__image__le, % 62.44/9.20 fact_67_card__image__le, fact_68_card__image__le, fact_69_card__image__le, % 62.44/9.20 fact_6_finite__Collect__subsets, fact_70_card__image__le, % 62.44/9.20 fact_71_card__image__le, fact_72_card__image__le, fact_73_card__image__le, % 62.44/9.20 fact_74_card__image__le, fact_75_card__image__le, fact_76_card__image__le, % 62.44/9.20 fact_77_card__image__le, fact_78_card__image__le, fact_79_card__image__le, % 62.44/9.20 fact_7_finite__Collect__subsets, fact_80_card__mono, fact_81_card__mono, % 62.44/9.20 fact_82_card__mono, fact_83_card__mono, fact_84_card__mono, fact_85_card__mono, % 62.44/9.20 fact_86_card__seteq, fact_87_card__seteq, fact_88_card__seteq, % 62.44/9.20 fact_89_card__seteq, fact_8_finite__Collect__subsets, fact_90_card__seteq, % 62.44/9.20 fact_91_card__seteq, fact_92_card__insert__le, fact_93_card__insert__le, % 62.44/9.20 fact_94_card__insert__le, fact_95_card__insert__le, fact_96_card__insert__le, % 62.44/9.20 fact_97_card__insert__le, fact_98_card__insert__if, fact_99_card__insert__if, % 62.44/9.20 fact_9_finite__Collect__subsets, % 62.44/9.20 help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opna, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a_U, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname_U, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__H, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Op, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Nat__On, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_043, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_044, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_045, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_046, % 62.44/9.20 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_047, % 62.44/9.20 help_COMBC_1_1_COMBC_000t__a_000t__a_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBC_1_1_COMBC_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Oboo, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__Com__Opname_000t__a_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Com__Opname_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Nat__Onat_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HO, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_049, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__048, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__H, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__H, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo, % 62.44/9.20 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool, % 62.44/9.20 help_COMBS_1_1_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBS_1_1_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U, % 62.44/9.20 help_COMBS_1_1_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc_, % 62.44/9.20 help_COMBS_1_1_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__O, % 62.44/9.20 help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo, % 62.44/9.20 help_fNot_1_1_U, help_fNot_2_1_U, help_fconj_1_1_U, help_fconj_2_1_U, % 62.44/9.20 help_fconj_3_1_U, help_fdisj_1_1_U, help_fdisj_2_1_U, help_fdisj_3_1_U, % 62.44/9.20 help_fequal_1_1_fequal_000t__a_T, help_fequal_1_1_fequal_000tc__Com__Opname_T, % 62.44/9.20 help_fequal_1_1_fequal_000tc__Nat__Onat_T, % 62.44/9.20 help_fequal_1_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fequal_1_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fequal_1_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fequal_2_1_fequal_000t__a_T, help_fequal_2_1_fequal_000tc__Com__Opname_T, % 62.44/9.20 help_fequal_2_1_fequal_000tc__Nat__Onat_T, % 62.44/9.20 help_fequal_2_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fequal_2_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fequal_2_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 62.44/9.20 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 62.44/9.20 % 62.44/9.20 Those formulas are unsatisfiable: % 62.44/9.20 --------------------------------- % 62.44/9.20 % 62.44/9.20 Begin of proof % 62.44/9.20 | % 62.44/9.20 | ALPHA: (fact_102_card__insert__if) implies: % 62.44/9.21 | (1) ! [v0: pname] : ! [v1: fun_pname_bool] : ! [v2: % 62.44/9.21 | fun_fu1430349052l_bool] : ! [v3: bool] : ( ~ % 62.44/9.21 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ % 62.44/9.21 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ fun_pname_bool(v1) | ~ % 62.44/9.21 | pname(v0) | ? [v4: bool] : ? [v5: fun_pname_bool] : ? [v6: nat] : % 62.44/9.21 | ? [v7: nat] : ? [v8: nat] : % 62.44/9.21 | ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & bool(v4) & % 62.44/9.21 | ~ hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 62.44/9.21 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 62.44/9.21 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & % 62.44/9.21 | insert_pname(v0, v1) = v5 & fun_pname_bool(v5) & nat(v6))) & % 62.44/9.21 | (hBOOL(v3) | (v8 = v6 & hAPP_nat_nat(suc, v7) = v6 & % 62.44/9.21 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 62.44/9.21 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & % 62.44/9.21 | insert_pname(v0, v1) = v5 & fun_pname_bool(v5) & nat(v7) & % 62.44/9.21 | nat(v6)))))) % 62.44/9.21 | % 62.44/9.21 | ALPHA: (fact_169_finite__surj) implies: % 62.44/9.21 | (2) ! [v0: fun_a_bool] : ! [v1: fun_pname_a] : ! [v2: fun_pname_bool] : % 62.44/9.21 | ! [v3: fun_fun_a_bool_bool] : ! [v4: fun_a_bool] : ! [v5: bool] : ( ~ % 62.44/9.21 | (image_pname_a(v1, v2) = v4) | ~ % 62.44/9.21 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = v3) | ~ % 62.44/9.21 | (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ fun_pname_bool(v2) | ~ % 62.44/9.21 | fun_pname_a(v1) | ~ fun_a_bool(v0) | ~ hBOOL(v5) | ? [v6: bool] : % 62.44/9.21 | ? [v7: bool] : ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 % 62.44/9.21 | & bool(v6) & ~ hBOOL(v6)) | % 62.44/9.21 | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & bool(v7) & % 62.44/9.21 | hBOOL(v7)))) % 62.44/9.21 | % 62.67/9.21 | ALPHA: (fact_170_finite__subset__image) implies: % 62.67/9.21 | (3) ! [v0: fun_pname_a] : ! [v1: fun_pname_bool] : ! [v2: fun_a_bool] : % 62.67/9.21 | ! [v3: fun_fun_a_bool_bool] : ! [v4: fun_a_bool] : ! [v5: bool] : ( ~ % 62.67/9.21 | (image_pname_a(v0, v1) = v4) | ~ % 62.67/9.21 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v2) = v3) | ~ % 62.67/9.21 | (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ fun_pname_bool(v1) | ~ % 62.67/9.21 | fun_pname_a(v0) | ~ fun_a_bool(v2) | ~ hBOOL(v5) | ? [v6: bool] : % 62.67/9.21 | ? [v7: fun_pname_bool] : ? [v8: fun_fu1430349052l_bool] : ? [v9: % 62.67/9.21 | bool] : ? [v10: bool] : ? [v11: fun_a_bool] : (fun_pname_bool(v7) % 62.67/9.21 | & ((v11 = v2 & image_pname_a(v0, v7) = v2 & % 62.67/9.21 | hAPP_f434788991l_bool(ord_le313189616e_bool, v7) = v8 & % 62.67/9.21 | hAPP_f1664156314l_bool(v8, v1) = v9 & % 62.67/9.21 | hAPP_f1664156314l_bool(finite_finite_pname, v7) = v10 & % 62.67/9.21 | fun_fu1430349052l_bool(v8) & bool(v10) & bool(v9) & hBOOL(v10) % 62.67/9.21 | & hBOOL(v9)) | (hAPP_fun_a_bool_bool(finite_finite_a, v2) = v6 % 62.67/9.21 | & bool(v6) & ~ hBOOL(v6))))) % 62.67/9.21 | % 62.67/9.21 | ALPHA: (fact_176_image__eqI) implies: % 62.67/9.21 | (4) ! [v0: fun_pname_bool] : ! [v1: x_a] : ! [v2: fun_pname_a] : ! [v3: % 62.67/9.21 | pname] : ! [v4: fun_fu1430349052l_bool] : ! [v5: bool] : ! [v6: % 62.67/9.21 | fun_fun_a_bool_bool] : ! [v7: fun_a_bool] : ! [v8: bool] : ( ~ % 62.67/9.21 | (hAPP_a85458249l_bool(member_a, v1) = v6) | ~ % 62.67/9.21 | (hAPP_p338031245l_bool(member_pname, v3) = v4) | ~ % 62.67/9.21 | (image_pname_a(v2, v0) = v7) | ~ (hAPP_f1664156314l_bool(v4, v0) = % 62.67/9.21 | v5) | ~ (hAPP_fun_a_bool_bool(v6, v7) = v8) | ~ % 62.67/9.21 | fun_pname_bool(v0) | ~ fun_pname_a(v2) | ~ pname(v3) | ~ x_a(v1) | % 62.67/9.21 | ~ hBOOL(v5) | hBOOL(v8) | ? [v9: x_a] : ( ~ (v9 = v1) & % 62.67/9.21 | hAPP_pname_a(v2, v3) = v9 & x_a(v9))) % 62.67/9.21 | % 62.67/9.21 | ALPHA: (fact_223_insert__absorb) implies: % 62.67/9.21 | (5) ! [v0: pname] : ! [v1: fun_pname_bool] : ! [v2: % 62.67/9.21 | fun_fu1430349052l_bool] : ! [v3: bool] : ( ~ % 62.67/9.21 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ % 62.67/9.21 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ fun_pname_bool(v1) | ~ % 62.67/9.21 | pname(v0) | ~ hBOOL(v3) | insert_pname(v0, v1) = v1) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (fact_274_insert__subset) implies: % 62.67/9.22 | (6) ! [v0: x_a] : ! [v1: fun_a_bool] : ! [v2: fun_a_bool] : ! [v3: % 62.67/9.22 | fun_a_bool] : ! [v4: fun_fun_a_bool_bool] : ! [v5: bool] : ( ~ % 62.67/9.22 | (insert_a(v0, v1) = v3) | ~ % 62.67/9.22 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 62.67/9.22 | (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ fun_a_bool(v2) | ~ % 62.67/9.22 | fun_a_bool(v1) | ~ x_a(v0) | hBOOL(v5) | ? [v6: % 62.67/9.22 | fun_fun_a_bool_bool] : ? [v7: bool] : ? [v8: fun_fun_a_bool_bool] % 62.67/9.22 | : ? [v9: bool] : ((hAPP_a85458249l_bool(member_a, v0) = v6 & % 62.67/9.22 | hAPP_fun_a_bool_bool(v6, v2) = v7 & fun_fun_a_bool_bool(v6) & % 62.67/9.22 | bool(v7) & ~ hBOOL(v7)) | % 62.67/9.22 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v8 & % 62.67/9.22 | hAPP_fun_a_bool_bool(v8, v2) = v9 & fun_fun_a_bool_bool(v8) & % 62.67/9.22 | bool(v9) & ~ hBOOL(v9)))) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (fact_290_subsetI) implies: % 62.67/9.22 | (7) ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: % 62.67/9.22 | fun_fun_a_bool_bool] : ! [v3: bool] : ( ~ % 62.67/9.22 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2) | ~ % 62.67/9.22 | (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ fun_a_bool(v1) | ~ % 62.67/9.22 | fun_a_bool(v0) | hBOOL(v3) | ? [v4: x_a] : ? [v5: % 62.67/9.22 | fun_fun_a_bool_bool] : ? [v6: bool] : ? [v7: bool] : % 62.67/9.22 | (hAPP_a85458249l_bool(member_a, v4) = v5 & hAPP_fun_a_bool_bool(v5, % 62.67/9.22 | v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = v7 & % 62.67/9.22 | fun_fun_a_bool_bool(v5) & bool(v7) & bool(v6) & x_a(v4) & hBOOL(v6) % 62.67/9.22 | & ~ hBOOL(v7))) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_0) implies: % 62.67/9.22 | (8) ? [v0: bool] : (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & % 62.67/9.22 | bool(v0) & hBOOL(v0)) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_1) implies: % 62.67/9.22 | (9) ? [v0: fun_fun_a_bool_bool] : ? [v1: fun_a_bool] : ? [v2: bool] : % 62.67/9.22 | (image_pname_a(mgt_call, u) = v1 & % 62.67/9.22 | hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v0 & % 62.67/9.22 | hAPP_fun_a_bool_bool(v0, v1) = v2 & fun_fun_a_bool_bool(v0) & % 62.67/9.22 | fun_a_bool(v1) & bool(v2) & hBOOL(v2)) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_2) implies: % 62.67/9.22 | (10) ? [v0: nat] : ? [v1: fun_nat_bool] : ? [v2: fun_a_bool] : ? [v3: % 62.67/9.22 | nat] : ? [v4: bool] : (hAPP_nat_nat(suc, na) = v0 & % 62.67/9.22 | hAPP_fun_a_bool_nat(finite_card_a, v2) = v3 & % 62.67/9.22 | hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & hAPP_nat_bool(v1, % 62.67/9.22 | v3) = v4 & image_pname_a(mgt_call, u) = v2 & fun_nat_bool(v1) & % 62.67/9.22 | fun_a_bool(v2) & nat(v3) & nat(v0) & bool(v4) & hBOOL(v4)) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_3) implies: % 62.67/9.22 | (11) ? [v0: nat] : ? [v1: fun_a_bool] : ? [v2: nat] : ? [v3: % 62.67/9.22 | fun_nat_nat] : ? [v4: nat] : (minus_minus_nat(v2) = v3 & % 62.67/9.22 | hAPP_nat_nat(v3, v4) = v0 & hAPP_nat_nat(suc, na) = v4 & % 62.67/9.22 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 62.67/9.22 | hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & image_pname_a(mgt_call, % 62.67/9.22 | u) = v1 & fun_nat_nat(v3) & fun_a_bool(v1) & nat(v4) & nat(v2) & % 62.67/9.22 | nat(v0)) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_4) implies: % 62.67/9.22 | (12) ? [v0: fun_fu1430349052l_bool] : ? [v1: bool] : % 62.67/9.22 | (hAPP_p338031245l_bool(member_pname, pn) = v0 & % 62.67/9.22 | hAPP_f1664156314l_bool(v0, u) = v1 & fun_fu1430349052l_bool(v0) & % 62.67/9.22 | bool(v1) & hBOOL(v1)) % 62.67/9.22 | % 62.67/9.22 | ALPHA: (conj_5) implies: % 62.67/9.23 | (13) ? [v0: x_a] : ? [v1: fun_fun_a_bool_bool] : ? [v2: bool] : % 62.67/9.23 | (hAPP_pname_a(mgt_call, pn) = v0 & hAPP_a85458249l_bool(member_a, v0) % 62.67/9.23 | = v1 & hAPP_fun_a_bool_bool(v1, g) = v2 & fun_fun_a_bool_bool(v1) & % 62.67/9.23 | bool(v2) & x_a(v0) & ~ hBOOL(v2)) % 62.67/9.23 | % 62.67/9.23 | ALPHA: (conj_6) implies: % 62.67/9.23 | (14) pname(pn) % 62.67/9.23 | (15) fun_a_bool(g) % 62.67/9.23 | (16) fun_pname_a(mgt_call) % 62.67/9.23 | (17) fun_pname_bool(u) % 62.67/9.23 | (18) ? [v0: x_a] : ? [v1: fun_a_bool] : ? [v2: fun_fun_a_bool_bool] : ? % 62.67/9.23 | [v3: fun_a_bool] : ? [v4: bool] : (hAPP_pname_a(mgt_call, pn) = v0 & % 62.67/9.23 | insert_a(v0, g) = v1 & image_pname_a(mgt_call, u) = v3 & % 62.67/9.23 | hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 62.67/9.23 | hAPP_fun_a_bool_bool(v2, v3) = v4 & fun_fun_a_bool_bool(v2) & % 62.67/9.23 | fun_a_bool(v3) & fun_a_bool(v1) & bool(v4) & x_a(v0) & ~ hBOOL(v4)) % 62.67/9.23 | % 62.67/9.23 | ALPHA: (function-axioms) implies: % 62.67/9.23 | (19) ! [v0: bool] : ! [v1: bool] : ! [v2: fun_a_bool] : ! [v3: % 62.67/9.23 | fun_fun_a_bool_bool] : (v1 = v0 | ~ (hAPP_fun_a_bool_bool(v3, v2) = % 62.67/9.23 | v1) | ~ (hAPP_fun_a_bool_bool(v3, v2) = v0)) % 62.67/9.23 | (20) ! [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! [v2: % 62.67/9.23 | fun_a_bool] : ! [v3: fun_fu1471507361l_bool] : (v1 = v0 | ~ % 62.67/9.23 | (hAPP_f1631501043l_bool(v3, v2) = v1) | ~ % 62.67/9.23 | (hAPP_f1631501043l_bool(v3, v2) = v0)) % 62.67/9.23 | (21) ! [v0: bool] : ! [v1: bool] : ! [v2: fun_pname_bool] : ! [v3: % 62.67/9.23 | fun_fu1430349052l_bool] : (v1 = v0 | ~ (hAPP_f1664156314l_bool(v3, % 62.67/9.23 | v2) = v1) | ~ (hAPP_f1664156314l_bool(v3, v2) = v0)) % 62.67/9.23 | (22) ! [v0: fun_a_bool] : ! [v1: fun_a_bool] : ! [v2: fun_pname_bool] : % 62.67/9.23 | ! [v3: fun_pname_a] : (v1 = v0 | ~ (image_pname_a(v3, v2) = v1) | ~ % 62.67/9.23 | (image_pname_a(v3, v2) = v0)) % 62.67/9.23 | (23) ! [v0: fun_pname_bool] : ! [v1: fun_pname_bool] : ! [v2: % 62.67/9.23 | fun_pname_bool] : ! [v3: pname] : (v1 = v0 | ~ (insert_pname(v3, % 62.67/9.23 | v2) = v1) | ~ (insert_pname(v3, v2) = v0)) % 62.67/9.23 | (24) ! [v0: fun_fun_a_bool_bool] : ! [v1: fun_fun_a_bool_bool] : ! [v2: % 62.67/9.23 | x_a] : ! [v3: fun_a_1255737515l_bool] : (v1 = v0 | ~ % 62.67/9.23 | (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, % 62.67/9.23 | v2) = v0)) % 62.67/9.23 | (25) ! [v0: x_a] : ! [v1: x_a] : ! [v2: pname] : ! [v3: fun_pname_a] : % 62.67/9.23 | (v1 = v0 | ~ (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, v2) = % 62.67/9.23 | v0)) % 62.67/9.23 | % 62.67/9.23 | DELTA: instantiating (8) with fresh symbol all_515_0 gives: % 62.67/9.24 | (26) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_515_0 & % 62.67/9.24 | bool(all_515_0) & hBOOL(all_515_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (26) implies: % 62.67/9.24 | (27) hBOOL(all_515_0) % 62.67/9.24 | (28) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_515_0 % 62.67/9.24 | % 62.67/9.24 | DELTA: instantiating (12) with fresh symbols all_517_0, all_517_1 gives: % 62.67/9.24 | (29) hAPP_p338031245l_bool(member_pname, pn) = all_517_1 & % 62.67/9.24 | hAPP_f1664156314l_bool(all_517_1, u) = all_517_0 & % 62.67/9.24 | fun_fu1430349052l_bool(all_517_1) & bool(all_517_0) & hBOOL(all_517_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (29) implies: % 62.67/9.24 | (30) hBOOL(all_517_0) % 62.67/9.24 | (31) hAPP_f1664156314l_bool(all_517_1, u) = all_517_0 % 62.67/9.24 | (32) hAPP_p338031245l_bool(member_pname, pn) = all_517_1 % 62.67/9.24 | % 62.67/9.24 | DELTA: instantiating (9) with fresh symbols all_519_0, all_519_1, all_519_2 % 62.67/9.24 | gives: % 62.67/9.24 | (33) image_pname_a(mgt_call, u) = all_519_1 & % 62.67/9.24 | hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_519_2 & % 62.67/9.24 | hAPP_fun_a_bool_bool(all_519_2, all_519_1) = all_519_0 & % 62.67/9.24 | fun_fun_a_bool_bool(all_519_2) & fun_a_bool(all_519_1) & % 62.67/9.24 | bool(all_519_0) & hBOOL(all_519_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (33) implies: % 62.67/9.24 | (34) hBOOL(all_519_0) % 62.67/9.24 | (35) hAPP_fun_a_bool_bool(all_519_2, all_519_1) = all_519_0 % 62.67/9.24 | (36) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_519_2 % 62.67/9.24 | (37) image_pname_a(mgt_call, u) = all_519_1 % 62.67/9.24 | % 62.67/9.24 | DELTA: instantiating (13) with fresh symbols all_521_0, all_521_1, all_521_2 % 62.67/9.24 | gives: % 62.67/9.24 | (38) hAPP_pname_a(mgt_call, pn) = all_521_2 & % 62.67/9.24 | hAPP_a85458249l_bool(member_a, all_521_2) = all_521_1 & % 62.67/9.24 | hAPP_fun_a_bool_bool(all_521_1, g) = all_521_0 & % 62.67/9.24 | fun_fun_a_bool_bool(all_521_1) & bool(all_521_0) & x_a(all_521_2) & ~ % 62.67/9.24 | hBOOL(all_521_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (38) implies: % 62.67/9.24 | (39) hAPP_a85458249l_bool(member_a, all_521_2) = all_521_1 % 62.67/9.24 | (40) hAPP_pname_a(mgt_call, pn) = all_521_2 % 62.67/9.24 | % 62.67/9.24 | DELTA: instantiating (10) with fresh symbols all_529_0, all_529_1, all_529_2, % 62.67/9.24 | all_529_3, all_529_4 gives: % 62.67/9.24 | (41) hAPP_nat_nat(suc, na) = all_529_4 & hAPP_fun_a_bool_nat(finite_card_a, % 62.67/9.24 | all_529_2) = all_529_1 & hAPP_n1699378549t_bool(ord_less_eq_nat, % 62.67/9.24 | all_529_4) = all_529_3 & hAPP_nat_bool(all_529_3, all_529_1) = % 62.67/9.24 | all_529_0 & image_pname_a(mgt_call, u) = all_529_2 & % 62.67/9.24 | fun_nat_bool(all_529_3) & fun_a_bool(all_529_2) & nat(all_529_1) & % 62.67/9.24 | nat(all_529_4) & bool(all_529_0) & hBOOL(all_529_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (41) implies: % 62.67/9.24 | (42) fun_a_bool(all_529_2) % 62.67/9.24 | (43) image_pname_a(mgt_call, u) = all_529_2 % 62.67/9.24 | % 62.67/9.24 | DELTA: instantiating (18) with fresh symbols all_531_0, all_531_1, all_531_2, % 62.67/9.24 | all_531_3, all_531_4 gives: % 62.67/9.24 | (44) hAPP_pname_a(mgt_call, pn) = all_531_4 & insert_a(all_531_4, g) = % 62.67/9.24 | all_531_3 & image_pname_a(mgt_call, u) = all_531_1 & % 62.67/9.24 | hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_531_3) = all_531_2 % 62.67/9.24 | & hAPP_fun_a_bool_bool(all_531_2, all_531_1) = all_531_0 & % 62.67/9.24 | fun_fun_a_bool_bool(all_531_2) & fun_a_bool(all_531_1) & % 62.67/9.24 | fun_a_bool(all_531_3) & bool(all_531_0) & x_a(all_531_4) & ~ % 62.67/9.24 | hBOOL(all_531_0) % 62.67/9.24 | % 62.67/9.24 | ALPHA: (44) implies: % 62.67/9.24 | (45) ~ hBOOL(all_531_0) % 62.67/9.24 | (46) x_a(all_531_4) % 62.67/9.24 | (47) fun_a_bool(all_531_3) % 62.67/9.24 | (48) hAPP_fun_a_bool_bool(all_531_2, all_531_1) = all_531_0 % 62.67/9.24 | (49) hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_531_3) = all_531_2 % 62.67/9.24 | (50) image_pname_a(mgt_call, u) = all_531_1 % 62.67/9.24 | (51) insert_a(all_531_4, g) = all_531_3 % 62.67/9.25 | (52) hAPP_pname_a(mgt_call, pn) = all_531_4 % 62.67/9.25 | % 62.67/9.25 | DELTA: instantiating (11) with fresh symbols all_533_0, all_533_1, all_533_2, % 62.67/9.25 | all_533_3, all_533_4 gives: % 62.67/9.25 | (53) minus_minus_nat(all_533_2) = all_533_1 & hAPP_nat_nat(all_533_1, % 62.67/9.25 | all_533_0) = all_533_4 & hAPP_nat_nat(suc, na) = all_533_0 & % 62.67/9.25 | hAPP_fun_a_bool_nat(finite_card_a, all_533_3) = all_533_2 & % 62.67/9.25 | hAPP_fun_a_bool_nat(finite_card_a, g) = all_533_4 & % 62.67/9.25 | image_pname_a(mgt_call, u) = all_533_3 & fun_nat_nat(all_533_1) & % 62.67/9.25 | fun_a_bool(all_533_3) & nat(all_533_0) & nat(all_533_2) & % 62.67/9.25 | nat(all_533_4) % 62.67/9.25 | % 62.67/9.25 | ALPHA: (53) implies: % 62.67/9.25 | (54) image_pname_a(mgt_call, u) = all_533_3 % 62.67/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (22) with all_529_2, all_531_1, u, mgt_call, % 62.82/9.25 | simplifying with (43), (50) gives: % 62.82/9.25 | (55) all_531_1 = all_529_2 % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (22) with all_531_1, all_533_3, u, mgt_call, % 62.82/9.25 | simplifying with (50), (54) gives: % 62.82/9.25 | (56) all_533_3 = all_531_1 % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (22) with all_519_1, all_533_3, u, mgt_call, % 62.82/9.25 | simplifying with (37), (54) gives: % 62.82/9.25 | (57) all_533_3 = all_519_1 % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (25) with all_521_2, all_531_4, pn, mgt_call, % 62.82/9.25 | simplifying with (40), (52) gives: % 62.82/9.25 | (58) all_531_4 = all_521_2 % 62.82/9.25 | % 62.82/9.25 | COMBINE_EQS: (56), (57) imply: % 62.82/9.25 | (59) all_531_1 = all_519_1 % 62.82/9.25 | % 62.82/9.25 | SIMP: (59) implies: % 62.82/9.25 | (60) all_531_1 = all_519_1 % 62.82/9.25 | % 62.82/9.25 | COMBINE_EQS: (55), (60) imply: % 62.82/9.25 | (61) all_529_2 = all_519_1 % 62.82/9.25 | % 62.82/9.25 | SIMP: (61) implies: % 62.82/9.25 | (62) all_529_2 = all_519_1 % 62.82/9.25 | % 62.82/9.25 | REDUCE: (51), (58) imply: % 62.82/9.25 | (63) insert_a(all_521_2, g) = all_531_3 % 62.82/9.25 | % 62.82/9.25 | REDUCE: (48), (60) imply: % 62.82/9.25 | (64) hAPP_fun_a_bool_bool(all_531_2, all_519_1) = all_531_0 % 62.82/9.25 | % 62.82/9.25 | REDUCE: (42), (62) imply: % 62.82/9.25 | (65) fun_a_bool(all_519_1) % 62.82/9.25 | % 62.82/9.25 | REDUCE: (46), (58) imply: % 62.82/9.25 | (66) x_a(all_521_2) % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (7) with all_519_1, all_531_3, all_531_2, % 62.82/9.25 | all_531_0, simplifying with (45), (47), (49), (64), (65) gives: % 62.82/9.25 | (67) ? [v0: x_a] : ? [v1: fun_fun_a_bool_bool] : ? [v2: bool] : ? [v3: % 62.82/9.25 | bool] : (hAPP_a85458249l_bool(member_a, v0) = v1 & % 62.82/9.25 | hAPP_fun_a_bool_bool(v1, all_531_3) = v2 & hAPP_fun_a_bool_bool(v1, % 62.82/9.25 | all_519_1) = v3 & fun_fun_a_bool_bool(v1) & bool(v3) & bool(v2) & % 62.82/9.25 | x_a(v0) & hBOOL(v2) & ~ hBOOL(v3)) % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (2) with g, mgt_call, u, all_519_2, all_519_1, % 62.82/9.25 | all_519_0, simplifying with (15), (16), (17), (34), (35), (36), % 62.82/9.25 | (37) gives: % 62.82/9.25 | (68) ? [v0: bool] : ? [v1: bool] : % 62.82/9.25 | ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & bool(v0) & ~ % 62.82/9.25 | hBOOL(v0)) | (hAPP_fun_a_bool_bool(finite_finite_a, g) = v1 & % 62.82/9.25 | bool(v1) & hBOOL(v1))) % 62.82/9.25 | % 62.82/9.25 | GROUND_INST: instantiating (3) with mgt_call, u, g, all_519_2, all_519_1, % 62.82/9.25 | all_519_0, simplifying with (15), (16), (17), (34), (35), (36), % 62.82/9.25 | (37) gives: % 62.82/9.26 | (69) ? [v0: bool] : ? [v1: fun_pname_bool] : ? [v2: % 62.82/9.26 | fun_fu1430349052l_bool] : ? [v3: bool] : ? [v4: bool] : ? [v5: % 62.82/9.26 | fun_a_bool] : (fun_pname_bool(v1) & ((v5 = g & % 62.82/9.26 | image_pname_a(mgt_call, v1) = g & % 62.82/9.26 | hAPP_f434788991l_bool(ord_le313189616e_bool, v1) = v2 & % 62.82/9.26 | hAPP_f1664156314l_bool(v2, u) = v3 & % 62.82/9.26 | hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & % 62.82/9.26 | fun_fu1430349052l_bool(v2) & bool(v4) & bool(v3) & hBOOL(v4) & % 62.82/9.26 | hBOOL(v3)) | (hAPP_fun_a_bool_bool(finite_finite_a, g) = v0 & % 62.82/9.26 | bool(v0) & ~ hBOOL(v0)))) % 62.82/9.26 | % 62.82/9.26 | GROUND_INST: instantiating (6) with all_521_2, g, all_519_1, all_531_3, % 62.82/9.26 | all_531_2, all_531_0, simplifying with (15), (45), (49), (63), % 62.82/9.26 | (64), (65), (66) gives: % 62.82/9.26 | (70) ? [v0: fun_fun_a_bool_bool] : ? [v1: bool] : ? [v2: % 62.82/9.26 | fun_fun_a_bool_bool] : ? [v3: bool] : % 62.82/9.26 | ((hAPP_a85458249l_bool(member_a, all_521_2) = v0 & % 62.82/9.26 | hAPP_fun_a_bool_bool(v0, all_519_1) = v1 & fun_fun_a_bool_bool(v0) % 62.82/9.26 | & bool(v1) & ~ hBOOL(v1)) | % 62.82/9.26 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v2 & % 62.82/9.26 | hAPP_fun_a_bool_bool(v2, all_519_1) = v3 & fun_fun_a_bool_bool(v2) % 62.82/9.26 | & bool(v3) & ~ hBOOL(v3))) % 62.82/9.26 | % 62.82/9.26 | GROUND_INST: instantiating (5) with pn, u, all_517_1, all_517_0, simplifying % 62.82/9.26 | with (14), (17), (30), (31), (32) gives: % 62.82/9.26 | (71) insert_pname(pn, u) = u % 62.82/9.26 | % 62.82/9.26 | GROUND_INST: instantiating (1) with pn, u, all_517_1, all_517_0, simplifying % 62.82/9.26 | with (14), (17), (31), (32) gives: % 62.82/9.26 | (72) ? [v0: bool] : ? [v1: fun_pname_bool] : ? [v2: nat] : ? [v3: nat] % 62.82/9.26 | : ? [v4: nat] : ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 % 62.82/9.26 | & bool(v0) & ~ hBOOL(v0)) | (( ~ hBOOL(all_517_0) | (v3 = v2 & % 62.82/9.26 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 62.82/9.26 | hAPP_f921600141ol_nat(finite_card_pname, u) = v2 & % 62.82/9.26 | insert_pname(pn, u) = v1 & fun_pname_bool(v1) & nat(v2))) & % 62.82/9.26 | (hBOOL(all_517_0) | (v4 = v2 & hAPP_nat_nat(suc, v3) = v2 & % 62.82/9.26 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 62.82/9.26 | hAPP_f921600141ol_nat(finite_card_pname, u) = v3 & % 62.82/9.26 | insert_pname(pn, u) = v1 & fun_pname_bool(v1) & nat(v3) & % 62.82/9.26 | nat(v2))))) % 62.82/9.26 | % 62.82/9.26 | DELTA: instantiating (68) with fresh symbols all_650_0, all_650_1 gives: % 62.82/9.26 | (73) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_650_1 & % 62.82/9.26 | bool(all_650_1) & ~ hBOOL(all_650_1)) | % 62.82/9.26 | (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_650_0 & % 62.82/9.26 | bool(all_650_0) & hBOOL(all_650_0)) % 62.82/9.26 | % 62.82/9.26 | DELTA: instantiating (67) with fresh symbols all_654_0, all_654_1, all_654_2, % 62.82/9.26 | all_654_3 gives: % 62.82/9.26 | (74) hAPP_a85458249l_bool(member_a, all_654_3) = all_654_2 & % 62.82/9.26 | hAPP_fun_a_bool_bool(all_654_2, all_531_3) = all_654_1 & % 62.82/9.26 | hAPP_fun_a_bool_bool(all_654_2, all_519_1) = all_654_0 & % 62.82/9.26 | fun_fun_a_bool_bool(all_654_2) & bool(all_654_0) & bool(all_654_1) & % 62.82/9.26 | x_a(all_654_3) & hBOOL(all_654_1) & ~ hBOOL(all_654_0) % 62.82/9.26 | % 62.82/9.26 | ALPHA: (74) implies: % 62.82/9.26 | (75) ~ hBOOL(all_654_0) % 62.82/9.26 | (76) x_a(all_654_3) % 62.82/9.26 | (77) hAPP_fun_a_bool_bool(all_654_2, all_519_1) = all_654_0 % 62.82/9.26 | (78) hAPP_a85458249l_bool(member_a, all_654_3) = all_654_2 % 62.82/9.26 | % 62.82/9.26 | DELTA: instantiating (70) with fresh symbols all_656_0, all_656_1, all_656_2, % 62.82/9.26 | all_656_3 gives: % 62.82/9.26 | (79) (hAPP_a85458249l_bool(member_a, all_521_2) = all_656_3 & % 62.82/9.26 | hAPP_fun_a_bool_bool(all_656_3, all_519_1) = all_656_2 & % 62.82/9.26 | fun_fun_a_bool_bool(all_656_3) & bool(all_656_2) & ~ % 62.82/9.26 | hBOOL(all_656_2)) | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, % 62.82/9.26 | g) = all_656_1 & hAPP_fun_a_bool_bool(all_656_1, all_519_1) = % 62.82/9.26 | all_656_0 & fun_fun_a_bool_bool(all_656_1) & bool(all_656_0) & ~ % 62.82/9.26 | hBOOL(all_656_0)) % 62.82/9.26 | % 62.82/9.26 | DELTA: instantiating (69) with fresh symbols all_658_0, all_658_1, all_658_2, % 62.82/9.26 | all_658_3, all_658_4, all_658_5 gives: % 62.82/9.27 | (80) fun_pname_bool(all_658_4) & ((all_658_0 = g & image_pname_a(mgt_call, % 62.82/9.27 | all_658_4) = g & hAPP_f434788991l_bool(ord_le313189616e_bool, % 62.82/9.27 | all_658_4) = all_658_3 & hAPP_f1664156314l_bool(all_658_3, u) = % 62.82/9.27 | all_658_2 & hAPP_f1664156314l_bool(finite_finite_pname, all_658_4) % 62.82/9.27 | = all_658_1 & fun_fu1430349052l_bool(all_658_3) & bool(all_658_1) % 62.82/9.27 | & bool(all_658_2) & hBOOL(all_658_1) & hBOOL(all_658_2)) | % 62.82/9.27 | (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_658_5 & % 62.82/9.27 | bool(all_658_5) & ~ hBOOL(all_658_5))) % 62.82/9.27 | % 62.82/9.27 | ALPHA: (80) implies: % 62.82/9.27 | (81) (all_658_0 = g & image_pname_a(mgt_call, all_658_4) = g & % 62.82/9.27 | hAPP_f434788991l_bool(ord_le313189616e_bool, all_658_4) = all_658_3 % 62.82/9.27 | & hAPP_f1664156314l_bool(all_658_3, u) = all_658_2 & % 62.82/9.27 | hAPP_f1664156314l_bool(finite_finite_pname, all_658_4) = all_658_1 & % 62.82/9.27 | fun_fu1430349052l_bool(all_658_3) & bool(all_658_1) & % 62.82/9.27 | bool(all_658_2) & hBOOL(all_658_1) & hBOOL(all_658_2)) | % 62.82/9.27 | (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_658_5 & % 62.82/9.27 | bool(all_658_5) & ~ hBOOL(all_658_5)) % 62.82/9.27 | % 62.82/9.27 | DELTA: instantiating (72) with fresh symbols all_661_0, all_661_1, all_661_2, % 62.82/9.27 | all_661_3, all_661_4 gives: % 62.82/9.27 | (82) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_661_4 & % 62.82/9.27 | bool(all_661_4) & ~ hBOOL(all_661_4)) | (( ~ hBOOL(all_517_0) | % 62.82/9.27 | (all_661_1 = all_661_2 & hAPP_f921600141ol_nat(finite_card_pname, % 62.82/9.27 | all_661_3) = all_661_2 & % 62.82/9.27 | hAPP_f921600141ol_nat(finite_card_pname, u) = all_661_2 & % 62.82/9.27 | insert_pname(pn, u) = all_661_3 & fun_pname_bool(all_661_3) & % 62.82/9.27 | nat(all_661_2))) & (hBOOL(all_517_0) | (all_661_0 = all_661_2 & % 62.82/9.27 | hAPP_nat_nat(suc, all_661_1) = all_661_2 & % 62.82/9.27 | hAPP_f921600141ol_nat(finite_card_pname, all_661_3) = all_661_2 % 62.82/9.27 | & hAPP_f921600141ol_nat(finite_card_pname, u) = all_661_1 & % 62.82/9.27 | insert_pname(pn, u) = all_661_3 & fun_pname_bool(all_661_3) & % 62.82/9.27 | nat(all_661_1) & nat(all_661_2)))) % 62.82/9.27 | % 62.82/9.27 | BETA: splitting (73) gives: % 62.82/9.27 | % 62.82/9.27 | Case 1: % 62.82/9.27 | | % 62.82/9.27 | | (83) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_650_1 & % 62.82/9.27 | | bool(all_650_1) & ~ hBOOL(all_650_1) % 62.82/9.27 | | % 62.82/9.27 | | ALPHA: (83) implies: % 62.82/9.27 | | (84) ~ hBOOL(all_650_1) % 62.82/9.27 | | (85) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_650_1 % 62.82/9.27 | | % 62.82/9.27 | | GROUND_INST: instantiating (21) with all_515_0, all_650_1, u, % 62.82/9.27 | | finite_finite_pname, simplifying with (28), (85) gives: % 62.82/9.27 | | (86) all_650_1 = all_515_0 % 62.82/9.27 | | % 62.82/9.27 | | REDUCE: (84), (86) imply: % 62.82/9.27 | | (87) ~ hBOOL(all_515_0) % 62.82/9.27 | | % 62.82/9.27 | | PRED_UNIFY: (27), (87) imply: % 62.82/9.27 | | (88) $false % 62.82/9.27 | | % 62.82/9.27 | | CLOSE: (88) is inconsistent. % 62.82/9.27 | | % 62.82/9.27 | Case 2: % 62.82/9.27 | | % 62.82/9.27 | | (89) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_650_0 & % 62.82/9.27 | | bool(all_650_0) & hBOOL(all_650_0) % 62.82/9.27 | | % 62.82/9.27 | | ALPHA: (89) implies: % 62.82/9.27 | | (90) hBOOL(all_650_0) % 62.82/9.27 | | (91) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_650_0 % 62.82/9.27 | | % 62.82/9.27 | | BETA: splitting (79) gives: % 62.82/9.27 | | % 62.82/9.27 | | Case 1: % 62.82/9.27 | | | % 62.82/9.27 | | | (92) hAPP_a85458249l_bool(member_a, all_521_2) = all_656_3 & % 62.82/9.27 | | | hAPP_fun_a_bool_bool(all_656_3, all_519_1) = all_656_2 & % 62.82/9.27 | | | fun_fun_a_bool_bool(all_656_3) & bool(all_656_2) & ~ % 62.82/9.27 | | | hBOOL(all_656_2) % 62.82/9.27 | | | % 62.82/9.27 | | | ALPHA: (92) implies: % 62.82/9.27 | | | (93) ~ hBOOL(all_656_2) % 62.82/9.27 | | | (94) hAPP_fun_a_bool_bool(all_656_3, all_519_1) = all_656_2 % 62.82/9.27 | | | (95) hAPP_a85458249l_bool(member_a, all_521_2) = all_656_3 % 62.82/9.27 | | | % 62.82/9.27 | | | BETA: splitting (82) gives: % 62.82/9.27 | | | % 62.82/9.27 | | | Case 1: % 62.82/9.27 | | | | % 62.82/9.27 | | | | (96) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_661_4 & % 62.82/9.27 | | | | bool(all_661_4) & ~ hBOOL(all_661_4) % 62.82/9.27 | | | | % 62.82/9.27 | | | | ALPHA: (96) implies: % 62.82/9.27 | | | | (97) ~ hBOOL(all_661_4) % 62.82/9.27 | | | | (98) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_661_4 % 62.82/9.27 | | | | % 62.82/9.27 | | | | GROUND_INST: instantiating (21) with all_515_0, all_661_4, u, % 62.82/9.27 | | | | finite_finite_pname, simplifying with (28), (98) gives: % 62.82/9.27 | | | | (99) all_661_4 = all_515_0 % 62.82/9.27 | | | | % 62.82/9.27 | | | | REDUCE: (97), (99) imply: % 62.82/9.27 | | | | (100) ~ hBOOL(all_515_0) % 62.82/9.27 | | | | % 62.82/9.28 | | | | PRED_UNIFY: (27), (100) imply: % 62.82/9.28 | | | | (101) $false % 62.82/9.28 | | | | % 62.82/9.28 | | | | CLOSE: (101) is inconsistent. % 62.82/9.28 | | | | % 62.82/9.28 | | | Case 2: % 62.82/9.28 | | | | % 62.82/9.28 | | | | (102) ( ~ hBOOL(all_517_0) | (all_661_1 = all_661_2 & % 62.82/9.28 | | | | hAPP_f921600141ol_nat(finite_card_pname, all_661_3) = % 62.82/9.28 | | | | all_661_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 62.82/9.28 | | | | all_661_2 & insert_pname(pn, u) = all_661_3 & % 62.82/9.28 | | | | fun_pname_bool(all_661_3) & nat(all_661_2))) & % 62.82/9.28 | | | | (hBOOL(all_517_0) | (all_661_0 = all_661_2 & hAPP_nat_nat(suc, % 62.82/9.28 | | | | all_661_1) = all_661_2 & % 62.82/9.28 | | | | hAPP_f921600141ol_nat(finite_card_pname, all_661_3) = % 62.82/9.28 | | | | all_661_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 62.82/9.28 | | | | all_661_1 & insert_pname(pn, u) = all_661_3 & % 62.82/9.28 | | | | fun_pname_bool(all_661_3) & nat(all_661_1) & % 62.82/9.28 | | | | nat(all_661_2))) % 62.82/9.28 | | | | % 62.82/9.28 | | | | ALPHA: (102) implies: % 62.82/9.28 | | | | (103) ~ hBOOL(all_517_0) | (all_661_1 = all_661_2 & % 62.82/9.28 | | | | hAPP_f921600141ol_nat(finite_card_pname, all_661_3) = % 62.82/9.28 | | | | all_661_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 62.82/9.28 | | | | all_661_2 & insert_pname(pn, u) = all_661_3 & % 62.82/9.28 | | | | fun_pname_bool(all_661_3) & nat(all_661_2)) % 62.82/9.28 | | | | % 62.82/9.28 | | | | BETA: splitting (103) gives: % 62.82/9.28 | | | | % 62.82/9.28 | | | | Case 1: % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | (104) ~ hBOOL(all_517_0) % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | PRED_UNIFY: (30), (104) imply: % 62.82/9.28 | | | | | (105) $false % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | CLOSE: (105) is inconsistent. % 62.82/9.28 | | | | | % 62.82/9.28 | | | | Case 2: % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | (106) all_661_1 = all_661_2 & % 62.82/9.28 | | | | | hAPP_f921600141ol_nat(finite_card_pname, all_661_3) = % 62.82/9.28 | | | | | all_661_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 62.82/9.28 | | | | | all_661_2 & insert_pname(pn, u) = all_661_3 & % 62.82/9.28 | | | | | fun_pname_bool(all_661_3) & nat(all_661_2) % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | ALPHA: (106) implies: % 62.82/9.28 | | | | | (107) fun_pname_bool(all_661_3) % 62.82/9.28 | | | | | (108) insert_pname(pn, u) = all_661_3 % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | BETA: splitting (81) gives: % 62.82/9.28 | | | | | % 62.82/9.28 | | | | | Case 1: % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (23) with u, all_661_3, u, pn, % 62.82/9.28 | | | | | | simplifying with (71), (108) gives: % 62.82/9.28 | | | | | | (109) all_661_3 = u % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (24) with all_521_1, all_656_3, % 62.82/9.28 | | | | | | all_521_2, member_a, simplifying with (39), (95) gives: % 62.82/9.28 | | | | | | (110) all_656_3 = all_521_1 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | REDUCE: (94), (110) imply: % 62.82/9.28 | | | | | | (111) hAPP_fun_a_bool_bool(all_521_1, all_519_1) = all_656_2 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (4) with u, all_521_2, mgt_call, pn, % 62.82/9.28 | | | | | | all_517_1, all_517_0, all_521_1, all_519_1, all_656_2, % 62.82/9.28 | | | | | | simplifying with (14), (16), (17), (30), (31), (32), % 62.82/9.28 | | | | | | (37), (39), (66), (93), (111) gives: % 62.82/9.28 | | | | | | (112) ? [v0: any] : ( ~ (v0 = all_521_2) & % 62.82/9.28 | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & x_a(v0)) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (4) with u, all_654_3, mgt_call, pn, % 62.82/9.28 | | | | | | all_517_1, all_517_0, all_654_2, all_519_1, all_654_0, % 62.82/9.28 | | | | | | simplifying with (14), (16), (17), (30), (31), (32), % 62.82/9.28 | | | | | | (37), (75), (76), (77), (78) gives: % 62.82/9.28 | | | | | | (113) ? [v0: any] : ( ~ (v0 = all_654_3) & % 62.82/9.28 | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & x_a(v0)) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | DELTA: instantiating (113) with fresh symbol all_720_0 gives: % 62.82/9.28 | | | | | | (114) ~ (all_720_0 = all_654_3) & hAPP_pname_a(mgt_call, pn) = % 62.82/9.28 | | | | | | all_720_0 & x_a(all_720_0) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | ALPHA: (114) implies: % 62.82/9.28 | | | | | | (115) hAPP_pname_a(mgt_call, pn) = all_720_0 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | DELTA: instantiating (112) with fresh symbol all_726_0 gives: % 62.82/9.28 | | | | | | (116) ~ (all_726_0 = all_521_2) & hAPP_pname_a(mgt_call, pn) = % 62.82/9.28 | | | | | | all_726_0 & x_a(all_726_0) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | ALPHA: (116) implies: % 62.82/9.28 | | | | | | (117) ~ (all_726_0 = all_521_2) % 62.82/9.28 | | | | | | (118) hAPP_pname_a(mgt_call, pn) = all_726_0 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (25) with all_521_2, all_726_0, pn, % 62.82/9.28 | | | | | | mgt_call, simplifying with (40), (118) gives: % 62.82/9.28 | | | | | | (119) all_726_0 = all_521_2 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (25) with all_720_0, all_726_0, pn, % 62.82/9.28 | | | | | | mgt_call, simplifying with (115), (118) gives: % 62.82/9.28 | | | | | | (120) all_726_0 = all_720_0 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | COMBINE_EQS: (119), (120) imply: % 62.82/9.28 | | | | | | (121) all_720_0 = all_521_2 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | REDUCE: (117), (119) imply: % 62.82/9.28 | | | | | | (122) $false % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | CLOSE: (122) is inconsistent. % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | Case 2: % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | (123) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_658_5 & % 62.82/9.28 | | | | | | bool(all_658_5) & ~ hBOOL(all_658_5) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | ALPHA: (123) implies: % 62.82/9.28 | | | | | | (124) ~ hBOOL(all_658_5) % 62.82/9.28 | | | | | | (125) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_658_5 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | GROUND_INST: instantiating (19) with all_650_0, all_658_5, g, % 62.82/9.28 | | | | | | finite_finite_a, simplifying with (91), (125) gives: % 62.82/9.28 | | | | | | (126) all_658_5 = all_650_0 % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | REDUCE: (124), (126) imply: % 62.82/9.28 | | | | | | (127) ~ hBOOL(all_650_0) % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | PRED_UNIFY: (90), (127) imply: % 62.82/9.28 | | | | | | (128) $false % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | | CLOSE: (128) is inconsistent. % 62.82/9.28 | | | | | | % 62.82/9.28 | | | | | End of split % 62.82/9.28 | | | | | % 62.82/9.28 | | | | End of split % 62.82/9.28 | | | | % 62.82/9.28 | | | End of split % 62.82/9.28 | | | % 62.82/9.28 | | Case 2: % 62.82/9.28 | | | % 62.82/9.28 | | | (129) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_656_1 & % 62.82/9.29 | | | hAPP_fun_a_bool_bool(all_656_1, all_519_1) = all_656_0 & % 62.82/9.29 | | | fun_fun_a_bool_bool(all_656_1) & bool(all_656_0) & ~ % 62.82/9.29 | | | hBOOL(all_656_0) % 62.82/9.29 | | | % 62.82/9.29 | | | ALPHA: (129) implies: % 62.82/9.29 | | | (130) ~ hBOOL(all_656_0) % 62.82/9.29 | | | (131) hAPP_fun_a_bool_bool(all_656_1, all_519_1) = all_656_0 % 62.82/9.29 | | | (132) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_656_1 % 62.82/9.29 | | | % 62.82/9.29 | | | GROUND_INST: instantiating (20) with all_519_2, all_656_1, g, % 62.82/9.29 | | | ord_le1311769555a_bool, simplifying with (36), (132) gives: % 62.82/9.29 | | | (133) all_656_1 = all_519_2 % 62.82/9.29 | | | % 62.82/9.29 | | | REDUCE: (131), (133) imply: % 62.82/9.29 | | | (134) hAPP_fun_a_bool_bool(all_519_2, all_519_1) = all_656_0 % 62.82/9.29 | | | % 62.82/9.29 | | | GROUND_INST: instantiating (19) with all_519_0, all_656_0, all_519_1, % 62.82/9.29 | | | all_519_2, simplifying with (35), (134) gives: % 62.82/9.29 | | | (135) all_656_0 = all_519_0 % 62.82/9.29 | | | % 62.82/9.29 | | | REDUCE: (130), (135) imply: % 62.82/9.29 | | | (136) ~ hBOOL(all_519_0) % 62.82/9.29 | | | % 62.82/9.29 | | | PRED_UNIFY: (34), (136) imply: % 62.82/9.29 | | | (137) $false % 62.82/9.29 | | | % 62.82/9.29 | | | CLOSE: (137) is inconsistent. % 62.82/9.29 | | | % 62.82/9.29 | | End of split % 62.82/9.29 | | % 62.82/9.29 | End of split % 62.82/9.29 | % 62.82/9.29 End of proof % 62.82/9.29 % SZS output end Proof for theBenchmark % 62.82/9.29 % 62.82/9.29 8640ms %------------------------------------------------------------------------------