%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM450+6 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:35:50 EDT 2024
% Result : Theorem 206.00s 206.23s
% Output : Refutation 206.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM450+6 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 16:36:07 EDT 2024
% 0.14/0.34 % CPUTime :
% 206.00/206.23 % Version: 1.5
% 206.00/206.23 % SZS status Theorem
% 206.00/206.23 % SZS output start CNFRefutation
% 206.00/206.23 fof(m__2144,plain,(((((((((aSet0(sbsmnsldt0(xS))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&(~aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=>(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((aInteger0(W2)&(((?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))|aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))|sdteqdtlpzmzozddtrp0(W2,W0,W1)))=>aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&(~aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=>(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((aInteger0(W2)&(((?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))|aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))|sdteqdtlpzmzozddtrp0(W2,W0,W1)))=>aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__2144)).
% 206.00/206.23 fof(c46,plain,(((((((((aSet0(sbsmnsldt0(xS))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=>(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((aInteger0(W2)&(((?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))|aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))|sdteqdtlpzmzozddtrp0(W2,W0,W1)))=>aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=>(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((aInteger0(W2)&(((?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))|aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))|sdteqdtlpzmzozddtrp0(W2,W0,W1)))=>aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=>aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),inference(fof_simplification,[status(thm)],[m__2144])).
% 206.00/206.23 fof(c47,plain,(((((((((aSet0(sbsmnsldt0(xS))&(![W0]:((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]:((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&(![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]:(~aInteger0(W3)|sdtasdt0(W1,W3)!=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]:((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]:((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&(![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]:((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]:(~aInteger0(W3)|sdtasdt0(W1,W3)!=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),inference(fof_nnf,[status(thm)],[c46])).
% 206.00/206.23 fof(c48,plain,(((((((((aSet0(sbsmnsldt0(xS))&((![W0]:(~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]:((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&((![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]:((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&(![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]:((~aInteger0(W2)|(((![W3]:(~aInteger0(W3)|sdtasdt0(W1,W3)!=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![W0]:(~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]:((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&((![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]:((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&(![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]:(((((aInteger0(W1)&W1!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]:(aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]:((~aInteger0(W2)|(((![W3]:(~aInteger0(W3)|sdtasdt0(W1,W3)!=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]:(~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),inference(shift_quantors,[status(thm)],[c47])).
% 206.00/206.23 fof(c49,plain,(((((((((aSet0(sbsmnsldt0(xS))&((![X14]:(~aElementOf0(X14,sbsmnsldt0(xS))|(aInteger0(X14)&(?[X15]:(aElementOf0(X15,xS)&aElementOf0(X14,X15))))))&(![X16]:((~aInteger0(X16)|(![X17]:(~aElementOf0(X17,xS)|~aElementOf0(X16,X17))))|aElementOf0(X16,sbsmnsldt0(xS))))))&((![X18]:(~aElementOf0(X18,stldt0(sbsmnsldt0(xS)))|(aInteger0(X18)&~aElementOf0(X18,sbsmnsldt0(xS)))))&(![X19]:((~aInteger0(X19)|aElementOf0(X19,sbsmnsldt0(xS)))|aElementOf0(X19,stldt0(sbsmnsldt0(xS)))))))&(![X20]:(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(?[X21]:(((((aInteger0(X21)&X21!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X20,X21)))&((![X22]:(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,X21))|(((aInteger0(X22)&(?[X23]:(aInteger0(X23)&sdtasdt0(X21,X23)=sdtpldt0(X22,smndt0(X20)))))&aDivisorOf0(X21,sdtpldt0(X22,smndt0(X20))))&sdteqdtlpzmzozddtrp0(X22,X20,X21))))&(![X24]:((~aInteger0(X24)|(((![X25]:(~aInteger0(X25)|sdtasdt0(X21,X25)!=sdtpldt0(X24,smndt0(X20))))&~aDivisorOf0(X21,sdtpldt0(X24,smndt0(X20))))&~sdteqdtlpzmzozddtrp0(X24,X20,X21)))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,X21))))))&(![X26]:(~aElementOf0(X26,szAzrzSzezqlpdtcmdtrp0(X20,X21))|aElementOf0(X26,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X20,X21),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![X27]:(~aElementOf0(X27,sbsmnsldt0(xS))|(aInteger0(X27)&(?[X28]:(aElementOf0(X28,xS)&aElementOf0(X27,X28))))))&(![X29]:((~aInteger0(X29)|(![X30]:(~aElementOf0(X30,xS)|~aElementOf0(X29,X30))))|aElementOf0(X29,sbsmnsldt0(xS))))))&((![X31]:(~aElementOf0(X31,stldt0(sbsmnsldt0(xS)))|(aInteger0(X31)&~aElementOf0(X31,sbsmnsldt0(xS)))))&(![X32]:((~aInteger0(X32)|aElementOf0(X32,sbsmnsldt0(xS)))|aElementOf0(X32,stldt0(sbsmnsldt0(xS)))))))&(![X33]:(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(?[X34]:(((((aInteger0(X34)&X34!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X33,X34)))&((![X35]:(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,X34))|(((aInteger0(X35)&(?[X36]:(aInteger0(X36)&sdtasdt0(X34,X36)=sdtpldt0(X35,smndt0(X33)))))&aDivisorOf0(X34,sdtpldt0(X35,smndt0(X33))))&sdteqdtlpzmzozddtrp0(X35,X33,X34))))&(![X37]:((~aInteger0(X37)|(((![X38]:(~aInteger0(X38)|sdtasdt0(X34,X38)!=sdtpldt0(X37,smndt0(X33))))&~aDivisorOf0(X34,sdtpldt0(X37,smndt0(X33))))&~sdteqdtlpzmzozddtrp0(X37,X33,X34)))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,X34))))))&(![X39]:(~aElementOf0(X39,szAzrzSzezqlpdtcmdtrp0(X33,X34))|aElementOf0(X39,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X33,X34),stldt0(sbsmnsldt0(xS)))))))),inference(variable_rename,[status(thm)],[c48])).
% 206.00/206.23 fof(c51,plain,(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X22]:(![X24]:(![X25]:(![X26]:(![X27]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X35]:(![X37]:(![X38]:(![X39]:(((((((((aSet0(sbsmnsldt0(xS))&((~aElementOf0(X14,sbsmnsldt0(xS))|(aInteger0(X14)&(aElementOf0(skolem0004(X14),xS)&aElementOf0(X14,skolem0004(X14)))))&((~aInteger0(X16)|(~aElementOf0(X17,xS)|~aElementOf0(X16,X17)))|aElementOf0(X16,sbsmnsldt0(xS)))))&((~aElementOf0(X18,stldt0(sbsmnsldt0(xS)))|(aInteger0(X18)&~aElementOf0(X18,sbsmnsldt0(xS))))&((~aInteger0(X19)|aElementOf0(X19,sbsmnsldt0(xS)))|aElementOf0(X19,stldt0(sbsmnsldt0(xS))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(skolem0005(X20))&skolem0005(X20)!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20))))&((~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|(((aInteger0(X22)&(aInteger0(skolem0006(X20,X22))&sdtasdt0(skolem0005(X20),skolem0006(X20,X22))=sdtpldt0(X22,smndt0(X20))))&aDivisorOf0(skolem0005(X20),sdtpldt0(X22,smndt0(X20))))&sdteqdtlpzmzozddtrp0(X22,X20,skolem0005(X20))))&((~aInteger0(X24)|(((~aInteger0(X25)|sdtasdt0(skolem0005(X20),X25)!=sdtpldt0(X24,smndt0(X20)))&~aDivisorOf0(skolem0005(X20),sdtpldt0(X24,smndt0(X20))))&~sdteqdtlpzmzozddtrp0(X24,X20,skolem0005(X20))))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20))))))&(~aElementOf0(X26,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aElementOf0(X26,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)),stldt0(sbsmnsldt0(xS))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((~aElementOf0(X27,sbsmnsldt0(xS))|(aInteger0(X27)&(aElementOf0(skolem0007(X27),xS)&aElementOf0(X27,skolem0007(X27)))))&((~aInteger0(X29)|(~aElementOf0(X30,xS)|~aElementOf0(X29,X30)))|aElementOf0(X29,sbsmnsldt0(xS)))))&((~aElementOf0(X31,stldt0(sbsmnsldt0(xS)))|(aInteger0(X31)&~aElementOf0(X31,sbsmnsldt0(xS))))&((~aInteger0(X32)|aElementOf0(X32,sbsmnsldt0(xS)))|aElementOf0(X32,stldt0(sbsmnsldt0(xS))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(skolem0008(X33))&skolem0008(X33)!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33))))&((~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|(((aInteger0(X35)&(aInteger0(skolem0009(X33,X35))&sdtasdt0(skolem0008(X33),skolem0009(X33,X35))=sdtpldt0(X35,smndt0(X33))))&aDivisorOf0(skolem0008(X33),sdtpldt0(X35,smndt0(X33))))&sdteqdtlpzmzozddtrp0(X35,X33,skolem0008(X33))))&((~aInteger0(X37)|(((~aInteger0(X38)|sdtasdt0(skolem0008(X33),X38)!=sdtpldt0(X37,smndt0(X33)))&~aDivisorOf0(skolem0008(X33),sdtpldt0(X37,smndt0(X33))))&~sdteqdtlpzmzozddtrp0(X37,X33,skolem0008(X33))))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33))))))&(~aElementOf0(X39,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aElementOf0(X39,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)),stldt0(sbsmnsldt0(xS)))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,(((((((((aSet0(sbsmnsldt0(xS))&((![X14]:(~aElementOf0(X14,sbsmnsldt0(xS))|(aInteger0(X14)&(aElementOf0(skolem0004(X14),xS)&aElementOf0(X14,skolem0004(X14))))))&(![X16]:((~aInteger0(X16)|(![X17]:(~aElementOf0(X17,xS)|~aElementOf0(X16,X17))))|aElementOf0(X16,sbsmnsldt0(xS))))))&((![X18]:(~aElementOf0(X18,stldt0(sbsmnsldt0(xS)))|(aInteger0(X18)&~aElementOf0(X18,sbsmnsldt0(xS)))))&(![X19]:((~aInteger0(X19)|aElementOf0(X19,sbsmnsldt0(xS)))|aElementOf0(X19,stldt0(sbsmnsldt0(xS)))))))&(![X20]:(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(skolem0005(X20))&skolem0005(X20)!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20))))&((![X22]:(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|(((aInteger0(X22)&(aInteger0(skolem0006(X20,X22))&sdtasdt0(skolem0005(X20),skolem0006(X20,X22))=sdtpldt0(X22,smndt0(X20))))&aDivisorOf0(skolem0005(X20),sdtpldt0(X22,smndt0(X20))))&sdteqdtlpzmzozddtrp0(X22,X20,skolem0005(X20)))))&(![X24]:((~aInteger0(X24)|(((![X25]:(~aInteger0(X25)|sdtasdt0(skolem0005(X20),X25)!=sdtpldt0(X24,smndt0(X20))))&~aDivisorOf0(skolem0005(X20),sdtpldt0(X24,smndt0(X20))))&~sdteqdtlpzmzozddtrp0(X24,X20,skolem0005(X20))))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))))))&(![X26]:(~aElementOf0(X26,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aElementOf0(X26,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)),stldt0(sbsmnsldt0(xS)))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![X27]:(~aElementOf0(X27,sbsmnsldt0(xS))|(aInteger0(X27)&(aElementOf0(skolem0007(X27),xS)&aElementOf0(X27,skolem0007(X27))))))&(![X29]:((~aInteger0(X29)|(![X30]:(~aElementOf0(X30,xS)|~aElementOf0(X29,X30))))|aElementOf0(X29,sbsmnsldt0(xS))))))&((![X31]:(~aElementOf0(X31,stldt0(sbsmnsldt0(xS)))|(aInteger0(X31)&~aElementOf0(X31,sbsmnsldt0(xS)))))&(![X32]:((~aInteger0(X32)|aElementOf0(X32,sbsmnsldt0(xS)))|aElementOf0(X32,stldt0(sbsmnsldt0(xS)))))))&(![X33]:(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(skolem0008(X33))&skolem0008(X33)!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33))))&((![X35]:(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|(((aInteger0(X35)&(aInteger0(skolem0009(X33,X35))&sdtasdt0(skolem0008(X33),skolem0009(X33,X35))=sdtpldt0(X35,smndt0(X33))))&aDivisorOf0(skolem0008(X33),sdtpldt0(X35,smndt0(X33))))&sdteqdtlpzmzozddtrp0(X35,X33,skolem0008(X33)))))&(![X37]:((~aInteger0(X37)|(((![X38]:(~aInteger0(X38)|sdtasdt0(skolem0008(X33),X38)!=sdtpldt0(X37,smndt0(X33))))&~aDivisorOf0(skolem0008(X33),sdtpldt0(X37,smndt0(X33))))&~sdteqdtlpzmzozddtrp0(X37,X33,skolem0008(X33))))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))))))&(![X39]:(~aElementOf0(X39,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aElementOf0(X39,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)),stldt0(sbsmnsldt0(xS))))))),inference(skolemize,[status(esa)],[c49])).])).
% 206.00/206.23 fof(c52,plain,(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X22]:(![X24]:(![X25]:(![X26]:(![X27]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X35]:(![X37]:(![X38]:(![X39]:(((((((((aSet0(sbsmnsldt0(xS))&(((~aElementOf0(X14,sbsmnsldt0(xS))|aInteger0(X14))&((~aElementOf0(X14,sbsmnsldt0(xS))|aElementOf0(skolem0004(X14),xS))&(~aElementOf0(X14,sbsmnsldt0(xS))|aElementOf0(X14,skolem0004(X14)))))&((~aInteger0(X16)|(~aElementOf0(X17,xS)|~aElementOf0(X16,X17)))|aElementOf0(X16,sbsmnsldt0(xS)))))&(((~aElementOf0(X18,stldt0(sbsmnsldt0(xS)))|aInteger0(X18))&(~aElementOf0(X18,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X18,sbsmnsldt0(xS))))&((~aInteger0(X19)|aElementOf0(X19,sbsmnsldt0(xS)))|aElementOf0(X19,stldt0(sbsmnsldt0(xS))))))&((((((~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|aInteger0(skolem0005(X20)))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|skolem0005(X20)!=sz00))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|aSet0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))))&(((((~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aInteger0(X22)))&((~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aInteger0(skolem0006(X20,X22))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|sdtasdt0(skolem0005(X20),skolem0006(X20,X22))=sdtpldt0(X22,smndt0(X20))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aDivisorOf0(skolem0005(X20),sdtpldt0(X22,smndt0(X20))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|sdteqdtlpzmzozddtrp0(X22,X20,skolem0005(X20)))))&(((~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X24)|(~aInteger0(X25)|sdtasdt0(skolem0005(X20),X25)!=sdtpldt0(X24,smndt0(X20))))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X24)|~aDivisorOf0(skolem0005(X20),sdtpldt0(X24,smndt0(X20))))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X24)|~sdteqdtlpzmzozddtrp0(X24,X20,skolem0005(X20)))|aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20))))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X26,szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)))|aElementOf0(X26,stldt0(sbsmnsldt0(xS))))))&(~aElementOf0(X20,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X20,skolem0005(X20)),stldt0(sbsmnsldt0(xS))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(((~aElementOf0(X27,sbsmnsldt0(xS))|aInteger0(X27))&((~aElementOf0(X27,sbsmnsldt0(xS))|aElementOf0(skolem0007(X27),xS))&(~aElementOf0(X27,sbsmnsldt0(xS))|aElementOf0(X27,skolem0007(X27)))))&((~aInteger0(X29)|(~aElementOf0(X30,xS)|~aElementOf0(X29,X30)))|aElementOf0(X29,sbsmnsldt0(xS)))))&(((~aElementOf0(X31,stldt0(sbsmnsldt0(xS)))|aInteger0(X31))&(~aElementOf0(X31,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X31,sbsmnsldt0(xS))))&((~aInteger0(X32)|aElementOf0(X32,sbsmnsldt0(xS)))|aElementOf0(X32,stldt0(sbsmnsldt0(xS))))))&((((((~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|aInteger0(skolem0008(X33)))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|skolem0008(X33)!=sz00))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|aSet0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))))&(((((~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aInteger0(X35)))&((~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aInteger0(skolem0009(X33,X35))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|sdtasdt0(skolem0008(X33),skolem0009(X33,X35))=sdtpldt0(X35,smndt0(X33))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aDivisorOf0(skolem0008(X33),sdtpldt0(X35,smndt0(X33))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X35,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|sdteqdtlpzmzozddtrp0(X35,X33,skolem0008(X33)))))&(((~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X37)|(~aInteger0(X38)|sdtasdt0(skolem0008(X33),X38)!=sdtpldt0(X37,smndt0(X33))))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X37)|~aDivisorOf0(skolem0008(X33),sdtpldt0(X37,smndt0(X33))))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|((~aInteger0(X37)|~sdteqdtlpzmzozddtrp0(X37,X33,skolem0008(X33)))|aElementOf0(X37,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33))))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|(~aElementOf0(X39,szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)))|aElementOf0(X39,stldt0(sbsmnsldt0(xS))))))&(~aElementOf0(X33,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X33,skolem0008(X33)),stldt0(sbsmnsldt0(xS)))))))))))))))))))))))))),inference(distribute,[status(thm)],[c51])).
% 206.00/206.23 cnf(c85,plain,~aElementOf0(X355,stldt0(sbsmnsldt0(xS)))|skolem0008(X355)!=sz00,inference(split_conjunct,[status(thm)],[c52])).
% 206.00/206.23 cnf(reflexivity,axiom,X168=X168,theory(equality)).
% 206.00/206.23 fof(m__2079,plain,(((((aSet0(sbsmnsldt0(xS))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&aSet0(stldt0(sbsmnsldt0(xS))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&(~aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(W0=sz10|W0=smndt0(sz10)))))&stldt0(sbsmnsldt0(xS))=cS2076),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__2079)).
% 206.00/206.23 fof(c98,plain,(((((aSet0(sbsmnsldt0(xS))&(![W0]:(aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&aSet0(stldt0(sbsmnsldt0(xS))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]:(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(W0=sz10|W0=smndt0(sz10)))))&stldt0(sbsmnsldt0(xS))=cS2076),inference(fof_simplification,[status(thm)],[m__2079])).
% 206.00/206.23 fof(c99,plain,(((((aSet0(sbsmnsldt0(xS))&(![W0]:((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&aSet0(stldt0(sbsmnsldt0(xS))))&(![W0]:((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&(![W0]:((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10)))&((W0!=sz10&W0!=smndt0(sz10))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076),inference(fof_nnf,[status(thm)],[c98])).
% 206.00/206.23 fof(c100,plain,(((((aSet0(sbsmnsldt0(xS))&((![W0]:(~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]:(aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]:((~aInteger0(W0)|(![W1]:(~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))|aElementOf0(W0,sbsmnsldt0(xS))))))&aSet0(stldt0(sbsmnsldt0(xS))))&((![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]:((~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&((![W0]:(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10))))&(![W0]:((W0!=sz10&W0!=smndt0(sz10))|aElementOf0(W0,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076),inference(shift_quantors,[status(thm)],[c99])).
% 206.00/206.23 fof(c101,plain,(((((aSet0(sbsmnsldt0(xS))&((![X40]:(~aElementOf0(X40,sbsmnsldt0(xS))|(aInteger0(X40)&(?[X41]:(aElementOf0(X41,xS)&aElementOf0(X40,X41))))))&(![X42]:((~aInteger0(X42)|(![X43]:(~aElementOf0(X43,xS)|~aElementOf0(X42,X43))))|aElementOf0(X42,sbsmnsldt0(xS))))))&aSet0(stldt0(sbsmnsldt0(xS))))&((![X44]:(~aElementOf0(X44,stldt0(sbsmnsldt0(xS)))|(aInteger0(X44)&~aElementOf0(X44,sbsmnsldt0(xS)))))&(![X45]:((~aInteger0(X45)|aElementOf0(X45,sbsmnsldt0(xS)))|aElementOf0(X45,stldt0(sbsmnsldt0(xS)))))))&((![X46]:(~aElementOf0(X46,stldt0(sbsmnsldt0(xS)))|(X46=sz10|X46=smndt0(sz10))))&(![X47]:((X47!=sz10&X47!=smndt0(sz10))|aElementOf0(X47,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076),inference(variable_rename,[status(thm)],[c100])).
% 206.00/206.23 fof(c103,plain,(![X40]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(((((aSet0(sbsmnsldt0(xS))&((~aElementOf0(X40,sbsmnsldt0(xS))|(aInteger0(X40)&(aElementOf0(skolem0010(X40),xS)&aElementOf0(X40,skolem0010(X40)))))&((~aInteger0(X42)|(~aElementOf0(X43,xS)|~aElementOf0(X42,X43)))|aElementOf0(X42,sbsmnsldt0(xS)))))&aSet0(stldt0(sbsmnsldt0(xS))))&((~aElementOf0(X44,stldt0(sbsmnsldt0(xS)))|(aInteger0(X44)&~aElementOf0(X44,sbsmnsldt0(xS))))&((~aInteger0(X45)|aElementOf0(X45,sbsmnsldt0(xS)))|aElementOf0(X45,stldt0(sbsmnsldt0(xS))))))&((~aElementOf0(X46,stldt0(sbsmnsldt0(xS)))|(X46=sz10|X46=smndt0(sz10)))&((X47!=sz10&X47!=smndt0(sz10))|aElementOf0(X47,stldt0(sbsmnsldt0(xS))))))&stldt0(sbsmnsldt0(xS))=cS2076)))))))),inference(shift_quantors,[status(thm)],[fof(c102,plain,(((((aSet0(sbsmnsldt0(xS))&((![X40]:(~aElementOf0(X40,sbsmnsldt0(xS))|(aInteger0(X40)&(aElementOf0(skolem0010(X40),xS)&aElementOf0(X40,skolem0010(X40))))))&(![X42]:((~aInteger0(X42)|(![X43]:(~aElementOf0(X43,xS)|~aElementOf0(X42,X43))))|aElementOf0(X42,sbsmnsldt0(xS))))))&aSet0(stldt0(sbsmnsldt0(xS))))&((![X44]:(~aElementOf0(X44,stldt0(sbsmnsldt0(xS)))|(aInteger0(X44)&~aElementOf0(X44,sbsmnsldt0(xS)))))&(![X45]:((~aInteger0(X45)|aElementOf0(X45,sbsmnsldt0(xS)))|aElementOf0(X45,stldt0(sbsmnsldt0(xS)))))))&((![X46]:(~aElementOf0(X46,stldt0(sbsmnsldt0(xS)))|(X46=sz10|X46=smndt0(sz10))))&(![X47]:((X47!=sz10&X47!=smndt0(sz10))|aElementOf0(X47,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076),inference(skolemize,[status(esa)],[c101])).])).
% 206.00/206.23 fof(c104,plain,(![X40]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(((((aSet0(sbsmnsldt0(xS))&(((~aElementOf0(X40,sbsmnsldt0(xS))|aInteger0(X40))&((~aElementOf0(X40,sbsmnsldt0(xS))|aElementOf0(skolem0010(X40),xS))&(~aElementOf0(X40,sbsmnsldt0(xS))|aElementOf0(X40,skolem0010(X40)))))&((~aInteger0(X42)|(~aElementOf0(X43,xS)|~aElementOf0(X42,X43)))|aElementOf0(X42,sbsmnsldt0(xS)))))&aSet0(stldt0(sbsmnsldt0(xS))))&(((~aElementOf0(X44,stldt0(sbsmnsldt0(xS)))|aInteger0(X44))&(~aElementOf0(X44,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X44,sbsmnsldt0(xS))))&((~aInteger0(X45)|aElementOf0(X45,sbsmnsldt0(xS)))|aElementOf0(X45,stldt0(sbsmnsldt0(xS))))))&((~aElementOf0(X46,stldt0(sbsmnsldt0(xS)))|(X46=sz10|X46=smndt0(sz10)))&((X47!=sz10|aElementOf0(X47,stldt0(sbsmnsldt0(xS))))&(X47!=smndt0(sz10)|aElementOf0(X47,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076)))))))),inference(distribute,[status(thm)],[c103])).
% 206.00/206.23 cnf(c115,plain,X388!=sz10|aElementOf0(X388,stldt0(sbsmnsldt0(xS))),inference(split_conjunct,[status(thm)],[c104])).
% 206.00/206.23 cnf(c3375,plain,aElementOf0(sz10,stldt0(sbsmnsldt0(xS))),inference(resolution,[status(thm)],[c115, reflexivity])).
% 206.00/206.23 cnf(c3377,plain,skolem0008(sz10)!=sz00,inference(resolution,[status(thm)],[c3375, c85])).
% 206.00/206.23 cnf(c84,plain,~aElementOf0(X354,stldt0(sbsmnsldt0(xS)))|aInteger0(skolem0008(X354)),inference(split_conjunct,[status(thm)],[c52])).
% 206.00/206.23 cnf(c3386,plain,aInteger0(skolem0008(sz10)),inference(resolution,[status(thm)],[c3375, c84])).
% 206.00/206.23 fof(m__,conjecture,(?[W0]:((aInteger0(W0)&W0!=sz00)&((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]:((aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>(((aInteger0(W1)&(?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((aInteger0(W1)&(((?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))|aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W1,sz10,W0)))=>aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))=>((aSet0(sbsmnsldt0(xS))&(![W1]:(aElementOf0(W1,sbsmnsldt0(xS))<=>(aInteger0(W1)&(?[W2]:(aElementOf0(W2,xS)&aElementOf0(W1,W2)))))))=>((![W1]:(aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W1)&(~aElementOf0(W1,sbsmnsldt0(xS))))))=>((![W1]:(aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 206.00/206.23 fof(c18,negated_conjecture,(~(?[W0]:((aInteger0(W0)&W0!=sz00)&((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]:((aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>(((aInteger0(W1)&(?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((aInteger0(W1)&(((?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))|aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W1,sz10,W0)))=>aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))=>((aSet0(sbsmnsldt0(xS))&(![W1]:(aElementOf0(W1,sbsmnsldt0(xS))<=>(aInteger0(W1)&(?[W2]:(aElementOf0(W2,xS)&aElementOf0(W1,W2)))))))=>((![W1]:(aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W1)&(~aElementOf0(W1,sbsmnsldt0(xS))))))=>((![W1]:(aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))))))))),inference(assume_negation,[status(cth)],[m__])).
% 206.00/206.23 fof(c19,negated_conjecture,(~(?[W0]:((aInteger0(W0)&W0!=sz00)&((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]:((aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>(((aInteger0(W1)&(?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((aInteger0(W1)&(((?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))|aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W1,sz10,W0)))=>aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))=>((aSet0(sbsmnsldt0(xS))&(![W1]:(aElementOf0(W1,sbsmnsldt0(xS))<=>(aInteger0(W1)&(?[W2]:(aElementOf0(W2,xS)&aElementOf0(W1,W2)))))))=>((![W1]:(aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS)))))=>((![W1]:(aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=>aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))))))))),inference(fof_simplification,[status(thm)],[c18])).
% 206.00/206.23 fof(c20,negated_conjecture,(![W0]:((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]:((~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((~aInteger0(W1)|(((![W2]:(~aInteger0(W2)|sdtasdt0(W0,W2)!=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&(![W1]:((~aElementOf0(W1,sbsmnsldt0(xS))|(aInteger0(W1)&(?[W2]:(aElementOf0(W2,xS)&aElementOf0(W1,W2)))))&((~aInteger0(W1)|(![W2]:(~aElementOf0(W2,xS)|~aElementOf0(W1,W2))))|aElementOf0(W1,sbsmnsldt0(xS))))))&((![W1]:((~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS))))&((~aInteger0(W1)|aElementOf0(W1,sbsmnsldt0(xS)))|aElementOf0(W1,stldt0(sbsmnsldt0(xS))))))&((?[W1]:(aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),inference(fof_nnf,[status(thm)],[c19])).
% 206.00/206.23 fof(c21,negated_conjecture,(![W0]:((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&((![W1]:(~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(?[W2]:(aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0))))&(![W1]:((~aInteger0(W1)|(((![W2]:(~aInteger0(W2)|sdtasdt0(W0,W2)!=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&((![W1]:(~aElementOf0(W1,sbsmnsldt0(xS))|(aInteger0(W1)&(?[W2]:(aElementOf0(W2,xS)&aElementOf0(W1,W2))))))&(![W1]:((~aInteger0(W1)|(![W2]:(~aElementOf0(W2,xS)|~aElementOf0(W1,W2))))|aElementOf0(W1,sbsmnsldt0(xS))))))&(((![W1]:(~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS)))))&(![W1]:((~aInteger0(W1)|aElementOf0(W1,sbsmnsldt0(xS)))|aElementOf0(W1,stldt0(sbsmnsldt0(xS))))))&((?[W1]:(aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),inference(shift_quantors,[status(thm)],[c20])).
% 206.00/206.23 fof(c22,negated_conjecture,(![X2]:((~aInteger0(X2)|X2=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,X2))&((![X3]:(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|(((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(sz10)))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(X3,sz10,X2))))&(![X5]:((~aInteger0(X5)|(((![X6]:(~aInteger0(X6)|sdtasdt0(X2,X6)!=sdtpldt0(X5,smndt0(sz10))))&~aDivisorOf0(X2,sdtpldt0(X5,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(X5,sz10,X2)))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2))))))&((aSet0(sbsmnsldt0(xS))&((![X7]:(~aElementOf0(X7,sbsmnsldt0(xS))|(aInteger0(X7)&(?[X8]:(aElementOf0(X8,xS)&aElementOf0(X7,X8))))))&(![X9]:((~aInteger0(X9)|(![X10]:(~aElementOf0(X10,xS)|~aElementOf0(X9,X10))))|aElementOf0(X9,sbsmnsldt0(xS))))))&(((![X11]:(~aElementOf0(X11,stldt0(sbsmnsldt0(xS)))|(aInteger0(X11)&~aElementOf0(X11,sbsmnsldt0(xS)))))&(![X12]:((~aInteger0(X12)|aElementOf0(X12,sbsmnsldt0(xS)))|aElementOf0(X12,stldt0(sbsmnsldt0(xS))))))&((?[X13]:(aElementOf0(X13,szAzrzSzezqlpdtcmdtrp0(sz10,X2))&~aElementOf0(X13,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X2),stldt0(sbsmnsldt0(xS))))))))),inference(variable_rename,[status(thm)],[c21])).
% 206.00/206.23 fof(c24,negated_conjecture,(![X2]:(![X3]:(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:((~aInteger0(X2)|X2=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,X2))&((~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|(((aInteger0(X3)&(aInteger0(skolem0001(X2,X3))&sdtasdt0(X2,skolem0001(X2,X3))=sdtpldt0(X3,smndt0(sz10))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(X3,sz10,X2)))&((~aInteger0(X5)|(((~aInteger0(X6)|sdtasdt0(X2,X6)!=sdtpldt0(X5,smndt0(sz10)))&~aDivisorOf0(X2,sdtpldt0(X5,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(X5,sz10,X2)))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2)))))&((aSet0(sbsmnsldt0(xS))&((~aElementOf0(X7,sbsmnsldt0(xS))|(aInteger0(X7)&(aElementOf0(skolem0002(X2,X7),xS)&aElementOf0(X7,skolem0002(X2,X7)))))&((~aInteger0(X9)|(~aElementOf0(X10,xS)|~aElementOf0(X9,X10)))|aElementOf0(X9,sbsmnsldt0(xS)))))&(((~aElementOf0(X11,stldt0(sbsmnsldt0(xS)))|(aInteger0(X11)&~aElementOf0(X11,sbsmnsldt0(xS))))&((~aInteger0(X12)|aElementOf0(X12,sbsmnsldt0(xS)))|aElementOf0(X12,stldt0(sbsmnsldt0(xS)))))&((aElementOf0(skolem0003(X2),szAzrzSzezqlpdtcmdtrp0(sz10,X2))&~aElementOf0(skolem0003(X2),stldt0(sbsmnsldt0(xS))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X2),stldt0(sbsmnsldt0(xS))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c23,negated_conjecture,(![X2]:((~aInteger0(X2)|X2=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,X2))&((![X3]:(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|(((aInteger0(X3)&(aInteger0(skolem0001(X2,X3))&sdtasdt0(X2,skolem0001(X2,X3))=sdtpldt0(X3,smndt0(sz10))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(X3,sz10,X2))))&(![X5]:((~aInteger0(X5)|(((![X6]:(~aInteger0(X6)|sdtasdt0(X2,X6)!=sdtpldt0(X5,smndt0(sz10))))&~aDivisorOf0(X2,sdtpldt0(X5,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(X5,sz10,X2)))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2))))))&((aSet0(sbsmnsldt0(xS))&((![X7]:(~aElementOf0(X7,sbsmnsldt0(xS))|(aInteger0(X7)&(aElementOf0(skolem0002(X2,X7),xS)&aElementOf0(X7,skolem0002(X2,X7))))))&(![X9]:((~aInteger0(X9)|(![X10]:(~aElementOf0(X10,xS)|~aElementOf0(X9,X10))))|aElementOf0(X9,sbsmnsldt0(xS))))))&(((![X11]:(~aElementOf0(X11,stldt0(sbsmnsldt0(xS)))|(aInteger0(X11)&~aElementOf0(X11,sbsmnsldt0(xS)))))&(![X12]:((~aInteger0(X12)|aElementOf0(X12,sbsmnsldt0(xS)))|aElementOf0(X12,stldt0(sbsmnsldt0(xS))))))&((aElementOf0(skolem0003(X2),szAzrzSzezqlpdtcmdtrp0(sz10,X2))&~aElementOf0(skolem0003(X2),stldt0(sbsmnsldt0(xS))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X2),stldt0(sbsmnsldt0(xS))))))))),inference(skolemize,[status(esa)],[c22])).])).
% 206.00/206.23 fof(c25,negated_conjecture,(![X2]:(![X3]:(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:((((~aInteger0(X2)|X2=sz00)|aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,X2)))&((((((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|aInteger0(X3)))&(((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|aInteger0(skolem0001(X2,X3))))&((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|sdtasdt0(X2,skolem0001(X2,X3))=sdtpldt0(X3,smndt0(sz10))))))&((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz10))))))&((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,X2))|sdteqdtlpzmzozddtrp0(X3,sz10,X2))))&((((~aInteger0(X2)|X2=sz00)|((~aInteger0(X5)|(~aInteger0(X6)|sdtasdt0(X2,X6)!=sdtpldt0(X5,smndt0(sz10))))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2))))&((~aInteger0(X2)|X2=sz00)|((~aInteger0(X5)|~aDivisorOf0(X2,sdtpldt0(X5,smndt0(sz10))))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2)))))&((~aInteger0(X2)|X2=sz00)|((~aInteger0(X5)|~sdteqdtlpzmzozddtrp0(X5,sz10,X2))|aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(sz10,X2)))))))&((((~aInteger0(X2)|X2=sz00)|aSet0(sbsmnsldt0(xS)))&((((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X7,sbsmnsldt0(xS))|aInteger0(X7)))&(((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X7,sbsmnsldt0(xS))|aElementOf0(skolem0002(X2,X7),xS)))&((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X7,sbsmnsldt0(xS))|aElementOf0(X7,skolem0002(X2,X7))))))&((~aInteger0(X2)|X2=sz00)|((~aInteger0(X9)|(~aElementOf0(X10,xS)|~aElementOf0(X9,X10)))|aElementOf0(X9,sbsmnsldt0(xS))))))&(((((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X11,stldt0(sbsmnsldt0(xS)))|aInteger0(X11)))&((~aInteger0(X2)|X2=sz00)|(~aElementOf0(X11,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X11,sbsmnsldt0(xS)))))&((~aInteger0(X2)|X2=sz00)|((~aInteger0(X12)|aElementOf0(X12,sbsmnsldt0(xS)))|aElementOf0(X12,stldt0(sbsmnsldt0(xS))))))&((((~aInteger0(X2)|X2=sz00)|aElementOf0(skolem0003(X2),szAzrzSzezqlpdtcmdtrp0(sz10,X2)))&((~aInteger0(X2)|X2=sz00)|~aElementOf0(skolem0003(X2),stldt0(sbsmnsldt0(xS)))))&((~aInteger0(X2)|X2=sz00)|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X2),stldt0(sbsmnsldt0(xS))))))))))))))))),inference(distribute,[status(thm)],[c24])).
% 206.00/206.24 cnf(c45,negated_conjecture,~aInteger0(X314)|X314=sz00|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X314),stldt0(sbsmnsldt0(xS))),inference(split_conjunct,[status(thm)],[c25])).
% 206.00/206.24 cnf(c96,plain,~aElementOf0(X380,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X380,skolem0008(X380)),stldt0(sbsmnsldt0(xS))),inference(split_conjunct,[status(thm)],[c52])).
% 206.00/206.24 cnf(c3381,plain,aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,skolem0008(sz10)),stldt0(sbsmnsldt0(xS))),inference(resolution,[status(thm)],[c3375, c96])).
% 206.00/206.24 cnf(c333698,plain,~aInteger0(skolem0008(sz10))|skolem0008(sz10)=sz00,inference(resolution,[status(thm)],[c3381, c45])).
% 206.00/206.24 cnf(c333700,plain,skolem0008(sz10)=sz00,inference(resolution,[status(thm)],[c333698, c3386])).
% 206.00/206.24 cnf(c333845,plain,$false,inference(resolution,[status(thm)],[c333700, c3377])).
% 206.00/206.24 % SZS output end CNFRefutation
% 206.00/206.24
% 206.00/206.24 % Initial clauses : 236
% 206.00/206.24 % Processed clauses : 3286
% 206.00/206.24 % Factors computed : 42
% 206.00/206.24 % Resolvents computed: 333466
% 206.00/206.24 % Tautologies deleted: 8
% 206.00/206.24 % Forward subsumed : 648
% 206.00/206.24 % Backward subsumed : 49
% 206.00/206.24 % -------- CPU Time ---------
% 206.00/206.24 % User time : 205.222 s
% 206.00/206.24 % System time : 0.643 s
% 206.00/206.24 % Total time : 205.865 s
%------------------------------------------------------------------------------