%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : RNG076+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n028.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:16 EDT 2022 % Result : Theorem 39.16s 14.06s % Output : Proof 50.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG076+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n028.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 15:50:35 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.58 ____ _ % 0.19/0.58 ___ / __ \_____(_)___ ________ __________ % 0.19/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.19/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.19/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic % 0.19/0.58 (ePrincess v.1.0) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2015 % 0.19/0.58 (c) Peter Backeman, 2014-2015 % 0.19/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.19/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.19/0.58 Bug reports to peter@backeman.se % 0.19/0.58 % 0.19/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.75/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.71/0.99 Prover 0: Preprocessing ... % 3.63/1.51 Prover 0: Constructing countermodel ... % 17.55/5.92 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 17.96/6.02 Prover 1: Preprocessing ... % 18.32/6.14 Prover 1: Constructing countermodel ... % 26.81/8.52 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 27.13/8.59 Prover 2: Preprocessing ... % 27.91/8.81 Prover 2: Warning: ignoring some quantifiers % 27.91/8.82 Prover 2: Constructing countermodel ... % 34.66/11.62 Prover 0: stopped % 35.02/11.82 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 35.31/11.87 Prover 3: Preprocessing ... % 35.31/11.91 Prover 3: Constructing countermodel ... % 39.16/14.05 Prover 3: proved (2232ms) % 39.16/14.06 Prover 2: stopped % 39.16/14.06 Prover 1: stopped % 39.16/14.06 % 39.16/14.06 No countermodel exists, formula is valid % 39.16/14.06 % SZS status Theorem for theBenchmark % 39.16/14.06 % 39.16/14.06 Generating proof ... found it (size 138) % 49.38/17.57 % 49.38/17.57 % SZS output start Proof for theBenchmark % 49.38/17.57 Assumed formulas after preprocessing and simplification: % 49.38/17.57 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ( ~ (v1 = sz00) & sdtasasdt0(xq, xq) = xD & sdtasasdt0(xp, xq) = xE & sdtasasdt0(xp, xp) = xC & sziznziztdt0(xt) = xq & sziznziztdt0(xs) = xp & sdtlbdtrb0(xt, v1) = xB & sdtlbdtrb0(xs, v1) = xA & aDimensionOf0(xt) = v1 & aDimensionOf0(xs) = v1 & smndt0(sz0z00) = v0 & sdtasdt0(xR, xS) = xN & sdtasdt0(xH, xH) = v6 & sdtasdt0(xF, xD) = xS & sdtasdt0(xE, xH) = xP & sdtasdt0(xE, xE) = v2 & sdtasdt0(xC, xG) = xR & sdtasdt0(xC, xD) = v3 & sdtasdt0(xB, xB) = xG & sdtasdt0(xA, xB) = xH & sdtasdt0(xA, xA) = xF & sdtpldt0(v5, v6) = v9 & sdtpldt0(v4, v6) = v7 & sdtpldt0(v3, v9) = v10 & sdtpldt0(v2, v7) = v8 & sdtpldt0(xP, xP) = v4 & sdtpldt0(xR, xS) = v5 & aVector0(xq) & aVector0(xp) & aVector0(xt) & aVector0(xs) & sdtlseqdt0(v4, v5) & sdtlseqdt0(v2, v3) & aScalar0(xN) & aScalar0(xS) & aScalar0(xP) & aScalar0(xR) & aScalar0(xH) & aScalar0(xG) & aScalar0(xF) & aScalar0(xE) & aScalar0(xD) & aScalar0(xC) & aScalar0(xB) & aScalar0(xA) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(v8, v10) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (sdtasdt0(v12, v14) = v19) | ~ (sdtasdt0(v12, v13) = v18) | ~ (sdtasdt0(v11, v14) = v16) | ~ (sdtasdt0(v11, v13) = v15) | ~ (sdtpldt0(v18, v19) = v20) | ~ (sdtpldt0(v17, v20) = v21) | ~ (sdtpldt0(v15, v16) = v17) | ~ aScalar0(v14) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | ? [v22] : ? [v23] : (sdtasdt0(v22, v23) = v21 & sdtpldt0(v13, v14) = v23 & sdtpldt0(v11, v12) = v22)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v13 = sz00 | ~ (sdtasasdt0(v14, v15) = v16) | ~ (sziznziztdt0(v12) = v15) | ~ (sziznziztdt0(v11) = v14) | ~ (sdtlbdtrb0(v12, v13) = v18) | ~ (sdtlbdtrb0(v11, v13) = v17) | ~ (aDimensionOf0(v12) = v13) | ~ (aDimensionOf0(v11) = v13) | ~ (sdtasdt0(v17, v18) = v19) | ~ (sdtpldt0(v16, v19) = v20) | ~ aVector0(v12) | ~ aVector0(v11) | sdtasasdt0(v11, v12) = v20) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtasdt0(v12, v14) = v16) | ~ (sdtasdt0(v11, v13) = v15) | ~ sdtlseqdt0(v13, v14) | ~ sdtlseqdt0(v11, v12) | ~ sdtlseqdt0(sz0z00, v13) | ~ aScalar0(v14) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | sdtlseqdt0(v15, v16)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtasdt0(v11, v13) = v15) | ~ (sdtasdt0(v11, v12) = v14) | ~ (sdtpldt0(v14, v15) = v16) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : (sdtasdt0(v18, v13) = v19 & sdtasdt0(v12, v13) = v20 & sdtasdt0(v11, v17) = v16 & sdtpldt0(v15, v20) = v19 & sdtpldt0(v12, v13) = v17 & sdtpldt0(v11, v12) = v18)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtpldt0(v12, v14) = v16) | ~ (sdtpldt0(v11, v13) = v15) | ~ sdtlseqdt0(v13, v14) | ~ sdtlseqdt0(v11, v12) | ~ aScalar0(v14) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | sdtlseqdt0(v15, v16)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (sdtasasdt0(v12, v12) = v14) | ~ (sdtasasdt0(v11, v11) = v13) | ~ (sdtasdt0(v13, v14) = v15) | ~ aVector0(v12) | ~ aVector0(v11) | ? [v16] : ? [v17] : ((sdtasasdt0(v11, v12) = v16 & sdtasdt0(v16, v16) = v17 & sdtlseqdt0(v17, v15)) | (aDimensionOf0(v11) = v16 & ( ~ iLess0(v16, v1) | ( ~ (v17 = v16) & aDimensionOf0(v12) = v17))))) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (smndt0(v12) = v14) | ~ (smndt0(v11) = v13) | ~ (sdtasdt0(v13, v14) = v15) | ~ aScalar0(v12) | ~ aScalar0(v11) | sdtasdt0(v11, v12) = v15) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (sdtpldt0(v14, v13) = v15) | ~ (sdtpldt0(v11, v12) = v14) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : (sdtasdt0(v17, v13) = v18 & sdtasdt0(v12, v13) = v19 & sdtasdt0(v12, v11) = v17 & sdtasdt0(v11, v19) = v18 & sdtasdt0(v11, v12) = v17 & sdtpldt0(v12, v13) = v16 & sdtpldt0(v12, v11) = v14 & sdtpldt0(v11, v16) = v15)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v12 = v11 | ~ (sdtasasdt0(v14, v13) = v12) | ~ (sdtasasdt0(v14, v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v12 = v11 | ~ (sdtlbdtrb0(v14, v13) = v12) | ~ (sdtlbdtrb0(v14, v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v12 = v11 | ~ (sdtasdt0(v14, v13) = v12) | ~ (sdtasdt0(v14, v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v12 = v11 | ~ (sdtpldt0(v14, v13) = v12) | ~ (sdtpldt0(v14, v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (sziznziztdt0(v12) = v14) | ~ (sziznziztdt0(v11) = v13) | ~ aVector0(v12) | ~ aVector0(v11) | ? [v15] : ? [v16] : ((v16 = v15 & aDimensionOf0(v14) = v15 & aDimensionOf0(v13) = v15) | (aDimensionOf0(v12) = v16 & (v16 = sz00 | ( ~ (v16 = v15) & aDimensionOf0(v11) = v15))))) & ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (smndt0(v11) = v13) | ~ (sdtasdt0(v13, v12) = v14) | ~ aScalar0(v12) | ~ aScalar0(v11) | ? [v15] : ? [v16] : (smndt0(v16) = v14 & smndt0(v12) = v15 & sdtasdt0(v11, v15) = v14 & sdtasdt0(v11, v12) = v16)) & ! [v11] : ! [v12] : ! [v13] : (v13 = sz0z00 | ~ (sdtasasdt0(v11, v12) = v13) | ~ aVector0(v12) | ~ aVector0(v11) | ? [v14] : ? [v15] : (aDimensionOf0(v12) = v15 & ( ~ (v15 = sz00) | ( ~ (v14 = sz00) & aDimensionOf0(v11) = v14)))) & ! [v11] : ! [v12] : ! [v13] : (v13 = sz0z00 | ~ (smndt0(v11) = v12) | ~ (sdtpldt0(v12, v11) = v13) | ~ aScalar0(v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (sziznziztdt0(v13) = v12) | ~ (sziznziztdt0(v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (aDimensionOf0(v13) = v12) | ~ (aDimensionOf0(v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (smndt0(v13) = v12) | ~ (smndt0(v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (sdtasdt0(v12, v12) = v13) | ~ (sdtasdt0(v11, v11) = v13) | ~ sdtlseqdt0(sz0z00, v12) | ~ sdtlseqdt0(sz0z00, v11) | ~ aScalar0(v12) | ~ aScalar0(v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (szszuzczcdt0(v13) = v12) | ~ (szszuzczcdt0(v13) = v11)) & ! [v11] : ! [v12] : ! [v13] : (v12 = v11 | ~ (szszuzczcdt0(v12) = v13) | ~ (szszuzczcdt0(v11) = v13) | ~ aNaturalNumber0(v12) | ~ aNaturalNumber0(v11)) & ! [v11] : ! [v12] : ! [v13] : (v0 = sz0z00 | ~ (smndt0(v11) = v12) | ~ (sdtpldt0(v12, v11) = v13) | ~ aScalar0(v11)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasasdt0(v11, v12) = v13) | ~ aVector0(v12) | ~ aVector0(v11) | aScalar0(v13) | ? [v14] : ? [v15] : ( ~ (v15 = v14) & aDimensionOf0(v12) = v15 & aDimensionOf0(v11) = v14)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtlbdtrb0(v11, v12) = v13) | ~ aVector0(v11) | ~ aNaturalNumber0(v12) | aScalar0(v13)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (smndt0(v11) = v12) | ~ (sdtpldt0(v12, v11) = v13) | ~ aScalar0(v11) | (smndt0(v12) = v11 & sdtasdt0(v11, sz0z00) = sz0z00 & sdtasdt0(sz0z00, v11) = sz0z00 & sdtpldt0(v11, v12) = sz0z00 & sdtpldt0(v11, sz0z00) = v11 & sdtpldt0(sz0z00, v11) = v11)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v11, v12) = v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | aScalar0(v13)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtpldt0(v11, v12) = v13) | ~ sdtlseqdt0(sz0z00, v12) | ~ sdtlseqdt0(sz0z00, v11) | ~ aScalar0(v12) | ~ aScalar0(v11) | sdtlseqdt0(sz0z00, v13)) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtpldt0(v11, v12) = v13) | ~ sdtlseqdt0(sz0z00, v12) | ~ sdtlseqdt0(sz0z00, v11) | ~ aScalar0(v12) | ~ aScalar0(v11) | ? [v14] : (sdtasdt0(v11, v12) = v14 & sdtlseqdt0(sz0z00, v14))) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtpldt0(v11, v12) = v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | aScalar0(v13)) & ! [v11] : ! [v12] : ! [v13] : ( ~ sdtlseqdt0(v12, v13) | ~ sdtlseqdt0(v11, v12) | ~ aScalar0(v13) | ~ aScalar0(v12) | ~ aScalar0(v11) | sdtlseqdt0(v11, v13)) & ! [v11] : ! [v12] : (v12 = v11 | ~ sdtlseqdt0(v12, v11) | ~ sdtlseqdt0(v11, v12) | ~ aScalar0(v12) | ~ aScalar0(v11)) & ! [v11] : ! [v12] : ( ~ (sdtasasdt0(v11, v11) = v12) | ~ aVector0(v11) | sdtlseqdt0(sz0z00, v12)) & ! [v11] : ! [v12] : ( ~ (sziznziztdt0(v11) = v12) | ~ aVector0(v11) | ? [v13] : (aDimensionOf0(v11) = v13 & (v13 = sz00 | ( ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtlbdtrb0(v11, v15) = v16) | ~ (aDimensionOf0(v12) = v14) | ~ aNaturalNumber0(v15) | sdtlbdtrb0(v12, v15) = v16) & ! [v14] : ! [v15] : (v14 = v12 | ~ (aDimensionOf0(v14) = v15) | ~ aVector0(v14) | ? [v16] : ? [v17] : ? [v18] : (( ~ (v18 = v17) & sdtlbdtrb0(v14, v16) = v17 & sdtlbdtrb0(v11, v16) = v18 & aNaturalNumber0(v16)) | ( ~ (v16 = v13) & szszuzczcdt0(v15) = v16))) & ! [v14] : ( ~ (aDimensionOf0(v12) = v14) | szszuzczcdt0(v14) = v13) & ! [v14] : ( ~ (aDimensionOf0(v12) = v14) | aVector0(v12)))))) & ! [v11] : ! [v12] : ( ~ (aDimensionOf0(v11) = v12) | ~ aVector0(v11) | aNaturalNumber0(v12)) & ! [v11] : ! [v12] : ( ~ (smndt0(v11) = v12) | ~ aScalar0(v11) | aScalar0(v12)) & ! [v11] : ! [v12] : ( ~ (sdtasdt0(v11, v11) = v12) | ~ aScalar0(v11) | sdtlseqdt0(sz0z00, v12)) & ! [v11] : ! [v12] : ( ~ (szszuzczcdt0(v11) = v12) | ~ aNaturalNumber0(v11) | iLess0(v11, v12)) & ! [v11] : ! [v12] : ( ~ (szszuzczcdt0(v11) = v12) | ~ aNaturalNumber0(v11) | aNaturalNumber0(v12)) & ! [v11] : ! [v12] : ( ~ aScalar0(v12) | ~ aScalar0(v11) | sdtlseqdt0(v12, v11) | sdtlseqdt0(v11, v12)) & ! [v11] : (v11 = sz00 | ~ aNaturalNumber0(v11) | ? [v12] : (szszuzczcdt0(v12) = v11 & aNaturalNumber0(v12))) & ! [v11] : ( ~ (szszuzczcdt0(v11) = sz00) | ~ aNaturalNumber0(v11)) & ! [v11] : ( ~ aScalar0(v11) | sdtlseqdt0(v11, v11))) % 49.75/17.62 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10 yields: % 49.75/17.62 | (1) ~ (all_0_9_9 = sz00) & sdtasasdt0(xq, xq) = xD & sdtasasdt0(xp, xq) = xE & sdtasasdt0(xp, xp) = xC & sziznziztdt0(xt) = xq & sziznziztdt0(xs) = xp & sdtlbdtrb0(xt, all_0_9_9) = xB & sdtlbdtrb0(xs, all_0_9_9) = xA & aDimensionOf0(xt) = all_0_9_9 & aDimensionOf0(xs) = all_0_9_9 & smndt0(sz0z00) = all_0_10_10 & sdtasdt0(xR, xS) = xN & sdtasdt0(xH, xH) = all_0_4_4 & sdtasdt0(xF, xD) = xS & sdtasdt0(xE, xH) = xP & sdtasdt0(xE, xE) = all_0_8_8 & sdtasdt0(xC, xG) = xR & sdtasdt0(xC, xD) = all_0_7_7 & sdtasdt0(xB, xB) = xG & sdtasdt0(xA, xB) = xH & sdtasdt0(xA, xA) = xF & sdtpldt0(all_0_5_5, all_0_4_4) = all_0_1_1 & sdtpldt0(all_0_6_6, all_0_4_4) = all_0_3_3 & sdtpldt0(all_0_7_7, all_0_1_1) = all_0_0_0 & sdtpldt0(all_0_8_8, all_0_3_3) = all_0_2_2 & sdtpldt0(xP, xP) = all_0_6_6 & sdtpldt0(xR, xS) = all_0_5_5 & aVector0(xq) & aVector0(xp) & aVector0(xt) & aVector0(xs) & sdtlseqdt0(all_0_6_6, all_0_5_5) & sdtlseqdt0(all_0_8_8, all_0_7_7) & aScalar0(xN) & aScalar0(xS) & aScalar0(xP) & aScalar0(xR) & aScalar0(xH) & aScalar0(xG) & aScalar0(xF) & aScalar0(xE) & aScalar0(xD) & aScalar0(xC) & aScalar0(xB) & aScalar0(xA) & aScalar0(sz0z00) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(all_0_2_2, 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] : ( ~ (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(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v4, v9) = v8 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v3) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasasdt0(v1, v1) = v3) | ~ (sdtasasdt0(v0, v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v5] : ? [v6] : ((sdtasasdt0(v0, v1) = v5 & sdtasdt0(v5, v5) = v6 & sdtlseqdt0(v6, v4)) | (aDimensionOf0(v0) = v5 & ( ~ iLess0(v5, all_0_9_9) | ( ~ (v6 = v5) & aDimensionOf0(v1) = v6))))) & ! [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] : ( ~ (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] : (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] : ((v5 = v4 & aDimensionOf0(v3) = v4 & aDimensionOf0(v2) = v4) | (aDimensionOf0(v1) = v5 & (v5 = sz00 | ( ~ (v5 = v4) & aDimensionOf0(v0) = 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 & ( ~ (v4 = sz00) | ( ~ (v3 = sz00) & aDimensionOf0(v0) = v3)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) & ! [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_10_10 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = 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] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | aScalar0(v2)) & ! [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] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(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 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v1) | ~ aScalar0(v0)) & ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1)) & ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (aDimensionOf0(v0) = v2 & (v2 = sz00 | ( ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlbdtrb0(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] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | aNaturalNumber0(v1)) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | aScalar0(v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v1)) & ! [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)) % 49.75/17.64 | % 49.75/17.64 | Applying alpha-rule on (1) yields: % 49.75/17.64 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 49.75/17.64 | (3) sdtasdt0(xE, xH) = xP % 49.75/17.64 | (4) sdtpldt0(all_0_5_5, all_0_4_4) = all_0_1_1 % 49.75/17.64 | (5) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3] : ? [v4] : (aDimensionOf0(v1) = v4 & ( ~ (v4 = sz00) | ( ~ (v3 = sz00) & aDimensionOf0(v0) = v3)))) % 49.75/17.64 | (6) ~ (all_0_9_9 = sz00) % 49.75/17.64 | (7) ! [v0] : ! [v1] : ! [v2] : (all_0_10_10 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 49.75/17.64 | (8) sdtpldt0(xP, xP) = all_0_6_6 % 49.75/17.64 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 49.75/17.64 | (10) sziznziztdt0(xt) = xq % 49.75/17.64 | (11) sdtpldt0(all_0_8_8, all_0_3_3) = all_0_2_2 % 49.75/17.64 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 49.75/17.64 | (13) aScalar0(sz0z00) % 49.75/17.64 | (14) ~ sdtlseqdt0(all_0_2_2, all_0_0_0) % 49.75/17.64 | (15) sdtasdt0(xC, xG) = xR % 49.75/17.64 | (16) ! [v0] : (v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1))) % 49.75/17.64 | (17) aScalar0(xS) % 49.75/17.64 | (18) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aScalar0(v0) | aScalar0(v1)) % 49.75/17.64 | (19) sdtasdt0(xR, xS) = xN % 49.75/17.64 | (20) sdtasasdt0(xq, xq) = xD % 49.75/17.64 | (21) ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aNaturalNumber0(v0)) % 49.75/17.64 | (22) aVector0(xq) % 49.75/17.64 | (23) ! [v0] : ! [v1] : ( ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | aNaturalNumber0(v1)) % 49.75/17.64 | (24) aScalar0(xC) % 49.75/17.64 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v4] : ? [v5] : ((v5 = v4 & aDimensionOf0(v3) = v4 & aDimensionOf0(v2) = v4) | (aDimensionOf0(v1) = v5 & (v5 = sz00 | ( ~ (v5 = v4) & aDimensionOf0(v0) = v4))))) % 49.75/17.64 | (26) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) % 49.75/17.64 | (27) sdtasdt0(xA, xB) = xH % 49.75/17.64 | (28) aScalar0(xP) % 49.75/17.64 | (29) sdtasasdt0(xp, xq) = xE % 49.75/17.64 | (30) ! [v0] : ! [v1] : ( ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) % 49.75/17.64 | (31) ! [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)) % 49.75/17.64 | (32) sdtpldt0(xR, xS) = all_0_5_5 % 49.75/17.64 | (33) sdtasdt0(xB, xB) = xG % 49.75/17.64 | (34) aVector0(xs) % 49.75/17.64 | (35) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v1)) % 49.75/17.64 | (36) aVector0(xt) % 49.75/17.64 | (37) aDimensionOf0(xs) = all_0_9_9 % 49.75/17.64 | (38) ! [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)) % 49.75/17.65 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 49.75/17.65 | (40) ! [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))) % 49.75/17.65 | (41) sdtlbdtrb0(xs, all_0_9_9) = xA % 49.75/17.65 | (42) sdtpldt0(all_0_6_6, all_0_4_4) = all_0_3_3 % 49.75/17.65 | (43) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v1)) % 49.75/17.65 | (44) ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1)) % 49.75/17.65 | (45) aScalar0(xF) % 49.75/17.65 | (46) sdtasasdt0(xp, xp) = xC % 49.75/17.65 | (47) aDimensionOf0(xt) = all_0_9_9 % 49.75/17.65 | (48) sdtlseqdt0(all_0_8_8, all_0_7_7) % 49.75/17.65 | (49) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) % 49.75/17.65 | (50) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 49.75/17.65 | (51) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) % 49.75/17.65 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 49.75/17.65 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 49.75/17.65 | (54) ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ~ aVector0(v0) | ? [v2] : (aDimensionOf0(v0) = v2 & (v2 = sz00 | ( ! [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)))))) % 49.75/17.65 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sdtasdt0(v1, v1) = v2) | ~ (sdtasdt0(v0, v0) = v2) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 49.75/17.65 | (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)) % 49.75/17.65 | (57) ! [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) % 49.75/17.65 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 49.75/17.65 | (59) aNaturalNumber0(sz00) % 49.75/17.65 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 49.75/17.65 | (61) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aVector0(v1) | ~ aVector0(v0) | aScalar0(v2) | ? [v3] : ? [v4] : ( ~ (v4 = v3) & aDimensionOf0(v1) = v4 & aDimensionOf0(v0) = v3)) % 49.75/17.65 | (62) aScalar0(xB) % 49.75/17.65 | (63) ! [v0] : ( ~ aScalar0(v0) | sdtlseqdt0(v0, v0)) % 49.75/17.65 | (64) sdtlseqdt0(all_0_6_6, all_0_5_5) % 49.75/17.65 | (65) sziznziztdt0(xs) = xp % 49.75/17.65 | (66) aScalar0(xR) % 49.75/17.65 | (67) aScalar0(xE) % 49.75/17.65 | (68) aVector0(xp) % 49.75/17.65 | (69) aScalar0(xG) % 49.75/17.65 | (70) sdtasdt0(xA, xA) = xF % 49.75/17.65 | (71) aScalar0(xH) % 49.75/17.65 | (72) sdtasdt0(xH, xH) = all_0_4_4 % 49.75/17.65 | (73) smndt0(sz0z00) = all_0_10_10 % 49.75/17.65 | (74) ! [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)) % 49.75/17.65 | (75) aScalar0(xD) % 49.75/17.65 | (76) ! [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)) % 49.75/17.66 | (77) ! [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)) % 49.75/17.66 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtasdt0(v0, v1) = v4) % 49.75/17.66 | (79) aScalar0(xN) % 49.75/17.66 | (80) sdtasdt0(xC, xD) = all_0_7_7 % 49.75/17.66 | (81) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v1) | ~ aScalar0(v0)) % 49.75/17.66 | (82) ! [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)) % 49.75/17.66 | (83) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ~ aScalar0(v0)) % 49.75/17.66 | (84) sdtasdt0(xF, xD) = xS % 49.75/17.66 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 49.75/17.66 | (86) sdtpldt0(all_0_7_7, all_0_1_1) = all_0_0_0 % 49.75/17.66 | (87) sdtlbdtrb0(xt, all_0_9_9) = xB % 49.75/17.66 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aScalar0(v2) | ~ aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(v0, v2)) % 49.75/17.66 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasasdt0(v1, v1) = v3) | ~ (sdtasasdt0(v0, v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v5] : ? [v6] : ((sdtasasdt0(v0, v1) = v5 & sdtasdt0(v5, v5) = v6 & sdtlseqdt0(v6, v4)) | (aDimensionOf0(v0) = v5 & ( ~ iLess0(v5, all_0_9_9) | ( ~ (v6 = v5) & aDimensionOf0(v1) = v6))))) % 49.75/17.66 | (90) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | aScalar0(v2)) % 49.75/17.66 | (91) aScalar0(xA) % 49.75/17.66 | (92) sdtasdt0(xE, xE) = all_0_8_8 % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (54) with xp, xs and discharging atoms sziznziztdt0(xs) = xp, aVector0(xs), yields: % 49.75/17.66 | (93) ? [v0] : (aDimensionOf0(xs) = v0 & (v0 = sz00 | ( ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xs, v2) = v3) | ~ (aDimensionOf0(xp) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xp, v2) = v3) & ! [v1] : ! [v2] : (v1 = xp | ~ (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(xp) = v1) | szszuzczcdt0(v1) = v0) & ! [v1] : ( ~ (aDimensionOf0(xp) = v1) | aVector0(xp))))) % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (23) with all_0_9_9, xs and discharging atoms aDimensionOf0(xs) = all_0_9_9, aVector0(xs), yields: % 49.75/17.66 | (94) aNaturalNumber0(all_0_9_9) % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (89) with all_0_7_7, xD, xC, xq, xp and discharging atoms sdtasasdt0(xq, xq) = xD, sdtasasdt0(xp, xp) = xC, sdtasdt0(xC, xD) = all_0_7_7, aVector0(xq), aVector0(xp), yields: % 49.75/17.66 | (95) ? [v0] : ? [v1] : ((sdtasasdt0(xp, xq) = v0 & sdtasdt0(v0, v0) = v1 & sdtlseqdt0(v1, all_0_7_7)) | (aDimensionOf0(xp) = v0 & ( ~ iLess0(v0, all_0_9_9) | ( ~ (v1 = v0) & aDimensionOf0(xq) = v1)))) % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (54) with xq, xt and discharging atoms sziznziztdt0(xt) = xq, aVector0(xt), yields: % 49.75/17.66 | (96) ? [v0] : (aDimensionOf0(xt) = v0 & (v0 = sz00 | ( ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlbdtrb0(xt, v2) = v3) | ~ (aDimensionOf0(xq) = v1) | ~ aNaturalNumber0(v2) | sdtlbdtrb0(xq, v2) = v3) & ! [v1] : ! [v2] : (v1 = xq | ~ (aDimensionOf0(v1) = v2) | ~ aVector0(v1) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v5 = v4) & sdtlbdtrb0(v1, v3) = v4 & sdtlbdtrb0(xt, v3) = v5 & aNaturalNumber0(v3)) | ( ~ (v3 = v0) & szszuzczcdt0(v2) = v3))) & ! [v1] : ( ~ (aDimensionOf0(xq) = v1) | szszuzczcdt0(v1) = v0) & ! [v1] : ( ~ (aDimensionOf0(xq) = v1) | aVector0(xq))))) % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (25) with xq, xp, xt, xs and discharging atoms sziznziztdt0(xt) = xq, sziznziztdt0(xs) = xp, aVector0(xt), aVector0(xs), yields: % 49.75/17.66 | (97) ? [v0] : ? [v1] : ((v1 = v0 & aDimensionOf0(xq) = v0 & aDimensionOf0(xp) = v0) | (aDimensionOf0(xt) = v1 & (v1 = sz00 | ( ~ (v1 = v0) & aDimensionOf0(xs) = v0)))) % 49.75/17.66 | % 49.75/17.66 | Instantiating formula (25) with xp, xp, xs, xs and discharging atoms sziznziztdt0(xs) = xp, aVector0(xs), yields: % 49.75/17.66 | (98) ? [v0] : ? [v1] : ((v1 = v0 & aDimensionOf0(xp) = v0) | (aDimensionOf0(xs) = v1 & (v1 = sz00 | ( ~ (v1 = v0) & aDimensionOf0(xs) = v0)))) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (25) with xp, xq, xs, xt and discharging atoms sziznziztdt0(xt) = xq, sziznziztdt0(xs) = xp, aVector0(xt), aVector0(xs), yields: % 49.75/17.67 | (99) ? [v0] : ? [v1] : ((v1 = v0 & aDimensionOf0(xq) = v0 & aDimensionOf0(xp) = v0) | (aDimensionOf0(xs) = v1 & (v1 = sz00 | ( ~ (v1 = v0) & aDimensionOf0(xt) = v0)))) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (60) with all_0_5_5, xS, xR and discharging atoms sdtpldt0(xR, xS) = all_0_5_5, aScalar0(xS), aScalar0(xR), yields: % 49.75/17.67 | (100) aScalar0(all_0_5_5) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (60) with all_0_6_6, xP, xP and discharging atoms sdtpldt0(xP, xP) = all_0_6_6, aScalar0(xP), yields: % 49.75/17.67 | (101) aScalar0(all_0_6_6) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (53) with all_0_4_4, xH, xH and discharging atoms sdtasdt0(xH, xH) = all_0_4_4, aScalar0(xH), yields: % 49.75/17.67 | (102) aScalar0(all_0_4_4) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (53) with all_0_8_8, xE, xE and discharging atoms sdtasdt0(xE, xE) = all_0_8_8, aScalar0(xE), yields: % 49.75/17.67 | (103) aScalar0(all_0_8_8) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (53) with all_0_7_7, xD, xC and discharging atoms sdtasdt0(xC, xD) = all_0_7_7, aScalar0(xD), aScalar0(xC), yields: % 49.75/17.67 | (104) aScalar0(all_0_7_7) % 49.75/17.67 | % 49.75/17.67 | Instantiating (93) with all_9_0_11 yields: % 49.75/17.67 | (105) aDimensionOf0(xs) = all_9_0_11 & (all_9_0_11 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) & ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp)))) % 49.75/17.67 | % 49.75/17.67 | Applying alpha-rule on (105) yields: % 49.75/17.67 | (106) aDimensionOf0(xs) = all_9_0_11 % 49.75/17.67 | (107) all_9_0_11 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) & ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp))) % 49.75/17.67 | % 49.75/17.67 | Instantiating (99) with all_11_0_12, all_11_1_13 yields: % 49.75/17.67 | (108) (all_11_0_12 = all_11_1_13 & aDimensionOf0(xq) = all_11_1_13 & aDimensionOf0(xp) = all_11_1_13) | (aDimensionOf0(xs) = all_11_0_12 & (all_11_0_12 = sz00 | ( ~ (all_11_0_12 = all_11_1_13) & aDimensionOf0(xt) = all_11_1_13))) % 49.75/17.67 | % 49.75/17.67 | Instantiating (97) with all_12_0_14, all_12_1_15 yields: % 49.75/17.67 | (109) (all_12_0_14 = all_12_1_15 & aDimensionOf0(xq) = all_12_1_15 & aDimensionOf0(xp) = all_12_1_15) | (aDimensionOf0(xt) = all_12_0_14 & (all_12_0_14 = sz00 | ( ~ (all_12_0_14 = all_12_1_15) & aDimensionOf0(xs) = all_12_1_15))) % 49.75/17.67 | % 49.75/17.67 | Instantiating (95) with all_13_0_16, all_13_1_17 yields: % 49.75/17.67 | (110) (sdtasasdt0(xp, xq) = all_13_1_17 & sdtasdt0(all_13_1_17, all_13_1_17) = all_13_0_16 & sdtlseqdt0(all_13_0_16, all_0_7_7)) | (aDimensionOf0(xp) = all_13_1_17 & ( ~ iLess0(all_13_1_17, all_0_9_9) | ( ~ (all_13_0_16 = all_13_1_17) & aDimensionOf0(xq) = all_13_0_16))) % 49.75/17.67 | % 49.75/17.67 | Instantiating (98) with all_14_0_18, all_14_1_19 yields: % 49.75/17.67 | (111) (all_14_0_18 = all_14_1_19 & aDimensionOf0(xp) = all_14_1_19) | (aDimensionOf0(xs) = all_14_0_18 & (all_14_0_18 = sz00 | ( ~ (all_14_0_18 = all_14_1_19) & aDimensionOf0(xs) = all_14_1_19))) % 49.75/17.67 | % 49.75/17.67 | Instantiating (96) with all_18_0_26 yields: % 49.75/17.67 | (112) aDimensionOf0(xt) = all_18_0_26 & (all_18_0_26 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xt, v1) = v2) | ~ (aDimensionOf0(xq) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xq, v1) = v2) & ! [v0] : ! [v1] : (v0 = xq | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xt, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_18_0_26) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | szszuzczcdt0(v0) = all_18_0_26) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | aVector0(xq)))) % 49.75/17.67 | % 49.75/17.67 | Applying alpha-rule on (112) yields: % 49.75/17.67 | (113) aDimensionOf0(xt) = all_18_0_26 % 49.75/17.67 | (114) all_18_0_26 = sz00 | ( ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xt, v1) = v2) | ~ (aDimensionOf0(xq) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xq, v1) = v2) & ! [v0] : ! [v1] : (v0 = xq | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xt, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_18_0_26) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | szszuzczcdt0(v0) = all_18_0_26) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | aVector0(xq))) % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (85) with xt, all_18_0_26, all_0_9_9 and discharging atoms aDimensionOf0(xt) = all_18_0_26, aDimensionOf0(xt) = all_0_9_9, yields: % 49.75/17.67 | (115) all_18_0_26 = all_0_9_9 % 49.75/17.67 | % 49.75/17.67 | Instantiating formula (85) with xs, all_9_0_11, all_0_9_9 and discharging atoms aDimensionOf0(xs) = all_9_0_11, aDimensionOf0(xs) = all_0_9_9, yields: % 49.75/17.67 | (116) all_9_0_11 = all_0_9_9 % 49.75/17.67 | % 49.75/17.67 | From (115) and (113) follows: % 49.75/17.67 | (47) aDimensionOf0(xt) = all_0_9_9 % 49.75/17.67 | % 49.75/17.67 | From (116) and (106) follows: % 49.75/17.67 | (37) aDimensionOf0(xs) = all_0_9_9 % 49.75/17.67 | % 49.75/17.67 +-Applying beta-rule and splitting (109), into two cases. % 49.75/17.67 |-Branch one: % 49.75/17.67 | (119) all_12_0_14 = all_12_1_15 & aDimensionOf0(xq) = all_12_1_15 & aDimensionOf0(xp) = all_12_1_15 % 49.75/17.67 | % 49.75/17.67 | Applying alpha-rule on (119) yields: % 49.75/17.68 | (120) all_12_0_14 = all_12_1_15 % 49.75/17.68 | (121) aDimensionOf0(xq) = all_12_1_15 % 49.75/17.68 | (122) aDimensionOf0(xp) = all_12_1_15 % 49.75/17.68 | % 49.75/17.68 +-Applying beta-rule and splitting (114), into two cases. % 49.75/17.68 |-Branch one: % 49.75/17.68 | (123) all_18_0_26 = sz00 % 49.75/17.68 | % 49.75/17.68 | Combining equations (123,115) yields a new equation: % 49.75/17.68 | (124) all_0_9_9 = sz00 % 49.75/17.68 | % 49.75/17.68 | Equations (124) can reduce 6 to: % 49.75/17.68 | (125) $false % 49.75/17.68 | % 49.75/17.68 |-The branch is then unsatisfiable % 49.75/17.68 |-Branch two: % 49.75/17.68 | (126) ~ (all_18_0_26 = sz00) % 49.75/17.68 | (127) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xt, v1) = v2) | ~ (aDimensionOf0(xq) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xq, v1) = v2) & ! [v0] : ! [v1] : (v0 = xq | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xt, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_18_0_26) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | szszuzczcdt0(v0) = all_18_0_26) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | aVector0(xq)) % 49.75/17.68 | % 49.75/17.68 | Equations (115) can reduce 126 to: % 49.75/17.68 | (6) ~ (all_0_9_9 = sz00) % 49.75/17.68 | % 49.75/17.68 +-Applying beta-rule and splitting (111), into two cases. % 49.75/17.68 |-Branch one: % 49.75/17.68 | (129) all_14_0_18 = all_14_1_19 & aDimensionOf0(xp) = all_14_1_19 % 49.75/17.68 | % 49.75/17.68 | Applying alpha-rule on (129) yields: % 49.75/17.68 | (130) all_14_0_18 = all_14_1_19 % 49.75/17.68 | (131) aDimensionOf0(xp) = all_14_1_19 % 49.75/17.68 | % 49.75/17.68 +-Applying beta-rule and splitting (107), into two cases. % 49.75/17.68 |-Branch one: % 49.75/17.68 | (132) all_9_0_11 = sz00 % 49.75/17.68 | % 49.75/17.68 | Combining equations (132,116) yields a new equation: % 49.75/17.68 | (124) all_0_9_9 = sz00 % 49.75/17.68 | % 49.75/17.68 | Equations (124) can reduce 6 to: % 49.75/17.68 | (125) $false % 49.75/17.68 | % 49.75/17.68 |-The branch is then unsatisfiable % 49.75/17.68 |-Branch two: % 49.75/17.68 | (135) ~ (all_9_0_11 = sz00) % 49.75/17.68 | (136) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) & ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp)) % 49.75/17.68 | % 49.75/17.68 | Applying alpha-rule on (136) yields: % 49.75/17.68 | (137) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) % 49.75/17.68 | (138) ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) % 49.75/17.68 | (139) ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) % 49.75/17.68 | (140) ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp)) % 49.75/17.68 | % 49.75/17.68 | Equations (116) can reduce 135 to: % 49.75/17.68 | (6) ~ (all_0_9_9 = sz00) % 49.75/17.68 | % 49.75/17.68 +-Applying beta-rule and splitting (108), into two cases. % 49.75/17.68 |-Branch one: % 49.75/17.68 | (142) all_11_0_12 = all_11_1_13 & aDimensionOf0(xq) = all_11_1_13 & aDimensionOf0(xp) = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | Applying alpha-rule on (142) yields: % 49.75/17.68 | (143) all_11_0_12 = all_11_1_13 % 49.75/17.68 | (144) aDimensionOf0(xq) = all_11_1_13 % 49.75/17.68 | (145) aDimensionOf0(xp) = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (85) with xp, all_14_1_19, all_12_1_15 and discharging atoms aDimensionOf0(xp) = all_14_1_19, aDimensionOf0(xp) = all_12_1_15, yields: % 49.75/17.68 | (146) all_14_1_19 = all_12_1_15 % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (85) with xp, all_14_1_19, all_11_1_13 and discharging atoms aDimensionOf0(xp) = all_14_1_19, aDimensionOf0(xp) = all_11_1_13, yields: % 49.75/17.68 | (147) all_14_1_19 = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | Combining equations (146,147) yields a new equation: % 49.75/17.68 | (148) all_12_1_15 = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | Simplifying 148 yields: % 49.75/17.68 | (149) all_12_1_15 = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | From (149) and (121) follows: % 49.75/17.68 | (144) aDimensionOf0(xq) = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | From (149) and (122) follows: % 49.75/17.68 | (145) aDimensionOf0(xp) = all_11_1_13 % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (23) with all_11_1_13, xp and discharging atoms aDimensionOf0(xp) = all_11_1_13, aVector0(xp), yields: % 49.75/17.68 | (152) aNaturalNumber0(all_11_1_13) % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (139) with all_11_1_13 and discharging atoms aDimensionOf0(xp) = all_11_1_13, yields: % 49.75/17.68 | (153) szszuzczcdt0(all_11_1_13) = all_9_0_11 % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (30) with all_0_4_4, all_0_4_4 and discharging atoms aScalar0(all_0_4_4), yields: % 49.75/17.68 | (154) sdtlseqdt0(all_0_4_4, all_0_4_4) % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (60) with all_0_1_1, all_0_4_4, all_0_5_5 and discharging atoms sdtpldt0(all_0_5_5, all_0_4_4) = all_0_1_1, aScalar0(all_0_4_4), aScalar0(all_0_5_5), yields: % 49.75/17.68 | (155) aScalar0(all_0_1_1) % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (60) with all_0_3_3, all_0_4_4, all_0_6_6 and discharging atoms sdtpldt0(all_0_6_6, all_0_4_4) = all_0_3_3, aScalar0(all_0_4_4), aScalar0(all_0_6_6), yields: % 49.75/17.68 | (156) aScalar0(all_0_3_3) % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (16) with all_0_9_9 and discharging atoms aNaturalNumber0(all_0_9_9), yields: % 49.75/17.68 | (157) all_0_9_9 = sz00 | ? [v0] : (szszuzczcdt0(v0) = all_0_9_9 & aNaturalNumber0(v0)) % 49.75/17.68 | % 49.75/17.68 | From (116) and (153) follows: % 49.75/17.68 | (158) szszuzczcdt0(all_11_1_13) = all_0_9_9 % 49.75/17.68 | % 49.75/17.68 +-Applying beta-rule and splitting (157), into two cases. % 49.75/17.68 |-Branch one: % 49.75/17.68 | (124) all_0_9_9 = sz00 % 49.75/17.68 | % 49.75/17.68 | Equations (124) can reduce 6 to: % 49.75/17.68 | (125) $false % 49.75/17.68 | % 49.75/17.68 |-The branch is then unsatisfiable % 49.75/17.68 |-Branch two: % 49.75/17.68 | (6) ~ (all_0_9_9 = sz00) % 49.75/17.68 | (162) ? [v0] : (szszuzczcdt0(v0) = all_0_9_9 & aNaturalNumber0(v0)) % 49.75/17.68 | % 49.75/17.68 | Instantiating (162) with all_74_0_39 yields: % 49.75/17.68 | (163) szszuzczcdt0(all_74_0_39) = all_0_9_9 & aNaturalNumber0(all_74_0_39) % 49.75/17.68 | % 49.75/17.68 | Applying alpha-rule on (163) yields: % 49.75/17.68 | (164) szszuzczcdt0(all_74_0_39) = all_0_9_9 % 49.75/17.68 | (165) aNaturalNumber0(all_74_0_39) % 49.75/17.68 | % 49.75/17.68 | Instantiating formula (50) with all_0_9_9, all_74_0_39, all_11_1_13 and discharging atoms szszuzczcdt0(all_74_0_39) = all_0_9_9, szszuzczcdt0(all_11_1_13) = all_0_9_9, aNaturalNumber0(all_74_0_39), aNaturalNumber0(all_11_1_13), yields: % 49.75/17.69 | (166) all_74_0_39 = all_11_1_13 % 49.75/17.69 | % 49.75/17.69 | From (166) and (164) follows: % 49.75/17.69 | (158) szszuzczcdt0(all_11_1_13) = all_0_9_9 % 49.75/17.69 | % 49.75/17.69 | From (166) and (165) follows: % 49.75/17.69 | (152) aNaturalNumber0(all_11_1_13) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (77) with all_0_1_1, all_0_3_3, all_0_4_4, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms sdtpldt0(all_0_5_5, all_0_4_4) = all_0_1_1, sdtpldt0(all_0_6_6, all_0_4_4) = all_0_3_3, sdtlseqdt0(all_0_4_4, all_0_4_4), sdtlseqdt0(all_0_6_6, all_0_5_5), aScalar0(all_0_4_4), aScalar0(all_0_5_5), aScalar0(all_0_6_6), yields: % 49.75/17.69 | (169) sdtlseqdt0(all_0_3_3, all_0_1_1) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (26) with all_0_9_9, all_11_1_13 and discharging atoms szszuzczcdt0(all_11_1_13) = all_0_9_9, aNaturalNumber0(all_11_1_13), yields: % 49.75/17.69 | (170) iLess0(all_11_1_13, all_0_9_9) % 49.75/17.69 | % 49.75/17.69 +-Applying beta-rule and splitting (110), into two cases. % 49.75/17.69 |-Branch one: % 49.75/17.69 | (171) sdtasasdt0(xp, xq) = all_13_1_17 & sdtasdt0(all_13_1_17, all_13_1_17) = all_13_0_16 & sdtlseqdt0(all_13_0_16, all_0_7_7) % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (171) yields: % 49.75/17.69 | (172) sdtasasdt0(xp, xq) = all_13_1_17 % 49.75/17.69 | (173) sdtasdt0(all_13_1_17, all_13_1_17) = all_13_0_16 % 49.75/17.69 | (174) sdtlseqdt0(all_13_0_16, all_0_7_7) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (2) with xp, xq, all_13_1_17, xE and discharging atoms sdtasasdt0(xp, xq) = all_13_1_17, sdtasasdt0(xp, xq) = xE, yields: % 49.75/17.69 | (175) all_13_1_17 = xE % 49.75/17.69 | % 49.75/17.69 | From (175)(175) and (173) follows: % 49.75/17.69 | (176) sdtasdt0(xE, xE) = all_13_0_16 % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (12) with xE, xE, all_13_0_16, all_0_8_8 and discharging atoms sdtasdt0(xE, xE) = all_13_0_16, sdtasdt0(xE, xE) = all_0_8_8, yields: % 49.75/17.69 | (177) all_13_0_16 = all_0_8_8 % 49.75/17.69 | % 49.75/17.69 | From (177) and (174) follows: % 49.75/17.69 | (48) sdtlseqdt0(all_0_8_8, all_0_7_7) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (77) with all_0_0_0, all_0_2_2, all_0_1_1, all_0_3_3, all_0_7_7, all_0_8_8 and discharging atoms sdtpldt0(all_0_7_7, all_0_1_1) = all_0_0_0, sdtpldt0(all_0_8_8, all_0_3_3) = all_0_2_2, sdtlseqdt0(all_0_3_3, all_0_1_1), sdtlseqdt0(all_0_8_8, all_0_7_7), aScalar0(all_0_1_1), aScalar0(all_0_3_3), aScalar0(all_0_7_7), aScalar0(all_0_8_8), ~ sdtlseqdt0(all_0_2_2, all_0_0_0), yields: % 49.75/17.69 | (179) $false % 49.75/17.69 | % 49.75/17.69 |-The branch is then unsatisfiable % 49.75/17.69 |-Branch two: % 49.75/17.69 | (180) aDimensionOf0(xp) = all_13_1_17 & ( ~ iLess0(all_13_1_17, all_0_9_9) | ( ~ (all_13_0_16 = all_13_1_17) & aDimensionOf0(xq) = all_13_0_16)) % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (180) yields: % 49.75/17.69 | (181) aDimensionOf0(xp) = all_13_1_17 % 49.75/17.69 | (182) ~ iLess0(all_13_1_17, all_0_9_9) | ( ~ (all_13_0_16 = all_13_1_17) & aDimensionOf0(xq) = all_13_0_16) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (85) with xp, all_13_1_17, all_11_1_13 and discharging atoms aDimensionOf0(xp) = all_13_1_17, aDimensionOf0(xp) = all_11_1_13, yields: % 49.75/17.69 | (183) all_13_1_17 = all_11_1_13 % 49.75/17.69 | % 49.75/17.69 +-Applying beta-rule and splitting (182), into two cases. % 49.75/17.69 |-Branch one: % 49.75/17.69 | (184) ~ iLess0(all_13_1_17, all_0_9_9) % 49.75/17.69 | % 49.75/17.69 | From (183) and (184) follows: % 49.75/17.69 | (185) ~ iLess0(all_11_1_13, all_0_9_9) % 49.75/17.69 | % 49.75/17.69 | Using (170) and (185) yields: % 49.75/17.69 | (179) $false % 49.75/17.69 | % 49.75/17.69 |-The branch is then unsatisfiable % 49.75/17.69 |-Branch two: % 49.75/17.69 | (187) iLess0(all_13_1_17, all_0_9_9) % 49.75/17.69 | (188) ~ (all_13_0_16 = all_13_1_17) & aDimensionOf0(xq) = all_13_0_16 % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (188) yields: % 49.75/17.69 | (189) ~ (all_13_0_16 = all_13_1_17) % 49.75/17.69 | (190) aDimensionOf0(xq) = all_13_0_16 % 49.75/17.69 | % 49.75/17.69 | Equations (183) can reduce 189 to: % 49.75/17.69 | (191) ~ (all_13_0_16 = all_11_1_13) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (85) with xq, all_13_0_16, all_11_1_13 and discharging atoms aDimensionOf0(xq) = all_13_0_16, aDimensionOf0(xq) = all_11_1_13, yields: % 49.75/17.69 | (192) all_13_0_16 = all_11_1_13 % 49.75/17.69 | % 49.75/17.69 | Equations (192) can reduce 191 to: % 49.75/17.69 | (125) $false % 49.75/17.69 | % 49.75/17.69 |-The branch is then unsatisfiable % 49.75/17.69 |-Branch two: % 49.75/17.69 | (194) aDimensionOf0(xs) = all_11_0_12 & (all_11_0_12 = sz00 | ( ~ (all_11_0_12 = all_11_1_13) & aDimensionOf0(xt) = all_11_1_13)) % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (194) yields: % 49.75/17.69 | (195) aDimensionOf0(xs) = all_11_0_12 % 49.75/17.69 | (196) all_11_0_12 = sz00 | ( ~ (all_11_0_12 = all_11_1_13) & aDimensionOf0(xt) = all_11_1_13) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (85) with xs, all_11_0_12, all_0_9_9 and discharging atoms aDimensionOf0(xs) = all_11_0_12, aDimensionOf0(xs) = all_0_9_9, yields: % 49.75/17.69 | (197) all_11_0_12 = all_0_9_9 % 49.75/17.69 | % 49.75/17.69 +-Applying beta-rule and splitting (196), into two cases. % 49.75/17.69 |-Branch one: % 49.75/17.69 | (198) all_11_0_12 = sz00 % 49.75/17.69 | % 49.75/17.69 | Combining equations (197,198) yields a new equation: % 49.75/17.69 | (199) all_0_9_9 = sz00 % 49.75/17.69 | % 49.75/17.69 | Simplifying 199 yields: % 49.75/17.69 | (124) all_0_9_9 = sz00 % 49.75/17.69 | % 49.75/17.69 | Equations (124) can reduce 6 to: % 49.75/17.69 | (125) $false % 49.75/17.69 | % 49.75/17.69 |-The branch is then unsatisfiable % 49.75/17.69 |-Branch two: % 49.75/17.69 | (202) ~ (all_11_0_12 = sz00) % 49.75/17.69 | (203) ~ (all_11_0_12 = all_11_1_13) & aDimensionOf0(xt) = all_11_1_13 % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (203) yields: % 49.75/17.69 | (204) ~ (all_11_0_12 = all_11_1_13) % 49.75/17.69 | (205) aDimensionOf0(xt) = all_11_1_13 % 49.75/17.69 | % 49.75/17.69 | Equations (197) can reduce 204 to: % 49.75/17.69 | (206) ~ (all_11_1_13 = all_0_9_9) % 49.75/17.69 | % 49.75/17.69 | Simplifying 206 yields: % 49.75/17.69 | (207) ~ (all_11_1_13 = all_0_9_9) % 49.75/17.69 | % 49.75/17.69 | Instantiating formula (85) with xt, all_11_1_13, all_0_9_9 and discharging atoms aDimensionOf0(xt) = all_11_1_13, aDimensionOf0(xt) = all_0_9_9, yields: % 49.75/17.69 | (208) all_11_1_13 = all_0_9_9 % 49.75/17.69 | % 49.75/17.69 | Equations (208) can reduce 207 to: % 49.75/17.69 | (125) $false % 49.75/17.69 | % 49.75/17.69 |-The branch is then unsatisfiable % 49.75/17.69 |-Branch two: % 49.75/17.69 | (210) aDimensionOf0(xs) = all_14_0_18 & (all_14_0_18 = sz00 | ( ~ (all_14_0_18 = all_14_1_19) & aDimensionOf0(xs) = all_14_1_19)) % 49.75/17.69 | % 49.75/17.69 | Applying alpha-rule on (210) yields: % 49.75/17.69 | (211) aDimensionOf0(xs) = all_14_0_18 % 49.75/17.69 | (212) all_14_0_18 = sz00 | ( ~ (all_14_0_18 = all_14_1_19) & aDimensionOf0(xs) = all_14_1_19) % 49.75/17.69 | % 49.75/17.69 +-Applying beta-rule and splitting (107), into two cases. % 49.75/17.69 |-Branch one: % 49.75/17.69 | (132) all_9_0_11 = sz00 % 49.75/17.69 | % 50.16/17.70 | Combining equations (132,116) yields a new equation: % 50.16/17.70 | (124) all_0_9_9 = sz00 % 50.16/17.70 | % 50.16/17.70 | Equations (124) can reduce 6 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (135) ~ (all_9_0_11 = sz00) % 50.16/17.70 | (136) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) & ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp)) % 50.16/17.70 | % 50.16/17.70 | Equations (116) can reduce 135 to: % 50.16/17.70 | (6) ~ (all_0_9_9 = sz00) % 50.16/17.70 | % 50.16/17.70 +-Applying beta-rule and splitting (212), into two cases. % 50.16/17.70 |-Branch one: % 50.16/17.70 | (219) all_14_0_18 = sz00 % 50.16/17.70 | % 50.16/17.70 | From (219) and (211) follows: % 50.16/17.70 | (220) aDimensionOf0(xs) = sz00 % 50.16/17.70 | % 50.16/17.70 | Instantiating formula (85) with xs, sz00, all_0_9_9 and discharging atoms aDimensionOf0(xs) = all_0_9_9, aDimensionOf0(xs) = sz00, yields: % 50.16/17.70 | (124) all_0_9_9 = sz00 % 50.16/17.70 | % 50.16/17.70 | Equations (124) can reduce 6 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (223) ~ (all_14_0_18 = sz00) % 50.16/17.70 | (224) ~ (all_14_0_18 = all_14_1_19) & aDimensionOf0(xs) = all_14_1_19 % 50.16/17.70 | % 50.16/17.70 | Applying alpha-rule on (224) yields: % 50.16/17.70 | (225) ~ (all_14_0_18 = all_14_1_19) % 50.16/17.70 | (226) aDimensionOf0(xs) = all_14_1_19 % 50.16/17.70 | % 50.16/17.70 | Instantiating formula (85) with xs, all_14_0_18, all_0_9_9 and discharging atoms aDimensionOf0(xs) = all_14_0_18, aDimensionOf0(xs) = all_0_9_9, yields: % 50.16/17.70 | (227) all_14_0_18 = all_0_9_9 % 50.16/17.70 | % 50.16/17.70 | Instantiating formula (85) with xs, all_14_1_19, all_14_0_18 and discharging atoms aDimensionOf0(xs) = all_14_0_18, aDimensionOf0(xs) = all_14_1_19, yields: % 50.16/17.70 | (130) all_14_0_18 = all_14_1_19 % 50.16/17.70 | % 50.16/17.70 | Combining equations (130,227) yields a new equation: % 50.16/17.70 | (229) all_14_1_19 = all_0_9_9 % 50.16/17.70 | % 50.16/17.70 | Simplifying 229 yields: % 50.16/17.70 | (230) all_14_1_19 = all_0_9_9 % 50.16/17.70 | % 50.16/17.70 | Equations (227,230) can reduce 225 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (232) aDimensionOf0(xt) = all_12_0_14 & (all_12_0_14 = sz00 | ( ~ (all_12_0_14 = all_12_1_15) & aDimensionOf0(xs) = all_12_1_15)) % 50.16/17.70 | % 50.16/17.70 | Applying alpha-rule on (232) yields: % 50.16/17.70 | (233) aDimensionOf0(xt) = all_12_0_14 % 50.16/17.70 | (234) all_12_0_14 = sz00 | ( ~ (all_12_0_14 = all_12_1_15) & aDimensionOf0(xs) = all_12_1_15) % 50.16/17.70 | % 50.16/17.70 +-Applying beta-rule and splitting (114), into two cases. % 50.16/17.70 |-Branch one: % 50.16/17.70 | (123) all_18_0_26 = sz00 % 50.16/17.70 | % 50.16/17.70 | Combining equations (123,115) yields a new equation: % 50.16/17.70 | (124) all_0_9_9 = sz00 % 50.16/17.70 | % 50.16/17.70 | Equations (124) can reduce 6 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (126) ~ (all_18_0_26 = sz00) % 50.16/17.70 | (127) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xt, v1) = v2) | ~ (aDimensionOf0(xq) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xq, v1) = v2) & ! [v0] : ! [v1] : (v0 = xq | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xt, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_18_0_26) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | szszuzczcdt0(v0) = all_18_0_26) & ! [v0] : ( ~ (aDimensionOf0(xq) = v0) | aVector0(xq)) % 50.16/17.70 | % 50.16/17.70 | Equations (115) can reduce 126 to: % 50.16/17.70 | (6) ~ (all_0_9_9 = sz00) % 50.16/17.70 | % 50.16/17.70 +-Applying beta-rule and splitting (107), into two cases. % 50.16/17.70 |-Branch one: % 50.16/17.70 | (132) all_9_0_11 = sz00 % 50.16/17.70 | % 50.16/17.70 | Combining equations (132,116) yields a new equation: % 50.16/17.70 | (124) all_0_9_9 = sz00 % 50.16/17.70 | % 50.16/17.70 | Equations (124) can reduce 6 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (135) ~ (all_9_0_11 = sz00) % 50.16/17.70 | (136) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ (aDimensionOf0(xp) = v0) | ~ aNaturalNumber0(v1) | sdtlbdtrb0(xp, v1) = v2) & ! [v0] : ! [v1] : (v0 = xp | ~ (aDimensionOf0(v0) = v1) | ~ aVector0(v0) | ? [v2] : ? [v3] : ? [v4] : (( ~ (v4 = v3) & sdtlbdtrb0(v0, v2) = v3 & sdtlbdtrb0(xs, v2) = v4 & aNaturalNumber0(v2)) | ( ~ (v2 = all_9_0_11) & szszuzczcdt0(v1) = v2))) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | szszuzczcdt0(v0) = all_9_0_11) & ! [v0] : ( ~ (aDimensionOf0(xp) = v0) | aVector0(xp)) % 50.16/17.70 | % 50.16/17.70 | Equations (116) can reduce 135 to: % 50.16/17.70 | (6) ~ (all_0_9_9 = sz00) % 50.16/17.70 | % 50.16/17.70 | Instantiating formula (85) with xt, all_12_0_14, all_0_9_9 and discharging atoms aDimensionOf0(xt) = all_12_0_14, aDimensionOf0(xt) = all_0_9_9, yields: % 50.16/17.70 | (247) all_12_0_14 = all_0_9_9 % 50.16/17.70 | % 50.16/17.70 +-Applying beta-rule and splitting (234), into two cases. % 50.16/17.70 |-Branch one: % 50.16/17.70 | (248) all_12_0_14 = sz00 % 50.16/17.70 | % 50.16/17.70 | Combining equations (248,247) yields a new equation: % 50.16/17.70 | (124) all_0_9_9 = sz00 % 50.16/17.70 | % 50.16/17.70 | Equations (124) can reduce 6 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 |-Branch two: % 50.16/17.70 | (251) ~ (all_12_0_14 = sz00) % 50.16/17.70 | (252) ~ (all_12_0_14 = all_12_1_15) & aDimensionOf0(xs) = all_12_1_15 % 50.16/17.70 | % 50.16/17.70 | Applying alpha-rule on (252) yields: % 50.16/17.70 | (253) ~ (all_12_0_14 = all_12_1_15) % 50.16/17.70 | (254) aDimensionOf0(xs) = all_12_1_15 % 50.16/17.70 | % 50.16/17.70 | Equations (247) can reduce 253 to: % 50.16/17.70 | (255) ~ (all_12_1_15 = all_0_9_9) % 50.16/17.70 | % 50.16/17.70 | Simplifying 255 yields: % 50.16/17.70 | (256) ~ (all_12_1_15 = all_0_9_9) % 50.16/17.70 | % 50.16/17.70 | Instantiating formula (85) with xs, all_12_1_15, all_0_9_9 and discharging atoms aDimensionOf0(xs) = all_12_1_15, aDimensionOf0(xs) = all_0_9_9, yields: % 50.16/17.70 | (257) all_12_1_15 = all_0_9_9 % 50.16/17.70 | % 50.16/17.70 | Equations (257) can reduce 256 to: % 50.16/17.70 | (125) $false % 50.16/17.70 | % 50.16/17.70 |-The branch is then unsatisfiable % 50.16/17.70 % SZS output end Proof for theBenchmark % 50.16/17.70 % 50.16/17.70 17111ms %------------------------------------------------------------------------------