%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW470_2 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n004.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 69.32s 9.77s % Output : Proof 139.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470_2 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n004.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 20:44:52 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 18.63/3.18 Prover 2: Preprocessing ... % 18.63/3.18 Prover 5: Preprocessing ... % 18.63/3.18 Prover 0: Preprocessing ... % 18.63/3.31 Prover 1: Preprocessing ... % 19.71/3.35 Prover 3: Preprocessing ... % 19.91/3.40 Prover 6: Preprocessing ... % 19.91/3.40 Prover 4: Preprocessing ... % 44.97/6.68 Prover 3: Warning: ignoring some quantifiers % 46.38/6.86 Prover 3: Constructing countermodel ... % 47.14/6.89 Prover 1: Warning: ignoring some quantifiers % 48.69/7.10 Prover 1: Constructing countermodel ... % 49.49/7.22 Prover 6: Proving ... % 51.79/7.51 Prover 4: Warning: ignoring some quantifiers % 54.61/7.97 Prover 4: Constructing countermodel ... % 58.45/8.39 Prover 0: Proving ... % 69.32/9.77 Prover 6: proved (9132ms) % 69.32/9.77 % 69.32/9.77 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 69.32/9.77 % 69.32/9.77 Prover 0: stopped % 69.32/9.79 Prover 3: stopped % 69.32/9.81 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 69.32/9.81 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 69.32/9.81 Prover 5: Proving ... % 69.32/9.81 Prover 5: stopped % 69.32/9.81 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 69.32/9.81 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 78.42/10.99 Prover 8: Preprocessing ... % 78.42/11.00 Prover 7: Preprocessing ... % 78.83/11.01 Prover 10: Preprocessing ... % 79.21/11.13 Prover 11: Preprocessing ... % 86.29/12.03 Prover 2: Proving ... % 86.76/12.03 Prover 2: stopped % 86.76/12.03 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 93.22/12.87 Prover 10: Warning: ignoring some quantifiers % 93.22/12.87 Prover 13: Preprocessing ... % 93.22/12.91 Prover 8: Warning: ignoring some quantifiers % 94.56/13.05 Prover 10: Constructing countermodel ... % 94.88/13.10 Prover 8: Constructing countermodel ... % 94.88/13.15 Prover 7: Warning: ignoring some quantifiers % 97.60/13.43 Prover 7: Constructing countermodel ... % 97.83/13.47 Prover 11: Warning: ignoring some quantifiers % 102.38/14.11 Prover 11: Constructing countermodel ... % 113.57/15.52 Prover 13: Warning: ignoring some quantifiers % 114.88/15.81 Prover 13: Constructing countermodel ... % 116.87/16.00 Prover 1: stopped % 116.87/16.00 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 119.29/16.27 Prover 13: stopped % 119.29/16.27 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 124.43/16.95 Prover 16: Preprocessing ... % 128.14/17.49 Prover 19: Preprocessing ... % 135.51/18.38 Prover 16: Warning: ignoring some quantifiers % 136.71/18.57 Prover 16: Constructing countermodel ... % 137.36/18.67 Prover 10: Found proof (size 19) % 137.36/18.67 Prover 10: proved (8861ms) % 137.36/18.67 Prover 7: stopped % 137.36/18.67 Prover 11: stopped % 137.36/18.67 Prover 4: stopped % 137.36/18.68 Prover 8: stopped % 137.86/18.71 Prover 16: stopped % 138.95/19.02 Prover 19: Warning: ignoring some quantifiers % 139.25/19.17 Prover 19: Constructing countermodel ... % 139.25/19.17 Prover 19: stopped % 139.25/19.17 % 139.25/19.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 139.25/19.17 % 139.25/19.18 % SZS output start Proof for theBenchmark % 139.25/19.22 Assumptions after simplification: % 139.25/19.22 --------------------------------- % 139.25/19.22 % 139.25/19.22 (conj_0) % 139.97/19.27 fun_fu1631777789e_bool(cOMBB_145932198bool_a) & % 139.97/19.27 fun_fu1340893257l_bool(cOMBB_1355796797bool_a) & % 139.97/19.27 fun_fu1873708859l_bool(cOMBB_188601460_state) & % 139.97/19.27 fun_fu88048803e_bool(cOMBB_160679318_state) & % 139.97/19.27 fun_fu1047394976e_bool(cOMBS_1378840469l_bool) & % 139.97/19.27 fun_fu281355805e_bool(cOMBK_1458035955bool_a) & % 139.97/19.27 fun_fu734682033e_bool(cOMBC_892787026e_bool) & % 139.97/19.27 fun_Ho611385006a_bool(insert1051021594iple_a) & fun_Ho287446294a_bool(g) & % 139.97/19.27 fun_Ho287446294a_bool(bot_bo1766443648a_bool) & fun_bo1549164019l_bool(fconj) % 139.97/19.27 & fun_bo1936561970e_bool(cOMBK_bool_state) & fun_bool_bool(fNot) & % 139.97/19.27 fun_state_bool(b) & fun_a_fun_state_bool(p) & bool(fFalse) & com(c) & ? [v0: % 139.97/19.27 fun_fu1441721944l_bool] : ? [v1: fun_state_bool] : ? [v2: % 139.97/19.27 fun_a_fun_state_bool] : ? [v3: fun_fu2008829792e_bool] : ? [v4: % 139.97/19.27 fun_fu1658206819l_bool] : ? [v5: fun_fu2118559873l_bool] : ? [v6: % 139.97/19.27 fun_a_1632297036l_bool] : ? [v7: fun_a_2117018159e_bool] : ? [v8: % 139.97/19.27 fun_fu281355805e_bool] : ? [v9: fun_fu373216837e_bool] : ? [v10: % 139.97/19.27 fun_state_bool] : ? [v11: fun_a_fun_state_bool] : ? [v12: % 139.97/19.28 hoare_1544627872iple_a] : ? [v13: fun_fu410471825a_bool] : ? [v14: % 139.97/19.28 fun_Ho287446294a_bool] : ? [v15: bool] : % 139.97/19.28 (hAPP_f375255701e_bool(cOMBB_145932198bool_a, cOMBS_1378840469l_bool) = v3 & % 139.97/19.28 hAPP_f963367678e_bool(v3, v6) = v7 & % 139.97/19.28 hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 139.97/19.28 hAPP_f2073279419e_bool(cOMBB_160679318_state, fNot) = v9 & % 139.97/19.28 hAPP_f1759915619e_bool(v9, b) = v10 & % 139.97/19.28 hAPP_b2019457360e_bool(cOMBK_bool_state, fFalse) = v1 & % 139.97/19.28 hAPP_f762886889e_bool(v8, v10) = v11 & % 139.97/19.28 hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v1) = v2 & % 139.97/19.28 hAPP_f1561913689l_bool(cOMBB_188601460_state, fconj) = v4 & % 139.97/19.28 hAPP_f1178339559l_bool(cOMBB_1355796797bool_a, v4) = v5 & % 139.97/19.28 hAPP_f1509969235l_bool(v5, p) = v6 & % 139.97/19.28 hAPP_H762155206a_bool(insert1051021594iple_a, v12) = v13 & % 139.97/19.28 hAPP_f909437487a_bool(v13, bot_bo1766443648a_bool) = v14 & % 139.97/19.28 hoare_196563068iple_a(v2, c, v11) = v12 & hoare_1546678894rivs_a(g) = v0 & % 139.97/19.28 hAPP_f2063540982l_bool(v0, v14) = v15 & fun_fu410471825a_bool(v13) & % 139.97/19.28 fun_fu1441721944l_bool(v0) & fun_fu1658206819l_bool(v4) & % 139.97/19.28 fun_fu373216837e_bool(v9) & fun_fu281355805e_bool(v8) & % 139.97/19.28 fun_fu2008829792e_bool(v3) & fun_fu2118559873l_bool(v5) & % 139.97/19.28 fun_Ho287446294a_bool(v14) & fun_state_bool(v10) & fun_state_bool(v1) & % 139.97/19.28 fun_a_2117018159e_bool(v7) & fun_a_1632297036l_bool(v6) & % 139.97/19.28 fun_a_fun_state_bool(v11) & fun_a_fun_state_bool(v2) & % 139.97/19.28 hoare_1544627872iple_a(v12) & bool(v15) & ~ hBOOL(v15)) % 139.97/19.28 % 139.97/19.28 (fact_10_escape) % 139.97/19.29 fun_fu402792811e_bool(cOMBC_2027030106e_bool) & % 139.97/19.29 fun_fu281355805e_bool(cOMBK_1458035955bool_a) & % 139.97/19.29 fun_Ho611385006a_bool(insert1051021594iple_a) & % 139.97/19.29 fun_Ho287446294a_bool(bot_bo1766443648a_bool) & % 139.97/19.29 fun_st1506752259e_bool(fequal_state) & ? [v0: fun_st1506752259e_bool] : % 139.97/19.29 (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = v0 & % 139.97/19.29 fun_st1506752259e_bool(v0) & ! [v1: fun_Ho287446294a_bool] : ! [v2: com] : % 139.97/19.29 ! [v3: fun_a_fun_state_bool] : ! [v4: fun_a_fun_state_bool] : ! [v5: % 139.97/19.29 fun_fu1441721944l_bool] : ! [v6: hoare_1544627872iple_a] : ! [v7: % 139.97/19.29 fun_fu410471825a_bool] : ! [v8: fun_Ho287446294a_bool] : ! [v9: bool] : % 139.97/19.29 ( ~ (hAPP_H762155206a_bool(insert1051021594iple_a, v6) = v7) | ~ % 139.97/19.29 (hAPP_f909437487a_bool(v7, bot_bo1766443648a_bool) = v8) | ~ % 139.97/19.29 (hoare_196563068iple_a(v4, v2, v3) = v6) | ~ (hoare_1546678894rivs_a(v1) % 139.97/19.29 = v5) | ~ (hAPP_f2063540982l_bool(v5, v8) = v9) | ~ % 139.97/19.29 fun_Ho287446294a_bool(v1) | ~ fun_a_fun_state_bool(v4) | ~ % 139.97/19.29 fun_a_fun_state_bool(v3) | ~ com(v2) | hBOOL(v9) | ? [v10: x_a] : ? % 139.97/19.29 [v11: state] : ? [v12: fun_state_bool] : ? [v13: bool] : ? [v14: % 139.97/19.29 fun_state_bool] : ? [v15: fun_a_fun_state_bool] : ? [v16: % 139.97/19.29 fun_state_bool] : ? [v17: fun_a_fun_state_bool] : ? [v18: % 139.97/19.29 hoare_1544627872iple_a] : ? [v19: fun_fu410471825a_bool] : ? [v20: % 139.97/19.29 fun_Ho287446294a_bool] : ? [v21: bool] : (hAPP_state_bool(v12, v11) = % 139.97/19.29 v13 & hAPP_s1806633685e_bool(v0, v11) = v14 & hAPP_a2036067514e_bool(v4, % 139.97/19.29 v10) = v12 & hAPP_a2036067514e_bool(v3, v10) = v16 & % 139.97/19.29 hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v16) = v17 & % 139.97/19.29 hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v14) = v15 & % 139.97/19.29 hAPP_H762155206a_bool(insert1051021594iple_a, v18) = v19 & % 139.97/19.29 hAPP_f909437487a_bool(v19, bot_bo1766443648a_bool) = v20 & % 139.97/19.29 hoare_196563068iple_a(v15, v2, v17) = v18 & hAPP_f2063540982l_bool(v5, % 139.97/19.29 v20) = v21 & fun_fu410471825a_bool(v19) & fun_Ho287446294a_bool(v20) & % 139.97/19.29 fun_state_bool(v16) & fun_state_bool(v14) & fun_state_bool(v12) & % 139.97/19.29 fun_a_fun_state_bool(v17) & fun_a_fun_state_bool(v15) & % 139.97/19.29 hoare_1544627872iple_a(v18) & bool(v21) & bool(v13) & state(v11) & % 139.97/19.29 x_a(v10) & hBOOL(v13) & ~ hBOOL(v21)))) % 139.97/19.29 % 139.97/19.29 (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) % 139.97/19.29 fun_bo1936561970e_bool(cOMBK_bool_state) & ! [v0: bool] : ! [v1: state] : ! % 139.97/19.29 [v2: fun_state_bool] : ! [v3: bool] : (v3 = v0 | ~ % 139.97/19.29 (hAPP_b2019457360e_bool(cOMBK_bool_state, v0) = v2) | ~ % 139.97/19.29 (hAPP_state_bool(v2, v1) = v3) | ~ bool(v0) | ~ state(v1)) % 139.97/19.29 % 139.97/19.29 (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 139.97/19.30 fun_fu281355805e_bool(cOMBK_1458035955bool_a) & ! [v0: fun_state_bool] : ! % 139.97/19.30 [v1: x_a] : ! [v2: fun_a_fun_state_bool] : ! [v3: fun_state_bool] : (v3 = v0 % 139.97/19.30 | ~ (hAPP_a2036067514e_bool(v2, v1) = v3) | ~ % 139.97/19.30 (hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v0) = v2) | ~ % 139.97/19.30 fun_state_bool(v0) | ~ x_a(v1)) % 139.97/19.30 % 139.97/19.30 (help_fFalse_1_1_U) % 139.97/19.30 bool(fFalse) & ~ hBOOL(fFalse) % 139.97/19.30 % 139.97/19.30 Further assumptions not needed in the proof: % 139.97/19.30 -------------------------------------------- % 139.97/19.30 fact_0_empty, fact_100_insert__compr__raw, fact_101_insert__compr__raw, % 139.97/19.30 fact_102_insert__compr__raw, fact_103_singleton__inject, % 139.97/19.30 fact_104_singleton__inject, fact_105_singleton__inject, fact_106_singletonE, % 139.97/19.30 fact_107_singletonE, fact_108_singletonE, fact_109_doubleton__eq__iff, % 139.97/19.30 fact_110_doubleton__eq__iff, fact_111_doubleton__eq__iff, % 139.97/19.30 fact_112_singleton__iff, fact_113_singleton__iff, fact_114_singleton__iff, % 139.97/19.30 fact_115_insert__not__empty, fact_116_insert__not__empty, % 139.97/19.30 fact_117_insert__not__empty, fact_118_empty__not__insert, % 139.97/19.30 fact_119_empty__not__insert, fact_11_escape, fact_120_empty__not__insert, % 139.97/19.30 fact_121_the__elem__eq, fact_122_the__elem__eq, fact_123_the__elem__eq, % 139.97/19.30 fact_124_bot__apply, fact_125_bot__apply, fact_126_bot__apply, % 139.97/19.30 fact_127_bot__fun__def, fact_128_bot__fun__def, fact_129_bot__fun__def, % 139.97/19.30 fact_12_conseq2, fact_130_hoare__derivs_OSkip, fact_131_hoare__derivs_OSkip, % 139.97/19.30 fact_132_Comp, fact_133_Comp, fact_134_triple_Oexhaust, % 139.97/19.30 fact_135_triple_Oexhaust, fact_136_Set_Oset__insert, fact_137_Set_Oset__insert, % 139.97/19.30 fact_138_Set_Oset__insert, fact_139_mk__disjoint__insert, fact_13_conseq2, % 139.97/19.30 fact_140_mk__disjoint__insert, fact_141_mk__disjoint__insert, fact_142_equals0I, % 139.97/19.30 fact_143_equals0I, fact_144_equals0I, fact_145_conseq, fact_146_conseq, % 139.97/19.30 fact_147_com_Osimps_I13_J, fact_148_com_Osimps_I12_J, fact_149_the__elem__def, % 139.97/19.30 fact_14_conseq1, fact_150_the__elem__def, fact_151_the__elem__def, % 139.97/19.30 fact_152_com_Osimps_I3_J, fact_153_nonempty__iff, fact_154_nonempty__iff, % 139.97/19.30 fact_155_nonempty__iff, fact_156_bot__empty__eq, fact_157_bot__empty__eq, % 139.97/19.30 fact_158_bot__empty__eq, fact_159_Ass, fact_15_conseq1, fact_160_Ass, % 139.97/19.30 fact_161_image__constant__conv, fact_162_image__constant__conv, % 139.97/19.30 fact_163_image__constant__conv, fact_164_image__constant__conv, % 139.97/19.30 fact_165_image__constant__conv, fact_166_image__constant__conv, % 139.97/19.30 fact_167_image__constant__conv, fact_168_image__constant, % 139.97/19.30 fact_169_image__constant, fact_16_conseq12, fact_170_image__constant, % 139.97/19.30 fact_171_image__constant, fact_172_image__constant, fact_173_image__constant, % 139.97/19.30 fact_174_image__constant, fact_175_image__constant, fact_176_image__eqI, % 139.97/19.30 fact_177_image__eqI, fact_178_image__eqI, fact_179_image__eqI, fact_17_conseq12, % 139.97/19.30 fact_180_image__eqI, fact_181_image__eqI, fact_182_image__eqI, % 139.97/19.30 fact_183_image__eqI, fact_184_image__eqI, fact_185_image__ident, % 139.97/19.30 fact_186_image__ident, fact_187_image__ident, fact_188_com_Osimps_I1_J, % 139.97/19.30 fact_189_rev__image__eqI, fact_18_insertE, fact_190_rev__image__eqI, % 139.97/19.30 fact_191_rev__image__eqI, fact_192_rev__image__eqI, fact_193_rev__image__eqI, % 139.97/19.30 fact_194_rev__image__eqI, fact_195_rev__image__eqI, fact_196_rev__image__eqI, % 139.97/19.30 fact_197_rev__image__eqI, fact_198_imageI, fact_199_imageI, fact_19_insertE, % 139.97/19.30 fact_1_empty, fact_200_imageI, fact_201_imageI, fact_202_imageI, % 139.97/19.30 fact_203_imageI, fact_204_imageI, fact_205_imageI, fact_206_imageI, % 139.97/19.30 fact_207_image__iff, fact_208_image__iff, fact_209_image__iff, fact_20_insertE, % 139.97/19.30 fact_210_image__iff, fact_211_image__iff, fact_212_image__iff, % 139.97/19.30 fact_213_image__iff, fact_214_com_Osimps_I24_J, fact_215_com_Osimps_I25_J, % 139.97/19.30 fact_216_com_Osimps_I8_J, fact_217_com_Osimps_I9_J, fact_218_image__is__empty, % 139.97/19.30 fact_219_image__is__empty, fact_21_insertCI, fact_220_image__is__empty, % 139.97/19.30 fact_221_image__is__empty, fact_222_image__empty, fact_223_image__empty, % 139.97/19.30 fact_224_image__empty, fact_225_image__empty, fact_226_empty__is__image, % 139.97/19.30 fact_227_empty__is__image, fact_228_empty__is__image, fact_229_empty__is__image, % 139.97/19.30 fact_22_insertCI, fact_230_mem__def, fact_231_mem__def, fact_232_Collect__def, % 139.97/19.30 fact_233_Collect__def, fact_234_insert__image, fact_235_insert__image, % 139.97/19.30 fact_236_image__insert, fact_237_image__insert, fact_238_image__insert, % 139.97/19.30 fact_239_image__insert, fact_23_insertCI, fact_240_the__sym__eq__trivial, % 139.97/19.30 fact_241_the__eq__trivial, fact_242_If__def, fact_243_fold1Set__sing, % 139.97/19.30 fact_244_fold1Set__sing, fact_245_fold1Set__sing, fact_246_the__equality, % 139.97/19.30 fact_247_folding__one_Osingleton, fact_248_folding__one_Osingleton, % 139.97/19.30 fact_249_folding__one_Osingleton, fact_24_emptyE, fact_250_hoare__derivs_OLocal, % 139.97/19.30 fact_251_hoare__derivs_OLocal, fact_252_vname_Osimps_I2_J, % 139.97/19.30 fact_253_com_Osimps_I2_J, fact_254_com_Osimps_I34_J, fact_255_com_Osimps_I35_J, % 139.97/19.30 fact_256_com_Osimps_I23_J, fact_257_com_Osimps_I22_J, fact_258_com_Osimps_I11_J, % 139.97/19.30 fact_259_com_Osimps_I10_J, fact_25_emptyE, fact_260_empty__fold1SetE, % 139.97/19.30 fact_261_empty__fold1SetE, fact_262_empty__fold1SetE, % 139.97/19.30 fact_263_fold1Set__nonempty, fact_264_fold1Set__nonempty, % 139.97/19.30 fact_265_fold1Set__nonempty, fact_266_theI, fact_267_the1__equality, % 139.97/19.30 fact_268_theI_H, fact_269_evalc_OLocal, fact_26_emptyE, fact_270_evaln_OLocal, % 139.97/19.30 fact_271_fold1Set_Ointros, fact_272_fold1Set_Ointros, fact_273_fold1Set_Ointros, % 139.97/19.30 fact_274_evaln_OSemi, fact_275_evaln_OSkip, fact_276_evaln__elim__cases_I1_J, % 139.97/19.30 fact_277_evalc_OSemi, fact_278_evalc_OSkip, fact_279_evalc__elim__cases_I1_J, % 139.97/19.30 fact_27_singleton__conv2, fact_280_evaln_OAssign, % 139.97/19.30 fact_281_evaln__elim__cases_I2_J, fact_282_evalc_OAssign, % 139.97/19.30 fact_283_evalc__elim__cases_I2_J, fact_284_eval__eq, fact_285_com__det, % 139.97/19.30 fact_286_evaln__evalc, fact_287_empty__fold__graphE, % 139.97/19.30 fact_288_fold__graph_OemptyI, fact_289_fold__graph_OinsertI, % 139.97/19.30 fact_28_singleton__conv2, fact_290_evalc__elim__cases_I3_J, % 139.97/19.30 fact_291_evaln__elim__cases_I3_J, fact_292_evalc__elim__cases_I4_J, % 139.97/19.30 fact_293_evaln__elim__cases_I4_J, fact_294_insert__fold1SetE, % 139.97/19.30 fact_295_insert__fold1SetE, fact_296_insert__fold1SetE, fact_297_MGT__def, % 139.97/19.30 fact_298_evalc__evaln, fact_299_fold1Set_Osimps, fact_29_singleton__conv2, % 139.97/19.30 fact_2_triple_Oinject, fact_300_fold1Set_Osimps, fact_301_fold1Set_Osimps, % 139.97/19.30 fact_302_fold__graph_Osimps, fact_303_evaln__max2, fact_304_triple__valid__def2, % 139.97/19.30 fact_305_triple__valid__def2, fact_306_folding__one_Oinsert, % 139.97/19.30 fact_307_folding__one_Oinsert, fact_308_folding__one_Oinsert, % 139.97/19.30 fact_309_finite__Collect__conjI, fact_30_singleton__conv2, % 139.97/19.30 fact_310_finite__Collect__conjI, fact_311_finite_OemptyI, % 139.97/19.30 fact_312_finite_OemptyI, fact_313_finite_OemptyI, fact_314_finite_OinsertI, % 139.97/19.30 fact_315_finite_OinsertI, fact_316_finite_OinsertI, % 139.97/19.30 fact_317_finite__Collect__disjI, fact_318_finite__Collect__disjI, % 139.97/19.30 fact_319_vname_Osimps_I1_J, fact_31_singleton__conv, fact_320_finite__insert, % 139.97/19.30 fact_321_finite__insert, fact_322_finite__insert, fact_323_vname_Osimps_I4_J, % 139.97/19.30 fact_324_vname_Osimps_I3_J, fact_325_folding__one_Oclosed, % 139.97/19.30 fact_326_folding__one_Oclosed, fact_327_folding__one_Oclosed, % 139.97/19.30 fact_328_finite__nonempty__imp__fold1Set, % 139.97/19.30 fact_329_finite__nonempty__imp__fold1Set, fact_32_singleton__conv, % 139.97/19.30 fact_330_finite__nonempty__imp__fold1Set, fact_331_finite__induct, % 139.97/19.30 fact_332_finite__induct, fact_333_finite__induct, fact_334_finite_Osimps, % 139.97/19.30 fact_335_finite_Osimps, fact_336_finite_Osimps, % 139.97/19.30 fact_337_finite__imp__fold__graph, fact_338_folding__one__idem_Oinsert__idem, % 139.97/19.30 fact_339_folding__one__idem_Oinsert__idem, fact_33_singleton__conv, % 139.97/19.30 fact_340_folding__one__idem_Oinsert__idem, fact_341_finite__ne__induct, % 139.97/19.30 fact_342_finite__ne__induct, fact_343_finite__ne__induct, % 139.97/19.30 fact_344_vname_Oexhaust, fact_345_folding__one_Oremove, % 139.97/19.30 fact_346_folding__one_Oremove, fact_347_folding__one_Oremove, % 139.97/19.30 fact_348_folding__one_Oinsert__remove, fact_349_folding__one_Oinsert__remove, % 139.97/19.30 fact_34_singleton__conv, fact_350_folding__one_Oinsert__remove, fact_351_DiffE, % 139.97/19.30 fact_352_DiffE, fact_353_DiffI, fact_354_DiffI, fact_355_finite__Diff, % 139.97/19.30 fact_356_DiffD2, fact_357_DiffD2, fact_358_DiffD1, fact_359_DiffD1, % 139.97/19.30 fact_35_Collect__conv__if2, fact_360_Diff__iff, fact_361_Diff__iff, % 139.97/19.30 fact_362_set__diff__eq, fact_363_set__diff__eq, fact_364_Diff__cancel, % 139.97/19.30 fact_365_Diff__cancel, fact_366_Diff__cancel, fact_367_Diff__empty, % 139.97/19.30 fact_368_Diff__empty, fact_369_Diff__empty, fact_36_Collect__conv__if2, % 139.97/19.30 fact_370_empty__Diff, fact_371_empty__Diff, fact_372_empty__Diff, % 139.97/19.30 fact_373_finite__Diff2, fact_374_insert__Diff1, fact_375_insert__Diff1, % 139.97/19.30 fact_376_insert__Diff1, fact_377_insert__Diff__if, fact_378_insert__Diff__if, % 139.97/19.30 fact_379_insert__Diff__if, fact_37_Collect__conv__if2, fact_380_insert__Diff, % 139.97/19.30 fact_381_insert__Diff, fact_382_insert__Diff, fact_383_Diff__insert__absorb, % 139.97/19.30 fact_384_Diff__insert__absorb, fact_385_Diff__insert__absorb, % 139.97/19.30 fact_386_insert__Diff__single, fact_387_insert__Diff__single, % 139.97/19.30 fact_388_insert__Diff__single, fact_389_Diff__insert2, % 139.97/19.30 fact_38_Collect__conv__if2, fact_390_Diff__insert2, fact_391_Diff__insert2, % 139.97/19.30 fact_392_Diff__insert, fact_393_Diff__insert, fact_394_Diff__insert, % 139.97/19.30 fact_395_finite__Diff__insert, fact_396_finite__Diff__insert, % 139.97/19.30 fact_397_finite__Diff__insert, fact_398_folding__one__idem_Oin__idem, % 139.97/19.30 fact_399_folding__one__idem_Oin__idem, fact_39_Collect__conv__if, % 139.97/19.30 fact_3_triple_Oinject, fact_400_folding__one__idem_Ohom__commute, % 139.97/19.30 fact_401_folding__one__idem_Ohom__commute, % 139.97/19.30 fact_402_folding__one__idem_Ohom__commute, fact_403_finite__empty__induct, % 139.97/19.30 fact_404_finite__empty__induct, fact_405_finite__empty__induct, % 139.97/19.30 fact_406_comp__fun__idem__remove, fact_407_comp__fun__idem__remove, % 139.97/19.30 fact_408_comp__fun__idem__remove, % 139.97/19.30 fact_409_comp__fun__commute_Ofold__graph__insertE__aux, % 139.97/19.30 fact_40_Collect__conv__if, fact_410_fold__graph__permute__diff, % 139.97/19.30 fact_411_comp__fun__idem__insert, fact_412_comp__fun__idem__insert, % 139.97/19.30 fact_413_comp__fun__idem__insert, % 139.97/19.30 fact_414_comp__fun__commute_Ofold__graph__determ, % 139.97/19.30 fact_415_fold__graph__insert__swap, % 139.97/19.30 fact_416_comp__fun__commute_Ofold__graph__insertE, fact_417_fold1__insert, % 139.97/19.30 fact_418_fold1__eq__fold, fact_419_fold1__singleton, fact_41_Collect__conv__if, % 139.97/19.30 fact_420_fold1__singleton, fact_421_fold1__singleton, % 139.97/19.30 fact_422_fold1__singleton__def, fact_423_fold1__singleton__def, % 139.97/19.30 fact_424_fold1__singleton__def, fact_425_comp__fun__commute_Ofold__equality, % 139.97/19.30 fact_426_fold__def, fact_427_folding__one_Oeq__fold, % 139.97/19.30 fact_428_folding__one_Oeq__fold, fact_429_folding__one_Oeq__fold_H, % 139.97/19.30 fact_42_Collect__conv__if, fact_430_folding__one_Oeq__fold_H, % 139.97/19.30 fact_431_folding__one_Oeq__fold_H, % 139.97/19.30 fact_432_folding__one__idem_Oeq__fold__idem_H, % 139.97/19.30 fact_433_folding__one__idem_Oeq__fold__idem_H, % 139.97/19.30 fact_434_folding__one__idem_Oeq__fold__idem_H, % 139.97/19.30 fact_435_comp__fun__commute_Ofold__graph__fold, fact_436_fold1__def, % 139.97/19.30 fact_437_minus__fold__remove, fact_438_minus__fold__remove, % 139.97/19.30 fact_439_minus__fold__remove, fact_43_equals0D, fact_440_fold1__in, % 139.97/19.30 fact_441_semilattice__big_OF__eq, fact_442_folding__one__idem_Osubset__idem, % 139.97/19.30 fact_443_folding__one__idem_Osubset__idem, % 139.97/19.30 fact_444_folding__one__idem_Osubset__idem, fact_445_order__refl, % 139.97/19.30 fact_446_subsetD, fact_447_subsetD, fact_448_UnCI, fact_449_UnCI, % 139.97/19.30 fact_44_equals0D, fact_450_UnE, fact_451_UnE, fact_452_empty__subsetI, % 139.97/19.30 fact_453_empty__subsetI, fact_454_empty__subsetI, % 139.97/19.30 fact_455_finite__Collect__subsets, fact_456_sup__le__fold__sup, % 139.97/19.30 fact_457_subset__empty, fact_458_subset__empty, fact_459_subset__empty, % 139.97/19.31 fact_45_equals0D, fact_460_rev__finite__subset, fact_461_finite__subset, % 139.97/19.31 fact_462_subset__insertI, fact_463_subset__insertI, fact_464_subset__insertI, % 139.97/19.31 fact_465_insert__subset, fact_466_insert__subset, fact_467_insert__subset, % 139.97/19.31 fact_468_subset__insert, fact_469_subset__insert, fact_46_Collect__empty__eq, % 139.97/19.31 fact_470_subset__insert, fact_471_subset__insertI2, fact_472_subset__insertI2, % 139.97/19.31 fact_473_subset__insertI2, fact_474_insert__mono, fact_475_insert__mono, % 139.97/19.31 fact_476_insert__mono, fact_477_le__supE, fact_478_sup__mono, % 139.97/19.31 fact_479_sup__least, fact_47_Collect__empty__eq, fact_480_le__supI, % 139.97/19.31 fact_481_sup__absorb1, fact_482_sup__absorb2, fact_483_le__supI2, % 139.97/19.31 fact_484_le__supI1, fact_485_le__sup__iff, fact_486_le__iff__sup, % 139.97/19.31 fact_487_sup__ge2, fact_488_inf__sup__ord_I4_J, fact_489_sup__ge1, % 139.97/19.31 fact_48_Collect__empty__eq, fact_490_inf__sup__ord_I3_J, % 139.97/19.31 fact_491_sup__eq__bot__iff, fact_492_sup__eq__bot__iff, % 139.97/19.31 fact_493_sup__eq__bot__iff, fact_494_sup__eq__bot__iff, % 139.97/19.31 fact_495_sup__bot__right, fact_496_sup__bot__right, fact_497_sup__bot__right, % 139.97/19.31 fact_498_sup__bot__right, fact_499_sup__bot__left, fact_49_Collect__empty__eq, % 139.97/19.31 fact_4_cut, fact_500_sup__bot__left, fact_501_sup__bot__left, % 139.97/19.31 fact_502_sup__bot__left, fact_503_Un__empty__left, fact_504_Un__empty__left, % 139.97/19.31 fact_505_Un__empty__left, fact_506_Un__empty__right, fact_507_Un__empty__right, % 139.97/19.31 fact_508_Un__empty__right, fact_509_Un__empty, fact_50_empty__iff, % 139.97/19.31 fact_510_Un__empty, fact_511_Un__empty, fact_512_finite__Un, % 139.97/19.31 fact_513_finite__UnI, fact_514_linorder__le__cases, fact_515_xt1_I6_J, % 139.97/19.31 fact_516_xt1_I5_J, fact_517_order__trans, fact_518_order__antisym, % 139.97/19.31 fact_519_xt1_I4_J, fact_51_empty__iff, fact_520_ord__le__eq__trans, % 139.97/19.31 fact_521_xt1_I3_J, fact_522_ord__eq__le__trans, fact_523_order__antisym__conv, % 139.97/19.31 fact_524_order__eq__refl, fact_525_order__eq__iff, fact_526_linorder__linear, % 139.97/19.31 fact_527_Collect__disj__eq, fact_528_Collect__disj__eq, fact_529_set__mp, % 139.97/19.31 fact_52_empty__iff, fact_530_set__mp, fact_531_set__rev__mp, % 139.97/19.31 fact_532_set__rev__mp, fact_533_in__mono, fact_534_in__mono, fact_535_UnI2, % 139.97/19.31 fact_536_UnI2, fact_537_UnI1, fact_538_UnI1, fact_539_Un__iff, % 139.97/19.31 fact_53_empty__Collect__eq, fact_540_Un__iff, fact_541_Un__def, % 139.97/19.31 fact_542_Un__def, fact_543_pred__subset__eq, fact_544_pred__subset__eq, % 139.97/19.31 fact_545_sup__Un__eq, fact_546_sup__Un__eq, fact_547_bot__least, % 139.97/19.31 fact_548_bot__least, fact_549_bot__least, fact_54_empty__Collect__eq, % 139.97/19.31 fact_550_bot__least, fact_551_bot__least, fact_552_bot__unique, % 139.97/19.31 fact_553_bot__unique, fact_554_bot__unique, fact_555_bot__unique, % 139.97/19.31 fact_556_bot__unique, fact_557_le__bot, fact_558_le__bot, fact_559_le__bot, % 139.97/19.31 fact_55_empty__Collect__eq, fact_560_le__bot, fact_561_le__bot, % 139.97/19.31 fact_562_Un__insert__right, fact_563_Un__insert__right, % 139.97/19.31 fact_564_Un__insert__right, fact_565_Un__insert__left, % 139.97/19.31 fact_566_Un__insert__left, fact_567_Un__insert__left, fact_568_weaken, % 139.97/19.31 fact_569_weaken, fact_56_empty__Collect__eq, fact_570_asm, fact_571_asm, % 139.97/19.31 fact_572_insert__def, fact_573_insert__def, fact_574_insert__def, % 139.97/19.31 fact_575_insert__is__Un, fact_576_insert__is__Un, fact_577_insert__is__Un, % 139.97/19.31 fact_578_fold__sup__insert, fact_579_union__fold__insert, fact_57_ex__in__conv, % 139.97/19.31 fact_580_union__fold__insert, fact_581_union__fold__insert, % 139.97/19.31 fact_582_subset__singletonD, fact_583_subset__singletonD, % 139.97/19.31 fact_584_subset__singletonD, fact_585_diff__single__insert, % 139.97/19.31 fact_586_diff__single__insert, fact_587_diff__single__insert, % 139.97/19.31 fact_588_subset__insert__iff, fact_589_subset__insert__iff, % 139.97/19.31 fact_58_ex__in__conv, fact_590_subset__insert__iff, % 139.97/19.31 fact_591_folding__one__idem_Ounion__idem, % 139.97/19.31 fact_592_folding__one__idem_Ounion__idem, % 139.97/19.31 fact_593_folding__one__idem_Ounion__idem, fact_594_fold__sup__le__sup, % 139.97/19.31 fact_595_finite__subset__induct, fact_596_finite__subset__induct, % 139.97/19.31 fact_597_finite__subset__induct, fact_598_subsetI, fact_599_subsetI, % 139.97/19.31 fact_59_ex__in__conv, fact_5_cut, fact_600_evaln__nonstrict, % 139.97/19.31 fact_601_finite__Collect__le__nat, fact_602_flat__lub__def, % 139.97/19.31 fact_603_flat__lub__def, fact_604_flat__lub__def, % 139.97/19.31 fact_605_finite__nat__set__iff__bounded__le, fact_606_finite__less__ub, % 139.97/19.31 fact_607_Sup__fin_Oremove, fact_608_Sup__fin_Osingleton, % 139.97/19.31 fact_609_Sup__fin_Oin__idem, fact_60_all__not__in__conv, % 139.97/19.31 fact_610_Sup__fin_OF__eq, fact_611_Sup__fin_Oinsert__idem, % 139.97/19.31 fact_612_Sup__fin_Oinsert, fact_613_Sup__fin_Osubset__idem, % 139.97/19.31 fact_614_Sup__fin_Ounion__idem, fact_615_Sup__fin_Oeq__fold__idem_H, % 139.97/19.31 fact_616_Sup__fin_Oeq__fold_H, fact_617_Sup__fin_Oinsert__remove, % 139.97/19.31 fact_618_Sup__fin_Ohom__commute, fact_619_Sup__fin_Oclosed, % 139.97/19.31 fact_61_all__not__in__conv, fact_620_Sup__fin_Ounion__disjoint, fact_621_IntI, % 139.97/19.31 fact_622_IntI, fact_623_IntE, fact_624_IntE, fact_625_finite__Int, % 139.97/19.31 fact_626_le__infE, fact_627_inf__mono, fact_628_inf__greatest, % 139.97/19.31 fact_629_le__infI, fact_62_all__not__in__conv, fact_630_inf__absorb2, % 139.97/19.31 fact_631_inf__absorb1, fact_632_le__infI2, fact_633_le__infI1, % 139.97/19.31 fact_634_le__inf__iff, fact_635_le__iff__inf, fact_636_inf__le2, % 139.97/19.31 fact_637_inf__sup__ord_I2_J, fact_638_inf__le1, fact_639_inf__sup__ord_I1_J, % 139.97/19.31 fact_63_empty__def, fact_640_distrib__sup__le, fact_641_distrib__inf__le, % 139.97/19.31 fact_642_Int__insert__left__if1, fact_643_Int__insert__left__if1, % 139.97/19.31 fact_644_Int__insert__left__if1, fact_645_Int__insert__right__if1, % 139.97/19.31 fact_646_Int__insert__right__if1, fact_647_Int__insert__right__if1, % 139.97/19.31 fact_648_Int__insert__left__if0, fact_649_Int__insert__left__if0, % 139.97/19.31 fact_64_empty__def, fact_650_Int__insert__left__if0, % 139.97/19.31 fact_651_Int__insert__right__if0, fact_652_Int__insert__right__if0, % 139.97/19.31 fact_653_Int__insert__right__if0, fact_654_insert__inter__insert, % 139.97/19.31 fact_655_insert__inter__insert, fact_656_insert__inter__insert, % 139.97/19.31 fact_657_Int__insert__left, fact_658_Int__insert__left, % 139.97/19.31 fact_659_Int__insert__left, fact_65_empty__def, fact_660_Int__insert__right, % 139.97/19.31 fact_661_Int__insert__right, fact_662_Int__insert__right, fact_663_inf__Int__eq, % 139.97/19.31 fact_664_inf__Int__eq, fact_665_Collect__conj__eq, fact_666_Collect__conj__eq, % 139.97/19.31 fact_667_Int__Collect, fact_668_Int__Collect, fact_669_Int__def, % 139.97/19.31 fact_66_empty__def, fact_670_Int__def, fact_671_Int__iff, fact_672_Int__iff, % 139.97/19.31 fact_673_IntD1, fact_674_IntD1, fact_675_IntD2, fact_676_IntD2, % 139.97/19.31 fact_677_disjoint__iff__not__equal, fact_678_disjoint__iff__not__equal, % 139.97/19.31 fact_679_disjoint__iff__not__equal, fact_67_insert__absorb, % 139.97/19.31 fact_680_Int__empty__right, fact_681_Int__empty__right, % 139.97/19.31 fact_682_Int__empty__right, fact_683_Int__empty__left, % 139.97/19.31 fact_684_Int__empty__left, fact_685_Int__empty__left, fact_686_inf__bot__left, % 139.97/19.31 fact_687_inf__bot__left, fact_688_inf__bot__left, fact_689_inf__bot__left, % 139.97/19.31 fact_68_insert__absorb, fact_690_inf__bot__right, fact_691_inf__bot__right, % 139.97/19.31 fact_692_inf__bot__right, fact_693_inf__bot__right, fact_694_Diff__triv, % 139.97/19.31 fact_695_Diff__triv, fact_696_Diff__triv, fact_697_Diff__disjoint, % 139.97/19.31 fact_698_Diff__disjoint, fact_699_Diff__disjoint, fact_69_insert__absorb, % 139.97/19.31 fact_6_hoare__derivs_Oinsert, fact_70_insertI2, fact_71_insertI2, % 139.97/19.31 fact_72_insertI2, fact_73_insert__ident, fact_74_insert__ident, % 139.97/19.31 fact_75_insert__ident, fact_76_insert__code, fact_77_insert__code, % 139.97/19.31 fact_78_insert__code, fact_79_insert__iff, fact_7_hoare__derivs_Oinsert, % 139.97/19.31 fact_80_insert__iff, fact_81_insert__iff, fact_82_insert__commute, % 139.97/19.31 fact_83_insert__commute, fact_84_insert__commute, fact_85_insert__absorb2, % 139.97/19.31 fact_86_insert__absorb2, fact_87_insert__absorb2, fact_88_insert__Collect, % 139.97/19.31 fact_89_insert__Collect, fact_8_constant, fact_90_insert__Collect, % 139.97/19.31 fact_91_insert__Collect, fact_92_insert__compr, fact_93_insert__compr, % 139.97/19.31 fact_94_insert__compr, fact_95_insert__compr, fact_96_insertI1, % 139.97/19.31 fact_97_insertI1, fact_98_insertI1, fact_99_insert__compr__raw, fact_9_constant, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__Com__Ostate_000tc__HOL__Obool_000tc__Com__Ostate_U, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Ostate_U, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Hoare____Mirabel, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Hoare____Mirabel_215, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Nat__On, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_210, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_217, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_220, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_223, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It_218, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It_222, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It_227, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It_228, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It_231, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H_230, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H_234, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I_232, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I_238, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I_239, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo, % 139.97/19.31 help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 139.97/19.31 help_COMBC_1_1_COMBC_000t__a_000tc__HOL__Obool_000tc__fun_Itc__Com__Ostate_Mtc__, % 139.97/19.31 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Com__Ostate_Mtc__Com__Ostate_J_000t, % 139.97/19.31 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__Com__Ostate_000tc__HOL__Obool_U, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__Com__Ovname_000tc__fun_Itc__Nat__, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__HOL__Obool_000tc__fun_Itc__Com__O, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__Nat__Onat_000tc__Com__Ostate_U, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__fun_Itc__Com__Ostate_Mtc__Com__Os, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00_229, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00_235, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com__, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com___233, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com___236, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Nat__Onat_000tc__HOL__Obool_U, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__216, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I_237, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__224, % 139.97/19.31 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__225, % 139.97/19.31 help_COMBI_1_1_COMBI_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_U, % 139.97/19.31 help_COMBI_1_1_COMBI_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com__, % 139.97/19.31 help_COMBI_1_1_COMBI_000tc__Nat__Onat_U, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____xlrqixeqwe__, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____xlrqixeqwe___212, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_U, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00_219, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00_221, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com__, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com___226, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Nat__Onat_000tc__Hoare____Mirabelle____xlrqixeqwe__O, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Nat__Onat_000tc__Hoare____Mirabelle____xlrqixeqwe__O_211, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__Nat__Onat_000tc__Nat__Onat_U, % 139.97/19.31 help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__Com__O, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__Com__Ostate_000tc__Nat__Onat_000tc__Com__Ostate_U, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com__, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U, % 139.97/19.31 help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo, % 139.97/19.31 help_fFalse_1_1_T, help_fNot_1_1_U, help_fNot_2_1_U, help_fconj_1_1_U, % 139.97/19.31 help_fconj_2_1_U, help_fconj_3_1_U, help_fdisj_1_1_U, help_fdisj_2_1_U, % 139.97/19.31 help_fdisj_3_1_U, help_fequal_1_1_fequal_000tc__Com__Ostate_T, % 139.97/19.31 help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_, % 139.97/19.31 help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com, % 139.97/19.31 help_fequal_1_1_fequal_000tc__Nat__Onat_T, % 139.97/19.31 help_fequal_1_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple, % 139.97/19.31 help_fequal_1_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_213, % 139.97/19.31 help_fequal_1_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 139.97/19.31 help_fequal_2_1_fequal_000tc__Com__Ostate_T, % 139.97/19.31 help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_, % 139.97/19.31 help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_Itc__Com, % 139.97/19.31 help_fequal_2_1_fequal_000tc__Nat__Onat_T, % 139.97/19.31 help_fequal_2_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple, % 139.97/19.31 help_fequal_2_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_214, % 139.97/19.31 help_fequal_2_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 139.97/19.31 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 139.97/19.31 % 139.97/19.31 Those formulas are unsatisfiable: % 139.97/19.31 --------------------------------- % 139.97/19.31 % 139.97/19.31 Begin of proof % 139.97/19.31 | % 139.97/19.31 | ALPHA: (fact_10_escape) implies: % 139.97/19.32 | (1) ? [v0: fun_st1506752259e_bool] : % 139.97/19.32 | (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = v0 & % 139.97/19.32 | fun_st1506752259e_bool(v0) & ! [v1: fun_Ho287446294a_bool] : ! [v2: % 139.97/19.32 | com] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 139.97/19.32 | fun_a_fun_state_bool] : ! [v5: fun_fu1441721944l_bool] : ! [v6: % 139.97/19.32 | hoare_1544627872iple_a] : ! [v7: fun_fu410471825a_bool] : ! [v8: % 139.97/19.32 | fun_Ho287446294a_bool] : ! [v9: bool] : ( ~ % 139.97/19.32 | (hAPP_H762155206a_bool(insert1051021594iple_a, v6) = v7) | ~ % 139.97/19.32 | (hAPP_f909437487a_bool(v7, bot_bo1766443648a_bool) = v8) | ~ % 139.97/19.32 | (hoare_196563068iple_a(v4, v2, v3) = v6) | ~ % 139.97/19.32 | (hoare_1546678894rivs_a(v1) = v5) | ~ (hAPP_f2063540982l_bool(v5, % 139.97/19.32 | v8) = v9) | ~ fun_Ho287446294a_bool(v1) | ~ % 139.97/19.32 | fun_a_fun_state_bool(v4) | ~ fun_a_fun_state_bool(v3) | ~ com(v2) % 139.97/19.32 | | hBOOL(v9) | ? [v10: x_a] : ? [v11: state] : ? [v12: % 139.97/19.32 | fun_state_bool] : ? [v13: bool] : ? [v14: fun_state_bool] : ? % 139.97/19.32 | [v15: fun_a_fun_state_bool] : ? [v16: fun_state_bool] : ? [v17: % 139.97/19.32 | fun_a_fun_state_bool] : ? [v18: hoare_1544627872iple_a] : ? % 139.97/19.32 | [v19: fun_fu410471825a_bool] : ? [v20: fun_Ho287446294a_bool] : ? % 139.97/19.32 | [v21: bool] : (hAPP_state_bool(v12, v11) = v13 & % 139.97/19.32 | hAPP_s1806633685e_bool(v0, v11) = v14 & % 139.97/19.32 | hAPP_a2036067514e_bool(v4, v10) = v12 & % 139.97/19.32 | hAPP_a2036067514e_bool(v3, v10) = v16 & % 139.97/19.32 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v16) = v17 & % 139.97/19.32 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v14) = v15 & % 139.97/19.32 | hAPP_H762155206a_bool(insert1051021594iple_a, v18) = v19 & % 139.97/19.32 | hAPP_f909437487a_bool(v19, bot_bo1766443648a_bool) = v20 & % 139.97/19.32 | hoare_196563068iple_a(v15, v2, v17) = v18 & % 139.97/19.32 | hAPP_f2063540982l_bool(v5, v20) = v21 & % 139.97/19.32 | fun_fu410471825a_bool(v19) & fun_Ho287446294a_bool(v20) & % 139.97/19.32 | fun_state_bool(v16) & fun_state_bool(v14) & fun_state_bool(v12) & % 139.97/19.32 | fun_a_fun_state_bool(v17) & fun_a_fun_state_bool(v15) & % 139.97/19.32 | hoare_1544627872iple_a(v18) & bool(v21) & bool(v13) & state(v11) % 139.97/19.32 | & x_a(v10) & hBOOL(v13) & ~ hBOOL(v21)))) % 139.97/19.32 | % 139.97/19.32 | ALPHA: (help_fFalse_1_1_U) implies: % 139.97/19.32 | (2) ~ hBOOL(fFalse) % 139.97/19.32 | % 139.97/19.32 | ALPHA: (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) implies: % 139.97/19.32 | (3) ! [v0: bool] : ! [v1: state] : ! [v2: fun_state_bool] : ! [v3: % 139.97/19.32 | bool] : (v3 = v0 | ~ (hAPP_b2019457360e_bool(cOMBK_bool_state, v0) = % 139.97/19.32 | v2) | ~ (hAPP_state_bool(v2, v1) = v3) | ~ bool(v0) | ~ % 139.97/19.32 | state(v1)) % 139.97/19.32 | % 139.97/19.32 | ALPHA: (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 139.97/19.32 | implies: % 139.97/19.32 | (4) ! [v0: fun_state_bool] : ! [v1: x_a] : ! [v2: fun_a_fun_state_bool] % 139.97/19.32 | : ! [v3: fun_state_bool] : (v3 = v0 | ~ (hAPP_a2036067514e_bool(v2, % 139.97/19.32 | v1) = v3) | ~ (hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v0) % 139.97/19.32 | = v2) | ~ fun_state_bool(v0) | ~ x_a(v1)) % 139.97/19.32 | % 139.97/19.32 | ALPHA: (conj_0) implies: % 139.97/19.32 | (5) com(c) % 139.97/19.32 | (6) bool(fFalse) % 139.97/19.32 | (7) fun_Ho287446294a_bool(g) % 139.97/19.32 | (8) ? [v0: fun_fu1441721944l_bool] : ? [v1: fun_state_bool] : ? [v2: % 139.97/19.32 | fun_a_fun_state_bool] : ? [v3: fun_fu2008829792e_bool] : ? [v4: % 139.97/19.32 | fun_fu1658206819l_bool] : ? [v5: fun_fu2118559873l_bool] : ? [v6: % 139.97/19.32 | fun_a_1632297036l_bool] : ? [v7: fun_a_2117018159e_bool] : ? [v8: % 139.97/19.32 | fun_fu281355805e_bool] : ? [v9: fun_fu373216837e_bool] : ? [v10: % 139.97/19.32 | fun_state_bool] : ? [v11: fun_a_fun_state_bool] : ? [v12: % 139.97/19.32 | hoare_1544627872iple_a] : ? [v13: fun_fu410471825a_bool] : ? [v14: % 139.97/19.32 | fun_Ho287446294a_bool] : ? [v15: bool] : % 139.97/19.32 | (hAPP_f375255701e_bool(cOMBB_145932198bool_a, cOMBS_1378840469l_bool) = % 139.97/19.32 | v3 & hAPP_f963367678e_bool(v3, v6) = v7 & % 139.97/19.32 | hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 139.97/19.32 | hAPP_f2073279419e_bool(cOMBB_160679318_state, fNot) = v9 & % 139.97/19.32 | hAPP_f1759915619e_bool(v9, b) = v10 & % 139.97/19.32 | hAPP_b2019457360e_bool(cOMBK_bool_state, fFalse) = v1 & % 139.97/19.32 | hAPP_f762886889e_bool(v8, v10) = v11 & % 139.97/19.32 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v1) = v2 & % 139.97/19.32 | hAPP_f1561913689l_bool(cOMBB_188601460_state, fconj) = v4 & % 139.97/19.32 | hAPP_f1178339559l_bool(cOMBB_1355796797bool_a, v4) = v5 & % 139.97/19.32 | hAPP_f1509969235l_bool(v5, p) = v6 & % 139.97/19.32 | hAPP_H762155206a_bool(insert1051021594iple_a, v12) = v13 & % 139.97/19.32 | hAPP_f909437487a_bool(v13, bot_bo1766443648a_bool) = v14 & % 139.97/19.32 | hoare_196563068iple_a(v2, c, v11) = v12 & hoare_1546678894rivs_a(g) = % 139.97/19.32 | v0 & hAPP_f2063540982l_bool(v0, v14) = v15 & % 139.97/19.32 | fun_fu410471825a_bool(v13) & fun_fu1441721944l_bool(v0) & % 139.97/19.32 | fun_fu1658206819l_bool(v4) & fun_fu373216837e_bool(v9) & % 139.97/19.32 | fun_fu281355805e_bool(v8) & fun_fu2008829792e_bool(v3) & % 139.97/19.32 | fun_fu2118559873l_bool(v5) & fun_Ho287446294a_bool(v14) & % 139.97/19.32 | fun_state_bool(v10) & fun_state_bool(v1) & fun_a_2117018159e_bool(v7) % 139.97/19.32 | & fun_a_1632297036l_bool(v6) & fun_a_fun_state_bool(v11) & % 139.97/19.32 | fun_a_fun_state_bool(v2) & hoare_1544627872iple_a(v12) & bool(v15) & % 139.97/19.32 | ~ hBOOL(v15)) % 139.97/19.32 | % 139.97/19.32 | DELTA: instantiating (8) with fresh symbols all_1337_0, all_1337_1, % 139.97/19.32 | all_1337_2, all_1337_3, all_1337_4, all_1337_5, all_1337_6, all_1337_7, % 139.97/19.32 | all_1337_8, all_1337_9, all_1337_10, all_1337_11, all_1337_12, % 139.97/19.32 | all_1337_13, all_1337_14, all_1337_15 gives: % 139.97/19.32 | (9) hAPP_f375255701e_bool(cOMBB_145932198bool_a, cOMBS_1378840469l_bool) = % 139.97/19.32 | all_1337_12 & hAPP_f963367678e_bool(all_1337_12, all_1337_9) = % 139.97/19.32 | all_1337_8 & hAPP_f1261923407e_bool(cOMBC_892787026e_bool, all_1337_8) % 139.97/19.32 | = all_1337_7 & hAPP_f2073279419e_bool(cOMBB_160679318_state, fNot) = % 139.97/19.32 | all_1337_6 & hAPP_f1759915619e_bool(all_1337_6, b) = all_1337_5 & % 139.97/19.32 | hAPP_b2019457360e_bool(cOMBK_bool_state, fFalse) = all_1337_14 & % 139.97/19.32 | hAPP_f762886889e_bool(all_1337_7, all_1337_5) = all_1337_4 & % 139.97/19.32 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, all_1337_14) = % 139.97/19.32 | all_1337_13 & hAPP_f1561913689l_bool(cOMBB_188601460_state, fconj) = % 139.97/19.32 | all_1337_11 & hAPP_f1178339559l_bool(cOMBB_1355796797bool_a, % 139.97/19.32 | all_1337_11) = all_1337_10 & hAPP_f1509969235l_bool(all_1337_10, p) = % 139.97/19.33 | all_1337_9 & hAPP_H762155206a_bool(insert1051021594iple_a, all_1337_3) % 139.97/19.33 | = all_1337_2 & hAPP_f909437487a_bool(all_1337_2, % 139.97/19.33 | bot_bo1766443648a_bool) = all_1337_1 & % 139.97/19.33 | hoare_196563068iple_a(all_1337_13, c, all_1337_4) = all_1337_3 & % 139.97/19.33 | hoare_1546678894rivs_a(g) = all_1337_15 & % 139.97/19.33 | hAPP_f2063540982l_bool(all_1337_15, all_1337_1) = all_1337_0 & % 139.97/19.33 | fun_fu410471825a_bool(all_1337_2) & fun_fu1441721944l_bool(all_1337_15) % 139.97/19.33 | & fun_fu1658206819l_bool(all_1337_11) & % 139.97/19.33 | fun_fu373216837e_bool(all_1337_6) & fun_fu281355805e_bool(all_1337_7) & % 139.97/19.33 | fun_fu2008829792e_bool(all_1337_12) & % 139.97/19.33 | fun_fu2118559873l_bool(all_1337_10) & fun_Ho287446294a_bool(all_1337_1) % 139.97/19.33 | & fun_state_bool(all_1337_5) & fun_state_bool(all_1337_14) & % 139.97/19.33 | fun_a_2117018159e_bool(all_1337_8) & fun_a_1632297036l_bool(all_1337_9) % 139.97/19.33 | & fun_a_fun_state_bool(all_1337_4) & fun_a_fun_state_bool(all_1337_13) % 139.97/19.33 | & hoare_1544627872iple_a(all_1337_3) & bool(all_1337_0) & ~ % 139.97/19.33 | hBOOL(all_1337_0) % 139.97/19.33 | % 139.97/19.33 | ALPHA: (9) implies: % 139.97/19.33 | (10) ~ hBOOL(all_1337_0) % 139.97/19.33 | (11) fun_a_fun_state_bool(all_1337_13) % 139.97/19.33 | (12) fun_a_fun_state_bool(all_1337_4) % 139.97/19.33 | (13) fun_state_bool(all_1337_14) % 139.97/19.33 | (14) hAPP_f2063540982l_bool(all_1337_15, all_1337_1) = all_1337_0 % 139.97/19.33 | (15) hoare_1546678894rivs_a(g) = all_1337_15 % 139.97/19.33 | (16) hoare_196563068iple_a(all_1337_13, c, all_1337_4) = all_1337_3 % 139.97/19.33 | (17) hAPP_f909437487a_bool(all_1337_2, bot_bo1766443648a_bool) = all_1337_1 % 139.97/19.33 | (18) hAPP_H762155206a_bool(insert1051021594iple_a, all_1337_3) = all_1337_2 % 139.97/19.33 | (19) hAPP_f762886889e_bool(cOMBK_1458035955bool_a, all_1337_14) = % 139.97/19.33 | all_1337_13 % 139.97/19.33 | (20) hAPP_b2019457360e_bool(cOMBK_bool_state, fFalse) = all_1337_14 % 139.97/19.33 | % 139.97/19.33 | DELTA: instantiating (1) with fresh symbol all_1339_0 gives: % 139.97/19.33 | (21) hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = % 139.97/19.33 | all_1339_0 & fun_st1506752259e_bool(all_1339_0) & ! [v0: % 139.97/19.33 | fun_Ho287446294a_bool] : ! [v1: com] : ! [v2: % 139.97/19.33 | fun_a_fun_state_bool] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 139.97/19.33 | fun_fu1441721944l_bool] : ! [v5: hoare_1544627872iple_a] : ! [v6: % 139.97/19.33 | fun_fu410471825a_bool] : ! [v7: fun_Ho287446294a_bool] : ! [v8: % 139.97/19.33 | bool] : ( ~ (hAPP_H762155206a_bool(insert1051021594iple_a, v5) = v6) % 139.97/19.33 | | ~ (hAPP_f909437487a_bool(v6, bot_bo1766443648a_bool) = v7) | ~ % 139.97/19.33 | (hoare_196563068iple_a(v3, v1, v2) = v5) | ~ % 139.97/19.33 | (hoare_1546678894rivs_a(v0) = v4) | ~ (hAPP_f2063540982l_bool(v4, % 139.97/19.33 | v7) = v8) | ~ fun_Ho287446294a_bool(v0) | ~ % 139.97/19.33 | fun_a_fun_state_bool(v3) | ~ fun_a_fun_state_bool(v2) | ~ com(v1) % 139.97/19.33 | | hBOOL(v8) | ? [v9: x_a] : ? [v10: state] : ? [v11: % 139.97/19.33 | fun_state_bool] : ? [v12: bool] : ? [v13: fun_state_bool] : ? % 139.97/19.33 | [v14: fun_a_fun_state_bool] : ? [v15: fun_state_bool] : ? [v16: % 139.97/19.33 | fun_a_fun_state_bool] : ? [v17: hoare_1544627872iple_a] : ? % 139.97/19.33 | [v18: fun_fu410471825a_bool] : ? [v19: fun_Ho287446294a_bool] : ? % 139.97/19.33 | [v20: bool] : (hAPP_state_bool(v11, v10) = v12 & % 139.97/19.33 | hAPP_s1806633685e_bool(all_1339_0, v10) = v13 & % 139.97/19.33 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 139.97/19.33 | v9) = v15 & hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v15) = % 139.97/19.33 | v16 & hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v13) = v14 & % 139.97/19.33 | hAPP_H762155206a_bool(insert1051021594iple_a, v17) = v18 & % 139.97/19.33 | hAPP_f909437487a_bool(v18, bot_bo1766443648a_bool) = v19 & % 139.97/19.33 | hoare_196563068iple_a(v14, v1, v16) = v17 & % 139.97/19.33 | hAPP_f2063540982l_bool(v4, v19) = v20 & fun_fu410471825a_bool(v18) % 139.97/19.33 | & fun_Ho287446294a_bool(v19) & fun_state_bool(v15) & % 139.97/19.33 | fun_state_bool(v13) & fun_state_bool(v11) & % 139.97/19.33 | fun_a_fun_state_bool(v16) & fun_a_fun_state_bool(v14) & % 139.97/19.33 | hoare_1544627872iple_a(v17) & bool(v20) & bool(v12) & state(v10) & % 139.97/19.33 | x_a(v9) & hBOOL(v12) & ~ hBOOL(v20))) % 139.97/19.33 | % 139.97/19.33 | ALPHA: (21) implies: % 139.97/19.33 | (22) ! [v0: fun_Ho287446294a_bool] : ! [v1: com] : ! [v2: % 139.97/19.33 | fun_a_fun_state_bool] : ! [v3: fun_a_fun_state_bool] : ! [v4: % 139.97/19.33 | fun_fu1441721944l_bool] : ! [v5: hoare_1544627872iple_a] : ! [v6: % 139.97/19.33 | fun_fu410471825a_bool] : ! [v7: fun_Ho287446294a_bool] : ! [v8: % 139.97/19.33 | bool] : ( ~ (hAPP_H762155206a_bool(insert1051021594iple_a, v5) = v6) % 139.97/19.33 | | ~ (hAPP_f909437487a_bool(v6, bot_bo1766443648a_bool) = v7) | ~ % 139.97/19.33 | (hoare_196563068iple_a(v3, v1, v2) = v5) | ~ % 139.97/19.33 | (hoare_1546678894rivs_a(v0) = v4) | ~ (hAPP_f2063540982l_bool(v4, % 139.97/19.33 | v7) = v8) | ~ fun_Ho287446294a_bool(v0) | ~ % 139.97/19.33 | fun_a_fun_state_bool(v3) | ~ fun_a_fun_state_bool(v2) | ~ com(v1) % 139.97/19.33 | | hBOOL(v8) | ? [v9: x_a] : ? [v10: state] : ? [v11: % 139.97/19.33 | fun_state_bool] : ? [v12: bool] : ? [v13: fun_state_bool] : ? % 139.97/19.33 | [v14: fun_a_fun_state_bool] : ? [v15: fun_state_bool] : ? [v16: % 139.97/19.33 | fun_a_fun_state_bool] : ? [v17: hoare_1544627872iple_a] : ? % 139.97/19.33 | [v18: fun_fu410471825a_bool] : ? [v19: fun_Ho287446294a_bool] : ? % 139.97/19.33 | [v20: bool] : (hAPP_state_bool(v11, v10) = v12 & % 139.97/19.33 | hAPP_s1806633685e_bool(all_1339_0, v10) = v13 & % 139.97/19.33 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 139.97/19.33 | v9) = v15 & hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v15) = % 139.97/19.33 | v16 & hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v13) = v14 & % 139.97/19.33 | hAPP_H762155206a_bool(insert1051021594iple_a, v17) = v18 & % 139.97/19.33 | hAPP_f909437487a_bool(v18, bot_bo1766443648a_bool) = v19 & % 139.97/19.33 | hoare_196563068iple_a(v14, v1, v16) = v17 & % 139.97/19.33 | hAPP_f2063540982l_bool(v4, v19) = v20 & fun_fu410471825a_bool(v18) % 139.97/19.33 | & fun_Ho287446294a_bool(v19) & fun_state_bool(v15) & % 139.97/19.33 | fun_state_bool(v13) & fun_state_bool(v11) & % 139.97/19.33 | fun_a_fun_state_bool(v16) & fun_a_fun_state_bool(v14) & % 139.97/19.33 | hoare_1544627872iple_a(v17) & bool(v20) & bool(v12) & state(v10) & % 139.97/19.33 | x_a(v9) & hBOOL(v12) & ~ hBOOL(v20))) % 139.97/19.33 | % 139.97/19.34 | GROUND_INST: instantiating (22) with g, c, all_1337_4, all_1337_13, % 139.97/19.34 | all_1337_15, all_1337_3, all_1337_2, all_1337_1, all_1337_0, % 139.97/19.34 | simplifying with (5), (7), (10), (11), (12), (14), (15), (16), % 139.97/19.34 | (17), (18) gives: % 139.97/19.34 | (23) ? [v0: x_a] : ? [v1: state] : ? [v2: fun_state_bool] : ? [v3: % 139.97/19.34 | bool] : ? [v4: fun_state_bool] : ? [v5: fun_a_fun_state_bool] : ? % 139.97/19.34 | [v6: fun_state_bool] : ? [v7: fun_a_fun_state_bool] : ? [v8: % 139.97/19.34 | hoare_1544627872iple_a] : ? [v9: fun_fu410471825a_bool] : ? [v10: % 139.97/19.34 | fun_Ho287446294a_bool] : ? [v11: bool] : (hAPP_state_bool(v2, v1) = % 139.97/19.34 | v3 & hAPP_s1806633685e_bool(all_1339_0, v1) = v4 & % 139.97/19.34 | hAPP_a2036067514e_bool(all_1337_4, v0) = v6 & % 139.97/19.34 | hAPP_a2036067514e_bool(all_1337_13, v0) = v2 & % 139.97/19.34 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v6) = v7 & % 139.97/19.34 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, v4) = v5 & % 139.97/19.34 | hAPP_H762155206a_bool(insert1051021594iple_a, v8) = v9 & % 139.97/19.34 | hAPP_f909437487a_bool(v9, bot_bo1766443648a_bool) = v10 & % 139.97/19.34 | hoare_196563068iple_a(v5, c, v7) = v8 & % 139.97/19.34 | hAPP_f2063540982l_bool(all_1337_15, v10) = v11 & % 139.97/19.34 | fun_fu410471825a_bool(v9) & fun_Ho287446294a_bool(v10) & % 139.97/19.34 | fun_state_bool(v6) & fun_state_bool(v4) & fun_state_bool(v2) & % 139.97/19.34 | fun_a_fun_state_bool(v7) & fun_a_fun_state_bool(v5) & % 139.97/19.34 | hoare_1544627872iple_a(v8) & bool(v11) & bool(v3) & state(v1) & % 139.97/19.34 | x_a(v0) & hBOOL(v3) & ~ hBOOL(v11)) % 139.97/19.34 | % 139.97/19.34 | DELTA: instantiating (23) with fresh symbols all_1419_0, all_1419_1, % 139.97/19.34 | all_1419_2, all_1419_3, all_1419_4, all_1419_5, all_1419_6, all_1419_7, % 139.97/19.34 | all_1419_8, all_1419_9, all_1419_10, all_1419_11 gives: % 139.97/19.34 | (24) hAPP_state_bool(all_1419_9, all_1419_10) = all_1419_8 & % 139.97/19.34 | hAPP_s1806633685e_bool(all_1339_0, all_1419_10) = all_1419_7 & % 139.97/19.34 | hAPP_a2036067514e_bool(all_1337_4, all_1419_11) = all_1419_5 & % 139.97/19.34 | hAPP_a2036067514e_bool(all_1337_13, all_1419_11) = all_1419_9 & % 139.97/19.34 | hAPP_f762886889e_bool(cOMBK_1458035955bool_a, all_1419_5) = all_1419_4 % 139.97/19.34 | & hAPP_f762886889e_bool(cOMBK_1458035955bool_a, all_1419_7) = % 139.97/19.34 | all_1419_6 & hAPP_H762155206a_bool(insert1051021594iple_a, all_1419_3) % 139.97/19.34 | = all_1419_2 & hAPP_f909437487a_bool(all_1419_2, % 139.97/19.34 | bot_bo1766443648a_bool) = all_1419_1 & % 139.97/19.34 | hoare_196563068iple_a(all_1419_6, c, all_1419_4) = all_1419_3 & % 139.97/19.34 | hAPP_f2063540982l_bool(all_1337_15, all_1419_1) = all_1419_0 & % 139.97/19.34 | fun_fu410471825a_bool(all_1419_2) & fun_Ho287446294a_bool(all_1419_1) % 139.97/19.34 | & fun_state_bool(all_1419_5) & fun_state_bool(all_1419_7) & % 139.97/19.34 | fun_state_bool(all_1419_9) & fun_a_fun_state_bool(all_1419_4) & % 139.97/19.34 | fun_a_fun_state_bool(all_1419_6) & hoare_1544627872iple_a(all_1419_3) % 139.97/19.34 | & bool(all_1419_0) & bool(all_1419_8) & state(all_1419_10) & % 139.97/19.34 | x_a(all_1419_11) & hBOOL(all_1419_8) & ~ hBOOL(all_1419_0) % 139.97/19.34 | % 139.97/19.34 | ALPHA: (24) implies: % 139.97/19.34 | (25) hBOOL(all_1419_8) % 139.97/19.34 | (26) x_a(all_1419_11) % 139.97/19.34 | (27) state(all_1419_10) % 139.97/19.34 | (28) hAPP_a2036067514e_bool(all_1337_13, all_1419_11) = all_1419_9 % 139.97/19.34 | (29) hAPP_state_bool(all_1419_9, all_1419_10) = all_1419_8 % 139.97/19.34 | % 139.97/19.34 | GROUND_INST: instantiating (4) with all_1337_14, all_1419_11, all_1337_13, % 139.97/19.34 | all_1419_9, simplifying with (13), (19), (26), (28) gives: % 139.97/19.34 | (30) all_1419_9 = all_1337_14 % 139.97/19.34 | % 139.97/19.34 | REDUCE: (29), (30) imply: % 139.97/19.34 | (31) hAPP_state_bool(all_1337_14, all_1419_10) = all_1419_8 % 139.97/19.34 | % 139.97/19.34 | GROUND_INST: instantiating (3) with fFalse, all_1419_10, all_1337_14, % 139.97/19.34 | all_1419_8, simplifying with (6), (20), (27), (31) gives: % 139.97/19.34 | (32) all_1419_8 = fFalse % 139.97/19.34 | % 139.97/19.34 | REDUCE: (25), (32) imply: % 139.97/19.34 | (33) hBOOL(fFalse) % 139.97/19.34 | % 139.97/19.34 | PRED_UNIFY: (2), (33) imply: % 139.97/19.34 | (34) $false % 139.97/19.34 | % 139.97/19.34 | CLOSE: (34) is inconsistent. % 139.97/19.34 | % 139.97/19.34 End of proof % 139.97/19.34 % SZS output end Proof for theBenchmark % 139.97/19.34 % 139.97/19.34 18730ms %------------------------------------------------------------------------------