%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS045+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:33 EDT 2024
% Result : Satisfiable 0.43s 0.61s
% Output : Saturation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS045+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n011.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:04:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.43/0.61 % Version: 1.5
% 0.43/0.61 % SZS status Satisfiable
% 0.43/0.61 % SZS output start Saturation
% 0.43/0.61 cnf(c6,axiom,X130!=X128|X129!=X131|~ra_Px1(X130,X129)|ra_Px1(X128,X131),theory(equality)).
% 0.43/0.61 fof(axiom_4,axiom,(![X]:(cp2(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.43/0.61 fof(c34,plain,(![X]:((~cp2(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp2(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.43/0.61 fof(c35,plain,((![X]:(~cp2(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp2(X)))),inference(shift_quantors,[status(thm)],[c34])).
% 0.43/0.61 fof(c36,plain,((![X16]:(~cp2(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:((?[X19]:ra_Px1(X18,X19))|cp2(X18)))),inference(variable_rename,[status(thm)],[c35])).
% 0.43/0.61 fof(c38,plain,(![X16]:(![X17]:(![X18]:((~cp2(X16)|~ra_Px1(X16,X17))&(ra_Px1(X18,skolem0002(X18))|cp2(X18)))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X16]:(~cp2(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:(ra_Px1(X18,skolem0002(X18))|cp2(X18)))),inference(skolemize,[status(esa)],[c36])).])).
% 0.43/0.61 cnf(c40,plain,ra_Px1(X103,skolem0002(X103))|cp2(X103),inference(split_conjunct,[status(thm)],[c38])).
% 0.43/0.61 cnf(c39,plain,~cp2(X87)|~ra_Px1(X87,X86),inference(split_conjunct,[status(thm)],[c38])).
% 0.43/0.61 fof(axiom_3,axiom,(![X]:(cp1(X)=>cp2xcomp(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.43/0.61 fof(c41,plain,(![X]:(~cp1(X)|cp2xcomp(X))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.43/0.61 fof(c42,plain,(![X20]:(~cp1(X20)|cp2xcomp(X20))),inference(variable_rename,[status(thm)],[c41])).
% 0.43/0.61 cnf(c43,plain,~cp1(X74)|cp2xcomp(X74),inference(split_conjunct,[status(thm)],[c42])).
% 0.43/0.61 fof(axiom_8,axiom,cSatisfiable(i2003_11_14_17_16_21280),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.43/0.61 cnf(c18,plain,cSatisfiable(i2003_11_14_17_16_21280),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.43/0.61 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.43/0.61 fof(c44,plain,(![X]:((~cSatisfiable(X)|((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y)))))&(((![Y]:(~rf2(X,Y)|~cp2(Y)))|(![Y]:(~rf1(X,Y)|~cp1(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.43/0.61 fof(c45,plain,((![X]:(~cSatisfiable(X)|((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y))))))&(![X]:(((![Y]:(~rf2(X,Y)|~cp2(Y)))|(![Y]:(~rf1(X,Y)|~cp1(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c44])).
% 0.43/0.61 fof(c46,plain,((![X21]:(~cSatisfiable(X21)|((?[X22]:(rf2(X21,X22)&cp2(X22)))&(?[X23]:(rf1(X21,X23)&cp1(X23))))))&(![X24]:(((![X25]:(~rf2(X24,X25)|~cp2(X25)))|(![X26]:(~rf1(X24,X26)|~cp1(X26))))|cSatisfiable(X24)))),inference(variable_rename,[status(thm)],[c45])).
% 0.43/0.61 fof(c48,plain,(![X21]:(![X24]:(![X25]:(![X26]:((~cSatisfiable(X21)|((rf2(X21,skolem0003(X21))&cp2(skolem0003(X21)))&(rf1(X21,skolem0004(X21))&cp1(skolem0004(X21)))))&(((~rf2(X24,X25)|~cp2(X25))|(~rf1(X24,X26)|~cp1(X26)))|cSatisfiable(X24))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X21]:(~cSatisfiable(X21)|((rf2(X21,skolem0003(X21))&cp2(skolem0003(X21)))&(rf1(X21,skolem0004(X21))&cp1(skolem0004(X21))))))&(![X24]:(((![X25]:(~rf2(X24,X25)|~cp2(X25)))|(![X26]:(~rf1(X24,X26)|~cp1(X26))))|cSatisfiable(X24)))),inference(skolemize,[status(esa)],[c46])).])).
% 0.43/0.61 fof(c49,plain,(![X21]:(![X24]:(![X25]:(![X26]:((((~cSatisfiable(X21)|rf2(X21,skolem0003(X21)))&(~cSatisfiable(X21)|cp2(skolem0003(X21))))&((~cSatisfiable(X21)|rf1(X21,skolem0004(X21)))&(~cSatisfiable(X21)|cp1(skolem0004(X21)))))&(((~rf2(X24,X25)|~cp2(X25))|(~rf1(X24,X26)|~cp1(X26)))|cSatisfiable(X24))))))),inference(distribute,[status(thm)],[c48])).
% 0.43/0.61 cnf(c53,plain,~cSatisfiable(X96)|cp1(skolem0004(X96)),inference(split_conjunct,[status(thm)],[c49])).
% 0.43/0.61 cnf(c122,plain,cp1(skolem0004(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c53, c18])).
% 0.43/0.61 cnf(c123,plain,cp2xcomp(skolem0004(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c122, c43])).
% 0.43/0.61 fof(axiom_5,axiom,(![X]:(cp2xcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.43/0.61 fof(c27,plain,(![X]:((~cp2xcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cp2xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.43/0.61 fof(c28,plain,((![X]:(~cp2xcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cp2xcomp(X)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.43/0.61 fof(c29,plain,((![X12]:(~cp2xcomp(X12)|(?[X13]:ra_Px1(X12,X13))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cp2xcomp(X14)))),inference(variable_rename,[status(thm)],[c28])).
% 0.43/0.61 fof(c31,plain,(![X12]:(![X14]:(![X15]:((~cp2xcomp(X12)|ra_Px1(X12,skolem0001(X12)))&(~ra_Px1(X14,X15)|cp2xcomp(X14)))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X12]:(~cp2xcomp(X12)|ra_Px1(X12,skolem0001(X12))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cp2xcomp(X14)))),inference(skolemize,[status(esa)],[c29])).])).
% 0.43/0.61 cnf(c32,plain,~cp2xcomp(X102)|ra_Px1(X102,skolem0001(X102)),inference(split_conjunct,[status(thm)],[c31])).
% 0.43/0.61 cnf(c124,plain,ra_Px1(skolem0004(i2003_11_14_17_16_21280),skolem0001(skolem0004(i2003_11_14_17_16_21280))),inference(resolution,[status(thm)],[c32, c123])).
% 0.43/0.61 cnf(c151,plain,~cp2(skolem0004(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c124, c39])).
% 0.43/0.61 cnf(c156,plain,ra_Px1(skolem0004(i2003_11_14_17_16_21280),skolem0002(skolem0004(i2003_11_14_17_16_21280))),inference(resolution,[status(thm)],[c151, c40])).
% 0.43/0.61 cnf(c167,plain,skolem0004(i2003_11_14_17_16_21280)!=X240|skolem0002(skolem0004(i2003_11_14_17_16_21280))!=X239|ra_Px1(X240,X239),inference(resolution,[status(thm)],[c156, c6])).
% 0.43/0.61 fof(ra_Px1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&ra_Px1(A,C))=>ra_Px1(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ra_Px1_substitution_1)).
% 0.43/0.61 fof(c95,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(A,C))|ra_Px1(B,C))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_1])).
% 0.43/0.61 fof(c96,plain,(![X56]:(![X57]:(![X58]:((X56!=X57|~ra_Px1(X56,X58))|ra_Px1(X57,X58))))),inference(variable_rename,[status(thm)],[c95])).
% 0.43/0.61 cnf(c97,plain,X183!=X181|~ra_Px1(X183,X182)|ra_Px1(X181,X182),inference(split_conjunct,[status(thm)],[c96])).
% 0.43/0.61 cnf(c170,plain,skolem0004(i2003_11_14_17_16_21280)!=X237|ra_Px1(X237,skolem0002(skolem0004(i2003_11_14_17_16_21280))),inference(resolution,[status(thm)],[c156, c97])).
% 0.43/0.61 fof(ra_Px1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&ra_Px1(C,A))=>ra_Px1(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ra_Px1_substitution_2)).
% 0.43/0.61 fof(c92,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(C,A))|ra_Px1(C,B))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_2])).
% 0.43/0.61 fof(c93,plain,(![X53]:(![X54]:(![X55]:((X53!=X54|~ra_Px1(X55,X53))|ra_Px1(X55,X54))))),inference(variable_rename,[status(thm)],[c92])).
% 0.43/0.61 cnf(c94,plain,X175!=X174|~ra_Px1(X176,X175)|ra_Px1(X176,X174),inference(split_conjunct,[status(thm)],[c93])).
% 0.43/0.61 cnf(c166,plain,skolem0002(skolem0004(i2003_11_14_17_16_21280))!=X236|ra_Px1(skolem0004(i2003_11_14_17_16_21280),X236),inference(resolution,[status(thm)],[c156, c94])).
% 0.43/0.61 cnf(c52,plain,~cSatisfiable(X109)|rf1(X109,skolem0004(X109)),inference(split_conjunct,[status(thm)],[c49])).
% 0.43/0.61 cnf(c129,plain,rf1(i2003_11_14_17_16_21280,skolem0004(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c52, c18])).
% 0.43/0.61 fof(axiom_6,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf1(X,Y0)&rf1(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.43/0.61 fof(c23,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf1(X,Y0)|~rf1(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.43/0.61 fof(c25,plain,(![X9]:(![X10]:(![X11]:(~cowlThing(X9)|((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X9]:(~cowlThing(X9)|(![X10]:(![X11]:((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.43/0.61 cnf(c26,plain,~cowlThing(X193)|~rf1(X193,X191)|~rf1(X193,X192)|X191=X192,inference(split_conjunct,[status(thm)],[c25])).
% 0.43/0.61 cnf(c162,plain,~cowlThing(i2003_11_14_17_16_21280)|~rf1(i2003_11_14_17_16_21280,X234)|X234=skolem0004(i2003_11_14_17_16_21280),inference(resolution,[status(thm)],[c26, c129])).
% 0.43/0.61 cnf(c50,plain,~cSatisfiable(X108)|rf2(X108,skolem0003(X108)),inference(split_conjunct,[status(thm)],[c49])).
% 0.43/0.61 cnf(c128,plain,rf2(i2003_11_14_17_16_21280,skolem0003(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c50, c18])).
% 0.43/0.61 fof(axiom_7,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf2(X,Y0)&rf2(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.43/0.61 fof(c19,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf2(X,Y0)|~rf2(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.43/0.61 fof(c21,plain,(![X6]:(![X7]:(![X8]:(~cowlThing(X6)|((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X6]:(~cowlThing(X6)|(![X7]:(![X8]:((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.43/0.61 cnf(c22,plain,~cowlThing(X184)|~rf2(X184,X186)|~rf2(X184,X185)|X186=X185,inference(split_conjunct,[status(thm)],[c21])).
% 0.43/0.61 cnf(c158,plain,~cowlThing(i2003_11_14_17_16_21280)|~rf2(i2003_11_14_17_16_21280,X233)|X233=skolem0003(i2003_11_14_17_16_21280),inference(resolution,[status(thm)],[c22, c128])).
% 0.43/0.61 cnf(c150,plain,skolem0004(i2003_11_14_17_16_21280)!=X232|skolem0001(skolem0004(i2003_11_14_17_16_21280))!=X231|ra_Px1(X232,X231),inference(resolution,[status(thm)],[c124, c6])).
% 0.43/0.61 cnf(c153,plain,skolem0004(i2003_11_14_17_16_21280)!=X230|ra_Px1(X230,skolem0001(skolem0004(i2003_11_14_17_16_21280))),inference(resolution,[status(thm)],[c124, c97])).
% 0.43/0.61 cnf(c149,plain,skolem0001(skolem0004(i2003_11_14_17_16_21280))!=X229|ra_Px1(skolem0004(i2003_11_14_17_16_21280),X229),inference(resolution,[status(thm)],[c124, c94])).
% 0.43/0.61 cnf(c8,axiom,X160!=X158|X159!=X161|~rf2(X160,X159)|rf2(X158,X161),theory(equality)).
% 0.43/0.61 cnf(c140,plain,i2003_11_14_17_16_21280!=X225|skolem0003(i2003_11_14_17_16_21280)!=X226|rf2(X225,X226),inference(resolution,[status(thm)],[c8, c128])).
% 0.43/0.61 cnf(c7,axiom,X144!=X142|X143!=X145|~rf1(X144,X143)|rf1(X142,X145),theory(equality)).
% 0.43/0.61 cnf(c139,plain,i2003_11_14_17_16_21280!=X224|skolem0004(i2003_11_14_17_16_21280)!=X223|rf1(X224,X223),inference(resolution,[status(thm)],[c7, c129])).
% 0.43/0.61 cnf(c148,plain,X217!=X216|ra_Px1(X216,skolem0002(X217))|cp2(X217),inference(resolution,[status(thm)],[c97, c40])).
% 0.43/0.61 cnf(c138,plain,X215!=X214|skolem0002(X215)!=X213|ra_Px1(X214,X213)|cp2(X215),inference(resolution,[status(thm)],[c6, c40])).
% 0.43/0.61 cnf(c33,plain,~ra_Px1(X82,X81)|cp2xcomp(X82),inference(split_conjunct,[status(thm)],[c31])).
% 0.43/0.61 cnf(c125,plain,cp2(X104)|cp2xcomp(X104),inference(resolution,[status(thm)],[c40, c33])).
% 0.43/0.61 cnf(c127,plain,cp2(X110)|ra_Px1(X110,skolem0001(X110)),inference(resolution,[status(thm)],[c125, c32])).
% 0.43/0.61 cnf(c147,plain,X211!=X210|ra_Px1(X210,skolem0001(X211))|cp2(X211),inference(resolution,[status(thm)],[c97, c127])).
% 0.43/0.61 cnf(c146,plain,skolem0002(X208)!=X207|ra_Px1(X208,X207)|cp2(X208),inference(resolution,[status(thm)],[c94, c40])).
% 0.43/0.61 cnf(c137,plain,X205!=X204|skolem0001(X205)!=X203|ra_Px1(X204,X203)|cp2(X205),inference(resolution,[status(thm)],[c6, c127])).
% 0.43/0.61 cnf(c145,plain,skolem0001(X202)!=X201|ra_Px1(X202,X201)|cp2(X202),inference(resolution,[status(thm)],[c94, c127])).
% 0.43/0.61 cnf(c54,plain,~rf2(X200,X199)|~cp2(X199)|~rf1(X200,X198)|~cp1(X198)|cSatisfiable(X200),inference(split_conjunct,[status(thm)],[c49])).
% 0.43/0.61 fof(rf1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf1(A,C))=>rf1(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf1_substitution_1)).
% 0.43/0.61 fof(c89,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(A,C))|rf1(B,C))))),inference(fof_nnf,[status(thm)],[rf1_substitution_1])).
% 0.43/0.61 fof(c90,plain,(![X50]:(![X51]:(![X52]:((X50!=X51|~rf1(X50,X52))|rf1(X51,X52))))),inference(variable_rename,[status(thm)],[c89])).
% 0.43/0.61 cnf(c91,plain,X173!=X172|~rf1(X173,X171)|rf1(X172,X171),inference(split_conjunct,[status(thm)],[c90])).
% 0.43/0.61 cnf(c144,plain,i2003_11_14_17_16_21280!=X197|rf1(X197,skolem0004(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c91, c129])).
% 0.43/0.61 fof(rf1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf1(C,A))=>rf1(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf1_substitution_2)).
% 0.43/0.61 fof(c86,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.43/0.61 fof(c87,plain,(![X47]:(![X48]:(![X49]:((X47!=X48|~rf1(X49,X47))|rf1(X49,X48))))),inference(variable_rename,[status(thm)],[c86])).
% 0.43/0.61 cnf(c88,plain,X169!=X168|~rf1(X170,X169)|rf1(X170,X168),inference(split_conjunct,[status(thm)],[c87])).
% 0.43/0.61 cnf(c143,plain,skolem0004(i2003_11_14_17_16_21280)!=X196|rf1(i2003_11_14_17_16_21280,X196),inference(resolution,[status(thm)],[c88, c129])).
% 0.43/0.61 fof(rf2_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf2(A,C))=>rf2(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf2_substitution_1)).
% 0.43/0.61 fof(c83,plain,(![A]:(![B]:(![C]:((A!=B|~rf2(A,C))|rf2(B,C))))),inference(fof_nnf,[status(thm)],[rf2_substitution_1])).
% 0.43/0.61 fof(c84,plain,(![X44]:(![X45]:(![X46]:((X44!=X45|~rf2(X44,X46))|rf2(X45,X46))))),inference(variable_rename,[status(thm)],[c83])).
% 0.43/0.61 cnf(c85,plain,X167!=X165|~rf2(X167,X166)|rf2(X165,X166),inference(split_conjunct,[status(thm)],[c84])).
% 0.43/0.61 cnf(c142,plain,i2003_11_14_17_16_21280!=X190|rf2(X190,skolem0003(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c85, c128])).
% 0.43/0.61 fof(rf2_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf2(C,A))=>rf2(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf2_substitution_2)).
% 0.43/0.61 fof(c80,plain,(![A]:(![B]:(![C]:((A!=B|~rf2(C,A))|rf2(C,B))))),inference(fof_nnf,[status(thm)],[rf2_substitution_2])).
% 0.43/0.61 fof(c81,plain,(![X41]:(![X42]:(![X43]:((X41!=X42|~rf2(X43,X41))|rf2(X43,X42))))),inference(variable_rename,[status(thm)],[c80])).
% 0.43/0.61 cnf(c82,plain,X163!=X162|~rf2(X164,X163)|rf2(X164,X162),inference(split_conjunct,[status(thm)],[c81])).
% 0.43/0.61 cnf(c141,plain,skolem0003(i2003_11_14_17_16_21280)!=X189|rf2(i2003_11_14_17_16_21280,X189),inference(resolution,[status(thm)],[c82, c128])).
% 0.43/0.61 cnf(c9,axiom,X179!=X177|X178!=X180|~rr(X179,X178)|rr(X177,X180),theory(equality)).
% 0.43/0.61 fof(rr_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rr(A,C))=>rr(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rr_substitution_1)).
% 0.43/0.61 fof(c77,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.43/0.61 fof(c78,plain,(![X38]:(![X39]:(![X40]:((X38!=X39|~rr(X38,X40))|rr(X39,X40))))),inference(variable_rename,[status(thm)],[c77])).
% 0.43/0.61 cnf(c79,plain,X157!=X155|~rr(X157,X156)|rr(X155,X156),inference(split_conjunct,[status(thm)],[c78])).
% 0.43/0.61 fof(rr_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rr(C,A))=>rr(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rr_substitution_2)).
% 0.43/0.61 fof(c74,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.43/0.61 fof(c75,plain,(![X35]:(![X36]:(![X37]:((X35!=X36|~rr(X37,X35))|rr(X37,X36))))),inference(variable_rename,[status(thm)],[c74])).
% 0.43/0.61 cnf(c76,plain,X153!=X152|~rr(X154,X153)|rr(X154,X152),inference(split_conjunct,[status(thm)],[c75])).
% 0.43/0.61 cnf(c11,axiom,X126!=X125|~xsd_string(X126)|xsd_string(X125),theory(equality)).
% 0.43/0.61 cnf(c10,axiom,X123!=X122|~xsd_integer(X123)|xsd_integer(X122),theory(equality)).
% 0.43/0.61 cnf(c5,axiom,X120!=X119|~cp2xcomp(X120)|cp2xcomp(X119),theory(equality)).
% 0.43/0.61 cnf(c4,axiom,X117!=X116|~cp2(X117)|cp2(X116),theory(equality)).
% 0.43/0.61 cnf(c3,axiom,X112!=X111|~cp1(X112)|cp1(X111),theory(equality)).
% 0.43/0.61 cnf(c0,axiom,X94!=X93|~cSatisfiable(X94)|cSatisfiable(X93),theory(equality)).
% 0.43/0.61 cnf(c51,plain,~cSatisfiable(X92)|cp2(skolem0003(X92)),inference(split_conjunct,[status(thm)],[c49])).
% 0.43/0.61 cnf(c120,plain,cp2(skolem0003(i2003_11_14_17_16_21280)),inference(resolution,[status(thm)],[c51, c18])).
% 0.43/0.61 fof(axiom_9,axiom,(![X]:(![Y]:(rr(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.43/0.61 fof(c15,plain,(![X]:(![Y]:(~rr(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.43/0.61 fof(c16,plain,(![X4]:(![X5]:(~rr(X4,X5)|rf1(X4,X5)))),inference(variable_rename,[status(thm)],[c15])).
% 0.43/0.61 cnf(c17,plain,~rr(X90,X91)|rf1(X90,X91),inference(split_conjunct,[status(thm)],[c16])).
% 0.43/0.61 fof(axiom_10,axiom,(![X]:(![Y]:(rr(X,Y)=>rf2(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.43/0.61 fof(c12,plain,(![X]:(![Y]:(~rr(X,Y)|rf2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.43/0.61 fof(c13,plain,(![X2]:(![X3]:(~rr(X2,X3)|rf2(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.43/0.61 cnf(c14,plain,~rr(X88,X89)|rf2(X88,X89),inference(split_conjunct,[status(thm)],[c13])).
% 0.43/0.61 cnf(transitivity,axiom,X85!=X83|X83!=X84|X85=X84,theory(equality)).
% 0.43/0.61 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.43/0.61 fof(c55,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.43/0.61 fof(c56,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c55])).
% 0.43/0.61 fof(c57,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c56])).
% 0.43/0.61 fof(c59,plain,(![X27]:(![X28]:((~xsd_string(X27)|~xsd_integer(X27))&(xsd_integer(X28)|xsd_string(X28))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,((![X27]:(~xsd_string(X27)|~xsd_integer(X27)))&(![X28]:(xsd_integer(X28)|xsd_string(X28)))),inference(variable_rename,[status(thm)],[c57])).])).
% 0.43/0.61 cnf(c61,plain,xsd_integer(X79)|xsd_string(X79),inference(split_conjunct,[status(thm)],[c59])).
% 0.43/0.61 cnf(c60,plain,~xsd_string(X78)|~xsd_integer(X78),inference(split_conjunct,[status(thm)],[c59])).
% 0.43/0.61 cnf(symmetry,axiom,X76!=X75|X75=X76,theory(equality)).
% 0.43/0.61 cnf(reflexivity,axiom,X73=X73,theory(equality)).
% 0.43/0.61 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.43/0.61 fof(c62,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.43/0.61 fof(c63,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c62])).
% 0.43/0.61 fof(c65,plain,(![X29]:(![X30]:(cowlThing(X29)&~cowlNothing(X30)))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X29]:cowlThing(X29))&(![X30]:~cowlNothing(X30))),inference(variable_rename,[status(thm)],[c63])).])).
% 0.43/0.61 cnf(c67,plain,~cowlNothing(X72),inference(split_conjunct,[status(thm)],[c65])).
% 0.43/0.61 cnf(c66,plain,cowlThing(X71),inference(split_conjunct,[status(thm)],[c65])).
% 0.43/0.61 % SZS output end Saturation
% 0.43/0.61
% 0.43/0.61 % Initial clauses : 50
% 0.43/0.61 % Processed clauses : 70
% 0.43/0.61 % Factors computed : 3
% 0.43/0.61 % Resolvents computed: 68
% 0.43/0.61 % Tautologies deleted: 11
% 0.43/0.61 % Forward subsumed : 40
% 0.43/0.61 % Backward subsumed : 0
% 0.43/0.61 % -------- CPU Time ---------
% 0.43/0.61 % User time : 0.227 s
% 0.43/0.61 % System time : 0.015 s
% 0.43/0.61 % Total time : 0.242 s
%------------------------------------------------------------------------------