%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM630+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n012.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 08:46:38 EDT 2022 % Result : Theorem 6.62s 2.16s % Output : Proof 15.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM630+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n012.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 : Wed Jul 6 10:05:00 EDT 2022 % 0.12/0.34 % CPUTime : % 0.55/0.61 ____ _ % 0.55/0.61 ___ / __ \_____(_)___ ________ __________ % 0.55/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.61 % 0.55/0.61 A Theorem Prover for First-Order Logic % 0.55/0.61 (ePrincess v.1.0) % 0.55/0.61 % 0.55/0.61 (c) Philipp Rümmer, 2009-2015 % 0.55/0.61 (c) Peter Backeman, 2014-2015 % 0.55/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.61 Bug reports to peter@backeman.se % 0.55/0.61 % 0.55/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.61 % 0.55/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.72/0.68 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.24/1.13 Prover 0: Preprocessing ... % 4.72/1.76 Prover 0: Constructing countermodel ... % 6.62/2.15 Prover 0: proved (1474ms) % 6.62/2.16 % 6.62/2.16 No countermodel exists, formula is valid % 6.62/2.16 % SZS status Theorem for theBenchmark % 6.62/2.16 % 6.62/2.16 Generating proof ... found it (size 81) % 14.59/4.01 % 14.59/4.01 % SZS output start Proof for theBenchmark % 14.59/4.02 Assumed formulas after preprocessing and simplification: % 14.59/4.02 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ( ~ (v15 = v13) & ~ (xQ = slcrc0) & ~ (xK = sz00) & szDzizrdt0(xd) = v3 & sdtlcdtrc0(xd, szNzAzT0) = v2 & sdtlcdtrc0(xe, v4) = xO & sdtlcdtrc0(xc, v0) = v1 & sdtlbdtrb0(xd, v3) = v4 & sdtlpdtrp0(v14, xP) = v15 & sdtlpdtrp0(xd, xn) = v3 & sdtlpdtrp0(xe, xn) = xp & sdtlpdtrp0(xC, xn) = v14 & sdtlpdtrp0(xN, v7) = v8 & sdtlpdtrp0(xN, xn) = v9 & sdtlpdtrp0(xN, sz00) = xS & sdtlpdtrp0(xc, v12) = v13 & szDzozmdt0(xd) = szNzAzT0 & szDzozmdt0(xe) = szNzAzT0 & szDzozmdt0(xC) = szNzAzT0 & szDzozmdt0(xN) = szNzAzT0 & szDzozmdt0(xc) = v0 & slbdtsldtrb0(xD, xk) = v11 & slbdtsldtrb0(xO, xk) = v6 & slbdtsldtrb0(xO, xK) = v5 & slbdtsldtrb0(xS, xK) = v0 & slbdtrb0(sz00) = slcrc0 & szmzizndt0(v9) = v10 & szmzizndt0(xQ) = xp & sbrdtbr0(xP) = xk & szszuzczcdt0(xn) = v7 & szszuzczcdt0(xk) = xK & sdtmndt0(v9, v10) = xD & sdtmndt0(xQ, xp) = xP & sdtpldt0(xP, v10) = v12 & aFunction0(xd) & aFunction0(xe) & aFunction0(xC) & aFunction0(xN) & aFunction0(xc) & aSubsetOf0(v2, xT) & aSubsetOf0(v1, xT) & aSubsetOf0(xP, v8) & aSubsetOf0(xP, xQ) & aSubsetOf0(xP, xO) & aSubsetOf0(xQ, xO) & aSubsetOf0(xQ, szNzAzT0) & aSubsetOf0(xO, xS) & aSubsetOf0(xS, szNzAzT0) & isCountable0(v4) & isCountable0(xO) & isCountable0(xS) & isCountable0(szNzAzT0) & isFinite0(xT) & isFinite0(slcrc0) & aElementOf0(v3, xT) & aElementOf0(xn, v4) & aElementOf0(xn, szNzAzT0) & aElementOf0(xP, v11) & aElementOf0(xP, v6) & aElementOf0(xp, xQ) & aElementOf0(xp, xO) & aElementOf0(xQ, v5) & aElementOf0(xQ, v0) & aElementOf0(xk, szNzAzT0) & aElementOf0(xK, szNzAzT0) & aElementOf0(sz00, szNzAzT0) & aSet0(xP) & aSet0(xO) & aSet0(xT) & aSet0(szNzAzT0) & aSet0(slcrc0) & ~ isCountable0(slcrc0) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ( ~ (sdtexdt0(v16, v18) = v19) | ~ (sdtlpdtrp0(v19, v21) = v22) | ~ (szDzozmdt0(v19) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ aElementOf0(v21, v18) | sdtlpdtrp0(v16, v21) = v22) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ( ~ (sdtexdt0(v16, v18) = v19) | ~ (sdtlpdtrp0(v16, v21) = v22) | ~ (szDzozmdt0(v19) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ aElementOf0(v21, v18) | sdtlpdtrp0(v19, v21) = v22) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (sdtlcdtrc0(v16, v18) = v19) | ~ (sdtlpdtrp0(v16, v21) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ aElementOf0(v21, v18) | aElementOf0(v20, v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = v19 | ~ (sdtexdt0(v16, v18) = v19) | ~ (szDzozmdt0(v20) = v18) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v20) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ? [v21] : ? [v22] : ? [v23] : ( ~ (v23 = v22) & sdtlpdtrp0(v20, v21) = v22 & sdtlpdtrp0(v16, v21) = v23 & aElementOf0(v21, v18))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = v19 | ~ (sdtlcdtrc0(v16, v18) = v19) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ aSet0(v20) | ? [v21] : ? [v22] : ? [v23] : (( ~ aElementOf0(v21, v20) | ! [v24] : ( ~ (sdtlpdtrp0(v16, v24) = v21) | ~ aElementOf0(v24, v18))) & (aElementOf0(v21, v20) | (v23 = v21 & sdtlpdtrp0(v16, v22) = v21 & aElementOf0(v22, v18))))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = v18 | ~ (sdtexdt0(v16, v18) = v19) | ~ (szDzozmdt0(v19) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = v17 | ~ (slbdtsldtrb0(v16, v17) = v18) | ~ (sbrdtbr0(v19) = v20) | ~ aElementOf0(v19, v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v19 = slcrc0 | v16 = sz00 | ~ (slbdtsldtrb0(v18, v16) = v20) | ~ (slbdtsldtrb0(v17, v16) = v19) | ~ aSubsetOf0(v19, v20) | ~ aElementOf0(v16, szNzAzT0) | ~ aSet0(v18) | ~ aSet0(v17) | aSubsetOf0(v17, v18)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtexdt0(v16, v18) = v19) | ~ (szDzozmdt0(v19) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | aFunction0(v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtlcdtrc0(v19, v18) = v20) | ~ (szDzozmdt0(v19) = v18) | ~ (slbdtsldtrb0(v17, v16) = v18) | ~ aFunction0(v19) | ~ iLess0(v16, xK) | ~ aSubsetOf0(v20, xT) | ~ aSubsetOf0(v17, szNzAzT0) | ~ isCountable0(v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v21] : ? [v22] : ? [v23] : (slbdtsldtrb0(v22, v16) = v23 & aSubsetOf0(v22, v17) & isCountable0(v22) & aElementOf0(v21, xT) & ! [v24] : ! [v25] : (v25 = v21 | ~ (sdtlpdtrp0(v19, v24) = v25) | ~ aElementOf0(v24, v23)))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtlcdtrc0(v16, v18) = v19) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ aElementOf0(v20, v19) | ? [v21] : (sdtlpdtrp0(v16, v21) = v20 & aElementOf0(v21, v18))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (sdtlcdtrc0(v16, v17) = v18) | ~ (sdtlpdtrp0(v16, v19) = v20) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aElementOf0(v19, v17) | aElementOf0(v20, v18)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (slbdtsldtrb0(v16, v17) = v18) | ~ (sbrdtbr0(v19) = v20) | ~ aElementOf0(v19, v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | aSubsetOf0(v19, v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v18 | v17 = slcrc0 | v16 = slcrc0 | ~ (szmzizndt0(v17) = v19) | ~ (szmzizndt0(v16) = v18) | ~ aSubsetOf0(v17, szNzAzT0) | ~ aSubsetOf0(v16, szNzAzT0) | ~ aElementOf0(v19, v16) | ~ aElementOf0(v18, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v18 | ~ (slbdtsldtrb0(v16, v17) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v19) | ~ aSet0(v16) | ? [v20] : ? [v21] : (sbrdtbr0(v20) = v21 & ( ~ (v21 = v17) | ~ aSubsetOf0(v20, v16) | ~ aElementOf0(v20, v19)) & (aElementOf0(v20, v19) | (v21 = v17 & aSubsetOf0(v20, v16))))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v18 | ~ (sdtmndt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aSet0(v19) | ~ aSet0(v16) | ? [v20] : ((v20 = v17 | ~ aElementOf0(v20, v19) | ~ aElementOf0(v20, v16) | ~ aElement0(v20)) & (aElementOf0(v20, v19) | ( ~ (v20 = v17) & aElementOf0(v20, v16) & aElement0(v20))))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v18 | ~ (sdtpldt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aSet0(v19) | ~ aSet0(v16) | ? [v20] : (( ~ aElementOf0(v20, v19) | ~ aElement0(v20) | ( ~ (v20 = v17) & ~ aElementOf0(v20, v16))) & (aElementOf0(v20, v19) | (aElement0(v20) & (v20 = v17 | aElementOf0(v20, v16)))))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v17 | ~ (sdtmndt0(v18, v16) = v19) | ~ (sdtpldt0(v17, v16) = v18) | ~ aElement0(v16) | ~ aSet0(v17) | aElementOf0(v16, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v17 | ~ (sdtmndt0(v16, v17) = v18) | ~ aElementOf0(v19, v16) | ~ aElement0(v19) | ~ aElement0(v17) | ~ aSet0(v16) | aElementOf0(v19, v18)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v17 | ~ (sdtpldt0(v16, v17) = v18) | ~ aElementOf0(v19, v18) | ~ aElement0(v17) | ~ aSet0(v16) | aElementOf0(v19, v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = v16 | ~ (sdtmndt0(v16, v17) = v18) | ~ (sdtpldt0(v18, v17) = v19) | ~ aElementOf0(v17, v16) | ~ aSet0(v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtexdt0(v19, v18) = v17) | ~ (sdtexdt0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtlcdtrc0(v19, v18) = v17) | ~ (sdtlcdtrc0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtlbdtrb0(v19, v18) = v17) | ~ (sdtlbdtrb0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtlpdtrp0(v19, v18) = v17) | ~ (sdtlpdtrp0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtlpdtrp0(xN, v17) = v19) | ~ (sdtlpdtrp0(xN, v16) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : ? [v21] : ( ~ (v21 = v20) & szmzizndt0(v19) = v21 & szmzizndt0(v18) = v20)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (slbdtsldtrb0(v19, v18) = v17) | ~ (slbdtsldtrb0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtmndt0(v19, v18) = v17) | ~ (sdtmndt0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v17 = v16 | ~ (sdtpldt0(v19, v18) = v17) | ~ (sdtpldt0(v19, v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlcdtrc0(v17, v18) = v19) | ~ (sdtlpdtrp0(xC, v16) = v17) | ~ (szDzozmdt0(v17) = v18) | ~ aElementOf0(v16, szNzAzT0) | aSubsetOf0(v19, xT)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlcdtrc0(v16, v18) = v19) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | ~ isCountable0(v18) | isCountable0(v19) | ? [v20] : ? [v21] : ? [v22] : ( ~ (v21 = v20) & sdtlpdtrp0(v16, v21) = v22 & sdtlpdtrp0(v16, v20) = v22 & aElementOf0(v21, v17) & aElementOf0(v20, v17))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlcdtrc0(v16, v18) = v19) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aSubsetOf0(v18, v17) | aSet0(v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(v16, v18) = v19) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ aElementOf0(v18, v17) | aElement0(v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v17) = v19) | ~ (sdtlpdtrp0(xN, v16) = v18) | ~ sdtlseqdt0(v17, v16) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | aSubsetOf0(v18, v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ (szmzizndt0(v17) = v18) | ~ (sdtmndt0(v17, v18) = v19) | ~ aSubsetOf0(v17, szNzAzT0) | ~ isCountable0(v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : ? [v21] : (sdtlpdtrp0(xN, v20) = v21 & szszuzczcdt0(v16) = v20 & aSubsetOf0(v21, v19) & isCountable0(v21))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ (szmzizndt0(v17) = v18) | ~ (sdtmndt0(v17, v18) = v19) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : ? [v21] : ? [v22] : ? [v23] : (sdtlpdtrp0(xC, v16) = v20 & slbdtsldtrb0(v22, xk) = v23 & aSubsetOf0(v22, v19) & isCountable0(v22) & aElementOf0(v21, xT) & ! [v24] : ! [v25] : (v25 = v21 | ~ (sdtlpdtrp0(v20, v24) = v25) | ~ aElementOf0(v24, v23) | ~ aSet0(v24)))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ (szmzizndt0(v17) = v18) | ~ (sdtmndt0(v17, v18) = v19) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : ? [v21] : (sdtlpdtrp0(xC, v16) = v20 & szDzozmdt0(v20) = v21 & slbdtsldtrb0(v19, xk) = v21 & aFunction0(v20) & ! [v22] : ! [v23] : ( ~ (sdtlpdtrp0(v20, v22) = v23) | ~ aElementOf0(v22, v21) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(xc, v24) = v23 & sdtpldt0(v22, v18) = v24)) & ! [v22] : ! [v23] : ( ~ (sdtpldt0(v22, v18) = v23) | ~ aElementOf0(v22, v21) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(v20, v22) = v24 & sdtlpdtrp0(xc, v23) = v24)))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ (szmzizndt0(v17) = v18) | ~ (sdtmndt0(v17, v18) = v19) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : (slbdtsldtrb0(v19, xk) = v20 & ! [v21] : ! [v22] : ! [v23] : ( ~ (slbdtsldtrb0(v21, xk) = v22) | ~ aSubsetOf0(v21, v19) | ~ isCountable0(v21) | ~ aElementOf0(v23, v22) | ~ aSet0(v23) | aElementOf0(v23, v20)))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ (szmzizndt0(v17) = v18) | ~ (sdtmndt0(v17, v18) = v19) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : (slbdtsldtrb0(v19, xk) = v20 & ! [v21] : ! [v22] : ( ~ (sdtpldt0(v21, v18) = v22) | ~ aElementOf0(v21, v20) | ~ aSet0(v21) | aElementOf0(v22, v0)))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (szDzozmdt0(v19) = v18) | ~ (slbdtsldtrb0(v17, v16) = v18) | ~ aFunction0(v19) | ~ iLess0(v16, xK) | ~ aSubsetOf0(v17, szNzAzT0) | ~ isCountable0(v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v20] : ? [v21] : ? [v22] : ((sdtlcdtrc0(v19, v18) = v20 & ~ aSubsetOf0(v20, xT)) | (slbdtsldtrb0(v21, v16) = v22 & aSubsetOf0(v21, v17) & isCountable0(v21) & aElementOf0(v20, xT) & ! [v23] : ! [v24] : (v24 = v20 | ~ (sdtlpdtrp0(v19, v23) = v24) | ~ aElementOf0(v23, v22))))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtsldtrb0(v16, v17) = v18) | ~ (sbrdtbr0(v19) = v17) | ~ aSubsetOf0(v19, v16) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | aElementOf0(v19, v18)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtsldtrb0(v16, v17) = v18) | ~ aSubsetOf0(v19, v18) | ~ isFinite0(v19) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | ? [v20] : ? [v21] : (slbdtsldtrb0(v20, v17) = v21 & aSubsetOf0(v20, v16) & aSubsetOf0(v19, v21) & isFinite0(v20))) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtrb0(v17) = v19) | ~ (slbdtrb0(v16) = v18) | ~ sdtlseqdt0(v16, v17) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | aSubsetOf0(v18, v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtrb0(v17) = v19) | ~ (slbdtrb0(v16) = v18) | ~ aSubsetOf0(v18, v19) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v16, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtrb0(v16) = v17) | ~ (szszuzczcdt0(v18) = v19) | ~ sdtlseqdt0(v19, v16) | ~ aElementOf0(v18, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | aElementOf0(v18, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtrb0(v16) = v17) | ~ (szszuzczcdt0(v18) = v19) | ~ aElementOf0(v18, v17) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v19, v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (slbdtrb0(v16) = v17) | ~ (szszuzczcdt0(v18) = v19) | ~ aElementOf0(v18, v17) | ~ aElementOf0(v16, szNzAzT0) | aElementOf0(v18, szNzAzT0)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sbrdtbr0(v18) = v19) | ~ (sbrdtbr0(v16) = v17) | ~ aSubsetOf0(v18, v16) | ~ isFinite0(v16) | ~ aSet0(v16) | sdtlseqdt0(v19, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sbrdtbr0(v16) = v17) | ~ (sdtmndt0(v16, v18) = v19) | ~ isFinite0(v16) | ~ aElementOf0(v18, v16) | ~ aSet0(v16) | ? [v20] : (sbrdtbr0(v19) = v20 & szszuzczcdt0(v20) = v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (szszuzczcdt0(v17) = v19) | ~ (szszuzczcdt0(v16) = v18) | ~ sdtlseqdt0(v18, v19) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v16, v17)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (szszuzczcdt0(v17) = v19) | ~ (szszuzczcdt0(v16) = v18) | ~ sdtlseqdt0(v16, v17) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v18, v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtmndt0(v16, v17) = v18) | ~ aElementOf0(v19, v18) | ~ aElement0(v17) | ~ aSet0(v16) | aElementOf0(v19, v16)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtmndt0(v16, v17) = v18) | ~ aElementOf0(v19, v18) | ~ aElement0(v17) | ~ aSet0(v16) | aElement0(v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ aElementOf0(v19, v18) | ~ aElement0(v17) | ~ aSet0(v16) | aElement0(v19)) & ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ aElementOf0(v19, v16) | ~ aElement0(v19) | ~ aElement0(v17) | ~ aSet0(v16) | aElementOf0(v19, v18)) & ! [v16] : ! [v17] : ! [v18] : (v18 = v17 | v16 = slcrc0 | ~ (szmzazxdt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | ~ isFinite0(v16) | ~ aElementOf0(v18, v16) | ? [v19] : (aElementOf0(v19, v16) & ~ sdtlseqdt0(v19, v18))) & ! [v16] : ! [v17] : ! [v18] : (v18 = v17 | v16 = slcrc0 | ~ (szmzizndt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | ~ aElementOf0(v18, v16) | ? [v19] : (aElementOf0(v19, v16) & ~ sdtlseqdt0(v18, v19))) & ! [v16] : ! [v17] : ! [v18] : (v18 = v17 | ~ (slbdtrb0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ~ aSet0(v18) | ? [v19] : ? [v20] : (szszuzczcdt0(v19) = v20 & ( ~ sdtlseqdt0(v20, v16) | ~ aElementOf0(v19, v18) | ~ aElementOf0(v19, szNzAzT0)) & (aElementOf0(v19, v18) | (sdtlseqdt0(v20, v16) & aElementOf0(v19, szNzAzT0))))) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szDzizrdt0(v18) = v17) | ~ (szDzizrdt0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szDzozmdt0(v18) = v17) | ~ (szDzozmdt0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (slbdtrb0(v18) = v17) | ~ (slbdtrb0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szmzazxdt0(v18) = v17) | ~ (szmzazxdt0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szmzizndt0(v18) = v17) | ~ (szmzizndt0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (sbrdtbr0(v18) = v17) | ~ (sbrdtbr0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szszuzczcdt0(v18) = v17) | ~ (szszuzczcdt0(v18) = v16)) & ! [v16] : ! [v17] : ! [v18] : (v17 = v16 | ~ (szszuzczcdt0(v17) = v18) | ~ (szszuzczcdt0(v16) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0)) & ! [v16] : ! [v17] : ! [v18] : (v17 = sz00 | ~ (slbdtsldtrb0(v16, v17) = v18) | ~ isCountable0(v16) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | isCountable0(v18)) & ! [v16] : ! [v17] : ! [v18] : (v16 = slcrc0 | ~ (szmzazxdt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | ~ isFinite0(v16) | ~ aElementOf0(v18, v16) | sdtlseqdt0(v18, v17)) & ! [v16] : ! [v17] : ! [v18] : (v16 = slcrc0 | ~ (szmzizndt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | ~ aElementOf0(v18, v16) | sdtlseqdt0(v17, v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (szDzizrdt0(v16) = v17) | ~ (sdtlbdtrb0(v16, v17) = v18) | ~ aFunction0(v16) | isCountable0(v18) | ? [v19] : ? [v20] : (sdtlcdtrc0(v16, v19) = v20 & szDzozmdt0(v16) = v19 & ( ~ isCountable0(v19) | ~ isFinite0(v20)))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (szDzizrdt0(v16) = v17) | ~ (sdtlbdtrb0(v16, v17) = v18) | ~ aFunction0(v16) | aElement0(v17) | ? [v19] : ? [v20] : (sdtlcdtrc0(v16, v19) = v20 & szDzozmdt0(v16) = v19 & ( ~ isCountable0(v19) | ~ isFinite0(v20)))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtlcdtrc0(v16, v17) = v18) | ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ isCountable0(v17) | ~ isFinite0(v18) | ? [v19] : ? [v20] : (szDzizrdt0(v16) = v19 & sdtlbdtrb0(v16, v19) = v20 & isCountable0(v20) & aElement0(v19))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtlbdtrb0(v16, v17) = v18) | ~ aFunction0(v16) | ~ aElement0(v17) | ? [v19] : (szDzozmdt0(v16) = v19 & aSubsetOf0(v18, v19))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtlbdtrb0(v16, v17) = v18) | ~ aFunction0(v16) | ~ aElement0(v17) | ? [v19] : (szDzozmdt0(v16) = v19 & aSet0(v18) & ! [v20] : ! [v21] : (v21 = v17 | ~ (sdtlpdtrp0(v16, v20) = v21) | ~ aElementOf0(v20, v18)) & ! [v20] : ! [v21] : ( ~ (sdtlpdtrp0(v16, v20) = v21) | ~ aElementOf0(v20, v18) | aElementOf0(v20, v19)) & ! [v20] : (v20 = v18 | ~ aSet0(v20) | ? [v21] : ? [v22] : (sdtlpdtrp0(v16, v21) = v22 & ( ~ (v22 = v17) | ~ aElementOf0(v21, v20) | ~ aElementOf0(v21, v19)) & (aElementOf0(v21, v20) | (v22 = v17 & aElementOf0(v21, v19))))) & ! [v20] : ( ~ (sdtlpdtrp0(v16, v20) = v17) | ~ aElementOf0(v20, v19) | aElementOf0(v20, v18)))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (slbdtsldtrb0(v16, v17) = v18) | ~ isFinite0(v16) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | isFinite0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (slbdtsldtrb0(v16, v17) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | aSet0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (slbdtrb0(v17) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | ? [v19] : ? [v20] : (slbdtrb0(v19) = v20 & szszuzczcdt0(v17) = v19 & (v17 = v16 | ~ aElementOf0(v16, v20) | aElementOf0(v16, v18)) & (aElementOf0(v16, v20) | ( ~ (v17 = v16) & ~ aElementOf0(v16, v18))))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sbrdtbr0(v16) = v18) | ~ sdtlseqdt0(v17, v18) | ~ isFinite0(v16) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | ? [v19] : (sbrdtbr0(v19) = v17 & aSubsetOf0(v19, v16))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (szszuzczcdt0(v17) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v18, v16) | sdtlseqdt0(v16, v17)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (szszuzczcdt0(v17) = v18) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | ? [v19] : ? [v20] : (slbdtrb0(v18) = v19 & slbdtrb0(v17) = v20 & (v17 = v16 | ~ aElementOf0(v16, v19) | aElementOf0(v16, v20)) & (aElementOf0(v16, v19) | ( ~ (v17 = v16) & ~ aElementOf0(v16, v20))))) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtmndt0(v17, v16) = v18) | ~ isCountable0(v17) | ~ aElement0(v16) | ~ aSet0(v17) | isCountable0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtmndt0(v17, v16) = v18) | ~ isFinite0(v17) | ~ aElement0(v16) | ~ aSet0(v17) | isFinite0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtmndt0(v16, v17) = v18) | ~ aElementOf0(v17, v18) | ~ aElement0(v17) | ~ aSet0(v16)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtmndt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aSet0(v16) | aSet0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v17, v16) = v18) | ~ isCountable0(v17) | ~ aElement0(v16) | ~ aSet0(v17) | isCountable0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v17, v16) = v18) | ~ isFinite0(v17) | ~ aElement0(v16) | ~ aSet0(v17) | isFinite0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aSet0(v16) | aElementOf0(v17, v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ (sdtpldt0(v16, v17) = v18) | ~ aElement0(v17) | ~ aSet0(v16) | aSet0(v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ sdtlseqdt0(v17, v18) | ~ sdtlseqdt0(v16, v17) | ~ aElementOf0(v18, szNzAzT0) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v16, v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ aSubsetOf0(v17, v18) | ~ aSubsetOf0(v16, v17) | ~ aSet0(v18) | ~ aSet0(v17) | ~ aSet0(v16) | aSubsetOf0(v16, v18)) & ! [v16] : ! [v17] : ! [v18] : ( ~ aSubsetOf0(v17, v16) | ~ aElementOf0(v18, v17) | ~ aSet0(v16) | aElementOf0(v18, v16)) & ! [v16] : ! [v17] : (v17 = v16 | ~ sdtlseqdt0(v17, v16) | ~ sdtlseqdt0(v16, v17) | ~ aElementOf0(v17, szNzAzT0) | ~ aElementOf0(v16, szNzAzT0)) & ! [v16] : ! [v17] : (v17 = v16 | ~ aSubsetOf0(v17, v16) | ~ aSubsetOf0(v16, v17) | ~ aSet0(v17) | ~ aSet0(v16)) & ! [v16] : ! [v17] : (v16 = slcrc0 | ~ (szmzazxdt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | ~ isFinite0(v16) | aElementOf0(v17, v16)) & ! [v16] : ! [v17] : (v16 = slcrc0 | ~ (szmzizndt0(v16) = v17) | ~ aSubsetOf0(v16, szNzAzT0) | aElementOf0(v17, v16)) & ! [v16] : ! [v17] : ( ~ (szDzizrdt0(v16) = v17) | ~ aFunction0(v16) | ? [v18] : ? [v19] : ? [v20] : (sdtlcdtrc0(v16, v18) = v19 & sdtlbdtrb0(v16, v17) = v20 & szDzozmdt0(v16) = v18 & ( ~ isCountable0(v18) | ~ isFinite0(v19) | (isCountable0(v20) & aElement0(v17))))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xd, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xC, v16) = v21 & sdtlpdtrp0(xN, v18) = v19 & slbdtsldtrb0(v19, xk) = v20 & szszuzczcdt0(v16) = v18 & ! [v22] : ! [v23] : (v23 = v17 | ~ (sdtlpdtrp0(v21, v22) = v23) | ~ aElementOf0(v22, v20) | ~ aSet0(v22)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xe, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : (sdtlpdtrp0(xN, v16) = v18 & szmzizndt0(v18) = v17)) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xC, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | aFunction0(v17)) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xC, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : (sdtlpdtrp0(xN, v16) = v18 & slbdtsldtrb0(v22, xk) = v23 & szmzizndt0(v18) = v19 & sdtmndt0(v18, v19) = v20 & aSubsetOf0(v22, v20) & isCountable0(v22) & aElementOf0(v21, xT) & ! [v24] : ! [v25] : (v25 = v21 | ~ (sdtlpdtrp0(v17, v24) = v25) | ~ aElementOf0(v24, v23) | ~ aSet0(v24)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xC, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xd, v16) = v21 & sdtlpdtrp0(xN, v18) = v19 & slbdtsldtrb0(v19, xk) = v20 & szszuzczcdt0(v16) = v18 & ! [v22] : ! [v23] : (v23 = v21 | ~ (sdtlpdtrp0(v17, v22) = v23) | ~ aElementOf0(v22, v20) | ~ aSet0(v22)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xC, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xN, v18) = v19 & slbdtsldtrb0(v19, xk) = v20 & szszuzczcdt0(v16) = v18 & aElementOf0(v21, xT) & ! [v22] : ! [v23] : (v23 = v21 | ~ (sdtlpdtrp0(v17, v22) = v23) | ~ aElementOf0(v22, v20) | ~ aSet0(v22)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xC, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xN, v16) = v19 & szDzozmdt0(v17) = v18 & slbdtsldtrb0(v21, xk) = v18 & szmzizndt0(v19) = v20 & sdtmndt0(v19, v20) = v21 & ! [v22] : ! [v23] : ( ~ (sdtlpdtrp0(v17, v22) = v23) | ~ aElementOf0(v22, v18) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(xc, v24) = v23 & sdtpldt0(v22, v20) = v24)) & ! [v22] : ! [v23] : ( ~ (sdtpldt0(v22, v20) = v23) | ~ aElementOf0(v22, v18) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(v17, v22) = v24 & sdtlpdtrp0(xc, v23) = v24)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aSubsetOf0(v17, szNzAzT0) | ~ isCountable0(v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xN, v18) = v19 & szmzizndt0(v17) = v20 & szszuzczcdt0(v16) = v18 & sdtmndt0(v17, v20) = v21 & aSubsetOf0(v19, v21) & isCountable0(v19))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | aSubsetOf0(v17, szNzAzT0)) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | isCountable0(v17)) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xC, v16) = v18 & szDzozmdt0(v18) = v19 & slbdtsldtrb0(v21, xk) = v19 & szmzizndt0(v17) = v20 & sdtmndt0(v17, v20) = v21 & aFunction0(v18) & ! [v22] : ! [v23] : ( ~ (sdtlpdtrp0(v18, v22) = v23) | ~ aElementOf0(v22, v19) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(xc, v24) = v23 & sdtpldt0(v22, v20) = v24)) & ! [v22] : ! [v23] : ( ~ (sdtpldt0(v22, v20) = v23) | ~ aElementOf0(v22, v19) | ~ aSet0(v22) | ? [v24] : (sdtlpdtrp0(v18, v22) = v24 & sdtlpdtrp0(xc, v23) = v24)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : (slbdtsldtrb0(v19, xk) = v20 & szmzizndt0(v17) = v18 & sdtmndt0(v17, v18) = v19 & ! [v21] : ! [v22] : ( ~ (sdtpldt0(v21, v18) = v22) | ~ aElementOf0(v21, v20) | ~ aSet0(v21) | aElementOf0(v22, v0)))) & ! [v16] : ! [v17] : ( ~ (sdtlpdtrp0(xN, v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : (sdtlpdtrp0(xe, v16) = v18 & szmzizndt0(v17) = v18)) & ! [v16] : ! [v17] : ( ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ~ isCountable0(v17) | ? [v18] : ? [v19] : ? [v20] : (szDzizrdt0(v16) = v19 & sdtlcdtrc0(v16, v17) = v18 & sdtlbdtrb0(v16, v19) = v20 & ( ~ isFinite0(v18) | (isCountable0(v20) & aElement0(v19))))) & ! [v16] : ! [v17] : ( ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | aSet0(v17)) & ! [v16] : ! [v17] : ( ~ (szDzozmdt0(v16) = v17) | ~ aFunction0(v16) | ? [v18] : (sdtlcdtrc0(v16, v17) = v18 & ! [v19] : ! [v20] : ( ~ (sdtlpdtrp0(v16, v19) = v20) | ~ aElementOf0(v19, v17) | aElementOf0(v20, v18)))) & ! [v16] : ! [v17] : ( ~ (slbdtsldtrb0(v16, v17) = slcrc0) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | isFinite0(v16)) & ! [v16] : ! [v17] : ( ~ (slbdtrb0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | sbrdtbr0(v17) = v16) & ! [v16] : ! [v17] : ( ~ (slbdtrb0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | isFinite0(v17)) & ! [v16] : ! [v17] : ( ~ (slbdtrb0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | aSet0(v17)) & ! [v16] : ! [v17] : ( ~ (sbrdtbr0(v16) = v17) | ~ isFinite0(v16) | ~ aSet0(v16) | aElementOf0(v17, szNzAzT0)) & ! [v16] : ! [v17] : ( ~ (sbrdtbr0(v16) = v17) | ~ isFinite0(v16) | ~ aSet0(v16) | ? [v18] : (szszuzczcdt0(v17) = v18 & ! [v19] : ! [v20] : ( ~ (sdtpldt0(v16, v19) = v20) | ~ aElement0(v19) | sbrdtbr0(v20) = v18 | aElementOf0(v19, v16)))) & ! [v16] : ! [v17] : ( ~ (sbrdtbr0(v16) = v17) | ~ aElementOf0(v17, szNzAzT0) | ~ aSet0(v16) | isFinite0(v16)) & ! [v16] : ! [v17] : ( ~ (sbrdtbr0(v16) = v17) | ~ aSet0(v16) | aElement0(v17)) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ sdtlseqdt0(v17, sz00) | ~ aElementOf0(v16, szNzAzT0)) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | iLess0(v16, v17)) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v16, v17)) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | aElementOf0(v17, szNzAzT0)) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xd, v16) = v20 & sdtlpdtrp0(xC, v16) = v21 & sdtlpdtrp0(xN, v17) = v18 & slbdtsldtrb0(v18, xk) = v19 & ! [v22] : ! [v23] : (v23 = v20 | ~ (sdtlpdtrp0(v21, v22) = v23) | ~ aElementOf0(v22, v19) | ~ aSet0(v22)))) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xC, v16) = v20 & sdtlpdtrp0(xN, v17) = v18 & slbdtsldtrb0(v18, xk) = v19 & aElementOf0(v21, xT) & ! [v22] : ! [v23] : (v23 = v21 | ~ (sdtlpdtrp0(v20, v22) = v23) | ~ aElementOf0(v22, v19) | ~ aSet0(v22)))) & ! [v16] : ! [v17] : ( ~ (szszuzczcdt0(v16) = v17) | ~ aElementOf0(v16, szNzAzT0) | ? [v18] : ? [v19] : ? [v20] : ? [v21] : (sdtlpdtrp0(xN, v17) = v19 & sdtlpdtrp0(xN, v16) = v18 & szmzizndt0(v18) = v20 & sdtmndt0(v18, v20) = v21 & ( ~ aSubsetOf0(v18, szNzAzT0) | ~ isCountable0(v18) | (aSubsetOf0(v19, v21) & isCountable0(v19))))) & ! [v16] : ! [v17] : ( ~ aSubsetOf0(v17, v16) | ~ isFinite0(v16) | ~ aSet0(v16) | isFinite0(v17)) & ! [v16] : ! [v17] : ( ~ aSubsetOf0(v17, v16) | ~ aSet0(v16) | aSet0(v17)) & ! [v16] : ! [v17] : ( ~ aElementOf0(v17, v16) | ~ aSet0(v16) | aElement0(v17)) & ! [v16] : ! [v17] : ( ~ aSet0(v17) | ~ aSet0(v16) | aSubsetOf0(v17, v16) | ? [v18] : (aElementOf0(v18, v17) & ~ aElementOf0(v18, v16))) & ! [v16] : (v16 = sz00 | ~ (sbrdtbr0(slcrc0) = v16)) & ! [v16] : (v16 = sz00 | ~ aElementOf0(v16, szNzAzT0) | ? [v17] : (szszuzczcdt0(v17) = v16 & aElementOf0(v17, szNzAzT0))) & ! [v16] : (v16 = slcrc0 | ~ (sbrdtbr0(v16) = sz00) | ~ aSet0(v16)) & ! [v16] : (v16 = slcrc0 | ~ aSet0(v16) | ? [v17] : aElementOf0(v17, v16)) & ! [v16] : ( ~ (szszuzczcdt0(v16) = v16) | ~ aElementOf0(v16, szNzAzT0)) & ! [v16] : ( ~ (szszuzczcdt0(v16) = sz00) | ~ aElementOf0(v16, szNzAzT0)) & ! [v16] : ( ~ aSubsetOf0(v16, szNzAzT0) | ~ isFinite0(v16) | ? [v17] : ? [v18] : (slbdtrb0(v17) = v18 & aSubsetOf0(v16, v18) & aElementOf0(v17, szNzAzT0))) & ! [v16] : ( ~ isCountable0(v16) | ~ isFinite0(v16) | ~ aSet0(v16)) & ! [v16] : ( ~ aElementOf0(v16, xO) | ? [v17] : (sdtlpdtrp0(xe, v17) = v16 & aElementOf0(v17, v4) & aElementOf0(v17, szNzAzT0))) & ! [v16] : ( ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(v16, v16)) & ! [v16] : ( ~ aElementOf0(v16, szNzAzT0) | sdtlseqdt0(sz00, v16)) & ! [v16] : ~ aElementOf0(v16, slcrc0) & ! [v16] : ( ~ aSet0(v16) | aSubsetOf0(v16, v16))) % 14.95/4.09 | 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, all_0_15_15 yields: % 14.95/4.09 | (1) ~ (all_0_0_0 = all_0_2_2) & ~ (xQ = slcrc0) & ~ (xK = sz00) & szDzizrdt0(xd) = all_0_12_12 & sdtlcdtrc0(xd, szNzAzT0) = all_0_13_13 & sdtlcdtrc0(xe, all_0_11_11) = xO & sdtlcdtrc0(xc, all_0_15_15) = all_0_14_14 & sdtlbdtrb0(xd, all_0_12_12) = all_0_11_11 & sdtlpdtrp0(all_0_1_1, xP) = all_0_0_0 & sdtlpdtrp0(xd, xn) = all_0_12_12 & sdtlpdtrp0(xe, xn) = xp & sdtlpdtrp0(xC, xn) = all_0_1_1 & sdtlpdtrp0(xN, all_0_8_8) = all_0_7_7 & sdtlpdtrp0(xN, xn) = all_0_6_6 & sdtlpdtrp0(xN, sz00) = xS & sdtlpdtrp0(xc, all_0_3_3) = all_0_2_2 & szDzozmdt0(xd) = szNzAzT0 & szDzozmdt0(xe) = szNzAzT0 & szDzozmdt0(xC) = szNzAzT0 & szDzozmdt0(xN) = szNzAzT0 & szDzozmdt0(xc) = all_0_15_15 & slbdtsldtrb0(xD, xk) = all_0_4_4 & slbdtsldtrb0(xO, xk) = all_0_9_9 & slbdtsldtrb0(xO, xK) = all_0_10_10 & slbdtsldtrb0(xS, xK) = all_0_15_15 & slbdtrb0(sz00) = slcrc0 & szmzizndt0(all_0_6_6) = all_0_5_5 & szmzizndt0(xQ) = xp & sbrdtbr0(xP) = xk & szszuzczcdt0(xn) = all_0_8_8 & szszuzczcdt0(xk) = xK & sdtmndt0(all_0_6_6, all_0_5_5) = xD & sdtmndt0(xQ, xp) = xP & sdtpldt0(xP, all_0_5_5) = all_0_3_3 & aFunction0(xd) & aFunction0(xe) & aFunction0(xC) & aFunction0(xN) & aFunction0(xc) & aSubsetOf0(all_0_13_13, xT) & aSubsetOf0(all_0_14_14, xT) & aSubsetOf0(xP, all_0_7_7) & aSubsetOf0(xP, xQ) & aSubsetOf0(xP, xO) & aSubsetOf0(xQ, xO) & aSubsetOf0(xQ, szNzAzT0) & aSubsetOf0(xO, xS) & aSubsetOf0(xS, szNzAzT0) & isCountable0(all_0_11_11) & isCountable0(xO) & isCountable0(xS) & isCountable0(szNzAzT0) & isFinite0(xT) & isFinite0(slcrc0) & aElementOf0(all_0_12_12, xT) & aElementOf0(xn, all_0_11_11) & aElementOf0(xn, szNzAzT0) & aElementOf0(xP, all_0_4_4) & aElementOf0(xP, all_0_9_9) & aElementOf0(xp, xQ) & aElementOf0(xp, xO) & aElementOf0(xQ, all_0_10_10) & aElementOf0(xQ, all_0_15_15) & aElementOf0(xk, szNzAzT0) & aElementOf0(xK, szNzAzT0) & aElementOf0(sz00, szNzAzT0) & aSet0(xP) & aSet0(xO) & aSet0(xT) & aSet0(szNzAzT0) & aSet0(slcrc0) & ~ isCountable0(slcrc0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (sdtlpdtrp0(v3, v5) = v6) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | sdtlpdtrp0(v0, v5) = v6) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (sdtlpdtrp0(v0, v5) = v6) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | sdtlpdtrp0(v3, v5) = v6) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (sdtlpdtrp0(v0, v5) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | aElementOf0(v4, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v4) = v2) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v4) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtlpdtrp0(v4, v5) = v6 & sdtlpdtrp0(v0, v5) = v7 & aElementOf0(v5, v2))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aSet0(v4) | ? [v5] : ? [v6] : ? [v7] : (( ~ aElementOf0(v5, v4) | ! [v8] : ( ~ (sdtlpdtrp0(v0, v8) = v5) | ~ aElementOf0(v8, v2))) & (aElementOf0(v5, v4) | (v7 = v5 & sdtlpdtrp0(v0, v6) = v5 & aElementOf0(v6, v2))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v4) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = slcrc0 | v0 = sz00 | ~ (slbdtsldtrb0(v2, v0) = v4) | ~ (slbdtsldtrb0(v1, v0) = v3) | ~ aSubsetOf0(v3, v4) | ~ aElementOf0(v0, szNzAzT0) | ~ aSet0(v2) | ~ aSet0(v1) | aSubsetOf0(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | aFunction0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v3, v2) = v4) | ~ (szDzozmdt0(v3) = v2) | ~ (slbdtsldtrb0(v1, v0) = v2) | ~ aFunction0(v3) | ~ iLess0(v0, xK) | ~ aSubsetOf0(v4, xT) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v5] : ? [v6] : ? [v7] : (slbdtsldtrb0(v6, v0) = v7 & aSubsetOf0(v6, v1) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v3, v8) = v9) | ~ aElementOf0(v8, v7)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v4, v3) | ? [v5] : (sdtlpdtrp0(v0, v5) = v4 & aElementOf0(v5, v2))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v0, v1) = v2) | ~ (sdtlpdtrp0(v0, v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aElementOf0(v3, v1) | aElementOf0(v4, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v4) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aSubsetOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v1 = slcrc0 | v0 = slcrc0 | ~ (szmzizndt0(v1) = v3) | ~ (szmzizndt0(v0) = v2) | ~ aSubsetOf0(v1, szNzAzT0) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v3, v0) | ~ aElementOf0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : ? [v5] : (sbrdtbr0(v4) = v5 & ( ~ (v5 = v1) | ~ aSubsetOf0(v4, v0) | ~ aElementOf0(v4, v3)) & (aElementOf0(v4, v3) | (v5 = v1 & aSubsetOf0(v4, v0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : ((v4 = v1 | ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v0) | ~ aElement0(v4)) & (aElementOf0(v4, v3) | ( ~ (v4 = v1) & aElementOf0(v4, v0) & aElement0(v4))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElement0(v4) | ( ~ (v4 = v1) & ~ aElementOf0(v4, v0))) & (aElementOf0(v4, v3) | (aElement0(v4) & (v4 = v1 | aElementOf0(v4, v0)))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v2, v0) = v3) | ~ (sdtpldt0(v1, v0) = v2) | ~ aElement0(v0) | ~ aSet0(v1) | aElementOf0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v0) | ~ aElement0(v3) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (sdtmndt0(v0, v1) = v2) | ~ (sdtpldt0(v2, v1) = v3) | ~ aElementOf0(v1, v0) | ~ aSet0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtexdt0(v3, v2) = v1) | ~ (sdtexdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlcdtrc0(v3, v2) = v1) | ~ (sdtlcdtrc0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlpdtrp0(v3, v2) = v1) | ~ (sdtlpdtrp0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlpdtrp0(xN, v1) = v3) | ~ (sdtlpdtrp0(xN, v0) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ( ~ (v5 = v4) & szmzizndt0(v3) = v5 & szmzizndt0(v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (slbdtsldtrb0(v3, v2) = v1) | ~ (slbdtsldtrb0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v1, v2) = v3) | ~ (sdtlpdtrp0(xC, v0) = v1) | ~ (szDzozmdt0(v1) = v2) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v3, xT)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ isCountable0(v2) | isCountable0(v3) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v5 = v4) & sdtlpdtrp0(v0, v5) = v6 & sdtlpdtrp0(v0, v4) = v6 & aElementOf0(v5, v1) & aElementOf0(v4, v1))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | aSet0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aElementOf0(v2, v1) | aElement0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v1) = v3) | ~ (sdtlpdtrp0(xN, v0) = v2) | ~ sdtlseqdt0(v1, v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v4) = v5 & szszuzczcdt0(v0) = v4 & aSubsetOf0(v5, v3) & isCountable0(v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlpdtrp0(xC, v0) = v4 & slbdtsldtrb0(v6, xk) = v7 & aSubsetOf0(v6, v3) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v4, v8) = v9) | ~ aElementOf0(v8, v7) | ~ aSet0(v8)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v4 & szDzozmdt0(v4) = v5 & slbdtsldtrb0(v3, xk) = v5 & aFunction0(v4) & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v4, v6) = v7) | ~ aElementOf0(v6, v5) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v2) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v2) = v7) | ~ aElementOf0(v6, v5) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v4, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (slbdtsldtrb0(v5, xk) = v6) | ~ aSubsetOf0(v5, v3) | ~ isCountable0(v5) | ~ aElementOf0(v7, v6) | ~ aSet0(v7) | aElementOf0(v7, v4)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v2) = v6) | ~ aElementOf0(v5, v4) | ~ aSet0(v5) | aElementOf0(v6, all_0_15_15)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szDzozmdt0(v3) = v2) | ~ (slbdtsldtrb0(v1, v0) = v2) | ~ aFunction0(v3) | ~ iLess0(v0, xK) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ? [v6] : ((sdtlcdtrc0(v3, v2) = v4 & ~ aSubsetOf0(v4, xT)) | (slbdtsldtrb0(v5, v0) = v6 & aSubsetOf0(v5, v1) & isCountable0(v5) & aElementOf0(v4, xT) & ! [v7] : ! [v8] : (v8 = v4 | ~ (sdtlpdtrp0(v3, v7) = v8) | ~ aElementOf0(v7, v6))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v1) | ~ aSubsetOf0(v3, v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aSubsetOf0(v3, v2) | ~ isFinite0(v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | ? [v4] : ? [v5] : (slbdtsldtrb0(v4, v1) = v5 & aSubsetOf0(v4, v0) & aSubsetOf0(v3, v5) & isFinite0(v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v1) = v3) | ~ (slbdtrb0(v0) = v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v1) = v3) | ~ (slbdtrb0(v0) = v2) | ~ aSubsetOf0(v2, v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ sdtlseqdt0(v3, v0) | ~ aElementOf0(v2, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v2, szNzAzT0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbrdtbr0(v2) = v3) | ~ (sbrdtbr0(v0) = v1) | ~ aSubsetOf0(v2, v0) | ~ isFinite0(v0) | ~ aSet0(v0) | sdtlseqdt0(v3, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbrdtbr0(v0) = v1) | ~ (sdtmndt0(v0, v2) = v3) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | ~ aSet0(v0) | ? [v4] : (sbrdtbr0(v3) = v4 & szszuzczcdt0(v4) = v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ~ sdtlseqdt0(v2, v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElement0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElement0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v0) | ~ aElement0(v3) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | ? [v3] : (aElementOf0(v3, v0) & ~ sdtlseqdt0(v3, v2))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v2, v0) | ? [v3] : (aElementOf0(v3, v0) & ~ sdtlseqdt0(v2, v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ~ aSet0(v2) | ? [v3] : ? [v4] : (szszuzczcdt0(v3) = v4 & ( ~ sdtlseqdt0(v4, v0) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v3, szNzAzT0)) & (aElementOf0(v3, v2) | (sdtlseqdt0(v4, v0) & aElementOf0(v3, szNzAzT0))))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szDzizrdt0(v2) = v1) | ~ (szDzizrdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szDzozmdt0(v2) = v1) | ~ (szDzozmdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (slbdtrb0(v2) = v1) | ~ (slbdtrb0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szmzazxdt0(v2) = v1) | ~ (szmzazxdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szmzizndt0(v2) = v1) | ~ (szmzizndt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ isCountable0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isCountable0(v2)) & ! [v0] : ! [v1] : ! [v2] : (v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | sdtlseqdt0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : (v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v2, v0) | sdtlseqdt0(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (szDzizrdt0(v0) = v1) | ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | isCountable0(v2) | ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v3) = v4 & szDzozmdt0(v0) = v3 & ( ~ isCountable0(v3) | ~ isFinite0(v4)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (szDzizrdt0(v0) = v1) | ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | aElement0(v1) | ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v3) = v4 & szDzozmdt0(v0) = v3 & ( ~ isCountable0(v3) | ~ isFinite0(v4)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlcdtrc0(v0, v1) = v2) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ isCountable0(v1) | ~ isFinite0(v2) | ? [v3] : ? [v4] : (szDzizrdt0(v0) = v3 & sdtlbdtrb0(v0, v3) = v4 & isCountable0(v4) & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | ~ aElement0(v1) | ? [v3] : (szDzozmdt0(v0) = v3 & aSubsetOf0(v2, v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | ~ aElement0(v1) | ? [v3] : (szDzozmdt0(v0) = v3 & aSet0(v2) & ! [v4] : ! [v5] : (v5 = v1 | ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v2)) & ! [v4] : ! [v5] : ( ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v2) | aElementOf0(v4, v3)) & ! [v4] : (v4 = v2 | ~ aSet0(v4) | ? [v5] : ? [v6] : (sdtlpdtrp0(v0, v5) = v6 & ( ~ (v6 = v1) | ~ aElementOf0(v5, v4) | ~ aElementOf0(v5, v3)) & (aElementOf0(v5, v4) | (v6 = v1 & aElementOf0(v5, v3))))) & ! [v4] : ( ~ (sdtlpdtrp0(v0, v4) = v1) | ~ aElementOf0(v4, v3) | aElementOf0(v4, v2)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ isFinite0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtrb0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v3] : ? [v4] : (slbdtrb0(v3) = v4 & szszuzczcdt0(v1) = v3 & (v1 = v0 | ~ aElementOf0(v0, v4) | aElementOf0(v0, v2)) & (aElementOf0(v0, v4) | ( ~ (v1 = v0) & ~ aElementOf0(v0, v2))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sbrdtbr0(v0) = v2) | ~ sdtlseqdt0(v1, v2) | ~ isFinite0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | ? [v3] : (sbrdtbr0(v3) = v1 & aSubsetOf0(v3, v0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (szszuzczcdt0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v2, v0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (szszuzczcdt0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v3] : ? [v4] : (slbdtrb0(v2) = v3 & slbdtrb0(v1) = v4 & (v1 = v0 | ~ aElementOf0(v0, v3) | aElementOf0(v0, v4)) & (aElementOf0(v0, v3) | ( ~ (v1 = v0) & ~ aElementOf0(v0, v4))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ isCountable0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isCountable0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ isFinite0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isFinite0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v1, v2) | ~ aElement0(v1) | ~ aSet0(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ isCountable0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isCountable0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ isFinite0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isFinite0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v2, szNzAzT0) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v2) | ~ aSubsetOf0(v0, v1) | ~ aSet0(v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v0) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aElementOf0(v2, v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ aSubsetOf0(v1, v0) | ~ aSubsetOf0(v0, v1) | ~ aSet0(v1) | ~ aSet0(v0)) & ! [v0] : ! [v1] : (v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | aElementOf0(v1, v0)) & ! [v0] : ! [v1] : (v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | aElementOf0(v1, v0)) & ! [v0] : ! [v1] : ( ~ (szDzizrdt0(v0) = v1) | ~ aFunction0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v2) = v3 & sdtlbdtrb0(v0, v1) = v4 & szDzozmdt0(v0) = v2 & ( ~ isCountable0(v2) | ~ isFinite0(v3) | (isCountable0(v4) & aElement0(v1))))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xd, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v5 & sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & ! [v6] : ! [v7] : (v7 = v1 | ~ (sdtlpdtrp0(v5, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xe, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : (sdtlpdtrp0(xN, v0) = v2 & szmzizndt0(v2) = v1)) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aFunction0(v1)) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlpdtrp0(xN, v0) = v2 & slbdtsldtrb0(v6, xk) = v7 & szmzizndt0(v2) = v3 & sdtmndt0(v2, v3) = v4 & aSubsetOf0(v6, v4) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v1, v8) = v9) | ~ aElementOf0(v8, v7) | ~ aSet0(v8)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xd, v0) = v5 & sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & aElementOf0(v5, xT) & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v0) = v3 & szDzozmdt0(v1) = v2 & slbdtsldtrb0(v5, xk) = v2 & szmzizndt0(v3) = v4 & sdtmndt0(v3, v4) = v5 & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v2) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v4) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v4) = v7) | ~ aElementOf0(v6, v2) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v1, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v2) = v3 & szmzizndt0(v1) = v4 & szszuzczcdt0(v0) = v2 & sdtmndt0(v1, v4) = v5 & aSubsetOf0(v3, v5) & isCountable0(v3))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v1, szNzAzT0)) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | isCountable0(v1)) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v2 & szDzozmdt0(v2) = v3 & slbdtsldtrb0(v5, xk) = v3 & szmzizndt0(v1) = v4 & sdtmndt0(v1, v4) = v5 & aFunction0(v2) & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v2, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v4) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v4) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v2, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & szmzizndt0(v1) = v2 & sdtmndt0(v1, v2) = v3 & ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v2) = v6) | ~ aElementOf0(v5, v4) | ~ aSet0(v5) | aElementOf0(v6, all_0_15_15)))) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : (sdtlpdtrp0(xe, v0) = v2 & szmzizndt0(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ isCountable0(v1) | ? [v2] : ? [v3] : ? [v4] : (szDzizrdt0(v0) = v3 & sdtlcdtrc0(v0, v1) = v2 & sdtlbdtrb0(v0, v3) = v4 & ( ~ isFinite0(v2) | (isCountable0(v4) & aElement0(v3))))) & ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ? [v2] : (sdtlcdtrc0(v0, v1) = v2 & ! [v3] : ! [v4] : ( ~ (sdtlpdtrp0(v0, v3) = v4) | ~ aElementOf0(v3, v1) | aElementOf0(v4, v2)))) & ! [v0] : ! [v1] : ( ~ (slbdtsldtrb0(v0, v1) = slcrc0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v0)) & ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | sbrdtbr0(v1) = v0) & ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | isFinite0(v1)) & ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | aElementOf0(v1, szNzAzT0)) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | ? [v2] : (szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ aElement0(v3) | sbrdtbr0(v4) = v2 | aElementOf0(v3, v0)))) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v0)) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ aSet0(v0) | aElement0(v1)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ sdtlseqdt0(v1, sz00) | ~ aElementOf0(v0, szNzAzT0)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | iLess0(v0, v1)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v1, szNzAzT0)) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xd, v0) = v4 & sdtlpdtrp0(xC, v0) = v5 & sdtlpdtrp0(xN, v1) = v2 & slbdtsldtrb0(v2, xk) = v3 & ! [v6] : ! [v7] : (v7 = v4 | ~ (sdtlpdtrp0(v5, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6)))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v4 & sdtlpdtrp0(xN, v1) = v2 & slbdtsldtrb0(v2, xk) = v3 & aElementOf0(v5, xT) & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v4, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6)))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v1) = v3 & sdtlpdtrp0(xN, v0) = v2 & szmzizndt0(v2) = v4 & sdtmndt0(v2, v4) = v5 & ( ~ aSubsetOf0(v2, szNzAzT0) | ~ isCountable0(v2) | (aSubsetOf0(v3, v5) & isCountable0(v3))))) & ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ isFinite0(v0) | ~ aSet0(v0) | isFinite0(v1)) & ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ aSet0(v0) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ aElementOf0(v1, v0) | ~ aSet0(v0) | aElement0(v1)) & ! [v0] : ! [v1] : ( ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v1, v0) | ? [v2] : (aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) & ! [v0] : (v0 = sz00 | ~ (sbrdtbr0(slcrc0) = v0)) & ! [v0] : (v0 = sz00 | ~ aElementOf0(v0, szNzAzT0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aElementOf0(v1, szNzAzT0))) & ! [v0] : (v0 = slcrc0 | ~ (sbrdtbr0(v0) = sz00) | ~ aSet0(v0)) & ! [v0] : (v0 = slcrc0 | ~ aSet0(v0) | ? [v1] : aElementOf0(v1, v0)) & ! [v0] : ( ~ (szszuzczcdt0(v0) = v0) | ~ aElementOf0(v0, szNzAzT0)) & ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aElementOf0(v0, szNzAzT0)) & ! [v0] : ( ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ? [v1] : ? [v2] : (slbdtrb0(v1) = v2 & aSubsetOf0(v0, v2) & aElementOf0(v1, szNzAzT0))) & ! [v0] : ( ~ isCountable0(v0) | ~ isFinite0(v0) | ~ aSet0(v0)) & ! [v0] : ( ~ aElementOf0(v0, xO) | ? [v1] : (sdtlpdtrp0(xe, v1) = v0 & aElementOf0(v1, all_0_11_11) & aElementOf0(v1, szNzAzT0))) & ! [v0] : ( ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v0)) & ! [v0] : ( ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(sz00, v0)) & ! [v0] : ~ aElementOf0(v0, slcrc0) & ! [v0] : ( ~ aSet0(v0) | aSubsetOf0(v0, v0)) % 15.31/4.13 | % 15.31/4.13 | Applying alpha-rule on (1) yields: % 15.31/4.13 | (2) ! [v0] : ! [v1] : ! [v2] : (v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | sdtlseqdt0(v2, v1)) % 15.31/4.13 | (3) szszuzczcdt0(xk) = xK % 15.31/4.13 | (4) ! [v0] : ( ~ aElementOf0(v0, xO) | ? [v1] : (sdtlpdtrp0(xe, v1) = v0 & aElementOf0(v1, all_0_11_11) & aElementOf0(v1, szNzAzT0))) % 15.31/4.13 | (5) aElementOf0(xK, szNzAzT0) % 15.31/4.13 | (6) ! [v0] : ( ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(sz00, v0)) % 15.31/4.13 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aSet0(v2)) % 15.31/4.13 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ (szszuzczcdt0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v2, v0) | sdtlseqdt0(v0, v1)) % 15.31/4.13 | (9) aElementOf0(xp, xO) % 15.31/4.13 | (10) isFinite0(xT) % 15.31/4.13 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) % 15.31/4.13 | (12) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xd, v0) = v4 & sdtlpdtrp0(xC, v0) = v5 & sdtlpdtrp0(xN, v1) = v2 & slbdtsldtrb0(v2, xk) = v3 & ! [v6] : ! [v7] : (v7 = v4 | ~ (sdtlpdtrp0(v5, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6)))) % 15.31/4.13 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v2) = v6) | ~ aElementOf0(v5, v4) | ~ aSet0(v5) | aElementOf0(v6, all_0_15_15)))) % 15.31/4.13 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0)) % 15.31/4.13 | (15) ! [v0] : ~ aElementOf0(v0, slcrc0) % 15.31/4.13 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 15.31/4.13 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szDzozmdt0(v2) = v1) | ~ (szDzozmdt0(v2) = v0)) % 15.31/4.13 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szDzozmdt0(v3) = v2) | ~ (slbdtsldtrb0(v1, v0) = v2) | ~ aFunction0(v3) | ~ iLess0(v0, xK) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ? [v6] : ((sdtlcdtrc0(v3, v2) = v4 & ~ aSubsetOf0(v4, xT)) | (slbdtsldtrb0(v5, v0) = v6 & aSubsetOf0(v5, v1) & isCountable0(v5) & aElementOf0(v4, xT) & ! [v7] : ! [v8] : (v8 = v4 | ~ (sdtlpdtrp0(v3, v7) = v8) | ~ aElementOf0(v7, v6))))) % 15.31/4.14 | (19) szDzozmdt0(xN) = szNzAzT0 % 15.31/4.14 | (20) ! [v0] : ! [v1] : ! [v2] : (v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v2, v0) | sdtlseqdt0(v1, v2)) % 15.31/4.14 | (21) aElementOf0(xP, all_0_9_9) % 15.31/4.14 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ~ sdtlseqdt0(v2, v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) % 15.31/4.14 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbrdtbr0(v0) = v1) | ~ (sdtmndt0(v0, v2) = v3) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | ~ aSet0(v0) | ? [v4] : (sbrdtbr0(v3) = v4 & szszuzczcdt0(v4) = v1)) % 15.31/4.14 | (24) sdtlcdtrc0(xe, all_0_11_11) = xO % 15.31/4.14 | (25) ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ isFinite0(v0) | ~ aSet0(v0) | isFinite0(v1)) % 15.31/4.14 | (26) ! [v0] : (v0 = slcrc0 | ~ aSet0(v0) | ? [v1] : aElementOf0(v1, v0)) % 15.31/4.14 | (27) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v2 & szDzozmdt0(v2) = v3 & slbdtsldtrb0(v5, xk) = v3 & szmzizndt0(v1) = v4 & sdtmndt0(v1, v4) = v5 & aFunction0(v2) & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v2, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v4) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v4) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v2, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) % 15.31/4.14 | (28) sdtlpdtrp0(xe, xn) = xp % 15.31/4.14 | (29) ! [v0] : ! [v1] : ( ~ (slbdtsldtrb0(v0, v1) = slcrc0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v0)) % 15.31/4.14 | (30) ! [v0] : ( ~ aSet0(v0) | aSubsetOf0(v0, v0)) % 15.31/4.14 | (31) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (slbdtrb0(v2) = v1) | ~ (slbdtrb0(v2) = v0)) % 15.31/4.14 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlpdtrp0(xC, v0) = v4 & slbdtsldtrb0(v6, xk) = v7 & aSubsetOf0(v6, v3) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v4, v8) = v9) | ~ aElementOf0(v8, v7) | ~ aSet0(v8)))) % 15.31/4.14 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szmzizndt0(v2) = v1) | ~ (szmzizndt0(v2) = v0)) % 15.31/4.14 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (sbrdtbr0(v0) = v2) | ~ sdtlseqdt0(v1, v2) | ~ isFinite0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | ? [v3] : (sbrdtbr0(v3) = v1 & aSubsetOf0(v3, v0))) % 15.31/4.14 | (35) aElementOf0(xn, szNzAzT0) % 15.31/4.14 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ isCountable0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isCountable0(v2)) % 15.31/4.14 | (37) sdtlpdtrp0(xc, all_0_3_3) = all_0_2_2 % 15.31/4.14 | (38) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ sdtlseqdt0(v1, sz00) | ~ aElementOf0(v0, szNzAzT0)) % 15.31/4.14 | (39) ! [v0] : ! [v1] : (v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | aElementOf0(v1, v0)) % 15.31/4.14 | (40) slbdtsldtrb0(xO, xK) = all_0_10_10 % 15.31/4.14 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v2, v0) = v3) | ~ (sdtpldt0(v1, v0) = v2) | ~ aElement0(v0) | ~ aSet0(v1) | aElementOf0(v0, v1)) % 15.31/4.14 | (42) ! [v0] : ! [v1] : (v1 = v0 | ~ aSubsetOf0(v1, v0) | ~ aSubsetOf0(v0, v1) | ~ aSet0(v1) | ~ aSet0(v0)) % 15.31/4.14 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ isCountable0(v2) | isCountable0(v3) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v5 = v4) & sdtlpdtrp0(v0, v5) = v6 & sdtlpdtrp0(v0, v4) = v6 & aElementOf0(v5, v1) & aElementOf0(v4, v1))) % 15.31/4.14 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v1, v2) = v3) | ~ (sdtlpdtrp0(xC, v0) = v1) | ~ (szDzozmdt0(v1) = v2) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v3, xT)) % 15.31/4.14 | (45) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) % 15.31/4.14 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = slcrc0 | v0 = sz00 | ~ (slbdtsldtrb0(v2, v0) = v4) | ~ (slbdtsldtrb0(v1, v0) = v3) | ~ aSubsetOf0(v3, v4) | ~ aElementOf0(v0, szNzAzT0) | ~ aSet0(v2) | ~ aSet0(v1) | aSubsetOf0(v1, v2)) % 15.31/4.14 | (47) aElementOf0(xQ, all_0_15_15) % 15.31/4.14 | (48) ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtrb0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v3] : ? [v4] : (slbdtrb0(v3) = v4 & szszuzczcdt0(v1) = v3 & (v1 = v0 | ~ aElementOf0(v0, v4) | aElementOf0(v0, v2)) & (aElementOf0(v0, v4) | ( ~ (v1 = v0) & ~ aElementOf0(v0, v2))))) % 15.31/4.14 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v3, v2) = v4) | ~ (szDzozmdt0(v3) = v2) | ~ (slbdtsldtrb0(v1, v0) = v2) | ~ aFunction0(v3) | ~ iLess0(v0, xK) | ~ aSubsetOf0(v4, xT) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v5] : ? [v6] : ? [v7] : (slbdtsldtrb0(v6, v0) = v7 & aSubsetOf0(v6, v1) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v3, v8) = v9) | ~ aElementOf0(v8, v7)))) % 15.31/4.14 | (50) aFunction0(xC) % 15.31/4.14 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ sdtlseqdt0(v3, v0) | ~ aElementOf0(v2, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v2, v1)) % 15.31/4.14 | (52) sdtlbdtrb0(xd, all_0_12_12) = all_0_11_11 % 15.31/4.14 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (sdtlpdtrp0(v0, v5) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | aElementOf0(v4, v3)) % 15.31/4.15 | (54) szDzozmdt0(xc) = all_0_15_15 % 15.31/4.15 | (55) ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ? [v2] : (sdtlcdtrc0(v0, v1) = v2 & ! [v3] : ! [v4] : ( ~ (sdtlpdtrp0(v0, v3) = v4) | ~ aElementOf0(v3, v1) | aElementOf0(v4, v2)))) % 15.31/4.15 | (56) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v1) = v3 & sdtlpdtrp0(xN, v0) = v2 & szmzizndt0(v2) = v4 & sdtmndt0(v2, v4) = v5 & ( ~ aSubsetOf0(v2, szNzAzT0) | ~ isCountable0(v2) | (aSubsetOf0(v3, v5) & isCountable0(v3))))) % 15.31/4.15 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbrdtbr0(v2) = v3) | ~ (sbrdtbr0(v0) = v1) | ~ aSubsetOf0(v2, v0) | ~ isFinite0(v0) | ~ aSet0(v0) | sdtlseqdt0(v3, v1)) % 15.31/4.15 | (58) aSubsetOf0(xO, xS) % 15.31/4.15 | (59) ! [v0] : ! [v1] : ( ~ aElementOf0(v1, v0) | ~ aSet0(v0) | aElement0(v1)) % 15.31/4.15 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ isFinite0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isFinite0(v2)) % 15.31/4.15 | (61) aSet0(xP) % 15.31/4.15 | (62) aSubsetOf0(xP, xQ) % 15.31/4.15 | (63) ! [v0] : (v0 = slcrc0 | ~ (sbrdtbr0(v0) = sz00) | ~ aSet0(v0)) % 15.31/4.15 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 15.31/4.15 | (65) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v0 = slcrc0 | ~ (szmzazxdt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ~ aElementOf0(v2, v0) | ? [v3] : (aElementOf0(v3, v0) & ~ sdtlseqdt0(v3, v2))) % 15.31/4.15 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szDzizrdt0(v2) = v1) | ~ (szDzizrdt0(v2) = v0)) % 15.31/4.15 | (67) ! [v0] : ( ~ (szszuzczcdt0(v0) = sz00) | ~ aElementOf0(v0, szNzAzT0)) % 15.31/4.15 | (68) ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ aSet0(v0) | aSet0(v1)) % 15.31/4.15 | (69) sdtmndt0(xQ, xp) = xP % 15.31/4.15 | (70) slbdtsldtrb0(xS, xK) = all_0_15_15 % 15.31/4.15 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : ((v4 = v1 | ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v0) | ~ aElement0(v4)) & (aElementOf0(v4, v3) | ( ~ (v4 = v1) & aElementOf0(v4, v0) & aElement0(v4))))) % 15.31/4.15 | (72) sdtlcdtrc0(xd, szNzAzT0) = all_0_13_13 % 15.31/4.15 | (73) sdtlpdtrp0(xC, xn) = all_0_1_1 % 15.31/4.15 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v1) = v3) | ~ (slbdtrb0(v0) = v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v2, v3)) % 15.31/4.15 | (75) ! [v0] : ( ~ (szszuzczcdt0(v0) = v0) | ~ aElementOf0(v0, szNzAzT0)) % 15.31/4.15 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & ! [v5] : ! [v6] : ! [v7] : ( ~ (slbdtsldtrb0(v5, xk) = v6) | ~ aSubsetOf0(v5, v3) | ~ isCountable0(v5) | ~ aElementOf0(v7, v6) | ~ aSet0(v7) | aElementOf0(v7, v4)))) % 15.31/4.15 | (77) sdtlpdtrp0(all_0_1_1, xP) = all_0_0_0 % 15.31/4.15 | (78) ~ (xQ = slcrc0) % 15.31/4.15 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElement0(v4) | ( ~ (v4 = v1) & ~ aElementOf0(v4, v0))) & (aElementOf0(v4, v3) | (aElement0(v4) & (v4 = v1 | aElementOf0(v4, v0)))))) % 15.31/4.15 | (80) aSet0(xO) % 15.31/4.15 | (81) ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ isCountable0(v1) | ? [v2] : ? [v3] : ? [v4] : (szDzizrdt0(v0) = v3 & sdtlcdtrc0(v0, v1) = v2 & sdtlbdtrb0(v0, v3) = v4 & ( ~ isFinite0(v2) | (isCountable0(v4) & aElement0(v3))))) % 15.31/4.15 | (82) aSubsetOf0(xP, xO) % 15.31/4.15 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v2) | ~ aSubsetOf0(v0, v1) | ~ aSet0(v2) | ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v0, v2)) % 15.31/4.15 | (84) szszuzczcdt0(xn) = all_0_8_8 % 15.31/4.15 | (85) sdtlpdtrp0(xN, xn) = all_0_6_6 % 15.31/4.15 | (86) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | isCountable0(v1)) % 15.31/4.15 | (87) aFunction0(xN) % 15.31/4.15 | (88) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v0) | ~ aElement0(v3) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) % 15.31/4.15 | (89) aElementOf0(xp, xQ) % 15.31/4.15 | (90) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aFunction0(v1)) % 15.31/4.15 | (91) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) % 15.31/4.15 | (92) slbdtsldtrb0(xD, xk) = all_0_4_4 % 15.31/4.15 | (93) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & aElementOf0(v5, xT) & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) % 15.31/4.15 | (94) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0)) % 15.31/4.15 | (95) sdtlpdtrp0(xd, xn) = all_0_12_12 % 15.31/4.15 | (96) aSet0(slcrc0) % 15.31/4.15 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szmzazxdt0(v2) = v1) | ~ (szmzazxdt0(v2) = v0)) % 15.31/4.15 | (98) aElementOf0(xn, all_0_11_11) % 15.31/4.15 | (99) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v0) | ~ aElement0(v3) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v2)) % 15.31/4.16 | (100) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlcdtrc0(v0, v1) = v2) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ isCountable0(v1) | ~ isFinite0(v2) | ? [v3] : ? [v4] : (szDzizrdt0(v0) = v3 & sdtlbdtrb0(v0, v3) = v4 & isCountable0(v4) & aElement0(v3))) % 15.31/4.16 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v1) | ~ aSubsetOf0(v3, v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aElementOf0(v3, v2)) % 15.31/4.16 | (102) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | aElementOf0(v1, szNzAzT0)) % 15.31/4.16 | (103) ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aSet0(v2)) % 15.31/4.16 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v4, v3) | ? [v5] : (sdtlpdtrp0(v0, v5) = v4 & aElementOf0(v5, v2))) % 15.31/4.16 | (105) aElementOf0(all_0_12_12, xT) % 15.31/4.16 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (slbdtsldtrb0(v3, v2) = v1) | ~ (slbdtsldtrb0(v3, v2) = v0)) % 15.31/4.16 | (107) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ isCountable0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isCountable0(v2)) % 15.31/4.16 | (108) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1)) % 15.31/4.16 | (109) szmzizndt0(all_0_6_6) = all_0_5_5 % 15.31/4.16 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v1) = v3) | ~ (sdtlpdtrp0(xN, v0) = v2) | ~ sdtlseqdt0(v1, v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v2, v3)) % 15.31/4.16 | (111) szDzozmdt0(xC) = szNzAzT0 % 15.31/4.16 | (112) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v4) = v5 & szszuzczcdt0(v0) = v4 & aSubsetOf0(v5, v3) & isCountable0(v5))) % 15.31/4.16 | (113) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (sdtmndt0(v0, v1) = v2) | ~ (sdtpldt0(v2, v1) = v3) | ~ aElementOf0(v1, v0) | ~ aSet0(v0)) % 15.31/4.16 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v1 = slcrc0 | v0 = slcrc0 | ~ (szmzizndt0(v1) = v3) | ~ (szmzizndt0(v0) = v2) | ~ aSubsetOf0(v1, szNzAzT0) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v3, v0) | ~ aElementOf0(v2, v1)) % 15.31/4.16 | (115) aElementOf0(sz00, szNzAzT0) % 15.31/4.16 | (116) ! [v0] : (v0 = sz00 | ~ aElementOf0(v0, szNzAzT0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aElementOf0(v1, szNzAzT0))) % 15.31/4.16 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v2, v3)) % 15.31/4.16 | (118) slbdtsldtrb0(xO, xk) = all_0_9_9 % 15.31/4.16 | (119) ~ (xK = sz00) % 15.31/4.16 | (120) isCountable0(all_0_11_11) % 15.31/4.16 | (121) aSubsetOf0(xS, szNzAzT0) % 15.31/4.16 | (122) ! [v0] : ( ~ isCountable0(v0) | ~ isFinite0(v0) | ~ aSet0(v0)) % 15.31/4.16 | (123) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v2, szNzAzT0)) % 15.31/4.16 | (124) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ isCountable0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isCountable0(v2)) % 15.31/4.16 | (125) aSubsetOf0(xQ, xO) % 15.31/4.16 | (126) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v4) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | aSubsetOf0(v3, v0)) % 15.31/4.16 | (127) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | aFunction0(v3)) % 15.31/4.16 | (128) ! [v0] : ! [v1] : ! [v2] : ( ~ (szDzizrdt0(v0) = v1) | ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | isCountable0(v2) | ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v3) = v4 & szDzozmdt0(v0) = v3 & ( ~ isCountable0(v3) | ~ isFinite0(v4)))) % 15.31/4.16 | (129) slbdtrb0(sz00) = slcrc0 % 15.31/4.16 | (130) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 15.31/4.16 | (131) sdtlcdtrc0(xc, all_0_15_15) = all_0_14_14 % 15.31/4.16 | (132) aSet0(szNzAzT0) % 15.31/4.16 | (133) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aSubsetOf0(v3, v2) | ~ isFinite0(v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | ? [v4] : ? [v5] : (slbdtsldtrb0(v4, v1) = v5 & aSubsetOf0(v4, v0) & aSubsetOf0(v3, v5) & isFinite0(v4))) % 15.31/4.16 | (134) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ (sbrdtbr0(v3) = v4) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0)) % 15.31/4.16 | (135) ! [v0] : ! [v1] : ( ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | aSet0(v1)) % 15.31/4.16 | (136) ~ isCountable0(slcrc0) % 15.31/4.16 | (137) sdtlpdtrp0(xN, sz00) = xS % 15.31/4.16 | (138) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | ? [v2] : (szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ~ aElement0(v3) | sbrdtbr0(v4) = v2 | aElementOf0(v3, v0)))) % 15.31/4.16 | (139) aFunction0(xc) % 15.31/4.16 | (140) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElement0(v3)) % 15.31/4.16 | (141) ! [v0] : (v0 = sz00 | ~ (sbrdtbr0(slcrc0) = v0)) % 15.31/4.16 | (142) szmzizndt0(xQ) = xp % 15.31/4.17 | (143) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ~ aSet0(v2) | ? [v3] : ? [v4] : (szszuzczcdt0(v3) = v4 & ( ~ sdtlseqdt0(v4, v0) | ~ aElementOf0(v3, v2) | ~ aElementOf0(v3, szNzAzT0)) & (aElementOf0(v3, v2) | (sdtlseqdt0(v4, v0) & aElementOf0(v3, szNzAzT0))))) % 15.31/4.17 | (144) aElementOf0(xk, szNzAzT0) % 15.31/4.17 | (145) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ aSet0(v0) | aElement0(v1)) % 15.31/4.17 | (146) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v3, v0)) % 15.31/4.17 | (147) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlpdtrp0(xN, v0) = v2 & slbdtsldtrb0(v6, xk) = v7 & szmzizndt0(v2) = v3 & sdtmndt0(v2, v3) = v4 & aSubsetOf0(v6, v4) & isCountable0(v6) & aElementOf0(v5, xT) & ! [v8] : ! [v9] : (v9 = v5 | ~ (sdtlpdtrp0(v1, v8) = v9) | ~ aElementOf0(v8, v7) | ~ aSet0(v8)))) % 15.31/4.17 | (148) szDzozmdt0(xd) = szNzAzT0 % 15.31/4.17 | (149) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | ~ aElementOf0(v2, v0) | ? [v3] : (aElementOf0(v3, v0) & ~ sdtlseqdt0(v2, v3))) % 15.31/4.17 | (150) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | ~ aElement0(v1) | ? [v3] : (szDzozmdt0(v0) = v3 & aSet0(v2) & ! [v4] : ! [v5] : (v5 = v1 | ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v2)) & ! [v4] : ! [v5] : ( ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v2) | aElementOf0(v4, v3)) & ! [v4] : (v4 = v2 | ~ aSet0(v4) | ? [v5] : ? [v6] : (sdtlpdtrp0(v0, v5) = v6 & ( ~ (v6 = v1) | ~ aElementOf0(v5, v4) | ~ aElementOf0(v5, v3)) & (aElementOf0(v5, v4) | (v6 = v1 & aElementOf0(v5, v3))))) & ! [v4] : ( ~ (sdtlpdtrp0(v0, v4) = v1) | ~ aElementOf0(v4, v3) | aElementOf0(v4, v2)))) % 15.31/4.17 | (151) ! [v0] : ! [v1] : ( ~ (szDzizrdt0(v0) = v1) | ~ aFunction0(v0) | ? [v2] : ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v2) = v3 & sdtlbdtrb0(v0, v1) = v4 & szDzozmdt0(v0) = v2 & ( ~ isCountable0(v2) | ~ isFinite0(v3) | (isCountable0(v4) & aElement0(v1))))) % 15.31/4.17 | (152) aSubsetOf0(all_0_14_14, xT) % 15.31/4.17 | (153) ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | isFinite0(v1)) % 15.31/4.17 | (154) ! [v0] : ! [v1] : ! [v2] : ( ~ (szszuzczcdt0(v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v3] : ? [v4] : (slbdtrb0(v2) = v3 & slbdtrb0(v1) = v4 & (v1 = v0 | ~ aElementOf0(v0, v3) | aElementOf0(v0, v4)) & (aElementOf0(v0, v3) | ( ~ (v1 = v0) & ~ aElementOf0(v0, v4))))) % 15.53/4.17 | (155) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aSubsetOf0(v1, szNzAzT0)) % 15.53/4.17 | (156) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v2, szNzAzT0) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v2)) % 15.53/4.17 | (157) ! [v0] : ! [v1] : ! [v2] : ( ~ (szDzizrdt0(v0) = v1) | ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | aElement0(v1) | ? [v3] : ? [v4] : (sdtlcdtrc0(v0, v3) = v4 & szDzozmdt0(v0) = v3 & ( ~ isCountable0(v3) | ~ isFinite0(v4)))) % 15.53/4.17 | (158) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlpdtrp0(v3, v2) = v1) | ~ (sdtlpdtrp0(v3, v2) = v0)) % 15.53/4.17 | (159) ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | sbrdtbr0(v1) = v0) % 15.53/4.17 | (160) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (sdtlpdtrp0(v0, v5) = v6) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | sdtlpdtrp0(v3, v5) = v6) % 15.53/4.17 | (161) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ aFunction0(v0) | ~ aElement0(v1) | ? [v3] : (szDzozmdt0(v0) = v3 & aSubsetOf0(v2, v3))) % 15.53/4.17 | (162) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlcdtrc0(v3, v2) = v1) | ~ (sdtlcdtrc0(v3, v2) = v0)) % 15.53/4.17 | (163) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aSet0(v2)) % 15.53/4.17 | (164) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 15.53/4.17 | (165) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | aSet0(v3)) % 15.53/4.17 | (166) isCountable0(xS) % 15.53/4.17 | (167) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v1, v2) | ~ aElement0(v1) | ~ aSet0(v0)) % 15.53/4.17 | (168) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ isFinite0(v1) | ~ aElement0(v0) | ~ aSet0(v1) | isFinite0(v2)) % 15.53/4.17 | (169) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : (slbdtsldtrb0(v3, xk) = v4 & szmzizndt0(v1) = v2 & sdtmndt0(v1, v2) = v3 & ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v2) = v6) | ~ aElementOf0(v5, v4) | ~ aSet0(v5) | aElementOf0(v6, all_0_15_15)))) % 15.53/4.17 | (170) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (slbdtsldtrb0(v0, v1) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v3) | ~ aSet0(v0) | ? [v4] : ? [v5] : (sbrdtbr0(v4) = v5 & ( ~ (v5 = v1) | ~ aSubsetOf0(v4, v0) | ~ aElementOf0(v4, v3)) & (aElementOf0(v4, v3) | (v5 = v1 & aSubsetOf0(v4, v0))))) % 15.53/4.17 | (171) aSet0(xT) % 15.53/4.17 | (172) aElementOf0(xQ, all_0_10_10) % 15.53/4.17 | (173) isCountable0(szNzAzT0) % 15.53/4.17 | (174) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v0) = v1) | ~ (szszuzczcdt0(v2) = v3) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v3, v0)) % 15.53/4.17 | (175) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlpdtrp0(xN, v1) = v3) | ~ (sdtlpdtrp0(xN, v0) = v2) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : ( ~ (v5 = v4) & szmzizndt0(v3) = v5 & szmzizndt0(v2) = v4)) % 15.53/4.17 | (176) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtexdt0(v3, v2) = v1) | ~ (sdtexdt0(v3, v2) = v0)) % 15.53/4.17 | (177) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | iLess0(v0, v1)) % 15.53/4.17 | (178) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v4 & sdtlpdtrp0(xN, v1) = v2 & slbdtsldtrb0(v2, xk) = v3 & aElementOf0(v5, xT) & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v4, v6) = v7) | ~ aElementOf0(v6, v3) | ~ aSet0(v6)))) % 15.53/4.18 | (179) ! [v0] : ! [v1] : ( ~ (slbdtrb0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aSet0(v1)) % 15.53/4.18 | (180) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xd, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v5 & sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & ! [v6] : ! [v7] : (v7 = v1 | ~ (sdtlpdtrp0(v5, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) % 15.53/4.18 | (181) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v0) = v3 & szDzozmdt0(v1) = v2 & slbdtsldtrb0(v5, xk) = v2 & szmzizndt0(v3) = v4 & sdtmndt0(v3, v4) = v5 & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v2) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v4) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v4) = v7) | ~ aElementOf0(v6, v2) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v1, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) % 15.53/4.18 | (182) isFinite0(slcrc0) % 15.53/4.18 | (183) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v0)) % 15.53/4.18 | (184) aFunction0(xe) % 15.53/4.18 | (185) aSubsetOf0(xP, all_0_7_7) % 15.53/4.18 | (186) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xC, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xd, v0) = v5 & sdtlpdtrp0(xN, v2) = v3 & slbdtsldtrb0(v3, xk) = v4 & szszuzczcdt0(v0) = v2 & ! [v6] : ! [v7] : (v7 = v5 | ~ (sdtlpdtrp0(v1, v6) = v7) | ~ aElementOf0(v6, v4) | ~ aSet0(v6)))) % 15.53/4.18 | (187) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aElementOf0(v2, v1) | aElement0(v3)) % 15.53/4.18 | (188) aElementOf0(xP, all_0_4_4) % 15.53/4.18 | (189) ! [v0] : ! [v1] : (v0 = slcrc0 | ~ (szmzizndt0(v0) = v1) | ~ aSubsetOf0(v0, szNzAzT0) | aElementOf0(v1, v0)) % 15.53/4.18 | (190) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtexdt0(v0, v2) = v3) | ~ (szDzozmdt0(v4) = v2) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v4) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtlpdtrp0(v4, v5) = v6 & sdtlpdtrp0(v0, v5) = v7 & aElementOf0(v5, v2))) % 15.53/4.18 | (191) ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v0) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aElementOf0(v2, v0)) % 15.53/4.18 | (192) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : (sdtlpdtrp0(xe, v0) = v2 & szmzizndt0(v1) = v2)) % 15.53/4.18 | (193) ! [v0] : ! [v1] : ! [v2] : ( ~ (slbdtsldtrb0(v0, v1) = v2) | ~ isFinite0(v0) | ~ aElementOf0(v1, szNzAzT0) | ~ aSet0(v0) | isFinite0(v2)) % 15.53/4.18 | (194) ! [v0] : ! [v1] : ( ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v1, v0) | ? [v2] : (aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) % 15.53/4.18 | (195) aFunction0(xd) % 15.53/4.18 | (196) sdtmndt0(all_0_6_6, all_0_5_5) = xD % 15.53/4.18 | (197) sdtpldt0(xP, all_0_5_5) = all_0_3_3 % 15.53/4.18 | (198) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | aElementOf0(v1, szNzAzT0)) % 15.53/4.18 | (199) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (slbdtrb0(v1) = v3) | ~ (slbdtrb0(v0) = v2) | ~ aSubsetOf0(v2, v3) | ~ aElementOf0(v1, szNzAzT0) | ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v1)) % 15.53/4.18 | (200) sbrdtbr0(xP) = xk % 15.53/4.18 | (201) sdtlpdtrp0(xN, all_0_8_8) = all_0_7_7 % 15.53/4.18 | (202) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ (szmzizndt0(v1) = v2) | ~ (sdtmndt0(v1, v2) = v3) | ~ aElementOf0(v0, szNzAzT0) | ? [v4] : ? [v5] : (sdtlpdtrp0(xC, v0) = v4 & szDzozmdt0(v4) = v5 & slbdtsldtrb0(v3, xk) = v5 & aFunction0(v4) & ! [v6] : ! [v7] : ( ~ (sdtlpdtrp0(v4, v6) = v7) | ~ aElementOf0(v6, v5) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(xc, v8) = v7 & sdtpldt0(v6, v2) = v8)) & ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v2) = v7) | ~ aElementOf0(v6, v5) | ~ aSet0(v6) | ? [v8] : (sdtlpdtrp0(v4, v6) = v8 & sdtlpdtrp0(xc, v7) = v8)))) % 15.53/4.18 | (203) ! [v0] : ( ~ aElementOf0(v0, szNzAzT0) | sdtlseqdt0(v0, v0)) % 15.53/4.18 | (204) szDzozmdt0(xe) = szNzAzT0 % 15.53/4.18 | (205) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtexdt0(v0, v2) = v3) | ~ (sdtlpdtrp0(v3, v5) = v6) | ~ (szDzozmdt0(v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aElementOf0(v5, v2) | sdtlpdtrp0(v0, v5) = v6) % 15.53/4.18 | (206) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xe, v0) = v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : (sdtlpdtrp0(xN, v0) = v2 & szmzizndt0(v2) = v1)) % 15.53/4.18 | (207) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElement0(v3)) % 15.53/4.18 | (208) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(xN, v0) = v1) | ~ aSubsetOf0(v1, szNzAzT0) | ~ isCountable0(v1) | ~ aElementOf0(v0, szNzAzT0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (sdtlpdtrp0(xN, v2) = v3 & szmzizndt0(v1) = v4 & szszuzczcdt0(v0) = v2 & sdtmndt0(v1, v4) = v5 & aSubsetOf0(v3, v5) & isCountable0(v3))) % 15.53/4.18 | (209) aSubsetOf0(xQ, szNzAzT0) % 15.53/4.18 | (210) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtlcdtrc0(v0, v2) = v3) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aSubsetOf0(v2, v1) | ~ aSet0(v4) | ? [v5] : ? [v6] : ? [v7] : (( ~ aElementOf0(v5, v4) | ! [v8] : ( ~ (sdtlpdtrp0(v0, v8) = v5) | ~ aElementOf0(v8, v2))) & (aElementOf0(v5, v4) | (v7 = v5 & sdtlpdtrp0(v0, v6) = v5 & aElementOf0(v6, v2))))) % 15.53/4.18 | (211) isCountable0(xO) % 15.53/4.18 | (212) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlcdtrc0(v0, v1) = v2) | ~ (sdtlpdtrp0(v0, v3) = v4) | ~ (szDzozmdt0(v0) = v1) | ~ aFunction0(v0) | ~ aElementOf0(v3, v1) | aElementOf0(v4, v2)) % 15.53/4.18 | (213) ! [v0] : ( ~ aSubsetOf0(v0, szNzAzT0) | ~ isFinite0(v0) | ? [v1] : ? [v2] : (slbdtrb0(v1) = v2 & aSubsetOf0(v0, v2) & aElementOf0(v1, szNzAzT0))) % 15.53/4.18 | (214) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aElement0(v1) | ~ aSet0(v0) | aElementOf0(v1, v2)) % 15.53/4.18 | (215) ~ (all_0_0_0 = all_0_2_2) % 15.53/4.18 | (216) szDzizrdt0(xd) = all_0_12_12 % 15.53/4.18 | (217) aSubsetOf0(all_0_13_13, xT) % 15.53/4.18 | % 15.53/4.18 | Instantiating formula (180) with all_0_12_12, xn and discharging atoms sdtlpdtrp0(xd, xn) = all_0_12_12, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (218) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtlpdtrp0(xC, xn) = v3 & sdtlpdtrp0(xN, v0) = v1 & slbdtsldtrb0(v1, xk) = v2 & szszuzczcdt0(xn) = v0 & ! [v4] : ! [v5] : (v5 = all_0_12_12 | ~ (sdtlpdtrp0(v3, v4) = v5) | ~ aElementOf0(v4, v2) | ~ aSet0(v4))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (32) with xD, all_0_5_5, all_0_6_6, xn and discharging atoms sdtlpdtrp0(xN, xn) = all_0_6_6, szmzizndt0(all_0_6_6) = all_0_5_5, sdtmndt0(all_0_6_6, all_0_5_5) = xD, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (219) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtlpdtrp0(xC, xn) = v0 & slbdtsldtrb0(v2, xk) = v3 & aSubsetOf0(v2, xD) & isCountable0(v2) & aElementOf0(v1, xT) & ! [v4] : ! [v5] : (v5 = v1 | ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v3) | ~ aSet0(v4))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (202) with xD, all_0_5_5, all_0_6_6, xn and discharging atoms sdtlpdtrp0(xN, xn) = all_0_6_6, szmzizndt0(all_0_6_6) = all_0_5_5, sdtmndt0(all_0_6_6, all_0_5_5) = xD, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (220) ? [v0] : ? [v1] : (sdtlpdtrp0(xC, xn) = v0 & szDzozmdt0(v0) = v1 & slbdtsldtrb0(xD, xk) = v1 & aFunction0(v0) & ! [v2] : ! [v3] : ( ~ (sdtlpdtrp0(v0, v2) = v3) | ~ aElementOf0(v2, v1) | ~ aSet0(v2) | ? [v4] : (sdtlpdtrp0(xc, v4) = v3 & sdtpldt0(v2, all_0_5_5) = v4)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_5_5) = v3) | ~ aElementOf0(v2, v1) | ~ aSet0(v2) | ? [v4] : (sdtlpdtrp0(v0, v2) = v4 & sdtlpdtrp0(xc, v3) = v4))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (27) with all_0_6_6, xn and discharging atoms sdtlpdtrp0(xN, xn) = all_0_6_6, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (221) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtlpdtrp0(xC, xn) = v0 & szDzozmdt0(v0) = v1 & slbdtsldtrb0(v3, xk) = v1 & szmzizndt0(all_0_6_6) = v2 & sdtmndt0(all_0_6_6, v2) = v3 & aFunction0(v0) & ! [v4] : ! [v5] : ( ~ (sdtlpdtrp0(v0, v4) = v5) | ~ aElementOf0(v4, v1) | ~ aSet0(v4) | ? [v6] : (sdtlpdtrp0(xc, v6) = v5 & sdtpldt0(v4, v2) = v6)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v2) = v5) | ~ aElementOf0(v4, v1) | ~ aSet0(v4) | ? [v6] : (sdtlpdtrp0(v0, v4) = v6 & sdtlpdtrp0(xc, v5) = v6))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (169) with all_0_6_6, xn and discharging atoms sdtlpdtrp0(xN, xn) = all_0_6_6, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (222) ? [v0] : ? [v1] : ? [v2] : (slbdtsldtrb0(v1, xk) = v2 & szmzizndt0(all_0_6_6) = v0 & sdtmndt0(all_0_6_6, v0) = v1 & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v0) = v4) | ~ aElementOf0(v3, v2) | ~ aSet0(v3) | aElementOf0(v4, all_0_15_15))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (192) with all_0_6_6, xn and discharging atoms sdtlpdtrp0(xN, xn) = all_0_6_6, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (223) ? [v0] : (sdtlpdtrp0(xe, xn) = v0 & szmzizndt0(all_0_6_6) = v0) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (12) with all_0_8_8, xn and discharging atoms szszuzczcdt0(xn) = all_0_8_8, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (224) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtlpdtrp0(xd, xn) = v2 & sdtlpdtrp0(xC, xn) = v3 & sdtlpdtrp0(xN, all_0_8_8) = v0 & slbdtsldtrb0(v0, xk) = v1 & ! [v4] : ! [v5] : (v5 = v2 | ~ (sdtlpdtrp0(v3, v4) = v5) | ~ aElementOf0(v4, v1) | ~ aSet0(v4))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (178) with all_0_8_8, xn and discharging atoms szszuzczcdt0(xn) = all_0_8_8, aElementOf0(xn, szNzAzT0), yields: % 15.53/4.19 | (225) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtlpdtrp0(xC, xn) = v2 & sdtlpdtrp0(xN, all_0_8_8) = v0 & slbdtsldtrb0(v0, xk) = v1 & aElementOf0(v3, xT) & ! [v4] : ! [v5] : (v5 = v3 | ~ (sdtlpdtrp0(v2, v4) = v5) | ~ aElementOf0(v4, v1) | ~ aSet0(v4))) % 15.53/4.19 | % 15.53/4.19 | Instantiating formula (68) with xQ, szNzAzT0 and discharging atoms aSubsetOf0(xQ, szNzAzT0), aSet0(szNzAzT0), yields: % 15.53/4.19 | (226) aSet0(xQ) % 15.53/4.19 | % 15.53/4.19 | Instantiating (218) with all_15_0_21, all_15_1_22, all_15_2_23, all_15_3_24 yields: % 15.53/4.19 | (227) sdtlpdtrp0(xC, xn) = all_15_0_21 & sdtlpdtrp0(xN, all_15_3_24) = all_15_2_23 & slbdtsldtrb0(all_15_2_23, xk) = all_15_1_22 & szszuzczcdt0(xn) = all_15_3_24 & ! [v0] : ! [v1] : (v1 = all_0_12_12 | ~ (sdtlpdtrp0(all_15_0_21, v0) = v1) | ~ aElementOf0(v0, all_15_1_22) | ~ aSet0(v0)) % 15.53/4.19 | % 15.53/4.19 | Applying alpha-rule on (227) yields: % 15.53/4.19 | (228) sdtlpdtrp0(xC, xn) = all_15_0_21 % 15.53/4.19 | (229) szszuzczcdt0(xn) = all_15_3_24 % 15.53/4.19 | (230) ! [v0] : ! [v1] : (v1 = all_0_12_12 | ~ (sdtlpdtrp0(all_15_0_21, v0) = v1) | ~ aElementOf0(v0, all_15_1_22) | ~ aSet0(v0)) % 15.53/4.19 | (231) sdtlpdtrp0(xN, all_15_3_24) = all_15_2_23 % 15.53/4.19 | (232) slbdtsldtrb0(all_15_2_23, xk) = all_15_1_22 % 15.53/4.19 | % 15.53/4.19 | Instantiating (225) with all_78_0_76, all_78_1_77, all_78_2_78, all_78_3_79 yields: % 15.53/4.19 | (233) sdtlpdtrp0(xC, xn) = all_78_1_77 & sdtlpdtrp0(xN, all_0_8_8) = all_78_3_79 & slbdtsldtrb0(all_78_3_79, xk) = all_78_2_78 & aElementOf0(all_78_0_76, xT) & ! [v0] : ! [v1] : (v1 = all_78_0_76 | ~ (sdtlpdtrp0(all_78_1_77, v0) = v1) | ~ aElementOf0(v0, all_78_2_78) | ~ aSet0(v0)) % 15.53/4.19 | % 15.53/4.19 | Applying alpha-rule on (233) yields: % 15.53/4.19 | (234) sdtlpdtrp0(xN, all_0_8_8) = all_78_3_79 % 15.53/4.19 | (235) ! [v0] : ! [v1] : (v1 = all_78_0_76 | ~ (sdtlpdtrp0(all_78_1_77, v0) = v1) | ~ aElementOf0(v0, all_78_2_78) | ~ aSet0(v0)) % 15.53/4.19 | (236) slbdtsldtrb0(all_78_3_79, xk) = all_78_2_78 % 15.53/4.19 | (237) sdtlpdtrp0(xC, xn) = all_78_1_77 % 15.53/4.19 | (238) aElementOf0(all_78_0_76, xT) % 15.53/4.19 | % 15.53/4.19 | Instantiating (224) with all_81_0_80, all_81_1_81, all_81_2_82, all_81_3_83 yields: % 15.53/4.19 | (239) sdtlpdtrp0(xd, xn) = all_81_1_81 & sdtlpdtrp0(xC, xn) = all_81_0_80 & sdtlpdtrp0(xN, all_0_8_8) = all_81_3_83 & slbdtsldtrb0(all_81_3_83, xk) = all_81_2_82 & ! [v0] : ! [v1] : (v1 = all_81_1_81 | ~ (sdtlpdtrp0(all_81_0_80, v0) = v1) | ~ aElementOf0(v0, all_81_2_82) | ~ aSet0(v0)) % 15.53/4.19 | % 15.53/4.19 | Applying alpha-rule on (239) yields: % 15.53/4.19 | (240) ! [v0] : ! [v1] : (v1 = all_81_1_81 | ~ (sdtlpdtrp0(all_81_0_80, v0) = v1) | ~ aElementOf0(v0, all_81_2_82) | ~ aSet0(v0)) % 15.53/4.19 | (241) sdtlpdtrp0(xd, xn) = all_81_1_81 % 15.53/4.19 | (242) slbdtsldtrb0(all_81_3_83, xk) = all_81_2_82 % 15.53/4.19 | (243) sdtlpdtrp0(xN, all_0_8_8) = all_81_3_83 % 15.53/4.19 | (244) sdtlpdtrp0(xC, xn) = all_81_0_80 % 15.53/4.19 | % 15.53/4.19 | Instantiating (220) with all_86_0_87, all_86_1_88 yields: % 15.53/4.19 | (245) sdtlpdtrp0(xC, xn) = all_86_1_88 & szDzozmdt0(all_86_1_88) = all_86_0_87 & slbdtsldtrb0(xD, xk) = all_86_0_87 & aFunction0(all_86_1_88) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(all_86_1_88, v0) = v1) | ~ aElementOf0(v0, all_86_0_87) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(xc, v2) = v1 & sdtpldt0(v0, all_0_5_5) = v2)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_5_5) = v1) | ~ aElementOf0(v0, all_86_0_87) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(all_86_1_88, v0) = v2 & sdtlpdtrp0(xc, v1) = v2)) % 15.53/4.19 | % 15.53/4.19 | Applying alpha-rule on (245) yields: % 15.53/4.19 | (246) szDzozmdt0(all_86_1_88) = all_86_0_87 % 15.53/4.19 | (247) slbdtsldtrb0(xD, xk) = all_86_0_87 % 15.53/4.19 | (248) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(all_86_1_88, v0) = v1) | ~ aElementOf0(v0, all_86_0_87) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(xc, v2) = v1 & sdtpldt0(v0, all_0_5_5) = v2)) % 15.53/4.19 | (249) aFunction0(all_86_1_88) % 15.53/4.19 | (250) sdtlpdtrp0(xC, xn) = all_86_1_88 % 15.53/4.19 | (251) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_5_5) = v1) | ~ aElementOf0(v0, all_86_0_87) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(all_86_1_88, v0) = v2 & sdtlpdtrp0(xc, v1) = v2)) % 15.53/4.19 | % 15.53/4.19 | Instantiating (219) with all_89_0_89, all_89_1_90, all_89_2_91, all_89_3_92 yields: % 15.53/4.19 | (252) sdtlpdtrp0(xC, xn) = all_89_3_92 & slbdtsldtrb0(all_89_1_90, xk) = all_89_0_89 & aSubsetOf0(all_89_1_90, xD) & isCountable0(all_89_1_90) & aElementOf0(all_89_2_91, xT) & ! [v0] : ! [v1] : (v1 = all_89_2_91 | ~ (sdtlpdtrp0(all_89_3_92, v0) = v1) | ~ aElementOf0(v0, all_89_0_89) | ~ aSet0(v0)) % 15.53/4.19 | % 15.53/4.19 | Applying alpha-rule on (252) yields: % 15.53/4.19 | (253) slbdtsldtrb0(all_89_1_90, xk) = all_89_0_89 % 15.53/4.19 | (254) aElementOf0(all_89_2_91, xT) % 15.53/4.19 | (255) isCountable0(all_89_1_90) % 15.53/4.19 | (256) sdtlpdtrp0(xC, xn) = all_89_3_92 % 15.53/4.20 | (257) aSubsetOf0(all_89_1_90, xD) % 15.53/4.20 | (258) ! [v0] : ! [v1] : (v1 = all_89_2_91 | ~ (sdtlpdtrp0(all_89_3_92, v0) = v1) | ~ aElementOf0(v0, all_89_0_89) | ~ aSet0(v0)) % 15.53/4.20 | % 15.53/4.20 | Instantiating (222) with all_98_0_99, all_98_1_100, all_98_2_101 yields: % 15.53/4.20 | (259) slbdtsldtrb0(all_98_1_100, xk) = all_98_0_99 & szmzizndt0(all_0_6_6) = all_98_2_101 & sdtmndt0(all_0_6_6, all_98_2_101) = all_98_1_100 & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_98_2_101) = v1) | ~ aElementOf0(v0, all_98_0_99) | ~ aSet0(v0) | aElementOf0(v1, all_0_15_15)) % 15.53/4.20 | % 15.53/4.20 | Applying alpha-rule on (259) yields: % 15.53/4.20 | (260) slbdtsldtrb0(all_98_1_100, xk) = all_98_0_99 % 15.53/4.20 | (261) szmzizndt0(all_0_6_6) = all_98_2_101 % 15.53/4.20 | (262) sdtmndt0(all_0_6_6, all_98_2_101) = all_98_1_100 % 15.53/4.20 | (263) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_98_2_101) = v1) | ~ aElementOf0(v0, all_98_0_99) | ~ aSet0(v0) | aElementOf0(v1, all_0_15_15)) % 15.53/4.20 | % 15.53/4.20 | Instantiating (221) with all_101_0_102, all_101_1_103, all_101_2_104, all_101_3_105 yields: % 15.53/4.20 | (264) sdtlpdtrp0(xC, xn) = all_101_3_105 & szDzozmdt0(all_101_3_105) = all_101_2_104 & slbdtsldtrb0(all_101_0_102, xk) = all_101_2_104 & szmzizndt0(all_0_6_6) = all_101_1_103 & sdtmndt0(all_0_6_6, all_101_1_103) = all_101_0_102 & aFunction0(all_101_3_105) & ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(all_101_3_105, v0) = v1) | ~ aElementOf0(v0, all_101_2_104) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(xc, v2) = v1 & sdtpldt0(v0, all_101_1_103) = v2)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_101_1_103) = v1) | ~ aElementOf0(v0, all_101_2_104) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(all_101_3_105, v0) = v2 & sdtlpdtrp0(xc, v1) = v2)) % 15.53/4.20 | % 15.53/4.20 | Applying alpha-rule on (264) yields: % 15.53/4.20 | (265) szDzozmdt0(all_101_3_105) = all_101_2_104 % 15.53/4.20 | (266) aFunction0(all_101_3_105) % 15.53/4.20 | (267) szmzizndt0(all_0_6_6) = all_101_1_103 % 15.53/4.20 | (268) sdtlpdtrp0(xC, xn) = all_101_3_105 % 15.53/4.20 | (269) ! [v0] : ! [v1] : ( ~ (sdtlpdtrp0(all_101_3_105, v0) = v1) | ~ aElementOf0(v0, all_101_2_104) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(xc, v2) = v1 & sdtpldt0(v0, all_101_1_103) = v2)) % 15.53/4.20 | (270) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_101_1_103) = v1) | ~ aElementOf0(v0, all_101_2_104) | ~ aSet0(v0) | ? [v2] : (sdtlpdtrp0(all_101_3_105, v0) = v2 & sdtlpdtrp0(xc, v1) = v2)) % 15.53/4.20 | (271) slbdtsldtrb0(all_101_0_102, xk) = all_101_2_104 % 15.53/4.20 | (272) sdtmndt0(all_0_6_6, all_101_1_103) = all_101_0_102 % 15.53/4.20 | % 15.53/4.20 | Instantiating (223) with all_104_0_106 yields: % 15.53/4.20 | (273) sdtlpdtrp0(xe, xn) = all_104_0_106 & szmzizndt0(all_0_6_6) = all_104_0_106 % 15.53/4.20 | % 15.53/4.20 | Applying alpha-rule on (273) yields: % 15.53/4.20 | (274) sdtlpdtrp0(xe, xn) = all_104_0_106 % 15.53/4.20 | (275) szmzizndt0(all_0_6_6) = all_104_0_106 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xe, xn, all_104_0_106, xp and discharging atoms sdtlpdtrp0(xe, xn) = all_104_0_106, sdtlpdtrp0(xe, xn) = xp, yields: % 15.53/4.20 | (276) all_104_0_106 = xp % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_101_3_105, all_0_1_1 and discharging atoms sdtlpdtrp0(xC, xn) = all_101_3_105, sdtlpdtrp0(xC, xn) = all_0_1_1, yields: % 15.53/4.20 | (277) all_101_3_105 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_86_1_88, all_89_3_92 and discharging atoms sdtlpdtrp0(xC, xn) = all_89_3_92, sdtlpdtrp0(xC, xn) = all_86_1_88, yields: % 15.53/4.20 | (278) all_89_3_92 = all_86_1_88 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_81_0_80, all_89_3_92 and discharging atoms sdtlpdtrp0(xC, xn) = all_89_3_92, sdtlpdtrp0(xC, xn) = all_81_0_80, yields: % 15.53/4.20 | (279) all_89_3_92 = all_81_0_80 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_78_1_77, all_101_3_105 and discharging atoms sdtlpdtrp0(xC, xn) = all_101_3_105, sdtlpdtrp0(xC, xn) = all_78_1_77, yields: % 15.53/4.20 | (280) all_101_3_105 = all_78_1_77 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_78_1_77, all_86_1_88 and discharging atoms sdtlpdtrp0(xC, xn) = all_86_1_88, sdtlpdtrp0(xC, xn) = all_78_1_77, yields: % 15.53/4.20 | (281) all_86_1_88 = all_78_1_77 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (158) with xC, xn, all_15_0_21, all_86_1_88 and discharging atoms sdtlpdtrp0(xC, xn) = all_86_1_88, sdtlpdtrp0(xC, xn) = all_15_0_21, yields: % 15.53/4.20 | (282) all_86_1_88 = all_15_0_21 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (106) with xD, xk, all_86_0_87, all_0_4_4 and discharging atoms slbdtsldtrb0(xD, xk) = all_86_0_87, slbdtsldtrb0(xD, xk) = all_0_4_4, yields: % 15.53/4.20 | (283) all_86_0_87 = all_0_4_4 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (33) with all_0_6_6, all_101_1_103, all_0_5_5 and discharging atoms szmzizndt0(all_0_6_6) = all_101_1_103, szmzizndt0(all_0_6_6) = all_0_5_5, yields: % 15.53/4.20 | (284) all_101_1_103 = all_0_5_5 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (33) with all_0_6_6, all_98_2_101, all_104_0_106 and discharging atoms szmzizndt0(all_0_6_6) = all_104_0_106, szmzizndt0(all_0_6_6) = all_98_2_101, yields: % 15.53/4.20 | (285) all_104_0_106 = all_98_2_101 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (33) with all_0_6_6, all_98_2_101, all_101_1_103 and discharging atoms szmzizndt0(all_0_6_6) = all_101_1_103, szmzizndt0(all_0_6_6) = all_98_2_101, yields: % 15.53/4.20 | (286) all_101_1_103 = all_98_2_101 % 15.53/4.20 | % 15.53/4.20 | Combining equations (285,276) yields a new equation: % 15.53/4.20 | (287) all_98_2_101 = xp % 15.53/4.20 | % 15.53/4.20 | Simplifying 287 yields: % 15.53/4.20 | (288) all_98_2_101 = xp % 15.53/4.20 | % 15.53/4.20 | Combining equations (286,284) yields a new equation: % 15.53/4.20 | (289) all_98_2_101 = all_0_5_5 % 15.53/4.20 | % 15.53/4.20 | Simplifying 289 yields: % 15.53/4.20 | (290) all_98_2_101 = all_0_5_5 % 15.53/4.20 | % 15.53/4.20 | Combining equations (280,277) yields a new equation: % 15.53/4.20 | (291) all_78_1_77 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Simplifying 291 yields: % 15.53/4.20 | (292) all_78_1_77 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Combining equations (288,290) yields a new equation: % 15.53/4.20 | (293) all_0_5_5 = xp % 15.53/4.20 | % 15.53/4.20 | Combining equations (278,279) yields a new equation: % 15.53/4.20 | (294) all_86_1_88 = all_81_0_80 % 15.53/4.20 | % 15.53/4.20 | Simplifying 294 yields: % 15.53/4.20 | (295) all_86_1_88 = all_81_0_80 % 15.53/4.20 | % 15.53/4.20 | Combining equations (281,295) yields a new equation: % 15.53/4.20 | (296) all_81_0_80 = all_78_1_77 % 15.53/4.20 | % 15.53/4.20 | Combining equations (282,295) yields a new equation: % 15.53/4.20 | (297) all_81_0_80 = all_15_0_21 % 15.53/4.20 | % 15.53/4.20 | Combining equations (296,297) yields a new equation: % 15.53/4.20 | (298) all_78_1_77 = all_15_0_21 % 15.53/4.20 | % 15.53/4.20 | Simplifying 298 yields: % 15.53/4.20 | (299) all_78_1_77 = all_15_0_21 % 15.53/4.20 | % 15.53/4.20 | Combining equations (299,292) yields a new equation: % 15.53/4.20 | (300) all_15_0_21 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Simplifying 300 yields: % 15.53/4.20 | (301) all_15_0_21 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Combining equations (301,297) yields a new equation: % 15.53/4.20 | (302) all_81_0_80 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Combining equations (302,295) yields a new equation: % 15.53/4.20 | (303) all_86_1_88 = all_0_1_1 % 15.53/4.20 | % 15.53/4.20 | Combining equations (293,284) yields a new equation: % 15.53/4.20 | (304) all_101_1_103 = xp % 15.53/4.20 | % 15.53/4.20 | From (277) and (265) follows: % 15.53/4.20 | (305) szDzozmdt0(all_0_1_1) = all_101_2_104 % 15.53/4.20 | % 15.53/4.20 | From (303)(283) and (246) follows: % 15.53/4.20 | (306) szDzozmdt0(all_0_1_1) = all_0_4_4 % 15.53/4.20 | % 15.53/4.20 | From (293) and (197) follows: % 15.53/4.20 | (307) sdtpldt0(xP, xp) = all_0_3_3 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (17) with all_0_1_1, all_0_4_4, all_101_2_104 and discharging atoms szDzozmdt0(all_0_1_1) = all_101_2_104, szDzozmdt0(all_0_1_1) = all_0_4_4, yields: % 15.53/4.20 | (308) all_101_2_104 = all_0_4_4 % 15.53/4.20 | % 15.53/4.20 | Instantiating formula (113) with all_0_3_3, xP, xp, xQ and discharging atoms sdtmndt0(xQ, xp) = xP, sdtpldt0(xP, xp) = all_0_3_3, aElementOf0(xp, xQ), aSet0(xQ), yields: % 15.53/4.20 | (309) all_0_3_3 = xQ % 15.53/4.20 | % 15.53/4.20 | From (309) and (37) follows: % 15.53/4.20 | (310) sdtlpdtrp0(xc, xQ) = all_0_2_2 % 15.53/4.20 | % 15.53/4.20 | From (309) and (307) follows: % 15.53/4.21 | (311) sdtpldt0(xP, xp) = xQ % 15.53/4.21 | % 15.53/4.21 | Instantiating formula (270) with xQ, xP and discharging atoms aSet0(xP), yields: % 15.53/4.21 | (312) ~ (sdtpldt0(xP, all_101_1_103) = xQ) | ~ aElementOf0(xP, all_101_2_104) | ? [v0] : (sdtlpdtrp0(all_101_3_105, xP) = v0 & sdtlpdtrp0(xc, xQ) = v0) % 15.53/4.21 | % 15.53/4.21 +-Applying beta-rule and splitting (312), into two cases. % 15.53/4.21 |-Branch one: % 15.53/4.21 | (313) ~ aElementOf0(xP, all_101_2_104) % 15.53/4.21 | % 15.53/4.21 | From (308) and (313) follows: % 15.53/4.21 | (314) ~ aElementOf0(xP, all_0_4_4) % 15.53/4.21 | % 15.53/4.21 | Using (188) and (314) yields: % 15.53/4.21 | (315) $false % 15.53/4.21 | % 15.53/4.21 |-The branch is then unsatisfiable % 15.53/4.21 |-Branch two: % 15.53/4.21 | (316) aElementOf0(xP, all_101_2_104) % 15.53/4.21 | (317) ~ (sdtpldt0(xP, all_101_1_103) = xQ) | ? [v0] : (sdtlpdtrp0(all_101_3_105, xP) = v0 & sdtlpdtrp0(xc, xQ) = v0) % 15.53/4.21 | % 15.53/4.21 +-Applying beta-rule and splitting (317), into two cases. % 15.53/4.21 |-Branch one: % 15.53/4.21 | (318) ~ (sdtpldt0(xP, all_101_1_103) = xQ) % 15.53/4.21 | % 15.53/4.21 | From (304) and (318) follows: % 15.53/4.21 | (319) ~ (sdtpldt0(xP, xp) = xQ) % 15.53/4.21 | % 15.53/4.21 | Using (311) and (319) yields: % 15.53/4.21 | (315) $false % 15.53/4.21 | % 15.53/4.21 |-The branch is then unsatisfiable % 15.53/4.21 |-Branch two: % 15.53/4.21 | (321) sdtpldt0(xP, all_101_1_103) = xQ % 15.53/4.21 | (322) ? [v0] : (sdtlpdtrp0(all_101_3_105, xP) = v0 & sdtlpdtrp0(xc, xQ) = v0) % 15.53/4.21 | % 15.53/4.21 | Instantiating (322) with all_420_0_336 yields: % 15.53/4.21 | (323) sdtlpdtrp0(all_101_3_105, xP) = all_420_0_336 & sdtlpdtrp0(xc, xQ) = all_420_0_336 % 15.53/4.21 | % 15.53/4.21 | Applying alpha-rule on (323) yields: % 15.53/4.21 | (324) sdtlpdtrp0(all_101_3_105, xP) = all_420_0_336 % 15.53/4.21 | (325) sdtlpdtrp0(xc, xQ) = all_420_0_336 % 15.53/4.21 | % 15.53/4.21 | From (277) and (324) follows: % 15.53/4.21 | (326) sdtlpdtrp0(all_0_1_1, xP) = all_420_0_336 % 15.53/4.21 | % 15.53/4.21 | Instantiating formula (158) with all_0_1_1, xP, all_420_0_336, all_0_0_0 and discharging atoms sdtlpdtrp0(all_0_1_1, xP) = all_420_0_336, sdtlpdtrp0(all_0_1_1, xP) = all_0_0_0, yields: % 15.53/4.21 | (327) all_420_0_336 = all_0_0_0 % 15.53/4.21 | % 15.53/4.21 | Instantiating formula (158) with xc, xQ, all_420_0_336, all_0_2_2 and discharging atoms sdtlpdtrp0(xc, xQ) = all_420_0_336, sdtlpdtrp0(xc, xQ) = all_0_2_2, yields: % 15.53/4.21 | (328) all_420_0_336 = all_0_2_2 % 15.53/4.21 | % 15.53/4.21 | Combining equations (327,328) yields a new equation: % 15.53/4.21 | (329) all_0_0_0 = all_0_2_2 % 15.53/4.21 | % 15.53/4.21 | Simplifying 329 yields: % 15.53/4.21 | (330) all_0_0_0 = all_0_2_2 % 15.53/4.21 | % 15.53/4.21 | Equations (330) can reduce 215 to: % 15.53/4.21 | (331) $false % 15.53/4.21 | % 15.53/4.21 |-The branch is then unsatisfiable % 15.53/4.21 % SZS output end Proof for theBenchmark % 15.53/4.21 % 15.53/4.21 3582ms %------------------------------------------------------------------------------