ET---2.0.THM-CRf.s

%------------------------------------------------------------------------------
% File     : ET---2.0
% Problem  : NUM444+6 : TPTP v8.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_ET %s %d

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Mon Jul 18 09:32:29 EDT 2022

% Result   : Theorem 0.21s 1.40s
% Output   : CNFRefutation 0.21s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   12
%            Number of leaves      :    3
% Syntax   : Number of formulae    :   35 (   8 unt;   0 def)
%            Number of atoms       : 3177 ( 308 equ)
%            Maximal formula atoms : 2772 (  90 avg)
%            Number of connectives : 5337 (2195   ~;2558   |; 524   &)
%                                         (   6 <=>;  54  =>;   0  <=;   0 <~>)
%            Maximal formula depth :  394 (  17 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :   11 (   9 usr;   2 prp; 0-3 aty)
%            Number of functors    :   17 (  17 usr;   6 con; 0-3 aty)
%            Number of variables   :  101 (   7 sgn  52   !;  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/solver/bin/../tmp/theBenchmark.p',m__) ).

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

fof(c_0_2,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_3,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_2]) ).

fof(c_0_4,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(assume_negation,[status(cth)],[m__]),c_0_2]) ).

fof(c_0_5,plain,
    ! [X5,X5,X7,X8,X8,X10,X11,X11,X13] :
      ( ( aInteger0(X5)
        | ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aInteger0(esk20_1(X5))
        | ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( sdtasdt0(xq,esk20_1(X5)) = sdtpldt0(X5,smndt0(xa))
        | ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa)))
        | ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X5,xa,xq)
        | ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ aInteger0(X7)
        | sdtasdt0(xq,X7) != sdtpldt0(X5,smndt0(xa))
        | ~ aInteger0(X5)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa)))
        | ~ aInteger0(X5)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X5,xa,xq)
        | ~ aInteger0(X5)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | epred1_0 )
      & ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aInteger0(X8)
        | ~ aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( ~ aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( ~ aInteger0(X8)
        | aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | epred1_0 )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( aInteger0(esk22_2(X10,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( sdtasdt0(X10,esk22_2(X10,X11)) = sdtpldt0(X11,smndt0(esk21_0))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X11,esk21_0,X10)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( ~ aInteger0(X13)
        | sdtasdt0(X10,X13) != sdtpldt0(X11,smndt0(esk21_0))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( ~ aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,esk21_0,X10)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( aElementOf0(esk23_1(X10),szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( ~ aElementOf0(esk23_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | X10 = sz00
        | epred1_0 )
      & ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | X10 = 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(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_3])])])])])])])]) ).

fof(c_0_6,negated_conjecture,
    ! [X5,X6,X7,X7,X9,X10,X11,X11,X13,X14,X14,X16,X17,X17] :
      ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(X7)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aInteger0(esk16_3(X5,X6,X7))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdtasdt0(xq,esk16_3(X5,X6,X7)) = sdtpldt0(X7,smndt0(xa))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aInteger0(X9)
        | sdtasdt0(xq,X9) != sdtpldt0(X7,smndt0(xa))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ sdteqdtlpzmzozddtrp0(X7,xa,xq)
        | ~ aInteger0(X7)
        | aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X10)
        | sdtasdt0(xq,X10) != sdtpldt0(X6,smndt0(X5))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(X11)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aInteger0(esk17_3(X5,X6,X11))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdtasdt0(xq,esk17_3(X5,X6,X11)) = sdtpldt0(X11,smndt0(xa))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aInteger0(X13)
        | sdtasdt0(xq,X13) != sdtpldt0(X11,smndt0(xa))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ sdteqdtlpzmzozddtrp0(X11,xa,xq)
        | ~ aInteger0(X11)
        | aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ sdteqdtlpzmzozddtrp0(X6,X5,xq)
        | ~ aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
        | ~ aInteger0(X5)
        | ~ aInteger0(X6) )
      & ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aInteger0(X14)
        | ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aInteger0(esk18_1(X14))
        | ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( sdtasdt0(xq,esk18_1(X14)) = sdtpldt0(X14,smndt0(xa))
        | ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa)))
        | ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( sdteqdtlpzmzozddtrp0(X14,xa,xq)
        | ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ aInteger0(X16)
        | sdtasdt0(xq,X16) != sdtpldt0(X14,smndt0(xa))
        | ~ aInteger0(X14)
        | aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa)))
        | ~ aInteger0(X14)
        | aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( ~ sdteqdtlpzmzozddtrp0(X14,xa,xq)
        | ~ aInteger0(X14)
        | aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq))
        | ~ epred1_0 )
      & ( aSet0(cS1395)
        | ~ epred1_0 )
      & ( ~ aElementOf0(X17,cS1395)
        | aInteger0(X17)
        | ~ epred1_0 )
      & ( ~ aInteger0(X17)
        | aElementOf0(X17,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(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_4])])])])])])])]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(c_0_18,plain,
    aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
    inference(sr,[status(thm)],[c_0_14,c_0_15]) ).

