%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : RNG114+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.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:25 EDT 2022 % Result : Theorem 11.15s 3.34s % Output : Proof 41.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG114+4 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon May 30 15:02:27 EDT 2022 % 0.12/0.33 % CPUTime : % 0.55/0.58 ____ _ % 0.55/0.58 ___ / __ \_____(_)___ ________ __________ % 0.55/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.58 % 0.55/0.58 A Theorem Prover for First-Order Logic % 0.55/0.58 (ePrincess v.1.0) % 0.55/0.58 % 0.55/0.58 (c) Philipp Rümmer, 2009-2015 % 0.55/0.58 (c) Peter Backeman, 2014-2015 % 0.55/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.58 Bug reports to peter@backeman.se % 0.55/0.58 % 0.55/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.58 % 0.55/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.92/1.04 Prover 0: Preprocessing ... % 3.82/1.56 Prover 0: Constructing countermodel ... % 11.15/3.33 Prover 0: proved (2697ms) % 11.15/3.34 % 11.15/3.34 No countermodel exists, formula is valid % 11.15/3.34 % SZS status Theorem for theBenchmark % 11.15/3.34 % 11.15/3.34 Generating proof ... found it (size 477) % 40.11/16.20 % 40.11/16.20 % SZS output start Proof for theBenchmark % 40.11/16.20 Assumed formulas after preprocessing and simplification: % 40.11/16.20 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ( ~ (v6 = sz00) & ~ (xu = sz00) & ~ (sz10 = sz00) & slsdtgt0(xb) = v2 & slsdtgt0(xa) = v1 & sbrdtbr0(xu) = v3 & sdtpldt1(v1, v2) = xI & sdtasdt0(xc, v14) = xa & sdtasdt0(xc, v13) = xb & sdtasdt0(xb, v10) = sz00 & sdtasdt0(xb, v9) = xb & sdtasdt0(xa, v12) = sz00 & sdtasdt0(xa, v11) = xa & sdtpldt0(v7, v8) = v6 & sdtpldt0(v4, v5) = xu & smndt0(sz10) = v0 & aGcdOfAnd0(xc, xa, xb) & aDivisorOf0(xc, xb) & aDivisorOf0(xc, xa) & doDivides0(xc, xb) & doDivides0(xc, xa) & aIdeal0(xI) & aElementOf0(v8, v2) & aElementOf0(v7, v1) & aElementOf0(v6, xI) & aElementOf0(v5, v2) & aElementOf0(v4, v1) & aElementOf0(xu, xI) & aElementOf0(xb, v2) & aElementOf0(xa, v1) & aElementOf0(sz00, v2) & aElementOf0(sz00, v1) & aSet0(xI) & aElement0(v14) & aElement0(v13) & aElement0(v12) & aElement0(v11) & aElement0(v10) & aElement0(v9) & aElement0(xc) & aElement0(xb) & aElement0(xa) & aElement0(sz10) & aElement0(sz00) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtpldt1(v15, v16) = v17) | ~ (sdtpldt0(v19, v20) = v18) | ~ aElementOf0(v20, v16) | ~ aElementOf0(v19, v15) | ~ aSet0(v16) | ~ aSet0(v15) | aElementOf0(v18, v17)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtasdt0(v17, v15) = v19) | ~ (sdtasdt0(v16, v15) = v18) | ~ (sdtpldt0(v18, v19) = v20) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v21] : ? [v22] : ? [v23] : ? [v24] : (sdtasdt0(v21, v15) = v20 & sdtasdt0(v15, v21) = v22 & sdtasdt0(v15, v17) = v24 & sdtasdt0(v15, v16) = v23 & sdtpldt0(v23, v24) = v22 & sdtpldt0(v16, v17) = v21)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtasdt0(v15, v17) = v19) | ~ (sdtasdt0(v15, v16) = v18) | ~ (sdtpldt0(v18, v19) = v20) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v21] : ? [v22] : ? [v23] : ? [v24] : (sdtasdt0(v21, v15) = v22 & sdtasdt0(v17, v15) = v24 & sdtasdt0(v16, v15) = v23 & sdtasdt0(v15, v21) = v20 & sdtpldt0(v23, v24) = v22 & sdtpldt0(v16, v17) = v21)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt1(v15, v16) = v17) | ~ aIdeal0(v16) | ~ aIdeal0(v15) | ~ aElement0(v19) | ~ aElement0(v18) | ? [v20] : ((sdteqdtlpzmzozddtrp0(v20, v19, v16) & sdteqdtlpzmzozddtrp0(v20, v18, v15) & aElement0(v20)) | (aElement0(v20) & ~ aElementOf0(v20, v17)))) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtasdt0(v18, v17) = v19) | ~ (sdtasdt0(v15, v16) = v18) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : (sdtasdt0(v16, v17) = v20 & sdtasdt0(v15, v20) = v19)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtasdt0(v18, v15) = v19) | ~ (sdtpldt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : (sdtasdt0(v17, v15) = v24 & sdtasdt0(v16, v15) = v23 & sdtasdt0(v15, v18) = v20 & sdtasdt0(v15, v17) = v22 & sdtasdt0(v15, v16) = v21 & sdtpldt0(v23, v24) = v19 & sdtpldt0(v21, v22) = v20)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtasdt0(v16, v17) = v18) | ~ (sdtasdt0(v15, v18) = v19) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : (sdtasdt0(v20, v17) = v19 & sdtasdt0(v15, v16) = v20)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtasdt0(v15, v18) = v19) | ~ (sdtpldt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : (sdtasdt0(v18, v15) = v22 & sdtasdt0(v17, v15) = v24 & sdtasdt0(v16, v15) = v23 & sdtasdt0(v15, v17) = v21 & sdtasdt0(v15, v16) = v20 & sdtpldt0(v23, v24) = v22 & sdtpldt0(v20, v21) = v19)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v18, v17) = v19) | ~ (sdtpldt0(v15, v16) = v18) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : (sdtpldt0(v16, v17) = v20 & sdtpldt0(v15, v20) = v19)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ (sdtpldt0(v15, v18) = v19) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v20] : (sdtpldt0(v20, v17) = v19 & sdtpldt0(v15, v16) = v20)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v15, v18) = v19) | ~ (smndt0(v16) = v18) | ~ sdteqdtlpzmzozddtrp0(v15, v16, v17) | ~ aIdeal0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | aElementOf0(v19, v17)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v15, v18) = v19) | ~ (smndt0(v16) = v18) | ~ aIdeal0(v17) | ~ aElementOf0(v19, v17) | ~ aElement0(v16) | ~ aElement0(v15) | sdteqdtlpzmzozddtrp0(v15, v16, v17)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = v17 | ~ (sdtasasdt0(v15, v16) = v17) | ~ aSet0(v18) | ~ aSet0(v16) | ~ aSet0(v15) | ? [v19] : (( ~ aElementOf0(v19, v18) | ~ aElementOf0(v19, v16) | ~ aElementOf0(v19, v15)) & (aElementOf0(v19, v18) | (aElementOf0(v19, v16) & aElementOf0(v19, v15))))) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = v17 | ~ (sdtpldt1(v15, v16) = v17) | ~ aSet0(v18) | ~ aSet0(v16) | ~ aSet0(v15) | ? [v19] : ? [v20] : ? [v21] : ? [v22] : (( ~ aElementOf0(v19, v18) | ! [v23] : ! [v24] : ( ~ (sdtpldt0(v23, v24) = v19) | ~ aElementOf0(v24, v16) | ~ aElementOf0(v23, v15))) & (aElementOf0(v19, v18) | (v22 = v19 & sdtpldt0(v20, v21) = v19 & aElementOf0(v21, v16) & aElementOf0(v20, v15))))) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v16 = v15 | ~ (sdtasasdt0(v18, v17) = v16) | ~ (sdtasasdt0(v18, v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v16 = v15 | ~ (sdtpldt1(v18, v17) = v16) | ~ (sdtpldt1(v18, v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v16 = v15 | ~ (sdtasdt0(v18, v17) = v16) | ~ (sdtasdt0(v18, v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v16 = v15 | ~ (sdtpldt0(v18, v17) = v16) | ~ (sdtpldt0(v18, v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = sz00 | ~ (sbrdtbr0(v15) = v16) | ~ (sdtpldt0(v17, v18) = v15) | ~ iLess0(v16, v3) | ~ aElementOf0(v18, v2) | ~ aElementOf0(v17, v1)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (slsdtgt0(v15) = v16) | ~ (sdtasdt0(v15, v18) = v17) | ~ aElement0(v18) | ~ aElement0(v15) | aElementOf0(v17, v16)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtasasdt0(v15, v16) = v17) | ~ aElementOf0(v18, v17) | ~ aSet0(v16) | ~ aSet0(v15) | aElementOf0(v18, v16)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtasasdt0(v15, v16) = v17) | ~ aElementOf0(v18, v17) | ~ aSet0(v16) | ~ aSet0(v15) | aElementOf0(v18, v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtasasdt0(v15, v16) = v17) | ~ aElementOf0(v18, v16) | ~ aElementOf0(v18, v15) | ~ aSet0(v16) | ~ aSet0(v15) | aElementOf0(v18, v17)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt1(v15, v16) = v17) | ~ aElementOf0(v18, v17) | ~ aSet0(v16) | ~ aSet0(v15) | ? [v19] : ? [v20] : (sdtpldt0(v19, v20) = v18 & aElementOf0(v20, v16) & aElementOf0(v19, v15))) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtasdt0(v17, v16) = v18) | ~ aIdeal0(v15) | ~ aElementOf0(v16, v15) | ~ aElement0(v17) | aElementOf0(v18, v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ aIdeal0(v15) | ~ aElementOf0(v17, v15) | ~ aElementOf0(v16, v15) | aElementOf0(v18, v15)) & ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ aGcdOfAnd0(v17, v15, v16) | ~ aDivisorOf0(v18, v16) | ~ aDivisorOf0(v18, v15) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v18, v17)) & ! [v15] : ! [v16] : ! [v17] : (v17 = v16 | ~ (slsdtgt0(v15) = v16) | ~ aSet0(v17) | ~ aElement0(v15) | ? [v18] : ? [v19] : ? [v20] : (( ~ aElementOf0(v18, v17) | ! [v21] : ( ~ (sdtasdt0(v15, v21) = v18) | ~ aElement0(v21))) & (aElementOf0(v18, v17) | (v20 = v18 & sdtasdt0(v15, v19) = v18 & aElement0(v19))))) & ! [v15] : ! [v16] : ! [v17] : (v17 = sz00 | ~ (sdtpldt0(v16, v15) = v17) | ~ (smndt0(v15) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : ! [v17] : (v17 = sz00 | ~ (sdtpldt0(v15, v16) = v17) | ~ (smndt0(v15) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : ! [v17] : (v16 = v15 | ~ (slsdtgt0(v17) = v16) | ~ (slsdtgt0(v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : (v16 = v15 | ~ (sbrdtbr0(v17) = v16) | ~ (sbrdtbr0(v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : (v16 = v15 | ~ (smndt0(v17) = v16) | ~ (smndt0(v17) = v15)) & ! [v15] : ! [v16] : ! [v17] : (v16 = sz00 | ~ (sbrdtbr0(v16) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sbrdtbr0(v19) = v21 & sdtasdt0(v18, v16) = v20 & sdtpldt0(v20, v19) = v15 & aElement0(v19) & aElement0(v18) & (v19 = sz00 | iLess0(v21, v17)))) & ! [v15] : ! [v16] : ! [v17] : ( ~ (slsdtgt0(v15) = v16) | ~ aElementOf0(v17, v16) | ~ aElement0(v15) | ? [v18] : (sdtasdt0(v15, v18) = v17 & aElement0(v18))) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasasdt0(v15, v16) = v17) | ~ aIdeal0(v16) | ~ aIdeal0(v15) | aIdeal0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasasdt0(v15, v16) = v17) | ~ aSet0(v16) | ~ aSet0(v15) | aSet0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt1(v15, v16) = v17) | ~ aIdeal0(v16) | ~ aIdeal0(v15) | aIdeal0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt1(v15, v16) = v17) | ~ aSet0(v16) | ~ aSet0(v15) | aSet0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v16, v15) = v17) | ~ aElementOf0(v15, xI) | ~ aElement0(v16) | aElementOf0(v17, xI)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v16, v15) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | sdtasdt0(v15, v16) = v17) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v15, v17) = v16) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v15, v16)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v15, v17) = xa) | ~ (sdtasdt0(v15, v16) = xb) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v15, v17) = xa) | ~ (sdtasdt0(v15, v16) = xb) | ~ aElement0(v17) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v18] : (sdtasdt0(v15, v18) = xc & aElement0(v18))) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v15, v16) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | sdtasdt0(v16, v15) = v17) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtasdt0(v15, v16) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | aElement0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v16, v17) = v15) | ~ aElementOf0(v17, v2) | ~ aElementOf0(v16, v1) | aElementOf0(v15, xI)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v16, v15) = v17) | ~ (smndt0(v15) = v16) | ~ aElement0(v15) | sdtpldt0(v15, v16) = sz00) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v16, v15) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | sdtpldt0(v15, v16) = v17) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v15, v16) = v17) | ~ (smndt0(v15) = v16) | ~ aElement0(v15) | sdtpldt0(v16, v15) = sz00) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v15, v16) = v17) | ~ aElementOf0(v16, xI) | ~ aElementOf0(v15, xI) | aElementOf0(v17, xI)) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v15, v16) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | sdtpldt0(v16, v15) = v17) & ! [v15] : ! [v16] : ! [v17] : ( ~ (sdtpldt0(v15, v16) = v17) | ~ aElement0(v16) | ~ aElement0(v15) | aElement0(v17)) & ! [v15] : ! [v16] : ! [v17] : ( ~ aGcdOfAnd0(v17, v15, v16) | ~ aElement0(v16) | ~ aElement0(v15) | aDivisorOf0(v17, v16)) & ! [v15] : ! [v16] : ! [v17] : ( ~ aGcdOfAnd0(v17, v15, v16) | ~ aElement0(v16) | ~ aElement0(v15) | aDivisorOf0(v17, v15)) & ! [v15] : ! [v16] : ! [v17] : ( ~ aDivisorOf0(v17, v16) | ~ aDivisorOf0(v17, v15) | ~ aElement0(v16) | ~ aElement0(v15) | aGcdOfAnd0(v17, v15, v16) | ? [v18] : (aDivisorOf0(v18, v16) & aDivisorOf0(v18, v15) & ~ doDivides0(v18, v17))) & ! [v15] : ! [v16] : (v16 = v15 | ~ (sdtasdt0(v15, sz10) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = v15 | ~ (sdtasdt0(sz10, v15) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = v15 | ~ (sdtpldt0(v15, sz00) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = v15 | ~ (sdtpldt0(sz00, v15) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = v15 | ~ aSet0(v16) | ~ aSet0(v15) | ? [v17] : ((aElementOf0(v17, v16) & ~ aElementOf0(v17, v15)) | (aElementOf0(v17, v15) & ~ aElementOf0(v17, v16)))) & ! [v15] : ! [v16] : (v16 = sz00 | v15 = sz00 | ~ (sdtasdt0(v15, v16) = sz00) | ~ aElement0(v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = sz00 | ~ (sdtasdt0(v15, sz00) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v16 = sz00 | ~ (sdtasdt0(sz00, v15) = v16) | ~ aElement0(v15)) & ! [v15] : ! [v16] : (v15 = sz00 | ~ (sbrdtbr0(v15) = v16) | ~ iLess0(v16, v3) | ~ aElementOf0(v15, xI)) & ! [v15] : ! [v16] : (v15 = sz00 | ~ (sbrdtbr0(v15) = v16) | ~ aElement0(v15) | aNaturalNumber0(v16)) & ! [v15] : ! [v16] : ( ~ (slsdtgt0(v15) = v16) | ~ aElement0(v15) | aIdeal0(v16)) & ! [v15] : ! [v16] : ( ~ (slsdtgt0(v15) = v16) | ~ aElement0(v15) | aSet0(v16)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xb) | ~ aDivisorOf0(v15, xa) | ~ aElement0(v16) | doDivides0(v15, xc)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xb) | ~ aDivisorOf0(v15, xa) | ~ aElement0(v16) | ? [v17] : (sdtasdt0(v15, v17) = xc & aElement0(v17))) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xb) | ~ doDivides0(v15, xa) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xb) | ~ doDivides0(v15, xa) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v17] : (sdtasdt0(v15, v17) = xc & aElement0(v17))) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xa) | ~ aDivisorOf0(v15, xb) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xa) | ~ aDivisorOf0(v15, xb) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v17] : (sdtasdt0(v15, v17) = xc & aElement0(v17))) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xa) | ~ doDivides0(v15, xb) | ~ aElement0(v16) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v16) = xa) | ~ doDivides0(v15, xb) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v17] : (sdtasdt0(v15, v17) = xc & aElement0(v17))) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, v0) = v16) | ~ aElement0(v15) | (sdtasdt0(v0, v15) = v16 & smndt0(v15) = v16)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, sz10) = v16) | ~ aElement0(v15) | sdtasdt0(sz10, v15) = v15) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v15, sz00) = v16) | ~ aElement0(v15) | sdtasdt0(sz00, v15) = sz00) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(v0, v15) = v16) | ~ aElement0(v15) | (sdtasdt0(v15, v0) = v16 & smndt0(v15) = v16)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(xb, v16) = v15) | ~ aElement0(v16) | aElementOf0(v15, v2)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(xa, v16) = v15) | ~ aElement0(v16) | aElementOf0(v15, v1)) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(sz10, v15) = v16) | ~ aElement0(v15) | sdtasdt0(v15, sz10) = v15) & ! [v15] : ! [v16] : ( ~ (sdtasdt0(sz00, v15) = v16) | ~ aElement0(v15) | sdtasdt0(v15, sz00) = sz00) & ! [v15] : ! [v16] : ( ~ (sdtpldt0(v15, sz00) = v16) | ~ aElement0(v15) | sdtpldt0(sz00, v15) = v15) & ! [v15] : ! [v16] : ( ~ (sdtpldt0(sz00, v15) = v16) | ~ aElement0(v15) | sdtpldt0(v15, sz00) = v15) & ! [v15] : ! [v16] : ( ~ (smndt0(v15) = v16) | ~ aElement0(v15) | aElement0(v16)) & ! [v15] : ! [v16] : ( ~ (smndt0(v15) = v16) | ~ aElement0(v15) | (sdtasdt0(v15, v0) = v16 & sdtasdt0(v0, v15) = v16)) & ! [v15] : ! [v16] : ( ~ misRelativelyPrime0(v15, v16) | ~ aElement0(v16) | ~ aElement0(v15) | aGcdOfAnd0(sz10, v15, v16)) & ! [v15] : ! [v16] : ( ~ aGcdOfAnd0(sz10, v15, v16) | ~ aElement0(v16) | ~ aElement0(v15) | misRelativelyPrime0(v15, v16)) & ! [v15] : ! [v16] : ( ~ aDivisorOf0(v16, v15) | ~ aElement0(v15) | doDivides0(v16, v15)) & ! [v15] : ! [v16] : ( ~ aDivisorOf0(v16, v15) | ~ aElement0(v15) | aElement0(v16)) & ! [v15] : ! [v16] : ( ~ doDivides0(v16, v15) | ~ aElement0(v16) | ~ aElement0(v15) | aDivisorOf0(v16, v15)) & ! [v15] : ! [v16] : ( ~ doDivides0(v15, v16) | ~ aElement0(v16) | ~ aElement0(v15) | ? [v17] : (sdtasdt0(v15, v17) = v16 & aElement0(v17))) & ! [v15] : ! [v16] : ( ~ aElementOf0(v16, v15) | ~ aSet0(v15) | aElement0(v16)) & ! [v15] : ! [v16] : ( ~ aElement0(v16) | ~ aElement0(v15) | ? [v17] : ? [v18] : ? [v19] : ( ~ (v19 = xu) & sdtasdt0(xb, v16) = v18 & sdtasdt0(xa, v15) = v17 & sdtpldt0(v17, v18) = v19)) & ! [v15] : ( ~ aDivisorOf0(v15, xb) | ~ aDivisorOf0(v15, xa) | doDivides0(v15, xc)) & ! [v15] : ( ~ aDivisorOf0(v15, xb) | ~ aDivisorOf0(v15, xa) | ? [v16] : (sdtasdt0(v15, v16) = xc & aElement0(v16))) & ! [v15] : ( ~ aDivisorOf0(v15, xb) | ~ doDivides0(v15, xa) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ( ~ aDivisorOf0(v15, xb) | ~ doDivides0(v15, xa) | ~ aElement0(v15) | ? [v16] : (sdtasdt0(v15, v16) = xc & aElement0(v16))) & ! [v15] : ( ~ aDivisorOf0(v15, xa) | ~ doDivides0(v15, xb) | doDivides0(v15, xc)) & ! [v15] : ( ~ aDivisorOf0(v15, xa) | ~ doDivides0(v15, xb) | ? [v16] : (sdtasdt0(v15, v16) = xc & aElement0(v16))) & ! [v15] : ( ~ doDivides0(v15, xb) | ~ doDivides0(v15, xa) | ~ aElement0(v15) | doDivides0(v15, xc)) & ! [v15] : ( ~ doDivides0(v15, xb) | ~ doDivides0(v15, xa) | ~ aElement0(v15) | ? [v16] : (sdtasdt0(v15, v16) = xc & aElement0(v16))) & ! [v15] : ( ~ aIdeal0(v15) | aSet0(v15)) & ! [v15] : ( ~ aElementOf0(v15, v2) | ? [v16] : (sdtasdt0(xb, v16) = v15 & aElement0(v16))) & ! [v15] : ( ~ aElementOf0(v15, v1) | ? [v16] : (sdtasdt0(xa, v16) = v15 & aElement0(v16))) & ! [v15] : ( ~ aElementOf0(v15, xI) | ? [v16] : ? [v17] : (sdtpldt0(v16, v17) = v15 & aElementOf0(v17, v2) & aElementOf0(v16, v1))) & ! [v15] : ( ~ aSet0(v15) | aIdeal0(v15) | ? [v16] : ? [v17] : ? [v18] : (aElementOf0(v16, v15) & ((sdtasdt0(v17, v16) = v18 & aElement0(v17) & ~ aElementOf0(v18, v15)) | (sdtpldt0(v16, v17) = v18 & aElementOf0(v17, v15) & ~ aElementOf0(v18, v15))))) & ( ~ (xb = sz00) | ~ (xa = sz00)) & (( ~ aDivisorOf0(xu, xb) & ~ doDivides0(xu, xb) & ! [v15] : ( ~ (sdtasdt0(xu, v15) = xb) | ~ aElement0(v15))) | ( ~ aDivisorOf0(xu, xa) & ~ doDivides0(xu, xa) & ! [v15] : ( ~ (sdtasdt0(xu, v15) = xa) | ~ aElement0(v15))))) % 40.27/16.28 | 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, all_0_14_14 yields: % 40.27/16.28 | (1) ~ (all_0_8_8 = sz00) & ~ (xu = sz00) & ~ (sz10 = sz00) & slsdtgt0(xb) = all_0_12_12 & slsdtgt0(xa) = all_0_13_13 & sbrdtbr0(xu) = all_0_11_11 & sdtpldt1(all_0_13_13, all_0_12_12) = xI & sdtasdt0(xc, all_0_0_0) = xa & sdtasdt0(xc, all_0_1_1) = xb & sdtasdt0(xb, all_0_4_4) = sz00 & sdtasdt0(xb, all_0_5_5) = xb & sdtasdt0(xa, all_0_2_2) = sz00 & sdtasdt0(xa, all_0_3_3) = xa & sdtpldt0(all_0_7_7, all_0_6_6) = all_0_8_8 & sdtpldt0(all_0_10_10, all_0_9_9) = xu & smndt0(sz10) = all_0_14_14 & aGcdOfAnd0(xc, xa, xb) & aDivisorOf0(xc, xb) & aDivisorOf0(xc, xa) & doDivides0(xc, xb) & doDivides0(xc, xa) & aIdeal0(xI) & aElementOf0(all_0_6_6, all_0_12_12) & aElementOf0(all_0_7_7, all_0_13_13) & aElementOf0(all_0_8_8, xI) & aElementOf0(all_0_9_9, all_0_12_12) & aElementOf0(all_0_10_10, all_0_13_13) & aElementOf0(xu, xI) & aElementOf0(xb, all_0_12_12) & aElementOf0(xa, all_0_13_13) & aElementOf0(sz00, all_0_12_12) & aElementOf0(sz00, all_0_13_13) & aSet0(xI) & aElement0(all_0_0_0) & aElement0(all_0_1_1) & aElement0(all_0_2_2) & aElement0(all_0_3_3) & aElement0(all_0_4_4) & aElement0(all_0_5_5) & aElement0(xc) & aElement0(xb) & aElement0(xa) & aElement0(sz10) & aElement0(sz00) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ (sdtpldt0(v4, v5) = v3) | ~ aElementOf0(v5, v1) | ~ aElementOf0(v4, v0) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | ~ aElement0(v4) | ~ aElement0(v3) | ? [v5] : ((sdteqdtlpzmzozddtrp0(v5, v4, v1) & sdteqdtlpzmzozddtrp0(v5, v3, v0) & aElement0(v5)) | (aElement0(v5) & ~ aElementOf0(v5, v2)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v3) = v5 & sdtasdt0(v0, v2) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v6, v7) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v3, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aIdeal0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElementOf0(v4, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ aIdeal0(v2) | ~ aElementOf0(v4, v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtasasdt0(v0, v1) = v2) | ~ aSet0(v3) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v1) | ~ aElementOf0(v4, v0)) & (aElementOf0(v4, v3) | (aElementOf0(v4, v1) & aElementOf0(v4, v0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt1(v0, v1) = v2) | ~ aSet0(v3) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ aElementOf0(v4, v3) | ! [v8] : ! [v9] : ( ~ (sdtpldt0(v8, v9) = v4) | ~ aElementOf0(v9, v1) | ~ aElementOf0(v8, v0))) & (aElementOf0(v4, v3) | (v7 = v4 & sdtpldt0(v5, v6) = v4 & aElementOf0(v6, v1) & aElementOf0(v5, v0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | ~ (sdtpldt1(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] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ (sdtpldt0(v2, v3) = v0) | ~ iLess0(v1, all_0_11_11) | ~ aElementOf0(v3, all_0_12_12) | ~ aElementOf0(v2, all_0_13_13)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slsdtgt0(v0) = v1) | ~ (sdtasdt0(v0, v3) = v2) | ~ aElement0(v3) | ~ aElement0(v0) | aElementOf0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v1) | ~ aElementOf0(v3, v0) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : ? [v5] : (sdtpldt0(v4, v5) = v3 & aElementOf0(v5, v1) & aElementOf0(v4, v0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasdt0(v2, v1) = v3) | ~ aIdeal0(v0) | ~ aElementOf0(v1, v0) | ~ aElement0(v2) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ aIdeal0(v0) | ~ aElementOf0(v2, v0) | ~ aElementOf0(v1, v0) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aDivisorOf0(v3, v1) | ~ aDivisorOf0(v3, v0) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (slsdtgt0(v0) = v1) | ~ aSet0(v2) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (( ~ aElementOf0(v3, v2) | ! [v6] : ( ~ (sdtasdt0(v0, v6) = v3) | ~ aElement0(v6))) & (aElementOf0(v3, v2) | (v5 = v3 & sdtasdt0(v0, v4) = v3 & aElement0(v4))))) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) | ~ (slsdtgt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (sbrdtbr0(v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sbrdtbr0(v4) = v6 & sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) & aElement0(v3) & (v4 = sz00 | iLess0(v6, v2)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (slsdtgt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aElement0(v0) | ? [v3] : (sdtasdt0(v0, v3) = v2 & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | aIdeal0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | aIdeal0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aElementOf0(v0, xI) | ~ aElement0(v1) | aElementOf0(v2, xI)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtasdt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = v1) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = xa) | ~ (sdtasdt0(v0, v1) = xb) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = xa) | ~ (sdtasdt0(v0, v1) = xb) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : (sdtasdt0(v0, v3) = xc & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtasdt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v2) = v0) | ~ aElementOf0(v2, all_0_12_12) | ~ aElementOf0(v1, all_0_13_13) | aElementOf0(v0, xI)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0) | sdtpldt0(v0, v1) = sz00) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtpldt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0) | sdtpldt0(v1, v0) = sz00) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v1, xI) | ~ aElementOf0(v0, xI) | aElementOf0(v2, xI)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtpldt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aDivisorOf0(v2, v1) | ~ aDivisorOf0(v2, v0) | ~ aElement0(v1) | ~ aElement0(v0) | aGcdOfAnd0(v2, v0, v1) | ? [v3] : (aDivisorOf0(v3, v1) & aDivisorOf0(v3, v0) & ~ doDivides0(v3, v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ aSet0(v1) | ~ aSet0(v0) | ? [v2] : ((aElementOf0(v2, v1) & ~ aElementOf0(v2, v0)) | (aElementOf0(v2, v0) & ~ aElementOf0(v2, v1)))) & ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aElement0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ iLess0(v1, all_0_11_11) | ~ aElementOf0(v0, xI)) & ! [v0] : ! [v1] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ aElement0(v0) | aNaturalNumber0(v1)) & ! [v0] : ! [v1] : ( ~ (slsdtgt0(v0) = v1) | ~ aElement0(v0) | aIdeal0(v1)) & ! [v0] : ! [v1] : ( ~ (slsdtgt0(v0) = v1) | ~ aElement0(v0) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ aDivisorOf0(v0, xa) | ~ aElement0(v1) | doDivides0(v0, xc)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ aDivisorOf0(v0, xa) | ~ aElement0(v1) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ doDivides0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ doDivides0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ aDivisorOf0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ aDivisorOf0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ doDivides0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ doDivides0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, all_0_14_14) = v1) | ~ aElement0(v0) | (sdtasdt0(all_0_14_14, v0) = v1 & smndt0(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aElement0(v0) | sdtasdt0(sz10, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aElement0(v0) | sdtasdt0(sz00, v0) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(all_0_14_14, v0) = v1) | ~ aElement0(v0) | (sdtasdt0(v0, all_0_14_14) = v1 & smndt0(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(xb, v1) = v0) | ~ aElement0(v1) | aElementOf0(v0, all_0_12_12)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(xa, v1) = v0) | ~ aElement0(v1) | aElementOf0(v0, all_0_13_13)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aElement0(v0) | sdtasdt0(v0, sz10) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aElement0(v0) | sdtasdt0(v0, sz00) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aElement0(v0) | sdtpldt0(sz00, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aElement0(v0) | sdtpldt0(v0, sz00) = v0) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElement0(v0) | aElement0(v1)) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElement0(v0) | (sdtasdt0(v0, all_0_14_14) = v1 & sdtasdt0(all_0_14_14, v0) = v1)) & ! [v0] : ! [v1] : ( ~ misRelativelyPrime0(v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aGcdOfAnd0(sz10, v0, v1)) & ! [v0] : ! [v1] : ( ~ aGcdOfAnd0(sz10, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | misRelativelyPrime0(v0, v1)) & ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aElement0(v0) | doDivides0(v1, v0)) & ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aElement0(v0) | aElement0(v1)) & ! [v0] : ! [v1] : ( ~ doDivides0(v1, v0) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v1, v0)) & ! [v0] : ! [v1] : ( ~ doDivides0(v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = v1 & aElement0(v2))) & ! [v0] : ! [v1] : ( ~ aElementOf0(v1, v0) | ~ aSet0(v0) | aElement0(v1)) & ! [v0] : ! [v1] : ( ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = xu) & sdtasdt0(xb, v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = v4)) & ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ aDivisorOf0(v0, xa) | doDivides0(v0, xc)) & ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ aDivisorOf0(v0, xa) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) & ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) & ! [v0] : ( ~ aDivisorOf0(v0, xa) | ~ doDivides0(v0, xb) | doDivides0(v0, xc)) & ! [v0] : ( ~ aDivisorOf0(v0, xa) | ~ doDivides0(v0, xb) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) & ! [v0] : ( ~ doDivides0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | doDivides0(v0, xc)) & ! [v0] : ( ~ doDivides0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) & ! [v0] : ( ~ aIdeal0(v0) | aSet0(v0)) & ! [v0] : ( ~ aElementOf0(v0, all_0_12_12) | ? [v1] : (sdtasdt0(xb, v1) = v0 & aElement0(v1))) & ! [v0] : ( ~ aElementOf0(v0, all_0_13_13) | ? [v1] : (sdtasdt0(xa, v1) = v0 & aElement0(v1))) & ! [v0] : ( ~ aElementOf0(v0, xI) | ? [v1] : ? [v2] : (sdtpldt0(v1, v2) = v0 & aElementOf0(v2, all_0_12_12) & aElementOf0(v1, all_0_13_13))) & ! [v0] : ( ~ aSet0(v0) | aIdeal0(v0) | ? [v1] : ? [v2] : ? [v3] : (aElementOf0(v1, v0) & ((sdtasdt0(v2, v1) = v3 & aElement0(v2) & ~ aElementOf0(v3, v0)) | (sdtpldt0(v1, v2) = v3 & aElementOf0(v2, v0) & ~ aElementOf0(v3, v0))))) & ( ~ (xb = sz00) | ~ (xa = sz00)) & (( ~ aDivisorOf0(xu, xb) & ~ doDivides0(xu, xb) & ! [v0] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ aElement0(v0))) | ( ~ aDivisorOf0(xu, xa) & ~ doDivides0(xu, xa) & ! [v0] : ( ~ (sdtasdt0(xu, v0) = xa) | ~ aElement0(v0)))) % 40.27/16.30 | % 40.27/16.30 | Applying alpha-rule on (1) yields: % 40.27/16.31 | (2) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) | ~ (slsdtgt0(v2) = v0)) % 40.69/16.31 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v1) | ~ aElementOf0(v3, v0) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) % 40.69/16.31 | (4) ! [v0] : ! [v1] : ( ~ (sdtasdt0(xb, v1) = v0) | ~ aElement0(v1) | aElementOf0(v0, all_0_12_12)) % 40.69/16.31 | (5) sdtasdt0(xb, all_0_5_5) = xb % 40.69/16.31 | (6) sdtpldt1(all_0_13_13, all_0_12_12) = xI % 40.69/16.31 | (7) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ doDivides0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.31 | (8) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0)) % 40.69/16.31 | (9) aElement0(all_0_3_3) % 40.69/16.31 | (10) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ iLess0(v1, all_0_11_11) | ~ aElementOf0(v0, xI)) % 40.69/16.31 | (11) aElementOf0(all_0_6_6, all_0_12_12) % 40.69/16.31 | (12) ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.31 | (13) aElementOf0(xa, all_0_13_13) % 40.69/16.31 | (14) sdtpldt0(all_0_10_10, all_0_9_9) = xu % 40.69/16.31 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aElementOf0(v0, xI) | ~ aElement0(v1) | aElementOf0(v2, xI)) % 40.69/16.31 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) % 40.69/16.31 | (17) ! [v0] : ( ~ aSet0(v0) | aIdeal0(v0) | ? [v1] : ? [v2] : ? [v3] : (aElementOf0(v1, v0) & ((sdtasdt0(v2, v1) = v3 & aElement0(v2) & ~ aElementOf0(v3, v0)) | (sdtpldt0(v1, v2) = v3 & aElementOf0(v2, v0) & ~ aElementOf0(v3, v0))))) % 40.69/16.31 | (18) ~ (xu = sz00) % 40.69/16.31 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 40.69/16.31 | (20) aElement0(all_0_2_2) % 40.69/16.31 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v2, v1)) % 40.69/16.31 | (22) aDivisorOf0(xc, xb) % 40.69/16.31 | (23) aElement0(all_0_5_5) % 40.69/16.31 | (24) aElement0(all_0_4_4) % 40.69/16.31 | (25) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ doDivides0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) % 40.69/16.31 | (26) aElementOf0(all_0_8_8, xI) % 40.69/16.31 | (27) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aElement0(v0)) % 40.69/16.31 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = v1) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, v1)) % 40.69/16.31 | (29) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ aDivisorOf0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.31 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | aIdeal0(v2)) % 40.69/16.31 | (31) ! [v0] : ( ~ aDivisorOf0(v0, xa) | ~ doDivides0(v0, xb) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) % 40.69/16.31 | (32) doDivides0(xc, xa) % 40.69/16.31 | (33) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtasdt0(v0, v1) = v2) % 40.69/16.31 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) % 40.69/16.31 | (35) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aElement0(v0) | sdtpldt0(sz00, v0) = v0) % 40.69/16.31 | (36) ~ (all_0_8_8 = sz00) % 40.69/16.31 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | ~ (sdtpldt1(v3, v2) = v0)) % 40.69/16.31 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtasdt0(v1, v0) = v2) % 40.69/16.31 | (39) ! [v0] : ! [v1] : ! [v2] : ( ~ aDivisorOf0(v2, v1) | ~ aDivisorOf0(v2, v0) | ~ aElement0(v1) | ~ aElement0(v0) | aGcdOfAnd0(v2, v0, v1) | ? [v3] : (aDivisorOf0(v3, v1) & aDivisorOf0(v3, v0) & ~ doDivides0(v3, v2))) % 40.69/16.31 | (40) ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aElement0(v0) | doDivides0(v1, v0)) % 40.69/16.31 | (41) ! [v0] : ! [v1] : ( ~ aElementOf0(v1, v0) | ~ aSet0(v0) | aElement0(v1)) % 40.69/16.31 | (42) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aElement0(v0)) % 40.69/16.32 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) % 40.69/16.32 | (44) aElement0(sz10) % 40.69/16.32 | (45) ! [v0] : ! [v1] : ( ~ (sdtasdt0(xa, v1) = v0) | ~ aElement0(v1) | aElementOf0(v0, all_0_13_13)) % 40.69/16.32 | (46) ! [v0] : ( ~ aElementOf0(v0, all_0_13_13) | ? [v1] : (sdtasdt0(xa, v1) = v0 & aElement0(v1))) % 40.69/16.32 | (47) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElement0(v2)) % 40.69/16.32 | (48) aElementOf0(all_0_9_9, all_0_12_12) % 40.69/16.32 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) % 40.69/16.32 | (50) sdtpldt0(all_0_7_7, all_0_6_6) = all_0_8_8 % 40.69/16.32 | (51) ( ~ aDivisorOf0(xu, xb) & ~ doDivides0(xu, xb) & ! [v0] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ aElement0(v0))) | ( ~ aDivisorOf0(xu, xa) & ~ doDivides0(xu, xa) & ! [v0] : ( ~ (sdtasdt0(xu, v0) = xa) | ~ aElement0(v0))) % 40.69/16.32 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aDivisorOf0(v3, v1) | ~ aDivisorOf0(v3, v0) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v3, v2)) % 40.69/16.32 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aIdeal0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElementOf0(v4, v2)) % 40.69/16.32 | (54) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aElement0(v0)) % 40.69/16.32 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v2) = v0) | ~ aElementOf0(v2, all_0_12_12) | ~ aElementOf0(v1, all_0_13_13) | aElementOf0(v0, xI)) % 40.69/16.32 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtpldt0(v1, v0) = v2) % 40.69/16.32 | (57) aElementOf0(sz00, all_0_13_13) % 40.69/16.32 | (58) sdtasdt0(xc, all_0_0_0) = xa % 40.69/16.32 | (59) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ doDivides0(v0, xa) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.32 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = xa) | ~ (sdtasdt0(v0, v1) = xb) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.32 | (61) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSet0(v2)) % 40.69/16.32 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdtpldt0(v0, v1) = v2) % 40.69/16.32 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) % 40.69/16.32 | (64) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ aDivisorOf0(v0, xa) | ~ aElement0(v1) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) % 40.69/16.32 | (65) aElement0(xc) % 40.69/16.32 | (66) aElement0(all_0_1_1) % 40.69/16.32 | (67) ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ aDivisorOf0(v0, xa) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) % 40.69/16.32 | (68) ! [v0] : ! [v1] : ( ~ aGcdOfAnd0(sz10, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | misRelativelyPrime0(v0, v1)) % 40.69/16.32 | (69) aElementOf0(all_0_7_7, all_0_13_13) % 40.69/16.32 | (70) aElementOf0(sz00, all_0_12_12) % 40.69/16.32 | (71) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0)) % 40.69/16.32 | (72) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (slsdtgt0(v0) = v1) | ~ aSet0(v2) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : (( ~ aElementOf0(v3, v2) | ! [v6] : ( ~ (sdtasdt0(v0, v6) = v3) | ~ aElement0(v6))) & (aElementOf0(v3, v2) | (v5 = v3 & sdtasdt0(v0, v4) = v3 & aElement0(v4))))) % 40.69/16.32 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : ? [v5] : (sdtpldt0(v4, v5) = v3 & aElementOf0(v5, v1) & aElementOf0(v4, v0))) % 40.69/16.32 | (74) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aElement0(v1) | ~ aElement0(v0)) % 40.69/16.32 | (75) smndt0(sz10) = all_0_14_14 % 40.69/16.32 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ (sdtpldt0(v2, v3) = v0) | ~ iLess0(v1, all_0_11_11) | ~ aElementOf0(v3, all_0_12_12) | ~ aElementOf0(v2, all_0_13_13)) % 40.69/16.33 | (77) sdtasdt0(xb, all_0_4_4) = sz00 % 40.69/16.33 | (78) aGcdOfAnd0(xc, xa, xb) % 40.69/16.33 | (79) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0) | sdtpldt0(v1, v0) = sz00) % 40.69/16.33 | (80) aElement0(xb) % 40.69/16.33 | (81) slsdtgt0(xb) = all_0_12_12 % 40.69/16.33 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) % 40.69/16.33 | (83) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aElement0(v0)) % 40.69/16.33 | (84) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aElement0(v0) | sdtpldt0(v0, v1) = sz00) % 40.69/16.33 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ aIdeal0(v2) | ~ aElementOf0(v4, v2) | ~ aElement0(v1) | ~ aElement0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) % 40.69/16.33 | (86) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aElement0(v0) | sdtasdt0(sz10, v0) = v0) % 40.69/16.33 | (87) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ aDivisorOf0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) % 40.69/16.33 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v1, xI) | ~ aElementOf0(v0, xI) | aElementOf0(v2, xI)) % 40.69/16.33 | (89) ~ (sz10 = sz00) % 40.69/16.33 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtasasdt0(v0, v1) = v2) | ~ aSet0(v3) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v1) | ~ aElementOf0(v4, v0)) & (aElementOf0(v4, v3) | (aElementOf0(v4, v1) & aElementOf0(v4, v0))))) % 40.69/16.33 | (91) ! [v0] : ! [v1] : ( ~ doDivides0(v1, v0) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v1, v0)) % 40.69/16.33 | (92) ! [v0] : ! [v1] : ( ~ doDivides0(v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = v1 & aElement0(v2))) % 40.69/16.33 | (93) ! [v0] : ! [v1] : ! [v2] : ( ~ (slsdtgt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aElement0(v0) | ? [v3] : (sdtasdt0(v0, v3) = v2 & aElement0(v3))) % 40.69/16.33 | (94) ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ aDivisorOf0(v0, xa) | doDivides0(v0, xc)) % 40.69/16.33 | (95) ! [v0] : ! [v1] : ( ~ (slsdtgt0(v0) = v1) | ~ aElement0(v0) | aIdeal0(v1)) % 40.69/16.33 | (96) ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aElement0(v0) | aElement0(v1)) % 40.69/16.33 | (97) aElementOf0(xu, xI) % 40.69/16.33 | (98) sbrdtbr0(xu) = all_0_11_11 % 40.69/16.33 | (99) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 40.69/16.33 | (100) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 40.69/16.33 | (101) doDivides0(xc, xb) % 40.69/16.33 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | ~ aElement0(v4) | ~ aElement0(v3) | ? [v5] : ((sdteqdtlpzmzozddtrp0(v5, v4, v1) & sdteqdtlpzmzozddtrp0(v5, v3, v0) & aElement0(v5)) | (aElement0(v5) & ~ aElementOf0(v5, v2)))) % 40.69/16.33 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) % 40.69/16.33 | (104) sdtasdt0(xc, all_0_1_1) = xb % 40.69/16.33 | (105) ! [v0] : ( ~ aDivisorOf0(v0, xa) | ~ doDivides0(v0, xb) | doDivides0(v0, xc)) % 40.69/16.33 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt1(v0, v1) = v2) | ~ aSet0(v3) | ~ aSet0(v1) | ~ aSet0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ aElementOf0(v4, v3) | ! [v8] : ! [v9] : ( ~ (sdtpldt0(v8, v9) = v4) | ~ aElementOf0(v9, v1) | ~ aElementOf0(v8, v0))) & (aElementOf0(v4, v3) | (v7 = v4 & sdtpldt0(v5, v6) = v4 & aElementOf0(v6, v1) & aElementOf0(v5, v0))))) % 40.69/16.33 | (107) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aElement0(v0) | sdtasdt0(v0, sz00) = sz00) % 40.69/16.33 | (108) ! [v0] : ! [v1] : ( ~ (sdtasdt0(all_0_14_14, v0) = v1) | ~ aElement0(v0) | (sdtasdt0(v0, all_0_14_14) = v1 & smndt0(v0) = v1)) % 40.69/16.34 | (109) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, all_0_14_14) = v1) | ~ aElement0(v0) | (sdtasdt0(all_0_14_14, v0) = v1 & smndt0(v0) = v1)) % 40.69/16.34 | (110) sdtasdt0(xa, all_0_2_2) = sz00 % 40.69/16.34 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v3) = v5 & sdtasdt0(v0, v2) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v6, v7) = v5)) % 40.69/16.34 | (112) aDivisorOf0(xc, xa) % 40.69/16.34 | (113) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xb) | ~ aDivisorOf0(v0, xa) | ~ aElement0(v1) | doDivides0(v0, xc)) % 40.69/16.34 | (114) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aElement0(v0) | sdtasdt0(sz00, v0) = sz00) % 40.69/16.34 | (115) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aElement0(v0) | sdtasdt0(v0, sz10) = v0) % 40.69/16.34 | (116) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElement0(v0) | (sdtasdt0(v0, all_0_14_14) = v1 & sdtasdt0(all_0_14_14, v0) = v1)) % 40.69/16.34 | (117) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aElement0(v0)) % 40.69/16.34 | (118) ! [v0] : ( ~ aDivisorOf0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) % 40.69/16.34 | (119) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = xa) | ~ (sdtasdt0(v0, v1) = xb) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : (sdtasdt0(v0, v3) = xc & aElement0(v3))) % 40.69/16.34 | (120) aElement0(sz00) % 40.69/16.34 | (121) aElement0(all_0_0_0) % 40.69/16.34 | (122) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasdt0(v2, v1) = v3) | ~ aIdeal0(v0) | ~ aElementOf0(v1, v0) | ~ aElement0(v2) | aElementOf0(v3, v0)) % 40.69/16.34 | (123) ! [v0] : ! [v1] : ( ~ (slsdtgt0(v0) = v1) | ~ aElement0(v0) | aSet0(v1)) % 40.69/16.34 | (124) aElementOf0(all_0_10_10, all_0_13_13) % 40.69/16.34 | (125) ! [v0] : ( ~ aIdeal0(v0) | aSet0(v0)) % 40.69/16.34 | (126) ! [v0] : ( ~ aElementOf0(v0, xI) | ? [v1] : ? [v2] : (sdtpldt0(v1, v2) = v0 & aElementOf0(v2, all_0_12_12) & aElementOf0(v1, all_0_13_13))) % 40.69/16.34 | (127) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ aElement0(v0) | aNaturalNumber0(v1)) % 40.69/16.34 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ aIdeal0(v0) | ~ aElementOf0(v2, v0) | ~ aElementOf0(v1, v0) | aElementOf0(v3, v0)) % 40.69/16.34 | (129) ! [v0] : ! [v1] : ! [v2] : ( ~ aGcdOfAnd0(v2, v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aDivisorOf0(v2, v0)) % 40.69/16.34 | (130) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aIdeal0(v1) | ~ aIdeal0(v0) | aIdeal0(v2)) % 40.69/16.34 | (131) ! [v0] : ( ~ aElementOf0(v0, all_0_12_12) | ? [v1] : (sdtasdt0(xb, v1) = v0 & aElement0(v1))) % 40.69/16.34 | (132) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v3, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v5, v6) = v4)) % 40.69/16.34 | (133) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aElement0(v0)) % 40.69/16.34 | (134) sdtasdt0(xa, all_0_3_3) = xa % 40.69/16.34 | (135) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElement0(v0) | aElement0(v1)) % 40.69/16.34 | (136) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 40.69/16.34 | (137) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slsdtgt0(v0) = v1) | ~ (sdtasdt0(v0, v3) = v2) | ~ aElement0(v3) | ~ aElement0(v0) | aElementOf0(v2, v1)) % 40.69/16.34 | (138) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (sbrdtbr0(v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (sbrdtbr0(v4) = v6 & sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) & aElement0(v3) & (v4 = sz00 | iLess0(v6, v2)))) % 40.69/16.34 | (139) ~ (xb = sz00) | ~ (xa = sz00) % 40.69/16.34 | (140) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSet0(v2)) % 40.69/16.35 | (141) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aElement0(v0) | sdtpldt0(v0, sz00) = v0) % 40.69/16.35 | (142) ! [v0] : ( ~ doDivides0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | doDivides0(v0, xc)) % 40.69/16.35 | (143) ! [v0] : ! [v1] : ( ~ misRelativelyPrime0(v0, v1) | ~ aElement0(v1) | ~ aElement0(v0) | aGcdOfAnd0(sz10, v0, v1)) % 40.69/16.35 | (144) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt1(v0, v1) = v2) | ~ (sdtpldt0(v4, v5) = v3) | ~ aElementOf0(v5, v1) | ~ aElementOf0(v4, v0) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) % 40.69/16.35 | (145) aSet0(xI) % 40.69/16.35 | (146) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aSet0(v1) | ~ aSet0(v0) | aElementOf0(v3, v1)) % 40.69/16.35 | (147) ! [v0] : ( ~ doDivides0(v0, xb) | ~ doDivides0(v0, xa) | ~ aElement0(v0) | ? [v1] : (sdtasdt0(v0, v1) = xc & aElement0(v1))) % 40.69/16.35 | (148) aElement0(xa) % 40.69/16.35 | (149) aElementOf0(xb, all_0_12_12) % 40.69/16.35 | (150) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, v1) = xa) | ~ doDivides0(v0, xb) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : (sdtasdt0(v0, v2) = xc & aElement0(v2))) % 40.69/16.35 | (151) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aElement0(v0) | aElement0(v2)) % 40.69/16.35 | (152) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) % 40.69/16.35 | (153) aIdeal0(xI) % 40.69/16.35 | (154) ! [v0] : ! [v1] : (v1 = v0 | ~ aSet0(v1) | ~ aSet0(v0) | ? [v2] : ((aElementOf0(v2, v1) & ~ aElementOf0(v2, v0)) | (aElementOf0(v2, v0) & ~ aElementOf0(v2, v1)))) % 40.69/16.35 | (155) slsdtgt0(xa) = all_0_13_13 % 40.69/16.35 | (156) ! [v0] : ! [v1] : ( ~ aElement0(v1) | ~ aElement0(v0) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = xu) & sdtasdt0(xb, v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = v4)) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (41) with all_0_8_8, xI and discharging atoms aElementOf0(all_0_8_8, xI), aSet0(xI), yields: % 40.69/16.35 | (157) aElement0(all_0_8_8) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (41) with xu, xI and discharging atoms aElementOf0(xu, xI), aSet0(xI), yields: % 40.69/16.35 | (158) aElement0(xu) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (156) with all_0_0_0, all_0_3_3 and discharging atoms aElement0(all_0_0_0), aElement0(all_0_3_3), yields: % 40.69/16.35 | (159) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_0_0) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (156) with all_0_1_1, all_0_3_3 and discharging atoms aElement0(all_0_1_1), aElement0(all_0_3_3), yields: % 40.69/16.35 | (160) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_1_1) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (156) with all_0_2_2, all_0_3_3 and discharging atoms aElement0(all_0_2_2), aElement0(all_0_3_3), yields: % 40.69/16.35 | (161) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_2_2) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (156) with all_0_4_4, all_0_0_0 and discharging atoms aElement0(all_0_0_0), aElement0(all_0_4_4), yields: % 40.69/16.35 | (162) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, all_0_0_0) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.35 | % 40.69/16.35 | Instantiating formula (156) with all_0_4_4, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(all_0_4_4), yields: % 40.69/16.35 | (163) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_5_5, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(all_0_5_5), yields: % 40.69/16.36 | (164) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_5_5) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_4_4, all_0_5_5 and discharging atoms aElement0(all_0_4_4), aElement0(all_0_5_5), yields: % 40.69/16.36 | (165) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, all_0_5_5) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (147) with xc and discharging atoms doDivides0(xc, xb), doDivides0(xc, xa), aElement0(xc), yields: % 40.69/16.36 | (166) ? [v0] : (sdtasdt0(xc, v0) = xc & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with xc, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(xc), yields: % 40.69/16.36 | (167) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xc) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with all_0_6_6, all_0_12_12, xb and discharging atoms slsdtgt0(xb) = all_0_12_12, aElementOf0(all_0_6_6, all_0_12_12), aElement0(xb), yields: % 40.69/16.36 | (168) ? [v0] : (sdtasdt0(xb, v0) = all_0_6_6 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with all_0_9_9, all_0_12_12, xb and discharging atoms slsdtgt0(xb) = all_0_12_12, aElementOf0(all_0_9_9, all_0_12_12), aElement0(xb), yields: % 40.69/16.36 | (169) ? [v0] : (sdtasdt0(xb, v0) = all_0_9_9 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with xb, all_0_12_12, xb and discharging atoms slsdtgt0(xb) = all_0_12_12, aElementOf0(xb, all_0_12_12), aElement0(xb), yields: % 40.69/16.36 | (170) ? [v0] : (sdtasdt0(xb, v0) = xb & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with sz00, all_0_12_12, xb and discharging atoms slsdtgt0(xb) = all_0_12_12, aElementOf0(sz00, all_0_12_12), aElement0(xb), yields: % 40.69/16.36 | (171) ? [v0] : (sdtasdt0(xb, v0) = sz00 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (92) with xb, xc and discharging atoms doDivides0(xc, xb), aElement0(xc), aElement0(xb), yields: % 40.69/16.36 | (172) ? [v0] : (sdtasdt0(xc, v0) = xb & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with xb, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(xb), yields: % 40.69/16.36 | (173) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xb) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_4_4, xb and discharging atoms aElement0(all_0_4_4), aElement0(xb), yields: % 40.69/16.36 | (174) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, xb) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (33) with xa, xa, all_0_3_3 and discharging atoms sdtasdt0(xa, all_0_3_3) = xa, aElement0(all_0_3_3), aElement0(xa), yields: % 40.69/16.36 | (175) sdtasdt0(all_0_3_3, xa) = xa % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with all_0_7_7, all_0_13_13, xa and discharging atoms slsdtgt0(xa) = all_0_13_13, aElementOf0(all_0_7_7, all_0_13_13), aElement0(xa), yields: % 40.69/16.36 | (176) ? [v0] : (sdtasdt0(xa, v0) = all_0_7_7 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with all_0_10_10, all_0_13_13, xa and discharging atoms slsdtgt0(xa) = all_0_13_13, aElementOf0(all_0_10_10, all_0_13_13), aElement0(xa), yields: % 40.69/16.36 | (177) ? [v0] : (sdtasdt0(xa, v0) = all_0_10_10 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with xa, all_0_13_13, xa and discharging atoms slsdtgt0(xa) = all_0_13_13, aElementOf0(xa, all_0_13_13), aElement0(xa), yields: % 40.69/16.36 | (178) ? [v0] : (sdtasdt0(xa, v0) = xa & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (93) with sz00, all_0_13_13, xa and discharging atoms slsdtgt0(xa) = all_0_13_13, aElementOf0(sz00, all_0_13_13), aElement0(xa), yields: % 40.69/16.36 | (179) ? [v0] : (sdtasdt0(xa, v0) = sz00 & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (92) with xa, xc and discharging atoms doDivides0(xc, xa), aElement0(xc), aElement0(xa), yields: % 40.69/16.36 | (180) ? [v0] : (sdtasdt0(xc, v0) = xa & aElement0(v0)) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with xa, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(xa), yields: % 40.69/16.36 | (181) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xa) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_4_4, xa and discharging atoms aElement0(all_0_4_4), aElement0(xa), yields: % 40.69/16.36 | (182) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, xa) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (135) with all_0_14_14, sz10 and discharging atoms smndt0(sz10) = all_0_14_14, aElement0(sz10), yields: % 40.69/16.36 | (183) aElement0(all_0_14_14) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_0_0, sz10 and discharging atoms aElement0(all_0_0_0), aElement0(sz10), yields: % 40.69/16.36 | (184) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_0_0) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_1_1, sz10 and discharging atoms aElement0(all_0_1_1), aElement0(sz10), yields: % 40.69/16.36 | (185) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_1_1) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_2_2, sz10 and discharging atoms aElement0(all_0_2_2), aElement0(sz10), yields: % 40.69/16.36 | (186) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_2_2) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with sz10, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(sz10), yields: % 40.69/16.36 | (187) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz10) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.36 | Instantiating formula (156) with all_0_3_3, sz10 and discharging atoms aElement0(all_0_3_3), aElement0(sz10), yields: % 40.69/16.36 | (188) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_3_3) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.36 | % 40.69/16.37 | Instantiating formula (156) with all_0_4_4, sz10 and discharging atoms aElement0(all_0_4_4), aElement0(sz10), yields: % 40.69/16.37 | (189) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with all_0_5_5, sz10 and discharging atoms aElement0(all_0_5_5), aElement0(sz10), yields: % 40.69/16.37 | (190) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_5_5) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with xc, sz10 and discharging atoms aElement0(xc), aElement0(sz10), yields: % 40.69/16.37 | (191) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xc) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with xb, sz10 and discharging atoms aElement0(xb), aElement0(sz10), yields: % 40.69/16.37 | (192) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xb) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with xa, sz10 and discharging atoms aElement0(xa), aElement0(sz10), yields: % 40.69/16.37 | (193) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xa) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz10, sz10 and discharging atoms aElement0(sz10), yields: % 40.69/16.37 | (194) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz10) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_0_0 and discharging atoms aElement0(all_0_0_0), aElement0(sz00), yields: % 40.69/16.37 | (195) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_0_0) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_1_1 and discharging atoms aElement0(all_0_1_1), aElement0(sz00), yields: % 40.69/16.37 | (196) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_1_1) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_2_2 and discharging atoms aElement0(all_0_2_2), aElement0(sz00), yields: % 40.69/16.37 | (197) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_2_2) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_3_3 and discharging atoms aElement0(all_0_3_3), aElement0(sz00), yields: % 40.69/16.37 | (198) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_3_3) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_4_4 and discharging atoms aElement0(all_0_4_4), aElement0(sz00), yields: % 40.69/16.37 | (199) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_4_4) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with all_0_4_4, sz00 and discharging atoms aElement0(all_0_4_4), aElement0(sz00), yields: % 40.69/16.37 | (200) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, sz00) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, all_0_5_5 and discharging atoms aElement0(all_0_5_5), aElement0(sz00), yields: % 40.69/16.37 | (201) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_0_5_5) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, xc and discharging atoms aElement0(xc), aElement0(sz00), yields: % 40.69/16.37 | (202) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, xc) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, xb and discharging atoms aElement0(xb), aElement0(sz00), yields: % 40.69/16.37 | (203) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, xb) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, xa and discharging atoms aElement0(xa), aElement0(sz00), yields: % 40.69/16.37 | (204) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, xa) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, sz10 and discharging atoms aElement0(sz10), aElement0(sz00), yields: % 40.69/16.37 | (205) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, sz10) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating formula (156) with sz00, sz00 and discharging atoms aElement0(sz00), yields: % 40.69/16.37 | (206) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, sz00) = v0 & sdtpldt0(v0, v1) = v2) % 40.69/16.37 | % 40.69/16.37 | Instantiating (179) with all_17_0_27 yields: % 40.69/16.37 | (207) sdtasdt0(xa, all_17_0_27) = sz00 & aElement0(all_17_0_27) % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (207) yields: % 40.69/16.37 | (208) sdtasdt0(xa, all_17_0_27) = sz00 % 40.69/16.37 | (209) aElement0(all_17_0_27) % 40.69/16.37 | % 40.69/16.37 | Instantiating (171) with all_19_0_28 yields: % 40.69/16.37 | (210) sdtasdt0(xb, all_19_0_28) = sz00 & aElement0(all_19_0_28) % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (210) yields: % 40.69/16.37 | (211) sdtasdt0(xb, all_19_0_28) = sz00 % 40.69/16.37 | (212) aElement0(all_19_0_28) % 40.69/16.37 | % 40.69/16.37 | Instantiating (169) with all_23_0_31 yields: % 40.69/16.37 | (213) sdtasdt0(xb, all_23_0_31) = all_0_9_9 & aElement0(all_23_0_31) % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (213) yields: % 40.69/16.37 | (214) sdtasdt0(xb, all_23_0_31) = all_0_9_9 % 40.69/16.37 | (215) aElement0(all_23_0_31) % 40.69/16.37 | % 40.69/16.37 | Instantiating (163) with all_41_0_56, all_41_1_57, all_41_2_58 yields: % 40.69/16.37 | (216) ~ (all_41_0_56 = xu) & sdtasdt0(xb, all_0_4_4) = all_41_1_57 & sdtasdt0(xa, all_0_3_3) = all_41_2_58 & sdtpldt0(all_41_2_58, all_41_1_57) = all_41_0_56 % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (216) yields: % 40.69/16.37 | (217) ~ (all_41_0_56 = xu) % 40.69/16.37 | (218) sdtasdt0(xb, all_0_4_4) = all_41_1_57 % 40.69/16.37 | (219) sdtasdt0(xa, all_0_3_3) = all_41_2_58 % 40.69/16.37 | (220) sdtpldt0(all_41_2_58, all_41_1_57) = all_41_0_56 % 40.69/16.37 | % 40.69/16.37 | Instantiating (193) with all_51_0_69, all_51_1_70, all_51_2_71 yields: % 40.69/16.37 | (221) ~ (all_51_0_69 = xu) & sdtasdt0(xb, xa) = all_51_1_70 & sdtasdt0(xa, sz10) = all_51_2_71 & sdtpldt0(all_51_2_71, all_51_1_70) = all_51_0_69 % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (221) yields: % 40.69/16.37 | (222) ~ (all_51_0_69 = xu) % 40.69/16.37 | (223) sdtasdt0(xb, xa) = all_51_1_70 % 40.69/16.37 | (224) sdtasdt0(xa, sz10) = all_51_2_71 % 40.69/16.37 | (225) sdtpldt0(all_51_2_71, all_51_1_70) = all_51_0_69 % 40.69/16.37 | % 40.69/16.37 | Instantiating (192) with all_53_0_72, all_53_1_73, all_53_2_74 yields: % 40.69/16.37 | (226) ~ (all_53_0_72 = xu) & sdtasdt0(xb, xb) = all_53_1_73 & sdtasdt0(xa, sz10) = all_53_2_74 & sdtpldt0(all_53_2_74, all_53_1_73) = all_53_0_72 % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (226) yields: % 40.69/16.37 | (227) ~ (all_53_0_72 = xu) % 40.69/16.37 | (228) sdtasdt0(xb, xb) = all_53_1_73 % 40.69/16.37 | (229) sdtasdt0(xa, sz10) = all_53_2_74 % 40.69/16.37 | (230) sdtpldt0(all_53_2_74, all_53_1_73) = all_53_0_72 % 40.69/16.37 | % 40.69/16.37 | Instantiating (167) with all_79_0_107, all_79_1_108, all_79_2_109 yields: % 40.69/16.37 | (231) ~ (all_79_0_107 = xu) & sdtasdt0(xb, xc) = all_79_1_108 & sdtasdt0(xa, all_0_3_3) = all_79_2_109 & sdtpldt0(all_79_2_109, all_79_1_108) = all_79_0_107 % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (231) yields: % 40.69/16.37 | (232) ~ (all_79_0_107 = xu) % 40.69/16.37 | (233) sdtasdt0(xb, xc) = all_79_1_108 % 40.69/16.37 | (234) sdtasdt0(xa, all_0_3_3) = all_79_2_109 % 40.69/16.37 | (235) sdtpldt0(all_79_2_109, all_79_1_108) = all_79_0_107 % 40.69/16.37 | % 40.69/16.37 | Instantiating (164) with all_95_0_129, all_95_1_130, all_95_2_131 yields: % 40.69/16.37 | (236) ~ (all_95_0_129 = xu) & sdtasdt0(xb, all_0_5_5) = all_95_1_130 & sdtasdt0(xa, all_0_3_3) = all_95_2_131 & sdtpldt0(all_95_2_131, all_95_1_130) = all_95_0_129 % 40.69/16.37 | % 40.69/16.37 | Applying alpha-rule on (236) yields: % 40.69/16.37 | (237) ~ (all_95_0_129 = xu) % 40.69/16.37 | (238) sdtasdt0(xb, all_0_5_5) = all_95_1_130 % 40.69/16.37 | (239) sdtasdt0(xa, all_0_3_3) = all_95_2_131 % 40.69/16.37 | (240) sdtpldt0(all_95_2_131, all_95_1_130) = all_95_0_129 % 40.69/16.37 | % 40.69/16.38 | Instantiating (190) with all_97_0_132, all_97_1_133, all_97_2_134 yields: % 40.69/16.38 | (241) ~ (all_97_0_132 = xu) & sdtasdt0(xb, all_0_5_5) = all_97_1_133 & sdtasdt0(xa, sz10) = all_97_2_134 & sdtpldt0(all_97_2_134, all_97_1_133) = all_97_0_132 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (241) yields: % 40.69/16.38 | (242) ~ (all_97_0_132 = xu) % 40.69/16.38 | (243) sdtasdt0(xb, all_0_5_5) = all_97_1_133 % 40.69/16.38 | (244) sdtasdt0(xa, sz10) = all_97_2_134 % 40.69/16.38 | (245) sdtpldt0(all_97_2_134, all_97_1_133) = all_97_0_132 % 40.69/16.38 | % 40.69/16.38 | Instantiating (189) with all_113_0_156, all_113_1_157, all_113_2_158 yields: % 40.69/16.38 | (246) ~ (all_113_0_156 = xu) & sdtasdt0(xb, all_0_4_4) = all_113_1_157 & sdtasdt0(xa, sz10) = all_113_2_158 & sdtpldt0(all_113_2_158, all_113_1_157) = all_113_0_156 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (246) yields: % 40.69/16.38 | (247) ~ (all_113_0_156 = xu) % 40.69/16.38 | (248) sdtasdt0(xb, all_0_4_4) = all_113_1_157 % 40.69/16.38 | (249) sdtasdt0(xa, sz10) = all_113_2_158 % 40.69/16.38 | (250) sdtpldt0(all_113_2_158, all_113_1_157) = all_113_0_156 % 40.69/16.38 | % 40.69/16.38 | Instantiating (191) with all_115_0_159, all_115_1_160, all_115_2_161 yields: % 40.69/16.38 | (251) ~ (all_115_0_159 = xu) & sdtasdt0(xb, xc) = all_115_1_160 & sdtasdt0(xa, sz10) = all_115_2_161 & sdtpldt0(all_115_2_161, all_115_1_160) = all_115_0_159 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (251) yields: % 40.69/16.38 | (252) ~ (all_115_0_159 = xu) % 40.69/16.38 | (253) sdtasdt0(xb, xc) = all_115_1_160 % 40.69/16.38 | (254) sdtasdt0(xa, sz10) = all_115_2_161 % 40.69/16.38 | (255) sdtpldt0(all_115_2_161, all_115_1_160) = all_115_0_159 % 40.69/16.38 | % 40.69/16.38 | Instantiating (188) with all_117_0_162, all_117_1_163, all_117_2_164 yields: % 40.69/16.38 | (256) ~ (all_117_0_162 = xu) & sdtasdt0(xb, all_0_3_3) = all_117_1_163 & sdtasdt0(xa, sz10) = all_117_2_164 & sdtpldt0(all_117_2_164, all_117_1_163) = all_117_0_162 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (256) yields: % 40.69/16.38 | (257) ~ (all_117_0_162 = xu) % 40.69/16.38 | (258) sdtasdt0(xb, all_0_3_3) = all_117_1_163 % 40.69/16.38 | (259) sdtasdt0(xa, sz10) = all_117_2_164 % 40.69/16.38 | (260) sdtpldt0(all_117_2_164, all_117_1_163) = all_117_0_162 % 40.69/16.38 | % 40.69/16.38 | Instantiating (187) with all_119_0_165, all_119_1_166, all_119_2_167 yields: % 40.69/16.38 | (261) ~ (all_119_0_165 = xu) & sdtasdt0(xb, sz10) = all_119_1_166 & sdtasdt0(xa, all_0_3_3) = all_119_2_167 & sdtpldt0(all_119_2_167, all_119_1_166) = all_119_0_165 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (261) yields: % 40.69/16.38 | (262) ~ (all_119_0_165 = xu) % 40.69/16.38 | (263) sdtasdt0(xb, sz10) = all_119_1_166 % 40.69/16.38 | (264) sdtasdt0(xa, all_0_3_3) = all_119_2_167 % 40.69/16.38 | (265) sdtpldt0(all_119_2_167, all_119_1_166) = all_119_0_165 % 40.69/16.38 | % 40.69/16.38 | Instantiating (185) with all_121_0_168, all_121_1_169, all_121_2_170 yields: % 40.69/16.38 | (266) ~ (all_121_0_168 = xu) & sdtasdt0(xb, all_0_1_1) = all_121_1_169 & sdtasdt0(xa, sz10) = all_121_2_170 & sdtpldt0(all_121_2_170, all_121_1_169) = all_121_0_168 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (266) yields: % 40.69/16.38 | (267) ~ (all_121_0_168 = xu) % 40.69/16.38 | (268) sdtasdt0(xb, all_0_1_1) = all_121_1_169 % 40.69/16.38 | (269) sdtasdt0(xa, sz10) = all_121_2_170 % 40.69/16.38 | (270) sdtpldt0(all_121_2_170, all_121_1_169) = all_121_0_168 % 40.69/16.38 | % 40.69/16.38 | Instantiating (184) with all_123_0_171, all_123_1_172, all_123_2_173 yields: % 40.69/16.38 | (271) ~ (all_123_0_171 = xu) & sdtasdt0(xb, all_0_0_0) = all_123_1_172 & sdtasdt0(xa, sz10) = all_123_2_173 & sdtpldt0(all_123_2_173, all_123_1_172) = all_123_0_171 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (271) yields: % 40.69/16.38 | (272) ~ (all_123_0_171 = xu) % 40.69/16.38 | (273) sdtasdt0(xb, all_0_0_0) = all_123_1_172 % 40.69/16.38 | (274) sdtasdt0(xa, sz10) = all_123_2_173 % 40.69/16.38 | (275) sdtpldt0(all_123_2_173, all_123_1_172) = all_123_0_171 % 40.69/16.38 | % 40.69/16.38 | Instantiating (206) with all_129_0_180, all_129_1_181, all_129_2_182 yields: % 40.69/16.38 | (276) ~ (all_129_0_180 = xu) & sdtasdt0(xb, sz00) = all_129_1_181 & sdtasdt0(xa, sz00) = all_129_2_182 & sdtpldt0(all_129_2_182, all_129_1_181) = all_129_0_180 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (276) yields: % 40.69/16.38 | (277) ~ (all_129_0_180 = xu) % 40.69/16.38 | (278) sdtasdt0(xb, sz00) = all_129_1_181 % 40.69/16.38 | (279) sdtasdt0(xa, sz00) = all_129_2_182 % 40.69/16.38 | (280) sdtpldt0(all_129_2_182, all_129_1_181) = all_129_0_180 % 40.69/16.38 | % 40.69/16.38 | Instantiating (201) with all_133_0_186, all_133_1_187, all_133_2_188 yields: % 40.69/16.38 | (281) ~ (all_133_0_186 = xu) & sdtasdt0(xb, sz00) = all_133_1_187 & sdtasdt0(xa, all_0_5_5) = all_133_2_188 & sdtpldt0(all_133_2_188, all_133_1_187) = all_133_0_186 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (281) yields: % 40.69/16.38 | (282) ~ (all_133_0_186 = xu) % 40.69/16.38 | (283) sdtasdt0(xb, sz00) = all_133_1_187 % 40.69/16.38 | (284) sdtasdt0(xa, all_0_5_5) = all_133_2_188 % 40.69/16.38 | (285) sdtpldt0(all_133_2_188, all_133_1_187) = all_133_0_186 % 40.69/16.38 | % 40.69/16.38 | Instantiating (200) with all_135_0_189, all_135_1_190, all_135_2_191 yields: % 40.69/16.38 | (286) ~ (all_135_0_189 = xu) & sdtasdt0(xb, all_0_4_4) = all_135_1_190 & sdtasdt0(xa, sz00) = all_135_2_191 & sdtpldt0(all_135_2_191, all_135_1_190) = all_135_0_189 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (286) yields: % 40.69/16.38 | (287) ~ (all_135_0_189 = xu) % 40.69/16.38 | (288) sdtasdt0(xb, all_0_4_4) = all_135_1_190 % 40.69/16.38 | (289) sdtasdt0(xa, sz00) = all_135_2_191 % 40.69/16.38 | (290) sdtpldt0(all_135_2_191, all_135_1_190) = all_135_0_189 % 40.69/16.38 | % 40.69/16.38 | Instantiating (198) with all_137_0_192, all_137_1_193, all_137_2_194 yields: % 40.69/16.38 | (291) ~ (all_137_0_192 = xu) & sdtasdt0(xb, sz00) = all_137_1_193 & sdtasdt0(xa, all_0_3_3) = all_137_2_194 & sdtpldt0(all_137_2_194, all_137_1_193) = all_137_0_192 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (291) yields: % 40.69/16.38 | (292) ~ (all_137_0_192 = xu) % 40.69/16.38 | (293) sdtasdt0(xb, sz00) = all_137_1_193 % 40.69/16.38 | (294) sdtasdt0(xa, all_0_3_3) = all_137_2_194 % 40.69/16.38 | (295) sdtpldt0(all_137_2_194, all_137_1_193) = all_137_0_192 % 40.69/16.38 | % 40.69/16.38 | Instantiating (197) with all_139_0_195, all_139_1_196, all_139_2_197 yields: % 40.69/16.38 | (296) ~ (all_139_0_195 = xu) & sdtasdt0(xb, sz00) = all_139_1_196 & sdtasdt0(xa, all_0_2_2) = all_139_2_197 & sdtpldt0(all_139_2_197, all_139_1_196) = all_139_0_195 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (296) yields: % 40.69/16.38 | (297) ~ (all_139_0_195 = xu) % 40.69/16.38 | (298) sdtasdt0(xb, sz00) = all_139_1_196 % 40.69/16.38 | (299) sdtasdt0(xa, all_0_2_2) = all_139_2_197 % 40.69/16.38 | (300) sdtpldt0(all_139_2_197, all_139_1_196) = all_139_0_195 % 40.69/16.38 | % 40.69/16.38 | Instantiating (205) with all_141_0_198, all_141_1_199, all_141_2_200 yields: % 40.69/16.38 | (301) ~ (all_141_0_198 = xu) & sdtasdt0(xb, sz00) = all_141_1_199 & sdtasdt0(xa, sz10) = all_141_2_200 & sdtpldt0(all_141_2_200, all_141_1_199) = all_141_0_198 % 40.69/16.38 | % 40.69/16.38 | Applying alpha-rule on (301) yields: % 40.69/16.38 | (302) ~ (all_141_0_198 = xu) % 41.07/16.38 | (303) sdtasdt0(xb, sz00) = all_141_1_199 % 41.07/16.38 | (304) sdtasdt0(xa, sz10) = all_141_2_200 % 41.07/16.38 | (305) sdtpldt0(all_141_2_200, all_141_1_199) = all_141_0_198 % 41.07/16.38 | % 41.07/16.38 | Instantiating (199) with all_149_0_210, all_149_1_211, all_149_2_212 yields: % 41.07/16.38 | (306) ~ (all_149_0_210 = xu) & sdtasdt0(xb, sz00) = all_149_1_211 & sdtasdt0(xa, all_0_4_4) = all_149_2_212 & sdtpldt0(all_149_2_212, all_149_1_211) = all_149_0_210 % 41.07/16.38 | % 41.07/16.38 | Applying alpha-rule on (306) yields: % 41.07/16.38 | (307) ~ (all_149_0_210 = xu) % 41.07/16.38 | (308) sdtasdt0(xb, sz00) = all_149_1_211 % 41.07/16.38 | (309) sdtasdt0(xa, all_0_4_4) = all_149_2_212 % 41.07/16.38 | (310) sdtpldt0(all_149_2_212, all_149_1_211) = all_149_0_210 % 41.07/16.38 | % 41.07/16.38 | Instantiating (186) with all_157_0_222, all_157_1_223, all_157_2_224 yields: % 41.07/16.38 | (311) ~ (all_157_0_222 = xu) & sdtasdt0(xb, all_0_2_2) = all_157_1_223 & sdtasdt0(xa, sz10) = all_157_2_224 & sdtpldt0(all_157_2_224, all_157_1_223) = all_157_0_222 % 41.07/16.38 | % 41.07/16.38 | Applying alpha-rule on (311) yields: % 41.07/16.38 | (312) ~ (all_157_0_222 = xu) % 41.07/16.38 | (313) sdtasdt0(xb, all_0_2_2) = all_157_1_223 % 41.07/16.38 | (314) sdtasdt0(xa, sz10) = all_157_2_224 % 41.07/16.38 | (315) sdtpldt0(all_157_2_224, all_157_1_223) = all_157_0_222 % 41.07/16.38 | % 41.07/16.38 | Instantiating (203) with all_163_0_231, all_163_1_232, all_163_2_233 yields: % 41.07/16.38 | (316) ~ (all_163_0_231 = xu) & sdtasdt0(xb, sz00) = all_163_1_232 & sdtasdt0(xa, xb) = all_163_2_233 & sdtpldt0(all_163_2_233, all_163_1_232) = all_163_0_231 % 41.07/16.38 | % 41.07/16.38 | Applying alpha-rule on (316) yields: % 41.07/16.38 | (317) ~ (all_163_0_231 = xu) % 41.07/16.38 | (318) sdtasdt0(xb, sz00) = all_163_1_232 % 41.07/16.38 | (319) sdtasdt0(xa, xb) = all_163_2_233 % 41.07/16.38 | (320) sdtpldt0(all_163_2_233, all_163_1_232) = all_163_0_231 % 41.07/16.38 | % 41.07/16.38 | Instantiating (202) with all_167_0_237, all_167_1_238, all_167_2_239 yields: % 41.07/16.38 | (321) ~ (all_167_0_237 = xu) & sdtasdt0(xb, sz00) = all_167_1_238 & sdtasdt0(xa, xc) = all_167_2_239 & sdtpldt0(all_167_2_239, all_167_1_238) = all_167_0_237 % 41.07/16.38 | % 41.07/16.38 | Applying alpha-rule on (321) yields: % 41.07/16.38 | (322) ~ (all_167_0_237 = xu) % 41.07/16.38 | (323) sdtasdt0(xb, sz00) = all_167_1_238 % 41.07/16.38 | (324) sdtasdt0(xa, xc) = all_167_2_239 % 41.07/16.38 | (325) sdtpldt0(all_167_2_239, all_167_1_238) = all_167_0_237 % 41.07/16.38 | % 41.07/16.38 | Instantiating (196) with all_171_0_243, all_171_1_244, all_171_2_245 yields: % 41.07/16.38 | (326) ~ (all_171_0_243 = xu) & sdtasdt0(xb, sz00) = all_171_1_244 & sdtasdt0(xa, all_0_1_1) = all_171_2_245 & sdtpldt0(all_171_2_245, all_171_1_244) = all_171_0_243 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (326) yields: % 41.07/16.39 | (327) ~ (all_171_0_243 = xu) % 41.07/16.39 | (328) sdtasdt0(xb, sz00) = all_171_1_244 % 41.07/16.39 | (329) sdtasdt0(xa, all_0_1_1) = all_171_2_245 % 41.07/16.39 | (330) sdtpldt0(all_171_2_245, all_171_1_244) = all_171_0_243 % 41.07/16.39 | % 41.07/16.39 | Instantiating (204) with all_175_0_249, all_175_1_250, all_175_2_251 yields: % 41.07/16.39 | (331) ~ (all_175_0_249 = xu) & sdtasdt0(xb, sz00) = all_175_1_250 & sdtasdt0(xa, xa) = all_175_2_251 & sdtpldt0(all_175_2_251, all_175_1_250) = all_175_0_249 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (331) yields: % 41.07/16.39 | (332) ~ (all_175_0_249 = xu) % 41.07/16.39 | (333) sdtasdt0(xb, sz00) = all_175_1_250 % 41.07/16.39 | (334) sdtasdt0(xa, xa) = all_175_2_251 % 41.07/16.39 | (335) sdtpldt0(all_175_2_251, all_175_1_250) = all_175_0_249 % 41.07/16.39 | % 41.07/16.39 | Instantiating (177) with all_181_0_257 yields: % 41.07/16.39 | (336) sdtasdt0(xa, all_181_0_257) = all_0_10_10 & aElement0(all_181_0_257) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (336) yields: % 41.07/16.39 | (337) sdtasdt0(xa, all_181_0_257) = all_0_10_10 % 41.07/16.39 | (338) aElement0(all_181_0_257) % 41.07/16.39 | % 41.07/16.39 | Instantiating (178) with all_183_0_258 yields: % 41.07/16.39 | (339) sdtasdt0(xa, all_183_0_258) = xa & aElement0(all_183_0_258) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (339) yields: % 41.07/16.39 | (340) sdtasdt0(xa, all_183_0_258) = xa % 41.07/16.39 | (341) aElement0(all_183_0_258) % 41.07/16.39 | % 41.07/16.39 | Instantiating (170) with all_185_0_259 yields: % 41.07/16.39 | (342) sdtasdt0(xb, all_185_0_259) = xb & aElement0(all_185_0_259) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (342) yields: % 41.07/16.39 | (343) sdtasdt0(xb, all_185_0_259) = xb % 41.07/16.39 | (344) aElement0(all_185_0_259) % 41.07/16.39 | % 41.07/16.39 | Instantiating (195) with all_187_0_260, all_187_1_261, all_187_2_262 yields: % 41.07/16.39 | (345) ~ (all_187_0_260 = xu) & sdtasdt0(xb, sz00) = all_187_1_261 & sdtasdt0(xa, all_0_0_0) = all_187_2_262 & sdtpldt0(all_187_2_262, all_187_1_261) = all_187_0_260 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (345) yields: % 41.07/16.39 | (346) ~ (all_187_0_260 = xu) % 41.07/16.39 | (347) sdtasdt0(xb, sz00) = all_187_1_261 % 41.07/16.39 | (348) sdtasdt0(xa, all_0_0_0) = all_187_2_262 % 41.07/16.39 | (349) sdtpldt0(all_187_2_262, all_187_1_261) = all_187_0_260 % 41.07/16.39 | % 41.07/16.39 | Instantiating (173) with all_199_0_278, all_199_1_279, all_199_2_280 yields: % 41.07/16.39 | (350) ~ (all_199_0_278 = xu) & sdtasdt0(xb, xb) = all_199_1_279 & sdtasdt0(xa, all_0_3_3) = all_199_2_280 & sdtpldt0(all_199_2_280, all_199_1_279) = all_199_0_278 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (350) yields: % 41.07/16.39 | (351) ~ (all_199_0_278 = xu) % 41.07/16.39 | (352) sdtasdt0(xb, xb) = all_199_1_279 % 41.07/16.39 | (353) sdtasdt0(xa, all_0_3_3) = all_199_2_280 % 41.07/16.39 | (354) sdtpldt0(all_199_2_280, all_199_1_279) = all_199_0_278 % 41.07/16.39 | % 41.07/16.39 | Instantiating (182) with all_203_0_284, all_203_1_285, all_203_2_286 yields: % 41.07/16.39 | (355) ~ (all_203_0_284 = xu) & sdtasdt0(xb, all_0_4_4) = all_203_1_285 & sdtasdt0(xa, xa) = all_203_2_286 & sdtpldt0(all_203_2_286, all_203_1_285) = all_203_0_284 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (355) yields: % 41.07/16.39 | (356) ~ (all_203_0_284 = xu) % 41.07/16.39 | (357) sdtasdt0(xb, all_0_4_4) = all_203_1_285 % 41.07/16.39 | (358) sdtasdt0(xa, xa) = all_203_2_286 % 41.07/16.39 | (359) sdtpldt0(all_203_2_286, all_203_1_285) = all_203_0_284 % 41.07/16.39 | % 41.07/16.39 | Instantiating (174) with all_211_0_296, all_211_1_297, all_211_2_298 yields: % 41.07/16.39 | (360) ~ (all_211_0_296 = xu) & sdtasdt0(xb, all_0_4_4) = all_211_1_297 & sdtasdt0(xa, xb) = all_211_2_298 & sdtpldt0(all_211_2_298, all_211_1_297) = all_211_0_296 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (360) yields: % 41.07/16.39 | (361) ~ (all_211_0_296 = xu) % 41.07/16.39 | (362) sdtasdt0(xb, all_0_4_4) = all_211_1_297 % 41.07/16.39 | (363) sdtasdt0(xa, xb) = all_211_2_298 % 41.07/16.39 | (364) sdtpldt0(all_211_2_298, all_211_1_297) = all_211_0_296 % 41.07/16.39 | % 41.07/16.39 | Instantiating (165) with all_215_0_302, all_215_1_303, all_215_2_304 yields: % 41.07/16.39 | (365) ~ (all_215_0_302 = xu) & sdtasdt0(xb, all_0_4_4) = all_215_1_303 & sdtasdt0(xa, all_0_5_5) = all_215_2_304 & sdtpldt0(all_215_2_304, all_215_1_303) = all_215_0_302 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (365) yields: % 41.07/16.39 | (366) ~ (all_215_0_302 = xu) % 41.07/16.39 | (367) sdtasdt0(xb, all_0_4_4) = all_215_1_303 % 41.07/16.39 | (368) sdtasdt0(xa, all_0_5_5) = all_215_2_304 % 41.07/16.39 | (369) sdtpldt0(all_215_2_304, all_215_1_303) = all_215_0_302 % 41.07/16.39 | % 41.07/16.39 | Instantiating (160) with all_225_0_313, all_225_1_314, all_225_2_315 yields: % 41.07/16.39 | (370) ~ (all_225_0_313 = xu) & sdtasdt0(xb, all_0_1_1) = all_225_1_314 & sdtasdt0(xa, all_0_3_3) = all_225_2_315 & sdtpldt0(all_225_2_315, all_225_1_314) = all_225_0_313 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (370) yields: % 41.07/16.39 | (371) ~ (all_225_0_313 = xu) % 41.07/16.39 | (372) sdtasdt0(xb, all_0_1_1) = all_225_1_314 % 41.07/16.39 | (373) sdtasdt0(xa, all_0_3_3) = all_225_2_315 % 41.07/16.39 | (374) sdtpldt0(all_225_2_315, all_225_1_314) = all_225_0_313 % 41.07/16.39 | % 41.07/16.39 | Instantiating (181) with all_231_0_318, all_231_1_319, all_231_2_320 yields: % 41.07/16.39 | (375) ~ (all_231_0_318 = xu) & sdtasdt0(xb, xa) = all_231_1_319 & sdtasdt0(xa, all_0_3_3) = all_231_2_320 & sdtpldt0(all_231_2_320, all_231_1_319) = all_231_0_318 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (375) yields: % 41.07/16.39 | (376) ~ (all_231_0_318 = xu) % 41.07/16.39 | (377) sdtasdt0(xb, xa) = all_231_1_319 % 41.07/16.39 | (378) sdtasdt0(xa, all_0_3_3) = all_231_2_320 % 41.07/16.39 | (379) sdtpldt0(all_231_2_320, all_231_1_319) = all_231_0_318 % 41.07/16.39 | % 41.07/16.39 | Instantiating (166) with all_235_0_324 yields: % 41.07/16.39 | (380) sdtasdt0(xc, all_235_0_324) = xc & aElement0(all_235_0_324) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (380) yields: % 41.07/16.39 | (381) sdtasdt0(xc, all_235_0_324) = xc % 41.07/16.39 | (382) aElement0(all_235_0_324) % 41.07/16.39 | % 41.07/16.39 | Instantiating (194) with all_257_0_355, all_257_1_356, all_257_2_357 yields: % 41.07/16.39 | (383) ~ (all_257_0_355 = xu) & sdtasdt0(xb, sz10) = all_257_1_356 & sdtasdt0(xa, sz10) = all_257_2_357 & sdtpldt0(all_257_2_357, all_257_1_356) = all_257_0_355 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (383) yields: % 41.07/16.39 | (384) ~ (all_257_0_355 = xu) % 41.07/16.39 | (385) sdtasdt0(xb, sz10) = all_257_1_356 % 41.07/16.39 | (386) sdtasdt0(xa, sz10) = all_257_2_357 % 41.07/16.39 | (387) sdtpldt0(all_257_2_357, all_257_1_356) = all_257_0_355 % 41.07/16.39 | % 41.07/16.39 | Instantiating (172) with all_261_0_361 yields: % 41.07/16.39 | (388) sdtasdt0(xc, all_261_0_361) = xb & aElement0(all_261_0_361) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (388) yields: % 41.07/16.39 | (389) sdtasdt0(xc, all_261_0_361) = xb % 41.07/16.39 | (390) aElement0(all_261_0_361) % 41.07/16.39 | % 41.07/16.39 | Instantiating (159) with all_265_0_365, all_265_1_366, all_265_2_367 yields: % 41.07/16.39 | (391) ~ (all_265_0_365 = xu) & sdtasdt0(xb, all_0_0_0) = all_265_1_366 & sdtasdt0(xa, all_0_3_3) = all_265_2_367 & sdtpldt0(all_265_2_367, all_265_1_366) = all_265_0_365 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (391) yields: % 41.07/16.39 | (392) ~ (all_265_0_365 = xu) % 41.07/16.39 | (393) sdtasdt0(xb, all_0_0_0) = all_265_1_366 % 41.07/16.39 | (394) sdtasdt0(xa, all_0_3_3) = all_265_2_367 % 41.07/16.39 | (395) sdtpldt0(all_265_2_367, all_265_1_366) = all_265_0_365 % 41.07/16.39 | % 41.07/16.39 | Instantiating (176) with all_267_0_368 yields: % 41.07/16.39 | (396) sdtasdt0(xa, all_267_0_368) = all_0_7_7 & aElement0(all_267_0_368) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (396) yields: % 41.07/16.39 | (397) sdtasdt0(xa, all_267_0_368) = all_0_7_7 % 41.07/16.39 | (398) aElement0(all_267_0_368) % 41.07/16.39 | % 41.07/16.39 | Instantiating (161) with all_269_0_369, all_269_1_370, all_269_2_371 yields: % 41.07/16.39 | (399) ~ (all_269_0_369 = xu) & sdtasdt0(xb, all_0_2_2) = all_269_1_370 & sdtasdt0(xa, all_0_3_3) = all_269_2_371 & sdtpldt0(all_269_2_371, all_269_1_370) = all_269_0_369 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (399) yields: % 41.07/16.39 | (400) ~ (all_269_0_369 = xu) % 41.07/16.39 | (401) sdtasdt0(xb, all_0_2_2) = all_269_1_370 % 41.07/16.39 | (402) sdtasdt0(xa, all_0_3_3) = all_269_2_371 % 41.07/16.39 | (403) sdtpldt0(all_269_2_371, all_269_1_370) = all_269_0_369 % 41.07/16.39 | % 41.07/16.39 | Instantiating (162) with all_271_0_372, all_271_1_373, all_271_2_374 yields: % 41.07/16.39 | (404) ~ (all_271_0_372 = xu) & sdtasdt0(xb, all_0_4_4) = all_271_1_373 & sdtasdt0(xa, all_0_0_0) = all_271_2_374 & sdtpldt0(all_271_2_374, all_271_1_373) = all_271_0_372 % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (404) yields: % 41.07/16.39 | (405) ~ (all_271_0_372 = xu) % 41.07/16.39 | (406) sdtasdt0(xb, all_0_4_4) = all_271_1_373 % 41.07/16.39 | (407) sdtasdt0(xa, all_0_0_0) = all_271_2_374 % 41.07/16.39 | (408) sdtpldt0(all_271_2_374, all_271_1_373) = all_271_0_372 % 41.07/16.39 | % 41.07/16.39 | Instantiating (180) with all_285_0_393 yields: % 41.07/16.39 | (409) sdtasdt0(xc, all_285_0_393) = xa & aElement0(all_285_0_393) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (409) yields: % 41.07/16.39 | (410) sdtasdt0(xc, all_285_0_393) = xa % 41.07/16.39 | (411) aElement0(all_285_0_393) % 41.07/16.39 | % 41.07/16.39 | Instantiating (168) with all_291_0_400 yields: % 41.07/16.39 | (412) sdtasdt0(xb, all_291_0_400) = all_0_6_6 & aElement0(all_291_0_400) % 41.07/16.39 | % 41.07/16.39 | Applying alpha-rule on (412) yields: % 41.07/16.39 | (413) sdtasdt0(xb, all_291_0_400) = all_0_6_6 % 41.07/16.39 | (414) aElement0(all_291_0_400) % 41.07/16.39 | % 41.07/16.39 | Instantiating formula (100) with xb, all_0_4_4, all_215_1_303, all_271_1_373 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_271_1_373, sdtasdt0(xb, all_0_4_4) = all_215_1_303, yields: % 41.07/16.40 | (415) all_271_1_373 = all_215_1_303 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_211_1_297, all_215_1_303 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_215_1_303, sdtasdt0(xb, all_0_4_4) = all_211_1_297, yields: % 41.07/16.40 | (416) all_215_1_303 = all_211_1_297 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_203_1_285, sz00 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_203_1_285, sdtasdt0(xb, all_0_4_4) = sz00, yields: % 41.07/16.40 | (417) all_203_1_285 = sz00 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_203_1_285, all_211_1_297 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_211_1_297, sdtasdt0(xb, all_0_4_4) = all_203_1_285, yields: % 41.07/16.40 | (418) all_211_1_297 = all_203_1_285 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_135_1_190, all_271_1_373 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_271_1_373, sdtasdt0(xb, all_0_4_4) = all_135_1_190, yields: % 41.07/16.40 | (419) all_271_1_373 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_113_1_157, all_211_1_297 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_211_1_297, sdtasdt0(xb, all_0_4_4) = all_113_1_157, yields: % 41.07/16.40 | (420) all_211_1_297 = all_113_1_157 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, all_0_4_4, all_41_1_57, all_113_1_157 and discharging atoms sdtasdt0(xb, all_0_4_4) = all_113_1_157, sdtasdt0(xb, all_0_4_4) = all_41_1_57, yields: % 41.07/16.40 | (421) all_113_1_157 = all_41_1_57 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_175_1_250, all_187_1_261 and discharging atoms sdtasdt0(xb, sz00) = all_187_1_261, sdtasdt0(xb, sz00) = all_175_1_250, yields: % 41.07/16.40 | (422) all_187_1_261 = all_175_1_250 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (42) with all_171_1_244, xb and discharging atoms sdtasdt0(xb, sz00) = all_171_1_244, aElement0(xb), yields: % 41.07/16.40 | (423) all_171_1_244 = sz00 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_167_1_238, all_171_1_244 and discharging atoms sdtasdt0(xb, sz00) = all_171_1_244, sdtasdt0(xb, sz00) = all_167_1_238, yields: % 41.07/16.40 | (424) all_171_1_244 = all_167_1_238 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_163_1_232, all_171_1_244 and discharging atoms sdtasdt0(xb, sz00) = all_171_1_244, sdtasdt0(xb, sz00) = all_163_1_232, yields: % 41.07/16.40 | (425) all_171_1_244 = all_163_1_232 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_149_1_211, all_187_1_261 and discharging atoms sdtasdt0(xb, sz00) = all_187_1_261, sdtasdt0(xb, sz00) = all_149_1_211, yields: % 41.07/16.40 | (426) all_187_1_261 = all_149_1_211 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_141_1_199, all_175_1_250 and discharging atoms sdtasdt0(xb, sz00) = all_175_1_250, sdtasdt0(xb, sz00) = all_141_1_199, yields: % 41.07/16.40 | (427) all_175_1_250 = all_141_1_199 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_139_1_196, all_163_1_232 and discharging atoms sdtasdt0(xb, sz00) = all_163_1_232, sdtasdt0(xb, sz00) = all_139_1_196, yields: % 41.07/16.40 | (428) all_163_1_232 = all_139_1_196 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_137_1_193, all_141_1_199 and discharging atoms sdtasdt0(xb, sz00) = all_141_1_199, sdtasdt0(xb, sz00) = all_137_1_193, yields: % 41.07/16.40 | (429) all_141_1_199 = all_137_1_193 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_137_1_193, all_139_1_196 and discharging atoms sdtasdt0(xb, sz00) = all_139_1_196, sdtasdt0(xb, sz00) = all_137_1_193, yields: % 41.07/16.40 | (430) all_139_1_196 = all_137_1_193 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_133_1_187, all_139_1_196 and discharging atoms sdtasdt0(xb, sz00) = all_139_1_196, sdtasdt0(xb, sz00) = all_133_1_187, yields: % 41.07/16.40 | (431) all_139_1_196 = all_133_1_187 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xb, sz00, all_129_1_181, all_175_1_250 and discharging atoms sdtasdt0(xb, sz00) = all_175_1_250, sdtasdt0(xb, sz00) = all_129_1_181, yields: % 41.07/16.40 | (432) all_175_1_250 = all_129_1_181 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_269_2_371, xa and discharging atoms sdtasdt0(xa, all_0_3_3) = all_269_2_371, sdtasdt0(xa, all_0_3_3) = xa, yields: % 41.07/16.40 | (433) all_269_2_371 = xa % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_265_2_367, all_269_2_371 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_269_2_371, sdtasdt0(xa, all_0_3_3) = all_265_2_367, yields: % 41.07/16.40 | (434) all_269_2_371 = all_265_2_367 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_225_2_315, all_265_2_367 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_265_2_367, sdtasdt0(xa, all_0_3_3) = all_225_2_315, yields: % 41.07/16.40 | (435) all_265_2_367 = all_225_2_315 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_199_2_280, all_231_2_320 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_231_2_320, sdtasdt0(xa, all_0_3_3) = all_199_2_280, yields: % 41.07/16.40 | (436) all_231_2_320 = all_199_2_280 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_199_2_280, all_225_2_315 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_225_2_315, sdtasdt0(xa, all_0_3_3) = all_199_2_280, yields: % 41.07/16.40 | (437) all_225_2_315 = all_199_2_280 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_137_2_194, all_231_2_320 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_231_2_320, sdtasdt0(xa, all_0_3_3) = all_137_2_194, yields: % 41.07/16.40 | (438) all_231_2_320 = all_137_2_194 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_119_2_167, all_199_2_280 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_199_2_280, sdtasdt0(xa, all_0_3_3) = all_119_2_167, yields: % 41.07/16.40 | (439) all_199_2_280 = all_119_2_167 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_95_2_131, all_119_2_167 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_119_2_167, sdtasdt0(xa, all_0_3_3) = all_95_2_131, yields: % 41.07/16.40 | (440) all_119_2_167 = all_95_2_131 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_79_2_109, all_95_2_131 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_95_2_131, sdtasdt0(xa, all_0_3_3) = all_79_2_109, yields: % 41.07/16.40 | (441) all_95_2_131 = all_79_2_109 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, all_0_3_3, all_41_2_58, all_79_2_109 and discharging atoms sdtasdt0(xa, all_0_3_3) = all_79_2_109, sdtasdt0(xa, all_0_3_3) = all_41_2_58, yields: % 41.07/16.40 | (442) all_79_2_109 = all_41_2_58 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_141_2_200, all_157_2_224 and discharging atoms sdtasdt0(xa, sz10) = all_157_2_224, sdtasdt0(xa, sz10) = all_141_2_200, yields: % 41.07/16.40 | (443) all_157_2_224 = all_141_2_200 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_123_2_173, all_141_2_200 and discharging atoms sdtasdt0(xa, sz10) = all_141_2_200, sdtasdt0(xa, sz10) = all_123_2_173, yields: % 41.07/16.40 | (444) all_141_2_200 = all_123_2_173 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_121_2_170, all_257_2_357 and discharging atoms sdtasdt0(xa, sz10) = all_257_2_357, sdtasdt0(xa, sz10) = all_121_2_170, yields: % 41.07/16.40 | (445) all_257_2_357 = all_121_2_170 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_121_2_170, all_123_2_173 and discharging atoms sdtasdt0(xa, sz10) = all_123_2_173, sdtasdt0(xa, sz10) = all_121_2_170, yields: % 41.07/16.40 | (446) all_123_2_173 = all_121_2_170 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_117_2_164, all_257_2_357 and discharging atoms sdtasdt0(xa, sz10) = all_257_2_357, sdtasdt0(xa, sz10) = all_117_2_164, yields: % 41.07/16.40 | (447) all_257_2_357 = all_117_2_164 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_115_2_161, all_157_2_224 and discharging atoms sdtasdt0(xa, sz10) = all_157_2_224, sdtasdt0(xa, sz10) = all_115_2_161, yields: % 41.07/16.40 | (448) all_157_2_224 = all_115_2_161 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_113_2_158, all_257_2_357 and discharging atoms sdtasdt0(xa, sz10) = all_257_2_357, sdtasdt0(xa, sz10) = all_113_2_158, yields: % 41.07/16.40 | (449) all_257_2_357 = all_113_2_158 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_97_2_134, all_257_2_357 and discharging atoms sdtasdt0(xa, sz10) = all_257_2_357, sdtasdt0(xa, sz10) = all_97_2_134, yields: % 41.07/16.40 | (450) all_257_2_357 = all_97_2_134 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_53_2_74, all_113_2_158 and discharging atoms sdtasdt0(xa, sz10) = all_113_2_158, sdtasdt0(xa, sz10) = all_53_2_74, yields: % 41.07/16.40 | (451) all_113_2_158 = all_53_2_74 % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (83) with all_53_2_74, xa and discharging atoms sdtasdt0(xa, sz10) = all_53_2_74, aElement0(xa), yields: % 41.07/16.40 | (452) all_53_2_74 = xa % 41.07/16.40 | % 41.07/16.40 | Instantiating formula (100) with xa, sz10, all_51_2_71, all_113_2_158 and discharging atoms sdtasdt0(xa, sz10) = all_113_2_158, sdtasdt0(xa, sz10) = all_51_2_71, yields: % 41.07/16.40 | (453) all_113_2_158 = all_51_2_71 % 41.07/16.40 | % 41.07/16.40 | Combining equations (415,419) yields a new equation: % 41.07/16.40 | (454) all_215_1_303 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Simplifying 454 yields: % 41.07/16.40 | (455) all_215_1_303 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Combining equations (434,433) yields a new equation: % 41.07/16.40 | (456) all_265_2_367 = xa % 41.07/16.40 | % 41.07/16.40 | Simplifying 456 yields: % 41.07/16.40 | (457) all_265_2_367 = xa % 41.07/16.40 | % 41.07/16.40 | Combining equations (435,457) yields a new equation: % 41.07/16.40 | (458) all_225_2_315 = xa % 41.07/16.40 | % 41.07/16.40 | Simplifying 458 yields: % 41.07/16.40 | (459) all_225_2_315 = xa % 41.07/16.40 | % 41.07/16.40 | Combining equations (449,447) yields a new equation: % 41.07/16.40 | (460) all_117_2_164 = all_113_2_158 % 41.07/16.40 | % 41.07/16.40 | Combining equations (445,447) yields a new equation: % 41.07/16.40 | (461) all_121_2_170 = all_117_2_164 % 41.07/16.40 | % 41.07/16.40 | Simplifying 461 yields: % 41.07/16.40 | (462) all_121_2_170 = all_117_2_164 % 41.07/16.40 | % 41.07/16.40 | Combining equations (450,447) yields a new equation: % 41.07/16.40 | (463) all_117_2_164 = all_97_2_134 % 41.07/16.40 | % 41.07/16.40 | Combining equations (436,438) yields a new equation: % 41.07/16.40 | (464) all_199_2_280 = all_137_2_194 % 41.07/16.40 | % 41.07/16.40 | Simplifying 464 yields: % 41.07/16.40 | (465) all_199_2_280 = all_137_2_194 % 41.07/16.40 | % 41.07/16.40 | Combining equations (437,459) yields a new equation: % 41.07/16.40 | (466) all_199_2_280 = xa % 41.07/16.40 | % 41.07/16.40 | Simplifying 466 yields: % 41.07/16.40 | (467) all_199_2_280 = xa % 41.07/16.40 | % 41.07/16.40 | Combining equations (416,455) yields a new equation: % 41.07/16.40 | (468) all_211_1_297 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Simplifying 468 yields: % 41.07/16.40 | (469) all_211_1_297 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Combining equations (418,469) yields a new equation: % 41.07/16.40 | (470) all_203_1_285 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Simplifying 470 yields: % 41.07/16.40 | (471) all_203_1_285 = all_135_1_190 % 41.07/16.40 | % 41.07/16.40 | Combining equations (420,469) yields a new equation: % 41.07/16.40 | (472) all_135_1_190 = all_113_1_157 % 41.07/16.40 | % 41.07/16.40 | Combining equations (471,417) yields a new equation: % 41.07/16.40 | (473) all_135_1_190 = sz00 % 41.07/16.40 | % 41.07/16.40 | Simplifying 473 yields: % 41.07/16.40 | (474) all_135_1_190 = sz00 % 41.07/16.40 | % 41.07/16.40 | Combining equations (467,465) yields a new equation: % 41.07/16.40 | (475) all_137_2_194 = xa % 41.07/16.40 | % 41.07/16.40 | Combining equations (439,465) yields a new equation: % 41.07/16.40 | (476) all_137_2_194 = all_119_2_167 % 41.07/16.40 | % 41.07/16.40 | Combining equations (422,426) yields a new equation: % 41.07/16.40 | (477) all_175_1_250 = all_149_1_211 % 41.07/16.40 | % 41.07/16.40 | Simplifying 477 yields: % 41.07/16.40 | (478) all_175_1_250 = all_149_1_211 % 41.07/16.40 | % 41.07/16.40 | Combining equations (427,478) yields a new equation: % 41.07/16.40 | (479) all_149_1_211 = all_141_1_199 % 41.07/16.40 | % 41.07/16.40 | Combining equations (432,478) yields a new equation: % 41.07/16.40 | (480) all_149_1_211 = all_129_1_181 % 41.07/16.40 | % 41.07/16.41 | Combining equations (425,424) yields a new equation: % 41.07/16.41 | (481) all_167_1_238 = all_163_1_232 % 41.07/16.41 | % 41.07/16.41 | Combining equations (423,424) yields a new equation: % 41.07/16.41 | (482) all_167_1_238 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (481,482) yields a new equation: % 41.07/16.41 | (483) all_163_1_232 = sz00 % 41.07/16.41 | % 41.07/16.41 | Simplifying 483 yields: % 41.07/16.41 | (484) all_163_1_232 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (428,484) yields a new equation: % 41.07/16.41 | (485) all_139_1_196 = sz00 % 41.07/16.41 | % 41.07/16.41 | Simplifying 485 yields: % 41.07/16.41 | (486) all_139_1_196 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (443,448) yields a new equation: % 41.07/16.41 | (487) all_141_2_200 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Simplifying 487 yields: % 41.07/16.41 | (488) all_141_2_200 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Combining equations (479,480) yields a new equation: % 41.07/16.41 | (489) all_141_1_199 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Simplifying 489 yields: % 41.07/16.41 | (490) all_141_1_199 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Combining equations (429,490) yields a new equation: % 41.07/16.41 | (491) all_137_1_193 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Simplifying 491 yields: % 41.07/16.41 | (492) all_137_1_193 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Combining equations (444,488) yields a new equation: % 41.07/16.41 | (493) all_123_2_173 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Simplifying 493 yields: % 41.07/16.41 | (494) all_123_2_173 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Combining equations (430,431) yields a new equation: % 41.07/16.41 | (495) all_137_1_193 = all_133_1_187 % 41.07/16.41 | % 41.07/16.41 | Simplifying 495 yields: % 41.07/16.41 | (496) all_137_1_193 = all_133_1_187 % 41.07/16.41 | % 41.07/16.41 | Combining equations (486,431) yields a new equation: % 41.07/16.41 | (497) all_133_1_187 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (496,492) yields a new equation: % 41.07/16.41 | (498) all_133_1_187 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Simplifying 498 yields: % 41.07/16.41 | (499) all_133_1_187 = all_129_1_181 % 41.07/16.41 | % 41.07/16.41 | Combining equations (476,475) yields a new equation: % 41.07/16.41 | (500) all_119_2_167 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 500 yields: % 41.07/16.41 | (501) all_119_2_167 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (472,474) yields a new equation: % 41.07/16.41 | (502) all_113_1_157 = sz00 % 41.07/16.41 | % 41.07/16.41 | Simplifying 502 yields: % 41.07/16.41 | (503) all_113_1_157 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (499,497) yields a new equation: % 41.07/16.41 | (504) all_129_1_181 = sz00 % 41.07/16.41 | % 41.07/16.41 | Simplifying 504 yields: % 41.07/16.41 | (505) all_129_1_181 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (446,494) yields a new equation: % 41.07/16.41 | (506) all_121_2_170 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Simplifying 506 yields: % 41.07/16.41 | (507) all_121_2_170 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Combining equations (462,507) yields a new equation: % 41.07/16.41 | (508) all_117_2_164 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Simplifying 508 yields: % 41.07/16.41 | (509) all_117_2_164 = all_115_2_161 % 41.07/16.41 | % 41.07/16.41 | Combining equations (440,501) yields a new equation: % 41.07/16.41 | (510) all_95_2_131 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 510 yields: % 41.07/16.41 | (511) all_95_2_131 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (463,509) yields a new equation: % 41.07/16.41 | (512) all_115_2_161 = all_97_2_134 % 41.07/16.41 | % 41.07/16.41 | Combining equations (460,509) yields a new equation: % 41.07/16.41 | (513) all_115_2_161 = all_113_2_158 % 41.07/16.41 | % 41.07/16.41 | Combining equations (513,512) yields a new equation: % 41.07/16.41 | (514) all_113_2_158 = all_97_2_134 % 41.07/16.41 | % 41.07/16.41 | Simplifying 514 yields: % 41.07/16.41 | (515) all_113_2_158 = all_97_2_134 % 41.07/16.41 | % 41.07/16.41 | Combining equations (503,421) yields a new equation: % 41.07/16.41 | (516) all_41_1_57 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (453,515) yields a new equation: % 41.07/16.41 | (517) all_97_2_134 = all_51_2_71 % 41.07/16.41 | % 41.07/16.41 | Combining equations (451,515) yields a new equation: % 41.07/16.41 | (518) all_97_2_134 = all_53_2_74 % 41.07/16.41 | % 41.07/16.41 | Combining equations (518,517) yields a new equation: % 41.07/16.41 | (519) all_53_2_74 = all_51_2_71 % 41.07/16.41 | % 41.07/16.41 | Simplifying 519 yields: % 41.07/16.41 | (520) all_53_2_74 = all_51_2_71 % 41.07/16.41 | % 41.07/16.41 | Combining equations (441,511) yields a new equation: % 41.07/16.41 | (521) all_79_2_109 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 521 yields: % 41.07/16.41 | (522) all_79_2_109 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (442,522) yields a new equation: % 41.07/16.41 | (523) all_41_2_58 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 523 yields: % 41.07/16.41 | (524) all_41_2_58 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (452,520) yields a new equation: % 41.07/16.41 | (525) all_51_2_71 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (525,517) yields a new equation: % 41.07/16.41 | (526) all_97_2_134 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (526,515) yields a new equation: % 41.07/16.41 | (527) all_113_2_158 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (516,421) yields a new equation: % 41.07/16.41 | (503) all_113_1_157 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (526,512) yields a new equation: % 41.07/16.41 | (529) all_115_2_161 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (505,492) yields a new equation: % 41.07/16.41 | (530) all_137_1_193 = sz00 % 41.07/16.41 | % 41.07/16.41 | Combining equations (529,488) yields a new equation: % 41.07/16.41 | (531) all_141_2_200 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (505,490) yields a new equation: % 41.07/16.41 | (532) all_141_1_199 = sz00 % 41.07/16.41 | % 41.07/16.41 | From (531)(532) and (305) follows: % 41.07/16.41 | (533) sdtpldt0(xa, sz00) = all_141_0_198 % 41.07/16.41 | % 41.07/16.41 | From (475)(530) and (295) follows: % 41.07/16.41 | (534) sdtpldt0(xa, sz00) = all_137_0_192 % 41.07/16.41 | % 41.07/16.41 | From (527)(503) and (250) follows: % 41.07/16.41 | (535) sdtpldt0(xa, sz00) = all_113_0_156 % 41.07/16.41 | % 41.07/16.41 | From (524)(516) and (220) follows: % 41.07/16.41 | (536) sdtpldt0(xa, sz00) = all_41_0_56 % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (136) with xa, sz00, all_137_0_192, all_141_0_198 and discharging atoms sdtpldt0(xa, sz00) = all_141_0_198, sdtpldt0(xa, sz00) = all_137_0_192, yields: % 41.07/16.41 | (537) all_141_0_198 = all_137_0_192 % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (117) with all_137_0_192, xa and discharging atoms sdtpldt0(xa, sz00) = all_137_0_192, aElement0(xa), yields: % 41.07/16.41 | (538) all_137_0_192 = xa % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (136) with xa, sz00, all_113_0_156, all_141_0_198 and discharging atoms sdtpldt0(xa, sz00) = all_141_0_198, sdtpldt0(xa, sz00) = all_113_0_156, yields: % 41.07/16.41 | (539) all_141_0_198 = all_113_0_156 % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (136) with xa, sz00, all_41_0_56, all_141_0_198 and discharging atoms sdtpldt0(xa, sz00) = all_141_0_198, sdtpldt0(xa, sz00) = all_41_0_56, yields: % 41.07/16.41 | (540) all_141_0_198 = all_41_0_56 % 41.07/16.41 | % 41.07/16.41 | Combining equations (537,539) yields a new equation: % 41.07/16.41 | (541) all_137_0_192 = all_113_0_156 % 41.07/16.41 | % 41.07/16.41 | Simplifying 541 yields: % 41.07/16.41 | (542) all_137_0_192 = all_113_0_156 % 41.07/16.41 | % 41.07/16.41 | Combining equations (540,539) yields a new equation: % 41.07/16.41 | (543) all_113_0_156 = all_41_0_56 % 41.07/16.41 | % 41.07/16.41 | Combining equations (542,538) yields a new equation: % 41.07/16.41 | (544) all_113_0_156 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 544 yields: % 41.07/16.41 | (545) all_113_0_156 = xa % 41.07/16.41 | % 41.07/16.41 | Combining equations (543,545) yields a new equation: % 41.07/16.41 | (546) all_41_0_56 = xa % 41.07/16.41 | % 41.07/16.41 | Simplifying 546 yields: % 41.07/16.41 | (547) all_41_0_56 = xa % 41.07/16.41 | % 41.07/16.41 | From (547) and (536) follows: % 41.07/16.41 | (548) sdtpldt0(xa, sz00) = xa % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (49) with all_0_10_10, xa, all_181_0_257, xa, all_0_3_3 and discharging atoms sdtasdt0(all_0_3_3, xa) = xa, sdtasdt0(xa, all_181_0_257) = all_0_10_10, aElement0(all_181_0_257), aElement0(all_0_3_3), aElement0(xa), yields: % 41.07/16.41 | (549) ? [v0] : (sdtasdt0(all_0_3_3, v0) = all_0_10_10 & sdtasdt0(xa, all_181_0_257) = v0) % 41.07/16.41 | % 41.07/16.41 | Instantiating formula (111) with all_0_10_10, xa, sz00, xa, all_181_0_257 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_0_10_10, sdtpldt0(xa, sz00) = xa, aElement0(all_181_0_257), aElement0(xa), aElement0(sz00), yields: % 41.07/16.41 | (550) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_181_0_257, xa) = v1 & sdtasdt0(all_181_0_257, xa) = v0 & sdtasdt0(all_181_0_257, sz00) = v2 & sdtasdt0(xa, all_181_0_257) = v3 & sdtasdt0(sz00, all_181_0_257) = v4 & sdtpldt0(v3, v4) = all_0_10_10 & sdtpldt0(v1, v2) = v0) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_0_0, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_0_0), yields: % 41.07/16.42 | (551) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_0_0) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_1_1, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_1_1), yields: % 41.07/16.42 | (552) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_1_1) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_2_2, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_2_2), yields: % 41.07/16.42 | (553) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_2_2) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_3_3, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_3_3), yields: % 41.07/16.42 | (554) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_3_3) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_4_4, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_4_4), yields: % 41.07/16.42 | (555) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_4_4) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_5_5, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_5_5), yields: % 41.07/16.42 | (556) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_5_5) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with xc, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(xc), yields: % 41.07/16.42 | (557) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xc) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with xb, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(xb), yields: % 41.07/16.42 | (558) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xb) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with xa, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(xa), yields: % 41.07/16.42 | (559) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xa) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with sz10, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(sz10), yields: % 41.07/16.42 | (560) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz10) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with sz00, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(sz00), yields: % 41.07/16.42 | (561) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, sz00) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_291_0_400, all_181_0_257 and discharging atoms aElement0(all_291_0_400), aElement0(all_181_0_257), yields: % 41.07/16.42 | (562) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_291_0_400) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_285_0_393, all_181_0_257 and discharging atoms aElement0(all_285_0_393), aElement0(all_181_0_257), yields: % 41.07/16.42 | (563) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_285_0_393) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_267_0_368, all_181_0_257 and discharging atoms aElement0(all_267_0_368), aElement0(all_181_0_257), yields: % 41.07/16.42 | (564) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_267_0_368) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_261_0_361, all_181_0_257 and discharging atoms aElement0(all_261_0_361), aElement0(all_181_0_257), yields: % 41.07/16.42 | (565) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_261_0_361) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_235_0_324, all_181_0_257 and discharging atoms aElement0(all_235_0_324), aElement0(all_181_0_257), yields: % 41.07/16.42 | (566) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_235_0_324) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_185_0_259, all_181_0_257 and discharging atoms aElement0(all_185_0_259), aElement0(all_181_0_257), yields: % 41.07/16.42 | (567) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_185_0_259) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_183_0_258, all_181_0_257 and discharging atoms aElement0(all_183_0_258), aElement0(all_181_0_257), yields: % 41.07/16.42 | (568) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_183_0_258) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_181_0_257, all_181_0_257 and discharging atoms aElement0(all_181_0_257), yields: % 41.07/16.42 | (569) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_181_0_257) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_23_0_31, all_183_0_258 and discharging atoms aElement0(all_183_0_258), aElement0(all_23_0_31), yields: % 41.07/16.42 | (570) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_23_0_31) = v1 & sdtasdt0(xa, all_183_0_258) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_23_0_31, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_23_0_31), yields: % 41.07/16.42 | (571) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_23_0_31) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_19_0_28, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_19_0_28), yields: % 41.07/16.42 | (572) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_19_0_28) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_17_0_27, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_17_0_27), yields: % 41.07/16.42 | (573) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_17_0_27) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_23_0_31, all_17_0_27 and discharging atoms aElement0(all_23_0_31), aElement0(all_17_0_27), yields: % 41.07/16.42 | (574) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_23_0_31) = v1 & sdtasdt0(xa, all_17_0_27) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_8_8, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_8_8), yields: % 41.07/16.42 | (575) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_8_8) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_23_0_31, all_0_8_8 and discharging atoms aElement0(all_23_0_31), aElement0(all_0_8_8), yields: % 41.07/16.42 | (576) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_23_0_31) = v1 & sdtasdt0(xa, all_0_8_8) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_0_14_14, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(all_0_14_14), yields: % 41.07/16.42 | (577) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_0_14_14) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with xu, all_181_0_257 and discharging atoms aElement0(all_181_0_257), aElement0(xu), yields: % 41.07/16.42 | (578) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, xu) = v1 & sdtasdt0(xa, all_181_0_257) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating formula (156) with all_23_0_31, xu and discharging atoms aElement0(all_23_0_31), aElement0(xu), yields: % 41.07/16.42 | (579) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xu) & sdtasdt0(xb, all_23_0_31) = v1 & sdtasdt0(xa, xu) = v0 & sdtpldt0(v0, v1) = v2) % 41.07/16.42 | % 41.07/16.42 | Instantiating (549) with all_317_0_407 yields: % 41.07/16.42 | (580) sdtasdt0(all_0_3_3, all_317_0_407) = all_0_10_10 & sdtasdt0(xa, all_181_0_257) = all_317_0_407 % 41.07/16.42 | % 41.07/16.42 | Applying alpha-rule on (580) yields: % 41.07/16.42 | (581) sdtasdt0(all_0_3_3, all_317_0_407) = all_0_10_10 % 41.07/16.42 | (582) sdtasdt0(xa, all_181_0_257) = all_317_0_407 % 41.07/16.42 | % 41.07/16.42 | Instantiating (561) with all_437_0_567, all_437_1_568, all_437_2_569 yields: % 41.07/16.42 | (583) ~ (all_437_0_567 = xu) & sdtasdt0(xb, sz00) = all_437_1_568 & sdtasdt0(xa, all_181_0_257) = all_437_2_569 & sdtpldt0(all_437_2_569, all_437_1_568) = all_437_0_567 % 41.07/16.42 | % 41.07/16.42 | Applying alpha-rule on (583) yields: % 41.07/16.42 | (584) ~ (all_437_0_567 = xu) % 41.07/16.42 | (585) sdtasdt0(xb, sz00) = all_437_1_568 % 41.07/16.42 | (586) sdtasdt0(xa, all_181_0_257) = all_437_2_569 % 41.07/16.42 | (587) sdtpldt0(all_437_2_569, all_437_1_568) = all_437_0_567 % 41.07/16.42 | % 41.07/16.42 | Instantiating (560) with all_439_0_570, all_439_1_571, all_439_2_572 yields: % 41.07/16.42 | (588) ~ (all_439_0_570 = xu) & sdtasdt0(xb, sz10) = all_439_1_571 & sdtasdt0(xa, all_181_0_257) = all_439_2_572 & sdtpldt0(all_439_2_572, all_439_1_571) = all_439_0_570 % 41.07/16.42 | % 41.07/16.42 | Applying alpha-rule on (588) yields: % 41.07/16.42 | (589) ~ (all_439_0_570 = xu) % 41.07/16.42 | (590) sdtasdt0(xb, sz10) = all_439_1_571 % 41.07/16.42 | (591) sdtasdt0(xa, all_181_0_257) = all_439_2_572 % 41.07/16.42 | (592) sdtpldt0(all_439_2_572, all_439_1_571) = all_439_0_570 % 41.07/16.42 | % 41.07/16.42 | Instantiating (557) with all_441_0_573, all_441_1_574, all_441_2_575 yields: % 41.07/16.42 | (593) ~ (all_441_0_573 = xu) & sdtasdt0(xb, xc) = all_441_1_574 & sdtasdt0(xa, all_181_0_257) = all_441_2_575 & sdtpldt0(all_441_2_575, all_441_1_574) = all_441_0_573 % 41.07/16.42 | % 41.07/16.42 | Applying alpha-rule on (593) yields: % 41.07/16.42 | (594) ~ (all_441_0_573 = xu) % 41.07/16.42 | (595) sdtasdt0(xb, xc) = all_441_1_574 % 41.07/16.42 | (596) sdtasdt0(xa, all_181_0_257) = all_441_2_575 % 41.07/16.42 | (597) sdtpldt0(all_441_2_575, all_441_1_574) = all_441_0_573 % 41.07/16.42 | % 41.07/16.42 | Instantiating (555) with all_445_0_579, all_445_1_580, all_445_2_581 yields: % 41.07/16.42 | (598) ~ (all_445_0_579 = xu) & sdtasdt0(xb, all_0_4_4) = all_445_1_580 & sdtasdt0(xa, all_181_0_257) = all_445_2_581 & sdtpldt0(all_445_2_581, all_445_1_580) = all_445_0_579 % 41.07/16.42 | % 41.07/16.42 | Applying alpha-rule on (598) yields: % 41.07/16.42 | (599) ~ (all_445_0_579 = xu) % 41.07/16.42 | (600) sdtasdt0(xb, all_0_4_4) = all_445_1_580 % 41.07/16.43 | (601) sdtasdt0(xa, all_181_0_257) = all_445_2_581 % 41.07/16.43 | (602) sdtpldt0(all_445_2_581, all_445_1_580) = all_445_0_579 % 41.07/16.43 | % 41.07/16.43 | Instantiating (554) with all_447_0_582, all_447_1_583, all_447_2_584 yields: % 41.07/16.43 | (603) ~ (all_447_0_582 = xu) & sdtasdt0(xb, all_0_3_3) = all_447_1_583 & sdtasdt0(xa, all_181_0_257) = all_447_2_584 & sdtpldt0(all_447_2_584, all_447_1_583) = all_447_0_582 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (603) yields: % 41.07/16.43 | (604) ~ (all_447_0_582 = xu) % 41.07/16.43 | (605) sdtasdt0(xb, all_0_3_3) = all_447_1_583 % 41.07/16.43 | (606) sdtasdt0(xa, all_181_0_257) = all_447_2_584 % 41.07/16.43 | (607) sdtpldt0(all_447_2_584, all_447_1_583) = all_447_0_582 % 41.07/16.43 | % 41.07/16.43 | Instantiating (556) with all_455_0_594, all_455_1_595, all_455_2_596 yields: % 41.07/16.43 | (608) ~ (all_455_0_594 = xu) & sdtasdt0(xb, all_0_5_5) = all_455_1_595 & sdtasdt0(xa, all_181_0_257) = all_455_2_596 & sdtpldt0(all_455_2_596, all_455_1_595) = all_455_0_594 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (608) yields: % 41.07/16.43 | (609) ~ (all_455_0_594 = xu) % 41.07/16.43 | (610) sdtasdt0(xb, all_0_5_5) = all_455_1_595 % 41.07/16.43 | (611) sdtasdt0(xa, all_181_0_257) = all_455_2_596 % 41.07/16.43 | (612) sdtpldt0(all_455_2_596, all_455_1_595) = all_455_0_594 % 41.07/16.43 | % 41.07/16.43 | Instantiating (559) with all_459_0_600, all_459_1_601, all_459_2_602 yields: % 41.07/16.43 | (613) ~ (all_459_0_600 = xu) & sdtasdt0(xb, xa) = all_459_1_601 & sdtasdt0(xa, all_181_0_257) = all_459_2_602 & sdtpldt0(all_459_2_602, all_459_1_601) = all_459_0_600 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (613) yields: % 41.07/16.43 | (614) ~ (all_459_0_600 = xu) % 41.07/16.43 | (615) sdtasdt0(xb, xa) = all_459_1_601 % 41.07/16.43 | (616) sdtasdt0(xa, all_181_0_257) = all_459_2_602 % 41.07/16.43 | (617) sdtpldt0(all_459_2_602, all_459_1_601) = all_459_0_600 % 41.07/16.43 | % 41.07/16.43 | Instantiating (558) with all_461_0_603, all_461_1_604, all_461_2_605 yields: % 41.07/16.43 | (618) ~ (all_461_0_603 = xu) & sdtasdt0(xb, xb) = all_461_1_604 & sdtasdt0(xa, all_181_0_257) = all_461_2_605 & sdtpldt0(all_461_2_605, all_461_1_604) = all_461_0_603 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (618) yields: % 41.07/16.43 | (619) ~ (all_461_0_603 = xu) % 41.07/16.43 | (620) sdtasdt0(xb, xb) = all_461_1_604 % 41.07/16.43 | (621) sdtasdt0(xa, all_181_0_257) = all_461_2_605 % 41.07/16.43 | (622) sdtpldt0(all_461_2_605, all_461_1_604) = all_461_0_603 % 41.07/16.43 | % 41.07/16.43 | Instantiating (553) with all_463_0_606, all_463_1_607, all_463_2_608 yields: % 41.07/16.43 | (623) ~ (all_463_0_606 = xu) & sdtasdt0(xb, all_0_2_2) = all_463_1_607 & sdtasdt0(xa, all_181_0_257) = all_463_2_608 & sdtpldt0(all_463_2_608, all_463_1_607) = all_463_0_606 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (623) yields: % 41.07/16.43 | (624) ~ (all_463_0_606 = xu) % 41.07/16.43 | (625) sdtasdt0(xb, all_0_2_2) = all_463_1_607 % 41.07/16.43 | (626) sdtasdt0(xa, all_181_0_257) = all_463_2_608 % 41.07/16.43 | (627) sdtpldt0(all_463_2_608, all_463_1_607) = all_463_0_606 % 41.07/16.43 | % 41.07/16.43 | Instantiating (550) with all_649_0_853, all_649_1_854, all_649_2_855, all_649_3_856, all_649_4_857 yields: % 41.07/16.43 | (628) sdtasdt0(all_181_0_257, xa) = all_649_3_856 & sdtasdt0(all_181_0_257, xa) = all_649_4_857 & sdtasdt0(all_181_0_257, sz00) = all_649_2_855 & sdtasdt0(xa, all_181_0_257) = all_649_1_854 & sdtasdt0(sz00, all_181_0_257) = all_649_0_853 & sdtpldt0(all_649_1_854, all_649_0_853) = all_0_10_10 & sdtpldt0(all_649_3_856, all_649_2_855) = all_649_4_857 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (628) yields: % 41.07/16.43 | (629) sdtasdt0(xa, all_181_0_257) = all_649_1_854 % 41.07/16.43 | (630) sdtasdt0(all_181_0_257, sz00) = all_649_2_855 % 41.07/16.43 | (631) sdtasdt0(all_181_0_257, xa) = all_649_3_856 % 41.07/16.43 | (632) sdtasdt0(sz00, all_181_0_257) = all_649_0_853 % 41.07/16.43 | (633) sdtpldt0(all_649_3_856, all_649_2_855) = all_649_4_857 % 41.07/16.43 | (634) sdtpldt0(all_649_1_854, all_649_0_853) = all_0_10_10 % 41.07/16.43 | (635) sdtasdt0(all_181_0_257, xa) = all_649_4_857 % 41.07/16.43 | % 41.07/16.43 | Instantiating (569) with all_800_0_1059, all_800_1_1060, all_800_2_1061 yields: % 41.07/16.43 | (636) ~ (all_800_0_1059 = xu) & sdtasdt0(xb, all_181_0_257) = all_800_1_1060 & sdtasdt0(xa, all_181_0_257) = all_800_2_1061 & sdtpldt0(all_800_2_1061, all_800_1_1060) = all_800_0_1059 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (636) yields: % 41.07/16.43 | (637) ~ (all_800_0_1059 = xu) % 41.07/16.43 | (638) sdtasdt0(xb, all_181_0_257) = all_800_1_1060 % 41.07/16.43 | (639) sdtasdt0(xa, all_181_0_257) = all_800_2_1061 % 41.07/16.43 | (640) sdtpldt0(all_800_2_1061, all_800_1_1060) = all_800_0_1059 % 41.07/16.43 | % 41.07/16.43 | Instantiating (551) with all_901_0_1193, all_901_1_1194, all_901_2_1195 yields: % 41.07/16.43 | (641) ~ (all_901_0_1193 = xu) & sdtasdt0(xb, all_0_0_0) = all_901_1_1194 & sdtasdt0(xa, all_181_0_257) = all_901_2_1195 & sdtpldt0(all_901_2_1195, all_901_1_1194) = all_901_0_1193 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (641) yields: % 41.07/16.43 | (642) ~ (all_901_0_1193 = xu) % 41.07/16.43 | (643) sdtasdt0(xb, all_0_0_0) = all_901_1_1194 % 41.07/16.43 | (644) sdtasdt0(xa, all_181_0_257) = all_901_2_1195 % 41.07/16.43 | (645) sdtpldt0(all_901_2_1195, all_901_1_1194) = all_901_0_1193 % 41.07/16.43 | % 41.07/16.43 | Instantiating (567) with all_911_0_1207, all_911_1_1208, all_911_2_1209 yields: % 41.07/16.43 | (646) ~ (all_911_0_1207 = xu) & sdtasdt0(xb, all_185_0_259) = all_911_1_1208 & sdtasdt0(xa, all_181_0_257) = all_911_2_1209 & sdtpldt0(all_911_2_1209, all_911_1_1208) = all_911_0_1207 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (646) yields: % 41.07/16.43 | (647) ~ (all_911_0_1207 = xu) % 41.07/16.43 | (648) sdtasdt0(xb, all_185_0_259) = all_911_1_1208 % 41.07/16.43 | (649) sdtasdt0(xa, all_181_0_257) = all_911_2_1209 % 41.07/16.43 | (650) sdtpldt0(all_911_2_1209, all_911_1_1208) = all_911_0_1207 % 41.07/16.43 | % 41.07/16.43 | Instantiating (568) with all_917_0_1216, all_917_1_1217, all_917_2_1218 yields: % 41.07/16.43 | (651) ~ (all_917_0_1216 = xu) & sdtasdt0(xb, all_183_0_258) = all_917_1_1217 & sdtasdt0(xa, all_181_0_257) = all_917_2_1218 & sdtpldt0(all_917_2_1218, all_917_1_1217) = all_917_0_1216 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (651) yields: % 41.07/16.43 | (652) ~ (all_917_0_1216 = xu) % 41.07/16.43 | (653) sdtasdt0(xb, all_183_0_258) = all_917_1_1217 % 41.07/16.43 | (654) sdtasdt0(xa, all_181_0_257) = all_917_2_1218 % 41.07/16.43 | (655) sdtpldt0(all_917_2_1218, all_917_1_1217) = all_917_0_1216 % 41.07/16.43 | % 41.07/16.43 | Instantiating (565) with all_919_0_1219, all_919_1_1220, all_919_2_1221 yields: % 41.07/16.43 | (656) ~ (all_919_0_1219 = xu) & sdtasdt0(xb, all_261_0_361) = all_919_1_1220 & sdtasdt0(xa, all_181_0_257) = all_919_2_1221 & sdtpldt0(all_919_2_1221, all_919_1_1220) = all_919_0_1219 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (656) yields: % 41.07/16.43 | (657) ~ (all_919_0_1219 = xu) % 41.07/16.43 | (658) sdtasdt0(xb, all_261_0_361) = all_919_1_1220 % 41.07/16.43 | (659) sdtasdt0(xa, all_181_0_257) = all_919_2_1221 % 41.07/16.43 | (660) sdtpldt0(all_919_2_1221, all_919_1_1220) = all_919_0_1219 % 41.07/16.43 | % 41.07/16.43 | Instantiating (577) with all_932_0_1238, all_932_1_1239, all_932_2_1240 yields: % 41.07/16.43 | (661) ~ (all_932_0_1238 = xu) & sdtasdt0(xb, all_0_14_14) = all_932_1_1239 & sdtasdt0(xa, all_181_0_257) = all_932_2_1240 & sdtpldt0(all_932_2_1240, all_932_1_1239) = all_932_0_1238 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (661) yields: % 41.07/16.43 | (662) ~ (all_932_0_1238 = xu) % 41.07/16.43 | (663) sdtasdt0(xb, all_0_14_14) = all_932_1_1239 % 41.07/16.43 | (664) sdtasdt0(xa, all_181_0_257) = all_932_2_1240 % 41.07/16.43 | (665) sdtpldt0(all_932_2_1240, all_932_1_1239) = all_932_0_1238 % 41.07/16.43 | % 41.07/16.43 | Instantiating (576) with all_939_0_1245, all_939_1_1246, all_939_2_1247 yields: % 41.07/16.43 | (666) ~ (all_939_0_1245 = xu) & sdtasdt0(xb, all_23_0_31) = all_939_1_1246 & sdtasdt0(xa, all_0_8_8) = all_939_2_1247 & sdtpldt0(all_939_2_1247, all_939_1_1246) = all_939_0_1245 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (666) yields: % 41.07/16.43 | (667) ~ (all_939_0_1245 = xu) % 41.07/16.43 | (668) sdtasdt0(xb, all_23_0_31) = all_939_1_1246 % 41.07/16.43 | (669) sdtasdt0(xa, all_0_8_8) = all_939_2_1247 % 41.07/16.43 | (670) sdtpldt0(all_939_2_1247, all_939_1_1246) = all_939_0_1245 % 41.07/16.43 | % 41.07/16.43 | Instantiating (575) with all_957_0_1272, all_957_1_1273, all_957_2_1274 yields: % 41.07/16.43 | (671) ~ (all_957_0_1272 = xu) & sdtasdt0(xb, all_0_8_8) = all_957_1_1273 & sdtasdt0(xa, all_181_0_257) = all_957_2_1274 & sdtpldt0(all_957_2_1274, all_957_1_1273) = all_957_0_1272 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (671) yields: % 41.07/16.43 | (672) ~ (all_957_0_1272 = xu) % 41.07/16.43 | (673) sdtasdt0(xb, all_0_8_8) = all_957_1_1273 % 41.07/16.43 | (674) sdtasdt0(xa, all_181_0_257) = all_957_2_1274 % 41.07/16.43 | (675) sdtpldt0(all_957_2_1274, all_957_1_1273) = all_957_0_1272 % 41.07/16.43 | % 41.07/16.43 | Instantiating (578) with all_1021_0_1368, all_1021_1_1369, all_1021_2_1370 yields: % 41.07/16.43 | (676) ~ (all_1021_0_1368 = xu) & sdtasdt0(xb, xu) = all_1021_1_1369 & sdtasdt0(xa, all_181_0_257) = all_1021_2_1370 & sdtpldt0(all_1021_2_1370, all_1021_1_1369) = all_1021_0_1368 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (676) yields: % 41.07/16.43 | (677) ~ (all_1021_0_1368 = xu) % 41.07/16.43 | (678) sdtasdt0(xb, xu) = all_1021_1_1369 % 41.07/16.43 | (679) sdtasdt0(xa, all_181_0_257) = all_1021_2_1370 % 41.07/16.43 | (680) sdtpldt0(all_1021_2_1370, all_1021_1_1369) = all_1021_0_1368 % 41.07/16.43 | % 41.07/16.43 | Instantiating (563) with all_1141_0_1529, all_1141_1_1530, all_1141_2_1531 yields: % 41.07/16.43 | (681) ~ (all_1141_0_1529 = xu) & sdtasdt0(xb, all_285_0_393) = all_1141_1_1530 & sdtasdt0(xa, all_181_0_257) = all_1141_2_1531 & sdtpldt0(all_1141_2_1531, all_1141_1_1530) = all_1141_0_1529 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (681) yields: % 41.07/16.43 | (682) ~ (all_1141_0_1529 = xu) % 41.07/16.43 | (683) sdtasdt0(xb, all_285_0_393) = all_1141_1_1530 % 41.07/16.43 | (684) sdtasdt0(xa, all_181_0_257) = all_1141_2_1531 % 41.07/16.43 | (685) sdtpldt0(all_1141_2_1531, all_1141_1_1530) = all_1141_0_1529 % 41.07/16.43 | % 41.07/16.43 | Instantiating (562) with all_1143_0_1532, all_1143_1_1533, all_1143_2_1534 yields: % 41.07/16.43 | (686) ~ (all_1143_0_1532 = xu) & sdtasdt0(xb, all_291_0_400) = all_1143_1_1533 & sdtasdt0(xa, all_181_0_257) = all_1143_2_1534 & sdtpldt0(all_1143_2_1534, all_1143_1_1533) = all_1143_0_1532 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (686) yields: % 41.07/16.43 | (687) ~ (all_1143_0_1532 = xu) % 41.07/16.43 | (688) sdtasdt0(xb, all_291_0_400) = all_1143_1_1533 % 41.07/16.43 | (689) sdtasdt0(xa, all_181_0_257) = all_1143_2_1534 % 41.07/16.43 | (690) sdtpldt0(all_1143_2_1534, all_1143_1_1533) = all_1143_0_1532 % 41.07/16.43 | % 41.07/16.43 | Instantiating (564) with all_1147_0_1538, all_1147_1_1539, all_1147_2_1540 yields: % 41.07/16.43 | (691) ~ (all_1147_0_1538 = xu) & sdtasdt0(xb, all_267_0_368) = all_1147_1_1539 & sdtasdt0(xa, all_181_0_257) = all_1147_2_1540 & sdtpldt0(all_1147_2_1540, all_1147_1_1539) = all_1147_0_1538 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (691) yields: % 41.07/16.43 | (692) ~ (all_1147_0_1538 = xu) % 41.07/16.43 | (693) sdtasdt0(xb, all_267_0_368) = all_1147_1_1539 % 41.07/16.43 | (694) sdtasdt0(xa, all_181_0_257) = all_1147_2_1540 % 41.07/16.43 | (695) sdtpldt0(all_1147_2_1540, all_1147_1_1539) = all_1147_0_1538 % 41.07/16.43 | % 41.07/16.43 | Instantiating (566) with all_1159_0_1554, all_1159_1_1555, all_1159_2_1556 yields: % 41.07/16.43 | (696) ~ (all_1159_0_1554 = xu) & sdtasdt0(xb, all_235_0_324) = all_1159_1_1555 & sdtasdt0(xa, all_181_0_257) = all_1159_2_1556 & sdtpldt0(all_1159_2_1556, all_1159_1_1555) = all_1159_0_1554 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (696) yields: % 41.07/16.43 | (697) ~ (all_1159_0_1554 = xu) % 41.07/16.43 | (698) sdtasdt0(xb, all_235_0_324) = all_1159_1_1555 % 41.07/16.43 | (699) sdtasdt0(xa, all_181_0_257) = all_1159_2_1556 % 41.07/16.43 | (700) sdtpldt0(all_1159_2_1556, all_1159_1_1555) = all_1159_0_1554 % 41.07/16.43 | % 41.07/16.43 | Instantiating (572) with all_1203_0_1609, all_1203_1_1610, all_1203_2_1611 yields: % 41.07/16.43 | (701) ~ (all_1203_0_1609 = xu) & sdtasdt0(xb, all_19_0_28) = all_1203_1_1610 & sdtasdt0(xa, all_181_0_257) = all_1203_2_1611 & sdtpldt0(all_1203_2_1611, all_1203_1_1610) = all_1203_0_1609 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (701) yields: % 41.07/16.43 | (702) ~ (all_1203_0_1609 = xu) % 41.07/16.43 | (703) sdtasdt0(xb, all_19_0_28) = all_1203_1_1610 % 41.07/16.43 | (704) sdtasdt0(xa, all_181_0_257) = all_1203_2_1611 % 41.07/16.43 | (705) sdtpldt0(all_1203_2_1611, all_1203_1_1610) = all_1203_0_1609 % 41.07/16.43 | % 41.07/16.43 | Instantiating (571) with all_1279_0_1713, all_1279_1_1714, all_1279_2_1715 yields: % 41.07/16.43 | (706) ~ (all_1279_0_1713 = xu) & sdtasdt0(xb, all_23_0_31) = all_1279_1_1714 & sdtasdt0(xa, all_181_0_257) = all_1279_2_1715 & sdtpldt0(all_1279_2_1715, all_1279_1_1714) = all_1279_0_1713 % 41.07/16.43 | % 41.07/16.43 | Applying alpha-rule on (706) yields: % 41.07/16.43 | (707) ~ (all_1279_0_1713 = xu) % 41.07/16.44 | (708) sdtasdt0(xb, all_23_0_31) = all_1279_1_1714 % 41.07/16.44 | (709) sdtasdt0(xa, all_181_0_257) = all_1279_2_1715 % 41.07/16.44 | (710) sdtpldt0(all_1279_2_1715, all_1279_1_1714) = all_1279_0_1713 % 41.07/16.44 | % 41.07/16.44 | Instantiating (552) with all_1285_0_1721, all_1285_1_1722, all_1285_2_1723 yields: % 41.07/16.44 | (711) ~ (all_1285_0_1721 = xu) & sdtasdt0(xb, all_0_1_1) = all_1285_1_1722 & sdtasdt0(xa, all_181_0_257) = all_1285_2_1723 & sdtpldt0(all_1285_2_1723, all_1285_1_1722) = all_1285_0_1721 % 41.07/16.44 | % 41.07/16.44 | Applying alpha-rule on (711) yields: % 41.07/16.44 | (712) ~ (all_1285_0_1721 = xu) % 41.07/16.44 | (713) sdtasdt0(xb, all_0_1_1) = all_1285_1_1722 % 41.07/16.44 | (714) sdtasdt0(xa, all_181_0_257) = all_1285_2_1723 % 41.07/16.44 | (715) sdtpldt0(all_1285_2_1723, all_1285_1_1722) = all_1285_0_1721 % 41.07/16.44 | % 41.07/16.44 | Instantiating (570) with all_1324_0_1763, all_1324_1_1764, all_1324_2_1765 yields: % 41.07/16.44 | (716) ~ (all_1324_0_1763 = xu) & sdtasdt0(xb, all_23_0_31) = all_1324_1_1764 & sdtasdt0(xa, all_183_0_258) = all_1324_2_1765 & sdtpldt0(all_1324_2_1765, all_1324_1_1764) = all_1324_0_1763 % 41.07/16.44 | % 41.07/16.44 | Applying alpha-rule on (716) yields: % 41.07/16.44 | (717) ~ (all_1324_0_1763 = xu) % 41.07/16.44 | (718) sdtasdt0(xb, all_23_0_31) = all_1324_1_1764 % 41.07/16.44 | (719) sdtasdt0(xa, all_183_0_258) = all_1324_2_1765 % 41.07/16.44 | (720) sdtpldt0(all_1324_2_1765, all_1324_1_1764) = all_1324_0_1763 % 41.07/16.44 | % 41.07/16.44 | Instantiating (579) with all_1331_0_1773, all_1331_1_1774, all_1331_2_1775 yields: % 41.07/16.44 | (721) ~ (all_1331_0_1773 = xu) & sdtasdt0(xb, all_23_0_31) = all_1331_1_1774 & sdtasdt0(xa, xu) = all_1331_2_1775 & sdtpldt0(all_1331_2_1775, all_1331_1_1774) = all_1331_0_1773 % 41.07/16.44 | % 41.07/16.44 | Applying alpha-rule on (721) yields: % 41.07/16.44 | (722) ~ (all_1331_0_1773 = xu) % 41.07/16.44 | (723) sdtasdt0(xb, all_23_0_31) = all_1331_1_1774 % 41.07/16.44 | (724) sdtasdt0(xa, xu) = all_1331_2_1775 % 41.07/16.44 | (725) sdtpldt0(all_1331_2_1775, all_1331_1_1774) = all_1331_0_1773 % 41.07/16.44 | % 41.07/16.44 | Instantiating (573) with all_1831_0_2390, all_1831_1_2391, all_1831_2_2392 yields: % 41.07/16.44 | (726) ~ (all_1831_0_2390 = xu) & sdtasdt0(xb, all_17_0_27) = all_1831_1_2391 & sdtasdt0(xa, all_181_0_257) = all_1831_2_2392 & sdtpldt0(all_1831_2_2392, all_1831_1_2391) = all_1831_0_2390 % 41.07/16.44 | % 41.07/16.44 | Applying alpha-rule on (726) yields: % 41.07/16.44 | (727) ~ (all_1831_0_2390 = xu) % 41.07/16.44 | (728) sdtasdt0(xb, all_17_0_27) = all_1831_1_2391 % 41.07/16.44 | (729) sdtasdt0(xa, all_181_0_257) = all_1831_2_2392 % 41.07/16.44 | (730) sdtpldt0(all_1831_2_2392, all_1831_1_2391) = all_1831_0_2390 % 41.07/16.44 | % 41.07/16.44 | Instantiating (574) with all_1871_0_2436, all_1871_1_2437, all_1871_2_2438 yields: % 41.07/16.44 | (731) ~ (all_1871_0_2436 = xu) & sdtasdt0(xb, all_23_0_31) = all_1871_1_2437 & sdtasdt0(xa, all_17_0_27) = all_1871_2_2438 & sdtpldt0(all_1871_2_2438, all_1871_1_2437) = all_1871_0_2436 % 41.07/16.44 | % 41.07/16.44 | Applying alpha-rule on (731) yields: % 41.07/16.44 | (732) ~ (all_1871_0_2436 = xu) % 41.07/16.44 | (733) sdtasdt0(xb, all_23_0_31) = all_1871_1_2437 % 41.07/16.44 | (734) sdtasdt0(xa, all_17_0_27) = all_1871_2_2438 % 41.07/16.44 | (735) sdtpldt0(all_1871_2_2438, all_1871_1_2437) = all_1871_0_2436 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xb, all_23_0_31, all_1331_1_1774, all_1871_1_2437 and discharging atoms sdtasdt0(xb, all_23_0_31) = all_1871_1_2437, sdtasdt0(xb, all_23_0_31) = all_1331_1_1774, yields: % 41.07/16.44 | (736) all_1871_1_2437 = all_1331_1_1774 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xb, all_23_0_31, all_1324_1_1764, all_1331_1_1774 and discharging atoms sdtasdt0(xb, all_23_0_31) = all_1331_1_1774, sdtasdt0(xb, all_23_0_31) = all_1324_1_1764, yields: % 41.07/16.44 | (737) all_1331_1_1774 = all_1324_1_1764 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xb, all_23_0_31, all_1279_1_1714, all_0_9_9 and discharging atoms sdtasdt0(xb, all_23_0_31) = all_1279_1_1714, sdtasdt0(xb, all_23_0_31) = all_0_9_9, yields: % 41.07/16.44 | (738) all_1279_1_1714 = all_0_9_9 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xb, all_23_0_31, all_1279_1_1714, all_1324_1_1764 and discharging atoms sdtasdt0(xb, all_23_0_31) = all_1324_1_1764, sdtasdt0(xb, all_23_0_31) = all_1279_1_1714, yields: % 41.07/16.44 | (739) all_1324_1_1764 = all_1279_1_1714 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xb, all_23_0_31, all_939_1_1246, all_1871_1_2437 and discharging atoms sdtasdt0(xb, all_23_0_31) = all_1871_1_2437, sdtasdt0(xb, all_23_0_31) = all_939_1_1246, yields: % 41.07/16.44 | (740) all_1871_1_2437 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_1279_2_1715, all_1285_2_1723 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1285_2_1723, sdtasdt0(xa, all_181_0_257) = all_1279_2_1715, yields: % 41.07/16.44 | (741) all_1285_2_1723 = all_1279_2_1715 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_1159_2_1556, all_1203_2_1611 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1203_2_1611, sdtasdt0(xa, all_181_0_257) = all_1159_2_1556, yields: % 41.07/16.44 | (742) all_1203_2_1611 = all_1159_2_1556 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_1147_2_1540, all_1279_2_1715 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1279_2_1715, sdtasdt0(xa, all_181_0_257) = all_1147_2_1540, yields: % 41.07/16.44 | (743) all_1279_2_1715 = all_1147_2_1540 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_1021_2_1370, all_1143_2_1534 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1143_2_1534, sdtasdt0(xa, all_181_0_257) = all_1021_2_1370, yields: % 41.07/16.44 | (744) all_1143_2_1534 = all_1021_2_1370 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_1021_2_1370, all_1141_2_1531 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1141_2_1531, sdtasdt0(xa, all_181_0_257) = all_1021_2_1370, yields: % 41.07/16.44 | (745) all_1141_2_1531 = all_1021_2_1370 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_932_2_1240, all_1831_2_2392 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1831_2_2392, sdtasdt0(xa, all_181_0_257) = all_932_2_1240, yields: % 41.07/16.44 | (746) all_1831_2_2392 = all_932_2_1240 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_932_2_1240, all_1147_2_1540 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1147_2_1540, sdtasdt0(xa, all_181_0_257) = all_932_2_1240, yields: % 41.07/16.44 | (747) all_1147_2_1540 = all_932_2_1240 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_919_2_1221, all_1141_2_1531 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1141_2_1531, sdtasdt0(xa, all_181_0_257) = all_919_2_1221, yields: % 41.07/16.44 | (748) all_1141_2_1531 = all_919_2_1221 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_917_2_1218, all_1021_2_1370 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1021_2_1370, sdtasdt0(xa, all_181_0_257) = all_917_2_1218, yields: % 41.07/16.44 | (749) all_1021_2_1370 = all_917_2_1218 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_911_2_1209, all_1203_2_1611 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1203_2_1611, sdtasdt0(xa, all_181_0_257) = all_911_2_1209, yields: % 41.07/16.44 | (750) all_1203_2_1611 = all_911_2_1209 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_901_2_1195, all_1831_2_2392 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1831_2_2392, sdtasdt0(xa, all_181_0_257) = all_901_2_1195, yields: % 41.07/16.44 | (751) all_1831_2_2392 = all_901_2_1195 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_800_2_1061, all_1159_2_1556 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1159_2_1556, sdtasdt0(xa, all_181_0_257) = all_800_2_1061, yields: % 41.07/16.44 | (752) all_1159_2_1556 = all_800_2_1061 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_649_1_854, all_1831_2_2392 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1831_2_2392, sdtasdt0(xa, all_181_0_257) = all_649_1_854, yields: % 41.07/16.44 | (753) all_1831_2_2392 = all_649_1_854 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_463_2_608, all_1143_2_1534 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1143_2_1534, sdtasdt0(xa, all_181_0_257) = all_463_2_608, yields: % 41.07/16.44 | (754) all_1143_2_1534 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_461_2_605, all_649_1_854 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_649_1_854, sdtasdt0(xa, all_181_0_257) = all_461_2_605, yields: % 41.07/16.44 | (755) all_649_1_854 = all_461_2_605 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_459_2_602, all_0_10_10 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_459_2_602, sdtasdt0(xa, all_181_0_257) = all_0_10_10, yields: % 41.07/16.44 | (756) all_459_2_602 = all_0_10_10 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_459_2_602, all_1159_2_1556 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1159_2_1556, sdtasdt0(xa, all_181_0_257) = all_459_2_602, yields: % 41.07/16.44 | (757) all_1159_2_1556 = all_459_2_602 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_459_2_602, all_461_2_605 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_461_2_605, sdtasdt0(xa, all_181_0_257) = all_459_2_602, yields: % 41.07/16.44 | (758) all_461_2_605 = all_459_2_602 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_455_2_596, all_1285_2_1723 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1285_2_1723, sdtasdt0(xa, all_181_0_257) = all_455_2_596, yields: % 41.07/16.44 | (759) all_1285_2_1723 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_447_2_584, all_957_2_1274 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_957_2_1274, sdtasdt0(xa, all_181_0_257) = all_447_2_584, yields: % 41.07/16.44 | (760) all_957_2_1274 = all_447_2_584 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_447_2_584, all_917_2_1218 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_917_2_1218, sdtasdt0(xa, all_181_0_257) = all_447_2_584, yields: % 41.07/16.44 | (761) all_917_2_1218 = all_447_2_584 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_447_2_584, all_459_2_602 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_459_2_602, sdtasdt0(xa, all_181_0_257) = all_447_2_584, yields: % 41.07/16.44 | (762) all_459_2_602 = all_447_2_584 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_445_2_581, all_459_2_602 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_459_2_602, sdtasdt0(xa, all_181_0_257) = all_445_2_581, yields: % 41.07/16.44 | (763) all_459_2_602 = all_445_2_581 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_441_2_575, all_957_2_1274 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_957_2_1274, sdtasdt0(xa, all_181_0_257) = all_441_2_575, yields: % 41.07/16.44 | (764) all_957_2_1274 = all_441_2_575 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_439_2_572, all_1159_2_1556 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_1159_2_1556, sdtasdt0(xa, all_181_0_257) = all_439_2_572, yields: % 41.07/16.44 | (765) all_1159_2_1556 = all_439_2_572 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_437_2_569, all_917_2_1218 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_917_2_1218, sdtasdt0(xa, all_181_0_257) = all_437_2_569, yields: % 41.07/16.44 | (766) all_917_2_1218 = all_437_2_569 % 41.07/16.44 | % 41.07/16.44 | Instantiating formula (100) with xa, all_181_0_257, all_317_0_407, all_445_2_581 and discharging atoms sdtasdt0(xa, all_181_0_257) = all_445_2_581, sdtasdt0(xa, all_181_0_257) = all_317_0_407, yields: % 41.07/16.44 | (767) all_445_2_581 = all_317_0_407 % 41.07/16.44 | % 41.07/16.44 | Combining equations (736,740) yields a new equation: % 41.07/16.44 | (768) all_1331_1_1774 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Simplifying 768 yields: % 41.07/16.44 | (769) all_1331_1_1774 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Combining equations (753,751) yields a new equation: % 41.07/16.44 | (770) all_901_2_1195 = all_649_1_854 % 41.07/16.44 | % 41.07/16.44 | Combining equations (746,751) yields a new equation: % 41.07/16.44 | (771) all_932_2_1240 = all_901_2_1195 % 41.07/16.44 | % 41.07/16.44 | Simplifying 771 yields: % 41.07/16.44 | (772) all_932_2_1240 = all_901_2_1195 % 41.07/16.44 | % 41.07/16.44 | Combining equations (737,769) yields a new equation: % 41.07/16.44 | (773) all_1324_1_1764 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Simplifying 773 yields: % 41.07/16.44 | (774) all_1324_1_1764 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Combining equations (739,774) yields a new equation: % 41.07/16.44 | (775) all_1279_1_1714 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Simplifying 775 yields: % 41.07/16.44 | (776) all_1279_1_1714 = all_939_1_1246 % 41.07/16.44 | % 41.07/16.44 | Combining equations (741,759) yields a new equation: % 41.07/16.44 | (777) all_1279_2_1715 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Simplifying 777 yields: % 41.07/16.44 | (778) all_1279_2_1715 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Combining equations (738,776) yields a new equation: % 41.07/16.44 | (779) all_939_1_1246 = all_0_9_9 % 41.07/16.44 | % 41.07/16.44 | Combining equations (743,778) yields a new equation: % 41.07/16.44 | (780) all_1147_2_1540 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Simplifying 780 yields: % 41.07/16.44 | (781) all_1147_2_1540 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Combining equations (742,750) yields a new equation: % 41.07/16.44 | (782) all_1159_2_1556 = all_911_2_1209 % 41.07/16.44 | % 41.07/16.44 | Simplifying 782 yields: % 41.07/16.44 | (783) all_1159_2_1556 = all_911_2_1209 % 41.07/16.44 | % 41.07/16.44 | Combining equations (757,783) yields a new equation: % 41.07/16.44 | (784) all_911_2_1209 = all_459_2_602 % 41.07/16.44 | % 41.07/16.44 | Combining equations (765,783) yields a new equation: % 41.07/16.44 | (785) all_911_2_1209 = all_439_2_572 % 41.07/16.44 | % 41.07/16.44 | Combining equations (752,783) yields a new equation: % 41.07/16.44 | (786) all_911_2_1209 = all_800_2_1061 % 41.07/16.44 | % 41.07/16.44 | Combining equations (747,781) yields a new equation: % 41.07/16.44 | (787) all_932_2_1240 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Simplifying 787 yields: % 41.07/16.44 | (788) all_932_2_1240 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Combining equations (744,754) yields a new equation: % 41.07/16.44 | (789) all_1021_2_1370 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Simplifying 789 yields: % 41.07/16.44 | (790) all_1021_2_1370 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Combining equations (745,748) yields a new equation: % 41.07/16.44 | (791) all_1021_2_1370 = all_919_2_1221 % 41.07/16.44 | % 41.07/16.44 | Simplifying 791 yields: % 41.07/16.44 | (792) all_1021_2_1370 = all_919_2_1221 % 41.07/16.44 | % 41.07/16.44 | Combining equations (749,792) yields a new equation: % 41.07/16.44 | (793) all_919_2_1221 = all_917_2_1218 % 41.07/16.44 | % 41.07/16.44 | Combining equations (790,792) yields a new equation: % 41.07/16.44 | (794) all_919_2_1221 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Combining equations (760,764) yields a new equation: % 41.07/16.44 | (795) all_447_2_584 = all_441_2_575 % 41.07/16.44 | % 41.07/16.44 | Simplifying 795 yields: % 41.07/16.44 | (796) all_447_2_584 = all_441_2_575 % 41.07/16.44 | % 41.07/16.44 | Combining equations (772,788) yields a new equation: % 41.07/16.44 | (797) all_901_2_1195 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Simplifying 797 yields: % 41.07/16.44 | (798) all_901_2_1195 = all_455_2_596 % 41.07/16.44 | % 41.07/16.44 | Combining equations (793,794) yields a new equation: % 41.07/16.44 | (799) all_917_2_1218 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Simplifying 799 yields: % 41.07/16.44 | (800) all_917_2_1218 = all_463_2_608 % 41.07/16.44 | % 41.07/16.44 | Combining equations (761,800) yields a new equation: % 41.07/16.44 | (801) all_463_2_608 = all_447_2_584 % 41.07/16.44 | % 41.07/16.44 | Combining equations (766,800) yields a new equation: % 41.07/16.44 | (802) all_463_2_608 = all_437_2_569 % 41.07/16.44 | % 41.07/16.44 | Combining equations (784,786) yields a new equation: % 41.07/16.44 | (803) all_800_2_1061 = all_459_2_602 % 41.07/16.44 | % 41.07/16.44 | Combining equations (785,786) yields a new equation: % 41.07/16.44 | (804) all_800_2_1061 = all_439_2_572 % 41.07/16.44 | % 41.07/16.45 | Combining equations (770,798) yields a new equation: % 41.07/16.45 | (805) all_649_1_854 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Simplifying 805 yields: % 41.07/16.45 | (806) all_649_1_854 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Combining equations (803,804) yields a new equation: % 41.07/16.45 | (807) all_459_2_602 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Simplifying 807 yields: % 41.07/16.45 | (808) all_459_2_602 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Combining equations (755,806) yields a new equation: % 41.07/16.45 | (809) all_461_2_605 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Simplifying 809 yields: % 41.07/16.45 | (810) all_461_2_605 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Combining equations (801,802) yields a new equation: % 41.07/16.45 | (811) all_447_2_584 = all_437_2_569 % 41.07/16.45 | % 41.07/16.45 | Simplifying 811 yields: % 41.07/16.45 | (812) all_447_2_584 = all_437_2_569 % 41.07/16.45 | % 41.07/16.45 | Combining equations (758,810) yields a new equation: % 41.07/16.45 | (813) all_459_2_602 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Simplifying 813 yields: % 41.07/16.45 | (814) all_459_2_602 = all_455_2_596 % 41.07/16.45 | % 41.07/16.45 | Combining equations (763,814) yields a new equation: % 41.07/16.45 | (815) all_455_2_596 = all_445_2_581 % 41.07/16.45 | % 41.07/16.45 | Combining equations (756,814) yields a new equation: % 41.07/16.45 | (816) all_455_2_596 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (762,814) yields a new equation: % 41.07/16.45 | (817) all_455_2_596 = all_447_2_584 % 41.07/16.45 | % 41.07/16.45 | Combining equations (808,814) yields a new equation: % 41.07/16.45 | (818) all_455_2_596 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Combining equations (815,818) yields a new equation: % 41.07/16.45 | (819) all_445_2_581 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Simplifying 819 yields: % 41.07/16.45 | (820) all_445_2_581 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Combining equations (817,818) yields a new equation: % 41.07/16.45 | (821) all_447_2_584 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Simplifying 821 yields: % 41.07/16.45 | (822) all_447_2_584 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Combining equations (816,818) yields a new equation: % 41.07/16.45 | (823) all_439_2_572 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (812,796) yields a new equation: % 41.07/16.45 | (824) all_441_2_575 = all_437_2_569 % 41.07/16.45 | % 41.07/16.45 | Combining equations (822,796) yields a new equation: % 41.07/16.45 | (825) all_441_2_575 = all_439_2_572 % 41.07/16.45 | % 41.07/16.45 | Combining equations (820,767) yields a new equation: % 41.07/16.45 | (826) all_439_2_572 = all_317_0_407 % 41.07/16.45 | % 41.07/16.45 | Simplifying 826 yields: % 41.07/16.45 | (827) all_439_2_572 = all_317_0_407 % 41.07/16.45 | % 41.07/16.45 | Combining equations (825,824) yields a new equation: % 41.07/16.45 | (828) all_439_2_572 = all_437_2_569 % 41.07/16.45 | % 41.07/16.45 | Simplifying 828 yields: % 41.07/16.45 | (829) all_439_2_572 = all_437_2_569 % 41.07/16.45 | % 41.07/16.45 | Combining equations (823,829) yields a new equation: % 41.07/16.45 | (830) all_437_2_569 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (827,829) yields a new equation: % 41.07/16.45 | (831) all_437_2_569 = all_317_0_407 % 41.07/16.45 | % 41.07/16.45 | Combining equations (830,831) yields a new equation: % 41.07/16.45 | (832) all_317_0_407 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (832,831) yields a new equation: % 41.07/16.45 | (830) all_437_2_569 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (830,829) yields a new equation: % 41.07/16.45 | (823) all_439_2_572 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (823,818) yields a new equation: % 41.07/16.45 | (816) all_455_2_596 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (816,778) yields a new equation: % 41.07/16.45 | (836) all_1279_2_1715 = all_0_10_10 % 41.07/16.45 | % 41.07/16.45 | Combining equations (779,776) yields a new equation: % 41.07/16.45 | (738) all_1279_1_1714 = all_0_9_9 % 41.07/16.45 | % 41.07/16.45 | From (836)(738) and (710) follows: % 41.07/16.45 | (838) sdtpldt0(all_0_10_10, all_0_9_9) = all_1279_0_1713 % 41.07/16.45 | % 41.07/16.45 | Instantiating formula (136) with all_0_10_10, all_0_9_9, all_1279_0_1713, xu and discharging atoms sdtpldt0(all_0_10_10, all_0_9_9) = all_1279_0_1713, sdtpldt0(all_0_10_10, all_0_9_9) = xu, yields: % 41.07/16.45 | (839) all_1279_0_1713 = xu % 41.07/16.45 | % 41.07/16.45 | Equations (839) can reduce 707 to: % 41.07/16.45 | (840) $false % 41.07/16.45 | % 41.07/16.45 |-The branch is then unsatisfiable % 41.07/16.45 % SZS output end Proof for theBenchmark % 41.07/16.45 % 41.07/16.45 15854ms %------------------------------------------------------------------------------