%------------------------------------------------------------------------------ % 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 : n028.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 36.63s 5.85s % Output : Proof 58.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470+1 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n028.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 19:55:24 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.66 ________ _____ % 0.19/0.66 ___ __ \_________(_)________________________________ % 0.19/0.66 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.66 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.66 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.66 % 0.19/0.66 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.66 (2023-06-19) % 0.19/0.66 % 0.19/0.66 (c) Philipp Rümmer, 2009-2023 % 0.19/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.66 Amanda Stjerna. % 0.19/0.66 Free software under BSD-3-Clause. % 0.19/0.66 % 0.19/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.66 % 0.19/0.66 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.69 Running up to 7 provers in parallel. % 0.19/0.73 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.73 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.73 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.73 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.73 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.73 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.73 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 6.30/1.80 Prover 1: Preprocessing ... % 6.30/1.86 Prover 4: Preprocessing ... % 6.97/1.87 Prover 6: Preprocessing ... % 6.97/1.87 Prover 5: Preprocessing ... % 6.97/1.87 Prover 0: Preprocessing ... % 6.97/1.87 Prover 2: Preprocessing ... % 6.97/1.87 Prover 3: Preprocessing ... % 22.64/4.00 Prover 1: Warning: ignoring some quantifiers % 23.23/4.07 Prover 6: Proving ... % 23.50/4.11 Prover 3: Warning: ignoring some quantifiers % 23.90/4.15 Prover 1: Constructing countermodel ... % 24.09/4.18 Prover 3: Constructing countermodel ... % 24.88/4.28 Prover 4: Warning: ignoring some quantifiers % 25.45/4.45 Prover 0: Proving ... % 25.45/4.55 Prover 4: Constructing countermodel ... % 26.64/4.66 Prover 5: Proving ... % 32.23/5.38 Prover 2: Proving ... % 36.37/5.84 Prover 6: proved (5120ms) % 36.37/5.84 % 36.63/5.85 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.63/5.85 % 36.63/5.85 Prover 5: stopped % 36.63/5.85 Prover 0: stopped % 36.63/5.85 Prover 2: stopped % 36.63/5.86 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 36.63/5.86 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 36.63/5.86 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 36.63/5.87 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 36.63/5.87 Prover 3: stopped % 36.63/5.87 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 39.61/6.31 Prover 8: Preprocessing ... % 39.61/6.31 Prover 10: Preprocessing ... % 39.61/6.31 Prover 13: Preprocessing ... % 40.38/6.39 Prover 11: Preprocessing ... % 40.38/6.43 Prover 7: Preprocessing ... % 46.49/7.21 Prover 10: Warning: ignoring some quantifiers % 46.99/7.24 Prover 7: Warning: ignoring some quantifiers % 47.22/7.30 Prover 10: Constructing countermodel ... % 47.22/7.31 Prover 7: Constructing countermodel ... % 48.04/7.43 Prover 8: Warning: ignoring some quantifiers % 48.87/7.49 Prover 8: Constructing countermodel ... % 48.87/7.50 Prover 11: Warning: ignoring some quantifiers % 48.87/7.65 Prover 11: Constructing countermodel ... % 53.08/8.04 Prover 13: Warning: ignoring some quantifiers % 53.08/8.12 Prover 13: Constructing countermodel ... % 57.19/8.69 Prover 10: Found proof (size 18) % 57.19/8.69 Prover 10: proved (2827ms) % 57.19/8.69 Prover 7: stopped % 57.19/8.69 Prover 11: stopped % 57.19/8.69 Prover 13: stopped % 57.19/8.69 Prover 8: stopped % 57.19/8.69 Prover 1: stopped % 57.19/8.69 Prover 4: stopped % 57.19/8.69 % 57.19/8.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.19/8.69 % 57.19/8.70 % SZS output start Proof for theBenchmark % 57.19/8.70 Assumptions after simplification: % 57.19/8.70 --------------------------------- % 57.19/8.70 % 57.19/8.70 (conj_0) % 58.21/8.73 $i(b) & $i(p) & $i(c) & $i(g) & $i(cOMBC_892787026e_bool) & % 58.21/8.73 $i(cOMBS_1378840469l_bool) & $i(fNot) & $i(fconj) & $i(insert1871499715iple_a) % 58.21/8.73 & $i(bot_bo1687970473a_bool) & $i(fFalse) & ? [v0: $i] : ? [v1: $i] : ? % 58.21/8.73 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 58.21/8.73 : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? % 58.21/8.73 [v13: $i] : ? [v14: $i] : ? [v15: $i] : % 58.21/8.73 (cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = v3 & % 58.21/8.73 hAPP_f963367678e_bool(v3, v6) = v7 & % 58.21/8.73 hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 58.21/8.73 hAPP_f762886889e_bool(v8, v10) = v11 & cOMBB_160679318_state(fNot) = v9 & % 58.21/8.73 hAPP_f1759915619e_bool(v9, b) = v10 & cOMBK_bool_state(fFalse) = v1 & % 58.21/8.73 cOMBK_1458035955bool_a(v1) = v2 & cOMBB_188601460_state(fconj) = v4 & % 58.21/8.73 cOMBB_1355796797bool_a(v4) = v5 & hAPP_f1509969235l_bool(v5, p) = v6 & % 58.21/8.73 hAPP_H1816261935a_bool(insert1871499715iple_a, v12) = v13 & % 58.21/8.73 hAPP_f1400872321a_bool(v13, bot_bo1687970473a_bool) = v14 & % 58.21/8.73 hoare_1050552211iple_a(v2, c, v11) = v12 & hoare_472868247rivs_a(g) = v0 & % 58.21/8.73 hAPP_f1753944735l_bool(v0, v14) = v15 & $i(v15) & $i(v14) & $i(v13) & % 58.21/8.73 $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 58.21/8.73 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v15)) % 58.21/8.73 % 58.21/8.73 (fact_5_escape) % 58.21/8.74 $i(fequal_state) & $i(cOMBC_2027030106e_bool) & $i(insert1871499715iple_a) & % 58.21/8.74 $i(bot_bo1687970473a_bool) & ? [v0: $i] : % 58.21/8.74 (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = v0 & $i(v0) & % 58.21/8.74 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: % 58.21/8.74 $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ( ~ % 58.21/8.74 (hAPP_H1816261935a_bool(insert1871499715iple_a, v6) = v7) | ~ % 58.21/8.74 (hAPP_f1400872321a_bool(v7, bot_bo1687970473a_bool) = v8) | ~ % 58.21/8.74 (hoare_1050552211iple_a(v4, v2, v3) = v6) | ~ (hoare_472868247rivs_a(v1) % 58.21/8.74 = v5) | ~ (hAPP_f1753944735l_bool(v5, v8) = v9) | ~ $i(v4) | ~ $i(v3) % 58.21/8.74 | ~ $i(v2) | ~ $i(v1) | hBOOL(v9) | ? [v10: $i] : ? [v11: $i] : ? % 58.21/8.74 [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? % 58.21/8.74 [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? [v20: $i] : ? [v21: $i] : % 58.21/8.74 (hAPP_s1806633685e_bool(v0, v11) = v14 & hAPP_a2036067514e_bool(v4, v10) = % 58.21/8.74 v12 & hAPP_a2036067514e_bool(v3, v10) = v16 & % 58.21/8.74 cOMBK_1458035955bool_a(v16) = v17 & cOMBK_1458035955bool_a(v14) = v15 & % 58.21/8.74 hAPP_H1816261935a_bool(insert1871499715iple_a, v18) = v19 & % 58.21/8.74 hAPP_f1400872321a_bool(v19, bot_bo1687970473a_bool) = v20 & % 58.21/8.74 hoare_1050552211iple_a(v15, v2, v17) = v18 & hAPP_f1753944735l_bool(v5, % 58.21/8.74 v20) = v21 & hAPP_state_bool(v12, v11) = v13 & $i(v21) & $i(v20) & % 58.21/8.74 $i(v19) & $i(v18) & $i(v17) & $i(v16) & $i(v15) & $i(v14) & $i(v13) & % 58.21/8.74 $i(v12) & $i(v11) & $i(v10) & hBOOL(v13) & ~ hBOOL(v21)))) % 58.21/8.74 % 58.21/8.74 (gsy_c_fFalse) % 58.21/8.74 $i(fFalse) & is_bool(fFalse) % 58.21/8.74 % 58.21/8.74 (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) % 58.21/8.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 | ~ % 58.21/8.74 (cOMBK_bool_state(v0) = v2) | ~ (hAPP_state_bool(v2, v1) = v3) | ~ $i(v1) % 58.21/8.74 | ~ $i(v0) | ~ is_bool(v0)) % 58.21/8.74 % 58.21/8.74 (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 58.21/8.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 | ~ % 58.21/8.74 (hAPP_a2036067514e_bool(v2, v1) = v3) | ~ (cOMBK_1458035955bool_a(v0) = v2) % 58.21/8.74 | ~ $i(v1) | ~ $i(v0)) % 58.21/8.74 % 58.21/8.74 (help_fFalse_1_1_U) % 58.21/8.74 $i(fFalse) & ~ hBOOL(fFalse) % 58.21/8.74 % 58.21/8.74 Further assumptions not needed in the proof: % 58.21/8.74 -------------------------------------------- % 58.21/8.74 fact_0_empty, fact_10_insertCI, fact_11_emptyE, fact_12_singleton__conv2, % 58.21/8.74 fact_13_singleton__conv, fact_14_Collect__conv__if2, fact_15_Collect__conv__if, % 58.21/8.74 fact_16_equals0D, fact_17_Collect__empty__eq, fact_18_empty__iff, % 58.21/8.74 fact_19_empty__Collect__eq, fact_1_triple_Oinject, fact_20_ex__in__conv, % 58.21/8.74 fact_21_all__not__in__conv, fact_22_empty__def, fact_23_insert__absorb, % 58.21/8.74 fact_24_insertI2, fact_25_insert__ident, fact_26_insert__code, % 58.21/8.74 fact_27_insert__iff, fact_28_insert__commute, fact_29_insert__absorb2, % 58.21/8.74 fact_2_cut, fact_30_insert__Collect, fact_31_insert__compr, fact_32_insertI1, % 58.21/8.74 fact_33_insert__compr__raw, fact_34_singleton__inject, fact_35_singletonE, % 58.21/8.74 fact_36_doubleton__eq__iff, fact_37_singleton__iff, fact_38_insert__not__empty, % 58.21/8.74 fact_39_empty__not__insert, fact_3_hoare__derivs_Oinsert, fact_40_the__elem__eq, % 58.21/8.74 fact_41_bot__apply, fact_42_bot__fun__def, fact_43_hoare__derivs_OSkip, % 58.21/8.74 fact_44_Comp, fact_45_triple_Oexhaust, fact_46_Set_Oset__insert, % 58.21/8.74 fact_47_com_Osimps_I13_J, fact_48_com_Osimps_I12_J, fact_49_the__elem__def, % 58.21/8.74 fact_4_constant, fact_50_mk__disjoint__insert, fact_51_com_Osimps_I3_J, % 58.21/8.74 fact_52_the__sym__eq__trivial, fact_53_the__eq__trivial, fact_54_If__def, % 58.21/8.74 fact_55_equals0I, fact_56_the__equality, fact_57_theI, fact_58_the1__equality, % 58.21/8.74 fact_59_theI_H, fact_60_conseq, fact_61_nonempty__iff, fact_62_fold1Set__sing, % 58.21/8.74 fact_63_folding__one_Osingleton, fact_64_bot__empty__eq, % 58.21/8.74 fact_65_empty__fold1SetE, fact_66_fold1Set__nonempty, fact_67_fold1Set_Ointros, % 58.21/8.74 fact_68_folding__one_Oinsert, fact_69_fold1__def, fact_6_conseq2, % 58.21/8.74 fact_70_finite__Collect__conjI, fact_71_finite_OemptyI, fact_72_finite_OinsertI, % 58.21/8.74 fact_73_mem__def, fact_74_Collect__def, fact_75_folding__one_Oeq__fold, % 58.21/8.74 fact_76_fold__graph_OemptyI, fact_77_empty__fold__graphE, % 58.21/8.74 fact_78_fold__graph_OinsertI, fact_79_finite__Collect__disjI, fact_7_conseq1, % 58.21/8.74 fact_80_finite__insert, fact_81_fold1__singleton__def, fact_82_fold1__singleton, % 58.21/8.74 fact_83_folding__one_Oclosed, fact_84_insert__fold1SetE, % 58.21/8.74 fact_85_finite__nonempty__imp__fold1Set, fact_86_finite__induct, % 58.21/8.74 fact_87_finite_Osimps, fact_88_finite__imp__fold__graph, % 58.21/8.74 fact_89_fold1Set_Osimps, fact_8_conseq12, fact_90_fold__graph_Osimps, % 58.21/8.74 fact_91_folding__one__idem_Oinsert__idem, fact_92_finite__ne__induct, % 58.21/8.74 fact_93_folding__one__idem_Oidem, fact_94_folding__one__idem_Oin__idem, % 58.21/8.74 fact_9_insertE, % 58.21/8.74 gsy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____jfehddehev__Otriple, % 58.21/8.74 gsy_c_Finite__Set_Ofolding__one__idem_000tc__Hoare____Mirabelle____jfehddehev__O, % 58.21/8.74 gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool, gsy_c_fTrue, % 58.21/8.74 gsy_c_hAPP_000tc__Com__Ostate_000tc__HOL__Obool, % 58.21/8.74 gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool, % 58.21/8.74 gsy_c_hAPP_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_000tc__HOL__, % 58.21/8.74 gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_Mtc, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Ostate_U, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Hoare____Mirabel, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_001, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc__fun_It, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Ostate_Mtc__fun_Itc__HOL__Obool_Mtc__H_003, % 58.21/8.74 help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____jfehddehev__Otriple_I, % 58.21/8.74 help_COMBC_1_1_COMBC_000t__a_000tc__HOL__Obool_000tc__fun_Itc__Com__Ostate_Mtc__, % 58.21/8.74 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000tc, % 58.21/8.74 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__Com__Ostate_000tc__HOL__Obool_U, % 58.21/8.74 help_COMBC_1_1_COMBC_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 58.21/8.74 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_00, % 58.21/8.74 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_00_002, % 58.21/8.74 help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_00_004, % 58.21/8.74 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____jfehddehev__, % 58.21/8.74 help_COMBS_1_1_COMBS_000tc__Com__Ostate_000tc__HOL__Obool_000tc__HOL__Obool_U, % 58.21/8.74 help_COMBS_1_1_COMBS_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_00, % 58.21/8.74 help_fFalse_1_1_T, help_fNot_1_1_U, help_fNot_2_1_U, help_fconj_1_1_U, % 58.21/8.74 help_fconj_2_1_U, help_fconj_3_1_U, help_fdisj_1_1_U, help_fdisj_2_1_U, % 58.21/8.74 help_fdisj_3_1_U, help_fequal_1_1_fequal_000tc__Com__Ostate_T, % 58.21/8.74 help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_, % 58.21/8.74 help_fequal_1_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____jfehddehev__Otriple, % 58.21/8.74 help_fequal_2_1_fequal_000tc__Com__Ostate_T, % 58.21/8.74 help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____jfehddehev__Otriple_It__a_J_, % 58.21/8.74 help_fequal_2_1_fequal_000tc__fun_Itc__Hoare____Mirabelle____jfehddehev__Otriple, % 58.21/8.74 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 58.21/8.74 % 58.21/8.74 Those formulas are unsatisfiable: % 58.21/8.74 --------------------------------- % 58.21/8.74 % 58.21/8.74 Begin of proof % 58.21/8.74 | % 58.21/8.74 | ALPHA: (gsy_c_fFalse) implies: % 58.21/8.74 | (1) is_bool(fFalse) % 58.21/8.74 | % 58.21/8.74 | ALPHA: (fact_5_escape) implies: % 58.21/8.74 | (2) ? [v0: $i] : (hAPP_f817621513e_bool(cOMBC_2027030106e_bool, % 58.21/8.74 | fequal_state) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: % 58.21/8.74 | $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! % 58.21/8.75 | [v8: $i] : ! [v9: $i] : ( ~ % 58.21/8.75 | (hAPP_H1816261935a_bool(insert1871499715iple_a, v6) = v7) | ~ % 58.21/8.75 | (hAPP_f1400872321a_bool(v7, bot_bo1687970473a_bool) = v8) | ~ % 58.21/8.75 | (hoare_1050552211iple_a(v4, v2, v3) = v6) | ~ % 58.21/8.75 | (hoare_472868247rivs_a(v1) = v5) | ~ (hAPP_f1753944735l_bool(v5, % 58.21/8.75 | v8) = v9) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 58.21/8.75 | hBOOL(v9) | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: % 58.21/8.75 | $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : % 58.21/8.75 | ? [v18: $i] : ? [v19: $i] : ? [v20: $i] : ? [v21: $i] : % 58.21/8.75 | (hAPP_s1806633685e_bool(v0, v11) = v14 & hAPP_a2036067514e_bool(v4, % 58.21/8.75 | v10) = v12 & hAPP_a2036067514e_bool(v3, v10) = v16 & % 58.21/8.75 | cOMBK_1458035955bool_a(v16) = v17 & cOMBK_1458035955bool_a(v14) = % 58.21/8.75 | v15 & hAPP_H1816261935a_bool(insert1871499715iple_a, v18) = v19 & % 58.21/8.75 | hAPP_f1400872321a_bool(v19, bot_bo1687970473a_bool) = v20 & % 58.21/8.75 | hoare_1050552211iple_a(v15, v2, v17) = v18 & % 58.21/8.75 | hAPP_f1753944735l_bool(v5, v20) = v21 & hAPP_state_bool(v12, v11) % 58.21/8.75 | = v13 & $i(v21) & $i(v20) & $i(v19) & $i(v18) & $i(v17) & $i(v16) % 58.21/8.75 | & $i(v15) & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & % 58.21/8.75 | hBOOL(v13) & ~ hBOOL(v21)))) % 58.21/8.75 | % 58.21/8.75 | ALPHA: (help_fFalse_1_1_U) implies: % 58.21/8.75 | (3) ~ hBOOL(fFalse) % 58.21/8.75 | % 58.21/8.75 | ALPHA: (conj_0) implies: % 58.21/8.75 | (4) $i(fFalse) % 58.21/8.75 | (5) $i(g) % 58.21/8.75 | (6) $i(c) % 58.21/8.75 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 58.21/8.75 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 58.21/8.75 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 58.21/8.75 | ? [v15: $i] : (cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = v3 & % 58.21/8.75 | hAPP_f963367678e_bool(v3, v6) = v7 & % 58.21/8.75 | hAPP_f1261923407e_bool(cOMBC_892787026e_bool, v7) = v8 & % 58.21/8.75 | hAPP_f762886889e_bool(v8, v10) = v11 & cOMBB_160679318_state(fNot) = % 58.21/8.75 | v9 & hAPP_f1759915619e_bool(v9, b) = v10 & cOMBK_bool_state(fFalse) = % 58.21/8.75 | v1 & cOMBK_1458035955bool_a(v1) = v2 & cOMBB_188601460_state(fconj) = % 58.21/8.75 | v4 & cOMBB_1355796797bool_a(v4) = v5 & hAPP_f1509969235l_bool(v5, p) % 58.21/8.75 | = v6 & hAPP_H1816261935a_bool(insert1871499715iple_a, v12) = v13 & % 58.21/8.75 | hAPP_f1400872321a_bool(v13, bot_bo1687970473a_bool) = v14 & % 58.21/8.75 | hoare_1050552211iple_a(v2, c, v11) = v12 & hoare_472868247rivs_a(g) = % 58.21/8.75 | v0 & hAPP_f1753944735l_bool(v0, v14) = v15 & $i(v15) & $i(v14) & % 58.21/8.75 | $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & % 58.21/8.75 | $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ % 58.21/8.75 | hBOOL(v15)) % 58.21/8.75 | % 58.21/8.75 | DELTA: instantiating (7) with fresh symbols all_162_0, all_162_1, all_162_2, % 58.21/8.75 | all_162_3, all_162_4, all_162_5, all_162_6, all_162_7, all_162_8, % 58.21/8.75 | all_162_9, all_162_10, all_162_11, all_162_12, all_162_13, all_162_14, % 58.21/8.75 | all_162_15 gives: % 58.21/8.75 | (8) cOMBB_145932198bool_a(cOMBS_1378840469l_bool) = all_162_12 & % 58.21/8.75 | hAPP_f963367678e_bool(all_162_12, all_162_9) = all_162_8 & % 58.21/8.75 | hAPP_f1261923407e_bool(cOMBC_892787026e_bool, all_162_8) = all_162_7 & % 58.21/8.75 | hAPP_f762886889e_bool(all_162_7, all_162_5) = all_162_4 & % 58.21/8.75 | cOMBB_160679318_state(fNot) = all_162_6 & % 58.21/8.75 | hAPP_f1759915619e_bool(all_162_6, b) = all_162_5 & % 58.21/8.75 | cOMBK_bool_state(fFalse) = all_162_14 & % 58.21/8.75 | cOMBK_1458035955bool_a(all_162_14) = all_162_13 & % 58.21/8.75 | cOMBB_188601460_state(fconj) = all_162_11 & % 58.21/8.75 | cOMBB_1355796797bool_a(all_162_11) = all_162_10 & % 58.21/8.75 | hAPP_f1509969235l_bool(all_162_10, p) = all_162_9 & % 58.21/8.75 | hAPP_H1816261935a_bool(insert1871499715iple_a, all_162_3) = all_162_2 & % 58.21/8.75 | hAPP_f1400872321a_bool(all_162_2, bot_bo1687970473a_bool) = all_162_1 & % 58.21/8.75 | hoare_1050552211iple_a(all_162_13, c, all_162_4) = all_162_3 & % 58.21/8.75 | hoare_472868247rivs_a(g) = all_162_15 & % 58.21/8.75 | hAPP_f1753944735l_bool(all_162_15, all_162_1) = all_162_0 & % 58.21/8.75 | $i(all_162_0) & $i(all_162_1) & $i(all_162_2) & $i(all_162_3) & % 58.21/8.75 | $i(all_162_4) & $i(all_162_5) & $i(all_162_6) & $i(all_162_7) & % 58.21/8.75 | $i(all_162_8) & $i(all_162_9) & $i(all_162_10) & $i(all_162_11) & % 58.21/8.75 | $i(all_162_12) & $i(all_162_13) & $i(all_162_14) & $i(all_162_15) & ~ % 58.21/8.75 | hBOOL(all_162_0) % 58.21/8.75 | % 58.21/8.75 | ALPHA: (8) implies: % 58.21/8.75 | (9) ~ hBOOL(all_162_0) % 58.21/8.75 | (10) $i(all_162_14) % 58.21/8.75 | (11) $i(all_162_13) % 58.21/8.75 | (12) $i(all_162_4) % 58.21/8.75 | (13) hAPP_f1753944735l_bool(all_162_15, all_162_1) = all_162_0 % 58.21/8.75 | (14) hoare_472868247rivs_a(g) = all_162_15 % 58.21/8.75 | (15) hoare_1050552211iple_a(all_162_13, c, all_162_4) = all_162_3 % 58.21/8.75 | (16) hAPP_f1400872321a_bool(all_162_2, bot_bo1687970473a_bool) = all_162_1 % 58.21/8.75 | (17) hAPP_H1816261935a_bool(insert1871499715iple_a, all_162_3) = all_162_2 % 58.21/8.75 | (18) cOMBK_1458035955bool_a(all_162_14) = all_162_13 % 58.21/8.75 | (19) cOMBK_bool_state(fFalse) = all_162_14 % 58.21/8.75 | % 58.21/8.75 | DELTA: instantiating (2) with fresh symbol all_164_0 gives: % 58.21/8.76 | (20) hAPP_f817621513e_bool(cOMBC_2027030106e_bool, fequal_state) = % 58.21/8.76 | all_164_0 & $i(all_164_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 58.21/8.76 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 58.21/8.76 | ! [v8: $i] : ( ~ (hAPP_H1816261935a_bool(insert1871499715iple_a, v5) = % 58.21/8.76 | v6) | ~ (hAPP_f1400872321a_bool(v6, bot_bo1687970473a_bool) = v7) % 58.21/8.76 | | ~ (hoare_1050552211iple_a(v3, v1, v2) = v5) | ~ % 58.21/8.76 | (hoare_472868247rivs_a(v0) = v4) | ~ (hAPP_f1753944735l_bool(v4, % 58.21/8.76 | v7) = v8) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 58.21/8.76 | hBOOL(v8) | ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 58.21/8.76 | : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? % 58.21/8.76 | [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? [v20: $i] : % 58.21/8.76 | (hAPP_s1806633685e_bool(all_164_0, v10) = v13 & % 58.21/8.76 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 58.21/8.76 | v9) = v15 & cOMBK_1458035955bool_a(v15) = v16 & % 58.21/8.76 | cOMBK_1458035955bool_a(v13) = v14 & % 58.21/8.76 | hAPP_H1816261935a_bool(insert1871499715iple_a, v17) = v18 & % 58.21/8.76 | hAPP_f1400872321a_bool(v18, bot_bo1687970473a_bool) = v19 & % 58.21/8.76 | hoare_1050552211iple_a(v14, v1, v16) = v17 & % 58.21/8.76 | hAPP_f1753944735l_bool(v4, v19) = v20 & hAPP_state_bool(v11, v10) % 58.21/8.76 | = v12 & $i(v20) & $i(v19) & $i(v18) & $i(v17) & $i(v16) & $i(v15) % 58.21/8.76 | & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & % 58.21/8.76 | hBOOL(v12) & ~ hBOOL(v20))) % 58.21/8.76 | % 58.21/8.76 | ALPHA: (20) implies: % 58.21/8.76 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 58.21/8.76 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 58.21/8.76 | (hAPP_H1816261935a_bool(insert1871499715iple_a, v5) = v6) | ~ % 58.21/8.76 | (hAPP_f1400872321a_bool(v6, bot_bo1687970473a_bool) = v7) | ~ % 58.21/8.76 | (hoare_1050552211iple_a(v3, v1, v2) = v5) | ~ % 58.21/8.76 | (hoare_472868247rivs_a(v0) = v4) | ~ (hAPP_f1753944735l_bool(v4, % 58.21/8.76 | v7) = v8) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 58.21/8.76 | hBOOL(v8) | ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 58.21/8.76 | : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? % 58.21/8.76 | [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? [v20: $i] : % 58.21/8.76 | (hAPP_s1806633685e_bool(all_164_0, v10) = v13 & % 58.21/8.76 | hAPP_a2036067514e_bool(v3, v9) = v11 & hAPP_a2036067514e_bool(v2, % 58.21/8.76 | v9) = v15 & cOMBK_1458035955bool_a(v15) = v16 & % 58.21/8.76 | cOMBK_1458035955bool_a(v13) = v14 & % 58.21/8.76 | hAPP_H1816261935a_bool(insert1871499715iple_a, v17) = v18 & % 58.21/8.76 | hAPP_f1400872321a_bool(v18, bot_bo1687970473a_bool) = v19 & % 58.21/8.76 | hoare_1050552211iple_a(v14, v1, v16) = v17 & % 58.21/8.76 | hAPP_f1753944735l_bool(v4, v19) = v20 & hAPP_state_bool(v11, v10) % 58.21/8.76 | = v12 & $i(v20) & $i(v19) & $i(v18) & $i(v17) & $i(v16) & $i(v15) % 58.21/8.76 | & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & % 58.21/8.76 | hBOOL(v12) & ~ hBOOL(v20))) % 58.21/8.76 | % 58.21/8.76 | GROUND_INST: instantiating (21) with g, c, all_162_4, all_162_13, all_162_15, % 58.21/8.76 | all_162_3, all_162_2, all_162_1, all_162_0, simplifying with (5), % 58.21/8.76 | (6), (9), (11), (12), (13), (14), (15), (16), (17) gives: % 58.21/8.76 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 58.21/8.76 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 58.21/8.76 | ? [v10: $i] : ? [v11: $i] : (hAPP_s1806633685e_bool(all_164_0, v1) = % 58.21/8.76 | v4 & hAPP_a2036067514e_bool(all_162_4, v0) = v6 & % 58.21/8.76 | hAPP_a2036067514e_bool(all_162_13, v0) = v2 & % 58.21/8.76 | cOMBK_1458035955bool_a(v6) = v7 & cOMBK_1458035955bool_a(v4) = v5 & % 58.21/8.76 | hAPP_H1816261935a_bool(insert1871499715iple_a, v8) = v9 & % 58.21/8.76 | hAPP_f1400872321a_bool(v9, bot_bo1687970473a_bool) = v10 & % 58.21/8.76 | hoare_1050552211iple_a(v5, c, v7) = v8 & % 58.21/8.76 | hAPP_f1753944735l_bool(all_162_15, v10) = v11 & hAPP_state_bool(v2, % 58.21/8.76 | v1) = v3 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 58.21/8.76 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & hBOOL(v3) & ~ % 58.21/8.76 | hBOOL(v11)) % 58.21/8.76 | % 58.21/8.76 | DELTA: instantiating (22) with fresh symbols all_198_0, all_198_1, all_198_2, % 58.21/8.76 | all_198_3, all_198_4, all_198_5, all_198_6, all_198_7, all_198_8, % 58.21/8.76 | all_198_9, all_198_10, all_198_11 gives: % 58.21/8.76 | (23) hAPP_s1806633685e_bool(all_164_0, all_198_10) = all_198_7 & % 58.21/8.76 | hAPP_a2036067514e_bool(all_162_4, all_198_11) = all_198_5 & % 58.21/8.76 | hAPP_a2036067514e_bool(all_162_13, all_198_11) = all_198_9 & % 58.21/8.76 | cOMBK_1458035955bool_a(all_198_5) = all_198_4 & % 58.21/8.76 | cOMBK_1458035955bool_a(all_198_7) = all_198_6 & % 58.21/8.76 | hAPP_H1816261935a_bool(insert1871499715iple_a, all_198_3) = all_198_2 % 58.21/8.76 | & hAPP_f1400872321a_bool(all_198_2, bot_bo1687970473a_bool) = % 58.21/8.76 | all_198_1 & hoare_1050552211iple_a(all_198_6, c, all_198_4) = % 58.21/8.76 | all_198_3 & hAPP_f1753944735l_bool(all_162_15, all_198_1) = all_198_0 % 58.21/8.76 | & hAPP_state_bool(all_198_9, all_198_10) = all_198_8 & $i(all_198_0) & % 58.21/8.76 | $i(all_198_1) & $i(all_198_2) & $i(all_198_3) & $i(all_198_4) & % 58.21/8.76 | $i(all_198_5) & $i(all_198_6) & $i(all_198_7) & $i(all_198_8) & % 58.21/8.76 | $i(all_198_9) & $i(all_198_10) & $i(all_198_11) & hBOOL(all_198_8) & % 58.21/8.76 | ~ hBOOL(all_198_0) % 58.21/8.76 | % 58.21/8.76 | ALPHA: (23) implies: % 58.21/8.76 | (24) hBOOL(all_198_8) % 58.21/8.76 | (25) $i(all_198_11) % 58.21/8.76 | (26) $i(all_198_10) % 58.21/8.76 | (27) hAPP_state_bool(all_198_9, all_198_10) = all_198_8 % 58.21/8.76 | (28) hAPP_a2036067514e_bool(all_162_13, all_198_11) = all_198_9 % 58.21/8.76 | % 58.21/8.76 | GROUND_INST: instantiating % 58.21/8.76 | (help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) % 58.21/8.76 | with all_162_14, all_198_11, all_162_13, all_198_9, simplifying % 58.21/8.76 | with (10), (18), (25), (28) gives: % 58.21/8.77 | (29) all_198_9 = all_162_14 % 58.21/8.77 | % 58.21/8.77 | REDUCE: (27), (29) imply: % 58.21/8.77 | (30) hAPP_state_bool(all_162_14, all_198_10) = all_198_8 % 58.21/8.77 | % 58.21/8.77 | GROUND_INST: instantiating % 58.21/8.77 | (help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) % 58.21/8.77 | with fFalse, all_198_10, all_162_14, all_198_8, simplifying with % 58.21/8.77 | (1), (4), (19), (26), (30) gives: % 58.21/8.77 | (31) all_198_8 = fFalse % 58.21/8.77 | % 58.21/8.77 | REDUCE: (24), (31) imply: % 58.21/8.77 | (32) hBOOL(fFalse) % 58.21/8.77 | % 58.21/8.77 | PRED_UNIFY: (3), (32) imply: % 58.21/8.77 | (33) $false % 58.21/8.77 | % 58.21/8.77 | CLOSE: (33) is inconsistent. % 58.21/8.77 | % 58.21/8.77 End of proof % 58.21/8.77 % SZS output end Proof for theBenchmark % 58.21/8.77 % 58.21/8.77 8104ms %------------------------------------------------------------------------------