%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEV567+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n014.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:02 AM UTC 2025 % Result : Theorem 8.83s 2.85s % Output : Proof 12.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEV567+1 : TPTP v9.1.0. Released v9.1.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n014.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.35 % DateTime : Mon Mar 31 12:35:49 EDT 2025 % 0.13/0.35 % CPUTime : % 0.59/0.66 ____ _ % 0.59/0.66 ___ / __ \_____(_)___ ________ __________ % 0.59/0.66 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.66 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.66 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.66 % 0.59/0.66 A Theorem Prover for First-Order Logic % 0.59/0.67 (ePrincess v.1.0) % 0.59/0.67 % 0.59/0.67 (c) Philipp Rümmer, 2009-2015 % 0.59/0.67 (c) Peter Backeman, 2014-2015 % 0.59/0.67 (contributions by Angelo Brillout, Peter Baumgartner) % 0.59/0.67 Free software under GNU Lesser General Public License (LGPL). % 0.59/0.67 Bug reports to peter@backeman.se % 0.59/0.67 % 0.59/0.67 For more information, visit http://user.uu.se/~petba168/breu/ % 0.59/0.67 % 0.59/0.67 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.70/0.74 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.93/1.14 Prover 0: Preprocessing ... % 2.89/1.51 Prover 0: Warning: ignoring some quantifiers % 3.09/1.55 Prover 0: Constructing countermodel ... % 8.43/2.85 Prover 0: proved (2110ms) % 8.83/2.85 % 8.83/2.85 No countermodel exists, formula is valid % 8.83/2.85 % SZS status Theorem for theBenchmark % 8.83/2.85 % 8.83/2.85 Generating proof ... Warning: ignoring some quantifiers % 11.68/3.53 found it (size 161) % 11.68/3.53 % 11.68/3.53 % SZS output start Proof for theBenchmark % 11.68/3.53 Assumed formulas after preprocessing and simplification: % 11.68/3.53 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : (n(v12) = v13 & n(v5) = v16 & n(v2) = v3 & n(v1) = v9 & n(v0) = v4 & n(e) = v0 & a(v17, v7) = v18 & a(v11, v12) = v19 & a(v6, v7) = v8 & a(v3, v5) = v6 & a(v1, v4) = v12 & a(v0, v4) = v7 & u(v18, v19) = v20 & u(v11, v13) = v14 & u(v8, v14) = v15 & u(v3, v16) = v17 & u(v0, v9) = v10 & s(v10) = v11 & s(v4) = v5 & s(v1) = v2 & s(v0) = v1 & subq(v15, v20) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v22 = v21 | ~ (a(v24, v23) = v22) | ~ (a(v24, v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v22 = v21 | ~ (m(v24, v23) = v22) | ~ (m(v24, v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v22 = v21 | ~ (u(v24, v23) = v22) | ~ (u(v24, v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (m(v22, v23) = v24) | ~ mem(v21, v24) | ~ mem(v21, v23)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (m(v22, v23) = v24) | ~ mem(v21, v24) | mem(v21, v22)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (m(v22, v23) = v24) | ~ mem(v21, v22) | mem(v21, v24) | mem(v21, v23)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (u(v22, v23) = v24) | ~ mem(v21, v24) | mem(v21, v23) | mem(v21, v22)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (u(v22, v23) = v24) | ~ mem(v21, v23) | mem(v21, v24)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (u(v22, v23) = v24) | ~ mem(v21, v22) | mem(v21, v24)) & ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (u(v21, v23) = v24) | ~ (s(v22) = v23) | a(v21, v22) = v24) & ! [v21] : ! [v22] : ! [v23] : (v22 = v21 | ~ (p(v23) = v22) | ~ (p(v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : (v22 = v21 | ~ (n(v23) = v22) | ~ (n(v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : (v22 = v21 | ~ (s(v23) = v22) | ~ (s(v23) = v21)) & ! [v21] : ! [v22] : ! [v23] : (v22 = v21 | ~ (s(v22) = v23) | ~ mem(v21, v23)) & ! [v21] : ! [v22] : ! [v23] : ( ~ (p(v22) = v23) | ~ mem(v22, v21) | atleast2p(v21) | subq(v21, v23)) & ! [v21] : ! [v22] : ! [v23] : ( ~ (p(v22) = v23) | ~ mem(v21, v23) | subq(v21, v22)) & ! [v21] : ! [v22] : ! [v23] : ( ~ (p(v22) = v23) | ~ subq(v21, v22) | mem(v21, v23)) & ! [v21] : ! [v22] : ! [v23] : ( ~ (a(v21, v22) = v23) | ? [v24] : (u(v21, v24) = v23 & s(v22) = v24)) & ! [v21] : ! [v22] : ! [v23] : ( ~ disj(v21, v22) | ~ mem(v23, v22) | ~ mem(v23, v21)) & ! [v21] : ! [v22] : ! [v23] : ( ~ mem(v23, v21) | ~ subq(v21, v22) | mem(v23, v22)) & ! [v21] : ! [v22] : (v22 = v21 | ~ subq(v22, v21) | ~ subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ (n(v21) = v22) | a(v21, v21) = v22) & ! [v21] : ! [v22] : ( ~ (a(v21, v21) = v22) | n(v21) = v22) & ! [v21] : ! [v22] : ( ~ (s(v21) = v22) | mem(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast15p(v22) | ~ subq(v22, v21) | atleast16p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast14p(v22) | ~ subq(v22, v21) | atleast15p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast13p(v22) | ~ subq(v22, v21) | atleast14p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast12p(v22) | ~ subq(v22, v21) | atleast13p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast11p(v22) | ~ subq(v22, v21) | atleast12p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast10p(v22) | ~ subq(v22, v21) | atleast11p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast9p(v22) | ~ subq(v22, v21) | atleast10p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast8p(v22) | ~ subq(v22, v21) | atleast9p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast7p(v22) | ~ subq(v22, v21) | atleast8p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast6p(v22) | ~ subq(v22, v21) | atleast7p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast5p(v22) | ~ subq(v22, v21) | atleast6p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast4p(v22) | ~ subq(v22, v21) | atleast5p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast3p(v22) | ~ subq(v22, v21) | atleast4p(v21) | subq(v21, v22)) & ! [v21] : ! [v22] : ( ~ atleast2p(v22) | ~ subq(v22, v21) | atleast3p(v21) | subq(v21, v22)) & ! [v21] : ( ~ atleast16p(v21) | ? [v22] : (atleast15p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast15p(v21) | ? [v22] : (atleast14p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast14p(v21) | ? [v22] : (atleast13p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast13p(v21) | ? [v22] : (atleast12p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast12p(v21) | ? [v22] : (atleast11p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast11p(v21) | ? [v22] : (atleast10p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast10p(v21) | ? [v22] : (atleast9p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast9p(v21) | ? [v22] : (atleast8p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast8p(v21) | ? [v22] : (atleast7p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast7p(v21) | ? [v22] : (atleast6p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast6p(v21) | ? [v22] : (atleast5p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast5p(v21) | ? [v22] : (atleast4p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast4p(v21) | ? [v22] : (atleast3p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast3p(v21) | ? [v22] : (atleast2p(v22) & subq(v22, v21) & ~ subq(v21, v22))) & ! [v21] : ( ~ atleast2p(v21) | ? [v22] : ? [v23] : (p(v22) = v23 & mem(v22, v21) & ~ subq(v21, v23))) & ! [v21] : ~ mem(v21, e) & ? [v21] : ? [v22] : (disj(v21, v22) | ? [v23] : (mem(v23, v22) & mem(v23, v21))) & ? [v21] : ? [v22] : (subq(v21, v22) | ? [v23] : (mem(v23, v21) & ~ mem(v23, v22)))) % 11.82/3.59 | 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 yields: % 11.82/3.59 | (1) n(all_0_8_8) = all_0_7_7 & n(all_0_15_15) = all_0_4_4 & n(all_0_18_18) = all_0_17_17 & n(all_0_19_19) = all_0_11_11 & n(all_0_20_20) = all_0_16_16 & n(e) = all_0_20_20 & a(all_0_3_3, all_0_13_13) = all_0_2_2 & a(all_0_9_9, all_0_8_8) = all_0_1_1 & a(all_0_14_14, all_0_13_13) = all_0_12_12 & a(all_0_17_17, all_0_15_15) = all_0_14_14 & a(all_0_19_19, all_0_16_16) = all_0_8_8 & a(all_0_20_20, all_0_16_16) = all_0_13_13 & u(all_0_2_2, all_0_1_1) = all_0_0_0 & u(all_0_9_9, all_0_7_7) = all_0_6_6 & u(all_0_12_12, all_0_6_6) = all_0_5_5 & u(all_0_17_17, all_0_4_4) = all_0_3_3 & u(all_0_20_20, all_0_11_11) = all_0_10_10 & s(all_0_10_10) = all_0_9_9 & s(all_0_16_16) = all_0_15_15 & s(all_0_19_19) = all_0_18_18 & s(all_0_20_20) = all_0_19_19 & subq(all_0_5_5, all_0_0_0) & ! [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] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v3) | ~ mem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v3) | mem(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v1) | mem(v0, v3) | mem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v3) | mem(v0, v2) | mem(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v2) | mem(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v1) | mem(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) & ! [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)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ mem(v1, v0) | atleast2p(v0) | subq(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ mem(v0, v2) | subq(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ subq(v0, v1) | mem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ disj(v0, v1) | ~ mem(v2, v1) | ~ mem(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ mem(v2, v0) | ~ subq(v0, v1) | mem(v2, v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ subq(v1, v0) | ~ subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) & ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | mem(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast15p(v1) | ~ subq(v1, v0) | atleast16p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast14p(v1) | ~ subq(v1, v0) | atleast15p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast13p(v1) | ~ subq(v1, v0) | atleast14p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast12p(v1) | ~ subq(v1, v0) | atleast13p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast11p(v1) | ~ subq(v1, v0) | atleast12p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast10p(v1) | ~ subq(v1, v0) | atleast11p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast9p(v1) | ~ subq(v1, v0) | atleast10p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast8p(v1) | ~ subq(v1, v0) | atleast9p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast7p(v1) | ~ subq(v1, v0) | atleast8p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast6p(v1) | ~ subq(v1, v0) | atleast7p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast5p(v1) | ~ subq(v1, v0) | atleast6p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast4p(v1) | ~ subq(v1, v0) | atleast5p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast3p(v1) | ~ subq(v1, v0) | atleast4p(v0) | subq(v0, v1)) & ! [v0] : ! [v1] : ( ~ atleast2p(v1) | ~ subq(v1, v0) | atleast3p(v0) | subq(v0, v1)) & ! [v0] : ( ~ atleast16p(v0) | ? [v1] : (atleast15p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast15p(v0) | ? [v1] : (atleast14p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast14p(v0) | ? [v1] : (atleast13p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast13p(v0) | ? [v1] : (atleast12p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast12p(v0) | ? [v1] : (atleast11p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast11p(v0) | ? [v1] : (atleast10p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast10p(v0) | ? [v1] : (atleast9p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast9p(v0) | ? [v1] : (atleast8p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast8p(v0) | ? [v1] : (atleast7p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast7p(v0) | ? [v1] : (atleast6p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast6p(v0) | ? [v1] : (atleast5p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast5p(v0) | ? [v1] : (atleast4p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast4p(v0) | ? [v1] : (atleast3p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast3p(v0) | ? [v1] : (atleast2p(v1) & subq(v1, v0) & ~ subq(v0, v1))) & ! [v0] : ( ~ atleast2p(v0) | ? [v1] : ? [v2] : (p(v1) = v2 & mem(v1, v0) & ~ subq(v0, v2))) & ! [v0] : ~ mem(v0, e) & ? [v0] : ? [v1] : (disj(v0, v1) | ? [v2] : (mem(v2, v1) & mem(v2, v0))) & ? [v0] : ? [v1] : (subq(v0, v1) | ? [v2] : (mem(v2, v0) & ~ mem(v2, v1))) % 11.82/3.61 | % 11.82/3.61 | Applying alpha-rule on (1) yields: % 11.82/3.61 | (2) subq(all_0_5_5, all_0_0_0) % 11.82/3.61 | (3) ! [v0] : ( ~ atleast14p(v0) | ? [v1] : (atleast13p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.61 | (4) ! [v0] : ( ~ atleast4p(v0) | ? [v1] : (atleast3p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.61 | (5) a(all_0_9_9, all_0_8_8) = all_0_1_1 % 11.82/3.61 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v3) | mem(v0, v2) | mem(v0, v1)) % 11.82/3.61 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v2) | mem(v0, v3)) % 11.82/3.61 | (8) ! [v0] : ( ~ atleast11p(v0) | ? [v1] : (atleast10p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.61 | (9) ! [v0] : ! [v1] : ( ~ atleast15p(v1) | ~ subq(v1, v0) | atleast16p(v0) | subq(v0, v1)) % 11.82/3.61 | (10) ! [v0] : ! [v1] : ( ~ atleast10p(v1) | ~ subq(v1, v0) | atleast11p(v0) | subq(v0, v1)) % 11.82/3.61 | (11) ! [v0] : ! [v1] : ( ~ atleast13p(v1) | ~ subq(v1, v0) | atleast14p(v0) | subq(v0, v1)) % 11.82/3.61 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ mem(v0, v2)) % 11.82/3.61 | (13) a(all_0_17_17, all_0_15_15) = all_0_14_14 % 11.82/3.61 | (14) s(all_0_16_16) = all_0_15_15 % 11.82/3.61 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ subq(v0, v1) | mem(v0, v2)) % 11.82/3.61 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ mem(v0, v2) | subq(v0, v1)) % 11.82/3.61 | (17) u(all_0_20_20, all_0_11_11) = all_0_10_10 % 11.82/3.61 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) % 11.82/3.61 | (19) ! [v0] : ( ~ atleast6p(v0) | ? [v1] : (atleast5p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.61 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (u(v3, v2) = v1) | ~ (u(v3, v2) = v0)) % 11.82/3.61 | (21) ! [v0] : ! [v1] : (v1 = v0 | ~ subq(v1, v0) | ~ subq(v0, v1)) % 11.82/3.61 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v1, v2) = v3) | ~ mem(v0, v1) | mem(v0, v3)) % 11.82/3.62 | (23) u(all_0_9_9, all_0_7_7) = all_0_6_6 % 11.82/3.62 | (24) n(all_0_15_15) = all_0_4_4 % 11.82/3.62 | (25) s(all_0_19_19) = all_0_18_18 % 11.82/3.62 | (26) n(all_0_18_18) = all_0_17_17 % 11.82/3.62 | (27) ! [v0] : ( ~ atleast10p(v0) | ? [v1] : (atleast9p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (28) a(all_0_14_14, all_0_13_13) = all_0_12_12 % 11.82/3.62 | (29) ! [v0] : ( ~ atleast9p(v0) | ? [v1] : (atleast8p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (30) ! [v0] : ( ~ atleast12p(v0) | ? [v1] : (atleast11p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (31) s(all_0_20_20) = all_0_19_19 % 11.82/3.62 | (32) ! [v0] : ( ~ atleast5p(v0) | ? [v1] : (atleast4p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (33) n(all_0_20_20) = all_0_16_16 % 11.82/3.62 | (34) u(all_0_2_2, all_0_1_1) = all_0_0_0 % 11.82/3.62 | (35) ! [v0] : ( ~ atleast3p(v0) | ? [v1] : (atleast2p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (36) ! [v0] : ! [v1] : ( ~ atleast8p(v1) | ~ subq(v1, v0) | atleast9p(v0) | subq(v0, v1)) % 11.82/3.62 | (37) ? [v0] : ? [v1] : (subq(v0, v1) | ? [v2] : (mem(v2, v0) & ~ mem(v2, v1))) % 11.82/3.62 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v1) | mem(v0, v3) | mem(v0, v2)) % 11.82/3.62 | (39) ! [v0] : ! [v1] : ( ~ atleast11p(v1) | ~ subq(v1, v0) | atleast12p(v0) | subq(v0, v1)) % 11.82/3.62 | (40) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | mem(v0, v1)) % 11.82/3.62 | (41) n(all_0_19_19) = all_0_11_11 % 11.82/3.62 | (42) ! [v0] : ( ~ atleast2p(v0) | ? [v1] : ? [v2] : (p(v1) = v2 & mem(v1, v0) & ~ subq(v0, v2))) % 11.82/3.62 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ disj(v0, v1) | ~ mem(v2, v1) | ~ mem(v2, v0)) % 11.82/3.62 | (44) n(all_0_8_8) = all_0_7_7 % 11.82/3.62 | (45) ! [v0] : ( ~ atleast8p(v0) | ? [v1] : (atleast7p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (46) ! [v0] : ( ~ atleast7p(v0) | ? [v1] : (atleast6p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (47) ! [v0] : ( ~ atleast15p(v0) | ? [v1] : (atleast14p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v3) | mem(v0, v1)) % 11.82/3.62 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ mem(v2, v0) | ~ subq(v0, v1) | mem(v2, v1)) % 11.82/3.62 | (50) ! [v0] : ! [v1] : ( ~ atleast14p(v1) | ~ subq(v1, v0) | atleast15p(v0) | subq(v0, v1)) % 11.82/3.62 | (51) ! [v0] : ! [v1] : ( ~ atleast12p(v1) | ~ subq(v1, v0) | atleast13p(v0) | subq(v0, v1)) % 11.82/3.62 | (52) ! [v0] : ~ mem(v0, e) % 11.82/3.62 | (53) a(all_0_20_20, all_0_16_16) = all_0_13_13 % 11.82/3.62 | (54) ! [v0] : ( ~ atleast13p(v0) | ? [v1] : (atleast12p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.62 | (55) a(all_0_19_19, all_0_16_16) = all_0_8_8 % 11.82/3.62 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 11.82/3.63 | (57) ! [v0] : ( ~ atleast16p(v0) | ? [v1] : (atleast15p(v1) & subq(v1, v0) & ~ subq(v0, v1))) % 11.82/3.63 | (58) ! [v0] : ! [v1] : ! [v2] : ( ~ (p(v1) = v2) | ~ mem(v1, v0) | atleast2p(v0) | subq(v0, v2)) % 11.82/3.63 | (59) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) % 11.82/3.63 | (60) ! [v0] : ! [v1] : ( ~ atleast4p(v1) | ~ subq(v1, v0) | atleast5p(v0) | subq(v0, v1)) % 11.82/3.63 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) % 11.82/3.63 | (62) ! [v0] : ! [v1] : ( ~ (a(v0, v0) = v1) | n(v0) = v1) % 11.82/3.63 | (63) ! [v0] : ! [v1] : ( ~ (n(v0) = v1) | a(v0, v0) = v1) % 11.82/3.63 | (64) a(all_0_3_3, all_0_13_13) = all_0_2_2 % 11.82/3.63 | (65) ! [v0] : ! [v1] : ( ~ atleast3p(v1) | ~ subq(v1, v0) | atleast4p(v0) | subq(v0, v1)) % 11.82/3.63 | (66) ? [v0] : ? [v1] : (disj(v0, v1) | ? [v2] : (mem(v2, v1) & mem(v2, v0))) % 11.82/3.63 | (67) ! [v0] : ! [v1] : ( ~ atleast2p(v1) | ~ subq(v1, v0) | atleast3p(v0) | subq(v0, v1)) % 11.82/3.63 | (68) ! [v0] : ! [v1] : ! [v2] : ( ~ (a(v0, v1) = v2) | ? [v3] : (u(v0, v3) = v2 & s(v1) = v3)) % 11.82/3.63 | (69) ! [v0] : ! [v1] : ( ~ atleast7p(v1) | ~ subq(v1, v0) | atleast8p(v0) | subq(v0, v1)) % 11.82/3.64 | (70) s(all_0_10_10) = all_0_9_9 % 11.82/3.64 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (u(v0, v2) = v3) | ~ (s(v1) = v2) | a(v0, v1) = v3) % 11.82/3.64 | (72) ! [v0] : ! [v1] : ( ~ atleast9p(v1) | ~ subq(v1, v0) | atleast10p(v0) | subq(v0, v1)) % 11.82/3.64 | (73) n(e) = all_0_20_20 % 11.82/3.64 | (74) u(all_0_12_12, all_0_6_6) = all_0_5_5 % 11.82/3.64 | (75) ! [v0] : ! [v1] : ( ~ atleast5p(v1) | ~ subq(v1, v0) | atleast6p(v0) | subq(v0, v1)) % 11.82/3.64 | (76) u(all_0_17_17, all_0_4_4) = all_0_3_3 % 11.82/3.64 | (77) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 11.82/3.64 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m(v1, v2) = v3) | ~ mem(v0, v3) | ~ mem(v0, v2)) % 11.82/3.64 | (79) ! [v0] : ! [v1] : ( ~ atleast6p(v1) | ~ subq(v1, v0) | atleast7p(v0) | subq(v0, v1)) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_7_7, all_0_8_8 and discharging atoms n(all_0_8_8) = all_0_7_7, yields: % 11.82/3.64 | (80) a(all_0_8_8, all_0_8_8) = all_0_7_7 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_4_4, all_0_15_15 and discharging atoms n(all_0_15_15) = all_0_4_4, yields: % 11.82/3.64 | (81) a(all_0_15_15, all_0_15_15) = all_0_4_4 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_17_17, all_0_18_18 and discharging atoms n(all_0_18_18) = all_0_17_17, yields: % 11.82/3.64 | (82) a(all_0_18_18, all_0_18_18) = all_0_17_17 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_11_11, all_0_19_19 and discharging atoms n(all_0_19_19) = all_0_11_11, yields: % 11.82/3.64 | (83) a(all_0_19_19, all_0_19_19) = all_0_11_11 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_16_16, all_0_20_20 and discharging atoms n(all_0_20_20) = all_0_16_16, yields: % 11.82/3.64 | (84) a(all_0_20_20, all_0_20_20) = all_0_16_16 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (63) with all_0_20_20, e and discharging atoms n(e) = all_0_20_20, yields: % 11.82/3.64 | (85) a(e, e) = all_0_20_20 % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) with all_0_2_2, all_0_13_13, all_0_3_3 and discharging atoms a(all_0_3_3, all_0_13_13) = all_0_2_2, yields: % 11.82/3.64 | (86) ? [v0] : (u(all_0_3_3, v0) = all_0_2_2 & s(all_0_13_13) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) with all_0_1_1, all_0_8_8, all_0_9_9 and discharging atoms a(all_0_9_9, all_0_8_8) = all_0_1_1, yields: % 11.82/3.64 | (87) ? [v0] : (u(all_0_9_9, v0) = all_0_1_1 & s(all_0_8_8) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) with all_0_12_12, all_0_13_13, all_0_14_14 and discharging atoms a(all_0_14_14, all_0_13_13) = all_0_12_12, yields: % 11.82/3.64 | (88) ? [v0] : (u(all_0_14_14, v0) = all_0_12_12 & s(all_0_13_13) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) 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: % 11.82/3.64 | (89) ? [v0] : (u(all_0_17_17, v0) = all_0_14_14 & s(all_0_15_15) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) with all_0_8_8, all_0_16_16, all_0_19_19 and discharging atoms a(all_0_19_19, all_0_16_16) = all_0_8_8, yields: % 11.82/3.64 | (90) ? [v0] : (u(all_0_19_19, v0) = all_0_8_8 & s(all_0_16_16) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (68) with all_0_13_13, all_0_16_16, all_0_20_20 and discharging atoms a(all_0_20_20, all_0_16_16) = all_0_13_13, yields: % 11.82/3.64 | (91) ? [v0] : (u(all_0_20_20, v0) = all_0_13_13 & s(all_0_16_16) = v0) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (40) with all_0_9_9, all_0_10_10 and discharging atoms s(all_0_10_10) = all_0_9_9, yields: % 11.82/3.64 | (92) mem(all_0_10_10, all_0_9_9) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (40) with all_0_15_15, all_0_16_16 and discharging atoms s(all_0_16_16) = all_0_15_15, yields: % 11.82/3.64 | (93) mem(all_0_16_16, all_0_15_15) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (40) with all_0_18_18, all_0_19_19 and discharging atoms s(all_0_19_19) = all_0_18_18, yields: % 11.82/3.64 | (94) mem(all_0_19_19, all_0_18_18) % 11.82/3.64 | % 11.82/3.64 | Instantiating formula (40) with all_0_19_19, all_0_20_20 and discharging atoms s(all_0_20_20) = all_0_19_19, yields: % 11.82/3.64 | (95) mem(all_0_20_20, all_0_19_19) % 11.82/3.64 | % 11.82/3.64 | Instantiating (89) with all_11_0_25 yields: % 11.82/3.64 | (96) u(all_0_17_17, all_11_0_25) = all_0_14_14 & s(all_0_15_15) = all_11_0_25 % 11.82/3.64 | % 11.82/3.64 | Applying alpha-rule on (96) yields: % 11.82/3.64 | (97) u(all_0_17_17, all_11_0_25) = all_0_14_14 % 11.82/3.64 | (98) s(all_0_15_15) = all_11_0_25 % 11.82/3.64 | % 11.82/3.64 | Instantiating (88) with all_13_0_26 yields: % 11.82/3.64 | (99) u(all_0_14_14, all_13_0_26) = all_0_12_12 & s(all_0_13_13) = all_13_0_26 % 11.82/3.64 | % 11.82/3.64 | Applying alpha-rule on (99) yields: % 11.82/3.64 | (100) u(all_0_14_14, all_13_0_26) = all_0_12_12 % 11.82/3.64 | (101) s(all_0_13_13) = all_13_0_26 % 11.82/3.64 | % 11.82/3.64 | Instantiating (87) with all_15_0_27 yields: % 11.82/3.64 | (102) u(all_0_9_9, all_15_0_27) = all_0_1_1 & s(all_0_8_8) = all_15_0_27 % 11.82/3.64 | % 11.82/3.64 | Applying alpha-rule on (102) yields: % 11.82/3.64 | (103) u(all_0_9_9, all_15_0_27) = all_0_1_1 % 11.82/3.64 | (104) s(all_0_8_8) = all_15_0_27 % 11.82/3.64 | % 11.82/3.64 | Instantiating (91) with all_17_0_28 yields: % 11.82/3.64 | (105) u(all_0_20_20, all_17_0_28) = all_0_13_13 & s(all_0_16_16) = all_17_0_28 % 11.82/3.65 | % 11.82/3.65 | Applying alpha-rule on (105) yields: % 11.82/3.65 | (106) u(all_0_20_20, all_17_0_28) = all_0_13_13 % 11.82/3.65 | (107) s(all_0_16_16) = all_17_0_28 % 11.82/3.65 | % 11.82/3.65 | Instantiating (90) with all_19_0_29 yields: % 11.82/3.65 | (108) u(all_0_19_19, all_19_0_29) = all_0_8_8 & s(all_0_16_16) = all_19_0_29 % 11.82/3.65 | % 11.82/3.65 | Applying alpha-rule on (108) yields: % 11.82/3.65 | (109) u(all_0_19_19, all_19_0_29) = all_0_8_8 % 11.82/3.65 | (110) s(all_0_16_16) = all_19_0_29 % 11.82/3.65 | % 11.82/3.65 | Instantiating (86) with all_21_0_30 yields: % 11.82/3.65 | (111) u(all_0_3_3, all_21_0_30) = all_0_2_2 & s(all_0_13_13) = all_21_0_30 % 11.82/3.65 | % 11.82/3.65 | Applying alpha-rule on (111) yields: % 11.82/3.65 | (112) u(all_0_3_3, all_21_0_30) = all_0_2_2 % 11.82/3.65 | (113) s(all_0_13_13) = all_21_0_30 % 11.82/3.65 | % 11.82/3.65 | Instantiating formula (56) with all_0_13_13, all_13_0_26, all_21_0_30 and discharging atoms s(all_0_13_13) = all_21_0_30, s(all_0_13_13) = all_13_0_26, yields: % 12.38/3.65 | (114) all_21_0_30 = all_13_0_26 % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (56) with all_0_16_16, all_19_0_29, all_0_15_15 and discharging atoms s(all_0_16_16) = all_19_0_29, s(all_0_16_16) = all_0_15_15, yields: % 12.38/3.65 | (115) all_19_0_29 = all_0_15_15 % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (56) with all_0_16_16, all_17_0_28, all_19_0_29 and discharging atoms s(all_0_16_16) = all_19_0_29, s(all_0_16_16) = all_17_0_28, yields: % 12.38/3.65 | (116) all_19_0_29 = all_17_0_28 % 12.38/3.65 | % 12.38/3.65 | Combining equations (115,116) yields a new equation: % 12.38/3.65 | (117) all_17_0_28 = all_0_15_15 % 12.38/3.65 | % 12.38/3.65 | Combining equations (117,116) yields a new equation: % 12.38/3.65 | (115) all_19_0_29 = all_0_15_15 % 12.38/3.65 | % 12.38/3.65 | From (114) and (112) follows: % 12.38/3.65 | (119) u(all_0_3_3, all_13_0_26) = all_0_2_2 % 12.38/3.65 | % 12.38/3.65 | From (115) and (109) follows: % 12.38/3.65 | (120) u(all_0_19_19, all_0_15_15) = all_0_8_8 % 12.38/3.65 | % 12.38/3.65 | From (117) and (106) follows: % 12.38/3.65 | (121) u(all_0_20_20, all_0_15_15) = all_0_13_13 % 12.38/3.65 | % 12.38/3.65 | From (114) and (113) follows: % 12.38/3.65 | (101) s(all_0_13_13) = all_13_0_26 % 12.38/3.65 | % 12.38/3.65 | From (117) and (107) follows: % 12.38/3.65 | (14) s(all_0_16_16) = all_0_15_15 % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_7_7, all_0_8_8, all_0_8_8 and discharging atoms a(all_0_8_8, all_0_8_8) = all_0_7_7, yields: % 12.38/3.65 | (124) ? [v0] : (u(all_0_8_8, v0) = all_0_7_7 & s(all_0_8_8) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_4_4, all_0_15_15, all_0_15_15 and discharging atoms a(all_0_15_15, all_0_15_15) = all_0_4_4, yields: % 12.38/3.65 | (125) ? [v0] : (u(all_0_15_15, v0) = all_0_4_4 & s(all_0_15_15) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_17_17, all_0_18_18, all_0_18_18 and discharging atoms a(all_0_18_18, all_0_18_18) = all_0_17_17, yields: % 12.38/3.65 | (126) ? [v0] : (u(all_0_18_18, v0) = all_0_17_17 & s(all_0_18_18) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_11_11, all_0_19_19, all_0_19_19 and discharging atoms a(all_0_19_19, all_0_19_19) = all_0_11_11, yields: % 12.38/3.65 | (127) ? [v0] : (u(all_0_19_19, v0) = all_0_11_11 & s(all_0_19_19) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_16_16, all_0_20_20, all_0_20_20 and discharging atoms a(all_0_20_20, all_0_20_20) = all_0_16_16, yields: % 12.38/3.65 | (128) ? [v0] : (u(all_0_20_20, v0) = all_0_16_16 & s(all_0_20_20) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (68) with all_0_20_20, e, e and discharging atoms a(e, e) = all_0_20_20, yields: % 12.38/3.65 | (129) ? [v0] : (u(e, v0) = all_0_20_20 & s(e) = v0) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (40) with all_13_0_26, all_0_13_13 and discharging atoms s(all_0_13_13) = all_13_0_26, yields: % 12.38/3.65 | (130) mem(all_0_13_13, all_13_0_26) % 12.38/3.65 | % 12.38/3.65 | Instantiating formula (7) with all_0_8_8, all_0_15_15, all_0_19_19, all_0_16_16 and discharging atoms u(all_0_19_19, all_0_15_15) = all_0_8_8, mem(all_0_16_16, all_0_15_15), yields: % 12.38/3.65 | (131) mem(all_0_16_16, all_0_8_8) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_13_13, all_0_15_15, all_0_20_20, all_0_16_16 and discharging atoms u(all_0_20_20, all_0_15_15) = all_0_13_13, mem(all_0_16_16, all_0_15_15), yields: % 12.38/3.66 | (132) mem(all_0_16_16, all_0_13_13) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (22) with all_0_8_8, all_0_15_15, all_0_19_19, all_0_20_20 and discharging atoms u(all_0_19_19, all_0_15_15) = all_0_8_8, mem(all_0_20_20, all_0_19_19), yields: % 12.38/3.66 | (133) mem(all_0_20_20, all_0_8_8) % 12.38/3.66 | % 12.38/3.66 | Instantiating (129) with all_33_0_31 yields: % 12.38/3.66 | (134) u(e, all_33_0_31) = all_0_20_20 & s(e) = all_33_0_31 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (134) yields: % 12.38/3.66 | (135) u(e, all_33_0_31) = all_0_20_20 % 12.38/3.66 | (136) s(e) = all_33_0_31 % 12.38/3.66 | % 12.38/3.66 | Instantiating (127) with all_35_0_32 yields: % 12.38/3.66 | (137) u(all_0_19_19, all_35_0_32) = all_0_11_11 & s(all_0_19_19) = all_35_0_32 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (137) yields: % 12.38/3.66 | (138) u(all_0_19_19, all_35_0_32) = all_0_11_11 % 12.38/3.66 | (139) s(all_0_19_19) = all_35_0_32 % 12.38/3.66 | % 12.38/3.66 | Instantiating (126) with all_37_0_33 yields: % 12.38/3.66 | (140) u(all_0_18_18, all_37_0_33) = all_0_17_17 & s(all_0_18_18) = all_37_0_33 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (140) yields: % 12.38/3.66 | (141) u(all_0_18_18, all_37_0_33) = all_0_17_17 % 12.38/3.66 | (142) s(all_0_18_18) = all_37_0_33 % 12.38/3.66 | % 12.38/3.66 | Instantiating (128) with all_39_0_34 yields: % 12.38/3.66 | (143) u(all_0_20_20, all_39_0_34) = all_0_16_16 & s(all_0_20_20) = all_39_0_34 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (143) yields: % 12.38/3.66 | (144) u(all_0_20_20, all_39_0_34) = all_0_16_16 % 12.38/3.66 | (145) s(all_0_20_20) = all_39_0_34 % 12.38/3.66 | % 12.38/3.66 | Instantiating (125) with all_41_0_35 yields: % 12.38/3.66 | (146) u(all_0_15_15, all_41_0_35) = all_0_4_4 & s(all_0_15_15) = all_41_0_35 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (146) yields: % 12.38/3.66 | (147) u(all_0_15_15, all_41_0_35) = all_0_4_4 % 12.38/3.66 | (148) s(all_0_15_15) = all_41_0_35 % 12.38/3.66 | % 12.38/3.66 | Instantiating (124) with all_43_0_36 yields: % 12.38/3.66 | (149) u(all_0_8_8, all_43_0_36) = all_0_7_7 & s(all_0_8_8) = all_43_0_36 % 12.38/3.66 | % 12.38/3.66 | Applying alpha-rule on (149) yields: % 12.38/3.66 | (150) u(all_0_8_8, all_43_0_36) = all_0_7_7 % 12.38/3.66 | (151) s(all_0_8_8) = all_43_0_36 % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (56) with all_0_8_8, all_43_0_36, all_15_0_27 and discharging atoms s(all_0_8_8) = all_43_0_36, s(all_0_8_8) = all_15_0_27, yields: % 12.38/3.66 | (152) all_43_0_36 = all_15_0_27 % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (56) with all_0_15_15, all_41_0_35, all_11_0_25 and discharging atoms s(all_0_15_15) = all_41_0_35, s(all_0_15_15) = all_11_0_25, yields: % 12.38/3.66 | (153) all_41_0_35 = all_11_0_25 % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (56) with all_0_19_19, all_35_0_32, all_0_18_18 and discharging atoms s(all_0_19_19) = all_35_0_32, s(all_0_19_19) = all_0_18_18, yields: % 12.38/3.66 | (154) all_35_0_32 = all_0_18_18 % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (56) with all_0_20_20, all_39_0_34, all_0_19_19 and discharging atoms s(all_0_20_20) = all_39_0_34, s(all_0_20_20) = all_0_19_19, yields: % 12.38/3.66 | (155) all_39_0_34 = all_0_19_19 % 12.38/3.66 | % 12.38/3.66 | From (152) and (150) follows: % 12.38/3.66 | (156) u(all_0_8_8, all_15_0_27) = all_0_7_7 % 12.38/3.66 | % 12.38/3.66 | From (153) and (147) follows: % 12.38/3.66 | (157) u(all_0_15_15, all_11_0_25) = all_0_4_4 % 12.38/3.66 | % 12.38/3.66 | From (154) and (138) follows: % 12.38/3.66 | (158) u(all_0_19_19, all_0_18_18) = all_0_11_11 % 12.38/3.66 | % 12.38/3.66 | From (155) and (144) follows: % 12.38/3.66 | (159) u(all_0_20_20, all_0_19_19) = all_0_16_16 % 12.38/3.66 | % 12.38/3.66 | From (152) and (151) follows: % 12.38/3.66 | (104) s(all_0_8_8) = all_15_0_27 % 12.38/3.66 | % 12.38/3.66 | From (153) and (148) follows: % 12.38/3.66 | (98) s(all_0_15_15) = all_11_0_25 % 12.38/3.66 | % 12.38/3.66 | From (154) and (139) follows: % 12.38/3.66 | (25) s(all_0_19_19) = all_0_18_18 % 12.38/3.66 | % 12.38/3.66 | From (155) and (145) follows: % 12.38/3.66 | (31) s(all_0_20_20) = all_0_19_19 % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_11_11, all_0_18_18, all_0_19_19, all_0_19_19 and discharging atoms u(all_0_19_19, all_0_18_18) = all_0_11_11, mem(all_0_19_19, all_0_18_18), yields: % 12.38/3.66 | (164) mem(all_0_19_19, all_0_11_11) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (40) with all_37_0_33, all_0_18_18 and discharging atoms s(all_0_18_18) = all_37_0_33, yields: % 12.38/3.66 | (165) mem(all_0_18_18, all_37_0_33) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (40) with all_33_0_31, e and discharging atoms s(e) = all_33_0_31, yields: % 12.38/3.66 | (166) mem(e, all_33_0_31) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (22) with all_0_7_7, all_15_0_27, all_0_8_8, all_0_20_20 and discharging atoms u(all_0_8_8, all_15_0_27) = all_0_7_7, mem(all_0_20_20, all_0_8_8), yields: % 12.38/3.66 | (167) mem(all_0_20_20, all_0_7_7) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_10_10, all_0_11_11, all_0_20_20, all_0_19_19 and discharging atoms u(all_0_20_20, all_0_11_11) = all_0_10_10, mem(all_0_19_19, all_0_11_11), yields: % 12.38/3.66 | (168) mem(all_0_19_19, all_0_10_10) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_6_6, all_0_7_7, all_0_9_9, all_0_20_20 and discharging atoms u(all_0_9_9, all_0_7_7) = all_0_6_6, mem(all_0_20_20, all_0_7_7), yields: % 12.38/3.66 | (169) mem(all_0_20_20, all_0_6_6) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_20_20, all_33_0_31, e, e and discharging atoms u(e, all_33_0_31) = all_0_20_20, mem(e, all_33_0_31), yields: % 12.38/3.66 | (170) mem(e, all_0_20_20) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (7) with all_0_5_5, all_0_6_6, all_0_12_12, all_0_20_20 and discharging atoms u(all_0_12_12, all_0_6_6) = all_0_5_5, mem(all_0_20_20, all_0_6_6), yields: % 12.38/3.66 | (171) mem(all_0_20_20, all_0_5_5) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (22) with all_0_16_16, all_0_19_19, all_0_20_20, e and discharging atoms u(all_0_20_20, all_0_19_19) = all_0_16_16, mem(e, all_0_20_20), yields: % 12.38/3.66 | (172) mem(e, all_0_16_16) % 12.38/3.66 | % 12.38/3.66 | Instantiating formula (49) with all_0_20_20, all_0_0_0, all_0_5_5 and discharging atoms mem(all_0_20_20, all_0_5_5), subq(all_0_5_5, all_0_0_0), yields: % 12.38/3.67 | (173) mem(all_0_20_20, all_0_0_0) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (6) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_20_20 and discharging atoms u(all_0_2_2, all_0_1_1) = all_0_0_0, mem(all_0_20_20, all_0_0_0), yields: % 12.38/3.67 | (174) mem(all_0_20_20, all_0_1_1) | mem(all_0_20_20, all_0_2_2) % 12.38/3.67 | % 12.38/3.67 +-Applying beta-rule and splitting (174), into two cases. % 12.38/3.67 |-Branch one: % 12.38/3.67 | (175) mem(all_0_20_20, all_0_1_1) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (6) with all_0_1_1, all_15_0_27, all_0_9_9, all_0_20_20 and discharging atoms u(all_0_9_9, all_15_0_27) = all_0_1_1, mem(all_0_20_20, all_0_1_1), yields: % 12.38/3.67 | (176) mem(all_0_20_20, all_15_0_27) | mem(all_0_20_20, all_0_9_9) % 12.38/3.67 | % 12.38/3.67 +-Applying beta-rule and splitting (176), into two cases. % 12.38/3.67 |-Branch one: % 12.38/3.67 | (177) mem(all_0_20_20, all_15_0_27) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (12) with all_15_0_27, all_0_8_8, all_0_20_20 and discharging atoms s(all_0_8_8) = all_15_0_27, mem(all_0_20_20, all_15_0_27), yields: % 12.38/3.67 | (178) all_0_8_8 = all_0_20_20 % 12.38/3.67 | % 12.38/3.67 | From (178) and (131) follows: % 12.38/3.67 | (179) mem(all_0_16_16, all_0_20_20) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (6) with all_0_20_20, all_33_0_31, e, all_0_16_16 and discharging atoms u(e, all_33_0_31) = all_0_20_20, mem(all_0_16_16, all_0_20_20), yields: % 12.38/3.67 | (180) mem(all_0_16_16, all_33_0_31) | mem(all_0_16_16, e) % 12.38/3.67 | % 12.38/3.67 +-Applying beta-rule and splitting (180), into two cases. % 12.38/3.67 |-Branch one: % 12.38/3.67 | (181) mem(all_0_16_16, e) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (52) with all_0_16_16 and discharging atoms mem(all_0_16_16, e), yields: % 12.38/3.67 | (182) $false % 12.38/3.67 | % 12.38/3.67 |-The branch is then unsatisfiable % 12.38/3.67 |-Branch two: % 12.38/3.67 | (183) ~ mem(all_0_16_16, e) % 12.38/3.67 | (184) mem(all_0_16_16, all_33_0_31) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (12) with all_33_0_31, e, all_0_16_16 and discharging atoms s(e) = all_33_0_31, mem(all_0_16_16, all_33_0_31), yields: % 12.38/3.67 | (185) all_0_16_16 = e % 12.38/3.67 | % 12.38/3.67 | From (185) and (172) follows: % 12.38/3.67 | (186) mem(e, e) % 12.38/3.67 | % 12.38/3.67 | From (185) and (183) follows: % 12.38/3.67 | (187) ~ mem(e, e) % 12.38/3.67 | % 12.38/3.67 | Using (186) and (187) yields: % 12.38/3.67 | (182) $false % 12.38/3.67 | % 12.38/3.67 |-The branch is then unsatisfiable % 12.38/3.67 |-Branch two: % 12.38/3.67 | (189) ~ mem(all_0_20_20, all_15_0_27) % 12.38/3.67 | (190) mem(all_0_20_20, all_0_9_9) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (12) with all_0_9_9, all_0_10_10, all_0_20_20 and discharging atoms s(all_0_10_10) = all_0_9_9, mem(all_0_20_20, all_0_9_9), yields: % 12.38/3.67 | (191) all_0_10_10 = all_0_20_20 % 12.38/3.67 | % 12.38/3.67 | From (191) and (70) follows: % 12.38/3.67 | (192) s(all_0_20_20) = all_0_9_9 % 12.38/3.67 | % 12.38/3.67 | From (191) and (92) follows: % 12.38/3.67 | (190) mem(all_0_20_20, all_0_9_9) % 12.38/3.67 | % 12.38/3.67 | From (191) and (168) follows: % 12.38/3.67 | (194) mem(all_0_19_19, all_0_20_20) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (56) with all_0_20_20, all_0_9_9, all_0_19_19 and discharging atoms s(all_0_20_20) = all_0_9_9, s(all_0_20_20) = all_0_19_19, yields: % 12.38/3.67 | (195) all_0_9_9 = all_0_19_19 % 12.38/3.67 | % 12.38/3.67 | From (195) and (190) follows: % 12.38/3.67 | (95) mem(all_0_20_20, all_0_19_19) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (6) with all_0_20_20, all_33_0_31, e, all_0_19_19 and discharging atoms u(e, all_33_0_31) = all_0_20_20, mem(all_0_19_19, all_0_20_20), yields: % 12.38/3.67 | (197) mem(all_0_19_19, all_33_0_31) | mem(all_0_19_19, e) % 12.38/3.67 | % 12.38/3.67 +-Applying beta-rule and splitting (197), into two cases. % 12.38/3.67 |-Branch one: % 12.38/3.67 | (198) mem(all_0_19_19, e) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (52) with all_0_19_19 and discharging atoms mem(all_0_19_19, e), yields: % 12.38/3.67 | (182) $false % 12.38/3.67 | % 12.38/3.67 |-The branch is then unsatisfiable % 12.38/3.67 |-Branch two: % 12.38/3.67 | (200) ~ mem(all_0_19_19, e) % 12.38/3.67 | (201) mem(all_0_19_19, all_33_0_31) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (12) with all_33_0_31, e, all_0_19_19 and discharging atoms s(e) = all_33_0_31, mem(all_0_19_19, all_33_0_31), yields: % 12.38/3.67 | (202) all_0_19_19 = e % 12.38/3.67 | % 12.38/3.67 | From (202) and (95) follows: % 12.38/3.67 | (203) mem(all_0_20_20, e) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (52) with all_0_20_20 and discharging atoms mem(all_0_20_20, e), yields: % 12.38/3.67 | (182) $false % 12.38/3.67 | % 12.38/3.67 |-The branch is then unsatisfiable % 12.38/3.67 |-Branch two: % 12.38/3.67 | (205) ~ mem(all_0_20_20, all_0_1_1) % 12.38/3.67 | (206) mem(all_0_20_20, all_0_2_2) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (6) with all_0_2_2, all_13_0_26, all_0_3_3, all_0_20_20 and discharging atoms u(all_0_3_3, all_13_0_26) = all_0_2_2, mem(all_0_20_20, all_0_2_2), yields: % 12.38/3.67 | (207) mem(all_0_20_20, all_13_0_26) | mem(all_0_20_20, all_0_3_3) % 12.38/3.67 | % 12.38/3.67 +-Applying beta-rule and splitting (207), into two cases. % 12.38/3.67 |-Branch one: % 12.38/3.67 | (208) mem(all_0_20_20, all_13_0_26) % 12.38/3.67 | % 12.38/3.67 | Instantiating formula (12) with all_13_0_26, all_0_13_13, all_0_20_20 and discharging atoms s(all_0_13_13) = all_13_0_26, mem(all_0_20_20, all_13_0_26), yields: % 12.38/3.67 | (209) all_0_13_13 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (209) and (132) follows: % 12.38/3.68 | (179) mem(all_0_16_16, all_0_20_20) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (6) with all_0_20_20, all_33_0_31, e, all_0_16_16 and discharging atoms u(e, all_33_0_31) = all_0_20_20, mem(all_0_16_16, all_0_20_20), yields: % 12.38/3.68 | (180) mem(all_0_16_16, all_33_0_31) | mem(all_0_16_16, e) % 12.38/3.68 | % 12.38/3.68 +-Applying beta-rule and splitting (180), into two cases. % 12.38/3.68 |-Branch one: % 12.38/3.68 | (181) mem(all_0_16_16, e) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (52) with all_0_16_16 and discharging atoms mem(all_0_16_16, e), yields: % 12.38/3.68 | (182) $false % 12.38/3.68 | % 12.38/3.68 |-The branch is then unsatisfiable % 12.38/3.68 |-Branch two: % 12.38/3.68 | (183) ~ mem(all_0_16_16, e) % 12.38/3.68 | (184) mem(all_0_16_16, all_33_0_31) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_33_0_31, e, all_0_16_16 and discharging atoms s(e) = all_33_0_31, mem(all_0_16_16, all_33_0_31), yields: % 12.38/3.68 | (185) all_0_16_16 = e % 12.38/3.68 | % 12.38/3.68 | From (185) and (172) follows: % 12.38/3.68 | (186) mem(e, e) % 12.38/3.68 | % 12.38/3.68 | From (185) and (183) follows: % 12.38/3.68 | (187) ~ mem(e, e) % 12.38/3.68 | % 12.38/3.68 | Using (186) and (187) yields: % 12.38/3.68 | (182) $false % 12.38/3.68 | % 12.38/3.68 |-The branch is then unsatisfiable % 12.38/3.68 |-Branch two: % 12.38/3.68 | (220) ~ mem(all_0_20_20, all_13_0_26) % 12.38/3.68 | (221) mem(all_0_20_20, all_0_3_3) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (6) with all_0_3_3, all_0_4_4, all_0_17_17, all_0_20_20 and discharging atoms u(all_0_17_17, all_0_4_4) = all_0_3_3, mem(all_0_20_20, all_0_3_3), yields: % 12.38/3.68 | (222) mem(all_0_20_20, all_0_4_4) | mem(all_0_20_20, all_0_17_17) % 12.38/3.68 | % 12.38/3.68 +-Applying beta-rule and splitting (222), into two cases. % 12.38/3.68 |-Branch one: % 12.38/3.68 | (223) mem(all_0_20_20, all_0_4_4) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (6) with all_0_4_4, all_11_0_25, all_0_15_15, all_0_20_20 and discharging atoms u(all_0_15_15, all_11_0_25) = all_0_4_4, mem(all_0_20_20, all_0_4_4), yields: % 12.38/3.68 | (224) mem(all_0_20_20, all_11_0_25) | mem(all_0_20_20, all_0_15_15) % 12.38/3.68 | % 12.38/3.68 +-Applying beta-rule and splitting (224), into two cases. % 12.38/3.68 |-Branch one: % 12.38/3.68 | (225) mem(all_0_20_20, all_11_0_25) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_11_0_25, all_0_15_15, all_0_20_20 and discharging atoms s(all_0_15_15) = all_11_0_25, mem(all_0_20_20, all_11_0_25), yields: % 12.38/3.68 | (226) all_0_15_15 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (226) and (14) follows: % 12.38/3.68 | (227) s(all_0_16_16) = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_0_20_20, all_0_16_16, e and discharging atoms s(all_0_16_16) = all_0_20_20, mem(e, all_0_20_20), yields: % 12.38/3.68 | (185) all_0_16_16 = e % 12.38/3.68 | % 12.38/3.68 | From (185) and (172) follows: % 12.38/3.68 | (186) mem(e, e) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (52) with e and discharging atoms mem(e, e), yields: % 12.38/3.68 | (182) $false % 12.38/3.68 | % 12.38/3.68 |-The branch is then unsatisfiable % 12.38/3.68 |-Branch two: % 12.38/3.68 | (231) ~ mem(all_0_20_20, all_11_0_25) % 12.38/3.68 | (232) mem(all_0_20_20, all_0_15_15) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_0_15_15, all_0_16_16, all_0_20_20 and discharging atoms s(all_0_16_16) = all_0_15_15, mem(all_0_20_20, all_0_15_15), yields: % 12.38/3.68 | (233) all_0_16_16 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (233) and (53) follows: % 12.38/3.68 | (234) a(all_0_20_20, all_0_20_20) = all_0_13_13 % 12.38/3.68 | % 12.38/3.68 | From (233) and (84) follows: % 12.38/3.68 | (235) a(all_0_20_20, all_0_20_20) = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (61) with all_0_20_20, all_0_20_20, all_0_20_20, all_0_13_13 and discharging atoms a(all_0_20_20, all_0_20_20) = all_0_13_13, a(all_0_20_20, all_0_20_20) = all_0_20_20, yields: % 12.38/3.68 | (209) all_0_13_13 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (209) and (130) follows: % 12.38/3.68 | (208) mem(all_0_20_20, all_13_0_26) % 12.38/3.68 | % 12.38/3.68 | Using (208) and (220) yields: % 12.38/3.68 | (182) $false % 12.38/3.68 | % 12.38/3.68 |-The branch is then unsatisfiable % 12.38/3.68 |-Branch two: % 12.38/3.68 | (239) ~ mem(all_0_20_20, all_0_4_4) % 12.38/3.68 | (240) mem(all_0_20_20, all_0_17_17) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (6) with all_0_17_17, all_37_0_33, all_0_18_18, all_0_20_20 and discharging atoms u(all_0_18_18, all_37_0_33) = all_0_17_17, mem(all_0_20_20, all_0_17_17), yields: % 12.38/3.68 | (241) mem(all_0_20_20, all_37_0_33) | mem(all_0_20_20, all_0_18_18) % 12.38/3.68 | % 12.38/3.68 +-Applying beta-rule and splitting (241), into two cases. % 12.38/3.68 |-Branch one: % 12.38/3.68 | (242) mem(all_0_20_20, all_37_0_33) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_37_0_33, all_0_18_18, all_0_20_20 and discharging atoms s(all_0_18_18) = all_37_0_33, mem(all_0_20_20, all_37_0_33), yields: % 12.38/3.68 | (243) all_0_18_18 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (243) and (25) follows: % 12.38/3.68 | (244) s(all_0_19_19) = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_0_20_20, all_0_19_19, e and discharging atoms s(all_0_19_19) = all_0_20_20, mem(e, all_0_20_20), yields: % 12.38/3.68 | (202) all_0_19_19 = e % 12.38/3.68 | % 12.38/3.68 | From (202) and (95) follows: % 12.38/3.68 | (203) mem(all_0_20_20, e) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (52) with all_0_20_20 and discharging atoms mem(all_0_20_20, e), yields: % 12.38/3.68 | (182) $false % 12.38/3.68 | % 12.38/3.68 |-The branch is then unsatisfiable % 12.38/3.68 |-Branch two: % 12.38/3.68 | (248) ~ mem(all_0_20_20, all_37_0_33) % 12.38/3.68 | (249) mem(all_0_20_20, all_0_18_18) % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (12) with all_0_18_18, all_0_19_19, all_0_20_20 and discharging atoms s(all_0_19_19) = all_0_18_18, mem(all_0_20_20, all_0_18_18), yields: % 12.38/3.68 | (250) all_0_19_19 = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | From (250) and (25) follows: % 12.38/3.68 | (251) s(all_0_20_20) = all_0_18_18 % 12.38/3.68 | % 12.38/3.68 | From (250) and (31) follows: % 12.38/3.68 | (252) s(all_0_20_20) = all_0_20_20 % 12.38/3.68 | % 12.38/3.68 | Instantiating formula (56) with all_0_20_20, all_0_20_20, all_0_18_18 and discharging atoms s(all_0_20_20) = all_0_18_18, s(all_0_20_20) = all_0_20_20, yields: % 12.38/3.69 | (243) all_0_18_18 = all_0_20_20 % 12.38/3.69 | % 12.38/3.69 | Instantiating formula (12) with all_0_20_20, all_0_20_20, e and discharging atoms s(all_0_20_20) = all_0_20_20, mem(e, all_0_20_20), yields: % 12.38/3.69 | (254) all_0_20_20 = e % 12.38/3.69 | % 12.38/3.69 | Combining equations (254,243) yields a new equation: % 12.38/3.69 | (255) all_0_18_18 = e % 12.38/3.69 | % 12.38/3.69 | From (255) and (165) follows: % 12.38/3.69 | (256) mem(e, all_37_0_33) % 12.38/3.69 | % 12.38/3.69 | From (254) and (248) follows: % 12.38/3.69 | (257) ~ mem(e, all_37_0_33) % 12.38/3.69 | % 12.38/3.69 | Using (256) and (257) yields: % 12.38/3.69 | (182) $false % 12.38/3.69 | % 12.38/3.69 |-The branch is then unsatisfiable % 12.38/3.69 % SZS output end Proof for theBenchmark % 12.38/3.69 % 12.38/3.69 3006ms %------------------------------------------------------------------------------