%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU360+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n009.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 : 600s % DateTime : Tue Jul 19 08:49:10 EDT 2022 % Result : Theorem 22.65s 6.51s % Output : Proof 59.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU360+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 20 13:10:22 EDT 2022 % 0.13/0.34 % CPUTime : % 0.63/0.68 ____ _ % 0.63/0.68 ___ / __ \_____(_)___ ________ __________ % 0.63/0.68 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.63/0.68 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.63/0.68 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.63/0.68 % 0.63/0.68 A Theorem Prover for First-Order Logic % 0.63/0.68 (ePrincess v.1.0) % 0.63/0.68 % 0.63/0.68 (c) Philipp Rümmer, 2009-2015 % 0.63/0.68 (c) Peter Backeman, 2014-2015 % 0.63/0.68 (contributions by Angelo Brillout, Peter Baumgartner) % 0.63/0.68 Free software under GNU Lesser General Public License (LGPL). % 0.63/0.68 Bug reports to peter@backeman.se % 0.63/0.68 % 0.63/0.68 For more information, visit http://user.uu.se/~petba168/breu/ % 0.63/0.68 % 0.63/0.68 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.83/0.75 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.77/1.13 Prover 0: Preprocessing ... % 2.26/1.37 Prover 0: Warning: ignoring some quantifiers % 2.38/1.40 Prover 0: Constructing countermodel ... % 20.42/6.04 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.42/6.08 Prover 1: Preprocessing ... % 21.33/6.25 Prover 1: Warning: ignoring some quantifiers % 21.33/6.26 Prover 1: Constructing countermodel ... % 22.56/6.51 Prover 1: proved (468ms) % 22.56/6.51 Prover 0: stopped % 22.65/6.51 % 22.65/6.51 No countermodel exists, formula is valid % 22.65/6.51 % SZS status Theorem for theBenchmark % 22.65/6.51 % 22.65/6.51 Generating proof ... Warning: ignoring some quantifiers % 57.68/16.73 found it (size 572) % 57.68/16.73 % 57.68/16.73 % SZS output start Proof for theBenchmark % 57.68/16.73 Assumed formulas after preprocessing and simplification: % 57.68/16.73 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & ~ (v8 = 0) & ~ (v6 = 0) & ~ (v1 = 0) & ex_inf_of_relstr_set(v0, v3) = v4 & antisymmetric_relstr(v0) = 0 & ex_sup_of_relstr_set(v0, empty_set) = v2 & empty_carrier(v5) = v6 & empty_carrier(v0) = v1 & one_sorted_str(v12) = 0 & one_sorted_str(v5) = 0 & lower_bounded_relstr(v0) = 0 & rel_str(v13) = 0 & rel_str(v0) = 0 & the_carrier(v0) = v3 & finite(v10) = 0 & empty(v10) = v11 & empty(v9) = 0 & empty(v7) = v8 & empty(empty_set) = 0 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = v14 | ~ (relstr_set_smaller(v18, v17, v16) = v15) | ~ (relstr_set_smaller(v18, v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = v14 | ~ (related(v18, v17, v16) = v15) | ~ (related(v18, v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = v14 | ~ (relstr_element_smaller(v18, v17, v16) = v15) | ~ (relstr_element_smaller(v18, v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ex_inf_of_relstr_set(v17, v16) = v15) | ~ (ex_inf_of_relstr_set(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ex_sup_of_relstr_set(v17, v16) = v15) | ~ (ex_sup_of_relstr_set(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (element(v17, v16) = v15) | ~ (element(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (in(v17, v16) = v15) | ~ (in(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (in(v14, v15) = v16) | ? [v17] : ? [v18] : (element(v14, v15) = v17 & empty(v15) = v18 & ( ~ (v17 = 0) | v18 = 0))) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (antisymmetric_relstr(v16) = v15) | ~ (antisymmetric_relstr(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (empty_carrier(v16) = v15) | ~ (empty_carrier(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (one_sorted_str(v16) = v15) | ~ (one_sorted_str(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (lower_bounded_relstr(v16) = v15) | ~ (lower_bounded_relstr(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (rel_str(v16) = v15) | ~ (rel_str(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (the_carrier(v16) = v15) | ~ (the_carrier(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (finite(v16) = v15) | ~ (finite(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (empty(v16) = v15) | ~ (empty(v16) = v14)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (empty(v15) = 0) | ~ (empty(v14) = 0)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (empty_carrier(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : (one_sorted_str(v14) = v16 & the_carrier(v14) = v17 & empty(v17) = v18 & ( ~ (v18 = 0) | ~ (v16 = 0)))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (one_sorted_str(v14) = v15) | ? [v16] : ( ~ (v16 = 0) & rel_str(v14) = v16)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (finite(v14) = v15) | ? [v16] : ( ~ (v16 = 0) & empty(v14) = v16)) & ! [v14] : ! [v15] : ( ~ (lower_bounded_relstr(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : (rel_str(v14) = v16 & the_carrier(v14) = v17 & ( ~ (v16 = 0) | (( ~ (v15 = 0) | (v20 = 0 & v19 = 0 & element(v18, v17) = 0 & relstr_element_smaller(v14, v17, v18) = 0)) & (v15 = 0 | ! [v21] : ( ~ (relstr_element_smaller(v14, v17, v21) = 0) | ? [v22] : ( ~ (v22 = 0) & element(v21, v17) = v22))))))) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | element(v14, v15) = 0) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & empty(v15) = v16)) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & in(v15, v14) = v16)) & ! [v14] : (v14 = empty_set | ~ (empty(v14) = 0)) & ! [v14] : ( ~ (antisymmetric_relstr(v14) = 0) | ? [v15] : ? [v16] : (rel_str(v14) = v15 & the_carrier(v14) = v16 & ( ~ (v15 = 0) | ( ! [v17] : ! [v18] : ! [v19] : (v18 = 0 | ~ (ex_inf_of_relstr_set(v14, v17) = v18) | ~ (element(v19, v16) = 0) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : ((v22 = 0 & v21 = 0 & ~ (v23 = 0) & related(v14, v20, v19) = v23 & element(v20, v16) = 0 & relstr_element_smaller(v14, v17, v20) = 0) | ( ~ (v20 = 0) & relstr_element_smaller(v14, v17, v19) = v20))) & ! [v17] : ( ~ (ex_inf_of_relstr_set(v14, v17) = 0) | ? [v18] : (element(v18, v16) = 0 & relstr_element_smaller(v14, v17, v18) = 0 & ! [v19] : ( ~ (element(v19, v16) = 0) | ? [v20] : ? [v21] : (related(v14, v19, v18) = v21 & relstr_element_smaller(v14, v17, v19) = v20 & ( ~ (v20 = 0) | v21 = 0))))))))) & ! [v14] : ( ~ (antisymmetric_relstr(v14) = 0) | ? [v15] : ? [v16] : (rel_str(v14) = v15 & the_carrier(v14) = v16 & ( ~ (v15 = 0) | ( ! [v17] : ! [v18] : ! [v19] : (v18 = 0 | ~ (ex_sup_of_relstr_set(v14, v17) = v18) | ~ (element(v19, v16) = 0) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : ((v22 = 0 & v21 = 0 & ~ (v23 = 0) & relstr_set_smaller(v14, v17, v20) = 0 & related(v14, v19, v20) = v23 & element(v20, v16) = 0) | ( ~ (v20 = 0) & relstr_set_smaller(v14, v17, v19) = v20))) & ! [v17] : ( ~ (ex_sup_of_relstr_set(v14, v17) = 0) | ? [v18] : (relstr_set_smaller(v14, v17, v18) = 0 & element(v18, v16) = 0 & ! [v19] : ( ~ (element(v19, v16) = 0) | ? [v20] : ? [v21] : (relstr_set_smaller(v14, v17, v19) = v20 & related(v14, v18, v19) = v21 & ( ~ (v20 = 0) | v21 = 0))))))))) & ! [v14] : ( ~ (rel_str(v14) = 0) | ? [v15] : (the_carrier(v14) = v15 & ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (relstr_element_smaller(v14, v16, v17) = v18) | ? [v19] : ? [v20] : ? [v21] : ? [v22] : ((v21 = 0 & v20 = 0 & ~ (v22 = 0) & related(v14, v17, v19) = v22 & element(v19, v15) = 0 & in(v19, v16) = 0) | ( ~ (v19 = 0) & element(v17, v15) = v19))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (element(v18, v15) = 0) | ~ (relstr_element_smaller(v14, v16, v17) = 0) | ? [v19] : ? [v20] : (( ~ (v19 = 0) & element(v17, v15) = v19) | (related(v14, v17, v18) = v20 & in(v18, v16) = v19 & ( ~ (v19 = 0) | v20 = 0)))))) & ! [v14] : ( ~ (rel_str(v14) = 0) | ? [v15] : (the_carrier(v14) = v15 & ! [v16] : ! [v17] : ( ~ (relstr_set_smaller(v14, empty_set, v16) = v17) | ? [v18] : ? [v19] : (element(v16, v15) = v18 & relstr_element_smaller(v14, empty_set, v16) = v19 & ( ~ (v18 = 0) | (v19 = 0 & v17 = 0)))))) & ? [v14] : ? [v15] : element(v15, v14) = 0 & ( ~ (v4 = 0) | ~ (v2 = 0))) % 57.68/16.80 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 57.68/16.81 | (1) ~ (all_0_2_2 = 0) & ~ (all_0_5_5 = 0) & ~ (all_0_7_7 = 0) & ~ (all_0_12_12 = 0) & ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = all_0_9_9 & antisymmetric_relstr(all_0_13_13) = 0 & ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11 & empty_carrier(all_0_8_8) = all_0_7_7 & empty_carrier(all_0_13_13) = all_0_12_12 & one_sorted_str(all_0_1_1) = 0 & one_sorted_str(all_0_8_8) = 0 & lower_bounded_relstr(all_0_13_13) = 0 & rel_str(all_0_0_0) = 0 & rel_str(all_0_13_13) = 0 & the_carrier(all_0_13_13) = all_0_10_10 & finite(all_0_3_3) = 0 & empty(all_0_3_3) = all_0_2_2 & empty(all_0_4_4) = 0 & empty(all_0_6_6) = all_0_5_5 & empty(empty_set) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (relstr_set_smaller(v4, v3, v2) = v1) | ~ (relstr_set_smaller(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (related(v4, v3, v2) = v1) | ~ (related(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (relstr_element_smaller(v4, v3, v2) = v1) | ~ (relstr_element_smaller(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ex_inf_of_relstr_set(v3, v2) = v1) | ~ (ex_inf_of_relstr_set(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ex_sup_of_relstr_set(v3, v2) = v1) | ~ (ex_sup_of_relstr_set(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (element(v0, v1) = v3 & empty(v1) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (antisymmetric_relstr(v2) = v1) | ~ (antisymmetric_relstr(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty_carrier(v2) = v1) | ~ (empty_carrier(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_sorted_str(v2) = v1) | ~ (one_sorted_str(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (lower_bounded_relstr(v2) = v1) | ~ (lower_bounded_relstr(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (rel_str(v2) = v1) | ~ (rel_str(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (finite(v2) = v1) | ~ (finite(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty_carrier(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : (one_sorted_str(v0) = v2 & the_carrier(v0) = v3 & empty(v3) = v4 & ( ~ (v4 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_sorted_str(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & rel_str(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (lower_bounded_relstr(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (rel_str(v0) = v2 & the_carrier(v0) = v3 & ( ~ (v2 = 0) | (( ~ (v1 = 0) | (v6 = 0 & v5 = 0 & element(v4, v3) = 0 & relstr_element_smaller(v0, v3, v4) = 0)) & (v1 = 0 | ! [v7] : ( ~ (relstr_element_smaller(v0, v3, v7) = 0) | ? [v8] : ( ~ (v8 = 0) & element(v7, v3) = v8))))))) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) & ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) & ! [v0] : ( ~ (antisymmetric_relstr(v0) = 0) | ? [v1] : ? [v2] : (rel_str(v0) = v1 & the_carrier(v0) = v2 & ( ~ (v1 = 0) | ( ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (ex_inf_of_relstr_set(v0, v3) = v4) | ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v8 = 0 & v7 = 0 & ~ (v9 = 0) & related(v0, v6, v5) = v9 & element(v6, v2) = 0 & relstr_element_smaller(v0, v3, v6) = 0) | ( ~ (v6 = 0) & relstr_element_smaller(v0, v3, v5) = v6))) & ! [v3] : ( ~ (ex_inf_of_relstr_set(v0, v3) = 0) | ? [v4] : (element(v4, v2) = 0 & relstr_element_smaller(v0, v3, v4) = 0 & ! [v5] : ( ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : (related(v0, v5, v4) = v7 & relstr_element_smaller(v0, v3, v5) = v6 & ( ~ (v6 = 0) | v7 = 0))))))))) & ! [v0] : ( ~ (antisymmetric_relstr(v0) = 0) | ? [v1] : ? [v2] : (rel_str(v0) = v1 & the_carrier(v0) = v2 & ( ~ (v1 = 0) | ( ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (ex_sup_of_relstr_set(v0, v3) = v4) | ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v8 = 0 & v7 = 0 & ~ (v9 = 0) & relstr_set_smaller(v0, v3, v6) = 0 & related(v0, v5, v6) = v9 & element(v6, v2) = 0) | ( ~ (v6 = 0) & relstr_set_smaller(v0, v3, v5) = v6))) & ! [v3] : ( ~ (ex_sup_of_relstr_set(v0, v3) = 0) | ? [v4] : (relstr_set_smaller(v0, v3, v4) = 0 & element(v4, v2) = 0 & ! [v5] : ( ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : (relstr_set_smaller(v0, v3, v5) = v6 & related(v0, v4, v5) = v7 & ( ~ (v6 = 0) | v7 = 0))))))))) & ! [v0] : ( ~ (rel_str(v0) = 0) | ? [v1] : (the_carrier(v0) = v1 & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (relstr_element_smaller(v0, v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v7 = 0 & v6 = 0 & ~ (v8 = 0) & related(v0, v3, v5) = v8 & element(v5, v1) = 0 & in(v5, v2) = 0) | ( ~ (v5 = 0) & element(v3, v1) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (element(v4, v1) = 0) | ~ (relstr_element_smaller(v0, v2, v3) = 0) | ? [v5] : ? [v6] : (( ~ (v5 = 0) & element(v3, v1) = v5) | (related(v0, v3, v4) = v6 & in(v4, v2) = v5 & ( ~ (v5 = 0) | v6 = 0)))))) & ! [v0] : ( ~ (rel_str(v0) = 0) | ? [v1] : (the_carrier(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relstr_set_smaller(v0, empty_set, v2) = v3) | ? [v4] : ? [v5] : (element(v2, v1) = v4 & relstr_element_smaller(v0, empty_set, v2) = v5 & ( ~ (v4 = 0) | (v5 = 0 & v3 = 0)))))) & ? [v0] : ? [v1] : element(v1, v0) = 0 & ( ~ (all_0_9_9 = 0) | ~ (all_0_11_11 = 0)) % 58.09/16.82 | % 58.09/16.82 | Applying alpha-rule on (1) yields: % 58.09/16.83 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (relstr_element_smaller(v4, v3, v2) = v1) | ~ (relstr_element_smaller(v4, v3, v2) = v0)) % 58.09/16.83 | (3) ! [v0] : ( ~ (rel_str(v0) = 0) | ? [v1] : (the_carrier(v0) = v1 & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (relstr_element_smaller(v0, v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v7 = 0 & v6 = 0 & ~ (v8 = 0) & related(v0, v3, v5) = v8 & element(v5, v1) = 0 & in(v5, v2) = 0) | ( ~ (v5 = 0) & element(v3, v1) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (element(v4, v1) = 0) | ~ (relstr_element_smaller(v0, v2, v3) = 0) | ? [v5] : ? [v6] : (( ~ (v5 = 0) & element(v3, v1) = v5) | (related(v0, v3, v4) = v6 & in(v4, v2) = v5 & ( ~ (v5 = 0) | v6 = 0)))))) % 58.09/16.83 | (4) ! [v0] : ( ~ (antisymmetric_relstr(v0) = 0) | ? [v1] : ? [v2] : (rel_str(v0) = v1 & the_carrier(v0) = v2 & ( ~ (v1 = 0) | ( ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (ex_inf_of_relstr_set(v0, v3) = v4) | ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v8 = 0 & v7 = 0 & ~ (v9 = 0) & related(v0, v6, v5) = v9 & element(v6, v2) = 0 & relstr_element_smaller(v0, v3, v6) = 0) | ( ~ (v6 = 0) & relstr_element_smaller(v0, v3, v5) = v6))) & ! [v3] : ( ~ (ex_inf_of_relstr_set(v0, v3) = 0) | ? [v4] : (element(v4, v2) = 0 & relstr_element_smaller(v0, v3, v4) = 0 & ! [v5] : ( ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : (related(v0, v5, v4) = v7 & relstr_element_smaller(v0, v3, v5) = v6 & ( ~ (v6 = 0) | v7 = 0))))))))) % 58.09/16.83 | (5) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty_carrier(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : (one_sorted_str(v0) = v2 & the_carrier(v0) = v3 & empty(v3) = v4 & ( ~ (v4 = 0) | ~ (v2 = 0)))) % 58.09/16.83 | (6) antisymmetric_relstr(all_0_13_13) = 0 % 58.09/16.83 | (7) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) % 58.09/16.83 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ex_sup_of_relstr_set(v3, v2) = v1) | ~ (ex_sup_of_relstr_set(v3, v2) = v0)) % 58.09/16.83 | (9) ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = all_0_9_9 % 58.09/16.83 | (10) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 58.09/16.83 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 58.09/16.83 | (12) ! [v0] : ( ~ (rel_str(v0) = 0) | ? [v1] : (the_carrier(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relstr_set_smaller(v0, empty_set, v2) = v3) | ? [v4] : ? [v5] : (element(v2, v1) = v4 & relstr_element_smaller(v0, empty_set, v2) = v5 & ( ~ (v4 = 0) | (v5 = 0 & v3 = 0)))))) % 58.09/16.83 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty_carrier(v2) = v1) | ~ (empty_carrier(v2) = v0)) % 58.09/16.83 | (14) ~ (all_0_5_5 = 0) % 58.09/16.83 | (15) ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11 % 58.09/16.83 | (16) empty(all_0_4_4) = 0 % 58.09/16.83 | (17) empty(all_0_3_3) = all_0_2_2 % 58.09/16.83 | (18) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (antisymmetric_relstr(v2) = v1) | ~ (antisymmetric_relstr(v2) = v0)) % 58.09/16.83 | (19) finite(all_0_3_3) = 0 % 58.09/16.83 | (20) ~ (all_0_2_2 = 0) % 58.09/16.83 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (related(v4, v3, v2) = v1) | ~ (related(v4, v3, v2) = v0)) % 58.09/16.83 | (22) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 58.09/16.84 | (23) the_carrier(all_0_13_13) = all_0_10_10 % 58.09/16.84 | (24) one_sorted_str(all_0_1_1) = 0 % 58.09/16.84 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (lower_bounded_relstr(v2) = v1) | ~ (lower_bounded_relstr(v2) = v0)) % 58.09/16.84 | (26) rel_str(all_0_0_0) = 0 % 58.09/16.84 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 58.09/16.84 | (28) empty_carrier(all_0_8_8) = all_0_7_7 % 58.09/16.84 | (29) ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) % 58.09/16.84 | (30) ~ (all_0_7_7 = 0) % 58.09/16.84 | (31) ~ (all_0_9_9 = 0) | ~ (all_0_11_11 = 0) % 58.09/16.84 | (32) empty_carrier(all_0_13_13) = all_0_12_12 % 58.09/16.84 | (33) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (element(v0, v1) = v3 & empty(v1) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 58.09/16.84 | (34) rel_str(all_0_13_13) = 0 % 58.09/16.84 | (35) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 58.09/16.84 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (finite(v2) = v1) | ~ (finite(v2) = v0)) % 58.09/16.84 | (37) lower_bounded_relstr(all_0_13_13) = 0 % 58.09/16.84 | (38) ! [v0] : ( ~ (antisymmetric_relstr(v0) = 0) | ? [v1] : ? [v2] : (rel_str(v0) = v1 & the_carrier(v0) = v2 & ( ~ (v1 = 0) | ( ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (ex_sup_of_relstr_set(v0, v3) = v4) | ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v8 = 0 & v7 = 0 & ~ (v9 = 0) & relstr_set_smaller(v0, v3, v6) = 0 & related(v0, v5, v6) = v9 & element(v6, v2) = 0) | ( ~ (v6 = 0) & relstr_set_smaller(v0, v3, v5) = v6))) & ! [v3] : ( ~ (ex_sup_of_relstr_set(v0, v3) = 0) | ? [v4] : (relstr_set_smaller(v0, v3, v4) = 0 & element(v4, v2) = 0 & ! [v5] : ( ~ (element(v5, v2) = 0) | ? [v6] : ? [v7] : (relstr_set_smaller(v0, v3, v5) = v6 & related(v0, v4, v5) = v7 & ( ~ (v6 = 0) | v7 = 0))))))))) % 58.09/16.84 | (39) ? [v0] : ? [v1] : element(v1, v0) = 0 % 58.09/16.84 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 58.09/16.84 | (41) ~ (all_0_12_12 = 0) % 58.09/16.84 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ex_inf_of_relstr_set(v3, v2) = v1) | ~ (ex_inf_of_relstr_set(v3, v2) = v0)) % 58.09/16.84 | (43) empty(all_0_6_6) = all_0_5_5 % 58.09/16.84 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (rel_str(v2) = v1) | ~ (rel_str(v2) = v0)) % 58.09/16.84 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (relstr_set_smaller(v4, v3, v2) = v1) | ~ (relstr_set_smaller(v4, v3, v2) = v0)) % 58.09/16.84 | (46) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_sorted_str(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & rel_str(v0) = v2)) % 58.09/16.84 | (47) empty(empty_set) = 0 % 58.09/16.84 | (48) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_sorted_str(v2) = v1) | ~ (one_sorted_str(v2) = v0)) % 58.09/16.84 | (49) ! [v0] : ! [v1] : ( ~ (lower_bounded_relstr(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (rel_str(v0) = v2 & the_carrier(v0) = v3 & ( ~ (v2 = 0) | (( ~ (v1 = 0) | (v6 = 0 & v5 = 0 & element(v4, v3) = 0 & relstr_element_smaller(v0, v3, v4) = 0)) & (v1 = 0 | ! [v7] : ( ~ (relstr_element_smaller(v0, v3, v7) = 0) | ? [v8] : ( ~ (v8 = 0) & element(v7, v3) = v8))))))) % 58.09/16.85 | (50) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 58.09/16.85 | (51) one_sorted_str(all_0_8_8) = 0 % 58.09/16.85 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (10) with empty_set, all_0_4_4 and discharging atoms empty(all_0_4_4) = 0, empty(empty_set) = 0, yields: % 58.09/16.85 | (53) all_0_4_4 = empty_set % 58.09/16.85 | % 58.09/16.85 | From (53) and (16) follows: % 58.09/16.85 | (47) empty(empty_set) = 0 % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (4) with all_0_13_13 and discharging atoms antisymmetric_relstr(all_0_13_13) = 0, yields: % 58.09/16.85 | (55) ? [v0] : ? [v1] : (rel_str(all_0_13_13) = v0 & the_carrier(all_0_13_13) = v1 & ( ~ (v0 = 0) | ( ! [v2] : ! [v3] : ! [v4] : (v3 = 0 | ~ (ex_inf_of_relstr_set(all_0_13_13, v2) = v3) | ~ (element(v4, v1) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v7 = 0 & v6 = 0 & ~ (v8 = 0) & related(all_0_13_13, v5, v4) = v8 & element(v5, v1) = 0 & relstr_element_smaller(all_0_13_13, v2, v5) = 0) | ( ~ (v5 = 0) & relstr_element_smaller(all_0_13_13, v2, v4) = v5))) & ! [v2] : ( ~ (ex_inf_of_relstr_set(all_0_13_13, v2) = 0) | ? [v3] : (element(v3, v1) = 0 & relstr_element_smaller(all_0_13_13, v2, v3) = 0 & ! [v4] : ( ~ (element(v4, v1) = 0) | ? [v5] : ? [v6] : (related(all_0_13_13, v4, v3) = v6 & relstr_element_smaller(all_0_13_13, v2, v4) = v5 & ( ~ (v5 = 0) | v6 = 0)))))))) % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (38) with all_0_13_13 and discharging atoms antisymmetric_relstr(all_0_13_13) = 0, yields: % 58.09/16.85 | (56) ? [v0] : ? [v1] : (rel_str(all_0_13_13) = v0 & the_carrier(all_0_13_13) = v1 & ( ~ (v0 = 0) | ( ! [v2] : ! [v3] : ! [v4] : (v3 = 0 | ~ (ex_sup_of_relstr_set(all_0_13_13, v2) = v3) | ~ (element(v4, v1) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v7 = 0 & v6 = 0 & ~ (v8 = 0) & relstr_set_smaller(all_0_13_13, v2, v5) = 0 & related(all_0_13_13, v4, v5) = v8 & element(v5, v1) = 0) | ( ~ (v5 = 0) & relstr_set_smaller(all_0_13_13, v2, v4) = v5))) & ! [v2] : ( ~ (ex_sup_of_relstr_set(all_0_13_13, v2) = 0) | ? [v3] : (relstr_set_smaller(all_0_13_13, v2, v3) = 0 & element(v3, v1) = 0 & ! [v4] : ( ~ (element(v4, v1) = 0) | ? [v5] : ? [v6] : (relstr_set_smaller(all_0_13_13, v2, v4) = v5 & related(all_0_13_13, v3, v4) = v6 & ( ~ (v5 = 0) | v6 = 0)))))))) % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (5) with all_0_12_12, all_0_13_13 and discharging atoms empty_carrier(all_0_13_13) = all_0_12_12, yields: % 58.09/16.85 | (57) all_0_12_12 = 0 | ? [v0] : ? [v1] : ? [v2] : (one_sorted_str(all_0_13_13) = v0 & the_carrier(all_0_13_13) = v1 & empty(v1) = v2 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (49) with 0, all_0_13_13 and discharging atoms lower_bounded_relstr(all_0_13_13) = 0, yields: % 58.09/16.85 | (58) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (rel_str(all_0_13_13) = v0 & the_carrier(all_0_13_13) = v1 & ( ~ (v0 = 0) | (v4 = 0 & v3 = 0 & element(v2, v1) = 0 & relstr_element_smaller(all_0_13_13, v1, v2) = 0))) % 58.09/16.85 | % 58.09/16.85 | Instantiating formula (3) with all_0_13_13 and discharging atoms rel_str(all_0_13_13) = 0, yields: % 58.09/16.85 | (59) ? [v0] : (the_carrier(all_0_13_13) = v0 & ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (relstr_element_smaller(all_0_13_13, v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ((v6 = 0 & v5 = 0 & ~ (v7 = 0) & related(all_0_13_13, v2, v4) = v7 & element(v4, v0) = 0 & in(v4, v1) = 0) | ( ~ (v4 = 0) & element(v2, v0) = v4))) & ! [v1] : ! [v2] : ! [v3] : ( ~ (element(v3, v0) = 0) | ~ (relstr_element_smaller(all_0_13_13, v1, v2) = 0) | ? [v4] : ? [v5] : (( ~ (v4 = 0) & element(v2, v0) = v4) | (related(all_0_13_13, v2, v3) = v5 & in(v3, v1) = v4 & ( ~ (v4 = 0) | v5 = 0))))) % 58.09/16.86 | % 58.09/16.86 | Instantiating formula (12) with all_0_13_13 and discharging atoms rel_str(all_0_13_13) = 0, yields: % 58.09/16.86 | (60) ? [v0] : (the_carrier(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (relstr_set_smaller(all_0_13_13, empty_set, v1) = v2) | ? [v3] : ? [v4] : (element(v1, v0) = v3 & relstr_element_smaller(all_0_13_13, empty_set, v1) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0))))) % 58.09/16.86 | % 58.09/16.86 | Instantiating (60) with all_14_0_16 yields: % 58.09/16.86 | (61) the_carrier(all_0_13_13) = all_14_0_16 & ! [v0] : ! [v1] : ( ~ (relstr_set_smaller(all_0_13_13, empty_set, v0) = v1) | ? [v2] : ? [v3] : (element(v0, all_14_0_16) = v2 & relstr_element_smaller(all_0_13_13, empty_set, v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) % 58.09/16.86 | % 58.09/16.86 | Applying alpha-rule on (61) yields: % 58.09/16.86 | (62) the_carrier(all_0_13_13) = all_14_0_16 % 58.09/16.86 | (63) ! [v0] : ! [v1] : ( ~ (relstr_set_smaller(all_0_13_13, empty_set, v0) = v1) | ? [v2] : ? [v3] : (element(v0, all_14_0_16) = v2 & relstr_element_smaller(all_0_13_13, empty_set, v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) % 58.09/16.86 | % 58.09/16.86 | Instantiating (59) with all_17_0_17 yields: % 58.09/16.86 | (64) the_carrier(all_0_13_13) = all_17_0_17 & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (relstr_element_smaller(all_0_13_13, v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v1, v3) = v6 & element(v3, all_17_0_17) = 0 & in(v3, v0) = 0) | ( ~ (v3 = 0) & element(v1, all_17_0_17) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (element(v2, all_17_0_17) = 0) | ~ (relstr_element_smaller(all_0_13_13, v0, v1) = 0) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & element(v1, all_17_0_17) = v3) | (related(all_0_13_13, v1, v2) = v4 & in(v2, v0) = v3 & ( ~ (v3 = 0) | v4 = 0)))) % 58.09/16.86 | % 58.09/16.86 | Applying alpha-rule on (64) yields: % 58.09/16.86 | (65) the_carrier(all_0_13_13) = all_17_0_17 % 58.09/16.86 | (66) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (relstr_element_smaller(all_0_13_13, v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v1, v3) = v6 & element(v3, all_17_0_17) = 0 & in(v3, v0) = 0) | ( ~ (v3 = 0) & element(v1, all_17_0_17) = v3))) % 58.09/16.86 | (67) ! [v0] : ! [v1] : ! [v2] : ( ~ (element(v2, all_17_0_17) = 0) | ~ (relstr_element_smaller(all_0_13_13, v0, v1) = 0) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & element(v1, all_17_0_17) = v3) | (related(all_0_13_13, v1, v2) = v4 & in(v2, v0) = v3 & ( ~ (v3 = 0) | v4 = 0)))) % 58.09/16.86 | % 58.09/16.86 | Instantiating (58) with all_26_0_20, all_26_1_21, all_26_2_22, all_26_3_23, all_26_4_24 yields: % 58.09/16.86 | (68) rel_str(all_0_13_13) = all_26_4_24 & the_carrier(all_0_13_13) = all_26_3_23 & ( ~ (all_26_4_24 = 0) | (all_26_0_20 = 0 & all_26_1_21 = 0 & element(all_26_2_22, all_26_3_23) = 0 & relstr_element_smaller(all_0_13_13, all_26_3_23, all_26_2_22) = 0)) % 58.09/16.86 | % 58.09/16.86 | Applying alpha-rule on (68) yields: % 58.09/16.86 | (69) rel_str(all_0_13_13) = all_26_4_24 % 58.09/16.86 | (70) the_carrier(all_0_13_13) = all_26_3_23 % 58.09/16.86 | (71) ~ (all_26_4_24 = 0) | (all_26_0_20 = 0 & all_26_1_21 = 0 & element(all_26_2_22, all_26_3_23) = 0 & relstr_element_smaller(all_0_13_13, all_26_3_23, all_26_2_22) = 0) % 58.09/16.86 | % 58.09/16.86 | Instantiating (56) with all_28_0_25, all_28_1_26 yields: % 58.09/16.86 | (72) rel_str(all_0_13_13) = all_28_1_26 & the_carrier(all_0_13_13) = all_28_0_25 & ( ~ (all_28_1_26 = 0) | ( ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & relstr_set_smaller(all_0_13_13, v0, v3) = 0 & related(all_0_13_13, v2, v3) = v6 & element(v3, all_28_0_25) = 0) | ( ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (relstr_set_smaller(all_0_13_13, v0, v1) = 0 & element(v1, all_28_0_25) = 0 & ! [v2] : ( ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : (relstr_set_smaller(all_0_13_13, v0, v2) = v3 & related(all_0_13_13, v1, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))))))) % 58.09/16.87 | % 58.09/16.87 | Applying alpha-rule on (72) yields: % 58.09/16.87 | (73) rel_str(all_0_13_13) = all_28_1_26 % 58.09/16.87 | (74) the_carrier(all_0_13_13) = all_28_0_25 % 58.09/16.87 | (75) ~ (all_28_1_26 = 0) | ( ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & relstr_set_smaller(all_0_13_13, v0, v3) = 0 & related(all_0_13_13, v2, v3) = v6 & element(v3, all_28_0_25) = 0) | ( ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (relstr_set_smaller(all_0_13_13, v0, v1) = 0 & element(v1, all_28_0_25) = 0 & ! [v2] : ( ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : (relstr_set_smaller(all_0_13_13, v0, v2) = v3 & related(all_0_13_13, v1, v2) = v4 & ( ~ (v3 = 0) | v4 = 0)))))) % 58.09/16.87 | % 58.09/16.87 | Instantiating (55) with all_30_0_27, all_30_1_28 yields: % 58.09/16.87 | (76) rel_str(all_0_13_13) = all_30_1_28 & the_carrier(all_0_13_13) = all_30_0_27 & ( ~ (all_30_1_28 = 0) | ( ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v3, v2) = v6 & element(v3, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v3) = 0) | ( ~ (v3 = 0) & relstr_element_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (element(v1, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v1) = 0 & ! [v2] : ( ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : (related(all_0_13_13, v2, v1) = v4 & relstr_element_smaller(all_0_13_13, v0, v2) = v3 & ( ~ (v3 = 0) | v4 = 0))))))) % 58.09/16.87 | % 58.09/16.87 | Applying alpha-rule on (76) yields: % 58.09/16.87 | (77) rel_str(all_0_13_13) = all_30_1_28 % 58.09/16.87 | (78) the_carrier(all_0_13_13) = all_30_0_27 % 58.09/16.87 | (79) ~ (all_30_1_28 = 0) | ( ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v3, v2) = v6 & element(v3, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v3) = 0) | ( ~ (v3 = 0) & relstr_element_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (element(v1, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v1) = 0 & ! [v2] : ( ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : (related(all_0_13_13, v2, v1) = v4 & relstr_element_smaller(all_0_13_13, v0, v2) = v3 & ( ~ (v3 = 0) | v4 = 0)))))) % 58.09/16.87 | % 58.09/16.87 +-Applying beta-rule and splitting (57), into two cases. % 58.09/16.87 |-Branch one: % 58.09/16.87 | (80) all_0_12_12 = 0 % 58.09/16.87 | % 58.09/16.87 | Equations (80) can reduce 41 to: % 58.09/16.87 | (81) $false % 58.09/16.87 | % 58.09/16.87 |-The branch is then unsatisfiable % 58.09/16.87 |-Branch two: % 58.09/16.87 | (41) ~ (all_0_12_12 = 0) % 58.09/16.87 | (83) ? [v0] : ? [v1] : ? [v2] : (one_sorted_str(all_0_13_13) = v0 & the_carrier(all_0_13_13) = v1 & empty(v1) = v2 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 58.09/16.87 | % 58.09/16.88 | Instantiating (83) with all_41_0_32, all_41_1_33, all_41_2_34 yields: % 58.09/16.88 | (84) one_sorted_str(all_0_13_13) = all_41_2_34 & the_carrier(all_0_13_13) = all_41_1_33 & empty(all_41_1_33) = all_41_0_32 & ( ~ (all_41_0_32 = 0) | ~ (all_41_2_34 = 0)) % 58.09/16.88 | % 58.09/16.88 | Applying alpha-rule on (84) yields: % 58.09/16.88 | (85) one_sorted_str(all_0_13_13) = all_41_2_34 % 58.09/16.88 | (86) the_carrier(all_0_13_13) = all_41_1_33 % 58.09/16.88 | (87) empty(all_41_1_33) = all_41_0_32 % 58.09/16.88 | (88) ~ (all_41_0_32 = 0) | ~ (all_41_2_34 = 0) % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (44) with all_0_13_13, all_30_1_28, 0 and discharging atoms rel_str(all_0_13_13) = all_30_1_28, rel_str(all_0_13_13) = 0, yields: % 58.09/16.88 | (89) all_30_1_28 = 0 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (44) with all_0_13_13, all_28_1_26, all_30_1_28 and discharging atoms rel_str(all_0_13_13) = all_30_1_28, rel_str(all_0_13_13) = all_28_1_26, yields: % 58.09/16.88 | (90) all_30_1_28 = all_28_1_26 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (44) with all_0_13_13, all_26_4_24, all_30_1_28 and discharging atoms rel_str(all_0_13_13) = all_30_1_28, rel_str(all_0_13_13) = all_26_4_24, yields: % 58.09/16.88 | (91) all_30_1_28 = all_26_4_24 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_30_0_27, all_41_1_33 and discharging atoms the_carrier(all_0_13_13) = all_41_1_33, the_carrier(all_0_13_13) = all_30_0_27, yields: % 58.09/16.88 | (92) all_41_1_33 = all_30_0_27 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_28_0_25, all_0_10_10 and discharging atoms the_carrier(all_0_13_13) = all_28_0_25, the_carrier(all_0_13_13) = all_0_10_10, yields: % 58.09/16.88 | (93) all_28_0_25 = all_0_10_10 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_28_0_25, all_30_0_27 and discharging atoms the_carrier(all_0_13_13) = all_30_0_27, the_carrier(all_0_13_13) = all_28_0_25, yields: % 58.09/16.88 | (94) all_30_0_27 = all_28_0_25 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_26_3_23, all_30_0_27 and discharging atoms the_carrier(all_0_13_13) = all_30_0_27, the_carrier(all_0_13_13) = all_26_3_23, yields: % 58.09/16.88 | (95) all_30_0_27 = all_26_3_23 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_17_0_17, all_41_1_33 and discharging atoms the_carrier(all_0_13_13) = all_41_1_33, the_carrier(all_0_13_13) = all_17_0_17, yields: % 58.09/16.88 | (96) all_41_1_33 = all_17_0_17 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (52) with all_0_13_13, all_14_0_16, all_41_1_33 and discharging atoms the_carrier(all_0_13_13) = all_41_1_33, the_carrier(all_0_13_13) = all_14_0_16, yields: % 58.09/16.88 | (97) all_41_1_33 = all_14_0_16 % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (40) with empty_set, all_41_0_32, 0 and discharging atoms empty(empty_set) = 0, yields: % 58.09/16.88 | (98) all_41_0_32 = 0 | ~ (empty(empty_set) = all_41_0_32) % 58.09/16.88 | % 58.09/16.88 | Instantiating formula (22) with all_41_1_33 yields: % 58.09/16.88 | (99) all_41_1_33 = empty_set | ~ (empty(all_41_1_33) = 0) % 58.09/16.88 | % 58.09/16.88 | Combining equations (92,96) yields a new equation: % 58.09/16.88 | (100) all_30_0_27 = all_17_0_17 % 58.09/16.88 | % 58.09/16.88 | Simplifying 100 yields: % 58.09/16.88 | (101) all_30_0_27 = all_17_0_17 % 58.09/16.88 | % 58.09/16.88 | Combining equations (97,96) yields a new equation: % 58.09/16.88 | (102) all_17_0_17 = all_14_0_16 % 58.09/16.88 | % 58.09/16.88 | Combining equations (94,95) yields a new equation: % 58.09/16.88 | (103) all_28_0_25 = all_26_3_23 % 58.09/16.88 | % 58.09/16.88 | Simplifying 103 yields: % 58.09/16.88 | (104) all_28_0_25 = all_26_3_23 % 58.09/16.88 | % 58.09/16.88 | Combining equations (101,95) yields a new equation: % 58.09/16.88 | (105) all_26_3_23 = all_17_0_17 % 58.09/16.88 | % 58.09/16.88 | Combining equations (91,90) yields a new equation: % 58.09/16.88 | (106) all_28_1_26 = all_26_4_24 % 58.09/16.88 | % 58.09/16.88 | Combining equations (89,90) yields a new equation: % 58.09/16.88 | (107) all_28_1_26 = 0 % 58.09/16.88 | % 58.09/16.88 | Combining equations (104,93) yields a new equation: % 58.09/16.88 | (108) all_26_3_23 = all_0_10_10 % 58.09/16.88 | % 58.09/16.88 | Simplifying 108 yields: % 58.09/16.88 | (109) all_26_3_23 = all_0_10_10 % 58.09/16.88 | % 58.09/16.88 | Combining equations (106,107) yields a new equation: % 58.09/16.88 | (110) all_26_4_24 = 0 % 58.09/16.88 | % 58.09/16.88 | Simplifying 110 yields: % 58.09/16.89 | (111) all_26_4_24 = 0 % 58.09/16.89 | % 58.09/16.89 | Combining equations (105,109) yields a new equation: % 58.09/16.89 | (112) all_17_0_17 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | Simplifying 112 yields: % 58.09/16.89 | (113) all_17_0_17 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | Combining equations (113,102) yields a new equation: % 58.09/16.89 | (114) all_14_0_16 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | Combining equations (114,102) yields a new equation: % 58.09/16.89 | (113) all_17_0_17 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | Combining equations (107,90) yields a new equation: % 58.09/16.89 | (89) all_30_1_28 = 0 % 58.09/16.89 | % 58.09/16.89 | Combining equations (109,95) yields a new equation: % 58.09/16.89 | (117) all_30_0_27 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | Combining equations (113,96) yields a new equation: % 58.09/16.89 | (118) all_41_1_33 = all_0_10_10 % 58.09/16.89 | % 58.09/16.89 | From (111) and (69) follows: % 58.09/16.89 | (34) rel_str(all_0_13_13) = 0 % 58.09/16.89 | % 58.09/16.89 | From (118) and (87) follows: % 58.09/16.89 | (120) empty(all_0_10_10) = all_41_0_32 % 58.09/16.89 | % 58.09/16.89 +-Applying beta-rule and splitting (71), into two cases. % 58.09/16.89 |-Branch one: % 58.09/16.89 | (121) ~ (all_26_4_24 = 0) % 58.09/16.89 | % 58.09/16.89 | Equations (111) can reduce 121 to: % 58.09/16.89 | (81) $false % 58.09/16.89 | % 58.09/16.89 |-The branch is then unsatisfiable % 58.09/16.89 |-Branch two: % 58.09/16.89 | (111) all_26_4_24 = 0 % 58.09/16.89 | (124) all_26_0_20 = 0 & all_26_1_21 = 0 & element(all_26_2_22, all_26_3_23) = 0 & relstr_element_smaller(all_0_13_13, all_26_3_23, all_26_2_22) = 0 % 58.09/16.89 | % 58.09/16.89 | Applying alpha-rule on (124) yields: % 58.09/16.89 | (125) all_26_0_20 = 0 % 58.09/16.89 | (126) all_26_1_21 = 0 % 58.09/16.89 | (127) element(all_26_2_22, all_26_3_23) = 0 % 58.09/16.89 | (128) relstr_element_smaller(all_0_13_13, all_26_3_23, all_26_2_22) = 0 % 58.09/16.89 | % 58.09/16.89 | From (109) and (127) follows: % 58.09/16.89 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.09/16.89 | % 58.09/16.89 | From (109) and (128) follows: % 58.09/16.89 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.09/16.89 | % 58.09/16.89 +-Applying beta-rule and splitting (75), into two cases. % 58.09/16.89 |-Branch one: % 58.09/16.89 | (131) ~ (all_28_1_26 = 0) % 58.09/16.89 | % 58.09/16.89 | Equations (107) can reduce 131 to: % 58.09/16.89 | (81) $false % 58.09/16.89 | % 58.09/16.89 |-The branch is then unsatisfiable % 58.09/16.89 |-Branch two: % 58.09/16.89 | (107) all_28_1_26 = 0 % 58.09/16.89 | (134) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & relstr_set_smaller(all_0_13_13, v0, v3) = 0 & related(all_0_13_13, v2, v3) = v6 & element(v3, all_28_0_25) = 0) | ( ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (relstr_set_smaller(all_0_13_13, v0, v1) = 0 & element(v1, all_28_0_25) = 0 & ! [v2] : ( ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : (relstr_set_smaller(all_0_13_13, v0, v2) = v3 & related(all_0_13_13, v1, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))))) % 58.09/16.89 | % 58.09/16.89 | Applying alpha-rule on (134) yields: % 58.09/16.89 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & relstr_set_smaller(all_0_13_13, v0, v3) = 0 & related(all_0_13_13, v2, v3) = v6 & element(v3, all_28_0_25) = 0) | ( ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, v0, v2) = v3))) % 58.47/16.90 | (136) ! [v0] : ( ~ (ex_sup_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (relstr_set_smaller(all_0_13_13, v0, v1) = 0 & element(v1, all_28_0_25) = 0 & ! [v2] : ( ~ (element(v2, all_28_0_25) = 0) | ? [v3] : ? [v4] : (relstr_set_smaller(all_0_13_13, v0, v2) = v3 & related(all_0_13_13, v1, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))))) % 58.47/16.90 | % 58.47/16.90 +-Applying beta-rule and splitting (79), into two cases. % 58.47/16.90 |-Branch one: % 58.47/16.90 | (137) ~ (all_30_1_28 = 0) % 58.47/16.90 | % 58.47/16.90 | Equations (89) can reduce 137 to: % 58.47/16.90 | (81) $false % 58.47/16.90 | % 58.47/16.90 |-The branch is then unsatisfiable % 58.47/16.90 |-Branch two: % 58.47/16.90 | (89) all_30_1_28 = 0 % 58.47/16.90 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v3, v2) = v6 & element(v3, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v3) = 0) | ( ~ (v3 = 0) & relstr_element_smaller(all_0_13_13, v0, v2) = v3))) & ! [v0] : ( ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (element(v1, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v1) = 0 & ! [v2] : ( ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : (related(all_0_13_13, v2, v1) = v4 & relstr_element_smaller(all_0_13_13, v0, v2) = v3 & ( ~ (v3 = 0) | v4 = 0))))) % 58.47/16.90 | % 58.47/16.90 | Applying alpha-rule on (140) yields: % 58.47/16.90 | (141) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = v1) | ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & v4 = 0 & ~ (v6 = 0) & related(all_0_13_13, v3, v2) = v6 & element(v3, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v3) = 0) | ( ~ (v3 = 0) & relstr_element_smaller(all_0_13_13, v0, v2) = v3))) % 58.47/16.90 | (142) ! [v0] : ( ~ (ex_inf_of_relstr_set(all_0_13_13, v0) = 0) | ? [v1] : (element(v1, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, v0, v1) = 0 & ! [v2] : ( ~ (element(v2, all_30_0_27) = 0) | ? [v3] : ? [v4] : (related(all_0_13_13, v2, v1) = v4 & relstr_element_smaller(all_0_13_13, v0, v2) = v3 & ( ~ (v3 = 0) | v4 = 0))))) % 58.47/16.90 | % 58.47/16.90 | Instantiating formula (142) with all_0_10_10 yields: % 58.47/16.90 | (143) ~ (ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = 0) | ? [v0] : (element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0 & ! [v1] : ( ~ (element(v1, all_30_0_27) = 0) | ? [v2] : ? [v3] : (related(all_0_13_13, v1, v0) = v3 & relstr_element_smaller(all_0_13_13, all_0_10_10, v1) = v2 & ( ~ (v2 = 0) | v3 = 0)))) % 58.47/16.91 | % 58.47/16.91 | Instantiating formula (46) with all_41_2_34, all_0_13_13 and discharging atoms one_sorted_str(all_0_13_13) = all_41_2_34, yields: % 58.47/16.91 | (144) all_41_2_34 = 0 | ? [v0] : ( ~ (v0 = 0) & rel_str(all_0_13_13) = v0) % 58.47/16.91 | % 58.47/16.91 | Instantiating formula (141) with all_26_2_22, all_0_9_9, all_0_10_10 and discharging atoms ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = all_0_9_9, yields: % 58.47/16.91 | (145) all_0_9_9 = 0 | ~ (element(all_26_2_22, all_30_0_27) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & related(all_0_13_13, v0, all_26_2_22) = v3 & element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0) | ( ~ (v0 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0)) % 58.47/16.91 | % 58.47/16.91 | Instantiating formula (135) with all_26_2_22, all_0_11_11, empty_set and discharging atoms ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11, yields: % 58.47/16.91 | (146) all_0_11_11 = 0 | ~ (element(all_26_2_22, all_28_0_25) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_26_2_22, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = v0)) % 58.47/16.91 | % 58.47/16.91 | Instantiating formula (67) with all_26_2_22, all_26_2_22, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.91 | (147) ~ (element(all_26_2_22, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.91 | % 58.47/16.91 +-Applying beta-rule and splitting (144), into two cases. % 58.47/16.91 |-Branch one: % 58.47/16.91 | (148) all_41_2_34 = 0 % 58.47/16.91 | % 58.47/16.91 +-Applying beta-rule and splitting (147), into two cases. % 58.47/16.91 |-Branch one: % 58.47/16.91 | (149) ~ (element(all_26_2_22, all_17_0_17) = 0) % 58.47/16.91 | % 58.47/16.91 | From (113) and (149) follows: % 58.47/16.91 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.91 | % 58.47/16.91 | Using (129) and (150) yields: % 58.47/16.91 | (151) $false % 58.47/16.91 | % 58.47/16.91 |-The branch is then unsatisfiable % 58.47/16.91 |-Branch two: % 58.47/16.91 | (152) element(all_26_2_22, all_17_0_17) = 0 % 58.47/16.91 | (153) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.91 | % 58.47/16.91 | Instantiating (153) with all_78_0_35, all_78_1_36 yields: % 58.47/16.91 | (154) ( ~ (all_78_1_36 = 0) & element(all_26_2_22, all_17_0_17) = all_78_1_36) | (related(all_0_13_13, all_26_2_22, all_26_2_22) = all_78_0_35 & in(all_26_2_22, all_0_10_10) = all_78_1_36 & ( ~ (all_78_1_36 = 0) | all_78_0_35 = 0)) % 58.47/16.91 | % 58.47/16.91 | From (113) and (152) follows: % 58.47/16.91 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.91 | % 58.47/16.91 +-Applying beta-rule and splitting (88), into two cases. % 58.47/16.91 |-Branch one: % 58.47/16.91 | (156) ~ (all_41_0_32 = 0) % 58.47/16.91 | % 58.47/16.91 +-Applying beta-rule and splitting (154), into two cases. % 58.47/16.91 |-Branch one: % 58.47/16.91 | (157) ~ (all_78_1_36 = 0) & element(all_26_2_22, all_17_0_17) = all_78_1_36 % 58.47/16.91 | % 58.47/16.91 | Applying alpha-rule on (157) yields: % 58.47/16.91 | (158) ~ (all_78_1_36 = 0) % 58.47/16.91 | (159) element(all_26_2_22, all_17_0_17) = all_78_1_36 % 58.47/16.91 | % 58.47/16.91 | From (113) and (159) follows: % 58.47/16.91 | (160) element(all_26_2_22, all_0_10_10) = all_78_1_36 % 58.47/16.91 | % 58.47/16.91 | Instantiating formula (11) with all_26_2_22, all_0_10_10, all_78_1_36, 0 and discharging atoms element(all_26_2_22, all_0_10_10) = all_78_1_36, element(all_26_2_22, all_0_10_10) = 0, yields: % 58.47/16.91 | (161) all_78_1_36 = 0 % 58.47/16.91 | % 58.47/16.91 | Equations (161) can reduce 158 to: % 58.47/16.92 | (81) $false % 58.47/16.92 | % 58.47/16.92 |-The branch is then unsatisfiable % 58.47/16.92 |-Branch two: % 58.47/16.92 | (163) related(all_0_13_13, all_26_2_22, all_26_2_22) = all_78_0_35 & in(all_26_2_22, all_0_10_10) = all_78_1_36 & ( ~ (all_78_1_36 = 0) | all_78_0_35 = 0) % 58.47/16.92 | % 58.47/16.92 | Applying alpha-rule on (163) yields: % 58.47/16.92 | (164) related(all_0_13_13, all_26_2_22, all_26_2_22) = all_78_0_35 % 58.47/16.92 | (165) in(all_26_2_22, all_0_10_10) = all_78_1_36 % 58.47/16.92 | (166) ~ (all_78_1_36 = 0) | all_78_0_35 = 0 % 58.47/16.92 | % 58.47/16.92 | Instantiating formula (50) with all_0_10_10, all_26_2_22 yields: % 58.47/16.92 | (167) ~ (in(all_26_2_22, all_0_10_10) = 0) | ? [v0] : ( ~ (v0 = 0) & in(all_0_10_10, all_26_2_22) = v0) % 58.47/16.92 | % 58.47/16.92 | Instantiating formula (33) with all_78_1_36, all_0_10_10, all_26_2_22 and discharging atoms in(all_26_2_22, all_0_10_10) = all_78_1_36, yields: % 58.47/16.92 | (168) all_78_1_36 = 0 | ? [v0] : ? [v1] : (element(all_26_2_22, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (168), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (161) all_78_1_36 = 0 % 58.47/16.92 | % 58.47/16.92 | From (161) and (165) follows: % 58.47/16.92 | (170) in(all_26_2_22, all_0_10_10) = 0 % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (167), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (171) ~ (in(all_26_2_22, all_0_10_10) = 0) % 58.47/16.92 | % 58.47/16.92 | Using (170) and (171) yields: % 58.47/16.92 | (151) $false % 58.47/16.92 | % 58.47/16.92 |-The branch is then unsatisfiable % 58.47/16.92 |-Branch two: % 58.47/16.92 | (170) in(all_26_2_22, all_0_10_10) = 0 % 58.47/16.92 | (174) ? [v0] : ( ~ (v0 = 0) & in(all_0_10_10, all_26_2_22) = v0) % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (31), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (175) ~ (all_0_9_9 = 0) % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (145), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (176) ~ (element(all_26_2_22, all_30_0_27) = 0) % 58.47/16.92 | % 58.47/16.92 | From (117) and (176) follows: % 58.47/16.92 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.92 | % 58.47/16.92 | Using (129) and (150) yields: % 58.47/16.92 | (151) $false % 58.47/16.92 | % 58.47/16.92 |-The branch is then unsatisfiable % 58.47/16.92 |-Branch two: % 58.47/16.92 | (179) element(all_26_2_22, all_30_0_27) = 0 % 58.47/16.92 | (180) all_0_9_9 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & related(all_0_13_13, v0, all_26_2_22) = v3 & element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0) | ( ~ (v0 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0)) % 58.47/16.92 | % 58.47/16.92 | From (117) and (179) follows: % 58.47/16.92 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (180), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (182) all_0_9_9 = 0 % 58.47/16.92 | % 58.47/16.92 | Equations (182) can reduce 175 to: % 58.47/16.92 | (81) $false % 58.47/16.92 | % 58.47/16.92 |-The branch is then unsatisfiable % 58.47/16.92 |-Branch two: % 58.47/16.92 | (175) ~ (all_0_9_9 = 0) % 58.47/16.92 | (185) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & related(all_0_13_13, v0, all_26_2_22) = v3 & element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0) | ( ~ (v0 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0)) % 58.47/16.92 | % 58.47/16.92 | Instantiating (185) with all_136_0_40, all_136_1_41, all_136_2_42, all_136_3_43 yields: % 58.47/16.92 | (186) (all_136_1_41 = 0 & all_136_2_42 = 0 & ~ (all_136_0_40 = 0) & related(all_0_13_13, all_136_3_43, all_26_2_22) = all_136_0_40 & element(all_136_3_43, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = 0) | ( ~ (all_136_3_43 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_136_3_43) % 58.47/16.92 | % 58.47/16.92 +-Applying beta-rule and splitting (186), into two cases. % 58.47/16.92 |-Branch one: % 58.47/16.92 | (187) all_136_1_41 = 0 & all_136_2_42 = 0 & ~ (all_136_0_40 = 0) & related(all_0_13_13, all_136_3_43, all_26_2_22) = all_136_0_40 & element(all_136_3_43, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = 0 % 58.47/16.92 | % 58.47/16.92 | Applying alpha-rule on (187) yields: % 58.47/16.92 | (188) relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = 0 % 58.47/16.92 | (189) related(all_0_13_13, all_136_3_43, all_26_2_22) = all_136_0_40 % 58.47/16.92 | (190) all_136_1_41 = 0 % 58.47/16.92 | (191) all_136_2_42 = 0 % 58.47/16.92 | (192) element(all_136_3_43, all_30_0_27) = 0 % 58.47/16.92 | (193) ~ (all_136_0_40 = 0) % 58.47/16.92 | % 58.47/16.92 | From (117) and (192) follows: % 58.47/16.92 | (194) element(all_136_3_43, all_0_10_10) = 0 % 58.47/16.92 | % 58.47/16.92 | Instantiating formula (141) with all_136_3_43, all_0_9_9, all_0_10_10 and discharging atoms ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = all_0_9_9, yields: % 58.47/16.92 | (195) all_0_9_9 = 0 | ~ (element(all_136_3_43, all_30_0_27) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & related(all_0_13_13, v0, all_136_3_43) = v3 & element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0) | ( ~ (v0 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = v0)) % 58.47/16.93 | % 58.47/16.93 | Instantiating formula (67) with all_136_3_43, all_26_2_22, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.93 | (196) ~ (element(all_136_3_43, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_136_3_43) = v1 & in(all_136_3_43, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 | Instantiating formula (67) with all_26_2_22, all_136_3_43, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = 0, yields: % 58.47/16.93 | (197) ~ (element(all_26_2_22, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_136_3_43, all_17_0_17) = v0) | (related(all_0_13_13, all_136_3_43, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 | Instantiating formula (67) with all_136_3_43, all_136_3_43, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = 0, yields: % 58.47/16.93 | (198) ~ (element(all_136_3_43, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_136_3_43, all_17_0_17) = v0) | (related(all_0_13_13, all_136_3_43, all_136_3_43) = v1 & in(all_136_3_43, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 +-Applying beta-rule and splitting (197), into two cases. % 58.47/16.93 |-Branch one: % 58.47/16.93 | (149) ~ (element(all_26_2_22, all_17_0_17) = 0) % 58.47/16.93 | % 58.47/16.93 | From (113) and (149) follows: % 58.47/16.93 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.93 | % 58.47/16.93 | Using (129) and (150) yields: % 58.47/16.93 | (151) $false % 58.47/16.93 | % 58.47/16.93 |-The branch is then unsatisfiable % 58.47/16.93 |-Branch two: % 58.47/16.93 | (152) element(all_26_2_22, all_17_0_17) = 0 % 58.47/16.93 | (203) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_136_3_43, all_17_0_17) = v0) | (related(all_0_13_13, all_136_3_43, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 | Instantiating (203) with all_184_0_44, all_184_1_45 yields: % 58.47/16.93 | (204) ( ~ (all_184_1_45 = 0) & element(all_136_3_43, all_17_0_17) = all_184_1_45) | (related(all_0_13_13, all_136_3_43, all_26_2_22) = all_184_0_44 & in(all_26_2_22, all_0_10_10) = all_184_1_45 & ( ~ (all_184_1_45 = 0) | all_184_0_44 = 0)) % 58.47/16.93 | % 58.47/16.93 +-Applying beta-rule and splitting (198), into two cases. % 58.47/16.93 |-Branch one: % 58.47/16.93 | (205) ~ (element(all_136_3_43, all_17_0_17) = 0) % 58.47/16.93 | % 58.47/16.93 | From (113) and (205) follows: % 58.47/16.93 | (206) ~ (element(all_136_3_43, all_0_10_10) = 0) % 58.47/16.93 | % 58.47/16.93 | Using (194) and (206) yields: % 58.47/16.93 | (151) $false % 58.47/16.93 | % 58.47/16.93 |-The branch is then unsatisfiable % 58.47/16.93 |-Branch two: % 58.47/16.93 | (208) element(all_136_3_43, all_17_0_17) = 0 % 58.47/16.93 | (209) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_136_3_43, all_17_0_17) = v0) | (related(all_0_13_13, all_136_3_43, all_136_3_43) = v1 & in(all_136_3_43, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 | From (113) and (208) follows: % 58.47/16.93 | (194) element(all_136_3_43, all_0_10_10) = 0 % 58.47/16.93 | % 58.47/16.93 +-Applying beta-rule and splitting (204), into two cases. % 58.47/16.93 |-Branch one: % 58.47/16.93 | (211) ~ (all_184_1_45 = 0) & element(all_136_3_43, all_17_0_17) = all_184_1_45 % 58.47/16.93 | % 58.47/16.93 | Applying alpha-rule on (211) yields: % 58.47/16.93 | (212) ~ (all_184_1_45 = 0) % 58.47/16.93 | (213) element(all_136_3_43, all_17_0_17) = all_184_1_45 % 58.47/16.93 | % 58.47/16.93 | From (113) and (213) follows: % 58.47/16.93 | (214) element(all_136_3_43, all_0_10_10) = all_184_1_45 % 58.47/16.93 | % 58.47/16.93 +-Applying beta-rule and splitting (196), into two cases. % 58.47/16.93 |-Branch one: % 58.47/16.93 | (205) ~ (element(all_136_3_43, all_17_0_17) = 0) % 58.47/16.93 | % 58.47/16.93 | From (113) and (205) follows: % 58.47/16.93 | (206) ~ (element(all_136_3_43, all_0_10_10) = 0) % 58.47/16.93 | % 58.47/16.93 | Using (194) and (206) yields: % 58.47/16.93 | (151) $false % 58.47/16.93 | % 58.47/16.93 |-The branch is then unsatisfiable % 58.47/16.93 |-Branch two: % 58.47/16.93 | (208) element(all_136_3_43, all_17_0_17) = 0 % 58.47/16.93 | (219) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_136_3_43) = v1 & in(all_136_3_43, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.93 | % 58.47/16.93 | From (113) and (208) follows: % 58.47/16.93 | (194) element(all_136_3_43, all_0_10_10) = 0 % 58.47/16.93 | % 58.47/16.93 +-Applying beta-rule and splitting (195), into two cases. % 58.47/16.93 |-Branch one: % 58.47/16.93 | (221) ~ (element(all_136_3_43, all_30_0_27) = 0) % 58.47/16.93 | % 58.47/16.93 | From (117) and (221) follows: % 58.47/16.93 | (206) ~ (element(all_136_3_43, all_0_10_10) = 0) % 58.47/16.93 | % 58.47/16.93 | Using (194) and (206) yields: % 58.47/16.93 | (151) $false % 58.47/16.93 | % 58.47/16.93 |-The branch is then unsatisfiable % 58.47/16.93 |-Branch two: % 58.47/16.93 | (192) element(all_136_3_43, all_30_0_27) = 0 % 58.47/16.93 | (225) all_0_9_9 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & related(all_0_13_13, v0, all_136_3_43) = v3 & element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0) | ( ~ (v0 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_136_3_43) = v0)) % 58.47/16.93 | % 58.47/16.93 | From (117) and (192) follows: % 58.47/16.93 | (194) element(all_136_3_43, all_0_10_10) = 0 % 58.47/16.93 | % 58.47/16.93 | Instantiating formula (11) with all_136_3_43, all_0_10_10, all_184_1_45, 0 and discharging atoms element(all_136_3_43, all_0_10_10) = all_184_1_45, element(all_136_3_43, all_0_10_10) = 0, yields: % 58.47/16.93 | (227) all_184_1_45 = 0 % 58.47/16.93 | % 58.47/16.93 | Equations (227) can reduce 212 to: % 58.47/16.93 | (81) $false % 58.47/16.93 | % 58.47/16.93 |-The branch is then unsatisfiable % 58.47/16.93 |-Branch two: % 58.47/16.93 | (229) related(all_0_13_13, all_136_3_43, all_26_2_22) = all_184_0_44 & in(all_26_2_22, all_0_10_10) = all_184_1_45 & ( ~ (all_184_1_45 = 0) | all_184_0_44 = 0) % 58.47/16.93 | % 58.47/16.93 | Applying alpha-rule on (229) yields: % 58.47/16.93 | (230) related(all_0_13_13, all_136_3_43, all_26_2_22) = all_184_0_44 % 58.47/16.93 | (231) in(all_26_2_22, all_0_10_10) = all_184_1_45 % 58.47/16.93 | (232) ~ (all_184_1_45 = 0) | all_184_0_44 = 0 % 58.47/16.93 | % 58.47/16.93 | Instantiating formula (21) with all_0_13_13, all_136_3_43, all_26_2_22, all_184_0_44, all_136_0_40 and discharging atoms related(all_0_13_13, all_136_3_43, all_26_2_22) = all_184_0_44, related(all_0_13_13, all_136_3_43, all_26_2_22) = all_136_0_40, yields: % 58.47/16.93 | (233) all_184_0_44 = all_136_0_40 % 58.47/16.94 | % 58.47/16.94 | Instantiating formula (27) with all_26_2_22, all_0_10_10, all_184_1_45, 0 and discharging atoms in(all_26_2_22, all_0_10_10) = all_184_1_45, in(all_26_2_22, all_0_10_10) = 0, yields: % 58.47/16.94 | (227) all_184_1_45 = 0 % 58.47/16.94 | % 58.47/16.94 +-Applying beta-rule and splitting (232), into two cases. % 58.47/16.94 |-Branch one: % 58.47/16.94 | (212) ~ (all_184_1_45 = 0) % 58.47/16.94 | % 58.47/16.94 | Equations (227) can reduce 212 to: % 58.47/16.94 | (81) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (227) all_184_1_45 = 0 % 58.47/16.94 | (238) all_184_0_44 = 0 % 58.47/16.94 | % 58.47/16.94 | Combining equations (238,233) yields a new equation: % 58.47/16.94 | (239) all_136_0_40 = 0 % 58.47/16.94 | % 58.47/16.94 | Equations (239) can reduce 193 to: % 58.47/16.94 | (81) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (241) ~ (all_136_3_43 = 0) & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_136_3_43 % 58.47/16.94 | % 58.47/16.94 | Applying alpha-rule on (241) yields: % 58.47/16.94 | (242) ~ (all_136_3_43 = 0) % 58.47/16.94 | (243) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_136_3_43 % 58.47/16.94 | % 58.47/16.94 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_136_3_43, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_136_3_43, relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.94 | (244) all_136_3_43 = 0 % 58.47/16.94 | % 58.47/16.94 | Equations (244) can reduce 242 to: % 58.47/16.94 | (81) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (182) all_0_9_9 = 0 % 58.47/16.94 | (247) ~ (all_0_11_11 = 0) % 58.47/16.94 | % 58.47/16.94 | From (182) and (9) follows: % 58.47/16.94 | (248) ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = 0 % 58.47/16.94 | % 58.47/16.94 +-Applying beta-rule and splitting (143), into two cases. % 58.47/16.94 |-Branch one: % 58.47/16.94 | (249) ~ (ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = 0) % 58.47/16.94 | % 58.47/16.94 | Using (248) and (249) yields: % 58.47/16.94 | (151) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (248) ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = 0 % 58.47/16.94 | (252) ? [v0] : (element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0 & ! [v1] : ( ~ (element(v1, all_30_0_27) = 0) | ? [v2] : ? [v3] : (related(all_0_13_13, v1, v0) = v3 & relstr_element_smaller(all_0_13_13, all_0_10_10, v1) = v2 & ( ~ (v2 = 0) | v3 = 0)))) % 58.47/16.94 | % 58.47/16.94 | Instantiating (252) with all_127_0_70 yields: % 58.47/16.94 | (253) element(all_127_0_70, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0 & ! [v0] : ( ~ (element(v0, all_30_0_27) = 0) | ? [v1] : ? [v2] : (related(all_0_13_13, v0, all_127_0_70) = v2 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 58.47/16.94 | % 58.47/16.94 | Applying alpha-rule on (253) yields: % 58.47/16.94 | (254) element(all_127_0_70, all_30_0_27) = 0 % 58.47/16.94 | (255) relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0 % 58.47/16.94 | (256) ! [v0] : ( ~ (element(v0, all_30_0_27) = 0) | ? [v1] : ? [v2] : (related(all_0_13_13, v0, all_127_0_70) = v2 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 58.47/16.94 | % 58.47/16.94 | Instantiating formula (256) with all_26_2_22 yields: % 58.47/16.94 | (257) ~ (element(all_26_2_22, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_26_2_22, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.94 | % 58.47/16.94 | From (117) and (254) follows: % 58.47/16.94 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.94 | % 58.47/16.94 +-Applying beta-rule and splitting (146), into two cases. % 58.47/16.94 |-Branch one: % 58.47/16.94 | (259) ~ (element(all_26_2_22, all_28_0_25) = 0) % 58.47/16.94 | % 58.47/16.94 | From (93) and (259) follows: % 58.47/16.94 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.94 | % 58.47/16.94 | Using (129) and (150) yields: % 58.47/16.94 | (151) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (262) element(all_26_2_22, all_28_0_25) = 0 % 58.47/16.94 | (263) all_0_11_11 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_26_2_22, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = v0)) % 58.47/16.94 | % 58.47/16.94 | From (93) and (262) follows: % 58.47/16.94 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.94 | % 58.47/16.94 +-Applying beta-rule and splitting (257), into two cases. % 58.47/16.94 |-Branch one: % 58.47/16.94 | (176) ~ (element(all_26_2_22, all_30_0_27) = 0) % 58.47/16.94 | % 58.47/16.94 | From (117) and (176) follows: % 58.47/16.94 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.94 | % 58.47/16.94 | Using (129) and (150) yields: % 58.47/16.94 | (151) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (179) element(all_26_2_22, all_30_0_27) = 0 % 58.47/16.94 | (269) ? [v0] : ? [v1] : (related(all_0_13_13, all_26_2_22, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.94 | % 58.47/16.94 | Instantiating (269) with all_142_0_73, all_142_1_74 yields: % 58.47/16.94 | (270) related(all_0_13_13, all_26_2_22, all_127_0_70) = all_142_0_73 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_142_1_74 & ( ~ (all_142_1_74 = 0) | all_142_0_73 = 0) % 58.47/16.94 | % 58.47/16.94 | Applying alpha-rule on (270) yields: % 58.47/16.94 | (271) related(all_0_13_13, all_26_2_22, all_127_0_70) = all_142_0_73 % 58.47/16.94 | (272) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_142_1_74 % 58.47/16.94 | (273) ~ (all_142_1_74 = 0) | all_142_0_73 = 0 % 58.47/16.94 | % 58.47/16.94 | From (117) and (179) follows: % 58.47/16.94 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.94 | % 58.47/16.94 +-Applying beta-rule and splitting (263), into two cases. % 58.47/16.94 |-Branch one: % 58.47/16.94 | (275) all_0_11_11 = 0 % 58.47/16.94 | % 58.47/16.94 | Equations (275) can reduce 247 to: % 58.47/16.94 | (81) $false % 58.47/16.94 | % 58.47/16.94 |-The branch is then unsatisfiable % 58.47/16.94 |-Branch two: % 58.47/16.94 | (247) ~ (all_0_11_11 = 0) % 58.47/16.94 | (278) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_26_2_22, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = v0)) % 58.47/16.94 | % 58.47/16.94 | Instantiating (278) with all_148_0_75, all_148_1_76, all_148_2_77, all_148_3_78 yields: % 58.47/16.94 | (279) (all_148_1_76 = 0 & all_148_2_77 = 0 & ~ (all_148_0_75 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = 0 & related(all_0_13_13, all_26_2_22, all_148_3_78) = all_148_0_75 & element(all_148_3_78, all_28_0_25) = 0) | ( ~ (all_148_3_78 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = all_148_3_78) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_142_1_74, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_142_1_74, relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.95 | (280) all_142_1_74 = 0 % 58.47/16.95 | % 58.47/16.95 | From (280) and (272) follows: % 58.47/16.95 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (142) with all_0_10_10 and discharging atoms ex_inf_of_relstr_set(all_0_13_13, all_0_10_10) = 0, yields: % 58.47/16.95 | (252) ? [v0] : (element(v0, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = 0 & ! [v1] : ( ~ (element(v1, all_30_0_27) = 0) | ? [v2] : ? [v3] : (related(all_0_13_13, v1, v0) = v3 & relstr_element_smaller(all_0_13_13, all_0_10_10, v1) = v2 & ( ~ (v2 = 0) | v3 = 0)))) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (256) with all_127_0_70 yields: % 58.47/16.95 | (283) ~ (element(all_127_0_70, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_127_0_70, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (135) with all_127_0_70, all_0_11_11, empty_set and discharging atoms ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11, yields: % 58.47/16.95 | (284) all_0_11_11 = 0 | ~ (element(all_127_0_70, all_28_0_25) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_127_0_70, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = v0)) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (67) with all_127_0_70, all_26_2_22, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.95 | (285) ~ (element(all_127_0_70, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (67) with all_26_2_22, all_127_0_70, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0, yields: % 58.47/16.95 | (286) ~ (element(all_26_2_22, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (67) with all_127_0_70, all_127_0_70, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0, yields: % 58.47/16.95 | (287) ~ (element(all_127_0_70, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | Instantiating (252) with all_194_0_79 yields: % 58.47/16.95 | (288) element(all_194_0_79, all_30_0_27) = 0 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0 & ! [v0] : ( ~ (element(v0, all_30_0_27) = 0) | ? [v1] : ? [v2] : (related(all_0_13_13, v0, all_194_0_79) = v2 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 58.47/16.95 | % 58.47/16.95 | Applying alpha-rule on (288) yields: % 58.47/16.95 | (289) element(all_194_0_79, all_30_0_27) = 0 % 58.47/16.95 | (290) relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0 % 58.47/16.95 | (291) ! [v0] : ( ~ (element(v0, all_30_0_27) = 0) | ? [v1] : ? [v2] : (related(all_0_13_13, v0, all_194_0_79) = v2 & relstr_element_smaller(all_0_13_13, all_0_10_10, v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (291) with all_127_0_70 yields: % 58.47/16.95 | (292) ~ (element(all_127_0_70, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_127_0_70, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.95 | % 58.47/16.95 | Instantiating formula (291) with all_26_2_22 yields: % 58.47/16.95 | (293) ~ (element(all_26_2_22, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_26_2_22, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.95 | % 58.47/16.95 | From (117) and (289) follows: % 58.47/16.95 | (294) element(all_194_0_79, all_0_10_10) = 0 % 58.47/16.95 | % 58.47/16.95 +-Applying beta-rule and splitting (286), into two cases. % 58.47/16.95 |-Branch one: % 58.47/16.95 | (149) ~ (element(all_26_2_22, all_17_0_17) = 0) % 58.47/16.95 | % 58.47/16.95 | From (113) and (149) follows: % 58.47/16.95 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.95 | % 58.47/16.95 | Using (129) and (150) yields: % 58.47/16.95 | (151) $false % 58.47/16.95 | % 58.47/16.95 |-The branch is then unsatisfiable % 58.47/16.95 |-Branch two: % 58.47/16.95 | (152) element(all_26_2_22, all_17_0_17) = 0 % 58.47/16.95 | (299) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | From (113) and (152) follows: % 58.47/16.95 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.95 | % 58.47/16.95 +-Applying beta-rule and splitting (287), into two cases. % 58.47/16.95 |-Branch one: % 58.47/16.95 | (301) ~ (element(all_127_0_70, all_17_0_17) = 0) % 58.47/16.95 | % 58.47/16.95 | From (113) and (301) follows: % 58.47/16.95 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.95 | % 58.47/16.95 | Using (258) and (302) yields: % 58.47/16.95 | (151) $false % 58.47/16.95 | % 58.47/16.95 |-The branch is then unsatisfiable % 58.47/16.95 |-Branch two: % 58.47/16.95 | (304) element(all_127_0_70, all_17_0_17) = 0 % 58.47/16.95 | (305) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | From (113) and (304) follows: % 58.47/16.95 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.95 | % 58.47/16.95 +-Applying beta-rule and splitting (285), into two cases. % 58.47/16.95 |-Branch one: % 58.47/16.95 | (301) ~ (element(all_127_0_70, all_17_0_17) = 0) % 58.47/16.95 | % 58.47/16.95 | From (113) and (301) follows: % 58.47/16.95 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.95 | % 58.47/16.95 | Using (258) and (302) yields: % 58.47/16.95 | (151) $false % 58.47/16.95 | % 58.47/16.95 |-The branch is then unsatisfiable % 58.47/16.95 |-Branch two: % 58.47/16.95 | (304) element(all_127_0_70, all_17_0_17) = 0 % 58.47/16.95 | (311) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.95 | % 58.47/16.95 | From (113) and (304) follows: % 58.47/16.95 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.95 | % 58.47/16.95 +-Applying beta-rule and splitting (284), into two cases. % 58.47/16.95 |-Branch one: % 58.47/16.95 | (313) ~ (element(all_127_0_70, all_28_0_25) = 0) % 58.47/16.96 | % 58.47/16.96 | From (93) and (313) follows: % 58.47/16.96 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.96 | % 58.47/16.96 | Using (258) and (302) yields: % 58.47/16.96 | (151) $false % 58.47/16.96 | % 58.47/16.96 |-The branch is then unsatisfiable % 58.47/16.96 |-Branch two: % 58.47/16.96 | (316) element(all_127_0_70, all_28_0_25) = 0 % 58.47/16.96 | (317) all_0_11_11 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_127_0_70, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = v0)) % 58.47/16.96 | % 58.47/16.96 | From (93) and (316) follows: % 58.47/16.96 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.96 | % 58.47/16.96 +-Applying beta-rule and splitting (317), into two cases. % 58.47/16.96 |-Branch one: % 58.47/16.96 | (275) all_0_11_11 = 0 % 58.47/16.96 | % 58.47/16.96 | Equations (275) can reduce 247 to: % 58.47/16.96 | (81) $false % 58.47/16.96 | % 58.47/16.96 |-The branch is then unsatisfiable % 58.47/16.96 |-Branch two: % 58.47/16.96 | (247) ~ (all_0_11_11 = 0) % 58.47/16.96 | (322) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_127_0_70, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = v0)) % 58.47/16.96 | % 58.47/16.96 | Instantiating (322) with all_220_0_102, all_220_1_103, all_220_2_104, all_220_3_105 yields: % 58.47/16.96 | (323) (all_220_1_103 = 0 & all_220_2_104 = 0 & ~ (all_220_0_102 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = 0 & related(all_0_13_13, all_127_0_70, all_220_3_105) = all_220_0_102 & element(all_220_3_105, all_28_0_25) = 0) | ( ~ (all_220_3_105 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = all_220_3_105) % 58.47/16.96 | % 58.47/16.96 +-Applying beta-rule and splitting (293), into two cases. % 58.47/16.96 |-Branch one: % 58.47/16.96 | (176) ~ (element(all_26_2_22, all_30_0_27) = 0) % 58.47/16.96 | % 58.47/16.96 | From (117) and (176) follows: % 58.47/16.96 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.96 | % 58.47/16.96 | Using (129) and (150) yields: % 58.47/16.96 | (151) $false % 58.47/16.96 | % 58.47/16.96 |-The branch is then unsatisfiable % 58.47/16.96 |-Branch two: % 58.47/16.96 | (179) element(all_26_2_22, all_30_0_27) = 0 % 58.47/16.96 | (328) ? [v0] : ? [v1] : (related(all_0_13_13, all_26_2_22, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.96 | % 58.47/16.96 | Instantiating (328) with all_225_0_106, all_225_1_107 yields: % 58.47/16.96 | (329) related(all_0_13_13, all_26_2_22, all_194_0_79) = all_225_0_106 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_225_1_107 & ( ~ (all_225_1_107 = 0) | all_225_0_106 = 0) % 58.47/16.96 | % 58.47/16.96 | Applying alpha-rule on (329) yields: % 58.47/16.96 | (330) related(all_0_13_13, all_26_2_22, all_194_0_79) = all_225_0_106 % 58.47/16.96 | (331) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_225_1_107 % 58.47/16.96 | (332) ~ (all_225_1_107 = 0) | all_225_0_106 = 0 % 58.47/16.96 | % 58.47/16.96 | From (117) and (179) follows: % 58.47/16.96 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.96 | % 58.47/16.96 +-Applying beta-rule and splitting (283), into two cases. % 58.47/16.96 |-Branch one: % 58.47/16.96 | (334) ~ (element(all_127_0_70, all_30_0_27) = 0) % 58.47/16.96 | % 58.47/16.96 | From (117) and (334) follows: % 58.47/16.96 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.96 | % 58.47/16.96 | Using (258) and (302) yields: % 58.47/16.96 | (151) $false % 58.47/16.96 | % 58.47/16.96 |-The branch is then unsatisfiable % 58.47/16.96 |-Branch two: % 58.47/16.96 | (254) element(all_127_0_70, all_30_0_27) = 0 % 58.47/16.96 | (338) ? [v0] : ? [v1] : (related(all_0_13_13, all_127_0_70, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.96 | % 58.47/16.96 | Instantiating (338) with all_235_0_112, all_235_1_113 yields: % 58.47/16.96 | (339) related(all_0_13_13, all_127_0_70, all_127_0_70) = all_235_0_112 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_235_1_113 & ( ~ (all_235_1_113 = 0) | all_235_0_112 = 0) % 58.47/16.96 | % 58.47/16.96 | Applying alpha-rule on (339) yields: % 58.47/16.96 | (340) related(all_0_13_13, all_127_0_70, all_127_0_70) = all_235_0_112 % 58.47/16.96 | (341) relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_235_1_113 % 58.47/16.96 | (342) ~ (all_235_1_113 = 0) | all_235_0_112 = 0 % 58.47/16.96 | % 58.47/16.96 | From (117) and (254) follows: % 58.47/16.96 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.96 | % 58.47/16.96 +-Applying beta-rule and splitting (292), into two cases. % 58.47/16.96 |-Branch one: % 58.47/16.96 | (334) ~ (element(all_127_0_70, all_30_0_27) = 0) % 58.47/16.96 | % 58.47/16.96 | From (117) and (334) follows: % 58.47/16.96 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.96 | % 58.47/16.96 | Using (258) and (302) yields: % 58.47/16.96 | (151) $false % 58.47/16.96 | % 58.47/16.96 |-The branch is then unsatisfiable % 58.47/16.96 |-Branch two: % 58.47/16.96 | (254) element(all_127_0_70, all_30_0_27) = 0 % 58.47/16.96 | (348) ? [v0] : ? [v1] : (related(all_0_13_13, all_127_0_70, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.96 | % 58.47/16.96 | Instantiating (348) with all_245_0_116, all_245_1_117 yields: % 58.47/16.96 | (349) related(all_0_13_13, all_127_0_70, all_194_0_79) = all_245_0_116 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_245_1_117 & ( ~ (all_245_1_117 = 0) | all_245_0_116 = 0) % 58.47/16.96 | % 58.47/16.96 | Applying alpha-rule on (349) yields: % 58.47/16.96 | (350) related(all_0_13_13, all_127_0_70, all_194_0_79) = all_245_0_116 % 58.47/16.96 | (351) relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_245_1_117 % 58.47/16.96 | (352) ~ (all_245_1_117 = 0) | all_245_0_116 = 0 % 58.47/16.96 | % 58.47/16.96 | From (117) and (254) follows: % 58.47/16.96 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_127_0_70, all_245_1_117, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_245_1_117, relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0, yields: % 58.47/16.96 | (354) all_245_1_117 = 0 % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_245_1_117, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.96 | (355) all_245_1_117 = 0 | ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117) % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_235_1_113, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.96 | (356) all_235_1_113 = 0 | ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113) % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_127_0_70, all_235_1_113, all_245_1_117 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_245_1_117, relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = all_235_1_113, yields: % 58.47/16.96 | (357) all_245_1_117 = all_235_1_113 % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_225_1_107, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_225_1_107, relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.47/16.96 | (358) all_225_1_107 = 0 % 58.47/16.96 | % 58.47/16.96 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_225_1_107, all_245_1_117 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_225_1_107, yields: % 58.47/16.96 | (359) all_245_1_117 = all_225_1_107 | ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_26_2_22, all_225_1_107, all_235_1_113 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_225_1_107, yields: % 58.47/16.97 | (360) all_235_1_113 = all_225_1_107 | ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113) % 58.47/16.97 | % 58.47/16.97 | Combining equations (354,357) yields a new equation: % 58.47/16.97 | (361) all_235_1_113 = 0 % 58.47/16.97 | % 58.47/16.97 | Combining equations (361,357) yields a new equation: % 58.47/16.97 | (354) all_245_1_117 = 0 % 58.47/16.97 | % 58.47/16.97 | From (361) and (341) follows: % 58.47/16.97 | (255) relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0 % 58.47/16.97 | % 58.47/16.97 | From (358) and (331) follows: % 58.47/16.97 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (342), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (365) ~ (all_235_1_113 = 0) % 58.47/16.97 | % 58.47/16.97 | Equations (361) can reduce 365 to: % 58.47/16.97 | (81) $false % 58.47/16.97 | % 58.47/16.97 |-The branch is then unsatisfiable % 58.47/16.97 |-Branch two: % 58.47/16.97 | (361) all_235_1_113 = 0 % 58.47/16.97 | (368) all_235_0_112 = 0 % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (352), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (369) ~ (all_245_1_117 = 0) % 58.47/16.97 | % 58.47/16.97 | Equations (354) can reduce 369 to: % 58.47/16.97 | (81) $false % 58.47/16.97 | % 58.47/16.97 |-The branch is then unsatisfiable % 58.47/16.97 |-Branch two: % 58.47/16.97 | (354) all_245_1_117 = 0 % 58.47/16.97 | (372) all_245_0_116 = 0 % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (98), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (373) ~ (empty(empty_set) = all_41_0_32) % 58.47/16.97 | % 58.47/16.97 | Using (120) and (373) yields: % 58.47/16.97 | (374) ~ (all_0_10_10 = empty_set) % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (99), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (375) ~ (empty(all_41_1_33) = 0) % 58.47/16.97 | % 58.47/16.97 | From (118) and (375) follows: % 58.47/16.97 | (376) ~ (empty(all_0_10_10) = 0) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (291) with all_194_0_79 yields: % 58.47/16.97 | (377) ~ (element(all_194_0_79, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_194_0_79, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (256) with all_194_0_79 yields: % 58.47/16.97 | (378) ~ (element(all_194_0_79, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_194_0_79, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (135) with all_194_0_79, all_0_11_11, empty_set and discharging atoms ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11, yields: % 58.47/16.97 | (379) all_0_11_11 = 0 | ~ (element(all_194_0_79, all_28_0_25) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_194_0_79, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_194_0_79) = v0)) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (67) with all_127_0_70, all_194_0_79, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.47/16.97 | (380) ~ (element(all_127_0_70, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (67) with all_26_2_22, all_194_0_79, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.47/16.97 | (381) ~ (element(all_26_2_22, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 | Instantiating formula (67) with all_194_0_79, all_194_0_79, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.47/16.97 | (382) ~ (element(all_194_0_79, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_194_0_79) = v1 & in(all_194_0_79, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (381), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (149) ~ (element(all_26_2_22, all_17_0_17) = 0) % 58.47/16.97 | % 58.47/16.97 | From (113) and (149) follows: % 58.47/16.97 | (150) ~ (element(all_26_2_22, all_0_10_10) = 0) % 58.47/16.97 | % 58.47/16.97 | Using (129) and (150) yields: % 58.47/16.97 | (151) $false % 58.47/16.97 | % 58.47/16.97 |-The branch is then unsatisfiable % 58.47/16.97 |-Branch two: % 58.47/16.97 | (152) element(all_26_2_22, all_17_0_17) = 0 % 58.47/16.97 | (387) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_26_2_22) = v1 & in(all_26_2_22, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 | From (113) and (152) follows: % 58.47/16.97 | (129) element(all_26_2_22, all_0_10_10) = 0 % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (382), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (389) ~ (element(all_194_0_79, all_17_0_17) = 0) % 58.47/16.97 | % 58.47/16.97 | From (113) and (389) follows: % 58.47/16.97 | (390) ~ (element(all_194_0_79, all_0_10_10) = 0) % 58.47/16.97 | % 58.47/16.97 | Using (294) and (390) yields: % 58.47/16.97 | (151) $false % 58.47/16.97 | % 58.47/16.97 |-The branch is then unsatisfiable % 58.47/16.97 |-Branch two: % 58.47/16.97 | (392) element(all_194_0_79, all_17_0_17) = 0 % 58.47/16.97 | (393) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_194_0_79) = v1 & in(all_194_0_79, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 | From (113) and (392) follows: % 58.47/16.97 | (294) element(all_194_0_79, all_0_10_10) = 0 % 58.47/16.97 | % 58.47/16.97 +-Applying beta-rule and splitting (380), into two cases. % 58.47/16.97 |-Branch one: % 58.47/16.97 | (301) ~ (element(all_127_0_70, all_17_0_17) = 0) % 58.47/16.97 | % 58.47/16.97 | From (113) and (301) follows: % 58.47/16.97 | (302) ~ (element(all_127_0_70, all_0_10_10) = 0) % 58.47/16.97 | % 58.47/16.97 | Using (258) and (302) yields: % 58.47/16.97 | (151) $false % 58.47/16.97 | % 58.47/16.97 |-The branch is then unsatisfiable % 58.47/16.97 |-Branch two: % 58.47/16.97 | (304) element(all_127_0_70, all_17_0_17) = 0 % 58.47/16.97 | (399) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_127_0_70) = v1 & in(all_127_0_70, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.47/16.97 | % 58.47/16.97 | From (113) and (304) follows: % 58.47/16.97 | (258) element(all_127_0_70, all_0_10_10) = 0 % 58.47/16.98 | % 58.47/16.98 +-Applying beta-rule and splitting (378), into two cases. % 58.47/16.98 |-Branch one: % 58.47/16.98 | (401) ~ (element(all_194_0_79, all_30_0_27) = 0) % 58.47/16.98 | % 58.47/16.98 | From (117) and (401) follows: % 58.47/16.98 | (390) ~ (element(all_194_0_79, all_0_10_10) = 0) % 58.47/16.98 | % 58.47/16.98 | Using (294) and (390) yields: % 58.47/16.98 | (151) $false % 58.47/16.98 | % 58.47/16.98 |-The branch is then unsatisfiable % 58.47/16.98 |-Branch two: % 58.47/16.98 | (289) element(all_194_0_79, all_30_0_27) = 0 % 58.47/16.98 | (405) ? [v0] : ? [v1] : (related(all_0_13_13, all_194_0_79, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.47/16.98 | % 58.47/16.98 | Instantiating (405) with all_575_0_157, all_575_1_158 yields: % 58.47/16.98 | (406) related(all_0_13_13, all_194_0_79, all_127_0_70) = all_575_0_157 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_575_1_158 & ( ~ (all_575_1_158 = 0) | all_575_0_157 = 0) % 58.47/16.98 | % 58.47/16.98 | Applying alpha-rule on (406) yields: % 58.47/16.98 | (407) related(all_0_13_13, all_194_0_79, all_127_0_70) = all_575_0_157 % 58.47/16.98 | (408) relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_575_1_158 % 58.47/16.98 | (409) ~ (all_575_1_158 = 0) | all_575_0_157 = 0 % 58.47/16.98 | % 58.47/16.98 | From (117) and (289) follows: % 58.47/16.98 | (294) element(all_194_0_79, all_0_10_10) = 0 % 58.47/16.98 | % 58.47/16.98 +-Applying beta-rule and splitting (379), into two cases. % 58.47/16.98 |-Branch one: % 58.47/16.98 | (411) ~ (element(all_194_0_79, all_28_0_25) = 0) % 58.47/16.98 | % 58.47/16.98 | From (93) and (411) follows: % 58.47/16.98 | (390) ~ (element(all_194_0_79, all_0_10_10) = 0) % 58.47/16.98 | % 58.47/16.98 | Using (294) and (390) yields: % 58.47/16.98 | (151) $false % 58.47/16.98 | % 58.47/16.98 |-The branch is then unsatisfiable % 58.47/16.98 |-Branch two: % 58.47/16.98 | (414) element(all_194_0_79, all_28_0_25) = 0 % 58.47/16.98 | (415) all_0_11_11 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_194_0_79, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_194_0_79) = v0)) % 58.47/16.98 | % 58.47/16.98 | From (93) and (414) follows: % 58.47/16.98 | (294) element(all_194_0_79, all_0_10_10) = 0 % 58.47/16.98 | % 58.47/16.98 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_194_0_79, all_575_1_158, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_575_1_158, relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.47/16.98 | (417) all_575_1_158 = 0 % 58.47/16.98 | % 58.47/16.98 | From (417) and (408) follows: % 58.47/16.98 | (290) relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0 % 58.47/16.98 | % 58.47/16.98 +-Applying beta-rule and splitting (377), into two cases. % 58.47/16.98 |-Branch one: % 58.47/16.98 | (401) ~ (element(all_194_0_79, all_30_0_27) = 0) % 58.47/16.98 | % 58.47/16.98 | From (117) and (401) follows: % 58.89/16.98 | (390) ~ (element(all_194_0_79, all_0_10_10) = 0) % 58.89/16.98 | % 58.89/16.98 | Using (294) and (390) yields: % 58.89/16.98 | (151) $false % 58.89/16.98 | % 58.89/16.98 |-The branch is then unsatisfiable % 58.89/16.98 |-Branch two: % 58.89/16.98 | (289) element(all_194_0_79, all_30_0_27) = 0 % 58.89/16.98 | (423) ? [v0] : ? [v1] : (related(all_0_13_13, all_194_0_79, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.89/16.98 | % 58.89/16.98 | Instantiating (423) with all_602_0_164, all_602_1_165 yields: % 58.89/16.98 | (424) related(all_0_13_13, all_194_0_79, all_194_0_79) = all_602_0_164 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_602_1_165 & ( ~ (all_602_1_165 = 0) | all_602_0_164 = 0) % 58.89/16.98 | % 58.89/16.98 | Applying alpha-rule on (424) yields: % 58.89/16.98 | (425) related(all_0_13_13, all_194_0_79, all_194_0_79) = all_602_0_164 % 58.89/16.98 | (426) relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_602_1_165 % 58.89/16.98 | (427) ~ (all_602_1_165 = 0) | all_602_0_164 = 0 % 58.89/16.98 | % 58.89/16.98 | From (117) and (289) follows: % 58.89/16.98 | (294) element(all_194_0_79, all_0_10_10) = 0 % 58.89/16.98 | % 58.89/16.98 | Instantiating formula (2) with all_0_13_13, all_0_10_10, all_194_0_79, all_602_1_165, 0 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = all_602_1_165, relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.89/16.98 | (429) all_602_1_165 = 0 % 58.89/16.98 | % 58.89/16.98 | From (429) and (426) follows: % 58.89/16.98 | (290) relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0 % 58.89/16.98 | % 58.89/16.98 +-Applying beta-rule and splitting (279), into two cases. % 58.89/16.98 |-Branch one: % 58.90/16.98 | (431) all_148_1_76 = 0 & all_148_2_77 = 0 & ~ (all_148_0_75 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = 0 & related(all_0_13_13, all_26_2_22, all_148_3_78) = all_148_0_75 & element(all_148_3_78, all_28_0_25) = 0 % 58.90/16.98 | % 58.90/16.98 | Applying alpha-rule on (431) yields: % 58.90/16.98 | (432) related(all_0_13_13, all_26_2_22, all_148_3_78) = all_148_0_75 % 58.90/16.98 | (433) ~ (all_148_0_75 = 0) % 58.90/16.98 | (434) all_148_2_77 = 0 % 58.90/16.98 | (435) element(all_148_3_78, all_28_0_25) = 0 % 58.90/16.98 | (436) all_148_1_76 = 0 % 58.90/16.98 | (437) relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = 0 % 58.90/16.98 | % 58.90/16.98 | From (93) and (435) follows: % 58.90/16.98 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.90/16.98 | % 58.90/16.98 +-Applying beta-rule and splitting (323), into two cases. % 58.90/16.98 |-Branch one: % 58.90/16.98 | (439) all_220_1_103 = 0 & all_220_2_104 = 0 & ~ (all_220_0_102 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = 0 & related(all_0_13_13, all_127_0_70, all_220_3_105) = all_220_0_102 & element(all_220_3_105, all_28_0_25) = 0 % 58.90/16.98 | % 58.90/16.98 | Applying alpha-rule on (439) yields: % 58.90/16.98 | (440) all_220_1_103 = 0 % 58.90/16.98 | (441) relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = 0 % 58.90/16.98 | (442) related(all_0_13_13, all_127_0_70, all_220_3_105) = all_220_0_102 % 58.90/16.98 | (443) all_220_2_104 = 0 % 58.90/16.98 | (444) ~ (all_220_0_102 = 0) % 58.90/16.98 | (445) element(all_220_3_105, all_28_0_25) = 0 % 58.90/16.98 | % 58.90/16.98 | From (93) and (445) follows: % 58.90/16.98 | (446) element(all_220_3_105, all_0_10_10) = 0 % 58.90/16.98 | % 58.90/16.98 +-Applying beta-rule and splitting (360), into two cases. % 58.90/16.98 |-Branch one: % 58.90/16.98 | (447) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113) % 58.90/16.98 | % 58.90/16.98 | From (361) and (447) follows: % 58.90/16.98 | (448) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0) % 58.90/16.98 | % 58.90/16.99 | Using (130) and (448) yields: % 58.90/16.99 | (151) $false % 58.90/16.99 | % 58.90/16.99 |-The branch is then unsatisfiable % 58.90/16.99 |-Branch two: % 58.90/16.99 | (450) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113 % 58.90/16.99 | (451) all_235_1_113 = all_225_1_107 % 58.90/16.99 | % 58.90/16.99 | Combining equations (361,451) yields a new equation: % 58.90/16.99 | (358) all_225_1_107 = 0 % 58.90/16.99 | % 58.90/16.99 | Combining equations (358,451) yields a new equation: % 58.90/16.99 | (361) all_235_1_113 = 0 % 58.90/16.99 | % 58.90/16.99 | From (361) and (450) follows: % 58.90/16.99 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.90/16.99 | % 58.90/16.99 +-Applying beta-rule and splitting (356), into two cases. % 58.90/16.99 |-Branch one: % 58.90/16.99 | (447) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113) % 58.90/16.99 | % 58.90/16.99 | From (361) and (447) follows: % 58.90/16.99 | (448) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0) % 58.90/16.99 | % 58.90/16.99 | Using (130) and (448) yields: % 58.90/16.99 | (151) $false % 58.90/16.99 | % 58.90/16.99 |-The branch is then unsatisfiable % 58.90/16.99 |-Branch two: % 58.90/16.99 | (450) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_235_1_113 % 58.90/16.99 | (361) all_235_1_113 = 0 % 58.90/16.99 | % 58.90/16.99 | From (361) and (450) follows: % 58.90/16.99 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.90/16.99 | % 58.90/16.99 +-Applying beta-rule and splitting (359), into two cases. % 58.90/16.99 |-Branch one: % 58.90/16.99 | (461) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117) % 58.90/16.99 | % 58.90/16.99 | From (354) and (461) follows: % 58.90/16.99 | (448) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0) % 58.90/16.99 | % 58.90/16.99 | Using (130) and (448) yields: % 58.90/16.99 | (151) $false % 58.90/16.99 | % 58.90/16.99 |-The branch is then unsatisfiable % 58.90/16.99 |-Branch two: % 58.90/16.99 | (464) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117 % 58.90/16.99 | (465) all_245_1_117 = all_225_1_107 % 58.90/16.99 | % 58.90/16.99 | From (354) and (464) follows: % 58.90/16.99 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.90/16.99 | % 58.90/16.99 +-Applying beta-rule and splitting (355), into two cases. % 58.90/16.99 |-Branch one: % 58.90/16.99 | (461) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117) % 58.90/16.99 | % 58.90/16.99 | From (354) and (461) follows: % 58.90/16.99 | (448) ~ (relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0) % 58.90/16.99 | % 58.90/16.99 | Using (130) and (448) yields: % 58.90/16.99 | (151) $false % 58.90/16.99 | % 58.90/16.99 |-The branch is then unsatisfiable % 58.90/16.99 |-Branch two: % 58.90/16.99 | (464) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = all_245_1_117 % 58.90/16.99 | (354) all_245_1_117 = 0 % 58.90/16.99 | % 58.90/16.99 | From (354) and (464) follows: % 58.90/16.99 | (130) relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0 % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (63) with 0, all_220_3_105 and discharging atoms relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = 0, yields: % 58.90/16.99 | (473) ? [v0] : ? [v1] : (element(all_220_3_105, all_14_0_16) = v0 & relstr_element_smaller(all_0_13_13, empty_set, all_220_3_105) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (63) with 0, all_148_3_78 and discharging atoms relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = 0, yields: % 58.90/16.99 | (474) ? [v0] : ? [v1] : (element(all_148_3_78, all_14_0_16) = v0 & relstr_element_smaller(all_0_13_13, empty_set, all_148_3_78) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (291) with all_220_3_105 yields: % 58.90/16.99 | (475) ~ (element(all_220_3_105, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_220_3_105, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_220_3_105) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (256) with all_220_3_105 yields: % 58.90/16.99 | (476) ~ (element(all_220_3_105, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_220_3_105, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_220_3_105) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (135) with all_220_3_105, all_0_11_11, empty_set and discharging atoms ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11, yields: % 58.90/16.99 | (477) all_0_11_11 = 0 | ~ (element(all_220_3_105, all_28_0_25) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_220_3_105, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = v0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (67) with all_220_3_105, all_194_0_79, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.90/16.99 | (478) ~ (element(all_220_3_105, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (67) with all_220_3_105, all_127_0_70, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0, yields: % 58.90/16.99 | (479) ~ (element(all_220_3_105, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (67) with all_220_3_105, all_26_2_22, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.90/16.99 | (480) ~ (element(all_220_3_105, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (291) with all_148_3_78 yields: % 58.90/16.99 | (481) ~ (element(all_148_3_78, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_148_3_78, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_148_3_78) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (256) with all_148_3_78 yields: % 58.90/16.99 | (482) ~ (element(all_148_3_78, all_30_0_27) = 0) | ? [v0] : ? [v1] : (related(all_0_13_13, all_148_3_78, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_148_3_78) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (135) with all_148_3_78, all_0_11_11, empty_set and discharging atoms ex_sup_of_relstr_set(all_0_13_13, empty_set) = all_0_11_11, yields: % 58.90/16.99 | (483) all_0_11_11 = 0 | ~ (element(all_148_3_78, all_28_0_25) = 0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_148_3_78, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = v0)) % 58.90/16.99 | % 58.90/16.99 | Instantiating formula (67) with all_148_3_78, all_194_0_79, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_194_0_79) = 0, yields: % 58.90/16.99 | (484) ~ (element(all_148_3_78, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/17.00 | % 58.90/17.00 | Instantiating formula (67) with all_148_3_78, all_127_0_70, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_127_0_70) = 0, yields: % 58.90/17.00 | (485) ~ (element(all_148_3_78, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/17.00 | % 58.90/17.00 | Instantiating formula (67) with all_148_3_78, all_26_2_22, all_0_10_10 and discharging atoms relstr_element_smaller(all_0_13_13, all_0_10_10, all_26_2_22) = 0, yields: % 58.90/17.00 | (486) ~ (element(all_148_3_78, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.90/17.00 | % 58.90/17.00 | Instantiating (474) with all_841_0_166, all_841_1_167 yields: % 58.90/17.00 | (487) element(all_148_3_78, all_14_0_16) = all_841_1_167 & relstr_element_smaller(all_0_13_13, empty_set, all_148_3_78) = all_841_0_166 & ( ~ (all_841_1_167 = 0) | all_841_0_166 = 0) % 58.90/17.00 | % 58.90/17.00 | Applying alpha-rule on (487) yields: % 58.90/17.00 | (488) element(all_148_3_78, all_14_0_16) = all_841_1_167 % 58.90/17.00 | (489) relstr_element_smaller(all_0_13_13, empty_set, all_148_3_78) = all_841_0_166 % 58.90/17.00 | (490) ~ (all_841_1_167 = 0) | all_841_0_166 = 0 % 58.90/17.00 | % 58.90/17.00 | Instantiating (473) with all_843_0_168, all_843_1_169 yields: % 58.90/17.00 | (491) element(all_220_3_105, all_14_0_16) = all_843_1_169 & relstr_element_smaller(all_0_13_13, empty_set, all_220_3_105) = all_843_0_168 & ( ~ (all_843_1_169 = 0) | all_843_0_168 = 0) % 58.90/17.00 | % 58.96/17.00 | Applying alpha-rule on (491) yields: % 58.96/17.00 | (492) element(all_220_3_105, all_14_0_16) = all_843_1_169 % 58.96/17.00 | (493) relstr_element_smaller(all_0_13_13, empty_set, all_220_3_105) = all_843_0_168 % 58.96/17.00 | (494) ~ (all_843_1_169 = 0) | all_843_0_168 = 0 % 58.96/17.00 | % 58.96/17.00 | From (114) and (492) follows: % 58.96/17.00 | (495) element(all_220_3_105, all_0_10_10) = all_843_1_169 % 58.96/17.00 | % 58.96/17.00 | From (114) and (488) follows: % 58.96/17.00 | (496) element(all_148_3_78, all_0_10_10) = all_841_1_167 % 58.96/17.00 | % 58.96/17.00 +-Applying beta-rule and splitting (475), into two cases. % 58.96/17.00 |-Branch one: % 58.96/17.00 | (497) ~ (element(all_220_3_105, all_30_0_27) = 0) % 58.96/17.00 | % 58.96/17.00 | From (117) and (497) follows: % 58.96/17.00 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 58.96/17.00 | % 58.96/17.00 | Using (446) and (498) yields: % 58.96/17.00 | (151) $false % 58.96/17.00 | % 58.96/17.00 |-The branch is then unsatisfiable % 58.96/17.00 |-Branch two: % 58.96/17.00 | (500) element(all_220_3_105, all_30_0_27) = 0 % 58.96/17.00 | (501) ? [v0] : ? [v1] : (related(all_0_13_13, all_220_3_105, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_220_3_105) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.96/17.00 | % 58.96/17.00 | From (117) and (500) follows: % 58.96/17.00 | (446) element(all_220_3_105, all_0_10_10) = 0 % 58.96/17.00 | % 58.96/17.00 +-Applying beta-rule and splitting (476), into two cases. % 58.96/17.00 |-Branch one: % 58.96/17.00 | (497) ~ (element(all_220_3_105, all_30_0_27) = 0) % 58.96/17.00 | % 58.96/17.00 | From (117) and (497) follows: % 58.96/17.00 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 58.96/17.00 | % 58.96/17.00 | Using (446) and (498) yields: % 58.96/17.00 | (151) $false % 58.96/17.00 | % 58.96/17.00 |-The branch is then unsatisfiable % 58.96/17.00 |-Branch two: % 58.96/17.00 | (500) element(all_220_3_105, all_30_0_27) = 0 % 58.96/17.00 | (507) ? [v0] : ? [v1] : (related(all_0_13_13, all_220_3_105, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_220_3_105) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.96/17.00 | % 58.96/17.00 | From (117) and (500) follows: % 58.96/17.00 | (446) element(all_220_3_105, all_0_10_10) = 0 % 58.96/17.00 | % 58.96/17.00 +-Applying beta-rule and splitting (481), into two cases. % 58.96/17.00 |-Branch one: % 58.96/17.00 | (509) ~ (element(all_148_3_78, all_30_0_27) = 0) % 58.96/17.00 | % 58.96/17.00 | From (117) and (509) follows: % 58.96/17.00 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.00 | % 58.96/17.00 | Using (438) and (510) yields: % 58.96/17.00 | (151) $false % 58.96/17.00 | % 58.96/17.00 |-The branch is then unsatisfiable % 58.96/17.00 |-Branch two: % 58.96/17.00 | (512) element(all_148_3_78, all_30_0_27) = 0 % 58.96/17.00 | (513) ? [v0] : ? [v1] : (related(all_0_13_13, all_148_3_78, all_194_0_79) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_148_3_78) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.96/17.00 | % 58.96/17.00 | From (117) and (512) follows: % 58.96/17.00 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.00 | % 58.96/17.00 +-Applying beta-rule and splitting (482), into two cases. % 58.96/17.00 |-Branch one: % 58.96/17.00 | (509) ~ (element(all_148_3_78, all_30_0_27) = 0) % 58.96/17.00 | % 58.96/17.00 | From (117) and (509) follows: % 58.96/17.00 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.00 | % 58.96/17.00 | Using (438) and (510) yields: % 58.96/17.00 | (151) $false % 58.96/17.00 | % 58.96/17.00 |-The branch is then unsatisfiable % 58.96/17.00 |-Branch two: % 58.96/17.00 | (512) element(all_148_3_78, all_30_0_27) = 0 % 58.96/17.00 | (519) ? [v0] : ? [v1] : (related(all_0_13_13, all_148_3_78, all_127_0_70) = v1 & relstr_element_smaller(all_0_13_13, all_0_10_10, all_148_3_78) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 58.96/17.00 | % 58.96/17.00 | From (117) and (512) follows: % 58.96/17.00 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.00 | % 58.96/17.00 +-Applying beta-rule and splitting (484), into two cases. % 58.96/17.00 |-Branch one: % 58.96/17.00 | (521) ~ (element(all_148_3_78, all_17_0_17) = 0) % 58.96/17.00 | % 58.96/17.00 | From (113) and (521) follows: % 58.96/17.00 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.00 | % 58.96/17.01 | Using (438) and (510) yields: % 58.96/17.01 | (151) $false % 58.96/17.01 | % 58.96/17.01 |-The branch is then unsatisfiable % 58.96/17.01 |-Branch two: % 58.96/17.01 | (524) element(all_148_3_78, all_17_0_17) = 0 % 58.96/17.01 | (525) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.96/17.01 | % 58.96/17.01 | Instantiating (525) with all_872_0_178, all_872_1_179 yields: % 58.96/17.01 | (526) ( ~ (all_872_1_179 = 0) & element(all_194_0_79, all_17_0_17) = all_872_1_179) | (related(all_0_13_13, all_194_0_79, all_148_3_78) = all_872_0_178 & in(all_148_3_78, all_0_10_10) = all_872_1_179 & ( ~ (all_872_1_179 = 0) | all_872_0_178 = 0)) % 58.96/17.01 | % 58.96/17.01 | From (113) and (524) follows: % 58.96/17.01 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.01 | % 58.96/17.01 +-Applying beta-rule and splitting (485), into two cases. % 58.96/17.01 |-Branch one: % 58.96/17.01 | (521) ~ (element(all_148_3_78, all_17_0_17) = 0) % 58.96/17.01 | % 58.96/17.01 | From (113) and (521) follows: % 58.96/17.01 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.01 | % 58.96/17.01 | Using (438) and (510) yields: % 58.96/17.01 | (151) $false % 58.96/17.01 | % 58.96/17.01 |-The branch is then unsatisfiable % 58.96/17.01 |-Branch two: % 58.96/17.01 | (524) element(all_148_3_78, all_17_0_17) = 0 % 58.96/17.01 | (532) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.96/17.01 | % 58.96/17.01 | Instantiating (532) with all_876_0_180, all_876_1_181 yields: % 58.96/17.01 | (533) ( ~ (all_876_1_181 = 0) & element(all_127_0_70, all_17_0_17) = all_876_1_181) | (related(all_0_13_13, all_127_0_70, all_148_3_78) = all_876_0_180 & in(all_148_3_78, all_0_10_10) = all_876_1_181 & ( ~ (all_876_1_181 = 0) | all_876_0_180 = 0)) % 58.96/17.01 | % 58.96/17.01 | From (113) and (524) follows: % 58.96/17.01 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.01 | % 58.96/17.01 +-Applying beta-rule and splitting (486), into two cases. % 58.96/17.01 |-Branch one: % 58.96/17.01 | (521) ~ (element(all_148_3_78, all_17_0_17) = 0) % 58.96/17.01 | % 58.96/17.01 | From (113) and (521) follows: % 58.96/17.01 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.01 | % 58.96/17.01 | Using (438) and (510) yields: % 58.96/17.01 | (151) $false % 58.96/17.01 | % 58.96/17.01 |-The branch is then unsatisfiable % 58.96/17.01 |-Branch two: % 58.96/17.01 | (524) element(all_148_3_78, all_17_0_17) = 0 % 58.96/17.01 | (539) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_148_3_78) = v1 & in(all_148_3_78, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 58.96/17.01 | % 58.96/17.01 | Instantiating (539) with all_880_0_182, all_880_1_183 yields: % 58.96/17.01 | (540) ( ~ (all_880_1_183 = 0) & element(all_26_2_22, all_17_0_17) = all_880_1_183) | (related(all_0_13_13, all_26_2_22, all_148_3_78) = all_880_0_182 & in(all_148_3_78, all_0_10_10) = all_880_1_183 & ( ~ (all_880_1_183 = 0) | all_880_0_182 = 0)) % 58.96/17.01 | % 58.96/17.01 | From (113) and (524) follows: % 58.96/17.01 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.01 | % 58.96/17.01 +-Applying beta-rule and splitting (483), into two cases. % 58.96/17.01 |-Branch one: % 58.96/17.01 | (542) ~ (element(all_148_3_78, all_28_0_25) = 0) % 58.96/17.01 | % 58.96/17.01 | From (93) and (542) follows: % 58.96/17.01 | (510) ~ (element(all_148_3_78, all_0_10_10) = 0) % 58.96/17.01 | % 58.96/17.01 | Using (438) and (510) yields: % 58.96/17.01 | (151) $false % 58.96/17.01 | % 58.96/17.01 |-The branch is then unsatisfiable % 58.96/17.01 |-Branch two: % 58.96/17.01 | (435) element(all_148_3_78, all_28_0_25) = 0 % 58.96/17.01 | (546) all_0_11_11 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_148_3_78, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_148_3_78) = v0)) % 58.96/17.01 | % 58.96/17.01 | From (93) and (435) follows: % 58.96/17.01 | (438) element(all_148_3_78, all_0_10_10) = 0 % 58.96/17.01 | % 58.96/17.01 +-Applying beta-rule and splitting (540), into two cases. % 58.96/17.01 |-Branch one: % 58.96/17.01 | (548) ~ (all_880_1_183 = 0) & element(all_26_2_22, all_17_0_17) = all_880_1_183 % 58.96/17.01 | % 58.96/17.01 | Applying alpha-rule on (548) yields: % 58.96/17.01 | (549) ~ (all_880_1_183 = 0) % 58.96/17.01 | (550) element(all_26_2_22, all_17_0_17) = all_880_1_183 % 58.96/17.01 | % 58.96/17.01 | From (113) and (550) follows: % 58.96/17.01 | (551) element(all_26_2_22, all_0_10_10) = all_880_1_183 % 58.96/17.01 | % 58.96/17.01 | Instantiating formula (11) with all_26_2_22, all_0_10_10, all_880_1_183, 0 and discharging atoms element(all_26_2_22, all_0_10_10) = all_880_1_183, element(all_26_2_22, all_0_10_10) = 0, yields: % 59.03/17.01 | (552) all_880_1_183 = 0 % 59.03/17.01 | % 59.03/17.01 | Equations (552) can reduce 549 to: % 59.03/17.01 | (81) $false % 59.03/17.01 | % 59.03/17.01 |-The branch is then unsatisfiable % 59.03/17.01 |-Branch two: % 59.03/17.01 | (554) related(all_0_13_13, all_26_2_22, all_148_3_78) = all_880_0_182 & in(all_148_3_78, all_0_10_10) = all_880_1_183 & ( ~ (all_880_1_183 = 0) | all_880_0_182 = 0) % 59.03/17.01 | % 59.03/17.01 | Applying alpha-rule on (554) yields: % 59.03/17.01 | (555) related(all_0_13_13, all_26_2_22, all_148_3_78) = all_880_0_182 % 59.03/17.01 | (556) in(all_148_3_78, all_0_10_10) = all_880_1_183 % 59.03/17.01 | (557) ~ (all_880_1_183 = 0) | all_880_0_182 = 0 % 59.03/17.01 | % 59.03/17.01 +-Applying beta-rule and splitting (526), into two cases. % 59.03/17.01 |-Branch one: % 59.03/17.01 | (558) ~ (all_872_1_179 = 0) & element(all_194_0_79, all_17_0_17) = all_872_1_179 % 59.03/17.01 | % 59.03/17.02 | Applying alpha-rule on (558) yields: % 59.03/17.02 | (559) ~ (all_872_1_179 = 0) % 59.03/17.02 | (560) element(all_194_0_79, all_17_0_17) = all_872_1_179 % 59.03/17.02 | % 59.03/17.02 | From (113) and (560) follows: % 59.03/17.02 | (561) element(all_194_0_79, all_0_10_10) = all_872_1_179 % 59.03/17.02 | % 59.03/17.02 | Instantiating formula (11) with all_194_0_79, all_0_10_10, all_872_1_179, 0 and discharging atoms element(all_194_0_79, all_0_10_10) = all_872_1_179, element(all_194_0_79, all_0_10_10) = 0, yields: % 59.03/17.02 | (562) all_872_1_179 = 0 % 59.03/17.02 | % 59.03/17.02 | Equations (562) can reduce 559 to: % 59.03/17.02 | (81) $false % 59.03/17.02 | % 59.03/17.02 |-The branch is then unsatisfiable % 59.03/17.02 |-Branch two: % 59.03/17.02 | (564) related(all_0_13_13, all_194_0_79, all_148_3_78) = all_872_0_178 & in(all_148_3_78, all_0_10_10) = all_872_1_179 & ( ~ (all_872_1_179 = 0) | all_872_0_178 = 0) % 59.03/17.02 | % 59.03/17.02 | Applying alpha-rule on (564) yields: % 59.03/17.02 | (565) related(all_0_13_13, all_194_0_79, all_148_3_78) = all_872_0_178 % 59.03/17.02 | (566) in(all_148_3_78, all_0_10_10) = all_872_1_179 % 59.03/17.02 | (567) ~ (all_872_1_179 = 0) | all_872_0_178 = 0 % 59.03/17.02 | % 59.03/17.02 +-Applying beta-rule and splitting (533), into two cases. % 59.03/17.02 |-Branch one: % 59.03/17.02 | (568) ~ (all_876_1_181 = 0) & element(all_127_0_70, all_17_0_17) = all_876_1_181 % 59.03/17.02 | % 59.03/17.02 | Applying alpha-rule on (568) yields: % 59.03/17.02 | (569) ~ (all_876_1_181 = 0) % 59.03/17.02 | (570) element(all_127_0_70, all_17_0_17) = all_876_1_181 % 59.03/17.02 | % 59.03/17.02 | From (113) and (570) follows: % 59.03/17.02 | (571) element(all_127_0_70, all_0_10_10) = all_876_1_181 % 59.03/17.02 | % 59.03/17.02 | Instantiating formula (11) with all_127_0_70, all_0_10_10, all_876_1_181, 0 and discharging atoms element(all_127_0_70, all_0_10_10) = all_876_1_181, element(all_127_0_70, all_0_10_10) = 0, yields: % 59.03/17.02 | (572) all_876_1_181 = 0 % 59.03/17.02 | % 59.03/17.02 | Equations (572) can reduce 569 to: % 59.03/17.02 | (81) $false % 59.03/17.02 | % 59.03/17.02 |-The branch is then unsatisfiable % 59.03/17.02 |-Branch two: % 59.03/17.02 | (574) related(all_0_13_13, all_127_0_70, all_148_3_78) = all_876_0_180 & in(all_148_3_78, all_0_10_10) = all_876_1_181 & ( ~ (all_876_1_181 = 0) | all_876_0_180 = 0) % 59.03/17.02 | % 59.03/17.02 | Applying alpha-rule on (574) yields: % 59.03/17.02 | (575) related(all_0_13_13, all_127_0_70, all_148_3_78) = all_876_0_180 % 59.03/17.02 | (576) in(all_148_3_78, all_0_10_10) = all_876_1_181 % 59.03/17.02 | (577) ~ (all_876_1_181 = 0) | all_876_0_180 = 0 % 59.03/17.02 | % 59.03/17.02 +-Applying beta-rule and splitting (479), into two cases. % 59.03/17.02 |-Branch one: % 59.03/17.02 | (578) ~ (element(all_220_3_105, all_17_0_17) = 0) % 59.03/17.02 | % 59.03/17.02 | From (113) and (578) follows: % 59.03/17.02 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.02 | % 59.03/17.02 | Using (446) and (498) yields: % 59.03/17.02 | (151) $false % 59.03/17.02 | % 59.03/17.02 |-The branch is then unsatisfiable % 59.03/17.02 |-Branch two: % 59.03/17.02 | (581) element(all_220_3_105, all_17_0_17) = 0 % 59.03/17.02 | (582) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_127_0_70, all_17_0_17) = v0) | (related(all_0_13_13, all_127_0_70, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.02 | % 59.03/17.02 | Instantiating (582) with all_899_0_269, all_899_1_270 yields: % 59.03/17.02 | (583) ( ~ (all_899_1_270 = 0) & element(all_127_0_70, all_17_0_17) = all_899_1_270) | (related(all_0_13_13, all_127_0_70, all_220_3_105) = all_899_0_269 & in(all_220_3_105, all_0_10_10) = all_899_1_270 & ( ~ (all_899_1_270 = 0) | all_899_0_269 = 0)) % 59.03/17.02 | % 59.03/17.02 | From (113) and (581) follows: % 59.03/17.02 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.02 | % 59.03/17.02 +-Applying beta-rule and splitting (478), into two cases. % 59.03/17.02 |-Branch one: % 59.03/17.02 | (578) ~ (element(all_220_3_105, all_17_0_17) = 0) % 59.03/17.02 | % 59.03/17.02 | From (113) and (578) follows: % 59.03/17.02 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.02 | % 59.03/17.02 | Using (446) and (498) yields: % 59.03/17.02 | (151) $false % 59.03/17.02 | % 59.03/17.02 |-The branch is then unsatisfiable % 59.03/17.02 |-Branch two: % 59.03/17.02 | (581) element(all_220_3_105, all_17_0_17) = 0 % 59.03/17.02 | (589) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_194_0_79, all_17_0_17) = v0) | (related(all_0_13_13, all_194_0_79, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.02 | % 59.03/17.02 | Instantiating (589) with all_903_0_271, all_903_1_272 yields: % 59.03/17.02 | (590) ( ~ (all_903_1_272 = 0) & element(all_194_0_79, all_17_0_17) = all_903_1_272) | (related(all_0_13_13, all_194_0_79, all_220_3_105) = all_903_0_271 & in(all_220_3_105, all_0_10_10) = all_903_1_272 & ( ~ (all_903_1_272 = 0) | all_903_0_271 = 0)) % 59.03/17.02 | % 59.03/17.02 | From (113) and (581) follows: % 59.03/17.02 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.02 | % 59.03/17.02 +-Applying beta-rule and splitting (480), into two cases. % 59.03/17.02 |-Branch one: % 59.03/17.02 | (578) ~ (element(all_220_3_105, all_17_0_17) = 0) % 59.03/17.02 | % 59.03/17.02 | From (113) and (578) follows: % 59.03/17.02 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.02 | % 59.03/17.02 | Using (446) and (498) yields: % 59.03/17.02 | (151) $false % 59.03/17.02 | % 59.03/17.02 |-The branch is then unsatisfiable % 59.03/17.02 |-Branch two: % 59.03/17.02 | (581) element(all_220_3_105, all_17_0_17) = 0 % 59.03/17.02 | (596) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_26_2_22, all_17_0_17) = v0) | (related(all_0_13_13, all_26_2_22, all_220_3_105) = v1 & in(all_220_3_105, all_0_10_10) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.02 | % 59.03/17.03 | Instantiating (596) with all_907_0_273, all_907_1_274 yields: % 59.03/17.03 | (597) ( ~ (all_907_1_274 = 0) & element(all_26_2_22, all_17_0_17) = all_907_1_274) | (related(all_0_13_13, all_26_2_22, all_220_3_105) = all_907_0_273 & in(all_220_3_105, all_0_10_10) = all_907_1_274 & ( ~ (all_907_1_274 = 0) | all_907_0_273 = 0)) % 59.03/17.03 | % 59.03/17.03 | From (113) and (581) follows: % 59.03/17.03 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.03 | % 59.03/17.03 +-Applying beta-rule and splitting (477), into two cases. % 59.03/17.03 |-Branch one: % 59.03/17.03 | (599) ~ (element(all_220_3_105, all_28_0_25) = 0) % 59.03/17.03 | % 59.03/17.03 | From (93) and (599) follows: % 59.03/17.03 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.03 | % 59.03/17.03 | Using (446) and (498) yields: % 59.03/17.03 | (151) $false % 59.03/17.03 | % 59.03/17.03 |-The branch is then unsatisfiable % 59.03/17.03 |-Branch two: % 59.03/17.03 | (445) element(all_220_3_105, all_28_0_25) = 0 % 59.03/17.03 | (603) all_0_11_11 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & v1 = 0 & ~ (v3 = 0) & relstr_set_smaller(all_0_13_13, empty_set, v0) = 0 & related(all_0_13_13, all_220_3_105, v0) = v3 & element(v0, all_28_0_25) = 0) | ( ~ (v0 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_220_3_105) = v0)) % 59.03/17.03 | % 59.03/17.03 | From (93) and (445) follows: % 59.03/17.03 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.03 | % 59.03/17.03 +-Applying beta-rule and splitting (597), into two cases. % 59.03/17.03 |-Branch one: % 59.03/17.03 | (605) ~ (all_907_1_274 = 0) & element(all_26_2_22, all_17_0_17) = all_907_1_274 % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (605) yields: % 59.03/17.03 | (606) ~ (all_907_1_274 = 0) % 59.03/17.03 | (607) element(all_26_2_22, all_17_0_17) = all_907_1_274 % 59.03/17.03 | % 59.03/17.03 | From (113) and (607) follows: % 59.03/17.03 | (608) element(all_26_2_22, all_0_10_10) = all_907_1_274 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (11) with all_26_2_22, all_0_10_10, all_907_1_274, 0 and discharging atoms element(all_26_2_22, all_0_10_10) = all_907_1_274, element(all_26_2_22, all_0_10_10) = 0, yields: % 59.03/17.03 | (609) all_907_1_274 = 0 % 59.03/17.03 | % 59.03/17.03 | Equations (609) can reduce 606 to: % 59.03/17.03 | (81) $false % 59.03/17.03 | % 59.03/17.03 |-The branch is then unsatisfiable % 59.03/17.03 |-Branch two: % 59.03/17.03 | (611) related(all_0_13_13, all_26_2_22, all_220_3_105) = all_907_0_273 & in(all_220_3_105, all_0_10_10) = all_907_1_274 & ( ~ (all_907_1_274 = 0) | all_907_0_273 = 0) % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (611) yields: % 59.03/17.03 | (612) related(all_0_13_13, all_26_2_22, all_220_3_105) = all_907_0_273 % 59.03/17.03 | (613) in(all_220_3_105, all_0_10_10) = all_907_1_274 % 59.03/17.03 | (614) ~ (all_907_1_274 = 0) | all_907_0_273 = 0 % 59.03/17.03 | % 59.03/17.03 +-Applying beta-rule and splitting (583), into two cases. % 59.03/17.03 |-Branch one: % 59.03/17.03 | (615) ~ (all_899_1_270 = 0) & element(all_127_0_70, all_17_0_17) = all_899_1_270 % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (615) yields: % 59.03/17.03 | (616) ~ (all_899_1_270 = 0) % 59.03/17.03 | (617) element(all_127_0_70, all_17_0_17) = all_899_1_270 % 59.03/17.03 | % 59.03/17.03 | From (113) and (617) follows: % 59.03/17.03 | (618) element(all_127_0_70, all_0_10_10) = all_899_1_270 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (11) with all_127_0_70, all_0_10_10, all_899_1_270, 0 and discharging atoms element(all_127_0_70, all_0_10_10) = all_899_1_270, element(all_127_0_70, all_0_10_10) = 0, yields: % 59.03/17.03 | (619) all_899_1_270 = 0 % 59.03/17.03 | % 59.03/17.03 | Equations (619) can reduce 616 to: % 59.03/17.03 | (81) $false % 59.03/17.03 | % 59.03/17.03 |-The branch is then unsatisfiable % 59.03/17.03 |-Branch two: % 59.03/17.03 | (621) related(all_0_13_13, all_127_0_70, all_220_3_105) = all_899_0_269 & in(all_220_3_105, all_0_10_10) = all_899_1_270 & ( ~ (all_899_1_270 = 0) | all_899_0_269 = 0) % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (621) yields: % 59.03/17.03 | (622) related(all_0_13_13, all_127_0_70, all_220_3_105) = all_899_0_269 % 59.03/17.03 | (623) in(all_220_3_105, all_0_10_10) = all_899_1_270 % 59.03/17.03 | (624) ~ (all_899_1_270 = 0) | all_899_0_269 = 0 % 59.03/17.03 | % 59.03/17.03 +-Applying beta-rule and splitting (590), into two cases. % 59.03/17.03 |-Branch one: % 59.03/17.03 | (625) ~ (all_903_1_272 = 0) & element(all_194_0_79, all_17_0_17) = all_903_1_272 % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (625) yields: % 59.03/17.03 | (626) ~ (all_903_1_272 = 0) % 59.03/17.03 | (627) element(all_194_0_79, all_17_0_17) = all_903_1_272 % 59.03/17.03 | % 59.03/17.03 | From (113) and (627) follows: % 59.03/17.03 | (628) element(all_194_0_79, all_0_10_10) = all_903_1_272 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (11) with all_194_0_79, all_0_10_10, all_903_1_272, 0 and discharging atoms element(all_194_0_79, all_0_10_10) = all_903_1_272, element(all_194_0_79, all_0_10_10) = 0, yields: % 59.03/17.03 | (629) all_903_1_272 = 0 % 59.03/17.03 | % 59.03/17.03 | Equations (629) can reduce 626 to: % 59.03/17.03 | (81) $false % 59.03/17.03 | % 59.03/17.03 |-The branch is then unsatisfiable % 59.03/17.03 |-Branch two: % 59.03/17.03 | (631) related(all_0_13_13, all_194_0_79, all_220_3_105) = all_903_0_271 & in(all_220_3_105, all_0_10_10) = all_903_1_272 & ( ~ (all_903_1_272 = 0) | all_903_0_271 = 0) % 59.03/17.03 | % 59.03/17.03 | Applying alpha-rule on (631) yields: % 59.03/17.03 | (632) related(all_0_13_13, all_194_0_79, all_220_3_105) = all_903_0_271 % 59.03/17.03 | (633) in(all_220_3_105, all_0_10_10) = all_903_1_272 % 59.03/17.03 | (634) ~ (all_903_1_272 = 0) | all_903_0_271 = 0 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (21) with all_0_13_13, all_127_0_70, all_220_3_105, all_899_0_269, all_220_0_102 and discharging atoms related(all_0_13_13, all_127_0_70, all_220_3_105) = all_899_0_269, related(all_0_13_13, all_127_0_70, all_220_3_105) = all_220_0_102, yields: % 59.03/17.03 | (635) all_899_0_269 = all_220_0_102 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (21) with all_0_13_13, all_26_2_22, all_148_3_78, all_880_0_182, all_148_0_75 and discharging atoms related(all_0_13_13, all_26_2_22, all_148_3_78) = all_880_0_182, related(all_0_13_13, all_26_2_22, all_148_3_78) = all_148_0_75, yields: % 59.03/17.03 | (636) all_880_0_182 = all_148_0_75 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (11) with all_220_3_105, all_0_10_10, all_843_1_169, 0 and discharging atoms element(all_220_3_105, all_0_10_10) = all_843_1_169, element(all_220_3_105, all_0_10_10) = 0, yields: % 59.03/17.03 | (637) all_843_1_169 = 0 % 59.03/17.03 | % 59.03/17.03 | Instantiating formula (11) with all_148_3_78, all_0_10_10, all_841_1_167, 0 and discharging atoms element(all_148_3_78, all_0_10_10) = all_841_1_167, element(all_148_3_78, all_0_10_10) = 0, yields: % 59.03/17.04 | (638) all_841_1_167 = 0 % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (27) with all_220_3_105, all_0_10_10, all_903_1_272, all_907_1_274 and discharging atoms in(all_220_3_105, all_0_10_10) = all_907_1_274, in(all_220_3_105, all_0_10_10) = all_903_1_272, yields: % 59.03/17.04 | (639) all_907_1_274 = all_903_1_272 % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (27) with all_220_3_105, all_0_10_10, all_899_1_270, all_907_1_274 and discharging atoms in(all_220_3_105, all_0_10_10) = all_907_1_274, in(all_220_3_105, all_0_10_10) = all_899_1_270, yields: % 59.03/17.04 | (640) all_907_1_274 = all_899_1_270 % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (27) with all_148_3_78, all_0_10_10, all_876_1_181, all_880_1_183 and discharging atoms in(all_148_3_78, all_0_10_10) = all_880_1_183, in(all_148_3_78, all_0_10_10) = all_876_1_181, yields: % 59.03/17.04 | (641) all_880_1_183 = all_876_1_181 % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (27) with all_148_3_78, all_0_10_10, all_872_1_179, all_880_1_183 and discharging atoms in(all_148_3_78, all_0_10_10) = all_880_1_183, in(all_148_3_78, all_0_10_10) = all_872_1_179, yields: % 59.03/17.04 | (642) all_880_1_183 = all_872_1_179 % 59.03/17.04 | % 59.03/17.04 | Combining equations (640,639) yields a new equation: % 59.03/17.04 | (643) all_903_1_272 = all_899_1_270 % 59.03/17.04 | % 59.03/17.04 | Combining equations (642,641) yields a new equation: % 59.03/17.04 | (644) all_876_1_181 = all_872_1_179 % 59.03/17.04 | % 59.03/17.04 | Combining equations (644,641) yields a new equation: % 59.03/17.04 | (642) all_880_1_183 = all_872_1_179 % 59.03/17.04 | % 59.03/17.04 | From (637) and (495) follows: % 59.03/17.04 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.04 | % 59.03/17.04 | From (643) and (633) follows: % 59.03/17.04 | (623) in(all_220_3_105, all_0_10_10) = all_899_1_270 % 59.03/17.04 | % 59.03/17.04 | From (644) and (576) follows: % 59.03/17.04 | (566) in(all_148_3_78, all_0_10_10) = all_872_1_179 % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (490), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (649) ~ (all_841_1_167 = 0) % 59.03/17.04 | % 59.03/17.04 | Equations (638) can reduce 649 to: % 59.03/17.04 | (81) $false % 59.03/17.04 | % 59.03/17.04 |-The branch is then unsatisfiable % 59.03/17.04 |-Branch two: % 59.03/17.04 | (638) all_841_1_167 = 0 % 59.03/17.04 | (652) all_841_0_166 = 0 % 59.03/17.04 | % 59.03/17.04 | From (652) and (489) follows: % 59.03/17.04 | (653) relstr_element_smaller(all_0_13_13, empty_set, all_148_3_78) = 0 % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (624), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (616) ~ (all_899_1_270 = 0) % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (557), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (549) ~ (all_880_1_183 = 0) % 59.03/17.04 | % 59.03/17.04 | Equations (642) can reduce 549 to: % 59.03/17.04 | (559) ~ (all_872_1_179 = 0) % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (494), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (657) ~ (all_843_1_169 = 0) % 59.03/17.04 | % 59.03/17.04 | Equations (637) can reduce 657 to: % 59.03/17.04 | (81) $false % 59.03/17.04 | % 59.03/17.04 |-The branch is then unsatisfiable % 59.03/17.04 |-Branch two: % 59.03/17.04 | (637) all_843_1_169 = 0 % 59.03/17.04 | (660) all_843_0_168 = 0 % 59.03/17.04 | % 59.03/17.04 | From (660) and (493) follows: % 59.03/17.04 | (661) relstr_element_smaller(all_0_13_13, empty_set, all_220_3_105) = 0 % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (67) with all_220_3_105, all_220_3_105, empty_set and discharging atoms relstr_element_smaller(all_0_13_13, empty_set, all_220_3_105) = 0, yields: % 59.03/17.04 | (662) ~ (element(all_220_3_105, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_220_3_105, all_17_0_17) = v0) | (related(all_0_13_13, all_220_3_105, all_220_3_105) = v1 & in(all_220_3_105, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (67) with all_220_3_105, all_148_3_78, empty_set and discharging atoms relstr_element_smaller(all_0_13_13, empty_set, all_148_3_78) = 0, yields: % 59.03/17.04 | (663) ~ (element(all_220_3_105, all_17_0_17) = 0) | ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_148_3_78, all_17_0_17) = v0) | (related(all_0_13_13, all_148_3_78, all_220_3_105) = v1 & in(all_220_3_105, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (33) with all_899_1_270, all_0_10_10, all_220_3_105 and discharging atoms in(all_220_3_105, all_0_10_10) = all_899_1_270, yields: % 59.03/17.04 | (664) all_899_1_270 = 0 | ? [v0] : ? [v1] : (element(all_220_3_105, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 59.03/17.04 | % 59.03/17.04 | Instantiating formula (33) with all_872_1_179, all_0_10_10, all_148_3_78 and discharging atoms in(all_148_3_78, all_0_10_10) = all_872_1_179, yields: % 59.03/17.04 | (665) all_872_1_179 = 0 | ? [v0] : ? [v1] : (element(all_148_3_78, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (664), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (619) all_899_1_270 = 0 % 59.03/17.04 | % 59.03/17.04 | Equations (619) can reduce 616 to: % 59.03/17.04 | (81) $false % 59.03/17.04 | % 59.03/17.04 |-The branch is then unsatisfiable % 59.03/17.04 |-Branch two: % 59.03/17.04 | (616) ~ (all_899_1_270 = 0) % 59.03/17.04 | (669) ? [v0] : ? [v1] : (element(all_220_3_105, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 59.03/17.04 | % 59.03/17.04 | Instantiating (669) with all_1210_0_304, all_1210_1_305 yields: % 59.03/17.04 | (670) element(all_220_3_105, all_0_10_10) = all_1210_1_305 & empty(all_0_10_10) = all_1210_0_304 & ( ~ (all_1210_1_305 = 0) | all_1210_0_304 = 0) % 59.03/17.04 | % 59.03/17.04 | Applying alpha-rule on (670) yields: % 59.03/17.04 | (671) element(all_220_3_105, all_0_10_10) = all_1210_1_305 % 59.03/17.04 | (672) empty(all_0_10_10) = all_1210_0_304 % 59.03/17.04 | (673) ~ (all_1210_1_305 = 0) | all_1210_0_304 = 0 % 59.03/17.04 | % 59.03/17.04 +-Applying beta-rule and splitting (662), into two cases. % 59.03/17.04 |-Branch one: % 59.03/17.04 | (578) ~ (element(all_220_3_105, all_17_0_17) = 0) % 59.03/17.04 | % 59.03/17.04 | From (113) and (578) follows: % 59.03/17.05 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.05 | % 59.03/17.05 | Using (446) and (498) yields: % 59.03/17.05 | (151) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (581) element(all_220_3_105, all_17_0_17) = 0 % 59.03/17.05 | (678) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_220_3_105, all_17_0_17) = v0) | (related(all_0_13_13, all_220_3_105, all_220_3_105) = v1 & in(all_220_3_105, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.05 | % 59.03/17.05 | From (113) and (581) follows: % 59.03/17.05 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.05 | % 59.03/17.05 +-Applying beta-rule and splitting (663), into two cases. % 59.03/17.05 |-Branch one: % 59.03/17.05 | (578) ~ (element(all_220_3_105, all_17_0_17) = 0) % 59.03/17.05 | % 59.03/17.05 | From (113) and (578) follows: % 59.03/17.05 | (498) ~ (element(all_220_3_105, all_0_10_10) = 0) % 59.03/17.05 | % 59.03/17.05 | Using (446) and (498) yields: % 59.03/17.05 | (151) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (581) element(all_220_3_105, all_17_0_17) = 0 % 59.03/17.05 | (684) ? [v0] : ? [v1] : (( ~ (v0 = 0) & element(all_148_3_78, all_17_0_17) = v0) | (related(all_0_13_13, all_148_3_78, all_220_3_105) = v1 & in(all_220_3_105, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 59.03/17.05 | % 59.03/17.05 | From (113) and (581) follows: % 59.03/17.05 | (446) element(all_220_3_105, all_0_10_10) = 0 % 59.03/17.05 | % 59.03/17.05 +-Applying beta-rule and splitting (665), into two cases. % 59.03/17.05 |-Branch one: % 59.03/17.05 | (562) all_872_1_179 = 0 % 59.03/17.05 | % 59.03/17.05 | Equations (562) can reduce 559 to: % 59.03/17.05 | (81) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (559) ~ (all_872_1_179 = 0) % 59.03/17.05 | (689) ? [v0] : ? [v1] : (element(all_148_3_78, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 59.03/17.05 | % 59.03/17.05 | Instantiating (689) with all_1387_0_446, all_1387_1_447 yields: % 59.03/17.05 | (690) element(all_148_3_78, all_0_10_10) = all_1387_1_447 & empty(all_0_10_10) = all_1387_0_446 & ( ~ (all_1387_1_447 = 0) | all_1387_0_446 = 0) % 59.03/17.05 | % 59.03/17.05 | Applying alpha-rule on (690) yields: % 59.03/17.05 | (691) element(all_148_3_78, all_0_10_10) = all_1387_1_447 % 59.03/17.05 | (692) empty(all_0_10_10) = all_1387_0_446 % 59.03/17.05 | (693) ~ (all_1387_1_447 = 0) | all_1387_0_446 = 0 % 59.03/17.05 | % 59.03/17.05 | Instantiating formula (11) with all_220_3_105, all_0_10_10, all_1210_1_305, 0 and discharging atoms element(all_220_3_105, all_0_10_10) = all_1210_1_305, element(all_220_3_105, all_0_10_10) = 0, yields: % 59.03/17.05 | (694) all_1210_1_305 = 0 % 59.03/17.05 | % 59.03/17.05 | Instantiating formula (40) with all_0_10_10, all_1387_0_446, all_41_0_32 and discharging atoms empty(all_0_10_10) = all_1387_0_446, empty(all_0_10_10) = all_41_0_32, yields: % 59.03/17.05 | (695) all_1387_0_446 = all_41_0_32 % 59.03/17.05 | % 59.03/17.05 | Instantiating formula (40) with all_0_10_10, all_1210_0_304, all_1387_0_446 and discharging atoms empty(all_0_10_10) = all_1387_0_446, empty(all_0_10_10) = all_1210_0_304, yields: % 59.03/17.05 | (696) all_1387_0_446 = all_1210_0_304 % 59.03/17.05 | % 59.03/17.05 | Using (672) and (376) yields: % 59.03/17.05 | (697) ~ (all_1210_0_304 = 0) % 59.03/17.05 | % 59.03/17.05 | Combining equations (695,696) yields a new equation: % 59.03/17.05 | (698) all_1210_0_304 = all_41_0_32 % 59.03/17.05 | % 59.03/17.05 | Equations (698) can reduce 697 to: % 59.03/17.05 | (156) ~ (all_41_0_32 = 0) % 59.03/17.05 | % 59.03/17.05 +-Applying beta-rule and splitting (673), into two cases. % 59.03/17.05 |-Branch one: % 59.03/17.05 | (700) ~ (all_1210_1_305 = 0) % 59.03/17.05 | % 59.03/17.05 | Equations (694) can reduce 700 to: % 59.03/17.05 | (81) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (694) all_1210_1_305 = 0 % 59.03/17.05 | (703) all_1210_0_304 = 0 % 59.03/17.05 | % 59.03/17.05 | Combining equations (703,698) yields a new equation: % 59.03/17.05 | (704) all_41_0_32 = 0 % 59.03/17.05 | % 59.03/17.05 | Equations (704) can reduce 156 to: % 59.03/17.05 | (81) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (552) all_880_1_183 = 0 % 59.03/17.05 | (707) all_880_0_182 = 0 % 59.03/17.05 | % 59.03/17.05 | Combining equations (707,636) yields a new equation: % 59.03/17.05 | (708) all_148_0_75 = 0 % 59.03/17.05 | % 59.03/17.05 | Equations (708) can reduce 433 to: % 59.03/17.05 | (81) $false % 59.03/17.05 | % 59.03/17.05 |-The branch is then unsatisfiable % 59.03/17.05 |-Branch two: % 59.03/17.05 | (619) all_899_1_270 = 0 % 59.03/17.05 | (711) all_899_0_269 = 0 % 59.03/17.05 | % 59.03/17.05 | Combining equations (635,711) yields a new equation: % 59.03/17.05 | (712) all_220_0_102 = 0 % 59.03/17.06 | % 59.03/17.06 | Simplifying 712 yields: % 59.03/17.06 | (713) all_220_0_102 = 0 % 59.03/17.06 | % 59.03/17.06 | Equations (713) can reduce 444 to: % 59.03/17.06 | (81) $false % 59.03/17.06 | % 59.03/17.06 |-The branch is then unsatisfiable % 59.03/17.06 |-Branch two: % 59.03/17.06 | (715) ~ (all_220_3_105 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = all_220_3_105 % 59.03/17.06 | % 59.03/17.06 | Applying alpha-rule on (715) yields: % 59.03/17.06 | (716) ~ (all_220_3_105 = 0) % 59.03/17.06 | (717) relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = all_220_3_105 % 59.03/17.06 | % 59.03/17.06 | Instantiating formula (63) with all_220_3_105, all_127_0_70 and discharging atoms relstr_set_smaller(all_0_13_13, empty_set, all_127_0_70) = all_220_3_105, yields: % 59.03/17.06 | (718) ? [v0] : ? [v1] : (element(all_127_0_70, all_14_0_16) = v0 & relstr_element_smaller(all_0_13_13, empty_set, all_127_0_70) = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_220_3_105 = 0))) % 59.03/17.06 | % 59.03/17.06 | Instantiating (718) with all_837_0_454, all_837_1_455 yields: % 59.03/17.06 | (719) element(all_127_0_70, all_14_0_16) = all_837_1_455 & relstr_element_smaller(all_0_13_13, empty_set, all_127_0_70) = all_837_0_454 & ( ~ (all_837_1_455 = 0) | (all_837_0_454 = 0 & all_220_3_105 = 0)) % 59.03/17.06 | % 59.03/17.06 | Applying alpha-rule on (719) yields: % 59.03/17.06 | (720) element(all_127_0_70, all_14_0_16) = all_837_1_455 % 59.03/17.06 | (721) relstr_element_smaller(all_0_13_13, empty_set, all_127_0_70) = all_837_0_454 % 59.03/17.06 | (722) ~ (all_837_1_455 = 0) | (all_837_0_454 = 0 & all_220_3_105 = 0) % 59.03/17.06 | % 59.03/17.06 | From (114) and (720) follows: % 59.03/17.06 | (723) element(all_127_0_70, all_0_10_10) = all_837_1_455 % 59.03/17.06 | % 59.03/17.06 +-Applying beta-rule and splitting (722), into two cases. % 59.03/17.06 |-Branch one: % 59.03/17.06 | (724) ~ (all_837_1_455 = 0) % 59.03/17.06 | % 59.03/17.06 | Instantiating formula (11) with all_127_0_70, all_0_10_10, all_837_1_455, 0 and discharging atoms element(all_127_0_70, all_0_10_10) = all_837_1_455, element(all_127_0_70, all_0_10_10) = 0, yields: % 59.03/17.06 | (725) all_837_1_455 = 0 % 59.03/17.06 | % 59.03/17.06 | Equations (725) can reduce 724 to: % 59.03/17.06 | (81) $false % 59.03/17.06 | % 59.03/17.06 |-The branch is then unsatisfiable % 59.03/17.06 |-Branch two: % 59.03/17.06 | (725) all_837_1_455 = 0 % 59.03/17.06 | (728) all_837_0_454 = 0 & all_220_3_105 = 0 % 59.03/17.06 | % 59.03/17.06 | Applying alpha-rule on (728) yields: % 59.03/17.06 | (729) all_837_0_454 = 0 % 59.03/17.06 | (730) all_220_3_105 = 0 % 59.03/17.06 | % 59.03/17.06 | Equations (730) can reduce 716 to: % 59.03/17.06 | (81) $false % 59.03/17.06 | % 59.03/17.06 |-The branch is then unsatisfiable % 59.03/17.06 |-Branch two: % 59.03/17.06 | (732) ~ (all_148_3_78 = 0) & relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = all_148_3_78 % 59.03/17.06 | % 59.03/17.06 | Applying alpha-rule on (732) yields: % 59.03/17.06 | (733) ~ (all_148_3_78 = 0) % 59.03/17.06 | (734) relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = all_148_3_78 % 59.03/17.06 | % 59.03/17.06 | Instantiating formula (63) with all_148_3_78, all_26_2_22 and discharging atoms relstr_set_smaller(all_0_13_13, empty_set, all_26_2_22) = all_148_3_78, yields: % 59.03/17.06 | (735) ? [v0] : ? [v1] : (element(all_26_2_22, all_14_0_16) = v0 & relstr_element_smaller(all_0_13_13, empty_set, all_26_2_22) = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_148_3_78 = 0))) % 59.03/17.06 | % 59.03/17.07 | Instantiating (735) with all_837_0_475, all_837_1_476 yields: % 59.03/17.07 | (736) element(all_26_2_22, all_14_0_16) = all_837_1_476 & relstr_element_smaller(all_0_13_13, empty_set, all_26_2_22) = all_837_0_475 & ( ~ (all_837_1_476 = 0) | (all_837_0_475 = 0 & all_148_3_78 = 0)) % 59.03/17.07 | % 59.03/17.07 | Applying alpha-rule on (736) yields: % 59.03/17.07 | (737) element(all_26_2_22, all_14_0_16) = all_837_1_476 % 59.03/17.07 | (738) relstr_element_smaller(all_0_13_13, empty_set, all_26_2_22) = all_837_0_475 % 59.03/17.07 | (739) ~ (all_837_1_476 = 0) | (all_837_0_475 = 0 & all_148_3_78 = 0) % 59.03/17.07 | % 59.03/17.07 | From (114) and (737) follows: % 59.03/17.07 | (740) element(all_26_2_22, all_0_10_10) = all_837_1_476 % 59.03/17.07 | % 59.03/17.07 +-Applying beta-rule and splitting (739), into two cases. % 59.03/17.07 |-Branch one: % 59.03/17.07 | (741) ~ (all_837_1_476 = 0) % 59.03/17.07 | % 59.03/17.07 | Instantiating formula (11) with all_26_2_22, all_0_10_10, all_837_1_476, 0 and discharging atoms element(all_26_2_22, all_0_10_10) = all_837_1_476, element(all_26_2_22, all_0_10_10) = 0, yields: % 59.03/17.07 | (742) all_837_1_476 = 0 % 59.03/17.07 | % 59.03/17.07 | Equations (742) can reduce 741 to: % 59.03/17.07 | (81) $false % 59.03/17.07 | % 59.03/17.07 |-The branch is then unsatisfiable % 59.03/17.07 |-Branch two: % 59.03/17.07 | (742) all_837_1_476 = 0 % 59.03/17.07 | (745) all_837_0_475 = 0 & all_148_3_78 = 0 % 59.03/17.07 | % 59.03/17.07 | Applying alpha-rule on (745) yields: % 59.03/17.07 | (746) all_837_0_475 = 0 % 59.03/17.07 | (747) all_148_3_78 = 0 % 59.03/17.07 | % 59.03/17.07 | Equations (747) can reduce 733 to: % 59.03/17.07 | (81) $false % 59.03/17.07 | % 59.03/17.07 |-The branch is then unsatisfiable % 59.03/17.07 |-Branch two: % 59.03/17.07 | (749) empty(all_41_1_33) = 0 % 59.03/17.07 | (750) all_41_1_33 = empty_set % 59.03/17.07 | % 59.03/17.07 | Combining equations (118,750) yields a new equation: % 59.03/17.07 | (751) all_0_10_10 = empty_set % 59.03/17.07 | % 59.03/17.07 | Simplifying 751 yields: % 59.03/17.07 | (752) all_0_10_10 = empty_set % 59.03/17.07 | % 59.03/17.07 | Equations (752) can reduce 374 to: % 59.03/17.07 | (81) $false % 59.03/17.07 | % 59.03/17.07 |-The branch is then unsatisfiable % 59.03/17.07 |-Branch two: % 59.03/17.07 | (754) empty(empty_set) = all_41_0_32 % 59.03/17.07 | (704) all_41_0_32 = 0 % 59.03/17.07 | % 59.03/17.07 | Equations (704) can reduce 156 to: % 59.03/17.07 | (81) $false % 59.03/17.07 | % 59.03/17.07 |-The branch is then unsatisfiable % 59.03/17.07 |-Branch two: % 59.03/17.07 | (158) ~ (all_78_1_36 = 0) % 59.03/17.07 | (758) ? [v0] : ? [v1] : (element(all_26_2_22, all_0_10_10) = v0 & empty(all_0_10_10) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 59.03/17.07 | % 59.03/17.07 | Instantiating (758) with all_102_0_496, all_102_1_497 yields: % 59.03/17.07 | (759) element(all_26_2_22, all_0_10_10) = all_102_1_497 & empty(all_0_10_10) = all_102_0_496 & ( ~ (all_102_1_497 = 0) | all_102_0_496 = 0) % 59.03/17.07 | % 59.03/17.07 | Applying alpha-rule on (759) yields: % 59.03/17.07 | (760) element(all_26_2_22, all_0_10_10) = all_102_1_497 % 59.03/17.07 | (761) empty(all_0_10_10) = all_102_0_496 % 59.03/17.07 | (762) ~ (all_102_1_497 = 0) | all_102_0_496 = 0 % 59.03/17.07 | % 59.03/17.07 | Instantiating formula (11) with all_26_2_22, all_0_10_10, all_102_1_497, 0 and discharging atoms element(all_26_2_22, all_0_10_10) = all_102_1_497, element(all_26_2_22, all_0_10_10) = 0, yields: % 59.03/17.07 | (763) all_102_1_497 = 0 % 59.03/17.07 | % 59.03/17.07 | Instantiating formula (40) with all_0_10_10, all_102_0_496, all_41_0_32 and discharging atoms empty(all_0_10_10) = all_102_0_496, empty(all_0_10_10) = all_41_0_32, yields: % 59.03/17.07 | (764) all_102_0_496 = all_41_0_32 % 59.03/17.07 | % 59.03/17.07 +-Applying beta-rule and splitting (762), into two cases. % 59.03/17.07 |-Branch one: % 59.03/17.07 | (765) ~ (all_102_1_497 = 0) % 59.03/17.07 | % 59.03/17.07 | Equations (763) can reduce 765 to: % 59.03/17.07 | (81) $false % 59.03/17.07 | % 59.03/17.07 |-The branch is then unsatisfiable % 59.03/17.07 |-Branch two: % 59.03/17.07 | (763) all_102_1_497 = 0 % 59.03/17.07 | (768) all_102_0_496 = 0 % 59.03/17.07 | % 59.03/17.08 | Combining equations (768,764) yields a new equation: % 59.03/17.08 | (704) all_41_0_32 = 0 % 59.03/17.08 | % 59.03/17.08 | Equations (704) can reduce 156 to: % 59.03/17.08 | (81) $false % 59.03/17.08 | % 59.03/17.08 |-The branch is then unsatisfiable % 59.03/17.08 |-Branch two: % 59.03/17.08 | (704) all_41_0_32 = 0 % 59.03/17.08 | (772) ~ (all_41_2_34 = 0) % 59.03/17.08 | % 59.03/17.08 | Equations (148) can reduce 772 to: % 59.03/17.08 | (81) $false % 59.03/17.08 | % 59.03/17.08 |-The branch is then unsatisfiable % 59.03/17.08 |-Branch two: % 59.03/17.08 | (772) ~ (all_41_2_34 = 0) % 59.03/17.08 | (775) ? [v0] : ( ~ (v0 = 0) & rel_str(all_0_13_13) = v0) % 59.03/17.08 | % 59.03/17.08 | Instantiating (775) with all_75_0_498 yields: % 59.03/17.08 | (776) ~ (all_75_0_498 = 0) & rel_str(all_0_13_13) = all_75_0_498 % 59.03/17.08 | % 59.03/17.08 | Applying alpha-rule on (776) yields: % 59.03/17.08 | (777) ~ (all_75_0_498 = 0) % 59.03/17.08 | (778) rel_str(all_0_13_13) = all_75_0_498 % 59.03/17.08 | % 59.03/17.08 | Instantiating formula (44) with all_0_13_13, all_75_0_498, 0 and discharging atoms rel_str(all_0_13_13) = all_75_0_498, rel_str(all_0_13_13) = 0, yields: % 59.03/17.08 | (779) all_75_0_498 = 0 % 59.03/17.08 | % 59.03/17.08 | Equations (779) can reduce 777 to: % 59.03/17.08 | (81) $false % 59.03/17.08 | % 59.03/17.08 |-The branch is then unsatisfiable % 59.03/17.08 % SZS output end Proof for theBenchmark % 59.03/17.08 % 59.03/17.08 16381ms %------------------------------------------------------------------------------