%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV580+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n021.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 21.40s 6.39s % Output : Proof 29.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEV580+1 : TPTP v9.1.0. Released v9.1.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Mar 31 13:10:37 EDT 2025 % 0.13/0.34 % CPUTime : % 0.60/0.59 ____ _ % 0.60/0.59 ___ / __ \_____(_)___ ________ __________ % 0.60/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.60/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.60/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.60/0.59 % 0.60/0.59 A Theorem Prover for First-Order Logic % 0.60/0.59 (ePrincess v.1.0) % 0.60/0.59 % 0.60/0.59 (c) Philipp Rümmer, 2009-2015 % 0.60/0.59 (c) Peter Backeman, 2014-2015 % 0.60/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.60/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.60/0.59 Bug reports to peter@backeman.se % 0.60/0.59 % 0.60/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.60/0.60 % 0.60/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.73/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.76/0.94 Prover 0: Preprocessing ... % 2.66/1.19 Prover 0: Warning: ignoring some quantifiers % 2.66/1.22 Prover 0: Constructing countermodel ... % 19.54/5.94 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 19.79/6.00 Prover 1: Preprocessing ... % 20.81/6.22 Prover 1: Constructing countermodel ... % 21.40/6.39 Prover 1: proved (451ms) % 21.40/6.39 Prover 0: stopped % 21.40/6.39 % 21.40/6.39 No countermodel exists, formula is valid % 21.40/6.39 % SZS status Theorem for theBenchmark % 21.40/6.39 % 21.40/6.39 Generating proof ... found it (size 79) % 28.88/8.31 % 28.88/8.31 % SZS output start Proof for theBenchmark % 28.88/8.31 Assumed formulas after preprocessing and simplification: % 28.88/8.31 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ( ~ (v19 = 0) & p(v5) = v15 & n(v8) = v9 & n(v7) = v12 & n(v1) = v2 & n(v0) = v7 & n(e) = v0 & u(v17, v13) = v18 & u(v15, v9) = v16 & u(v11, v13) = v14 & u(v6, v9) = v10 & u(v4, v16) = v17 & u(v4, v10) = v11 & u(v0, v2) = v3 & s(v12) = v13 & s(v7) = v8 & s(v5) = v6 & s(v3) = v4 & s(v1) = v5 & s(v0) = v1 & subq(v14, v18) = v19 & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v24 = 0 | v21 = 0 | ~ (atleast2p(v20) = v21) | ~ (p(v22) = v23) | ~ (subq(v20, v23) = v24) | ? [v25] : ( ~ (v25 = 0) & mem(v22, v20) = v25)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v24 = 0 | ~ (m(v21, v22) = v23) | ~ (mem(v20, v23) = v24) | ? [v25] : ? [v26] : (mem(v20, v22) = v26 & mem(v20, v21) = v25 & ( ~ (v25 = 0) | v26 = 0))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v24 = 0 | ~ (u(v21, v22) = v23) | ~ (mem(v20, v23) = v24) | ? [v25] : ? [v26] : ( ~ (v26 = 0) & ~ (v25 = 0) & mem(v20, v22) = v26 & mem(v20, v21) = v25)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = 0 | ~ (p(v21) = v22) | ~ (mem(v20, v22) = v23) | ? [v24] : ( ~ (v24 = 0) & subq(v20, v21) = v24)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (a(v23, v22) = v21) | ~ (a(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (m(v23, v22) = v21) | ~ (m(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (u(v23, v22) = v21) | ~ (u(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (disj(v23, v22) = v21) | ~ (disj(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (subq(v23, v22) = v21) | ~ (subq(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (mem(v23, v22) = v21) | ~ (mem(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m(v21, v22) = v23) | ~ (mem(v20, v23) = 0) | ? [v24] : ( ~ (v24 = 0) & mem(v20, v22) = v24 & mem(v20, v21) = 0)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (u(v21, v22) = v23) | ~ (mem(v20, v23) = 0) | ? [v24] : ? [v25] : (mem(v20, v22) = v25 & mem(v20, v21) = v24 & (v25 = 0 | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (u(v20, v22) = v23) | ~ (s(v21) = v22) | a(v20, v21) = v23) & ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | ~ (s(v20) = v21) | ~ (mem(v20, v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | ~ (disj(v20, v21) = v22) | ? [v23] : (mem(v23, v21) = 0 & mem(v23, v20) = 0)) & ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | ~ (subq(v20, v21) = v22) | ? [v23] : ? [v24] : ( ~ (v24 = 0) & mem(v23, v21) = v24 & mem(v23, v20) = 0)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast16p(v22) = v21) | ~ (atleast16p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast15p(v22) = v21) | ~ (atleast15p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast14p(v22) = v21) | ~ (atleast14p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast13p(v22) = v21) | ~ (atleast13p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast12p(v22) = v21) | ~ (atleast12p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast11p(v22) = v21) | ~ (atleast11p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast10p(v22) = v21) | ~ (atleast10p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast9p(v22) = v21) | ~ (atleast9p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast8p(v22) = v21) | ~ (atleast8p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast7p(v22) = v21) | ~ (atleast7p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast6p(v22) = v21) | ~ (atleast6p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast5p(v22) = v21) | ~ (atleast5p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast4p(v22) = v21) | ~ (atleast4p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast3p(v22) = v21) | ~ (atleast3p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (atleast2p(v22) = v21) | ~ (atleast2p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (p(v22) = v21) | ~ (p(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (n(v22) = v21) | ~ (n(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (s(v22) = v21) | ~ (s(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (s(v21) = v22) | ~ (mem(v20, v22) = 0)) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast16p(v20) = v21) | ~ (atleast15p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast15p(v20) = v21) | ~ (atleast14p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast14p(v20) = v21) | ~ (atleast13p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast13p(v20) = v21) | ~ (atleast12p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast12p(v20) = v21) | ~ (atleast11p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast11p(v20) = v21) | ~ (atleast10p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast10p(v20) = v21) | ~ (atleast9p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast9p(v20) = v21) | ~ (atleast8p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast8p(v20) = v21) | ~ (atleast7p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast7p(v20) = v21) | ~ (atleast6p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast6p(v20) = v21) | ~ (atleast5p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast5p(v20) = v21) | ~ (atleast4p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast4p(v20) = v21) | ~ (atleast3p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : (v21 = 0 | ~ (atleast3p(v20) = v21) | ~ (atleast2p(v22) = 0) | ? [v23] : ? [v24] : (subq(v22, v20) = v23 & subq(v20, v22) = v24 & ( ~ (v23 = 0) | v24 = 0))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (p(v21) = v22) | ~ (mem(v20, v22) = 0) | subq(v20, v21) = 0) & ! [v20] : ! [v21] : ! [v22] : ( ~ (disj(v20, v21) = 0) | ~ (mem(v22, v20) = 0) | ? [v23] : ( ~ (v23 = 0) & mem(v22, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (subq(v20, v21) = 0) | ~ (mem(v22, v20) = 0) | mem(v22, v21) = 0) & ! [v20] : ! [v21] : (v21 = v20 | ~ (subq(v20, v21) = 0) | ? [v22] : ( ~ (v22 = 0) & subq(v21, v20) = v22)) & ! [v20] : ! [v21] : ( ~ (a(v20, v20) = v21) | n(v20) = v21) & ! [v20] : ( ~ (atleast16p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast15p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast15p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast14p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast14p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast13p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast13p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast12p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast12p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast11p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast11p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast10p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast10p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast9p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast9p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast8p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast8p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast7p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast7p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast6p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast6p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast5p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast5p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast4p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast4p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast3p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast3p(v20) = 0) | ? [v21] : ? [v22] : ( ~ (v22 = 0) & atleast2p(v21) = 0 & subq(v21, v20) = 0 & subq(v20, v21) = v22)) & ! [v20] : ( ~ (atleast2p(v20) = 0) | ? [v21] : ? [v22] : ? [v23] : ( ~ (v23 = 0) & p(v21) = v22 & subq(v20, v22) = v23 & mem(v21, v20) = 0)) & ! [v20] : ~ (mem(v20, e) = 0)) % 29.13/8.39 | 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 yields: % 29.13/8.39 | (1) ~ (all_0_0_0 = 0) & p(all_0_14_14) = all_0_4_4 & n(all_0_11_11) = all_0_10_10 & n(all_0_12_12) = all_0_7_7 & n(all_0_18_18) = all_0_17_17 & n(all_0_19_19) = all_0_12_12 & n(e) = all_0_19_19 & u(all_0_2_2, all_0_6_6) = all_0_1_1 & u(all_0_4_4, all_0_10_10) = all_0_3_3 & u(all_0_8_8, all_0_6_6) = all_0_5_5 & u(all_0_13_13, all_0_10_10) = all_0_9_9 & u(all_0_15_15, all_0_3_3) = all_0_2_2 & u(all_0_15_15, all_0_9_9) = all_0_8_8 & u(all_0_19_19, all_0_17_17) = all_0_16_16 & s(all_0_7_7) = all_0_6_6 & s(all_0_12_12) = all_0_11_11 & s(all_0_14_14) = all_0_13_13 & s(all_0_16_16) = all_0_15_15 & s(all_0_18_18) = all_0_14_14 & s(all_0_19_19) = all_0_18_18 & subq(all_0_5_5, all_0_1_1) = all_0_0_0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ~ (subq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & mem(v2, v0) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ? [v6] : (mem(v0, v2) = v6 & mem(v0, v1) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [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 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = 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] : ( ~ (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] : ? [v5] : (mem(v0, v2) = v5 & mem(v0, v1) = v4 & (v5 = 0 | v4 = 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) & 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] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) & ! [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(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) & ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) & ! [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) % 29.13/8.41 | % 29.13/8.41 | Applying alpha-rule on (1) yields: % 29.13/8.41 | (2) u(all_0_8_8, all_0_6_6) = all_0_5_5 % 29.13/8.41 | (3) u(all_0_4_4, all_0_10_10) = all_0_3_3 % 29.13/8.41 | (4) ! [v0] : ( ~ (atleast11p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast10p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.41 | (5) s(all_0_18_18) = all_0_14_14 % 29.13/8.41 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (disj(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ? [v3] : ( ~ (v3 = 0) & mem(v2, v1) = v3)) % 29.13/8.41 | (7) n(all_0_11_11) = all_0_10_10 % 29.13/8.41 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ (atleast13p(v2) = v0)) % 29.13/8.41 | (9) ! [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)) % 29.13/8.41 | (10) u(all_0_15_15, all_0_3_3) = all_0_2_2 % 29.13/8.41 | (11) subq(all_0_5_5, all_0_1_1) = all_0_0_0 % 29.13/8.41 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 29.13/8.41 | (13) n(all_0_12_12) = all_0_7_7 % 29.13/8.41 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ (atleast7p(v2) = v0)) % 29.13/8.41 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast8p(v0) = v1) | ~ (atleast7p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.41 | (16) p(all_0_14_14) = all_0_4_4 % 29.13/8.41 | (17) ! [v0] : ( ~ (atleast14p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast13p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.41 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 29.13/8.41 | (19) u(all_0_15_15, all_0_9_9) = all_0_8_8 % 29.13/8.41 | (20) ! [v0] : ( ~ (atleast13p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast12p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.41 | (21) ~ (all_0_0_0 = 0) % 29.13/8.41 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subq(v3, v2) = v1) | ~ (subq(v3, v2) = v0)) % 29.13/8.42 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ (atleast10p(v2) = v0)) % 29.13/8.42 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ? [v5] : (mem(v0, v2) = v5 & mem(v0, v1) = v4 & (v5 = 0 | v4 = 0))) % 29.13/8.42 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) | subq(v0, v1) = 0) % 29.13/8.42 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast13p(v0) = v1) | ~ (atleast12p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast16p(v0) = v1) | ~ (atleast15p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (28) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ (atleast2p(v2) = v0)) % 29.13/8.42 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ (atleast16p(v2) = v0)) % 29.13/8.42 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ (atleast8p(v2) = v0)) % 29.13/8.42 | (31) ! [v0] : ( ~ (atleast8p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast7p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.42 | (32) s(all_0_19_19) = all_0_18_18 % 29.13/8.42 | (33) ! [v0] : ( ~ (atleast15p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast14p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.42 | (34) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 29.13/8.42 | (35) s(all_0_12_12) = all_0_11_11 % 29.13/8.42 | (36) ! [v0] : ! [v1] : (v1 = v0 | ~ (subq(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subq(v1, v0) = v2)) % 29.13/8.42 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 29.13/8.42 | (38) ! [v0] : ( ~ (atleast2p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0)) % 29.13/8.42 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ (atleast11p(v2) = v0)) % 29.13/8.42 | (40) ! [v0] : ( ~ (atleast5p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast4p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.42 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast5p(v0) = v1) | ~ (atleast4p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ? [v5] : ? [v6] : (mem(v0, v2) = v6 & mem(v0, v1) = v5 & ( ~ (v5 = 0) | v6 = 0))) % 29.13/8.42 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 29.13/8.42 | (44) s(all_0_7_7) = all_0_6_6 % 29.13/8.42 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast10p(v0) = v1) | ~ (atleast9p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (46) ! [v0] : ( ~ (atleast9p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast8p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.42 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ (atleast4p(v2) = v0)) % 29.13/8.42 | (48) ! [v0] : ( ~ (atleast3p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.42 | (49) n(all_0_19_19) = all_0_12_12 % 29.13/8.42 | (50) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast6p(v0) = v1) | ~ (atleast5p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ (atleast14p(v2) = v0)) % 29.13/8.42 | (52) s(all_0_14_14) = all_0_13_13 % 29.13/8.42 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.42 | (54) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ (atleast12p(v2) = v0)) % 29.13/8.43 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ (atleast3p(v2) = v0)) % 29.13/8.43 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (disj(v3, v2) = v1) | ~ (disj(v3, v2) = v0)) % 29.13/8.43 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v1 = 0 | ~ (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ~ (subq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & mem(v2, v0) = v5)) % 29.13/8.43 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast9p(v0) = v1) | ~ (atleast8p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (59) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 29.13/8.43 | (60) s(all_0_16_16) = all_0_15_15 % 29.13/8.43 | (61) ! [v0] : ( ~ (atleast7p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast6p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.43 | (62) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ (atleast5p(v2) = v0)) % 29.13/8.43 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0)) % 29.13/8.43 | (64) u(all_0_2_2, all_0_6_6) = all_0_1_1 % 29.13/8.43 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 29.13/8.43 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast11p(v0) = v1) | ~ (atleast10p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast7p(v0) = v1) | ~ (atleast6p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (68) n(e) = all_0_19_19 % 29.13/8.43 | (69) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ (atleast15p(v2) = v0)) % 29.13/8.43 | (70) u(all_0_13_13, all_0_10_10) = all_0_9_9 % 29.13/8.43 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 29.13/8.43 | (72) n(all_0_18_18) = all_0_17_17 % 29.13/8.43 | (73) ! [v0] : ( ~ (atleast4p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.43 | (74) ! [v0] : ( ~ (atleast12p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast11p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.43 | (75) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0)) % 29.13/8.43 | (76) ! [v0] : ( ~ (atleast10p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast9p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.43 | (77) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast15p(v0) = v1) | ~ (atleast14p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (78) ! [v0] : ( ~ (atleast6p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast5p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.43 | (79) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ (atleast9p(v2) = v0)) % 29.13/8.43 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast14p(v0) = v1) | ~ (atleast13p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (81) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (s(v0) = v1) | ~ (mem(v0, v1) = v2)) % 29.13/8.43 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 29.13/8.43 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | mem(v2, v1) = 0) % 29.13/8.43 | (84) u(all_0_19_19, all_0_17_17) = all_0_16_16 % 29.13/8.43 | (85) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 29.13/8.43 | (86) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (disj(v0, v1) = v2) | ? [v3] : (mem(v3, v1) = 0 & mem(v3, v0) = 0)) % 29.13/8.43 | (87) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ (atleast6p(v2) = v0)) % 29.13/8.43 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast12p(v0) = v1) | ~ (atleast11p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.43 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & mem(v0, v2) = v4 & mem(v0, v1) = 0)) % 29.13/8.44 | (90) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ? [v3] : ? [v4] : (subq(v2, v0) = v3 & subq(v0, v2) = v4 & ( ~ (v3 = 0) | v4 = 0))) % 29.13/8.44 | (91) ! [v0] : ( ~ (atleast16p(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & atleast15p(v1) = 0 & subq(v1, v0) = 0 & subq(v0, v1) = v2)) % 29.13/8.44 | (92) ! [v0] : ~ (mem(v0, e) = 0) % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (75) with all_0_0_0, all_0_1_1, all_0_5_5 and discharging atoms subq(all_0_5_5, all_0_1_1) = all_0_0_0, yields: % 29.13/8.44 | (93) all_0_0_0 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_5_5) = 0) % 29.13/8.44 | % 29.13/8.44 +-Applying beta-rule and splitting (93), into two cases. % 29.13/8.44 |-Branch one: % 29.13/8.44 | (94) all_0_0_0 = 0 % 29.13/8.44 | % 29.13/8.44 | Equations (94) can reduce 21 to: % 29.13/8.44 | (95) $false % 29.13/8.44 | % 29.13/8.44 |-The branch is then unsatisfiable % 29.13/8.44 |-Branch two: % 29.13/8.44 | (21) ~ (all_0_0_0 = 0) % 29.13/8.44 | (97) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_1_1) = v1 & mem(v0, all_0_5_5) = 0) % 29.13/8.44 | % 29.13/8.44 | Instantiating (97) with all_13_0_20, all_13_1_21 yields: % 29.13/8.44 | (98) ~ (all_13_0_20 = 0) & mem(all_13_1_21, all_0_1_1) = all_13_0_20 & mem(all_13_1_21, all_0_5_5) = 0 % 29.13/8.44 | % 29.13/8.44 | Applying alpha-rule on (98) yields: % 29.13/8.44 | (99) ~ (all_13_0_20 = 0) % 29.13/8.44 | (100) mem(all_13_1_21, all_0_1_1) = all_13_0_20 % 29.13/8.44 | (101) mem(all_13_1_21, all_0_5_5) = 0 % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (63) with all_0_13_13, all_0_14_14, all_13_1_21 and discharging atoms s(all_0_14_14) = all_0_13_13, yields: % 29.13/8.44 | (102) all_13_1_21 = all_0_14_14 | ~ (mem(all_13_1_21, all_0_13_13) = 0) % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (9) with all_13_0_20, all_0_1_1, all_0_6_6, all_0_2_2, all_13_1_21 and discharging atoms u(all_0_2_2, all_0_6_6) = all_0_1_1, mem(all_13_1_21, all_0_1_1) = all_13_0_20, yields: % 29.13/8.44 | (103) all_13_0_20 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_2_2) = v0 & mem(all_13_1_21, all_0_6_6) = v1) % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (24) with all_0_5_5, all_0_6_6, all_0_8_8, all_13_1_21 and discharging atoms u(all_0_8_8, all_0_6_6) = all_0_5_5, mem(all_13_1_21, all_0_5_5) = 0, yields: % 29.13/8.44 | (104) ? [v0] : ? [v1] : (mem(all_13_1_21, all_0_6_6) = v1 & mem(all_13_1_21, all_0_8_8) = v0 & (v1 = 0 | v0 = 0)) % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (24) with all_0_9_9, all_0_10_10, all_0_13_13, all_13_1_21 and discharging atoms u(all_0_13_13, all_0_10_10) = all_0_9_9, yields: % 29.13/8.44 | (105) ~ (mem(all_13_1_21, all_0_9_9) = 0) | ? [v0] : ? [v1] : (mem(all_13_1_21, all_0_10_10) = v1 & mem(all_13_1_21, all_0_13_13) = v0 & (v1 = 0 | v0 = 0)) % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (24) with all_0_8_8, all_0_9_9, all_0_15_15, all_13_1_21 and discharging atoms u(all_0_15_15, all_0_9_9) = all_0_8_8, yields: % 29.13/8.44 | (106) ~ (mem(all_13_1_21, all_0_8_8) = 0) | ? [v0] : ? [v1] : (mem(all_13_1_21, all_0_9_9) = v1 & mem(all_13_1_21, all_0_15_15) = v0 & (v1 = 0 | v0 = 0)) % 29.13/8.44 | % 29.13/8.44 | Instantiating (104) with all_28_0_22, all_28_1_23 yields: % 29.13/8.44 | (107) mem(all_13_1_21, all_0_6_6) = all_28_0_22 & mem(all_13_1_21, all_0_8_8) = all_28_1_23 & (all_28_0_22 = 0 | all_28_1_23 = 0) % 29.13/8.44 | % 29.13/8.44 | Applying alpha-rule on (107) yields: % 29.13/8.44 | (108) mem(all_13_1_21, all_0_6_6) = all_28_0_22 % 29.13/8.44 | (109) mem(all_13_1_21, all_0_8_8) = all_28_1_23 % 29.13/8.44 | (110) all_28_0_22 = 0 | all_28_1_23 = 0 % 29.13/8.44 | % 29.13/8.44 +-Applying beta-rule and splitting (103), into two cases. % 29.13/8.44 |-Branch one: % 29.13/8.44 | (111) all_13_0_20 = 0 % 29.13/8.44 | % 29.13/8.44 | Equations (111) can reduce 99 to: % 29.13/8.44 | (95) $false % 29.13/8.44 | % 29.13/8.44 |-The branch is then unsatisfiable % 29.13/8.44 |-Branch two: % 29.13/8.44 | (99) ~ (all_13_0_20 = 0) % 29.13/8.44 | (114) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_2_2) = v0 & mem(all_13_1_21, all_0_6_6) = v1) % 29.13/8.44 | % 29.13/8.44 | Instantiating (114) with all_34_0_24, all_34_1_25 yields: % 29.13/8.44 | (115) ~ (all_34_0_24 = 0) & ~ (all_34_1_25 = 0) & mem(all_13_1_21, all_0_2_2) = all_34_1_25 & mem(all_13_1_21, all_0_6_6) = all_34_0_24 % 29.13/8.44 | % 29.13/8.44 | Applying alpha-rule on (115) yields: % 29.13/8.44 | (116) ~ (all_34_0_24 = 0) % 29.13/8.44 | (117) ~ (all_34_1_25 = 0) % 29.13/8.44 | (118) mem(all_13_1_21, all_0_2_2) = all_34_1_25 % 29.13/8.44 | (119) mem(all_13_1_21, all_0_6_6) = all_34_0_24 % 29.13/8.44 | % 29.13/8.44 | Instantiating formula (37) with all_13_1_21, all_0_6_6, all_28_0_22, all_34_0_24 and discharging atoms mem(all_13_1_21, all_0_6_6) = all_34_0_24, mem(all_13_1_21, all_0_6_6) = all_28_0_22, yields: % 29.13/8.44 | (120) all_34_0_24 = all_28_0_22 % 29.13/8.44 | % 29.13/8.44 | Equations (120) can reduce 116 to: % 29.13/8.45 | (121) ~ (all_28_0_22 = 0) % 29.13/8.45 | % 29.13/8.45 +-Applying beta-rule and splitting (110), into two cases. % 29.13/8.45 |-Branch one: % 29.13/8.45 | (122) all_28_0_22 = 0 % 29.13/8.45 | % 29.13/8.45 | Equations (122) can reduce 121 to: % 29.13/8.45 | (95) $false % 29.13/8.45 | % 29.13/8.45 |-The branch is then unsatisfiable % 29.13/8.45 |-Branch two: % 29.13/8.45 | (121) ~ (all_28_0_22 = 0) % 29.13/8.45 | (125) all_28_1_23 = 0 % 29.13/8.45 | % 29.13/8.45 | From (125) and (109) follows: % 29.13/8.45 | (126) mem(all_13_1_21, all_0_8_8) = 0 % 29.13/8.45 | % 29.13/8.45 +-Applying beta-rule and splitting (106), into two cases. % 29.13/8.45 |-Branch one: % 29.13/8.45 | (127) ~ (mem(all_13_1_21, all_0_8_8) = 0) % 29.13/8.45 | % 29.13/8.45 | Using (126) and (127) yields: % 29.13/8.45 | (128) $false % 29.13/8.45 | % 29.13/8.45 |-The branch is then unsatisfiable % 29.13/8.45 |-Branch two: % 29.13/8.45 | (126) mem(all_13_1_21, all_0_8_8) = 0 % 29.13/8.45 | (130) ? [v0] : ? [v1] : (mem(all_13_1_21, all_0_9_9) = v1 & mem(all_13_1_21, all_0_15_15) = v0 & (v1 = 0 | v0 = 0)) % 29.13/8.45 | % 29.13/8.45 | Instantiating (130) with all_56_0_26, all_56_1_27 yields: % 29.13/8.45 | (131) mem(all_13_1_21, all_0_9_9) = all_56_0_26 & mem(all_13_1_21, all_0_15_15) = all_56_1_27 & (all_56_0_26 = 0 | all_56_1_27 = 0) % 29.13/8.45 | % 29.13/8.45 | Applying alpha-rule on (131) yields: % 29.13/8.45 | (132) mem(all_13_1_21, all_0_9_9) = all_56_0_26 % 29.13/8.45 | (133) mem(all_13_1_21, all_0_15_15) = all_56_1_27 % 29.13/8.45 | (134) all_56_0_26 = 0 | all_56_1_27 = 0 % 29.13/8.45 | % 29.13/8.45 | Instantiating formula (9) with all_34_1_25, all_0_2_2, all_0_3_3, all_0_15_15, all_13_1_21 and discharging atoms u(all_0_15_15, all_0_3_3) = all_0_2_2, mem(all_13_1_21, all_0_2_2) = all_34_1_25, yields: % 29.13/8.45 | (135) all_34_1_25 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_3_3) = v1 & mem(all_13_1_21, all_0_15_15) = v0) % 29.13/8.45 | % 29.13/8.45 +-Applying beta-rule and splitting (135), into two cases. % 29.13/8.45 |-Branch one: % 29.13/8.45 | (136) all_34_1_25 = 0 % 29.13/8.45 | % 29.13/8.45 | Equations (136) can reduce 117 to: % 29.13/8.45 | (95) $false % 29.13/8.45 | % 29.13/8.45 |-The branch is then unsatisfiable % 29.13/8.45 |-Branch two: % 29.13/8.45 | (117) ~ (all_34_1_25 = 0) % 29.13/8.45 | (139) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_3_3) = v1 & mem(all_13_1_21, all_0_15_15) = v0) % 29.13/8.45 | % 29.13/8.45 | Instantiating (139) with all_88_0_28, all_88_1_29 yields: % 29.13/8.45 | (140) ~ (all_88_0_28 = 0) & ~ (all_88_1_29 = 0) & mem(all_13_1_21, all_0_3_3) = all_88_0_28 & mem(all_13_1_21, all_0_15_15) = all_88_1_29 % 29.13/8.45 | % 29.13/8.45 | Applying alpha-rule on (140) yields: % 29.13/8.45 | (141) ~ (all_88_0_28 = 0) % 29.13/8.45 | (142) ~ (all_88_1_29 = 0) % 29.13/8.45 | (143) mem(all_13_1_21, all_0_3_3) = all_88_0_28 % 29.13/8.45 | (144) mem(all_13_1_21, all_0_15_15) = all_88_1_29 % 29.13/8.45 | % 29.13/8.45 | Instantiating formula (37) with all_13_1_21, all_0_15_15, all_88_1_29, all_56_1_27 and discharging atoms mem(all_13_1_21, all_0_15_15) = all_88_1_29, mem(all_13_1_21, all_0_15_15) = all_56_1_27, yields: % 29.13/8.45 | (145) all_88_1_29 = all_56_1_27 % 29.13/8.45 | % 29.13/8.45 | Equations (145) can reduce 142 to: % 29.13/8.45 | (146) ~ (all_56_1_27 = 0) % 29.13/8.45 | % 29.13/8.45 +-Applying beta-rule and splitting (134), into two cases. % 29.13/8.45 |-Branch one: % 29.13/8.45 | (147) all_56_0_26 = 0 % 29.13/8.45 | % 29.13/8.45 | From (147) and (132) follows: % 29.13/8.45 | (148) mem(all_13_1_21, all_0_9_9) = 0 % 29.13/8.45 | % 29.13/8.45 +-Applying beta-rule and splitting (105), into two cases. % 29.13/8.45 |-Branch one: % 29.13/8.45 | (149) ~ (mem(all_13_1_21, all_0_9_9) = 0) % 29.13/8.45 | % 29.13/8.45 | Using (148) and (149) yields: % 29.13/8.45 | (128) $false % 29.13/8.45 | % 29.13/8.45 |-The branch is then unsatisfiable % 29.13/8.45 |-Branch two: % 29.13/8.45 | (148) mem(all_13_1_21, all_0_9_9) = 0 % 29.13/8.45 | (152) ? [v0] : ? [v1] : (mem(all_13_1_21, all_0_10_10) = v1 & mem(all_13_1_21, all_0_13_13) = v0 & (v1 = 0 | v0 = 0)) % 29.13/8.45 | % 29.13/8.45 | Instantiating (152) with all_118_0_30, all_118_1_31 yields: % 29.13/8.45 | (153) mem(all_13_1_21, all_0_10_10) = all_118_0_30 & mem(all_13_1_21, all_0_13_13) = all_118_1_31 & (all_118_0_30 = 0 | all_118_1_31 = 0) % 29.13/8.45 | % 29.13/8.45 | Applying alpha-rule on (153) yields: % 29.13/8.45 | (154) mem(all_13_1_21, all_0_10_10) = all_118_0_30 % 29.13/8.45 | (155) mem(all_13_1_21, all_0_13_13) = all_118_1_31 % 29.13/8.45 | (156) all_118_0_30 = 0 | all_118_1_31 = 0 % 29.13/8.45 | % 29.13/8.45 | Instantiating formula (9) with all_88_0_28, all_0_3_3, all_0_10_10, all_0_4_4, all_13_1_21 and discharging atoms u(all_0_4_4, all_0_10_10) = all_0_3_3, mem(all_13_1_21, all_0_3_3) = all_88_0_28, yields: % 29.13/8.45 | (157) all_88_0_28 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_4_4) = v0 & mem(all_13_1_21, all_0_10_10) = v1) % 29.13/8.45 | % 29.13/8.46 +-Applying beta-rule and splitting (157), into two cases. % 29.13/8.46 |-Branch one: % 29.13/8.46 | (158) all_88_0_28 = 0 % 29.13/8.46 | % 29.13/8.46 | Equations (158) can reduce 141 to: % 29.13/8.46 | (95) $false % 29.13/8.46 | % 29.13/8.46 |-The branch is then unsatisfiable % 29.13/8.46 |-Branch two: % 29.13/8.46 | (141) ~ (all_88_0_28 = 0) % 29.13/8.46 | (161) ? [v0] : ? [v1] : ( ~ (v1 = 0) & ~ (v0 = 0) & mem(all_13_1_21, all_0_4_4) = v0 & mem(all_13_1_21, all_0_10_10) = v1) % 29.13/8.46 | % 29.13/8.46 | Instantiating (161) with all_150_0_32, all_150_1_33 yields: % 29.13/8.46 | (162) ~ (all_150_0_32 = 0) & ~ (all_150_1_33 = 0) & mem(all_13_1_21, all_0_4_4) = all_150_1_33 & mem(all_13_1_21, all_0_10_10) = all_150_0_32 % 29.13/8.46 | % 29.13/8.46 | Applying alpha-rule on (162) yields: % 29.13/8.46 | (163) ~ (all_150_0_32 = 0) % 29.13/8.46 | (164) ~ (all_150_1_33 = 0) % 29.13/8.46 | (165) mem(all_13_1_21, all_0_4_4) = all_150_1_33 % 29.13/8.46 | (166) mem(all_13_1_21, all_0_10_10) = all_150_0_32 % 29.13/8.46 | % 29.13/8.46 | Instantiating formula (37) with all_13_1_21, all_0_10_10, all_150_0_32, all_118_0_30 and discharging atoms mem(all_13_1_21, all_0_10_10) = all_150_0_32, mem(all_13_1_21, all_0_10_10) = all_118_0_30, yields: % 29.13/8.46 | (167) all_150_0_32 = all_118_0_30 % 29.13/8.46 | % 29.13/8.46 | Equations (167) can reduce 163 to: % 29.13/8.46 | (168) ~ (all_118_0_30 = 0) % 29.13/8.46 | % 29.13/8.46 +-Applying beta-rule and splitting (156), into two cases. % 29.13/8.46 |-Branch one: % 29.13/8.46 | (169) all_118_0_30 = 0 % 29.13/8.46 | % 29.13/8.46 | Equations (169) can reduce 168 to: % 29.13/8.46 | (95) $false % 29.13/8.46 | % 29.13/8.46 |-The branch is then unsatisfiable % 29.13/8.46 |-Branch two: % 29.13/8.46 | (168) ~ (all_118_0_30 = 0) % 29.13/8.46 | (172) all_118_1_31 = 0 % 29.13/8.46 | % 29.13/8.46 | From (172) and (155) follows: % 29.13/8.46 | (173) mem(all_13_1_21, all_0_13_13) = 0 % 29.13/8.46 | % 29.13/8.46 +-Applying beta-rule and splitting (102), into two cases. % 29.13/8.46 |-Branch one: % 29.13/8.46 | (174) ~ (mem(all_13_1_21, all_0_13_13) = 0) % 29.13/8.46 | % 29.13/8.46 | Using (173) and (174) yields: % 29.13/8.46 | (128) $false % 29.13/8.46 | % 29.13/8.46 |-The branch is then unsatisfiable % 29.13/8.46 |-Branch two: % 29.13/8.46 | (173) mem(all_13_1_21, all_0_13_13) = 0 % 29.13/8.46 | (177) all_13_1_21 = all_0_14_14 % 29.13/8.46 | % 29.13/8.46 | From (177) and (165) follows: % 29.13/8.46 | (178) mem(all_0_14_14, all_0_4_4) = all_150_1_33 % 29.13/8.46 | % 29.13/8.46 | Instantiating formula (18) with all_150_1_33, all_0_4_4, all_0_14_14, all_0_14_14 and discharging atoms p(all_0_14_14) = all_0_4_4, mem(all_0_14_14, all_0_4_4) = all_150_1_33, yields: % 29.13/8.46 | (179) all_150_1_33 = 0 | ? [v0] : ( ~ (v0 = 0) & subq(all_0_14_14, all_0_14_14) = v0) % 29.13/8.46 | % 29.13/8.46 +-Applying beta-rule and splitting (179), into two cases. % 29.13/8.46 |-Branch one: % 29.13/8.46 | (180) all_150_1_33 = 0 % 29.13/8.46 | % 29.13/8.46 | Equations (180) can reduce 164 to: % 29.13/8.46 | (95) $false % 29.13/8.46 | % 29.13/8.46 |-The branch is then unsatisfiable % 29.13/8.46 |-Branch two: % 29.13/8.46 | (164) ~ (all_150_1_33 = 0) % 29.13/8.46 | (183) ? [v0] : ( ~ (v0 = 0) & subq(all_0_14_14, all_0_14_14) = v0) % 29.13/8.46 | % 29.13/8.46 | Instantiating (183) with all_894_0_35 yields: % 29.13/8.46 | (184) ~ (all_894_0_35 = 0) & subq(all_0_14_14, all_0_14_14) = all_894_0_35 % 29.13/8.46 | % 29.13/8.46 | Applying alpha-rule on (184) yields: % 29.13/8.46 | (185) ~ (all_894_0_35 = 0) % 29.13/8.46 | (186) subq(all_0_14_14, all_0_14_14) = all_894_0_35 % 29.13/8.46 | % 29.13/8.46 | Instantiating formula (75) with all_894_0_35, all_0_14_14, all_0_14_14 and discharging atoms subq(all_0_14_14, all_0_14_14) = all_894_0_35, yields: % 29.13/8.46 | (187) all_894_0_35 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_14_14) = v1 & mem(v0, all_0_14_14) = 0) % 29.13/8.46 | % 29.13/8.46 +-Applying beta-rule and splitting (187), into two cases. % 29.13/8.46 |-Branch one: % 29.13/8.46 | (188) all_894_0_35 = 0 % 29.13/8.46 | % 29.13/8.46 | Equations (188) can reduce 185 to: % 29.13/8.46 | (95) $false % 29.13/8.46 | % 29.13/8.46 |-The branch is then unsatisfiable % 29.13/8.46 |-Branch two: % 29.13/8.46 | (185) ~ (all_894_0_35 = 0) % 29.13/8.46 | (191) ? [v0] : ? [v1] : ( ~ (v1 = 0) & mem(v0, all_0_14_14) = v1 & mem(v0, all_0_14_14) = 0) % 29.13/8.46 | % 29.13/8.46 | Instantiating (191) with all_1489_0_36, all_1489_1_37 yields: % 29.13/8.46 | (192) ~ (all_1489_0_36 = 0) & mem(all_1489_1_37, all_0_14_14) = all_1489_0_36 & mem(all_1489_1_37, all_0_14_14) = 0 % 29.13/8.47 | % 29.13/8.47 | Applying alpha-rule on (192) yields: % 29.13/8.47 | (193) ~ (all_1489_0_36 = 0) % 29.13/8.47 | (194) mem(all_1489_1_37, all_0_14_14) = all_1489_0_36 % 29.13/8.47 | (195) mem(all_1489_1_37, all_0_14_14) = 0 % 29.13/8.47 | % 29.13/8.47 | Instantiating formula (37) with all_1489_1_37, all_0_14_14, 0, all_1489_0_36 and discharging atoms mem(all_1489_1_37, all_0_14_14) = all_1489_0_36, mem(all_1489_1_37, all_0_14_14) = 0, yields: % 29.13/8.47 | (196) all_1489_0_36 = 0 % 29.13/8.47 | % 29.13/8.47 | Equations (196) can reduce 193 to: % 29.13/8.47 | (95) $false % 29.13/8.47 | % 29.13/8.47 |-The branch is then unsatisfiable % 29.13/8.47 |-Branch two: % 29.13/8.47 | (198) ~ (all_56_0_26 = 0) % 29.13/8.47 | (199) all_56_1_27 = 0 % 29.13/8.47 | % 29.13/8.47 | Equations (199) can reduce 146 to: % 29.13/8.47 | (95) $false % 29.13/8.47 | % 29.13/8.47 |-The branch is then unsatisfiable % 29.13/8.47 % SZS output end Proof for theBenchmark % 29.13/8.47 % 29.13/8.47 7864ms %------------------------------------------------------------------------------