%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : RNG073+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n026.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 16.63s 6.39s % Output : Proof 30.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : RNG073+1 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon May 30 12:37:10 EDT 2022 % 0.13/0.34 % CPUTime : % 0.57/0.59 ____ _ % 0.57/0.59 ___ / __ \_____(_)___ ________ __________ % 0.57/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.59 % 0.57/0.59 A Theorem Prover for First-Order Logic % 0.57/0.59 (ePrincess v.1.0) % 0.57/0.59 % 0.57/0.59 (c) Philipp Rümmer, 2009-2015 % 0.57/0.59 (c) Peter Backeman, 2014-2015 % 0.57/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.59 Bug reports to peter@backeman.se % 0.57/0.59 % 0.57/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.59 % 0.57/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.75/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.96/1.00 Prover 0: Preprocessing ... % 3.92/1.53 Prover 0: Constructing countermodel ... % 14.81/5.93 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 14.81/6.03 Prover 1: Preprocessing ... % 15.70/6.18 Prover 1: Constructing countermodel ... % 16.63/6.38 Prover 1: proved (451ms) % 16.63/6.39 Prover 0: stopped % 16.63/6.39 % 16.63/6.39 No countermodel exists, formula is valid % 16.63/6.39 % SZS status Theorem for theBenchmark % 16.63/6.39 % 16.63/6.39 Generating proof ... found it (size 225) % 29.95/9.62 % 29.95/9.62 % SZS output start Proof for theBenchmark % 29.95/9.62 Assumed formulas after preprocessing and simplification: % 29.95/9.62 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v13 = 0) & ~ (v11 = v9) & ~ (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 & aVector0(xq) = 0 & aVector0(xp) = 0 & aVector0(xt) = 0 & aVector0(xs) = 0 & aDimensionOf0(xt) = v1 & aDimensionOf0(xs) = v1 & sdtlseqdt0(v12, v10) = 0 & sdtlseqdt0(v11, v9) = 0 & sdtlseqdt0(v10, v12) = 0 & sdtlseqdt0(v9, v11) = v13 & sdtlseqdt0(v5, v8) = 0 & sdtlseqdt0(v4, xN) = 0 & sdtlseqdt0(v2, v3) = 0 & sdtlseqdt0(sz0z00, v11) = 0 & sdtlseqdt0(sz0z00, v9) = 0 & smndt0(sz0z00) = v0 & sdtasdt0(v11, v11) = v12 & sdtasdt0(v9, v9) = v10 & sdtasdt0(xS, xS) = v7 & sdtasdt0(xP, xP) = v4 & sdtasdt0(xR, xS) = xN & sdtasdt0(xR, xR) = 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(v6, v7) = v8 & sdtpldt0(v4, v4) = v5 & sdtpldt0(xP, xP) = v9 & sdtpldt0(xR, xS) = v11 & aScalar0(xN) = 0 & aScalar0(xS) = 0 & aScalar0(xP) = 0 & aScalar0(xR) = 0 & aScalar0(xH) = 0 & aScalar0(xG) = 0 & aScalar0(xF) = 0 & aScalar0(xE) = 0 & aScalar0(xD) = 0 & aScalar0(xC) = 0 & aScalar0(xB) = 0 & aScalar0(xA) = 0 & aScalar0(sz0z00) = 0 & aNaturalNumber0(sz00) = 0 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (sdtasdt0(v15, v17) = v22) | ~ (sdtasdt0(v15, v16) = v21) | ~ (sdtasdt0(v14, v17) = v19) | ~ (sdtasdt0(v14, v16) = v18) | ~ (sdtpldt0(v21, v22) = v23) | ~ (sdtpldt0(v20, v23) = v24) | ~ (sdtpldt0(v18, v19) = v20) | ? [v25] : ? [v26] : ? [v27] : ? [v28] : ? [v29] : ? [v30] : ? [v31] : (sdtasdt0(v29, v30) = v31 & sdtpldt0(v16, v17) = v30 & sdtpldt0(v14, v15) = v29 & aScalar0(v17) = v28 & aScalar0(v16) = v27 & aScalar0(v15) = v26 & aScalar0(v14) = v25 & ( ~ (v28 = 0) | ~ (v27 = 0) | ~ (v26 = 0) | ~ (v25 = 0) | v31 = v24))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v16 = sz00 | ~ (sdtasasdt0(v17, v18) = v19) | ~ (sziznziztdt0(v15) = v18) | ~ (sziznziztdt0(v14) = v17) | ~ (sdtlbdtrb0(v15, v16) = v21) | ~ (sdtlbdtrb0(v14, v16) = v20) | ~ (aDimensionOf0(v15) = v16) | ~ (aDimensionOf0(v14) = v16) | ~ (sdtasdt0(v20, v21) = v22) | ~ (sdtpldt0(v19, v22) = v23) | ? [v24] : ? [v25] : ? [v26] : (sdtasasdt0(v14, v15) = v26 & aVector0(v15) = v25 & aVector0(v14) = v24 & ( ~ (v25 = 0) | ~ (v24 = 0) | v26 = v23))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (sdtasasdt0(v15, v15) = v19) | ~ (sdtasasdt0(v14, v15) = v16) | ~ (sdtasasdt0(v14, v14) = v18) | ~ (sdtlseqdt0(v17, v20) = v21) | ~ (sdtasdt0(v18, v19) = v20) | ~ (sdtasdt0(v16, v16) = v17) | ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : (aVector0(v15) = v23 & aVector0(v14) = v22 & aDimensionOf0(v15) = v25 & aDimensionOf0(v14) = v24 & iLess0(v24, v1) = v26 & ( ~ (v26 = 0) | ~ (v25 = v24) | ~ (v23 = 0) | ~ (v22 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = 0 | ~ (sdtlseqdt0(v18, v19) = v20) | ~ (sdtasdt0(v15, v17) = v19) | ~ (sdtasdt0(v14, v16) = v18) | ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : (sdtlseqdt0(v16, v17) = v27 & sdtlseqdt0(v14, v15) = v25 & sdtlseqdt0(sz0z00, v16) = v26 & aScalar0(v17) = v24 & aScalar0(v16) = v23 & aScalar0(v15) = v22 & aScalar0(v14) = v21 & ( ~ (v27 = 0) | ~ (v26 = 0) | ~ (v25 = 0) | ~ (v24 = 0) | ~ (v23 = 0) | ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = 0 | ~ (sdtlseqdt0(v18, v19) = v20) | ~ (sdtpldt0(v15, v17) = v19) | ~ (sdtpldt0(v14, v16) = v18) | ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : (sdtlseqdt0(v16, v17) = v26 & sdtlseqdt0(v14, v15) = v25 & aScalar0(v17) = v24 & aScalar0(v16) = v23 & aScalar0(v15) = v22 & aScalar0(v14) = v21 & ( ~ (v26 = 0) | ~ (v25 = 0) | ~ (v24 = 0) | ~ (v23 = 0) | ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtasdt0(v14, v16) = v18) | ~ (sdtasdt0(v14, v15) = v17) | ~ (sdtpldt0(v17, v18) = v19) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : ? [v28] : (sdtasdt0(v25, v16) = v26 & sdtasdt0(v15, v16) = v27 & sdtasdt0(v14, v23) = v24 & sdtpldt0(v18, v27) = v28 & sdtpldt0(v15, v16) = v23 & sdtpldt0(v14, v15) = v25 & aScalar0(v16) = v22 & aScalar0(v15) = v21 & aScalar0(v14) = v20 & ( ~ (v22 = 0) | ~ (v21 = 0) | ~ (v20 = 0) | (v28 = v26 & v24 = v19)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (smndt0(v15) = v17) | ~ (smndt0(v14) = v16) | ~ (sdtasdt0(v16, v17) = v18) | ? [v19] : ? [v20] : ? [v21] : (sdtasdt0(v14, v15) = v21 & aScalar0(v15) = v20 & aScalar0(v14) = v19 & ( ~ (v20 = 0) | ~ (v19 = 0) | v21 = v18))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v17, v16) = v18) | ~ (sdtpldt0(v14, v15) = v17) | ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : ? [v28] : ? [v29] : (sdtasdt0(v25, v16) = v26 & sdtasdt0(v15, v16) = v27 & sdtasdt0(v15, v14) = v29 & sdtasdt0(v14, v27) = v28 & sdtasdt0(v14, v15) = v25 & sdtpldt0(v15, v16) = v22 & sdtpldt0(v15, v14) = v24 & sdtpldt0(v14, v22) = v23 & aScalar0(v16) = v21 & aScalar0(v15) = v20 & aScalar0(v14) = v19 & ( ~ (v21 = 0) | ~ (v20 = 0) | ~ (v19 = 0) | (v29 = v25 & v28 = v26 & v24 = v17 & v23 = v18)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (sdtlseqdt0(v14, v16) = v17) | ~ (sdtlseqdt0(v14, v15) = 0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlseqdt0(v15, v16) = v21 & aScalar0(v16) = v20 & aScalar0(v15) = v19 & aScalar0(v14) = v18 & ( ~ (v21 = 0) | ~ (v20 = 0) | ~ (v19 = 0) | ~ (v18 = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (sdtasasdt0(v17, v16) = v15) | ~ (sdtasasdt0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (sdtlbdtrb0(v17, v16) = v15) | ~ (sdtlbdtrb0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (sdtlseqdt0(v17, v16) = v15) | ~ (sdtlseqdt0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (sdtasdt0(v17, v16) = v15) | ~ (sdtasdt0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (sdtpldt0(v17, v16) = v15) | ~ (sdtpldt0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (iLess0(v17, v16) = v15) | ~ (iLess0(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (sziznziztdt0(v15) = v17) | ~ (sziznziztdt0(v14) = v16) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : (aVector0(v15) = v19 & aVector0(v14) = v18 & aDimensionOf0(v17) = v23 & aDimensionOf0(v16) = v22 & aDimensionOf0(v15) = v21 & aDimensionOf0(v14) = v20 & ( ~ (v21 = v20) | ~ (v19 = 0) | ~ (v18 = 0) | v23 = v22 | v20 = sz00))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (smndt0(v14) = v16) | ~ (sdtasdt0(v16, v15) = v17) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : (smndt0(v22) = v23 & smndt0(v15) = v20 & sdtasdt0(v14, v20) = v21 & sdtasdt0(v14, v15) = v22 & aScalar0(v15) = v19 & aScalar0(v14) = v18 & ( ~ (v19 = 0) | ~ (v18 = 0) | (v23 = v17 & v21 = v17)))) & ! [v14] : ! [v15] : ! [v16] : (v16 = sz0z00 | ~ (sdtasasdt0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : (aVector0(v15) = v18 & aVector0(v14) = v17 & aDimensionOf0(v15) = v20 & aDimensionOf0(v14) = v19 & ( ~ (v20 = sz00) | ~ (v19 = sz00) | ~ (v18 = 0) | ~ (v17 = 0)))) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (sdtlseqdt0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : (sdtlseqdt0(v15, v14) = v19 & aScalar0(v15) = v18 & aScalar0(v14) = v17 & ( ~ (v18 = 0) | ~ (v17 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (iLess0(v14, v15) = v16) | ~ (szszuzczcdt0(v14) = v15) | ? [v17] : ( ~ (v17 = 0) & aNaturalNumber0(v14) = v17)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (sziznziztdt0(v16) = v15) | ~ (sziznziztdt0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (aVector0(v16) = v15) | ~ (aVector0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (aDimensionOf0(v16) = v15) | ~ (aDimensionOf0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (smndt0(v16) = v15) | ~ (smndt0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (aScalar0(v16) = v15) | ~ (aScalar0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (szszuzczcdt0(v16) = v15) | ~ (szszuzczcdt0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (szszuzczcdt0(v15) = v16) | ~ (szszuzczcdt0(v14) = v16) | ? [v17] : ? [v18] : (aNaturalNumber0(v15) = v18 & aNaturalNumber0(v14) = v17 & ( ~ (v18 = 0) | ~ (v17 = 0)))) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (aNaturalNumber0(v16) = v15) | ~ (aNaturalNumber0(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtasasdt0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : (aVector0(v15) = v18 & aVector0(v14) = v17 & aDimensionOf0(v15) = v20 & aDimensionOf0(v14) = v19 & aScalar0(v16) = v21 & ( ~ (v20 = v19) | ~ (v18 = 0) | ~ (v17 = 0) | v21 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtlbdtrb0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : (aVector0(v14) = v17 & aScalar0(v16) = v19 & aNaturalNumber0(v15) = v18 & ( ~ (v18 = 0) | ~ (v17 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (smndt0(v14) = v15) | ~ (sdtpldt0(v15, v14) = v16) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : (smndt0(v15) = v23 & sdtasdt0(v14, sz0z00) = v20 & sdtasdt0(sz0z00, v14) = v21 & sdtpldt0(v14, v15) = v22 & sdtpldt0(v14, sz0z00) = v18 & sdtpldt0(sz0z00, v14) = v19 & aScalar0(v14) = v17 & ( ~ (v17 = 0) | (v23 = v14 & v22 = sz0z00 & v21 = sz0z00 & v20 = sz0z00 & v19 = v14 & v18 = v14 & v16 = sz0z00 & v0 = sz0z00)))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtasdt0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : (aScalar0(v16) = v19 & aScalar0(v15) = v18 & aScalar0(v14) = v17 & ( ~ (v18 = 0) | ~ (v17 = 0) | v19 = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (sdtpldt0(v14, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : (aScalar0(v16) = v19 & aScalar0(v15) = v18 & aScalar0(v14) = v17 & ( ~ (v18 = 0) | ~ (v17 = 0) | v19 = 0))) & ! [v14] : ! [v15] : (v15 = v14 | ~ (sdtlseqdt0(v14, v15) = 0) | ? [v16] : ? [v17] : ? [v18] : (sdtlseqdt0(v15, v14) = v18 & aScalar0(v15) = v17 & aScalar0(v14) = v16 & ( ~ (v18 = 0) | ~ (v17 = 0) | ~ (v16 = 0)))) & ! [v14] : ! [v15] : (v15 = v14 | ~ (sdtlseqdt0(sz0z00, v15) = 0) | ~ (sdtlseqdt0(sz0z00, v14) = 0) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : (sdtasdt0(v15, v15) = v19 & sdtasdt0(v14, v14) = v18 & aScalar0(v15) = v17 & aScalar0(v14) = v16 & ( ~ (v19 = v18) | ~ (v17 = 0) | ~ (v16 = 0)))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (sdtlseqdt0(v14, v14) = v15) | ? [v16] : ( ~ (v16 = 0) & aScalar0(v14) = v16)) & ! [v14] : ! [v15] : ( ~ (sdtasasdt0(v14, v14) = v15) | ? [v16] : ? [v17] : (aVector0(v14) = v16 & sdtlseqdt0(sz0z00, v15) = v17 & ( ~ (v16 = 0) | v17 = 0))) & ! [v14] : ! [v15] : ( ~ (sziznziztdt0(v14) = v15) | ? [v16] : ? [v17] : (aVector0(v14) = v16 & aDimensionOf0(v14) = v17 & ( ~ (v16 = 0) | v17 = sz00 | ( ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtlbdtrb0(v14, v19) = v20) | ~ (aVector0(v15) = v18) | ? [v21] : ? [v22] : (sdtlbdtrb0(v15, v19) = v22 & aNaturalNumber0(v19) = v21 & ( ~ (v21 = 0) | v22 = v20))) & ! [v18] : (v18 = v15 | ~ (aVector0(v18) = 0) | ? [v19] : ? [v20] : ? [v21] : ? [v22] : ((v20 = 0 & ~ (v22 = v21) & sdtlbdtrb0(v18, v19) = v21 & sdtlbdtrb0(v14, v19) = v22 & aNaturalNumber0(v19) = 0) | ( ~ (v20 = v17) & aDimensionOf0(v18) = v19 & szszuzczcdt0(v19) = v20))) & ! [v18] : (v18 = 0 | ~ (aVector0(v15) = v18)) & ! [v18] : ( ~ (aVector0(v15) = v18) | ? [v19] : (aDimensionOf0(v15) = v19 & szszuzczcdt0(v19) = v17)))))) & ! [v14] : ! [v15] : ( ~ (sdtlseqdt0(sz0z00, v15) = 0) | ~ (sdtlseqdt0(sz0z00, v14) = 0) | ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlseqdt0(sz0z00, v20) = v21 & sdtlseqdt0(sz0z00, v18) = v19 & sdtasdt0(v14, v15) = v20 & sdtpldt0(v14, v15) = v18 & aScalar0(v15) = v17 & aScalar0(v14) = v16 & ( ~ (v17 = 0) | ~ (v16 = 0) | (v21 = 0 & v19 = 0)))) & ! [v14] : ! [v15] : ( ~ (smndt0(v14) = v15) | ? [v16] : ? [v17] : (aScalar0(v15) = v17 & aScalar0(v14) = v16 & ( ~ (v16 = 0) | v17 = 0))) & ! [v14] : ! [v15] : ( ~ (sdtasdt0(v14, v14) = v15) | ? [v16] : ? [v17] : (sdtlseqdt0(sz0z00, v15) = v17 & aScalar0(v14) = v16 & ( ~ (v16 = 0) | v17 = 0))) & ! [v14] : ! [v15] : ( ~ (szszuzczcdt0(v14) = v15) | ? [v16] : ? [v17] : (aNaturalNumber0(v15) = v17 & aNaturalNumber0(v14) = v16 & ( ~ (v16 = 0) | (v17 = 0 & ~ (v15 = sz00))))) & ! [v14] : (v14 = sz00 | ~ (aNaturalNumber0(v14) = 0) | ? [v15] : (szszuzczcdt0(v15) = v14 & aNaturalNumber0(v15) = 0)) & ! [v14] : ( ~ (aVector0(v14) = 0) | ? [v15] : (aDimensionOf0(v14) = v15 & aNaturalNumber0(v15) = 0))) % 29.95/9.67 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 29.95/9.67 | (1) ~ (all_0_0_0 = 0) & ~ (all_0_2_2 = all_0_4_4) & ~ (all_0_12_12 = sz00) & sdtasasdt0(xq, xq) = xD & sdtasasdt0(xp, xq) = xE & sdtasasdt0(xp, xp) = xC & sziznziztdt0(xt) = xq & sziznziztdt0(xs) = xp & sdtlbdtrb0(xt, all_0_12_12) = xB & sdtlbdtrb0(xs, all_0_12_12) = xA & aVector0(xq) = 0 & aVector0(xp) = 0 & aVector0(xt) = 0 & aVector0(xs) = 0 & aDimensionOf0(xt) = all_0_12_12 & aDimensionOf0(xs) = all_0_12_12 & sdtlseqdt0(all_0_1_1, all_0_3_3) = 0 & sdtlseqdt0(all_0_2_2, all_0_4_4) = 0 & sdtlseqdt0(all_0_3_3, all_0_1_1) = 0 & sdtlseqdt0(all_0_4_4, all_0_2_2) = all_0_0_0 & sdtlseqdt0(all_0_8_8, all_0_5_5) = 0 & sdtlseqdt0(all_0_9_9, xN) = 0 & sdtlseqdt0(all_0_11_11, all_0_10_10) = 0 & sdtlseqdt0(sz0z00, all_0_2_2) = 0 & sdtlseqdt0(sz0z00, all_0_4_4) = 0 & smndt0(sz0z00) = all_0_13_13 & sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 & sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3 & sdtasdt0(xS, xS) = all_0_6_6 & sdtasdt0(xP, xP) = all_0_9_9 & sdtasdt0(xR, xS) = xN & sdtasdt0(xR, xR) = all_0_7_7 & sdtasdt0(xF, xD) = xS & sdtasdt0(xE, xH) = xP & sdtasdt0(xE, xE) = all_0_11_11 & sdtasdt0(xC, xG) = xR & sdtasdt0(xC, xD) = all_0_10_10 & sdtasdt0(xB, xB) = xG & sdtasdt0(xA, xB) = xH & sdtasdt0(xA, xA) = xF & sdtpldt0(all_0_7_7, all_0_6_6) = all_0_5_5 & sdtpldt0(all_0_9_9, all_0_9_9) = all_0_8_8 & sdtpldt0(xP, xP) = all_0_4_4 & sdtpldt0(xR, xS) = all_0_2_2 & aScalar0(xN) = 0 & aScalar0(xS) = 0 & aScalar0(xP) = 0 & aScalar0(xR) = 0 & aScalar0(xH) = 0 & aScalar0(xG) = 0 & aScalar0(xF) = 0 & aScalar0(xE) = 0 & aScalar0(xD) = 0 & aScalar0(xC) = 0 & aScalar0(xB) = 0 & aScalar0(xA) = 0 & aScalar0(sz0z00) = 0 & aNaturalNumber0(sz00) = 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) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (sdtasdt0(v15, v16) = v17 & sdtpldt0(v2, v3) = v16 & sdtpldt0(v0, v1) = v15 & aScalar0(v3) = v14 & aScalar0(v2) = v13 & aScalar0(v1) = v12 & aScalar0(v0) = v11 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | v17 = v10))) & ! [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) | ? [v10] : ? [v11] : ? [v12] : (sdtasasdt0(v0, v1) = v12 & aVector0(v1) = v11 & aVector0(v0) = v10 & ( ~ (v11 = 0) | ~ (v10 = 0) | v12 = v9))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtasasdt0(v1, v1) = v5) | ~ (sdtasasdt0(v0, v1) = v2) | ~ (sdtasasdt0(v0, v0) = v4) | ~ (sdtlseqdt0(v3, v6) = v7) | ~ (sdtasdt0(v4, v5) = v6) | ~ (sdtasdt0(v2, v2) = v3) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (aVector0(v1) = v9 & aVector0(v0) = v8 & aDimensionOf0(v1) = v11 & aDimensionOf0(v0) = v10 & iLess0(v10, all_0_12_12) = v12 & ( ~ (v12 = 0) | ~ (v11 = v10) | ~ (v9 = 0) | ~ (v8 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sdtlseqdt0(v2, v3) = v13 & sdtlseqdt0(v0, v1) = v11 & sdtlseqdt0(sz0z00, v2) = v12 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtlseqdt0(v2, v3) = v12 & sdtlseqdt0(v0, v1) = v11 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v11, v2) = v12 & sdtasdt0(v1, v2) = v13 & sdtasdt0(v0, v9) = v10 & sdtpldt0(v4, v13) = v14 & sdtpldt0(v1, v2) = v9 & sdtpldt0(v0, v1) = v11 & aScalar0(v2) = v8 & aScalar0(v1) = v7 & aScalar0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v14 = v12 & v10 = v5)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (sdtasdt0(v0, v1) = v7 & aScalar0(v1) = v6 & aScalar0(v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | v7 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v11, v2) = v12 & sdtasdt0(v1, v2) = v13 & sdtasdt0(v1, v0) = v15 & sdtasdt0(v0, v13) = v14 & sdtasdt0(v0, v1) = v11 & sdtpldt0(v1, v2) = v8 & sdtpldt0(v1, v0) = v10 & sdtpldt0(v0, v8) = v9 & aScalar0(v2) = v7 & aScalar0(v1) = v6 & aScalar0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v15 = v11 & v14 = v12 & v10 = v3 & v9 = v4)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(v1, v2) = v7 & aScalar0(v2) = v6 & aScalar0(v1) = v5 & aScalar0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [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 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(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] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (aVector0(v1) = v5 & aVector0(v0) = v4 & aDimensionOf0(v3) = v9 & aDimensionOf0(v2) = v8 & aDimensionOf0(v1) = v7 & aDimensionOf0(v0) = v6 & ( ~ (v7 = v6) | ~ (v5 = 0) | ~ (v4 = 0) | v9 = v8 | v6 = sz00))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (smndt0(v8) = v9 & smndt0(v1) = v6 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & aScalar0(v1) = v5 & aScalar0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v9 = v3 & v7 = v3)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (sdtasasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (aVector0(v1) = v4 & aVector0(v0) = v3 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & ( ~ (v6 = sz00) | ~ (v5 = sz00) | ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v1, v0) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (iLess0(v0, v1) = v2) | ~ (szszuzczcdt0(v0) = v1) | ? [v3] : ( ~ (v3 = 0) & aNaturalNumber0(v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aVector0(v2) = v1) | ~ (aVector0(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 | ~ (aScalar0(v2) = v1) | ~ (aScalar0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ? [v3] : ? [v4] : (aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (aVector0(v1) = v4 & aVector0(v0) = v3 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & aScalar0(v2) = v7 & ( ~ (v6 = v5) | ~ (v4 = 0) | ~ (v3 = 0) | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aVector0(v0) = v3 & aScalar0(v2) = v5 & aNaturalNumber0(v1) = v4 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (smndt0(v1) = v9 & sdtasdt0(v0, sz0z00) = v6 & sdtasdt0(sz0z00, v0) = v7 & sdtpldt0(v0, v1) = v8 & sdtpldt0(v0, sz0z00) = v4 & sdtpldt0(sz0z00, v0) = v5 & aScalar0(v0) = v3 & ( ~ (v3 = 0) | (v9 = v0 & v8 = sz0z00 & v7 = sz0z00 & v6 = sz0z00 & v5 = v0 & v4 = v0 & v2 = sz0z00 & all_0_13_13 = sz0z00)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v1, v0) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(sz0z00, v1) = 0) | ~ (sdtlseqdt0(sz0z00, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtasdt0(v1, v1) = v5 & sdtasdt0(v0, v0) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v5 = v4) | ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aScalar0(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ? [v2] : ? [v3] : (aVector0(v0) = v2 & sdtlseqdt0(sz0z00, v1) = v3 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ? [v2] : ? [v3] : (aVector0(v0) = v2 & aDimensionOf0(v0) = v3 & ( ~ (v2 = 0) | v3 = sz00 | ( ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlbdtrb0(v0, v5) = v6) | ~ (aVector0(v1) = v4) | ? [v7] : ? [v8] : (sdtlbdtrb0(v1, v5) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v7 = 0) | v8 = v6))) & ! [v4] : (v4 = v1 | ~ (aVector0(v4) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v6 = 0 & ~ (v8 = v7) & sdtlbdtrb0(v4, v5) = v7 & sdtlbdtrb0(v0, v5) = v8 & aNaturalNumber0(v5) = 0) | ( ~ (v6 = v3) & aDimensionOf0(v4) = v5 & szszuzczcdt0(v5) = v6))) & ! [v4] : (v4 = 0 | ~ (aVector0(v1) = v4)) & ! [v4] : ( ~ (aVector0(v1) = v4) | ? [v5] : (aDimensionOf0(v1) = v5 & szszuzczcdt0(v5) = v3)))))) & ! [v0] : ! [v1] : ( ~ (sdtlseqdt0(sz0z00, v1) = 0) | ~ (sdtlseqdt0(sz0z00, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(sz0z00, v6) = v7 & sdtlseqdt0(sz0z00, v4) = v5 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v0, v1) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v7 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ? [v2] : ? [v3] : (aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ? [v2] : ? [v3] : (sdtlseqdt0(sz0z00, v1) = v3 & aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = sz00))))) & ! [v0] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1) = 0)) & ! [v0] : ( ~ (aVector0(v0) = 0) | ? [v1] : (aDimensionOf0(v0) = v1 & aNaturalNumber0(v1) = 0)) % 30.27/9.69 | % 30.27/9.69 | Applying alpha-rule on (1) yields: % 30.27/9.69 | (2) ~ (all_0_12_12 = sz00) % 30.27/9.69 | (3) sdtlbdtrb0(xs, all_0_12_12) = xA % 30.27/9.69 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) % 30.27/9.69 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 30.27/9.69 | (6) sdtpldt0(xR, xS) = all_0_2_2 % 30.27/9.69 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 30.27/9.69 | (8) sdtpldt0(all_0_9_9, all_0_9_9) = all_0_8_8 % 30.27/9.69 | (9) sdtpldt0(all_0_7_7, all_0_6_6) = all_0_5_5 % 30.27/9.69 | (10) aNaturalNumber0(sz00) = 0 % 30.27/9.69 | (11) aScalar0(xS) = 0 % 30.27/9.69 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) % 30.27/9.69 | (13) ~ (all_0_2_2 = all_0_4_4) % 30.27/9.69 | (14) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = sz00))))) % 30.27/9.69 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aScalar0(v2) = v1) | ~ (aScalar0(v2) = v0)) % 30.27/9.69 | (16) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(sz0z00, v1) = 0) | ~ (sdtlseqdt0(sz0z00, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtasdt0(v1, v1) = v5 & sdtasdt0(v0, v0) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v5 = v4) | ~ (v3 = 0) | ~ (v2 = 0)))) % 30.27/9.69 | (17) aScalar0(xN) = 0 % 30.27/9.69 | (18) sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3 % 30.27/9.69 | (19) sdtasdt0(xS, xS) = all_0_6_6 % 30.27/9.69 | (20) aVector0(xs) = 0 % 30.27/9.69 | (21) aScalar0(xD) = 0 % 30.27/9.69 | (22) ! [v0] : ! [v1] : ( ~ (sdtlseqdt0(sz0z00, v1) = 0) | ~ (sdtlseqdt0(sz0z00, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(sz0z00, v6) = v7 & sdtlseqdt0(sz0z00, v4) = v5 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v0, v1) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v7 = 0 & v5 = 0)))) % 30.27/9.70 | (23) sdtpldt0(xP, xP) = all_0_4_4 % 30.27/9.70 | (24) sdtasdt0(xC, xD) = all_0_10_10 % 30.27/9.70 | (25) sdtlseqdt0(sz0z00, all_0_4_4) = 0 % 30.27/9.70 | (26) aScalar0(xF) = 0 % 30.27/9.70 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) % 30.27/9.70 | (28) sdtlbdtrb0(xt, all_0_12_12) = xB % 30.27/9.70 | (29) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v0) = v1) | ? [v2] : ? [v3] : (sdtlseqdt0(sz0z00, v1) = v3 & aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 30.27/9.70 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 30.27/9.70 | (31) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v1, v0) = v4 & aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) % 30.27/9.70 | (32) aScalar0(xA) = 0 % 30.27/9.70 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ? [v3] : ? [v4] : (aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 30.27/9.70 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 30.27/9.70 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(v1, v2) = v7 & aScalar0(v2) = v6 & aScalar0(v1) = v5 & aScalar0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 30.27/9.70 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (sdtasdt0(v0, v1) = v7 & aScalar0(v1) = v6 & aScalar0(v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | v7 = v4))) % 30.27/9.70 | (37) sdtasdt0(xC, xG) = xR % 30.27/9.70 | (38) ! [v0] : ( ~ (aVector0(v0) = 0) | ? [v1] : (aDimensionOf0(v0) = v1 & aNaturalNumber0(v1) = 0)) % 30.27/9.70 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 30.27/9.70 | (40) sdtlseqdt0(sz0z00, all_0_2_2) = 0 % 30.27/9.70 | (41) ~ (all_0_0_0 = 0) % 30.27/9.70 | (42) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 30.27/9.70 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (aVector0(v1) = v4 & aVector0(v0) = v3 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & aScalar0(v2) = v7 & ( ~ (v6 = v5) | ~ (v4 = 0) | ~ (v3 = 0) | v7 = 0))) % 30.27/9.70 | (44) sdtasdt0(xB, xB) = xG % 30.27/9.70 | (45) sdtlseqdt0(all_0_8_8, all_0_5_5) = 0 % 30.27/9.70 | (46) ! [v0] : ! [v1] : ( ~ (sziznziztdt0(v0) = v1) | ? [v2] : ? [v3] : (aVector0(v0) = v2 & aDimensionOf0(v0) = v3 & ( ~ (v2 = 0) | v3 = sz00 | ( ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlbdtrb0(v0, v5) = v6) | ~ (aVector0(v1) = v4) | ? [v7] : ? [v8] : (sdtlbdtrb0(v1, v5) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v7 = 0) | v8 = v6))) & ! [v4] : (v4 = v1 | ~ (aVector0(v4) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ((v6 = 0 & ~ (v8 = v7) & sdtlbdtrb0(v4, v5) = v7 & sdtlbdtrb0(v0, v5) = v8 & aNaturalNumber0(v5) = 0) | ( ~ (v6 = v3) & aDimensionOf0(v4) = v5 & szszuzczcdt0(v5) = v6))) & ! [v4] : (v4 = 0 | ~ (aVector0(v1) = v4)) & ! [v4] : ( ~ (aVector0(v1) = v4) | ? [v5] : (aDimensionOf0(v1) = v5 & szszuzczcdt0(v5) = v3)))))) % 30.27/9.70 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 30.27/9.70 | (48) sdtasasdt0(xp, xq) = xE % 30.27/9.70 | (49) ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aScalar0(v0) = v2)) % 30.27/9.70 | (50) aScalar0(xG) = 0 % 30.27/9.70 | (51) sdtasdt0(xE, xH) = xP % 30.27/9.70 | (52) aVector0(xq) = 0 % 30.27/9.70 | (53) sdtlseqdt0(all_0_4_4, all_0_2_2) = all_0_0_0 % 30.27/9.70 | (54) sdtasdt0(xR, xR) = all_0_7_7 % 30.27/9.70 | (55) sdtasdt0(xR, xS) = xN % 30.27/9.70 | (56) sdtasdt0(xA, xA) = xF % 30.27/9.70 | (57) sziznziztdt0(xs) = xp % 30.27/9.70 | (58) sdtasdt0(xE, xE) = all_0_11_11 % 30.27/9.70 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtlseqdt0(v2, v3) = v12 & sdtlseqdt0(v0, v1) = v11 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) % 30.27/9.70 | (60) aScalar0(xC) = 0 % 30.27/9.70 | (61) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 % 30.27/9.70 | (62) aScalar0(xP) = 0 % 30.27/9.70 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aVector0(v2) = v1) | ~ (aVector0(v2) = v0)) % 30.27/9.70 | (64) sdtlseqdt0(all_0_1_1, all_0_3_3) = 0 % 30.27/9.70 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 30.27/9.70 | (66) sdtlseqdt0(all_0_3_3, all_0_1_1) = 0 % 30.27/9.70 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v11, v2) = v12 & sdtasdt0(v1, v2) = v13 & sdtasdt0(v0, v9) = v10 & sdtpldt0(v4, v13) = v14 & sdtpldt0(v1, v2) = v9 & sdtpldt0(v0, v1) = v11 & aScalar0(v2) = v8 & aScalar0(v1) = v7 & aScalar0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v14 = v12 & v10 = v5)))) % 30.27/9.71 | (68) ! [v0] : ! [v1] : ( ~ (sdtasasdt0(v0, v0) = v1) | ? [v2] : ? [v3] : (aVector0(v0) = v2 & sdtlseqdt0(sz0z00, v1) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 30.27/9.71 | (69) sdtasasdt0(xq, xq) = xD % 30.27/9.71 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (sdtasdt0(v11, v2) = v12 & sdtasdt0(v1, v2) = v13 & sdtasdt0(v1, v0) = v15 & sdtasdt0(v0, v13) = v14 & sdtasdt0(v0, v1) = v11 & sdtpldt0(v1, v2) = v8 & sdtpldt0(v1, v0) = v10 & sdtpldt0(v0, v8) = v9 & aScalar0(v2) = v7 & aScalar0(v1) = v6 & aScalar0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v15 = v11 & v14 = v12 & v10 = v3 & v9 = v4)))) % 30.27/9.71 | (71) aVector0(xt) = 0 % 30.27/9.71 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtasasdt0(v1, v1) = v5) | ~ (sdtasasdt0(v0, v1) = v2) | ~ (sdtasasdt0(v0, v0) = v4) | ~ (sdtlseqdt0(v3, v6) = v7) | ~ (sdtasdt0(v4, v5) = v6) | ~ (sdtasdt0(v2, v2) = v3) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (aVector0(v1) = v9 & aVector0(v0) = v8 & aDimensionOf0(v1) = v11 & aDimensionOf0(v0) = v10 & iLess0(v10, all_0_12_12) = v12 & ( ~ (v12 = 0) | ~ (v11 = v10) | ~ (v9 = 0) | ~ (v8 = 0)))) % 30.27/9.71 | (73) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ? [v2] : ? [v3] : (aScalar0(v1) = v3 & aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 30.27/9.71 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aVector0(v0) = v3 & aScalar0(v2) = v5 & aNaturalNumber0(v1) = v4 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 30.27/9.71 | (75) sdtlseqdt0(all_0_11_11, all_0_10_10) = 0 % 30.27/9.71 | (76) sdtlseqdt0(all_0_9_9, xN) = 0 % 30.27/9.71 | (77) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) % 30.27/9.71 | (78) aScalar0(xH) = 0 % 30.27/9.71 | (79) aDimensionOf0(xs) = all_0_12_12 % 30.27/9.71 | (80) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v1, v0) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 30.27/9.71 | (81) aScalar0(sz0z00) = 0 % 30.27/9.71 | (82) sdtasdt0(xA, xB) = xH % 30.27/9.71 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (smndt0(v8) = v9 & smndt0(v1) = v6 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & aScalar0(v1) = v5 & aScalar0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v9 = v3 & v7 = v3)))) % 30.27/9.71 | (84) ! [v0] : ! [v1] : ! [v2] : (v2 = sz0z00 | ~ (sdtasasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (aVector0(v1) = v4 & aVector0(v0) = v3 & aDimensionOf0(v1) = v6 & aDimensionOf0(v0) = v5 & ( ~ (v6 = sz00) | ~ (v5 = sz00) | ~ (v4 = 0) | ~ (v3 = 0)))) % 30.27/9.71 | (85) ! [v0] : ! [v1] : ! [v2] : ( ~ (smndt0(v0) = v1) | ~ (sdtpldt0(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (smndt0(v1) = v9 & sdtasdt0(v0, sz0z00) = v6 & sdtasdt0(sz0z00, v0) = v7 & sdtpldt0(v0, v1) = v8 & sdtpldt0(v0, sz0z00) = v4 & sdtpldt0(sz0z00, v0) = v5 & aScalar0(v0) = v3 & ( ~ (v3 = 0) | (v9 = v0 & v8 = sz0z00 & v7 = sz0z00 & v6 = sz0z00 & v5 = v0 & v4 = v0 & v2 = sz0z00 & all_0_13_13 = sz0z00)))) % 30.27/9.71 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sdtlseqdt0(v2, v3) = v13 & sdtlseqdt0(v0, v1) = v11 & sdtlseqdt0(sz0z00, v2) = v12 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) % 30.27/9.71 | (87) aVector0(xp) = 0 % 30.27/9.71 | (88) sdtlseqdt0(all_0_2_2, all_0_4_4) = 0 % 30.27/9.71 | (89) sziznziztdt0(xt) = xq % 30.27/9.71 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (aVector0(v1) = v5 & aVector0(v0) = v4 & aDimensionOf0(v3) = v9 & aDimensionOf0(v2) = v8 & aDimensionOf0(v1) = v7 & aDimensionOf0(v0) = v6 & ( ~ (v7 = v6) | ~ (v5 = 0) | ~ (v4 = 0) | v9 = v8 | v6 = sz00))) % 30.27/9.71 | (91) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (iLess0(v0, v1) = v2) | ~ (szszuzczcdt0(v0) = v1) | ? [v3] : ( ~ (v3 = 0) & aNaturalNumber0(v0) = v3)) % 30.27/9.71 | (92) aScalar0(xE) = 0 % 30.27/9.71 | (93) ! [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) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (sdtasdt0(v15, v16) = v17 & sdtpldt0(v2, v3) = v16 & sdtpldt0(v0, v1) = v15 & aScalar0(v3) = v14 & aScalar0(v2) = v13 & aScalar0(v1) = v12 & aScalar0(v0) = v11 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | v17 = v10))) % 30.27/9.71 | (94) sdtasasdt0(xp, xp) = xC % 30.27/9.71 | (95) ! [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) | ? [v10] : ? [v11] : ? [v12] : (sdtasasdt0(v0, v1) = v12 & aVector0(v1) = v11 & aVector0(v0) = v10 & ( ~ (v11 = 0) | ~ (v10 = 0) | v12 = v9))) % 30.27/9.72 | (96) aScalar0(xR) = 0 % 30.27/9.72 | (97) aScalar0(xB) = 0 % 30.27/9.72 | (98) ! [v0] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aNaturalNumber0(v1) = 0)) % 30.27/9.72 | (99) aDimensionOf0(xt) = all_0_12_12 % 30.27/9.72 | (100) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 30.27/9.72 | (101) smndt0(sz0z00) = all_0_13_13 % 30.27/9.72 | (102) sdtasdt0(xF, xD) = xS % 30.27/9.72 | (103) sdtasdt0(xP, xP) = all_0_9_9 % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (31) with all_0_1_1, all_0_3_3 and discharging atoms sdtlseqdt0(all_0_3_3, all_0_1_1) = 0, yields: % 30.27/9.72 | (104) all_0_1_1 = all_0_3_3 | ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_0_1_1, all_0_3_3) = v2 & aScalar0(all_0_1_1) = v1 & aScalar0(all_0_3_3) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (22) with all_0_2_2, all_0_2_2 and discharging atoms sdtlseqdt0(sz0z00, all_0_2_2) = 0, yields: % 30.27/9.72 | (105) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(sz0z00, v4) = v5 & sdtlseqdt0(sz0z00, v2) = v3 & sdtasdt0(all_0_2_2, all_0_2_2) = v4 & sdtpldt0(all_0_2_2, all_0_2_2) = v2 & aScalar0(all_0_2_2) = v1 & aScalar0(all_0_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v5 = 0 & v3 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (16) with all_0_2_2, all_0_4_4 and discharging atoms sdtlseqdt0(sz0z00, all_0_2_2) = 0, sdtlseqdt0(sz0z00, all_0_4_4) = 0, yields: % 30.27/9.72 | (106) all_0_2_2 = all_0_4_4 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(all_0_2_2, all_0_2_2) = v3 & sdtasdt0(all_0_4_4, all_0_4_4) = v2 & aScalar0(all_0_2_2) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v3 = v2) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (22) with all_0_4_4, all_0_2_2 and discharging atoms sdtlseqdt0(sz0z00, all_0_2_2) = 0, sdtlseqdt0(sz0z00, all_0_4_4) = 0, yields: % 30.27/9.72 | (107) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(sz0z00, v4) = v5 & sdtlseqdt0(sz0z00, v2) = v3 & sdtasdt0(all_0_2_2, all_0_4_4) = v4 & sdtpldt0(all_0_2_2, all_0_4_4) = v2 & aScalar0(all_0_2_2) = v0 & aScalar0(all_0_4_4) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v5 = 0 & v3 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (22) with all_0_2_2, all_0_4_4 and discharging atoms sdtlseqdt0(sz0z00, all_0_2_2) = 0, sdtlseqdt0(sz0z00, all_0_4_4) = 0, yields: % 30.27/9.72 | (108) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(sz0z00, v4) = v5 & sdtlseqdt0(sz0z00, v2) = v3 & sdtasdt0(all_0_4_4, all_0_2_2) = v4 & sdtpldt0(all_0_4_4, all_0_2_2) = v2 & aScalar0(all_0_2_2) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v5 = 0 & v3 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (22) with all_0_4_4, all_0_4_4 and discharging atoms sdtlseqdt0(sz0z00, all_0_4_4) = 0, yields: % 30.27/9.72 | (109) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(sz0z00, v4) = v5 & sdtlseqdt0(sz0z00, v2) = v3 & sdtasdt0(all_0_4_4, all_0_4_4) = v4 & sdtpldt0(all_0_4_4, all_0_4_4) = v2 & aScalar0(all_0_4_4) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v5 = 0 & v3 = 0))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (29) with all_0_1_1, all_0_2_2 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 30.27/9.72 | (110) ? [v0] : ? [v1] : (sdtlseqdt0(sz0z00, all_0_1_1) = v1 & aScalar0(all_0_2_2) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (42) 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, yields: % 30.27/9.72 | (111) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_1_1) = v2 & aScalar0(all_0_2_2) = v1 & aScalar0(all_0_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (29) with all_0_3_3, all_0_4_4 and discharging atoms sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3, yields: % 30.27/9.72 | (112) ? [v0] : ? [v1] : (sdtlseqdt0(sz0z00, all_0_3_3) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (42) with all_0_3_3, all_0_4_4, all_0_4_4 and discharging atoms sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3, yields: % 30.27/9.72 | (113) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_3_3) = v2 & aScalar0(all_0_4_4) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (29) with all_0_6_6, xS and discharging atoms sdtasdt0(xS, xS) = all_0_6_6, yields: % 30.27/9.72 | (114) ? [v0] : ? [v1] : (sdtlseqdt0(sz0z00, all_0_6_6) = v1 & aScalar0(xS) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (42) with all_0_6_6, xS, xS and discharging atoms sdtasdt0(xS, xS) = all_0_6_6, yields: % 30.27/9.72 | (115) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_6_6) = v2 & aScalar0(xS) = v1 & aScalar0(xS) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (29) with all_0_9_9, xP and discharging atoms sdtasdt0(xP, xP) = all_0_9_9, yields: % 30.27/9.72 | (116) ? [v0] : ? [v1] : (sdtlseqdt0(sz0z00, all_0_9_9) = v1 & aScalar0(xP) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (42) with all_0_9_9, xP, xP and discharging atoms sdtasdt0(xP, xP) = all_0_9_9, yields: % 30.27/9.72 | (117) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_9_9) = v2 & aScalar0(xP) = v1 & aScalar0(xP) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (29) with all_0_7_7, xR and discharging atoms sdtasdt0(xR, xR) = all_0_7_7, yields: % 30.27/9.72 | (118) ? [v0] : ? [v1] : (sdtlseqdt0(sz0z00, all_0_7_7) = v1 & aScalar0(xR) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (42) with all_0_7_7, xR, xR and discharging atoms sdtasdt0(xR, xR) = all_0_7_7, yields: % 30.27/9.72 | (119) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_7_7) = v2 & aScalar0(xR) = v1 & aScalar0(xR) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (67) with all_0_8_8, all_0_9_9, all_0_9_9, xP, xP, xP and discharging atoms sdtasdt0(xP, xP) = all_0_9_9, sdtpldt0(all_0_9_9, all_0_9_9) = all_0_8_8, yields: % 30.27/9.72 | (120) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v5, xP) = v6 & sdtasdt0(xP, v3) = v4 & sdtasdt0(xP, xP) = v7 & sdtpldt0(all_0_9_9, v7) = v8 & sdtpldt0(xP, xP) = v5 & sdtpldt0(xP, xP) = v3 & aScalar0(xP) = v2 & aScalar0(xP) = v1 & aScalar0(xP) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v6 & v4 = all_0_8_8))) % 30.27/9.72 | % 30.27/9.72 | Instantiating formula (100) with all_0_4_4, xP, xP and discharging atoms sdtpldt0(xP, xP) = all_0_4_4, yields: % 30.27/9.73 | (121) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_4_4) = v2 & aScalar0(xP) = v1 & aScalar0(xP) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.73 | % 30.27/9.73 | Instantiating formula (59) with all_0_0_0, all_0_2_2, all_0_4_4, xS, xP, xR, xP and discharging atoms sdtlseqdt0(all_0_4_4, all_0_2_2) = all_0_0_0, sdtpldt0(xP, xP) = all_0_4_4, sdtpldt0(xR, xS) = all_0_2_2, yields: % 30.27/9.73 | (122) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(xP, xS) = v5 & sdtlseqdt0(xP, xR) = v4 & aScalar0(xS) = v3 & aScalar0(xP) = v2 & aScalar0(xP) = v0 & aScalar0(xR) = v1 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.73 | % 30.27/9.73 | Instantiating formula (100) with all_0_2_2, xS, xR and discharging atoms sdtpldt0(xR, xS) = all_0_2_2, yields: % 30.27/9.73 | (123) ? [v0] : ? [v1] : ? [v2] : (aScalar0(all_0_2_2) = v2 & aScalar0(xS) = v1 & aScalar0(xR) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 30.27/9.73 | % 30.27/9.73 | Instantiating (123) with all_8_0_14, all_8_1_15, all_8_2_16 yields: % 30.27/9.73 | (124) aScalar0(all_0_2_2) = all_8_0_14 & aScalar0(xS) = all_8_1_15 & aScalar0(xR) = all_8_2_16 & ( ~ (all_8_1_15 = 0) | ~ (all_8_2_16 = 0) | all_8_0_14 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (124) yields: % 30.27/9.73 | (125) aScalar0(all_0_2_2) = all_8_0_14 % 30.27/9.73 | (126) aScalar0(xS) = all_8_1_15 % 30.27/9.73 | (127) aScalar0(xR) = all_8_2_16 % 30.27/9.73 | (128) ~ (all_8_1_15 = 0) | ~ (all_8_2_16 = 0) | all_8_0_14 = 0 % 30.27/9.73 | % 30.27/9.73 | Instantiating (121) with all_10_0_17, all_10_1_18, all_10_2_19 yields: % 30.27/9.73 | (129) aScalar0(all_0_4_4) = all_10_0_17 & aScalar0(xP) = all_10_1_18 & aScalar0(xP) = all_10_2_19 & ( ~ (all_10_1_18 = 0) | ~ (all_10_2_19 = 0) | all_10_0_17 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (129) yields: % 30.27/9.73 | (130) aScalar0(all_0_4_4) = all_10_0_17 % 30.27/9.73 | (131) aScalar0(xP) = all_10_1_18 % 30.27/9.73 | (132) aScalar0(xP) = all_10_2_19 % 30.27/9.73 | (133) ~ (all_10_1_18 = 0) | ~ (all_10_2_19 = 0) | all_10_0_17 = 0 % 30.27/9.73 | % 30.27/9.73 | Instantiating (111) with all_16_0_32, all_16_1_33, all_16_2_34 yields: % 30.27/9.73 | (134) aScalar0(all_0_1_1) = all_16_0_32 & aScalar0(all_0_2_2) = all_16_1_33 & aScalar0(all_0_2_2) = all_16_2_34 & ( ~ (all_16_1_33 = 0) | ~ (all_16_2_34 = 0) | all_16_0_32 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (134) yields: % 30.27/9.73 | (135) aScalar0(all_0_1_1) = all_16_0_32 % 30.27/9.73 | (136) aScalar0(all_0_2_2) = all_16_1_33 % 30.27/9.73 | (137) aScalar0(all_0_2_2) = all_16_2_34 % 30.27/9.73 | (138) ~ (all_16_1_33 = 0) | ~ (all_16_2_34 = 0) | all_16_0_32 = 0 % 30.27/9.73 | % 30.27/9.73 | Instantiating (110) with all_18_0_35, all_18_1_36 yields: % 30.27/9.73 | (139) sdtlseqdt0(sz0z00, all_0_1_1) = all_18_0_35 & aScalar0(all_0_2_2) = all_18_1_36 & ( ~ (all_18_1_36 = 0) | all_18_0_35 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (139) yields: % 30.27/9.73 | (140) sdtlseqdt0(sz0z00, all_0_1_1) = all_18_0_35 % 30.27/9.73 | (141) aScalar0(all_0_2_2) = all_18_1_36 % 30.27/9.73 | (142) ~ (all_18_1_36 = 0) | all_18_0_35 = 0 % 30.27/9.73 | % 30.27/9.73 | Instantiating (109) with all_30_0_56, all_30_1_57, all_30_2_58, all_30_3_59, all_30_4_60, all_30_5_61 yields: % 30.27/9.73 | (143) sdtlseqdt0(sz0z00, all_30_1_57) = all_30_0_56 & sdtlseqdt0(sz0z00, all_30_3_59) = all_30_2_58 & sdtasdt0(all_0_4_4, all_0_4_4) = all_30_1_57 & sdtpldt0(all_0_4_4, all_0_4_4) = all_30_3_59 & aScalar0(all_0_4_4) = all_30_4_60 & aScalar0(all_0_4_4) = all_30_5_61 & ( ~ (all_30_4_60 = 0) | ~ (all_30_5_61 = 0) | (all_30_0_56 = 0 & all_30_2_58 = 0)) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (143) yields: % 30.27/9.73 | (144) sdtpldt0(all_0_4_4, all_0_4_4) = all_30_3_59 % 30.27/9.73 | (145) sdtasdt0(all_0_4_4, all_0_4_4) = all_30_1_57 % 30.27/9.73 | (146) sdtlseqdt0(sz0z00, all_30_1_57) = all_30_0_56 % 30.27/9.73 | (147) aScalar0(all_0_4_4) = all_30_4_60 % 30.27/9.73 | (148) sdtlseqdt0(sz0z00, all_30_3_59) = all_30_2_58 % 30.27/9.73 | (149) ~ (all_30_4_60 = 0) | ~ (all_30_5_61 = 0) | (all_30_0_56 = 0 & all_30_2_58 = 0) % 30.27/9.73 | (150) aScalar0(all_0_4_4) = all_30_5_61 % 30.27/9.73 | % 30.27/9.73 | Instantiating (108) with all_40_0_66, all_40_1_67, all_40_2_68, all_40_3_69, all_40_4_70, all_40_5_71 yields: % 30.27/9.73 | (151) sdtlseqdt0(sz0z00, all_40_1_67) = all_40_0_66 & sdtlseqdt0(sz0z00, all_40_3_69) = all_40_2_68 & sdtasdt0(all_0_4_4, all_0_2_2) = all_40_1_67 & sdtpldt0(all_0_4_4, all_0_2_2) = all_40_3_69 & aScalar0(all_0_2_2) = all_40_4_70 & aScalar0(all_0_4_4) = all_40_5_71 & ( ~ (all_40_4_70 = 0) | ~ (all_40_5_71 = 0) | (all_40_0_66 = 0 & all_40_2_68 = 0)) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (151) yields: % 30.27/9.73 | (152) sdtlseqdt0(sz0z00, all_40_1_67) = all_40_0_66 % 30.27/9.73 | (153) sdtpldt0(all_0_4_4, all_0_2_2) = all_40_3_69 % 30.27/9.73 | (154) aScalar0(all_0_4_4) = all_40_5_71 % 30.27/9.73 | (155) sdtlseqdt0(sz0z00, all_40_3_69) = all_40_2_68 % 30.27/9.73 | (156) aScalar0(all_0_2_2) = all_40_4_70 % 30.27/9.73 | (157) sdtasdt0(all_0_4_4, all_0_2_2) = all_40_1_67 % 30.27/9.73 | (158) ~ (all_40_4_70 = 0) | ~ (all_40_5_71 = 0) | (all_40_0_66 = 0 & all_40_2_68 = 0) % 30.27/9.73 | % 30.27/9.73 | Instantiating (107) with all_60_0_108, all_60_1_109, all_60_2_110, all_60_3_111, all_60_4_112, all_60_5_113 yields: % 30.27/9.73 | (159) sdtlseqdt0(sz0z00, all_60_1_109) = all_60_0_108 & sdtlseqdt0(sz0z00, all_60_3_111) = all_60_2_110 & sdtasdt0(all_0_2_2, all_0_4_4) = all_60_1_109 & sdtpldt0(all_0_2_2, all_0_4_4) = all_60_3_111 & aScalar0(all_0_2_2) = all_60_5_113 & aScalar0(all_0_4_4) = all_60_4_112 & ( ~ (all_60_4_112 = 0) | ~ (all_60_5_113 = 0) | (all_60_0_108 = 0 & all_60_2_110 = 0)) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (159) yields: % 30.27/9.73 | (160) aScalar0(all_0_2_2) = all_60_5_113 % 30.27/9.73 | (161) sdtasdt0(all_0_2_2, all_0_4_4) = all_60_1_109 % 30.27/9.73 | (162) sdtlseqdt0(sz0z00, all_60_3_111) = all_60_2_110 % 30.27/9.73 | (163) sdtpldt0(all_0_2_2, all_0_4_4) = all_60_3_111 % 30.27/9.73 | (164) ~ (all_60_4_112 = 0) | ~ (all_60_5_113 = 0) | (all_60_0_108 = 0 & all_60_2_110 = 0) % 30.27/9.73 | (165) sdtlseqdt0(sz0z00, all_60_1_109) = all_60_0_108 % 30.27/9.73 | (166) aScalar0(all_0_4_4) = all_60_4_112 % 30.27/9.73 | % 30.27/9.73 | Instantiating (105) with all_62_0_114, all_62_1_115, all_62_2_116, all_62_3_117, all_62_4_118, all_62_5_119 yields: % 30.27/9.73 | (167) sdtlseqdt0(sz0z00, all_62_1_115) = all_62_0_114 & sdtlseqdt0(sz0z00, all_62_3_117) = all_62_2_116 & sdtasdt0(all_0_2_2, all_0_2_2) = all_62_1_115 & sdtpldt0(all_0_2_2, all_0_2_2) = all_62_3_117 & aScalar0(all_0_2_2) = all_62_4_118 & aScalar0(all_0_2_2) = all_62_5_119 & ( ~ (all_62_4_118 = 0) | ~ (all_62_5_119 = 0) | (all_62_0_114 = 0 & all_62_2_116 = 0)) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (167) yields: % 30.27/9.73 | (168) aScalar0(all_0_2_2) = all_62_4_118 % 30.27/9.73 | (169) sdtlseqdt0(sz0z00, all_62_3_117) = all_62_2_116 % 30.27/9.73 | (170) ~ (all_62_4_118 = 0) | ~ (all_62_5_119 = 0) | (all_62_0_114 = 0 & all_62_2_116 = 0) % 30.27/9.73 | (171) sdtlseqdt0(sz0z00, all_62_1_115) = all_62_0_114 % 30.27/9.73 | (172) aScalar0(all_0_2_2) = all_62_5_119 % 30.27/9.73 | (173) sdtpldt0(all_0_2_2, all_0_2_2) = all_62_3_117 % 30.27/9.73 | (174) sdtasdt0(all_0_2_2, all_0_2_2) = all_62_1_115 % 30.27/9.73 | % 30.27/9.73 | Instantiating (120) with all_64_0_120, all_64_1_121, all_64_2_122, all_64_3_123, all_64_4_124, all_64_5_125, all_64_6_126, all_64_7_127, all_64_8_128 yields: % 30.27/9.73 | (175) sdtasdt0(all_64_3_123, xP) = all_64_2_122 & sdtasdt0(xP, all_64_5_125) = all_64_4_124 & sdtasdt0(xP, xP) = all_64_1_121 & sdtpldt0(all_0_9_9, all_64_1_121) = all_64_0_120 & sdtpldt0(xP, xP) = all_64_3_123 & sdtpldt0(xP, xP) = all_64_5_125 & aScalar0(xP) = all_64_6_126 & aScalar0(xP) = all_64_7_127 & aScalar0(xP) = all_64_8_128 & ( ~ (all_64_6_126 = 0) | ~ (all_64_7_127 = 0) | ~ (all_64_8_128 = 0) | (all_64_0_120 = all_64_2_122 & all_64_4_124 = all_0_8_8)) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (175) yields: % 30.27/9.73 | (176) aScalar0(xP) = all_64_8_128 % 30.27/9.73 | (177) sdtasdt0(xP, xP) = all_64_1_121 % 30.27/9.73 | (178) sdtasdt0(xP, all_64_5_125) = all_64_4_124 % 30.27/9.73 | (179) sdtasdt0(all_64_3_123, xP) = all_64_2_122 % 30.27/9.73 | (180) sdtpldt0(all_0_9_9, all_64_1_121) = all_64_0_120 % 30.27/9.73 | (181) aScalar0(xP) = all_64_7_127 % 30.27/9.73 | (182) sdtpldt0(xP, xP) = all_64_5_125 % 30.27/9.73 | (183) ~ (all_64_6_126 = 0) | ~ (all_64_7_127 = 0) | ~ (all_64_8_128 = 0) | (all_64_0_120 = all_64_2_122 & all_64_4_124 = all_0_8_8) % 30.27/9.73 | (184) aScalar0(xP) = all_64_6_126 % 30.27/9.73 | (185) sdtpldt0(xP, xP) = all_64_3_123 % 30.27/9.73 | % 30.27/9.73 | Instantiating (119) with all_78_0_144, all_78_1_145, all_78_2_146 yields: % 30.27/9.73 | (186) aScalar0(all_0_7_7) = all_78_0_144 & aScalar0(xR) = all_78_1_145 & aScalar0(xR) = all_78_2_146 & ( ~ (all_78_1_145 = 0) | ~ (all_78_2_146 = 0) | all_78_0_144 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (186) yields: % 30.27/9.73 | (187) aScalar0(all_0_7_7) = all_78_0_144 % 30.27/9.73 | (188) aScalar0(xR) = all_78_1_145 % 30.27/9.73 | (189) aScalar0(xR) = all_78_2_146 % 30.27/9.73 | (190) ~ (all_78_1_145 = 0) | ~ (all_78_2_146 = 0) | all_78_0_144 = 0 % 30.27/9.73 | % 30.27/9.73 | Instantiating (118) with all_80_0_147, all_80_1_148 yields: % 30.27/9.73 | (191) sdtlseqdt0(sz0z00, all_0_7_7) = all_80_0_147 & aScalar0(xR) = all_80_1_148 & ( ~ (all_80_1_148 = 0) | all_80_0_147 = 0) % 30.27/9.73 | % 30.27/9.73 | Applying alpha-rule on (191) yields: % 30.27/9.73 | (192) sdtlseqdt0(sz0z00, all_0_7_7) = all_80_0_147 % 30.27/9.73 | (193) aScalar0(xR) = all_80_1_148 % 30.27/9.73 | (194) ~ (all_80_1_148 = 0) | all_80_0_147 = 0 % 30.27/9.73 | % 30.27/9.74 | Instantiating (117) with all_82_0_149, all_82_1_150, all_82_2_151 yields: % 30.27/9.74 | (195) aScalar0(all_0_9_9) = all_82_0_149 & aScalar0(xP) = all_82_1_150 & aScalar0(xP) = all_82_2_151 & ( ~ (all_82_1_150 = 0) | ~ (all_82_2_151 = 0) | all_82_0_149 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (195) yields: % 30.27/9.74 | (196) aScalar0(all_0_9_9) = all_82_0_149 % 30.27/9.74 | (197) aScalar0(xP) = all_82_1_150 % 30.27/9.74 | (198) aScalar0(xP) = all_82_2_151 % 30.27/9.74 | (199) ~ (all_82_1_150 = 0) | ~ (all_82_2_151 = 0) | all_82_0_149 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating (115) with all_84_0_152, all_84_1_153, all_84_2_154 yields: % 30.27/9.74 | (200) aScalar0(all_0_6_6) = all_84_0_152 & aScalar0(xS) = all_84_1_153 & aScalar0(xS) = all_84_2_154 & ( ~ (all_84_1_153 = 0) | ~ (all_84_2_154 = 0) | all_84_0_152 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (200) yields: % 30.27/9.74 | (201) aScalar0(all_0_6_6) = all_84_0_152 % 30.27/9.74 | (202) aScalar0(xS) = all_84_1_153 % 30.27/9.74 | (203) aScalar0(xS) = all_84_2_154 % 30.27/9.74 | (204) ~ (all_84_1_153 = 0) | ~ (all_84_2_154 = 0) | all_84_0_152 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating (116) with all_86_0_155, all_86_1_156 yields: % 30.27/9.74 | (205) sdtlseqdt0(sz0z00, all_0_9_9) = all_86_0_155 & aScalar0(xP) = all_86_1_156 & ( ~ (all_86_1_156 = 0) | all_86_0_155 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (205) yields: % 30.27/9.74 | (206) sdtlseqdt0(sz0z00, all_0_9_9) = all_86_0_155 % 30.27/9.74 | (207) aScalar0(xP) = all_86_1_156 % 30.27/9.74 | (208) ~ (all_86_1_156 = 0) | all_86_0_155 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating (114) with all_88_0_157, all_88_1_158 yields: % 30.27/9.74 | (209) sdtlseqdt0(sz0z00, all_0_6_6) = all_88_0_157 & aScalar0(xS) = all_88_1_158 & ( ~ (all_88_1_158 = 0) | all_88_0_157 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (209) yields: % 30.27/9.74 | (210) sdtlseqdt0(sz0z00, all_0_6_6) = all_88_0_157 % 30.27/9.74 | (211) aScalar0(xS) = all_88_1_158 % 30.27/9.74 | (212) ~ (all_88_1_158 = 0) | all_88_0_157 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating (113) with all_90_0_159, all_90_1_160, all_90_2_161 yields: % 30.27/9.74 | (213) aScalar0(all_0_3_3) = all_90_0_159 & aScalar0(all_0_4_4) = all_90_1_160 & aScalar0(all_0_4_4) = all_90_2_161 & ( ~ (all_90_1_160 = 0) | ~ (all_90_2_161 = 0) | all_90_0_159 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (213) yields: % 30.27/9.74 | (214) aScalar0(all_0_3_3) = all_90_0_159 % 30.27/9.74 | (215) aScalar0(all_0_4_4) = all_90_1_160 % 30.27/9.74 | (216) aScalar0(all_0_4_4) = all_90_2_161 % 30.27/9.74 | (217) ~ (all_90_1_160 = 0) | ~ (all_90_2_161 = 0) | all_90_0_159 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating (112) with all_92_0_162, all_92_1_163 yields: % 30.27/9.74 | (218) sdtlseqdt0(sz0z00, all_0_3_3) = all_92_0_162 & aScalar0(all_0_4_4) = all_92_1_163 & ( ~ (all_92_1_163 = 0) | all_92_0_162 = 0) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (218) yields: % 30.27/9.74 | (219) sdtlseqdt0(sz0z00, all_0_3_3) = all_92_0_162 % 30.27/9.74 | (220) aScalar0(all_0_4_4) = all_92_1_163 % 30.27/9.74 | (221) ~ (all_92_1_163 = 0) | all_92_0_162 = 0 % 30.27/9.74 | % 30.27/9.74 +-Applying beta-rule and splitting (122), into two cases. % 30.27/9.74 |-Branch one: % 30.27/9.74 | (222) all_0_0_0 = 0 % 30.27/9.74 | % 30.27/9.74 | Equations (222) can reduce 41 to: % 30.27/9.74 | (223) $false % 30.27/9.74 | % 30.27/9.74 |-The branch is then unsatisfiable % 30.27/9.74 |-Branch two: % 30.27/9.74 | (41) ~ (all_0_0_0 = 0) % 30.27/9.74 | (225) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(xP, xS) = v5 & sdtlseqdt0(xP, xR) = v4 & aScalar0(xS) = v3 & aScalar0(xP) = v2 & aScalar0(xP) = v0 & aScalar0(xR) = v1 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.74 | % 30.27/9.74 | Instantiating (225) with all_98_0_164, all_98_1_165, all_98_2_166, all_98_3_167, all_98_4_168, all_98_5_169 yields: % 30.27/9.74 | (226) sdtlseqdt0(xP, xS) = all_98_0_164 & sdtlseqdt0(xP, xR) = all_98_1_165 & aScalar0(xS) = all_98_2_166 & aScalar0(xP) = all_98_3_167 & aScalar0(xP) = all_98_5_169 & aScalar0(xR) = all_98_4_168 & ( ~ (all_98_0_164 = 0) | ~ (all_98_1_165 = 0) | ~ (all_98_2_166 = 0) | ~ (all_98_3_167 = 0) | ~ (all_98_4_168 = 0) | ~ (all_98_5_169 = 0)) % 30.27/9.74 | % 30.27/9.74 | Applying alpha-rule on (226) yields: % 30.27/9.74 | (227) aScalar0(xP) = all_98_3_167 % 30.27/9.74 | (228) aScalar0(xP) = all_98_5_169 % 30.27/9.74 | (229) ~ (all_98_0_164 = 0) | ~ (all_98_1_165 = 0) | ~ (all_98_2_166 = 0) | ~ (all_98_3_167 = 0) | ~ (all_98_4_168 = 0) | ~ (all_98_5_169 = 0) % 30.27/9.74 | (230) sdtlseqdt0(xP, xS) = all_98_0_164 % 30.27/9.74 | (231) sdtlseqdt0(xP, xR) = all_98_1_165 % 30.27/9.74 | (232) aScalar0(xS) = all_98_2_166 % 30.27/9.74 | (233) aScalar0(xR) = all_98_4_168 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (5) with all_0_2_2, all_0_2_2, all_62_1_115, all_0_1_1 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_62_1_115, sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 30.27/9.74 | (234) all_62_1_115 = all_0_1_1 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (5) with all_0_4_4, all_0_4_4, all_30_1_57, all_0_3_3 and discharging atoms sdtasdt0(all_0_4_4, all_0_4_4) = all_30_1_57, sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3, yields: % 30.27/9.74 | (235) all_30_1_57 = all_0_3_3 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_60_5_113, all_62_4_118 and discharging atoms aScalar0(all_0_2_2) = all_62_4_118, aScalar0(all_0_2_2) = all_60_5_113, yields: % 30.27/9.74 | (236) all_62_4_118 = all_60_5_113 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_40_4_70, all_60_5_113 and discharging atoms aScalar0(all_0_2_2) = all_60_5_113, aScalar0(all_0_2_2) = all_40_4_70, yields: % 30.27/9.74 | (237) all_60_5_113 = all_40_4_70 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_18_1_36, all_40_4_70 and discharging atoms aScalar0(all_0_2_2) = all_40_4_70, aScalar0(all_0_2_2) = all_18_1_36, yields: % 30.27/9.74 | (238) all_40_4_70 = all_18_1_36 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_16_1_33, all_62_5_119 and discharging atoms aScalar0(all_0_2_2) = all_62_5_119, aScalar0(all_0_2_2) = all_16_1_33, yields: % 30.27/9.74 | (239) all_62_5_119 = all_16_1_33 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_16_1_33, all_18_1_36 and discharging atoms aScalar0(all_0_2_2) = all_18_1_36, aScalar0(all_0_2_2) = all_16_1_33, yields: % 30.27/9.74 | (240) all_18_1_36 = all_16_1_33 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_16_2_34, all_62_5_119 and discharging atoms aScalar0(all_0_2_2) = all_62_5_119, aScalar0(all_0_2_2) = all_16_2_34, yields: % 30.27/9.74 | (241) all_62_5_119 = all_16_2_34 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_2_2, all_8_0_14, all_62_4_118 and discharging atoms aScalar0(all_0_2_2) = all_62_4_118, aScalar0(all_0_2_2) = all_8_0_14, yields: % 30.27/9.74 | (242) all_62_4_118 = all_8_0_14 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_90_1_160, all_92_1_163 and discharging atoms aScalar0(all_0_4_4) = all_92_1_163, aScalar0(all_0_4_4) = all_90_1_160, yields: % 30.27/9.74 | (243) all_92_1_163 = all_90_1_160 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_90_2_161, all_92_1_163 and discharging atoms aScalar0(all_0_4_4) = all_92_1_163, aScalar0(all_0_4_4) = all_90_2_161, yields: % 30.27/9.74 | (244) all_92_1_163 = all_90_2_161 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_60_4_112, all_90_2_161 and discharging atoms aScalar0(all_0_4_4) = all_90_2_161, aScalar0(all_0_4_4) = all_60_4_112, yields: % 30.27/9.74 | (245) all_90_2_161 = all_60_4_112 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_40_5_71, all_60_4_112 and discharging atoms aScalar0(all_0_4_4) = all_60_4_112, aScalar0(all_0_4_4) = all_40_5_71, yields: % 30.27/9.74 | (246) all_60_4_112 = all_40_5_71 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_30_4_60, all_40_5_71 and discharging atoms aScalar0(all_0_4_4) = all_40_5_71, aScalar0(all_0_4_4) = all_30_4_60, yields: % 30.27/9.74 | (247) all_40_5_71 = all_30_4_60 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_30_5_61, all_30_4_60 and discharging atoms aScalar0(all_0_4_4) = all_30_4_60, aScalar0(all_0_4_4) = all_30_5_61, yields: % 30.27/9.74 | (248) all_30_4_60 = all_30_5_61 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with all_0_4_4, all_10_0_17, all_92_1_163 and discharging atoms aScalar0(all_0_4_4) = all_92_1_163, aScalar0(all_0_4_4) = all_10_0_17, yields: % 30.27/9.74 | (249) all_92_1_163 = all_10_0_17 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xS, all_88_1_158, all_98_2_166 and discharging atoms aScalar0(xS) = all_98_2_166, aScalar0(xS) = all_88_1_158, yields: % 30.27/9.74 | (250) all_98_2_166 = all_88_1_158 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xS, all_84_1_153, all_88_1_158 and discharging atoms aScalar0(xS) = all_88_1_158, aScalar0(xS) = all_84_1_153, yields: % 30.27/9.74 | (251) all_88_1_158 = all_84_1_153 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xS, all_84_2_154, 0 and discharging atoms aScalar0(xS) = all_84_2_154, aScalar0(xS) = 0, yields: % 30.27/9.74 | (252) all_84_2_154 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xS, all_84_2_154, all_88_1_158 and discharging atoms aScalar0(xS) = all_88_1_158, aScalar0(xS) = all_84_2_154, yields: % 30.27/9.74 | (253) all_88_1_158 = all_84_2_154 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xS, all_8_1_15, all_98_2_166 and discharging atoms aScalar0(xS) = all_98_2_166, aScalar0(xS) = all_8_1_15, yields: % 30.27/9.74 | (254) all_98_2_166 = all_8_1_15 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_98_5_169, all_98_3_167 and discharging atoms aScalar0(xP) = all_98_3_167, aScalar0(xP) = all_98_5_169, yields: % 30.27/9.74 | (255) all_98_3_167 = all_98_5_169 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_86_1_156, all_98_5_169 and discharging atoms aScalar0(xP) = all_98_5_169, aScalar0(xP) = all_86_1_156, yields: % 30.27/9.74 | (256) all_98_5_169 = all_86_1_156 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_82_2_151, all_82_1_150 and discharging atoms aScalar0(xP) = all_82_1_150, aScalar0(xP) = all_82_2_151, yields: % 30.27/9.74 | (257) all_82_1_150 = all_82_2_151 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_64_6_126, 0 and discharging atoms aScalar0(xP) = all_64_6_126, aScalar0(xP) = 0, yields: % 30.27/9.74 | (258) all_64_6_126 = 0 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_64_6_126, all_86_1_156 and discharging atoms aScalar0(xP) = all_86_1_156, aScalar0(xP) = all_64_6_126, yields: % 30.27/9.74 | (259) all_86_1_156 = all_64_6_126 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_64_6_126, all_82_2_151 and discharging atoms aScalar0(xP) = all_82_2_151, aScalar0(xP) = all_64_6_126, yields: % 30.27/9.74 | (260) all_82_2_151 = all_64_6_126 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_64_7_127, all_98_3_167 and discharging atoms aScalar0(xP) = all_98_3_167, aScalar0(xP) = all_64_7_127, yields: % 30.27/9.74 | (261) all_98_3_167 = all_64_7_127 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_64_8_128, all_82_1_150 and discharging atoms aScalar0(xP) = all_82_1_150, aScalar0(xP) = all_64_8_128, yields: % 30.27/9.74 | (262) all_82_1_150 = all_64_8_128 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_10_1_18, all_82_2_151 and discharging atoms aScalar0(xP) = all_82_2_151, aScalar0(xP) = all_10_1_18, yields: % 30.27/9.74 | (263) all_82_2_151 = all_10_1_18 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xP, all_10_2_19, all_82_2_151 and discharging atoms aScalar0(xP) = all_82_2_151, aScalar0(xP) = all_10_2_19, yields: % 30.27/9.74 | (264) all_82_2_151 = all_10_2_19 % 30.27/9.74 | % 30.27/9.74 | Instantiating formula (15) with xR, all_98_4_168, 0 and discharging atoms aScalar0(xR) = all_98_4_168, aScalar0(xR) = 0, yields: % 30.27/9.74 | (265) all_98_4_168 = 0 % 30.27/9.75 | % 30.27/9.75 | Instantiating formula (15) with xR, all_80_1_148, all_98_4_168 and discharging atoms aScalar0(xR) = all_98_4_168, aScalar0(xR) = all_80_1_148, yields: % 30.27/9.75 | (266) all_98_4_168 = all_80_1_148 % 30.27/9.75 | % 30.27/9.75 | Instantiating formula (15) with xR, all_78_1_145, all_80_1_148 and discharging atoms aScalar0(xR) = all_80_1_148, aScalar0(xR) = all_78_1_145, yields: % 30.27/9.75 | (267) all_80_1_148 = all_78_1_145 % 30.27/9.75 | % 30.27/9.75 | Instantiating formula (15) with xR, all_78_2_146, all_78_1_145 and discharging atoms aScalar0(xR) = all_78_1_145, aScalar0(xR) = all_78_2_146, yields: % 30.27/9.75 | (268) all_78_1_145 = all_78_2_146 % 30.27/9.75 | % 30.27/9.75 | Instantiating formula (15) with xR, all_8_2_16, all_78_2_146 and discharging atoms aScalar0(xR) = all_78_2_146, aScalar0(xR) = all_8_2_16, yields: % 30.27/9.75 | (269) all_78_2_146 = all_8_2_16 % 30.27/9.75 | % 30.27/9.75 | Combining equations (250,254) yields a new equation: % 30.27/9.75 | (270) all_88_1_158 = all_8_1_15 % 30.27/9.75 | % 30.27/9.75 | Simplifying 270 yields: % 30.27/9.75 | (271) all_88_1_158 = all_8_1_15 % 30.27/9.75 | % 30.27/9.75 | Combining equations (255,261) yields a new equation: % 30.27/9.75 | (272) all_98_5_169 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Simplifying 272 yields: % 30.27/9.75 | (273) all_98_5_169 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Combining equations (266,265) yields a new equation: % 30.27/9.75 | (274) all_80_1_148 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 274 yields: % 30.27/9.75 | (275) all_80_1_148 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (256,273) yields a new equation: % 30.27/9.75 | (276) all_86_1_156 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Simplifying 276 yields: % 30.27/9.75 | (277) all_86_1_156 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Combining equations (244,243) yields a new equation: % 30.27/9.75 | (278) all_90_1_160 = all_90_2_161 % 30.27/9.75 | % 30.27/9.75 | Combining equations (249,243) yields a new equation: % 30.27/9.75 | (279) all_90_1_160 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (278,279) yields a new equation: % 30.27/9.75 | (280) all_90_2_161 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Simplifying 280 yields: % 30.27/9.75 | (281) all_90_2_161 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (245,281) yields a new equation: % 30.27/9.75 | (282) all_60_4_112 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Simplifying 282 yields: % 30.27/9.75 | (283) all_60_4_112 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (253,251) yields a new equation: % 30.27/9.75 | (284) all_84_1_153 = all_84_2_154 % 30.27/9.75 | % 30.27/9.75 | Combining equations (271,251) yields a new equation: % 30.27/9.75 | (285) all_84_1_153 = all_8_1_15 % 30.27/9.75 | % 30.27/9.75 | Combining equations (259,277) yields a new equation: % 30.27/9.75 | (286) all_64_6_126 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Simplifying 286 yields: % 30.27/9.75 | (287) all_64_6_126 = all_64_7_127 % 30.27/9.75 | % 30.27/9.75 | Combining equations (284,285) yields a new equation: % 30.27/9.75 | (288) all_84_2_154 = all_8_1_15 % 30.27/9.75 | % 30.27/9.75 | Simplifying 288 yields: % 30.27/9.75 | (289) all_84_2_154 = all_8_1_15 % 30.27/9.75 | % 30.27/9.75 | Combining equations (289,252) yields a new equation: % 30.27/9.75 | (290) all_8_1_15 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 290 yields: % 30.27/9.75 | (291) all_8_1_15 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (257,262) yields a new equation: % 30.27/9.75 | (292) all_82_2_151 = all_64_8_128 % 30.27/9.75 | % 30.27/9.75 | Simplifying 292 yields: % 30.27/9.75 | (293) all_82_2_151 = all_64_8_128 % 30.27/9.75 | % 30.27/9.75 | Combining equations (264,293) yields a new equation: % 30.27/9.75 | (294) all_64_8_128 = all_10_2_19 % 30.27/9.75 | % 30.27/9.75 | Combining equations (260,293) yields a new equation: % 30.27/9.75 | (295) all_64_6_126 = all_64_8_128 % 30.27/9.75 | % 30.27/9.75 | Simplifying 295 yields: % 30.27/9.75 | (296) all_64_6_126 = all_64_8_128 % 30.27/9.75 | % 30.27/9.75 | Combining equations (263,293) yields a new equation: % 30.27/9.75 | (297) all_64_8_128 = all_10_1_18 % 30.27/9.75 | % 30.27/9.75 | Combining equations (267,275) yields a new equation: % 30.27/9.75 | (298) all_78_1_145 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 298 yields: % 30.27/9.75 | (299) all_78_1_145 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (268,299) yields a new equation: % 30.27/9.75 | (300) all_78_2_146 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 300 yields: % 30.27/9.75 | (301) all_78_2_146 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (269,301) yields a new equation: % 30.27/9.75 | (302) all_8_2_16 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 302 yields: % 30.27/9.75 | (303) all_8_2_16 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (258,287) yields a new equation: % 30.27/9.75 | (304) all_64_7_127 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (296,287) yields a new equation: % 30.27/9.75 | (305) all_64_7_127 = all_64_8_128 % 30.27/9.75 | % 30.27/9.75 | Combining equations (305,304) yields a new equation: % 30.27/9.75 | (306) all_64_8_128 = 0 % 30.27/9.75 | % 30.27/9.75 | Simplifying 306 yields: % 30.27/9.75 | (307) all_64_8_128 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (294,297) yields a new equation: % 30.27/9.75 | (308) all_10_1_18 = all_10_2_19 % 30.27/9.75 | % 30.27/9.75 | Combining equations (307,297) yields a new equation: % 30.27/9.75 | (309) all_10_1_18 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (236,242) yields a new equation: % 30.27/9.75 | (310) all_60_5_113 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Simplifying 310 yields: % 30.27/9.75 | (311) all_60_5_113 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Combining equations (239,241) yields a new equation: % 30.27/9.75 | (312) all_16_1_33 = all_16_2_34 % 30.27/9.75 | % 30.27/9.75 | Simplifying 312 yields: % 30.27/9.75 | (313) all_16_1_33 = all_16_2_34 % 30.27/9.75 | % 30.27/9.75 | Combining equations (246,283) yields a new equation: % 30.27/9.75 | (314) all_40_5_71 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Simplifying 314 yields: % 30.27/9.75 | (315) all_40_5_71 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (237,311) yields a new equation: % 30.27/9.75 | (316) all_40_4_70 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Simplifying 316 yields: % 30.27/9.75 | (317) all_40_4_70 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Combining equations (238,317) yields a new equation: % 30.27/9.75 | (318) all_18_1_36 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Simplifying 318 yields: % 30.27/9.75 | (319) all_18_1_36 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Combining equations (247,315) yields a new equation: % 30.27/9.75 | (320) all_30_4_60 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Simplifying 320 yields: % 30.27/9.75 | (321) all_30_4_60 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (248,321) yields a new equation: % 30.27/9.75 | (322) all_30_5_61 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Simplifying 322 yields: % 30.27/9.75 | (323) all_30_5_61 = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 | Combining equations (240,319) yields a new equation: % 30.27/9.75 | (324) all_16_1_33 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Simplifying 324 yields: % 30.27/9.75 | (325) all_16_1_33 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Combining equations (313,325) yields a new equation: % 30.27/9.75 | (326) all_16_2_34 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Simplifying 326 yields: % 30.27/9.75 | (327) all_16_2_34 = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | Combining equations (309,308) yields a new equation: % 30.27/9.75 | (328) all_10_2_19 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (328,308) yields a new equation: % 30.27/9.75 | (309) all_10_1_18 = 0 % 30.27/9.75 | % 30.27/9.75 | From (234) and (174) follows: % 30.27/9.75 | (61) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_1_1 % 30.27/9.75 | % 30.27/9.75 | From (235) and (145) follows: % 30.27/9.75 | (18) sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3 % 30.27/9.75 | % 30.27/9.75 | From (327) and (137) follows: % 30.27/9.75 | (125) aScalar0(all_0_2_2) = all_8_0_14 % 30.27/9.75 | % 30.27/9.75 | From (323) and (150) follows: % 30.27/9.75 | (130) aScalar0(all_0_4_4) = all_10_0_17 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (133), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (334) ~ (all_10_1_18 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (309) can reduce 334 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (309) all_10_1_18 = 0 % 30.27/9.75 | (337) ~ (all_10_2_19 = 0) | all_10_0_17 = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (337), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (338) ~ (all_10_2_19 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (328) can reduce 338 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (328) all_10_2_19 = 0 % 30.27/9.75 | (341) all_10_0_17 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (341,281) yields a new equation: % 30.27/9.75 | (342) all_90_2_161 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (341,279) yields a new equation: % 30.27/9.75 | (343) all_90_1_160 = 0 % 30.27/9.75 | % 30.27/9.75 | From (341) and (130) follows: % 30.27/9.75 | (344) aScalar0(all_0_4_4) = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (217), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (345) ~ (all_90_1_160 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (343) can reduce 345 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (343) all_90_1_160 = 0 % 30.27/9.75 | (348) ~ (all_90_2_161 = 0) | all_90_0_159 = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (128), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (349) ~ (all_8_1_15 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (291) can reduce 349 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (291) all_8_1_15 = 0 % 30.27/9.75 | (352) ~ (all_8_2_16 = 0) | all_8_0_14 = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (352), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (353) ~ (all_8_2_16 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (303) can reduce 353 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (303) all_8_2_16 = 0 % 30.27/9.75 | (356) all_8_0_14 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (356,327) yields a new equation: % 30.27/9.75 | (357) all_16_2_34 = 0 % 30.27/9.75 | % 30.27/9.75 | Combining equations (356,325) yields a new equation: % 30.27/9.75 | (358) all_16_1_33 = 0 % 30.27/9.75 | % 30.27/9.75 | From (356) and (125) follows: % 30.27/9.75 | (359) aScalar0(all_0_2_2) = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (138), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (360) ~ (all_16_1_33 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (358) can reduce 360 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (358) all_16_1_33 = 0 % 30.27/9.75 | (363) ~ (all_16_2_34 = 0) | all_16_0_32 = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (363), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (364) ~ (all_16_2_34 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (357) can reduce 364 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (357) all_16_2_34 = 0 % 30.27/9.75 | (367) all_16_0_32 = 0 % 30.27/9.75 | % 30.27/9.75 | From (367) and (135) follows: % 30.27/9.75 | (368) aScalar0(all_0_1_1) = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (348), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (369) ~ (all_90_2_161 = 0) % 30.27/9.75 | % 30.27/9.75 | Equations (342) can reduce 369 to: % 30.27/9.75 | (223) $false % 30.27/9.75 | % 30.27/9.75 |-The branch is then unsatisfiable % 30.27/9.75 |-Branch two: % 30.27/9.75 | (342) all_90_2_161 = 0 % 30.27/9.75 | (372) all_90_0_159 = 0 % 30.27/9.75 | % 30.27/9.75 | From (372) and (214) follows: % 30.27/9.75 | (373) aScalar0(all_0_3_3) = 0 % 30.27/9.75 | % 30.27/9.75 +-Applying beta-rule and splitting (106), into two cases. % 30.27/9.75 |-Branch one: % 30.27/9.75 | (374) all_0_2_2 = all_0_4_4 % 30.27/9.75 | % 30.27/9.75 | Equations (374) can reduce 13 to: % 30.27/9.75 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (13) ~ (all_0_2_2 = all_0_4_4) % 30.27/9.76 | (377) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(all_0_2_2, all_0_2_2) = v3 & sdtasdt0(all_0_4_4, all_0_4_4) = v2 & aScalar0(all_0_2_2) = v1 & aScalar0(all_0_4_4) = v0 & ( ~ (v3 = v2) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.76 | % 30.27/9.76 | Instantiating (377) with all_246_0_176, all_246_1_177, all_246_2_178, all_246_3_179 yields: % 30.27/9.76 | (378) sdtasdt0(all_0_2_2, all_0_2_2) = all_246_0_176 & sdtasdt0(all_0_4_4, all_0_4_4) = all_246_1_177 & aScalar0(all_0_2_2) = all_246_2_178 & aScalar0(all_0_4_4) = all_246_3_179 & ( ~ (all_246_0_176 = all_246_1_177) | ~ (all_246_2_178 = 0) | ~ (all_246_3_179 = 0)) % 30.27/9.76 | % 30.27/9.76 | Applying alpha-rule on (378) yields: % 30.27/9.76 | (379) sdtasdt0(all_0_2_2, all_0_2_2) = all_246_0_176 % 30.27/9.76 | (380) aScalar0(all_0_2_2) = all_246_2_178 % 30.27/9.76 | (381) aScalar0(all_0_4_4) = all_246_3_179 % 30.27/9.76 | (382) sdtasdt0(all_0_4_4, all_0_4_4) = all_246_1_177 % 30.27/9.76 | (383) ~ (all_246_0_176 = all_246_1_177) | ~ (all_246_2_178 = 0) | ~ (all_246_3_179 = 0) % 30.27/9.76 | % 30.27/9.76 +-Applying beta-rule and splitting (104), into two cases. % 30.27/9.76 |-Branch one: % 30.27/9.76 | (384) all_0_1_1 = all_0_3_3 % 30.27/9.76 | % 30.27/9.76 | From (384) and (61) follows: % 30.27/9.76 | (385) sdtasdt0(all_0_2_2, all_0_2_2) = all_0_3_3 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (5) with all_0_2_2, all_0_2_2, all_0_3_3, all_246_0_176 and discharging atoms sdtasdt0(all_0_2_2, all_0_2_2) = all_246_0_176, sdtasdt0(all_0_2_2, all_0_2_2) = all_0_3_3, yields: % 30.27/9.76 | (386) all_246_0_176 = all_0_3_3 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (5) with all_0_4_4, all_0_4_4, all_246_1_177, all_0_3_3 and discharging atoms sdtasdt0(all_0_4_4, all_0_4_4) = all_246_1_177, sdtasdt0(all_0_4_4, all_0_4_4) = all_0_3_3, yields: % 30.27/9.76 | (387) all_246_1_177 = all_0_3_3 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (15) with all_0_2_2, 0, all_246_2_178 and discharging atoms aScalar0(all_0_2_2) = all_246_2_178, aScalar0(all_0_2_2) = 0, yields: % 30.27/9.76 | (388) all_246_2_178 = 0 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (15) with all_0_4_4, all_246_3_179, 0 and discharging atoms aScalar0(all_0_4_4) = all_246_3_179, aScalar0(all_0_4_4) = 0, yields: % 30.27/9.76 | (389) all_246_3_179 = 0 % 30.27/9.76 | % 30.27/9.76 +-Applying beta-rule and splitting (383), into two cases. % 30.27/9.76 |-Branch one: % 30.27/9.76 | (390) ~ (all_246_2_178 = 0) % 30.27/9.76 | % 30.27/9.76 | Equations (388) can reduce 390 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (388) all_246_2_178 = 0 % 30.27/9.76 | (393) ~ (all_246_0_176 = all_246_1_177) | ~ (all_246_3_179 = 0) % 30.27/9.76 | % 30.27/9.76 +-Applying beta-rule and splitting (393), into two cases. % 30.27/9.76 |-Branch one: % 30.27/9.76 | (394) ~ (all_246_3_179 = 0) % 30.27/9.76 | % 30.27/9.76 | Equations (389) can reduce 394 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (389) all_246_3_179 = 0 % 30.27/9.76 | (397) ~ (all_246_0_176 = all_246_1_177) % 30.27/9.76 | % 30.27/9.76 | Equations (386,387) can reduce 397 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (399) ~ (all_0_1_1 = all_0_3_3) % 30.27/9.76 | (400) ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_0_1_1, all_0_3_3) = v2 & aScalar0(all_0_1_1) = v1 & aScalar0(all_0_3_3) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 30.27/9.76 | % 30.27/9.76 | Instantiating (400) with all_260_0_184, all_260_1_185, all_260_2_186 yields: % 30.27/9.76 | (401) sdtlseqdt0(all_0_1_1, all_0_3_3) = all_260_0_184 & aScalar0(all_0_1_1) = all_260_1_185 & aScalar0(all_0_3_3) = all_260_2_186 & ( ~ (all_260_0_184 = 0) | ~ (all_260_1_185 = 0) | ~ (all_260_2_186 = 0)) % 30.27/9.76 | % 30.27/9.76 | Applying alpha-rule on (401) yields: % 30.27/9.76 | (402) sdtlseqdt0(all_0_1_1, all_0_3_3) = all_260_0_184 % 30.27/9.76 | (403) aScalar0(all_0_1_1) = all_260_1_185 % 30.27/9.76 | (404) aScalar0(all_0_3_3) = all_260_2_186 % 30.27/9.76 | (405) ~ (all_260_0_184 = 0) | ~ (all_260_1_185 = 0) | ~ (all_260_2_186 = 0) % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (4) with all_0_1_1, all_0_3_3, all_260_0_184, 0 and discharging atoms sdtlseqdt0(all_0_1_1, all_0_3_3) = all_260_0_184, sdtlseqdt0(all_0_1_1, all_0_3_3) = 0, yields: % 30.27/9.76 | (406) all_260_0_184 = 0 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (15) with all_0_1_1, 0, all_260_1_185 and discharging atoms aScalar0(all_0_1_1) = all_260_1_185, aScalar0(all_0_1_1) = 0, yields: % 30.27/9.76 | (407) all_260_1_185 = 0 % 30.27/9.76 | % 30.27/9.76 | Instantiating formula (15) with all_0_3_3, all_260_2_186, 0 and discharging atoms aScalar0(all_0_3_3) = all_260_2_186, aScalar0(all_0_3_3) = 0, yields: % 30.27/9.76 | (408) all_260_2_186 = 0 % 30.27/9.76 | % 30.27/9.76 +-Applying beta-rule and splitting (405), into two cases. % 30.27/9.76 |-Branch one: % 30.27/9.76 | (409) ~ (all_260_0_184 = 0) % 30.27/9.76 | % 30.27/9.76 | Equations (406) can reduce 409 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (406) all_260_0_184 = 0 % 30.27/9.76 | (412) ~ (all_260_1_185 = 0) | ~ (all_260_2_186 = 0) % 30.27/9.76 | % 30.27/9.76 +-Applying beta-rule and splitting (412), into two cases. % 30.27/9.76 |-Branch one: % 30.27/9.76 | (413) ~ (all_260_1_185 = 0) % 30.27/9.76 | % 30.27/9.76 | Equations (407) can reduce 413 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 |-Branch two: % 30.27/9.76 | (407) all_260_1_185 = 0 % 30.27/9.76 | (416) ~ (all_260_2_186 = 0) % 30.27/9.76 | % 30.27/9.76 | Equations (408) can reduce 416 to: % 30.27/9.76 | (223) $false % 30.27/9.76 | % 30.27/9.76 |-The branch is then unsatisfiable % 30.27/9.76 % SZS output end Proof for theBenchmark % 30.27/9.76 % 30.27/9.76 9156ms %------------------------------------------------------------------------------