%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS042+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:32 EDT 2024
% Result : Satisfiable 0.62s 0.79s
% Output : Saturation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS042+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n009.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:04:52 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.62/0.79 % Version: 1.5
% 0.62/0.79 % SZS status Satisfiable
% 0.62/0.79 % SZS output start Saturation
% 0.62/0.79 cnf(c18,axiom,X314!=X317|X316!=X315|~rrxa(X314,X316)|rrxa(X317,X315),theory(equality)).
% 0.62/0.79 fof(axiom_17,axiom,(![X]:(![Y]:(rrx3a(X,Y)=>rrxa(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_17)).
% 0.62/0.79 fof(c30,plain,(![X]:(![Y]:(~rrx3a(X,Y)|rrxa(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_17])).
% 0.62/0.79 fof(c31,plain,(![X8]:(![X9]:(~rrx3a(X8,X9)|rrxa(X8,X9)))),inference(variable_rename,[status(thm)],[c30])).
% 0.62/0.79 cnf(c32,plain,~rrx3a(X171,X172)|rrxa(X171,X172),inference(split_conjunct,[status(thm)],[c31])).
% 0.62/0.79 fof(axiom_6,axiom,(![X]:(ca_Cx1xcomp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.62/0.79 fof(c61,plain,(![X]:((~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.62/0.79 fof(c62,plain,((![X]:(~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 0.62/0.79 fof(c63,plain,((![X33]:(~ca_Cx1xcomp(X33)|(![X34]:~ra_Px1(X33,X34))))&(![X35]:((?[X36]:ra_Px1(X35,X36))|ca_Cx1xcomp(X35)))),inference(variable_rename,[status(thm)],[c62])).
% 0.62/0.79 fof(c65,plain,(![X33]:(![X34]:(![X35]:((~ca_Cx1xcomp(X33)|~ra_Px1(X33,X34))&(ra_Px1(X35,skolem0001(X35))|ca_Cx1xcomp(X35)))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X33]:(~ca_Cx1xcomp(X33)|(![X34]:~ra_Px1(X33,X34))))&(![X35]:(ra_Px1(X35,skolem0001(X35))|ca_Cx1xcomp(X35)))),inference(skolemize,[status(esa)],[c63])).])).
% 0.62/0.79 cnf(c67,plain,ra_Px1(X196,skolem0001(X196))|ca_Cx1xcomp(X196),inference(split_conjunct,[status(thm)],[c65])).
% 0.62/0.79 fof(axiom_5,axiom,(![X]:(ca_Cx1xcomp(X)<=>(?[Y]:(rrx3a(X,Y)&ca_Ax2(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.62/0.79 fof(c68,plain,(![X]:((~ca_Cx1xcomp(X)|(?[Y]:(rrx3a(X,Y)&ca_Ax2(Y))))&((![Y]:(~rrx3a(X,Y)|~ca_Ax2(Y)))|ca_Cx1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.62/0.79 fof(c69,plain,((![X]:(~ca_Cx1xcomp(X)|(?[Y]:(rrx3a(X,Y)&ca_Ax2(Y)))))&(![X]:((![Y]:(~rrx3a(X,Y)|~ca_Ax2(Y)))|ca_Cx1xcomp(X)))),inference(shift_quantors,[status(thm)],[c68])).
% 0.62/0.79 fof(c70,plain,((![X37]:(~ca_Cx1xcomp(X37)|(?[X38]:(rrx3a(X37,X38)&ca_Ax2(X38)))))&(![X39]:((![X40]:(~rrx3a(X39,X40)|~ca_Ax2(X40)))|ca_Cx1xcomp(X39)))),inference(variable_rename,[status(thm)],[c69])).
% 0.62/0.79 fof(c72,plain,(![X37]:(![X39]:(![X40]:((~ca_Cx1xcomp(X37)|(rrx3a(X37,skolem0002(X37))&ca_Ax2(skolem0002(X37))))&((~rrx3a(X39,X40)|~ca_Ax2(X40))|ca_Cx1xcomp(X39)))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,((![X37]:(~ca_Cx1xcomp(X37)|(rrx3a(X37,skolem0002(X37))&ca_Ax2(skolem0002(X37)))))&(![X39]:((![X40]:(~rrx3a(X39,X40)|~ca_Ax2(X40)))|ca_Cx1xcomp(X39)))),inference(skolemize,[status(esa)],[c70])).])).
% 0.62/0.79 fof(c73,plain,(![X37]:(![X39]:(![X40]:(((~ca_Cx1xcomp(X37)|rrx3a(X37,skolem0002(X37)))&(~ca_Cx1xcomp(X37)|ca_Ax2(skolem0002(X37))))&((~rrx3a(X39,X40)|~ca_Ax2(X40))|ca_Cx1xcomp(X39)))))),inference(distribute,[status(thm)],[c72])).
% 0.62/0.79 cnf(c74,plain,~ca_Cx1xcomp(X208)|rrx3a(X208,skolem0002(X208)),inference(split_conjunct,[status(thm)],[c73])).
% 0.62/0.79 cnf(c232,plain,rrx3a(X417,skolem0002(X417))|ra_Px1(X417,skolem0001(X417)),inference(resolution,[status(thm)],[c74, c67])).
% 0.62/0.79 cnf(c363,plain,ra_Px1(X477,skolem0001(X477))|rrxa(X477,skolem0002(X477)),inference(resolution,[status(thm)],[c232, c32])).
% 0.62/0.79 cnf(c448,plain,ra_Px1(X753,skolem0001(X753))|X753!=X752|skolem0002(X753)!=X751|rrxa(X752,X751),inference(resolution,[status(thm)],[c363, c18])).
% 0.62/0.79 cnf(c8,axiom,X216!=X219|X218!=X217|~ra_Px1(X216,X218)|ra_Px1(X219,X217),theory(equality)).
% 0.62/0.79 cnf(c443,plain,rrxa(X749,skolem0002(X749))|X749!=X748|skolem0001(X749)!=X750|ra_Px1(X748,X750),inference(resolution,[status(thm)],[c363, c8])).
% 0.62/0.79 cnf(c11,axiom,X241!=X244|X243!=X242|~rrx1a(X241,X243)|rrx1a(X244,X242),theory(equality)).
% 0.62/0.79 fof(axiom_13,axiom,(![X]:(![Y]:(rrx3a(X,Y)=>rrx1a(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_13)).
% 0.62/0.79 fof(c42,plain,(![X]:(![Y]:(~rrx3a(X,Y)|rrx1a(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_13])).
% 0.62/0.79 fof(c43,plain,(![X16]:(![X17]:(~rrx3a(X16,X17)|rrx1a(X16,X17)))),inference(variable_rename,[status(thm)],[c42])).
% 0.62/0.79 cnf(c44,plain,~rrx3a(X182,X183)|rrx1a(X182,X183),inference(split_conjunct,[status(thm)],[c43])).
% 0.62/0.79 cnf(c359,plain,ra_Px1(X471,skolem0001(X471))|rrx1a(X471,skolem0002(X471)),inference(resolution,[status(thm)],[c232, c44])).
% 0.62/0.79 cnf(c437,plain,ra_Px1(X744,skolem0001(X744))|X744!=X743|skolem0002(X744)!=X742|rrx1a(X743,X742),inference(resolution,[status(thm)],[c359, c11])).
% 0.62/0.79 cnf(c434,plain,rrx1a(X733,skolem0002(X733))|X733!=X732|skolem0001(X733)!=X734|ra_Px1(X732,X734),inference(resolution,[status(thm)],[c359, c8])).
% 0.62/0.79 fof(rrxa_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrxa(A,C))=>rrxa(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrxa_substitution_1)).
% 0.62/0.79 fof(c126,plain,(![A]:(![B]:(![C]:((A!=B|~rrxa(A,C))|rrxa(B,C))))),inference(fof_nnf,[status(thm)],[rrxa_substitution_1])).
% 0.62/0.79 fof(c127,plain,(![X64]:(![X65]:(![X66]:((X64!=X65|~rrxa(X64,X66))|rrxa(X65,X66))))),inference(variable_rename,[status(thm)],[c126])).
% 0.62/0.79 cnf(c128,plain,X353!=X352|~rrxa(X353,X351)|rrxa(X352,X351),inference(split_conjunct,[status(thm)],[c127])).
% 0.62/0.79 cnf(c447,plain,ra_Px1(X716,skolem0001(X716))|X716!=X715|rrxa(X715,skolem0002(X716)),inference(resolution,[status(thm)],[c363, c128])).
% 0.62/0.79 fof(rrxa_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrxa(C,A))=>rrxa(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrxa_substitution_2)).
% 0.62/0.79 fof(c123,plain,(![A]:(![B]:(![C]:((A!=B|~rrxa(C,A))|rrxa(C,B))))),inference(fof_nnf,[status(thm)],[rrxa_substitution_2])).
% 0.62/0.79 fof(c124,plain,(![X61]:(![X62]:(![X63]:((X61!=X62|~rrxa(X63,X61))|rrxa(X63,X62))))),inference(variable_rename,[status(thm)],[c123])).
% 0.62/0.79 cnf(c125,plain,X349!=X350|~rrxa(X348,X349)|rrxa(X348,X350),inference(split_conjunct,[status(thm)],[c124])).
% 0.62/0.79 cnf(c446,plain,ra_Px1(X712,skolem0001(X712))|skolem0002(X712)!=X713|rrxa(X712,X713),inference(resolution,[status(thm)],[c363, c125])).
% 0.62/0.79 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.62/0.79 fof(c186,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(A,C))|ra_Px1(B,C))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_1])).
% 0.62/0.79 fof(c187,plain,(![X124]:(![X125]:(![X126]:((X124!=X125|~ra_Px1(X124,X126))|ra_Px1(X125,X126))))),inference(variable_rename,[status(thm)],[c186])).
% 0.62/0.79 cnf(c188,plain,X415!=X414|~ra_Px1(X415,X416)|ra_Px1(X414,X416),inference(split_conjunct,[status(thm)],[c187])).
% 0.62/0.79 cnf(c444,plain,rrxa(X710,skolem0002(X710))|X710!=X709|ra_Px1(X709,skolem0001(X710)),inference(resolution,[status(thm)],[c363, c188])).
% 0.62/0.79 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.62/0.79 fof(c183,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(C,A))|ra_Px1(C,B))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_2])).
% 0.62/0.79 fof(c184,plain,(![X121]:(![X122]:(![X123]:((X121!=X122|~ra_Px1(X123,X121))|ra_Px1(X123,X122))))),inference(variable_rename,[status(thm)],[c183])).
% 0.62/0.79 cnf(c185,plain,X412!=X411|~ra_Px1(X413,X412)|ra_Px1(X413,X411),inference(split_conjunct,[status(thm)],[c184])).
% 0.62/0.79 cnf(c441,plain,rrxa(X707,skolem0002(X707))|skolem0001(X707)!=X706|ra_Px1(X707,X706),inference(resolution,[status(thm)],[c363, c185])).
% 0.62/0.79 fof(axiom_4,axiom,(![X]:(ca_Cx1(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.62/0.79 fof(c77,plain,(![X]:((~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.62/0.79 fof(c78,plain,((![X]:(~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(shift_quantors,[status(thm)],[c77])).
% 0.62/0.79 fof(c79,plain,((![X41]:(~ca_Cx1(X41)|(?[X42]:ra_Px1(X41,X42))))&(![X43]:((![X44]:~ra_Px1(X43,X44))|ca_Cx1(X43)))),inference(variable_rename,[status(thm)],[c78])).
% 0.62/0.79 fof(c81,plain,(![X41]:(![X43]:(![X44]:((~ca_Cx1(X41)|ra_Px1(X41,skolem0003(X41)))&(~ra_Px1(X43,X44)|ca_Cx1(X43)))))),inference(shift_quantors,[status(thm)],[fof(c80,plain,((![X41]:(~ca_Cx1(X41)|ra_Px1(X41,skolem0003(X41))))&(![X43]:((![X44]:~ra_Px1(X43,X44))|ca_Cx1(X43)))),inference(skolemize,[status(esa)],[c79])).])).
% 0.62/0.80 cnf(c82,plain,~ca_Cx1(X209)|ra_Px1(X209,skolem0003(X209)),inference(split_conjunct,[status(thm)],[c81])).
% 0.62/0.80 cnf(c83,plain,~ra_Px1(X161,X160)|ca_Cx1(X161),inference(split_conjunct,[status(thm)],[c81])).
% 0.62/0.80 cnf(c225,plain,ca_Cx1xcomp(X200)|ca_Cx1(X200),inference(resolution,[status(thm)],[c67, c83])).
% 0.62/0.80 cnf(c233,plain,rrx3a(X221,skolem0002(X221))|ca_Cx1(X221),inference(resolution,[status(thm)],[c74, c225])).
% 0.62/0.80 cnf(c257,plain,ca_Cx1(X234)|rrxa(X234,skolem0002(X234)),inference(resolution,[status(thm)],[c233, c32])).
% 0.62/0.80 cnf(c266,plain,rrxa(X429,skolem0002(X429))|ra_Px1(X429,skolem0003(X429)),inference(resolution,[status(thm)],[c257, c82])).
% 0.62/0.80 cnf(c397,plain,rrxa(X704,skolem0002(X704))|X704!=X703|skolem0003(X704)!=X705|ra_Px1(X703,X705),inference(resolution,[status(thm)],[c266, c8])).
% 0.62/0.80 fof(rrx1a_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx1a(C,A))=>rrx1a(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx1a_substitution_2)).
% 0.62/0.80 fof(c165,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1a(C,A))|rrx1a(C,B))))),inference(fof_nnf,[status(thm)],[rrx1a_substitution_2])).
% 0.62/0.80 fof(c166,plain,(![X103]:(![X104]:(![X105]:((X103!=X104|~rrx1a(X105,X103))|rrx1a(X105,X104))))),inference(variable_rename,[status(thm)],[c165])).
% 0.62/0.80 cnf(c167,plain,X393!=X395|~rrx1a(X394,X393)|rrx1a(X394,X395),inference(split_conjunct,[status(thm)],[c166])).
% 0.62/0.80 cnf(c439,plain,ra_Px1(X701,skolem0001(X701))|skolem0002(X701)!=X700|rrx1a(X701,X700),inference(resolution,[status(thm)],[c359, c167])).
% 0.62/0.80 fof(rrx1a_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx1a(A,C))=>rrx1a(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx1a_substitution_1)).
% 0.62/0.80 fof(c168,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1a(A,C))|rrx1a(B,C))))),inference(fof_nnf,[status(thm)],[rrx1a_substitution_1])).
% 0.62/0.80 fof(c169,plain,(![X106]:(![X107]:(![X108]:((X106!=X107|~rrx1a(X106,X108))|rrx1a(X107,X108))))),inference(variable_rename,[status(thm)],[c168])).
% 0.62/0.80 cnf(c170,plain,X398!=X396|~rrx1a(X398,X397)|rrx1a(X396,X397),inference(split_conjunct,[status(thm)],[c169])).
% 0.62/0.80 cnf(c438,plain,ra_Px1(X697,skolem0001(X697))|X697!=X698|rrx1a(X698,skolem0002(X697)),inference(resolution,[status(thm)],[c359, c170])).
% 0.62/0.80 cnf(c394,plain,ra_Px1(X695,skolem0003(X695))|X695!=X694|skolem0002(X695)!=X693|rrxa(X694,X693),inference(resolution,[status(thm)],[c266, c18])).
% 0.62/0.80 cnf(c435,plain,rrx1a(X692,skolem0002(X692))|X692!=X691|ra_Px1(X691,skolem0001(X692)),inference(resolution,[status(thm)],[c359, c188])).
% 0.62/0.80 cnf(c432,plain,rrx1a(X689,skolem0002(X689))|skolem0001(X689)!=X688|ra_Px1(X689,X688),inference(resolution,[status(thm)],[c359, c185])).
% 0.62/0.80 cnf(c398,plain,rrxa(X686,skolem0002(X686))|X686!=X685|ra_Px1(X685,skolem0003(X686)),inference(resolution,[status(thm)],[c266, c188])).
% 0.62/0.80 cnf(c256,plain,ca_Cx1(X229)|rrx1a(X229,skolem0002(X229)),inference(resolution,[status(thm)],[c233, c44])).
% 0.62/0.80 cnf(c265,plain,rrx1a(X424,skolem0002(X424))|ra_Px1(X424,skolem0003(X424)),inference(resolution,[status(thm)],[c256, c82])).
% 0.62/0.80 cnf(c386,plain,rrx1a(X683,skolem0002(X683))|X683!=X682|skolem0003(X683)!=X684|ra_Px1(X682,X684),inference(resolution,[status(thm)],[c265, c8])).
% 0.62/0.80 cnf(c395,plain,rrxa(X680,skolem0002(X680))|skolem0003(X680)!=X679|ra_Px1(X680,X679),inference(resolution,[status(thm)],[c266, c185])).
% 0.62/0.80 cnf(c393,plain,ra_Px1(X677,skolem0003(X677))|X677!=X676|rrxa(X676,skolem0002(X677)),inference(resolution,[status(thm)],[c266, c128])).
% 0.62/0.80 cnf(c381,plain,ra_Px1(X674,skolem0003(X674))|X674!=X673|skolem0002(X674)!=X672|rrx1a(X673,X672),inference(resolution,[status(thm)],[c265, c11])).
% 0.62/0.80 cnf(c392,plain,ra_Px1(X670,skolem0003(X670))|skolem0002(X670)!=X671|rrxa(X670,X671),inference(resolution,[status(thm)],[c266, c125])).
% 0.62/0.80 cnf(c387,plain,rrx1a(X668,skolem0002(X668))|X668!=X667|ra_Px1(X667,skolem0003(X668)),inference(resolution,[status(thm)],[c265, c188])).
% 0.62/0.80 cnf(c384,plain,rrx1a(X665,skolem0002(X665))|skolem0003(X665)!=X664|ra_Px1(X665,X664),inference(resolution,[status(thm)],[c265, c185])).
% 0.62/0.80 cnf(c258,plain,rrx3a(X420,skolem0002(X420))|ra_Px1(X420,skolem0003(X420)),inference(resolution,[status(thm)],[c233, c82])).
% 0.62/0.80 cnf(c378,plain,rrx3a(X662,skolem0002(X662))|X662!=X661|skolem0003(X662)!=X663|ra_Px1(X661,X663),inference(resolution,[status(thm)],[c258, c8])).
% 0.62/0.80 cnf(c383,plain,ra_Px1(X659,skolem0003(X659))|skolem0002(X659)!=X658|rrx1a(X659,X658),inference(resolution,[status(thm)],[c265, c167])).
% 0.62/0.80 cnf(c382,plain,ra_Px1(X655,skolem0003(X655))|X655!=X656|rrx1a(X656,skolem0002(X655)),inference(resolution,[status(thm)],[c265, c170])).
% 0.62/0.80 cnf(c15,axiom,X287!=X290|X289!=X288|~rrx3a(X287,X289)|rrx3a(X290,X288),theory(equality)).
% 0.62/0.80 cnf(c374,plain,ra_Px1(X653,skolem0003(X653))|X653!=X652|skolem0002(X653)!=X651|rrx3a(X652,X651),inference(resolution,[status(thm)],[c258, c15])).
% 0.62/0.80 cnf(c379,plain,rrx3a(X650,skolem0002(X650))|X650!=X649|ra_Px1(X649,skolem0003(X650)),inference(resolution,[status(thm)],[c258, c188])).
% 0.62/0.80 cnf(c376,plain,rrx3a(X647,skolem0002(X647))|skolem0003(X647)!=X646|ra_Px1(X647,X646),inference(resolution,[status(thm)],[c258, c185])).
% 0.62/0.80 fof(rrx3a_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx3a(A,C))=>rrx3a(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx3a_substitution_1)).
% 0.62/0.80 fof(c144,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3a(A,C))|rrx3a(B,C))))),inference(fof_nnf,[status(thm)],[rrx3a_substitution_1])).
% 0.62/0.80 fof(c145,plain,(![X82]:(![X83]:(![X84]:((X82!=X83|~rrx3a(X82,X84))|rrx3a(X83,X84))))),inference(variable_rename,[status(thm)],[c144])).
% 0.62/0.80 cnf(c146,plain,X373!=X374|~rrx3a(X373,X372)|rrx3a(X374,X372),inference(split_conjunct,[status(thm)],[c145])).
% 0.62/0.80 cnf(c373,plain,ra_Px1(X644,skolem0003(X644))|X644!=X643|rrx3a(X643,skolem0002(X644)),inference(resolution,[status(thm)],[c258, c146])).
% 0.62/0.80 cnf(c366,plain,rrx3a(X641,skolem0002(X641))|X641!=X640|skolem0001(X641)!=X642|ra_Px1(X640,X642),inference(resolution,[status(thm)],[c232, c8])).
% 0.62/0.80 fof(axiom_9,axiom,(![X]:(![Y]:(![Z]:((rrx3a(X,Y)&rrx3a(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.62/0.80 fof(c52,plain,(![X]:(![Y]:(![Z]:((~rrx3a(X,Y)|~rrx3a(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.62/0.80 fof(c53,plain,(![X24]:(![X25]:(![X26]:((~rrx3a(X24,X25)|~rrx3a(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c52])).
% 0.62/0.80 cnf(c54,plain,~rrx3a(X335,X333)|~rrx3a(X335,X334)|X333=X334,inference(split_conjunct,[status(thm)],[c53])).
% 0.62/0.80 cnf(c372,plain,ra_Px1(X637,skolem0003(X637))|~rrx3a(X637,X638)|X638=skolem0002(X637),inference(resolution,[status(thm)],[c258, c54])).
% 0.62/0.80 fof(rrx3a_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx3a(C,A))=>rrx3a(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx3a_substitution_2)).
% 0.62/0.80 fof(c141,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3a(C,A))|rrx3a(C,B))))),inference(fof_nnf,[status(thm)],[rrx3a_substitution_2])).
% 0.62/0.80 fof(c142,plain,(![X79]:(![X80]:(![X81]:((X79!=X80|~rrx3a(X81,X79))|rrx3a(X81,X80))))),inference(variable_rename,[status(thm)],[c141])).
% 0.62/0.80 cnf(c143,plain,X371!=X369|~rrx3a(X370,X371)|rrx3a(X370,X369),inference(split_conjunct,[status(thm)],[c142])).
% 0.62/0.80 cnf(c369,plain,ra_Px1(X634,skolem0003(X634))|skolem0002(X634)!=X635|rrx3a(X634,X635),inference(resolution,[status(thm)],[c258, c143])).
% 0.62/0.80 cnf(c362,plain,ra_Px1(X632,skolem0001(X632))|X632!=X631|skolem0002(X632)!=X630|rrx3a(X631,X630),inference(resolution,[status(thm)],[c232, c15])).
% 0.62/0.80 cnf(c367,plain,rrx3a(X629,skolem0002(X629))|X629!=X628|ra_Px1(X628,skolem0001(X629)),inference(resolution,[status(thm)],[c232, c188])).
% 0.62/0.80 cnf(c364,plain,rrx3a(X626,skolem0002(X626))|skolem0001(X626)!=X625|ra_Px1(X626,X625),inference(resolution,[status(thm)],[c232, c185])).
% 0.62/0.80 cnf(c361,plain,ra_Px1(X622,skolem0001(X622))|X622!=X621|rrx3a(X621,skolem0002(X622)),inference(resolution,[status(thm)],[c232, c146])).
% 0.62/0.80 cnf(c360,plain,ra_Px1(X619,skolem0001(X619))|~rrx3a(X619,X620)|X620=skolem0002(X619),inference(resolution,[status(thm)],[c232, c54])).
% 0.62/0.80 cnf(c357,plain,ra_Px1(X610,skolem0001(X610))|skolem0002(X610)!=X611|rrx3a(X610,X611),inference(resolution,[status(thm)],[c232, c143])).
% 0.62/0.80 fof(axiom_3,axiom,(![X]:(ca_Ax2(X)<=>(cc2(X)&cc1(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.62/0.80 fof(c84,plain,(![X]:((~ca_Ax2(X)|(cc2(X)&cc1(X)))&((~cc2(X)|~cc1(X))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.62/0.80 fof(c85,plain,((![X]:(~ca_Ax2(X)|(cc2(X)&cc1(X))))&(![X]:((~cc2(X)|~cc1(X))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c84])).
% 0.62/0.80 fof(c87,plain,(![X45]:(![X46]:((~ca_Ax2(X45)|(cc2(X45)&cc1(X45)))&((~cc2(X46)|~cc1(X46))|ca_Ax2(X46))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,((![X45]:(~ca_Ax2(X45)|(cc2(X45)&cc1(X45))))&(![X46]:((~cc2(X46)|~cc1(X46))|ca_Ax2(X46)))),inference(variable_rename,[status(thm)],[c85])).])).
% 0.62/0.80 fof(c88,plain,(![X45]:(![X46]:(((~ca_Ax2(X45)|cc2(X45))&(~ca_Ax2(X45)|cc1(X45)))&((~cc2(X46)|~cc1(X46))|ca_Ax2(X46))))),inference(distribute,[status(thm)],[c87])).
% 0.62/0.80 cnf(c89,plain,~ca_Ax2(X146)|cc2(X146),inference(split_conjunct,[status(thm)],[c88])).
% 0.62/0.80 cnf(c75,plain,~ca_Cx1xcomp(X184)|ca_Ax2(skolem0002(X184)),inference(split_conjunct,[status(thm)],[c73])).
% 0.62/0.80 cnf(c228,plain,ca_Cx1(X202)|ca_Ax2(skolem0002(X202)),inference(resolution,[status(thm)],[c225, c75])).
% 0.62/0.80 cnf(c229,plain,ca_Cx1(X203)|cc2(skolem0002(X203)),inference(resolution,[status(thm)],[c228, c89])).
% 0.62/0.80 cnf(c238,plain,ra_Px1(X293,skolem0003(X293))|cc2(skolem0002(X293)),inference(resolution,[status(thm)],[c82, c229])).
% 0.62/0.80 cnf(c354,plain,X601!=X600|ra_Px1(X600,skolem0003(X601))|cc2(skolem0002(X601)),inference(resolution,[status(thm)],[c188, c238])).
% 0.62/0.80 cnf(c90,plain,~ca_Ax2(X150)|cc1(X150),inference(split_conjunct,[status(thm)],[c88])).
% 0.62/0.80 cnf(c226,plain,ra_Px1(X275,skolem0001(X275))|ca_Ax2(skolem0002(X275)),inference(resolution,[status(thm)],[c67, c75])).
% 0.62/0.80 cnf(c278,plain,ra_Px1(X310,skolem0001(X310))|cc1(skolem0002(X310)),inference(resolution,[status(thm)],[c226, c90])).
% 0.62/0.80 cnf(c353,plain,X599!=X598|ra_Px1(X598,skolem0001(X599))|cc1(skolem0002(X599)),inference(resolution,[status(thm)],[c188, c278])).
% 0.62/0.80 cnf(c237,plain,ra_Px1(X286,skolem0003(X286))|ca_Ax2(skolem0002(X286)),inference(resolution,[status(thm)],[c82, c228])).
% 0.62/0.80 cnf(c352,plain,X596!=X595|ra_Px1(X595,skolem0003(X596))|ca_Ax2(skolem0002(X596)),inference(resolution,[status(thm)],[c188, c237])).
% 0.62/0.80 cnf(c277,plain,ra_Px1(X303,skolem0001(X303))|cc2(skolem0002(X303)),inference(resolution,[status(thm)],[c226, c89])).
% 0.62/0.80 cnf(c350,plain,X593!=X592|ra_Px1(X592,skolem0001(X593))|cc2(skolem0002(X593)),inference(resolution,[status(thm)],[c188, c277])).
% 0.62/0.80 cnf(c230,plain,ca_Cx1(X204)|cc1(skolem0002(X204)),inference(resolution,[status(thm)],[c228, c90])).
% 0.62/0.80 cnf(c234,plain,ra_Px1(X282,skolem0003(X282))|cc1(skolem0002(X282)),inference(resolution,[status(thm)],[c82, c230])).
% 0.62/0.80 cnf(c349,plain,X588!=X589|ra_Px1(X589,skolem0003(X588))|cc1(skolem0002(X588)),inference(resolution,[status(thm)],[c188, c234])).
% 0.62/0.80 cnf(c347,plain,X585!=X586|ra_Px1(X586,skolem0001(X585))|ca_Ax2(skolem0002(X585)),inference(resolution,[status(thm)],[c188, c226])).
% 0.62/0.80 fof(axiom_16,axiom,(![X]:(![Y]:(rrx4a(X,Y)=>rrxa(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_16)).
% 0.62/0.80 fof(c33,plain,(![X]:(![Y]:(~rrx4a(X,Y)|rrxa(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 0.62/0.80 fof(c34,plain,(![X10]:(![X11]:(~rrx4a(X10,X11)|rrxa(X10,X11)))),inference(variable_rename,[status(thm)],[c33])).
% 0.62/0.80 cnf(c35,plain,~rrx4a(X174,X173)|rrxa(X174,X173),inference(split_conjunct,[status(thm)],[c34])).
% 0.62/0.80 fof(axiom_12,axiom,cSatisfiable(i2003_11_14_17_16_10980),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.62/0.80 cnf(c45,plain,cSatisfiable(i2003_11_14_17_16_10980),inference(split_conjunct,[status(thm)],[axiom_12])).
% 0.62/0.80 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>(((?[Y]:(rrx3a(X,Y)&cc1(Y)))&ca_Cx1(X))&(?[Y]:(rrx4a(X,Y)&cc2(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.62/0.80 fof(c92,plain,(![X]:((~cSatisfiable(X)|(((?[Y]:(rrx3a(X,Y)&cc1(Y)))&ca_Cx1(X))&(?[Y]:(rrx4a(X,Y)&cc2(Y)))))&((((![Y]:(~rrx3a(X,Y)|~cc1(Y)))|~ca_Cx1(X))|(![Y]:(~rrx4a(X,Y)|~cc2(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.62/0.80 fof(c93,plain,((![X]:(~cSatisfiable(X)|(((?[Y]:(rrx3a(X,Y)&cc1(Y)))&ca_Cx1(X))&(?[Y]:(rrx4a(X,Y)&cc2(Y))))))&(![X]:((((![Y]:(~rrx3a(X,Y)|~cc1(Y)))|~ca_Cx1(X))|(![Y]:(~rrx4a(X,Y)|~cc2(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c92])).
% 0.62/0.80 fof(c94,plain,((![X47]:(~cSatisfiable(X47)|(((?[X48]:(rrx3a(X47,X48)&cc1(X48)))&ca_Cx1(X47))&(?[X49]:(rrx4a(X47,X49)&cc2(X49))))))&(![X50]:((((![X51]:(~rrx3a(X50,X51)|~cc1(X51)))|~ca_Cx1(X50))|(![X52]:(~rrx4a(X50,X52)|~cc2(X52))))|cSatisfiable(X50)))),inference(variable_rename,[status(thm)],[c93])).
% 0.62/0.80 fof(c96,plain,(![X47]:(![X50]:(![X51]:(![X52]:((~cSatisfiable(X47)|(((rrx3a(X47,skolem0004(X47))&cc1(skolem0004(X47)))&ca_Cx1(X47))&(rrx4a(X47,skolem0005(X47))&cc2(skolem0005(X47)))))&((((~rrx3a(X50,X51)|~cc1(X51))|~ca_Cx1(X50))|(~rrx4a(X50,X52)|~cc2(X52)))|cSatisfiable(X50))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X47]:(~cSatisfiable(X47)|(((rrx3a(X47,skolem0004(X47))&cc1(skolem0004(X47)))&ca_Cx1(X47))&(rrx4a(X47,skolem0005(X47))&cc2(skolem0005(X47))))))&(![X50]:((((![X51]:(~rrx3a(X50,X51)|~cc1(X51)))|~ca_Cx1(X50))|(![X52]:(~rrx4a(X50,X52)|~cc2(X52))))|cSatisfiable(X50)))),inference(skolemize,[status(esa)],[c94])).])).
% 0.62/0.80 fof(c97,plain,(![X47]:(![X50]:(![X51]:(![X52]:(((((~cSatisfiable(X47)|rrx3a(X47,skolem0004(X47)))&(~cSatisfiable(X47)|cc1(skolem0004(X47))))&(~cSatisfiable(X47)|ca_Cx1(X47)))&((~cSatisfiable(X47)|rrx4a(X47,skolem0005(X47)))&(~cSatisfiable(X47)|cc2(skolem0005(X47)))))&((((~rrx3a(X50,X51)|~cc1(X51))|~ca_Cx1(X50))|(~rrx4a(X50,X52)|~cc2(X52)))|cSatisfiable(X50))))))),inference(distribute,[status(thm)],[c96])).
% 0.62/0.80 cnf(c101,plain,~cSatisfiable(X220)|rrx4a(X220,skolem0005(X220)),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.80 cnf(c253,plain,rrx4a(i2003_11_14_17_16_10980,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c101, c45])).
% 0.62/0.80 cnf(c254,plain,rrxa(i2003_11_14_17_16_10980,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c253, c35])).
% 0.62/0.80 cnf(c309,plain,i2003_11_14_17_16_10980!=X583|skolem0005(i2003_11_14_17_16_10980)!=X582|rrxa(X583,X582),inference(resolution,[status(thm)],[c18, c254])).
% 0.62/0.80 cnf(c344,plain,skolem0003(X580)!=X579|ra_Px1(X580,X579)|cc2(skolem0002(X580)),inference(resolution,[status(thm)],[c185, c238])).
% 0.62/0.80 cnf(c343,plain,skolem0001(X577)!=X576|ra_Px1(X577,X576)|cc1(skolem0002(X577)),inference(resolution,[status(thm)],[c185, c278])).
% 0.62/0.80 cnf(c98,plain,~cSatisfiable(X215)|rrx3a(X215,skolem0004(X215)),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.80 cnf(c247,plain,rrx3a(i2003_11_14_17_16_10980,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c98, c45])).
% 0.62/0.80 cnf(c249,plain,rrxa(i2003_11_14_17_16_10980,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c247, c32])).
% 0.62/0.80 cnf(c308,plain,i2003_11_14_17_16_10980!=X574|skolem0004(i2003_11_14_17_16_10980)!=X573|rrxa(X574,X573),inference(resolution,[status(thm)],[c18, c249])).
% 0.62/0.80 cnf(c342,plain,skolem0003(X571)!=X570|ra_Px1(X571,X570)|ca_Ax2(skolem0002(X571)),inference(resolution,[status(thm)],[c185, c237])).
% 0.62/0.80 cnf(c340,plain,skolem0001(X567)!=X568|ra_Px1(X567,X568)|cc2(skolem0002(X567)),inference(resolution,[status(thm)],[c185, c277])).
% 0.62/0.80 cnf(c307,plain,X564!=X563|skolem0002(X564)!=X562|rrxa(X563,X562)|ca_Cx1(X564),inference(resolution,[status(thm)],[c18, c257])).
% 0.62/0.80 cnf(c339,plain,skolem0003(X559)!=X560|ra_Px1(X559,X560)|cc1(skolem0002(X559)),inference(resolution,[status(thm)],[c185, c234])).
% 0.62/0.80 cnf(c337,plain,skolem0001(X556)!=X557|ra_Px1(X556,X557)|ca_Ax2(skolem0002(X556)),inference(resolution,[status(thm)],[c185, c226])).
% 0.62/0.80 cnf(c305,plain,cc1(skolem0002(X547))|X547!=X546|skolem0001(X547)!=X548|ra_Px1(X546,X548),inference(resolution,[status(thm)],[c278, c8])).
% 0.62/0.80 cnf(c356,plain,X540!=X539|ra_Px1(X539,skolem0001(X540))|ca_Cx1xcomp(X540),inference(resolution,[status(thm)],[c188, c67])).
% 0.62/0.80 cnf(c17,axiom,X305!=X308|X307!=X306|~rrx4a(X305,X307)|rrx4a(X308,X306),theory(equality)).
% 0.62/0.80 cnf(c302,plain,i2003_11_14_17_16_10980!=X537|skolem0005(i2003_11_14_17_16_10980)!=X536|rrx4a(X537,X536),inference(resolution,[status(thm)],[c17, c253])).
% 0.62/0.80 cnf(c235,plain,ra_Px1(X226,skolem0003(X226))|ca_Cx1xcomp(X226),inference(resolution,[status(thm)],[c82, c225])).
% 0.62/0.80 cnf(c351,plain,X534!=X533|ra_Px1(X533,skolem0003(X534))|ca_Cx1xcomp(X534),inference(resolution,[status(thm)],[c188, c235])).
% 0.62/0.80 cnf(c346,plain,skolem0001(X531)!=X530|ra_Px1(X531,X530)|ca_Cx1xcomp(X531),inference(resolution,[status(thm)],[c185, c67])).
% 0.62/0.80 cnf(c301,plain,cc2(skolem0002(X527))|X527!=X526|skolem0001(X527)!=X528|ra_Px1(X526,X528),inference(resolution,[status(thm)],[c277, c8])).
% 0.62/0.80 cnf(c341,plain,skolem0003(X524)!=X525|ra_Px1(X524,X525)|ca_Cx1xcomp(X524),inference(resolution,[status(thm)],[c185, c235])).
% 0.62/0.80 cnf(c336,plain,X521!=X522|rrx1a(X522,skolem0002(X521))|ca_Cx1(X521),inference(resolution,[status(thm)],[c170, c256])).
% 0.62/0.80 cnf(c334,plain,skolem0002(X518)!=X519|rrx1a(X518,X519)|ca_Cx1(X518),inference(resolution,[status(thm)],[c167, c256])).
% 0.62/0.80 cnf(c295,plain,cc2(skolem0002(X516))|X516!=X515|skolem0003(X516)!=X517|ra_Px1(X515,X517),inference(resolution,[status(thm)],[c238, c8])).
% 0.62/0.80 cnf(c330,plain,X512!=X513|rrx3a(X513,skolem0002(X512))|ca_Cx1(X512),inference(resolution,[status(thm)],[c146, c233])).
% 0.62/0.80 cnf(c328,plain,skolem0002(X510)!=X509|rrx3a(X510,X509)|ca_Cx1(X510),inference(resolution,[status(thm)],[c143, c233])).
% 0.62/0.80 cnf(c292,plain,X505!=X506|skolem0002(X505)!=X507|rrx3a(X506,X507)|ca_Cx1(X505),inference(resolution,[status(thm)],[c15, c233])).
% 0.62/0.80 cnf(c321,plain,X504!=X503|rrxa(X503,skolem0002(X504))|ca_Cx1(X504),inference(resolution,[status(thm)],[c128, c257])).
% 0.62/0.80 cnf(c318,plain,skolem0002(X501)!=X500|rrxa(X501,X500)|ca_Cx1(X501),inference(resolution,[status(thm)],[c125, c257])).
% 0.62/0.80 cnf(c291,plain,i2003_11_14_17_16_10980!=X496|skolem0004(i2003_11_14_17_16_10980)!=X497|rrx3a(X496,X497),inference(resolution,[status(thm)],[c15, c247])).
% 0.62/0.80 cnf(c315,plain,~rrx3a(X494,X495)|X495=skolem0002(X494)|ca_Cx1(X494),inference(resolution,[status(thm)],[c54, c233])).
% 0.62/0.80 cnf(c288,plain,ca_Ax2(skolem0002(X488))|X488!=X487|skolem0003(X488)!=X489|ra_Px1(X487,X489),inference(resolution,[status(thm)],[c237, c8])).
% 0.62/0.80 cnf(c281,plain,cc1(skolem0002(X474))|X474!=X473|skolem0003(X474)!=X475|ra_Px1(X473,X475),inference(resolution,[status(thm)],[c234, c8])).
% 0.62/0.80 cnf(c66,plain,~ca_Cx1xcomp(X158)|~ra_Px1(X158,X159),inference(split_conjunct,[status(thm)],[c65])).
% 0.62/0.80 cnf(c100,plain,~cSatisfiable(X151)|ca_Cx1(X151),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.80 cnf(c214,plain,ca_Cx1(i2003_11_14_17_16_10980),inference(resolution,[status(thm)],[c100, c45])).
% 0.62/0.80 cnf(c236,plain,ra_Px1(i2003_11_14_17_16_10980,skolem0003(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c82, c214])).
% 0.62/0.80 cnf(c239,plain,~ca_Cx1xcomp(i2003_11_14_17_16_10980),inference(resolution,[status(thm)],[c236, c66])).
% 0.62/0.80 cnf(c241,plain,ra_Px1(i2003_11_14_17_16_10980,skolem0001(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c239, c67])).
% 0.62/0.80 cnf(c355,plain,i2003_11_14_17_16_10980!=X470|ra_Px1(X470,skolem0001(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c188, c241])).
% 0.62/0.80 cnf(c276,plain,ca_Ax2(skolem0002(X468))|X468!=X467|skolem0001(X468)!=X469|ra_Px1(X467,X469),inference(resolution,[status(thm)],[c226, c8])).
% 0.62/0.80 cnf(c348,plain,i2003_11_14_17_16_10980!=X466|ra_Px1(X466,skolem0003(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c188, c236])).
% 0.62/0.80 cnf(c345,plain,skolem0001(i2003_11_14_17_16_10980)!=X465|ra_Px1(i2003_11_14_17_16_10980,X465),inference(resolution,[status(thm)],[c185, c241])).
% 0.62/0.80 cnf(c338,plain,skolem0003(i2003_11_14_17_16_10980)!=X464|ra_Px1(i2003_11_14_17_16_10980,X464),inference(resolution,[status(thm)],[c185, c236])).
% 0.62/0.80 fof(axiom_19,axiom,(![X]:(![Y]:(rrx4a(X,Y)=>rrx2a(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_19)).
% 0.62/0.80 fof(c24,plain,(![X]:(![Y]:(~rrx4a(X,Y)|rrx2a(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_19])).
% 0.62/0.80 fof(c25,plain,(![X4]:(![X5]:(~rrx4a(X4,X5)|rrx2a(X4,X5)))),inference(variable_rename,[status(thm)],[c24])).
% 0.62/0.80 cnf(c26,plain,~rrx4a(X167,X168)|rrx2a(X167,X168),inference(split_conjunct,[status(thm)],[c25])).
% 0.62/0.80 cnf(c255,plain,rrx2a(i2003_11_14_17_16_10980,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c253, c26])).
% 0.62/0.80 cnf(c13,axiom,X269!=X272|X271!=X270|~rrx2a(X269,X271)|rrx2a(X272,X270),theory(equality)).
% 0.62/0.80 cnf(c273,plain,i2003_11_14_17_16_10980!=X463|skolem0005(i2003_11_14_17_16_10980)!=X462|rrx2a(X463,X462),inference(resolution,[status(thm)],[c13, c255])).
% 0.62/0.80 cnf(c248,plain,rrx1a(i2003_11_14_17_16_10980,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c247, c44])).
% 0.62/0.80 cnf(c335,plain,i2003_11_14_17_16_10980!=X461|rrx1a(X461,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c170, c248])).
% 0.62/0.80 cnf(c333,plain,skolem0004(i2003_11_14_17_16_10980)!=X460|rrx1a(i2003_11_14_17_16_10980,X460),inference(resolution,[status(thm)],[c167, c248])).
% 0.62/0.80 cnf(c270,plain,X457!=X459|skolem0002(X457)!=X458|rrx1a(X459,X458)|ca_Cx1(X457),inference(resolution,[status(thm)],[c11, c256])).
% 0.62/0.80 fof(rrx2a_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx2a(A,C))=>rrx2a(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx2a_substitution_1)).
% 0.62/0.80 fof(c156,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2a(A,C))|rrx2a(B,C))))),inference(fof_nnf,[status(thm)],[rrx2a_substitution_1])).
% 0.62/0.80 fof(c157,plain,(![X94]:(![X95]:(![X96]:((X94!=X95|~rrx2a(X94,X96))|rrx2a(X95,X96))))),inference(variable_rename,[status(thm)],[c156])).
% 0.62/0.80 cnf(c158,plain,X384!=X386|~rrx2a(X384,X385)|rrx2a(X386,X385),inference(split_conjunct,[status(thm)],[c157])).
% 0.62/0.80 cnf(c332,plain,i2003_11_14_17_16_10980!=X456|rrx2a(X456,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c158, c255])).
% 0.62/0.80 fof(rrx2a_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx2a(C,A))=>rrx2a(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx2a_substitution_2)).
% 0.62/0.80 fof(c153,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2a(C,A))|rrx2a(C,B))))),inference(fof_nnf,[status(thm)],[rrx2a_substitution_2])).
% 0.62/0.80 fof(c154,plain,(![X91]:(![X92]:(![X93]:((X91!=X92|~rrx2a(X93,X91))|rrx2a(X93,X92))))),inference(variable_rename,[status(thm)],[c153])).
% 0.62/0.80 cnf(c155,plain,X381!=X383|~rrx2a(X382,X381)|rrx2a(X382,X383),inference(split_conjunct,[status(thm)],[c154])).
% 0.62/0.80 cnf(c331,plain,skolem0005(i2003_11_14_17_16_10980)!=X455|rrx2a(i2003_11_14_17_16_10980,X455),inference(resolution,[status(thm)],[c155, c255])).
% 0.62/0.80 cnf(c329,plain,i2003_11_14_17_16_10980!=X454|rrx3a(X454,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c146, c247])).
% 0.62/0.80 cnf(c269,plain,i2003_11_14_17_16_10980!=X453|skolem0004(i2003_11_14_17_16_10980)!=X452|rrx1a(X453,X452),inference(resolution,[status(thm)],[c11, c248])).
% 0.62/0.80 cnf(c327,plain,skolem0004(i2003_11_14_17_16_10980)!=X451|rrx3a(i2003_11_14_17_16_10980,X451),inference(resolution,[status(thm)],[c143, c247])).
% 0.62/0.80 fof(rrx4a_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx4a(A,C))=>rrx4a(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx4a_substitution_1)).
% 0.62/0.80 fof(c132,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4a(A,C))|rrx4a(B,C))))),inference(fof_nnf,[status(thm)],[rrx4a_substitution_1])).
% 0.62/0.80 fof(c133,plain,(![X70]:(![X71]:(![X72]:((X70!=X71|~rrx4a(X70,X72))|rrx4a(X71,X72))))),inference(variable_rename,[status(thm)],[c132])).
% 0.62/0.80 cnf(c134,plain,X362!=X360|~rrx4a(X362,X361)|rrx4a(X360,X361),inference(split_conjunct,[status(thm)],[c133])).
% 0.62/0.80 cnf(c326,plain,i2003_11_14_17_16_10980!=X450|rrx4a(X450,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c134, c253])).
% 0.62/0.80 cnf(c261,plain,ca_Cx1xcomp(X448)|X448!=X447|skolem0003(X448)!=X449|ra_Px1(X447,X449),inference(resolution,[status(thm)],[c235, c8])).
% 0.62/0.80 fof(rrx4a_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx4a(C,A))=>rrx4a(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx4a_substitution_2)).
% 0.62/0.80 fof(c129,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4a(C,A))|rrx4a(C,B))))),inference(fof_nnf,[status(thm)],[rrx4a_substitution_2])).
% 0.62/0.80 fof(c130,plain,(![X67]:(![X68]:(![X69]:((X67!=X68|~rrx4a(X69,X67))|rrx4a(X69,X68))))),inference(variable_rename,[status(thm)],[c129])).
% 0.62/0.80 cnf(c131,plain,X359!=X358|~rrx4a(X357,X359)|rrx4a(X357,X358),inference(split_conjunct,[status(thm)],[c130])).
% 0.62/0.80 cnf(c325,plain,skolem0005(i2003_11_14_17_16_10980)!=X446|rrx4a(i2003_11_14_17_16_10980,X446),inference(resolution,[status(thm)],[c131, c253])).
% 0.62/0.80 cnf(c323,plain,i2003_11_14_17_16_10980!=X445|rrxa(X445,skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c128, c254])).
% 0.62/0.80 cnf(c322,plain,i2003_11_14_17_16_10980!=X444|rrxa(X444,skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c128, c249])).
% 0.62/0.80 cnf(c252,plain,X443!=X441|skolem0001(X443)!=X442|ra_Px1(X441,X442)|ca_Cx1xcomp(X443),inference(resolution,[status(thm)],[c8, c67])).
% 0.62/0.80 cnf(c320,plain,skolem0005(i2003_11_14_17_16_10980)!=X440|rrxa(i2003_11_14_17_16_10980,X440),inference(resolution,[status(thm)],[c125, c254])).
% 0.62/0.80 cnf(c319,plain,skolem0004(i2003_11_14_17_16_10980)!=X439|rrxa(i2003_11_14_17_16_10980,X439),inference(resolution,[status(thm)],[c125, c249])).
% 0.62/0.80 cnf(c251,plain,i2003_11_14_17_16_10980!=X437|skolem0003(i2003_11_14_17_16_10980)!=X438|ra_Px1(X437,X438),inference(resolution,[status(thm)],[c8, c236])).
% 0.62/0.80 cnf(c314,plain,~rrx3a(i2003_11_14_17_16_10980,X436)|X436=skolem0004(i2003_11_14_17_16_10980),inference(resolution,[status(thm)],[c54, c247])).
% 0.62/0.80 fof(axiom_11,axiom,(![X]:(![Y]:(![Z]:((rrx4a(X,Y)&rrx4a(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.62/0.80 fof(c46,plain,(![X]:(![Y]:(![Z]:((~rrx4a(X,Y)|~rrx4a(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.62/0.80 fof(c47,plain,(![X18]:(![X19]:(![X20]:((~rrx4a(X18,X19)|~rrx4a(X18,X20))|X19=X20)))),inference(variable_rename,[status(thm)],[c46])).
% 0.62/0.80 cnf(c48,plain,~rrx4a(X323,X324)|~rrx4a(X323,X325)|X324=X325,inference(split_conjunct,[status(thm)],[c47])).
% 0.62/0.80 cnf(c311,plain,~rrx4a(i2003_11_14_17_16_10980,X435)|X435=skolem0005(i2003_11_14_17_16_10980),inference(resolution,[status(thm)],[c48, c253])).
% 0.62/0.80 cnf(c399,plain,rrxa(X433,skolem0002(X433))|~ca_Cx1xcomp(X433),inference(resolution,[status(thm)],[c266, c66])).
% 0.62/0.80 cnf(c250,plain,i2003_11_14_17_16_10980!=X431|skolem0001(i2003_11_14_17_16_10980)!=X432|ra_Px1(X431,X432),inference(resolution,[status(thm)],[c8, c241])).
% 0.62/0.80 cnf(c388,plain,rrx1a(X427,skolem0002(X427))|~ca_Cx1xcomp(X427),inference(resolution,[status(thm)],[c265, c66])).
% 0.62/0.80 cnf(c99,plain,~cSatisfiable(X188)|cc1(skolem0004(X188)),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.80 cnf(c221,plain,cc1(skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c99, c45])).
% 0.62/0.80 cnf(c91,plain,~cc2(X214)|~cc1(X214)|ca_Ax2(X214),inference(split_conjunct,[status(thm)],[c88])).
% 0.62/0.80 cnf(c245,plain,~cc2(skolem0004(i2003_11_14_17_16_10980))|ca_Ax2(skolem0004(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c91, c221])).
% 0.62/0.80 fof(rrx_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx(A,C))=>rrx(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx_substitution_1)).
% 0.62/0.80 fof(c180,plain,(![A]:(![B]:(![C]:((A!=B|~rrx(A,C))|rrx(B,C))))),inference(fof_nnf,[status(thm)],[rrx_substitution_1])).
% 0.62/0.80 fof(c181,plain,(![X118]:(![X119]:(![X120]:((X118!=X119|~rrx(X118,X120))|rrx(X119,X120))))),inference(variable_rename,[status(thm)],[c180])).
% 0.62/0.80 cnf(c182,plain,X410!=X409|~rrx(X410,X408)|rrx(X409,X408),inference(split_conjunct,[status(thm)],[c181])).
% 0.62/0.80 fof(rrx_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx(C,A))=>rrx(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx_substitution_2)).
% 0.62/0.80 fof(c177,plain,(![A]:(![B]:(![C]:((A!=B|~rrx(C,A))|rrx(C,B))))),inference(fof_nnf,[status(thm)],[rrx_substitution_2])).
% 0.62/0.80 fof(c178,plain,(![X115]:(![X116]:(![X117]:((X115!=X116|~rrx(X117,X115))|rrx(X117,X116))))),inference(variable_rename,[status(thm)],[c177])).
% 0.62/0.80 cnf(c179,plain,X406!=X407|~rrx(X405,X406)|rrx(X405,X407),inference(split_conjunct,[status(thm)],[c178])).
% 0.62/0.80 fof(rrx1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx1(A,C))=>rrx1(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx1_substitution_1)).
% 0.62/0.80 fof(c174,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1(A,C))|rrx1(B,C))))),inference(fof_nnf,[status(thm)],[rrx1_substitution_1])).
% 0.62/0.80 fof(c175,plain,(![X112]:(![X113]:(![X114]:((X112!=X113|~rrx1(X112,X114))|rrx1(X113,X114))))),inference(variable_rename,[status(thm)],[c174])).
% 0.62/0.80 cnf(c176,plain,X402!=X404|~rrx1(X402,X403)|rrx1(X404,X403),inference(split_conjunct,[status(thm)],[c175])).
% 0.62/0.80 fof(rrx1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx1(C,A))=>rrx1(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx1_substitution_2)).
% 0.62/0.80 fof(c171,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1(C,A))|rrx1(C,B))))),inference(fof_nnf,[status(thm)],[rrx1_substitution_2])).
% 0.62/0.80 fof(c172,plain,(![X109]:(![X110]:(![X111]:((X109!=X110|~rrx1(X111,X109))|rrx1(X111,X110))))),inference(variable_rename,[status(thm)],[c171])).
% 0.62/0.80 cnf(c173,plain,X399!=X401|~rrx1(X400,X399)|rrx1(X400,X401),inference(split_conjunct,[status(thm)],[c172])).
% 0.62/0.80 fof(rrx2_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx2(A,C))=>rrx2(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx2_substitution_1)).
% 0.62/0.80 fof(c162,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2(A,C))|rrx2(B,C))))),inference(fof_nnf,[status(thm)],[rrx2_substitution_1])).
% 0.62/0.80 fof(c163,plain,(![X100]:(![X101]:(![X102]:((X100!=X101|~rrx2(X100,X102))|rrx2(X101,X102))))),inference(variable_rename,[status(thm)],[c162])).
% 0.62/0.80 cnf(c164,plain,X390!=X392|~rrx2(X390,X391)|rrx2(X392,X391),inference(split_conjunct,[status(thm)],[c163])).
% 0.62/0.80 fof(rrx2_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx2(C,A))=>rrx2(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx2_substitution_2)).
% 0.62/0.80 fof(c159,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2(C,A))|rrx2(C,B))))),inference(fof_nnf,[status(thm)],[rrx2_substitution_2])).
% 0.62/0.80 fof(c160,plain,(![X97]:(![X98]:(![X99]:((X97!=X98|~rrx2(X99,X97))|rrx2(X99,X98))))),inference(variable_rename,[status(thm)],[c159])).
% 0.62/0.80 cnf(c161,plain,X388!=X387|~rrx2(X389,X388)|rrx2(X389,X387),inference(split_conjunct,[status(thm)],[c160])).
% 0.62/0.80 fof(rrx3_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx3(A,C))=>rrx3(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx3_substitution_1)).
% 0.62/0.80 fof(c150,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3(A,C))|rrx3(B,C))))),inference(fof_nnf,[status(thm)],[rrx3_substitution_1])).
% 0.62/0.80 fof(c151,plain,(![X88]:(![X89]:(![X90]:((X88!=X89|~rrx3(X88,X90))|rrx3(X89,X90))))),inference(variable_rename,[status(thm)],[c150])).
% 0.62/0.80 cnf(c152,plain,X379!=X378|~rrx3(X379,X380)|rrx3(X378,X380),inference(split_conjunct,[status(thm)],[c151])).
% 0.62/0.80 fof(rrx3_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx3(C,A))=>rrx3(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx3_substitution_2)).
% 0.62/0.80 fof(c147,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3(C,A))|rrx3(C,B))))),inference(fof_nnf,[status(thm)],[rrx3_substitution_2])).
% 0.62/0.80 fof(c148,plain,(![X85]:(![X86]:(![X87]:((X85!=X86|~rrx3(X87,X85))|rrx3(X87,X86))))),inference(variable_rename,[status(thm)],[c147])).
% 0.62/0.80 cnf(c149,plain,X377!=X375|~rrx3(X376,X377)|rrx3(X376,X375),inference(split_conjunct,[status(thm)],[c148])).
% 0.62/0.80 fof(rrx4_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rrx4(A,C))=>rrx4(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx4_substitution_1)).
% 0.62/0.80 fof(c138,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4(A,C))|rrx4(B,C))))),inference(fof_nnf,[status(thm)],[rrx4_substitution_1])).
% 0.62/0.80 fof(c139,plain,(![X76]:(![X77]:(![X78]:((X76!=X77|~rrx4(X76,X78))|rrx4(X77,X78))))),inference(variable_rename,[status(thm)],[c138])).
% 0.62/0.80 cnf(c140,plain,X367!=X366|~rrx4(X367,X368)|rrx4(X366,X368),inference(split_conjunct,[status(thm)],[c139])).
% 0.62/0.80 fof(rrx4_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rrx4(C,A))=>rrx4(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rrx4_substitution_2)).
% 0.62/0.80 fof(c135,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4(C,A))|rrx4(C,B))))),inference(fof_nnf,[status(thm)],[rrx4_substitution_2])).
% 0.62/0.80 fof(c136,plain,(![X73]:(![X74]:(![X75]:((X73!=X74|~rrx4(X75,X73))|rrx4(X75,X74))))),inference(variable_rename,[status(thm)],[c135])).
% 0.62/0.80 cnf(c137,plain,X364!=X365|~rrx4(X363,X364)|rrx4(X363,X365),inference(split_conjunct,[status(thm)],[c136])).
% 0.62/0.80 cnf(c103,plain,~rrx3a(X356,X354)|~cc1(X354)|~ca_Cx1(X356)|~rrx4a(X356,X355)|~cc2(X355)|cSatisfiable(X356),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.80 fof(axiom_7,axiom,(![X]:(![Y]:(![Z]:((rrx(X,Y)&rrx(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.62/0.80 fof(c58,plain,(![X]:(![Y]:(![Z]:((~rrx(X,Y)|~rrx(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.62/0.80 fof(c59,plain,(![X30]:(![X31]:(![X32]:((~rrx(X30,X31)|~rrx(X30,X32))|X31=X32)))),inference(variable_rename,[status(thm)],[c58])).
% 0.62/0.80 cnf(c60,plain,~rrx(X344,X343)|~rrx(X344,X345)|X343=X345,inference(split_conjunct,[status(thm)],[c59])).
% 0.62/0.80 fof(axiom_8,axiom,(![X]:(![Y]:(![Z]:((rrx3(X,Y)&rrx3(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.62/0.80 fof(c55,plain,(![X]:(![Y]:(![Z]:((~rrx3(X,Y)|~rrx3(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.62/0.80 fof(c56,plain,(![X27]:(![X28]:(![X29]:((~rrx3(X27,X28)|~rrx3(X27,X29))|X28=X29)))),inference(variable_rename,[status(thm)],[c55])).
% 0.62/0.81 cnf(c57,plain,~rrx3(X340,X338)|~rrx3(X340,X339)|X338=X339,inference(split_conjunct,[status(thm)],[c56])).
% 0.62/0.81 fof(axiom_10,axiom,(![X]:(![Y]:(![Z]:((rrx4(X,Y)&rrx4(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.62/0.81 fof(c49,plain,(![X]:(![Y]:(![Z]:((~rrx4(X,Y)|~rrx4(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.62/0.81 fof(c50,plain,(![X21]:(![X22]:(![X23]:((~rrx4(X21,X22)|~rrx4(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c49])).
% 0.62/0.81 cnf(c51,plain,~rrx4(X330,X329)|~rrx4(X330,X328)|X329=X328,inference(split_conjunct,[status(thm)],[c50])).
% 0.62/0.81 cnf(c16,axiom,X296!=X299|X298!=X297|~rrx4(X296,X298)|rrx4(X299,X297),theory(equality)).
% 0.62/0.81 cnf(c293,plain,cc2(skolem0002(X294))|~ca_Cx1xcomp(X294),inference(resolution,[status(thm)],[c238, c66])).
% 0.62/0.81 cnf(c279,plain,cc1(skolem0002(X283))|~ca_Cx1xcomp(X283),inference(resolution,[status(thm)],[c234, c66])).
% 0.62/0.81 cnf(c14,axiom,X278!=X281|X280!=X279|~rrx3(X278,X280)|rrx3(X281,X279),theory(equality)).
% 0.62/0.81 cnf(c76,plain,~rrx3a(X245,X246)|~ca_Ax2(X246)|ca_Cx1xcomp(X245),inference(split_conjunct,[status(thm)],[c73])).
% 0.62/0.81 cnf(c271,plain,~ca_Ax2(skolem0004(i2003_11_14_17_16_10980))|ca_Cx1xcomp(i2003_11_14_17_16_10980),inference(resolution,[status(thm)],[c76, c247])).
% 0.62/0.81 cnf(c12,axiom,X255!=X258|X257!=X256|~rrx2(X255,X257)|rrx2(X258,X256),theory(equality)).
% 0.62/0.81 cnf(c20,axiom,X238!=X239|~xsd_string(X238)|xsd_string(X239),theory(equality)).
% 0.62/0.81 cnf(c19,axiom,X235!=X236|~xsd_integer(X235)|xsd_integer(X236),theory(equality)).
% 0.62/0.81 cnf(c10,axiom,X230!=X233|X232!=X231|~rrx1(X230,X232)|rrx1(X233,X231),theory(equality)).
% 0.62/0.81 cnf(c9,axiom,X222!=X225|X224!=X223|~rrx(X222,X224)|rrx(X225,X223),theory(equality)).
% 0.62/0.81 cnf(c5,axiom,X205!=X206|~cc2(X205)|cc2(X206),theory(equality)).
% 0.62/0.81 cnf(c4,axiom,X198!=X199|~cc1(X198)|cc1(X199),theory(equality)).
% 0.62/0.81 cnf(c3,axiom,X190!=X191|~ca_Cx1xcomp(X190)|ca_Cx1xcomp(X191),theory(equality)).
% 0.62/0.81 cnf(c102,plain,~cSatisfiable(X189)|cc2(skolem0005(X189)),inference(split_conjunct,[status(thm)],[c97])).
% 0.62/0.81 cnf(c222,plain,cc2(skolem0005(i2003_11_14_17_16_10980)),inference(resolution,[status(thm)],[c102, c45])).
% 0.62/0.81 cnf(c2,axiom,X185!=X186|~ca_Cx1(X185)|ca_Cx1(X186),theory(equality)).
% 0.62/0.81 fof(axiom_14,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_14)).
% 0.62/0.81 fof(c39,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.62/0.81 fof(c40,plain,(![X14]:(![X15]:(~rrx4(X14,X15)|rrx(X14,X15)))),inference(variable_rename,[status(thm)],[c39])).
% 0.62/0.81 cnf(c41,plain,~rrx4(X181,X180)|rrx(X181,X180),inference(split_conjunct,[status(thm)],[c40])).
% 0.62/0.81 fof(axiom_15,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_15)).
% 0.62/0.81 fof(c36,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 0.62/0.81 fof(c37,plain,(![X12]:(![X13]:(~rrx3(X12,X13)|rrx(X12,X13)))),inference(variable_rename,[status(thm)],[c36])).
% 0.62/0.81 cnf(c38,plain,~rrx3(X178,X179)|rrx(X178,X179),inference(split_conjunct,[status(thm)],[c37])).
% 0.62/0.81 cnf(c1,axiom,X175!=X176|~ca_Ax2(X175)|ca_Ax2(X176),theory(equality)).
% 0.62/0.81 fof(axiom_18,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_18)).
% 0.62/0.81 fof(c27,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_18])).
% 0.62/0.81 fof(c28,plain,(![X6]:(![X7]:(~rrx3(X6,X7)|rrx1(X6,X7)))),inference(variable_rename,[status(thm)],[c27])).
% 0.62/0.81 cnf(c29,plain,~rrx3(X169,X170)|rrx1(X169,X170),inference(split_conjunct,[status(thm)],[c28])).
% 0.62/0.81 cnf(c0,axiom,X164!=X165|~cSatisfiable(X164)|cSatisfiable(X165),theory(equality)).
% 0.62/0.81 fof(axiom_20,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx2(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_20)).
% 0.62/0.81 fof(c21,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_20])).
% 0.62/0.81 fof(c22,plain,(![X2]:(![X3]:(~rrx4(X2,X3)|rrx2(X2,X3)))),inference(variable_rename,[status(thm)],[c21])).
% 0.62/0.81 cnf(c23,plain,~rrx4(X163,X162)|rrx2(X163,X162),inference(split_conjunct,[status(thm)],[c22])).
% 0.62/0.81 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.62/0.81 fof(c104,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.62/0.81 fof(c105,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c104])).
% 0.62/0.81 fof(c106,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c105])).
% 0.62/0.81 fof(c108,plain,(![X53]:(![X54]:((~xsd_string(X53)|~xsd_integer(X53))&(xsd_integer(X54)|xsd_string(X54))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,((![X53]:(~xsd_string(X53)|~xsd_integer(X53)))&(![X54]:(xsd_integer(X54)|xsd_string(X54)))),inference(variable_rename,[status(thm)],[c106])).])).
% 0.62/0.81 cnf(c110,plain,xsd_integer(X156)|xsd_string(X156),inference(split_conjunct,[status(thm)],[c108])).
% 0.62/0.81 cnf(transitivity,axiom,X153!=X154|X154!=X155|X153=X155,theory(equality)).
% 0.62/0.81 cnf(c109,plain,~xsd_string(X152)|~xsd_integer(X152),inference(split_conjunct,[status(thm)],[c108])).
% 0.62/0.81 cnf(symmetry,axiom,X147!=X148|X148=X147,theory(equality)).
% 0.62/0.81 cnf(reflexivity,axiom,X145=X145,theory(equality)).
% 0.62/0.81 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.62/0.81 fof(c111,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.62/0.81 fof(c112,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c111])).
% 0.62/0.81 fof(c114,plain,(![X55]:(![X56]:(cowlThing(X55)&~cowlNothing(X56)))),inference(shift_quantors,[status(thm)],[fof(c113,plain,((![X55]:cowlThing(X55))&(![X56]:~cowlNothing(X56))),inference(variable_rename,[status(thm)],[c112])).])).
% 0.62/0.81 cnf(c116,plain,~cowlNothing(X144),inference(split_conjunct,[status(thm)],[c114])).
% 0.62/0.81 cnf(c115,plain,cowlThing(X143),inference(split_conjunct,[status(thm)],[c114])).
% 0.62/0.81 % SZS output end Saturation
% 0.62/0.81
% 0.62/0.81 % Initial clauses : 90
% 0.62/0.81 % Processed clauses : 214
% 0.62/0.81 % Factors computed : 6
% 0.62/0.81 % Resolvents computed: 310
% 0.62/0.81 % Tautologies deleted: 13
% 0.62/0.81 % Forward subsumed : 179
% 0.62/0.81 % Backward subsumed : 0
% 0.62/0.81 % -------- CPU Time ---------
% 0.62/0.81 % User time : 0.447 s
% 0.62/0.81 % System time : 0.016 s
% 0.62/0.81 % Total time : 0.463 s
%------------------------------------------------------------------------------