%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM443+4 : 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:07:25 EST 2010
% Result : Theorem 1.04s
% Output : Solution 1.04s
% 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/SystemOnTPTP6289/NUM443+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6289/NUM443+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6289/NUM443+4.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 6385
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.023 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(17, axiom,![X1]:![X2]:![X3]:((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&~(X3=sz00))=>(sdteqdtlpzmzozddtrp0(X1,X2,X3)=>sdteqdtlpzmzozddtrp0(X2,X1,X3))),file('/tmp/SRASS.s.p', mEquModSym)).
% fof(18, axiom,![X1]:![X2]:![X3]:![X4]:(((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&~(X3=sz00))&aInteger0(X4))=>((sdteqdtlpzmzozddtrp0(X1,X2,X3)&sdteqdtlpzmzozddtrp0(X2,X4,X3))=>sdteqdtlpzmzozddtrp0(X1,X4,X3))),file('/tmp/SRASS.s.p', mEquModTrn)).
% fof(21, axiom,((aInteger0(xa)&aInteger0(xq))&~(xq=sz00)),file('/tmp/SRASS.s.p', m__1962)).
% fof(22, axiom,(aInteger0(xb)&aInteger0(xc)),file('/tmp/SRASS.s.p', m__2010)).
% fof(43, conjecture,(((((((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)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&?[X1]:(aInteger0(X1)&sdtasdt0(xq,X1)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,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)))))=>(~(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))),file('/tmp/SRASS.s.p', m__)).
% fof(44, negated_conjecture,~((((((((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)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&?[X1]:(aInteger0(X1)&sdtasdt0(xq,X1)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,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)))))=>(~(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))),inference(assume_negation,[status(cth)],[43])).
% fof(51, negated_conjecture,~((((((((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)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&?[X1]:(aInteger0(X1)&sdtasdt0(xq,X1)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,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)))))=>(~(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))),inference(fof_simplification,[status(thm)],[44,theory(equality)])).
% fof(115, plain,![X1]:![X2]:![X3]:((((~(aInteger0(X1))|~(aInteger0(X2)))|~(aInteger0(X3)))|X3=sz00)|(~(sdteqdtlpzmzozddtrp0(X1,X2,X3))|sdteqdtlpzmzozddtrp0(X2,X1,X3))),inference(fof_nnf,[status(thm)],[17])).
% fof(116, plain,![X4]:![X5]:![X6]:((((~(aInteger0(X4))|~(aInteger0(X5)))|~(aInteger0(X6)))|X6=sz00)|(~(sdteqdtlpzmzozddtrp0(X4,X5,X6))|sdteqdtlpzmzozddtrp0(X5,X4,X6))),inference(variable_rename,[status(thm)],[115])).
% cnf(117,plain,(sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00|~sdteqdtlpzmzozddtrp0(X2,X1,X3)|~aInteger0(X3)|~aInteger0(X1)|~aInteger0(X2)),inference(split_conjunct,[status(thm)],[116])).
% fof(118, plain,![X1]:![X2]:![X3]:![X4]:(((((~(aInteger0(X1))|~(aInteger0(X2)))|~(aInteger0(X3)))|X3=sz00)|~(aInteger0(X4)))|((~(sdteqdtlpzmzozddtrp0(X1,X2,X3))|~(sdteqdtlpzmzozddtrp0(X2,X4,X3)))|sdteqdtlpzmzozddtrp0(X1,X4,X3))),inference(fof_nnf,[status(thm)],[18])).
% fof(119, plain,![X5]:![X6]:![X7]:![X8]:(((((~(aInteger0(X5))|~(aInteger0(X6)))|~(aInteger0(X7)))|X7=sz00)|~(aInteger0(X8)))|((~(sdteqdtlpzmzozddtrp0(X5,X6,X7))|~(sdteqdtlpzmzozddtrp0(X6,X8,X7)))|sdteqdtlpzmzozddtrp0(X5,X8,X7))),inference(variable_rename,[status(thm)],[118])).
% cnf(120,plain,(sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00|~sdteqdtlpzmzozddtrp0(X4,X2,X3)|~sdteqdtlpzmzozddtrp0(X1,X4,X3)|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X4)|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[119])).
% cnf(138,plain,(xq!=sz00),inference(split_conjunct,[status(thm)],[21])).
% cnf(139,plain,(aInteger0(xq)),inference(split_conjunct,[status(thm)],[21])).
% cnf(140,plain,(aInteger0(xa)),inference(split_conjunct,[status(thm)],[21])).
% cnf(141,plain,(aInteger0(xc)),inference(split_conjunct,[status(thm)],[22])).
% cnf(142,plain,(aInteger0(xb)),inference(split_conjunct,[status(thm)],[22])).
% fof(280, negated_conjecture,(((((((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)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&?[X1]:(aInteger0(X1)&sdtasdt0(xq,X1)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,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)))))&(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))),inference(fof_nnf,[status(thm)],[51])).
% fof(281, negated_conjecture,(((((((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))|((![X5]:(~(aInteger0(X5))|~(sdtasdt0(xq,X5)=sdtpldt0(X3,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X3,xa,xq))))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&?[X6]:(aInteger0(X6)&sdtasdt0(xq,X6)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,xq))&((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(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))),inference(variable_rename,[status(thm)],[280])).
% fof(282, negated_conjecture,(((((((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X3]:((~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X3)&(aInteger0(esk16_1(X3))&sdtasdt0(xq,esk16_1(X3))=sdtpldt0(X3,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X3,xa,xq)))&((~(aInteger0(X3))|((![X5]:(~(aInteger0(X5))|~(sdtasdt0(xq,X5)=sdtpldt0(X3,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X3,xa,xq))))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(aInteger0(esk17_0)&sdtasdt0(xq,esk17_0)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,xq))&((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))&![X7]:((~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X7)&(aInteger0(esk18_1(X7))&sdtasdt0(xq,esk18_1(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(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))),inference(skolemize,[status(esa)],[281])).
% fof(283, negated_conjecture,![X3]:![X5]:![X7]:![X9]:(((((((((~(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(esk18_1(X7))&sdtasdt0(xq,esk18_1(X7))=sdtpldt0(X7,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X7,xa,xq))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&((((((((((((~(aInteger0(X5))|~(sdtasdt0(xq,X5)=sdtpldt0(X3,smndt0(xa))))&~(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))))&~(sdteqdtlpzmzozddtrp0(X3,xa,xq)))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X3)&(aInteger0(esk16_1(X3))&sdtasdt0(xq,esk16_1(X3))=sdtpldt0(X3,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X3,xa,xq))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(aInteger0(esk17_0)&sdtasdt0(xq,esk17_0)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,xq))),inference(shift_quantors,[status(thm)],[282])).
% fof(284, negated_conjecture,![X3]:![X5]:![X7]:![X9]:(((((((((~(aInteger0(X9))|~(sdtasdt0(xq,X9)=sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&((~(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa))))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((~(sdteqdtlpzmzozddtrp0(X7,xa,xq))|~(aInteger0(X7)))|aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((((aInteger0(X7)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((aInteger0(esk18_1(X7))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(sdtasdt0(xq,esk18_1(X7))=sdtpldt0(X7,smndt0(xa))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&(aDivisorOf0(xq,sdtpldt0(X7,smndt0(xa)))|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&(sdteqdtlpzmzozddtrp0(X7,xa,xq)|~(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&((((((((((((~(aInteger0(X5))|~(sdtasdt0(xq,X5)=sdtpldt0(X3,smndt0(xa))))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))&((~(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa))))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((~(sdteqdtlpzmzozddtrp0(X3,xa,xq))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((((aInteger0(X3)|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&((aInteger0(esk16_1(X3))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(sdtasdt0(xq,esk16_1(X3))=sdtpldt0(X3,smndt0(xa))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&(sdteqdtlpzmzozddtrp0(X3,xa,xq)|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&~(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))))&aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))&(aInteger0(esk17_0)&sdtasdt0(xq,esk17_0)=sdtpldt0(xc,smndt0(xb))))&aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xc,xb,xq))),inference(distribute,[status(thm)],[283])).
% cnf(285,negated_conjecture,(sdteqdtlpzmzozddtrp0(xc,xb,xq)),inference(split_conjunct,[status(thm)],[284])).
% cnf(290,negated_conjecture,(~aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[284])).
% cnf(292,negated_conjecture,(sdteqdtlpzmzozddtrp0(X1,xa,xq)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[284])).
% cnf(297,negated_conjecture,(aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,xa,xq)),inference(split_conjunct,[status(thm)],[284])).
% cnf(301,negated_conjecture,(aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[284])).
% cnf(340,negated_conjecture,(sdteqdtlpzmzozddtrp0(xc,xa,xq)),inference(spm,[status(thm)],[292,301,theory(equality)])).
% cnf(708,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|~aInteger0(xc)|~aInteger0(xq)|~aInteger0(xb)|~aInteger0(X1)),inference(spm,[status(thm)],[120,285,theory(equality)])).
% cnf(710,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|$false|~aInteger0(xq)|~aInteger0(xb)|~aInteger0(X1)),inference(rw,[status(thm)],[708,141,theory(equality)])).
% cnf(711,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|$false|$false|~aInteger0(xb)|~aInteger0(X1)),inference(rw,[status(thm)],[710,139,theory(equality)])).
% cnf(712,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|$false|$false|$false|~aInteger0(X1)),inference(rw,[status(thm)],[711,142,theory(equality)])).
% cnf(713,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|~aInteger0(X1)),inference(cn,[status(thm)],[712,theory(equality)])).
% cnf(714,negated_conjecture,(sdteqdtlpzmzozddtrp0(X1,xb,xq)|~sdteqdtlpzmzozddtrp0(X1,xc,xq)|~aInteger0(X1)),inference(sr,[status(thm)],[713,138,theory(equality)])).
% cnf(944,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,xc,xq)|~aInteger0(xq)|~aInteger0(xc)|~aInteger0(xa)),inference(spm,[status(thm)],[117,340,theory(equality)])).
% cnf(948,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,xc,xq)|$false|~aInteger0(xc)|~aInteger0(xa)),inference(rw,[status(thm)],[944,139,theory(equality)])).
% cnf(949,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,xc,xq)|$false|$false|~aInteger0(xa)),inference(rw,[status(thm)],[948,141,theory(equality)])).
% cnf(950,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,xc,xq)|$false|$false|$false),inference(rw,[status(thm)],[949,140,theory(equality)])).
% cnf(951,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,xc,xq)),inference(cn,[status(thm)],[950,theory(equality)])).
% cnf(952,negated_conjecture,(sdteqdtlpzmzozddtrp0(xa,xc,xq)),inference(sr,[status(thm)],[951,138,theory(equality)])).
% cnf(1347,negated_conjecture,(sdteqdtlpzmzozddtrp0(xa,xb,xq)|~aInteger0(xa)),inference(spm,[status(thm)],[714,952,theory(equality)])).
% cnf(1355,negated_conjecture,(sdteqdtlpzmzozddtrp0(xa,xb,xq)|$false),inference(rw,[status(thm)],[1347,140,theory(equality)])).
% cnf(1356,negated_conjecture,(sdteqdtlpzmzozddtrp0(xa,xb,xq)),inference(cn,[status(thm)],[1355,theory(equality)])).
% cnf(1375,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xb,xa,xq)|~aInteger0(xq)|~aInteger0(xa)|~aInteger0(xb)),inference(spm,[status(thm)],[117,1356,theory(equality)])).
% cnf(1378,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xb,xa,xq)|$false|~aInteger0(xa)|~aInteger0(xb)),inference(rw,[status(thm)],[1375,139,theory(equality)])).
% cnf(1379,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xb,xa,xq)|$false|$false|~aInteger0(xb)),inference(rw,[status(thm)],[1378,140,theory(equality)])).
% cnf(1380,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xb,xa,xq)|$false|$false|$false),inference(rw,[status(thm)],[1379,142,theory(equality)])).
% cnf(1381,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xb,xa,xq)),inference(cn,[status(thm)],[1380,theory(equality)])).
% cnf(1382,negated_conjecture,(sdteqdtlpzmzozddtrp0(xb,xa,xq)),inference(sr,[status(thm)],[1381,138,theory(equality)])).
% cnf(1396,negated_conjecture,(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~aInteger0(xb)),inference(spm,[status(thm)],[297,1382,theory(equality)])).
% cnf(1412,negated_conjecture,(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))|$false),inference(rw,[status(thm)],[1396,142,theory(equality)])).
% cnf(1413,negated_conjecture,(aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(cn,[status(thm)],[1412,theory(equality)])).
% cnf(1414,negated_conjecture,($false),inference(sr,[status(thm)],[1413,290,theory(equality)])).
% cnf(1415,negated_conjecture,($false),1414,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 184
% # ...of these trivial : 9
% # ...subsumed : 7
% # ...remaining for further processing: 168
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 5
% # Generated clauses : 413
% # ...of the previous two non-trivial : 363
% # Contextual simplify-reflections : 1
% # Paramodulations : 378
% # Factorizations : 0
% # Equation resolutions : 35
% # Current number of processed clauses: 163
% # Positive orientable unit clauses: 41
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 119
% # Current number of unprocessed clauses: 306
% # ...number of literals in the above : 1264
% # Clause-clause subsumption calls (NU) : 450
% # Rec. Clause-clause subsumption calls : 176
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 5
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 177 leaves, 1.38+/-1.099 terms/leaf
% # Paramod-from index: 73 leaves, 1.05+/-0.228 terms/leaf
% # Paramod-into index: 131 leaves, 1.19+/-0.594 terms/leaf
% # -------------------------------------------------
% # User time : 0.050 s
% # System time : 0.003 s
% # Total time : 0.053 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.25 WC
% FINAL PrfWatch: 0.16 CPU 0.25 WC
% SZS output end Solution for /tmp/SystemOnTPTP6289/NUM443+4.tptp
%
%------------------------------------------------------------------------------