%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS035+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:28:31 EDT 2024
% Result : Satisfiable 0.44s 0.70s
% Output : Saturation 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : KRS035+1 : TPTP v8.1.2. Released v3.1.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n014.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 9 00:04:53 EDT 2024
% 0.15/0.35 % CPUTime :
% 0.44/0.70 % Version: 1.5
% 0.44/0.70 % SZS status Satisfiable
% 0.44/0.70 % SZS output start Saturation
% 0.44/0.70 fof(axiom_5,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.44/0.70 fof(c17,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.44/0.70 fof(c18,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c17])).
% 0.44/0.70 fof(c20,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~rinvR(X7,X8)|rr(X8,X7))&(~rr(X10,X9)|rinvR(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,((![X7]:(![X8]:(~rinvR(X7,X8)|rr(X8,X7))))&(![X9]:(![X10]:(~rr(X10,X9)|rinvR(X9,X10))))),inference(variable_rename,[status(thm)],[c18])).])).
% 0.44/0.70 cnf(c22,plain,~rr(X84,X83)|rinvR(X83,X84),inference(split_conjunct,[status(thm)],[c20])).
% 0.44/0.70 fof(axiom_8,axiom,(![X]:(![Y]:(rf(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.44/0.70 fof(c10,plain,(![X]:(![Y]:(~rf(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.44/0.70 fof(c11,plain,(![X2]:(![X3]:(~rf(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c10])).
% 0.44/0.70 cnf(c12,plain,~rf(X76,X77)|rr(X76,X77),inference(split_conjunct,[status(thm)],[c11])).
% 0.44/0.70 fof(axiom_4,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.44/0.70 fof(c23,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.44/0.70 fof(c24,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c23])).
% 0.44/0.70 fof(c26,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~rinvF(X11,X12)|rf(X12,X11))&(~rf(X14,X13)|rinvF(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X11]:(![X12]:(~rinvF(X11,X12)|rf(X12,X11))))&(![X13]:(![X14]:(~rf(X14,X13)|rinvF(X13,X14))))),inference(variable_rename,[status(thm)],[c24])).])).
% 0.44/0.70 cnf(c27,plain,~rinvF(X85,X86)|rf(X86,X85),inference(split_conjunct,[status(thm)],[c26])).
% 0.44/0.70 fof(axiom_7,axiom,cSatisfiable(i2003_11_14_17_15_44810),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.44/0.70 cnf(c13,plain,cSatisfiable(i2003_11_14_17_15_44810),inference(split_conjunct,[status(thm)],[axiom_7])).
% 0.44/0.70 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>(((~ca(X))&(?[Y]:(rinvR(X,Y)&(?[Z]:(rinvF(Y,Z)&ca(Z))))))&(?[Y]:(rinvF(X,Y)&ca(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.44/0.70 fof(c33,plain,(![X]:(cSatisfiable(X)<=>((~ca(X)&(?[Y]:(rinvR(X,Y)&(?[Z]:(rinvF(Y,Z)&ca(Z))))))&(?[Y]:(rinvF(X,Y)&ca(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.44/0.70 fof(c34,plain,(![X]:((~cSatisfiable(X)|((~ca(X)&(?[Y]:(rinvR(X,Y)&(?[Z]:(rinvF(Y,Z)&ca(Z))))))&(?[Y]:(rinvF(X,Y)&ca(Y)))))&(((ca(X)|(![Y]:(~rinvR(X,Y)|(![Z]:(~rinvF(Y,Z)|~ca(Z))))))|(![Y]:(~rinvF(X,Y)|~ca(Y))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[c33])).
% 0.44/0.70 fof(c35,plain,((![X]:(~cSatisfiable(X)|((~ca(X)&(?[Y]:(rinvR(X,Y)&(?[Z]:(rinvF(Y,Z)&ca(Z))))))&(?[Y]:(rinvF(X,Y)&ca(Y))))))&(![X]:(((ca(X)|(![Y]:(~rinvR(X,Y)|(![Z]:(~rinvF(Y,Z)|~ca(Z))))))|(![Y]:(~rinvF(X,Y)|~ca(Y))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c34])).
% 0.44/0.70 fof(c36,plain,((![X18]:(~cSatisfiable(X18)|((~ca(X18)&(?[X19]:(rinvR(X18,X19)&(?[X20]:(rinvF(X19,X20)&ca(X20))))))&(?[X21]:(rinvF(X18,X21)&ca(X21))))))&(![X22]:(((ca(X22)|(![X23]:(~rinvR(X22,X23)|(![X24]:(~rinvF(X23,X24)|~ca(X24))))))|(![X25]:(~rinvF(X22,X25)|~ca(X25))))|cSatisfiable(X22)))),inference(variable_rename,[status(thm)],[c35])).
% 0.44/0.70 fof(c38,plain,(![X18]:(![X22]:(![X23]:(![X24]:(![X25]:((~cSatisfiable(X18)|((~ca(X18)&(rinvR(X18,skolem0001(X18))&(rinvF(skolem0001(X18),skolem0002(X18))&ca(skolem0002(X18)))))&(rinvF(X18,skolem0003(X18))&ca(skolem0003(X18)))))&(((ca(X22)|(~rinvR(X22,X23)|(~rinvF(X23,X24)|~ca(X24))))|(~rinvF(X22,X25)|~ca(X25)))|cSatisfiable(X22)))))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X18]:(~cSatisfiable(X18)|((~ca(X18)&(rinvR(X18,skolem0001(X18))&(rinvF(skolem0001(X18),skolem0002(X18))&ca(skolem0002(X18)))))&(rinvF(X18,skolem0003(X18))&ca(skolem0003(X18))))))&(![X22]:(((ca(X22)|(![X23]:(~rinvR(X22,X23)|(![X24]:(~rinvF(X23,X24)|~ca(X24))))))|(![X25]:(~rinvF(X22,X25)|~ca(X25))))|cSatisfiable(X22)))),inference(skolemize,[status(esa)],[c36])).])).
% 0.44/0.70 fof(c39,plain,(![X18]:(![X22]:(![X23]:(![X24]:(![X25]:((((~cSatisfiable(X18)|~ca(X18))&((~cSatisfiable(X18)|rinvR(X18,skolem0001(X18)))&((~cSatisfiable(X18)|rinvF(skolem0001(X18),skolem0002(X18)))&(~cSatisfiable(X18)|ca(skolem0002(X18))))))&((~cSatisfiable(X18)|rinvF(X18,skolem0003(X18)))&(~cSatisfiable(X18)|ca(skolem0003(X18)))))&(((ca(X22)|(~rinvR(X22,X23)|(~rinvF(X23,X24)|~ca(X24))))|(~rinvF(X22,X25)|~ca(X25)))|cSatisfiable(X22)))))))),inference(distribute,[status(thm)],[c38])).
% 0.44/0.70 cnf(c42,plain,~cSatisfiable(X136)|rinvF(skolem0001(X136),skolem0002(X136)),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c127,plain,rinvF(skolem0001(i2003_11_14_17_15_44810),skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c42, c13])).
% 0.44/0.70 cnf(c129,plain,rf(skolem0002(i2003_11_14_17_15_44810),skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c127, c27])).
% 0.44/0.70 cnf(c132,plain,rr(skolem0002(i2003_11_14_17_15_44810),skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c129, c12])).
% 0.44/0.70 cnf(c133,plain,rinvR(skolem0001(i2003_11_14_17_15_44810),skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c132, c22])).
% 0.44/0.70 cnf(c46,plain,ca(X166)|~rinvR(X166,X165)|~rinvF(X165,X168)|~ca(X168)|~rinvF(X166,X167)|~ca(X167)|cSatisfiable(X166),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c161,plain,ca(skolem0001(i2003_11_14_17_15_44810))|~rinvR(skolem0001(i2003_11_14_17_15_44810),X242)|~rinvF(X242,X243)|~ca(X243)|~ca(skolem0002(i2003_11_14_17_15_44810))|cSatisfiable(skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c46, c127])).
% 0.44/0.70 cnf(c218,plain,ca(skolem0001(i2003_11_14_17_15_44810))|~rinvF(skolem0002(i2003_11_14_17_15_44810),X250)|~ca(X250)|~ca(skolem0002(i2003_11_14_17_15_44810))|cSatisfiable(skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c161, c133])).
% 0.44/0.70 cnf(c160,plain,ca(X234)|~rinvR(X234,X234)|~rinvF(X234,X235)|~ca(X235)|cSatisfiable(X234),inference(factor,[status(thm)],[c46])).
% 0.44/0.70 cnf(c215,plain,ca(skolem0001(i2003_11_14_17_15_44810))|~rinvR(skolem0001(i2003_11_14_17_15_44810),skolem0001(i2003_11_14_17_15_44810))|~ca(skolem0002(i2003_11_14_17_15_44810))|cSatisfiable(skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c160, c127])).
% 0.44/0.70 cnf(c6,axiom,X134!=X133|X132!=X135|~rinvR(X134,X132)|rinvR(X133,X135),theory(equality)).
% 0.44/0.70 cnf(c21,plain,~rinvR(X81,X82)|rr(X82,X81),inference(split_conjunct,[status(thm)],[c20])).
% 0.44/0.70 cnf(c41,plain,~cSatisfiable(X100)|rinvR(X100,skolem0001(X100)),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c112,plain,rinvR(i2003_11_14_17_15_44810,skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c41, c13])).
% 0.44/0.70 cnf(c113,plain,rr(skolem0001(i2003_11_14_17_15_44810),i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c112, c21])).
% 0.44/0.70 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rr(X,Y)&rr(Y,Z))=>rr(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.44/0.70 fof(c14,plain,(![X]:(![Y]:(![Z]:((~rr(X,Y)|~rr(Y,Z))|rr(X,Z))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.44/0.70 fof(c15,plain,(![X4]:(![X5]:(![X6]:((~rr(X4,X5)|~rr(X5,X6))|rr(X4,X6))))),inference(variable_rename,[status(thm)],[c14])).
% 0.44/0.70 cnf(c16,plain,~rr(X143,X141)|~rr(X141,X142)|rr(X143,X142),inference(split_conjunct,[status(thm)],[c15])).
% 0.44/0.70 cnf(c140,plain,~rr(X178,skolem0001(i2003_11_14_17_15_44810))|rr(X178,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c16, c113])).
% 0.44/0.70 cnf(c169,plain,rr(skolem0002(i2003_11_14_17_15_44810),i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c140, c132])).
% 0.44/0.70 cnf(c173,plain,rinvR(i2003_11_14_17_15_44810,skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c169, c22])).
% 0.44/0.70 cnf(c178,plain,i2003_11_14_17_15_44810!=X246|skolem0002(i2003_11_14_17_15_44810)!=X245|rinvR(X246,X245),inference(resolution,[status(thm)],[c173, c6])).
% 0.44/0.70 cnf(c7,axiom,X139!=X138|X137!=X140|~rr(X139,X137)|rr(X138,X140),theory(equality)).
% 0.44/0.70 cnf(c172,plain,skolem0002(i2003_11_14_17_15_44810)!=X240|i2003_11_14_17_15_44810!=X241|rr(X240,X241),inference(resolution,[status(thm)],[c169, c7])).
% 0.44/0.70 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.44/0.70 fof(c87,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.44/0.70 fof(c88,plain,(![X55]:(![X56]:(![X57]:((X55!=X56|~rf(X55,X57))|rf(X56,X57))))),inference(variable_rename,[status(thm)],[c87])).
% 0.44/0.70 cnf(c89,plain,X177!=X176|~rf(X177,X175)|rf(X176,X175),inference(split_conjunct,[status(thm)],[c88])).
% 0.44/0.70 cnf(c168,plain,skolem0002(i2003_11_14_17_15_44810)!=X233|rf(X233,skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c89, c129])).
% 0.44/0.70 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.44/0.70 fof(c84,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.44/0.70 fof(c85,plain,(![X52]:(![X53]:(![X54]:((X52!=X53|~rf(X54,X52))|rf(X54,X53))))),inference(variable_rename,[status(thm)],[c84])).
% 0.44/0.70 cnf(c86,plain,X174!=X172|~rf(X173,X174)|rf(X173,X172),inference(split_conjunct,[status(thm)],[c85])).
% 0.44/0.70 cnf(c166,plain,skolem0001(i2003_11_14_17_15_44810)!=X232|rf(skolem0002(i2003_11_14_17_15_44810),X232),inference(resolution,[status(thm)],[c86, c129])).
% 0.44/0.70 fof(axiom_3,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf(X,Y0)&rf(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.44/0.70 fof(c29,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf(X,Y0)|~rf(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.44/0.70 fof(c31,plain,(![X15]:(![X16]:(![X17]:(~cowlThing(X15)|((~rf(X15,X16)|~rf(X15,X17))|X16=X17))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,(![X15]:(~cowlThing(X15)|(![X16]:(![X17]:((~rf(X15,X16)|~rf(X15,X17))|X16=X17))))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.44/0.70 cnf(c32,plain,~cowlThing(X150)|~rf(X150,X148)|~rf(X150,X149)|X148=X149,inference(split_conjunct,[status(thm)],[c31])).
% 0.44/0.70 cnf(c148,plain,~cowlThing(skolem0002(i2003_11_14_17_15_44810))|~rf(skolem0002(i2003_11_14_17_15_44810),X231)|X231=skolem0001(i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c32, c129])).
% 0.44/0.70 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.44/0.70 fof(c81,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.44/0.70 fof(c82,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rinvF(X49,X51))|rinvF(X50,X51))))),inference(variable_rename,[status(thm)],[c81])).
% 0.44/0.70 cnf(c83,plain,X170!=X171|~rinvF(X170,X169)|rinvF(X171,X169),inference(split_conjunct,[status(thm)],[c82])).
% 0.44/0.70 cnf(c163,plain,skolem0001(i2003_11_14_17_15_44810)!=X230|rinvF(X230,skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c83, c127])).
% 0.44/0.70 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.44/0.70 fof(c78,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.44/0.70 fof(c79,plain,(![X46]:(![X47]:(![X48]:((X46!=X47|~rinvF(X48,X46))|rinvF(X48,X47))))),inference(variable_rename,[status(thm)],[c78])).
% 0.44/0.70 cnf(c80,plain,X163!=X162|~rinvF(X164,X163)|rinvF(X164,X162),inference(split_conjunct,[status(thm)],[c79])).
% 0.44/0.70 cnf(c158,plain,skolem0002(i2003_11_14_17_15_44810)!=X229|rinvF(skolem0001(i2003_11_14_17_15_44810),X229),inference(resolution,[status(thm)],[c80, c127])).
% 0.44/0.70 cnf(c44,plain,~cSatisfiable(X103)|rinvF(X103,skolem0003(X103)),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c115,plain,rinvF(i2003_11_14_17_15_44810,skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c44, c13])).
% 0.44/0.70 cnf(c116,plain,rf(skolem0003(i2003_11_14_17_15_44810),i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c115, c27])).
% 0.44/0.70 cnf(c147,plain,~cowlThing(skolem0003(i2003_11_14_17_15_44810))|~rf(skolem0003(i2003_11_14_17_15_44810),X228)|X228=i2003_11_14_17_15_44810,inference(resolution,[status(thm)],[c32, c116])).
% 0.44/0.70 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.44/0.70 fof(c75,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(A,C))|rinvR(B,C))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_1])).
% 0.44/0.70 fof(c76,plain,(![X43]:(![X44]:(![X45]:((X43!=X44|~rinvR(X43,X45))|rinvR(X44,X45))))),inference(variable_rename,[status(thm)],[c75])).
% 0.44/0.70 cnf(c77,plain,X159!=X161|~rinvR(X159,X160)|rinvR(X161,X160),inference(split_conjunct,[status(thm)],[c76])).
% 0.44/0.70 cnf(c157,plain,skolem0001(i2003_11_14_17_15_44810)!=X227|rinvR(X227,skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c77, c133])).
% 0.44/0.70 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.44/0.70 fof(c72,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(C,A))|rinvR(C,B))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_2])).
% 0.44/0.70 fof(c73,plain,(![X40]:(![X41]:(![X42]:((X40!=X41|~rinvR(X42,X40))|rinvR(X42,X41))))),inference(variable_rename,[status(thm)],[c72])).
% 0.44/0.70 cnf(c74,plain,X158!=X156|~rinvR(X157,X158)|rinvR(X157,X156),inference(split_conjunct,[status(thm)],[c73])).
% 0.44/0.70 cnf(c154,plain,skolem0002(i2003_11_14_17_15_44810)!=X226|rinvR(skolem0001(i2003_11_14_17_15_44810),X226),inference(resolution,[status(thm)],[c74, c133])).
% 0.44/0.70 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.44/0.70 fof(c69,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.44/0.70 fof(c70,plain,(![X37]:(![X38]:(![X39]:((X37!=X38|~rr(X37,X39))|rr(X38,X39))))),inference(variable_rename,[status(thm)],[c69])).
% 0.44/0.70 cnf(c71,plain,X155!=X154|~rr(X155,X153)|rr(X154,X153),inference(split_conjunct,[status(thm)],[c70])).
% 0.44/0.70 cnf(c150,plain,skolem0002(i2003_11_14_17_15_44810)!=X225|rr(X225,skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c71, c132])).
% 0.44/0.70 cnf(c138,plain,skolem0001(i2003_11_14_17_15_44810)!=X224|skolem0002(i2003_11_14_17_15_44810)!=X223|rinvR(X224,X223),inference(resolution,[status(thm)],[c133, c6])).
% 0.44/0.70 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.44/0.70 fof(c66,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.44/0.70 fof(c67,plain,(![X34]:(![X35]:(![X36]:((X34!=X35|~rr(X36,X34))|rr(X36,X35))))),inference(variable_rename,[status(thm)],[c66])).
% 0.44/0.70 cnf(c68,plain,X147!=X146|~rr(X145,X147)|rr(X145,X146),inference(split_conjunct,[status(thm)],[c67])).
% 0.44/0.70 cnf(c144,plain,skolem0001(i2003_11_14_17_15_44810)!=X222|rr(skolem0002(i2003_11_14_17_15_44810),X222),inference(resolution,[status(thm)],[c68, c132])).
% 0.44/0.70 cnf(c141,plain,~rr(X221,skolem0002(i2003_11_14_17_15_44810))|rr(X221,skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c16, c132])).
% 0.44/0.70 cnf(c118,plain,rr(skolem0003(i2003_11_14_17_15_44810),i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c116, c12])).
% 0.44/0.70 cnf(c136,plain,skolem0003(i2003_11_14_17_15_44810)!=X217|i2003_11_14_17_15_44810!=X218|rr(X217,X218),inference(resolution,[status(thm)],[c7, c118])).
% 0.44/0.70 cnf(c179,plain,skolem0002(i2003_11_14_17_15_44810)!=X213|rinvR(i2003_11_14_17_15_44810,X213),inference(resolution,[status(thm)],[c173, c74])).
% 0.44/0.70 cnf(c135,plain,skolem0002(i2003_11_14_17_15_44810)!=X211|skolem0001(i2003_11_14_17_15_44810)!=X212|rr(X211,X212),inference(resolution,[status(thm)],[c7, c132])).
% 0.44/0.70 cnf(c177,plain,i2003_11_14_17_15_44810!=X210|rinvR(X210,skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c173, c77])).
% 0.44/0.70 cnf(c174,plain,skolem0002(i2003_11_14_17_15_44810)!=X208|rr(X208,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c169, c71])).
% 0.44/0.70 cnf(c134,plain,skolem0001(i2003_11_14_17_15_44810)!=X206|i2003_11_14_17_15_44810!=X207|rr(X206,X207),inference(resolution,[status(thm)],[c7, c113])).
% 0.44/0.70 cnf(c171,plain,~rr(X205,skolem0002(i2003_11_14_17_15_44810))|rr(X205,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c169, c16])).
% 0.44/0.70 cnf(c170,plain,i2003_11_14_17_15_44810!=X204|rr(skolem0002(i2003_11_14_17_15_44810),X204),inference(resolution,[status(thm)],[c169, c68])).
% 0.44/0.70 cnf(c167,plain,skolem0003(i2003_11_14_17_15_44810)!=X203|rf(X203,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c89, c116])).
% 0.44/0.70 cnf(c4,axiom,X108!=X107|X106!=X109|~rf(X108,X106)|rf(X107,X109),theory(equality)).
% 0.44/0.70 cnf(c130,plain,skolem0002(i2003_11_14_17_15_44810)!=X202|skolem0001(i2003_11_14_17_15_44810)!=X201|rf(X202,X201),inference(resolution,[status(thm)],[c129, c4])).
% 0.44/0.70 cnf(c165,plain,i2003_11_14_17_15_44810!=X200|rf(skolem0003(i2003_11_14_17_15_44810),X200),inference(resolution,[status(thm)],[c86, c116])).
% 0.44/0.70 cnf(c164,plain,i2003_11_14_17_15_44810!=X199|rinvF(X199,skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c83, c115])).
% 0.44/0.70 cnf(c5,axiom,X120!=X119|X118!=X121|~rinvF(X120,X118)|rinvF(X119,X121),theory(equality)).
% 0.44/0.70 cnf(c128,plain,skolem0001(i2003_11_14_17_15_44810)!=X198|skolem0002(i2003_11_14_17_15_44810)!=X197|rinvF(X198,X197),inference(resolution,[status(thm)],[c127, c5])).
% 0.44/0.70 cnf(c159,plain,skolem0003(i2003_11_14_17_15_44810)!=X196|rinvF(i2003_11_14_17_15_44810,X196),inference(resolution,[status(thm)],[c80, c115])).
% 0.44/0.70 cnf(c156,plain,i2003_11_14_17_15_44810!=X195|rinvR(X195,skolem0001(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c77, c112])).
% 0.44/0.70 cnf(c119,plain,rinvR(i2003_11_14_17_15_44810,skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c118, c22])).
% 0.44/0.70 cnf(c155,plain,i2003_11_14_17_15_44810!=X194|rinvR(X194,skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c77, c119])).
% 0.44/0.70 cnf(c126,plain,i2003_11_14_17_15_44810!=X193|skolem0001(i2003_11_14_17_15_44810)!=X192|rinvR(X193,X192),inference(resolution,[status(thm)],[c6, c112])).
% 0.44/0.70 cnf(c153,plain,skolem0001(i2003_11_14_17_15_44810)!=X191|rinvR(i2003_11_14_17_15_44810,X191),inference(resolution,[status(thm)],[c74, c112])).
% 0.44/0.70 cnf(c152,plain,skolem0003(i2003_11_14_17_15_44810)!=X190|rinvR(i2003_11_14_17_15_44810,X190),inference(resolution,[status(thm)],[c74, c119])).
% 0.44/0.70 cnf(c125,plain,i2003_11_14_17_15_44810!=X189|skolem0003(i2003_11_14_17_15_44810)!=X188|rinvR(X189,X188),inference(resolution,[status(thm)],[c6, c119])).
% 0.44/0.70 cnf(c151,plain,skolem0003(i2003_11_14_17_15_44810)!=X187|rr(X187,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c71, c118])).
% 0.44/0.70 cnf(c149,plain,skolem0001(i2003_11_14_17_15_44810)!=X186|rr(X186,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c71, c113])).
% 0.44/0.70 cnf(c145,plain,i2003_11_14_17_15_44810!=X185|rr(skolem0003(i2003_11_14_17_15_44810),X185),inference(resolution,[status(thm)],[c68, c118])).
% 0.44/0.70 cnf(c124,plain,i2003_11_14_17_15_44810!=X184|skolem0003(i2003_11_14_17_15_44810)!=X183|rinvF(X184,X183),inference(resolution,[status(thm)],[c5, c115])).
% 0.44/0.70 cnf(c143,plain,i2003_11_14_17_15_44810!=X182|rr(skolem0001(i2003_11_14_17_15_44810),X182),inference(resolution,[status(thm)],[c68, c113])).
% 0.44/0.70 cnf(c142,plain,~rr(X181,skolem0003(i2003_11_14_17_15_44810))|rr(X181,i2003_11_14_17_15_44810),inference(resolution,[status(thm)],[c16, c118])).
% 0.44/0.70 cnf(c121,plain,skolem0003(i2003_11_14_17_15_44810)!=X180|i2003_11_14_17_15_44810!=X179|rf(X180,X179),inference(resolution,[status(thm)],[c4, c116])).
% 0.44/0.70 cnf(c9,axiom,X114!=X113|~xsd_string(X114)|xsd_string(X113),theory(equality)).
% 0.44/0.70 cnf(c8,axiom,X111!=X110|~xsd_integer(X111)|xsd_integer(X110),theory(equality)).
% 0.44/0.70 cnf(c40,plain,~cSatisfiable(X69)|~ca(X69),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c45,plain,~cSatisfiable(X93)|ca(skolem0003(X93)),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c109,plain,ca(skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c45, c13])).
% 0.44/0.70 cnf(c110,plain,~cSatisfiable(skolem0003(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c109, c40])).
% 0.44/0.70 cnf(c1,axiom,X95!=X94|~ca(X95)|ca(X94),theory(equality)).
% 0.44/0.70 cnf(c43,plain,~cSatisfiable(X89)|ca(skolem0002(X89)),inference(split_conjunct,[status(thm)],[c39])).
% 0.44/0.70 cnf(c106,plain,ca(skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c43, c13])).
% 0.44/0.70 cnf(c108,plain,~cSatisfiable(skolem0002(i2003_11_14_17_15_44810)),inference(resolution,[status(thm)],[c106, c40])).
% 0.44/0.70 cnf(c0,axiom,X91!=X90|~cSatisfiable(X91)|cSatisfiable(X90),theory(equality)).
% 0.44/0.70 cnf(c28,plain,~rf(X88,X87)|rinvF(X87,X88),inference(split_conjunct,[status(thm)],[c26])).
% 0.44/0.70 cnf(transitivity,axiom,X79!=X78|X78!=X80|X79=X80,theory(equality)).
% 0.44/0.70 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.44/0.70 fof(c47,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.44/0.70 fof(c48,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c47])).
% 0.44/0.70 fof(c49,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c48])).
% 0.44/0.70 fof(c51,plain,(![X26]:(![X27]:((~xsd_string(X26)|~xsd_integer(X26))&(xsd_integer(X27)|xsd_string(X27))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X26]:(~xsd_string(X26)|~xsd_integer(X26)))&(![X27]:(xsd_integer(X27)|xsd_string(X27)))),inference(variable_rename,[status(thm)],[c49])).])).
% 0.44/0.70 cnf(c53,plain,xsd_integer(X74)|xsd_string(X74),inference(split_conjunct,[status(thm)],[c51])).
% 0.44/0.70 cnf(c52,plain,~xsd_string(X73)|~xsd_integer(X73),inference(split_conjunct,[status(thm)],[c51])).
% 0.44/0.70 cnf(symmetry,axiom,X71!=X70|X70=X71,theory(equality)).
% 0.44/0.70 cnf(reflexivity,axiom,X68=X68,theory(equality)).
% 0.44/0.70 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.44/0.70 fof(c54,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.44/0.70 fof(c55,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c54])).
% 0.44/0.70 fof(c57,plain,(![X28]:(![X29]:(cowlThing(X28)&~cowlNothing(X29)))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X28]:cowlThing(X28))&(![X29]:~cowlNothing(X29))),inference(variable_rename,[status(thm)],[c55])).])).
% 0.44/0.70 cnf(c59,plain,~cowlNothing(X67),inference(split_conjunct,[status(thm)],[c57])).
% 0.44/0.70 cnf(c58,plain,cowlThing(X66),inference(split_conjunct,[status(thm)],[c57])).
% 0.44/0.70 % SZS output end Saturation
% 0.44/0.70
% 0.44/0.70 % Initial clauses : 46
% 0.44/0.70 % Processed clauses : 100
% 0.44/0.70 % Factors computed : 4
% 0.44/0.70 % Resolvents computed: 114
% 0.44/0.70 % Tautologies deleted: 8
% 0.44/0.70 % Forward subsumed : 56
% 0.44/0.70 % Backward subsumed : 0
% 0.44/0.70 % -------- CPU Time ---------
% 0.44/0.70 % User time : 0.271 s
% 0.44/0.70 % System time : 0.013 s
% 0.44/0.70 % Total time : 0.284 s
%------------------------------------------------------------------------------