%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS131+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:47 EDT 2024
% Result : Theorem 0.39s 0.55s
% Output : Refutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS131+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 00:10:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.39/0.55 % Version: 1.5
% 0.39/0.55 % SZS status Theorem
% 0.39/0.55 % SZS output start CNFRefutation
% 0.39/0.55 fof(axiom_5,axiom,(![X]:(cnotA(X)<=>(![Y]:(rq(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.39/0.55 fof(c11,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.39/0.55 fof(c12,plain,((![X]:(~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.39/0.55 fof(c13,plain,((![X6]:(~cnotA(X6)|(![X7]:(~rq(X6,X7)|cNothing(X7)))))&(![X8]:((?[X9]:(rq(X8,X9)&~cNothing(X9)))|cnotA(X8)))),inference(variable_rename,[status(thm)],[c12])).
% 0.39/0.55 fof(c15,plain,(![X6]:(![X7]:(![X8]:((~cnotA(X6)|(~rq(X6,X7)|cNothing(X7)))&((rq(X8,skolem0005(X8))&~cNothing(skolem0005(X8)))|cnotA(X8)))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X6]:(~cnotA(X6)|(![X7]:(~rq(X6,X7)|cNothing(X7)))))&(![X8]:((rq(X8,skolem0005(X8))&~cNothing(skolem0005(X8)))|cnotA(X8)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.39/0.55 fof(c16,plain,(![X6]:(![X7]:(![X8]:((~cnotA(X6)|(~rq(X6,X7)|cNothing(X7)))&((rq(X8,skolem0005(X8))|cnotA(X8))&(~cNothing(skolem0005(X8))|cnotA(X8))))))),inference(distribute,[status(thm)],[c15])).
% 0.39/0.55 cnf(c17,plain,~cnotA(X34)|~rq(X34,X35)|cNothing(X35),inference(split_conjunct,[status(thm)],[c16])).
% 0.39/0.55 fof(axiom_2,axiom,(![X]:(cA(X)<=>(?[Y]:(rq(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.39/0.55 fof(c28,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.39/0.55 fof(c29,plain,((![X]:(~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 0.39/0.55 fof(c30,plain,((![X14]:(~cA(X14)|(?[X15]:(rq(X14,X15)&cowlThing(X15)))))&(![X16]:((![X17]:(~rq(X16,X17)|~cowlThing(X17)))|cA(X16)))),inference(variable_rename,[status(thm)],[c29])).
% 0.39/0.55 fof(c32,plain,(![X14]:(![X16]:(![X17]:((~cA(X14)|(rq(X14,skolem0007(X14))&cowlThing(skolem0007(X14))))&((~rq(X16,X17)|~cowlThing(X17))|cA(X16)))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,((![X14]:(~cA(X14)|(rq(X14,skolem0007(X14))&cowlThing(skolem0007(X14)))))&(![X16]:((![X17]:(~rq(X16,X17)|~cowlThing(X17)))|cA(X16)))),inference(skolemize,[status(esa)],[c30])).])).
% 0.39/0.55 fof(c33,plain,(![X14]:(![X16]:(![X17]:(((~cA(X14)|rq(X14,skolem0007(X14)))&(~cA(X14)|cowlThing(skolem0007(X14))))&((~rq(X16,X17)|~cowlThing(X17))|cA(X16)))))),inference(distribute,[status(thm)],[c32])).
% 0.39/0.55 cnf(c34,plain,~cA(X33)|rq(X33,skolem0007(X33)),inference(split_conjunct,[status(thm)],[c33])).
% 0.39/0.55 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.39/0.55 fof(c44,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.39/0.55 fof(c45,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c44])).
% 0.39/0.55 fof(c47,plain,(![X20]:(![X21]:(cowlThing(X20)&~cowlNothing(X21)))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X20]:cowlThing(X20))&(![X21]:~cowlNothing(X21))),inference(variable_rename,[status(thm)],[c45])).])).
% 0.39/0.55 cnf(c49,plain,~cowlNothing(X23),inference(split_conjunct,[status(thm)],[c47])).
% 0.39/0.55 cnf(c48,plain,cowlThing(X22),inference(split_conjunct,[status(thm)],[c47])).
% 0.39/0.55 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.39/0.55 fof(c37,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.39/0.55 fof(c38,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c37])).
% 0.39/0.55 fof(c39,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c38])).
% 0.39/0.55 fof(c41,plain,(![X18]:(![X19]:((~xsd_string(X18)|~xsd_integer(X18))&(xsd_integer(X19)|xsd_string(X19))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,((![X18]:(~xsd_string(X18)|~xsd_integer(X18)))&(![X19]:(xsd_integer(X19)|xsd_string(X19)))),inference(variable_rename,[status(thm)],[c39])).])).
% 0.39/0.55 cnf(c43,plain,xsd_integer(X25)|xsd_string(X25),inference(split_conjunct,[status(thm)],[c41])).
% 0.39/0.55 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cnotA(X)<=>(~cA(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 0.39/0.55 fof(c0,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cnotA(X)<=>(~cA(X)))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 0.39/0.55 fof(c1,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cnotA(X)<=>~cA(X))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.39/0.55 fof(c2,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cnotA(X)|cA(X))&(cnotA(X)|~cA(X))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.39/0.55 fof(c3,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cnotA(X)|cA(X))&(cnotA(X)|~cA(X))))),inference(shift_quantors,[status(thm)],[c2])).
% 0.39/0.55 fof(c4,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:((~cnotA(X5)|cA(X5))&(cnotA(X5)|~cA(X5))))),inference(variable_rename,[status(thm)],[c3])).
% 0.39/0.55 fof(c5,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~cnotA(skolem0004)|cA(skolem0004))&(cnotA(skolem0004)|~cA(skolem0004)))),inference(skolemize,[status(esa)],[c4])).
% 0.39/0.55 fof(c6,negated_conjecture,(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cnotA(skolem0004)|cA(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(cnotA(skolem0004)|~cA(skolem0004))))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cnotA(skolem0004)|cA(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(cnotA(skolem0004)|~cA(skolem0004))))),inference(distribute,[status(thm)],[c5])).
% 0.39/0.55 cnf(c9,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cnotA(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.55 cnf(c18,plain,rq(X31,skolem0005(X31))|cnotA(X31),inference(split_conjunct,[status(thm)],[c16])).
% 0.39/0.55 cnf(c36,plain,~rq(X36,X37)|~cowlThing(X37)|cA(X36),inference(split_conjunct,[status(thm)],[c33])).
% 0.39/0.55 cnf(c53,plain,~cowlThing(skolem0005(X39))|cA(X39)|cnotA(X39),inference(resolution,[status(thm)],[c36, c18])).
% 0.39/0.55 cnf(c54,plain,cA(X40)|cnotA(X40),inference(resolution,[status(thm)],[c53, c48])).
% 0.39/0.55 cnf(c58,plain,cA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c54, c9])).
% 0.39/0.55 cnf(c76,plain,cA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c58, c43])).
% 0.39/0.55 cnf(c78,plain,cA(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c76, c48])).
% 0.39/0.55 cnf(c81,plain,cA(skolem0004)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c78, c49])).
% 0.39/0.55 cnf(c42,plain,~xsd_string(X24)|~xsd_integer(X24),inference(split_conjunct,[status(thm)],[c41])).
% 0.39/0.55 cnf(c7,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cnotA(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.55 cnf(c59,plain,cA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c54, c7])).
% 0.39/0.55 cnf(c96,plain,cA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c59, c81])).
% 0.39/0.55 cnf(c99,plain,cA(skolem0004)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c96, c48])).
% 0.39/0.55 cnf(c102,plain,cA(skolem0004)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c99, c49])).
% 0.39/0.55 cnf(c106,plain,cA(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c102, c42])).
% 0.39/0.55 cnf(c107,plain,cA(skolem0004),inference(resolution,[status(thm)],[c106, c81])).
% 0.39/0.55 cnf(c111,plain,rq(skolem0004,skolem0007(skolem0004)),inference(resolution,[status(thm)],[c107, c34])).
% 0.39/0.55 cnf(c112,plain,~cnotA(skolem0004)|cNothing(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c111, c17])).
% 0.39/0.55 cnf(c8,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cnotA(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.55 cnf(c56,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c54, c8])).
% 0.39/0.55 cnf(c64,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c56, c43])).
% 0.39/0.55 cnf(c66,plain,cnotA(skolem0004)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c64, c48])).
% 0.39/0.55 cnf(c69,plain,cnotA(skolem0004)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c66, c49])).
% 0.39/0.55 cnf(c115,plain,cNothing(skolem0007(skolem0004))|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c112, c69])).
% 0.39/0.55 fof(axiom_3,axiom,(![X]:(cNothing(X)=>(~(?[Y]:rp(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.39/0.55 fof(c24,plain,(![X]:(~cNothing(X)|(![Y]:~rp(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.39/0.55 fof(c26,plain,(![X12]:(![X13]:(~cNothing(X12)|~rp(X12,X13)))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X12]:(~cNothing(X12)|(![X13]:~rp(X12,X13)))),inference(variable_rename,[status(thm)],[c24])).])).
% 0.39/0.55 cnf(c27,plain,~cNothing(X27)|~rp(X27,X28),inference(split_conjunct,[status(thm)],[c26])).
% 0.39/0.55 fof(axiom_4,axiom,(![X]:(cNothing(X)=>(?[Y0]:rp(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.39/0.55 fof(c20,plain,(![X]:(~cNothing(X)|(?[Y0]:rp(X,Y0)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.39/0.55 fof(c21,plain,(![X10]:(~cNothing(X10)|(?[X11]:rp(X10,X11)))),inference(variable_rename,[status(thm)],[c20])).
% 0.39/0.55 fof(c22,plain,(![X10]:(~cNothing(X10)|rp(X10,skolem0006(X10)))),inference(skolemize,[status(esa)],[c21])).
% 0.39/0.55 cnf(c23,plain,~cNothing(X32)|rp(X32,skolem0006(X32)),inference(split_conjunct,[status(thm)],[c22])).
% 0.39/0.55 cnf(c118,plain,xsd_integer(skolem0003)|rp(skolem0007(skolem0004),skolem0006(skolem0007(skolem0004))),inference(resolution,[status(thm)],[c115, c23])).
% 0.39/0.55 cnf(c129,plain,xsd_integer(skolem0003)|~cNothing(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c118, c27])).
% 0.39/0.55 cnf(c130,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c129, c115])).
% 0.39/0.55 cnf(c133,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c130, c42])).
% 0.39/0.55 cnf(c10,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cnotA(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.55 cnf(c65,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cnotA(skolem0004),inference(resolution,[status(thm)],[c10, c54])).
% 0.39/0.55 cnf(c120,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cnotA(skolem0004),inference(resolution,[status(thm)],[c65, c69])).
% 0.39/0.55 cnf(c135,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cnotA(skolem0004),inference(resolution,[status(thm)],[c120, c48])).
% 0.39/0.55 cnf(c136,plain,xsd_string(skolem0003)|cnotA(skolem0004),inference(resolution,[status(thm)],[c135, c49])).
% 0.39/0.55 cnf(c139,plain,cnotA(skolem0004),inference(resolution,[status(thm)],[c136, c133])).
% 0.39/0.55 cnf(c141,plain,cNothing(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c139, c112])).
% 0.39/0.55 cnf(c142,plain,rp(skolem0007(skolem0004),skolem0006(skolem0007(skolem0004))),inference(resolution,[status(thm)],[c141, c23])).
% 0.39/0.55 cnf(c143,plain,~cNothing(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c142, c27])).
% 0.39/0.55 cnf(c144,plain,$false,inference(resolution,[status(thm)],[c143, c141])).
% 0.39/0.55 % SZS output end CNFRefutation
% 0.39/0.55
% 0.39/0.55 % Initial clauses : 16
% 0.39/0.55 % Processed clauses : 53
% 0.39/0.55 % Factors computed : 0
% 0.39/0.55 % Resolvents computed: 95
% 0.39/0.55 % Tautologies deleted: 5
% 0.39/0.55 % Forward subsumed : 30
% 0.39/0.55 % Backward subsumed : 32
% 0.39/0.55 % -------- CPU Time ---------
% 0.39/0.55 % User time : 0.199 s
% 0.39/0.55 % System time : 0.011 s
% 0.39/0.55 % Total time : 0.210 s
%------------------------------------------------------------------------------