%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU324+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n021.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:48:52 EDT 2022 % Result : Theorem 3.34s 1.49s % Output : Proof 6.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU324+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun Jun 19 06:22:47 EDT 2022 % 0.12/0.33 % CPUTime : % 0.54/0.60 ____ _ % 0.54/0.60 ___ / __ \_____(_)___ ________ __________ % 0.54/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.54/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.54/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.54/0.60 % 0.54/0.60 A Theorem Prover for First-Order Logic % 0.54/0.60 (ePrincess v.1.0) % 0.54/0.60 % 0.54/0.60 (c) Philipp Rümmer, 2009-2015 % 0.54/0.60 (c) Peter Backeman, 2014-2015 % 0.54/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.54/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.54/0.60 Bug reports to peter@backeman.se % 0.54/0.60 % 0.54/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.54/0.60 % 0.54/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.75/0.67 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.57/0.97 Prover 0: Preprocessing ... % 2.15/1.19 Prover 0: Warning: ignoring some quantifiers % 2.15/1.22 Prover 0: Constructing countermodel ... % 3.34/1.49 Prover 0: proved (810ms) % 3.34/1.49 % 3.34/1.49 No countermodel exists, formula is valid % 3.34/1.49 % SZS status Theorem for theBenchmark % 3.34/1.49 % 3.34/1.49 Generating proof ... Warning: ignoring some quantifiers % 5.67/2.01 found it (size 151) % 5.67/2.01 % 5.67/2.01 % SZS output start Proof for theBenchmark % 5.67/2.01 Assumed formulas after preprocessing and simplification: % 5.67/2.01 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : (the_carrier(v3) = v4 & the_carrier(v0) = v1 & powerset(v4) = v5 & powerset(v1) = v2 & interior(v3, v8) = v9 & interior(v0, v6) = v7 & topological_space(v0) & one_sorted_str(v10) & element(v8, v5) & element(v6, v2) & top_str(v11) & top_str(v3) & top_str(v0) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v15 = v13 | ~ (subset_complement(v12, v14) = v15) | ~ (subset_complement(v12, v13) = v14) | ? [v16] : (powerset(v12) = v16 & ~ element(v13, v16))) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v13 = v12 | ~ (interior(v15, v14) = v13) | ~ (interior(v15, v14) = v12)) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v13 = v12 | ~ (topstr_closure(v15, v14) = v13) | ~ (topstr_closure(v15, v14) = v12)) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v13 = v12 | ~ (subset_complement(v15, v14) = v13) | ~ (subset_complement(v15, v14) = v12)) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (the_carrier(v12) = v14) | ~ (subset_complement(v14, v13) = v15) | ~ open_subset(v13, v12) | ~ topological_space(v12) | ~ top_str(v12) | closed_subset(v15, v12) | ? [v16] : (powerset(v14) = v16 & ~ element(v13, v16))) & ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (the_carrier(v12) = v14) | ~ (subset_complement(v14, v13) = v15) | ~ closed_subset(v13, v12) | ~ topological_space(v12) | ~ top_str(v12) | open_subset(v15, v12) | ? [v16] : (powerset(v14) = v16 & ~ element(v13, v16))) & ! [v12] : ! [v13] : ! [v14] : (v13 = v12 | ~ (the_carrier(v14) = v13) | ~ (the_carrier(v14) = v12)) & ! [v12] : ! [v13] : ! [v14] : (v13 = v12 | ~ (powerset(v14) = v13) | ~ (powerset(v14) = v12)) & ! [v12] : ! [v13] : ! [v14] : ( ~ (powerset(v13) = v14) | ~ subset(v12, v13) | element(v12, v14)) & ! [v12] : ! [v13] : ! [v14] : ( ~ (powerset(v13) = v14) | ~ element(v12, v14) | subset(v12, v13)) & ! [v12] : ! [v13] : ! [v14] : ( ~ (interior(v12, v13) = v14) | ~ topological_space(v12) | ~ top_str(v12) | open_subset(v14, v12) | ? [v15] : ? [v16] : (the_carrier(v12) = v15 & powerset(v15) = v16 & ~ element(v13, v16))) & ! [v12] : ! [v13] : ! [v14] : ( ~ (interior(v12, v13) = v14) | ~ top_str(v12) | ? [v15] : ? [v16] : (the_carrier(v12) = v15 & powerset(v15) = v16 & ( ~ element(v13, v16) | element(v14, v16)))) & ! [v12] : ! [v13] : ! [v14] : ( ~ (topstr_closure(v12, v13) = v14) | ~ topological_space(v12) | ~ top_str(v12) | closed_subset(v14, v12) | ? [v15] : ? [v16] : (the_carrier(v12) = v15 & powerset(v15) = v16 & ~ element(v13, v16))) & ! [v12] : ! [v13] : ! [v14] : ( ~ (topstr_closure(v12, v13) = v14) | ~ top_str(v12) | ? [v15] : ? [v16] : (the_carrier(v12) = v15 & powerset(v15) = v16 & ( ~ element(v13, v16) | element(v14, v16)))) & ! [v12] : ! [v13] : ! [v14] : ( ~ (subset_complement(v12, v13) = v14) | ? [v15] : (powerset(v12) = v15 & ( ~ element(v13, v15) | element(v14, v15)))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ topological_space(v12) | ~ top_str(v12) | ? [v14] : ? [v15] : (powerset(v13) = v14 & open_subset(v15, v12) & closed_subset(v15, v12) & element(v15, v14))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ topological_space(v12) | ~ top_str(v12) | ? [v14] : ? [v15] : (powerset(v13) = v14 & open_subset(v15, v12) & element(v15, v14))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ topological_space(v12) | ~ top_str(v12) | ? [v14] : ? [v15] : (powerset(v13) = v14 & closed_subset(v15, v12) & element(v15, v14))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ top_str(v12) | ? [v14] : (powerset(v13) = v14 & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (topstr_closure(v12, v16) = v17) | ~ (subset_complement(v13, v17) = v18) | ~ (subset_complement(v13, v15) = v16) | ~ element(v15, v14) | interior(v12, v15) = v18) & ! [v15] : ! [v16] : ( ~ (interior(v12, v15) = v16) | ~ element(v15, v14) | ? [v17] : ? [v18] : (topstr_closure(v12, v17) = v18 & subset_complement(v13, v18) = v16 & subset_complement(v13, v15) = v17)))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ top_str(v12) | ? [v14] : (powerset(v13) = v14 & ! [v15] : ! [v16] : (v16 = v15 | ~ (topstr_closure(v12, v15) = v16) | ~ closed_subset(v15, v12) | ~ element(v15, v14)) & ! [v15] : ( ~ (topstr_closure(v12, v15) = v15) | ~ topological_space(v12) | ~ element(v15, v14) | closed_subset(v15, v12)))) & ! [v12] : ! [v13] : ( ~ (the_carrier(v12) = v13) | ~ top_str(v12) | ? [v14] : (powerset(v13) = v14 & ! [v15] : ! [v16] : ( ~ (subset_complement(v13, v15) = v16) | ~ open_subset(v15, v12) | ~ element(v15, v14) | closed_subset(v16, v12)) & ! [v15] : ! [v16] : ( ~ (subset_complement(v13, v15) = v16) | ~ closed_subset(v16, v12) | ~ element(v15, v14) | open_subset(v15, v12)))) & ! [v12] : ( ~ top_str(v12) | one_sorted_str(v12)) & ? [v12] : ? [v13] : element(v13, v12) & ? [v12] : subset(v12, v12) & ((v7 = v6 & ~ open_subset(v6, v0)) | ( ~ (v9 = v8) & open_subset(v8, v3)))) % 5.67/2.06 | 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 yields: % 5.67/2.06 | (1) the_carrier(all_0_8_8) = all_0_7_7 & the_carrier(all_0_11_11) = all_0_10_10 & powerset(all_0_7_7) = all_0_6_6 & powerset(all_0_10_10) = all_0_9_9 & interior(all_0_8_8, all_0_3_3) = all_0_2_2 & interior(all_0_11_11, all_0_5_5) = all_0_4_4 & topological_space(all_0_11_11) & one_sorted_str(all_0_1_1) & element(all_0_3_3, all_0_6_6) & element(all_0_5_5, all_0_9_9) & top_str(all_0_0_0) & top_str(all_0_8_8) & top_str(all_0_11_11) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (subset_complement(v0, v2) = v3) | ~ (subset_complement(v0, v1) = v2) | ? [v4] : (powerset(v0) = v4 & ~ element(v1, v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (interior(v3, v2) = v1) | ~ (interior(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (topstr_closure(v3, v2) = v1) | ~ (topstr_closure(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (the_carrier(v0) = v2) | ~ (subset_complement(v2, v1) = v3) | ~ open_subset(v1, v0) | ~ topological_space(v0) | ~ top_str(v0) | closed_subset(v3, v0) | ? [v4] : (powerset(v2) = v4 & ~ element(v1, v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (the_carrier(v0) = v2) | ~ (subset_complement(v2, v1) = v3) | ~ closed_subset(v1, v0) | ~ topological_space(v0) | ~ top_str(v0) | open_subset(v3, v0) | ? [v4] : (powerset(v2) = v4 & ~ element(v1, v4))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ subset(v0, v1) | element(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ element(v0, v2) | subset(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (interior(v0, v1) = v2) | ~ topological_space(v0) | ~ top_str(v0) | open_subset(v2, v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ~ element(v1, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (interior(v0, v1) = v2) | ~ top_str(v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ( ~ element(v1, v4) | element(v2, v4)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (topstr_closure(v0, v1) = v2) | ~ topological_space(v0) | ~ top_str(v0) | closed_subset(v2, v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ~ element(v1, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (topstr_closure(v0, v1) = v2) | ~ top_str(v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ( ~ element(v1, v4) | element(v2, v4)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : (powerset(v0) = v3 & ( ~ element(v1, v3) | element(v2, v3)))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & open_subset(v3, v0) & closed_subset(v3, v0) & element(v3, v2))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & open_subset(v3, v0) & element(v3, v2))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & closed_subset(v3, v0) & element(v3, v2))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (topstr_closure(v0, v4) = v5) | ~ (subset_complement(v1, v5) = v6) | ~ (subset_complement(v1, v3) = v4) | ~ element(v3, v2) | interior(v0, v3) = v6) & ! [v3] : ! [v4] : ( ~ (interior(v0, v3) = v4) | ~ element(v3, v2) | ? [v5] : ? [v6] : (topstr_closure(v0, v5) = v6 & subset_complement(v1, v6) = v4 & subset_complement(v1, v3) = v5)))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : (v4 = v3 | ~ (topstr_closure(v0, v3) = v4) | ~ closed_subset(v3, v0) | ~ element(v3, v2)) & ! [v3] : ( ~ (topstr_closure(v0, v3) = v3) | ~ topological_space(v0) | ~ element(v3, v2) | closed_subset(v3, v0)))) & ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : ( ~ (subset_complement(v1, v3) = v4) | ~ open_subset(v3, v0) | ~ element(v3, v2) | closed_subset(v4, v0)) & ! [v3] : ! [v4] : ( ~ (subset_complement(v1, v3) = v4) | ~ closed_subset(v4, v0) | ~ element(v3, v2) | open_subset(v3, v0)))) & ! [v0] : ( ~ top_str(v0) | one_sorted_str(v0)) & ? [v0] : ? [v1] : element(v1, v0) & ? [v0] : subset(v0, v0) & ((all_0_4_4 = all_0_5_5 & ~ open_subset(all_0_5_5, all_0_11_11)) | ( ~ (all_0_2_2 = all_0_3_3) & open_subset(all_0_3_3, all_0_8_8))) % 6.05/2.08 | % 6.05/2.08 | Applying alpha-rule on (1) yields: % 6.05/2.08 | (2) interior(all_0_11_11, all_0_5_5) = all_0_4_4 % 6.05/2.08 | (3) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & open_subset(v3, v0) & closed_subset(v3, v0) & element(v3, v2))) % 6.05/2.08 | (4) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & open_subset(v3, v0) & element(v3, v2))) % 6.05/2.08 | (5) one_sorted_str(all_0_1_1) % 6.05/2.08 | (6) ? [v0] : subset(v0, v0) % 6.05/2.08 | (7) ? [v0] : ? [v1] : element(v1, v0) % 6.05/2.08 | (8) interior(all_0_8_8, all_0_3_3) = all_0_2_2 % 6.05/2.08 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : (powerset(v0) = v3 & ( ~ element(v1, v3) | element(v2, v3)))) % 6.05/2.08 | (10) powerset(all_0_10_10) = all_0_9_9 % 6.05/2.08 | (11) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : (v4 = v3 | ~ (topstr_closure(v0, v3) = v4) | ~ closed_subset(v3, v0) | ~ element(v3, v2)) & ! [v3] : ( ~ (topstr_closure(v0, v3) = v3) | ~ topological_space(v0) | ~ element(v3, v2) | closed_subset(v3, v0)))) % 6.05/2.08 | (12) ! [v0] : ! [v1] : ! [v2] : ( ~ (topstr_closure(v0, v1) = v2) | ~ topological_space(v0) | ~ top_str(v0) | closed_subset(v2, v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ~ element(v1, v4))) % 6.05/2.08 | (13) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ topological_space(v0) | ~ top_str(v0) | ? [v2] : ? [v3] : (powerset(v1) = v2 & closed_subset(v3, v0) & element(v3, v2))) % 6.05/2.08 | (14) element(all_0_5_5, all_0_9_9) % 6.05/2.08 | (15) the_carrier(all_0_11_11) = all_0_10_10 % 6.05/2.08 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (topstr_closure(v3, v2) = v1) | ~ (topstr_closure(v3, v2) = v0)) % 6.05/2.08 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 6.09/2.08 | (18) top_str(all_0_0_0) % 6.09/2.08 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (subset_complement(v0, v2) = v3) | ~ (subset_complement(v0, v1) = v2) | ? [v4] : (powerset(v0) = v4 & ~ element(v1, v4))) % 6.09/2.08 | (20) top_str(all_0_11_11) % 6.09/2.08 | (21) powerset(all_0_7_7) = all_0_6_6 % 6.09/2.08 | (22) the_carrier(all_0_8_8) = all_0_7_7 % 6.09/2.08 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ (interior(v0, v1) = v2) | ~ top_str(v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ( ~ element(v1, v4) | element(v2, v4)))) % 6.09/2.08 | (24) ! [v0] : ( ~ top_str(v0) | one_sorted_str(v0)) % 6.09/2.08 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (the_carrier(v0) = v2) | ~ (subset_complement(v2, v1) = v3) | ~ open_subset(v1, v0) | ~ topological_space(v0) | ~ top_str(v0) | closed_subset(v3, v0) | ? [v4] : (powerset(v2) = v4 & ~ element(v1, v4))) % 6.09/2.08 | (26) top_str(all_0_8_8) % 6.09/2.08 | (27) element(all_0_3_3, all_0_6_6) % 6.09/2.08 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (interior(v3, v2) = v1) | ~ (interior(v3, v2) = v0)) % 6.09/2.08 | (29) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : ( ~ (subset_complement(v1, v3) = v4) | ~ open_subset(v3, v0) | ~ element(v3, v2) | closed_subset(v4, v0)) & ! [v3] : ! [v4] : ( ~ (subset_complement(v1, v3) = v4) | ~ closed_subset(v4, v0) | ~ element(v3, v2) | open_subset(v3, v0)))) % 6.09/2.08 | (30) topological_space(all_0_11_11) % 6.09/2.08 | (31) (all_0_4_4 = all_0_5_5 & ~ open_subset(all_0_5_5, all_0_11_11)) | ( ~ (all_0_2_2 = all_0_3_3) & open_subset(all_0_3_3, all_0_8_8)) % 6.09/2.08 | (32) ! [v0] : ! [v1] : ( ~ (the_carrier(v0) = v1) | ~ top_str(v0) | ? [v2] : (powerset(v1) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (topstr_closure(v0, v4) = v5) | ~ (subset_complement(v1, v5) = v6) | ~ (subset_complement(v1, v3) = v4) | ~ element(v3, v2) | interior(v0, v3) = v6) & ! [v3] : ! [v4] : ( ~ (interior(v0, v3) = v4) | ~ element(v3, v2) | ? [v5] : ? [v6] : (topstr_closure(v0, v5) = v6 & subset_complement(v1, v6) = v4 & subset_complement(v1, v3) = v5)))) % 6.09/2.09 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) % 6.09/2.09 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (topstr_closure(v0, v1) = v2) | ~ top_str(v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ( ~ element(v1, v4) | element(v2, v4)))) % 6.09/2.09 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) % 6.09/2.09 | (36) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ element(v0, v2) | subset(v0, v1)) % 6.09/2.09 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ subset(v0, v1) | element(v0, v2)) % 6.09/2.09 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (the_carrier(v0) = v2) | ~ (subset_complement(v2, v1) = v3) | ~ closed_subset(v1, v0) | ~ topological_space(v0) | ~ top_str(v0) | open_subset(v3, v0) | ? [v4] : (powerset(v2) = v4 & ~ element(v1, v4))) % 6.09/2.09 | (39) ! [v0] : ! [v1] : ! [v2] : ( ~ (interior(v0, v1) = v2) | ~ topological_space(v0) | ~ top_str(v0) | open_subset(v2, v0) | ? [v3] : ? [v4] : (the_carrier(v0) = v3 & powerset(v3) = v4 & ~ element(v1, v4))) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (32) with all_0_7_7, all_0_8_8 and discharging atoms the_carrier(all_0_8_8) = all_0_7_7, top_str(all_0_8_8), yields: % 6.09/2.09 | (40) ? [v0] : (powerset(all_0_7_7) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (topstr_closure(all_0_8_8, v2) = v3) | ~ (subset_complement(all_0_7_7, v3) = v4) | ~ (subset_complement(all_0_7_7, v1) = v2) | ~ element(v1, v0) | interior(all_0_8_8, v1) = v4) & ! [v1] : ! [v2] : ( ~ (interior(all_0_8_8, v1) = v2) | ~ element(v1, v0) | ? [v3] : ? [v4] : (topstr_closure(all_0_8_8, v3) = v4 & subset_complement(all_0_7_7, v4) = v2 & subset_complement(all_0_7_7, v1) = v3))) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (11) with all_0_7_7, all_0_8_8 and discharging atoms the_carrier(all_0_8_8) = all_0_7_7, top_str(all_0_8_8), yields: % 6.09/2.09 | (41) ? [v0] : (powerset(all_0_7_7) = v0 & ! [v1] : ! [v2] : (v2 = v1 | ~ (topstr_closure(all_0_8_8, v1) = v2) | ~ closed_subset(v1, all_0_8_8) | ~ element(v1, v0)) & ! [v1] : ( ~ (topstr_closure(all_0_8_8, v1) = v1) | ~ topological_space(all_0_8_8) | ~ element(v1, v0) | closed_subset(v1, all_0_8_8))) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (29) with all_0_7_7, all_0_8_8 and discharging atoms the_carrier(all_0_8_8) = all_0_7_7, top_str(all_0_8_8), yields: % 6.09/2.09 | (42) ? [v0] : (powerset(all_0_7_7) = v0 & ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_7_7, v1) = v2) | ~ open_subset(v1, all_0_8_8) | ~ element(v1, v0) | closed_subset(v2, all_0_8_8)) & ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_7_7, v1) = v2) | ~ closed_subset(v2, all_0_8_8) | ~ element(v1, v0) | open_subset(v1, all_0_8_8))) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (23) with all_0_2_2, all_0_3_3, all_0_8_8 and discharging atoms interior(all_0_8_8, all_0_3_3) = all_0_2_2, top_str(all_0_8_8), yields: % 6.09/2.09 | (43) ? [v0] : ? [v1] : (the_carrier(all_0_8_8) = v0 & powerset(v0) = v1 & ( ~ element(all_0_3_3, v1) | element(all_0_2_2, v1))) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (3) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, topological_space(all_0_11_11), top_str(all_0_11_11), yields: % 6.09/2.09 | (44) ? [v0] : ? [v1] : (powerset(all_0_10_10) = v0 & open_subset(v1, all_0_11_11) & closed_subset(v1, all_0_11_11) & element(v1, v0)) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (4) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, topological_space(all_0_11_11), top_str(all_0_11_11), yields: % 6.09/2.09 | (45) ? [v0] : ? [v1] : (powerset(all_0_10_10) = v0 & open_subset(v1, all_0_11_11) & element(v1, v0)) % 6.09/2.09 | % 6.09/2.09 | Instantiating formula (13) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, topological_space(all_0_11_11), top_str(all_0_11_11), yields: % 6.09/2.10 | (46) ? [v0] : ? [v1] : (powerset(all_0_10_10) = v0 & closed_subset(v1, all_0_11_11) & element(v1, v0)) % 6.09/2.10 | % 6.09/2.10 | Instantiating formula (32) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, top_str(all_0_11_11), yields: % 6.09/2.10 | (47) ? [v0] : (powerset(all_0_10_10) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (topstr_closure(all_0_11_11, v2) = v3) | ~ (subset_complement(all_0_10_10, v3) = v4) | ~ (subset_complement(all_0_10_10, v1) = v2) | ~ element(v1, v0) | interior(all_0_11_11, v1) = v4) & ! [v1] : ! [v2] : ( ~ (interior(all_0_11_11, v1) = v2) | ~ element(v1, v0) | ? [v3] : ? [v4] : (topstr_closure(all_0_11_11, v3) = v4 & subset_complement(all_0_10_10, v4) = v2 & subset_complement(all_0_10_10, v1) = v3))) % 6.09/2.10 | % 6.09/2.10 | Instantiating formula (11) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, top_str(all_0_11_11), yields: % 6.09/2.10 | (48) ? [v0] : (powerset(all_0_10_10) = v0 & ! [v1] : ! [v2] : (v2 = v1 | ~ (topstr_closure(all_0_11_11, v1) = v2) | ~ closed_subset(v1, all_0_11_11) | ~ element(v1, v0)) & ! [v1] : ( ~ (topstr_closure(all_0_11_11, v1) = v1) | ~ topological_space(all_0_11_11) | ~ element(v1, v0) | closed_subset(v1, all_0_11_11))) % 6.09/2.10 | % 6.09/2.10 | Instantiating formula (29) with all_0_10_10, all_0_11_11 and discharging atoms the_carrier(all_0_11_11) = all_0_10_10, top_str(all_0_11_11), yields: % 6.09/2.10 | (49) ? [v0] : (powerset(all_0_10_10) = v0 & ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_10_10, v1) = v2) | ~ open_subset(v1, all_0_11_11) | ~ element(v1, v0) | closed_subset(v2, all_0_11_11)) & ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_10_10, v1) = v2) | ~ closed_subset(v2, all_0_11_11) | ~ element(v1, v0) | open_subset(v1, all_0_11_11))) % 6.09/2.10 | % 6.09/2.10 | Instantiating formula (39) with all_0_4_4, all_0_5_5, all_0_11_11 and discharging atoms interior(all_0_11_11, all_0_5_5) = all_0_4_4, topological_space(all_0_11_11), top_str(all_0_11_11), yields: % 6.09/2.10 | (50) open_subset(all_0_4_4, all_0_11_11) | ? [v0] : ? [v1] : (the_carrier(all_0_11_11) = v0 & powerset(v0) = v1 & ~ element(all_0_5_5, v1)) % 6.09/2.10 | % 6.09/2.10 | Instantiating formula (23) with all_0_4_4, all_0_5_5, all_0_11_11 and discharging atoms interior(all_0_11_11, all_0_5_5) = all_0_4_4, top_str(all_0_11_11), yields: % 6.09/2.10 | (51) ? [v0] : ? [v1] : (the_carrier(all_0_11_11) = v0 & powerset(v0) = v1 & ( ~ element(all_0_5_5, v1) | element(all_0_4_4, v1))) % 6.09/2.10 | % 6.09/2.10 | Instantiating (46) with all_13_0_15, all_13_1_16 yields: % 6.09/2.10 | (52) powerset(all_0_10_10) = all_13_1_16 & closed_subset(all_13_0_15, all_0_11_11) & element(all_13_0_15, all_13_1_16) % 6.09/2.10 | % 6.09/2.10 | Applying alpha-rule on (52) yields: % 6.09/2.10 | (53) powerset(all_0_10_10) = all_13_1_16 % 6.09/2.10 | (54) closed_subset(all_13_0_15, all_0_11_11) % 6.09/2.10 | (55) element(all_13_0_15, all_13_1_16) % 6.09/2.10 | % 6.09/2.10 | Instantiating (45) with all_15_0_17, all_15_1_18 yields: % 6.09/2.10 | (56) powerset(all_0_10_10) = all_15_1_18 & open_subset(all_15_0_17, all_0_11_11) & element(all_15_0_17, all_15_1_18) % 6.09/2.10 | % 6.09/2.10 | Applying alpha-rule on (56) yields: % 6.09/2.10 | (57) powerset(all_0_10_10) = all_15_1_18 % 6.09/2.10 | (58) open_subset(all_15_0_17, all_0_11_11) % 6.09/2.10 | (59) element(all_15_0_17, all_15_1_18) % 6.09/2.10 | % 6.09/2.10 | Instantiating (49) with all_17_0_19 yields: % 6.09/2.10 | (60) powerset(all_0_10_10) = all_17_0_19 & ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_10_10, v0) = v1) | ~ open_subset(v0, all_0_11_11) | ~ element(v0, all_17_0_19) | closed_subset(v1, all_0_11_11)) & ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_10_10, v0) = v1) | ~ closed_subset(v1, all_0_11_11) | ~ element(v0, all_17_0_19) | open_subset(v0, all_0_11_11)) % 6.09/2.10 | % 6.09/2.10 | Applying alpha-rule on (60) yields: % 6.09/2.10 | (61) powerset(all_0_10_10) = all_17_0_19 % 6.09/2.10 | (62) ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_10_10, v0) = v1) | ~ open_subset(v0, all_0_11_11) | ~ element(v0, all_17_0_19) | closed_subset(v1, all_0_11_11)) % 6.09/2.10 | (63) ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_10_10, v0) = v1) | ~ closed_subset(v1, all_0_11_11) | ~ element(v0, all_17_0_19) | open_subset(v0, all_0_11_11)) % 6.09/2.10 | % 6.09/2.10 | Instantiating (48) with all_20_0_20 yields: % 6.09/2.10 | (64) powerset(all_0_10_10) = all_20_0_20 & ! [v0] : ! [v1] : (v1 = v0 | ~ (topstr_closure(all_0_11_11, v0) = v1) | ~ closed_subset(v0, all_0_11_11) | ~ element(v0, all_20_0_20)) & ! [v0] : ( ~ (topstr_closure(all_0_11_11, v0) = v0) | ~ topological_space(all_0_11_11) | ~ element(v0, all_20_0_20) | closed_subset(v0, all_0_11_11)) % 6.09/2.10 | % 6.09/2.10 | Applying alpha-rule on (64) yields: % 6.09/2.10 | (65) powerset(all_0_10_10) = all_20_0_20 % 6.09/2.10 | (66) ! [v0] : ! [v1] : (v1 = v0 | ~ (topstr_closure(all_0_11_11, v0) = v1) | ~ closed_subset(v0, all_0_11_11) | ~ element(v0, all_20_0_20)) % 6.09/2.10 | (67) ! [v0] : ( ~ (topstr_closure(all_0_11_11, v0) = v0) | ~ topological_space(all_0_11_11) | ~ element(v0, all_20_0_20) | closed_subset(v0, all_0_11_11)) % 6.09/2.10 | % 6.09/2.10 | Instantiating (51) with all_23_0_21, all_23_1_22 yields: % 6.09/2.10 | (68) the_carrier(all_0_11_11) = all_23_1_22 & powerset(all_23_1_22) = all_23_0_21 & ( ~ element(all_0_5_5, all_23_0_21) | element(all_0_4_4, all_23_0_21)) % 6.09/2.10 | % 6.09/2.10 | Applying alpha-rule on (68) yields: % 6.09/2.10 | (69) the_carrier(all_0_11_11) = all_23_1_22 % 6.09/2.10 | (70) powerset(all_23_1_22) = all_23_0_21 % 6.09/2.10 | (71) ~ element(all_0_5_5, all_23_0_21) | element(all_0_4_4, all_23_0_21) % 6.09/2.10 | % 6.09/2.10 | Instantiating (44) with all_25_0_23, all_25_1_24 yields: % 6.09/2.11 | (72) powerset(all_0_10_10) = all_25_1_24 & open_subset(all_25_0_23, all_0_11_11) & closed_subset(all_25_0_23, all_0_11_11) & element(all_25_0_23, all_25_1_24) % 6.09/2.11 | % 6.09/2.11 | Applying alpha-rule on (72) yields: % 6.09/2.11 | (73) powerset(all_0_10_10) = all_25_1_24 % 6.09/2.11 | (74) open_subset(all_25_0_23, all_0_11_11) % 6.09/2.11 | (75) closed_subset(all_25_0_23, all_0_11_11) % 6.09/2.11 | (76) element(all_25_0_23, all_25_1_24) % 6.09/2.11 | % 6.09/2.11 | Instantiating (47) with all_27_0_25 yields: % 6.09/2.11 | (77) powerset(all_0_10_10) = all_27_0_25 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (topstr_closure(all_0_11_11, v1) = v2) | ~ (subset_complement(all_0_10_10, v2) = v3) | ~ (subset_complement(all_0_10_10, v0) = v1) | ~ element(v0, all_27_0_25) | interior(all_0_11_11, v0) = v3) & ! [v0] : ! [v1] : ( ~ (interior(all_0_11_11, v0) = v1) | ~ element(v0, all_27_0_25) | ? [v2] : ? [v3] : (topstr_closure(all_0_11_11, v2) = v3 & subset_complement(all_0_10_10, v3) = v1 & subset_complement(all_0_10_10, v0) = v2)) % 6.09/2.11 | % 6.09/2.11 | Applying alpha-rule on (77) yields: % 6.09/2.11 | (78) powerset(all_0_10_10) = all_27_0_25 % 6.22/2.11 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (topstr_closure(all_0_11_11, v1) = v2) | ~ (subset_complement(all_0_10_10, v2) = v3) | ~ (subset_complement(all_0_10_10, v0) = v1) | ~ element(v0, all_27_0_25) | interior(all_0_11_11, v0) = v3) % 6.22/2.11 | (80) ! [v0] : ! [v1] : ( ~ (interior(all_0_11_11, v0) = v1) | ~ element(v0, all_27_0_25) | ? [v2] : ? [v3] : (topstr_closure(all_0_11_11, v2) = v3 & subset_complement(all_0_10_10, v3) = v1 & subset_complement(all_0_10_10, v0) = v2)) % 6.22/2.11 | % 6.22/2.11 | Instantiating (43) with all_30_0_26, all_30_1_27 yields: % 6.22/2.11 | (81) the_carrier(all_0_8_8) = all_30_1_27 & powerset(all_30_1_27) = all_30_0_26 & ( ~ element(all_0_3_3, all_30_0_26) | element(all_0_2_2, all_30_0_26)) % 6.22/2.11 | % 6.22/2.11 | Applying alpha-rule on (81) yields: % 6.22/2.11 | (82) the_carrier(all_0_8_8) = all_30_1_27 % 6.22/2.11 | (83) powerset(all_30_1_27) = all_30_0_26 % 6.22/2.11 | (84) ~ element(all_0_3_3, all_30_0_26) | element(all_0_2_2, all_30_0_26) % 6.22/2.11 | % 6.22/2.11 | Instantiating (41) with all_32_0_28 yields: % 6.22/2.11 | (85) powerset(all_0_7_7) = all_32_0_28 & ! [v0] : ! [v1] : (v1 = v0 | ~ (topstr_closure(all_0_8_8, v0) = v1) | ~ closed_subset(v0, all_0_8_8) | ~ element(v0, all_32_0_28)) & ! [v0] : ( ~ (topstr_closure(all_0_8_8, v0) = v0) | ~ topological_space(all_0_8_8) | ~ element(v0, all_32_0_28) | closed_subset(v0, all_0_8_8)) % 6.22/2.11 | % 6.22/2.11 | Applying alpha-rule on (85) yields: % 6.22/2.11 | (86) powerset(all_0_7_7) = all_32_0_28 % 6.22/2.11 | (87) ! [v0] : ! [v1] : (v1 = v0 | ~ (topstr_closure(all_0_8_8, v0) = v1) | ~ closed_subset(v0, all_0_8_8) | ~ element(v0, all_32_0_28)) % 6.22/2.11 | (88) ! [v0] : ( ~ (topstr_closure(all_0_8_8, v0) = v0) | ~ topological_space(all_0_8_8) | ~ element(v0, all_32_0_28) | closed_subset(v0, all_0_8_8)) % 6.22/2.11 | % 6.22/2.11 | Instantiating (40) with all_35_0_29 yields: % 6.22/2.11 | (89) powerset(all_0_7_7) = all_35_0_29 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (topstr_closure(all_0_8_8, v1) = v2) | ~ (subset_complement(all_0_7_7, v2) = v3) | ~ (subset_complement(all_0_7_7, v0) = v1) | ~ element(v0, all_35_0_29) | interior(all_0_8_8, v0) = v3) & ! [v0] : ! [v1] : ( ~ (interior(all_0_8_8, v0) = v1) | ~ element(v0, all_35_0_29) | ? [v2] : ? [v3] : (topstr_closure(all_0_8_8, v2) = v3 & subset_complement(all_0_7_7, v3) = v1 & subset_complement(all_0_7_7, v0) = v2)) % 6.22/2.11 | % 6.22/2.11 | Applying alpha-rule on (89) yields: % 6.22/2.11 | (90) powerset(all_0_7_7) = all_35_0_29 % 6.22/2.11 | (91) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (topstr_closure(all_0_8_8, v1) = v2) | ~ (subset_complement(all_0_7_7, v2) = v3) | ~ (subset_complement(all_0_7_7, v0) = v1) | ~ element(v0, all_35_0_29) | interior(all_0_8_8, v0) = v3) % 6.22/2.11 | (92) ! [v0] : ! [v1] : ( ~ (interior(all_0_8_8, v0) = v1) | ~ element(v0, all_35_0_29) | ? [v2] : ? [v3] : (topstr_closure(all_0_8_8, v2) = v3 & subset_complement(all_0_7_7, v3) = v1 & subset_complement(all_0_7_7, v0) = v2)) % 6.22/2.11 | % 6.22/2.11 | Instantiating (42) with all_38_0_30 yields: % 6.22/2.11 | (93) powerset(all_0_7_7) = all_38_0_30 & ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_7_7, v0) = v1) | ~ open_subset(v0, all_0_8_8) | ~ element(v0, all_38_0_30) | closed_subset(v1, all_0_8_8)) & ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_7_7, v0) = v1) | ~ closed_subset(v1, all_0_8_8) | ~ element(v0, all_38_0_30) | open_subset(v0, all_0_8_8)) % 6.22/2.11 | % 6.22/2.11 | Applying alpha-rule on (93) yields: % 6.22/2.11 | (94) powerset(all_0_7_7) = all_38_0_30 % 6.22/2.11 | (95) ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_7_7, v0) = v1) | ~ open_subset(v0, all_0_8_8) | ~ element(v0, all_38_0_30) | closed_subset(v1, all_0_8_8)) % 6.22/2.11 | (96) ! [v0] : ! [v1] : ( ~ (subset_complement(all_0_7_7, v0) = v1) | ~ closed_subset(v1, all_0_8_8) | ~ element(v0, all_38_0_30) | open_subset(v0, all_0_8_8)) % 6.22/2.11 | % 6.22/2.11 | Instantiating formula (33) with all_0_8_8, all_30_1_27, all_0_7_7 and discharging atoms the_carrier(all_0_8_8) = all_30_1_27, the_carrier(all_0_8_8) = all_0_7_7, yields: % 6.22/2.11 | (97) all_30_1_27 = all_0_7_7 % 6.22/2.11 | % 6.22/2.11 | Instantiating formula (33) with all_0_11_11, all_23_1_22, all_0_10_10 and discharging atoms the_carrier(all_0_11_11) = all_23_1_22, the_carrier(all_0_11_11) = all_0_10_10, yields: % 6.22/2.12 | (98) all_23_1_22 = all_0_10_10 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_7_7, all_35_0_29, all_0_6_6 and discharging atoms powerset(all_0_7_7) = all_35_0_29, powerset(all_0_7_7) = all_0_6_6, yields: % 6.22/2.12 | (99) all_35_0_29 = all_0_6_6 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_7_7, all_35_0_29, all_38_0_30 and discharging atoms powerset(all_0_7_7) = all_38_0_30, powerset(all_0_7_7) = all_35_0_29, yields: % 6.22/2.12 | (100) all_38_0_30 = all_35_0_29 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_7_7, all_32_0_28, all_38_0_30 and discharging atoms powerset(all_0_7_7) = all_38_0_30, powerset(all_0_7_7) = all_32_0_28, yields: % 6.22/2.12 | (101) all_38_0_30 = all_32_0_28 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_20_0_20, all_0_9_9 and discharging atoms powerset(all_0_10_10) = all_20_0_20, powerset(all_0_10_10) = all_0_9_9, yields: % 6.22/2.12 | (102) all_20_0_20 = all_0_9_9 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_20_0_20, all_25_1_24 and discharging atoms powerset(all_0_10_10) = all_25_1_24, powerset(all_0_10_10) = all_20_0_20, yields: % 6.22/2.12 | (103) all_25_1_24 = all_20_0_20 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_17_0_19, all_27_0_25 and discharging atoms powerset(all_0_10_10) = all_27_0_25, powerset(all_0_10_10) = all_17_0_19, yields: % 6.22/2.12 | (104) all_27_0_25 = all_17_0_19 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_17_0_19, all_20_0_20 and discharging atoms powerset(all_0_10_10) = all_20_0_20, powerset(all_0_10_10) = all_17_0_19, yields: % 6.22/2.12 | (105) all_20_0_20 = all_17_0_19 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_15_1_18, all_25_1_24 and discharging atoms powerset(all_0_10_10) = all_25_1_24, powerset(all_0_10_10) = all_15_1_18, yields: % 6.22/2.12 | (106) all_25_1_24 = all_15_1_18 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_10_10, all_13_1_16, all_27_0_25 and discharging atoms powerset(all_0_10_10) = all_27_0_25, powerset(all_0_10_10) = all_13_1_16, yields: % 6.22/2.12 | (107) all_27_0_25 = all_13_1_16 % 6.22/2.12 | % 6.22/2.12 | Combining equations (100,101) yields a new equation: % 6.22/2.12 | (108) all_35_0_29 = all_32_0_28 % 6.22/2.12 | % 6.22/2.12 | Simplifying 108 yields: % 6.22/2.12 | (109) all_35_0_29 = all_32_0_28 % 6.22/2.12 | % 6.22/2.12 | Combining equations (109,99) yields a new equation: % 6.22/2.12 | (110) all_32_0_28 = all_0_6_6 % 6.22/2.12 | % 6.22/2.12 | Simplifying 110 yields: % 6.22/2.12 | (111) all_32_0_28 = all_0_6_6 % 6.22/2.12 | % 6.22/2.12 | Combining equations (104,107) yields a new equation: % 6.22/2.12 | (112) all_17_0_19 = all_13_1_16 % 6.22/2.12 | % 6.22/2.12 | Simplifying 112 yields: % 6.22/2.12 | (113) all_17_0_19 = all_13_1_16 % 6.22/2.12 | % 6.22/2.12 | Combining equations (103,106) yields a new equation: % 6.22/2.12 | (114) all_20_0_20 = all_15_1_18 % 6.22/2.12 | % 6.22/2.12 | Simplifying 114 yields: % 6.22/2.12 | (115) all_20_0_20 = all_15_1_18 % 6.22/2.12 | % 6.22/2.12 | Combining equations (105,115) yields a new equation: % 6.22/2.12 | (116) all_17_0_19 = all_15_1_18 % 6.22/2.12 | % 6.22/2.12 | Simplifying 116 yields: % 6.22/2.12 | (117) all_17_0_19 = all_15_1_18 % 6.22/2.12 | % 6.22/2.12 | Combining equations (102,115) yields a new equation: % 6.22/2.12 | (118) all_15_1_18 = all_0_9_9 % 6.22/2.12 | % 6.22/2.12 | Combining equations (117,113) yields a new equation: % 6.22/2.12 | (119) all_15_1_18 = all_13_1_16 % 6.22/2.12 | % 6.22/2.12 | Simplifying 119 yields: % 6.22/2.12 | (120) all_15_1_18 = all_13_1_16 % 6.22/2.12 | % 6.22/2.12 | Combining equations (120,118) yields a new equation: % 6.22/2.12 | (121) all_13_1_16 = all_0_9_9 % 6.22/2.12 | % 6.22/2.12 | Simplifying 121 yields: % 6.22/2.12 | (122) all_13_1_16 = all_0_9_9 % 6.22/2.12 | % 6.22/2.12 | Combining equations (111,101) yields a new equation: % 6.22/2.12 | (123) all_38_0_30 = all_0_6_6 % 6.22/2.12 | % 6.22/2.12 | From (97) and (82) follows: % 6.22/2.12 | (22) the_carrier(all_0_8_8) = all_0_7_7 % 6.22/2.12 | % 6.22/2.12 | From (98) and (69) follows: % 6.22/2.12 | (15) the_carrier(all_0_11_11) = all_0_10_10 % 6.22/2.12 | % 6.22/2.12 | From (97) and (83) follows: % 6.22/2.12 | (126) powerset(all_0_7_7) = all_30_0_26 % 6.22/2.12 | % 6.22/2.12 | From (98) and (70) follows: % 6.22/2.12 | (127) powerset(all_0_10_10) = all_23_0_21 % 6.22/2.12 | % 6.22/2.12 | From (111) and (86) follows: % 6.22/2.12 | (21) powerset(all_0_7_7) = all_0_6_6 % 6.22/2.12 | % 6.22/2.12 | From (122) and (53) follows: % 6.22/2.12 | (10) powerset(all_0_10_10) = all_0_9_9 % 6.22/2.12 | % 6.22/2.12 | Instantiating formula (17) with all_0_7_7, all_30_0_26, all_0_6_6 and discharging atoms powerset(all_0_7_7) = all_30_0_26, powerset(all_0_7_7) = all_0_6_6, yields: % 6.22/2.12 | (130) all_30_0_26 = all_0_6_6 % 6.22/2.13 | % 6.22/2.13 | Instantiating formula (17) with all_0_10_10, all_23_0_21, all_0_9_9 and discharging atoms powerset(all_0_10_10) = all_23_0_21, powerset(all_0_10_10) = all_0_9_9, yields: % 6.22/2.13 | (131) all_23_0_21 = all_0_9_9 % 6.22/2.13 | % 6.22/2.13 | From (130) and (126) follows: % 6.22/2.13 | (21) powerset(all_0_7_7) = all_0_6_6 % 6.22/2.13 | % 6.22/2.13 | From (131) and (127) follows: % 6.22/2.13 | (10) powerset(all_0_10_10) = all_0_9_9 % 6.22/2.13 | % 6.22/2.13 +-Applying beta-rule and splitting (50), into two cases. % 6.22/2.13 |-Branch one: % 6.22/2.13 | (134) open_subset(all_0_4_4, all_0_11_11) % 6.22/2.13 | % 6.22/2.13 +-Applying beta-rule and splitting (84), into two cases. % 6.22/2.13 |-Branch one: % 6.22/2.13 | (135) ~ element(all_0_3_3, all_30_0_26) % 6.22/2.13 | % 6.22/2.13 | From (130) and (135) follows: % 6.22/2.13 | (136) ~ element(all_0_3_3, all_0_6_6) % 6.22/2.13 | % 6.22/2.13 | Using (27) and (136) yields: % 6.22/2.13 | (137) $false % 6.22/2.13 | % 6.22/2.13 |-The branch is then unsatisfiable % 6.22/2.13 |-Branch two: % 6.22/2.13 | (138) element(all_0_3_3, all_30_0_26) % 6.22/2.13 | (139) element(all_0_2_2, all_30_0_26) % 6.22/2.13 | % 6.22/2.13 | From (130) and (138) follows: % 6.22/2.13 | (27) element(all_0_3_3, all_0_6_6) % 6.22/2.13 | % 6.22/2.13 +-Applying beta-rule and splitting (31), into two cases. % 6.22/2.13 |-Branch one: % 6.22/2.13 | (141) all_0_4_4 = all_0_5_5 & ~ open_subset(all_0_5_5, all_0_11_11) % 6.22/2.13 | % 6.22/2.13 | Applying alpha-rule on (141) yields: % 6.22/2.13 | (142) all_0_4_4 = all_0_5_5 % 6.22/2.13 | (143) ~ open_subset(all_0_5_5, all_0_11_11) % 6.22/2.13 | % 6.22/2.13 | From (142) and (134) follows: % 6.22/2.13 | (144) open_subset(all_0_5_5, all_0_11_11) % 6.22/2.13 | % 6.22/2.13 | Using (144) and (143) yields: % 6.22/2.13 | (137) $false % 6.22/2.13 | % 6.22/2.13 |-The branch is then unsatisfiable % 6.22/2.13 |-Branch two: % 6.22/2.13 | (146) ~ (all_0_2_2 = all_0_3_3) & open_subset(all_0_3_3, all_0_8_8) % 6.22/2.13 | % 6.22/2.13 | Applying alpha-rule on (146) yields: % 6.22/2.13 | (147) ~ (all_0_2_2 = all_0_3_3) % 6.22/2.13 | (148) open_subset(all_0_3_3, all_0_8_8) % 6.22/2.13 | % 6.22/2.13 | Instantiating formula (92) with all_0_2_2, all_0_3_3 and discharging atoms interior(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 6.22/2.13 | (149) ~ element(all_0_3_3, all_35_0_29) | ? [v0] : ? [v1] : (topstr_closure(all_0_8_8, v0) = v1 & subset_complement(all_0_7_7, v1) = all_0_2_2 & subset_complement(all_0_7_7, all_0_3_3) = v0) % 6.22/2.13 | % 6.22/2.13 +-Applying beta-rule and splitting (149), into two cases. % 6.22/2.13 |-Branch one: % 6.22/2.13 | (150) ~ element(all_0_3_3, all_35_0_29) % 6.22/2.13 | % 6.22/2.13 | From (99) and (150) follows: % 6.22/2.13 | (136) ~ element(all_0_3_3, all_0_6_6) % 6.22/2.13 | % 6.22/2.13 | Using (27) and (136) yields: % 6.22/2.13 | (137) $false % 6.22/2.13 | % 6.22/2.13 |-The branch is then unsatisfiable % 6.22/2.13 |-Branch two: % 6.22/2.13 | (153) element(all_0_3_3, all_35_0_29) % 6.22/2.13 | (154) ? [v0] : ? [v1] : (topstr_closure(all_0_8_8, v0) = v1 & subset_complement(all_0_7_7, v1) = all_0_2_2 & subset_complement(all_0_7_7, all_0_3_3) = v0) % 6.22/2.13 | % 6.22/2.13 | Instantiating (154) with all_109_0_33, all_109_1_34 yields: % 6.22/2.13 | (155) topstr_closure(all_0_8_8, all_109_1_34) = all_109_0_33 & subset_complement(all_0_7_7, all_109_0_33) = all_0_2_2 & subset_complement(all_0_7_7, all_0_3_3) = all_109_1_34 % 6.22/2.13 | % 6.22/2.13 | Applying alpha-rule on (155) yields: % 6.22/2.13 | (156) topstr_closure(all_0_8_8, all_109_1_34) = all_109_0_33 % 6.22/2.13 | (157) subset_complement(all_0_7_7, all_109_0_33) = all_0_2_2 % 6.22/2.13 | (158) subset_complement(all_0_7_7, all_0_3_3) = all_109_1_34 % 6.22/2.13 | % 6.22/2.13 | From (99) and (153) follows: % 6.22/2.13 | (27) element(all_0_3_3, all_0_6_6) % 6.22/2.13 | % 6.22/2.13 | Instantiating formula (34) with all_109_0_33, all_109_1_34, all_0_8_8 and discharging atoms topstr_closure(all_0_8_8, all_109_1_34) = all_109_0_33, top_str(all_0_8_8), yields: % 6.22/2.13 | (160) ? [v0] : ? [v1] : (the_carrier(all_0_8_8) = v0 & powerset(v0) = v1 & ( ~ element(all_109_1_34, v1) | element(all_109_0_33, v1))) % 6.22/2.14 | % 6.22/2.14 | Instantiating formula (95) with all_109_1_34, all_0_3_3 and discharging atoms subset_complement(all_0_7_7, all_0_3_3) = all_109_1_34, open_subset(all_0_3_3, all_0_8_8), yields: % 6.22/2.14 | (161) ~ element(all_0_3_3, all_38_0_30) | closed_subset(all_109_1_34, all_0_8_8) % 6.22/2.14 | % 6.22/2.14 | Instantiating formula (9) with all_109_1_34, all_0_3_3, all_0_7_7 and discharging atoms subset_complement(all_0_7_7, all_0_3_3) = all_109_1_34, yields: % 6.22/2.14 | (162) ? [v0] : (powerset(all_0_7_7) = v0 & ( ~ element(all_0_3_3, v0) | element(all_109_1_34, v0))) % 6.22/2.14 | % 6.22/2.14 | Instantiating (162) with all_124_0_38 yields: % 6.22/2.14 | (163) powerset(all_0_7_7) = all_124_0_38 & ( ~ element(all_0_3_3, all_124_0_38) | element(all_109_1_34, all_124_0_38)) % 6.22/2.14 | % 6.22/2.14 | Applying alpha-rule on (163) yields: % 6.22/2.14 | (164) powerset(all_0_7_7) = all_124_0_38 % 6.22/2.14 | (165) ~ element(all_0_3_3, all_124_0_38) | element(all_109_1_34, all_124_0_38) % 6.22/2.14 | % 6.22/2.14 | Instantiating (160) with all_126_0_39, all_126_1_40 yields: % 6.22/2.14 | (166) the_carrier(all_0_8_8) = all_126_1_40 & powerset(all_126_1_40) = all_126_0_39 & ( ~ element(all_109_1_34, all_126_0_39) | element(all_109_0_33, all_126_0_39)) % 6.22/2.14 | % 6.22/2.14 | Applying alpha-rule on (166) yields: % 6.22/2.14 | (167) the_carrier(all_0_8_8) = all_126_1_40 % 6.22/2.14 | (168) powerset(all_126_1_40) = all_126_0_39 % 6.22/2.14 | (169) ~ element(all_109_1_34, all_126_0_39) | element(all_109_0_33, all_126_0_39) % 6.22/2.14 | % 6.22/2.14 +-Applying beta-rule and splitting (161), into two cases. % 6.22/2.14 |-Branch one: % 6.22/2.14 | (170) ~ element(all_0_3_3, all_38_0_30) % 6.22/2.14 | % 6.22/2.14 | From (123) and (170) follows: % 6.22/2.14 | (136) ~ element(all_0_3_3, all_0_6_6) % 6.22/2.14 | % 6.22/2.14 | Using (27) and (136) yields: % 6.22/2.14 | (137) $false % 6.22/2.14 | % 6.22/2.14 |-The branch is then unsatisfiable % 6.22/2.14 |-Branch two: % 6.22/2.14 | (173) element(all_0_3_3, all_38_0_30) % 6.22/2.14 | (174) closed_subset(all_109_1_34, all_0_8_8) % 6.22/2.14 | % 6.22/2.14 | From (123) and (173) follows: % 6.22/2.14 | (27) element(all_0_3_3, all_0_6_6) % 6.22/2.14 | % 6.22/2.14 | Instantiating formula (33) with all_0_8_8, all_126_1_40, all_0_7_7 and discharging atoms the_carrier(all_0_8_8) = all_126_1_40, the_carrier(all_0_8_8) = all_0_7_7, yields: % 6.22/2.14 | (176) all_126_1_40 = all_0_7_7 % 6.22/2.14 | % 6.22/2.14 | Instantiating formula (17) with all_0_7_7, all_124_0_38, all_0_6_6 and discharging atoms powerset(all_0_7_7) = all_124_0_38, powerset(all_0_7_7) = all_0_6_6, yields: % 6.22/2.14 | (177) all_124_0_38 = all_0_6_6 % 6.22/2.14 | % 6.22/2.14 | From (176) and (168) follows: % 6.22/2.14 | (178) powerset(all_0_7_7) = all_126_0_39 % 6.22/2.14 | % 6.22/2.14 | From (177) and (164) follows: % 6.22/2.14 | (21) powerset(all_0_7_7) = all_0_6_6 % 6.22/2.14 | % 6.22/2.14 +-Applying beta-rule and splitting (165), into two cases. % 6.22/2.14 |-Branch one: % 6.22/2.14 | (180) ~ element(all_0_3_3, all_124_0_38) % 6.22/2.14 | % 6.22/2.14 | From (177) and (180) follows: % 6.22/2.14 | (136) ~ element(all_0_3_3, all_0_6_6) % 6.22/2.14 | % 6.22/2.14 | Using (27) and (136) yields: % 6.22/2.14 | (137) $false % 6.22/2.14 | % 6.22/2.14 |-The branch is then unsatisfiable % 6.22/2.14 |-Branch two: % 6.22/2.14 | (183) element(all_0_3_3, all_124_0_38) % 6.22/2.14 | (184) element(all_109_1_34, all_124_0_38) % 6.22/2.14 | % 6.22/2.14 | From (177) and (184) follows: % 6.22/2.14 | (185) element(all_109_1_34, all_0_6_6) % 6.38/2.14 | % 6.38/2.14 | From (177) and (183) follows: % 6.38/2.14 | (27) element(all_0_3_3, all_0_6_6) % 6.38/2.14 | % 6.38/2.14 | Instantiating formula (17) with all_0_7_7, all_126_0_39, all_0_6_6 and discharging atoms powerset(all_0_7_7) = all_126_0_39, powerset(all_0_7_7) = all_0_6_6, yields: % 6.38/2.14 | (187) all_126_0_39 = all_0_6_6 % 6.38/2.14 | % 6.38/2.14 | Instantiating formula (87) with all_109_0_33, all_109_1_34 and discharging atoms topstr_closure(all_0_8_8, all_109_1_34) = all_109_0_33, closed_subset(all_109_1_34, all_0_8_8), yields: % 6.38/2.14 | (188) all_109_0_33 = all_109_1_34 | ~ element(all_109_1_34, all_32_0_28) % 6.38/2.14 | % 6.38/2.14 | From (187) and (178) follows: % 6.38/2.14 | (21) powerset(all_0_7_7) = all_0_6_6 % 6.38/2.14 | % 6.38/2.14 +-Applying beta-rule and splitting (169), into two cases. % 6.38/2.14 |-Branch one: % 6.38/2.15 | (190) ~ element(all_109_1_34, all_126_0_39) % 6.38/2.15 | % 6.38/2.15 | From (187) and (190) follows: % 6.38/2.15 | (191) ~ element(all_109_1_34, all_0_6_6) % 6.38/2.15 | % 6.38/2.15 | Using (185) and (191) yields: % 6.38/2.15 | (137) $false % 6.38/2.15 | % 6.38/2.15 |-The branch is then unsatisfiable % 6.38/2.15 |-Branch two: % 6.38/2.15 | (193) element(all_109_1_34, all_126_0_39) % 6.38/2.15 | (194) element(all_109_0_33, all_126_0_39) % 6.38/2.15 | % 6.38/2.15 | From (187) and (193) follows: % 6.38/2.15 | (185) element(all_109_1_34, all_0_6_6) % 6.38/2.15 | % 6.38/2.15 +-Applying beta-rule and splitting (188), into two cases. % 6.38/2.15 |-Branch one: % 6.38/2.15 | (196) ~ element(all_109_1_34, all_32_0_28) % 6.38/2.15 | % 6.38/2.15 | From (111) and (196) follows: % 6.38/2.15 | (191) ~ element(all_109_1_34, all_0_6_6) % 6.38/2.15 | % 6.38/2.15 | Using (185) and (191) yields: % 6.38/2.15 | (137) $false % 6.38/2.15 | % 6.38/2.15 |-The branch is then unsatisfiable % 6.38/2.15 |-Branch two: % 6.38/2.15 | (199) element(all_109_1_34, all_32_0_28) % 6.38/2.15 | (200) all_109_0_33 = all_109_1_34 % 6.38/2.15 | % 6.38/2.15 | From (200) and (157) follows: % 6.38/2.15 | (201) subset_complement(all_0_7_7, all_109_1_34) = all_0_2_2 % 6.38/2.15 | % 6.38/2.15 | Instantiating formula (19) with all_0_2_2, all_109_1_34, all_0_3_3, all_0_7_7 and discharging atoms subset_complement(all_0_7_7, all_109_1_34) = all_0_2_2, subset_complement(all_0_7_7, all_0_3_3) = all_109_1_34, yields: % 6.38/2.15 | (202) all_0_2_2 = all_0_3_3 | ? [v0] : (powerset(all_0_7_7) = v0 & ~ element(all_0_3_3, v0)) % 6.38/2.15 | % 6.38/2.15 +-Applying beta-rule and splitting (202), into two cases. % 6.38/2.15 |-Branch one: % 6.38/2.15 | (203) all_0_2_2 = all_0_3_3 % 6.38/2.15 | % 6.38/2.15 | Equations (203) can reduce 147 to: % 6.38/2.15 | (204) $false % 6.38/2.15 | % 6.38/2.15 |-The branch is then unsatisfiable % 6.38/2.15 |-Branch two: % 6.38/2.15 | (147) ~ (all_0_2_2 = all_0_3_3) % 6.38/2.15 | (206) ? [v0] : (powerset(all_0_7_7) = v0 & ~ element(all_0_3_3, v0)) % 6.38/2.15 | % 6.38/2.15 | Instantiating (206) with all_174_0_41 yields: % 6.38/2.15 | (207) powerset(all_0_7_7) = all_174_0_41 & ~ element(all_0_3_3, all_174_0_41) % 6.38/2.15 | % 6.38/2.15 | Applying alpha-rule on (207) yields: % 6.38/2.15 | (208) powerset(all_0_7_7) = all_174_0_41 % 6.38/2.15 | (209) ~ element(all_0_3_3, all_174_0_41) % 6.38/2.15 | % 6.38/2.15 | Instantiating formula (17) with all_0_7_7, all_174_0_41, all_0_6_6 and discharging atoms powerset(all_0_7_7) = all_174_0_41, powerset(all_0_7_7) = all_0_6_6, yields: % 6.38/2.15 | (210) all_174_0_41 = all_0_6_6 % 6.38/2.15 | % 6.38/2.15 | From (210) and (209) follows: % 6.38/2.15 | (136) ~ element(all_0_3_3, all_0_6_6) % 6.38/2.15 | % 6.38/2.15 | Using (27) and (136) yields: % 6.38/2.15 | (137) $false % 6.38/2.15 | % 6.38/2.15 |-The branch is then unsatisfiable % 6.38/2.15 |-Branch two: % 6.38/2.15 | (213) ~ open_subset(all_0_4_4, all_0_11_11) % 6.38/2.15 | (214) ? [v0] : ? [v1] : (the_carrier(all_0_11_11) = v0 & powerset(v0) = v1 & ~ element(all_0_5_5, v1)) % 6.38/2.15 | % 6.38/2.15 | Instantiating (214) with all_53_0_42, all_53_1_43 yields: % 6.38/2.15 | (215) the_carrier(all_0_11_11) = all_53_1_43 & powerset(all_53_1_43) = all_53_0_42 & ~ element(all_0_5_5, all_53_0_42) % 6.38/2.16 | % 6.38/2.16 | Applying alpha-rule on (215) yields: % 6.38/2.16 | (216) the_carrier(all_0_11_11) = all_53_1_43 % 6.38/2.16 | (217) powerset(all_53_1_43) = all_53_0_42 % 6.38/2.16 | (218) ~ element(all_0_5_5, all_53_0_42) % 6.38/2.16 | % 6.38/2.16 +-Applying beta-rule and splitting (71), into two cases. % 6.38/2.16 |-Branch one: % 6.38/2.16 | (219) ~ element(all_0_5_5, all_23_0_21) % 6.38/2.16 | % 6.38/2.16 | From (131) and (219) follows: % 6.38/2.16 | (220) ~ element(all_0_5_5, all_0_9_9) % 6.38/2.16 | % 6.38/2.16 | Using (14) and (220) yields: % 6.38/2.16 | (137) $false % 6.38/2.16 | % 6.38/2.16 |-The branch is then unsatisfiable % 6.38/2.16 |-Branch two: % 6.38/2.16 | (222) element(all_0_5_5, all_23_0_21) % 6.38/2.16 | (223) element(all_0_4_4, all_23_0_21) % 6.38/2.16 | % 6.38/2.16 | From (131) and (222) follows: % 6.38/2.16 | (14) element(all_0_5_5, all_0_9_9) % 6.38/2.16 | % 6.38/2.16 | Instantiating formula (33) with all_0_11_11, all_53_1_43, all_0_10_10 and discharging atoms the_carrier(all_0_11_11) = all_53_1_43, the_carrier(all_0_11_11) = all_0_10_10, yields: % 6.38/2.16 | (225) all_53_1_43 = all_0_10_10 % 6.38/2.16 | % 6.38/2.16 | From (225) and (217) follows: % 6.38/2.16 | (226) powerset(all_0_10_10) = all_53_0_42 % 6.38/2.16 | % 6.38/2.16 | Instantiating formula (17) with all_0_10_10, all_53_0_42, all_0_9_9 and discharging atoms powerset(all_0_10_10) = all_53_0_42, powerset(all_0_10_10) = all_0_9_9, yields: % 6.38/2.16 | (227) all_53_0_42 = all_0_9_9 % 6.38/2.16 | % 6.38/2.16 | From (227) and (218) follows: % 6.38/2.16 | (220) ~ element(all_0_5_5, all_0_9_9) % 6.38/2.16 | % 6.38/2.16 | Using (14) and (220) yields: % 6.38/2.16 | (137) $false % 6.38/2.16 | % 6.38/2.16 |-The branch is then unsatisfiable % 6.38/2.16 % SZS output end Proof for theBenchmark % 6.38/2.16 % 6.38/2.16 1544ms %------------------------------------------------------------------------------