%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM533+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:36:06 EDT 2024
% Result : Theorem 0.69s 0.87s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUM533+1 : TPTP v8.1.2. Released v4.0.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n010.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 16:32:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.69/0.87 % Version: 1.5
% 0.69/0.87 % SZS status Theorem
% 0.69/0.87 % SZS output start CNFRefutation
% 0.69/0.87 fof(m__,conjecture,((aSubsetOf0(xA,xB)&aSubsetOf0(xB,xC))=>aSubsetOf0(xA,xC)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.69/0.87 fof(c6,negated_conjecture,(~((aSubsetOf0(xA,xB)&aSubsetOf0(xB,xC))=>aSubsetOf0(xA,xC))),inference(assume_negation,[status(cth)],[m__])).
% 0.69/0.87 fof(c7,negated_conjecture,((aSubsetOf0(xA,xB)&aSubsetOf0(xB,xC))&~aSubsetOf0(xA,xC)),inference(fof_nnf,[status(thm)],[c6])).
% 0.69/0.87 cnf(c10,negated_conjecture,~aSubsetOf0(xA,xC),inference(split_conjunct,[status(thm)],[c7])).
% 0.69/0.87 fof(m__522,plain,((aSet0(xA)&aSet0(xB))&aSet0(xC)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__522)).
% 0.69/0.87 cnf(c13,plain,aSet0(xC),inference(split_conjunct,[status(thm)],[m__522])).
% 0.69/0.87 cnf(c11,plain,aSet0(xA),inference(split_conjunct,[status(thm)],[m__522])).
% 0.69/0.87 fof(mDefSub,plain,(![W0]:(aSet0(W0)=>(![W1]:(aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]:(aElementOf0(W2,W1)=>aElementOf0(W2,W0)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefSub)).
% 0.69/0.87 fof(c24,plain,(![W0]:(~aSet0(W0)|(![W1]:((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]:(~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&((~aSet0(W1)|(?[W2]:(aElementOf0(W2,W1)&~aElementOf0(W2,W0))))|aSubsetOf0(W1,W0)))))),inference(fof_nnf,[status(thm)],[mDefSub])).
% 0.69/0.87 fof(c25,plain,(![W0]:(~aSet0(W0)|((![W1]:(~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]:(~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]:((~aSet0(W1)|(?[W2]:(aElementOf0(W2,W1)&~aElementOf0(W2,W0))))|aSubsetOf0(W1,W0)))))),inference(shift_quantors,[status(thm)],[c24])).
% 0.69/0.87 fof(c26,plain,(![X7]:(~aSet0(X7)|((![X8]:(~aSubsetOf0(X8,X7)|(aSet0(X8)&(![X9]:(~aElementOf0(X9,X8)|aElementOf0(X9,X7))))))&(![X10]:((~aSet0(X10)|(?[X11]:(aElementOf0(X11,X10)&~aElementOf0(X11,X7))))|aSubsetOf0(X10,X7)))))),inference(variable_rename,[status(thm)],[c25])).
% 0.69/0.87 fof(c28,plain,(![X7]:(![X8]:(![X9]:(![X10]:(~aSet0(X7)|((~aSubsetOf0(X8,X7)|(aSet0(X8)&(~aElementOf0(X9,X8)|aElementOf0(X9,X7))))&((~aSet0(X10)|(aElementOf0(skolem0001(X7,X10),X10)&~aElementOf0(skolem0001(X7,X10),X7)))|aSubsetOf0(X10,X7)))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,(![X7]:(~aSet0(X7)|((![X8]:(~aSubsetOf0(X8,X7)|(aSet0(X8)&(![X9]:(~aElementOf0(X9,X8)|aElementOf0(X9,X7))))))&(![X10]:((~aSet0(X10)|(aElementOf0(skolem0001(X7,X10),X10)&~aElementOf0(skolem0001(X7,X10),X7)))|aSubsetOf0(X10,X7)))))),inference(skolemize,[status(esa)],[c26])).])).
% 0.69/0.87 fof(c29,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~aSet0(X7)|(~aSubsetOf0(X8,X7)|aSet0(X8)))&(~aSet0(X7)|(~aSubsetOf0(X8,X7)|(~aElementOf0(X9,X8)|aElementOf0(X9,X7)))))&((~aSet0(X7)|((~aSet0(X10)|aElementOf0(skolem0001(X7,X10),X10))|aSubsetOf0(X10,X7)))&(~aSet0(X7)|((~aSet0(X10)|~aElementOf0(skolem0001(X7,X10),X7))|aSubsetOf0(X10,X7))))))))),inference(distribute,[status(thm)],[c28])).
% 0.69/0.87 cnf(c33,plain,~aSet0(X77)|~aSet0(X78)|~aElementOf0(skolem0001(X77,X78),X77)|aSubsetOf0(X78,X77),inference(split_conjunct,[status(thm)],[c29])).
% 0.69/0.87 cnf(c9,negated_conjecture,aSubsetOf0(xB,xC),inference(split_conjunct,[status(thm)],[c7])).
% 0.69/0.87 cnf(c31,plain,~aSet0(X65)|~aSubsetOf0(X67,X65)|~aElementOf0(X66,X67)|aElementOf0(X66,X65),inference(split_conjunct,[status(thm)],[c29])).
% 0.69/0.87 cnf(c12,plain,aSet0(xB),inference(split_conjunct,[status(thm)],[m__522])).
% 0.69/0.87 cnf(c8,negated_conjecture,aSubsetOf0(xA,xB),inference(split_conjunct,[status(thm)],[c7])).
% 0.69/0.87 cnf(c32,plain,~aSet0(X71)|~aSet0(X72)|aElementOf0(skolem0001(X71,X72),X72)|aSubsetOf0(X72,X71),inference(split_conjunct,[status(thm)],[c29])).
% 0.69/0.87 cnf(c110,plain,~aSet0(X97)|aElementOf0(skolem0001(X97,xA),xA)|aSubsetOf0(xA,X97),inference(resolution,[status(thm)],[c32, c11])).
% 0.69/0.87 cnf(c281,plain,aElementOf0(skolem0001(xC,xA),xA)|aSubsetOf0(xA,xC),inference(resolution,[status(thm)],[c110, c13])).
% 0.69/0.87 cnf(c633,plain,aElementOf0(skolem0001(xC,xA),xA),inference(resolution,[status(thm)],[c281, c10])).
% 0.69/0.87 cnf(c637,plain,~aSet0(X204)|~aSubsetOf0(xA,X204)|aElementOf0(skolem0001(xC,xA),X204),inference(resolution,[status(thm)],[c633, c31])).
% 0.69/0.87 cnf(c785,plain,~aSet0(xB)|aElementOf0(skolem0001(xC,xA),xB),inference(resolution,[status(thm)],[c637, c8])).
% 0.69/0.87 cnf(c788,plain,aElementOf0(skolem0001(xC,xA),xB),inference(resolution,[status(thm)],[c785, c12])).
% 0.69/0.87 cnf(c792,plain,~aSet0(X207)|~aSubsetOf0(xB,X207)|aElementOf0(skolem0001(xC,xA),X207),inference(resolution,[status(thm)],[c788, c31])).
% 0.69/0.87 cnf(c793,plain,~aSet0(xC)|aElementOf0(skolem0001(xC,xA),xC),inference(resolution,[status(thm)],[c792, c9])).
% 0.69/0.87 cnf(c797,plain,aElementOf0(skolem0001(xC,xA),xC),inference(resolution,[status(thm)],[c793, c13])).
% 0.69/0.87 cnf(c801,plain,~aSet0(xC)|~aSet0(xA)|aSubsetOf0(xA,xC),inference(resolution,[status(thm)],[c797, c33])).
% 0.69/0.87 cnf(c803,plain,~aSet0(xC)|aSubsetOf0(xA,xC),inference(resolution,[status(thm)],[c801, c11])).
% 0.69/0.87 cnf(c804,plain,aSubsetOf0(xA,xC),inference(resolution,[status(thm)],[c803, c13])).
% 0.69/0.87 cnf(c811,plain,$false,inference(resolution,[status(thm)],[c804, c10])).
% 0.69/0.87 % SZS output end CNFRefutation
% 0.69/0.87
% 0.69/0.87 % Initial clauses : 33
% 0.69/0.87 % Processed clauses : 254
% 0.69/0.87 % Factors computed : 7
% 0.69/0.87 % Resolvents computed: 742
% 0.69/0.87 % Tautologies deleted: 17
% 0.69/0.87 % Forward subsumed : 245
% 0.69/0.87 % Backward subsumed : 142
% 0.69/0.87 % -------- CPU Time ---------
% 0.69/0.87 % User time : 0.502 s
% 0.69/0.87 % System time : 0.022 s
% 0.69/0.87 % Total time : 0.524 s
%------------------------------------------------------------------------------