%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS036+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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.52s 0.68s
% Output : Saturation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS036+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n008.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:07:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.52/0.68 % Version: 1.5
% 0.52/0.68 % SZS status Satisfiable
% 0.52/0.68 % SZS output start Saturation
% 0.52/0.68 fof(axiom_5,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.52/0.68 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.52/0.68 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.52/0.68 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.52/0.68 cnf(c22,plain,~rr(X84,X83)|rinvR(X83,X84),inference(split_conjunct,[status(thm)],[c20])).
% 0.52/0.68 fof(axiom_8,axiom,(![X]:(![Y]:(rf(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.52/0.68 fof(c10,plain,(![X]:(![Y]:(~rf(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.52/0.68 fof(c11,plain,(![X2]:(![X3]:(~rf(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c10])).
% 0.52/0.68 cnf(c12,plain,~rf(X76,X77)|rr(X76,X77),inference(split_conjunct,[status(thm)],[c11])).
% 0.52/0.68 fof(axiom_4,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.52/0.68 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.52/0.68 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.52/0.68 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.52/0.68 cnf(c27,plain,~rinvF(X86,X85)|rf(X85,X86),inference(split_conjunct,[status(thm)],[c26])).
% 0.52/0.68 fof(axiom_7,axiom,cSatisfiable(i2003_11_14_17_15_47436),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.52/0.68 cnf(c13,plain,cSatisfiable(i2003_11_14_17_15_47436),inference(split_conjunct,[status(thm)],[axiom_7])).
% 0.52/0.68 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/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.52/0.68 fof(c32,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.52/0.68 fof(c33,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)],[c32])).
% 0.52/0.68 fof(c34,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)],[c33])).
% 0.52/0.68 fof(c35,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)],[c34])).
% 0.52/0.68 fof(c37,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(c36,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)],[c35])).])).
% 0.52/0.68 fof(c38,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)],[c37])).
% 0.52/0.68 cnf(c41,plain,~cSatisfiable(X136)|rinvF(skolem0001(X136),skolem0002(X136)),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.68 cnf(c126,plain,rinvF(skolem0001(i2003_11_14_17_15_47436),skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c41, c13])).
% 0.52/0.68 cnf(c128,plain,rf(skolem0002(i2003_11_14_17_15_47436),skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c126, c27])).
% 0.52/0.68 cnf(c129,plain,rr(skolem0002(i2003_11_14_17_15_47436),skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c128, c12])).
% 0.52/0.68 cnf(c132,plain,rinvR(skolem0001(i2003_11_14_17_15_47436),skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c129, c22])).
% 0.52/0.68 cnf(c45,plain,ca(X151)|~rinvR(X151,X148)|~rinvF(X148,X150)|~ca(X150)|~rinvF(X151,X149)|~ca(X149)|cSatisfiable(X151),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.68 cnf(c147,plain,ca(skolem0001(i2003_11_14_17_15_47436))|~rinvR(skolem0001(i2003_11_14_17_15_47436),X238)|~rinvF(X238,X237)|~ca(X237)|~ca(skolem0002(i2003_11_14_17_15_47436))|cSatisfiable(skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c45, c126])).
% 0.52/0.68 cnf(c215,plain,ca(skolem0001(i2003_11_14_17_15_47436))|~rinvF(skolem0002(i2003_11_14_17_15_47436),X250)|~ca(X250)|~ca(skolem0002(i2003_11_14_17_15_47436))|cSatisfiable(skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c147, c132])).
% 0.52/0.68 cnf(c145,plain,ca(X229)|~rinvR(X229,X229)|~rinvF(X229,X228)|~ca(X228)|cSatisfiable(X229),inference(factor,[status(thm)],[c45])).
% 0.52/0.68 cnf(c209,plain,ca(skolem0001(i2003_11_14_17_15_47436))|~rinvR(skolem0001(i2003_11_14_17_15_47436),skolem0001(i2003_11_14_17_15_47436))|~ca(skolem0002(i2003_11_14_17_15_47436))|cSatisfiable(skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c145, c126])).
% 0.52/0.68 cnf(c6,axiom,X135!=X132|X133!=X134|~rinvR(X135,X133)|rinvR(X132,X134),theory(equality)).
% 0.52/0.68 cnf(c21,plain,~rinvR(X81,X82)|rr(X82,X81),inference(split_conjunct,[status(thm)],[c20])).
% 0.52/0.68 cnf(c40,plain,~cSatisfiable(X100)|rinvR(X100,skolem0001(X100)),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.68 cnf(c111,plain,rinvR(i2003_11_14_17_15_47436,skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c40, c13])).
% 0.52/0.68 cnf(c112,plain,rr(skolem0001(i2003_11_14_17_15_47436),i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c111, c21])).
% 0.52/0.68 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rr(X,Y)&rr(Y,Z))=>rr(X,Z))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.52/0.68 fof(c14,plain,(![X]:(![Y]:(![Z]:((~rr(X,Y)|~rr(Y,Z))|rr(X,Z))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.52/0.68 fof(c15,plain,(![X4]:(![X5]:(![X6]:((~rr(X4,X5)|~rr(X5,X6))|rr(X4,X6))))),inference(variable_rename,[status(thm)],[c14])).
% 0.52/0.68 cnf(c16,plain,~rr(X141,X143)|~rr(X143,X142)|rr(X141,X142),inference(split_conjunct,[status(thm)],[c15])).
% 0.52/0.68 cnf(c141,plain,~rr(X179,skolem0001(i2003_11_14_17_15_47436))|rr(X179,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c16, c112])).
% 0.52/0.68 cnf(c168,plain,rr(skolem0002(i2003_11_14_17_15_47436),i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c141, c129])).
% 0.52/0.68 cnf(c172,plain,rinvR(i2003_11_14_17_15_47436,skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c168, c22])).
% 0.52/0.68 cnf(c177,plain,i2003_11_14_17_15_47436!=X248|skolem0002(i2003_11_14_17_15_47436)!=X247|rinvR(X248,X247),inference(resolution,[status(thm)],[c172, c6])).
% 0.52/0.68 cnf(c7,axiom,X140!=X137|X138!=X139|~rr(X140,X138)|rr(X137,X139),theory(equality)).
% 0.52/0.69 cnf(c170,plain,skolem0002(i2003_11_14_17_15_47436)!=X242|i2003_11_14_17_15_47436!=X243|rr(X242,X243),inference(resolution,[status(thm)],[c168, c7])).
% 0.52/0.69 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.52/0.69 fof(c86,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.52/0.69 fof(c87,plain,(![X55]:(![X56]:(![X57]:((X55!=X56|~rf(X55,X57))|rf(X56,X57))))),inference(variable_rename,[status(thm)],[c86])).
% 0.52/0.69 cnf(c88,plain,X177!=X175|~rf(X177,X176)|rf(X175,X176),inference(split_conjunct,[status(thm)],[c87])).
% 0.52/0.69 cnf(c166,plain,skolem0002(i2003_11_14_17_15_47436)!=X239|rf(X239,skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c88, c128])).
% 0.52/0.69 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.52/0.69 fof(c83,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.52/0.69 fof(c84,plain,(![X52]:(![X53]:(![X54]:((X52!=X53|~rf(X54,X52))|rf(X54,X53))))),inference(variable_rename,[status(thm)],[c83])).
% 0.52/0.69 cnf(c85,plain,X173!=X174|~rf(X172,X173)|rf(X172,X174),inference(split_conjunct,[status(thm)],[c84])).
% 0.52/0.69 cnf(c164,plain,skolem0001(i2003_11_14_17_15_47436)!=X236|rf(skolem0002(i2003_11_14_17_15_47436),X236),inference(resolution,[status(thm)],[c85, c128])).
% 0.52/0.69 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.52/0.69 fof(c80,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.52/0.69 fof(c81,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rinvF(X49,X51))|rinvF(X50,X51))))),inference(variable_rename,[status(thm)],[c80])).
% 0.52/0.69 cnf(c82,plain,X169!=X170|~rinvF(X169,X171)|rinvF(X170,X171),inference(split_conjunct,[status(thm)],[c81])).
% 0.52/0.69 cnf(c163,plain,skolem0001(i2003_11_14_17_15_47436)!=X235|rinvF(X235,skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c82, c126])).
% 0.52/0.69 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.52/0.69 fof(c77,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.52/0.69 fof(c78,plain,(![X46]:(![X47]:(![X48]:((X46!=X47|~rinvF(X48,X46))|rinvF(X48,X47))))),inference(variable_rename,[status(thm)],[c77])).
% 0.52/0.69 cnf(c79,plain,X168!=X167|~rinvF(X166,X168)|rinvF(X166,X167),inference(split_conjunct,[status(thm)],[c78])).
% 0.52/0.69 cnf(c161,plain,skolem0002(i2003_11_14_17_15_47436)!=X234|rinvF(skolem0001(i2003_11_14_17_15_47436),X234),inference(resolution,[status(thm)],[c79, c126])).
% 0.52/0.69 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.52/0.69 fof(c74,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(A,C))|rinvR(B,C))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_1])).
% 0.52/0.69 fof(c75,plain,(![X43]:(![X44]:(![X45]:((X43!=X44|~rinvR(X43,X45))|rinvR(X44,X45))))),inference(variable_rename,[status(thm)],[c74])).
% 0.52/0.69 cnf(c76,plain,X164!=X163|~rinvR(X164,X165)|rinvR(X163,X165),inference(split_conjunct,[status(thm)],[c75])).
% 0.52/0.69 cnf(c159,plain,skolem0001(i2003_11_14_17_15_47436)!=X231|rinvR(X231,skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c76, c132])).
% 0.52/0.69 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.52/0.69 fof(c71,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(C,A))|rinvR(C,B))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_2])).
% 0.52/0.69 fof(c72,plain,(![X40]:(![X41]:(![X42]:((X40!=X41|~rinvR(X42,X40))|rinvR(X42,X41))))),inference(variable_rename,[status(thm)],[c71])).
% 0.52/0.69 cnf(c73,plain,X162!=X160|~rinvR(X161,X162)|rinvR(X161,X160),inference(split_conjunct,[status(thm)],[c72])).
% 0.52/0.69 cnf(c156,plain,skolem0002(i2003_11_14_17_15_47436)!=X230|rinvR(skolem0001(i2003_11_14_17_15_47436),X230),inference(resolution,[status(thm)],[c73, c132])).
% 0.52/0.69 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.52/0.69 fof(c68,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.52/0.69 fof(c69,plain,(![X37]:(![X38]:(![X39]:((X37!=X38|~rr(X37,X39))|rr(X38,X39))))),inference(variable_rename,[status(thm)],[c68])).
% 0.52/0.69 cnf(c70,plain,X159!=X158|~rr(X159,X157)|rr(X158,X157),inference(split_conjunct,[status(thm)],[c69])).
% 0.52/0.69 cnf(c152,plain,skolem0002(i2003_11_14_17_15_47436)!=X227|rr(X227,skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c70, c129])).
% 0.52/0.69 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.52/0.69 fof(c65,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.52/0.69 fof(c66,plain,(![X34]:(![X35]:(![X36]:((X34!=X35|~rr(X36,X34))|rr(X36,X35))))),inference(variable_rename,[status(thm)],[c65])).
% 0.52/0.69 cnf(c67,plain,X156!=X155|~rr(X154,X156)|rr(X154,X155),inference(split_conjunct,[status(thm)],[c66])).
% 0.52/0.69 cnf(c149,plain,skolem0001(i2003_11_14_17_15_47436)!=X226|rr(skolem0002(i2003_11_14_17_15_47436),X226),inference(resolution,[status(thm)],[c67, c129])).
% 0.52/0.69 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.52/0.69 fof(c29,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.52/0.69 fof(c30,plain,(![X15]:(![X16]:(![X17]:((~rf(X15,X16)|~rf(X15,X17))|X16=X17)))),inference(variable_rename,[status(thm)],[c29])).
% 0.52/0.69 cnf(c31,plain,~rf(X145,X147)|~rf(X145,X146)|X147=X146,inference(split_conjunct,[status(thm)],[c30])).
% 0.52/0.69 cnf(c143,plain,~rf(skolem0002(i2003_11_14_17_15_47436),X225)|X225=skolem0001(i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c31, c128])).
% 0.52/0.69 cnf(c137,plain,skolem0001(i2003_11_14_17_15_47436)!=X224|skolem0002(i2003_11_14_17_15_47436)!=X223|rinvR(X224,X223),inference(resolution,[status(thm)],[c132, c6])).
% 0.52/0.69 cnf(c140,plain,~rr(X222,skolem0002(i2003_11_14_17_15_47436))|rr(X222,skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c16, c129])).
% 0.52/0.69 cnf(c135,plain,skolem0001(i2003_11_14_17_15_47436)!=X216|i2003_11_14_17_15_47436!=X217|rr(X216,X217),inference(resolution,[status(thm)],[c7, c112])).
% 0.52/0.69 cnf(c178,plain,i2003_11_14_17_15_47436!=X214|rinvR(X214,skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c172, c76])).
% 0.52/0.69 cnf(c176,plain,skolem0002(i2003_11_14_17_15_47436)!=X213|rinvR(i2003_11_14_17_15_47436,X213),inference(resolution,[status(thm)],[c172, c73])).
% 0.52/0.69 cnf(c134,plain,skolem0002(i2003_11_14_17_15_47436)!=X211|skolem0001(i2003_11_14_17_15_47436)!=X212|rr(X211,X212),inference(resolution,[status(thm)],[c7, c129])).
% 0.52/0.69 cnf(c174,plain,~rr(X210,skolem0002(i2003_11_14_17_15_47436))|rr(X210,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c168, c16])).
% 0.52/0.69 cnf(c173,plain,skolem0002(i2003_11_14_17_15_47436)!=X209|rr(X209,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c168, c70])).
% 0.52/0.69 cnf(c171,plain,i2003_11_14_17_15_47436!=X208|rr(skolem0002(i2003_11_14_17_15_47436),X208),inference(resolution,[status(thm)],[c168, c67])).
% 0.52/0.69 cnf(c43,plain,~cSatisfiable(X103)|rinvF(X103,skolem0003(X103)),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.69 cnf(c114,plain,rinvF(i2003_11_14_17_15_47436,skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c43, c13])).
% 0.52/0.69 cnf(c115,plain,rf(skolem0003(i2003_11_14_17_15_47436),i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c114, c27])).
% 0.52/0.69 cnf(c116,plain,rr(skolem0003(i2003_11_14_17_15_47436),i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c115, c12])).
% 0.52/0.69 cnf(c133,plain,skolem0003(i2003_11_14_17_15_47436)!=X206|i2003_11_14_17_15_47436!=X207|rr(X206,X207),inference(resolution,[status(thm)],[c7, c116])).
% 0.52/0.69 cnf(c167,plain,skolem0003(i2003_11_14_17_15_47436)!=X204|rf(X204,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c88, c115])).
% 0.52/0.69 cnf(c165,plain,i2003_11_14_17_15_47436!=X203|rf(skolem0003(i2003_11_14_17_15_47436),X203),inference(resolution,[status(thm)],[c85, c115])).
% 0.52/0.69 cnf(c4,axiom,X109!=X106|X107!=X108|~rf(X109,X107)|rf(X106,X108),theory(equality)).
% 0.52/0.69 cnf(c131,plain,skolem0002(i2003_11_14_17_15_47436)!=X202|skolem0001(i2003_11_14_17_15_47436)!=X201|rf(X202,X201),inference(resolution,[status(thm)],[c128, c4])).
% 0.52/0.69 cnf(c162,plain,i2003_11_14_17_15_47436!=X200|rinvF(X200,skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c82, c114])).
% 0.52/0.69 cnf(c160,plain,skolem0003(i2003_11_14_17_15_47436)!=X199|rinvF(i2003_11_14_17_15_47436,X199),inference(resolution,[status(thm)],[c79, c114])).
% 0.52/0.69 cnf(c5,axiom,X121!=X118|X119!=X120|~rinvF(X121,X119)|rinvF(X118,X120),theory(equality)).
% 0.52/0.69 cnf(c127,plain,skolem0001(i2003_11_14_17_15_47436)!=X197|skolem0002(i2003_11_14_17_15_47436)!=X198|rinvF(X197,X198),inference(resolution,[status(thm)],[c126, c5])).
% 0.52/0.69 cnf(c158,plain,i2003_11_14_17_15_47436!=X196|rinvR(X196,skolem0001(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c76, c111])).
% 0.52/0.69 cnf(c118,plain,rinvR(i2003_11_14_17_15_47436,skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c116, c22])).
% 0.52/0.69 cnf(c157,plain,i2003_11_14_17_15_47436!=X195|rinvR(X195,skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c76, c118])).
% 0.52/0.69 cnf(c155,plain,skolem0001(i2003_11_14_17_15_47436)!=X194|rinvR(i2003_11_14_17_15_47436,X194),inference(resolution,[status(thm)],[c73, c111])).
% 0.52/0.69 cnf(c125,plain,i2003_11_14_17_15_47436!=X193|skolem0001(i2003_11_14_17_15_47436)!=X192|rinvR(X193,X192),inference(resolution,[status(thm)],[c6, c111])).
% 0.52/0.69 cnf(c154,plain,skolem0003(i2003_11_14_17_15_47436)!=X191|rinvR(i2003_11_14_17_15_47436,X191),inference(resolution,[status(thm)],[c73, c118])).
% 0.52/0.69 cnf(c153,plain,skolem0001(i2003_11_14_17_15_47436)!=X190|rr(X190,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c70, c112])).
% 0.52/0.69 cnf(c124,plain,i2003_11_14_17_15_47436!=X189|skolem0003(i2003_11_14_17_15_47436)!=X188|rinvR(X189,X188),inference(resolution,[status(thm)],[c6, c118])).
% 0.52/0.69 cnf(c151,plain,skolem0003(i2003_11_14_17_15_47436)!=X187|rr(X187,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c70, c116])).
% 0.52/0.69 cnf(c150,plain,i2003_11_14_17_15_47436!=X186|rr(skolem0001(i2003_11_14_17_15_47436),X186),inference(resolution,[status(thm)],[c67, c112])).
% 0.52/0.69 cnf(c148,plain,i2003_11_14_17_15_47436!=X185|rr(skolem0003(i2003_11_14_17_15_47436),X185),inference(resolution,[status(thm)],[c67, c116])).
% 0.52/0.69 cnf(c123,plain,i2003_11_14_17_15_47436!=X183|skolem0003(i2003_11_14_17_15_47436)!=X184|rinvF(X183,X184),inference(resolution,[status(thm)],[c5, c114])).
% 0.52/0.69 cnf(c144,plain,~rf(skolem0003(i2003_11_14_17_15_47436),X182)|X182=i2003_11_14_17_15_47436,inference(resolution,[status(thm)],[c31, c115])).
% 0.52/0.69 cnf(c120,plain,skolem0003(i2003_11_14_17_15_47436)!=X181|i2003_11_14_17_15_47436!=X180|rf(X181,X180),inference(resolution,[status(thm)],[c4, c115])).
% 0.52/0.69 cnf(c139,plain,~rr(X178,skolem0003(i2003_11_14_17_15_47436))|rr(X178,i2003_11_14_17_15_47436),inference(resolution,[status(thm)],[c16, c116])).
% 0.52/0.69 cnf(c9,axiom,X114!=X113|~xsd_string(X114)|xsd_string(X113),theory(equality)).
% 0.52/0.69 cnf(c8,axiom,X111!=X110|~xsd_integer(X111)|xsd_integer(X110),theory(equality)).
% 0.52/0.69 cnf(c39,plain,~cSatisfiable(X69)|~ca(X69),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.69 cnf(c44,plain,~cSatisfiable(X93)|ca(skolem0003(X93)),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.69 cnf(c108,plain,ca(skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c44, c13])).
% 0.52/0.69 cnf(c109,plain,~cSatisfiable(skolem0003(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c108, c39])).
% 0.52/0.69 cnf(c1,axiom,X95!=X94|~ca(X95)|ca(X94),theory(equality)).
% 0.52/0.69 cnf(c42,plain,~cSatisfiable(X89)|ca(skolem0002(X89)),inference(split_conjunct,[status(thm)],[c38])).
% 0.52/0.69 cnf(c105,plain,ca(skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c42, c13])).
% 0.52/0.69 cnf(c107,plain,~cSatisfiable(skolem0002(i2003_11_14_17_15_47436)),inference(resolution,[status(thm)],[c105, c39])).
% 0.52/0.69 cnf(c0,axiom,X91!=X90|~cSatisfiable(X91)|cSatisfiable(X90),theory(equality)).
% 0.52/0.69 cnf(c28,plain,~rf(X88,X87)|rinvF(X87,X88),inference(split_conjunct,[status(thm)],[c26])).
% 0.52/0.69 cnf(transitivity,axiom,X80!=X78|X78!=X79|X80=X79,theory(equality)).
% 0.52/0.69 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.52/0.69 fof(c46,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.52/0.69 fof(c47,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c46])).
% 0.52/0.69 fof(c48,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c47])).
% 0.52/0.69 fof(c50,plain,(![X26]:(![X27]:((~xsd_string(X26)|~xsd_integer(X26))&(xsd_integer(X27)|xsd_string(X27))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X26]:(~xsd_string(X26)|~xsd_integer(X26)))&(![X27]:(xsd_integer(X27)|xsd_string(X27)))),inference(variable_rename,[status(thm)],[c48])).])).
% 0.52/0.69 cnf(c52,plain,xsd_integer(X74)|xsd_string(X74),inference(split_conjunct,[status(thm)],[c50])).
% 0.52/0.69 cnf(c51,plain,~xsd_string(X73)|~xsd_integer(X73),inference(split_conjunct,[status(thm)],[c50])).
% 0.52/0.69 cnf(symmetry,axiom,X71!=X70|X70=X71,theory(equality)).
% 0.52/0.69 cnf(reflexivity,axiom,X68=X68,theory(equality)).
% 0.52/0.69 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.52/0.69 fof(c53,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.52/0.69 fof(c54,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c53])).
% 0.52/0.69 fof(c56,plain,(![X28]:(![X29]:(cowlThing(X28)&~cowlNothing(X29)))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X28]:cowlThing(X28))&(![X29]:~cowlNothing(X29))),inference(variable_rename,[status(thm)],[c54])).])).
% 0.52/0.69 cnf(c58,plain,~cowlNothing(X67),inference(split_conjunct,[status(thm)],[c56])).
% 0.52/0.69 cnf(c57,plain,cowlThing(X66),inference(split_conjunct,[status(thm)],[c56])).
% 0.52/0.69 % SZS output end Saturation
% 0.52/0.69
% 0.52/0.69 % Initial clauses : 46
% 0.52/0.69 % Processed clauses : 100
% 0.52/0.69 % Factors computed : 4
% 0.52/0.69 % Resolvents computed: 114
% 0.52/0.69 % Tautologies deleted: 8
% 0.52/0.69 % Forward subsumed : 56
% 0.52/0.69 % Backward subsumed : 0
% 0.52/0.69 % -------- CPU Time ---------
% 0.52/0.69 % User time : 0.320 s
% 0.52/0.69 % System time : 0.015 s
% 0.52/0.69 % Total time : 0.335 s
%------------------------------------------------------------------------------