%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM017+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:17:44 EDT 2024
% Result : Theorem 91.20s 91.45s
% Output : Refutation 91.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.13 % Problem : COM017+1 : TPTP v8.1.2. Released v4.0.0.
% 0.09/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n022.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 07:09:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 91.20/91.45 % Version: 1.5
% 91.20/91.45 % SZS status Theorem
% 91.20/91.45 % SZS output start CNFRefutation
% 91.20/91.45 fof(m__656,plain,aRewritingSystem0(xR),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__656)).
% 91.20/91.45 cnf(c34,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__656])).
% 91.20/91.45 fof(m__656_01,plain,(isLocallyConfluent0(xR)&isTerminating0(xR)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__656_01)).
% 91.20/91.45 cnf(c32,plain,isLocallyConfluent0(xR),inference(split_conjunct,[status(thm)],[m__656_01])).
% 91.20/91.45 fof(m__731,plain,((aElement0(xa)&aElement0(xb))&aElement0(xc)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__731)).
% 91.20/91.45 cnf(c29,plain,aElement0(xa),inference(split_conjunct,[status(thm)],[m__731])).
% 91.20/91.45 fof(m__779,plain,((aElement0(xv)&aReductOfIn0(xv,xa,xR))&sdtmndtasgtdt0(xv,xR,xc)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__779)).
% 91.20/91.45 cnf(c14,plain,aElement0(xv),inference(split_conjunct,[status(thm)],[m__779])).
% 91.20/91.45 fof(m__755,plain,((aElement0(xu)&aReductOfIn0(xu,xa,xR))&sdtmndtasgtdt0(xu,xR,xb)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__755)).
% 91.20/91.45 cnf(c17,plain,aElement0(xu),inference(split_conjunct,[status(thm)],[m__755])).
% 91.20/91.45 cnf(c15,plain,aReductOfIn0(xv,xa,xR),inference(split_conjunct,[status(thm)],[m__779])).
% 91.20/91.45 cnf(c18,plain,aReductOfIn0(xu,xa,xR),inference(split_conjunct,[status(thm)],[m__755])).
% 91.20/91.45 fof(mWCRDef,plain,(![W0]:(aRewritingSystem0(W0)=>(isLocallyConfluent0(W0)<=>(![W1]:(![W2]:(![W3]:(((((aElement0(W1)&aElement0(W2))&aElement0(W3))&aReductOfIn0(W2,W1,W0))&aReductOfIn0(W3,W1,W0))=>(?[W4]:((aElement0(W4)&sdtmndtasgtdt0(W2,W0,W4))&sdtmndtasgtdt0(W3,W0,W4)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mWCRDef)).
% 91.20/91.45 fof(c60,plain,(![W0]:(~aRewritingSystem0(W0)|((~isLocallyConfluent0(W0)|(![W1]:(![W2]:(![W3]:(((((~aElement0(W1)|~aElement0(W2))|~aElement0(W3))|~aReductOfIn0(W2,W1,W0))|~aReductOfIn0(W3,W1,W0))|(?[W4]:((aElement0(W4)&sdtmndtasgtdt0(W2,W0,W4))&sdtmndtasgtdt0(W3,W0,W4))))))))&((?[W1]:(?[W2]:(?[W3]:(((((aElement0(W1)&aElement0(W2))&aElement0(W3))&aReductOfIn0(W2,W1,W0))&aReductOfIn0(W3,W1,W0))&(![W4]:((~aElement0(W4)|~sdtmndtasgtdt0(W2,W0,W4))|~sdtmndtasgtdt0(W3,W0,W4)))))))|isLocallyConfluent0(W0))))),inference(fof_nnf,[status(thm)],[mWCRDef])).
% 91.20/91.45 fof(c61,plain,(![X21]:(~aRewritingSystem0(X21)|((~isLocallyConfluent0(X21)|(![X22]:(![X23]:(![X24]:(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|(?[X25]:((aElement0(X25)&sdtmndtasgtdt0(X23,X21,X25))&sdtmndtasgtdt0(X24,X21,X25))))))))&((?[X26]:(?[X27]:(?[X28]:(((((aElement0(X26)&aElement0(X27))&aElement0(X28))&aReductOfIn0(X27,X26,X21))&aReductOfIn0(X28,X26,X21))&(![X29]:((~aElement0(X29)|~sdtmndtasgtdt0(X27,X21,X29))|~sdtmndtasgtdt0(X28,X21,X29)))))))|isLocallyConfluent0(X21))))),inference(variable_rename,[status(thm)],[c60])).
% 91.20/91.45 fof(c63,plain,(![X21]:(![X22]:(![X23]:(![X24]:(![X29]:(~aRewritingSystem0(X21)|((~isLocallyConfluent0(X21)|(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|((aElement0(skolem0006(X21,X22,X23,X24))&sdtmndtasgtdt0(X23,X21,skolem0006(X21,X22,X23,X24)))&sdtmndtasgtdt0(X24,X21,skolem0006(X21,X22,X23,X24)))))&((((((aElement0(skolem0007(X21))&aElement0(skolem0008(X21)))&aElement0(skolem0009(X21)))&aReductOfIn0(skolem0008(X21),skolem0007(X21),X21))&aReductOfIn0(skolem0009(X21),skolem0007(X21),X21))&((~aElement0(X29)|~sdtmndtasgtdt0(skolem0008(X21),X21,X29))|~sdtmndtasgtdt0(skolem0009(X21),X21,X29)))|isLocallyConfluent0(X21))))))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,(![X21]:(~aRewritingSystem0(X21)|((~isLocallyConfluent0(X21)|(![X22]:(![X23]:(![X24]:(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|((aElement0(skolem0006(X21,X22,X23,X24))&sdtmndtasgtdt0(X23,X21,skolem0006(X21,X22,X23,X24)))&sdtmndtasgtdt0(X24,X21,skolem0006(X21,X22,X23,X24))))))))&((((((aElement0(skolem0007(X21))&aElement0(skolem0008(X21)))&aElement0(skolem0009(X21)))&aReductOfIn0(skolem0008(X21),skolem0007(X21),X21))&aReductOfIn0(skolem0009(X21),skolem0007(X21),X21))&(![X29]:((~aElement0(X29)|~sdtmndtasgtdt0(skolem0008(X21),X21,X29))|~sdtmndtasgtdt0(skolem0009(X21),X21,X29))))|isLocallyConfluent0(X21))))),inference(skolemize,[status(esa)],[c61])).])).
% 91.20/91.45 fof(c64,plain,(![X21]:(![X22]:(![X23]:(![X24]:(![X29]:((((~aRewritingSystem0(X21)|(~isLocallyConfluent0(X21)|(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|aElement0(skolem0006(X21,X22,X23,X24)))))&(~aRewritingSystem0(X21)|(~isLocallyConfluent0(X21)|(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|sdtmndtasgtdt0(X23,X21,skolem0006(X21,X22,X23,X24))))))&(~aRewritingSystem0(X21)|(~isLocallyConfluent0(X21)|(((((~aElement0(X22)|~aElement0(X23))|~aElement0(X24))|~aReductOfIn0(X23,X22,X21))|~aReductOfIn0(X24,X22,X21))|sdtmndtasgtdt0(X24,X21,skolem0006(X21,X22,X23,X24))))))&((((((~aRewritingSystem0(X21)|(aElement0(skolem0007(X21))|isLocallyConfluent0(X21)))&(~aRewritingSystem0(X21)|(aElement0(skolem0008(X21))|isLocallyConfluent0(X21))))&(~aRewritingSystem0(X21)|(aElement0(skolem0009(X21))|isLocallyConfluent0(X21))))&(~aRewritingSystem0(X21)|(aReductOfIn0(skolem0008(X21),skolem0007(X21),X21)|isLocallyConfluent0(X21))))&(~aRewritingSystem0(X21)|(aReductOfIn0(skolem0009(X21),skolem0007(X21),X21)|isLocallyConfluent0(X21))))&(~aRewritingSystem0(X21)|(((~aElement0(X29)|~sdtmndtasgtdt0(skolem0008(X21),X21,X29))|~sdtmndtasgtdt0(skolem0009(X21),X21,X29))|isLocallyConfluent0(X21)))))))))),inference(distribute,[status(thm)],[c63])).
% 91.20/91.45 cnf(c65,plain,~aRewritingSystem0(X163)|~isLocallyConfluent0(X163)|~aElement0(X166)|~aElement0(X165)|~aElement0(X164)|~aReductOfIn0(X165,X166,X163)|~aReductOfIn0(X164,X166,X163)|aElement0(skolem0006(X163,X166,X165,X164)),inference(split_conjunct,[status(thm)],[c64])).
% 91.20/91.45 cnf(c207,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X411)|~aElement0(xu)|~aReductOfIn0(X411,xa,xR)|aElement0(skolem0006(xR,xa,X411,xu)),inference(resolution,[status(thm)],[c65, c18])).
% 91.20/91.45 cnf(c806,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|~aElement0(xu)|aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c207, c15])).
% 91.20/91.45 cnf(c9439,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c806, c17])).
% 91.20/91.45 cnf(c10053,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c9439, c14])).
% 91.20/91.45 cnf(c10054,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c10053, c29])).
% 91.20/91.45 cnf(c10056,plain,~aRewritingSystem0(xR)|aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c10054, c32])).
% 91.20/91.45 cnf(c10057,plain,aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c10056, c34])).
% 91.20/91.45 fof(m__,conjecture,(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xu,xR,W0))&sdtmndtasgtdt0(xv,xR,W0))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 91.20/91.45 fof(c10,negated_conjecture,(~(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xu,xR,W0))&sdtmndtasgtdt0(xv,xR,W0)))),inference(assume_negation,[status(cth)],[m__])).
% 91.20/91.45 fof(c11,negated_conjecture,(![W0]:((~aElement0(W0)|~sdtmndtasgtdt0(xu,xR,W0))|~sdtmndtasgtdt0(xv,xR,W0))),inference(fof_nnf,[status(thm)],[c10])).
% 91.20/91.45 fof(c12,negated_conjecture,(![X2]:((~aElement0(X2)|~sdtmndtasgtdt0(xu,xR,X2))|~sdtmndtasgtdt0(xv,xR,X2))),inference(variable_rename,[status(thm)],[c11])).
% 91.20/91.45 cnf(c13,negated_conjecture,~aElement0(X126)|~sdtmndtasgtdt0(xu,xR,X126)|~sdtmndtasgtdt0(xv,xR,X126),inference(split_conjunct,[status(thm)],[c12])).
% 91.20/91.45 cnf(c66,plain,~aRewritingSystem0(X167)|~isLocallyConfluent0(X167)|~aElement0(X170)|~aElement0(X169)|~aElement0(X168)|~aReductOfIn0(X169,X170,X167)|~aReductOfIn0(X168,X170,X167)|sdtmndtasgtdt0(X169,X167,skolem0006(X167,X170,X169,X168)),inference(split_conjunct,[status(thm)],[c64])).
% 91.20/91.45 cnf(c217,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X439)|~aElement0(xu)|~aReductOfIn0(X439,xa,xR)|sdtmndtasgtdt0(X439,xR,skolem0006(xR,xa,X439,xu)),inference(resolution,[status(thm)],[c66, c18])).
% 91.20/91.45 cnf(c843,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|~aElement0(xu)|sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c217, c15])).
% 91.20/91.45 cnf(c9910,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c843, c17])).
% 91.20/91.45 cnf(c47645,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c9910, c14])).
% 91.20/91.45 cnf(c47646,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47645, c29])).
% 91.20/91.45 cnf(c47647,plain,~aRewritingSystem0(xR)|sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47646, c32])).
% 91.20/91.45 cnf(c47649,plain,sdtmndtasgtdt0(xv,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47647, c34])).
% 91.20/91.45 cnf(c47674,plain,~aElement0(skolem0006(xR,xa,xv,xu))|~sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47649, c13])).
% 91.20/91.45 cnf(c67,plain,~aRewritingSystem0(X171)|~isLocallyConfluent0(X171)|~aElement0(X174)|~aElement0(X173)|~aElement0(X172)|~aReductOfIn0(X173,X174,X171)|~aReductOfIn0(X172,X174,X171)|sdtmndtasgtdt0(X172,X171,skolem0006(X171,X174,X173,X172)),inference(split_conjunct,[status(thm)],[c64])).
% 91.20/91.45 cnf(c225,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X459)|~aElement0(xu)|~aReductOfIn0(X459,xa,xR)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,X459,xu)),inference(resolution,[status(thm)],[c67, c18])).
% 91.20/91.45 cnf(c860,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|~aElement0(xu)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c225, c15])).
% 91.20/91.45 cnf(c10055,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(xv)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c860, c17])).
% 91.20/91.45 cnf(c47899,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c10055, c14])).
% 91.20/91.45 cnf(c47900,plain,~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47899, c29])).
% 91.20/91.45 cnf(c47901,plain,~aRewritingSystem0(xR)|sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47900, c32])).
% 91.20/91.45 cnf(c47903,plain,sdtmndtasgtdt0(xu,xR,skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47901, c34])).
% 91.20/91.45 cnf(c47928,plain,~aElement0(skolem0006(xR,xa,xv,xu)),inference(resolution,[status(thm)],[c47903, c47674])).
% 91.20/91.45 cnf(c47937,plain,$false,inference(resolution,[status(thm)],[c47928, c10057])).
% 91.20/91.45 % SZS output end CNFRefutation
% 91.20/91.45
% 91.20/91.45 % Initial clauses : 74
% 91.20/91.45 % Processed clauses : 4884
% 91.20/91.45 % Factors computed : 97
% 91.20/91.45 % Resolvents computed: 47719
% 91.20/91.45 % Tautologies deleted: 147
% 91.20/91.45 % Forward subsumed : 1722
% 91.20/91.45 % Backward subsumed : 1482
% 91.20/91.45 % -------- CPU Time ---------
% 91.20/91.45 % User time : 90.838 s
% 91.20/91.45 % System time : 0.223 s
% 91.20/91.45 % Total time : 91.061 s
%------------------------------------------------------------------------------