cnf(c_0_19,negated_conjecture,
    ( ~ aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
    | ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ sdteqdtlpzmzozddtrp0(X2,X1,xq)
    | ~ aInteger0(X1) ),
    inference(csr,[status(thm)],[c_0_16,c_0_11]) ).

cnf(c_0_20,plain,
    aInteger0(esk21_0),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_15]) ).

cnf(c_0_21,negated_conjecture,
    ( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ sdteqdtlpzmzozddtrp0(X1,esk21_0,xq) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19,c_0_18]),c_0_20])]) ).

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

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

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

cnf(c_0_25,plain,
    ( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(esk21_0,xq)) ),
    inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_22]),c_0_23])]),c_0_24]),c_0_15]) ).

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

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

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

cnf(c_0_29,plain,
    ~ aElementOf0(esk23_1(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq)),
    inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_23])]),c_0_24]),c_0_15]) ).

cnf(c_0_30,plain,
    ( X1 = sz00
    | aElementOf0(esk23_1(X1),szAzrzSzezqlpdtcmdtrp0(xa,xq))
    | ~ aInteger0(esk23_1(X1))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_15]) ).

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

cnf(c_0_32,plain,
    ~ aInteger0(esk23_1(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_23])]),c_0_24]) ).

cnf(c_0_33,plain,
    ( X1 = sz00
    | aInteger0(esk23_1(X1))
    | ~ aInteger0(X1) ),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_26]),c_0_15]) ).

