%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS072+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:37 EDT 2024
% Result : Unsatisfiable 0.42s 0.60s
% Output : Refutation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS072+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:17:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.42/0.60 % Version: 1.5
% 0.42/0.60 % SZS status Unsatisfiable
% 0.42/0.60 % SZS output start CNFRefutation
% 0.42/0.60 fof(axiom_3,axiom,(![X]:(cp1(X)=>(~(((cp3(X)|cp2(X))|cp4(X))|cp5(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.42/0.60 fof(c34,plain,(![X]:(~cp1(X)|(((~cp3(X)&~cp2(X))&~cp4(X))&~cp5(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.42/0.60 fof(c35,plain,(![X9]:(~cp1(X9)|(((~cp3(X9)&~cp2(X9))&~cp4(X9))&~cp5(X9)))),inference(variable_rename,[status(thm)],[c34])).
% 0.42/0.60 fof(c36,plain,(![X9]:((((~cp1(X9)|~cp3(X9))&(~cp1(X9)|~cp2(X9)))&(~cp1(X9)|~cp4(X9)))&(~cp1(X9)|~cp5(X9)))),inference(distribute,[status(thm)],[c35])).
% 0.42/0.60 cnf(c38,plain,~cp1(X72)|~cp2(X72),inference(split_conjunct,[status(thm)],[c36])).
% 0.42/0.60 fof(axiom_8,axiom,cUnsatisfiable(i2003_11_14_17_18_50190),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.42/0.60 cnf(c12,plain,cUnsatisfiable(i2003_11_14_17_18_50190),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.42/0.60 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:((rinvR(X,Y)&(![Z0]:(![Z1]:((rr(Y,Z0)&rr(Y,Z1))=>Z0=Z1))))&(?[Z]:(rr(Y,Z)&cp1(Z)))))&cp2(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.42/0.60 fof(c41,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:((rinvR(X,Y)&(![Z0]:(![Z1]:((~rr(Y,Z0)|~rr(Y,Z1))|Z0=Z1))))&(?[Z]:(rr(Y,Z)&cp1(Z)))))&cp2(X)))&(((![Y]:((~rinvR(X,Y)|(?[Z0]:(?[Z1]:((rr(Y,Z0)&rr(Y,Z1))&Z0!=Z1))))|(![Z]:(~rr(Y,Z)|~cp1(Z)))))|~cp2(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.42/0.60 fof(c42,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:((rinvR(X,Y)&(![Z0]:(![Z1]:((~rr(Y,Z0)|~rr(Y,Z1))|Z0=Z1))))&(?[Z]:(rr(Y,Z)&cp1(Z)))))&cp2(X))))&(![X]:(((![Y]:((~rinvR(X,Y)|(?[Z0]:(?[Z1]:((rr(Y,Z0)&rr(Y,Z1))&Z0!=Z1))))|(![Z]:(~rr(Y,Z)|~cp1(Z)))))|~cp2(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c41])).
% 0.42/0.60 fof(c43,plain,((![X10]:(~cUnsatisfiable(X10)|((?[X11]:((rinvR(X10,X11)&(![X12]:(![X13]:((~rr(X11,X12)|~rr(X11,X13))|X12=X13))))&(?[X14]:(rr(X11,X14)&cp1(X14)))))&cp2(X10))))&(![X15]:(((![X16]:((~rinvR(X15,X16)|(?[X17]:(?[X18]:((rr(X16,X17)&rr(X16,X18))&X17!=X18))))|(![X19]:(~rr(X16,X19)|~cp1(X19)))))|~cp2(X15))|cUnsatisfiable(X15)))),inference(variable_rename,[status(thm)],[c42])).
% 0.42/0.60 fof(c45,plain,(![X10]:(![X12]:(![X13]:(![X15]:(![X16]:(![X19]:((~cUnsatisfiable(X10)|(((rinvR(X10,skolem0001(X10))&((~rr(skolem0001(X10),X12)|~rr(skolem0001(X10),X13))|X12=X13))&(rr(skolem0001(X10),skolem0002(X10))&cp1(skolem0002(X10))))&cp2(X10)))&((((~rinvR(X15,X16)|((rr(X16,skolem0003(X15,X16))&rr(X16,skolem0004(X15,X16)))&skolem0003(X15,X16)!=skolem0004(X15,X16)))|(~rr(X16,X19)|~cp1(X19)))|~cp2(X15))|cUnsatisfiable(X15))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X10]:(~cUnsatisfiable(X10)|(((rinvR(X10,skolem0001(X10))&(![X12]:(![X13]:((~rr(skolem0001(X10),X12)|~rr(skolem0001(X10),X13))|X12=X13))))&(rr(skolem0001(X10),skolem0002(X10))&cp1(skolem0002(X10))))&cp2(X10))))&(![X15]:(((![X16]:((~rinvR(X15,X16)|((rr(X16,skolem0003(X15,X16))&rr(X16,skolem0004(X15,X16)))&skolem0003(X15,X16)!=skolem0004(X15,X16)))|(![X19]:(~rr(X16,X19)|~cp1(X19)))))|~cp2(X15))|cUnsatisfiable(X15)))),inference(skolemize,[status(esa)],[c43])).])).
% 0.42/0.60 fof(c46,plain,(![X10]:(![X12]:(![X13]:(![X15]:(![X16]:(![X19]:(((((~cUnsatisfiable(X10)|rinvR(X10,skolem0001(X10)))&(~cUnsatisfiable(X10)|((~rr(skolem0001(X10),X12)|~rr(skolem0001(X10),X13))|X12=X13)))&((~cUnsatisfiable(X10)|rr(skolem0001(X10),skolem0002(X10)))&(~cUnsatisfiable(X10)|cp1(skolem0002(X10)))))&(~cUnsatisfiable(X10)|cp2(X10)))&((((((~rinvR(X15,X16)|rr(X16,skolem0003(X15,X16)))|(~rr(X16,X19)|~cp1(X19)))|~cp2(X15))|cUnsatisfiable(X15))&((((~rinvR(X15,X16)|rr(X16,skolem0004(X15,X16)))|(~rr(X16,X19)|~cp1(X19)))|~cp2(X15))|cUnsatisfiable(X15)))&((((~rinvR(X15,X16)|skolem0003(X15,X16)!=skolem0004(X15,X16))|(~rr(X16,X19)|~cp1(X19)))|~cp2(X15))|cUnsatisfiable(X15)))))))))),inference(distribute,[status(thm)],[c45])).
% 0.42/0.60 cnf(c51,plain,~cUnsatisfiable(X77)|cp2(X77),inference(split_conjunct,[status(thm)],[c46])).
% 0.42/0.60 cnf(c114,plain,cp2(i2003_11_14_17_18_50190),inference(resolution,[status(thm)],[c51, c12])).
% 0.42/0.60 cnf(c115,plain,~cp1(i2003_11_14_17_18_50190),inference(resolution,[status(thm)],[c114, c38])).
% 0.42/0.60 cnf(c50,plain,~cUnsatisfiable(X88)|cp1(skolem0002(X88)),inference(split_conjunct,[status(thm)],[c46])).
% 0.42/0.60 cnf(c117,plain,cp1(skolem0002(i2003_11_14_17_18_50190)),inference(resolution,[status(thm)],[c50, c12])).
% 0.42/0.60 cnf(c3,axiom,X96!=X95|~cp1(X96)|cp1(X95),theory(equality)).
% 0.42/0.60 cnf(c49,plain,~cUnsatisfiable(X147)|rr(skolem0001(X147),skolem0002(X147)),inference(split_conjunct,[status(thm)],[c46])).
% 0.42/0.60 cnf(c132,plain,rr(skolem0001(i2003_11_14_17_18_50190),skolem0002(i2003_11_14_17_18_50190)),inference(resolution,[status(thm)],[c49, c12])).
% 0.42/0.60 fof(axiom_7,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.42/0.60 fof(c13,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.42/0.60 fof(c14,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c13])).
% 0.42/0.60 fof(c16,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rinvR(X2,X3)|rr(X3,X2))&(~rr(X5,X4)|rinvR(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X2]:(![X3]:(~rinvR(X2,X3)|rr(X3,X2))))&(![X4]:(![X5]:(~rr(X5,X4)|rinvR(X4,X5))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.42/0.60 cnf(c17,plain,~rinvR(X85,X84)|rr(X84,X85),inference(split_conjunct,[status(thm)],[c16])).
% 0.42/0.60 cnf(c47,plain,~cUnsatisfiable(X94)|rinvR(X94,skolem0001(X94)),inference(split_conjunct,[status(thm)],[c46])).
% 0.42/0.60 cnf(c118,plain,rinvR(i2003_11_14_17_18_50190,skolem0001(i2003_11_14_17_18_50190)),inference(resolution,[status(thm)],[c47, c12])).
% 0.42/0.60 cnf(c119,plain,rr(skolem0001(i2003_11_14_17_18_50190),i2003_11_14_17_18_50190),inference(resolution,[status(thm)],[c118, c17])).
% 0.42/0.60 cnf(c48,plain,~cUnsatisfiable(X137)|~rr(skolem0001(X137),X138)|~rr(skolem0001(X137),X136)|X138=X136,inference(split_conjunct,[status(thm)],[c46])).
% 0.42/0.60 cnf(c131,plain,~cUnsatisfiable(i2003_11_14_17_18_50190)|~rr(skolem0001(i2003_11_14_17_18_50190),X185)|X185=i2003_11_14_17_18_50190,inference(resolution,[status(thm)],[c48, c119])).
% 0.42/0.60 cnf(c160,plain,~cUnsatisfiable(i2003_11_14_17_18_50190)|skolem0002(i2003_11_14_17_18_50190)=i2003_11_14_17_18_50190,inference(resolution,[status(thm)],[c131, c132])).
% 0.42/0.60 cnf(c162,plain,skolem0002(i2003_11_14_17_18_50190)=i2003_11_14_17_18_50190,inference(resolution,[status(thm)],[c160, c12])).
% 0.42/0.60 cnf(c163,plain,~cp1(skolem0002(i2003_11_14_17_18_50190))|cp1(i2003_11_14_17_18_50190),inference(resolution,[status(thm)],[c162, c3])).
% 0.42/0.60 cnf(c187,plain,cp1(i2003_11_14_17_18_50190),inference(resolution,[status(thm)],[c163, c117])).
% 0.42/0.60 cnf(c188,plain,$false,inference(resolution,[status(thm)],[c187, c115])).
% 0.42/0.60 % SZS output end CNFRefutation
% 0.42/0.60
% 0.42/0.60 % Initial clauses : 54
% 0.42/0.60 % Processed clauses : 66
% 0.42/0.60 % Factors computed : 2
% 0.42/0.60 % Resolvents computed: 79
% 0.42/0.60 % Tautologies deleted: 11
% 0.42/0.60 % Forward subsumed : 31
% 0.42/0.60 % Backward subsumed : 2
% 0.42/0.60 % -------- CPU Time ---------
% 0.42/0.60 % User time : 0.232 s
% 0.42/0.60 % System time : 0.015 s
% 0.42/0.60 % Total time : 0.247 s
%------------------------------------------------------------------------------