%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS031+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:31 EDT 2024
% Result : Satisfiable 0.19s 0.56s
% Output : Saturation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS031+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.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:05:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.19/0.56 % Version: 1.5
% 0.19/0.56 % SZS status Satisfiable
% 0.19/0.56 % SZS output start Saturation
% 0.19/0.56 fof(axiom_6,axiom,cSatisfiable(i2003_11_14_17_15_2938),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.19/0.56 cnf(c16,plain,cSatisfiable(i2003_11_14_17_15_2938),inference(split_conjunct,[status(thm)],[axiom_6])).
% 0.19/0.56 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&cp2(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.19/0.56 fof(c29,plain,(![X]:((~cSatisfiable(X)|((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&cp2(Y)))))&(((![Y]:(~rf1(X,Y)|~cp1(Y)))|(![Y]:(~rf2(X,Y)|~cp2(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.19/0.56 fof(c30,plain,((![X]:(~cSatisfiable(X)|((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&cp2(Y))))))&(![X]:(((![Y]:(~rf1(X,Y)|~cp1(Y)))|(![Y]:(~rf2(X,Y)|~cp2(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c29])).
% 0.19/0.56 fof(c31,plain,((![X13]:(~cSatisfiable(X13)|((?[X14]:(rf1(X13,X14)&cp1(X14)))&(?[X15]:(rf2(X13,X15)&cp2(X15))))))&(![X16]:(((![X17]:(~rf1(X16,X17)|~cp1(X17)))|(![X18]:(~rf2(X16,X18)|~cp2(X18))))|cSatisfiable(X16)))),inference(variable_rename,[status(thm)],[c30])).
% 0.19/0.56 fof(c33,plain,(![X13]:(![X16]:(![X17]:(![X18]:((~cSatisfiable(X13)|((rf1(X13,skolem0001(X13))&cp1(skolem0001(X13)))&(rf2(X13,skolem0002(X13))&cp2(skolem0002(X13)))))&(((~rf1(X16,X17)|~cp1(X17))|(~rf2(X16,X18)|~cp2(X18)))|cSatisfiable(X16))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X13]:(~cSatisfiable(X13)|((rf1(X13,skolem0001(X13))&cp1(skolem0001(X13)))&(rf2(X13,skolem0002(X13))&cp2(skolem0002(X13))))))&(![X16]:(((![X17]:(~rf1(X16,X17)|~cp1(X17)))|(![X18]:(~rf2(X16,X18)|~cp2(X18))))|cSatisfiable(X16)))),inference(skolemize,[status(esa)],[c31])).])).
% 0.19/0.56 fof(c34,plain,(![X13]:(![X16]:(![X17]:(![X18]:((((~cSatisfiable(X13)|rf1(X13,skolem0001(X13)))&(~cSatisfiable(X13)|cp1(skolem0001(X13))))&((~cSatisfiable(X13)|rf2(X13,skolem0002(X13)))&(~cSatisfiable(X13)|cp2(skolem0002(X13)))))&(((~rf1(X16,X17)|~cp1(X17))|(~rf2(X16,X18)|~cp2(X18)))|cSatisfiable(X16))))))),inference(distribute,[status(thm)],[c33])).
% 0.19/0.56 cnf(c37,plain,~cSatisfiable(X83)|rf2(X83,skolem0002(X83)),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.56 cnf(c101,plain,rf2(i2003_11_14_17_15_2938,skolem0002(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c37, c16])).
% 0.19/0.56 fof(axiom_4,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf2(X,Y0)&rf2(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.19/0.56 fof(c21,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf2(X,Y0)|~rf2(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.19/0.56 fof(c23,plain,(![X9]:(![X10]:(![X11]:(~cowlThing(X9)|((~rf2(X9,X10)|~rf2(X9,X11))|X10=X11))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,(![X9]:(~cowlThing(X9)|(![X10]:(![X11]:((~rf2(X9,X10)|~rf2(X9,X11))|X10=X11))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.19/0.56 cnf(c24,plain,~cowlThing(X151)|~rf2(X151,X150)|~rf2(X151,X152)|X150=X152,inference(split_conjunct,[status(thm)],[c23])).
% 0.19/0.56 cnf(c118,plain,~cowlThing(i2003_11_14_17_15_2938)|~rf2(i2003_11_14_17_15_2938,X166)|X166=skolem0002(i2003_11_14_17_15_2938),inference(resolution,[status(thm)],[c24, c101])).
% 0.19/0.56 cnf(c35,plain,~cSatisfiable(X80)|rf1(X80,skolem0001(X80)),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.56 cnf(c100,plain,rf1(i2003_11_14_17_15_2938,skolem0001(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c35, c16])).
% 0.19/0.56 fof(axiom_5,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf1(X,Y0)&rf1(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.19/0.56 fof(c17,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf1(X,Y0)|~rf1(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.19/0.56 fof(c19,plain,(![X6]:(![X7]:(![X8]:(~cowlThing(X6)|((~rf1(X6,X7)|~rf1(X6,X8))|X7=X8))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X6]:(~cowlThing(X6)|(![X7]:(![X8]:((~rf1(X6,X7)|~rf1(X6,X8))|X7=X8))))),inference(variable_rename,[status(thm)],[c17])).])).
% 0.19/0.56 cnf(c20,plain,~cowlThing(X144)|~rf1(X144,X145)|~rf1(X144,X143)|X145=X143,inference(split_conjunct,[status(thm)],[c19])).
% 0.19/0.56 cnf(c114,plain,~cowlThing(i2003_11_14_17_15_2938)|~rf1(i2003_11_14_17_15_2938,X165)|X165=skolem0001(i2003_11_14_17_15_2938),inference(resolution,[status(thm)],[c20, c100])).
% 0.19/0.56 cnf(c6,axiom,X113!=X112|X111!=X110|~rf2(X113,X111)|rf2(X112,X110),theory(equality)).
% 0.19/0.56 cnf(c107,plain,i2003_11_14_17_15_2938!=X163|skolem0002(i2003_11_14_17_15_2938)!=X162|rf2(X163,X162),inference(resolution,[status(thm)],[c6, c101])).
% 0.19/0.56 cnf(c39,plain,~rf1(X160,X158)|~cp1(X158)|~rf2(X160,X159)|~cp2(X159)|cSatisfiable(X160),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.56 cnf(c5,axiom,X100!=X99|X98!=X97|~rf1(X100,X98)|rf1(X99,X97),theory(equality)).
% 0.19/0.56 cnf(c106,plain,i2003_11_14_17_15_2938!=X156|skolem0001(i2003_11_14_17_15_2938)!=X157|rf1(X156,X157),inference(resolution,[status(thm)],[c5, c100])).
% 0.19/0.56 fof(rf1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf1(A,C))=>rf1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf1_substitution_1)).
% 0.19/0.56 fof(c74,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(A,C))|rf1(B,C))))),inference(fof_nnf,[status(thm)],[rf1_substitution_1])).
% 0.19/0.56 fof(c75,plain,(![X42]:(![X43]:(![X44]:((X42!=X43|~rf1(X42,X44))|rf1(X43,X44))))),inference(variable_rename,[status(thm)],[c74])).
% 0.19/0.56 cnf(c76,plain,X139!=X141|~rf1(X139,X140)|rf1(X141,X140),inference(split_conjunct,[status(thm)],[c75])).
% 0.19/0.56 cnf(c111,plain,i2003_11_14_17_15_2938!=X155|rf1(X155,skolem0001(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c76, c100])).
% 0.19/0.56 fof(rf1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf1(C,A))=>rf1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf1_substitution_2)).
% 0.19/0.56 fof(c71,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.19/0.56 fof(c72,plain,(![X39]:(![X40]:(![X41]:((X39!=X40|~rf1(X41,X39))|rf1(X41,X40))))),inference(variable_rename,[status(thm)],[c71])).
% 0.19/0.56 cnf(c73,plain,X138!=X137|~rf1(X136,X138)|rf1(X136,X137),inference(split_conjunct,[status(thm)],[c72])).
% 0.19/0.56 cnf(c110,plain,skolem0001(i2003_11_14_17_15_2938)!=X149|rf1(i2003_11_14_17_15_2938,X149),inference(resolution,[status(thm)],[c73, c100])).
% 0.19/0.56 fof(rf2_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf2(A,C))=>rf2(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf2_substitution_1)).
% 0.19/0.56 fof(c68,plain,(![A]:(![B]:(![C]:((A!=B|~rf2(A,C))|rf2(B,C))))),inference(fof_nnf,[status(thm)],[rf2_substitution_1])).
% 0.19/0.56 fof(c69,plain,(![X36]:(![X37]:(![X38]:((X36!=X37|~rf2(X36,X38))|rf2(X37,X38))))),inference(variable_rename,[status(thm)],[c68])).
% 0.19/0.56 cnf(c70,plain,X133!=X134|~rf2(X133,X135)|rf2(X134,X135),inference(split_conjunct,[status(thm)],[c69])).
% 0.19/0.56 cnf(c109,plain,i2003_11_14_17_15_2938!=X148|rf2(X148,skolem0002(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c70, c101])).
% 0.19/0.56 fof(rf2_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf2(C,A))=>rf2(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf2_substitution_2)).
% 0.19/0.56 fof(c65,plain,(![A]:(![B]:(![C]:((A!=B|~rf2(C,A))|rf2(C,B))))),inference(fof_nnf,[status(thm)],[rf2_substitution_2])).
% 0.19/0.56 fof(c66,plain,(![X33]:(![X34]:(![X35]:((X33!=X34|~rf2(X35,X33))|rf2(X35,X34))))),inference(variable_rename,[status(thm)],[c65])).
% 0.19/0.56 cnf(c67,plain,X130!=X132|~rf2(X131,X130)|rf2(X131,X132),inference(split_conjunct,[status(thm)],[c66])).
% 0.19/0.56 cnf(c108,plain,skolem0002(i2003_11_14_17_15_2938)!=X142|rf2(i2003_11_14_17_15_2938,X142),inference(resolution,[status(thm)],[c67, c101])).
% 0.19/0.56 cnf(c7,axiom,X129!=X128|X127!=X126|~rr(X129,X127)|rr(X128,X126),theory(equality)).
% 0.19/0.56 fof(rr_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rr(A,C))=>rr(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rr_substitution_1)).
% 0.19/0.56 fof(c62,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.19/0.56 fof(c63,plain,(![X30]:(![X31]:(![X32]:((X30!=X31|~rr(X30,X32))|rr(X31,X32))))),inference(variable_rename,[status(thm)],[c62])).
% 0.19/0.56 cnf(c64,plain,X125!=X124|~rr(X125,X123)|rr(X124,X123),inference(split_conjunct,[status(thm)],[c63])).
% 0.19/0.56 fof(rr_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rr(C,A))=>rr(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rr_substitution_2)).
% 0.19/0.56 fof(c59,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.19/0.56 fof(c60,plain,(![X27]:(![X28]:(![X29]:((X27!=X28|~rr(X29,X27))|rr(X29,X28))))),inference(variable_rename,[status(thm)],[c59])).
% 0.19/0.56 cnf(c61,plain,X122!=X121|~rr(X120,X122)|rr(X120,X121),inference(split_conjunct,[status(thm)],[c60])).
% 0.19/0.56 cnf(c9,axiom,X96!=X95|~xsd_string(X96)|xsd_string(X95),theory(equality)).
% 0.19/0.56 cnf(c8,axiom,X93!=X92|~xsd_integer(X93)|xsd_integer(X92),theory(equality)).
% 0.19/0.56 cnf(c4,axiom,X89!=X88|~cp2(X89)|cp2(X88),theory(equality)).
% 0.19/0.56 cnf(c3,axiom,X87!=X86|~cp1(X87)|cp1(X86),theory(equality)).
% 0.19/0.56 fof(axiom_3,axiom,(![X]:(cp1(X)=>(~cp2(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.19/0.56 fof(c25,plain,(![X]:(cp1(X)=>~cp2(X))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.19/0.56 fof(c26,plain,(![X]:(~cp1(X)|~cp2(X))),inference(fof_nnf,[status(thm)],[c25])).
% 0.19/0.56 fof(c27,plain,(![X12]:(~cp1(X12)|~cp2(X12))),inference(variable_rename,[status(thm)],[c26])).
% 0.19/0.56 cnf(c28,plain,~cp1(X58)|~cp2(X58),inference(split_conjunct,[status(thm)],[c27])).
% 0.19/0.56 cnf(c38,plain,~cSatisfiable(X73)|cp2(skolem0002(X73)),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.56 cnf(c97,plain,cp2(skolem0002(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c38, c16])).
% 0.19/0.56 cnf(c98,plain,~cp1(skolem0002(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c97, c28])).
% 0.19/0.56 cnf(c0,axiom,X75!=X74|~cSatisfiable(X75)|cSatisfiable(X74),theory(equality)).
% 0.19/0.56 cnf(c36,plain,~cSatisfiable(X72)|cp1(skolem0001(X72)),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.56 cnf(c96,plain,cp1(skolem0001(i2003_11_14_17_15_2938)),inference(resolution,[status(thm)],[c36, c16])).
% 0.19/0.56 fof(axiom_7,axiom,(![X]:(![Y]:(rr(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.19/0.56 fof(c13,plain,(![X]:(![Y]:(~rr(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.19/0.56 fof(c14,plain,(![X4]:(![X5]:(~rr(X4,X5)|rf1(X4,X5)))),inference(variable_rename,[status(thm)],[c13])).
% 0.19/0.56 cnf(c15,plain,~rr(X70,X71)|rf1(X70,X71),inference(split_conjunct,[status(thm)],[c14])).
% 0.19/0.56 cnf(transitivity,axiom,X69!=X68|X68!=X67|X69=X67,theory(equality)).
% 0.19/0.56 fof(axiom_8,axiom,(![X]:(![Y]:(rr(X,Y)=>rf2(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.19/0.56 fof(c10,plain,(![X]:(![Y]:(~rr(X,Y)|rf2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.19/0.56 fof(c11,plain,(![X2]:(![X3]:(~rr(X2,X3)|rf2(X2,X3)))),inference(variable_rename,[status(thm)],[c10])).
% 0.19/0.56 cnf(c12,plain,~rr(X65,X66)|rf2(X65,X66),inference(split_conjunct,[status(thm)],[c11])).
% 0.19/0.56 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.19/0.56 fof(c40,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.19/0.56 fof(c41,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c40])).
% 0.19/0.56 fof(c42,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c41])).
% 0.19/0.56 fof(c44,plain,(![X19]:(![X20]:((~xsd_string(X19)|~xsd_integer(X19))&(xsd_integer(X20)|xsd_string(X20))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X19]:(~xsd_string(X19)|~xsd_integer(X19)))&(![X20]:(xsd_integer(X20)|xsd_string(X20)))),inference(variable_rename,[status(thm)],[c42])).])).
% 0.19/0.56 cnf(c46,plain,xsd_integer(X63)|xsd_string(X63),inference(split_conjunct,[status(thm)],[c44])).
% 0.19/0.56 cnf(c45,plain,~xsd_string(X62)|~xsd_integer(X62),inference(split_conjunct,[status(thm)],[c44])).
% 0.19/0.56 cnf(symmetry,axiom,X60!=X59|X59=X60,theory(equality)).
% 0.19/0.56 cnf(reflexivity,axiom,X57=X57,theory(equality)).
% 0.19/0.56 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.19/0.56 fof(c47,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.19/0.56 fof(c48,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c47])).
% 0.19/0.56 fof(c50,plain,(![X21]:(![X22]:(cowlThing(X21)&~cowlNothing(X22)))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X21]:cowlThing(X21))&(![X22]:~cowlNothing(X22))),inference(variable_rename,[status(thm)],[c48])).])).
% 0.19/0.56 cnf(c52,plain,~cowlNothing(X56),inference(split_conjunct,[status(thm)],[c50])).
% 0.19/0.56 cnf(c51,plain,cowlThing(X55),inference(split_conjunct,[status(thm)],[c50])).
% 0.19/0.56 % SZS output end Saturation
% 0.19/0.56
% 0.19/0.56 % Initial clauses : 41
% 0.19/0.56 % Processed clauses : 45
% 0.19/0.56 % Factors computed : 3
% 0.19/0.56 % Resolvents computed: 30
% 0.19/0.56 % Tautologies deleted: 8
% 0.19/0.56 % Forward subsumed : 21
% 0.19/0.56 % Backward subsumed : 0
% 0.19/0.56 % -------- CPU Time ---------
% 0.19/0.56 % User time : 0.208 s
% 0.19/0.56 % System time : 0.011 s
% 0.19/0.56 % Total time : 0.219 s
%------------------------------------------------------------------------------