CSE_E---1.7.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : NUM444+6 : TPTP v9.2.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n017.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  : 300s
% DateTime : Tue May  5 04:57:21 PM UTC 2026

% Result   : Theorem 1.57s 1.85s
% Output   : CNFRefutation 1.57s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   12
%            Number of leaves      :    4
% Syntax   : Number of formulae    :   45 (  12 unt;   0 def)
%            Number of atoms       : 3250 ( 327 equ)
%            Maximal formula atoms : 2772 (  72 avg)
%            Number of connectives : 5435 (2230   ~;2608   |; 534   &)
%                                         (   8 <=>;  55  =>;   0  <=;   0 <~>)
%            Maximal formula depth :  393 (  15 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :   11 (   9 usr;   2 prp; 0-3 aty)
%            Number of functors    :   18 (  18 usr;   6 con; 0-3 aty)
%            Number of variables   :  117 (   0 sgn  59   !;  29   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(m__,conjecture,
    ( ! [X1,X2] :
        ( ( aInteger0(X1)
          & aInteger0(X2) )
       => ( ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
                & ! [X3] :
                    ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                     => ( aInteger0(X3)
                        & ? [X4] :
                            ( aInteger0(X4)
                            & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                        & aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                        & sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                    & ( ( aInteger0(X3)
                        & ( ? [X4] :
                              ( aInteger0(X4)
                              & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                          | aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                          | sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                     => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
             => ( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                | aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
            & ( ? [X3] :
                  ( aInteger0(X3)
                  & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(X1)) )
              | aDivisorOf0(xq,sdtpldt0(X2,smndt0(X1)))
              | sdteqdtlpzmzozddtrp0(X2,X1,xq) ) )
         => ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
            & ! [X3] :
                ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                 => ( aInteger0(X3)
                    & ? [X4] :
                        ( aInteger0(X4)
                        & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                    & aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                    & sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                & ( ( aInteger0(X3)
                    & ( ? [X4] :
                          ( aInteger0(X4)
                          & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                      | aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                      | sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                 => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
            & ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
            & aElementOf0(X2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) )
   => ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
          & ! [X1] :
              ( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
               => ( aInteger0(X1)
                  & ? [X2] :
                      ( aInteger0(X2)
                      & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                  & aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                  & sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
              & ( ( aInteger0(X1)
                  & ( ? [X2] :
                        ( aInteger0(X2)
                        & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                    | aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                    | sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
               => aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
       => ( ( aSet0(cS1395)
            & ! [X1] :
                ( aElementOf0(X1,cS1395)
              <=> aInteger0(X1) ) )
         => ( ! [X1] :
                ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
               => aElementOf0(X1,cS1395) )
            | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395) ) ) )
      & ( ! [X1] :
            ( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
             => ( aInteger0(X1)
                & ? [X2] :
                    ( aInteger0(X2)
                    & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                & aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                & sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
            & ( ( aInteger0(X1)
                & ( ? [X2] :
                      ( aInteger0(X2)
                      & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                  | aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                  | sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
             => aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
       => ( ( ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
              & ! [X1] :
                  ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
                <=> ( aInteger0(X1)
                    & ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
           => ( ! [X1] :
                  ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
                 => ? [X2] :
                      ( aInteger0(X2)
                      & X2 != sz00
                      & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
                          & ! [X3] :
                              ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                               => ( aInteger0(X3)
                                  & ? [X4] :
                                      ( aInteger0(X4)
                                      & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                  & aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                  & sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                              & ( ( aInteger0(X3)
                                  & ( ? [X4] :
                                        ( aInteger0(X4)
                                        & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                    | aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                    | sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                               => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
                       => ( ! [X3] :
                              ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                             => aElementOf0(X3,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
                          | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) ) )
              | isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
          | isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).

fof(mArSeq,axiom,
    ! [X1,X2] :
      ( ( aInteger0(X1)
        & aInteger0(X2)
        & X2 != sz00 )
     => ! [X3] :
          ( X3 = szAzrzSzezqlpdtcmdtrp0(X1,X2)
        <=> ( aSet0(X3)
            & ! [X4] :
                ( aElementOf0(X4,X3)
              <=> ( aInteger0(X4)
                  & sdteqdtlpzmzozddtrp0(X4,X1,X2) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeq) ).

fof(m__1962,hypothesis,
    ( aInteger0(xa)
    & aInteger0(xq)
    & xq != sz00 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1962) ).

fof(c_0_3,plain,
    ( epred1_0
  <=> ( ! [X1] :
          ( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
           => ( aInteger0(X1)
              & ? [X2] :
                  ( aInteger0(X2)
                  & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
              & aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
              & sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
          & ( ( aInteger0(X1)
              & ( ? [X2] :
                    ( aInteger0(X2)
                    & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                | aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                | sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
           => aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
     => ( ( ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
            & ! [X1] :
                ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
              <=> ( aInteger0(X1)
                  & ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
         => ( ! [X1] :
                ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
               => ? [X2] :
                    ( aInteger0(X2)
                    & X2 != sz00
                    & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
                        & ! [X3] :
                            ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                             => ( aInteger0(X3)
                                & ? [X4] :
                                    ( aInteger0(X4)
                                    & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                & aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                & sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                            & ( ( aInteger0(X3)
                                & ( ? [X4] :
                                      ( aInteger0(X4)
                                      & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                  | aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                  | sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                             => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
                     => ( ! [X3] :
                            ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                           => aElementOf0(X3,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
                        | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) ) )
            | isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
        | isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ),
    introduced(definition) ).

fof(c_0_4,plain,
    ( ( ! [X1] :
          ( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
           => ( aInteger0(X1)
              & ? [X2] :
                  ( aInteger0(X2)
                  & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
              & aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
              & sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
          & ( ( aInteger0(X1)
              & ( ? [X2] :
                    ( aInteger0(X2)
                    & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                | aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                | sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
           => aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
     => ( ( ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
            & ! [X1] :
                ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
              <=> ( aInteger0(X1)
                  & ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
         => ( ! [X1] :
                ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
               => ? [X2] :
                    ( aInteger0(X2)
                    & X2 != sz00
                    & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
                        & ! [X3] :
                            ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                             => ( aInteger0(X3)
                                & ? [X4] :
                                    ( aInteger0(X4)
                                    & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                & aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                & sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                            & ( ( aInteger0(X3)
                                & ( ? [X4] :
                                      ( aInteger0(X4)
                                      & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
                                  | aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
                                  | sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
                             => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
                     => ( ! [X3] :
                            ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
                           => aElementOf0(X3,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
                        | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) ) )
            | isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
        | isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
   => epred1_0 ),
    inference(split_equiv,[status(thm)],[c_0_3]) ).

fof(c_0_5,negated_conjecture,
    ~ ( ! [X1,X2] :
          ( ( aInteger0(X1)
            & aInteger0(X2) )
         => ( ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
                  & ! [X3] :
                      ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                       => ( aInteger0(X3)
                          & ? [X4] :
                              ( aInteger0(X4)
                              & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                          & aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                          & sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                      & ( ( aInteger0(X3)
                          & ( ? [X4] :
                                ( aInteger0(X4)
                                & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                            | aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                            | sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                       => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
               => ( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                  | aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
              & ( ? [X3] :
                    ( aInteger0(X3)
                    & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(X1)) )
                | aDivisorOf0(xq,sdtpldt0(X2,smndt0(X1)))
                | sdteqdtlpzmzozddtrp0(X2,X1,xq) ) )
           => ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
              & ! [X3] :
                  ( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                   => ( aInteger0(X3)
                      & ? [X4] :
                          ( aInteger0(X4)
                          & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                      & aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                      & sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                  & ( ( aInteger0(X3)
                      & ( ? [X4] :
                            ( aInteger0(X4)
                            & sdtasdt0(xq,X4) = sdtpldt0(X3,smndt0(xa)) )
                        | aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))
                        | sdteqdtlpzmzozddtrp0(X3,xa,xq) ) )
                   => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
              & ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
              & aElementOf0(X2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) )
     => ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
            & ! [X1] :
                ( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                 => ( aInteger0(X1)
                    & ? [X2] :
                        ( aInteger0(X2)
                        & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                    & aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                    & sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
                & ( ( aInteger0(X1)
                    & ( ? [X2] :
                          ( aInteger0(X2)
                          & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(xa)) )
                      | aDivisorOf0(xq,sdtpldt0(X1,smndt0(xa)))
                      | sdteqdtlpzmzozddtrp0(X1,xa,xq) ) )
                 => aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
         => ( ( aSet0(cS1395)
              & ! [X1] :
                  ( aElementOf0(X1,cS1395)
                <=> aInteger0(X1) ) )
           => ( ! [X1] :
                  ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
                 => aElementOf0(X1,cS1395) )
              | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395) ) ) )
        & epred1_0 ) ),
    inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[m__])]),c_0_3]) ).

fof(c_0_6,plain,
    ! [X239,X241,X242,X243,X245,X246,X248] :
      ( ( aInteger0(X239)
        | ~ aElementOf0(X239,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aInteger0(esk20_1(X239))
        | ~ aElementOf0(X239,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( sdtasdt0(xq,esk20_1(X239)) = sdtpldt0(X239,smndt0(xa))
        | ~ aElementOf0(X239,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aDivisorOf0(xq,sdtpldt0(X239,smndt0(xa)))
        | ~ aElementOf0(X239,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X239,xa,xq)
        | ~ aElementOf0(X239,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ aInteger0(X242)
        | sdtasdt0(xq,X242) != sdtpldt0(X241,smndt0(xa))
        | ~ aInteger0(X241)
        | aElementOf0(X241,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X241,smndt0(xa)))
        | ~ aInteger0(X241)
        | aElementOf0(X241,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X241,xa,xq)
        | ~ aInteger0(X241)
        | aElementOf0(X241,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aInteger0(X243)
        | ~ aElementOf0(X243,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( ~ aElementOf0(X243,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aElementOf0(X243,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( ~ aInteger0(X243)
        | aElementOf0(X243,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | aElementOf0(X243,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( aInteger0(X246)
        | ~ aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( aInteger0(esk22_2(X245,X246))
        | ~ aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( sdtasdt0(X245,esk22_2(X245,X246)) = sdtpldt0(X246,smndt0(esk21_0))
        | ~ aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( aDivisorOf0(X245,sdtpldt0(X246,smndt0(esk21_0)))
        | ~ aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X246,esk21_0,X245)
        | ~ aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ aInteger0(X248)
        | sdtasdt0(X245,X248) != sdtpldt0(X246,smndt0(esk21_0))
        | ~ aInteger0(X246)
        | aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ aDivisorOf0(X245,sdtpldt0(X246,smndt0(esk21_0)))
        | ~ aInteger0(X246)
        | aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X246,esk21_0,X245)
        | ~ aInteger0(X246)
        | aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( aElementOf0(esk23_1(X245),szAzrzSzezqlpdtcmdtrp0(esk21_0,X245))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ aElementOf0(esk23_1(X245),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X245),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X245)
        | X245 = sz00
        | epred1_0 )
      & ( ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 ) ),
    inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])]) ).

fof(c_0_7,negated_conjecture,
    ! [X222,X223,X224,X226,X227,X228,X229,X231,X232,X233,X235,X236,X237] :
      ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(X224)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aInteger0(esk16_3(X222,X223,X224))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdtasdt0(xq,esk16_3(X222,X223,X224)) = sdtpldt0(X224,smndt0(xa))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aDivisorOf0(xq,sdtpldt0(X224,smndt0(xa)))
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | sdteqdtlpzmzozddtrp0(X224,xa,xq)
        | ~ aElementOf0(X224,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aInteger0(X227)
        | sdtasdt0(xq,X227) != sdtpldt0(X226,smndt0(xa))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X226,smndt0(xa)))
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ sdteqdtlpzmzozddtrp0(X226,xa,xq)
        | ~ aInteger0(X226)
        | aElementOf0(X226,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | aElementOf0(X222,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X228)
        | sdtasdt0(xq,X228) != sdtpldt0(X223,smndt0(X222))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X223,smndt0(X222)))
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(X229)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aInteger0(esk17_3(X222,X223,X229))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdtasdt0(xq,esk17_3(X222,X223,X229)) = sdtpldt0(X229,smndt0(xa))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aDivisorOf0(xq,sdtpldt0(X229,smndt0(xa)))
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( sdteqdtlpzmzozddtrp0(X229,xa,xq)
        | ~ aElementOf0(X229,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aInteger0(X232)
        | sdtasdt0(xq,X232) != sdtpldt0(X231,smndt0(xa))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X231,smndt0(xa)))
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ sdteqdtlpzmzozddtrp0(X231,xa,xq)
        | ~ aInteger0(X231)
        | aElementOf0(X231,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( ~ aElementOf0(X223,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aElementOf0(X223,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X223,X222,xq)
        | ~ aElementOf0(X222,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X222)
        | ~ aInteger0(X223) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aInteger0(X233)
        | ~ aElementOf0(X233,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aInteger0(esk18_1(X233))
        | ~ aElementOf0(X233,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( sdtasdt0(xq,esk18_1(X233)) = sdtpldt0(X233,smndt0(xa))
        | ~ aElementOf0(X233,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aDivisorOf0(xq,sdtpldt0(X233,smndt0(xa)))
        | ~ aElementOf0(X233,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X233,xa,xq)
        | ~ aElementOf0(X233,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ aInteger0(X236)
        | sdtasdt0(xq,X236) != sdtpldt0(X235,smndt0(xa))
        | ~ aInteger0(X235)
        | aElementOf0(X235,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X235,smndt0(xa)))
        | ~ aInteger0(X235)
        | aElementOf0(X235,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X235,xa,xq)
        | ~ aInteger0(X235)
        | aElementOf0(X235,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aSet0(cS1395)
        | ~ epred1_0 )
      & ( ~ aElementOf0(X237,cS1395)
        | aInteger0(X237)
        | ~ epred1_0 )
      & ( ~ aInteger0(X237)
        | aElementOf0(X237,cS1395)
        | ~ epred1_0 )
      & ( aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ aElementOf0(esk19_0,cS1395)
        | ~ epred1_0 )
      & ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
        | ~ epred1_0 ) ),
    inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])])]) ).

cnf(c_0_8,plain,
    ( aInteger0(X1)
    | epred1_0
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_9,negated_conjecture,
    ( aInteger0(X1)
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_7]) ).

cnf(c_0_10,plain,
    ( aInteger0(X1)
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
    inference(csr,[status(thm)],[c_0_8,c_0_9]) ).

cnf(c_0_11,negated_conjecture,
    ( aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_7]) ).

cnf(c_0_12,negated_conjecture,
    ( ~ aElementOf0(esk19_0,cS1395)
    | ~ epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_7]) ).

cnf(c_0_13,negated_conjecture,
    ( aElementOf0(X1,cS1395)
    | ~ aInteger0(X1)
    | ~ epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_7]) ).

cnf(c_0_14,negated_conjecture,
    ( aInteger0(esk19_0)
    | ~ epred1_0 ),
    inference(spm,[status(thm)],[c_0_10,c_0_11]) ).

cnf(c_0_15,plain,
    ( aElementOf0(esk23_1(X1),szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))
    | X1 = sz00
    | epred1_0
    | ~ aInteger0(X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_16,negated_conjecture,
    ~ epred1_0,
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13]),c_0_14]) ).

fof(c_0_17,plain,
    ! [X201,X202,X203,X204,X205,X206] :
      ( ( aSet0(X203)
        | X203 != szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( aInteger0(X204)
        | ~ aElementOf0(X204,X203)
        | X203 != szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( sdteqdtlpzmzozddtrp0(X204,X201,X202)
        | ~ aElementOf0(X204,X203)
        | X203 != szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( ~ aInteger0(X205)
        | ~ sdteqdtlpzmzozddtrp0(X205,X201,X202)
        | aElementOf0(X205,X203)
        | X203 != szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( ~ aElementOf0(esk11_3(X201,X202,X206),X206)
        | ~ aInteger0(esk11_3(X201,X202,X206))
        | ~ sdteqdtlpzmzozddtrp0(esk11_3(X201,X202,X206),X201,X202)
        | ~ aSet0(X206)
        | X206 = szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( aInteger0(esk11_3(X201,X202,X206))
        | aElementOf0(esk11_3(X201,X202,X206),X206)
        | ~ aSet0(X206)
        | X206 = szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 )
      & ( sdteqdtlpzmzozddtrp0(esk11_3(X201,X202,X206),X201,X202)
        | aElementOf0(esk11_3(X201,X202,X206),X206)
        | ~ aSet0(X206)
        | X206 = szAzrzSzezqlpdtcmdtrp0(X201,X202)
        | ~ aInteger0(X201)
        | ~ aInteger0(X202)
        | X202 = sz00 ) ),
    inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mArSeq])])])])])]) ).

cnf(c_0_18,plain,
    ( aInteger0(X1)
    | epred1_0
    | ~ aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_19,plain,
    ( aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_20,plain,
    ( sdteqdtlpzmzozddtrp0(X1,esk21_0,X2)
    | X2 = sz00
    | epred1_0
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(esk21_0,X2))
    | ~ aInteger0(X2) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_21,plain,
    ( X1 = sz00
    | aElementOf0(esk23_1(X1),szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[c_0_15,c_0_16]) ).

cnf(c_0_22,hypothesis,
    aInteger0(xq),
    inference(split_conjunct,[status(thm)],[m__1962]) ).

cnf(c_0_23,hypothesis,
    xq != sz00,
    inference(split_conjunct,[status(thm)],[m__1962]) ).

cnf(c_0_24,plain,
    ( epred1_0
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_25,plain,
    ( aInteger0(X1)
    | X4 = sz00
    | ~ aElementOf0(X1,X2)
    | X2 != szAzrzSzezqlpdtcmdtrp0(X3,X4)
    | ~ aInteger0(X3)
    | ~ aInteger0(X4) ),
    inference(split_conjunct,[status(thm)],[c_0_17]) ).

cnf(c_0_26,plain,
    ( aInteger0(X1)
    | ~ aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
    inference(sr,[status(thm)],[c_0_18,c_0_16]) ).

cnf(c_0_27,plain,
    aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
    inference(sr,[status(thm)],[c_0_19,c_0_16]) ).

cnf(c_0_28,negated_conjecture,
    ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ sdteqdtlpzmzozddtrp0(X1,X2,xq)
    | ~ aInteger0(X2)
    | ~ aInteger0(X1) ),
    inference(split_conjunct,[status(thm)],[c_0_7]) ).

cnf(c_0_29,plain,
    ( X1 = sz00
    | sdteqdtlpzmzozddtrp0(X2,esk21_0,X1)
    | ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[c_0_20,c_0_16]) ).

cnf(c_0_30,hypothesis,
    aElementOf0(esk23_1(xq),szAzrzSzezqlpdtcmdtrp0(esk21_0,xq)),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_22]),c_0_23]) ).

cnf(c_0_31,plain,
    ( ~ aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
    inference(sr,[status(thm)],[c_0_24,c_0_16]) ).

cnf(c_0_32,plain,
    ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | epred1_0
    | ~ aInteger0(X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_33,plain,
    ( X1 = sz00
    | aInteger0(X2)
    | ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X3,X1))
    | ~ aInteger0(X1)
    | ~ aInteger0(X3) ),
    inference(er,[status(thm)],[c_0_25]) ).

cnf(c_0_34,plain,
    aInteger0(esk21_0),
    inference(spm,[status(thm)],[c_0_26,c_0_27]) ).

cnf(c_0_35,negated_conjecture,
    ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ sdteqdtlpzmzozddtrp0(X2,X1,xq)
    | ~ aInteger0(X1) ),
    inference(csr,[status(thm)],[c_0_28,c_0_10]) ).

cnf(c_0_36,hypothesis,
    sdteqdtlpzmzozddtrp0(esk23_1(xq),esk21_0,xq),
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_22])]),c_0_23]) ).

cnf(c_0_37,plain,
    ~ aElementOf0(esk21_0,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
    inference(spm,[status(thm)],[c_0_31,c_0_27]) ).

cnf(c_0_38,plain,
    ( X1 = sz00
    | epred1_0
    | ~ aElementOf0(esk23_1(X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | ~ aInteger0(X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]) ).

cnf(c_0_39,plain,
    ( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[c_0_32,c_0_16]) ).

cnf(c_0_40,hypothesis,
    aInteger0(esk23_1(xq)),
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_30]),c_0_22]),c_0_34])]),c_0_23]) ).

cnf(c_0_41,negated_conjecture,
    ~ aElementOf0(esk23_1(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq)),
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_34])]),c_0_37]) ).

cnf(c_0_42,plain,
    ( X1 = sz00
    | ~ aElementOf0(esk23_1(X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[c_0_38,c_0_16]) ).

cnf(c_0_43,plain,
    aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_40]),c_0_41]) ).

cnf(c_0_44,plain,
    $false,
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_22])]),c_0_23]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : NUM444+6 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.18/0.34  % Computer : n017.cluster.edu
% 0.18/0.34  % Model    : x86_64 x86_64
% 0.18/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34  % Memory   : 8042.1875MB
% 0.18/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34  % CPULimit   : 300
% 0.18/0.34  % WCLimit    : 300
% 0.18/0.34  % DateTime   : Tue May  5 00:32:57 EDT 2026
% 0.18/0.34  % CPUTime    : 
% 0.18/0.35  % start to proof: theBenchmark
% 1.57/1.85  % Version  : CSE_E---1.7
% 1.57/1.85  % Problem  : theBenchmark.p
% 1.57/1.85  % SZS status Theorem for theBenchmark.p
% 1.57/1.85  % SZS output start CNFRefutation
% See solution above
% 1.57/1.85  % Total time : 1.427s
%------------------------------------------------------------------------------