%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS028+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:30 EDT 2024
% Result : Satisfiable 0.45s 0.62s
% Output : Saturation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS028+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n029.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:13:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.62 % Version: 1.5
% 0.45/0.62 % SZS status Satisfiable
% 0.45/0.62 % SZS output start Saturation
% 0.45/0.62 fof(axiom_8,axiom,cSatisfiable(i2003_11_14_17_15_19316),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.45/0.62 cnf(c41,plain,cSatisfiable(i2003_11_14_17_15_19316),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.45/0.62 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>(((?[Y]:(rrx4a(X,Y)&cc2(Y)))&(?[Y]:(rrx3a(X,Y)&cc1(Y))))&(~(?[Y]:((rrx3a(X,Y)&cc1(Y))&cc2(Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.45/0.62 fof(c57,plain,(![X]:((~cSatisfiable(X)|(((?[Y]:(rrx4a(X,Y)&cc2(Y)))&(?[Y]:(rrx3a(X,Y)&cc1(Y))))&(![Y]:((~rrx3a(X,Y)|~cc1(Y))|~cc2(Y)))))&((((![Y]:(~rrx4a(X,Y)|~cc2(Y)))|(![Y]:(~rrx3a(X,Y)|~cc1(Y))))|(?[Y]:((rrx3a(X,Y)&cc1(Y))&cc2(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.45/0.62 fof(c58,plain,((![X]:(~cSatisfiable(X)|(((?[Y]:(rrx4a(X,Y)&cc2(Y)))&(?[Y]:(rrx3a(X,Y)&cc1(Y))))&(![Y]:((~rrx3a(X,Y)|~cc1(Y))|~cc2(Y))))))&(![X]:((((![Y]:(~rrx4a(X,Y)|~cc2(Y)))|(![Y]:(~rrx3a(X,Y)|~cc1(Y))))|(?[Y]:((rrx3a(X,Y)&cc1(Y))&cc2(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c57])).
% 0.45/0.62 fof(c59,plain,((![X33]:(~cSatisfiable(X33)|(((?[X34]:(rrx4a(X33,X34)&cc2(X34)))&(?[X35]:(rrx3a(X33,X35)&cc1(X35))))&(![X36]:((~rrx3a(X33,X36)|~cc1(X36))|~cc2(X36))))))&(![X37]:((((![X38]:(~rrx4a(X37,X38)|~cc2(X38)))|(![X39]:(~rrx3a(X37,X39)|~cc1(X39))))|(?[X40]:((rrx3a(X37,X40)&cc1(X40))&cc2(X40))))|cSatisfiable(X37)))),inference(variable_rename,[status(thm)],[c58])).
% 0.45/0.62 fof(c61,plain,(![X33]:(![X36]:(![X37]:(![X38]:(![X39]:((~cSatisfiable(X33)|(((rrx4a(X33,skolem0001(X33))&cc2(skolem0001(X33)))&(rrx3a(X33,skolem0002(X33))&cc1(skolem0002(X33))))&((~rrx3a(X33,X36)|~cc1(X36))|~cc2(X36))))&((((~rrx4a(X37,X38)|~cc2(X38))|(~rrx3a(X37,X39)|~cc1(X39)))|((rrx3a(X37,skolem0003(X37))&cc1(skolem0003(X37)))&cc2(skolem0003(X37))))|cSatisfiable(X37)))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X33]:(~cSatisfiable(X33)|(((rrx4a(X33,skolem0001(X33))&cc2(skolem0001(X33)))&(rrx3a(X33,skolem0002(X33))&cc1(skolem0002(X33))))&(![X36]:((~rrx3a(X33,X36)|~cc1(X36))|~cc2(X36))))))&(![X37]:((((![X38]:(~rrx4a(X37,X38)|~cc2(X38)))|(![X39]:(~rrx3a(X37,X39)|~cc1(X39))))|((rrx3a(X37,skolem0003(X37))&cc1(skolem0003(X37)))&cc2(skolem0003(X37))))|cSatisfiable(X37)))),inference(skolemize,[status(esa)],[c59])).])).
% 0.45/0.62 fof(c62,plain,(![X33]:(![X36]:(![X37]:(![X38]:(![X39]:(((((~cSatisfiable(X33)|rrx4a(X33,skolem0001(X33)))&(~cSatisfiable(X33)|cc2(skolem0001(X33))))&((~cSatisfiable(X33)|rrx3a(X33,skolem0002(X33)))&(~cSatisfiable(X33)|cc1(skolem0002(X33)))))&(~cSatisfiable(X33)|((~rrx3a(X33,X36)|~cc1(X36))|~cc2(X36))))&((((((~rrx4a(X37,X38)|~cc2(X38))|(~rrx3a(X37,X39)|~cc1(X39)))|rrx3a(X37,skolem0003(X37)))|cSatisfiable(X37))&((((~rrx4a(X37,X38)|~cc2(X38))|(~rrx3a(X37,X39)|~cc1(X39)))|cc1(skolem0003(X37)))|cSatisfiable(X37)))&((((~rrx4a(X37,X38)|~cc2(X38))|(~rrx3a(X37,X39)|~cc1(X39)))|cc2(skolem0003(X37)))|cSatisfiable(X37))))))))),inference(distribute,[status(thm)],[c61])).
% 0.45/0.62 cnf(c65,plain,~cSatisfiable(X162)|rrx3a(X162,skolem0002(X162)),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 cnf(c177,plain,rrx3a(i2003_11_14_17_15_19316,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c65, c41])).
% 0.45/0.62 cnf(c67,plain,~cSatisfiable(X317)|~rrx3a(X317,X318)|~cc1(X318)|~cc2(X318),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 cnf(c212,plain,~cSatisfiable(i2003_11_14_17_15_19316)|~cc1(skolem0002(i2003_11_14_17_15_19316))|~cc2(skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c67, c177])).
% 0.45/0.62 fof(axiom_9,axiom,(![X]:(![Y]:(rrx3a(X,Y)=>rrxa(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.45/0.62 fof(c38,plain,(![X]:(![Y]:(~rrx3a(X,Y)|rrxa(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.45/0.62 fof(c39,plain,(![X16]:(![X17]:(~rrx3a(X16,X17)|rrxa(X16,X17)))),inference(variable_rename,[status(thm)],[c38])).
% 0.45/0.62 cnf(c40,plain,~rrx3a(X148,X149)|rrxa(X148,X149),inference(split_conjunct,[status(thm)],[c39])).
% 0.45/0.62 cnf(c178,plain,rrxa(i2003_11_14_17_15_19316,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c177, c40])).
% 0.45/0.62 cnf(c14,axiom,X312!=X313|X314!=X311|~rrxa(X312,X314)|rrxa(X313,X311),theory(equality)).
% 0.45/0.62 cnf(c209,plain,i2003_11_14_17_15_19316!=X352|skolem0002(i2003_11_14_17_15_19316)!=X353|rrxa(X352,X353),inference(resolution,[status(thm)],[c14, c178])).
% 0.45/0.62 fof(axiom_11,axiom,(![X]:(![Y]:(rrx4a(X,Y)=>rrxa(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.45/0.62 fof(c32,plain,(![X]:(![Y]:(~rrx4a(X,Y)|rrxa(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.45/0.62 fof(c33,plain,(![X12]:(![X13]:(~rrx4a(X12,X13)|rrxa(X12,X13)))),inference(variable_rename,[status(thm)],[c32])).
% 0.45/0.62 cnf(c34,plain,~rrx4a(X142,X141)|rrxa(X142,X141),inference(split_conjunct,[status(thm)],[c33])).
% 0.45/0.62 cnf(c63,plain,~cSatisfiable(X158)|rrx4a(X158,skolem0001(X158)),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 cnf(c173,plain,rrx4a(i2003_11_14_17_15_19316,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c63, c41])).
% 0.45/0.62 cnf(c176,plain,rrxa(i2003_11_14_17_15_19316,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c173, c34])).
% 0.45/0.62 cnf(c208,plain,i2003_11_14_17_15_19316!=X349|skolem0001(i2003_11_14_17_15_19316)!=X350|rrxa(X349,X350),inference(resolution,[status(thm)],[c14, c176])).
% 0.45/0.62 cnf(c13,axiom,X305!=X306|X307!=X304|~rrx4a(X305,X307)|rrx4a(X306,X304),theory(equality)).
% 0.45/0.62 cnf(c204,plain,i2003_11_14_17_15_19316!=X346|skolem0001(i2003_11_14_17_15_19316)!=X347|rrx4a(X346,X347),inference(resolution,[status(thm)],[c13, c173])).
% 0.45/0.62 cnf(c11,axiom,X267!=X268|X269!=X266|~rrx3a(X267,X269)|rrx3a(X268,X266),theory(equality)).
% 0.45/0.62 cnf(c199,plain,i2003_11_14_17_15_19316!=X343|skolem0002(i2003_11_14_17_15_19316)!=X344|rrx3a(X343,X344),inference(resolution,[status(thm)],[c11, c177])).
% 0.45/0.62 fof(axiom_14,axiom,(![X]:(![Y]:(rrx4a(X,Y)=>rrx2a(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_14)).
% 0.45/0.62 fof(c23,plain,(![X]:(![Y]:(~rrx4a(X,Y)|rrx2a(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.45/0.62 fof(c24,plain,(![X6]:(![X7]:(~rrx4a(X6,X7)|rrx2a(X6,X7)))),inference(variable_rename,[status(thm)],[c23])).
% 0.45/0.62 cnf(c25,plain,~rrx4a(X136,X135)|rrx2a(X136,X135),inference(split_conjunct,[status(thm)],[c24])).
% 0.45/0.62 cnf(c175,plain,rrx2a(i2003_11_14_17_15_19316,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c173, c25])).
% 0.45/0.62 cnf(c9,axiom,X229!=X230|X231!=X228|~rrx2a(X229,X231)|rrx2a(X230,X228),theory(equality)).
% 0.45/0.62 cnf(c190,plain,i2003_11_14_17_15_19316!=X340|skolem0001(i2003_11_14_17_15_19316)!=X341|rrx2a(X340,X341),inference(resolution,[status(thm)],[c9, c175])).
% 0.45/0.62 fof(axiom_16,axiom,(![X]:(![Y]:(rrx3a(X,Y)=>rrx1a(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_16)).
% 0.45/0.62 fof(c17,plain,(![X]:(![Y]:(~rrx3a(X,Y)|rrx1a(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 0.45/0.62 fof(c18,plain,(![X2]:(![X3]:(~rrx3a(X2,X3)|rrx1a(X2,X3)))),inference(variable_rename,[status(thm)],[c17])).
% 0.45/0.62 cnf(c19,plain,~rrx3a(X128,X129)|rrx1a(X128,X129),inference(split_conjunct,[status(thm)],[c18])).
% 0.45/0.62 cnf(c179,plain,rrx1a(i2003_11_14_17_15_19316,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c177, c19])).
% 0.45/0.62 cnf(c7,axiom,X196!=X197|X198!=X195|~rrx1a(X196,X198)|rrx1a(X197,X195),theory(equality)).
% 0.45/0.62 cnf(c182,plain,i2003_11_14_17_15_19316!=X337|skolem0002(i2003_11_14_17_15_19316)!=X338|rrx1a(X337,X338),inference(resolution,[status(thm)],[c7, c179])).
% 0.45/0.62 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.45/0.62 fof(c135,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1a(A,C))|rrx1a(B,C))))),inference(fof_nnf,[status(thm)],[rrx1a_substitution_1])).
% 0.45/0.62 fof(c136,plain,(![X94]:(![X95]:(![X96]:((X94!=X95|~rrx1a(X94,X96))|rrx1a(X95,X96))))),inference(variable_rename,[status(thm)],[c135])).
% 0.45/0.62 cnf(c137,plain,X290!=X289|~rrx1a(X290,X291)|rrx1a(X289,X291),inference(split_conjunct,[status(thm)],[c136])).
% 0.45/0.62 cnf(c203,plain,i2003_11_14_17_15_19316!=X336|rrx1a(X336,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c137, c179])).
% 0.45/0.62 cnf(c70,plain,~rrx4a(X334,X335)|~cc2(X335)|~rrx3a(X334,X333)|~cc1(X333)|cc2(skolem0003(X334))|cSatisfiable(X334),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 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.45/0.62 fof(c132,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1a(C,A))|rrx1a(C,B))))),inference(fof_nnf,[status(thm)],[rrx1a_substitution_2])).
% 0.45/0.62 fof(c133,plain,(![X91]:(![X92]:(![X93]:((X91!=X92|~rrx1a(X93,X91))|rrx1a(X93,X92))))),inference(variable_rename,[status(thm)],[c132])).
% 0.45/0.62 cnf(c134,plain,X283!=X282|~rrx1a(X284,X283)|rrx1a(X284,X282),inference(split_conjunct,[status(thm)],[c133])).
% 0.45/0.62 cnf(c202,plain,skolem0002(i2003_11_14_17_15_19316)!=X332|rrx1a(i2003_11_14_17_15_19316,X332),inference(resolution,[status(thm)],[c134, c179])).
% 0.45/0.62 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.45/0.62 fof(c123,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2a(A,C))|rrx2a(B,C))))),inference(fof_nnf,[status(thm)],[rrx2a_substitution_1])).
% 0.45/0.62 fof(c124,plain,(![X82]:(![X83]:(![X84]:((X82!=X83|~rrx2a(X82,X84))|rrx2a(X83,X84))))),inference(variable_rename,[status(thm)],[c123])).
% 0.45/0.62 cnf(c125,plain,X273!=X275|~rrx2a(X273,X274)|rrx2a(X275,X274),inference(split_conjunct,[status(thm)],[c124])).
% 0.45/0.62 cnf(c201,plain,i2003_11_14_17_15_19316!=X331|rrx2a(X331,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c125, c175])).
% 0.45/0.62 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.45/0.62 fof(c120,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2a(C,A))|rrx2a(C,B))))),inference(fof_nnf,[status(thm)],[rrx2a_substitution_2])).
% 0.45/0.62 fof(c121,plain,(![X79]:(![X80]:(![X81]:((X79!=X80|~rrx2a(X81,X79))|rrx2a(X81,X80))))),inference(variable_rename,[status(thm)],[c120])).
% 0.45/0.62 cnf(c122,plain,X272!=X271|~rrx2a(X270,X272)|rrx2a(X270,X271),inference(split_conjunct,[status(thm)],[c121])).
% 0.45/0.62 cnf(c200,plain,skolem0001(i2003_11_14_17_15_19316)!=X330|rrx2a(i2003_11_14_17_15_19316,X330),inference(resolution,[status(thm)],[c122, c175])).
% 0.45/0.62 cnf(c69,plain,~rrx4a(X328,X329)|~cc2(X329)|~rrx3a(X328,X327)|~cc1(X327)|cc1(skolem0003(X328))|cSatisfiable(X328),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 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.45/0.62 fof(c111,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3a(A,C))|rrx3a(B,C))))),inference(fof_nnf,[status(thm)],[rrx3a_substitution_1])).
% 0.45/0.62 fof(c112,plain,(![X70]:(![X71]:(![X72]:((X70!=X71|~rrx3a(X70,X72))|rrx3a(X71,X72))))),inference(variable_rename,[status(thm)],[c111])).
% 0.45/0.62 cnf(c113,plain,X259!=X257|~rrx3a(X259,X258)|rrx3a(X257,X258),inference(split_conjunct,[status(thm)],[c112])).
% 0.45/0.62 cnf(c198,plain,i2003_11_14_17_15_19316!=X326|rrx3a(X326,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c113, c177])).
% 0.45/0.62 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.45/0.62 fof(c108,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3a(C,A))|rrx3a(C,B))))),inference(fof_nnf,[status(thm)],[rrx3a_substitution_2])).
% 0.45/0.62 fof(c109,plain,(![X67]:(![X68]:(![X69]:((X67!=X68|~rrx3a(X69,X67))|rrx3a(X69,X68))))),inference(variable_rename,[status(thm)],[c108])).
% 0.45/0.62 cnf(c110,plain,X256!=X254|~rrx3a(X255,X256)|rrx3a(X255,X254),inference(split_conjunct,[status(thm)],[c109])).
% 0.45/0.62 cnf(c197,plain,skolem0002(i2003_11_14_17_15_19316)!=X325|rrx3a(i2003_11_14_17_15_19316,X325),inference(resolution,[status(thm)],[c110, c177])).
% 0.45/0.62 cnf(c68,plain,~rrx4a(X323,X324)|~cc2(X324)|~rrx3a(X323,X322)|~cc1(X322)|rrx3a(X323,skolem0003(X323))|cSatisfiable(X323),inference(split_conjunct,[status(thm)],[c62])).
% 0.45/0.62 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.45/0.62 fof(c99,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4a(A,C))|rrx4a(B,C))))),inference(fof_nnf,[status(thm)],[rrx4a_substitution_1])).
% 0.45/0.62 fof(c100,plain,(![X58]:(![X59]:(![X60]:((X58!=X59|~rrx4a(X58,X60))|rrx4a(X59,X60))))),inference(variable_rename,[status(thm)],[c99])).
% 0.45/0.62 cnf(c101,plain,X242!=X243|~rrx4a(X242,X241)|rrx4a(X243,X241),inference(split_conjunct,[status(thm)],[c100])).
% 0.45/0.62 cnf(c196,plain,i2003_11_14_17_15_19316!=X321|rrx4a(X321,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c101, c173])).
% 0.45/0.62 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.45/0.62 fof(c96,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4a(C,A))|rrx4a(C,B))))),inference(fof_nnf,[status(thm)],[rrx4a_substitution_2])).
% 0.45/0.62 fof(c97,plain,(![X55]:(![X56]:(![X57]:((X55!=X56|~rrx4a(X57,X55))|rrx4a(X57,X56))))),inference(variable_rename,[status(thm)],[c96])).
% 0.45/0.62 cnf(c98,plain,X238!=X240|~rrx4a(X239,X238)|rrx4a(X239,X240),inference(split_conjunct,[status(thm)],[c97])).
% 0.45/0.62 cnf(c195,plain,skolem0001(i2003_11_14_17_15_19316)!=X320|rrx4a(i2003_11_14_17_15_19316,X320),inference(resolution,[status(thm)],[c98, c173])).
% 0.45/0.62 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.45/0.62 fof(c93,plain,(![A]:(![B]:(![C]:((A!=B|~rrxa(A,C))|rrxa(B,C))))),inference(fof_nnf,[status(thm)],[rrxa_substitution_1])).
% 0.45/0.62 fof(c94,plain,(![X52]:(![X53]:(![X54]:((X52!=X53|~rrxa(X52,X54))|rrxa(X53,X54))))),inference(variable_rename,[status(thm)],[c93])).
% 0.45/0.62 cnf(c95,plain,X237!=X235|~rrxa(X237,X236)|rrxa(X235,X236),inference(split_conjunct,[status(thm)],[c94])).
% 0.45/0.62 cnf(c194,plain,i2003_11_14_17_15_19316!=X319|rrxa(X319,skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c95, c178])).
% 0.45/0.62 cnf(c193,plain,i2003_11_14_17_15_19316!=X316|rrxa(X316,skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c95, c176])).
% 0.45/0.62 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.45/0.62 fof(c90,plain,(![A]:(![B]:(![C]:((A!=B|~rrxa(C,A))|rrxa(C,B))))),inference(fof_nnf,[status(thm)],[rrxa_substitution_2])).
% 0.45/0.62 fof(c91,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rrxa(X51,X49))|rrxa(X51,X50))))),inference(variable_rename,[status(thm)],[c90])).
% 0.45/0.62 cnf(c92,plain,X232!=X234|~rrxa(X233,X232)|rrxa(X233,X234),inference(split_conjunct,[status(thm)],[c91])).
% 0.45/0.62 cnf(c192,plain,skolem0002(i2003_11_14_17_15_19316)!=X315|rrxa(i2003_11_14_17_15_19316,X315),inference(resolution,[status(thm)],[c92, c178])).
% 0.45/0.62 cnf(c191,plain,skolem0001(i2003_11_14_17_15_19316)!=X310|rrxa(i2003_11_14_17_15_19316,X310),inference(resolution,[status(thm)],[c92, c176])).
% 0.45/0.62 fof(axiom_5,axiom,(![X]:(![Y]:(![Z]:((rrx3a(X,Y)&rrx3a(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.45/0.62 fof(c48,plain,(![X]:(![Y]:(![Z]:((~rrx3a(X,Y)|~rrx3a(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.45/0.62 fof(c49,plain,(![X24]:(![X25]:(![X26]:((~rrx3a(X24,X25)|~rrx3a(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c48])).
% 0.45/0.62 cnf(c50,plain,~rrx3a(X210,X211)|~rrx3a(X210,X209)|X211=X209,inference(split_conjunct,[status(thm)],[c49])).
% 0.45/0.62 cnf(c187,plain,~rrx3a(i2003_11_14_17_15_19316,X309)|X309=skolem0002(i2003_11_14_17_15_19316),inference(resolution,[status(thm)],[c50, c177])).
% 0.45/0.62 fof(axiom_7,axiom,(![X]:(![Y]:(![Z]:((rrx4a(X,Y)&rrx4a(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.45/0.62 fof(c42,plain,(![X]:(![Y]:(![Z]:((~rrx4a(X,Y)|~rrx4a(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.45/0.62 fof(c43,plain,(![X18]:(![X19]:(![X20]:((~rrx4a(X18,X19)|~rrx4a(X18,X20))|X19=X20)))),inference(variable_rename,[status(thm)],[c42])).
% 0.45/0.62 cnf(c44,plain,~rrx4a(X201,X199)|~rrx4a(X201,X200)|X199=X200,inference(split_conjunct,[status(thm)],[c43])).
% 0.45/0.62 cnf(c184,plain,~rrx4a(i2003_11_14_17_15_19316,X308)|X308=skolem0001(i2003_11_14_17_15_19316),inference(resolution,[status(thm)],[c44, c173])).
% 0.45/0.62 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.45/0.62 fof(c147,plain,(![A]:(![B]:(![C]:((A!=B|~rrx(A,C))|rrx(B,C))))),inference(fof_nnf,[status(thm)],[rrx_substitution_1])).
% 0.45/0.62 fof(c148,plain,(![X106]:(![X107]:(![X108]:((X106!=X107|~rrx(X106,X108))|rrx(X107,X108))))),inference(variable_rename,[status(thm)],[c147])).
% 0.45/0.62 cnf(c149,plain,X303!=X301|~rrx(X303,X302)|rrx(X301,X302),inference(split_conjunct,[status(thm)],[c148])).
% 0.45/0.62 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.45/0.62 fof(c144,plain,(![A]:(![B]:(![C]:((A!=B|~rrx(C,A))|rrx(C,B))))),inference(fof_nnf,[status(thm)],[rrx_substitution_2])).
% 0.45/0.62 fof(c145,plain,(![X103]:(![X104]:(![X105]:((X103!=X104|~rrx(X105,X103))|rrx(X105,X104))))),inference(variable_rename,[status(thm)],[c144])).
% 0.45/0.62 cnf(c146,plain,X300!=X298|~rrx(X299,X300)|rrx(X299,X298),inference(split_conjunct,[status(thm)],[c145])).
% 0.45/0.62 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.45/0.62 fof(c141,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1(A,C))|rrx1(B,C))))),inference(fof_nnf,[status(thm)],[rrx1_substitution_1])).
% 0.45/0.62 fof(c142,plain,(![X100]:(![X101]:(![X102]:((X100!=X101|~rrx1(X100,X102))|rrx1(X101,X102))))),inference(variable_rename,[status(thm)],[c141])).
% 0.45/0.62 cnf(c143,plain,X295!=X296|~rrx1(X295,X297)|rrx1(X296,X297),inference(split_conjunct,[status(thm)],[c142])).
% 0.45/0.62 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.45/0.62 fof(c138,plain,(![A]:(![B]:(![C]:((A!=B|~rrx1(C,A))|rrx1(C,B))))),inference(fof_nnf,[status(thm)],[rrx1_substitution_2])).
% 0.45/0.62 fof(c139,plain,(![X97]:(![X98]:(![X99]:((X97!=X98|~rrx1(X99,X97))|rrx1(X99,X98))))),inference(variable_rename,[status(thm)],[c138])).
% 0.45/0.62 cnf(c140,plain,X293!=X294|~rrx1(X292,X293)|rrx1(X292,X294),inference(split_conjunct,[status(thm)],[c139])).
% 0.45/0.62 cnf(c12,axiom,X286!=X287|X288!=X285|~rrx4(X286,X288)|rrx4(X287,X285),theory(equality)).
% 0.45/0.62 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.45/0.62 fof(c129,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2(A,C))|rrx2(B,C))))),inference(fof_nnf,[status(thm)],[rrx2_substitution_1])).
% 0.45/0.62 fof(c130,plain,(![X88]:(![X89]:(![X90]:((X88!=X89|~rrx2(X88,X90))|rrx2(X89,X90))))),inference(variable_rename,[status(thm)],[c129])).
% 0.45/0.62 cnf(c131,plain,X279!=X280|~rrx2(X279,X281)|rrx2(X280,X281),inference(split_conjunct,[status(thm)],[c130])).
% 0.45/0.62 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.45/0.62 fof(c126,plain,(![A]:(![B]:(![C]:((A!=B|~rrx2(C,A))|rrx2(C,B))))),inference(fof_nnf,[status(thm)],[rrx2_substitution_2])).
% 0.45/0.62 fof(c127,plain,(![X85]:(![X86]:(![X87]:((X85!=X86|~rrx2(X87,X85))|rrx2(X87,X86))))),inference(variable_rename,[status(thm)],[c126])).
% 0.45/0.62 cnf(c128,plain,X277!=X276|~rrx2(X278,X277)|rrx2(X278,X276),inference(split_conjunct,[status(thm)],[c127])).
% 0.45/0.62 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.45/0.62 fof(c117,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3(A,C))|rrx3(B,C))))),inference(fof_nnf,[status(thm)],[rrx3_substitution_1])).
% 0.45/0.62 fof(c118,plain,(![X76]:(![X77]:(![X78]:((X76!=X77|~rrx3(X76,X78))|rrx3(X77,X78))))),inference(variable_rename,[status(thm)],[c117])).
% 0.45/0.62 cnf(c119,plain,X265!=X264|~rrx3(X265,X263)|rrx3(X264,X263),inference(split_conjunct,[status(thm)],[c118])).
% 0.45/0.62 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.45/0.62 fof(c114,plain,(![A]:(![B]:(![C]:((A!=B|~rrx3(C,A))|rrx3(C,B))))),inference(fof_nnf,[status(thm)],[rrx3_substitution_2])).
% 0.45/0.62 fof(c115,plain,(![X73]:(![X74]:(![X75]:((X73!=X74|~rrx3(X75,X73))|rrx3(X75,X74))))),inference(variable_rename,[status(thm)],[c114])).
% 0.45/0.62 cnf(c116,plain,X260!=X262|~rrx3(X261,X260)|rrx3(X261,X262),inference(split_conjunct,[status(thm)],[c115])).
% 0.45/0.62 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.45/0.62 fof(c105,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4(A,C))|rrx4(B,C))))),inference(fof_nnf,[status(thm)],[rrx4_substitution_1])).
% 0.45/0.62 fof(c106,plain,(![X64]:(![X65]:(![X66]:((X64!=X65|~rrx4(X64,X66))|rrx4(X65,X66))))),inference(variable_rename,[status(thm)],[c105])).
% 0.45/0.62 cnf(c107,plain,X251!=X253|~rrx4(X251,X252)|rrx4(X253,X252),inference(split_conjunct,[status(thm)],[c106])).
% 0.45/0.62 cnf(c10,axiom,X248!=X249|X250!=X247|~rrx3(X248,X250)|rrx3(X249,X247),theory(equality)).
% 0.45/0.62 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.45/0.62 fof(c102,plain,(![A]:(![B]:(![C]:((A!=B|~rrx4(C,A))|rrx4(C,B))))),inference(fof_nnf,[status(thm)],[rrx4_substitution_2])).
% 0.45/0.62 fof(c103,plain,(![X61]:(![X62]:(![X63]:((X61!=X62|~rrx4(X63,X61))|rrx4(X63,X62))))),inference(variable_rename,[status(thm)],[c102])).
% 0.45/0.62 cnf(c104,plain,X245!=X244|~rrx4(X246,X245)|rrx4(X246,X244),inference(split_conjunct,[status(thm)],[c103])).
% 0.45/0.62 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rrx(X,Y)&rrx(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.45/0.62 fof(c54,plain,(![X]:(![Y]:(![Z]:((~rrx(X,Y)|~rrx(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.45/0.62 fof(c55,plain,(![X30]:(![X31]:(![X32]:((~rrx(X30,X31)|~rrx(X30,X32))|X31=X32)))),inference(variable_rename,[status(thm)],[c54])).
% 0.45/0.62 cnf(c56,plain,~rrx(X224,X223)|~rrx(X224,X225)|X223=X225,inference(split_conjunct,[status(thm)],[c55])).
% 0.45/0.62 fof(axiom_4,axiom,(![X]:(![Y]:(![Z]:((rrx3(X,Y)&rrx3(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.45/0.62 fof(c51,plain,(![X]:(![Y]:(![Z]:((~rrx3(X,Y)|~rrx3(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.45/0.62 fof(c52,plain,(![X27]:(![X28]:(![X29]:((~rrx3(X27,X28)|~rrx3(X27,X29))|X28=X29)))),inference(variable_rename,[status(thm)],[c51])).
% 0.45/0.62 cnf(c53,plain,~rrx3(X219,X220)|~rrx3(X219,X218)|X220=X218,inference(split_conjunct,[status(thm)],[c52])).
% 0.45/0.62 cnf(c8,axiom,X213!=X214|X215!=X212|~rrx2(X213,X215)|rrx2(X214,X212),theory(equality)).
% 0.45/0.62 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rrx4(X,Y)&rrx4(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.45/0.62 fof(c45,plain,(![X]:(![Y]:(![Z]:((~rrx4(X,Y)|~rrx4(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.45/0.62 fof(c46,plain,(![X21]:(![X22]:(![X23]:((~rrx4(X21,X22)|~rrx4(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c45])).
% 0.45/0.62 cnf(c47,plain,~rrx4(X206,X204)|~rrx4(X206,X205)|X204=X205,inference(split_conjunct,[status(thm)],[c46])).
% 0.45/0.62 cnf(c6,axiom,X182!=X183|X184!=X181|~rrx1(X182,X184)|rrx1(X183,X181),theory(equality)).
% 0.45/0.62 cnf(c16,axiom,X174!=X175|~xsd_string(X174)|xsd_string(X175),theory(equality)).
% 0.45/0.62 cnf(c5,axiom,X170!=X171|X172!=X169|~rrx(X170,X172)|rrx(X171,X169),theory(equality)).
% 0.45/0.62 cnf(c15,axiom,X167!=X168|~xsd_integer(X167)|xsd_integer(X168),theory(equality)).
% 0.45/0.62 cnf(c2,axiom,X159!=X160|~cc2(X159)|cc2(X160),theory(equality)).
% 0.45/0.62 cnf(c66,plain,~cSatisfiable(X151)|cc1(skolem0002(X151)),inference(split_conjunct,[status(thm)],[c62])).
% 0.47/0.62 cnf(c171,plain,cc1(skolem0002(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c66, c41])).
% 0.47/0.62 cnf(c1,axiom,X152!=X153|~cc1(X152)|cc1(X153),theory(equality)).
% 0.47/0.62 cnf(c64,plain,~cSatisfiable(X150)|cc2(skolem0001(X150)),inference(split_conjunct,[status(thm)],[c62])).
% 0.47/0.62 cnf(c170,plain,cc2(skolem0001(i2003_11_14_17_15_19316)),inference(resolution,[status(thm)],[c64, c41])).
% 0.47/0.62 cnf(c0,axiom,X145!=X146|~cSatisfiable(X145)|cSatisfiable(X146),theory(equality)).
% 0.47/0.62 fof(axiom_10,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.47/0.62 fof(c35,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.47/0.62 fof(c36,plain,(![X14]:(![X15]:(~rrx3(X14,X15)|rrx1(X14,X15)))),inference(variable_rename,[status(thm)],[c35])).
% 0.47/0.62 cnf(c37,plain,~rrx3(X143,X144)|rrx1(X143,X144),inference(split_conjunct,[status(thm)],[c36])).
% 0.47/0.62 fof(axiom_12,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.47/0.62 fof(c29,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 0.47/0.62 fof(c30,plain,(![X10]:(![X11]:(~rrx3(X10,X11)|rrx(X10,X11)))),inference(variable_rename,[status(thm)],[c29])).
% 0.47/0.62 cnf(c31,plain,~rrx3(X140,X139)|rrx(X140,X139),inference(split_conjunct,[status(thm)],[c30])).
% 0.47/0.62 fof(axiom_13,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx2(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_13)).
% 0.47/0.62 fof(c26,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_13])).
% 0.47/0.62 fof(c27,plain,(![X8]:(![X9]:(~rrx4(X8,X9)|rrx2(X8,X9)))),inference(variable_rename,[status(thm)],[c26])).
% 0.47/0.62 cnf(c28,plain,~rrx4(X138,X137)|rrx2(X138,X137),inference(split_conjunct,[status(thm)],[c27])).
% 0.47/0.62 cnf(transitivity,axiom,X134!=X132|X132!=X133|X134=X133,theory(equality)).
% 0.47/0.62 fof(axiom_15,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_15)).
% 0.47/0.62 fof(c20,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 0.47/0.62 fof(c21,plain,(![X4]:(![X5]:(~rrx4(X4,X5)|rrx(X4,X5)))),inference(variable_rename,[status(thm)],[c20])).
% 0.47/0.62 cnf(c22,plain,~rrx4(X130,X131)|rrx(X130,X131),inference(split_conjunct,[status(thm)],[c21])).
% 0.47/0.62 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.47/0.62 fof(c71,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.47/0.62 fof(c72,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c71])).
% 0.47/0.62 fof(c73,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c72])).
% 0.47/0.62 fof(c75,plain,(![X41]:(![X42]:((~xsd_string(X41)|~xsd_integer(X41))&(xsd_integer(X42)|xsd_string(X42))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X41]:(~xsd_string(X41)|~xsd_integer(X41)))&(![X42]:(xsd_integer(X42)|xsd_string(X42)))),inference(variable_rename,[status(thm)],[c73])).])).
% 0.47/0.62 cnf(c77,plain,xsd_integer(X126)|xsd_string(X126),inference(split_conjunct,[status(thm)],[c75])).
% 0.47/0.62 cnf(symmetry,axiom,X124!=X123|X123=X124,theory(equality)).
% 0.47/0.62 cnf(c76,plain,~xsd_string(X122)|~xsd_integer(X122),inference(split_conjunct,[status(thm)],[c75])).
% 0.47/0.62 cnf(reflexivity,axiom,X121=X121,theory(equality)).
% 0.47/0.62 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.47/0.62 fof(c78,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.47/0.62 fof(c79,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c78])).
% 0.47/0.62 fof(c81,plain,(![X43]:(![X44]:(cowlThing(X43)&~cowlNothing(X44)))),inference(shift_quantors,[status(thm)],[fof(c80,plain,((![X43]:cowlThing(X43))&(![X44]:~cowlNothing(X44))),inference(variable_rename,[status(thm)],[c79])).])).
% 0.47/0.62 cnf(c83,plain,~cowlNothing(X120),inference(split_conjunct,[status(thm)],[c81])).
% 0.47/0.62 cnf(c82,plain,cowlThing(X119),inference(split_conjunct,[status(thm)],[c81])).
% 0.47/0.62 % SZS output end Saturation
% 0.47/0.62
% 0.47/0.62 % Initial clauses : 73
% 0.47/0.62 % Processed clauses : 93
% 0.47/0.62 % Factors computed : 6
% 0.47/0.62 % Resolvents computed: 60
% 0.47/0.62 % Tautologies deleted: 8
% 0.47/0.62 % Forward subsumed : 38
% 0.47/0.62 % Backward subsumed : 0
% 0.47/0.62 % -------- CPU Time ---------
% 0.47/0.62 % User time : 0.270 s
% 0.47/0.62 % System time : 0.011 s
% 0.47/0.62 % Total time : 0.281 s
%------------------------------------------------------------------------------