%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS129+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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.59s
% Output : Refutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS129+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:13:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.39/0.59 % Version: 1.5
% 0.39/0.59 % SZS status Theorem
% 0.39/0.59 % SZS output start CNFRefutation
% 0.39/0.59 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.39/0.59 fof(c59,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.39/0.59 fof(c60,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c59])).
% 0.39/0.59 fof(c61,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 0.39/0.59 fof(c63,plain,(![X17]:(![X18]:((~xsd_string(X17)|~xsd_integer(X17))&(xsd_integer(X18)|xsd_string(X18))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X17]:(~xsd_string(X17)|~xsd_integer(X17)))&(![X18]:(xsd_integer(X18)|xsd_string(X18)))),inference(variable_rename,[status(thm)],[c61])).])).
% 0.39/0.59 cnf(c64,plain,~xsd_string(X58)|~xsd_integer(X58),inference(split_conjunct,[status(thm)],[c63])).
% 0.39/0.59 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.39/0.59 fof(c66,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.39/0.59 fof(c67,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c66])).
% 0.39/0.59 fof(c69,plain,(![X19]:(![X20]:(cowlThing(X19)&~cowlNothing(X20)))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X19]:cowlThing(X19))&(![X20]:~cowlNothing(X20))),inference(variable_rename,[status(thm)],[c67])).])).
% 0.39/0.59 cnf(c71,plain,~cowlNothing(X50),inference(split_conjunct,[status(thm)],[c69])).
% 0.39/0.59 cnf(c70,plain,cowlThing(X49),inference(split_conjunct,[status(thm)],[c69])).
% 0.39/0.59 cnf(c65,plain,xsd_integer(X59)|xsd_string(X59),inference(split_conjunct,[status(thm)],[c63])).
% 0.39/0.59 fof(axiom_13,axiom,rhasEuroMP(iUK,iKinnock),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_13)).
% 0.39/0.59 cnf(c19,plain,rhasEuroMP(iUK,iKinnock),inference(split_conjunct,[status(thm)],[axiom_13])).
% 0.39/0.59 fof(axiom_5,axiom,(![X]:(![Y]:(risEuroMPFrom(X,Y)<=>rhasEuroMP(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.39/0.59 fof(c27,plain,(![X]:(![Y]:((~risEuroMPFrom(X,Y)|rhasEuroMP(Y,X))&(~rhasEuroMP(Y,X)|risEuroMPFrom(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.39/0.59 fof(c28,plain,((![X]:(![Y]:(~risEuroMPFrom(X,Y)|rhasEuroMP(Y,X))))&(![X]:(![Y]:(~rhasEuroMP(Y,X)|risEuroMPFrom(X,Y))))),inference(shift_quantors,[status(thm)],[c27])).
% 0.39/0.59 fof(c30,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~risEuroMPFrom(X5,X6)|rhasEuroMP(X6,X5))&(~rhasEuroMP(X8,X7)|risEuroMPFrom(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X5]:(![X6]:(~risEuroMPFrom(X5,X6)|rhasEuroMP(X6,X5))))&(![X7]:(![X8]:(~rhasEuroMP(X8,X7)|risEuroMPFrom(X7,X8))))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.39/0.59 cnf(c32,plain,~rhasEuroMP(X68,X69)|risEuroMPFrom(X69,X68),inference(split_conjunct,[status(thm)],[c30])).
% 0.39/0.59 cnf(c114,plain,risEuroMPFrom(iKinnock,iUK),inference(resolution,[status(thm)],[c32, c19])).
% 0.39/0.59 fof(axiom_3,axiom,(![X]:(cEuroMP(X)<=>(?[Y]:(risEuroMPFrom(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.39/0.59 fof(c38,plain,(![X]:((~cEuroMP(X)|(?[Y]:(risEuroMPFrom(X,Y)&cowlThing(Y))))&((![Y]:(~risEuroMPFrom(X,Y)|~cowlThing(Y)))|cEuroMP(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.39/0.59 fof(c39,plain,((![X]:(~cEuroMP(X)|(?[Y]:(risEuroMPFrom(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~risEuroMPFrom(X,Y)|~cowlThing(Y)))|cEuroMP(X)))),inference(shift_quantors,[status(thm)],[c38])).
% 0.39/0.59 fof(c40,plain,((![X11]:(~cEuroMP(X11)|(?[X12]:(risEuroMPFrom(X11,X12)&cowlThing(X12)))))&(![X13]:((![X14]:(~risEuroMPFrom(X13,X14)|~cowlThing(X14)))|cEuroMP(X13)))),inference(variable_rename,[status(thm)],[c39])).
% 0.39/0.59 fof(c42,plain,(![X11]:(![X13]:(![X14]:((~cEuroMP(X11)|(risEuroMPFrom(X11,skolem0004(X11))&cowlThing(skolem0004(X11))))&((~risEuroMPFrom(X13,X14)|~cowlThing(X14))|cEuroMP(X13)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X11]:(~cEuroMP(X11)|(risEuroMPFrom(X11,skolem0004(X11))&cowlThing(skolem0004(X11)))))&(![X13]:((![X14]:(~risEuroMPFrom(X13,X14)|~cowlThing(X14)))|cEuroMP(X13)))),inference(skolemize,[status(esa)],[c40])).])).
% 0.39/0.59 fof(c43,plain,(![X11]:(![X13]:(![X14]:(((~cEuroMP(X11)|risEuroMPFrom(X11,skolem0004(X11)))&(~cEuroMP(X11)|cowlThing(skolem0004(X11))))&((~risEuroMPFrom(X13,X14)|~cowlThing(X14))|cEuroMP(X13)))))),inference(distribute,[status(thm)],[c42])).
% 0.39/0.59 cnf(c46,plain,~risEuroMPFrom(X105,X104)|~cowlThing(X104)|cEuroMP(X105),inference(split_conjunct,[status(thm)],[c43])).
% 0.39/0.59 cnf(c128,plain,~cowlThing(iUK)|cEuroMP(iKinnock),inference(resolution,[status(thm)],[c46, c114])).
% 0.39/0.59 cnf(c129,plain,cEuroMP(iKinnock),inference(resolution,[status(thm)],[c128, c70])).
% 0.39/0.59 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&cEuroMP(iKinnock)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 0.39/0.59 fof(c10,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&cEuroMP(iKinnock))),inference(assume_negation,[status(cth)],[the_axiom])).
% 0.39/0.59 fof(c11,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&cEuroMP(iKinnock))),inference(fof_simplification,[status(thm)],[c10])).
% 0.39/0.59 fof(c12,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|~cEuroMP(iKinnock)),inference(fof_nnf,[status(thm)],[c11])).
% 0.39/0.59 fof(c13,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|~cEuroMP(iKinnock)),inference(shift_quantors,[status(thm)],[c12])).
% 0.39/0.59 fof(c14,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|~cEuroMP(iKinnock)),inference(variable_rename,[status(thm)],[c13])).
% 0.39/0.59 fof(c15,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|~cEuroMP(iKinnock)),inference(skolemize,[status(esa)],[c14])).
% 0.39/0.59 fof(c16,negated_conjecture,((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|~cEuroMP(iKinnock))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|~cEuroMP(iKinnock))),inference(distribute,[status(thm)],[c15])).
% 0.39/0.59 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cEuroMP(iKinnock),inference(split_conjunct,[status(thm)],[c16])).
% 0.39/0.59 cnf(c138,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c17, c129])).
% 0.39/0.59 cnf(c167,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c138, c65])).
% 0.39/0.59 cnf(c168,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c167, c70])).
% 0.39/0.59 cnf(c169,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c168, c71])).
% 0.39/0.59 cnf(c171,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c169, c64])).
% 0.39/0.59 cnf(c18,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cEuroMP(iKinnock),inference(split_conjunct,[status(thm)],[c16])).
% 0.39/0.59 cnf(c139,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c18, c129])).
% 0.39/0.59 cnf(c173,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c139, c65])).
% 0.39/0.59 cnf(c175,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c173, c70])).
% 0.39/0.59 cnf(c176,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c175, c71])).
% 0.39/0.59 cnf(c178,plain,$false,inference(resolution,[status(thm)],[c176, c171])).
% 0.39/0.59 % SZS output end CNFRefutation
% 0.39/0.59
% 0.39/0.59 % Initial clauses : 52
% 0.39/0.59 % Processed clauses : 74
% 0.39/0.59 % Factors computed : 1
% 0.39/0.59 % Resolvents computed: 70
% 0.39/0.59 % Tautologies deleted: 9
% 0.39/0.59 % Forward subsumed : 31
% 0.39/0.59 % Backward subsumed : 9
% 0.39/0.59 % -------- CPU Time ---------
% 0.39/0.59 % User time : 0.221 s
% 0.39/0.59 % System time : 0.020 s
% 0.39/0.59 % Total time : 0.241 s
%------------------------------------------------------------------------------