cnf(c_0_34,plain,
    $false,
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_23])]),c_0_24]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11  % Problem  : NUM444+6 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12  % Command  : run_ET %s %d
% 0.12/0.33  % Computer : n026.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Thu Jul  7 13:53:54 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.21/1.40  # Running protocol protocol_eprover_63dc1b1eb7d762c2f3686774d32795976f981b97 for 23 seconds:
% 0.21/1.40  # Preprocessing time       : 0.053 s
% 0.21/1.40  
% 0.21/1.40  # Proof found!
% 0.21/1.40  # SZS status Theorem
% 0.21/1.40  # SZS output start CNFRefutation
% See solution above
% 0.21/1.40  # Proof object total steps             : 35
% 0.21/1.40  # Proof object clause steps            : 28
% 0.21/1.40  # Proof object formula steps           : 7
% 0.21/1.40  # Proof object conjectures             : 12
% 0.21/1.40  # Proof object clause conjectures      : 9
% 0.21/1.40  # Proof object formula conjectures     : 3
% 0.21/1.40  # Proof object initial clauses used    : 15
% 0.21/1.40  # Proof object initial formulas used   : 2
% 0.21/1.40  # Proof object generating inferences   : 10
% 0.21/1.40  # Proof object simplifying inferences  : 23
% 0.21/1.40  # Training examples: 0 positive, 0 negative
% 0.21/1.40  # Parsed axioms                        : 42
% 0.21/1.40  # Removed by relevancy pruning/SinE    : 0
% 0.21/1.40  # Initial clauses                      : 518
% 0.21/1.40  # Removed in clause preprocessing      : 5
% 0.21/1.40  # Initial clauses in saturation        : 513
% 0.21/1.40  # Processed clauses                    : 664
% 0.21/1.40  # ...of these trivial                  : 9
% 0.21/1.40  # ...subsumed                          : 356
% 0.21/1.40  # ...remaining for further processing  : 299
% 0.21/1.40  # Other redundant clauses eliminated   : 3
% 0.21/1.40  # Clauses deleted for lack of memory   : 0
% 0.21/1.40  # Backward-subsumed                    : 14
% 0.21/1.40  # Backward-rewritten                   : 6
% 0.21/1.40  # Generated clauses                    : 1425
% 0.21/1.40  # ...of the previous two non-trivial   : 1304
% 0.21/1.40  # Contextual simplify-reflections      : 1526
% 0.21/1.40  # Paramodulations                      : 1403
% 0.21/1.40  # Factorizations                       : 0
% 0.21/1.40  # Equation resolutions                 : 20
% 0.21/1.40  # Current number of processed clauses  : 277
% 0.21/1.40  #    Positive orientable unit clauses  : 12
% 0.21/1.40  #    Positive unorientable unit clauses: 0
% 0.21/1.40  #    Negative unit clauses             : 5
% 0.21/1.40  #    Non-unit-clauses                  : 260
% 0.21/1.40  # Current number of unprocessed clauses: 1060
% 0.21/1.40  # ...number of literals in the above   : 7819
% 0.21/1.40  # Current number of archived formulas  : 0
% 0.21/1.40  # Current number of archived clauses   : 22
% 0.21/1.40  # Clause-clause subsumption calls (NU) : 58576
% 0.21/1.40  # Rec. Clause-clause subsumption calls : 7461
% 0.21/1.40  # Non-unit clause-clause subsumptions  : 1882
% 0.21/1.40  # Unit Clause-clause subsumption calls : 427
% 0.21/1.40  # Rewrite failures with RHS unbound    : 0
% 0.21/1.40  # BW rewrite match attempts            : 2
% 0.21/1.40  # BW rewrite match successes           : 2
% 0.21/1.40  # Condensation attempts                : 0
% 0.21/1.40  # Condensation successes               : 0
% 0.21/1.40  # Termbank termtop insertions          : 71111
% 0.21/1.40  
% 0.21/1.40  # -------------------------------------------------
% 0.21/1.40  # User time                : 0.131 s
% 0.21/1.40  # System time              : 0.003 s
% 0.21/1.40  # Total time               : 0.134 s
% 0.21/1.40  # Maximum resident set size: 5752 pages
% 0.21/23.39  eprover: CPU time limit exceeded, terminating
% 0.21/23.40  eprover: CPU time limit exceeded, terminating
% 0.21/23.40  eprover: CPU time limit exceeded, terminating
% 0.21/23.40  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.40  eprover: No such file or directory
% 0.21/23.41  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.41  eprover: No such file or directory
% 0.21/23.41  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.41  eprover: No such file or directory
% 0.21/23.41  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.41  eprover: No such file or directory
% 0.21/23.42  eprover: eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.42  Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.42  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.42  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.43  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.43  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.44  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.44  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.45  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.45  eprover: No such file or directory
% 0.21/23.46  eprover: eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 0.21/23.46  Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.46  eprover: No such file or directory
% 0.21/23.46  eprover: No such file or directory
% 0.21/23.46  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.46  eprover: No such file or directory
% 0.21/23.47  eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.21/23.47  eprover: No such file or directory
%------------------------------------------------------------------------------