%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM538+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n016.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:45:37 EDT 2022 % Result : Theorem 21.56s 5.84s % Output : Proof 145.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NUM538+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n016.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 : Thu Jul 7 02:04:06 EDT 2022 % 0.12/0.33 % CPUTime : % 0.48/0.61 ____ _ % 0.48/0.61 ___ / __ \_____(_)___ ________ __________ % 0.48/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.48/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.48/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.48/0.61 % 0.48/0.61 A Theorem Prover for First-Order Logic % 0.48/0.61 (ePrincess v.1.0) % 0.48/0.61 % 0.48/0.61 (c) Philipp Rümmer, 2009-2015 % 0.48/0.61 (c) Peter Backeman, 2014-2015 % 0.48/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.48/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.48/0.61 Bug reports to peter@backeman.se % 0.48/0.61 % 0.48/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.48/0.61 % 0.48/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.67/0.68 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.75/1.04 Prover 0: Preprocessing ... % 3.02/1.38 Prover 0: Constructing countermodel ... % 6.57/2.19 Prover 0: gave up % 6.57/2.19 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 6.57/2.25 Prover 1: Preprocessing ... % 7.45/2.39 Prover 1: Constructing countermodel ... % 19.42/5.36 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 19.59/5.40 Prover 2: Preprocessing ... % 20.09/5.55 Prover 2: Warning: ignoring some quantifiers % 20.37/5.56 Prover 2: Constructing countermodel ... % 21.56/5.84 Prover 2: proved (477ms) % 21.56/5.84 Prover 1: stopped % 21.56/5.84 % 21.56/5.84 No countermodel exists, formula is valid % 21.56/5.84 % SZS status Theorem for theBenchmark % 21.56/5.84 % 21.56/5.84 Generating proof ... Warning: ignoring some quantifiers % 144.83/109.17 found it (size 254) % 144.83/109.17 % 144.83/109.17 % SZS output start Proof for theBenchmark % 144.83/109.17 Assumed formulas after preprocessing and simplification: % 144.83/109.17 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v2) & sbrdtbr0(v0) = v1 & sbrdtbr0(xS) = v3 & szszuzczcdt0(v1) = v2 & sdtmndt0(xS, xx) = v0 & isFinite0(xS) = 0 & isFinite0(slcrc0) = 0 & isCountable0(szNzAzT0) = 0 & aSet0(v0) = 0 & aSet0(xS) = 0 & aSet0(szNzAzT0) = 0 & aElementOf0(xx, xS) = 0 & aElementOf0(sz00, szNzAzT0) = 0 & ~ (aElementOf0(xx, v0) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = v5 | ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v6) = v9) | ? [v10] : (( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v8) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v4) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElement0(v8) = v9) | ? [v10] : (( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v6) = v9) | ? [v10] : (( ~ (v10 = 0) & ~ (v8 = v5) & aElementOf0(v8, v4) = v10) | ( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v8) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = v5 | ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElement0(v8) = v9) | ? [v10] : ((v10 = 0 & aElementOf0(v8, v4) = 0) | ( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElement0(v8) = v9) | ? [v10] : ((v10 = 0 & v9 = 0 & ~ (v8 = v5) & aElementOf0(v8, v4) = 0) | ( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v4) = v9) | ? [v10] : ((v10 = 0 & v9 = 0 & ~ (v8 = v5) & aElement0(v8) = 0) | ( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v4) = v9) | ? [v10] : ((v10 = 0 & aElement0(v8) = 0 & (v9 = 0 | v8 = v5)) | ( ~ (v10 = 0) & aSet0(v4) = v10) | ( ~ (v10 = 0) & aElement0(v5) = v10) | ( ~ (v10 = 0) & aElementOf0(v8, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v5 | ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElement0(v8) = 0) | ? [v9] : ((v9 = 0 & aElementOf0(v8, v6) = 0) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9) | ( ~ (v9 = 0) & aElementOf0(v8, v4) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v5 | ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v4) = 0) | ? [v9] : ((v9 = 0 & aElementOf0(v8, v6) = 0) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v8) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (aSet0(v5) = v6) | ~ (aSet0(v4) = 0) | ~ (aElementOf0(v7, v4) = v8) | ? [v9] : (( ~ (v9 = 0) & aSubsetOf0(v5, v4) = v9) | ( ~ (v9 = 0) & aElementOf0(v7, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtlseqdt0(v6, v7) = v8) | ~ (szszuzczcdt0(v5) = v7) | ~ (szszuzczcdt0(v4) = v6) | ? [v9] : (( ~ (v9 = 0) & aElementOf0(v5, szNzAzT0) = v9) | ( ~ (v9 = 0) & aElementOf0(v4, szNzAzT0) = v9) | (( ~ (v8 = 0) | (v9 = 0 & sdtlseqdt0(v4, v5) = 0)) & (v8 = 0 | ( ~ (v9 = 0) & sdtlseqdt0(v4, v5) = v9))))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v6) = 0) | ? [v9] : ? [v10] : ((v10 = 0 & v9 = 0 & aElement0(v8) = 0 & aElementOf0(v8, v4) = 0) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElement0(v8) = 0) | ? [v9] : ((v9 = 0 & aElementOf0(v8, v6) = 0) | ( ~ (v9 = 0) & ~ (v8 = v5) & aElementOf0(v8, v4) = v9) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v6) = 0) | ? [v9] : ? [v10] : ((v9 = 0 & aElement0(v8) = 0 & (v8 = v5 | (v10 = 0 & aElementOf0(v8, v4) = 0))) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v8, v4) = 0) | ? [v9] : ((v9 = 0 & aElementOf0(v8, v6) = 0) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v8) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v5, v4) = v8) | ? [v9] : ((v9 = 0 & aElementOf0(v5, v6) = 0) | ( ~ (v9 = 0) & aSet0(v4) = v9) | ( ~ (v9 = 0) & aElement0(v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = v6 | ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v7) = 0) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : (( ~ (v8 = 0) & aSet0(v4) = v8) | ( ~ (v8 = 0) & aElement0(v5) = v8) | ((v8 = v5 | ( ~ (v11 = 0) & aElementOf0(v8, v4) = v11) | ( ~ (v10 = 0) & aElement0(v8) = v10) | ( ~ (v9 = 0) & aElementOf0(v8, v7) = v9)) & ((v11 = 0 & v10 = 0 & ~ (v8 = v5) & aElement0(v8) = 0 & aElementOf0(v8, v4) = 0) | (v9 = 0 & aElementOf0(v8, v7) = 0))))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = v6 | ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v7) = 0) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : (( ~ (v8 = 0) & aSet0(v4) = v8) | ( ~ (v8 = 0) & aElement0(v5) = v8) | (((v10 = 0 & aElement0(v8) = 0 & (v8 = v5 | (v11 = 0 & aElementOf0(v8, v4) = 0))) | (v9 = 0 & aElementOf0(v8, v7) = 0)) & (( ~ (v11 = 0) & ~ (v8 = v5) & aElementOf0(v8, v4) = v11) | ( ~ (v10 = 0) & aElement0(v8) = v10) | ( ~ (v9 = 0) & aElementOf0(v8, v7) = v9))))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtlseqdt0(v6, v4) = v7) | ~ (szszuzczcdt0(v5) = v6) | ? [v8] : ((v8 = 0 & sdtlseqdt0(v4, v5) = 0) | ( ~ (v8 = 0) & aElementOf0(v5, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v4, szNzAzT0) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtlseqdt0(v5, v6) = 0) | ~ (sdtlseqdt0(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & sdtlseqdt0(v4, v5) = v8) | ( ~ (v8 = 0) & aElementOf0(v6, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v5, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v4, szNzAzT0) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtlseqdt0(v4, v6) = v7) | ~ (sdtlseqdt0(v4, v5) = 0) | ? [v8] : (( ~ (v8 = 0) & sdtlseqdt0(v5, v6) = v8) | ( ~ (v8 = 0) & aElementOf0(v6, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v5, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v4, szNzAzT0) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtlseqdt0(v4, v6) = v7) | ~ (aElementOf0(v5, szNzAzT0) = 0) | ? [v8] : (( ~ (v8 = 0) & sdtlseqdt0(v5, v6) = v8) | ( ~ (v8 = 0) & sdtlseqdt0(v4, v5) = v8) | ( ~ (v8 = 0) & aElementOf0(v6, szNzAzT0) = v8) | ( ~ (v8 = 0) & aElementOf0(v4, szNzAzT0) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ? [v8] : (( ~ (v8 = 0) & aSet0(v4) = v8) | ( ~ (v8 = 0) & aElement0(v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtpldt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ? [v8] : (( ~ (v8 = 0) & aSet0(v4) = v8) | ( ~ (v8 = 0) & aElement0(v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (aSubsetOf0(v5, v6) = 0) | ~ (aSubsetOf0(v4, v6) = v7) | ? [v8] : (( ~ (v8 = 0) & aSubsetOf0(v4, v5) = v8) | ( ~ (v8 = 0) & aSet0(v6) = v8) | ( ~ (v8 = 0) & aSet0(v5) = v8) | ( ~ (v8 = 0) & aSet0(v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (aSubsetOf0(v5, v4) = 0) | ~ (aSet0(v4) = 0) | ~ (aElementOf0(v6, v4) = v7) | ? [v8] : ( ~ (v8 = 0) & aElementOf0(v6, v5) = v8)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (aSubsetOf0(v4, v6) = v7) | ~ (aSubsetOf0(v4, v5) = 0) | ? [v8] : (( ~ (v8 = 0) & aSubsetOf0(v5, v6) = v8) | ( ~ (v8 = 0) & aSet0(v6) = v8) | ( ~ (v8 = 0) & aSet0(v5) = v8) | ( ~ (v8 = 0) & aSet0(v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (aSubsetOf0(v4, v6) = v7) | ~ (aSet0(v5) = 0) | ? [v8] : (( ~ (v8 = 0) & aSubsetOf0(v5, v6) = v8) | ( ~ (v8 = 0) & aSubsetOf0(v4, v5) = v8) | ( ~ (v8 = 0) & aSet0(v6) = v8) | ( ~ (v8 = 0) & aSet0(v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (iLess0(v7, v6) = v5) | ~ (iLess0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (sdtlseqdt0(v7, v6) = v5) | ~ (sdtlseqdt0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (sdtmndt0(v7, v6) = v5) | ~ (sdtmndt0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (sdtpldt0(v7, v6) = v5) | ~ (sdtpldt0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (aSubsetOf0(v7, v6) = v5) | ~ (aSubsetOf0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (aElementOf0(v7, v6) = v5) | ~ (aElementOf0(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v6) = v7) | ~ (aElementOf0(v5, v6) = 0) | ? [v8] : (( ~ (v8 = 0) & aSet0(v4) = v8) | ( ~ (v8 = 0) & aElement0(v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (aSet0(v5) = v6) | ~ (aSet0(v4) = 0) | ~ (aElementOf0(v7, v5) = 0) | ? [v8] : ((v8 = 0 & aElementOf0(v7, v4) = 0) | ( ~ (v8 = 0) & aSubsetOf0(v5, v4) = v8))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ? [v7] : ? [v8] : ((v8 = 0 & sdtlseqdt0(v7, v4) = 0 & szszuzczcdt0(v5) = v7) | ( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (aSubsetOf0(v5, v4) = v6) | ~ (aSet0(v4) = 0) | ? [v7] : ? [v8] : ? [v9] : ((v8 = 0 & ~ (v9 = 0) & aElementOf0(v7, v5) = 0 & aElementOf0(v7, v4) = v9) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (isFinite0(v5) = v6) | ~ (isFinite0(v4) = 0) | ? [v7] : (( ~ (v7 = 0) & aSubsetOf0(v5, v4) = v7) | ( ~ (v7 = 0) & aSet0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (isFinite0(v5) = v6) | ~ (aSet0(v4) = 0) | ? [v7] : (( ~ (v7 = 0) & aSubsetOf0(v5, v4) = v7) | ( ~ (v7 = 0) & isFinite0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (aSet0(v5) = v6) | ~ (aSet0(v4) = 0) | ? [v7] : ( ~ (v7 = 0) & aSubsetOf0(v5, v4) = v7)) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (aSet0(v4) = 0) | ~ (aElement0(v5) = v6) | ? [v7] : ( ~ (v7 = 0) & aElementOf0(v5, v4) = v7)) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (aElementOf0(v4, v5) = v6) | ? [v7] : ? [v8] : ((v8 = v5 & sdtmndt0(v7, v4) = v5 & sdtpldt0(v5, v4) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7) | ( ~ (v7 = 0) & aElement0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (sbrdtbr0(v6) = v5) | ~ (sbrdtbr0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (szszuzczcdt0(v6) = v5) | ~ (szszuzczcdt0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (szszuzczcdt0(v5) = v6) | ~ (szszuzczcdt0(v4) = v6) | ? [v7] : (( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (szszuzczcdt0(v5) = v6) | ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v7] : (( ~ (v7 = v6) & szszuzczcdt0(v4) = v7) | ( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (szszuzczcdt0(v4) = v6) | ~ (aElementOf0(v5, szNzAzT0) = 0) | ? [v7] : (( ~ (v7 = v6) & szszuzczcdt0(v5) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (isFinite0(v6) = v5) | ~ (isFinite0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (isCountable0(v6) = v5) | ~ (isCountable0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (aSet0(v6) = v5) | ~ (aSet0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (aElement0(v6) = v5) | ~ (aElement0(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlseqdt0(v5, v6) = 0) | ~ (sdtlseqdt0(v4, v5) = 0) | ? [v7] : ((v7 = 0 & sdtlseqdt0(v4, v6) = 0) | ( ~ (v7 = 0) & aElementOf0(v6, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlseqdt0(v5, v6) = 0) | ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v7] : ((v7 = 0 & sdtlseqdt0(v4, v6) = 0) | ( ~ (v7 = 0) & sdtlseqdt0(v4, v5) = v7) | ( ~ (v7 = 0) & aElementOf0(v6, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlseqdt0(v4, v5) = v6) | ? [v7] : ? [v8] : ? [v9] : (( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7) | (( ~ (v6 = 0) | (v9 = 0 & sdtlseqdt0(v7, v8) = 0 & szszuzczcdt0(v5) = v8 & szszuzczcdt0(v4) = v7)) & (v6 = 0 | ( ~ (v9 = 0) & sdtlseqdt0(v7, v8) = v9 & szszuzczcdt0(v5) = v8 & szszuzczcdt0(v4) = v7))))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtlseqdt0(v4, v5) = 0) | ~ (aElementOf0(v6, szNzAzT0) = 0) | ? [v7] : ((v7 = 0 & sdtlseqdt0(v4, v6) = 0) | ( ~ (v7 = 0) & sdtlseqdt0(v5, v6) = v7) | ( ~ (v7 = 0) & aElementOf0(v5, szNzAzT0) = v7) | ( ~ (v7 = 0) & aElementOf0(v4, szNzAzT0) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtmndt0(v5, v4) = v6) | ~ (aElement0(v4) = 0) | ? [v7] : ((v7 = 0 & isFinite0(v6) = 0) | ( ~ (v7 = 0) & isFinite0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtmndt0(v5, v4) = v6) | ~ (aElement0(v4) = 0) | ? [v7] : ((v7 = 0 & isCountable0(v6) = 0) | ( ~ (v7 = 0) & isCountable0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtmndt0(v4, v5) = v6) | ~ (aSet0(v4) = 0) | ? [v7] : ((v7 = v4 & sdtpldt0(v6, v5) = v4) | ( ~ (v7 = 0) & aElementOf0(v5, v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v4) = v6) | ~ (aElement0(v4) = 0) | ? [v7] : ((v7 = 0 & isFinite0(v6) = 0) | ( ~ (v7 = 0) & isFinite0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v4) = v6) | ~ (aElement0(v4) = 0) | ? [v7] : ((v7 = 0 & isCountable0(v6) = 0) | ( ~ (v7 = 0) & isCountable0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtpldt0(v5, v4) = v6) | ? [v7] : ((v7 = v5 & sdtmndt0(v6, v4) = v5) | (v7 = 0 & aElementOf0(v4, v5) = 0) | ( ~ (v7 = 0) & aSet0(v5) = v7) | ( ~ (v7 = 0) & aElement0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aSubsetOf0(v5, v6) = 0) | ~ (aSubsetOf0(v4, v5) = 0) | ? [v7] : ((v7 = 0 & aSubsetOf0(v4, v6) = 0) | ( ~ (v7 = 0) & aSet0(v6) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aSubsetOf0(v5, v6) = 0) | ~ (aSet0(v4) = 0) | ? [v7] : ((v7 = 0 & aSubsetOf0(v4, v6) = 0) | ( ~ (v7 = 0) & aSubsetOf0(v4, v5) = v7) | ( ~ (v7 = 0) & aSet0(v6) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aSubsetOf0(v5, v4) = 0) | ~ (aSet0(v4) = 0) | ~ (aElementOf0(v6, v5) = 0) | aElementOf0(v6, v4) = 0) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aSubsetOf0(v4, v5) = 0) | ~ (aSet0(v6) = 0) | ? [v7] : ((v7 = 0 & aSubsetOf0(v4, v6) = 0) | ( ~ (v7 = 0) & aSubsetOf0(v5, v6) = v7) | ( ~ (v7 = 0) & aSet0(v5) = v7) | ( ~ (v7 = 0) & aSet0(v4) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aSet0(v6) = 0) | ~ (aSet0(v5) = 0) | ~ (aSet0(v4) = 0) | ? [v7] : ((v7 = 0 & aSubsetOf0(v4, v6) = 0) | ( ~ (v7 = 0) & aSubsetOf0(v5, v6) = v7) | ( ~ (v7 = 0) & aSubsetOf0(v4, v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (aElementOf0(v6, szNzAzT0) = 0) | ~ (aElementOf0(v5, szNzAzT0) = 0) | ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v7] : ((v7 = 0 & sdtlseqdt0(v4, v6) = 0) | ( ~ (v7 = 0) & sdtlseqdt0(v5, v6) = v7) | ( ~ (v7 = 0) & sdtlseqdt0(v4, v5) = v7))) & ! [v4] : ! [v5] : (v5 = v4 | ~ (sdtlseqdt0(v5, v4) = 0) | ? [v6] : (( ~ (v6 = 0) & sdtlseqdt0(v4, v5) = v6) | ( ~ (v6 = 0) & aElementOf0(v5, szNzAzT0) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : (v5 = v4 | ~ (sdtlseqdt0(v4, v5) = 0) | ? [v6] : (( ~ (v6 = 0) & sdtlseqdt0(v5, v4) = v6) | ( ~ (v6 = 0) & aElementOf0(v5, szNzAzT0) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : (v5 = v4 | ~ (aSubsetOf0(v5, v4) = 0) | ? [v6] : (( ~ (v6 = 0) & aSubsetOf0(v4, v5) = v6) | ( ~ (v6 = 0) & aSet0(v5) = v6) | ( ~ (v6 = 0) & aSet0(v4) = v6))) & ! [v4] : ! [v5] : (v5 = v4 | ~ (aSubsetOf0(v4, v5) = 0) | ? [v6] : (( ~ (v6 = 0) & aSubsetOf0(v5, v4) = v6) | ( ~ (v6 = 0) & aSet0(v5) = v6) | ( ~ (v6 = 0) & aSet0(v4) = v6))) & ! [v4] : ! [v5] : (v5 = v4 | ~ (aElementOf0(v5, szNzAzT0) = 0) | ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & szszuzczcdt0(v5) = v7 & szszuzczcdt0(v4) = v6)) & ! [v4] : ! [v5] : (v5 = 0 | v4 = xx | ~ (aElementOf0(v4, v0) = v5) | ? [v6] : (( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, xS) = v6))) & ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtlseqdt0(v4, v4) = v5) | ? [v6] : ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6)) & ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtlseqdt0(sz00, v4) = v5) | ? [v6] : ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6)) & ! [v4] : ! [v5] : (v5 = 0 | ~ (aSubsetOf0(v4, v4) = v5) | ? [v6] : ( ~ (v6 = 0) & aSet0(v4) = v6)) & ! [v4] : ! [v5] : ( ~ (sbrdtbr0(v4) = v5) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & aSet0(v4) = v6) | (((v7 = 0 & isFinite0(v4) = 0) | ( ~ (v6 = 0) & aElementOf0(v5, szNzAzT0) = v6)) & ((v6 = 0 & aElementOf0(v5, szNzAzT0) = 0) | ( ~ (v7 = 0) & isFinite0(v4) = v7))))) & ! [v4] : ! [v5] : ( ~ (sbrdtbr0(v4) = v5) | ? [v6] : ((v6 = 0 & aElement0(v5) = 0) | ( ~ (v6 = 0) & aSet0(v4) = v6))) & ! [v4] : ! [v5] : ( ~ (sbrdtbr0(v4) = v5) | ? [v6] : (( ~ (v6 = 0) & isFinite0(v4) = v6) | ( ~ (v6 = 0) & aSet0(v4) = v6) | (szszuzczcdt0(v5) = v6 & ! [v7] : ! [v8] : (v8 = 0 | ~ (aElementOf0(v7, v4) = v8) | ? [v9] : ? [v10] : ((v10 = v6 & sbrdtbr0(v9) = v6 & sdtpldt0(v4, v7) = v9) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v7) = v8) | ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6) | (v9 = 0 & aElementOf0(v7, v4) = 0) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ( ~ (aElement0(v7) = 0) | ? [v8] : ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6 & sdtpldt0(v4, v7) = v8) | (v8 = 0 & aElementOf0(v7, v4) = 0)))))) & ! [v4] : ! [v5] : ( ~ (szszuzczcdt0(v4) = v5) | ? [v6] : ((v6 = 0 & ~ (v5 = sz00) & aElementOf0(v5, szNzAzT0) = 0) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : ( ~ (szszuzczcdt0(v4) = v5) | ? [v6] : ((v6 = 0 & iLess0(v4, v5) = 0) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : ( ~ (szszuzczcdt0(v4) = v5) | ? [v6] : ((v6 = 0 & sdtlseqdt0(v4, v5) = 0) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : ( ~ (szszuzczcdt0(v4) = v5) | ? [v6] : (( ~ (v6 = 0) & sdtlseqdt0(v5, sz00) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, szNzAzT0) = v6))) & ! [v4] : ! [v5] : ( ~ (aSubsetOf0(v5, v4) = 0) | ~ (isFinite0(v4) = 0) | ? [v6] : ((v6 = 0 & isFinite0(v5) = 0) | ( ~ (v6 = 0) & aSet0(v4) = v6))) & ! [v4] : ! [v5] : ( ~ (aSubsetOf0(v5, v4) = 0) | ~ (aSet0(v4) = 0) | aSet0(v5) = 0) & ! [v4] : ! [v5] : ( ~ (aSubsetOf0(v5, v4) = 0) | ~ (aSet0(v4) = 0) | ? [v6] : ((v6 = 0 & isFinite0(v5) = 0) | ( ~ (v6 = 0) & isFinite0(v4) = v6))) & ! [v4] : ! [v5] : ( ~ (isFinite0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtmndt0(v5, v4) = v6 & isFinite0(v6) = 0) | ( ~ (v6 = 0) & aSet0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (isFinite0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtpldt0(v5, v4) = v6 & isFinite0(v6) = 0) | ( ~ (v6 = 0) & aSet0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (isFinite0(v4) = v5) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & aSet0(v4) = v6) | (( ~ (v5 = 0) | (v7 = 0 & sbrdtbr0(v4) = v6 & aElementOf0(v6, szNzAzT0) = 0)) & (v5 = 0 | ( ~ (v7 = 0) & sbrdtbr0(v4) = v6 & aElementOf0(v6, szNzAzT0) = v7))))) & ! [v4] : ! [v5] : ( ~ (isCountable0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtmndt0(v5, v4) = v6 & isCountable0(v6) = 0) | ( ~ (v6 = 0) & aSet0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (isCountable0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtpldt0(v5, v4) = v6 & isCountable0(v6) = 0) | ( ~ (v6 = 0) & aSet0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (aSet0(v5) = 0) | ~ (aSet0(v4) = 0) | ? [v6] : ? [v7] : ? [v8] : ((v7 = 0 & ~ (v8 = 0) & aElementOf0(v6, v5) = 0 & aElementOf0(v6, v4) = v8) | (v6 = 0 & aSubsetOf0(v5, v4) = 0))) & ! [v4] : ! [v5] : ( ~ (aSet0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtmndt0(v5, v4) = v6 & isFinite0(v6) = 0) | ( ~ (v6 = 0) & isFinite0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (aSet0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtmndt0(v5, v4) = v6 & isCountable0(v6) = 0) | ( ~ (v6 = 0) & isCountable0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (aSet0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtpldt0(v5, v4) = v6 & isFinite0(v6) = 0) | ( ~ (v6 = 0) & isFinite0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (aSet0(v5) = 0) | ~ (aElement0(v4) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & sdtpldt0(v5, v4) = v6 & isCountable0(v6) = 0) | ( ~ (v6 = 0) & isCountable0(v5) = v6))) & ! [v4] : ! [v5] : ( ~ (aSet0(v4) = 0) | ~ (aElementOf0(v5, v4) = 0) | aElement0(v5) = 0) & ! [v4] : ! [v5] : ( ~ (aSet0(v4) = 0) | ~ (aElementOf0(v5, v4) = 0) | ? [v6] : (sdtmndt0(v4, v5) = v6 & sdtpldt0(v6, v5) = v4)) & ! [v4] : ! [v5] : ( ~ (aSet0(slcrc0) = v4) | ~ (aElementOf0(v5, slcrc0) = 0)) & ! [v4] : ! [v5] : ( ~ (aElement0(v4) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = xx) & aElementOf0(v4, xS) = 0) | ( ~ (v6 = 0) & aElementOf0(v4, v0) = v6))) & ! [v4] : ! [v5] : ( ~ (aElementOf0(v4, xS) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = xx) & aElement0(v4) = 0) | ( ~ (v6 = 0) & aElementOf0(v4, v0) = v6))) & ! [v4] : (v4 = xx | ~ (aElement0(v4) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v5 = 0) & aElementOf0(v4, xS) = v5))) & ! [v4] : (v4 = xx | ~ (aElementOf0(v4, xS) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v5 = 0) & aElement0(v4) = v5))) & ! [v4] : (v4 = sz00 | ~ (sbrdtbr0(slcrc0) = v4) | ? [v5] : ( ~ (v5 = 0) & aSet0(slcrc0) = v5)) & ! [v4] : (v4 = sz00 | ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : (szszuzczcdt0(v5) = v4 & aElementOf0(v5, szNzAzT0) = 0)) & ! [v4] : (v4 = slcrc0 | ~ (sbrdtbr0(v4) = sz00) | ? [v5] : ( ~ (v5 = 0) & aSet0(v4) = v5)) & ! [v4] : (v4 = slcrc0 | ~ (aSet0(v4) = 0) | ? [v5] : aElementOf0(v5, v4) = 0) & ! [v4] : (v4 = 0 | ~ (aSet0(slcrc0) = v4)) & ! [v4] : ( ~ (szszuzczcdt0(v4) = v4) | ? [v5] : ( ~ (v5 = 0) & aElementOf0(v4, szNzAzT0) = v5)) & ! [v4] : ( ~ (isFinite0(v4) = 0) | ? [v5] : ? [v6] : (( ~ (v5 = 0) & aSet0(v4) = v5) | (sbrdtbr0(v4) = v5 & szszuzczcdt0(v5) = v6 & ! [v7] : ! [v8] : (v8 = 0 | ~ (aElementOf0(v7, v4) = v8) | ? [v9] : ? [v10] : ((v10 = v6 & sbrdtbr0(v9) = v6 & sdtpldt0(v4, v7) = v9) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v7) = v8) | ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6) | (v9 = 0 & aElementOf0(v7, v4) = 0) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ( ~ (aElement0(v7) = 0) | ? [v8] : ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6 & sdtpldt0(v4, v7) = v8) | (v8 = 0 & aElementOf0(v7, v4) = 0)))))) & ! [v4] : ( ~ (isFinite0(v4) = 0) | ? [v5] : (( ~ (v5 = 0) & isCountable0(v4) = v5) | ( ~ (v5 = 0) & aSet0(v4) = v5))) & ! [v4] : ( ~ (isCountable0(v4) = 0) | ? [v5] : (( ~ (v5 = 0) & isFinite0(v4) = v5) | ( ~ (v5 = 0) & aSet0(v4) = v5))) & ! [v4] : ( ~ (aSet0(v4) = 0) | aSubsetOf0(v4, v4) = 0) & ! [v4] : ( ~ (aSet0(v4) = 0) | ? [v5] : ? [v6] : ? [v7] : (((v7 = 0 & isFinite0(v4) = 0) | ( ~ (v6 = 0) & sbrdtbr0(v4) = v5 & aElementOf0(v5, szNzAzT0) = v6)) & ((v6 = 0 & sbrdtbr0(v4) = v5 & aElementOf0(v5, szNzAzT0) = 0) | ( ~ (v7 = 0) & isFinite0(v4) = v7)))) & ! [v4] : ( ~ (aSet0(v4) = 0) | ? [v5] : ? [v6] : (( ~ (v5 = 0) & isFinite0(v4) = v5) | (sbrdtbr0(v4) = v5 & szszuzczcdt0(v5) = v6 & ! [v7] : ! [v8] : (v8 = 0 | ~ (aElementOf0(v7, v4) = v8) | ? [v9] : ? [v10] : ((v10 = v6 & sbrdtbr0(v9) = v6 & sdtpldt0(v4, v7) = v9) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ! [v8] : ( ~ (sdtpldt0(v4, v7) = v8) | ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6) | (v9 = 0 & aElementOf0(v7, v4) = 0) | ( ~ (v9 = 0) & aElement0(v7) = v9))) & ! [v7] : ( ~ (aElement0(v7) = 0) | ? [v8] : ? [v9] : ((v9 = v6 & sbrdtbr0(v8) = v6 & sdtpldt0(v4, v7) = v8) | (v8 = 0 & aElementOf0(v7, v4) = 0)))))) & ! [v4] : ( ~ (aSet0(v4) = 0) | ? [v5] : (sbrdtbr0(v4) = v5 & aElement0(v5) = 0)) & ! [v4] : ( ~ (aSet0(v4) = 0) | ? [v5] : (( ~ (v4 = slcrc0) | (v5 = sz00 & sbrdtbr0(slcrc0) = sz00)) & (v4 = slcrc0 | ( ~ (v5 = sz00) & sbrdtbr0(v4) = v5)))) & ! [v4] : ( ~ (aSet0(v4) = 0) | ? [v5] : (( ~ (v5 = 0) & isFinite0(v4) = v5) | ( ~ (v5 = 0) & isCountable0(v4) = v5))) & ! [v4] : ( ~ (aElementOf0(v4, v0) = 0) | (aElement0(v4) = 0 & aElementOf0(v4, xS) = 0)) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | sdtlseqdt0(v4, v4) = 0) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | sdtlseqdt0(sz00, v4) = 0) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : ? [v6] : ( ~ (v6 = 0) & sdtlseqdt0(v5, sz00) = v6 & szszuzczcdt0(v4) = v5)) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : ( ~ (v5 = v4) & szszuzczcdt0(v4) = v5)) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : ( ~ (v5 = sz00) & szszuzczcdt0(v4) = v5 & aElementOf0(v5, szNzAzT0) = 0)) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : (iLess0(v4, v5) = 0 & szszuzczcdt0(v4) = v5)) & ! [v4] : ( ~ (aElementOf0(v4, szNzAzT0) = 0) | ? [v5] : (sdtlseqdt0(v4, v5) = 0 & szszuzczcdt0(v4) = v5)) & ? [v4] : ? [v5] : ? [v6] : iLess0(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : sdtlseqdt0(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : sdtmndt0(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : sdtpldt0(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : aSubsetOf0(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : aElementOf0(v5, v4) = v6 & ? [v4] : ? [v5] : sbrdtbr0(v4) = v5 & ? [v4] : ? [v5] : szszuzczcdt0(v4) = v5 & ? [v4] : ? [v5] : isFinite0(v4) = v5 & ? [v4] : ? [v5] : isCountable0(v4) = v5 & ? [v4] : ? [v5] : aSet0(v4) = v5 & ? [v4] : ? [v5] : aElement0(v4) = v5 & ( ~ (isCountable0(slcrc0) = 0) | ? [v4] : ( ~ (v4 = 0) & aSet0(slcrc0) = v4)) & ( ~ (aSet0(slcrc0) = 0) | ? [v4] : ( ~ (v4 = 0) & isCountable0(slcrc0) = v4))) % 145.02/109.26 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 145.02/109.26 | (1) ~ (all_0_0_0 = all_0_1_1) & sbrdtbr0(all_0_3_3) = all_0_2_2 & sbrdtbr0(xS) = all_0_0_0 & szszuzczcdt0(all_0_2_2) = all_0_1_1 & sdtmndt0(xS, xx) = all_0_3_3 & isFinite0(xS) = 0 & isFinite0(slcrc0) = 0 & isCountable0(szNzAzT0) = 0 & aSet0(all_0_3_3) = 0 & aSet0(xS) = 0 & aSet0(szNzAzT0) = 0 & aElementOf0(xx, xS) = 0 & aElementOf0(sz00, szNzAzT0) = 0 & ~ (aElementOf0(xx, all_0_3_3) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = v5) | ? [v6] : (( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v0) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : (( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = v5) | ? [v6] : (( ~ (v6 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v6) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v1 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : ((v6 = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = v1) & aElementOf0(v4, v0) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = v1) & aElement0(v4) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = v5) | ? [v6] : ((v6 = 0 & aElement0(v4) = 0 & (v5 = 0 | v4 = v1)) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5) | ( ~ (v5 = 0) & aElementOf0(v4, v0) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v4) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : (( ~ (v5 = 0) & aSubsetOf0(v1, v0) = v5) | ( ~ (v5 = 0) & aElementOf0(v3, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlseqdt0(v2, v3) = v4) | ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ? [v5] : (( ~ (v5 = 0) & aElementOf0(v1, szNzAzT0) = v5) | ( ~ (v5 = 0) & aElementOf0(v0, szNzAzT0) = v5) | (( ~ (v4 = 0) | (v5 = 0 & sdtlseqdt0(v0, v1) = 0)) & (v4 = 0 | ( ~ (v5 = 0) & sdtlseqdt0(v0, v1) = v5))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = 0) | ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & aElement0(v4) = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v5) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = 0) | ? [v5] : ? [v6] : ((v5 = 0 & aElement0(v4) = 0 & (v4 = v1 | (v6 = 0 & aElementOf0(v4, v0) = 0))) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v4) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v1, v0) = v4) | ? [v5] : ((v5 = 0 & aElementOf0(v1, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v3) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4) | ((v4 = v1 | ( ~ (v7 = 0) & aElementOf0(v4, v0) = v7) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v5 = 0) & aElementOf0(v4, v3) = v5)) & ((v7 = 0 & v6 = 0 & ~ (v4 = v1) & aElement0(v4) = 0 & aElementOf0(v4, v0) = 0) | (v5 = 0 & aElementOf0(v4, v3) = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v3) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4) | (((v6 = 0 & aElement0(v4) = 0 & (v4 = v1 | (v7 = 0 & aElementOf0(v4, v0) = 0))) | (v5 = 0 & aElementOf0(v4, v3) = 0)) & (( ~ (v7 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v7) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v5 = 0) & aElementOf0(v4, v3) = v5))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v2, v0) = v3) | ~ (szszuzczcdt0(v1) = v2) | ? [v4] : ((v4 = 0 & sdtlseqdt0(v0, v1) = 0) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v0, v1) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v1, v2) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v1, v2) = v4) | ( ~ (v4 = 0) & sdtlseqdt0(v0, v1) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSubsetOf0(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v0, v1) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v1) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v2, v0) = v3) | ? [v4] : ( ~ (v4 = 0) & aElementOf0(v2, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v0, v2) = v3) | ~ (aSubsetOf0(v0, v1) = 0) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v1, v2) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v1) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v0, v2) = v3) | ~ (aSet0(v1) = 0) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v1, v2) = v4) | ( ~ (v4 = 0) & aSubsetOf0(v0, v1) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(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] : (v1 = v0 | ~ (aSubsetOf0(v3, v2) = v1) | ~ (aSubsetOf0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v1, v2) = 0) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v3, v1) = 0) | ? [v4] : ((v4 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v4 = 0) & aSubsetOf0(v1, v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & sdtlseqdt0(v3, v0) = 0 & szszuzczcdt0(v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSubsetOf0(v1, v0) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & ~ (v5 = 0) & aElementOf0(v3, v1) = 0 & aElementOf0(v3, v0) = v5) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (isFinite0(v1) = v2) | ~ (isFinite0(v0) = 0) | ? [v3] : (( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (isFinite0(v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : (( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3) | ( ~ (v3 = 0) & isFinite0(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSet0(v0) = 0) | ~ (aElement0(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & aElementOf0(v1, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aElementOf0(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = v1 & sdtmndt0(v3, v0) = v1 & sdtpldt0(v1, v0) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aElement0(v0) = v3))) & ! [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) | ? [v3] : (( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : (( ~ (v3 = v2) & szszuzczcdt0(v0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v0) = v2) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ? [v3] : (( ~ (v3 = v2) & szszuzczcdt0(v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isFinite0(v2) = v1) | ~ (isFinite0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isCountable0(v2) = v1) | ~ (isCountable0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ (aSet0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & aElementOf0(v2, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v0, v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v2, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3) | (( ~ (v2 = 0) | (v5 = 0 & sdtlseqdt0(v3, v4) = 0 & szszuzczcdt0(v1) = v4 & szszuzczcdt0(v0) = v3)) & (v2 = 0 | ( ~ (v5 = 0) & sdtlseqdt0(v3, v4) = v5 & szszuzczcdt0(v1) = v4 & szszuzczcdt0(v0) = v3))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ~ (aElementOf0(v2, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v1, v2) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isFinite0(v2) = 0) | ( ~ (v3 = 0) & isFinite0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isCountable0(v2) = 0) | ( ~ (v3 = 0) & isCountable0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = v0 & sdtpldt0(v2, v1) = v0) | ( ~ (v3 = 0) & aElementOf0(v1, v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isFinite0(v2) = 0) | ( ~ (v3 = 0) & isFinite0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isCountable0(v2) = 0) | ( ~ (v3 = 0) & isCountable0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ? [v3] : ((v3 = v1 & sdtmndt0(v2, v0) = v1) | (v3 = 0 & aElementOf0(v0, v1) = 0) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aElement0(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSubsetOf0(v0, v1) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSet0(v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v0, v1) = v3) | ( ~ (v3 = 0) & aSet0(v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v2, v1) = 0) | aElementOf0(v2, v0) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v0, v1) = 0) | ~ (aSet0(v2) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v1, v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aSet0(v2) = 0) | ~ (aSet0(v1) = 0) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v1, v2) = v3) | ( ~ (v3 = 0) & aSubsetOf0(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (aElementOf0(v2, szNzAzT0) = 0) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v1, v2) = v3) | ( ~ (v3 = 0) & sdtlseqdt0(v0, v1) = v3))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v0, v1) = v2) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v1, v0) = v2) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (aSubsetOf0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & aSubsetOf0(v0, v1) = v2) | ( ~ (v2 = 0) & aSet0(v1) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (aSubsetOf0(v0, v1) = 0) | ? [v2] : (( ~ (v2 = 0) & aSubsetOf0(v1, v0) = v2) | ( ~ (v2 = 0) & aSet0(v1) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (aElementOf0(v1, szNzAzT0) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = v2) & szszuzczcdt0(v1) = v3 & szszuzczcdt0(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | v0 = xx | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : (( ~ (v2 = 0) & aElement0(v0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, xS) = v2))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(sz00, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (aSubsetOf0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aSet0(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & aSet0(v0) = v2) | (((v3 = 0 & isFinite0(v0) = 0) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2)) & ((v2 = 0 & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v3 = 0) & isFinite0(v0) = v3))))) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : ((v2 = 0 & aElement0(v1) = 0) | ( ~ (v2 = 0) & aSet0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & isFinite0(v0) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2) | (szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & ~ (v1 = sz00) & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & iLess0(v0, v1) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & sdtlseqdt0(v0, v1) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v1, sz00) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) & ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (isFinite0(v0) = 0) | ? [v2] : ((v2 = 0 & isFinite0(v1) = 0) | ( ~ (v2 = 0) & aSet0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | aSet0(v1) = 0) & ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ? [v2] : ((v2 = 0 & isFinite0(v1) = 0) | ( ~ (v2 = 0) & isFinite0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (isFinite0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (isFinite0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (isFinite0(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & aSet0(v0) = v2) | (( ~ (v1 = 0) | (v3 = 0 & sbrdtbr0(v0) = v2 & aElementOf0(v2, szNzAzT0) = 0)) & (v1 = 0 | ( ~ (v3 = 0) & sbrdtbr0(v0) = v2 & aElementOf0(v2, szNzAzT0) = v3))))) & ! [v0] : ! [v1] : ( ~ (isCountable0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (isCountable0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aSet0(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & aElementOf0(v2, v1) = 0 & aElementOf0(v2, v0) = v4) | (v2 = 0 & aSubsetOf0(v1, v0) = 0))) & ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & isFinite0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & isCountable0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & isFinite0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & isCountable0(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (aSet0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | aElement0(v1) = 0) & ! [v0] : ! [v1] : ( ~ (aSet0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ? [v2] : (sdtmndt0(v0, v1) = v2 & sdtpldt0(v2, v1) = v0)) & ! [v0] : ! [v1] : ( ~ (aSet0(slcrc0) = v0) | ~ (aElementOf0(v1, slcrc0) = 0)) & ! [v0] : ! [v1] : ( ~ (aElement0(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & ~ (v0 = xx) & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, all_0_3_3) = v2))) & ! [v0] : ! [v1] : ( ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & ~ (v0 = xx) & aElement0(v0) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, all_0_3_3) = v2))) & ! [v0] : (v0 = xx | ~ (aElement0(v0) = 0) | ? [v1] : ((v1 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v1 = 0) & aElementOf0(v0, xS) = v1))) & ! [v0] : (v0 = xx | ~ (aElementOf0(v0, xS) = 0) | ? [v1] : ((v1 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v1 = 0) & aElement0(v0) = v1))) & ! [v0] : (v0 = sz00 | ~ (sbrdtbr0(slcrc0) = v0) | ? [v1] : ( ~ (v1 = 0) & aSet0(slcrc0) = v1)) & ! [v0] : (v0 = sz00 | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aElementOf0(v1, szNzAzT0) = 0)) & ! [v0] : (v0 = slcrc0 | ~ (sbrdtbr0(v0) = sz00) | ? [v1] : ( ~ (v1 = 0) & aSet0(v0) = v1)) & ! [v0] : (v0 = slcrc0 | ~ (aSet0(v0) = 0) | ? [v1] : aElementOf0(v1, v0) = 0) & ! [v0] : (v0 = 0 | ~ (aSet0(slcrc0) = v0)) & ! [v0] : ( ~ (szszuzczcdt0(v0) = v0) | ? [v1] : ( ~ (v1 = 0) & aElementOf0(v0, szNzAzT0) = v1)) & ! [v0] : ( ~ (isFinite0(v0) = 0) | ? [v1] : ? [v2] : (( ~ (v1 = 0) & aSet0(v0) = v1) | (sbrdtbr0(v0) = v1 & szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) & ! [v0] : ( ~ (isFinite0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isCountable0(v0) = v1) | ( ~ (v1 = 0) & aSet0(v0) = v1))) & ! [v0] : ( ~ (isCountable0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | ( ~ (v1 = 0) & aSet0(v0) = v1))) & ! [v0] : ( ~ (aSet0(v0) = 0) | aSubsetOf0(v0, v0) = 0) & ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (((v3 = 0 & isFinite0(v0) = 0) | ( ~ (v2 = 0) & sbrdtbr0(v0) = v1 & aElementOf0(v1, szNzAzT0) = v2)) & ((v2 = 0 & sbrdtbr0(v0) = v1 & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v3 = 0) & isFinite0(v0) = v3)))) & ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : ? [v2] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | (sbrdtbr0(v0) = v1 & szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) & ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (sbrdtbr0(v0) = v1 & aElement0(v1) = 0)) & ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (( ~ (v0 = slcrc0) | (v1 = sz00 & sbrdtbr0(slcrc0) = sz00)) & (v0 = slcrc0 | ( ~ (v1 = sz00) & sbrdtbr0(v0) = v1)))) & ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | ( ~ (v1 = 0) & isCountable0(v0) = v1))) & ! [v0] : ( ~ (aElementOf0(v0, all_0_3_3) = 0) | (aElement0(v0) = 0 & aElementOf0(v0, xS) = 0)) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | sdtlseqdt0(v0, v0) = 0) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | sdtlseqdt0(sz00, v0) = 0) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & sdtlseqdt0(v1, sz00) = v2 & szszuzczcdt0(v0) = v1)) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ( ~ (v1 = v0) & szszuzczcdt0(v0) = v1)) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ( ~ (v1 = sz00) & szszuzczcdt0(v0) = v1 & aElementOf0(v1, szNzAzT0) = 0)) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (iLess0(v0, v1) = 0 & szszuzczcdt0(v0) = v1)) & ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (sdtlseqdt0(v0, v1) = 0 & szszuzczcdt0(v0) = v1)) & ? [v0] : ? [v1] : ? [v2] : iLess0(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : sdtlseqdt0(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : sdtmndt0(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : sdtpldt0(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : aSubsetOf0(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : aElementOf0(v1, v0) = v2 & ? [v0] : ? [v1] : sbrdtbr0(v0) = v1 & ? [v0] : ? [v1] : szszuzczcdt0(v0) = v1 & ? [v0] : ? [v1] : isFinite0(v0) = v1 & ? [v0] : ? [v1] : isCountable0(v0) = v1 & ? [v0] : ? [v1] : aSet0(v0) = v1 & ? [v0] : ? [v1] : aElement0(v0) = v1 & ( ~ (isCountable0(slcrc0) = 0) | ? [v0] : ( ~ (v0 = 0) & aSet0(slcrc0) = v0)) & ( ~ (aSet0(slcrc0) = 0) | ? [v0] : ( ~ (v0 = 0) & isCountable0(slcrc0) = v0)) % 145.34/109.31 | % 145.34/109.31 | Applying alpha-rule on (1) yields: % 145.34/109.31 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5) | ( ~ (v5 = 0) & aElementOf0(v4, v0) = v5))) % 145.34/109.31 | (3) ! [v0] : ! [v1] : (v1 = v0 | ~ (aSubsetOf0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & aSubsetOf0(v0, v1) = v2) | ( ~ (v2 = 0) & aSet0(v1) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2))) % 145.34/109.31 | (4) ! [v0] : ! [v1] : ( ~ (aSet0(slcrc0) = v0) | ~ (aElementOf0(v1, slcrc0) = 0)) % 145.34/109.31 | (5) sdtmndt0(xS, xx) = all_0_3_3 % 145.34/109.31 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSubsetOf0(v0, v1) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSet0(v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) % 145.34/109.31 | (7) ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ? [v2] : ((v2 = 0 & isFinite0(v1) = 0) | ( ~ (v2 = 0) & isFinite0(v0) = v2))) % 145.34/109.31 | (8) ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (isFinite0(v0) = 0) | ? [v2] : ((v2 = 0 & isFinite0(v1) = 0) | ( ~ (v2 = 0) & aSet0(v0) = v2))) % 145.34/109.31 | (9) ? [v0] : ? [v1] : isCountable0(v0) = v1 % 145.34/109.31 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v1, v2) = 0) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) % 145.34/109.31 | (11) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | sdtlseqdt0(v0, v0) = 0) % 145.34/109.31 | (12) ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & isFinite0(v1) = v2))) % 145.34/109.31 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) % 145.34/109.31 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v4) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.31 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 145.34/109.32 | (16) aElementOf0(sz00, szNzAzT0) = 0 % 145.34/109.32 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v3) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4) | (((v6 = 0 & aElement0(v4) = 0 & (v4 = v1 | (v7 = 0 & aElementOf0(v4, v0) = 0))) | (v5 = 0 & aElementOf0(v4, v3) = 0)) & (( ~ (v7 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v7) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v5 = 0) & aElementOf0(v4, v3) = v5))))) % 145.34/109.32 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isCountable0(v2) = 0) | ( ~ (v3 = 0) & isCountable0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.32 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v0, v2) = v3) | ~ (aSubsetOf0(v0, v1) = 0) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v1, v2) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v1) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) % 145.34/109.32 | (20) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ? [v3] : ((v3 = v1 & sdtmndt0(v2, v0) = v1) | (v3 = 0 & aElementOf0(v0, v1) = 0) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aElement0(v0) = v3))) % 145.34/109.32 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v1, v0) = v4) | ? [v5] : ((v5 = 0 & aElementOf0(v1, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.32 | (22) ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (( ~ (v0 = slcrc0) | (v1 = sz00 & sbrdtbr0(slcrc0) = sz00)) & (v0 = slcrc0 | ( ~ (v1 = sz00) & sbrdtbr0(v0) = v1)))) % 145.34/109.32 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) % 145.34/109.32 | (24) aSet0(szNzAzT0) = 0 % 145.34/109.32 | (25) ? [v0] : ? [v1] : ? [v2] : aElementOf0(v1, v0) = v2 % 145.34/109.32 | (26) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & sdtlseqdt0(v0, v1) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.32 | (27) ! [v0] : ( ~ (isFinite0(v0) = 0) | ? [v1] : ? [v2] : (( ~ (v1 = 0) & aSet0(v0) = v1) | (sbrdtbr0(v0) = v1 & szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) % 145.34/109.32 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (aSubsetOf0(v3, v2) = v1) | ~ (aSubsetOf0(v3, v2) = v0)) % 145.34/109.32 | (29) ? [v0] : ? [v1] : szszuzczcdt0(v0) = v1 % 145.34/109.32 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) % 145.34/109.32 | (31) ! [v0] : ! [v1] : ( ~ (isFinite0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) % 145.34/109.32 | (32) ? [v0] : ? [v1] : aElement0(v0) = v1 % 145.34/109.32 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : (( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) % 145.34/109.32 | (34) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | sdtlseqdt0(sz00, v0) = 0) % 145.34/109.32 | (35) ! [v0] : ! [v1] : ( ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & ~ (v0 = xx) & aElement0(v0) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, all_0_3_3) = v2))) % 145.34/109.32 | (36) ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aSet0(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & aElementOf0(v2, v1) = 0 & aElementOf0(v2, v0) = v4) | (v2 = 0 & aSubsetOf0(v1, v0) = 0))) % 145.34/109.32 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v2, v0) = v3) | ~ (szszuzczcdt0(v1) = v2) | ? [v4] : ((v4 = 0 & sdtlseqdt0(v0, v1) = 0) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) % 145.34/109.32 | (38) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & sdtlseqdt0(v1, sz00) = v2 & szszuzczcdt0(v0) = v1)) % 145.34/109.32 | (39) ! [v0] : (v0 = slcrc0 | ~ (sbrdtbr0(v0) = sz00) | ? [v1] : ( ~ (v1 = 0) & aSet0(v0) = v1)) % 145.34/109.32 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v2, v0) = v3) | ? [v4] : ( ~ (v4 = 0) & aElementOf0(v2, v1) = v4)) % 145.34/109.33 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v1 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : ((v6 = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) % 145.34/109.33 | (42) ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2)) % 145.34/109.33 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isFinite0(v2) = 0) | ( ~ (v3 = 0) & isFinite0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.33 | (44) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aElementOf0(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = v1 & sdtmndt0(v3, v0) = v1 & sdtpldt0(v1, v0) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aElement0(v0) = v3))) % 145.34/109.33 | (45) ! [v0] : ! [v1] : ( ~ (isFinite0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) % 145.34/109.33 | (46) ! [v0] : (v0 = xx | ~ (aElementOf0(v0, xS) = 0) | ? [v1] : ((v1 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v1 = 0) & aElement0(v0) = v1))) % 145.34/109.33 | (47) isFinite0(slcrc0) = 0 % 145.34/109.33 | (48) ! [v0] : ! [v1] : ( ~ (aSet0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | aElement0(v1) = 0) % 145.34/109.33 | (49) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) % 145.34/109.33 | (50) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 145.34/109.33 | (51) ! [v0] : ! [v1] : ( ~ (aElement0(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & ~ (v0 = xx) & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, all_0_3_3) = v2))) % 145.34/109.33 | (52) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : ((v2 = 0 & aElement0(v1) = 0) | ( ~ (v2 = 0) & aSet0(v0) = v2))) % 145.34/109.33 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = v1) & aElementOf0(v4, v0) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) % 145.34/109.33 | (54) ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v2, v1) = 0) | aElementOf0(v2, v0) = 0) % 145.34/109.33 | (55) ! [v0] : (v0 = sz00 | ~ (sbrdtbr0(slcrc0) = v0) | ? [v1] : ( ~ (v1 = 0) & aSet0(slcrc0) = v1)) % 145.34/109.33 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v1, v2) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) % 145.34/109.33 | (57) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v0) = v2) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ? [v3] : (( ~ (v3 = v2) & szszuzczcdt0(v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) % 145.34/109.33 | (58) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ( ~ (v1 = v0) & szszuzczcdt0(v0) = v1)) % 145.34/109.33 | (59) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isFinite0(v2) = v1) | ~ (isFinite0(v2) = v0)) % 145.34/109.33 | (60) ! [v0] : (v0 = 0 | ~ (aSet0(slcrc0) = v0)) % 145.34/109.33 | (61) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & aElementOf0(v2, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) % 145.34/109.33 | (62) ! [v0] : ! [v1] : (v1 = 0 | ~ (aSubsetOf0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aSet0(v0) = v2)) % 145.34/109.33 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v0, v1) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v1, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) % 145.34/109.34 | (64) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3) | (( ~ (v2 = 0) | (v5 = 0 & sdtlseqdt0(v3, v4) = 0 & szszuzczcdt0(v1) = v4 & szszuzczcdt0(v0) = v3)) & (v2 = 0 | ( ~ (v5 = 0) & sdtlseqdt0(v3, v4) = v5 & szszuzczcdt0(v1) = v4 & szszuzczcdt0(v0) = v3))))) % 145.34/109.34 | (65) ! [v0] : ( ~ (szszuzczcdt0(v0) = v0) | ? [v1] : ( ~ (v1 = 0) & aElementOf0(v0, szNzAzT0) = v1)) % 145.34/109.34 | (66) ? [v0] : ? [v1] : sbrdtbr0(v0) = v1 % 145.34/109.34 | (67) sbrdtbr0(all_0_3_3) = all_0_2_2 % 145.34/109.34 | (68) szszuzczcdt0(all_0_2_2) = all_0_1_1 % 145.34/109.34 | (69) ~ (all_0_0_0 = all_0_1_1) % 145.34/109.34 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v3, v1) = 0) | ? [v4] : ((v4 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v4 = 0) & aSubsetOf0(v1, v0) = v4))) % 145.34/109.34 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElement0(v4) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v5) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.34 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v1 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = v5) | ? [v6] : (( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v0) = v6))) % 145.34/109.34 | (73) ! [v0] : ! [v1] : ( ~ (isCountable0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) % 145.34/109.34 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isCountable0(v2) = 0) | ( ~ (v3 = 0) & isCountable0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.34 | (75) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = v0 & sdtpldt0(v2, v1) = v0) | ( ~ (v3 = 0) & aElementOf0(v1, v0) = v3))) % 145.34/109.34 | (76) ? [v0] : ? [v1] : ? [v2] : sdtmndt0(v1, v0) = v2 % 145.34/109.34 | (77) ! [v0] : ( ~ (isFinite0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isCountable0(v0) = v1) | ( ~ (v1 = 0) & aSet0(v0) = v1))) % 145.34/109.34 | (78) ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isFinite0(v2) = 0) | ( ~ (v2 = 0) & isFinite0(v1) = v2))) % 145.34/109.34 | (79) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ~ (aElementOf0(v2, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v1, v2) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) % 145.34/109.34 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v0, v2) = v3) | ~ (aSet0(v1) = 0) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v1, v2) = v4) | ( ~ (v4 = 0) & aSubsetOf0(v0, v1) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) % 145.34/109.34 | (81) ! [v0] : (v0 = slcrc0 | ~ (aSet0(v0) = 0) | ? [v1] : aElementOf0(v1, v0) = 0) % 145.34/109.34 | (82) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v1, v0) = v2) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.34 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : (( ~ (v5 = 0) & aSubsetOf0(v1, v0) = v5) | ( ~ (v5 = 0) & aElementOf0(v3, v1) = v5))) % 145.34/109.34 | (84) sbrdtbr0(xS) = all_0_0_0 % 145.34/109.34 | (85) ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (sbrdtbr0(v0) = v1 & aElement0(v1) = 0)) % 145.34/109.34 | (86) ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (((v3 = 0 & isFinite0(v0) = 0) | ( ~ (v2 = 0) & sbrdtbr0(v0) = v1 & aElementOf0(v1, szNzAzT0) = v2)) & ((v2 = 0 & sbrdtbr0(v0) = v1 & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v3 = 0) & isFinite0(v0) = v3)))) % 145.34/109.34 | (87) aSet0(xS) = 0 % 145.34/109.34 | (88) ! [v0] : ! [v1] : ( ~ (isCountable0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & aSet0(v1) = v2))) % 145.34/109.34 | (89) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v0, v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v2, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3))) % 145.34/109.34 | (90) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & isFinite0(v0) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2) | (szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) % 145.34/109.34 | (91) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & iLess0(v0, v1) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.34 | (92) ! [v0] : ! [v1] : (v1 = v0 | ~ (aElementOf0(v1, szNzAzT0) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = v2) & szszuzczcdt0(v1) = v3 & szszuzczcdt0(v0) = v2)) % 145.34/109.34 | (93) ! [v0] : ! [v1] : ( ~ (sbrdtbr0(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & aSet0(v0) = v2) | (((v3 = 0 & isFinite0(v0) = 0) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2)) & ((v2 = 0 & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v3 = 0) & isFinite0(v0) = v3))))) % 145.34/109.34 | (94) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v1, sz00) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.34 | (95) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) % 145.34/109.34 | (96) ? [v0] : ? [v1] : isFinite0(v0) = v1 % 145.34/109.35 | (97) ! [v0] : ! [v1] : ( ~ (szszuzczcdt0(v0) = v1) | ? [v2] : ((v2 = 0 & ~ (v1 = sz00) & aElementOf0(v1, szNzAzT0) = 0) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.35 | (98) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSet0(v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3)) % 145.34/109.35 | (99) ? [v0] : ? [v1] : aSet0(v0) = v1 % 145.34/109.35 | (100) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtlseqdt0(v2, v3) = v4) | ~ (szszuzczcdt0(v1) = v3) | ~ (szszuzczcdt0(v0) = v2) | ? [v5] : (( ~ (v5 = 0) & aElementOf0(v1, szNzAzT0) = v5) | ( ~ (v5 = 0) & aElementOf0(v0, szNzAzT0) = v5) | (( ~ (v4 = 0) | (v5 = 0 & sdtlseqdt0(v0, v1) = 0)) & (v4 = 0 | ( ~ (v5 = 0) & sdtlseqdt0(v0, v1) = v5))))) % 145.34/109.35 | (101) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) % 145.34/109.35 | (102) ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : ? [v2] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | (sbrdtbr0(v0) = v1 & szszuzczcdt0(v1) = v2 & ! [v3] : ! [v4] : (v4 = 0 | ~ (aElementOf0(v3, v0) = v4) | ? [v5] : ? [v6] : ((v6 = v2 & sbrdtbr0(v5) = v2 & sdtpldt0(v0, v3) = v5) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v3) = v4) | ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2) | (v5 = 0 & aElementOf0(v3, v0) = 0) | ( ~ (v5 = 0) & aElement0(v3) = v5))) & ! [v3] : ( ~ (aElement0(v3) = 0) | ? [v4] : ? [v5] : ((v5 = v2 & sbrdtbr0(v4) = v2 & sdtpldt0(v0, v3) = v4) | (v4 = 0 & aElementOf0(v3, v0) = 0)))))) % 145.34/109.35 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = 0) | ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & aElement0(v4) = 0 & aElementOf0(v4, v0) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.35 | (104) ! [v0] : ! [v1] : (v1 = 0 | v0 = xx | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : (( ~ (v2 = 0) & aElement0(v0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, xS) = v2))) % 145.34/109.35 | (105) ? [v0] : ? [v1] : ? [v2] : sdtlseqdt0(v1, v0) = v2 % 145.34/109.35 | (106) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : ( ~ (v1 = sz00) & szszuzczcdt0(v0) = v1 & aElementOf0(v1, szNzAzT0) = 0)) % 145.34/109.35 | (107) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4))) % 145.34/109.35 | (108) ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtmndt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & isCountable0(v1) = v2))) % 145.34/109.35 | (109) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ? [v4] : (( ~ (v4 = 0) & sdtlseqdt0(v1, v2) = v4) | ( ~ (v4 = 0) & sdtlseqdt0(v0, v1) = v4) | ( ~ (v4 = 0) & aElementOf0(v2, szNzAzT0) = v4) | ( ~ (v4 = 0) & aElementOf0(v0, szNzAzT0) = v4))) % 145.34/109.35 | (110) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSet0(v0) = 0) | ~ (aElement0(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & aElementOf0(v1, v0) = v3)) % 145.34/109.35 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = 0) | ? [v5] : ? [v6] : ((v5 = 0 & aElement0(v4) = 0 & (v4 = v1 | (v6 = 0 & aElementOf0(v4, v0) = 0))) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.35 | (112) ! [v0] : (v0 = xx | ~ (aElement0(v0) = 0) | ? [v1] : ((v1 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v1 = 0) & aElementOf0(v0, xS) = v1))) % 145.34/109.35 | (113) ? [v0] : ? [v1] : ? [v2] : iLess0(v1, v0) = v2 % 145.34/109.35 | (114) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (iLess0(v0, v1) = 0 & szszuzczcdt0(v0) = v1)) % 145.34/109.35 | (115) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ? [v3] : ((v3 = 0 & isFinite0(v2) = 0) | ( ~ (v3 = 0) & isFinite0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.35 | (116) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & sdtlseqdt0(v0, v1) = v2) | ( ~ (v2 = 0) & aElementOf0(v1, szNzAzT0) = v2) | ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2))) % 145.34/109.35 | (117) ! [v0] : ! [v1] : ( ~ (aSet0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ? [v2] : (sdtmndt0(v0, v1) = v2 & sdtpldt0(v2, v1) = v0)) % 145.34/109.35 | (118) ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(sz00, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aElementOf0(v0, szNzAzT0) = v2)) % 145.34/109.35 | (119) ~ (aSet0(slcrc0) = 0) | ? [v0] : ( ~ (v0 = 0) & isCountable0(slcrc0) = v0) % 145.34/109.35 | (120) ~ (isCountable0(slcrc0) = 0) | ? [v0] : ( ~ (v0 = 0) & aSet0(slcrc0) = v0) % 145.34/109.35 | (121) ? [v0] : ? [v1] : ? [v2] : sdtpldt0(v1, v0) = v2 % 145.34/109.35 | (122) ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v0, v1) = v3) | ( ~ (v3 = 0) & aSet0(v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.35 | (123) ? [v0] : ? [v1] : ? [v2] : aSubsetOf0(v1, v0) = v2 % 145.34/109.35 | (124) isFinite0(xS) = 0 % 145.34/109.35 | (125) aSet0(all_0_3_3) = 0 % 145.34/109.35 | (126) isCountable0(szNzAzT0) = 0 % 145.34/109.35 | (127) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (isFinite0(v1) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : (( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3) | ( ~ (v3 = 0) & isFinite0(v0) = v3))) % 145.34/109.35 | (128) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (isFinite0(v1) = v2) | ~ (isFinite0(v0) = 0) | ? [v3] : (( ~ (v3 = 0) & aSubsetOf0(v1, v0) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) % 145.34/109.35 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v3) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (( ~ (v4 = 0) & aSet0(v0) = v4) | ( ~ (v4 = 0) & aElement0(v1) = v4) | ((v4 = v1 | ( ~ (v7 = 0) & aElementOf0(v4, v0) = v7) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v5 = 0) & aElementOf0(v4, v3) = v5)) & ((v7 = 0 & v6 = 0 & ~ (v4 = v1) & aElement0(v4) = 0 & aElementOf0(v4, v0) = 0) | (v5 = 0 & aElementOf0(v4, v3) = 0))))) % 145.34/109.35 | (130) ! [v0] : ! [v1] : ( ~ (isFinite0(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & aSet0(v0) = v2) | (( ~ (v1 = 0) | (v3 = 0 & sbrdtbr0(v0) = v2 & aElementOf0(v2, szNzAzT0) = 0)) & (v1 = 0 | ( ~ (v3 = 0) & sbrdtbr0(v0) = v2 & aElementOf0(v2, szNzAzT0) = v3))))) % 145.34/109.35 | (131) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (szszuzczcdt0(v0) = v2) | ? [v3] : (( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) % 145.34/109.35 | (132) ! [v0] : (v0 = sz00 | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (szszuzczcdt0(v1) = v0 & aElementOf0(v1, szNzAzT0) = 0)) % 145.34/109.35 | (133) ! [v0] : ! [v1] : ( ~ (aSet0(v1) = 0) | ~ (aElement0(v0) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & sdtpldt0(v1, v0) = v2 & isCountable0(v2) = 0) | ( ~ (v2 = 0) & isCountable0(v1) = v2))) % 145.34/109.35 | (134) ! [v0] : ( ~ (aSet0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | ( ~ (v1 = 0) & isCountable0(v0) = v1))) % 145.34/109.35 | (135) ! [v0] : ( ~ (isCountable0(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & isFinite0(v0) = v1) | ( ~ (v1 = 0) & aSet0(v0) = v1))) % 145.34/109.36 | (136) ! [v0] : ! [v1] : ( ~ (aSubsetOf0(v1, v0) = 0) | ~ (aSet0(v0) = 0) | aSet0(v1) = 0) % 145.34/109.36 | (137) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (szszuzczcdt0(v1) = v2) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : (( ~ (v3 = v2) & szszuzczcdt0(v0) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3))) % 145.34/109.36 | (138) ! [v0] : ! [v1] : ! [v2] : ( ~ (aSubsetOf0(v0, v1) = 0) | ~ (aSet0(v2) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v1, v2) = v3) | ( ~ (v3 = 0) & aSet0(v1) = v3) | ( ~ (v3 = 0) & aSet0(v0) = v3))) % 145.34/109.36 | (139) ~ (aElementOf0(xx, all_0_3_3) = 0) % 145.34/109.36 | (140) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = 0) | ? [v5] : ((v5 = 0 & aElementOf0(v4, v2) = 0) | ( ~ (v5 = 0) & aSet0(v0) = v5) | ( ~ (v5 = 0) & aElement0(v4) = v5) | ( ~ (v5 = 0) & aElement0(v1) = v5))) % 145.34/109.36 | (141) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & sdtlseqdt0(v3, v0) = 0 & szszuzczcdt0(v1) = v3) | ( ~ (v3 = 0) & aElementOf0(v1, szNzAzT0) = v3) | ( ~ (v3 = 0) & aElementOf0(v0, szNzAzT0) = v3))) % 145.34/109.36 | (142) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (aSubsetOf0(v1, v2) = 0) | ~ (aSubsetOf0(v0, v2) = v3) | ? [v4] : (( ~ (v4 = 0) & aSubsetOf0(v0, v1) = v4) | ( ~ (v4 = 0) & aSet0(v2) = v4) | ( ~ (v4 = 0) & aSet0(v1) = v4) | ( ~ (v4 = 0) & aSet0(v0) = v4))) % 145.34/109.36 | (143) ! [v0] : ( ~ (aElementOf0(v0, all_0_3_3) = 0) | (aElement0(v0) = 0 & aElementOf0(v0, xS) = 0)) % 145.34/109.36 | (144) ! [v0] : ! [v1] : ! [v2] : ( ~ (aSet0(v2) = 0) | ~ (aSet0(v1) = 0) | ~ (aSet0(v0) = 0) | ? [v3] : ((v3 = 0 & aSubsetOf0(v0, v2) = 0) | ( ~ (v3 = 0) & aSubsetOf0(v1, v2) = v3) | ( ~ (v3 = 0) & aSubsetOf0(v0, v1) = v3))) % 145.34/109.36 | (145) aElementOf0(xx, xS) = 0 % 145.34/109.36 | (146) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v2) = v5) | ? [v6] : (( ~ (v6 = 0) & ~ (v4 = v1) & aElementOf0(v4, v0) = v6) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v4) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6))) % 145.34/109.36 | (147) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isCountable0(v2) = v1) | ~ (isCountable0(v2) = v0)) % 145.34/109.36 | (148) ! [v0] : ! [v1] : ! [v2] : ( ~ (aElementOf0(v2, szNzAzT0) = 0) | ~ (aElementOf0(v1, szNzAzT0) = 0) | ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v3] : ((v3 = 0 & sdtlseqdt0(v0, v2) = 0) | ( ~ (v3 = 0) & sdtlseqdt0(v1, v2) = v3) | ( ~ (v3 = 0) & sdtlseqdt0(v0, v1) = v3))) % 145.34/109.36 | (149) ! [v0] : ( ~ (aElementOf0(v0, szNzAzT0) = 0) | ? [v1] : (sdtlseqdt0(v0, v1) = 0 & szszuzczcdt0(v0) = v1)) % 145.34/109.36 | (150) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 145.34/109.36 | (151) ! [v0] : ! [v1] : (v1 = v0 | ~ (aSubsetOf0(v0, v1) = 0) | ? [v2] : (( ~ (v2 = 0) & aSubsetOf0(v1, v0) = v2) | ( ~ (v2 = 0) & aSet0(v1) = v2) | ( ~ (v2 = 0) & aSet0(v0) = v2))) % 145.34/109.36 | (152) ! [v0] : ( ~ (aSet0(v0) = 0) | aSubsetOf0(v0, v0) = 0) % 145.34/109.36 | (153) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = v5) | ? [v6] : ((v6 = 0 & aElement0(v4) = 0 & (v5 = 0 | v4 = v1)) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) % 145.34/109.36 | (154) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ (aSet0(v2) = v0)) % 145.34/109.36 | (155) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtmndt0(v0, v1) = v2) | ~ (aSet0(v2) = v3) | ~ (aElementOf0(v4, v0) = v5) | ? [v6] : ((v6 = 0 & v5 = 0 & ~ (v4 = v1) & aElement0(v4) = 0) | ( ~ (v6 = 0) & aSet0(v0) = v6) | ( ~ (v6 = 0) & aElement0(v1) = v6) | ( ~ (v6 = 0) & aElementOf0(v4, v2) = v6))) % 145.34/109.36 | (156) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (aSubsetOf0(v1, v0) = v2) | ~ (aSet0(v0) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & ~ (v5 = 0) & aElementOf0(v3, v1) = 0 & aElementOf0(v3, v0) = v5) | ( ~ (v3 = 0) & aSet0(v1) = v3))) % 145.34/109.36 | % 145.34/109.36 | Instantiating formula (93) with all_0_2_2, all_0_3_3 and discharging atoms sbrdtbr0(all_0_3_3) = all_0_2_2, yields: % 145.34/109.36 | (157) ? [v0] : ? [v1] : (( ~ (v0 = 0) & aSet0(all_0_3_3) = v0) | (((v1 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (v0 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = v0)) & ((v0 = 0 & aElementOf0(all_0_2_2, szNzAzT0) = 0) | ( ~ (v1 = 0) & isFinite0(all_0_3_3) = v1)))) % 145.34/109.36 | % 145.34/109.36 | Instantiating formula (90) with all_0_2_2, all_0_3_3 and discharging atoms sbrdtbr0(all_0_3_3) = all_0_2_2, yields: % 145.34/109.36 | (158) ? [v0] : (( ~ (v0 = 0) & isFinite0(all_0_3_3) = v0) | ( ~ (v0 = 0) & aSet0(all_0_3_3) = v0) | (szszuzczcdt0(all_0_2_2) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (aElementOf0(v1, all_0_3_3) = v2) | ? [v3] : ? [v4] : ((v4 = v0 & sbrdtbr0(v3) = v0 & sdtpldt0(all_0_3_3, v1) = v3) | ( ~ (v3 = 0) & aElement0(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (sdtpldt0(all_0_3_3, v1) = v2) | ? [v3] : ((v3 = v0 & sbrdtbr0(v2) = v0) | (v3 = 0 & aElementOf0(v1, all_0_3_3) = 0) | ( ~ (v3 = 0) & aElement0(v1) = v3))) & ! [v1] : ( ~ (aElement0(v1) = 0) | ? [v2] : ? [v3] : ((v3 = v0 & sbrdtbr0(v2) = v0 & sdtpldt0(all_0_3_3, v1) = v2) | (v2 = 0 & aElementOf0(v1, all_0_3_3) = 0))))) % 145.72/109.36 | % 145.72/109.36 | Instantiating formula (93) with all_0_0_0, xS and discharging atoms sbrdtbr0(xS) = all_0_0_0, yields: % 145.72/109.36 | (159) ? [v0] : ? [v1] : (( ~ (v0 = 0) & aSet0(xS) = v0) | (((v1 = 0 & isFinite0(xS) = 0) | ( ~ (v0 = 0) & aElementOf0(all_0_0_0, szNzAzT0) = v0)) & ((v0 = 0 & aElementOf0(all_0_0_0, szNzAzT0) = 0) | ( ~ (v1 = 0) & isFinite0(xS) = v1)))) % 145.72/109.36 | % 145.72/109.36 | Instantiating formula (27) with xS and discharging atoms isFinite0(xS) = 0, yields: % 145.72/109.36 | (160) ? [v0] : ? [v1] : (( ~ (v0 = 0) & aSet0(xS) = v0) | (sbrdtbr0(xS) = v0 & szszuzczcdt0(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (aElementOf0(v2, xS) = v3) | ? [v4] : ? [v5] : ((v5 = v1 & sbrdtbr0(v4) = v1 & sdtpldt0(xS, v2) = v4) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(xS, v2) = v3) | ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1) | (v4 = 0 & aElementOf0(v2, xS) = 0) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ( ~ (aElement0(v2) = 0) | ? [v3] : ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1 & sdtpldt0(xS, v2) = v3) | (v3 = 0 & aElementOf0(v2, xS) = 0))))) % 145.72/109.36 | % 145.72/109.36 | Instantiating formula (130) with 0, xS and discharging atoms isFinite0(xS) = 0, yields: % 145.72/109.36 | (161) ? [v0] : ? [v1] : ((v1 = 0 & sbrdtbr0(xS) = v0 & aElementOf0(v0, szNzAzT0) = 0) | ( ~ (v0 = 0) & aSet0(xS) = v0)) % 145.72/109.36 | % 145.72/109.36 | Instantiating formula (86) with all_0_3_3 and discharging atoms aSet0(all_0_3_3) = 0, yields: % 145.72/109.36 | (162) ? [v0] : ? [v1] : ? [v2] : (((v2 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (v1 = 0) & sbrdtbr0(all_0_3_3) = v0 & aElementOf0(v0, szNzAzT0) = v1)) & ((v1 = 0 & sbrdtbr0(all_0_3_3) = v0 & aElementOf0(v0, szNzAzT0) = 0) | ( ~ (v2 = 0) & isFinite0(all_0_3_3) = v2))) % 145.72/109.36 | % 145.72/109.36 | Instantiating formula (102) with all_0_3_3 and discharging atoms aSet0(all_0_3_3) = 0, yields: % 145.72/109.36 | (163) ? [v0] : ? [v1] : (( ~ (v0 = 0) & isFinite0(all_0_3_3) = v0) | (sbrdtbr0(all_0_3_3) = v0 & szszuzczcdt0(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (aElementOf0(v2, all_0_3_3) = v3) | ? [v4] : ? [v5] : ((v5 = v1 & sbrdtbr0(v4) = v1 & sdtpldt0(all_0_3_3, v2) = v4) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(all_0_3_3, v2) = v3) | ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1) | (v4 = 0 & aElementOf0(v2, all_0_3_3) = 0) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ( ~ (aElement0(v2) = 0) | ? [v3] : ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1 & sdtpldt0(all_0_3_3, v2) = v3) | (v3 = 0 & aElementOf0(v2, all_0_3_3) = 0))))) % 145.72/109.36 | % 145.72/109.37 | Instantiating formula (36) with xS, all_0_3_3 and discharging atoms aSet0(all_0_3_3) = 0, aSet0(xS) = 0, yields: % 145.72/109.37 | (164) ? [v0] : ? [v1] : ? [v2] : ((v1 = 0 & ~ (v2 = 0) & aElementOf0(v0, all_0_3_3) = v2 & aElementOf0(v0, xS) = 0) | (v0 = 0 & aSubsetOf0(xS, all_0_3_3) = 0)) % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (86) with xS and discharging atoms aSet0(xS) = 0, yields: % 145.72/109.37 | (165) ? [v0] : ? [v1] : ? [v2] : (((v2 = 0 & isFinite0(xS) = 0) | ( ~ (v1 = 0) & sbrdtbr0(xS) = v0 & aElementOf0(v0, szNzAzT0) = v1)) & ((v1 = 0 & sbrdtbr0(xS) = v0 & aElementOf0(v0, szNzAzT0) = 0) | ( ~ (v2 = 0) & isFinite0(xS) = v2))) % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (102) with xS and discharging atoms aSet0(xS) = 0, yields: % 145.72/109.37 | (166) ? [v0] : ? [v1] : (( ~ (v0 = 0) & isFinite0(xS) = v0) | (sbrdtbr0(xS) = v0 & szszuzczcdt0(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (aElementOf0(v2, xS) = v3) | ? [v4] : ? [v5] : ((v5 = v1 & sbrdtbr0(v4) = v1 & sdtpldt0(xS, v2) = v4) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(xS, v2) = v3) | ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1) | (v4 = 0 & aElementOf0(v2, xS) = 0) | ( ~ (v4 = 0) & aElement0(v2) = v4))) & ! [v2] : ( ~ (aElement0(v2) = 0) | ? [v3] : ? [v4] : ((v4 = v1 & sbrdtbr0(v3) = v1 & sdtpldt0(xS, v2) = v3) | (v3 = 0 & aElementOf0(v2, xS) = 0))))) % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (85) with xS and discharging atoms aSet0(xS) = 0, yields: % 145.72/109.37 | (167) ? [v0] : (sbrdtbr0(xS) = v0 & aElement0(v0) = 0) % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (70) with xx, 0, xS, all_0_3_3 and discharging atoms aSet0(all_0_3_3) = 0, aSet0(xS) = 0, aElementOf0(xx, xS) = 0, yields: % 145.72/109.37 | (168) ? [v0] : ((v0 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (v0 = 0) & aSubsetOf0(xS, all_0_3_3) = v0)) % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (48) with xx, xS and discharging atoms aSet0(xS) = 0, aElementOf0(xx, xS) = 0, yields: % 145.72/109.37 | (169) aElement0(xx) = 0 % 145.72/109.37 | % 145.72/109.37 | Instantiating formula (117) with xx, xS and discharging atoms aSet0(xS) = 0, aElementOf0(xx, xS) = 0, yields: % 145.72/109.37 | (170) ? [v0] : (sdtmndt0(xS, xx) = v0 & sdtpldt0(v0, xx) = xS) % 145.72/109.37 | % 145.72/109.37 | Instantiating (162) with all_33_0_34, all_33_1_35, all_33_2_36 yields: % 145.72/109.37 | (171) ((all_33_0_34 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_33_1_35 = 0) & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = all_33_1_35)) & ((all_33_1_35 = 0 & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = 0) | ( ~ (all_33_0_34 = 0) & isFinite0(all_0_3_3) = all_33_0_34)) % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (171) yields: % 145.72/109.37 | (172) (all_33_0_34 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_33_1_35 = 0) & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = all_33_1_35) % 145.72/109.37 | (173) (all_33_1_35 = 0 & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = 0) | ( ~ (all_33_0_34 = 0) & isFinite0(all_0_3_3) = all_33_0_34) % 145.72/109.37 | % 145.72/109.37 | Instantiating (160) with all_36_0_40, all_36_1_41 yields: % 145.72/109.37 | (174) ( ~ (all_36_1_41 = 0) & aSet0(xS) = all_36_1_41) | (sbrdtbr0(xS) = all_36_1_41 & szszuzczcdt0(all_36_1_41) = all_36_0_40 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_36_0_40 & sbrdtbr0(v2) = all_36_0_40 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0)))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (168) with all_46_0_53 yields: % 145.72/109.37 | (175) (all_46_0_53 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (all_46_0_53 = 0) & aSubsetOf0(xS, all_0_3_3) = all_46_0_53) % 145.72/109.37 | % 145.72/109.37 | Instantiating (157) with all_57_0_64, all_57_1_65 yields: % 145.72/109.37 | (176) ( ~ (all_57_1_65 = 0) & aSet0(all_0_3_3) = all_57_1_65) | (((all_57_0_64 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_57_1_65 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65)) & ((all_57_1_65 = 0 & aElementOf0(all_0_2_2, szNzAzT0) = 0) | ( ~ (all_57_0_64 = 0) & isFinite0(all_0_3_3) = all_57_0_64))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (159) with all_65_0_75, all_65_1_76 yields: % 145.72/109.37 | (177) ( ~ (all_65_1_76 = 0) & aSet0(xS) = all_65_1_76) | (((all_65_0_75 = 0 & isFinite0(xS) = 0) | ( ~ (all_65_1_76 = 0) & aElementOf0(all_0_0_0, szNzAzT0) = all_65_1_76)) & ((all_65_1_76 = 0 & aElementOf0(all_0_0_0, szNzAzT0) = 0) | ( ~ (all_65_0_75 = 0) & isFinite0(xS) = all_65_0_75))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (158) with all_66_0_77 yields: % 145.72/109.37 | (178) ( ~ (all_66_0_77 = 0) & isFinite0(all_0_3_3) = all_66_0_77) | ( ~ (all_66_0_77 = 0) & aSet0(all_0_3_3) = all_66_0_77) | (szszuzczcdt0(all_0_2_2) = all_66_0_77 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_66_0_77 & sbrdtbr0(v2) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0)))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (170) with all_73_0_83 yields: % 145.72/109.37 | (179) sdtmndt0(xS, xx) = all_73_0_83 & sdtpldt0(all_73_0_83, xx) = xS % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (179) yields: % 145.72/109.37 | (180) sdtmndt0(xS, xx) = all_73_0_83 % 145.72/109.37 | (181) sdtpldt0(all_73_0_83, xx) = xS % 145.72/109.37 | % 145.72/109.37 | Instantiating (161) with all_75_0_84, all_75_1_85 yields: % 145.72/109.37 | (182) (all_75_0_84 = 0 & sbrdtbr0(xS) = all_75_1_85 & aElementOf0(all_75_1_85, szNzAzT0) = 0) | ( ~ (all_75_1_85 = 0) & aSet0(xS) = all_75_1_85) % 145.72/109.37 | % 145.72/109.37 | Instantiating (166) with all_78_0_87, all_78_1_88 yields: % 145.72/109.37 | (183) ( ~ (all_78_1_88 = 0) & isFinite0(xS) = all_78_1_88) | (sbrdtbr0(xS) = all_78_1_88 & szszuzczcdt0(all_78_1_88) = all_78_0_87 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_78_0_87 & sbrdtbr0(v2) = all_78_0_87 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0)))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (165) with all_79_0_89, all_79_1_90, all_79_2_91 yields: % 145.72/109.37 | (184) ((all_79_0_89 = 0 & isFinite0(xS) = 0) | ( ~ (all_79_1_90 = 0) & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90)) & ((all_79_1_90 = 0 & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = 0) | ( ~ (all_79_0_89 = 0) & isFinite0(xS) = all_79_0_89)) % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (184) yields: % 145.72/109.37 | (185) (all_79_0_89 = 0 & isFinite0(xS) = 0) | ( ~ (all_79_1_90 = 0) & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90) % 145.72/109.37 | (186) (all_79_1_90 = 0 & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = 0) | ( ~ (all_79_0_89 = 0) & isFinite0(xS) = all_79_0_89) % 145.72/109.37 | % 145.72/109.37 | Instantiating (164) with all_91_0_106, all_91_1_107, all_91_2_108 yields: % 145.72/109.37 | (187) (all_91_1_107 = 0 & ~ (all_91_0_106 = 0) & aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106 & aElementOf0(all_91_2_108, xS) = 0) | (all_91_2_108 = 0 & aSubsetOf0(xS, all_0_3_3) = 0) % 145.72/109.37 | % 145.72/109.37 | Instantiating (163) with all_98_0_114, all_98_1_115 yields: % 145.72/109.37 | (188) ( ~ (all_98_1_115 = 0) & isFinite0(all_0_3_3) = all_98_1_115) | (sbrdtbr0(all_0_3_3) = all_98_1_115 & szszuzczcdt0(all_98_1_115) = all_98_0_114 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_98_0_114 & sbrdtbr0(v2) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0)))) % 145.72/109.37 | % 145.72/109.37 | Instantiating (167) with all_110_0_131 yields: % 145.72/109.37 | (189) sbrdtbr0(xS) = all_110_0_131 & aElement0(all_110_0_131) = 0 % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (189) yields: % 145.72/109.37 | (190) sbrdtbr0(xS) = all_110_0_131 % 145.72/109.37 | (191) aElement0(all_110_0_131) = 0 % 145.72/109.37 | % 145.72/109.37 +-Applying beta-rule and splitting (182), into two cases. % 145.72/109.37 |-Branch one: % 145.72/109.37 | (192) all_75_0_84 = 0 & sbrdtbr0(xS) = all_75_1_85 & aElementOf0(all_75_1_85, szNzAzT0) = 0 % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (192) yields: % 145.72/109.37 | (193) all_75_0_84 = 0 % 145.72/109.37 | (194) sbrdtbr0(xS) = all_75_1_85 % 145.72/109.37 | (195) aElementOf0(all_75_1_85, szNzAzT0) = 0 % 145.72/109.37 | % 145.72/109.37 +-Applying beta-rule and splitting (175), into two cases. % 145.72/109.37 |-Branch one: % 145.72/109.37 | (196) all_46_0_53 = 0 & aElementOf0(xx, all_0_3_3) = 0 % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (196) yields: % 145.72/109.37 | (197) all_46_0_53 = 0 % 145.72/109.37 | (198) aElementOf0(xx, all_0_3_3) = 0 % 145.72/109.37 | % 145.72/109.37 | Using (198) and (139) yields: % 145.72/109.37 | (199) $false % 145.72/109.37 | % 145.72/109.37 |-The branch is then unsatisfiable % 145.72/109.37 |-Branch two: % 145.72/109.37 | (200) ~ (all_46_0_53 = 0) & aSubsetOf0(xS, all_0_3_3) = all_46_0_53 % 145.72/109.37 | % 145.72/109.37 | Applying alpha-rule on (200) yields: % 145.72/109.37 | (201) ~ (all_46_0_53 = 0) % 145.72/109.37 | (202) aSubsetOf0(xS, all_0_3_3) = all_46_0_53 % 145.72/109.37 | % 145.72/109.37 +-Applying beta-rule and splitting (187), into two cases. % 145.72/109.37 |-Branch one: % 145.72/109.38 | (203) all_91_1_107 = 0 & ~ (all_91_0_106 = 0) & aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106 & aElementOf0(all_91_2_108, xS) = 0 % 145.72/109.38 | % 145.72/109.38 | Applying alpha-rule on (203) yields: % 145.72/109.38 | (204) all_91_1_107 = 0 % 145.72/109.38 | (205) ~ (all_91_0_106 = 0) % 145.72/109.38 | (206) aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106 % 145.72/109.38 | (207) aElementOf0(all_91_2_108, xS) = 0 % 145.72/109.38 | % 145.72/109.38 +-Applying beta-rule and splitting (177), into two cases. % 145.72/109.38 |-Branch one: % 145.72/109.38 | (208) ~ (all_65_1_76 = 0) & aSet0(xS) = all_65_1_76 % 145.72/109.38 | % 145.72/109.38 | Applying alpha-rule on (208) yields: % 145.72/109.38 | (209) ~ (all_65_1_76 = 0) % 145.72/109.38 | (210) aSet0(xS) = all_65_1_76 % 145.72/109.38 | % 145.72/109.38 | Instantiating formula (154) with xS, all_65_1_76, 0 and discharging atoms aSet0(xS) = all_65_1_76, aSet0(xS) = 0, yields: % 145.72/109.38 | (211) all_65_1_76 = 0 % 145.72/109.38 | % 145.72/109.38 | Equations (211) can reduce 209 to: % 145.78/109.38 | (212) $false % 145.78/109.38 | % 145.78/109.38 |-The branch is then unsatisfiable % 145.78/109.38 |-Branch two: % 145.78/109.38 | (213) ((all_65_0_75 = 0 & isFinite0(xS) = 0) | ( ~ (all_65_1_76 = 0) & aElementOf0(all_0_0_0, szNzAzT0) = all_65_1_76)) & ((all_65_1_76 = 0 & aElementOf0(all_0_0_0, szNzAzT0) = 0) | ( ~ (all_65_0_75 = 0) & isFinite0(xS) = all_65_0_75)) % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (213) yields: % 145.78/109.38 | (214) (all_65_0_75 = 0 & isFinite0(xS) = 0) | ( ~ (all_65_1_76 = 0) & aElementOf0(all_0_0_0, szNzAzT0) = all_65_1_76) % 145.78/109.38 | (215) (all_65_1_76 = 0 & aElementOf0(all_0_0_0, szNzAzT0) = 0) | ( ~ (all_65_0_75 = 0) & isFinite0(xS) = all_65_0_75) % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (174), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (216) ~ (all_36_1_41 = 0) & aSet0(xS) = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (216) yields: % 145.78/109.38 | (217) ~ (all_36_1_41 = 0) % 145.78/109.38 | (218) aSet0(xS) = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (154) with xS, all_36_1_41, 0 and discharging atoms aSet0(xS) = all_36_1_41, aSet0(xS) = 0, yields: % 145.78/109.38 | (219) all_36_1_41 = 0 % 145.78/109.38 | % 145.78/109.38 | Equations (219) can reduce 217 to: % 145.78/109.38 | (212) $false % 145.78/109.38 | % 145.78/109.38 |-The branch is then unsatisfiable % 145.78/109.38 |-Branch two: % 145.78/109.38 | (221) sbrdtbr0(xS) = all_36_1_41 & szszuzczcdt0(all_36_1_41) = all_36_0_40 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_36_0_40 & sbrdtbr0(v2) = all_36_0_40 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0))) % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (221) yields: % 145.78/109.38 | (222) ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.38 | (223) szszuzczcdt0(all_36_1_41) = all_36_0_40 % 145.78/109.38 | (224) ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_36_0_40 & sbrdtbr0(v1) = all_36_0_40 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0))) % 145.78/109.38 | (225) sbrdtbr0(xS) = all_36_1_41 % 145.78/109.38 | (226) ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_36_0_40 & sbrdtbr0(v2) = all_36_0_40 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (186), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (227) all_79_1_90 = 0 & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = 0 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (227) yields: % 145.78/109.38 | (228) all_79_1_90 = 0 % 145.78/109.38 | (229) sbrdtbr0(xS) = all_79_2_91 % 145.78/109.38 | (230) aElementOf0(all_79_2_91, szNzAzT0) = 0 % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (183), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (231) ~ (all_78_1_88 = 0) & isFinite0(xS) = all_78_1_88 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (231) yields: % 145.78/109.38 | (232) ~ (all_78_1_88 = 0) % 145.78/109.38 | (233) isFinite0(xS) = all_78_1_88 % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (185), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (234) all_79_0_89 = 0 & isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (234) yields: % 145.78/109.38 | (235) all_79_0_89 = 0 % 145.78/109.38 | (124) isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (59) with xS, all_78_1_88, 0 and discharging atoms isFinite0(xS) = all_78_1_88, isFinite0(xS) = 0, yields: % 145.78/109.38 | (237) all_78_1_88 = 0 % 145.78/109.38 | % 145.78/109.38 | Equations (237) can reduce 232 to: % 145.78/109.38 | (212) $false % 145.78/109.38 | % 145.78/109.38 |-The branch is then unsatisfiable % 145.78/109.38 |-Branch two: % 145.78/109.38 | (239) ~ (all_79_1_90 = 0) & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (239) yields: % 145.78/109.38 | (240) ~ (all_79_1_90 = 0) % 145.78/109.38 | (229) sbrdtbr0(xS) = all_79_2_91 % 145.78/109.38 | (242) aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90 % 145.78/109.38 | % 145.78/109.38 | Equations (228) can reduce 240 to: % 145.78/109.38 | (212) $false % 145.78/109.38 | % 145.78/109.38 |-The branch is then unsatisfiable % 145.78/109.38 |-Branch two: % 145.78/109.38 | (244) sbrdtbr0(xS) = all_78_1_88 & szszuzczcdt0(all_78_1_88) = all_78_0_87 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_78_0_87 & sbrdtbr0(v2) = all_78_0_87 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0))) % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (244) yields: % 145.78/109.38 | (245) ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | ? [v2] : ? [v3] : ((v3 = all_78_0_87 & sbrdtbr0(v2) = all_78_0_87 & sdtpldt0(xS, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.38 | (246) sbrdtbr0(xS) = all_78_1_88 % 145.78/109.38 | (247) szszuzczcdt0(all_78_1_88) = all_78_0_87 % 145.78/109.38 | (248) ! [v0] : ! [v1] : ( ~ (sdtpldt0(xS, v0) = v1) | ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87) | (v2 = 0 & aElementOf0(v0, xS) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.38 | (249) ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_78_0_87 & sbrdtbr0(v1) = all_78_0_87 & sdtpldt0(xS, v0) = v1) | (v1 = 0 & aElementOf0(v0, xS) = 0))) % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (185), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (234) all_79_0_89 = 0 & isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (234) yields: % 145.78/109.38 | (235) all_79_0_89 = 0 % 145.78/109.38 | (124) isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (215), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (253) all_65_1_76 = 0 & aElementOf0(all_0_0_0, szNzAzT0) = 0 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (253) yields: % 145.78/109.38 | (211) all_65_1_76 = 0 % 145.78/109.38 | (255) aElementOf0(all_0_0_0, szNzAzT0) = 0 % 145.78/109.38 | % 145.78/109.38 +-Applying beta-rule and splitting (214), into two cases. % 145.78/109.38 |-Branch one: % 145.78/109.38 | (256) all_65_0_75 = 0 & isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 | Applying alpha-rule on (256) yields: % 145.78/109.38 | (257) all_65_0_75 = 0 % 145.78/109.38 | (124) isFinite0(xS) = 0 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (101) with xS, all_79_2_91, all_0_0_0 and discharging atoms sbrdtbr0(xS) = all_79_2_91, sbrdtbr0(xS) = all_0_0_0, yields: % 145.78/109.38 | (259) all_79_2_91 = all_0_0_0 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (101) with xS, all_78_1_88, all_110_0_131 and discharging atoms sbrdtbr0(xS) = all_110_0_131, sbrdtbr0(xS) = all_78_1_88, yields: % 145.78/109.38 | (260) all_110_0_131 = all_78_1_88 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (101) with xS, all_75_1_85, all_79_2_91 and discharging atoms sbrdtbr0(xS) = all_79_2_91, sbrdtbr0(xS) = all_75_1_85, yields: % 145.78/109.38 | (261) all_79_2_91 = all_75_1_85 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (101) with xS, all_75_1_85, all_78_1_88 and discharging atoms sbrdtbr0(xS) = all_78_1_88, sbrdtbr0(xS) = all_75_1_85, yields: % 145.78/109.38 | (262) all_78_1_88 = all_75_1_85 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (101) with xS, all_36_1_41, all_110_0_131 and discharging atoms sbrdtbr0(xS) = all_110_0_131, sbrdtbr0(xS) = all_36_1_41, yields: % 145.78/109.38 | (263) all_110_0_131 = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Instantiating formula (150) with xS, xx, all_73_0_83, all_0_3_3 and discharging atoms sdtmndt0(xS, xx) = all_73_0_83, sdtmndt0(xS, xx) = all_0_3_3, yields: % 145.78/109.38 | (264) all_73_0_83 = all_0_3_3 % 145.78/109.38 | % 145.78/109.38 | Combining equations (260,263) yields a new equation: % 145.78/109.38 | (265) all_78_1_88 = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Simplifying 265 yields: % 145.78/109.38 | (266) all_78_1_88 = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Combining equations (261,259) yields a new equation: % 145.78/109.38 | (267) all_75_1_85 = all_0_0_0 % 145.78/109.38 | % 145.78/109.38 | Simplifying 267 yields: % 145.78/109.38 | (268) all_75_1_85 = all_0_0_0 % 145.78/109.38 | % 145.78/109.38 | Combining equations (262,266) yields a new equation: % 145.78/109.38 | (269) all_75_1_85 = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Simplifying 269 yields: % 145.78/109.38 | (270) all_75_1_85 = all_36_1_41 % 145.78/109.38 | % 145.78/109.38 | Combining equations (268,270) yields a new equation: % 145.78/109.38 | (271) all_36_1_41 = all_0_0_0 % 145.78/109.38 | % 145.78/109.38 | From (271) and (225) follows: % 145.78/109.38 | (84) sbrdtbr0(xS) = all_0_0_0 % 145.78/109.38 | % 145.78/109.38 | From (264) and (180) follows: % 145.78/109.38 | (5) sdtmndt0(xS, xx) = all_0_3_3 % 145.78/109.38 | % 145.78/109.38 | From (264) and (181) follows: % 145.78/109.39 | (274) sdtpldt0(all_0_3_3, xx) = xS % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (43) with all_0_3_3, xS, xx and discharging atoms sdtmndt0(xS, xx) = all_0_3_3, aElement0(xx) = 0, yields: % 145.78/109.39 | (275) ? [v0] : ((v0 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (v0 = 0) & isFinite0(xS) = v0) | ( ~ (v0 = 0) & aSet0(xS) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (83) with all_91_0_106, all_91_2_108, 0, szNzAzT0, all_0_3_3 and discharging atoms aSet0(all_0_3_3) = 0, aSet0(szNzAzT0) = 0, aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106, yields: % 145.78/109.39 | (276) all_91_0_106 = 0 | ? [v0] : (( ~ (v0 = 0) & aSubsetOf0(szNzAzT0, all_0_3_3) = v0) | ( ~ (v0 = 0) & aElementOf0(all_91_2_108, szNzAzT0) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (44) with all_91_0_106, all_0_3_3, all_91_2_108 and discharging atoms aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106, yields: % 145.78/109.39 | (277) all_91_0_106 = 0 | ? [v0] : ? [v1] : ((v1 = all_0_3_3 & sdtmndt0(v0, all_91_2_108) = all_0_3_3 & sdtpldt0(all_0_3_3, all_91_2_108) = v0) | ( ~ (v0 = 0) & aSet0(all_0_3_3) = v0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (14) with all_91_2_108, 0, all_0_3_3, xx, xS and discharging atoms sdtmndt0(xS, xx) = all_0_3_3, aSet0(all_0_3_3) = 0, aElementOf0(all_91_2_108, xS) = 0, yields: % 145.78/109.39 | (278) all_91_2_108 = xx | ? [v0] : ((v0 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) | ( ~ (v0 = 0) & aSet0(xS) = v0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0) | ( ~ (v0 = 0) & aElement0(xx) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (111) with all_91_2_108, 0, xS, xx, all_0_3_3 and discharging atoms sdtpldt0(all_0_3_3, xx) = xS, aSet0(xS) = 0, aElementOf0(all_91_2_108, xS) = 0, yields: % 145.78/109.39 | (279) ? [v0] : ? [v1] : ((v0 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (v1 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0))) | ( ~ (v0 = 0) & aSet0(all_0_3_3) = v0) | ( ~ (v0 = 0) & aElement0(xx) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (48) with all_91_2_108, xS and discharging atoms aSet0(xS) = 0, aElementOf0(all_91_2_108, xS) = 0, yields: % 145.78/109.39 | (280) aElement0(all_91_2_108) = 0 % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (46) with all_91_2_108 and discharging atoms aElementOf0(all_91_2_108, xS) = 0, yields: % 145.78/109.39 | (281) all_91_2_108 = xx | ? [v0] : ((v0 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating (279) with all_313_0_189, all_313_1_190 yields: % 145.78/109.39 | (282) (all_313_1_190 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0))) | ( ~ (all_313_1_190 = 0) & aSet0(all_0_3_3) = all_313_1_190) | ( ~ (all_313_1_190 = 0) & aElement0(xx) = all_313_1_190) % 145.78/109.39 | % 145.78/109.39 | Instantiating (275) with all_321_0_197 yields: % 145.78/109.39 | (283) (all_321_0_197 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_321_0_197 = 0) & isFinite0(xS) = all_321_0_197) | ( ~ (all_321_0_197 = 0) & aSet0(xS) = all_321_0_197) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (278), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (284) all_91_2_108 = xx % 145.78/109.39 | % 145.78/109.39 | From (284) and (280) follows: % 145.78/109.39 | (169) aElement0(xx) = 0 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (283), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (286) (all_321_0_197 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_321_0_197 = 0) & isFinite0(xS) = all_321_0_197) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (286), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (287) all_321_0_197 = 0 & isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (287) yields: % 145.78/109.39 | (288) all_321_0_197 = 0 % 145.78/109.39 | (289) isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (173), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (290) all_33_1_35 = 0 & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = 0 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (290) yields: % 145.78/109.39 | (291) all_33_1_35 = 0 % 145.78/109.39 | (292) sbrdtbr0(all_0_3_3) = all_33_2_36 % 145.78/109.39 | (293) aElementOf0(all_33_2_36, szNzAzT0) = 0 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (176), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (294) ~ (all_57_1_65 = 0) & aSet0(all_0_3_3) = all_57_1_65 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (294) yields: % 145.78/109.39 | (295) ~ (all_57_1_65 = 0) % 145.78/109.39 | (296) aSet0(all_0_3_3) = all_57_1_65 % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (154) with all_0_3_3, all_57_1_65, 0 and discharging atoms aSet0(all_0_3_3) = all_57_1_65, aSet0(all_0_3_3) = 0, yields: % 145.78/109.39 | (297) all_57_1_65 = 0 % 145.78/109.39 | % 145.78/109.39 | Equations (297) can reduce 295 to: % 145.78/109.39 | (212) $false % 145.78/109.39 | % 145.78/109.39 |-The branch is then unsatisfiable % 145.78/109.39 |-Branch two: % 145.78/109.39 | (299) ((all_57_0_64 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_57_1_65 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65)) & ((all_57_1_65 = 0 & aElementOf0(all_0_2_2, szNzAzT0) = 0) | ( ~ (all_57_0_64 = 0) & isFinite0(all_0_3_3) = all_57_0_64)) % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (299) yields: % 145.78/109.39 | (300) (all_57_0_64 = 0 & isFinite0(all_0_3_3) = 0) | ( ~ (all_57_1_65 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65) % 145.78/109.39 | (301) (all_57_1_65 = 0 & aElementOf0(all_0_2_2, szNzAzT0) = 0) | ( ~ (all_57_0_64 = 0) & isFinite0(all_0_3_3) = all_57_0_64) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (301), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (302) all_57_1_65 = 0 & aElementOf0(all_0_2_2, szNzAzT0) = 0 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (302) yields: % 145.78/109.39 | (297) all_57_1_65 = 0 % 145.78/109.39 | (304) aElementOf0(all_0_2_2, szNzAzT0) = 0 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (282), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (305) (all_313_1_190 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0))) | ( ~ (all_313_1_190 = 0) & aSet0(all_0_3_3) = all_313_1_190) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (305), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (306) all_313_1_190 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0)) % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (306) yields: % 145.78/109.39 | (307) all_313_1_190 = 0 % 145.78/109.39 | (280) aElement0(all_91_2_108) = 0 % 145.78/109.39 | (309) all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) % 145.78/109.39 | % 145.78/109.39 | From (284) and (280) follows: % 145.78/109.39 | (169) aElement0(xx) = 0 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (188), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (311) ~ (all_98_1_115 = 0) & isFinite0(all_0_3_3) = all_98_1_115 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (311) yields: % 145.78/109.39 | (312) ~ (all_98_1_115 = 0) % 145.78/109.39 | (313) isFinite0(all_0_3_3) = all_98_1_115 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (300), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (314) all_57_0_64 = 0 & isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (314) yields: % 145.78/109.39 | (315) all_57_0_64 = 0 % 145.78/109.39 | (289) isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (59) with all_0_3_3, 0, all_98_1_115 and discharging atoms isFinite0(all_0_3_3) = all_98_1_115, isFinite0(all_0_3_3) = 0, yields: % 145.78/109.39 | (317) all_98_1_115 = 0 % 145.78/109.39 | % 145.78/109.39 | Equations (317) can reduce 312 to: % 145.78/109.39 | (212) $false % 145.78/109.39 | % 145.78/109.39 |-The branch is then unsatisfiable % 145.78/109.39 |-Branch two: % 145.78/109.39 | (319) ~ (all_57_1_65 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (319) yields: % 145.78/109.39 | (295) ~ (all_57_1_65 = 0) % 145.78/109.39 | (321) aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65 % 145.78/109.39 | % 145.78/109.39 | Equations (297) can reduce 295 to: % 145.78/109.39 | (212) $false % 145.78/109.39 | % 145.78/109.39 |-The branch is then unsatisfiable % 145.78/109.39 |-Branch two: % 145.78/109.39 | (323) sbrdtbr0(all_0_3_3) = all_98_1_115 & szszuzczcdt0(all_98_1_115) = all_98_0_114 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_98_0_114 & sbrdtbr0(v2) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0))) % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (323) yields: % 145.78/109.39 | (324) ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_98_0_114 & sbrdtbr0(v2) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.39 | (325) sbrdtbr0(all_0_3_3) = all_98_1_115 % 145.78/109.39 | (326) ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0))) % 145.78/109.39 | (327) ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_98_0_114 & sbrdtbr0(v1) = all_98_0_114) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.39 | (328) szszuzczcdt0(all_98_1_115) = all_98_0_114 % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (327) with xS, xx and discharging atoms sdtpldt0(all_0_3_3, xx) = xS, yields: % 145.78/109.39 | (329) ? [v0] : ((v0 = all_98_0_114 & sbrdtbr0(xS) = all_98_0_114) | (v0 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (v0 = 0) & aElement0(xx) = v0)) % 145.78/109.39 | % 145.78/109.39 | Instantiating (329) with all_707_0_1482 yields: % 145.78/109.39 | (330) (all_707_0_1482 = all_98_0_114 & sbrdtbr0(xS) = all_98_0_114) | (all_707_0_1482 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (all_707_0_1482 = 0) & aElement0(xx) = all_707_0_1482) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (330), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (331) (all_707_0_1482 = all_98_0_114 & sbrdtbr0(xS) = all_98_0_114) | (all_707_0_1482 = 0 & aElementOf0(xx, all_0_3_3) = 0) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (331), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (332) all_707_0_1482 = all_98_0_114 & sbrdtbr0(xS) = all_98_0_114 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (332) yields: % 145.78/109.39 | (333) all_707_0_1482 = all_98_0_114 % 145.78/109.39 | (334) sbrdtbr0(xS) = all_98_0_114 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (178), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (335) ( ~ (all_66_0_77 = 0) & isFinite0(all_0_3_3) = all_66_0_77) | ( ~ (all_66_0_77 = 0) & aSet0(all_0_3_3) = all_66_0_77) % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (335), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (336) ~ (all_66_0_77 = 0) & isFinite0(all_0_3_3) = all_66_0_77 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (336) yields: % 145.78/109.39 | (337) ~ (all_66_0_77 = 0) % 145.78/109.39 | (338) isFinite0(all_0_3_3) = all_66_0_77 % 145.78/109.39 | % 145.78/109.39 +-Applying beta-rule and splitting (300), into two cases. % 145.78/109.39 |-Branch one: % 145.78/109.39 | (314) all_57_0_64 = 0 & isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 | Applying alpha-rule on (314) yields: % 145.78/109.39 | (315) all_57_0_64 = 0 % 145.78/109.39 | (289) isFinite0(all_0_3_3) = 0 % 145.78/109.39 | % 145.78/109.39 | Instantiating formula (59) with all_0_3_3, 0, all_66_0_77 and discharging atoms isFinite0(all_0_3_3) = all_66_0_77, isFinite0(all_0_3_3) = 0, yields: % 145.78/109.40 | (342) all_66_0_77 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (342) can reduce 337 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (319) ~ (all_57_1_65 = 0) & aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (319) yields: % 145.78/109.40 | (295) ~ (all_57_1_65 = 0) % 145.78/109.40 | (321) aElementOf0(all_0_2_2, szNzAzT0) = all_57_1_65 % 145.78/109.40 | % 145.78/109.40 | Equations (297) can reduce 295 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (348) ~ (all_66_0_77 = 0) & aSet0(all_0_3_3) = all_66_0_77 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (348) yields: % 145.78/109.40 | (337) ~ (all_66_0_77 = 0) % 145.78/109.40 | (350) aSet0(all_0_3_3) = all_66_0_77 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (154) with all_0_3_3, all_66_0_77, 0 and discharging atoms aSet0(all_0_3_3) = all_66_0_77, aSet0(all_0_3_3) = 0, yields: % 145.78/109.40 | (342) all_66_0_77 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (342) can reduce 337 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (353) szszuzczcdt0(all_0_2_2) = all_66_0_77 & ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_66_0_77 & sbrdtbr0(v2) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) & ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0))) % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (353) yields: % 145.78/109.40 | (354) szszuzczcdt0(all_0_2_2) = all_66_0_77 % 145.78/109.40 | (355) ! [v0] : ! [v1] : (v1 = 0 | ~ (aElementOf0(v0, all_0_3_3) = v1) | ? [v2] : ? [v3] : ((v3 = all_66_0_77 & sbrdtbr0(v2) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v2) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.40 | (356) ! [v0] : ! [v1] : ( ~ (sdtpldt0(all_0_3_3, v0) = v1) | ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77) | (v2 = 0 & aElementOf0(v0, all_0_3_3) = 0) | ( ~ (v2 = 0) & aElement0(v0) = v2))) % 145.78/109.40 | (357) ! [v0] : ( ~ (aElement0(v0) = 0) | ? [v1] : ? [v2] : ((v2 = all_66_0_77 & sbrdtbr0(v1) = all_66_0_77 & sdtpldt0(all_0_3_3, v0) = v1) | (v1 = 0 & aElementOf0(v0, all_0_3_3) = 0))) % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (356) with xS, xx and discharging atoms sdtpldt0(all_0_3_3, xx) = xS, yields: % 145.78/109.40 | (358) ? [v0] : ((v0 = all_66_0_77 & sbrdtbr0(xS) = all_66_0_77) | (v0 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (v0 = 0) & aElement0(xx) = v0)) % 145.78/109.40 | % 145.78/109.40 | Instantiating (358) with all_731_0_1523 yields: % 145.78/109.40 | (359) (all_731_0_1523 = all_66_0_77 & sbrdtbr0(xS) = all_66_0_77) | (all_731_0_1523 = 0 & aElementOf0(xx, all_0_3_3) = 0) | ( ~ (all_731_0_1523 = 0) & aElement0(xx) = all_731_0_1523) % 145.78/109.40 | % 145.78/109.40 +-Applying beta-rule and splitting (359), into two cases. % 145.78/109.40 |-Branch one: % 145.78/109.40 | (360) (all_731_0_1523 = all_66_0_77 & sbrdtbr0(xS) = all_66_0_77) | (all_731_0_1523 = 0 & aElementOf0(xx, all_0_3_3) = 0) % 145.78/109.40 | % 145.78/109.40 +-Applying beta-rule and splitting (360), into two cases. % 145.78/109.40 |-Branch one: % 145.78/109.40 | (361) all_731_0_1523 = all_66_0_77 & sbrdtbr0(xS) = all_66_0_77 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (361) yields: % 145.78/109.40 | (362) all_731_0_1523 = all_66_0_77 % 145.78/109.40 | (363) sbrdtbr0(xS) = all_66_0_77 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (101) with xS, all_98_0_114, all_0_0_0 and discharging atoms sbrdtbr0(xS) = all_98_0_114, sbrdtbr0(xS) = all_0_0_0, yields: % 145.78/109.40 | (364) all_98_0_114 = all_0_0_0 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (101) with xS, all_66_0_77, all_98_0_114 and discharging atoms sbrdtbr0(xS) = all_98_0_114, sbrdtbr0(xS) = all_66_0_77, yields: % 145.78/109.40 | (365) all_98_0_114 = all_66_0_77 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (50) with all_0_2_2, all_66_0_77, all_0_1_1 and discharging atoms szszuzczcdt0(all_0_2_2) = all_66_0_77, szszuzczcdt0(all_0_2_2) = all_0_1_1, yields: % 145.78/109.40 | (366) all_66_0_77 = all_0_1_1 % 145.78/109.40 | % 145.78/109.40 | Combining equations (365,364) yields a new equation: % 145.78/109.40 | (367) all_66_0_77 = all_0_0_0 % 145.78/109.40 | % 145.78/109.40 | Simplifying 367 yields: % 145.78/109.40 | (368) all_66_0_77 = all_0_0_0 % 145.78/109.40 | % 145.78/109.40 | Combining equations (366,368) yields a new equation: % 145.78/109.40 | (369) all_0_0_0 = all_0_1_1 % 145.78/109.40 | % 145.78/109.40 | Equations (369) can reduce 69 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (371) all_731_0_1523 = 0 & aElementOf0(xx, all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (371) yields: % 145.78/109.40 | (372) all_731_0_1523 = 0 % 145.78/109.40 | (198) aElementOf0(xx, all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Using (198) and (139) yields: % 145.78/109.40 | (199) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (375) ~ (all_731_0_1523 = 0) & aElement0(xx) = all_731_0_1523 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (375) yields: % 145.78/109.40 | (376) ~ (all_731_0_1523 = 0) % 145.78/109.40 | (377) aElement0(xx) = all_731_0_1523 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (49) with xx, all_731_0_1523, 0 and discharging atoms aElement0(xx) = all_731_0_1523, aElement0(xx) = 0, yields: % 145.78/109.40 | (372) all_731_0_1523 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (372) can reduce 376 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (380) all_707_0_1482 = 0 & aElementOf0(xx, all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (380) yields: % 145.78/109.40 | (381) all_707_0_1482 = 0 % 145.78/109.40 | (198) aElementOf0(xx, all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Using (198) and (139) yields: % 145.78/109.40 | (199) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (384) ~ (all_707_0_1482 = 0) & aElement0(xx) = all_707_0_1482 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (384) yields: % 145.78/109.40 | (385) ~ (all_707_0_1482 = 0) % 145.78/109.40 | (386) aElement0(xx) = all_707_0_1482 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (49) with xx, all_707_0_1482, 0 and discharging atoms aElement0(xx) = all_707_0_1482, aElement0(xx) = 0, yields: % 145.78/109.40 | (381) all_707_0_1482 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (381) can reduce 385 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (389) ~ (all_313_1_190 = 0) & aSet0(all_0_3_3) = all_313_1_190 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (389) yields: % 145.78/109.40 | (390) ~ (all_313_1_190 = 0) % 145.78/109.40 | (391) aSet0(all_0_3_3) = all_313_1_190 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (154) with all_0_3_3, all_313_1_190, 0 and discharging atoms aSet0(all_0_3_3) = all_313_1_190, aSet0(all_0_3_3) = 0, yields: % 145.78/109.40 | (307) all_313_1_190 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (307) can reduce 390 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (394) ~ (all_313_1_190 = 0) & aElement0(xx) = all_313_1_190 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (394) yields: % 145.78/109.40 | (390) ~ (all_313_1_190 = 0) % 145.78/109.40 | (396) aElement0(xx) = all_313_1_190 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (49) with xx, all_313_1_190, 0 and discharging atoms aElement0(xx) = all_313_1_190, aElement0(xx) = 0, yields: % 145.78/109.40 | (307) all_313_1_190 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (307) can reduce 390 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (399) ~ (all_57_0_64 = 0) & isFinite0(all_0_3_3) = all_57_0_64 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (399) yields: % 145.78/109.40 | (400) ~ (all_57_0_64 = 0) % 145.78/109.40 | (401) isFinite0(all_0_3_3) = all_57_0_64 % 145.78/109.40 | % 145.78/109.40 +-Applying beta-rule and splitting (172), into two cases. % 145.78/109.40 |-Branch one: % 145.78/109.40 | (402) all_33_0_34 = 0 & isFinite0(all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (402) yields: % 145.78/109.40 | (403) all_33_0_34 = 0 % 145.78/109.40 | (289) isFinite0(all_0_3_3) = 0 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (59) with all_0_3_3, 0, all_57_0_64 and discharging atoms isFinite0(all_0_3_3) = all_57_0_64, isFinite0(all_0_3_3) = 0, yields: % 145.78/109.40 | (315) all_57_0_64 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (315) can reduce 400 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (407) ~ (all_33_1_35 = 0) & sbrdtbr0(all_0_3_3) = all_33_2_36 & aElementOf0(all_33_2_36, szNzAzT0) = all_33_1_35 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (407) yields: % 145.78/109.40 | (408) ~ (all_33_1_35 = 0) % 145.78/109.40 | (292) sbrdtbr0(all_0_3_3) = all_33_2_36 % 145.78/109.40 | (410) aElementOf0(all_33_2_36, szNzAzT0) = all_33_1_35 % 145.78/109.40 | % 145.78/109.40 | Equations (291) can reduce 408 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (412) ~ (all_33_0_34 = 0) & isFinite0(all_0_3_3) = all_33_0_34 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (412) yields: % 145.78/109.40 | (413) ~ (all_33_0_34 = 0) % 145.78/109.40 | (414) isFinite0(all_0_3_3) = all_33_0_34 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (59) with all_0_3_3, 0, all_33_0_34 and discharging atoms isFinite0(all_0_3_3) = all_33_0_34, isFinite0(all_0_3_3) = 0, yields: % 145.78/109.40 | (403) all_33_0_34 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (403) can reduce 413 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (417) ~ (all_321_0_197 = 0) & isFinite0(xS) = all_321_0_197 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (417) yields: % 145.78/109.40 | (418) ~ (all_321_0_197 = 0) % 145.78/109.40 | (419) isFinite0(xS) = all_321_0_197 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (59) with xS, all_321_0_197, 0 and discharging atoms isFinite0(xS) = all_321_0_197, isFinite0(xS) = 0, yields: % 145.78/109.40 | (288) all_321_0_197 = 0 % 145.78/109.40 | % 145.78/109.40 | Equations (288) can reduce 418 to: % 145.78/109.40 | (212) $false % 145.78/109.40 | % 145.78/109.40 |-The branch is then unsatisfiable % 145.78/109.40 |-Branch two: % 145.78/109.40 | (422) ~ (all_321_0_197 = 0) & aSet0(xS) = all_321_0_197 % 145.78/109.40 | % 145.78/109.40 | Applying alpha-rule on (422) yields: % 145.78/109.40 | (418) ~ (all_321_0_197 = 0) % 145.78/109.40 | (424) aSet0(xS) = all_321_0_197 % 145.78/109.40 | % 145.78/109.40 | Instantiating formula (154) with xS, all_321_0_197, 0 and discharging atoms aSet0(xS) = all_321_0_197, aSet0(xS) = 0, yields: % 145.78/109.41 | (288) all_321_0_197 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (288) can reduce 418 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (427) ~ (all_91_2_108 = xx) % 145.78/109.41 | (428) ? [v0] : ((v0 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) | ( ~ (v0 = 0) & aSet0(xS) = v0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0) | ( ~ (v0 = 0) & aElement0(xx) = v0)) % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (282), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (305) (all_313_1_190 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0))) | ( ~ (all_313_1_190 = 0) & aSet0(all_0_3_3) = all_313_1_190) % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (305), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (306) all_313_1_190 = 0 & aElement0(all_91_2_108) = 0 & (all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0)) % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (306) yields: % 145.78/109.41 | (307) all_313_1_190 = 0 % 145.78/109.41 | (280) aElement0(all_91_2_108) = 0 % 145.78/109.41 | (309) all_91_2_108 = xx | (all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (281), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (284) all_91_2_108 = xx % 145.78/109.41 | % 145.78/109.41 | Equations (284) can reduce 427 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (427) ~ (all_91_2_108 = xx) % 145.78/109.41 | (437) ? [v0] : ((v0 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0)) % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (309), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (284) all_91_2_108 = xx % 145.78/109.41 | % 145.78/109.41 | Equations (284) can reduce 427 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (427) ~ (all_91_2_108 = xx) % 145.78/109.41 | (441) all_313_0_189 = 0 & aElementOf0(all_91_2_108, all_0_3_3) = 0 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (441) yields: % 145.78/109.41 | (442) all_313_0_189 = 0 % 145.78/109.41 | (443) aElementOf0(all_91_2_108, all_0_3_3) = 0 % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (277), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (444) all_91_0_106 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (444) can reduce 205 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (205) ~ (all_91_0_106 = 0) % 145.78/109.41 | (447) ? [v0] : ? [v1] : ((v1 = all_0_3_3 & sdtmndt0(v0, all_91_2_108) = all_0_3_3 & sdtpldt0(all_0_3_3, all_91_2_108) = v0) | ( ~ (v0 = 0) & aSet0(all_0_3_3) = v0) | ( ~ (v0 = 0) & aElement0(all_91_2_108) = v0)) % 145.78/109.41 | % 145.78/109.41 +-Applying beta-rule and splitting (276), into two cases. % 145.78/109.41 |-Branch one: % 145.78/109.41 | (444) all_91_0_106 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (444) can reduce 205 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (205) ~ (all_91_0_106 = 0) % 145.78/109.41 | (451) ? [v0] : (( ~ (v0 = 0) & aSubsetOf0(szNzAzT0, all_0_3_3) = v0) | ( ~ (v0 = 0) & aElementOf0(all_91_2_108, szNzAzT0) = v0)) % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (23) with all_91_2_108, all_0_3_3, 0, all_91_0_106 and discharging atoms aElementOf0(all_91_2_108, all_0_3_3) = all_91_0_106, aElementOf0(all_91_2_108, all_0_3_3) = 0, yields: % 145.78/109.41 | (444) all_91_0_106 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (444) can reduce 205 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (389) ~ (all_313_1_190 = 0) & aSet0(all_0_3_3) = all_313_1_190 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (389) yields: % 145.78/109.41 | (390) ~ (all_313_1_190 = 0) % 145.78/109.41 | (391) aSet0(all_0_3_3) = all_313_1_190 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (154) with all_0_3_3, all_313_1_190, 0 and discharging atoms aSet0(all_0_3_3) = all_313_1_190, aSet0(all_0_3_3) = 0, yields: % 145.78/109.41 | (307) all_313_1_190 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (307) can reduce 390 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (394) ~ (all_313_1_190 = 0) & aElement0(xx) = all_313_1_190 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (394) yields: % 145.78/109.41 | (390) ~ (all_313_1_190 = 0) % 145.78/109.41 | (396) aElement0(xx) = all_313_1_190 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (49) with xx, all_313_1_190, 0 and discharging atoms aElement0(xx) = all_313_1_190, aElement0(xx) = 0, yields: % 145.78/109.41 | (307) all_313_1_190 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (307) can reduce 390 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (464) ~ (all_65_1_76 = 0) & aElementOf0(all_0_0_0, szNzAzT0) = all_65_1_76 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (464) yields: % 145.78/109.41 | (209) ~ (all_65_1_76 = 0) % 145.78/109.41 | (466) aElementOf0(all_0_0_0, szNzAzT0) = all_65_1_76 % 145.78/109.41 | % 145.78/109.41 | Equations (211) can reduce 209 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (468) ~ (all_65_0_75 = 0) & isFinite0(xS) = all_65_0_75 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (468) yields: % 145.78/109.41 | (469) ~ (all_65_0_75 = 0) % 145.78/109.41 | (470) isFinite0(xS) = all_65_0_75 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (59) with xS, all_65_0_75, 0 and discharging atoms isFinite0(xS) = all_65_0_75, isFinite0(xS) = 0, yields: % 145.78/109.41 | (257) all_65_0_75 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (257) can reduce 469 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (239) ~ (all_79_1_90 = 0) & sbrdtbr0(xS) = all_79_2_91 & aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (239) yields: % 145.78/109.41 | (240) ~ (all_79_1_90 = 0) % 145.78/109.41 | (229) sbrdtbr0(xS) = all_79_2_91 % 145.78/109.41 | (242) aElementOf0(all_79_2_91, szNzAzT0) = all_79_1_90 % 145.78/109.41 | % 145.78/109.41 | Equations (228) can reduce 240 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (478) ~ (all_79_0_89 = 0) & isFinite0(xS) = all_79_0_89 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (478) yields: % 145.78/109.41 | (479) ~ (all_79_0_89 = 0) % 145.78/109.41 | (480) isFinite0(xS) = all_79_0_89 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (59) with xS, all_79_0_89, 0 and discharging atoms isFinite0(xS) = all_79_0_89, isFinite0(xS) = 0, yields: % 145.78/109.41 | (235) all_79_0_89 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (235) can reduce 479 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (483) all_91_2_108 = 0 & aSubsetOf0(xS, all_0_3_3) = 0 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (483) yields: % 145.78/109.41 | (484) all_91_2_108 = 0 % 145.78/109.41 | (485) aSubsetOf0(xS, all_0_3_3) = 0 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (28) with xS, all_0_3_3, 0, all_46_0_53 and discharging atoms aSubsetOf0(xS, all_0_3_3) = all_46_0_53, aSubsetOf0(xS, all_0_3_3) = 0, yields: % 145.78/109.41 | (197) all_46_0_53 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (197) can reduce 201 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 |-Branch two: % 145.78/109.41 | (488) ~ (all_75_1_85 = 0) & aSet0(xS) = all_75_1_85 % 145.78/109.41 | % 145.78/109.41 | Applying alpha-rule on (488) yields: % 145.78/109.41 | (489) ~ (all_75_1_85 = 0) % 145.78/109.41 | (490) aSet0(xS) = all_75_1_85 % 145.78/109.41 | % 145.78/109.41 | Instantiating formula (154) with xS, all_75_1_85, 0 and discharging atoms aSet0(xS) = all_75_1_85, aSet0(xS) = 0, yields: % 145.78/109.41 | (491) all_75_1_85 = 0 % 145.78/109.41 | % 145.78/109.41 | Equations (491) can reduce 489 to: % 145.78/109.41 | (212) $false % 145.78/109.41 | % 145.78/109.41 |-The branch is then unsatisfiable % 145.78/109.41 % SZS output end Proof for theBenchmark % 145.78/109.41 % 145.78/109.41 108781ms %------------------------------------------------------------------------------