%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : RNG052+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n024.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 : 600s % DateTime : Mon Jul 18 20:25:12 EDT 2022 % Result : Theorem 9.93s 3.23s % Output : Proof 17.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : RNG052+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n024.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon May 30 06:55:36 EDT 2022 % 0.13/0.33 % CPUTime : % 0.50/0.57 ____ _ % 0.50/0.57 ___ / __ \_____(_)___ ________ __________ % 0.50/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.50/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.50/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.50/0.57 % 0.50/0.57 A Theorem Prover for First-Order Logic % 0.50/0.57 (ePrincess v.1.0) % 0.50/0.57 % 0.50/0.57 (c) Philipp Rümmer, 2009-2015 % 0.50/0.57 (c) Peter Backeman, 2014-2015 % 0.50/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.50/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.50/0.57 Bug reports to peter@backeman.se % 0.50/0.57 % 0.50/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.50/0.57 % 0.50/0.57 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.50/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.89/1.02 Prover 0: Preprocessing ... % 3.89/1.54 Prover 0: Constructing countermodel ... % 9.93/3.22 Prover 0: proved (2599ms) % 9.93/3.23 % 9.93/3.23 No countermodel exists, formula is valid % 9.93/3.23 % SZS status Theorem for theBenchmark % 9.93/3.23 % 9.93/3.23 Generating proof ... found it (size 176) % 16.82/5.01 % 16.82/5.01 % SZS output start Proof for theBenchmark % 16.82/5.01 Assumed formulas after preprocessing and simplification: % 16.82/5.01 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v1 = sz00) & sdtasasdt0(xq, xq) = xD & sdtasasdt0(xp, xq) = xE & sdtasasdt0(xp, xp) = xC & sziznziztdt0(xt) = xq & sziznziztdt0(xs) = xp & sdtlbdtrb0(xt, v1) = xB & sdtlbdtrb0(xs, v1) = xA & aDimensionOf0(xq) = v3 & aDimensionOf0(xp) = v2 & aDimensionOf0(xt) = v1 & aDimensionOf0(xs) = v1 & smndt0(sz0z00) = v0 & sdtasdt0(xR, xS) = xN & sdtasdt0(xF, xD) = xS & sdtasdt0(xE, xH) = xP & sdtasdt0(xE, xE) = v4 & sdtasdt0(xC, xG) = xR & sdtasdt0(xC, xD) = v5 & sdtasdt0(xB, xB) = xG & sdtasdt0(xA, xB) = xH & sdtasdt0(xA, xA) = xF & szszuzczcdt0(v3) = v1 & szszuzczcdt0(v2) = v1 & aVector0(xq) & aVector0(xp) & aVector0(xt) & aVector0(xs) & aScalar0(xN) & aScalar0(xS) & aScalar0(xP) & aScalar0(xR) & aScalar0(xH) & aScalar0(xG) & aScalar0(xF) & aScalar0(xE) & aScalar0(xD) & aScalar0(xC) & aScalar0(xB) & aScalar0(xA) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(v4, v5) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtasdt0(v7, v9) = v14) | ~ (sdtasdt0(v7, v8) = v13) | ~ (sdtasdt0(v6, v9) = v11) | ~ (sdtasdt0(v6, v8) = v10) | ~ (sdtpldt0(v13, v14) = v15) | ~ (sdtpldt0(v12, v15) = v16) | ~ (sdtpldt0(v10, v11) = v12) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v17] : ? [v18] : (sdtasdt0(v17, v18) = v16 & sdtpldt0(v8, v9) = v18 & sdtpldt0(v6, v7) = v17)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v8 = sz00 | ~ (sdtasasdt0(v9, v10) = v11) | ~ (sziznziztdt0(v7) = v10) | ~ (sziznziztdt0(v6) = v9) | ~ (sdtlbdtrb0(v7, v8) = v13) | ~ (sdtlbdtrb0(v6, v8) = v12) | ~ (aDimensionOf0(v7) = v8) | ~ (aDimensionOf0(v6) = v8) | ~ (sdtasdt0(v12, v13) = v14) | ~ (sdtpldt0(v11, v14) = v15) | ~ aVector0(v7) | ~ aVector0(v6) | sdtasasdt0(v6, v7) = v15) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtasdt0(v10, v11) = v12) | ~ (sdtpldt0(v8, v9) = v11) | ~ (sdtpldt0(v6, v7) = v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasdt0(v7, v9) = v17 & sdtasdt0(v7, v8) = v16 & sdtasdt0(v6, v9) = v14 & sdtasdt0(v6, v8) = v13 & sdtpldt0(v16, v17) = v18 & sdtpldt0(v15, v18) = v12 & sdtpldt0(v13, v14) = v15)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v7, v9) = v11) | ~ (sdtasdt0(v6, v8) = v10) | ~ sdtlseqdt0(v8, v9) | ~ sdtlseqdt0(v6, v7) | ~ sdtlseqdt0(sz0z00, v8) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(v10, v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v7, v8) = v10) | ~ (sdtasdt0(v6, v8) = v9) | ~ (sdtpldt0(v9, v10) = v11) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v15, v8) = v11 & sdtasdt0(v6, v12) = v13 & sdtasdt0(v6, v7) = v14 & sdtpldt0(v14, v9) = v13 & sdtpldt0(v7, v8) = v12 & sdtpldt0(v6, v7) = v15)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v6, v8) = v10) | ~ (sdtasdt0(v6, v7) = v9) | ~ (sdtpldt0(v9, v10) = v11) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v13, v8) = v14 & sdtasdt0(v7, v8) = v15 & sdtasdt0(v6, v12) = v11 & sdtpldt0(v10, v15) = v14 & sdtpldt0(v7, v8) = v12 & sdtpldt0(v6, v7) = v13)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v7, v9) = v11) | ~ (sdtpldt0(v6, v8) = v10) | ~ sdtlseqdt0(v8, v9) | ~ sdtlseqdt0(v6, v7) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(v10, v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasasdt0(v7, v7) = v9) | ~ (sdtasasdt0(v6, v6) = v8) | ~ (sdtasdt0(v8, v9) = v10) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasasdt0(v6, v7) = v13 & aDimensionOf0(v7) = v12 & aDimensionOf0(v6) = v11 & sdtasdt0(v13, v13) = v14 & ( ~ (v12 = v11) | ~ iLess0(v11, v1) | sdtlseqdt0(v14, v10)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (smndt0(v7) = v9) | ~ (smndt0(v6) = v8) | ~ (sdtasdt0(v8, v9) = v10) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtasdt0(v6, v7) = v10) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v9, v8) = v10) | ~ (sdtasdt0(v6, v7) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v7, v8) = v14 & sdtasdt0(v7, v6) = v9 & sdtasdt0(v6, v14) = v10 & sdtpldt0(v11, v8) = v12 & sdtpldt0(v7, v8) = v13 & sdtpldt0(v7, v6) = v11 & sdtpldt0(v6, v13) = v12 & sdtpldt0(v6, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v9, v8) = v10) | ~ (sdtpldt0(v6, v7) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v7, v8) = v15 & sdtasdt0(v6, v11) = v12 & sdtasdt0(v6, v8) = v14 & sdtasdt0(v6, v7) = v13 & sdtpldt0(v14, v15) = v10 & sdtpldt0(v13, v14) = v12 & sdtpldt0(v7, v8) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ (sdtasdt0(v6, v9) = v10) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v14, v8) = v10 & sdtasdt0(v7, v6) = v14 & sdtasdt0(v6, v7) = v14 & sdtpldt0(v11, v8) = v12 & sdtpldt0(v7, v8) = v13 & sdtpldt0(v7, v6) = v11 & sdtpldt0(v6, v13) = v12 & sdtpldt0(v6, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v6, v9) = v10) | ~ (sdtpldt0(v7, v8) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v13, v8) = v14 & sdtasdt0(v7, v8) = v15 & sdtasdt0(v6, v8) = v12 & sdtasdt0(v6, v7) = v11 & sdtpldt0(v12, v15) = v14 & sdtpldt0(v11, v12) = v10 & sdtpldt0(v6, v7) = v13)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v8) = v10) | ~ (sdtpldt0(v6, v7) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v12, v8) = v13 & sdtasdt0(v7, v8) = v14 & sdtasdt0(v7, v6) = v12 & sdtasdt0(v6, v14) = v13 & sdtasdt0(v6, v7) = v12 & sdtpldt0(v7, v8) = v11 & sdtpldt0(v7, v6) = v9 & sdtpldt0(v6, v11) = v10)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtpldt0(v7, v8) = v9) | ~ (sdtpldt0(v6, v9) = v10) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v12, v8) = v13 & sdtasdt0(v7, v8) = v14 & sdtasdt0(v7, v6) = v12 & sdtasdt0(v6, v14) = v13 & sdtasdt0(v6, v7) = v12 & sdtpldt0(v11, v8) = v10 & sdtpldt0(v7, v6) = v11 & sdtpldt0(v6, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = sz00 | ~ (sziznziztdt0(v6) = v9) | ~ (aDimensionOf0(v7) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sziznziztdt0(v7) = v12 & aDimensionOf0(v12) = v13 & aDimensionOf0(v9) = v11 & aDimensionOf0(v6) = v10 & ( ~ (v10 = v8) | v13 = v11))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (sdtasasdt0(v9, v8) = v7) | ~ (sdtasasdt0(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (sdtlbdtrb0(v9, v8) = v7) | ~ (sdtlbdtrb0(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (sdtasdt0(v9, v8) = v7) | ~ (sdtasdt0(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (sdtpldt0(v9, v8) = v7) | ~ (sdtpldt0(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasasdt0(v6, v7) = v8) | ~ (sdtasdt0(v8, v8) = v9) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasasdt0(v7, v7) = v13 & sdtasasdt0(v6, v6) = v12 & aDimensionOf0(v7) = v11 & aDimensionOf0(v6) = v10 & sdtasdt0(v12, v13) = v14 & ( ~ (v11 = v10) | ~ iLess0(v10, v1) | sdtlseqdt0(v9, v14)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sziznziztdt0(v7) = v9) | ~ (sziznziztdt0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : (aDimensionOf0(v9) = v13 & aDimensionOf0(v8) = v12 & aDimensionOf0(v7) = v11 & aDimensionOf0(v6) = v10 & ( ~ (v11 = v10) | v13 = v12 | v10 = sz00))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sziznziztdt0(v7) = v9) | ~ (aDimensionOf0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sziznziztdt0(v6) = v11 & aDimensionOf0(v11) = v12 & aDimensionOf0(v9) = v13 & aDimensionOf0(v7) = v10 & ( ~ (v10 = v8) | v13 = v12 | v8 = sz00))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (smndt0(v7) = v8) | ~ (sdtasdt0(v6, v8) = v9) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v10] : ? [v11] : (smndt0(v10) = v9 & smndt0(v6) = v11 & sdtasdt0(v11, v7) = v9 & sdtasdt0(v6, v7) = v10)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (smndt0(v6) = v8) | ~ (sdtasdt0(v8, v7) = v9) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v10] : ? [v11] : (smndt0(v11) = v9 & smndt0(v7) = v10 & sdtasdt0(v6, v10) = v9 & sdtasdt0(v6, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : (v8 = sz0z00 | ~ (sdtasasdt0(v6, v7) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v9] : ? [v10] : (aDimensionOf0(v7) = v10 & aDimensionOf0(v6) = v9 & ( ~ (v10 = sz00) | ~ (v9 = sz00)))) & ! [v6] : ! [v7] : ! [v8] : (v8 = sz0z00 | ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v7, v6) = v8) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ! [v8] : (v8 = sz0z00 | ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v6, v7) = v8) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ! [v8] : (v8 = sz00 | ~ (aDimensionOf0(v7) = v8) | ~ (aDimensionOf0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasasdt0(v10, v11) = v12 & sdtasasdt0(v6, v7) = v9 & sziznziztdt0(v7) = v11 & sziznziztdt0(v6) = v10 & sdtlbdtrb0(v7, v8) = v14 & sdtlbdtrb0(v6, v8) = v13 & sdtasdt0(v13, v14) = v15 & sdtpldt0(v12, v15) = v9)) & ! [v6] : ! [v7] : ! [v8] : (v8 = sz00 | ~ (aDimensionOf0(v7) = v8) | ~ (aDimensionOf0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v9] : ? [v10] : ? [v11] : (sziznziztdt0(v7) = v11 & sziznziztdt0(v6) = v9 & aDimensionOf0(v11) = v10 & aDimensionOf0(v9) = v10)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (sziznziztdt0(v8) = v7) | ~ (sziznziztdt0(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (aDimensionOf0(v8) = v7) | ~ (aDimensionOf0(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (smndt0(v8) = v7) | ~ (smndt0(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (sdtasdt0(v7, v7) = v8) | ~ (sdtasdt0(v6, v6) = v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ sdtlseqdt0(sz0z00, v6) | ~ aScalar0(v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (szszuzczcdt0(v8) = v7) | ~ (szszuzczcdt0(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (szszuzczcdt0(v7) = v8) | ~ (szszuzczcdt0(v6) = v8) | ~ aNaturalNumber0(v7) | ~ aNaturalNumber0(v6)) & ! [v6] : ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v7, v6) = v8) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v6, v7) = v8) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasasdt0(v6, v7) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | aScalar0(v8) | ? [v9] : ? [v10] : ( ~ (v10 = v9) & aDimensionOf0(v7) = v10 & aDimensionOf0(v6) = v9)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasasdt0(v6, v7) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (sdtasasdt0(v11, v12) = v13 & sziznziztdt0(v7) = v12 & sziznziztdt0(v6) = v11 & sdtlbdtrb0(v7, v10) = v15 & sdtlbdtrb0(v6, v9) = v14 & aDimensionOf0(v7) = v10 & aDimensionOf0(v6) = v9 & sdtasdt0(v14, v15) = v16 & sdtpldt0(v13, v16) = v17 & ( ~ (v10 = v9) | v17 = v8 | v9 = sz00))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtlbdtrb0(v6, v7) = v8) | ~ aVector0(v6) | ~ aNaturalNumber0(v7) | aScalar0(v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (aDimensionOf0(v7) = v8) | ~ (aDimensionOf0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ~ iLess0(v8, v1) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sdtasasdt0(v7, v7) = v12 & sdtasasdt0(v6, v7) = v9 & sdtasasdt0(v6, v6) = v11 & sdtasdt0(v11, v12) = v13 & sdtasdt0(v9, v9) = v10 & sdtlseqdt0(v10, v13))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (aDimensionOf0(v7) = v8) | ~ (aDimensionOf0(v6) = v8) | ~ aVector0(v7) | ~ aVector0(v6) | ? [v9] : (sdtasasdt0(v6, v7) = v9 & aScalar0(v9))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v7, v6) = v8) | ~ aScalar0(v6) | (smndt0(v7) = v6 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v6, v7) = sz0z00 & sdtpldt0(v6, sz0z00) = v6 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (smndt0(v6) = v7) | ~ (sdtpldt0(v6, v7) = v8) | ~ aScalar0(v6) | (smndt0(v7) = v6 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v7, v6) = sz0z00 & sdtpldt0(v6, sz0z00) = v6 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v6, v7) = v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ sdtlseqdt0(sz0z00, v6) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(sz0z00, v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v6, v7) = v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ sdtlseqdt0(sz0z00, v6) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v9] : (sdtpldt0(v6, v7) = v9 & sdtlseqdt0(sz0z00, v9))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v6, v7) = v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | aScalar0(v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v6, v7) = v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v9] : ? [v10] : ? [v11] : (smndt0(v8) = v10 & smndt0(v7) = v9 & smndt0(v6) = v11 & sdtasdt0(v11, v7) = v10 & sdtasdt0(v6, v9) = v10)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v6, v7) = v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v9] : ? [v10] : (smndt0(v7) = v10 & smndt0(v6) = v9 & sdtasdt0(v9, v10) = v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v6, v7) = v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ sdtlseqdt0(sz0z00, v6) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(sz0z00, v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v6, v7) = v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ sdtlseqdt0(sz0z00, v6) | ~ aScalar0(v7) | ~ aScalar0(v6) | ? [v9] : (sdtasdt0(v6, v7) = v9 & sdtlseqdt0(sz0z00, v9))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v6, v7) = v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | aScalar0(v8)) & ! [v6] : ! [v7] : ! [v8] : ( ~ sdtlseqdt0(v7, v8) | ~ sdtlseqdt0(v6, v7) | ~ aScalar0(v8) | ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(v6, v8)) & ! [v6] : ! [v7] : (v7 = v6 | ~ (sdtpldt0(v6, sz0z00) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v7 = v6 | ~ (sdtpldt0(sz0z00, v6) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v7 = v6 | ~ sdtlseqdt0(v7, v6) | ~ sdtlseqdt0(v6, v7) | ~ aScalar0(v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v7 = sz0z00 | ~ (sdtasdt0(v6, sz0z00) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v7 = sz0z00 | ~ (sdtasdt0(sz0z00, v6) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v7 = sz00 | ~ (aDimensionOf0(v6) = v7) | ~ aVector0(v6) | ? [v8] : (sziznziztdt0(v6) = v8 & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtlbdtrb0(v8, v10) = v11) | ~ (aDimensionOf0(v8) = v9) | ~ aNaturalNumber0(v10) | sdtlbdtrb0(v6, v10) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtlbdtrb0(v6, v10) = v11) | ~ (aDimensionOf0(v8) = v9) | ~ aNaturalNumber0(v10) | sdtlbdtrb0(v8, v10) = v11) & ! [v9] : ! [v10] : (v9 = v8 | ~ (aDimensionOf0(v9) = v10) | ~ aVector0(v9) | ? [v11] : ? [v12] : ? [v13] : (( ~ (v13 = v12) & sdtlbdtrb0(v9, v11) = v12 & sdtlbdtrb0(v6, v11) = v13 & aNaturalNumber0(v11)) | ( ~ (v11 = v7) & szszuzczcdt0(v10) = v11))) & ! [v9] : ( ~ (aDimensionOf0(v8) = v9) | szszuzczcdt0(v9) = v7) & ! [v9] : ( ~ (aDimensionOf0(v8) = v9) | aVector0(v8)))) & ! [v6] : ! [v7] : (v0 = sz0z00 | ~ (smndt0(v6) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v0 = sz0z00 | ~ (sdtasdt0(v6, sz0z00) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v0 = sz0z00 | ~ (sdtasdt0(sz0z00, v6) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v0 = sz0z00 | ~ (sdtpldt0(v6, sz0z00) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : (v0 = sz0z00 | ~ (sdtpldt0(sz0z00, v6) = v7) | ~ aScalar0(v6)) & ! [v6] : ! [v7] : ( ~ (sdtasasdt0(v6, v6) = v7) | ~ aVector0(v6) | sdtlseqdt0(sz0z00, v7)) & ! [v6] : ! [v7] : ( ~ (sziznziztdt0(v6) = v7) | ~ aVector0(v6) | ? [v8] : (aDimensionOf0(v6) = v8 & (v8 = sz00 | ( ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtlbdtrb0(v7, v10) = v11) | ~ (aDimensionOf0(v7) = v9) | ~ aNaturalNumber0(v10) | sdtlbdtrb0(v6, v10) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtlbdtrb0(v6, v10) = v11) | ~ (aDimensionOf0(v7) = v9) | ~ aNaturalNumber0(v10) | sdtlbdtrb0(v7, v10) = v11) & ! [v9] : ! [v10] : (v9 = v7 | ~ (aDimensionOf0(v9) = v10) | ~ aVector0(v9) | ? [v11] : ? [v12] : ? [v13] : (( ~ (v13 = v12) & sdtlbdtrb0(v9, v11) = v12 & sdtlbdtrb0(v6, v11) = v13 & aNaturalNumber0(v11)) | ( ~ (v11 = v8) & szszuzczcdt0(v10) = v11))) & ! [v9] : ( ~ (aDimensionOf0(v7) = v9) | szszuzczcdt0(v9) = v8) & ! [v9] : ( ~ (aDimensionOf0(v7) = v9) | aVector0(v7)))))) & ! [v6] : ! [v7] : ( ~ (sdtlbdtrb0(xq, v6) = v7) | ~ aNaturalNumber0(v6) | sdtlbdtrb0(xt, v6) = v7) & ! [v6] : ! [v7] : ( ~ (sdtlbdtrb0(xp, v6) = v7) | ~ aNaturalNumber0(v6) | sdtlbdtrb0(xs, v6) = v7) & ! [v6] : ! [v7] : ( ~ (sdtlbdtrb0(xt, v6) = v7) | ~ aNaturalNumber0(v6) | sdtlbdtrb0(xq, v6) = v7) & ! [v6] : ! [v7] : ( ~ (sdtlbdtrb0(xs, v6) = v7) | ~ aNaturalNumber0(v6) | sdtlbdtrb0(xp, v6) = v7) & ! [v6] : ! [v7] : ( ~ (aDimensionOf0(v7) = sz00) | ~ (aDimensionOf0(v6) = sz00) | ~ aVector0(v7) | ~ aVector0(v6) | sdtasasdt0(v6, v7) = sz0z00) & ! [v6] : ! [v7] : ( ~ (aDimensionOf0(v6) = v7) | ~ aVector0(v6) | aNaturalNumber0(v7)) & ! [v6] : ! [v7] : ( ~ (smndt0(v6) = v7) | ~ aScalar0(v6) | aScalar0(v7)) & ! [v6] : ! [v7] : ( ~ (smndt0(v6) = v7) | ~ aScalar0(v6) | (smndt0(v7) = v6 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v7, v6) = sz0z00 & sdtpldt0(v6, v7) = sz0z00 & sdtpldt0(v6, sz0z00) = v6 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ( ~ (sdtasdt0(v6, v6) = v7) | ~ aScalar0(v6) | sdtlseqdt0(sz0z00, v7)) & ! [v6] : ! [v7] : ( ~ (sdtasdt0(v6, sz0z00) = v7) | ~ aScalar0(v6) | ? [v8] : (smndt0(v8) = v6 & smndt0(v6) = v8 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v8, v6) = sz0z00 & sdtpldt0(v6, v8) = sz0z00 & sdtpldt0(v6, sz0z00) = v6 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ( ~ (sdtasdt0(sz0z00, v6) = v7) | ~ aScalar0(v6) | ? [v8] : (smndt0(v8) = v6 & smndt0(v6) = v8 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtpldt0(v8, v6) = sz0z00 & sdtpldt0(v6, v8) = sz0z00 & sdtpldt0(v6, sz0z00) = v6 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, sz0z00) = v7) | ~ aScalar0(v6) | ? [v8] : (smndt0(v8) = v6 & smndt0(v6) = v8 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v8, v6) = sz0z00 & sdtpldt0(v6, v8) = sz0z00 & sdtpldt0(sz0z00, v6) = v6)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(sz0z00, v6) = v7) | ~ aScalar0(v6) | ? [v8] : (smndt0(v8) = v6 & smndt0(v6) = v8 & sdtasdt0(v6, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v6) = sz0z00 & sdtpldt0(v8, v6) = sz0z00 & sdtpldt0(v6, v8) = sz0z00 & sdtpldt0(v6, sz0z00) = v6)) & ! [v6] : ! [v7] : ( ~ (szszuzczcdt0(v6) = v7) | ~ aNaturalNumber0(v6) | iLess0(v6, v7)) & ! [v6] : ! [v7] : ( ~ (szszuzczcdt0(v6) = v7) | ~ aNaturalNumber0(v6) | aNaturalNumber0(v7)) & ! [v6] : ! [v7] : ( ~ aScalar0(v7) | ~ aScalar0(v6) | sdtlseqdt0(v7, v6) | sdtlseqdt0(v6, v7)) & ! [v6] : (v6 = sz00 | ~ aNaturalNumber0(v6) | ? [v7] : (szszuzczcdt0(v7) = v6 & aNaturalNumber0(v7))) & ! [v6] : ( ~ (szszuzczcdt0(v6) = sz00) | ~ aNaturalNumber0(v6)) & ! [v6] : ( ~ aScalar0(v6) | sdtlseqdt0(v6, v6))) % 17.39/5.11 | 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 yields: % 17.39/5.11 | (1) ~ (all_0_4_4 = sz00) & sdtasasdt0(xq, xq) = xD & sdtasasdt0(xp, xq) = xE & sdtasasdt0(xp, xp) = xC & sziznziztdt0(xt) = xq & sziznziztdt0(xs) = xp & sdtlbdtrb0(xt, all_0_4_4) = xB & sdtlbdtrb0(xs, all_0_4_4) = xA & aDimensionOf0(xq) = all_0_2_2 & aDimensionOf0(xp) = all_0_3_3 & aDimensionOf0(xt) = all_0_4_4 & aDimensionOf0(xs) = all_0_4_4 & smndt0(sz0z00) = all_0_5_5 & sdtasdt0(xR, xS) = xN & sdtasdt0(xF, xD) = xS & sdtasdt0(xE, xH) = xP & sdtasdt0(xE, xE) = all_0_1_1 & sdtasdt0(xC, xG) = xR & sdtasdt0(xC, xD) = all_0_0_0 & sdtasdt0(xB, xB) = xG & sdtasdt0(xA, xB) = xH & sdtasdt0(xA, xA) = xF & szszuzczcdt0(all_0_2_2) = all_0_4_4 & szszuzczcdt0(all_0_3_3) = all_0_4_4 & aVector0(xq) & aVector0(xp) & aVector0(xt) & aVector0(xs) & aScalar0(xN) & aScalar0(xS) & aScalar0(xP) & aScalar0(xR) & aScalar0(xH) & aScalar0(xG) & aScalar0(xF) & aScalar0(xE) & aScalar0(xD) & aScalar0(xC) & aScalar0(xB) & aScalar0(xA) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(all_0_1_1, all_0_0_0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v1, v3) = v8) | ~ (sdtasdt0(v1, v2) = v7) | ~ (sdtasdt0(v0, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtpldt0(v7, v8) = v9) | ~ (sdtpldt0(v6, v9) = v10) | ~ (sdtpldt0(v4, v5) = v6) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v11] : ? [v12] : (sdtasdt0(v11, v12) = v10 & sdtpldt0(v2, v3) = v12 & sdtpldt0(v0, v1) = v11)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v2 = sz00 | ~ (sdtasasdt0(v3, v4) = v5) | ~ (sziznziztdt0(v1) = v4) | ~ (sziznziztdt0(v0) = v3) | ~ (sdtlbdtrb0(v1, v2) = v7) | ~ (sdtlbdtrb0(v0, v2) = v6) | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ (sdtasdt0(v6, v7) = v8) | ~ (sdtpldt0(v5, v8) = v9) | ~ aVector0(v1) | ~ aVector0(v0) | sdtasasdt0(v0, v1) = v9) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v4, v5) = v6) | ~ (sdtpldt0(v2, v3) = v5) | ~ (sdtpldt0(v0, v1) = v4) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtasdt0(v1, v3) = v11 & sdtasdt0(v1, v2) = v10 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) = v7 & sdtpldt0(v10, v11) = v12 & sdtpldt0(v9, v12) = v6 & sdtpldt0(v7, v8) = v9)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v0, v1) | ~ sdtlseqdt0(sz0z00, v2) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v2) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v9, v2) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v3) = v7 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v9)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v4, v9) = v8 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasasdt0(v1, v1) = v3) | ~ (sdtasasdt0(v0, v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v0, v1) = v7 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & sdtasdt0(v7, v7) = v8 & ( ~ (v6 = v5) | ~ iLess0(v5, all_0_4_4) | sdtlseqdt0(v8, v4)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtasdt0(v0, v1) = v4) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v3 & sdtasdt0(v0, v8) = v4 & sdtpldt0(v5, v2) = v6 & sdtpldt0(v1, v2) = v7 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v7) = v6 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v5) = v6 & sdtasdt0(v0, v2) = v8 & sdtasdt0(v0, v1) = v7 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v7, v8) = v6 & sdtpldt0(v1, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v8, v2) = v4 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v5, v2) = v6 & sdtpldt0(v1, v2) = v7 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v7) = v6 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v6, v9) = v8 & sdtpldt0(v5, v6) = v4 & sdtpldt0(v0, v1) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v6, v2) = v7 & sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v8) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v1, v2) = v5 & sdtpldt0(v1, v0) = v3 & sdtpldt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v6, v2) = v7 & sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v8) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v5, v2) = v4 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = sz00 | ~ (sziznziztdt0(v0) = v3) | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sziznziztdt0(v1) = v6 & aDimensionOf0(v6) = v7 & aDimensionOf0(v3) = v5 & aDimensionOf0(v0) = v4 & ( ~ (v4 = v2) | v7 = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ (sdtasdt0(v2, v2) = v3) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v1, v1) = v7 & sdtasasdt0(v0, v0) = v6 & aDimensionOf0(v1) = v5 & aDimensionOf0(v0) = v4 & sdtasdt0(v6, v7) = v8 & ( ~ (v5 = v4) | ~ iLess0(v4, all_0_4_4) | sdtlseqdt0(v3, v8)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (aDimensionOf0(v3) = v7 & aDimensionOf0(v2) = v6 & aDimensionOf0(v1) = v5 & aDimensionOf0(v0) = v4 & ( ~ (v5 = v4) | v7 = v6 | v4 = sz00))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sziznziztdt0(v0) = v5 & aDimensionOf0(v5) = v6 & aDimensionOf0(v3) = v7 & aDimensionOf0(v1) = v4 & ( ~ (v4 = v2) | v7 = v6 | v2 = sz00))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v1) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v4] : ? [v5] : (smndt0(v4) = v3 & smndt0(v0) = v5 & sdtasdt0(v5, v1) = v3 & sdtasdt0(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v1) = v3) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v4] : ? [v5] : (smndt0(v5) = v3 & smndt0(v1) = v4 & sdtasdt0(v0, v4) = v3 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : (aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3 & ( ~ (v4 = sz00) | ~ (v3 = sz00)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasasdt0(v4, v5) = v6 & sdtasasdt0(v0, v1) = v3 & sziznziztdt0(v1) = v5 & sziznziztdt0(v0) = v4 & sdtlbdtrb0(v1, v2) = v8 & sdtlbdtrb0(v0, v2) = v7 & sdtasdt0(v7, v8) = v9 & sdtpldt0(v6, v9) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : (sziznziztdt0(v1) = v5 & sziznziztdt0(v0) = v3 & aDimensionOf0(v5) = v4 & aDimensionOf0(v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sdtasdt0(v1, v1) = v2) | ~ (sdtasdt0(v0, v0) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | aScalar0(v2) | ? [v3] : ? [v4] : ( ~ (v4 = v3) & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : (sdtasasdt0(v5, v6) = v7 & sziznziztdt0(v1) = v6 & sziznziztdt0(v0) = v5 & sdtlbdtrb0(v1, v4) = v9 & sdtlbdtrb0(v0, v3) = v8 & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3 & sdtasdt0(v8, v9) = v10 & sdtpldt0(v7, v10) = v11 & ( ~ (v4 = v3) | v11 = v2 | v3 = sz00))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | aScalar0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ~ iLess0(v2, all_0_4_4) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtasasdt0(v1, v1) = v6 & sdtasasdt0(v0, v1) = v3 & sdtasasdt0(v0, v0) = v5 & sdtasdt0(v5, v6) = v7 & sdtasdt0(v3, v3) = v4 & sdtlseqdt0(v4, v7))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : (sdtasasdt0(v0, v1) = v3 & aScalar0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v0, v1) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v1, v0) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : (sdtpldt0(v0, v1) = v3 & sdtlseqdt0(sz0z00, v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : ? [v4] : ? [v5] : (smndt0(v2) = v4 & smndt0(v1) = v3 & smndt0(v0) = v5 & sdtasdt0(v5, v1) = v4 & sdtasdt0(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : ? [v4] : (smndt0(v1) = v4 & smndt0(v0) = v3 & sdtasdt0(v3, v4) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : (sdtasdt0(v0, v1) = v3 & sdtlseqdt0(sz0z00, v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v0, v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (sziznziztdt0(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v2, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v0, v4) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v2, v4) = v5) & ! [v3] : ! [v4] : (v3 = v2 | ~ (aDimensionOf0(v3) = v4) | ~ aVector0(v3) | ? [v5] : ? [v6] : ? [v7] : (( ~ (v7 = v6) & sdtlbdtrb0(v3, v5) = v6 & sdtlbdtrb0(v0, v5) = v7 & aNaturalNumber0(v5)) | ( ~ (v5 = v1) & szszuzczcdt0(v4) = v5))) & ! [v3] : ( ~ (aDimensionOf0(v2) = v3) | szszuzczcdt0(v3) = v1) & ! [v3] : ( ~ (aDimensionOf0(v2) = v3) | aVector0(v2)))) & ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1)) & ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (aDimensionOf0(v0) = v2 & (v2 = sz00 | ( ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v1, v4) = v5) | ~ (aDimensionOf0(v1) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v0, v4) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v1) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v1, v4) = v5) & ! [v3] : ! [v4] : (v3 = v1 | ~ (aDimensionOf0(v3) = v4) | ~ aVector0(v3) | ? [v5] : ? [v6] : ? [v7] : (( ~ (v7 = v6) & sdtlbdtrb0(v3, v5) = v6 & sdtlbdtrb0(v0, v5) = v7 & aNaturalNumber0(v5)) | ( ~ (v5 = v2) & szszuzczcdt0(v4) = v5))) & ! [v3] : ( ~ (aDimensionOf0(v1) = v3) | szszuzczcdt0(v3) = v2) & ! [v3] : ( ~ (aDimensionOf0(v1) = v3) | aVector0(v1)))))) & ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xq, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xt, v0) = v1) & ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xp, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xs, v0) = v1) & ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xt, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xq, v0) = v1) & ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xs, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xp, v0) = v1) & ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v1) = sz00) | ~ (aDimensionOf0(v0) = sz00) | ~ aVector0(v1) | ~ aVector0(v0) | sdtasasdt0(v0, v1) = sz0z00) & ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | aNaturalNumber0(v1)) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | aScalar0(v1)) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v1, v0) = sz0z00 & sdtpldt0(v0, v1) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(sz0z00, v0) = v0)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v1)) & ! [v0] : ! [v1] : ( ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) & ! [v0] : (v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1))) & ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aNaturalNumber0(v0)) & ! [v0] : ( ~ aScalar0(v0) | sdtlseqdt0(v0, v0)) % 17.55/5.14 | % 17.55/5.14 | Applying alpha-rule on (1) yields: % 17.55/5.14 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (aDimensionOf0(v3) = v7 & aDimensionOf0(v2) = v6 & aDimensionOf0(v1) = v5 & aDimensionOf0(v0) = v4 & ( ~ (v5 = v4) | v7 = v6 | v4 = sz00))) % 17.55/5.14 | (3) aVector0(xq) % 17.55/5.14 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v8, v2) = v4 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v5, v2) = v6 & sdtpldt0(v1, v2) = v7 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v7) = v6 & sdtpldt0(v0, v1) = v5)) % 17.55/5.14 | (5) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 17.55/5.14 | (6) sdtasdt0(xA, xA) = xF % 17.55/5.14 | (7) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.14 | (8) sdtasdt0(xB, xB) = xG % 17.55/5.14 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v4, v5) = v6) | ~ (sdtpldt0(v2, v3) = v5) | ~ (sdtpldt0(v0, v1) = v4) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtasdt0(v1, v3) = v11 & sdtasdt0(v1, v2) = v10 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) = v7 & sdtpldt0(v10, v11) = v12 & sdtpldt0(v9, v12) = v6 & sdtpldt0(v7, v8) = v9)) % 17.55/5.14 | (10) smndt0(sz0z00) = all_0_5_5 % 17.55/5.14 | (11) aDimensionOf0(xs) = all_0_4_4 % 17.55/5.14 | (12) sdtasdt0(xC, xD) = all_0_0_0 % 17.55/5.14 | (13) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : (sdtasasdt0(v5, v6) = v7 & sziznziztdt0(v1) = v6 & sziznziztdt0(v0) = v5 & sdtlbdtrb0(v1, v4) = v9 & sdtlbdtrb0(v0, v3) = v8 & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3 & sdtasdt0(v8, v9) = v10 & sdtpldt0(v7, v10) = v11 & ( ~ (v4 = v3) | v11 = v2 | v3 = sz00))) % 17.55/5.14 | (14) ! [v0] : ! [v1] : ! [v2] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) % 17.55/5.14 | (15) sziznziztdt0(xt) = xq % 17.55/5.14 | (16) ~ sdtlseqdt0(all_0_1_1, all_0_0_0) % 17.55/5.14 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = sz00 | ~ (sziznziztdt0(v0) = v3) | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sziznziztdt0(v1) = v6 & aDimensionOf0(v6) = v7 & aDimensionOf0(v3) = v5 & aDimensionOf0(v0) = v4 & ( ~ (v4 = v2) | v7 = v5))) % 17.55/5.14 | (18) aScalar0(xH) % 17.55/5.14 | (19) ! [v0] : ! [v1] : ! [v2] : ( ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : (sdtasasdt0(v0, v1) = v3 & aScalar0(v3))) % 17.55/5.14 | (20) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 17.55/5.14 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v0, v1) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.15 | (22) aDimensionOf0(xq) = all_0_2_2 % 17.55/5.15 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) % 17.55/5.15 | (24) aDimensionOf0(xp) = all_0_3_3 % 17.55/5.15 | (25) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | aScalar0(v1)) % 17.55/5.15 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v1) = v3) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v4] : ? [v5] : (smndt0(v5) = v3 & smndt0(v1) = v4 & sdtasdt0(v0, v4) = v3 & sdtasdt0(v0, v1) = v5)) % 17.55/5.15 | (27) ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 17.55/5.15 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 17.55/5.15 | (29) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xq, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xt, v0) = v1) % 17.55/5.15 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : (sdtasdt0(v0, v1) = v3 & sdtlseqdt0(sz0z00, v3))) % 17.55/5.15 | (31) ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 17.55/5.15 | (32) ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 17.55/5.15 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 17.55/5.15 | (34) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v1)) % 17.55/5.15 | (35) ! [v0] : (v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1))) % 17.55/5.15 | (36) aVector0(xp) % 17.55/5.15 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | aScalar0(v2)) % 17.55/5.15 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : ? [v4] : (smndt0(v1) = v4 & smndt0(v0) = v3 & sdtasdt0(v3, v4) = v2)) % 17.55/5.15 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) % 17.55/5.15 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v4, v9) = v8 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v7)) % 17.55/5.15 | (41) szszuzczcdt0(all_0_2_2) = all_0_4_4 % 17.55/5.15 | (42) ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aNaturalNumber0(v0)) % 17.55/5.15 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v2) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v9, v2) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v3) = v7 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v9)) % 17.55/5.15 | (44) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v0, v2)) % 17.55/5.15 | (45) aScalar0(xA) % 17.55/5.15 | (46) ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ aScalar0(v0)) % 17.55/5.15 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 17.55/5.15 | (48) aScalar0(xE) % 17.55/5.15 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v0, v1) | ~ sdtlseqdt0(sz0z00, v2) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v4, v5)) % 17.55/5.15 | (50) sziznziztdt0(xs) = xp % 17.55/5.15 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v5) = v6 & sdtasdt0(v0, v2) = v8 & sdtasdt0(v0, v1) = v7 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v7, v8) = v6 & sdtpldt0(v1, v2) = v5)) % 17.55/5.15 | (52) ! [v0] : ! [v1] : (all_0_5_5 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 17.55/5.15 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : ? [v4] : ? [v5] : (smndt0(v2) = v4 & smndt0(v1) = v3 & smndt0(v0) = v5 & sdtasdt0(v5, v1) = v4 & sdtasdt0(v0, v3) = v4)) % 17.55/5.15 | (54) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v1) = sz00) | ~ (aDimensionOf0(v0) = sz00) | ~ aVector0(v1) | ~ aVector0(v0) | sdtasasdt0(v0, v1) = sz0z00) % 17.55/5.16 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 17.55/5.16 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sdtasdt0(v1, v1) = v2) | ~ (sdtasdt0(v0, v0) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 17.55/5.16 | (57) ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (aDimensionOf0(v0) = v2 & (v2 = sz00 | ( ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v1, v4) = v5) | ~ (aDimensionOf0(v1) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v0, v4) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v1) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v1, v4) = v5) & ! [v3] : ! [v4] : (v3 = v1 | ~ (aDimensionOf0(v3) = v4) | ~ aVector0(v3) | ? [v5] : ? [v6] : ? [v7] : (( ~ (v7 = v6) & sdtlbdtrb0(v3, v5) = v6 & sdtlbdtrb0(v0, v5) = v7 & aNaturalNumber0(v5)) | ( ~ (v5 = v2) & szszuzczcdt0(v4) = v5))) & ! [v3] : ( ~ (aDimensionOf0(v1) = v3) | szszuzczcdt0(v3) = v2) & ! [v3] : ( ~ (aDimensionOf0(v1) = v3) | aVector0(v1)))))) % 17.55/5.16 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v1) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v4] : ? [v5] : (smndt0(v4) = v3 & smndt0(v0) = v5 & sdtasdt0(v5, v1) = v3 & sdtasdt0(v0, v1) = v4)) % 17.55/5.16 | (59) ! [v0] : ! [v1] : ! [v2] : (all_0_5_5 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 17.55/5.16 | (60) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : (aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3 & ( ~ (v4 = sz00) | ~ (v3 = sz00)))) % 17.55/5.16 | (61) ! [v0] : ( ~ aScalar0(v0) | sdtlseqdt0(v0, v0)) % 17.55/5.16 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v1, v0) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.16 | (63) aScalar0(xR) % 17.55/5.16 | (64) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 17.55/5.16 | (65) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xs, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xp, v0) = v1) % 17.55/5.16 | (66) aScalar0(xC) % 17.55/5.16 | (67) sdtasdt0(xE, xE) = all_0_1_1 % 17.55/5.16 | (68) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 17.55/5.16 | (69) aScalar0(xB) % 17.55/5.16 | (70) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0)) % 17.55/5.16 | (71) sdtasdt0(xE, xH) = xP % 17.55/5.16 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v4, v5)) % 17.55/5.16 | (73) sdtasasdt0(xp, xp) = xC % 17.55/5.16 | (74) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) % 17.55/5.16 | (75) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v1)) % 17.55/5.16 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v6, v9) = v8 & sdtpldt0(v5, v6) = v4 & sdtpldt0(v0, v1) = v7)) % 17.55/5.16 | (77) aScalar0(xF) % 17.55/5.16 | (78) szszuzczcdt0(all_0_3_3) = all_0_4_4 % 17.55/5.16 | (79) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : (sdtpldt0(v0, v1) = v3 & sdtlseqdt0(sz0z00, v3))) % 17.55/5.16 | (80) aScalar0(xS) % 17.55/5.16 | (81) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : (sziznziztdt0(v1) = v5 & sziznziztdt0(v0) = v3 & aDimensionOf0(v5) = v4 & aDimensionOf0(v3) = v4)) % 17.55/5.16 | (82) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | (smndt0(v1) = v0 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v1, v0) = sz0z00 & sdtpldt0(v0, v1) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.16 | (83) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasasdt0(v4, v5) = v6 & sdtasasdt0(v0, v1) = v3 & sziznziztdt0(v1) = v5 & sziznziztdt0(v0) = v4 & sdtlbdtrb0(v1, v2) = v8 & sdtlbdtrb0(v0, v2) = v7 & sdtasdt0(v7, v8) = v9 & sdtpldt0(v6, v9) = v3)) % 17.55/5.16 | (84) ! [v0] : ! [v1] : (v1 = sz00 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (sziznziztdt0(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v2, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v0, v4) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ aNaturalNumber0(v4) | sdtlbdtrb0(v2, v4) = v5) & ! [v3] : ! [v4] : (v3 = v2 | ~ (aDimensionOf0(v3) = v4) | ~ aVector0(v3) | ? [v5] : ? [v6] : ? [v7] : (( ~ (v7 = v6) & sdtlbdtrb0(v3, v5) = v6 & sdtlbdtrb0(v0, v5) = v7 & aNaturalNumber0(v5)) | ( ~ (v5 = v1) & szszuzczcdt0(v4) = v5))) & ! [v3] : ( ~ (aDimensionOf0(v2) = v3) | szszuzczcdt0(v3) = v1) & ! [v3] : ( ~ (aDimensionOf0(v2) = v3) | aVector0(v2)))) % 17.55/5.16 | (85) aVector0(xt) % 17.55/5.16 | (86) aNaturalNumber0(sz00) % 17.55/5.16 | (87) sdtasdt0(xF, xD) = xS % 17.55/5.16 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) % 17.55/5.16 | (89) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 17.55/5.17 | (90) sdtasdt0(xA, xB) = xH % 17.55/5.17 | (91) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | aNaturalNumber0(v1)) % 17.55/5.17 | (92) sdtasasdt0(xp, xq) = xE % 17.55/5.17 | (93) aVector0(xs) % 17.55/5.17 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.17 | (95) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v6, v2) = v7 & sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v8) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v5, v2) = v4 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v1) = v5)) % 17.55/5.17 | (96) aDimensionOf0(xt) = all_0_4_4 % 17.55/5.17 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v1, v3) = v8) | ~ (sdtasdt0(v1, v2) = v7) | ~ (sdtasdt0(v0, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtpldt0(v7, v8) = v9) | ~ (sdtpldt0(v6, v9) = v10) | ~ (sdtpldt0(v4, v5) = v6) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v11] : ? [v12] : (sdtasdt0(v11, v12) = v10 & sdtpldt0(v2, v3) = v12 & sdtpldt0(v0, v1) = v11)) % 17.55/5.17 | (98) sdtasdt0(xC, xG) = xR % 17.55/5.17 | (99) ! [v0] : ! [v1] : ( ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) % 17.55/5.17 | (100) ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 17.55/5.17 | (101) aScalar0(sz0z00) % 17.55/5.17 | (102) ! [v0] : ! [v1] : ! [v2] : ( ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ~ iLess0(v2, all_0_4_4) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtasasdt0(v1, v1) = v6 & sdtasasdt0(v0, v1) = v3 & sdtasasdt0(v0, v0) = v5 & sdtasdt0(v5, v6) = v7 & sdtasdt0(v3, v3) = v4 & sdtlseqdt0(v4, v7))) % 17.55/5.17 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasasdt0(v1, v1) = v3) | ~ (sdtasasdt0(v0, v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v0, v1) = v7 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & sdtasdt0(v7, v7) = v8 & ( ~ (v6 = v5) | ~ iLess0(v5, all_0_4_4) | sdtlseqdt0(v8, v4)))) % 17.55/5.17 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 17.55/5.17 | (105) sdtlbdtrb0(xs, all_0_4_4) = xA % 17.55/5.17 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v6, v2) = v7 & sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v8) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v1, v2) = v5 & sdtpldt0(v1, v0) = v3 & sdtpldt0(v0, v5) = v4)) % 17.55/5.17 | (107) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 17.55/5.17 | (108) sdtasdt0(xR, xS) = xN % 17.55/5.17 | (109) aScalar0(xG) % 17.55/5.17 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 17.55/5.17 | (111) sdtasasdt0(xq, xq) = xD % 17.55/5.17 | (112) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xp, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xs, v0) = v1) % 17.55/5.17 | (113) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 17.55/5.17 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtasdt0(v0, v1) = v4) % 17.55/5.17 | (115) aScalar0(xN) % 17.55/5.17 | (116) ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 17.55/5.17 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v1, v0) = v3 & sdtasdt0(v0, v8) = v4 & sdtpldt0(v5, v2) = v6 & sdtpldt0(v1, v2) = v7 & sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v7) = v6 & sdtpldt0(v0, v1) = v5)) % 17.55/5.17 | (118) aScalar0(xP) % 17.55/5.17 | (119) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sziznziztdt0(v0) = v5 & aDimensionOf0(v5) = v6 & aDimensionOf0(v3) = v7 & aDimensionOf0(v1) = v4 & ( ~ (v4 = v2) | v7 = v6 | v2 = sz00))) % 17.55/5.17 | (120) ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1)) % 17.55/5.17 | (121) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) % 17.55/5.17 | (122) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xt, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xq, v0) = v1) % 17.55/5.17 | (123) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ (sdtasdt0(v2, v2) = v3) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v1, v1) = v7 & sdtasasdt0(v0, v0) = v6 & aDimensionOf0(v1) = v5 & aDimensionOf0(v0) = v4 & sdtasdt0(v6, v7) = v8 & ( ~ (v5 = v4) | ~ iLess0(v4, all_0_4_4) | sdtlseqdt0(v3, v8)))) % 17.55/5.17 | (124) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | aScalar0(v2) | ? [v3] : ? [v4] : ( ~ (v4 = v3) & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3)) % 17.55/5.17 | (125) aScalar0(xD) % 17.55/5.17 | (126) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(sz0z00, v0) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.17 | (127) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0) | ? [v2] : (smndt0(v2) = v0 & smndt0(v0) = v2 & sdtasdt0(v0, sz0z00) = sz0z00 & sdtpldt0(v2, v0) = sz0z00 & sdtpldt0(v0, v2) = sz0z00 & sdtpldt0(v0, sz0z00) = v0 & sdtpldt0(sz0z00, v0) = v0)) % 17.55/5.17 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v2 = sz00 | ~ (sdtasasdt0(v3, v4) = v5) | ~ (sziznziztdt0(v1) = v4) | ~ (sziznziztdt0(v0) = v3) | ~ (sdtlbdtrb0(v1, v2) = v7) | ~ (sdtlbdtrb0(v0, v2) = v6) | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ (sdtasdt0(v6, v7) = v8) | ~ (sdtpldt0(v5, v8) = v9) | ~ aVector0(v1) | ~ aVector0(v0) | sdtasasdt0(v0, v1) = v9) % 17.55/5.17 | (129) sdtlbdtrb0(xt, all_0_4_4) = xB % 17.55/5.17 | (130) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (13) with xD, xq, xq and discharging atoms sdtasasdt0(xq, xq) = xD, aVector0(xq), yields: % 17.55/5.18 | (131) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v2, v3) = v4 & sziznziztdt0(xq) = v3 & sziznziztdt0(xq) = v2 & sdtlbdtrb0(xq, v1) = v6 & sdtlbdtrb0(xq, v0) = v5 & aDimensionOf0(xq) = v1 & aDimensionOf0(xq) = v0 & sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = v8 & ( ~ (v1 = v0) | v8 = xD | v0 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (91) with all_0_2_2, xq and discharging atoms aDimensionOf0(xq) = all_0_2_2, aVector0(xq), yields: % 17.55/5.18 | (132) aNaturalNumber0(all_0_2_2) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (103) with all_0_0_0, xD, xC, xq, xp and discharging atoms sdtasasdt0(xq, xq) = xD, sdtasasdt0(xp, xp) = xC, sdtasdt0(xC, xD) = all_0_0_0, aVector0(xq), aVector0(xp), yields: % 17.55/5.18 | (133) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasasdt0(xp, xq) = v2 & aDimensionOf0(xq) = v1 & aDimensionOf0(xp) = v0 & sdtasdt0(v2, v2) = v3 & ( ~ (v1 = v0) | ~ iLess0(v0, all_0_4_4) | sdtlseqdt0(v3, all_0_0_0))) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (123) with all_0_1_1, xE, xq, xp and discharging atoms sdtasasdt0(xp, xq) = xE, sdtasdt0(xE, xE) = all_0_1_1, aVector0(xq), aVector0(xp), yields: % 17.55/5.18 | (134) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasasdt0(xq, xq) = v3 & sdtasasdt0(xp, xp) = v2 & aDimensionOf0(xq) = v1 & aDimensionOf0(xp) = v0 & sdtasdt0(v2, v3) = v4 & ( ~ (v1 = v0) | ~ iLess0(v0, all_0_4_4) | sdtlseqdt0(all_0_1_1, v4))) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (13) with xE, xq, xp and discharging atoms sdtasasdt0(xp, xq) = xE, aVector0(xq), aVector0(xp), yields: % 17.55/5.18 | (135) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v2, v3) = v4 & sziznziztdt0(xq) = v3 & sziznziztdt0(xp) = v2 & sdtlbdtrb0(xq, v1) = v6 & sdtlbdtrb0(xp, v0) = v5 & aDimensionOf0(xq) = v1 & aDimensionOf0(xp) = v0 & sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = v8 & ( ~ (v1 = v0) | v8 = xE | v0 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (13) with xC, xp, xp and discharging atoms sdtasasdt0(xp, xp) = xC, aVector0(xp), yields: % 17.55/5.18 | (136) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v2, v3) = v4 & sziznziztdt0(xp) = v3 & sziznziztdt0(xp) = v2 & sdtlbdtrb0(xp, v1) = v6 & sdtlbdtrb0(xp, v0) = v5 & aDimensionOf0(xp) = v1 & aDimensionOf0(xp) = v0 & sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = v8 & ( ~ (v1 = v0) | v8 = xC | v0 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (91) with all_0_3_3, xp and discharging atoms aDimensionOf0(xp) = all_0_3_3, aVector0(xp), yields: % 17.55/5.18 | (137) aNaturalNumber0(all_0_3_3) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xq, all_0_2_2, xt, xq and discharging atoms sziznziztdt0(xt) = xq, aDimensionOf0(xq) = all_0_2_2, aVector0(xq), aVector0(xt), yields: % 17.55/5.18 | (138) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xq) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xq) = v3 & aDimensionOf0(xt) = v0 & ( ~ (v0 = all_0_2_2) | v3 = v2 | all_0_2_2 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xq, all_0_3_3, xt, xp and discharging atoms sziznziztdt0(xt) = xq, aDimensionOf0(xp) = all_0_3_3, aVector0(xp), aVector0(xt), yields: % 17.55/5.18 | (139) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xp) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xq) = v3 & aDimensionOf0(xt) = v0 & ( ~ (v0 = all_0_3_3) | v3 = v2 | all_0_3_3 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (83) with all_0_4_4, xt, xt and discharging atoms aDimensionOf0(xt) = all_0_4_4, aVector0(xt), yields: % 17.55/5.18 | (140) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xt, xt) = v0 & sziznziztdt0(xt) = v2 & sziznziztdt0(xt) = v1 & sdtlbdtrb0(xt, all_0_4_4) = v5 & sdtlbdtrb0(xt, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (84) with all_0_4_4, xt and discharging atoms aDimensionOf0(xt) = all_0_4_4, aVector0(xt), yields: % 17.55/5.18 | (141) all_0_4_4 = sz00 | ? [v0] : (sziznziztdt0(xt) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(v0, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xt, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xt, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(v0, v2) = v3) & ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xt, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = all_0_4_4) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_4_4) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (17) with xq, all_0_4_4, xs, xt and discharging atoms sziznziztdt0(xt) = xq, aDimensionOf0(xs) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (142) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xs) = v2 & aDimensionOf0(v2) = v3 & aDimensionOf0(xq) = v1 & aDimensionOf0(xt) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v1)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xq, all_0_4_4, xt, xs and discharging atoms sziznziztdt0(xt) = xq, aDimensionOf0(xs) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (143) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xs) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xq) = v3 & aDimensionOf0(xt) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v2 | all_0_4_4 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (2) with xq, xp, xt, xs and discharging atoms sziznziztdt0(xt) = xq, sziznziztdt0(xs) = xp, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (144) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (aDimensionOf0(xq) = v3 & aDimensionOf0(xp) = v2 & aDimensionOf0(xt) = v1 & aDimensionOf0(xs) = v0 & ( ~ (v1 = v0) | v3 = v2 | v0 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xp, all_0_2_2, xs, xq and discharging atoms sziznziztdt0(xs) = xp, aDimensionOf0(xq) = all_0_2_2, aVector0(xq), aVector0(xs), yields: % 17.55/5.18 | (145) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xq) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xp) = v3 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_2_2) | v3 = v2 | all_0_2_2 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xp, all_0_3_3, xs, xp and discharging atoms sziznziztdt0(xs) = xp, aDimensionOf0(xp) = all_0_3_3, aVector0(xp), aVector0(xs), yields: % 17.55/5.18 | (146) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xp) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xp) = v3 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_3_3) | v3 = v2 | all_0_3_3 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (17) with xp, all_0_4_4, xt, xs and discharging atoms sziznziztdt0(xs) = xp, aDimensionOf0(xt) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (147) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xt) = v2 & aDimensionOf0(v2) = v3 & aDimensionOf0(xp) = v1 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v1)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (119) with xp, all_0_4_4, xs, xt and discharging atoms sziznziztdt0(xs) = xp, aDimensionOf0(xt) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (148) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xt) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(xp) = v3 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v2 | all_0_4_4 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (2) with xp, xq, xs, xt and discharging atoms sziznziztdt0(xt) = xq, sziznziztdt0(xs) = xp, aVector0(xt), aVector0(xs), yields: % 17.55/5.18 | (149) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (aDimensionOf0(xq) = v2 & aDimensionOf0(xp) = v3 & aDimensionOf0(xt) = v0 & aDimensionOf0(xs) = v1 & ( ~ (v1 = v0) | v3 = v2 | v0 = sz00)) % 17.55/5.18 | % 17.55/5.18 | Instantiating formula (83) with all_0_4_4, xt, xs and discharging atoms aDimensionOf0(xt) = all_0_4_4, aDimensionOf0(xs) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.19 | (150) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xt) = v0 & sziznziztdt0(xt) = v2 & sziznziztdt0(xs) = v1 & sdtlbdtrb0(xt, all_0_4_4) = v5 & sdtlbdtrb0(xs, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.19 | % 17.55/5.19 | Instantiating formula (83) with all_0_4_4, xs, xs and discharging atoms aDimensionOf0(xs) = all_0_4_4, aVector0(xs), yields: % 17.55/5.19 | (151) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xs) = v0 & sziznziztdt0(xs) = v2 & sziznziztdt0(xs) = v1 & sdtlbdtrb0(xs, all_0_4_4) = v5 & sdtlbdtrb0(xs, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.19 | % 17.55/5.19 | Instantiating formula (83) with all_0_4_4, xs, xt and discharging atoms aDimensionOf0(xt) = all_0_4_4, aDimensionOf0(xs) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.19 | (152) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xt, xs) = v0 & sziznziztdt0(xt) = v1 & sziznziztdt0(xs) = v2 & sdtlbdtrb0(xt, all_0_4_4) = v4 & sdtlbdtrb0(xs, all_0_4_4) = v5 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.19 | % 17.55/5.19 | Instantiating formula (81) with all_0_4_4, xs, xt and discharging atoms aDimensionOf0(xt) = all_0_4_4, aDimensionOf0(xs) = all_0_4_4, aVector0(xt), aVector0(xs), yields: % 17.55/5.19 | (153) all_0_4_4 = sz00 | ? [v0] : ? [v1] : ? [v2] : (sziznziztdt0(xt) = v0 & sziznziztdt0(xs) = v2 & aDimensionOf0(v2) = v1 & aDimensionOf0(v0) = v1) % 17.55/5.19 | % 17.55/5.19 | Instantiating formula (84) with all_0_4_4, xs and discharging atoms aDimensionOf0(xs) = all_0_4_4, aVector0(xs), yields: % 17.55/5.19 | (154) all_0_4_4 = sz00 | ? [v0] : (sziznziztdt0(xs) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(v0, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xs, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xs, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(v0, v2) = v3) & ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xs, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = all_0_4_4) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_4_4) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 17.55/5.19 | % 17.55/5.19 | Instantiating (131) with all_17_0_8, all_17_1_9, all_17_2_10, all_17_3_11, all_17_4_12, all_17_5_13, all_17_6_14, all_17_7_15, all_17_8_16 yields: % 17.55/5.19 | (155) sdtasasdt0(all_17_6_14, all_17_5_13) = all_17_4_12 & sziznziztdt0(xq) = all_17_5_13 & sziznziztdt0(xq) = all_17_6_14 & sdtlbdtrb0(xq, all_17_7_15) = all_17_2_10 & sdtlbdtrb0(xq, all_17_8_16) = all_17_3_11 & aDimensionOf0(xq) = all_17_7_15 & aDimensionOf0(xq) = all_17_8_16 & sdtasdt0(all_17_3_11, all_17_2_10) = all_17_1_9 & sdtpldt0(all_17_4_12, all_17_1_9) = all_17_0_8 & ( ~ (all_17_7_15 = all_17_8_16) | all_17_0_8 = xD | all_17_8_16 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (155) yields: % 17.55/5.19 | (156) sdtasdt0(all_17_3_11, all_17_2_10) = all_17_1_9 % 17.55/5.19 | (157) sdtlbdtrb0(xq, all_17_8_16) = all_17_3_11 % 17.55/5.19 | (158) ~ (all_17_7_15 = all_17_8_16) | all_17_0_8 = xD | all_17_8_16 = sz00 % 17.55/5.19 | (159) aDimensionOf0(xq) = all_17_7_15 % 17.55/5.19 | (160) sdtpldt0(all_17_4_12, all_17_1_9) = all_17_0_8 % 17.55/5.19 | (161) sdtlbdtrb0(xq, all_17_7_15) = all_17_2_10 % 17.55/5.19 | (162) sdtasasdt0(all_17_6_14, all_17_5_13) = all_17_4_12 % 17.55/5.19 | (163) sziznziztdt0(xq) = all_17_5_13 % 17.55/5.19 | (164) aDimensionOf0(xq) = all_17_8_16 % 17.55/5.19 | (165) sziznziztdt0(xq) = all_17_6_14 % 17.55/5.19 | % 17.55/5.19 | Instantiating (138) with all_21_0_18, all_21_1_19, all_21_2_20, all_21_3_21 yields: % 17.55/5.19 | (166) sziznziztdt0(xq) = all_21_2_20 & aDimensionOf0(all_21_2_20) = all_21_1_19 & aDimensionOf0(xq) = all_21_0_18 & aDimensionOf0(xt) = all_21_3_21 & ( ~ (all_21_3_21 = all_0_2_2) | all_21_0_18 = all_21_1_19 | all_0_2_2 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (166) yields: % 17.55/5.19 | (167) aDimensionOf0(all_21_2_20) = all_21_1_19 % 17.55/5.19 | (168) aDimensionOf0(xt) = all_21_3_21 % 17.55/5.19 | (169) aDimensionOf0(xq) = all_21_0_18 % 17.55/5.19 | (170) sziznziztdt0(xq) = all_21_2_20 % 17.55/5.19 | (171) ~ (all_21_3_21 = all_0_2_2) | all_21_0_18 = all_21_1_19 | all_0_2_2 = sz00 % 17.55/5.19 | % 17.55/5.19 | Instantiating (149) with all_29_0_28, all_29_1_29, all_29_2_30, all_29_3_31 yields: % 17.55/5.19 | (172) aDimensionOf0(xq) = all_29_1_29 & aDimensionOf0(xp) = all_29_0_28 & aDimensionOf0(xt) = all_29_3_31 & aDimensionOf0(xs) = all_29_2_30 & ( ~ (all_29_2_30 = all_29_3_31) | all_29_0_28 = all_29_1_29 | all_29_3_31 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (172) yields: % 17.55/5.19 | (173) ~ (all_29_2_30 = all_29_3_31) | all_29_0_28 = all_29_1_29 | all_29_3_31 = sz00 % 17.55/5.19 | (174) aDimensionOf0(xt) = all_29_3_31 % 17.55/5.19 | (175) aDimensionOf0(xp) = all_29_0_28 % 17.55/5.19 | (176) aDimensionOf0(xs) = all_29_2_30 % 17.55/5.19 | (177) aDimensionOf0(xq) = all_29_1_29 % 17.55/5.19 | % 17.55/5.19 | Instantiating (133) with all_47_0_53, all_47_1_54, all_47_2_55, all_47_3_56 yields: % 17.55/5.19 | (178) sdtasasdt0(xp, xq) = all_47_1_54 & aDimensionOf0(xq) = all_47_2_55 & aDimensionOf0(xp) = all_47_3_56 & sdtasdt0(all_47_1_54, all_47_1_54) = all_47_0_53 & ( ~ (all_47_2_55 = all_47_3_56) | ~ iLess0(all_47_3_56, all_0_4_4) | sdtlseqdt0(all_47_0_53, all_0_0_0)) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (178) yields: % 17.55/5.19 | (179) ~ (all_47_2_55 = all_47_3_56) | ~ iLess0(all_47_3_56, all_0_4_4) | sdtlseqdt0(all_47_0_53, all_0_0_0) % 17.55/5.19 | (180) aDimensionOf0(xq) = all_47_2_55 % 17.55/5.19 | (181) sdtasdt0(all_47_1_54, all_47_1_54) = all_47_0_53 % 17.55/5.19 | (182) aDimensionOf0(xp) = all_47_3_56 % 17.55/5.19 | (183) sdtasasdt0(xp, xq) = all_47_1_54 % 17.55/5.19 | % 17.55/5.19 | Instantiating (145) with all_51_0_61, all_51_1_62, all_51_2_63, all_51_3_64 yields: % 17.55/5.19 | (184) sziznziztdt0(xq) = all_51_2_63 & aDimensionOf0(all_51_2_63) = all_51_1_62 & aDimensionOf0(xp) = all_51_0_61 & aDimensionOf0(xs) = all_51_3_64 & ( ~ (all_51_3_64 = all_0_2_2) | all_51_0_61 = all_51_1_62 | all_0_2_2 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (184) yields: % 17.55/5.19 | (185) sziznziztdt0(xq) = all_51_2_63 % 17.55/5.19 | (186) aDimensionOf0(xp) = all_51_0_61 % 17.55/5.19 | (187) aDimensionOf0(all_51_2_63) = all_51_1_62 % 17.55/5.19 | (188) aDimensionOf0(xs) = all_51_3_64 % 17.55/5.19 | (189) ~ (all_51_3_64 = all_0_2_2) | all_51_0_61 = all_51_1_62 | all_0_2_2 = sz00 % 17.55/5.19 | % 17.55/5.19 | Instantiating (144) with all_53_0_65, all_53_1_66, all_53_2_67, all_53_3_68 yields: % 17.55/5.19 | (190) aDimensionOf0(xq) = all_53_0_65 & aDimensionOf0(xp) = all_53_1_66 & aDimensionOf0(xt) = all_53_2_67 & aDimensionOf0(xs) = all_53_3_68 & ( ~ (all_53_2_67 = all_53_3_68) | all_53_0_65 = all_53_1_66 | all_53_3_68 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (190) yields: % 17.55/5.19 | (191) aDimensionOf0(xp) = all_53_1_66 % 17.55/5.19 | (192) aDimensionOf0(xt) = all_53_2_67 % 17.55/5.19 | (193) ~ (all_53_2_67 = all_53_3_68) | all_53_0_65 = all_53_1_66 | all_53_3_68 = sz00 % 17.55/5.19 | (194) aDimensionOf0(xs) = all_53_3_68 % 17.55/5.19 | (195) aDimensionOf0(xq) = all_53_0_65 % 17.55/5.19 | % 17.55/5.19 | Instantiating (143) with all_55_0_69, all_55_1_70, all_55_2_71, all_55_3_72 yields: % 17.55/5.19 | (196) sziznziztdt0(xs) = all_55_2_71 & aDimensionOf0(all_55_2_71) = all_55_1_70 & aDimensionOf0(xq) = all_55_0_69 & aDimensionOf0(xt) = all_55_3_72 & ( ~ (all_55_3_72 = all_0_4_4) | all_55_0_69 = all_55_1_70 | all_0_4_4 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (196) yields: % 17.55/5.19 | (197) aDimensionOf0(xq) = all_55_0_69 % 17.55/5.19 | (198) aDimensionOf0(all_55_2_71) = all_55_1_70 % 17.55/5.19 | (199) ~ (all_55_3_72 = all_0_4_4) | all_55_0_69 = all_55_1_70 | all_0_4_4 = sz00 % 17.55/5.19 | (200) aDimensionOf0(xt) = all_55_3_72 % 17.55/5.19 | (201) sziznziztdt0(xs) = all_55_2_71 % 17.55/5.19 | % 17.55/5.19 | Instantiating (148) with all_57_0_73, all_57_1_74, all_57_2_75, all_57_3_76 yields: % 17.55/5.19 | (202) sziznziztdt0(xt) = all_57_2_75 & aDimensionOf0(all_57_2_75) = all_57_1_74 & aDimensionOf0(xp) = all_57_0_73 & aDimensionOf0(xs) = all_57_3_76 & ( ~ (all_57_3_76 = all_0_4_4) | all_57_0_73 = all_57_1_74 | all_0_4_4 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (202) yields: % 17.55/5.19 | (203) aDimensionOf0(xs) = all_57_3_76 % 17.55/5.19 | (204) ~ (all_57_3_76 = all_0_4_4) | all_57_0_73 = all_57_1_74 | all_0_4_4 = sz00 % 17.55/5.19 | (205) aDimensionOf0(all_57_2_75) = all_57_1_74 % 17.55/5.19 | (206) sziznziztdt0(xt) = all_57_2_75 % 17.55/5.19 | (207) aDimensionOf0(xp) = all_57_0_73 % 17.55/5.19 | % 17.55/5.19 | Instantiating (146) with all_65_0_87, all_65_1_88, all_65_2_89, all_65_3_90 yields: % 17.55/5.19 | (208) sziznziztdt0(xp) = all_65_2_89 & aDimensionOf0(all_65_2_89) = all_65_1_88 & aDimensionOf0(xp) = all_65_0_87 & aDimensionOf0(xs) = all_65_3_90 & ( ~ (all_65_3_90 = all_0_3_3) | all_65_0_87 = all_65_1_88 | all_0_3_3 = sz00) % 17.55/5.19 | % 17.55/5.19 | Applying alpha-rule on (208) yields: % 17.55/5.19 | (209) aDimensionOf0(xs) = all_65_3_90 % 17.55/5.19 | (210) sziznziztdt0(xp) = all_65_2_89 % 17.55/5.19 | (211) aDimensionOf0(xp) = all_65_0_87 % 17.55/5.19 | (212) ~ (all_65_3_90 = all_0_3_3) | all_65_0_87 = all_65_1_88 | all_0_3_3 = sz00 % 17.55/5.19 | (213) aDimensionOf0(all_65_2_89) = all_65_1_88 % 17.55/5.19 | % 17.55/5.19 | Instantiating (136) with all_67_0_91, all_67_1_92, all_67_2_93, all_67_3_94, all_67_4_95, all_67_5_96, all_67_6_97, all_67_7_98, all_67_8_99 yields: % 17.55/5.19 | (214) sdtasasdt0(all_67_6_97, all_67_5_96) = all_67_4_95 & sziznziztdt0(xp) = all_67_5_96 & sziznziztdt0(xp) = all_67_6_97 & sdtlbdtrb0(xp, all_67_7_98) = all_67_2_93 & sdtlbdtrb0(xp, all_67_8_99) = all_67_3_94 & aDimensionOf0(xp) = all_67_7_98 & aDimensionOf0(xp) = all_67_8_99 & sdtasdt0(all_67_3_94, all_67_2_93) = all_67_1_92 & sdtpldt0(all_67_4_95, all_67_1_92) = all_67_0_91 & ( ~ (all_67_7_98 = all_67_8_99) | all_67_0_91 = xC | all_67_8_99 = sz00) % 17.55/5.20 | % 17.55/5.20 | Applying alpha-rule on (214) yields: % 17.55/5.20 | (215) sziznziztdt0(xp) = all_67_6_97 % 17.55/5.20 | (216) sziznziztdt0(xp) = all_67_5_96 % 17.55/5.20 | (217) ~ (all_67_7_98 = all_67_8_99) | all_67_0_91 = xC | all_67_8_99 = sz00 % 17.55/5.20 | (218) sdtlbdtrb0(xp, all_67_8_99) = all_67_3_94 % 17.55/5.20 | (219) sdtlbdtrb0(xp, all_67_7_98) = all_67_2_93 % 17.55/5.20 | (220) aDimensionOf0(xp) = all_67_7_98 % 17.55/5.20 | (221) aDimensionOf0(xp) = all_67_8_99 % 17.55/5.20 | (222) sdtasdt0(all_67_3_94, all_67_2_93) = all_67_1_92 % 17.55/5.20 | (223) sdtpldt0(all_67_4_95, all_67_1_92) = all_67_0_91 % 17.55/5.20 | (224) sdtasasdt0(all_67_6_97, all_67_5_96) = all_67_4_95 % 17.55/5.20 | % 17.55/5.20 | Instantiating (135) with all_69_0_100, all_69_1_101, all_69_2_102, all_69_3_103, all_69_4_104, all_69_5_105, all_69_6_106, all_69_7_107, all_69_8_108 yields: % 17.55/5.20 | (225) sdtasasdt0(all_69_6_106, all_69_5_105) = all_69_4_104 & sziznziztdt0(xq) = all_69_5_105 & sziznziztdt0(xp) = all_69_6_106 & sdtlbdtrb0(xq, all_69_7_107) = all_69_2_102 & sdtlbdtrb0(xp, all_69_8_108) = all_69_3_103 & aDimensionOf0(xq) = all_69_7_107 & aDimensionOf0(xp) = all_69_8_108 & sdtasdt0(all_69_3_103, all_69_2_102) = all_69_1_101 & sdtpldt0(all_69_4_104, all_69_1_101) = all_69_0_100 & ( ~ (all_69_7_107 = all_69_8_108) | all_69_0_100 = xE | all_69_8_108 = sz00) % 17.55/5.20 | % 17.55/5.20 | Applying alpha-rule on (225) yields: % 17.55/5.20 | (226) sdtasasdt0(all_69_6_106, all_69_5_105) = all_69_4_104 % 17.55/5.20 | (227) sziznziztdt0(xp) = all_69_6_106 % 17.55/5.20 | (228) sdtpldt0(all_69_4_104, all_69_1_101) = all_69_0_100 % 17.55/5.20 | (229) aDimensionOf0(xq) = all_69_7_107 % 17.55/5.20 | (230) sdtlbdtrb0(xp, all_69_8_108) = all_69_3_103 % 17.55/5.20 | (231) sziznziztdt0(xq) = all_69_5_105 % 17.55/5.20 | (232) sdtasdt0(all_69_3_103, all_69_2_102) = all_69_1_101 % 17.55/5.20 | (233) aDimensionOf0(xp) = all_69_8_108 % 17.55/5.20 | (234) sdtlbdtrb0(xq, all_69_7_107) = all_69_2_102 % 17.55/5.20 | (235) ~ (all_69_7_107 = all_69_8_108) | all_69_0_100 = xE | all_69_8_108 = sz00 % 17.55/5.20 | % 17.55/5.20 | Instantiating (134) with all_71_0_109, all_71_1_110, all_71_2_111, all_71_3_112, all_71_4_113 yields: % 17.55/5.20 | (236) sdtasasdt0(xq, xq) = all_71_1_110 & sdtasasdt0(xp, xp) = all_71_2_111 & aDimensionOf0(xq) = all_71_3_112 & aDimensionOf0(xp) = all_71_4_113 & sdtasdt0(all_71_2_111, all_71_1_110) = all_71_0_109 & ( ~ (all_71_3_112 = all_71_4_113) | ~ iLess0(all_71_4_113, all_0_4_4) | sdtlseqdt0(all_0_1_1, all_71_0_109)) % 17.55/5.20 | % 17.55/5.20 | Applying alpha-rule on (236) yields: % 17.55/5.20 | (237) ~ (all_71_3_112 = all_71_4_113) | ~ iLess0(all_71_4_113, all_0_4_4) | sdtlseqdt0(all_0_1_1, all_71_0_109) % 17.55/5.20 | (238) sdtasasdt0(xp, xp) = all_71_2_111 % 17.55/5.20 | (239) sdtasdt0(all_71_2_111, all_71_1_110) = all_71_0_109 % 17.55/5.20 | (240) aDimensionOf0(xp) = all_71_4_113 % 17.55/5.20 | (241) aDimensionOf0(xq) = all_71_3_112 % 17.55/5.20 | (242) sdtasasdt0(xq, xq) = all_71_1_110 % 17.55/5.20 | % 17.55/5.20 | Instantiating (139) with all_79_0_121, all_79_1_122, all_79_2_123, all_79_3_124 yields: % 17.55/5.20 | (243) sziznziztdt0(xp) = all_79_2_123 & aDimensionOf0(all_79_2_123) = all_79_1_122 & aDimensionOf0(xq) = all_79_0_121 & aDimensionOf0(xt) = all_79_3_124 & ( ~ (all_79_3_124 = all_0_3_3) | all_79_0_121 = all_79_1_122 | all_0_3_3 = sz00) % 17.55/5.20 | % 17.55/5.20 | Applying alpha-rule on (243) yields: % 17.55/5.20 | (244) sziznziztdt0(xp) = all_79_2_123 % 17.55/5.20 | (245) aDimensionOf0(xq) = all_79_0_121 % 17.55/5.20 | (246) ~ (all_79_3_124 = all_0_3_3) | all_79_0_121 = all_79_1_122 | all_0_3_3 = sz00 % 17.55/5.20 | (247) aDimensionOf0(all_79_2_123) = all_79_1_122 % 17.55/5.20 | (248) aDimensionOf0(xt) = all_79_3_124 % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (153), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (252) ? [v0] : ? [v1] : ? [v2] : (sziznziztdt0(xt) = v0 & sziznziztdt0(xs) = v2 & aDimensionOf0(v2) = v1 & aDimensionOf0(v0) = v1) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (141), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (256) ? [v0] : (sziznziztdt0(xt) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(v0, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xt, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xt, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(v0, v2) = v3) & ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xt, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = all_0_4_4) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_4_4) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (151), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (260) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xs) = v0 & sziznziztdt0(xs) = v2 & sziznziztdt0(xs) = v1 & sdtlbdtrb0(xs, all_0_4_4) = v5 & sdtlbdtrb0(xs, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (150), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (264) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xt) = v0 & sziznziztdt0(xt) = v2 & sziznziztdt0(xs) = v1 & sdtlbdtrb0(xt, all_0_4_4) = v5 & sdtlbdtrb0(xs, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (140), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (268) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xt, xt) = v0 & sziznziztdt0(xt) = v2 & sziznziztdt0(xt) = v1 & sdtlbdtrb0(xt, all_0_4_4) = v5 & sdtlbdtrb0(xt, all_0_4_4) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (154), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (272) ? [v0] : (sziznziztdt0(xs) = v0 & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(v0, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xs, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xs, v2) = v3) | ~ (aDimensionOf0(v0) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(v0, v2) = v3) & ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xs, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = all_0_4_4) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_4_4) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 17.55/5.20 | % 17.55/5.20 +-Applying beta-rule and splitting (152), into two cases. % 17.55/5.20 |-Branch one: % 17.55/5.20 | (249) all_0_4_4 = sz00 % 17.55/5.20 | % 17.55/5.20 | Equations (249) can reduce 94 to: % 17.55/5.20 | (250) $false % 17.55/5.20 | % 17.55/5.20 |-The branch is then unsatisfiable % 17.55/5.20 |-Branch two: % 17.55/5.20 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.20 | (276) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xt, xs) = v0 & sziznziztdt0(xt) = v1 & sziznziztdt0(xs) = v2 & sdtlbdtrb0(xt, all_0_4_4) = v4 & sdtlbdtrb0(xs, all_0_4_4) = v5 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 17.55/5.21 | % 17.55/5.21 +-Applying beta-rule and splitting (147), into two cases. % 17.55/5.21 |-Branch one: % 17.55/5.21 | (249) all_0_4_4 = sz00 % 17.55/5.21 | % 17.55/5.21 | Equations (249) can reduce 94 to: % 17.55/5.21 | (250) $false % 17.55/5.21 | % 17.55/5.21 |-The branch is then unsatisfiable % 17.55/5.21 |-Branch two: % 17.55/5.21 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.21 | (280) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xt) = v2 & aDimensionOf0(v2) = v3 & aDimensionOf0(xp) = v1 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v1)) % 17.55/5.21 | % 17.55/5.21 | Instantiating (280) with all_140_0_178, all_140_1_179, all_140_2_180, all_140_3_181 yields: % 17.55/5.21 | (281) sziznziztdt0(xt) = all_140_1_179 & aDimensionOf0(all_140_1_179) = all_140_0_178 & aDimensionOf0(xp) = all_140_2_180 & aDimensionOf0(xs) = all_140_3_181 & ( ~ (all_140_3_181 = all_0_4_4) | all_140_0_178 = all_140_2_180) % 17.55/5.21 | % 17.55/5.21 | Applying alpha-rule on (281) yields: % 17.55/5.21 | (282) sziznziztdt0(xt) = all_140_1_179 % 17.55/5.21 | (283) aDimensionOf0(all_140_1_179) = all_140_0_178 % 17.55/5.21 | (284) ~ (all_140_3_181 = all_0_4_4) | all_140_0_178 = all_140_2_180 % 17.55/5.21 | (285) aDimensionOf0(xs) = all_140_3_181 % 17.55/5.21 | (286) aDimensionOf0(xp) = all_140_2_180 % 17.55/5.21 | % 17.55/5.21 +-Applying beta-rule and splitting (142), into two cases. % 17.55/5.21 |-Branch one: % 17.55/5.21 | (249) all_0_4_4 = sz00 % 17.55/5.21 | % 17.55/5.21 | Equations (249) can reduce 94 to: % 17.55/5.21 | (250) $false % 17.55/5.21 | % 17.55/5.21 |-The branch is then unsatisfiable % 17.55/5.21 |-Branch two: % 17.55/5.21 | (94) ~ (all_0_4_4 = sz00) % 17.55/5.21 | (290) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xs) = v2 & aDimensionOf0(v2) = v3 & aDimensionOf0(xq) = v1 & aDimensionOf0(xt) = v0 & ( ~ (v0 = all_0_4_4) | v3 = v1)) % 17.55/5.21 | % 17.55/5.21 | Instantiating (290) with all_145_0_182, all_145_1_183, all_145_2_184, all_145_3_185 yields: % 17.55/5.21 | (291) sziznziztdt0(xs) = all_145_1_183 & aDimensionOf0(all_145_1_183) = all_145_0_182 & aDimensionOf0(xq) = all_145_2_184 & aDimensionOf0(xt) = all_145_3_185 & ( ~ (all_145_3_185 = all_0_4_4) | all_145_0_182 = all_145_2_184) % 17.55/5.21 | % 17.55/5.21 | Applying alpha-rule on (291) yields: % 17.55/5.21 | (292) aDimensionOf0(xq) = all_145_2_184 % 17.55/5.21 | (293) aDimensionOf0(xt) = all_145_3_185 % 17.55/5.21 | (294) sziznziztdt0(xs) = all_145_1_183 % 17.55/5.21 | (295) aDimensionOf0(all_145_1_183) = all_145_0_182 % 17.55/5.21 | (296) ~ (all_145_3_185 = all_0_4_4) | all_145_0_182 = all_145_2_184 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (110) with xq, xq, all_71_1_110, xD and discharging atoms sdtasasdt0(xq, xq) = all_71_1_110, sdtasasdt0(xq, xq) = xD, yields: % 17.55/5.21 | (297) all_71_1_110 = xD % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (110) with xp, xp, all_71_2_111, xC and discharging atoms sdtasasdt0(xp, xp) = all_71_2_111, sdtasasdt0(xp, xp) = xC, yields: % 17.55/5.21 | (298) all_71_2_111 = xC % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_145_2_184, all_0_2_2 and discharging atoms aDimensionOf0(xq) = all_145_2_184, aDimensionOf0(xq) = all_0_2_2, yields: % 17.55/5.21 | (299) all_145_2_184 = all_0_2_2 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_71_3_112, all_79_0_121 and discharging atoms aDimensionOf0(xq) = all_79_0_121, aDimensionOf0(xq) = all_71_3_112, yields: % 17.55/5.21 | (300) all_79_0_121 = all_71_3_112 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_69_7_107, all_79_0_121 and discharging atoms aDimensionOf0(xq) = all_79_0_121, aDimensionOf0(xq) = all_69_7_107, yields: % 17.55/5.21 | (301) all_79_0_121 = all_69_7_107 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_53_0_65, all_71_3_112 and discharging atoms aDimensionOf0(xq) = all_71_3_112, aDimensionOf0(xq) = all_53_0_65, yields: % 17.55/5.21 | (302) all_71_3_112 = all_53_0_65 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_47_2_55, all_145_2_184 and discharging atoms aDimensionOf0(xq) = all_145_2_184, aDimensionOf0(xq) = all_47_2_55, yields: % 17.55/5.21 | (303) all_145_2_184 = all_47_2_55 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_47_2_55, all_71_3_112 and discharging atoms aDimensionOf0(xq) = all_71_3_112, aDimensionOf0(xq) = all_47_2_55, yields: % 17.55/5.21 | (304) all_71_3_112 = all_47_2_55 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_47_2_55, all_55_0_69 and discharging atoms aDimensionOf0(xq) = all_55_0_69, aDimensionOf0(xq) = all_47_2_55, yields: % 17.55/5.21 | (305) all_55_0_69 = all_47_2_55 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_29_1_29, all_71_3_112 and discharging atoms aDimensionOf0(xq) = all_71_3_112, aDimensionOf0(xq) = all_29_1_29, yields: % 17.55/5.21 | (306) all_71_3_112 = all_29_1_29 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_21_0_18, all_47_2_55 and discharging atoms aDimensionOf0(xq) = all_47_2_55, aDimensionOf0(xq) = all_21_0_18, yields: % 17.55/5.21 | (307) all_47_2_55 = all_21_0_18 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_17_7_15, all_47_2_55 and discharging atoms aDimensionOf0(xq) = all_47_2_55, aDimensionOf0(xq) = all_17_7_15, yields: % 17.55/5.21 | (308) all_47_2_55 = all_17_7_15 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xq, all_17_8_16, all_55_0_69 and discharging atoms aDimensionOf0(xq) = all_55_0_69, aDimensionOf0(xq) = all_17_8_16, yields: % 17.55/5.21 | (309) all_55_0_69 = all_17_8_16 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_71_4_113, all_140_2_180 and discharging atoms aDimensionOf0(xp) = all_140_2_180, aDimensionOf0(xp) = all_71_4_113, yields: % 17.55/5.21 | (310) all_140_2_180 = all_71_4_113 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_69_8_108, all_140_2_180 and discharging atoms aDimensionOf0(xp) = all_140_2_180, aDimensionOf0(xp) = all_69_8_108, yields: % 17.55/5.21 | (311) all_140_2_180 = all_69_8_108 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_67_7_98, all_0_3_3 and discharging atoms aDimensionOf0(xp) = all_67_7_98, aDimensionOf0(xp) = all_0_3_3, yields: % 17.55/5.21 | (312) all_67_7_98 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_67_7_98, all_69_8_108 and discharging atoms aDimensionOf0(xp) = all_69_8_108, aDimensionOf0(xp) = all_67_7_98, yields: % 17.55/5.21 | (313) all_69_8_108 = all_67_7_98 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_67_8_99, all_140_2_180 and discharging atoms aDimensionOf0(xp) = all_140_2_180, aDimensionOf0(xp) = all_67_8_99, yields: % 17.55/5.21 | (314) all_140_2_180 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_65_0_87, all_67_7_98 and discharging atoms aDimensionOf0(xp) = all_67_7_98, aDimensionOf0(xp) = all_65_0_87, yields: % 17.55/5.21 | (315) all_67_7_98 = all_65_0_87 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_57_0_73, all_65_0_87 and discharging atoms aDimensionOf0(xp) = all_65_0_87, aDimensionOf0(xp) = all_57_0_73, yields: % 17.55/5.21 | (316) all_65_0_87 = all_57_0_73 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_53_1_66, all_65_0_87 and discharging atoms aDimensionOf0(xp) = all_65_0_87, aDimensionOf0(xp) = all_53_1_66, yields: % 17.55/5.21 | (317) all_65_0_87 = all_53_1_66 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_51_0_61, all_57_0_73 and discharging atoms aDimensionOf0(xp) = all_57_0_73, aDimensionOf0(xp) = all_51_0_61, yields: % 17.55/5.21 | (318) all_57_0_73 = all_51_0_61 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (89) with xp, all_47_3_56, all_57_0_73 and discharging atoms aDimensionOf0(xp) = all_57_0_73, aDimensionOf0(xp) = all_47_3_56, yields: % 17.55/5.21 | (319) all_57_0_73 = all_47_3_56 % 17.55/5.21 | % 17.55/5.21 | Instantiating formula (55) with all_0_4_4, all_0_2_2, all_0_3_3 and discharging atoms szszuzczcdt0(all_0_2_2) = all_0_4_4, szszuzczcdt0(all_0_3_3) = all_0_4_4, aNaturalNumber0(all_0_2_2), aNaturalNumber0(all_0_3_3), yields: % 17.55/5.21 | (320) all_0_2_2 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Combining equations (303,299) yields a new equation: % 17.55/5.21 | (321) all_47_2_55 = all_0_2_2 % 17.55/5.21 | % 17.55/5.21 | Simplifying 321 yields: % 17.55/5.21 | (322) all_47_2_55 = all_0_2_2 % 17.55/5.21 | % 17.55/5.21 | Combining equations (311,310) yields a new equation: % 17.55/5.21 | (323) all_71_4_113 = all_69_8_108 % 17.55/5.21 | % 17.55/5.21 | Combining equations (314,310) yields a new equation: % 17.55/5.21 | (324) all_71_4_113 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Combining equations (300,301) yields a new equation: % 17.55/5.21 | (325) all_71_3_112 = all_69_7_107 % 17.55/5.21 | % 17.55/5.21 | Simplifying 325 yields: % 17.55/5.21 | (326) all_71_3_112 = all_69_7_107 % 17.55/5.21 | % 17.55/5.21 | Combining equations (306,326) yields a new equation: % 17.55/5.21 | (327) all_69_7_107 = all_29_1_29 % 17.55/5.21 | % 17.55/5.21 | Combining equations (304,326) yields a new equation: % 17.55/5.21 | (328) all_69_7_107 = all_47_2_55 % 17.55/5.21 | % 17.55/5.21 | Combining equations (302,326) yields a new equation: % 17.55/5.21 | (329) all_69_7_107 = all_53_0_65 % 17.55/5.21 | % 17.55/5.21 | Combining equations (323,324) yields a new equation: % 17.55/5.21 | (330) all_69_8_108 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Simplifying 330 yields: % 17.55/5.21 | (331) all_69_8_108 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Combining equations (327,329) yields a new equation: % 17.55/5.21 | (332) all_53_0_65 = all_29_1_29 % 17.55/5.21 | % 17.55/5.21 | Combining equations (328,329) yields a new equation: % 17.55/5.21 | (333) all_53_0_65 = all_47_2_55 % 17.55/5.21 | % 17.55/5.21 | Combining equations (313,331) yields a new equation: % 17.55/5.21 | (334) all_67_7_98 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Simplifying 334 yields: % 17.55/5.21 | (335) all_67_7_98 = all_67_8_99 % 17.55/5.21 | % 17.55/5.21 | Combining equations (315,335) yields a new equation: % 17.55/5.21 | (336) all_67_8_99 = all_65_0_87 % 17.55/5.21 | % 17.55/5.21 | Combining equations (312,335) yields a new equation: % 17.55/5.21 | (337) all_67_8_99 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Combining equations (336,337) yields a new equation: % 17.55/5.21 | (338) all_65_0_87 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Simplifying 338 yields: % 17.55/5.21 | (339) all_65_0_87 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Combining equations (316,317) yields a new equation: % 17.55/5.21 | (340) all_57_0_73 = all_53_1_66 % 17.55/5.21 | % 17.55/5.21 | Simplifying 340 yields: % 17.55/5.21 | (341) all_57_0_73 = all_53_1_66 % 17.55/5.21 | % 17.55/5.21 | Combining equations (339,317) yields a new equation: % 17.55/5.21 | (342) all_53_1_66 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Combining equations (319,318) yields a new equation: % 17.55/5.21 | (343) all_51_0_61 = all_47_3_56 % 17.55/5.21 | % 17.55/5.21 | Combining equations (341,318) yields a new equation: % 17.55/5.21 | (344) all_53_1_66 = all_51_0_61 % 17.55/5.21 | % 17.55/5.21 | Simplifying 344 yields: % 17.55/5.21 | (345) all_53_1_66 = all_51_0_61 % 17.55/5.21 | % 17.55/5.21 | Combining equations (305,309) yields a new equation: % 17.55/5.21 | (346) all_47_2_55 = all_17_8_16 % 17.55/5.21 | % 17.55/5.21 | Simplifying 346 yields: % 17.55/5.21 | (347) all_47_2_55 = all_17_8_16 % 17.55/5.21 | % 17.55/5.21 | Combining equations (333,332) yields a new equation: % 17.55/5.21 | (348) all_47_2_55 = all_29_1_29 % 17.55/5.21 | % 17.55/5.21 | Simplifying 348 yields: % 17.55/5.21 | (349) all_47_2_55 = all_29_1_29 % 17.55/5.21 | % 17.55/5.21 | Combining equations (345,342) yields a new equation: % 17.55/5.21 | (350) all_51_0_61 = all_0_3_3 % 17.55/5.21 | % 17.55/5.21 | Simplifying 350 yields: % 17.55/5.21 | (351) all_51_0_61 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (351,343) yields a new equation: % 17.55/5.22 | (352) all_47_3_56 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (347,349) yields a new equation: % 17.55/5.22 | (353) all_29_1_29 = all_17_8_16 % 17.55/5.22 | % 17.55/5.22 | Combining equations (308,349) yields a new equation: % 17.55/5.22 | (354) all_29_1_29 = all_17_7_15 % 17.55/5.22 | % 17.55/5.22 | Combining equations (307,349) yields a new equation: % 17.55/5.22 | (355) all_29_1_29 = all_21_0_18 % 17.55/5.22 | % 17.55/5.22 | Combining equations (322,349) yields a new equation: % 17.55/5.22 | (356) all_29_1_29 = all_0_2_2 % 17.55/5.22 | % 17.55/5.22 | Combining equations (353,355) yields a new equation: % 17.55/5.22 | (357) all_21_0_18 = all_17_8_16 % 17.55/5.22 | % 17.55/5.22 | Combining equations (356,355) yields a new equation: % 17.55/5.22 | (358) all_21_0_18 = all_0_2_2 % 17.55/5.22 | % 17.55/5.22 | Combining equations (354,355) yields a new equation: % 17.55/5.22 | (359) all_21_0_18 = all_17_7_15 % 17.55/5.22 | % 17.55/5.22 | Combining equations (357,359) yields a new equation: % 17.55/5.22 | (360) all_17_7_15 = all_17_8_16 % 17.55/5.22 | % 17.55/5.22 | Combining equations (358,359) yields a new equation: % 17.55/5.22 | (361) all_17_7_15 = all_0_2_2 % 17.55/5.22 | % 17.55/5.22 | Combining equations (361,360) yields a new equation: % 17.55/5.22 | (362) all_17_8_16 = all_0_2_2 % 17.55/5.22 | % 17.55/5.22 | Combining equations (320,362) yields a new equation: % 17.55/5.22 | (363) all_17_8_16 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (363,360) yields a new equation: % 17.55/5.22 | (364) all_17_7_15 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (364,359) yields a new equation: % 17.55/5.22 | (365) all_21_0_18 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (365,355) yields a new equation: % 17.55/5.22 | (366) all_29_1_29 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (366,332) yields a new equation: % 17.55/5.22 | (367) all_53_0_65 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (367,329) yields a new equation: % 17.55/5.22 | (368) all_69_7_107 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (337,324) yields a new equation: % 17.55/5.22 | (369) all_71_4_113 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | Combining equations (368,326) yields a new equation: % 17.55/5.22 | (370) all_71_3_112 = all_0_3_3 % 17.55/5.22 | % 17.55/5.22 | From (298)(297) and (239) follows: % 17.55/5.22 | (371) sdtasdt0(xC, xD) = all_71_0_109 % 17.55/5.22 | % 17.55/5.22 | From (320) and (41) follows: % 17.55/5.22 | (78) szszuzczcdt0(all_0_3_3) = all_0_4_4 % 17.55/5.22 | % 17.55/5.22 | From (320) and (132) follows: % 17.55/5.22 | (137) aNaturalNumber0(all_0_3_3) % 17.55/5.22 | % 17.55/5.22 | Instantiating formula (47) with xC, xD, all_71_0_109, all_0_0_0 and discharging atoms sdtasdt0(xC, xD) = all_71_0_109, sdtasdt0(xC, xD) = all_0_0_0, yields: % 17.55/5.22 | (374) all_71_0_109 = all_0_0_0 % 17.55/5.22 | % 17.55/5.22 +-Applying beta-rule and splitting (179), into two cases. % 17.55/5.22 |-Branch one: % 17.55/5.22 | (375) ~ iLess0(all_47_3_56, all_0_4_4) % 17.55/5.22 | % 17.55/5.22 | From (352) and (375) follows: % 17.55/5.22 | (376) ~ iLess0(all_0_3_3, all_0_4_4) % 17.55/5.22 | % 17.55/5.22 | Instantiating formula (74) with all_0_4_4, all_0_3_3 and discharging atoms szszuzczcdt0(all_0_3_3) = all_0_4_4, aNaturalNumber0(all_0_3_3), ~ iLess0(all_0_3_3, all_0_4_4), yields: % 17.55/5.22 | (377) $false % 17.55/5.22 | % 17.55/5.22 |-The branch is then unsatisfiable % 17.55/5.22 |-Branch two: % 17.55/5.22 | (378) iLess0(all_47_3_56, all_0_4_4) % 17.55/5.22 | (379) ~ (all_47_2_55 = all_47_3_56) | sdtlseqdt0(all_47_0_53, all_0_0_0) % 17.55/5.22 | % 17.55/5.22 | From (352) and (378) follows: % 17.55/5.22 | (380) iLess0(all_0_3_3, all_0_4_4) % 17.55/5.22 | % 17.55/5.22 +-Applying beta-rule and splitting (237), into two cases. % 17.55/5.22 |-Branch one: % 17.55/5.22 | (381) ~ iLess0(all_71_4_113, all_0_4_4) % 17.55/5.22 | % 17.55/5.22 | From (369) and (381) follows: % 17.55/5.22 | (376) ~ iLess0(all_0_3_3, all_0_4_4) % 17.55/5.22 | % 17.55/5.22 | Using (380) and (376) yields: % 17.55/5.22 | (377) $false % 17.55/5.22 | % 17.55/5.22 |-The branch is then unsatisfiable % 17.55/5.22 |-Branch two: % 17.55/5.22 | (384) iLess0(all_71_4_113, all_0_4_4) % 17.55/5.22 | (385) ~ (all_71_3_112 = all_71_4_113) | sdtlseqdt0(all_0_1_1, all_71_0_109) % 17.55/5.22 | % 17.55/5.22 +-Applying beta-rule and splitting (385), into two cases. % 17.55/5.22 |-Branch one: % 17.55/5.22 | (386) sdtlseqdt0(all_0_1_1, all_71_0_109) % 17.55/5.22 | % 17.55/5.22 | From (374) and (386) follows: % 17.55/5.22 | (387) sdtlseqdt0(all_0_1_1, all_0_0_0) % 17.55/5.22 | % 17.55/5.22 | Using (387) and (16) yields: % 17.55/5.22 | (377) $false % 17.55/5.22 | % 17.55/5.22 |-The branch is then unsatisfiable % 17.55/5.22 |-Branch two: % 17.55/5.22 | (389) ~ sdtlseqdt0(all_0_1_1, all_71_0_109) % 17.55/5.22 | (390) ~ (all_71_3_112 = all_71_4_113) % 17.55/5.22 | % 17.55/5.22 | Equations (370,369) can reduce 390 to: % 17.55/5.22 | (250) $false % 17.55/5.22 | % 17.55/5.22 |-The branch is then unsatisfiable % 17.55/5.22 % SZS output end Proof for theBenchmark % 17.55/5.22 % 17.55/5.22 4637ms %------------------------------------------------------------------------------