%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV552+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n032.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 22.44s 6.52s % Output : Proof 24.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SEV552+1 : TPTP v9.1.0. Released v9.1.0. % 0.00/0.11 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.30 % Computer : n032.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Mon Mar 31 11:54:46 EDT 2025 % 0.11/0.30 % CPUTime : % 0.15/0.50 ____ _ % 0.15/0.50 ___ / __ \_____(_)___ ________ __________ % 0.15/0.50 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.15/0.50 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.15/0.50 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.15/0.50 % 0.15/0.50 A Theorem Prover for First-Order Logic % 0.15/0.50 (ePrincess v.1.0) % 0.15/0.50 % 0.15/0.50 (c) Philipp Rümmer, 2009-2015 % 0.15/0.50 (c) Peter Backeman, 2014-2015 % 0.15/0.50 (contributions by Angelo Brillout, Peter Baumgartner) % 0.15/0.50 Free software under GNU Lesser General Public License (LGPL). % 0.15/0.50 Bug reports to peter@backeman.se % 0.15/0.50 % 0.15/0.50 For more information, visit http://user.uu.se/~petba168/breu/ % 0.15/0.50 % 0.15/0.50 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.15/0.55 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.27/0.84 Prover 0: Preprocessing ... % 2.03/1.10 Prover 0: Warning: ignoring some quantifiers % 2.03/1.13 Prover 0: Constructing countermodel ... % 19.33/5.84 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 19.65/5.90 Prover 1: Preprocessing ... % 20.11/6.06 Prover 1: Constructing countermodel ... % 21.06/6.24 Prover 1: gave up % 21.06/6.24 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 21.06/6.26 Prover 2: Preprocessing ... % 21.50/6.38 Prover 2: Warning: ignoring some quantifiers % 21.50/6.39 Prover 2: Constructing countermodel ... % 22.44/6.52 Prover 2: proved (285ms) % 22.44/6.52 Prover 0: stopped % 22.44/6.52 % 22.44/6.52 No countermodel exists, formula is valid % 22.44/6.52 % SZS status Theorem for theBenchmark % 22.44/6.53 % 22.44/6.53 Generating proof ... Warning: ignoring some quantifiers % 23.77/6.86 found it (size 118) % 23.77/6.86 % 23.77/6.86 % SZS output start Proof for theBenchmark % 23.77/6.86 Assumed formulas after preprocessing and simplification: % 23.77/6.86 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (atleast3p(v7) = 0 & n(v0) = v1 & n(e) = v0 & a(v5, v1) = v6 & a(v3, v6) = v7 & s(v4) = v5 & s(v2) = v3 & s(v1) = v2 & s(v0) = v4 & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (m(v9, v10) = v11) | ~ (mem(v8, v11) = v12) | ? [v13] : ((v13 = 0 & mem(v8, v10) = 0) | ( ~ (v13 = 0) & mem(v8, v9) = v13))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (u(v9, v10) = v11) | ~ (mem(v8, v11) = v12) | ? [v13] : ? [v14] : ( ~ (v14 = 0) & ~ (v13 = 0) & mem(v8, v10) = v14 & mem(v8, v9) = v13)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast16p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast15p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast15p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast14p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast14p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast13p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast13p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast12p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast12p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast11p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast11p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast10p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast10p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast9p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast9p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast8p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast8p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast7p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast7p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast6p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast6p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast5p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast5p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast4p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast4p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast3p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | v9 = 0 | ~ (atleast3p(v8) = v9) | ~ (subq(v8, v10) = v11) | ? [v12] : (( ~ (v12 = 0) & atleast2p(v10) = v12) | ( ~ (v12 = 0) & subq(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (p(v9) = v10) | ~ (mem(v8, v10) = v11) | ? [v12] : ( ~ (v12 = 0) & subq(v8, v9) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (subq(v8, v9) = 0) | ~ (mem(v10, v9) = v11) | ? [v12] : ( ~ (v12 = 0) & mem(v10, v8) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (a(v11, v10) = v9) | ~ (a(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (m(v11, v10) = v9) | ~ (m(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (u(v11, v10) = v9) | ~ (u(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (disj(v11, v10) = v9) | ~ (disj(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (subq(v11, v10) = v9) | ~ (subq(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (mem(v11, v10) = v9) | ~ (mem(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = 0 | ~ (atleast2p(v8) = v9) | ~ (p(v10) = v11) | ? [v12] : ((v12 = 0 & subq(v8, v11) = 0) | ( ~ (v12 = 0) & mem(v10, v8) = v12))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (m(v9, v10) = v11) | ~ (mem(v8, v11) = 0) | ? [v12] : ( ~ (v12 = 0) & mem(v8, v10) = v12 & mem(v8, v9) = 0)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (u(v9, v10) = v11) | ~ (mem(v8, v11) = 0) | ? [v12] : ((v12 = 0 & mem(v8, v10) = 0) | (v12 = 0 & mem(v8, v9) = 0))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (u(v8, v10) = v11) | ~ (s(v9) = v10) | a(v8, v9) = v11) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (s(v8) = v9) | ~ (mem(v8, v9) = v10)) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (disj(v8, v9) = v10) | ? [v11] : (mem(v11, v9) = 0 & mem(v11, v8) = 0)) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (subq(v8, v9) = v10) | ? [v11] : ? [v12] : ( ~ (v12 = 0) & p(v9) = v11 & mem(v8, v11) = v12)) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (subq(v8, v9) = v10) | ? [v11] : ? [v12] : ( ~ (v12 = 0) & mem(v11, v9) = v12 & mem(v11, v8) = 0)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast16p(v10) = v9) | ~ (atleast16p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast15p(v10) = v9) | ~ (atleast15p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast14p(v10) = v9) | ~ (atleast14p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast13p(v10) = v9) | ~ (atleast13p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast12p(v10) = v9) | ~ (atleast12p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast11p(v10) = v9) | ~ (atleast11p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast10p(v10) = v9) | ~ (atleast10p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast9p(v10) = v9) | ~ (atleast9p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast8p(v10) = v9) | ~ (atleast8p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast7p(v10) = v9) | ~ (atleast7p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast6p(v10) = v9) | ~ (atleast6p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast5p(v10) = v9) | ~ (atleast5p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast4p(v10) = v9) | ~ (atleast4p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast3p(v10) = v9) | ~ (atleast3p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (atleast2p(v10) = v9) | ~ (atleast2p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (p(v10) = v9) | ~ (p(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (n(v10) = v9) | ~ (n(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (s(v10) = v9) | ~ (s(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (s(v9) = v10) | ~ (mem(v8, v10) = 0)) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast16p(v8) = v9) | ~ (atleast15p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast16p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast15p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast15p(v8) = v9) | ~ (atleast14p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast15p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast14p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast14p(v8) = v9) | ~ (atleast13p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast14p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast13p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast13p(v8) = v9) | ~ (atleast12p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast13p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast12p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast12p(v8) = v9) | ~ (atleast11p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast12p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast11p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast11p(v8) = v9) | ~ (atleast10p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast11p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast10p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast10p(v8) = v9) | ~ (atleast9p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast10p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast9p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast9p(v8) = v9) | ~ (atleast8p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast9p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast8p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast8p(v8) = v9) | ~ (atleast7p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast8p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast7p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast7p(v8) = v9) | ~ (atleast6p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast7p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast6p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast6p(v8) = v9) | ~ (atleast5p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast6p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast5p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast5p(v8) = v9) | ~ (atleast4p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast5p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast4p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast4p(v8) = v9) | ~ (atleast3p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast4p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast3p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast3p(v8) = v9) | ~ (atleast2p(v10) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & subq(v10, v8) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast3p(v8) = v9) | ~ (subq(v10, v8) = 0) | ? [v11] : ((v11 = 0 & subq(v8, v10) = 0) | ( ~ (v11 = 0) & atleast2p(v10) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (atleast2p(v8) = v9) | ~ (mem(v10, v8) = 0) | ? [v11] : (p(v10) = v11 & subq(v8, v11) = 0)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (p(v9) = v10) | ~ (mem(v8, v10) = 0) | subq(v8, v9) = 0) & ! [v8] : ! [v9] : ! [v10] : ( ~ (a(v8, v9) = v10) | ? [v11] : (u(v8, v11) = v10 & s(v9) = v11)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (disj(v8, v9) = 0) | ~ (mem(v10, v9) = 0) | ? [v11] : ( ~ (v11 = 0) & mem(v10, v8) = v11)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (disj(v8, v9) = 0) | ~ (mem(v10, v8) = 0) | ? [v11] : ( ~ (v11 = 0) & mem(v10, v9) = v11)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (subq(v8, v9) = 0) | ~ (mem(v10, v8) = 0) | mem(v10, v9) = 0) & ! [v8] : ! [v9] : (v9 = v8 | ~ (subq(v9, v8) = 0) | ? [v10] : ( ~ (v10 = 0) & subq(v8, v9) = v10)) & ! [v8] : ! [v9] : (v9 = v8 | ~ (subq(v8, v9) = 0) | ? [v10] : ( ~ (v10 = 0) & subq(v9, v8) = v10)) & ! [v8] : ! [v9] : ( ~ (n(v8) = v9) | a(v8, v8) = v9) & ! [v8] : ! [v9] : ( ~ (a(v8, v8) = v9) | n(v8) = v9) & ! [v8] : ! [v9] : ( ~ (subq(v8, v9) = 0) | ? [v10] : (p(v9) = v10 & mem(v8, v10) = 0)) & ! [v8] : ( ~ (atleast16p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast15p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast15p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast14p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast14p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast13p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast13p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast12p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast12p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast11p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast11p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast10p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast10p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast9p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast9p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast8p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast8p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast7p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast7p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast6p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast6p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast5p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast5p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast4p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast4p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast3p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast3p(v8) = 0) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & atleast2p(v9) = 0 & subq(v9, v8) = 0 & subq(v8, v9) = v10)) & ! [v8] : ( ~ (atleast2p(v8) = 0) | ? [v9] : ? [v10] : ? [v11] : ( ~ (v11 = 0) & p(v9) = v10 & subq(v8, v10) = v11 & mem(v9, v8) = 0)) & ! [v8] : ~ (mem(v8, e) = 0) & ? [v8] : ? [v9] : ? [v10] : a(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : m(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : u(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : disj(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : subq(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : mem(v9, v8) = v10 & ? [v8] : ? [v9] : atleast16p(v8) = v9 & ? [v8] : ? [v9] : atleast15p(v8) = v9 & ? [v8] : ? [v9] : atleast14p(v8) = v9 & ? [v8] : ? [v9] : atleast13p(v8) = v9 & ? [v8] : ? [v9] : atleast12p(v8) = v9 & ? [v8] : ? [v9] : atleast11p(v8) = v9 & ? [v8] : ? [v9] : atleast10p(v8) = v9 & ? [v8] : ? [v9] : atleast9p(v8) = v9 & ? [v8] : ? [v9] : atleast8p(v8) = v9 & ? [v8] : ? [v9] : atleast7p(v8) = v9 & ? [v8] : ? [v9] : atleast6p(v8) = v9 & ? [v8] : ? [v9] : atleast5p(v8) = v9 & ? [v8] : ? [v9] : atleast4p(v8) = v9 & ? [v8] : ? [v9] : atleast3p(v8) = v9 & ? [v8] : ? [v9] : atleast2p(v8) = v9 & ? [v8] : ? [v9] : p(v8) = v9 & ? [v8] : ? [v9] : n(v8) = v9 & ? [v8] : ? [v9] : s(v8) = v9) % 24.15/6.92 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7 yields: % 24.15/6.92 | (1) atleast3p(all_0_0_0) = 0 & n(all_0_7_7) = all_0_6_6 & n(e) = all_0_7_7 & a(all_0_2_2, all_0_6_6) = all_0_1_1 & a(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_5_5 & s(all_0_7_7) = 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 % 24.15/6.95 | % 24.15/6.95 | Applying alpha-rule on (1) yields: % 24.15/6.95 | (2) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.95 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 24.15/6.95 | (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))) % 24.15/6.95 | (5) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.95 | (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))) % 24.15/6.95 | (7) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 24.15/6.95 | (8) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 24.15/6.95 | (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))) % 24.15/6.95 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 24.15/6.95 | (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))) % 24.15/6.95 | (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))) % 24.15/6.95 | (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))) % 24.15/6.95 | (14) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 24.15/6.95 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 24.15/6.95 | (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))) % 24.15/6.96 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 24.15/6.96 | (18) s(all_0_3_3) = all_0_2_2 % 24.15/6.96 | (19) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.96 | (20) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 24.15/6.96 | (21) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 24.15/6.96 | (22) ! [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))) % 24.15/6.96 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 24.15/6.96 | (24) ! [v0] : ~ (mem(v0, e) = 0) % 24.15/6.96 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.96 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 24.15/6.96 | (27) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 24.15/6.96 | (28) ! [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))) % 24.15/6.96 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 24.15/6.96 | (30) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 24.15/6.96 | (31) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.96 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 24.15/6.96 | (33) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 24.15/6.96 | (34) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 24.15/6.96 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 24.15/6.96 | (36) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.96 | (37) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.96 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 24.15/6.96 | (39) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 24.15/6.96 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 24.15/6.96 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 24.15/6.96 | (42) ! [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))) % 24.15/6.96 | (43) ? [v0] : ? [v1] : s(v0) = v1 % 24.15/6.96 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 24.15/6.96 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 24.15/6.96 | (46) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 24.15/6.96 | (47) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 24.15/6.96 | (48) ! [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))) % 24.15/6.96 | (49) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 24.15/6.96 | (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))) % 24.15/6.96 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.96 | (52) s(all_0_6_6) = all_0_5_5 % 24.15/6.96 | (53) ! [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))) % 24.15/6.96 | (54) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.97 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.97 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 24.15/6.97 | (57) ! [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))) % 24.15/6.97 | (58) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 24.15/6.97 | (59) ! [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))) % 24.15/6.97 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 24.15/6.97 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 24.15/6.97 | (62) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 24.15/6.97 | (63) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 24.15/6.97 | (64) ! [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))) % 24.15/6.97 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 24.15/6.97 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 24.15/6.97 | (67) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 24.15/6.97 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.97 | (69) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 24.15/6.97 | (70) n(e) = all_0_7_7 % 24.15/6.97 | (71) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 24.15/6.97 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.97 | (73) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 24.15/6.97 | (74) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.97 | (75) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 24.15/6.97 | (76) s(all_0_7_7) = all_0_3_3 % 24.15/6.97 | (77) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 24.15/6.97 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 24.15/6.97 | (79) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 24.15/6.97 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 24.15/6.97 | (81) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.97 | (82) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.97 | (83) atleast3p(all_0_0_0) = 0 % 24.15/6.97 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 24.15/6.97 | (85) ? [v0] : ? [v1] : n(v0) = v1 % 24.15/6.97 | (86) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 24.15/6.97 | (87) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.97 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 24.15/6.97 | (89) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 24.15/6.97 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 24.15/6.98 | (91) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.98 | (92) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 24.15/6.98 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 24.15/6.98 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 24.15/6.98 | (95) ! [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))) % 24.15/6.98 | (96) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 24.15/6.98 | (97) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 24.15/6.98 | (98) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 24.15/6.98 | (99) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 24.15/6.98 | (100) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 24.15/6.98 | (101) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 24.15/6.98 | (102) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 24.15/6.98 | (103) a(all_0_2_2, all_0_6_6) = all_0_1_1 % 24.15/6.98 | (104) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.98 | (105) ? [v0] : ? [v1] : p(v0) = v1 % 24.15/6.98 | (106) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.98 | (107) ! [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))) % 24.15/6.98 | (108) s(all_0_5_5) = all_0_4_4 % 24.15/6.98 | (109) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.98 | (110) ! [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)) % 24.15/6.98 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 24.15/6.98 | (112) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 24.15/6.98 | (113) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 24.15/6.98 | (114) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.98 | (115) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.98 | (116) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 24.15/6.98 | (117) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 24.15/6.98 | (118) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 24.15/6.98 | (119) n(all_0_7_7) = all_0_6_6 % 24.15/6.98 | (120) a(all_0_4_4, all_0_1_1) = all_0_0_0 % 24.15/6.98 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 24.15/6.98 | (122) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 24.15/6.98 | (123) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 24.15/6.98 | (124) ! [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))) % 24.15/6.98 | (125) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.98 | (126) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 24.15/6.98 | (127) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 24.15/6.98 | (128) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 24.15/6.98 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 24.15/6.98 | (130) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 24.15/6.98 | (131) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 24.15/6.98 | (132) ! [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))) % 24.15/6.98 | (133) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 24.15/6.98 | (134) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 24.15/6.98 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.15/6.98 | (136) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 24.15/6.98 | (137) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 24.15/6.98 | (138) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.98 | (139) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.15/6.98 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 24.15/6.98 | % 24.15/6.98 | Instantiating formula (104) with all_0_0_0 and discharging atoms atleast3p(all_0_0_0) = 0, yields: % 24.15/6.98 | (141) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast2p(v0) = 0 & subq(v0, all_0_0_0) = 0 & subq(all_0_0_0, v0) = v1) % 24.15/6.98 | % 24.15/6.99 | Instantiating formula (15) with all_0_1_1, all_0_6_6, all_0_2_2 and discharging atoms a(all_0_2_2, all_0_6_6) = all_0_1_1, yields: % 24.15/6.99 | (142) ? [v0] : (u(all_0_2_2, v0) = all_0_1_1 & s(all_0_6_6) = v0) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (15) with all_0_0_0, all_0_1_1, all_0_4_4 and discharging atoms a(all_0_4_4, all_0_1_1) = all_0_0_0, yields: % 24.15/6.99 | (143) ? [v0] : (u(all_0_4_4, v0) = all_0_0_0 & s(all_0_1_1) = v0) % 24.15/6.99 | % 24.15/6.99 | Instantiating (143) with all_57_0_62 yields: % 24.15/6.99 | (144) u(all_0_4_4, all_57_0_62) = all_0_0_0 & s(all_0_1_1) = all_57_0_62 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (144) yields: % 24.15/6.99 | (145) u(all_0_4_4, all_57_0_62) = all_0_0_0 % 24.15/6.99 | (146) s(all_0_1_1) = all_57_0_62 % 24.15/6.99 | % 24.15/6.99 | Instantiating (142) with all_59_0_63 yields: % 24.15/6.99 | (147) u(all_0_2_2, all_59_0_63) = all_0_1_1 & s(all_0_6_6) = all_59_0_63 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (147) yields: % 24.15/6.99 | (148) u(all_0_2_2, all_59_0_63) = all_0_1_1 % 24.15/6.99 | (149) s(all_0_6_6) = all_59_0_63 % 24.15/6.99 | % 24.15/6.99 | Instantiating (141) with all_61_0_64, all_61_1_65 yields: % 24.15/6.99 | (150) ~ (all_61_0_64 = 0) & atleast2p(all_61_1_65) = 0 & subq(all_61_1_65, all_0_0_0) = 0 & subq(all_0_0_0, all_61_1_65) = all_61_0_64 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (150) yields: % 24.15/6.99 | (151) ~ (all_61_0_64 = 0) % 24.15/6.99 | (152) atleast2p(all_61_1_65) = 0 % 24.15/6.99 | (153) subq(all_61_1_65, all_0_0_0) = 0 % 24.15/6.99 | (154) subq(all_0_0_0, all_61_1_65) = all_61_0_64 % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (3) with all_0_6_6, all_59_0_63, all_0_5_5 and discharging atoms s(all_0_6_6) = all_59_0_63, s(all_0_6_6) = all_0_5_5, yields: % 24.15/6.99 | (155) all_59_0_63 = all_0_5_5 % 24.15/6.99 | % 24.15/6.99 | From (155) and (148) follows: % 24.15/6.99 | (156) u(all_0_2_2, all_0_5_5) = all_0_1_1 % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (96) with all_61_1_65 and discharging atoms atleast2p(all_61_1_65) = 0, yields: % 24.15/6.99 | (157) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & p(v0) = v1 & subq(all_61_1_65, v1) = v2 & mem(v0, all_61_1_65) = 0) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (73) with all_61_0_64, all_61_1_65, all_0_0_0 and discharging atoms subq(all_0_0_0, all_61_1_65) = all_61_0_64, yields: % 24.15/6.99 | (158) all_61_0_64 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_61_1_65) = v0 & mem(all_0_0_0, v0) = v1) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (7) with all_61_0_64, all_61_1_65, all_0_0_0 and discharging atoms subq(all_0_0_0, all_61_1_65) = all_61_0_64, yields: % 24.15/6.99 | (159) all_61_0_64 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_61_1_65) = v1 & mem(v0, all_0_0_0) = 0) % 24.15/6.99 | % 24.15/6.99 | Instantiating (157) with all_78_0_69, all_78_1_70, all_78_2_71 yields: % 24.15/6.99 | (160) ~ (all_78_0_69 = 0) & p(all_78_2_71) = all_78_1_70 & subq(all_61_1_65, all_78_1_70) = all_78_0_69 & mem(all_78_2_71, all_61_1_65) = 0 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (160) yields: % 24.15/6.99 | (161) ~ (all_78_0_69 = 0) % 24.15/6.99 | (162) p(all_78_2_71) = all_78_1_70 % 24.15/6.99 | (163) subq(all_61_1_65, all_78_1_70) = all_78_0_69 % 24.15/6.99 | (164) mem(all_78_2_71, all_61_1_65) = 0 % 24.15/6.99 | % 24.15/6.99 +-Applying beta-rule and splitting (158), into two cases. % 24.15/6.99 |-Branch one: % 24.15/6.99 | (165) all_61_0_64 = 0 % 24.15/6.99 | % 24.15/6.99 | Equations (165) can reduce 151 to: % 24.15/6.99 | (166) $false % 24.15/6.99 | % 24.15/6.99 |-The branch is then unsatisfiable % 24.15/6.99 |-Branch two: % 24.15/6.99 | (151) ~ (all_61_0_64 = 0) % 24.15/6.99 | (168) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_61_1_65) = v0 & mem(all_0_0_0, v0) = v1) % 24.15/6.99 | % 24.15/6.99 +-Applying beta-rule and splitting (159), into two cases. % 24.15/6.99 |-Branch one: % 24.15/6.99 | (165) all_61_0_64 = 0 % 24.15/6.99 | % 24.15/6.99 | Equations (165) can reduce 151 to: % 24.15/6.99 | (166) $false % 24.15/6.99 | % 24.15/6.99 |-The branch is then unsatisfiable % 24.15/6.99 |-Branch two: % 24.15/6.99 | (151) ~ (all_61_0_64 = 0) % 24.15/6.99 | (172) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_61_1_65) = v1 & mem(v0, all_0_0_0) = 0) % 24.15/6.99 | % 24.15/6.99 | Instantiating (172) with all_89_0_74, all_89_1_75 yields: % 24.15/6.99 | (173) ~ (all_89_0_74 = 0) & mem(all_89_1_75, all_61_1_65) = all_89_0_74 & mem(all_89_1_75, all_0_0_0) = 0 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (173) yields: % 24.15/6.99 | (174) ~ (all_89_0_74 = 0) % 24.15/6.99 | (175) mem(all_89_1_75, all_61_1_65) = all_89_0_74 % 24.15/6.99 | (176) mem(all_89_1_75, all_0_0_0) = 0 % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (73) with all_78_0_69, all_78_1_70, all_61_1_65 and discharging atoms subq(all_61_1_65, all_78_1_70) = all_78_0_69, yields: % 24.15/6.99 | (177) all_78_0_69 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_78_1_70) = v0 & mem(all_61_1_65, v0) = v1) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (7) with all_78_0_69, all_78_1_70, all_61_1_65 and discharging atoms subq(all_61_1_65, all_78_1_70) = all_78_0_69, yields: % 24.15/6.99 | (178) all_78_0_69 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_78_1_70) = v1 & mem(v0, all_61_1_65) = 0) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (42) with all_0_0_0, all_57_0_62, all_0_4_4, all_89_1_75 and discharging atoms u(all_0_4_4, all_57_0_62) = all_0_0_0, mem(all_89_1_75, all_0_0_0) = 0, yields: % 24.15/6.99 | (179) ? [v0] : ((v0 = 0 & mem(all_89_1_75, all_57_0_62) = 0) | (v0 = 0 & mem(all_89_1_75, all_0_4_4) = 0)) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (17) with all_78_2_71, all_0_0_0, all_61_1_65 and discharging atoms subq(all_61_1_65, all_0_0_0) = 0, mem(all_78_2_71, all_61_1_65) = 0, yields: % 24.15/6.99 | (180) mem(all_78_2_71, all_0_0_0) = 0 % 24.15/6.99 | % 24.15/6.99 | Instantiating (179) with all_101_0_76 yields: % 24.15/6.99 | (181) (all_101_0_76 = 0 & mem(all_89_1_75, all_57_0_62) = 0) | (all_101_0_76 = 0 & mem(all_89_1_75, all_0_4_4) = 0) % 24.15/6.99 | % 24.15/6.99 +-Applying beta-rule and splitting (177), into two cases. % 24.15/6.99 |-Branch one: % 24.15/6.99 | (182) all_78_0_69 = 0 % 24.15/6.99 | % 24.15/6.99 | Equations (182) can reduce 161 to: % 24.15/6.99 | (166) $false % 24.15/6.99 | % 24.15/6.99 |-The branch is then unsatisfiable % 24.15/6.99 |-Branch two: % 24.15/6.99 | (161) ~ (all_78_0_69 = 0) % 24.15/6.99 | (185) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_78_1_70) = v0 & mem(all_61_1_65, v0) = v1) % 24.15/6.99 | % 24.15/6.99 +-Applying beta-rule and splitting (178), into two cases. % 24.15/6.99 |-Branch one: % 24.15/6.99 | (182) all_78_0_69 = 0 % 24.15/6.99 | % 24.15/6.99 | Equations (182) can reduce 161 to: % 24.15/6.99 | (166) $false % 24.15/6.99 | % 24.15/6.99 |-The branch is then unsatisfiable % 24.15/6.99 |-Branch two: % 24.15/6.99 | (161) ~ (all_78_0_69 = 0) % 24.15/6.99 | (189) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_78_1_70) = v1 & mem(v0, all_61_1_65) = 0) % 24.15/6.99 | % 24.15/6.99 | Instantiating (189) with all_111_0_79, all_111_1_80 yields: % 24.15/6.99 | (190) ~ (all_111_0_79 = 0) & mem(all_111_1_80, all_78_1_70) = all_111_0_79 & mem(all_111_1_80, all_61_1_65) = 0 % 24.15/6.99 | % 24.15/6.99 | Applying alpha-rule on (190) yields: % 24.15/6.99 | (191) ~ (all_111_0_79 = 0) % 24.15/6.99 | (192) mem(all_111_1_80, all_78_1_70) = all_111_0_79 % 24.15/6.99 | (193) mem(all_111_1_80, all_61_1_65) = 0 % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (32) with all_111_0_79, all_78_1_70, all_78_2_71, all_111_1_80 and discharging atoms p(all_78_2_71) = all_78_1_70, mem(all_111_1_80, all_78_1_70) = all_111_0_79, yields: % 24.15/6.99 | (194) all_111_0_79 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_111_1_80, all_78_2_71) = v0) % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (17) with all_111_1_80, all_0_0_0, all_61_1_65 and discharging atoms subq(all_61_1_65, all_0_0_0) = 0, mem(all_111_1_80, all_61_1_65) = 0, yields: % 24.15/6.99 | (195) mem(all_111_1_80, all_0_0_0) = 0 % 24.15/6.99 | % 24.15/6.99 | Instantiating formula (42) with all_0_0_0, all_57_0_62, all_0_4_4, all_78_2_71 and discharging atoms u(all_0_4_4, all_57_0_62) = all_0_0_0, mem(all_78_2_71, all_0_0_0) = 0, yields: % 24.15/7.00 | (196) ? [v0] : ((v0 = 0 & mem(all_78_2_71, all_57_0_62) = 0) | (v0 = 0 & mem(all_78_2_71, all_0_4_4) = 0)) % 24.15/7.00 | % 24.15/7.00 | Instantiating (196) with all_119_0_81 yields: % 24.15/7.00 | (197) (all_119_0_81 = 0 & mem(all_78_2_71, all_57_0_62) = 0) | (all_119_0_81 = 0 & mem(all_78_2_71, all_0_4_4) = 0) % 24.15/7.00 | % 24.15/7.00 +-Applying beta-rule and splitting (194), into two cases. % 24.15/7.00 |-Branch one: % 24.15/7.00 | (198) all_111_0_79 = 0 % 24.15/7.00 | % 24.15/7.00 | Equations (198) can reduce 191 to: % 24.15/7.00 | (166) $false % 24.15/7.00 | % 24.15/7.00 |-The branch is then unsatisfiable % 24.15/7.00 |-Branch two: % 24.15/7.00 | (191) ~ (all_111_0_79 = 0) % 24.15/7.00 | (201) ? [v0] : ( ~ (v0 = 0) & subq(all_111_1_80, all_78_2_71) = v0) % 24.15/7.00 | % 24.15/7.00 | Instantiating (201) with all_124_0_82 yields: % 24.15/7.00 | (202) ~ (all_124_0_82 = 0) & subq(all_111_1_80, all_78_2_71) = all_124_0_82 % 24.15/7.00 | % 24.15/7.00 | Applying alpha-rule on (202) yields: % 24.15/7.00 | (203) ~ (all_124_0_82 = 0) % 24.15/7.00 | (204) subq(all_111_1_80, all_78_2_71) = all_124_0_82 % 24.15/7.00 | % 24.15/7.00 | Instantiating formula (7) with all_124_0_82, all_78_2_71, all_111_1_80 and discharging atoms subq(all_111_1_80, all_78_2_71) = all_124_0_82, yields: % 24.15/7.00 | (205) all_124_0_82 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_111_1_80) = 0 & mem(v0, all_78_2_71) = v1) % 24.15/7.00 | % 24.15/7.00 | Instantiating formula (42) with all_0_0_0, all_57_0_62, all_0_4_4, all_111_1_80 and discharging atoms u(all_0_4_4, all_57_0_62) = all_0_0_0, mem(all_111_1_80, all_0_0_0) = 0, yields: % 24.15/7.00 | (206) ? [v0] : ((v0 = 0 & mem(all_111_1_80, all_57_0_62) = 0) | (v0 = 0 & mem(all_111_1_80, all_0_4_4) = 0)) % 24.15/7.00 | % 24.15/7.00 | Instantiating (206) with all_131_0_83 yields: % 24.15/7.00 | (207) (all_131_0_83 = 0 & mem(all_111_1_80, all_57_0_62) = 0) | (all_131_0_83 = 0 & mem(all_111_1_80, all_0_4_4) = 0) % 24.15/7.00 | % 24.15/7.00 +-Applying beta-rule and splitting (181), into two cases. % 24.15/7.00 |-Branch one: % 24.15/7.00 | (208) all_101_0_76 = 0 & mem(all_89_1_75, all_57_0_62) = 0 % 24.15/7.00 | % 24.15/7.00 | Applying alpha-rule on (208) yields: % 24.15/7.00 | (209) all_101_0_76 = 0 % 24.15/7.00 | (210) mem(all_89_1_75, all_57_0_62) = 0 % 24.15/7.00 | % 24.15/7.00 +-Applying beta-rule and splitting (205), into two cases. % 24.15/7.00 |-Branch one: % 24.15/7.00 | (211) all_124_0_82 = 0 % 24.15/7.00 | % 24.15/7.00 | Equations (211) can reduce 203 to: % 24.15/7.00 | (166) $false % 24.15/7.00 | % 24.15/7.00 |-The branch is then unsatisfiable % 24.15/7.00 |-Branch two: % 24.15/7.00 | (203) ~ (all_124_0_82 = 0) % 24.15/7.00 | (214) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_111_1_80) = 0 & mem(v0, all_78_2_71) = v1) % 24.15/7.00 | % 24.15/7.00 | Instantiating (214) with all_138_0_84, all_138_1_85 yields: % 24.15/7.00 | (215) ~ (all_138_0_84 = 0) & mem(all_138_1_85, all_111_1_80) = 0 & mem(all_138_1_85, all_78_2_71) = all_138_0_84 % 24.15/7.00 | % 24.15/7.00 | Applying alpha-rule on (215) yields: % 24.15/7.00 | (216) ~ (all_138_0_84 = 0) % 24.15/7.00 | (217) mem(all_138_1_85, all_111_1_80) = 0 % 24.15/7.00 | (218) mem(all_138_1_85, all_78_2_71) = all_138_0_84 % 24.15/7.00 | % 24.15/7.00 | Instantiating formula (121) with all_57_0_62, all_0_1_1, all_89_1_75 and discharging atoms s(all_0_1_1) = all_57_0_62, mem(all_89_1_75, all_57_0_62) = 0, yields: % 24.15/7.00 | (219) all_89_1_75 = all_0_1_1 % 24.15/7.00 | % 24.15/7.00 | From (219) and (175) follows: % 24.15/7.00 | (220) mem(all_0_1_1, all_61_1_65) = all_89_0_74 % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (197), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (221) all_119_0_81 = 0 & mem(all_78_2_71, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (221) yields: % 24.70/7.00 | (222) all_119_0_81 = 0 % 24.70/7.00 | (223) mem(all_78_2_71, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_57_0_62, all_0_1_1, all_78_2_71 and discharging atoms s(all_0_1_1) = all_57_0_62, mem(all_78_2_71, all_57_0_62) = 0, yields: % 24.70/7.00 | (224) all_78_2_71 = all_0_1_1 % 24.70/7.00 | % 24.70/7.00 | From (224) and (164) follows: % 24.70/7.00 | (225) mem(all_0_1_1, all_61_1_65) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (78) with all_0_1_1, all_61_1_65, 0, all_89_0_74 and discharging atoms mem(all_0_1_1, all_61_1_65) = all_89_0_74, mem(all_0_1_1, all_61_1_65) = 0, yields: % 24.70/7.00 | (226) all_89_0_74 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (226) can reduce 174 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (228) all_119_0_81 = 0 & mem(all_78_2_71, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (228) yields: % 24.70/7.00 | (222) all_119_0_81 = 0 % 24.70/7.00 | (230) mem(all_78_2_71, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_0_4_4, all_0_5_5, all_78_2_71 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_78_2_71, all_0_4_4) = 0, yields: % 24.70/7.00 | (231) all_78_2_71 = all_0_5_5 % 24.70/7.00 | % 24.70/7.00 | From (231) and (218) follows: % 24.70/7.00 | (232) mem(all_138_1_85, all_0_5_5) = all_138_0_84 % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (207), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (233) all_131_0_83 = 0 & mem(all_111_1_80, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (233) yields: % 24.70/7.00 | (234) all_131_0_83 = 0 % 24.70/7.00 | (235) mem(all_111_1_80, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_57_0_62, all_0_1_1, all_111_1_80 and discharging atoms s(all_0_1_1) = all_57_0_62, mem(all_111_1_80, all_57_0_62) = 0, yields: % 24.70/7.00 | (236) all_111_1_80 = all_0_1_1 % 24.70/7.00 | % 24.70/7.00 | From (236) and (193) follows: % 24.70/7.00 | (225) mem(all_0_1_1, all_61_1_65) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (78) with all_0_1_1, all_61_1_65, 0, all_89_0_74 and discharging atoms mem(all_0_1_1, all_61_1_65) = all_89_0_74, mem(all_0_1_1, all_61_1_65) = 0, yields: % 24.70/7.00 | (226) all_89_0_74 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (226) can reduce 174 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (240) all_131_0_83 = 0 & mem(all_111_1_80, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (240) yields: % 24.70/7.00 | (234) all_131_0_83 = 0 % 24.70/7.00 | (242) mem(all_111_1_80, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_0_4_4, all_0_5_5, all_111_1_80 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_111_1_80, all_0_4_4) = 0, yields: % 24.70/7.00 | (243) all_111_1_80 = all_0_5_5 % 24.70/7.00 | % 24.70/7.00 | From (243) and (217) follows: % 24.70/7.00 | (244) mem(all_138_1_85, all_0_5_5) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (78) with all_138_1_85, all_0_5_5, 0, all_138_0_84 and discharging atoms mem(all_138_1_85, all_0_5_5) = all_138_0_84, mem(all_138_1_85, all_0_5_5) = 0, yields: % 24.70/7.00 | (245) all_138_0_84 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (245) can reduce 216 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (247) all_101_0_76 = 0 & mem(all_89_1_75, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (247) yields: % 24.70/7.00 | (209) all_101_0_76 = 0 % 24.70/7.00 | (249) mem(all_89_1_75, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (205), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (211) all_124_0_82 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (211) can reduce 203 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (203) ~ (all_124_0_82 = 0) % 24.70/7.00 | (214) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_111_1_80) = 0 & mem(v0, all_78_2_71) = v1) % 24.70/7.00 | % 24.70/7.00 | Instantiating (214) with all_138_0_90, all_138_1_91 yields: % 24.70/7.00 | (254) ~ (all_138_0_90 = 0) & mem(all_138_1_91, all_111_1_80) = 0 & mem(all_138_1_91, all_78_2_71) = all_138_0_90 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (254) yields: % 24.70/7.00 | (255) ~ (all_138_0_90 = 0) % 24.70/7.00 | (256) mem(all_138_1_91, all_111_1_80) = 0 % 24.70/7.00 | (257) mem(all_138_1_91, all_78_2_71) = all_138_0_90 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_0_4_4, all_0_5_5, all_89_1_75 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_89_1_75, all_0_4_4) = 0, yields: % 24.70/7.00 | (258) all_89_1_75 = all_0_5_5 % 24.70/7.00 | % 24.70/7.00 | From (258) and (175) follows: % 24.70/7.00 | (259) mem(all_0_5_5, all_61_1_65) = all_89_0_74 % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (197), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (221) all_119_0_81 = 0 & mem(all_78_2_71, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (221) yields: % 24.70/7.00 | (222) all_119_0_81 = 0 % 24.70/7.00 | (223) mem(all_78_2_71, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_57_0_62, all_0_1_1, all_78_2_71 and discharging atoms s(all_0_1_1) = all_57_0_62, mem(all_78_2_71, all_57_0_62) = 0, yields: % 24.70/7.00 | (224) all_78_2_71 = all_0_1_1 % 24.70/7.00 | % 24.70/7.00 | From (224) and (257) follows: % 24.70/7.00 | (264) mem(all_138_1_91, all_0_1_1) = all_138_0_90 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (110) with all_138_0_90, all_0_1_1, all_0_5_5, all_0_2_2, all_138_1_91 and discharging atoms u(all_0_2_2, all_0_5_5) = all_0_1_1, mem(all_138_1_91, all_0_1_1) = all_138_0_90, yields: % 24.70/7.00 | (265) all_138_0_90 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_138_1_91, all_0_2_2) = v0 & mem(all_138_1_91, all_0_5_5) = v1) % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (207), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (233) all_131_0_83 = 0 & mem(all_111_1_80, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (233) yields: % 24.70/7.00 | (234) all_131_0_83 = 0 % 24.70/7.00 | (235) mem(all_111_1_80, all_57_0_62) = 0 % 24.70/7.00 | % 24.70/7.00 +-Applying beta-rule and splitting (265), into two cases. % 24.70/7.00 |-Branch one: % 24.70/7.00 | (269) all_138_0_90 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (269) can reduce 255 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (255) ~ (all_138_0_90 = 0) % 24.70/7.00 | (272) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_138_1_91, all_0_2_2) = v0 & mem(all_138_1_91, all_0_5_5) = v1) % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_57_0_62, all_0_1_1, all_111_1_80 and discharging atoms s(all_0_1_1) = all_57_0_62, mem(all_111_1_80, all_57_0_62) = 0, yields: % 24.70/7.00 | (236) all_111_1_80 = all_0_1_1 % 24.70/7.00 | % 24.70/7.00 | From (236) and (256) follows: % 24.70/7.00 | (274) mem(all_138_1_91, all_0_1_1) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (78) with all_138_1_91, all_0_1_1, 0, all_138_0_90 and discharging atoms mem(all_138_1_91, all_0_1_1) = all_138_0_90, mem(all_138_1_91, all_0_1_1) = 0, yields: % 24.70/7.00 | (269) all_138_0_90 = 0 % 24.70/7.00 | % 24.70/7.00 | Equations (269) can reduce 255 to: % 24.70/7.00 | (166) $false % 24.70/7.00 | % 24.70/7.00 |-The branch is then unsatisfiable % 24.70/7.00 |-Branch two: % 24.70/7.00 | (240) all_131_0_83 = 0 & mem(all_111_1_80, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Applying alpha-rule on (240) yields: % 24.70/7.00 | (234) all_131_0_83 = 0 % 24.70/7.00 | (242) mem(all_111_1_80, all_0_4_4) = 0 % 24.70/7.00 | % 24.70/7.00 | Instantiating formula (121) with all_0_4_4, all_0_5_5, all_111_1_80 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_111_1_80, all_0_4_4) = 0, yields: % 24.70/7.01 | (243) all_111_1_80 = all_0_5_5 % 24.70/7.01 | % 24.70/7.01 | From (243) and (193) follows: % 24.70/7.01 | (281) mem(all_0_5_5, all_61_1_65) = 0 % 24.70/7.01 | % 24.70/7.01 | Instantiating formula (78) with all_0_5_5, all_61_1_65, 0, all_89_0_74 and discharging atoms mem(all_0_5_5, all_61_1_65) = all_89_0_74, mem(all_0_5_5, all_61_1_65) = 0, yields: % 24.70/7.01 | (226) all_89_0_74 = 0 % 24.70/7.01 | % 24.70/7.01 | Equations (226) can reduce 174 to: % 24.70/7.01 | (166) $false % 24.70/7.01 | % 24.70/7.01 |-The branch is then unsatisfiable % 24.70/7.01 |-Branch two: % 24.70/7.01 | (228) all_119_0_81 = 0 & mem(all_78_2_71, all_0_4_4) = 0 % 24.70/7.01 | % 24.70/7.01 | Applying alpha-rule on (228) yields: % 24.70/7.01 | (222) all_119_0_81 = 0 % 24.70/7.01 | (230) mem(all_78_2_71, all_0_4_4) = 0 % 24.70/7.01 | % 24.70/7.01 | Instantiating formula (121) with all_0_4_4, all_0_5_5, all_78_2_71 and discharging atoms s(all_0_5_5) = all_0_4_4, mem(all_78_2_71, all_0_4_4) = 0, yields: % 24.70/7.01 | (231) all_78_2_71 = all_0_5_5 % 24.70/7.01 | % 24.70/7.01 | From (231) and (164) follows: % 24.70/7.01 | (281) mem(all_0_5_5, all_61_1_65) = 0 % 24.70/7.01 | % 24.70/7.01 | Instantiating formula (78) with all_0_5_5, all_61_1_65, 0, all_89_0_74 and discharging atoms mem(all_0_5_5, all_61_1_65) = all_89_0_74, mem(all_0_5_5, all_61_1_65) = 0, yields: % 24.70/7.01 | (226) all_89_0_74 = 0 % 24.70/7.01 | % 24.70/7.01 | Equations (226) can reduce 174 to: % 24.70/7.01 | (166) $false % 24.70/7.01 | % 24.70/7.01 |-The branch is then unsatisfiable % 24.70/7.01 % SZS output end Proof for theBenchmark % 24.70/7.01 % 24.70/7.01 6493ms %------------------------------------------------------------------------------