%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU170+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n003.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:16 EDT 2022 % Result : Theorem 14.48s 4.08s % Output : Proof 17.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU170+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n003.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 05:24:58 EDT 2022 % 0.12/0.33 % CPUTime : % 0.54/0.58 ____ _ % 0.54/0.58 ___ / __ \_____(_)___ ________ __________ % 0.54/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.54/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.54/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.54/0.58 % 0.54/0.58 A Theorem Prover for First-Order Logic % 0.54/0.58 (ePrincess v.1.0) % 0.54/0.58 % 0.54/0.58 (c) Philipp Rümmer, 2009-2015 % 0.54/0.58 (c) Peter Backeman, 2014-2015 % 0.54/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.54/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.54/0.58 Bug reports to peter@backeman.se % 0.54/0.58 % 0.54/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.54/0.58 % 0.54/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.75/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.47/0.91 Prover 0: Preprocessing ... % 1.99/1.08 Prover 0: Warning: ignoring some quantifiers % 1.99/1.10 Prover 0: Constructing countermodel ... % 2.84/1.33 Prover 0: gave up % 2.84/1.33 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.84/1.35 Prover 1: Preprocessing ... % 3.03/1.44 Prover 1: Warning: ignoring some quantifiers % 3.42/1.45 Prover 1: Constructing countermodel ... % 7.13/2.34 Prover 1: gave up % 7.13/2.34 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 7.44/2.36 Prover 2: Preprocessing ... % 7.76/2.44 Prover 2: Warning: ignoring some quantifiers % 7.76/2.44 Prover 2: Constructing countermodel ... % 14.48/4.08 Prover 2: proved (1739ms) % 14.48/4.08 % 14.48/4.08 No countermodel exists, formula is valid % 14.48/4.08 % SZS status Theorem for theBenchmark % 14.48/4.08 % 14.48/4.08 Generating proof ... Warning: ignoring some quantifiers % 17.54/4.79 found it (size 130) % 17.54/4.79 % 17.54/4.79 % SZS output start Proof for theBenchmark % 17.54/4.79 Assumed formulas after preprocessing and simplification: % 17.54/4.79 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v8 = 0) & disjoint(v1, v3) = v4 & empty(v9) = 0 & empty(v7) = v8 & empty(empty_set) = 0 & subset_complement(v0, v3) = v5 & powerset(v0) = v2 & element(v3, v2) = 0 & element(v1, v2) = 0 & subset(v1, v5) = v6 & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v14 = 0 | ~ (powerset(v10) = v12) | ~ (element(v11, v12) = 0) | ~ (in(v13, v10) = v14) | ? [v15] : ( ~ (v15 = 0) & in(v13, v11) = v15)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v14 = 0 | ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v12) = v14) | ? [v15] : ((v15 = 0 & in(v13, v11) = 0) | ( ~ (v15 = 0) & in(v13, v10) = v15))) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v14 = 0 | ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v11) = v14) | ? [v15] : ((v15 = 0 & in(v13, v12) = 0) | ( ~ (v15 = 0) & in(v13, v10) = v15))) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v11) = v14) | ? [v15] : ((v15 = 0 & ~ (v14 = 0) & in(v13, v10) = 0) | ( ~ (v15 = 0) & in(v13, v12) = v15))) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v10) = v14) | ? [v15] : ((v14 = 0 & ~ (v15 = 0) & in(v13, v11) = v15) | ( ~ (v15 = 0) & in(v13, v12) = v15))) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | ~ (subset(v10, v11) = 0) | ~ (in(v12, v11) = v13) | ? [v14] : ( ~ (v14 = 0) & in(v12, v10) = v14)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (disjoint(v13, v12) = v11) | ~ (disjoint(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (subset_complement(v13, v12) = v11) | ~ (subset_complement(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (element(v13, v12) = v11) | ~ (element(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (set_difference(v13, v12) = v11) | ~ (set_difference(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (subset(v13, v12) = v11) | ~ (subset(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = v10 | ~ (in(v13, v12) = v11) | ~ (in(v13, v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (powerset(v10) = v12) | ~ (element(v11, v12) = 0) | ~ (in(v13, v11) = 0) | in(v13, v10) = 0) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v12) = 0) | ? [v14] : ( ~ (v14 = 0) & in(v13, v11) = v14 & in(v13, v10) = 0)) & ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (set_difference(v10, v11) = v12) | ~ (in(v13, v10) = 0) | ? [v14] : ((v14 = 0 & in(v13, v12) = 0) | (v14 = 0 & in(v13, v11) = 0))) & ? [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = v10 | ~ (set_difference(v11, v12) = v13) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : (((v17 = 0 & in(v14, v12) = 0) | ( ~ (v16 = 0) & in(v14, v11) = v16) | ( ~ (v15 = 0) & in(v14, v10) = v15)) & ((v16 = 0 & ~ (v17 = 0) & in(v14, v12) = v17 & in(v14, v11) = 0) | (v15 = 0 & in(v14, v10) = 0)))) & ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (disjoint(v11, v10) = v12) | ? [v13] : ( ~ (v13 = 0) & disjoint(v10, v11) = v13)) & ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (disjoint(v10, v11) = v12) | ? [v13] : (in(v13, v11) = 0 & in(v13, v10) = 0)) & ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (subset(v10, v11) = v12) | ? [v13] : ? [v14] : ( ~ (v14 = 0) & in(v13, v11) = v14 & in(v13, v10) = 0)) & ! [v10] : ! [v11] : ! [v12] : (v11 = v10 | ~ (empty(v12) = v11) | ~ (empty(v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : (v11 = v10 | ~ (powerset(v12) = v11) | ~ (powerset(v12) = v10)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (disjoint(v10, v11) = 0) | ~ (in(v12, v11) = 0) | ? [v13] : ( ~ (v13 = 0) & in(v12, v10) = v13)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (disjoint(v10, v11) = 0) | ~ (in(v12, v10) = 0) | ? [v13] : ( ~ (v13 = 0) & in(v12, v11) = v13)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (subset_complement(v10, v11) = v12) | ? [v13] : ? [v14] : (powerset(v10) = v13 & ((v14 = 0 & element(v12, v13) = 0) | ( ~ (v14 = 0) & element(v11, v13) = v14)))) & ! [v10] : ! [v11] : ! [v12] : ( ~ (subset_complement(v10, v11) = v12) | ? [v13] : ? [v14] : ((v13 = v12 & set_difference(v10, v11) = v12) | ( ~ (v14 = 0) & powerset(v10) = v13 & element(v11, v13) = v14))) & ! [v10] : ! [v11] : ! [v12] : ( ~ (subset_complement(v10, v11) = v12) | ? [v13] : ? [v14] : ((v13 = v11 & subset_complement(v10, v12) = v11) | ( ~ (v14 = 0) & powerset(v10) = v13 & element(v11, v13) = v14))) & ! [v10] : ! [v11] : ! [v12] : ( ~ (powerset(v10) = v12) | ~ (element(v11, v12) = 0) | ? [v13] : (subset_complement(v10, v13) = v11 & subset_complement(v10, v11) = v13)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (powerset(v10) = v12) | ~ (element(v11, v12) = 0) | ? [v13] : (subset_complement(v10, v11) = v13 & element(v13, v12) = 0)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (powerset(v10) = v12) | ~ (element(v11, v12) = 0) | ? [v13] : (subset_complement(v10, v11) = v13 & set_difference(v10, v11) = v13)) & ! [v10] : ! [v11] : ! [v12] : ( ~ (set_difference(v10, v11) = v12) | ? [v13] : ? [v14] : ((v13 = v12 & subset_complement(v10, v11) = v12) | ( ~ (v14 = 0) & powerset(v10) = v13 & element(v11, v13) = v14))) & ! [v10] : ! [v11] : ! [v12] : ( ~ (subset(v10, v11) = 0) | ~ (in(v12, v10) = 0) | in(v12, v11) = 0) & ! [v10] : ! [v11] : (v11 = v10 | ~ (empty(v11) = 0) | ~ (empty(v10) = 0)) & ! [v10] : ! [v11] : (v11 = v10 | ~ (set_difference(v10, empty_set) = v11)) & ! [v10] : ! [v11] : (v11 = empty_set | ~ (set_difference(empty_set, v10) = v11)) & ! [v10] : ! [v11] : (v11 = 0 | ~ (empty(v10) = v11) | ? [v12] : ? [v13] : ? [v14] : ( ~ (v14 = 0) & empty(v13) = v14 & powerset(v10) = v12 & element(v13, v12) = 0)) & ! [v10] : ! [v11] : (v11 = 0 | ~ (subset(v10, v10) = v11)) & ! [v10] : ! [v11] : ( ~ (disjoint(v10, v11) = 0) | disjoint(v11, v10) = 0) & ! [v10] : ! [v11] : ( ~ (powerset(v10) = v11) | ? [v12] : ? [v13] : ? [v14] : ((v13 = 0 & ~ (v14 = 0) & empty(v12) = v14 & element(v12, v11) = 0) | (v12 = 0 & empty(v10) = 0))) & ! [v10] : ! [v11] : ( ~ (powerset(v10) = v11) | ? [v12] : ( ~ (v12 = 0) & empty(v11) = v12)) & ! [v10] : ! [v11] : ( ~ (powerset(v10) = v11) | ? [v12] : (empty(v12) = 0 & element(v12, v11) = 0)) & ! [v10] : ! [v11] : ( ~ (in(v11, v10) = 0) | ? [v12] : ( ~ (v12 = 0) & in(v10, v11) = v12)) & ! [v10] : ! [v11] : ( ~ (in(v10, v11) = 0) | ? [v12] : ( ~ (v12 = 0) & empty(v11) = v12)) & ! [v10] : ! [v11] : ( ~ (in(v10, v11) = 0) | ? [v12] : ( ~ (v12 = 0) & in(v11, v10) = v12)) & ! [v10] : (v10 = empty_set | ~ (empty(v10) = 0)) & ? [v10] : ? [v11] : ? [v12] : disjoint(v11, v10) = v12 & ? [v10] : ? [v11] : ? [v12] : subset_complement(v11, v10) = v12 & ? [v10] : ? [v11] : ? [v12] : element(v11, v10) = v12 & ? [v10] : ? [v11] : ? [v12] : set_difference(v11, v10) = v12 & ? [v10] : ? [v11] : ? [v12] : subset(v11, v10) = v12 & ? [v10] : ? [v11] : ? [v12] : in(v11, v10) = v12 & ? [v10] : ? [v11] : empty(v10) = v11 & ? [v10] : ? [v11] : powerset(v10) = v11 & ? [v10] : ? [v11] : element(v11, v10) = 0 & ((v6 = 0 & ~ (v4 = 0)) | (v4 = 0 & ~ (v6 = 0)))) % 17.76/4.84 | 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 yields: % 17.76/4.84 | (1) ~ (all_0_1_1 = 0) & disjoint(all_0_8_8, all_0_6_6) = all_0_5_5 & empty(all_0_0_0) = 0 & empty(all_0_2_2) = all_0_1_1 & empty(empty_set) = 0 & subset_complement(all_0_9_9, all_0_6_6) = all_0_4_4 & powerset(all_0_9_9) = all_0_7_7 & element(all_0_6_6, all_0_7_7) = 0 & element(all_0_8_8, all_0_7_7) = 0 & subset(all_0_8_8, all_0_4_4) = all_0_3_3 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ~ (in(v3, v0) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v3, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ? [v5] : ((v5 = 0 & in(v3, v1) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ((v5 = 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ((v5 = 0 & ~ (v4 = 0) & in(v3, v0) = 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ? [v5] : ((v4 = 0 & ~ (v5 = 0) & in(v3, v1) = v5) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v1) = 0) | ~ (in(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & in(v2, v0) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disjoint(v3, v2) = v1) | ~ (disjoint(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 | ~ (set_difference(v3, v2) = v1) | ~ (set_difference(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(v0) = v2) | ~ (element(v1, v2) = 0) | ~ (in(v3, v1) = 0) | in(v3, v0) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ? [v4] : ((v4 = 0 & in(v3, v2) = 0) | (v4 = 0 & in(v3, v1) = 0))) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (set_difference(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (((v7 = 0 & in(v4, v2) = 0) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v5 = 0) & in(v4, v0) = v5)) & ((v6 = 0 & ~ (v7 = 0) & in(v4, v2) = v7 & in(v4, v1) = 0) | (v5 = 0 & in(v4, v0) = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disjoint(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & disjoint(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disjoint(v0, v1) = v2) | ? [v3] : (in(v3, v1) = 0 & in(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 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] : ( ~ (disjoint(v0, v1) = 0) | ~ (in(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & in(v2, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (disjoint(v0, v1) = 0) | ~ (in(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & in(v2, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : (powerset(v0) = v3 & ((v4 = 0 & element(v2, v3) = 0) | ( ~ (v4 = 0) & element(v1, v3) = v4)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v2 & set_difference(v0, v1) = v2) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v1 & subset_complement(v0, v2) = v1) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v3) = v1 & subset_complement(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v1) = v3 & element(v3, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v1) = v3 & set_difference(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_difference(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v2 & subset_complement(v0, v1) = v2) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) & ! [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 = v0 | ~ (set_difference(v0, empty_set) = v1)) & ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_difference(empty_set, v0) = v1)) & ! [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] : ( ~ (disjoint(v0, v1) = 0) | disjoint(v1, v0) = 0) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & empty(v2) = v4 & element(v2, v1) = 0) | (v2 = 0 & empty(v0) = 0))) & ! [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(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) & ! [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] : ? [v2] : disjoint(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subset_complement(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : set_difference(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 & ? [v0] : ? [v1] : empty(v0) = v1 & ? [v0] : ? [v1] : powerset(v0) = v1 & ? [v0] : ? [v1] : element(v1, v0) = 0 & ((all_0_3_3 = 0 & ~ (all_0_5_5 = 0)) | (all_0_5_5 = 0 & ~ (all_0_3_3 = 0))) % 17.84/4.86 | % 17.84/4.86 | Applying alpha-rule on (1) yields: % 17.84/4.86 | (2) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & empty(v3) = v4 & powerset(v0) = v2 & element(v3, v2) = 0)) % 17.84/4.86 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ? [v5] : ((v5 = 0 & in(v3, v1) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) % 17.84/4.86 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ (disjoint(v0, v1) = 0) | ~ (in(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & in(v2, v0) = v3)) % 17.84/4.86 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) % 17.84/4.86 | (6) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 17.84/4.86 | (7) ~ (all_0_1_1 = 0) % 17.84/4.86 | (8) ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 % 17.84/4.86 | (9) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disjoint(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & disjoint(v0, v1) = v3)) % 17.84/4.86 | (10) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 17.84/4.86 | (11) ? [v0] : ? [v1] : ? [v2] : disjoint(v1, v0) = v2 % 17.84/4.86 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 17.84/4.86 | (13) ? [v0] : ? [v1] : ? [v2] : subset_complement(v1, v0) = v2 % 17.84/4.86 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ((v5 = 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) % 17.84/4.86 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v1) = 0) | ~ (in(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & in(v2, v0) = v4)) % 17.84/4.86 | (16) subset(all_0_8_8, all_0_4_4) = all_0_3_3 % 17.84/4.86 | (17) ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) % 17.84/4.86 | (18) ? [v0] : ? [v1] : element(v1, v0) = 0 % 17.84/4.86 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 17.84/4.86 | (20) empty(all_0_2_2) = all_0_1_1 % 17.84/4.86 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ (disjoint(v0, v1) = 0) | ~ (in(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & in(v2, v1) = v3)) % 17.84/4.86 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v1 & subset_complement(v0, v2) = v1) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) % 17.84/4.86 | (23) powerset(all_0_9_9) = all_0_7_7 % 17.84/4.86 | (24) ? [v0] : ? [v1] : powerset(v0) = v1 % 17.84/4.86 | (25) element(all_0_8_8, all_0_7_7) = 0 % 17.84/4.86 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) % 17.84/4.86 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ((v5 = 0 & ~ (v4 = 0) & in(v3, v0) = 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) % 17.84/4.86 | (28) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & empty(v2) = v4 & element(v2, v1) = 0) | (v2 = 0 & empty(v0) = 0))) % 17.84/4.86 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v2 & set_difference(v0, v1) = v2) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) % 17.84/4.86 | (30) subset_complement(all_0_9_9, all_0_6_6) = all_0_4_4 % 17.84/4.87 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ~ (in(v3, v1) = 0) | in(v3, v0) = 0) % 17.84/4.87 | (32) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 17.84/4.87 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 17.84/4.87 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v1) = v3 & set_difference(v0, v1) = v3)) % 17.84/4.87 | (35) ! [v0] : ! [v1] : ( ~ (disjoint(v0, v1) = 0) | disjoint(v1, v0) = 0) % 17.84/4.87 | (36) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v3) = v1 & subset_complement(v0, v1) = v3)) % 17.84/4.87 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disjoint(v3, v2) = v1) | ~ (disjoint(v3, v2) = v0)) % 17.84/4.87 | (38) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disjoint(v0, v1) = v2) | ? [v3] : (in(v3, v1) = 0 & in(v3, v0) = 0)) % 17.84/4.87 | (39) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset_complement(v0, v1) = v2) | ? [v3] : ? [v4] : (powerset(v0) = v3 & ((v4 = 0 & element(v2, v3) = 0) | ( ~ (v4 = 0) & element(v1, v3) = v4)))) % 17.84/4.87 | (40) empty(all_0_0_0) = 0 % 17.84/4.87 | (41) empty(empty_set) = 0 % 17.84/4.87 | (42) disjoint(all_0_8_8, all_0_6_6) = all_0_5_5 % 17.84/4.87 | (43) ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 % 17.84/4.87 | (44) ? [v0] : ? [v1] : ? [v2] : set_difference(v1, v0) = v2 % 17.84/4.87 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 17.84/4.87 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ? [v4] : ((v4 = 0 & in(v3, v2) = 0) | (v4 = 0 & in(v3, v1) = 0))) % 17.84/4.87 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ? [v5] : ((v4 = 0 & ~ (v5 = 0) & in(v3, v1) = v5) | ( ~ (v5 = 0) & in(v3, v2) = v5))) % 17.84/4.87 | (48) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0)) % 17.84/4.87 | (49) (all_0_3_3 = 0 & ~ (all_0_5_5 = 0)) | (all_0_5_5 = 0 & ~ (all_0_3_3 = 0)) % 17.84/4.87 | (50) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v0, v1) = 0) | ~ (in(v2, v0) = 0) | in(v2, v1) = 0) % 17.84/4.87 | (51) ? [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (set_difference(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (((v7 = 0 & in(v4, v2) = 0) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v5 = 0) & in(v4, v0) = v5)) & ((v6 = 0 & ~ (v7 = 0) & in(v4, v2) = v7 & in(v4, v1) = 0) | (v5 = 0 & in(v4, v0) = 0)))) % 17.84/4.87 | (52) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_difference(v0, v1) = v2) | ? [v3] : ? [v4] : ((v3 = v2 & subset_complement(v0, v1) = v2) | ( ~ (v4 = 0) & powerset(v0) = v3 & element(v1, v3) = v4))) % 17.84/4.87 | (53) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 17.84/4.87 | (54) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 17.84/4.87 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 17.84/4.87 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0)) % 17.84/4.87 | (57) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 17.84/4.87 | (58) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ? [v3] : (subset_complement(v0, v1) = v3 & element(v3, v2) = 0)) % 17.84/4.87 | (59) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_difference(v0, empty_set) = v1)) % 17.84/4.87 | (60) ? [v0] : ? [v1] : empty(v0) = v1 % 17.84/4.87 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v0) = v2) | ~ (element(v1, v2) = 0) | ~ (in(v3, v0) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v3, v1) = v5)) % 17.84/4.87 | (62) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (empty(v2) = 0 & element(v2, v1) = 0)) % 17.84/4.87 | (63) ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 % 17.84/4.87 | (64) element(all_0_6_6, all_0_7_7) = 0 % 17.84/4.87 | (65) ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_difference(empty_set, v0) = v1)) % 17.84/4.87 | % 17.84/4.87 | Instantiating formula (38) with all_0_5_5, all_0_6_6, all_0_8_8 and discharging atoms disjoint(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 17.84/4.87 | (66) all_0_5_5 = 0 | ? [v0] : (in(v0, all_0_6_6) = 0 & in(v0, all_0_8_8) = 0) % 17.84/4.87 | % 17.84/4.87 | Instantiating formula (39) with all_0_4_4, all_0_6_6, all_0_9_9 and discharging atoms subset_complement(all_0_9_9, all_0_6_6) = all_0_4_4, yields: % 17.84/4.87 | (67) ? [v0] : ? [v1] : (powerset(all_0_9_9) = v0 & ((v1 = 0 & element(all_0_4_4, v0) = 0) | ( ~ (v1 = 0) & element(all_0_6_6, v0) = v1))) % 17.84/4.87 | % 17.84/4.87 | Instantiating formula (29) with all_0_4_4, all_0_6_6, all_0_9_9 and discharging atoms subset_complement(all_0_9_9, all_0_6_6) = all_0_4_4, yields: % 17.84/4.87 | (68) ? [v0] : ? [v1] : ((v0 = all_0_4_4 & set_difference(all_0_9_9, all_0_6_6) = all_0_4_4) | ( ~ (v1 = 0) & powerset(all_0_9_9) = v0 & element(all_0_6_6, v0) = v1)) % 17.84/4.87 | % 17.84/4.87 | Instantiating formula (22) with all_0_4_4, all_0_6_6, all_0_9_9 and discharging atoms subset_complement(all_0_9_9, all_0_6_6) = all_0_4_4, yields: % 17.84/4.88 | (69) ? [v0] : ? [v1] : ((v0 = all_0_6_6 & subset_complement(all_0_9_9, all_0_4_4) = all_0_6_6) | ( ~ (v1 = 0) & powerset(all_0_9_9) = v0 & element(all_0_6_6, v0) = v1)) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (36) with all_0_7_7, all_0_8_8, all_0_9_9 and discharging atoms powerset(all_0_9_9) = all_0_7_7, element(all_0_8_8, all_0_7_7) = 0, yields: % 17.84/4.88 | (70) ? [v0] : (subset_complement(all_0_9_9, v0) = all_0_8_8 & subset_complement(all_0_9_9, all_0_8_8) = v0) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (58) with all_0_7_7, all_0_8_8, all_0_9_9 and discharging atoms powerset(all_0_9_9) = all_0_7_7, element(all_0_8_8, all_0_7_7) = 0, yields: % 17.84/4.88 | (71) ? [v0] : (subset_complement(all_0_9_9, all_0_8_8) = v0 & element(v0, all_0_7_7) = 0) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (34) with all_0_7_7, all_0_8_8, all_0_9_9 and discharging atoms powerset(all_0_9_9) = all_0_7_7, element(all_0_8_8, all_0_7_7) = 0, yields: % 17.84/4.88 | (72) ? [v0] : (subset_complement(all_0_9_9, all_0_8_8) = v0 & set_difference(all_0_9_9, all_0_8_8) = v0) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (48) with all_0_3_3, all_0_4_4, all_0_8_8 and discharging atoms subset(all_0_8_8, all_0_4_4) = all_0_3_3, yields: % 17.84/4.88 | (73) all_0_3_3 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & in(v0, all_0_4_4) = v1 & in(v0, all_0_8_8) = 0) % 17.84/4.88 | % 17.84/4.88 | Instantiating (72) with all_32_0_35 yields: % 17.84/4.88 | (74) subset_complement(all_0_9_9, all_0_8_8) = all_32_0_35 & set_difference(all_0_9_9, all_0_8_8) = all_32_0_35 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (74) yields: % 17.84/4.88 | (75) subset_complement(all_0_9_9, all_0_8_8) = all_32_0_35 % 17.84/4.88 | (76) set_difference(all_0_9_9, all_0_8_8) = all_32_0_35 % 17.84/4.88 | % 17.84/4.88 | Instantiating (71) with all_34_0_36 yields: % 17.84/4.88 | (77) subset_complement(all_0_9_9, all_0_8_8) = all_34_0_36 & element(all_34_0_36, all_0_7_7) = 0 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (77) yields: % 17.84/4.88 | (78) subset_complement(all_0_9_9, all_0_8_8) = all_34_0_36 % 17.84/4.88 | (79) element(all_34_0_36, all_0_7_7) = 0 % 17.84/4.88 | % 17.84/4.88 | Instantiating (70) with all_40_0_39 yields: % 17.84/4.88 | (80) subset_complement(all_0_9_9, all_40_0_39) = all_0_8_8 & subset_complement(all_0_9_9, all_0_8_8) = all_40_0_39 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (80) yields: % 17.84/4.88 | (81) subset_complement(all_0_9_9, all_40_0_39) = all_0_8_8 % 17.84/4.88 | (82) subset_complement(all_0_9_9, all_0_8_8) = all_40_0_39 % 17.84/4.88 | % 17.84/4.88 | Instantiating (69) with all_45_0_44, all_45_1_45 yields: % 17.84/4.88 | (83) (all_45_1_45 = all_0_6_6 & subset_complement(all_0_9_9, all_0_4_4) = all_0_6_6) | ( ~ (all_45_0_44 = 0) & powerset(all_0_9_9) = all_45_1_45 & element(all_0_6_6, all_45_1_45) = all_45_0_44) % 17.84/4.88 | % 17.84/4.88 | Instantiating (68) with all_48_0_47, all_48_1_48 yields: % 17.84/4.88 | (84) (all_48_1_48 = all_0_4_4 & set_difference(all_0_9_9, all_0_6_6) = all_0_4_4) | ( ~ (all_48_0_47 = 0) & powerset(all_0_9_9) = all_48_1_48 & element(all_0_6_6, all_48_1_48) = all_48_0_47) % 17.84/4.88 | % 17.84/4.88 | Instantiating (67) with all_51_0_50, all_51_1_51 yields: % 17.84/4.88 | (85) powerset(all_0_9_9) = all_51_1_51 & ((all_51_0_50 = 0 & element(all_0_4_4, all_51_1_51) = 0) | ( ~ (all_51_0_50 = 0) & element(all_0_6_6, all_51_1_51) = all_51_0_50)) % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (85) yields: % 17.84/4.88 | (86) powerset(all_0_9_9) = all_51_1_51 % 17.84/4.88 | (87) (all_51_0_50 = 0 & element(all_0_4_4, all_51_1_51) = 0) | ( ~ (all_51_0_50 = 0) & element(all_0_6_6, all_51_1_51) = all_51_0_50) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (5) with all_0_9_9, all_0_8_8, all_34_0_36, all_40_0_39 and discharging atoms subset_complement(all_0_9_9, all_0_8_8) = all_40_0_39, subset_complement(all_0_9_9, all_0_8_8) = all_34_0_36, yields: % 17.84/4.88 | (88) all_40_0_39 = all_34_0_36 % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (5) with all_0_9_9, all_0_8_8, all_32_0_35, all_40_0_39 and discharging atoms subset_complement(all_0_9_9, all_0_8_8) = all_40_0_39, subset_complement(all_0_9_9, all_0_8_8) = all_32_0_35, yields: % 17.84/4.88 | (89) all_40_0_39 = all_32_0_35 % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (55) with all_0_9_9, all_51_1_51, all_0_7_7 and discharging atoms powerset(all_0_9_9) = all_51_1_51, powerset(all_0_9_9) = all_0_7_7, yields: % 17.84/4.88 | (90) all_51_1_51 = all_0_7_7 % 17.84/4.88 | % 17.84/4.88 | Combining equations (89,88) yields a new equation: % 17.84/4.88 | (91) all_34_0_36 = all_32_0_35 % 17.84/4.88 | % 17.84/4.88 | Combining equations (91,88) yields a new equation: % 17.84/4.88 | (89) all_40_0_39 = all_32_0_35 % 17.84/4.88 | % 17.84/4.88 | From (89) and (81) follows: % 17.84/4.88 | (93) subset_complement(all_0_9_9, all_32_0_35) = all_0_8_8 % 17.84/4.88 | % 17.84/4.88 | From (90) and (86) follows: % 17.84/4.88 | (23) powerset(all_0_9_9) = all_0_7_7 % 17.84/4.88 | % 17.84/4.88 | From (91) and (79) follows: % 17.84/4.88 | (95) element(all_32_0_35, all_0_7_7) = 0 % 17.84/4.88 | % 17.84/4.88 +-Applying beta-rule and splitting (87), into two cases. % 17.84/4.88 |-Branch one: % 17.84/4.88 | (96) all_51_0_50 = 0 & element(all_0_4_4, all_51_1_51) = 0 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (96) yields: % 17.84/4.88 | (97) all_51_0_50 = 0 % 17.84/4.88 | (98) element(all_0_4_4, all_51_1_51) = 0 % 17.84/4.88 | % 17.84/4.88 | From (90) and (98) follows: % 17.84/4.88 | (99) element(all_0_4_4, all_0_7_7) = 0 % 17.84/4.88 | % 17.84/4.88 +-Applying beta-rule and splitting (83), into two cases. % 17.84/4.88 |-Branch one: % 17.84/4.88 | (100) all_45_1_45 = all_0_6_6 & subset_complement(all_0_9_9, all_0_4_4) = all_0_6_6 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (100) yields: % 17.84/4.88 | (101) all_45_1_45 = all_0_6_6 % 17.84/4.88 | (102) subset_complement(all_0_9_9, all_0_4_4) = all_0_6_6 % 17.84/4.88 | % 17.84/4.88 +-Applying beta-rule and splitting (84), into two cases. % 17.84/4.88 |-Branch one: % 17.84/4.88 | (103) all_48_1_48 = all_0_4_4 & set_difference(all_0_9_9, all_0_6_6) = all_0_4_4 % 17.84/4.88 | % 17.84/4.88 | Applying alpha-rule on (103) yields: % 17.84/4.88 | (104) all_48_1_48 = all_0_4_4 % 17.84/4.88 | (105) set_difference(all_0_9_9, all_0_6_6) = all_0_4_4 % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (29) with all_0_8_8, all_32_0_35, all_0_9_9 and discharging atoms subset_complement(all_0_9_9, all_32_0_35) = all_0_8_8, yields: % 17.84/4.88 | (106) ? [v0] : ? [v1] : ((v0 = all_0_8_8 & set_difference(all_0_9_9, all_32_0_35) = all_0_8_8) | ( ~ (v1 = 0) & powerset(all_0_9_9) = v0 & element(all_32_0_35, v0) = v1)) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (29) with all_0_6_6, all_0_4_4, all_0_9_9 and discharging atoms subset_complement(all_0_9_9, all_0_4_4) = all_0_6_6, yields: % 17.84/4.88 | (107) ? [v0] : ? [v1] : ((v0 = all_0_6_6 & set_difference(all_0_9_9, all_0_4_4) = all_0_6_6) | ( ~ (v1 = 0) & powerset(all_0_9_9) = v0 & element(all_0_4_4, v0) = v1)) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (34) with all_0_7_7, all_32_0_35, all_0_9_9 and discharging atoms powerset(all_0_9_9) = all_0_7_7, element(all_32_0_35, all_0_7_7) = 0, yields: % 17.84/4.88 | (108) ? [v0] : (subset_complement(all_0_9_9, all_32_0_35) = v0 & set_difference(all_0_9_9, all_32_0_35) = v0) % 17.84/4.88 | % 17.84/4.88 | Instantiating formula (34) with all_0_7_7, all_0_4_4, all_0_9_9 and discharging atoms powerset(all_0_9_9) = all_0_7_7, element(all_0_4_4, all_0_7_7) = 0, yields: % 17.84/4.88 | (109) ? [v0] : (subset_complement(all_0_9_9, all_0_4_4) = v0 & set_difference(all_0_9_9, all_0_4_4) = v0) % 17.84/4.88 | % 17.84/4.88 | Instantiating (109) with all_82_0_56 yields: % 17.84/4.88 | (110) subset_complement(all_0_9_9, all_0_4_4) = all_82_0_56 & set_difference(all_0_9_9, all_0_4_4) = all_82_0_56 % 17.84/4.88 | % 17.84/4.89 | Applying alpha-rule on (110) yields: % 17.84/4.89 | (111) subset_complement(all_0_9_9, all_0_4_4) = all_82_0_56 % 17.84/4.89 | (112) set_difference(all_0_9_9, all_0_4_4) = all_82_0_56 % 17.84/4.89 | % 17.84/4.89 | Instantiating (108) with all_93_0_64 yields: % 17.84/4.89 | (113) subset_complement(all_0_9_9, all_32_0_35) = all_93_0_64 & set_difference(all_0_9_9, all_32_0_35) = all_93_0_64 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (113) yields: % 17.84/4.89 | (114) subset_complement(all_0_9_9, all_32_0_35) = all_93_0_64 % 17.84/4.89 | (115) set_difference(all_0_9_9, all_32_0_35) = all_93_0_64 % 17.84/4.89 | % 17.84/4.89 | Instantiating (107) with all_101_0_68, all_101_1_69 yields: % 17.84/4.89 | (116) (all_101_1_69 = all_0_6_6 & set_difference(all_0_9_9, all_0_4_4) = all_0_6_6) | ( ~ (all_101_0_68 = 0) & powerset(all_0_9_9) = all_101_1_69 & element(all_0_4_4, all_101_1_69) = all_101_0_68) % 17.84/4.89 | % 17.84/4.89 | Instantiating (106) with all_102_0_70, all_102_1_71 yields: % 17.84/4.89 | (117) (all_102_1_71 = all_0_8_8 & set_difference(all_0_9_9, all_32_0_35) = all_0_8_8) | ( ~ (all_102_0_70 = 0) & powerset(all_0_9_9) = all_102_1_71 & element(all_32_0_35, all_102_1_71) = all_102_0_70) % 17.84/4.89 | % 17.84/4.89 +-Applying beta-rule and splitting (116), into two cases. % 17.84/4.89 |-Branch one: % 17.84/4.89 | (118) all_101_1_69 = all_0_6_6 & set_difference(all_0_9_9, all_0_4_4) = all_0_6_6 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (118) yields: % 17.84/4.89 | (119) all_101_1_69 = all_0_6_6 % 17.84/4.89 | (120) set_difference(all_0_9_9, all_0_4_4) = all_0_6_6 % 17.84/4.89 | % 17.84/4.89 +-Applying beta-rule and splitting (117), into two cases. % 17.84/4.89 |-Branch one: % 17.84/4.89 | (121) all_102_1_71 = all_0_8_8 & set_difference(all_0_9_9, all_32_0_35) = all_0_8_8 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (121) yields: % 17.84/4.89 | (122) all_102_1_71 = all_0_8_8 % 17.84/4.89 | (123) set_difference(all_0_9_9, all_32_0_35) = all_0_8_8 % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (26) with all_0_9_9, all_32_0_35, all_0_8_8, all_93_0_64 and discharging atoms set_difference(all_0_9_9, all_32_0_35) = all_93_0_64, set_difference(all_0_9_9, all_32_0_35) = all_0_8_8, yields: % 17.84/4.89 | (124) all_93_0_64 = all_0_8_8 % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (26) with all_0_9_9, all_0_4_4, all_0_6_6, all_82_0_56 and discharging atoms set_difference(all_0_9_9, all_0_4_4) = all_82_0_56, set_difference(all_0_9_9, all_0_4_4) = all_0_6_6, yields: % 17.84/4.89 | (125) all_82_0_56 = all_0_6_6 % 17.84/4.89 | % 17.84/4.89 | From (124) and (115) follows: % 17.84/4.89 | (123) set_difference(all_0_9_9, all_32_0_35) = all_0_8_8 % 17.84/4.89 | % 17.84/4.89 | From (125) and (112) follows: % 17.84/4.89 | (120) set_difference(all_0_9_9, all_0_4_4) = all_0_6_6 % 17.84/4.89 | % 17.84/4.89 +-Applying beta-rule and splitting (49), into two cases. % 17.84/4.89 |-Branch one: % 17.84/4.89 | (128) all_0_3_3 = 0 & ~ (all_0_5_5 = 0) % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (128) yields: % 17.84/4.89 | (129) all_0_3_3 = 0 % 17.84/4.89 | (130) ~ (all_0_5_5 = 0) % 17.84/4.89 | % 17.84/4.89 | From (129) and (16) follows: % 17.84/4.89 | (131) subset(all_0_8_8, all_0_4_4) = 0 % 17.84/4.89 | % 17.84/4.89 +-Applying beta-rule and splitting (66), into two cases. % 17.84/4.89 |-Branch one: % 17.84/4.89 | (132) all_0_5_5 = 0 % 17.84/4.89 | % 17.84/4.89 | Equations (132) can reduce 130 to: % 17.84/4.89 | (133) $false % 17.84/4.89 | % 17.84/4.89 |-The branch is then unsatisfiable % 17.84/4.89 |-Branch two: % 17.84/4.89 | (130) ~ (all_0_5_5 = 0) % 17.84/4.89 | (135) ? [v0] : (in(v0, all_0_6_6) = 0 & in(v0, all_0_8_8) = 0) % 17.84/4.89 | % 17.84/4.89 | Instantiating (135) with all_224_0_118 yields: % 17.84/4.89 | (136) in(all_224_0_118, all_0_6_6) = 0 & in(all_224_0_118, all_0_8_8) = 0 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (136) yields: % 17.84/4.89 | (137) in(all_224_0_118, all_0_6_6) = 0 % 17.84/4.89 | (138) in(all_224_0_118, all_0_8_8) = 0 % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (27) with 0, all_224_0_118, all_0_4_4, all_0_6_6, all_0_9_9 and discharging atoms set_difference(all_0_9_9, all_0_6_6) = all_0_4_4, in(all_224_0_118, all_0_6_6) = 0, yields: % 17.84/4.89 | (139) ? [v0] : ( ~ (v0 = 0) & in(all_224_0_118, all_0_4_4) = v0) % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (56) with all_224_0_118, all_0_6_6, all_0_4_4, all_0_9_9 and discharging atoms set_difference(all_0_9_9, all_0_4_4) = all_0_6_6, in(all_224_0_118, all_0_6_6) = 0, yields: % 17.84/4.89 | (140) ? [v0] : ( ~ (v0 = 0) & in(all_224_0_118, all_0_4_4) = v0 & in(all_224_0_118, all_0_9_9) = 0) % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (50) with all_224_0_118, all_0_4_4, all_0_8_8 and discharging atoms subset(all_0_8_8, all_0_4_4) = 0, in(all_224_0_118, all_0_8_8) = 0, yields: % 17.84/4.89 | (141) in(all_224_0_118, all_0_4_4) = 0 % 17.84/4.89 | % 17.84/4.89 | Instantiating (140) with all_245_0_124 yields: % 17.84/4.89 | (142) ~ (all_245_0_124 = 0) & in(all_224_0_118, all_0_4_4) = all_245_0_124 & in(all_224_0_118, all_0_9_9) = 0 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (142) yields: % 17.84/4.89 | (143) ~ (all_245_0_124 = 0) % 17.84/4.89 | (144) in(all_224_0_118, all_0_4_4) = all_245_0_124 % 17.84/4.89 | (145) in(all_224_0_118, all_0_9_9) = 0 % 17.84/4.89 | % 17.84/4.89 | Instantiating (139) with all_267_0_135 yields: % 17.84/4.89 | (146) ~ (all_267_0_135 = 0) & in(all_224_0_118, all_0_4_4) = all_267_0_135 % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (146) yields: % 17.84/4.89 | (147) ~ (all_267_0_135 = 0) % 17.84/4.89 | (148) in(all_224_0_118, all_0_4_4) = all_267_0_135 % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (19) with all_224_0_118, all_0_4_4, all_245_0_124, all_267_0_135 and discharging atoms in(all_224_0_118, all_0_4_4) = all_267_0_135, in(all_224_0_118, all_0_4_4) = all_245_0_124, yields: % 17.84/4.89 | (149) all_267_0_135 = all_245_0_124 % 17.84/4.89 | % 17.84/4.89 | Instantiating formula (19) with all_224_0_118, all_0_4_4, 0, all_267_0_135 and discharging atoms in(all_224_0_118, all_0_4_4) = all_267_0_135, in(all_224_0_118, all_0_4_4) = 0, yields: % 17.84/4.89 | (150) all_267_0_135 = 0 % 17.84/4.89 | % 17.84/4.89 | Combining equations (149,150) yields a new equation: % 17.84/4.89 | (151) all_245_0_124 = 0 % 17.84/4.89 | % 17.84/4.89 | Simplifying 151 yields: % 17.84/4.89 | (152) all_245_0_124 = 0 % 17.84/4.89 | % 17.84/4.89 | Equations (152) can reduce 143 to: % 17.84/4.89 | (133) $false % 17.84/4.89 | % 17.84/4.89 |-The branch is then unsatisfiable % 17.84/4.89 |-Branch two: % 17.84/4.89 | (154) all_0_5_5 = 0 & ~ (all_0_3_3 = 0) % 17.84/4.89 | % 17.84/4.89 | Applying alpha-rule on (154) yields: % 17.84/4.89 | (132) all_0_5_5 = 0 % 17.84/4.89 | (156) ~ (all_0_3_3 = 0) % 17.84/4.89 | % 17.84/4.89 | From (132) and (42) follows: % 17.84/4.89 | (157) disjoint(all_0_8_8, all_0_6_6) = 0 % 17.84/4.89 | % 17.84/4.89 +-Applying beta-rule and splitting (73), into two cases. % 17.84/4.89 |-Branch one: % 17.84/4.89 | (129) all_0_3_3 = 0 % 17.84/4.89 | % 17.84/4.89 | Equations (129) can reduce 156 to: % 17.84/4.89 | (133) $false % 17.84/4.89 | % 17.84/4.89 |-The branch is then unsatisfiable % 17.84/4.89 |-Branch two: % 17.84/4.89 | (156) ~ (all_0_3_3 = 0) % 17.84/4.90 | (161) ? [v0] : ? [v1] : ( ~ (v1 = 0) & in(v0, all_0_4_4) = v1 & in(v0, all_0_8_8) = 0) % 17.84/4.90 | % 17.84/4.90 | Instantiating (161) with all_224_0_209, all_224_1_210 yields: % 17.84/4.90 | (162) ~ (all_224_0_209 = 0) & in(all_224_1_210, all_0_4_4) = all_224_0_209 & in(all_224_1_210, all_0_8_8) = 0 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (162) yields: % 17.84/4.90 | (163) ~ (all_224_0_209 = 0) % 17.84/4.90 | (164) in(all_224_1_210, all_0_4_4) = all_224_0_209 % 17.84/4.90 | (165) in(all_224_1_210, all_0_8_8) = 0 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (3) with all_224_0_209, all_224_1_210, all_0_4_4, all_0_6_6, all_0_9_9 and discharging atoms set_difference(all_0_9_9, all_0_6_6) = all_0_4_4, in(all_224_1_210, all_0_4_4) = all_224_0_209, yields: % 17.84/4.90 | (166) all_224_0_209 = 0 | ? [v0] : ((v0 = 0 & in(all_224_1_210, all_0_6_6) = 0) | ( ~ (v0 = 0) & in(all_224_1_210, all_0_9_9) = v0)) % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (56) with all_224_1_210, all_0_8_8, all_32_0_35, all_0_9_9 and discharging atoms set_difference(all_0_9_9, all_32_0_35) = all_0_8_8, in(all_224_1_210, all_0_8_8) = 0, yields: % 17.84/4.90 | (167) ? [v0] : ( ~ (v0 = 0) & in(all_224_1_210, all_32_0_35) = v0 & in(all_224_1_210, all_0_9_9) = 0) % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (21) with all_224_1_210, all_0_6_6, all_0_8_8 and discharging atoms disjoint(all_0_8_8, all_0_6_6) = 0, in(all_224_1_210, all_0_8_8) = 0, yields: % 17.84/4.90 | (168) ? [v0] : ( ~ (v0 = 0) & in(all_224_1_210, all_0_6_6) = v0) % 17.84/4.90 | % 17.84/4.90 | Instantiating (168) with all_258_0_224 yields: % 17.84/4.90 | (169) ~ (all_258_0_224 = 0) & in(all_224_1_210, all_0_6_6) = all_258_0_224 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (169) yields: % 17.84/4.90 | (170) ~ (all_258_0_224 = 0) % 17.84/4.90 | (171) in(all_224_1_210, all_0_6_6) = all_258_0_224 % 17.84/4.90 | % 17.84/4.90 | Instantiating (167) with all_260_0_225 yields: % 17.84/4.90 | (172) ~ (all_260_0_225 = 0) & in(all_224_1_210, all_32_0_35) = all_260_0_225 & in(all_224_1_210, all_0_9_9) = 0 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (172) yields: % 17.84/4.90 | (173) ~ (all_260_0_225 = 0) % 17.84/4.90 | (174) in(all_224_1_210, all_32_0_35) = all_260_0_225 % 17.84/4.90 | (175) in(all_224_1_210, all_0_9_9) = 0 % 17.84/4.90 | % 17.84/4.90 +-Applying beta-rule and splitting (166), into two cases. % 17.84/4.90 |-Branch one: % 17.84/4.90 | (176) all_224_0_209 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (176) can reduce 163 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (163) ~ (all_224_0_209 = 0) % 17.84/4.90 | (179) ? [v0] : ((v0 = 0 & in(all_224_1_210, all_0_6_6) = 0) | ( ~ (v0 = 0) & in(all_224_1_210, all_0_9_9) = v0)) % 17.84/4.90 | % 17.84/4.90 | Instantiating (179) with all_358_0_282 yields: % 17.84/4.90 | (180) (all_358_0_282 = 0 & in(all_224_1_210, all_0_6_6) = 0) | ( ~ (all_358_0_282 = 0) & in(all_224_1_210, all_0_9_9) = all_358_0_282) % 17.84/4.90 | % 17.84/4.90 +-Applying beta-rule and splitting (180), into two cases. % 17.84/4.90 |-Branch one: % 17.84/4.90 | (181) all_358_0_282 = 0 & in(all_224_1_210, all_0_6_6) = 0 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (181) yields: % 17.84/4.90 | (182) all_358_0_282 = 0 % 17.84/4.90 | (183) in(all_224_1_210, all_0_6_6) = 0 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (19) with all_224_1_210, all_0_6_6, 0, all_258_0_224 and discharging atoms in(all_224_1_210, all_0_6_6) = all_258_0_224, in(all_224_1_210, all_0_6_6) = 0, yields: % 17.84/4.90 | (184) all_258_0_224 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (184) can reduce 170 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (186) ~ (all_358_0_282 = 0) & in(all_224_1_210, all_0_9_9) = all_358_0_282 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (186) yields: % 17.84/4.90 | (187) ~ (all_358_0_282 = 0) % 17.84/4.90 | (188) in(all_224_1_210, all_0_9_9) = all_358_0_282 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (19) with all_224_1_210, all_0_9_9, 0, all_358_0_282 and discharging atoms in(all_224_1_210, all_0_9_9) = all_358_0_282, in(all_224_1_210, all_0_9_9) = 0, yields: % 17.84/4.90 | (182) all_358_0_282 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (182) can reduce 187 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (191) ~ (all_102_0_70 = 0) & powerset(all_0_9_9) = all_102_1_71 & element(all_32_0_35, all_102_1_71) = all_102_0_70 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (191) yields: % 17.84/4.90 | (192) ~ (all_102_0_70 = 0) % 17.84/4.90 | (193) powerset(all_0_9_9) = all_102_1_71 % 17.84/4.90 | (194) element(all_32_0_35, all_102_1_71) = all_102_0_70 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (55) with all_0_9_9, all_102_1_71, all_0_7_7 and discharging atoms powerset(all_0_9_9) = all_102_1_71, powerset(all_0_9_9) = all_0_7_7, yields: % 17.84/4.90 | (195) all_102_1_71 = all_0_7_7 % 17.84/4.90 | % 17.84/4.90 | From (195) and (194) follows: % 17.84/4.90 | (196) element(all_32_0_35, all_0_7_7) = all_102_0_70 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (33) with all_32_0_35, all_0_7_7, all_102_0_70, 0 and discharging atoms element(all_32_0_35, all_0_7_7) = all_102_0_70, element(all_32_0_35, all_0_7_7) = 0, yields: % 17.84/4.90 | (197) all_102_0_70 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (197) can reduce 192 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (199) ~ (all_101_0_68 = 0) & powerset(all_0_9_9) = all_101_1_69 & element(all_0_4_4, all_101_1_69) = all_101_0_68 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (199) yields: % 17.84/4.90 | (200) ~ (all_101_0_68 = 0) % 17.84/4.90 | (201) powerset(all_0_9_9) = all_101_1_69 % 17.84/4.90 | (202) element(all_0_4_4, all_101_1_69) = all_101_0_68 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (55) with all_0_9_9, all_101_1_69, all_0_7_7 and discharging atoms powerset(all_0_9_9) = all_101_1_69, powerset(all_0_9_9) = all_0_7_7, yields: % 17.84/4.90 | (203) all_101_1_69 = all_0_7_7 % 17.84/4.90 | % 17.84/4.90 | From (203) and (202) follows: % 17.84/4.90 | (204) element(all_0_4_4, all_0_7_7) = all_101_0_68 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (33) with all_0_4_4, all_0_7_7, all_101_0_68, 0 and discharging atoms element(all_0_4_4, all_0_7_7) = all_101_0_68, element(all_0_4_4, all_0_7_7) = 0, yields: % 17.84/4.90 | (205) all_101_0_68 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (205) can reduce 200 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (207) ~ (all_48_0_47 = 0) & powerset(all_0_9_9) = all_48_1_48 & element(all_0_6_6, all_48_1_48) = all_48_0_47 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (207) yields: % 17.84/4.90 | (208) ~ (all_48_0_47 = 0) % 17.84/4.90 | (209) powerset(all_0_9_9) = all_48_1_48 % 17.84/4.90 | (210) element(all_0_6_6, all_48_1_48) = all_48_0_47 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (55) with all_0_9_9, all_48_1_48, all_0_7_7 and discharging atoms powerset(all_0_9_9) = all_48_1_48, powerset(all_0_9_9) = all_0_7_7, yields: % 17.84/4.90 | (211) all_48_1_48 = all_0_7_7 % 17.84/4.90 | % 17.84/4.90 | From (211) and (210) follows: % 17.84/4.90 | (212) element(all_0_6_6, all_0_7_7) = all_48_0_47 % 17.84/4.90 | % 17.84/4.90 | Instantiating formula (33) with all_0_6_6, all_0_7_7, all_48_0_47, 0 and discharging atoms element(all_0_6_6, all_0_7_7) = all_48_0_47, element(all_0_6_6, all_0_7_7) = 0, yields: % 17.84/4.90 | (213) all_48_0_47 = 0 % 17.84/4.90 | % 17.84/4.90 | Equations (213) can reduce 208 to: % 17.84/4.90 | (133) $false % 17.84/4.90 | % 17.84/4.90 |-The branch is then unsatisfiable % 17.84/4.90 |-Branch two: % 17.84/4.90 | (215) ~ (all_45_0_44 = 0) & powerset(all_0_9_9) = all_45_1_45 & element(all_0_6_6, all_45_1_45) = all_45_0_44 % 17.84/4.90 | % 17.84/4.90 | Applying alpha-rule on (215) yields: % 17.84/4.91 | (216) ~ (all_45_0_44 = 0) % 17.84/4.91 | (217) powerset(all_0_9_9) = all_45_1_45 % 17.84/4.91 | (218) element(all_0_6_6, all_45_1_45) = all_45_0_44 % 17.84/4.91 | % 17.84/4.91 | Instantiating formula (55) with all_0_9_9, all_45_1_45, all_0_7_7 and discharging atoms powerset(all_0_9_9) = all_45_1_45, powerset(all_0_9_9) = all_0_7_7, yields: % 17.84/4.91 | (219) all_45_1_45 = all_0_7_7 % 17.84/4.91 | % 17.84/4.91 | From (219) and (218) follows: % 17.84/4.91 | (220) element(all_0_6_6, all_0_7_7) = all_45_0_44 % 17.84/4.91 | % 17.84/4.91 | Instantiating formula (33) with all_0_6_6, all_0_7_7, all_45_0_44, 0 and discharging atoms element(all_0_6_6, all_0_7_7) = all_45_0_44, element(all_0_6_6, all_0_7_7) = 0, yields: % 17.84/4.91 | (221) all_45_0_44 = 0 % 17.84/4.91 | % 17.84/4.91 | Equations (221) can reduce 216 to: % 17.84/4.91 | (133) $false % 17.84/4.91 | % 17.84/4.91 |-The branch is then unsatisfiable % 17.84/4.91 |-Branch two: % 17.84/4.91 | (223) ~ (all_51_0_50 = 0) & element(all_0_6_6, all_51_1_51) = all_51_0_50 % 17.84/4.91 | % 17.84/4.91 | Applying alpha-rule on (223) yields: % 17.84/4.91 | (224) ~ (all_51_0_50 = 0) % 17.84/4.91 | (225) element(all_0_6_6, all_51_1_51) = all_51_0_50 % 17.84/4.91 | % 17.84/4.91 | From (90) and (225) follows: % 17.84/4.91 | (226) element(all_0_6_6, all_0_7_7) = all_51_0_50 % 17.84/4.91 | % 17.84/4.91 | Instantiating formula (33) with all_0_6_6, all_0_7_7, all_51_0_50, 0 and discharging atoms element(all_0_6_6, all_0_7_7) = all_51_0_50, element(all_0_6_6, all_0_7_7) = 0, yields: % 17.84/4.91 | (97) all_51_0_50 = 0 % 17.84/4.91 | % 17.84/4.91 | Equations (97) can reduce 224 to: % 17.84/4.91 | (133) $false % 17.84/4.91 | % 17.84/4.91 |-The branch is then unsatisfiable % 17.84/4.91 % SZS output end Proof for theBenchmark % 17.84/4.91 % 17.84/4.91 4315ms %------------------------------------------------------------------------------