%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV549+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Apr 1 02:01:01 AM UTC 2025 % Result : Theorem 26.89s 7.01s % Output : Proof 30.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV549+1 : TPTP v9.1.0. Released v9.1.0. % 0.00/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Mar 31 11:47:13 EDT 2025 % 0.12/0.33 % CPUTime : % 0.60/0.58 ____ _ % 0.60/0.58 ___ / __ \_____(_)___ ________ __________ % 0.60/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.60/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.60/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.60/0.59 % 0.60/0.59 A Theorem Prover for First-Order Logic % 0.60/0.59 (ePrincess v.1.0) % 0.60/0.59 % 0.60/0.59 (c) Philipp Rümmer, 2009-2015 % 0.60/0.59 (c) Peter Backeman, 2014-2015 % 0.60/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.60/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.60/0.59 Bug reports to peter@backeman.se % 0.60/0.59 % 0.60/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.60/0.59 % 0.60/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.73/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.72/0.93 Prover 0: Preprocessing ... % 2.39/1.19 Prover 0: Warning: ignoring some quantifiers % 2.50/1.21 Prover 0: Constructing countermodel ... % 22.09/5.93 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 22.09/5.96 Prover 1: Preprocessing ... % 22.98/6.11 Prover 1: Constructing countermodel ... % 24.78/6.56 Prover 1: gave up % 24.78/6.56 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 24.78/6.58 Prover 2: Preprocessing ... % 25.58/6.70 Prover 2: Warning: ignoring some quantifiers % 25.58/6.70 Prover 2: Constructing countermodel ... % 26.89/7.01 Prover 2: proved (452ms) % 26.89/7.01 Prover 0: stopped % 26.89/7.01 % 26.89/7.01 No countermodel exists, formula is valid % 26.89/7.01 % SZS status Theorem for theBenchmark % 26.89/7.01 % 26.89/7.01 Generating proof ... Warning: ignoring some quantifiers % 29.41/7.59 found it (size 373) % 29.41/7.59 % 29.41/7.59 % SZS output start Proof for theBenchmark % 29.41/7.59 Assumed formulas after preprocessing and simplification: % 29.41/7.59 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (atleast4p(v6) = 0 & n(v4) = v5 & n(v0) = v1 & n(e) = v0 & u(v2, v5) = v6 & s(v3) = v4 & s(v1) = v2 & s(v0) = v3 & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (m(v8, v9) = v10) | ~ (mem(v7, v10) = v11) | ? [v12] : ((v12 = 0 & mem(v7, v9) = 0) | ( ~ (v12 = 0) & mem(v7, v8) = v12))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (u(v8, v9) = v10) | ~ (mem(v7, v10) = v11) | ? [v12] : ? [v13] : ( ~ (v13 = 0) & ~ (v12 = 0) & mem(v7, v9) = v13 & mem(v7, v8) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast16p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast15p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast15p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast14p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast14p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast13p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast13p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast12p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast12p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast11p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast11p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast10p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast10p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast9p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast9p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast8p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast8p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast7p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast7p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast6p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast6p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast5p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast5p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast4p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast4p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast3p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | v8 = 0 | ~ (atleast3p(v7) = v8) | ~ (subq(v7, v9) = v10) | ? [v11] : (( ~ (v11 = 0) & atleast2p(v9) = v11) | ( ~ (v11 = 0) & subq(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (p(v8) = v9) | ~ (mem(v7, v9) = v10) | ? [v11] : ( ~ (v11 = 0) & subq(v7, v8) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (subq(v7, v8) = 0) | ~ (mem(v9, v8) = v10) | ? [v11] : ( ~ (v11 = 0) & mem(v9, v7) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (a(v10, v9) = v8) | ~ (a(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (m(v10, v9) = v8) | ~ (m(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (u(v10, v9) = v8) | ~ (u(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (disj(v10, v9) = v8) | ~ (disj(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (subq(v10, v9) = v8) | ~ (subq(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (mem(v10, v9) = v8) | ~ (mem(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = 0 | ~ (atleast2p(v7) = v8) | ~ (p(v9) = v10) | ? [v11] : ((v11 = 0 & subq(v7, v10) = 0) | ( ~ (v11 = 0) & mem(v9, v7) = v11))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (m(v8, v9) = v10) | ~ (mem(v7, v10) = 0) | ? [v11] : ( ~ (v11 = 0) & mem(v7, v9) = v11 & mem(v7, v8) = 0)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (u(v8, v9) = v10) | ~ (mem(v7, v10) = 0) | ? [v11] : ((v11 = 0 & mem(v7, v9) = 0) | (v11 = 0 & mem(v7, v8) = 0))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (u(v7, v9) = v10) | ~ (s(v8) = v9) | a(v7, v8) = v10) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (s(v7) = v8) | ~ (mem(v7, v8) = v9)) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (disj(v7, v8) = v9) | ? [v10] : (mem(v10, v8) = 0 & mem(v10, v7) = 0)) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (subq(v7, v8) = v9) | ? [v10] : ? [v11] : ( ~ (v11 = 0) & p(v8) = v10 & mem(v7, v10) = v11)) & ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (subq(v7, v8) = v9) | ? [v10] : ? [v11] : ( ~ (v11 = 0) & mem(v10, v8) = v11 & mem(v10, v7) = 0)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast16p(v9) = v8) | ~ (atleast16p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast15p(v9) = v8) | ~ (atleast15p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast14p(v9) = v8) | ~ (atleast14p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast13p(v9) = v8) | ~ (atleast13p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast12p(v9) = v8) | ~ (atleast12p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast11p(v9) = v8) | ~ (atleast11p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast10p(v9) = v8) | ~ (atleast10p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast9p(v9) = v8) | ~ (atleast9p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast8p(v9) = v8) | ~ (atleast8p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast7p(v9) = v8) | ~ (atleast7p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast6p(v9) = v8) | ~ (atleast6p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast5p(v9) = v8) | ~ (atleast5p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast4p(v9) = v8) | ~ (atleast4p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast3p(v9) = v8) | ~ (atleast3p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (atleast2p(v9) = v8) | ~ (atleast2p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (p(v9) = v8) | ~ (p(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (n(v9) = v8) | ~ (n(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (s(v9) = v8) | ~ (s(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (s(v8) = v9) | ~ (mem(v7, v9) = 0)) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast16p(v7) = v8) | ~ (atleast15p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast16p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast15p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast15p(v7) = v8) | ~ (atleast14p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast15p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast14p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast14p(v7) = v8) | ~ (atleast13p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast14p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast13p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast13p(v7) = v8) | ~ (atleast12p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast13p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast12p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast12p(v7) = v8) | ~ (atleast11p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast12p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast11p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast11p(v7) = v8) | ~ (atleast10p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast11p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast10p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast10p(v7) = v8) | ~ (atleast9p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast10p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast9p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast9p(v7) = v8) | ~ (atleast8p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast9p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast8p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast8p(v7) = v8) | ~ (atleast7p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast8p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast7p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast7p(v7) = v8) | ~ (atleast6p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast7p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast6p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast6p(v7) = v8) | ~ (atleast5p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast6p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast5p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast5p(v7) = v8) | ~ (atleast4p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast5p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast4p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast4p(v7) = v8) | ~ (atleast3p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast4p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast3p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast3p(v7) = v8) | ~ (atleast2p(v9) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & subq(v9, v7) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast3p(v7) = v8) | ~ (subq(v9, v7) = 0) | ? [v10] : ((v10 = 0 & subq(v7, v9) = 0) | ( ~ (v10 = 0) & atleast2p(v9) = v10))) & ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (atleast2p(v7) = v8) | ~ (mem(v9, v7) = 0) | ? [v10] : (p(v9) = v10 & subq(v7, v10) = 0)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (p(v8) = v9) | ~ (mem(v7, v9) = 0) | subq(v7, v8) = 0) & ! [v7] : ! [v8] : ! [v9] : ( ~ (a(v7, v8) = v9) | ? [v10] : (u(v7, v10) = v9 & s(v8) = v10)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (disj(v7, v8) = 0) | ~ (mem(v9, v8) = 0) | ? [v10] : ( ~ (v10 = 0) & mem(v9, v7) = v10)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (disj(v7, v8) = 0) | ~ (mem(v9, v7) = 0) | ? [v10] : ( ~ (v10 = 0) & mem(v9, v8) = v10)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (subq(v7, v8) = 0) | ~ (mem(v9, v7) = 0) | mem(v9, v8) = 0) & ! [v7] : ! [v8] : (v8 = v7 | ~ (subq(v8, v7) = 0) | ? [v9] : ( ~ (v9 = 0) & subq(v7, v8) = v9)) & ! [v7] : ! [v8] : (v8 = v7 | ~ (subq(v7, v8) = 0) | ? [v9] : ( ~ (v9 = 0) & subq(v8, v7) = v9)) & ! [v7] : ! [v8] : ( ~ (n(v7) = v8) | a(v7, v7) = v8) & ! [v7] : ! [v8] : ( ~ (a(v7, v7) = v8) | n(v7) = v8) & ! [v7] : ! [v8] : ( ~ (subq(v7, v8) = 0) | ? [v9] : (p(v8) = v9 & mem(v7, v9) = 0)) & ! [v7] : ( ~ (atleast16p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast15p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast15p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast14p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast14p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast13p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast13p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast12p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast12p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast11p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast11p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast10p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast10p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast9p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast9p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast8p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast8p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast7p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast7p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast6p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast6p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast5p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast5p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast4p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast4p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast3p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast3p(v7) = 0) | ? [v8] : ? [v9] : ( ~ (v9 = 0) & atleast2p(v8) = 0 & subq(v8, v7) = 0 & subq(v7, v8) = v9)) & ! [v7] : ( ~ (atleast2p(v7) = 0) | ? [v8] : ? [v9] : ? [v10] : ( ~ (v10 = 0) & p(v8) = v9 & subq(v7, v9) = v10 & mem(v8, v7) = 0)) & ! [v7] : ~ (mem(v7, e) = 0) & ? [v7] : ? [v8] : ? [v9] : a(v8, v7) = v9 & ? [v7] : ? [v8] : ? [v9] : m(v8, v7) = v9 & ? [v7] : ? [v8] : ? [v9] : u(v8, v7) = v9 & ? [v7] : ? [v8] : ? [v9] : disj(v8, v7) = v9 & ? [v7] : ? [v8] : ? [v9] : subq(v8, v7) = v9 & ? [v7] : ? [v8] : ? [v9] : mem(v8, v7) = v9 & ? [v7] : ? [v8] : atleast16p(v7) = v8 & ? [v7] : ? [v8] : atleast15p(v7) = v8 & ? [v7] : ? [v8] : atleast14p(v7) = v8 & ? [v7] : ? [v8] : atleast13p(v7) = v8 & ? [v7] : ? [v8] : atleast12p(v7) = v8 & ? [v7] : ? [v8] : atleast11p(v7) = v8 & ? [v7] : ? [v8] : atleast10p(v7) = v8 & ? [v7] : ? [v8] : atleast9p(v7) = v8 & ? [v7] : ? [v8] : atleast8p(v7) = v8 & ? [v7] : ? [v8] : atleast7p(v7) = v8 & ? [v7] : ? [v8] : atleast6p(v7) = v8 & ? [v7] : ? [v8] : atleast5p(v7) = v8 & ? [v7] : ? [v8] : atleast4p(v7) = v8 & ? [v7] : ? [v8] : atleast3p(v7) = v8 & ? [v7] : ? [v8] : atleast2p(v7) = v8 & ? [v7] : ? [v8] : p(v7) = v8 & ? [v7] : ? [v8] : n(v7) = v8 & ? [v7] : ? [v8] : s(v7) = v8) % 29.69/7.65 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 yields: % 29.69/7.65 | (1) atleast4p(all_0_0_0) = 0 & n(all_0_2_2) = all_0_1_1 & n(all_0_6_6) = all_0_5_5 & n(e) = all_0_6_6 & u(all_0_4_4, all_0_1_1) = all_0_0_0 & s(all_0_3_3) = all_0_2_2 & s(all_0_5_5) = all_0_4_4 & s(all_0_6_6) = all_0_3_3 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ((v5 = 0 & mem(v0, v2) = 0) | ( ~ (v5 = 0) & mem(v0, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & ~ (v5 = 0) & mem(v0, v2) = v6 & mem(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast15p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast14p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast13p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast12p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast11p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast10p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast9p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast8p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast7p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast6p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast5p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast4p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast3p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast2p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ? [v4] : ((v4 = 0 & subq(v0, v3) = 0) | ( ~ (v4 = 0) & mem(v2, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ((v4 = 0 & mem(v0, v2) = 0) | (v4 = 0 & mem(v0, v1) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) & ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) & ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) & ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) & ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) & ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) & ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) & ! [v0] : ~ (mem(v0, e) = 0) & ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 & ? [v0] : ? [v1] : atleast16p(v0) = v1 & ? [v0] : ? [v1] : atleast15p(v0) = v1 & ? [v0] : ? [v1] : atleast14p(v0) = v1 & ? [v0] : ? [v1] : atleast13p(v0) = v1 & ? [v0] : ? [v1] : atleast12p(v0) = v1 & ? [v0] : ? [v1] : atleast11p(v0) = v1 & ? [v0] : ? [v1] : atleast10p(v0) = v1 & ? [v0] : ? [v1] : atleast9p(v0) = v1 & ? [v0] : ? [v1] : atleast8p(v0) = v1 & ? [v0] : ? [v1] : atleast7p(v0) = v1 & ? [v0] : ? [v1] : atleast6p(v0) = v1 & ? [v0] : ? [v1] : atleast5p(v0) = v1 & ? [v0] : ? [v1] : atleast4p(v0) = v1 & ? [v0] : ? [v1] : atleast3p(v0) = v1 & ? [v0] : ? [v1] : atleast2p(v0) = v1 & ? [v0] : ? [v1] : p(v0) = v1 & ? [v0] : ? [v1] : n(v0) = v1 & ? [v0] : ? [v1] : s(v0) = v1 % 29.69/7.67 | % 29.69/7.67 | Applying alpha-rule on (1) yields: % 29.69/7.67 | (2) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.67 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 29.69/7.68 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 29.69/7.68 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 29.69/7.68 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 29.69/7.68 | (7) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 29.69/7.68 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 29.69/7.68 | (9) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.68 | (10) u(all_0_4_4, all_0_1_1) = all_0_0_0 % 29.69/7.68 | (11) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 29.69/7.68 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 29.69/7.68 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 29.69/7.68 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 29.69/7.68 | (15) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 29.69/7.68 | (16) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 29.69/7.68 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 29.69/7.68 | (18) n(all_0_6_6) = all_0_5_5 % 29.69/7.68 | (19) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.68 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.68 | (21) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 29.69/7.68 | (22) s(all_0_5_5) = all_0_4_4 % 29.69/7.68 | (23) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 29.69/7.68 | (24) n(e) = all_0_6_6 % 29.69/7.68 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 29.69/7.68 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.68 | (27) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 29.69/7.68 | (28) s(all_0_6_6) = all_0_3_3 % 29.69/7.68 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.68 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 29.69/7.68 | (31) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.68 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.68 | (33) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 29.69/7.68 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast9p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.68 | (35) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 29.69/7.68 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 29.69/7.68 | (37) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.68 | (38) atleast4p(all_0_0_0) = 0 % 29.69/7.68 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.68 | (40) n(all_0_2_2) = all_0_1_1 % 29.69/7.68 | (41) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 29.69/7.68 | (42) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 29.69/7.69 | (43) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 29.69/7.69 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 29.69/7.69 | (45) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 29.69/7.69 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast8p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.69 | (47) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 29.69/7.69 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 29.69/7.69 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ((v5 = 0 & mem(v0, v2) = 0) | ( ~ (v5 = 0) & mem(v0, v1) = v5))) % 29.69/7.69 | (50) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.69 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 29.69/7.69 | (52) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 29.69/7.69 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast4p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.69 | (54) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.69 | (55) ? [v0] : ? [v1] : s(v0) = v1 % 29.69/7.69 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.69 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast6p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.69 | (58) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 29.69/7.69 | (59) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 29.69/7.69 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.69 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast7p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.69 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 29.69/7.69 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.69 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ? [v4] : ((v4 = 0 & subq(v0, v3) = 0) | ( ~ (v4 = 0) & mem(v2, v0) = v4))) % 29.69/7.69 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 29.69/7.69 | (66) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 29.69/7.69 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast13p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.69 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 29.69/7.69 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & ~ (v5 = 0) & mem(v0, v2) = v6 & mem(v0, v1) = v5)) % 29.69/7.69 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 29.69/7.69 | (71) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 29.69/7.69 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ((v4 = 0 & mem(v0, v2) = 0) | (v4 = 0 & mem(v0, v1) = 0))) % 29.69/7.69 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 29.69/7.69 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 29.69/7.70 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 29.69/7.70 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 29.69/7.70 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast3p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (78) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 29.69/7.70 | (79) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 29.69/7.70 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast15p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (81) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.70 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 29.69/7.70 | (83) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 29.69/7.70 | (84) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast10p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (85) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.70 | (86) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.70 | (87) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 29.69/7.70 | (88) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast5p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (89) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 29.69/7.70 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 29.69/7.70 | (91) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.70 | (92) s(all_0_3_3) = all_0_2_2 % 29.69/7.70 | (93) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 29.69/7.70 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.70 | (95) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 29.69/7.70 | (96) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 29.69/7.70 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.70 | (98) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.70 | (99) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 29.69/7.70 | (100) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 29.69/7.70 | (101) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 29.69/7.70 | (102) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 29.69/7.70 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast12p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (104) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 29.69/7.70 | (105) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 29.69/7.70 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast14p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.70 | (107) ! [v0] : ~ (mem(v0, e) = 0) % 29.69/7.70 | (108) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 29.69/7.70 | (109) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 29.69/7.71 | (110) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.71 | (111) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 29.69/7.71 | (112) ? [v0] : ? [v1] : p(v0) = v1 % 29.69/7.71 | (113) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 29.69/7.71 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast2p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.71 | (115) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 29.69/7.71 | (116) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.71 | (117) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 29.69/7.71 | (118) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.71 | (119) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 29.69/7.71 | (120) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 29.69/7.71 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.71 | (122) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 29.69/7.71 | (123) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 29.69/7.71 | (124) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 29.69/7.71 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 29.69/7.71 | (126) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 29.69/7.71 | (127) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 29.69/7.71 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 29.69/7.71 | (129) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 29.69/7.71 | (130) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 29.69/7.71 | (131) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.69/7.71 | (132) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 29.69/7.71 | (133) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 29.69/7.71 | (134) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 29.69/7.71 | (135) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 29.69/7.71 | (136) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast11p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 29.69/7.71 | (137) ? [v0] : ? [v1] : n(v0) = v1 % 29.69/7.71 | (138) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 29.69/7.71 | (139) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 29.69/7.71 | % 29.69/7.71 | Instantiating formula (86) with all_0_0_0 and discharging atoms atleast4p(all_0_0_0) = 0, yields: % 29.69/7.71 | (140) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast3p(v0) = 0 & subq(v0, all_0_0_0) = 0 & subq(all_0_0_0, v0) = v1) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (16) with all_0_1_1, all_0_2_2 and discharging atoms n(all_0_2_2) = all_0_1_1, yields: % 29.69/7.72 | (141) a(all_0_2_2, all_0_2_2) = all_0_1_1 % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (16) with all_0_5_5, all_0_6_6 and discharging atoms n(all_0_6_6) = all_0_5_5, yields: % 29.69/7.72 | (142) a(all_0_6_6, all_0_6_6) = all_0_5_5 % 29.69/7.72 | % 29.69/7.72 | Instantiating (140) with all_57_0_61, all_57_1_62 yields: % 29.69/7.72 | (143) ~ (all_57_0_61 = 0) & atleast3p(all_57_1_62) = 0 & subq(all_57_1_62, all_0_0_0) = 0 & subq(all_0_0_0, all_57_1_62) = all_57_0_61 % 29.69/7.72 | % 29.69/7.72 | Applying alpha-rule on (143) yields: % 29.69/7.72 | (144) ~ (all_57_0_61 = 0) % 29.69/7.72 | (145) atleast3p(all_57_1_62) = 0 % 29.69/7.72 | (146) subq(all_57_1_62, all_0_0_0) = 0 % 29.69/7.72 | (147) subq(all_0_0_0, all_57_1_62) = all_57_0_61 % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (19) with all_57_1_62 and discharging atoms atleast3p(all_57_1_62) = 0, yields: % 29.69/7.72 | (148) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast2p(v0) = 0 & subq(v0, all_57_1_62) = 0 & subq(all_57_1_62, v0) = v1) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (124) with all_0_1_1, all_0_2_2, all_0_2_2 and discharging atoms a(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 29.69/7.72 | (149) ? [v0] : (u(all_0_2_2, v0) = all_0_1_1 & s(all_0_2_2) = v0) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (124) with all_0_5_5, all_0_6_6, all_0_6_6 and discharging atoms a(all_0_6_6, all_0_6_6) = all_0_5_5, yields: % 29.69/7.72 | (150) ? [v0] : (u(all_0_6_6, v0) = all_0_5_5 & s(all_0_6_6) = v0) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (58) with all_57_0_61, all_57_1_62, all_0_0_0 and discharging atoms subq(all_0_0_0, all_57_1_62) = all_57_0_61, yields: % 29.69/7.72 | (151) all_57_0_61 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_57_1_62) = v0 & mem(all_0_0_0, v0) = v1) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (45) with all_57_0_61, all_57_1_62, all_0_0_0 and discharging atoms subq(all_0_0_0, all_57_1_62) = all_57_0_61, yields: % 29.69/7.72 | (152) all_57_0_61 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_57_1_62) = v1 & mem(v0, all_0_0_0) = 0) % 29.69/7.72 | % 29.69/7.72 | Instantiating (150) with all_68_0_65 yields: % 29.69/7.72 | (153) u(all_0_6_6, all_68_0_65) = all_0_5_5 & s(all_0_6_6) = all_68_0_65 % 29.69/7.72 | % 29.69/7.72 | Applying alpha-rule on (153) yields: % 29.69/7.72 | (154) u(all_0_6_6, all_68_0_65) = all_0_5_5 % 29.69/7.72 | (155) s(all_0_6_6) = all_68_0_65 % 29.69/7.72 | % 29.69/7.72 | Instantiating (149) with all_70_0_66 yields: % 29.69/7.72 | (156) u(all_0_2_2, all_70_0_66) = all_0_1_1 & s(all_0_2_2) = all_70_0_66 % 29.69/7.72 | % 29.69/7.72 | Applying alpha-rule on (156) yields: % 29.69/7.72 | (157) u(all_0_2_2, all_70_0_66) = all_0_1_1 % 29.69/7.72 | (158) s(all_0_2_2) = all_70_0_66 % 29.69/7.72 | % 29.69/7.72 | Instantiating (148) with all_72_0_67, all_72_1_68 yields: % 29.69/7.72 | (159) ~ (all_72_0_67 = 0) & atleast2p(all_72_1_68) = 0 & subq(all_72_1_68, all_57_1_62) = 0 & subq(all_57_1_62, all_72_1_68) = all_72_0_67 % 29.69/7.72 | % 29.69/7.72 | Applying alpha-rule on (159) yields: % 29.69/7.72 | (160) ~ (all_72_0_67 = 0) % 29.69/7.72 | (161) atleast2p(all_72_1_68) = 0 % 29.69/7.72 | (162) subq(all_72_1_68, all_57_1_62) = 0 % 29.69/7.72 | (163) subq(all_57_1_62, all_72_1_68) = all_72_0_67 % 29.69/7.72 | % 29.69/7.72 +-Applying beta-rule and splitting (151), into two cases. % 29.69/7.72 |-Branch one: % 29.69/7.72 | (164) all_57_0_61 = 0 % 29.69/7.72 | % 29.69/7.72 | Equations (164) can reduce 144 to: % 29.69/7.72 | (165) $false % 29.69/7.72 | % 29.69/7.72 |-The branch is then unsatisfiable % 29.69/7.72 |-Branch two: % 29.69/7.72 | (144) ~ (all_57_0_61 = 0) % 29.69/7.72 | (167) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_57_1_62) = v0 & mem(all_0_0_0, v0) = v1) % 29.69/7.72 | % 29.69/7.72 +-Applying beta-rule and splitting (152), into two cases. % 29.69/7.72 |-Branch one: % 29.69/7.72 | (164) all_57_0_61 = 0 % 29.69/7.72 | % 29.69/7.72 | Equations (164) can reduce 144 to: % 29.69/7.72 | (165) $false % 29.69/7.72 | % 29.69/7.72 |-The branch is then unsatisfiable % 29.69/7.72 |-Branch two: % 29.69/7.72 | (144) ~ (all_57_0_61 = 0) % 29.69/7.72 | (171) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_57_1_62) = v1 & mem(v0, all_0_0_0) = 0) % 29.69/7.72 | % 29.69/7.72 | Instantiating (171) with all_83_0_71, all_83_1_72 yields: % 29.69/7.72 | (172) ~ (all_83_0_71 = 0) & mem(all_83_1_72, all_57_1_62) = all_83_0_71 & mem(all_83_1_72, all_0_0_0) = 0 % 29.69/7.72 | % 29.69/7.72 | Applying alpha-rule on (172) yields: % 29.69/7.72 | (173) ~ (all_83_0_71 = 0) % 29.69/7.72 | (174) mem(all_83_1_72, all_57_1_62) = all_83_0_71 % 29.69/7.72 | (175) mem(all_83_1_72, all_0_0_0) = 0 % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (117) with all_0_6_6, all_68_0_65, all_0_3_3 and discharging atoms s(all_0_6_6) = all_68_0_65, s(all_0_6_6) = all_0_3_3, yields: % 29.69/7.72 | (176) all_68_0_65 = all_0_3_3 % 29.69/7.72 | % 29.69/7.72 | From (176) and (154) follows: % 29.69/7.72 | (177) u(all_0_6_6, all_0_3_3) = all_0_5_5 % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (89) with all_72_1_68 and discharging atoms atleast2p(all_72_1_68) = 0, yields: % 29.69/7.72 | (178) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & p(v0) = v1 & subq(all_72_1_68, v1) = v2 & mem(v0, all_72_1_68) = 0) % 29.69/7.72 | % 29.69/7.72 | Instantiating formula (58) with all_72_0_67, all_72_1_68, all_57_1_62 and discharging atoms subq(all_57_1_62, all_72_1_68) = all_72_0_67, yields: % 29.69/7.73 | (179) all_72_0_67 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_72_1_68) = v0 & mem(all_57_1_62, v0) = v1) % 29.69/7.73 | % 29.69/7.73 | Instantiating formula (45) with all_72_0_67, all_72_1_68, all_57_1_62 and discharging atoms subq(all_57_1_62, all_72_1_68) = all_72_0_67, yields: % 29.69/7.73 | (180) all_72_0_67 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_72_1_68) = v1 & mem(v0, all_57_1_62) = 0) % 29.69/7.73 | % 29.69/7.73 | Instantiating formula (62) with all_83_0_71, all_83_1_72, all_57_1_62, all_72_1_68 and discharging atoms subq(all_72_1_68, all_57_1_62) = 0, mem(all_83_1_72, all_57_1_62) = all_83_0_71, yields: % 29.69/7.73 | (181) all_83_0_71 = 0 | ? [v0] : ( ~ (v0 = 0) & mem(all_83_1_72, all_72_1_68) = v0) % 29.69/7.73 | % 29.69/7.73 | Instantiating formula (72) with all_0_0_0, all_0_1_1, all_0_4_4, all_83_1_72 and discharging atoms u(all_0_4_4, all_0_1_1) = all_0_0_0, mem(all_83_1_72, all_0_0_0) = 0, yields: % 29.69/7.73 | (182) ? [v0] : ((v0 = 0 & mem(all_83_1_72, all_0_1_1) = 0) | (v0 = 0 & mem(all_83_1_72, all_0_4_4) = 0)) % 29.69/7.73 | % 29.69/7.73 | Instantiating (182) with all_94_0_73 yields: % 29.69/7.73 | (183) (all_94_0_73 = 0 & mem(all_83_1_72, all_0_1_1) = 0) | (all_94_0_73 = 0 & mem(all_83_1_72, all_0_4_4) = 0) % 29.69/7.73 | % 29.69/7.73 | Instantiating (178) with all_97_0_75, all_97_1_76, all_97_2_77 yields: % 29.69/7.73 | (184) ~ (all_97_0_75 = 0) & p(all_97_2_77) = all_97_1_76 & subq(all_72_1_68, all_97_1_76) = all_97_0_75 & mem(all_97_2_77, all_72_1_68) = 0 % 29.69/7.73 | % 29.69/7.73 | Applying alpha-rule on (184) yields: % 29.69/7.73 | (185) ~ (all_97_0_75 = 0) % 29.69/7.73 | (186) p(all_97_2_77) = all_97_1_76 % 30.19/7.73 | (187) subq(all_72_1_68, all_97_1_76) = all_97_0_75 % 30.19/7.73 | (188) mem(all_97_2_77, all_72_1_68) = 0 % 30.19/7.73 | % 30.19/7.73 +-Applying beta-rule and splitting (179), into two cases. % 30.19/7.73 |-Branch one: % 30.19/7.73 | (189) all_72_0_67 = 0 % 30.19/7.73 | % 30.19/7.73 | Equations (189) can reduce 160 to: % 30.19/7.73 | (165) $false % 30.19/7.73 | % 30.19/7.73 |-The branch is then unsatisfiable % 30.19/7.73 |-Branch two: % 30.19/7.73 | (160) ~ (all_72_0_67 = 0) % 30.19/7.73 | (192) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_72_1_68) = v0 & mem(all_57_1_62, v0) = v1) % 30.19/7.73 | % 30.19/7.73 +-Applying beta-rule and splitting (180), into two cases. % 30.19/7.73 |-Branch one: % 30.19/7.73 | (189) all_72_0_67 = 0 % 30.19/7.73 | % 30.19/7.73 | Equations (189) can reduce 160 to: % 30.19/7.73 | (165) $false % 30.19/7.73 | % 30.19/7.73 |-The branch is then unsatisfiable % 30.19/7.73 |-Branch two: % 30.19/7.73 | (160) ~ (all_72_0_67 = 0) % 30.19/7.73 | (196) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_72_1_68) = v1 & mem(v0, all_57_1_62) = 0) % 30.19/7.73 | % 30.19/7.73 | Instantiating (196) with all_108_0_80, all_108_1_81 yields: % 30.19/7.73 | (197) ~ (all_108_0_80 = 0) & mem(all_108_1_81, all_72_1_68) = all_108_0_80 & mem(all_108_1_81, all_57_1_62) = 0 % 30.19/7.73 | % 30.19/7.73 | Applying alpha-rule on (197) yields: % 30.19/7.73 | (198) ~ (all_108_0_80 = 0) % 30.19/7.73 | (199) mem(all_108_1_81, all_72_1_68) = all_108_0_80 % 30.19/7.73 | (200) mem(all_108_1_81, all_57_1_62) = 0 % 30.19/7.73 | % 30.19/7.73 +-Applying beta-rule and splitting (181), into two cases. % 30.19/7.73 |-Branch one: % 30.19/7.73 | (201) all_83_0_71 = 0 % 30.19/7.73 | % 30.19/7.73 | Equations (201) can reduce 173 to: % 30.19/7.73 | (165) $false % 30.19/7.73 | % 30.19/7.73 |-The branch is then unsatisfiable % 30.19/7.73 |-Branch two: % 30.19/7.73 | (173) ~ (all_83_0_71 = 0) % 30.19/7.73 | (204) ? [v0] : ( ~ (v0 = 0) & mem(all_83_1_72, all_72_1_68) = v0) % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (45) with all_97_0_75, all_97_1_76, all_72_1_68 and discharging atoms subq(all_72_1_68, all_97_1_76) = all_97_0_75, yields: % 30.19/7.73 | (205) all_97_0_75 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_97_1_76) = v1 & mem(v0, all_72_1_68) = 0) % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (78) with all_108_1_81, all_0_0_0, all_57_1_62 and discharging atoms subq(all_57_1_62, all_0_0_0) = 0, mem(all_108_1_81, all_57_1_62) = 0, yields: % 30.19/7.73 | (206) mem(all_108_1_81, all_0_0_0) = 0 % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (78) with all_97_2_77, all_57_1_62, all_72_1_68 and discharging atoms subq(all_72_1_68, all_57_1_62) = 0, mem(all_97_2_77, all_72_1_68) = 0, yields: % 30.19/7.73 | (207) mem(all_97_2_77, all_57_1_62) = 0 % 30.19/7.73 | % 30.19/7.73 +-Applying beta-rule and splitting (205), into two cases. % 30.19/7.73 |-Branch one: % 30.19/7.73 | (208) all_97_0_75 = 0 % 30.19/7.73 | % 30.19/7.73 | Equations (208) can reduce 185 to: % 30.19/7.73 | (165) $false % 30.19/7.73 | % 30.19/7.73 |-The branch is then unsatisfiable % 30.19/7.73 |-Branch two: % 30.19/7.73 | (185) ~ (all_97_0_75 = 0) % 30.19/7.73 | (211) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_97_1_76) = v1 & mem(v0, all_72_1_68) = 0) % 30.19/7.73 | % 30.19/7.73 | Instantiating (211) with all_129_0_83, all_129_1_84 yields: % 30.19/7.73 | (212) ~ (all_129_0_83 = 0) & mem(all_129_1_84, all_97_1_76) = all_129_0_83 & mem(all_129_1_84, all_72_1_68) = 0 % 30.19/7.73 | % 30.19/7.73 | Applying alpha-rule on (212) yields: % 30.19/7.73 | (213) ~ (all_129_0_83 = 0) % 30.19/7.73 | (214) mem(all_129_1_84, all_97_1_76) = all_129_0_83 % 30.19/7.73 | (215) mem(all_129_1_84, all_72_1_68) = 0 % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (74) with all_129_0_83, all_97_1_76, all_97_2_77, all_129_1_84 and discharging atoms p(all_97_2_77) = all_97_1_76, mem(all_129_1_84, all_97_1_76) = all_129_0_83, yields: % 30.19/7.73 | (216) all_129_0_83 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_129_1_84, all_97_2_77) = v0) % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (78) with all_129_1_84, all_57_1_62, all_72_1_68 and discharging atoms subq(all_72_1_68, all_57_1_62) = 0, mem(all_129_1_84, all_72_1_68) = 0, yields: % 30.19/7.73 | (217) mem(all_129_1_84, all_57_1_62) = 0 % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (72) with all_0_0_0, all_0_1_1, all_0_4_4, all_108_1_81 and discharging atoms u(all_0_4_4, all_0_1_1) = all_0_0_0, mem(all_108_1_81, all_0_0_0) = 0, yields: % 30.19/7.73 | (218) ? [v0] : ((v0 = 0 & mem(all_108_1_81, all_0_1_1) = 0) | (v0 = 0 & mem(all_108_1_81, all_0_4_4) = 0)) % 30.19/7.73 | % 30.19/7.73 | Instantiating formula (78) with all_97_2_77, all_0_0_0, all_57_1_62 and discharging atoms subq(all_57_1_62, all_0_0_0) = 0, mem(all_97_2_77, all_57_1_62) = 0, yields: % 30.19/7.73 | (219) mem(all_97_2_77, all_0_0_0) = 0 % 30.19/7.73 | % 30.19/7.73 | Instantiating (218) with all_142_0_87 yields: % 30.19/7.73 | (220) (all_142_0_87 = 0 & mem(all_108_1_81, all_0_1_1) = 0) | (all_142_0_87 = 0 & mem(all_108_1_81, all_0_4_4) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (216), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (221) all_129_0_83 = 0 % 30.19/7.74 | % 30.19/7.74 | Equations (221) can reduce 213 to: % 30.19/7.74 | (165) $false % 30.19/7.74 | % 30.19/7.74 |-The branch is then unsatisfiable % 30.19/7.74 |-Branch two: % 30.19/7.74 | (213) ~ (all_129_0_83 = 0) % 30.19/7.74 | (224) ? [v0] : ( ~ (v0 = 0) & subq(all_129_1_84, all_97_2_77) = v0) % 30.19/7.74 | % 30.19/7.74 | Instantiating (224) with all_147_0_88 yields: % 30.19/7.74 | (225) ~ (all_147_0_88 = 0) & subq(all_129_1_84, all_97_2_77) = all_147_0_88 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (225) yields: % 30.19/7.74 | (226) ~ (all_147_0_88 = 0) % 30.19/7.74 | (227) subq(all_129_1_84, all_97_2_77) = all_147_0_88 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (45) with all_147_0_88, all_97_2_77, all_129_1_84 and discharging atoms subq(all_129_1_84, all_97_2_77) = all_147_0_88, yields: % 30.19/7.74 | (228) all_147_0_88 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_129_1_84) = 0 & mem(v0, all_97_2_77) = v1) % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (78) with all_129_1_84, all_0_0_0, all_57_1_62 and discharging atoms subq(all_57_1_62, all_0_0_0) = 0, mem(all_129_1_84, all_57_1_62) = 0, yields: % 30.19/7.74 | (229) mem(all_129_1_84, all_0_0_0) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (72) with all_0_0_0, all_0_1_1, all_0_4_4, all_97_2_77 and discharging atoms u(all_0_4_4, all_0_1_1) = all_0_0_0, mem(all_97_2_77, all_0_0_0) = 0, yields: % 30.19/7.74 | (230) ? [v0] : ((v0 = 0 & mem(all_97_2_77, all_0_1_1) = 0) | (v0 = 0 & mem(all_97_2_77, all_0_4_4) = 0)) % 30.19/7.74 | % 30.19/7.74 | Instantiating (230) with all_155_0_89 yields: % 30.19/7.74 | (231) (all_155_0_89 = 0 & mem(all_97_2_77, all_0_1_1) = 0) | (all_155_0_89 = 0 & mem(all_97_2_77, all_0_4_4) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (228), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (232) all_147_0_88 = 0 % 30.19/7.74 | % 30.19/7.74 | Equations (232) can reduce 226 to: % 30.19/7.74 | (165) $false % 30.19/7.74 | % 30.19/7.74 |-The branch is then unsatisfiable % 30.19/7.74 |-Branch two: % 30.19/7.74 | (226) ~ (all_147_0_88 = 0) % 30.19/7.74 | (235) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_129_1_84) = 0 & mem(v0, all_97_2_77) = v1) % 30.19/7.74 | % 30.19/7.74 | Instantiating (235) with all_160_0_90, all_160_1_91 yields: % 30.19/7.74 | (236) ~ (all_160_0_90 = 0) & mem(all_160_1_91, all_129_1_84) = 0 & mem(all_160_1_91, all_97_2_77) = all_160_0_90 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (236) yields: % 30.19/7.74 | (237) ~ (all_160_0_90 = 0) % 30.19/7.74 | (238) mem(all_160_1_91, all_129_1_84) = 0 % 30.19/7.74 | (239) mem(all_160_1_91, all_97_2_77) = all_160_0_90 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (72) with all_0_0_0, all_0_1_1, all_0_4_4, all_129_1_84 and discharging atoms u(all_0_4_4, all_0_1_1) = all_0_0_0, mem(all_129_1_84, all_0_0_0) = 0, yields: % 30.19/7.74 | (240) ? [v0] : ((v0 = 0 & mem(all_129_1_84, all_0_1_1) = 0) | (v0 = 0 & mem(all_129_1_84, all_0_4_4) = 0)) % 30.19/7.74 | % 30.19/7.74 | Instantiating (240) with all_167_0_92 yields: % 30.19/7.74 | (241) (all_167_0_92 = 0 & mem(all_129_1_84, all_0_1_1) = 0) | (all_167_0_92 = 0 & mem(all_129_1_84, all_0_4_4) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (183), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (242) all_94_0_73 = 0 & mem(all_83_1_72, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (242) yields: % 30.19/7.74 | (243) all_94_0_73 = 0 % 30.19/7.74 | (244) mem(all_83_1_72, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_83_1_72 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_83_1_72, all_0_1_1) = 0, yields: % 30.19/7.74 | (245) ? [v0] : ((v0 = 0 & mem(all_83_1_72, all_70_0_66) = 0) | (v0 = 0 & mem(all_83_1_72, all_0_2_2) = 0)) % 30.19/7.74 | % 30.19/7.74 | Instantiating (245) with all_175_0_93 yields: % 30.19/7.74 | (246) (all_175_0_93 = 0 & mem(all_83_1_72, all_70_0_66) = 0) | (all_175_0_93 = 0 & mem(all_83_1_72, all_0_2_2) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (220), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (247) all_142_0_87 = 0 & mem(all_108_1_81, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (247) yields: % 30.19/7.74 | (248) all_142_0_87 = 0 % 30.19/7.74 | (249) mem(all_108_1_81, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_108_1_81, all_0_1_1) = 0, yields: % 30.19/7.74 | (250) ? [v0] : ((v0 = 0 & mem(all_108_1_81, all_70_0_66) = 0) | (v0 = 0 & mem(all_108_1_81, all_0_2_2) = 0)) % 30.19/7.74 | % 30.19/7.74 | Instantiating (250) with all_183_0_94 yields: % 30.19/7.74 | (251) (all_183_0_94 = 0 & mem(all_108_1_81, all_70_0_66) = 0) | (all_183_0_94 = 0 & mem(all_108_1_81, all_0_2_2) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (231), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (252) all_155_0_89 = 0 & mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (252) yields: % 30.19/7.74 | (253) all_155_0_89 = 0 % 30.19/7.74 | (254) mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_97_2_77, all_0_1_1) = 0, yields: % 30.19/7.74 | (255) ? [v0] : ((v0 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (v0 = 0 & mem(all_97_2_77, all_0_2_2) = 0)) % 30.19/7.74 | % 30.19/7.74 | Instantiating (255) with all_191_0_95 yields: % 30.19/7.74 | (256) (all_191_0_95 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (all_191_0_95 = 0 & mem(all_97_2_77, all_0_2_2) = 0) % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (246), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (257) all_175_0_93 = 0 & mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (257) yields: % 30.19/7.74 | (258) all_175_0_93 = 0 % 30.19/7.74 | (259) mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_83_1_72 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_83_1_72, all_70_0_66) = 0, yields: % 30.19/7.74 | (260) all_83_1_72 = all_0_2_2 % 30.19/7.74 | % 30.19/7.74 | From (260) and (174) follows: % 30.19/7.74 | (261) mem(all_0_2_2, all_57_1_62) = all_83_0_71 % 30.19/7.74 | % 30.19/7.74 +-Applying beta-rule and splitting (251), into two cases. % 30.19/7.74 |-Branch one: % 30.19/7.74 | (262) all_183_0_94 = 0 & mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (262) yields: % 30.19/7.74 | (263) all_183_0_94 = 0 % 30.19/7.74 | (264) mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_108_1_81, all_70_0_66) = 0, yields: % 30.19/7.74 | (265) all_108_1_81 = all_0_2_2 % 30.19/7.74 | % 30.19/7.74 | From (265) and (200) follows: % 30.19/7.74 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.74 | (201) all_83_0_71 = 0 % 30.19/7.74 | % 30.19/7.74 | Equations (201) can reduce 173 to: % 30.19/7.74 | (165) $false % 30.19/7.74 | % 30.19/7.74 |-The branch is then unsatisfiable % 30.19/7.74 |-Branch two: % 30.19/7.74 | (269) all_183_0_94 = 0 & mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.74 | % 30.19/7.74 | Applying alpha-rule on (269) yields: % 30.19/7.74 | (263) all_183_0_94 = 0 % 30.19/7.74 | (271) mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.74 | % 30.19/7.74 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_108_1_81 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_108_1_81, all_0_2_2) = 0, yields: % 30.19/7.75 | (272) all_108_1_81 = all_0_3_3 % 30.19/7.75 | % 30.19/7.75 | From (272) and (199) follows: % 30.19/7.75 | (273) mem(all_0_3_3, all_72_1_68) = all_108_0_80 % 30.19/7.75 | % 30.19/7.75 +-Applying beta-rule and splitting (256), into two cases. % 30.19/7.75 |-Branch one: % 30.19/7.75 | (274) all_191_0_95 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (274) yields: % 30.19/7.75 | (275) all_191_0_95 = 0 % 30.19/7.75 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.75 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.75 | % 30.19/7.75 | From (277) and (207) follows: % 30.19/7.75 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.75 | (201) all_83_0_71 = 0 % 30.19/7.75 | % 30.19/7.75 | Equations (201) can reduce 173 to: % 30.19/7.75 | (165) $false % 30.19/7.75 | % 30.19/7.75 |-The branch is then unsatisfiable % 30.19/7.75 |-Branch two: % 30.19/7.75 | (281) all_191_0_95 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (281) yields: % 30.19/7.75 | (275) all_191_0_95 = 0 % 30.19/7.75 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.75 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.75 | % 30.19/7.75 | From (284) and (188) follows: % 30.19/7.75 | (285) mem(all_0_3_3, all_72_1_68) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (113) with all_0_3_3, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_3_3, all_72_1_68) = all_108_0_80, mem(all_0_3_3, all_72_1_68) = 0, yields: % 30.19/7.75 | (286) all_108_0_80 = 0 % 30.19/7.75 | % 30.19/7.75 | Equations (286) can reduce 198 to: % 30.19/7.75 | (165) $false % 30.19/7.75 | % 30.19/7.75 |-The branch is then unsatisfiable % 30.19/7.75 |-Branch two: % 30.19/7.75 | (288) all_175_0_93 = 0 & mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (288) yields: % 30.19/7.75 | (258) all_175_0_93 = 0 % 30.19/7.75 | (290) mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_83_1_72 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_83_1_72, all_0_2_2) = 0, yields: % 30.19/7.75 | (291) all_83_1_72 = all_0_3_3 % 30.19/7.75 | % 30.19/7.75 | From (291) and (174) follows: % 30.19/7.75 | (292) mem(all_0_3_3, all_57_1_62) = all_83_0_71 % 30.19/7.75 | % 30.19/7.75 +-Applying beta-rule and splitting (251), into two cases. % 30.19/7.75 |-Branch one: % 30.19/7.75 | (262) all_183_0_94 = 0 & mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (262) yields: % 30.19/7.75 | (263) all_183_0_94 = 0 % 30.19/7.75 | (264) mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_108_1_81, all_70_0_66) = 0, yields: % 30.19/7.75 | (265) all_108_1_81 = all_0_2_2 % 30.19/7.75 | % 30.19/7.75 | From (265) and (199) follows: % 30.19/7.75 | (297) mem(all_0_2_2, all_72_1_68) = all_108_0_80 % 30.19/7.75 | % 30.19/7.75 +-Applying beta-rule and splitting (256), into two cases. % 30.19/7.75 |-Branch one: % 30.19/7.75 | (274) all_191_0_95 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (274) yields: % 30.19/7.75 | (275) all_191_0_95 = 0 % 30.19/7.75 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.75 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.75 | % 30.19/7.75 | From (277) and (188) follows: % 30.19/7.75 | (302) mem(all_0_2_2, all_72_1_68) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (113) with all_0_2_2, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_2_2, all_72_1_68) = all_108_0_80, mem(all_0_2_2, all_72_1_68) = 0, yields: % 30.19/7.75 | (286) all_108_0_80 = 0 % 30.19/7.75 | % 30.19/7.75 | Equations (286) can reduce 198 to: % 30.19/7.75 | (165) $false % 30.19/7.75 | % 30.19/7.75 |-The branch is then unsatisfiable % 30.19/7.75 |-Branch two: % 30.19/7.75 | (281) all_191_0_95 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (281) yields: % 30.19/7.75 | (275) all_191_0_95 = 0 % 30.19/7.75 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.75 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.75 | % 30.19/7.75 | From (284) and (207) follows: % 30.19/7.75 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.75 | (201) all_83_0_71 = 0 % 30.19/7.75 | % 30.19/7.75 | Equations (201) can reduce 173 to: % 30.19/7.75 | (165) $false % 30.19/7.75 | % 30.19/7.75 |-The branch is then unsatisfiable % 30.19/7.75 |-Branch two: % 30.19/7.75 | (269) all_183_0_94 = 0 & mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (269) yields: % 30.19/7.75 | (263) all_183_0_94 = 0 % 30.19/7.75 | (271) mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_108_1_81 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_108_1_81, all_0_2_2) = 0, yields: % 30.19/7.75 | (272) all_108_1_81 = all_0_3_3 % 30.19/7.75 | % 30.19/7.75 | From (272) and (200) follows: % 30.19/7.75 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.75 | (201) all_83_0_71 = 0 % 30.19/7.75 | % 30.19/7.75 | Equations (201) can reduce 173 to: % 30.19/7.75 | (165) $false % 30.19/7.75 | % 30.19/7.75 |-The branch is then unsatisfiable % 30.19/7.75 |-Branch two: % 30.19/7.75 | (319) all_155_0_89 = 0 & mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (319) yields: % 30.19/7.75 | (253) all_155_0_89 = 0 % 30.19/7.75 | (321) mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_97_2_77 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_97_2_77, all_0_4_4) = 0, yields: % 30.19/7.75 | (322) all_97_2_77 = all_0_5_5 % 30.19/7.75 | % 30.19/7.75 | From (322) and (239) follows: % 30.19/7.75 | (323) mem(all_160_1_91, all_0_5_5) = all_160_0_90 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (69) with all_160_0_90, all_0_5_5, all_0_3_3, all_0_6_6, all_160_1_91 and discharging atoms u(all_0_6_6, all_0_3_3) = all_0_5_5, mem(all_160_1_91, all_0_5_5) = all_160_0_90, yields: % 30.19/7.75 | (324) all_160_0_90 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_160_1_91, all_0_3_3) = v1 & mem(all_160_1_91, all_0_6_6) = v0) % 30.19/7.75 | % 30.19/7.75 +-Applying beta-rule and splitting (241), into two cases. % 30.19/7.75 |-Branch one: % 30.19/7.75 | (325) all_167_0_92 = 0 & mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.75 | % 30.19/7.75 | Applying alpha-rule on (325) yields: % 30.19/7.75 | (326) all_167_0_92 = 0 % 30.19/7.75 | (327) mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.75 | % 30.19/7.75 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_129_1_84, all_0_1_1) = 0, yields: % 30.19/7.75 | (328) ? [v0] : ((v0 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (v0 = 0 & mem(all_129_1_84, all_0_2_2) = 0)) % 30.19/7.75 | % 30.19/7.75 | Instantiating (328) with all_213_0_101 yields: % 30.19/7.75 | (329) (all_213_0_101 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (all_213_0_101 = 0 & mem(all_129_1_84, all_0_2_2) = 0) % 30.19/7.75 | % 30.19/7.75 +-Applying beta-rule and splitting (246), into two cases. % 30.19/7.75 |-Branch one: % 30.19/7.75 | (257) all_175_0_93 = 0 & mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.75 | % 30.19/7.76 | Applying alpha-rule on (257) yields: % 30.19/7.76 | (258) all_175_0_93 = 0 % 30.19/7.76 | (259) mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_83_1_72 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_83_1_72, all_70_0_66) = 0, yields: % 30.19/7.76 | (260) all_83_1_72 = all_0_2_2 % 30.19/7.76 | % 30.19/7.76 | From (260) and (174) follows: % 30.19/7.76 | (261) mem(all_0_2_2, all_57_1_62) = all_83_0_71 % 30.19/7.76 | % 30.19/7.76 +-Applying beta-rule and splitting (251), into two cases. % 30.19/7.76 |-Branch one: % 30.19/7.76 | (262) all_183_0_94 = 0 & mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (262) yields: % 30.19/7.76 | (263) all_183_0_94 = 0 % 30.19/7.76 | (264) mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_108_1_81, all_70_0_66) = 0, yields: % 30.19/7.76 | (265) all_108_1_81 = all_0_2_2 % 30.19/7.76 | % 30.19/7.76 | From (265) and (200) follows: % 30.19/7.76 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.76 | (201) all_83_0_71 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (201) can reduce 173 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (269) all_183_0_94 = 0 & mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (269) yields: % 30.19/7.76 | (263) all_183_0_94 = 0 % 30.19/7.76 | (271) mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_108_1_81 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_108_1_81, all_0_2_2) = 0, yields: % 30.19/7.76 | (272) all_108_1_81 = all_0_3_3 % 30.19/7.76 | % 30.19/7.76 | From (272) and (199) follows: % 30.19/7.76 | (273) mem(all_0_3_3, all_72_1_68) = all_108_0_80 % 30.19/7.76 | % 30.19/7.76 +-Applying beta-rule and splitting (329), into two cases. % 30.19/7.76 |-Branch one: % 30.19/7.76 | (347) all_213_0_101 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (347) yields: % 30.19/7.76 | (348) all_213_0_101 = 0 % 30.19/7.76 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.76 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.76 | % 30.19/7.76 | From (350) and (217) follows: % 30.19/7.76 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.76 | (201) all_83_0_71 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (201) can reduce 173 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (354) all_213_0_101 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (354) yields: % 30.19/7.76 | (348) all_213_0_101 = 0 % 30.19/7.76 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.76 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.76 | % 30.19/7.76 | From (357) and (215) follows: % 30.19/7.76 | (285) mem(all_0_3_3, all_72_1_68) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_3_3, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_3_3, all_72_1_68) = all_108_0_80, mem(all_0_3_3, all_72_1_68) = 0, yields: % 30.19/7.76 | (286) all_108_0_80 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (286) can reduce 198 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (288) all_175_0_93 = 0 & mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (288) yields: % 30.19/7.76 | (258) all_175_0_93 = 0 % 30.19/7.76 | (290) mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_83_1_72 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_83_1_72, all_0_2_2) = 0, yields: % 30.19/7.76 | (291) all_83_1_72 = all_0_3_3 % 30.19/7.76 | % 30.19/7.76 | From (291) and (174) follows: % 30.19/7.76 | (292) mem(all_0_3_3, all_57_1_62) = all_83_0_71 % 30.19/7.76 | % 30.19/7.76 +-Applying beta-rule and splitting (251), into two cases. % 30.19/7.76 |-Branch one: % 30.19/7.76 | (262) all_183_0_94 = 0 & mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (262) yields: % 30.19/7.76 | (263) all_183_0_94 = 0 % 30.19/7.76 | (264) mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_108_1_81, all_70_0_66) = 0, yields: % 30.19/7.76 | (265) all_108_1_81 = all_0_2_2 % 30.19/7.76 | % 30.19/7.76 | From (265) and (199) follows: % 30.19/7.76 | (297) mem(all_0_2_2, all_72_1_68) = all_108_0_80 % 30.19/7.76 | % 30.19/7.76 +-Applying beta-rule and splitting (329), into two cases. % 30.19/7.76 |-Branch one: % 30.19/7.76 | (347) all_213_0_101 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (347) yields: % 30.19/7.76 | (348) all_213_0_101 = 0 % 30.19/7.76 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.76 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.76 | % 30.19/7.76 | From (350) and (215) follows: % 30.19/7.76 | (302) mem(all_0_2_2, all_72_1_68) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_2_2, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_2_2, all_72_1_68) = all_108_0_80, mem(all_0_2_2, all_72_1_68) = 0, yields: % 30.19/7.76 | (286) all_108_0_80 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (286) can reduce 198 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (354) all_213_0_101 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (354) yields: % 30.19/7.76 | (348) all_213_0_101 = 0 % 30.19/7.76 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.76 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.76 | % 30.19/7.76 | From (357) and (217) follows: % 30.19/7.76 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.76 | (201) all_83_0_71 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (201) can reduce 173 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (269) all_183_0_94 = 0 & mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (269) yields: % 30.19/7.76 | (263) all_183_0_94 = 0 % 30.19/7.76 | (271) mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_108_1_81 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_108_1_81, all_0_2_2) = 0, yields: % 30.19/7.76 | (272) all_108_1_81 = all_0_3_3 % 30.19/7.76 | % 30.19/7.76 | From (272) and (200) follows: % 30.19/7.76 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.76 | % 30.19/7.76 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.76 | (201) all_83_0_71 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (201) can reduce 173 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (392) all_167_0_92 = 0 & mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.76 | % 30.19/7.76 | Applying alpha-rule on (392) yields: % 30.19/7.76 | (326) all_167_0_92 = 0 % 30.19/7.76 | (394) mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.76 | % 30.19/7.76 +-Applying beta-rule and splitting (324), into two cases. % 30.19/7.76 |-Branch one: % 30.19/7.76 | (395) all_160_0_90 = 0 % 30.19/7.76 | % 30.19/7.76 | Equations (395) can reduce 237 to: % 30.19/7.76 | (165) $false % 30.19/7.76 | % 30.19/7.76 |-The branch is then unsatisfiable % 30.19/7.76 |-Branch two: % 30.19/7.76 | (237) ~ (all_160_0_90 = 0) % 30.19/7.76 | (398) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_160_1_91, all_0_3_3) = v1 & mem(all_160_1_91, all_0_6_6) = v0) % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_129_1_84 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_129_1_84, all_0_4_4) = 0, yields: % 30.19/7.77 | (399) all_129_1_84 = all_0_5_5 % 30.19/7.77 | % 30.19/7.77 | From (399) and (238) follows: % 30.19/7.77 | (400) mem(all_160_1_91, all_0_5_5) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (113) with all_160_1_91, all_0_5_5, 0, all_160_0_90 and discharging atoms mem(all_160_1_91, all_0_5_5) = all_160_0_90, mem(all_160_1_91, all_0_5_5) = 0, yields: % 30.19/7.77 | (395) all_160_0_90 = 0 % 30.19/7.77 | % 30.19/7.77 | Equations (395) can reduce 237 to: % 30.19/7.77 | (165) $false % 30.19/7.77 | % 30.19/7.77 |-The branch is then unsatisfiable % 30.19/7.77 |-Branch two: % 30.19/7.77 | (403) all_142_0_87 = 0 & mem(all_108_1_81, all_0_4_4) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (403) yields: % 30.19/7.77 | (248) all_142_0_87 = 0 % 30.19/7.77 | (405) mem(all_108_1_81, all_0_4_4) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_108_1_81 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_108_1_81, all_0_4_4) = 0, yields: % 30.19/7.77 | (406) all_108_1_81 = all_0_5_5 % 30.19/7.77 | % 30.19/7.77 | From (406) and (199) follows: % 30.19/7.77 | (407) mem(all_0_5_5, all_72_1_68) = all_108_0_80 % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (231), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (252) all_155_0_89 = 0 & mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (252) yields: % 30.19/7.77 | (253) all_155_0_89 = 0 % 30.19/7.77 | (254) mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_97_2_77, all_0_1_1) = 0, yields: % 30.19/7.77 | (255) ? [v0] : ((v0 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (v0 = 0 & mem(all_97_2_77, all_0_2_2) = 0)) % 30.19/7.77 | % 30.19/7.77 | Instantiating (255) with all_194_0_122 yields: % 30.19/7.77 | (412) (all_194_0_122 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (all_194_0_122 = 0 & mem(all_97_2_77, all_0_2_2) = 0) % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (241), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (325) all_167_0_92 = 0 & mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (325) yields: % 30.19/7.77 | (326) all_167_0_92 = 0 % 30.19/7.77 | (327) mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_129_1_84, all_0_1_1) = 0, yields: % 30.19/7.77 | (328) ? [v0] : ((v0 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (v0 = 0 & mem(all_129_1_84, all_0_2_2) = 0)) % 30.19/7.77 | % 30.19/7.77 | Instantiating (328) with all_202_0_123 yields: % 30.19/7.77 | (417) (all_202_0_123 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (all_202_0_123 = 0 & mem(all_129_1_84, all_0_2_2) = 0) % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (246), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (257) all_175_0_93 = 0 & mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (257) yields: % 30.19/7.77 | (258) all_175_0_93 = 0 % 30.19/7.77 | (259) mem(all_83_1_72, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_83_1_72 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_83_1_72, all_70_0_66) = 0, yields: % 30.19/7.77 | (260) all_83_1_72 = all_0_2_2 % 30.19/7.77 | % 30.19/7.77 | From (260) and (174) follows: % 30.19/7.77 | (261) mem(all_0_2_2, all_57_1_62) = all_83_0_71 % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (412), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (423) all_194_0_122 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (423) yields: % 30.19/7.77 | (424) all_194_0_122 = 0 % 30.19/7.77 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.77 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.77 | % 30.19/7.77 | From (277) and (207) follows: % 30.19/7.77 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.77 | (201) all_83_0_71 = 0 % 30.19/7.77 | % 30.19/7.77 | Equations (201) can reduce 173 to: % 30.19/7.77 | (165) $false % 30.19/7.77 | % 30.19/7.77 |-The branch is then unsatisfiable % 30.19/7.77 |-Branch two: % 30.19/7.77 | (430) all_194_0_122 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (430) yields: % 30.19/7.77 | (424) all_194_0_122 = 0 % 30.19/7.77 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.77 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.77 | % 30.19/7.77 | From (284) and (239) follows: % 30.19/7.77 | (434) mem(all_160_1_91, all_0_3_3) = all_160_0_90 % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (417), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (435) all_202_0_123 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (435) yields: % 30.19/7.77 | (436) all_202_0_123 = 0 % 30.19/7.77 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.77 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.77 | % 30.19/7.77 | From (350) and (217) follows: % 30.19/7.77 | (266) mem(all_0_2_2, all_57_1_62) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (113) with all_0_2_2, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_2_2, all_57_1_62) = all_83_0_71, mem(all_0_2_2, all_57_1_62) = 0, yields: % 30.19/7.77 | (201) all_83_0_71 = 0 % 30.19/7.77 | % 30.19/7.77 | Equations (201) can reduce 173 to: % 30.19/7.77 | (165) $false % 30.19/7.77 | % 30.19/7.77 |-The branch is then unsatisfiable % 30.19/7.77 |-Branch two: % 30.19/7.77 | (442) all_202_0_123 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (442) yields: % 30.19/7.77 | (436) all_202_0_123 = 0 % 30.19/7.77 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.77 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.77 | % 30.19/7.77 | From (357) and (238) follows: % 30.19/7.77 | (446) mem(all_160_1_91, all_0_3_3) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (113) with all_160_1_91, all_0_3_3, 0, all_160_0_90 and discharging atoms mem(all_160_1_91, all_0_3_3) = all_160_0_90, mem(all_160_1_91, all_0_3_3) = 0, yields: % 30.19/7.77 | (395) all_160_0_90 = 0 % 30.19/7.77 | % 30.19/7.77 | Equations (395) can reduce 237 to: % 30.19/7.77 | (165) $false % 30.19/7.77 | % 30.19/7.77 |-The branch is then unsatisfiable % 30.19/7.77 |-Branch two: % 30.19/7.77 | (288) all_175_0_93 = 0 & mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (288) yields: % 30.19/7.77 | (258) all_175_0_93 = 0 % 30.19/7.77 | (290) mem(all_83_1_72, all_0_2_2) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_83_1_72 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_83_1_72, all_0_2_2) = 0, yields: % 30.19/7.77 | (291) all_83_1_72 = all_0_3_3 % 30.19/7.77 | % 30.19/7.77 | From (291) and (174) follows: % 30.19/7.77 | (292) mem(all_0_3_3, all_57_1_62) = all_83_0_71 % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (412), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.77 | (423) all_194_0_122 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Applying alpha-rule on (423) yields: % 30.19/7.77 | (424) all_194_0_122 = 0 % 30.19/7.77 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.77 | % 30.19/7.77 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.77 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.77 | % 30.19/7.77 | From (277) and (239) follows: % 30.19/7.77 | (458) mem(all_160_1_91, all_0_2_2) = all_160_0_90 % 30.19/7.77 | % 30.19/7.77 +-Applying beta-rule and splitting (417), into two cases. % 30.19/7.77 |-Branch one: % 30.19/7.78 | (435) all_202_0_123 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (435) yields: % 30.19/7.78 | (436) all_202_0_123 = 0 % 30.19/7.78 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.78 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.78 | % 30.19/7.78 | From (350) and (238) follows: % 30.19/7.78 | (463) mem(all_160_1_91, all_0_2_2) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (113) with all_160_1_91, all_0_2_2, 0, all_160_0_90 and discharging atoms mem(all_160_1_91, all_0_2_2) = all_160_0_90, mem(all_160_1_91, all_0_2_2) = 0, yields: % 30.19/7.78 | (395) all_160_0_90 = 0 % 30.19/7.78 | % 30.19/7.78 | Equations (395) can reduce 237 to: % 30.19/7.78 | (165) $false % 30.19/7.78 | % 30.19/7.78 |-The branch is then unsatisfiable % 30.19/7.78 |-Branch two: % 30.19/7.78 | (442) all_202_0_123 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (442) yields: % 30.19/7.78 | (436) all_202_0_123 = 0 % 30.19/7.78 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.78 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.78 | % 30.19/7.78 | From (357) and (217) follows: % 30.19/7.78 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.78 | (201) all_83_0_71 = 0 % 30.19/7.78 | % 30.19/7.78 | Equations (201) can reduce 173 to: % 30.19/7.78 | (165) $false % 30.19/7.78 | % 30.19/7.78 |-The branch is then unsatisfiable % 30.19/7.78 |-Branch two: % 30.19/7.78 | (430) all_194_0_122 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (430) yields: % 30.19/7.78 | (424) all_194_0_122 = 0 % 30.19/7.78 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.78 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.78 | % 30.19/7.78 | From (284) and (207) follows: % 30.19/7.78 | (309) mem(all_0_3_3, all_57_1_62) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (113) with all_0_3_3, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_3_3, all_57_1_62) = all_83_0_71, mem(all_0_3_3, all_57_1_62) = 0, yields: % 30.19/7.78 | (201) all_83_0_71 = 0 % 30.19/7.78 | % 30.19/7.78 | Equations (201) can reduce 173 to: % 30.19/7.78 | (165) $false % 30.19/7.78 | % 30.19/7.78 |-The branch is then unsatisfiable % 30.19/7.78 |-Branch two: % 30.19/7.78 | (392) all_167_0_92 = 0 & mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (392) yields: % 30.19/7.78 | (326) all_167_0_92 = 0 % 30.19/7.78 | (394) mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_129_1_84 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_129_1_84, all_0_4_4) = 0, yields: % 30.19/7.78 | (399) all_129_1_84 = all_0_5_5 % 30.19/7.78 | % 30.19/7.78 | From (399) and (215) follows: % 30.19/7.78 | (484) mem(all_0_5_5, all_72_1_68) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (113) with all_0_5_5, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_5_5, all_72_1_68) = all_108_0_80, mem(all_0_5_5, all_72_1_68) = 0, yields: % 30.19/7.78 | (286) all_108_0_80 = 0 % 30.19/7.78 | % 30.19/7.78 | Equations (286) can reduce 198 to: % 30.19/7.78 | (165) $false % 30.19/7.78 | % 30.19/7.78 |-The branch is then unsatisfiable % 30.19/7.78 |-Branch two: % 30.19/7.78 | (319) all_155_0_89 = 0 & mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (319) yields: % 30.19/7.78 | (253) all_155_0_89 = 0 % 30.19/7.78 | (321) mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_97_2_77 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_97_2_77, all_0_4_4) = 0, yields: % 30.19/7.78 | (322) all_97_2_77 = all_0_5_5 % 30.19/7.78 | % 30.19/7.78 | From (322) and (188) follows: % 30.19/7.78 | (484) mem(all_0_5_5, all_72_1_68) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (113) with all_0_5_5, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_5_5, all_72_1_68) = all_108_0_80, mem(all_0_5_5, all_72_1_68) = 0, yields: % 30.19/7.78 | (286) all_108_0_80 = 0 % 30.19/7.78 | % 30.19/7.78 | Equations (286) can reduce 198 to: % 30.19/7.78 | (165) $false % 30.19/7.78 | % 30.19/7.78 |-The branch is then unsatisfiable % 30.19/7.78 |-Branch two: % 30.19/7.78 | (494) all_94_0_73 = 0 & mem(all_83_1_72, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (494) yields: % 30.19/7.78 | (243) all_94_0_73 = 0 % 30.19/7.78 | (496) mem(all_83_1_72, all_0_4_4) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_83_1_72 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_83_1_72, all_0_4_4) = 0, yields: % 30.19/7.78 | (497) all_83_1_72 = all_0_5_5 % 30.19/7.78 | % 30.19/7.78 | From (497) and (174) follows: % 30.19/7.78 | (498) mem(all_0_5_5, all_57_1_62) = all_83_0_71 % 30.19/7.78 | % 30.19/7.78 +-Applying beta-rule and splitting (220), into two cases. % 30.19/7.78 |-Branch one: % 30.19/7.78 | (247) all_142_0_87 = 0 & mem(all_108_1_81, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (247) yields: % 30.19/7.78 | (248) all_142_0_87 = 0 % 30.19/7.78 | (249) mem(all_108_1_81, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_108_1_81, all_0_1_1) = 0, yields: % 30.19/7.78 | (250) ? [v0] : ((v0 = 0 & mem(all_108_1_81, all_70_0_66) = 0) | (v0 = 0 & mem(all_108_1_81, all_0_2_2) = 0)) % 30.19/7.78 | % 30.19/7.78 | Instantiating (250) with all_186_0_132 yields: % 30.19/7.78 | (503) (all_186_0_132 = 0 & mem(all_108_1_81, all_70_0_66) = 0) | (all_186_0_132 = 0 & mem(all_108_1_81, all_0_2_2) = 0) % 30.19/7.78 | % 30.19/7.78 +-Applying beta-rule and splitting (231), into two cases. % 30.19/7.78 |-Branch one: % 30.19/7.78 | (252) all_155_0_89 = 0 & mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (252) yields: % 30.19/7.78 | (253) all_155_0_89 = 0 % 30.19/7.78 | (254) mem(all_97_2_77, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_97_2_77, all_0_1_1) = 0, yields: % 30.19/7.78 | (255) ? [v0] : ((v0 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (v0 = 0 & mem(all_97_2_77, all_0_2_2) = 0)) % 30.19/7.78 | % 30.19/7.78 | Instantiating (255) with all_194_0_133 yields: % 30.19/7.78 | (508) (all_194_0_133 = 0 & mem(all_97_2_77, all_70_0_66) = 0) | (all_194_0_133 = 0 & mem(all_97_2_77, all_0_2_2) = 0) % 30.19/7.78 | % 30.19/7.78 +-Applying beta-rule and splitting (241), into two cases. % 30.19/7.78 |-Branch one: % 30.19/7.78 | (325) all_167_0_92 = 0 & mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (325) yields: % 30.19/7.78 | (326) all_167_0_92 = 0 % 30.19/7.78 | (327) mem(all_129_1_84, all_0_1_1) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (72) with all_0_1_1, all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms u(all_0_2_2, all_70_0_66) = all_0_1_1, mem(all_129_1_84, all_0_1_1) = 0, yields: % 30.19/7.78 | (328) ? [v0] : ((v0 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (v0 = 0 & mem(all_129_1_84, all_0_2_2) = 0)) % 30.19/7.78 | % 30.19/7.78 | Instantiating (328) with all_202_0_134 yields: % 30.19/7.78 | (513) (all_202_0_134 = 0 & mem(all_129_1_84, all_70_0_66) = 0) | (all_202_0_134 = 0 & mem(all_129_1_84, all_0_2_2) = 0) % 30.19/7.78 | % 30.19/7.78 +-Applying beta-rule and splitting (503), into two cases. % 30.19/7.78 |-Branch one: % 30.19/7.78 | (514) all_186_0_132 = 0 & mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.78 | % 30.19/7.78 | Applying alpha-rule on (514) yields: % 30.19/7.78 | (515) all_186_0_132 = 0 % 30.19/7.78 | (264) mem(all_108_1_81, all_70_0_66) = 0 % 30.19/7.78 | % 30.19/7.78 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_108_1_81 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_108_1_81, all_70_0_66) = 0, yields: % 30.19/7.78 | (265) all_108_1_81 = all_0_2_2 % 30.19/7.78 | % 30.19/7.78 | From (265) and (199) follows: % 30.19/7.78 | (297) mem(all_0_2_2, all_72_1_68) = all_108_0_80 % 30.19/7.78 | % 30.19/7.79 +-Applying beta-rule and splitting (508), into two cases. % 30.19/7.79 |-Branch one: % 30.19/7.79 | (519) all_194_0_133 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (519) yields: % 30.19/7.79 | (520) all_194_0_133 = 0 % 30.19/7.79 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.79 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.79 | % 30.19/7.79 | From (277) and (188) follows: % 30.19/7.79 | (302) mem(all_0_2_2, all_72_1_68) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_0_2_2, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_2_2, all_72_1_68) = all_108_0_80, mem(all_0_2_2, all_72_1_68) = 0, yields: % 30.19/7.79 | (286) all_108_0_80 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (286) can reduce 198 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (526) all_194_0_133 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (526) yields: % 30.19/7.79 | (520) all_194_0_133 = 0 % 30.19/7.79 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.79 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.79 | % 30.19/7.79 | From (284) and (239) follows: % 30.19/7.79 | (434) mem(all_160_1_91, all_0_3_3) = all_160_0_90 % 30.19/7.79 | % 30.19/7.79 +-Applying beta-rule and splitting (513), into two cases. % 30.19/7.79 |-Branch one: % 30.19/7.79 | (531) all_202_0_134 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (531) yields: % 30.19/7.79 | (532) all_202_0_134 = 0 % 30.19/7.79 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.79 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.79 | % 30.19/7.79 | From (350) and (215) follows: % 30.19/7.79 | (302) mem(all_0_2_2, all_72_1_68) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_0_2_2, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_2_2, all_72_1_68) = all_108_0_80, mem(all_0_2_2, all_72_1_68) = 0, yields: % 30.19/7.79 | (286) all_108_0_80 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (286) can reduce 198 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (538) all_202_0_134 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (538) yields: % 30.19/7.79 | (532) all_202_0_134 = 0 % 30.19/7.79 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.79 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.79 | % 30.19/7.79 | From (357) and (238) follows: % 30.19/7.79 | (446) mem(all_160_1_91, all_0_3_3) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_160_1_91, all_0_3_3, 0, all_160_0_90 and discharging atoms mem(all_160_1_91, all_0_3_3) = all_160_0_90, mem(all_160_1_91, all_0_3_3) = 0, yields: % 30.19/7.79 | (395) all_160_0_90 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (395) can reduce 237 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (545) all_186_0_132 = 0 & mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (545) yields: % 30.19/7.79 | (515) all_186_0_132 = 0 % 30.19/7.79 | (271) mem(all_108_1_81, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_108_1_81 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_108_1_81, all_0_2_2) = 0, yields: % 30.19/7.79 | (272) all_108_1_81 = all_0_3_3 % 30.19/7.79 | % 30.19/7.79 | From (272) and (199) follows: % 30.19/7.79 | (273) mem(all_0_3_3, all_72_1_68) = all_108_0_80 % 30.19/7.79 | % 30.19/7.79 +-Applying beta-rule and splitting (508), into two cases. % 30.19/7.79 |-Branch one: % 30.19/7.79 | (519) all_194_0_133 = 0 & mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (519) yields: % 30.19/7.79 | (520) all_194_0_133 = 0 % 30.19/7.79 | (276) mem(all_97_2_77, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_97_2_77 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_97_2_77, all_70_0_66) = 0, yields: % 30.19/7.79 | (277) all_97_2_77 = all_0_2_2 % 30.19/7.79 | % 30.19/7.79 | From (277) and (239) follows: % 30.19/7.79 | (458) mem(all_160_1_91, all_0_2_2) = all_160_0_90 % 30.19/7.79 | % 30.19/7.79 +-Applying beta-rule and splitting (513), into two cases. % 30.19/7.79 |-Branch one: % 30.19/7.79 | (531) all_202_0_134 = 0 & mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (531) yields: % 30.19/7.79 | (532) all_202_0_134 = 0 % 30.19/7.79 | (349) mem(all_129_1_84, all_70_0_66) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_70_0_66, all_0_2_2, all_129_1_84 and discharging atoms s(all_0_2_2) = all_70_0_66, mem(all_129_1_84, all_70_0_66) = 0, yields: % 30.19/7.79 | (350) all_129_1_84 = all_0_2_2 % 30.19/7.79 | % 30.19/7.79 | From (350) and (238) follows: % 30.19/7.79 | (463) mem(all_160_1_91, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_160_1_91, all_0_2_2, 0, all_160_0_90 and discharging atoms mem(all_160_1_91, all_0_2_2) = all_160_0_90, mem(all_160_1_91, all_0_2_2) = 0, yields: % 30.19/7.79 | (395) all_160_0_90 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (395) can reduce 237 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (538) all_202_0_134 = 0 & mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (538) yields: % 30.19/7.79 | (532) all_202_0_134 = 0 % 30.19/7.79 | (356) mem(all_129_1_84, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_129_1_84 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_129_1_84, all_0_2_2) = 0, yields: % 30.19/7.79 | (357) all_129_1_84 = all_0_3_3 % 30.19/7.79 | % 30.19/7.79 | From (357) and (215) follows: % 30.19/7.79 | (285) mem(all_0_3_3, all_72_1_68) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_0_3_3, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_3_3, all_72_1_68) = all_108_0_80, mem(all_0_3_3, all_72_1_68) = 0, yields: % 30.19/7.79 | (286) all_108_0_80 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (286) can reduce 198 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (526) all_194_0_133 = 0 & mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (526) yields: % 30.19/7.79 | (520) all_194_0_133 = 0 % 30.19/7.79 | (283) mem(all_97_2_77, all_0_2_2) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_2_2, all_0_3_3, all_97_2_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_97_2_77, all_0_2_2) = 0, yields: % 30.19/7.79 | (284) all_97_2_77 = all_0_3_3 % 30.19/7.79 | % 30.19/7.79 | From (284) and (188) follows: % 30.19/7.79 | (285) mem(all_0_3_3, all_72_1_68) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_0_3_3, all_72_1_68, 0, all_108_0_80 and discharging atoms mem(all_0_3_3, all_72_1_68) = all_108_0_80, mem(all_0_3_3, all_72_1_68) = 0, yields: % 30.19/7.79 | (286) all_108_0_80 = 0 % 30.19/7.79 | % 30.19/7.79 | Equations (286) can reduce 198 to: % 30.19/7.79 | (165) $false % 30.19/7.79 | % 30.19/7.79 |-The branch is then unsatisfiable % 30.19/7.79 |-Branch two: % 30.19/7.79 | (392) all_167_0_92 = 0 & mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.79 | % 30.19/7.79 | Applying alpha-rule on (392) yields: % 30.19/7.79 | (326) all_167_0_92 = 0 % 30.19/7.79 | (394) mem(all_129_1_84, all_0_4_4) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_129_1_84 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_129_1_84, all_0_4_4) = 0, yields: % 30.19/7.79 | (399) all_129_1_84 = all_0_5_5 % 30.19/7.79 | % 30.19/7.79 | From (399) and (217) follows: % 30.19/7.79 | (580) mem(all_0_5_5, all_57_1_62) = 0 % 30.19/7.79 | % 30.19/7.79 | Instantiating formula (113) with all_0_5_5, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_5_5, all_57_1_62) = all_83_0_71, mem(all_0_5_5, all_57_1_62) = 0, yields: % 30.19/7.80 | (201) all_83_0_71 = 0 % 30.19/7.80 | % 30.19/7.80 | Equations (201) can reduce 173 to: % 30.19/7.80 | (165) $false % 30.19/7.80 | % 30.19/7.80 |-The branch is then unsatisfiable % 30.19/7.80 |-Branch two: % 30.19/7.80 | (319) all_155_0_89 = 0 & mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.80 | % 30.19/7.80 | Applying alpha-rule on (319) yields: % 30.19/7.80 | (253) all_155_0_89 = 0 % 30.19/7.80 | (321) mem(all_97_2_77, all_0_4_4) = 0 % 30.19/7.80 | % 30.19/7.80 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_97_2_77 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_97_2_77, all_0_4_4) = 0, yields: % 30.19/7.80 | (322) all_97_2_77 = all_0_5_5 % 30.19/7.80 | % 30.19/7.80 | From (322) and (207) follows: % 30.19/7.80 | (580) mem(all_0_5_5, all_57_1_62) = 0 % 30.19/7.80 | % 30.19/7.80 | Instantiating formula (113) with all_0_5_5, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_5_5, all_57_1_62) = all_83_0_71, mem(all_0_5_5, all_57_1_62) = 0, yields: % 30.19/7.80 | (201) all_83_0_71 = 0 % 30.19/7.80 | % 30.19/7.80 | Equations (201) can reduce 173 to: % 30.19/7.80 | (165) $false % 30.19/7.80 | % 30.19/7.80 |-The branch is then unsatisfiable % 30.19/7.80 |-Branch two: % 30.19/7.80 | (403) all_142_0_87 = 0 & mem(all_108_1_81, all_0_4_4) = 0 % 30.19/7.80 | % 30.19/7.80 | Applying alpha-rule on (403) yields: % 30.19/7.80 | (248) all_142_0_87 = 0 % 30.19/7.80 | (405) mem(all_108_1_81, all_0_4_4) = 0 % 30.19/7.80 | % 30.19/7.80 | Instantiating formula (25) with all_0_4_4, all_0_5_5, all_108_1_81 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_108_1_81, all_0_4_4) = 0, yields: % 30.19/7.80 | (406) all_108_1_81 = all_0_5_5 % 30.19/7.80 | % 30.19/7.80 | From (406) and (200) follows: % 30.19/7.80 | (580) mem(all_0_5_5, all_57_1_62) = 0 % 30.19/7.80 | % 30.19/7.80 | Instantiating formula (113) with all_0_5_5, all_57_1_62, 0, all_83_0_71 and discharging atoms mem(all_0_5_5, all_57_1_62) = all_83_0_71, mem(all_0_5_5, all_57_1_62) = 0, yields: % 30.19/7.80 | (201) all_83_0_71 = 0 % 30.19/7.80 | % 30.19/7.80 | Equations (201) can reduce 173 to: % 30.19/7.80 | (165) $false % 30.19/7.80 | % 30.19/7.80 |-The branch is then unsatisfiable % 30.50/7.80 % SZS output end Proof for theBenchmark % 30.50/7.80 % 30.50/7.80 7200ms %------------------------------------------------------------------------------