%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV578+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n004.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 33.96s 8.95s % Output : Proof 37.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEV578+1 : TPTP v9.1.0. Released v9.1.0. % 0.11/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n004.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Mon Mar 31 13:05:25 EDT 2025 % 0.13/0.34 % CPUTime : % 0.57/0.62 ____ _ % 0.57/0.62 ___ / __ \_____(_)___ ________ __________ % 0.57/0.62 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.62 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.62 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.62 % 0.57/0.62 A Theorem Prover for First-Order Logic % 0.57/0.62 (ePrincess v.1.0) % 0.57/0.62 % 0.57/0.62 (c) Philipp Rümmer, 2009-2015 % 0.57/0.62 (c) Peter Backeman, 2014-2015 % 0.57/0.62 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.62 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.62 Bug reports to peter@backeman.se % 0.57/0.62 % 0.57/0.62 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.62 % 0.57/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.63/0.69 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.75/1.04 Prover 0: Preprocessing ... % 2.46/1.37 Prover 0: Warning: ignoring some quantifiers % 2.93/1.41 Prover 0: Constructing countermodel ... % 21.51/5.98 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 21.84/6.03 Prover 1: Preprocessing ... % 22.94/6.22 Prover 1: Constructing countermodel ... % 32.57/8.58 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 32.70/8.62 Prover 2: Preprocessing ... % 33.29/8.78 Prover 2: Warning: ignoring some quantifiers % 33.29/8.79 Prover 2: Constructing countermodel ... % 33.96/8.95 Prover 2: proved (371ms) % 33.96/8.95 Prover 1: stopped % 33.96/8.95 Prover 0: stopped % 33.96/8.95 % 33.96/8.95 No countermodel exists, formula is valid % 33.96/8.95 % SZS status Theorem for theBenchmark % 33.96/8.95 % 33.96/8.95 Generating proof ... Warning: ignoring some quantifiers % 36.25/9.44 found it (size 193) % 36.25/9.44 % 36.25/9.44 % SZS output start Proof for theBenchmark % 36.25/9.44 Assumed formulas after preprocessing and simplification: % 36.25/9.44 | (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(v5) = v18 & p(v1) = v5 & n(v11) = v12 & n(v3) = v17 & n(v1) = v2 & n(v0) = v7 & n(e) = v0 & a(v18, v8) = v19 & a(v13, v14) = v15 & a(v6, v8) = v9 & a(v1, v7) = v14 & u(v20, v21) = v22 & u(v17, v19) = v20 & u(v10, v15) = v16 & u(v4, v9) = v10 & u(v1, v12) = v13 & u(v0, v2) = v3 & s(v14) = v21 & s(v7) = v8 & s(v5) = v6 & s(v3) = v4 & s(v1) = v11 & s(v0) = v1 & subq(v16, 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) % 36.60/9.53 | 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: % 36.60/9.53 | (1) ~ (all_0_0_0 = 0) & p(all_0_18_18) = all_0_5_5 & p(all_0_22_22) = all_0_18_18 & n(all_0_12_12) = all_0_11_11 & n(all_0_20_20) = all_0_6_6 & n(all_0_22_22) = all_0_21_21 & n(all_0_23_23) = all_0_16_16 & n(e) = all_0_23_23 & a(all_0_5_5, all_0_15_15) = all_0_4_4 & a(all_0_10_10, all_0_9_9) = all_0_8_8 & a(all_0_17_17, all_0_15_15) = all_0_14_14 & a(all_0_22_22, all_0_16_16) = all_0_9_9 & u(all_0_3_3, all_0_2_2) = all_0_1_1 & u(all_0_6_6, all_0_4_4) = all_0_3_3 & u(all_0_13_13, all_0_8_8) = all_0_7_7 & u(all_0_19_19, all_0_14_14) = all_0_13_13 & u(all_0_22_22, all_0_11_11) = all_0_10_10 & u(all_0_23_23, all_0_21_21) = all_0_20_20 & s(all_0_9_9) = all_0_2_2 & s(all_0_16_16) = all_0_15_15 & s(all_0_18_18) = all_0_17_17 & s(all_0_20_20) = all_0_19_19 & s(all_0_22_22) = all_0_12_12 & s(all_0_23_23) = all_0_22_22 & subq(all_0_7_7, 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 % 36.60/9.57 | % 36.60/9.57 | Applying alpha-rule on (1) yields: % 36.60/9.57 | (2) ! [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))) % 36.60/9.57 | (3) s(all_0_16_16) = all_0_15_15 % 36.60/9.57 | (4) ? [v0] : ? [v1] : atleast13p(v0) = v1 % 36.60/9.57 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 36.60/9.57 | (6) ? [v0] : ? [v1] : atleast12p(v0) = v1 % 36.60/9.57 | (7) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 36.60/9.57 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 36.60/9.57 | (9) ? [v0] : ? [v1] : atleast9p(v0) = v1 % 36.60/9.57 | (10) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v1) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v0) = v3)) % 36.60/9.57 | (11) ? [v0] : ? [v1] : atleast10p(v0) = v1 % 36.60/9.57 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast3p(v2) = v3))) % 36.60/9.57 | (13) a(all_0_22_22, all_0_16_16) = all_0_9_9 % 36.60/9.57 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 36.60/9.57 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 36.60/9.57 | (16) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast6p(v2) = v3))) % 36.60/9.57 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast2p(v2) = v3))) % 36.60/9.57 | (18) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 36.60/9.57 | (19) s(all_0_22_22) = all_0_12_12 % 36.60/9.57 | (20) a(all_0_5_5, all_0_15_15) = all_0_4_4 % 36.60/9.57 | (21) ? [v0] : ? [v1] : ? [v2] : mem(v1, v0) = v2 % 36.60/9.57 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 36.60/9.57 | (23) ! [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))) % 36.60/9.57 | (24) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 36.60/9.57 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 36.60/9.57 | (26) a(all_0_17_17, all_0_15_15) = all_0_14_14 % 36.60/9.57 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 36.60/9.57 | (28) ? [v0] : ? [v1] : atleast7p(v0) = v1 % 36.60/9.57 | (29) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 36.60/9.57 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast8p(v2) = v3))) % 36.60/9.57 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 36.60/9.58 | (32) ! [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))) % 36.60/9.58 | (33) ! [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))) % 36.60/9.58 | (34) u(all_0_22_22, all_0_11_11) = all_0_10_10 % 36.60/9.58 | (35) ? [v0] : ? [v1] : atleast14p(v0) = v1 % 36.60/9.58 | (36) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 36.60/9.58 | (37) ? [v0] : ? [v1] : ? [v2] : a(v1, v0) = v2 % 36.60/9.58 | (38) ? [v0] : ? [v1] : atleast11p(v0) = v1 % 36.60/9.58 | (39) ? [v0] : ? [v1] : atleast4p(v0) = v1 % 36.60/9.58 | (40) ? [v0] : ? [v1] : atleast8p(v0) = v1 % 36.60/9.58 | (41) ? [v0] : ? [v1] : ? [v2] : subq(v1, v0) = v2 % 36.60/9.58 | (42) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 36.60/9.58 | (43) n(all_0_20_20) = all_0_6_6 % 36.60/9.58 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 36.60/9.58 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 36.60/9.58 | (46) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 36.60/9.58 | (47) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4)) % 36.60/9.58 | (48) subq(all_0_7_7, all_0_1_1) = all_0_0_0 % 36.60/9.58 | (49) ! [v0] : ~ (mem(v0, e) = 0) % 36.60/9.58 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) % 36.60/9.58 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 36.60/9.58 | (52) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 36.60/9.58 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 37.00/9.58 | (54) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.00/9.58 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.00/9.58 | (56) n(all_0_22_22) = all_0_21_21 % 37.00/9.58 | (57) s(all_0_18_18) = all_0_17_17 % 37.00/9.58 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 37.00/9.58 | (59) ! [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)) % 37.00/9.58 | (60) p(all_0_22_22) = all_0_18_18 % 37.00/9.58 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast7p(v2) = v3))) % 37.00/9.58 | (62) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 37.00/9.58 | (63) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.00/9.58 | (64) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 37.00/9.58 | (65) ! [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))) % 37.00/9.59 | (66) ! [v0] : ! [v1] : ( ~ (subq(v0, v1) = 0) | ? [v2] : (p(v1) = v2 & mem(v0, v2) = 0)) % 37.00/9.59 | (67) ! [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))) % 37.00/9.59 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.00/9.59 | (69) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 37.00/9.59 | (70) ! [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))) % 37.00/9.59 | (71) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 37.00/9.59 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.00/9.59 | (73) ? [v0] : ? [v1] : atleast3p(v0) = v1 % 37.00/9.59 | (74) a(all_0_10_10, all_0_9_9) = all_0_8_8 % 37.00/9.59 | (75) ? [v0] : ? [v1] : ? [v2] : m(v1, v0) = v2 % 37.00/9.59 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 37.00/9.59 | (77) ! [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))) % 37.00/9.59 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 37.00/9.59 | (79) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast12p(v2) = v3))) % 37.00/9.59 | (80) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.00/9.59 | (81) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.00/9.59 | (82) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 37.00/9.59 | (83) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 37.00/9.59 | (84) ! [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))) % 37.00/9.59 | (85) ? [v0] : ? [v1] : n(v0) = v1 % 37.00/9.59 | (86) ? [v0] : ? [v1] : atleast5p(v0) = v1 % 37.00/9.59 | (87) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.00/9.59 | (88) ? [v0] : ? [v1] : p(v0) = v1 % 37.00/9.59 | (89) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v0, v1) = v2)) % 37.00/9.59 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast4p(v2) = v3))) % 37.05/9.59 | (91) p(all_0_18_18) = all_0_5_5 % 37.05/9.59 | (92) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.05/9.59 | (93) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.05/9.59 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast13p(v2) = v3))) % 37.05/9.59 | (95) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.05/9.59 | (96) s(all_0_9_9) = all_0_2_2 % 37.05/9.60 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast15p(v2) = v3))) % 37.05/9.60 | (98) ! [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))) % 37.05/9.60 | (99) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ? [v3] : (p(v2) = v3 & subq(v0, v3) = 0)) % 37.05/9.60 | (100) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 37.05/9.60 | (101) ? [v0] : ? [v1] : ? [v2] : disj(v1, v0) = v2 % 37.05/9.60 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 37.05/9.60 | (103) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 37.05/9.60 | (104) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast5p(v2) = v3))) % 37.05/9.60 | (105) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.05/9.60 | (106) ! [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))) % 37.05/9.60 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.05/9.60 | (108) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 37.05/9.60 | (109) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 37.05/9.60 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 37.05/9.60 | (111) n(all_0_12_12) = all_0_11_11 % 37.05/9.60 | (112) ~ (all_0_0_0 = 0) % 37.05/9.60 | (113) n(e) = all_0_23_23 % 37.05/9.60 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 37.05/9.60 | (115) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.05/9.60 | (116) n(all_0_23_23) = all_0_16_16 % 37.05/9.60 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 37.05/9.60 | (118) ? [v0] : ? [v1] : atleast16p(v0) = v1 % 37.05/9.60 | (119) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.05/9.60 | (120) u(all_0_6_6, all_0_4_4) = all_0_3_3 % 37.05/9.60 | (121) ? [v0] : ? [v1] : atleast6p(v0) = v1 % 37.05/9.60 | (122) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast9p(v2) = v3))) % 37.05/9.60 | (123) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.05/9.60 | (124) ? [v0] : ? [v1] : atleast2p(v0) = v1 % 37.05/9.60 | (125) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.05/9.60 | (126) ! [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))) % 37.05/9.60 | (127) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast10p(v2) = v3))) % 37.05/9.60 | (128) ! [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))) % 37.05/9.61 | (129) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 37.05/9.61 | (130) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 37.05/9.61 | (131) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast11p(v2) = v3))) % 37.05/9.61 | (132) s(all_0_23_23) = all_0_22_22 % 37.05/9.61 | (133) ! [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))) % 37.05/9.61 | (134) u(all_0_23_23, all_0_21_21) = all_0_20_20 % 37.05/9.61 | (135) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 37.05/9.61 | (136) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 37.05/9.61 | (137) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (subq(v2, v0) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & atleast14p(v2) = v3))) % 37.05/9.61 | (138) ? [v0] : ? [v1] : ? [v2] : u(v1, v0) = v2 % 37.05/9.61 | (139) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 37.05/9.61 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 37.11/9.61 | (141) u(all_0_13_13, all_0_8_8) = all_0_7_7 % 37.11/9.61 | (142) u(all_0_3_3, all_0_2_2) = all_0_1_1 % 37.11/9.61 | (143) u(all_0_19_19, all_0_14_14) = all_0_13_13 % 37.11/9.61 | (144) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 37.11/9.61 | (145) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 37.11/9.61 | (146) ? [v0] : ? [v1] : atleast15p(v0) = v1 % 37.11/9.61 | (147) ! [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))) % 37.11/9.61 | (148) ! [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))) % 37.11/9.61 | (149) ! [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))) % 37.11/9.61 | (150) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.11/9.61 | (151) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 37.11/9.61 | (152) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 37.11/9.61 | (153) s(all_0_20_20) = all_0_19_19 % 37.12/9.61 | (154) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ((v3 = 0 & subq(v0, v2) = 0) | ( ~ (v3 = 0) & subq(v2, v0) = v3))) % 37.12/9.61 | (155) ? [v0] : ? [v1] : s(v0) = v1 % 37.12/9.61 | (156) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 37.12/9.61 | % 37.12/9.61 | Instantiating formula (83) with all_0_11_11, all_0_12_12 and discharging atoms n(all_0_12_12) = all_0_11_11, yields: % 37.12/9.61 | (157) a(all_0_12_12, all_0_12_12) = all_0_11_11 % 37.12/9.61 | % 37.12/9.61 | Instantiating formula (83) with all_0_6_6, all_0_20_20 and discharging atoms n(all_0_20_20) = all_0_6_6, yields: % 37.12/9.61 | (158) a(all_0_20_20, all_0_20_20) = all_0_6_6 % 37.12/9.61 | % 37.12/9.61 | Instantiating formula (83) with all_0_21_21, all_0_22_22 and discharging atoms n(all_0_22_22) = all_0_21_21, yields: % 37.12/9.61 | (159) a(all_0_22_22, all_0_22_22) = all_0_21_21 % 37.12/9.61 | % 37.12/9.61 | Instantiating formula (108) with all_0_4_4, all_0_15_15, all_0_5_5 and discharging atoms a(all_0_5_5, all_0_15_15) = all_0_4_4, yields: % 37.12/9.61 | (160) ? [v0] : (u(all_0_5_5, v0) = all_0_4_4 & s(all_0_15_15) = v0) % 37.12/9.61 | % 37.12/9.61 | Instantiating formula (108) with all_0_8_8, all_0_9_9, all_0_10_10 and discharging atoms a(all_0_10_10, all_0_9_9) = all_0_8_8, yields: % 37.12/9.62 | (161) ? [v0] : (u(all_0_10_10, v0) = all_0_8_8 & s(all_0_9_9) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (108) with all_0_14_14, all_0_15_15, all_0_17_17 and discharging atoms a(all_0_17_17, all_0_15_15) = all_0_14_14, yields: % 37.12/9.62 | (162) ? [v0] : (u(all_0_17_17, v0) = all_0_14_14 & s(all_0_15_15) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (47) with all_0_0_0, all_0_1_1, all_0_7_7 and discharging atoms subq(all_0_7_7, all_0_1_1) = all_0_0_0, yields: % 37.12/9.62 | (163) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_7_7, v0) = v1) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (139) with all_0_0_0, all_0_1_1, all_0_7_7 and discharging atoms subq(all_0_7_7, all_0_1_1) = all_0_0_0, yields: % 37.12/9.62 | (164) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_7_7) = 0) % 37.12/9.62 | % 37.12/9.62 | Instantiating (162) with all_59_0_79 yields: % 37.12/9.62 | (165) u(all_0_17_17, all_59_0_79) = all_0_14_14 & s(all_0_15_15) = all_59_0_79 % 37.12/9.62 | % 37.12/9.62 | Applying alpha-rule on (165) yields: % 37.12/9.62 | (166) u(all_0_17_17, all_59_0_79) = all_0_14_14 % 37.12/9.62 | (167) s(all_0_15_15) = all_59_0_79 % 37.12/9.62 | % 37.12/9.62 | Instantiating (161) with all_61_0_80 yields: % 37.12/9.62 | (168) u(all_0_10_10, all_61_0_80) = all_0_8_8 & s(all_0_9_9) = all_61_0_80 % 37.12/9.62 | % 37.12/9.62 | Applying alpha-rule on (168) yields: % 37.12/9.62 | (169) u(all_0_10_10, all_61_0_80) = all_0_8_8 % 37.12/9.62 | (170) s(all_0_9_9) = all_61_0_80 % 37.12/9.62 | % 37.12/9.62 | Instantiating (160) with all_63_0_81 yields: % 37.12/9.62 | (171) u(all_0_5_5, all_63_0_81) = all_0_4_4 & s(all_0_15_15) = all_63_0_81 % 37.12/9.62 | % 37.12/9.62 | Applying alpha-rule on (171) yields: % 37.12/9.62 | (172) u(all_0_5_5, all_63_0_81) = all_0_4_4 % 37.12/9.62 | (173) s(all_0_15_15) = all_63_0_81 % 37.12/9.62 | % 37.12/9.62 +-Applying beta-rule and splitting (163), into two cases. % 37.12/9.62 |-Branch one: % 37.12/9.62 | (174) all_0_0_0 = 0 % 37.12/9.62 | % 37.12/9.62 | Equations (174) can reduce 112 to: % 37.12/9.62 | (175) $false % 37.12/9.62 | % 37.12/9.62 |-The branch is then unsatisfiable % 37.12/9.62 |-Branch two: % 37.12/9.62 | (112) ~ (all_0_0_0 = 0) % 37.12/9.62 | (177) ? [v0] : ? [v1] : ( ~ (v1 = 0) & p(all_0_1_1) = v0 & mem(all_0_7_7, v0) = v1) % 37.12/9.62 | % 37.12/9.62 +-Applying beta-rule and splitting (164), into two cases. % 37.12/9.62 |-Branch one: % 37.12/9.62 | (174) all_0_0_0 = 0 % 37.12/9.62 | % 37.12/9.62 | Equations (174) can reduce 112 to: % 37.12/9.62 | (175) $false % 37.12/9.62 | % 37.12/9.62 |-The branch is then unsatisfiable % 37.12/9.62 |-Branch two: % 37.12/9.62 | (112) ~ (all_0_0_0 = 0) % 37.12/9.62 | (181) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_7_7) = 0) % 37.12/9.62 | % 37.12/9.62 | Instantiating (181) with all_74_0_84, all_74_1_85 yields: % 37.12/9.62 | (182) ~ (all_74_0_84 = 0) & mem(all_74_1_85, all_0_1_1) = all_74_0_84 & mem(all_74_1_85, all_0_7_7) = 0 % 37.12/9.62 | % 37.12/9.62 | Applying alpha-rule on (182) yields: % 37.12/9.62 | (183) ~ (all_74_0_84 = 0) % 37.12/9.62 | (184) mem(all_74_1_85, all_0_1_1) = all_74_0_84 % 37.12/9.62 | (185) mem(all_74_1_85, all_0_7_7) = 0 % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (62) with all_0_9_9, all_61_0_80, all_0_2_2 and discharging atoms s(all_0_9_9) = all_61_0_80, s(all_0_9_9) = all_0_2_2, yields: % 37.12/9.62 | (186) all_61_0_80 = all_0_2_2 % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (62) with all_0_15_15, all_59_0_79, all_63_0_81 and discharging atoms s(all_0_15_15) = all_63_0_81, s(all_0_15_15) = all_59_0_79, yields: % 37.12/9.62 | (187) all_63_0_81 = all_59_0_79 % 37.12/9.62 | % 37.12/9.62 | From (187) and (172) follows: % 37.12/9.62 | (188) u(all_0_5_5, all_59_0_79) = all_0_4_4 % 37.12/9.62 | % 37.12/9.62 | From (186) and (169) follows: % 37.12/9.62 | (189) u(all_0_10_10, all_0_2_2) = all_0_8_8 % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (108) with all_0_11_11, all_0_12_12, all_0_12_12 and discharging atoms a(all_0_12_12, all_0_12_12) = all_0_11_11, yields: % 37.12/9.62 | (190) ? [v0] : (u(all_0_12_12, v0) = all_0_11_11 & s(all_0_12_12) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (108) with all_0_6_6, all_0_20_20, all_0_20_20 and discharging atoms a(all_0_20_20, all_0_20_20) = all_0_6_6, yields: % 37.12/9.62 | (191) ? [v0] : (u(all_0_20_20, v0) = all_0_6_6 & s(all_0_20_20) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (108) with all_0_21_21, all_0_22_22, all_0_22_22 and discharging atoms a(all_0_22_22, all_0_22_22) = all_0_21_21, yields: % 37.12/9.62 | (192) ? [v0] : (u(all_0_22_22, v0) = all_0_21_21 & s(all_0_22_22) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (59) with all_74_0_84, all_0_1_1, all_0_2_2, all_0_3_3, all_74_1_85 and discharging atoms u(all_0_3_3, all_0_2_2) = all_0_1_1, mem(all_74_1_85, all_0_1_1) = all_74_0_84, yields: % 37.12/9.62 | (193) all_74_0_84 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_2_2) = v1 & mem(all_74_1_85, all_0_3_3) = v0) % 37.12/9.62 | % 37.12/9.62 | Instantiating formula (126) with all_0_7_7, all_0_8_8, all_0_13_13, all_74_1_85 and discharging atoms u(all_0_13_13, all_0_8_8) = all_0_7_7, mem(all_74_1_85, all_0_7_7) = 0, yields: % 37.12/9.62 | (194) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_0_8_8) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_13_13) = 0)) % 37.12/9.63 | % 37.12/9.63 | Instantiating (194) with all_85_0_86 yields: % 37.12/9.63 | (195) (all_85_0_86 = 0 & mem(all_74_1_85, all_0_8_8) = 0) | (all_85_0_86 = 0 & mem(all_74_1_85, all_0_13_13) = 0) % 37.12/9.63 | % 37.12/9.63 | Instantiating (191) with all_88_0_88 yields: % 37.12/9.63 | (196) u(all_0_20_20, all_88_0_88) = all_0_6_6 & s(all_0_20_20) = all_88_0_88 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (196) yields: % 37.12/9.63 | (197) u(all_0_20_20, all_88_0_88) = all_0_6_6 % 37.12/9.63 | (198) s(all_0_20_20) = all_88_0_88 % 37.12/9.63 | % 37.12/9.63 | Instantiating (190) with all_90_0_89 yields: % 37.12/9.63 | (199) u(all_0_12_12, all_90_0_89) = all_0_11_11 & s(all_0_12_12) = all_90_0_89 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (199) yields: % 37.12/9.63 | (200) u(all_0_12_12, all_90_0_89) = all_0_11_11 % 37.12/9.63 | (201) s(all_0_12_12) = all_90_0_89 % 37.12/9.63 | % 37.12/9.63 | Instantiating (192) with all_92_0_90 yields: % 37.12/9.63 | (202) u(all_0_22_22, all_92_0_90) = all_0_21_21 & s(all_0_22_22) = all_92_0_90 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (202) yields: % 37.12/9.63 | (203) u(all_0_22_22, all_92_0_90) = all_0_21_21 % 37.12/9.63 | (204) s(all_0_22_22) = all_92_0_90 % 37.12/9.63 | % 37.12/9.63 +-Applying beta-rule and splitting (193), into two cases. % 37.12/9.63 |-Branch one: % 37.12/9.63 | (205) all_74_0_84 = 0 % 37.12/9.63 | % 37.12/9.63 | Equations (205) can reduce 183 to: % 37.12/9.63 | (175) $false % 37.12/9.63 | % 37.12/9.63 |-The branch is then unsatisfiable % 37.12/9.63 |-Branch two: % 37.12/9.63 | (183) ~ (all_74_0_84 = 0) % 37.12/9.63 | (208) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_2_2) = v1 & mem(all_74_1_85, all_0_3_3) = v0) % 37.12/9.63 | % 37.12/9.63 | Instantiating (208) with all_100_0_92, all_100_1_93 yields: % 37.12/9.63 | (209) ~ (all_100_0_92 = 0) & ~ (all_100_1_93 = 0) & mem(all_74_1_85, all_0_2_2) = all_100_0_92 & mem(all_74_1_85, all_0_3_3) = all_100_1_93 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (209) yields: % 37.12/9.63 | (210) ~ (all_100_0_92 = 0) % 37.12/9.63 | (211) ~ (all_100_1_93 = 0) % 37.12/9.63 | (212) mem(all_74_1_85, all_0_2_2) = all_100_0_92 % 37.12/9.63 | (213) mem(all_74_1_85, all_0_3_3) = all_100_1_93 % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (62) with all_0_20_20, all_88_0_88, all_0_19_19 and discharging atoms s(all_0_20_20) = all_88_0_88, s(all_0_20_20) = all_0_19_19, yields: % 37.12/9.63 | (214) all_88_0_88 = all_0_19_19 % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (62) with all_0_22_22, all_92_0_90, all_0_12_12 and discharging atoms s(all_0_22_22) = all_92_0_90, s(all_0_22_22) = all_0_12_12, yields: % 37.12/9.63 | (215) all_92_0_90 = all_0_12_12 % 37.12/9.63 | % 37.12/9.63 | From (214) and (197) follows: % 37.12/9.63 | (216) u(all_0_20_20, all_0_19_19) = all_0_6_6 % 37.12/9.63 | % 37.12/9.63 | From (215) and (203) follows: % 37.12/9.63 | (217) u(all_0_22_22, all_0_12_12) = all_0_21_21 % 37.12/9.63 | % 37.12/9.63 | From (215) and (204) follows: % 37.12/9.63 | (19) s(all_0_22_22) = all_0_12_12 % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (59) with all_100_1_93, all_0_3_3, all_0_4_4, all_0_6_6, all_74_1_85 and discharging atoms u(all_0_6_6, all_0_4_4) = all_0_3_3, mem(all_74_1_85, all_0_3_3) = all_100_1_93, yields: % 37.12/9.63 | (219) all_100_1_93 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_4_4) = v1 & mem(all_74_1_85, all_0_6_6) = v0) % 37.12/9.63 | % 37.12/9.63 +-Applying beta-rule and splitting (195), into two cases. % 37.12/9.63 |-Branch one: % 37.12/9.63 | (220) all_85_0_86 = 0 & mem(all_74_1_85, all_0_8_8) = 0 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (220) yields: % 37.12/9.63 | (221) all_85_0_86 = 0 % 37.12/9.63 | (222) mem(all_74_1_85, all_0_8_8) = 0 % 37.12/9.63 | % 37.12/9.63 +-Applying beta-rule and splitting (219), into two cases. % 37.12/9.63 |-Branch one: % 37.12/9.63 | (223) all_100_1_93 = 0 % 37.12/9.63 | % 37.12/9.63 | Equations (223) can reduce 211 to: % 37.12/9.63 | (175) $false % 37.12/9.63 | % 37.12/9.63 |-The branch is then unsatisfiable % 37.12/9.63 |-Branch two: % 37.12/9.63 | (211) ~ (all_100_1_93 = 0) % 37.12/9.63 | (226) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_4_4) = v1 & mem(all_74_1_85, all_0_6_6) = v0) % 37.12/9.63 | % 37.12/9.63 | Instantiating (226) with all_117_0_94, all_117_1_95 yields: % 37.12/9.63 | (227) ~ (all_117_0_94 = 0) & ~ (all_117_1_95 = 0) & mem(all_74_1_85, all_0_4_4) = all_117_0_94 & mem(all_74_1_85, all_0_6_6) = all_117_1_95 % 37.12/9.63 | % 37.12/9.63 | Applying alpha-rule on (227) yields: % 37.12/9.63 | (228) ~ (all_117_0_94 = 0) % 37.12/9.63 | (229) ~ (all_117_1_95 = 0) % 37.12/9.63 | (230) mem(all_74_1_85, all_0_4_4) = all_117_0_94 % 37.12/9.63 | (231) mem(all_74_1_85, all_0_6_6) = all_117_1_95 % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (59) with all_117_0_94, all_0_4_4, all_59_0_79, all_0_5_5, all_74_1_85 and discharging atoms u(all_0_5_5, all_59_0_79) = all_0_4_4, mem(all_74_1_85, all_0_4_4) = all_117_0_94, yields: % 37.12/9.63 | (232) all_117_0_94 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_59_0_79) = v1 & mem(all_74_1_85, all_0_5_5) = v0) % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (59) with all_117_1_95, all_0_6_6, all_0_19_19, all_0_20_20, all_74_1_85 and discharging atoms u(all_0_20_20, all_0_19_19) = all_0_6_6, mem(all_74_1_85, all_0_6_6) = all_117_1_95, yields: % 37.12/9.63 | (233) all_117_1_95 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_19_19) = v1 & mem(all_74_1_85, all_0_20_20) = v0) % 37.12/9.63 | % 37.12/9.63 | Instantiating formula (126) with all_0_8_8, all_0_2_2, all_0_10_10, all_74_1_85 and discharging atoms u(all_0_10_10, all_0_2_2) = all_0_8_8, mem(all_74_1_85, all_0_8_8) = 0, yields: % 37.12/9.63 | (234) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_0_2_2) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_10_10) = 0)) % 37.12/9.63 | % 37.12/9.63 | Instantiating (234) with all_124_0_96 yields: % 37.12/9.63 | (235) (all_124_0_96 = 0 & mem(all_74_1_85, all_0_2_2) = 0) | (all_124_0_96 = 0 & mem(all_74_1_85, all_0_10_10) = 0) % 37.12/9.63 | % 37.12/9.63 +-Applying beta-rule and splitting (233), into two cases. % 37.12/9.63 |-Branch one: % 37.12/9.63 | (236) all_117_1_95 = 0 % 37.12/9.63 | % 37.12/9.63 | Equations (236) can reduce 229 to: % 37.12/9.63 | (175) $false % 37.12/9.63 | % 37.12/9.63 |-The branch is then unsatisfiable % 37.12/9.63 |-Branch two: % 37.12/9.63 | (229) ~ (all_117_1_95 = 0) % 37.12/9.63 | (239) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_19_19) = v1 & mem(all_74_1_85, all_0_20_20) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating (239) with all_127_0_97, all_127_1_98 yields: % 37.12/9.64 | (240) ~ (all_127_0_97 = 0) & ~ (all_127_1_98 = 0) & mem(all_74_1_85, all_0_19_19) = all_127_0_97 & mem(all_74_1_85, all_0_20_20) = all_127_1_98 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (240) yields: % 37.12/9.64 | (241) ~ (all_127_0_97 = 0) % 37.12/9.64 | (242) ~ (all_127_1_98 = 0) % 37.12/9.64 | (243) mem(all_74_1_85, all_0_19_19) = all_127_0_97 % 37.12/9.64 | (244) mem(all_74_1_85, all_0_20_20) = all_127_1_98 % 37.12/9.64 | % 37.12/9.64 +-Applying beta-rule and splitting (235), into two cases. % 37.12/9.64 |-Branch one: % 37.12/9.64 | (245) all_124_0_96 = 0 & mem(all_74_1_85, all_0_2_2) = 0 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (245) yields: % 37.12/9.64 | (246) all_124_0_96 = 0 % 37.12/9.64 | (247) mem(all_74_1_85, all_0_2_2) = 0 % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (117) with all_74_1_85, all_0_2_2, 0, all_100_0_92 and discharging atoms mem(all_74_1_85, all_0_2_2) = all_100_0_92, mem(all_74_1_85, all_0_2_2) = 0, yields: % 37.12/9.64 | (248) all_100_0_92 = 0 % 37.12/9.64 | % 37.12/9.64 | Equations (248) can reduce 210 to: % 37.12/9.64 | (175) $false % 37.12/9.64 | % 37.12/9.64 |-The branch is then unsatisfiable % 37.12/9.64 |-Branch two: % 37.12/9.64 | (250) all_124_0_96 = 0 & mem(all_74_1_85, all_0_10_10) = 0 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (250) yields: % 37.12/9.64 | (246) all_124_0_96 = 0 % 37.12/9.64 | (252) mem(all_74_1_85, all_0_10_10) = 0 % 37.12/9.64 | % 37.12/9.64 +-Applying beta-rule and splitting (232), into two cases. % 37.12/9.64 |-Branch one: % 37.12/9.64 | (253) all_117_0_94 = 0 % 37.12/9.64 | % 37.12/9.64 | Equations (253) can reduce 228 to: % 37.12/9.64 | (175) $false % 37.12/9.64 | % 37.12/9.64 |-The branch is then unsatisfiable % 37.12/9.64 |-Branch two: % 37.12/9.64 | (228) ~ (all_117_0_94 = 0) % 37.12/9.64 | (256) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_59_0_79) = v1 & mem(all_74_1_85, all_0_5_5) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating (256) with all_136_0_101, all_136_1_102 yields: % 37.12/9.64 | (257) ~ (all_136_0_101 = 0) & ~ (all_136_1_102 = 0) & mem(all_74_1_85, all_59_0_79) = all_136_0_101 & mem(all_74_1_85, all_0_5_5) = all_136_1_102 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (257) yields: % 37.12/9.64 | (258) ~ (all_136_0_101 = 0) % 37.12/9.64 | (259) ~ (all_136_1_102 = 0) % 37.12/9.64 | (260) mem(all_74_1_85, all_59_0_79) = all_136_0_101 % 37.12/9.64 | (261) mem(all_74_1_85, all_0_5_5) = all_136_1_102 % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (15) with all_136_1_102, all_0_5_5, all_0_18_18, all_74_1_85 and discharging atoms p(all_0_18_18) = all_0_5_5, mem(all_74_1_85, all_0_5_5) = all_136_1_102, yields: % 37.12/9.64 | (262) all_136_1_102 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_74_1_85, all_0_18_18) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (126) with all_0_10_10, all_0_11_11, all_0_22_22, all_74_1_85 and discharging atoms u(all_0_22_22, all_0_11_11) = all_0_10_10, mem(all_74_1_85, all_0_10_10) = 0, yields: % 37.12/9.64 | (263) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_0_11_11) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_22_22) = 0)) % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (59) with all_127_1_98, all_0_20_20, all_0_21_21, all_0_23_23, all_74_1_85 and discharging atoms u(all_0_23_23, all_0_21_21) = all_0_20_20, mem(all_74_1_85, all_0_20_20) = all_127_1_98, yields: % 37.12/9.64 | (264) all_127_1_98 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_21_21) = v1 & mem(all_74_1_85, all_0_23_23) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating (263) with all_143_0_103 yields: % 37.12/9.64 | (265) (all_143_0_103 = 0 & mem(all_74_1_85, all_0_11_11) = 0) | (all_143_0_103 = 0 & mem(all_74_1_85, all_0_22_22) = 0) % 37.12/9.64 | % 37.12/9.64 +-Applying beta-rule and splitting (262), into two cases. % 37.12/9.64 |-Branch one: % 37.12/9.64 | (266) all_136_1_102 = 0 % 37.12/9.64 | % 37.12/9.64 | Equations (266) can reduce 259 to: % 37.12/9.64 | (175) $false % 37.12/9.64 | % 37.12/9.64 |-The branch is then unsatisfiable % 37.12/9.64 |-Branch two: % 37.12/9.64 | (259) ~ (all_136_1_102 = 0) % 37.12/9.64 | (269) ? [v0] : ( ~ (v0 = 0) & subq(all_74_1_85, all_0_18_18) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating (269) with all_146_0_104 yields: % 37.12/9.64 | (270) ~ (all_146_0_104 = 0) & subq(all_74_1_85, all_0_18_18) = all_146_0_104 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (270) yields: % 37.12/9.64 | (271) ~ (all_146_0_104 = 0) % 37.12/9.64 | (272) subq(all_74_1_85, all_0_18_18) = all_146_0_104 % 37.12/9.64 | % 37.12/9.64 +-Applying beta-rule and splitting (264), into two cases. % 37.12/9.64 |-Branch one: % 37.12/9.64 | (273) all_127_1_98 = 0 % 37.12/9.64 | % 37.12/9.64 | Equations (273) can reduce 242 to: % 37.12/9.64 | (175) $false % 37.12/9.64 | % 37.12/9.64 |-The branch is then unsatisfiable % 37.12/9.64 |-Branch two: % 37.12/9.64 | (242) ~ (all_127_1_98 = 0) % 37.12/9.64 | (276) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_21_21) = v1 & mem(all_74_1_85, all_0_23_23) = v0) % 37.12/9.64 | % 37.12/9.64 | Instantiating (276) with all_152_0_105, all_152_1_106 yields: % 37.12/9.64 | (277) ~ (all_152_0_105 = 0) & ~ (all_152_1_106 = 0) & mem(all_74_1_85, all_0_21_21) = all_152_0_105 & mem(all_74_1_85, all_0_23_23) = all_152_1_106 % 37.12/9.64 | % 37.12/9.64 | Applying alpha-rule on (277) yields: % 37.12/9.64 | (278) ~ (all_152_0_105 = 0) % 37.12/9.64 | (279) ~ (all_152_1_106 = 0) % 37.12/9.64 | (280) mem(all_74_1_85, all_0_21_21) = all_152_0_105 % 37.12/9.64 | (281) mem(all_74_1_85, all_0_23_23) = all_152_1_106 % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (139) with all_146_0_104, all_0_18_18, all_74_1_85 and discharging atoms subq(all_74_1_85, all_0_18_18) = all_146_0_104, yields: % 37.12/9.64 | (282) all_146_0_104 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_74_1_85) = 0 & mem(v0, all_0_18_18) = v1) % 37.12/9.64 | % 37.12/9.64 | Instantiating formula (59) with all_152_0_105, all_0_21_21, all_0_12_12, all_0_22_22, all_74_1_85 and discharging atoms u(all_0_22_22, all_0_12_12) = all_0_21_21, mem(all_74_1_85, all_0_21_21) = all_152_0_105, yields: % 37.12/9.64 | (283) all_152_0_105 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_12_12) = v1 & mem(all_74_1_85, all_0_22_22) = v0) % 37.12/9.64 | % 37.12/9.64 +-Applying beta-rule and splitting (265), into two cases. % 37.12/9.64 |-Branch one: % 37.12/9.64 | (284) all_143_0_103 = 0 & mem(all_74_1_85, all_0_11_11) = 0 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (284) yields: % 37.12/9.65 | (285) all_143_0_103 = 0 % 37.12/9.65 | (286) mem(all_74_1_85, all_0_11_11) = 0 % 37.12/9.65 | % 37.12/9.65 +-Applying beta-rule and splitting (282), into two cases. % 37.12/9.65 |-Branch one: % 37.12/9.65 | (287) all_146_0_104 = 0 % 37.12/9.65 | % 37.12/9.65 | Equations (287) can reduce 271 to: % 37.12/9.65 | (175) $false % 37.12/9.65 | % 37.12/9.65 |-The branch is then unsatisfiable % 37.12/9.65 |-Branch two: % 37.12/9.65 | (271) ~ (all_146_0_104 = 0) % 37.12/9.65 | (290) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_74_1_85) = 0 & mem(v0, all_0_18_18) = v1) % 37.12/9.65 | % 37.12/9.65 | Instantiating (290) with all_170_0_109, all_170_1_110 yields: % 37.12/9.65 | (291) ~ (all_170_0_109 = 0) & mem(all_170_1_110, all_74_1_85) = 0 & mem(all_170_1_110, all_0_18_18) = all_170_0_109 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (291) yields: % 37.12/9.65 | (292) ~ (all_170_0_109 = 0) % 37.12/9.65 | (293) mem(all_170_1_110, all_74_1_85) = 0 % 37.12/9.65 | (294) mem(all_170_1_110, all_0_18_18) = all_170_0_109 % 37.12/9.65 | % 37.12/9.65 +-Applying beta-rule and splitting (283), into two cases. % 37.12/9.65 |-Branch one: % 37.12/9.65 | (295) all_152_0_105 = 0 % 37.12/9.65 | % 37.12/9.65 | Equations (295) can reduce 278 to: % 37.12/9.65 | (175) $false % 37.12/9.65 | % 37.12/9.65 |-The branch is then unsatisfiable % 37.12/9.65 |-Branch two: % 37.12/9.65 | (278) ~ (all_152_0_105 = 0) % 37.12/9.65 | (298) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_12_12) = v1 & mem(all_74_1_85, all_0_22_22) = v0) % 37.12/9.65 | % 37.12/9.65 | Instantiating (298) with all_175_0_111, all_175_1_112 yields: % 37.12/9.65 | (299) ~ (all_175_0_111 = 0) & ~ (all_175_1_112 = 0) & mem(all_74_1_85, all_0_12_12) = all_175_0_111 & mem(all_74_1_85, all_0_22_22) = all_175_1_112 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (299) yields: % 37.12/9.65 | (300) ~ (all_175_0_111 = 0) % 37.12/9.65 | (301) ~ (all_175_1_112 = 0) % 37.12/9.65 | (302) mem(all_74_1_85, all_0_12_12) = all_175_0_111 % 37.12/9.65 | (303) mem(all_74_1_85, all_0_22_22) = all_175_1_112 % 37.12/9.65 | % 37.12/9.65 | Instantiating formula (15) with all_170_0_109, all_0_18_18, all_0_22_22, all_170_1_110 and discharging atoms p(all_0_22_22) = all_0_18_18, mem(all_170_1_110, all_0_18_18) = all_170_0_109, yields: % 37.12/9.65 | (304) all_170_0_109 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_170_1_110, all_0_22_22) = v0) % 37.12/9.65 | % 37.12/9.65 | Instantiating formula (126) with all_0_11_11, all_90_0_89, all_0_12_12, all_74_1_85 and discharging atoms u(all_0_12_12, all_90_0_89) = all_0_11_11, mem(all_74_1_85, all_0_11_11) = 0, yields: % 37.12/9.65 | (305) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_90_0_89) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_12_12) = 0)) % 37.12/9.65 | % 37.12/9.65 | Instantiating (305) with all_182_0_113 yields: % 37.12/9.65 | (306) (all_182_0_113 = 0 & mem(all_74_1_85, all_90_0_89) = 0) | (all_182_0_113 = 0 & mem(all_74_1_85, all_0_12_12) = 0) % 37.12/9.65 | % 37.12/9.65 +-Applying beta-rule and splitting (304), into two cases. % 37.12/9.65 |-Branch one: % 37.12/9.65 | (307) all_170_0_109 = 0 % 37.12/9.65 | % 37.12/9.65 | Equations (307) can reduce 292 to: % 37.12/9.65 | (175) $false % 37.12/9.65 | % 37.12/9.65 |-The branch is then unsatisfiable % 37.12/9.65 |-Branch two: % 37.12/9.65 | (292) ~ (all_170_0_109 = 0) % 37.12/9.65 | (310) ? [v0] : ( ~ (v0 = 0) & subq(all_170_1_110, all_0_22_22) = v0) % 37.12/9.65 | % 37.12/9.65 | Instantiating (310) with all_185_0_114 yields: % 37.12/9.65 | (311) ~ (all_185_0_114 = 0) & subq(all_170_1_110, all_0_22_22) = all_185_0_114 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (311) yields: % 37.12/9.65 | (312) ~ (all_185_0_114 = 0) % 37.12/9.65 | (313) subq(all_170_1_110, all_0_22_22) = all_185_0_114 % 37.12/9.65 | % 37.12/9.65 +-Applying beta-rule and splitting (306), into two cases. % 37.12/9.65 |-Branch one: % 37.12/9.65 | (314) all_182_0_113 = 0 & mem(all_74_1_85, all_90_0_89) = 0 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (314) yields: % 37.12/9.65 | (315) all_182_0_113 = 0 % 37.12/9.65 | (316) mem(all_74_1_85, all_90_0_89) = 0 % 37.12/9.65 | % 37.12/9.65 | Instantiating formula (71) with all_90_0_89, all_0_12_12, all_74_1_85 and discharging atoms s(all_0_12_12) = all_90_0_89, mem(all_74_1_85, all_90_0_89) = 0, yields: % 37.12/9.65 | (317) all_74_1_85 = all_0_12_12 % 37.12/9.65 | % 37.12/9.65 | From (317) and (293) follows: % 37.12/9.65 | (318) mem(all_170_1_110, all_0_12_12) = 0 % 37.12/9.65 | % 37.12/9.65 | Instantiating formula (71) with all_0_12_12, all_0_22_22, all_170_1_110 and discharging atoms s(all_0_22_22) = all_0_12_12, mem(all_170_1_110, all_0_12_12) = 0, yields: % 37.12/9.65 | (319) all_170_1_110 = all_0_22_22 % 37.12/9.65 | % 37.12/9.65 | From (319) and (313) follows: % 37.12/9.65 | (320) subq(all_0_22_22, all_0_22_22) = all_185_0_114 % 37.12/9.65 | % 37.12/9.65 | Instantiating formula (139) with all_185_0_114, all_0_22_22, all_0_22_22 and discharging atoms subq(all_0_22_22, all_0_22_22) = all_185_0_114, yields: % 37.12/9.65 | (321) all_185_0_114 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_22_22) = v1 & mem(v0, all_0_22_22) = 0) % 37.12/9.65 | % 37.12/9.65 +-Applying beta-rule and splitting (321), into two cases. % 37.12/9.65 |-Branch one: % 37.12/9.65 | (322) all_185_0_114 = 0 % 37.12/9.65 | % 37.12/9.65 | Equations (322) can reduce 312 to: % 37.12/9.65 | (175) $false % 37.12/9.65 | % 37.12/9.65 |-The branch is then unsatisfiable % 37.12/9.65 |-Branch two: % 37.12/9.65 | (312) ~ (all_185_0_114 = 0) % 37.12/9.65 | (325) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_22_22) = v1 & mem(v0, all_0_22_22) = 0) % 37.12/9.65 | % 37.12/9.65 | Instantiating (325) with all_206_0_115, all_206_1_116 yields: % 37.12/9.65 | (326) ~ (all_206_0_115 = 0) & mem(all_206_1_116, all_0_22_22) = all_206_0_115 & mem(all_206_1_116, all_0_22_22) = 0 % 37.12/9.65 | % 37.12/9.65 | Applying alpha-rule on (326) yields: % 37.12/9.65 | (327) ~ (all_206_0_115 = 0) % 37.12/9.65 | (328) mem(all_206_1_116, all_0_22_22) = all_206_0_115 % 37.12/9.66 | (329) mem(all_206_1_116, all_0_22_22) = 0 % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (117) with all_206_1_116, all_0_22_22, 0, all_206_0_115 and discharging atoms mem(all_206_1_116, all_0_22_22) = all_206_0_115, mem(all_206_1_116, all_0_22_22) = 0, yields: % 37.12/9.66 | (330) all_206_0_115 = 0 % 37.12/9.66 | % 37.12/9.66 | Equations (330) can reduce 327 to: % 37.12/9.66 | (175) $false % 37.12/9.66 | % 37.12/9.66 |-The branch is then unsatisfiable % 37.12/9.66 |-Branch two: % 37.12/9.66 | (332) all_182_0_113 = 0 & mem(all_74_1_85, all_0_12_12) = 0 % 37.12/9.66 | % 37.12/9.66 | Applying alpha-rule on (332) yields: % 37.12/9.66 | (315) all_182_0_113 = 0 % 37.12/9.66 | (334) mem(all_74_1_85, all_0_12_12) = 0 % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (117) with all_74_1_85, all_0_12_12, 0, all_175_0_111 and discharging atoms mem(all_74_1_85, all_0_12_12) = all_175_0_111, mem(all_74_1_85, all_0_12_12) = 0, yields: % 37.12/9.66 | (335) all_175_0_111 = 0 % 37.12/9.66 | % 37.12/9.66 | Equations (335) can reduce 300 to: % 37.12/9.66 | (175) $false % 37.12/9.66 | % 37.12/9.66 |-The branch is then unsatisfiable % 37.12/9.66 |-Branch two: % 37.12/9.66 | (337) all_143_0_103 = 0 & mem(all_74_1_85, all_0_22_22) = 0 % 37.12/9.66 | % 37.12/9.66 | Applying alpha-rule on (337) yields: % 37.12/9.66 | (285) all_143_0_103 = 0 % 37.12/9.66 | (339) mem(all_74_1_85, all_0_22_22) = 0 % 37.12/9.66 | % 37.12/9.66 +-Applying beta-rule and splitting (283), into two cases. % 37.12/9.66 |-Branch one: % 37.12/9.66 | (295) all_152_0_105 = 0 % 37.12/9.66 | % 37.12/9.66 | Equations (295) can reduce 278 to: % 37.12/9.66 | (175) $false % 37.12/9.66 | % 37.12/9.66 |-The branch is then unsatisfiable % 37.12/9.66 |-Branch two: % 37.12/9.66 | (278) ~ (all_152_0_105 = 0) % 37.12/9.66 | (298) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_12_12) = v1 & mem(all_74_1_85, all_0_22_22) = v0) % 37.12/9.66 | % 37.12/9.66 | Instantiating (298) with all_165_0_119, all_165_1_120 yields: % 37.12/9.66 | (344) ~ (all_165_0_119 = 0) & ~ (all_165_1_120 = 0) & mem(all_74_1_85, all_0_12_12) = all_165_0_119 & mem(all_74_1_85, all_0_22_22) = all_165_1_120 % 37.12/9.66 | % 37.12/9.66 | Applying alpha-rule on (344) yields: % 37.12/9.66 | (345) ~ (all_165_0_119 = 0) % 37.12/9.66 | (346) ~ (all_165_1_120 = 0) % 37.12/9.66 | (347) mem(all_74_1_85, all_0_12_12) = all_165_0_119 % 37.12/9.66 | (348) mem(all_74_1_85, all_0_22_22) = all_165_1_120 % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (117) with all_74_1_85, all_0_22_22, 0, all_165_1_120 and discharging atoms mem(all_74_1_85, all_0_22_22) = all_165_1_120, mem(all_74_1_85, all_0_22_22) = 0, yields: % 37.12/9.66 | (349) all_165_1_120 = 0 % 37.12/9.66 | % 37.12/9.66 | Equations (349) can reduce 346 to: % 37.12/9.66 | (175) $false % 37.12/9.66 | % 37.12/9.66 |-The branch is then unsatisfiable % 37.12/9.66 |-Branch two: % 37.12/9.66 | (351) all_85_0_86 = 0 & mem(all_74_1_85, all_0_13_13) = 0 % 37.12/9.66 | % 37.12/9.66 | Applying alpha-rule on (351) yields: % 37.12/9.66 | (221) all_85_0_86 = 0 % 37.12/9.66 | (353) mem(all_74_1_85, all_0_13_13) = 0 % 37.12/9.66 | % 37.12/9.66 +-Applying beta-rule and splitting (219), into two cases. % 37.12/9.66 |-Branch one: % 37.12/9.66 | (223) all_100_1_93 = 0 % 37.12/9.66 | % 37.12/9.66 | Equations (223) can reduce 211 to: % 37.12/9.66 | (175) $false % 37.12/9.66 | % 37.12/9.66 |-The branch is then unsatisfiable % 37.12/9.66 |-Branch two: % 37.12/9.66 | (211) ~ (all_100_1_93 = 0) % 37.12/9.66 | (226) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_4_4) = v1 & mem(all_74_1_85, all_0_6_6) = v0) % 37.12/9.66 | % 37.12/9.66 | Instantiating (226) with all_117_0_125, all_117_1_126 yields: % 37.12/9.66 | (358) ~ (all_117_0_125 = 0) & ~ (all_117_1_126 = 0) & mem(all_74_1_85, all_0_4_4) = all_117_0_125 & mem(all_74_1_85, all_0_6_6) = all_117_1_126 % 37.12/9.66 | % 37.12/9.66 | Applying alpha-rule on (358) yields: % 37.12/9.66 | (359) ~ (all_117_0_125 = 0) % 37.12/9.66 | (360) ~ (all_117_1_126 = 0) % 37.12/9.66 | (361) mem(all_74_1_85, all_0_4_4) = all_117_0_125 % 37.12/9.66 | (362) mem(all_74_1_85, all_0_6_6) = all_117_1_126 % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (59) with all_117_0_125, all_0_4_4, all_59_0_79, all_0_5_5, all_74_1_85 and discharging atoms u(all_0_5_5, all_59_0_79) = all_0_4_4, mem(all_74_1_85, all_0_4_4) = all_117_0_125, yields: % 37.12/9.66 | (363) all_117_0_125 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_59_0_79) = v1 & mem(all_74_1_85, all_0_5_5) = v0) % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (59) with all_117_1_126, all_0_6_6, all_0_19_19, all_0_20_20, all_74_1_85 and discharging atoms u(all_0_20_20, all_0_19_19) = all_0_6_6, mem(all_74_1_85, all_0_6_6) = all_117_1_126, yields: % 37.12/9.66 | (364) all_117_1_126 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_19_19) = v1 & mem(all_74_1_85, all_0_20_20) = v0) % 37.12/9.66 | % 37.12/9.66 | Instantiating formula (126) with all_0_13_13, all_0_14_14, all_0_19_19, all_74_1_85 and discharging atoms u(all_0_19_19, all_0_14_14) = all_0_13_13, mem(all_74_1_85, all_0_13_13) = 0, yields: % 37.12/9.66 | (365) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_0_14_14) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_19_19) = 0)) % 37.12/9.66 | % 37.12/9.67 | Instantiating (365) with all_124_0_127 yields: % 37.12/9.67 | (366) (all_124_0_127 = 0 & mem(all_74_1_85, all_0_14_14) = 0) | (all_124_0_127 = 0 & mem(all_74_1_85, all_0_19_19) = 0) % 37.12/9.67 | % 37.12/9.67 +-Applying beta-rule and splitting (364), into two cases. % 37.12/9.67 |-Branch one: % 37.12/9.67 | (367) all_117_1_126 = 0 % 37.12/9.67 | % 37.12/9.67 | Equations (367) can reduce 360 to: % 37.12/9.67 | (175) $false % 37.12/9.67 | % 37.12/9.67 |-The branch is then unsatisfiable % 37.12/9.67 |-Branch two: % 37.12/9.67 | (360) ~ (all_117_1_126 = 0) % 37.12/9.67 | (239) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_0_19_19) = v1 & mem(all_74_1_85, all_0_20_20) = v0) % 37.12/9.67 | % 37.12/9.67 | Instantiating (239) with all_127_0_128, all_127_1_129 yields: % 37.12/9.67 | (371) ~ (all_127_0_128 = 0) & ~ (all_127_1_129 = 0) & mem(all_74_1_85, all_0_19_19) = all_127_0_128 & mem(all_74_1_85, all_0_20_20) = all_127_1_129 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (371) yields: % 37.12/9.67 | (372) ~ (all_127_0_128 = 0) % 37.12/9.67 | (373) ~ (all_127_1_129 = 0) % 37.12/9.67 | (374) mem(all_74_1_85, all_0_19_19) = all_127_0_128 % 37.12/9.67 | (375) mem(all_74_1_85, all_0_20_20) = all_127_1_129 % 37.12/9.67 | % 37.12/9.67 +-Applying beta-rule and splitting (366), into two cases. % 37.12/9.67 |-Branch one: % 37.12/9.67 | (376) all_124_0_127 = 0 & mem(all_74_1_85, all_0_14_14) = 0 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (376) yields: % 37.12/9.67 | (377) all_124_0_127 = 0 % 37.12/9.67 | (378) mem(all_74_1_85, all_0_14_14) = 0 % 37.12/9.67 | % 37.12/9.67 +-Applying beta-rule and splitting (363), into two cases. % 37.12/9.67 |-Branch one: % 37.12/9.67 | (379) all_117_0_125 = 0 % 37.12/9.67 | % 37.12/9.67 | Equations (379) can reduce 359 to: % 37.12/9.67 | (175) $false % 37.12/9.67 | % 37.12/9.67 |-The branch is then unsatisfiable % 37.12/9.67 |-Branch two: % 37.12/9.67 | (359) ~ (all_117_0_125 = 0) % 37.12/9.67 | (256) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_74_1_85, all_59_0_79) = v1 & mem(all_74_1_85, all_0_5_5) = v0) % 37.12/9.67 | % 37.12/9.67 | Instantiating (256) with all_136_0_130, all_136_1_131 yields: % 37.12/9.67 | (383) ~ (all_136_0_130 = 0) & ~ (all_136_1_131 = 0) & mem(all_74_1_85, all_59_0_79) = all_136_0_130 & mem(all_74_1_85, all_0_5_5) = all_136_1_131 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (383) yields: % 37.12/9.67 | (384) ~ (all_136_0_130 = 0) % 37.12/9.67 | (385) ~ (all_136_1_131 = 0) % 37.12/9.67 | (386) mem(all_74_1_85, all_59_0_79) = all_136_0_130 % 37.12/9.67 | (387) mem(all_74_1_85, all_0_5_5) = all_136_1_131 % 37.12/9.67 | % 37.12/9.67 | Instantiating formula (15) with all_136_1_131, all_0_5_5, all_0_18_18, all_74_1_85 and discharging atoms p(all_0_18_18) = all_0_5_5, mem(all_74_1_85, all_0_5_5) = all_136_1_131, yields: % 37.12/9.67 | (388) all_136_1_131 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_74_1_85, all_0_18_18) = v0) % 37.12/9.67 | % 37.12/9.67 | Instantiating formula (126) with all_0_14_14, all_59_0_79, all_0_17_17, all_74_1_85 and discharging atoms u(all_0_17_17, all_59_0_79) = all_0_14_14, mem(all_74_1_85, all_0_14_14) = 0, yields: % 37.12/9.67 | (389) ? [v0] : ((v0 = 0 & mem(all_74_1_85, all_59_0_79) = 0) | (v0 = 0 & mem(all_74_1_85, all_0_17_17) = 0)) % 37.12/9.67 | % 37.12/9.67 | Instantiating (389) with all_143_0_132 yields: % 37.12/9.67 | (390) (all_143_0_132 = 0 & mem(all_74_1_85, all_59_0_79) = 0) | (all_143_0_132 = 0 & mem(all_74_1_85, all_0_17_17) = 0) % 37.12/9.67 | % 37.12/9.67 +-Applying beta-rule and splitting (388), into two cases. % 37.12/9.67 |-Branch one: % 37.12/9.67 | (391) all_136_1_131 = 0 % 37.12/9.67 | % 37.12/9.67 | Equations (391) can reduce 385 to: % 37.12/9.67 | (175) $false % 37.12/9.67 | % 37.12/9.67 |-The branch is then unsatisfiable % 37.12/9.67 |-Branch two: % 37.12/9.67 | (385) ~ (all_136_1_131 = 0) % 37.12/9.67 | (269) ? [v0] : ( ~ (v0 = 0) & subq(all_74_1_85, all_0_18_18) = v0) % 37.12/9.67 | % 37.12/9.67 | Instantiating (269) with all_146_0_133 yields: % 37.12/9.67 | (395) ~ (all_146_0_133 = 0) & subq(all_74_1_85, all_0_18_18) = all_146_0_133 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (395) yields: % 37.12/9.67 | (396) ~ (all_146_0_133 = 0) % 37.12/9.67 | (397) subq(all_74_1_85, all_0_18_18) = all_146_0_133 % 37.12/9.67 | % 37.12/9.67 +-Applying beta-rule and splitting (390), into two cases. % 37.12/9.67 |-Branch one: % 37.12/9.67 | (398) all_143_0_132 = 0 & mem(all_74_1_85, all_59_0_79) = 0 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (398) yields: % 37.12/9.67 | (399) all_143_0_132 = 0 % 37.12/9.67 | (400) mem(all_74_1_85, all_59_0_79) = 0 % 37.12/9.67 | % 37.12/9.67 | Instantiating formula (117) with all_74_1_85, all_59_0_79, 0, all_136_0_130 and discharging atoms mem(all_74_1_85, all_59_0_79) = all_136_0_130, mem(all_74_1_85, all_59_0_79) = 0, yields: % 37.12/9.67 | (401) all_136_0_130 = 0 % 37.12/9.67 | % 37.12/9.67 | Equations (401) can reduce 384 to: % 37.12/9.67 | (175) $false % 37.12/9.67 | % 37.12/9.67 |-The branch is then unsatisfiable % 37.12/9.67 |-Branch two: % 37.12/9.67 | (403) all_143_0_132 = 0 & mem(all_74_1_85, all_0_17_17) = 0 % 37.12/9.67 | % 37.12/9.67 | Applying alpha-rule on (403) yields: % 37.12/9.67 | (399) all_143_0_132 = 0 % 37.12/9.67 | (405) mem(all_74_1_85, all_0_17_17) = 0 % 37.12/9.67 | % 37.12/9.67 | Instantiating formula (71) with all_0_17_17, all_0_18_18, all_74_1_85 and discharging atoms s(all_0_18_18) = all_0_17_17, mem(all_74_1_85, all_0_17_17) = 0, yields: % 37.12/9.67 | (406) all_74_1_85 = all_0_18_18 % 37.12/9.67 | % 37.12/9.67 | From (406) and (397) follows: % 37.12/9.68 | (407) subq(all_0_18_18, all_0_18_18) = all_146_0_133 % 37.12/9.68 | % 37.12/9.68 | Instantiating formula (139) with all_146_0_133, all_0_18_18, all_0_18_18 and discharging atoms subq(all_0_18_18, all_0_18_18) = all_146_0_133, yields: % 37.12/9.68 | (408) all_146_0_133 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_18_18) = v1 & mem(v0, all_0_18_18) = 0) % 37.12/9.68 | % 37.12/9.68 +-Applying beta-rule and splitting (408), into two cases. % 37.12/9.68 |-Branch one: % 37.12/9.68 | (409) all_146_0_133 = 0 % 37.12/9.68 | % 37.12/9.68 | Equations (409) can reduce 396 to: % 37.12/9.68 | (175) $false % 37.12/9.68 | % 37.12/9.68 |-The branch is then unsatisfiable % 37.12/9.68 |-Branch two: % 37.12/9.68 | (396) ~ (all_146_0_133 = 0) % 37.12/9.68 | (412) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_18_18) = v1 & mem(v0, all_0_18_18) = 0) % 37.12/9.68 | % 37.12/9.68 | Instantiating (412) with all_174_0_140, all_174_1_141 yields: % 37.12/9.68 | (413) ~ (all_174_0_140 = 0) & mem(all_174_1_141, all_0_18_18) = all_174_0_140 & mem(all_174_1_141, all_0_18_18) = 0 % 37.12/9.68 | % 37.12/9.68 | Applying alpha-rule on (413) yields: % 37.12/9.68 | (414) ~ (all_174_0_140 = 0) % 37.12/9.68 | (415) mem(all_174_1_141, all_0_18_18) = all_174_0_140 % 37.12/9.68 | (416) mem(all_174_1_141, all_0_18_18) = 0 % 37.12/9.68 | % 37.12/9.68 | Instantiating formula (117) with all_174_1_141, all_0_18_18, 0, all_174_0_140 and discharging atoms mem(all_174_1_141, all_0_18_18) = all_174_0_140, mem(all_174_1_141, all_0_18_18) = 0, yields: % 37.12/9.68 | (417) all_174_0_140 = 0 % 37.12/9.68 | % 37.12/9.68 | Equations (417) can reduce 414 to: % 37.12/9.68 | (175) $false % 37.12/9.68 | % 37.12/9.68 |-The branch is then unsatisfiable % 37.12/9.68 |-Branch two: % 37.12/9.68 | (419) all_124_0_127 = 0 & mem(all_74_1_85, all_0_19_19) = 0 % 37.12/9.68 | % 37.12/9.68 | Applying alpha-rule on (419) yields: % 37.12/9.68 | (377) all_124_0_127 = 0 % 37.12/9.68 | (421) mem(all_74_1_85, all_0_19_19) = 0 % 37.12/9.68 | % 37.12/9.68 | Instantiating formula (117) with all_74_1_85, all_0_19_19, 0, all_127_0_128 and discharging atoms mem(all_74_1_85, all_0_19_19) = all_127_0_128, mem(all_74_1_85, all_0_19_19) = 0, yields: % 37.12/9.68 | (422) all_127_0_128 = 0 % 37.12/9.68 | % 37.12/9.68 | Equations (422) can reduce 372 to: % 37.12/9.68 | (175) $false % 37.12/9.68 | % 37.12/9.68 |-The branch is then unsatisfiable % 37.12/9.68 % SZS output end Proof for theBenchmark % 37.12/9.68 % 37.12/9.68 9044ms %------------------------------------------------------------------------------