%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU174+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n007.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:47:19 EDT 2022 % Result : Theorem 22.01s 6.31s % Output : Proof 29.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU174+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n007.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 03:32:58 EDT 2022 % 0.12/0.34 % CPUTime : % 0.49/0.58 ____ _ % 0.49/0.58 ___ / __ \_____(_)___ ________ __________ % 0.49/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.49/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.49/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.49/0.58 % 0.49/0.58 A Theorem Prover for First-Order Logic % 0.49/0.58 (ePrincess v.1.0) % 0.49/0.58 % 0.49/0.58 (c) Philipp Rümmer, 2009-2015 % 0.49/0.58 (c) Peter Backeman, 2014-2015 % 0.49/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.49/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.49/0.58 Bug reports to peter@backeman.se % 0.49/0.58 % 0.49/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.49/0.58 % 0.49/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.49/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.46/0.92 Prover 0: Preprocessing ... % 2.16/1.13 Prover 0: Warning: ignoring some quantifiers % 2.16/1.15 Prover 0: Constructing countermodel ... % 20.27/5.92 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.55/5.96 Prover 1: Preprocessing ... % 20.77/6.03 Prover 1: Warning: ignoring some quantifiers % 20.77/6.03 Prover 1: Constructing countermodel ... % 22.01/6.31 Prover 1: proved (382ms) % 22.01/6.31 Prover 0: stopped % 22.01/6.31 % 22.01/6.31 No countermodel exists, formula is valid % 22.01/6.31 % SZS status Theorem for theBenchmark % 22.01/6.31 % 22.01/6.31 Generating proof ... Warning: ignoring some quantifiers % 28.78/7.87 found it (size 126) % 28.78/7.87 % 28.78/7.87 % SZS output start Proof for theBenchmark % 28.78/7.87 Assumed formulas after preprocessing and simplification: % 28.78/7.87 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v5 = 0) & ~ (v1 = empty_set) & empty(v6) = 0 & empty(v4) = v5 & empty(empty_set) = 0 & powerset(v2) = v3 & powerset(v0) = v2 & complements_of_subsets(v0, v1) = empty_set & element(v1, v3) = 0 & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (powerset(v9) = v10) | ~ (powerset(v7) = v9) | ~ (complements_of_subsets(v7, v8) = v11) | ~ (element(v11, v10) = v12) | ? [v13] : ( ~ (v13 = 0) & element(v8, v10) = v13)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (powerset(v7) = v9) | ~ (subset_complement(v7, v8) = v10) | ~ (element(v10, v9) = v11) | ? [v12] : ( ~ (v12 = 0) & element(v8, v9) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = v8 | ~ (subset_complement(v7, v9) = v10) | ~ (subset_complement(v7, v8) = v9) | ? [v11] : ? [v12] : ( ~ (v12 = 0) & powerset(v7) = v11 & element(v8, v11) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (powerset(v8) = v9) | ~ (element(v7, v9) = v10) | ? [v11] : ( ~ (v11 = 0) & subset(v7, v8) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (complements_of_subsets(v10, v9) = v8) | ~ (complements_of_subsets(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (subset_complement(v10, v9) = v8) | ~ (subset_complement(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (element(v10, v9) = v8) | ~ (element(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (subset(v10, v9) = v8) | ~ (subset(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (in(v10, v9) = v8) | ~ (in(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (powerset(v9) = v10) | ~ (powerset(v7) = v9) | ~ (element(v8, v10) = 0) | ? [v11] : (complements_of_subsets(v7, v11) = v8 & complements_of_subsets(v7, v8) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (powerset(v9) = v10) | ~ (powerset(v7) = v9) | ~ (element(v8, v10) = 0) | ? [v11] : (complements_of_subsets(v7, v8) = v11 & ! [v12] : ! [v13] : ! [v14] : ( ~ (subset_complement(v7, v12) = v13) | ~ (element(v11, v10) = 0) | ~ (in(v13, v8) = v14) | ? [v15] : ? [v16] : (element(v12, v9) = v15 & in(v12, v11) = v16 & ( ~ (v15 = 0) | (( ~ (v16 = 0) | v14 = 0) & ( ~ (v14 = 0) | v16 = 0))))) & ! [v12] : (v12 = v11 | ~ (element(v12, v10) = 0) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : (subset_complement(v7, v13) = v15 & element(v13, v9) = 0 & in(v15, v8) = v16 & in(v13, v12) = v14 & ( ~ (v16 = 0) | ~ (v14 = 0)) & (v16 = 0 | v14 = 0))))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (powerset(v9) = v10) | ~ (element(v8, v10) = 0) | ~ (in(v7, v8) = 0) | element(v7, v9) = 0) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (powerset(v9) = v10) | ~ (element(v8, v10) = 0) | ~ (in(v7, v8) = 0) | ? [v11] : ( ~ (v11 = 0) & empty(v9) = v11)) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (subset(v7, v8) = v9) | ? [v10] : ? [v11] : ( ~ (v11 = 0) & in(v10, v8) = v11 & in(v10, v7) = 0)) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (in(v7, v8) = v9) | ? [v10] : ? [v11] : (empty(v8) = v11 & element(v7, v8) = v10 & ( ~ (v10 = 0) | v11 = 0))) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (empty(v9) = v8) | ~ (empty(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (powerset(v9) = v8) | ~ (powerset(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (powerset(v8) = v9) | ~ (element(v7, v9) = 0) | subset(v7, v8) = 0) & ! [v7] : ! [v8] : ! [v9] : ( ~ (subset(v7, v8) = 0) | ~ (in(v9, v7) = 0) | in(v9, v8) = 0) & ! [v7] : ! [v8] : (v8 = v7 | ~ (empty(v8) = 0) | ~ (empty(v7) = 0)) & ! [v7] : ! [v8] : (v8 = 0 | ~ (empty(v7) = v8) | ? [v9] : ? [v10] : ? [v11] : ( ~ (v11 = 0) & empty(v10) = v11 & powerset(v7) = v9 & element(v10, v9) = 0)) & ! [v7] : ! [v8] : (v8 = 0 | ~ (subset(v7, v7) = v8)) & ! [v7] : ! [v8] : ( ~ (powerset(v7) = v8) | ? [v9] : ( ~ (v9 = 0) & empty(v8) = v9)) & ! [v7] : ! [v8] : ( ~ (powerset(v7) = v8) | ? [v9] : (empty(v9) = 0 & element(v9, v8) = 0)) & ! [v7] : ! [v8] : ( ~ (in(v7, v8) = 0) | element(v7, v8) = 0) & ! [v7] : ! [v8] : ( ~ (in(v7, v8) = 0) | ? [v9] : ( ~ (v9 = 0) & empty(v8) = v9)) & ! [v7] : ! [v8] : ( ~ (in(v7, v8) = 0) | ? [v9] : ( ~ (v9 = 0) & in(v8, v7) = v9)) & ! [v7] : (v7 = empty_set | ~ (empty(v7) = 0)) & ? [v7] : ? [v8] : element(v8, v7) = 0) % 28.78/7.91 | 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 yields: % 28.78/7.91 | (1) ~ (all_0_1_1 = 0) & ~ (all_0_5_5 = empty_set) & empty(all_0_0_0) = 0 & empty(all_0_2_2) = all_0_1_1 & empty(empty_set) = 0 & powerset(all_0_4_4) = all_0_3_3 & powerset(all_0_6_6) = all_0_4_4 & complements_of_subsets(all_0_6_6, all_0_5_5) = empty_set & element(all_0_5_5, all_0_3_3) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (complements_of_subsets(v0, v1) = v4) | ~ (element(v4, v3) = v5) | ? [v6] : ( ~ (v6 = 0) & element(v1, v3) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v0) = v2) | ~ (subset_complement(v0, v1) = v3) | ~ (element(v3, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & element(v1, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (subset_complement(v0, v2) = v3) | ~ (subset_complement(v0, v1) = v2) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v0) = v4 & element(v1, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (complements_of_subsets(v3, v2) = v1) | ~ (complements_of_subsets(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (element(v1, v3) = 0) | ? [v4] : (complements_of_subsets(v0, v4) = v1 & complements_of_subsets(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (element(v1, v3) = 0) | ? [v4] : (complements_of_subsets(v0, v1) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (subset_complement(v0, v5) = v6) | ~ (element(v4, v3) = 0) | ~ (in(v6, v1) = v7) | ? [v8] : ? [v9] : (element(v5, v2) = v8 & in(v5, v4) = v9 & ( ~ (v8 = 0) | (( ~ (v9 = 0) | v7 = 0) & ( ~ (v7 = 0) | v9 = 0))))) & ! [v5] : (v5 = v4 | ~ (element(v5, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (subset_complement(v0, v6) = v8 & element(v6, v2) = 0 & in(v8, v1) = v9 & in(v6, v5) = v7 & ( ~ (v9 = 0) | ~ (v7 = 0)) & (v9 = 0 | v7 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (empty(v1) = v4 & element(v0, v1) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v0, v1) = 0) | ~ (in(v2, v0) = 0) | in(v2, v1) = 0) & ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & empty(v3) = v4 & powerset(v0) = v2 & element(v3, v2) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (empty(v2) = 0 & element(v2, v1) = 0)) & ! [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] : ? [v1] : element(v1, v0) = 0 % 28.78/7.92 | % 28.78/7.92 | Applying alpha-rule on (1) yields: % 28.78/7.92 | (2) empty(all_0_0_0) = 0 % 28.78/7.92 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (complements_of_subsets(v3, v2) = v1) | ~ (complements_of_subsets(v3, v2) = v0)) % 28.78/7.92 | (4) complements_of_subsets(all_0_6_6, all_0_5_5) = empty_set % 28.78/7.92 | (5) empty(empty_set) = 0 % 28.78/7.92 | (6) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & empty(v3) = v4 & powerset(v0) = v2 & element(v3, v2) = 0)) % 28.78/7.92 | (7) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 28.78/7.92 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) % 28.78/7.92 | (9) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0)) % 28.78/7.92 | (10) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 28.78/7.92 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 28.78/7.92 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) % 28.78/7.92 | (13) element(all_0_5_5, all_0_3_3) = 0 % 28.78/7.92 | (14) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (empty(v1) = v4 & element(v0, v1) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 28.78/7.92 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) % 28.78/7.92 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (complements_of_subsets(v0, v1) = v4) | ~ (element(v4, v3) = v5) | ? [v6] : ( ~ (v6 = 0) & element(v1, v3) = v6)) % 28.78/7.92 | (17) powerset(all_0_6_6) = all_0_4_4 % 28.78/7.92 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v0) = v2) | ~ (subset_complement(v0, v1) = v3) | ~ (element(v3, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & element(v1, v2) = v5)) % 28.78/7.92 | (19) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 28.78/7.92 | (20) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) % 28.78/7.92 | (21) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 28.78/7.92 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) % 28.78/7.93 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 28.78/7.93 | (24) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (empty(v2) = 0 & element(v2, v1) = 0)) % 28.78/7.93 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v0, v1) = 0) | ~ (in(v2, v0) = 0) | in(v2, v1) = 0) % 28.78/7.93 | (26) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 28.78/7.93 | (27) empty(all_0_2_2) = all_0_1_1 % 28.78/7.93 | (28) ~ (all_0_1_1 = 0) % 28.78/7.93 | (29) powerset(all_0_4_4) = all_0_3_3 % 28.78/7.93 | (30) ? [v0] : ? [v1] : element(v1, v0) = 0 % 28.78/7.93 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 28.78/7.93 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (subset_complement(v0, v2) = v3) | ~ (subset_complement(v0, v1) = v2) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v0) = v4 & element(v1, v4) = v5)) % 28.78/7.93 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) % 28.78/7.93 | (34) ~ (all_0_5_5 = empty_set) % 28.78/7.93 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 28.78/7.93 | (36) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 28.78/7.93 | (37) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 28.78/7.93 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (element(v1, v3) = 0) | ? [v4] : (complements_of_subsets(v0, v1) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (subset_complement(v0, v5) = v6) | ~ (element(v4, v3) = 0) | ~ (in(v6, v1) = v7) | ? [v8] : ? [v9] : (element(v5, v2) = v8 & in(v5, v4) = v9 & ( ~ (v8 = 0) | (( ~ (v9 = 0) | v7 = 0) & ( ~ (v7 = 0) | v9 = 0))))) & ! [v5] : (v5 = v4 | ~ (element(v5, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (subset_complement(v0, v6) = v8 & element(v6, v2) = 0 & in(v8, v1) = v9 & in(v6, v5) = v7 & ( ~ (v9 = 0) | ~ (v7 = 0)) & (v9 = 0 | v7 = 0))))) % 28.78/7.93 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (powerset(v0) = v2) | ~ (element(v1, v3) = 0) | ? [v4] : (complements_of_subsets(v0, v4) = v1 & complements_of_subsets(v0, v1) = v4)) % 28.78/7.93 | % 28.78/7.93 | Instantiating formula (6) with all_0_1_1, all_0_2_2 and discharging atoms empty(all_0_2_2) = all_0_1_1, yields: % 28.78/7.93 | (40) all_0_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2 & powerset(all_0_2_2) = v0 & element(v1, v0) = 0) % 28.78/7.93 | % 28.78/7.93 | Instantiating formula (24) with all_0_3_3, all_0_4_4 and discharging atoms powerset(all_0_4_4) = all_0_3_3, yields: % 29.20/7.93 | (41) ? [v0] : (empty(v0) = 0 & element(v0, all_0_3_3) = 0) % 29.20/7.93 | % 29.20/7.93 | Instantiating formula (24) with all_0_4_4, all_0_6_6 and discharging atoms powerset(all_0_6_6) = all_0_4_4, yields: % 29.20/7.93 | (42) ? [v0] : (empty(v0) = 0 & element(v0, all_0_4_4) = 0) % 29.20/7.93 | % 29.20/7.93 | Instantiating formula (39) with all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms powerset(all_0_4_4) = all_0_3_3, powerset(all_0_6_6) = all_0_4_4, element(all_0_5_5, all_0_3_3) = 0, yields: % 29.20/7.94 | (43) ? [v0] : (complements_of_subsets(all_0_6_6, v0) = all_0_5_5 & complements_of_subsets(all_0_6_6, all_0_5_5) = v0) % 29.20/7.94 | % 29.20/7.94 | Instantiating formula (38) with all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms powerset(all_0_4_4) = all_0_3_3, powerset(all_0_6_6) = all_0_4_4, element(all_0_5_5, all_0_3_3) = 0, yields: % 29.20/7.94 | (44) ? [v0] : (complements_of_subsets(all_0_6_6, all_0_5_5) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (subset_complement(all_0_6_6, v1) = v2) | ~ (element(v0, all_0_3_3) = 0) | ~ (in(v2, all_0_5_5) = v3) | ? [v4] : ? [v5] : (element(v1, all_0_4_4) = v4 & in(v1, v0) = v5 & ( ~ (v4 = 0) | (( ~ (v5 = 0) | v3 = 0) & ( ~ (v3 = 0) | v5 = 0))))) & ! [v1] : (v1 = v0 | ~ (element(v1, all_0_3_3) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (subset_complement(all_0_6_6, v2) = v4 & element(v2, all_0_4_4) = 0 & in(v4, all_0_5_5) = v5 & in(v2, v1) = v3 & ( ~ (v5 = 0) | ~ (v3 = 0)) & (v5 = 0 | v3 = 0)))) % 29.20/7.94 | % 29.20/7.94 | Instantiating (44) with all_15_0_9 yields: % 29.20/7.94 | (45) complements_of_subsets(all_0_6_6, all_0_5_5) = all_15_0_9 & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_6_6, v0) = v1) | ~ (element(all_15_0_9, all_0_3_3) = 0) | ~ (in(v1, all_0_5_5) = v2) | ? [v3] : ? [v4] : (element(v0, all_0_4_4) = v3 & in(v0, all_15_0_9) = v4 & ( ~ (v3 = 0) | (( ~ (v4 = 0) | v2 = 0) & ( ~ (v2 = 0) | v4 = 0))))) & ! [v0] : (v0 = all_15_0_9 | ~ (element(v0, all_0_3_3) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset_complement(all_0_6_6, v1) = v3 & element(v1, all_0_4_4) = 0 & in(v3, all_0_5_5) = v4 & in(v1, v0) = v2 & ( ~ (v4 = 0) | ~ (v2 = 0)) & (v4 = 0 | v2 = 0))) % 29.20/7.94 | % 29.20/7.94 | Applying alpha-rule on (45) yields: % 29.20/7.94 | (46) complements_of_subsets(all_0_6_6, all_0_5_5) = all_15_0_9 % 29.20/7.94 | (47) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_6_6, v0) = v1) | ~ (element(all_15_0_9, all_0_3_3) = 0) | ~ (in(v1, all_0_5_5) = v2) | ? [v3] : ? [v4] : (element(v0, all_0_4_4) = v3 & in(v0, all_15_0_9) = v4 & ( ~ (v3 = 0) | (( ~ (v4 = 0) | v2 = 0) & ( ~ (v2 = 0) | v4 = 0))))) % 29.20/7.94 | (48) ! [v0] : (v0 = all_15_0_9 | ~ (element(v0, all_0_3_3) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset_complement(all_0_6_6, v1) = v3 & element(v1, all_0_4_4) = 0 & in(v3, all_0_5_5) = v4 & in(v1, v0) = v2 & ( ~ (v4 = 0) | ~ (v2 = 0)) & (v4 = 0 | v2 = 0))) % 29.20/7.94 | % 29.20/7.94 | Instantiating formula (48) with all_0_5_5 and discharging atoms element(all_0_5_5, all_0_3_3) = 0, yields: % 29.20/7.94 | (49) all_15_0_9 = all_0_5_5 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (subset_complement(all_0_6_6, v0) = v2 & element(v0, all_0_4_4) = 0 & in(v2, all_0_5_5) = v3 & in(v0, all_0_5_5) = v1 & ( ~ (v3 = 0) | ~ (v1 = 0)) & (v3 = 0 | v1 = 0)) % 29.20/7.94 | % 29.20/7.94 | Instantiating (43) with all_18_0_10 yields: % 29.20/7.94 | (50) complements_of_subsets(all_0_6_6, all_18_0_10) = all_0_5_5 & complements_of_subsets(all_0_6_6, all_0_5_5) = all_18_0_10 % 29.20/7.94 | % 29.20/7.94 | Applying alpha-rule on (50) yields: % 29.20/7.94 | (51) complements_of_subsets(all_0_6_6, all_18_0_10) = all_0_5_5 % 29.20/7.94 | (52) complements_of_subsets(all_0_6_6, all_0_5_5) = all_18_0_10 % 29.20/7.94 | % 29.20/7.94 | Instantiating (42) with all_24_0_13 yields: % 29.20/7.94 | (53) empty(all_24_0_13) = 0 & element(all_24_0_13, all_0_4_4) = 0 % 29.20/7.94 | % 29.20/7.94 | Applying alpha-rule on (53) yields: % 29.20/7.94 | (54) empty(all_24_0_13) = 0 % 29.20/7.94 | (55) element(all_24_0_13, all_0_4_4) = 0 % 29.20/7.94 | % 29.20/7.94 | Instantiating (41) with all_26_0_14 yields: % 29.20/7.94 | (56) empty(all_26_0_14) = 0 & element(all_26_0_14, all_0_3_3) = 0 % 29.20/7.94 | % 29.20/7.94 | Applying alpha-rule on (56) yields: % 29.20/7.94 | (57) empty(all_26_0_14) = 0 % 29.20/7.94 | (58) element(all_26_0_14, all_0_3_3) = 0 % 29.20/7.94 | % 29.20/7.94 +-Applying beta-rule and splitting (40), into two cases. % 29.20/7.94 |-Branch one: % 29.20/7.94 | (59) all_0_1_1 = 0 % 29.20/7.94 | % 29.20/7.94 | Equations (59) can reduce 28 to: % 29.20/7.94 | (60) $false % 29.20/7.95 | % 29.20/7.95 |-The branch is then unsatisfiable % 29.20/7.95 |-Branch two: % 29.20/7.95 | (28) ~ (all_0_1_1 = 0) % 29.20/7.95 | (62) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2 & powerset(all_0_2_2) = v0 & element(v1, v0) = 0) % 29.20/7.95 | % 29.20/7.95 | Instantiating (62) with all_32_0_15, all_32_1_16, all_32_2_17 yields: % 29.20/7.95 | (63) ~ (all_32_0_15 = 0) & empty(all_32_1_16) = all_32_0_15 & powerset(all_0_2_2) = all_32_2_17 & element(all_32_1_16, all_32_2_17) = 0 % 29.20/7.95 | % 29.20/7.95 | Applying alpha-rule on (63) yields: % 29.20/7.95 | (64) ~ (all_32_0_15 = 0) % 29.20/7.95 | (65) empty(all_32_1_16) = all_32_0_15 % 29.20/7.95 | (66) powerset(all_0_2_2) = all_32_2_17 % 29.20/7.95 | (67) element(all_32_1_16, all_32_2_17) = 0 % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (19) with all_26_0_14 and discharging atoms empty(all_26_0_14) = 0, yields: % 29.20/7.95 | (68) all_26_0_14 = empty_set % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (7) with all_24_0_13, all_26_0_14 and discharging atoms empty(all_26_0_14) = 0, empty(all_24_0_13) = 0, yields: % 29.20/7.95 | (69) all_26_0_14 = all_24_0_13 % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (3) with all_0_6_6, all_0_5_5, all_18_0_10, empty_set and discharging atoms complements_of_subsets(all_0_6_6, all_0_5_5) = all_18_0_10, complements_of_subsets(all_0_6_6, all_0_5_5) = empty_set, yields: % 29.20/7.95 | (70) all_18_0_10 = empty_set % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (3) with all_0_6_6, all_0_5_5, all_15_0_9, all_18_0_10 and discharging atoms complements_of_subsets(all_0_6_6, all_0_5_5) = all_18_0_10, complements_of_subsets(all_0_6_6, all_0_5_5) = all_15_0_9, yields: % 29.20/7.95 | (71) all_18_0_10 = all_15_0_9 % 29.20/7.95 | % 29.20/7.95 | Combining equations (68,69) yields a new equation: % 29.20/7.95 | (72) all_24_0_13 = empty_set % 29.20/7.95 | % 29.20/7.95 | Combining equations (71,70) yields a new equation: % 29.20/7.95 | (73) all_15_0_9 = empty_set % 29.20/7.95 | % 29.20/7.95 | Simplifying 73 yields: % 29.20/7.95 | (74) all_15_0_9 = empty_set % 29.20/7.95 | % 29.20/7.95 | Combining equations (72,69) yields a new equation: % 29.20/7.95 | (68) all_26_0_14 = empty_set % 29.20/7.95 | % 29.20/7.95 | From (70) and (51) follows: % 29.20/7.95 | (76) complements_of_subsets(all_0_6_6, empty_set) = all_0_5_5 % 29.20/7.95 | % 29.20/7.95 | From (68) and (58) follows: % 29.20/7.95 | (77) element(empty_set, all_0_3_3) = 0 % 29.20/7.95 | % 29.20/7.95 +-Applying beta-rule and splitting (49), into two cases. % 29.20/7.95 |-Branch one: % 29.20/7.95 | (78) all_15_0_9 = all_0_5_5 % 29.20/7.95 | % 29.20/7.95 | Combining equations (78,74) yields a new equation: % 29.20/7.95 | (79) all_0_5_5 = empty_set % 29.20/7.95 | % 29.20/7.95 | Simplifying 79 yields: % 29.20/7.95 | (80) all_0_5_5 = empty_set % 29.20/7.95 | % 29.20/7.95 | Equations (80) can reduce 34 to: % 29.20/7.95 | (60) $false % 29.20/7.95 | % 29.20/7.95 |-The branch is then unsatisfiable % 29.20/7.95 |-Branch two: % 29.20/7.95 | (82) ~ (all_15_0_9 = all_0_5_5) % 29.20/7.95 | (83) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (subset_complement(all_0_6_6, v0) = v2 & element(v0, all_0_4_4) = 0 & in(v2, all_0_5_5) = v3 & in(v0, all_0_5_5) = v1 & ( ~ (v3 = 0) | ~ (v1 = 0)) & (v3 = 0 | v1 = 0)) % 29.20/7.95 | % 29.20/7.95 | Equations (74) can reduce 82 to: % 29.20/7.95 | (84) ~ (all_0_5_5 = empty_set) % 29.20/7.95 | % 29.20/7.95 | Simplifying 84 yields: % 29.20/7.95 | (34) ~ (all_0_5_5 = empty_set) % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (24) with all_32_2_17, all_0_2_2 and discharging atoms powerset(all_0_2_2) = all_32_2_17, yields: % 29.20/7.95 | (86) ? [v0] : (empty(v0) = 0 & element(v0, all_32_2_17) = 0) % 29.20/7.95 | % 29.20/7.95 | Instantiating formula (38) with all_0_3_3, all_0_4_4, empty_set, all_0_6_6 and discharging atoms powerset(all_0_4_4) = all_0_3_3, powerset(all_0_6_6) = all_0_4_4, element(empty_set, all_0_3_3) = 0, yields: % 29.20/7.95 | (87) ? [v0] : (complements_of_subsets(all_0_6_6, empty_set) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (subset_complement(all_0_6_6, v1) = v2) | ~ (element(v0, all_0_3_3) = 0) | ~ (in(v2, empty_set) = v3) | ? [v4] : ? [v5] : (element(v1, all_0_4_4) = v4 & in(v1, v0) = v5 & ( ~ (v4 = 0) | (( ~ (v5 = 0) | v3 = 0) & ( ~ (v3 = 0) | v5 = 0))))) & ! [v1] : (v1 = v0 | ~ (element(v1, all_0_3_3) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (subset_complement(all_0_6_6, v2) = v4 & element(v2, all_0_4_4) = 0 & in(v4, empty_set) = v5 & in(v2, v1) = v3 & ( ~ (v5 = 0) | ~ (v3 = 0)) & (v5 = 0 | v3 = 0)))) % 29.20/7.95 | % 29.20/7.95 | Instantiating (87) with all_50_0_22 yields: % 29.20/7.95 | (88) complements_of_subsets(all_0_6_6, empty_set) = all_50_0_22 & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_6_6, v0) = v1) | ~ (element(all_50_0_22, all_0_3_3) = 0) | ~ (in(v1, empty_set) = v2) | ? [v3] : ? [v4] : (element(v0, all_0_4_4) = v3 & in(v0, all_50_0_22) = v4 & ( ~ (v3 = 0) | (( ~ (v4 = 0) | v2 = 0) & ( ~ (v2 = 0) | v4 = 0))))) & ! [v0] : (v0 = all_50_0_22 | ~ (element(v0, all_0_3_3) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset_complement(all_0_6_6, v1) = v3 & element(v1, all_0_4_4) = 0 & in(v3, empty_set) = v4 & in(v1, v0) = v2 & ( ~ (v4 = 0) | ~ (v2 = 0)) & (v4 = 0 | v2 = 0))) % 29.20/7.96 | % 29.20/7.96 | Applying alpha-rule on (88) yields: % 29.20/7.96 | (89) complements_of_subsets(all_0_6_6, empty_set) = all_50_0_22 % 29.20/7.96 | (90) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(all_0_6_6, v0) = v1) | ~ (element(all_50_0_22, all_0_3_3) = 0) | ~ (in(v1, empty_set) = v2) | ? [v3] : ? [v4] : (element(v0, all_0_4_4) = v3 & in(v0, all_50_0_22) = v4 & ( ~ (v3 = 0) | (( ~ (v4 = 0) | v2 = 0) & ( ~ (v2 = 0) | v4 = 0))))) % 29.20/7.96 | (91) ! [v0] : (v0 = all_50_0_22 | ~ (element(v0, all_0_3_3) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset_complement(all_0_6_6, v1) = v3 & element(v1, all_0_4_4) = 0 & in(v3, empty_set) = v4 & in(v1, v0) = v2 & ( ~ (v4 = 0) | ~ (v2 = 0)) & (v4 = 0 | v2 = 0))) % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (91) with empty_set and discharging atoms element(empty_set, all_0_3_3) = 0, yields: % 29.20/7.96 | (92) all_50_0_22 = empty_set | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (subset_complement(all_0_6_6, v0) = v2 & element(v0, all_0_4_4) = 0 & in(v2, empty_set) = v3 & in(v0, empty_set) = v1 & ( ~ (v3 = 0) | ~ (v1 = 0)) & (v3 = 0 | v1 = 0)) % 29.20/7.96 | % 29.20/7.96 | Instantiating (86) with all_53_0_23 yields: % 29.20/7.96 | (93) empty(all_53_0_23) = 0 & element(all_53_0_23, all_32_2_17) = 0 % 29.20/7.96 | % 29.20/7.96 | Applying alpha-rule on (93) yields: % 29.20/7.96 | (94) empty(all_53_0_23) = 0 % 29.20/7.96 | (95) element(all_53_0_23, all_32_2_17) = 0 % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (19) with all_53_0_23 and discharging atoms empty(all_53_0_23) = 0, yields: % 29.20/7.96 | (96) all_53_0_23 = empty_set % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (3) with all_0_6_6, empty_set, all_50_0_22, all_0_5_5 and discharging atoms complements_of_subsets(all_0_6_6, empty_set) = all_50_0_22, complements_of_subsets(all_0_6_6, empty_set) = all_0_5_5, yields: % 29.20/7.96 | (97) all_50_0_22 = all_0_5_5 % 29.20/7.96 | % 29.20/7.96 | From (96) and (94) follows: % 29.20/7.96 | (5) empty(empty_set) = 0 % 29.20/7.96 | % 29.20/7.96 +-Applying beta-rule and splitting (92), into two cases. % 29.20/7.96 |-Branch one: % 29.20/7.96 | (99) all_50_0_22 = empty_set % 29.20/7.96 | % 29.20/7.96 | Combining equations (97,99) yields a new equation: % 29.20/7.96 | (79) all_0_5_5 = empty_set % 29.20/7.96 | % 29.20/7.96 | Simplifying 79 yields: % 29.20/7.96 | (80) all_0_5_5 = empty_set % 29.20/7.96 | % 29.20/7.96 | Equations (80) can reduce 34 to: % 29.20/7.96 | (60) $false % 29.20/7.96 | % 29.20/7.96 |-The branch is then unsatisfiable % 29.20/7.96 |-Branch two: % 29.20/7.96 | (103) ~ (all_50_0_22 = empty_set) % 29.20/7.96 | (104) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (subset_complement(all_0_6_6, v0) = v2 & element(v0, all_0_4_4) = 0 & in(v2, empty_set) = v3 & in(v0, empty_set) = v1 & ( ~ (v3 = 0) | ~ (v1 = 0)) & (v3 = 0 | v1 = 0)) % 29.20/7.96 | % 29.20/7.96 | Instantiating (104) with all_86_0_36, all_86_1_37, all_86_2_38, all_86_3_39 yields: % 29.20/7.96 | (105) subset_complement(all_0_6_6, all_86_3_39) = all_86_1_37 & element(all_86_3_39, all_0_4_4) = 0 & in(all_86_1_37, empty_set) = all_86_0_36 & in(all_86_3_39, empty_set) = all_86_2_38 & ( ~ (all_86_0_36 = 0) | ~ (all_86_2_38 = 0)) & (all_86_0_36 = 0 | all_86_2_38 = 0) % 29.20/7.96 | % 29.20/7.96 | Applying alpha-rule on (105) yields: % 29.20/7.96 | (106) in(all_86_1_37, empty_set) = all_86_0_36 % 29.20/7.96 | (107) all_86_0_36 = 0 | all_86_2_38 = 0 % 29.20/7.96 | (108) ~ (all_86_0_36 = 0) | ~ (all_86_2_38 = 0) % 29.20/7.96 | (109) in(all_86_3_39, empty_set) = all_86_2_38 % 29.20/7.96 | (110) element(all_86_3_39, all_0_4_4) = 0 % 29.20/7.96 | (111) subset_complement(all_0_6_6, all_86_3_39) = all_86_1_37 % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (20) with empty_set, all_86_1_37 yields: % 29.20/7.96 | (112) ~ (in(all_86_1_37, empty_set) = 0) | element(all_86_1_37, empty_set) = 0 % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (36) with empty_set, all_86_1_37 yields: % 29.20/7.96 | (113) ~ (in(all_86_1_37, empty_set) = 0) | ? [v0] : ( ~ (v0 = 0) & empty(empty_set) = v0) % 29.20/7.96 | % 29.20/7.96 | Instantiating formula (37) with empty_set, all_86_1_37 yields: % 29.20/7.97 | (114) ~ (in(all_86_1_37, empty_set) = 0) | ? [v0] : ( ~ (v0 = 0) & in(empty_set, all_86_1_37) = v0) % 29.20/7.97 | % 29.20/7.97 | Instantiating formula (14) with all_86_0_36, empty_set, all_86_1_37 and discharging atoms in(all_86_1_37, empty_set) = all_86_0_36, yields: % 29.20/7.97 | (115) all_86_0_36 = 0 | ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_1_37, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.97 | % 29.20/7.97 | Instantiating formula (36) with empty_set, all_86_3_39 yields: % 29.20/7.97 | (116) ~ (in(all_86_3_39, empty_set) = 0) | ? [v0] : ( ~ (v0 = 0) & empty(empty_set) = v0) % 29.20/7.97 | % 29.20/7.97 | Instantiating formula (14) with all_86_2_38, empty_set, all_86_3_39 and discharging atoms in(all_86_3_39, empty_set) = all_86_2_38, yields: % 29.20/7.97 | (117) all_86_2_38 = 0 | ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_3_39, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (113), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (118) ~ (in(all_86_1_37, empty_set) = 0) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (116), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (119) ~ (in(all_86_3_39, empty_set) = 0) % 29.20/7.97 | % 29.20/7.97 | Using (106) and (118) yields: % 29.20/7.97 | (120) ~ (all_86_0_36 = 0) % 29.20/7.97 | % 29.20/7.97 | Using (109) and (119) yields: % 29.20/7.97 | (121) ~ (all_86_2_38 = 0) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (117), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (122) all_86_2_38 = 0 % 29.20/7.97 | % 29.20/7.97 | Equations (122) can reduce 121 to: % 29.20/7.97 | (60) $false % 29.20/7.97 | % 29.20/7.97 |-The branch is then unsatisfiable % 29.20/7.97 |-Branch two: % 29.20/7.97 | (121) ~ (all_86_2_38 = 0) % 29.20/7.97 | (125) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_3_39, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (115), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (126) all_86_0_36 = 0 % 29.20/7.97 | % 29.20/7.97 | Equations (126) can reduce 120 to: % 29.20/7.97 | (60) $false % 29.20/7.97 | % 29.20/7.97 |-The branch is then unsatisfiable % 29.20/7.97 |-Branch two: % 29.20/7.97 | (120) ~ (all_86_0_36 = 0) % 29.20/7.97 | (129) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_1_37, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (107), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (126) all_86_0_36 = 0 % 29.20/7.97 | % 29.20/7.97 | Equations (126) can reduce 120 to: % 29.20/7.97 | (60) $false % 29.20/7.97 | % 29.20/7.97 |-The branch is then unsatisfiable % 29.20/7.97 |-Branch two: % 29.20/7.97 | (120) ~ (all_86_0_36 = 0) % 29.20/7.97 | (122) all_86_2_38 = 0 % 29.20/7.97 | % 29.20/7.97 | Equations (122) can reduce 121 to: % 29.20/7.97 | (60) $false % 29.20/7.97 | % 29.20/7.97 |-The branch is then unsatisfiable % 29.20/7.97 |-Branch two: % 29.20/7.97 | (135) in(all_86_3_39, empty_set) = 0 % 29.20/7.97 | (136) ? [v0] : ( ~ (v0 = 0) & empty(empty_set) = v0) % 29.20/7.97 | % 29.20/7.97 | Instantiating (136) with all_154_0_74 yields: % 29.20/7.97 | (137) ~ (all_154_0_74 = 0) & empty(empty_set) = all_154_0_74 % 29.20/7.97 | % 29.20/7.97 | Applying alpha-rule on (137) yields: % 29.20/7.97 | (138) ~ (all_154_0_74 = 0) % 29.20/7.97 | (139) empty(empty_set) = all_154_0_74 % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (117), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (122) all_86_2_38 = 0 % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (108), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (120) ~ (all_86_0_36 = 0) % 29.20/7.97 | % 29.20/7.97 +-Applying beta-rule and splitting (115), into two cases. % 29.20/7.97 |-Branch one: % 29.20/7.97 | (126) all_86_0_36 = 0 % 29.20/7.97 | % 29.20/7.97 | Equations (126) can reduce 120 to: % 29.20/7.97 | (60) $false % 29.20/7.97 | % 29.20/7.97 |-The branch is then unsatisfiable % 29.20/7.97 |-Branch two: % 29.20/7.97 | (120) ~ (all_86_0_36 = 0) % 29.20/7.97 | (129) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_1_37, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.97 | % 29.20/7.98 | Instantiating (129) with all_209_0_76, all_209_1_77 yields: % 29.20/7.98 | (146) empty(empty_set) = all_209_0_76 & element(all_86_1_37, empty_set) = all_209_1_77 & ( ~ (all_209_1_77 = 0) | all_209_0_76 = 0) % 29.20/7.98 | % 29.20/7.98 | Applying alpha-rule on (146) yields: % 29.20/7.98 | (147) empty(empty_set) = all_209_0_76 % 29.20/7.98 | (148) element(all_86_1_37, empty_set) = all_209_1_77 % 29.20/7.98 | (149) ~ (all_209_1_77 = 0) | all_209_0_76 = 0 % 29.20/7.98 | % 29.20/7.98 | Instantiating formula (21) with empty_set, all_209_0_76, 0 and discharging atoms empty(empty_set) = all_209_0_76, empty(empty_set) = 0, yields: % 29.20/7.98 | (150) all_209_0_76 = 0 % 29.20/7.98 | % 29.20/7.98 | Instantiating formula (21) with empty_set, all_154_0_74, all_209_0_76 and discharging atoms empty(empty_set) = all_209_0_76, empty(empty_set) = all_154_0_74, yields: % 29.20/7.98 | (151) all_209_0_76 = all_154_0_74 % 29.20/7.98 | % 29.20/7.98 | Combining equations (150,151) yields a new equation: % 29.20/7.98 | (152) all_154_0_74 = 0 % 29.20/7.98 | % 29.20/7.98 | Equations (152) can reduce 138 to: % 29.20/7.98 | (60) $false % 29.20/7.98 | % 29.20/7.98 |-The branch is then unsatisfiable % 29.20/7.98 |-Branch two: % 29.20/7.98 | (126) all_86_0_36 = 0 % 29.20/7.98 | (121) ~ (all_86_2_38 = 0) % 29.20/7.98 | % 29.20/7.98 | Equations (122) can reduce 121 to: % 29.20/7.98 | (60) $false % 29.20/7.98 | % 29.20/7.98 |-The branch is then unsatisfiable % 29.20/7.98 |-Branch two: % 29.20/7.98 | (121) ~ (all_86_2_38 = 0) % 29.20/7.98 | (125) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_3_39, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.20/7.98 | % 29.20/7.98 +-Applying beta-rule and splitting (107), into two cases. % 29.20/7.98 |-Branch one: % 29.20/7.98 | (126) all_86_0_36 = 0 % 29.20/7.98 | % 29.20/7.98 | From (126) and (106) follows: % 29.20/7.98 | (160) in(all_86_1_37, empty_set) = 0 % 29.20/7.98 | % 29.20/7.98 | Using (160) and (118) yields: % 29.20/7.98 | (161) $false % 29.20/7.98 | % 29.20/7.98 |-The branch is then unsatisfiable % 29.20/7.98 |-Branch two: % 29.20/7.98 | (120) ~ (all_86_0_36 = 0) % 29.20/7.98 | (122) all_86_2_38 = 0 % 29.20/7.98 | % 29.20/7.98 | Equations (122) can reduce 121 to: % 29.20/7.98 | (60) $false % 29.20/7.98 | % 29.20/7.98 |-The branch is then unsatisfiable % 29.20/7.98 |-Branch two: % 29.20/7.98 | (160) in(all_86_1_37, empty_set) = 0 % 29.20/7.98 | (136) ? [v0] : ( ~ (v0 = 0) & empty(empty_set) = v0) % 29.20/7.98 | % 29.20/7.98 | Instantiating (136) with all_116_0_80 yields: % 29.20/7.98 | (167) ~ (all_116_0_80 = 0) & empty(empty_set) = all_116_0_80 % 29.20/7.98 | % 29.20/7.98 | Applying alpha-rule on (167) yields: % 29.20/7.98 | (168) ~ (all_116_0_80 = 0) % 29.20/7.98 | (169) empty(empty_set) = all_116_0_80 % 29.20/7.98 | % 29.20/7.98 +-Applying beta-rule and splitting (112), into two cases. % 29.20/7.98 |-Branch one: % 29.20/7.98 | (118) ~ (in(all_86_1_37, empty_set) = 0) % 29.20/7.98 | % 29.44/7.98 | Using (160) and (118) yields: % 29.44/7.98 | (161) $false % 29.44/7.98 | % 29.44/7.98 |-The branch is then unsatisfiable % 29.44/7.98 |-Branch two: % 29.44/7.98 | (160) in(all_86_1_37, empty_set) = 0 % 29.44/7.98 | (173) element(all_86_1_37, empty_set) = 0 % 29.44/7.98 | % 29.44/7.98 +-Applying beta-rule and splitting (115), into two cases. % 29.44/7.98 |-Branch one: % 29.44/7.98 | (126) all_86_0_36 = 0 % 29.44/7.98 | % 29.44/7.98 +-Applying beta-rule and splitting (108), into two cases. % 29.44/7.98 |-Branch one: % 29.44/7.98 | (120) ~ (all_86_0_36 = 0) % 29.44/7.98 | % 29.44/7.98 | Equations (126) can reduce 120 to: % 29.44/7.98 | (60) $false % 29.44/7.98 | % 29.44/7.98 |-The branch is then unsatisfiable % 29.44/7.98 |-Branch two: % 29.44/7.98 | (126) all_86_0_36 = 0 % 29.44/7.98 | (121) ~ (all_86_2_38 = 0) % 29.44/7.98 | % 29.44/7.98 +-Applying beta-rule and splitting (117), into two cases. % 29.44/7.98 |-Branch one: % 29.44/7.98 | (122) all_86_2_38 = 0 % 29.44/7.98 | % 29.44/7.98 | Equations (122) can reduce 121 to: % 29.44/7.98 | (60) $false % 29.44/7.98 | % 29.44/7.98 |-The branch is then unsatisfiable % 29.44/7.98 |-Branch two: % 29.44/7.98 | (121) ~ (all_86_2_38 = 0) % 29.44/7.98 | (125) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_3_39, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.44/7.98 | % 29.44/7.98 | Instantiating (125) with all_201_0_100, all_201_1_101 yields: % 29.44/7.98 | (183) empty(empty_set) = all_201_0_100 & element(all_86_3_39, empty_set) = all_201_1_101 & ( ~ (all_201_1_101 = 0) | all_201_0_100 = 0) % 29.44/7.98 | % 29.44/7.98 | Applying alpha-rule on (183) yields: % 29.44/7.98 | (184) empty(empty_set) = all_201_0_100 % 29.44/7.99 | (185) element(all_86_3_39, empty_set) = all_201_1_101 % 29.44/7.99 | (186) ~ (all_201_1_101 = 0) | all_201_0_100 = 0 % 29.44/7.99 | % 29.44/7.99 | Instantiating formula (21) with empty_set, all_201_0_100, 0 and discharging atoms empty(empty_set) = all_201_0_100, empty(empty_set) = 0, yields: % 29.44/7.99 | (187) all_201_0_100 = 0 % 29.44/7.99 | % 29.44/7.99 | Instantiating formula (21) with empty_set, all_116_0_80, all_201_0_100 and discharging atoms empty(empty_set) = all_201_0_100, empty(empty_set) = all_116_0_80, yields: % 29.44/7.99 | (188) all_201_0_100 = all_116_0_80 % 29.44/7.99 | % 29.44/7.99 | Combining equations (187,188) yields a new equation: % 29.44/7.99 | (189) all_116_0_80 = 0 % 29.44/7.99 | % 29.44/7.99 | Equations (189) can reduce 168 to: % 29.44/7.99 | (60) $false % 29.44/7.99 | % 29.44/7.99 |-The branch is then unsatisfiable % 29.44/7.99 |-Branch two: % 29.44/7.99 | (120) ~ (all_86_0_36 = 0) % 29.44/7.99 | (129) ? [v0] : ? [v1] : (empty(empty_set) = v1 & element(all_86_1_37, empty_set) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 29.44/7.99 | % 29.44/7.99 +-Applying beta-rule and splitting (107), into two cases. % 29.44/7.99 |-Branch one: % 29.44/7.99 | (126) all_86_0_36 = 0 % 29.44/7.99 | % 29.44/7.99 | Equations (126) can reduce 120 to: % 29.44/7.99 | (60) $false % 29.44/7.99 | % 29.44/7.99 |-The branch is then unsatisfiable % 29.44/7.99 |-Branch two: % 29.44/7.99 | (120) ~ (all_86_0_36 = 0) % 29.44/7.99 | (122) all_86_2_38 = 0 % 29.44/7.99 | % 29.44/7.99 +-Applying beta-rule and splitting (114), into two cases. % 29.44/7.99 |-Branch one: % 29.44/7.99 | (118) ~ (in(all_86_1_37, empty_set) = 0) % 29.44/7.99 | % 29.44/7.99 | Using (160) and (118) yields: % 29.44/7.99 | (161) $false % 29.44/7.99 | % 29.44/7.99 |-The branch is then unsatisfiable % 29.44/7.99 |-Branch two: % 29.44/7.99 | (160) in(all_86_1_37, empty_set) = 0 % 29.44/7.99 | (200) ? [v0] : ( ~ (v0 = 0) & in(empty_set, all_86_1_37) = v0) % 29.44/7.99 | % 29.44/7.99 | Instantiating formula (11) with all_86_1_37, empty_set, 0, all_86_0_36 and discharging atoms in(all_86_1_37, empty_set) = all_86_0_36, in(all_86_1_37, empty_set) = 0, yields: % 29.44/7.99 | (126) all_86_0_36 = 0 % 29.44/7.99 | % 29.44/7.99 | Equations (126) can reduce 120 to: % 29.44/7.99 | (60) $false % 29.44/7.99 | % 29.44/7.99 |-The branch is then unsatisfiable % 29.44/7.99 % SZS output end Proof for theBenchmark % 29.44/7.99 % 29.44/7.99 7396ms %------------------------------------------------------------------------------