%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW470_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 : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:10 EDT 2023 % Result : Theorem 23.01s 3.77s % Output : Proof 37.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWW470_1 : TPTP v8.1.2. Released v5.3.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n023.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 22:56:41 EDT 2023 % 0.13/0.34 % CPUTime : % 0.67/0.65 ________ _____ % 0.67/0.65 ___ __ \_________(_)________________________________ % 0.67/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.65 % 0.67/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.65 (2023-06-19) % 0.67/0.65 % 0.67/0.65 (c) Philipp Rümmer, 2009-2023 % 0.67/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.66 Amanda Stjerna. % 0.67/0.66 Free software under BSD-3-Clause. % 0.67/0.66 % 0.67/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.66 % 0.67/0.66 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.67/0.68 Running up to 7 provers in parallel. % 0.67/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.87/1.59 Prover 1: Preprocessing ... % 5.87/1.59 Prover 4: Preprocessing ... % 5.87/1.62 Prover 0: Preprocessing ... % 5.87/1.62 Prover 3: Preprocessing ... % 5.87/1.62 Prover 2: Preprocessing ... % 5.87/1.62 Prover 5: Preprocessing ... % 5.87/1.62 Prover 6: Preprocessing ... % 14.22/2.63 Prover 1: Warning: ignoring some quantifiers % 14.81/2.70 Prover 3: Warning: ignoring some quantifiers % 14.81/2.72 Prover 1: Constructing countermodel ... % 14.81/2.74 Prover 3: Constructing countermodel ... % 15.42/2.77 Prover 4: Warning: ignoring some quantifiers % 15.42/2.78 Prover 6: Proving ... % 15.89/2.90 Prover 4: Constructing countermodel ... % 16.59/2.95 Prover 0: Proving ... % 17.59/3.06 Prover 5: Proving ... % 20.64/3.46 Prover 2: Proving ... % 23.01/3.77 Prover 6: proved (3074ms) % 23.01/3.77 % 23.01/3.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.01/3.77 % 23.01/3.77 Prover 5: stopped % 23.01/3.78 Prover 3: stopped % 23.01/3.79 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 23.01/3.79 Prover 0: stopped % 23.01/3.80 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 23.01/3.80 Prover 2: stopped % 23.55/3.83 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 23.55/3.83 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 23.55/3.84 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 25.79/4.13 Prover 8: Preprocessing ... % 26.12/4.16 Prover 7: Preprocessing ... % 26.12/4.18 Prover 10: Preprocessing ... % 26.12/4.18 Prover 13: Preprocessing ... % 26.12/4.20 Prover 11: Preprocessing ... % 29.86/4.64 Prover 8: Warning: ignoring some quantifiers % 29.86/4.68 Prover 8: Constructing countermodel ... % 30.43/4.72 Prover 10: Warning: ignoring some quantifiers % 30.43/4.76 Prover 10: Constructing countermodel ... % 31.86/4.92 Prover 7: Warning: ignoring some quantifiers % 32.21/4.97 Prover 7: Constructing countermodel ... % 32.21/4.98 Prover 11: Warning: ignoring some quantifiers % 32.21/5.00 Prover 13: Warning: ignoring some quantifiers % 32.84/5.05 Prover 11: Constructing countermodel ... % 32.84/5.06 Prover 13: Constructing countermodel ... % 36.80/5.58 Prover 10: Found proof (size 17) % 36.80/5.58 Prover 10: proved (1788ms) % 36.80/5.58 Prover 11: stopped % 36.80/5.58 Prover 13: stopped % 36.80/5.58 Prover 8: stopped % 36.80/5.58 Prover 7: stopped % 36.80/5.59 Prover 4: stopped % 36.80/5.59 Prover 1: stopped % 36.80/5.59 % 36.80/5.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.80/5.59 % 36.80/5.59 % SZS output start Proof for theBenchmark % 36.80/5.60 Assumptions after simplification: % 36.80/5.60 --------------------------------- % 36.80/5.60 % 36.80/5.60 (conj_0) % 37.50/5.63 fun_fu1047394976e_bool(cOMBS_1378840469l_bool) & % 37.50/5.63 fun_fu734682033e_bool(cOMBC_892787026e_bool) & % 37.50/5.63 fun_Ho1630563774a_bool(insert1434104874iple_a) & fun_Ho1877127206a_bool(g) & % 37.50/5.63 fun_Ho1877127206a_bool(bot_bo1208640912a_bool) & fun_bo1549164019l_bool(fconj) % 37.50/5.63 & fun_bool_bool(fNot) & fun_state_bool(b) & fun_a_fun_state_bool(p) & % 37.50/5.63 bool(fFalse) & com(c) & ? [v0: fun_fu832487784l_bool] : ? [v1: % 37.50/5.63 fun_state_bool] : ? [v2: fun_a_fun_state_bool] : ? [v3: % 37.50/5.63 fun_fu2008829792e_bool] : ? [v4: fun_fu1658206819l_bool] : ? [v5: % 37.50/5.63 fun_fu2118559873l_bool] : ? [v6: fun_a_1632297036l_bool] : ? [v7: % 37.50/5.63 fun_a_2117018159e_bool] : ? [v8: fun_fu281355805e_bool] : ? [v9: % 37.50/5.63 fun_fu373216837e_bool] : ? [v10: fun_state_bool] : ? [v11: % 37.50/5.63 fun_a_fun_state_bool] : ? [v12: hoare_1927711152iple_a] : ? [v13: % 37.50/5.63 fun_fu1585556401a_bool] : ? [v14: fun_Ho1877127206a_bool] : ? [v15: bool] % 37.50/5.63 : (cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = v3 & % 37.50/5.63 hAPP_f963367678e_bool(v3, v6) = v7 & % 37.50/5.63 hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 37.50/5.63 hAPP_f762886889e_bool(v8, v10) = v11 & cOMBB_160679318_state(fNot) = v9 & % 37.50/5.63 hAPP_f1759915619e_bool(v9, b) = v10 & cOMBK_bool_state(fFalse) = v1 & % 37.50/5.63 cOMBK_1458035955bool_a(v1) = v2 & cOMBB_188601460_state(fconj) = v4 & % 37.50/5.63 cOMBB_1355796797bool_a(v4) = v5 & hAPP_f1509969235l_bool(v5, p) = v6 & % 37.50/5.63 hAPP_H1975128022a_bool(insert1434104874iple_a, v12) = v13 & % 37.50/5.63 hAPP_f16502863a_bool(v13, bot_bo1208640912a_bool) = v14 & % 37.50/5.63 hoare_1652181356iple_a(v2, c, v11) = v12 & hoare_1617968510rivs_a(g) = v0 & % 37.50/5.63 hAPP_f1454306822l_bool(v0, v14) = v15 & fun_fu1585556401a_bool(v13) & % 37.50/5.63 fun_fu832487784l_bool(v0) & fun_fu1658206819l_bool(v4) & % 37.50/5.63 fun_fu373216837e_bool(v9) & fun_fu281355805e_bool(v8) & % 37.50/5.63 fun_fu2008829792e_bool(v3) & fun_fu2118559873l_bool(v5) & % 37.50/5.63 fun_Ho1877127206a_bool(v14) & fun_state_bool(v10) & fun_state_bool(v1) & % 37.50/5.63 fun_a_2117018159e_bool(v7) & fun_a_1632297036l_bool(v6) & % 37.50/5.63 fun_a_fun_state_bool(v11) & fun_a_fun_state_bool(v2) & % 37.50/5.63 hoare_1927711152iple_a(v12) & bool(v15) & ~ hBOOL(v15)) % 37.50/5.63 % 37.50/5.63 (fact_5_escape) % 37.50/5.64 fun_fu402792811e_bool(cOMBC_2027030106e_bool) & % 37.50/5.64 fun_Ho1630563774a_bool(insert1434104874iple_a) & % 37.50/5.64 fun_Ho1877127206a_bool(bot_bo1208640912a_bool) & % 37.50/5.64 fun_st1506752259e_bool(fequal_state) & ? [v0: fun_st1506752259e_bool] : % 37.50/5.64 (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = v0 & % 37.50/5.64 fun_st1506752259e_bool(v0) & ! [v1: fun_Ho1877127206a_bool] : ! [v2: com] % 37.50/5.64 : ! [v3: fun_a_fun_state_bool] : ! [v4: fun_a_fun_state_bool] : ! [v5: % 37.50/5.64 fun_fu832487784l_bool] : ! [v6: hoare_1927711152iple_a] : ! [v7: % 37.50/5.64 fun_fu1585556401a_bool] : ! [v8: fun_Ho1877127206a_bool] : ! [v9: bool] % 37.50/5.64 : ( ~ (hAPP_H1975128022a_bool(insert1434104874iple_a, v6) = v7) | ~ % 37.50/5.64 (hAPP_f16502863a_bool(v7, bot_bo1208640912a_bool) = v8) | ~ % 37.50/5.64 (hoare_1652181356iple_a(v4, v2, v3) = v6) | ~ (hoare_1617968510rivs_a(v1) % 37.50/5.64 = v5) | ~ (hAPP_f1454306822l_bool(v5, v8) = v9) | ~ % 37.50/5.64 fun_Ho1877127206a_bool(v1) | ~ fun_a_fun_state_bool(v4) | ~ % 37.50/5.64 fun_a_fun_state_bool(v3) | ~ com(v2) | hBOOL(v9) | ? [v10: x_a] : ? % 37.50/5.64 [v11: state] : ? [v12: fun_state_bool] : ? [v13: bool] : ? [v14: % 37.50/5.64 fun_state_bool] : ? [v15: fun_a_fun_state_bool] : ? [v16: % 37.50/5.64 fun_state_bool] : ? [v17: fun_a_fun_state_bool] : ? [v18: % 37.50/5.64 hoare_1927711152iple_a] : ? [v19: fun_fu1585556401a_bool] : ? [v20: % 37.50/5.64 fun_Ho1877127206a_bool] : ? [v21: bool] : (hAPP_state_bool(v12, v11) = % 37.50/5.64 v13 & hAPP_s1806633685e_bool(v0, v11) = v14 & hAPP_a2036067514e_bool(v4, % 37.50/5.64 v10) = v12 & hAPP_a2036067514e_bool(v3, v10) = v16 & % 37.50/5.64 cOMBK_1458035955bool_a(v16) = v17 & cOMBK_1458035955bool_a(v14) = v15 & % 37.50/5.64 hAPP_H1975128022a_bool(insert1434104874iple_a, v18) = v19 & % 37.50/5.64 hAPP_f16502863a_bool(v19, bot_bo1208640912a_bool) = v20 & % 37.50/5.64 hoare_1652181356iple_a(v15, v2, v17) = v18 & hAPP_f1454306822l_bool(v5, % 37.50/5.64 v20) = v21 & fun_fu1585556401a_bool(v19) & fun_Ho1877127206a_bool(v20) % 37.50/5.64 & fun_state_bool(v16) & fun_state_bool(v14) & fun_state_bool(v12) & % 37.50/5.64 fun_a_fun_state_bool(v17) & fun_a_fun_state_bool(v15) & % 37.50/5.64 hoare_1927711152iple_a(v18) & bool(v21) & bool(v13) & state(v11) & % 37.50/5.64 x_a(v10) & hBOOL(v13) & ~ hBOOL(v21)))) % 37.50/5.64 % 37.50/5.64 (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) % 37.50/5.64 ! [v0: bool] : ! [v1: state] : ! [v2: fun_state_bool] : ! [v3: bool] : (v3 % 37.50/5.64 = v0 | ~ (cOMBK_bool_state(v0) = v2) | ~ (hAPP_state_bool(v2, v1) = v3) | % 37.50/5.64 ~ bool(v0) | ~ state(v1)) % 37.50/5.64 % 37.50/5.64 (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 37.50/5.64 ! [v0: fun_state_bool] : ! [v1: x_a] : ! [v2: fun_a_fun_state_bool] : ! % 37.50/5.64 [v3: fun_state_bool] : (v3 = v0 | ~ (hAPP_a2036067514e_bool(v2, v1) = v3) | % 37.50/5.64 ~ (cOMBK_1458035955bool_a(v0) = v2) | ~ fun_state_bool(v0) | ~ x_a(v1)) % 37.50/5.64 % 37.50/5.64 (help_fFalse_1_1_U) % 37.50/5.64 bool(fFalse) & ~ hBOOL(fFalse) % 37.50/5.64 % 37.50/5.64 Further assumptions not needed in the proof: % 37.50/5.64 -------------------------------------------- % 37.50/5.64 fact_0_empty, fact_10_insertCI, fact_11_emptyE, fact_12_singleton__conv2, % 37.50/5.64 fact_13_singleton__conv, fact_14_Collect__conv__if2, fact_15_Collect__conv__if, % 37.50/5.64 fact_16_equals0D, fact_17_Collect__empty__eq, fact_18_empty__iff, % 37.50/5.64 fact_19_empty__Collect__eq, fact_1_triple_Oinject, fact_20_ex__in__conv, % 37.50/5.64 fact_21_all__not__in__conv, fact_22_empty__def, fact_23_insert__absorb, % 37.50/5.64 fact_24_insertI2, fact_25_insert__ident, fact_26_insert__code, % 37.50/5.64 fact_27_insert__iff, fact_28_insert__commute, fact_29_insert__absorb2, % 37.50/5.64 fact_2_cut, fact_30_insert__Collect, fact_31_insert__compr, fact_32_insertI1, % 37.50/5.64 fact_33_insert__compr__raw, fact_34_singleton__inject, fact_35_singletonE, % 37.50/5.64 fact_36_doubleton__eq__iff, fact_37_singleton__iff, fact_38_insert__not__empty, % 37.50/5.64 fact_39_empty__not__insert, fact_3_hoare__derivs_Oinsert, fact_40_the__elem__eq, % 37.50/5.64 fact_41_bot__apply, fact_42_bot__fun__def, fact_43_hoare__derivs_OSkip, % 37.50/5.64 fact_44_Comp, fact_45_triple_Oexhaust, fact_46_Set_Oset__insert, % 37.50/5.64 fact_47_com_Osimps_I13_J, fact_48_com_Osimps_I12_J, fact_49_the__elem__def, % 37.50/5.64 fact_4_constant, fact_50_mk__disjoint__insert, fact_51_com_Osimps_I3_J, % 37.50/5.64 fact_52_the__sym__eq__trivial, fact_53_the__eq__trivial, fact_54_If__def, % 37.50/5.64 fact_55_equals0I, fact_56_the__equality, fact_57_theI, fact_58_the1__equality, % 37.50/5.64 fact_59_theI_H, fact_60_conseq, fact_61_nonempty__iff, fact_62_fold1Set__sing, % 37.50/5.64 fact_63_folding__one_Osingleton, fact_64_bot__empty__eq, % 37.50/5.64 fact_65_empty__fold1SetE, fact_66_fold1Set__nonempty, fact_67_fold1Set_Ointros, % 37.50/5.64 fact_68_folding__one_Oinsert, fact_69_fold1__def, fact_6_conseq2, % 37.50/5.64 fact_70_finite__Collect__conjI, fact_71_finite_OemptyI, fact_72_finite_OinsertI, % 37.50/5.64 fact_73_mem__def, fact_74_Collect__def, fact_75_folding__one_Oeq__fold, % 37.50/5.64 fact_76_fold__graph_OemptyI, fact_77_empty__fold__graphE, % 37.50/5.64 fact_78_fold__graph_OinsertI, fact_79_finite__Collect__disjI, fact_7_conseq1, % 37.50/5.64 fact_80_finite__insert, fact_81_fold1__singleton__def, fact_82_fold1__singleton, % 37.50/5.64 fact_83_folding__one_Oclosed, fact_84_insert__fold1SetE, % 37.50/5.64 fact_85_finite__nonempty__imp__fold1Set, fact_86_finite__induct, % 37.50/5.64 fact_87_finite_Osimps, fact_88_finite__imp__fold__graph, % 37.50/5.64 fact_89_fold1Set_Osimps, fact_8_conseq12, fact_90_fold__graph_Osimps, % 37.50/5.64 fact_91_folding__one__idem_Oinsert__idem, fact_92_finite__ne__induct, % 37.50/5.64 fact_93_folding__one__idem_Oidem, fact_94_folding__one__idem_Oin__idem, % 37.50/5.64 fact_9_insertE, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Ostate_U, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Hoare____Mirabel, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_038, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H_040, % 37.50/5.64 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____yiemogtkbg__Otriple_I, % 37.50/5.64 help_COMBC_1_1_COMBC_000t__a_000tc__HOL__Obool_000tc__fun_Itc__Com__Ostate_Mtc__, % 37.50/5.64 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc, % 37.50/5.64 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__Com__Ostate_000tc__HOL__Obool_U, % 37.50/5.64 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 37.50/5.64 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_00, % 37.50/5.64 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_00_039, % 37.50/5.64 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_00_041, % 37.50/5.64 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____yiemogtkbg__, % 37.50/5.64 help_COMBS_1_1_COMBS_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 37.50/5.64 help_COMBS_1_1_COMBS_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_00, % 37.50/5.64 help_fFalse_1_1_T, help_fNot_1_1_U, help_fNot_2_1_U, help_fconj_1_1_U, % 37.50/5.64 help_fconj_2_1_U, help_fconj_3_1_U, help_fdisj_1_1_U, help_fdisj_2_1_U, % 37.50/5.64 help_fdisj_3_1_U, help_fequal_1_1_fequal_000tc__Com__Ostate_T, % 37.50/5.64 help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_, % 37.50/5.64 help_fequal_1_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____yiemogtkbg__Otriple, % 37.50/5.64 help_fequal_2_1_fequal_000tc__Com__Ostate_T, % 37.50/5.64 help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____yiemogtkbg__Otriple_It__a_J_, % 37.50/5.64 help_fequal_2_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____yiemogtkbg__Otriple, % 37.50/5.64 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 37.50/5.64 % 37.50/5.64 Those formulas are unsatisfiable: % 37.50/5.64 --------------------------------- % 37.50/5.64 % 37.50/5.64 Begin of proof % 37.50/5.64 | % 37.50/5.64 | ALPHA: (fact_5_escape) implies: % 37.50/5.65 | (1) ? [v0: fun_st1506752259e_bool] : % 37.50/5.65 | (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = v0 & % 37.50/5.65 | fun_st1506752259e_bool(v0) & ! [v1: fun_Ho1877127206a_bool] : ! % 37.50/5.65 | [v2: com] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 37.50/5.65 | fun_a_fun_state_bool] : ! [v5: fun_fu832487784l_bool] : ! [v6: % 37.50/5.65 | hoare_1927711152iple_a] : ! [v7: fun_fu1585556401a_bool] : ! [v8: % 37.50/5.65 | fun_Ho1877127206a_bool] : ! [v9: bool] : ( ~ % 37.50/5.65 | (hAPP_H1975128022a_bool(insert1434104874iple_a, v6) = v7) | ~ % 37.50/5.65 | (hAPP_f16502863a_bool(v7, bot_bo1208640912a_bool) = v8) | ~ % 37.50/5.65 | (hoare_1652181356iple_a(v4, v2, v3) = v6) | ~ % 37.50/5.65 | (hoare_1617968510rivs_a(v1) = v5) | ~ (hAPP_f1454306822l_bool(v5, % 37.50/5.65 | v8) = v9) | ~ fun_Ho1877127206a_bool(v1) | ~ % 37.50/5.65 | fun_a_fun_state_bool(v4) | ~ fun_a_fun_state_bool(v3) | ~ com(v2) % 37.50/5.65 | | hBOOL(v9) | ? [v10: x_a] : ? [v11: state] : ? [v12: % 37.50/5.65 | fun_state_bool] : ? [v13: bool] : ? [v14: fun_state_bool] : ? % 37.50/5.65 | [v15: fun_a_fun_state_bool] : ? [v16: fun_state_bool] : ? [v17: % 37.50/5.65 | fun_a_fun_state_bool] : ? [v18: hoare_1927711152iple_a] : ? % 37.50/5.65 | [v19: fun_fu1585556401a_bool] : ? [v20: fun_Ho1877127206a_bool] : % 37.50/5.65 | ? [v21: bool] : (hAPP_state_bool(v12, v11) = v13 & % 37.50/5.65 | hAPP_s1806633685e_bool(v0, v11) = v14 & % 37.50/5.65 | hAPP_a2036067514e_bool(v4, v10) = v12 & % 37.50/5.65 | hAPP_a2036067514e_bool(v3, v10) = v16 & % 37.50/5.65 | cOMBK_1458035955bool_a(v16) = v17 & cOMBK_1458035955bool_a(v14) = % 37.50/5.65 | v15 & hAPP_H1975128022a_bool(insert1434104874iple_a, v18) = v19 & % 37.50/5.65 | hAPP_f16502863a_bool(v19, bot_bo1208640912a_bool) = v20 & % 37.50/5.65 | hoare_1652181356iple_a(v15, v2, v17) = v18 & % 37.50/5.65 | hAPP_f1454306822l_bool(v5, v20) = v21 & % 37.50/5.65 | fun_fu1585556401a_bool(v19) & fun_Ho1877127206a_bool(v20) & % 37.50/5.65 | fun_state_bool(v16) & fun_state_bool(v14) & fun_state_bool(v12) & % 37.50/5.65 | fun_a_fun_state_bool(v17) & fun_a_fun_state_bool(v15) & % 37.50/5.65 | hoare_1927711152iple_a(v18) & bool(v21) & bool(v13) & state(v11) % 37.50/5.65 | & x_a(v10) & hBOOL(v13) & ~ hBOOL(v21)))) % 37.50/5.65 | % 37.50/5.65 | ALPHA: (help_fFalse_1_1_U) implies: % 37.50/5.65 | (2) ~ hBOOL(fFalse) % 37.50/5.65 | % 37.50/5.65 | ALPHA: (conj_0) implies: % 37.50/5.65 | (3) com(c) % 37.50/5.65 | (4) bool(fFalse) % 37.50/5.65 | (5) fun_Ho1877127206a_bool(g) % 37.50/5.65 | (6) ? [v0: fun_fu832487784l_bool] : ? [v1: fun_state_bool] : ? [v2: % 37.50/5.65 | fun_a_fun_state_bool] : ? [v3: fun_fu2008829792e_bool] : ? [v4: % 37.50/5.65 | fun_fu1658206819l_bool] : ? [v5: fun_fu2118559873l_bool] : ? [v6: % 37.50/5.65 | fun_a_1632297036l_bool] : ? [v7: fun_a_2117018159e_bool] : ? [v8: % 37.50/5.65 | fun_fu281355805e_bool] : ? [v9: fun_fu373216837e_bool] : ? [v10: % 37.50/5.65 | fun_state_bool] : ? [v11: fun_a_fun_state_bool] : ? [v12: % 37.50/5.65 | hoare_1927711152iple_a] : ? [v13: fun_fu1585556401a_bool] : ? [v14: % 37.50/5.65 | fun_Ho1877127206a_bool] : ? [v15: bool] : % 37.50/5.65 | (cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = v3 & % 37.50/5.65 | hAPP_f963367678e_bool(v3, v6) = v7 & % 37.50/5.65 | hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 37.50/5.65 | hAPP_f762886889e_bool(v8, v10) = v11 & cOMBB_160679318_state(fNot) = % 37.50/5.65 | v9 & hAPP_f1759915619e_bool(v9, b) = v10 & cOMBK_bool_state(fFalse) = % 37.50/5.65 | v1 & cOMBK_1458035955bool_a(v1) = v2 & cOMBB_188601460_state(fconj) = % 37.50/5.65 | v4 & cOMBB_1355796797bool_a(v4) = v5 & hAPP_f1509969235l_bool(v5, p) % 37.50/5.65 | = v6 & hAPP_H1975128022a_bool(insert1434104874iple_a, v12) = v13 & % 37.50/5.65 | hAPP_f16502863a_bool(v13, bot_bo1208640912a_bool) = v14 & % 37.50/5.65 | hoare_1652181356iple_a(v2, c, v11) = v12 & hoare_1617968510rivs_a(g) % 37.50/5.65 | = v0 & hAPP_f1454306822l_bool(v0, v14) = v15 & % 37.50/5.65 | fun_fu1585556401a_bool(v13) & fun_fu832487784l_bool(v0) & % 37.50/5.65 | fun_fu1658206819l_bool(v4) & fun_fu373216837e_bool(v9) & % 37.50/5.65 | fun_fu281355805e_bool(v8) & fun_fu2008829792e_bool(v3) & % 37.50/5.65 | fun_fu2118559873l_bool(v5) & fun_Ho1877127206a_bool(v14) & % 37.50/5.65 | fun_state_bool(v10) & fun_state_bool(v1) & fun_a_2117018159e_bool(v7) % 37.50/5.65 | & fun_a_1632297036l_bool(v6) & fun_a_fun_state_bool(v11) & % 37.50/5.65 | fun_a_fun_state_bool(v2) & hoare_1927711152iple_a(v12) & bool(v15) & % 37.50/5.65 | ~ hBOOL(v15)) % 37.50/5.65 | % 37.50/5.65 | DELTA: instantiating (6) with fresh symbols all_246_0, all_246_1, all_246_2, % 37.50/5.65 | all_246_3, all_246_4, all_246_5, all_246_6, all_246_7, all_246_8, % 37.50/5.65 | all_246_9, all_246_10, all_246_11, all_246_12, all_246_13, all_246_14, % 37.50/5.65 | all_246_15 gives: % 37.50/5.65 | (7) cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = all_246_12 & % 37.50/5.65 | hAPP_f963367678e_bool(all_246_12, all_246_9) = all_246_8 & % 37.50/5.65 | hAPP_f1261923407e_bool(cOMBC_892787026e_bool, all_246_8) = all_246_7 & % 37.50/5.65 | hAPP_f762886889e_bool(all_246_7, all_246_5) = all_246_4 & % 37.50/5.65 | cOMBB_160679318_state(fNot) = all_246_6 & % 37.50/5.65 | hAPP_f1759915619e_bool(all_246_6, b) = all_246_5 & % 37.50/5.65 | cOMBK_bool_state(fFalse) = all_246_14 & % 37.50/5.65 | cOMBK_1458035955bool_a(all_246_14) = all_246_13 & % 37.50/5.65 | cOMBB_188601460_state(fconj) = all_246_11 & % 37.50/5.65 | cOMBB_1355796797bool_a(all_246_11) = all_246_10 & % 37.50/5.65 | hAPP_f1509969235l_bool(all_246_10, p) = all_246_9 & % 37.50/5.65 | hAPP_H1975128022a_bool(insert1434104874iple_a, all_246_3) = all_246_2 & % 37.50/5.65 | hAPP_f16502863a_bool(all_246_2, bot_bo1208640912a_bool) = all_246_1 & % 37.50/5.65 | hoare_1652181356iple_a(all_246_13, c, all_246_4) = all_246_3 & % 37.50/5.65 | hoare_1617968510rivs_a(g) = all_246_15 & % 37.50/5.65 | hAPP_f1454306822l_bool(all_246_15, all_246_1) = all_246_0 & % 37.50/5.65 | fun_fu1585556401a_bool(all_246_2) & fun_fu832487784l_bool(all_246_15) & % 37.50/5.65 | fun_fu1658206819l_bool(all_246_11) & fun_fu373216837e_bool(all_246_6) & % 37.50/5.65 | fun_fu281355805e_bool(all_246_7) & fun_fu2008829792e_bool(all_246_12) & % 37.50/5.65 | fun_fu2118559873l_bool(all_246_10) & fun_Ho1877127206a_bool(all_246_1) % 37.50/5.65 | & fun_state_bool(all_246_5) & fun_state_bool(all_246_14) & % 37.50/5.65 | fun_a_2117018159e_bool(all_246_8) & fun_a_1632297036l_bool(all_246_9) & % 37.50/5.65 | fun_a_fun_state_bool(all_246_4) & fun_a_fun_state_bool(all_246_13) & % 37.50/5.65 | hoare_1927711152iple_a(all_246_3) & bool(all_246_0) & ~ % 37.50/5.65 | hBOOL(all_246_0) % 37.50/5.65 | % 37.50/5.65 | ALPHA: (7) implies: % 37.50/5.65 | (8) ~ hBOOL(all_246_0) % 37.50/5.65 | (9) fun_a_fun_state_bool(all_246_13) % 37.50/5.66 | (10) fun_a_fun_state_bool(all_246_4) % 37.50/5.66 | (11) fun_state_bool(all_246_14) % 37.50/5.66 | (12) hAPP_f1454306822l_bool(all_246_15, all_246_1) = all_246_0 % 37.50/5.66 | (13) hoare_1617968510rivs_a(g) = all_246_15 % 37.50/5.66 | (14) hoare_1652181356iple_a(all_246_13, c, all_246_4) = all_246_3 % 37.50/5.66 | (15) hAPP_f16502863a_bool(all_246_2, bot_bo1208640912a_bool) = all_246_1 % 37.50/5.66 | (16) hAPP_H1975128022a_bool(insert1434104874iple_a, all_246_3) = all_246_2 % 37.50/5.66 | (17) cOMBK_1458035955bool_a(all_246_14) = all_246_13 % 37.50/5.66 | (18) cOMBK_bool_state(fFalse) = all_246_14 % 37.50/5.66 | % 37.50/5.66 | DELTA: instantiating (1) with fresh symbol all_248_0 gives: % 37.50/5.66 | (19) hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = % 37.50/5.66 | all_248_0 & fun_st1506752259e_bool(all_248_0) & ! [v0: % 37.50/5.66 | fun_Ho1877127206a_bool] : ! [v1: com] : ! [v2: % 37.50/5.66 | fun_a_fun_state_bool] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 37.50/5.66 | fun_fu832487784l_bool] : ! [v5: hoare_1927711152iple_a] : ! [v6: % 37.50/5.66 | fun_fu1585556401a_bool] : ! [v7: fun_Ho1877127206a_bool] : ! [v8: % 37.50/5.66 | bool] : ( ~ (hAPP_H1975128022a_bool(insert1434104874iple_a, v5) = % 37.50/5.66 | v6) | ~ (hAPP_f16502863a_bool(v6, bot_bo1208640912a_bool) = v7) | % 37.50/5.66 | ~ (hoare_1652181356iple_a(v3, v1, v2) = v5) | ~ % 37.50/5.66 | (hoare_1617968510rivs_a(v0) = v4) | ~ (hAPP_f1454306822l_bool(v4, % 37.50/5.66 | v7) = v8) | ~ fun_Ho1877127206a_bool(v0) | ~ % 37.50/5.66 | fun_a_fun_state_bool(v3) | ~ fun_a_fun_state_bool(v2) | ~ com(v1) % 37.50/5.66 | | hBOOL(v8) | ? [v9: x_a] : ? [v10: state] : ? [v11: % 37.50/5.66 | fun_state_bool] : ? [v12: bool] : ? [v13: fun_state_bool] : ? % 37.50/5.66 | [v14: fun_a_fun_state_bool] : ? [v15: fun_state_bool] : ? [v16: % 37.50/5.66 | fun_a_fun_state_bool] : ? [v17: hoare_1927711152iple_a] : ? % 37.50/5.66 | [v18: fun_fu1585556401a_bool] : ? [v19: fun_Ho1877127206a_bool] : % 37.50/5.66 | ? [v20: bool] : (hAPP_state_bool(v11, v10) = v12 & % 37.50/5.66 | hAPP_s1806633685e_bool(all_248_0, v10) = v13 & % 37.50/5.66 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 37.50/5.66 | v9) = v15 & cOMBK_1458035955bool_a(v15) = v16 & % 37.50/5.66 | cOMBK_1458035955bool_a(v13) = v14 & % 37.50/5.66 | hAPP_H1975128022a_bool(insert1434104874iple_a, v17) = v18 & % 37.50/5.66 | hAPP_f16502863a_bool(v18, bot_bo1208640912a_bool) = v19 & % 37.50/5.66 | hoare_1652181356iple_a(v14, v1, v16) = v17 & % 37.50/5.66 | hAPP_f1454306822l_bool(v4, v19) = v20 & % 37.50/5.66 | fun_fu1585556401a_bool(v18) & fun_Ho1877127206a_bool(v19) & % 37.50/5.66 | fun_state_bool(v15) & fun_state_bool(v13) & fun_state_bool(v11) & % 37.50/5.66 | fun_a_fun_state_bool(v16) & fun_a_fun_state_bool(v14) & % 37.50/5.66 | hoare_1927711152iple_a(v17) & bool(v20) & bool(v12) & state(v10) & % 37.50/5.66 | x_a(v9) & hBOOL(v12) & ~ hBOOL(v20))) % 37.50/5.66 | % 37.50/5.66 | ALPHA: (19) implies: % 37.50/5.67 | (20) ! [v0: fun_Ho1877127206a_bool] : ! [v1: com] : ! [v2: % 37.50/5.67 | fun_a_fun_state_bool] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 37.50/5.67 | fun_fu832487784l_bool] : ! [v5: hoare_1927711152iple_a] : ! [v6: % 37.50/5.67 | fun_fu1585556401a_bool] : ! [v7: fun_Ho1877127206a_bool] : ! [v8: % 37.50/5.67 | bool] : ( ~ (hAPP_H1975128022a_bool(insert1434104874iple_a, v5) = % 37.50/5.67 | v6) | ~ (hAPP_f16502863a_bool(v6, bot_bo1208640912a_bool) = v7) | % 37.50/5.67 | ~ (hoare_1652181356iple_a(v3, v1, v2) = v5) | ~ % 37.50/5.67 | (hoare_1617968510rivs_a(v0) = v4) | ~ (hAPP_f1454306822l_bool(v4, % 37.50/5.67 | v7) = v8) | ~ fun_Ho1877127206a_bool(v0) | ~ % 37.50/5.67 | fun_a_fun_state_bool(v3) | ~ fun_a_fun_state_bool(v2) | ~ com(v1) % 37.50/5.67 | | hBOOL(v8) | ? [v9: x_a] : ? [v10: state] : ? [v11: % 37.50/5.67 | fun_state_bool] : ? [v12: bool] : ? [v13: fun_state_bool] : ? % 37.50/5.67 | [v14: fun_a_fun_state_bool] : ? [v15: fun_state_bool] : ? [v16: % 37.50/5.67 | fun_a_fun_state_bool] : ? [v17: hoare_1927711152iple_a] : ? % 37.50/5.67 | [v18: fun_fu1585556401a_bool] : ? [v19: fun_Ho1877127206a_bool] : % 37.50/5.67 | ? [v20: bool] : (hAPP_state_bool(v11, v10) = v12 & % 37.50/5.67 | hAPP_s1806633685e_bool(all_248_0, v10) = v13 & % 37.50/5.67 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 37.50/5.67 | v9) = v15 & cOMBK_1458035955bool_a(v15) = v16 & % 37.50/5.67 | cOMBK_1458035955bool_a(v13) = v14 & % 37.50/5.67 | hAPP_H1975128022a_bool(insert1434104874iple_a, v17) = v18 & % 37.50/5.67 | hAPP_f16502863a_bool(v18, bot_bo1208640912a_bool) = v19 & % 37.50/5.67 | hoare_1652181356iple_a(v14, v1, v16) = v17 & % 37.50/5.67 | hAPP_f1454306822l_bool(v4, v19) = v20 & % 37.50/5.67 | fun_fu1585556401a_bool(v18) & fun_Ho1877127206a_bool(v19) & % 37.50/5.67 | fun_state_bool(v15) & fun_state_bool(v13) & fun_state_bool(v11) & % 37.50/5.67 | fun_a_fun_state_bool(v16) & fun_a_fun_state_bool(v14) & % 37.50/5.67 | hoare_1927711152iple_a(v17) & bool(v20) & bool(v12) & state(v10) & % 37.50/5.67 | x_a(v9) & hBOOL(v12) & ~ hBOOL(v20))) % 37.50/5.67 | % 37.50/5.68 | GROUND_INST: instantiating (20) with g, c, all_246_4, all_246_13, all_246_15, % 37.50/5.68 | all_246_3, all_246_2, all_246_1, all_246_0, simplifying with (3), % 37.50/5.68 | (5), (8), (9), (10), (12), (13), (14), (15), (16) gives: % 37.50/5.68 | (21) ? [v0: x_a] : ? [v1: state] : ? [v2: fun_state_bool] : ? [v3: % 37.50/5.68 | bool] : ? [v4: fun_state_bool] : ? [v5: fun_a_fun_state_bool] : ? % 37.50/5.68 | [v6: fun_state_bool] : ? [v7: fun_a_fun_state_bool] : ? [v8: % 37.50/5.68 | hoare_1927711152iple_a] : ? [v9: fun_fu1585556401a_bool] : ? [v10: % 37.50/5.68 | fun_Ho1877127206a_bool] : ? [v11: bool] : (hAPP_state_bool(v2, v1) % 37.50/5.68 | = v3 & hAPP_s1806633685e_bool(all_248_0, v1) = v4 & % 37.50/5.68 | hAPP_a2036067514e_bool(all_246_4, v0) = v6 & % 37.50/5.68 | hAPP_a2036067514e_bool(all_246_13, v0) = v2 & % 37.50/5.68 | cOMBK_1458035955bool_a(v6) = v7 & cOMBK_1458035955bool_a(v4) = v5 & % 37.50/5.68 | hAPP_H1975128022a_bool(insert1434104874iple_a, v8) = v9 & % 37.50/5.68 | hAPP_f16502863a_bool(v9, bot_bo1208640912a_bool) = v10 & % 37.50/5.68 | hoare_1652181356iple_a(v5, c, v7) = v8 & % 37.50/5.68 | hAPP_f1454306822l_bool(all_246_15, v10) = v11 & % 37.50/5.68 | fun_fu1585556401a_bool(v9) & fun_Ho1877127206a_bool(v10) & % 37.50/5.68 | fun_state_bool(v6) & fun_state_bool(v4) & fun_state_bool(v2) & % 37.50/5.68 | fun_a_fun_state_bool(v7) & fun_a_fun_state_bool(v5) & % 37.50/5.68 | hoare_1927711152iple_a(v8) & bool(v11) & bool(v3) & state(v1) & % 37.50/5.68 | x_a(v0) & hBOOL(v3) & ~ hBOOL(v11)) % 37.50/5.68 | % 37.50/5.68 | DELTA: instantiating (21) with fresh symbols all_282_0, all_282_1, all_282_2, % 37.50/5.68 | all_282_3, all_282_4, all_282_5, all_282_6, all_282_7, all_282_8, % 37.50/5.68 | all_282_9, all_282_10, all_282_11 gives: % 37.50/5.68 | (22) hAPP_state_bool(all_282_9, all_282_10) = all_282_8 & % 37.50/5.68 | hAPP_s1806633685e_bool(all_248_0, all_282_10) = all_282_7 & % 37.50/5.68 | hAPP_a2036067514e_bool(all_246_4, all_282_11) = all_282_5 & % 37.50/5.68 | hAPP_a2036067514e_bool(all_246_13, all_282_11) = all_282_9 & % 37.50/5.68 | cOMBK_1458035955bool_a(all_282_5) = all_282_4 & % 37.50/5.68 | cOMBK_1458035955bool_a(all_282_7) = all_282_6 & % 37.50/5.68 | hAPP_H1975128022a_bool(insert1434104874iple_a, all_282_3) = all_282_2 % 37.50/5.68 | & hAPP_f16502863a_bool(all_282_2, bot_bo1208640912a_bool) = all_282_1 % 37.50/5.68 | & hoare_1652181356iple_a(all_282_6, c, all_282_4) = all_282_3 & % 37.50/5.68 | hAPP_f1454306822l_bool(all_246_15, all_282_1) = all_282_0 & % 37.50/5.68 | fun_fu1585556401a_bool(all_282_2) & fun_Ho1877127206a_bool(all_282_1) % 37.50/5.68 | & fun_state_bool(all_282_5) & fun_state_bool(all_282_7) & % 37.50/5.68 | fun_state_bool(all_282_9) & fun_a_fun_state_bool(all_282_4) & % 37.50/5.68 | fun_a_fun_state_bool(all_282_6) & hoare_1927711152iple_a(all_282_3) & % 37.50/5.68 | bool(all_282_0) & bool(all_282_8) & state(all_282_10) & % 37.50/5.68 | x_a(all_282_11) & hBOOL(all_282_8) & ~ hBOOL(all_282_0) % 37.50/5.68 | % 37.50/5.68 | ALPHA: (22) implies: % 37.50/5.68 | (23) hBOOL(all_282_8) % 37.50/5.68 | (24) x_a(all_282_11) % 37.50/5.68 | (25) state(all_282_10) % 37.50/5.68 | (26) hAPP_a2036067514e_bool(all_246_13, all_282_11) = all_282_9 % 37.50/5.68 | (27) hAPP_state_bool(all_282_9, all_282_10) = all_282_8 % 37.50/5.68 | % 37.50/5.68 | GROUND_INST: instantiating % 37.50/5.68 | (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 37.50/5.68 | with all_246_14, all_282_11, all_246_13, all_282_9, simplifying % 37.50/5.68 | with (11), (17), (24), (26) gives: % 37.50/5.68 | (28) all_282_9 = all_246_14 % 37.50/5.68 | % 37.50/5.68 | REDUCE: (27), (28) imply: % 37.50/5.68 | (29) hAPP_state_bool(all_246_14, all_282_10) = all_282_8 % 37.50/5.68 | % 37.50/5.68 | GROUND_INST: instantiating % 37.50/5.68 | (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) % 37.50/5.68 | with fFalse, all_282_10, all_246_14, all_282_8, simplifying with % 37.50/5.68 | (4), (18), (25), (29) gives: % 37.50/5.68 | (30) all_282_8 = fFalse % 37.50/5.68 | % 37.50/5.68 | REDUCE: (23), (30) imply: % 37.50/5.68 | (31) hBOOL(fFalse) % 37.50/5.68 | % 37.50/5.68 | PRED_UNIFY: (2), (31) imply: % 37.50/5.68 | (32) $false % 37.50/5.68 | % 37.50/5.68 | CLOSE: (32) is inconsistent. % 37.50/5.68 | % 37.50/5.68 End of proof % 37.50/5.68 % SZS output end Proof for theBenchmark % 37.50/5.68 % 37.50/5.68 5026ms %------------------------------------------------------------------------------