%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV550+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n016.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 21.34s 5.66s % Output : Proof 25.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEV550+1 : TPTP v9.1.0. Released v9.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n016.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Mar 31 11:49:23 EDT 2025 % 0.12/0.33 % CPUTime : % 0.59/0.58 ____ _ % 0.59/0.58 ___ / __ \_____(_)___ ________ __________ % 0.59/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.58 % 0.59/0.58 A Theorem Prover for First-Order Logic % 0.59/0.58 (ePrincess v.1.0) % 0.59/0.58 % 0.59/0.58 (c) Philipp Rümmer, 2009-2015 % 0.59/0.58 (c) Peter Backeman, 2014-2015 % 0.59/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.59/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.59/0.58 Bug reports to peter@backeman.se % 0.59/0.58 % 0.59/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.59/0.58 % 0.59/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.59/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.62/0.92 Prover 0: Preprocessing ... % 2.34/1.17 Prover 0: Warning: ignoring some quantifiers % 2.46/1.20 Prover 0: Constructing countermodel ... % 15.55/4.30 Prover 0: gave up % 15.55/4.30 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 15.81/4.34 Prover 1: Preprocessing ... % 16.41/4.46 Prover 1: Constructing countermodel ... % 17.88/4.82 Prover 1: gave up % 17.88/4.82 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 18.17/4.85 Prover 2: Preprocessing ... % 18.71/4.99 Prover 2: Warning: ignoring some quantifiers % 18.71/5.00 Prover 2: Constructing countermodel ... % 21.34/5.66 Prover 2: proved (840ms) % 21.34/5.66 % 21.34/5.66 No countermodel exists, formula is valid % 21.34/5.66 % SZS status Theorem for theBenchmark % 21.34/5.66 % 21.34/5.66 Generating proof ... Warning: ignoring some quantifiers % 25.23/6.50 found it (size 375) % 25.23/6.50 % 25.23/6.50 % SZS output start Proof for theBenchmark % 25.23/6.50 Assumed formulas after preprocessing and simplification: % 25.23/6.50 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (atleast4p(v3) = 0 & n(v1) = v2 & n(e) = v0 & u(v0, v2) = v3 & s(v0) = v1 & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (m(v5, v6) = v7) | ~ (mem(v4, v7) = v8) | ? [v9] : ((v9 = 0 & mem(v4, v6) = 0) | ( ~ (v9 = 0) & mem(v4, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (u(v5, v6) = v7) | ~ (mem(v4, v7) = v8) | ? [v9] : ? [v10] : ( ~ (v10 = 0) & ~ (v9 = 0) & mem(v4, v6) = v10 & mem(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast16p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast15p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast15p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast14p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast14p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast13p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast13p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast12p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast12p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast11p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast11p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast10p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast10p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast9p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast9p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast8p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast8p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast7p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast7p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast6p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast6p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast5p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast5p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast4p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast4p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast3p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v5 = 0 | ~ (atleast3p(v4) = v5) | ~ (subq(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & atleast2p(v6) = v8) | ( ~ (v8 = 0) & subq(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (p(v5) = v6) | ~ (mem(v4, v6) = v7) | ? [v8] : ( ~ (v8 = 0) & subq(v4, v5) = v8)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (subq(v4, v5) = 0) | ~ (mem(v6, v5) = v7) | ? [v8] : ( ~ (v8 = 0) & mem(v6, v4) = v8)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (a(v7, v6) = v5) | ~ (a(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (m(v7, v6) = v5) | ~ (m(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (u(v7, v6) = v5) | ~ (u(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (disj(v7, v6) = v5) | ~ (disj(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (subq(v7, v6) = v5) | ~ (subq(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (mem(v7, v6) = v5) | ~ (mem(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = 0 | ~ (atleast2p(v4) = v5) | ~ (p(v6) = v7) | ? [v8] : ((v8 = 0 & subq(v4, v7) = 0) | ( ~ (v8 = 0) & mem(v6, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (m(v5, v6) = v7) | ~ (mem(v4, v7) = 0) | ? [v8] : ( ~ (v8 = 0) & mem(v4, v6) = v8 & mem(v4, v5) = 0)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (u(v5, v6) = v7) | ~ (mem(v4, v7) = 0) | ? [v8] : ((v8 = 0 & mem(v4, v6) = 0) | (v8 = 0 & mem(v4, v5) = 0))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (u(v4, v6) = v7) | ~ (s(v5) = v6) | a(v4, v5) = v7) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (s(v4) = v5) | ~ (mem(v4, v5) = v6)) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (disj(v4, v5) = v6) | ? [v7] : (mem(v7, v5) = 0 & mem(v7, v4) = 0)) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (subq(v4, v5) = v6) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & p(v5) = v7 & mem(v4, v7) = v8)) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (subq(v4, v5) = v6) | ? [v7] : ? [v8] : ( ~ (v8 = 0) & mem(v7, v5) = v8 & mem(v7, v4) = 0)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast16p(v6) = v5) | ~ (atleast16p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast15p(v6) = v5) | ~ (atleast15p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast14p(v6) = v5) | ~ (atleast14p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast13p(v6) = v5) | ~ (atleast13p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast12p(v6) = v5) | ~ (atleast12p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast11p(v6) = v5) | ~ (atleast11p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast10p(v6) = v5) | ~ (atleast10p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast9p(v6) = v5) | ~ (atleast9p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast8p(v6) = v5) | ~ (atleast8p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast7p(v6) = v5) | ~ (atleast7p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast6p(v6) = v5) | ~ (atleast6p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast5p(v6) = v5) | ~ (atleast5p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast4p(v6) = v5) | ~ (atleast4p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast3p(v6) = v5) | ~ (atleast3p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (atleast2p(v6) = v5) | ~ (atleast2p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (p(v6) = v5) | ~ (p(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (n(v6) = v5) | ~ (n(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (s(v6) = v5) | ~ (s(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (s(v5) = v6) | ~ (mem(v4, v6) = 0)) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast16p(v4) = v5) | ~ (atleast15p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast16p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast15p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast15p(v4) = v5) | ~ (atleast14p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast15p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast14p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast14p(v4) = v5) | ~ (atleast13p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast14p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast13p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast13p(v4) = v5) | ~ (atleast12p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast13p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast12p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast12p(v4) = v5) | ~ (atleast11p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast12p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast11p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast11p(v4) = v5) | ~ (atleast10p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast11p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast10p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast10p(v4) = v5) | ~ (atleast9p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast10p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast9p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast9p(v4) = v5) | ~ (atleast8p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast9p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast8p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast8p(v4) = v5) | ~ (atleast7p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast8p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast7p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast7p(v4) = v5) | ~ (atleast6p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast7p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast6p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast6p(v4) = v5) | ~ (atleast5p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast6p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast5p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast5p(v4) = v5) | ~ (atleast4p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast5p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast4p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast4p(v4) = v5) | ~ (atleast3p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast4p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast3p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast3p(v4) = v5) | ~ (atleast2p(v6) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & subq(v6, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast3p(v4) = v5) | ~ (subq(v6, v4) = 0) | ? [v7] : ((v7 = 0 & subq(v4, v6) = 0) | ( ~ (v7 = 0) & atleast2p(v6) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = 0 | ~ (atleast2p(v4) = v5) | ~ (mem(v6, v4) = 0) | ? [v7] : (p(v6) = v7 & subq(v4, v7) = 0)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (p(v5) = v6) | ~ (mem(v4, v6) = 0) | subq(v4, v5) = 0) & ! [v4] : ! [v5] : ! [v6] : ( ~ (a(v4, v5) = v6) | ? [v7] : (u(v4, v7) = v6 & s(v5) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (disj(v4, v5) = 0) | ~ (mem(v6, v5) = 0) | ? [v7] : ( ~ (v7 = 0) & mem(v6, v4) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (disj(v4, v5) = 0) | ~ (mem(v6, v4) = 0) | ? [v7] : ( ~ (v7 = 0) & mem(v6, v5) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (subq(v4, v5) = 0) | ~ (mem(v6, v4) = 0) | mem(v6, v5) = 0) & ! [v4] : ! [v5] : (v5 = v4 | ~ (subq(v5, v4) = 0) | ? [v6] : ( ~ (v6 = 0) & subq(v4, v5) = v6)) & ! [v4] : ! [v5] : (v5 = v4 | ~ (subq(v4, v5) = 0) | ? [v6] : ( ~ (v6 = 0) & subq(v5, v4) = v6)) & ! [v4] : ! [v5] : ( ~ (n(v4) = v5) | a(v4, v4) = v5) & ! [v4] : ! [v5] : ( ~ (a(v4, v4) = v5) | n(v4) = v5) & ! [v4] : ! [v5] : ( ~ (subq(v4, v5) = 0) | ? [v6] : (p(v5) = v6 & mem(v4, v6) = 0)) & ! [v4] : ( ~ (atleast16p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast15p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast15p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast14p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast14p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast13p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast13p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast12p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast12p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast11p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast11p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast10p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast10p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast9p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast9p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast8p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast8p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast7p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast7p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast6p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast6p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast5p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast5p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast4p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast4p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast3p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast3p(v4) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & atleast2p(v5) = 0 & subq(v5, v4) = 0 & subq(v4, v5) = v6)) & ! [v4] : ( ~ (atleast2p(v4) = 0) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = 0) & p(v5) = v6 & subq(v4, v6) = v7 & mem(v5, v4) = 0)) & ! [v4] : ~ (mem(v4, e) = 0) & ? [v4] : ? [v5] : ? [v6] : a(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : m(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : u(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : disj(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : subq(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : mem(v5, v4) = v6 & ? [v4] : ? [v5] : atleast16p(v4) = v5 & ? [v4] : ? [v5] : atleast15p(v4) = v5 & ? [v4] : ? [v5] : atleast14p(v4) = v5 & ? [v4] : ? [v5] : atleast13p(v4) = v5 & ? [v4] : ? [v5] : atleast12p(v4) = v5 & ? [v4] : ? [v5] : atleast11p(v4) = v5 & ? [v4] : ? [v5] : atleast10p(v4) = v5 & ? [v4] : ? [v5] : atleast9p(v4) = v5 & ? [v4] : ? [v5] : atleast8p(v4) = v5 & ? [v4] : ? [v5] : atleast7p(v4) = v5 & ? [v4] : ? [v5] : atleast6p(v4) = v5 & ? [v4] : ? [v5] : atleast5p(v4) = v5 & ? [v4] : ? [v5] : atleast4p(v4) = v5 & ? [v4] : ? [v5] : atleast3p(v4) = v5 & ? [v4] : ? [v5] : atleast2p(v4) = v5 & ? [v4] : ? [v5] : p(v4) = v5 & ? [v4] : ? [v5] : n(v4) = v5 & ? [v4] : ? [v5] : s(v4) = v5) % 25.56/6.56 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 25.56/6.56 | (1) atleast4p(all_0_0_0) = 0 & n(all_0_2_2) = all_0_1_1 & n(e) = all_0_3_3 & u(all_0_3_3, all_0_1_1) = all_0_0_0 & 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 % 25.64/6.59 | % 25.64/6.59 | Applying alpha-rule on (1) yields: % 25.64/6.59 | (2) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.59 | (3) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 25.64/6.59 | (4) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 25.64/6.59 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 25.64/6.59 | (6) ! [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))) % 25.64/6.59 | (7) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 25.64/6.59 | (8) atleast4p(all_0_0_0) = 0 % 25.64/6.59 | (9) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.59 | (10) ! [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))) % 25.64/6.59 | (11) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 25.64/6.59 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.59 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 25.64/6.60 | (14) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 25.64/6.60 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 25.64/6.60 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 25.64/6.60 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 25.64/6.60 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 25.64/6.60 | (19) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 25.64/6.60 | (20) ! [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)) % 25.64/6.60 | (21) ! [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))) % 25.64/6.60 | (22) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.60 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 25.64/6.60 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 25.64/6.60 | (25) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 25.64/6.60 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.60 | (27) ! [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))) % 25.64/6.60 | (28) ! [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))) % 25.64/6.60 | (29) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.60 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 25.64/6.60 | (31) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 25.64/6.60 | (32) s(all_0_3_3) = all_0_2_2 % 25.64/6.60 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 25.64/6.60 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 25.64/6.60 | (35) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.60 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 25.64/6.60 | (37) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 25.64/6.60 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 25.64/6.60 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.60 | (40) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 25.64/6.60 | (41) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 25.64/6.60 | (42) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 25.64/6.60 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 25.64/6.60 | (44) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.60 | (45) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.61 | (46) ! [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))) % 25.64/6.61 | (47) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 25.64/6.61 | (48) ! [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))) % 25.64/6.61 | (49) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 25.64/6.61 | (50) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 25.64/6.61 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 25.64/6.61 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 25.64/6.61 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.61 | (54) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.64/6.61 | (55) ! [v0] : ~ (mem(v0, e) = 0) % 25.64/6.61 | (56) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 25.64/6.61 | (57) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 25.64/6.61 | (58) ? [v0] : ? [v1] : s(v0) = v1 % 25.64/6.61 | (59) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 25.64/6.61 | (60) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 25.64/6.61 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 25.64/6.61 | (62) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.61 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 25.64/6.61 | (64) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.61 | (65) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 25.64/6.61 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.64/6.61 | (67) ? [v0] : ? [v1] : n(v0) = v1 % 25.64/6.61 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 25.64/6.61 | (69) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 25.64/6.61 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 25.64/6.61 | (71) n(e) = all_0_3_3 % 25.64/6.61 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 25.64/6.61 | (73) ! [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))) % 25.64/6.61 | (74) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 25.64/6.61 | (75) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 25.64/6.61 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 25.64/6.61 | (77) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 25.64/6.61 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 25.64/6.61 | (79) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 25.64/6.61 | (80) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 25.64/6.61 | (81) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 25.64/6.61 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 25.64/6.61 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 25.64/6.62 | (84) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 25.64/6.62 | (85) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 25.64/6.62 | (86) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.62 | (87) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 25.80/6.62 | (88) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 25.80/6.62 | (89) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 25.80/6.62 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 25.80/6.62 | (91) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 25.80/6.62 | (92) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 25.80/6.62 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.62 | (94) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 25.80/6.62 | (95) ! [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))) % 25.80/6.62 | (96) ! [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))) % 25.80/6.62 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.62 | (98) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 25.80/6.62 | (99) ! [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))) % 25.80/6.62 | (100) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 25.80/6.62 | (101) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 25.80/6.62 | (102) ! [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))) % 25.80/6.62 | (103) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 25.80/6.62 | (104) ! [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))) % 25.80/6.62 | (105) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 25.80/6.62 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 25.80/6.62 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 25.80/6.62 | (108) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 25.80/6.62 | (109) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.62 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 25.80/6.62 | (111) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 25.80/6.62 | (112) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.62 | (113) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 25.80/6.62 | (114) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.62 | (115) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.63 | (116) ! [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))) % 25.80/6.63 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 25.80/6.63 | (118) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 25.80/6.63 | (119) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.63 | (120) ! [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))) % 25.80/6.63 | (121) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.63 | (122) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.63 | (123) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 25.80/6.63 | (124) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.63 | (125) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 25.80/6.63 | (126) u(all_0_3_3, all_0_1_1) = all_0_0_0 % 25.80/6.63 | (127) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 25.80/6.63 | (128) ! [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))) % 25.80/6.63 | (129) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 25.80/6.63 | (130) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 25.80/6.63 | (131) n(all_0_2_2) = all_0_1_1 % 25.80/6.63 | (132) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 25.80/6.63 | (133) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.80/6.63 | (134) ? [v0] : ? [v1] : p(v0) = v1 % 25.80/6.63 | (135) ! [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))) % 25.80/6.63 | (136) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (124) with all_0_0_0 and discharging atoms atleast4p(all_0_0_0) = 0, yields: % 25.80/6.63 | (137) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast3p(v0) = 0 & subq(v0, all_0_0_0) = 0 & subq(all_0_0_0, v0) = v1) % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (75) with all_0_1_1, all_0_2_2 and discharging atoms n(all_0_2_2) = all_0_1_1, yields: % 25.80/6.63 | (138) a(all_0_2_2, all_0_2_2) = all_0_1_1 % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (75) with all_0_3_3, e and discharging atoms n(e) = all_0_3_3, yields: % 25.80/6.63 | (139) a(e, e) = all_0_3_3 % 25.80/6.63 | % 25.80/6.63 | Instantiating (137) with all_57_0_58, all_57_1_59 yields: % 25.80/6.63 | (140) ~ (all_57_0_58 = 0) & atleast3p(all_57_1_59) = 0 & subq(all_57_1_59, all_0_0_0) = 0 & subq(all_0_0_0, all_57_1_59) = all_57_0_58 % 25.80/6.63 | % 25.80/6.63 | Applying alpha-rule on (140) yields: % 25.80/6.63 | (141) ~ (all_57_0_58 = 0) % 25.80/6.63 | (142) atleast3p(all_57_1_59) = 0 % 25.80/6.63 | (143) subq(all_57_1_59, all_0_0_0) = 0 % 25.80/6.63 | (144) subq(all_0_0_0, all_57_1_59) = all_57_0_58 % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (29) with all_57_1_59 and discharging atoms atleast3p(all_57_1_59) = 0, yields: % 25.80/6.63 | (145) ? [v0] : ? [v1] : ( ~ (v1 = 0) & atleast2p(v0) = 0 & subq(v0, all_57_1_59) = 0 & subq(all_57_1_59, v0) = v1) % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (125) with all_0_1_1, all_0_2_2, all_0_2_2 and discharging atoms a(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 25.80/6.63 | (146) ? [v0] : (u(all_0_2_2, v0) = all_0_1_1 & s(all_0_2_2) = v0) % 25.80/6.63 | % 25.80/6.63 | Instantiating formula (125) with all_0_3_3, e, e and discharging atoms a(e, e) = all_0_3_3, yields: % 25.80/6.64 | (147) ? [v0] : (u(e, v0) = all_0_3_3 & s(e) = v0) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (103) with all_57_0_58, all_57_1_59, all_0_0_0 and discharging atoms subq(all_0_0_0, all_57_1_59) = all_57_0_58, yields: % 25.80/6.64 | (148) all_57_0_58 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_57_1_59) = v0 & mem(all_0_0_0, v0) = v1) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (88) with all_57_0_58, all_57_1_59, all_0_0_0 and discharging atoms subq(all_0_0_0, all_57_1_59) = all_57_0_58, yields: % 25.80/6.64 | (149) all_57_0_58 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_57_1_59) = v1 & mem(v0, all_0_0_0) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating (147) with all_66_0_61 yields: % 25.80/6.64 | (150) u(e, all_66_0_61) = all_0_3_3 & s(e) = all_66_0_61 % 25.80/6.64 | % 25.80/6.64 | Applying alpha-rule on (150) yields: % 25.80/6.64 | (151) u(e, all_66_0_61) = all_0_3_3 % 25.80/6.64 | (152) s(e) = all_66_0_61 % 25.80/6.64 | % 25.80/6.64 | Instantiating (146) with all_68_0_62 yields: % 25.80/6.64 | (153) u(all_0_2_2, all_68_0_62) = all_0_1_1 & s(all_0_2_2) = all_68_0_62 % 25.80/6.64 | % 25.80/6.64 | Applying alpha-rule on (153) yields: % 25.80/6.64 | (154) u(all_0_2_2, all_68_0_62) = all_0_1_1 % 25.80/6.64 | (155) s(all_0_2_2) = all_68_0_62 % 25.80/6.64 | % 25.80/6.64 | Instantiating (145) with all_70_0_63, all_70_1_64 yields: % 25.80/6.64 | (156) ~ (all_70_0_63 = 0) & atleast2p(all_70_1_64) = 0 & subq(all_70_1_64, all_57_1_59) = 0 & subq(all_57_1_59, all_70_1_64) = all_70_0_63 % 25.80/6.64 | % 25.80/6.64 | Applying alpha-rule on (156) yields: % 25.80/6.64 | (157) ~ (all_70_0_63 = 0) % 25.80/6.64 | (158) atleast2p(all_70_1_64) = 0 % 25.80/6.64 | (159) subq(all_70_1_64, all_57_1_59) = 0 % 25.80/6.64 | (160) subq(all_57_1_59, all_70_1_64) = all_70_0_63 % 25.80/6.64 | % 25.80/6.64 +-Applying beta-rule and splitting (148), into two cases. % 25.80/6.64 |-Branch one: % 25.80/6.64 | (161) all_57_0_58 = 0 % 25.80/6.64 | % 25.80/6.64 | Equations (161) can reduce 141 to: % 25.80/6.64 | (162) $false % 25.80/6.64 | % 25.80/6.64 |-The branch is then unsatisfiable % 25.80/6.64 |-Branch two: % 25.80/6.64 | (141) ~ (all_57_0_58 = 0) % 25.80/6.64 | (164) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_57_1_59) = v0 & mem(all_0_0_0, v0) = v1) % 25.80/6.64 | % 25.80/6.64 +-Applying beta-rule and splitting (149), into two cases. % 25.80/6.64 |-Branch one: % 25.80/6.64 | (161) all_57_0_58 = 0 % 25.80/6.64 | % 25.80/6.64 | Equations (161) can reduce 141 to: % 25.80/6.64 | (162) $false % 25.80/6.64 | % 25.80/6.64 |-The branch is then unsatisfiable % 25.80/6.64 |-Branch two: % 25.80/6.64 | (141) ~ (all_57_0_58 = 0) % 25.80/6.64 | (168) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_57_1_59) = v1 & mem(v0, all_0_0_0) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating (168) with all_81_0_67, all_81_1_68 yields: % 25.80/6.64 | (169) ~ (all_81_0_67 = 0) & mem(all_81_1_68, all_57_1_59) = all_81_0_67 & mem(all_81_1_68, all_0_0_0) = 0 % 25.80/6.64 | % 25.80/6.64 | Applying alpha-rule on (169) yields: % 25.80/6.64 | (170) ~ (all_81_0_67 = 0) % 25.80/6.64 | (171) mem(all_81_1_68, all_57_1_59) = all_81_0_67 % 25.80/6.64 | (172) mem(all_81_1_68, all_0_0_0) = 0 % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (14) with all_70_1_64 and discharging atoms atleast2p(all_70_1_64) = 0, yields: % 25.80/6.64 | (173) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = 0) & p(v0) = v1 & subq(all_70_1_64, v1) = v2 & mem(v0, all_70_1_64) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (103) with all_70_0_63, all_70_1_64, all_57_1_59 and discharging atoms subq(all_57_1_59, all_70_1_64) = all_70_0_63, yields: % 25.80/6.64 | (174) all_70_0_63 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_70_1_64) = v0 & mem(all_57_1_59, v0) = v1) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (88) with all_70_0_63, all_70_1_64, all_57_1_59 and discharging atoms subq(all_57_1_59, all_70_1_64) = all_70_0_63, yields: % 25.80/6.64 | (175) all_70_0_63 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_70_1_64) = v1 & mem(v0, all_57_1_59) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (16) with all_81_0_67, all_81_1_68, all_57_1_59, all_70_1_64 and discharging atoms subq(all_70_1_64, all_57_1_59) = 0, mem(all_81_1_68, all_57_1_59) = all_81_0_67, yields: % 25.80/6.64 | (176) all_81_0_67 = 0 | ? [v0] : ( ~ (v0 = 0) & mem(all_81_1_68, all_70_1_64) = v0) % 25.80/6.64 | % 25.80/6.64 | Instantiating formula (95) with all_0_0_0, all_0_1_1, all_0_3_3, all_81_1_68 and discharging atoms u(all_0_3_3, all_0_1_1) = all_0_0_0, mem(all_81_1_68, all_0_0_0) = 0, yields: % 25.80/6.64 | (177) ? [v0] : ((v0 = 0 & mem(all_81_1_68, all_0_1_1) = 0) | (v0 = 0 & mem(all_81_1_68, all_0_3_3) = 0)) % 25.80/6.64 | % 25.80/6.64 | Instantiating (177) with all_88_0_69 yields: % 25.80/6.64 | (178) (all_88_0_69 = 0 & mem(all_81_1_68, all_0_1_1) = 0) | (all_88_0_69 = 0 & mem(all_81_1_68, all_0_3_3) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating (173) with all_91_0_71, all_91_1_72, all_91_2_73 yields: % 25.80/6.64 | (179) ~ (all_91_0_71 = 0) & p(all_91_2_73) = all_91_1_72 & subq(all_70_1_64, all_91_1_72) = all_91_0_71 & mem(all_91_2_73, all_70_1_64) = 0 % 25.80/6.64 | % 25.80/6.64 | Applying alpha-rule on (179) yields: % 25.80/6.64 | (180) ~ (all_91_0_71 = 0) % 25.80/6.64 | (181) p(all_91_2_73) = all_91_1_72 % 25.80/6.64 | (182) subq(all_70_1_64, all_91_1_72) = all_91_0_71 % 25.80/6.64 | (183) mem(all_91_2_73, all_70_1_64) = 0 % 25.80/6.64 | % 25.80/6.64 +-Applying beta-rule and splitting (174), into two cases. % 25.80/6.64 |-Branch one: % 25.80/6.64 | (184) all_70_0_63 = 0 % 25.80/6.64 | % 25.80/6.64 | Equations (184) can reduce 157 to: % 25.80/6.64 | (162) $false % 25.80/6.64 | % 25.80/6.64 |-The branch is then unsatisfiable % 25.80/6.64 |-Branch two: % 25.80/6.64 | (157) ~ (all_70_0_63 = 0) % 25.80/6.64 | (187) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_70_1_64) = v0 & mem(all_57_1_59, v0) = v1) % 25.80/6.64 | % 25.80/6.64 +-Applying beta-rule and splitting (175), into two cases. % 25.80/6.64 |-Branch one: % 25.80/6.64 | (184) all_70_0_63 = 0 % 25.80/6.64 | % 25.80/6.64 | Equations (184) can reduce 157 to: % 25.80/6.64 | (162) $false % 25.80/6.64 | % 25.80/6.64 |-The branch is then unsatisfiable % 25.80/6.64 |-Branch two: % 25.80/6.64 | (157) ~ (all_70_0_63 = 0) % 25.80/6.64 | (191) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_70_1_64) = v1 & mem(v0, all_57_1_59) = 0) % 25.80/6.64 | % 25.80/6.64 | Instantiating (191) with all_102_0_76, all_102_1_77 yields: % 25.80/6.64 | (192) ~ (all_102_0_76 = 0) & mem(all_102_1_77, all_70_1_64) = all_102_0_76 & mem(all_102_1_77, all_57_1_59) = 0 % 25.80/6.65 | % 25.80/6.65 | Applying alpha-rule on (192) yields: % 25.80/6.65 | (193) ~ (all_102_0_76 = 0) % 25.80/6.65 | (194) mem(all_102_1_77, all_70_1_64) = all_102_0_76 % 25.80/6.65 | (195) mem(all_102_1_77, all_57_1_59) = 0 % 25.80/6.65 | % 25.80/6.65 +-Applying beta-rule and splitting (176), into two cases. % 25.80/6.65 |-Branch one: % 25.80/6.65 | (196) all_81_0_67 = 0 % 25.80/6.65 | % 25.80/6.65 | Equations (196) can reduce 170 to: % 25.80/6.65 | (162) $false % 25.80/6.65 | % 25.80/6.65 |-The branch is then unsatisfiable % 25.80/6.65 |-Branch two: % 25.80/6.65 | (170) ~ (all_81_0_67 = 0) % 25.80/6.65 | (199) ? [v0] : ( ~ (v0 = 0) & mem(all_81_1_68, all_70_1_64) = v0) % 25.80/6.65 | % 25.93/6.65 | Instantiating formula (88) with all_91_0_71, all_91_1_72, all_70_1_64 and discharging atoms subq(all_70_1_64, all_91_1_72) = all_91_0_71, yields: % 25.93/6.65 | (200) all_91_0_71 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_91_1_72) = v1 & mem(v0, all_70_1_64) = 0) % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (43) with all_102_1_77, all_0_0_0, all_57_1_59 and discharging atoms subq(all_57_1_59, all_0_0_0) = 0, mem(all_102_1_77, all_57_1_59) = 0, yields: % 25.93/6.65 | (201) mem(all_102_1_77, all_0_0_0) = 0 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (43) with all_91_2_73, all_57_1_59, all_70_1_64 and discharging atoms subq(all_70_1_64, all_57_1_59) = 0, mem(all_91_2_73, all_70_1_64) = 0, yields: % 25.93/6.65 | (202) mem(all_91_2_73, all_57_1_59) = 0 % 25.93/6.65 | % 25.93/6.65 +-Applying beta-rule and splitting (200), into two cases. % 25.93/6.65 |-Branch one: % 25.93/6.65 | (203) all_91_0_71 = 0 % 25.93/6.65 | % 25.93/6.65 | Equations (203) can reduce 180 to: % 25.93/6.65 | (162) $false % 25.93/6.65 | % 25.93/6.65 |-The branch is then unsatisfiable % 25.93/6.65 |-Branch two: % 25.93/6.65 | (180) ~ (all_91_0_71 = 0) % 25.93/6.65 | (206) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_91_1_72) = v1 & mem(v0, all_70_1_64) = 0) % 25.93/6.65 | % 25.93/6.65 | Instantiating (206) with all_123_0_79, all_123_1_80 yields: % 25.93/6.65 | (207) ~ (all_123_0_79 = 0) & mem(all_123_1_80, all_91_1_72) = all_123_0_79 & mem(all_123_1_80, all_70_1_64) = 0 % 25.93/6.65 | % 25.93/6.65 | Applying alpha-rule on (207) yields: % 25.93/6.65 | (208) ~ (all_123_0_79 = 0) % 25.93/6.65 | (209) mem(all_123_1_80, all_91_1_72) = all_123_0_79 % 25.93/6.65 | (210) mem(all_123_1_80, all_70_1_64) = 0 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (110) with all_123_0_79, all_91_1_72, all_91_2_73, all_123_1_80 and discharging atoms p(all_91_2_73) = all_91_1_72, mem(all_123_1_80, all_91_1_72) = all_123_0_79, yields: % 25.93/6.65 | (211) all_123_0_79 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_123_1_80, all_91_2_73) = v0) % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (43) with all_123_1_80, all_57_1_59, all_70_1_64 and discharging atoms subq(all_70_1_64, all_57_1_59) = 0, mem(all_123_1_80, all_70_1_64) = 0, yields: % 25.93/6.65 | (212) mem(all_123_1_80, all_57_1_59) = 0 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (95) with all_0_0_0, all_0_1_1, all_0_3_3, all_102_1_77 and discharging atoms u(all_0_3_3, all_0_1_1) = all_0_0_0, mem(all_102_1_77, all_0_0_0) = 0, yields: % 25.93/6.65 | (213) ? [v0] : ((v0 = 0 & mem(all_102_1_77, all_0_1_1) = 0) | (v0 = 0 & mem(all_102_1_77, all_0_3_3) = 0)) % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (43) with all_91_2_73, all_0_0_0, all_57_1_59 and discharging atoms subq(all_57_1_59, all_0_0_0) = 0, mem(all_91_2_73, all_57_1_59) = 0, yields: % 25.93/6.65 | (214) mem(all_91_2_73, all_0_0_0) = 0 % 25.93/6.65 | % 25.93/6.65 | Instantiating (213) with all_136_0_83 yields: % 25.93/6.65 | (215) (all_136_0_83 = 0 & mem(all_102_1_77, all_0_1_1) = 0) | (all_136_0_83 = 0 & mem(all_102_1_77, all_0_3_3) = 0) % 25.93/6.65 | % 25.93/6.65 +-Applying beta-rule and splitting (211), into two cases. % 25.93/6.65 |-Branch one: % 25.93/6.65 | (216) all_123_0_79 = 0 % 25.93/6.65 | % 25.93/6.65 | Equations (216) can reduce 208 to: % 25.93/6.65 | (162) $false % 25.93/6.65 | % 25.93/6.65 |-The branch is then unsatisfiable % 25.93/6.65 |-Branch two: % 25.93/6.65 | (208) ~ (all_123_0_79 = 0) % 25.93/6.65 | (219) ? [v0] : ( ~ (v0 = 0) & subq(all_123_1_80, all_91_2_73) = v0) % 25.93/6.65 | % 25.93/6.65 | Instantiating (219) with all_141_0_84 yields: % 25.93/6.65 | (220) ~ (all_141_0_84 = 0) & subq(all_123_1_80, all_91_2_73) = all_141_0_84 % 25.93/6.65 | % 25.93/6.65 | Applying alpha-rule on (220) yields: % 25.93/6.65 | (221) ~ (all_141_0_84 = 0) % 25.93/6.65 | (222) subq(all_123_1_80, all_91_2_73) = all_141_0_84 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (88) with all_141_0_84, all_91_2_73, all_123_1_80 and discharging atoms subq(all_123_1_80, all_91_2_73) = all_141_0_84, yields: % 25.93/6.65 | (223) all_141_0_84 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_123_1_80) = 0 & mem(v0, all_91_2_73) = v1) % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (43) with all_123_1_80, all_0_0_0, all_57_1_59 and discharging atoms subq(all_57_1_59, all_0_0_0) = 0, mem(all_123_1_80, all_57_1_59) = 0, yields: % 25.93/6.65 | (224) mem(all_123_1_80, all_0_0_0) = 0 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (95) with all_0_0_0, all_0_1_1, all_0_3_3, all_91_2_73 and discharging atoms u(all_0_3_3, all_0_1_1) = all_0_0_0, mem(all_91_2_73, all_0_0_0) = 0, yields: % 25.93/6.65 | (225) ? [v0] : ((v0 = 0 & mem(all_91_2_73, all_0_1_1) = 0) | (v0 = 0 & mem(all_91_2_73, all_0_3_3) = 0)) % 25.93/6.65 | % 25.93/6.65 | Instantiating (225) with all_149_0_85 yields: % 25.93/6.65 | (226) (all_149_0_85 = 0 & mem(all_91_2_73, all_0_1_1) = 0) | (all_149_0_85 = 0 & mem(all_91_2_73, all_0_3_3) = 0) % 25.93/6.65 | % 25.93/6.65 +-Applying beta-rule and splitting (223), into two cases. % 25.93/6.65 |-Branch one: % 25.93/6.65 | (227) all_141_0_84 = 0 % 25.93/6.65 | % 25.93/6.65 | Equations (227) can reduce 221 to: % 25.93/6.65 | (162) $false % 25.93/6.65 | % 25.93/6.65 |-The branch is then unsatisfiable % 25.93/6.65 |-Branch two: % 25.93/6.65 | (221) ~ (all_141_0_84 = 0) % 25.93/6.65 | (230) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_123_1_80) = 0 & mem(v0, all_91_2_73) = v1) % 25.93/6.65 | % 25.93/6.65 | Instantiating (230) with all_154_0_86, all_154_1_87 yields: % 25.93/6.65 | (231) ~ (all_154_0_86 = 0) & mem(all_154_1_87, all_123_1_80) = 0 & mem(all_154_1_87, all_91_2_73) = all_154_0_86 % 25.93/6.65 | % 25.93/6.65 | Applying alpha-rule on (231) yields: % 25.93/6.65 | (232) ~ (all_154_0_86 = 0) % 25.93/6.65 | (233) mem(all_154_1_87, all_123_1_80) = 0 % 25.93/6.65 | (234) mem(all_154_1_87, all_91_2_73) = all_154_0_86 % 25.93/6.65 | % 25.93/6.65 | Instantiating formula (95) with all_0_0_0, all_0_1_1, all_0_3_3, all_123_1_80 and discharging atoms u(all_0_3_3, all_0_1_1) = all_0_0_0, mem(all_123_1_80, all_0_0_0) = 0, yields: % 25.93/6.65 | (235) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_0_1_1) = 0) | (v0 = 0 & mem(all_123_1_80, all_0_3_3) = 0)) % 25.93/6.66 | % 25.93/6.66 | Instantiating (235) with all_161_0_88 yields: % 25.93/6.66 | (236) (all_161_0_88 = 0 & mem(all_123_1_80, all_0_1_1) = 0) | (all_161_0_88 = 0 & mem(all_123_1_80, all_0_3_3) = 0) % 25.93/6.66 | % 25.93/6.66 +-Applying beta-rule and splitting (178), into two cases. % 25.93/6.66 |-Branch one: % 25.93/6.66 | (237) all_88_0_69 = 0 & mem(all_81_1_68, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Applying alpha-rule on (237) yields: % 25.93/6.66 | (238) all_88_0_69 = 0 % 25.93/6.66 | (239) mem(all_81_1_68, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_81_1_68 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_81_1_68, all_0_1_1) = 0, yields: % 25.93/6.66 | (240) ? [v0] : ((v0 = 0 & mem(all_81_1_68, all_68_0_62) = 0) | (v0 = 0 & mem(all_81_1_68, all_0_2_2) = 0)) % 25.93/6.66 | % 25.93/6.66 | Instantiating (240) with all_169_0_89 yields: % 25.93/6.66 | (241) (all_169_0_89 = 0 & mem(all_81_1_68, all_68_0_62) = 0) | (all_169_0_89 = 0 & mem(all_81_1_68, all_0_2_2) = 0) % 25.93/6.66 | % 25.93/6.66 +-Applying beta-rule and splitting (215), into two cases. % 25.93/6.66 |-Branch one: % 25.93/6.66 | (242) all_136_0_83 = 0 & mem(all_102_1_77, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Applying alpha-rule on (242) yields: % 25.93/6.66 | (243) all_136_0_83 = 0 % 25.93/6.66 | (244) mem(all_102_1_77, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_102_1_77 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_102_1_77, all_0_1_1) = 0, yields: % 25.93/6.66 | (245) ? [v0] : ((v0 = 0 & mem(all_102_1_77, all_68_0_62) = 0) | (v0 = 0 & mem(all_102_1_77, all_0_2_2) = 0)) % 25.93/6.66 | % 25.93/6.66 | Instantiating (245) with all_177_0_90 yields: % 25.93/6.66 | (246) (all_177_0_90 = 0 & mem(all_102_1_77, all_68_0_62) = 0) | (all_177_0_90 = 0 & mem(all_102_1_77, all_0_2_2) = 0) % 25.93/6.66 | % 25.93/6.66 +-Applying beta-rule and splitting (236), into two cases. % 25.93/6.66 |-Branch one: % 25.93/6.66 | (247) all_161_0_88 = 0 & mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Applying alpha-rule on (247) yields: % 25.93/6.66 | (248) all_161_0_88 = 0 % 25.93/6.66 | (249) mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_123_1_80, all_0_1_1) = 0, yields: % 25.93/6.66 | (250) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (v0 = 0 & mem(all_123_1_80, all_0_2_2) = 0)) % 25.93/6.66 | % 25.93/6.66 | Instantiating (250) with all_193_0_94 yields: % 25.93/6.66 | (251) (all_193_0_94 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (all_193_0_94 = 0 & mem(all_123_1_80, all_0_2_2) = 0) % 25.93/6.66 | % 25.93/6.66 +-Applying beta-rule and splitting (241), into two cases. % 25.93/6.66 |-Branch one: % 25.93/6.66 | (252) all_169_0_89 = 0 & mem(all_81_1_68, all_68_0_62) = 0 % 25.93/6.66 | % 25.93/6.66 | Applying alpha-rule on (252) yields: % 25.93/6.66 | (253) all_169_0_89 = 0 % 25.93/6.66 | (254) mem(all_81_1_68, all_68_0_62) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_81_1_68 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_81_1_68, all_68_0_62) = 0, yields: % 25.93/6.66 | (255) all_81_1_68 = all_0_2_2 % 25.93/6.66 | % 25.93/6.66 | From (255) and (171) follows: % 25.93/6.66 | (256) mem(all_0_2_2, all_57_1_59) = all_81_0_67 % 25.93/6.66 | % 25.93/6.66 +-Applying beta-rule and splitting (246), into two cases. % 25.93/6.66 |-Branch one: % 25.93/6.66 | (257) all_177_0_90 = 0 & mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.66 | % 25.93/6.66 | Applying alpha-rule on (257) yields: % 25.93/6.66 | (258) all_177_0_90 = 0 % 25.93/6.66 | (259) mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_102_1_77 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_102_1_77, all_68_0_62) = 0, yields: % 25.93/6.66 | (260) all_102_1_77 = all_0_2_2 % 25.93/6.66 | % 25.93/6.66 | From (260) and (195) follows: % 25.93/6.66 | (261) mem(all_0_2_2, all_57_1_59) = 0 % 25.93/6.66 | % 25.93/6.66 | Instantiating formula (83) with all_0_2_2, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_2_2, all_57_1_59) = all_81_0_67, mem(all_0_2_2, all_57_1_59) = 0, yields: % 25.93/6.67 | (196) all_81_0_67 = 0 % 25.93/6.67 | % 25.93/6.67 | Equations (196) can reduce 170 to: % 25.93/6.67 | (162) $false % 25.93/6.67 | % 25.93/6.67 |-The branch is then unsatisfiable % 25.93/6.67 |-Branch two: % 25.93/6.67 | (264) all_177_0_90 = 0 & mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (264) yields: % 25.93/6.67 | (258) all_177_0_90 = 0 % 25.93/6.67 | (266) mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_102_1_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_102_1_77, all_0_2_2) = 0, yields: % 25.93/6.67 | (267) all_102_1_77 = all_0_3_3 % 25.93/6.67 | % 25.93/6.67 | From (267) and (194) follows: % 25.93/6.67 | (268) mem(all_0_3_3, all_70_1_64) = all_102_0_76 % 25.93/6.67 | % 25.93/6.67 +-Applying beta-rule and splitting (251), into two cases. % 25.93/6.67 |-Branch one: % 25.93/6.67 | (269) all_193_0_94 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (269) yields: % 25.93/6.67 | (270) all_193_0_94 = 0 % 25.93/6.67 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.67 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.67 | % 25.93/6.67 | From (272) and (212) follows: % 25.93/6.67 | (261) mem(all_0_2_2, all_57_1_59) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (83) with all_0_2_2, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_2_2, all_57_1_59) = all_81_0_67, mem(all_0_2_2, all_57_1_59) = 0, yields: % 25.93/6.67 | (196) all_81_0_67 = 0 % 25.93/6.67 | % 25.93/6.67 | Equations (196) can reduce 170 to: % 25.93/6.67 | (162) $false % 25.93/6.67 | % 25.93/6.67 |-The branch is then unsatisfiable % 25.93/6.67 |-Branch two: % 25.93/6.67 | (276) all_193_0_94 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (276) yields: % 25.93/6.67 | (270) all_193_0_94 = 0 % 25.93/6.67 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.67 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.67 | % 25.93/6.67 | From (279) and (210) follows: % 25.93/6.67 | (280) mem(all_0_3_3, all_70_1_64) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (83) with all_0_3_3, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_3_3, all_70_1_64) = all_102_0_76, mem(all_0_3_3, all_70_1_64) = 0, yields: % 25.93/6.67 | (281) all_102_0_76 = 0 % 25.93/6.67 | % 25.93/6.67 | Equations (281) can reduce 193 to: % 25.93/6.67 | (162) $false % 25.93/6.67 | % 25.93/6.67 |-The branch is then unsatisfiable % 25.93/6.67 |-Branch two: % 25.93/6.67 | (283) all_169_0_89 = 0 & mem(all_81_1_68, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (283) yields: % 25.93/6.67 | (253) all_169_0_89 = 0 % 25.93/6.67 | (285) mem(all_81_1_68, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_81_1_68 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_81_1_68, all_0_2_2) = 0, yields: % 25.93/6.67 | (286) all_81_1_68 = all_0_3_3 % 25.93/6.67 | % 25.93/6.67 | From (286) and (171) follows: % 25.93/6.67 | (287) mem(all_0_3_3, all_57_1_59) = all_81_0_67 % 25.93/6.67 | % 25.93/6.67 +-Applying beta-rule and splitting (246), into two cases. % 25.93/6.67 |-Branch one: % 25.93/6.67 | (257) all_177_0_90 = 0 & mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (257) yields: % 25.93/6.67 | (258) all_177_0_90 = 0 % 25.93/6.67 | (259) mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_102_1_77 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_102_1_77, all_68_0_62) = 0, yields: % 25.93/6.67 | (260) all_102_1_77 = all_0_2_2 % 25.93/6.67 | % 25.93/6.67 | From (260) and (194) follows: % 25.93/6.67 | (292) mem(all_0_2_2, all_70_1_64) = all_102_0_76 % 25.93/6.67 | % 25.93/6.67 +-Applying beta-rule and splitting (251), into two cases. % 25.93/6.67 |-Branch one: % 25.93/6.67 | (269) all_193_0_94 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (269) yields: % 25.93/6.67 | (270) all_193_0_94 = 0 % 25.93/6.67 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.67 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.67 | % 25.93/6.67 | From (272) and (210) follows: % 25.93/6.67 | (297) mem(all_0_2_2, all_70_1_64) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (83) with all_0_2_2, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_2_2, all_70_1_64) = all_102_0_76, mem(all_0_2_2, all_70_1_64) = 0, yields: % 25.93/6.67 | (281) all_102_0_76 = 0 % 25.93/6.67 | % 25.93/6.67 | Equations (281) can reduce 193 to: % 25.93/6.67 | (162) $false % 25.93/6.67 | % 25.93/6.67 |-The branch is then unsatisfiable % 25.93/6.67 |-Branch two: % 25.93/6.67 | (276) all_193_0_94 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Applying alpha-rule on (276) yields: % 25.93/6.67 | (270) all_193_0_94 = 0 % 25.93/6.67 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.67 | % 25.93/6.67 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.67 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.67 | % 25.93/6.67 | From (279) and (212) follows: % 25.93/6.68 | (304) mem(all_0_3_3, all_57_1_59) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (83) with all_0_3_3, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_3_3, all_57_1_59) = all_81_0_67, mem(all_0_3_3, all_57_1_59) = 0, yields: % 25.93/6.68 | (196) all_81_0_67 = 0 % 25.93/6.68 | % 25.93/6.68 | Equations (196) can reduce 170 to: % 25.93/6.68 | (162) $false % 25.93/6.68 | % 25.93/6.68 |-The branch is then unsatisfiable % 25.93/6.68 |-Branch two: % 25.93/6.68 | (264) all_177_0_90 = 0 & mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (264) yields: % 25.93/6.68 | (258) all_177_0_90 = 0 % 25.93/6.68 | (266) mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_102_1_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_102_1_77, all_0_2_2) = 0, yields: % 25.93/6.68 | (267) all_102_1_77 = all_0_3_3 % 25.93/6.68 | % 25.93/6.68 | From (267) and (195) follows: % 25.93/6.68 | (304) mem(all_0_3_3, all_57_1_59) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (83) with all_0_3_3, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_3_3, all_57_1_59) = all_81_0_67, mem(all_0_3_3, all_57_1_59) = 0, yields: % 25.93/6.68 | (196) all_81_0_67 = 0 % 25.93/6.68 | % 25.93/6.68 | Equations (196) can reduce 170 to: % 25.93/6.68 | (162) $false % 25.93/6.68 | % 25.93/6.68 |-The branch is then unsatisfiable % 25.93/6.68 |-Branch two: % 25.93/6.68 | (314) all_161_0_88 = 0 & mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (314) yields: % 25.93/6.68 | (248) all_161_0_88 = 0 % 25.93/6.68 | (316) mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_123_1_80 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_123_1_80, all_0_3_3) = 0, yields: % 25.93/6.68 | (317) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (v0 = 0 & mem(all_123_1_80, e) = 0)) % 25.93/6.68 | % 25.93/6.68 | Instantiating (317) with all_193_0_103 yields: % 25.93/6.68 | (318) (all_193_0_103 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (all_193_0_103 = 0 & mem(all_123_1_80, e) = 0) % 25.93/6.68 | % 25.93/6.68 +-Applying beta-rule and splitting (318), into two cases. % 25.93/6.68 |-Branch one: % 25.93/6.68 | (319) all_193_0_103 = 0 & mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (319) yields: % 25.93/6.68 | (320) all_193_0_103 = 0 % 25.93/6.68 | (321) mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (101) with all_66_0_61, e, all_123_1_80 and discharging atoms s(e) = all_66_0_61, mem(all_123_1_80, all_66_0_61) = 0, yields: % 25.93/6.68 | (322) all_123_1_80 = e % 25.93/6.68 | % 25.93/6.68 | From (322) and (233) follows: % 25.93/6.68 | (323) mem(all_154_1_87, e) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (55) with all_154_1_87 and discharging atoms mem(all_154_1_87, e) = 0, yields: % 25.93/6.68 | (324) $false % 25.93/6.68 | % 25.93/6.68 |-The branch is then unsatisfiable % 25.93/6.68 |-Branch two: % 25.93/6.68 | (325) all_193_0_103 = 0 & mem(all_123_1_80, e) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (325) yields: % 25.93/6.68 | (320) all_193_0_103 = 0 % 25.93/6.68 | (327) mem(all_123_1_80, e) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (55) with all_123_1_80 and discharging atoms mem(all_123_1_80, e) = 0, yields: % 25.93/6.68 | (324) $false % 25.93/6.68 | % 25.93/6.68 |-The branch is then unsatisfiable % 25.93/6.68 |-Branch two: % 25.93/6.68 | (329) all_136_0_83 = 0 & mem(all_102_1_77, all_0_3_3) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (329) yields: % 25.93/6.68 | (243) all_136_0_83 = 0 % 25.93/6.68 | (331) mem(all_102_1_77, all_0_3_3) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_102_1_77 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_102_1_77, all_0_3_3) = 0, yields: % 25.93/6.68 | (332) ? [v0] : ((v0 = 0 & mem(all_102_1_77, all_66_0_61) = 0) | (v0 = 0 & mem(all_102_1_77, e) = 0)) % 25.93/6.68 | % 25.93/6.68 | Instantiating (332) with all_177_0_108 yields: % 25.93/6.68 | (333) (all_177_0_108 = 0 & mem(all_102_1_77, all_66_0_61) = 0) | (all_177_0_108 = 0 & mem(all_102_1_77, e) = 0) % 25.93/6.68 | % 25.93/6.68 +-Applying beta-rule and splitting (226), into two cases. % 25.93/6.68 |-Branch one: % 25.93/6.68 | (334) all_149_0_85 = 0 & mem(all_91_2_73, all_0_1_1) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (334) yields: % 25.93/6.68 | (335) all_149_0_85 = 0 % 25.93/6.68 | (336) mem(all_91_2_73, all_0_1_1) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_91_2_73, all_0_1_1) = 0, yields: % 25.93/6.68 | (337) ? [v0] : ((v0 = 0 & mem(all_91_2_73, all_68_0_62) = 0) | (v0 = 0 & mem(all_91_2_73, all_0_2_2) = 0)) % 25.93/6.68 | % 25.93/6.68 | Instantiating (337) with all_185_0_109 yields: % 25.93/6.68 | (338) (all_185_0_109 = 0 & mem(all_91_2_73, all_68_0_62) = 0) | (all_185_0_109 = 0 & mem(all_91_2_73, all_0_2_2) = 0) % 25.93/6.68 | % 25.93/6.68 +-Applying beta-rule and splitting (236), into two cases. % 25.93/6.68 |-Branch one: % 25.93/6.68 | (247) all_161_0_88 = 0 & mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (247) yields: % 25.93/6.68 | (248) all_161_0_88 = 0 % 25.93/6.68 | (249) mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_123_1_80, all_0_1_1) = 0, yields: % 25.93/6.68 | (250) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (v0 = 0 & mem(all_123_1_80, all_0_2_2) = 0)) % 25.93/6.68 | % 25.93/6.68 | Instantiating (250) with all_193_0_110 yields: % 25.93/6.68 | (343) (all_193_0_110 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (all_193_0_110 = 0 & mem(all_123_1_80, all_0_2_2) = 0) % 25.93/6.68 | % 25.93/6.68 +-Applying beta-rule and splitting (241), into two cases. % 25.93/6.68 |-Branch one: % 25.93/6.68 | (252) all_169_0_89 = 0 & mem(all_81_1_68, all_68_0_62) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (252) yields: % 25.93/6.68 | (253) all_169_0_89 = 0 % 25.93/6.68 | (254) mem(all_81_1_68, all_68_0_62) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_81_1_68 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_81_1_68, all_68_0_62) = 0, yields: % 25.93/6.68 | (255) all_81_1_68 = all_0_2_2 % 25.93/6.68 | % 25.93/6.68 | From (255) and (171) follows: % 25.93/6.68 | (256) mem(all_0_2_2, all_57_1_59) = all_81_0_67 % 25.93/6.68 | % 25.93/6.68 +-Applying beta-rule and splitting (338), into two cases. % 25.93/6.68 |-Branch one: % 25.93/6.68 | (349) all_185_0_109 = 0 & mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (349) yields: % 25.93/6.68 | (350) all_185_0_109 = 0 % 25.93/6.68 | (351) mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_91_2_73, all_68_0_62) = 0, yields: % 25.93/6.68 | (352) all_91_2_73 = all_0_2_2 % 25.93/6.68 | % 25.93/6.68 | From (352) and (202) follows: % 25.93/6.68 | (261) mem(all_0_2_2, all_57_1_59) = 0 % 25.93/6.68 | % 25.93/6.68 | Instantiating formula (83) with all_0_2_2, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_2_2, all_57_1_59) = all_81_0_67, mem(all_0_2_2, all_57_1_59) = 0, yields: % 25.93/6.68 | (196) all_81_0_67 = 0 % 25.93/6.68 | % 25.93/6.68 | Equations (196) can reduce 170 to: % 25.93/6.68 | (162) $false % 25.93/6.68 | % 25.93/6.68 |-The branch is then unsatisfiable % 25.93/6.68 |-Branch two: % 25.93/6.68 | (356) all_185_0_109 = 0 & mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.68 | % 25.93/6.68 | Applying alpha-rule on (356) yields: % 25.93/6.69 | (350) all_185_0_109 = 0 % 25.93/6.69 | (358) mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_91_2_73 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_91_2_73, all_0_2_2) = 0, yields: % 25.93/6.69 | (359) all_91_2_73 = all_0_3_3 % 25.93/6.69 | % 25.93/6.69 | From (359) and (234) follows: % 25.93/6.69 | (360) mem(all_154_1_87, all_0_3_3) = all_154_0_86 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (20) with all_154_0_86, all_0_3_3, all_66_0_61, e, all_154_1_87 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_154_1_87, all_0_3_3) = all_154_0_86, yields: % 25.93/6.69 | (361) all_154_0_86 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_154_1_87, all_66_0_61) = v1 & mem(all_154_1_87, e) = v0) % 25.93/6.69 | % 25.93/6.69 +-Applying beta-rule and splitting (343), into two cases. % 25.93/6.69 |-Branch one: % 25.93/6.69 | (362) all_193_0_110 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (362) yields: % 25.93/6.69 | (363) all_193_0_110 = 0 % 25.93/6.69 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.69 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.69 | % 25.93/6.69 | From (272) and (212) follows: % 25.93/6.69 | (261) mem(all_0_2_2, all_57_1_59) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (83) with all_0_2_2, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_2_2, all_57_1_59) = all_81_0_67, mem(all_0_2_2, all_57_1_59) = 0, yields: % 25.93/6.69 | (196) all_81_0_67 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (196) can reduce 170 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (369) all_193_0_110 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (369) yields: % 25.93/6.69 | (363) all_193_0_110 = 0 % 25.93/6.69 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 +-Applying beta-rule and splitting (361), into two cases. % 25.93/6.69 |-Branch one: % 25.93/6.69 | (372) all_154_0_86 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (372) can reduce 232 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (232) ~ (all_154_0_86 = 0) % 25.93/6.69 | (375) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_154_1_87, all_66_0_61) = v1 & mem(all_154_1_87, e) = v0) % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.69 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.69 | % 25.93/6.69 | From (279) and (233) follows: % 25.93/6.69 | (377) mem(all_154_1_87, all_0_3_3) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (83) with all_154_1_87, all_0_3_3, 0, all_154_0_86 and discharging atoms mem(all_154_1_87, all_0_3_3) = all_154_0_86, mem(all_154_1_87, all_0_3_3) = 0, yields: % 25.93/6.69 | (372) all_154_0_86 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (372) can reduce 232 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (283) all_169_0_89 = 0 & mem(all_81_1_68, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (283) yields: % 25.93/6.69 | (253) all_169_0_89 = 0 % 25.93/6.69 | (285) mem(all_81_1_68, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_81_1_68 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_81_1_68, all_0_2_2) = 0, yields: % 25.93/6.69 | (286) all_81_1_68 = all_0_3_3 % 25.93/6.69 | % 25.93/6.69 | From (286) and (171) follows: % 25.93/6.69 | (287) mem(all_0_3_3, all_57_1_59) = all_81_0_67 % 25.93/6.69 | % 25.93/6.69 +-Applying beta-rule and splitting (338), into two cases. % 25.93/6.69 |-Branch one: % 25.93/6.69 | (349) all_185_0_109 = 0 & mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (349) yields: % 25.93/6.69 | (350) all_185_0_109 = 0 % 25.93/6.69 | (351) mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_91_2_73, all_68_0_62) = 0, yields: % 25.93/6.69 | (352) all_91_2_73 = all_0_2_2 % 25.93/6.69 | % 25.93/6.69 | From (352) and (234) follows: % 25.93/6.69 | (389) mem(all_154_1_87, all_0_2_2) = all_154_0_86 % 25.93/6.69 | % 25.93/6.69 +-Applying beta-rule and splitting (343), into two cases. % 25.93/6.69 |-Branch one: % 25.93/6.69 | (362) all_193_0_110 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (362) yields: % 25.93/6.69 | (363) all_193_0_110 = 0 % 25.93/6.69 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.69 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.69 | % 25.93/6.69 | From (272) and (233) follows: % 25.93/6.69 | (394) mem(all_154_1_87, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (83) with all_154_1_87, all_0_2_2, 0, all_154_0_86 and discharging atoms mem(all_154_1_87, all_0_2_2) = all_154_0_86, mem(all_154_1_87, all_0_2_2) = 0, yields: % 25.93/6.69 | (372) all_154_0_86 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (372) can reduce 232 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (369) all_193_0_110 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (369) yields: % 25.93/6.69 | (363) all_193_0_110 = 0 % 25.93/6.69 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.69 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.69 | % 25.93/6.69 | From (279) and (212) follows: % 25.93/6.69 | (304) mem(all_0_3_3, all_57_1_59) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (83) with all_0_3_3, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_3_3, all_57_1_59) = all_81_0_67, mem(all_0_3_3, all_57_1_59) = 0, yields: % 25.93/6.69 | (196) all_81_0_67 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (196) can reduce 170 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (356) all_185_0_109 = 0 & mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (356) yields: % 25.93/6.69 | (350) all_185_0_109 = 0 % 25.93/6.69 | (358) mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_91_2_73 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_91_2_73, all_0_2_2) = 0, yields: % 25.93/6.69 | (359) all_91_2_73 = all_0_3_3 % 25.93/6.69 | % 25.93/6.69 | From (359) and (202) follows: % 25.93/6.69 | (304) mem(all_0_3_3, all_57_1_59) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (83) with all_0_3_3, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(all_0_3_3, all_57_1_59) = all_81_0_67, mem(all_0_3_3, all_57_1_59) = 0, yields: % 25.93/6.69 | (196) all_81_0_67 = 0 % 25.93/6.69 | % 25.93/6.69 | Equations (196) can reduce 170 to: % 25.93/6.69 | (162) $false % 25.93/6.69 | % 25.93/6.69 |-The branch is then unsatisfiable % 25.93/6.69 |-Branch two: % 25.93/6.69 | (314) all_161_0_88 = 0 & mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.69 | % 25.93/6.69 | Applying alpha-rule on (314) yields: % 25.93/6.69 | (248) all_161_0_88 = 0 % 25.93/6.69 | (316) mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.69 | % 25.93/6.69 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_123_1_80 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_123_1_80, all_0_3_3) = 0, yields: % 25.93/6.69 | (317) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (v0 = 0 & mem(all_123_1_80, e) = 0)) % 25.93/6.69 | % 25.93/6.69 | Instantiating (317) with all_193_0_123 yields: % 25.93/6.69 | (415) (all_193_0_123 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (all_193_0_123 = 0 & mem(all_123_1_80, e) = 0) % 25.93/6.69 | % 25.93/6.69 +-Applying beta-rule and splitting (415), into two cases. % 25.93/6.69 |-Branch one: % 25.93/6.70 | (416) all_193_0_123 = 0 & mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (416) yields: % 25.93/6.70 | (417) all_193_0_123 = 0 % 25.93/6.70 | (321) mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (101) with all_66_0_61, e, all_123_1_80 and discharging atoms s(e) = all_66_0_61, mem(all_123_1_80, all_66_0_61) = 0, yields: % 25.93/6.70 | (322) all_123_1_80 = e % 25.93/6.70 | % 25.93/6.70 | From (322) and (233) follows: % 25.93/6.70 | (323) mem(all_154_1_87, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (55) with all_154_1_87 and discharging atoms mem(all_154_1_87, e) = 0, yields: % 25.93/6.70 | (324) $false % 25.93/6.70 | % 25.93/6.70 |-The branch is then unsatisfiable % 25.93/6.70 |-Branch two: % 25.93/6.70 | (422) all_193_0_123 = 0 & mem(all_123_1_80, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (422) yields: % 25.93/6.70 | (417) all_193_0_123 = 0 % 25.93/6.70 | (327) mem(all_123_1_80, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (55) with all_123_1_80 and discharging atoms mem(all_123_1_80, e) = 0, yields: % 25.93/6.70 | (324) $false % 25.93/6.70 | % 25.93/6.70 |-The branch is then unsatisfiable % 25.93/6.70 |-Branch two: % 25.93/6.70 | (426) all_149_0_85 = 0 & mem(all_91_2_73, all_0_3_3) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (426) yields: % 25.93/6.70 | (335) all_149_0_85 = 0 % 25.93/6.70 | (428) mem(all_91_2_73, all_0_3_3) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_91_2_73 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_91_2_73, all_0_3_3) = 0, yields: % 25.93/6.70 | (429) ? [v0] : ((v0 = 0 & mem(all_91_2_73, all_66_0_61) = 0) | (v0 = 0 & mem(all_91_2_73, e) = 0)) % 25.93/6.70 | % 25.93/6.70 | Instantiating (429) with all_185_0_132 yields: % 25.93/6.70 | (430) (all_185_0_132 = 0 & mem(all_91_2_73, all_66_0_61) = 0) | (all_185_0_132 = 0 & mem(all_91_2_73, e) = 0) % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (333), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (431) all_177_0_108 = 0 & mem(all_102_1_77, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (431) yields: % 25.93/6.70 | (432) all_177_0_108 = 0 % 25.93/6.70 | (433) mem(all_102_1_77, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (101) with all_66_0_61, e, all_102_1_77 and discharging atoms s(e) = all_66_0_61, mem(all_102_1_77, all_66_0_61) = 0, yields: % 25.93/6.70 | (434) all_102_1_77 = e % 25.93/6.70 | % 25.93/6.70 | From (434) and (194) follows: % 25.93/6.70 | (435) mem(e, all_70_1_64) = all_102_0_76 % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (430), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (436) all_185_0_132 = 0 & mem(all_91_2_73, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (436) yields: % 25.93/6.70 | (437) all_185_0_132 = 0 % 25.93/6.70 | (438) mem(all_91_2_73, all_66_0_61) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (101) with all_66_0_61, e, all_91_2_73 and discharging atoms s(e) = all_66_0_61, mem(all_91_2_73, all_66_0_61) = 0, yields: % 25.93/6.70 | (439) all_91_2_73 = e % 25.93/6.70 | % 25.93/6.70 | From (439) and (183) follows: % 25.93/6.70 | (440) mem(e, all_70_1_64) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (83) with e, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(e, all_70_1_64) = all_102_0_76, mem(e, all_70_1_64) = 0, yields: % 25.93/6.70 | (281) all_102_0_76 = 0 % 25.93/6.70 | % 25.93/6.70 | Equations (281) can reduce 193 to: % 25.93/6.70 | (162) $false % 25.93/6.70 | % 25.93/6.70 |-The branch is then unsatisfiable % 25.93/6.70 |-Branch two: % 25.93/6.70 | (443) all_185_0_132 = 0 & mem(all_91_2_73, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (443) yields: % 25.93/6.70 | (437) all_185_0_132 = 0 % 25.93/6.70 | (445) mem(all_91_2_73, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (55) with all_91_2_73 and discharging atoms mem(all_91_2_73, e) = 0, yields: % 25.93/6.70 | (324) $false % 25.93/6.70 | % 25.93/6.70 |-The branch is then unsatisfiable % 25.93/6.70 |-Branch two: % 25.93/6.70 | (447) all_177_0_108 = 0 & mem(all_102_1_77, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (447) yields: % 25.93/6.70 | (432) all_177_0_108 = 0 % 25.93/6.70 | (449) mem(all_102_1_77, e) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (55) with all_102_1_77 and discharging atoms mem(all_102_1_77, e) = 0, yields: % 25.93/6.70 | (324) $false % 25.93/6.70 | % 25.93/6.70 |-The branch is then unsatisfiable % 25.93/6.70 |-Branch two: % 25.93/6.70 | (451) all_88_0_69 = 0 & mem(all_81_1_68, all_0_3_3) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (451) yields: % 25.93/6.70 | (238) all_88_0_69 = 0 % 25.93/6.70 | (453) mem(all_81_1_68, all_0_3_3) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_81_1_68 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_81_1_68, all_0_3_3) = 0, yields: % 25.93/6.70 | (454) ? [v0] : ((v0 = 0 & mem(all_81_1_68, all_66_0_61) = 0) | (v0 = 0 & mem(all_81_1_68, e) = 0)) % 25.93/6.70 | % 25.93/6.70 | Instantiating (454) with all_169_0_134 yields: % 25.93/6.70 | (455) (all_169_0_134 = 0 & mem(all_81_1_68, all_66_0_61) = 0) | (all_169_0_134 = 0 & mem(all_81_1_68, e) = 0) % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (215), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (242) all_136_0_83 = 0 & mem(all_102_1_77, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (242) yields: % 25.93/6.70 | (243) all_136_0_83 = 0 % 25.93/6.70 | (244) mem(all_102_1_77, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_102_1_77 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_102_1_77, all_0_1_1) = 0, yields: % 25.93/6.70 | (245) ? [v0] : ((v0 = 0 & mem(all_102_1_77, all_68_0_62) = 0) | (v0 = 0 & mem(all_102_1_77, all_0_2_2) = 0)) % 25.93/6.70 | % 25.93/6.70 | Instantiating (245) with all_177_0_135 yields: % 25.93/6.70 | (460) (all_177_0_135 = 0 & mem(all_102_1_77, all_68_0_62) = 0) | (all_177_0_135 = 0 & mem(all_102_1_77, all_0_2_2) = 0) % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (226), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (334) all_149_0_85 = 0 & mem(all_91_2_73, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (334) yields: % 25.93/6.70 | (335) all_149_0_85 = 0 % 25.93/6.70 | (336) mem(all_91_2_73, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_91_2_73, all_0_1_1) = 0, yields: % 25.93/6.70 | (337) ? [v0] : ((v0 = 0 & mem(all_91_2_73, all_68_0_62) = 0) | (v0 = 0 & mem(all_91_2_73, all_0_2_2) = 0)) % 25.93/6.70 | % 25.93/6.70 | Instantiating (337) with all_185_0_136 yields: % 25.93/6.70 | (465) (all_185_0_136 = 0 & mem(all_91_2_73, all_68_0_62) = 0) | (all_185_0_136 = 0 & mem(all_91_2_73, all_0_2_2) = 0) % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (236), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (247) all_161_0_88 = 0 & mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (247) yields: % 25.93/6.70 | (248) all_161_0_88 = 0 % 25.93/6.70 | (249) mem(all_123_1_80, all_0_1_1) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (95) with all_0_1_1, all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms u(all_0_2_2, all_68_0_62) = all_0_1_1, mem(all_123_1_80, all_0_1_1) = 0, yields: % 25.93/6.70 | (250) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (v0 = 0 & mem(all_123_1_80, all_0_2_2) = 0)) % 25.93/6.70 | % 25.93/6.70 | Instantiating (250) with all_193_0_137 yields: % 25.93/6.70 | (470) (all_193_0_137 = 0 & mem(all_123_1_80, all_68_0_62) = 0) | (all_193_0_137 = 0 & mem(all_123_1_80, all_0_2_2) = 0) % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (460), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (471) all_177_0_135 = 0 & mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (471) yields: % 25.93/6.70 | (472) all_177_0_135 = 0 % 25.93/6.70 | (259) mem(all_102_1_77, all_68_0_62) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_102_1_77 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_102_1_77, all_68_0_62) = 0, yields: % 25.93/6.70 | (260) all_102_1_77 = all_0_2_2 % 25.93/6.70 | % 25.93/6.70 | From (260) and (194) follows: % 25.93/6.70 | (292) mem(all_0_2_2, all_70_1_64) = all_102_0_76 % 25.93/6.70 | % 25.93/6.70 +-Applying beta-rule and splitting (465), into two cases. % 25.93/6.70 |-Branch one: % 25.93/6.70 | (476) all_185_0_136 = 0 & mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.70 | % 25.93/6.70 | Applying alpha-rule on (476) yields: % 25.93/6.70 | (477) all_185_0_136 = 0 % 25.93/6.70 | (351) mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.70 | % 25.93/6.70 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_91_2_73, all_68_0_62) = 0, yields: % 25.93/6.71 | (352) all_91_2_73 = all_0_2_2 % 25.93/6.71 | % 25.93/6.71 | From (352) and (183) follows: % 25.93/6.71 | (297) mem(all_0_2_2, all_70_1_64) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_0_2_2, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_2_2, all_70_1_64) = all_102_0_76, mem(all_0_2_2, all_70_1_64) = 0, yields: % 25.93/6.71 | (281) all_102_0_76 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (281) can reduce 193 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (483) all_185_0_136 = 0 & mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (483) yields: % 25.93/6.71 | (477) all_185_0_136 = 0 % 25.93/6.71 | (358) mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_91_2_73 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_91_2_73, all_0_2_2) = 0, yields: % 25.93/6.71 | (359) all_91_2_73 = all_0_3_3 % 25.93/6.71 | % 25.93/6.71 | From (359) and (234) follows: % 25.93/6.71 | (360) mem(all_154_1_87, all_0_3_3) = all_154_0_86 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (20) with all_154_0_86, all_0_3_3, all_66_0_61, e, all_154_1_87 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_154_1_87, all_0_3_3) = all_154_0_86, yields: % 25.93/6.71 | (361) all_154_0_86 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_154_1_87, all_66_0_61) = v1 & mem(all_154_1_87, e) = v0) % 25.93/6.71 | % 25.93/6.71 +-Applying beta-rule and splitting (470), into two cases. % 25.93/6.71 |-Branch one: % 25.93/6.71 | (489) all_193_0_137 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (489) yields: % 25.93/6.71 | (490) all_193_0_137 = 0 % 25.93/6.71 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.71 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.71 | % 25.93/6.71 | From (272) and (210) follows: % 25.93/6.71 | (297) mem(all_0_2_2, all_70_1_64) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_0_2_2, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_2_2, all_70_1_64) = all_102_0_76, mem(all_0_2_2, all_70_1_64) = 0, yields: % 25.93/6.71 | (281) all_102_0_76 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (281) can reduce 193 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (496) all_193_0_137 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (496) yields: % 25.93/6.71 | (490) all_193_0_137 = 0 % 25.93/6.71 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 +-Applying beta-rule and splitting (361), into two cases. % 25.93/6.71 |-Branch one: % 25.93/6.71 | (372) all_154_0_86 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (372) can reduce 232 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (232) ~ (all_154_0_86 = 0) % 25.93/6.71 | (375) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_154_1_87, all_66_0_61) = v1 & mem(all_154_1_87, e) = v0) % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.71 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.71 | % 25.93/6.71 | From (279) and (233) follows: % 25.93/6.71 | (377) mem(all_154_1_87, all_0_3_3) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_154_1_87, all_0_3_3, 0, all_154_0_86 and discharging atoms mem(all_154_1_87, all_0_3_3) = all_154_0_86, mem(all_154_1_87, all_0_3_3) = 0, yields: % 25.93/6.71 | (372) all_154_0_86 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (372) can reduce 232 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (507) all_177_0_135 = 0 & mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (507) yields: % 25.93/6.71 | (472) all_177_0_135 = 0 % 25.93/6.71 | (266) mem(all_102_1_77, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_102_1_77 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_102_1_77, all_0_2_2) = 0, yields: % 25.93/6.71 | (267) all_102_1_77 = all_0_3_3 % 25.93/6.71 | % 25.93/6.71 | From (267) and (194) follows: % 25.93/6.71 | (268) mem(all_0_3_3, all_70_1_64) = all_102_0_76 % 25.93/6.71 | % 25.93/6.71 +-Applying beta-rule and splitting (465), into two cases. % 25.93/6.71 |-Branch one: % 25.93/6.71 | (476) all_185_0_136 = 0 & mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (476) yields: % 25.93/6.71 | (477) all_185_0_136 = 0 % 25.93/6.71 | (351) mem(all_91_2_73, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_91_2_73 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_91_2_73, all_68_0_62) = 0, yields: % 25.93/6.71 | (352) all_91_2_73 = all_0_2_2 % 25.93/6.71 | % 25.93/6.71 | From (352) and (234) follows: % 25.93/6.71 | (389) mem(all_154_1_87, all_0_2_2) = all_154_0_86 % 25.93/6.71 | % 25.93/6.71 +-Applying beta-rule and splitting (470), into two cases. % 25.93/6.71 |-Branch one: % 25.93/6.71 | (489) all_193_0_137 = 0 & mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (489) yields: % 25.93/6.71 | (490) all_193_0_137 = 0 % 25.93/6.71 | (271) mem(all_123_1_80, all_68_0_62) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_68_0_62, all_0_2_2, all_123_1_80 and discharging atoms s(all_0_2_2) = all_68_0_62, mem(all_123_1_80, all_68_0_62) = 0, yields: % 25.93/6.71 | (272) all_123_1_80 = all_0_2_2 % 25.93/6.71 | % 25.93/6.71 | From (272) and (233) follows: % 25.93/6.71 | (394) mem(all_154_1_87, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_154_1_87, all_0_2_2, 0, all_154_0_86 and discharging atoms mem(all_154_1_87, all_0_2_2) = all_154_0_86, mem(all_154_1_87, all_0_2_2) = 0, yields: % 25.93/6.71 | (372) all_154_0_86 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (372) can reduce 232 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (496) all_193_0_137 = 0 & mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (496) yields: % 25.93/6.71 | (490) all_193_0_137 = 0 % 25.93/6.71 | (278) mem(all_123_1_80, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_123_1_80 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_123_1_80, all_0_2_2) = 0, yields: % 25.93/6.71 | (279) all_123_1_80 = all_0_3_3 % 25.93/6.71 | % 25.93/6.71 | From (279) and (210) follows: % 25.93/6.71 | (280) mem(all_0_3_3, all_70_1_64) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_0_3_3, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_3_3, all_70_1_64) = all_102_0_76, mem(all_0_3_3, all_70_1_64) = 0, yields: % 25.93/6.71 | (281) all_102_0_76 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (281) can reduce 193 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (483) all_185_0_136 = 0 & mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (483) yields: % 25.93/6.71 | (477) all_185_0_136 = 0 % 25.93/6.71 | (358) mem(all_91_2_73, all_0_2_2) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_0_2_2, all_0_3_3, all_91_2_73 and discharging atoms s(all_0_3_3) = all_0_2_2, mem(all_91_2_73, all_0_2_2) = 0, yields: % 25.93/6.71 | (359) all_91_2_73 = all_0_3_3 % 25.93/6.71 | % 25.93/6.71 | From (359) and (183) follows: % 25.93/6.71 | (280) mem(all_0_3_3, all_70_1_64) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (83) with all_0_3_3, all_70_1_64, 0, all_102_0_76 and discharging atoms mem(all_0_3_3, all_70_1_64) = all_102_0_76, mem(all_0_3_3, all_70_1_64) = 0, yields: % 25.93/6.71 | (281) all_102_0_76 = 0 % 25.93/6.71 | % 25.93/6.71 | Equations (281) can reduce 193 to: % 25.93/6.71 | (162) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (314) all_161_0_88 = 0 & mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (314) yields: % 25.93/6.71 | (248) all_161_0_88 = 0 % 25.93/6.71 | (316) mem(all_123_1_80, all_0_3_3) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_123_1_80 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_123_1_80, all_0_3_3) = 0, yields: % 25.93/6.71 | (317) ? [v0] : ((v0 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (v0 = 0 & mem(all_123_1_80, e) = 0)) % 25.93/6.71 | % 25.93/6.71 | Instantiating (317) with all_193_0_150 yields: % 25.93/6.71 | (542) (all_193_0_150 = 0 & mem(all_123_1_80, all_66_0_61) = 0) | (all_193_0_150 = 0 & mem(all_123_1_80, e) = 0) % 25.93/6.71 | % 25.93/6.71 +-Applying beta-rule and splitting (542), into two cases. % 25.93/6.71 |-Branch one: % 25.93/6.71 | (543) all_193_0_150 = 0 & mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (543) yields: % 25.93/6.71 | (544) all_193_0_150 = 0 % 25.93/6.71 | (321) mem(all_123_1_80, all_66_0_61) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (101) with all_66_0_61, e, all_123_1_80 and discharging atoms s(e) = all_66_0_61, mem(all_123_1_80, all_66_0_61) = 0, yields: % 25.93/6.71 | (322) all_123_1_80 = e % 25.93/6.71 | % 25.93/6.71 | From (322) and (233) follows: % 25.93/6.71 | (323) mem(all_154_1_87, e) = 0 % 25.93/6.71 | % 25.93/6.71 | Instantiating formula (55) with all_154_1_87 and discharging atoms mem(all_154_1_87, e) = 0, yields: % 25.93/6.71 | (324) $false % 25.93/6.71 | % 25.93/6.71 |-The branch is then unsatisfiable % 25.93/6.71 |-Branch two: % 25.93/6.71 | (549) all_193_0_150 = 0 & mem(all_123_1_80, e) = 0 % 25.93/6.71 | % 25.93/6.71 | Applying alpha-rule on (549) yields: % 25.93/6.72 | (544) all_193_0_150 = 0 % 25.93/6.72 | (327) mem(all_123_1_80, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (55) with all_123_1_80 and discharging atoms mem(all_123_1_80, e) = 0, yields: % 25.93/6.72 | (324) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (426) all_149_0_85 = 0 & mem(all_91_2_73, all_0_3_3) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (426) yields: % 25.93/6.72 | (335) all_149_0_85 = 0 % 25.93/6.72 | (428) mem(all_91_2_73, all_0_3_3) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_91_2_73 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_91_2_73, all_0_3_3) = 0, yields: % 25.93/6.72 | (429) ? [v0] : ((v0 = 0 & mem(all_91_2_73, all_66_0_61) = 0) | (v0 = 0 & mem(all_91_2_73, e) = 0)) % 25.93/6.72 | % 25.93/6.72 | Instantiating (429) with all_185_0_159 yields: % 25.93/6.72 | (557) (all_185_0_159 = 0 & mem(all_91_2_73, all_66_0_61) = 0) | (all_185_0_159 = 0 & mem(all_91_2_73, e) = 0) % 25.93/6.72 | % 25.93/6.72 +-Applying beta-rule and splitting (455), into two cases. % 25.93/6.72 |-Branch one: % 25.93/6.72 | (558) all_169_0_134 = 0 & mem(all_81_1_68, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (558) yields: % 25.93/6.72 | (559) all_169_0_134 = 0 % 25.93/6.72 | (560) mem(all_81_1_68, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (101) with all_66_0_61, e, all_81_1_68 and discharging atoms s(e) = all_66_0_61, mem(all_81_1_68, all_66_0_61) = 0, yields: % 25.93/6.72 | (561) all_81_1_68 = e % 25.93/6.72 | % 25.93/6.72 | From (561) and (171) follows: % 25.93/6.72 | (562) mem(e, all_57_1_59) = all_81_0_67 % 25.93/6.72 | % 25.93/6.72 +-Applying beta-rule and splitting (557), into two cases. % 25.93/6.72 |-Branch one: % 25.93/6.72 | (563) all_185_0_159 = 0 & mem(all_91_2_73, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (563) yields: % 25.93/6.72 | (564) all_185_0_159 = 0 % 25.93/6.72 | (438) mem(all_91_2_73, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (101) with all_66_0_61, e, all_91_2_73 and discharging atoms s(e) = all_66_0_61, mem(all_91_2_73, all_66_0_61) = 0, yields: % 25.93/6.72 | (439) all_91_2_73 = e % 25.93/6.72 | % 25.93/6.72 | From (439) and (202) follows: % 25.93/6.72 | (567) mem(e, all_57_1_59) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (83) with e, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(e, all_57_1_59) = all_81_0_67, mem(e, all_57_1_59) = 0, yields: % 25.93/6.72 | (196) all_81_0_67 = 0 % 25.93/6.72 | % 25.93/6.72 | Equations (196) can reduce 170 to: % 25.93/6.72 | (162) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (570) all_185_0_159 = 0 & mem(all_91_2_73, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (570) yields: % 25.93/6.72 | (564) all_185_0_159 = 0 % 25.93/6.72 | (445) mem(all_91_2_73, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (55) with all_91_2_73 and discharging atoms mem(all_91_2_73, e) = 0, yields: % 25.93/6.72 | (324) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (574) all_169_0_134 = 0 & mem(all_81_1_68, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (574) yields: % 25.93/6.72 | (559) all_169_0_134 = 0 % 25.93/6.72 | (576) mem(all_81_1_68, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (55) with all_81_1_68 and discharging atoms mem(all_81_1_68, e) = 0, yields: % 25.93/6.72 | (324) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (329) all_136_0_83 = 0 & mem(all_102_1_77, all_0_3_3) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (329) yields: % 25.93/6.72 | (243) all_136_0_83 = 0 % 25.93/6.72 | (331) mem(all_102_1_77, all_0_3_3) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (95) with all_0_3_3, all_66_0_61, e, all_102_1_77 and discharging atoms u(e, all_66_0_61) = all_0_3_3, mem(all_102_1_77, all_0_3_3) = 0, yields: % 25.93/6.72 | (332) ? [v0] : ((v0 = 0 & mem(all_102_1_77, all_66_0_61) = 0) | (v0 = 0 & mem(all_102_1_77, e) = 0)) % 25.93/6.72 | % 25.93/6.72 | Instantiating (332) with all_177_0_161 yields: % 25.93/6.72 | (582) (all_177_0_161 = 0 & mem(all_102_1_77, all_66_0_61) = 0) | (all_177_0_161 = 0 & mem(all_102_1_77, e) = 0) % 25.93/6.72 | % 25.93/6.72 +-Applying beta-rule and splitting (455), into two cases. % 25.93/6.72 |-Branch one: % 25.93/6.72 | (558) all_169_0_134 = 0 & mem(all_81_1_68, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (558) yields: % 25.93/6.72 | (559) all_169_0_134 = 0 % 25.93/6.72 | (560) mem(all_81_1_68, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (101) with all_66_0_61, e, all_81_1_68 and discharging atoms s(e) = all_66_0_61, mem(all_81_1_68, all_66_0_61) = 0, yields: % 25.93/6.72 | (561) all_81_1_68 = e % 25.93/6.72 | % 25.93/6.72 | From (561) and (171) follows: % 25.93/6.72 | (562) mem(e, all_57_1_59) = all_81_0_67 % 25.93/6.72 | % 25.93/6.72 +-Applying beta-rule and splitting (582), into two cases. % 25.93/6.72 |-Branch one: % 25.93/6.72 | (588) all_177_0_161 = 0 & mem(all_102_1_77, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (588) yields: % 25.93/6.72 | (589) all_177_0_161 = 0 % 25.93/6.72 | (433) mem(all_102_1_77, all_66_0_61) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (101) with all_66_0_61, e, all_102_1_77 and discharging atoms s(e) = all_66_0_61, mem(all_102_1_77, all_66_0_61) = 0, yields: % 25.93/6.72 | (434) all_102_1_77 = e % 25.93/6.72 | % 25.93/6.72 | From (434) and (195) follows: % 25.93/6.72 | (567) mem(e, all_57_1_59) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (83) with e, all_57_1_59, 0, all_81_0_67 and discharging atoms mem(e, all_57_1_59) = all_81_0_67, mem(e, all_57_1_59) = 0, yields: % 25.93/6.72 | (196) all_81_0_67 = 0 % 25.93/6.72 | % 25.93/6.72 | Equations (196) can reduce 170 to: % 25.93/6.72 | (162) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (595) all_177_0_161 = 0 & mem(all_102_1_77, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (595) yields: % 25.93/6.72 | (589) all_177_0_161 = 0 % 25.93/6.72 | (449) mem(all_102_1_77, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (55) with all_102_1_77 and discharging atoms mem(all_102_1_77, e) = 0, yields: % 25.93/6.72 | (324) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 |-Branch two: % 25.93/6.72 | (574) all_169_0_134 = 0 & mem(all_81_1_68, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Applying alpha-rule on (574) yields: % 25.93/6.72 | (559) all_169_0_134 = 0 % 25.93/6.72 | (576) mem(all_81_1_68, e) = 0 % 25.93/6.72 | % 25.93/6.72 | Instantiating formula (55) with all_81_1_68 and discharging atoms mem(all_81_1_68, e) = 0, yields: % 25.93/6.72 | (324) $false % 25.93/6.72 | % 25.93/6.72 |-The branch is then unsatisfiable % 25.93/6.72 % SZS output end Proof for theBenchmark % 25.93/6.72 % 25.93/6.72 6134ms %------------------------------------------------------------------------------