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