%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:11:40 EDT 2023 % Result : Theorem 56.51s 8.13s % Output : Proof 92.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.00/0.09 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.28 % Computer : n032.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 300 % 0.10/0.28 % DateTime : Sun Aug 27 15:35:45 EDT 2023 % 0.10/0.28 % CPUTime : % 0.14/0.48 ________ _____ % 0.14/0.48 ___ __ \_________(_)________________________________ % 0.14/0.48 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.14/0.48 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.14/0.48 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.14/0.48 % 0.14/0.48 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.14/0.48 (2023-06-19) % 0.14/0.48 % 0.14/0.48 (c) Philipp Rümmer, 2009-2023 % 0.14/0.48 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.14/0.48 Amanda Stjerna. % 0.14/0.48 Free software under BSD-3-Clause. % 0.14/0.48 % 0.14/0.48 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.14/0.48 % 0.14/0.48 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.14/0.49 Running up to 7 provers in parallel. % 0.14/0.50 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.14/0.50 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.14/0.50 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.14/0.50 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.14/0.50 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.14/0.50 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.14/0.50 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 14.35/2.54 Prover 5: Preprocessing ... % 14.35/2.54 Prover 0: Preprocessing ... % 14.35/2.54 Prover 6: Preprocessing ... % 15.44/2.65 Prover 1: Preprocessing ... % 15.44/2.67 Prover 3: Preprocessing ... % 15.44/2.67 Prover 2: Preprocessing ... % 16.20/2.83 Prover 4: Preprocessing ... % 39.30/5.93 Prover 1: Warning: ignoring some quantifiers % 39.30/5.97 Prover 3: Warning: ignoring some quantifiers % 40.77/6.09 Prover 3: Constructing countermodel ... % 41.46/6.11 Prover 1: Constructing countermodel ... % 43.22/6.38 Prover 6: Proving ... % 45.05/6.80 Prover 4: Warning: ignoring some quantifiers % 48.97/7.13 Prover 4: Constructing countermodel ... % 53.35/7.71 Prover 0: Proving ... % 53.46/7.81 Prover 5: Proving ... % 56.51/8.11 Prover 6: proved (7615ms) % 56.51/8.11 % 56.51/8.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.51/8.13 % 56.51/8.14 Prover 5: stopped % 56.51/8.14 Prover 0: stopped % 56.51/8.15 Prover 3: stopped % 56.51/8.16 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 56.51/8.16 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 56.51/8.16 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 56.51/8.16 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 59.89/8.56 Prover 2: Proving ... % 59.89/8.56 Prover 2: stopped % 59.89/8.58 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 65.35/9.30 Prover 7: Preprocessing ... % 65.35/9.31 Prover 11: Preprocessing ... % 65.35/9.33 Prover 10: Preprocessing ... % 65.35/9.34 Prover 8: Preprocessing ... % 67.28/9.55 Prover 13: Preprocessing ... % 78.52/11.01 Prover 10: Warning: ignoring some quantifiers % 78.52/11.09 Prover 8: Warning: ignoring some quantifiers % 78.52/11.14 Prover 10: Constructing countermodel ... % 80.40/11.26 Prover 7: Warning: ignoring some quantifiers % 80.40/11.31 Prover 8: Constructing countermodel ... % 82.57/11.57 Prover 7: Constructing countermodel ... % 84.28/11.85 Prover 11: Warning: ignoring some quantifiers % 86.55/12.07 Prover 11: Constructing countermodel ... % 87.11/12.16 Prover 13: Warning: ignoring some quantifiers % 89.44/12.43 Prover 13: Constructing countermodel ... % 90.44/12.64 Prover 4: Found proof (size 56) % 90.44/12.64 Prover 4: proved (12148ms) % 90.44/12.64 Prover 10: stopped % 90.44/12.64 Prover 11: stopped % 90.44/12.64 Prover 8: stopped % 90.44/12.64 Prover 7: stopped % 90.44/12.65 Prover 1: stopped % 90.44/12.69 Prover 13: stopped % 90.44/12.69 % 90.44/12.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.44/12.69 % 91.40/12.70 % SZS output start Proof for theBenchmark % 91.40/12.75 Assumptions after simplification: % 91.40/12.75 --------------------------------- % 91.40/12.75 % 91.40/12.75 (axiom123) % 91.61/12.78 B_character_data_ptr_b_character_data_ptr_option_fun$(some$) & % 91.61/12.78 B_character_data_ptr_option_b_character_data_ptr_fun$(the$) & % 91.61/12.78 B_character_data_ptr_option$(none$) & ! [v0: B_character_data_ptr_option$] : % 91.61/12.78 ! [v1: B_character_data_ptr$] : (v0 = none$ | ~ (fun_app$al(the$, v0) = v1) | % 91.61/12.78 ~ B_character_data_ptr_option$(v0) | fun_app$t(some$, v1) = v0) % 91.61/12.78 % 91.61/12.78 (axiom139) % 91.61/12.78 tlbool(tlfalse) & B_character_data_ptr_bool_fun$(uu$) & % 91.61/12.78 B_character_data_ptr_option$(none$) & ? [v0: % 91.61/12.78 B_character_data_ptr_option_bool_fun$] : (case_option$(tlfalse, uu$) = v0 & % 91.61/12.78 B_character_data_ptr_option_bool_fun$(v0) & ~ (fun_app$b(v0, none$) = 0) & % 91.61/12.78 ! [v1: B_character_data_ptr_option$] : ! [v2: int] : (v2 = 0 | v1 = none$ | % 91.61/12.78 ~ (fun_app$b(v0, v1) = v2) | ~ B_character_data_ptr_option$(v1))) % 91.70/12.78 % 91.70/12.78 (axiom162) % 91.70/12.78 B_character_data_ptr_b_character_data_ptr_option_fun$(some$) & % 91.70/12.78 B_character_data_ptr_option_b_character_data_ptr_fun$(the$) & % 91.70/12.78 B_character_data_ptr_option$(none$) & ! [v0: B_character_data_ptr_option$] : % 91.70/12.78 ! [v1: B_character_data_ptr$] : (v0 = none$ | ~ (fun_app$al(the$, v0) = v1) | % 91.70/12.78 ~ B_character_data_ptr_option$(v0) | fun_app$t(some$, v1) = v0) % 91.70/12.78 % 91.70/12.78 (axiom211) % 91.70/12.78 ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Bool_set$] : ! % 91.70/12.78 [v3: Bool_set$] : (v3 = v2 | ~ (collect$c(v1) = v3) | ~ (collect$c(v0) = v2) % 91.70/12.78 | ~ Bool_bool_fun$(v1) | ~ Bool_bool_fun$(v0) | ? [v4: tlbool] : ? [v5: % 91.70/12.78 any] : ? [v6: any] : (fun_app$j(v1, v4) = v6 & fun_app$j(v0, v4) = v5 & % 91.70/12.78 tlbool(v4) & ( ~ (v6 = 0) | ~ (v5 = 0)) & (v6 = 0 | v5 = 0))) % 91.70/12.78 % 91.70/12.78 (axiom354) % 91.70/12.78 A_element_ptr_b_character_data_ptr_option_fun$(uvf$) & % 91.70/12.78 C_b_character_data_ptr_option_fun$(uvg$) & % 91.70/12.78 B_character_data_ptr_b_character_data_ptr_option_fun$(some$) & ? [v0: % 91.70/12.78 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ? [v1: % 91.70/12.78 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 91.70/12.78 : (case_sum$a(some$, uvg$) = v0 & case_sum$(uvf$, v0) = v1 & % 91.70/12.78 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$(v1) % 91.70/12.78 & B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$(v0) & ! [v2: % 91.70/12.78 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v3: % 91.70/12.78 B_character_data_ptr_option$] : ( ~ (case_node_ptr$(v1, v2) = v3) | ~ % 91.70/12.78 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) | % 91.70/12.78 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v3 & % 91.70/12.78 B_character_data_ptr_option$(v3))) & ! [v2: % 91.70/12.78 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v3: % 91.70/12.78 B_character_data_ptr_option$] : ( ~ % 91.70/12.78 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v3) | ~ % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) | % 91.70/12.79 (case_node_ptr$(v1, v2) = v3 & B_character_data_ptr_option$(v3)))) % 91.70/12.79 % 91.70/12.79 (axiom489) % 91.70/12.79 collect$c(bot$g) = bot$ & Bool_set$(bot$) & Bool_bool_fun$(bot$g) % 91.70/12.79 % 91.70/12.79 (axiom527) % 91.70/12.79 Bool_set$(bot$) & Bool_bool_fun$(bot$g) & ! [v0: tlbool] : ! [v1: int] : (v1 % 91.70/12.79 = 0 | ~ (fun_app$j(bot$g, v0) = v1) | ~ tlbool(v0) | ? [v2: % 91.70/12.79 Bool_set_bool_fun$] : ? [v3: int] : ( ~ (v3 = 0) & member$a(v0) = v2 & % 91.70/12.79 fun_app$k(v2, bot$) = v3 & Bool_set_bool_fun$(v2))) & ! [v0: tlbool] : ! % 91.70/12.79 [v1: Bool_set_bool_fun$] : ( ~ (member$a(v0) = v1) | ~ tlbool(v0) | ? [v2: % 91.70/12.79 any] : ? [v3: any] : (fun_app$k(v1, bot$) = v3 & fun_app$j(bot$g, v0) = % 91.70/12.79 v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: tlbool] : ! [v1: % 91.70/12.79 Bool_set_bool_fun$] : ( ~ (member$a(v0) = v1) | ~ tlbool(v0) | ? [v2: any] % 91.70/12.79 : ? [v3: any] : (fun_app$k(v1, bot$) = v2 & fun_app$j(bot$g, v0) = v3 & ( ~ % 91.70/12.79 (v2 = 0) | v3 = 0))) & ! [v0: tlbool] : ( ~ (fun_app$j(bot$g, v0) = 0) % 91.70/12.79 | ~ tlbool(v0) | ? [v1: Bool_set_bool_fun$] : (member$a(v0) = v1 & % 91.70/12.79 fun_app$k(v1, bot$) = 0 & Bool_set_bool_fun$(v1))) % 91.70/12.79 % 91.70/12.79 (axiom551) % 91.70/12.79 ~ (top$ = bot$) & Bool_set$(top$) & Bool_set$(bot$) % 91.70/12.79 % 91.70/12.79 (axiom553) % 91.70/12.79 collect$c(uua$) = top$ & Bool_set$(top$) & Bool_bool_fun$(uua$) % 91.70/12.79 % 91.70/12.79 (axiom86) % 91.70/12.79 is_character_data_ptr_kind_n_o_d_e_p_t_r$(node_ptr$) = 0 & % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(node_ptr$) % 91.70/12.79 % 91.70/12.79 (axiom88) % 91.70/12.79 B_character_data_ptr_b_character_data_ptr_option_fun$(some$) & ! [v0: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 91.70/12.79 B_character_data_ptr$] : ! [v2: B_character_data_ptr_option$] : ! [v3: % 91.70/12.79 B_character_data_ptr_option$] : (v3 = v2 | ~ % 91.70/12.79 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v2) | ~ % 91.70/12.79 (fun_app$t(some$, v1) = v3) | ~ B_character_data_ptr$(v1) | ~ % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v4: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ (v4 = v0) & % 91.70/12.79 cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v4 & % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v4))) & ! [v0: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 91.70/12.79 B_character_data_ptr$] : ! [v2: B_character_data_ptr_option$] : ! [v3: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v3 = v0 | ~ % 91.70/12.79 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v2) | ~ % 91.70/12.79 (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v3) | ~ % 91.70/12.79 B_character_data_ptr$(v1) | ~ % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v4: % 91.70/12.79 B_character_data_ptr_option$] : ( ~ (v4 = v2) & fun_app$t(some$, v1) = v4 % 91.70/12.79 & B_character_data_ptr_option$(v4))) & ! [v0: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 91.70/12.79 B_character_data_ptr$] : ! [v2: B_character_data_ptr_option$] : ( ~ % 91.70/12.79 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v2) | ~ % 91.70/12.79 (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v0) | ~ % 91.70/12.79 B_character_data_ptr$(v1) | ~ % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | % 91.70/12.79 (fun_app$t(some$, v1) = v2 & B_character_data_ptr_option$(v2))) & ! [v0: % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 91.70/12.79 B_character_data_ptr$] : ! [v2: B_character_data_ptr_option$] : ( ~ % 91.70/12.79 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v2) | ~ % 91.70/12.79 (fun_app$t(some$, v1) = v2) | ~ B_character_data_ptr$(v1) | ~ % 91.70/12.79 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | % 91.70/12.79 cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v0) % 91.70/12.79 % 91.70/12.79 (axiom89) % 91.70/12.80 B_character_data_ptr_b_character_data_ptr_option_fun$(some$) & ! [v0: % 91.70/12.80 B_character_data_ptr$] : ! [v1: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 91.70/12.80 (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v0) = v1) | ~ % 91.70/12.80 B_character_data_ptr$(v0) | ? [v2: B_character_data_ptr_option$] : % 91.70/12.80 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2 & % 91.70/12.80 fun_app$t(some$, v0) = v2 & B_character_data_ptr_option$(v2))) & ! [v0: % 91.70/12.80 B_character_data_ptr$] : ! [v1: B_character_data_ptr_option$] : ( ~ % 91.70/12.80 (fun_app$t(some$, v0) = v1) | ~ B_character_data_ptr$(v0) | ? [v2: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : % 91.70/12.80 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v1 & % 91.70/12.80 cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v0) = v2 & % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) & % 91.70/12.80 B_character_data_ptr_option$(v1))) % 91.70/12.80 % 91.70/12.80 (axiom99) % 91.70/12.80 tlbool(tlfalse) & B_character_data_ptr_bool_fun$(uu$) & ? [v0: % 91.70/12.80 B_character_data_ptr_option_bool_fun$] : (case_option$(tlfalse, uu$) = v0 & % 91.70/12.80 B_character_data_ptr_option_bool_fun$(v0) & ! [v1: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: int] : % 91.70/12.80 (v2 = 0 | ~ (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = v2) | ~ % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? [v3: % 91.70/12.80 B_character_data_ptr_option$] : ? [v4: int] : ( ~ (v4 = 0) & % 91.70/12.80 cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v3 & % 91.70/12.80 fun_app$b(v0, v3) = v4 & B_character_data_ptr_option$(v3))) & ! [v1: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 91.70/12.80 B_character_data_ptr_option$] : ( ~ % 91.70/12.80 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2) | ~ % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? [v3: any] % 91.70/12.80 : ? [v4: any] : (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = v4 & % 91.70/12.80 fun_app$b(v0, v2) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v1: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 91.70/12.80 B_character_data_ptr_option$] : ( ~ % 91.70/12.80 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2) | ~ % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? [v3: any] % 91.70/12.80 : ? [v4: any] : (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = v3 & % 91.70/12.80 fun_app$b(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v1: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 91.70/12.80 (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = 0) | ~ % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? [v2: % 91.70/12.80 B_character_data_ptr_option$] : % 91.70/12.80 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2 & % 91.70/12.80 fun_app$b(v0, v2) = 0 & B_character_data_ptr_option$(v2)))) % 91.70/12.80 % 91.70/12.80 (conjecture85) % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(node_ptr$) & % 91.70/12.80 B_character_data_ptr_option_b_character_data_ptr_fun$(the$) & ? [v0: % 91.70/12.80 B_character_data_ptr_option$] : ? [v1: B_character_data_ptr$] : ? [v2: % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ (v2 = % 91.70/12.80 node_ptr$) & fun_app$al(the$, v0) = v1 & % 91.70/12.80 cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = v0 & % 91.70/12.80 cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v2 & % 91.70/12.80 B_character_data_ptr$(v1) & % 91.70/12.80 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) & % 91.70/12.80 B_character_data_ptr_option$(v0)) % 91.70/12.80 % 91.70/12.80 (function-axioms) % 92.00/12.87 ! [v0: Bool_set_set$] : ! [v1: Bool_set_set$] : ! [v2: Bool_set$] : ! [v3: % 92.00/12.87 Bool_set_set$] : ! [v4: Bool_bool_set_set_bool_set_set_fun_fun$] : (v1 = v0 % 92.00/12.87 | ~ (fold$f(v4, v3, v2) = v1) | ~ (fold$f(v4, v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_set_set$] : ! [v1: Nat_set_set$] : ! [v2: Nat_set$] : ! [v3: % 92.00/12.87 Nat_set_set$] : ! [v4: Nat_nat_set_set_nat_set_set_fun_fun$] : (v1 = v0 | % 92.00/12.87 ~ (fold$e(v4, v3, v2) = v1) | ~ (fold$e(v4, v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: tlbool] : ! [v3: % 92.00/12.87 tlbool] : ! [v4: Bool_bool_fun$] : (v1 = v0 | ~ (fun_upd$a(v4, v3, v2) = % 92.00/12.87 v1) | ~ (fun_upd$a(v4, v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: % 92.00/12.87 Nat_set$] : ! [v2: Nat_set$] : ! [v3: Nat_set$] : ! [v4: % 92.00/12.87 Nat_nat_set_nat_set_fun_fun$] : (v1 = v0 | ~ (fold$c(v4, v3, v2) = v1) | ~ % 92.00/12.87 (fold$c(v4, v3, v2) = v0)) & ! [v0: Bool_bool_set_fun$] : ! [v1: % 92.00/12.87 Bool_bool_set_fun$] : ! [v2: Bool_set$] : ! [v3: tlbool] : ! [v4: % 92.00/12.87 Bool_bool_set_fun$] : (v1 = v0 | ~ (fun_upd$(v4, v3, v2) = v1) | ~ % 92.00/12.87 (fun_upd$(v4, v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! % 92.00/12.87 [v2: Nat_set$] : ! [v3: Bool_set$] : ! [v4: Nat_bool_set_bool_set_fun_fun$] % 92.00/12.87 : (v1 = v0 | ~ (fold$a(v4, v3, v2) = v1) | ~ (fold$a(v4, v3, v2) = v0)) & ! % 92.00/12.87 [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: Bool_set_set$] : ! [v3: % 92.00/12.87 Bool_set$] : ! [v4: Bool_set_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fold$(v4, v3, v2) = v1) | ~ (fold$(v4, v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr$] : ! [v1: B_character_data_ptr$] : ! [v2: % 92.00/12.87 B_character_data_ptr_element_ptr$] : ! [v3: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v4: % 92.00/12.87 Nat_b_character_data_ptr_fun$] : (v1 = v0 | ~ (case_element_ptr$(v4, v3, % 92.00/12.87 v2) = v1) | ~ (case_element_ptr$(v4, v3, v2) = v0)) & ! [v0: Nat$] : % 92.00/12.87 ! [v1: Nat$] : ! [v2: Nat_option$] : ! [v3: Nat_nat_fun$] : ! [v4: Nat$] : % 92.00/12.87 (v1 = v0 | ~ (case_option$e(v4, v3, v2) = v1) | ~ (case_option$e(v4, v3, v2) % 92.00/12.87 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.87 A_element_ptr_option$] : ! [v3: A_element_ptr_bool_fun$] : ! [v4: tlbool] % 92.00/12.87 : (v1 = v0 | ~ (case_option$d(v4, v3, v2) = v1) | ~ (case_option$d(v4, v3, % 92.00/12.87 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] : ! % 92.00/12.87 [v4: tlbool] : (v1 = v0 | ~ (def_12(v4, v3, v2) = v1) | ~ (def_12(v4, v3, % 92.00/12.87 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] : ! % 92.00/12.87 [v4: tlbool] : (v1 = v0 | ~ (def_10(v4, v3, v2) = v1) | ~ (def_10(v4, v3, % 92.00/12.87 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] : ! % 92.00/12.87 [v4: tlbool] : (v1 = v0 | ~ (def_8(v4, v3, v2) = v1) | ~ (def_8(v4, v3, v2) % 92.00/12.87 = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] : ! % 92.00/12.87 [v4: tlbool] : (v1 = v0 | ~ (def_5(v4, v3, v2) = v1) | ~ (def_5(v4, v3, v2) % 92.00/12.87 = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: % 92.00/12.87 Nat_bool_fun$] : ! [v3: Nat_set$] : ! [v4: Nat_nat_fun$] : (v1 = v0 | ~ % 92.00/12.87 (uwd$(v4, v3, v2) = v1) | ~ (uwd$(v4, v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: % 92.00/12.87 Nat_set$] : ! [v4: Nat_nat_fun$] : (v1 = v0 | ~ (uwc$(v4, v3, v2) = v1) | % 92.00/12.87 ~ (uwc$(v4, v3, v2) = v0)) & ! [v0: Bool_set_set$] : ! [v1: Bool_set_set$] % 92.00/12.87 : ! [v2: Bool_set_set$] : ! [v3: Bool_set$] : (v1 = v0 | ~ (insert$e(v3, % 92.00/12.87 v2) = v1) | ~ (insert$e(v3, v2) = v0)) & ! [v0: Nat_set_set$] : ! % 92.00/12.87 [v1: Nat_set_set$] : ! [v2: Nat_set_set$] : ! [v3: Nat_set$] : (v1 = v0 | ~ % 92.00/12.87 (insert$d(v3, v2) = v1) | ~ (insert$d(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: % 92.00/12.87 Nat_bool_fun$] : (v1 = v0 | ~ (minus$b(v3, v2) = v1) | ~ (minus$b(v3, v2) % 92.00/12.87 = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_set$] : ! % 92.00/12.87 [v3: Nat_bool_fun$] : (v1 = v0 | ~ (filter$(v3, v2) = v1) | ~ (filter$(v3, % 92.00/12.87 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] : ! % 92.00/12.87 [v3: Bool_set$] : (v1 = v0 | ~ (def_46(v3, v2) = v1) | ~ (def_46(v3, v2) = % 92.00/12.87 v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: Nat_set$] : ! % 92.00/12.87 [v3: Nat_bool_fun$] : (v1 = v0 | ~ (image$m(v3, v2) = v1) | ~ (image$m(v3, % 92.00/12.87 v2) = v0)) & ! [v0: Nat_set_bool_fun$] : ! [v1: Nat_set_bool_fun$] : % 92.00/12.87 ! [v2: tlbool] : ! [v3: Nat_bool_bool_fun_fun$] : (v1 = v0 | ~ (fold$b(v3, % 92.00/12.87 v2) = v1) | ~ (fold$b(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: % 92.00/12.87 tlbool] : ! [v2: tlbool] : ! [v3: Bool_set$] : (v1 = v0 | ~ (def_45(v3, % 92.00/12.87 v2) = v1) | ~ (def_45(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: % 92.00/12.87 Nat_set$] : ! [v2: Nat_set$] : ! [v3: Nat_set$] : (v1 = v0 | ~ % 92.00/12.87 (minus$a(v3, v2) = v1) | ~ (minus$a(v3, v2) = v0)) & ! [v0: Bool_set_set$] % 92.00/12.87 : ! [v1: Bool_set_set$] : ! [v2: Nat_set$] : ! [v3: Nat_bool_set_fun$] : % 92.00/12.87 (v1 = v0 | ~ (image$l(v3, v2) = v1) | ~ (image$l(v3, v2) = v0)) & ! [v0: % 92.00/12.87 tlbool] : ! [v1: tlbool] : ! [v2: tlbool] : ! [v3: tlbool] : (v1 = v0 | % 92.00/12.87 ~ (def_41(v3, v2) = v1) | ~ (def_41(v3, v2) = v0)) & ! [v0: tlbool] : ! % 92.00/12.87 [v1: tlbool] : ! [v2: tlbool] : ! [v3: tlbool] : (v1 = v0 | ~ (def_36(v3, % 92.00/12.87 v2) = v1) | ~ (def_36(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: % 92.00/12.87 tlbool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ % 92.00/12.87 (def_37(v3, v2) = v1) | ~ (def_37(v3, v2) = v0)) & ! [v0: tlbool] : ! % 92.00/12.87 [v1: tlbool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ % 92.00/12.87 (def_38(v3, v2) = v1) | ~ (def_38(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_bool_sum_set$] : ! [v1: Bool_bool_sum_set$] : ! [v2: Bool_set$] : ! % 92.00/12.87 [v3: Bool_set$] : (v1 = v0 | ~ (plus$(v3, v2) = v1) | ~ (plus$(v3, v2) = % 92.00/12.87 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_int_fun$] : ! % 92.00/12.87 [v3: Bool_set$] : (v1 = v0 | ~ (def_34(v3, v2) = v1) | ~ (def_34(v3, v2) = % 92.00/12.87 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: tlbool] : ! [v3: % 92.00/12.87 Bool_int_fun$] : (v1 = v0 | ~ (fun_app$bo(v3, v2) = v1) | ~ % 92.00/12.87 (fun_app$bo(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 92.00/12.87 Nat_set$] : ! [v3: Nat_int_fun$] : (v1 = v0 | ~ (arg_min_on$(v3, v2) = v1) % 92.00/12.87 | ~ (arg_min_on$(v3, v2) = v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : % 92.00/12.87 ! [v2: Int_set$] : ! [v3: int] : (v1 = v0 | ~ (insert$c(v3, v2) = v1) | ~ % 92.00/12.87 (insert$c(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 tlbool] : ! [v3: tlbool] : (v1 = v0 | ~ (def_32(v3, v2) = v1) | ~ % 92.00/12.87 (def_32(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 92.00/12.87 Bool_set$] : ! [v3: Bool_nat_fun$] : (v1 = v0 | ~ (image$k(v3, v2) = v1) | % 92.00/12.87 ~ (image$k(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] % 92.00/12.87 : ! [v2: Nat_bool_fun$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ (sup$h(v3, % 92.00/12.87 v2) = v1) | ~ (sup$h(v3, v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: % 92.00/12.87 Nat_set_set$] : ! [v2: Nat_set$] : ! [v3: Nat_nat_set_fun$] : (v1 = v0 | % 92.00/12.87 ~ (image$j(v3, v2) = v1) | ~ (image$j(v3, v2) = v0)) & ! [v0: Nat_set$] : % 92.00/12.87 ! [v1: Nat_set$] : ! [v2: Nat$] : ! [v3: Nat_nat_set_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bn(v3, v2) = v1) | ~ (fun_app$bn(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_bool_sum_set$] : ! [v1: Bool_bool_sum_set$] : ! [v2: Bool_set$] : ! % 92.00/12.87 [v3: Bool_bool_bool_sum_fun$] : (v1 = v0 | ~ (image$i(v3, v2) = v1) | ~ % 92.00/12.87 (image$i(v3, v2) = v0)) & ! [v0: Bool_bool_sum_set$] : ! [v1: % 92.00/12.87 Bool_bool_sum_set$] : ! [v2: Bool_bool_sum_set$] : ! [v3: % 92.00/12.87 Bool_bool_sum_set$] : (v1 = v0 | ~ (sup$g(v3, v2) = v1) | ~ (sup$g(v3, v2) % 92.00/12.87 = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_set$] : ! % 92.00/12.87 [v3: Nat_set$] : (v1 = v0 | ~ (sup$f(v3, v2) = v1) | ~ (sup$f(v3, v2) = v0)) % 92.00/12.87 & ! [v0: Nat_option_set$] : ! [v1: Nat_option_set$] : ! [v2: Nat_set$] : ! % 92.00/12.87 [v3: Nat_nat_option_fun$] : (v1 = v0 | ~ (image$h(v3, v2) = v1) | ~ % 92.00/12.87 (image$h(v3, v2) = v0)) & ! [v0: Bool_set_set$] : ! [v1: Bool_set_set$] : % 92.00/12.87 ! [v2: Bool_set$] : ! [v3: Bool_bool_set_fun$] : (v1 = v0 | ~ (image$g(v3, % 92.00/12.87 v2) = v1) | ~ (image$g(v3, v2) = v0)) & ! [v0: Bool_option_set$] : ! % 92.00/12.87 [v1: Bool_option_set$] : ! [v2: Bool_set$] : ! [v3: Bool_bool_option_fun$] : % 92.00/12.87 (v1 = v0 | ~ (image$f(v3, v2) = v1) | ~ (image$f(v3, v2) = v0)) & ! [v0: % 92.00/12.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Bool_option_set$] % 92.00/12.87 : ! [v3: Bool_option$] : (v1 = v0 | ~ (member$g(v3, v2) = v1) | ~ % 92.00/12.87 (member$g(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: % 92.00/12.87 Bool_bool_set_fun$] : ! [v3: Bool_set$] : (v1 = v0 | ~ (bind$i(v3, v2) = % 92.00/12.87 v1) | ~ (bind$i(v3, v2) = v0)) & ! [v0: B_character_data_ptr_set$] : ! % 92.00/12.87 [v1: B_character_data_ptr_set$] : ! [v2: B_character_data_ptr_option_set$] : % 92.00/12.87 ! [v3: B_character_data_ptr_option_b_character_data_ptr_fun$] : (v1 = v0 | ~ % 92.00/12.87 (image$d(v3, v2) = v1) | ~ (image$d(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_option_set$] : ! [v1: Bool_option_set$] : ! [v2: Bool_option_set$] : % 92.00/12.87 ! [v3: Bool_option$] : (v1 = v0 | ~ (insert$b(v3, v2) = v1) | ~ % 92.00/12.87 (insert$b(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_28(v3, v2) = v1) | ~ % 92.00/12.87 (def_28(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] % 92.00/12.87 : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_26(v3, v2) = v1) | ~ % 92.00/12.87 (def_26(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 Bool_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ (def_27(v3, v2) = v1) | ~ % 92.00/12.87 (def_27(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 Bool_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ (def_25(v3, v2) = v1) | ~ % 92.00/12.87 (def_25(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] % 92.00/12.87 : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_24(v3, v2) = v1) | ~ % 92.00/12.87 (def_24(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] % 92.00/12.87 : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_23(v3, v2) = v1) | ~ % 92.00/12.87 (def_23(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] % 92.00/12.87 : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_21(v3, v2) = v1) | ~ % 92.00/12.87 (def_21(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.87 Bool_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ (def_22(v3, v2) = v1) | ~ % 92.00/12.87 (def_22(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: % 92.00/12.87 Nat$] : ! [v3: Nat_bool_set_fun$] : (v1 = v0 | ~ (fun_app$bm(v3, v2) = v1) % 92.00/12.87 | ~ (fun_app$bm(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! % 92.00/12.87 [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_20(v3, v2) = v1) | % 92.00/12.87 ~ (def_20(v3, v2) = v0)) & ! [v0: Nat_bool_set_bool_set_fun_fun$] : ! % 92.00/12.87 [v1: Nat_bool_set_bool_set_fun_fun$] : ! [v2: Nat_bool_set_bool_set_fun_fun$] % 92.00/12.87 : ! [v3: Bool_set_bool_set_fun_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (comp$r(v3, v2) = v1) | ~ (comp$r(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_set_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.87 Bool_set_bool_set_bool_set_fun_fun$] : ! [v2: % 92.00/12.87 Bool_set_bool_set_bool_set_fun_fun$] : ! [v3: % 92.00/12.87 Bool_set_bool_set_fun_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (comp$q(v3, v2) = v1) | ~ (comp$q(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_bool_set_fun$] : ! [v1: Nat_bool_set_fun$] : ! [v2: Nat_bool_set_fun$] % 92.00/12.87 : ! [v3: Bool_set_bool_set_fun$] : (v1 = v0 | ~ (comp$n(v3, v2) = v1) | ~ % 92.00/12.87 (comp$n(v3, v2) = v0)) & ! [v0: Nat_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.87 Nat_bool_set_bool_set_fun_fun$] : ! [v2: Nat_nat_fun$] : ! [v3: % 92.00/12.87 Nat_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (comp$p(v3, v2) = v1) | ~ % 92.00/12.87 (comp$p(v3, v2) = v0)) & ! [v0: Nat_bool_set_fun$] : ! [v1: % 92.00/12.87 Nat_bool_set_fun$] : ! [v2: Nat_nat_fun$] : ! [v3: Nat_bool_set_fun$] : % 92.00/12.87 (v1 = v0 | ~ (comp$m(v3, v2) = v1) | ~ (comp$m(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_set_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.87 Bool_set_bool_set_bool_set_fun_fun$] : ! [v2: Bool_set_bool_set_fun$] : ! % 92.00/12.87 [v3: Bool_set_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (comp$o(v3, v2) = % 92.00/12.87 v1) | ~ (comp$o(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.87 ~ (comp$k(v3, v2) = v1) | ~ (comp$k(v3, v2) = v0)) & ! [v0: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.87 ~ (comp$l(v3, v2) = v1) | ~ (comp$l(v3, v2) = v0)) & ! [v0: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : ! [v1: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : ! [v2: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : ! [v3: B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 % 92.00/12.87 = v0 | ~ (comp$h(v3, v2) = v1) | ~ (comp$h(v3, v2) = v0)) & ! [v0: % 92.00/12.87 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.87 ~ (comp$i(v3, v2) = v1) | ~ (comp$i(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.87 ~ (comp$j(v3, v2) = v1) | ~ (comp$j(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_nat_sum_bool_set_fun$] : ! [v1: Nat_nat_sum_bool_set_fun$] : ! [v2: % 92.00/12.87 Nat_bool_set_fun$] : ! [v3: Nat_bool_set_fun$] : (v1 = v0 | ~ % 92.00/12.87 (case_sum$c(v3, v2) = v1) | ~ (case_sum$c(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_nat_sum_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.87 Nat_nat_sum_bool_set_bool_set_fun_fun$] : ! [v2: Nat_nat_sum_bool_set_fun$] % 92.00/12.87 : ! [v3: Bool_set_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (comp$f(v3, v2) % 92.00/12.87 = v1) | ~ (comp$f(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_bool_set_bool_set_fun_fun$] : ! [v1: Nat_bool_set_bool_set_fun_fun$] : % 92.00/12.87 ! [v2: Nat_bool_set_fun$] : ! [v3: Bool_set_bool_set_bool_set_fun_fun$] : (v1 % 92.00/12.87 = v0 | ~ (comp$g(v3, v2) = v1) | ~ (comp$g(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_nat_sum_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.87 Nat_nat_sum_bool_set_bool_set_fun_fun$] : ! [v2: % 92.00/12.87 Nat_bool_set_bool_set_fun_fun$] : ! [v3: Nat_bool_set_bool_set_fun_fun$] : % 92.00/12.87 (v1 = v0 | ~ (case_sum$d(v3, v2) = v1) | ~ (case_sum$d(v3, v2) = v0)) & ! % 92.00/12.87 [v0: Bool_bool_sum_bool_fun$] : ! [v1: Bool_bool_sum_bool_fun$] : ! [v2: % 92.00/12.87 Bool_bool_sum_bool_fun$] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ % 92.00/12.87 (comp$d(v3, v2) = v1) | ~ (comp$d(v3, v2) = v0)) & ! [v0: Bool_bool_fun$] % 92.00/12.87 : ! [v1: Bool_bool_fun$] : ! [v2: Bool_bool_fun$] : ! [v3: Bool_bool_fun$] % 92.00/12.87 : (v1 = v0 | ~ (comp$e(v3, v2) = v1) | ~ (comp$e(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_bool_sum_bool_fun$] : ! [v1: Bool_bool_sum_bool_fun$] : ! [v2: % 92.00/12.87 Bool_bool_fun$] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (case_sum$b(v3, % 92.00/12.87 v2) = v1) | ~ (case_sum$b(v3, v2) = v0)) & ! [v0: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 C_b_character_data_ptr_c_sum_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.87 (comp$c(v3, v2) = v1) | ~ (comp$c(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_c_sum_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.87 (comp$b(v3, v2) = v1) | ~ (comp$b(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_c_sum_a_element_ptr_b_character_data_ptr_c_sum_sum_fun$] % 92.00/12.87 : ! [v3: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : (v1 = v0 | ~ (comp$a(v3, v2) = v1) | ~ (comp$a(v3, v2) = v0)) & ! [v0: % 92.00/12.87 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 A_element_ptr_a_element_ptr_b_character_data_ptr_c_sum_sum_fun$] : ! [v3: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : (v1 = v0 | ~ (comp$(v3, v2) = v1) | ~ (comp$(v3, v2) = v0)) & ! [v0: % 92.00/12.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.87 B_character_data_ptr_set$] : ! [v3: B_character_data_ptr$] : (v1 = v0 | ~ % 92.00/12.87 (member$f(v3, v2) = v1) | ~ (member$f(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.87 C_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.87 B_character_data_ptr_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.87 (case_sum$a(v3, v2) = v1) | ~ (case_sum$a(v3, v2) = v0)) & ! [v0: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : ! [v1: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : ! [v2: B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! % 92.00/12.87 [v3: A_element_ptr_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.87 (case_sum$(v3, v2) = v1) | ~ (case_sum$(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.87 [v2: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v3: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.87 : (v1 = v0 | ~ (case_node_ptr$(v3, v2) = v1) | ~ (case_node_ptr$(v3, v2) = % 92.00/12.87 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.87 Bool_bool_sum$] : ! [v3: Bool_bool_sum_bool_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bl(v3, v2) = v1) | ~ (fun_app$bl(v3, v2) = v0)) & ! [v0: % 92.00/12.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v3: % 92.00/12.87 A_element_ptr_b_character_data_ptr_c_sum_sum_bool_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bk(v3, v2) = v1) | ~ (fun_app$bk(v3, v2) = v0)) & ! [v0: % 92.00/12.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.87 B_character_data_ptr_c_sum$] : ! [v3: B_character_data_ptr_c_sum_bool_fun$] % 92.00/12.87 : (v1 = v0 | ~ (fun_app$bj(v3, v2) = v1) | ~ (fun_app$bj(v3, v2) = v0)) & ! % 92.00/12.87 [v0: Bool_bool_sum$] : ! [v1: Bool_bool_sum$] : ! [v2: tlbool] : ! [v3: % 92.00/12.87 Bool_bool_bool_sum_fun$] : (v1 = v0 | ~ (fun_app$bi(v3, v2) = v1) | ~ % 92.00/12.87 (fun_app$bi(v3, v2) = v0)) & ! [v0: Nat_option_bool_fun$] : ! [v1: % 92.00/12.87 Nat_option_bool_fun$] : ! [v2: Nat_option$] : ! [v3: % 92.00/12.87 Nat_option_nat_option_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$bh(v3, v2) = % 92.00/12.87 v1) | ~ (fun_app$bh(v3, v2) = v0)) & ! [v0: Bool_option_bool_fun$] : ! % 92.00/12.87 [v1: Bool_option_bool_fun$] : ! [v2: Nat_option$] : ! [v3: % 92.00/12.87 Nat_option_bool_option_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$bg(v3, v2) = % 92.00/12.87 v1) | ~ (fun_app$bg(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_option_bool_fun$] : ! [v2: Nat_option$] : ! [v3: % 92.00/12.87 Nat_option_b_character_data_ptr_option_bool_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bf(v3, v2) = v1) | ~ (fun_app$bf(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_option_bool_fun$] : ! [v1: Nat_option_bool_fun$] : ! [v2: % 92.00/12.87 Bool_option$] : ! [v3: Bool_option_nat_option_bool_fun_fun$] : (v1 = v0 | % 92.00/12.87 ~ (fun_app$be(v3, v2) = v1) | ~ (fun_app$be(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_option_bool_fun$] : ! [v1: Bool_option_bool_fun$] : ! [v2: % 92.00/12.87 Bool_option$] : ! [v3: Bool_option_bool_option_bool_fun_fun$] : (v1 = v0 | % 92.00/12.87 ~ (fun_app$bd(v3, v2) = v1) | ~ (fun_app$bd(v3, v2) = v0)) & ! [v0: % 92.00/12.87 B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.87 B_character_data_ptr_option_bool_fun$] : ! [v2: Bool_option$] : ! [v3: % 92.00/12.87 Bool_option_b_character_data_ptr_option_bool_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bc(v3, v2) = v1) | ~ (fun_app$bc(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Nat_option_bool_fun$] : ! [v1: Nat_option_bool_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_nat_option_bool_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$bb(v3, v2) = v1) | ~ (fun_app$bb(v3, v2) = v0)) & ! [v0: % 92.00/12.87 Bool_option_bool_fun$] : ! [v1: Bool_option_bool_fun$] : ! [v2: % 92.00/12.87 B_character_data_ptr_option$] : ! [v3: % 92.00/12.87 B_character_data_ptr_option_bool_option_bool_fun_fun$] : (v1 = v0 | ~ % 92.00/12.87 (fun_app$ba(v3, v2) = v1) | ~ (fun_app$ba(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_bool_fun_fun$] : (v1 % 92.00/12.88 = v0 | ~ (fun_app$az(v3, v2) = v1) | ~ (fun_app$az(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_option$] : ! [v1: Bool_option$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_bool_option_fun$] : (v1 = v0 | ~ (fun_app$ay(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$ay(v3, v2) = v0)) & ! [v0: B_character_data_ptr_option$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ (fun_app$ax(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$ax(v3, v2) = v0)) & ! [v0: Nat_option$] : ! [v1: % 92.00/12.88 Nat_option$] : ! [v2: tlbool] : ! [v3: Bool_nat_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (fun_app$aw(v3, v2) = v1) | ~ (fun_app$aw(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: tlbool] : ! [v3: Bool_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$av(v3, v2) = v1) | ~ (fun_app$av(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_option$] : ! [v1: Nat_option$] : ! [v2: B_character_data_ptr$] : ! % 92.00/12.88 [v3: B_character_data_ptr_nat_option_fun$] : (v1 = v0 | ~ (fun_app$au(v3, v2) % 92.00/12.88 = v1) | ~ (fun_app$au(v3, v2) = v0)) & ! [v0: Bool_option$] : ! [v1: % 92.00/12.88 Bool_option$] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_option_fun$] : (v1 = v0 | ~ (fun_app$at(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$at(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : % 92.00/12.88 ! [v2: B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] % 92.00/12.88 : (v1 = v0 | ~ (def_13(v3, v2) = v1) | ~ (def_13(v3, v2) = v0)) & ! [v0: % 92.00/12.88 tlbool] : ! [v1: tlbool] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_fun$] : (v1 = v0 | ~ (def_11(v3, v2) = v1) | ~ % 92.00/12.88 (def_11(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] % 92.00/12.88 : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (def_9(v3, v2) = v1) | ~ (def_9(v3, % 92.00/12.88 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : ! [v3: B_character_data_ptr_bool_fun$] : % 92.00/12.88 (v1 = v0 | ~ (def_6(v3, v2) = v1) | ~ (def_6(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_option$] : ! [v1: Bool_option$] : ! [v2: Nat_bool_option_fun$] : ! % 92.00/12.88 [v3: Nat_option$] : (v1 = v0 | ~ (bind$h(v3, v2) = v1) | ~ (bind$h(v3, v2) = % 92.00/12.88 v0)) & ! [v0: B_character_data_ptr_option$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option$] : ! [v2: % 92.00/12.88 Nat_b_character_data_ptr_option_fun$] : ! [v3: Nat_option$] : (v1 = v0 | ~ % 92.00/12.88 (bind$g(v3, v2) = v1) | ~ (bind$g(v3, v2) = v0)) & ! [v0: Nat_option$] : % 92.00/12.88 ! [v1: Nat_option$] : ! [v2: Bool_nat_option_fun$] : ! [v3: Bool_option$] : % 92.00/12.88 (v1 = v0 | ~ (bind$f(v3, v2) = v1) | ~ (bind$f(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: Bool_b_character_data_ptr_option_fun$] : ! [v3: Bool_option$] : (v1 = v0 % 92.00/12.88 | ~ (bind$e(v3, v2) = v1) | ~ (bind$e(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_option$] : ! [v1: Nat_option$] : ! [v2: % 92.00/12.88 B_character_data_ptr_nat_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (bind$d(v3, v2) = v1) | ~ % 92.00/12.88 (bind$d(v3, v2) = v0)) & ! [v0: Bool_option$] : ! [v1: Bool_option$] : ! % 92.00/12.88 [v2: B_character_data_ptr_bool_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (bind$c(v3, v2) = v1) | ~ % 92.00/12.88 (bind$c(v3, v2) = v0)) & ! [v0: Nat_option_bool_fun$] : ! [v1: % 92.00/12.88 Nat_option_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: tlbool] : (v1 = v0 % 92.00/12.88 | ~ (case_option$c(v3, v2) = v1) | ~ (case_option$c(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_option_bool_fun$] : ! [v1: Bool_option_bool_fun$] : ! [v2: % 92.00/12.88 Bool_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ (case_option$b(v3, v2) = % 92.00/12.88 v1) | ~ (case_option$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 92.00/12.88 [v1: MultipleValueBool] : ! [v2: Nat_option$] : ! [v3: Nat_option_bool_fun$] % 92.00/12.88 : (v1 = v0 | ~ (fun_app$as(v3, v2) = v1) | ~ (fun_app$as(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Nat_option$] : ! [v1: Nat_option$] : ! [v2: Nat_nat_option_fun$] : ! % 92.00/12.88 [v3: Nat_nat_option_fun_nat_option_fun$] : (v1 = v0 | ~ (fun_app$ar(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$ar(v3, v2) = v0)) & ! [v0: Bool_option$] : ! [v1: % 92.00/12.88 Bool_option$] : ! [v2: Bool_bool_option_fun$] : ! [v3: % 92.00/12.88 Bool_bool_option_fun_bool_option_fun$] : (v1 = v0 | ~ (fun_app$aq(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$aq(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun_b_character_data_ptr_option_fun$] % 92.00/12.88 : (v1 = v0 | ~ (fun_app$ap(v3, v2) = v1) | ~ (fun_app$ap(v3, v2) = v0)) & ! % 92.00/12.88 [v0: B_character_data_ptr_option_b_character_data_ptr_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr$] : (v1 = v0 | ~ (case_option$a(v3, v2) = v1) | ~ % 92.00/12.88 (case_option$a(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ % 92.00/12.88 (case_option$(v3, v2) = v1) | ~ (case_option$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_option$] : ! [v1: Nat_option$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_nat_option_fun$] : (v1 = v0 | ~ (fun_app$ao(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$ao(v3, v2) = v0)) & ! [v0: Bool_option$] : ! [v1: Bool_option$] : % 92.00/12.88 ! [v2: tlbool] : ! [v3: Bool_bool_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$an(v3, v2) = v1) | ~ (fun_app$an(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr$] : ! [v1: B_character_data_ptr$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$al(v3, v2) = v1) | ~ (fun_app$al(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Bool_option$] : ! % 92.00/12.88 [v3: Bool_option_bool_fun$] : (v1 = v0 | ~ (fun_app$am(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$am(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: A_element_ptr$] : ! [v3: % 92.00/12.88 A_element_ptr_bool_fun$] : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$ak(v3, v2) = v0)) & ! [v0: B_character_data_ptr$] : ! [v1: % 92.00/12.88 B_character_data_ptr$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_b_character_data_ptr_fun$] : (v1 = v0 | ~ (fun_app$aj(v3, v2) = v1) | % 92.00/12.88 ~ (fun_app$aj(v3, v2) = v0)) & ! [v0: Nat_nat_bool_fun_fun$] : ! [v1: % 92.00/12.88 Nat_nat_bool_fun_fun$] : ! [v2: Nat_nat_fun$] : ! [v3: Nat_set$] : (v1 = % 92.00/12.88 v0 | ~ (uwv$(v3, v2) = v1) | ~ (uwv$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_nat_bool_fun_fun$] : ! [v1: Nat_nat_bool_fun_fun$] : ! [v2: % 92.00/12.88 Nat_nat_bool_fun_fun$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (uwt$(v3, v2) = % 92.00/12.88 v1) | ~ (uwt$(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! % 92.00/12.88 [v2: Nat_set$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (image$c(v3, v2) = v1) % 92.00/12.88 | ~ (image$c(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 92.00/12.88 Nat_bool_fun$] : ! [v2: Nat_nat_bool_fun_fun$] : ! [v3: Nat_set$] : (v1 = % 92.00/12.88 v0 | ~ (uwm$(v3, v2) = v1) | ~ (uwm$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_nat_fun$] : ! [v1: Bool_nat_fun$] : ! [v2: Nat_nat_fun$] : ! [v3: % 92.00/12.88 Bool_nat_fun$] : (v1 = v0 | ~ (uww$(v3, v2) = v1) | ~ (uww$(v3, v2) = v0)) % 92.00/12.88 & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: tlbool] : ! [v3: Bool_nat_fun$] : % 92.00/12.88 (v1 = v0 | ~ (fun_app$ah(v3, v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat$] : ! [v3: Nat_nat_fun$] : (v1 = v0 % 92.00/12.88 | ~ (fun_app$ai(v3, v2) = v1) | ~ (fun_app$ai(v3, v2) = v0)) & ! [v0: % 92.00/12.88 tlbool] : ! [v1: tlbool] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_fun$] : (v1 = v0 | ~ (def_3(v3, v2) = v1) | ~ % 92.00/12.88 (def_3(v3, v2) = v0)) & ! [v0: B_character_data_ptr_bool_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_bool_fun$] : ! [v2: B_character_data_ptr_bool_fun$] : % 92.00/12.88 ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (uuf$(v3, v2) = v1) | ~ (uuf$(v3, v2) % 92.00/12.88 = v0)) & ! [v0: B_character_data_ptr_b_character_data_ptr_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_bool_fun$] : ! [v3: Bool_b_character_data_ptr_fun$] : % 92.00/12.88 (v1 = v0 | ~ (uug$(v3, v2) = v1) | ~ (uug$(v3, v2) = v0)) & ! [v0: tlbool] % 92.00/12.88 : ! [v1: tlbool] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_fun$] : (v1 = v0 | ~ (def_2(v3, v2) = v1) | ~ % 92.00/12.88 (def_2(v3, v2) = v0)) & ! [v0: B_character_data_ptr$] : ! [v1: % 92.00/12.88 B_character_data_ptr$] : ! [v2: tlbool] : ! [v3: % 92.00/12.88 Bool_b_character_data_ptr_fun$] : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) | % 92.00/12.88 ~ (fun_app$ag(v3, v2) = v0)) & ! [v0: C_b_character_data_ptr_option_fun$] : % 92.00/12.88 ! [v1: C_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 C_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (uvd$(v3, v2) = v1) | ~ (uvd$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : ! [v3: B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 % 92.00/12.88 = v0 | ~ (uve$(v3, v2) = v1) | ~ (uve$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (uvb$(v3, v2) = v1) | ~ (uvb$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (uva$(v3, v2) = v1) | ~ (uva$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (uvc$(v3, v2) = v1) | ~ (uvc$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: B_character_data_ptr_option$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_b_character_data_ptr_option_fun$] : (v1 = v0 | % 92.00/12.88 ~ (fun_app$af(v3, v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_bool_fun$] : ! [v1: B_character_data_ptr_bool_fun$] : % 92.00/12.88 ! [v2: B_character_data_ptr_b_character_data_ptr_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_fun$] : (v1 = v0 | ~ (uuh$(v3, v2) = v1) | ~ % 92.00/12.88 (uuh$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_bool_fun$] : (v1 = v0 | ~ (fun_app$ae(v3, v2) = v1) | % 92.00/12.88 ~ (fun_app$ae(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : ! [v3: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : (v1 = v0 | ~ (uui$(v3, % 92.00/12.88 v2) = v1) | ~ (uui$(v3, v2) = v0)) & ! [v0: B_character_data_ptr$] : % 92.00/12.88 ! [v1: B_character_data_ptr$] : ! [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$ad(v3, v2) = v1) | ~ (fun_app$ad(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_bool_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ac(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$ac(v3, v2) = v0)) & ! [v0: Bool_bool_set_fun$] : ! [v1: % 92.00/12.88 Bool_bool_set_fun$] : ! [v2: Bool_bool_set_fun$] : ! [v3: tlbool] : (v1 = % 92.00/12.88 v0 | ~ (uwh$(v3, v2) = v1) | ~ (uwh$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_set_fun$] : ! [v1: Bool_bool_set_fun$] : ! [v2: % 92.00/12.88 Bool_bool_set_fun$] : ! [v3: Bool_set$] : (v1 = v0 | ~ (uwk$(v3, v2) = v1) % 92.00/12.88 | ~ (uwk$(v3, v2) = v0)) & ! [v0: Bool_bool_set_fun$] : ! [v1: % 92.00/12.88 Bool_bool_set_fun$] : ! [v2: Bool_bool_set_fun$] : ! [v3: Bool_set$] : (v1 % 92.00/12.88 = v0 | ~ (uxd$(v3, v2) = v1) | ~ (uxd$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: % 92.00/12.88 Nat$] : (v1 = v0 | ~ (uvt$(v3, v2) = v1) | ~ (uvt$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Bool_bool_fun$] : ! % 92.00/12.88 [v3: tlbool] : (v1 = v0 | ~ (uvs$(v3, v2) = v1) | ~ (uvs$(v3, v2) = v0)) & % 92.00/12.88 ! [v0: Bool_bool_set_fun$] : ! [v1: Bool_bool_set_fun$] : ! [v2: Bool_set$] % 92.00/12.88 : ! [v3: Bool_bool_set_fun$] : (v1 = v0 | ~ (uwj$(v3, v2) = v1) | ~ % 92.00/12.88 (uwj$(v3, v2) = v0)) & ! [v0: Bool_set_bool_set_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_set_fun$] : ! [v2: Bool_set$] : ! [v3: % 92.00/12.88 Bool_set_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 92.00/12.88 Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: Nat_bool_fun$] : (v1 = v0 % 92.00/12.88 | ~ (uwo$(v3, v2) = v1) | ~ (uwo$(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] % 92.00/12.88 : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: Nat_bool_fun$] : % 92.00/12.88 (v1 = v0 | ~ (uwp$(v3, v2) = v1) | ~ (uwp$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : ! [v3: % 92.00/12.88 Nat_set$] : (v1 = v0 | ~ (uwy$(v3, v2) = v1) | ~ (uwy$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! % 92.00/12.88 [v3: Nat$] : (v1 = v0 | ~ (uvw$(v3, v2) = v1) | ~ (uvw$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Bool_bool_fun$] : ! % 92.00/12.88 [v3: tlbool] : (v1 = v0 | ~ (uvx$(v3, v2) = v1) | ~ (uvx$(v3, v2) = v0)) & % 92.00/12.88 ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! % 92.00/12.88 [v3: Nat$] : (v1 = v0 | ~ (uvy$(v3, v2) = v1) | ~ (uvy$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Bool_bool_fun$] : ! % 92.00/12.88 [v3: tlbool] : (v1 = v0 | ~ (uvz$(v3, v2) = v1) | ~ (uvz$(v3, v2) = v0)) & % 92.00/12.88 ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : ! [v3: % 92.00/12.88 Nat_bool_fun$] : (v1 = v0 | ~ (uxc$(v3, v2) = v1) | ~ (uxc$(v3, v2) = v0)) % 92.00/12.88 & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : ! % 92.00/12.88 [v3: Nat$] : (v1 = v0 | ~ (uvv$(v3, v2) = v1) | ~ (uvv$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: Bool_set$] : ! [v3: % 92.00/12.88 tlbool] : (v1 = v0 | ~ (uvu$(v3, v2) = v1) | ~ (uvu$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : ! [v3: % 92.00/12.88 Nat_set$] : (v1 = v0 | ~ (uws$(v3, v2) = v1) | ~ (uws$(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Nat_set_nat_set_fun$] : ! [v1: Nat_set_nat_set_fun$] : ! [v2: Nat$] : % 92.00/12.88 ! [v3: Nat_nat_set_nat_set_fun_fun$] : (v1 = v0 | ~ (fun_app$aa(v3, v2) = v1) % 92.00/12.88 | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! % 92.00/12.88 [v2: Nat_set$] : ! [v3: Nat_set_nat_set_fun$] : (v1 = v0 | ~ (fun_app$z(v3, % 92.00/12.88 v2) = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_bool_set_fun$] : ! [v1: Bool_set_bool_set_fun$] : ! [v2: tlbool] % 92.00/12.88 : ! [v3: Bool_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (fun_app$y(v3, v2) % 92.00/12.88 = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! [v0: Bool_set_bool_set_fun$] : % 92.00/12.88 ! [v1: Bool_set_bool_set_fun$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (fun_app$x(v3, v2) = v1) | % 92.00/12.88 ~ (fun_app$x(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.88 Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ (def_1(v3, v2) = v1) | ~ % 92.00/12.88 (def_1(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: % 92.00/12.88 Nat_set_set$] : ! [v3: Nat_set_bool_fun$] : (v1 = v0 | ~ (image$b(v3, v2) % 92.00/12.88 = v1) | ~ (image$b(v3, v2) = v0)) & ! [v0: B_character_data_ptr_option$] % 92.00/12.88 : ! [v1: B_character_data_ptr_option$] : ! [v2: A_element_ptr$] : ! [v3: % 92.00/12.88 A_element_ptr_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$v(v3, v2) = v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v2: A_element_ptr$] : % 92.00/12.88 ! [v3: A_element_ptr_a_element_ptr_b_character_data_ptr_c_sum_sum_fun$] : (v1 % 92.00/12.88 = v0 | ~ (fun_app$w(v3, v2) = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_c_sum$] : ! [v1: B_character_data_ptr_c_sum$] : ! % 92.00/12.88 [v2: B_character_data_ptr$] : ! [v3: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_c_sum_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$u(v3, v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v2: % 92.00/12.88 B_character_data_ptr_c_sum$] : ! [v3: % 92.00/12.88 B_character_data_ptr_c_sum_a_element_ptr_b_character_data_ptr_c_sum_sum_fun$] % 92.00/12.88 : (v1 = v0 | ~ (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! % 92.00/12.88 [v0: B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : % 92.00/12.88 ! [v2: A_element_ptr_b_character_data_ptr_c_sum_sum$] : ! [v3: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : (v1 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! % 92.00/12.88 [v0: B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : % 92.00/12.88 ! [v2: C$] : ! [v3: C_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$o(v3, v2) = v1) | ~ (fun_app$o(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_c_sum$] : ! [v1: B_character_data_ptr_c_sum$] : ! % 92.00/12.88 [v2: C$] : ! [v3: C_b_character_data_ptr_c_sum_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$q(v3, v2) = v1) | ~ (fun_app$q(v3, v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: B_character_data_ptr_c_sum$] : ! [v3: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Int_set$] : ! % 92.00/12.88 [v3: Int_set_bool_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$n(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: int] : ! [v3: Int_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set_set$] : ! % 92.00/12.88 [v3: Nat_set$] : (v1 = v0 | ~ (member$c(v3, v2) = v1) | ~ (member$c(v3, v2) % 92.00/12.88 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.88 Nat_set$] : ! [v3: Nat_set_bool_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: Bool_set_set$] : ! [v3: Bool_set$] : (v1 = v0 % 92.00/12.88 | ~ (member$b(v3, v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Bool_set$] : ! % 92.00/12.88 [v3: Bool_set_bool_fun$] : (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$k(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | % 92.00/12.88 ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_set_set_nat_set_set_fun$] : ! [v1: Nat_set_set_nat_set_set_fun$] : ! % 92.00/12.88 [v2: Nat$] : ! [v3: Nat_nat_set_set_nat_set_set_fun_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Nat_set_set$] : ! [v1: Nat_set_set$] : ! [v2: Nat_set_set$] : ! [v3: % 92.00/12.88 Nat_set_set_nat_set_set_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$h(v3, v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: Nat_set_set$] : % 92.00/12.88 ! [v2: Nat_set_set$] : ! [v3: Nat_set_nat_set_fun$] : (v1 = v0 | ~ % 92.00/12.88 (image$a(v3, v2) = v1) | ~ (image$a(v3, v2) = v0)) & ! [v0: Nat_set_set$] % 92.00/12.88 : ! [v1: Nat_set_set$] : ! [v2: Nat_set_set$] : ! [v3: Nat_set_set$] : (v1 % 92.00/12.88 = v0 | ~ (sup$a(v3, v2) = v1) | ~ (sup$a(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_set_bool_set_set_fun$] : ! [v1: Bool_set_set_bool_set_set_fun$] : % 92.00/12.88 ! [v2: tlbool] : ! [v3: Bool_bool_set_set_bool_set_set_fun_fun$] : (v1 = v0 | % 92.00/12.88 ~ (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_set$] : ! [v1: Bool_set_set$] : ! [v2: Bool_set_set$] : ! [v3: % 92.00/12.88 Bool_set_set_bool_set_set_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | % 92.00/12.88 ~ (fun_app$f(v3, v2) = v0)) & ! [v0: Bool_set_set$] : ! [v1: % 92.00/12.88 Bool_set_set$] : ! [v2: Bool_set_set$] : ! [v3: Bool_set_bool_set_fun$] : % 92.00/12.88 (v1 = v0 | ~ (image$(v3, v2) = v1) | ~ (image$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_set$] : ! [v1: Bool_set_set$] : ! [v2: Bool_set_set$] : ! [v3: % 92.00/12.88 Bool_set_set$] : (v1 = v0 | ~ (sup$(v3, v2) = v1) | ~ (sup$(v3, v2) = v0)) % 92.00/12.88 & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : ! [v3: % 92.00/12.88 Nat_nat_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 92.00/12.88 (fun_app$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: int] : ! % 92.00/12.88 [v1: int] : ! [v2: Nat$] : ! [v3: Nat_int_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.88 B_character_data_ptr_option_set$] : ! [v3: B_character_data_ptr_option$] : % 92.00/12.88 (v1 = v0 | ~ (member$(v3, v2) = v1) | ~ (member$(v3, v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : ! [v3: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = % 92.00/12.88 v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: % 92.00/12.88 Bool_set$] : ! [v2: tlbool] : ! [v3: Bool_bool_set_fun$] : (v1 = v0 | ~ % 92.00/12.88 (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: Bool_set$] : % 92.00/12.88 ! [v1: Bool_set$] : ! [v2: Bool_set$] : ! [v3: Bool_set_bool_set_fun$] : % 92.00/12.88 (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! % 92.00/12.88 [v0: Bool_set_bool_fun$] : ! [v1: Bool_set_bool_fun$] : ! [v2: % 92.00/12.88 Bool_int_fun$] : (v1 = v0 | ~ (arg_min_on$a(v2) = v1) | ~ % 92.00/12.88 (arg_min_on$a(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : % 92.00/12.88 (v1 = v0 | ~ (nat$(v2) = v1) | ~ (nat$(v2) = v0)) & ! [v0: Bool_set_set$] : % 92.00/12.88 ! [v1: Bool_set_set$] : ! [v2: Bool_set$] : (v1 = v0 | ~ (pow$a(v2) = v1) | % 92.00/12.88 ~ (pow$a(v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: Nat_set_set$] : ! % 92.00/12.88 [v2: Nat_set$] : (v1 = v0 | ~ (pow$(v2) = v1) | ~ (pow$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set$] : ! [v1: Bool_set$] : ! [v2: Bool_set_set$] : (v1 = v0 | ~ % 92.00/12.88 (inf$(v2) = v1) | ~ (inf$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_set_bool_set_fun_fun$] : ! [v2: % 92.00/12.88 Bool_bool_set_bool_set_fun_fun$] : (v1 = v0 | ~ (fold$d(v2) = v1) | ~ % 92.00/12.88 (fold$d(v2) = v0)) & ! [v0: Bool_set_bool_set_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_set_fun$] : ! [v2: Bool_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (filter$a(v2) = v1) | ~ (filter$a(v2) = v0)) & ! [v0: Nat_set_bool_fun$] : % 92.00/12.88 ! [v1: Nat_set_bool_fun$] : ! [v2: Nat_set$] : (v1 = v0 | ~ (less$c(v2) = % 92.00/12.88 v1) | ~ (less$c(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: Bool_set_set$] : (v1 = v0 | ~ (finite$e(v2) = % 92.00/12.88 v1) | ~ (finite$e(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! % 92.00/12.88 [v2: Bool_set$] : (v1 = v0 | ~ (def_43(v2) = v1) | ~ (def_43(v2) = v0)) & ! % 92.00/12.88 [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_set$] : (v1 = v0 | ~ % 92.00/12.88 (def_44(v2) = v1) | ~ (def_44(v2) = v0)) & ! [v0: tlbool] : ! [v1: % 92.00/12.88 tlbool] : ! [v2: Bool_set$] : (v1 = v0 | ~ (def_42(v2) = v1) | ~ % 92.00/12.88 (def_42(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_set$] % 92.00/12.88 : (v1 = v0 | ~ (def_40(v2) = v1) | ~ (def_40(v2) = v0)) & ! [v0: tlbool] : % 92.00/12.88 ! [v1: tlbool] : ! [v2: Bool_set$] : (v1 = v0 | ~ (def_39(v2) = v1) | ~ % 92.00/12.88 (def_39(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! % 92.00/12.88 [v2: tlbool] : (v1 = v0 | ~ (sup$i(v2) = v1) | ~ (sup$i(v2) = v0)) & ! [v0: % 92.00/12.88 tlbool] : ! [v1: tlbool] : ! [v2: Bool_set$] : (v1 = v0 | ~ (def_35(v2) = % 92.00/12.88 v1) | ~ (def_35(v2) = v0)) & ! [v0: Nat_nat_fun$] : ! [v1: % 92.00/12.88 Nat_nat_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ (sup$j(v2) = v1) | ~ % 92.00/12.88 (sup$j(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_set$] : (v1 % 92.00/12.88 = v0 | ~ (sup_fin$(v2) = v1) | ~ (sup_fin$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ % 92.00/12.88 (less$b(v2) = v1) | ~ (less$b(v2) = v0)) & ! [v0: tlbool] : ! [v1: % 92.00/12.88 tlbool] : ! [v2: Bool_set$] : (v1 = v0 | ~ (def_33(v2) = v1) | ~ % 92.00/12.88 (def_33(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 92.00/12.88 : ! [v2: Bool_option_set$] : (v1 = v0 | ~ (finite$b(v2) = v1) | ~ % 92.00/12.88 (finite$b(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: Nat_option_set$] : (v1 = v0 | ~ (finite$(v2) = % 92.00/12.88 v1) | ~ (finite$(v2) = v0)) & ! [v0: Bool_set_bool_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_fun$] : ! [v2: Bool_set$] : (v1 = v0 | ~ (less$(v2) = v1) | % 92.00/12.88 ~ (less$(v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 92.00/12.88 Nat_set_set$] : (v1 = v0 | ~ (sup$e(v2) = v1) | ~ (sup$e(v2) = v0)) & ! % 92.00/12.88 [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: Bool_set_set$] : (v1 = v0 | ~ % 92.00/12.88 (sup$d(v2) = v1) | ~ (sup$d(v2) = v0)) & ! [v0: Bool_set_bool_set_fun$] : % 92.00/12.88 ! [v1: Bool_set_bool_set_fun$] : ! [v2: Bool_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (image$e(v2) = v1) | ~ (image$e(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_set$] : ! [v1: B_character_data_ptr_set$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option_set$] : (v1 = v0 | ~ (these$a(v2) = v1) | ~ % 92.00/12.88 (these$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 92.00/12.88 MultipleValueBool] : ! [v2: Bool_bool_fun$] : (v1 = v0 | ~ (the$g(v2) = % 92.00/12.88 v1) | ~ (the$g(v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! % 92.00/12.88 [v2: Bool_node_ptr$] : (v1 = v0 | ~ (set_node_ptr$(v2) = v1) | ~ % 92.00/12.88 (set_node_ptr$(v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! % 92.00/12.88 [v2: Bool_option_set$] : (v1 = v0 | ~ (these$(v2) = v1) | ~ (these$(v2) = % 92.00/12.88 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_set$] : (v1 = v0 | % 92.00/12.88 ~ (def_31(v2) = v1) | ~ (def_31(v2) = v0)) & ! [v0: Bool_set$] : ! [v1: % 92.00/12.88 Bool_set$] : ! [v2: Bool_bool_sum$] : (v1 = v0 | ~ (setr$(v2) = v1) | ~ % 92.00/12.88 (setr$(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.88 Bool_bool_sum$] : (v1 = v0 | ~ (def_30(v2) = v1) | ~ (def_30(v2) = v0)) & % 92.00/12.88 ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_bool_sum$] : (v1 = v0 | ~ % 92.00/12.88 (def_29(v2) = v1) | ~ (def_29(v2) = v0)) & ! [v0: B_character_data_ptr$] : % 92.00/12.88 ! [v1: B_character_data_ptr$] : ! [v2: B_character_data_ptr_element_ptr$] : % 92.00/12.88 (v1 = v0 | ~ (un_Ext$(v2) = v1) | ~ (un_Ext$(v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set_set$] : % 92.00/12.88 (v1 = v0 | ~ (is_empty$(v2) = v1) | ~ (is_empty$(v2) = v0)) & ! [v0: % 92.00/12.88 tlbool] : ! [v1: tlbool] : ! [v2: Bool_bool_sum$] : (v1 = v0 | ~ % 92.00/12.88 (def_19(v2) = v1) | ~ (def_19(v2) = v0)) & ! [v0: tlbool] : ! [v1: % 92.00/12.88 tlbool] : ! [v2: Bool_bool_sum$] : (v1 = v0 | ~ (def_18(v2) = v1) | ~ % 92.00/12.88 (def_18(v2) = v0)) & ! [v0: B_character_data_ptr_c_sum$] : ! [v1: % 92.00/12.88 B_character_data_ptr_c_sum$] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : (v1 = v0 | ~ (projr$a(v2) % 92.00/12.88 = v1) | ~ (projr$a(v2) = v0)) & ! [v0: A_element_ptr$] : ! [v1: % 92.00/12.88 A_element_ptr$] : ! [v2: A_element_ptr_b_character_data_ptr_c_sum_sum$] : % 92.00/12.88 (v1 = v0 | ~ (projl$a(v2) = v1) | ~ (projl$a(v2) = v0)) & ! [v0: C$] : ! % 92.00/12.88 [v1: C$] : ! [v2: B_character_data_ptr_c_sum$] : (v1 = v0 | ~ (projr$(v2) = % 92.00/12.88 v1) | ~ (projr$(v2) = v0)) & ! [v0: B_character_data_ptr$] : ! [v1: % 92.00/12.88 B_character_data_ptr$] : ! [v2: B_character_data_ptr_c_sum$] : (v1 = v0 | % 92.00/12.88 ~ (projl$(v2) = v1) | ~ (projl$(v2) = v0)) & ! [v0: Int_option$] : ! [v1: % 92.00/12.88 Int_option$] : ! [v2: int] : (v1 = v0 | ~ (some$f(v2) = v1) | ~ % 92.00/12.88 (some$f(v2) = v0)) & ! [v0: Nat_set_option$] : ! [v1: Nat_set_option$] : % 92.00/12.88 ! [v2: Nat_set$] : (v1 = v0 | ~ (some$e(v2) = v1) | ~ (some$e(v2) = v0)) & % 92.00/12.88 ! [v0: Bool_set_option$] : ! [v1: Bool_set_option$] : ! [v2: Bool_set$] : % 92.00/12.88 (v1 = v0 | ~ (some$d(v2) = v1) | ~ (some$d(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_set$] : ! [v1: B_character_data_ptr_set$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (set_option$e(v2) = v1) | ~ % 92.00/12.88 (set_option$e(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.88 Bool_option$] : (v1 = v0 | ~ (def_17(v2) = v1) | ~ (def_17(v2) = v0)) & ! % 92.00/12.88 [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: Bool_option$] : (v1 = v0 | ~ % 92.00/12.88 (set_option$d(v2) = v1) | ~ (set_option$d(v2) = v0)) & ! [v0: Nat_set$] : % 92.00/12.88 ! [v1: Nat_set$] : ! [v2: Nat_option$] : (v1 = v0 | ~ (set_option$c(v2) = % 92.00/12.88 v1) | ~ (set_option$c(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 92.00/12.88 Int_option$] : (v1 = v0 | ~ (the$f(v2) = v1) | ~ (the$f(v2) = v0)) & ! % 92.00/12.88 [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: Int_option$] : (v1 = v0 | ~ % 92.00/12.88 (set_option$b(v2) = v1) | ~ (set_option$b(v2) = v0)) & ! [v0: Nat_set$] : % 92.00/12.88 ! [v1: Nat_set$] : ! [v2: Nat_set_option$] : (v1 = v0 | ~ (the$e(v2) = v1) | % 92.00/12.88 ~ (the$e(v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: Nat_set_set$] : ! % 92.00/12.88 [v2: Nat_set_option$] : (v1 = v0 | ~ (set_option$a(v2) = v1) | ~ % 92.00/12.88 (set_option$a(v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: % 92.00/12.88 Bool_set_option$] : (v1 = v0 | ~ (the$d(v2) = v1) | ~ (the$d(v2) = v0)) & % 92.00/12.88 ! [v0: Bool_set_set$] : ! [v1: Bool_set_set$] : ! [v2: Bool_set_option$] : % 92.00/12.88 (v1 = v0 | ~ (set_option$(v2) = v1) | ~ (set_option$(v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_option$] : ! [v1: A_element_ptr_option$] : ! [v2: % 92.00/12.88 A_element_ptr$] : (v1 = v0 | ~ (some$c(v2) = v1) | ~ (some$c(v2) = v0)) & % 92.00/12.88 ! [v0: A_element_ptr$] : ! [v1: A_element_ptr$] : ! [v2: % 92.00/12.88 A_element_ptr_option$] : (v1 = v0 | ~ (the$c(v2) = v1) | ~ (the$c(v2) = % 92.00/12.88 v0)) & ! [v0: A_element_ptr_option$] : ! [v1: A_element_ptr_option$] : % 92.00/12.88 ! [v2: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (cast_n_o_d_e_p_t_r_2_e_l_e_m_e_n_t_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (cast_n_o_d_e_p_t_r_2_e_l_e_m_e_n_t_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_node_ptr$] : ! [v1: Bool_node_ptr$] : ! [v2: tlbool] : (v1 = v0 | ~ % 92.00/12.88 (ext$a(v2) = v1) | ~ (ext$a(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] % 92.00/12.88 : ! [v2: Bool_option$] : (v1 = v0 | ~ (def_16(v2) = v1) | ~ (def_16(v2) = % 92.00/12.88 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Bool_option$] : (v1 = % 92.00/12.88 v0 | ~ (def_15(v2) = v1) | ~ (def_15(v2) = v0)) & ! [v0: tlbool] : ! % 92.00/12.88 [v1: tlbool] : ! [v2: Bool_option$] : (v1 = v0 | ~ (def_14(v2) = v1) | ~ % 92.00/12.88 (def_14(v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 92.00/12.88 Nat_bool_fun$] : (v1 = v0 | ~ (collect$e(v2) = v1) | ~ (collect$e(v2) = % 92.00/12.88 v0)) & ! [v0: B_character_data_ptr_option_set$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_set$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : (v1 = v0 | ~ (collect$d(v2) = v1) % 92.00/12.88 | ~ (collect$d(v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! % 92.00/12.88 [v2: Bool_bool_fun$] : (v1 = v0 | ~ (collect$c(v2) = v1) | ~ (collect$c(v2) % 92.00/12.88 = v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: Int_bool_fun$] : % 92.00/12.88 (v1 = v0 | ~ (collect$b(v2) = v1) | ~ (collect$b(v2) = v0)) & ! [v0: % 92.00/12.88 Nat_set_set$] : ! [v1: Nat_set_set$] : ! [v2: Nat_set_bool_fun$] : (v1 = % 92.00/12.88 v0 | ~ (collect$a(v2) = v1) | ~ (collect$a(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_set$] : ! [v1: Bool_set_set$] : ! [v2: Bool_set_bool_fun$] : (v1 % 92.00/12.88 = v0 | ~ (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & ! [v0: tlbool] : % 92.00/12.88 ! [v1: tlbool] : ! [v2: Bool_option$] : (v1 = v0 | ~ (def_7(v2) = v1) | ~ % 92.00/12.88 (def_7(v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 92.00/12.88 Bool_option$] : (v1 = v0 | ~ (def_4(v2) = v1) | ~ (def_4(v2) = v0)) & ! % 92.00/12.88 [v0: Nat_nat_option_fun_nat_option_fun$] : ! [v1: % 92.00/12.88 Nat_nat_option_fun_nat_option_fun$] : ! [v2: Nat_option$] : (v1 = v0 | ~ % 92.00/12.88 (bind$b(v2) = v1) | ~ (bind$b(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_option_fun_bool_option_fun$] : ! [v1: % 92.00/12.88 Bool_bool_option_fun_bool_option_fun$] : ! [v2: Bool_option$] : (v1 = v0 | % 92.00/12.88 ~ (bind$a(v2) = v1) | ~ (bind$a(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun_b_character_data_ptr_option_fun$] % 92.00/12.88 : ! [v1: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun_b_character_data_ptr_option_fun$] % 92.00/12.88 : ! [v2: B_character_data_ptr_option$] : (v1 = v0 | ~ (bind$(v2) = v1) | ~ % 92.00/12.88 (bind$(v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum$] : (v1 = v0 | ~ (ext$(v2) = % 92.00/12.88 v1) | ~ (ext$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 92.00/12.88 Nat_option$] : (v1 = v0 | ~ (the$b(v2) = v1) | ~ (the$b(v2) = v0)) & ! % 92.00/12.88 [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 92.00/12.88 A_element_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (cast_e_l_e_m_e_n_t_p_t_r_2_n_o_d_e_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (cast_e_l_e_m_e_n_t_p_t_r_2_n_o_d_e_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (is_element_ptr_kind_n_o_d_e_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (is_element_ptr_kind_n_o_d_e_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option$] : ! [v1: B_character_data_ptr_option$] : ! % 92.00/12.88 [v2: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 92.00/12.88 B_character_data_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v1 = v0 | ~ % 92.00/12.88 (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v2) = v1) | ~ % 92.00/12.88 (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_set_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_set_bool_set_fun_fun$] : ! [v2: Bool_set_bool_set_fun$] : (v1 % 92.00/12.88 = v0 | ~ (uvm$(v2) = v1) | ~ (uvm$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_set_fun$] : ! [v1: Bool_bool_set_fun$] : ! [v2: Bool_set$] : (v1 % 92.00/12.88 = v0 | ~ (uwe$(v2) = v1) | ~ (uwe$(v2) = v0)) & ! [v0: Nat_bool_fun$] : % 92.00/12.88 ! [v1: Nat_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (uwf$(v2) = v1) | ~ % 92.00/12.88 (uwf$(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! % 92.00/12.88 [v2: tlbool] : (v1 = v0 | ~ (uvl$(v2) = v1) | ~ (uvl$(v2) = v0)) & ! [v0: % 92.00/12.88 C_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 C_b_character_data_ptr_option_fun$] : ! [v2: B_character_data_ptr_option$] % 92.00/12.88 : (v1 = v0 | ~ (uuz$(v2) = v1) | ~ (uuz$(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (uux$(v2) = v1) | ~ (uux$(v2) % 92.00/12.88 = v0)) & ! [v0: A_element_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 A_element_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (uuw$(v2) = v1) | ~ (uuw$(v2) % 92.00/12.88 = v0)) & ! [v0: B_character_data_ptr_b_character_data_ptr_option_fun$] : % 92.00/12.88 ! [v1: B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option$] : (v1 = v0 | ~ (uuy$(v2) = v1) | ~ (uuy$(v2) % 92.00/12.88 = v0)) & ! [v0: Nat_bool_bool_fun_fun$] : ! [v1: Nat_bool_bool_fun_fun$] % 92.00/12.88 : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (uwx$(v2) = v1) | ~ (uwx$(v2) = v0)) % 92.00/12.88 & ! [v0: Nat_nat_bool_fun_fun$] : ! [v1: Nat_nat_bool_fun_fun$] : ! [v2: % 92.00/12.88 Nat_nat_bool_fun_fun$] : (v1 = v0 | ~ (uwn$(v2) = v1) | ~ (uwn$(v2) = v0)) % 92.00/12.88 & ! [v0: Nat_nat_set_nat_set_fun_fun$] : ! [v1: % 92.00/12.88 Nat_nat_set_nat_set_fun_fun$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (uxa$(v2) = v1) | ~ (uxa$(v2) = v0)) & ! [v0: % 92.00/12.88 Bool_bool_set_bool_set_fun_fun$] : ! [v1: Bool_bool_set_bool_set_fun_fun$] % 92.00/12.88 : ! [v2: Bool_bool_fun$] : (v1 = v0 | ~ (uxb$(v2) = v1) | ~ (uxb$(v2) = % 92.00/12.88 v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: % 92.00/12.88 Nat_set_set$] : (v1 = v0 | ~ (uwl$(v2) = v1) | ~ (uwl$(v2) = v0)) & ! % 92.00/12.88 [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : (v1 = % 92.00/12.88 v0 | ~ (uwq$(v2) = v1) | ~ (uwq$(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! % 92.00/12.88 [v1: Bool_bool_fun$] : ! [v2: Bool_bool_fun$] : (v1 = v0 | ~ (uwr$(v2) = v1) % 92.00/12.88 | ~ (uwr$(v2) = v0)) & ! [v0: Nat_bool_set_bool_set_fun_fun$] : ! [v1: % 92.00/12.88 Nat_bool_set_bool_set_fun_fun$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ % 92.00/12.88 (uwz$(v2) = v1) | ~ (uwz$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 92.00/12.88 Nat_bool_fun$] : ! [v2: Nat_set_set$] : (v1 = v0 | ~ (uwi$(v2) = v1) | ~ % 92.00/12.88 (uwi$(v2) = v0)) & ! [v0: A_element_ptr_b_character_data_ptr_option_fun$] : % 92.00/12.88 ! [v1: A_element_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : (v1 = v0 | ~ (uus$(v2) = v1) | ~ (uus$(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (uuu$(v2) = v1) | ~ (uuu$(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.88 : (v1 = v0 | ~ (uut$(v2) = v1) | ~ (uut$(v2) = v0)) & ! [v0: % 92.00/12.88 C_b_character_data_ptr_option_fun$] : ! [v1: % 92.00/12.88 C_b_character_data_ptr_option_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : (v1 = v0 | ~ % 92.00/12.88 (uuv$(v2) = v1) | ~ (uuv$(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: % 92.00/12.88 Bool_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (uvp$(v2) = v1) | ~ % 92.00/12.88 (uvp$(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! % 92.00/12.88 [v2: tlbool] : (v1 = v0 | ~ (uvr$(v2) = v1) | ~ (uvr$(v2) = v0)) & ! [v0: % 92.00/12.88 Int_set_bool_fun$] : ! [v1: Int_set_bool_fun$] : ! [v2: int] : (v1 = v0 | % 92.00/12.88 ~ (member$e(v2) = v1) | ~ (member$e(v2) = v0)) & ! [v0: Int_bool_fun$] : % 92.00/12.88 ! [v1: Int_bool_fun$] : ! [v2: Int_set$] : (v1 = v0 | ~ (uul$(v2) = v1) | ~ % 92.00/12.88 (uul$(v2) = v0)) & ! [v0: Nat_set_bool_fun$] : ! [v1: Nat_set_bool_fun$] : % 92.00/12.88 ! [v2: Nat$] : (v1 = v0 | ~ (member$d(v2) = v1) | ~ (member$d(v2) = v0)) & % 92.00/12.88 ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : (v1 = v0 % 92.00/12.88 | ~ (uuo$(v2) = v1) | ~ (uuo$(v2) = v0)) & ! [v0: Nat_set_bool_fun$] : ! % 92.00/12.88 [v1: Nat_set_bool_fun$] : ! [v2: Nat_set_set$] : (v1 = v0 | ~ (uuk$(v2) = % 92.00/12.88 v1) | ~ (uuk$(v2) = v0)) & ! [v0: Bool_set_bool_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_fun$] : ! [v2: Bool_set_set$] : (v1 = v0 | ~ (uuj$(v2) = v1) % 92.00/12.88 | ~ (uuj$(v2) = v0)) & ! [v0: Bool_set_bool_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (member$a(v2) = v1) | % 92.00/12.88 ~ (member$a(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : % 92.00/12.88 ! [v2: Bool_set$] : (v1 = v0 | ~ (uum$(v2) = v1) | ~ (uum$(v2) = v0)) & ! % 92.00/12.88 [v0: B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option_set$] : (v1 = v0 | ~ (uun$(v2) = v1) | ~ % 92.00/12.88 (uun$(v2) = v0)) & ! [v0: Bool_bool_fun$] : ! [v1: Bool_bool_fun$] : ! % 92.00/12.88 [v2: Bool_set$] : (v1 = v0 | ~ (uwa$(v2) = v1) | ~ (uwa$(v2) = v0)) & ! % 92.00/12.88 [v0: Nat_set_nat_set_fun$] : ! [v1: Nat_set_nat_set_fun$] : ! [v2: Nat$] : % 92.00/12.88 (v1 = v0 | ~ (insert$a(v2) = v1) | ~ (insert$a(v2) = v0)) & ! [v0: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.88 B_character_data_ptr_option_bool_fun$] : ! [v2: % 92.00/12.88 B_character_data_ptr_option_set$] : (v1 = v0 | ~ (uwb$(v2) = v1) | ~ % 92.00/12.88 (uwb$(v2) = v0)) & ! [v0: Bool_set_bool_set_fun$] : ! [v1: % 92.00/12.88 Bool_set_bool_set_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (insert$(v2) = v1) % 92.00/12.88 | ~ (insert$(v2) = v0)) % 92.00/12.88 % 92.00/12.88 Further assumptions not needed in the proof: % 92.00/12.88 -------------------------------------------- % 92.00/12.88 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 92.00/12.88 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 92.00/12.88 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 92.00/12.88 axiom12, axiom120, axiom121, axiom122, axiom124, axiom125, axiom126, axiom127, % 92.00/12.88 axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, % 92.00/12.88 axiom135, axiom136, axiom137, axiom138, axiom14, axiom140, axiom141, axiom142, % 92.00/12.88 axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, % 92.00/12.88 axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, % 92.00/12.88 axiom158, axiom159, axiom16, axiom160, axiom161, axiom163, axiom164, axiom165, % 92.00/12.88 axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, axiom172, % 92.00/12.88 axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom179, axiom18, % 92.00/12.88 axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, axiom187, % 92.00/12.88 axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, axiom194, % 92.00/12.88 axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, axiom200, % 92.00/12.88 axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, axiom208, % 92.00/12.88 axiom209, axiom21, axiom210, axiom212, axiom213, axiom214, axiom215, axiom216, % 92.00/12.88 axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, axiom222, axiom223, % 92.00/12.88 axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, axiom23, axiom230, % 92.00/12.88 axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, axiom237, axiom238, % 92.00/12.88 axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, axiom244, axiom245, % 92.00/12.88 axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, axiom251, axiom252, % 92.00/12.88 axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, axiom26, % 92.00/12.88 axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, axiom266, axiom267, % 92.00/12.88 axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, axiom273, axiom274, % 92.00/12.88 axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, axiom280, axiom281, % 92.00/12.88 axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, axiom289, % 92.00/12.88 axiom29, axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, % 92.00/12.88 axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, % 92.00/12.88 axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, % 92.00/12.88 axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, axiom317, % 92.00/12.88 axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, % 92.00/12.88 axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, % 92.00/12.88 axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, % 92.00/12.88 axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, % 92.00/12.88 axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, % 92.00/12.88 axiom355, axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, % 92.00/12.88 axiom362, axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, % 92.00/12.88 axiom37, axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, % 92.00/12.88 axiom377, axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, % 92.00/12.88 axiom384, axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, % 92.00/12.88 axiom391, axiom392, axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, % 92.00/12.88 axiom399, axiom4, axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, % 92.00/12.88 axiom405, axiom406, axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, % 92.00/12.88 axiom412, axiom413, axiom414, axiom415, axiom416, axiom417, axiom418, axiom419, % 92.00/12.88 axiom42, axiom420, axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, % 92.00/12.88 axiom427, axiom428, axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, % 92.00/12.88 axiom434, axiom435, axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, % 92.00/12.88 axiom441, axiom442, axiom443, axiom444, axiom445, axiom446, axiom447, axiom448, % 92.00/12.88 axiom449, axiom45, axiom450, axiom451, axiom452, axiom453, axiom454, axiom455, % 92.00/12.88 axiom456, axiom457, axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, % 92.00/12.88 axiom463, axiom464, axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, % 92.00/12.88 axiom470, axiom471, axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, % 92.00/12.88 axiom478, axiom479, axiom48, axiom480, axiom481, axiom482, axiom483, axiom484, % 92.00/12.88 axiom485, axiom486, axiom487, axiom488, axiom49, axiom490, axiom491, axiom492, % 92.00/12.88 axiom493, axiom494, axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, % 92.00/12.88 axiom50, axiom500, axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, % 92.00/12.88 axiom507, axiom508, axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, % 92.00/12.88 axiom514, axiom515, axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, % 92.00/12.88 axiom521, axiom522, axiom523, axiom524, axiom525, axiom526, axiom528, axiom529, % 92.00/12.88 axiom53, axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, % 92.00/12.88 axiom537, axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, % 92.00/12.88 axiom544, axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, % 92.00/12.88 axiom552, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, axiom56, % 92.00/12.88 axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, axiom567, % 92.00/12.88 axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, axiom574, % 92.00/12.88 axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, % 92.00/12.88 axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, % 92.00/12.88 axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, % 92.00/12.88 axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, axiom602, % 92.00/12.88 axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, axiom61, % 92.00/12.88 axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, axiom617, % 92.00/12.88 axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, axiom624, % 92.00/12.88 axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, axiom631, % 92.00/12.88 axiom632, axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, axiom639, % 92.00/12.88 axiom64, axiom640, axiom641, axiom642, axiom643, axiom644, axiom645, axiom646, % 92.00/12.88 axiom647, axiom648, axiom649, axiom65, axiom650, axiom651, axiom652, axiom653, % 92.00/12.88 axiom654, axiom655, axiom656, axiom657, axiom658, axiom659, axiom66, axiom660, % 92.00/12.88 axiom661, axiom662, axiom663, axiom664, axiom665, axiom666, axiom667, axiom668, % 92.00/12.88 axiom669, axiom67, axiom670, axiom671, axiom672, axiom673, axiom674, axiom675, % 92.00/12.88 axiom676, axiom677, axiom678, axiom679, axiom68, axiom680, axiom681, axiom682, % 92.00/12.88 axiom683, axiom684, axiom685, axiom686, axiom687, axiom688, axiom689, axiom69, % 92.00/12.88 axiom690, axiom691, axiom692, axiom693, axiom694, axiom695, axiom696, axiom697, % 92.00/12.88 axiom698, axiom699, axiom7, axiom70, axiom700, axiom701, axiom702, axiom703, % 92.00/12.88 axiom704, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, % 92.00/12.88 axiom78, axiom79, axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom87, % 92.00/12.88 axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, axiom96, axiom97, % 92.00/12.88 axiom98, formula_706, formula_707, formula_708, formula_709, formula_710, % 92.00/12.88 formula_711, formula_712, formula_713, formula_714, formula_715, formula_716, % 92.00/12.88 formula_717, formula_718, formula_719, formula_720, formula_721, formula_722, % 92.00/12.88 formula_723, formula_724, formula_725, formula_726, formula_727, formula_728, % 92.00/12.88 formula_729, formula_730, formula_731, formula_732, formula_733, formula_734, % 92.00/12.88 formula_735, formula_736, formula_737, formula_738, formula_739, formula_740, % 92.00/12.88 formula_741, formula_742, formula_743, formula_744, formula_745, formula_746, % 92.00/12.88 formula_747, formula_748, formula_749, formula_750, formula_751, formula_752, % 92.00/12.88 formula_753 % 92.00/12.88 % 92.00/12.88 Those formulas are unsatisfiable: % 92.00/12.88 --------------------------------- % 92.00/12.88 % 92.00/12.88 Begin of proof % 92.00/12.88 | % 92.00/12.89 | ALPHA: (axiom86) implies: % 92.00/12.89 | (1) is_character_data_ptr_kind_n_o_d_e_p_t_r$(node_ptr$) = 0 % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom88) implies: % 92.00/12.89 | (2) ! [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! % 92.00/12.89 | [v1: B_character_data_ptr$] : ! [v2: B_character_data_ptr_option$] : % 92.00/12.89 | ! [v3: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v3 = % 92.00/12.89 | v0 | ~ (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = % 92.00/12.89 | v2) | ~ (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) % 92.00/12.89 | = v3) | ~ B_character_data_ptr$(v1) | ~ % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v4: % 92.00/12.89 | B_character_data_ptr_option$] : ( ~ (v4 = v2) & fun_app$t(some$, % 92.00/12.89 | v1) = v4 & B_character_data_ptr_option$(v4))) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom89) implies: % 92.00/12.89 | (3) ! [v0: B_character_data_ptr$] : ! [v1: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 92.00/12.89 | (cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v0) = v1) | ~ % 92.00/12.89 | B_character_data_ptr$(v0) | ? [v2: B_character_data_ptr_option$] : % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2 & % 92.00/12.89 | fun_app$t(some$, v0) = v2 & B_character_data_ptr_option$(v2))) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom99) implies: % 92.00/12.89 | (4) ? [v0: B_character_data_ptr_option_bool_fun$] : (case_option$(tlfalse, % 92.00/12.89 | uu$) = v0 & B_character_data_ptr_option_bool_fun$(v0) & ! [v1: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 92.00/12.89 | int] : (v2 = 0 | ~ (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) % 92.00/12.89 | = v2) | ~ % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? % 92.00/12.89 | [v3: B_character_data_ptr_option$] : ? [v4: int] : ( ~ (v4 = 0) & % 92.00/12.89 | cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v3 & % 92.00/12.89 | fun_app$b(v0, v3) = v4 & B_character_data_ptr_option$(v3))) & ! % 92.00/12.89 | [v1: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! % 92.00/12.89 | [v2: B_character_data_ptr_option$] : ( ~ % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2) | % 92.00/12.89 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? % 92.00/12.89 | [v3: any] : ? [v4: any] : % 92.00/12.89 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = v4 & fun_app$b(v0, % 92.00/12.89 | v2) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v1: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v2: % 92.00/12.89 | B_character_data_ptr_option$] : ( ~ % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2) | % 92.00/12.89 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? % 92.00/12.89 | [v3: any] : ? [v4: any] : % 92.00/12.89 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = v3 & fun_app$b(v0, % 92.00/12.89 | v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v1: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 92.00/12.89 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v1) = 0) | ~ % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v1) | ? % 92.00/12.89 | [v2: B_character_data_ptr_option$] : % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v1) = v2 & % 92.00/12.89 | fun_app$b(v0, v2) = 0 & B_character_data_ptr_option$(v2)))) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom139) implies: % 92.00/12.89 | (5) ? [v0: B_character_data_ptr_option_bool_fun$] : (case_option$(tlfalse, % 92.00/12.89 | uu$) = v0 & B_character_data_ptr_option_bool_fun$(v0) & ~ % 92.00/12.89 | (fun_app$b(v0, none$) = 0) & ! [v1: B_character_data_ptr_option$] : % 92.00/12.89 | ! [v2: int] : (v2 = 0 | v1 = none$ | ~ (fun_app$b(v0, v1) = v2) | ~ % 92.00/12.89 | B_character_data_ptr_option$(v1))) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom162) implies: % 92.00/12.89 | (6) ! [v0: B_character_data_ptr_option$] : ! [v1: B_character_data_ptr$] % 92.00/12.89 | : (v0 = none$ | ~ (fun_app$al(the$, v0) = v1) | ~ % 92.00/12.89 | B_character_data_ptr_option$(v0) | fun_app$t(some$, v1) = v0) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom354) implies: % 92.00/12.89 | (7) ? [v0: B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$] : % 92.00/12.89 | ? [v1: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$] % 92.00/12.89 | : (case_sum$a(some$, uvg$) = v0 & case_sum$(uvf$, v0) = v1 & % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$(v1) % 92.00/12.89 | & B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$(v0) & % 92.00/12.89 | ! [v2: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! % 92.00/12.89 | [v3: B_character_data_ptr_option$] : ( ~ (case_node_ptr$(v1, v2) = % 92.00/12.89 | v3) | ~ % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) | % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v3 & % 92.00/12.89 | B_character_data_ptr_option$(v3))) & ! [v2: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v3: % 92.00/12.89 | B_character_data_ptr_option$] : ( ~ % 92.00/12.89 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v3) | % 92.00/12.89 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) | % 92.00/12.89 | (case_node_ptr$(v1, v2) = v3 & B_character_data_ptr_option$(v3)))) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom489) implies: % 92.00/12.89 | (8) collect$c(bot$g) = bot$ % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom527) implies: % 92.00/12.89 | (9) Bool_bool_fun$(bot$g) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom551) implies: % 92.00/12.89 | (10) ~ (top$ = bot$) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (axiom553) implies: % 92.00/12.89 | (11) Bool_bool_fun$(uua$) % 92.00/12.89 | (12) collect$c(uua$) = top$ % 92.00/12.89 | % 92.00/12.89 | ALPHA: (conjecture85) implies: % 92.00/12.89 | (13) A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(node_ptr$) % 92.00/12.89 | (14) ? [v0: B_character_data_ptr_option$] : ? [v1: B_character_data_ptr$] % 92.00/12.89 | : ? [v2: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( % 92.00/12.89 | ~ (v2 = node_ptr$) & fun_app$al(the$, v0) = v1 & % 92.00/12.89 | cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = % 92.00/12.89 | v0 & cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(v1) = v2 % 92.00/12.89 | & B_character_data_ptr$(v1) & % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v2) & % 92.00/12.89 | B_character_data_ptr_option$(v0)) % 92.00/12.89 | % 92.00/12.89 | ALPHA: (function-axioms) implies: % 92.00/12.89 | (15) ! [v0: B_character_data_ptr_option$] : ! [v1: % 92.00/12.89 | B_character_data_ptr_option$] : ! [v2: % 92.00/12.89 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : (v1 = v0 | % 92.00/12.89 | ~ (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = v1) % 92.00/12.89 | | ~ (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v2) = % 92.00/12.89 | v0)) % 92.00/12.90 | (16) ! [v0: B_character_data_ptr_option$] : ! [v1: % 92.00/12.90 | B_character_data_ptr_option$] : ! [v2: B_character_data_ptr$] : ! % 92.00/12.90 | [v3: B_character_data_ptr_b_character_data_ptr_option_fun$] : (v1 = v0 % 92.00/12.90 | | ~ (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) % 92.00/12.90 | (17) ! [v0: B_character_data_ptr_option_bool_fun$] : ! [v1: % 92.00/12.90 | B_character_data_ptr_option_bool_fun$] : ! [v2: % 92.00/12.90 | B_character_data_ptr_bool_fun$] : ! [v3: tlbool] : (v1 = v0 | ~ % 92.00/12.90 | (case_option$(v3, v2) = v1) | ~ (case_option$(v3, v2) = v0)) % 92.00/12.90 | % 92.00/12.90 | DELTA: instantiating (5) with fresh symbol all_951_0 gives: % 92.00/12.90 | (18) case_option$(tlfalse, uu$) = all_951_0 & % 92.00/12.90 | B_character_data_ptr_option_bool_fun$(all_951_0) & ~ % 92.00/12.90 | (fun_app$b(all_951_0, none$) = 0) & ! [v0: % 92.00/12.90 | B_character_data_ptr_option$] : ! [v1: int] : (v1 = 0 | v0 = none$ % 92.00/12.90 | | ~ (fun_app$b(all_951_0, v0) = v1) | ~ % 92.00/12.90 | B_character_data_ptr_option$(v0)) % 92.00/12.90 | % 92.00/12.90 | ALPHA: (18) implies: % 92.00/12.90 | (19) ~ (fun_app$b(all_951_0, none$) = 0) % 92.00/12.90 | (20) case_option$(tlfalse, uu$) = all_951_0 % 92.00/12.90 | % 92.00/12.90 | DELTA: instantiating (14) with fresh symbols all_957_0, all_957_1, all_957_2 % 92.00/12.90 | gives: % 92.00/12.90 | (21) ~ (all_957_0 = node_ptr$) & fun_app$al(the$, all_957_2) = all_957_1 & % 92.00/12.90 | cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = % 92.00/12.90 | all_957_2 & % 92.00/12.90 | cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(all_957_1) = % 92.00/12.90 | all_957_0 & B_character_data_ptr$(all_957_1) & % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(all_957_0) & % 92.00/12.90 | B_character_data_ptr_option$(all_957_2) % 92.00/12.90 | % 92.00/12.90 | ALPHA: (21) implies: % 92.00/12.90 | (22) ~ (all_957_0 = node_ptr$) % 92.00/12.90 | (23) B_character_data_ptr$(all_957_1) % 92.00/12.90 | (24) cast_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r_2_n_o_d_e_p_t_r$(all_957_1) = % 92.00/12.90 | all_957_0 % 92.00/12.90 | (25) cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = % 92.00/12.90 | all_957_2 % 92.00/12.90 | (26) fun_app$al(the$, all_957_2) = all_957_1 % 92.00/12.90 | % 92.00/12.90 | DELTA: instantiating (7) with fresh symbols all_1006_0, all_1006_1 gives: % 92.00/12.90 | (27) case_sum$a(some$, uvg$) = all_1006_1 & case_sum$(uvf$, all_1006_1) = % 92.00/12.90 | all_1006_0 & % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_b_character_data_ptr_option_fun$(all_1006_0) % 92.00/12.90 | & % 92.00/12.90 | B_character_data_ptr_c_sum_b_character_data_ptr_option_fun$(all_1006_1) % 92.00/12.90 | & ! [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! % 92.00/12.90 | [v1: B_character_data_ptr_option$] : ( ~ (case_node_ptr$(all_1006_0, % 92.00/12.90 | v0) = v1) | ~ % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1 & % 92.00/12.90 | B_character_data_ptr_option$(v1))) & ! [v0: % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.90 | B_character_data_ptr_option$] : ( ~ % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1) | % 92.00/12.90 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | % 92.00/12.90 | (case_node_ptr$(all_1006_0, v0) = v1 & % 92.00/12.90 | B_character_data_ptr_option$(v1))) % 92.00/12.90 | % 92.00/12.90 | ALPHA: (27) implies: % 92.00/12.90 | (28) ! [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! % 92.00/12.90 | [v1: B_character_data_ptr_option$] : ( ~ % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1) | % 92.00/12.90 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | % 92.00/12.90 | (case_node_ptr$(all_1006_0, v0) = v1 & % 92.00/12.90 | B_character_data_ptr_option$(v1))) % 92.00/12.90 | % 92.00/12.90 | DELTA: instantiating (4) with fresh symbol all_1023_0 gives: % 92.00/12.90 | (29) case_option$(tlfalse, uu$) = all_1023_0 & % 92.00/12.90 | B_character_data_ptr_option_bool_fun$(all_1023_0) & ! [v0: % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.90 | int] : (v1 = 0 | ~ (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v0) = % 92.00/12.90 | v1) | ~ % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v2: % 92.00/12.90 | B_character_data_ptr_option$] : ? [v3: int] : ( ~ (v3 = 0) & % 92.00/12.90 | cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v2 & % 92.00/12.90 | fun_app$b(all_1023_0, v2) = v3 & % 92.00/12.90 | B_character_data_ptr_option$(v2))) & ! [v0: % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.90 | B_character_data_ptr_option$] : ( ~ % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1) | % 92.00/12.90 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? % 92.00/12.90 | [v2: any] : ? [v3: any] : % 92.00/12.90 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v0) = v3 & % 92.00/12.90 | fun_app$b(all_1023_0, v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! % 92.00/12.90 | [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ! [v1: % 92.00/12.90 | B_character_data_ptr_option$] : ( ~ % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1) | % 92.00/12.90 | ~ A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? % 92.00/12.90 | [v2: any] : ? [v3: any] : % 92.00/12.90 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v0) = v2 & % 92.00/12.90 | fun_app$b(all_1023_0, v1) = v3 & ( ~ (v2 = 0) | v3 = 0))) & ! % 92.00/12.90 | [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 92.00/12.90 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v0) = 0) | ~ % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v1: % 92.00/12.90 | B_character_data_ptr_option$] : % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1 & % 92.00/12.90 | fun_app$b(all_1023_0, v1) = 0 & B_character_data_ptr_option$(v1))) % 92.00/12.90 | % 92.00/12.90 | ALPHA: (29) implies: % 92.00/12.90 | (30) case_option$(tlfalse, uu$) = all_1023_0 % 92.00/12.90 | (31) ! [v0: A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$] : ( ~ % 92.00/12.90 | (is_character_data_ptr_kind_n_o_d_e_p_t_r$(v0) = 0) | ~ % 92.00/12.90 | A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr$(v0) | ? [v1: % 92.00/12.90 | B_character_data_ptr_option$] : % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(v0) = v1 & % 92.00/12.90 | fun_app$b(all_1023_0, v1) = 0 & B_character_data_ptr_option$(v1))) % 92.00/12.90 | % 92.00/12.90 | GROUND_INST: instantiating (17) with all_951_0, all_1023_0, uu$, tlfalse, % 92.00/12.90 | simplifying with (20), (30) gives: % 92.00/12.90 | (32) all_1023_0 = all_951_0 % 92.00/12.90 | % 92.00/12.90 | GROUND_INST: instantiating (31) with node_ptr$, simplifying with (1), (13) % 92.00/12.90 | gives: % 92.00/12.90 | (33) ? [v0: B_character_data_ptr_option$] : % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = v0 % 92.00/12.90 | & fun_app$b(all_1023_0, v0) = 0 & B_character_data_ptr_option$(v0)) % 92.00/12.90 | % 92.00/12.90 | GROUND_INST: instantiating (3) with all_957_1, all_957_0, simplifying with % 92.00/12.90 | (23), (24) gives: % 92.00/12.90 | (34) ? [v0: B_character_data_ptr_option$] : % 92.00/12.90 | (cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(all_957_0) = v0 % 92.00/12.90 | & fun_app$t(some$, all_957_1) = v0 & % 92.00/12.90 | B_character_data_ptr_option$(v0)) % 92.00/12.90 | % 92.00/12.90 | GROUND_INST: instantiating (2) with node_ptr$, all_957_1, all_957_2, % 92.00/12.90 | all_957_0, simplifying with (13), (23), (24), (25) gives: % 92.00/12.90 | (35) all_957_0 = node_ptr$ | ? [v0: any] : ( ~ (v0 = all_957_2) & % 92.00/12.90 | fun_app$t(some$, all_957_1) = v0 & B_character_data_ptr_option$(v0)) % 92.00/12.90 | % 92.00/12.90 | GROUND_INST: instantiating (28) with node_ptr$, all_957_2, simplifying with % 92.00/12.90 | (13), (25) gives: % 92.00/12.90 | (36) case_node_ptr$(all_1006_0, node_ptr$) = all_957_2 & % 92.00/12.90 | B_character_data_ptr_option$(all_957_2) % 92.00/12.90 | % 92.00/12.90 | ALPHA: (36) implies: % 92.00/12.90 | (37) B_character_data_ptr_option$(all_957_2) % 92.00/12.90 | % 92.00/12.91 | GROUND_INST: instantiating (6) with all_957_2, all_957_1, simplifying with % 92.00/12.91 | (26), (37) gives: % 92.00/12.91 | (38) all_957_2 = none$ | fun_app$t(some$, all_957_1) = all_957_2 % 92.00/12.91 | % 92.00/12.91 | GROUND_INST: instantiating (axiom211) with bot$g, uua$, bot$, top$, % 92.00/12.91 | simplifying with (8), (9), (11), (12) gives: % 92.00/12.91 | (39) top$ = bot$ | ? [v0: tlbool] : ? [v1: any] : ? [v2: any] : % 92.00/12.91 | (fun_app$j(bot$g, v0) = v1 & fun_app$j(uua$, v0) = v2 & tlbool(v0) & ( % 92.00/12.91 | ~ (v2 = 0) | ~ (v1 = 0)) & (v2 = 0 | v1 = 0)) % 92.00/12.91 | % 92.00/12.91 | DELTA: instantiating (34) with fresh symbol all_1056_0 gives: % 92.00/12.91 | (40) cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(all_957_0) = % 92.00/12.91 | all_1056_0 & fun_app$t(some$, all_957_1) = all_1056_0 & % 92.00/12.91 | B_character_data_ptr_option$(all_1056_0) % 92.00/12.91 | % 92.00/12.91 | ALPHA: (40) implies: % 92.00/12.91 | (41) fun_app$t(some$, all_957_1) = all_1056_0 % 92.00/12.91 | % 92.00/12.91 | DELTA: instantiating (33) with fresh symbol all_1062_0 gives: % 92.00/12.91 | (42) cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = % 92.00/12.91 | all_1062_0 & fun_app$b(all_1023_0, all_1062_0) = 0 & % 92.00/12.91 | B_character_data_ptr_option$(all_1062_0) % 92.00/12.91 | % 92.00/12.91 | ALPHA: (42) implies: % 92.00/12.91 | (43) fun_app$b(all_1023_0, all_1062_0) = 0 % 92.00/12.91 | (44) cast_n_o_d_e_p_t_r_2_c_h_a_r_a_c_t_e_r_d_a_t_a_p_t_r$(node_ptr$) = % 92.00/12.91 | all_1062_0 % 92.00/12.91 | % 92.00/12.91 | REDUCE: (32), (43) imply: % 92.00/12.91 | (45) fun_app$b(all_951_0, all_1062_0) = 0 % 92.00/12.91 | % 92.00/12.91 | BETA: splitting (35) gives: % 92.00/12.91 | % 92.00/12.91 | Case 1: % 92.00/12.91 | | % 92.00/12.91 | | (46) all_957_0 = node_ptr$ % 92.00/12.91 | | % 92.00/12.91 | | REDUCE: (22), (46) imply: % 92.00/12.91 | | (47) $false % 92.00/12.91 | | % 92.00/12.91 | | CLOSE: (47) is inconsistent. % 92.00/12.91 | | % 92.00/12.91 | Case 2: % 92.00/12.91 | | % 92.00/12.91 | | (48) ? [v0: any] : ( ~ (v0 = all_957_2) & fun_app$t(some$, all_957_1) = % 92.00/12.91 | | v0 & B_character_data_ptr_option$(v0)) % 92.00/12.91 | | % 92.00/12.91 | | DELTA: instantiating (48) with fresh symbol all_1180_0 gives: % 92.00/12.91 | | (49) ~ (all_1180_0 = all_957_2) & fun_app$t(some$, all_957_1) = % 92.00/12.91 | | all_1180_0 & B_character_data_ptr_option$(all_1180_0) % 92.00/12.91 | | % 92.00/12.91 | | ALPHA: (49) implies: % 92.00/12.91 | | (50) ~ (all_1180_0 = all_957_2) % 92.00/12.91 | | (51) fun_app$t(some$, all_957_1) = all_1180_0 % 92.00/12.91 | | % 92.00/12.91 | | BETA: splitting (39) gives: % 92.00/12.91 | | % 92.00/12.91 | | Case 1: % 92.00/12.91 | | | % 92.00/12.91 | | | (52) top$ = bot$ % 92.00/12.91 | | | % 92.00/12.91 | | | REDUCE: (10), (52) imply: % 92.00/12.91 | | | (53) $false % 92.00/12.91 | | | % 92.00/12.91 | | | CLOSE: (53) is inconsistent. % 92.00/12.91 | | | % 92.00/12.91 | | Case 2: % 92.00/12.91 | | | % 92.00/12.91 | | | % 92.00/12.91 | | | GROUND_INST: instantiating (16) with all_1056_0, all_1180_0, all_957_1, % 92.00/12.91 | | | some$, simplifying with (41), (51) gives: % 92.00/12.91 | | | (54) all_1180_0 = all_1056_0 % 92.00/12.91 | | | % 92.00/12.91 | | | GROUND_INST: instantiating (15) with all_957_2, all_1062_0, node_ptr$, % 92.00/12.91 | | | simplifying with (25), (44) gives: % 92.00/12.91 | | | (55) all_1062_0 = all_957_2 % 92.00/12.91 | | | % 92.00/12.91 | | | REDUCE: (50), (54) imply: % 92.00/12.91 | | | (56) ~ (all_1056_0 = all_957_2) % 92.00/12.91 | | | % 92.00/12.91 | | | REDUCE: (45), (55) imply: % 92.00/12.91 | | | (57) fun_app$b(all_951_0, all_957_2) = 0 % 92.00/12.91 | | | % 92.00/12.91 | | | BETA: splitting (38) gives: % 92.00/12.91 | | | % 92.00/12.91 | | | Case 1: % 92.00/12.91 | | | | % 92.00/12.91 | | | | (58) fun_app$t(some$, all_957_1) = all_957_2 % 92.00/12.91 | | | | % 92.00/12.91 | | | | GROUND_INST: instantiating (16) with all_1056_0, all_957_2, all_957_1, % 92.00/12.91 | | | | some$, simplifying with (41), (58) gives: % 92.00/12.91 | | | | (59) all_1056_0 = all_957_2 % 92.00/12.91 | | | | % 92.00/12.91 | | | | REDUCE: (56), (59) imply: % 92.00/12.91 | | | | (60) $false % 92.00/12.91 | | | | % 92.00/12.91 | | | | CLOSE: (60) is inconsistent. % 92.00/12.91 | | | | % 92.00/12.91 | | | Case 2: % 92.00/12.91 | | | | % 92.00/12.91 | | | | (61) all_957_2 = none$ % 92.00/12.91 | | | | % 92.00/12.91 | | | | REDUCE: (57), (61) imply: % 92.00/12.91 | | | | (62) fun_app$b(all_951_0, none$) = 0 % 92.00/12.91 | | | | % 92.00/12.91 | | | | PRED_UNIFY: (19), (62) imply: % 92.00/12.91 | | | | (63) $false % 92.00/12.91 | | | | % 92.00/12.91 | | | | CLOSE: (63) is inconsistent. % 92.00/12.91 | | | | % 92.00/12.91 | | | End of split % 92.00/12.91 | | | % 92.00/12.91 | | End of split % 92.00/12.91 | | % 92.00/12.91 | End of split % 92.00/12.91 | % 92.00/12.91 End of proof % 92.00/12.91 % SZS output end Proof for theBenchmark % 92.00/12.91 % 92.00/12.91 12433ms %------------------------------------------------------------------------------