%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS044+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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.47s 0.64s
% Output : Saturation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : KRS044+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n014.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:05:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.47/0.64 % Version: 1.5
% 0.47/0.64 % SZS status Satisfiable
% 0.47/0.64 % SZS output start Saturation
% 0.47/0.64 cnf(c5,axiom,X158!=X161|X159!=X160|~ra_Px1(X158,X159)|ra_Px1(X161,X160),theory(equality)).
% 0.47/0.64 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.47/0.64 fof(c55,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.47/0.64 fof(c56,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c55])).
% 0.47/0.64 fof(c57,plain,((![X31]:(~cp(X31)|(![X32]:~ra_Px1(X31,X32))))&(![X33]:((?[X34]:ra_Px1(X33,X34))|cp(X33)))),inference(variable_rename,[status(thm)],[c56])).
% 0.47/0.64 fof(c59,plain,(![X31]:(![X32]:(![X33]:((~cp(X31)|~ra_Px1(X31,X32))&(ra_Px1(X33,skolem0002(X33))|cp(X33)))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,((![X31]:(~cp(X31)|(![X32]:~ra_Px1(X31,X32))))&(![X33]:(ra_Px1(X33,skolem0002(X33))|cp(X33)))),inference(skolemize,[status(esa)],[c57])).])).
% 0.47/0.64 cnf(c61,plain,ra_Px1(X146,skolem0002(X146))|cp(X146),inference(split_conjunct,[status(thm)],[c59])).
% 0.47/0.64 cnf(c60,plain,~cp(X112)|~ra_Px1(X112,X113),inference(split_conjunct,[status(thm)],[c59])).
% 0.47/0.64 fof(axiom_11,axiom,cSatisfiable(i2003_11_14_17_16_1832),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.47/0.64 cnf(c20,plain,cSatisfiable(i2003_11_14_17_16_1832),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.47/0.64 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:(rf1(X,Y)&cpxcomp(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.47/0.64 fof(c62,plain,(![X]:((~cSatisfiable(X)|((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:(rf1(X,Y)&cpxcomp(Y)))))&(((![Y]:(~rf(X,Y)|~cp(Y)))|(![Y]:(~rf1(X,Y)|~cpxcomp(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.47/0.64 fof(c63,plain,((![X]:(~cSatisfiable(X)|((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:(rf1(X,Y)&cpxcomp(Y))))))&(![X]:(((![Y]:(~rf(X,Y)|~cp(Y)))|(![Y]:(~rf1(X,Y)|~cpxcomp(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c62])).
% 0.47/0.64 fof(c64,plain,((![X35]:(~cSatisfiable(X35)|((?[X36]:(rf(X35,X36)&cp(X36)))&(?[X37]:(rf1(X35,X37)&cpxcomp(X37))))))&(![X38]:(((![X39]:(~rf(X38,X39)|~cp(X39)))|(![X40]:(~rf1(X38,X40)|~cpxcomp(X40))))|cSatisfiable(X38)))),inference(variable_rename,[status(thm)],[c63])).
% 0.47/0.64 fof(c66,plain,(![X35]:(![X38]:(![X39]:(![X40]:((~cSatisfiable(X35)|((rf(X35,skolem0003(X35))&cp(skolem0003(X35)))&(rf1(X35,skolem0004(X35))&cpxcomp(skolem0004(X35)))))&(((~rf(X38,X39)|~cp(X39))|(~rf1(X38,X40)|~cpxcomp(X40)))|cSatisfiable(X38))))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X35]:(~cSatisfiable(X35)|((rf(X35,skolem0003(X35))&cp(skolem0003(X35)))&(rf1(X35,skolem0004(X35))&cpxcomp(skolem0004(X35))))))&(![X38]:(((![X39]:(~rf(X38,X39)|~cp(X39)))|(![X40]:(~rf1(X38,X40)|~cpxcomp(X40))))|cSatisfiable(X38)))),inference(skolemize,[status(esa)],[c64])).])).
% 0.47/0.64 fof(c67,plain,(![X35]:(![X38]:(![X39]:(![X40]:((((~cSatisfiable(X35)|rf(X35,skolem0003(X35)))&(~cSatisfiable(X35)|cp(skolem0003(X35))))&((~cSatisfiable(X35)|rf1(X35,skolem0004(X35)))&(~cSatisfiable(X35)|cpxcomp(skolem0004(X35)))))&(((~rf(X38,X39)|~cp(X39))|(~rf1(X38,X40)|~cpxcomp(X40)))|cSatisfiable(X38))))))),inference(distribute,[status(thm)],[c66])).
% 0.47/0.64 cnf(c71,plain,~cSatisfiable(X139)|cpxcomp(skolem0004(X139)),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.64 cnf(c155,plain,cpxcomp(skolem0004(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c71, c20])).
% 0.47/0.64 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.47/0.64 fof(c48,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.47/0.64 fof(c49,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c48])).
% 0.47/0.64 fof(c50,plain,((![X27]:(~cpxcomp(X27)|(?[X28]:ra_Px1(X27,X28))))&(![X29]:((![X30]:~ra_Px1(X29,X30))|cpxcomp(X29)))),inference(variable_rename,[status(thm)],[c49])).
% 0.47/0.64 fof(c52,plain,(![X27]:(![X29]:(![X30]:((~cpxcomp(X27)|ra_Px1(X27,skolem0001(X27)))&(~ra_Px1(X29,X30)|cpxcomp(X29)))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X27]:(~cpxcomp(X27)|ra_Px1(X27,skolem0001(X27))))&(![X29]:((![X30]:~ra_Px1(X29,X30))|cpxcomp(X29)))),inference(skolemize,[status(esa)],[c50])).])).
% 0.47/0.64 cnf(c53,plain,~cpxcomp(X145)|ra_Px1(X145,skolem0001(X145)),inference(split_conjunct,[status(thm)],[c52])).
% 0.47/0.64 cnf(c156,plain,ra_Px1(skolem0004(i2003_11_14_17_16_1832),skolem0001(skolem0004(i2003_11_14_17_16_1832))),inference(resolution,[status(thm)],[c53, c155])).
% 0.47/0.64 cnf(c197,plain,~cp(skolem0004(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c156, c60])).
% 0.47/0.64 cnf(c201,plain,ra_Px1(skolem0004(i2003_11_14_17_16_1832),skolem0002(skolem0004(i2003_11_14_17_16_1832))),inference(resolution,[status(thm)],[c197, c61])).
% 0.47/0.64 cnf(c219,plain,skolem0004(i2003_11_14_17_16_1832)!=X321|skolem0002(skolem0004(i2003_11_14_17_16_1832))!=X320|ra_Px1(X321,X320),inference(resolution,[status(thm)],[c201, c5])).
% 0.47/0.64 fof(ra_Px1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&ra_Px1(A,C))=>ra_Px1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ra_Px1_substitution_1)).
% 0.47/0.64 fof(c131,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(A,C))|ra_Px1(B,C))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_1])).
% 0.47/0.64 fof(c132,plain,(![X88]:(![X89]:(![X90]:((X88!=X89|~ra_Px1(X88,X90))|ra_Px1(X89,X90))))),inference(variable_rename,[status(thm)],[c131])).
% 0.47/0.64 cnf(c133,plain,X264!=X262|~ra_Px1(X264,X263)|ra_Px1(X262,X263),inference(split_conjunct,[status(thm)],[c132])).
% 0.47/0.64 cnf(c222,plain,skolem0004(i2003_11_14_17_16_1832)!=X318|ra_Px1(X318,skolem0002(skolem0004(i2003_11_14_17_16_1832))),inference(resolution,[status(thm)],[c201, c133])).
% 0.47/0.64 fof(ra_Px1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&ra_Px1(C,A))=>ra_Px1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ra_Px1_substitution_2)).
% 0.47/0.64 fof(c128,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(C,A))|ra_Px1(C,B))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_2])).
% 0.47/0.64 fof(c129,plain,(![X85]:(![X86]:(![X87]:((X85!=X86|~ra_Px1(X87,X85))|ra_Px1(X87,X86))))),inference(variable_rename,[status(thm)],[c128])).
% 0.47/0.64 cnf(c130,plain,X261!=X260|~ra_Px1(X259,X261)|ra_Px1(X259,X260),inference(split_conjunct,[status(thm)],[c129])).
% 0.47/0.64 cnf(c221,plain,skolem0002(skolem0004(i2003_11_14_17_16_1832))!=X316|ra_Px1(skolem0004(i2003_11_14_17_16_1832),X316),inference(resolution,[status(thm)],[c201, c130])).
% 0.47/0.64 cnf(c199,plain,skolem0004(i2003_11_14_17_16_1832)!=X315|ra_Px1(X315,skolem0001(skolem0004(i2003_11_14_17_16_1832))),inference(resolution,[status(thm)],[c156, c133])).
% 0.47/0.64 cnf(c196,plain,skolem0004(i2003_11_14_17_16_1832)!=X314|skolem0001(skolem0004(i2003_11_14_17_16_1832))!=X313|ra_Px1(X314,X313),inference(resolution,[status(thm)],[c156, c5])).
% 0.47/0.64 cnf(c198,plain,skolem0001(skolem0004(i2003_11_14_17_16_1832))!=X312|ra_Px1(skolem0004(i2003_11_14_17_16_1832),X312),inference(resolution,[status(thm)],[c156, c130])).
% 0.47/0.64 cnf(c194,plain,X304!=X305|ra_Px1(X305,skolem0002(X304))|cp(X304),inference(resolution,[status(thm)],[c133, c61])).
% 0.47/0.64 cnf(c54,plain,~ra_Px1(X110,X111)|cpxcomp(X110),inference(split_conjunct,[status(thm)],[c52])).
% 0.47/0.64 cnf(c157,plain,cp(X147)|cpxcomp(X147),inference(resolution,[status(thm)],[c61, c54])).
% 0.47/0.64 cnf(c159,plain,cp(X157)|ra_Px1(X157,skolem0001(X157)),inference(resolution,[status(thm)],[c157, c53])).
% 0.47/0.64 cnf(c193,plain,X303!=X302|ra_Px1(X302,skolem0001(X303))|cp(X303),inference(resolution,[status(thm)],[c133, c159])).
% 0.47/0.64 cnf(c192,plain,skolem0002(X299)!=X300|ra_Px1(X299,X300)|cp(X299),inference(resolution,[status(thm)],[c130, c61])).
% 0.47/0.64 fof(axiom_8,axiom,(![X]:(![Y]:(rinvF1(X,Y)<=>rf1(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.47/0.64 fof(c30,plain,(![X]:(![Y]:((~rinvF1(X,Y)|rf1(Y,X))&(~rf1(Y,X)|rinvF1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.47/0.64 fof(c31,plain,((![X]:(![Y]:(~rinvF1(X,Y)|rf1(Y,X))))&(![X]:(![Y]:(~rf1(Y,X)|rinvF1(X,Y))))),inference(shift_quantors,[status(thm)],[c30])).
% 0.47/0.64 fof(c33,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rinvF1(X13,X14)|rf1(X14,X13))&(~rf1(X16,X15)|rinvF1(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X13]:(![X14]:(~rinvF1(X13,X14)|rf1(X14,X13))))&(![X15]:(![X16]:(~rf1(X16,X15)|rinvF1(X15,X16))))),inference(variable_rename,[status(thm)],[c31])).])).
% 0.47/0.64 cnf(c35,plain,~rf1(X131,X130)|rinvF1(X130,X131),inference(split_conjunct,[status(thm)],[c33])).
% 0.47/0.64 cnf(c70,plain,~cSatisfiable(X153)|rf1(X153,skolem0004(X153)),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.64 cnf(c164,plain,rf1(i2003_11_14_17_16_1832,skolem0004(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c70, c20])).
% 0.47/0.64 cnf(c166,plain,rinvF1(skolem0004(i2003_11_14_17_16_1832),i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c164, c35])).
% 0.47/0.64 cnf(c9,axiom,X214!=X217|X215!=X216|~rinvF1(X214,X215)|rinvF1(X217,X216),theory(equality)).
% 0.47/0.64 cnf(c182,plain,skolem0004(i2003_11_14_17_16_1832)!=X296|i2003_11_14_17_16_1832!=X295|rinvF1(X296,X295),inference(resolution,[status(thm)],[c9, c166])).
% 0.47/0.64 cnf(c191,plain,skolem0001(X294)!=X293|ra_Px1(X294,X293)|cp(X294),inference(resolution,[status(thm)],[c130, c159])).
% 0.47/0.64 fof(axiom_7,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.47/0.64 fof(c36,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.47/0.64 fof(c37,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c36])).
% 0.47/0.64 fof(c39,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~rinvF(X17,X18)|rf(X18,X17))&(~rf(X20,X19)|rinvF(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X17]:(![X18]:(~rinvF(X17,X18)|rf(X18,X17))))&(![X19]:(![X20]:(~rf(X20,X19)|rinvF(X19,X20))))),inference(variable_rename,[status(thm)],[c37])).])).
% 0.47/0.64 cnf(c41,plain,~rf(X134,X135)|rinvF(X135,X134),inference(split_conjunct,[status(thm)],[c39])).
% 0.47/0.64 cnf(c68,plain,~cSatisfiable(X149)|rf(X149,skolem0003(X149)),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.64 cnf(c160,plain,rf(i2003_11_14_17_16_1832,skolem0003(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c68, c20])).
% 0.47/0.64 cnf(c162,plain,rinvF(skolem0003(i2003_11_14_17_16_1832),i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c160, c41])).
% 0.47/0.64 cnf(c8,axiom,X197!=X200|X198!=X199|~rinvF(X197,X198)|rinvF(X200,X199),theory(equality)).
% 0.47/0.64 cnf(c177,plain,skolem0003(i2003_11_14_17_16_1832)!=X288|i2003_11_14_17_16_1832!=X289|rinvF(X288,X289),inference(resolution,[status(thm)],[c8, c162])).
% 0.47/0.64 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.47/0.64 fof(c125,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.47/0.64 fof(c126,plain,(![X82]:(![X83]:(![X84]:((X82!=X83|~rf(X82,X84))|rf(X83,X84))))),inference(variable_rename,[status(thm)],[c125])).
% 0.47/0.64 cnf(c127,plain,X256!=X257|~rf(X256,X258)|rf(X257,X258),inference(split_conjunct,[status(thm)],[c126])).
% 0.47/0.64 cnf(c190,plain,i2003_11_14_17_16_1832!=X287|rf(X287,skolem0003(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c127, c160])).
% 0.47/0.64 cnf(c7,axiom,X182!=X185|X183!=X184|~rf1(X182,X183)|rf1(X185,X184),theory(equality)).
% 0.47/0.64 cnf(c175,plain,i2003_11_14_17_16_1832!=X286|skolem0004(i2003_11_14_17_16_1832)!=X285|rf1(X286,X285),inference(resolution,[status(thm)],[c7, c164])).
% 0.47/0.64 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.47/0.64 fof(c122,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.47/0.64 fof(c123,plain,(![X79]:(![X80]:(![X81]:((X79!=X80|~rf(X81,X79))|rf(X81,X80))))),inference(variable_rename,[status(thm)],[c122])).
% 0.47/0.64 cnf(c124,plain,X249!=X250|~rf(X251,X249)|rf(X251,X250),inference(split_conjunct,[status(thm)],[c123])).
% 0.47/0.64 cnf(c189,plain,skolem0003(i2003_11_14_17_16_1832)!=X284|rf(i2003_11_14_17_16_1832,X284),inference(resolution,[status(thm)],[c124, c160])).
% 0.47/0.64 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.47/0.64 fof(c119,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(A,C))|rf1(B,C))))),inference(fof_nnf,[status(thm)],[rf1_substitution_1])).
% 0.47/0.64 fof(c120,plain,(![X76]:(![X77]:(![X78]:((X76!=X77|~rf1(X76,X78))|rf1(X77,X78))))),inference(variable_rename,[status(thm)],[c119])).
% 0.47/0.64 cnf(c121,plain,X248!=X246|~rf1(X248,X247)|rf1(X246,X247),inference(split_conjunct,[status(thm)],[c120])).
% 0.47/0.64 cnf(c188,plain,i2003_11_14_17_16_1832!=X283|rf1(X283,skolem0004(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c121, c164])).
% 0.47/0.64 cnf(c6,axiom,X169!=X172|X170!=X171|~rf(X169,X170)|rf(X172,X171),theory(equality)).
% 0.47/0.64 cnf(c174,plain,i2003_11_14_17_16_1832!=X281|skolem0003(i2003_11_14_17_16_1832)!=X282|rf(X281,X282),inference(resolution,[status(thm)],[c6, c160])).
% 0.47/0.64 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.47/0.64 fof(c116,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.47/0.64 fof(c117,plain,(![X73]:(![X74]:(![X75]:((X73!=X74|~rf1(X75,X73))|rf1(X75,X74))))),inference(variable_rename,[status(thm)],[c116])).
% 0.47/0.64 cnf(c118,plain,X243!=X245|~rf1(X244,X243)|rf1(X244,X245),inference(split_conjunct,[status(thm)],[c117])).
% 0.47/0.64 cnf(c187,plain,skolem0004(i2003_11_14_17_16_1832)!=X280|rf1(i2003_11_14_17_16_1832,X280),inference(resolution,[status(thm)],[c118, c164])).
% 0.47/0.64 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.47/0.64 fof(c113,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.47/0.64 fof(c114,plain,(![X70]:(![X71]:(![X72]:((X70!=X71|~rinvF(X70,X72))|rinvF(X71,X72))))),inference(variable_rename,[status(thm)],[c113])).
% 0.47/0.64 cnf(c115,plain,X242!=X241|~rinvF(X242,X240)|rinvF(X241,X240),inference(split_conjunct,[status(thm)],[c114])).
% 0.47/0.64 cnf(c186,plain,skolem0003(i2003_11_14_17_16_1832)!=X279|rinvF(X279,i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c115, c162])).
% 0.47/0.64 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.47/0.64 fof(c110,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.47/0.64 fof(c111,plain,(![X67]:(![X68]:(![X69]:((X67!=X68|~rinvF(X69,X67))|rinvF(X69,X68))))),inference(variable_rename,[status(thm)],[c110])).
% 0.47/0.64 cnf(c112,plain,X237!=X239|~rinvF(X238,X237)|rinvF(X238,X239),inference(split_conjunct,[status(thm)],[c111])).
% 0.47/0.64 cnf(c185,plain,i2003_11_14_17_16_1832!=X278|rinvF(skolem0003(i2003_11_14_17_16_1832),X278),inference(resolution,[status(thm)],[c112, c162])).
% 0.47/0.64 cnf(c171,plain,X276!=X277|skolem0002(X276)!=X275|ra_Px1(X277,X275)|cp(X276),inference(resolution,[status(thm)],[c5, c61])).
% 0.47/0.64 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.47/0.64 fof(c107,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF1(A,C))|rinvF1(B,C))))),inference(fof_nnf,[status(thm)],[rinvF1_substitution_1])).
% 0.47/0.64 fof(c108,plain,(![X64]:(![X65]:(![X66]:((X64!=X65|~rinvF1(X64,X66))|rinvF1(X65,X66))))),inference(variable_rename,[status(thm)],[c107])).
% 0.47/0.64 cnf(c109,plain,X231!=X232|~rinvF1(X231,X230)|rinvF1(X232,X230),inference(split_conjunct,[status(thm)],[c108])).
% 0.47/0.64 cnf(c184,plain,skolem0004(i2003_11_14_17_16_1832)!=X274|rinvF1(X274,i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c109, c166])).
% 0.47/0.64 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.47/0.64 fof(c104,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF1(C,A))|rinvF1(C,B))))),inference(fof_nnf,[status(thm)],[rinvF1_substitution_2])).
% 0.47/0.64 fof(c105,plain,(![X61]:(![X62]:(![X63]:((X61!=X62|~rinvF1(X63,X61))|rinvF1(X63,X62))))),inference(variable_rename,[status(thm)],[c104])).
% 0.47/0.64 cnf(c106,plain,X227!=X229|~rinvF1(X228,X227)|rinvF1(X228,X229),inference(split_conjunct,[status(thm)],[c105])).
% 0.47/0.64 cnf(c183,plain,i2003_11_14_17_16_1832!=X273|rinvF1(skolem0004(i2003_11_14_17_16_1832),X273),inference(resolution,[status(thm)],[c106, c166])).
% 0.47/0.64 cnf(c170,plain,X271!=X272|skolem0001(X271)!=X270|ra_Px1(X272,X270)|cp(X271),inference(resolution,[status(thm)],[c5, c159])).
% 0.48/0.64 fof(axiom_5,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.48/0.64 fof(c45,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.48/0.64 fof(c46,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c45])).
% 0.48/0.64 cnf(c47,plain,~rf(X208,X207)|~rf(X208,X206)|X207=X206,inference(split_conjunct,[status(thm)],[c46])).
% 0.48/0.64 cnf(c181,plain,~rf(i2003_11_14_17_16_1832,X269)|X269=skolem0003(i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c47, c160])).
% 0.48/0.64 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rf1(X,Y)&rf1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.64 fof(c42,plain,(![X]:(![Y]:(![Z]:((~rf1(X,Y)|~rf1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.64 fof(c43,plain,(![X21]:(![X22]:(![X23]:((~rf1(X21,X22)|~rf1(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c42])).
% 0.48/0.64 cnf(c44,plain,~rf1(X201,X203)|~rf1(X201,X202)|X203=X202,inference(split_conjunct,[status(thm)],[c43])).
% 0.48/0.64 cnf(c179,plain,~rf1(i2003_11_14_17_16_1832,X268)|X268=skolem0004(i2003_11_14_17_16_1832),inference(resolution,[status(thm)],[c44, c164])).
% 0.48/0.64 cnf(c72,plain,~rf(X265,X267)|~cp(X267)|~rf1(X265,X266)|~cpxcomp(X266)|cSatisfiable(X265),inference(split_conjunct,[status(thm)],[c67])).
% 0.48/0.64 cnf(c11,axiom,X252!=X255|X253!=X254|~rs(X252,X253)|rs(X255,X254),theory(equality)).
% 0.48/0.64 cnf(c10,axiom,X233!=X236|X234!=X235|~rinvS(X233,X234)|rinvS(X236,X235),theory(equality)).
% 0.48/0.64 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.48/0.64 fof(c101,plain,(![A]:(![B]:(![C]:((A!=B|~rinvS(A,C))|rinvS(B,C))))),inference(fof_nnf,[status(thm)],[rinvS_substitution_1])).
% 0.48/0.64 fof(c102,plain,(![X58]:(![X59]:(![X60]:((X58!=X59|~rinvS(X58,X60))|rinvS(X59,X60))))),inference(variable_rename,[status(thm)],[c101])).
% 0.48/0.64 cnf(c103,plain,X224!=X225|~rinvS(X224,X226)|rinvS(X225,X226),inference(split_conjunct,[status(thm)],[c102])).
% 0.48/0.64 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.48/0.64 fof(c98,plain,(![A]:(![B]:(![C]:((A!=B|~rinvS(C,A))|rinvS(C,B))))),inference(fof_nnf,[status(thm)],[rinvS_substitution_2])).
% 0.48/0.64 fof(c99,plain,(![X55]:(![X56]:(![X57]:((X55!=X56|~rinvS(X57,X55))|rinvS(X57,X56))))),inference(variable_rename,[status(thm)],[c98])).
% 0.48/0.64 cnf(c100,plain,X222!=X221|~rinvS(X223,X222)|rinvS(X223,X221),inference(split_conjunct,[status(thm)],[c99])).
% 0.48/0.64 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.48/0.64 fof(c95,plain,(![A]:(![B]:(![C]:((A!=B|~rs(A,C))|rs(B,C))))),inference(fof_nnf,[status(thm)],[rs_substitution_1])).
% 0.48/0.64 fof(c96,plain,(![X52]:(![X53]:(![X54]:((X52!=X53|~rs(X52,X54))|rs(X53,X54))))),inference(variable_rename,[status(thm)],[c95])).
% 0.48/0.64 cnf(c97,plain,X220!=X218|~rs(X220,X219)|rs(X218,X219),inference(split_conjunct,[status(thm)],[c96])).
% 0.48/0.64 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.48/0.64 fof(c92,plain,(![A]:(![B]:(![C]:((A!=B|~rs(C,A))|rs(C,B))))),inference(fof_nnf,[status(thm)],[rs_substitution_2])).
% 0.48/0.64 fof(c93,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rs(X51,X49))|rs(X51,X50))))),inference(variable_rename,[status(thm)],[c92])).
% 0.48/0.64 cnf(c94,plain,X213!=X211|~rs(X212,X213)|rs(X212,X211),inference(split_conjunct,[status(thm)],[c93])).
% 0.48/0.64 fof(axiom_10,axiom,(![X]:(![Y]:(![Z]:((rs(X,Y)&rs(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.48/0.64 fof(c21,plain,(![X]:(![Y]:(![Z]:((~rs(X,Y)|~rs(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.48/0.64 fof(c22,plain,(![X6]:(![X7]:(![X8]:((~rs(X6,X7)|~rs(X6,X8))|X7=X8)))),inference(variable_rename,[status(thm)],[c21])).
% 0.48/0.64 cnf(c23,plain,~rs(X194,X193)|~rs(X194,X192)|X193=X192,inference(split_conjunct,[status(thm)],[c22])).
% 0.48/0.64 cnf(c13,axiom,X167!=X168|~xsd_string(X167)|xsd_string(X168),theory(equality)).
% 0.48/0.64 cnf(c12,axiom,X164!=X165|~xsd_integer(X164)|xsd_integer(X165),theory(equality)).
% 0.48/0.64 cnf(c4,axiom,X154!=X155|~cpxcomp(X154)|cpxcomp(X155),theory(equality)).
% 0.48/0.64 cnf(c3,axiom,X150!=X151|~cp(X150)|cp(X151),theory(equality)).
% 0.48/0.64 cnf(c69,plain,~cSatisfiable(X136)|cp(skolem0003(X136)),inference(split_conjunct,[status(thm)],[c67])).
% 0.48/0.64 cnf(c154,plain,cp(skolem0003(i2003_11_14_17_16_1832)),inference(resolution,[status(thm)],[c69, c20])).
% 0.48/0.64 cnf(c40,plain,~rinvF(X133,X132)|rf(X132,X133),inference(split_conjunct,[status(thm)],[c39])).
% 0.48/0.64 cnf(c0,axiom,X127!=X128|~cSatisfiable(X127)|cSatisfiable(X128),theory(equality)).
% 0.48/0.64 cnf(c34,plain,~rinvF1(X125,X126)|rf1(X126,X125),inference(split_conjunct,[status(thm)],[c33])).
% 0.48/0.64 fof(axiom_9,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.48/0.64 fof(c24,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.48/0.64 fof(c25,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c24])).
% 0.48/0.64 fof(c27,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvS(X9,X10)|rs(X10,X9))&(~rs(X12,X11)|rinvS(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X9]:(![X10]:(~rinvS(X9,X10)|rs(X10,X9))))&(![X11]:(![X12]:(~rs(X12,X11)|rinvS(X11,X12))))),inference(variable_rename,[status(thm)],[c25])).])).
% 0.48/0.64 cnf(c29,plain,~rs(X123,X124)|rinvS(X124,X123),inference(split_conjunct,[status(thm)],[c27])).
% 0.48/0.64 cnf(c28,plain,~rinvS(X121,X122)|rs(X122,X121),inference(split_conjunct,[status(thm)],[c27])).
% 0.48/0.64 fof(axiom_12,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_12)).
% 0.48/0.64 fof(c17,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 0.48/0.64 fof(c18,plain,(![X4]:(![X5]:(~rs(X4,X5)|rf(X4,X5)))),inference(variable_rename,[status(thm)],[c17])).
% 0.48/0.64 cnf(c19,plain,~rs(X120,X119)|rf(X120,X119),inference(split_conjunct,[status(thm)],[c18])).
% 0.48/0.64 fof(axiom_13,axiom,(![X]:(![Y]:(rs(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_13)).
% 0.48/0.64 fof(c14,plain,(![X]:(![Y]:(~rs(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_13])).
% 0.48/0.64 fof(c15,plain,(![X2]:(![X3]:(~rs(X2,X3)|rf1(X2,X3)))),inference(variable_rename,[status(thm)],[c14])).
% 0.48/0.64 cnf(c16,plain,~rs(X118,X117)|rf1(X118,X117),inference(split_conjunct,[status(thm)],[c15])).
% 0.48/0.64 cnf(transitivity,axiom,X115!=X114|X114!=X116|X115=X116,theory(equality)).
% 0.48/0.64 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.48/0.64 fof(c73,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.48/0.64 fof(c74,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c73])).
% 0.48/0.64 fof(c75,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c74])).
% 0.48/0.64 fof(c77,plain,(![X41]:(![X42]:((~xsd_string(X41)|~xsd_integer(X41))&(xsd_integer(X42)|xsd_string(X42))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,((![X41]:(~xsd_string(X41)|~xsd_integer(X41)))&(![X42]:(xsd_integer(X42)|xsd_string(X42)))),inference(variable_rename,[status(thm)],[c75])).])).
% 0.48/0.64 cnf(c79,plain,xsd_integer(X108)|xsd_string(X108),inference(split_conjunct,[status(thm)],[c77])).
% 0.48/0.64 cnf(symmetry,axiom,X106!=X105|X105=X106,theory(equality)).
% 0.48/0.64 cnf(c78,plain,~xsd_string(X104)|~xsd_integer(X104),inference(split_conjunct,[status(thm)],[c77])).
% 0.48/0.64 cnf(reflexivity,axiom,X103=X103,theory(equality)).
% 0.48/0.64 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.48/0.64 fof(c80,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.48/0.64 fof(c81,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c80])).
% 0.48/0.64 fof(c83,plain,(![X43]:(![X44]:(cowlThing(X43)&~cowlNothing(X44)))),inference(shift_quantors,[status(thm)],[fof(c82,plain,((![X43]:cowlThing(X43))&(![X44]:~cowlNothing(X44))),inference(variable_rename,[status(thm)],[c81])).])).
% 0.48/0.64 cnf(c85,plain,~cowlNothing(X102),inference(split_conjunct,[status(thm)],[c83])).
% 0.48/0.64 cnf(c84,plain,cowlThing(X101),inference(split_conjunct,[status(thm)],[c83])).
% 0.48/0.64 % SZS output end Saturation
% 0.48/0.64
% 0.48/0.64 % Initial clauses : 63
% 0.48/0.64 % Processed clauses : 91
% 0.48/0.64 % Factors computed : 4
% 0.48/0.64 % Resolvents computed: 82
% 0.48/0.64 % Tautologies deleted: 10
% 0.48/0.64 % Forward subsumed : 48
% 0.48/0.64 % Backward subsumed : 0
% 0.48/0.64 % -------- CPU Time ---------
% 0.48/0.64 % User time : 0.273 s
% 0.48/0.64 % System time : 0.012 s
% 0.48/0.64 % Total time : 0.285 s
%------------------------------------------------------------------------------