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