%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM550+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:09 EDT 2024
% Result : Theorem 1.24s 1.44s
% Output : Refutation 1.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : NUM550+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n016.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 16:06:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.24/1.44 % Version: 1.5
% 1.24/1.44 % SZS status Theorem
% 1.24/1.44 % SZS output start CNFRefutation
% 1.24/1.44 fof(m__2202_02,plain,((aSet0(xS)&aSet0(xT))&xk!=sz00),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__2202_02)).
% 1.24/1.44 cnf(c28,plain,xk!=sz00,inference(split_conjunct,[status(thm)],[m__2202_02])).
% 1.24/1.44 cnf(symmetry,axiom,X121!=X122|X122=X121,theory(equality)).
% 1.24/1.44 cnf(transitivity,axiom,X124!=X125|X125!=X126|X124=X126,theory(equality)).
% 1.24/1.44 fof(m__,conjecture,xQ!=slcrc0,file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 1.24/1.44 fof(c16,negated_conjecture,(~xQ!=slcrc0),inference(assume_negation,[status(cth)],[m__])).
% 1.24/1.44 fof(c17,negated_conjecture,xQ=slcrc0,inference(fof_simplification,[status(thm)],[c16])).
% 1.24/1.44 cnf(c18,negated_conjecture,xQ=slcrc0,inference(split_conjunct,[status(thm)],[c17])).
% 1.24/1.44 cnf(c309,plain,slcrc0=xQ,inference(resolution,[status(thm)],[c18, symmetry])).
% 1.24/1.44 cnf(c3,axiom,X140!=X141|sbrdtbr0(X140)=sbrdtbr0(X141),theory(equality)).
% 1.24/1.44 cnf(c352,plain,sbrdtbr0(slcrc0)=sbrdtbr0(xQ),inference(resolution,[status(thm)],[c3, c309])).
% 1.24/1.44 fof(m__2291,plain,((aSet0(xQ)&isFinite0(xQ))&sbrdtbr0(xQ)=xk),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__2291)).
% 1.24/1.44 cnf(c21,plain,sbrdtbr0(xQ)=xk,inference(split_conjunct,[status(thm)],[m__2291])).
% 1.24/1.44 cnf(c328,plain,X264!=sbrdtbr0(xQ)|X264=xk,inference(resolution,[status(thm)],[c21, transitivity])).
% 1.24/1.44 cnf(c865,plain,sbrdtbr0(slcrc0)=xk,inference(resolution,[status(thm)],[c328, c352])).
% 1.24/1.44 cnf(c874,plain,X328!=sbrdtbr0(slcrc0)|X328=xk,inference(resolution,[status(thm)],[c865, transitivity])).
% 1.24/1.44 cnf(reflexivity,axiom,X120=X120,theory(equality)).
% 1.24/1.44 fof(mDefEmp,plain,(![W0]:(W0=slcrc0<=>(aSet0(W0)&(~(?[W1]:aElementOf0(W1,W0)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefEmp)).
% 1.24/1.44 fof(c289,plain,(![W0]:((W0!=slcrc0|(aSet0(W0)&(![W1]:~aElementOf0(W1,W0))))&((~aSet0(W0)|(?[W1]:aElementOf0(W1,W0)))|W0=slcrc0))),inference(fof_nnf,[status(thm)],[mDefEmp])).
% 1.24/1.44 fof(c290,plain,((![W0]:(W0!=slcrc0|(aSet0(W0)&(![W1]:~aElementOf0(W1,W0)))))&(![W0]:((~aSet0(W0)|(?[W1]:aElementOf0(W1,W0)))|W0=slcrc0))),inference(shift_quantors,[status(thm)],[c289])).
% 1.24/1.44 fof(c291,plain,((![X114]:(X114!=slcrc0|(aSet0(X114)&(![X115]:~aElementOf0(X115,X114)))))&(![X116]:((~aSet0(X116)|(?[X117]:aElementOf0(X117,X116)))|X116=slcrc0))),inference(variable_rename,[status(thm)],[c290])).
% 1.24/1.44 fof(c293,plain,(![X114]:(![X115]:(![X116]:((X114!=slcrc0|(aSet0(X114)&~aElementOf0(X115,X114)))&((~aSet0(X116)|aElementOf0(skolem0011(X116),X116))|X116=slcrc0))))),inference(shift_quantors,[status(thm)],[fof(c292,plain,((![X114]:(X114!=slcrc0|(aSet0(X114)&(![X115]:~aElementOf0(X115,X114)))))&(![X116]:((~aSet0(X116)|aElementOf0(skolem0011(X116),X116))|X116=slcrc0))),inference(skolemize,[status(esa)],[c291])).])).
% 1.24/1.44 fof(c294,plain,(![X114]:(![X115]:(![X116]:(((X114!=slcrc0|aSet0(X114))&(X114!=slcrc0|~aElementOf0(X115,X114)))&((~aSet0(X116)|aElementOf0(skolem0011(X116),X116))|X116=slcrc0))))),inference(distribute,[status(thm)],[c293])).
% 1.24/1.44 cnf(c295,plain,X139!=slcrc0|aSet0(X139),inference(split_conjunct,[status(thm)],[c294])).
% 1.24/1.44 cnf(c345,plain,aSet0(slcrc0),inference(resolution,[status(thm)],[c295, reflexivity])).
% 1.24/1.44 fof(mCardEmpty,axiom,(![W0]:(aSet0(W0)=>(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mCardEmpty)).
% 1.24/1.44 fof(c135,plain,(![W0]:(~aSet0(W0)|((sbrdtbr0(W0)!=sz00|W0=slcrc0)&(W0!=slcrc0|sbrdtbr0(W0)=sz00)))),inference(fof_nnf,[status(thm)],[mCardEmpty])).
% 1.24/1.44 fof(c136,plain,(![X50]:(~aSet0(X50)|((sbrdtbr0(X50)!=sz00|X50=slcrc0)&(X50!=slcrc0|sbrdtbr0(X50)=sz00)))),inference(variable_rename,[status(thm)],[c135])).
% 1.24/1.44 fof(c137,plain,(![X50]:((~aSet0(X50)|(sbrdtbr0(X50)!=sz00|X50=slcrc0))&(~aSet0(X50)|(X50!=slcrc0|sbrdtbr0(X50)=sz00)))),inference(distribute,[status(thm)],[c136])).
% 1.24/1.44 cnf(c139,plain,~aSet0(X305)|X305!=slcrc0|sbrdtbr0(X305)=sz00,inference(split_conjunct,[status(thm)],[c137])).
% 1.24/1.44 cnf(c1509,plain,~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00,inference(resolution,[status(thm)],[c139, reflexivity])).
% 1.24/1.44 cnf(c1909,plain,sbrdtbr0(slcrc0)=sz00,inference(resolution,[status(thm)],[c1509, c345])).
% 1.24/1.44 cnf(c1920,plain,sz00=sbrdtbr0(slcrc0),inference(resolution,[status(thm)],[c1909, symmetry])).
% 1.24/1.44 cnf(c1931,plain,sz00=xk,inference(resolution,[status(thm)],[c1920, c874])).
% 1.24/1.44 cnf(c1953,plain,xk=sz00,inference(resolution,[status(thm)],[c1931, symmetry])).
% 1.24/1.44 cnf(c1960,plain,$false,inference(resolution,[status(thm)],[c1953, c28])).
% 1.24/1.44 % SZS output end CNFRefutation
% 1.24/1.44
% 1.24/1.44 % Initial clauses : 141
% 1.24/1.44 % Processed clauses : 357
% 1.24/1.44 % Factors computed : 11
% 1.24/1.44 % Resolvents computed: 1656
% 1.24/1.44 % Tautologies deleted: 13
% 1.24/1.44 % Forward subsumed : 134
% 1.24/1.44 % Backward subsumed : 8
% 1.24/1.44 % -------- CPU Time ---------
% 1.24/1.44 % User time : 1.055 s
% 1.24/1.44 % System time : 0.018 s
% 1.24/1.44 % Total time : 1.073 s
%------------------------------------------------------------------------------