%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV581+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n015.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:03 AM UTC 2025 % Result : Theorem 23.69s 6.65s % Output : Proof 25.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEV581+1 : TPTP v9.1.0. Released v9.1.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.34 % Computer : n015.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Mon Mar 31 13:13:35 EDT 2025 % 0.14/0.34 % CPUTime : % 0.48/0.58 ____ _ % 0.48/0.58 ___ / __ \_____(_)___ ________ __________ % 0.48/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.48/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.48/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.48/0.58 % 0.48/0.58 A Theorem Prover for First-Order Logic % 0.48/0.59 (ePrincess v.1.0) % 0.48/0.59 % 0.48/0.59 (c) Philipp Rümmer, 2009-2015 % 0.48/0.59 (c) Peter Backeman, 2014-2015 % 0.48/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.48/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.48/0.59 Bug reports to peter@backeman.se % 0.48/0.59 % 0.48/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.48/0.59 % 0.48/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.69/0.97 Prover 0: Preprocessing ... % 2.25/1.22 Prover 0: Warning: ignoring some quantifiers % 2.50/1.25 Prover 0: Constructing countermodel ... % 20.24/5.93 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.66/5.99 Prover 1: Preprocessing ... % 21.52/6.16 Prover 1: Constructing countermodel ... % 22.73/6.42 Prover 1: gave up % 22.73/6.42 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 22.87/6.44 Prover 2: Preprocessing ... % 23.36/6.56 Prover 2: Warning: ignoring some quantifiers % 23.36/6.56 Prover 2: Constructing countermodel ... % 23.69/6.65 Prover 2: proved (233ms) % 23.69/6.65 Prover 0: stopped % 23.69/6.65 % 23.69/6.65 No countermodel exists, formula is valid % 23.69/6.65 % SZS status Theorem for theBenchmark % 23.69/6.65 % 23.69/6.65 Generating proof ... Warning: ignoring some quantifiers % 25.23/6.99 found it (size 130) % 25.23/6.99 % 25.23/6.99 % SZS output start Proof for theBenchmark % 25.23/6.99 Assumed formulas after preprocessing and simplification: % 25.23/6.99 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v13 = 0) & p(v4) = v10 & n(v4) = v5 & n(v1) = v4 & n(v0) = v6 & n(e) = v0 & a(v10, v7) = v11 & a(v5, v7) = v8 & u(v3, v8) = v9 & u(v1, v11) = v12 & s(v6) = v7 & s(v2) = v3 & s(v1) = v2 & s(v0) = v1 & subq(v9, v12) = v13 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (m(v15, v16) = v17) | ~ (mem(v14, v17) = v18) | ? [v19] : ((v19 = 0 & mem(v14, v16) = 0) | ( ~ (v19 = 0) & mem(v14, v15) = v19))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (u(v15, v16) = v17) | ~ (mem(v14, v17) = v18) | ? [v19] : ? [v20] : ( ~ (v20 = 0) & ~ (v19 = 0) & mem(v14, v16) = v20 & mem(v14, v15) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast16p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast15p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast15p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast14p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast14p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast13p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast13p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast12p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast12p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast11p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast11p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast10p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast10p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast9p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast9p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast8p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast8p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast7p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast7p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast6p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast6p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast5p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast5p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast4p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast4p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast3p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | v15 = 0 | ~ (atleast3p(v14) = v15) | ~ (subq(v14, v16) = v17) | ? [v18] : (( ~ (v18 = 0) & atleast2p(v16) = v18) | ( ~ (v18 = 0) & subq(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (p(v15) = v16) | ~ (mem(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & subq(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (subq(v14, v15) = 0) | ~ (mem(v16, v15) = v17) | ? [v18] : ( ~ (v18 = 0) & mem(v16, v14) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (a(v17, v16) = v15) | ~ (a(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (m(v17, v16) = v15) | ~ (m(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (u(v17, v16) = v15) | ~ (u(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (disj(v17, v16) = v15) | ~ (disj(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (subq(v17, v16) = v15) | ~ (subq(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (mem(v17, v16) = v15) | ~ (mem(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = 0 | ~ (atleast2p(v14) = v15) | ~ (p(v16) = v17) | ? [v18] : ((v18 = 0 & subq(v14, v17) = 0) | ( ~ (v18 = 0) & mem(v16, v14) = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (m(v15, v16) = v17) | ~ (mem(v14, v17) = 0) | ? [v18] : ( ~ (v18 = 0) & mem(v14, v16) = v18 & mem(v14, v15) = 0)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (u(v15, v16) = v17) | ~ (mem(v14, v17) = 0) | ? [v18] : ((v18 = 0 & mem(v14, v16) = 0) | (v18 = 0 & mem(v14, v15) = 0))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (u(v14, v16) = v17) | ~ (s(v15) = v16) | a(v14, v15) = v17) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (s(v14) = v15) | ~ (mem(v14, v15) = v16)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (disj(v14, v15) = v16) | ? [v17] : (mem(v17, v15) = 0 & mem(v17, v14) = 0)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (subq(v14, v15) = v16) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & p(v15) = v17 & mem(v14, v17) = v18)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (subq(v14, v15) = v16) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & mem(v17, v15) = v18 & mem(v17, v14) = 0)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast16p(v16) = v15) | ~ (atleast16p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast15p(v16) = v15) | ~ (atleast15p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast14p(v16) = v15) | ~ (atleast14p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast13p(v16) = v15) | ~ (atleast13p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast12p(v16) = v15) | ~ (atleast12p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast11p(v16) = v15) | ~ (atleast11p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast10p(v16) = v15) | ~ (atleast10p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast9p(v16) = v15) | ~ (atleast9p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast8p(v16) = v15) | ~ (atleast8p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast7p(v16) = v15) | ~ (atleast7p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast6p(v16) = v15) | ~ (atleast6p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast5p(v16) = v15) | ~ (atleast5p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast4p(v16) = v15) | ~ (atleast4p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast3p(v16) = v15) | ~ (atleast3p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (atleast2p(v16) = v15) | ~ (atleast2p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (p(v16) = v15) | ~ (p(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (n(v16) = v15) | ~ (n(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (s(v16) = v15) | ~ (s(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (s(v15) = v16) | ~ (mem(v14, v16) = 0)) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast16p(v14) = v15) | ~ (atleast15p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast16p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast15p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast15p(v14) = v15) | ~ (atleast14p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast15p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast14p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast14p(v14) = v15) | ~ (atleast13p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast14p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast13p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast13p(v14) = v15) | ~ (atleast12p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast13p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast12p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast12p(v14) = v15) | ~ (atleast11p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast12p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast11p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast11p(v14) = v15) | ~ (atleast10p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast11p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast10p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast10p(v14) = v15) | ~ (atleast9p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast10p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast9p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast9p(v14) = v15) | ~ (atleast8p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast9p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast8p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast8p(v14) = v15) | ~ (atleast7p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast8p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast7p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast7p(v14) = v15) | ~ (atleast6p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast7p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast6p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast6p(v14) = v15) | ~ (atleast5p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast6p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast5p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast5p(v14) = v15) | ~ (atleast4p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast5p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast4p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast4p(v14) = v15) | ~ (atleast3p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast4p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast3p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast3p(v14) = v15) | ~ (atleast2p(v16) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & subq(v16, v14) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast3p(v14) = v15) | ~ (subq(v16, v14) = 0) | ? [v17] : ((v17 = 0 & subq(v14, v16) = 0) | ( ~ (v17 = 0) & atleast2p(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = 0 | ~ (atleast2p(v14) = v15) | ~ (mem(v16, v14) = 0) | ? [v17] : (p(v16) = v17 & subq(v14, v17) = 0)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (p(v15) = v16) | ~ (mem(v14, v16) = 0) | subq(v14, v15) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (a(v14, v15) = v16) | ? [v17] : (u(v14, v17) = v16 & s(v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (disj(v14, v15) = 0) | ~ (mem(v16, v15) = 0) | ? [v17] : ( ~ (v17 = 0) & mem(v16, v14) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (disj(v14, v15) = 0) | ~ (mem(v16, v14) = 0) | ? [v17] : ( ~ (v17 = 0) & mem(v16, v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (subq(v14, v15) = 0) | ~ (mem(v16, v14) = 0) | mem(v16, v15) = 0) & ! [v14] : ! [v15] : (v15 = v14 | ~ (subq(v15, v14) = 0) | ? [v16] : ( ~ (v16 = 0) & subq(v14, v15) = v16)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (subq(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & subq(v15, v14) = v16)) & ! [v14] : ! [v15] : ( ~ (n(v14) = v15) | a(v14, v14) = v15) & ! [v14] : ! [v15] : ( ~ (a(v14, v14) = v15) | n(v14) = v15) & ! [v14] : ! [v15] : ( ~ (subq(v14, v15) = 0) | ? [v16] : (p(v15) = v16 & mem(v14, v16) = 0)) & ! [v14] : ( ~ (atleast16p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast15p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast15p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast14p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast14p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast13p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast13p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast12p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast12p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast11p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast11p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast10p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast10p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast9p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast9p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast8p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast8p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast7p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast7p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast6p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast6p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast5p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast5p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast4p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast4p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast3p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast3p(v14) = 0) | ? [v15] : ? [v16] : ( ~ (v16 = 0) & atleast2p(v15) = 0 & subq(v15, v14) = 0 & subq(v14, v15) = v16)) & ! [v14] : ( ~ (atleast2p(v14) = 0) | ? [v15] : ? [v16] : ? [v17] : ( ~ (v17 = 0) & p(v15) = v16 & subq(v14, v16) = v17 & mem(v15, v14) = 0)) & ! [v14] : ~ (mem(v14, e) = 0) & ? [v14] : ? [v15] : ? [v16] : a(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : m(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : u(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : disj(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : subq(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : mem(v15, v14) = v16 & ? [v14] : ? [v15] : atleast16p(v14) = v15 & ? [v14] : ? [v15] : atleast15p(v14) = v15 & ? [v14] : ? [v15] : atleast14p(v14) = v15 & ? [v14] : ? [v15] : atleast13p(v14) = v15 & ? [v14] : ? [v15] : atleast12p(v14) = v15 & ? [v14] : ? [v15] : atleast11p(v14) = v15 & ? [v14] : ? [v15] : atleast10p(v14) = v15 & ? [v14] : ? [v15] : atleast9p(v14) = v15 & ? [v14] : ? [v15] : atleast8p(v14) = v15 & ? [v14] : ? [v15] : atleast7p(v14) = v15 & ? [v14] : ? [v15] : atleast6p(v14) = v15 & ? [v14] : ? [v15] : atleast5p(v14) = v15 & ? [v14] : ? [v15] : atleast4p(v14) = v15 & ? [v14] : ? [v15] : atleast3p(v14) = v15 & ? [v14] : ? [v15] : atleast2p(v14) = v15 & ? [v14] : ? [v15] : p(v14) = v15 & ? [v14] : ? [v15] : n(v14) = v15 & ? [v14] : ? [v15] : s(v14) = v15) % 25.55/7.03 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 25.55/7.03 | (1) ~ (all_0_0_0 = 0) & p(all_0_9_9) = all_0_3_3 & n(all_0_9_9) = all_0_8_8 & n(all_0_12_12) = all_0_9_9 & n(all_0_13_13) = all_0_7_7 & n(e) = all_0_13_13 & a(all_0_3_3, all_0_6_6) = all_0_2_2 & a(all_0_8_8, all_0_6_6) = all_0_5_5 & u(all_0_10_10, all_0_5_5) = all_0_4_4 & u(all_0_12_12, all_0_2_2) = all_0_1_1 & s(all_0_7_7) = all_0_6_6 & s(all_0_11_11) = all_0_10_10 & s(all_0_12_12) = all_0_11_11 & s(all_0_13_13) = all_0_12_12 & subq(all_0_4_4, all_0_1_1) = all_0_0_0 & ! [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.55/7.06 | % 25.55/7.06 | Applying alpha-rule on (1) yields: % 25.55/7.06 | (2) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.06 | (3) ! [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.55/7.06 | (4) s(all_0_12_12) = all_0_11_11 % 25.55/7.06 | (5) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 25.55/7.06 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 25.55/7.06 | (7) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 25.55/7.06 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 25.55/7.06 | (9) ! [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.55/7.06 | (10) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 25.55/7.06 | (11) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 25.55/7.06 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 25.55/7.06 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 25.55/7.06 | (14) ! [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.55/7.06 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 25.55/7.06 | (16) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 25.55/7.06 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 25.55/7.06 | (18) ! [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.55/7.06 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 25.55/7.06 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 25.55/7.06 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 25.55/7.06 | (22) subq(all_0_4_4, all_0_1_1) = all_0_0_0 % 25.55/7.06 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 25.55/7.06 | (24) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 25.55/7.06 | (25) ! [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.55/7.06 | (26) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 25.55/7.06 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 25.55/7.06 | (28) n(e) = all_0_13_13 % 25.55/7.06 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 25.55/7.06 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 25.55/7.06 | (31) ! [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.55/7.06 | (32) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 25.55/7.06 | (33) ! [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.55/7.06 | (34) s(all_0_13_13) = all_0_12_12 % 25.55/7.06 | (35) ! [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.55/7.06 | (36) ! [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.55/7.06 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 25.55/7.06 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 25.55/7.06 | (39) ! [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.55/7.06 | (40) ? [v0] : ? [v1] : p(v0) = v1 % 25.55/7.06 | (41) ! [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.55/7.06 | (42) ! [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.55/7.06 | (43) a(all_0_8_8, all_0_6_6) = all_0_5_5 % 25.55/7.06 | (44) ! [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.55/7.06 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 25.55/7.06 | (46) p(all_0_9_9) = all_0_3_3 % 25.55/7.06 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 25.55/7.06 | (48) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.06 | (49) ! [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.55/7.07 | (50) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 25.55/7.07 | (51) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 25.55/7.07 | (53) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 25.55/7.07 | (54) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 25.55/7.07 | (55) ! [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.55/7.07 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 25.55/7.07 | (57) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 25.55/7.07 | (58) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 25.55/7.07 | (59) ! [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.55/7.07 | (60) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (61) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 25.55/7.07 | (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.55/7.07 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 25.55/7.07 | (64) ! [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.55/7.07 | (65) ! [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.55/7.07 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 25.55/7.07 | (67) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (68) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (69) n(all_0_13_13) = all_0_7_7 % 25.55/7.07 | (70) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 25.55/7.07 | (71) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 25.55/7.07 | (72) ! [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.55/7.07 | (73) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 25.55/7.07 | (74) ! [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.55/7.07 | (75) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 25.55/7.07 | (76) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 25.55/7.07 | (77) ~ (all_0_0_0 = 0) % 25.55/7.07 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 25.55/7.07 | (79) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 25.55/7.07 | (80) ! [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.55/7.07 | (81) ! [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.55/7.07 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 25.55/7.07 | (83) ! [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.55/7.07 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 25.55/7.07 | (85) ! [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.55/7.07 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 25.55/7.07 | (87) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (88) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 25.55/7.07 | (89) ! [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.55/7.07 | (90) ! [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.55/7.07 | (91) a(all_0_3_3, all_0_6_6) = all_0_2_2 % 25.55/7.07 | (92) ! [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.55/7.07 | (93) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 25.55/7.07 | (94) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 25.55/7.07 | (95) ! [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.55/7.07 | (96) ! [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.55/7.07 | (97) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (98) ! [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.55/7.07 | (99) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (100) s(all_0_11_11) = all_0_10_10 % 25.55/7.07 | (101) ! [v0] : ~ (mem(v0, e) = 0) % 25.55/7.07 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 25.55/7.07 | (103) ! [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.55/7.07 | (104) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 25.55/7.07 | (105) ! [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.55/7.07 | (106) ? [v0] : ? [v1] : s(v0) = v1 % 25.55/7.07 | (107) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 25.55/7.07 | (108) ! [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.55/7.07 | (109) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 25.55/7.07 | (110) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 25.55/7.07 | (111) u(all_0_12_12, all_0_2_2) = all_0_1_1 % 25.55/7.07 | (112) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 25.55/7.07 | (113) ! [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.55/7.07 | (114) n(all_0_12_12) = all_0_9_9 % 25.55/7.07 | (115) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.07 | (116) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 25.55/7.07 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 25.55/7.07 | (118) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 25.55/7.07 | (119) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 25.55/7.07 | (120) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.08 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 25.55/7.08 | (122) ! [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.55/7.08 | (123) ? [v0] : ? [v1] : n(v0) = v1 % 25.55/7.08 | (124) ! [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.55/7.08 | (125) ! [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.55/7.08 | (126) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 25.55/7.08 | (127) ! [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.55/7.08 | (128) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 25.55/7.08 | (129) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 25.55/7.08 | (130) ! [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.55/7.08 | (131) s(all_0_7_7) = all_0_6_6 % 25.55/7.08 | (132) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.08 | (133) n(all_0_9_9) = all_0_8_8 % 25.55/7.08 | (134) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 25.55/7.08 | (135) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.08 | (136) u(all_0_10_10, all_0_5_5) = all_0_4_4 % 25.55/7.08 | (137) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 25.55/7.08 | (138) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 25.55/7.08 | (139) ! [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.55/7.08 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 25.55/7.08 | (141) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 25.55/7.08 | (142) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 25.55/7.08 | (143) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 25.55/7.08 | (144) ! [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.55/7.08 | (145) ! [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.55/7.08 | (146) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (11) with all_0_8_8, all_0_9_9 and discharging atoms n(all_0_9_9) = all_0_8_8, yields: % 25.55/7.08 | (147) a(all_0_9_9, all_0_9_9) = all_0_8_8 % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (11) with all_0_9_9, all_0_12_12 and discharging atoms n(all_0_12_12) = all_0_9_9, yields: % 25.55/7.08 | (148) a(all_0_12_12, all_0_12_12) = all_0_9_9 % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (15) with all_0_2_2, all_0_6_6, all_0_3_3 and discharging atoms a(all_0_3_3, all_0_6_6) = all_0_2_2, yields: % 25.55/7.08 | (149) ? [v0] : (u(all_0_3_3, v0) = all_0_2_2 & s(all_0_6_6) = v0) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (15) with all_0_5_5, all_0_6_6, all_0_8_8 and discharging atoms a(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 25.55/7.08 | (150) ? [v0] : (u(all_0_8_8, v0) = all_0_5_5 & s(all_0_6_6) = v0) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (129) with all_0_0_0, all_0_1_1, all_0_4_4 and discharging atoms subq(all_0_4_4, all_0_1_1) = all_0_0_0, yields: % 25.55/7.08 | (151) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_4_4, v0) = v1) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (61) with all_0_0_0, all_0_1_1, all_0_4_4 and discharging atoms subq(all_0_4_4, all_0_1_1) = all_0_0_0, yields: % 25.55/7.08 | (152) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_4_4) = 0) % 25.55/7.08 | % 25.55/7.08 | Instantiating (150) with all_57_0_68 yields: % 25.55/7.08 | (153) u(all_0_8_8, all_57_0_68) = all_0_5_5 & s(all_0_6_6) = all_57_0_68 % 25.55/7.08 | % 25.55/7.08 | Applying alpha-rule on (153) yields: % 25.55/7.08 | (154) u(all_0_8_8, all_57_0_68) = all_0_5_5 % 25.55/7.08 | (155) s(all_0_6_6) = all_57_0_68 % 25.55/7.08 | % 25.55/7.08 | Instantiating (149) with all_59_0_69 yields: % 25.55/7.08 | (156) u(all_0_3_3, all_59_0_69) = all_0_2_2 & s(all_0_6_6) = all_59_0_69 % 25.55/7.08 | % 25.55/7.08 | Applying alpha-rule on (156) yields: % 25.55/7.08 | (157) u(all_0_3_3, all_59_0_69) = all_0_2_2 % 25.55/7.08 | (158) s(all_0_6_6) = all_59_0_69 % 25.55/7.08 | % 25.55/7.08 +-Applying beta-rule and splitting (151), into two cases. % 25.55/7.08 |-Branch one: % 25.55/7.08 | (159) all_0_0_0 = 0 % 25.55/7.08 | % 25.55/7.08 | Equations (159) can reduce 77 to: % 25.55/7.08 | (160) $false % 25.55/7.08 | % 25.55/7.08 |-The branch is then unsatisfiable % 25.55/7.08 |-Branch two: % 25.55/7.08 | (77) ~ (all_0_0_0 = 0) % 25.55/7.08 | (162) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_4_4, v0) = v1) % 25.55/7.08 | % 25.55/7.08 +-Applying beta-rule and splitting (152), into two cases. % 25.55/7.08 |-Branch one: % 25.55/7.08 | (159) all_0_0_0 = 0 % 25.55/7.08 | % 25.55/7.08 | Equations (159) can reduce 77 to: % 25.55/7.08 | (160) $false % 25.55/7.08 | % 25.55/7.08 |-The branch is then unsatisfiable % 25.55/7.08 |-Branch two: % 25.55/7.08 | (77) ~ (all_0_0_0 = 0) % 25.55/7.08 | (166) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_4_4) = 0) % 25.55/7.08 | % 25.55/7.08 | Instantiating (166) with all_70_0_72, all_70_1_73 yields: % 25.55/7.08 | (167) ~ (all_70_0_72 = 0) & mem(all_70_1_73, all_0_1_1) = all_70_0_72 & mem(all_70_1_73, all_0_4_4) = 0 % 25.55/7.08 | % 25.55/7.08 | Applying alpha-rule on (167) yields: % 25.55/7.08 | (168) ~ (all_70_0_72 = 0) % 25.55/7.08 | (169) mem(all_70_1_73, all_0_1_1) = all_70_0_72 % 25.55/7.08 | (170) mem(all_70_1_73, all_0_4_4) = 0 % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (79) with all_0_6_6, all_57_0_68, all_59_0_69 and discharging atoms s(all_0_6_6) = all_59_0_69, s(all_0_6_6) = all_57_0_68, yields: % 25.55/7.08 | (171) all_59_0_69 = all_57_0_68 % 25.55/7.08 | % 25.55/7.08 | From (171) and (157) follows: % 25.55/7.08 | (172) u(all_0_3_3, all_57_0_68) = all_0_2_2 % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (15) with all_0_8_8, all_0_9_9, all_0_9_9 and discharging atoms a(all_0_9_9, all_0_9_9) = all_0_8_8, yields: % 25.55/7.08 | (173) ? [v0] : (u(all_0_9_9, v0) = all_0_8_8 & s(all_0_9_9) = v0) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (15) with all_0_9_9, all_0_12_12, all_0_12_12 and discharging atoms a(all_0_12_12, all_0_12_12) = all_0_9_9, yields: % 25.55/7.08 | (174) ? [v0] : (u(all_0_12_12, v0) = all_0_9_9 & s(all_0_12_12) = v0) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (89) with all_70_0_72, all_0_1_1, all_0_2_2, all_0_12_12, all_70_1_73 and discharging atoms u(all_0_12_12, all_0_2_2) = all_0_1_1, mem(all_70_1_73, all_0_1_1) = all_70_0_72, yields: % 25.55/7.08 | (175) all_70_0_72 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_70_1_73, all_0_2_2) = v1 & mem(all_70_1_73, all_0_12_12) = v0) % 25.55/7.08 | % 25.55/7.08 | Instantiating formula (145) with all_0_4_4, all_0_5_5, all_0_10_10, all_70_1_73 and discharging atoms u(all_0_10_10, all_0_5_5) = all_0_4_4, mem(all_70_1_73, all_0_4_4) = 0, yields: % 25.55/7.08 | (176) ? [v0] : ((v0 = 0 & mem(all_70_1_73, all_0_5_5) = 0) | (v0 = 0 & mem(all_70_1_73, all_0_10_10) = 0)) % 25.55/7.08 | % 25.55/7.08 | Instantiating (176) with all_81_0_74 yields: % 25.55/7.08 | (177) (all_81_0_74 = 0 & mem(all_70_1_73, all_0_5_5) = 0) | (all_81_0_74 = 0 & mem(all_70_1_73, all_0_10_10) = 0) % 25.55/7.08 | % 25.55/7.08 | Instantiating (174) with all_84_0_76 yields: % 25.55/7.08 | (178) u(all_0_12_12, all_84_0_76) = all_0_9_9 & s(all_0_12_12) = all_84_0_76 % 25.55/7.08 | % 25.55/7.08 | Applying alpha-rule on (178) yields: % 25.55/7.08 | (179) u(all_0_12_12, all_84_0_76) = all_0_9_9 % 25.55/7.08 | (180) s(all_0_12_12) = all_84_0_76 % 25.55/7.09 | % 25.55/7.09 | Instantiating (173) with all_86_0_77 yields: % 25.55/7.09 | (181) u(all_0_9_9, all_86_0_77) = all_0_8_8 & s(all_0_9_9) = all_86_0_77 % 25.55/7.09 | % 25.55/7.09 | Applying alpha-rule on (181) yields: % 25.55/7.09 | (182) u(all_0_9_9, all_86_0_77) = all_0_8_8 % 25.55/7.09 | (183) s(all_0_9_9) = all_86_0_77 % 25.55/7.09 | % 25.55/7.09 +-Applying beta-rule and splitting (175), into two cases. % 25.55/7.09 |-Branch one: % 25.55/7.09 | (184) all_70_0_72 = 0 % 25.55/7.09 | % 25.55/7.09 | Equations (184) can reduce 168 to: % 25.55/7.09 | (160) $false % 25.55/7.09 | % 25.55/7.09 |-The branch is then unsatisfiable % 25.55/7.09 |-Branch two: % 25.55/7.09 | (168) ~ (all_70_0_72 = 0) % 25.55/7.09 | (187) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_70_1_73, all_0_2_2) = v1 & mem(all_70_1_73, all_0_12_12) = v0) % 25.55/7.09 | % 25.55/7.09 | Instantiating (187) with all_94_0_79, all_94_1_80 yields: % 25.55/7.09 | (188) ~ (all_94_0_79 = 0) & ~ (all_94_1_80 = 0) & mem(all_70_1_73, all_0_2_2) = all_94_0_79 & mem(all_70_1_73, all_0_12_12) = all_94_1_80 % 25.55/7.09 | % 25.55/7.09 | Applying alpha-rule on (188) yields: % 25.55/7.09 | (189) ~ (all_94_0_79 = 0) % 25.55/7.09 | (190) ~ (all_94_1_80 = 0) % 25.55/7.09 | (191) mem(all_70_1_73, all_0_2_2) = all_94_0_79 % 25.55/7.09 | (192) mem(all_70_1_73, all_0_12_12) = all_94_1_80 % 25.55/7.09 | % 25.55/7.09 | Instantiating formula (79) with all_0_12_12, all_84_0_76, all_0_11_11 and discharging atoms s(all_0_12_12) = all_84_0_76, s(all_0_12_12) = all_0_11_11, yields: % 25.55/7.09 | (193) all_84_0_76 = all_0_11_11 % 25.55/7.09 | % 25.55/7.09 | From (193) and (179) follows: % 25.55/7.09 | (194) u(all_0_12_12, all_0_11_11) = all_0_9_9 % 25.55/7.09 | % 25.55/7.09 | From (193) and (180) follows: % 25.55/7.09 | (4) s(all_0_12_12) = all_0_11_11 % 25.55/7.09 | % 25.55/7.09 | Instantiating formula (89) with all_94_0_79, all_0_2_2, all_57_0_68, all_0_3_3, all_70_1_73 and discharging atoms u(all_0_3_3, all_57_0_68) = all_0_2_2, mem(all_70_1_73, all_0_2_2) = all_94_0_79, yields: % 25.55/7.09 | (196) all_94_0_79 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_70_1_73, all_57_0_68) = v1 & mem(all_70_1_73, all_0_3_3) = v0) % 25.55/7.09 | % 25.55/7.09 +-Applying beta-rule and splitting (177), into two cases. % 25.55/7.09 |-Branch one: % 25.55/7.09 | (197) all_81_0_74 = 0 & mem(all_70_1_73, all_0_5_5) = 0 % 25.55/7.09 | % 25.55/7.09 | Applying alpha-rule on (197) yields: % 25.55/7.09 | (198) all_81_0_74 = 0 % 25.91/7.09 | (199) mem(all_70_1_73, all_0_5_5) = 0 % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (196), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (200) all_94_0_79 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (200) can reduce 189 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (189) ~ (all_94_0_79 = 0) % 25.91/7.09 | (203) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_70_1_73, all_57_0_68) = v1 & mem(all_70_1_73, all_0_3_3) = v0) % 25.91/7.09 | % 25.91/7.09 | Instantiating (203) with all_111_0_81, all_111_1_82 yields: % 25.91/7.09 | (204) ~ (all_111_0_81 = 0) & ~ (all_111_1_82 = 0) & mem(all_70_1_73, all_57_0_68) = all_111_0_81 & mem(all_70_1_73, all_0_3_3) = all_111_1_82 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (204) yields: % 25.91/7.09 | (205) ~ (all_111_0_81 = 0) % 25.91/7.09 | (206) ~ (all_111_1_82 = 0) % 25.91/7.09 | (207) mem(all_70_1_73, all_57_0_68) = all_111_0_81 % 25.91/7.09 | (208) mem(all_70_1_73, all_0_3_3) = all_111_1_82 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (86) with all_111_1_82, all_0_3_3, all_0_9_9, all_70_1_73 and discharging atoms p(all_0_9_9) = all_0_3_3, mem(all_70_1_73, all_0_3_3) = all_111_1_82, yields: % 25.91/7.09 | (209) all_111_1_82 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_70_1_73, all_0_9_9) = v0) % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (145) with all_0_5_5, all_57_0_68, all_0_8_8, all_70_1_73 and discharging atoms u(all_0_8_8, all_57_0_68) = all_0_5_5, mem(all_70_1_73, all_0_5_5) = 0, yields: % 25.91/7.09 | (210) ? [v0] : ((v0 = 0 & mem(all_70_1_73, all_57_0_68) = 0) | (v0 = 0 & mem(all_70_1_73, all_0_8_8) = 0)) % 25.91/7.09 | % 25.91/7.09 | Instantiating (210) with all_118_0_83 yields: % 25.91/7.09 | (211) (all_118_0_83 = 0 & mem(all_70_1_73, all_57_0_68) = 0) | (all_118_0_83 = 0 & mem(all_70_1_73, all_0_8_8) = 0) % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (209), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (212) all_111_1_82 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (212) can reduce 206 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (206) ~ (all_111_1_82 = 0) % 25.91/7.09 | (215) ? [v0] : ( ~ (v0 = 0) & subq(all_70_1_73, all_0_9_9) = v0) % 25.91/7.09 | % 25.91/7.09 | Instantiating (215) with all_121_0_84 yields: % 25.91/7.09 | (216) ~ (all_121_0_84 = 0) & subq(all_70_1_73, all_0_9_9) = all_121_0_84 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (216) yields: % 25.91/7.09 | (217) ~ (all_121_0_84 = 0) % 25.91/7.09 | (218) subq(all_70_1_73, all_0_9_9) = all_121_0_84 % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (211), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (219) all_118_0_83 = 0 & mem(all_70_1_73, all_57_0_68) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (219) yields: % 25.91/7.09 | (220) all_118_0_83 = 0 % 25.91/7.09 | (221) mem(all_70_1_73, all_57_0_68) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (6) with all_70_1_73, all_57_0_68, 0, all_111_0_81 and discharging atoms mem(all_70_1_73, all_57_0_68) = all_111_0_81, mem(all_70_1_73, all_57_0_68) = 0, yields: % 25.91/7.09 | (222) all_111_0_81 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (222) can reduce 205 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (224) all_118_0_83 = 0 & mem(all_70_1_73, all_0_8_8) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (224) yields: % 25.91/7.09 | (220) all_118_0_83 = 0 % 25.91/7.09 | (226) mem(all_70_1_73, all_0_8_8) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (61) with all_121_0_84, all_0_9_9, all_70_1_73 and discharging atoms subq(all_70_1_73, all_0_9_9) = all_121_0_84, yields: % 25.91/7.09 | (227) all_121_0_84 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_70_1_73) = 0 & mem(v0, all_0_9_9) = v1) % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (145) with all_0_8_8, all_86_0_77, all_0_9_9, all_70_1_73 and discharging atoms u(all_0_9_9, all_86_0_77) = all_0_8_8, mem(all_70_1_73, all_0_8_8) = 0, yields: % 25.91/7.09 | (228) ? [v0] : ((v0 = 0 & mem(all_70_1_73, all_86_0_77) = 0) | (v0 = 0 & mem(all_70_1_73, all_0_9_9) = 0)) % 25.91/7.09 | % 25.91/7.09 | Instantiating (228) with all_132_0_85 yields: % 25.91/7.09 | (229) (all_132_0_85 = 0 & mem(all_70_1_73, all_86_0_77) = 0) | (all_132_0_85 = 0 & mem(all_70_1_73, all_0_9_9) = 0) % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (227), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (230) all_121_0_84 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (230) can reduce 217 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (217) ~ (all_121_0_84 = 0) % 25.91/7.09 | (233) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_70_1_73) = 0 & mem(v0, all_0_9_9) = v1) % 25.91/7.09 | % 25.91/7.09 | Instantiating (233) with all_135_0_86, all_135_1_87 yields: % 25.91/7.09 | (234) ~ (all_135_0_86 = 0) & mem(all_135_1_87, all_70_1_73) = 0 & mem(all_135_1_87, all_0_9_9) = all_135_0_86 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (234) yields: % 25.91/7.09 | (235) ~ (all_135_0_86 = 0) % 25.91/7.09 | (236) mem(all_135_1_87, all_70_1_73) = 0 % 25.91/7.09 | (237) mem(all_135_1_87, all_0_9_9) = all_135_0_86 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (89) with all_135_0_86, all_0_9_9, all_0_11_11, all_0_12_12, all_135_1_87 and discharging atoms u(all_0_12_12, all_0_11_11) = all_0_9_9, mem(all_135_1_87, all_0_9_9) = all_135_0_86, yields: % 25.91/7.09 | (238) all_135_0_86 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_135_1_87, all_0_11_11) = v1 & mem(all_135_1_87, all_0_12_12) = v0) % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (229), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (239) all_132_0_85 = 0 & mem(all_70_1_73, all_86_0_77) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (239) yields: % 25.91/7.09 | (240) all_132_0_85 = 0 % 25.91/7.09 | (241) mem(all_70_1_73, all_86_0_77) = 0 % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (238), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (242) all_135_0_86 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (242) can reduce 235 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (235) ~ (all_135_0_86 = 0) % 25.91/7.09 | (245) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_135_1_87, all_0_11_11) = v1 & mem(all_135_1_87, all_0_12_12) = v0) % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (140) with all_86_0_77, all_0_9_9, all_70_1_73 and discharging atoms s(all_0_9_9) = all_86_0_77, mem(all_70_1_73, all_86_0_77) = 0, yields: % 25.91/7.09 | (246) all_70_1_73 = all_0_9_9 % 25.91/7.09 | % 25.91/7.09 | From (246) and (236) follows: % 25.91/7.09 | (247) mem(all_135_1_87, all_0_9_9) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (6) with all_135_1_87, all_0_9_9, 0, all_135_0_86 and discharging atoms mem(all_135_1_87, all_0_9_9) = all_135_0_86, mem(all_135_1_87, all_0_9_9) = 0, yields: % 25.91/7.09 | (242) all_135_0_86 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (242) can reduce 235 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (250) all_132_0_85 = 0 & mem(all_70_1_73, all_0_9_9) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (250) yields: % 25.91/7.09 | (240) all_132_0_85 = 0 % 25.91/7.09 | (252) mem(all_70_1_73, all_0_9_9) = 0 % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (238), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (242) all_135_0_86 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (242) can reduce 235 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (235) ~ (all_135_0_86 = 0) % 25.91/7.09 | (245) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_135_1_87, all_0_11_11) = v1 & mem(all_135_1_87, all_0_12_12) = v0) % 25.91/7.09 | % 25.91/7.09 | Instantiating (245) with all_148_0_90, all_148_1_91 yields: % 25.91/7.09 | (257) ~ (all_148_0_90 = 0) & ~ (all_148_1_91 = 0) & mem(all_135_1_87, all_0_11_11) = all_148_0_90 & mem(all_135_1_87, all_0_12_12) = all_148_1_91 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (257) yields: % 25.91/7.09 | (258) ~ (all_148_0_90 = 0) % 25.91/7.09 | (259) ~ (all_148_1_91 = 0) % 25.91/7.09 | (260) mem(all_135_1_87, all_0_11_11) = all_148_0_90 % 25.91/7.09 | (261) mem(all_135_1_87, all_0_12_12) = all_148_1_91 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (145) with all_0_9_9, all_0_11_11, all_0_12_12, all_70_1_73 and discharging atoms u(all_0_12_12, all_0_11_11) = all_0_9_9, mem(all_70_1_73, all_0_9_9) = 0, yields: % 25.91/7.09 | (262) ? [v0] : ((v0 = 0 & mem(all_70_1_73, all_0_11_11) = 0) | (v0 = 0 & mem(all_70_1_73, all_0_12_12) = 0)) % 25.91/7.09 | % 25.91/7.09 | Instantiating (262) with all_155_0_92 yields: % 25.91/7.09 | (263) (all_155_0_92 = 0 & mem(all_70_1_73, all_0_11_11) = 0) | (all_155_0_92 = 0 & mem(all_70_1_73, all_0_12_12) = 0) % 25.91/7.09 | % 25.91/7.09 +-Applying beta-rule and splitting (263), into two cases. % 25.91/7.09 |-Branch one: % 25.91/7.09 | (264) all_155_0_92 = 0 & mem(all_70_1_73, all_0_11_11) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (264) yields: % 25.91/7.09 | (265) all_155_0_92 = 0 % 25.91/7.09 | (266) mem(all_70_1_73, all_0_11_11) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (140) with all_0_11_11, all_0_12_12, all_70_1_73 and discharging atoms s(all_0_12_12) = all_0_11_11, mem(all_70_1_73, all_0_11_11) = 0, yields: % 25.91/7.09 | (267) all_70_1_73 = all_0_12_12 % 25.91/7.09 | % 25.91/7.09 | From (267) and (236) follows: % 25.91/7.09 | (268) mem(all_135_1_87, all_0_12_12) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (6) with all_135_1_87, all_0_12_12, 0, all_148_1_91 and discharging atoms mem(all_135_1_87, all_0_12_12) = all_148_1_91, mem(all_135_1_87, all_0_12_12) = 0, yields: % 25.91/7.09 | (269) all_148_1_91 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (269) can reduce 259 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.09 |-Branch two: % 25.91/7.09 | (271) all_155_0_92 = 0 & mem(all_70_1_73, all_0_12_12) = 0 % 25.91/7.09 | % 25.91/7.09 | Applying alpha-rule on (271) yields: % 25.91/7.09 | (265) all_155_0_92 = 0 % 25.91/7.09 | (273) mem(all_70_1_73, all_0_12_12) = 0 % 25.91/7.09 | % 25.91/7.09 | Instantiating formula (6) with all_70_1_73, all_0_12_12, 0, all_94_1_80 and discharging atoms mem(all_70_1_73, all_0_12_12) = all_94_1_80, mem(all_70_1_73, all_0_12_12) = 0, yields: % 25.91/7.09 | (274) all_94_1_80 = 0 % 25.91/7.09 | % 25.91/7.09 | Equations (274) can reduce 190 to: % 25.91/7.09 | (160) $false % 25.91/7.09 | % 25.91/7.09 |-The branch is then unsatisfiable % 25.91/7.10 |-Branch two: % 25.91/7.10 | (276) all_81_0_74 = 0 & mem(all_70_1_73, all_0_10_10) = 0 % 25.91/7.10 | % 25.91/7.10 | Applying alpha-rule on (276) yields: % 25.91/7.10 | (198) all_81_0_74 = 0 % 25.91/7.10 | (278) mem(all_70_1_73, all_0_10_10) = 0 % 25.91/7.10 | % 25.91/7.10 +-Applying beta-rule and splitting (196), into two cases. % 25.91/7.10 |-Branch one: % 25.91/7.10 | (200) all_94_0_79 = 0 % 25.91/7.10 | % 25.91/7.10 | Equations (200) can reduce 189 to: % 25.91/7.10 | (160) $false % 25.91/7.10 | % 25.91/7.10 |-The branch is then unsatisfiable % 25.91/7.10 |-Branch two: % 25.91/7.10 | (189) ~ (all_94_0_79 = 0) % 25.91/7.10 | (203) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_70_1_73, all_57_0_68) = v1 & mem(all_70_1_73, all_0_3_3) = v0) % 25.91/7.10 | % 25.91/7.10 | Instantiating (203) with all_111_0_93, all_111_1_94 yields: % 25.91/7.10 | (283) ~ (all_111_0_93 = 0) & ~ (all_111_1_94 = 0) & mem(all_70_1_73, all_57_0_68) = all_111_0_93 & mem(all_70_1_73, all_0_3_3) = all_111_1_94 % 25.91/7.10 | % 25.91/7.10 | Applying alpha-rule on (283) yields: % 25.91/7.10 | (284) ~ (all_111_0_93 = 0) % 25.91/7.10 | (285) ~ (all_111_1_94 = 0) % 25.91/7.10 | (286) mem(all_70_1_73, all_57_0_68) = all_111_0_93 % 25.91/7.10 | (287) mem(all_70_1_73, all_0_3_3) = all_111_1_94 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (140) with all_0_10_10, all_0_11_11, all_70_1_73 and discharging atoms s(all_0_11_11) = all_0_10_10, mem(all_70_1_73, all_0_10_10) = 0, yields: % 25.91/7.10 | (288) all_70_1_73 = all_0_11_11 % 25.91/7.10 | % 25.91/7.10 | From (288) and (287) follows: % 25.91/7.10 | (289) mem(all_0_11_11, all_0_3_3) = all_111_1_94 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (86) with all_111_1_94, all_0_3_3, all_0_9_9, all_0_11_11 and discharging atoms p(all_0_9_9) = all_0_3_3, mem(all_0_11_11, all_0_3_3) = all_111_1_94, yields: % 25.91/7.10 | (290) all_111_1_94 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_0_11_11, all_0_9_9) = v0) % 25.91/7.10 | % 25.91/7.10 +-Applying beta-rule and splitting (290), into two cases. % 25.91/7.10 |-Branch one: % 25.91/7.10 | (291) all_111_1_94 = 0 % 25.91/7.10 | % 25.91/7.10 | Equations (291) can reduce 285 to: % 25.91/7.10 | (160) $false % 25.91/7.10 | % 25.91/7.10 |-The branch is then unsatisfiable % 25.91/7.10 |-Branch two: % 25.91/7.10 | (285) ~ (all_111_1_94 = 0) % 25.91/7.10 | (294) ? [v0] : ( ~ (v0 = 0) & subq(all_0_11_11, all_0_9_9) = v0) % 25.91/7.10 | % 25.91/7.10 | Instantiating (294) with all_124_0_95 yields: % 25.91/7.10 | (295) ~ (all_124_0_95 = 0) & subq(all_0_11_11, all_0_9_9) = all_124_0_95 % 25.91/7.10 | % 25.91/7.10 | Applying alpha-rule on (295) yields: % 25.91/7.10 | (296) ~ (all_124_0_95 = 0) % 25.91/7.10 | (297) subq(all_0_11_11, all_0_9_9) = all_124_0_95 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (61) with all_124_0_95, all_0_9_9, all_0_11_11 and discharging atoms subq(all_0_11_11, all_0_9_9) = all_124_0_95, yields: % 25.91/7.10 | (298) all_124_0_95 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_9_9) = v1 & mem(v0, all_0_11_11) = 0) % 25.91/7.10 | % 25.91/7.10 +-Applying beta-rule and splitting (298), into two cases. % 25.91/7.10 |-Branch one: % 25.91/7.10 | (299) all_124_0_95 = 0 % 25.91/7.10 | % 25.91/7.10 | Equations (299) can reduce 296 to: % 25.91/7.10 | (160) $false % 25.91/7.10 | % 25.91/7.10 |-The branch is then unsatisfiable % 25.91/7.10 |-Branch two: % 25.91/7.10 | (296) ~ (all_124_0_95 = 0) % 25.91/7.10 | (302) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_9_9) = v1 & mem(v0, all_0_11_11) = 0) % 25.91/7.10 | % 25.91/7.10 | Instantiating (302) with all_133_0_96, all_133_1_97 yields: % 25.91/7.10 | (303) ~ (all_133_0_96 = 0) & mem(all_133_1_97, all_0_9_9) = all_133_0_96 & mem(all_133_1_97, all_0_11_11) = 0 % 25.91/7.10 | % 25.91/7.10 | Applying alpha-rule on (303) yields: % 25.91/7.10 | (304) ~ (all_133_0_96 = 0) % 25.91/7.10 | (305) mem(all_133_1_97, all_0_9_9) = all_133_0_96 % 25.91/7.10 | (306) mem(all_133_1_97, all_0_11_11) = 0 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (140) with all_0_11_11, all_0_12_12, all_133_1_97 and discharging atoms s(all_0_12_12) = all_0_11_11, mem(all_133_1_97, all_0_11_11) = 0, yields: % 25.91/7.10 | (307) all_133_1_97 = all_0_12_12 % 25.91/7.10 | % 25.91/7.10 | From (307) and (305) follows: % 25.91/7.10 | (308) mem(all_0_12_12, all_0_9_9) = all_133_0_96 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (89) with all_133_0_96, all_0_9_9, all_0_11_11, all_0_12_12, all_0_12_12 and discharging atoms u(all_0_12_12, all_0_11_11) = all_0_9_9, mem(all_0_12_12, all_0_9_9) = all_133_0_96, yields: % 25.91/7.10 | (309) all_133_0_96 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_12_12, all_0_11_11) = v1 & mem(all_0_12_12, all_0_12_12) = v0) % 25.91/7.10 | % 25.91/7.10 +-Applying beta-rule and splitting (309), into two cases. % 25.91/7.10 |-Branch one: % 25.91/7.10 | (310) all_133_0_96 = 0 % 25.91/7.10 | % 25.91/7.10 | Equations (310) can reduce 304 to: % 25.91/7.10 | (160) $false % 25.91/7.10 | % 25.91/7.10 |-The branch is then unsatisfiable % 25.91/7.10 |-Branch two: % 25.91/7.10 | (304) ~ (all_133_0_96 = 0) % 25.91/7.10 | (313) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_12_12, all_0_11_11) = v1 & mem(all_0_12_12, all_0_12_12) = v0) % 25.91/7.10 | % 25.91/7.10 | Instantiating (313) with all_146_0_98, all_146_1_99 yields: % 25.91/7.10 | (314) ~ (all_146_0_98 = 0) & ~ (all_146_1_99 = 0) & mem(all_0_12_12, all_0_11_11) = all_146_0_98 & mem(all_0_12_12, all_0_12_12) = all_146_1_99 % 25.91/7.10 | % 25.91/7.10 | Applying alpha-rule on (314) yields: % 25.91/7.10 | (315) ~ (all_146_0_98 = 0) % 25.91/7.10 | (316) ~ (all_146_1_99 = 0) % 25.91/7.10 | (317) mem(all_0_12_12, all_0_11_11) = all_146_0_98 % 25.91/7.10 | (318) mem(all_0_12_12, all_0_12_12) = all_146_1_99 % 25.91/7.10 | % 25.91/7.10 | Instantiating formula (93) with all_146_0_98, all_0_11_11, all_0_12_12 and discharging atoms s(all_0_12_12) = all_0_11_11, mem(all_0_12_12, all_0_11_11) = all_146_0_98, yields: % 25.91/7.10 | (319) all_146_0_98 = 0 % 25.91/7.10 | % 25.91/7.10 | Equations (319) can reduce 315 to: % 25.91/7.10 | (160) $false % 25.91/7.10 | % 25.91/7.10 |-The branch is then unsatisfiable % 25.91/7.10 % SZS output end Proof for theBenchmark % 25.91/7.10 % 25.91/7.10 6504ms %------------------------------------------------------------------------------