%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV582+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Apr 1 02:01:03 AM UTC 2025 % Result : Theorem 23.05s 6.86s % Output : Proof 24.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEV582+1 : TPTP v9.1.0. Released v9.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n005.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Mar 31 13:15:43 EDT 2025 % 0.12/0.33 % CPUTime : % 0.60/0.57 ____ _ % 0.60/0.57 ___ / __ \_____(_)___ ________ __________ % 0.60/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.60/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.60/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.60/0.57 % 0.60/0.57 A Theorem Prover for First-Order Logic % 0.60/0.57 (ePrincess v.1.0) % 0.60/0.57 % 0.60/0.57 (c) Philipp Rümmer, 2009-2015 % 0.60/0.57 (c) Peter Backeman, 2014-2015 % 0.60/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.60/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.60/0.57 Bug reports to peter@backeman.se % 0.60/0.57 % 0.60/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.60/0.57 % 0.60/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.60/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.68/0.95 Prover 0: Preprocessing ... % 2.49/1.21 Prover 0: Warning: ignoring some quantifiers % 2.65/1.24 Prover 0: Constructing countermodel ... % 18.79/5.92 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.86/5.98 Prover 1: Preprocessing ... % 20.00/6.17 Prover 1: Constructing countermodel ... % 22.03/6.65 Prover 1: gave up % 22.03/6.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 22.03/6.68 Prover 2: Preprocessing ... % 22.69/6.78 Prover 2: Warning: ignoring some quantifiers % 22.69/6.79 Prover 2: Constructing countermodel ... % 23.05/6.86 Prover 2: proved (206ms) % 23.05/6.86 Prover 0: stopped % 23.05/6.86 % 23.05/6.86 No countermodel exists, formula is valid % 23.05/6.86 % SZS status Theorem for theBenchmark % 23.05/6.86 % 23.05/6.86 Generating proof ... Warning: ignoring some quantifiers % 24.38/7.19 found it (size 95) % 24.38/7.19 % 24.38/7.19 % SZS output start Proof for theBenchmark % 24.38/7.19 Assumed formulas after preprocessing and simplification: % 24.38/7.19 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ( ~ (v18 = 0) & p(v7) = v15 & n(v1) = v4 & n(v0) = v7 & n(e) = v0 & a(v12, v8) = v13 & a(v3, v5) = v6 & a(v1, v15) = v16 & a(v1, v2) = v3 & u(v14, v16) = v17 & u(v11, v13) = v14 & u(v6, v9) = v10 & u(v0, v4) = v5 & s(v8) = v9 & s(v7) = v8 & s(v5) = v11 & s(v2) = v12 & s(v1) = v2 & s(v0) = v1 & subq(v10, v17) = v18 & ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = 0 | ~ (m(v20, v21) = v22) | ~ (mem(v19, v22) = v23) | ? [v24] : ((v24 = 0 & mem(v19, v21) = 0) | ( ~ (v24 = 0) & mem(v19, v20) = v24))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = 0 | ~ (u(v20, v21) = v22) | ~ (mem(v19, v22) = v23) | ? [v24] : ? [v25] : ( ~ (v25 = 0) & ~ (v24 = 0) & mem(v19, v21) = v25 & mem(v19, v20) = v24)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast16p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast15p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast15p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast14p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast14p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast13p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast13p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast12p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast12p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast11p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast11p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast10p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast10p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast9p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast9p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast8p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast8p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast7p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast7p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast6p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast6p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast5p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast5p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast4p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast4p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast3p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (atleast3p(v19) = v20) | ~ (subq(v19, v21) = v22) | ? [v23] : (( ~ (v23 = 0) & atleast2p(v21) = v23) | ( ~ (v23 = 0) & subq(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | ~ (p(v20) = v21) | ~ (mem(v19, v21) = v22) | ? [v23] : ( ~ (v23 = 0) & subq(v19, v20) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | ~ (subq(v19, v20) = 0) | ~ (mem(v21, v20) = v22) | ? [v23] : ( ~ (v23 = 0) & mem(v21, v19) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (a(v22, v21) = v20) | ~ (a(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (m(v22, v21) = v20) | ~ (m(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (u(v22, v21) = v20) | ~ (u(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (disj(v22, v21) = v20) | ~ (disj(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (subq(v22, v21) = v20) | ~ (subq(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (mem(v22, v21) = v20) | ~ (mem(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = 0 | ~ (atleast2p(v19) = v20) | ~ (p(v21) = v22) | ? [v23] : ((v23 = 0 & subq(v19, v22) = 0) | ( ~ (v23 = 0) & mem(v21, v19) = v23))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : ( ~ (m(v20, v21) = v22) | ~ (mem(v19, v22) = 0) | ? [v23] : ( ~ (v23 = 0) & mem(v19, v21) = v23 & mem(v19, v20) = 0)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : ( ~ (u(v20, v21) = v22) | ~ (mem(v19, v22) = 0) | ? [v23] : ((v23 = 0 & mem(v19, v21) = 0) | (v23 = 0 & mem(v19, v20) = 0))) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : ( ~ (u(v19, v21) = v22) | ~ (s(v20) = v21) | a(v19, v20) = v22) & ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (s(v19) = v20) | ~ (mem(v19, v20) = v21)) & ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (disj(v19, v20) = v21) | ? [v22] : (mem(v22, v20) = 0 & mem(v22, v19) = 0)) & ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (subq(v19, v20) = v21) | ? [v22] : ? [v23] : ( ~ (v23 = 0) & p(v20) = v22 & mem(v19, v22) = v23)) & ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (subq(v19, v20) = v21) | ? [v22] : ? [v23] : ( ~ (v23 = 0) & mem(v22, v20) = v23 & mem(v22, v19) = 0)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast16p(v21) = v20) | ~ (atleast16p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast15p(v21) = v20) | ~ (atleast15p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast14p(v21) = v20) | ~ (atleast14p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast13p(v21) = v20) | ~ (atleast13p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast12p(v21) = v20) | ~ (atleast12p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast11p(v21) = v20) | ~ (atleast11p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast10p(v21) = v20) | ~ (atleast10p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast9p(v21) = v20) | ~ (atleast9p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast8p(v21) = v20) | ~ (atleast8p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast7p(v21) = v20) | ~ (atleast7p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast6p(v21) = v20) | ~ (atleast6p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast5p(v21) = v20) | ~ (atleast5p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast4p(v21) = v20) | ~ (atleast4p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast3p(v21) = v20) | ~ (atleast3p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (atleast2p(v21) = v20) | ~ (atleast2p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (p(v21) = v20) | ~ (p(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (n(v21) = v20) | ~ (n(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (s(v21) = v20) | ~ (s(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (s(v20) = v21) | ~ (mem(v19, v21) = 0)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast16p(v19) = v20) | ~ (atleast15p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast16p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast15p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast15p(v19) = v20) | ~ (atleast14p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast15p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast14p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast14p(v19) = v20) | ~ (atleast13p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast14p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast13p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast13p(v19) = v20) | ~ (atleast12p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast13p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast12p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast12p(v19) = v20) | ~ (atleast11p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast12p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast11p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast11p(v19) = v20) | ~ (atleast10p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast11p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast10p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast10p(v19) = v20) | ~ (atleast9p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast10p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast9p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast9p(v19) = v20) | ~ (atleast8p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast9p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast8p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast8p(v19) = v20) | ~ (atleast7p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast8p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast7p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast7p(v19) = v20) | ~ (atleast6p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast7p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast6p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast6p(v19) = v20) | ~ (atleast5p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast6p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast5p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast5p(v19) = v20) | ~ (atleast4p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast5p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast4p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast4p(v19) = v20) | ~ (atleast3p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast4p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast3p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast3p(v19) = v20) | ~ (atleast2p(v21) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & subq(v21, v19) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast3p(v19) = v20) | ~ (subq(v21, v19) = 0) | ? [v22] : ((v22 = 0 & subq(v19, v21) = 0) | ( ~ (v22 = 0) & atleast2p(v21) = v22))) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (atleast2p(v19) = v20) | ~ (mem(v21, v19) = 0) | ? [v22] : (p(v21) = v22 & subq(v19, v22) = 0)) & ! [v19] : ! [v20] : ! [v21] : ( ~ (p(v20) = v21) | ~ (mem(v19, v21) = 0) | subq(v19, v20) = 0) & ! [v19] : ! [v20] : ! [v21] : ( ~ (a(v19, v20) = v21) | ? [v22] : (u(v19, v22) = v21 & s(v20) = v22)) & ! [v19] : ! [v20] : ! [v21] : ( ~ (disj(v19, v20) = 0) | ~ (mem(v21, v20) = 0) | ? [v22] : ( ~ (v22 = 0) & mem(v21, v19) = v22)) & ! [v19] : ! [v20] : ! [v21] : ( ~ (disj(v19, v20) = 0) | ~ (mem(v21, v19) = 0) | ? [v22] : ( ~ (v22 = 0) & mem(v21, v20) = v22)) & ! [v19] : ! [v20] : ! [v21] : ( ~ (subq(v19, v20) = 0) | ~ (mem(v21, v19) = 0) | mem(v21, v20) = 0) & ! [v19] : ! [v20] : (v20 = v19 | ~ (subq(v20, v19) = 0) | ? [v21] : ( ~ (v21 = 0) & subq(v19, v20) = v21)) & ! [v19] : ! [v20] : (v20 = v19 | ~ (subq(v19, v20) = 0) | ? [v21] : ( ~ (v21 = 0) & subq(v20, v19) = v21)) & ! [v19] : ! [v20] : ( ~ (n(v19) = v20) | a(v19, v19) = v20) & ! [v19] : ! [v20] : ( ~ (a(v19, v19) = v20) | n(v19) = v20) & ! [v19] : ! [v20] : ( ~ (subq(v19, v20) = 0) | ? [v21] : (p(v20) = v21 & mem(v19, v21) = 0)) & ! [v19] : ( ~ (atleast16p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast15p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast15p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast14p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast14p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast13p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast13p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast12p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast12p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast11p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast11p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast10p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast10p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast9p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast9p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast8p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast8p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast7p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast7p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast6p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast6p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast5p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast5p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast4p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast4p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast3p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast3p(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & atleast2p(v20) = 0 & subq(v20, v19) = 0 & subq(v19, v20) = v21)) & ! [v19] : ( ~ (atleast2p(v19) = 0) | ? [v20] : ? [v21] : ? [v22] : ( ~ (v22 = 0) & p(v20) = v21 & subq(v19, v21) = v22 & mem(v20, v19) = 0)) & ! [v19] : ~ (mem(v19, e) = 0) & ? [v19] : ? [v20] : ? [v21] : a(v20, v19) = v21 & ? [v19] : ? [v20] : ? [v21] : m(v20, v19) = v21 & ? [v19] : ? [v20] : ? [v21] : u(v20, v19) = v21 & ? [v19] : ? [v20] : ? [v21] : disj(v20, v19) = v21 & ? [v19] : ? [v20] : ? [v21] : subq(v20, v19) = v21 & ? [v19] : ? [v20] : ? [v21] : mem(v20, v19) = v21 & ? [v19] : ? [v20] : atleast16p(v19) = v20 & ? [v19] : ? [v20] : atleast15p(v19) = v20 & ? [v19] : ? [v20] : atleast14p(v19) = v20 & ? [v19] : ? [v20] : atleast13p(v19) = v20 & ? [v19] : ? [v20] : atleast12p(v19) = v20 & ? [v19] : ? [v20] : atleast11p(v19) = v20 & ? [v19] : ? [v20] : atleast10p(v19) = v20 & ? [v19] : ? [v20] : atleast9p(v19) = v20 & ? [v19] : ? [v20] : atleast8p(v19) = v20 & ? [v19] : ? [v20] : atleast7p(v19) = v20 & ? [v19] : ? [v20] : atleast6p(v19) = v20 & ? [v19] : ? [v20] : atleast5p(v19) = v20 & ? [v19] : ? [v20] : atleast4p(v19) = v20 & ? [v19] : ? [v20] : atleast3p(v19) = v20 & ? [v19] : ? [v20] : atleast2p(v19) = v20 & ? [v19] : ? [v20] : p(v19) = v20 & ? [v19] : ? [v20] : n(v19) = v20 & ? [v19] : ? [v20] : s(v19) = v20) % 24.75/7.26 | 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 yields: % 24.75/7.26 | (1) ~ (all_0_0_0 = 0) & p(all_0_11_11) = all_0_3_3 & n(all_0_17_17) = all_0_14_14 & n(all_0_18_18) = all_0_11_11 & n(e) = all_0_18_18 & a(all_0_6_6, all_0_10_10) = all_0_5_5 & a(all_0_15_15, all_0_13_13) = all_0_12_12 & a(all_0_17_17, all_0_3_3) = all_0_2_2 & a(all_0_17_17, all_0_16_16) = all_0_15_15 & u(all_0_4_4, all_0_2_2) = all_0_1_1 & u(all_0_7_7, all_0_5_5) = all_0_4_4 & u(all_0_12_12, all_0_9_9) = all_0_8_8 & u(all_0_18_18, all_0_14_14) = all_0_13_13 & s(all_0_10_10) = all_0_9_9 & s(all_0_11_11) = all_0_10_10 & s(all_0_13_13) = all_0_7_7 & s(all_0_16_16) = all_0_6_6 & s(all_0_17_17) = all_0_16_16 & s(all_0_18_18) = all_0_17_17 & subq(all_0_8_8, 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 % 24.95/7.29 | % 24.95/7.29 | Applying alpha-rule on (1) yields: % 24.95/7.29 | (2) u(all_0_12_12, all_0_9_9) = all_0_8_8 % 24.95/7.29 | (3) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.29 | (4) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 24.95/7.29 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast15p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.29 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.29 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 24.95/7.29 | (8) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.29 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 24.95/7.29 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast6p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.29 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 24.95/7.29 | (12) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 24.95/7.30 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 24.95/7.30 | (15) s(all_0_17_17) = all_0_16_16 % 24.95/7.30 | (16) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 24.95/7.30 | (18) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 24.95/7.30 | (19) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.30 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 24.95/7.30 | (22) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 24.95/7.30 | (23) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (24) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 24.95/7.30 | (26) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 24.95/7.30 | (27) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 24.95/7.30 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast12p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.30 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 24.95/7.30 | (30) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 24.95/7.30 | (31) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.30 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 24.95/7.30 | (33) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.30 | (34) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 24.95/7.30 | (35) ? [v0] : ? [v1] : p(v0) = v1 % 24.95/7.30 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.30 | (37) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 24.95/7.30 | (38) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 24.95/7.30 | (39) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 24.95/7.30 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 24.95/7.30 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 24.95/7.30 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast3p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.30 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast7p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.30 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.31 | (45) s(all_0_16_16) = all_0_6_6 % 24.95/7.31 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 24.95/7.31 | (47) u(all_0_18_18, all_0_14_14) = all_0_13_13 % 24.95/7.31 | (48) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 24.95/7.31 | (49) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 24.95/7.31 | (50) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 24.95/7.31 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 24.95/7.31 | (52) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 24.95/7.31 | (53) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 24.95/7.31 | (54) u(all_0_4_4, all_0_2_2) = all_0_1_1 % 24.95/7.31 | (55) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 24.95/7.31 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 24.95/7.31 | (57) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 24.95/7.31 | (58) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 24.95/7.31 | (59) a(all_0_6_6, all_0_10_10) = all_0_5_5 % 24.95/7.31 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast9p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.31 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 24.95/7.31 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 24.95/7.31 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.31 | (64) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 24.95/7.31 | (66) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (67) ~ (all_0_0_0 = 0) % 24.95/7.31 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast10p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.31 | (69) s(all_0_13_13) = all_0_7_7 % 24.95/7.31 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast14p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.31 | (71) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 24.95/7.31 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 24.95/7.31 | (73) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (74) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 24.95/7.31 | (75) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast8p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.31 | (77) a(all_0_17_17, all_0_3_3) = all_0_2_2 % 24.95/7.31 | (78) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 24.95/7.31 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 24.95/7.31 | (81) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 24.95/7.31 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.31 | (83) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 24.95/7.31 | (84) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 24.95/7.31 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 24.95/7.31 | (86) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 24.95/7.31 | (87) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.32 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 24.95/7.32 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ? [v4] : ((v4 = 0 & subq(v0, v3) = 0) | ( ~ (v4 = 0) & mem(v2, v0) = v4))) % 24.95/7.32 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.32 | (91) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 24.95/7.32 | (92) a(all_0_17_17, all_0_16_16) = all_0_15_15 % 24.95/7.32 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 24.95/7.32 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 24.95/7.32 | (95) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 24.95/7.32 | (96) ? [v0] : ? [v1] : s(v0) = v1 % 24.95/7.32 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 24.95/7.32 | (98) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & ~ (v5 = 0) & mem(v0, v2) = v6 & mem(v0, v1) = v5)) % 24.95/7.32 | (99) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 24.95/7.32 | (100) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 24.95/7.32 | (101) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.32 | (102) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 24.95/7.32 | (103) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 24.95/7.32 | (104) s(all_0_18_18) = all_0_17_17 % 24.95/7.32 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast4p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.32 | (106) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 24.95/7.32 | (107) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast11p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.32 | (108) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 24.95/7.32 | (109) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast13p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.32 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ((v4 = 0 & mem(v0, v2) = 0) | (v4 = 0 & mem(v0, v1) = 0))) % 24.95/7.32 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 24.95/7.32 | (112) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 24.95/7.32 | (113) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 24.95/7.32 | (114) n(e) = all_0_18_18 % 24.95/7.32 | (115) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast2p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.32 | (116) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 24.95/7.32 | (117) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 24.95/7.32 | (118) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 24.95/7.32 | (119) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 24.95/7.32 | (120) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 24.95/7.32 | (121) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 24.95/7.32 | (122) n(all_0_18_18) = all_0_11_11 % 24.95/7.32 | (123) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 24.95/7.32 | (124) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.32 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & atleast5p(v2) = v4) | ( ~ (v4 = 0) & subq(v2, v0) = v4))) % 24.95/7.32 | (126) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 24.95/7.32 | (127) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.32 | (128) s(all_0_10_10) = all_0_9_9 % 24.95/7.32 | (129) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 24.95/7.32 | (130) ? [v0] : ? [v1] : n(v0) = v1 % 24.95/7.32 | (131) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 24.95/7.32 | (132) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 24.95/7.32 | (133) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.33 | (134) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 24.95/7.33 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 24.95/7.33 | (136) s(all_0_11_11) = all_0_10_10 % 24.95/7.33 | (137) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 24.95/7.33 | (138) subq(all_0_8_8, all_0_1_1) = all_0_0_0 % 24.95/7.33 | (139) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 24.95/7.33 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 24.95/7.33 | (141) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 24.95/7.33 | (142) a(all_0_15_15, all_0_13_13) = all_0_12_12 % 24.95/7.33 | (143) p(all_0_11_11) = all_0_3_3 % 24.95/7.33 | (144) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 24.95/7.33 | (145) n(all_0_17_17) = all_0_14_14 % 24.95/7.33 | (146) ! [v0] : ~ (mem(v0, e) = 0) % 24.95/7.33 | (147) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 24.95/7.33 | (148) u(all_0_7_7, all_0_5_5) = all_0_4_4 % 24.95/7.33 | (149) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ((v5 = 0 & mem(v0, v2) = 0) | ( ~ (v5 = 0) & mem(v0, v1) = v5))) % 24.95/7.33 | (150) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 24.95/7.33 | (151) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (108) with all_0_5_5, all_0_10_10, all_0_6_6 and discharging atoms a(all_0_6_6, all_0_10_10) = all_0_5_5, yields: % 24.95/7.33 | (152) ? [v0] : (u(all_0_6_6, v0) = all_0_5_5 & s(all_0_10_10) = v0) % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (108) with all_0_12_12, all_0_13_13, all_0_15_15 and discharging atoms a(all_0_15_15, all_0_13_13) = all_0_12_12, yields: % 24.95/7.33 | (153) ? [v0] : (u(all_0_15_15, v0) = all_0_12_12 & s(all_0_13_13) = v0) % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (108) with all_0_2_2, all_0_3_3, all_0_17_17 and discharging atoms a(all_0_17_17, all_0_3_3) = all_0_2_2, yields: % 24.95/7.33 | (154) ? [v0] : (u(all_0_17_17, v0) = all_0_2_2 & s(all_0_3_3) = v0) % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (108) with all_0_15_15, all_0_16_16, all_0_17_17 and discharging atoms a(all_0_17_17, all_0_16_16) = all_0_15_15, yields: % 24.95/7.33 | (155) ? [v0] : (u(all_0_17_17, v0) = all_0_15_15 & s(all_0_16_16) = v0) % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (84) with all_0_0_0, all_0_1_1, all_0_8_8 and discharging atoms subq(all_0_8_8, all_0_1_1) = all_0_0_0, yields: % 24.95/7.33 | (156) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_8_8, v0) = v1) % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (55) with all_0_0_0, all_0_1_1, all_0_8_8 and discharging atoms subq(all_0_8_8, all_0_1_1) = all_0_0_0, yields: % 24.95/7.33 | (157) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_8_8) = 0) % 24.95/7.33 | % 24.95/7.33 | Instantiating (154) with all_57_0_73 yields: % 24.95/7.33 | (158) u(all_0_17_17, all_57_0_73) = all_0_2_2 & s(all_0_3_3) = all_57_0_73 % 24.95/7.33 | % 24.95/7.33 | Applying alpha-rule on (158) yields: % 24.95/7.33 | (159) u(all_0_17_17, all_57_0_73) = all_0_2_2 % 24.95/7.33 | (160) s(all_0_3_3) = all_57_0_73 % 24.95/7.33 | % 24.95/7.33 | Instantiating (153) with all_59_0_74 yields: % 24.95/7.33 | (161) u(all_0_15_15, all_59_0_74) = all_0_12_12 & s(all_0_13_13) = all_59_0_74 % 24.95/7.33 | % 24.95/7.33 | Applying alpha-rule on (161) yields: % 24.95/7.33 | (162) u(all_0_15_15, all_59_0_74) = all_0_12_12 % 24.95/7.33 | (163) s(all_0_13_13) = all_59_0_74 % 24.95/7.33 | % 24.95/7.33 | Instantiating (155) with all_61_0_75 yields: % 24.95/7.33 | (164) u(all_0_17_17, all_61_0_75) = all_0_15_15 & s(all_0_16_16) = all_61_0_75 % 24.95/7.33 | % 24.95/7.33 | Applying alpha-rule on (164) yields: % 24.95/7.33 | (165) u(all_0_17_17, all_61_0_75) = all_0_15_15 % 24.95/7.33 | (166) s(all_0_16_16) = all_61_0_75 % 24.95/7.33 | % 24.95/7.33 | Instantiating (152) with all_63_0_76 yields: % 24.95/7.33 | (167) u(all_0_6_6, all_63_0_76) = all_0_5_5 & s(all_0_10_10) = all_63_0_76 % 24.95/7.33 | % 24.95/7.33 | Applying alpha-rule on (167) yields: % 24.95/7.33 | (168) u(all_0_6_6, all_63_0_76) = all_0_5_5 % 24.95/7.33 | (169) s(all_0_10_10) = all_63_0_76 % 24.95/7.33 | % 24.95/7.33 +-Applying beta-rule and splitting (156), into two cases. % 24.95/7.33 |-Branch one: % 24.95/7.33 | (170) all_0_0_0 = 0 % 24.95/7.33 | % 24.95/7.33 | Equations (170) can reduce 67 to: % 24.95/7.33 | (171) $false % 24.95/7.33 | % 24.95/7.33 |-The branch is then unsatisfiable % 24.95/7.33 |-Branch two: % 24.95/7.33 | (67) ~ (all_0_0_0 = 0) % 24.95/7.33 | (173) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_8_8, v0) = v1) % 24.95/7.33 | % 24.95/7.33 +-Applying beta-rule and splitting (157), into two cases. % 24.95/7.33 |-Branch one: % 24.95/7.33 | (170) all_0_0_0 = 0 % 24.95/7.33 | % 24.95/7.33 | Equations (170) can reduce 67 to: % 24.95/7.33 | (171) $false % 24.95/7.33 | % 24.95/7.33 |-The branch is then unsatisfiable % 24.95/7.33 |-Branch two: % 24.95/7.33 | (67) ~ (all_0_0_0 = 0) % 24.95/7.33 | (177) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_8_8) = 0) % 24.95/7.33 | % 24.95/7.33 | Instantiating (177) with all_74_0_79, all_74_1_80 yields: % 24.95/7.33 | (178) ~ (all_74_0_79 = 0) & mem(all_74_1_80, all_0_1_1) = all_74_0_79 & mem(all_74_1_80, all_0_8_8) = 0 % 24.95/7.33 | % 24.95/7.33 | Applying alpha-rule on (178) yields: % 24.95/7.33 | (179) ~ (all_74_0_79 = 0) % 24.95/7.33 | (180) mem(all_74_1_80, all_0_1_1) = all_74_0_79 % 24.95/7.33 | (181) mem(all_74_1_80, all_0_8_8) = 0 % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (137) with all_0_10_10, all_63_0_76, all_0_9_9 and discharging atoms s(all_0_10_10) = all_63_0_76, s(all_0_10_10) = all_0_9_9, yields: % 24.95/7.33 | (182) all_63_0_76 = all_0_9_9 % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (137) with all_0_13_13, all_59_0_74, all_0_7_7 and discharging atoms s(all_0_13_13) = all_59_0_74, s(all_0_13_13) = all_0_7_7, yields: % 24.95/7.33 | (183) all_59_0_74 = all_0_7_7 % 24.95/7.33 | % 24.95/7.33 | Instantiating formula (137) with all_0_16_16, all_61_0_75, all_0_6_6 and discharging atoms s(all_0_16_16) = all_61_0_75, s(all_0_16_16) = all_0_6_6, yields: % 24.95/7.33 | (184) all_61_0_75 = all_0_6_6 % 24.95/7.33 | % 24.95/7.33 | From (182) and (168) follows: % 24.95/7.34 | (185) u(all_0_6_6, all_0_9_9) = all_0_5_5 % 24.95/7.34 | % 24.95/7.34 | From (183) and (162) follows: % 24.95/7.34 | (186) u(all_0_15_15, all_0_7_7) = all_0_12_12 % 24.95/7.34 | % 24.95/7.34 | From (184) and (165) follows: % 24.95/7.34 | (187) u(all_0_17_17, all_0_6_6) = all_0_15_15 % 24.95/7.34 | % 24.95/7.34 | From (182) and (169) follows: % 24.95/7.34 | (128) s(all_0_10_10) = all_0_9_9 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (98) with all_74_0_79, all_0_1_1, all_0_2_2, all_0_4_4, all_74_1_80 and discharging atoms u(all_0_4_4, all_0_2_2) = all_0_1_1, mem(all_74_1_80, all_0_1_1) = all_74_0_79, yields: % 24.95/7.34 | (189) all_74_0_79 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_2_2) = v1 & mem(all_74_1_80, all_0_4_4) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (110) with all_0_8_8, all_0_9_9, all_0_12_12, all_74_1_80 and discharging atoms u(all_0_12_12, all_0_9_9) = all_0_8_8, mem(all_74_1_80, all_0_8_8) = 0, yields: % 24.95/7.34 | (190) ? [v0] : ((v0 = 0 & mem(all_74_1_80, all_0_9_9) = 0) | (v0 = 0 & mem(all_74_1_80, all_0_12_12) = 0)) % 24.95/7.34 | % 24.95/7.34 | Instantiating (190) with all_85_0_81 yields: % 24.95/7.34 | (191) (all_85_0_81 = 0 & mem(all_74_1_80, all_0_9_9) = 0) | (all_85_0_81 = 0 & mem(all_74_1_80, all_0_12_12) = 0) % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (189), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (192) all_74_0_79 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (192) can reduce 179 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (179) ~ (all_74_0_79 = 0) % 24.95/7.34 | (195) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_2_2) = v1 & mem(all_74_1_80, all_0_4_4) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating (195) with all_96_0_85, all_96_1_86 yields: % 24.95/7.34 | (196) ~ (all_96_0_85 = 0) & ~ (all_96_1_86 = 0) & mem(all_74_1_80, all_0_2_2) = all_96_0_85 & mem(all_74_1_80, all_0_4_4) = all_96_1_86 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (196) yields: % 24.95/7.34 | (197) ~ (all_96_0_85 = 0) % 24.95/7.34 | (198) ~ (all_96_1_86 = 0) % 24.95/7.34 | (199) mem(all_74_1_80, all_0_2_2) = all_96_0_85 % 24.95/7.34 | (200) mem(all_74_1_80, all_0_4_4) = all_96_1_86 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (98) with all_96_0_85, all_0_2_2, all_57_0_73, all_0_17_17, all_74_1_80 and discharging atoms u(all_0_17_17, all_57_0_73) = all_0_2_2, mem(all_74_1_80, all_0_2_2) = all_96_0_85, yields: % 24.95/7.34 | (201) all_96_0_85 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_57_0_73) = v1 & mem(all_74_1_80, all_0_17_17) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (98) with all_96_1_86, all_0_4_4, all_0_5_5, all_0_7_7, all_74_1_80 and discharging atoms u(all_0_7_7, all_0_5_5) = all_0_4_4, mem(all_74_1_80, all_0_4_4) = all_96_1_86, yields: % 24.95/7.34 | (202) all_96_1_86 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_5_5) = v1 & mem(all_74_1_80, all_0_7_7) = v0) % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (191), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (203) all_85_0_81 = 0 & mem(all_74_1_80, all_0_9_9) = 0 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (203) yields: % 24.95/7.34 | (204) all_85_0_81 = 0 % 24.95/7.34 | (205) mem(all_74_1_80, all_0_9_9) = 0 % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (202), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (206) all_96_1_86 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (206) can reduce 198 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (198) ~ (all_96_1_86 = 0) % 24.95/7.34 | (209) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_5_5) = v1 & mem(all_74_1_80, all_0_7_7) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating (209) with all_118_0_89, all_118_1_90 yields: % 24.95/7.34 | (210) ~ (all_118_0_89 = 0) & ~ (all_118_1_90 = 0) & mem(all_74_1_80, all_0_5_5) = all_118_0_89 & mem(all_74_1_80, all_0_7_7) = all_118_1_90 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (210) yields: % 24.95/7.34 | (211) ~ (all_118_0_89 = 0) % 24.95/7.34 | (212) ~ (all_118_1_90 = 0) % 24.95/7.34 | (213) mem(all_74_1_80, all_0_5_5) = all_118_0_89 % 24.95/7.34 | (214) mem(all_74_1_80, all_0_7_7) = all_118_1_90 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (74) with all_0_9_9, all_0_10_10, all_74_1_80 and discharging atoms s(all_0_10_10) = all_0_9_9, mem(all_74_1_80, all_0_9_9) = 0, yields: % 24.95/7.34 | (215) all_74_1_80 = all_0_10_10 % 24.95/7.34 | % 24.95/7.34 | From (215) and (213) follows: % 24.95/7.34 | (216) mem(all_0_10_10, all_0_5_5) = all_118_0_89 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (98) with all_118_0_89, all_0_5_5, all_0_9_9, all_0_6_6, all_0_10_10 and discharging atoms u(all_0_6_6, all_0_9_9) = all_0_5_5, mem(all_0_10_10, all_0_5_5) = all_118_0_89, yields: % 24.95/7.34 | (217) all_118_0_89 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_10_10, all_0_6_6) = v0 & mem(all_0_10_10, all_0_9_9) = v1) % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (217), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (218) all_118_0_89 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (218) can reduce 211 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (211) ~ (all_118_0_89 = 0) % 24.95/7.34 | (221) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_0_10_10, all_0_6_6) = v0 & mem(all_0_10_10, all_0_9_9) = v1) % 24.95/7.34 | % 24.95/7.34 | Instantiating (221) with all_131_0_91, all_131_1_92 yields: % 24.95/7.34 | (222) ~ (all_131_0_91 = 0) & ~ (all_131_1_92 = 0) & mem(all_0_10_10, all_0_6_6) = all_131_1_92 & mem(all_0_10_10, all_0_9_9) = all_131_0_91 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (222) yields: % 24.95/7.34 | (223) ~ (all_131_0_91 = 0) % 24.95/7.34 | (224) ~ (all_131_1_92 = 0) % 24.95/7.34 | (225) mem(all_0_10_10, all_0_6_6) = all_131_1_92 % 24.95/7.34 | (226) mem(all_0_10_10, all_0_9_9) = all_131_0_91 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (102) with all_131_0_91, all_0_9_9, all_0_10_10 and discharging atoms s(all_0_10_10) = all_0_9_9, mem(all_0_10_10, all_0_9_9) = all_131_0_91, yields: % 24.95/7.34 | (227) all_131_0_91 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (227) can reduce 223 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (229) all_85_0_81 = 0 & mem(all_74_1_80, all_0_12_12) = 0 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (229) yields: % 24.95/7.34 | (204) all_85_0_81 = 0 % 24.95/7.34 | (231) mem(all_74_1_80, all_0_12_12) = 0 % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (201), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (232) all_96_0_85 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (232) can reduce 197 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (197) ~ (all_96_0_85 = 0) % 24.95/7.34 | (235) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_57_0_73) = v1 & mem(all_74_1_80, all_0_17_17) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating (235) with all_113_0_93, all_113_1_94 yields: % 24.95/7.34 | (236) ~ (all_113_0_93 = 0) & ~ (all_113_1_94 = 0) & mem(all_74_1_80, all_57_0_73) = all_113_0_93 & mem(all_74_1_80, all_0_17_17) = all_113_1_94 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (236) yields: % 24.95/7.34 | (237) ~ (all_113_0_93 = 0) % 24.95/7.34 | (238) ~ (all_113_1_94 = 0) % 24.95/7.34 | (239) mem(all_74_1_80, all_57_0_73) = all_113_0_93 % 24.95/7.34 | (240) mem(all_74_1_80, all_0_17_17) = all_113_1_94 % 24.95/7.34 | % 24.95/7.34 +-Applying beta-rule and splitting (202), into two cases. % 24.95/7.34 |-Branch one: % 24.95/7.34 | (206) all_96_1_86 = 0 % 24.95/7.34 | % 24.95/7.34 | Equations (206) can reduce 198 to: % 24.95/7.34 | (171) $false % 24.95/7.34 | % 24.95/7.34 |-The branch is then unsatisfiable % 24.95/7.34 |-Branch two: % 24.95/7.34 | (198) ~ (all_96_1_86 = 0) % 24.95/7.34 | (209) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_5_5) = v1 & mem(all_74_1_80, all_0_7_7) = v0) % 24.95/7.34 | % 24.95/7.34 | Instantiating (209) with all_118_0_95, all_118_1_96 yields: % 24.95/7.34 | (245) ~ (all_118_0_95 = 0) & ~ (all_118_1_96 = 0) & mem(all_74_1_80, all_0_5_5) = all_118_0_95 & mem(all_74_1_80, all_0_7_7) = all_118_1_96 % 24.95/7.34 | % 24.95/7.34 | Applying alpha-rule on (245) yields: % 24.95/7.34 | (246) ~ (all_118_0_95 = 0) % 24.95/7.34 | (247) ~ (all_118_1_96 = 0) % 24.95/7.34 | (248) mem(all_74_1_80, all_0_5_5) = all_118_0_95 % 24.95/7.34 | (249) mem(all_74_1_80, all_0_7_7) = all_118_1_96 % 24.95/7.34 | % 24.95/7.34 | Instantiating formula (98) with all_118_0_95, all_0_5_5, all_0_9_9, all_0_6_6, all_74_1_80 and discharging atoms u(all_0_6_6, all_0_9_9) = all_0_5_5, mem(all_74_1_80, all_0_5_5) = all_118_0_95, yields: % 24.95/7.34 | (250) all_118_0_95 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_6_6) = v0 & mem(all_74_1_80, all_0_9_9) = v1) % 24.95/7.34 | % 24.95/7.35 | Instantiating formula (110) with all_0_12_12, all_0_7_7, all_0_15_15, all_74_1_80 and discharging atoms u(all_0_15_15, all_0_7_7) = all_0_12_12, mem(all_74_1_80, all_0_12_12) = 0, yields: % 24.95/7.35 | (251) ? [v0] : ((v0 = 0 & mem(all_74_1_80, all_0_7_7) = 0) | (v0 = 0 & mem(all_74_1_80, all_0_15_15) = 0)) % 24.95/7.35 | % 24.95/7.35 | Instantiating (251) with all_125_0_97 yields: % 24.95/7.35 | (252) (all_125_0_97 = 0 & mem(all_74_1_80, all_0_7_7) = 0) | (all_125_0_97 = 0 & mem(all_74_1_80, all_0_15_15) = 0) % 24.95/7.35 | % 24.95/7.35 +-Applying beta-rule and splitting (250), into two cases. % 24.95/7.35 |-Branch one: % 24.95/7.35 | (253) all_118_0_95 = 0 % 24.95/7.35 | % 24.95/7.35 | Equations (253) can reduce 246 to: % 24.95/7.35 | (171) $false % 24.95/7.35 | % 24.95/7.35 |-The branch is then unsatisfiable % 24.95/7.35 |-Branch two: % 24.95/7.35 | (246) ~ (all_118_0_95 = 0) % 24.95/7.35 | (256) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_80, all_0_6_6) = v0 & mem(all_74_1_80, all_0_9_9) = v1) % 24.95/7.35 | % 24.95/7.35 | Instantiating (256) with all_128_0_98, all_128_1_99 yields: % 24.95/7.35 | (257) ~ (all_128_0_98 = 0) & ~ (all_128_1_99 = 0) & mem(all_74_1_80, all_0_6_6) = all_128_1_99 & mem(all_74_1_80, all_0_9_9) = all_128_0_98 % 24.95/7.35 | % 24.95/7.35 | Applying alpha-rule on (257) yields: % 24.95/7.35 | (258) ~ (all_128_0_98 = 0) % 24.95/7.35 | (259) ~ (all_128_1_99 = 0) % 24.95/7.35 | (260) mem(all_74_1_80, all_0_6_6) = all_128_1_99 % 24.95/7.35 | (261) mem(all_74_1_80, all_0_9_9) = all_128_0_98 % 24.95/7.35 | % 24.95/7.35 +-Applying beta-rule and splitting (252), into two cases. % 24.95/7.35 |-Branch one: % 24.95/7.35 | (262) all_125_0_97 = 0 & mem(all_74_1_80, all_0_7_7) = 0 % 24.95/7.35 | % 24.95/7.35 | Applying alpha-rule on (262) yields: % 24.95/7.35 | (263) all_125_0_97 = 0 % 24.95/7.35 | (264) mem(all_74_1_80, all_0_7_7) = 0 % 24.95/7.35 | % 24.95/7.35 | Instantiating formula (131) with all_74_1_80, all_0_7_7, 0, all_118_1_96 and discharging atoms mem(all_74_1_80, all_0_7_7) = all_118_1_96, mem(all_74_1_80, all_0_7_7) = 0, yields: % 24.95/7.35 | (265) all_118_1_96 = 0 % 24.95/7.35 | % 24.95/7.35 | Equations (265) can reduce 247 to: % 24.95/7.35 | (171) $false % 24.95/7.35 | % 24.95/7.35 |-The branch is then unsatisfiable % 24.95/7.35 |-Branch two: % 24.95/7.35 | (267) all_125_0_97 = 0 & mem(all_74_1_80, all_0_15_15) = 0 % 24.95/7.35 | % 24.95/7.35 | Applying alpha-rule on (267) yields: % 24.95/7.35 | (263) all_125_0_97 = 0 % 24.95/7.35 | (269) mem(all_74_1_80, all_0_15_15) = 0 % 24.95/7.35 | % 24.95/7.35 | Instantiating formula (110) with all_0_15_15, all_0_6_6, all_0_17_17, all_74_1_80 and discharging atoms u(all_0_17_17, all_0_6_6) = all_0_15_15, mem(all_74_1_80, all_0_15_15) = 0, yields: % 24.95/7.35 | (270) ? [v0] : ((v0 = 0 & mem(all_74_1_80, all_0_6_6) = 0) | (v0 = 0 & mem(all_74_1_80, all_0_17_17) = 0)) % 24.95/7.35 | % 24.95/7.35 | Instantiating (270) with all_139_0_100 yields: % 24.95/7.35 | (271) (all_139_0_100 = 0 & mem(all_74_1_80, all_0_6_6) = 0) | (all_139_0_100 = 0 & mem(all_74_1_80, all_0_17_17) = 0) % 24.95/7.35 | % 24.95/7.35 +-Applying beta-rule and splitting (271), into two cases. % 24.95/7.35 |-Branch one: % 24.95/7.35 | (272) all_139_0_100 = 0 & mem(all_74_1_80, all_0_6_6) = 0 % 24.95/7.35 | % 24.95/7.35 | Applying alpha-rule on (272) yields: % 24.95/7.35 | (273) all_139_0_100 = 0 % 24.95/7.35 | (274) mem(all_74_1_80, all_0_6_6) = 0 % 24.95/7.35 | % 24.95/7.35 | Instantiating formula (131) with all_74_1_80, all_0_6_6, 0, all_128_1_99 and discharging atoms mem(all_74_1_80, all_0_6_6) = all_128_1_99, mem(all_74_1_80, all_0_6_6) = 0, yields: % 24.95/7.35 | (275) all_128_1_99 = 0 % 24.95/7.35 | % 24.95/7.35 | Equations (275) can reduce 259 to: % 24.95/7.35 | (171) $false % 24.95/7.35 | % 24.95/7.35 |-The branch is then unsatisfiable % 24.95/7.35 |-Branch two: % 24.95/7.35 | (277) all_139_0_100 = 0 & mem(all_74_1_80, all_0_17_17) = 0 % 24.95/7.35 | % 24.95/7.35 | Applying alpha-rule on (277) yields: % 24.95/7.35 | (273) all_139_0_100 = 0 % 24.95/7.35 | (279) mem(all_74_1_80, all_0_17_17) = 0 % 24.95/7.35 | % 24.95/7.35 | Instantiating formula (131) with all_74_1_80, all_0_17_17, 0, all_113_1_94 and discharging atoms mem(all_74_1_80, all_0_17_17) = all_113_1_94, mem(all_74_1_80, all_0_17_17) = 0, yields: % 24.95/7.35 | (280) all_113_1_94 = 0 % 24.95/7.35 | % 24.95/7.35 | Equations (280) can reduce 238 to: % 24.95/7.35 | (171) $false % 24.95/7.35 | % 24.95/7.35 |-The branch is then unsatisfiable % 24.95/7.35 % SZS output end Proof for theBenchmark % 24.95/7.35 % 24.95/7.35 6765ms %------------------------------------------------------------------------------