%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM442+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 : art01.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:10 EST 2010
% Result : Theorem 7.73s
% Output : Solution 7.73s
% 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/SystemOnTPTP10164/NUM442+6.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10164/NUM442+6.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10164/NUM442+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 10260
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.03 WC
% PrfWatch: 3.92 CPU 4.04 WC
% # Preprocessing time : 0.026 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 5.90 CPU 6.04 WC
% # 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(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,(((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,~((((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,~((((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,~((((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(116, 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(117, 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)],[116])).
% cnf(118,plain,(sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00|~sdteqdtlpzmzozddtrp0(X2,X1,X3)|~aInteger0(X3)|~aInteger0(X1)|~aInteger0(X2)),inference(split_conjunct,[status(thm)],[117])).
% fof(119, 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(120, 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)],[119])).
% cnf(121,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)],[120])).
% 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(157,plain,(X1=sz00|aElementOf0(X4,X3)|~aInteger0(X1)|~aInteger0(X2)|X3!=szAzrzSzezqlpdtcmdtrp0(X2,X1)|~sdteqdtlpzmzozddtrp0(X4,X2,X1)|~aInteger0(X4)),inference(split_conjunct,[status(thm)],[152])).
% 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,(((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,(((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)))))&((aSet0(cS1395)&![X6]:((~(aElementOf0(X6,cS1395))|aInteger0(X6))&(~(aInteger0(X6))|aElementOf0(X6,cS1395))))&(?[X7]:(aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(X7,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))))|~(epred1_0)),inference(variable_rename,[status(thm)],[279])).
% fof(281, 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)))))&((aSet0(cS1395)&![X6]:((~(aElementOf0(X6,cS1395))|aInteger0(X6))&(~(aInteger0(X6))|aElementOf0(X6,cS1395))))&((aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(esk17_0,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))))|~(epred1_0)),inference(skolemize,[status(esa)],[280])).
% fof(282, negated_conjecture,![X3]:![X5]:![X6]:((((((~(aElementOf0(X6,cS1395))|aInteger0(X6))&(~(aInteger0(X6))|aElementOf0(X6,cS1395)))&aSet0(cS1395))&((aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))&~(aElementOf0(esk17_0,cS1395)))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395))))&(((((((~(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))))|~(epred1_0)),inference(shift_quantors,[status(thm)],[281])).
% fof(283, negated_conjecture,![X3]:![X5]:![X6]:((((((~(aElementOf0(X6,cS1395))|aInteger0(X6))|~(epred1_0))&((~(aInteger0(X6))|aElementOf0(X6,cS1395))|~(epred1_0)))&(aSet0(cS1395)|~(epred1_0)))&(((aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(epred1_0))&(~(aElementOf0(esk17_0,cS1395))|~(epred1_0)))&(~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395))|~(epred1_0))))&((((((((~(aInteger0(X5))|~(sdtasdt0(xq,X5)=sdtpldt0(X3,smndt0(xa))))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(epred1_0))&(((~(aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa))))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(epred1_0)))&(((~(sdteqdtlpzmzozddtrp0(X3,xa,xq))|~(aInteger0(X3)))|aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~(epred1_0)))&(((((aInteger0(X3)|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0))&(((aInteger0(esk16_1(X3))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0))&((sdtasdt0(xq,esk16_1(X3))=sdtpldt0(X3,smndt0(xa))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0))))&((aDivisorOf0(xq,sdtpldt0(X3,smndt0(xa)))|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0)))&((sdteqdtlpzmzozddtrp0(X3,xa,xq)|~(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|~(epred1_0))))&(aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))|~(epred1_0)))),inference(distribute,[status(thm)],[282])).
% cnf(285,negated_conjecture,(sdteqdtlpzmzozddtrp0(X1,xa,xq)|~epred1_0|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[283])).
% cnf(294,negated_conjecture,(~epred1_0|~aElementOf0(esk17_0,cS1395)),inference(split_conjunct,[status(thm)],[283])).
% cnf(295,negated_conjecture,(aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~epred1_0),inference(split_conjunct,[status(thm)],[283])).
% cnf(297,negated_conjecture,(aElementOf0(X1,cS1395)|~epred1_0|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[283])).
% fof(299, 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(300, 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)],[299])).
% fof(301, plain,((![X5]:((~(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq)))|(((aInteger0(X5)&(aInteger0(esk18_1(X5))&sdtasdt0(xq,esk18_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(esk19_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))&![X10]:((~(aInteger0(X10))|X10=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))&![X11]:((~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))|(((aInteger0(X11)&(aInteger0(esk20_2(X10,X11))&sdtasdt0(X10,esk20_2(X10,X11))=sdtpldt0(X11,smndt0(esk19_0))))&aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0))))&sdteqdtlpzmzozddtrp0(X11,esk19_0,X10)))&((~(aInteger0(X11))|((![X13]:(~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(esk19_0))))&~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0)))))&~(sdteqdtlpzmzozddtrp0(X11,esk19_0,X10))))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))))&((aElementOf0(esk21_1(X10),szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))&~(aElementOf0(esk21_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))&~(isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))&~(isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))|epred1_0),inference(skolemize,[status(esa)],[300])).
% fof(302, plain,![X5]:![X7]:![X8]:![X10]:![X11]:![X13]:(((((((((((((((~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(esk19_0))))&~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0)))))&~(sdteqdtlpzmzozddtrp0(X11,esk19_0,X10)))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))&(~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))|(((aInteger0(X11)&(aInteger0(esk20_2(X10,X11))&sdtasdt0(X10,esk20_2(X10,X11))=sdtpldt0(X11,smndt0(esk19_0))))&aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0))))&sdteqdtlpzmzozddtrp0(X11,esk19_0,X10))))&aSet0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))&((aElementOf0(esk21_1(X10),szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))&~(aElementOf0(esk21_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))&~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))|(~(aInteger0(X10))|X10=sz00))&aElementOf0(esk19_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(esk18_1(X5))&sdtasdt0(xq,esk18_1(X5))=sdtpldt0(X5,smndt0(xa))))&aDivisorOf0(xq,sdtpldt0(X5,smndt0(xa))))&sdteqdtlpzmzozddtrp0(X5,xa,xq)))))|epred1_0),inference(shift_quantors,[status(thm)],[301])).
% fof(303, plain,![X5]:![X7]:![X8]:![X10]:![X11]:![X13]:(((((((((((((((~(aInteger0(X13))|~(sdtasdt0(X10,X13)=sdtpldt0(X11,smndt0(esk19_0))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))|(~(aInteger0(X10))|X10=sz00))|epred1_0)&((((~(aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0))))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))|(~(aInteger0(X10))|X10=sz00))|epred1_0))&((((~(sdteqdtlpzmzozddtrp0(X11,esk19_0,X10))|~(aInteger0(X11)))|aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10)))|(~(aInteger0(X10))|X10=sz00))|epred1_0))&((((((aInteger0(X11)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))))|(~(aInteger0(X10))|X10=sz00))|epred1_0)&((((aInteger0(esk20_2(X10,X11))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))))|(~(aInteger0(X10))|X10=sz00))|epred1_0)&(((sdtasdt0(X10,esk20_2(X10,X11))=sdtpldt0(X11,smndt0(esk19_0))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))))|(~(aInteger0(X10))|X10=sz00))|epred1_0)))&(((aDivisorOf0(X10,sdtpldt0(X11,smndt0(esk19_0)))|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))))|(~(aInteger0(X10))|X10=sz00))|epred1_0))&(((sdteqdtlpzmzozddtrp0(X11,esk19_0,X10)|~(aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))))|(~(aInteger0(X10))|X10=sz00))|epred1_0)))&((aSet0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))|(~(aInteger0(X10))|X10=sz00))|epred1_0))&((((aElementOf0(esk21_1(X10),szAzrzSzezqlpdtcmdtrp0(esk19_0,X10))|(~(aInteger0(X10))|X10=sz00))|epred1_0)&((~(aElementOf0(esk21_1(X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|X10=sz00))|epred1_0))&((~(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk19_0,X10),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))|(~(aInteger0(X10))|X10=sz00))|epred1_0)))&(aElementOf0(esk19_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(esk18_1(X5))|~(aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(xa,xq))))|epred1_0)&((sdtasdt0(xq,esk18_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)],[302])).
% cnf(304,plain,(epred1_0|sdteqdtlpzmzozddtrp0(X1,xa,xq)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[303])).
% cnf(314,plain,(epred1_0|aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[303])).
% cnf(315,plain,(epred1_0|~aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(split_conjunct,[status(thm)],[303])).
% cnf(316,plain,(epred1_0|aInteger0(X1)|~aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[303])).
% cnf(318,plain,(epred1_0|aElementOf0(esk19_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[303])).
% cnf(320,plain,(epred1_0|X1=sz00|~aInteger0(X1)|~aElementOf0(esk21_1(X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(split_conjunct,[status(thm)],[303])).
% cnf(321,plain,(epred1_0|X1=sz00|aElementOf0(esk21_1(X1),szAzrzSzezqlpdtcmdtrp0(esk19_0,X1))|~aInteger0(X1)),inference(split_conjunct,[status(thm)],[303])).
% cnf(323,plain,(epred1_0|X1=sz00|sdteqdtlpzmzozddtrp0(X2,esk19_0,X1)|~aInteger0(X1)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(esk19_0,X1))),inference(split_conjunct,[status(thm)],[303])).
% cnf(327,plain,(epred1_0|X1=sz00|aInteger0(X2)|~aInteger0(X1)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(esk19_0,X1))),inference(split_conjunct,[status(thm)],[303])).
% cnf(358,negated_conjecture,(sdteqdtlpzmzozddtrp0(X1,xa,xq)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(csr,[status(thm)],[285,304])).
% cnf(365,plain,(epred1_0|aInteger0(esk19_0)),inference(spm,[status(thm)],[316,318,theory(equality)])).
% cnf(494,plain,(sz00=X1|epred1_0|aInteger0(esk21_1(X1))|~aInteger0(X1)),inference(spm,[status(thm)],[327,321,theory(equality)])).
% cnf(514,plain,(sz00=X1|epred1_0|aElementOf0(esk21_1(X1),szAzrzSzezqlpdtcmdtrp0(xa,xq))|~aInteger0(X1)|~aInteger0(esk21_1(X1))),inference(spm,[status(thm)],[320,314,theory(equality)])).
% cnf(547,plain,(sz00=X1|epred1_0|sdteqdtlpzmzozddtrp0(esk21_1(X1),esk19_0,X1)|~aInteger0(X1)),inference(spm,[status(thm)],[323,321,theory(equality)])).
% cnf(551,plain,(sz00=X1|aInteger0(X2)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X3,X1))|~aInteger0(X3)|~aInteger0(X1)),inference(er,[status(thm)],[159,theory(equality)])).
% cnf(739,plain,(sz00=X1|aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X3,X1))|~sdteqdtlpzmzozddtrp0(X2,X3,X1)|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X1)),inference(er,[status(thm)],[157,theory(equality)])).
% cnf(2304,plain,(sz00=X1|sdteqdtlpzmzozddtrp0(X2,esk19_0,X1)|epred1_0|~sdteqdtlpzmzozddtrp0(X2,esk21_1(X1),X1)|~aInteger0(esk21_1(X1))|~aInteger0(X1)|~aInteger0(esk19_0)|~aInteger0(X2)),inference(spm,[status(thm)],[121,547,theory(equality)])).
% cnf(4672,plain,(sz00=X1|epred1_0|aElementOf0(esk21_1(X1),szAzrzSzezqlpdtcmdtrp0(xa,xq))|~aInteger0(X1)),inference(csr,[status(thm)],[514,494])).
% cnf(4677,negated_conjecture,(sdteqdtlpzmzozddtrp0(esk21_1(X1),xa,xq)|sz00=X1|epred1_0|~aInteger0(X1)),inference(spm,[status(thm)],[358,4672,theory(equality)])).
% cnf(5538,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|sz00=X1|epred1_0|~aInteger0(xq)|~aInteger0(esk21_1(X1))|~aInteger0(xa)|~aInteger0(X1)),inference(spm,[status(thm)],[118,4677,theory(equality)])).
% cnf(5543,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|sz00=X1|epred1_0|$false|~aInteger0(esk21_1(X1))|~aInteger0(xa)|~aInteger0(X1)),inference(rw,[status(thm)],[5538,176,theory(equality)])).
% cnf(5544,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|sz00=X1|epred1_0|$false|~aInteger0(esk21_1(X1))|$false|~aInteger0(X1)),inference(rw,[status(thm)],[5543,177,theory(equality)])).
% cnf(5545,negated_conjecture,(sz00=xq|sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|sz00=X1|epred1_0|~aInteger0(esk21_1(X1))|~aInteger0(X1)),inference(cn,[status(thm)],[5544,theory(equality)])).
% cnf(5546,negated_conjecture,(sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|sz00=X1|epred1_0|~aInteger0(esk21_1(X1))|~aInteger0(X1)),inference(sr,[status(thm)],[5545,175,theory(equality)])).
% cnf(113638,plain,(sz00=X1|epred1_0|sdteqdtlpzmzozddtrp0(X2,esk19_0,X1)|~sdteqdtlpzmzozddtrp0(X2,esk21_1(X1),X1)|~aInteger0(esk21_1(X1))|~aInteger0(X2)|~aInteger0(X1)),inference(csr,[status(thm)],[2304,365])).
% cnf(113639,plain,(sz00=X1|epred1_0|sdteqdtlpzmzozddtrp0(X2,esk19_0,X1)|~sdteqdtlpzmzozddtrp0(X2,esk21_1(X1),X1)|~aInteger0(X1)|~aInteger0(X2)),inference(csr,[status(thm)],[113638,494])).
% cnf(210864,negated_conjecture,(sz00=X1|epred1_0|sdteqdtlpzmzozddtrp0(xa,esk21_1(X1),xq)|~aInteger0(X1)),inference(csr,[status(thm)],[5546,494])).
% cnf(210875,plain,(sz00=xq|epred1_0|sdteqdtlpzmzozddtrp0(xa,esk19_0,xq)|~aInteger0(xq)|~aInteger0(xa)),inference(spm,[status(thm)],[113639,210864,theory(equality)])).
% cnf(210908,plain,(sz00=xq|epred1_0|sdteqdtlpzmzozddtrp0(xa,esk19_0,xq)|$false|~aInteger0(xa)),inference(rw,[status(thm)],[210875,176,theory(equality)])).
% cnf(210909,plain,(sz00=xq|epred1_0|sdteqdtlpzmzozddtrp0(xa,esk19_0,xq)|$false|$false),inference(rw,[status(thm)],[210908,177,theory(equality)])).
% cnf(210910,plain,(sz00=xq|epred1_0|sdteqdtlpzmzozddtrp0(xa,esk19_0,xq)),inference(cn,[status(thm)],[210909,theory(equality)])).
% cnf(210911,plain,(epred1_0|sdteqdtlpzmzozddtrp0(xa,esk19_0,xq)),inference(sr,[status(thm)],[210910,175,theory(equality)])).
% cnf(210912,plain,(sz00=xq|sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)|epred1_0|~aInteger0(xq)|~aInteger0(xa)|~aInteger0(esk19_0)),inference(spm,[status(thm)],[118,210911,theory(equality)])).
% cnf(210923,plain,(sz00=xq|sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)|epred1_0|$false|~aInteger0(xa)|~aInteger0(esk19_0)),inference(rw,[status(thm)],[210912,176,theory(equality)])).
% cnf(210924,plain,(sz00=xq|sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)|epred1_0|$false|$false|~aInteger0(esk19_0)),inference(rw,[status(thm)],[210923,177,theory(equality)])).
% cnf(210925,plain,(sz00=xq|sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)|epred1_0|~aInteger0(esk19_0)),inference(cn,[status(thm)],[210924,theory(equality)])).
% cnf(210926,plain,(sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)|epred1_0|~aInteger0(esk19_0)),inference(sr,[status(thm)],[210925,175,theory(equality)])).
% cnf(211002,plain,(epred1_0|sdteqdtlpzmzozddtrp0(esk19_0,xa,xq)),inference(csr,[status(thm)],[210926,365])).
% cnf(211007,plain,(sz00=xq|aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|epred1_0|~aInteger0(esk19_0)|~aInteger0(xa)|~aInteger0(xq)),inference(spm,[status(thm)],[739,211002,theory(equality)])).
% cnf(211033,plain,(sz00=xq|aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|epred1_0|~aInteger0(esk19_0)|$false|~aInteger0(xq)),inference(rw,[status(thm)],[211007,177,theory(equality)])).
% cnf(211034,plain,(sz00=xq|aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|epred1_0|~aInteger0(esk19_0)|$false|$false),inference(rw,[status(thm)],[211033,176,theory(equality)])).
% cnf(211035,plain,(sz00=xq|aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|epred1_0|~aInteger0(esk19_0)),inference(cn,[status(thm)],[211034,theory(equality)])).
% cnf(211036,plain,(aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|epred1_0|~aInteger0(esk19_0)),inference(sr,[status(thm)],[211035,175,theory(equality)])).
% cnf(211424,plain,(epred1_0|aElementOf0(esk19_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(csr,[status(thm)],[211036,365])).
% cnf(211433,plain,(epred1_0|~aElementOf0(esk19_0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))),inference(spm,[status(thm)],[315,211424,theory(equality)])).
% cnf(211456,plain,(epred1_0),inference(csr,[status(thm)],[211433,318])).
% cnf(212093,negated_conjecture,(aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))|$false),inference(rw,[status(thm)],[295,211456,theory(equality)])).
% cnf(212094,negated_conjecture,(aElementOf0(esk17_0,szAzrzSzezqlpdtcmdtrp0(xa,xq))),inference(cn,[status(thm)],[212093,theory(equality)])).
% cnf(212099,negated_conjecture,(aElementOf0(X1,cS1395)|$false|~aInteger0(X1)),inference(rw,[status(thm)],[297,211456,theory(equality)])).
% cnf(212100,negated_conjecture,(aElementOf0(X1,cS1395)|~aInteger0(X1)),inference(cn,[status(thm)],[212099,theory(equality)])).
% cnf(212101,negated_conjecture,($false|~aElementOf0(esk17_0,cS1395)),inference(rw,[status(thm)],[294,211456,theory(equality)])).
% cnf(212102,negated_conjecture,(~aElementOf0(esk17_0,cS1395)),inference(cn,[status(thm)],[212101,theory(equality)])).
% cnf(212192,negated_conjecture,(sz00=xq|aInteger0(esk17_0)|~aInteger0(xa)|~aInteger0(xq)),inference(spm,[status(thm)],[551,212094,theory(equality)])).
% cnf(212200,negated_conjecture,(sz00=xq|aInteger0(esk17_0)|$false|~aInteger0(xq)),inference(rw,[status(thm)],[212192,177,theory(equality)])).
% cnf(212201,negated_conjecture,(sz00=xq|aInteger0(esk17_0)|$false|$false),inference(rw,[status(thm)],[212200,176,theory(equality)])).
% cnf(212202,negated_conjecture,(sz00=xq|aInteger0(esk17_0)),inference(cn,[status(thm)],[212201,theory(equality)])).
% cnf(212203,negated_conjecture,(aInteger0(esk17_0)),inference(sr,[status(thm)],[212202,175,theory(equality)])).
% cnf(212392,negated_conjecture,(~aInteger0(esk17_0)),inference(spm,[status(thm)],[212102,212100,theory(equality)])).
% cnf(212396,negated_conjecture,($false),inference(rw,[status(thm)],[212392,212203,theory(equality)])).
% cnf(212397,negated_conjecture,($false),inference(cn,[status(thm)],[212396,theory(equality)])).
% cnf(212398,negated_conjecture,($false),212397,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 7281
% # ...of these trivial : 257
% # ...subsumed : 4791
% # ...remaining for further processing: 2233
% # Other redundant clauses eliminated : 10
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 65
% # Backward-rewritten : 748
% # Generated clauses : 73497
% # ...of the previous two non-trivial : 61474
% # Contextual simplify-reflections : 1413
% # Paramodulations : 73404
% # Factorizations : 2
% # Equation resolutions : 91
% # Current number of processed clauses: 1420
% # Positive orientable unit clauses: 435
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 980
% # Current number of unprocessed clauses: 39127
% # ...number of literals in the above : 154518
% # Clause-clause subsumption calls (NU) : 99794
% # Rec. Clause-clause subsumption calls : 67648
% # Unit Clause-clause subsumption calls : 1130
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1233
% # Indexed BW rewrite successes : 56
% # Backwards rewriting index: 1309 leaves, 1.57+/-1.982 terms/leaf
% # Paramod-from index: 684 leaves, 1.66+/-2.170 terms/leaf
% # Paramod-into index: 1123 leaves, 1.56+/-1.828 terms/leaf
% # -------------------------------------------------
% # User time : 3.701 s
% # System time : 0.158 s
% # Total time : 3.859 s
% # Maximum resident set size: 0 pages
% PrfWatch: 6.69 CPU 6.84 WC
% FINAL PrfWatch: 6.69 CPU 6.84 WC
% SZS output end Solution for /tmp/SystemOnTPTP10164/NUM442+6.tptp
%
%------------------------------------------------------------------------------