%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS019+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:28:29 EDT 2024
% Result : Satisfiable 0.38s 0.55s
% Output : Saturation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : KRS019+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 00:15:08 EDT 2024
% 0.14/0.37 % CPUTime :
% 0.38/0.55 % Version: 1.5
% 0.38/0.55 % SZS status Satisfiable
% 0.38/0.55 % SZS output start Saturation
% 0.38/0.55 fof(axiom_2,axiom,(![X]:(cA(X)<=>(?[Y]:(rq(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.38/0.55 fof(c17,plain,(![X]:((~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y))))&((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.38/0.55 fof(c18,plain,((![X]:(~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(shift_quantors,[status(thm)],[c17])).
% 0.38/0.55 fof(c19,plain,((![X10]:(~cA(X10)|(?[X11]:(rq(X10,X11)&cowlThing(X11)))))&(![X12]:((![X13]:(~rq(X12,X13)|~cowlThing(X13)))|cA(X12)))),inference(variable_rename,[status(thm)],[c18])).
% 0.38/0.55 fof(c21,plain,(![X10]:(![X12]:(![X13]:((~cA(X10)|(rq(X10,skolem0003(X10))&cowlThing(skolem0003(X10))))&((~rq(X12,X13)|~cowlThing(X13))|cA(X12)))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X10]:(~cA(X10)|(rq(X10,skolem0003(X10))&cowlThing(skolem0003(X10)))))&(![X12]:((![X13]:(~rq(X12,X13)|~cowlThing(X13)))|cA(X12)))),inference(skolemize,[status(esa)],[c19])).])).
% 0.38/0.55 fof(c22,plain,(![X10]:(![X12]:(![X13]:(((~cA(X10)|rq(X10,skolem0003(X10)))&(~cA(X10)|cowlThing(skolem0003(X10))))&((~rq(X12,X13)|~cowlThing(X13))|cA(X12)))))),inference(distribute,[status(thm)],[c21])).
% 0.38/0.55 cnf(c23,plain,~cA(X31)|rq(X31,skolem0003(X31)),inference(split_conjunct,[status(thm)],[c22])).
% 0.38/0.55 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.38/0.55 fof(c33,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.38/0.55 fof(c34,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c33])).
% 0.38/0.55 fof(c36,plain,(![X16]:(![X17]:(cowlThing(X16)&~cowlNothing(X17)))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((![X16]:cowlThing(X16))&(![X17]:~cowlNothing(X17))),inference(variable_rename,[status(thm)],[c34])).])).
% 0.38/0.55 cnf(c37,plain,cowlThing(X18),inference(split_conjunct,[status(thm)],[c36])).
% 0.38/0.55 fof(axiom_5,axiom,(![X]:(cnotA(X)<=>(![Y]:(rq(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.38/0.55 fof(c0,plain,(![X]:((~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y))))&((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.38/0.55 fof(c1,plain,((![X]:(~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(shift_quantors,[status(thm)],[c0])).
% 0.38/0.55 fof(c2,plain,((![X2]:(~cnotA(X2)|(![X3]:(~rq(X2,X3)|cNothing(X3)))))&(![X4]:((?[X5]:(rq(X4,X5)&~cNothing(X5)))|cnotA(X4)))),inference(variable_rename,[status(thm)],[c1])).
% 0.38/0.55 fof(c4,plain,(![X2]:(![X3]:(![X4]:((~cnotA(X2)|(~rq(X2,X3)|cNothing(X3)))&((rq(X4,skolem0001(X4))&~cNothing(skolem0001(X4)))|cnotA(X4)))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~cnotA(X2)|(![X3]:(~rq(X2,X3)|cNothing(X3)))))&(![X4]:((rq(X4,skolem0001(X4))&~cNothing(skolem0001(X4)))|cnotA(X4)))),inference(skolemize,[status(esa)],[c2])).])).
% 0.38/0.55 fof(c5,plain,(![X2]:(![X3]:(![X4]:((~cnotA(X2)|(~rq(X2,X3)|cNothing(X3)))&((rq(X4,skolem0001(X4))|cnotA(X4))&(~cNothing(skolem0001(X4))|cnotA(X4))))))),inference(distribute,[status(thm)],[c4])).
% 0.38/0.55 cnf(c7,plain,rq(X29,skolem0001(X29))|cnotA(X29),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.55 cnf(c25,plain,~rq(X33,X32)|~cowlThing(X32)|cA(X33),inference(split_conjunct,[status(thm)],[c22])).
% 0.38/0.55 cnf(c41,plain,~cowlThing(skolem0001(X35))|cA(X35)|cnotA(X35),inference(resolution,[status(thm)],[c25, c7])).
% 0.38/0.55 cnf(c42,plain,cA(X36)|cnotA(X36),inference(resolution,[status(thm)],[c41, c37])).
% 0.38/0.55 cnf(c43,plain,cnotA(X37)|rq(X37,skolem0003(X37)),inference(resolution,[status(thm)],[c42, c23])).
% 0.38/0.55 fof(axiom_4,axiom,(![X]:(cNothing(X)=>(?[Y0]:rp(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.38/0.55 fof(c9,plain,(![X]:(~cNothing(X)|(?[Y0]:rp(X,Y0)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.38/0.55 fof(c10,plain,(![X6]:(~cNothing(X6)|(?[X7]:rp(X6,X7)))),inference(variable_rename,[status(thm)],[c9])).
% 0.38/0.55 fof(c11,plain,(![X6]:(~cNothing(X6)|rp(X6,skolem0002(X6)))),inference(skolemize,[status(esa)],[c10])).
% 0.38/0.55 cnf(c12,plain,~cNothing(X30)|rp(X30,skolem0002(X30)),inference(split_conjunct,[status(thm)],[c11])).
% 0.38/0.55 cnf(c8,plain,~cNothing(skolem0001(X27))|cnotA(X27),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.55 fof(axiom_3,axiom,(![X]:(cNothing(X)=>(~(?[Y]:rp(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.38/0.55 fof(c13,plain,(![X]:(~cNothing(X)|(![Y]:~rp(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.38/0.55 fof(c15,plain,(![X8]:(![X9]:(~cNothing(X8)|~rp(X8,X9)))),inference(shift_quantors,[status(thm)],[fof(c14,plain,(![X8]:(~cNothing(X8)|(![X9]:~rp(X8,X9)))),inference(variable_rename,[status(thm)],[c13])).])).
% 0.38/0.55 cnf(c16,plain,~cNothing(X25)|~rp(X25,X26),inference(split_conjunct,[status(thm)],[c15])).
% 0.38/0.55 cnf(c6,plain,~cnotA(X23)|~rq(X23,X24)|cNothing(X24),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.55 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.38/0.55 fof(c26,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.38/0.55 fof(c27,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c26])).
% 0.38/0.55 fof(c28,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.38/0.55 fof(c30,plain,(![X14]:(![X15]:((~xsd_string(X14)|~xsd_integer(X14))&(xsd_integer(X15)|xsd_string(X15))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X14]:(~xsd_string(X14)|~xsd_integer(X14)))&(![X15]:(xsd_integer(X15)|xsd_string(X15)))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.38/0.55 cnf(c32,plain,xsd_integer(X21)|xsd_string(X21),inference(split_conjunct,[status(thm)],[c30])).
% 0.38/0.55 cnf(c31,plain,~xsd_string(X20)|~xsd_integer(X20),inference(split_conjunct,[status(thm)],[c30])).
% 0.38/0.55 cnf(c38,plain,~cowlNothing(X19),inference(split_conjunct,[status(thm)],[c36])).
% 0.38/0.55 % SZS output end Saturation
% 0.38/0.55
% 0.38/0.55 % Initial clauses : 12
% 0.38/0.55 % Processed clauses : 14
% 0.38/0.55 % Factors computed : 0
% 0.38/0.55 % Resolvents computed: 7
% 0.38/0.55 % Tautologies deleted: 3
% 0.38/0.55 % Forward subsumed : 2
% 0.38/0.55 % Backward subsumed : 1
% 0.38/0.55 % -------- CPU Time ---------
% 0.38/0.55 % User time : 0.169 s
% 0.38/0.55 % System time : 0.013 s
% 0.38/0.55 % Total time : 0.182 s
%------------------------------------------------------------------------------