%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU109+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n027.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:46:38 EDT 2022 % Result : Theorem 68.35s 42.23s % Output : Proof 99.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU109+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n027.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 18 20:34:08 EDT 2022 % 0.13/0.34 % CPUTime : % 0.55/0.59 ____ _ % 0.55/0.59 ___ / __ \_____(_)___ ________ __________ % 0.55/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.59 % 0.55/0.59 A Theorem Prover for First-Order Logic % 0.55/0.60 (ePrincess v.1.0) % 0.55/0.60 % 0.55/0.60 (c) Philipp Rümmer, 2009-2015 % 0.55/0.60 (c) Peter Backeman, 2014-2015 % 0.55/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.60 Bug reports to peter@backeman.se % 0.55/0.60 % 0.55/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.60 % 0.55/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.71/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.66/0.94 Prover 0: Preprocessing ... % 2.40/1.20 Prover 0: Warning: ignoring some quantifiers % 2.40/1.22 Prover 0: Constructing countermodel ... % 3.79/1.55 Prover 0: gave up % 3.79/1.56 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.79/1.60 Prover 1: Preprocessing ... % 4.45/1.72 Prover 1: Warning: ignoring some quantifiers % 4.45/1.73 Prover 1: Constructing countermodel ... % 5.49/1.97 Prover 1: gave up % 5.49/1.97 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 5.82/2.01 Prover 2: Preprocessing ... % 6.45/2.12 Prover 2: Warning: ignoring some quantifiers % 6.45/2.13 Prover 2: Constructing countermodel ... % 14.82/4.17 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 14.96/4.21 Prover 3: Preprocessing ... % 15.29/4.26 Prover 3: Warning: ignoring some quantifiers % 15.29/4.27 Prover 3: Constructing countermodel ... % 15.57/4.37 Prover 3: gave up % 15.57/4.37 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 15.82/4.39 Prover 4: Preprocessing ... % 16.17/4.49 Prover 4: Warning: ignoring some quantifiers % 16.31/4.50 Prover 4: Constructing countermodel ... % 19.89/5.39 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 19.98/5.41 Prover 5: Preprocessing ... % 20.22/5.46 Prover 5: Warning: ignoring some quantifiers % 20.22/5.46 Prover 5: Constructing countermodel ... % 43.58/20.83 Prover 5: stopped % 43.87/21.04 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 43.99/21.06 Prover 6: Preprocessing ... % 44.07/21.11 Prover 6: Warning: ignoring some quantifiers % 44.30/21.12 Prover 6: Constructing countermodel ... % 68.35/42.23 Prover 4: proved (2393ms) % 68.35/42.23 Prover 6: stopped % 68.35/42.23 Prover 2: stopped % 68.35/42.23 % 68.35/42.23 No countermodel exists, formula is valid % 68.35/42.23 % SZS status Theorem for theBenchmark % 68.35/42.23 % 68.35/42.23 Generating proof ... Warning: ignoring some quantifiers % 98.82/61.84 found it (size 423) % 98.82/61.84 % 98.82/61.84 % SZS output start Proof for theBenchmark % 98.82/61.84 Assumed formulas after preprocessing and simplification: % 98.82/61.84 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v13 = 0) & ~ (v11 = 0) & ~ (v8 = 0) & ~ (v3 = 0) & ~ (v1 = 0) & cap_closed(v10) = 0 & set_intersection2(v0, v2) = v4 & preboolean(v10) = 0 & preboolean(v4) = v6 & preboolean(v2) = 0 & preboolean(v0) = 0 & cup_closed(v10) = 0 & diff_closed(v10) = 0 & empty(v12) = v13 & empty(v10) = v11 & empty(v9) = 0 & empty(v7) = v8 & empty(v4) = v5 & empty(v2) = v3 & empty(v0) = v1 & empty(empty_set) = 0 & finite(v12) = 0 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v16) = v18) | ? [v19] : ? [v20] : (in(v17, v15) = v20 & in(v17, v14) = v19 & ( ~ (v20 = 0) | ~ (v19 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (element(v14, v16) = v18) | ? [v19] : ( ~ (v19 = 0) & in(v14, v15) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v15) = v18) | ? [v19] : ? [v20] : (in(v17, v16) = v19 & in(v17, v14) = v20 & ( ~ (v19 = 0) | (v20 = 0 & v18 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v14) = v18) | ? [v19] : ? [v20] : (in(v17, v16) = v19 & in(v17, v15) = v20 & ( ~ (v19 = 0) | (v20 = 0 & v18 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (powerset(v15) = v16) | ~ (element(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & subset(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (powerset(v14) = v15) | ~ (finite(v16) = v17) | ? [v18] : (( ~ (v18 = 0) & element(v16, v15) = v18) | ( ~ (v18 = 0) & finite(v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (element(v14, v16) = v17) | ~ (in(v14, v15) = 0) | ? [v18] : ? [v19] : ( ~ (v19 = 0) & powerset(v16) = v18 & element(v15, v18) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (subset(v17, v16) = v15) | ~ (subset(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (set_difference(v17, v16) = v15) | ~ (set_difference(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (set_intersection2(v17, v16) = v15) | ~ (set_intersection2(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (set_union2(v17, v16) = v15) | ~ (set_union2(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (element(v17, v16) = v15) | ~ (element(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (in(v17, v16) = v15) | ~ (in(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (set_difference(v15, v16) = v17) | ~ (preboolean(v14) = 0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : (set_union2(v15, v16) = v20 & in(v20, v14) = v21 & in(v17, v14) = v22 & in(v16, v14) = v19 & in(v15, v14) = v18 & ( ~ (v19 = 0) | ~ (v18 = 0) | (v22 = 0 & v21 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v16) = 0) | (in(v17, v15) = 0 & in(v17, v14) = 0)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v15) = 0) | ? [v18] : ? [v19] : (in(v17, v16) = v19 & in(v17, v14) = v18 & ( ~ (v18 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (set_intersection2(v14, v15) = v16) | ~ (in(v17, v14) = 0) | ? [v18] : ? [v19] : (in(v17, v16) = v19 & in(v17, v15) = v18 & ( ~ (v18 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (set_union2(v15, v16) = v17) | ~ (preboolean(v14) = 0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : (set_difference(v15, v16) = v21 & in(v21, v14) = v22 & in(v17, v14) = v20 & in(v16, v14) = v19 & in(v15, v14) = v18 & ( ~ (v19 = 0) | ~ (v18 = 0) | (v22 = 0 & v20 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (in(v14, v15) = 0) | element(v14, v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (in(v14, v15) = 0) | ? [v18] : ( ~ (v18 = 0) & empty(v16) = v18)) & ? [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = v14 | ~ (set_intersection2(v15, v16) = v17) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (in(v18, v16) = v21 & in(v18, v15) = v20 & in(v18, v14) = v19 & ( ~ (v21 = 0) | ~ (v20 = 0) | ~ (v19 = 0)) & (v19 = 0 | (v21 = 0 & v20 = 0)))) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (subset(v14, v15) = v16) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v15) = v17 & element(v14, v17) = v18)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (element(v14, v15) = v16) | ? [v17] : ( ~ (v17 = 0) & in(v14, v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (in(v14, v15) = v16) | ? [v17] : ? [v18] : (element(v14, v15) = v17 & empty(v15) = v18 & ( ~ (v17 = 0) | v18 = 0))) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation(v16) = v15) | ~ (relation(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (function(v16) = v15) | ~ (function(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (one_to_one(v16) = v15) | ~ (one_to_one(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (epsilon_transitive(v16) = v15) | ~ (epsilon_transitive(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (epsilon_connected(v16) = v15) | ~ (epsilon_connected(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (ordinal(v16) = v15) | ~ (ordinal(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (natural(v16) = v15) | ~ (natural(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (cap_closed(v16) = v15) | ~ (cap_closed(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (powerset(v16) = v15) | ~ (powerset(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (preboolean(v16) = v15) | ~ (preboolean(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (cup_closed(v16) = v15) | ~ (cup_closed(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (diff_closed(v16) = v15) | ~ (diff_closed(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (empty(v16) = v15) | ~ (empty(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (finite(v16) = v15) | ~ (finite(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_difference(v14, v15) = v16) | ? [v17] : ? [v18] : (finite(v16) = v18 & finite(v14) = v17 & ( ~ (v17 = 0) | v18 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_intersection2(v15, v14) = v16) | set_intersection2(v14, v15) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_intersection2(v14, v15) = v16) | set_intersection2(v15, v14) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_intersection2(v14, v15) = v16) | ? [v17] : ? [v18] : (finite(v16) = v18 & finite(v15) = v17 & ( ~ (v17 = 0) | v18 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_intersection2(v14, v15) = v16) | ? [v17] : ? [v18] : (finite(v16) = v18 & finite(v14) = v17 & ( ~ (v17 = 0) | v18 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v15, v14) = v16) | set_union2(v14, v15) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v15, v14) = v16) | ? [v17] : ? [v18] : (empty(v16) = v18 & empty(v14) = v17 & ( ~ (v18 = 0) | v17 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v14, v15) = v16) | set_union2(v15, v14) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : (finite(v16) = v19 & finite(v15) = v18 & finite(v14) = v17 & ( ~ (v18 = 0) | ~ (v17 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v14, v15) = v16) | ? [v17] : ? [v18] : (empty(v16) = v18 & empty(v14) = v17 & ( ~ (v18 = 0) | v17 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (powerset(v15) = v16) | ~ (element(v14, v16) = 0) | subset(v14, v15) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (powerset(v14) = v15) | ~ (element(v16, v15) = 0) | ? [v17] : ((v17 = 0 & finite(v16) = 0) | ( ~ (v17 = 0) & finite(v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (empty(v16) = 0) | ~ (in(v14, v15) = 0) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v16) = v17 & element(v15, v17) = v18)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_difference(v14, empty_set) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_intersection2(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_union2(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_union2(v14, empty_set) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (empty(v15) = 0) | ~ (empty(v14) = 0)) & ! [v14] : ! [v15] : (v15 = empty_set | ~ (set_difference(empty_set, v14) = v15)) & ! [v14] : ! [v15] : (v15 = empty_set | ~ (set_intersection2(v14, empty_set) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (subset(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (preboolean(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : (set_difference(v16, v17) = v20 & set_union2(v16, v17) = v18 & in(v20, v14) = v21 & in(v18, v14) = v19 & in(v17, v14) = 0 & in(v16, v14) = 0 & ( ~ (v21 = 0) | ~ (v19 = 0)))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (preboolean(v14) = v15) | ? [v16] : ? [v17] : (cup_closed(v14) = v16 & diff_closed(v14) = v17 & ( ~ (v17 = 0) | ~ (v16 = 0)))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (empty(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v14) = v16 & element(v17, v16) = 0 & empty(v17) = v18 & finite(v17) = 0)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (empty(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v14) = v16 & element(v17, v16) = 0 & empty(v17) = v18)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (empty(v14) = v15) | ? [v16] : ? [v17] : (preboolean(v14) = v16 & in(empty_set, v14) = v17 & ( ~ (v16 = 0) | v17 = 0))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (finite(v14) = v15) | ? [v16] : ( ~ (v16 = 0) & empty(v14) = v16)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (in(empty_set, v14) = v15) | ? [v16] : ? [v17] : (preboolean(v14) = v17 & empty(v14) = v16 & ( ~ (v17 = 0) | v16 = 0))) & ! [v14] : ! [v15] : ( ~ (subset(v14, v15) = 0) | ? [v16] : (powerset(v15) = v16 & element(v14, v16) = 0)) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | preboolean(v15) = 0) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | cup_closed(v15) = 0) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | diff_closed(v15) = 0) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : ((v19 = 0 & v17 = 0 & ~ (v18 = 0) & element(v16, v15) = 0 & empty(v16) = v18 & finite(v16) = 0) | (v16 = 0 & empty(v14) = 0))) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & ~ (v18 = 0) & element(v16, v15) = 0 & empty(v16) = v18) | (v16 = 0 & empty(v14) = 0))) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ? [v16] : ( ~ (v16 = 0) & empty(v15) = v16)) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ? [v16] : (relation(v16) = 0 & function(v16) = 0 & one_to_one(v16) = 0 & epsilon_transitive(v16) = 0 & epsilon_connected(v16) = 0 & ordinal(v16) = 0 & natural(v16) = 0 & element(v16, v15) = 0 & empty(v16) = 0 & finite(v16) = 0)) & ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ? [v16] : (element(v16, v15) = 0 & empty(v16) = 0)) & ! [v14] : ! [v15] : ( ~ (element(v14, v15) = 0) | ? [v16] : ? [v17] : (empty(v15) = v16 & in(v14, v15) = v17 & (v17 = 0 | v16 = 0))) & ! [v14] : ! [v15] : ( ~ (cup_closed(v14) = v15) | ? [v16] : ? [v17] : (preboolean(v14) = v16 & diff_closed(v14) = v17 & ( ~ (v16 = 0) | (v17 = 0 & v15 = 0)))) & ! [v14] : ! [v15] : ( ~ (diff_closed(v14) = v15) | ? [v16] : ? [v17] : (preboolean(v14) = v16 & cup_closed(v14) = v17 & ( ~ (v16 = 0) | (v17 = 0 & v15 = 0)))) & ! [v14] : ! [v15] : ( ~ (in(v15, v14) = 0) | ? [v16] : ( ~ (v16 = 0) & in(v14, v15) = v16)) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | element(v14, v15) = 0) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & empty(v15) = v16)) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & in(v15, v14) = v16)) & ! [v14] : (v14 = empty_set | ~ (empty(v14) = 0)) & ! [v14] : ( ~ (preboolean(v14) = 0) | ? [v15] : ? [v16] : (empty(v14) = v15 & in(empty_set, v14) = v16 & (v16 = 0 | v15 = 0))) & ! [v14] : ( ~ (preboolean(v14) = 0) | (cup_closed(v14) = 0 & diff_closed(v14) = 0)) & ! [v14] : ( ~ (cup_closed(v14) = 0) | ? [v15] : ? [v16] : (preboolean(v14) = v16 & diff_closed(v14) = v15 & ( ~ (v15 = 0) | v16 = 0))) & ! [v14] : ( ~ (diff_closed(v14) = 0) | ? [v15] : ? [v16] : (preboolean(v14) = v16 & cup_closed(v14) = v15 & ( ~ (v15 = 0) | v16 = 0))) & ! [v14] : ( ~ (empty(v14) = 0) | finite(v14) = 0) & ! [v14] : ( ~ (finite(v14) = 0) | ? [v15] : (powerset(v14) = v15 & ! [v16] : ! [v17] : (v17 = 0 | ~ (finite(v16) = v17) | ? [v18] : ( ~ (v18 = 0) & element(v16, v15) = v18)) & ! [v16] : ( ~ (element(v16, v15) = 0) | finite(v16) = 0))) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : (powerset(v16) = v18 & element(v15, v18) = v19 & element(v14, v16) = v20 & in(v14, v15) = v17 & ( ~ (v19 = 0) | ~ (v17 = 0) | v20 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : (set_union2(v14, v15) = v18 & finite(v18) = v19 & finite(v15) = v17 & finite(v14) = v16 & ( ~ (v17 = 0) | ~ (v16 = 0) | v19 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (subset(v14, v15) = v16 & powerset(v15) = v17 & element(v14, v17) = v18 & ( ~ (v16 = 0) | v18 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (set_difference(v14, v15) = v17 & finite(v17) = v18 & finite(v14) = v16 & ( ~ (v16 = 0) | v18 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (set_intersection2(v14, v15) = v17 & finite(v17) = v18 & finite(v14) = v16 & ( ~ (v16 = 0) | v18 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : (preboolean(v14) = v17 & cup_closed(v14) = v15 & diff_closed(v14) = v16 & ( ~ (v16 = 0) | ~ (v15 = 0) | v17 = 0)) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : (empty(v15) = v17 & in(v14, v15) = v16 & ( ~ (v17 = 0) | ~ (v16 = 0))) & ? [v14] : ? [v15] : ? [v16] : (relation(v16) = 0 & function(v16) = 0 & one_to_one(v16) = 0 & epsilon_transitive(v16) = 0 & epsilon_connected(v16) = 0 & ordinal(v16) = 0 & natural(v16) = 0 & powerset(v14) = v15 & element(v16, v15) = 0 & empty(v16) = 0 & finite(v16) = 0) & ? [v14] : ? [v15] : element(v15, v14) = 0 & ( ~ (v6 = 0) | v5 = 0)) % 98.82/61.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, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 98.82/61.91 | (1) ~ (all_0_0_0 = 0) & ~ (all_0_2_2 = 0) & ~ (all_0_5_5 = 0) & ~ (all_0_10_10 = 0) & ~ (all_0_12_12 = 0) & cap_closed(all_0_3_3) = 0 & set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9 & preboolean(all_0_3_3) = 0 & preboolean(all_0_9_9) = all_0_7_7 & preboolean(all_0_11_11) = 0 & preboolean(all_0_13_13) = 0 & cup_closed(all_0_3_3) = 0 & diff_closed(all_0_3_3) = 0 & empty(all_0_1_1) = all_0_0_0 & empty(all_0_3_3) = all_0_2_2 & empty(all_0_4_4) = 0 & empty(all_0_6_6) = all_0_5_5 & empty(all_0_9_9) = all_0_8_8 & empty(all_0_11_11) = all_0_10_10 & empty(all_0_13_13) = all_0_12_12 & empty(empty_set) = 0 & finite(all_0_1_1) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ? [v5] : ? [v6] : (in(v3, v1) = v6 & in(v3, v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (element(v0, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ? [v6] : (in(v3, v2) = v5 & in(v3, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ? [v5] : ? [v6] : (in(v3, v2) = v5 & in(v3, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v0) = v1) | ~ (finite(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & element(v2, v1) = v4) | ( ~ (v4 = 0) & finite(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (element(v0, v2) = v3) | ~ (in(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v2) = v4 & element(v1, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(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 | ~ (set_intersection2(v3, v2) = v1) | ~ (set_intersection2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v1, v2) = v3) | ~ (preboolean(v0) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (set_union2(v1, v2) = v6 & in(v6, v0) = v7 & in(v3, v0) = v8 & in(v2, v0) = v5 & in(v1, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v8 = 0 & v7 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = 0) | (in(v3, v1) = 0 & in(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = 0) | ? [v4] : ? [v5] : (in(v3, v2) = v5 & in(v3, v0) = v4 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ? [v4] : ? [v5] : (in(v3, v2) = v5 & in(v3, v1) = v4 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_union2(v1, v2) = v3) | ~ (preboolean(v0) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (set_difference(v1, v2) = v7 & in(v7, v0) = v8 & in(v3, v0) = v6 & in(v2, v0) = v5 & in(v1, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v8 = 0 & v6 = 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] : ! [v3] : (v3 = v0 | ~ (set_intersection2(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (in(v4, v2) = v7 & in(v4, v1) = v6 & in(v4, v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0)) & (v5 = 0 | (v7 = 0 & v6 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (element(v0, v1) = v3 & empty(v1) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (function(v2) = v1) | ~ (function(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_transitive(v2) = v1) | ~ (epsilon_transitive(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_connected(v2) = v1) | ~ (epsilon_connected(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ordinal(v2) = v1) | ~ (ordinal(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (natural(v2) = v1) | ~ (natural(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cap_closed(v2) = v1) | ~ (cap_closed(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (preboolean(v2) = v1) | ~ (preboolean(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cup_closed(v2) = v1) | ~ (cup_closed(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (diff_closed(v2) = v1) | ~ (diff_closed(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (finite(v2) = v1) | ~ (finite(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_difference(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v1, v0) = v2) | set_intersection2(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | set_intersection2(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v1) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | set_union2(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | ? [v3] : ? [v4] : (empty(v2) = v4 & empty(v0) = v3 & ( ~ (v4 = 0) | v3 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | set_union2(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (finite(v2) = v5 & finite(v1) = v4 & finite(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ? [v4] : (empty(v2) = v4 & empty(v0) = v3 & ( ~ (v4 = 0) | v3 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v1) | ~ (element(v2, v1) = 0) | ? [v3] : ((v3 = 0 & finite(v2) = 0) | ( ~ (v3 = 0) & finite(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (empty(v2) = 0) | ~ (in(v0, v1) = 0) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v2) = v3 & element(v1, v3) = v4)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_difference(v0, empty_set) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_intersection2(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, empty_set) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) & ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_difference(empty_set, v0) = v1)) & ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_intersection2(v0, empty_set) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (preboolean(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (set_difference(v2, v3) = v6 & set_union2(v2, v3) = v4 & in(v6, v0) = v7 & in(v4, v0) = v5 & in(v3, v0) = 0 & in(v2, v0) = 0 & ( ~ (v7 = 0) | ~ (v5 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (preboolean(v0) = v1) | ? [v2] : ? [v3] : (cup_closed(v0) = v2 & diff_closed(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4 & finite(v3) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & in(empty_set, v0) = v3 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (in(empty_set, v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v3 & empty(v0) = v2 & ( ~ (v3 = 0) | v2 = 0))) & ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | preboolean(v1) = 0) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | cup_closed(v1) = 0) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | diff_closed(v1) = 0) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4 & finite(v2) = 0) | (v2 = 0 & empty(v0) = 0))) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4) | (v2 = 0 & empty(v0) = 0))) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (relation(v2) = 0 & function(v2) = 0 & one_to_one(v2) = 0 & epsilon_transitive(v2) = 0 & epsilon_connected(v2) = 0 & ordinal(v2) = 0 & natural(v2) = 0 & element(v2, v1) = 0 & empty(v2) = 0 & finite(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (element(v2, v1) = 0 & empty(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ? [v3] : (empty(v1) = v2 & in(v0, v1) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : ( ~ (cup_closed(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & diff_closed(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) & ! [v0] : ! [v1] : ( ~ (diff_closed(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & cup_closed(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) & ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) & ! [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] : ( ~ (preboolean(v0) = 0) | ? [v1] : ? [v2] : (empty(v0) = v1 & in(empty_set, v0) = v2 & (v2 = 0 | v1 = 0))) & ! [v0] : ( ~ (preboolean(v0) = 0) | (cup_closed(v0) = 0 & diff_closed(v0) = 0)) & ! [v0] : ( ~ (cup_closed(v0) = 0) | ? [v1] : ? [v2] : (preboolean(v0) = v2 & diff_closed(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) & ! [v0] : ( ~ (diff_closed(v0) = 0) | ? [v1] : ? [v2] : (preboolean(v0) = v2 & cup_closed(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) & ! [v0] : ( ~ (empty(v0) = 0) | finite(v0) = 0) & ! [v0] : ( ~ (finite(v0) = 0) | ? [v1] : (powerset(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (finite(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & element(v2, v1) = v4)) & ! [v2] : ( ~ (element(v2, v1) = 0) | finite(v2) = 0))) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (powerset(v2) = v4 & element(v1, v4) = v5 & element(v0, v2) = v6 & in(v0, v1) = v3 & ( ~ (v5 = 0) | ~ (v3 = 0) | v6 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (set_union2(v0, v1) = v4 & finite(v4) = v5 & finite(v1) = v3 & finite(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset(v0, v1) = v2 & powerset(v1) = v3 & element(v0, v3) = v4 & ( ~ (v2 = 0) | v4 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(v0, v1) = v3 & finite(v3) = v4 & finite(v0) = v2 & ( ~ (v2 = 0) | v4 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_intersection2(v0, v1) = v3 & finite(v3) = v4 & finite(v0) = v2 & ( ~ (v2 = 0) | v4 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : (preboolean(v0) = v3 & cup_closed(v0) = v1 & diff_closed(v0) = v2 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : (empty(v1) = v3 & in(v0, v1) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))) & ? [v0] : ? [v1] : ? [v2] : (relation(v2) = 0 & function(v2) = 0 & one_to_one(v2) = 0 & epsilon_transitive(v2) = 0 & epsilon_connected(v2) = 0 & ordinal(v2) = 0 & natural(v2) = 0 & powerset(v0) = v1 & element(v2, v1) = 0 & empty(v2) = 0 & finite(v2) = 0) & ? [v0] : ? [v1] : element(v1, v0) = 0 & ( ~ (all_0_7_7 = 0) | all_0_8_8 = 0) % 99.24/61.94 | % 99.24/61.94 | Applying alpha-rule on (1) yields: % 99.24/61.94 | (2) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4)) % 99.24/61.94 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (function(v2) = v1) | ~ (function(v2) = v0)) % 99.24/61.94 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ? [v5] : ? [v6] : (in(v3, v1) = v6 & in(v3, v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0)))) % 99.24/61.94 | (5) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (preboolean(v0) = v3 & cup_closed(v0) = v1 & diff_closed(v0) = v2 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0)) % 99.24/61.94 | (6) ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ? [v3] : (empty(v1) = v2 & in(v0, v1) = v3 & (v3 = 0 | v2 = 0))) % 99.24/61.94 | (7) empty(all_0_13_13) = all_0_12_12 % 99.24/61.94 | (8) ! [v0] : ( ~ (preboolean(v0) = 0) | (cup_closed(v0) = 0 & diff_closed(v0) = 0)) % 99.24/61.94 | (9) empty(all_0_3_3) = all_0_2_2 % 99.24/61.94 | (10) ? [v0] : ? [v1] : element(v1, v0) = 0 % 99.24/61.94 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = 0) | ? [v4] : ? [v5] : (in(v3, v2) = v5 & in(v3, v0) = v4 & ( ~ (v4 = 0) | v5 = 0))) % 99.24/61.94 | (12) ! [v0] : ( ~ (empty(v0) = 0) | finite(v0) = 0) % 99.24/61.94 | (13) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 99.24/61.94 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | set_intersection2(v1, v0) = v2) % 99.24/61.94 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v1, v0) = v2) | set_intersection2(v0, v1) = v2) % 99.24/61.94 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v0) = v1) | ~ (element(v2, v1) = 0) | ? [v3] : ((v3 = 0 & finite(v2) = 0) | ( ~ (v3 = 0) & finite(v0) = v3))) % 99.24/61.94 | (17) ! [v0] : ( ~ (finite(v0) = 0) | ? [v1] : (powerset(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (finite(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & element(v2, v1) = v4)) & ! [v2] : ( ~ (element(v2, v1) = 0) | finite(v2) = 0))) % 99.24/61.94 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = 0) | (in(v3, v1) = 0 & in(v3, v0) = 0)) % 99.24/61.94 | (19) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) % 99.24/61.94 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_transitive(v2) = v1) | ~ (epsilon_transitive(v2) = v0)) % 99.24/61.94 | (21) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4) | (v2 = 0 & empty(v0) = 0))) % 99.24/61.94 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cup_closed(v2) = v1) | ~ (cup_closed(v2) = v0)) % 99.24/61.94 | (23) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 99.24/61.94 | (24) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_connected(v2) = v1) | ~ (epsilon_connected(v2) = v0)) % 99.24/61.94 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (element(v0, v2) = v3) | ~ (in(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v2) = v4 & element(v1, v4) = v5)) % 99.24/61.94 | (26) ! [v0] : ( ~ (diff_closed(v0) = 0) | ? [v1] : ? [v2] : (preboolean(v0) = v2 & cup_closed(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 99.24/61.94 | (27) ! [v0] : ( ~ (cup_closed(v0) = 0) | ? [v1] : ? [v2] : (preboolean(v0) = v2 & diff_closed(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) % 99.24/61.95 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 99.24/61.95 | (29) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 99.24/61.95 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ? [v4] : ? [v5] : (in(v3, v2) = v5 & in(v3, v1) = v4 & ( ~ (v4 = 0) | v5 = 0))) % 99.24/61.95 | (31) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (powerset(v2) = v4 & element(v1, v4) = v5 & element(v0, v2) = v6 & in(v0, v1) = v3 & ( ~ (v5 = 0) | ~ (v3 = 0) | v6 = 0)) % 99.24/61.95 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (diff_closed(v2) = v1) | ~ (diff_closed(v2) = v0)) % 99.24/61.95 | (33) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_difference(v0, empty_set) = v1)) % 99.24/61.95 | (34) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (set_union2(v0, v1) = v4 & finite(v4) = v5 & finite(v1) = v3 & finite(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0)) % 99.24/61.95 | (35) ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_difference(empty_set, v0) = v1)) % 99.24/61.95 | (36) empty(all_0_11_11) = all_0_10_10 % 99.24/61.95 | (37) empty(all_0_4_4) = 0 % 99.24/61.95 | (38) ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) % 99.24/61.95 | (39) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | preboolean(v1) = 0) % 99.24/61.95 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 99.24/61.95 | (41) ~ (all_0_0_0 = 0) % 99.24/61.95 | (42) ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) % 99.24/61.95 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | ? [v3] : ? [v4] : (empty(v2) = v4 & empty(v0) = v3 & ( ~ (v4 = 0) | v3 = 0))) % 99.24/61.95 | (44) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4 & finite(v2) = 0) | (v2 = 0 & empty(v0) = 0))) % 99.24/61.95 | (45) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (subset(v0, v1) = v2 & powerset(v1) = v3 & element(v0, v3) = v4 & ( ~ (v2 = 0) | v4 = 0)) % 99.24/61.95 | (46) ! [v0] : ! [v1] : (v1 = empty_set | ~ (set_intersection2(v0, empty_set) = v1)) % 99.24/61.95 | (47) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | cup_closed(v1) = 0) % 99.24/61.95 | (48) ? [v0] : ? [v1] : ? [v2] : (relation(v2) = 0 & function(v2) = 0 & one_to_one(v2) = 0 & epsilon_transitive(v2) = 0 & epsilon_connected(v2) = 0 & ordinal(v2) = 0 & natural(v2) = 0 & powerset(v0) = v1 & element(v2, v1) = 0 & empty(v2) = 0 & finite(v2) = 0) % 99.24/61.95 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ (empty(v2) = 0) | ~ (in(v0, v1) = 0) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v2) = v3 & element(v1, v3) = v4)) % 99.24/61.95 | (50) preboolean(all_0_13_13) = 0 % 99.24/61.95 | (51) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(v0, v1) = v3 & finite(v3) = v4 & finite(v0) = v2 & ( ~ (v2 = 0) | v4 = 0)) % 99.24/61.95 | (52) cup_closed(all_0_3_3) = 0 % 99.24/61.95 | (53) empty(all_0_6_6) = all_0_5_5 % 99.24/61.95 | (54) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_difference(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 99.24/61.95 | (55) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 99.24/61.95 | (56) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) % 99.24/61.95 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_difference(v1, v2) = v3) | ~ (preboolean(v0) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (set_union2(v1, v2) = v6 & in(v6, v0) = v7 & in(v3, v0) = v8 & in(v2, v0) = v5 & in(v1, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v8 = 0 & v7 = 0)))) % 99.24/61.95 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ordinal(v2) = v1) | ~ (ordinal(v2) = v0)) % 99.24/61.95 | (59) preboolean(all_0_3_3) = 0 % 99.24/61.95 | (60) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_intersection2(v0, v1) = v3 & finite(v3) = v4 & finite(v0) = v2 & ( ~ (v2 = 0) | v4 = 0)) % 99.24/61.95 | (61) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) % 99.24/61.95 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v1) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 99.24/61.95 | (63) ! [v0] : ! [v1] : (v1 = 0 | ~ (in(empty_set, v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v3 & empty(v0) = v2 & ( ~ (v3 = 0) | v2 = 0))) % 99.24/61.96 | (64) ~ (all_0_5_5 = 0) % 99.24/61.96 | (65) ! [v0] : ! [v1] : (v1 = 0 | ~ (preboolean(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (set_difference(v2, v3) = v6 & set_union2(v2, v3) = v4 & in(v6, v0) = v7 & in(v4, v0) = v5 & in(v3, v0) = 0 & in(v2, v0) = 0 & ( ~ (v7 = 0) | ~ (v5 = 0)))) % 99.24/61.96 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ? [v5] : ? [v6] : (in(v3, v2) = v5 & in(v3, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v4 = 0)))) % 99.24/61.96 | (67) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (empty(v1) = v3 & in(v0, v1) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))) % 99.24/61.96 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) % 99.24/61.96 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v0) = v1) | ~ (finite(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & element(v2, v1) = v4) | ( ~ (v4 = 0) & finite(v0) = v4))) % 99.24/61.96 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 99.24/61.96 | (71) finite(all_0_1_1) = 0 % 99.24/61.96 | (72) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (finite(v2) = v5 & finite(v1) = v4 & finite(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 99.24/61.96 | (73) ~ (all_0_7_7 = 0) | all_0_8_8 = 0 % 99.24/61.96 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) % 99.24/61.96 | (75) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (element(v2, v1) = 0 & empty(v2) = 0)) % 99.24/61.96 | (76) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, empty_set) = v1)) % 99.24/61.96 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ? [v5] : ? [v6] : (in(v3, v2) = v5 & in(v3, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v4 = 0)))) % 99.24/61.96 | (78) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | diff_closed(v1) = 0) % 99.24/61.96 | (79) ! [v0] : ( ~ (preboolean(v0) = 0) | ? [v1] : ? [v2] : (empty(v0) = v1 & in(empty_set, v0) = v2 & (v2 = 0 | v1 = 0))) % 99.24/61.96 | (80) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) % 99.24/61.96 | (81) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) % 99.24/61.96 | (82) preboolean(all_0_11_11) = 0 % 99.24/61.96 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (set_union2(v1, v2) = v3) | ~ (preboolean(v0) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (set_difference(v1, v2) = v7 & in(v7, v0) = v8 & in(v3, v0) = v6 & in(v2, v0) = v5 & in(v1, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v8 = 0 & v6 = 0)))) % 99.24/61.96 | (84) ~ (all_0_12_12 = 0) % 99.24/61.96 | (85) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 99.24/61.96 | (86) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, v0) = v1)) % 99.24/61.96 | (87) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : (element(v0, v1) = v3 & empty(v1) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 99.24/61.96 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (preboolean(v2) = v1) | ~ (preboolean(v2) = v0)) % 99.24/61.96 | (89) ~ (all_0_2_2 = 0) % 99.24/61.96 | (90) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (relation(v2) = 0 & function(v2) = 0 & one_to_one(v2) = 0 & epsilon_transitive(v2) = 0 & epsilon_connected(v2) = 0 & ordinal(v2) = 0 & natural(v2) = 0 & element(v2, v1) = 0 & empty(v2) = 0 & finite(v2) = 0)) % 99.24/61.96 | (91) diff_closed(all_0_3_3) = 0 % 99.24/61.96 | (92) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4 & finite(v3) = 0)) % 99.24/61.96 | (93) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | set_union2(v1, v0) = v2) % 99.24/61.96 | (94) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | set_union2(v0, v1) = v2) % 99.24/61.96 | (95) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_intersection2(v0, v0) = v1)) % 99.24/61.96 | (96) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cap_closed(v2) = v1) | ~ (cap_closed(v2) = v0)) % 99.24/61.96 | (97) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 99.24/61.96 | (98) set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9 % 99.24/61.97 | (99) ! [v0] : ! [v1] : ( ~ (diff_closed(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & cup_closed(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) % 99.24/61.97 | (100) ! [v0] : ! [v1] : ( ~ (cup_closed(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & diff_closed(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) % 99.24/61.97 | (101) cap_closed(all_0_3_3) = 0 % 99.24/61.97 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 99.24/61.97 | (103) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (natural(v2) = v1) | ~ (natural(v2) = v0)) % 99.24/61.97 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) % 99.24/61.97 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) % 99.24/61.97 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_intersection2(v3, v2) = v1) | ~ (set_intersection2(v3, v2) = v0)) % 99.24/61.97 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (finite(v2) = v1) | ~ (finite(v2) = v0)) % 99.24/61.97 | (108) preboolean(all_0_9_9) = all_0_7_7 % 99.24/61.97 | (109) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (element(v0, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v0, v1) = v5)) % 99.24/61.97 | (110) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 99.24/61.97 | (111) empty(all_0_9_9) = all_0_8_8 % 99.24/61.97 | (112) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ? [v4] : (empty(v2) = v4 & empty(v0) = v3 & ( ~ (v4 = 0) | v3 = 0))) % 99.24/61.97 | (113) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) % 99.24/61.97 | (114) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_intersection2(v0, v1) = v2) | ? [v3] : ? [v4] : (finite(v2) = v4 & finite(v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 99.24/61.97 | (115) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) % 99.24/61.97 | (116) ~ (all_0_10_10 = 0) % 99.24/61.97 | (117) ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) % 99.24/61.97 | (118) empty(empty_set) = 0 % 99.24/61.97 | (119) ? [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (set_intersection2(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (in(v4, v2) = v7 & in(v4, v1) = v6 & in(v4, v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0)) & (v5 = 0 | (v7 = 0 & v6 = 0)))) % 99.24/61.97 | (120) ! [v0] : ! [v1] : (v1 = 0 | ~ (preboolean(v0) = v1) | ? [v2] : ? [v3] : (cup_closed(v0) = v2 & diff_closed(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 99.24/61.97 | (121) empty(all_0_1_1) = all_0_0_0 % 99.24/61.97 | (122) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (preboolean(v0) = v2 & in(empty_set, v0) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 99.24/61.97 | % 99.24/61.97 | Instantiating (48) with all_5_0_16, all_5_1_17, all_5_2_18 yields: % 99.24/61.97 | (123) relation(all_5_0_16) = 0 & function(all_5_0_16) = 0 & one_to_one(all_5_0_16) = 0 & epsilon_transitive(all_5_0_16) = 0 & epsilon_connected(all_5_0_16) = 0 & ordinal(all_5_0_16) = 0 & natural(all_5_0_16) = 0 & powerset(all_5_2_18) = all_5_1_17 & element(all_5_0_16, all_5_1_17) = 0 & empty(all_5_0_16) = 0 & finite(all_5_0_16) = 0 % 99.24/61.97 | % 99.24/61.97 | Applying alpha-rule on (123) yields: % 99.24/61.97 | (124) function(all_5_0_16) = 0 % 99.24/61.97 | (125) element(all_5_0_16, all_5_1_17) = 0 % 99.24/61.97 | (126) powerset(all_5_2_18) = all_5_1_17 % 99.24/61.97 | (127) epsilon_connected(all_5_0_16) = 0 % 99.24/61.97 | (128) ordinal(all_5_0_16) = 0 % 99.24/61.97 | (129) empty(all_5_0_16) = 0 % 99.24/61.97 | (130) natural(all_5_0_16) = 0 % 99.24/61.97 | (131) one_to_one(all_5_0_16) = 0 % 99.24/61.97 | (132) relation(all_5_0_16) = 0 % 99.24/61.97 | (133) epsilon_transitive(all_5_0_16) = 0 % 99.24/61.97 | (134) finite(all_5_0_16) = 0 % 99.24/61.97 | % 99.24/61.97 | Instantiating (45) with all_11_0_27, all_11_1_28, all_11_2_29, all_11_3_30, all_11_4_31 yields: % 99.24/61.97 | (135) subset(all_11_4_31, all_11_3_30) = all_11_2_29 & powerset(all_11_3_30) = all_11_1_28 & element(all_11_4_31, all_11_1_28) = all_11_0_27 & ( ~ (all_11_2_29 = 0) | all_11_0_27 = 0) % 99.24/61.97 | % 99.24/61.97 | Applying alpha-rule on (135) yields: % 99.24/61.97 | (136) subset(all_11_4_31, all_11_3_30) = all_11_2_29 % 99.24/61.97 | (137) powerset(all_11_3_30) = all_11_1_28 % 99.24/61.97 | (138) element(all_11_4_31, all_11_1_28) = all_11_0_27 % 99.24/61.97 | (139) ~ (all_11_2_29 = 0) | all_11_0_27 = 0 % 99.24/61.97 | % 99.24/61.97 | Instantiating (31) with all_15_0_38, all_15_1_39, all_15_2_40, all_15_3_41, all_15_4_42, all_15_5_43, all_15_6_44 yields: % 99.24/61.97 | (140) powerset(all_15_4_42) = all_15_2_40 & element(all_15_5_43, all_15_2_40) = all_15_1_39 & element(all_15_6_44, all_15_4_42) = all_15_0_38 & in(all_15_6_44, all_15_5_43) = all_15_3_41 & ( ~ (all_15_1_39 = 0) | ~ (all_15_3_41 = 0) | all_15_0_38 = 0) % 99.24/61.97 | % 99.24/61.97 | Applying alpha-rule on (140) yields: % 99.24/61.97 | (141) in(all_15_6_44, all_15_5_43) = all_15_3_41 % 99.24/61.97 | (142) powerset(all_15_4_42) = all_15_2_40 % 99.24/61.98 | (143) element(all_15_6_44, all_15_4_42) = all_15_0_38 % 99.24/61.98 | (144) ~ (all_15_1_39 = 0) | ~ (all_15_3_41 = 0) | all_15_0_38 = 0 % 99.24/61.98 | (145) element(all_15_5_43, all_15_2_40) = all_15_1_39 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (97) with all_0_4_4, all_5_0_16 and discharging atoms empty(all_5_0_16) = 0, empty(all_0_4_4) = 0, yields: % 99.24/61.98 | (146) all_5_0_16 = all_0_4_4 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (97) with empty_set, all_5_0_16 and discharging atoms empty(all_5_0_16) = 0, empty(empty_set) = 0, yields: % 99.24/61.98 | (147) all_5_0_16 = empty_set % 99.24/61.98 | % 99.24/61.98 | Combining equations (147,146) yields a new equation: % 99.24/61.98 | (148) all_0_4_4 = empty_set % 99.24/61.98 | % 99.24/61.98 | Combining equations (148,146) yields a new equation: % 99.24/61.98 | (147) all_5_0_16 = empty_set % 99.24/61.98 | % 99.24/61.98 | From (147) and (134) follows: % 99.24/61.98 | (150) finite(empty_set) = 0 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (15) with all_0_9_9, all_0_13_13, all_0_11_11 and discharging atoms set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9, yields: % 99.24/61.98 | (151) set_intersection2(all_0_11_11, all_0_13_13) = all_0_9_9 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (39) with all_15_2_40, all_15_4_42 and discharging atoms powerset(all_15_4_42) = all_15_2_40, yields: % 99.24/61.98 | (152) preboolean(all_15_2_40) = 0 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (85) with all_15_2_40, all_15_4_42 and discharging atoms powerset(all_15_4_42) = all_15_2_40, yields: % 99.24/61.98 | (153) ? [v0] : ( ~ (v0 = 0) & empty(all_15_2_40) = v0) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (39) with all_11_1_28, all_11_3_30 and discharging atoms powerset(all_11_3_30) = all_11_1_28, yields: % 99.24/61.98 | (154) preboolean(all_11_1_28) = 0 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (85) with all_11_1_28, all_11_3_30 and discharging atoms powerset(all_11_3_30) = all_11_1_28, yields: % 99.24/61.98 | (155) ? [v0] : ( ~ (v0 = 0) & empty(all_11_1_28) = v0) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (39) with all_5_1_17, all_5_2_18 and discharging atoms powerset(all_5_2_18) = all_5_1_17, yields: % 99.24/61.98 | (156) preboolean(all_5_1_17) = 0 % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (65) with all_0_7_7, all_0_9_9 and discharging atoms preboolean(all_0_9_9) = all_0_7_7, yields: % 99.24/61.98 | (157) all_0_7_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (set_difference(v0, v1) = v4 & set_union2(v0, v1) = v2 & in(v4, all_0_9_9) = v5 & in(v2, all_0_9_9) = v3 & in(v1, all_0_9_9) = 0 & in(v0, all_0_9_9) = 0 & ( ~ (v5 = 0) | ~ (v3 = 0))) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (79) with all_0_11_11 and discharging atoms preboolean(all_0_11_11) = 0, yields: % 99.24/61.98 | (158) ? [v0] : ? [v1] : (empty(all_0_11_11) = v0 & in(empty_set, all_0_11_11) = v1 & (v1 = 0 | v0 = 0)) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (79) with all_0_13_13 and discharging atoms preboolean(all_0_13_13) = 0, yields: % 99.24/61.98 | (159) ? [v0] : ? [v1] : (empty(all_0_13_13) = v0 & in(empty_set, all_0_13_13) = v1 & (v1 = 0 | v0 = 0)) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (92) with all_0_0_0, all_0_1_1 and discharging atoms empty(all_0_1_1) = all_0_0_0, yields: % 99.24/61.98 | (160) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_1_1) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (2) with all_0_0_0, all_0_1_1 and discharging atoms empty(all_0_1_1) = all_0_0_0, yields: % 99.24/61.98 | (161) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_1_1) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (122) with all_0_0_0, all_0_1_1 and discharging atoms empty(all_0_1_1) = all_0_0_0, yields: % 99.24/61.98 | (162) all_0_0_0 = 0 | ? [v0] : ? [v1] : (preboolean(all_0_1_1) = v0 & in(empty_set, all_0_1_1) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (92) with all_0_2_2, all_0_3_3 and discharging atoms empty(all_0_3_3) = all_0_2_2, yields: % 99.24/61.98 | (163) all_0_2_2 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_3_3) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (2) with all_0_2_2, all_0_3_3 and discharging atoms empty(all_0_3_3) = all_0_2_2, yields: % 99.24/61.98 | (164) all_0_2_2 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_3_3) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (122) with all_0_2_2, all_0_3_3 and discharging atoms empty(all_0_3_3) = all_0_2_2, yields: % 99.24/61.98 | (165) all_0_2_2 = 0 | ? [v0] : ? [v1] : (preboolean(all_0_3_3) = v0 & in(empty_set, all_0_3_3) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (92) with all_0_5_5, all_0_6_6 and discharging atoms empty(all_0_6_6) = all_0_5_5, yields: % 99.24/61.98 | (166) all_0_5_5 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_6_6) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (2) with all_0_5_5, all_0_6_6 and discharging atoms empty(all_0_6_6) = all_0_5_5, yields: % 99.24/61.98 | (167) all_0_5_5 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_6_6) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (122) with all_0_5_5, all_0_6_6 and discharging atoms empty(all_0_6_6) = all_0_5_5, yields: % 99.24/61.98 | (168) all_0_5_5 = 0 | ? [v0] : ? [v1] : (preboolean(all_0_6_6) = v0 & in(empty_set, all_0_6_6) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.98 | % 99.24/61.98 | Instantiating formula (92) with all_0_10_10, all_0_11_11 and discharging atoms empty(all_0_11_11) = all_0_10_10, yields: % 99.24/61.99 | (169) all_0_10_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_11_11) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (2) with all_0_10_10, all_0_11_11 and discharging atoms empty(all_0_11_11) = all_0_10_10, yields: % 99.24/61.99 | (170) all_0_10_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_11_11) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (122) with all_0_10_10, all_0_11_11 and discharging atoms empty(all_0_11_11) = all_0_10_10, yields: % 99.24/61.99 | (171) all_0_10_10 = 0 | ? [v0] : ? [v1] : (preboolean(all_0_11_11) = v0 & in(empty_set, all_0_11_11) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (92) with all_0_12_12, all_0_13_13 and discharging atoms empty(all_0_13_13) = all_0_12_12, yields: % 99.24/61.99 | (172) all_0_12_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_13_13) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (2) with all_0_12_12, all_0_13_13 and discharging atoms empty(all_0_13_13) = all_0_12_12, yields: % 99.24/61.99 | (173) all_0_12_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_13_13) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (122) with all_0_12_12, all_0_13_13 and discharging atoms empty(all_0_13_13) = all_0_12_12, yields: % 99.24/61.99 | (174) all_0_12_12 = 0 | ? [v0] : ? [v1] : (preboolean(all_0_13_13) = v0 & in(empty_set, all_0_13_13) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (17) with all_0_1_1 and discharging atoms finite(all_0_1_1) = 0, yields: % 99.24/61.99 | (175) ? [v0] : (powerset(all_0_1_1) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (finite(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & element(v1, v0) = v3)) & ! [v1] : ( ~ (element(v1, v0) = 0) | finite(v1) = 0)) % 99.24/61.99 | % 99.24/61.99 | Instantiating formula (17) with empty_set and discharging atoms finite(empty_set) = 0, yields: % 99.24/61.99 | (176) ? [v0] : (powerset(empty_set) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (finite(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & element(v1, v0) = v3)) & ! [v1] : ( ~ (element(v1, v0) = 0) | finite(v1) = 0)) % 99.24/61.99 | % 99.24/61.99 | Instantiating (176) with all_38_0_70 yields: % 99.24/61.99 | (177) powerset(empty_set) = all_38_0_70 & ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & element(v0, all_38_0_70) = v2)) & ! [v0] : ( ~ (element(v0, all_38_0_70) = 0) | finite(v0) = 0) % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (177) yields: % 99.24/61.99 | (178) powerset(empty_set) = all_38_0_70 % 99.24/61.99 | (179) ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & element(v0, all_38_0_70) = v2)) % 99.24/61.99 | (180) ! [v0] : ( ~ (element(v0, all_38_0_70) = 0) | finite(v0) = 0) % 99.24/61.99 | % 99.24/61.99 | Instantiating (155) with all_41_0_71 yields: % 99.24/61.99 | (181) ~ (all_41_0_71 = 0) & empty(all_11_1_28) = all_41_0_71 % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (181) yields: % 99.24/61.99 | (182) ~ (all_41_0_71 = 0) % 99.24/61.99 | (183) empty(all_11_1_28) = all_41_0_71 % 99.24/61.99 | % 99.24/61.99 | Instantiating (159) with all_43_0_72, all_43_1_73 yields: % 99.24/61.99 | (184) empty(all_0_13_13) = all_43_1_73 & in(empty_set, all_0_13_13) = all_43_0_72 & (all_43_0_72 = 0 | all_43_1_73 = 0) % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (184) yields: % 99.24/61.99 | (185) empty(all_0_13_13) = all_43_1_73 % 99.24/61.99 | (186) in(empty_set, all_0_13_13) = all_43_0_72 % 99.24/61.99 | (187) all_43_0_72 = 0 | all_43_1_73 = 0 % 99.24/61.99 | % 99.24/61.99 | Instantiating (158) with all_45_0_74, all_45_1_75 yields: % 99.24/61.99 | (188) empty(all_0_11_11) = all_45_1_75 & in(empty_set, all_0_11_11) = all_45_0_74 & (all_45_0_74 = 0 | all_45_1_75 = 0) % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (188) yields: % 99.24/61.99 | (189) empty(all_0_11_11) = all_45_1_75 % 99.24/61.99 | (190) in(empty_set, all_0_11_11) = all_45_0_74 % 99.24/61.99 | (191) all_45_0_74 = 0 | all_45_1_75 = 0 % 99.24/61.99 | % 99.24/61.99 | Instantiating (175) with all_88_0_133 yields: % 99.24/61.99 | (192) powerset(all_0_1_1) = all_88_0_133 & ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & element(v0, all_88_0_133) = v2)) & ! [v0] : ( ~ (element(v0, all_88_0_133) = 0) | finite(v0) = 0) % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (192) yields: % 99.24/61.99 | (193) powerset(all_0_1_1) = all_88_0_133 % 99.24/61.99 | (194) ! [v0] : ! [v1] : (v1 = 0 | ~ (finite(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & element(v0, all_88_0_133) = v2)) % 99.24/61.99 | (195) ! [v0] : ( ~ (element(v0, all_88_0_133) = 0) | finite(v0) = 0) % 99.24/61.99 | % 99.24/61.99 | Instantiating (153) with all_95_0_138 yields: % 99.24/61.99 | (196) ~ (all_95_0_138 = 0) & empty(all_15_2_40) = all_95_0_138 % 99.24/61.99 | % 99.24/61.99 | Applying alpha-rule on (196) yields: % 99.24/61.99 | (197) ~ (all_95_0_138 = 0) % 99.24/61.99 | (198) empty(all_15_2_40) = all_95_0_138 % 99.24/61.99 | % 99.24/61.99 +-Applying beta-rule and splitting (174), into two cases. % 99.24/61.99 |-Branch one: % 99.24/61.99 | (199) all_0_12_12 = 0 % 99.24/61.99 | % 99.24/61.99 | Equations (199) can reduce 84 to: % 99.24/61.99 | (200) $false % 99.24/61.99 | % 99.24/61.99 |-The branch is then unsatisfiable % 99.24/61.99 |-Branch two: % 99.24/61.99 | (84) ~ (all_0_12_12 = 0) % 99.24/61.99 | (202) ? [v0] : ? [v1] : (preboolean(all_0_13_13) = v0 & in(empty_set, all_0_13_13) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/61.99 | % 99.24/62.00 | Instantiating (202) with all_110_0_150, all_110_1_151 yields: % 99.24/62.00 | (203) preboolean(all_0_13_13) = all_110_1_151 & in(empty_set, all_0_13_13) = all_110_0_150 & ( ~ (all_110_1_151 = 0) | all_110_0_150 = 0) % 99.24/62.00 | % 99.24/62.00 | Applying alpha-rule on (203) yields: % 99.24/62.00 | (204) preboolean(all_0_13_13) = all_110_1_151 % 99.24/62.00 | (205) in(empty_set, all_0_13_13) = all_110_0_150 % 99.24/62.00 | (206) ~ (all_110_1_151 = 0) | all_110_0_150 = 0 % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (171), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (207) all_0_10_10 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (207) can reduce 116 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (116) ~ (all_0_10_10 = 0) % 99.24/62.00 | (210) ? [v0] : ? [v1] : (preboolean(all_0_11_11) = v0 & in(empty_set, all_0_11_11) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/62.00 | % 99.24/62.00 | Instantiating (210) with all_116_0_152, all_116_1_153 yields: % 99.24/62.00 | (211) preboolean(all_0_11_11) = all_116_1_153 & in(empty_set, all_0_11_11) = all_116_0_152 & ( ~ (all_116_1_153 = 0) | all_116_0_152 = 0) % 99.24/62.00 | % 99.24/62.00 | Applying alpha-rule on (211) yields: % 99.24/62.00 | (212) preboolean(all_0_11_11) = all_116_1_153 % 99.24/62.00 | (213) in(empty_set, all_0_11_11) = all_116_0_152 % 99.24/62.00 | (214) ~ (all_116_1_153 = 0) | all_116_0_152 = 0 % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (165), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (215) all_0_2_2 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (215) can reduce 89 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (89) ~ (all_0_2_2 = 0) % 99.24/62.00 | (218) ? [v0] : ? [v1] : (preboolean(all_0_3_3) = v0 & in(empty_set, all_0_3_3) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/62.00 | % 99.24/62.00 | Instantiating (218) with all_122_0_154, all_122_1_155 yields: % 99.24/62.00 | (219) preboolean(all_0_3_3) = all_122_1_155 & in(empty_set, all_0_3_3) = all_122_0_154 & ( ~ (all_122_1_155 = 0) | all_122_0_154 = 0) % 99.24/62.00 | % 99.24/62.00 | Applying alpha-rule on (219) yields: % 99.24/62.00 | (220) preboolean(all_0_3_3) = all_122_1_155 % 99.24/62.00 | (221) in(empty_set, all_0_3_3) = all_122_0_154 % 99.24/62.00 | (222) ~ (all_122_1_155 = 0) | all_122_0_154 = 0 % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (168), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (223) all_0_5_5 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (223) can reduce 64 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (64) ~ (all_0_5_5 = 0) % 99.24/62.00 | (226) ? [v0] : ? [v1] : (preboolean(all_0_6_6) = v0 & in(empty_set, all_0_6_6) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (162), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (227) all_0_0_0 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (227) can reduce 41 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (41) ~ (all_0_0_0 = 0) % 99.24/62.00 | (230) ? [v0] : ? [v1] : (preboolean(all_0_1_1) = v0 & in(empty_set, all_0_1_1) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (170), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (207) all_0_10_10 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (207) can reduce 116 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (116) ~ (all_0_10_10 = 0) % 99.24/62.00 | (234) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_11_11) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.24/62.00 | % 99.24/62.00 | Instantiating (234) with all_137_0_160, all_137_1_161, all_137_2_162 yields: % 99.24/62.00 | (235) ~ (all_137_0_160 = 0) & powerset(all_0_11_11) = all_137_2_162 & element(all_137_1_161, all_137_2_162) = 0 & empty(all_137_1_161) = all_137_0_160 % 99.24/62.00 | % 99.24/62.00 | Applying alpha-rule on (235) yields: % 99.24/62.00 | (236) ~ (all_137_0_160 = 0) % 99.24/62.00 | (237) powerset(all_0_11_11) = all_137_2_162 % 99.24/62.00 | (238) element(all_137_1_161, all_137_2_162) = 0 % 99.24/62.00 | (239) empty(all_137_1_161) = all_137_0_160 % 99.24/62.00 | % 99.24/62.00 +-Applying beta-rule and splitting (160), into two cases. % 99.24/62.00 |-Branch one: % 99.24/62.00 | (227) all_0_0_0 = 0 % 99.24/62.00 | % 99.24/62.00 | Equations (227) can reduce 41 to: % 99.24/62.00 | (200) $false % 99.24/62.00 | % 99.24/62.00 |-The branch is then unsatisfiable % 99.24/62.00 |-Branch two: % 99.24/62.00 | (41) ~ (all_0_0_0 = 0) % 99.24/62.00 | (243) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_1_1) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.24/62.00 | % 99.24/62.00 | Instantiating (243) with all_142_0_163, all_142_1_164, all_142_2_165 yields: % 99.24/62.00 | (244) ~ (all_142_0_163 = 0) & powerset(all_0_1_1) = all_142_2_165 & element(all_142_1_164, all_142_2_165) = 0 & empty(all_142_1_164) = all_142_0_163 & finite(all_142_1_164) = 0 % 99.24/62.00 | % 99.24/62.00 | Applying alpha-rule on (244) yields: % 99.24/62.00 | (245) powerset(all_0_1_1) = all_142_2_165 % 99.24/62.00 | (246) empty(all_142_1_164) = all_142_0_163 % 99.24/62.00 | (247) ~ (all_142_0_163 = 0) % 99.24/62.00 | (248) finite(all_142_1_164) = 0 % 99.24/62.00 | (249) element(all_142_1_164, all_142_2_165) = 0 % 99.65/62.00 | % 99.65/62.00 +-Applying beta-rule and splitting (161), into two cases. % 99.65/62.00 |-Branch one: % 99.65/62.00 | (227) all_0_0_0 = 0 % 99.65/62.00 | % 99.65/62.00 | Equations (227) can reduce 41 to: % 99.65/62.00 | (200) $false % 99.65/62.00 | % 99.65/62.00 |-The branch is then unsatisfiable % 99.65/62.00 |-Branch two: % 99.65/62.00 | (41) ~ (all_0_0_0 = 0) % 99.65/62.00 | (253) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_1_1) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.65/62.01 | % 99.65/62.01 | Instantiating (253) with all_147_0_166, all_147_1_167, all_147_2_168 yields: % 99.65/62.01 | (254) ~ (all_147_0_166 = 0) & powerset(all_0_1_1) = all_147_2_168 & element(all_147_1_167, all_147_2_168) = 0 & empty(all_147_1_167) = all_147_0_166 % 99.65/62.01 | % 99.65/62.01 | Applying alpha-rule on (254) yields: % 99.65/62.01 | (255) ~ (all_147_0_166 = 0) % 99.65/62.01 | (256) powerset(all_0_1_1) = all_147_2_168 % 99.65/62.01 | (257) element(all_147_1_167, all_147_2_168) = 0 % 99.65/62.01 | (258) empty(all_147_1_167) = all_147_0_166 % 99.65/62.01 | % 99.65/62.01 +-Applying beta-rule and splitting (172), into two cases. % 99.65/62.01 |-Branch one: % 99.65/62.01 | (199) all_0_12_12 = 0 % 99.65/62.01 | % 99.65/62.01 | Equations (199) can reduce 84 to: % 99.65/62.01 | (200) $false % 99.65/62.01 | % 99.65/62.01 |-The branch is then unsatisfiable % 99.65/62.01 |-Branch two: % 99.65/62.01 | (84) ~ (all_0_12_12 = 0) % 99.65/62.01 | (262) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_13_13) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.65/62.01 | % 99.65/62.01 | Instantiating (262) with all_152_0_169, all_152_1_170, all_152_2_171 yields: % 99.65/62.01 | (263) ~ (all_152_0_169 = 0) & powerset(all_0_13_13) = all_152_2_171 & element(all_152_1_170, all_152_2_171) = 0 & empty(all_152_1_170) = all_152_0_169 & finite(all_152_1_170) = 0 % 99.65/62.01 | % 99.65/62.01 | Applying alpha-rule on (263) yields: % 99.65/62.01 | (264) finite(all_152_1_170) = 0 % 99.65/62.01 | (265) powerset(all_0_13_13) = all_152_2_171 % 99.65/62.01 | (266) empty(all_152_1_170) = all_152_0_169 % 99.65/62.01 | (267) element(all_152_1_170, all_152_2_171) = 0 % 99.65/62.01 | (268) ~ (all_152_0_169 = 0) % 99.65/62.01 | % 99.65/62.01 +-Applying beta-rule and splitting (173), into two cases. % 99.65/62.01 |-Branch one: % 99.65/62.01 | (199) all_0_12_12 = 0 % 99.65/62.01 | % 99.65/62.01 | Equations (199) can reduce 84 to: % 99.65/62.01 | (200) $false % 99.65/62.01 | % 99.65/62.01 |-The branch is then unsatisfiable % 99.65/62.01 |-Branch two: % 99.65/62.01 | (84) ~ (all_0_12_12 = 0) % 99.65/62.01 | (272) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_13_13) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.65/62.01 | % 99.65/62.01 | Instantiating (272) with all_157_0_172, all_157_1_173, all_157_2_174 yields: % 99.65/62.01 | (273) ~ (all_157_0_172 = 0) & powerset(all_0_13_13) = all_157_2_174 & element(all_157_1_173, all_157_2_174) = 0 & empty(all_157_1_173) = all_157_0_172 % 99.65/62.01 | % 99.65/62.01 | Applying alpha-rule on (273) yields: % 99.65/62.01 | (274) ~ (all_157_0_172 = 0) % 99.65/62.01 | (275) powerset(all_0_13_13) = all_157_2_174 % 99.65/62.01 | (276) element(all_157_1_173, all_157_2_174) = 0 % 99.65/62.01 | (277) empty(all_157_1_173) = all_157_0_172 % 99.65/62.01 | % 99.65/62.01 +-Applying beta-rule and splitting (163), into two cases. % 99.65/62.01 |-Branch one: % 99.65/62.01 | (215) all_0_2_2 = 0 % 99.65/62.01 | % 99.65/62.01 | Equations (215) can reduce 89 to: % 99.65/62.01 | (200) $false % 99.65/62.01 | % 99.65/62.01 |-The branch is then unsatisfiable % 99.65/62.01 |-Branch two: % 99.65/62.01 | (89) ~ (all_0_2_2 = 0) % 99.65/62.01 | (281) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_3_3) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.65/62.01 | % 99.65/62.01 | Instantiating (281) with all_162_0_175, all_162_1_176, all_162_2_177 yields: % 99.65/62.01 | (282) ~ (all_162_0_175 = 0) & powerset(all_0_3_3) = all_162_2_177 & element(all_162_1_176, all_162_2_177) = 0 & empty(all_162_1_176) = all_162_0_175 & finite(all_162_1_176) = 0 % 99.65/62.01 | % 99.65/62.01 | Applying alpha-rule on (282) yields: % 99.65/62.01 | (283) element(all_162_1_176, all_162_2_177) = 0 % 99.65/62.01 | (284) ~ (all_162_0_175 = 0) % 99.65/62.01 | (285) empty(all_162_1_176) = all_162_0_175 % 99.65/62.01 | (286) finite(all_162_1_176) = 0 % 99.65/62.01 | (287) powerset(all_0_3_3) = all_162_2_177 % 99.65/62.01 | % 99.65/62.01 +-Applying beta-rule and splitting (164), into two cases. % 99.65/62.01 |-Branch one: % 99.65/62.01 | (215) all_0_2_2 = 0 % 99.65/62.01 | % 99.65/62.01 | Equations (215) can reduce 89 to: % 99.65/62.01 | (200) $false % 99.65/62.01 | % 99.65/62.01 |-The branch is then unsatisfiable % 99.65/62.01 |-Branch two: % 99.65/62.01 | (89) ~ (all_0_2_2 = 0) % 99.65/62.01 | (291) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_3_3) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.65/62.01 | % 99.65/62.01 | Instantiating (291) with all_167_0_178, all_167_1_179, all_167_2_180 yields: % 99.65/62.01 | (292) ~ (all_167_0_178 = 0) & powerset(all_0_3_3) = all_167_2_180 & element(all_167_1_179, all_167_2_180) = 0 & empty(all_167_1_179) = all_167_0_178 % 99.65/62.01 | % 99.65/62.01 | Applying alpha-rule on (292) yields: % 99.65/62.01 | (293) ~ (all_167_0_178 = 0) % 99.65/62.01 | (294) powerset(all_0_3_3) = all_167_2_180 % 99.65/62.01 | (295) element(all_167_1_179, all_167_2_180) = 0 % 99.65/62.01 | (296) empty(all_167_1_179) = all_167_0_178 % 99.65/62.01 | % 99.65/62.01 +-Applying beta-rule and splitting (167), into two cases. % 99.65/62.01 |-Branch one: % 99.65/62.01 | (223) all_0_5_5 = 0 % 99.65/62.01 | % 99.65/62.01 | Equations (223) can reduce 64 to: % 99.65/62.01 | (200) $false % 99.65/62.01 | % 99.65/62.01 |-The branch is then unsatisfiable % 99.65/62.01 |-Branch two: % 99.65/62.01 | (64) ~ (all_0_5_5 = 0) % 99.65/62.01 | (300) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_6_6) = v0 & element(v1, v0) = 0 & empty(v1) = v2) % 99.65/62.01 | % 99.65/62.01 | Instantiating (300) with all_173_0_181, all_173_1_182, all_173_2_183 yields: % 99.65/62.01 | (301) ~ (all_173_0_181 = 0) & powerset(all_0_6_6) = all_173_2_183 & element(all_173_1_182, all_173_2_183) = 0 & empty(all_173_1_182) = all_173_0_181 % 99.65/62.02 | % 99.65/62.02 | Applying alpha-rule on (301) yields: % 99.65/62.02 | (302) ~ (all_173_0_181 = 0) % 99.65/62.02 | (303) powerset(all_0_6_6) = all_173_2_183 % 99.65/62.02 | (304) element(all_173_1_182, all_173_2_183) = 0 % 99.65/62.02 | (305) empty(all_173_1_182) = all_173_0_181 % 99.65/62.02 | % 99.65/62.02 +-Applying beta-rule and splitting (169), into two cases. % 99.65/62.02 |-Branch one: % 99.65/62.02 | (207) all_0_10_10 = 0 % 99.65/62.02 | % 99.65/62.02 | Equations (207) can reduce 116 to: % 99.65/62.02 | (200) $false % 99.65/62.02 | % 99.65/62.02 |-The branch is then unsatisfiable % 99.65/62.02 |-Branch two: % 99.65/62.02 | (116) ~ (all_0_10_10 = 0) % 99.65/62.02 | (309) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_11_11) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.65/62.02 | % 99.65/62.02 | Instantiating (309) with all_178_0_184, all_178_1_185, all_178_2_186 yields: % 99.65/62.02 | (310) ~ (all_178_0_184 = 0) & powerset(all_0_11_11) = all_178_2_186 & element(all_178_1_185, all_178_2_186) = 0 & empty(all_178_1_185) = all_178_0_184 & finite(all_178_1_185) = 0 % 99.65/62.02 | % 99.65/62.02 | Applying alpha-rule on (310) yields: % 99.65/62.02 | (311) finite(all_178_1_185) = 0 % 99.65/62.02 | (312) element(all_178_1_185, all_178_2_186) = 0 % 99.65/62.02 | (313) empty(all_178_1_185) = all_178_0_184 % 99.65/62.02 | (314) ~ (all_178_0_184 = 0) % 99.65/62.02 | (315) powerset(all_0_11_11) = all_178_2_186 % 99.65/62.02 | % 99.65/62.02 +-Applying beta-rule and splitting (166), into two cases. % 99.65/62.02 |-Branch one: % 99.65/62.02 | (223) all_0_5_5 = 0 % 99.65/62.02 | % 99.65/62.02 | Equations (223) can reduce 64 to: % 99.65/62.02 | (200) $false % 99.65/62.02 | % 99.65/62.02 |-The branch is then unsatisfiable % 99.65/62.02 |-Branch two: % 99.65/62.02 | (64) ~ (all_0_5_5 = 0) % 99.65/62.02 | (319) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & powerset(all_0_6_6) = v0 & element(v1, v0) = 0 & empty(v1) = v2 & finite(v1) = 0) % 99.65/62.02 | % 99.65/62.02 | Instantiating (319) with all_183_0_187, all_183_1_188, all_183_2_189 yields: % 99.65/62.02 | (320) ~ (all_183_0_187 = 0) & powerset(all_0_6_6) = all_183_2_189 & element(all_183_1_188, all_183_2_189) = 0 & empty(all_183_1_188) = all_183_0_187 & finite(all_183_1_188) = 0 % 99.65/62.02 | % 99.65/62.02 | Applying alpha-rule on (320) yields: % 99.65/62.02 | (321) empty(all_183_1_188) = all_183_0_187 % 99.65/62.02 | (322) ~ (all_183_0_187 = 0) % 99.65/62.02 | (323) finite(all_183_1_188) = 0 % 99.65/62.02 | (324) powerset(all_0_6_6) = all_183_2_189 % 99.65/62.02 | (325) element(all_183_1_188, all_183_2_189) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_1_1, all_142_2_165, all_147_2_168 and discharging atoms powerset(all_0_1_1) = all_147_2_168, powerset(all_0_1_1) = all_142_2_165, yields: % 99.65/62.02 | (326) all_147_2_168 = all_142_2_165 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_1_1, all_88_0_133, all_147_2_168 and discharging atoms powerset(all_0_1_1) = all_147_2_168, powerset(all_0_1_1) = all_88_0_133, yields: % 99.65/62.02 | (327) all_147_2_168 = all_88_0_133 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_3_3, all_162_2_177, all_167_2_180 and discharging atoms powerset(all_0_3_3) = all_167_2_180, powerset(all_0_3_3) = all_162_2_177, yields: % 99.65/62.02 | (328) all_167_2_180 = all_162_2_177 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_6_6, all_173_2_183, all_183_2_189 and discharging atoms powerset(all_0_6_6) = all_183_2_189, powerset(all_0_6_6) = all_173_2_183, yields: % 99.65/62.02 | (329) all_183_2_189 = all_173_2_183 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_11_11, all_137_2_162, all_178_2_186 and discharging atoms powerset(all_0_11_11) = all_178_2_186, powerset(all_0_11_11) = all_137_2_162, yields: % 99.65/62.02 | (330) all_178_2_186 = all_137_2_162 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (110) with all_0_13_13, all_152_2_171, all_157_2_174 and discharging atoms powerset(all_0_13_13) = all_157_2_174, powerset(all_0_13_13) = all_152_2_171, yields: % 99.65/62.02 | (331) all_157_2_174 = all_152_2_171 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (88) with all_0_3_3, all_122_1_155, 0 and discharging atoms preboolean(all_0_3_3) = all_122_1_155, preboolean(all_0_3_3) = 0, yields: % 99.65/62.02 | (332) all_122_1_155 = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (88) with all_0_11_11, all_116_1_153, 0 and discharging atoms preboolean(all_0_11_11) = all_116_1_153, preboolean(all_0_11_11) = 0, yields: % 99.65/62.02 | (333) all_116_1_153 = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (88) with all_0_13_13, all_110_1_151, 0 and discharging atoms preboolean(all_0_13_13) = all_110_1_151, preboolean(all_0_13_13) = 0, yields: % 99.65/62.02 | (334) all_110_1_151 = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (28) with empty_set, all_0_11_11, all_45_0_74, all_116_0_152 and discharging atoms in(empty_set, all_0_11_11) = all_116_0_152, in(empty_set, all_0_11_11) = all_45_0_74, yields: % 99.65/62.02 | (335) all_116_0_152 = all_45_0_74 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (28) with empty_set, all_0_13_13, all_43_0_72, all_110_0_150 and discharging atoms in(empty_set, all_0_13_13) = all_110_0_150, in(empty_set, all_0_13_13) = all_43_0_72, yields: % 99.65/62.02 | (336) all_110_0_150 = all_43_0_72 % 99.65/62.02 | % 99.65/62.02 | Combining equations (326,327) yields a new equation: % 99.65/62.02 | (337) all_142_2_165 = all_88_0_133 % 99.65/62.02 | % 99.65/62.02 | Simplifying 337 yields: % 99.65/62.02 | (338) all_142_2_165 = all_88_0_133 % 99.65/62.02 | % 99.65/62.02 | From (338) and (245) follows: % 99.65/62.02 | (193) powerset(all_0_1_1) = all_88_0_133 % 99.65/62.02 | % 99.65/62.02 | From (328) and (294) follows: % 99.65/62.02 | (287) powerset(all_0_3_3) = all_162_2_177 % 99.65/62.02 | % 99.65/62.02 | From (329) and (324) follows: % 99.65/62.02 | (303) powerset(all_0_6_6) = all_173_2_183 % 99.65/62.02 | % 99.65/62.02 | From (330) and (315) follows: % 99.65/62.02 | (237) powerset(all_0_11_11) = all_137_2_162 % 99.65/62.02 | % 99.65/62.02 | From (331) and (275) follows: % 99.65/62.02 | (265) powerset(all_0_13_13) = all_152_2_171 % 99.65/62.02 | % 99.65/62.02 | From (332) and (220) follows: % 99.65/62.02 | (59) preboolean(all_0_3_3) = 0 % 99.65/62.02 | % 99.65/62.02 | From (333) and (212) follows: % 99.65/62.02 | (82) preboolean(all_0_11_11) = 0 % 99.65/62.02 | % 99.65/62.02 | From (334) and (204) follows: % 99.65/62.02 | (50) preboolean(all_0_13_13) = 0 % 99.65/62.02 | % 99.65/62.02 | From (335) and (213) follows: % 99.65/62.02 | (190) in(empty_set, all_0_11_11) = all_45_0_74 % 99.65/62.02 | % 99.65/62.02 | From (336) and (205) follows: % 99.65/62.02 | (186) in(empty_set, all_0_13_13) = all_43_0_72 % 99.65/62.02 | % 99.65/62.02 +-Applying beta-rule and splitting (214), into two cases. % 99.65/62.02 |-Branch one: % 99.65/62.02 | (349) ~ (all_116_1_153 = 0) % 99.65/62.02 | % 99.65/62.02 | Equations (333) can reduce 349 to: % 99.65/62.02 | (200) $false % 99.65/62.02 | % 99.65/62.02 |-The branch is then unsatisfiable % 99.65/62.02 |-Branch two: % 99.65/62.02 | (333) all_116_1_153 = 0 % 99.65/62.02 | (352) all_116_0_152 = 0 % 99.65/62.02 | % 99.65/62.02 | Combining equations (352,335) yields a new equation: % 99.65/62.02 | (353) all_45_0_74 = 0 % 99.65/62.02 | % 99.65/62.02 | From (353) and (190) follows: % 99.65/62.02 | (354) in(empty_set, all_0_11_11) = 0 % 99.65/62.02 | % 99.65/62.02 +-Applying beta-rule and splitting (206), into two cases. % 99.65/62.02 |-Branch one: % 99.65/62.02 | (355) ~ (all_110_1_151 = 0) % 99.65/62.02 | % 99.65/62.02 | Equations (334) can reduce 355 to: % 99.65/62.02 | (200) $false % 99.65/62.02 | % 99.65/62.02 |-The branch is then unsatisfiable % 99.65/62.02 |-Branch two: % 99.65/62.02 | (334) all_110_1_151 = 0 % 99.65/62.02 | (358) all_110_0_150 = 0 % 99.65/62.02 | % 99.65/62.02 | Combining equations (358,336) yields a new equation: % 99.65/62.02 | (359) all_43_0_72 = 0 % 99.65/62.02 | % 99.65/62.02 | From (359) and (186) follows: % 99.65/62.02 | (360) in(empty_set, all_0_13_13) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_88_0_133, all_0_1_1 and discharging atoms powerset(all_0_1_1) = all_88_0_133, yields: % 99.65/62.02 | (361) preboolean(all_88_0_133) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_162_2_177, all_0_3_3 and discharging atoms powerset(all_0_3_3) = all_162_2_177, yields: % 99.65/62.02 | (362) preboolean(all_162_2_177) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_173_2_183, all_0_6_6 and discharging atoms powerset(all_0_6_6) = all_173_2_183, yields: % 99.65/62.02 | (363) preboolean(all_173_2_183) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_137_2_162, all_0_11_11 and discharging atoms powerset(all_0_11_11) = all_137_2_162, yields: % 99.65/62.02 | (364) preboolean(all_137_2_162) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_152_2_171, all_0_13_13 and discharging atoms powerset(all_0_13_13) = all_152_2_171, yields: % 99.65/62.02 | (365) preboolean(all_152_2_171) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (39) with all_38_0_70, empty_set and discharging atoms powerset(empty_set) = all_38_0_70, yields: % 99.65/62.02 | (366) preboolean(all_38_0_70) = 0 % 99.65/62.02 | % 99.65/62.02 | Instantiating formula (122) with all_95_0_138, all_15_2_40 and discharging atoms empty(all_15_2_40) = all_95_0_138, yields: % 99.65/62.02 | (367) all_95_0_138 = 0 | ? [v0] : ? [v1] : (preboolean(all_15_2_40) = v0 & in(empty_set, all_15_2_40) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (122) with all_41_0_71, all_11_1_28 and discharging atoms empty(all_11_1_28) = all_41_0_71, yields: % 99.65/62.03 | (368) all_41_0_71 = 0 | ? [v0] : ? [v1] : (preboolean(all_11_1_28) = v0 & in(empty_set, all_11_1_28) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (77) with 0, empty_set, all_0_9_9, all_0_13_13, all_0_11_11 and discharging atoms set_intersection2(all_0_11_11, all_0_13_13) = all_0_9_9, in(empty_set, all_0_11_11) = 0, yields: % 99.65/62.03 | (369) ? [v0] : ? [v1] : (in(empty_set, all_0_9_9) = v0 & in(empty_set, all_0_13_13) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (30) with empty_set, all_0_9_9, all_0_13_13, all_0_11_11 and discharging atoms set_intersection2(all_0_11_11, all_0_13_13) = all_0_9_9, in(empty_set, all_0_11_11) = 0, yields: % 99.65/62.03 | (370) ? [v0] : ? [v1] : (in(empty_set, all_0_9_9) = v1 & in(empty_set, all_0_13_13) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (66) with 0, empty_set, all_0_9_9, all_0_13_13, all_0_11_11 and discharging atoms set_intersection2(all_0_11_11, all_0_13_13) = all_0_9_9, in(empty_set, all_0_13_13) = 0, yields: % 99.65/62.03 | (371) ? [v0] : ? [v1] : (in(empty_set, all_0_9_9) = v0 & in(empty_set, all_0_11_11) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (11) with empty_set, all_0_9_9, all_0_13_13, all_0_11_11 and discharging atoms set_intersection2(all_0_11_11, all_0_13_13) = all_0_9_9, in(empty_set, all_0_13_13) = 0, yields: % 99.65/62.03 | (372) ? [v0] : ? [v1] : (in(empty_set, all_0_9_9) = v1 & in(empty_set, all_0_11_11) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating (371) with all_320_0_329, all_320_1_330 yields: % 99.65/62.03 | (373) in(empty_set, all_0_9_9) = all_320_1_330 & in(empty_set, all_0_11_11) = all_320_0_329 & ( ~ (all_320_1_330 = 0) | all_320_0_329 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (373) yields: % 99.65/62.03 | (374) in(empty_set, all_0_9_9) = all_320_1_330 % 99.65/62.03 | (375) in(empty_set, all_0_11_11) = all_320_0_329 % 99.65/62.03 | (376) ~ (all_320_1_330 = 0) | all_320_0_329 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating (372) with all_360_0_371, all_360_1_372 yields: % 99.65/62.03 | (377) in(empty_set, all_0_9_9) = all_360_0_371 & in(empty_set, all_0_11_11) = all_360_1_372 & ( ~ (all_360_1_372 = 0) | all_360_0_371 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (377) yields: % 99.65/62.03 | (378) in(empty_set, all_0_9_9) = all_360_0_371 % 99.65/62.03 | (379) in(empty_set, all_0_11_11) = all_360_1_372 % 99.65/62.03 | (380) ~ (all_360_1_372 = 0) | all_360_0_371 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating (370) with all_427_0_475, all_427_1_476 yields: % 99.65/62.03 | (381) in(empty_set, all_0_9_9) = all_427_0_475 & in(empty_set, all_0_13_13) = all_427_1_476 & ( ~ (all_427_1_476 = 0) | all_427_0_475 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (381) yields: % 99.65/62.03 | (382) in(empty_set, all_0_9_9) = all_427_0_475 % 99.65/62.03 | (383) in(empty_set, all_0_13_13) = all_427_1_476 % 99.65/62.03 | (384) ~ (all_427_1_476 = 0) | all_427_0_475 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating (369) with all_429_0_477, all_429_1_478 yields: % 99.65/62.03 | (385) in(empty_set, all_0_9_9) = all_429_1_478 & in(empty_set, all_0_13_13) = all_429_0_477 & ( ~ (all_429_1_478 = 0) | all_429_0_477 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (385) yields: % 99.65/62.03 | (386) in(empty_set, all_0_9_9) = all_429_1_478 % 99.65/62.03 | (387) in(empty_set, all_0_13_13) = all_429_0_477 % 99.65/62.03 | (388) ~ (all_429_1_478 = 0) | all_429_0_477 = 0 % 99.65/62.03 | % 99.65/62.03 +-Applying beta-rule and splitting (368), into two cases. % 99.65/62.03 |-Branch one: % 99.65/62.03 | (389) all_41_0_71 = 0 % 99.65/62.03 | % 99.65/62.03 | Equations (389) can reduce 182 to: % 99.65/62.03 | (200) $false % 99.65/62.03 | % 99.65/62.03 |-The branch is then unsatisfiable % 99.65/62.03 |-Branch two: % 99.65/62.03 | (182) ~ (all_41_0_71 = 0) % 99.65/62.03 | (392) ? [v0] : ? [v1] : (preboolean(all_11_1_28) = v0 & in(empty_set, all_11_1_28) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating (392) with all_447_0_486, all_447_1_487 yields: % 99.65/62.03 | (393) preboolean(all_11_1_28) = all_447_1_487 & in(empty_set, all_11_1_28) = all_447_0_486 & ( ~ (all_447_1_487 = 0) | all_447_0_486 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (393) yields: % 99.65/62.03 | (394) preboolean(all_11_1_28) = all_447_1_487 % 99.65/62.03 | (395) in(empty_set, all_11_1_28) = all_447_0_486 % 99.65/62.03 | (396) ~ (all_447_1_487 = 0) | all_447_0_486 = 0 % 99.65/62.03 | % 99.65/62.03 +-Applying beta-rule and splitting (367), into two cases. % 99.65/62.03 |-Branch one: % 99.65/62.03 | (397) all_95_0_138 = 0 % 99.65/62.03 | % 99.65/62.03 | Equations (397) can reduce 197 to: % 99.65/62.03 | (200) $false % 99.65/62.03 | % 99.65/62.03 |-The branch is then unsatisfiable % 99.65/62.03 |-Branch two: % 99.65/62.03 | (197) ~ (all_95_0_138 = 0) % 99.65/62.03 | (400) ? [v0] : ? [v1] : (preboolean(all_15_2_40) = v0 & in(empty_set, all_15_2_40) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 99.65/62.03 | % 99.65/62.03 | Instantiating (400) with all_453_0_488, all_453_1_489 yields: % 99.65/62.03 | (401) preboolean(all_15_2_40) = all_453_1_489 & in(empty_set, all_15_2_40) = all_453_0_488 & ( ~ (all_453_1_489 = 0) | all_453_0_488 = 0) % 99.65/62.03 | % 99.65/62.03 | Applying alpha-rule on (401) yields: % 99.65/62.03 | (402) preboolean(all_15_2_40) = all_453_1_489 % 99.65/62.03 | (403) in(empty_set, all_15_2_40) = all_453_0_488 % 99.65/62.03 | (404) ~ (all_453_1_489 = 0) | all_453_0_488 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (88) with all_15_2_40, all_453_1_489, 0 and discharging atoms preboolean(all_15_2_40) = all_453_1_489, preboolean(all_15_2_40) = 0, yields: % 99.65/62.03 | (405) all_453_1_489 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (88) with all_11_1_28, all_447_1_487, 0 and discharging atoms preboolean(all_11_1_28) = all_447_1_487, preboolean(all_11_1_28) = 0, yields: % 99.65/62.03 | (406) all_447_1_487 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (28) with empty_set, all_0_9_9, all_427_0_475, all_429_1_478 and discharging atoms in(empty_set, all_0_9_9) = all_429_1_478, in(empty_set, all_0_9_9) = all_427_0_475, yields: % 99.65/62.03 | (407) all_429_1_478 = all_427_0_475 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (28) with empty_set, all_0_9_9, all_360_0_371, all_429_1_478 and discharging atoms in(empty_set, all_0_9_9) = all_429_1_478, in(empty_set, all_0_9_9) = all_360_0_371, yields: % 99.65/62.03 | (408) all_429_1_478 = all_360_0_371 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (28) with empty_set, all_0_9_9, all_320_1_330, all_427_0_475 and discharging atoms in(empty_set, all_0_9_9) = all_427_0_475, in(empty_set, all_0_9_9) = all_320_1_330, yields: % 99.65/62.03 | (409) all_427_0_475 = all_320_1_330 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (28) with empty_set, all_0_11_11, all_360_1_372, 0 and discharging atoms in(empty_set, all_0_11_11) = all_360_1_372, in(empty_set, all_0_11_11) = 0, yields: % 99.65/62.03 | (410) all_360_1_372 = 0 % 99.65/62.03 | % 99.65/62.03 | Instantiating formula (28) with empty_set, all_0_11_11, all_320_0_329, all_360_1_372 and discharging atoms in(empty_set, all_0_11_11) = all_360_1_372, in(empty_set, all_0_11_11) = all_320_0_329, yields: % 99.65/62.03 | (411) all_360_1_372 = all_320_0_329 % 99.65/62.03 | % 99.65/62.03 | Combining equations (407,408) yields a new equation: % 99.65/62.03 | (412) all_427_0_475 = all_360_0_371 % 99.65/62.03 | % 99.65/62.03 | Simplifying 412 yields: % 99.65/62.03 | (413) all_427_0_475 = all_360_0_371 % 99.65/62.03 | % 99.65/62.03 | Combining equations (409,413) yields a new equation: % 99.65/62.03 | (414) all_360_0_371 = all_320_1_330 % 99.65/62.03 | % 99.65/62.03 | Combining equations (410,411) yields a new equation: % 99.65/62.03 | (415) all_320_0_329 = 0 % 99.65/62.03 | % 99.65/62.03 | Combining equations (415,411) yields a new equation: % 99.65/62.03 | (410) all_360_1_372 = 0 % 99.65/62.03 | % 99.65/62.03 | From (405) and (402) follows: % 99.65/62.03 | (152) preboolean(all_15_2_40) = 0 % 99.65/62.03 | % 99.65/62.03 | From (406) and (394) follows: % 99.65/62.03 | (154) preboolean(all_11_1_28) = 0 % 99.65/62.03 | % 99.65/62.03 | From (414) and (378) follows: % 99.65/62.03 | (374) in(empty_set, all_0_9_9) = all_320_1_330 % 99.65/62.03 | % 99.65/62.03 +-Applying beta-rule and splitting (380), into two cases. % 99.65/62.03 |-Branch one: % 99.65/62.03 | (420) ~ (all_360_1_372 = 0) % 99.65/62.03 | % 99.65/62.03 | Equations (410) can reduce 420 to: % 99.65/62.03 | (200) $false % 99.65/62.03 | % 99.65/62.03 |-The branch is then unsatisfiable % 99.65/62.03 |-Branch two: % 99.65/62.03 | (410) all_360_1_372 = 0 % 99.65/62.03 | (423) all_360_0_371 = 0 % 99.65/62.03 | % 99.65/62.03 | Combining equations (423,414) yields a new equation: % 99.65/62.03 | (424) all_320_1_330 = 0 % 99.65/62.03 | % 99.65/62.03 | From (424) and (374) follows: % 99.65/62.03 | (425) in(empty_set, all_0_9_9) = 0 % 99.65/62.03 | % 99.65/62.03 +-Applying beta-rule and splitting (73), into two cases. % 99.65/62.03 |-Branch one: % 99.65/62.03 | (426) ~ (all_0_7_7 = 0) % 99.65/62.03 | % 99.65/62.03 +-Applying beta-rule and splitting (157), into two cases. % 99.65/62.03 |-Branch one: % 99.65/62.03 | (427) all_0_7_7 = 0 % 99.65/62.03 | % 99.65/62.03 | Equations (427) can reduce 426 to: % 99.65/62.03 | (200) $false % 99.65/62.03 | % 99.65/62.03 |-The branch is then unsatisfiable % 99.65/62.03 |-Branch two: % 99.65/62.03 | (426) ~ (all_0_7_7 = 0) % 99.65/62.03 | (430) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (set_difference(v0, v1) = v4 & set_union2(v0, v1) = v2 & in(v4, all_0_9_9) = v5 & in(v2, all_0_9_9) = v3 & in(v1, all_0_9_9) = 0 & in(v0, all_0_9_9) = 0 & ( ~ (v5 = 0) | ~ (v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating (430) with all_741_0_588, all_741_1_589, all_741_2_590, all_741_3_591, all_741_4_592, all_741_5_593 yields: % 99.65/62.04 | (431) set_difference(all_741_5_593, all_741_4_592) = all_741_1_589 & set_union2(all_741_5_593, all_741_4_592) = all_741_3_591 & in(all_741_1_589, all_0_9_9) = all_741_0_588 & in(all_741_3_591, all_0_9_9) = all_741_2_590 & in(all_741_4_592, all_0_9_9) = 0 & in(all_741_5_593, all_0_9_9) = 0 & ( ~ (all_741_0_588 = 0) | ~ (all_741_2_590 = 0)) % 99.65/62.04 | % 99.65/62.04 | Applying alpha-rule on (431) yields: % 99.65/62.04 | (432) ~ (all_741_0_588 = 0) | ~ (all_741_2_590 = 0) % 99.65/62.04 | (433) in(all_741_4_592, all_0_9_9) = 0 % 99.65/62.04 | (434) set_difference(all_741_5_593, all_741_4_592) = all_741_1_589 % 99.65/62.04 | (435) set_union2(all_741_5_593, all_741_4_592) = all_741_3_591 % 99.65/62.04 | (436) in(all_741_5_593, all_0_9_9) = 0 % 99.65/62.04 | (437) in(all_741_3_591, all_0_9_9) = all_741_2_590 % 99.65/62.04 | (438) in(all_741_1_589, all_0_9_9) = all_741_0_588 % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_15_2_40 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_15_2_40) = 0, yields: % 99.65/62.04 | (439) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_15_2_40) = v3 & in(all_741_1_589, all_15_2_40) = v4 & in(all_741_4_592, all_15_2_40) = v1 & in(all_741_5_593, all_15_2_40) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_11_1_28 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_11_1_28) = 0, yields: % 99.65/62.04 | (440) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_11_1_28) = v3 & in(all_741_1_589, all_11_1_28) = v4 & in(all_741_4_592, all_11_1_28) = v1 & in(all_741_5_593, all_11_1_28) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_5_1_17 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_5_1_17) = 0, yields: % 99.65/62.04 | (441) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_5_1_17) = v3 & in(all_741_1_589, all_5_1_17) = v4 & in(all_741_4_592, all_5_1_17) = v1 & in(all_741_5_593, all_5_1_17) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_0_3_3 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_0_3_3) = 0, yields: % 99.65/62.04 | (442) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_0_3_3) = v3 & in(all_741_1_589, all_0_3_3) = v4 & in(all_741_4_592, all_0_3_3) = v1 & in(all_741_5_593, all_0_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_0_11_11 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_0_11_11) = 0, yields: % 99.65/62.04 | (443) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_0_11_11) = v3 & in(all_741_1_589, all_0_11_11) = v4 & in(all_741_4_592, all_0_11_11) = v1 & in(all_741_5_593, all_0_11_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_0_13_13 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_0_13_13) = 0, yields: % 99.65/62.04 | (444) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_0_13_13) = v3 & in(all_741_1_589, all_0_13_13) = v4 & in(all_741_4_592, all_0_13_13) = v1 & in(all_741_5_593, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_15_2_40 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_15_2_40) = 0, yields: % 99.65/62.04 | (445) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_15_2_40) = v4 & in(all_741_3_591, all_15_2_40) = v2 & in(all_741_4_592, all_15_2_40) = v1 & in(all_741_5_593, all_15_2_40) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_11_1_28 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_11_1_28) = 0, yields: % 99.65/62.04 | (446) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_11_1_28) = v4 & in(all_741_3_591, all_11_1_28) = v2 & in(all_741_4_592, all_11_1_28) = v1 & in(all_741_5_593, all_11_1_28) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_5_1_17 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_5_1_17) = 0, yields: % 99.65/62.04 | (447) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_5_1_17) = v4 & in(all_741_3_591, all_5_1_17) = v2 & in(all_741_4_592, all_5_1_17) = v1 & in(all_741_5_593, all_5_1_17) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_0_3_3 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_0_3_3) = 0, yields: % 99.65/62.04 | (448) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_0_3_3) = v4 & in(all_741_3_591, all_0_3_3) = v2 & in(all_741_4_592, all_0_3_3) = v1 & in(all_741_5_593, all_0_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_0_11_11 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_0_11_11) = 0, yields: % 99.65/62.04 | (449) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_0_11_11) = v4 & in(all_741_3_591, all_0_11_11) = v2 & in(all_741_4_592, all_0_11_11) = v1 & in(all_741_5_593, all_0_11_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_0_13_13 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_0_13_13) = 0, yields: % 99.65/62.04 | (450) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_0_13_13) = v4 & in(all_741_3_591, all_0_13_13) = v2 & in(all_741_4_592, all_0_13_13) = v1 & in(all_741_5_593, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_173_2_183 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_173_2_183) = 0, yields: % 99.65/62.04 | (451) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_173_2_183) = v3 & in(all_741_1_589, all_173_2_183) = v4 & in(all_741_4_592, all_173_2_183) = v1 & in(all_741_5_593, all_173_2_183) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_173_2_183 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_173_2_183) = 0, yields: % 99.65/62.04 | (452) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_173_2_183) = v4 & in(all_741_3_591, all_173_2_183) = v2 & in(all_741_4_592, all_173_2_183) = v1 & in(all_741_5_593, all_173_2_183) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_162_2_177 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_162_2_177) = 0, yields: % 99.65/62.04 | (453) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_162_2_177) = v3 & in(all_741_1_589, all_162_2_177) = v4 & in(all_741_4_592, all_162_2_177) = v1 & in(all_741_5_593, all_162_2_177) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_162_2_177 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_162_2_177) = 0, yields: % 99.65/62.04 | (454) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_162_2_177) = v4 & in(all_741_3_591, all_162_2_177) = v2 & in(all_741_4_592, all_162_2_177) = v1 & in(all_741_5_593, all_162_2_177) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_152_2_171 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_152_2_171) = 0, yields: % 99.65/62.04 | (455) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_152_2_171) = v4 & in(all_741_3_591, all_152_2_171) = v2 & in(all_741_4_592, all_152_2_171) = v1 & in(all_741_5_593, all_152_2_171) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_137_2_162 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_137_2_162) = 0, yields: % 99.65/62.04 | (456) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_137_2_162) = v3 & in(all_741_1_589, all_137_2_162) = v4 & in(all_741_4_592, all_137_2_162) = v1 & in(all_741_5_593, all_137_2_162) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_137_2_162 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_137_2_162) = 0, yields: % 99.65/62.04 | (457) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_137_2_162) = v4 & in(all_741_3_591, all_137_2_162) = v2 & in(all_741_4_592, all_137_2_162) = v1 & in(all_741_5_593, all_137_2_162) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_88_0_133 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_88_0_133) = 0, yields: % 99.65/62.04 | (458) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_88_0_133) = v3 & in(all_741_1_589, all_88_0_133) = v4 & in(all_741_4_592, all_88_0_133) = v1 & in(all_741_5_593, all_88_0_133) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_88_0_133 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_88_0_133) = 0, yields: % 99.65/62.04 | (459) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_88_0_133) = v4 & in(all_741_3_591, all_88_0_133) = v2 & in(all_741_4_592, all_88_0_133) = v1 & in(all_741_5_593, all_88_0_133) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.04 | % 99.65/62.04 | Instantiating formula (57) with all_741_1_589, all_741_4_592, all_741_5_593, all_38_0_70 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, preboolean(all_38_0_70) = 0, yields: % 99.65/62.04 | (460) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_union2(all_741_5_593, all_741_4_592) = v2 & in(v2, all_38_0_70) = v3 & in(all_741_1_589, all_38_0_70) = v4 & in(all_741_4_592, all_38_0_70) = v1 & in(all_741_5_593, all_38_0_70) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v3 = 0))) % 99.65/62.05 | % 99.65/62.05 | Instantiating formula (83) with all_741_3_591, all_741_4_592, all_741_5_593, all_38_0_70 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, preboolean(all_38_0_70) = 0, yields: % 99.65/62.05 | (461) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (set_difference(all_741_5_593, all_741_4_592) = v3 & in(v3, all_38_0_70) = v4 & in(all_741_3_591, all_38_0_70) = v2 & in(all_741_4_592, all_38_0_70) = v1 & in(all_741_5_593, all_38_0_70) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v4 = 0 & v2 = 0))) % 99.65/62.05 | % 99.65/62.05 | Instantiating formula (4) with all_741_0_588, all_741_1_589, all_0_9_9, all_0_11_11, all_0_13_13 and discharging atoms set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9, in(all_741_1_589, all_0_9_9) = all_741_0_588, yields: % 99.65/62.05 | (462) all_741_0_588 = 0 | ? [v0] : ? [v1] : (in(all_741_1_589, all_0_11_11) = v1 & in(all_741_1_589, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 99.65/62.05 | % 99.65/62.05 | Instantiating formula (4) with all_741_2_590, all_741_3_591, all_0_9_9, all_0_11_11, all_0_13_13 and discharging atoms set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9, in(all_741_3_591, all_0_9_9) = all_741_2_590, yields: % 99.65/62.05 | (463) all_741_2_590 = 0 | ? [v0] : ? [v1] : (in(all_741_3_591, all_0_11_11) = v1 & in(all_741_3_591, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 99.65/62.05 | % 99.65/62.05 | Instantiating formula (18) with all_741_4_592, all_0_9_9, all_0_11_11, all_0_13_13 and discharging atoms set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9, in(all_741_4_592, all_0_9_9) = 0, yields: % 99.65/62.05 | (464) in(all_741_4_592, all_0_11_11) = 0 & in(all_741_4_592, all_0_13_13) = 0 % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (464) yields: % 99.65/62.05 | (465) in(all_741_4_592, all_0_11_11) = 0 % 99.65/62.05 | (466) in(all_741_4_592, all_0_13_13) = 0 % 99.65/62.05 | % 99.65/62.05 | Instantiating formula (18) with all_741_5_593, all_0_9_9, all_0_11_11, all_0_13_13 and discharging atoms set_intersection2(all_0_13_13, all_0_11_11) = all_0_9_9, in(all_741_5_593, all_0_9_9) = 0, yields: % 99.65/62.05 | (467) in(all_741_5_593, all_0_11_11) = 0 & in(all_741_5_593, all_0_13_13) = 0 % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (467) yields: % 99.65/62.05 | (468) in(all_741_5_593, all_0_11_11) = 0 % 99.65/62.05 | (469) in(all_741_5_593, all_0_13_13) = 0 % 99.65/62.05 | % 99.65/62.05 | Instantiating (455) with all_1574_0_2376, all_1574_1_2377, all_1574_2_2378, all_1574_3_2379, all_1574_4_2380 yields: % 99.65/62.05 | (470) set_difference(all_741_5_593, all_741_4_592) = all_1574_1_2377 & in(all_1574_1_2377, all_152_2_171) = all_1574_0_2376 & in(all_741_3_591, all_152_2_171) = all_1574_2_2378 & in(all_741_4_592, all_152_2_171) = all_1574_3_2379 & in(all_741_5_593, all_152_2_171) = all_1574_4_2380 & ( ~ (all_1574_3_2379 = 0) | ~ (all_1574_4_2380 = 0) | (all_1574_0_2376 = 0 & all_1574_2_2378 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (470) yields: % 99.65/62.05 | (471) in(all_741_4_592, all_152_2_171) = all_1574_3_2379 % 99.65/62.05 | (472) in(all_741_5_593, all_152_2_171) = all_1574_4_2380 % 99.65/62.05 | (473) ~ (all_1574_3_2379 = 0) | ~ (all_1574_4_2380 = 0) | (all_1574_0_2376 = 0 & all_1574_2_2378 = 0) % 99.65/62.05 | (474) in(all_1574_1_2377, all_152_2_171) = all_1574_0_2376 % 99.65/62.05 | (475) in(all_741_3_591, all_152_2_171) = all_1574_2_2378 % 99.65/62.05 | (476) set_difference(all_741_5_593, all_741_4_592) = all_1574_1_2377 % 99.65/62.05 | % 99.65/62.05 | Instantiating (454) with all_1653_0_2479, all_1653_1_2480, all_1653_2_2481, all_1653_3_2482, all_1653_4_2483 yields: % 99.65/62.05 | (477) set_difference(all_741_5_593, all_741_4_592) = all_1653_1_2480 & in(all_1653_1_2480, all_162_2_177) = all_1653_0_2479 & in(all_741_3_591, all_162_2_177) = all_1653_2_2481 & in(all_741_4_592, all_162_2_177) = all_1653_3_2482 & in(all_741_5_593, all_162_2_177) = all_1653_4_2483 & ( ~ (all_1653_3_2482 = 0) | ~ (all_1653_4_2483 = 0) | (all_1653_0_2479 = 0 & all_1653_2_2481 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (477) yields: % 99.65/62.05 | (478) in(all_741_5_593, all_162_2_177) = all_1653_4_2483 % 99.65/62.05 | (479) in(all_741_3_591, all_162_2_177) = all_1653_2_2481 % 99.65/62.05 | (480) ~ (all_1653_3_2482 = 0) | ~ (all_1653_4_2483 = 0) | (all_1653_0_2479 = 0 & all_1653_2_2481 = 0) % 99.65/62.05 | (481) in(all_1653_1_2480, all_162_2_177) = all_1653_0_2479 % 99.65/62.05 | (482) in(all_741_4_592, all_162_2_177) = all_1653_3_2482 % 99.65/62.05 | (483) set_difference(all_741_5_593, all_741_4_592) = all_1653_1_2480 % 99.65/62.05 | % 99.65/62.05 | Instantiating (453) with all_1676_0_2525, all_1676_1_2526, all_1676_2_2527, all_1676_3_2528, all_1676_4_2529 yields: % 99.65/62.05 | (484) set_union2(all_741_5_593, all_741_4_592) = all_1676_2_2527 & in(all_1676_2_2527, all_162_2_177) = all_1676_1_2526 & in(all_741_1_589, all_162_2_177) = all_1676_0_2525 & in(all_741_4_592, all_162_2_177) = all_1676_3_2528 & in(all_741_5_593, all_162_2_177) = all_1676_4_2529 & ( ~ (all_1676_3_2528 = 0) | ~ (all_1676_4_2529 = 0) | (all_1676_0_2525 = 0 & all_1676_1_2526 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (484) yields: % 99.65/62.05 | (485) set_union2(all_741_5_593, all_741_4_592) = all_1676_2_2527 % 99.65/62.05 | (486) in(all_741_5_593, all_162_2_177) = all_1676_4_2529 % 99.65/62.05 | (487) in(all_741_1_589, all_162_2_177) = all_1676_0_2525 % 99.65/62.05 | (488) in(all_1676_2_2527, all_162_2_177) = all_1676_1_2526 % 99.65/62.05 | (489) in(all_741_4_592, all_162_2_177) = all_1676_3_2528 % 99.65/62.05 | (490) ~ (all_1676_3_2528 = 0) | ~ (all_1676_4_2529 = 0) | (all_1676_0_2525 = 0 & all_1676_1_2526 = 0) % 99.65/62.05 | % 99.65/62.05 | Instantiating (450) with all_1708_0_2572, all_1708_1_2573, all_1708_2_2574, all_1708_3_2575, all_1708_4_2576 yields: % 99.65/62.05 | (491) set_difference(all_741_5_593, all_741_4_592) = all_1708_1_2573 & in(all_1708_1_2573, all_0_13_13) = all_1708_0_2572 & in(all_741_3_591, all_0_13_13) = all_1708_2_2574 & in(all_741_4_592, all_0_13_13) = all_1708_3_2575 & in(all_741_5_593, all_0_13_13) = all_1708_4_2576 & ( ~ (all_1708_3_2575 = 0) | ~ (all_1708_4_2576 = 0) | (all_1708_0_2572 = 0 & all_1708_2_2574 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (491) yields: % 99.65/62.05 | (492) in(all_1708_1_2573, all_0_13_13) = all_1708_0_2572 % 99.65/62.05 | (493) in(all_741_3_591, all_0_13_13) = all_1708_2_2574 % 99.65/62.05 | (494) ~ (all_1708_3_2575 = 0) | ~ (all_1708_4_2576 = 0) | (all_1708_0_2572 = 0 & all_1708_2_2574 = 0) % 99.65/62.05 | (495) set_difference(all_741_5_593, all_741_4_592) = all_1708_1_2573 % 99.65/62.05 | (496) in(all_741_5_593, all_0_13_13) = all_1708_4_2576 % 99.65/62.05 | (497) in(all_741_4_592, all_0_13_13) = all_1708_3_2575 % 99.65/62.05 | % 99.65/62.05 | Instantiating (449) with all_1710_0_2577, all_1710_1_2578, all_1710_2_2579, all_1710_3_2580, all_1710_4_2581 yields: % 99.65/62.05 | (498) set_difference(all_741_5_593, all_741_4_592) = all_1710_1_2578 & in(all_1710_1_2578, all_0_11_11) = all_1710_0_2577 & in(all_741_3_591, all_0_11_11) = all_1710_2_2579 & in(all_741_4_592, all_0_11_11) = all_1710_3_2580 & in(all_741_5_593, all_0_11_11) = all_1710_4_2581 & ( ~ (all_1710_3_2580 = 0) | ~ (all_1710_4_2581 = 0) | (all_1710_0_2577 = 0 & all_1710_2_2579 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (498) yields: % 99.65/62.05 | (499) in(all_741_3_591, all_0_11_11) = all_1710_2_2579 % 99.65/62.05 | (500) in(all_741_4_592, all_0_11_11) = all_1710_3_2580 % 99.65/62.05 | (501) in(all_1710_1_2578, all_0_11_11) = all_1710_0_2577 % 99.65/62.05 | (502) ~ (all_1710_3_2580 = 0) | ~ (all_1710_4_2581 = 0) | (all_1710_0_2577 = 0 & all_1710_2_2579 = 0) % 99.65/62.05 | (503) in(all_741_5_593, all_0_11_11) = all_1710_4_2581 % 99.65/62.05 | (504) set_difference(all_741_5_593, all_741_4_592) = all_1710_1_2578 % 99.65/62.05 | % 99.65/62.05 | Instantiating (448) with all_1712_0_2582, all_1712_1_2583, all_1712_2_2584, all_1712_3_2585, all_1712_4_2586 yields: % 99.65/62.05 | (505) set_difference(all_741_5_593, all_741_4_592) = all_1712_1_2583 & in(all_1712_1_2583, all_0_3_3) = all_1712_0_2582 & in(all_741_3_591, all_0_3_3) = all_1712_2_2584 & in(all_741_4_592, all_0_3_3) = all_1712_3_2585 & in(all_741_5_593, all_0_3_3) = all_1712_4_2586 & ( ~ (all_1712_3_2585 = 0) | ~ (all_1712_4_2586 = 0) | (all_1712_0_2582 = 0 & all_1712_2_2584 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (505) yields: % 99.65/62.05 | (506) ~ (all_1712_3_2585 = 0) | ~ (all_1712_4_2586 = 0) | (all_1712_0_2582 = 0 & all_1712_2_2584 = 0) % 99.65/62.05 | (507) in(all_741_4_592, all_0_3_3) = all_1712_3_2585 % 99.65/62.05 | (508) set_difference(all_741_5_593, all_741_4_592) = all_1712_1_2583 % 99.65/62.05 | (509) in(all_741_5_593, all_0_3_3) = all_1712_4_2586 % 99.65/62.05 | (510) in(all_741_3_591, all_0_3_3) = all_1712_2_2584 % 99.65/62.05 | (511) in(all_1712_1_2583, all_0_3_3) = all_1712_0_2582 % 99.65/62.05 | % 99.65/62.05 | Instantiating (447) with all_1714_0_2587, all_1714_1_2588, all_1714_2_2589, all_1714_3_2590, all_1714_4_2591 yields: % 99.65/62.05 | (512) set_difference(all_741_5_593, all_741_4_592) = all_1714_1_2588 & in(all_1714_1_2588, all_5_1_17) = all_1714_0_2587 & in(all_741_3_591, all_5_1_17) = all_1714_2_2589 & in(all_741_4_592, all_5_1_17) = all_1714_3_2590 & in(all_741_5_593, all_5_1_17) = all_1714_4_2591 & ( ~ (all_1714_3_2590 = 0) | ~ (all_1714_4_2591 = 0) | (all_1714_0_2587 = 0 & all_1714_2_2589 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (512) yields: % 99.65/62.05 | (513) in(all_1714_1_2588, all_5_1_17) = all_1714_0_2587 % 99.65/62.05 | (514) in(all_741_4_592, all_5_1_17) = all_1714_3_2590 % 99.65/62.05 | (515) ~ (all_1714_3_2590 = 0) | ~ (all_1714_4_2591 = 0) | (all_1714_0_2587 = 0 & all_1714_2_2589 = 0) % 99.65/62.05 | (516) in(all_741_3_591, all_5_1_17) = all_1714_2_2589 % 99.65/62.05 | (517) set_difference(all_741_5_593, all_741_4_592) = all_1714_1_2588 % 99.65/62.05 | (518) in(all_741_5_593, all_5_1_17) = all_1714_4_2591 % 99.65/62.05 | % 99.65/62.05 | Instantiating (446) with all_1716_0_2592, all_1716_1_2593, all_1716_2_2594, all_1716_3_2595, all_1716_4_2596 yields: % 99.65/62.05 | (519) set_difference(all_741_5_593, all_741_4_592) = all_1716_1_2593 & in(all_1716_1_2593, all_11_1_28) = all_1716_0_2592 & in(all_741_3_591, all_11_1_28) = all_1716_2_2594 & in(all_741_4_592, all_11_1_28) = all_1716_3_2595 & in(all_741_5_593, all_11_1_28) = all_1716_4_2596 & ( ~ (all_1716_3_2595 = 0) | ~ (all_1716_4_2596 = 0) | (all_1716_0_2592 = 0 & all_1716_2_2594 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (519) yields: % 99.65/62.05 | (520) in(all_741_5_593, all_11_1_28) = all_1716_4_2596 % 99.65/62.05 | (521) in(all_1716_1_2593, all_11_1_28) = all_1716_0_2592 % 99.65/62.05 | (522) ~ (all_1716_3_2595 = 0) | ~ (all_1716_4_2596 = 0) | (all_1716_0_2592 = 0 & all_1716_2_2594 = 0) % 99.65/62.05 | (523) in(all_741_3_591, all_11_1_28) = all_1716_2_2594 % 99.65/62.05 | (524) set_difference(all_741_5_593, all_741_4_592) = all_1716_1_2593 % 99.65/62.05 | (525) in(all_741_4_592, all_11_1_28) = all_1716_3_2595 % 99.65/62.05 | % 99.65/62.05 | Instantiating (461) with all_1780_0_2678, all_1780_1_2679, all_1780_2_2680, all_1780_3_2681, all_1780_4_2682 yields: % 99.65/62.05 | (526) set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679 & in(all_1780_1_2679, all_38_0_70) = all_1780_0_2678 & in(all_741_3_591, all_38_0_70) = all_1780_2_2680 & in(all_741_4_592, all_38_0_70) = all_1780_3_2681 & in(all_741_5_593, all_38_0_70) = all_1780_4_2682 & ( ~ (all_1780_3_2681 = 0) | ~ (all_1780_4_2682 = 0) | (all_1780_0_2678 = 0 & all_1780_2_2680 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (526) yields: % 99.65/62.05 | (527) in(all_741_5_593, all_38_0_70) = all_1780_4_2682 % 99.65/62.05 | (528) in(all_741_3_591, all_38_0_70) = all_1780_2_2680 % 99.65/62.05 | (529) ~ (all_1780_3_2681 = 0) | ~ (all_1780_4_2682 = 0) | (all_1780_0_2678 = 0 & all_1780_2_2680 = 0) % 99.65/62.05 | (530) in(all_741_4_592, all_38_0_70) = all_1780_3_2681 % 99.65/62.05 | (531) in(all_1780_1_2679, all_38_0_70) = all_1780_0_2678 % 99.65/62.05 | (532) set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679 % 99.65/62.05 | % 99.65/62.05 | Instantiating (457) with all_1788_0_2698, all_1788_1_2699, all_1788_2_2700, all_1788_3_2701, all_1788_4_2702 yields: % 99.65/62.05 | (533) set_difference(all_741_5_593, all_741_4_592) = all_1788_1_2699 & in(all_1788_1_2699, all_137_2_162) = all_1788_0_2698 & in(all_741_3_591, all_137_2_162) = all_1788_2_2700 & in(all_741_4_592, all_137_2_162) = all_1788_3_2701 & in(all_741_5_593, all_137_2_162) = all_1788_4_2702 & ( ~ (all_1788_3_2701 = 0) | ~ (all_1788_4_2702 = 0) | (all_1788_0_2698 = 0 & all_1788_2_2700 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (533) yields: % 99.65/62.05 | (534) in(all_741_4_592, all_137_2_162) = all_1788_3_2701 % 99.65/62.05 | (535) in(all_741_5_593, all_137_2_162) = all_1788_4_2702 % 99.65/62.05 | (536) set_difference(all_741_5_593, all_741_4_592) = all_1788_1_2699 % 99.65/62.05 | (537) in(all_1788_1_2699, all_137_2_162) = all_1788_0_2698 % 99.65/62.05 | (538) in(all_741_3_591, all_137_2_162) = all_1788_2_2700 % 99.65/62.05 | (539) ~ (all_1788_3_2701 = 0) | ~ (all_1788_4_2702 = 0) | (all_1788_0_2698 = 0 & all_1788_2_2700 = 0) % 99.65/62.05 | % 99.65/62.05 | Instantiating (456) with all_1800_0_2728, all_1800_1_2729, all_1800_2_2730, all_1800_3_2731, all_1800_4_2732 yields: % 99.65/62.05 | (540) set_union2(all_741_5_593, all_741_4_592) = all_1800_2_2730 & in(all_1800_2_2730, all_137_2_162) = all_1800_1_2729 & in(all_741_1_589, all_137_2_162) = all_1800_0_2728 & in(all_741_4_592, all_137_2_162) = all_1800_3_2731 & in(all_741_5_593, all_137_2_162) = all_1800_4_2732 & ( ~ (all_1800_3_2731 = 0) | ~ (all_1800_4_2732 = 0) | (all_1800_0_2728 = 0 & all_1800_1_2729 = 0)) % 99.65/62.05 | % 99.65/62.05 | Applying alpha-rule on (540) yields: % 99.65/62.05 | (541) in(all_1800_2_2730, all_137_2_162) = all_1800_1_2729 % 99.65/62.05 | (542) set_union2(all_741_5_593, all_741_4_592) = all_1800_2_2730 % 99.65/62.05 | (543) ~ (all_1800_3_2731 = 0) | ~ (all_1800_4_2732 = 0) | (all_1800_0_2728 = 0 & all_1800_1_2729 = 0) % 99.65/62.05 | (544) in(all_741_4_592, all_137_2_162) = all_1800_3_2731 % 99.65/62.05 | (545) in(all_741_1_589, all_137_2_162) = all_1800_0_2728 % 99.65/62.06 | (546) in(all_741_5_593, all_137_2_162) = all_1800_4_2732 % 99.65/62.06 | % 99.65/62.06 | Instantiating (458) with all_1819_0_2755, all_1819_1_2756, all_1819_2_2757, all_1819_3_2758, all_1819_4_2759 yields: % 99.65/62.06 | (547) set_union2(all_741_5_593, all_741_4_592) = all_1819_2_2757 & in(all_1819_2_2757, all_88_0_133) = all_1819_1_2756 & in(all_741_1_589, all_88_0_133) = all_1819_0_2755 & in(all_741_4_592, all_88_0_133) = all_1819_3_2758 & in(all_741_5_593, all_88_0_133) = all_1819_4_2759 & ( ~ (all_1819_3_2758 = 0) | ~ (all_1819_4_2759 = 0) | (all_1819_0_2755 = 0 & all_1819_1_2756 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (547) yields: % 99.65/62.06 | (548) in(all_1819_2_2757, all_88_0_133) = all_1819_1_2756 % 99.65/62.06 | (549) ~ (all_1819_3_2758 = 0) | ~ (all_1819_4_2759 = 0) | (all_1819_0_2755 = 0 & all_1819_1_2756 = 0) % 99.65/62.06 | (550) in(all_741_5_593, all_88_0_133) = all_1819_4_2759 % 99.65/62.06 | (551) in(all_741_1_589, all_88_0_133) = all_1819_0_2755 % 99.65/62.06 | (552) set_union2(all_741_5_593, all_741_4_592) = all_1819_2_2757 % 99.65/62.06 | (553) in(all_741_4_592, all_88_0_133) = all_1819_3_2758 % 99.65/62.06 | % 99.65/62.06 | Instantiating (460) with all_1886_0_2849, all_1886_1_2850, all_1886_2_2851, all_1886_3_2852, all_1886_4_2853 yields: % 99.65/62.06 | (554) set_union2(all_741_5_593, all_741_4_592) = all_1886_2_2851 & in(all_1886_2_2851, all_38_0_70) = all_1886_1_2850 & in(all_741_1_589, all_38_0_70) = all_1886_0_2849 & in(all_741_4_592, all_38_0_70) = all_1886_3_2852 & in(all_741_5_593, all_38_0_70) = all_1886_4_2853 & ( ~ (all_1886_3_2852 = 0) | ~ (all_1886_4_2853 = 0) | (all_1886_0_2849 = 0 & all_1886_1_2850 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (554) yields: % 99.65/62.06 | (555) in(all_1886_2_2851, all_38_0_70) = all_1886_1_2850 % 99.65/62.06 | (556) in(all_741_5_593, all_38_0_70) = all_1886_4_2853 % 99.65/62.06 | (557) in(all_741_1_589, all_38_0_70) = all_1886_0_2849 % 99.65/62.06 | (558) set_union2(all_741_5_593, all_741_4_592) = all_1886_2_2851 % 99.65/62.06 | (559) ~ (all_1886_3_2852 = 0) | ~ (all_1886_4_2853 = 0) | (all_1886_0_2849 = 0 & all_1886_1_2850 = 0) % 99.65/62.06 | (560) in(all_741_4_592, all_38_0_70) = all_1886_3_2852 % 99.65/62.06 | % 99.65/62.06 | Instantiating (459) with all_1898_0_2876, all_1898_1_2877, all_1898_2_2878, all_1898_3_2879, all_1898_4_2880 yields: % 99.65/62.06 | (561) set_difference(all_741_5_593, all_741_4_592) = all_1898_1_2877 & in(all_1898_1_2877, all_88_0_133) = all_1898_0_2876 & in(all_741_3_591, all_88_0_133) = all_1898_2_2878 & in(all_741_4_592, all_88_0_133) = all_1898_3_2879 & in(all_741_5_593, all_88_0_133) = all_1898_4_2880 & ( ~ (all_1898_3_2879 = 0) | ~ (all_1898_4_2880 = 0) | (all_1898_0_2876 = 0 & all_1898_2_2878 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (561) yields: % 99.65/62.06 | (562) set_difference(all_741_5_593, all_741_4_592) = all_1898_1_2877 % 99.65/62.06 | (563) in(all_741_4_592, all_88_0_133) = all_1898_3_2879 % 99.65/62.06 | (564) in(all_1898_1_2877, all_88_0_133) = all_1898_0_2876 % 99.65/62.06 | (565) in(all_741_3_591, all_88_0_133) = all_1898_2_2878 % 99.65/62.06 | (566) in(all_741_5_593, all_88_0_133) = all_1898_4_2880 % 99.65/62.06 | (567) ~ (all_1898_3_2879 = 0) | ~ (all_1898_4_2880 = 0) | (all_1898_0_2876 = 0 & all_1898_2_2878 = 0) % 99.65/62.06 | % 99.65/62.06 | Instantiating (445) with all_1908_0_2895, all_1908_1_2896, all_1908_2_2897, all_1908_3_2898, all_1908_4_2899 yields: % 99.65/62.06 | (568) set_difference(all_741_5_593, all_741_4_592) = all_1908_1_2896 & in(all_1908_1_2896, all_15_2_40) = all_1908_0_2895 & in(all_741_3_591, all_15_2_40) = all_1908_2_2897 & in(all_741_4_592, all_15_2_40) = all_1908_3_2898 & in(all_741_5_593, all_15_2_40) = all_1908_4_2899 & ( ~ (all_1908_3_2898 = 0) | ~ (all_1908_4_2899 = 0) | (all_1908_0_2895 = 0 & all_1908_2_2897 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (568) yields: % 99.65/62.06 | (569) in(all_1908_1_2896, all_15_2_40) = all_1908_0_2895 % 99.65/62.06 | (570) in(all_741_5_593, all_15_2_40) = all_1908_4_2899 % 99.65/62.06 | (571) ~ (all_1908_3_2898 = 0) | ~ (all_1908_4_2899 = 0) | (all_1908_0_2895 = 0 & all_1908_2_2897 = 0) % 99.65/62.06 | (572) in(all_741_4_592, all_15_2_40) = all_1908_3_2898 % 99.65/62.06 | (573) set_difference(all_741_5_593, all_741_4_592) = all_1908_1_2896 % 99.65/62.06 | (574) in(all_741_3_591, all_15_2_40) = all_1908_2_2897 % 99.65/62.06 | % 99.65/62.06 | Instantiating (439) with all_2034_0_3006, all_2034_1_3007, all_2034_2_3008, all_2034_3_3009, all_2034_4_3010 yields: % 99.65/62.06 | (575) set_union2(all_741_5_593, all_741_4_592) = all_2034_2_3008 & in(all_2034_2_3008, all_15_2_40) = all_2034_1_3007 & in(all_741_1_589, all_15_2_40) = all_2034_0_3006 & in(all_741_4_592, all_15_2_40) = all_2034_3_3009 & in(all_741_5_593, all_15_2_40) = all_2034_4_3010 & ( ~ (all_2034_3_3009 = 0) | ~ (all_2034_4_3010 = 0) | (all_2034_0_3006 = 0 & all_2034_1_3007 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (575) yields: % 99.65/62.06 | (576) in(all_741_1_589, all_15_2_40) = all_2034_0_3006 % 99.65/62.06 | (577) in(all_2034_2_3008, all_15_2_40) = all_2034_1_3007 % 99.65/62.06 | (578) in(all_741_5_593, all_15_2_40) = all_2034_4_3010 % 99.65/62.06 | (579) ~ (all_2034_3_3009 = 0) | ~ (all_2034_4_3010 = 0) | (all_2034_0_3006 = 0 & all_2034_1_3007 = 0) % 99.65/62.06 | (580) in(all_741_4_592, all_15_2_40) = all_2034_3_3009 % 99.65/62.06 | (581) set_union2(all_741_5_593, all_741_4_592) = all_2034_2_3008 % 99.65/62.06 | % 99.65/62.06 | Instantiating (452) with all_2077_0_3071, all_2077_1_3072, all_2077_2_3073, all_2077_3_3074, all_2077_4_3075 yields: % 99.65/62.06 | (582) set_difference(all_741_5_593, all_741_4_592) = all_2077_1_3072 & in(all_2077_1_3072, all_173_2_183) = all_2077_0_3071 & in(all_741_3_591, all_173_2_183) = all_2077_2_3073 & in(all_741_4_592, all_173_2_183) = all_2077_3_3074 & in(all_741_5_593, all_173_2_183) = all_2077_4_3075 & ( ~ (all_2077_3_3074 = 0) | ~ (all_2077_4_3075 = 0) | (all_2077_0_3071 = 0 & all_2077_2_3073 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (582) yields: % 99.65/62.06 | (583) in(all_741_4_592, all_173_2_183) = all_2077_3_3074 % 99.65/62.06 | (584) ~ (all_2077_3_3074 = 0) | ~ (all_2077_4_3075 = 0) | (all_2077_0_3071 = 0 & all_2077_2_3073 = 0) % 99.65/62.06 | (585) in(all_741_5_593, all_173_2_183) = all_2077_4_3075 % 99.65/62.06 | (586) in(all_2077_1_3072, all_173_2_183) = all_2077_0_3071 % 99.65/62.06 | (587) set_difference(all_741_5_593, all_741_4_592) = all_2077_1_3072 % 99.65/62.06 | (588) in(all_741_3_591, all_173_2_183) = all_2077_2_3073 % 99.65/62.06 | % 99.65/62.06 | Instantiating (443) with all_2085_0_3088, all_2085_1_3089, all_2085_2_3090, all_2085_3_3091, all_2085_4_3092 yields: % 99.65/62.06 | (589) set_union2(all_741_5_593, all_741_4_592) = all_2085_2_3090 & in(all_2085_2_3090, all_0_11_11) = all_2085_1_3089 & in(all_741_1_589, all_0_11_11) = all_2085_0_3088 & in(all_741_4_592, all_0_11_11) = all_2085_3_3091 & in(all_741_5_593, all_0_11_11) = all_2085_4_3092 & ( ~ (all_2085_3_3091 = 0) | ~ (all_2085_4_3092 = 0) | (all_2085_0_3088 = 0 & all_2085_1_3089 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (589) yields: % 99.65/62.06 | (590) ~ (all_2085_3_3091 = 0) | ~ (all_2085_4_3092 = 0) | (all_2085_0_3088 = 0 & all_2085_1_3089 = 0) % 99.65/62.06 | (591) in(all_2085_2_3090, all_0_11_11) = all_2085_1_3089 % 99.65/62.06 | (592) in(all_741_1_589, all_0_11_11) = all_2085_0_3088 % 99.65/62.06 | (593) set_union2(all_741_5_593, all_741_4_592) = all_2085_2_3090 % 99.65/62.06 | (594) in(all_741_4_592, all_0_11_11) = all_2085_3_3091 % 99.65/62.06 | (595) in(all_741_5_593, all_0_11_11) = all_2085_4_3092 % 99.65/62.06 | % 99.65/62.06 | Instantiating (441) with all_2087_0_3093, all_2087_1_3094, all_2087_2_3095, all_2087_3_3096, all_2087_4_3097 yields: % 99.65/62.06 | (596) set_union2(all_741_5_593, all_741_4_592) = all_2087_2_3095 & in(all_2087_2_3095, all_5_1_17) = all_2087_1_3094 & in(all_741_1_589, all_5_1_17) = all_2087_0_3093 & in(all_741_4_592, all_5_1_17) = all_2087_3_3096 & in(all_741_5_593, all_5_1_17) = all_2087_4_3097 & ( ~ (all_2087_3_3096 = 0) | ~ (all_2087_4_3097 = 0) | (all_2087_0_3093 = 0 & all_2087_1_3094 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (596) yields: % 99.65/62.06 | (597) in(all_2087_2_3095, all_5_1_17) = all_2087_1_3094 % 99.65/62.06 | (598) set_union2(all_741_5_593, all_741_4_592) = all_2087_2_3095 % 99.65/62.06 | (599) in(all_741_1_589, all_5_1_17) = all_2087_0_3093 % 99.65/62.06 | (600) in(all_741_5_593, all_5_1_17) = all_2087_4_3097 % 99.65/62.06 | (601) in(all_741_4_592, all_5_1_17) = all_2087_3_3096 % 99.65/62.06 | (602) ~ (all_2087_3_3096 = 0) | ~ (all_2087_4_3097 = 0) | (all_2087_0_3093 = 0 & all_2087_1_3094 = 0) % 99.65/62.06 | % 99.65/62.06 | Instantiating (442) with all_2089_0_3098, all_2089_1_3099, all_2089_2_3100, all_2089_3_3101, all_2089_4_3102 yields: % 99.65/62.06 | (603) set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100 & in(all_2089_2_3100, all_0_3_3) = all_2089_1_3099 & in(all_741_1_589, all_0_3_3) = all_2089_0_3098 & in(all_741_4_592, all_0_3_3) = all_2089_3_3101 & in(all_741_5_593, all_0_3_3) = all_2089_4_3102 & ( ~ (all_2089_3_3101 = 0) | ~ (all_2089_4_3102 = 0) | (all_2089_0_3098 = 0 & all_2089_1_3099 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (603) yields: % 99.65/62.06 | (604) ~ (all_2089_3_3101 = 0) | ~ (all_2089_4_3102 = 0) | (all_2089_0_3098 = 0 & all_2089_1_3099 = 0) % 99.65/62.06 | (605) in(all_741_1_589, all_0_3_3) = all_2089_0_3098 % 99.65/62.06 | (606) set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100 % 99.65/62.06 | (607) in(all_741_4_592, all_0_3_3) = all_2089_3_3101 % 99.65/62.06 | (608) in(all_741_5_593, all_0_3_3) = all_2089_4_3102 % 99.65/62.06 | (609) in(all_2089_2_3100, all_0_3_3) = all_2089_1_3099 % 99.65/62.06 | % 99.65/62.06 | Instantiating (451) with all_2095_0_3113, all_2095_1_3114, all_2095_2_3115, all_2095_3_3116, all_2095_4_3117 yields: % 99.65/62.06 | (610) set_union2(all_741_5_593, all_741_4_592) = all_2095_2_3115 & in(all_2095_2_3115, all_173_2_183) = all_2095_1_3114 & in(all_741_1_589, all_173_2_183) = all_2095_0_3113 & in(all_741_4_592, all_173_2_183) = all_2095_3_3116 & in(all_741_5_593, all_173_2_183) = all_2095_4_3117 & ( ~ (all_2095_3_3116 = 0) | ~ (all_2095_4_3117 = 0) | (all_2095_0_3113 = 0 & all_2095_1_3114 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (610) yields: % 99.65/62.06 | (611) ~ (all_2095_3_3116 = 0) | ~ (all_2095_4_3117 = 0) | (all_2095_0_3113 = 0 & all_2095_1_3114 = 0) % 99.65/62.06 | (612) in(all_741_1_589, all_173_2_183) = all_2095_0_3113 % 99.65/62.06 | (613) in(all_741_4_592, all_173_2_183) = all_2095_3_3116 % 99.65/62.06 | (614) in(all_2095_2_3115, all_173_2_183) = all_2095_1_3114 % 99.65/62.06 | (615) set_union2(all_741_5_593, all_741_4_592) = all_2095_2_3115 % 99.65/62.06 | (616) in(all_741_5_593, all_173_2_183) = all_2095_4_3117 % 99.65/62.06 | % 99.65/62.06 | Instantiating (440) with all_2099_0_3123, all_2099_1_3124, all_2099_2_3125, all_2099_3_3126, all_2099_4_3127 yields: % 99.65/62.06 | (617) set_union2(all_741_5_593, all_741_4_592) = all_2099_2_3125 & in(all_2099_2_3125, all_11_1_28) = all_2099_1_3124 & in(all_741_1_589, all_11_1_28) = all_2099_0_3123 & in(all_741_4_592, all_11_1_28) = all_2099_3_3126 & in(all_741_5_593, all_11_1_28) = all_2099_4_3127 & ( ~ (all_2099_3_3126 = 0) | ~ (all_2099_4_3127 = 0) | (all_2099_0_3123 = 0 & all_2099_1_3124 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (617) yields: % 99.65/62.06 | (618) ~ (all_2099_3_3126 = 0) | ~ (all_2099_4_3127 = 0) | (all_2099_0_3123 = 0 & all_2099_1_3124 = 0) % 99.65/62.06 | (619) in(all_741_1_589, all_11_1_28) = all_2099_0_3123 % 99.65/62.06 | (620) in(all_2099_2_3125, all_11_1_28) = all_2099_1_3124 % 99.65/62.06 | (621) set_union2(all_741_5_593, all_741_4_592) = all_2099_2_3125 % 99.65/62.06 | (622) in(all_741_4_592, all_11_1_28) = all_2099_3_3126 % 99.65/62.06 | (623) in(all_741_5_593, all_11_1_28) = all_2099_4_3127 % 99.65/62.06 | % 99.65/62.06 | Instantiating (444) with all_2105_0_3138, all_2105_1_3139, all_2105_2_3140, all_2105_3_3141, all_2105_4_3142 yields: % 99.65/62.06 | (624) set_union2(all_741_5_593, all_741_4_592) = all_2105_2_3140 & in(all_2105_2_3140, all_0_13_13) = all_2105_1_3139 & in(all_741_1_589, all_0_13_13) = all_2105_0_3138 & in(all_741_4_592, all_0_13_13) = all_2105_3_3141 & in(all_741_5_593, all_0_13_13) = all_2105_4_3142 & ( ~ (all_2105_3_3141 = 0) | ~ (all_2105_4_3142 = 0) | (all_2105_0_3138 = 0 & all_2105_1_3139 = 0)) % 99.65/62.06 | % 99.65/62.06 | Applying alpha-rule on (624) yields: % 99.65/62.06 | (625) in(all_741_5_593, all_0_13_13) = all_2105_4_3142 % 99.65/62.06 | (626) in(all_2105_2_3140, all_0_13_13) = all_2105_1_3139 % 99.65/62.06 | (627) set_union2(all_741_5_593, all_741_4_592) = all_2105_2_3140 % 99.65/62.06 | (628) in(all_741_1_589, all_0_13_13) = all_2105_0_3138 % 99.65/62.06 | (629) ~ (all_2105_3_3141 = 0) | ~ (all_2105_4_3142 = 0) | (all_2105_0_3138 = 0 & all_2105_1_3139 = 0) % 99.65/62.06 | (630) in(all_741_4_592, all_0_13_13) = all_2105_3_3141 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1908_1_2896, all_2077_1_3072 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_2077_1_3072, set_difference(all_741_5_593, all_741_4_592) = all_1908_1_2896, yields: % 99.65/62.06 | (631) all_2077_1_3072 = all_1908_1_2896 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1788_1_2699, all_1898_1_2877 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1898_1_2877, set_difference(all_741_5_593, all_741_4_592) = all_1788_1_2699, yields: % 99.65/62.06 | (632) all_1898_1_2877 = all_1788_1_2699 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1780_1_2679, all_1908_1_2896 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1908_1_2896, set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679, yields: % 99.65/62.06 | (633) all_1908_1_2896 = all_1780_1_2679 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1780_1_2679, all_1788_1_2699 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1788_1_2699, set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679, yields: % 99.65/62.06 | (634) all_1788_1_2699 = all_1780_1_2679 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1716_1_2593, all_1898_1_2877 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1898_1_2877, set_difference(all_741_5_593, all_741_4_592) = all_1716_1_2593, yields: % 99.65/62.06 | (635) all_1898_1_2877 = all_1716_1_2593 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1714_1_2588, all_2077_1_3072 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_2077_1_3072, set_difference(all_741_5_593, all_741_4_592) = all_1714_1_2588, yields: % 99.65/62.06 | (636) all_2077_1_3072 = all_1714_1_2588 % 99.65/62.06 | % 99.65/62.06 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1712_1_2583, all_1780_1_2679 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679, set_difference(all_741_5_593, all_741_4_592) = all_1712_1_2583, yields: % 99.65/62.07 | (637) all_1780_1_2679 = all_1712_1_2583 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1708_1_2573, all_741_1_589 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1708_1_2573, set_difference(all_741_5_593, all_741_4_592) = all_741_1_589, yields: % 99.65/62.07 | (638) all_1708_1_2573 = all_741_1_589 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1708_1_2573, all_1780_1_2679 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679, set_difference(all_741_5_593, all_741_4_592) = all_1708_1_2573, yields: % 99.65/62.07 | (639) all_1780_1_2679 = all_1708_1_2573 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1708_1_2573, all_1710_1_2578 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1710_1_2578, set_difference(all_741_5_593, all_741_4_592) = all_1708_1_2573, yields: % 99.65/62.07 | (640) all_1710_1_2578 = all_1708_1_2573 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1653_1_2480, all_1780_1_2679 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1780_1_2679, set_difference(all_741_5_593, all_741_4_592) = all_1653_1_2480, yields: % 99.65/62.07 | (641) all_1780_1_2679 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (105) with all_741_5_593, all_741_4_592, all_1574_1_2377, all_1710_1_2578 and discharging atoms set_difference(all_741_5_593, all_741_4_592) = all_1710_1_2578, set_difference(all_741_5_593, all_741_4_592) = all_1574_1_2377, yields: % 99.65/62.07 | (642) all_1710_1_2578 = all_1574_1_2377 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2095_2_3115, all_2105_2_3140 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2105_2_3140, set_union2(all_741_5_593, all_741_4_592) = all_2095_2_3115, yields: % 99.65/62.07 | (643) all_2105_2_3140 = all_2095_2_3115 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2089_2_3100, all_2105_2_3140 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2105_2_3140, set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100, yields: % 99.65/62.07 | (644) all_2105_2_3140 = all_2089_2_3100 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2089_2_3100, all_2099_2_3125 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2099_2_3125, set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100, yields: % 99.65/62.07 | (645) all_2099_2_3125 = all_2089_2_3100 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2087_2_3095, all_2105_2_3140 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2105_2_3140, set_union2(all_741_5_593, all_741_4_592) = all_2087_2_3095, yields: % 99.65/62.07 | (646) all_2105_2_3140 = all_2087_2_3095 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2085_2_3090, all_2099_2_3125 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2099_2_3125, set_union2(all_741_5_593, all_741_4_592) = all_2085_2_3090, yields: % 99.65/62.07 | (647) all_2099_2_3125 = all_2085_2_3090 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_2034_2_3008, all_741_3_591 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2034_2_3008, set_union2(all_741_5_593, all_741_4_592) = all_741_3_591, yields: % 99.65/62.07 | (648) all_2034_2_3008 = all_741_3_591 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_1886_2_2851, all_2089_2_3100 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100, set_union2(all_741_5_593, all_741_4_592) = all_1886_2_2851, yields: % 99.65/62.07 | (649) all_2089_2_3100 = all_1886_2_2851 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_1819_2_2757, all_1886_2_2851 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_1886_2_2851, set_union2(all_741_5_593, all_741_4_592) = all_1819_2_2757, yields: % 99.65/62.07 | (650) all_1886_2_2851 = all_1819_2_2757 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_1800_2_2730, all_2034_2_3008 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2034_2_3008, set_union2(all_741_5_593, all_741_4_592) = all_1800_2_2730, yields: % 99.65/62.07 | (651) all_2034_2_3008 = all_1800_2_2730 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_1800_2_2730, all_1819_2_2757 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_1819_2_2757, set_union2(all_741_5_593, all_741_4_592) = all_1800_2_2730, yields: % 99.65/62.07 | (652) all_1819_2_2757 = all_1800_2_2730 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (74) with all_741_5_593, all_741_4_592, all_1676_2_2527, all_2089_2_3100 and discharging atoms set_union2(all_741_5_593, all_741_4_592) = all_2089_2_3100, set_union2(all_741_5_593, all_741_4_592) = all_1676_2_2527, yields: % 99.65/62.07 | (653) all_2089_2_3100 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_4_592, all_0_11_11, 0, all_2085_3_3091 and discharging atoms in(all_741_4_592, all_0_11_11) = all_2085_3_3091, in(all_741_4_592, all_0_11_11) = 0, yields: % 99.65/62.07 | (654) all_2085_3_3091 = 0 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_4_592, all_0_13_13, all_1708_3_2575, all_2105_3_3141 and discharging atoms in(all_741_4_592, all_0_13_13) = all_2105_3_3141, in(all_741_4_592, all_0_13_13) = all_1708_3_2575, yields: % 99.65/62.07 | (655) all_2105_3_3141 = all_1708_3_2575 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_4_592, all_0_13_13, 0, all_2105_3_3141 and discharging atoms in(all_741_4_592, all_0_13_13) = all_2105_3_3141, in(all_741_4_592, all_0_13_13) = 0, yields: % 99.65/62.07 | (656) all_2105_3_3141 = 0 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_5_593, all_0_11_11, all_1710_4_2581, all_2085_4_3092 and discharging atoms in(all_741_5_593, all_0_11_11) = all_2085_4_3092, in(all_741_5_593, all_0_11_11) = all_1710_4_2581, yields: % 99.65/62.07 | (657) all_2085_4_3092 = all_1710_4_2581 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_5_593, all_0_11_11, 0, all_2085_4_3092 and discharging atoms in(all_741_5_593, all_0_11_11) = all_2085_4_3092, in(all_741_5_593, all_0_11_11) = 0, yields: % 99.65/62.07 | (658) all_2085_4_3092 = 0 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_5_593, all_0_13_13, all_1708_4_2576, all_2105_4_3142 and discharging atoms in(all_741_5_593, all_0_13_13) = all_2105_4_3142, in(all_741_5_593, all_0_13_13) = all_1708_4_2576, yields: % 99.65/62.07 | (659) all_2105_4_3142 = all_1708_4_2576 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_5_593, all_0_13_13, 0, all_2105_4_3142 and discharging atoms in(all_741_5_593, all_0_13_13) = all_2105_4_3142, in(all_741_5_593, all_0_13_13) = 0, yields: % 99.65/62.07 | (660) all_2105_4_3142 = 0 % 99.65/62.07 | % 99.65/62.07 | Combining equations (646,643) yields a new equation: % 99.65/62.07 | (661) all_2095_2_3115 = all_2087_2_3095 % 99.65/62.07 | % 99.65/62.07 | Combining equations (644,643) yields a new equation: % 99.65/62.07 | (662) all_2095_2_3115 = all_2089_2_3100 % 99.65/62.07 | % 99.65/62.07 | Combining equations (655,656) yields a new equation: % 99.65/62.07 | (663) all_1708_3_2575 = 0 % 99.65/62.07 | % 99.65/62.07 | Simplifying 663 yields: % 99.65/62.07 | (664) all_1708_3_2575 = 0 % 99.65/62.07 | % 99.65/62.07 | Combining equations (659,660) yields a new equation: % 99.65/62.07 | (665) all_1708_4_2576 = 0 % 99.65/62.07 | % 99.65/62.07 | Simplifying 665 yields: % 99.65/62.07 | (666) all_1708_4_2576 = 0 % 99.65/62.07 | % 99.65/62.07 | Combining equations (645,647) yields a new equation: % 99.65/62.07 | (667) all_2089_2_3100 = all_2085_2_3090 % 99.65/62.07 | % 99.65/62.07 | Simplifying 667 yields: % 99.65/62.07 | (668) all_2089_2_3100 = all_2085_2_3090 % 99.65/62.07 | % 99.65/62.07 | Combining equations (662,661) yields a new equation: % 99.65/62.07 | (669) all_2089_2_3100 = all_2087_2_3095 % 99.65/62.07 | % 99.65/62.07 | Simplifying 669 yields: % 99.65/62.07 | (670) all_2089_2_3100 = all_2087_2_3095 % 99.65/62.07 | % 99.65/62.07 | Combining equations (653,670) yields a new equation: % 99.65/62.07 | (671) all_2087_2_3095 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Combining equations (649,670) yields a new equation: % 99.65/62.07 | (672) all_2087_2_3095 = all_1886_2_2851 % 99.65/62.07 | % 99.65/62.07 | Combining equations (668,670) yields a new equation: % 99.65/62.07 | (673) all_2087_2_3095 = all_2085_2_3090 % 99.65/62.07 | % 99.65/62.07 | Combining equations (672,673) yields a new equation: % 99.65/62.07 | (674) all_2085_2_3090 = all_1886_2_2851 % 99.65/62.07 | % 99.65/62.07 | Combining equations (671,673) yields a new equation: % 99.65/62.07 | (675) all_2085_2_3090 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Combining equations (674,675) yields a new equation: % 99.65/62.07 | (676) all_1886_2_2851 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Simplifying 676 yields: % 99.65/62.07 | (677) all_1886_2_2851 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Combining equations (658,657) yields a new equation: % 99.65/62.07 | (678) all_1710_4_2581 = 0 % 99.65/62.07 | % 99.65/62.07 | Combining equations (631,636) yields a new equation: % 99.65/62.07 | (679) all_1908_1_2896 = all_1714_1_2588 % 99.65/62.07 | % 99.65/62.07 | Simplifying 679 yields: % 99.65/62.07 | (680) all_1908_1_2896 = all_1714_1_2588 % 99.65/62.07 | % 99.65/62.07 | Combining equations (651,648) yields a new equation: % 99.65/62.07 | (681) all_1800_2_2730 = all_741_3_591 % 99.65/62.07 | % 99.65/62.07 | Simplifying 681 yields: % 99.65/62.07 | (682) all_1800_2_2730 = all_741_3_591 % 99.65/62.07 | % 99.65/62.07 | Combining equations (633,680) yields a new equation: % 99.65/62.07 | (683) all_1780_1_2679 = all_1714_1_2588 % 99.65/62.07 | % 99.65/62.07 | Simplifying 683 yields: % 99.65/62.07 | (684) all_1780_1_2679 = all_1714_1_2588 % 99.65/62.07 | % 99.65/62.07 | Combining equations (632,635) yields a new equation: % 99.65/62.07 | (685) all_1788_1_2699 = all_1716_1_2593 % 99.65/62.07 | % 99.65/62.07 | Simplifying 685 yields: % 99.65/62.07 | (686) all_1788_1_2699 = all_1716_1_2593 % 99.65/62.07 | % 99.65/62.07 | Combining equations (650,677) yields a new equation: % 99.65/62.07 | (687) all_1819_2_2757 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Simplifying 687 yields: % 99.65/62.07 | (688) all_1819_2_2757 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Combining equations (652,688) yields a new equation: % 99.65/62.07 | (689) all_1800_2_2730 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Simplifying 689 yields: % 99.65/62.07 | (690) all_1800_2_2730 = all_1676_2_2527 % 99.65/62.07 | % 99.65/62.07 | Combining equations (682,690) yields a new equation: % 99.65/62.07 | (691) all_1676_2_2527 = all_741_3_591 % 99.65/62.07 | % 99.65/62.07 | Combining equations (634,686) yields a new equation: % 99.65/62.07 | (692) all_1780_1_2679 = all_1716_1_2593 % 99.65/62.07 | % 99.65/62.07 | Simplifying 692 yields: % 99.65/62.07 | (693) all_1780_1_2679 = all_1716_1_2593 % 99.65/62.07 | % 99.65/62.07 | Combining equations (639,693) yields a new equation: % 99.65/62.07 | (694) all_1716_1_2593 = all_1708_1_2573 % 99.65/62.07 | % 99.65/62.07 | Combining equations (684,693) yields a new equation: % 99.65/62.07 | (695) all_1716_1_2593 = all_1714_1_2588 % 99.65/62.07 | % 99.65/62.07 | Combining equations (641,693) yields a new equation: % 99.65/62.07 | (696) all_1716_1_2593 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Combining equations (637,693) yields a new equation: % 99.65/62.07 | (697) all_1716_1_2593 = all_1712_1_2583 % 99.65/62.07 | % 99.65/62.07 | Combining equations (697,695) yields a new equation: % 99.65/62.07 | (698) all_1714_1_2588 = all_1712_1_2583 % 99.65/62.07 | % 99.65/62.07 | Combining equations (696,695) yields a new equation: % 99.65/62.07 | (699) all_1714_1_2588 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Combining equations (694,695) yields a new equation: % 99.65/62.07 | (700) all_1714_1_2588 = all_1708_1_2573 % 99.65/62.07 | % 99.65/62.07 | Combining equations (700,698) yields a new equation: % 99.65/62.07 | (701) all_1712_1_2583 = all_1708_1_2573 % 99.65/62.07 | % 99.65/62.07 | Combining equations (699,698) yields a new equation: % 99.65/62.07 | (702) all_1712_1_2583 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Combining equations (701,702) yields a new equation: % 99.65/62.07 | (703) all_1708_1_2573 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Simplifying 703 yields: % 99.65/62.07 | (704) all_1708_1_2573 = all_1653_1_2480 % 99.65/62.07 | % 99.65/62.07 | Combining equations (640,642) yields a new equation: % 99.65/62.07 | (705) all_1708_1_2573 = all_1574_1_2377 % 99.65/62.07 | % 99.65/62.07 | Simplifying 705 yields: % 99.65/62.07 | (706) all_1708_1_2573 = all_1574_1_2377 % 99.65/62.07 | % 99.65/62.07 | Combining equations (638,704) yields a new equation: % 99.65/62.07 | (707) all_1653_1_2480 = all_741_1_589 % 99.65/62.07 | % 99.65/62.07 | Combining equations (706,704) yields a new equation: % 99.65/62.07 | (708) all_1653_1_2480 = all_1574_1_2377 % 99.65/62.07 | % 99.65/62.07 | Combining equations (707,708) yields a new equation: % 99.65/62.07 | (709) all_1574_1_2377 = all_741_1_589 % 99.65/62.07 | % 99.65/62.07 | Combining equations (709,708) yields a new equation: % 99.65/62.07 | (707) all_1653_1_2480 = all_741_1_589 % 99.65/62.07 | % 99.65/62.07 | Combining equations (707,704) yields a new equation: % 99.65/62.07 | (638) all_1708_1_2573 = all_741_1_589 % 99.65/62.07 | % 99.65/62.07 | Combining equations (678,657) yields a new equation: % 99.65/62.07 | (658) all_2085_4_3092 = 0 % 99.65/62.07 | % 99.65/62.07 | Combining equations (691,675) yields a new equation: % 99.65/62.07 | (713) all_2085_2_3090 = all_741_3_591 % 99.65/62.07 | % 99.65/62.07 | From (713) and (591) follows: % 99.65/62.07 | (714) in(all_741_3_591, all_0_11_11) = all_2085_1_3089 % 99.65/62.07 | % 99.65/62.07 | From (638) and (492) follows: % 99.65/62.07 | (715) in(all_741_1_589, all_0_13_13) = all_1708_0_2572 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (494), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (716) ~ (all_1708_3_2575 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (664) can reduce 716 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (664) all_1708_3_2575 = 0 % 99.65/62.07 | (719) ~ (all_1708_4_2576 = 0) | (all_1708_0_2572 = 0 & all_1708_2_2574 = 0) % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (719), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (720) ~ (all_1708_4_2576 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (666) can reduce 720 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (666) all_1708_4_2576 = 0 % 99.65/62.07 | (723) all_1708_0_2572 = 0 & all_1708_2_2574 = 0 % 99.65/62.07 | % 99.65/62.07 | Applying alpha-rule on (723) yields: % 99.65/62.07 | (724) all_1708_0_2572 = 0 % 99.65/62.07 | (725) all_1708_2_2574 = 0 % 99.65/62.07 | % 99.65/62.07 | From (724) and (715) follows: % 99.65/62.07 | (726) in(all_741_1_589, all_0_13_13) = 0 % 99.65/62.07 | % 99.65/62.07 | From (725) and (493) follows: % 99.65/62.07 | (727) in(all_741_3_591, all_0_13_13) = 0 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (590), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (728) ~ (all_2085_3_3091 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (654) can reduce 728 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (654) all_2085_3_3091 = 0 % 99.65/62.07 | (731) ~ (all_2085_4_3092 = 0) | (all_2085_0_3088 = 0 & all_2085_1_3089 = 0) % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (731), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (732) ~ (all_2085_4_3092 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (658) can reduce 732 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (658) all_2085_4_3092 = 0 % 99.65/62.07 | (735) all_2085_0_3088 = 0 & all_2085_1_3089 = 0 % 99.65/62.07 | % 99.65/62.07 | Applying alpha-rule on (735) yields: % 99.65/62.07 | (736) all_2085_0_3088 = 0 % 99.65/62.07 | (737) all_2085_1_3089 = 0 % 99.65/62.07 | % 99.65/62.07 | From (736) and (592) follows: % 99.65/62.07 | (738) in(all_741_1_589, all_0_11_11) = 0 % 99.65/62.07 | % 99.65/62.07 | From (737) and (714) follows: % 99.65/62.07 | (739) in(all_741_3_591, all_0_11_11) = 0 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (463), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (740) all_741_2_590 = 0 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (462), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (741) all_741_0_588 = 0 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (432), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (742) ~ (all_741_0_588 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (741) can reduce 742 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (741) all_741_0_588 = 0 % 99.65/62.07 | (745) ~ (all_741_2_590 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (740) can reduce 745 to: % 99.65/62.07 | (200) $false % 99.65/62.07 | % 99.65/62.07 |-The branch is then unsatisfiable % 99.65/62.07 |-Branch two: % 99.65/62.07 | (742) ~ (all_741_0_588 = 0) % 99.65/62.07 | (748) ? [v0] : ? [v1] : (in(all_741_1_589, all_0_11_11) = v1 & in(all_741_1_589, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 99.65/62.07 | % 99.65/62.07 | Instantiating (748) with all_3843_0_3581, all_3843_1_3582 yields: % 99.65/62.07 | (749) in(all_741_1_589, all_0_11_11) = all_3843_0_3581 & in(all_741_1_589, all_0_13_13) = all_3843_1_3582 & ( ~ (all_3843_0_3581 = 0) | ~ (all_3843_1_3582 = 0)) % 99.65/62.07 | % 99.65/62.07 | Applying alpha-rule on (749) yields: % 99.65/62.07 | (750) in(all_741_1_589, all_0_11_11) = all_3843_0_3581 % 99.65/62.07 | (751) in(all_741_1_589, all_0_13_13) = all_3843_1_3582 % 99.65/62.07 | (752) ~ (all_3843_0_3581 = 0) | ~ (all_3843_1_3582 = 0) % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_1_589, all_0_11_11, 0, all_3843_0_3581 and discharging atoms in(all_741_1_589, all_0_11_11) = all_3843_0_3581, in(all_741_1_589, all_0_11_11) = 0, yields: % 99.65/62.07 | (753) all_3843_0_3581 = 0 % 99.65/62.07 | % 99.65/62.07 | Instantiating formula (28) with all_741_1_589, all_0_13_13, 0, all_3843_1_3582 and discharging atoms in(all_741_1_589, all_0_13_13) = all_3843_1_3582, in(all_741_1_589, all_0_13_13) = 0, yields: % 99.65/62.07 | (754) all_3843_1_3582 = 0 % 99.65/62.07 | % 99.65/62.07 +-Applying beta-rule and splitting (752), into two cases. % 99.65/62.07 |-Branch one: % 99.65/62.07 | (755) ~ (all_3843_0_3581 = 0) % 99.65/62.07 | % 99.65/62.07 | Equations (753) can reduce 755 to: % 99.65/62.07 | (200) $false % 99.65/62.08 | % 99.65/62.08 |-The branch is then unsatisfiable % 99.65/62.08 |-Branch two: % 99.65/62.08 | (753) all_3843_0_3581 = 0 % 99.65/62.08 | (758) ~ (all_3843_1_3582 = 0) % 99.65/62.08 | % 99.65/62.08 | Equations (754) can reduce 758 to: % 99.65/62.08 | (200) $false % 99.65/62.08 | % 99.65/62.08 |-The branch is then unsatisfiable % 99.65/62.08 |-Branch two: % 99.65/62.08 | (745) ~ (all_741_2_590 = 0) % 99.65/62.08 | (761) ? [v0] : ? [v1] : (in(all_741_3_591, all_0_11_11) = v1 & in(all_741_3_591, all_0_13_13) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 99.65/62.08 | % 99.65/62.08 | Instantiating (761) with all_3839_0_3583, all_3839_1_3584 yields: % 99.65/62.08 | (762) in(all_741_3_591, all_0_11_11) = all_3839_0_3583 & in(all_741_3_591, all_0_13_13) = all_3839_1_3584 & ( ~ (all_3839_0_3583 = 0) | ~ (all_3839_1_3584 = 0)) % 99.65/62.08 | % 99.65/62.08 | Applying alpha-rule on (762) yields: % 99.65/62.08 | (763) in(all_741_3_591, all_0_11_11) = all_3839_0_3583 % 99.65/62.08 | (764) in(all_741_3_591, all_0_13_13) = all_3839_1_3584 % 99.65/62.08 | (765) ~ (all_3839_0_3583 = 0) | ~ (all_3839_1_3584 = 0) % 99.65/62.08 | % 99.65/62.08 | Instantiating formula (28) with all_741_3_591, all_0_11_11, 0, all_3839_0_3583 and discharging atoms in(all_741_3_591, all_0_11_11) = all_3839_0_3583, in(all_741_3_591, all_0_11_11) = 0, yields: % 99.65/62.08 | (766) all_3839_0_3583 = 0 % 99.65/62.08 | % 99.65/62.08 | Instantiating formula (28) with all_741_3_591, all_0_13_13, 0, all_3839_1_3584 and discharging atoms in(all_741_3_591, all_0_13_13) = all_3839_1_3584, in(all_741_3_591, all_0_13_13) = 0, yields: % 99.65/62.08 | (767) all_3839_1_3584 = 0 % 99.65/62.08 | % 99.65/62.08 +-Applying beta-rule and splitting (765), into two cases. % 99.65/62.08 |-Branch one: % 99.65/62.08 | (768) ~ (all_3839_0_3583 = 0) % 99.65/62.08 | % 99.65/62.08 | Equations (766) can reduce 768 to: % 99.65/62.08 | (200) $false % 99.65/62.08 | % 99.65/62.08 |-The branch is then unsatisfiable % 99.65/62.08 |-Branch two: % 99.65/62.08 | (766) all_3839_0_3583 = 0 % 99.65/62.08 | (771) ~ (all_3839_1_3584 = 0) % 99.65/62.08 | % 99.65/62.08 | Equations (767) can reduce 771 to: % 99.65/62.08 | (200) $false % 99.65/62.08 | % 99.65/62.08 |-The branch is then unsatisfiable % 99.65/62.08 |-Branch two: % 99.65/62.08 | (427) all_0_7_7 = 0 % 99.65/62.08 | (774) all_0_8_8 = 0 % 99.65/62.08 | % 99.65/62.08 | From (774) and (111) follows: % 99.65/62.08 | (775) empty(all_0_9_9) = 0 % 99.65/62.08 | % 99.65/62.08 | Instantiating formula (55) with all_0_9_9 and discharging atoms empty(all_0_9_9) = 0, yields: % 99.65/62.08 | (776) all_0_9_9 = empty_set % 99.65/62.08 | % 99.65/62.08 | From (776) and (425) follows: % 99.65/62.08 | (777) in(empty_set, empty_set) = 0 % 99.65/62.08 | % 99.65/62.08 | Instantiating formula (42) with empty_set, empty_set and discharging atoms in(empty_set, empty_set) = 0, yields: % 99.65/62.08 | (778) ? [v0] : ( ~ (v0 = 0) & in(empty_set, empty_set) = v0) % 99.65/62.08 | % 99.65/62.08 | Instantiating (778) with all_1532_0_3924 yields: % 99.65/62.08 | (779) ~ (all_1532_0_3924 = 0) & in(empty_set, empty_set) = all_1532_0_3924 % 99.65/62.08 | % 99.65/62.08 | Applying alpha-rule on (779) yields: % 99.65/62.08 | (780) ~ (all_1532_0_3924 = 0) % 99.65/62.08 | (781) in(empty_set, empty_set) = all_1532_0_3924 % 99.65/62.08 | % 99.65/62.08 | Instantiating formula (28) with empty_set, empty_set, all_1532_0_3924, 0 and discharging atoms in(empty_set, empty_set) = all_1532_0_3924, in(empty_set, empty_set) = 0, yields: % 99.65/62.08 | (782) all_1532_0_3924 = 0 % 99.65/62.08 | % 99.65/62.08 | Equations (782) can reduce 780 to: % 99.65/62.08 | (200) $false % 99.65/62.08 | % 99.65/62.08 |-The branch is then unsatisfiable % 99.65/62.08 % SZS output end Proof for theBenchmark % 99.65/62.08 % 99.65/62.08 61472ms %------------------------------------------------------------------------------