%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS030+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:31 EDT 2024
% Result : Satisfiable 0.40s 0.60s
% Output : Saturation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS030+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 : n026.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:10:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.40/0.60 % Version: 1.5
% 0.40/0.60 % SZS status Satisfiable
% 0.40/0.60 % SZS output start Saturation
% 0.40/0.60 fof(axiom_6,axiom,(![X]:(![Y]:(rinvF1(X,Y)<=>rf1(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.40/0.60 fof(c28,plain,(![X]:(![Y]:((~rinvF1(X,Y)|rf1(Y,X))&(~rf1(Y,X)|rinvF1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.40/0.60 fof(c29,plain,((![X]:(![Y]:(~rinvF1(X,Y)|rf1(Y,X))))&(![X]:(![Y]:(~rf1(Y,X)|rinvF1(X,Y))))),inference(shift_quantors,[status(thm)],[c28])).
% 0.40/0.60 fof(c31,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rinvF1(X13,X14)|rf1(X14,X13))&(~rf1(X16,X15)|rinvF1(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X13]:(![X14]:(~rinvF1(X13,X14)|rf1(X14,X13))))&(![X15]:(![X16]:(~rf1(X16,X15)|rinvF1(X15,X16))))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.40/0.60 cnf(c33,plain,~rf1(X108,X107)|rinvF1(X107,X108),inference(split_conjunct,[status(thm)],[c31])).
% 0.40/0.60 fof(axiom_9,axiom,cSatisfiable(i2003_11_14_17_15_26245),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.40/0.60 cnf(c18,plain,cSatisfiable(i2003_11_14_17_15_26245),inference(split_conjunct,[status(thm)],[axiom_9])).
% 0.40/0.60 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>((?[Y]:(rf1(X,Y)&(~cp(Y))))&(?[Y]:(rf(X,Y)&cp(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.40/0.60 fof(c46,plain,(![X]:(cSatisfiable(X)<=>((?[Y]:(rf1(X,Y)&~cp(Y)))&(?[Y]:(rf(X,Y)&cp(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.40/0.60 fof(c47,plain,(![X]:((~cSatisfiable(X)|((?[Y]:(rf1(X,Y)&~cp(Y)))&(?[Y]:(rf(X,Y)&cp(Y)))))&(((![Y]:(~rf1(X,Y)|cp(Y)))|(![Y]:(~rf(X,Y)|~cp(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[c46])).
% 0.40/0.60 fof(c48,plain,((![X]:(~cSatisfiable(X)|((?[Y]:(rf1(X,Y)&~cp(Y)))&(?[Y]:(rf(X,Y)&cp(Y))))))&(![X]:(((![Y]:(~rf1(X,Y)|cp(Y)))|(![Y]:(~rf(X,Y)|~cp(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c47])).
% 0.40/0.60 fof(c49,plain,((![X27]:(~cSatisfiable(X27)|((?[X28]:(rf1(X27,X28)&~cp(X28)))&(?[X29]:(rf(X27,X29)&cp(X29))))))&(![X30]:(((![X31]:(~rf1(X30,X31)|cp(X31)))|(![X32]:(~rf(X30,X32)|~cp(X32))))|cSatisfiable(X30)))),inference(variable_rename,[status(thm)],[c48])).
% 0.40/0.60 fof(c51,plain,(![X27]:(![X30]:(![X31]:(![X32]:((~cSatisfiable(X27)|((rf1(X27,skolem0001(X27))&~cp(skolem0001(X27)))&(rf(X27,skolem0002(X27))&cp(skolem0002(X27)))))&(((~rf1(X30,X31)|cp(X31))|(~rf(X30,X32)|~cp(X32)))|cSatisfiable(X30))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X27]:(~cSatisfiable(X27)|((rf1(X27,skolem0001(X27))&~cp(skolem0001(X27)))&(rf(X27,skolem0002(X27))&cp(skolem0002(X27))))))&(![X30]:(((![X31]:(~rf1(X30,X31)|cp(X31)))|(![X32]:(~rf(X30,X32)|~cp(X32))))|cSatisfiable(X30)))),inference(skolemize,[status(esa)],[c49])).])).
% 0.40/0.60 fof(c52,plain,(![X27]:(![X30]:(![X31]:(![X32]:((((~cSatisfiable(X27)|rf1(X27,skolem0001(X27)))&(~cSatisfiable(X27)|~cp(skolem0001(X27))))&((~cSatisfiable(X27)|rf(X27,skolem0002(X27)))&(~cSatisfiable(X27)|cp(skolem0002(X27)))))&(((~rf1(X30,X31)|cp(X31))|(~rf(X30,X32)|~cp(X32)))|cSatisfiable(X30))))))),inference(distribute,[status(thm)],[c51])).
% 0.40/0.60 cnf(c53,plain,~cSatisfiable(X123)|rf1(X123,skolem0001(X123)),inference(split_conjunct,[status(thm)],[c52])).
% 0.40/0.60 cnf(c131,plain,rf1(i2003_11_14_17_15_26245,skolem0001(i2003_11_14_17_15_26245)),inference(resolution,[status(thm)],[c53, c18])).
% 0.40/0.60 cnf(c132,plain,rinvF1(skolem0001(i2003_11_14_17_15_26245),i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c131, c33])).
% 0.40/0.60 cnf(c7,axiom,X186!=X185|X187!=X184|~rinvF1(X186,X187)|rinvF1(X185,X184),theory(equality)).
% 0.40/0.60 cnf(c148,plain,skolem0001(i2003_11_14_17_15_26245)!=X246|i2003_11_14_17_15_26245!=X245|rinvF1(X246,X245),inference(resolution,[status(thm)],[c7, c132])).
% 0.40/0.60 fof(axiom_5,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.40/0.60 fof(c34,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.40/0.60 fof(c35,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c34])).
% 0.40/0.60 fof(c37,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~rinvF(X17,X18)|rf(X18,X17))&(~rf(X20,X19)|rinvF(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X17]:(![X18]:(~rinvF(X17,X18)|rf(X18,X17))))&(![X19]:(![X20]:(~rf(X20,X19)|rinvF(X19,X20))))),inference(variable_rename,[status(thm)],[c35])).])).
% 0.40/0.60 cnf(c39,plain,~rf(X114,X115)|rinvF(X115,X114),inference(split_conjunct,[status(thm)],[c37])).
% 0.40/0.60 cnf(c55,plain,~cSatisfiable(X126)|rf(X126,skolem0002(X126)),inference(split_conjunct,[status(thm)],[c52])).
% 0.40/0.60 cnf(c134,plain,rf(i2003_11_14_17_15_26245,skolem0002(i2003_11_14_17_15_26245)),inference(resolution,[status(thm)],[c55, c18])).
% 0.40/0.60 cnf(c135,plain,rinvF(skolem0002(i2003_11_14_17_15_26245),i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c134, c39])).
% 0.40/0.60 cnf(c6,axiom,X168!=X167|X169!=X166|~rinvF(X168,X169)|rinvF(X167,X166),theory(equality)).
% 0.40/0.60 cnf(c145,plain,skolem0002(i2003_11_14_17_15_26245)!=X242|i2003_11_14_17_15_26245!=X241|rinvF(X242,X241),inference(resolution,[status(thm)],[c6, c135])).
% 0.40/0.60 fof(rf_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf(A,C))=>rf(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf_substitution_1)).
% 0.40/0.60 fof(c110,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.40/0.60 fof(c111,plain,(![X74]:(![X75]:(![X76]:((X74!=X75|~rf(X74,X76))|rf(X75,X76))))),inference(variable_rename,[status(thm)],[c110])).
% 0.40/0.60 cnf(c112,plain,X216!=X217|~rf(X216,X218)|rf(X217,X218),inference(split_conjunct,[status(thm)],[c111])).
% 0.40/0.60 cnf(c156,plain,i2003_11_14_17_15_26245!=X239|rf(X239,skolem0002(i2003_11_14_17_15_26245)),inference(resolution,[status(thm)],[c112, c134])).
% 0.40/0.60 fof(rf_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf(C,A))=>rf(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf_substitution_2)).
% 0.40/0.60 fof(c107,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.40/0.60 fof(c108,plain,(![X71]:(![X72]:(![X73]:((X71!=X72|~rf(X73,X71))|rf(X73,X72))))),inference(variable_rename,[status(thm)],[c107])).
% 0.40/0.60 cnf(c109,plain,X213!=X215|~rf(X214,X213)|rf(X214,X215),inference(split_conjunct,[status(thm)],[c108])).
% 0.40/0.60 cnf(c155,plain,skolem0002(i2003_11_14_17_15_26245)!=X238|rf(i2003_11_14_17_15_26245,X238),inference(resolution,[status(thm)],[c109, c134])).
% 0.40/0.60 cnf(c5,axiom,X152!=X151|X153!=X150|~rf1(X152,X153)|rf1(X151,X150),theory(equality)).
% 0.40/0.60 cnf(c141,plain,i2003_11_14_17_15_26245!=X236|skolem0001(i2003_11_14_17_15_26245)!=X237|rf1(X236,X237),inference(resolution,[status(thm)],[c5, c131])).
% 0.40/0.60 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.40/0.60 fof(c104,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(A,C))|rf1(B,C))))),inference(fof_nnf,[status(thm)],[rf1_substitution_1])).
% 0.40/0.60 fof(c105,plain,(![X68]:(![X69]:(![X70]:((X68!=X69|~rf1(X68,X70))|rf1(X69,X70))))),inference(variable_rename,[status(thm)],[c104])).
% 0.40/0.60 cnf(c106,plain,X210!=X211|~rf1(X210,X212)|rf1(X211,X212),inference(split_conjunct,[status(thm)],[c105])).
% 0.40/0.60 cnf(c154,plain,i2003_11_14_17_15_26245!=X235|rf1(X235,skolem0001(i2003_11_14_17_15_26245)),inference(resolution,[status(thm)],[c106, c131])).
% 0.40/0.60 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.40/0.60 fof(c101,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.40/0.60 fof(c102,plain,(![X65]:(![X66]:(![X67]:((X65!=X66|~rf1(X67,X65))|rf1(X67,X66))))),inference(variable_rename,[status(thm)],[c101])).
% 0.40/0.60 cnf(c103,plain,X207!=X208|~rf1(X209,X207)|rf1(X209,X208),inference(split_conjunct,[status(thm)],[c102])).
% 0.40/0.60 cnf(c153,plain,skolem0001(i2003_11_14_17_15_26245)!=X234|rf1(i2003_11_14_17_15_26245,X234),inference(resolution,[status(thm)],[c103, c131])).
% 0.40/0.60 cnf(c4,axiom,X138!=X137|X139!=X136|~rf(X138,X139)|rf(X137,X136),theory(equality)).
% 0.40/0.60 cnf(c140,plain,i2003_11_14_17_15_26245!=X233|skolem0002(i2003_11_14_17_15_26245)!=X232|rf(X233,X232),inference(resolution,[status(thm)],[c4, c134])).
% 0.40/0.60 fof(rinvF_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvF(A,C))=>rinvF(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvF_substitution_1)).
% 0.40/0.61 fof(c98,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.40/0.61 fof(c99,plain,(![X62]:(![X63]:(![X64]:((X62!=X63|~rinvF(X62,X64))|rinvF(X63,X64))))),inference(variable_rename,[status(thm)],[c98])).
% 0.40/0.61 cnf(c100,plain,X201!=X202|~rinvF(X201,X200)|rinvF(X202,X200),inference(split_conjunct,[status(thm)],[c99])).
% 0.40/0.61 cnf(c152,plain,skolem0002(i2003_11_14_17_15_26245)!=X231|rinvF(X231,i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c100, c135])).
% 0.40/0.61 fof(rinvF_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvF(C,A))=>rinvF(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvF_substitution_2)).
% 0.40/0.61 fof(c95,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.40/0.61 fof(c96,plain,(![X59]:(![X60]:(![X61]:((X59!=X60|~rinvF(X61,X59))|rinvF(X61,X60))))),inference(variable_rename,[status(thm)],[c95])).
% 0.40/0.61 cnf(c97,plain,X198!=X197|~rinvF(X199,X198)|rinvF(X199,X197),inference(split_conjunct,[status(thm)],[c96])).
% 0.40/0.61 cnf(c151,plain,i2003_11_14_17_15_26245!=X230|rinvF(skolem0002(i2003_11_14_17_15_26245),X230),inference(resolution,[status(thm)],[c97, c135])).
% 0.40/0.61 fof(rinvF1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvF1(A,C))=>rinvF1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvF1_substitution_1)).
% 0.40/0.61 fof(c92,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF1(A,C))|rinvF1(B,C))))),inference(fof_nnf,[status(thm)],[rinvF1_substitution_1])).
% 0.40/0.61 fof(c93,plain,(![X56]:(![X57]:(![X58]:((X56!=X57|~rinvF1(X56,X58))|rinvF1(X57,X58))))),inference(variable_rename,[status(thm)],[c92])).
% 0.40/0.61 cnf(c94,plain,X194!=X196|~rinvF1(X194,X195)|rinvF1(X196,X195),inference(split_conjunct,[status(thm)],[c93])).
% 0.40/0.61 cnf(c150,plain,skolem0001(i2003_11_14_17_15_26245)!=X229|rinvF1(X229,i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c94, c132])).
% 0.40/0.61 cnf(c57,plain,~rf1(X227,X228)|cp(X228)|~rf(X227,X226)|~cp(X226)|cSatisfiable(X227),inference(split_conjunct,[status(thm)],[c52])).
% 0.40/0.61 fof(rinvF1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvF1(C,A))=>rinvF1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvF1_substitution_2)).
% 0.40/0.61 fof(c89,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF1(C,A))|rinvF1(C,B))))),inference(fof_nnf,[status(thm)],[rinvF1_substitution_2])).
% 0.40/0.61 fof(c90,plain,(![X53]:(![X54]:(![X55]:((X53!=X54|~rinvF1(X55,X53))|rinvF1(X55,X54))))),inference(variable_rename,[status(thm)],[c89])).
% 0.40/0.61 cnf(c91,plain,X191!=X192|~rinvF1(X193,X191)|rinvF1(X193,X192),inference(split_conjunct,[status(thm)],[c90])).
% 0.40/0.61 cnf(c149,plain,i2003_11_14_17_15_26245!=X225|rinvF1(skolem0001(i2003_11_14_17_15_26245),X225),inference(resolution,[status(thm)],[c91, c132])).
% 0.40/0.61 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.40/0.61 fof(c43,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.40/0.61 fof(c44,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c43])).
% 0.40/0.61 cnf(c45,plain,~rf(X172,X171)|~rf(X172,X170)|X171=X170,inference(split_conjunct,[status(thm)],[c44])).
% 0.40/0.61 cnf(c147,plain,~rf(i2003_11_14_17_15_26245,X224)|X224=skolem0002(i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c45, c134])).
% 0.40/0.61 cnf(c9,axiom,X222!=X221|X223!=X220|~rs(X222,X223)|rs(X221,X220),theory(equality)).
% 0.40/0.61 fof(axiom_4,axiom,(![X]:(![Y]:(![Z]:((rf1(X,Y)&rf1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.40/0.61 fof(c40,plain,(![X]:(![Y]:(![Z]:((~rf1(X,Y)|~rf1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.40/0.61 fof(c41,plain,(![X21]:(![X22]:(![X23]:((~rf1(X21,X22)|~rf1(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c40])).
% 0.40/0.61 cnf(c42,plain,~rf1(X161,X163)|~rf1(X161,X162)|X163=X162,inference(split_conjunct,[status(thm)],[c41])).
% 0.40/0.61 cnf(c144,plain,~rf1(i2003_11_14_17_15_26245,X219)|X219=skolem0001(i2003_11_14_17_15_26245),inference(resolution,[status(thm)],[c42, c131])).
% 0.40/0.61 cnf(c8,axiom,X205!=X204|X206!=X203|~rinvS(X205,X206)|rinvS(X204,X203),theory(equality)).
% 0.40/0.61 fof(rinvS_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvS(A,C))=>rinvS(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvS_substitution_1)).
% 0.40/0.61 fof(c86,plain,(![A]:(![B]:(![C]:((A!=B|~rinvS(A,C))|rinvS(B,C))))),inference(fof_nnf,[status(thm)],[rinvS_substitution_1])).
% 0.40/0.61 fof(c87,plain,(![X50]:(![X51]:(![X52]:((X50!=X51|~rinvS(X50,X52))|rinvS(X51,X52))))),inference(variable_rename,[status(thm)],[c86])).
% 0.40/0.61 cnf(c88,plain,X190!=X189|~rinvS(X190,X188)|rinvS(X189,X188),inference(split_conjunct,[status(thm)],[c87])).
% 0.40/0.61 fof(rinvS_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvS(C,A))=>rinvS(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvS_substitution_2)).
% 0.40/0.61 fof(c83,plain,(![A]:(![B]:(![C]:((A!=B|~rinvS(C,A))|rinvS(C,B))))),inference(fof_nnf,[status(thm)],[rinvS_substitution_2])).
% 0.40/0.61 fof(c84,plain,(![X47]:(![X48]:(![X49]:((X47!=X48|~rinvS(X49,X47))|rinvS(X49,X48))))),inference(variable_rename,[status(thm)],[c83])).
% 0.40/0.61 cnf(c85,plain,X181!=X182|~rinvS(X183,X181)|rinvS(X183,X182),inference(split_conjunct,[status(thm)],[c84])).
% 0.40/0.61 fof(rs_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rs(A,C))=>rs(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rs_substitution_1)).
% 0.40/0.61 fof(c80,plain,(![A]:(![B]:(![C]:((A!=B|~rs(A,C))|rs(B,C))))),inference(fof_nnf,[status(thm)],[rs_substitution_1])).
% 0.40/0.61 fof(c81,plain,(![X44]:(![X45]:(![X46]:((X44!=X45|~rs(X44,X46))|rs(X45,X46))))),inference(variable_rename,[status(thm)],[c80])).
% 0.40/0.61 cnf(c82,plain,X180!=X178|~rs(X180,X179)|rs(X178,X179),inference(split_conjunct,[status(thm)],[c81])).
% 0.40/0.61 fof(rs_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rs(C,A))=>rs(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rs_substitution_2)).
% 0.40/0.61 fof(c77,plain,(![A]:(![B]:(![C]:((A!=B|~rs(C,A))|rs(C,B))))),inference(fof_nnf,[status(thm)],[rs_substitution_2])).
% 0.40/0.61 fof(c78,plain,(![X41]:(![X42]:(![X43]:((X41!=X42|~rs(X43,X41))|rs(X43,X42))))),inference(variable_rename,[status(thm)],[c77])).
% 0.40/0.61 cnf(c79,plain,X176!=X175|~rs(X177,X176)|rs(X177,X175),inference(split_conjunct,[status(thm)],[c78])).
% 0.40/0.61 fof(axiom_8,axiom,(![X]:(![Y]:(![Z]:((rs(X,Y)&rs(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.40/0.61 fof(c19,plain,(![X]:(![Y]:(![Z]:((~rs(X,Y)|~rs(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.40/0.61 fof(c20,plain,(![X6]:(![X7]:(![X8]:((~rs(X6,X7)|~rs(X6,X8))|X7=X8)))),inference(variable_rename,[status(thm)],[c19])).
% 0.40/0.61 cnf(c21,plain,~rs(X157,X156)|~rs(X157,X158)|X156=X158,inference(split_conjunct,[status(thm)],[c20])).
% 0.40/0.61 cnf(c11,axiom,X134!=X133|~xsd_string(X134)|xsd_string(X133),theory(equality)).
% 0.40/0.61 cnf(c10,axiom,X131!=X130|~xsd_integer(X131)|xsd_integer(X130),theory(equality)).
% 0.40/0.61 cnf(c3,axiom,X128!=X127|~cp(X128)|cp(X127),theory(equality)).
% 0.40/0.61 cnf(c56,plain,~cSatisfiable(X117)|cp(skolem0002(X117)),inference(split_conjunct,[status(thm)],[c52])).
% 0.40/0.61 cnf(c130,plain,cp(skolem0002(i2003_11_14_17_15_26245)),inference(resolution,[status(thm)],[c56, c18])).
% 0.40/0.61 cnf(c54,plain,~cSatisfiable(X116)|~cp(skolem0001(X116)),inference(split_conjunct,[status(thm)],[c52])).
% 0.40/0.61 cnf(c0,axiom,X112!=X111|~cSatisfiable(X112)|cSatisfiable(X111),theory(equality)).
% 0.40/0.61 cnf(c38,plain,~rinvF(X110,X109)|rf(X109,X110),inference(split_conjunct,[status(thm)],[c37])).
% 0.40/0.61 cnf(c32,plain,~rinvF1(X105,X106)|rf1(X106,X105),inference(split_conjunct,[status(thm)],[c31])).
% 0.40/0.61 fof(axiom_7,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.40/0.61 fof(c22,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.40/0.61 fof(c23,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.40/0.61 fof(c25,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvS(X9,X10)|rs(X10,X9))&(~rs(X12,X11)|rinvS(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X9]:(![X10]:(~rinvS(X9,X10)|rs(X10,X9))))&(![X11]:(![X12]:(~rs(X12,X11)|rinvS(X11,X12))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.40/0.61 cnf(c27,plain,~rs(X103,X104)|rinvS(X104,X103),inference(split_conjunct,[status(thm)],[c25])).
% 0.40/0.61 cnf(c26,plain,~rinvS(X102,X101)|rs(X101,X102),inference(split_conjunct,[status(thm)],[c25])).
% 0.40/0.61 cnf(transitivity,axiom,X99!=X100|X100!=X98|X99=X98,theory(equality)).
% 0.40/0.61 fof(axiom_10,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.40/0.61 fof(c15,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.40/0.61 fof(c16,plain,(![X4]:(![X5]:(~rs(X4,X5)|rf(X4,X5)))),inference(variable_rename,[status(thm)],[c15])).
% 0.40/0.61 cnf(c17,plain,~rs(X96,X97)|rf(X96,X97),inference(split_conjunct,[status(thm)],[c16])).
% 0.40/0.61 fof(axiom_11,axiom,(![X]:(![Y]:(rs(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.40/0.61 fof(c12,plain,(![X]:(![Y]:(~rs(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.40/0.61 fof(c13,plain,(![X2]:(![X3]:(~rs(X2,X3)|rf1(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.40/0.61 cnf(c14,plain,~rs(X94,X95)|rf1(X94,X95),inference(split_conjunct,[status(thm)],[c13])).
% 0.40/0.61 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.40/0.61 fof(c58,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.40/0.61 fof(c59,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c58])).
% 0.40/0.61 fof(c60,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 0.40/0.61 fof(c62,plain,(![X33]:(![X34]:((~xsd_string(X33)|~xsd_integer(X33))&(xsd_integer(X34)|xsd_string(X34))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X33]:(~xsd_string(X33)|~xsd_integer(X33)))&(![X34]:(xsd_integer(X34)|xsd_string(X34)))),inference(variable_rename,[status(thm)],[c60])).])).
% 0.40/0.61 cnf(c64,plain,xsd_integer(X92)|xsd_string(X92),inference(split_conjunct,[status(thm)],[c62])).
% 0.40/0.61 cnf(symmetry,axiom,X89!=X90|X90=X89,theory(equality)).
% 0.40/0.61 cnf(c63,plain,~xsd_string(X88)|~xsd_integer(X88),inference(split_conjunct,[status(thm)],[c62])).
% 0.40/0.61 cnf(reflexivity,axiom,X87=X87,theory(equality)).
% 0.40/0.61 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.40/0.61 fof(c65,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.40/0.61 fof(c66,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c65])).
% 0.40/0.61 fof(c68,plain,(![X35]:(![X36]:(cowlThing(X35)&~cowlNothing(X36)))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X35]:cowlThing(X35))&(![X36]:~cowlNothing(X36))),inference(variable_rename,[status(thm)],[c66])).])).
% 0.40/0.61 cnf(c70,plain,~cowlNothing(X86),inference(split_conjunct,[status(thm)],[c68])).
% 0.40/0.61 cnf(c69,plain,cowlThing(X85),inference(split_conjunct,[status(thm)],[c68])).
% 0.40/0.61 % SZS output end Saturation
% 0.40/0.61
% 0.40/0.61 % Initial clauses : 54
% 0.40/0.61 % Processed clauses : 65
% 0.40/0.61 % Factors computed : 4
% 0.40/0.61 % Resolvents computed: 43
% 0.40/0.61 % Tautologies deleted: 7
% 0.40/0.61 % Forward subsumed : 29
% 0.40/0.61 % Backward subsumed : 0
% 0.40/0.61 % -------- CPU Time ---------
% 0.40/0.61 % User time : 0.245 s
% 0.40/0.61 % System time : 0.019 s
% 0.40/0.61 % Total time : 0.264 s
%------------------------------------------------------------------------------