%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV579+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n012.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 25.00s 7.05s % Output : Proof 27.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SEV579+1 : TPTP v9.1.0. Released v9.1.0. % 0.08/0.14 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.35 % Computer : n012.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Mar 31 13:07:49 EDT 2025 % 0.13/0.36 % CPUTime : % 0.58/0.60 ____ _ % 0.58/0.60 ___ / __ \_____(_)___ ________ __________ % 0.58/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.58/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.58/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.58/0.60 % 0.58/0.60 A Theorem Prover for First-Order Logic % 0.58/0.61 (ePrincess v.1.0) % 0.58/0.61 % 0.58/0.61 (c) Philipp Rümmer, 2009-2015 % 0.58/0.61 (c) Peter Backeman, 2014-2015 % 0.58/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.58/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.58/0.61 Bug reports to peter@backeman.se % 0.58/0.61 % 0.58/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.58/0.61 % 0.58/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.69/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.69/0.99 Prover 0: Preprocessing ... % 2.58/1.25 Prover 0: Warning: ignoring some quantifiers % 2.58/1.28 Prover 0: Constructing countermodel ... % 20.11/5.95 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.42/6.01 Prover 1: Preprocessing ... % 20.92/6.16 Prover 1: Constructing countermodel ... % 24.04/6.83 Prover 1: gave up % 24.04/6.83 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 24.04/6.85 Prover 2: Preprocessing ... % 24.59/6.95 Prover 2: Warning: ignoring some quantifiers % 24.59/6.96 Prover 2: Constructing countermodel ... % 25.00/7.05 Prover 2: proved (220ms) % 25.00/7.05 Prover 0: stopped % 25.00/7.05 % 25.00/7.05 No countermodel exists, formula is valid % 25.00/7.05 % SZS status Theorem for theBenchmark % 25.00/7.05 % 25.00/7.05 Generating proof ... Warning: ignoring some quantifiers % 26.75/7.43 found it (size 180) % 26.75/7.43 % 26.75/7.43 % SZS output start Proof for theBenchmark % 26.75/7.43 Assumed formulas after preprocessing and simplification: % 26.75/7.43 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ( ~ (v23 = 0) & p(v3) = v4 & p(v1) = v19 & n(v14) = v15 & n(v6) = v7 & n(v3) = v6 & n(v1) = v8 & n(v0) = v1 & n(e) = v0 & a(v18, v19) = v20 & a(v13, v1) = v14 & a(v11, v8) = v12 & a(v7, v8) = v9 & a(v3, v4) = v17 & a(v2, v4) = v5 & u(v17, v20) = v21 & u(v16, v21) = v22 & u(v12, v15) = v16 & u(v5, v9) = v10 & s(v6) = v18 & s(v3) = v13 & s(v2) = v11 & s(v1) = v2 & s(v0) = v3 & subq(v10, v22) = v23 & ! [v24] : ! [v25] : ! [v26] : ! [v27] : ! [v28] : (v28 = 0 | ~ (m(v25, v26) = v27) | ~ (mem(v24, v27) = v28) | ? [v29] : ((v29 = 0 & mem(v24, v26) = 0) | ( ~ (v29 = 0) & mem(v24, v25) = v29))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : ! [v28] : (v28 = 0 | ~ (u(v25, v26) = v27) | ~ (mem(v24, v27) = v28) | ? [v29] : ? [v30] : ( ~ (v30 = 0) & ~ (v29 = 0) & mem(v24, v26) = v30 & mem(v24, v25) = v29)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast16p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast15p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast15p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast14p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast14p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast13p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast13p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast12p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast12p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast11p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast11p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast10p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast10p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast9p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast9p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast8p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast8p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast7p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast7p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast6p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast6p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast5p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast5p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast4p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast4p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast3p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | v25 = 0 | ~ (atleast3p(v24) = v25) | ~ (subq(v24, v26) = v27) | ? [v28] : (( ~ (v28 = 0) & atleast2p(v26) = v28) | ( ~ (v28 = 0) & subq(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | ~ (p(v25) = v26) | ~ (mem(v24, v26) = v27) | ? [v28] : ( ~ (v28 = 0) & subq(v24, v25) = v28)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | ~ (subq(v24, v25) = 0) | ~ (mem(v26, v25) = v27) | ? [v28] : ( ~ (v28 = 0) & mem(v26, v24) = v28)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (a(v27, v26) = v25) | ~ (a(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (m(v27, v26) = v25) | ~ (m(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (u(v27, v26) = v25) | ~ (u(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (disj(v27, v26) = v25) | ~ (disj(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (subq(v27, v26) = v25) | ~ (subq(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (mem(v27, v26) = v25) | ~ (mem(v27, v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = 0 | ~ (atleast2p(v24) = v25) | ~ (p(v26) = v27) | ? [v28] : ((v28 = 0 & subq(v24, v27) = 0) | ( ~ (v28 = 0) & mem(v26, v24) = v28))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : ( ~ (m(v25, v26) = v27) | ~ (mem(v24, v27) = 0) | ? [v28] : ( ~ (v28 = 0) & mem(v24, v26) = v28 & mem(v24, v25) = 0)) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : ( ~ (u(v25, v26) = v27) | ~ (mem(v24, v27) = 0) | ? [v28] : ((v28 = 0 & mem(v24, v26) = 0) | (v28 = 0 & mem(v24, v25) = 0))) & ! [v24] : ! [v25] : ! [v26] : ! [v27] : ( ~ (u(v24, v26) = v27) | ~ (s(v25) = v26) | a(v24, v25) = v27) & ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (s(v24) = v25) | ~ (mem(v24, v25) = v26)) & ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (disj(v24, v25) = v26) | ? [v27] : (mem(v27, v25) = 0 & mem(v27, v24) = 0)) & ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (subq(v24, v25) = v26) | ? [v27] : ? [v28] : ( ~ (v28 = 0) & p(v25) = v27 & mem(v24, v27) = v28)) & ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (subq(v24, v25) = v26) | ? [v27] : ? [v28] : ( ~ (v28 = 0) & mem(v27, v25) = v28 & mem(v27, v24) = 0)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast16p(v26) = v25) | ~ (atleast16p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast15p(v26) = v25) | ~ (atleast15p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast14p(v26) = v25) | ~ (atleast14p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast13p(v26) = v25) | ~ (atleast13p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast12p(v26) = v25) | ~ (atleast12p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast11p(v26) = v25) | ~ (atleast11p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast10p(v26) = v25) | ~ (atleast10p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast9p(v26) = v25) | ~ (atleast9p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast8p(v26) = v25) | ~ (atleast8p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast7p(v26) = v25) | ~ (atleast7p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast6p(v26) = v25) | ~ (atleast6p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast5p(v26) = v25) | ~ (atleast5p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast4p(v26) = v25) | ~ (atleast4p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast3p(v26) = v25) | ~ (atleast3p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (atleast2p(v26) = v25) | ~ (atleast2p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (p(v26) = v25) | ~ (p(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (n(v26) = v25) | ~ (n(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (s(v26) = v25) | ~ (s(v26) = v24)) & ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (s(v25) = v26) | ~ (mem(v24, v26) = 0)) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast16p(v24) = v25) | ~ (atleast15p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast16p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast15p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast15p(v24) = v25) | ~ (atleast14p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast15p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast14p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast14p(v24) = v25) | ~ (atleast13p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast14p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast13p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast13p(v24) = v25) | ~ (atleast12p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast13p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast12p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast12p(v24) = v25) | ~ (atleast11p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast12p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast11p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast11p(v24) = v25) | ~ (atleast10p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast11p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast10p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast10p(v24) = v25) | ~ (atleast9p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast10p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast9p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast9p(v24) = v25) | ~ (atleast8p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast9p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast8p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast8p(v24) = v25) | ~ (atleast7p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast8p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast7p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast7p(v24) = v25) | ~ (atleast6p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast7p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast6p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast6p(v24) = v25) | ~ (atleast5p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast6p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast5p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast5p(v24) = v25) | ~ (atleast4p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast5p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast4p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast4p(v24) = v25) | ~ (atleast3p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast4p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast3p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast3p(v24) = v25) | ~ (atleast2p(v26) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & subq(v26, v24) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast3p(v24) = v25) | ~ (subq(v26, v24) = 0) | ? [v27] : ((v27 = 0 & subq(v24, v26) = 0) | ( ~ (v27 = 0) & atleast2p(v26) = v27))) & ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (atleast2p(v24) = v25) | ~ (mem(v26, v24) = 0) | ? [v27] : (p(v26) = v27 & subq(v24, v27) = 0)) & ! [v24] : ! [v25] : ! [v26] : ( ~ (p(v25) = v26) | ~ (mem(v24, v26) = 0) | subq(v24, v25) = 0) & ! [v24] : ! [v25] : ! [v26] : ( ~ (a(v24, v25) = v26) | ? [v27] : (u(v24, v27) = v26 & s(v25) = v27)) & ! [v24] : ! [v25] : ! [v26] : ( ~ (disj(v24, v25) = 0) | ~ (mem(v26, v25) = 0) | ? [v27] : ( ~ (v27 = 0) & mem(v26, v24) = v27)) & ! [v24] : ! [v25] : ! [v26] : ( ~ (disj(v24, v25) = 0) | ~ (mem(v26, v24) = 0) | ? [v27] : ( ~ (v27 = 0) & mem(v26, v25) = v27)) & ! [v24] : ! [v25] : ! [v26] : ( ~ (subq(v24, v25) = 0) | ~ (mem(v26, v24) = 0) | mem(v26, v25) = 0) & ! [v24] : ! [v25] : (v25 = v24 | ~ (subq(v25, v24) = 0) | ? [v26] : ( ~ (v26 = 0) & subq(v24, v25) = v26)) & ! [v24] : ! [v25] : (v25 = v24 | ~ (subq(v24, v25) = 0) | ? [v26] : ( ~ (v26 = 0) & subq(v25, v24) = v26)) & ! [v24] : ! [v25] : ( ~ (n(v24) = v25) | a(v24, v24) = v25) & ! [v24] : ! [v25] : ( ~ (a(v24, v24) = v25) | n(v24) = v25) & ! [v24] : ! [v25] : ( ~ (subq(v24, v25) = 0) | ? [v26] : (p(v25) = v26 & mem(v24, v26) = 0)) & ! [v24] : ( ~ (atleast16p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast15p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast15p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast14p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast14p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast13p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast13p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast12p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast12p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast11p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast11p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast10p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast10p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast9p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast9p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast8p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast8p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast7p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast7p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast6p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast6p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast5p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast5p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast4p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast4p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast3p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast3p(v24) = 0) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & atleast2p(v25) = 0 & subq(v25, v24) = 0 & subq(v24, v25) = v26)) & ! [v24] : ( ~ (atleast2p(v24) = 0) | ? [v25] : ? [v26] : ? [v27] : ( ~ (v27 = 0) & p(v25) = v26 & subq(v24, v26) = v27 & mem(v25, v24) = 0)) & ! [v24] : ~ (mem(v24, e) = 0) & ? [v24] : ? [v25] : ? [v26] : a(v25, v24) = v26 & ? [v24] : ? [v25] : ? [v26] : m(v25, v24) = v26 & ? [v24] : ? [v25] : ? [v26] : u(v25, v24) = v26 & ? [v24] : ? [v25] : ? [v26] : disj(v25, v24) = v26 & ? [v24] : ? [v25] : ? [v26] : subq(v25, v24) = v26 & ? [v24] : ? [v25] : ? [v26] : mem(v25, v24) = v26 & ? [v24] : ? [v25] : atleast16p(v24) = v25 & ? [v24] : ? [v25] : atleast15p(v24) = v25 & ? [v24] : ? [v25] : atleast14p(v24) = v25 & ? [v24] : ? [v25] : atleast13p(v24) = v25 & ? [v24] : ? [v25] : atleast12p(v24) = v25 & ? [v24] : ? [v25] : atleast11p(v24) = v25 & ? [v24] : ? [v25] : atleast10p(v24) = v25 & ? [v24] : ? [v25] : atleast9p(v24) = v25 & ? [v24] : ? [v25] : atleast8p(v24) = v25 & ? [v24] : ? [v25] : atleast7p(v24) = v25 & ? [v24] : ? [v25] : atleast6p(v24) = v25 & ? [v24] : ? [v25] : atleast5p(v24) = v25 & ? [v24] : ? [v25] : atleast4p(v24) = v25 & ? [v24] : ? [v25] : atleast3p(v24) = v25 & ? [v24] : ? [v25] : atleast2p(v24) = v25 & ? [v24] : ? [v25] : p(v24) = v25 & ? [v24] : ? [v25] : n(v24) = v25 & ? [v24] : ? [v25] : s(v24) = v25) % 26.75/7.49 | 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, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19, all_0_20_20, all_0_21_21, all_0_22_22, all_0_23_23 yields: % 26.75/7.49 | (1) ~ (all_0_0_0 = 0) & p(all_0_20_20) = all_0_19_19 & p(all_0_22_22) = all_0_4_4 & n(all_0_9_9) = all_0_8_8 & n(all_0_17_17) = all_0_16_16 & n(all_0_20_20) = all_0_17_17 & n(all_0_22_22) = all_0_15_15 & n(all_0_23_23) = all_0_22_22 & n(e) = all_0_23_23 & a(all_0_5_5, all_0_4_4) = all_0_3_3 & a(all_0_10_10, all_0_22_22) = all_0_9_9 & a(all_0_12_12, all_0_15_15) = all_0_11_11 & a(all_0_16_16, all_0_15_15) = all_0_14_14 & a(all_0_20_20, all_0_19_19) = all_0_6_6 & a(all_0_21_21, all_0_19_19) = all_0_18_18 & u(all_0_6_6, all_0_3_3) = all_0_2_2 & u(all_0_7_7, all_0_2_2) = all_0_1_1 & u(all_0_11_11, all_0_8_8) = all_0_7_7 & u(all_0_18_18, all_0_14_14) = all_0_13_13 & s(all_0_17_17) = all_0_5_5 & s(all_0_20_20) = all_0_10_10 & s(all_0_21_21) = all_0_12_12 & s(all_0_22_22) = all_0_21_21 & s(all_0_23_23) = all_0_20_20 & subq(all_0_13_13, 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 % 27.18/7.51 | % 27.18/7.51 | Applying alpha-rule on (1) yields: % 27.18/7.51 | (2) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 27.18/7.51 | (3) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 27.18/7.51 | (4) s(all_0_20_20) = all_0_10_10 % 27.18/7.51 | (5) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.51 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 27.18/7.51 | (7) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 27.18/7.52 | (8) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 27.18/7.52 | (9) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.52 | (10) s(all_0_21_21) = all_0_12_12 % 27.18/7.52 | (11) p(all_0_20_20) = all_0_19_19 % 27.18/7.52 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.52 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 27.18/7.52 | (14) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 27.18/7.52 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.52 | (16) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 27.18/7.52 | (17) u(all_0_11_11, all_0_8_8) = all_0_7_7 % 27.18/7.52 | (18) ! [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)) % 27.18/7.52 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 27.18/7.52 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 27.18/7.52 | (21) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 27.18/7.52 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 27.18/7.52 | (23) u(all_0_18_18, all_0_14_14) = all_0_13_13 % 27.18/7.52 | (24) ! [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))) % 27.18/7.52 | (25) ! [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))) % 27.18/7.52 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.52 | (27) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 27.18/7.52 | (28) n(all_0_20_20) = all_0_17_17 % 27.18/7.52 | (29) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.52 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 27.18/7.52 | (31) ! [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))) % 27.18/7.52 | (32) ! [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))) % 27.18/7.52 | (33) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.52 | (34) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 27.18/7.52 | (35) a(all_0_20_20, all_0_19_19) = all_0_6_6 % 27.18/7.52 | (36) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 27.18/7.52 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 27.18/7.52 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 27.18/7.52 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.52 | (40) ? [v0] : ? [v1] : s(v0) = v1 % 27.18/7.52 | (41) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 27.18/7.52 | (42) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 27.18/7.52 | (43) a(all_0_21_21, all_0_19_19) = all_0_18_18 % 27.18/7.52 | (44) ! [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))) % 27.18/7.52 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 27.18/7.52 | (46) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 27.18/7.52 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 27.18/7.52 | (48) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.52 | (49) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 27.18/7.52 | (50) u(all_0_6_6, all_0_3_3) = all_0_2_2 % 27.18/7.52 | (51) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 27.18/7.52 | (52) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 27.18/7.52 | (53) a(all_0_12_12, all_0_15_15) = all_0_11_11 % 27.18/7.52 | (54) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.52 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 27.18/7.52 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 27.18/7.52 | (57) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 27.18/7.53 | (58) ! [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))) % 27.18/7.53 | (59) ! [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))) % 27.18/7.53 | (60) u(all_0_7_7, all_0_2_2) = all_0_1_1 % 27.18/7.53 | (61) ! [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))) % 27.18/7.53 | (62) ! [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))) % 27.18/7.53 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 27.18/7.53 | (64) subq(all_0_13_13, all_0_1_1) = all_0_0_0 % 27.18/7.53 | (65) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 27.18/7.53 | (66) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 27.18/7.53 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 27.18/7.53 | (68) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.53 | (69) s(all_0_22_22) = all_0_21_21 % 27.18/7.53 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 27.18/7.53 | (71) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 27.18/7.53 | (72) n(all_0_9_9) = all_0_8_8 % 27.18/7.53 | (73) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (74) a(all_0_10_10, all_0_22_22) = all_0_9_9 % 27.18/7.53 | (75) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 27.18/7.53 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (77) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.53 | (78) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 27.18/7.53 | (79) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (81) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 27.18/7.53 | (82) s(all_0_23_23) = all_0_20_20 % 27.18/7.53 | (83) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 27.18/7.53 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 27.18/7.53 | (85) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.53 | (86) s(all_0_17_17) = all_0_5_5 % 27.18/7.53 | (87) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 27.18/7.53 | (88) ! [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))) % 27.18/7.53 | (89) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 27.18/7.53 | (90) ! [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))) % 27.18/7.53 | (91) ! [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))) % 27.18/7.53 | (92) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 27.18/7.53 | (93) p(all_0_22_22) = all_0_4_4 % 27.18/7.53 | (94) n(all_0_23_23) = all_0_22_22 % 27.18/7.53 | (95) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 27.18/7.53 | (96) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (97) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 27.18/7.53 | (98) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 27.18/7.53 | (99) n(all_0_22_22) = all_0_15_15 % 27.18/7.53 | (100) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 27.18/7.53 | (101) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 27.18/7.53 | (102) a(all_0_5_5, all_0_4_4) = all_0_3_3 % 27.18/7.53 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 27.18/7.53 | (104) ! [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))) % 27.18/7.53 | (105) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (106) n(all_0_17_17) = all_0_16_16 % 27.18/7.53 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 27.18/7.53 | (108) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 27.18/7.53 | (109) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.53 | (110) ! [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))) % 27.18/7.53 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 27.18/7.53 | (112) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 27.18/7.53 | (113) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 27.18/7.53 | (114) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 27.18/7.53 | (115) ? [v0] : ? [v1] : p(v0) = v1 % 27.18/7.53 | (116) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 27.18/7.53 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 27.18/7.53 | (118) n(e) = all_0_23_23 % 27.18/7.53 | (119) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 27.18/7.53 | (120) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.53 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 27.18/7.54 | (122) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 27.18/7.54 | (123) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 27.18/7.54 | (124) ! [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))) % 27.18/7.54 | (125) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.54 | (126) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.54 | (127) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.54 | (128) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 27.18/7.54 | (129) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 27.18/7.54 | (130) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.54 | (131) ~ (all_0_0_0 = 0) % 27.18/7.54 | (132) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast14p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 27.18/7.54 | (133) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.54 | (134) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 27.18/7.54 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 27.18/7.54 | (136) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 27.18/7.54 | (137) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 27.18/7.54 | (138) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 27.18/7.54 | (139) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 27.18/7.54 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 27.18/7.54 | (141) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 27.18/7.54 | (142) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 27.18/7.54 | (143) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 27.18/7.54 | (144) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 27.18/7.54 | (145) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 27.18/7.54 | (146) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 27.18/7.54 | (147) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 27.18/7.54 | (148) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 27.18/7.54 | (149) a(all_0_16_16, all_0_15_15) = all_0_14_14 % 27.18/7.54 | (150) ? [v0] : ? [v1] : n(v0) = v1 % 27.18/7.54 | (151) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 27.18/7.54 | (152) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 27.18/7.54 | (153) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 27.18/7.54 | (154) ! [v0] : ~ (mem(v0, e) = 0) % 27.18/7.54 | (155) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 27.18/7.54 | (156) ! [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))) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (142) with all_0_8_8, all_0_9_9 and discharging atoms n(all_0_9_9) = all_0_8_8, yields: % 27.18/7.54 | (157) a(all_0_9_9, all_0_9_9) = all_0_8_8 % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (142) with all_0_16_16, all_0_17_17 and discharging atoms n(all_0_17_17) = all_0_16_16, yields: % 27.18/7.54 | (158) a(all_0_17_17, all_0_17_17) = all_0_16_16 % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (142) with all_0_17_17, all_0_20_20 and discharging atoms n(all_0_20_20) = all_0_17_17, yields: % 27.18/7.54 | (159) a(all_0_20_20, all_0_20_20) = all_0_17_17 % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (142) with all_0_15_15, all_0_22_22 and discharging atoms n(all_0_22_22) = all_0_15_15, yields: % 27.18/7.54 | (160) a(all_0_22_22, all_0_22_22) = all_0_15_15 % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_3_3, all_0_4_4, all_0_5_5 and discharging atoms a(all_0_5_5, all_0_4_4) = all_0_3_3, yields: % 27.18/7.54 | (161) ? [v0] : (u(all_0_5_5, v0) = all_0_3_3 & s(all_0_4_4) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_9_9, all_0_22_22, all_0_10_10 and discharging atoms a(all_0_10_10, all_0_22_22) = all_0_9_9, yields: % 27.18/7.54 | (162) ? [v0] : (u(all_0_10_10, v0) = all_0_9_9 & s(all_0_22_22) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_11_11, all_0_15_15, all_0_12_12 and discharging atoms a(all_0_12_12, all_0_15_15) = all_0_11_11, yields: % 27.18/7.54 | (163) ? [v0] : (u(all_0_12_12, v0) = all_0_11_11 & s(all_0_15_15) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_14_14, all_0_15_15, all_0_16_16 and discharging atoms a(all_0_16_16, all_0_15_15) = all_0_14_14, yields: % 27.18/7.54 | (164) ? [v0] : (u(all_0_16_16, v0) = all_0_14_14 & s(all_0_15_15) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_6_6, all_0_19_19, all_0_20_20 and discharging atoms a(all_0_20_20, all_0_19_19) = all_0_6_6, yields: % 27.18/7.54 | (165) ? [v0] : (u(all_0_20_20, v0) = all_0_6_6 & s(all_0_19_19) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (71) with all_0_18_18, all_0_19_19, all_0_21_21 and discharging atoms a(all_0_21_21, all_0_19_19) = all_0_18_18, yields: % 27.18/7.54 | (166) ? [v0] : (u(all_0_21_21, v0) = all_0_18_18 & s(all_0_19_19) = v0) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (7) with all_0_0_0, all_0_1_1, all_0_13_13 and discharging atoms subq(all_0_13_13, all_0_1_1) = all_0_0_0, yields: % 27.18/7.54 | (167) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_13_13, v0) = v1) % 27.18/7.54 | % 27.18/7.54 | Instantiating formula (128) with all_0_0_0, all_0_1_1, all_0_13_13 and discharging atoms subq(all_0_13_13, all_0_1_1) = all_0_0_0, yields: % 27.18/7.54 | (168) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_13_13) = 0) % 27.18/7.54 | % 27.18/7.54 | Instantiating (166) with all_57_0_78 yields: % 27.18/7.54 | (169) u(all_0_21_21, all_57_0_78) = all_0_18_18 & s(all_0_19_19) = all_57_0_78 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (169) yields: % 27.18/7.54 | (170) u(all_0_21_21, all_57_0_78) = all_0_18_18 % 27.18/7.54 | (171) s(all_0_19_19) = all_57_0_78 % 27.18/7.54 | % 27.18/7.54 | Instantiating (165) with all_59_0_79 yields: % 27.18/7.54 | (172) u(all_0_20_20, all_59_0_79) = all_0_6_6 & s(all_0_19_19) = all_59_0_79 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (172) yields: % 27.18/7.54 | (173) u(all_0_20_20, all_59_0_79) = all_0_6_6 % 27.18/7.54 | (174) s(all_0_19_19) = all_59_0_79 % 27.18/7.54 | % 27.18/7.54 | Instantiating (164) with all_61_0_80 yields: % 27.18/7.54 | (175) u(all_0_16_16, all_61_0_80) = all_0_14_14 & s(all_0_15_15) = all_61_0_80 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (175) yields: % 27.18/7.54 | (176) u(all_0_16_16, all_61_0_80) = all_0_14_14 % 27.18/7.54 | (177) s(all_0_15_15) = all_61_0_80 % 27.18/7.54 | % 27.18/7.54 | Instantiating (162) with all_63_0_81 yields: % 27.18/7.54 | (178) u(all_0_10_10, all_63_0_81) = all_0_9_9 & s(all_0_22_22) = all_63_0_81 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (178) yields: % 27.18/7.54 | (179) u(all_0_10_10, all_63_0_81) = all_0_9_9 % 27.18/7.54 | (180) s(all_0_22_22) = all_63_0_81 % 27.18/7.54 | % 27.18/7.54 | Instantiating (161) with all_65_0_82 yields: % 27.18/7.54 | (181) u(all_0_5_5, all_65_0_82) = all_0_3_3 & s(all_0_4_4) = all_65_0_82 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (181) yields: % 27.18/7.54 | (182) u(all_0_5_5, all_65_0_82) = all_0_3_3 % 27.18/7.54 | (183) s(all_0_4_4) = all_65_0_82 % 27.18/7.54 | % 27.18/7.54 | Instantiating (163) with all_67_0_83 yields: % 27.18/7.54 | (184) u(all_0_12_12, all_67_0_83) = all_0_11_11 & s(all_0_15_15) = all_67_0_83 % 27.18/7.54 | % 27.18/7.54 | Applying alpha-rule on (184) yields: % 27.18/7.54 | (185) u(all_0_12_12, all_67_0_83) = all_0_11_11 % 27.18/7.54 | (186) s(all_0_15_15) = all_67_0_83 % 27.18/7.54 | % 27.18/7.54 +-Applying beta-rule and splitting (167), into two cases. % 27.18/7.54 |-Branch one: % 27.18/7.54 | (187) all_0_0_0 = 0 % 27.18/7.54 | % 27.18/7.54 | Equations (187) can reduce 131 to: % 27.18/7.54 | (188) $false % 27.18/7.54 | % 27.18/7.54 |-The branch is then unsatisfiable % 27.18/7.54 |-Branch two: % 27.18/7.54 | (131) ~ (all_0_0_0 = 0) % 27.18/7.54 | (190) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_13_13, v0) = v1) % 27.18/7.54 | % 27.18/7.54 +-Applying beta-rule and splitting (168), into two cases. % 27.18/7.54 |-Branch one: % 27.18/7.54 | (187) all_0_0_0 = 0 % 27.18/7.54 | % 27.18/7.54 | Equations (187) can reduce 131 to: % 27.18/7.54 | (188) $false % 27.18/7.54 | % 27.18/7.55 |-The branch is then unsatisfiable % 27.18/7.55 |-Branch two: % 27.18/7.55 | (131) ~ (all_0_0_0 = 0) % 27.18/7.55 | (194) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_13_13) = 0) % 27.18/7.55 | % 27.18/7.55 | Instantiating (194) with all_78_0_86, all_78_1_87 yields: % 27.18/7.55 | (195) ~ (all_78_0_86 = 0) & mem(all_78_1_87, all_0_1_1) = all_78_0_86 & mem(all_78_1_87, all_0_13_13) = 0 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (195) yields: % 27.18/7.55 | (196) ~ (all_78_0_86 = 0) % 27.18/7.55 | (197) mem(all_78_1_87, all_0_1_1) = all_78_0_86 % 27.18/7.55 | (198) mem(all_78_1_87, all_0_13_13) = 0 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_15_15, all_61_0_80, all_67_0_83 and discharging atoms s(all_0_15_15) = all_67_0_83, s(all_0_15_15) = all_61_0_80, yields: % 27.18/7.55 | (199) all_67_0_83 = all_61_0_80 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_19_19, all_57_0_78, all_59_0_79 and discharging atoms s(all_0_19_19) = all_59_0_79, s(all_0_19_19) = all_57_0_78, yields: % 27.18/7.55 | (200) all_59_0_79 = all_57_0_78 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_22_22, all_63_0_81, all_0_21_21 and discharging atoms s(all_0_22_22) = all_63_0_81, s(all_0_22_22) = all_0_21_21, yields: % 27.18/7.55 | (201) all_63_0_81 = all_0_21_21 % 27.18/7.55 | % 27.18/7.55 | From (201) and (179) follows: % 27.18/7.55 | (202) u(all_0_10_10, all_0_21_21) = all_0_9_9 % 27.18/7.55 | % 27.18/7.55 | From (199) and (185) follows: % 27.18/7.55 | (203) u(all_0_12_12, all_61_0_80) = all_0_11_11 % 27.18/7.55 | % 27.18/7.55 | From (200) and (173) follows: % 27.18/7.55 | (204) u(all_0_20_20, all_57_0_78) = all_0_6_6 % 27.18/7.55 | % 27.18/7.55 | From (201) and (180) follows: % 27.18/7.55 | (69) s(all_0_22_22) = all_0_21_21 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (71) 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: % 27.18/7.55 | (206) ? [v0] : (u(all_0_9_9, v0) = all_0_8_8 & s(all_0_9_9) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (71) with all_0_16_16, all_0_17_17, all_0_17_17 and discharging atoms a(all_0_17_17, all_0_17_17) = all_0_16_16, yields: % 27.18/7.55 | (207) ? [v0] : (u(all_0_17_17, v0) = all_0_16_16 & s(all_0_17_17) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (71) with all_0_17_17, all_0_20_20, all_0_20_20 and discharging atoms a(all_0_20_20, all_0_20_20) = all_0_17_17, yields: % 27.18/7.55 | (208) ? [v0] : (u(all_0_20_20, v0) = all_0_17_17 & s(all_0_20_20) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (71) with all_0_15_15, all_0_22_22, all_0_22_22 and discharging atoms a(all_0_22_22, all_0_22_22) = all_0_15_15, yields: % 27.18/7.55 | (209) ? [v0] : (u(all_0_22_22, v0) = all_0_15_15 & s(all_0_22_22) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_78_0_86, all_0_1_1, all_0_2_2, all_0_7_7, all_78_1_87 and discharging atoms u(all_0_7_7, all_0_2_2) = all_0_1_1, mem(all_78_1_87, all_0_1_1) = all_78_0_86, yields: % 27.18/7.55 | (210) all_78_0_86 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_2_2) = v1 & mem(all_78_1_87, all_0_7_7) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (44) with all_0_13_13, all_0_14_14, all_0_18_18, all_78_1_87 and discharging atoms u(all_0_18_18, all_0_14_14) = all_0_13_13, mem(all_78_1_87, all_0_13_13) = 0, yields: % 27.18/7.55 | (211) ? [v0] : ((v0 = 0 & mem(all_78_1_87, all_0_14_14) = 0) | (v0 = 0 & mem(all_78_1_87, all_0_18_18) = 0)) % 27.18/7.55 | % 27.18/7.55 | Instantiating (211) with all_89_0_88 yields: % 27.18/7.55 | (212) (all_89_0_88 = 0 & mem(all_78_1_87, all_0_14_14) = 0) | (all_89_0_88 = 0 & mem(all_78_1_87, all_0_18_18) = 0) % 27.18/7.55 | % 27.18/7.55 | Instantiating (209) with all_90_0_89 yields: % 27.18/7.55 | (213) u(all_0_22_22, all_90_0_89) = all_0_15_15 & s(all_0_22_22) = all_90_0_89 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (213) yields: % 27.18/7.55 | (214) u(all_0_22_22, all_90_0_89) = all_0_15_15 % 27.18/7.55 | (215) s(all_0_22_22) = all_90_0_89 % 27.18/7.55 | % 27.18/7.55 | Instantiating (208) with all_92_0_90 yields: % 27.18/7.55 | (216) u(all_0_20_20, all_92_0_90) = all_0_17_17 & s(all_0_20_20) = all_92_0_90 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (216) yields: % 27.18/7.55 | (217) u(all_0_20_20, all_92_0_90) = all_0_17_17 % 27.18/7.55 | (218) s(all_0_20_20) = all_92_0_90 % 27.18/7.55 | % 27.18/7.55 | Instantiating (207) with all_94_0_91 yields: % 27.18/7.55 | (219) u(all_0_17_17, all_94_0_91) = all_0_16_16 & s(all_0_17_17) = all_94_0_91 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (219) yields: % 27.18/7.55 | (220) u(all_0_17_17, all_94_0_91) = all_0_16_16 % 27.18/7.55 | (221) s(all_0_17_17) = all_94_0_91 % 27.18/7.55 | % 27.18/7.55 | Instantiating (206) with all_100_0_94 yields: % 27.18/7.55 | (222) u(all_0_9_9, all_100_0_94) = all_0_8_8 & s(all_0_9_9) = all_100_0_94 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (222) yields: % 27.18/7.55 | (223) u(all_0_9_9, all_100_0_94) = all_0_8_8 % 27.18/7.55 | (224) s(all_0_9_9) = all_100_0_94 % 27.18/7.55 | % 27.18/7.55 +-Applying beta-rule and splitting (210), into two cases. % 27.18/7.55 |-Branch one: % 27.18/7.55 | (225) all_78_0_86 = 0 % 27.18/7.55 | % 27.18/7.55 | Equations (225) can reduce 196 to: % 27.18/7.55 | (188) $false % 27.18/7.55 | % 27.18/7.55 |-The branch is then unsatisfiable % 27.18/7.55 |-Branch two: % 27.18/7.55 | (196) ~ (all_78_0_86 = 0) % 27.18/7.55 | (228) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_2_2) = v1 & mem(all_78_1_87, all_0_7_7) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating (228) with all_106_0_95, all_106_1_96 yields: % 27.18/7.55 | (229) ~ (all_106_0_95 = 0) & ~ (all_106_1_96 = 0) & mem(all_78_1_87, all_0_2_2) = all_106_0_95 & mem(all_78_1_87, all_0_7_7) = all_106_1_96 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (229) yields: % 27.18/7.55 | (230) ~ (all_106_0_95 = 0) % 27.18/7.55 | (231) ~ (all_106_1_96 = 0) % 27.18/7.55 | (232) mem(all_78_1_87, all_0_2_2) = all_106_0_95 % 27.18/7.55 | (233) mem(all_78_1_87, all_0_7_7) = all_106_1_96 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_17_17, all_94_0_91, all_0_5_5 and discharging atoms s(all_0_17_17) = all_94_0_91, s(all_0_17_17) = all_0_5_5, yields: % 27.18/7.55 | (234) all_94_0_91 = all_0_5_5 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_20_20, all_92_0_90, all_0_10_10 and discharging atoms s(all_0_20_20) = all_92_0_90, s(all_0_20_20) = all_0_10_10, yields: % 27.18/7.55 | (235) all_92_0_90 = all_0_10_10 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (56) with all_0_22_22, all_90_0_89, all_0_21_21 and discharging atoms s(all_0_22_22) = all_90_0_89, s(all_0_22_22) = all_0_21_21, yields: % 27.18/7.55 | (236) all_90_0_89 = all_0_21_21 % 27.18/7.55 | % 27.18/7.55 | From (234) and (220) follows: % 27.18/7.55 | (237) u(all_0_17_17, all_0_5_5) = all_0_16_16 % 27.18/7.55 | % 27.18/7.55 | From (235) and (217) follows: % 27.18/7.55 | (238) u(all_0_20_20, all_0_10_10) = all_0_17_17 % 27.18/7.55 | % 27.18/7.55 | From (236) and (215) follows: % 27.18/7.55 | (69) s(all_0_22_22) = all_0_21_21 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_106_0_95, all_0_2_2, all_0_3_3, all_0_6_6, all_78_1_87 and discharging atoms u(all_0_6_6, all_0_3_3) = all_0_2_2, mem(all_78_1_87, all_0_2_2) = all_106_0_95, yields: % 27.18/7.55 | (240) all_106_0_95 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_3_3) = v1 & mem(all_78_1_87, all_0_6_6) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_106_1_96, all_0_7_7, all_0_8_8, all_0_11_11, all_78_1_87 and discharging atoms u(all_0_11_11, all_0_8_8) = all_0_7_7, mem(all_78_1_87, all_0_7_7) = all_106_1_96, yields: % 27.18/7.55 | (241) all_106_1_96 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_8_8) = v1 & mem(all_78_1_87, all_0_11_11) = v0) % 27.18/7.55 | % 27.18/7.55 +-Applying beta-rule and splitting (212), into two cases. % 27.18/7.55 |-Branch one: % 27.18/7.55 | (242) all_89_0_88 = 0 & mem(all_78_1_87, all_0_14_14) = 0 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (242) yields: % 27.18/7.55 | (243) all_89_0_88 = 0 % 27.18/7.55 | (244) mem(all_78_1_87, all_0_14_14) = 0 % 27.18/7.55 | % 27.18/7.55 +-Applying beta-rule and splitting (240), into two cases. % 27.18/7.55 |-Branch one: % 27.18/7.55 | (245) all_106_0_95 = 0 % 27.18/7.55 | % 27.18/7.55 | Equations (245) can reduce 230 to: % 27.18/7.55 | (188) $false % 27.18/7.55 | % 27.18/7.55 |-The branch is then unsatisfiable % 27.18/7.55 |-Branch two: % 27.18/7.55 | (230) ~ (all_106_0_95 = 0) % 27.18/7.55 | (248) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_3_3) = v1 & mem(all_78_1_87, all_0_6_6) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating (248) with all_123_0_97, all_123_1_98 yields: % 27.18/7.55 | (249) ~ (all_123_0_97 = 0) & ~ (all_123_1_98 = 0) & mem(all_78_1_87, all_0_3_3) = all_123_0_97 & mem(all_78_1_87, all_0_6_6) = all_123_1_98 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (249) yields: % 27.18/7.55 | (250) ~ (all_123_0_97 = 0) % 27.18/7.55 | (251) ~ (all_123_1_98 = 0) % 27.18/7.55 | (252) mem(all_78_1_87, all_0_3_3) = all_123_0_97 % 27.18/7.55 | (253) mem(all_78_1_87, all_0_6_6) = all_123_1_98 % 27.18/7.55 | % 27.18/7.55 +-Applying beta-rule and splitting (241), into two cases. % 27.18/7.55 |-Branch one: % 27.18/7.55 | (254) all_106_1_96 = 0 % 27.18/7.55 | % 27.18/7.55 | Equations (254) can reduce 231 to: % 27.18/7.55 | (188) $false % 27.18/7.55 | % 27.18/7.55 |-The branch is then unsatisfiable % 27.18/7.55 |-Branch two: % 27.18/7.55 | (231) ~ (all_106_1_96 = 0) % 27.18/7.55 | (257) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_8_8) = v1 & mem(all_78_1_87, all_0_11_11) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating (257) with all_128_0_99, all_128_1_100 yields: % 27.18/7.55 | (258) ~ (all_128_0_99 = 0) & ~ (all_128_1_100 = 0) & mem(all_78_1_87, all_0_8_8) = all_128_0_99 & mem(all_78_1_87, all_0_11_11) = all_128_1_100 % 27.18/7.55 | % 27.18/7.55 | Applying alpha-rule on (258) yields: % 27.18/7.55 | (259) ~ (all_128_0_99 = 0) % 27.18/7.55 | (260) ~ (all_128_1_100 = 0) % 27.18/7.55 | (261) mem(all_78_1_87, all_0_8_8) = all_128_0_99 % 27.18/7.55 | (262) mem(all_78_1_87, all_0_11_11) = all_128_1_100 % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_123_0_97, all_0_3_3, all_65_0_82, all_0_5_5, all_78_1_87 and discharging atoms u(all_0_5_5, all_65_0_82) = all_0_3_3, mem(all_78_1_87, all_0_3_3) = all_123_0_97, yields: % 27.18/7.55 | (263) all_123_0_97 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_65_0_82) = v1 & mem(all_78_1_87, all_0_5_5) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_123_1_98, all_0_6_6, all_57_0_78, all_0_20_20, all_78_1_87 and discharging atoms u(all_0_20_20, all_57_0_78) = all_0_6_6, mem(all_78_1_87, all_0_6_6) = all_123_1_98, yields: % 27.18/7.55 | (264) all_123_1_98 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_57_0_78) = v1 & mem(all_78_1_87, all_0_20_20) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_128_0_99, all_0_8_8, all_100_0_94, all_0_9_9, all_78_1_87 and discharging atoms u(all_0_9_9, all_100_0_94) = all_0_8_8, mem(all_78_1_87, all_0_8_8) = all_128_0_99, yields: % 27.18/7.55 | (265) all_128_0_99 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_100_0_94) = v1 & mem(all_78_1_87, all_0_9_9) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (18) with all_128_1_100, all_0_11_11, all_61_0_80, all_0_12_12, all_78_1_87 and discharging atoms u(all_0_12_12, all_61_0_80) = all_0_11_11, mem(all_78_1_87, all_0_11_11) = all_128_1_100, yields: % 27.18/7.55 | (266) all_128_1_100 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_61_0_80) = v1 & mem(all_78_1_87, all_0_12_12) = v0) % 27.18/7.55 | % 27.18/7.55 | Instantiating formula (44) with all_0_14_14, all_61_0_80, all_0_16_16, all_78_1_87 and discharging atoms u(all_0_16_16, all_61_0_80) = all_0_14_14, mem(all_78_1_87, all_0_14_14) = 0, yields: % 27.18/7.55 | (267) ? [v0] : ((v0 = 0 & mem(all_78_1_87, all_61_0_80) = 0) | (v0 = 0 & mem(all_78_1_87, all_0_16_16) = 0)) % 27.18/7.55 | % 27.18/7.55 | Instantiating (267) with all_135_0_101 yields: % 27.18/7.55 | (268) (all_135_0_101 = 0 & mem(all_78_1_87, all_61_0_80) = 0) | (all_135_0_101 = 0 & mem(all_78_1_87, all_0_16_16) = 0) % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (266), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (269) all_128_1_100 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (269) can reduce 260 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (260) ~ (all_128_1_100 = 0) % 27.18/7.56 | (272) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_61_0_80) = v1 & mem(all_78_1_87, all_0_12_12) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (272) with all_138_0_102, all_138_1_103 yields: % 27.18/7.56 | (273) ~ (all_138_0_102 = 0) & ~ (all_138_1_103 = 0) & mem(all_78_1_87, all_61_0_80) = all_138_0_102 & mem(all_78_1_87, all_0_12_12) = all_138_1_103 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (273) yields: % 27.18/7.56 | (274) ~ (all_138_0_102 = 0) % 27.18/7.56 | (275) ~ (all_138_1_103 = 0) % 27.18/7.56 | (276) mem(all_78_1_87, all_61_0_80) = all_138_0_102 % 27.18/7.56 | (277) mem(all_78_1_87, all_0_12_12) = all_138_1_103 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (268), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (278) all_135_0_101 = 0 & mem(all_78_1_87, all_61_0_80) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (278) yields: % 27.18/7.56 | (279) all_135_0_101 = 0 % 27.18/7.56 | (280) mem(all_78_1_87, all_61_0_80) = 0 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (63) with all_78_1_87, all_61_0_80, 0, all_138_0_102 and discharging atoms mem(all_78_1_87, all_61_0_80) = all_138_0_102, mem(all_78_1_87, all_61_0_80) = 0, yields: % 27.18/7.56 | (281) all_138_0_102 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (281) can reduce 274 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (283) all_135_0_101 = 0 & mem(all_78_1_87, all_0_16_16) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (283) yields: % 27.18/7.56 | (279) all_135_0_101 = 0 % 27.18/7.56 | (285) mem(all_78_1_87, all_0_16_16) = 0 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (265), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (286) all_128_0_99 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (286) can reduce 259 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (259) ~ (all_128_0_99 = 0) % 27.18/7.56 | (289) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_100_0_94) = v1 & mem(all_78_1_87, all_0_9_9) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (289) with all_147_0_110, all_147_1_111 yields: % 27.18/7.56 | (290) ~ (all_147_0_110 = 0) & ~ (all_147_1_111 = 0) & mem(all_78_1_87, all_100_0_94) = all_147_0_110 & mem(all_78_1_87, all_0_9_9) = all_147_1_111 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (290) yields: % 27.18/7.56 | (291) ~ (all_147_0_110 = 0) % 27.18/7.56 | (292) ~ (all_147_1_111 = 0) % 27.18/7.56 | (293) mem(all_78_1_87, all_100_0_94) = all_147_0_110 % 27.18/7.56 | (294) mem(all_78_1_87, all_0_9_9) = all_147_1_111 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (263), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (295) all_123_0_97 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (295) can reduce 250 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (250) ~ (all_123_0_97 = 0) % 27.18/7.56 | (298) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_65_0_82) = v1 & mem(all_78_1_87, all_0_5_5) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (298) with all_153_0_112, all_153_1_113 yields: % 27.18/7.56 | (299) ~ (all_153_0_112 = 0) & ~ (all_153_1_113 = 0) & mem(all_78_1_87, all_65_0_82) = all_153_0_112 & mem(all_78_1_87, all_0_5_5) = all_153_1_113 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (299) yields: % 27.18/7.56 | (300) ~ (all_153_0_112 = 0) % 27.18/7.56 | (301) ~ (all_153_1_113 = 0) % 27.18/7.56 | (302) mem(all_78_1_87, all_65_0_82) = all_153_0_112 % 27.18/7.56 | (303) mem(all_78_1_87, all_0_5_5) = all_153_1_113 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (264), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (304) all_123_1_98 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (304) can reduce 251 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (251) ~ (all_123_1_98 = 0) % 27.18/7.56 | (307) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_57_0_78) = v1 & mem(all_78_1_87, all_0_20_20) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (307) with all_158_0_114, all_158_1_115 yields: % 27.18/7.56 | (308) ~ (all_158_0_114 = 0) & ~ (all_158_1_115 = 0) & mem(all_78_1_87, all_57_0_78) = all_158_0_114 & mem(all_78_1_87, all_0_20_20) = all_158_1_115 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (308) yields: % 27.18/7.56 | (309) ~ (all_158_0_114 = 0) % 27.18/7.56 | (310) ~ (all_158_1_115 = 0) % 27.18/7.56 | (311) mem(all_78_1_87, all_57_0_78) = all_158_0_114 % 27.18/7.56 | (312) mem(all_78_1_87, all_0_20_20) = all_158_1_115 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (18) with all_147_1_111, all_0_9_9, all_0_21_21, all_0_10_10, all_78_1_87 and discharging atoms u(all_0_10_10, all_0_21_21) = all_0_9_9, mem(all_78_1_87, all_0_9_9) = all_147_1_111, yields: % 27.18/7.56 | (313) all_147_1_111 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_10_10) = v0 & mem(all_78_1_87, all_0_21_21) = v1) % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (44) with all_0_16_16, all_0_5_5, all_0_17_17, all_78_1_87 and discharging atoms u(all_0_17_17, all_0_5_5) = all_0_16_16, mem(all_78_1_87, all_0_16_16) = 0, yields: % 27.18/7.56 | (314) ? [v0] : ((v0 = 0 & mem(all_78_1_87, all_0_5_5) = 0) | (v0 = 0 & mem(all_78_1_87, all_0_17_17) = 0)) % 27.18/7.56 | % 27.18/7.56 | Instantiating (314) with all_165_0_116 yields: % 27.18/7.56 | (315) (all_165_0_116 = 0 & mem(all_78_1_87, all_0_5_5) = 0) | (all_165_0_116 = 0 & mem(all_78_1_87, all_0_17_17) = 0) % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (313), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (316) all_147_1_111 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (316) can reduce 292 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (292) ~ (all_147_1_111 = 0) % 27.18/7.56 | (319) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_10_10) = v0 & mem(all_78_1_87, all_0_21_21) = v1) % 27.18/7.56 | % 27.18/7.56 | Instantiating (319) with all_168_0_117, all_168_1_118 yields: % 27.18/7.56 | (320) ~ (all_168_0_117 = 0) & ~ (all_168_1_118 = 0) & mem(all_78_1_87, all_0_10_10) = all_168_1_118 & mem(all_78_1_87, all_0_21_21) = all_168_0_117 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (320) yields: % 27.18/7.56 | (321) ~ (all_168_0_117 = 0) % 27.18/7.56 | (322) ~ (all_168_1_118 = 0) % 27.18/7.56 | (323) mem(all_78_1_87, all_0_10_10) = all_168_1_118 % 27.18/7.56 | (324) mem(all_78_1_87, all_0_21_21) = all_168_0_117 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (315), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (325) all_165_0_116 = 0 & mem(all_78_1_87, all_0_5_5) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (325) yields: % 27.18/7.56 | (326) all_165_0_116 = 0 % 27.18/7.56 | (327) mem(all_78_1_87, all_0_5_5) = 0 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (63) with all_78_1_87, all_0_5_5, 0, all_153_1_113 and discharging atoms mem(all_78_1_87, all_0_5_5) = all_153_1_113, mem(all_78_1_87, all_0_5_5) = 0, yields: % 27.18/7.56 | (328) all_153_1_113 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (328) can reduce 301 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (330) all_165_0_116 = 0 & mem(all_78_1_87, all_0_17_17) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (330) yields: % 27.18/7.56 | (326) all_165_0_116 = 0 % 27.18/7.56 | (332) mem(all_78_1_87, all_0_17_17) = 0 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (44) with all_0_17_17, all_0_10_10, all_0_20_20, all_78_1_87 and discharging atoms u(all_0_20_20, all_0_10_10) = all_0_17_17, mem(all_78_1_87, all_0_17_17) = 0, yields: % 27.18/7.56 | (333) ? [v0] : ((v0 = 0 & mem(all_78_1_87, all_0_10_10) = 0) | (v0 = 0 & mem(all_78_1_87, all_0_20_20) = 0)) % 27.18/7.56 | % 27.18/7.56 | Instantiating (333) with all_179_0_119 yields: % 27.18/7.56 | (334) (all_179_0_119 = 0 & mem(all_78_1_87, all_0_10_10) = 0) | (all_179_0_119 = 0 & mem(all_78_1_87, all_0_20_20) = 0) % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (334), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (335) all_179_0_119 = 0 & mem(all_78_1_87, all_0_10_10) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (335) yields: % 27.18/7.56 | (336) all_179_0_119 = 0 % 27.18/7.56 | (337) mem(all_78_1_87, all_0_10_10) = 0 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (63) with all_78_1_87, all_0_10_10, 0, all_168_1_118 and discharging atoms mem(all_78_1_87, all_0_10_10) = all_168_1_118, mem(all_78_1_87, all_0_10_10) = 0, yields: % 27.18/7.56 | (338) all_168_1_118 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (338) can reduce 322 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (340) all_179_0_119 = 0 & mem(all_78_1_87, all_0_20_20) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (340) yields: % 27.18/7.56 | (336) all_179_0_119 = 0 % 27.18/7.56 | (342) mem(all_78_1_87, all_0_20_20) = 0 % 27.18/7.56 | % 27.18/7.56 | Instantiating formula (63) with all_78_1_87, all_0_20_20, 0, all_158_1_115 and discharging atoms mem(all_78_1_87, all_0_20_20) = all_158_1_115, mem(all_78_1_87, all_0_20_20) = 0, yields: % 27.18/7.56 | (343) all_158_1_115 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (343) can reduce 310 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (345) all_89_0_88 = 0 & mem(all_78_1_87, all_0_18_18) = 0 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (345) yields: % 27.18/7.56 | (243) all_89_0_88 = 0 % 27.18/7.56 | (347) mem(all_78_1_87, all_0_18_18) = 0 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (240), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (245) all_106_0_95 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (245) can reduce 230 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (230) ~ (all_106_0_95 = 0) % 27.18/7.56 | (248) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_3_3) = v1 & mem(all_78_1_87, all_0_6_6) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (248) with all_123_0_120, all_123_1_121 yields: % 27.18/7.56 | (352) ~ (all_123_0_120 = 0) & ~ (all_123_1_121 = 0) & mem(all_78_1_87, all_0_3_3) = all_123_0_120 & mem(all_78_1_87, all_0_6_6) = all_123_1_121 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (352) yields: % 27.18/7.56 | (353) ~ (all_123_0_120 = 0) % 27.18/7.56 | (354) ~ (all_123_1_121 = 0) % 27.18/7.56 | (355) mem(all_78_1_87, all_0_3_3) = all_123_0_120 % 27.18/7.56 | (356) mem(all_78_1_87, all_0_6_6) = all_123_1_121 % 27.18/7.56 | % 27.18/7.56 +-Applying beta-rule and splitting (241), into two cases. % 27.18/7.56 |-Branch one: % 27.18/7.56 | (254) all_106_1_96 = 0 % 27.18/7.56 | % 27.18/7.56 | Equations (254) can reduce 231 to: % 27.18/7.56 | (188) $false % 27.18/7.56 | % 27.18/7.56 |-The branch is then unsatisfiable % 27.18/7.56 |-Branch two: % 27.18/7.56 | (231) ~ (all_106_1_96 = 0) % 27.18/7.56 | (257) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_0_8_8) = v1 & mem(all_78_1_87, all_0_11_11) = v0) % 27.18/7.56 | % 27.18/7.56 | Instantiating (257) with all_128_0_122, all_128_1_123 yields: % 27.18/7.56 | (361) ~ (all_128_0_122 = 0) & ~ (all_128_1_123 = 0) & mem(all_78_1_87, all_0_8_8) = all_128_0_122 & mem(all_78_1_87, all_0_11_11) = all_128_1_123 % 27.18/7.56 | % 27.18/7.56 | Applying alpha-rule on (361) yields: % 27.18/7.56 | (362) ~ (all_128_0_122 = 0) % 27.18/7.57 | (363) ~ (all_128_1_123 = 0) % 27.18/7.57 | (364) mem(all_78_1_87, all_0_8_8) = all_128_0_122 % 27.18/7.57 | (365) mem(all_78_1_87, all_0_11_11) = all_128_1_123 % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (18) with all_123_1_121, all_0_6_6, all_57_0_78, all_0_20_20, all_78_1_87 and discharging atoms u(all_0_20_20, all_57_0_78) = all_0_6_6, mem(all_78_1_87, all_0_6_6) = all_123_1_121, yields: % 27.18/7.57 | (366) all_123_1_121 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_57_0_78) = v1 & mem(all_78_1_87, all_0_20_20) = v0) % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (18) with all_128_0_122, all_0_8_8, all_100_0_94, all_0_9_9, all_78_1_87 and discharging atoms u(all_0_9_9, all_100_0_94) = all_0_8_8, mem(all_78_1_87, all_0_8_8) = all_128_0_122, yields: % 27.18/7.57 | (367) all_128_0_122 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_100_0_94) = v1 & mem(all_78_1_87, all_0_9_9) = v0) % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (44) with all_0_18_18, all_57_0_78, all_0_21_21, all_78_1_87 and discharging atoms u(all_0_21_21, all_57_0_78) = all_0_18_18, mem(all_78_1_87, all_0_18_18) = 0, yields: % 27.18/7.57 | (368) ? [v0] : ((v0 = 0 & mem(all_78_1_87, all_57_0_78) = 0) | (v0 = 0 & mem(all_78_1_87, all_0_21_21) = 0)) % 27.18/7.57 | % 27.18/7.57 | Instantiating (368) with all_135_0_124 yields: % 27.18/7.57 | (369) (all_135_0_124 = 0 & mem(all_78_1_87, all_57_0_78) = 0) | (all_135_0_124 = 0 & mem(all_78_1_87, all_0_21_21) = 0) % 27.18/7.57 | % 27.18/7.57 +-Applying beta-rule and splitting (366), into two cases. % 27.18/7.57 |-Branch one: % 27.18/7.57 | (370) all_123_1_121 = 0 % 27.18/7.57 | % 27.18/7.57 | Equations (370) can reduce 354 to: % 27.18/7.57 | (188) $false % 27.18/7.57 | % 27.18/7.57 |-The branch is then unsatisfiable % 27.18/7.57 |-Branch two: % 27.18/7.57 | (354) ~ (all_123_1_121 = 0) % 27.18/7.57 | (307) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_57_0_78) = v1 & mem(all_78_1_87, all_0_20_20) = v0) % 27.18/7.57 | % 27.18/7.57 | Instantiating (307) with all_149_0_129, all_149_1_130 yields: % 27.18/7.57 | (374) ~ (all_149_0_129 = 0) & ~ (all_149_1_130 = 0) & mem(all_78_1_87, all_57_0_78) = all_149_0_129 & mem(all_78_1_87, all_0_20_20) = all_149_1_130 % 27.18/7.57 | % 27.18/7.57 | Applying alpha-rule on (374) yields: % 27.18/7.57 | (375) ~ (all_149_0_129 = 0) % 27.18/7.57 | (376) ~ (all_149_1_130 = 0) % 27.18/7.57 | (377) mem(all_78_1_87, all_57_0_78) = all_149_0_129 % 27.18/7.57 | (378) mem(all_78_1_87, all_0_20_20) = all_149_1_130 % 27.18/7.57 | % 27.18/7.57 +-Applying beta-rule and splitting (367), into two cases. % 27.18/7.57 |-Branch one: % 27.18/7.57 | (379) all_128_0_122 = 0 % 27.18/7.57 | % 27.18/7.57 | Equations (379) can reduce 362 to: % 27.18/7.57 | (188) $false % 27.18/7.57 | % 27.18/7.57 |-The branch is then unsatisfiable % 27.18/7.57 |-Branch two: % 27.18/7.57 | (362) ~ (all_128_0_122 = 0) % 27.18/7.57 | (289) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_78_1_87, all_100_0_94) = v1 & mem(all_78_1_87, all_0_9_9) = v0) % 27.18/7.57 | % 27.18/7.57 | Instantiating (289) with all_154_0_131, all_154_1_132 yields: % 27.18/7.57 | (383) ~ (all_154_0_131 = 0) & ~ (all_154_1_132 = 0) & mem(all_78_1_87, all_100_0_94) = all_154_0_131 & mem(all_78_1_87, all_0_9_9) = all_154_1_132 % 27.18/7.57 | % 27.18/7.57 | Applying alpha-rule on (383) yields: % 27.18/7.57 | (384) ~ (all_154_0_131 = 0) % 27.18/7.57 | (385) ~ (all_154_1_132 = 0) % 27.18/7.57 | (386) mem(all_78_1_87, all_100_0_94) = all_154_0_131 % 27.18/7.57 | (387) mem(all_78_1_87, all_0_9_9) = all_154_1_132 % 27.18/7.57 | % 27.18/7.57 +-Applying beta-rule and splitting (369), into two cases. % 27.18/7.57 |-Branch one: % 27.18/7.57 | (388) all_135_0_124 = 0 & mem(all_78_1_87, all_57_0_78) = 0 % 27.18/7.57 | % 27.18/7.57 | Applying alpha-rule on (388) yields: % 27.18/7.57 | (389) all_135_0_124 = 0 % 27.18/7.57 | (390) mem(all_78_1_87, all_57_0_78) = 0 % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (63) with all_78_1_87, all_57_0_78, 0, all_149_0_129 and discharging atoms mem(all_78_1_87, all_57_0_78) = all_149_0_129, mem(all_78_1_87, all_57_0_78) = 0, yields: % 27.18/7.57 | (391) all_149_0_129 = 0 % 27.18/7.57 | % 27.18/7.57 | Equations (391) can reduce 375 to: % 27.18/7.57 | (188) $false % 27.18/7.57 | % 27.18/7.57 |-The branch is then unsatisfiable % 27.18/7.57 |-Branch two: % 27.18/7.57 | (393) all_135_0_124 = 0 & mem(all_78_1_87, all_0_21_21) = 0 % 27.18/7.57 | % 27.18/7.57 | Applying alpha-rule on (393) yields: % 27.18/7.57 | (389) all_135_0_124 = 0 % 27.18/7.57 | (395) mem(all_78_1_87, all_0_21_21) = 0 % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (113) with all_0_21_21, all_0_22_22, all_78_1_87 and discharging atoms s(all_0_22_22) = all_0_21_21, mem(all_78_1_87, all_0_21_21) = 0, yields: % 27.18/7.57 | (396) all_78_1_87 = all_0_22_22 % 27.18/7.57 | % 27.18/7.57 | From (396) and (387) follows: % 27.18/7.57 | (397) mem(all_0_22_22, all_0_9_9) = all_154_1_132 % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (18) with all_154_1_132, all_0_9_9, all_0_21_21, all_0_10_10, all_0_22_22 and discharging atoms u(all_0_10_10, all_0_21_21) = all_0_9_9, mem(all_0_22_22, all_0_9_9) = all_154_1_132, yields: % 27.18/7.57 | (398) all_154_1_132 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_22_22, all_0_10_10) = v0 & mem(all_0_22_22, all_0_21_21) = v1) % 27.18/7.57 | % 27.18/7.57 +-Applying beta-rule and splitting (398), into two cases. % 27.18/7.57 |-Branch one: % 27.18/7.57 | (399) all_154_1_132 = 0 % 27.18/7.57 | % 27.18/7.57 | Equations (399) can reduce 385 to: % 27.18/7.57 | (188) $false % 27.18/7.57 | % 27.18/7.57 |-The branch is then unsatisfiable % 27.18/7.57 |-Branch two: % 27.18/7.57 | (385) ~ (all_154_1_132 = 0) % 27.18/7.57 | (402) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_22_22, all_0_10_10) = v0 & mem(all_0_22_22, all_0_21_21) = v1) % 27.18/7.57 | % 27.18/7.57 | Instantiating (402) with all_171_0_133, all_171_1_134 yields: % 27.18/7.57 | (403) ~ (all_171_0_133 = 0) & ~ (all_171_1_134 = 0) & mem(all_0_22_22, all_0_10_10) = all_171_1_134 & mem(all_0_22_22, all_0_21_21) = all_171_0_133 % 27.18/7.57 | % 27.18/7.57 | Applying alpha-rule on (403) yields: % 27.18/7.57 | (404) ~ (all_171_0_133 = 0) % 27.18/7.57 | (405) ~ (all_171_1_134 = 0) % 27.18/7.57 | (406) mem(all_0_22_22, all_0_10_10) = all_171_1_134 % 27.18/7.57 | (407) mem(all_0_22_22, all_0_21_21) = all_171_0_133 % 27.18/7.57 | % 27.18/7.57 | Instantiating formula (137) with all_171_0_133, all_0_21_21, all_0_22_22 and discharging atoms s(all_0_22_22) = all_0_21_21, mem(all_0_22_22, all_0_21_21) = all_171_0_133, yields: % 27.18/7.57 | (408) all_171_0_133 = 0 % 27.18/7.57 | % 27.18/7.57 | Equations (408) can reduce 404 to: % 27.18/7.57 | (188) $false % 27.18/7.57 | % 27.18/7.57 |-The branch is then unsatisfiable % 27.18/7.57 % SZS output end Proof for theBenchmark % 27.18/7.57 % 27.18/7.57 6956ms %------------------------------------------------------------------------------