%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV551+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n005.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 24.65s 6.56s % Output : Proof 27.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEV551+1 : TPTP v9.1.0. Released v9.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.33 % Computer : n005.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Mon Mar 31 11:51:58 EDT 2025 % 0.11/0.33 % CPUTime : % 0.55/0.56 ____ _ % 0.55/0.56 ___ / __ \_____(_)___ ________ __________ % 0.55/0.56 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.56 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.56 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.56 % 0.55/0.56 A Theorem Prover for First-Order Logic % 0.55/0.57 (ePrincess v.1.0) % 0.55/0.57 % 0.55/0.57 (c) Philipp Rümmer, 2009-2015 % 0.55/0.57 (c) Peter Backeman, 2014-2015 % 0.55/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.57 Bug reports to peter@backeman.se % 0.55/0.57 % 0.55/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.57 % 0.55/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.58/0.61 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.61/0.93 Prover 0: Preprocessing ... % 2.27/1.17 Prover 0: Warning: ignoring some quantifiers % 2.38/1.20 Prover 0: Constructing countermodel ... % 21.86/5.91 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 21.86/5.96 Prover 1: Preprocessing ... % 22.84/6.13 Prover 1: Constructing countermodel ... % 23.30/6.29 Prover 1: gave up % 23.30/6.29 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 23.61/6.31 Prover 2: Preprocessing ... % 24.12/6.42 Prover 2: Warning: ignoring some quantifiers % 24.12/6.42 Prover 2: Constructing countermodel ... % 24.65/6.55 Prover 2: proved (266ms) % 24.65/6.56 Prover 0: stopped % 24.65/6.56 % 24.65/6.56 No countermodel exists, formula is valid % 24.65/6.56 % SZS status Theorem for theBenchmark % 24.65/6.56 % 24.65/6.56 Generating proof ... Warning: ignoring some quantifiers % 25.94/6.93 found it (size 126) % 25.94/6.93 % 25.94/6.93 % SZS output start Proof for theBenchmark % 25.94/6.93 Assumed formulas after preprocessing and simplification: % 25.94/6.93 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (atleast3p(v5) = 0 & n(v1) = v4 & n(v0) = v1 & n(e) = v0 & a(v3, v4) = v5 & a(v0, v1) = v2 & s(v2) = v3 & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (m(v7, v8) = v9) | ~ (mem(v6, v9) = v10) | ? [v11] : ((v11 = 0 & mem(v6, v8) = 0) | ( ~ (v11 = 0) & mem(v6, v7) = v11))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (u(v7, v8) = v9) | ~ (mem(v6, v9) = v10) | ? [v11] : ? [v12] : ( ~ (v12 = 0) & ~ (v11 = 0) & mem(v6, v8) = v12 & mem(v6, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast16p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast15p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast15p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast14p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast14p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast13p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast13p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast12p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast12p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast11p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast11p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast10p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast10p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast9p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast9p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast8p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast8p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast7p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast7p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast6p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast6p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast5p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast5p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast4p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast4p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast3p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v7 = 0 | ~ (atleast3p(v6) = v7) | ~ (subq(v6, v8) = v9) | ? [v10] : (( ~ (v10 = 0) & atleast2p(v8) = v10) | ( ~ (v10 = 0) & subq(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (p(v7) = v8) | ~ (mem(v6, v8) = v9) | ? [v10] : ( ~ (v10 = 0) & subq(v6, v7) = v10)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (subq(v6, v7) = 0) | ~ (mem(v8, v7) = v9) | ? [v10] : ( ~ (v10 = 0) & mem(v8, v6) = v10)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (a(v9, v8) = v7) | ~ (a(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (m(v9, v8) = v7) | ~ (m(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (u(v9, v8) = v7) | ~ (u(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (disj(v9, v8) = v7) | ~ (disj(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (subq(v9, v8) = v7) | ~ (subq(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (mem(v9, v8) = v7) | ~ (mem(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = 0 | ~ (atleast2p(v6) = v7) | ~ (p(v8) = v9) | ? [v10] : ((v10 = 0 & subq(v6, v9) = 0) | ( ~ (v10 = 0) & mem(v8, v6) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (m(v7, v8) = v9) | ~ (mem(v6, v9) = 0) | ? [v10] : ( ~ (v10 = 0) & mem(v6, v8) = v10 & mem(v6, v7) = 0)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (u(v7, v8) = v9) | ~ (mem(v6, v9) = 0) | ? [v10] : ((v10 = 0 & mem(v6, v8) = 0) | (v10 = 0 & mem(v6, v7) = 0))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (u(v6, v8) = v9) | ~ (s(v7) = v8) | a(v6, v7) = v9) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (s(v6) = v7) | ~ (mem(v6, v7) = v8)) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (disj(v6, v7) = v8) | ? [v9] : (mem(v9, v7) = 0 & mem(v9, v6) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (subq(v6, v7) = v8) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & p(v7) = v9 & mem(v6, v9) = v10)) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (subq(v6, v7) = v8) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & mem(v9, v7) = v10 & mem(v9, v6) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast16p(v8) = v7) | ~ (atleast16p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast15p(v8) = v7) | ~ (atleast15p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast14p(v8) = v7) | ~ (atleast14p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast13p(v8) = v7) | ~ (atleast13p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast12p(v8) = v7) | ~ (atleast12p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast11p(v8) = v7) | ~ (atleast11p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast10p(v8) = v7) | ~ (atleast10p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast9p(v8) = v7) | ~ (atleast9p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast8p(v8) = v7) | ~ (atleast8p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast7p(v8) = v7) | ~ (atleast7p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast6p(v8) = v7) | ~ (atleast6p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast5p(v8) = v7) | ~ (atleast5p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast4p(v8) = v7) | ~ (atleast4p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast3p(v8) = v7) | ~ (atleast3p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (atleast2p(v8) = v7) | ~ (atleast2p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (p(v8) = v7) | ~ (p(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (n(v8) = v7) | ~ (n(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (s(v8) = v7) | ~ (s(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (s(v7) = v8) | ~ (mem(v6, v8) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast16p(v6) = v7) | ~ (atleast15p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast16p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast15p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast15p(v6) = v7) | ~ (atleast14p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast15p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast14p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast14p(v6) = v7) | ~ (atleast13p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast14p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast13p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast13p(v6) = v7) | ~ (atleast12p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast13p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast12p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast12p(v6) = v7) | ~ (atleast11p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast12p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast11p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast11p(v6) = v7) | ~ (atleast10p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast11p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast10p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast10p(v6) = v7) | ~ (atleast9p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast10p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast9p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast9p(v6) = v7) | ~ (atleast8p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast9p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast8p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast8p(v6) = v7) | ~ (atleast7p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast8p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast7p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast7p(v6) = v7) | ~ (atleast6p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast7p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast6p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast6p(v6) = v7) | ~ (atleast5p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast6p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast5p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast5p(v6) = v7) | ~ (atleast4p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast5p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast4p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast4p(v6) = v7) | ~ (atleast3p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast4p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast3p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast3p(v6) = v7) | ~ (atleast2p(v8) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & subq(v8, v6) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast3p(v6) = v7) | ~ (subq(v8, v6) = 0) | ? [v9] : ((v9 = 0 & subq(v6, v8) = 0) | ( ~ (v9 = 0) & atleast2p(v8) = v9))) & ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (atleast2p(v6) = v7) | ~ (mem(v8, v6) = 0) | ? [v9] : (p(v8) = v9 & subq(v6, v9) = 0)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (p(v7) = v8) | ~ (mem(v6, v8) = 0) | subq(v6, v7) = 0) & ! [v6] : ! [v7] : ! [v8] : ( ~ (a(v6, v7) = v8) | ? [v9] : (u(v6, v9) = v8 & s(v7) = v9)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (disj(v6, v7) = 0) | ~ (mem(v8, v7) = 0) | ? [v9] : ( ~ (v9 = 0) & mem(v8, v6) = v9)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (disj(v6, v7) = 0) | ~ (mem(v8, v6) = 0) | ? [v9] : ( ~ (v9 = 0) & mem(v8, v7) = v9)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (subq(v6, v7) = 0) | ~ (mem(v8, v6) = 0) | mem(v8, v7) = 0) & ! [v6] : ! [v7] : (v7 = v6 | ~ (subq(v7, v6) = 0) | ? [v8] : ( ~ (v8 = 0) & subq(v6, v7) = v8)) & ! [v6] : ! [v7] : (v7 = v6 | ~ (subq(v6, v7) = 0) | ? [v8] : ( ~ (v8 = 0) & subq(v7, v6) = v8)) & ! [v6] : ! [v7] : ( ~ (n(v6) = v7) | a(v6, v6) = v7) & ! [v6] : ! [v7] : ( ~ (a(v6, v6) = v7) | n(v6) = v7) & ! [v6] : ! [v7] : ( ~ (subq(v6, v7) = 0) | ? [v8] : (p(v7) = v8 & mem(v6, v8) = 0)) & ! [v6] : ( ~ (atleast16p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast15p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast15p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast14p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast14p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast13p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast13p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast12p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast12p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast11p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast11p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast10p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast10p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast9p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast9p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast8p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast8p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast7p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast7p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast6p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast6p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast5p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast5p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast4p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast4p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast3p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast3p(v6) = 0) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & atleast2p(v7) = 0 & subq(v7, v6) = 0 & subq(v6, v7) = v8)) & ! [v6] : ( ~ (atleast2p(v6) = 0) | ? [v7] : ? [v8] : ? [v9] : ( ~ (v9 = 0) & p(v7) = v8 & subq(v6, v8) = v9 & mem(v7, v6) = 0)) & ! [v6] : ~ (mem(v6, e) = 0) & ? [v6] : ? [v7] : ? [v8] : a(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : m(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : u(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : disj(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : subq(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : mem(v7, v6) = v8 & ? [v6] : ? [v7] : atleast16p(v6) = v7 & ? [v6] : ? [v7] : atleast15p(v6) = v7 & ? [v6] : ? [v7] : atleast14p(v6) = v7 & ? [v6] : ? [v7] : atleast13p(v6) = v7 & ? [v6] : ? [v7] : atleast12p(v6) = v7 & ? [v6] : ? [v7] : atleast11p(v6) = v7 & ? [v6] : ? [v7] : atleast10p(v6) = v7 & ? [v6] : ? [v7] : atleast9p(v6) = v7 & ? [v6] : ? [v7] : atleast8p(v6) = v7 & ? [v6] : ? [v7] : atleast7p(v6) = v7 & ? [v6] : ? [v7] : atleast6p(v6) = v7 & ? [v6] : ? [v7] : atleast5p(v6) = v7 & ? [v6] : ? [v7] : atleast4p(v6) = v7 & ? [v6] : ? [v7] : atleast3p(v6) = v7 & ? [v6] : ? [v7] : atleast2p(v6) = v7 & ? [v6] : ? [v7] : p(v6) = v7 & ? [v6] : ? [v7] : n(v6) = v7 & ? [v6] : ? [v7] : s(v6) = v7) % 26.67/7.00 | 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 yields: % 26.67/7.00 | (1) atleast3p(all_0_0_0) = 0 & n(all_0_4_4) = all_0_1_1 & n(all_0_5_5) = all_0_4_4 & n(e) = all_0_5_5 & a(all_0_2_2, all_0_1_1) = all_0_0_0 & a(all_0_5_5, all_0_4_4) = all_0_3_3 & s(all_0_3_3) = all_0_2_2 & ! [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 % 26.67/7.02 | % 26.67/7.02 | Applying alpha-rule on (1) yields: % 26.67/7.02 | (2) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.02 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 26.67/7.02 | (4) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.02 | (5) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.02 | (6) ! [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))) % 26.67/7.02 | (7) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 26.67/7.02 | (8) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 26.67/7.02 | (9) ! [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))) % 26.67/7.02 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 26.67/7.02 | (11) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 26.67/7.02 | (12) ! [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))) % 26.67/7.02 | (13) ! [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))) % 26.67/7.03 | (14) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 26.67/7.03 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 26.67/7.03 | (16) ! [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))) % 26.67/7.03 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 26.67/7.03 | (18) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.03 | (19) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 26.67/7.03 | (20) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 26.67/7.03 | (21) ! [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))) % 26.67/7.03 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 26.67/7.03 | (23) ! [v0] : ~ (mem(v0, e) = 0) % 26.67/7.03 | (24) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.03 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 26.67/7.03 | (26) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 26.67/7.03 | (27) ! [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))) % 26.67/7.03 | (28) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 26.67/7.03 | (29) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 26.67/7.03 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.03 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 26.67/7.03 | (32) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 26.67/7.03 | (33) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 26.67/7.03 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 26.67/7.03 | (35) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.03 | (36) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.03 | (37) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 26.67/7.03 | (38) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 26.67/7.03 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 26.67/7.03 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 26.67/7.03 | (41) ! [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))) % 26.67/7.03 | (42) ? [v0] : ? [v1] : s(v0) = v1 % 26.67/7.03 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 26.67/7.03 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 26.67/7.03 | (45) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 26.67/7.03 | (46) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 26.67/7.03 | (47) ! [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))) % 26.67/7.03 | (48) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 26.67/7.03 | (49) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.03 | (50) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.03 | (51) ! [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))) % 26.67/7.03 | (52) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.03 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.03 | (54) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 26.67/7.03 | (55) ! [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))) % 26.67/7.03 | (56) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 26.67/7.03 | (57) ! [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))) % 26.67/7.04 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 26.67/7.04 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 26.67/7.04 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 26.67/7.04 | (61) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 26.67/7.04 | (62) ! [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))) % 26.67/7.04 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 26.67/7.04 | (64) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 26.67/7.04 | (65) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 26.67/7.04 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.04 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 26.67/7.04 | (68) n(e) = all_0_5_5 % 26.67/7.04 | (69) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 26.67/7.04 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.04 | (71) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 26.67/7.04 | (72) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.04 | (73) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 26.67/7.04 | (74) a(all_0_5_5, all_0_4_4) = all_0_3_3 % 26.67/7.04 | (75) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 26.67/7.04 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 26.67/7.04 | (77) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 26.67/7.04 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 26.67/7.04 | (79) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.04 | (80) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.04 | (81) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 26.67/7.04 | (82) ? [v0] : ? [v1] : n(v0) = v1 % 26.67/7.04 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 26.67/7.04 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.04 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 26.67/7.04 | (86) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 26.67/7.04 | (87) n(all_0_4_4) = all_0_1_1 % 26.67/7.04 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 26.67/7.04 | (89) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.04 | (90) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 26.67/7.04 | (91) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 26.67/7.04 | (92) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 26.67/7.04 | (93) ! [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))) % 26.67/7.04 | (94) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 26.67/7.04 | (95) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 26.67/7.04 | (96) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 26.67/7.04 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 26.67/7.04 | (98) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 26.67/7.04 | (99) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 26.67/7.04 | (100) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 26.67/7.04 | (101) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.04 | (102) a(all_0_2_2, all_0_1_1) = all_0_0_0 % 26.67/7.05 | (103) ? [v0] : ? [v1] : p(v0) = v1 % 26.67/7.05 | (104) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.05 | (105) ! [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))) % 26.67/7.05 | (106) s(all_0_3_3) = all_0_2_2 % 26.67/7.05 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.05 | (108) ! [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)) % 26.67/7.05 | (109) atleast3p(all_0_0_0) = 0 % 26.67/7.05 | (110) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 26.67/7.05 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 26.67/7.05 | (112) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 26.67/7.05 | (113) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.05 | (114) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.05 | (115) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 26.67/7.05 | (116) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 26.67/7.05 | (117) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 26.67/7.05 | (118) n(all_0_5_5) = all_0_4_4 % 26.67/7.05 | (119) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 26.67/7.05 | (120) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 26.67/7.05 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 26.67/7.05 | (122) ! [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))) % 26.67/7.05 | (123) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.05 | (124) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 26.67/7.05 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 26.67/7.05 | (126) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 26.67/7.05 | (127) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 26.67/7.05 | (128) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 26.67/7.05 | (129) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 26.67/7.05 | (130) ! [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))) % 26.67/7.05 | (131) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 26.67/7.05 | (132) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 26.67/7.05 | (133) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 26.67/7.05 | (134) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 26.67/7.05 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 26.67/7.05 | (136) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.05 | (137) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 26.67/7.05 | (138) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 26.67/7.05 | % 26.67/7.05 | Instantiating formula (101) with all_0_0_0 and discharging atoms atleast3p(all_0_0_0) = 0, yields: % 26.67/7.05 | (139) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast2p(v0) = 0 & subq(v0, all_0_0_0) = 0 & subq(all_0_0_0, v0) = v1) % 26.67/7.05 | % 26.67/7.05 | Instantiating formula (46) with all_0_1_1, all_0_4_4 and discharging atoms n(all_0_4_4) = all_0_1_1, yields: % 26.67/7.05 | (140) a(all_0_4_4, all_0_4_4) = all_0_1_1 % 26.67/7.05 | % 26.67/7.05 | Instantiating formula (15) with all_0_0_0, all_0_1_1, all_0_2_2 and discharging atoms a(all_0_2_2, all_0_1_1) = all_0_0_0, yields: % 26.67/7.05 | (141) ? [v0] : (u(all_0_2_2, v0) = all_0_0_0 & s(all_0_1_1) = v0) % 26.67/7.05 | % 26.67/7.05 | Instantiating formula (15) with all_0_3_3, all_0_4_4, all_0_5_5 and discharging atoms a(all_0_5_5, all_0_4_4) = all_0_3_3, yields: % 26.67/7.05 | (142) ? [v0] : (u(all_0_5_5, v0) = all_0_3_3 & s(all_0_4_4) = v0) % 26.67/7.05 | % 26.67/7.05 | Instantiating (142) with all_57_0_60 yields: % 26.67/7.05 | (143) u(all_0_5_5, all_57_0_60) = all_0_3_3 & s(all_0_4_4) = all_57_0_60 % 26.67/7.05 | % 26.67/7.05 | Applying alpha-rule on (143) yields: % 26.67/7.05 | (144) u(all_0_5_5, all_57_0_60) = all_0_3_3 % 26.67/7.05 | (145) s(all_0_4_4) = all_57_0_60 % 26.67/7.05 | % 26.67/7.05 | Instantiating (141) with all_59_0_61 yields: % 26.67/7.05 | (146) u(all_0_2_2, all_59_0_61) = all_0_0_0 & s(all_0_1_1) = all_59_0_61 % 26.67/7.05 | % 26.67/7.05 | Applying alpha-rule on (146) yields: % 26.67/7.05 | (147) u(all_0_2_2, all_59_0_61) = all_0_0_0 % 26.67/7.05 | (148) s(all_0_1_1) = all_59_0_61 % 26.67/7.05 | % 26.67/7.05 | Instantiating (139) with all_61_0_62, all_61_1_63 yields: % 26.67/7.05 | (149) ~ (all_61_0_62 = 0) & atleast2p(all_61_1_63) = 0 & subq(all_61_1_63, all_0_0_0) = 0 & subq(all_0_0_0, all_61_1_63) = all_61_0_62 % 26.67/7.05 | % 26.67/7.05 | Applying alpha-rule on (149) yields: % 26.67/7.05 | (150) ~ (all_61_0_62 = 0) % 26.67/7.05 | (151) atleast2p(all_61_1_63) = 0 % 26.67/7.05 | (152) subq(all_61_1_63, all_0_0_0) = 0 % 26.67/7.05 | (153) subq(all_0_0_0, all_61_1_63) = all_61_0_62 % 26.67/7.06 | % 26.67/7.06 | Instantiating formula (94) with all_61_1_63 and discharging atoms atleast2p(all_61_1_63) = 0, yields: % 26.67/7.06 | (154) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & p(v0) = v1 & subq(all_61_1_63, v1) = v2 & mem(v0, all_61_1_63) = 0) % 26.67/7.06 | % 26.67/7.06 | Instantiating formula (15) with all_0_1_1, all_0_4_4, all_0_4_4 and discharging atoms a(all_0_4_4, all_0_4_4) = all_0_1_1, yields: % 26.67/7.06 | (155) ? [v0] : (u(all_0_4_4, v0) = all_0_1_1 & s(all_0_4_4) = v0) % 26.67/7.06 | % 26.67/7.06 | Instantiating formula (71) with all_61_0_62, all_61_1_63, all_0_0_0 and discharging atoms subq(all_0_0_0, all_61_1_63) = all_61_0_62, yields: % 26.67/7.06 | (156) all_61_0_62 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_61_1_63) = v0 & mem(all_0_0_0, v0) = v1) % 26.67/7.06 | % 26.67/7.06 | Instantiating formula (7) with all_61_0_62, all_61_1_63, all_0_0_0 and discharging atoms subq(all_0_0_0, all_61_1_63) = all_61_0_62, yields: % 26.67/7.06 | (157) all_61_0_62 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_61_1_63) = v1 & mem(v0, all_0_0_0) = 0) % 26.67/7.06 | % 26.67/7.06 | Instantiating (155) with all_74_0_67 yields: % 26.67/7.06 | (158) u(all_0_4_4, all_74_0_67) = all_0_1_1 & s(all_0_4_4) = all_74_0_67 % 26.67/7.06 | % 26.67/7.06 | Applying alpha-rule on (158) yields: % 26.67/7.06 | (159) u(all_0_4_4, all_74_0_67) = all_0_1_1 % 26.67/7.06 | (160) s(all_0_4_4) = all_74_0_67 % 26.67/7.06 | % 26.67/7.06 | Instantiating (154) with all_76_0_68, all_76_1_69, all_76_2_70 yields: % 26.67/7.06 | (161) ~ (all_76_0_68 = 0) & p(all_76_2_70) = all_76_1_69 & subq(all_61_1_63, all_76_1_69) = all_76_0_68 & mem(all_76_2_70, all_61_1_63) = 0 % 26.67/7.06 | % 26.67/7.06 | Applying alpha-rule on (161) yields: % 26.67/7.06 | (162) ~ (all_76_0_68 = 0) % 26.67/7.06 | (163) p(all_76_2_70) = all_76_1_69 % 26.67/7.06 | (164) subq(all_61_1_63, all_76_1_69) = all_76_0_68 % 26.67/7.06 | (165) mem(all_76_2_70, all_61_1_63) = 0 % 26.67/7.06 | % 26.67/7.06 +-Applying beta-rule and splitting (156), into two cases. % 26.67/7.06 |-Branch one: % 26.67/7.06 | (166) all_61_0_62 = 0 % 26.67/7.06 | % 26.96/7.06 | Equations (166) can reduce 150 to: % 26.96/7.06 | (167) $false % 26.96/7.06 | % 26.96/7.06 |-The branch is then unsatisfiable % 26.96/7.06 |-Branch two: % 26.96/7.06 | (150) ~ (all_61_0_62 = 0) % 26.96/7.06 | (169) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_61_1_63) = v0 & mem(all_0_0_0, v0) = v1) % 26.96/7.06 | % 26.96/7.06 +-Applying beta-rule and splitting (157), into two cases. % 26.96/7.06 |-Branch one: % 26.96/7.06 | (166) all_61_0_62 = 0 % 26.96/7.06 | % 26.96/7.06 | Equations (166) can reduce 150 to: % 26.96/7.06 | (167) $false % 26.96/7.06 | % 26.96/7.06 |-The branch is then unsatisfiable % 26.96/7.06 |-Branch two: % 26.96/7.06 | (150) ~ (all_61_0_62 = 0) % 26.96/7.06 | (173) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_61_1_63) = v1 & mem(v0, all_0_0_0) = 0) % 26.96/7.06 | % 26.96/7.06 | Instantiating (173) with all_87_0_73, all_87_1_74 yields: % 26.96/7.06 | (174) ~ (all_87_0_73 = 0) & mem(all_87_1_74, all_61_1_63) = all_87_0_73 & mem(all_87_1_74, all_0_0_0) = 0 % 26.96/7.06 | % 26.96/7.06 | Applying alpha-rule on (174) yields: % 26.96/7.06 | (175) ~ (all_87_0_73 = 0) % 26.96/7.06 | (176) mem(all_87_1_74, all_61_1_63) = all_87_0_73 % 26.96/7.06 | (177) mem(all_87_1_74, all_0_0_0) = 0 % 26.96/7.06 | % 26.96/7.06 | Instantiating formula (3) with all_0_4_4, all_74_0_67, all_57_0_60 and discharging atoms s(all_0_4_4) = all_74_0_67, s(all_0_4_4) = all_57_0_60, yields: % 26.96/7.06 | (178) all_74_0_67 = all_57_0_60 % 26.96/7.06 | % 26.96/7.06 | From (178) and (159) follows: % 26.96/7.06 | (179) u(all_0_4_4, all_57_0_60) = all_0_1_1 % 26.96/7.06 | % 26.96/7.06 | Instantiating formula (71) with all_76_0_68, all_76_1_69, all_61_1_63 and discharging atoms subq(all_61_1_63, all_76_1_69) = all_76_0_68, yields: % 26.96/7.06 | (180) all_76_0_68 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_76_1_69) = v0 & mem(all_61_1_63, v0) = v1) % 26.96/7.06 | % 26.96/7.06 | Instantiating formula (7) with all_76_0_68, all_76_1_69, all_61_1_63 and discharging atoms subq(all_61_1_63, all_76_1_69) = all_76_0_68, yields: % 26.96/7.06 | (181) all_76_0_68 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_76_1_69) = v1 & mem(v0, all_61_1_63) = 0) % 26.96/7.06 | % 26.96/7.06 | Instantiating formula (41) with all_0_0_0, all_59_0_61, all_0_2_2, all_87_1_74 and discharging atoms u(all_0_2_2, all_59_0_61) = all_0_0_0, mem(all_87_1_74, all_0_0_0) = 0, yields: % 26.96/7.06 | (182) ? [v0] : ((v0 = 0 & mem(all_87_1_74, all_59_0_61) = 0) | (v0 = 0 & mem(all_87_1_74, all_0_2_2) = 0)) % 26.96/7.06 | % 26.96/7.06 | Instantiating formula (17) with all_76_2_70, all_0_0_0, all_61_1_63 and discharging atoms subq(all_61_1_63, all_0_0_0) = 0, mem(all_76_2_70, all_61_1_63) = 0, yields: % 26.96/7.06 | (183) mem(all_76_2_70, all_0_0_0) = 0 % 26.96/7.06 | % 26.96/7.06 | Instantiating (182) with all_99_0_75 yields: % 26.96/7.06 | (184) (all_99_0_75 = 0 & mem(all_87_1_74, all_59_0_61) = 0) | (all_99_0_75 = 0 & mem(all_87_1_74, all_0_2_2) = 0) % 26.96/7.06 | % 26.96/7.06 +-Applying beta-rule and splitting (180), into two cases. % 26.96/7.06 |-Branch one: % 26.96/7.06 | (185) all_76_0_68 = 0 % 26.96/7.06 | % 26.96/7.06 | Equations (185) can reduce 162 to: % 26.96/7.06 | (167) $false % 26.96/7.06 | % 26.96/7.06 |-The branch is then unsatisfiable % 26.96/7.06 |-Branch two: % 26.96/7.06 | (162) ~ (all_76_0_68 = 0) % 26.96/7.06 | (188) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_76_1_69) = v0 & mem(all_61_1_63, v0) = v1) % 26.96/7.06 | % 26.96/7.06 +-Applying beta-rule and splitting (181), into two cases. % 26.96/7.06 |-Branch one: % 26.96/7.06 | (185) all_76_0_68 = 0 % 26.96/7.06 | % 26.96/7.06 | Equations (185) can reduce 162 to: % 26.96/7.06 | (167) $false % 26.96/7.06 | % 26.96/7.06 |-The branch is then unsatisfiable % 26.96/7.06 |-Branch two: % 26.96/7.06 | (162) ~ (all_76_0_68 = 0) % 26.96/7.06 | (192) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_76_1_69) = v1 & mem(v0, all_61_1_63) = 0) % 26.96/7.06 | % 26.96/7.06 | Instantiating (192) with all_109_0_78, all_109_1_79 yields: % 26.96/7.06 | (193) ~ (all_109_0_78 = 0) & mem(all_109_1_79, all_76_1_69) = all_109_0_78 & mem(all_109_1_79, all_61_1_63) = 0 % 26.96/7.06 | % 26.96/7.06 | Applying alpha-rule on (193) yields: % 26.96/7.06 | (194) ~ (all_109_0_78 = 0) % 26.96/7.06 | (195) mem(all_109_1_79, all_76_1_69) = all_109_0_78 % 26.96/7.06 | (196) mem(all_109_1_79, all_61_1_63) = 0 % 26.96/7.07 | % 26.96/7.07 | Instantiating formula (31) with all_109_0_78, all_76_1_69, all_76_2_70, all_109_1_79 and discharging atoms p(all_76_2_70) = all_76_1_69, mem(all_109_1_79, all_76_1_69) = all_109_0_78, yields: % 26.96/7.07 | (197) all_109_0_78 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_109_1_79, all_76_2_70) = v0) % 26.96/7.07 | % 26.96/7.07 | Instantiating formula (17) with all_109_1_79, all_0_0_0, all_61_1_63 and discharging atoms subq(all_61_1_63, all_0_0_0) = 0, mem(all_109_1_79, all_61_1_63) = 0, yields: % 26.96/7.07 | (198) mem(all_109_1_79, all_0_0_0) = 0 % 26.96/7.07 | % 26.96/7.07 | Instantiating formula (41) with all_0_0_0, all_59_0_61, all_0_2_2, all_76_2_70 and discharging atoms u(all_0_2_2, all_59_0_61) = all_0_0_0, mem(all_76_2_70, all_0_0_0) = 0, yields: % 26.96/7.07 | (199) ? [v0] : ((v0 = 0 & mem(all_76_2_70, all_59_0_61) = 0) | (v0 = 0 & mem(all_76_2_70, all_0_2_2) = 0)) % 26.96/7.07 | % 26.96/7.07 | Instantiating (199) with all_117_0_80 yields: % 26.96/7.07 | (200) (all_117_0_80 = 0 & mem(all_76_2_70, all_59_0_61) = 0) | (all_117_0_80 = 0 & mem(all_76_2_70, all_0_2_2) = 0) % 26.96/7.07 | % 26.96/7.07 +-Applying beta-rule and splitting (197), into two cases. % 26.96/7.07 |-Branch one: % 26.96/7.07 | (201) all_109_0_78 = 0 % 26.96/7.07 | % 26.96/7.07 | Equations (201) can reduce 194 to: % 26.96/7.07 | (167) $false % 26.96/7.07 | % 26.96/7.07 |-The branch is then unsatisfiable % 26.96/7.07 |-Branch two: % 26.96/7.07 | (194) ~ (all_109_0_78 = 0) % 26.96/7.07 | (204) ? [v0] : ( ~ (v0 = 0) & subq(all_109_1_79, all_76_2_70) = v0) % 26.96/7.07 | % 26.96/7.07 | Instantiating (204) with all_122_0_81 yields: % 26.96/7.07 | (205) ~ (all_122_0_81 = 0) & subq(all_109_1_79, all_76_2_70) = all_122_0_81 % 26.96/7.07 | % 26.96/7.07 | Applying alpha-rule on (205) yields: % 26.96/7.07 | (206) ~ (all_122_0_81 = 0) % 26.96/7.07 | (207) subq(all_109_1_79, all_76_2_70) = all_122_0_81 % 26.96/7.07 | % 26.96/7.07 | Instantiating formula (7) with all_122_0_81, all_76_2_70, all_109_1_79 and discharging atoms subq(all_109_1_79, all_76_2_70) = all_122_0_81, yields: % 26.96/7.07 | (208) all_122_0_81 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_109_1_79) = 0 & mem(v0, all_76_2_70) = v1) % 26.96/7.07 | % 26.96/7.07 | Instantiating formula (41) with all_0_0_0, all_59_0_61, all_0_2_2, all_109_1_79 and discharging atoms u(all_0_2_2, all_59_0_61) = all_0_0_0, mem(all_109_1_79, all_0_0_0) = 0, yields: % 26.96/7.07 | (209) ? [v0] : ((v0 = 0 & mem(all_109_1_79, all_59_0_61) = 0) | (v0 = 0 & mem(all_109_1_79, all_0_2_2) = 0)) % 26.96/7.07 | % 26.96/7.07 | Instantiating (209) with all_129_0_82 yields: % 26.96/7.07 | (210) (all_129_0_82 = 0 & mem(all_109_1_79, all_59_0_61) = 0) | (all_129_0_82 = 0 & mem(all_109_1_79, all_0_2_2) = 0) % 26.96/7.07 | % 26.96/7.07 +-Applying beta-rule and splitting (184), into two cases. % 26.96/7.07 |-Branch one: % 26.96/7.07 | (211) all_99_0_75 = 0 & mem(all_87_1_74, all_59_0_61) = 0 % 26.96/7.07 | % 26.96/7.07 | Applying alpha-rule on (211) yields: % 26.96/7.07 | (212) all_99_0_75 = 0 % 26.96/7.07 | (213) mem(all_87_1_74, all_59_0_61) = 0 % 26.96/7.07 | % 26.96/7.07 +-Applying beta-rule and splitting (208), into two cases. % 26.96/7.07 |-Branch one: % 26.96/7.07 | (214) all_122_0_81 = 0 % 26.96/7.07 | % 26.96/7.07 | Equations (214) can reduce 206 to: % 26.96/7.07 | (167) $false % 26.96/7.07 | % 26.96/7.07 |-The branch is then unsatisfiable % 26.96/7.07 |-Branch two: % 26.96/7.07 | (206) ~ (all_122_0_81 = 0) % 26.96/7.07 | (217) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_109_1_79) = 0 & mem(v0, all_76_2_70) = v1) % 27.01/7.07 | % 27.01/7.07 | Instantiating (217) with all_136_0_83, all_136_1_84 yields: % 27.01/7.07 | (218) ~ (all_136_0_83 = 0) & mem(all_136_1_84, all_109_1_79) = 0 & mem(all_136_1_84, all_76_2_70) = all_136_0_83 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (218) yields: % 27.01/7.07 | (219) ~ (all_136_0_83 = 0) % 27.01/7.07 | (220) mem(all_136_1_84, all_109_1_79) = 0 % 27.01/7.07 | (221) mem(all_136_1_84, all_76_2_70) = all_136_0_83 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_59_0_61, all_0_1_1, all_87_1_74 and discharging atoms s(all_0_1_1) = all_59_0_61, mem(all_87_1_74, all_59_0_61) = 0, yields: % 27.01/7.07 | (222) all_87_1_74 = all_0_1_1 % 27.01/7.07 | % 27.01/7.07 | From (222) and (176) follows: % 27.01/7.07 | (223) mem(all_0_1_1, all_61_1_63) = all_87_0_73 % 27.01/7.07 | % 27.01/7.07 +-Applying beta-rule and splitting (200), into two cases. % 27.01/7.07 |-Branch one: % 27.01/7.07 | (224) all_117_0_80 = 0 & mem(all_76_2_70, all_59_0_61) = 0 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (224) yields: % 27.01/7.07 | (225) all_117_0_80 = 0 % 27.01/7.07 | (226) mem(all_76_2_70, all_59_0_61) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_59_0_61, all_0_1_1, all_76_2_70 and discharging atoms s(all_0_1_1) = all_59_0_61, mem(all_76_2_70, all_59_0_61) = 0, yields: % 27.01/7.07 | (227) all_76_2_70 = all_0_1_1 % 27.01/7.07 | % 27.01/7.07 | From (227) and (165) follows: % 27.01/7.07 | (228) mem(all_0_1_1, all_61_1_63) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (76) with all_0_1_1, all_61_1_63, 0, all_87_0_73 and discharging atoms mem(all_0_1_1, all_61_1_63) = all_87_0_73, mem(all_0_1_1, all_61_1_63) = 0, yields: % 27.01/7.07 | (229) all_87_0_73 = 0 % 27.01/7.07 | % 27.01/7.07 | Equations (229) can reduce 175 to: % 27.01/7.07 | (167) $false % 27.01/7.07 | % 27.01/7.07 |-The branch is then unsatisfiable % 27.01/7.07 |-Branch two: % 27.01/7.07 | (231) all_117_0_80 = 0 & mem(all_76_2_70, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (231) yields: % 27.01/7.07 | (225) all_117_0_80 = 0 % 27.01/7.07 | (233) mem(all_76_2_70, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_0_2_2, all_0_3_3, all_76_2_70 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_76_2_70, all_0_2_2) = 0, yields: % 27.01/7.07 | (234) all_76_2_70 = all_0_3_3 % 27.01/7.07 | % 27.01/7.07 | From (234) and (221) follows: % 27.01/7.07 | (235) mem(all_136_1_84, all_0_3_3) = all_136_0_83 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (108) with all_136_0_83, all_0_3_3, all_57_0_60, all_0_5_5, all_136_1_84 and discharging atoms u(all_0_5_5, all_57_0_60) = all_0_3_3, mem(all_136_1_84, all_0_3_3) = all_136_0_83, yields: % 27.01/7.07 | (236) all_136_0_83 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_136_1_84, all_57_0_60) = v1 & mem(all_136_1_84, all_0_5_5) = v0) % 27.01/7.07 | % 27.01/7.07 +-Applying beta-rule and splitting (210), into two cases. % 27.01/7.07 |-Branch one: % 27.01/7.07 | (237) all_129_0_82 = 0 & mem(all_109_1_79, all_59_0_61) = 0 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (237) yields: % 27.01/7.07 | (238) all_129_0_82 = 0 % 27.01/7.07 | (239) mem(all_109_1_79, all_59_0_61) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_59_0_61, all_0_1_1, all_109_1_79 and discharging atoms s(all_0_1_1) = all_59_0_61, mem(all_109_1_79, all_59_0_61) = 0, yields: % 27.01/7.07 | (240) all_109_1_79 = all_0_1_1 % 27.01/7.07 | % 27.01/7.07 | From (240) and (196) follows: % 27.01/7.07 | (228) mem(all_0_1_1, all_61_1_63) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (76) with all_0_1_1, all_61_1_63, 0, all_87_0_73 and discharging atoms mem(all_0_1_1, all_61_1_63) = all_87_0_73, mem(all_0_1_1, all_61_1_63) = 0, yields: % 27.01/7.07 | (229) all_87_0_73 = 0 % 27.01/7.07 | % 27.01/7.07 | Equations (229) can reduce 175 to: % 27.01/7.07 | (167) $false % 27.01/7.07 | % 27.01/7.07 |-The branch is then unsatisfiable % 27.01/7.07 |-Branch two: % 27.01/7.07 | (244) all_129_0_82 = 0 & mem(all_109_1_79, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (244) yields: % 27.01/7.07 | (238) all_129_0_82 = 0 % 27.01/7.07 | (246) mem(all_109_1_79, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 +-Applying beta-rule and splitting (236), into two cases. % 27.01/7.07 |-Branch one: % 27.01/7.07 | (247) all_136_0_83 = 0 % 27.01/7.07 | % 27.01/7.07 | Equations (247) can reduce 219 to: % 27.01/7.07 | (167) $false % 27.01/7.07 | % 27.01/7.07 |-The branch is then unsatisfiable % 27.01/7.07 |-Branch two: % 27.01/7.07 | (219) ~ (all_136_0_83 = 0) % 27.01/7.07 | (250) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_136_1_84, all_57_0_60) = v1 & mem(all_136_1_84, all_0_5_5) = v0) % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_0_2_2, all_0_3_3, all_109_1_79 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_109_1_79, all_0_2_2) = 0, yields: % 27.01/7.07 | (251) all_109_1_79 = all_0_3_3 % 27.01/7.07 | % 27.01/7.07 | From (251) and (220) follows: % 27.01/7.07 | (252) mem(all_136_1_84, all_0_3_3) = 0 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (76) with all_136_1_84, all_0_3_3, 0, all_136_0_83 and discharging atoms mem(all_136_1_84, all_0_3_3) = all_136_0_83, mem(all_136_1_84, all_0_3_3) = 0, yields: % 27.01/7.07 | (247) all_136_0_83 = 0 % 27.01/7.07 | % 27.01/7.07 | Equations (247) can reduce 219 to: % 27.01/7.07 | (167) $false % 27.01/7.07 | % 27.01/7.07 |-The branch is then unsatisfiable % 27.01/7.07 |-Branch two: % 27.01/7.07 | (255) all_99_0_75 = 0 & mem(all_87_1_74, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (255) yields: % 27.01/7.07 | (212) all_99_0_75 = 0 % 27.01/7.07 | (257) mem(all_87_1_74, all_0_2_2) = 0 % 27.01/7.07 | % 27.01/7.07 +-Applying beta-rule and splitting (208), into two cases. % 27.01/7.07 |-Branch one: % 27.01/7.07 | (214) all_122_0_81 = 0 % 27.01/7.07 | % 27.01/7.07 | Equations (214) can reduce 206 to: % 27.01/7.07 | (167) $false % 27.01/7.07 | % 27.01/7.07 |-The branch is then unsatisfiable % 27.01/7.07 |-Branch two: % 27.01/7.07 | (206) ~ (all_122_0_81 = 0) % 27.01/7.07 | (217) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_109_1_79) = 0 & mem(v0, all_76_2_70) = v1) % 27.01/7.07 | % 27.01/7.07 | Instantiating (217) with all_136_0_93, all_136_1_94 yields: % 27.01/7.07 | (262) ~ (all_136_0_93 = 0) & mem(all_136_1_94, all_109_1_79) = 0 & mem(all_136_1_94, all_76_2_70) = all_136_0_93 % 27.01/7.07 | % 27.01/7.07 | Applying alpha-rule on (262) yields: % 27.01/7.07 | (263) ~ (all_136_0_93 = 0) % 27.01/7.07 | (264) mem(all_136_1_94, all_109_1_79) = 0 % 27.01/7.07 | (265) mem(all_136_1_94, all_76_2_70) = all_136_0_93 % 27.01/7.07 | % 27.01/7.07 | Instantiating formula (119) with all_0_2_2, all_0_3_3, all_87_1_74 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_87_1_74, all_0_2_2) = 0, yields: % 27.01/7.07 | (266) all_87_1_74 = all_0_3_3 % 27.01/7.07 | % 27.01/7.07 | From (266) and (176) follows: % 27.01/7.07 | (267) mem(all_0_3_3, all_61_1_63) = all_87_0_73 % 27.01/7.07 | % 27.01/7.07 +-Applying beta-rule and splitting (200), into two cases. % 27.01/7.07 |-Branch one: % 27.01/7.07 | (224) all_117_0_80 = 0 & mem(all_76_2_70, all_59_0_61) = 0 % 27.01/7.08 | % 27.01/7.08 | Applying alpha-rule on (224) yields: % 27.01/7.08 | (225) all_117_0_80 = 0 % 27.01/7.08 | (226) mem(all_76_2_70, all_59_0_61) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (119) with all_59_0_61, all_0_1_1, all_76_2_70 and discharging atoms s(all_0_1_1) = all_59_0_61, mem(all_76_2_70, all_59_0_61) = 0, yields: % 27.01/7.08 | (227) all_76_2_70 = all_0_1_1 % 27.01/7.08 | % 27.01/7.08 | From (227) and (265) follows: % 27.01/7.08 | (272) mem(all_136_1_94, all_0_1_1) = all_136_0_93 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (108) with all_136_0_93, all_0_1_1, all_57_0_60, all_0_4_4, all_136_1_94 and discharging atoms u(all_0_4_4, all_57_0_60) = all_0_1_1, mem(all_136_1_94, all_0_1_1) = all_136_0_93, yields: % 27.01/7.08 | (273) all_136_0_93 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_136_1_94, all_57_0_60) = v1 & mem(all_136_1_94, all_0_4_4) = v0) % 27.01/7.08 | % 27.01/7.08 +-Applying beta-rule and splitting (210), into two cases. % 27.01/7.08 |-Branch one: % 27.01/7.08 | (237) all_129_0_82 = 0 & mem(all_109_1_79, all_59_0_61) = 0 % 27.01/7.08 | % 27.01/7.08 | Applying alpha-rule on (237) yields: % 27.01/7.08 | (238) all_129_0_82 = 0 % 27.01/7.08 | (239) mem(all_109_1_79, all_59_0_61) = 0 % 27.01/7.08 | % 27.01/7.08 +-Applying beta-rule and splitting (273), into two cases. % 27.01/7.08 |-Branch one: % 27.01/7.08 | (277) all_136_0_93 = 0 % 27.01/7.08 | % 27.01/7.08 | Equations (277) can reduce 263 to: % 27.01/7.08 | (167) $false % 27.01/7.08 | % 27.01/7.08 |-The branch is then unsatisfiable % 27.01/7.08 |-Branch two: % 27.01/7.08 | (263) ~ (all_136_0_93 = 0) % 27.01/7.08 | (280) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_136_1_94, all_57_0_60) = v1 & mem(all_136_1_94, all_0_4_4) = v0) % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (119) with all_59_0_61, all_0_1_1, all_109_1_79 and discharging atoms s(all_0_1_1) = all_59_0_61, mem(all_109_1_79, all_59_0_61) = 0, yields: % 27.01/7.08 | (240) all_109_1_79 = all_0_1_1 % 27.01/7.08 | % 27.01/7.08 | From (240) and (264) follows: % 27.01/7.08 | (282) mem(all_136_1_94, all_0_1_1) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (76) with all_136_1_94, all_0_1_1, 0, all_136_0_93 and discharging atoms mem(all_136_1_94, all_0_1_1) = all_136_0_93, mem(all_136_1_94, all_0_1_1) = 0, yields: % 27.01/7.08 | (277) all_136_0_93 = 0 % 27.01/7.08 | % 27.01/7.08 | Equations (277) can reduce 263 to: % 27.01/7.08 | (167) $false % 27.01/7.08 | % 27.01/7.08 |-The branch is then unsatisfiable % 27.01/7.08 |-Branch two: % 27.01/7.08 | (244) all_129_0_82 = 0 & mem(all_109_1_79, all_0_2_2) = 0 % 27.01/7.08 | % 27.01/7.08 | Applying alpha-rule on (244) yields: % 27.01/7.08 | (238) all_129_0_82 = 0 % 27.01/7.08 | (246) mem(all_109_1_79, all_0_2_2) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (119) with all_0_2_2, all_0_3_3, all_109_1_79 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_109_1_79, all_0_2_2) = 0, yields: % 27.01/7.08 | (251) all_109_1_79 = all_0_3_3 % 27.01/7.08 | % 27.01/7.08 | From (251) and (196) follows: % 27.01/7.08 | (289) mem(all_0_3_3, all_61_1_63) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (76) with all_0_3_3, all_61_1_63, 0, all_87_0_73 and discharging atoms mem(all_0_3_3, all_61_1_63) = all_87_0_73, mem(all_0_3_3, all_61_1_63) = 0, yields: % 27.01/7.08 | (229) all_87_0_73 = 0 % 27.01/7.08 | % 27.01/7.08 | Equations (229) can reduce 175 to: % 27.01/7.08 | (167) $false % 27.01/7.08 | % 27.01/7.08 |-The branch is then unsatisfiable % 27.01/7.08 |-Branch two: % 27.01/7.08 | (231) all_117_0_80 = 0 & mem(all_76_2_70, all_0_2_2) = 0 % 27.01/7.08 | % 27.01/7.08 | Applying alpha-rule on (231) yields: % 27.01/7.08 | (225) all_117_0_80 = 0 % 27.01/7.08 | (233) mem(all_76_2_70, all_0_2_2) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (119) with all_0_2_2, all_0_3_3, all_76_2_70 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_76_2_70, all_0_2_2) = 0, yields: % 27.01/7.08 | (234) all_76_2_70 = all_0_3_3 % 27.01/7.08 | % 27.01/7.08 | From (234) and (165) follows: % 27.01/7.08 | (289) mem(all_0_3_3, all_61_1_63) = 0 % 27.01/7.08 | % 27.01/7.08 | Instantiating formula (76) with all_0_3_3, all_61_1_63, 0, all_87_0_73 and discharging atoms mem(all_0_3_3, all_61_1_63) = all_87_0_73, mem(all_0_3_3, all_61_1_63) = 0, yields: % 27.01/7.08 | (229) all_87_0_73 = 0 % 27.01/7.08 | % 27.01/7.08 | Equations (229) can reduce 175 to: % 27.01/7.08 | (167) $false % 27.01/7.08 | % 27.01/7.08 |-The branch is then unsatisfiable % 27.01/7.08 % SZS output end Proof for theBenchmark % 27.01/7.08 % 27.01/7.08 6505ms %------------------------------------------------------------------------------