ePrincess---1.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : ePrincess---1.0
% Problem  : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : ePrincess-casc -timeout=%d %s

% Computer : n024.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:44 EDT 2022

% Result   : Theorem 22.73s 6.60s
% Output   : Proof 30.08s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.12  % Command  : ePrincess-casc -timeout=%d %s
% 0.12/0.33  % Computer : n024.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Tue Jun  7 14:52:34 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.56/0.57          ____       _                          
% 0.56/0.57    ___  / __ \_____(_)___  ________  __________
% 0.56/0.57   / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/
% 0.56/0.57  /  __/ ____/ /  / / / / / /__/  __(__  |__  ) 
% 0.56/0.57  \___/_/   /_/  /_/_/ /_/\___/\___/____/____/  
% 0.56/0.57  
% 0.56/0.57  A Theorem Prover for First-Order Logic
% 0.56/0.58  (ePrincess v.1.0)
% 0.56/0.58  
% 0.56/0.58  (c) Philipp Rümmer, 2009-2015
% 0.56/0.58  (c) Peter Backeman, 2014-2015
% 0.56/0.58  (contributions by Angelo Brillout, Peter Baumgartner)
% 0.56/0.58  Free software under GNU Lesser General Public License (LGPL).
% 0.56/0.58  Bug reports to peter@backeman.se
% 0.56/0.58  
% 0.56/0.58  For more information, visit http://user.uu.se/~petba168/breu/
% 0.56/0.58  
% 0.56/0.58  Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 0.56/0.62  Prover 0: Options:  -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all
% 2.14/1.07  Prover 0: Preprocessing ...
% 3.52/1.43  Prover 0: Warning: ignoring some quantifiers
% 3.74/1.47  Prover 0: Constructing countermodel ...
% 19.66/5.91  Prover 1: Options:  +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all
% 19.87/5.98  Prover 1: Preprocessing ...
% 21.72/6.40  Prover 1: Constructing countermodel ...
% 22.73/6.60  Prover 1: proved (683ms)
% 22.73/6.60  Prover 0: stopped
% 22.73/6.60  
% 22.73/6.60  No countermodel exists, formula is valid
% 22.73/6.60  % SZS status Theorem for theBenchmark
% 22.73/6.60  
% 22.73/6.60  Generating proof ... found it (size 197)
% 28.90/8.04  
% 28.90/8.04  % SZS output start Proof for theBenchmark
% 28.90/8.04  Assumed formulas after preprocessing and simplification: 
% 28.90/8.04  | (0)  ? [v0] :  ? [v1] :  ? [v2] :  ? [v3] :  ? [v4] :  ? [v5] :  ? [v6] :  ? [v7] :  ? [v8] :  ? [v9] :  ? [v10] :  ? [v11] :  ? [v12] :  ? [v13] :  ? [v14] : (cC92xcomp(iV8467) = 0 & cC82(iV8467) = v3 & cC80(iV8471) = v9 & cC78xcomp(iV8471) = 0 & cC72xcomp(iV8467) = 0 & cC62(iV8467) = v4 & cC60(iV8472) = v11 & cC6xcomp(iV8469) = 0 & cC58(iV8472) = v10 & cC52xcomp(iV8467) = 0 & cC48(iV8467) = v8 & cC42xcomp(iV8467) = 0 & cC34(iV8467) = v6 & cC32xcomp(iV8474) = 0 & cC26xcomp(iV8467) = 0 & cC20(iV8467) = v0 & cC2xcomp(iV8472) = 0 & cC2xcomp(iV8475) = 0 & cC2xcomp(iV8473) = 0 & cC2xcomp(iV8468) = 0 & cC2xcomp(iV8471) = 0 & cC2(iV8476) = 0 & cTOP(iV8470) = 0 & cC14(iV8467) = v5 & rR1(iV8472, iV8476) = 0 & rR1(iV8467, iV8472) = 0 & rR1(iV8467, iV8475) = 0 & rR1(iV8467, iV8473) = 0 & rR1(iV8467, iV8468) = 0 & rR1(iV8467, iV8474) = 0 & rR1(iV8467, iV8469) = 0 & rR1(iV8467, iV8470) = 0 & rR1(iV8467, iV8471) = 0 & cC8(iV8467) = v2 & cC10(iV8467) = v7 & cC4(iV8467) = v1 & cowlThing(iV8476) = 0 & cowlThing(iV8472) = 0 & cowlThing(iV8475) = 0 & cowlThing(iV8473) = 0 & cowlThing(iV8468) = 0 & cowlThing(iV8474) = 0 & cowlThing(iV8469) = 0 & cowlThing(iV8470) = 0 & cowlThing(iV8471) = 0 & cowlThing(iV8467) = 0 &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px29(v18, v17) = v16) |  ~ (ra_Px29(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px34(v18, v17) = v16) |  ~ (ra_Px34(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px23(v18, v17) = v16) |  ~ (ra_Px23(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px25(v18, v17) = v16) |  ~ (ra_Px25(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px20(v18, v17) = v16) |  ~ (ra_Px20(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px18(v18, v17) = v16) |  ~ (ra_Px18(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px33(v18, v17) = v16) |  ~ (ra_Px33(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px17(v18, v17) = v16) |  ~ (ra_Px17(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px28(v18, v17) = v16) |  ~ (ra_Px28(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px14(v18, v17) = v16) |  ~ (ra_Px14(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px32(v18, v17) = v16) |  ~ (ra_Px32(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px13(v18, v17) = v16) |  ~ (ra_Px13(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px12(v18, v17) = v16) |  ~ (ra_Px12(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px10(v18, v17) = v16) |  ~ (ra_Px10(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px31(v18, v17) = v16) |  ~ (ra_Px31(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px8(v18, v17) = v16) |  ~ (ra_Px8(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px9(v18, v17) = v16) |  ~ (ra_Px9(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px7(v18, v17) = v16) |  ~ (ra_Px7(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px6(v18, v17) = v16) |  ~ (ra_Px6(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px30(v18, v17) = v16) |  ~ (ra_Px30(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px5(v18, v17) = v16) |  ~ (ra_Px5(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px3(v18, v17) = v16) |  ~ (ra_Px3(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px2(v18, v17) = v16) |  ~ (ra_Px2(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (ra_Px1(v18, v17) = v16) |  ~ (ra_Px1(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] :  ! [v18] : (v16 = v15 |  ~ (rR1(v18, v17) = v16) |  ~ (rR1(v18, v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cTEST(v17) = v16) |  ~ (cTEST(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC94xcomp(v17) = v16) |  ~ (cC94xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC94(v17) = v16) |  ~ (cC94(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC92xcomp(v17) = v16) |  ~ (cC92xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC92(v17) = v16) |  ~ (cC92(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC90(v17) = v16) |  ~ (cC90(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC88(v17) = v16) |  ~ (cC88(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC86(v17) = v16) |  ~ (cC86(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC84xcomp(v17) = v16) |  ~ (cC84xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC84(v17) = v16) |  ~ (cC84(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC82xcomp(v17) = v16) |  ~ (cC82xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC82(v17) = v16) |  ~ (cC82(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC80(v17) = v16) |  ~ (cC80(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC78xcomp(v17) = v16) |  ~ (cC78xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC78(v17) = v16) |  ~ (cC78(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC76(v17) = v16) |  ~ (cC76(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC74xcomp(v17) = v16) |  ~ (cC74xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC74(v17) = v16) |  ~ (cC74(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC72xcomp(v17) = v16) |  ~ (cC72xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC72(v17) = v16) |  ~ (cC72(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC70(v17) = v16) |  ~ (cC70(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC68(v17) = v16) |  ~ (cC68(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC66(v17) = v16) |  ~ (cC66(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC64(v17) = v16) |  ~ (cC64(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC62xcomp(v17) = v16) |  ~ (cC62xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC62(v17) = v16) |  ~ (cC62(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC60(v17) = v16) |  ~ (cC60(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC6xcomp(v17) = v16) |  ~ (cC6xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC6(v17) = v16) |  ~ (cC6(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC58(v17) = v16) |  ~ (cC58(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC56(v17) = v16) |  ~ (cC56(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC54xcomp(v17) = v16) |  ~ (cC54xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC54(v17) = v16) |  ~ (cC54(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC52xcomp(v17) = v16) |  ~ (cC52xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC52(v17) = v16) |  ~ (cC52(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC50xcomp(v17) = v16) |  ~ (cC50xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC50(v17) = v16) |  ~ (cC50(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC48xcomp(v17) = v16) |  ~ (cC48xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC48(v17) = v16) |  ~ (cC48(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC46(v17) = v16) |  ~ (cC46(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC44xcomp(v17) = v16) |  ~ (cC44xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC44(v17) = v16) |  ~ (cC44(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC42xcomp(v17) = v16) |  ~ (cC42xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC42(v17) = v16) |  ~ (cC42(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC40(v17) = v16) |  ~ (cC40(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC38(v17) = v16) |  ~ (cC38(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC36xcomp(v17) = v16) |  ~ (cC36xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC36(v17) = v16) |  ~ (cC36(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC34xcomp(v17) = v16) |  ~ (cC34xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC34(v17) = v16) |  ~ (cC34(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC32xcomp(v17) = v16) |  ~ (cC32xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC32(v17) = v16) |  ~ (cC32(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC30(v17) = v16) |  ~ (cC30(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC28xcomp(v17) = v16) |  ~ (cC28xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC28(v17) = v16) |  ~ (cC28(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC26xcomp(v17) = v16) |  ~ (cC26xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC26(v17) = v16) |  ~ (cC26(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC24(v17) = v16) |  ~ (cC24(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC22(v17) = v16) |  ~ (cC22(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC20xcomp(v17) = v16) |  ~ (cC20xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC20(v17) = v16) |  ~ (cC20(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC2xcomp(v17) = v16) |  ~ (cC2xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC2(v17) = v16) |  ~ (cC2(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC18(v17) = v16) |  ~ (cC18(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC16xcomp(v17) = v16) |  ~ (cC16xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC16(v17) = v16) |  ~ (cC16(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC14xcomp(v17) = v16) |  ~ (cC14xcomp(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cTOP(v17) = v16) |  ~ (cTOP(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC14(v17) = v16) |  ~ (cC14(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC12(v17) = v16) |  ~ (cC12(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC8(v17) = v16) |  ~ (cC8(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC10(v17) = v16) |  ~ (cC10(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cC4(v17) = v16) |  ~ (cC4(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (xsd_string(v17) = v16) |  ~ (xsd_string(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (xsd_integer(v17) = v16) |  ~ (xsd_integer(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cowlNothing(v17) = v16) |  ~ (cowlNothing(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = v15 |  ~ (cowlThing(v17) = v16) |  ~ (cowlThing(v17) = v15)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC94(v15) = v16) |  ~ (ra_Px29(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC94(v15) = v16) |  ~ (cC92(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC92xcomp(v15) = v16) |  ~ (ra_Px34(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC90(v15) = v16) |  ~ (cC88(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC88(v15) = v16) |  ~ (cC86(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px23(v15, v17) = 0) |  ~ (cC84(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC84(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC82xcomp(v15) = v16) |  ~ (ra_Px25(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC82(v15) = v16) |  ~ (cC80(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px20(v15, v17) = 0) |  ~ (cC78(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC78(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px18(v15, v17) = 0) |  ~ (cC74(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC74(v15) = v16) |  ~ (cC72(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px33(v15, v17) = 0) |  ~ (cC72(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC70(v15) = v16) |  ~ (cC68(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC68(v15) = v16) |  ~ (cC66(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC64(v15) = v16) |  ~ (cC2(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px17(v15, v17) = 0) |  ~ (cC62(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC62(v15) = v16) |  ~ (cC60(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC6xcomp(v17) = 0) |  ~ (cC8(v15) = v16) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC6xcomp(v15) = v16) |  ~ (ra_Px28(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC6(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC58(v15) = v16) |  ~ (cC2(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px14(v15, v17) = 0) |  ~ (cC54(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC54(v15) = v16) |  ~ (cC52(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC52(v15) = v16) |  ~ (ra_Px32(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC50xcomp(v15) = v16) |  ~ (ra_Px13(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC50(v15) = v16) |  ~ (cC2(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px12(v15, v17) = 0) |  ~ (cC48(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC48(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC44xcomp(v15) = v16) |  ~ (ra_Px10(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC44(v15) = v16) |  ~ (cC42(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC42xcomp(v15) = v16) |  ~ (ra_Px31(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC40(v15) = v16) |  ~ (cC38(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC38(v15) = v16) |  ~ (cC36xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px8(v15, v17) = 0) |  ~ (cC36(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC36(v15) = v16) |  ~ (cC2(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC34(v15) = v16) |  ~ (ra_Px9(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC34(v15) = v16) |  ~ (cC32xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC32xcomp(v15) = v16) |  ~ (ra_Px7(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC32(v15) = v16) |  ~ (cC2(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC28(v15) = v16) |  ~ (ra_Px6(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC28(v15) = v16) |  ~ (cC26(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px30(v15, v17) = 0) |  ~ (cC26(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC24(v15) = v16) |  ~ (cC22(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC22(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (ra_Px5(v15, v17) = 0) |  ~ (cC20(v15) = v16)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC20(v15) = v16) |  ~ (cC2xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC2xcomp(v17) = 0) |  ~ (cC4(v15) = v16) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC2(v15) = v16) |  ~ (ra_Px3(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC16(v15) = v16) |  ~ (ra_Px2(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC16(v15) = v16) |  ~ (cC14xcomp(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC14xcomp(v15) = v16) |  ~ (ra_Px1(v15, v17) = 0)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cTOP(v17) = 0) |  ~ (cC14(v15) = v16) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] :  ! [v17] : (v16 = 0 |  ~ (cC12(v15) = v16) |  ~ (cC10(v17) = 0) |  ? [v18] : ( ~ (v18 = 0) & rR1(v15, v17) = v18)) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cTEST(v15) = v16) |  ? [v17] :  ? [v18] : (cC94xcomp(v15) = v18 & cC76(v15) = v17 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC94xcomp(v15) = v16) |  ? [v17] : ra_Px29(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC92(v15) = v16) |  ? [v17] : ra_Px34(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC86(v15) = v16) |  ? [v17] :  ? [v18] : (cC84xcomp(v15) = v17 & cC2xcomp(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC84xcomp(v15) = v16) |  ? [v17] : ra_Px23(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC82(v15) = v16) |  ? [v17] : ra_Px25(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC80(v15) = v16) |  ? [v17] :  ? [v18] : (cC78xcomp(v15) = v17 & cC2xcomp(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC78xcomp(v15) = v16) |  ? [v17] : ra_Px20(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC76(v15) = v16) |  ? [v17] :  ? [v18] : (cC74xcomp(v15) = v17 & cC56(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC74xcomp(v15) = v16) |  ? [v17] : ra_Px18(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC72xcomp(v15) = v16) |  ? [v17] : ra_Px33(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC66(v15) = v16) |  ? [v17] :  ? [v18] : (cC64(v15) = v18 & cC2xcomp(v15) = v17 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC62xcomp(v15) = v16) |  ? [v17] : ra_Px17(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC60(v15) = v16) |  ? [v17] :  ? [v18] : (cC58(v15) = v18 & cC2xcomp(v15) = v17 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC6(v15) = v16) |  ? [v17] : ra_Px28(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC56(v15) = v16) |  ? [v17] :  ? [v18] : (cC54xcomp(v15) = v17 & cC46(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC54xcomp(v15) = v16) |  ? [v17] : ra_Px14(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC52xcomp(v15) = v16) |  ? [v17] : ra_Px32(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC50(v15) = v16) |  ? [v17] : ra_Px13(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC48xcomp(v15) = v16) |  ? [v17] : ra_Px12(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC46(v15) = v16) |  ? [v17] :  ? [v18] : (cC44xcomp(v15) = v17 & cC30(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC44(v15) = v16) |  ? [v17] : ra_Px10(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC42(v15) = v16) |  ? [v17] : ra_Px31(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC36xcomp(v15) = v16) |  ? [v17] : ra_Px8(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC34xcomp(v15) = v16) |  ? [v17] : ra_Px9(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC32(v15) = v16) |  ? [v17] : ra_Px7(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC30(v15) = v16) |  ? [v17] :  ? [v18] : (cC28xcomp(v15) = v18 & cC18(v15) = v17 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC28xcomp(v15) = v16) |  ? [v17] : ra_Px6(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC26xcomp(v15) = v16) |  ? [v17] : ra_Px30(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC20xcomp(v15) = v16) |  ? [v17] : ra_Px5(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC2xcomp(v15) = v16) |  ? [v17] : ra_Px3(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC18(v15) = v16) |  ? [v17] :  ? [v18] : (cC16xcomp(v15) = v17 & cC12(v15) = v18 & ( ~ (v18 = 0) |  ~ (v17 = 0)))) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC16xcomp(v15) = v16) |  ? [v17] : ra_Px2(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cC14(v15) = v16) |  ? [v17] : ra_Px1(v15, v17) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (xsd_string(v15) = v16) | xsd_integer(v15) = 0) &  ! [v15] :  ! [v16] : (v16 = 0 |  ~ (cowlThing(v15) = v16)) &  ! [v15] :  ! [v16] : ( ~ (cC94xcomp(v15) = 0) |  ~ (ra_Px29(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (ra_Px34(v15, v16) = 0) |  ~ (cC92(v15) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC90(v15) = v16) |  ? [v17] :  ? [v18] : (cC92(v15) = v17 & cC82xcomp(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] :  ! [v16] : ( ~ (cC84xcomp(v15) = 0) |  ~ (ra_Px23(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC82(v15) = 0) |  ~ (ra_Px25(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC78xcomp(v15) = 0) |  ~ (ra_Px20(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC74xcomp(v15) = 0) |  ~ (ra_Px18(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC72xcomp(v15) = 0) |  ~ (ra_Px33(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC70(v15) = v16) |  ? [v17] :  ? [v18] : (cC72(v15) = v17 & cC62xcomp(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] :  ! [v16] : ( ~ (cC62xcomp(v15) = 0) |  ~ (ra_Px17(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC6(v15) = 0) |  ~ (ra_Px28(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC54xcomp(v15) = 0) |  ~ (ra_Px14(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC52xcomp(v15) = 0) |  ~ (ra_Px32(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC50xcomp(v15) = v16) |  ? [v17] :  ? [v18] : (cC52(v15) = v17 & cC48xcomp(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] :  ! [v16] : ( ~ (cC50(v15) = 0) |  ~ (ra_Px13(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC48xcomp(v15) = 0) |  ~ (ra_Px12(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC44(v15) = 0) |  ~ (ra_Px10(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC42(v15) = 0) |  ~ (ra_Px31(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC40(v15) = v16) |  ? [v17] :  ? [v18] : (cC42(v15) = v17 & cC34xcomp(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] :  ! [v16] : ( ~ (cC36xcomp(v15) = 0) |  ~ (ra_Px8(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC34xcomp(v15) = 0) |  ~ (ra_Px9(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (ra_Px7(v15, v16) = 0) |  ~ (cC32(v15) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC28xcomp(v15) = 0) |  ~ (ra_Px6(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC26xcomp(v15) = 0) |  ~ (ra_Px30(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC24(v15) = v16) |  ? [v17] :  ? [v18] : (cC26(v15) = v17 & cC20xcomp(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] :  ! [v16] : ( ~ (cC20xcomp(v15) = 0) |  ~ (ra_Px5(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC2xcomp(v15) = 0) |  ~ (ra_Px3(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC16xcomp(v15) = 0) |  ~ (ra_Px2(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC14(v15) = 0) |  ~ (ra_Px1(v15, v16) = 0)) &  ! [v15] :  ! [v16] : ( ~ (cC8(v15) = v16) |  ? [v17] :  ? [v18] : (cC10(v15) = v17 & cC4(v15) = v18 & ( ~ (v17 = 0) | (v18 = 0 & v16 = 0)))) &  ! [v15] : ( ~ (cTEST(v15) = 0) | (cC94xcomp(v15) = 0 & cC76(v15) = 0)) &  ! [v15] : ( ~ (cC94(v15) = 0) |  ? [v16] : ra_Px29(v15, v16) = 0) &  ! [v15] : ( ~ (cC94(v15) = 0) |  ? [v16] : (cC92(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC92xcomp(v15) = 0) |  ? [v16] : ra_Px34(v15, v16) = 0) &  ! [v15] : ( ~ (cC90(v15) = 0) |  ? [v16] :  ? [v17] : (cC92(v15) = v17 & cC82xcomp(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC90(v15) = 0) |  ? [v16] : (cC88(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC88(v15) = 0) |  ? [v16] : (cC86(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC86(v15) = 0) | (cC84xcomp(v15) = 0 & cC2xcomp(v15) = 0)) &  ! [v15] : ( ~ (cC84(v15) = 0) |  ? [v16] : ra_Px23(v15, v16) = 0) &  ! [v15] : ( ~ (cC84(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC82xcomp(v15) = 0) |  ? [v16] : ra_Px25(v15, v16) = 0) &  ! [v15] : ( ~ (cC82(v15) = 0) |  ? [v16] : (cC80(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC80(v15) = 0) | (cC78xcomp(v15) = 0 & cC2xcomp(v15) = 0)) &  ! [v15] : ( ~ (cC78(v15) = 0) |  ? [v16] : ra_Px20(v15, v16) = 0) &  ! [v15] : ( ~ (cC78(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC76(v15) = 0) | (cC74xcomp(v15) = 0 & cC56(v15) = 0)) &  ! [v15] : ( ~ (cC74(v15) = 0) |  ? [v16] : ra_Px18(v15, v16) = 0) &  ! [v15] : ( ~ (cC74(v15) = 0) |  ? [v16] : (cC72(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC72(v15) = 0) |  ? [v16] : ra_Px33(v15, v16) = 0) &  ! [v15] : ( ~ (cC70(v15) = 0) |  ? [v16] :  ? [v17] : (cC72(v15) = v17 & cC62xcomp(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC70(v15) = 0) |  ? [v16] : (cC68(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC68(v15) = 0) |  ? [v16] : (cC66(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC66(v15) = 0) | (cC64(v15) = 0 & cC2xcomp(v15) = 0)) &  ! [v15] : ( ~ (cC64(v15) = 0) |  ? [v16] : (cC2(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC62(v15) = 0) |  ? [v16] : ra_Px17(v15, v16) = 0) &  ! [v15] : ( ~ (cC62(v15) = 0) |  ? [v16] : (cC60(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC60(v15) = 0) | (cC58(v15) = 0 & cC2xcomp(v15) = 0)) &  ! [v15] : ( ~ (cC6xcomp(v15) = 0) |  ? [v16] : ra_Px28(v15, v16) = 0) &  ! [v15] : ( ~ (cC6(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC58(v15) = 0) |  ? [v16] : (cC2(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC56(v15) = 0) | (cC54xcomp(v15) = 0 & cC46(v15) = 0)) &  ! [v15] : ( ~ (cC54(v15) = 0) |  ? [v16] : ra_Px14(v15, v16) = 0) &  ! [v15] : ( ~ (cC54(v15) = 0) |  ? [v16] : (cC52(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC52(v15) = 0) |  ? [v16] : ra_Px32(v15, v16) = 0) &  ! [v15] : ( ~ (cC50xcomp(v15) = 0) |  ? [v16] :  ? [v17] : (cC52(v15) = v17 & cC48xcomp(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC50xcomp(v15) = 0) |  ? [v16] : ra_Px13(v15, v16) = 0) &  ! [v15] : ( ~ (cC50(v15) = 0) |  ? [v16] : (cC2(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC48(v15) = 0) |  ? [v16] : ra_Px12(v15, v16) = 0) &  ! [v15] : ( ~ (cC48(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC46(v15) = 0) | (cC44xcomp(v15) = 0 & cC30(v15) = 0)) &  ! [v15] : ( ~ (cC44xcomp(v15) = 0) |  ? [v16] : ra_Px10(v15, v16) = 0) &  ! [v15] : ( ~ (cC44(v15) = 0) |  ? [v16] : (cC42(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC42xcomp(v15) = 0) |  ? [v16] : ra_Px31(v15, v16) = 0) &  ! [v15] : ( ~ (cC40(v15) = 0) |  ? [v16] :  ? [v17] : (cC42(v15) = v17 & cC34xcomp(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC40(v15) = 0) |  ? [v16] : (cC38(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC38(v15) = 0) |  ? [v16] : (cC36xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC36(v15) = 0) |  ? [v16] : ra_Px8(v15, v16) = 0) &  ! [v15] : ( ~ (cC36(v15) = 0) |  ? [v16] : (cC2(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC34(v15) = 0) |  ? [v16] : ra_Px9(v15, v16) = 0) &  ! [v15] : ( ~ (cC34(v15) = 0) |  ? [v16] : (cC32xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC32xcomp(v15) = 0) |  ? [v16] : ra_Px7(v15, v16) = 0) &  ! [v15] : ( ~ (cC32(v15) = 0) |  ? [v16] : (cC2(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC30(v15) = 0) | (cC28xcomp(v15) = 0 & cC18(v15) = 0)) &  ! [v15] : ( ~ (cC28(v15) = 0) |  ? [v16] : ra_Px6(v15, v16) = 0) &  ! [v15] : ( ~ (cC28(v15) = 0) |  ? [v16] : (cC26(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC26(v15) = 0) |  ? [v16] : ra_Px30(v15, v16) = 0) &  ! [v15] : ( ~ (cC24(v15) = 0) |  ? [v16] :  ? [v17] : (cC26(v15) = v17 & cC20xcomp(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC24(v15) = 0) |  ? [v16] : (cC22(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC22(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC20(v15) = 0) |  ? [v16] : ra_Px5(v15, v16) = 0) &  ! [v15] : ( ~ (cC20(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC2(v15) = 0) |  ? [v16] : ra_Px3(v15, v16) = 0) &  ! [v15] : ( ~ (cC18(v15) = 0) | (cC16xcomp(v15) = 0 & cC12(v15) = 0)) &  ! [v15] : ( ~ (cC16(v15) = 0) |  ? [v16] : ra_Px2(v15, v16) = 0) &  ! [v15] : ( ~ (cC16(v15) = 0) |  ? [v16] : (cC14xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC14xcomp(v15) = 0) |  ? [v16] : ra_Px1(v15, v16) = 0) &  ! [v15] : ( ~ (cC14(v15) = 0) |  ? [v16] : (cTOP(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC12(v15) = 0) |  ? [v16] : (rR1(v15, v16) = 0 & cC10(v16) = 0)) &  ! [v15] : ( ~ (rR1(iV8474, v15) = 0) | cC2xcomp(v15) = 0) &  ! [v15] : ( ~ (rR1(iV8469, v15) = 0) | cC2(v15) = 0) &  ! [v15] : ( ~ (rR1(iV8471, v15) = 0) | cC2(v15) = 0) &  ! [v15] : ( ~ (cC8(v15) = 0) |  ? [v16] :  ? [v17] : (cC10(v15) = v17 & cC4(v15) = v16 & ( ~ (v16 = 0) | v17 = 0))) &  ! [v15] : ( ~ (cC8(v15) = 0) |  ? [v16] : (cC6xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (cC4(v15) = 0) |  ? [v16] : (cC2xcomp(v16) = 0 & rR1(v15, v16) = 0)) &  ! [v15] : ( ~ (xsd_string(v15) = 0) |  ? [v16] : ( ~ (v16 = 0) & xsd_integer(v15) = v16)) &  ! [v15] :  ~ (cowlNothing(v15) = 0) & ( ~ (v11 = 0) |  ~ (v10 = 0) |  ~ (v9 = 0) |  ~ (v8 = 0) |  ~ (v7 = 0) |  ~ (v6 = 0) |  ~ (v5 = 0) |  ~ (v4 = 0) |  ~ (v3 = 0) |  ~ (v2 = 0) |  ~ (v1 = 0) |  ~ (v0 = 0) | (xsd_string(v12) = v13 & xsd_integer(v12) = v14 & ((v14 = 0 & v13 = 0) | ( ~ (v14 = 0) &  ~ (v13 = 0)))) | (cowlNothing(v12) = v14 & cowlThing(v12) = v13 & ( ~ (v13 = 0) | v14 = 0))))
% 29.57/8.14  | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14 yields:
% 29.57/8.14  | (1) cC92xcomp(iV8467) = 0 & cC82(iV8467) = all_0_11_11 & cC80(iV8471) = all_0_5_5 & cC78xcomp(iV8471) = 0 & cC72xcomp(iV8467) = 0 & cC62(iV8467) = all_0_10_10 & cC60(iV8472) = all_0_3_3 & cC6xcomp(iV8469) = 0 & cC58(iV8472) = all_0_4_4 & cC52xcomp(iV8467) = 0 & cC48(iV8467) = all_0_6_6 & cC42xcomp(iV8467) = 0 & cC34(iV8467) = all_0_8_8 & cC32xcomp(iV8474) = 0 & cC26xcomp(iV8467) = 0 & cC20(iV8467) = all_0_14_14 & cC2xcomp(iV8472) = 0 & cC2xcomp(iV8475) = 0 & cC2xcomp(iV8473) = 0 & cC2xcomp(iV8468) = 0 & cC2xcomp(iV8471) = 0 & cC2(iV8476) = 0 & cTOP(iV8470) = 0 & cC14(iV8467) = all_0_9_9 & rR1(iV8472, iV8476) = 0 & rR1(iV8467, iV8472) = 0 & rR1(iV8467, iV8475) = 0 & rR1(iV8467, iV8473) = 0 & rR1(iV8467, iV8468) = 0 & rR1(iV8467, iV8474) = 0 & rR1(iV8467, iV8469) = 0 & rR1(iV8467, iV8470) = 0 & rR1(iV8467, iV8471) = 0 & cC8(iV8467) = all_0_12_12 & cC10(iV8467) = all_0_7_7 & cC4(iV8467) = all_0_13_13 & cowlThing(iV8476) = 0 & cowlThing(iV8472) = 0 & cowlThing(iV8475) = 0 & cowlThing(iV8473) = 0 & cowlThing(iV8468) = 0 & cowlThing(iV8474) = 0 & cowlThing(iV8469) = 0 & cowlThing(iV8470) = 0 & cowlThing(iV8471) = 0 & cowlThing(iV8467) = 0 &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px29(v3, v2) = v1) |  ~ (ra_Px29(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px34(v3, v2) = v1) |  ~ (ra_Px34(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px23(v3, v2) = v1) |  ~ (ra_Px23(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px25(v3, v2) = v1) |  ~ (ra_Px25(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px20(v3, v2) = v1) |  ~ (ra_Px20(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px18(v3, v2) = v1) |  ~ (ra_Px18(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px33(v3, v2) = v1) |  ~ (ra_Px33(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px17(v3, v2) = v1) |  ~ (ra_Px17(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px28(v3, v2) = v1) |  ~ (ra_Px28(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px14(v3, v2) = v1) |  ~ (ra_Px14(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px32(v3, v2) = v1) |  ~ (ra_Px32(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px13(v3, v2) = v1) |  ~ (ra_Px13(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px12(v3, v2) = v1) |  ~ (ra_Px12(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px10(v3, v2) = v1) |  ~ (ra_Px10(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px31(v3, v2) = v1) |  ~ (ra_Px31(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px8(v3, v2) = v1) |  ~ (ra_Px8(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px9(v3, v2) = v1) |  ~ (ra_Px9(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px7(v3, v2) = v1) |  ~ (ra_Px7(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px6(v3, v2) = v1) |  ~ (ra_Px6(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px30(v3, v2) = v1) |  ~ (ra_Px30(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px5(v3, v2) = v1) |  ~ (ra_Px5(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px3(v3, v2) = v1) |  ~ (ra_Px3(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px2(v3, v2) = v1) |  ~ (ra_Px2(v3, v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px1(v3, v2) = v1) |  ~ (ra_Px1(v3, v2) = v0)) &  ! [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 |  ~ (cC94xcomp(v2) = v1) |  ~ (cC94xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC94(v2) = v1) |  ~ (cC94(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC92xcomp(v2) = v1) |  ~ (cC92xcomp(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 |  ~ (cC84xcomp(v2) = v1) |  ~ (cC84xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC84(v2) = v1) |  ~ (cC84(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC82xcomp(v2) = v1) |  ~ (cC82xcomp(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 |  ~ (cC78xcomp(v2) = v1) |  ~ (cC78xcomp(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 |  ~ (cC74xcomp(v2) = v1) |  ~ (cC74xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC74(v2) = v1) |  ~ (cC74(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC72xcomp(v2) = v1) |  ~ (cC72xcomp(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 |  ~ (cC64(v2) = v1) |  ~ (cC64(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC62xcomp(v2) = v1) |  ~ (cC62xcomp(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 |  ~ (cC6xcomp(v2) = v1) |  ~ (cC6xcomp(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 |  ~ (cC54xcomp(v2) = v1) |  ~ (cC54xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC54(v2) = v1) |  ~ (cC54(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC52xcomp(v2) = v1) |  ~ (cC52xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC52(v2) = v1) |  ~ (cC52(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC50xcomp(v2) = v1) |  ~ (cC50xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC50(v2) = v1) |  ~ (cC50(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC48xcomp(v2) = v1) |  ~ (cC48xcomp(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 |  ~ (cC44xcomp(v2) = v1) |  ~ (cC44xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC44(v2) = v1) |  ~ (cC44(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC42xcomp(v2) = v1) |  ~ (cC42xcomp(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 |  ~ (cC38(v2) = v1) |  ~ (cC38(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC36xcomp(v2) = v1) |  ~ (cC36xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC36(v2) = v1) |  ~ (cC36(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC34xcomp(v2) = v1) |  ~ (cC34xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC34(v2) = v1) |  ~ (cC34(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC32xcomp(v2) = v1) |  ~ (cC32xcomp(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 |  ~ (cC28xcomp(v2) = v1) |  ~ (cC28xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC28(v2) = v1) |  ~ (cC28(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC26xcomp(v2) = v1) |  ~ (cC26xcomp(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 |  ~ (cC20xcomp(v2) = v1) |  ~ (cC20xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC20(v2) = v1) |  ~ (cC20(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC2xcomp(v2) = v1) |  ~ (cC2xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC2(v2) = v1) |  ~ (cC2(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC18(v2) = v1) |  ~ (cC18(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC16xcomp(v2) = v1) |  ~ (cC16xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC16(v2) = v1) |  ~ (cC16(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC14xcomp(v2) = v1) |  ~ (cC14xcomp(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cTOP(v2) = v1) |  ~ (cTOP(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC14(v2) = v1) |  ~ (cC14(v2) = v0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC12(v2) = v1) |  ~ (cC12(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 |  ~ (cC4(v2) = v1) |  ~ (cC4(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) |  ~ (ra_Px29(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC94(v0) = v1) |  ~ (cC92(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC92xcomp(v0) = v1) |  ~ (ra_Px34(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC90(v0) = v1) |  ~ (cC88(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC88(v0) = v1) |  ~ (cC86(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px23(v0, v2) = 0) |  ~ (cC84(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC84(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC82xcomp(v0) = v1) |  ~ (ra_Px25(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC82(v0) = v1) |  ~ (cC80(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px20(v0, v2) = 0) |  ~ (cC78(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC78(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px18(v0, v2) = 0) |  ~ (cC74(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC74(v0) = v1) |  ~ (cC72(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px33(v0, v2) = 0) |  ~ (cC72(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC70(v0) = v1) |  ~ (cC68(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC68(v0) = v1) |  ~ (cC66(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC64(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px17(v0, v2) = 0) |  ~ (cC62(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC62(v0) = v1) |  ~ (cC60(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6xcomp(v2) = 0) |  ~ (cC8(v0) = v1) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6xcomp(v0) = v1) |  ~ (ra_Px28(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC58(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px14(v0, v2) = 0) |  ~ (cC54(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC54(v0) = v1) |  ~ (cC52(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC52(v0) = v1) |  ~ (ra_Px32(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC50xcomp(v0) = v1) |  ~ (ra_Px13(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC50(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px12(v0, v2) = 0) |  ~ (cC48(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC48(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC44xcomp(v0) = v1) |  ~ (ra_Px10(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC44(v0) = v1) |  ~ (cC42(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC42xcomp(v0) = v1) |  ~ (ra_Px31(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC40(v0) = v1) |  ~ (cC38(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC38(v0) = v1) |  ~ (cC36xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px8(v0, v2) = 0) |  ~ (cC36(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC36(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC34(v0) = v1) |  ~ (ra_Px9(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC34(v0) = v1) |  ~ (cC32xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC32xcomp(v0) = v1) |  ~ (ra_Px7(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC32(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC28(v0) = v1) |  ~ (ra_Px6(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC28(v0) = v1) |  ~ (cC26(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px30(v0, v2) = 0) |  ~ (cC26(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC24(v0) = v1) |  ~ (cC22(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC22(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px5(v0, v2) = 0) |  ~ (cC20(v0) = v1)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC20(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC2xcomp(v2) = 0) |  ~ (cC4(v0) = v1) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC2(v0) = v1) |  ~ (ra_Px3(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC16(v0) = v1) |  ~ (ra_Px2(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC16(v0) = v1) |  ~ (cC14xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC14xcomp(v0) = v1) |  ~ (ra_Px1(v0, v2) = 0)) &  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cTOP(v2) = 0) |  ~ (cC14(v0) = v1) |  ? [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] : (v1 = 0 |  ~ (cTEST(v0) = v1) |  ? [v2] :  ? [v3] : (cC94xcomp(v0) = v3 & cC76(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC94xcomp(v0) = v1) |  ? [v2] : ra_Px29(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC92(v0) = v1) |  ? [v2] : ra_Px34(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC86(v0) = v1) |  ? [v2] :  ? [v3] : (cC84xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC84xcomp(v0) = v1) |  ? [v2] : ra_Px23(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC82(v0) = v1) |  ? [v2] : ra_Px25(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC80(v0) = v1) |  ? [v2] :  ? [v3] : (cC78xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC78xcomp(v0) = v1) |  ? [v2] : ra_Px20(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC76(v0) = v1) |  ? [v2] :  ? [v3] : (cC74xcomp(v0) = v2 & cC56(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC74xcomp(v0) = v1) |  ? [v2] : ra_Px18(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC72xcomp(v0) = v1) |  ? [v2] : ra_Px33(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC66(v0) = v1) |  ? [v2] :  ? [v3] : (cC64(v0) = v3 & cC2xcomp(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC62xcomp(v0) = v1) |  ? [v2] : ra_Px17(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC60(v0) = v1) |  ? [v2] :  ? [v3] : (cC58(v0) = v3 & cC2xcomp(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC6(v0) = v1) |  ? [v2] : ra_Px28(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC56(v0) = v1) |  ? [v2] :  ? [v3] : (cC54xcomp(v0) = v2 & cC46(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC54xcomp(v0) = v1) |  ? [v2] : ra_Px14(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC52xcomp(v0) = v1) |  ? [v2] : ra_Px32(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC50(v0) = v1) |  ? [v2] : ra_Px13(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC48xcomp(v0) = v1) |  ? [v2] : ra_Px12(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC46(v0) = v1) |  ? [v2] :  ? [v3] : (cC44xcomp(v0) = v2 & cC30(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC44(v0) = v1) |  ? [v2] : ra_Px10(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC42(v0) = v1) |  ? [v2] : ra_Px31(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC36xcomp(v0) = v1) |  ? [v2] : ra_Px8(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC34xcomp(v0) = v1) |  ? [v2] : ra_Px9(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC32(v0) = v1) |  ? [v2] : ra_Px7(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC30(v0) = v1) |  ? [v2] :  ? [v3] : (cC28xcomp(v0) = v3 & cC18(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC28xcomp(v0) = v1) |  ? [v2] : ra_Px6(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC26xcomp(v0) = v1) |  ? [v2] : ra_Px30(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC20xcomp(v0) = v1) |  ? [v2] : ra_Px5(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC2xcomp(v0) = v1) |  ? [v2] : ra_Px3(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC18(v0) = v1) |  ? [v2] :  ? [v3] : (cC16xcomp(v0) = v2 & cC12(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0)))) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC16xcomp(v0) = v1) |  ? [v2] : ra_Px2(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC14(v0) = v1) |  ? [v2] : ra_Px1(v0, v2) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0) &  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cowlThing(v0) = v1)) &  ! [v0] :  ! [v1] : ( ~ (cC94xcomp(v0) = 0) |  ~ (ra_Px29(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (ra_Px34(v0, v1) = 0) |  ~ (cC92(v0) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC90(v0) = v1) |  ? [v2] :  ? [v3] : (cC92(v0) = v2 & cC82xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] :  ! [v1] : ( ~ (cC84xcomp(v0) = 0) |  ~ (ra_Px23(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC82(v0) = 0) |  ~ (ra_Px25(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC78xcomp(v0) = 0) |  ~ (ra_Px20(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC74xcomp(v0) = 0) |  ~ (ra_Px18(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC72xcomp(v0) = 0) |  ~ (ra_Px33(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC70(v0) = v1) |  ? [v2] :  ? [v3] : (cC72(v0) = v2 & cC62xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] :  ! [v1] : ( ~ (cC62xcomp(v0) = 0) |  ~ (ra_Px17(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC6(v0) = 0) |  ~ (ra_Px28(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC54xcomp(v0) = 0) |  ~ (ra_Px14(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC52xcomp(v0) = 0) |  ~ (ra_Px32(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC50xcomp(v0) = v1) |  ? [v2] :  ? [v3] : (cC52(v0) = v2 & cC48xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] :  ! [v1] : ( ~ (cC50(v0) = 0) |  ~ (ra_Px13(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC48xcomp(v0) = 0) |  ~ (ra_Px12(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC44(v0) = 0) |  ~ (ra_Px10(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC42(v0) = 0) |  ~ (ra_Px31(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC40(v0) = v1) |  ? [v2] :  ? [v3] : (cC42(v0) = v2 & cC34xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] :  ! [v1] : ( ~ (cC36xcomp(v0) = 0) |  ~ (ra_Px8(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC34xcomp(v0) = 0) |  ~ (ra_Px9(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (ra_Px7(v0, v1) = 0) |  ~ (cC32(v0) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC28xcomp(v0) = 0) |  ~ (ra_Px6(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC26xcomp(v0) = 0) |  ~ (ra_Px30(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC24(v0) = v1) |  ? [v2] :  ? [v3] : (cC26(v0) = v2 & cC20xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] :  ! [v1] : ( ~ (cC20xcomp(v0) = 0) |  ~ (ra_Px5(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC2xcomp(v0) = 0) |  ~ (ra_Px3(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC16xcomp(v0) = 0) |  ~ (ra_Px2(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC14(v0) = 0) |  ~ (ra_Px1(v0, v1) = 0)) &  ! [v0] :  ! [v1] : ( ~ (cC8(v0) = v1) |  ? [v2] :  ? [v3] : (cC10(v0) = v2 & cC4(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0)))) &  ! [v0] : ( ~ (cTEST(v0) = 0) | (cC94xcomp(v0) = 0 & cC76(v0) = 0)) &  ! [v0] : ( ~ (cC94(v0) = 0) |  ? [v1] : ra_Px29(v0, v1) = 0) &  ! [v0] : ( ~ (cC94(v0) = 0) |  ? [v1] : (cC92(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC92xcomp(v0) = 0) |  ? [v1] : ra_Px34(v0, v1) = 0) &  ! [v0] : ( ~ (cC90(v0) = 0) |  ? [v1] :  ? [v2] : (cC92(v0) = v2 & cC82xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC90(v0) = 0) |  ? [v1] : (cC88(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC88(v0) = 0) |  ? [v1] : (cC86(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC86(v0) = 0) | (cC84xcomp(v0) = 0 & cC2xcomp(v0) = 0)) &  ! [v0] : ( ~ (cC84(v0) = 0) |  ? [v1] : ra_Px23(v0, v1) = 0) &  ! [v0] : ( ~ (cC84(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC82xcomp(v0) = 0) |  ? [v1] : ra_Px25(v0, v1) = 0) &  ! [v0] : ( ~ (cC82(v0) = 0) |  ? [v1] : (cC80(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC80(v0) = 0) | (cC78xcomp(v0) = 0 & cC2xcomp(v0) = 0)) &  ! [v0] : ( ~ (cC78(v0) = 0) |  ? [v1] : ra_Px20(v0, v1) = 0) &  ! [v0] : ( ~ (cC78(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC76(v0) = 0) | (cC74xcomp(v0) = 0 & cC56(v0) = 0)) &  ! [v0] : ( ~ (cC74(v0) = 0) |  ? [v1] : ra_Px18(v0, v1) = 0) &  ! [v0] : ( ~ (cC74(v0) = 0) |  ? [v1] : (cC72(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC72(v0) = 0) |  ? [v1] : ra_Px33(v0, v1) = 0) &  ! [v0] : ( ~ (cC70(v0) = 0) |  ? [v1] :  ? [v2] : (cC72(v0) = v2 & cC62xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC70(v0) = 0) |  ? [v1] : (cC68(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC68(v0) = 0) |  ? [v1] : (cC66(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC66(v0) = 0) | (cC64(v0) = 0 & cC2xcomp(v0) = 0)) &  ! [v0] : ( ~ (cC64(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC62(v0) = 0) |  ? [v1] : ra_Px17(v0, v1) = 0) &  ! [v0] : ( ~ (cC62(v0) = 0) |  ? [v1] : (cC60(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC60(v0) = 0) | (cC58(v0) = 0 & cC2xcomp(v0) = 0)) &  ! [v0] : ( ~ (cC6xcomp(v0) = 0) |  ? [v1] : ra_Px28(v0, v1) = 0) &  ! [v0] : ( ~ (cC6(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC58(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC56(v0) = 0) | (cC54xcomp(v0) = 0 & cC46(v0) = 0)) &  ! [v0] : ( ~ (cC54(v0) = 0) |  ? [v1] : ra_Px14(v0, v1) = 0) &  ! [v0] : ( ~ (cC54(v0) = 0) |  ? [v1] : (cC52(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC52(v0) = 0) |  ? [v1] : ra_Px32(v0, v1) = 0) &  ! [v0] : ( ~ (cC50xcomp(v0) = 0) |  ? [v1] :  ? [v2] : (cC52(v0) = v2 & cC48xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC50xcomp(v0) = 0) |  ? [v1] : ra_Px13(v0, v1) = 0) &  ! [v0] : ( ~ (cC50(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC48(v0) = 0) |  ? [v1] : ra_Px12(v0, v1) = 0) &  ! [v0] : ( ~ (cC48(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC46(v0) = 0) | (cC44xcomp(v0) = 0 & cC30(v0) = 0)) &  ! [v0] : ( ~ (cC44xcomp(v0) = 0) |  ? [v1] : ra_Px10(v0, v1) = 0) &  ! [v0] : ( ~ (cC44(v0) = 0) |  ? [v1] : (cC42(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC42xcomp(v0) = 0) |  ? [v1] : ra_Px31(v0, v1) = 0) &  ! [v0] : ( ~ (cC40(v0) = 0) |  ? [v1] :  ? [v2] : (cC42(v0) = v2 & cC34xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC40(v0) = 0) |  ? [v1] : (cC38(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC38(v0) = 0) |  ? [v1] : (cC36xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC36(v0) = 0) |  ? [v1] : ra_Px8(v0, v1) = 0) &  ! [v0] : ( ~ (cC36(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC34(v0) = 0) |  ? [v1] : ra_Px9(v0, v1) = 0) &  ! [v0] : ( ~ (cC34(v0) = 0) |  ? [v1] : (cC32xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC32xcomp(v0) = 0) |  ? [v1] : ra_Px7(v0, v1) = 0) &  ! [v0] : ( ~ (cC32(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC30(v0) = 0) | (cC28xcomp(v0) = 0 & cC18(v0) = 0)) &  ! [v0] : ( ~ (cC28(v0) = 0) |  ? [v1] : ra_Px6(v0, v1) = 0) &  ! [v0] : ( ~ (cC28(v0) = 0) |  ? [v1] : (cC26(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC26(v0) = 0) |  ? [v1] : ra_Px30(v0, v1) = 0) &  ! [v0] : ( ~ (cC24(v0) = 0) |  ? [v1] :  ? [v2] : (cC26(v0) = v2 & cC20xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC24(v0) = 0) |  ? [v1] : (cC22(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC22(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC20(v0) = 0) |  ? [v1] : ra_Px5(v0, v1) = 0) &  ! [v0] : ( ~ (cC20(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC2(v0) = 0) |  ? [v1] : ra_Px3(v0, v1) = 0) &  ! [v0] : ( ~ (cC18(v0) = 0) | (cC16xcomp(v0) = 0 & cC12(v0) = 0)) &  ! [v0] : ( ~ (cC16(v0) = 0) |  ? [v1] : ra_Px2(v0, v1) = 0) &  ! [v0] : ( ~ (cC16(v0) = 0) |  ? [v1] : (cC14xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC14xcomp(v0) = 0) |  ? [v1] : ra_Px1(v0, v1) = 0) &  ! [v0] : ( ~ (cC14(v0) = 0) |  ? [v1] : (cTOP(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC12(v0) = 0) |  ? [v1] : (rR1(v0, v1) = 0 & cC10(v1) = 0)) &  ! [v0] : ( ~ (rR1(iV8474, v0) = 0) | cC2xcomp(v0) = 0) &  ! [v0] : ( ~ (rR1(iV8469, v0) = 0) | cC2(v0) = 0) &  ! [v0] : ( ~ (rR1(iV8471, v0) = 0) | cC2(v0) = 0) &  ! [v0] : ( ~ (cC8(v0) = 0) |  ? [v1] :  ? [v2] : (cC10(v0) = v2 & cC4(v0) = v1 & ( ~ (v1 = 0) | v2 = 0))) &  ! [v0] : ( ~ (cC8(v0) = 0) |  ? [v1] : (cC6xcomp(v1) = 0 & rR1(v0, v1) = 0)) &  ! [v0] : ( ~ (cC4(v0) = 0) |  ? [v1] : (cC2xcomp(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) |  ~ (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) | (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)))
% 29.57/8.18  |
% 29.57/8.18  | Applying alpha-rule on (1) yields:
% 29.57/8.18  | (2)  ! [v0] :  ! [v1] : ( ~ (cC34xcomp(v0) = 0) |  ~ (ra_Px9(v0, v1) = 0))
% 29.57/8.18  | (3)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC52xcomp(v2) = v1) |  ~ (cC52xcomp(v2) = v0))
% 29.57/8.18  | (4) cowlThing(iV8475) = 0
% 29.57/8.18  | (5) cC48(iV8467) = all_0_6_6
% 29.57/8.18  | (6)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC74(v0) = v1) |  ~ (cC72(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.57/8.18  | (7)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC94xcomp(v0) = v1) |  ? [v2] : ra_Px29(v0, v2) = 0)
% 29.57/8.18  | (8)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC32(v0) = v1) |  ? [v2] : ra_Px7(v0, v2) = 0)
% 29.57/8.18  | (9)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC2(v2) = v1) |  ~ (cC2(v2) = v0))
% 29.57/8.18  | (10)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC6xcomp(v2) = v1) |  ~ (cC6xcomp(v2) = v0))
% 29.57/8.18  | (11)  ! [v0] : ( ~ (cTEST(v0) = 0) | (cC94xcomp(v0) = 0 & cC76(v0) = 0))
% 29.57/8.18  | (12)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC2xcomp(v0) = v1) |  ? [v2] : ra_Px3(v0, v2) = 0)
% 29.57/8.18  | (13)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC72(v2) = v1) |  ~ (cC72(v2) = v0))
% 29.57/8.18  | (14)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC78(v2) = v1) |  ~ (cC78(v2) = v0))
% 29.57/8.18  | (15)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC68(v0) = v1) |  ~ (cC66(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.57/8.18  | (16)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC76(v2) = v1) |  ~ (cC76(v2) = v0))
% 29.57/8.18  | (17)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC32(v2) = v1) |  ~ (cC32(v2) = v0))
% 29.57/8.18  | (18)  ! [v0] : ( ~ (cC2(v0) = 0) |  ? [v1] : ra_Px3(v0, v1) = 0)
% 29.57/8.18  | (19) cC52xcomp(iV8467) = 0
% 29.57/8.18  | (20)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC28(v2) = v1) |  ~ (cC28(v2) = v0))
% 29.57/8.18  | (21)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC34(v2) = v1) |  ~ (cC34(v2) = v0))
% 29.57/8.18  | (22)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC90(v0) = v1) |  ~ (cC88(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.57/8.18  | (23)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC52(v0) = v1) |  ~ (ra_Px32(v0, v2) = 0))
% 29.57/8.18  | (24)  ! [v0] : ( ~ (cC48(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.57/8.18  | (25)  ! [v0] :  ! [v1] : ( ~ (cC78xcomp(v0) = 0) |  ~ (ra_Px20(v0, v1) = 0))
% 29.57/8.18  | (26)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (rR1(v3, v2) = v1) |  ~ (rR1(v3, v2) = v0))
% 29.57/8.18  | (27)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC68(v2) = v1) |  ~ (cC68(v2) = v0))
% 29.57/8.18  | (28)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px10(v3, v2) = v1) |  ~ (ra_Px10(v3, v2) = v0))
% 29.57/8.18  | (29)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0)
% 29.57/8.18  | (30)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC78xcomp(v0) = v1) |  ? [v2] : ra_Px20(v0, v2) = 0)
% 29.57/8.18  | (31)  ! [v0] : ( ~ (cC92xcomp(v0) = 0) |  ? [v1] : ra_Px34(v0, v1) = 0)
% 29.57/8.19  | (32)  ! [v0] : ( ~ (cC38(v0) = 0) |  ? [v1] : (cC36xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.57/8.19  | (33)  ~ (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) |  ~ (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) | (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))
% 29.57/8.19  | (34)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px23(v0, v2) = 0) |  ~ (cC84(v0) = v1))
% 29.57/8.19  | (35)  ! [v0] : ( ~ (cC20(v0) = 0) |  ? [v1] : ra_Px5(v0, v1) = 0)
% 29.57/8.19  | (36) cC80(iV8471) = all_0_5_5
% 29.57/8.19  | (37)  ! [v0] : ( ~ (cC18(v0) = 0) | (cC16xcomp(v0) = 0 & cC12(v0) = 0))
% 29.57/8.19  | (38)  ! [v0] : ( ~ (xsd_string(v0) = 0) |  ? [v1] : ( ~ (v1 = 0) & xsd_integer(v0) = v1))
% 29.57/8.19  | (39)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC82xcomp(v2) = v1) |  ~ (cC82xcomp(v2) = v0))
% 29.57/8.19  | (40)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC16(v0) = v1) |  ~ (cC14xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.57/8.19  | (41)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC84xcomp(v0) = v1) |  ? [v2] : ra_Px23(v0, v2) = 0)
% 29.57/8.19  | (42)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px2(v3, v2) = v1) |  ~ (ra_Px2(v3, v2) = v0))
% 29.57/8.19  | (43)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px18(v3, v2) = v1) |  ~ (ra_Px18(v3, v2) = v0))
% 29.57/8.19  | (44)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC40(v2) = v1) |  ~ (cC40(v2) = v0))
% 29.57/8.19  | (45)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC82xcomp(v0) = v1) |  ~ (ra_Px25(v0, v2) = 0))
% 29.57/8.19  | (46)  ! [v0] : ( ~ (cC54(v0) = 0) |  ? [v1] : (cC52(v1) = 0 & rR1(v0, v1) = 0))
% 29.57/8.19  | (47)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC42xcomp(v0) = v1) |  ~ (ra_Px31(v0, v2) = 0))
% 29.57/8.19  | (48)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px32(v3, v2) = v1) |  ~ (ra_Px32(v3, v2) = v0))
% 29.57/8.19  | (49)  ! [v0] :  ! [v1] : ( ~ (cC20xcomp(v0) = 0) |  ~ (ra_Px5(v0, v1) = 0))
% 29.57/8.19  | (50)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (xsd_string(v2) = v1) |  ~ (xsd_string(v2) = v0))
% 29.57/8.19  | (51)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC24(v0) = v1) |  ~ (cC22(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.57/8.19  | (52)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC26xcomp(v0) = v1) |  ? [v2] : ra_Px30(v0, v2) = 0)
% 29.57/8.19  | (53) cC4(iV8467) = all_0_13_13
% 29.57/8.19  | (54)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC2xcomp(v2) = v1) |  ~ (cC2xcomp(v2) = v0))
% 29.57/8.19  | (55)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC16xcomp(v2) = v1) |  ~ (cC16xcomp(v2) = v0))
% 29.57/8.19  | (56)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px34(v3, v2) = v1) |  ~ (ra_Px34(v3, v2) = v0))
% 29.57/8.19  | (57)  ! [v0] :  ! [v1] : ( ~ (cC50(v0) = 0) |  ~ (ra_Px13(v0, v1) = 0))
% 29.57/8.19  | (58)  ! [v0] :  ! [v1] : ( ~ (cC48xcomp(v0) = 0) |  ~ (ra_Px12(v0, v1) = 0))
% 29.57/8.19  | (59)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px30(v3, v2) = v1) |  ~ (ra_Px30(v3, v2) = v0))
% 29.57/8.19  | (60)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC42(v0) = v1) |  ? [v2] : ra_Px31(v0, v2) = 0)
% 29.57/8.19  | (61)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC42(v2) = v1) |  ~ (cC42(v2) = v0))
% 29.57/8.19  | (62) cowlThing(iV8469) = 0
% 29.57/8.19  | (63)  ! [v0] :  ! [v1] : ( ~ (cC74xcomp(v0) = 0) |  ~ (ra_Px18(v0, v1) = 0))
% 29.57/8.19  | (64)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC94(v2) = v1) |  ~ (cC94(v2) = v0))
% 29.57/8.19  | (65)  ! [v0] : ( ~ (cC44xcomp(v0) = 0) |  ? [v1] : ra_Px10(v0, v1) = 0)
% 29.57/8.19  | (66)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC44xcomp(v0) = v1) |  ~ (ra_Px10(v0, v2) = 0))
% 29.57/8.19  | (67)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC92xcomp(v0) = v1) |  ~ (ra_Px34(v0, v2) = 0))
% 29.57/8.19  | (68)  ! [v0] : ( ~ (cC80(v0) = 0) | (cC78xcomp(v0) = 0 & cC2xcomp(v0) = 0))
% 29.57/8.19  | (69) rR1(iV8467, iV8475) = 0
% 29.57/8.19  | (70)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC34xcomp(v0) = v1) |  ? [v2] : ra_Px9(v0, v2) = 0)
% 29.57/8.19  | (71)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px18(v0, v2) = 0) |  ~ (cC74(v0) = v1))
% 29.57/8.19  | (72)  ! [v0] : ( ~ (cC78(v0) = 0) |  ? [v1] : ra_Px20(v0, v1) = 0)
% 29.57/8.19  | (73)  ! [v0] : ( ~ (rR1(iV8474, v0) = 0) | cC2xcomp(v0) = 0)
% 29.57/8.19  | (74) cC6xcomp(iV8469) = 0
% 29.57/8.19  | (75)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px14(v3, v2) = v1) |  ~ (ra_Px14(v3, v2) = v0))
% 29.57/8.19  | (76)  ! [v0] : ( ~ (cC74(v0) = 0) |  ? [v1] : (cC72(v1) = 0 & rR1(v0, v1) = 0))
% 29.57/8.19  | (77)  ! [v0] :  ! [v1] : ( ~ (ra_Px7(v0, v1) = 0) |  ~ (cC32(v0) = 0))
% 29.57/8.19  | (78) rR1(iV8467, iV8471) = 0
% 29.57/8.19  | (79)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC56(v2) = v1) |  ~ (cC56(v2) = v0))
% 29.57/8.19  | (80)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC46(v2) = v1) |  ~ (cC46(v2) = v0))
% 29.57/8.19  | (81)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC44xcomp(v2) = v1) |  ~ (cC44xcomp(v2) = v0))
% 29.57/8.19  | (82)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC54(v2) = v1) |  ~ (cC54(v2) = v0))
% 29.57/8.19  | (83)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC48xcomp(v2) = v1) |  ~ (cC48xcomp(v2) = v0))
% 29.57/8.19  | (84)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC38(v2) = v1) |  ~ (cC38(v2) = v0))
% 29.57/8.19  | (85)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cTOP(v2) = v1) |  ~ (cTOP(v2) = v0))
% 29.57/8.19  | (86)  ! [v0] : ( ~ (cC68(v0) = 0) |  ? [v1] : (cC66(v1) = 0 & rR1(v0, v1) = 0))
% 29.57/8.19  | (87)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC8(v2) = v1) |  ~ (cC8(v2) = v0))
% 29.57/8.19  | (88)  ! [v0] : ( ~ (cC48(v0) = 0) |  ? [v1] : ra_Px12(v0, v1) = 0)
% 29.82/8.19  | (89)  ! [v0] : ( ~ (cC84(v0) = 0) |  ? [v1] : ra_Px23(v0, v1) = 0)
% 29.82/8.19  | (90)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cowlThing(v0) = v1))
% 29.82/8.19  | (91)  ! [v0] : ( ~ (cC50(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.19  | (92)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC72xcomp(v2) = v1) |  ~ (cC72xcomp(v2) = v0))
% 29.82/8.19  | (93)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC50(v0) = v1) |  ? [v2] : ra_Px13(v0, v2) = 0)
% 29.82/8.19  | (94) cC78xcomp(iV8471) = 0
% 29.82/8.19  | (95)  ! [v0] :  ! [v1] : ( ~ (cC28xcomp(v0) = 0) |  ~ (ra_Px6(v0, v1) = 0))
% 29.82/8.19  | (96)  ! [v0] : ( ~ (cC56(v0) = 0) | (cC54xcomp(v0) = 0 & cC46(v0) = 0))
% 29.82/8.19  | (97)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC88(v0) = v1) |  ~ (cC86(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.19  | (98)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px14(v0, v2) = 0) |  ~ (cC54(v0) = v1))
% 29.82/8.19  | (99)  ! [v0] :  ! [v1] : ( ~ (cC82(v0) = 0) |  ~ (ra_Px25(v0, v1) = 0))
% 29.82/8.19  | (100)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC74xcomp(v0) = v1) |  ? [v2] : ra_Px18(v0, v2) = 0)
% 29.82/8.20  | (101)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC32(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (102)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC12(v2) = v1) |  ~ (cC12(v2) = v0))
% 29.82/8.20  | (103)  ! [v0] : ( ~ (cC14(v0) = 0) |  ? [v1] : (cTOP(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (104) cC42xcomp(iV8467) = 0
% 29.82/8.20  | (105)  ! [v0] :  ! [v1] : ( ~ (cC94xcomp(v0) = 0) |  ~ (ra_Px29(v0, v1) = 0))
% 29.82/8.20  | (106)  ! [v0] : ( ~ (cC30(v0) = 0) | (cC28xcomp(v0) = 0 & cC18(v0) = 0))
% 29.82/8.20  | (107)  ! [v0] : ( ~ (cC50xcomp(v0) = 0) |  ? [v1] :  ? [v2] : (cC52(v0) = v2 & cC48xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.20  | (108)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC40(v0) = v1) |  ~ (cC38(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (109)  ! [v0] : ( ~ (cC60(v0) = 0) | (cC58(v0) = 0 & cC2xcomp(v0) = 0))
% 29.82/8.20  | (110)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px33(v0, v2) = 0) |  ~ (cC72(v0) = v1))
% 29.82/8.20  | (111) cC92xcomp(iV8467) = 0
% 29.82/8.20  | (112)  ! [v0] : ( ~ (cC82xcomp(v0) = 0) |  ? [v1] : ra_Px25(v0, v1) = 0)
% 29.82/8.20  | (113)  ! [v0] : ( ~ (cC36(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (114) cC2xcomp(iV8475) = 0
% 29.82/8.20  | (115)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC74(v2) = v1) |  ~ (cC74(v2) = v0))
% 29.82/8.20  | (116)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC44(v0) = v1) |  ~ (cC42(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (117) cC62(iV8467) = all_0_10_10
% 29.82/8.20  | (118)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC60(v0) = v1) |  ? [v2] :  ? [v3] : (cC58(v0) = v3 & cC2xcomp(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.20  | (119)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px9(v3, v2) = v1) |  ~ (ra_Px9(v3, v2) = v0))
% 29.82/8.20  | (120)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC78(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (121)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC30(v2) = v1) |  ~ (cC30(v2) = v0))
% 29.82/8.20  | (122)  ! [v0] : ( ~ (cC52(v0) = 0) |  ? [v1] : ra_Px32(v0, v1) = 0)
% 29.82/8.20  | (123)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC36(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (124)  ! [v0] : ( ~ (cC40(v0) = 0) |  ? [v1] : (cC38(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (125)  ! [v0] :  ! [v1] : ( ~ (cC44(v0) = 0) |  ~ (ra_Px10(v0, v1) = 0))
% 29.82/8.20  | (126)  ! [v0] : ( ~ (cC94(v0) = 0) |  ? [v1] : ra_Px29(v0, v1) = 0)
% 29.82/8.20  | (127)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px8(v0, v2) = 0) |  ~ (cC36(v0) = v1))
% 29.82/8.20  | (128) rR1(iV8467, iV8470) = 0
% 29.82/8.20  | (129) cowlThing(iV8473) = 0
% 29.82/8.20  | (130) cowlThing(iV8467) = 0
% 29.82/8.20  | (131)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px3(v3, v2) = v1) |  ~ (ra_Px3(v3, v2) = v0))
% 29.82/8.20  | (132)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC36(v2) = v1) |  ~ (cC36(v2) = v0))
% 29.82/8.20  | (133) cC14(iV8467) = all_0_9_9
% 29.82/8.20  | (134)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC46(v0) = v1) |  ? [v2] :  ? [v3] : (cC44xcomp(v0) = v2 & cC30(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.20  | (135)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC28(v0) = v1) |  ~ (cC26(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (136)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC16(v0) = v1) |  ~ (ra_Px2(v0, v2) = 0))
% 29.82/8.20  | (137) cowlThing(iV8472) = 0
% 29.82/8.20  | (138)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px17(v0, v2) = 0) |  ~ (cC62(v0) = v1))
% 29.82/8.20  | (139)  ! [v0] :  ! [v1] : ( ~ (cC90(v0) = v1) |  ? [v2] :  ? [v3] : (cC92(v0) = v2 & cC82xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.20  | (140)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cTEST(v2) = v1) |  ~ (cTEST(v2) = v0))
% 29.82/8.20  | (141) rR1(iV8467, iV8472) = 0
% 29.82/8.20  | (142)  ! [v0] : ( ~ (cC4(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (143)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC20(v2) = v1) |  ~ (cC20(v2) = v0))
% 29.82/8.20  | (144)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC92xcomp(v2) = v1) |  ~ (cC92xcomp(v2) = v0))
% 29.82/8.20  | (145)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC94(v0) = v1) |  ~ (ra_Px29(v0, v2) = 0))
% 29.82/8.20  | (146)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px12(v0, v2) = 0) |  ~ (cC48(v0) = v1))
% 29.82/8.20  | (147)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC82(v2) = v1) |  ~ (cC82(v2) = v0))
% 29.82/8.20  | (148)  ! [v0] :  ! [v1] : ( ~ (cC24(v0) = v1) |  ? [v2] :  ? [v3] : (cC26(v0) = v2 & cC20xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.20  | (149) cowlThing(iV8470) = 0
% 29.82/8.20  | (150)  ! [v0] : ( ~ (cC86(v0) = 0) | (cC84xcomp(v0) = 0 & cC2xcomp(v0) = 0))
% 29.82/8.20  | (151)  ! [v0] :  ! [v1] : ( ~ (cC40(v0) = v1) |  ? [v2] :  ? [v3] : (cC42(v0) = v2 & cC34xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.20  | (152)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC50(v2) = v1) |  ~ (cC50(v2) = v0))
% 29.82/8.20  | (153) cC32xcomp(iV8474) = 0
% 29.82/8.20  | (154)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC48(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (155)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cTOP(v2) = 0) |  ~ (cC14(v0) = v1) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.20  | (156)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cTEST(v0) = v1) |  ? [v2] :  ? [v3] : (cC94xcomp(v0) = v3 & cC76(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.20  | (157) cowlThing(iV8468) = 0
% 29.82/8.20  | (158)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (xsd_integer(v2) = v1) |  ~ (xsd_integer(v2) = v0))
% 29.82/8.20  | (159)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cowlThing(v2) = v1) |  ~ (cowlThing(v2) = v0))
% 29.82/8.20  | (160)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px30(v0, v2) = 0) |  ~ (cC26(v0) = v1))
% 29.82/8.20  | (161)  ! [v0] :  ! [v1] : ( ~ (cC62xcomp(v0) = 0) |  ~ (ra_Px17(v0, v1) = 0))
% 29.82/8.20  | (162)  ! [v0] : ( ~ (cC6(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (163) cC58(iV8472) = all_0_4_4
% 29.82/8.20  | (164)  ! [v0] : ( ~ (cC6xcomp(v0) = 0) |  ? [v1] : ra_Px28(v0, v1) = 0)
% 29.82/8.20  | (165)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC14xcomp(v2) = v1) |  ~ (cC14xcomp(v2) = v0))
% 29.82/8.20  | (166)  ! [v0] :  ! [v1] : ( ~ (cC14(v0) = 0) |  ~ (ra_Px1(v0, v1) = 0))
% 29.82/8.20  | (167)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC90(v2) = v1) |  ~ (cC90(v2) = v0))
% 29.82/8.20  | (168)  ! [v0] : ( ~ (cC24(v0) = 0) |  ? [v1] :  ? [v2] : (cC26(v0) = v2 & cC20xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.20  | (169)  ! [v0] : ( ~ (cC26(v0) = 0) |  ? [v1] : ra_Px30(v0, v1) = 0)
% 29.82/8.20  | (170)  ! [v0] : ( ~ (cC20(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (171)  ! [v0] : ( ~ (cC82(v0) = 0) |  ? [v1] : (cC80(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.20  | (172)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC16(v2) = v1) |  ~ (cC16(v2) = v0))
% 29.82/8.21  | (173)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC26xcomp(v2) = v1) |  ~ (cC26xcomp(v2) = v0))
% 29.82/8.21  | (174) cC2xcomp(iV8472) = 0
% 29.82/8.21  | (175)  ! [v0] : ( ~ (cC32(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (176)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC88(v2) = v1) |  ~ (cC88(v2) = v0))
% 29.82/8.21  | (177)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC66(v2) = v1) |  ~ (cC66(v2) = v0))
% 29.82/8.21  | (178)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px5(v3, v2) = v1) |  ~ (ra_Px5(v3, v2) = v0))
% 29.82/8.21  | (179)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC36xcomp(v0) = v1) |  ? [v2] : ra_Px8(v0, v2) = 0)
% 29.82/8.21  | (180)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC50xcomp(v2) = v1) |  ~ (cC50xcomp(v2) = v0))
% 29.82/8.21  | (181)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC64(v2) = v1) |  ~ (cC64(v2) = v0))
% 29.82/8.21  | (182)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC66(v0) = v1) |  ? [v2] :  ? [v3] : (cC64(v0) = v3 & cC2xcomp(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.21  | (183)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC28xcomp(v2) = v1) |  ~ (cC28xcomp(v2) = v0))
% 29.82/8.21  | (184)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC62xcomp(v0) = v1) |  ? [v2] : ra_Px17(v0, v2) = 0)
% 29.82/8.21  | (185)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC82(v0) = v1) |  ~ (cC80(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (186) cowlThing(iV8471) = 0
% 29.82/8.21  | (187)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC24(v2) = v1) |  ~ (cC24(v2) = v0))
% 29.82/8.21  | (188)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC94(v0) = v1) |  ~ (cC92(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (189)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC54(v0) = v1) |  ~ (cC52(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (190)  ! [v0] :  ! [v1] : ( ~ (cC16xcomp(v0) = 0) |  ~ (ra_Px2(v0, v1) = 0))
% 29.82/8.21  | (191)  ! [v0] :  ! [v1] : ( ~ (cC2xcomp(v0) = 0) |  ~ (ra_Px3(v0, v1) = 0))
% 29.82/8.21  | (192) rR1(iV8467, iV8468) = 0
% 29.82/8.21  | (193)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px6(v3, v2) = v1) |  ~ (ra_Px6(v3, v2) = v0))
% 29.82/8.21  | (194)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC70(v2) = v1) |  ~ (cC70(v2) = v0))
% 29.82/8.21  | (195)  ! [v0] : ( ~ (cC28(v0) = 0) |  ? [v1] : (cC26(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (196)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC34(v0) = v1) |  ~ (cC32xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (197)  ! [v0] :  ! [v1] : ( ~ (cC84xcomp(v0) = 0) |  ~ (ra_Px23(v0, v1) = 0))
% 29.82/8.21  | (198)  ! [v0] :  ! [v1] : ( ~ (cC70(v0) = v1) |  ? [v2] :  ? [v3] : (cC72(v0) = v2 & cC62xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.21  | (199)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC72xcomp(v0) = v1) |  ? [v2] : ra_Px33(v0, v2) = 0)
% 29.82/8.21  | (200)  ! [v0] : ( ~ (cC44(v0) = 0) |  ? [v1] : (cC42(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (201)  ! [v0] : ( ~ (cC34(v0) = 0) |  ? [v1] : (cC32xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (202)  ! [v0] : ( ~ (cC78(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (203)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC18(v0) = v1) |  ? [v2] :  ? [v3] : (cC16xcomp(v0) = v2 & cC12(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.21  | (204)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC34(v0) = v1) |  ~ (ra_Px9(v0, v2) = 0))
% 29.82/8.21  | (205)  ! [v0] : ( ~ (cC76(v0) = 0) | (cC74xcomp(v0) = 0 & cC56(v0) = 0))
% 29.82/8.21  | (206)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC92(v2) = v1) |  ~ (cC92(v2) = v0))
% 29.82/8.21  | (207)  ! [v0] : ( ~ (cC46(v0) = 0) | (cC44xcomp(v0) = 0 & cC30(v0) = 0))
% 29.82/8.21  | (208)  ! [v0] : ( ~ (cC70(v0) = 0) |  ? [v1] :  ? [v2] : (cC72(v0) = v2 & cC62xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.21  | (209)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC4(v2) = v1) |  ~ (cC4(v2) = v0))
% 29.82/8.21  | (210)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC38(v0) = v1) |  ~ (cC36xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (211)  ! [v0] : ( ~ (cC8(v0) = 0) |  ? [v1] :  ? [v2] : (cC10(v0) = v2 & cC4(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.21  | (212)  ! [v0] : ( ~ (cC90(v0) = 0) |  ? [v1] :  ? [v2] : (cC92(v0) = v2 & cC82xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.21  | (213)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC86(v0) = v1) |  ? [v2] :  ? [v3] : (cC84xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.21  | (214)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC58(v2) = v1) |  ~ (cC58(v2) = v0))
% 29.82/8.21  | (215)  ! [v0] :  ! [v1] : ( ~ (ra_Px34(v0, v1) = 0) |  ~ (cC92(v0) = 0))
% 29.82/8.21  | (216)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC80(v2) = v1) |  ~ (cC80(v2) = v0))
% 29.82/8.21  | (217)  ! [v0] : ( ~ (cC42xcomp(v0) = 0) |  ? [v1] : ra_Px31(v0, v1) = 0)
% 29.82/8.21  | (218)  ! [v0] : ( ~ (cC24(v0) = 0) |  ? [v1] : (cC22(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (219)  ! [v0] :  ! [v1] : ( ~ (cC26xcomp(v0) = 0) |  ~ (ra_Px30(v0, v1) = 0))
% 29.82/8.21  | (220) rR1(iV8472, iV8476) = 0
% 29.82/8.21  | (221)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC22(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.21  | (222)  ! [v0] : ( ~ (cC40(v0) = 0) |  ? [v1] :  ? [v2] : (cC42(v0) = v2 & cC34xcomp(v0) = v1 & ( ~ (v1 = 0) | v2 = 0)))
% 29.82/8.21  | (223)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC18(v2) = v1) |  ~ (cC18(v2) = v0))
% 29.82/8.21  | (224)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC6(v0) = v1) |  ? [v2] : ra_Px28(v0, v2) = 0)
% 29.82/8.21  | (225)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px7(v3, v2) = v1) |  ~ (ra_Px7(v3, v2) = v0))
% 29.82/8.21  | (226)  ! [v0] : ( ~ (cC62(v0) = 0) |  ? [v1] : (cC60(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.21  | (227)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC16xcomp(v0) = v1) |  ? [v2] : ra_Px2(v0, v2) = 0)
% 29.82/8.21  | (228)  ! [v0] :  ! [v1] : ( ~ (cC42(v0) = 0) |  ~ (ra_Px31(v0, v1) = 0))
% 29.82/8.21  | (229)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px20(v0, v2) = 0) |  ~ (cC78(v0) = v1))
% 29.82/8.21  | (230)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px8(v3, v2) = v1) |  ~ (ra_Px8(v3, v2) = v0))
% 29.82/8.21  | (231)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC62(v2) = v1) |  ~ (cC62(v2) = v0))
% 29.82/8.21  | (232)  ! [v0] : ( ~ (cC36(v0) = 0) |  ? [v1] : ra_Px8(v0, v1) = 0)
% 29.82/8.21  | (233)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px28(v3, v2) = v1) |  ~ (ra_Px28(v3, v2) = v0))
% 29.82/8.21  | (234) cC2(iV8476) = 0
% 29.82/8.21  | (235)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC44(v0) = v1) |  ? [v2] : ra_Px10(v0, v2) = 0)
% 29.82/8.21  | (236)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC10(v2) = v1) |  ~ (cC10(v2) = v0))
% 29.82/8.21  | (237) cC60(iV8472) = all_0_3_3
% 29.82/8.21  | (238) cC2xcomp(iV8473) = 0
% 29.82/8.21  | (239)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC2xcomp(v2) = 0) |  ~ (cC4(v0) = v1) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (240)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC14xcomp(v0) = v1) |  ~ (ra_Px1(v0, v2) = 0))
% 29.82/8.22  | (241)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px29(v3, v2) = v1) |  ~ (ra_Px29(v3, v2) = v0))
% 29.82/8.22  | (242)  ! [v0] :  ! [v1] : ( ~ (cC8(v0) = v1) |  ? [v2] :  ? [v3] : (cC10(v0) = v2 & cC4(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.22  | (243)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (ra_Px5(v0, v2) = 0) |  ~ (cC20(v0) = v1))
% 29.82/8.22  | (244)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC14(v2) = v1) |  ~ (cC14(v2) = v0))
% 29.82/8.22  | (245)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC54xcomp(v2) = v1) |  ~ (cC54xcomp(v2) = v0))
% 29.82/8.22  | (246)  ! [v0] :  ! [v1] : ( ~ (cC36xcomp(v0) = 0) |  ~ (ra_Px8(v0, v1) = 0))
% 29.82/8.22  | (247)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC84(v2) = v1) |  ~ (cC84(v2) = v0))
% 29.82/8.22  | (248)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC64(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (249)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px20(v3, v2) = v1) |  ~ (ra_Px20(v3, v2) = v0))
% 29.82/8.22  | (250)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC36xcomp(v2) = v1) |  ~ (cC36xcomp(v2) = v0))
% 29.82/8.22  | (251)  ! [v0] : ( ~ (cC84(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (252)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px13(v3, v2) = v1) |  ~ (ra_Px13(v3, v2) = v0))
% 29.82/8.22  | (253)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC48(v2) = v1) |  ~ (cC48(v2) = v0))
% 29.82/8.22  | (254)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px1(v3, v2) = v1) |  ~ (ra_Px1(v3, v2) = v0))
% 29.82/8.22  | (255)  ! [v0] : ( ~ (cC16(v0) = 0) |  ? [v1] : (cC14xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (256)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC32xcomp(v2) = v1) |  ~ (cC32xcomp(v2) = v0))
% 29.82/8.22  | (257)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC20xcomp(v2) = v1) |  ~ (cC20xcomp(v2) = v0))
% 29.82/8.22  | (258)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC54xcomp(v0) = v1) |  ? [v2] : ra_Px14(v0, v2) = 0)
% 29.82/8.22  | (259)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC34xcomp(v2) = v1) |  ~ (cC34xcomp(v2) = v0))
% 29.82/8.22  | (260)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC80(v0) = v1) |  ? [v2] :  ? [v3] : (cC78xcomp(v0) = v2 & cC2xcomp(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.22  | (261)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC50(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (262) cC2xcomp(iV8468) = 0
% 29.82/8.22  | (263)  ! [v0] :  ! [v1] : ( ~ (cC52xcomp(v0) = 0) |  ~ (ra_Px32(v0, v1) = 0))
% 29.82/8.22  | (264)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC32xcomp(v0) = v1) |  ~ (ra_Px7(v0, v2) = 0))
% 29.82/8.22  | (265)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6xcomp(v2) = 0) |  ~ (cC8(v0) = v1) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (266)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px25(v3, v2) = v1) |  ~ (ra_Px25(v3, v2) = v0))
% 29.82/8.22  | (267)  ! [v0] : ( ~ (cC70(v0) = 0) |  ? [v1] : (cC68(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (268)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC84xcomp(v2) = v1) |  ~ (cC84xcomp(v2) = v0))
% 29.82/8.22  | (269) cC34(iV8467) = all_0_8_8
% 29.82/8.22  | (270)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC12(v0) = v1) |  ~ (cC10(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (271) cC8(iV8467) = all_0_12_12
% 29.82/8.22  | (272)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC82(v0) = v1) |  ? [v2] : ra_Px25(v0, v2) = 0)
% 29.82/8.22  | (273)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (274) rR1(iV8467, iV8474) = 0
% 29.82/8.22  | (275)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC50xcomp(v0) = v1) |  ~ (ra_Px13(v0, v2) = 0))
% 29.82/8.22  | (276)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px31(v3, v2) = v1) |  ~ (ra_Px31(v3, v2) = v0))
% 29.82/8.22  | (277)  ! [v0] :  ! [v1] : ( ~ (cC50xcomp(v0) = v1) |  ? [v2] :  ? [v3] : (cC52(v0) = v2 & cC48xcomp(v0) = v3 & ( ~ (v2 = 0) | (v3 = 0 & v1 = 0))))
% 29.82/8.22  | (278)  ! [v0] : ( ~ (cC22(v0) = 0) |  ? [v1] : (cC2xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (279)  ! [v0] : ( ~ (cC72(v0) = 0) |  ? [v1] : ra_Px33(v0, v1) = 0)
% 29.82/8.22  | (280)  ! [v0] : ( ~ (cC14xcomp(v0) = 0) |  ? [v1] : ra_Px1(v0, v1) = 0)
% 29.82/8.22  | (281) cC10(iV8467) = all_0_7_7
% 29.82/8.22  | (282)  ! [v0] : ( ~ (cC54(v0) = 0) |  ? [v1] : ra_Px14(v0, v1) = 0)
% 29.82/8.22  | (283)  ! [v0] : ( ~ (cC90(v0) = 0) |  ? [v1] : (cC88(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (284)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC58(v0) = v1) |  ~ (cC2(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (285)  ! [v0] :  ~ (cowlNothing(v0) = 0)
% 29.82/8.22  | (286) cowlThing(iV8474) = 0
% 29.82/8.22  | (287)  ! [v0] : ( ~ (cC94(v0) = 0) |  ? [v1] : (cC92(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (288)  ! [v0] : ( ~ (cC88(v0) = 0) |  ? [v1] : (cC86(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.22  | (289)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC86(v2) = v1) |  ~ (cC86(v2) = v0))
% 29.82/8.22  | (290)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px12(v3, v2) = v1) |  ~ (ra_Px12(v3, v2) = v0))
% 29.82/8.22  | (291)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC6xcomp(v0) = v1) |  ~ (ra_Px28(v0, v2) = 0))
% 29.82/8.22  | (292)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC70(v0) = v1) |  ~ (cC68(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (293)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC52(v2) = v1) |  ~ (cC52(v2) = v0))
% 29.82/8.22  | (294)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC56(v0) = v1) |  ? [v2] :  ? [v3] : (cC54xcomp(v0) = v2 & cC46(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.22  | (295) cTOP(iV8470) = 0
% 29.82/8.22  | (296)  ! [v0] : ( ~ (cC74(v0) = 0) |  ? [v1] : ra_Px18(v0, v1) = 0)
% 29.82/8.22  | (297)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC94xcomp(v2) = v1) |  ~ (cC94xcomp(v2) = v0))
% 29.82/8.22  | (298) cowlThing(iV8476) = 0
% 29.82/8.22  | (299)  ! [v0] : ( ~ (cC34(v0) = 0) |  ? [v1] : ra_Px9(v0, v1) = 0)
% 29.82/8.22  | (300)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC60(v2) = v1) |  ~ (cC60(v2) = v0))
% 29.82/8.22  | (301) cC26xcomp(iV8467) = 0
% 29.82/8.22  | (302)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC84(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.22  | (303)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC2(v0) = v1) |  ~ (ra_Px3(v0, v2) = 0))
% 29.82/8.22  | (304)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC6(v2) = v1) |  ~ (cC6(v2) = v0))
% 29.82/8.22  | (305) rR1(iV8467, iV8469) = 0
% 29.82/8.22  | (306)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC42xcomp(v2) = v1) |  ~ (cC42xcomp(v2) = v0))
% 29.82/8.22  | (307)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC92(v0) = v1) |  ? [v2] : ra_Px34(v0, v2) = 0)
% 29.82/8.22  | (308)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC20(v0) = v1) |  ~ (cC2xcomp(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.23  | (309)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC76(v0) = v1) |  ? [v2] :  ? [v3] : (cC74xcomp(v0) = v2 & cC56(v0) = v3 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.23  | (310)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC78xcomp(v2) = v1) |  ~ (cC78xcomp(v2) = v0))
% 29.82/8.23  | (311)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC20xcomp(v0) = v1) |  ? [v2] : ra_Px5(v0, v2) = 0)
% 29.82/8.23  | (312)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC52xcomp(v0) = v1) |  ? [v2] : ra_Px32(v0, v2) = 0)
% 29.82/8.23  | (313)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC62xcomp(v2) = v1) |  ~ (cC62xcomp(v2) = v0))
% 29.82/8.23  | (314)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cowlNothing(v2) = v1) |  ~ (cowlNothing(v2) = v0))
% 29.82/8.23  | (315)  ! [v0] : ( ~ (cC50xcomp(v0) = 0) |  ? [v1] : ra_Px13(v0, v1) = 0)
% 29.82/8.23  | (316)  ! [v0] : ( ~ (cC16(v0) = 0) |  ? [v1] : ra_Px2(v0, v1) = 0)
% 29.82/8.23  | (317)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC48xcomp(v0) = v1) |  ? [v2] : ra_Px12(v0, v2) = 0)
% 29.82/8.23  | (318)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px33(v3, v2) = v1) |  ~ (ra_Px33(v3, v2) = v0))
% 29.82/8.23  | (319)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px23(v3, v2) = v1) |  ~ (ra_Px23(v3, v2) = v0))
% 29.82/8.23  | (320) cC2xcomp(iV8471) = 0
% 29.82/8.23  | (321)  ! [v0] : ( ~ (cC66(v0) = 0) | (cC64(v0) = 0 & cC2xcomp(v0) = 0))
% 29.82/8.23  | (322)  ! [v0] : ( ~ (rR1(iV8471, v0) = 0) | cC2(v0) = 0)
% 29.82/8.23  | (323)  ! [v0] : ( ~ (cC12(v0) = 0) |  ? [v1] : (rR1(v0, v1) = 0 & cC10(v1) = 0))
% 29.82/8.23  | (324)  ! [v0] : ( ~ (cC58(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.23  | (325)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC22(v2) = v1) |  ~ (cC22(v2) = v0))
% 29.82/8.23  | (326)  ! [v0] : ( ~ (cC8(v0) = 0) |  ? [v1] : (cC6xcomp(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.23  | (327)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC28(v0) = v1) |  ~ (ra_Px6(v0, v2) = 0))
% 29.82/8.23  | (328)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC28xcomp(v0) = v1) |  ? [v2] : ra_Px6(v0, v2) = 0)
% 29.82/8.23  | (329) rR1(iV8467, iV8473) = 0
% 29.82/8.23  | (330)  ! [v0] :  ! [v1] :  ! [v2] :  ! [v3] : (v1 = v0 |  ~ (ra_Px17(v3, v2) = v1) |  ~ (ra_Px17(v3, v2) = v0))
% 29.82/8.23  | (331)  ! [v0] : ( ~ (cC62(v0) = 0) |  ? [v1] : ra_Px17(v0, v1) = 0)
% 29.82/8.23  | (332) cC82(iV8467) = all_0_11_11
% 29.82/8.23  | (333)  ! [v0] : ( ~ (rR1(iV8469, v0) = 0) | cC2(v0) = 0)
% 29.82/8.23  | (334) cC20(iV8467) = all_0_14_14
% 29.82/8.23  | (335) cC72xcomp(iV8467) = 0
% 29.82/8.23  | (336)  ! [v0] : ( ~ (cC28(v0) = 0) |  ? [v1] : ra_Px6(v0, v1) = 0)
% 29.82/8.23  | (337)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC44(v2) = v1) |  ~ (cC44(v2) = v0))
% 29.82/8.23  | (338)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC30(v0) = v1) |  ? [v2] :  ? [v3] : (cC28xcomp(v0) = v3 & cC18(v0) = v2 & ( ~ (v3 = 0) |  ~ (v2 = 0))))
% 29.82/8.23  | (339)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC74xcomp(v2) = v1) |  ~ (cC74xcomp(v2) = v0))
% 29.82/8.23  | (340)  ! [v0] :  ! [v1] : (v1 = 0 |  ~ (cC14(v0) = v1) |  ? [v2] : ra_Px1(v0, v2) = 0)
% 29.82/8.23  | (341)  ! [v0] : ( ~ (cC32xcomp(v0) = 0) |  ? [v1] : ra_Px7(v0, v1) = 0)
% 29.82/8.23  | (342)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = v0 |  ~ (cC26(v2) = v1) |  ~ (cC26(v2) = v0))
% 29.82/8.23  | (343)  ! [v0] :  ! [v1] : ( ~ (cC72xcomp(v0) = 0) |  ~ (ra_Px33(v0, v1) = 0))
% 29.82/8.23  | (344)  ! [v0] :  ! [v1] :  ! [v2] : (v1 = 0 |  ~ (cC62(v0) = v1) |  ~ (cC60(v2) = 0) |  ? [v3] : ( ~ (v3 = 0) & rR1(v0, v2) = v3))
% 29.82/8.23  | (345)  ! [v0] :  ! [v1] : ( ~ (cC54xcomp(v0) = 0) |  ~ (ra_Px14(v0, v1) = 0))
% 29.82/8.23  | (346)  ! [v0] :  ! [v1] : ( ~ (cC6(v0) = 0) |  ~ (ra_Px28(v0, v1) = 0))
% 29.82/8.23  | (347)  ! [v0] : ( ~ (cC64(v0) = 0) |  ? [v1] : (cC2(v1) = 0 & rR1(v0, v1) = 0))
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (185) with iV8471, all_0_11_11, iV8467 and discharging atoms cC82(iV8467) = all_0_11_11, yields:
% 29.82/8.23  | (348) all_0_11_11 = 0 |  ~ (cC80(iV8471) = 0) |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8471) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (260) with all_0_5_5, iV8471 and discharging atoms cC80(iV8471) = all_0_5_5, yields:
% 29.82/8.23  | (349) all_0_5_5 = 0 |  ? [v0] :  ? [v1] : (cC78xcomp(iV8471) = v0 & cC2xcomp(iV8471) = v1 & ( ~ (v1 = 0) |  ~ (v0 = 0)))
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (344) with iV8472, all_0_10_10, iV8467 and discharging atoms cC62(iV8467) = all_0_10_10, yields:
% 29.82/8.23  | (350) all_0_10_10 = 0 |  ~ (cC60(iV8472) = 0) |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8472) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (118) with all_0_3_3, iV8472 and discharging atoms cC60(iV8472) = all_0_3_3, yields:
% 29.82/8.23  | (351) all_0_3_3 = 0 |  ? [v0] :  ? [v1] : (cC58(iV8472) = v1 & cC2xcomp(iV8472) = v0 & ( ~ (v1 = 0) |  ~ (v0 = 0)))
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (324) with iV8472 yields:
% 29.82/8.23  | (352)  ~ (cC58(iV8472) = 0) |  ? [v0] : (cC2(v0) = 0 & rR1(iV8472, v0) = 0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (196) with iV8474, all_0_8_8, iV8467 and discharging atoms cC34(iV8467) = all_0_8_8, cC32xcomp(iV8474) = 0, yields:
% 29.82/8.23  | (353) all_0_8_8 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8474) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (308) with iV8472, all_0_14_14, iV8467 and discharging atoms cC20(iV8467) = all_0_14_14, cC2xcomp(iV8472) = 0, yields:
% 29.82/8.23  | (354) all_0_14_14 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8472) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (154) with iV8468, all_0_6_6, iV8467 and discharging atoms cC48(iV8467) = all_0_6_6, cC2xcomp(iV8468) = 0, yields:
% 29.82/8.23  | (355) all_0_6_6 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8468) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (284) with iV8476, all_0_4_4, iV8472 and discharging atoms cC58(iV8472) = all_0_4_4, cC2(iV8476) = 0, yields:
% 29.82/8.23  | (356) all_0_4_4 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8472, iV8476) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (155) with iV8470, all_0_9_9, iV8467 and discharging atoms cTOP(iV8470) = 0, cC14(iV8467) = all_0_9_9, yields:
% 29.82/8.23  | (357) all_0_9_9 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8470) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (265) with iV8469, all_0_12_12, iV8467 and discharging atoms cC6xcomp(iV8469) = 0, cC8(iV8467) = all_0_12_12, yields:
% 29.82/8.23  | (358) all_0_12_12 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8469) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (211) with iV8467 yields:
% 29.82/8.23  | (359)  ~ (cC8(iV8467) = 0) |  ? [v0] :  ? [v1] : (cC10(iV8467) = v1 & cC4(iV8467) = v0 & ( ~ (v0 = 0) | v1 = 0))
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (326) with iV8467 yields:
% 29.82/8.23  | (360)  ~ (cC8(iV8467) = 0) |  ? [v0] : (cC6xcomp(v0) = 0 & rR1(iV8467, v0) = 0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (242) with all_0_12_12, iV8467 and discharging atoms cC8(iV8467) = all_0_12_12, yields:
% 29.82/8.23  | (361)  ? [v0] :  ? [v1] : (cC10(iV8467) = v0 & cC4(iV8467) = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_0_12_12 = 0)))
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (239) with iV8471, all_0_13_13, iV8467 and discharging atoms cC2xcomp(iV8471) = 0, cC4(iV8467) = all_0_13_13, yields:
% 29.82/8.23  | (362) all_0_13_13 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8471) = v0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating formula (142) with iV8467 yields:
% 29.82/8.23  | (363)  ~ (cC4(iV8467) = 0) |  ? [v0] : (cC2xcomp(v0) = 0 & rR1(iV8467, v0) = 0)
% 29.82/8.23  |
% 29.82/8.23  | Instantiating (361) with all_8_0_15, all_8_1_16 yields:
% 29.82/8.23  | (364) cC10(iV8467) = all_8_1_16 & cC4(iV8467) = all_8_0_15 & ( ~ (all_8_1_16 = 0) | (all_8_0_15 = 0 & all_0_12_12 = 0))
% 29.82/8.24  |
% 29.82/8.24  | Applying alpha-rule on (364) yields:
% 29.82/8.24  | (365) cC10(iV8467) = all_8_1_16
% 29.82/8.24  | (366) cC4(iV8467) = all_8_0_15
% 29.82/8.24  | (367)  ~ (all_8_1_16 = 0) | (all_8_0_15 = 0 & all_0_12_12 = 0)
% 29.82/8.24  |
% 29.82/8.24  +-Applying beta-rule and splitting (362), into two cases.
% 29.82/8.24  |-Branch one:
% 29.82/8.24  | (368) all_0_13_13 = 0
% 29.82/8.24  |
% 29.82/8.24  	| From (368) and (53) follows:
% 29.82/8.24  	| (369) cC4(iV8467) = 0
% 29.82/8.24  	|
% 29.82/8.24  	+-Applying beta-rule and splitting (357), into two cases.
% 29.82/8.24  	|-Branch one:
% 29.82/8.24  	| (370) all_0_9_9 = 0
% 29.82/8.24  	|
% 29.82/8.24  		+-Applying beta-rule and splitting (353), into two cases.
% 29.82/8.24  		|-Branch one:
% 29.82/8.24  		| (371) all_0_8_8 = 0
% 29.82/8.24  		|
% 29.82/8.24  			+-Applying beta-rule and splitting (358), into two cases.
% 29.82/8.24  			|-Branch one:
% 29.82/8.24  			| (372) all_0_12_12 = 0
% 29.82/8.24  			|
% 29.82/8.24  				| From (372) and (271) follows:
% 29.82/8.24  				| (373) cC8(iV8467) = 0
% 29.82/8.24  				|
% 29.82/8.24  				+-Applying beta-rule and splitting (354), into two cases.
% 29.82/8.24  				|-Branch one:
% 29.82/8.24  				| (374) all_0_14_14 = 0
% 29.82/8.24  				|
% 29.82/8.24  					+-Applying beta-rule and splitting (349), into two cases.
% 29.82/8.24  					|-Branch one:
% 29.82/8.24  					| (375) all_0_5_5 = 0
% 29.82/8.24  					|
% 29.82/8.24  						| From (375) and (36) follows:
% 29.82/8.24  						| (376) cC80(iV8471) = 0
% 29.82/8.24  						|
% 29.82/8.24  						+-Applying beta-rule and splitting (355), into two cases.
% 29.82/8.24  						|-Branch one:
% 29.82/8.24  						| (377) all_0_6_6 = 0
% 29.82/8.24  						|
% 29.82/8.24  							+-Applying beta-rule and splitting (348), into two cases.
% 29.82/8.24  							|-Branch one:
% 29.82/8.24  							| (378)  ~ (cC80(iV8471) = 0)
% 29.82/8.24  							|
% 29.82/8.24  								| Using (376) and (378) yields:
% 29.82/8.24  								| (379) $false
% 29.82/8.24  								|
% 29.82/8.24  								|-The branch is then unsatisfiable
% 29.82/8.24  							|-Branch two:
% 29.82/8.24  							| (376) cC80(iV8471) = 0
% 29.82/8.24  							| (381) all_0_11_11 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8471) = v0)
% 29.82/8.24  							|
% 29.82/8.24  								+-Applying beta-rule and splitting (356), into two cases.
% 29.82/8.24  								|-Branch one:
% 29.82/8.24  								| (382) all_0_4_4 = 0
% 29.82/8.24  								|
% 29.82/8.24  									| From (382) and (163) follows:
% 29.82/8.24  									| (383) cC58(iV8472) = 0
% 29.82/8.24  									|
% 29.82/8.24  									+-Applying beta-rule and splitting (351), into two cases.
% 29.82/8.24  									|-Branch one:
% 29.82/8.24  									| (384) all_0_3_3 = 0
% 29.82/8.24  									|
% 29.82/8.24  										| From (384) and (237) follows:
% 29.82/8.24  										| (385) cC60(iV8472) = 0
% 29.82/8.24  										|
% 29.82/8.24  										+-Applying beta-rule and splitting (363), into two cases.
% 29.82/8.24  										|-Branch one:
% 29.82/8.24  										| (386)  ~ (cC4(iV8467) = 0)
% 29.82/8.24  										|
% 29.82/8.24  											| Using (369) and (386) yields:
% 29.82/8.24  											| (379) $false
% 29.82/8.24  											|
% 29.82/8.24  											|-The branch is then unsatisfiable
% 29.82/8.24  										|-Branch two:
% 29.82/8.24  										| (369) cC4(iV8467) = 0
% 29.82/8.24  										| (389)  ? [v0] : (cC2xcomp(v0) = 0 & rR1(iV8467, v0) = 0)
% 29.82/8.24  										|
% 29.82/8.24  											+-Applying beta-rule and splitting (350), into two cases.
% 29.82/8.24  											|-Branch one:
% 29.82/8.24  											| (390)  ~ (cC60(iV8472) = 0)
% 29.82/8.24  											|
% 29.82/8.24  												| Using (385) and (390) yields:
% 29.82/8.24  												| (379) $false
% 29.82/8.24  												|
% 29.82/8.24  												|-The branch is then unsatisfiable
% 29.82/8.24  											|-Branch two:
% 29.82/8.24  											| (385) cC60(iV8472) = 0
% 29.82/8.24  											| (393) all_0_10_10 = 0 |  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8472) = v0)
% 29.82/8.24  											|
% 29.82/8.24  												+-Applying beta-rule and splitting (360), into two cases.
% 29.82/8.24  												|-Branch one:
% 29.82/8.24  												| (394)  ~ (cC8(iV8467) = 0)
% 29.82/8.24  												|
% 29.82/8.24  													| Using (373) and (394) yields:
% 29.82/8.24  													| (379) $false
% 29.82/8.24  													|
% 29.82/8.24  													|-The branch is then unsatisfiable
% 29.82/8.24  												|-Branch two:
% 29.82/8.24  												| (373) cC8(iV8467) = 0
% 29.82/8.24  												| (397)  ? [v0] : (cC6xcomp(v0) = 0 & rR1(iV8467, v0) = 0)
% 29.82/8.24  												|
% 29.82/8.24  													+-Applying beta-rule and splitting (393), into two cases.
% 29.82/8.24  													|-Branch one:
% 29.82/8.24  													| (398) all_0_10_10 = 0
% 29.82/8.24  													|
% 29.82/8.24  														+-Applying beta-rule and splitting (381), into two cases.
% 29.82/8.24  														|-Branch one:
% 29.82/8.24  														| (399) all_0_11_11 = 0
% 29.82/8.24  														|
% 29.82/8.24  															| Instantiating formula (236) with iV8467, all_8_1_16, all_0_7_7 and discharging atoms cC10(iV8467) = all_8_1_16, cC10(iV8467) = all_0_7_7, yields:
% 29.82/8.24  															| (400) all_8_1_16 = all_0_7_7
% 29.82/8.24  															|
% 29.82/8.24  															| Instantiating formula (209) with iV8467, 0, all_8_0_15 and discharging atoms cC4(iV8467) = all_8_0_15, cC4(iV8467) = 0, yields:
% 29.82/8.24  															| (401) all_8_0_15 = 0
% 29.82/8.24  															|
% 29.82/8.24  															| From (400) and (365) follows:
% 29.82/8.24  															| (281) cC10(iV8467) = all_0_7_7
% 29.82/8.24  															|
% 29.82/8.24  															| From (401) and (366) follows:
% 29.82/8.24  															| (369) cC4(iV8467) = 0
% 29.82/8.24  															|
% 29.82/8.24  															+-Applying beta-rule and splitting (359), into two cases.
% 29.82/8.24  															|-Branch one:
% 29.82/8.24  															| (394)  ~ (cC8(iV8467) = 0)
% 29.82/8.24  															|
% 29.82/8.24  																| Using (373) and (394) yields:
% 29.82/8.24  																| (379) $false
% 29.82/8.24  																|
% 29.82/8.24  																|-The branch is then unsatisfiable
% 29.82/8.24  															|-Branch two:
% 29.82/8.24  															| (373) cC8(iV8467) = 0
% 29.82/8.24  															| (407)  ? [v0] :  ? [v1] : (cC10(iV8467) = v1 & cC4(iV8467) = v0 & ( ~ (v0 = 0) | v1 = 0))
% 29.82/8.24  															|
% 29.82/8.24  																| Instantiating (407) with all_146_0_35, all_146_1_36 yields:
% 29.82/8.24  																| (408) cC10(iV8467) = all_146_0_35 & cC4(iV8467) = all_146_1_36 & ( ~ (all_146_1_36 = 0) | all_146_0_35 = 0)
% 29.82/8.24  																|
% 29.82/8.24  																| Applying alpha-rule on (408) yields:
% 29.82/8.24  																| (409) cC10(iV8467) = all_146_0_35
% 29.82/8.24  																| (410) cC4(iV8467) = all_146_1_36
% 29.82/8.24  																| (411)  ~ (all_146_1_36 = 0) | all_146_0_35 = 0
% 29.82/8.24  																|
% 29.82/8.24  																| Instantiating formula (236) with iV8467, all_146_0_35, all_0_7_7 and discharging atoms cC10(iV8467) = all_146_0_35, cC10(iV8467) = all_0_7_7, yields:
% 29.82/8.24  																| (412) all_146_0_35 = all_0_7_7
% 29.82/8.24  																|
% 29.82/8.24  																| Instantiating formula (209) with iV8467, all_146_1_36, 0 and discharging atoms cC4(iV8467) = all_146_1_36, cC4(iV8467) = 0, yields:
% 29.82/8.24  																| (413) all_146_1_36 = 0
% 29.82/8.24  																|
% 29.82/8.24  																+-Applying beta-rule and splitting (411), into two cases.
% 29.82/8.24  																|-Branch one:
% 29.82/8.24  																| (414)  ~ (all_146_1_36 = 0)
% 29.82/8.24  																|
% 29.82/8.24  																	| Equations (413) can reduce 414 to:
% 29.82/8.24  																	| (415) $false
% 29.82/8.24  																	|
% 29.82/8.24  																	|-The branch is then unsatisfiable
% 29.82/8.24  																|-Branch two:
% 29.82/8.24  																| (413) all_146_1_36 = 0
% 29.82/8.24  																| (417) all_146_0_35 = 0
% 29.82/8.24  																|
% 29.82/8.24  																	| Combining equations (417,412) yields a new equation:
% 29.82/8.24  																	| (418) all_0_7_7 = 0
% 29.82/8.24  																	|
% 29.82/8.24  																	+-Applying beta-rule and splitting (33), into two cases.
% 29.82/8.24  																	|-Branch one:
% 29.82/8.24  																	| (419)  ~ (all_0_3_3 = 0)
% 29.82/8.24  																	|
% 29.82/8.24  																		| Equations (384) can reduce 419 to:
% 29.82/8.24  																		| (415) $false
% 29.82/8.24  																		|
% 29.82/8.24  																		|-The branch is then unsatisfiable
% 29.82/8.24  																	|-Branch two:
% 29.82/8.24  																	| (384) all_0_3_3 = 0
% 29.82/8.24  																	| (422)  ~ (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) |  ~ (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) | (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))
% 29.82/8.24  																	|
% 29.82/8.24  																		+-Applying beta-rule and splitting (422), into two cases.
% 29.82/8.24  																		|-Branch one:
% 29.82/8.24  																		| (423)  ~ (all_0_4_4 = 0)
% 29.82/8.24  																		|
% 29.82/8.24  																			| Equations (382) can reduce 423 to:
% 29.82/8.24  																			| (415) $false
% 29.82/8.24  																			|
% 29.82/8.24  																			|-The branch is then unsatisfiable
% 29.82/8.24  																		|-Branch two:
% 29.82/8.24  																		| (382) all_0_4_4 = 0
% 29.82/8.24  																		| (426)  ~ (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) |  ~ (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) | (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))
% 29.82/8.25  																		|
% 29.82/8.25  																			+-Applying beta-rule and splitting (426), into two cases.
% 29.82/8.25  																			|-Branch one:
% 29.82/8.25  																			| (427)  ~ (all_0_5_5 = 0)
% 29.82/8.25  																			|
% 29.82/8.25  																				| Equations (375) can reduce 427 to:
% 29.82/8.25  																				| (415) $false
% 29.82/8.25  																				|
% 29.82/8.25  																				|-The branch is then unsatisfiable
% 29.82/8.25  																			|-Branch two:
% 29.82/8.25  																			| (375) all_0_5_5 = 0
% 29.82/8.25  																			| (430)  ~ (all_0_6_6 = 0) |  ~ (all_0_7_7 = 0) |  ~ (all_0_8_8 = 0) |  ~ (all_0_9_9 = 0) |  ~ (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) | (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))
% 29.82/8.25  																			|
% 29.82/8.25  																				+-Applying beta-rule and splitting (430), into two cases.
% 29.82/8.25  																				|-Branch one:
% 29.82/8.25  																				| (431)  ~ (all_0_6_6 = 0)
% 29.82/8.25  																				|
% 29.82/8.25  																					| Equations (377) can reduce 431 to:
% 29.82/8.25  																					| (415) $false
% 29.82/8.25  																					|
% 29.82/8.25  																					|-The branch is then unsatisfiable
% 29.82/8.25  																				|-Branch two:
% 29.82/8.25  																				| (377) all_0_6_6 = 0
% 29.82/8.25  																				| (434)  ~ (all_0_7_7 = 0) |  ~ (all_0_8_8 = 0) |  ~ (all_0_9_9 = 0) |  ~ (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) | (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))
% 29.82/8.25  																				|
% 29.82/8.25  																					+-Applying beta-rule and splitting (434), into two cases.
% 29.82/8.25  																					|-Branch one:
% 29.82/8.25  																					| (435)  ~ (all_0_7_7 = 0)
% 29.82/8.25  																					|
% 29.82/8.25  																						| Equations (418) can reduce 435 to:
% 29.82/8.25  																						| (415) $false
% 29.82/8.25  																						|
% 29.82/8.25  																						|-The branch is then unsatisfiable
% 29.82/8.25  																					|-Branch two:
% 29.82/8.25  																					| (418) all_0_7_7 = 0
% 29.82/8.25  																					| (438)  ~ (all_0_8_8 = 0) |  ~ (all_0_9_9 = 0) |  ~ (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) | (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))
% 29.82/8.25  																					|
% 29.82/8.25  																						+-Applying beta-rule and splitting (438), into two cases.
% 29.82/8.25  																						|-Branch one:
% 29.82/8.25  																						| (439)  ~ (all_0_8_8 = 0)
% 29.82/8.25  																						|
% 29.82/8.25  																							| Equations (371) can reduce 439 to:
% 29.82/8.25  																							| (415) $false
% 29.82/8.25  																							|
% 29.82/8.25  																							|-The branch is then unsatisfiable
% 29.82/8.25  																						|-Branch two:
% 29.82/8.25  																						| (371) all_0_8_8 = 0
% 29.82/8.25  																						| (442)  ~ (all_0_9_9 = 0) |  ~ (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) | (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))
% 29.82/8.25  																						|
% 29.82/8.25  																							+-Applying beta-rule and splitting (442), into two cases.
% 29.82/8.25  																							|-Branch one:
% 29.82/8.25  																							| (443)  ~ (all_0_9_9 = 0)
% 29.82/8.25  																							|
% 29.82/8.25  																								| Equations (370) can reduce 443 to:
% 29.82/8.25  																								| (415) $false
% 29.82/8.25  																								|
% 29.82/8.25  																								|-The branch is then unsatisfiable
% 29.82/8.25  																							|-Branch two:
% 29.82/8.25  																							| (370) all_0_9_9 = 0
% 29.82/8.25  																							| (446)  ~ (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) | (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))
% 29.82/8.25  																							|
% 29.82/8.25  																								+-Applying beta-rule and splitting (446), into two cases.
% 29.82/8.25  																								|-Branch one:
% 29.82/8.25  																								| (447)  ~ (all_0_10_10 = 0)
% 29.82/8.25  																								|
% 29.82/8.25  																									| Equations (398) can reduce 447 to:
% 29.82/8.25  																									| (415) $false
% 29.82/8.25  																									|
% 29.82/8.25  																									|-The branch is then unsatisfiable
% 29.82/8.25  																								|-Branch two:
% 29.82/8.25  																								| (398) all_0_10_10 = 0
% 29.82/8.25  																								| (450)  ~ (all_0_11_11 = 0) |  ~ (all_0_12_12 = 0) |  ~ (all_0_13_13 = 0) |  ~ (all_0_14_14 = 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))
% 29.82/8.25  																								|
% 29.82/8.25  																									+-Applying beta-rule and splitting (450), into two cases.
% 29.82/8.25  																									|-Branch one:
% 29.82/8.25  																									| (451)  ~ (all_0_11_11 = 0)
% 29.82/8.25  																									|
% 29.82/8.25  																										| Equations (399) can reduce 451 to:
% 29.82/8.25  																										| (415) $false
% 29.82/8.25  																										|
% 29.82/8.25  																										|-The branch is then unsatisfiable
% 29.82/8.25  																									|-Branch two:
% 29.82/8.25  																									| (399) all_0_11_11 = 0
% 29.82/8.25  																									| (454)  ~ (all_0_12_12 = 0) |  ~ (all_0_13_13 = 0) |  ~ (all_0_14_14 = 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))
% 29.82/8.25  																									|
% 29.82/8.25  																										+-Applying beta-rule and splitting (454), into two cases.
% 29.82/8.25  																										|-Branch one:
% 29.82/8.25  																										| (455)  ~ (all_0_12_12 = 0)
% 29.82/8.25  																										|
% 29.82/8.25  																											| Equations (372) can reduce 455 to:
% 29.82/8.25  																											| (415) $false
% 29.82/8.25  																											|
% 29.82/8.25  																											|-The branch is then unsatisfiable
% 29.82/8.25  																										|-Branch two:
% 29.82/8.25  																										| (372) all_0_12_12 = 0
% 29.82/8.25  																										| (458)  ~ (all_0_13_13 = 0) |  ~ (all_0_14_14 = 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))
% 30.06/8.25  																										|
% 30.06/8.25  																											+-Applying beta-rule and splitting (458), into two cases.
% 30.06/8.25  																											|-Branch one:
% 30.06/8.25  																											| (459)  ~ (all_0_13_13 = 0)
% 30.06/8.25  																											|
% 30.06/8.25  																												| Equations (368) can reduce 459 to:
% 30.06/8.25  																												| (415) $false
% 30.06/8.25  																												|
% 30.06/8.25  																												|-The branch is then unsatisfiable
% 30.06/8.25  																											|-Branch two:
% 30.06/8.25  																											| (368) all_0_13_13 = 0
% 30.06/8.25  																											| (462)  ~ (all_0_14_14 = 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))
% 30.06/8.25  																											|
% 30.06/8.25  																												+-Applying beta-rule and splitting (462), into two cases.
% 30.06/8.25  																												|-Branch one:
% 30.06/8.25  																												| (463)  ~ (all_0_14_14 = 0)
% 30.06/8.25  																												|
% 30.06/8.25  																													| Equations (374) can reduce 463 to:
% 30.06/8.25  																													| (415) $false
% 30.06/8.25  																													|
% 30.06/8.25  																													|-The branch is then unsatisfiable
% 30.06/8.25  																												|-Branch two:
% 30.06/8.25  																												| (374) all_0_14_14 = 0
% 30.06/8.25  																												| (466) (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))
% 30.06/8.25  																												|
% 30.06/8.25  																													+-Applying beta-rule and splitting (466), into two cases.
% 30.06/8.25  																													|-Branch one:
% 30.06/8.25  																													| (467) 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)))
% 30.06/8.25  																													|
% 30.06/8.25  																														| Applying alpha-rule on (467) yields:
% 30.06/8.25  																														| (468) xsd_string(all_0_2_2) = all_0_1_1
% 30.06/8.25  																														| (469) xsd_integer(all_0_2_2) = all_0_0_0
% 30.06/8.25  																														| (470) (all_0_0_0 = 0 & all_0_1_1 = 0) | ( ~ (all_0_0_0 = 0) &  ~ (all_0_1_1 = 0))
% 30.06/8.25  																														|
% 30.06/8.25  																														| Instantiating formula (38) with all_0_2_2 yields:
% 30.06/8.25  																														| (471)  ~ (xsd_string(all_0_2_2) = 0) |  ? [v0] : ( ~ (v0 = 0) & xsd_integer(all_0_2_2) = v0)
% 30.06/8.25  																														|
% 30.06/8.25  																														| Instantiating formula (29) with all_0_1_1, all_0_2_2 and discharging atoms xsd_string(all_0_2_2) = all_0_1_1, yields:
% 30.06/8.25  																														| (472) all_0_1_1 = 0 | xsd_integer(all_0_2_2) = 0
% 30.06/8.25  																														|
% 30.06/8.25  																														+-Applying beta-rule and splitting (470), into two cases.
% 30.06/8.25  																														|-Branch one:
% 30.06/8.25  																														| (473) all_0_0_0 = 0 & all_0_1_1 = 0
% 30.06/8.25  																														|
% 30.06/8.25  																															| Applying alpha-rule on (473) yields:
% 30.06/8.25  																															| (474) all_0_0_0 = 0
% 30.06/8.25  																															| (475) all_0_1_1 = 0
% 30.06/8.25  																															|
% 30.06/8.25  																															| From (475) and (468) follows:
% 30.06/8.25  																															| (476) xsd_string(all_0_2_2) = 0
% 30.06/8.25  																															|
% 30.06/8.25  																															| From (474) and (469) follows:
% 30.06/8.25  																															| (477) xsd_integer(all_0_2_2) = 0
% 30.06/8.25  																															|
% 30.06/8.25  																															+-Applying beta-rule and splitting (471), into two cases.
% 30.06/8.25  																															|-Branch one:
% 30.06/8.25  																															| (478)  ~ (xsd_string(all_0_2_2) = 0)
% 30.06/8.25  																															|
% 30.06/8.25  																																| Using (476) and (478) yields:
% 30.06/8.25  																																| (379) $false
% 30.06/8.25  																																|
% 30.06/8.25  																																|-The branch is then unsatisfiable
% 30.06/8.25  																															|-Branch two:
% 30.06/8.25  																															| (476) xsd_string(all_0_2_2) = 0
% 30.06/8.25  																															| (481)  ? [v0] : ( ~ (v0 = 0) & xsd_integer(all_0_2_2) = v0)
% 30.06/8.25  																															|
% 30.06/8.25  																																| Instantiating (481) with all_554_0_42 yields:
% 30.06/8.25  																																| (482)  ~ (all_554_0_42 = 0) & xsd_integer(all_0_2_2) = all_554_0_42
% 30.06/8.25  																																|
% 30.06/8.25  																																| Applying alpha-rule on (482) yields:
% 30.06/8.25  																																| (483)  ~ (all_554_0_42 = 0)
% 30.06/8.25  																																| (484) xsd_integer(all_0_2_2) = all_554_0_42
% 30.06/8.25  																																|
% 30.06/8.25  																																| Instantiating formula (158) with all_0_2_2, 0, all_554_0_42 and discharging atoms xsd_integer(all_0_2_2) = all_554_0_42, xsd_integer(all_0_2_2) = 0, yields:
% 30.08/8.25  																																| (485) all_554_0_42 = 0
% 30.08/8.25  																																|
% 30.08/8.25  																																| Equations (485) can reduce 483 to:
% 30.08/8.25  																																| (415) $false
% 30.08/8.25  																																|
% 30.08/8.25  																																|-The branch is then unsatisfiable
% 30.08/8.25  																														|-Branch two:
% 30.08/8.25  																														| (487)  ~ (all_0_0_0 = 0) &  ~ (all_0_1_1 = 0)
% 30.08/8.25  																														|
% 30.08/8.25  																															| Applying alpha-rule on (487) yields:
% 30.08/8.25  																															| (488)  ~ (all_0_0_0 = 0)
% 30.08/8.25  																															| (489)  ~ (all_0_1_1 = 0)
% 30.08/8.25  																															|
% 30.08/8.25  																															+-Applying beta-rule and splitting (472), into two cases.
% 30.08/8.25  																															|-Branch one:
% 30.08/8.25  																															| (477) xsd_integer(all_0_2_2) = 0
% 30.08/8.25  																															|
% 30.08/8.25  																																| Instantiating formula (158) 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:
% 30.08/8.25  																																| (474) all_0_0_0 = 0
% 30.08/8.25  																																|
% 30.08/8.25  																																| Equations (474) can reduce 488 to:
% 30.08/8.25  																																| (415) $false
% 30.08/8.25  																																|
% 30.08/8.25  																																|-The branch is then unsatisfiable
% 30.08/8.25  																															|-Branch two:
% 30.08/8.25  																															| (493)  ~ (xsd_integer(all_0_2_2) = 0)
% 30.08/8.25  																															| (475) all_0_1_1 = 0
% 30.08/8.25  																															|
% 30.08/8.25  																																| Equations (475) can reduce 489 to:
% 30.08/8.25  																																| (415) $false
% 30.08/8.25  																																|
% 30.08/8.25  																																|-The branch is then unsatisfiable
% 30.08/8.26  																													|-Branch two:
% 30.08/8.26  																													| (496) 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)
% 30.08/8.26  																													|
% 30.08/8.26  																														| Applying alpha-rule on (496) yields:
% 30.08/8.26  																														| (497) cowlNothing(all_0_2_2) = all_0_0_0
% 30.08/8.26  																														| (498) cowlThing(all_0_2_2) = all_0_1_1
% 30.08/8.26  																														| (499)  ~ (all_0_1_1 = 0) | all_0_0_0 = 0
% 30.08/8.26  																														|
% 30.08/8.26  																														| Instantiating formula (285) with all_0_2_2 yields:
% 30.08/8.26  																														| (500)  ~ (cowlNothing(all_0_2_2) = 0)
% 30.08/8.26  																														|
% 30.08/8.26  																														| Instantiating formula (90) with all_0_1_1, all_0_2_2 and discharging atoms cowlThing(all_0_2_2) = all_0_1_1, yields:
% 30.08/8.26  																														| (475) all_0_1_1 = 0
% 30.08/8.26  																														|
% 30.08/8.26  																														+-Applying beta-rule and splitting (499), into two cases.
% 30.08/8.26  																														|-Branch one:
% 30.08/8.26  																														| (489)  ~ (all_0_1_1 = 0)
% 30.08/8.26  																														|
% 30.08/8.26  																															| Equations (475) can reduce 489 to:
% 30.08/8.26  																															| (415) $false
% 30.08/8.26  																															|
% 30.08/8.26  																															|-The branch is then unsatisfiable
% 30.08/8.26  																														|-Branch two:
% 30.08/8.26  																														| (475) all_0_1_1 = 0
% 30.08/8.26  																														| (474) all_0_0_0 = 0
% 30.08/8.26  																														|
% 30.08/8.26  																															| From (474) and (497) follows:
% 30.08/8.26  																															| (506) cowlNothing(all_0_2_2) = 0
% 30.08/8.26  																															|
% 30.08/8.26  																															| Using (506) and (500) yields:
% 30.08/8.26  																															| (379) $false
% 30.08/8.26  																															|
% 30.08/8.26  																															|-The branch is then unsatisfiable
% 30.08/8.26  														|-Branch two:
% 30.08/8.26  														| (451)  ~ (all_0_11_11 = 0)
% 30.08/8.26  														| (509)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8471) = v0)
% 30.08/8.26  														|
% 30.08/8.26  															| Instantiating (509) with all_117_0_43 yields:
% 30.08/8.26  															| (510)  ~ (all_117_0_43 = 0) & rR1(iV8467, iV8471) = all_117_0_43
% 30.08/8.26  															|
% 30.08/8.26  															| Applying alpha-rule on (510) yields:
% 30.08/8.26  															| (511)  ~ (all_117_0_43 = 0)
% 30.08/8.26  															| (512) rR1(iV8467, iV8471) = all_117_0_43
% 30.08/8.26  															|
% 30.08/8.26  															| Instantiating formula (26) with iV8467, iV8471, all_117_0_43, 0 and discharging atoms rR1(iV8467, iV8471) = all_117_0_43, rR1(iV8467, iV8471) = 0, yields:
% 30.08/8.26  															| (513) all_117_0_43 = 0
% 30.08/8.26  															|
% 30.08/8.26  															| Equations (513) can reduce 511 to:
% 30.08/8.26  															| (415) $false
% 30.08/8.26  															|
% 30.08/8.26  															|-The branch is then unsatisfiable
% 30.08/8.26  													|-Branch two:
% 30.08/8.26  													| (447)  ~ (all_0_10_10 = 0)
% 30.08/8.26  													| (516)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8472) = v0)
% 30.08/8.26  													|
% 30.08/8.26  														| Instantiating (516) with all_113_0_48 yields:
% 30.08/8.26  														| (517)  ~ (all_113_0_48 = 0) & rR1(iV8467, iV8472) = all_113_0_48
% 30.08/8.26  														|
% 30.08/8.26  														| Applying alpha-rule on (517) yields:
% 30.08/8.26  														| (518)  ~ (all_113_0_48 = 0)
% 30.08/8.26  														| (519) rR1(iV8467, iV8472) = all_113_0_48
% 30.08/8.26  														|
% 30.08/8.26  														| Instantiating formula (26) with iV8467, iV8472, all_113_0_48, 0 and discharging atoms rR1(iV8467, iV8472) = all_113_0_48, rR1(iV8467, iV8472) = 0, yields:
% 30.08/8.26  														| (520) all_113_0_48 = 0
% 30.08/8.26  														|
% 30.08/8.26  														| Equations (520) can reduce 518 to:
% 30.08/8.26  														| (415) $false
% 30.08/8.26  														|
% 30.08/8.26  														|-The branch is then unsatisfiable
% 30.08/8.26  									|-Branch two:
% 30.08/8.26  									| (419)  ~ (all_0_3_3 = 0)
% 30.08/8.26  									| (523)  ? [v0] :  ? [v1] : (cC58(iV8472) = v1 & cC2xcomp(iV8472) = v0 & ( ~ (v1 = 0) |  ~ (v0 = 0)))
% 30.08/8.26  									|
% 30.08/8.26  										| Instantiating (523) with all_90_0_51, all_90_1_52 yields:
% 30.08/8.26  										| (524) cC58(iV8472) = all_90_0_51 & cC2xcomp(iV8472) = all_90_1_52 & ( ~ (all_90_0_51 = 0) |  ~ (all_90_1_52 = 0))
% 30.08/8.26  										|
% 30.08/8.26  										| Applying alpha-rule on (524) yields:
% 30.08/8.26  										| (525) cC58(iV8472) = all_90_0_51
% 30.08/8.26  										| (526) cC2xcomp(iV8472) = all_90_1_52
% 30.08/8.26  										| (527)  ~ (all_90_0_51 = 0) |  ~ (all_90_1_52 = 0)
% 30.08/8.26  										|
% 30.08/8.26  										+-Applying beta-rule and splitting (352), into two cases.
% 30.08/8.26  										|-Branch one:
% 30.08/8.26  										| (528)  ~ (cC58(iV8472) = 0)
% 30.08/8.26  										|
% 30.08/8.26  											| Using (383) and (528) yields:
% 30.08/8.26  											| (379) $false
% 30.08/8.26  											|
% 30.08/8.26  											|-The branch is then unsatisfiable
% 30.08/8.26  										|-Branch two:
% 30.08/8.26  										| (383) cC58(iV8472) = 0
% 30.08/8.26  										| (531)  ? [v0] : (cC2(v0) = 0 & rR1(iV8472, v0) = 0)
% 30.08/8.26  										|
% 30.08/8.26  											| Instantiating formula (214) with iV8472, 0, all_90_0_51 and discharging atoms cC58(iV8472) = all_90_0_51, cC58(iV8472) = 0, yields:
% 30.08/8.26  											| (532) all_90_0_51 = 0
% 30.08/8.26  											|
% 30.08/8.26  											| Instantiating formula (54) with iV8472, all_90_1_52, 0 and discharging atoms cC2xcomp(iV8472) = all_90_1_52, cC2xcomp(iV8472) = 0, yields:
% 30.08/8.26  											| (533) all_90_1_52 = 0
% 30.08/8.26  											|
% 30.08/8.26  											+-Applying beta-rule and splitting (527), into two cases.
% 30.08/8.26  											|-Branch one:
% 30.08/8.26  											| (534)  ~ (all_90_0_51 = 0)
% 30.08/8.26  											|
% 30.08/8.26  												| Equations (532) can reduce 534 to:
% 30.08/8.26  												| (415) $false
% 30.08/8.26  												|
% 30.08/8.26  												|-The branch is then unsatisfiable
% 30.08/8.26  											|-Branch two:
% 30.08/8.26  											| (532) all_90_0_51 = 0
% 30.08/8.26  											| (537)  ~ (all_90_1_52 = 0)
% 30.08/8.26  											|
% 30.08/8.26  												| Equations (533) can reduce 537 to:
% 30.08/8.26  												| (415) $false
% 30.08/8.26  												|
% 30.08/8.26  												|-The branch is then unsatisfiable
% 30.08/8.26  								|-Branch two:
% 30.08/8.26  								| (423)  ~ (all_0_4_4 = 0)
% 30.08/8.26  								| (540)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8472, iV8476) = v0)
% 30.08/8.26  								|
% 30.08/8.26  									| Instantiating (540) with all_81_0_60 yields:
% 30.08/8.26  									| (541)  ~ (all_81_0_60 = 0) & rR1(iV8472, iV8476) = all_81_0_60
% 30.08/8.26  									|
% 30.08/8.26  									| Applying alpha-rule on (541) yields:
% 30.08/8.26  									| (542)  ~ (all_81_0_60 = 0)
% 30.08/8.26  									| (543) rR1(iV8472, iV8476) = all_81_0_60
% 30.08/8.26  									|
% 30.08/8.26  									| Instantiating formula (26) with iV8472, iV8476, all_81_0_60, 0 and discharging atoms rR1(iV8472, iV8476) = all_81_0_60, rR1(iV8472, iV8476) = 0, yields:
% 30.08/8.26  									| (544) all_81_0_60 = 0
% 30.08/8.26  									|
% 30.08/8.26  									| Equations (544) can reduce 542 to:
% 30.08/8.26  									| (415) $false
% 30.08/8.26  									|
% 30.08/8.26  									|-The branch is then unsatisfiable
% 30.08/8.26  						|-Branch two:
% 30.08/8.26  						| (431)  ~ (all_0_6_6 = 0)
% 30.08/8.26  						| (547)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8468) = v0)
% 30.08/8.26  						|
% 30.08/8.26  							| Instantiating (547) with all_63_0_66 yields:
% 30.08/8.26  							| (548)  ~ (all_63_0_66 = 0) & rR1(iV8467, iV8468) = all_63_0_66
% 30.08/8.26  							|
% 30.08/8.26  							| Applying alpha-rule on (548) yields:
% 30.08/8.26  							| (549)  ~ (all_63_0_66 = 0)
% 30.08/8.26  							| (550) rR1(iV8467, iV8468) = all_63_0_66
% 30.08/8.26  							|
% 30.08/8.26  							| Instantiating formula (26) with iV8467, iV8468, all_63_0_66, 0 and discharging atoms rR1(iV8467, iV8468) = all_63_0_66, rR1(iV8467, iV8468) = 0, yields:
% 30.08/8.26  							| (551) all_63_0_66 = 0
% 30.08/8.26  							|
% 30.08/8.26  							| Equations (551) can reduce 549 to:
% 30.08/8.26  							| (415) $false
% 30.08/8.26  							|
% 30.08/8.26  							|-The branch is then unsatisfiable
% 30.08/8.26  					|-Branch two:
% 30.08/8.26  					| (427)  ~ (all_0_5_5 = 0)
% 30.08/8.26  					| (554)  ? [v0] :  ? [v1] : (cC78xcomp(iV8471) = v0 & cC2xcomp(iV8471) = v1 & ( ~ (v1 = 0) |  ~ (v0 = 0)))
% 30.08/8.26  					|
% 30.08/8.26  						| Instantiating (554) with all_49_0_76, all_49_1_77 yields:
% 30.08/8.26  						| (555) cC78xcomp(iV8471) = all_49_1_77 & cC2xcomp(iV8471) = all_49_0_76 & ( ~ (all_49_0_76 = 0) |  ~ (all_49_1_77 = 0))
% 30.08/8.26  						|
% 30.08/8.26  						| Applying alpha-rule on (555) yields:
% 30.08/8.26  						| (556) cC78xcomp(iV8471) = all_49_1_77
% 30.08/8.26  						| (557) cC2xcomp(iV8471) = all_49_0_76
% 30.08/8.26  						| (558)  ~ (all_49_0_76 = 0) |  ~ (all_49_1_77 = 0)
% 30.08/8.26  						|
% 30.08/8.26  						| Instantiating formula (310) with iV8471, all_49_1_77, 0 and discharging atoms cC78xcomp(iV8471) = all_49_1_77, cC78xcomp(iV8471) = 0, yields:
% 30.08/8.26  						| (559) all_49_1_77 = 0
% 30.08/8.26  						|
% 30.08/8.26  						| Instantiating formula (54) with iV8471, all_49_0_76, 0 and discharging atoms cC2xcomp(iV8471) = all_49_0_76, cC2xcomp(iV8471) = 0, yields:
% 30.08/8.26  						| (560) all_49_0_76 = 0
% 30.08/8.26  						|
% 30.08/8.26  						+-Applying beta-rule and splitting (558), into two cases.
% 30.08/8.26  						|-Branch one:
% 30.08/8.26  						| (561)  ~ (all_49_0_76 = 0)
% 30.08/8.26  						|
% 30.08/8.26  							| Equations (560) can reduce 561 to:
% 30.08/8.26  							| (415) $false
% 30.08/8.26  							|
% 30.08/8.26  							|-The branch is then unsatisfiable
% 30.08/8.26  						|-Branch two:
% 30.08/8.26  						| (560) all_49_0_76 = 0
% 30.08/8.26  						| (564)  ~ (all_49_1_77 = 0)
% 30.08/8.26  						|
% 30.08/8.26  							| Equations (559) can reduce 564 to:
% 30.08/8.26  							| (415) $false
% 30.08/8.26  							|
% 30.08/8.26  							|-The branch is then unsatisfiable
% 30.08/8.26  				|-Branch two:
% 30.08/8.26  				| (463)  ~ (all_0_14_14 = 0)
% 30.08/8.26  				| (516)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8472) = v0)
% 30.08/8.26  				|
% 30.08/8.26  					| Instantiating (516) with all_45_0_91 yields:
% 30.08/8.26  					| (568)  ~ (all_45_0_91 = 0) & rR1(iV8467, iV8472) = all_45_0_91
% 30.08/8.26  					|
% 30.08/8.26  					| Applying alpha-rule on (568) yields:
% 30.08/8.27  					| (569)  ~ (all_45_0_91 = 0)
% 30.08/8.27  					| (570) rR1(iV8467, iV8472) = all_45_0_91
% 30.08/8.27  					|
% 30.08/8.27  					| Instantiating formula (26) with iV8467, iV8472, all_45_0_91, 0 and discharging atoms rR1(iV8467, iV8472) = all_45_0_91, rR1(iV8467, iV8472) = 0, yields:
% 30.08/8.27  					| (571) all_45_0_91 = 0
% 30.08/8.27  					|
% 30.08/8.27  					| Equations (571) can reduce 569 to:
% 30.08/8.27  					| (415) $false
% 30.08/8.27  					|
% 30.08/8.27  					|-The branch is then unsatisfiable
% 30.08/8.27  			|-Branch two:
% 30.08/8.27  			| (455)  ~ (all_0_12_12 = 0)
% 30.08/8.27  			| (574)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8469) = v0)
% 30.08/8.27  			|
% 30.08/8.27  				| Instantiating (574) with all_41_0_102 yields:
% 30.08/8.27  				| (575)  ~ (all_41_0_102 = 0) & rR1(iV8467, iV8469) = all_41_0_102
% 30.08/8.27  				|
% 30.08/8.27  				| Applying alpha-rule on (575) yields:
% 30.08/8.27  				| (576)  ~ (all_41_0_102 = 0)
% 30.08/8.27  				| (577) rR1(iV8467, iV8469) = all_41_0_102
% 30.08/8.27  				|
% 30.08/8.27  				| Instantiating formula (26) with iV8467, iV8469, all_41_0_102, 0 and discharging atoms rR1(iV8467, iV8469) = all_41_0_102, rR1(iV8467, iV8469) = 0, yields:
% 30.08/8.27  				| (578) all_41_0_102 = 0
% 30.08/8.27  				|
% 30.08/8.27  				| Equations (578) can reduce 576 to:
% 30.08/8.27  				| (415) $false
% 30.08/8.27  				|
% 30.08/8.27  				|-The branch is then unsatisfiable
% 30.08/8.27  		|-Branch two:
% 30.08/8.27  		| (439)  ~ (all_0_8_8 = 0)
% 30.08/8.27  		| (581)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8474) = v0)
% 30.08/8.27  		|
% 30.08/8.27  			| Instantiating (581) with all_32_0_114 yields:
% 30.08/8.27  			| (582)  ~ (all_32_0_114 = 0) & rR1(iV8467, iV8474) = all_32_0_114
% 30.08/8.27  			|
% 30.08/8.27  			| Applying alpha-rule on (582) yields:
% 30.08/8.27  			| (583)  ~ (all_32_0_114 = 0)
% 30.08/8.27  			| (584) rR1(iV8467, iV8474) = all_32_0_114
% 30.08/8.27  			|
% 30.08/8.27  			| Instantiating formula (26) with iV8467, iV8474, all_32_0_114, 0 and discharging atoms rR1(iV8467, iV8474) = all_32_0_114, rR1(iV8467, iV8474) = 0, yields:
% 30.08/8.27  			| (585) all_32_0_114 = 0
% 30.08/8.27  			|
% 30.08/8.27  			| Equations (585) can reduce 583 to:
% 30.08/8.27  			| (415) $false
% 30.08/8.27  			|
% 30.08/8.27  			|-The branch is then unsatisfiable
% 30.08/8.27  	|-Branch two:
% 30.08/8.27  	| (443)  ~ (all_0_9_9 = 0)
% 30.08/8.27  	| (588)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8470) = v0)
% 30.08/8.27  	|
% 30.08/8.27  		| Instantiating (588) with all_28_0_126 yields:
% 30.08/8.27  		| (589)  ~ (all_28_0_126 = 0) & rR1(iV8467, iV8470) = all_28_0_126
% 30.08/8.27  		|
% 30.08/8.27  		| Applying alpha-rule on (589) yields:
% 30.08/8.27  		| (590)  ~ (all_28_0_126 = 0)
% 30.08/8.27  		| (591) rR1(iV8467, iV8470) = all_28_0_126
% 30.08/8.27  		|
% 30.08/8.27  		| Instantiating formula (26) with iV8467, iV8470, all_28_0_126, 0 and discharging atoms rR1(iV8467, iV8470) = all_28_0_126, rR1(iV8467, iV8470) = 0, yields:
% 30.08/8.27  		| (592) all_28_0_126 = 0
% 30.08/8.27  		|
% 30.08/8.27  		| Equations (592) can reduce 590 to:
% 30.08/8.27  		| (415) $false
% 30.08/8.27  		|
% 30.08/8.27  		|-The branch is then unsatisfiable
% 30.08/8.27  |-Branch two:
% 30.08/8.27  | (459)  ~ (all_0_13_13 = 0)
% 30.08/8.27  | (509)  ? [v0] : ( ~ (v0 = 0) & rR1(iV8467, iV8471) = v0)
% 30.08/8.27  |
% 30.08/8.27  	| Instantiating (509) with all_24_0_140 yields:
% 30.08/8.27  	| (596)  ~ (all_24_0_140 = 0) & rR1(iV8467, iV8471) = all_24_0_140
% 30.08/8.27  	|
% 30.08/8.27  	| Applying alpha-rule on (596) yields:
% 30.08/8.27  	| (597)  ~ (all_24_0_140 = 0)
% 30.08/8.27  	| (598) rR1(iV8467, iV8471) = all_24_0_140
% 30.08/8.27  	|
% 30.08/8.27  	| Instantiating formula (26) with iV8467, iV8471, all_24_0_140, 0 and discharging atoms rR1(iV8467, iV8471) = all_24_0_140, rR1(iV8467, iV8471) = 0, yields:
% 30.08/8.27  	| (599) all_24_0_140 = 0
% 30.08/8.27  	|
% 30.08/8.27  	| Equations (599) can reduce 597 to:
% 30.08/8.27  	| (415) $false
% 30.08/8.27  	|
% 30.08/8.27  	|-The branch is then unsatisfiable
% 30.08/8.27  % SZS output end Proof for theBenchmark
% 30.08/8.27  
% 30.08/8.27  7684ms
%------------------------------------------------------------------------------