%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : RNG049+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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 5.72s 1.94s % Output : Proof 9.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG049+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon May 30 10:10:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.52/0.59 ____ _ % 0.52/0.59 ___ / __ \_____(_)___ ________ __________ % 0.52/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.52/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.52/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.52/0.59 % 0.52/0.59 A Theorem Prover for First-Order Logic % 0.52/0.59 (ePrincess v.1.0) % 0.52/0.59 % 0.52/0.59 (c) Philipp Rümmer, 2009-2015 % 0.52/0.59 (c) Peter Backeman, 2014-2015 % 0.52/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.52/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.52/0.59 Bug reports to peter@backeman.se % 0.52/0.59 % 0.52/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.52/0.59 % 0.52/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.88/1.00 Prover 0: Preprocessing ... % 3.78/1.52 Prover 0: Constructing countermodel ... % 5.72/1.94 Prover 0: proved (1293ms) % 5.72/1.94 % 5.72/1.94 No countermodel exists, formula is valid % 5.72/1.94 % SZS status Theorem for theBenchmark % 5.72/1.94 % 5.72/1.94 Generating proof ... found it (size 156) % 9.03/2.69 % 9.03/2.69 % SZS output start Proof for theBenchmark % 9.03/2.69 Assumed formulas after preprocessing and simplification: % 9.03/2.69 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v1 = sz00) & sdtasasdt0(xs, xs) = v6 & sziznziztdt0(xs) = v2 & sdtlbdtrb0(xs, v1) = v4 & aDimensionOf0(v2) = v3 & aDimensionOf0(xs) = v1 & smndt0(sz0z00) = v0 & sdtasdt0(v4, v4) = v5 & szszuzczcdt0(v3) = v1 & aVector0(v2) & aVector0(xs) & sdtlseqdt0(sz0z00, v5) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(sz0z00, v6) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v8, v10) = v15) | ~ (sdtasdt0(v8, v9) = v14) | ~ (sdtasdt0(v7, v10) = v12) | ~ (sdtasdt0(v7, v9) = v11) | ~ (sdtpldt0(v14, v15) = v16) | ~ (sdtpldt0(v13, v16) = v17) | ~ (sdtpldt0(v11, v12) = v13) | ~ aScalar0(v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v18] : ? [v19] : (sdtasdt0(v18, v19) = v17 & sdtpldt0(v9, v10) = v19 & sdtpldt0(v7, v8) = v18)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v9 = sz00 | ~ (sdtasasdt0(v10, v11) = v12) | ~ (sziznziztdt0(v8) = v11) | ~ (sziznziztdt0(v7) = v10) | ~ (sdtlbdtrb0(v8, v9) = v14) | ~ (sdtlbdtrb0(v7, v9) = v13) | ~ (aDimensionOf0(v8) = v9) | ~ (aDimensionOf0(v7) = v9) | ~ (sdtasdt0(v13, v14) = v15) | ~ (sdtpldt0(v12, v15) = v16) | ~ aVector0(v8) | ~ aVector0(v7) | sdtasasdt0(v7, v8) = v16) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v11, v12) = v13) | ~ (sdtpldt0(v9, v10) = v12) | ~ (sdtpldt0(v7, v8) = v11) | ~ aScalar0(v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : (sdtasdt0(v8, v10) = v18 & sdtasdt0(v8, v9) = v17 & sdtasdt0(v7, v10) = v15 & sdtasdt0(v7, v9) = v14 & sdtpldt0(v17, v18) = v19 & sdtpldt0(v16, v19) = v13 & sdtpldt0(v14, v15) = v16)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtasdt0(v8, v10) = v12) | ~ (sdtasdt0(v7, v9) = v11) | ~ sdtlseqdt0(v9, v10) | ~ sdtlseqdt0(v7, v8) | ~ sdtlseqdt0(sz0z00, v9) | ~ aScalar0(v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(v11, v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtasdt0(v8, v9) = v11) | ~ (sdtasdt0(v7, v9) = v10) | ~ (sdtpldt0(v10, v11) = v12) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : (sdtasdt0(v16, v9) = v12 & sdtasdt0(v7, v13) = v14 & sdtasdt0(v7, v8) = v15 & sdtpldt0(v15, v10) = v14 & sdtpldt0(v8, v9) = v13 & sdtpldt0(v7, v8) = v16)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtasdt0(v7, v9) = v11) | ~ (sdtasdt0(v7, v8) = v10) | ~ (sdtpldt0(v10, v11) = v12) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : (sdtasdt0(v14, v9) = v15 & sdtasdt0(v8, v9) = v16 & sdtasdt0(v7, v13) = v12 & sdtpldt0(v11, v16) = v15 & sdtpldt0(v8, v9) = v13 & sdtpldt0(v7, v8) = v14)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtpldt0(v8, v10) = v12) | ~ (sdtpldt0(v7, v9) = v11) | ~ sdtlseqdt0(v9, v10) | ~ sdtlseqdt0(v7, v8) | ~ aScalar0(v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(v11, v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (smndt0(v8) = v10) | ~ (smndt0(v7) = v9) | ~ (sdtasdt0(v9, v10) = v11) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtasdt0(v7, v8) = v11) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v10, v9) = v11) | ~ (sdtasdt0(v7, v8) = v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v8, v9) = v15 & sdtasdt0(v8, v7) = v10 & sdtasdt0(v7, v15) = v11 & sdtpldt0(v12, v9) = v13 & sdtpldt0(v8, v9) = v14 & sdtpldt0(v8, v7) = v12 & sdtpldt0(v7, v14) = v13 & sdtpldt0(v7, v8) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v10, v9) = v11) | ~ (sdtpldt0(v7, v8) = v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (sdtasdt0(v8, v9) = v16 & sdtasdt0(v7, v12) = v13 & sdtasdt0(v7, v9) = v15 & sdtasdt0(v7, v8) = v14 & sdtpldt0(v15, v16) = v11 & sdtpldt0(v14, v15) = v13 & sdtpldt0(v8, v9) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v8, v9) = v10) | ~ (sdtasdt0(v7, v10) = v11) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v15, v9) = v11 & sdtasdt0(v8, v7) = v15 & sdtasdt0(v7, v8) = v15 & sdtpldt0(v12, v9) = v13 & sdtpldt0(v8, v9) = v14 & sdtpldt0(v8, v7) = v12 & sdtpldt0(v7, v14) = v13 & sdtpldt0(v7, v8) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v7, v10) = v11) | ~ (sdtpldt0(v8, v9) = v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (sdtasdt0(v14, v9) = v15 & sdtasdt0(v8, v9) = v16 & sdtasdt0(v7, v9) = v13 & sdtasdt0(v7, v8) = v12 & sdtpldt0(v13, v16) = v15 & sdtpldt0(v12, v13) = v11 & sdtpldt0(v7, v8) = v14)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v10, v9) = v11) | ~ (sdtpldt0(v7, v8) = v10) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v13, v9) = v14 & sdtasdt0(v8, v9) = v15 & sdtasdt0(v8, v7) = v13 & sdtasdt0(v7, v15) = v14 & sdtasdt0(v7, v8) = v13 & sdtpldt0(v8, v9) = v12 & sdtpldt0(v8, v7) = v10 & sdtpldt0(v7, v12) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v8, v9) = v10) | ~ (sdtpldt0(v7, v10) = v11) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v13, v9) = v14 & sdtasdt0(v8, v9) = v15 & sdtasdt0(v8, v7) = v13 & sdtasdt0(v7, v15) = v14 & sdtasdt0(v7, v8) = v13 & sdtpldt0(v12, v9) = v11 & sdtpldt0(v8, v7) = v12 & sdtpldt0(v7, v8) = v12)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v9 = sz00 | ~ (sziznziztdt0(v7) = v10) | ~ (aDimensionOf0(v8) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sziznziztdt0(v8) = v13 & aDimensionOf0(v13) = v14 & aDimensionOf0(v10) = v12 & aDimensionOf0(v7) = v11 & ( ~ (v11 = v9) | v14 = v12))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (sdtasasdt0(v10, v9) = v8) | ~ (sdtasasdt0(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (sdtlbdtrb0(v10, v9) = v8) | ~ (sdtlbdtrb0(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (sdtasdt0(v10, v9) = v8) | ~ (sdtasdt0(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (sdtpldt0(v10, v9) = v8) | ~ (sdtpldt0(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sziznziztdt0(v8) = v10) | ~ (sziznziztdt0(v7) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (aDimensionOf0(v10) = v14 & aDimensionOf0(v9) = v13 & aDimensionOf0(v8) = v12 & aDimensionOf0(v7) = v11 & ( ~ (v12 = v11) | v14 = v13 | v11 = sz00))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sziznziztdt0(v8) = v10) | ~ (aDimensionOf0(v7) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sziznziztdt0(v7) = v12 & aDimensionOf0(v12) = v13 & aDimensionOf0(v10) = v14 & aDimensionOf0(v8) = v11 & ( ~ (v11 = v9) | v14 = v13 | v9 = sz00))) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (smndt0(v8) = v9) | ~ (sdtasdt0(v7, v9) = v10) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v11] : ? [v12] : (smndt0(v11) = v10 & smndt0(v7) = v12 & sdtasdt0(v12, v8) = v10 & sdtasdt0(v7, v8) = v11)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (smndt0(v7) = v9) | ~ (sdtasdt0(v9, v8) = v10) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v11] : ? [v12] : (smndt0(v12) = v10 & smndt0(v8) = v11 & sdtasdt0(v7, v11) = v10 & sdtasdt0(v7, v8) = v12)) & ! [v7] : ! [v8] : ! [v9] : (v9 = sz0z00 | ~ (sdtasasdt0(v7, v8) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v10] : ? [v11] : (aDimensionOf0(v8) = v11 & aDimensionOf0(v7) = v10 & ( ~ (v11 = sz00) | ~ (v10 = sz00)))) & ! [v7] : ! [v8] : ! [v9] : (v9 = sz0z00 | ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v8, v7) = v9) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ! [v9] : (v9 = sz0z00 | ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v7, v8) = v9) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ! [v9] : (v9 = sz00 | ~ (aDimensionOf0(v8) = v9) | ~ (aDimensionOf0(v7) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (sdtasasdt0(v11, v12) = v13 & sdtasasdt0(v7, v8) = v10 & sziznziztdt0(v8) = v12 & sziznziztdt0(v7) = v11 & sdtlbdtrb0(v8, v9) = v15 & sdtlbdtrb0(v7, v9) = v14 & sdtasdt0(v14, v15) = v16 & sdtpldt0(v13, v16) = v10)) & ! [v7] : ! [v8] : ! [v9] : (v9 = sz00 | ~ (aDimensionOf0(v8) = v9) | ~ (aDimensionOf0(v7) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v10] : ? [v11] : ? [v12] : (sziznziztdt0(v8) = v12 & sziznziztdt0(v7) = v10 & aDimensionOf0(v12) = v11 & aDimensionOf0(v10) = v11)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (sziznziztdt0(v9) = v8) | ~ (sziznziztdt0(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (aDimensionOf0(v9) = v8) | ~ (aDimensionOf0(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (smndt0(v9) = v8) | ~ (smndt0(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (sdtasdt0(v8, v8) = v9) | ~ (sdtasdt0(v7, v7) = v9) | ~ sdtlseqdt0(sz0z00, v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ aScalar0(v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (szszuzczcdt0(v9) = v8) | ~ (szszuzczcdt0(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (szszuzczcdt0(v8) = v9) | ~ (szszuzczcdt0(v7) = v9) | ~ aNaturalNumber0(v8) | ~ aNaturalNumber0(v7)) & ! [v7] : ! [v8] : ! [v9] : (v0 = sz0z00 | ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v8, v7) = v9) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ! [v9] : (v0 = sz0z00 | ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v7, v8) = v9) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasasdt0(v7, v8) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | aScalar0(v9) | ? [v10] : ? [v11] : ( ~ (v11 = v10) & aDimensionOf0(v8) = v11 & aDimensionOf0(v7) = v10)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasasdt0(v7, v8) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasasdt0(v12, v13) = v14 & sziznziztdt0(v8) = v13 & sziznziztdt0(v7) = v12 & sdtlbdtrb0(v8, v11) = v16 & sdtlbdtrb0(v7, v10) = v15 & aDimensionOf0(v8) = v11 & aDimensionOf0(v7) = v10 & sdtasdt0(v15, v16) = v17 & sdtpldt0(v14, v17) = v18 & ( ~ (v11 = v10) | v18 = v9 | v10 = sz00))) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtlbdtrb0(v7, v8) = v9) | ~ aVector0(v7) | ~ aNaturalNumber0(v8) | aScalar0(v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (aDimensionOf0(v8) = v9) | ~ (aDimensionOf0(v7) = v9) | ~ aVector0(v8) | ~ aVector0(v7) | ? [v10] : (sdtasasdt0(v7, v8) = v10 & aScalar0(v10))) & ! [v7] : ! [v8] : ! [v9] : ( ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v8, v7) = v9) | ~ aScalar0(v7) | (smndt0(v8) = v7 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v7, v8) = sz0z00 & sdtpldt0(v7, sz0z00) = v7 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (smndt0(v7) = v8) | ~ (sdtpldt0(v7, v8) = v9) | ~ aScalar0(v7) | (smndt0(v8) = v7 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v8, v7) = sz0z00 & sdtpldt0(v7, sz0z00) = v7 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ sdtlseqdt0(sz0z00, v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(sz0z00, v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ sdtlseqdt0(sz0z00, v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v10] : (sdtpldt0(v7, v8) = v10 & sdtlseqdt0(sz0z00, v10))) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | aScalar0(v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v10] : ? [v11] : ? [v12] : (smndt0(v9) = v11 & smndt0(v8) = v10 & smndt0(v7) = v12 & sdtasdt0(v12, v8) = v11 & sdtasdt0(v7, v10) = v11)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v7, v8) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v10] : ? [v11] : (smndt0(v8) = v11 & smndt0(v7) = v10 & sdtasdt0(v10, v11) = v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtpldt0(v7, v8) = v9) | ~ sdtlseqdt0(sz0z00, v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(sz0z00, v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtpldt0(v7, v8) = v9) | ~ sdtlseqdt0(sz0z00, v8) | ~ sdtlseqdt0(sz0z00, v7) | ~ aScalar0(v8) | ~ aScalar0(v7) | ? [v10] : (sdtasdt0(v7, v8) = v10 & sdtlseqdt0(sz0z00, v10))) & ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtpldt0(v7, v8) = v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | aScalar0(v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ sdtlseqdt0(v8, v9) | ~ sdtlseqdt0(v7, v8) | ~ aScalar0(v9) | ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(v7, v9)) & ! [v7] : ! [v8] : (v8 = v7 | ~ (sdtpldt0(v7, sz0z00) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v8 = v7 | ~ (sdtpldt0(sz0z00, v7) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v8 = v7 | ~ sdtlseqdt0(v8, v7) | ~ sdtlseqdt0(v7, v8) | ~ aScalar0(v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v8 = sz0z00 | ~ (sdtasdt0(v7, sz0z00) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v8 = sz0z00 | ~ (sdtasdt0(sz0z00, v7) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v8 = sz00 | ~ (aDimensionOf0(v7) = v8) | ~ aVector0(v7) | ? [v9] : (sziznziztdt0(v7) = v9 & ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtlbdtrb0(v9, v11) = v12) | ~ (aDimensionOf0(v9) = v10) | ~ aNaturalNumber0(v11) | sdtlbdtrb0(v7, v11) = v12) & ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtlbdtrb0(v7, v11) = v12) | ~ (aDimensionOf0(v9) = v10) | ~ aNaturalNumber0(v11) | sdtlbdtrb0(v9, v11) = v12) & ! [v10] : ! [v11] : (v10 = v9 | ~ (aDimensionOf0(v10) = v11) | ~ aVector0(v10) | ? [v12] : ? [v13] : ? [v14] : (( ~ (v14 = v13) & sdtlbdtrb0(v10, v12) = v13 & sdtlbdtrb0(v7, v12) = v14 & aNaturalNumber0(v12)) | ( ~ (v12 = v8) & szszuzczcdt0(v11) = v12))) & ! [v10] : ( ~ (aDimensionOf0(v9) = v10) | szszuzczcdt0(v10) = v8) & ! [v10] : ( ~ (aDimensionOf0(v9) = v10) | aVector0(v9)))) & ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (smndt0(v7) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (sdtasdt0(v7, sz0z00) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (sdtasdt0(sz0z00, v7) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (sdtpldt0(v7, sz0z00) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : (v0 = sz0z00 | ~ (sdtpldt0(sz0z00, v7) = v8) | ~ aScalar0(v7)) & ! [v7] : ! [v8] : ( ~ (sdtasasdt0(v7, v7) = v8) | ~ aVector0(v7) | sdtlseqdt0(sz0z00, v8) | ? [v9] : (aDimensionOf0(v7) = v9 & ~ iLess0(v9, v1))) & ! [v7] : ! [v8] : ( ~ (sziznziztdt0(v7) = v8) | ~ aVector0(v7) | ? [v9] : (aDimensionOf0(v7) = v9 & (v9 = sz00 | ( ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtlbdtrb0(v8, v11) = v12) | ~ (aDimensionOf0(v8) = v10) | ~ aNaturalNumber0(v11) | sdtlbdtrb0(v7, v11) = v12) & ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtlbdtrb0(v7, v11) = v12) | ~ (aDimensionOf0(v8) = v10) | ~ aNaturalNumber0(v11) | sdtlbdtrb0(v8, v11) = v12) & ! [v10] : ! [v11] : (v10 = v8 | ~ (aDimensionOf0(v10) = v11) | ~ aVector0(v10) | ? [v12] : ? [v13] : ? [v14] : (( ~ (v14 = v13) & sdtlbdtrb0(v10, v12) = v13 & sdtlbdtrb0(v7, v12) = v14 & aNaturalNumber0(v12)) | ( ~ (v12 = v9) & szszuzczcdt0(v11) = v12))) & ! [v10] : ( ~ (aDimensionOf0(v8) = v10) | szszuzczcdt0(v10) = v9) & ! [v10] : ( ~ (aDimensionOf0(v8) = v10) | aVector0(v8)))))) & ! [v7] : ! [v8] : ( ~ (sdtlbdtrb0(v2, v7) = v8) | ~ aNaturalNumber0(v7) | sdtlbdtrb0(xs, v7) = v8) & ! [v7] : ! [v8] : ( ~ (sdtlbdtrb0(xs, v7) = v8) | ~ aNaturalNumber0(v7) | sdtlbdtrb0(v2, v7) = v8) & ! [v7] : ! [v8] : ( ~ (aDimensionOf0(v8) = sz00) | ~ (aDimensionOf0(v7) = sz00) | ~ aVector0(v8) | ~ aVector0(v7) | sdtasasdt0(v7, v8) = sz0z00) & ! [v7] : ! [v8] : ( ~ (aDimensionOf0(v7) = v8) | ~ aVector0(v7) | ~ iLess0(v8, v1) | ? [v9] : (sdtasasdt0(v7, v7) = v9 & sdtlseqdt0(sz0z00, v9))) & ! [v7] : ! [v8] : ( ~ (aDimensionOf0(v7) = v8) | ~ aVector0(v7) | aNaturalNumber0(v8)) & ! [v7] : ! [v8] : ( ~ (smndt0(v7) = v8) | ~ aScalar0(v7) | aScalar0(v8)) & ! [v7] : ! [v8] : ( ~ (smndt0(v7) = v8) | ~ aScalar0(v7) | (smndt0(v8) = v7 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v8, v7) = sz0z00 & sdtpldt0(v7, v8) = sz0z00 & sdtpldt0(v7, sz0z00) = v7 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ( ~ (sdtasdt0(v7, v7) = v8) | ~ aScalar0(v7) | sdtlseqdt0(sz0z00, v8)) & ! [v7] : ! [v8] : ( ~ (sdtasdt0(v7, sz0z00) = v8) | ~ aScalar0(v7) | ? [v9] : (smndt0(v9) = v7 & smndt0(v7) = v9 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v9, v7) = sz0z00 & sdtpldt0(v7, v9) = sz0z00 & sdtpldt0(v7, sz0z00) = v7 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ( ~ (sdtasdt0(sz0z00, v7) = v8) | ~ aScalar0(v7) | ? [v9] : (smndt0(v9) = v7 & smndt0(v7) = v9 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtpldt0(v9, v7) = sz0z00 & sdtpldt0(v7, v9) = sz0z00 & sdtpldt0(v7, sz0z00) = v7 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ( ~ (sdtpldt0(v7, sz0z00) = v8) | ~ aScalar0(v7) | ? [v9] : (smndt0(v9) = v7 & smndt0(v7) = v9 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v9, v7) = sz0z00 & sdtpldt0(v7, v9) = sz0z00 & sdtpldt0(sz0z00, v7) = v7)) & ! [v7] : ! [v8] : ( ~ (sdtpldt0(sz0z00, v7) = v8) | ~ aScalar0(v7) | ? [v9] : (smndt0(v9) = v7 & smndt0(v7) = v9 & sdtasdt0(v7, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v7) = sz0z00 & sdtpldt0(v9, v7) = sz0z00 & sdtpldt0(v7, v9) = sz0z00 & sdtpldt0(v7, sz0z00) = v7)) & ! [v7] : ! [v8] : ( ~ (szszuzczcdt0(v7) = v8) | ~ aNaturalNumber0(v7) | iLess0(v7, v8)) & ! [v7] : ! [v8] : ( ~ (szszuzczcdt0(v7) = v8) | ~ aNaturalNumber0(v7) | aNaturalNumber0(v8)) & ! [v7] : ! [v8] : ( ~ aScalar0(v8) | ~ aScalar0(v7) | sdtlseqdt0(v8, v7) | sdtlseqdt0(v7, v8)) & ! [v7] : (v7 = sz00 | ~ aNaturalNumber0(v7) | ? [v8] : (szszuzczcdt0(v8) = v7 & aNaturalNumber0(v8))) & ! [v7] : ( ~ (szszuzczcdt0(v7) = sz00) | ~ aNaturalNumber0(v7)) & ! [v7] : ( ~ aScalar0(v7) | sdtlseqdt0(v7, v7))) % 9.46/2.76 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 yields: % 9.46/2.76 | (1) ~ (all_0_5_5 = sz00) & sdtasasdt0(xs, xs) = all_0_0_0 & sziznziztdt0(xs) = all_0_4_4 & sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2 & aDimensionOf0(all_0_4_4) = all_0_3_3 & aDimensionOf0(xs) = all_0_5_5 & smndt0(sz0z00) = all_0_6_6 & sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 & szszuzczcdt0(all_0_3_3) = all_0_5_5 & aVector0(all_0_4_4) & aVector0(xs) & sdtlseqdt0(sz0z00, all_0_1_1) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(sz0z00, 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] : ( ~ (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] : ( ~ (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_6_6 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ! [v2] : (all_0_6_6 = 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) | ? [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_6_6 = sz0z00 | ~ (smndt0(v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1) | ? [v2] : (aDimensionOf0(v0) = v2 & ~ iLess0(v2, all_0_5_5))) & ! [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(all_0_4_4, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xs, v0) = v1) & ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xs, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(all_0_4_4, 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) | ~ iLess0(v1, all_0_5_5) | ? [v2] : (sdtasasdt0(v0, v0) = v2 & sdtlseqdt0(sz0z00, v2))) & ! [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)) % 9.46/2.78 | % 9.46/2.78 | Applying alpha-rule on (1) yields: % 9.46/2.78 | (2) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v1)) % 9.46/2.78 | (3) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 9.46/2.78 | (4) ! [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)) % 9.46/2.79 | (5) aDimensionOf0(xs) = all_0_5_5 % 9.46/2.79 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 9.46/2.79 | (7) ! [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))) % 9.46/2.79 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 9.46/2.79 | (9) sdtasasdt0(xs, xs) = all_0_0_0 % 9.46/2.79 | (10) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | aScalar0(v2)) % 9.46/2.79 | (11) ! [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)))) % 9.46/2.79 | (12) ! [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)) % 9.46/2.79 | (13) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) % 9.46/2.79 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : (sdtasasdt0(v0, v1) = v3 & aScalar0(v3))) % 9.46/2.79 | (15) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 9.46/2.79 | (16) ! [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)) % 9.46/2.79 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) % 9.46/2.79 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) % 9.46/2.79 | (19) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sdtasdt0(v1, v1) = v2) | ~ (sdtasdt0(v0, v0) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 9.46/2.79 | (20) ~ sdtlseqdt0(sz0z00, all_0_0_0) % 9.46/2.79 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 9.46/2.79 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 9.46/2.79 | (23) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v1) = sz00) | ~ (aDimensionOf0(v0) = sz00) | ~ aVector0(v1) | ~ aVector0(v0) | sdtasasdt0(v0, v1) = sz0z00) % 9.46/2.79 | (24) smndt0(sz0z00) = all_0_6_6 % 9.46/2.79 | (25) ! [v0] : ! [v1] : ! [v2] : (all_0_6_6 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 9.46/2.79 | (26) sdtlseqdt0(sz0z00, all_0_1_1) % 9.46/2.79 | (27) ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 9.46/2.79 | (28) ! [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)) % 9.46/2.79 | (29) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 % 9.46/2.79 | (30) ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 9.46/2.79 | (31) ! [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)) % 9.46/2.79 | (32) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v1)) % 9.46/2.79 | (33) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3] : ? [v4] : (smndt0(v1) = v4 & smndt0(v0) = v3 & sdtasdt0(v3, v4) = v2)) % 9.46/2.79 | (34) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 9.46/2.79 | (35) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 9.46/2.79 | (36) ! [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)) % 9.46/2.79 | (37) ! [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)))))) % 9.46/2.79 | (38) ! [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))) % 9.46/2.79 | (39) ! [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)) % 9.46/2.79 | (40) aNaturalNumber0(sz00) % 9.46/2.79 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) % 9.46/2.79 | (42) ! [v0] : ( ~ aScalar0(v0) | sdtlseqdt0(v0, v0)) % 9.46/2.79 | (43) ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtpldt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 9.46/2.79 | (44) ! [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)) % 9.46/2.79 | (45) szszuzczcdt0(all_0_3_3) = all_0_5_5 % 9.46/2.79 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 9.46/2.79 | (47) aScalar0(sz0z00) % 9.46/2.79 | (48) sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2 % 9.46/2.79 | (49) ! [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)) % 9.46/2.80 | (50) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | aScalar0(v1)) % 9.46/2.80 | (51) ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aNaturalNumber0(v0)) % 9.46/2.80 | (52) ! [v0] : ! [v1] : ( ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) % 9.46/2.80 | (53) ! [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))) % 9.46/2.80 | (54) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | aNaturalNumber0(v1)) % 9.46/2.80 | (55) ! [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)) % 9.46/2.80 | (56) ! [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)) % 9.46/2.80 | (57) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 9.46/2.80 | (58) ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1) | ? [v2] : (aDimensionOf0(v0) = v2 & ~ iLess0(v2, all_0_5_5))) % 9.46/2.80 | (59) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(xs, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(all_0_4_4, v0) = v1) % 9.46/2.80 | (60) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ~ iLess0(v1, all_0_5_5) | ? [v2] : (sdtasasdt0(v0, v0) = v2 & sdtlseqdt0(sz0z00, v2))) % 9.46/2.80 | (61) ! [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)) % 9.46/2.80 | (62) ! [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))) % 9.46/2.80 | (63) ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 9.46/2.80 | (64) ! [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)) % 9.46/2.80 | (65) ! [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) % 9.46/2.80 | (66) ! [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)) % 9.46/2.80 | (67) ! [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))) % 9.46/2.80 | (68) ! [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)) % 9.46/2.80 | (69) ! [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)) % 9.46/2.80 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtasdt0(v0, v1) = v4) % 9.46/2.80 | (71) ~ (all_0_5_5 = sz00) % 9.46/2.80 | (72) ! [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)) % 9.46/2.80 | (73) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v0, v2)) % 9.46/2.80 | (74) ! [v0] : ! [v1] : (v1 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 9.46/2.80 | (75) ! [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)) % 9.46/2.80 | (76) ! [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)) % 9.46/2.80 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 9.46/2.80 | (78) ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (sdtasdt0(sz0z00, v0) = v1) | ~ aScalar0(v0)) % 9.46/2.80 | (79) ! [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))) % 9.46/2.80 | (80) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz0z00) = v1) | ~ aScalar0(v0)) % 9.46/2.80 | (81) aDimensionOf0(all_0_4_4) = all_0_3_3 % 9.46/2.80 | (82) ! [v0] : (v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1))) % 9.46/2.80 | (83) aVector0(all_0_4_4) % 9.46/2.80 | (84) ! [v0] : ! [v1] : ! [v2] : (all_0_6_6 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v0)) % 9.46/2.80 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 9.46/2.80 | (86) ! [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)) % 9.46/2.80 | (87) ! [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)) % 9.46/2.80 | (88) ! [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)) % 9.46/2.80 | (89) ! [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)) % 9.46/2.80 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 9.46/2.80 | (91) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | aScalar0(v2) | ? [v3] : ? [v4] : ( ~ (v4 = v3) & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3)) % 9.46/2.80 | (92) ! [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)) % 9.46/2.80 | (93) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) % 9.46/2.80 | (94) ! [v0] : ! [v1] : (all_0_6_6 = sz0z00 | ~ (smndt0(v0) = v1) | ~ aScalar0(v0)) % 9.46/2.80 | (95) ! [v0] : ! [v1] : ( ~ (sdtlbdtrb0(all_0_4_4, v0) = v1) | ~ aNaturalNumber0(v0) | sdtlbdtrb0(xs, v0) = v1) % 9.46/2.80 | (96) ! [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)))) % 9.46/2.81 | (97) aVector0(xs) % 9.46/2.81 | (98) sziznziztdt0(xs) = all_0_4_4 % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (14) with all_0_3_3, all_0_4_4, all_0_4_4 and discharging atoms aDimensionOf0(all_0_4_4) = all_0_3_3, aVector0(all_0_4_4), yields: % 9.46/2.81 | (99) ? [v0] : (sdtasasdt0(all_0_4_4, all_0_4_4) = v0 & aScalar0(v0)) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (54) with all_0_3_3, all_0_4_4 and discharging atoms aDimensionOf0(all_0_4_4) = all_0_3_3, aVector0(all_0_4_4), yields: % 9.46/2.81 | (100) aNaturalNumber0(all_0_3_3) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (7) with all_0_0_0, xs, xs and discharging atoms sdtasasdt0(xs, xs) = all_0_0_0, aVector0(xs), yields: % 9.46/2.81 | (101) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v2, v3) = v4 & sziznziztdt0(xs) = v3 & sziznziztdt0(xs) = v2 & sdtlbdtrb0(xs, v1) = v6 & sdtlbdtrb0(xs, v0) = v5 & aDimensionOf0(xs) = v1 & aDimensionOf0(xs) = v0 & sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = v8 & ( ~ (v1 = v0) | v8 = all_0_0_0 | v0 = sz00)) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (58) with all_0_0_0, xs and discharging atoms sdtasasdt0(xs, xs) = all_0_0_0, aVector0(xs), ~ sdtlseqdt0(sz0z00, all_0_0_0), yields: % 9.46/2.81 | (102) ? [v0] : (aDimensionOf0(xs) = v0 & ~ iLess0(v0, all_0_5_5)) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (67) with all_0_4_4, all_0_3_3, xs, all_0_4_4 and discharging atoms sziznziztdt0(xs) = all_0_4_4, aDimensionOf0(all_0_4_4) = all_0_3_3, aVector0(all_0_4_4), aVector0(xs), yields: % 9.46/2.81 | (103) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(all_0_4_4) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(all_0_4_4) = v3 & aDimensionOf0(xs) = v0 & ( ~ (v0 = all_0_3_3) | v3 = v2 | all_0_3_3 = sz00)) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (37) with all_0_4_4, xs and discharging atoms sziznziztdt0(xs) = all_0_4_4, aVector0(xs), yields: % 9.46/2.81 | (104) ? [v0] : (aDimensionOf0(xs) = v0 & (v0 = sz00 | ( ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(all_0_4_4, v2) = v3) | ~ (aDimensionOf0(all_0_4_4) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xs, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xs, v2) = v3) | ~ (aDimensionOf0(all_0_4_4) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(all_0_4_4, v2) = v3) & ! [v1] : ! [v2] : (v1 = all_0_4_4 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xs, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = v0) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(all_0_4_4) = v1) | szszuzczcdt0(v1) = v0) & ! [v1] : ( ~ (aDimensionOf0(all_0_4_4) = v1) | aVector0(all_0_4_4))))) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (49) with all_0_5_5, xs, xs and discharging atoms aDimensionOf0(xs) = all_0_5_5, aVector0(xs), yields: % 9.46/2.81 | (105) all_0_5_5 = 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_5_5) = v5 & sdtlbdtrb0(xs, all_0_5_5) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (11) with all_0_5_5, xs and discharging atoms aDimensionOf0(xs) = all_0_5_5, aVector0(xs), yields: % 9.46/2.81 | (106) all_0_5_5 = 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_5_5) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_5_5) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 9.46/2.81 | % 9.46/2.81 | Instantiating formula (54) with all_0_5_5, xs and discharging atoms aDimensionOf0(xs) = all_0_5_5, aVector0(xs), yields: % 9.46/2.81 | (107) aNaturalNumber0(all_0_5_5) % 9.46/2.81 | % 9.46/2.81 | Instantiating (104) with all_13_0_7 yields: % 9.46/2.81 | (108) aDimensionOf0(xs) = all_13_0_7 & (all_13_0_7 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_0_4_4, v1) = v2) | ~ (aDimensionOf0(all_0_4_4) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xs, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(all_0_4_4) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_0_4_4, v1) = v2) & ! [v0] : ! [v1] : (v0 = all_0_4_4 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_13_0_7) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(all_0_4_4) = v0) | szszuzczcdt0(v0) = all_13_0_7) & ! [v0] : ( ~ (aDimensionOf0(all_0_4_4) = v0) | aVector0(all_0_4_4)))) % 9.46/2.81 | % 9.46/2.81 | Applying alpha-rule on (108) yields: % 9.46/2.81 | (109) aDimensionOf0(xs) = all_13_0_7 % 9.46/2.81 | (110) all_13_0_7 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_0_4_4, v1) = v2) | ~ (aDimensionOf0(all_0_4_4) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xs, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(all_0_4_4) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_0_4_4, v1) = v2) & ! [v0] : ! [v1] : (v0 = all_0_4_4 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_13_0_7) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(all_0_4_4) = v0) | szszuzczcdt0(v0) = all_13_0_7) & ! [v0] : ( ~ (aDimensionOf0(all_0_4_4) = v0) | aVector0(all_0_4_4))) % 9.46/2.81 | % 9.46/2.81 | Instantiating (103) with all_17_0_9, all_17_1_10, all_17_2_11, all_17_3_12 yields: % 9.46/2.81 | (111) sziznziztdt0(all_0_4_4) = all_17_2_11 & aDimensionOf0(all_17_2_11) = all_17_1_10 & aDimensionOf0(all_0_4_4) = all_17_0_9 & aDimensionOf0(xs) = all_17_3_12 & ( ~ (all_17_3_12 = all_0_3_3) | all_17_0_9 = all_17_1_10 | all_0_3_3 = sz00) % 9.46/2.81 | % 9.46/2.81 | Applying alpha-rule on (111) yields: % 9.46/2.81 | (112) aDimensionOf0(xs) = all_17_3_12 % 9.46/2.81 | (113) aDimensionOf0(all_0_4_4) = all_17_0_9 % 9.46/2.81 | (114) aDimensionOf0(all_17_2_11) = all_17_1_10 % 9.46/2.81 | (115) ~ (all_17_3_12 = all_0_3_3) | all_17_0_9 = all_17_1_10 | all_0_3_3 = sz00 % 9.46/2.81 | (116) sziznziztdt0(all_0_4_4) = all_17_2_11 % 9.46/2.81 | % 9.46/2.81 | Instantiating (99) with all_19_0_13 yields: % 9.46/2.81 | (117) sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13 & aScalar0(all_19_0_13) % 9.46/2.81 | % 9.46/2.81 | Applying alpha-rule on (117) yields: % 9.46/2.81 | (118) sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13 % 9.46/2.81 | (119) aScalar0(all_19_0_13) % 9.46/2.81 | % 9.46/2.81 | Instantiating (102) with all_21_0_14 yields: % 9.46/2.81 | (120) aDimensionOf0(xs) = all_21_0_14 & ~ iLess0(all_21_0_14, all_0_5_5) % 9.46/2.81 | % 9.46/2.81 | Applying alpha-rule on (120) yields: % 9.46/2.81 | (121) aDimensionOf0(xs) = all_21_0_14 % 9.46/2.81 | (122) ~ iLess0(all_21_0_14, all_0_5_5) % 9.46/2.81 | % 9.46/2.81 | Instantiating (101) with all_23_0_15, all_23_1_16, all_23_2_17, all_23_3_18, all_23_4_19, all_23_5_20, all_23_6_21, all_23_7_22, all_23_8_23 yields: % 9.46/2.81 | (123) sdtasasdt0(all_23_6_21, all_23_5_20) = all_23_4_19 & sziznziztdt0(xs) = all_23_5_20 & sziznziztdt0(xs) = all_23_6_21 & sdtlbdtrb0(xs, all_23_7_22) = all_23_2_17 & sdtlbdtrb0(xs, all_23_8_23) = all_23_3_18 & aDimensionOf0(xs) = all_23_7_22 & aDimensionOf0(xs) = all_23_8_23 & sdtasdt0(all_23_3_18, all_23_2_17) = all_23_1_16 & sdtpldt0(all_23_4_19, all_23_1_16) = all_23_0_15 & ( ~ (all_23_7_22 = all_23_8_23) | all_23_0_15 = all_0_0_0 | all_23_8_23 = sz00) % 9.46/2.81 | % 9.46/2.81 | Applying alpha-rule on (123) yields: % 9.46/2.81 | (124) sdtasdt0(all_23_3_18, all_23_2_17) = all_23_1_16 % 9.46/2.81 | (125) sdtlbdtrb0(xs, all_23_8_23) = all_23_3_18 % 9.46/2.81 | (126) aDimensionOf0(xs) = all_23_8_23 % 9.46/2.81 | (127) sdtlbdtrb0(xs, all_23_7_22) = all_23_2_17 % 9.46/2.81 | (128) sdtpldt0(all_23_4_19, all_23_1_16) = all_23_0_15 % 9.46/2.81 | (129) sziznziztdt0(xs) = all_23_6_21 % 9.46/2.81 | (130) aDimensionOf0(xs) = all_23_7_22 % 9.46/2.81 | (131) ~ (all_23_7_22 = all_23_8_23) | all_23_0_15 = all_0_0_0 | all_23_8_23 = sz00 % 9.46/2.81 | (132) sziznziztdt0(xs) = all_23_5_20 % 9.46/2.81 | (133) sdtasasdt0(all_23_6_21, all_23_5_20) = all_23_4_19 % 9.46/2.81 | % 9.46/2.81 +-Applying beta-rule and splitting (106), into two cases. % 9.46/2.81 |-Branch one: % 9.46/2.81 | (134) all_0_5_5 = sz00 % 9.46/2.81 | % 9.46/2.81 | Equations (134) can reduce 71 to: % 9.46/2.81 | (135) $false % 9.46/2.81 | % 9.46/2.81 |-The branch is then unsatisfiable % 9.46/2.81 |-Branch two: % 9.46/2.81 | (71) ~ (all_0_5_5 = sz00) % 9.46/2.81 | (137) ? [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_5_5) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | szszuzczcdt0(v1) = all_0_5_5) & ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | aVector0(v0))) % 9.46/2.82 | % 9.46/2.82 | Instantiating (137) with all_33_0_24 yields: % 9.46/2.82 | (138) sziznziztdt0(xs) = all_33_0_24 & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_33_0_24, v1) = v2) | ~ (aDimensionOf0(all_33_0_24) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xs, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(all_33_0_24) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_33_0_24, v1) = v2) & ! [v0] : ! [v1] : (v0 = all_33_0_24 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_0_5_5) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(all_33_0_24) = v0) | szszuzczcdt0(v0) = all_0_5_5) & ! [v0] : ( ~ (aDimensionOf0(all_33_0_24) = v0) | aVector0(all_33_0_24)) % 9.46/2.82 | % 9.46/2.82 | Applying alpha-rule on (138) yields: % 9.46/2.82 | (139) ! [v0] : ! [v1] : (v0 = all_33_0_24 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_0_5_5) & szszuzczcdt0(v1) = v2))) % 9.46/2.82 | (140) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_33_0_24, v1) = v2) | ~ (aDimensionOf0(all_33_0_24) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xs, v1) = v2) % 9.46/2.82 | (141) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(all_33_0_24) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_33_0_24, v1) = v2) % 9.46/2.82 | (142) ! [v0] : ( ~ (aDimensionOf0(all_33_0_24) = v0) | szszuzczcdt0(v0) = all_0_5_5) % 9.46/2.82 | (143) sziznziztdt0(xs) = all_33_0_24 % 9.46/2.82 | (144) ! [v0] : ( ~ (aDimensionOf0(all_33_0_24) = v0) | aVector0(all_33_0_24)) % 9.46/2.82 | % 9.46/2.82 +-Applying beta-rule and splitting (105), into two cases. % 9.46/2.82 |-Branch one: % 9.46/2.82 | (134) all_0_5_5 = sz00 % 9.46/2.82 | % 9.46/2.82 | Equations (134) can reduce 71 to: % 9.46/2.82 | (135) $false % 9.46/2.82 | % 9.46/2.82 |-The branch is then unsatisfiable % 9.46/2.82 |-Branch two: % 9.46/2.82 | (71) ~ (all_0_5_5 = sz00) % 9.46/2.82 | (148) ? [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_5_5) = v5 & sdtlbdtrb0(xs, all_0_5_5) = v4 & sdtasdt0(v4, v5) = v6 & sdtpldt0(v3, v6) = v0) % 9.46/2.82 | % 9.46/2.82 | Instantiating (148) with all_39_0_25, all_39_1_26, all_39_2_27, all_39_3_28, all_39_4_29, all_39_5_30, all_39_6_31 yields: % 9.46/2.82 | (149) sdtasasdt0(all_39_5_30, all_39_4_29) = all_39_3_28 & sdtasasdt0(xs, xs) = all_39_6_31 & sziznziztdt0(xs) = all_39_4_29 & sziznziztdt0(xs) = all_39_5_30 & sdtlbdtrb0(xs, all_0_5_5) = all_39_1_26 & sdtlbdtrb0(xs, all_0_5_5) = all_39_2_27 & sdtasdt0(all_39_2_27, all_39_1_26) = all_39_0_25 & sdtpldt0(all_39_3_28, all_39_0_25) = all_39_6_31 % 9.46/2.82 | % 9.46/2.82 | Applying alpha-rule on (149) yields: % 9.46/2.82 | (150) sdtlbdtrb0(xs, all_0_5_5) = all_39_2_27 % 9.46/2.82 | (151) sziznziztdt0(xs) = all_39_4_29 % 9.46/2.82 | (152) sdtasasdt0(all_39_5_30, all_39_4_29) = all_39_3_28 % 9.46/2.82 | (153) sdtasdt0(all_39_2_27, all_39_1_26) = all_39_0_25 % 9.46/2.82 | (154) sziznziztdt0(xs) = all_39_5_30 % 9.46/2.82 | (155) sdtlbdtrb0(xs, all_0_5_5) = all_39_1_26 % 9.46/2.82 | (156) sdtasasdt0(xs, xs) = all_39_6_31 % 9.46/2.82 | (157) sdtpldt0(all_39_3_28, all_39_0_25) = all_39_6_31 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (41) with xs, all_39_4_29, all_0_4_4 and discharging atoms sziznziztdt0(xs) = all_39_4_29, sziznziztdt0(xs) = all_0_4_4, yields: % 9.46/2.82 | (158) all_39_4_29 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (41) with xs, all_33_0_24, all_39_4_29 and discharging atoms sziznziztdt0(xs) = all_39_4_29, sziznziztdt0(xs) = all_33_0_24, yields: % 9.46/2.82 | (159) all_39_4_29 = all_33_0_24 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (41) with xs, all_23_5_20, all_39_5_30 and discharging atoms sziznziztdt0(xs) = all_39_5_30, sziznziztdt0(xs) = all_23_5_20, yields: % 9.46/2.82 | (160) all_39_5_30 = all_23_5_20 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (41) with xs, all_23_5_20, all_33_0_24 and discharging atoms sziznziztdt0(xs) = all_33_0_24, sziznziztdt0(xs) = all_23_5_20, yields: % 9.46/2.82 | (161) all_33_0_24 = all_23_5_20 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (41) with xs, all_23_6_21, all_39_5_30 and discharging atoms sziznziztdt0(xs) = all_39_5_30, sziznziztdt0(xs) = all_23_6_21, yields: % 9.46/2.82 | (162) all_39_5_30 = all_23_6_21 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (77) with xs, all_0_5_5, all_39_1_26, all_0_2_2 and discharging atoms sdtlbdtrb0(xs, all_0_5_5) = all_39_1_26, sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2, yields: % 9.46/2.82 | (163) all_39_1_26 = all_0_2_2 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (77) with xs, all_0_5_5, all_39_2_27, all_39_1_26 and discharging atoms sdtlbdtrb0(xs, all_0_5_5) = all_39_1_26, sdtlbdtrb0(xs, all_0_5_5) = all_39_2_27, yields: % 9.46/2.82 | (164) all_39_1_26 = all_39_2_27 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with all_0_4_4, all_17_0_9, all_0_3_3 and discharging atoms aDimensionOf0(all_0_4_4) = all_17_0_9, aDimensionOf0(all_0_4_4) = all_0_3_3, yields: % 9.46/2.82 | (165) all_17_0_9 = all_0_3_3 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with xs, all_23_8_23, all_0_5_5 and discharging atoms aDimensionOf0(xs) = all_23_8_23, aDimensionOf0(xs) = all_0_5_5, yields: % 9.46/2.82 | (166) all_23_8_23 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with xs, all_21_0_14, all_23_7_22 and discharging atoms aDimensionOf0(xs) = all_23_7_22, aDimensionOf0(xs) = all_21_0_14, yields: % 9.46/2.82 | (167) all_23_7_22 = all_21_0_14 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with xs, all_21_0_14, all_23_8_23 and discharging atoms aDimensionOf0(xs) = all_23_8_23, aDimensionOf0(xs) = all_21_0_14, yields: % 9.46/2.82 | (168) all_23_8_23 = all_21_0_14 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with xs, all_17_3_12, all_23_8_23 and discharging atoms aDimensionOf0(xs) = all_23_8_23, aDimensionOf0(xs) = all_17_3_12, yields: % 9.46/2.82 | (169) all_23_8_23 = all_17_3_12 % 9.46/2.82 | % 9.46/2.82 | Instantiating formula (85) with xs, all_13_0_7, all_23_7_22 and discharging atoms aDimensionOf0(xs) = all_23_7_22, aDimensionOf0(xs) = all_13_0_7, yields: % 9.46/2.82 | (170) all_23_7_22 = all_13_0_7 % 9.46/2.82 | % 9.46/2.82 | Combining equations (164,163) yields a new equation: % 9.46/2.82 | (171) all_39_2_27 = all_0_2_2 % 9.46/2.82 | % 9.46/2.82 | Simplifying 171 yields: % 9.46/2.82 | (172) all_39_2_27 = all_0_2_2 % 9.46/2.82 | % 9.46/2.82 | Combining equations (159,158) yields a new equation: % 9.46/2.82 | (173) all_33_0_24 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Simplifying 173 yields: % 9.46/2.82 | (174) all_33_0_24 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Combining equations (160,162) yields a new equation: % 9.46/2.82 | (175) all_23_5_20 = all_23_6_21 % 9.46/2.82 | % 9.46/2.82 | Simplifying 175 yields: % 9.46/2.82 | (176) all_23_5_20 = all_23_6_21 % 9.46/2.82 | % 9.46/2.82 | Combining equations (161,174) yields a new equation: % 9.46/2.82 | (177) all_23_5_20 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Simplifying 177 yields: % 9.46/2.82 | (178) all_23_5_20 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Combining equations (176,178) yields a new equation: % 9.46/2.82 | (179) all_23_6_21 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Simplifying 179 yields: % 9.46/2.82 | (180) all_23_6_21 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | Combining equations (167,170) yields a new equation: % 9.46/2.82 | (181) all_21_0_14 = all_13_0_7 % 9.46/2.82 | % 9.46/2.82 | Simplifying 181 yields: % 9.46/2.82 | (182) all_21_0_14 = all_13_0_7 % 9.46/2.82 | % 9.46/2.82 | Combining equations (168,169) yields a new equation: % 9.46/2.82 | (183) all_21_0_14 = all_17_3_12 % 9.46/2.82 | % 9.46/2.82 | Simplifying 183 yields: % 9.46/2.82 | (184) all_21_0_14 = all_17_3_12 % 9.46/2.82 | % 9.46/2.82 | Combining equations (166,169) yields a new equation: % 9.46/2.82 | (185) all_17_3_12 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Combining equations (184,182) yields a new equation: % 9.46/2.82 | (186) all_17_3_12 = all_13_0_7 % 9.46/2.82 | % 9.46/2.82 | Simplifying 186 yields: % 9.46/2.82 | (187) all_17_3_12 = all_13_0_7 % 9.46/2.82 | % 9.46/2.82 | Combining equations (185,187) yields a new equation: % 9.46/2.82 | (188) all_13_0_7 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Combining equations (188,187) yields a new equation: % 9.46/2.82 | (185) all_17_3_12 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Combining equations (185,169) yields a new equation: % 9.46/2.82 | (166) all_23_8_23 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Combining equations (188,170) yields a new equation: % 9.46/2.82 | (191) all_23_7_22 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | Combining equations (180,162) yields a new equation: % 9.46/2.82 | (192) all_39_5_30 = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | From (192)(158) and (152) follows: % 9.46/2.82 | (193) sdtasasdt0(all_0_4_4, all_0_4_4) = all_39_3_28 % 9.46/2.82 | % 9.46/2.82 | From (180)(178) and (133) follows: % 9.46/2.82 | (194) sdtasasdt0(all_0_4_4, all_0_4_4) = all_23_4_19 % 9.46/2.82 | % 9.46/2.82 | From (180) and (129) follows: % 9.46/2.82 | (98) sziznziztdt0(xs) = all_0_4_4 % 9.46/2.82 | % 9.46/2.82 | From (191) and (127) follows: % 9.46/2.82 | (196) sdtlbdtrb0(xs, all_0_5_5) = all_23_2_17 % 9.46/2.82 | % 9.46/2.82 | From (166) and (125) follows: % 9.46/2.82 | (197) sdtlbdtrb0(xs, all_0_5_5) = all_23_3_18 % 9.46/2.82 | % 9.46/2.82 | From (172) and (150) follows: % 9.46/2.82 | (48) sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2 % 9.46/2.82 | % 9.46/2.82 | From (165) and (113) follows: % 9.46/2.82 | (81) aDimensionOf0(all_0_4_4) = all_0_3_3 % 9.46/2.82 | % 9.46/2.82 | From (188) and (109) follows: % 9.46/2.82 | (5) aDimensionOf0(xs) = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 | From (172)(163) and (153) follows: % 9.46/2.82 | (201) sdtasdt0(all_0_2_2, all_0_2_2) = all_39_0_25 % 9.46/2.82 | % 9.46/2.82 +-Applying beta-rule and splitting (131), into two cases. % 9.46/2.82 |-Branch one: % 9.46/2.82 | (202) ~ (all_23_7_22 = all_23_8_23) % 9.46/2.82 | % 9.46/2.82 | Equations (191,166) can reduce 202 to: % 9.46/2.82 | (135) $false % 9.46/2.82 | % 9.46/2.82 |-The branch is then unsatisfiable % 9.46/2.82 |-Branch two: % 9.46/2.82 | (204) all_23_7_22 = all_23_8_23 % 9.46/2.82 | (205) all_23_0_15 = all_0_0_0 | all_23_8_23 = sz00 % 9.46/2.82 | % 9.46/2.82 | Combining equations (191,204) yields a new equation: % 9.46/2.82 | (166) all_23_8_23 = all_0_5_5 % 9.46/2.82 | % 9.46/2.82 +-Applying beta-rule and splitting (205), into two cases. % 9.46/2.82 |-Branch one: % 9.46/2.82 | (207) all_23_0_15 = all_0_0_0 % 9.46/2.83 | % 9.46/2.83 | From (207) and (128) follows: % 9.46/2.83 | (208) sdtpldt0(all_23_4_19, all_23_1_16) = all_0_0_0 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (46) with all_0_4_4, all_0_4_4, all_39_3_28, all_19_0_13 and discharging atoms sdtasasdt0(all_0_4_4, all_0_4_4) = all_39_3_28, sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13, yields: % 9.46/2.83 | (209) all_39_3_28 = all_19_0_13 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (46) with all_0_4_4, all_0_4_4, all_23_4_19, all_39_3_28 and discharging atoms sdtasasdt0(all_0_4_4, all_0_4_4) = all_39_3_28, sdtasasdt0(all_0_4_4, all_0_4_4) = all_23_4_19, yields: % 9.46/2.83 | (210) all_39_3_28 = all_23_4_19 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (77) with xs, all_0_5_5, all_23_2_17, all_0_2_2 and discharging atoms sdtlbdtrb0(xs, all_0_5_5) = all_23_2_17, sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2, yields: % 9.46/2.83 | (211) all_23_2_17 = all_0_2_2 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (77) with xs, all_0_5_5, all_23_3_18, all_23_2_17 and discharging atoms sdtlbdtrb0(xs, all_0_5_5) = all_23_2_17, sdtlbdtrb0(xs, all_0_5_5) = all_23_3_18, yields: % 9.46/2.83 | (212) all_23_2_17 = all_23_3_18 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (21) with all_0_2_2, all_0_2_2, all_39_0_25, all_0_1_1 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_39_0_25, sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 9.46/2.83 | (213) all_39_0_25 = all_0_1_1 % 9.46/2.83 | % 9.46/2.83 | Combining equations (209,210) yields a new equation: % 9.46/2.83 | (214) all_23_4_19 = all_19_0_13 % 9.46/2.83 | % 9.46/2.83 | Combining equations (211,212) yields a new equation: % 9.46/2.83 | (215) all_23_3_18 = all_0_2_2 % 9.46/2.83 | % 9.46/2.83 | Combining equations (215,212) yields a new equation: % 9.46/2.83 | (211) all_23_2_17 = all_0_2_2 % 9.46/2.83 | % 9.46/2.83 | From (214) and (194) follows: % 9.46/2.83 | (118) sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13 % 9.46/2.83 | % 9.46/2.83 | From (215) and (197) follows: % 9.46/2.83 | (48) sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2 % 9.46/2.83 | % 9.46/2.83 | From (215)(211) and (124) follows: % 9.46/2.83 | (219) sdtasdt0(all_0_2_2, all_0_2_2) = all_23_1_16 % 9.46/2.83 | % 9.46/2.83 | From (213) and (201) follows: % 9.46/2.83 | (29) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 % 9.46/2.83 | % 9.46/2.83 | From (214) and (208) follows: % 9.46/2.83 | (221) sdtpldt0(all_19_0_13, all_23_1_16) = all_0_0_0 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (21) with all_0_2_2, all_0_2_2, all_23_1_16, all_0_1_1 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_23_1_16, sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 9.46/2.83 | (222) all_23_1_16 = all_0_1_1 % 9.46/2.83 | % 9.46/2.83 | From (222) and (219) follows: % 9.46/2.83 | (29) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 % 9.46/2.83 | % 9.46/2.83 | From (222) and (221) follows: % 9.46/2.83 | (224) sdtpldt0(all_19_0_13, all_0_1_1) = all_0_0_0 % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (7) with all_19_0_13, all_0_4_4, all_0_4_4 and discharging atoms sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13, aVector0(all_0_4_4), yields: % 9.46/2.83 | (225) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasasdt0(v2, v3) = v4 & sziznziztdt0(all_0_4_4) = v3 & sziznziztdt0(all_0_4_4) = v2 & sdtlbdtrb0(all_0_4_4, v1) = v6 & sdtlbdtrb0(all_0_4_4, v0) = v5 & aDimensionOf0(all_0_4_4) = v1 & aDimensionOf0(all_0_4_4) = v0 & sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = v8 & ( ~ (v1 = v0) | v8 = all_19_0_13 | v0 = sz00)) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (58) with all_19_0_13, all_0_4_4 and discharging atoms sdtasasdt0(all_0_4_4, all_0_4_4) = all_19_0_13, aVector0(all_0_4_4), yields: % 9.46/2.83 | (226) sdtlseqdt0(sz0z00, all_19_0_13) | ? [v0] : (aDimensionOf0(all_0_4_4) = v0 & ~ iLess0(v0, all_0_5_5)) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (67) with all_17_2_11, all_0_5_5, all_0_4_4, xs and discharging atoms sziznziztdt0(all_0_4_4) = all_17_2_11, aDimensionOf0(xs) = all_0_5_5, aVector0(all_0_4_4), aVector0(xs), yields: % 9.46/2.83 | (227) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sziznziztdt0(xs) = v1 & aDimensionOf0(v1) = v2 & aDimensionOf0(all_17_2_11) = v3 & aDimensionOf0(all_0_4_4) = v0 & ( ~ (v0 = all_0_5_5) | v3 = v2 | all_0_5_5 = sz00)) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (79) with all_17_2_11, all_0_4_4, all_0_4_4, xs and discharging atoms sziznziztdt0(all_0_4_4) = all_17_2_11, sziznziztdt0(xs) = all_0_4_4, aVector0(all_0_4_4), aVector0(xs), yields: % 9.46/2.83 | (228) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (aDimensionOf0(all_17_2_11) = v3 & aDimensionOf0(all_0_4_4) = v2 & aDimensionOf0(all_0_4_4) = v1 & aDimensionOf0(xs) = v0 & ( ~ (v1 = v0) | v3 = v2 | v0 = sz00)) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (79) with all_0_4_4, all_17_2_11, xs, all_0_4_4 and discharging atoms sziznziztdt0(all_0_4_4) = all_17_2_11, sziznziztdt0(xs) = all_0_4_4, aVector0(all_0_4_4), aVector0(xs), yields: % 9.46/2.83 | (229) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (aDimensionOf0(all_17_2_11) = v2 & aDimensionOf0(all_0_4_4) = v3 & aDimensionOf0(all_0_4_4) = v0 & aDimensionOf0(xs) = v1 & ( ~ (v1 = v0) | v3 = v2 | v0 = sz00)) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (37) with all_17_2_11, all_0_4_4 and discharging atoms sziznziztdt0(all_0_4_4) = all_17_2_11, aVector0(all_0_4_4), yields: % 9.46/2.83 | (230) ? [v0] : (aDimensionOf0(all_0_4_4) = v0 & (v0 = sz00 | ( ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(all_17_2_11, v2) = v3) | ~ (aDimensionOf0(all_17_2_11) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(all_0_4_4, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(all_0_4_4, v2) = v3) | ~ (aDimensionOf0(all_17_2_11) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(all_17_2_11, v2) = v3) & ! [v1] : ! [v2] : (v1 = all_17_2_11 | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(all_0_4_4, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = v0) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(all_17_2_11) = v1) | szszuzczcdt0(v1) = v0) & ! [v1] : ( ~ (aDimensionOf0(all_17_2_11) = v1) | aVector0(all_17_2_11))))) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (93) with all_0_5_5, all_0_3_3 and discharging atoms szszuzczcdt0(all_0_3_3) = all_0_5_5, aNaturalNumber0(all_0_3_3), yields: % 9.46/2.83 | (231) iLess0(all_0_3_3, all_0_5_5) % 9.46/2.83 | % 9.46/2.83 | Instantiating formula (10) with all_0_2_2, all_0_5_5, xs and discharging atoms sdtlbdtrb0(xs, all_0_5_5) = all_0_2_2, aVector0(xs), aNaturalNumber0(all_0_5_5), yields: % 9.46/2.83 | (232) aScalar0(all_0_2_2) % 9.46/2.83 | % 9.46/2.83 | Instantiating (230) with all_71_0_32 yields: % 9.46/2.83 | (233) aDimensionOf0(all_0_4_4) = all_71_0_32 & (all_71_0_32 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_17_2_11, v1) = v2) | ~ (aDimensionOf0(all_17_2_11) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_0_4_4, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_0_4_4, v1) = v2) | ~ (aDimensionOf0(all_17_2_11) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_17_2_11, v1) = v2) & ! [v0] : ! [v1] : (v0 = all_17_2_11 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(all_0_4_4, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_71_0_32) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(all_17_2_11) = v0) | szszuzczcdt0(v0) = all_71_0_32) & ! [v0] : ( ~ (aDimensionOf0(all_17_2_11) = v0) | aVector0(all_17_2_11)))) % 9.46/2.83 | % 9.46/2.83 | Applying alpha-rule on (233) yields: % 9.46/2.83 | (234) aDimensionOf0(all_0_4_4) = all_71_0_32 % 9.46/2.83 | (235) all_71_0_32 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_17_2_11, v1) = v2) | ~ (aDimensionOf0(all_17_2_11) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_0_4_4, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(all_0_4_4, v1) = v2) | ~ (aDimensionOf0(all_17_2_11) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(all_17_2_11, v1) = v2) & ! [v0] : ! [v1] : (v0 = all_17_2_11 | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(all_0_4_4, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_71_0_32) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(all_17_2_11) = v0) | szszuzczcdt0(v0) = all_71_0_32) & ! [v0] : ( ~ (aDimensionOf0(all_17_2_11) = v0) | aVector0(all_17_2_11))) % 9.46/2.83 | % 9.46/2.83 | Instantiating (229) with all_73_0_33, all_73_1_34, all_73_2_35, all_73_3_36 yields: % 9.46/2.83 | (236) aDimensionOf0(all_17_2_11) = all_73_1_34 & aDimensionOf0(all_0_4_4) = all_73_0_33 & aDimensionOf0(all_0_4_4) = all_73_3_36 & aDimensionOf0(xs) = all_73_2_35 & ( ~ (all_73_2_35 = all_73_3_36) | all_73_0_33 = all_73_1_34 | all_73_3_36 = sz00) % 9.46/2.83 | % 9.46/2.83 | Applying alpha-rule on (236) yields: % 9.46/2.83 | (237) aDimensionOf0(all_0_4_4) = all_73_3_36 % 9.46/2.83 | (238) aDimensionOf0(all_0_4_4) = all_73_0_33 % 9.46/2.83 | (239) ~ (all_73_2_35 = all_73_3_36) | all_73_0_33 = all_73_1_34 | all_73_3_36 = sz00 % 9.46/2.83 | (240) aDimensionOf0(all_17_2_11) = all_73_1_34 % 9.46/2.83 | (241) aDimensionOf0(xs) = all_73_2_35 % 9.46/2.83 | % 9.46/2.83 | Instantiating (227) with all_75_0_37, all_75_1_38, all_75_2_39, all_75_3_40 yields: % 9.46/2.83 | (242) sziznziztdt0(xs) = all_75_2_39 & aDimensionOf0(all_75_2_39) = all_75_1_38 & aDimensionOf0(all_17_2_11) = all_75_0_37 & aDimensionOf0(all_0_4_4) = all_75_3_40 & ( ~ (all_75_3_40 = all_0_5_5) | all_75_0_37 = all_75_1_38 | all_0_5_5 = sz00) % 9.46/2.83 | % 9.46/2.83 | Applying alpha-rule on (242) yields: % 9.46/2.83 | (243) sziznziztdt0(xs) = all_75_2_39 % 9.46/2.83 | (244) ~ (all_75_3_40 = all_0_5_5) | all_75_0_37 = all_75_1_38 | all_0_5_5 = sz00 % 9.46/2.83 | (245) aDimensionOf0(all_75_2_39) = all_75_1_38 % 9.46/2.83 | (246) aDimensionOf0(all_17_2_11) = all_75_0_37 % 9.46/2.83 | (247) aDimensionOf0(all_0_4_4) = all_75_3_40 % 9.46/2.83 | % 9.46/2.83 | Instantiating (228) with all_77_0_41, all_77_1_42, all_77_2_43, all_77_3_44 yields: % 9.46/2.83 | (248) aDimensionOf0(all_17_2_11) = all_77_0_41 & aDimensionOf0(all_0_4_4) = all_77_1_42 & aDimensionOf0(all_0_4_4) = all_77_2_43 & aDimensionOf0(xs) = all_77_3_44 & ( ~ (all_77_2_43 = all_77_3_44) | all_77_0_41 = all_77_1_42 | all_77_3_44 = sz00) % 9.46/2.83 | % 9.46/2.83 | Applying alpha-rule on (248) yields: % 9.46/2.83 | (249) aDimensionOf0(all_0_4_4) = all_77_2_43 % 9.46/2.83 | (250) aDimensionOf0(xs) = all_77_3_44 % 9.46/2.83 | (251) aDimensionOf0(all_17_2_11) = all_77_0_41 % 9.46/2.83 | (252) ~ (all_77_2_43 = all_77_3_44) | all_77_0_41 = all_77_1_42 | all_77_3_44 = sz00 % 9.46/2.83 | (253) aDimensionOf0(all_0_4_4) = all_77_1_42 % 9.46/2.83 | % 9.46/2.83 | Instantiating (225) with all_79_0_45, all_79_1_46, all_79_2_47, all_79_3_48, all_79_4_49, all_79_5_50, all_79_6_51, all_79_7_52, all_79_8_53 yields: % 9.46/2.83 | (254) sdtasasdt0(all_79_6_51, all_79_5_50) = all_79_4_49 & sziznziztdt0(all_0_4_4) = all_79_5_50 & sziznziztdt0(all_0_4_4) = all_79_6_51 & sdtlbdtrb0(all_0_4_4, all_79_7_52) = all_79_2_47 & sdtlbdtrb0(all_0_4_4, all_79_8_53) = all_79_3_48 & aDimensionOf0(all_0_4_4) = all_79_7_52 & aDimensionOf0(all_0_4_4) = all_79_8_53 & sdtasdt0(all_79_3_48, all_79_2_47) = all_79_1_46 & sdtpldt0(all_79_4_49, all_79_1_46) = all_79_0_45 & ( ~ (all_79_7_52 = all_79_8_53) | all_79_0_45 = all_19_0_13 | all_79_8_53 = sz00) % 9.46/2.83 | % 9.46/2.83 | Applying alpha-rule on (254) yields: % 9.46/2.83 | (255) sziznziztdt0(all_0_4_4) = all_79_5_50 % 9.46/2.83 | (256) sdtpldt0(all_79_4_49, all_79_1_46) = all_79_0_45 % 9.46/2.83 | (257) sdtasdt0(all_79_3_48, all_79_2_47) = all_79_1_46 % 9.46/2.83 | (258) ~ (all_79_7_52 = all_79_8_53) | all_79_0_45 = all_19_0_13 | all_79_8_53 = sz00 % 9.46/2.83 | (259) aDimensionOf0(all_0_4_4) = all_79_7_52 % 9.46/2.84 | (260) sdtasasdt0(all_79_6_51, all_79_5_50) = all_79_4_49 % 9.46/2.84 | (261) sziznziztdt0(all_0_4_4) = all_79_6_51 % 9.46/2.84 | (262) sdtlbdtrb0(all_0_4_4, all_79_8_53) = all_79_3_48 % 9.46/2.84 | (263) aDimensionOf0(all_0_4_4) = all_79_8_53 % 9.46/2.84 | (264) sdtlbdtrb0(all_0_4_4, all_79_7_52) = all_79_2_47 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (41) with xs, all_75_2_39, all_0_4_4 and discharging atoms sziznziztdt0(xs) = all_75_2_39, sziznziztdt0(xs) = all_0_4_4, yields: % 9.46/2.84 | (265) all_75_2_39 = all_0_4_4 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_79_8_53, all_79_7_52 and discharging atoms aDimensionOf0(all_0_4_4) = all_79_7_52, aDimensionOf0(all_0_4_4) = all_79_8_53, yields: % 9.46/2.84 | (266) all_79_7_52 = all_79_8_53 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_77_2_43, all_79_8_53 and discharging atoms aDimensionOf0(all_0_4_4) = all_79_8_53, aDimensionOf0(all_0_4_4) = all_77_2_43, yields: % 9.46/2.84 | (267) all_79_8_53 = all_77_2_43 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_77_2_43, all_77_1_42 and discharging atoms aDimensionOf0(all_0_4_4) = all_77_1_42, aDimensionOf0(all_0_4_4) = all_77_2_43, yields: % 9.46/2.84 | (268) all_77_1_42 = all_77_2_43 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_75_3_40, all_77_1_42 and discharging atoms aDimensionOf0(all_0_4_4) = all_77_1_42, aDimensionOf0(all_0_4_4) = all_75_3_40, yields: % 9.46/2.84 | (269) all_77_1_42 = all_75_3_40 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_73_0_33, all_0_3_3 and discharging atoms aDimensionOf0(all_0_4_4) = all_73_0_33, aDimensionOf0(all_0_4_4) = all_0_3_3, yields: % 9.46/2.84 | (270) all_73_0_33 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_73_3_36, all_77_1_42 and discharging atoms aDimensionOf0(all_0_4_4) = all_77_1_42, aDimensionOf0(all_0_4_4) = all_73_3_36, yields: % 9.46/2.84 | (271) all_77_1_42 = all_73_3_36 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_73_3_36, all_73_0_33 and discharging atoms aDimensionOf0(all_0_4_4) = all_73_0_33, aDimensionOf0(all_0_4_4) = all_73_3_36, yields: % 9.46/2.84 | (272) all_73_0_33 = all_73_3_36 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_71_0_32, all_79_7_52 and discharging atoms aDimensionOf0(all_0_4_4) = all_79_7_52, aDimensionOf0(all_0_4_4) = all_71_0_32, yields: % 9.46/2.84 | (273) all_79_7_52 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Combining equations (266,273) yields a new equation: % 9.46/2.84 | (274) all_79_8_53 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Simplifying 274 yields: % 9.46/2.84 | (275) all_79_8_53 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Combining equations (267,275) yields a new equation: % 9.46/2.84 | (276) all_77_2_43 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Simplifying 276 yields: % 9.46/2.84 | (277) all_77_2_43 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Combining equations (271,269) yields a new equation: % 9.46/2.84 | (278) all_75_3_40 = all_73_3_36 % 9.46/2.84 | % 9.46/2.84 | Combining equations (268,269) yields a new equation: % 9.46/2.84 | (279) all_77_2_43 = all_75_3_40 % 9.46/2.84 | % 9.46/2.84 | Simplifying 279 yields: % 9.46/2.84 | (280) all_77_2_43 = all_75_3_40 % 9.46/2.84 | % 9.46/2.84 | Combining equations (280,277) yields a new equation: % 9.46/2.84 | (281) all_75_3_40 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Simplifying 281 yields: % 9.46/2.84 | (282) all_75_3_40 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Combining equations (278,282) yields a new equation: % 9.46/2.84 | (283) all_73_3_36 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Simplifying 283 yields: % 9.46/2.84 | (284) all_73_3_36 = all_71_0_32 % 9.46/2.84 | % 9.46/2.84 | Combining equations (272,270) yields a new equation: % 9.46/2.84 | (285) all_73_3_36 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | Simplifying 285 yields: % 9.46/2.84 | (286) all_73_3_36 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | Combining equations (286,284) yields a new equation: % 9.46/2.84 | (287) all_71_0_32 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | From (265) and (245) follows: % 9.46/2.84 | (288) aDimensionOf0(all_0_4_4) = all_75_1_38 % 9.46/2.84 | % 9.46/2.84 | From (287) and (234) follows: % 9.46/2.84 | (81) aDimensionOf0(all_0_4_4) = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_75_1_38, all_0_3_3 and discharging atoms aDimensionOf0(all_0_4_4) = all_75_1_38, aDimensionOf0(all_0_4_4) = all_0_3_3, yields: % 9.46/2.84 | (290) all_75_1_38 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | From (290) and (288) follows: % 9.46/2.84 | (81) aDimensionOf0(all_0_4_4) = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 +-Applying beta-rule and splitting (226), into two cases. % 9.46/2.84 |-Branch one: % 9.46/2.84 | (292) sdtlseqdt0(sz0z00, all_19_0_13) % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (57) with all_0_1_1, all_0_2_2, all_0_2_2 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1, aScalar0(all_0_2_2), yields: % 9.46/2.84 | (293) aScalar0(all_0_1_1) % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (17) with all_0_0_0, all_0_1_1, all_19_0_13 and discharging atoms sdtpldt0(all_19_0_13, all_0_1_1) = all_0_0_0, sdtlseqdt0(sz0z00, all_19_0_13), sdtlseqdt0(sz0z00, all_0_1_1), aScalar0(all_19_0_13), aScalar0(all_0_1_1), ~ sdtlseqdt0(sz0z00, all_0_0_0), yields: % 9.46/2.84 | (294) $false % 9.46/2.84 | % 9.46/2.84 |-The branch is then unsatisfiable % 9.46/2.84 |-Branch two: % 9.46/2.84 | (295) ~ sdtlseqdt0(sz0z00, all_19_0_13) % 9.46/2.84 | (296) ? [v0] : (aDimensionOf0(all_0_4_4) = v0 & ~ iLess0(v0, all_0_5_5)) % 9.46/2.84 | % 9.46/2.84 | Instantiating (296) with all_99_0_60 yields: % 9.46/2.84 | (297) aDimensionOf0(all_0_4_4) = all_99_0_60 & ~ iLess0(all_99_0_60, all_0_5_5) % 9.46/2.84 | % 9.46/2.84 | Applying alpha-rule on (297) yields: % 9.46/2.84 | (298) aDimensionOf0(all_0_4_4) = all_99_0_60 % 9.46/2.84 | (299) ~ iLess0(all_99_0_60, all_0_5_5) % 9.46/2.84 | % 9.46/2.84 | Instantiating formula (85) with all_0_4_4, all_99_0_60, all_0_3_3 and discharging atoms aDimensionOf0(all_0_4_4) = all_99_0_60, aDimensionOf0(all_0_4_4) = all_0_3_3, yields: % 9.46/2.84 | (300) all_99_0_60 = all_0_3_3 % 9.46/2.84 | % 9.46/2.84 | From (300) and (299) follows: % 9.46/2.84 | (301) ~ iLess0(all_0_3_3, all_0_5_5) % 9.46/2.84 | % 9.46/2.84 | Using (231) and (301) yields: % 9.46/2.84 | (294) $false % 9.46/2.84 | % 9.46/2.84 |-The branch is then unsatisfiable % 9.46/2.84 |-Branch two: % 9.46/2.84 | (303) ~ (all_23_0_15 = all_0_0_0) % 9.46/2.84 | (304) all_23_8_23 = sz00 % 9.46/2.84 | % 9.46/2.84 | Combining equations (166,304) yields a new equation: % 9.46/2.84 | (305) all_0_5_5 = sz00 % 9.46/2.84 | % 9.46/2.84 | Simplifying 305 yields: % 9.46/2.84 | (134) all_0_5_5 = sz00 % 9.46/2.84 | % 9.46/2.84 | Equations (134) can reduce 71 to: % 9.46/2.84 | (135) $false % 9.46/2.84 | % 9.46/2.84 |-The branch is then unsatisfiable % 9.46/2.84 % SZS output end Proof for theBenchmark % 9.46/2.84 % 9.46/2.84 2237ms %------------------------------------------------------------------------------