%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS047+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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.51s 0.70s
% Output : Saturation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS047+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n010.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:15:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.51/0.70 % Version: 1.5
% 0.51/0.70 % SZS status Satisfiable
% 0.51/0.70 % SZS output start Saturation
% 0.51/0.70 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>(((?[Y]:(rinvF(X,Y)&ca(Y)))&caxcomp(X))&(?[Y]:(rinvR(X,Y)&ca_Vx2(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.51/0.70 fof(c58,plain,(![X]:((~cSatisfiable(X)|(((?[Y]:(rinvF(X,Y)&ca(Y)))&caxcomp(X))&(?[Y]:(rinvR(X,Y)&ca_Vx2(Y)))))&((((![Y]:(~rinvF(X,Y)|~ca(Y)))|~caxcomp(X))|(![Y]:(~rinvR(X,Y)|~ca_Vx2(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.51/0.70 fof(c59,plain,((![X]:(~cSatisfiable(X)|(((?[Y]:(rinvF(X,Y)&ca(Y)))&caxcomp(X))&(?[Y]:(rinvR(X,Y)&ca_Vx2(Y))))))&(![X]:((((![Y]:(~rinvF(X,Y)|~ca(Y)))|~caxcomp(X))|(![Y]:(~rinvR(X,Y)|~ca_Vx2(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c58])).
% 0.51/0.70 fof(c60,plain,((![X30]:(~cSatisfiable(X30)|(((?[X31]:(rinvF(X30,X31)&ca(X31)))&caxcomp(X30))&(?[X32]:(rinvR(X30,X32)&ca_Vx2(X32))))))&(![X33]:((((![X34]:(~rinvF(X33,X34)|~ca(X34)))|~caxcomp(X33))|(![X35]:(~rinvR(X33,X35)|~ca_Vx2(X35))))|cSatisfiable(X33)))),inference(variable_rename,[status(thm)],[c59])).
% 0.51/0.70 fof(c62,plain,(![X30]:(![X33]:(![X34]:(![X35]:((~cSatisfiable(X30)|(((rinvF(X30,skolem0004(X30))&ca(skolem0004(X30)))&caxcomp(X30))&(rinvR(X30,skolem0005(X30))&ca_Vx2(skolem0005(X30)))))&((((~rinvF(X33,X34)|~ca(X34))|~caxcomp(X33))|(~rinvR(X33,X35)|~ca_Vx2(X35)))|cSatisfiable(X33))))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X30]:(~cSatisfiable(X30)|(((rinvF(X30,skolem0004(X30))&ca(skolem0004(X30)))&caxcomp(X30))&(rinvR(X30,skolem0005(X30))&ca_Vx2(skolem0005(X30))))))&(![X33]:((((![X34]:(~rinvF(X33,X34)|~ca(X34)))|~caxcomp(X33))|(![X35]:(~rinvR(X33,X35)|~ca_Vx2(X35))))|cSatisfiable(X33)))),inference(skolemize,[status(esa)],[c60])).])).
% 0.51/0.70 fof(c63,plain,(![X30]:(![X33]:(![X34]:(![X35]:(((((~cSatisfiable(X30)|rinvF(X30,skolem0004(X30)))&(~cSatisfiable(X30)|ca(skolem0004(X30))))&(~cSatisfiable(X30)|caxcomp(X30)))&((~cSatisfiable(X30)|rinvR(X30,skolem0005(X30)))&(~cSatisfiable(X30)|ca_Vx2(skolem0005(X30)))))&((((~rinvF(X33,X34)|~ca(X34))|~caxcomp(X33))|(~rinvR(X33,X35)|~ca_Vx2(X35)))|cSatisfiable(X33))))))),inference(distribute,[status(thm)],[c62])).
% 0.51/0.70 cnf(c69,plain,~rinvF(X200,X199)|~ca(X199)|~caxcomp(X200)|~rinvR(X200,X198)|~ca_Vx2(X198)|cSatisfiable(X200),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 fof(axiom_8,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.51/0.70 fof(c20,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.51/0.70 fof(c21,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c20])).
% 0.51/0.70 fof(c23,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~rinvR(X7,X8)|rr(X8,X7))&(~rr(X10,X9)|rinvR(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,((![X7]:(![X8]:(~rinvR(X7,X8)|rr(X8,X7))))&(![X9]:(![X10]:(~rr(X10,X9)|rinvR(X9,X10))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.51/0.70 cnf(c25,plain,~rr(X108,X107)|rinvR(X107,X108),inference(split_conjunct,[status(thm)],[c23])).
% 0.51/0.70 fof(axiom_11,axiom,(![X]:(![Y]:(rf(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.51/0.70 fof(c13,plain,(![X]:(![Y]:(~rf(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.51/0.70 fof(c14,plain,(![X2]:(![X3]:(~rf(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c13])).
% 0.51/0.70 cnf(c15,plain,~rf(X104,X103)|rr(X104,X103),inference(split_conjunct,[status(thm)],[c14])).
% 0.51/0.70 fof(axiom_7,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.51/0.70 fof(c26,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.51/0.70 fof(c27,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.51/0.70 fof(c29,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~rinvF(X11,X12)|rf(X12,X11))&(~rf(X14,X13)|rinvF(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X11]:(![X12]:(~rinvF(X11,X12)|rf(X12,X11))))&(![X13]:(![X14]:(~rf(X14,X13)|rinvF(X13,X14))))),inference(variable_rename,[status(thm)],[c27])).])).
% 0.51/0.70 cnf(c30,plain,~rinvF(X112,X113)|rf(X113,X112),inference(split_conjunct,[status(thm)],[c29])).
% 0.51/0.70 fof(axiom_10,axiom,cSatisfiable(i2003_11_14_17_16_29157),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.51/0.70 cnf(c16,plain,cSatisfiable(i2003_11_14_17_16_29157),inference(split_conjunct,[status(thm)],[axiom_10])).
% 0.51/0.70 cnf(c68,plain,~cSatisfiable(X121)|ca_Vx2(skolem0005(X121)),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 cnf(c145,plain,ca_Vx2(skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c68, c16])).
% 0.51/0.70 fof(axiom_5,axiom,(![X]:(ca_Vx2(X)<=>(?[Y]:(rinvF(X,Y)&ca(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.51/0.70 fof(c35,plain,(![X]:((~ca_Vx2(X)|(?[Y]:(rinvF(X,Y)&ca(Y))))&((![Y]:(~rinvF(X,Y)|~ca(Y)))|ca_Vx2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.51/0.70 fof(c36,plain,((![X]:(~ca_Vx2(X)|(?[Y]:(rinvF(X,Y)&ca(Y)))))&(![X]:((![Y]:(~rinvF(X,Y)|~ca(Y)))|ca_Vx2(X)))),inference(shift_quantors,[status(thm)],[c35])).
% 0.51/0.70 fof(c37,plain,((![X18]:(~ca_Vx2(X18)|(?[X19]:(rinvF(X18,X19)&ca(X19)))))&(![X20]:((![X21]:(~rinvF(X20,X21)|~ca(X21)))|ca_Vx2(X20)))),inference(variable_rename,[status(thm)],[c36])).
% 0.51/0.70 fof(c39,plain,(![X18]:(![X20]:(![X21]:((~ca_Vx2(X18)|(rinvF(X18,skolem0001(X18))&ca(skolem0001(X18))))&((~rinvF(X20,X21)|~ca(X21))|ca_Vx2(X20)))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X18]:(~ca_Vx2(X18)|(rinvF(X18,skolem0001(X18))&ca(skolem0001(X18)))))&(![X20]:((![X21]:(~rinvF(X20,X21)|~ca(X21)))|ca_Vx2(X20)))),inference(skolemize,[status(esa)],[c37])).])).
% 0.51/0.70 fof(c40,plain,(![X18]:(![X20]:(![X21]:(((~ca_Vx2(X18)|rinvF(X18,skolem0001(X18)))&(~ca_Vx2(X18)|ca(skolem0001(X18))))&((~rinvF(X20,X21)|~ca(X21))|ca_Vx2(X20)))))),inference(distribute,[status(thm)],[c39])).
% 0.51/0.70 cnf(c41,plain,~ca_Vx2(X128)|rinvF(X128,skolem0001(X128)),inference(split_conjunct,[status(thm)],[c40])).
% 0.51/0.70 cnf(c148,plain,rinvF(skolem0005(i2003_11_14_17_16_29157),skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c41, c145])).
% 0.51/0.70 cnf(c243,plain,rf(skolem0001(skolem0005(i2003_11_14_17_16_29157)),skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c148, c30])).
% 0.51/0.70 cnf(c284,plain,rr(skolem0001(skolem0005(i2003_11_14_17_16_29157)),skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c243, c15])).
% 0.51/0.70 cnf(c292,plain,rinvR(skolem0005(i2003_11_14_17_16_29157),skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c284, c25])).
% 0.51/0.70 cnf(c304,plain,~rinvF(skolem0005(i2003_11_14_17_16_29157),X355)|~ca(X355)|~caxcomp(skolem0005(i2003_11_14_17_16_29157))|~ca_Vx2(skolem0001(skolem0005(i2003_11_14_17_16_29157)))|cSatisfiable(skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c292, c69])).
% 0.51/0.70 cnf(c9,axiom,X163!=X165|X166!=X164|~rinvR(X163,X166)|rinvR(X165,X164),theory(equality)).
% 0.51/0.70 cnf(c305,plain,skolem0005(i2003_11_14_17_16_29157)!=X353|skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X352|rinvR(X353,X352),inference(resolution,[status(thm)],[c292, c9])).
% 0.51/0.70 cnf(c24,plain,~rinvR(X106,X105)|rr(X105,X106),inference(split_conjunct,[status(thm)],[c23])).
% 0.51/0.70 cnf(c67,plain,~cSatisfiable(X145)|rinvR(X145,skolem0005(X145)),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 cnf(c169,plain,rinvR(i2003_11_14_17_16_29157,skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c67, c16])).
% 0.51/0.70 cnf(c170,plain,rr(skolem0005(i2003_11_14_17_16_29157),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c169, c24])).
% 0.51/0.70 fof(axiom_9,axiom,(![X]:(![Y]:(![Z]:((rr(X,Y)&rr(Y,Z))=>rr(X,Z))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.51/0.70 fof(c17,plain,(![X]:(![Y]:(![Z]:((~rr(X,Y)|~rr(Y,Z))|rr(X,Z))))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.51/0.70 fof(c18,plain,(![X4]:(![X5]:(![X6]:((~rr(X4,X5)|~rr(X5,X6))|rr(X4,X6))))),inference(variable_rename,[status(thm)],[c17])).
% 0.51/0.70 cnf(c19,plain,~rr(X189,X190)|~rr(X190,X191)|rr(X189,X191),inference(split_conjunct,[status(thm)],[c18])).
% 0.51/0.70 cnf(c191,plain,~rr(X232,skolem0005(i2003_11_14_17_16_29157))|rr(X232,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c19, c170])).
% 0.51/0.70 cnf(c287,plain,rr(skolem0001(skolem0005(i2003_11_14_17_16_29157)),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c284, c191])).
% 0.51/0.70 cnf(c297,plain,rinvR(i2003_11_14_17_16_29157,skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c287, c25])).
% 0.51/0.70 cnf(c299,plain,i2003_11_14_17_16_29157!=X349|skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X348|rinvR(X349,X348),inference(resolution,[status(thm)],[c297, c9])).
% 0.51/0.70 cnf(c10,axiom,X177!=X179|X180!=X178|~rr(X177,X180)|rr(X179,X178),theory(equality)).
% 0.51/0.70 cnf(c293,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X342|i2003_11_14_17_16_29157!=X343|rr(X342,X343),inference(resolution,[status(thm)],[c287, c10])).
% 0.51/0.70 fof(rinvR_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvR(C,A))=>rinvR(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvR_substitution_2)).
% 0.51/0.70 fof(c95,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(C,A))|rinvR(C,B))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_2])).
% 0.51/0.70 fof(c96,plain,(![X50]:(![X51]:(![X52]:((X50!=X51|~rinvR(X52,X50))|rinvR(X52,X51))))),inference(variable_rename,[status(thm)],[c95])).
% 0.51/0.70 cnf(c97,plain,X209!=X207|~rinvR(X208,X209)|rinvR(X208,X207),inference(split_conjunct,[status(thm)],[c96])).
% 0.51/0.70 cnf(c307,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X341|rinvR(skolem0005(i2003_11_14_17_16_29157),X341),inference(resolution,[status(thm)],[c292, c97])).
% 0.51/0.70 fof(rinvR_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvR(A,C))=>rinvR(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvR_substitution_1)).
% 0.51/0.70 fof(c98,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(A,C))|rinvR(B,C))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_1])).
% 0.51/0.70 fof(c99,plain,(![X53]:(![X54]:(![X55]:((X53!=X54|~rinvR(X53,X55))|rinvR(X54,X55))))),inference(variable_rename,[status(thm)],[c98])).
% 0.51/0.70 cnf(c100,plain,X210!=X212|~rinvR(X210,X211)|rinvR(X212,X211),inference(split_conjunct,[status(thm)],[c99])).
% 0.51/0.70 cnf(c306,plain,skolem0005(i2003_11_14_17_16_29157)!=X340|rinvR(X340,skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c292, c100])).
% 0.51/0.70 cnf(c291,plain,~rr(X339,skolem0001(skolem0005(i2003_11_14_17_16_29157)))|rr(X339,skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c284, c19])).
% 0.51/0.70 cnf(c288,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X337|skolem0005(i2003_11_14_17_16_29157)!=X338|rr(X337,X338),inference(resolution,[status(thm)],[c284, c10])).
% 0.51/0.70 fof(rr_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rr(A,C))=>rr(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rr_substitution_1)).
% 0.51/0.70 fof(c92,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.51/0.70 fof(c93,plain,(![X47]:(![X48]:(![X49]:((X47!=X48|~rr(X47,X49))|rr(X48,X49))))),inference(variable_rename,[status(thm)],[c92])).
% 0.51/0.70 cnf(c94,plain,X204!=X206|~rr(X204,X205)|rr(X206,X205),inference(split_conjunct,[status(thm)],[c93])).
% 0.51/0.70 cnf(c290,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X336|rr(X336,skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c284, c94])).
% 0.51/0.70 fof(rr_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rr(C,A))=>rr(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rr_substitution_2)).
% 0.51/0.70 fof(c89,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.51/0.70 fof(c90,plain,(![X44]:(![X45]:(![X46]:((X44!=X45|~rr(X46,X44))|rr(X46,X45))))),inference(variable_rename,[status(thm)],[c89])).
% 0.51/0.70 cnf(c91,plain,X202!=X201|~rr(X203,X202)|rr(X203,X201),inference(split_conjunct,[status(thm)],[c90])).
% 0.51/0.70 cnf(c289,plain,skolem0005(i2003_11_14_17_16_29157)!=X335|rr(skolem0001(skolem0005(i2003_11_14_17_16_29157)),X335),inference(resolution,[status(thm)],[c284, c91])).
% 0.51/0.70 cnf(c7,axiom,X146!=X148|X149!=X147|~rf(X146,X149)|rf(X148,X147),theory(equality)).
% 0.51/0.70 cnf(c285,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X333|skolem0005(i2003_11_14_17_16_29157)!=X334|rf(X333,X334),inference(resolution,[status(thm)],[c243, c7])).
% 0.51/0.70 fof(rf_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf(C,A))=>rf(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf_substitution_2)).
% 0.51/0.70 fof(c107,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.51/0.70 fof(c108,plain,(![X62]:(![X63]:(![X64]:((X62!=X63|~rf(X64,X62))|rf(X64,X63))))),inference(variable_rename,[status(thm)],[c107])).
% 0.51/0.70 cnf(c109,plain,X219!=X221|~rf(X220,X219)|rf(X220,X221),inference(split_conjunct,[status(thm)],[c108])).
% 0.51/0.70 cnf(c282,plain,skolem0005(i2003_11_14_17_16_29157)!=X332|rf(skolem0001(skolem0005(i2003_11_14_17_16_29157)),X332),inference(resolution,[status(thm)],[c243, c109])).
% 0.51/0.70 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.51/0.70 fof(c32,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.51/0.70 fof(c33,plain,(![X15]:(![X16]:(![X17]:((~rf(X15,X16)|~rf(X15,X17))|X16=X17)))),inference(variable_rename,[status(thm)],[c32])).
% 0.51/0.70 cnf(c34,plain,~rf(X193,X195)|~rf(X193,X194)|X195=X194,inference(split_conjunct,[status(thm)],[c33])).
% 0.51/0.70 cnf(c281,plain,~rf(skolem0001(skolem0005(i2003_11_14_17_16_29157)),X331)|X331=skolem0005(i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c243, c34])).
% 0.51/0.70 fof(rf_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rf(A,C))=>rf(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf_substitution_1)).
% 0.51/0.70 fof(c110,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.51/0.70 fof(c111,plain,(![X65]:(![X66]:(![X67]:((X65!=X66|~rf(X65,X67))|rf(X66,X67))))),inference(variable_rename,[status(thm)],[c110])).
% 0.51/0.70 cnf(c112,plain,X223!=X222|~rf(X223,X224)|rf(X222,X224),inference(split_conjunct,[status(thm)],[c111])).
% 0.51/0.70 cnf(c280,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X330|rf(X330,skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c243, c112])).
% 0.51/0.70 cnf(c8,axiom,X153!=X155|X156!=X154|~rinvF(X153,X156)|rinvF(X155,X154),theory(equality)).
% 0.51/0.70 cnf(c239,plain,skolem0005(i2003_11_14_17_16_29157)!=X328|skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X329|rinvF(X328,X329),inference(resolution,[status(thm)],[c148, c8])).
% 0.51/0.70 fof(rinvF_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvF(A,C))=>rinvF(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvF_substitution_1)).
% 0.51/0.70 fof(c104,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.51/0.70 fof(c105,plain,(![X59]:(![X60]:(![X61]:((X59!=X60|~rinvF(X59,X61))|rinvF(X60,X61))))),inference(variable_rename,[status(thm)],[c104])).
% 0.51/0.70 cnf(c106,plain,X216!=X217|~rinvF(X216,X218)|rinvF(X217,X218),inference(split_conjunct,[status(thm)],[c105])).
% 0.51/0.70 cnf(c241,plain,skolem0005(i2003_11_14_17_16_29157)!=X327|rinvF(X327,skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c148, c106])).
% 0.51/0.70 fof(rinvF_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvF(C,A))=>rinvF(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvF_substitution_2)).
% 0.51/0.70 fof(c101,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.51/0.70 fof(c102,plain,(![X56]:(![X57]:(![X58]:((X56!=X57|~rinvF(X58,X56))|rinvF(X58,X57))))),inference(variable_rename,[status(thm)],[c101])).
% 0.51/0.70 cnf(c103,plain,X213!=X214|~rinvF(X215,X213)|rinvF(X215,X214),inference(split_conjunct,[status(thm)],[c102])).
% 0.51/0.70 cnf(c240,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X326|rinvF(skolem0005(i2003_11_14_17_16_29157),X326),inference(resolution,[status(thm)],[c148, c103])).
% 0.51/0.70 cnf(c301,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X324|rinvR(i2003_11_14_17_16_29157,X324),inference(resolution,[status(thm)],[c297, c97])).
% 0.51/0.70 cnf(c300,plain,i2003_11_14_17_16_29157!=X323|rinvR(X323,skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c297, c100])).
% 0.51/0.70 cnf(c296,plain,~rr(X322,skolem0001(skolem0005(i2003_11_14_17_16_29157)))|rr(X322,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c287, c19])).
% 0.51/0.70 cnf(c295,plain,skolem0001(skolem0005(i2003_11_14_17_16_29157))!=X320|rr(X320,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c287, c94])).
% 0.51/0.70 cnf(c294,plain,i2003_11_14_17_16_29157!=X319|rr(skolem0001(skolem0005(i2003_11_14_17_16_29157)),X319),inference(resolution,[status(thm)],[c287, c91])).
% 0.51/0.70 fof(axiom_4,axiom,(![X]:(caxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.51/0.70 fof(c44,plain,(![X]:((~caxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|caxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.51/0.70 fof(c45,plain,((![X]:(~caxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|caxcomp(X)))),inference(shift_quantors,[status(thm)],[c44])).
% 0.51/0.70 fof(c46,plain,((![X22]:(~caxcomp(X22)|(?[X23]:ra_Px1(X22,X23))))&(![X24]:((![X25]:~ra_Px1(X24,X25))|caxcomp(X24)))),inference(variable_rename,[status(thm)],[c45])).
% 0.51/0.70 fof(c48,plain,(![X22]:(![X24]:(![X25]:((~caxcomp(X22)|ra_Px1(X22,skolem0002(X22)))&(~ra_Px1(X24,X25)|caxcomp(X24)))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X22]:(~caxcomp(X22)|ra_Px1(X22,skolem0002(X22))))&(![X24]:((![X25]:~ra_Px1(X24,X25))|caxcomp(X24)))),inference(skolemize,[status(esa)],[c46])).])).
% 0.51/0.70 cnf(c49,plain,~caxcomp(X129)|ra_Px1(X129,skolem0002(X129)),inference(split_conjunct,[status(thm)],[c48])).
% 0.51/0.70 cnf(c50,plain,~ra_Px1(X100,X99)|caxcomp(X100),inference(split_conjunct,[status(thm)],[c48])).
% 0.51/0.70 fof(axiom_3,axiom,(![X]:(ca(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.51/0.70 fof(c51,plain,(![X]:((~ca(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|ca(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.51/0.70 fof(c52,plain,((![X]:(~ca(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|ca(X)))),inference(shift_quantors,[status(thm)],[c51])).
% 0.51/0.70 fof(c53,plain,((![X26]:(~ca(X26)|(![X27]:~ra_Px1(X26,X27))))&(![X28]:((?[X29]:ra_Px1(X28,X29))|ca(X28)))),inference(variable_rename,[status(thm)],[c52])).
% 0.51/0.70 fof(c55,plain,(![X26]:(![X27]:(![X28]:((~ca(X26)|~ra_Px1(X26,X27))&(ra_Px1(X28,skolem0003(X28))|ca(X28)))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X26]:(~ca(X26)|(![X27]:~ra_Px1(X26,X27))))&(![X28]:(ra_Px1(X28,skolem0003(X28))|ca(X28)))),inference(skolemize,[status(esa)],[c53])).])).
% 0.51/0.70 cnf(c57,plain,ra_Px1(X133,skolem0003(X133))|ca(X133),inference(split_conjunct,[status(thm)],[c55])).
% 0.51/0.70 cnf(c153,plain,ca(X136)|caxcomp(X136),inference(resolution,[status(thm)],[c57, c50])).
% 0.51/0.70 cnf(c157,plain,ca(X150)|ra_Px1(X150,skolem0002(X150)),inference(resolution,[status(thm)],[c153, c49])).
% 0.51/0.70 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.51/0.70 fof(c116,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(A,C))|ra_Px1(B,C))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_1])).
% 0.51/0.70 fof(c117,plain,(![X71]:(![X72]:(![X73]:((X71!=X72|~ra_Px1(X71,X73))|ra_Px1(X72,X73))))),inference(variable_rename,[status(thm)],[c116])).
% 0.51/0.70 cnf(c118,plain,X230!=X228|~ra_Px1(X230,X229)|ra_Px1(X228,X229),inference(split_conjunct,[status(thm)],[c117])).
% 0.51/0.70 cnf(c237,plain,X311!=X312|ra_Px1(X312,skolem0002(X311))|ca(X311),inference(resolution,[status(thm)],[c118, c157])).
% 0.51/0.70 cnf(c65,plain,~cSatisfiable(X117)|ca(skolem0004(X117)),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 cnf(c143,plain,ca(skolem0004(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c65, c16])).
% 0.51/0.70 cnf(c64,plain,~cSatisfiable(X140)|rinvF(X140,skolem0004(X140)),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 cnf(c160,plain,rinvF(i2003_11_14_17_16_29157,skolem0004(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c64, c16])).
% 0.51/0.70 cnf(c43,plain,~rinvF(X168,X167)|~ca(X167)|ca_Vx2(X168),inference(split_conjunct,[status(thm)],[c40])).
% 0.51/0.70 cnf(c182,plain,~ca(skolem0004(i2003_11_14_17_16_29157))|ca_Vx2(i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c43, c160])).
% 0.51/0.70 cnf(c186,plain,ca_Vx2(i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c182, c143])).
% 0.51/0.70 cnf(c192,plain,rinvF(i2003_11_14_17_16_29157,skolem0001(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c186, c41])).
% 0.51/0.70 cnf(c195,plain,rf(skolem0001(i2003_11_14_17_16_29157),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c192, c30])).
% 0.51/0.70 cnf(c198,plain,rr(skolem0001(i2003_11_14_17_16_29157),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c195, c15])).
% 0.51/0.70 cnf(c205,plain,rinvR(i2003_11_14_17_16_29157,skolem0001(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c198, c25])).
% 0.51/0.70 cnf(c207,plain,i2003_11_14_17_16_29157!=X308|skolem0001(i2003_11_14_17_16_29157)!=X307|rinvR(X308,X307),inference(resolution,[status(thm)],[c205, c9])).
% 0.51/0.70 cnf(c235,plain,X306!=X305|ra_Px1(X305,skolem0003(X306))|ca(X306),inference(resolution,[status(thm)],[c118, c57])).
% 0.51/0.70 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.51/0.70 fof(c113,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(C,A))|ra_Px1(C,B))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_2])).
% 0.51/0.70 fof(c114,plain,(![X68]:(![X69]:(![X70]:((X68!=X69|~ra_Px1(X70,X68))|ra_Px1(X70,X69))))),inference(variable_rename,[status(thm)],[c113])).
% 0.51/0.70 cnf(c115,plain,X225!=X227|~ra_Px1(X226,X225)|ra_Px1(X226,X227),inference(split_conjunct,[status(thm)],[c114])).
% 0.51/0.70 cnf(c233,plain,skolem0002(X302)!=X303|ra_Px1(X302,X303)|ca(X302),inference(resolution,[status(thm)],[c115, c157])).
% 0.51/0.70 cnf(c203,plain,skolem0001(i2003_11_14_17_16_29157)!=X298|i2003_11_14_17_16_29157!=X299|rr(X298,X299),inference(resolution,[status(thm)],[c198, c10])).
% 0.51/0.70 cnf(c231,plain,skolem0003(X297)!=X296|ra_Px1(X297,X296)|ca(X297),inference(resolution,[status(thm)],[c115, c57])).
% 0.51/0.70 cnf(c199,plain,skolem0001(i2003_11_14_17_16_29157)!=X292|i2003_11_14_17_16_29157!=X293|rf(X292,X293),inference(resolution,[status(thm)],[c195, c7])).
% 0.51/0.70 cnf(c194,plain,i2003_11_14_17_16_29157!=X290|skolem0001(i2003_11_14_17_16_29157)!=X291|rinvF(X290,X291),inference(resolution,[status(thm)],[c192, c8])).
% 0.51/0.70 cnf(c56,plain,~ca(X101)|~ra_Px1(X101,X102),inference(split_conjunct,[status(thm)],[c55])).
% 0.51/0.70 cnf(c66,plain,~cSatisfiable(X89)|caxcomp(X89),inference(split_conjunct,[status(thm)],[c63])).
% 0.51/0.70 cnf(c137,plain,caxcomp(i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c66, c16])).
% 0.51/0.70 cnf(c149,plain,ra_Px1(i2003_11_14_17_16_29157,skolem0002(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c49, c137])).
% 0.51/0.70 cnf(c152,plain,~ca(i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c149, c56])).
% 0.51/0.70 cnf(c155,plain,ra_Px1(i2003_11_14_17_16_29157,skolem0003(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c57, c152])).
% 0.51/0.70 cnf(c238,plain,i2003_11_14_17_16_29157!=X281|ra_Px1(X281,skolem0003(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c118, c155])).
% 0.51/0.70 cnf(c236,plain,i2003_11_14_17_16_29157!=X280|ra_Px1(X280,skolem0002(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c118, c149])).
% 0.51/0.70 cnf(c234,plain,skolem0003(i2003_11_14_17_16_29157)!=X279|ra_Px1(i2003_11_14_17_16_29157,X279),inference(resolution,[status(thm)],[c115, c155])).
% 0.51/0.70 cnf(c184,plain,skolem0005(i2003_11_14_17_16_29157)!=X277|i2003_11_14_17_16_29157!=X278|rr(X277,X278),inference(resolution,[status(thm)],[c10, c170])).
% 0.51/0.70 cnf(c232,plain,skolem0002(i2003_11_14_17_16_29157)!=X276|ra_Px1(i2003_11_14_17_16_29157,X276),inference(resolution,[status(thm)],[c115, c149])).
% 0.51/0.70 cnf(c161,plain,rf(skolem0004(i2003_11_14_17_16_29157),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c160, c30])).
% 0.51/0.70 cnf(c230,plain,skolem0004(i2003_11_14_17_16_29157)!=X275|rf(X275,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c112, c161])).
% 0.51/0.70 cnf(c163,plain,rr(skolem0004(i2003_11_14_17_16_29157),i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c161, c15])).
% 0.51/0.70 cnf(c183,plain,skolem0004(i2003_11_14_17_16_29157)!=X273|i2003_11_14_17_16_29157!=X274|rr(X273,X274),inference(resolution,[status(thm)],[c10, c163])).
% 0.51/0.70 cnf(c229,plain,skolem0001(i2003_11_14_17_16_29157)!=X272|rf(X272,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c112, c195])).
% 0.51/0.70 cnf(c228,plain,i2003_11_14_17_16_29157!=X271|rf(skolem0004(i2003_11_14_17_16_29157),X271),inference(resolution,[status(thm)],[c109, c161])).
% 0.51/0.70 cnf(c227,plain,i2003_11_14_17_16_29157!=X270|rf(skolem0001(i2003_11_14_17_16_29157),X270),inference(resolution,[status(thm)],[c109, c195])).
% 0.51/0.70 cnf(c167,plain,rinvR(i2003_11_14_17_16_29157,skolem0004(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c163, c25])).
% 0.51/0.70 cnf(c181,plain,i2003_11_14_17_16_29157!=X269|skolem0004(i2003_11_14_17_16_29157)!=X268|rinvR(X269,X268),inference(resolution,[status(thm)],[c9, c167])).
% 0.51/0.70 cnf(c226,plain,i2003_11_14_17_16_29157!=X267|rinvF(X267,skolem0001(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c106, c192])).
% 0.51/0.70 cnf(c225,plain,i2003_11_14_17_16_29157!=X266|rinvF(X266,skolem0004(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c106, c160])).
% 0.51/0.70 cnf(c180,plain,i2003_11_14_17_16_29157!=X265|skolem0005(i2003_11_14_17_16_29157)!=X264|rinvR(X265,X264),inference(resolution,[status(thm)],[c9, c169])).
% 0.51/0.70 cnf(c224,plain,skolem0001(i2003_11_14_17_16_29157)!=X263|rinvF(i2003_11_14_17_16_29157,X263),inference(resolution,[status(thm)],[c103, c192])).
% 0.51/0.70 cnf(c223,plain,skolem0004(i2003_11_14_17_16_29157)!=X262|rinvF(i2003_11_14_17_16_29157,X262),inference(resolution,[status(thm)],[c103, c160])).
% 0.51/0.70 cnf(c222,plain,i2003_11_14_17_16_29157!=X261|rinvR(X261,skolem0001(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c100, c205])).
% 0.51/0.70 cnf(c177,plain,i2003_11_14_17_16_29157!=X259|skolem0004(i2003_11_14_17_16_29157)!=X260|rinvF(X259,X260),inference(resolution,[status(thm)],[c8, c160])).
% 0.51/0.70 cnf(c221,plain,i2003_11_14_17_16_29157!=X258|rinvR(X258,skolem0004(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c100, c167])).
% 0.51/0.70 cnf(c220,plain,i2003_11_14_17_16_29157!=X257|rinvR(X257,skolem0005(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c100, c169])).
% 0.51/0.70 cnf(c6,axiom,X141!=X143|X144!=X142|~ra_Px1(X141,X144)|ra_Px1(X143,X142),theory(equality)).
% 0.51/0.70 cnf(c176,plain,ca(X255)|X255!=X256|skolem0002(X255)!=X254|ra_Px1(X256,X254),inference(resolution,[status(thm)],[c157, c6])).
% 0.51/0.70 cnf(c219,plain,skolem0001(i2003_11_14_17_16_29157)!=X253|rinvR(i2003_11_14_17_16_29157,X253),inference(resolution,[status(thm)],[c97, c205])).
% 0.51/0.70 cnf(c218,plain,skolem0004(i2003_11_14_17_16_29157)!=X252|rinvR(i2003_11_14_17_16_29157,X252),inference(resolution,[status(thm)],[c97, c167])).
% 0.51/0.70 cnf(c217,plain,skolem0005(i2003_11_14_17_16_29157)!=X251|rinvR(i2003_11_14_17_16_29157,X251),inference(resolution,[status(thm)],[c97, c169])).
% 0.51/0.70 cnf(c171,plain,skolem0004(i2003_11_14_17_16_29157)!=X249|i2003_11_14_17_16_29157!=X250|rf(X249,X250),inference(resolution,[status(thm)],[c7, c161])).
% 0.51/0.70 cnf(c216,plain,skolem0005(i2003_11_14_17_16_29157)!=X248|rr(X248,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c94, c170])).
% 0.51/0.70 cnf(c215,plain,skolem0004(i2003_11_14_17_16_29157)!=X247|rr(X247,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c94, c163])).
% 0.51/0.70 cnf(c166,plain,i2003_11_14_17_16_29157!=X246|skolem0003(i2003_11_14_17_16_29157)!=X245|ra_Px1(X246,X245),inference(resolution,[status(thm)],[c6, c155])).
% 0.51/0.70 cnf(c214,plain,skolem0001(i2003_11_14_17_16_29157)!=X244|rr(X244,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c94, c198])).
% 0.51/0.70 cnf(c213,plain,i2003_11_14_17_16_29157!=X243|rr(skolem0005(i2003_11_14_17_16_29157),X243),inference(resolution,[status(thm)],[c91, c170])).
% 0.51/0.70 cnf(c212,plain,i2003_11_14_17_16_29157!=X242|rr(skolem0004(i2003_11_14_17_16_29157),X242),inference(resolution,[status(thm)],[c91, c163])).
% 0.51/0.70 cnf(c165,plain,i2003_11_14_17_16_29157!=X241|skolem0002(i2003_11_14_17_16_29157)!=X240|ra_Px1(X241,X240),inference(resolution,[status(thm)],[c6, c149])).
% 0.51/0.70 cnf(c211,plain,i2003_11_14_17_16_29157!=X239|rr(skolem0001(i2003_11_14_17_16_29157),X239),inference(resolution,[status(thm)],[c91, c198])).
% 0.51/0.70 cnf(c204,plain,~rr(X238,skolem0001(i2003_11_14_17_16_29157))|rr(X238,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c198, c19])).
% 0.51/0.70 cnf(c202,plain,~rf(skolem0004(i2003_11_14_17_16_29157),X237)|X237=i2003_11_14_17_16_29157,inference(resolution,[status(thm)],[c34, c161])).
% 0.51/0.70 cnf(c164,plain,X236!=X235|skolem0003(X236)!=X234|ra_Px1(X235,X234)|ca(X236),inference(resolution,[status(thm)],[c6, c57])).
% 0.51/0.70 cnf(c201,plain,~rf(skolem0001(i2003_11_14_17_16_29157),X233)|X233=i2003_11_14_17_16_29157,inference(resolution,[status(thm)],[c34, c195])).
% 0.51/0.70 cnf(c190,plain,~rr(X231,skolem0004(i2003_11_14_17_16_29157))|rr(X231,i2003_11_14_17_16_29157),inference(resolution,[status(thm)],[c19, c163])).
% 0.51/0.70 cnf(c42,plain,~ca_Vx2(X116)|ca(skolem0001(X116)),inference(split_conjunct,[status(thm)],[c40])).
% 0.51/0.70 cnf(c193,plain,ca(skolem0001(i2003_11_14_17_16_29157)),inference(resolution,[status(thm)],[c186, c42])).
% 0.51/0.70 cnf(c12,axiom,X160!=X161|~xsd_string(X160)|xsd_string(X161),theory(equality)).
% 0.51/0.70 cnf(c11,axiom,X157!=X158|~xsd_integer(X157)|xsd_integer(X158),theory(equality)).
% 0.51/0.70 cnf(c3,axiom,X130!=X131|~caxcomp(X130)|caxcomp(X131),theory(equality)).
% 0.51/0.70 cnf(c146,plain,ca(skolem0001(skolem0005(i2003_11_14_17_16_29157))),inference(resolution,[status(thm)],[c145, c42])).
% 0.51/0.70 cnf(c2,axiom,X123!=X124|~ca_Vx2(X123)|ca_Vx2(X124),theory(equality)).
% 0.51/0.70 cnf(c1,axiom,X118!=X119|~ca(X118)|ca(X119),theory(equality)).
% 0.51/0.70 cnf(c31,plain,~rf(X114,X115)|rinvF(X115,X114),inference(split_conjunct,[status(thm)],[c29])).
% 0.51/0.70 cnf(c0,axiom,X109!=X110|~cSatisfiable(X109)|cSatisfiable(X110),theory(equality)).
% 0.51/0.70 cnf(transitivity,axiom,X96!=X98|X98!=X97|X96=X97,theory(equality)).
% 0.51/0.70 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.51/0.70 fof(c70,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.51/0.70 fof(c71,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c70])).
% 0.51/0.70 fof(c72,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 0.51/0.70 fof(c74,plain,(![X36]:(![X37]:((~xsd_string(X36)|~xsd_integer(X36))&(xsd_integer(X37)|xsd_string(X37))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X36]:(~xsd_string(X36)|~xsd_integer(X36)))&(![X37]:(xsd_integer(X37)|xsd_string(X37)))),inference(variable_rename,[status(thm)],[c72])).])).
% 0.51/0.70 cnf(c76,plain,xsd_integer(X94)|xsd_string(X94),inference(split_conjunct,[status(thm)],[c74])).
% 0.51/0.70 cnf(c75,plain,~xsd_string(X93)|~xsd_integer(X93),inference(split_conjunct,[status(thm)],[c74])).
% 0.51/0.70 cnf(symmetry,axiom,X90!=X91|X91=X90,theory(equality)).
% 0.51/0.70 cnf(reflexivity,axiom,X88=X88,theory(equality)).
% 0.51/0.70 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.51/0.70 fof(c77,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.51/0.70 fof(c78,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c77])).
% 0.51/0.70 fof(c80,plain,(![X38]:(![X39]:(cowlThing(X38)&~cowlNothing(X39)))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X38]:cowlThing(X38))&(![X39]:~cowlNothing(X39))),inference(variable_rename,[status(thm)],[c78])).])).
% 0.51/0.70 cnf(c82,plain,~cowlNothing(X87),inference(split_conjunct,[status(thm)],[c80])).
% 0.51/0.70 cnf(c81,plain,cowlThing(X86),inference(split_conjunct,[status(thm)],[c80])).
% 0.51/0.70 % SZS output end Saturation
% 0.51/0.70
% 0.51/0.70 % Initial clauses : 59
% 0.51/0.70 % Processed clauses : 146
% 0.51/0.70 % Factors computed : 3
% 0.51/0.70 % Resolvents computed: 194
% 0.51/0.70 % Tautologies deleted: 12
% 0.51/0.70 % Forward subsumed : 98
% 0.51/0.70 % Backward subsumed : 1
% 0.51/0.70 % -------- CPU Time ---------
% 0.51/0.70 % User time : 0.317 s
% 0.51/0.70 % System time : 0.020 s
% 0.51/0.70 % Total time : 0.337 s
%------------------------------------------------------------------------------