%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n023.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 : Fri Jul 15 01:07:53 EDT 2022 % Result : Theorem 6.63s 2.24s % Output : Proof 9.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 16 20:25:34 EDT 2022 % 0.13/0.34 % CPUTime : % 0.66/0.65 ____ _ % 0.66/0.65 ___ / __ \_____(_)___ ________ __________ % 0.66/0.65 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.66/0.65 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.66/0.65 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.66/0.65 % 0.66/0.65 A Theorem Prover for First-Order Logic % 0.66/0.65 (ePrincess v.1.0) % 0.66/0.65 % 0.66/0.65 (c) Philipp Rümmer, 2009-2015 % 0.66/0.65 (c) Peter Backeman, 2014-2015 % 0.66/0.65 (contributions by Angelo Brillout, Peter Baumgartner) % 0.66/0.65 Free software under GNU Lesser General Public License (LGPL). % 0.66/0.65 Bug reports to peter@backeman.se % 0.66/0.65 % 0.66/0.65 For more information, visit http://user.uu.se/~petba168/breu/ % 0.66/0.65 % 0.66/0.65 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.84/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.01/1.10 Prover 0: Preprocessing ... % 3.77/1.58 Prover 0: Constructing countermodel ... % 6.63/2.24 Prover 0: proved (1533ms) % 6.63/2.24 % 6.63/2.24 No countermodel exists, formula is valid % 6.63/2.24 % SZS status Theorem for theBenchmark % 6.63/2.24 % 6.63/2.24 Generating proof ... found it (size 23) % 9.12/2.83 % 9.12/2.83 % SZS output start Proof for theBenchmark % 9.12/2.83 Assumed formulas after preprocessing and simplification: % 9.12/2.83 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ( ~ (xc = xb) & isTerminating0(xR) & isLocallyConfluent0(xR) & sdtmndtasgtdt0(xa, xR, xc) & sdtmndtasgtdt0(xa, xR, xb) & aRewritingSystem0(xR) & aElement0(xc) & aElement0(xb) & aElement0(xa) & ~ sdtmndtasgtdt0(xc, xR, xb) & ~ sdtmndtasgtdt0(xb, xR, xc) & ~ sdtmndtplgtdt0(xc, xR, xb) & ~ sdtmndtplgtdt0(xb, xR, xc) & ~ aReductOfIn0(xc, xb, xR) & ~ aReductOfIn0(xb, xc, xR) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ sdtmndtplgtdt0(v17, xR, v14) | ~ sdtmndtplgtdt0(v16, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v17, v13, xR) | ~ aReductOfIn0(v16, v13, xR) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v18] : ? [v19] : ? [v20] : (sdtmndtasgtdt0(v15, xR, v18) & sdtmndtasgtdt0(v14, xR, v18) & aElement0(v18) & (v18 = v15 | (sdtmndtplgtdt0(v15, xR, v18) & (aReductOfIn0(v18, v15, xR) | (sdtmndtplgtdt0(v19, xR, v18) & aReductOfIn0(v19, v15, xR) & aElement0(v19))))) & (v18 = v14 | (sdtmndtplgtdt0(v14, xR, v18) & (aReductOfIn0(v18, v14, xR) | (sdtmndtplgtdt0(v20, xR, v18) & aReductOfIn0(v20, v14, xR) & aElement0(v20))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ aNormalFormOfIn0(v15, v13, v14) | ~ aReductOfIn0(v16, v15, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ isLocallyConfluent0(v13) | ~ aReductOfIn0(v16, v14, v13) | ~ aReductOfIn0(v15, v14, v13) | ~ aRewritingSystem0(v13) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ? [v17] : (sdtmndtasgtdt0(v16, v13, v17) & sdtmndtasgtdt0(v15, v13, v17) & aElement0(v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ isConfluent0(v13) | ~ sdtmndtasgtdt0(v14, v13, v16) | ~ sdtmndtasgtdt0(v14, v13, v15) | ~ aRewritingSystem0(v13) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ? [v17] : (sdtmndtasgtdt0(v16, v13, v17) & sdtmndtasgtdt0(v15, v13, v17) & aElement0(v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtasgtdt0(v15, v14, v16) | ~ sdtmndtasgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtasgtdt0(v13, v14, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtasgtdt0(v13, xR, v15) | ~ sdtmndtplgtdt0(v16, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtasgtdt0(v13, xR, v14) | ~ sdtmndtplgtdt0(v16, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v16, v14, v15) | ~ aReductOfIn0(v16, v13, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtplgtdt0(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v16, xR, v15) | ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v16, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v16, xR, v14) | ~ sdtmndtplgtdt0(v13, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v16, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v16, v13, xR) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v17] : ? [v18] : ? [v19] : (sdtmndtasgtdt0(v15, xR, v17) & sdtmndtasgtdt0(v14, xR, v17) & aElement0(v17) & (v17 = v15 | (sdtmndtplgtdt0(v15, xR, v17) & (aReductOfIn0(v17, v15, xR) | (sdtmndtplgtdt0(v18, xR, v17) & aReductOfIn0(v18, v15, xR) & aElement0(v18))))) & (v17 = v14 | (sdtmndtplgtdt0(v14, xR, v17) & (aReductOfIn0(v17, v14, xR) | (sdtmndtplgtdt0(v19, xR, v17) & aReductOfIn0(v19, v14, xR) & aElement0(v19))))))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ sdtmndtplgtdt0(v15, v14, v16) | ~ sdtmndtplgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v16) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtplgtdt0(v13, v14, v16)) & ! [v13] : ! [v14] : ! [v15] : (v15 = v13 | ~ sdtmndtasgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtplgtdt0(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ aNormalFormOfIn0(v15, v13, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v13) | sdtmndtasgtdt0(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ aNormalFormOfIn0(v15, v13, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v13) | aElement0(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ isTerminating0(v13) | ~ sdtmndtplgtdt0(v14, v13, v15) | ~ aRewritingSystem0(v13) | ~ aElement0(v15) | ~ aElement0(v14) | iLess0(v15, v14)) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v15) | ~ aElement0(v13) | aNormalFormOfIn0(v15, v13, v14) | ? [v16] : aReductOfIn0(v16, v15, v14)) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, xR, v15) | ~ sdtmndtasgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, xR, v15) | ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, xR, v14) | ~ sdtmndtplgtdt0(v13, xR, v15) | ~ iLess0(v13, xa) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtasgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v15, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v14, xR, v16) & sdtmndtasgtdt0(v13, xR, v16) & aElement0(v16) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))) & (v16 = v13 | (sdtmndtplgtdt0(v13, xR, v16) & (aReductOfIn0(v16, v13, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v13, xR) & aElement0(v17))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v15, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v14, xR, v16) & sdtmndtasgtdt0(v13, xR, v16) & aElement0(v16) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v14, xR) & aElement0(v17))))) & (v16 = v13 | (sdtmndtplgtdt0(v13, xR, v16) & (aReductOfIn0(v16, v13, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v13, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v15, xR, v14) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | iLess0(v14, v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v15, xR, v13) | ~ sdtmndtplgtdt0(v14, xR, v13) | ~ aReductOfIn0(v15, xb, xR) | ~ aReductOfIn0(v14, xc, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtasgtdt0(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v13, v14, v15) | ~ aRewritingSystem0(v14) | ~ aElement0(v15) | ~ aElement0(v13) | aReductOfIn0(v15, v13, v14) | ? [v16] : (sdtmndtplgtdt0(v16, v14, v15) & aReductOfIn0(v16, v13, v14) & aElement0(v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v13, xR, v15) | ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v13, xR, v15) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aReductOfIn0(v15, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ iLess0(v13, xa) | ~ aReductOfIn0(v15, v13, xR) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ! [v15] : ( ~ aReductOfIn0(v15, v13, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v15) | ~ aElement0(v13) | sdtmndtplgtdt0(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ aReductOfIn0(v15, v13, v14) | ~ aRewritingSystem0(v14) | ~ aElement0(v13) | aElement0(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ aReductOfIn0(v15, v13, xR) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v15) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v16] : ? [v17] : ? [v18] : (sdtmndtasgtdt0(v15, xR, v16) & sdtmndtasgtdt0(v14, xR, v16) & aElement0(v16) & (v16 = v15 | (sdtmndtplgtdt0(v15, xR, v16) & (aReductOfIn0(v16, v15, xR) | (sdtmndtplgtdt0(v17, xR, v16) & aReductOfIn0(v17, v15, xR) & aElement0(v17))))) & (v16 = v14 | (sdtmndtplgtdt0(v14, xR, v16) & (aReductOfIn0(v16, v14, xR) | (sdtmndtplgtdt0(v18, xR, v16) & aReductOfIn0(v18, v14, xR) & aElement0(v18))))))) & ! [v13] : ! [v14] : ( ~ isTerminating0(v13) | ~ aRewritingSystem0(v13) | ~ aElement0(v14) | ? [v15] : aNormalFormOfIn0(v15, v14, v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtasgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v14, xR) & aElement0(v17))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v13, xR) & aElement0(v16))))))) & ! [v13] : ! [v14] : ( ~ sdtmndtasgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v14, xR) & aElement0(v16))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v13, xR) & aElement0(v17))))))) & ! [v13] : ! [v14] : ( ~ sdtmndtasgtdt0(xc, xR, v13) | ~ sdtmndtplgtdt0(v14, xR, v13) | ~ aReductOfIn0(v14, xb, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtasgtdt0(xb, xR, v13) | ~ sdtmndtplgtdt0(v14, xR, v13) | ~ aReductOfIn0(v14, xc, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v14, xR, v13) | ~ sdtmndtplgtdt0(xc, xR, v13) | ~ aReductOfIn0(v14, xb, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v14, xR, v13) | ~ sdtmndtplgtdt0(xb, xR, v13) | ~ aReductOfIn0(v14, xc, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v14, xR, v13) | ~ aReductOfIn0(v14, xc, xR) | ~ aReductOfIn0(v13, xb, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v14, xR, v13) | ~ aReductOfIn0(v14, xb, xR) | ~ aReductOfIn0(v13, xc, xR) | ~ aElement0(v14) | ~ aElement0(v13)) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v14, xR) & aElement0(v17))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v13, xR) & aElement0(v16))))))) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v13, xR, v14) | ~ iLess0(v13, xa) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v14, xR) & aElement0(v16))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v13, xR) & aElement0(v17))))))) & ! [v13] : ! [v14] : ( ~ sdtmndtplgtdt0(v13, xR, v14) | ~ aElement0(v14) | ~ aElement0(v13) | iLess0(v14, v13)) & ! [v13] : ! [v14] : ( ~ iLess0(v13, xa) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v14, xR) & aElement0(v17))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v13, xR) & aElement0(v16))))))) & ! [v13] : ! [v14] : ( ~ iLess0(v13, xa) | ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v14) | ~ aElement0(v13) | ? [v15] : ? [v16] : ? [v17] : (sdtmndtasgtdt0(v14, xR, v15) & sdtmndtasgtdt0(v13, xR, v15) & aElement0(v15) & (v15 = v14 | (sdtmndtplgtdt0(v14, xR, v15) & (aReductOfIn0(v15, v14, xR) | (sdtmndtplgtdt0(v16, xR, v15) & aReductOfIn0(v16, v14, xR) & aElement0(v16))))) & (v15 = v13 | (sdtmndtplgtdt0(v13, xR, v15) & (aReductOfIn0(v15, v13, xR) | (sdtmndtplgtdt0(v17, xR, v15) & aReductOfIn0(v17, v13, xR) & aElement0(v17))))))) & ! [v13] : ! [v14] : ( ~ aReductOfIn0(v14, v13, xR) | ~ aElement0(v14) | ~ aElement0(v13) | iLess0(v14, v13)) & ! [v13] : ! [v14] : ( ~ aRewritingSystem0(v14) | ~ aElement0(v13) | sdtmndtasgtdt0(v13, v14, v13)) & ! [v13] : ( ~ sdtmndtasgtdt0(xc, xR, v13) | ~ sdtmndtasgtdt0(xb, xR, v13) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtasgtdt0(xc, xR, v13) | ~ sdtmndtplgtdt0(xb, xR, v13) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtasgtdt0(xc, xR, v13) | ~ aReductOfIn0(v13, xb, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtasgtdt0(xb, xR, v13) | ~ sdtmndtplgtdt0(xc, xR, v13) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtasgtdt0(xb, xR, v13) | ~ aReductOfIn0(v13, xc, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtplgtdt0(v13, xR, xc) | ~ aReductOfIn0(v13, xb, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtplgtdt0(v13, xR, xb) | ~ aReductOfIn0(v13, xc, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtplgtdt0(xc, xR, v13) | ~ sdtmndtplgtdt0(xb, xR, v13) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtplgtdt0(xc, xR, v13) | ~ aReductOfIn0(v13, xb, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ sdtmndtplgtdt0(xb, xR, v13) | ~ aReductOfIn0(v13, xc, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ iLess0(v13, xa) | ~ aElement0(v13) | ? [v14] : ? [v15] : ? [v16] : (sdtmndtasgtdt0(v13, xR, v14) & aElement0(v14) & (v14 = v13 | (sdtmndtplgtdt0(v13, xR, v14) & (aReductOfIn0(v14, v13, xR) | (sdtmndtplgtdt0(v16, xR, v14) & aReductOfIn0(v16, v13, xR) & aElement0(v16))))) & (v14 = v13 | (sdtmndtplgtdt0(v13, xR, v14) & (aReductOfIn0(v14, v13, xR) | (sdtmndtplgtdt0(v15, xR, v14) & aReductOfIn0(v15, v13, xR) & aElement0(v15))))))) & ! [v13] : ( ~ aReductOfIn0(v13, xc, xR) | ~ aReductOfIn0(v13, xb, xR) | ~ aElement0(v13)) & ! [v13] : ( ~ aRewritingSystem0(v13) | isTerminating0(v13) | ? [v14] : ? [v15] : (sdtmndtplgtdt0(v14, v13, v15) & aElement0(v15) & aElement0(v14) & ~ iLess0(v15, v14))) & ! [v13] : ( ~ aRewritingSystem0(v13) | isLocallyConfluent0(v13) | ? [v14] : ? [v15] : ? [v16] : (aReductOfIn0(v16, v14, v13) & aReductOfIn0(v15, v14, v13) & aElement0(v16) & aElement0(v15) & aElement0(v14) & ! [v17] : ( ~ sdtmndtasgtdt0(v16, v13, v17) | ~ sdtmndtasgtdt0(v15, v13, v17) | ~ aElement0(v17)))) & ! [v13] : ( ~ aRewritingSystem0(v13) | isConfluent0(v13) | ? [v14] : ? [v15] : ? [v16] : (sdtmndtasgtdt0(v14, v13, v16) & sdtmndtasgtdt0(v14, v13, v15) & aElement0(v16) & aElement0(v15) & aElement0(v14) & ! [v17] : ( ~ sdtmndtasgtdt0(v16, v13, v17) | ~ sdtmndtasgtdt0(v15, v13, v17) | ~ aElement0(v17)))) & (xc = xa | (sdtmndtplgtdt0(xa, xR, xc) & (aReductOfIn0(xc, xa, xR) | (sdtmndtplgtdt0(v0, xR, xc) & aReductOfIn0(v0, xa, xR) & aElement0(v0))))) & (xb = xa | (sdtmndtplgtdt0(xa, xR, xb) & (aReductOfIn0(xb, xa, xR) | (sdtmndtplgtdt0(v1, xR, xb) & aReductOfIn0(v1, xa, xR) & aElement0(v1))))) & ((aNormalFormOfIn0(v5, v4, xR) & sdtmndtasgtdt0(v4, xR, v5) & sdtmndtasgtdt0(v3, xR, v4) & sdtmndtasgtdt0(v3, xR, xc) & sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v2, xR, xb) & sdtmndtasgtdt0(xc, xR, v5) & sdtmndtasgtdt0(xb, xR, v5) & aReductOfIn0(v3, xa, xR) & aReductOfIn0(v2, xa, xR) & aElement0(v5) & aElement0(v4) & aElement0(v3) & aElement0(v2) & ! [v13] : ~ aReductOfIn0(v13, v5, xR) & (v5 = v4 | (sdtmndtplgtdt0(v4, xR, v5) & (aReductOfIn0(v5, v4, xR) | (sdtmndtplgtdt0(v8, xR, v5) & aReductOfIn0(v8, v4, xR) & aElement0(v8))))) & (v5 = xc | (sdtmndtplgtdt0(xc, xR, v5) & (aReductOfIn0(v5, xc, xR) | (sdtmndtplgtdt0(v6, xR, v5) & aReductOfIn0(v6, xc, xR) & aElement0(v6))))) & (v5 = xb | (sdtmndtplgtdt0(xb, xR, v5) & (aReductOfIn0(v5, xb, xR) | (sdtmndtplgtdt0(v7, xR, v5) & aReductOfIn0(v7, xb, xR) & aElement0(v7))))) & (v4 = v3 | (sdtmndtplgtdt0(v3, xR, v4) & (aReductOfIn0(v4, v3, xR) | (sdtmndtplgtdt0(v9, xR, v4) & aReductOfIn0(v9, v3, xR) & aElement0(v9))))) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v10, xR, v4) & aReductOfIn0(v10, v2, xR) & aElement0(v10))))) & (v3 = xc | (sdtmndtplgtdt0(v3, xR, xc) & (aReductOfIn0(xc, v3, xR) | (sdtmndtplgtdt0(v11, xR, xc) & aReductOfIn0(v11, v3, xR) & aElement0(v11))))) & (v2 = xb | (sdtmndtplgtdt0(v2, xR, xb) & (aReductOfIn0(xb, v2, xR) | (sdtmndtplgtdt0(v12, xR, xb) & aReductOfIn0(v12, v2, xR) & aElement0(v12)))))) | ( ~ sdtmndtplgtdt0(xa, xR, xc) & ~ aReductOfIn0(xc, xa, xR) & ! [v13] : ( ~ sdtmndtplgtdt0(v13, xR, xc) | ~ aReductOfIn0(v13, xa, xR) | ~ aElement0(v13))) | ( ~ sdtmndtplgtdt0(xa, xR, xb) & ~ aReductOfIn0(xb, xa, xR) & ! [v13] : ( ~ sdtmndtplgtdt0(v13, xR, xb) | ~ aReductOfIn0(v13, xa, xR) | ~ aElement0(v13))))) % 9.59/2.89 | 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 yields: % 9.59/2.89 | (1) ~ (xc = xb) & isTerminating0(xR) & isLocallyConfluent0(xR) & sdtmndtasgtdt0(xa, xR, xc) & sdtmndtasgtdt0(xa, xR, xb) & aRewritingSystem0(xR) & aElement0(xc) & aElement0(xb) & aElement0(xa) & ~ sdtmndtasgtdt0(xc, xR, xb) & ~ sdtmndtasgtdt0(xb, xR, xc) & ~ sdtmndtplgtdt0(xc, xR, xb) & ~ sdtmndtplgtdt0(xb, xR, xc) & ~ aReductOfIn0(xc, xb, xR) & ~ aReductOfIn0(xb, xc, xR) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ sdtmndtplgtdt0(v4, xR, v1) | ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v4, v0, xR) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v4) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : (sdtmndtasgtdt0(v2, xR, v5) & sdtmndtasgtdt0(v1, xR, v5) & aElement0(v5) & (v5 = v2 | (sdtmndtplgtdt0(v2, xR, v5) & (aReductOfIn0(v5, v2, xR) | (sdtmndtplgtdt0(v6, xR, v5) & aReductOfIn0(v6, v2, xR) & aElement0(v6))))) & (v5 = v1 | (sdtmndtplgtdt0(v1, xR, v5) & (aReductOfIn0(v5, v1, xR) | (sdtmndtplgtdt0(v7, xR, v5) & aReductOfIn0(v7, v1, xR) & aElement0(v7))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aReductOfIn0(v3, v2, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isLocallyConfluent0(v0) | ~ aReductOfIn0(v3, v1, v0) | ~ aReductOfIn0(v2, v1, v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isConfluent0(v0) | ~ sdtmndtasgtdt0(v1, v0, v3) | ~ sdtmndtasgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v2, v1, v3) | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v3, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, v1, v2) | ~ aReductOfIn0(v3, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v1) | ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v2, v1, v3) | ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ isTerminating0(v0) | ~ sdtmndtplgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v2) | ~ aElement0(v1) | iLess0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aNormalFormOfIn0(v2, v0, v1) | ? [v3] : aReductOfIn0(v3, v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v1, xR, v3) & sdtmndtasgtdt0(v0, xR, v3) & aElement0(v3) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))) & (v3 = v0 | (sdtmndtplgtdt0(v0, xR, v3) & (aReductOfIn0(v3, v0, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v1, xR, v3) & sdtmndtasgtdt0(v0, xR, v3) & aElement0(v3) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v3 = v0 | (sdtmndtplgtdt0(v0, xR, v3) & (aReductOfIn0(v3, v0, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v0, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v2, xb, xR) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aReductOfIn0(v2, v0, v1) | ? [v3] : (sdtmndtplgtdt0(v3, v1, v2) & aReductOfIn0(v3, v0, v1) & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) & ! [v0] : ! [v1] : ( ~ isTerminating0(v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v1) | ? [v2] : aNormalFormOfIn0(v2, v1, v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) & ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) & ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) & ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) & ! [v0] : ! [v1] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) & ! [v0] : ! [v1] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) & ! [v0] : ! [v1] : ( ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) & ! [v0] : ! [v1] : ( ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtplgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ iLess0(v0, xa) | ~ aElement0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v0, xR, v1) & aElement0(v1) & (v1 = v0 | (sdtmndtplgtdt0(v0, xR, v1) & (aReductOfIn0(v1, v0, xR) | (sdtmndtplgtdt0(v3, xR, v1) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))) & (v1 = v0 | (sdtmndtplgtdt0(v0, xR, v1) & (aReductOfIn0(v1, v0, xR) | (sdtmndtplgtdt0(v2, xR, v1) & aReductOfIn0(v2, v0, xR) & aElement0(v2))))))) & ! [v0] : ( ~ aReductOfIn0(v0, xc, xR) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) & ! [v0] : ( ~ aRewritingSystem0(v0) | isTerminating0(v0) | ? [v1] : ? [v2] : (sdtmndtplgtdt0(v1, v0, v2) & aElement0(v2) & aElement0(v1) & ~ iLess0(v2, v1))) & ! [v0] : ( ~ aRewritingSystem0(v0) | isLocallyConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (aReductOfIn0(v3, v1, v0) & aReductOfIn0(v2, v1, v0) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) & ! [v0] : ( ~ aRewritingSystem0(v0) | isConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v1, v0, v3) & sdtmndtasgtdt0(v1, v0, v2) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) & (xc = xa | (sdtmndtplgtdt0(xa, xR, xc) & (aReductOfIn0(xc, xa, xR) | (sdtmndtplgtdt0(all_0_12_12, xR, xc) & aReductOfIn0(all_0_12_12, xa, xR) & aElement0(all_0_12_12))))) & (xb = xa | (sdtmndtplgtdt0(xa, xR, xb) & (aReductOfIn0(xb, xa, xR) | (sdtmndtplgtdt0(all_0_11_11, xR, xb) & aReductOfIn0(all_0_11_11, xa, xR) & aElement0(all_0_11_11))))) & ((aNormalFormOfIn0(all_0_7_7, all_0_8_8, xR) & sdtmndtasgtdt0(all_0_8_8, xR, all_0_7_7) & sdtmndtasgtdt0(all_0_9_9, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_9_9, xR, xc) & sdtmndtasgtdt0(all_0_10_10, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_10_10, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_7_7) & sdtmndtasgtdt0(xb, xR, all_0_7_7) & aReductOfIn0(all_0_9_9, xa, xR) & aReductOfIn0(all_0_10_10, xa, xR) & aElement0(all_0_7_7) & aElement0(all_0_8_8) & aElement0(all_0_9_9) & aElement0(all_0_10_10) & ! [v0] : ~ aReductOfIn0(v0, all_0_7_7, xR) & (all_0_7_7 = all_0_8_8 | (sdtmndtplgtdt0(all_0_8_8, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, all_0_8_8, xR) | (sdtmndtplgtdt0(all_0_4_4, xR, all_0_7_7) & aReductOfIn0(all_0_4_4, all_0_8_8, xR) & aElement0(all_0_4_4))))) & (all_0_7_7 = xc | (sdtmndtplgtdt0(xc, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xc, xR) | (sdtmndtplgtdt0(all_0_6_6, xR, all_0_7_7) & aReductOfIn0(all_0_6_6, xc, xR) & aElement0(all_0_6_6))))) & (all_0_7_7 = xb | (sdtmndtplgtdt0(xb, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xb, xR) | (sdtmndtplgtdt0(all_0_5_5, xR, all_0_7_7) & aReductOfIn0(all_0_5_5, xb, xR) & aElement0(all_0_5_5))))) & (all_0_8_8 = all_0_9_9 | (sdtmndtplgtdt0(all_0_9_9, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_3_3, xR, all_0_8_8) & aReductOfIn0(all_0_3_3, all_0_9_9, xR) & aElement0(all_0_3_3))))) & (all_0_8_8 = all_0_10_10 | (sdtmndtplgtdt0(all_0_10_10, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_2_2, xR, all_0_8_8) & aReductOfIn0(all_0_2_2, all_0_10_10, xR) & aElement0(all_0_2_2))))) & (all_0_9_9 = xc | (sdtmndtplgtdt0(all_0_9_9, xR, xc) & (aReductOfIn0(xc, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_1_1, xR, xc) & aReductOfIn0(all_0_1_1, all_0_9_9, xR) & aElement0(all_0_1_1))))) & (all_0_10_10 = xb | (sdtmndtplgtdt0(all_0_10_10, xR, xb) & (aReductOfIn0(xb, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_0_0, xR, xb) & aReductOfIn0(all_0_0_0, all_0_10_10, xR) & aElement0(all_0_0_0)))))) | ( ~ sdtmndtplgtdt0(xa, xR, xc) & ~ aReductOfIn0(xc, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0))) | ( ~ sdtmndtplgtdt0(xa, xR, xb) & ~ aReductOfIn0(xb, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0)))) % 9.80/2.93 | % 9.80/2.93 | Applying alpha-rule on (1) yields: % 9.80/2.93 | (2) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) % 9.80/2.93 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.93 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 9.80/2.93 | (5) ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) % 9.80/2.93 | (6) ! [v0] : ( ~ aRewritingSystem0(v0) | isLocallyConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (aReductOfIn0(v3, v1, v0) & aReductOfIn0(v2, v1, v0) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) % 9.80/2.93 | (7) ~ aReductOfIn0(xc, xb, xR) % 9.80/2.93 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v2, v1, v3) | ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v3)) % 9.80/2.93 | (9) ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aElement0(v0)) % 9.80/2.93 | (10) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.93 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aReductOfIn0(v2, v0, v1) | ? [v3] : (sdtmndtplgtdt0(v3, v1, v2) & aReductOfIn0(v3, v0, v1) & aElement0(v3))) % 9.80/2.93 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.93 | (13) aElement0(xb) % 9.80/2.93 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) % 9.80/2.93 | (15) xc = xa | (sdtmndtplgtdt0(xa, xR, xc) & (aReductOfIn0(xc, xa, xR) | (sdtmndtplgtdt0(all_0_12_12, xR, xc) & aReductOfIn0(all_0_12_12, xa, xR) & aElement0(all_0_12_12)))) % 9.80/2.93 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) % 9.80/2.93 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.93 | (18) xb = xa | (sdtmndtplgtdt0(xa, xR, xb) & (aReductOfIn0(xb, xa, xR) | (sdtmndtplgtdt0(all_0_11_11, xR, xb) & aReductOfIn0(all_0_11_11, xa, xR) & aElement0(all_0_11_11)))) % 9.80/2.93 | (19) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) % 9.80/2.93 | (20) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.94 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v1) | ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.94 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.94 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aNormalFormOfIn0(v2, v0, v1) | ? [v3] : aReductOfIn0(v3, v2, v1)) % 9.80/2.94 | (24) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) % 9.80/2.94 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v3, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.94 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aReductOfIn0(v3, v2, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0)) % 9.80/2.94 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v2, v1, v3) | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v3)) % 9.80/2.94 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.94 | (29) ! [v0] : ( ~ iLess0(v0, xa) | ~ aElement0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v0, xR, v1) & aElement0(v1) & (v1 = v0 | (sdtmndtplgtdt0(v0, xR, v1) & (aReductOfIn0(v1, v0, xR) | (sdtmndtplgtdt0(v3, xR, v1) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))) & (v1 = v0 | (sdtmndtplgtdt0(v0, xR, v1) & (aReductOfIn0(v1, v0, xR) | (sdtmndtplgtdt0(v2, xR, v1) & aReductOfIn0(v2, v0, xR) & aElement0(v2))))))) % 9.80/2.94 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) % 9.80/2.94 | (31) ! [v0] : ! [v1] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) % 9.80/2.94 | (32) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.94 | (33) ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) % 9.80/2.94 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.94 | (35) ! [v0] : ( ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) % 9.80/2.94 | (36) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.94 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) % 9.80/2.94 | (38) ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aElement0(v0)) % 9.80/2.94 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isConfluent0(v0) | ~ sdtmndtasgtdt0(v1, v0, v3) | ~ sdtmndtasgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) % 9.80/2.94 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isLocallyConfluent0(v0) | ~ aReductOfIn0(v3, v1, v0) | ~ aReductOfIn0(v2, v1, v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) % 9.80/2.94 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ sdtmndtplgtdt0(v4, xR, v1) | ~ sdtmndtplgtdt0(v3, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v4, v0, xR) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v4) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : (sdtmndtasgtdt0(v2, xR, v5) & sdtmndtasgtdt0(v1, xR, v5) & aElement0(v5) & (v5 = v2 | (sdtmndtplgtdt0(v2, xR, v5) & (aReductOfIn0(v5, v2, xR) | (sdtmndtplgtdt0(v6, xR, v5) & aReductOfIn0(v6, v2, xR) & aElement0(v6))))) & (v5 = v1 | (sdtmndtplgtdt0(v1, xR, v5) & (aReductOfIn0(v5, v1, xR) | (sdtmndtplgtdt0(v7, xR, v5) & aReductOfIn0(v7, v1, xR) & aElement0(v7))))))) % 9.80/2.95 | (42) ! [v0] : ! [v1] : ! [v2] : ( ~ isTerminating0(v0) | ~ sdtmndtplgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v2) | ~ aElement0(v1) | iLess0(v2, v1)) % 9.80/2.95 | (43) sdtmndtasgtdt0(xa, xR, xc) % 9.80/2.95 | (44) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.95 | (45) ! [v0] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aElement0(v0)) % 9.80/2.95 | (46) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) % 9.80/2.95 | (47) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v1, xR, v3) & sdtmndtasgtdt0(v0, xR, v3) & aElement0(v3) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v3 = v0 | (sdtmndtplgtdt0(v0, xR, v3) & (aReductOfIn0(v3, v0, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v0, xR) & aElement0(v5))))))) % 9.80/2.95 | (48) isLocallyConfluent0(xR) % 9.80/2.95 | (49) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ sdtmndtplgtdt0(xc, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.95 | (50) ! [v0] : ( ~ aRewritingSystem0(v0) | isTerminating0(v0) | ? [v1] : ? [v2] : (sdtmndtplgtdt0(v1, v0, v2) & aElement0(v2) & aElement0(v1) & ~ iLess0(v2, v1))) % 9.80/2.95 | (51) ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, xR) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.95 | (52) ~ sdtmndtplgtdt0(xb, xR, xc) % 9.80/2.95 | (53) ! [v0] : ! [v1] : ( ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v0)) % 9.80/2.95 | (54) ! [v0] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) % 9.80/2.95 | (55) sdtmndtasgtdt0(xa, xR, xb) % 9.80/2.95 | (56) aElement0(xc) % 9.80/2.95 | (57) ~ sdtmndtasgtdt0(xb, xR, xc) % 9.80/2.95 | (58) ! [v0] : ( ~ aRewritingSystem0(v0) | isConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v1, v0, v3) & sdtmndtasgtdt0(v1, v0, v2) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) % 9.80/2.95 | (59) ! [v0] : ! [v1] : ( ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | iLess0(v1, v0)) % 9.80/2.95 | (60) ! [v0] : ( ~ sdtmndtplgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aElement0(v0)) % 9.80/2.95 | (61) ~ (xc = xb) % 9.80/2.95 | (62) ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v1, xR) & aElement0(v4))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v0, xR) & aElement0(v3))))))) % 9.80/2.95 | (63) ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) % 9.80/2.95 | (64) ! [v0] : ! [v1] : ( ~ isTerminating0(v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v1) | ? [v2] : aNormalFormOfIn0(v2, v1, v0)) % 9.80/2.95 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v3, v0, xR) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v4] : ? [v5] : ? [v6] : (sdtmndtasgtdt0(v2, xR, v4) & sdtmndtasgtdt0(v1, xR, v4) & aElement0(v4) & (v4 = v2 | (sdtmndtplgtdt0(v2, xR, v4) & (aReductOfIn0(v4, v2, xR) | (sdtmndtplgtdt0(v5, xR, v4) & aReductOfIn0(v5, v2, xR) & aElement0(v5))))) & (v4 = v1 | (sdtmndtplgtdt0(v1, xR, v4) & (aReductOfIn0(v4, v1, xR) | (sdtmndtplgtdt0(v6, xR, v4) & aReductOfIn0(v6, v1, xR) & aElement0(v6))))))) % 9.80/2.95 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.95 | (67) aElement0(xa) % 9.80/2.95 | (68) ! [v0] : ( ~ aReductOfIn0(v0, xc, xR) | ~ aReductOfIn0(v0, xb, xR) | ~ aElement0(v0)) % 9.80/2.95 | (69) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 9.80/2.95 | (70) ~ aReductOfIn0(xb, xc, xR) % 9.80/2.95 | (71) ! [v0] : ! [v1] : ( ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v0, xR, v2) & aElement0(v2) & (v2 = v1 | (sdtmndtplgtdt0(v1, xR, v2) & (aReductOfIn0(v2, v1, xR) | (sdtmndtplgtdt0(v3, xR, v2) & aReductOfIn0(v3, v1, xR) & aElement0(v3))))) & (v2 = v0 | (sdtmndtplgtdt0(v0, xR, v2) & (aReductOfIn0(v2, v0, xR) | (sdtmndtplgtdt0(v4, xR, v2) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) % 9.80/2.95 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, v1, v2) | ~ aReductOfIn0(v3, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 9.80/2.95 | (73) aRewritingSystem0(xR) % 9.80/2.95 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v2) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v1, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.95 | (75) ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) % 9.80/2.95 | (76) ~ sdtmndtasgtdt0(xc, xR, xb) % 9.80/2.95 | (77) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v1) | ~ iLess0(v0, xa) | ~ aReductOfIn0(v2, v0, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v1, xR, v3) & sdtmndtasgtdt0(v0, xR, v3) & aElement0(v3) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))) & (v3 = v0 | (sdtmndtplgtdt0(v0, xR, v3) & (aReductOfIn0(v3, v0, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v0, xR) & aElement0(v4))))))) % 9.80/2.95 | (78) ! [v0] : ! [v1] : ( ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.95 | (79) (aNormalFormOfIn0(all_0_7_7, all_0_8_8, xR) & sdtmndtasgtdt0(all_0_8_8, xR, all_0_7_7) & sdtmndtasgtdt0(all_0_9_9, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_9_9, xR, xc) & sdtmndtasgtdt0(all_0_10_10, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_10_10, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_7_7) & sdtmndtasgtdt0(xb, xR, all_0_7_7) & aReductOfIn0(all_0_9_9, xa, xR) & aReductOfIn0(all_0_10_10, xa, xR) & aElement0(all_0_7_7) & aElement0(all_0_8_8) & aElement0(all_0_9_9) & aElement0(all_0_10_10) & ! [v0] : ~ aReductOfIn0(v0, all_0_7_7, xR) & (all_0_7_7 = all_0_8_8 | (sdtmndtplgtdt0(all_0_8_8, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, all_0_8_8, xR) | (sdtmndtplgtdt0(all_0_4_4, xR, all_0_7_7) & aReductOfIn0(all_0_4_4, all_0_8_8, xR) & aElement0(all_0_4_4))))) & (all_0_7_7 = xc | (sdtmndtplgtdt0(xc, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xc, xR) | (sdtmndtplgtdt0(all_0_6_6, xR, all_0_7_7) & aReductOfIn0(all_0_6_6, xc, xR) & aElement0(all_0_6_6))))) & (all_0_7_7 = xb | (sdtmndtplgtdt0(xb, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xb, xR) | (sdtmndtplgtdt0(all_0_5_5, xR, all_0_7_7) & aReductOfIn0(all_0_5_5, xb, xR) & aElement0(all_0_5_5))))) & (all_0_8_8 = all_0_9_9 | (sdtmndtplgtdt0(all_0_9_9, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_3_3, xR, all_0_8_8) & aReductOfIn0(all_0_3_3, all_0_9_9, xR) & aElement0(all_0_3_3))))) & (all_0_8_8 = all_0_10_10 | (sdtmndtplgtdt0(all_0_10_10, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_2_2, xR, all_0_8_8) & aReductOfIn0(all_0_2_2, all_0_10_10, xR) & aElement0(all_0_2_2))))) & (all_0_9_9 = xc | (sdtmndtplgtdt0(all_0_9_9, xR, xc) & (aReductOfIn0(xc, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_1_1, xR, xc) & aReductOfIn0(all_0_1_1, all_0_9_9, xR) & aElement0(all_0_1_1))))) & (all_0_10_10 = xb | (sdtmndtplgtdt0(all_0_10_10, xR, xb) & (aReductOfIn0(xb, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_0_0, xR, xb) & aReductOfIn0(all_0_0_0, all_0_10_10, xR) & aElement0(all_0_0_0)))))) | ( ~ sdtmndtplgtdt0(xa, xR, xc) & ~ aReductOfIn0(xc, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0))) | ( ~ sdtmndtplgtdt0(xa, xR, xb) & ~ aReductOfIn0(xb, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0))) % 9.80/2.96 | (80) ~ sdtmndtplgtdt0(xc, xR, xb) % 9.80/2.96 | (81) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v2, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v2, xb, xR) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.96 | (82) ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xb, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.96 | (83) ! [v0] : ( ~ sdtmndtplgtdt0(xb, xR, v0) | ~ aReductOfIn0(v0, xc, xR) | ~ aElement0(v0)) % 9.80/2.96 | (84) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, xR, v2) | ~ sdtmndtplgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3) & (v3 = v2 | (sdtmndtplgtdt0(v2, xR, v3) & (aReductOfIn0(v3, v2, xR) | (sdtmndtplgtdt0(v4, xR, v3) & aReductOfIn0(v4, v2, xR) & aElement0(v4))))) & (v3 = v1 | (sdtmndtplgtdt0(v1, xR, v3) & (aReductOfIn0(v3, v1, xR) | (sdtmndtplgtdt0(v5, xR, v3) & aReductOfIn0(v5, v1, xR) & aElement0(v5))))))) % 9.80/2.96 | (85) isTerminating0(xR) % 9.80/2.96 | (86) ! [v0] : ! [v1] : ( ~ sdtmndtasgtdt0(xb, xR, v0) | ~ sdtmndtplgtdt0(v1, xR, v0) | ~ aReductOfIn0(v1, xc, xR) | ~ aElement0(v1) | ~ aElement0(v0)) % 9.80/2.96 | % 9.80/2.96 +-Applying beta-rule and splitting (15), into two cases. % 9.80/2.96 |-Branch one: % 9.80/2.96 | (87) xc = xa % 9.80/2.96 | % 9.80/2.96 | From (87) and (76) follows: % 9.80/2.96 | (88) ~ sdtmndtasgtdt0(xa, xR, xb) % 9.80/2.96 | % 9.80/2.96 | Using (55) and (88) yields: % 9.80/2.96 | (89) $false % 9.80/2.96 | % 9.80/2.96 |-The branch is then unsatisfiable % 9.80/2.96 |-Branch two: % 9.80/2.96 | (90) ~ (xc = xa) % 9.80/2.96 | (91) sdtmndtplgtdt0(xa, xR, xc) & (aReductOfIn0(xc, xa, xR) | (sdtmndtplgtdt0(all_0_12_12, xR, xc) & aReductOfIn0(all_0_12_12, xa, xR) & aElement0(all_0_12_12))) % 9.80/2.96 | % 9.80/2.96 | Applying alpha-rule on (91) yields: % 9.80/2.96 | (92) sdtmndtplgtdt0(xa, xR, xc) % 9.80/2.96 | (93) aReductOfIn0(xc, xa, xR) | (sdtmndtplgtdt0(all_0_12_12, xR, xc) & aReductOfIn0(all_0_12_12, xa, xR) & aElement0(all_0_12_12)) % 9.80/2.96 | % 9.80/2.96 +-Applying beta-rule and splitting (18), into two cases. % 9.80/2.96 |-Branch one: % 9.80/2.96 | (94) xb = xa % 9.80/2.96 | % 9.80/2.96 | From (94) and (57) follows: % 9.80/2.96 | (95) ~ sdtmndtasgtdt0(xa, xR, xc) % 9.80/2.96 | % 9.80/2.96 | Using (43) and (95) yields: % 9.80/2.96 | (89) $false % 9.80/2.96 | % 9.80/2.96 |-The branch is then unsatisfiable % 9.80/2.96 |-Branch two: % 9.80/2.96 | (97) ~ (xb = xa) % 9.80/2.96 | (98) sdtmndtplgtdt0(xa, xR, xb) & (aReductOfIn0(xb, xa, xR) | (sdtmndtplgtdt0(all_0_11_11, xR, xb) & aReductOfIn0(all_0_11_11, xa, xR) & aElement0(all_0_11_11))) % 9.80/2.96 | % 9.80/2.96 | Applying alpha-rule on (98) yields: % 9.80/2.96 | (99) sdtmndtplgtdt0(xa, xR, xb) % 9.80/2.96 | (100) aReductOfIn0(xb, xa, xR) | (sdtmndtplgtdt0(all_0_11_11, xR, xb) & aReductOfIn0(all_0_11_11, xa, xR) & aElement0(all_0_11_11)) % 9.80/2.96 | % 9.80/2.96 +-Applying beta-rule and splitting (79), into two cases. % 9.80/2.96 |-Branch one: % 9.80/2.96 | (101) (aNormalFormOfIn0(all_0_7_7, all_0_8_8, xR) & sdtmndtasgtdt0(all_0_8_8, xR, all_0_7_7) & sdtmndtasgtdt0(all_0_9_9, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_9_9, xR, xc) & sdtmndtasgtdt0(all_0_10_10, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_10_10, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_7_7) & sdtmndtasgtdt0(xb, xR, all_0_7_7) & aReductOfIn0(all_0_9_9, xa, xR) & aReductOfIn0(all_0_10_10, xa, xR) & aElement0(all_0_7_7) & aElement0(all_0_8_8) & aElement0(all_0_9_9) & aElement0(all_0_10_10) & ! [v0] : ~ aReductOfIn0(v0, all_0_7_7, xR) & (all_0_7_7 = all_0_8_8 | (sdtmndtplgtdt0(all_0_8_8, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, all_0_8_8, xR) | (sdtmndtplgtdt0(all_0_4_4, xR, all_0_7_7) & aReductOfIn0(all_0_4_4, all_0_8_8, xR) & aElement0(all_0_4_4))))) & (all_0_7_7 = xc | (sdtmndtplgtdt0(xc, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xc, xR) | (sdtmndtplgtdt0(all_0_6_6, xR, all_0_7_7) & aReductOfIn0(all_0_6_6, xc, xR) & aElement0(all_0_6_6))))) & (all_0_7_7 = xb | (sdtmndtplgtdt0(xb, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xb, xR) | (sdtmndtplgtdt0(all_0_5_5, xR, all_0_7_7) & aReductOfIn0(all_0_5_5, xb, xR) & aElement0(all_0_5_5))))) & (all_0_8_8 = all_0_9_9 | (sdtmndtplgtdt0(all_0_9_9, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_3_3, xR, all_0_8_8) & aReductOfIn0(all_0_3_3, all_0_9_9, xR) & aElement0(all_0_3_3))))) & (all_0_8_8 = all_0_10_10 | (sdtmndtplgtdt0(all_0_10_10, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_2_2, xR, all_0_8_8) & aReductOfIn0(all_0_2_2, all_0_10_10, xR) & aElement0(all_0_2_2))))) & (all_0_9_9 = xc | (sdtmndtplgtdt0(all_0_9_9, xR, xc) & (aReductOfIn0(xc, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_1_1, xR, xc) & aReductOfIn0(all_0_1_1, all_0_9_9, xR) & aElement0(all_0_1_1))))) & (all_0_10_10 = xb | (sdtmndtplgtdt0(all_0_10_10, xR, xb) & (aReductOfIn0(xb, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_0_0, xR, xb) & aReductOfIn0(all_0_0_0, all_0_10_10, xR) & aElement0(all_0_0_0)))))) | ( ~ sdtmndtplgtdt0(xa, xR, xc) & ~ aReductOfIn0(xc, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0))) % 9.80/2.96 | % 9.80/2.96 +-Applying beta-rule and splitting (101), into two cases. % 9.80/2.96 |-Branch one: % 9.80/2.96 | (102) aNormalFormOfIn0(all_0_7_7, all_0_8_8, xR) & sdtmndtasgtdt0(all_0_8_8, xR, all_0_7_7) & sdtmndtasgtdt0(all_0_9_9, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_9_9, xR, xc) & sdtmndtasgtdt0(all_0_10_10, xR, all_0_8_8) & sdtmndtasgtdt0(all_0_10_10, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_7_7) & sdtmndtasgtdt0(xb, xR, all_0_7_7) & aReductOfIn0(all_0_9_9, xa, xR) & aReductOfIn0(all_0_10_10, xa, xR) & aElement0(all_0_7_7) & aElement0(all_0_8_8) & aElement0(all_0_9_9) & aElement0(all_0_10_10) & ! [v0] : ~ aReductOfIn0(v0, all_0_7_7, xR) & (all_0_7_7 = all_0_8_8 | (sdtmndtplgtdt0(all_0_8_8, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, all_0_8_8, xR) | (sdtmndtplgtdt0(all_0_4_4, xR, all_0_7_7) & aReductOfIn0(all_0_4_4, all_0_8_8, xR) & aElement0(all_0_4_4))))) & (all_0_7_7 = xc | (sdtmndtplgtdt0(xc, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xc, xR) | (sdtmndtplgtdt0(all_0_6_6, xR, all_0_7_7) & aReductOfIn0(all_0_6_6, xc, xR) & aElement0(all_0_6_6))))) & (all_0_7_7 = xb | (sdtmndtplgtdt0(xb, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xb, xR) | (sdtmndtplgtdt0(all_0_5_5, xR, all_0_7_7) & aReductOfIn0(all_0_5_5, xb, xR) & aElement0(all_0_5_5))))) & (all_0_8_8 = all_0_9_9 | (sdtmndtplgtdt0(all_0_9_9, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_3_3, xR, all_0_8_8) & aReductOfIn0(all_0_3_3, all_0_9_9, xR) & aElement0(all_0_3_3))))) & (all_0_8_8 = all_0_10_10 | (sdtmndtplgtdt0(all_0_10_10, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_2_2, xR, all_0_8_8) & aReductOfIn0(all_0_2_2, all_0_10_10, xR) & aElement0(all_0_2_2))))) & (all_0_9_9 = xc | (sdtmndtplgtdt0(all_0_9_9, xR, xc) & (aReductOfIn0(xc, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_1_1, xR, xc) & aReductOfIn0(all_0_1_1, all_0_9_9, xR) & aElement0(all_0_1_1))))) & (all_0_10_10 = xb | (sdtmndtplgtdt0(all_0_10_10, xR, xb) & (aReductOfIn0(xb, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_0_0, xR, xb) & aReductOfIn0(all_0_0_0, all_0_10_10, xR) & aElement0(all_0_0_0))))) % 9.80/2.97 | % 9.80/2.97 | Applying alpha-rule on (102) yields: % 9.80/2.97 | (103) all_0_7_7 = xc | (sdtmndtplgtdt0(xc, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xc, xR) | (sdtmndtplgtdt0(all_0_6_6, xR, all_0_7_7) & aReductOfIn0(all_0_6_6, xc, xR) & aElement0(all_0_6_6)))) % 9.80/2.97 | (104) sdtmndtasgtdt0(all_0_8_8, xR, all_0_7_7) % 9.80/2.97 | (105) aReductOfIn0(all_0_10_10, xa, xR) % 9.80/2.97 | (106) sdtmndtasgtdt0(xb, xR, all_0_7_7) % 9.80/2.97 | (107) sdtmndtasgtdt0(all_0_10_10, xR, all_0_8_8) % 9.80/2.97 | (108) all_0_9_9 = xc | (sdtmndtplgtdt0(all_0_9_9, xR, xc) & (aReductOfIn0(xc, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_1_1, xR, xc) & aReductOfIn0(all_0_1_1, all_0_9_9, xR) & aElement0(all_0_1_1)))) % 9.80/2.97 | (109) aElement0(all_0_7_7) % 9.80/2.97 | (110) all_0_10_10 = xb | (sdtmndtplgtdt0(all_0_10_10, xR, xb) & (aReductOfIn0(xb, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_0_0, xR, xb) & aReductOfIn0(all_0_0_0, all_0_10_10, xR) & aElement0(all_0_0_0)))) % 9.80/2.97 | (111) sdtmndtasgtdt0(xc, xR, all_0_7_7) % 9.80/2.97 | (112) aElement0(all_0_9_9) % 9.80/2.97 | (113) all_0_7_7 = xb | (sdtmndtplgtdt0(xb, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, xb, xR) | (sdtmndtplgtdt0(all_0_5_5, xR, all_0_7_7) & aReductOfIn0(all_0_5_5, xb, xR) & aElement0(all_0_5_5)))) % 9.80/2.97 | (114) aReductOfIn0(all_0_9_9, xa, xR) % 9.80/2.97 | (115) aElement0(all_0_10_10) % 9.80/2.97 | (116) aNormalFormOfIn0(all_0_7_7, all_0_8_8, xR) % 9.80/2.97 | (117) sdtmndtasgtdt0(all_0_9_9, xR, xc) % 9.80/2.97 | (118) sdtmndtasgtdt0(all_0_10_10, xR, xb) % 9.80/2.97 | (119) aElement0(all_0_8_8) % 9.80/2.97 | (120) all_0_8_8 = all_0_9_9 | (sdtmndtplgtdt0(all_0_9_9, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_9_9, xR) | (sdtmndtplgtdt0(all_0_3_3, xR, all_0_8_8) & aReductOfIn0(all_0_3_3, all_0_9_9, xR) & aElement0(all_0_3_3)))) % 9.80/2.97 | (121) sdtmndtasgtdt0(all_0_9_9, xR, all_0_8_8) % 9.80/2.97 | (122) all_0_7_7 = all_0_8_8 | (sdtmndtplgtdt0(all_0_8_8, xR, all_0_7_7) & (aReductOfIn0(all_0_7_7, all_0_8_8, xR) | (sdtmndtplgtdt0(all_0_4_4, xR, all_0_7_7) & aReductOfIn0(all_0_4_4, all_0_8_8, xR) & aElement0(all_0_4_4)))) % 9.80/2.97 | (123) all_0_8_8 = all_0_10_10 | (sdtmndtplgtdt0(all_0_10_10, xR, all_0_8_8) & (aReductOfIn0(all_0_8_8, all_0_10_10, xR) | (sdtmndtplgtdt0(all_0_2_2, xR, all_0_8_8) & aReductOfIn0(all_0_2_2, all_0_10_10, xR) & aElement0(all_0_2_2)))) % 9.80/2.97 | (124) ! [v0] : ~ aReductOfIn0(v0, all_0_7_7, xR) % 9.80/2.97 | % 9.80/2.97 | Instantiating formula (38) with all_0_7_7 and discharging atoms sdtmndtasgtdt0(xc, xR, all_0_7_7), sdtmndtasgtdt0(xb, xR, all_0_7_7), aElement0(all_0_7_7), yields: % 9.80/2.97 | (89) $false % 9.80/2.97 | % 9.80/2.97 |-The branch is then unsatisfiable % 9.80/2.97 |-Branch two: % 9.80/2.97 | (126) ~ sdtmndtplgtdt0(xa, xR, xc) & ~ aReductOfIn0(xc, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0)) % 9.80/2.97 | % 9.80/2.97 | Applying alpha-rule on (126) yields: % 9.80/2.97 | (127) ~ sdtmndtplgtdt0(xa, xR, xc) % 9.80/2.97 | (128) ~ aReductOfIn0(xc, xa, xR) % 9.80/2.97 | (129) ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xc) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0)) % 9.80/2.97 | % 9.80/2.97 | Using (92) and (127) yields: % 9.80/2.97 | (89) $false % 9.80/2.97 | % 9.80/2.97 |-The branch is then unsatisfiable % 9.80/2.97 |-Branch two: % 9.80/2.97 | (131) ~ sdtmndtplgtdt0(xa, xR, xb) & ~ aReductOfIn0(xb, xa, xR) & ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0)) % 9.80/2.97 | % 9.80/2.97 | Applying alpha-rule on (131) yields: % 9.80/2.97 | (132) ~ sdtmndtplgtdt0(xa, xR, xb) % 9.80/2.97 | (133) ~ aReductOfIn0(xb, xa, xR) % 9.80/2.97 | (134) ! [v0] : ( ~ sdtmndtplgtdt0(v0, xR, xb) | ~ aReductOfIn0(v0, xa, xR) | ~ aElement0(v0)) % 9.80/2.97 | % 9.80/2.97 | Using (99) and (132) yields: % 9.80/2.97 | (89) $false % 9.80/2.97 | % 9.80/2.97 |-The branch is then unsatisfiable % 9.80/2.97 % SZS output end Proof for theBenchmark % 9.80/2.97 % 9.80/2.97 2304ms %------------------------------------------------------------------------------