%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM444+6 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 19:08:00 EST 2010
% Result : Theorem 10.48s
% Output : Solution 10.48s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP6548/NUM444+6.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6548/NUM444+6.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6548/NUM444+6.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 6644
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% # Preprocessing time : 0.053 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 5.91 CPU 6.03 WC
% PrfWatch: 7.90 CPU 8.04 WC
% # SZS output start CNFRefutation.
% fof(22, axiom,![X1]:![X2]:(((aInteger0(X1)&aInteger0(X2))&~(X2=sz00))=>![X3]:(X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aInteger0(X4)&sdteqdtlpzmzozddtrp0(X4,X1,X2)))))),file('/tmp/SRASS.s.p', mArSeq)).
% fof(25, axiom,((aInteger0(xa)&aInteger0(xq))&~(xq=sz00)),file('/tmp/SRASS.s.p', m__1962)).
% fof(42, 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('/tmp/SRASS.s.p', m__)).
% fof(43, 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))))&(![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))))))),inference(assume_negation,[status(cth)],[42])).
% fof(50, 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))))&(![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))))))),inference(fof_simplification,[status(thm)],[43,theory(equality)])).
% fof(51, 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),introduced(definition)).
% fof(52, 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(esa)],[50,51,theory(equality)])).
% fof(148, plain,![X1]:![X2]:(((~(aInteger0(X1))|~(aInteger0(X2)))|X2=sz00)|![X3]:((~(X3=szAzrzSzezqlpdtcmdtrp0(X1,X2))|(aSet0(X3)&![X4]:((~(aElementOf0(X4,X3))|(aInteger0(X4)&sdteqdtlpzmzozddtrp0(X4,X1,X2)))&((~(aInteger0(X4))|~(sdteqdtlpzmzozddtrp0(X4,X1,X2)))|aElementOf0(X4,X3)))))&((~(aSet0(X3))|?[X4]:((~(aElementOf0(X4,X3))|(~(aInteger0(X4))|~(sdteqdtlpzmzozddtrp0(X4,X1,X2))))&(aElementOf0(X4,X3)|(aInteger0(X4)&sdteqdtlpzmzozddtrp0(X4,X1,X2)))))|X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)))),inference(fof_nnf,[status(thm)],[22])).
% fof(149, plain,![X5]:![X6]:(((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)|![X7]:((~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aInteger0(X8)&sdteqdtlpzmzozddtrp0(X8,X5,X6)))&((~(aInteger0(X8))|~(sdteqdtlpzmzozddtrp0(X8,X5,X6)))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|?[X9]:((~(aElementOf0(X9,X7))|(~(aInteger0(X9))|~(sdteqdtlpzmzozddtrp0(X9,X5,X6))))&(aElementOf0(X9,X7)|(aInteger0(X9)&sdteqdtlpzmzozddtrp0(X9,X5,X6)))))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))),inference(variable_rename,[status(thm)],[148])).
% fof(150, plain,![X5]:![X6]:(((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)|![X7]:((~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aInteger0(X8)&sdteqdtlpzmzozddtrp0(X8,X5,X6)))&((~(aInteger0(X8))|~(sdteqdtlpzmzozddtrp0(X8,X5,X6)))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|((~(aElementOf0(esk4_3(X5,X6,X7),X7))|(~(aInteger0(esk4_3(X5,X6,X7)))|~(sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6))))&(aElementOf0(esk4_3(X5,X6,X7),X7)|(aInteger0(esk4_3(X5,X6,X7))&sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6)))))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))),inference(skolemize,[status(esa)],[149])).
% fof(151, plain,![X5]:![X6]:![X7]:![X8]:((((((~(aElementOf0(X8,X7))|(aInteger0(X8)&sdteqdtlpzmzozddtrp0(X8,X5,X6)))&((~(aInteger0(X8))|~(sdteqdtlpzmzozddtrp0(X8,X5,X6)))|aElementOf0(X8,X7)))&aSet0(X7))|~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))&((~(aSet0(X7))|((~(aElementOf0(esk4_3(X5,X6,X7),X7))|(~(aInteger0(esk4_3(X5,X6,X7)))|~(sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6))))&(aElementOf0(esk4_3(X5,X6,X7),X7)|(aInteger0(esk4_3(X5,X6,X7))&sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6)))))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)),inference(shift_quantors,[status(thm)],[150])).
% fof(152, plain,![X5]:![X6]:![X7]:![X8]:(((((((aInteger0(X8)|~(aElementOf0(X8,X7)))|~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00))&(((sdteqdtlpzmzozddtrp0(X8,X5,X6)|~(aElementOf0(X8,X7)))|~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)))&((((~(aInteger0(X8))|~(sdteqdtlpzmzozddtrp0(X8,X5,X6)))|aElementOf0(X8,X7))|~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)))&((aSet0(X7)|~(X7=szAzrzSzezqlpdtcmdtrp0(X5,X6)))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00)))&(((((~(aElementOf0(esk4_3(X5,X6,X7),X7))|(~(aInteger0(esk4_3(X5,X6,X7)))|~(sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6))))|~(aSet0(X7)))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00))&(((((aInteger0(esk4_3(X5,X6,X7))|aElementOf0(esk4_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00))&((((sdteqdtlpzmzozddtrp0(esk4_3(X5,X6,X7),X5,X6)|aElementOf0(esk4_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=szAzrzSzezqlpdtcmdtrp0(X5,X6))|((~(aInteger0(X5))|~(aInteger0(X6)))|X6=sz00))))),inference(distribute,[status(thm)],[151])).
% cnf(159,plain,(X1=sz00|aInteger0(X4)|~aInteger0(X1)|~aInteger0(X2)|X3!=szAzrzSzezqlpdtcmdtrp0(X2,X1)|~aElementOf0(X4,X3)),inference(split_conjunct,[status(thm)],[152])).
% cnf(175,plain,(xq!=sz00),inference(split_conjunct,[status(thm)],[25])).
% cnf(176,plain,(aInteger0(xq)),inference(split_conjunct,[status(thm)],[25])).
% cnf(177,plain,(aInteger0(xa)),inference(split_conjunct,[status(thm)],[25])).
% fof(279, 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))&(~(aInteger0(X1))|aElementOf0(X1,cS1395))))&(?[X1]:(aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X1,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))))|~(epred1_0))),inference(fof_nnf,[status(thm)],[52])).
% fof(280, negated_conjecture,(![X5]:![X6]:((~(aInteger0(X5))|~(aInteger0(X6)))|((((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X7]:((~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X7)&?[X8]:(aInteger0(X8)&sdtasdt0(xq,X8)=sdtpldt0(X7,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X7,xa,xq)))&((~(aInteger0(X7))|((![X9]:(~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X7,xa,xq))))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))|((![X10]:(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5))))&~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))&~(sdteqdtlpzmzozddtrp0(X6,X5,xq))))|(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X11]:((~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X11)&?[X12]:(aInteger0(X12)&sdtasdt0(xq,X12)=sdtpldt0(X11,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X11,xa,xq)))&((~(aInteger0(X11))|((![X13]:(~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X11,xa,xq))))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X14]:((~(aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X14)&?[X15]:(aInteger0(X15)&sdtasdt0(xq,X15)=sdtpldt0(X14,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X14,xa,xq)))&((~(aInteger0(X14))|((![X16]:(~(aInteger0(X16))|~(sdtasdt0(xq,X16)=sdtpldt0(X14,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X14,xa,xq))))|aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&((aSet0(cS1395)&![X17]:((~(aElementOf0(X17,cS1395))|aInteger0(X17))&(~(aInteger0(X17))|aElementOf0(X17,cS1395))))&(?[X18]:(aElementOf0(X18,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X18,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))))|~(epred1_0))),inference(variable_rename,[status(thm)],[279])).
% fof(281, negated_conjecture,(![X5]:![X6]:((~(aInteger0(X5))|~(aInteger0(X6)))|((((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X7]:((~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X7)&(aInteger0(esk16_3(X5,X6,X7))&sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X7,xa,xq)))&((~(aInteger0(X7))|((![X9]:(~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X7,xa,xq))))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))|((![X10]:(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5))))&~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))&~(sdteqdtlpzmzozddtrp0(X6,X5,xq))))|(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X11]:((~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X11)&(aInteger0(esk17_3(X5,X6,X11))&sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X11,xa,xq)))&((~(aInteger0(X11))|((![X13]:(~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X11,xa,xq))))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X14]:((~(aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X14)&(aInteger0(esk18_1(X14))&sdtasdt0(xq,esk18_1(X14))=sdtpldt0(X14,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X14,xa,xq)))&((~(aInteger0(X14))|((![X16]:(~(aInteger0(X16))|~(sdtasdt0(xq,X16)=sdtpldt0(X14,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X14,xa,xq))))|aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&((aSet0(cS1395)&![X17]:((~(aElementOf0(X17,cS1395))|aInteger0(X17))&(~(aInteger0(X17))|aElementOf0(X17,cS1395))))&((aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(esk19_0,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))))|~(epred1_0))),inference(skolemize,[status(esa)],[280])).
% fof(282, negated_conjecture,![X5]:![X6]:![X7]:![X9]:![X10]:![X11]:![X13]:![X14]:![X16]:![X17]:(((((((~(aElementOf0(X17,cS1395))|aInteger0(X17))&(~(aInteger0(X17))|aElementOf0(X17,cS1395)))&aSet0(cS1395))&((aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(esk19_0,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395))))&(((((((~(aInteger0(X16))|~(sdtasdt0(xq,X16)=sdtpldt0(X14,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X14,xa,xq)))|~(aInteger0(X14)))|aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(~(aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X14)&(aInteger0(esk18_1(X14))&sdtasdt0(xq,esk18_1(X14))=sdtpldt0(X14,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X14,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X14,xa,xq))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0))&(((((((((((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X11,xa,xq)))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X11)&(aInteger0(esk17_3(X5,X6,X11))&sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X11,xa,xq))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|((((~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5))))&~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))&~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X7,xa,xq)))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X7)&(aInteger0(esk16_3(X5,X6,X7))&sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X7,xa,xq))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))|(~(aInteger0(X5))|~(aInteger0(X6))))),inference(shift_quantors,[status(thm)],[281])).
% fof(283, negated_conjecture,![X5]:![X6]:![X7]:![X9]:![X10]:![X11]:![X13]:![X14]:![X16]:![X17]:(((((((~(aElementOf0(X17,cS1395))|aInteger0(X17))|~(epred1_0))&((~(aInteger0(X17))|aElementOf0(X17,cS1395))|~(epred1_0)))&(aSet0(cS1395)|~(epred1_0)))&(((aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(epred1_0))&(~(aElementOf0(esk19_0,cS1395))|~(epred1_0)))&(~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395))|~(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)))&(((((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))))&(aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(epred1_0))))&(((((((((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(((~(aInteger0(X13))|~(sdtasdt0(xq,X13)=sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|((~(sdteqdtlpzmzozddtrp0(X11,xa,xq))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))))&((((((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&((((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aInteger0(esk17_3(X5,X6,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdtasdt0(xq,esk17_3(X5,X6,X11))=sdtpldt0(X11,smndt0(xa))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(aDivisorOf0(xq,sdtpldt0(X11,smndt0(xa)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|(sdteqdtlpzmzozddtrp0(X11,xa,xq)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,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)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X5))|~(aInteger0(X6))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|~(aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))))&(((((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|~(sdtasdt0(xq,X10)=sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(aDivisorOf0(xq,sdtpldt0(X6,smndt0(X5)))))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))))&(((((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&(((((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((((aInteger0(esk16_3(X5,X6,X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&((((sdtasdt0(xq,esk16_3(X5,X6,X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&((((aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6)))))&((((aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))&(((~(aElementOf0(X5,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(sdteqdtlpzmzozddtrp0(X6,X5,xq)))|aElementOf0(X6,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X5))|~(aInteger0(X6))))))))),inference(distribute,[status(thm)],[282])).
% cnf(284,negated_conjecture,(aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(X1)|~aInteger0(X2)|~sdteqdtlpzmzozddtrp0(X1,X2,xq)|~aElementOf0(X2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[283])).
% cnf(657,negated_conjecture,(~epred1_0|~aElementOf0(esk19_0,cS1395)),inference(split_conjunct,[status(thm)],[283])).
% cnf(658,negated_conjecture,(aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~epred1_0),inference(split_conjunct,[status(thm)],[283])).
% cnf(660,negated_conjecture,(aElementOf0(X1,cS1395)|~epred1_0|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[283])).
% fof(662, 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)))))&((~(aInteger0(X1))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(X1,stldt0(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(fof_nnf,[status(thm)],[51])).
% fof(663, plain,((![X5]:((~(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X5)&?[X6]:(aInteger0(X6)&sdtasdt0(xq,X6)=sdtpldt0(X5,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X5,xa,xq)))&((~(aInteger0(X5))|((![X7]:(~(aInteger0(X7))|~(sdtasdt0(xq,X7)=sdtpldt0(X5,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X5,xa,xq))))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(((aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&![X8]:((~(aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(aInteger0(X8)&~(aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&((~(aInteger0(X8))|aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&(?[X9]:(aElementOf0(X9,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&![X10]:((~(aInteger0(X10))|X10=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(X9,X10))&![X11]:((~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,X10)))|(((aInteger0(X11)&?[X12]:(aInteger0(X12)&sdtasdt0(X10,X12)=sdtpldt0(X11,smndt0(X9))))&aDivisorOf0(X10,sdtpldt0(X11,smndt0(X9))))&sdteqdtlpzmzozddtrp0(X11,X9,X10)))&((~(aInteger0(X11))|((![X13]:(~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(X9))))&~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(X9)))))&~(sdteqdtlpzmzozddtrp0(X11,X9,X10))))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,X10)))))&(?[X14]:(aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X9,X10))&~(aElementOf0(X14,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X9,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))&~(isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&~(isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|epred1_0),inference(variable_rename,[status(thm)],[662])).
% fof(664, plain,((![X5]:((~(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X5)&(aInteger0(esk20_1(X5))&sdtasdt0(xq,esk20_1(X5))=sdtpldt0(X5,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X5,xa,xq)))&((~(aInteger0(X5))|((![X7]:(~(aInteger0(X7))|~(sdtasdt0(xq,X7)=sdtpldt0(X5,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X5,xa,xq))))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(((aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&![X8]:((~(aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(aInteger0(X8)&~(aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&((~(aInteger0(X8))|aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&((aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&![X10]:((~(aInteger0(X10))|X10=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))&![X11]:((~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10)))|(((aInteger0(X11)&(aInteger0(esk22_2(X10,X11))&sdtasdt0(X10,esk22_2(X10,X11))=sdtpldt0(X11,smndt0(esk21_0))))&aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0))))&sdteqdtlpzmzozddtrp0(X11,esk21_0,X10)))&((~(aInteger0(X11))|((![X13]:(~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(esk21_0))))&~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0)))))&~(sdteqdtlpzmzozddtrp0(X11,esk21_0,X10))))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10)))))&((aElementOf0(esk23_1(X10),szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))&~(aElementOf0(esk23_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))&~(isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&~(isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|epred1_0),inference(skolemize,[status(esa)],[663])).
% fof(665, plain,![X5]:![X7]:![X8]:![X10]:![X11]:![X13]:(((((((((((((((~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(esk21_0))))&~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0)))))&~(sdteqdtlpzmzozddtrp0(X11,esk21_0,X10)))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10)))&(~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk21_0,X10)))|(((aInteger0(X11)&(aInteger0(esk22_2(X10,X11))&sdtasdt0(X10,esk22_2(X10,X11))=sdtpldt0(X11,smndt0(esk21_0))))&aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk21_0))))&sdteqdtlpzmzozddtrp0(X11,esk21_0,X10))))&aSet0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10)))&((aElementOf0(esk23_1(X10),szAzrzSzezqlpdtcmdtrp0(esk21_0,X10))&~(aElementOf0(esk23_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk21_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))|(~(aInteger0(X10))|X10=sz00))&aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&~(isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&(((~(aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(aInteger0(X8)&~(aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&((~(aInteger0(X8))|aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(X8,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((((((~(aInteger0(X7))|~(sdtasdt0(xq,X7)=sdtpldt0(X5,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X5,xa,xq)))|~(aInteger0(X5)))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(~(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X5)&(aInteger0(esk20_1(X5))&sdtasdt0(xq,esk20_1(X5))=sdtpldt0(X5,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X5,xa,xq)))))|epred1_0),inference(shift_quantors,[status(thm)],[664])).
% fof(666, plain,![X5]:![X7]:![X8]:![X10]:![X11]:![X13]:(((((((((((((((~(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))&((((((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)))&((aSet0(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)))&(aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|epred1_0))&(~(isOpen0(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))&(aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|epred1_0)))&(~(isClosed0(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))&(((((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)))),inference(distribute,[status(thm)],[665])).
% cnf(679,plain,(epred1_0|aInteger0(X1)|~aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[666])).
% cnf(681,plain,(epred1_0|aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[666])).
% cnf(683,plain,(epred1_0|X1=sz00|~aInteger0(X1)|~aElementOf0(esk23_1(X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[666])).
% cnf(684,plain,(epred1_0|X1=sz00|aElementOf0(esk23_1(X1),szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[666])).
% cnf(686,plain,(epred1_0|X1=sz00|sdteqdtlpzmzozddtrp0(X2,esk21_0,X1)|~aInteger0(X1)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))),inference(split_conjunct,[status(thm)],[666])).
% cnf(690,plain,(epred1_0|X1=sz00|aInteger0(X2)|~aInteger0(X1)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(esk21_0,X1))),inference(split_conjunct,[status(thm)],[666])).
% cnf(716,plain,(epred1_0|aInteger0(esk21_0)),inference(spm,[status(thm)],[679,681,theory(equality)])).
% cnf(861,plain,(sz00=X1|epred1_0|aInteger0(esk23_1(X1))|~aInteger0(X1)),inference(spm,[status(thm)],[690,684,theory(equality)])).
% cnf(886,plain,(sz00=X1|aInteger0(X2)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X3,X1))|~aInteger0(X3)|~aInteger0(X1)),inference(er,[status(thm)],[159,theory(equality)])).
% cnf(997,plain,(sz00=X1|epred1_0|sdteqdtlpzmzozddtrp0(esk23_1(X1),esk21_0,X1)|~aInteger0(X1)),inference(spm,[status(thm)],[686,684,theory(equality)])).
% cnf(6995,negated_conjecture,(aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq|epred1_0|~aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk21_0)|~aInteger0(esk23_1(xq))|~aInteger0(xq)),inference(spm,[status(thm)],[284,997,theory(equality)])).
% cnf(7019,negated_conjecture,(aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq|epred1_0|~aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk21_0)|~aInteger0(esk23_1(xq))|$false),inference(rw,[status(thm)],[6995,176,theory(equality)])).
% cnf(7020,negated_conjecture,(aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq|epred1_0|~aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk21_0)|~aInteger0(esk23_1(xq))),inference(cn,[status(thm)],[7019,theory(equality)])).
% cnf(7021,negated_conjecture,(aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|epred1_0|~aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk21_0)|~aInteger0(esk23_1(xq))),inference(sr,[status(thm)],[7020,175,theory(equality)])).
% cnf(273529,negated_conjecture,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aElementOf0(esk21_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk23_1(xq))),inference(csr,[status(thm)],[7021,716])).
% cnf(273530,negated_conjecture,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aInteger0(esk23_1(xq))),inference(csr,[status(thm)],[273529,681])).
% cnf(273531,plain,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq|~aInteger0(xq)),inference(spm,[status(thm)],[273530,861,theory(equality)])).
% cnf(273532,plain,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq|$false),inference(rw,[status(thm)],[273531,176,theory(equality)])).
% cnf(273533,plain,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|sz00=xq),inference(cn,[status(thm)],[273532,theory(equality)])).
% cnf(273534,plain,(epred1_0|aElementOf0(esk23_1(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(sr,[status(thm)],[273533,175,theory(equality)])).
% cnf(273553,plain,(sz00=xq|epred1_0|~aInteger0(xq)),inference(spm,[status(thm)],[683,273534,theory(equality)])).
% cnf(273554,plain,(sz00=xq|epred1_0|$false),inference(rw,[status(thm)],[273553,176,theory(equality)])).
% cnf(273555,plain,(sz00=xq|epred1_0),inference(cn,[status(thm)],[273554,theory(equality)])).
% cnf(273556,plain,(epred1_0),inference(sr,[status(thm)],[273555,175,theory(equality)])).
% cnf(274153,negated_conjecture,(aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|$false),inference(rw,[status(thm)],[658,273556,theory(equality)])).
% cnf(274154,negated_conjecture,(aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(cn,[status(thm)],[274153,theory(equality)])).
% cnf(274157,negated_conjecture,(aElementOf0(X1,cS1395)|$false|~aInteger0(X1)),inference(rw,[status(thm)],[660,273556,theory(equality)])).
% cnf(274158,negated_conjecture,(aElementOf0(X1,cS1395)|~aInteger0(X1)),inference(cn,[status(thm)],[274157,theory(equality)])).
% cnf(274159,negated_conjecture,($false|~aElementOf0(esk19_0,cS1395)),inference(rw,[status(thm)],[657,273556,theory(equality)])).
% cnf(274160,negated_conjecture,(~aElementOf0(esk19_0,cS1395)),inference(cn,[status(thm)],[274159,theory(equality)])).
% cnf(274213,negated_conjecture,(sz00=xq|aInteger0(esk19_0)|~aInteger0(xa)|~aInteger0(xq)),inference(spm,[status(thm)],[886,274154,theory(equality)])).
% cnf(274337,negated_conjecture,(sz00=xq|aInteger0(esk19_0)|$false|~aInteger0(xq)),inference(rw,[status(thm)],[274213,177,theory(equality)])).
% cnf(274338,negated_conjecture,(sz00=xq|aInteger0(esk19_0)|$false|$false),inference(rw,[status(thm)],[274337,176,theory(equality)])).
% cnf(274339,negated_conjecture,(sz00=xq|aInteger0(esk19_0)),inference(cn,[status(thm)],[274338,theory(equality)])).
% cnf(274340,negated_conjecture,(aInteger0(esk19_0)),inference(sr,[status(thm)],[274339,175,theory(equality)])).
% cnf(274909,negated_conjecture,(~aInteger0(esk19_0)),inference(spm,[status(thm)],[274160,274158,theory(equality)])).
% cnf(274913,negated_conjecture,($false),inference(rw,[status(thm)],[274909,274340,theory(equality)])).
% cnf(274914,negated_conjecture,($false),inference(cn,[status(thm)],[274913,theory(equality)])).
% cnf(274915,negated_conjecture,($false),274914,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 10845
% # ...of these trivial : 427
% # ...subsumed : 7183
% # ...remaining for further processing: 3235
% # Other redundant clauses eliminated : 10
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 124
% # Backward-rewritten : 859
% # Generated clauses : 93130
% # ...of the previous two non-trivial : 78234
% # Contextual simplify-reflections : 3316
% # Paramodulations : 92993
% # Factorizations : 2
% # Equation resolutions : 132
% # Current number of processed clauses: 2251
% # Positive orientable unit clauses: 712
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 10
% # Non-unit-clauses : 1529
% # Current number of unprocessed clauses: 43232
% # ...number of literals in the above : 222404
% # Clause-clause subsumption calls (NU) : 218837
% # Rec. Clause-clause subsumption calls : 107500
% # Unit Clause-clause subsumption calls : 3863
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 4418
% # Indexed BW rewrite successes : 120
% # Backwards rewriting index: 1691 leaves, 1.79+/-2.631 terms/leaf
% # Paramod-from index: 779 leaves, 1.93+/-3.188 terms/leaf
% # Paramod-into index: 1455 leaves, 1.71+/-2.479 terms/leaf
% # -------------------------------------------------
% # User time : 5.525 s
% # System time : 0.205 s
% # Total time : 5.730 s
% # Maximum resident set size: 0 pages
% PrfWatch: 9.58 CPU 9.73 WC
% FINAL PrfWatch: 9.58 CPU 9.73 WC
% SZS output end Solution for /tmp/SystemOnTPTP6548/NUM444+6.tptp
%
%------------------------------------------------------------------------------