%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS149+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n027.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 : Sun Jul 17 02:56:42 EDT 2022 % Result : Theorem 24.37s 6.76s % Output : Proof 27.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS149+1 : TPTP v8.1.0. Released v3.1.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.34 % Computer : n027.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jun 7 09:09:25 EDT 2022 % 0.14/0.34 % CPUTime : % 0.52/0.61 ____ _ % 0.52/0.61 ___ / __ \_____(_)___ ________ __________ % 0.52/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.52/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.52/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.52/0.61 % 0.52/0.61 A Theorem Prover for First-Order Logic % 0.52/0.61 (ePrincess v.1.0) % 0.52/0.61 % 0.52/0.61 (c) Philipp Rümmer, 2009-2015 % 0.52/0.61 (c) Peter Backeman, 2014-2015 % 0.52/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.52/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.52/0.61 Bug reports to peter@backeman.se % 0.52/0.61 % 0.52/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.52/0.61 % 0.52/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.75/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.15/1.11 Prover 0: Preprocessing ... % 3.73/1.47 Prover 0: Warning: ignoring some quantifiers % 3.87/1.51 Prover 0: Constructing countermodel ... % 20.80/5.95 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 21.35/6.08 Prover 1: Preprocessing ... % 23.60/6.65 Prover 1: Constructing countermodel ... % 24.37/6.75 Prover 1: proved (799ms) % 24.37/6.76 Prover 0: stopped % 24.37/6.76 % 24.37/6.76 No countermodel exists, formula is valid % 24.37/6.76 % SZS status Theorem for theBenchmark % 24.37/6.76 % 24.37/6.76 Generating proof ... found it (size 107) % 26.50/7.23 % 26.50/7.23 % SZS output start Proof for theBenchmark % 26.50/7.23 Assumed formulas after preprocessing and simplification: % 26.50/7.23 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ( ~ (v8 = 0) & ~ (v7 = 0) & ~ (v6 = 0) & ~ (v5 = 0) & ~ (v4 = 0) & ~ (v3 = 0) & ~ (v2 = 0) & ~ (v1 = 0) & ~ (v0 = 0) & cTEST(iV3102) = 0 & cTOP(iV3102) = 0 & cC62(iV3102) = v4 & cC46(iV3102) = v10 & cC44(iV3102) = v12 & cC42(iV3102) = v0 & cC32(iV3102) = v7 & cC30(iV3102) = v11 & cC28(iV3102) = v13 & cC26(iV3102) = v2 & cC64(iV3102) = v14 & cC216(iV3102) = v9 & cC214(iV3102) = v3 & cC14(iV3102) = v15 & cC12(iV3102) = v1 & cC16(iV3102) = v5 & cC100(iV3102) = v8 & cC2(iV3102) = v6 & cowlThing(iV3102) = 0 & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC86(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC74(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC66(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC50(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC48(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC4(v19) = v20) | ~ (cC2(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC34(v19) = v20) | ~ (cC32(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC192(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC180(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC18(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC172(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC170(v19) = v20) | ~ (cC168(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC156(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC144(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC136(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC122(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC110(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC102(v19) = v20) | ~ (cC16(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v22 = 0 | v20 = 0 | ~ (cC100(v19) = v20) | ~ (cC98(v21) = v22) | ? [v23] : ( ~ (v23 = 0) & rR1(v19, v21) = v23)) & ! [v19] : ! [v20] : ! [v21] : ! [v22] : (v20 = v19 | ~ (rR1(v22, v21) = v20) | ~ (rR1(v22, v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cTEST(v21) = v20) | ~ (cTEST(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC96(v21) = v20) | ~ (cC96(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC94(v21) = v20) | ~ (cC94(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC92(v21) = v20) | ~ (cC92(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC90(v21) = v20) | ~ (cC90(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC88(v21) = v20) | ~ (cC88(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC86(v21) = v20) | ~ (cC86(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC84(v21) = v20) | ~ (cC84(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC82(v21) = v20) | ~ (cC82(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC80(v21) = v20) | ~ (cC80(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC78(v21) = v20) | ~ (cC78(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC76(v21) = v20) | ~ (cC76(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC74(v21) = v20) | ~ (cC74(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC72(v21) = v20) | ~ (cC72(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC70(v21) = v20) | ~ (cC70(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC68(v21) = v20) | ~ (cC68(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC66(v21) = v20) | ~ (cC66(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cTOP(v21) = v20) | ~ (cTOP(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC62(v21) = v20) | ~ (cC62(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC60(v21) = v20) | ~ (cC60(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC6(v21) = v20) | ~ (cC6(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC58(v21) = v20) | ~ (cC58(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC56(v21) = v20) | ~ (cC56(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC54(v21) = v20) | ~ (cC54(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC52(v21) = v20) | ~ (cC52(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC50(v21) = v20) | ~ (cC50(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC48(v21) = v20) | ~ (cC48(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC46(v21) = v20) | ~ (cC46(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC44(v21) = v20) | ~ (cC44(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC42(v21) = v20) | ~ (cC42(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC40(v21) = v20) | ~ (cC40(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC4(v21) = v20) | ~ (cC4(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC38(v21) = v20) | ~ (cC38(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC36(v21) = v20) | ~ (cC36(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC34(v21) = v20) | ~ (cC34(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC32(v21) = v20) | ~ (cC32(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC30(v21) = v20) | ~ (cC30(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC28(v21) = v20) | ~ (cC28(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC26(v21) = v20) | ~ (cC26(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC24(v21) = v20) | ~ (cC24(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC22(v21) = v20) | ~ (cC22(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC64(v21) = v20) | ~ (cC64(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC216(v21) = v20) | ~ (cC216(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC214(v21) = v20) | ~ (cC214(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC212(v21) = v20) | ~ (cC212(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC210(v21) = v20) | ~ (cC210(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC208(v21) = v20) | ~ (cC208(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC206(v21) = v20) | ~ (cC206(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC204(v21) = v20) | ~ (cC204(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC202(v21) = v20) | ~ (cC202(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC200(v21) = v20) | ~ (cC200(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC20(v21) = v20) | ~ (cC20(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC198(v21) = v20) | ~ (cC198(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC196(v21) = v20) | ~ (cC196(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC194(v21) = v20) | ~ (cC194(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC192(v21) = v20) | ~ (cC192(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC190(v21) = v20) | ~ (cC190(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC188(v21) = v20) | ~ (cC188(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC186(v21) = v20) | ~ (cC186(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC184(v21) = v20) | ~ (cC184(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC182(v21) = v20) | ~ (cC182(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC180(v21) = v20) | ~ (cC180(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC18(v21) = v20) | ~ (cC18(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC178(v21) = v20) | ~ (cC178(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC176(v21) = v20) | ~ (cC176(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC174(v21) = v20) | ~ (cC174(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC172(v21) = v20) | ~ (cC172(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC170(v21) = v20) | ~ (cC170(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC168(v21) = v20) | ~ (cC168(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC166(v21) = v20) | ~ (cC166(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC164(v21) = v20) | ~ (cC164(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC162(v21) = v20) | ~ (cC162(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC160(v21) = v20) | ~ (cC160(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC158(v21) = v20) | ~ (cC158(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC156(v21) = v20) | ~ (cC156(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC154(v21) = v20) | ~ (cC154(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC152(v21) = v20) | ~ (cC152(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC150(v21) = v20) | ~ (cC150(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC148(v21) = v20) | ~ (cC148(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC146(v21) = v20) | ~ (cC146(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC144(v21) = v20) | ~ (cC144(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC142(v21) = v20) | ~ (cC142(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC140(v21) = v20) | ~ (cC140(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC14(v21) = v20) | ~ (cC14(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC138(v21) = v20) | ~ (cC138(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC136(v21) = v20) | ~ (cC136(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC134(v21) = v20) | ~ (cC134(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC132(v21) = v20) | ~ (cC132(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC130(v21) = v20) | ~ (cC130(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC128(v21) = v20) | ~ (cC128(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC126(v21) = v20) | ~ (cC126(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC124(v21) = v20) | ~ (cC124(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC122(v21) = v20) | ~ (cC122(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC120(v21) = v20) | ~ (cC120(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC12(v21) = v20) | ~ (cC12(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC118(v21) = v20) | ~ (cC118(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC116(v21) = v20) | ~ (cC116(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC114(v21) = v20) | ~ (cC114(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC112(v21) = v20) | ~ (cC112(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC110(v21) = v20) | ~ (cC110(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC108(v21) = v20) | ~ (cC108(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC106(v21) = v20) | ~ (cC106(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC104(v21) = v20) | ~ (cC104(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC102(v21) = v20) | ~ (cC102(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC16(v21) = v20) | ~ (cC16(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC100(v21) = v20) | ~ (cC100(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC98(v21) = v20) | ~ (cC98(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC8(v21) = v20) | ~ (cC8(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC10(v21) = v20) | ~ (cC10(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cC2(v21) = v20) | ~ (cC2(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (xsd_string(v21) = v20) | ~ (xsd_string(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (xsd_integer(v21) = v20) | ~ (xsd_integer(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cowlNothing(v21) = v20) | ~ (cowlNothing(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = v19 | ~ (cowlThing(v21) = v20) | ~ (cowlThing(v21) = v19)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC94(v19) = v20) | ~ (cC92(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC90(v19) = v20) | ~ (cC88(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC84(v19) = v20) | ~ (cC82(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC82(v19) = v20) | ~ (cC80(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC78(v19) = v20) | ~ (cC76(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC70(v19) = v20) | ~ (cC68(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC62(v19) = v20) | ~ (cC60(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC6(v21) = 0) | ~ (cC8(v19) = v20) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC58(v19) = v20) | ~ (cC56(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC54(v19) = v20) | ~ (cC52(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC42(v19) = v20) | ~ (cC40(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC38(v19) = v20) | ~ (cC36(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC26(v19) = v20) | ~ (cC24(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC22(v19) = v20) | ~ (cC20(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC212(v19) = v20) | ~ (cC210(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC208(v19) = v20) | ~ (cC206(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC200(v19) = v20) | ~ (cC198(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC196(v19) = v20) | ~ (cC194(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC190(v19) = v20) | ~ (cC188(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC188(v19) = v20) | ~ (cC186(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC184(v19) = v20) | ~ (cC182(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC176(v19) = v20) | ~ (cC174(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC164(v19) = v20) | ~ (cC162(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC160(v19) = v20) | ~ (cC158(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC154(v19) = v20) | ~ (cC152(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC152(v19) = v20) | ~ (cC150(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC148(v19) = v20) | ~ (cC146(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC140(v19) = v20) | ~ (cC138(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC130(v19) = v20) | ~ (cC128(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC126(v19) = v20) | ~ (cC124(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC120(v19) = v20) | ~ (cC118(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC12(v19) = v20) | ~ (cC10(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC118(v19) = v20) | ~ (cC116(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC114(v19) = v20) | ~ (cC112(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : ! [v21] : (v20 = 0 | ~ (cC106(v19) = v20) | ~ (cC104(v21) = 0) | ? [v22] : ( ~ (v22 = 0) & rR1(v19, v21) = v22)) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cTEST(v19) = v20) | ? [v21] : ? [v22] : (cC46(v19) = v22 & cC216(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC96(v19) = v20) | ? [v21] : ? [v22] : (cC94(v19) = v22 & cC84(v19) = v21 & ( ~ (v21 = 0) | v22 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC96(v19) = v20) | ? [v21] : ? [v22] : (cC72(v19) = v21 & cC98(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC92(v19) = v20) | ? [v21] : ? [v22] : (cC90(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC88(v19) = v20) | ? [v21] : ? [v22] : (cC86(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC80(v19) = v20) | ? [v21] : ? [v22] : (cC78(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC76(v19) = v20) | ? [v21] : ? [v22] : (cC74(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC72(v19) = v20) | ? [v21] : ? [v22] : (cC70(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC68(v19) = v20) | ? [v21] : ? [v22] : (cC66(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC6(v19) = v20) | ? [v21] : ? [v22] : (cC4(v19) = v22 & cC2(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC58(v19) = v20) | ? [v21] : ? [v22] : (cC60(v19) = v22 & cC48(v19) = v21 & ( ~ (v21 = 0) | v22 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC56(v19) = v20) | ? [v21] : ? [v22] : (cC54(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC52(v19) = v20) | ? [v21] : ? [v22] : (cC50(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC46(v19) = v20) | ? [v21] : ? [v22] : (cC44(v19) = v22 & cC30(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC44(v19) = v20) | ? [v21] : ? [v22] : (cC42(v19) = v22 & cC32(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC38(v19) = v20) | ? [v21] : ? [v22] : (cC40(v19) = v22 & cC32(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC36(v19) = v20) | ? [v21] : ? [v22] : (cC34(v19) = v22 & cC32(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC30(v19) = v20) | ? [v21] : ? [v22] : (cC28(v19) = v22 & cC14(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC28(v19) = v20) | ? [v21] : ? [v22] : (cC26(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC22(v19) = v20) | ? [v21] : ? [v22] : (cC24(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC212(v19) = v20) | ? [v21] : ? [v22] : (cC214(v19) = v22 & cC100(v19) = v21 & ( ~ (v21 = 0) | v22 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC210(v19) = v20) | ? [v21] : ? [v22] : (cC208(v19) = v21 & cC134(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC206(v19) = v20) | ? [v21] : ? [v22] : (cC204(v19) = v22 & cC170(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC204(v19) = v20) | ? [v21] : ? [v22] : (cC202(v19) = v22 & cC178(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC202(v19) = v20) | ? [v21] : ? [v22] : (cC200(v19) = v22 & cC190(v19) = v21 & ( ~ (v21 = 0) | v22 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC20(v19) = v20) | ? [v21] : ? [v22] : (cC18(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC198(v19) = v20) | ? [v21] : ? [v22] : (cC196(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC194(v19) = v20) | ? [v21] : ? [v22] : (cC192(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC186(v19) = v20) | ? [v21] : ? [v22] : (cC184(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC182(v19) = v20) | ? [v21] : ? [v22] : (cC180(v19) = v22 & cC16(v19) = v21 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC178(v19) = v20) | ? [v21] : ? [v22] : (cC176(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC174(v19) = v20) | ? [v21] : ? [v22] : (cC172(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC168(v19) = v20) | ? [v21] : ? [v22] : (cC166(v19) = v21 & cC142(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC166(v19) = v20) | ? [v21] : ? [v22] : (cC164(v19) = v22 & cC154(v19) = v21 & ( ~ (v21 = 0) | v22 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC162(v19) = v20) | ? [v21] : ? [v22] : (cC160(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC158(v19) = v20) | ? [v21] : ? [v22] : (cC156(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC150(v19) = v20) | ? [v21] : ? [v22] : (cC148(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC146(v19) = v20) | ? [v21] : ? [v22] : (cC144(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC142(v19) = v20) | ? [v21] : ? [v22] : (cC140(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC14(v19) = v20) | ? [v21] : ? [v22] : (cC12(v19) = v21 & cC2(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC138(v19) = v20) | ? [v21] : ? [v22] : (cC136(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC134(v19) = v20) | ? [v21] : ? [v22] : (cC132(v19) = v21 & cC108(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC132(v19) = v20) | ? [v21] : ? [v22] : (cC130(v19) = v21 & cC120(v19) = v22 & ( ~ (v22 = 0) | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC128(v19) = v20) | ? [v21] : ? [v22] : (cC126(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC124(v19) = v20) | ? [v21] : ? [v22] : (cC122(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC116(v19) = v20) | ? [v21] : ? [v22] : (cC114(v19) = v22 & cC16(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC112(v19) = v20) | ? [v21] : ? [v22] : (cC110(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC108(v19) = v20) | ? [v21] : ? [v22] : (cC106(v19) = v21 & cC16(v19) = v22 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC104(v19) = v20) | ? [v21] : ? [v22] : (cC102(v19) = v21 & cC16(v19) = v22 & ( ~ (v22 = 0) | ~ (v21 = 0)))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cC8(v19) = v20) | ? [v21] : ? [v22] : (cC10(v19) = v22 & cC2(v19) = v21 & (v22 = 0 | v21 = 0))) & ! [v19] : ! [v20] : (v20 = 0 | ~ (xsd_string(v19) = v20) | xsd_integer(v19) = 0) & ! [v19] : ! [v20] : (v20 = 0 | ~ (cowlThing(v19) = v20)) & ! [v19] : ! [v20] : ( ~ (cC96(v19) = v20) | ? [v21] : ? [v22] : (cC72(v19) = v22 & cC98(v19) = v21 & ( ~ (v21 = 0) | ( ~ (v22 = 0) & ~ (v20 = 0))))) & ! [v19] : ! [v20] : ( ~ (cTOP(v19) = v20) | ? [v21] : ? [v22] : (cC62(v19) = v22 & cC64(v19) = v21 & ( ~ (v21 = 0) | (v20 = 0 & ~ (v22 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC58(v19) = v20) | ? [v21] : ? [v22] : (cC60(v19) = v21 & cC48(v19) = v22 & ( ~ (v21 = 0) | (v22 = 0 & ~ (v20 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC38(v19) = v20) | ? [v21] : ? [v22] : (cC40(v19) = v21 & cC32(v19) = v22 & ( ~ (v21 = 0) | ( ~ (v22 = 0) & ~ (v20 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC22(v19) = v20) | ? [v21] : ? [v22] : (cC24(v19) = v21 & cC16(v19) = v22 & ( ~ (v21 = 0) | ( ~ (v22 = 0) & ~ (v20 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC64(v19) = v20) | ? [v21] : ? [v22] : (cC216(v19) = v21 & cC214(v19) = v22 & ( ~ (v21 = 0) | (v20 = 0 & ~ (v22 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC212(v19) = v20) | ? [v21] : ? [v22] : (cC214(v19) = v21 & cC100(v19) = v22 & ( ~ (v21 = 0) | (v22 = 0 & ~ (v20 = 0))))) & ! [v19] : ! [v20] : ( ~ (cC8(v19) = v20) | ? [v21] : ? [v22] : (cC10(v19) = v21 & cC2(v19) = v22 & ( ~ (v21 = 0) | ( ~ (v22 = 0) & ~ (v20 = 0))))) & ! [v19] : ( ~ (cTEST(v19) = 0) | (cC46(v19) = 0 & cC216(v19) = 0)) & ! [v19] : ( ~ (cC96(v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC94(v19) = v20 & cC84(v19) = 0)) & ! [v19] : ( ~ (cC94(v19) = 0) | ? [v20] : (cC92(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC92(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC90(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC90(v19) = 0) | ? [v20] : (cC88(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC88(v19) = 0) | (cC86(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC86(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC84(v19) = 0) | ? [v20] : (cC82(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC82(v19) = 0) | ? [v20] : (cC80(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC80(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC78(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC78(v19) = 0) | ? [v20] : (cC76(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC76(v19) = 0) | (cC74(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC74(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC72(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC70(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC70(v19) = 0) | ? [v20] : (cC68(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC68(v19) = 0) | (cC66(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC66(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cTOP(v19) = 0) | ? [v20] : ? [v21] : (cC62(v19) = v20 & cC64(v19) = v21 & (v21 = 0 | v20 = 0))) & ! [v19] : ( ~ (cC62(v19) = 0) | ? [v20] : (cC60(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC6(v19) = 0) | (cC4(v19) = 0 & cC2(v19) = 0)) & ! [v19] : ( ~ (cC58(v19) = 0) | ? [v20] : (cC56(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC56(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC54(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC54(v19) = 0) | ? [v20] : (cC52(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC52(v19) = 0) | (cC50(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC50(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC48(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC46(v19) = 0) | (cC44(v19) = 0 & cC30(v19) = 0)) & ! [v19] : ( ~ (cC44(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC42(v19) = v21 & cC32(v19) = v20)) & ! [v19] : ( ~ (cC42(v19) = 0) | ? [v20] : (cC40(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC4(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & rR1(v19, v20) = 0 & cC2(v20) = v21)) & ! [v19] : ( ~ (cC38(v19) = 0) | ? [v20] : (cC36(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC36(v19) = 0) | (cC34(v19) = 0 & cC32(v19) = 0)) & ! [v19] : ( ~ (cC34(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC32(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC30(v19) = 0) | (cC28(v19) = 0 & cC14(v19) = 0)) & ! [v19] : ( ~ (cC28(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC26(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC26(v19) = 0) | ? [v20] : (cC24(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC22(v19) = 0) | ? [v20] : (cC20(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC64(v19) = 0) | ? [v20] : ? [v21] : (cC216(v19) = v21 & cC214(v19) = v20 & (v21 = 0 | v20 = 0))) & ! [v19] : ( ~ (cC212(v19) = 0) | ? [v20] : (cC210(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC210(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC208(v19) = v20 & cC134(v19) = v21)) & ! [v19] : ( ~ (cC208(v19) = 0) | ? [v20] : (cC206(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC206(v19) = 0) | (cC204(v19) = 0 & cC170(v19) = 0)) & ! [v19] : ( ~ (cC204(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC202(v19) = v21 & cC178(v19) = v20)) & ! [v19] : ( ~ (cC202(v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC200(v19) = v20 & cC190(v19) = 0)) & ! [v19] : ( ~ (cC200(v19) = 0) | ? [v20] : (cC198(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC20(v19) = 0) | (cC18(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC198(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC196(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC196(v19) = 0) | ? [v20] : (cC194(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC194(v19) = 0) | (cC192(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC192(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC190(v19) = 0) | ? [v20] : (cC188(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC188(v19) = 0) | ? [v20] : (cC186(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC186(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC184(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC184(v19) = 0) | ? [v20] : (cC182(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC182(v19) = 0) | (cC180(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC180(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC18(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC178(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC176(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC176(v19) = 0) | ? [v20] : (cC174(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC174(v19) = 0) | (cC172(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC172(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC170(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC168(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC168(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC166(v19) = v20 & cC142(v19) = v21)) & ! [v19] : ( ~ (cC166(v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC164(v19) = v20 & cC154(v19) = 0)) & ! [v19] : ( ~ (cC164(v19) = 0) | ? [v20] : (cC162(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC162(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC160(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC160(v19) = 0) | ? [v20] : (cC158(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC158(v19) = 0) | (cC156(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC156(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC154(v19) = 0) | ? [v20] : (cC152(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC152(v19) = 0) | ? [v20] : (cC150(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC150(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC148(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC148(v19) = 0) | ? [v20] : (cC146(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC146(v19) = 0) | (cC144(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC144(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC142(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC140(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC140(v19) = 0) | ? [v20] : (cC138(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC14(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC12(v19) = v20 & cC2(v19) = v21)) & ! [v19] : ( ~ (cC138(v19) = 0) | (cC136(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC136(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC134(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC132(v19) = v20 & cC108(v19) = v21)) & ! [v19] : ( ~ (cC132(v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC130(v19) = v20 & cC120(v19) = 0)) & ! [v19] : ( ~ (cC130(v19) = 0) | ? [v20] : (cC128(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC128(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC126(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC126(v19) = 0) | ? [v20] : (cC124(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC124(v19) = 0) | (cC122(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC122(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC120(v19) = 0) | ? [v20] : (cC118(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC12(v19) = 0) | ? [v20] : (rR1(v19, v20) = 0 & cC10(v20) = 0)) & ! [v19] : ( ~ (cC118(v19) = 0) | ? [v20] : (cC116(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC116(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC114(v19) = v21 & cC16(v19) = v20)) & ! [v19] : ( ~ (cC114(v19) = 0) | ? [v20] : (cC112(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC112(v19) = 0) | (cC110(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC110(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC108(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & ~ (v20 = 0) & cC106(v19) = v20 & cC16(v19) = v21)) & ! [v19] : ( ~ (cC106(v19) = 0) | ? [v20] : (cC104(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC104(v19) = 0) | (cC102(v19) = 0 & cC16(v19) = 0)) & ! [v19] : ( ~ (cC102(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & cC16(v20) = v21 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (cC100(v19) = 0) | ? [v20] : ? [v21] : ( ~ (v21 = 0) & rR1(v19, v20) = 0 & cC98(v20) = v21)) & ! [v19] : ( ~ (rR1(iV3102, v19) = 0) | cC98(v19) = 0) & ! [v19] : ( ~ (rR1(iV3102, v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC60(v19) = v20)) & ! [v19] : ( ~ (rR1(iV3102, v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC40(v19) = v20)) & ! [v19] : ( ~ (rR1(iV3102, v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC24(v19) = v20)) & ! [v19] : ( ~ (rR1(iV3102, v19) = 0) | ? [v20] : ( ~ (v20 = 0) & cC10(v19) = v20)) & ! [v19] : ( ~ (cC8(v19) = 0) | ? [v20] : (cC6(v20) = 0 & rR1(v19, v20) = 0)) & ! [v19] : ( ~ (xsd_string(v19) = 0) | ? [v20] : ( ~ (v20 = 0) & xsd_integer(v19) = v20)) & ! [v19] : ~ (cowlNothing(v19) = 0) & ( ~ (v15 = 0) | ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | (xsd_string(v16) = v17 & xsd_integer(v16) = v18 & ((v18 = 0 & v17 = 0) | ( ~ (v18 = 0) & ~ (v17 = 0)))) | (cowlNothing(v16) = v18 & cowlThing(v16) = v17 & ( ~ (v17 = 0) | v18 = 0)))) % 27.17/7.33 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18 yields: % 27.17/7.33 | (1) ~ (all_0_10_10 = 0) & ~ (all_0_11_11 = 0) & ~ (all_0_12_12 = 0) & ~ (all_0_13_13 = 0) & ~ (all_0_14_14 = 0) & ~ (all_0_15_15 = 0) & ~ (all_0_16_16 = 0) & ~ (all_0_17_17 = 0) & ~ (all_0_18_18 = 0) & cTEST(iV3102) = 0 & cTOP(iV3102) = 0 & cC62(iV3102) = all_0_14_14 & cC46(iV3102) = all_0_8_8 & cC44(iV3102) = all_0_6_6 & cC42(iV3102) = all_0_18_18 & cC32(iV3102) = all_0_11_11 & cC30(iV3102) = all_0_7_7 & cC28(iV3102) = all_0_5_5 & cC26(iV3102) = all_0_16_16 & cC64(iV3102) = all_0_4_4 & cC216(iV3102) = all_0_9_9 & cC214(iV3102) = all_0_15_15 & cC14(iV3102) = all_0_3_3 & cC12(iV3102) = all_0_17_17 & cC16(iV3102) = all_0_13_13 & cC100(iV3102) = all_0_10_10 & cC2(iV3102) = all_0_12_12 & cowlThing(iV3102) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC86(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC74(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC66(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC50(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC48(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC4(v0) = v1) | ~ (cC2(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC34(v0) = v1) | ~ (cC32(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC192(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC180(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC18(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC172(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC170(v0) = v1) | ~ (cC168(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC156(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC144(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC136(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC122(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC110(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC102(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC100(v0) = v1) | ~ (cC98(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (rR1(v3, v2) = v1) | ~ (rR1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC96(v2) = v1) | ~ (cC96(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC94(v2) = v1) | ~ (cC94(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC92(v2) = v1) | ~ (cC92(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC90(v2) = v1) | ~ (cC90(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC88(v2) = v1) | ~ (cC88(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC86(v2) = v1) | ~ (cC86(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC84(v2) = v1) | ~ (cC84(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC82(v2) = v1) | ~ (cC82(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC80(v2) = v1) | ~ (cC80(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC78(v2) = v1) | ~ (cC78(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC76(v2) = v1) | ~ (cC76(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC74(v2) = v1) | ~ (cC74(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC72(v2) = v1) | ~ (cC72(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC70(v2) = v1) | ~ (cC70(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC68(v2) = v1) | ~ (cC68(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC66(v2) = v1) | ~ (cC66(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTOP(v2) = v1) | ~ (cTOP(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC62(v2) = v1) | ~ (cC62(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC60(v2) = v1) | ~ (cC60(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC6(v2) = v1) | ~ (cC6(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC58(v2) = v1) | ~ (cC58(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC56(v2) = v1) | ~ (cC56(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC54(v2) = v1) | ~ (cC54(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC52(v2) = v1) | ~ (cC52(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC50(v2) = v1) | ~ (cC50(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC48(v2) = v1) | ~ (cC48(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC46(v2) = v1) | ~ (cC46(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC44(v2) = v1) | ~ (cC44(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC42(v2) = v1) | ~ (cC42(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC40(v2) = v1) | ~ (cC40(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC38(v2) = v1) | ~ (cC38(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC36(v2) = v1) | ~ (cC36(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC34(v2) = v1) | ~ (cC34(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC32(v2) = v1) | ~ (cC32(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC30(v2) = v1) | ~ (cC30(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC28(v2) = v1) | ~ (cC28(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC26(v2) = v1) | ~ (cC26(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC24(v2) = v1) | ~ (cC24(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC22(v2) = v1) | ~ (cC22(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC214(v2) = v1) | ~ (cC214(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC212(v2) = v1) | ~ (cC212(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC210(v2) = v1) | ~ (cC210(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC208(v2) = v1) | ~ (cC208(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC206(v2) = v1) | ~ (cC206(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC204(v2) = v1) | ~ (cC204(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC202(v2) = v1) | ~ (cC202(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC200(v2) = v1) | ~ (cC200(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC20(v2) = v1) | ~ (cC20(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC198(v2) = v1) | ~ (cC198(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC196(v2) = v1) | ~ (cC196(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC194(v2) = v1) | ~ (cC194(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC192(v2) = v1) | ~ (cC192(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC190(v2) = v1) | ~ (cC190(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC188(v2) = v1) | ~ (cC188(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC186(v2) = v1) | ~ (cC186(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC184(v2) = v1) | ~ (cC184(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC182(v2) = v1) | ~ (cC182(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC180(v2) = v1) | ~ (cC180(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC178(v2) = v1) | ~ (cC178(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC176(v2) = v1) | ~ (cC176(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC174(v2) = v1) | ~ (cC174(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC172(v2) = v1) | ~ (cC172(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC170(v2) = v1) | ~ (cC170(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC168(v2) = v1) | ~ (cC168(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC166(v2) = v1) | ~ (cC166(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC164(v2) = v1) | ~ (cC164(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC162(v2) = v1) | ~ (cC162(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC160(v2) = v1) | ~ (cC160(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC158(v2) = v1) | ~ (cC158(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC156(v2) = v1) | ~ (cC156(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC154(v2) = v1) | ~ (cC154(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC152(v2) = v1) | ~ (cC152(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC150(v2) = v1) | ~ (cC150(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC148(v2) = v1) | ~ (cC148(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC146(v2) = v1) | ~ (cC146(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC144(v2) = v1) | ~ (cC144(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC142(v2) = v1) | ~ (cC142(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC140(v2) = v1) | ~ (cC140(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC138(v2) = v1) | ~ (cC138(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC136(v2) = v1) | ~ (cC136(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC134(v2) = v1) | ~ (cC134(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC132(v2) = v1) | ~ (cC132(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC130(v2) = v1) | ~ (cC130(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC128(v2) = v1) | ~ (cC128(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC126(v2) = v1) | ~ (cC126(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC124(v2) = v1) | ~ (cC124(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC122(v2) = v1) | ~ (cC122(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC120(v2) = v1) | ~ (cC120(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC12(v2) = v1) | ~ (cC12(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC118(v2) = v1) | ~ (cC118(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC116(v2) = v1) | ~ (cC116(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC114(v2) = v1) | ~ (cC114(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC112(v2) = v1) | ~ (cC112(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC110(v2) = v1) | ~ (cC110(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC108(v2) = v1) | ~ (cC108(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC106(v2) = v1) | ~ (cC106(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC104(v2) = v1) | ~ (cC104(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC102(v2) = v1) | ~ (cC102(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC100(v2) = v1) | ~ (cC100(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC98(v2) = v1) | ~ (cC98(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC8(v2) = v1) | ~ (cC8(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC10(v2) = v1) | ~ (cC10(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC94(v0) = v1) | ~ (cC92(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC90(v0) = v1) | ~ (cC88(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC84(v0) = v1) | ~ (cC82(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC82(v0) = v1) | ~ (cC80(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC78(v0) = v1) | ~ (cC76(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC70(v0) = v1) | ~ (cC68(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC62(v0) = v1) | ~ (cC60(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC6(v2) = 0) | ~ (cC8(v0) = v1) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC58(v0) = v1) | ~ (cC56(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC54(v0) = v1) | ~ (cC52(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC42(v0) = v1) | ~ (cC40(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC38(v0) = v1) | ~ (cC36(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC26(v0) = v1) | ~ (cC24(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC22(v0) = v1) | ~ (cC20(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC212(v0) = v1) | ~ (cC210(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC208(v0) = v1) | ~ (cC206(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC200(v0) = v1) | ~ (cC198(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC196(v0) = v1) | ~ (cC194(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC190(v0) = v1) | ~ (cC188(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC188(v0) = v1) | ~ (cC186(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC184(v0) = v1) | ~ (cC182(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC176(v0) = v1) | ~ (cC174(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC164(v0) = v1) | ~ (cC162(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC160(v0) = v1) | ~ (cC158(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC154(v0) = v1) | ~ (cC152(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC152(v0) = v1) | ~ (cC150(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC148(v0) = v1) | ~ (cC146(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC140(v0) = v1) | ~ (cC138(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC130(v0) = v1) | ~ (cC128(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC126(v0) = v1) | ~ (cC124(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC120(v0) = v1) | ~ (cC118(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ (cC10(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC118(v0) = v1) | ~ (cC116(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC114(v0) = v1) | ~ (cC112(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC106(v0) = v1) | ~ (cC104(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cTEST(v0) = v1) | ? [v2] : ? [v3] : (cC46(v0) = v3 & cC216(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC94(v0) = v3 & cC84(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC72(v0) = v2 & cC98(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC92(v0) = v1) | ? [v2] : ? [v3] : (cC90(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC88(v0) = v1) | ? [v2] : ? [v3] : (cC86(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC80(v0) = v1) | ? [v2] : ? [v3] : (cC78(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC76(v0) = v1) | ? [v2] : ? [v3] : (cC74(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC72(v0) = v1) | ? [v2] : ? [v3] : (cC70(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC68(v0) = v1) | ? [v2] : ? [v3] : (cC66(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC6(v0) = v1) | ? [v2] : ? [v3] : (cC4(v0) = v3 & cC2(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC58(v0) = v1) | ? [v2] : ? [v3] : (cC60(v0) = v3 & cC48(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC56(v0) = v1) | ? [v2] : ? [v3] : (cC54(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC52(v0) = v1) | ? [v2] : ? [v3] : (cC50(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC46(v0) = v1) | ? [v2] : ? [v3] : (cC44(v0) = v3 & cC30(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC44(v0) = v1) | ? [v2] : ? [v3] : (cC42(v0) = v3 & cC32(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC38(v0) = v1) | ? [v2] : ? [v3] : (cC40(v0) = v3 & cC32(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC36(v0) = v1) | ? [v2] : ? [v3] : (cC34(v0) = v3 & cC32(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC30(v0) = v1) | ? [v2] : ? [v3] : (cC28(v0) = v3 & cC14(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC28(v0) = v1) | ? [v2] : ? [v3] : (cC26(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC22(v0) = v1) | ? [v2] : ? [v3] : (cC24(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC212(v0) = v1) | ? [v2] : ? [v3] : (cC214(v0) = v3 & cC100(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC210(v0) = v1) | ? [v2] : ? [v3] : (cC208(v0) = v2 & cC134(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC206(v0) = v1) | ? [v2] : ? [v3] : (cC204(v0) = v3 & cC170(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC204(v0) = v1) | ? [v2] : ? [v3] : (cC202(v0) = v3 & cC178(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC202(v0) = v1) | ? [v2] : ? [v3] : (cC200(v0) = v3 & cC190(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC20(v0) = v1) | ? [v2] : ? [v3] : (cC18(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC198(v0) = v1) | ? [v2] : ? [v3] : (cC196(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC194(v0) = v1) | ? [v2] : ? [v3] : (cC192(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC186(v0) = v1) | ? [v2] : ? [v3] : (cC184(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC182(v0) = v1) | ? [v2] : ? [v3] : (cC180(v0) = v3 & cC16(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC178(v0) = v1) | ? [v2] : ? [v3] : (cC176(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC174(v0) = v1) | ? [v2] : ? [v3] : (cC172(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC168(v0) = v1) | ? [v2] : ? [v3] : (cC166(v0) = v2 & cC142(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC166(v0) = v1) | ? [v2] : ? [v3] : (cC164(v0) = v3 & cC154(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC162(v0) = v1) | ? [v2] : ? [v3] : (cC160(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC158(v0) = v1) | ? [v2] : ? [v3] : (cC156(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC150(v0) = v1) | ? [v2] : ? [v3] : (cC148(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC146(v0) = v1) | ? [v2] : ? [v3] : (cC144(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC142(v0) = v1) | ? [v2] : ? [v3] : (cC140(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC14(v0) = v1) | ? [v2] : ? [v3] : (cC12(v0) = v2 & cC2(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC138(v0) = v1) | ? [v2] : ? [v3] : (cC136(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC134(v0) = v1) | ? [v2] : ? [v3] : (cC132(v0) = v2 & cC108(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC132(v0) = v1) | ? [v2] : ? [v3] : (cC130(v0) = v2 & cC120(v0) = v3 & ( ~ (v3 = 0) | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC128(v0) = v1) | ? [v2] : ? [v3] : (cC126(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC124(v0) = v1) | ? [v2] : ? [v3] : (cC122(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC116(v0) = v1) | ? [v2] : ? [v3] : (cC114(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC112(v0) = v1) | ? [v2] : ? [v3] : (cC110(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC108(v0) = v1) | ? [v2] : ? [v3] : (cC106(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC104(v0) = v1) | ? [v2] : ? [v3] : (cC102(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cC8(v0) = v1) | ? [v2] : ? [v3] : (cC10(v0) = v3 & cC2(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cowlThing(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC72(v0) = v3 & cC98(v0) = v2 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) & ! [v0] : ! [v1] : ( ~ (cTOP(v0) = v1) | ? [v2] : ? [v3] : (cC62(v0) = v3 & cC64(v0) = v2 & ( ~ (v2 = 0) | (v1 = 0 & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC58(v0) = v1) | ? [v2] : ? [v3] : (cC60(v0) = v2 & cC48(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC38(v0) = v1) | ? [v2] : ? [v3] : (cC40(v0) = v2 & cC32(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC22(v0) = v1) | ? [v2] : ? [v3] : (cC24(v0) = v2 & cC16(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC64(v0) = v1) | ? [v2] : ? [v3] : (cC216(v0) = v2 & cC214(v0) = v3 & ( ~ (v2 = 0) | (v1 = 0 & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC212(v0) = v1) | ? [v2] : ? [v3] : (cC214(v0) = v2 & cC100(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = 0))))) & ! [v0] : ! [v1] : ( ~ (cC8(v0) = v1) | ? [v2] : ? [v3] : (cC10(v0) = v2 & cC2(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) & ! [v0] : ( ~ (cTEST(v0) = 0) | (cC46(v0) = 0 & cC216(v0) = 0)) & ! [v0] : ( ~ (cC96(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC94(v0) = v1 & cC84(v0) = 0)) & ! [v0] : ( ~ (cC94(v0) = 0) | ? [v1] : (cC92(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC92(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC90(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC90(v0) = 0) | ? [v1] : (cC88(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC88(v0) = 0) | (cC86(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC86(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC84(v0) = 0) | ? [v1] : (cC82(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC82(v0) = 0) | ? [v1] : (cC80(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC80(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC78(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC78(v0) = 0) | ? [v1] : (cC76(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC76(v0) = 0) | (cC74(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC74(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC72(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC70(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC70(v0) = 0) | ? [v1] : (cC68(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC68(v0) = 0) | (cC66(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC66(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cTOP(v0) = 0) | ? [v1] : ? [v2] : (cC62(v0) = v1 & cC64(v0) = v2 & (v2 = 0 | v1 = 0))) & ! [v0] : ( ~ (cC62(v0) = 0) | ? [v1] : (cC60(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC6(v0) = 0) | (cC4(v0) = 0 & cC2(v0) = 0)) & ! [v0] : ( ~ (cC58(v0) = 0) | ? [v1] : (cC56(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC56(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC54(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC54(v0) = 0) | ? [v1] : (cC52(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC52(v0) = 0) | (cC50(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC50(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC48(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC46(v0) = 0) | (cC44(v0) = 0 & cC30(v0) = 0)) & ! [v0] : ( ~ (cC44(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC42(v0) = v2 & cC32(v0) = v1)) & ! [v0] : ( ~ (cC42(v0) = 0) | ? [v1] : (cC40(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC4(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & rR1(v0, v1) = 0 & cC2(v1) = v2)) & ! [v0] : ( ~ (cC38(v0) = 0) | ? [v1] : (cC36(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC36(v0) = 0) | (cC34(v0) = 0 & cC32(v0) = 0)) & ! [v0] : ( ~ (cC34(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC32(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC30(v0) = 0) | (cC28(v0) = 0 & cC14(v0) = 0)) & ! [v0] : ( ~ (cC28(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC26(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC26(v0) = 0) | ? [v1] : (cC24(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC22(v0) = 0) | ? [v1] : (cC20(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC64(v0) = 0) | ? [v1] : ? [v2] : (cC216(v0) = v2 & cC214(v0) = v1 & (v2 = 0 | v1 = 0))) & ! [v0] : ( ~ (cC212(v0) = 0) | ? [v1] : (cC210(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC210(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC208(v0) = v1 & cC134(v0) = v2)) & ! [v0] : ( ~ (cC208(v0) = 0) | ? [v1] : (cC206(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC206(v0) = 0) | (cC204(v0) = 0 & cC170(v0) = 0)) & ! [v0] : ( ~ (cC204(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC202(v0) = v2 & cC178(v0) = v1)) & ! [v0] : ( ~ (cC202(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC200(v0) = v1 & cC190(v0) = 0)) & ! [v0] : ( ~ (cC200(v0) = 0) | ? [v1] : (cC198(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC20(v0) = 0) | (cC18(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC198(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC196(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC196(v0) = 0) | ? [v1] : (cC194(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC194(v0) = 0) | (cC192(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC192(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC190(v0) = 0) | ? [v1] : (cC188(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC188(v0) = 0) | ? [v1] : (cC186(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC186(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC184(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC184(v0) = 0) | ? [v1] : (cC182(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC182(v0) = 0) | (cC180(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC180(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC18(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC178(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC176(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC176(v0) = 0) | ? [v1] : (cC174(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC174(v0) = 0) | (cC172(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC172(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC170(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC168(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC168(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC166(v0) = v1 & cC142(v0) = v2)) & ! [v0] : ( ~ (cC166(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC164(v0) = v1 & cC154(v0) = 0)) & ! [v0] : ( ~ (cC164(v0) = 0) | ? [v1] : (cC162(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC162(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC160(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC160(v0) = 0) | ? [v1] : (cC158(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC158(v0) = 0) | (cC156(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC156(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC154(v0) = 0) | ? [v1] : (cC152(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC152(v0) = 0) | ? [v1] : (cC150(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC150(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC148(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC148(v0) = 0) | ? [v1] : (cC146(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC146(v0) = 0) | (cC144(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC144(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC142(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC140(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC140(v0) = 0) | ? [v1] : (cC138(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC14(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC12(v0) = v1 & cC2(v0) = v2)) & ! [v0] : ( ~ (cC138(v0) = 0) | (cC136(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC136(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC134(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC132(v0) = v1 & cC108(v0) = v2)) & ! [v0] : ( ~ (cC132(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC130(v0) = v1 & cC120(v0) = 0)) & ! [v0] : ( ~ (cC130(v0) = 0) | ? [v1] : (cC128(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC128(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC126(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC126(v0) = 0) | ? [v1] : (cC124(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC124(v0) = 0) | (cC122(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC122(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC120(v0) = 0) | ? [v1] : (cC118(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC12(v0) = 0) | ? [v1] : (rR1(v0, v1) = 0 & cC10(v1) = 0)) & ! [v0] : ( ~ (cC118(v0) = 0) | ? [v1] : (cC116(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC116(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC114(v0) = v2 & cC16(v0) = v1)) & ! [v0] : ( ~ (cC114(v0) = 0) | ? [v1] : (cC112(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC112(v0) = 0) | (cC110(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC110(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC108(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC106(v0) = v1 & cC16(v0) = v2)) & ! [v0] : ( ~ (cC106(v0) = 0) | ? [v1] : (cC104(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC104(v0) = 0) | (cC102(v0) = 0 & cC16(v0) = 0)) & ! [v0] : ( ~ (cC102(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (cC100(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & rR1(v0, v1) = 0 & cC98(v1) = v2)) & ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | cC98(v0) = 0) & ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC60(v0) = v1)) & ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC40(v0) = v1)) & ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC24(v0) = v1)) & ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC10(v0) = v1)) & ! [v0] : ( ~ (cC8(v0) = 0) | ? [v1] : (cC6(v1) = 0 & rR1(v0, v1) = 0)) & ! [v0] : ( ~ (xsd_string(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) & ! [v0] : ~ (cowlNothing(v0) = 0) & ( ~ (all_0_3_3 = 0) | ~ (all_0_4_4 = 0) | ~ (all_0_5_5 = 0) | ~ (all_0_6_6 = 0) | ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0))) % 27.17/7.36 | % 27.17/7.36 | Applying alpha-rule on (1) yields: % 27.17/7.36 | (2) ! [v0] : ( ~ (cC104(v0) = 0) | (cC102(v0) = 0 & cC16(v0) = 0)) % 27.17/7.36 | (3) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC36(v0) = v1) | ? [v2] : ? [v3] : (cC34(v0) = v3 & cC32(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.17/7.36 | (4) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC212(v2) = v1) | ~ (cC212(v2) = v0)) % 27.17/7.36 | (5) ! [v0] : ( ~ (cC126(v0) = 0) | ? [v1] : (cC124(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.36 | (6) ! [v0] : ( ~ (cC70(v0) = 0) | ? [v1] : (cC68(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.36 | (7) ! [v0] : ! [v1] : ( ~ (cTOP(v0) = v1) | ? [v2] : ? [v3] : (cC62(v0) = v3 & cC64(v0) = v2 & ( ~ (v2 = 0) | (v1 = 0 & ~ (v3 = 0))))) % 27.17/7.36 | (8) ~ (all_0_12_12 = 0) % 27.17/7.36 | (9) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC168(v0) = v1) | ? [v2] : ? [v3] : (cC166(v0) = v2 & cC142(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.17/7.36 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC60(v2) = v1) | ~ (cC60(v2) = v0)) % 27.17/7.36 | (11) cC216(iV3102) = all_0_9_9 % 27.17/7.36 | (12) ! [v0] : ( ~ (cC100(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & rR1(v0, v1) = 0 & cC98(v1) = v2)) % 27.17/7.36 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC78(v2) = v1) | ~ (cC78(v2) = v0)) % 27.17/7.36 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC156(v2) = v1) | ~ (cC156(v2) = v0)) % 27.17/7.36 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC166(v2) = v1) | ~ (cC166(v2) = v0)) % 27.17/7.36 | (16) ! [v0] : ( ~ (cC178(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC176(v0) = v2 & cC16(v0) = v1)) % 27.17/7.36 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC140(v0) = v1) | ~ (cC138(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.36 | (18) cC16(iV3102) = all_0_13_13 % 27.17/7.36 | (19) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC134(v0) = v1) | ? [v2] : ? [v3] : (cC132(v0) = v2 & cC108(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.17/7.36 | (20) ! [v0] : ( ~ (cC82(v0) = 0) | ? [v1] : (cC80(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.36 | (21) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC34(v2) = v1) | ~ (cC34(v2) = v0)) % 27.17/7.36 | (22) cC30(iV3102) = all_0_7_7 % 27.17/7.36 | (23) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC166(v0) = v1) | ? [v2] : ? [v3] : (cC164(v0) = v3 & cC154(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.17/7.36 | (24) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC162(v2) = v1) | ~ (cC162(v2) = v0)) % 27.17/7.36 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC56(v2) = v1) | ~ (cC56(v2) = v0)) % 27.17/7.36 | (26) ! [v0] : ( ~ (cC52(v0) = 0) | (cC50(v0) = 0 & cC16(v0) = 0)) % 27.17/7.36 | (27) ! [v0] : ( ~ (cC66(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.17/7.36 | (28) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC142(v0) = v1) | ? [v2] : ? [v3] : (cC140(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.17/7.36 | (29) ~ (all_0_16_16 = 0) % 27.17/7.36 | (30) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC58(v0) = v1) | ? [v2] : ? [v3] : (cC60(v0) = v3 & cC48(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.17/7.37 | (31) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC164(v0) = v1) | ~ (cC162(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.37 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC106(v2) = v1) | ~ (cC106(v2) = v0)) % 27.17/7.37 | (33) ! [v0] : ( ~ (cC58(v0) = 0) | ? [v1] : (cC56(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.37 | (34) ! [v0] : ( ~ (cC14(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC12(v0) = v1 & cC2(v0) = v2)) % 27.17/7.37 | (35) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC88(v2) = v1) | ~ (cC88(v2) = v0)) % 27.17/7.37 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC130(v0) = v1) | ~ (cC128(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.37 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC192(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.17/7.37 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) % 27.17/7.37 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC84(v0) = v1) | ~ (cC82(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.37 | (40) ! [v0] : ( ~ (cC72(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC70(v0) = v1 & cC16(v0) = v2)) % 27.17/7.37 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC62(v0) = v1) | ~ (cC60(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.37 | (42) ! [v0] : ( ~ (cC76(v0) = 0) | (cC74(v0) = 0 & cC16(v0) = 0)) % 27.17/7.37 | (43) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC116(v2) = v1) | ~ (cC116(v2) = v0)) % 27.17/7.37 | (44) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC194(v0) = v1) | ? [v2] : ? [v3] : (cC192(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.17/7.37 | (45) ! [v0] : ( ~ (cC186(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC184(v0) = v2 & cC16(v0) = v1)) % 27.17/7.37 | (46) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC112(v0) = v1) | ? [v2] : ? [v3] : (cC110(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.17/7.37 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC32(v2) = v1) | ~ (cC32(v2) = v0)) % 27.17/7.37 | (48) ! [v0] : ( ~ (cTEST(v0) = 0) | (cC46(v0) = 0 & cC216(v0) = 0)) % 27.17/7.37 | (49) ! [v0] : ! [v1] : ( ~ (cC58(v0) = v1) | ? [v2] : ? [v3] : (cC60(v0) = v2 & cC48(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = 0))))) % 27.17/7.37 | (50) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC204(v0) = v1) | ? [v2] : ? [v3] : (cC202(v0) = v3 & cC178(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.17/7.37 | (51) ! [v0] : ( ~ (cC192(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.17/7.37 | (52) ! [v0] : ( ~ (cC154(v0) = 0) | ? [v1] : (cC152(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.37 | (53) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC92(v0) = v1) | ? [v2] : ? [v3] : (cC90(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.17/7.37 | (54) ! [v0] : ( ~ (cC120(v0) = 0) | ? [v1] : (cC118(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.37 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC142(v2) = v1) | ~ (cC142(v2) = v0)) % 27.17/7.37 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC190(v2) = v1) | ~ (cC190(v2) = v0)) % 27.17/7.37 | (57) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC162(v0) = v1) | ? [v2] : ? [v3] : (cC160(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.17/7.37 | (58) ! [v0] : ( ~ (cC150(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC148(v0) = v2 & cC16(v0) = v1)) % 27.17/7.37 | (59) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC68(v0) = v1) | ? [v2] : ? [v3] : (cC66(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.17/7.37 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC132(v2) = v1) | ~ (cC132(v2) = v0)) % 27.17/7.37 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC182(v2) = v1) | ~ (cC182(v2) = v0)) % 27.17/7.37 | (62) ! [v0] : ! [v1] : ( ~ (cC8(v0) = v1) | ? [v2] : ? [v3] : (cC10(v0) = v2 & cC2(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) % 27.17/7.37 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC14(v2) = v1) | ~ (cC14(v2) = v0)) % 27.17/7.37 | (64) ! [v0] : ( ~ (cC48(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.17/7.37 | (65) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC8(v0) = v1) | ? [v2] : ? [v3] : (cC10(v0) = v3 & cC2(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.17/7.37 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC62(v2) = v1) | ~ (cC62(v2) = v0)) % 27.17/7.37 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC34(v0) = v1) | ~ (cC32(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.17/7.37 | (68) cC214(iV3102) = all_0_15_15 % 27.17/7.37 | (69) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC136(v2) = v1) | ~ (cC136(v2) = v0)) % 27.17/7.37 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 27.17/7.37 | (71) cTOP(iV3102) = 0 % 27.17/7.37 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC188(v2) = v1) | ~ (cC188(v2) = v0)) % 27.17/7.37 | (73) ! [v0] : ( ~ (cC106(v0) = 0) | ? [v1] : (cC104(v1) = 0 & rR1(v0, v1) = 0)) % 27.17/7.37 | (74) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC70(v0) = v1) | ~ (cC68(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.17/7.37 | (75) ! [v0] : ( ~ (cC18(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.17/7.37 | (76) ! [v0] : ( ~ (cC34(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC32(v1) = v2 & rR1(v0, v1) = 0)) % 27.17/7.37 | (77) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC154(v2) = v1) | ~ (cC154(v2) = v0)) % 27.17/7.37 | (78) ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC24(v0) = v1)) % 27.17/7.37 | (79) ~ (all_0_11_11 = 0) % 27.17/7.37 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC104(v2) = v1) | ~ (cC104(v2) = v0)) % 27.17/7.37 | (81) ! [v0] : ~ (cowlNothing(v0) = 0) % 27.17/7.37 | (82) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC132(v0) = v1) | ? [v2] : ? [v3] : (cC130(v0) = v2 & cC120(v0) = v3 & ( ~ (v3 = 0) | v2 = 0))) % 27.17/7.37 | (83) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC176(v2) = v1) | ~ (cC176(v2) = v0)) % 27.17/7.37 | (84) ! [v0] : ( ~ (cC80(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC78(v0) = v2 & cC16(v0) = v1)) % 27.37/7.37 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC102(v2) = v1) | ~ (cC102(v2) = v0)) % 27.37/7.37 | (86) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC126(v2) = v1) | ~ (cC126(v2) = v0)) % 27.37/7.37 | (87) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC38(v0) = v1) | ? [v2] : ? [v3] : (cC40(v0) = v3 & cC32(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.37 | (88) ! [v0] : ( ~ (cC132(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC130(v0) = v1 & cC120(v0) = 0)) % 27.37/7.37 | (89) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC174(v0) = v1) | ? [v2] : ? [v3] : (cC172(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.37 | (90) cTEST(iV3102) = 0 % 27.37/7.37 | (91) ! [v0] : ( ~ (cC28(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC26(v0) = v1 & cC16(v0) = v2)) % 27.37/7.37 | (92) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC38(v0) = v1) | ~ (cC36(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.37 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) % 27.37/7.38 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC114(v2) = v1) | ~ (cC114(v2) = v0)) % 27.37/7.38 | (95) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC124(v0) = v1) | ? [v2] : ? [v3] : (cC122(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (96) ! [v0] : ( ~ (cC170(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC168(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.38 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC152(v0) = v1) | ~ (cC150(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.38 | (98) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC130(v2) = v1) | ~ (cC130(v2) = v0)) % 27.37/7.38 | (99) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC164(v2) = v1) | ~ (cC164(v2) = v0)) % 27.37/7.38 | (100) ! [v0] : ( ~ (cC204(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC202(v0) = v2 & cC178(v0) = v1)) % 27.37/7.38 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC144(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.38 | (102) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC202(v0) = v1) | ? [v2] : ? [v3] : (cC200(v0) = v3 & cC190(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.37/7.38 | (103) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC52(v2) = v1) | ~ (cC52(v2) = v0)) % 27.37/7.38 | (104) ~ (all_0_3_3 = 0) | ~ (all_0_4_4 = 0) | ~ (all_0_5_5 = 0) | ~ (all_0_6_6 = 0) | ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.38 | (105) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC206(v0) = v1) | ? [v2] : ? [v3] : (cC204(v0) = v3 & cC170(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (106) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTOP(v2) = v1) | ~ (cTOP(v2) = v0)) % 27.37/7.38 | (107) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC74(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.38 | (108) cC14(iV3102) = all_0_3_3 % 27.37/7.38 | (109) ! [v0] : ! [v1] : ( ~ (cC38(v0) = v1) | ? [v2] : ? [v3] : (cC40(v0) = v2 & cC32(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) % 27.37/7.38 | (110) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC214(v2) = v1) | ~ (cC214(v2) = v0)) % 27.37/7.38 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC12(v0) = v1) | ~ (cC10(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.38 | (112) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC20(v0) = v1) | ? [v2] : ? [v3] : (cC18(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (113) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC180(v2) = v1) | ~ (cC180(v2) = v0)) % 27.37/7.38 | (114) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC46(v0) = v1) | ? [v2] : ? [v3] : (cC44(v0) = v3 & cC30(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (115) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC6(v0) = v1) | ? [v2] : ? [v3] : (cC4(v0) = v3 & cC2(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (116) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC210(v2) = v1) | ~ (cC210(v2) = v0)) % 27.37/7.38 | (117) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC14(v0) = v1) | ? [v2] : ? [v3] : (cC12(v0) = v2 & cC2(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.38 | (118) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC88(v0) = v1) | ? [v2] : ? [v3] : (cC86(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.38 | (119) ! [v0] : ( ~ (cC26(v0) = 0) | ? [v1] : (cC24(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.38 | (120) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC26(v0) = v1) | ~ (cC24(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.38 | (121) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC134(v2) = v1) | ~ (cC134(v2) = v0)) % 27.37/7.38 | (122) ! [v0] : ( ~ (cC162(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC160(v0) = v2 & cC16(v0) = v1)) % 27.37/7.38 | (123) ! [v0] : ( ~ (cC90(v0) = 0) | ? [v1] : (cC88(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.38 | (124) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC194(v2) = v1) | ~ (cC194(v2) = v0)) % 27.37/7.38 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC100(v0) = v1) | ~ (cC98(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.38 | (126) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC138(v2) = v1) | ~ (cC138(v2) = v0)) % 27.37/7.38 | (127) ! [v0] : ( ~ (cC6(v0) = 0) | (cC4(v0) = 0 & cC2(v0) = 0)) % 27.37/7.38 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC48(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.38 | (129) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) % 27.37/7.38 | (130) ! [v0] : ( ~ (cC174(v0) = 0) | (cC172(v0) = 0 & cC16(v0) = 0)) % 27.37/7.38 | (131) ! [v0] : ( ~ (cC160(v0) = 0) | ? [v1] : (cC158(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.38 | (132) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC102(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.38 | (133) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC44(v0) = v1) | ? [v2] : ? [v3] : (cC42(v0) = v3 & cC32(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.38 | (134) ! [v0] : ( ~ (cC114(v0) = 0) | ? [v1] : (cC112(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.38 | (135) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC170(v2) = v1) | ~ (cC170(v2) = v0)) % 27.37/7.38 | (136) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC26(v2) = v1) | ~ (cC26(v2) = v0)) % 27.37/7.38 | (137) ! [v0] : ( ~ (cC172(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.38 | (138) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC22(v2) = v1) | ~ (cC22(v2) = v0)) % 27.37/7.38 | (139) ! [v0] : ( ~ (cC202(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC200(v0) = v1 & cC190(v0) = 0)) % 27.37/7.38 | (140) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC68(v2) = v1) | ~ (cC68(v2) = v0)) % 27.37/7.38 | (141) ! [v0] : ( ~ (cC134(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC132(v0) = v1 & cC108(v0) = v2)) % 27.37/7.38 | (142) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC54(v2) = v1) | ~ (cC54(v2) = v0)) % 27.37/7.38 | (143) cC32(iV3102) = all_0_11_11 % 27.37/7.38 | (144) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC36(v2) = v1) | ~ (cC36(v2) = v0)) % 27.37/7.38 | (145) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC86(v2) = v1) | ~ (cC86(v2) = v0)) % 27.37/7.38 | (146) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC122(v2) = v1) | ~ (cC122(v2) = v0)) % 27.37/7.38 | (147) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC196(v2) = v1) | ~ (cC196(v2) = v0)) % 27.37/7.38 | (148) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC58(v0) = v1) | ~ (cC56(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.38 | (149) ! [v0] : ( ~ (cC128(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC126(v0) = v2 & cC16(v0) = v1)) % 27.37/7.38 | (150) ! [v0] : ( ~ (cC110(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.38 | (151) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC82(v0) = v1) | ~ (cC80(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.38 | (152) ! [v0] : ( ~ (cC50(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.38 | (153) ! [v0] : ( ~ (cC176(v0) = 0) | ? [v1] : (cC174(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.38 | (154) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC150(v0) = v1) | ? [v2] : ? [v3] : (cC148(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.38 | (155) ! [v0] : ( ~ (cC44(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC42(v0) = v2 & cC32(v0) = v1)) % 27.37/7.38 | (156) ~ (all_0_14_14 = 0) % 27.37/7.39 | (157) cC42(iV3102) = all_0_18_18 % 27.37/7.39 | (158) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC202(v2) = v1) | ~ (cC202(v2) = v0)) % 27.37/7.39 | (159) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC22(v0) = v1) | ? [v2] : ? [v3] : (cC24(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.39 | (160) ! [v0] : ( ~ (cC196(v0) = 0) | ? [v1] : (cC194(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (161) ! [v0] : ( ~ (cC8(v0) = 0) | ? [v1] : (cC6(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (162) ! [v0] : ( ~ (cC124(v0) = 0) | (cC122(v0) = 0 & cC16(v0) = 0)) % 27.37/7.39 | (163) cC26(iV3102) = all_0_16_16 % 27.37/7.39 | (164) ~ (all_0_13_13 = 0) % 27.37/7.39 | (165) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC72(v0) = v1) | ? [v2] : ? [v3] : (cC70(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.39 | (166) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC184(v2) = v1) | ~ (cC184(v2) = v0)) % 27.37/7.39 | (167) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC54(v0) = v1) | ~ (cC52(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (168) ! [v0] : ( ~ (cC166(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC164(v0) = v1 & cC154(v0) = 0)) % 27.37/7.39 | (169) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC64(v2) = v1) | ~ (cC64(v2) = v0)) % 27.37/7.39 | (170) ! [v0] : ( ~ (cC62(v0) = 0) | ? [v1] : (cC60(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (171) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC126(v0) = v1) | ~ (cC124(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (172) ! [v0] : ( ~ (cC64(v0) = 0) | ? [v1] : ? [v2] : (cC216(v0) = v2 & cC214(v0) = v1 & (v2 = 0 | v1 = 0))) % 27.37/7.39 | (173) ! [v0] : ( ~ (cC210(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC208(v0) = v1 & cC134(v0) = v2)) % 27.37/7.39 | (174) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC216(v2) = v1) | ~ (cC216(v2) = v0)) % 27.37/7.39 | (175) ! [v0] : ( ~ (cTOP(v0) = 0) | ? [v1] : ? [v2] : (cC62(v0) = v1 & cC64(v0) = v2 & (v2 = 0 | v1 = 0))) % 27.37/7.39 | (176) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) % 27.37/7.39 | (177) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC52(v0) = v1) | ? [v2] : ? [v3] : (cC50(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.39 | (178) ! [v0] : ( ~ (cC68(v0) = 0) | (cC66(v0) = 0 & cC16(v0) = 0)) % 27.37/7.39 | (179) cC28(iV3102) = all_0_5_5 % 27.37/7.39 | (180) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC80(v2) = v1) | ~ (cC80(v2) = v0)) % 27.37/7.39 | (181) ! [v0] : ( ~ (cC36(v0) = 0) | (cC34(v0) = 0 & cC32(v0) = 0)) % 27.37/7.39 | (182) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC196(v0) = v1) | ~ (cC194(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (183) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC28(v0) = v1) | ? [v2] : ? [v3] : (cC26(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.39 | (184) ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | cC98(v0) = 0) % 27.37/7.39 | (185) ! [v0] : ( ~ (cC116(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC114(v0) = v2 & cC16(v0) = v1)) % 27.37/7.39 | (186) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC24(v2) = v1) | ~ (cC24(v2) = v0)) % 27.37/7.39 | (187) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC66(v2) = v1) | ~ (cC66(v2) = v0)) % 27.37/7.39 | (188) ! [v0] : ! [v1] : (v1 = 0 | ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0) % 27.37/7.39 | (189) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC120(v0) = v1) | ~ (cC118(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (190) ! [v0] : ( ~ (cC184(v0) = 0) | ? [v1] : (cC182(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (191) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC106(v0) = v1) | ~ (cC104(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (192) ! [v0] : ( ~ (cC144(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.39 | (193) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC146(v0) = v1) | ? [v2] : ? [v3] : (cC144(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.39 | (194) ! [v0] : ( ~ (cC138(v0) = 0) | (cC136(v0) = 0 & cC16(v0) = 0)) % 27.37/7.39 | (195) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC50(v2) = v1) | ~ (cC50(v2) = v0)) % 27.37/7.39 | (196) ! [v0] : ( ~ (cC140(v0) = 0) | ? [v1] : (cC138(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (197) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC30(v2) = v1) | ~ (cC30(v2) = v0)) % 27.37/7.39 | (198) ! [v0] : ( ~ (cC94(v0) = 0) | ? [v1] : (cC92(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (199) ! [v0] : ( ~ (cC122(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.39 | (200) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC76(v2) = v1) | ~ (cC76(v2) = v0)) % 27.37/7.39 | (201) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC184(v0) = v1) | ~ (cC182(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (202) ! [v0] : ( ~ (cC12(v0) = 0) | ? [v1] : (rR1(v0, v1) = 0 & cC10(v1) = 0)) % 27.37/7.39 | (203) ~ (all_0_15_15 = 0) % 27.37/7.39 | (204) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC8(v2) = v1) | ~ (cC8(v2) = v0)) % 27.37/7.39 | (205) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC128(v0) = v1) | ? [v2] : ? [v3] : (cC126(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.39 | (206) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC160(v2) = v1) | ~ (cC160(v2) = v0)) % 27.37/7.39 | (207) cC46(iV3102) = all_0_8_8 % 27.37/7.39 | (208) ! [v0] : ( ~ (cC30(v0) = 0) | (cC28(v0) = 0 & cC14(v0) = 0)) % 27.37/7.39 | (209) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC78(v0) = v1) | ~ (cC76(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (210) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC198(v2) = v1) | ~ (cC198(v2) = v0)) % 27.37/7.39 | (211) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC86(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.39 | (212) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC158(v2) = v1) | ~ (cC158(v2) = v0)) % 27.37/7.39 | (213) ~ (all_0_17_17 = 0) % 27.37/7.39 | (214) ! [v0] : ! [v1] : ( ~ (cC64(v0) = v1) | ? [v2] : ? [v3] : (cC216(v0) = v2 & cC214(v0) = v3 & ( ~ (v2 = 0) | (v1 = 0 & ~ (v3 = 0))))) % 27.37/7.39 | (215) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC150(v2) = v1) | ~ (cC150(v2) = v0)) % 27.37/7.39 | (216) cC12(iV3102) = all_0_17_17 % 27.37/7.39 | (217) ! [v0] : ( ~ (cC54(v0) = 0) | ? [v1] : (cC52(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.39 | (218) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC94(v2) = v1) | ~ (cC94(v2) = v0)) % 27.37/7.39 | (219) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC200(v2) = v1) | ~ (cC200(v2) = v0)) % 27.37/7.39 | (220) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC144(v2) = v1) | ~ (cC144(v2) = v0)) % 27.37/7.39 | (221) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC10(v2) = v1) | ~ (cC10(v2) = v0)) % 27.37/7.39 | (222) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC114(v0) = v1) | ~ (cC112(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (223) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC148(v0) = v1) | ~ (cC146(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (224) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC152(v2) = v1) | ~ (cC152(v2) = v0)) % 27.37/7.39 | (225) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC118(v0) = v1) | ~ (cC116(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.39 | (226) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC148(v2) = v1) | ~ (cC148(v2) = v0)) % 27.37/7.39 | (227) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC96(v2) = v1) | ~ (cC96(v2) = v0)) % 27.37/7.40 | (228) ~ (all_0_18_18 = 0) % 27.37/7.40 | (229) ! [v0] : ( ~ (cC22(v0) = 0) | ? [v1] : (cC20(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (230) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC172(v2) = v1) | ~ (cC172(v2) = v0)) % 27.37/7.40 | (231) ! [v0] : ( ~ (cC158(v0) = 0) | (cC156(v0) = 0 & cC16(v0) = 0)) % 27.37/7.40 | (232) ! [v0] : ( ~ (cC206(v0) = 0) | (cC204(v0) = 0 & cC170(v0) = 0)) % 27.37/7.40 | (233) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC160(v0) = v1) | ~ (cC158(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (234) ! [v0] : ( ~ (cC190(v0) = 0) | ? [v1] : (cC188(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (235) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC18(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (236) ! [v0] : ( ~ (cC84(v0) = 0) | ? [v1] : (cC82(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (237) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC122(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (238) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC94(v0) = v1) | ~ (cC92(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (239) ! [v0] : ! [v1] : ( ~ (cC212(v0) = v1) | ? [v2] : ? [v3] : (cC214(v0) = v2 & cC100(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = 0))))) % 27.37/7.40 | (240) ! [v0] : ( ~ (cC180(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.40 | (241) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC16(v2) = v1) | ~ (cC16(v2) = v0)) % 27.37/7.40 | (242) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC186(v2) = v1) | ~ (cC186(v2) = v0)) % 27.37/7.40 | (243) ! [v0] : ( ~ (cC96(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC94(v0) = v1 & cC84(v0) = 0)) % 27.37/7.40 | (244) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (rR1(v3, v2) = v1) | ~ (rR1(v3, v2) = v0)) % 27.37/7.40 | (245) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC128(v2) = v1) | ~ (cC128(v2) = v0)) % 27.37/7.40 | (246) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC172(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (247) ! [v0] : ( ~ (cC130(v0) = 0) | ? [v1] : (cC128(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (248) cC64(iV3102) = all_0_4_4 % 27.37/7.40 | (249) cC100(iV3102) = all_0_10_10 % 27.37/7.40 | (250) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC208(v0) = v1) | ~ (cC206(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (251) ! [v0] : ! [v1] : (v1 = 0 | ~ (cowlThing(v0) = v1)) % 27.37/7.40 | (252) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC4(v0) = v1) | ~ (cC2(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (253) ! [v0] : ! [v1] : (v1 = 0 | ~ (cTEST(v0) = v1) | ? [v2] : ? [v3] : (cC46(v0) = v3 & cC216(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.40 | (254) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC40(v2) = v1) | ~ (cC40(v2) = v0)) % 27.37/7.40 | (255) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC56(v0) = v1) | ? [v2] : ? [v3] : (cC54(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.40 | (256) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC84(v2) = v1) | ~ (cC84(v2) = v0)) % 27.37/7.40 | (257) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC18(v2) = v1) | ~ (cC18(v2) = v0)) % 27.37/7.40 | (258) ! [v0] : ( ~ (cC38(v0) = 0) | ? [v1] : (cC36(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (259) ! [v0] : ( ~ (cC146(v0) = 0) | (cC144(v0) = 0 & cC16(v0) = 0)) % 27.37/7.40 | (260) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC208(v2) = v1) | ~ (cC208(v2) = v0)) % 27.37/7.40 | (261) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC38(v2) = v1) | ~ (cC38(v2) = v0)) % 27.37/7.40 | (262) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC92(v2) = v1) | ~ (cC92(v2) = v0)) % 27.37/7.40 | (263) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC186(v0) = v1) | ? [v2] : ? [v3] : (cC184(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.40 | (264) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC82(v2) = v1) | ~ (cC82(v2) = v0)) % 27.37/7.40 | (265) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC6(v2) = v1) | ~ (cC6(v2) = v0)) % 27.37/7.40 | (266) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC212(v0) = v1) | ~ (cC210(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (267) ! [v0] : ( ~ (cC108(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC106(v0) = v1 & cC16(v0) = v2)) % 27.37/7.40 | (268) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC190(v0) = v1) | ~ (cC188(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (269) ! [v0] : ( ~ (cC118(v0) = 0) | ? [v1] : (cC116(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (270) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC22(v0) = v1) | ~ (cC20(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (271) ! [v0] : ( ~ (cC142(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC140(v0) = v1 & cC16(v0) = v2)) % 27.37/7.40 | (272) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC198(v0) = v1) | ? [v2] : ? [v3] : (cC196(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.40 | (273) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 27.37/7.40 | (274) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC12(v2) = v1) | ~ (cC12(v2) = v0)) % 27.37/7.40 | (275) ! [v0] : ( ~ (cC208(v0) = 0) | ? [v1] : (cC206(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (276) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC182(v0) = v1) | ? [v2] : ? [v3] : (cC180(v0) = v3 & cC16(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.40 | (277) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC30(v0) = v1) | ? [v2] : ? [v3] : (cC28(v0) = v3 & cC14(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.40 | (278) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC140(v2) = v1) | ~ (cC140(v2) = v0)) % 27.37/7.40 | (279) ~ (all_0_10_10 = 0) % 27.37/7.40 | (280) ! [v0] : ( ~ (cC148(v0) = 0) | ? [v1] : (cC146(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.40 | (281) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC176(v0) = v1) | ~ (cC174(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (282) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC156(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (283) ! [v0] : ( ~ (cC46(v0) = 0) | (cC44(v0) = 0 & cC30(v0) = 0)) % 27.37/7.40 | (284) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC104(v0) = v1) | ? [v2] : ? [v3] : (cC102(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.40 | (285) ! [v0] : ( ~ (cC168(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC166(v0) = v1 & cC142(v0) = v2)) % 27.37/7.40 | (286) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC66(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.40 | (287) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC188(v0) = v1) | ~ (cC186(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.40 | (288) ! [v0] : ( ~ (cC102(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.40 | (289) ! [v0] : ( ~ (cC112(v0) = 0) | (cC110(v0) = 0 & cC16(v0) = 0)) % 27.37/7.41 | (290) ! [v0] : ( ~ (cC92(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC90(v0) = v1 & cC16(v0) = v2)) % 27.37/7.41 | (291) ! [v0] : ( ~ (cC152(v0) = 0) | ? [v1] : (cC150(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (292) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC6(v2) = 0) | ~ (cC8(v0) = v1) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.41 | (293) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC94(v0) = v3 & cC84(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.37/7.41 | (294) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) % 27.37/7.41 | (295) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC90(v2) = v1) | ~ (cC90(v2) = v0)) % 27.37/7.41 | (296) ! [v0] : ( ~ (cC74(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.41 | (297) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC110(v2) = v1) | ~ (cC110(v2) = v0)) % 27.37/7.41 | (298) ! [v0] : ( ~ (cC156(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.41 | (299) ! [v0] : ( ~ (cC194(v0) = 0) | (cC192(v0) = 0 & cC16(v0) = 0)) % 27.37/7.41 | (300) cC62(iV3102) = all_0_14_14 % 27.37/7.41 | (301) ! [v0] : ( ~ (cC136(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.41 | (302) ! [v0] : ( ~ (cC212(v0) = 0) | ? [v1] : (cC210(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (303) cC2(iV3102) = all_0_12_12 % 27.37/7.41 | (304) ! [v0] : ( ~ (cC200(v0) = 0) | ? [v1] : (cC198(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (305) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC48(v2) = v1) | ~ (cC48(v2) = v0)) % 27.37/7.41 | (306) cC44(iV3102) = all_0_6_6 % 27.37/7.41 | (307) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC58(v2) = v1) | ~ (cC58(v2) = v0)) % 27.37/7.41 | (308) ! [v0] : ! [v1] : ( ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC72(v0) = v3 & cC98(v0) = v2 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) % 27.37/7.41 | (309) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC138(v0) = v1) | ? [v2] : ? [v3] : (cC136(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.41 | (310) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC80(v0) = v1) | ? [v2] : ? [v3] : (cC78(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.41 | (311) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC204(v2) = v1) | ~ (cC204(v2) = v0)) % 27.37/7.41 | (312) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC108(v2) = v1) | ~ (cC108(v2) = v0)) % 27.37/7.41 | (313) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC74(v2) = v1) | ~ (cC74(v2) = v0)) % 27.37/7.41 | (314) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC146(v2) = v1) | ~ (cC146(v2) = v0)) % 27.37/7.41 | (315) ! [v0] : ( ~ (cC182(v0) = 0) | (cC180(v0) = 0 & cC16(v0) = 0)) % 27.37/7.41 | (316) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC96(v0) = v1) | ? [v2] : ? [v3] : (cC72(v0) = v2 & cC98(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.41 | (317) ! [v0] : ( ~ (cC20(v0) = 0) | (cC18(v0) = 0 & cC16(v0) = 0)) % 27.37/7.41 | (318) ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC60(v0) = v1)) % 27.37/7.41 | (319) ! [v0] : ( ~ (cC188(v0) = 0) | ? [v1] : (cC186(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (320) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC154(v0) = v1) | ~ (cC152(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.41 | (321) ! [v0] : ( ~ (cC164(v0) = 0) | ? [v1] : (cC162(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (322) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC136(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.41 | (323) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC118(v2) = v1) | ~ (cC118(v2) = v0)) % 27.37/7.41 | (324) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC76(v0) = v1) | ? [v2] : ? [v3] : (cC74(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.41 | (325) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC124(v2) = v1) | ~ (cC124(v2) = v0)) % 27.37/7.41 | (326) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC120(v2) = v1) | ~ (cC120(v2) = v0)) % 27.37/7.41 | (327) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC46(v2) = v1) | ~ (cC46(v2) = v0)) % 27.37/7.41 | (328) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC20(v2) = v1) | ~ (cC20(v2) = v0)) % 27.37/7.41 | (329) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC192(v2) = v1) | ~ (cC192(v2) = v0)) % 27.37/7.41 | (330) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC100(v2) = v1) | ~ (cC100(v2) = v0)) % 27.37/7.41 | (331) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC50(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.41 | (332) ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC40(v0) = v1)) % 27.37/7.41 | (333) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC170(v0) = v1) | ~ (cC168(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.41 | (334) ! [v0] : ( ~ (cC86(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cC16(v1) = v2 & rR1(v0, v1) = 0)) % 27.37/7.41 | (335) ! [v0] : ( ~ (xsd_string(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) % 27.37/7.41 | (336) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC110(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.41 | (337) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC28(v2) = v1) | ~ (cC28(v2) = v0)) % 27.37/7.41 | (338) ! [v0] : ( ~ (cC88(v0) = 0) | (cC86(v0) = 0 & cC16(v0) = 0)) % 27.37/7.41 | (339) cowlThing(iV3102) = 0 % 27.37/7.41 | (340) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC90(v0) = v1) | ~ (cC88(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.41 | (341) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC108(v0) = v1) | ? [v2] : ? [v3] : (cC106(v0) = v2 & cC16(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.41 | (342) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC70(v2) = v1) | ~ (cC70(v2) = v0)) % 27.37/7.41 | (343) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC174(v2) = v1) | ~ (cC174(v2) = v0)) % 27.37/7.41 | (344) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC178(v0) = v1) | ? [v2] : ? [v3] : (cC176(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.41 | (345) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC210(v0) = v1) | ? [v2] : ? [v3] : (cC208(v0) = v2 & cC134(v0) = v3 & (v3 = 0 | v2 = 0))) % 27.37/7.41 | (346) ! [v0] : ( ~ (cC78(v0) = 0) | ? [v1] : (cC76(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.41 | (347) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC42(v2) = v1) | ~ (cC42(v2) = v0)) % 27.37/7.41 | (348) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC158(v0) = v1) | ? [v2] : ? [v3] : (cC156(v0) = v2 & cC16(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.37/7.41 | (349) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC44(v2) = v1) | ~ (cC44(v2) = v0)) % 27.37/7.41 | (350) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC72(v2) = v1) | ~ (cC72(v2) = v0)) % 27.37/7.41 | (351) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC206(v2) = v1) | ~ (cC206(v2) = v0)) % 27.37/7.41 | (352) ! [v0] : ( ~ (cC198(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC196(v0) = v1 & cC16(v0) = v2)) % 27.37/7.41 | (353) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC98(v2) = v1) | ~ (cC98(v2) = v0)) % 27.37/7.41 | (354) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v1 = 0 | ~ (cC180(v0) = v1) | ~ (cC16(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & rR1(v0, v2) = v4)) % 27.37/7.41 | (355) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC112(v2) = v1) | ~ (cC112(v2) = v0)) % 27.37/7.42 | (356) ! [v0] : ( ~ (rR1(iV3102, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & cC10(v0) = v1)) % 27.37/7.42 | (357) ! [v0] : ( ~ (cC4(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & rR1(v0, v1) = 0 & cC2(v1) = v2)) % 27.37/7.42 | (358) ! [v0] : ( ~ (cC42(v0) = 0) | ? [v1] : (cC40(v1) = 0 & rR1(v0, v1) = 0)) % 27.37/7.42 | (359) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC178(v2) = v1) | ~ (cC178(v2) = v0)) % 27.37/7.42 | (360) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC116(v0) = v1) | ? [v2] : ? [v3] : (cC114(v0) = v3 & cC16(v0) = v2 & (v3 = 0 | v2 = 0))) % 27.37/7.42 | (361) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC200(v0) = v1) | ~ (cC198(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.42 | (362) ! [v0] : ! [v1] : (v1 = 0 | ~ (cC212(v0) = v1) | ? [v2] : ? [v3] : (cC214(v0) = v3 & cC100(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.37/7.42 | (363) ! [v0] : ! [v1] : ( ~ (cC22(v0) = v1) | ? [v2] : ? [v3] : (cC24(v0) = v2 & cC16(v0) = v3 & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ~ (v1 = 0))))) % 27.37/7.42 | (364) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC168(v2) = v1) | ~ (cC168(v2) = v0)) % 27.37/7.42 | (365) ! [v0] : ! [v1] : ! [v2] : (v1 = 0 | ~ (cC42(v0) = v1) | ~ (cC40(v2) = 0) | ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) % 27.37/7.42 | (366) ! [v0] : ( ~ (cC56(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & ~ (v1 = 0) & cC54(v0) = v2 & cC16(v0) = v1)) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (48) with iV3102 and discharging atoms cTEST(iV3102) = 0, yields: % 27.37/7.42 | (367) cC46(iV3102) = 0 & cC216(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 | Applying alpha-rule on (367) yields: % 27.37/7.42 | (368) cC46(iV3102) = 0 % 27.37/7.42 | (369) cC216(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (283) with iV3102 yields: % 27.37/7.42 | (370) ~ (cC46(iV3102) = 0) | (cC44(iV3102) = 0 & cC30(iV3102) = 0) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (114) with all_0_8_8, iV3102 and discharging atoms cC46(iV3102) = all_0_8_8, yields: % 27.37/7.42 | (371) all_0_8_8 = 0 | ? [v0] : ? [v1] : (cC44(iV3102) = v1 & cC30(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (133) with all_0_6_6, iV3102 and discharging atoms cC44(iV3102) = all_0_6_6, yields: % 27.37/7.42 | (372) all_0_6_6 = 0 | ? [v0] : ? [v1] : (cC42(iV3102) = v1 & cC32(iV3102) = v0 & (v1 = 0 | v0 = 0)) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (208) with iV3102 yields: % 27.37/7.42 | (373) ~ (cC30(iV3102) = 0) | (cC28(iV3102) = 0 & cC14(iV3102) = 0) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (277) with all_0_7_7, iV3102 and discharging atoms cC30(iV3102) = all_0_7_7, yields: % 27.37/7.42 | (374) all_0_7_7 = 0 | ? [v0] : ? [v1] : (cC28(iV3102) = v1 & cC14(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (183) with all_0_5_5, iV3102 and discharging atoms cC28(iV3102) = all_0_5_5, yields: % 27.37/7.42 | (375) all_0_5_5 = 0 | ? [v0] : ? [v1] : (cC26(iV3102) = v0 & cC16(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (214) with all_0_4_4, iV3102 and discharging atoms cC64(iV3102) = all_0_4_4, yields: % 27.37/7.42 | (376) ? [v0] : ? [v1] : (cC216(iV3102) = v0 & cC214(iV3102) = v1 & ( ~ (v0 = 0) | (all_0_4_4 = 0 & ~ (v1 = 0)))) % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (117) with all_0_3_3, iV3102 and discharging atoms cC14(iV3102) = all_0_3_3, yields: % 27.37/7.42 | (377) all_0_3_3 = 0 | ? [v0] : ? [v1] : (cC12(iV3102) = v0 & cC2(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 27.37/7.42 | % 27.37/7.42 | Instantiating (376) with all_9_0_19, all_9_1_20 yields: % 27.37/7.42 | (378) cC216(iV3102) = all_9_1_20 & cC214(iV3102) = all_9_0_19 & ( ~ (all_9_1_20 = 0) | (all_0_4_4 = 0 & ~ (all_9_0_19 = 0))) % 27.37/7.42 | % 27.37/7.42 | Applying alpha-rule on (378) yields: % 27.37/7.42 | (379) cC216(iV3102) = all_9_1_20 % 27.37/7.42 | (380) cC214(iV3102) = all_9_0_19 % 27.37/7.42 | (381) ~ (all_9_1_20 = 0) | (all_0_4_4 = 0 & ~ (all_9_0_19 = 0)) % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (370), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (382) ~ (cC46(iV3102) = 0) % 27.37/7.42 | % 27.37/7.42 | Using (368) and (382) yields: % 27.37/7.42 | (383) $false % 27.37/7.42 | % 27.37/7.42 |-The branch is then unsatisfiable % 27.37/7.42 |-Branch two: % 27.37/7.42 | (368) cC46(iV3102) = 0 % 27.37/7.42 | (385) cC44(iV3102) = 0 & cC30(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 | Applying alpha-rule on (385) yields: % 27.37/7.42 | (386) cC44(iV3102) = 0 % 27.37/7.42 | (387) cC30(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (377), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (388) all_0_3_3 = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (373), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (389) ~ (cC30(iV3102) = 0) % 27.37/7.42 | % 27.37/7.42 | Using (387) and (389) yields: % 27.37/7.42 | (383) $false % 27.37/7.42 | % 27.37/7.42 |-The branch is then unsatisfiable % 27.37/7.42 |-Branch two: % 27.37/7.42 | (387) cC30(iV3102) = 0 % 27.37/7.42 | (392) cC28(iV3102) = 0 & cC14(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 | Applying alpha-rule on (392) yields: % 27.37/7.42 | (393) cC28(iV3102) = 0 % 27.37/7.42 | (394) cC14(iV3102) = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (375), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (395) all_0_5_5 = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (372), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (396) all_0_6_6 = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (374), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (397) all_0_7_7 = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (371), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (398) all_0_8_8 = 0 % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (174) with iV3102, all_9_1_20, all_0_9_9 and discharging atoms cC216(iV3102) = all_9_1_20, cC216(iV3102) = all_0_9_9, yields: % 27.37/7.42 | (399) all_9_1_20 = all_0_9_9 % 27.37/7.42 | % 27.37/7.42 | Instantiating formula (174) with iV3102, 0, all_9_1_20 and discharging atoms cC216(iV3102) = all_9_1_20, cC216(iV3102) = 0, yields: % 27.37/7.42 | (400) all_9_1_20 = 0 % 27.37/7.42 | % 27.37/7.42 | Combining equations (400,399) yields a new equation: % 27.37/7.42 | (401) all_0_9_9 = 0 % 27.37/7.42 | % 27.37/7.42 | Combining equations (401,399) yields a new equation: % 27.37/7.42 | (400) all_9_1_20 = 0 % 27.37/7.42 | % 27.37/7.42 +-Applying beta-rule and splitting (381), into two cases. % 27.37/7.42 |-Branch one: % 27.37/7.42 | (403) ~ (all_9_1_20 = 0) % 27.37/7.42 | % 27.37/7.42 | Equations (400) can reduce 403 to: % 27.37/7.42 | (404) $false % 27.37/7.42 | % 27.37/7.42 |-The branch is then unsatisfiable % 27.37/7.42 |-Branch two: % 27.37/7.42 | (400) all_9_1_20 = 0 % 27.37/7.42 | (406) all_0_4_4 = 0 & ~ (all_9_0_19 = 0) % 27.37/7.42 | % 27.37/7.42 | Applying alpha-rule on (406) yields: % 27.37/7.42 | (407) all_0_4_4 = 0 % 27.37/7.43 | (408) ~ (all_9_0_19 = 0) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (104), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (409) ~ (all_0_3_3 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (388) can reduce 409 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (388) all_0_3_3 = 0 % 27.37/7.43 | (412) ~ (all_0_4_4 = 0) | ~ (all_0_5_5 = 0) | ~ (all_0_6_6 = 0) | ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (412), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (413) ~ (all_0_4_4 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (407) can reduce 413 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (407) all_0_4_4 = 0 % 27.37/7.43 | (416) ~ (all_0_5_5 = 0) | ~ (all_0_6_6 = 0) | ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (416), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (417) ~ (all_0_5_5 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (395) can reduce 417 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (395) all_0_5_5 = 0 % 27.37/7.43 | (420) ~ (all_0_6_6 = 0) | ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (420), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (421) ~ (all_0_6_6 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (396) can reduce 421 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (396) all_0_6_6 = 0 % 27.37/7.43 | (424) ~ (all_0_7_7 = 0) | ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (424), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (425) ~ (all_0_7_7 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (397) can reduce 425 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (397) all_0_7_7 = 0 % 27.37/7.43 | (428) ~ (all_0_8_8 = 0) | ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (428), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (429) ~ (all_0_8_8 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (398) can reduce 429 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (398) all_0_8_8 = 0 % 27.37/7.43 | (432) ~ (all_0_9_9 = 0) | (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (432), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (433) ~ (all_0_9_9 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (401) can reduce 433 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (401) all_0_9_9 = 0 % 27.37/7.43 | (436) (xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)))) | (cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0)) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (436), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (437) xsd_string(all_0_2_2) = all_0_1_1 & xsd_integer(all_0_2_2) = all_0_0_0 & ((all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0))) % 27.37/7.43 | % 27.37/7.43 | Applying alpha-rule on (437) yields: % 27.37/7.43 | (438) xsd_string(all_0_2_2) = all_0_1_1 % 27.37/7.43 | (439) xsd_integer(all_0_2_2) = all_0_0_0 % 27.37/7.43 | (440) (all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0)) % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (335) with all_0_2_2 yields: % 27.37/7.43 | (441) ~ (xsd_string(all_0_2_2) = 0) | ? [v0] : ( ~ (v0 = 0) & xsd_integer(all_0_2_2) = v0) % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (188) with all_0_1_1, all_0_2_2 and discharging atoms xsd_string(all_0_2_2) = all_0_1_1, yields: % 27.37/7.43 | (442) all_0_1_1 = 0 | xsd_integer(all_0_2_2) = 0 % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (440), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (443) all_0_0_0 = 0 & all_0_1_1 = 0 % 27.37/7.43 | % 27.37/7.43 | Applying alpha-rule on (443) yields: % 27.37/7.43 | (444) all_0_0_0 = 0 % 27.37/7.43 | (445) all_0_1_1 = 0 % 27.37/7.43 | % 27.37/7.43 | From (445) and (438) follows: % 27.37/7.43 | (446) xsd_string(all_0_2_2) = 0 % 27.37/7.43 | % 27.37/7.43 | From (444) and (439) follows: % 27.37/7.43 | (447) xsd_integer(all_0_2_2) = 0 % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (441), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (448) ~ (xsd_string(all_0_2_2) = 0) % 27.37/7.43 | % 27.37/7.43 | Using (446) and (448) yields: % 27.37/7.43 | (383) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (446) xsd_string(all_0_2_2) = 0 % 27.37/7.43 | (451) ? [v0] : ( ~ (v0 = 0) & xsd_integer(all_0_2_2) = v0) % 27.37/7.43 | % 27.37/7.43 | Instantiating (451) with all_116_0_23 yields: % 27.37/7.43 | (452) ~ (all_116_0_23 = 0) & xsd_integer(all_0_2_2) = all_116_0_23 % 27.37/7.43 | % 27.37/7.43 | Applying alpha-rule on (452) yields: % 27.37/7.43 | (453) ~ (all_116_0_23 = 0) % 27.37/7.43 | (454) xsd_integer(all_0_2_2) = all_116_0_23 % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (70) with all_0_2_2, 0, all_116_0_23 and discharging atoms xsd_integer(all_0_2_2) = all_116_0_23, xsd_integer(all_0_2_2) = 0, yields: % 27.37/7.43 | (455) all_116_0_23 = 0 % 27.37/7.43 | % 27.37/7.43 | Equations (455) can reduce 453 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (457) ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0) % 27.37/7.43 | % 27.37/7.43 | Applying alpha-rule on (457) yields: % 27.37/7.43 | (458) ~ (all_0_0_0 = 0) % 27.37/7.43 | (459) ~ (all_0_1_1 = 0) % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (442), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (447) xsd_integer(all_0_2_2) = 0 % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (70) with all_0_2_2, 0, all_0_0_0 and discharging atoms xsd_integer(all_0_2_2) = all_0_0_0, xsd_integer(all_0_2_2) = 0, yields: % 27.37/7.43 | (444) all_0_0_0 = 0 % 27.37/7.43 | % 27.37/7.43 | Equations (444) can reduce 458 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (463) ~ (xsd_integer(all_0_2_2) = 0) % 27.37/7.43 | (445) all_0_1_1 = 0 % 27.37/7.43 | % 27.37/7.43 | Equations (445) can reduce 459 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (466) cowlNothing(all_0_2_2) = all_0_0_0 & cowlThing(all_0_2_2) = all_0_1_1 & ( ~ (all_0_1_1 = 0) | all_0_0_0 = 0) % 27.37/7.43 | % 27.37/7.43 | Applying alpha-rule on (466) yields: % 27.37/7.43 | (467) cowlNothing(all_0_2_2) = all_0_0_0 % 27.37/7.43 | (468) cowlThing(all_0_2_2) = all_0_1_1 % 27.37/7.43 | (469) ~ (all_0_1_1 = 0) | all_0_0_0 = 0 % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (81) with all_0_2_2 yields: % 27.37/7.43 | (470) ~ (cowlNothing(all_0_2_2) = 0) % 27.37/7.43 | % 27.37/7.43 | Instantiating formula (251) with all_0_1_1, all_0_2_2 and discharging atoms cowlThing(all_0_2_2) = all_0_1_1, yields: % 27.37/7.43 | (445) all_0_1_1 = 0 % 27.37/7.43 | % 27.37/7.43 +-Applying beta-rule and splitting (469), into two cases. % 27.37/7.43 |-Branch one: % 27.37/7.43 | (459) ~ (all_0_1_1 = 0) % 27.37/7.43 | % 27.37/7.43 | Equations (445) can reduce 459 to: % 27.37/7.43 | (404) $false % 27.37/7.43 | % 27.37/7.43 |-The branch is then unsatisfiable % 27.37/7.43 |-Branch two: % 27.37/7.43 | (445) all_0_1_1 = 0 % 27.37/7.44 | (444) all_0_0_0 = 0 % 27.37/7.44 | % 27.37/7.44 | From (444) and (467) follows: % 27.37/7.44 | (476) cowlNothing(all_0_2_2) = 0 % 27.37/7.44 | % 27.37/7.44 | Using (476) and (470) yields: % 27.37/7.44 | (383) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (429) ~ (all_0_8_8 = 0) % 27.37/7.44 | (479) ? [v0] : ? [v1] : (cC44(iV3102) = v1 & cC30(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 27.37/7.44 | % 27.37/7.44 | Instantiating formula (327) with iV3102, 0, all_0_8_8 and discharging atoms cC46(iV3102) = all_0_8_8, cC46(iV3102) = 0, yields: % 27.37/7.44 | (398) all_0_8_8 = 0 % 27.37/7.44 | % 27.37/7.44 | Equations (398) can reduce 429 to: % 27.37/7.44 | (404) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (425) ~ (all_0_7_7 = 0) % 27.37/7.44 | (483) ? [v0] : ? [v1] : (cC28(iV3102) = v1 & cC14(iV3102) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 27.37/7.44 | % 27.37/7.44 | Instantiating formula (197) with iV3102, 0, all_0_7_7 and discharging atoms cC30(iV3102) = all_0_7_7, cC30(iV3102) = 0, yields: % 27.37/7.44 | (397) all_0_7_7 = 0 % 27.37/7.44 | % 27.37/7.44 | Equations (397) can reduce 425 to: % 27.37/7.44 | (404) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (421) ~ (all_0_6_6 = 0) % 27.37/7.44 | (487) ? [v0] : ? [v1] : (cC42(iV3102) = v1 & cC32(iV3102) = v0 & (v1 = 0 | v0 = 0)) % 27.37/7.44 | % 27.37/7.44 | Instantiating formula (349) with iV3102, 0, all_0_6_6 and discharging atoms cC44(iV3102) = all_0_6_6, cC44(iV3102) = 0, yields: % 27.37/7.44 | (396) all_0_6_6 = 0 % 27.37/7.44 | % 27.37/7.44 | Equations (396) can reduce 421 to: % 27.37/7.44 | (404) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (417) ~ (all_0_5_5 = 0) % 27.37/7.44 | (491) ? [v0] : ? [v1] : (cC26(iV3102) = v0 & cC16(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 27.37/7.44 | % 27.37/7.44 | Instantiating formula (337) with iV3102, 0, all_0_5_5 and discharging atoms cC28(iV3102) = all_0_5_5, cC28(iV3102) = 0, yields: % 27.37/7.44 | (395) all_0_5_5 = 0 % 27.37/7.44 | % 27.37/7.44 | Equations (395) can reduce 417 to: % 27.37/7.44 | (404) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (409) ~ (all_0_3_3 = 0) % 27.37/7.44 | (495) ? [v0] : ? [v1] : (cC12(iV3102) = v0 & cC2(iV3102) = v1 & (v1 = 0 | v0 = 0)) % 27.37/7.44 | % 27.37/7.44 +-Applying beta-rule and splitting (373), into two cases. % 27.37/7.44 |-Branch one: % 27.37/7.44 | (389) ~ (cC30(iV3102) = 0) % 27.37/7.44 | % 27.37/7.44 | Using (387) and (389) yields: % 27.37/7.44 | (383) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 |-Branch two: % 27.37/7.44 | (387) cC30(iV3102) = 0 % 27.37/7.44 | (392) cC28(iV3102) = 0 & cC14(iV3102) = 0 % 27.37/7.44 | % 27.37/7.44 | Applying alpha-rule on (392) yields: % 27.37/7.44 | (393) cC28(iV3102) = 0 % 27.37/7.44 | (394) cC14(iV3102) = 0 % 27.37/7.44 | % 27.37/7.44 | Instantiating formula (63) with iV3102, 0, all_0_3_3 and discharging atoms cC14(iV3102) = all_0_3_3, cC14(iV3102) = 0, yields: % 27.37/7.44 | (388) all_0_3_3 = 0 % 27.37/7.44 | % 27.37/7.44 | Equations (388) can reduce 409 to: % 27.37/7.44 | (404) $false % 27.37/7.44 | % 27.37/7.44 |-The branch is then unsatisfiable % 27.37/7.44 % SZS output end Proof for theBenchmark % 27.37/7.44 % 27.37/7.44 6820ms %------------------------------------------------------------------------------