%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS038+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:28:32 EDT 2024
% Result : Satisfiable 0.50s 0.72s
% Output : Saturation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : KRS038+1 : TPTP v8.1.2. Released v3.1.0.
% 0.14/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n029.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 00:07:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.50/0.72 % Version: 1.5
% 0.50/0.72 % SZS status Satisfiable
% 0.50/0.72 % SZS output start Saturation
% 0.50/0.72 fof(axiom_7,axiom,cSatisfiable(i2003_11_14_17_15_54995),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.50/0.72 cnf(c10,plain,cSatisfiable(i2003_11_14_17_15_54995),inference(split_conjunct,[status(thm)],[axiom_7])).
% 0.50/0.72 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>(cp1(X)&(?[Y]:(rr(X,Y)&(?[Z]:((rr(Y,Z)&cp1(Z))&(![W]:(rinvR(Z,W)=>((![A]:(rr(W,A)=>cp1(A)))|(~cp1(W)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.50/0.72 fof(c29,plain,(![X]:(cSatisfiable(X)<=>(cp1(X)&(?[Y]:(rr(X,Y)&(?[Z]:((rr(Y,Z)&cp1(Z))&(![W]:(rinvR(Z,W)=>((![A]:(rr(W,A)=>cp1(A)))|~cp1(W))))))))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.50/0.72 fof(c30,plain,(![X]:((~cSatisfiable(X)|(cp1(X)&(?[Y]:(rr(X,Y)&(?[Z]:((rr(Y,Z)&cp1(Z))&(![W]:(~rinvR(Z,W)|((![A]:(~rr(W,A)|cp1(A)))|~cp1(W))))))))))&((~cp1(X)|(![Y]:(~rr(X,Y)|(![Z]:((~rr(Y,Z)|~cp1(Z))|(?[W]:(rinvR(Z,W)&((?[A]:(rr(W,A)&~cp1(A)))&cp1(W)))))))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[c29])).
% 0.50/0.72 fof(c31,plain,((![X]:(~cSatisfiable(X)|(cp1(X)&(?[Y]:(rr(X,Y)&(?[Z]:((rr(Y,Z)&cp1(Z))&(![W]:(~rinvR(Z,W)|((![A]:(~rr(W,A)|cp1(A)))|~cp1(W)))))))))))&(![X]:((~cp1(X)|(![Y]:(~rr(X,Y)|(![Z]:((~rr(Y,Z)|~cp1(Z))|(?[W]:(rinvR(Z,W)&((?[A]:(rr(W,A)&~cp1(A)))&cp1(W)))))))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c30])).
% 0.50/0.72 fof(c32,plain,((![X16]:(~cSatisfiable(X16)|(cp1(X16)&(?[X17]:(rr(X16,X17)&(?[X18]:((rr(X17,X18)&cp1(X18))&(![X19]:(~rinvR(X18,X19)|((![X20]:(~rr(X19,X20)|cp1(X20)))|~cp1(X19)))))))))))&(![X21]:((~cp1(X21)|(![X22]:(~rr(X21,X22)|(![X23]:((~rr(X22,X23)|~cp1(X23))|(?[X24]:(rinvR(X23,X24)&((?[X25]:(rr(X24,X25)&~cp1(X25)))&cp1(X24)))))))))|cSatisfiable(X21)))),inference(variable_rename,[status(thm)],[c31])).
% 0.50/0.72 fof(c34,plain,(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~cSatisfiable(X16)|(cp1(X16)&(rr(X16,skolem0001(X16))&((rr(skolem0001(X16),skolem0002(X16))&cp1(skolem0002(X16)))&(~rinvR(skolem0002(X16),X19)|((~rr(X19,X20)|cp1(X20))|~cp1(X19)))))))&((~cp1(X21)|(~rr(X21,X22)|((~rr(X22,X23)|~cp1(X23))|(rinvR(X23,skolem0003(X21,X22,X23))&((rr(skolem0003(X21,X22,X23),skolem0004(X21,X22,X23))&~cp1(skolem0004(X21,X22,X23)))&cp1(skolem0003(X21,X22,X23)))))))|cSatisfiable(X21))))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X16]:(~cSatisfiable(X16)|(cp1(X16)&(rr(X16,skolem0001(X16))&((rr(skolem0001(X16),skolem0002(X16))&cp1(skolem0002(X16)))&(![X19]:(~rinvR(skolem0002(X16),X19)|((![X20]:(~rr(X19,X20)|cp1(X20)))|~cp1(X19)))))))))&(![X21]:((~cp1(X21)|(![X22]:(~rr(X21,X22)|(![X23]:((~rr(X22,X23)|~cp1(X23))|(rinvR(X23,skolem0003(X21,X22,X23))&((rr(skolem0003(X21,X22,X23),skolem0004(X21,X22,X23))&~cp1(skolem0004(X21,X22,X23)))&cp1(skolem0003(X21,X22,X23)))))))))|cSatisfiable(X21)))),inference(skolemize,[status(esa)],[c32])).])).
% 0.50/0.72 fof(c35,plain,(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~cSatisfiable(X16)|cp1(X16))&((~cSatisfiable(X16)|rr(X16,skolem0001(X16)))&(((~cSatisfiable(X16)|rr(skolem0001(X16),skolem0002(X16)))&(~cSatisfiable(X16)|cp1(skolem0002(X16))))&(~cSatisfiable(X16)|(~rinvR(skolem0002(X16),X19)|((~rr(X19,X20)|cp1(X20))|~cp1(X19)))))))&(((~cp1(X21)|(~rr(X21,X22)|((~rr(X22,X23)|~cp1(X23))|rinvR(X23,skolem0003(X21,X22,X23)))))|cSatisfiable(X21))&((((~cp1(X21)|(~rr(X21,X22)|((~rr(X22,X23)|~cp1(X23))|rr(skolem0003(X21,X22,X23),skolem0004(X21,X22,X23)))))|cSatisfiable(X21))&((~cp1(X21)|(~rr(X21,X22)|((~rr(X22,X23)|~cp1(X23))|~cp1(skolem0004(X21,X22,X23)))))|cSatisfiable(X21)))&((~cp1(X21)|(~rr(X21,X22)|((~rr(X22,X23)|~cp1(X23))|cp1(skolem0003(X21,X22,X23)))))|cSatisfiable(X21))))))))))),inference(distribute,[status(thm)],[c34])).
% 0.50/0.72 cnf(c38,plain,~cSatisfiable(X132)|rr(skolem0001(X132),skolem0002(X132)),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 cnf(c114,plain,rr(skolem0001(i2003_11_14_17_15_54995),skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c38, c10])).
% 0.50/0.72 cnf(c42,plain,~cp1(X180)|~rr(X180,X179)|~rr(X179,X178)|~cp1(X178)|rr(skolem0003(X180,X179,X178),skolem0004(X180,X179,X178))|cSatisfiable(X180),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 cnf(c139,plain,~cp1(X237)|~rr(X237,skolem0001(i2003_11_14_17_15_54995))|~cp1(skolem0002(i2003_11_14_17_15_54995))|rr(skolem0003(X237,skolem0001(i2003_11_14_17_15_54995),skolem0002(i2003_11_14_17_15_54995)),skolem0004(X237,skolem0001(i2003_11_14_17_15_54995),skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X237),inference(resolution,[status(thm)],[c42, c114])).
% 0.50/0.72 cnf(c39,plain,~cSatisfiable(X87)|cp1(skolem0002(X87)),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 cnf(c105,plain,cp1(skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c39, c10])).
% 0.50/0.72 cnf(c37,plain,~cSatisfiable(X94)|rr(X94,skolem0001(X94)),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 cnf(c107,plain,rr(i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c37, c10])).
% 0.50/0.72 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.50/0.72 fof(c11,plain,(![X]:(![Y]:(![Z]:((~rr(X,Y)|~rr(Y,Z))|rr(X,Z))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.50/0.72 fof(c12,plain,(![X2]:(![X3]:(![X4]:((~rr(X2,X3)|~rr(X3,X4))|rr(X2,X4))))),inference(variable_rename,[status(thm)],[c11])).
% 0.50/0.72 cnf(c13,plain,~rr(X139,X138)|~rr(X138,X137)|rr(X139,X137),inference(split_conjunct,[status(thm)],[c12])).
% 0.50/0.72 cnf(c122,plain,~rr(X187,skolem0001(i2003_11_14_17_15_54995))|rr(X187,skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c13, c114])).
% 0.50/0.72 cnf(c143,plain,rr(i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c122, c107])).
% 0.50/0.72 cnf(c147,plain,~cp1(X235)|~rr(X235,i2003_11_14_17_15_54995)|~cp1(skolem0002(i2003_11_14_17_15_54995))|rr(skolem0003(X235,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)),skolem0004(X235,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X235),inference(resolution,[status(thm)],[c143, c42])).
% 0.50/0.72 cnf(c192,plain,~cp1(X236)|~rr(X236,i2003_11_14_17_15_54995)|rr(skolem0003(X236,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)),skolem0004(X236,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X236),inference(resolution,[status(thm)],[c147, c105])).
% 0.50/0.72 cnf(c36,plain,~cSatisfiable(X69)|cp1(X69),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 cnf(c100,plain,cp1(i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c36, c10])).
% 0.50/0.72 cnf(c40,plain,~cSatisfiable(X150)|~rinvR(skolem0002(X150),X149)|~rr(X149,X151)|cp1(X151)|~cp1(X149),inference(split_conjunct,[status(thm)],[c35])).
% 0.50/0.72 fof(axiom_5,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.50/0.72 fof(c14,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.50/0.72 fof(c15,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c14])).
% 0.50/0.72 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~rinvR(X5,X6)|rr(X6,X5))&(~rr(X8,X7)|rinvR(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X5]:(![X6]:(~rinvR(X5,X6)|rr(X6,X5))))&(![X7]:(![X8]:(~rr(X8,X7)|rinvR(X7,X8))))),inference(variable_rename,[status(thm)],[c15])).])).
% 0.50/0.72 cnf(c19,plain,~rr(X82,X81)|rinvR(X81,X82),inference(split_conjunct,[status(thm)],[c17])).
% 0.50/0.72 cnf(c144,plain,rinvR(skolem0002(i2003_11_14_17_15_54995),i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c143, c19])).
% 0.50/0.72 cnf(c152,plain,~cSatisfiable(i2003_11_14_17_15_54995)|~rr(i2003_11_14_17_15_54995,X215)|cp1(X215)|~cp1(i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c144, c40])).
% 0.50/0.72 cnf(c173,plain,~cSatisfiable(i2003_11_14_17_15_54995)|cp1(skolem0001(i2003_11_14_17_15_54995))|~cp1(i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c152, c107])).
% 0.50/0.72 cnf(c175,plain,~cSatisfiable(i2003_11_14_17_15_54995)|cp1(skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c173, c100])).
% 0.50/0.72 cnf(c177,plain,cp1(skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c175, c10])).
% 0.50/0.72 cnf(c138,plain,~cp1(X233)|~rr(X233,i2003_11_14_17_15_54995)|~cp1(skolem0001(i2003_11_14_17_15_54995))|rr(skolem0003(X233,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)),skolem0004(X233,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X233),inference(resolution,[status(thm)],[c42, c107])).
% 0.56/0.72 cnf(c190,plain,~cp1(X234)|~rr(X234,i2003_11_14_17_15_54995)|rr(skolem0003(X234,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)),skolem0004(X234,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X234),inference(resolution,[status(thm)],[c138, c177])).
% 0.56/0.72 cnf(c44,plain,~cp1(X190)|~rr(X190,X189)|~rr(X189,X188)|~cp1(X188)|cp1(skolem0003(X190,X189,X188))|cSatisfiable(X190),inference(split_conjunct,[status(thm)],[c35])).
% 0.56/0.72 cnf(c158,plain,~cp1(X232)|~rr(X232,skolem0001(i2003_11_14_17_15_54995))|~cp1(skolem0002(i2003_11_14_17_15_54995))|cp1(skolem0003(X232,skolem0001(i2003_11_14_17_15_54995),skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X232),inference(resolution,[status(thm)],[c44, c114])).
% 0.56/0.72 cnf(c41,plain,~cp1(X169)|~rr(X169,X168)|~rr(X168,X167)|~cp1(X167)|rinvR(X167,skolem0003(X169,X168,X167))|cSatisfiable(X169),inference(split_conjunct,[status(thm)],[c35])).
% 0.56/0.72 cnf(c135,plain,~cp1(X231)|~rr(X231,skolem0001(i2003_11_14_17_15_54995))|~cp1(skolem0002(i2003_11_14_17_15_54995))|rinvR(skolem0002(i2003_11_14_17_15_54995),skolem0003(X231,skolem0001(i2003_11_14_17_15_54995),skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X231),inference(resolution,[status(thm)],[c41, c114])).
% 0.56/0.72 cnf(c148,plain,~cp1(X229)|~rr(X229,i2003_11_14_17_15_54995)|~cp1(skolem0002(i2003_11_14_17_15_54995))|rinvR(skolem0002(i2003_11_14_17_15_54995),skolem0003(X229,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X229),inference(resolution,[status(thm)],[c143, c41])).
% 0.56/0.72 cnf(c186,plain,~cp1(X230)|~rr(X230,i2003_11_14_17_15_54995)|rinvR(skolem0002(i2003_11_14_17_15_54995),skolem0003(X230,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X230),inference(resolution,[status(thm)],[c148, c105])).
% 0.56/0.72 cnf(c159,plain,~cp1(X227)|~rr(X227,i2003_11_14_17_15_54995)|~cp1(skolem0002(i2003_11_14_17_15_54995))|cp1(skolem0003(X227,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X227),inference(resolution,[status(thm)],[c44, c143])).
% 0.56/0.72 cnf(c184,plain,~cp1(X228)|~rr(X228,i2003_11_14_17_15_54995)|cp1(skolem0003(X228,i2003_11_14_17_15_54995,skolem0002(i2003_11_14_17_15_54995)))|cSatisfiable(X228),inference(resolution,[status(thm)],[c159, c105])).
% 0.56/0.72 cnf(c134,plain,~cp1(X225)|~rr(X225,i2003_11_14_17_15_54995)|~cp1(skolem0001(i2003_11_14_17_15_54995))|rinvR(skolem0001(i2003_11_14_17_15_54995),skolem0003(X225,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X225),inference(resolution,[status(thm)],[c41, c107])).
% 0.56/0.72 cnf(c182,plain,~cp1(X226)|~rr(X226,i2003_11_14_17_15_54995)|rinvR(skolem0001(i2003_11_14_17_15_54995),skolem0003(X226,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X226),inference(resolution,[status(thm)],[c134, c177])).
% 0.56/0.72 cnf(c157,plain,~cp1(X223)|~rr(X223,i2003_11_14_17_15_54995)|~cp1(skolem0001(i2003_11_14_17_15_54995))|cp1(skolem0003(X223,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X223),inference(resolution,[status(thm)],[c44, c107])).
% 0.56/0.72 cnf(c180,plain,~cp1(X224)|~rr(X224,i2003_11_14_17_15_54995)|cp1(skolem0003(X224,i2003_11_14_17_15_54995,skolem0001(i2003_11_14_17_15_54995)))|cSatisfiable(X224),inference(resolution,[status(thm)],[c157, c177])).
% 0.56/0.72 cnf(c137,plain,~cp1(X222)|~rr(X222,X222)|rr(skolem0003(X222,X222,X222),skolem0004(X222,X222,X222))|cSatisfiable(X222),inference(factor,[status(thm)],[c42])).
% 0.56/0.72 cnf(c156,plain,~cp1(X221)|~rr(X221,X221)|cp1(skolem0003(X221,X221,X221))|cSatisfiable(X221),inference(factor,[status(thm)],[c44])).
% 0.56/0.72 cnf(c133,plain,~cp1(X220)|~rr(X220,X220)|rinvR(X220,skolem0003(X220,X220,X220))|cSatisfiable(X220),inference(factor,[status(thm)],[c41])).
% 0.56/0.72 cnf(c6,axiom,X129!=X126|X127!=X128|~rinvR(X129,X127)|rinvR(X126,X128),theory(equality)).
% 0.56/0.72 cnf(c153,plain,skolem0002(i2003_11_14_17_15_54995)!=X218|i2003_11_14_17_15_54995!=X217|rinvR(X218,X217),inference(resolution,[status(thm)],[c144, c6])).
% 0.56/0.72 cnf(c115,plain,rinvR(skolem0002(i2003_11_14_17_15_54995),skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c114, c19])).
% 0.56/0.72 cnf(c126,plain,~cSatisfiable(i2003_11_14_17_15_54995)|~rr(skolem0001(i2003_11_14_17_15_54995),X216)|cp1(X216)|~cp1(skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c40, c115])).
% 0.56/0.72 cnf(c7,axiom,X136!=X133|X134!=X135|~rr(X136,X134)|rr(X133,X135),theory(equality)).
% 0.56/0.72 cnf(c145,plain,i2003_11_14_17_15_54995!=X213|skolem0002(i2003_11_14_17_15_54995)!=X212|rr(X213,X212),inference(resolution,[status(thm)],[c143, c7])).
% 0.56/0.72 cnf(c119,plain,skolem0001(i2003_11_14_17_15_54995)!=X210|skolem0002(i2003_11_14_17_15_54995)!=X209|rr(X210,X209),inference(resolution,[status(thm)],[c7, c114])).
% 0.56/0.72 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.56/0.72 fof(c73,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(A,C))|rinvR(B,C))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_1])).
% 0.56/0.72 fof(c74,plain,(![X43]:(![X44]:(![X45]:((X43!=X44|~rinvR(X43,X45))|rinvR(X44,X45))))),inference(variable_rename,[status(thm)],[c73])).
% 0.56/0.72 cnf(c75,plain,X160!=X158|~rinvR(X160,X159)|rinvR(X158,X159),inference(split_conjunct,[status(thm)],[c74])).
% 0.56/0.72 cnf(c132,plain,skolem0002(i2003_11_14_17_15_54995)!=X207|rinvR(X207,skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c75, c115])).
% 0.56/0.72 cnf(c118,plain,i2003_11_14_17_15_54995!=X205|skolem0001(i2003_11_14_17_15_54995)!=X204|rr(X205,X204),inference(resolution,[status(thm)],[c7, c107])).
% 0.56/0.72 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.56/0.72 fof(c70,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR(C,A))|rinvR(C,B))))),inference(fof_nnf,[status(thm)],[rinvR_substitution_2])).
% 0.56/0.72 fof(c71,plain,(![X40]:(![X41]:(![X42]:((X40!=X41|~rinvR(X42,X40))|rinvR(X42,X41))))),inference(variable_rename,[status(thm)],[c70])).
% 0.56/0.72 cnf(c72,plain,X157!=X155|~rinvR(X156,X157)|rinvR(X156,X155),inference(split_conjunct,[status(thm)],[c71])).
% 0.56/0.72 cnf(c130,plain,skolem0001(i2003_11_14_17_15_54995)!=X203|rinvR(skolem0002(i2003_11_14_17_15_54995),X203),inference(resolution,[status(thm)],[c72, c115])).
% 0.56/0.72 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.56/0.72 fof(c67,plain,(![A]:(![B]:(![C]:((A!=B|~rr(A,C))|rr(B,C))))),inference(fof_nnf,[status(thm)],[rr_substitution_1])).
% 0.56/0.72 fof(c68,plain,(![X37]:(![X38]:(![X39]:((X37!=X38|~rr(X37,X39))|rr(X38,X39))))),inference(variable_rename,[status(thm)],[c67])).
% 0.56/0.72 cnf(c69,plain,X152!=X154|~rr(X152,X153)|rr(X154,X153),inference(split_conjunct,[status(thm)],[c68])).
% 0.56/0.72 cnf(c128,plain,skolem0001(i2003_11_14_17_15_54995)!=X202|rr(X202,skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c69, c114])).
% 0.56/0.72 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.56/0.72 fof(c64,plain,(![A]:(![B]:(![C]:((A!=B|~rr(C,A))|rr(C,B))))),inference(fof_nnf,[status(thm)],[rr_substitution_2])).
% 0.56/0.72 fof(c65,plain,(![X34]:(![X35]:(![X36]:((X34!=X35|~rr(X36,X34))|rr(X36,X35))))),inference(variable_rename,[status(thm)],[c64])).
% 0.56/0.72 cnf(c66,plain,X146!=X147|~rr(X148,X146)|rr(X148,X147),inference(split_conjunct,[status(thm)],[c65])).
% 0.56/0.72 cnf(c125,plain,skolem0002(i2003_11_14_17_15_54995)!=X201|rr(skolem0001(i2003_11_14_17_15_54995),X201),inference(resolution,[status(thm)],[c66, c114])).
% 0.56/0.72 cnf(c116,plain,skolem0002(i2003_11_14_17_15_54995)!=X200|skolem0001(i2003_11_14_17_15_54995)!=X199|rinvR(X200,X199),inference(resolution,[status(thm)],[c115, c6])).
% 0.56/0.72 cnf(c155,plain,skolem0002(i2003_11_14_17_15_54995)!=X197|rinvR(X197,i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c144, c75])).
% 0.56/0.72 cnf(c154,plain,i2003_11_14_17_15_54995!=X196|rinvR(skolem0002(i2003_11_14_17_15_54995),X196),inference(resolution,[status(thm)],[c144, c72])).
% 0.56/0.72 cnf(c108,plain,rinvR(skolem0001(i2003_11_14_17_15_54995),i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c107, c19])).
% 0.56/0.72 cnf(c113,plain,skolem0001(i2003_11_14_17_15_54995)!=X195|i2003_11_14_17_15_54995!=X194|rinvR(X195,X194),inference(resolution,[status(thm)],[c6, c108])).
% 0.56/0.72 cnf(c150,plain,i2003_11_14_17_15_54995!=X193|rr(X193,skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c143, c69])).
% 0.56/0.72 cnf(c149,plain,~rr(X192,i2003_11_14_17_15_54995)|rr(X192,skolem0002(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c143, c13])).
% 0.56/0.72 cnf(c146,plain,skolem0002(i2003_11_14_17_15_54995)!=X191|rr(i2003_11_14_17_15_54995,X191),inference(resolution,[status(thm)],[c143, c66])).
% 0.56/0.72 cnf(c43,plain,~cp1(X186)|~rr(X186,X185)|~rr(X185,X184)|~cp1(X184)|~cp1(skolem0004(X186,X185,X184))|cSatisfiable(X186),inference(split_conjunct,[status(thm)],[c35])).
% 0.56/0.72 cnf(c131,plain,skolem0001(i2003_11_14_17_15_54995)!=X183|rinvR(X183,i2003_11_14_17_15_54995),inference(resolution,[status(thm)],[c75, c108])).
% 0.56/0.72 cnf(c129,plain,i2003_11_14_17_15_54995!=X182|rinvR(skolem0001(i2003_11_14_17_15_54995),X182),inference(resolution,[status(thm)],[c72, c108])).
% 0.56/0.72 cnf(c127,plain,i2003_11_14_17_15_54995!=X181|rr(X181,skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c69, c107])).
% 0.56/0.72 cnf(c124,plain,skolem0001(i2003_11_14_17_15_54995)!=X177|rr(i2003_11_14_17_15_54995,X177),inference(resolution,[status(thm)],[c66, c107])).
% 0.56/0.72 cnf(c121,plain,~rr(X176,i2003_11_14_17_15_54995)|rr(X176,skolem0001(i2003_11_14_17_15_54995)),inference(resolution,[status(thm)],[c13, c107])).
% 0.56/0.72 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.56/0.72 fof(c85,plain,(![A]:(![B]:(![C]:((A!=B|~rf(A,C))|rf(B,C))))),inference(fof_nnf,[status(thm)],[rf_substitution_1])).
% 0.56/0.72 fof(c86,plain,(![X55]:(![X56]:(![X57]:((X55!=X56|~rf(X55,X57))|rf(X56,X57))))),inference(variable_rename,[status(thm)],[c85])).
% 0.56/0.72 cnf(c87,plain,X175!=X174|~rf(X175,X173)|rf(X174,X173),inference(split_conjunct,[status(thm)],[c86])).
% 0.56/0.72 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.56/0.72 fof(c82,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.56/0.72 fof(c83,plain,(![X52]:(![X53]:(![X54]:((X52!=X53|~rf(X54,X52))|rf(X54,X53))))),inference(variable_rename,[status(thm)],[c82])).
% 0.56/0.72 cnf(c84,plain,X172!=X170|~rf(X171,X172)|rf(X171,X170),inference(split_conjunct,[status(thm)],[c83])).
% 0.56/0.72 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.56/0.72 fof(c79,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(A,C))|rinvF(B,C))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_1])).
% 0.56/0.72 fof(c80,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rinvF(X49,X51))|rinvF(X50,X51))))),inference(variable_rename,[status(thm)],[c79])).
% 0.56/0.72 cnf(c81,plain,X164!=X166|~rinvF(X164,X165)|rinvF(X166,X165),inference(split_conjunct,[status(thm)],[c80])).
% 0.56/0.72 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.56/0.72 fof(c76,plain,(![A]:(![B]:(![C]:((A!=B|~rinvF(C,A))|rinvF(C,B))))),inference(fof_nnf,[status(thm)],[rinvF_substitution_2])).
% 0.56/0.72 fof(c77,plain,(![X46]:(![X47]:(![X48]:((X46!=X47|~rinvF(X48,X46))|rinvF(X48,X47))))),inference(variable_rename,[status(thm)],[c76])).
% 0.56/0.72 cnf(c78,plain,X162!=X163|~rinvF(X161,X162)|rinvF(X161,X163),inference(split_conjunct,[status(thm)],[c77])).
% 0.56/0.72 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.56/0.72 fof(c26,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.56/0.72 fof(c27,plain,(![X13]:(![X14]:(![X15]:((~rf(X13,X14)|~rf(X13,X15))|X14=X15)))),inference(variable_rename,[status(thm)],[c26])).
% 0.56/0.72 cnf(c28,plain,~rf(X141,X143)|~rf(X141,X142)|X143=X142,inference(split_conjunct,[status(thm)],[c27])).
% 0.56/0.72 cnf(c5,axiom,X115!=X112|X113!=X114|~rinvF(X115,X113)|rinvF(X112,X114),theory(equality)).
% 0.56/0.72 cnf(c9,axiom,X110!=X109|~xsd_string(X110)|xsd_string(X109),theory(equality)).
% 0.56/0.72 cnf(c8,axiom,X107!=X106|~xsd_integer(X107)|xsd_integer(X106),theory(equality)).
% 0.56/0.72 cnf(c4,axiom,X104!=X101|X102!=X103|~rf(X104,X102)|rf(X101,X103),theory(equality)).
% 0.56/0.72 cnf(c3,axiom,X100!=X99|~cp1(X100)|cp1(X99),theory(equality)).
% 0.56/0.72 cnf(c0,axiom,X89!=X88|~cSatisfiable(X89)|cSatisfiable(X88),theory(equality)).
% 0.56/0.72 fof(axiom_4,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.56/0.72 fof(c20,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.56/0.72 fof(c21,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c20])).
% 0.56/0.72 fof(c23,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvF(X9,X10)|rf(X10,X9))&(~rf(X12,X11)|rinvF(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,((![X9]:(![X10]:(~rinvF(X9,X10)|rf(X10,X9))))&(![X11]:(![X12]:(~rf(X12,X11)|rinvF(X11,X12))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.56/0.72 cnf(c25,plain,~rf(X86,X85)|rinvF(X85,X86),inference(split_conjunct,[status(thm)],[c23])).
% 0.56/0.72 cnf(c24,plain,~rinvF(X84,X83)|rf(X83,X84),inference(split_conjunct,[status(thm)],[c23])).
% 0.56/0.72 cnf(c18,plain,~rinvR(X80,X79)|rr(X79,X80),inference(split_conjunct,[status(thm)],[c17])).
% 0.56/0.72 cnf(transitivity,axiom,X78!=X77|X77!=X76|X78=X76,theory(equality)).
% 0.56/0.72 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.56/0.72 fof(c45,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.56/0.72 fof(c46,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c45])).
% 0.56/0.72 fof(c47,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c46])).
% 0.56/0.72 fof(c49,plain,(![X26]:(![X27]:((~xsd_string(X26)|~xsd_integer(X26))&(xsd_integer(X27)|xsd_string(X27))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X26]:(~xsd_string(X26)|~xsd_integer(X26)))&(![X27]:(xsd_integer(X27)|xsd_string(X27)))),inference(variable_rename,[status(thm)],[c47])).])).
% 0.56/0.72 cnf(c51,plain,xsd_integer(X74)|xsd_string(X74),inference(split_conjunct,[status(thm)],[c49])).
% 0.56/0.72 cnf(c50,plain,~xsd_string(X73)|~xsd_integer(X73),inference(split_conjunct,[status(thm)],[c49])).
% 0.56/0.72 cnf(symmetry,axiom,X71!=X70|X70=X71,theory(equality)).
% 0.56/0.72 cnf(reflexivity,axiom,X68=X68,theory(equality)).
% 0.56/0.72 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.56/0.72 fof(c52,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.56/0.72 fof(c53,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c52])).
% 0.56/0.72 fof(c55,plain,(![X28]:(![X29]:(cowlThing(X28)&~cowlNothing(X29)))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X28]:cowlThing(X28))&(![X29]:~cowlNothing(X29))),inference(variable_rename,[status(thm)],[c53])).])).
% 0.56/0.72 cnf(c57,plain,~cowlNothing(X67),inference(split_conjunct,[status(thm)],[c55])).
% 0.56/0.72 cnf(c56,plain,cowlThing(X66),inference(split_conjunct,[status(thm)],[c55])).
% 0.56/0.72 % SZS output end Saturation
% 0.56/0.72
% 0.56/0.72 % Initial clauses : 47
% 0.56/0.72 % Processed clauses : 91
% 0.56/0.72 % Factors computed : 12
% 0.56/0.72 % Resolvents computed: 82
% 0.56/0.72 % Tautologies deleted: 8
% 0.56/0.72 % Forward subsumed : 42
% 0.56/0.72 % Backward subsumed : 8
% 0.56/0.72 % -------- CPU Time ---------
% 0.56/0.72 % User time : 0.328 s
% 0.56/0.72 % System time : 0.025 s
% 0.56/0.72 % Total time : 0.353 s
%------------------------------------------------------------------------------