%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS078+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:38 EDT 2024
% Result : Unsatisfiable 0.47s 0.67s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS078+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.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:11:37 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.47/0.67 % Version: 1.5
% 0.47/0.67 % SZS status Unsatisfiable
% 0.47/0.67 % SZS output start CNFRefutation
% 0.47/0.67 fof(axiom_4,axiom,cUnsatisfiable(i2003_11_14_17_19_13721),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.47/0.67 cnf(c10,plain,cUnsatisfiable(i2003_11_14_17_19_13721),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.47/0.67 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:((rr(X,Y)&(?[Z]:(rinvR(Y,Z)&(![W]:(rs(Z,W)=>cp(W))))))&(![Z0]:(![Z1]:((rinvR(Y,Z0)&rinvR(Y,Z1))=>Z0=Z1)))))&(?[Y]:((rs(X,Y)&(~cq(Y)))&(~cp(Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.47/0.67 fof(c17,plain,(![X]:(cUnsatisfiable(X)<=>((?[Y]:((rr(X,Y)&(?[Z]:(rinvR(Y,Z)&(![W]:(rs(Z,W)=>cp(W))))))&(![Z0]:(![Z1]:((rinvR(Y,Z0)&rinvR(Y,Z1))=>Z0=Z1)))))&(?[Y]:((rs(X,Y)&~cq(Y))&~cp(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.47/0.67 fof(c18,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:((rr(X,Y)&(?[Z]:(rinvR(Y,Z)&(![W]:(~rs(Z,W)|cp(W))))))&(![Z0]:(![Z1]:((~rinvR(Y,Z0)|~rinvR(Y,Z1))|Z0=Z1)))))&(?[Y]:((rs(X,Y)&~cq(Y))&~cp(Y)))))&(((![Y]:((~rr(X,Y)|(![Z]:(~rinvR(Y,Z)|(?[W]:(rs(Z,W)&~cp(W))))))|(?[Z0]:(?[Z1]:((rinvR(Y,Z0)&rinvR(Y,Z1))&Z0!=Z1)))))|(![Y]:((~rs(X,Y)|cq(Y))|cp(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c17])).
% 0.47/0.67 fof(c19,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:((rr(X,Y)&(?[Z]:(rinvR(Y,Z)&(![W]:(~rs(Z,W)|cp(W))))))&(![Z0]:(![Z1]:((~rinvR(Y,Z0)|~rinvR(Y,Z1))|Z0=Z1)))))&(?[Y]:((rs(X,Y)&~cq(Y))&~cp(Y))))))&(![X]:(((![Y]:((~rr(X,Y)|(![Z]:(~rinvR(Y,Z)|(?[W]:(rs(Z,W)&~cp(W))))))|(?[Z0]:(?[Z1]:((rinvR(Y,Z0)&rinvR(Y,Z1))&Z0!=Z1)))))|(![Y]:((~rs(X,Y)|cq(Y))|cp(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c18])).
% 0.47/0.67 fof(c20,plain,((![X6]:(~cUnsatisfiable(X6)|((?[X7]:((rr(X6,X7)&(?[X8]:(rinvR(X7,X8)&(![X9]:(~rs(X8,X9)|cp(X9))))))&(![X10]:(![X11]:((~rinvR(X7,X10)|~rinvR(X7,X11))|X10=X11)))))&(?[X12]:((rs(X6,X12)&~cq(X12))&~cp(X12))))))&(![X13]:(((![X14]:((~rr(X13,X14)|(![X15]:(~rinvR(X14,X15)|(?[X16]:(rs(X15,X16)&~cp(X16))))))|(?[X17]:(?[X18]:((rinvR(X14,X17)&rinvR(X14,X18))&X17!=X18)))))|(![X19]:((~rs(X13,X19)|cq(X19))|cp(X19))))|cUnsatisfiable(X13)))),inference(variable_rename,[status(thm)],[c19])).
% 0.47/0.67 fof(c22,plain,(![X6]:(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X19]:((~cUnsatisfiable(X6)|(((rr(X6,skolem0001(X6))&(rinvR(skolem0001(X6),skolem0002(X6))&(~rs(skolem0002(X6),X9)|cp(X9))))&((~rinvR(skolem0001(X6),X10)|~rinvR(skolem0001(X6),X11))|X10=X11))&((rs(X6,skolem0003(X6))&~cq(skolem0003(X6)))&~cp(skolem0003(X6)))))&((((~rr(X13,X14)|(~rinvR(X14,X15)|(rs(X15,skolem0004(X13,X14,X15))&~cp(skolem0004(X13,X14,X15)))))|((rinvR(X14,skolem0005(X13,X14))&rinvR(X14,skolem0006(X13,X14)))&skolem0005(X13,X14)!=skolem0006(X13,X14)))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13))))))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X6]:(~cUnsatisfiable(X6)|(((rr(X6,skolem0001(X6))&(rinvR(skolem0001(X6),skolem0002(X6))&(![X9]:(~rs(skolem0002(X6),X9)|cp(X9)))))&(![X10]:(![X11]:((~rinvR(skolem0001(X6),X10)|~rinvR(skolem0001(X6),X11))|X10=X11))))&((rs(X6,skolem0003(X6))&~cq(skolem0003(X6)))&~cp(skolem0003(X6))))))&(![X13]:(((![X14]:((~rr(X13,X14)|(![X15]:(~rinvR(X14,X15)|(rs(X15,skolem0004(X13,X14,X15))&~cp(skolem0004(X13,X14,X15))))))|((rinvR(X14,skolem0005(X13,X14))&rinvR(X14,skolem0006(X13,X14)))&skolem0005(X13,X14)!=skolem0006(X13,X14))))|(![X19]:((~rs(X13,X19)|cq(X19))|cp(X19))))|cUnsatisfiable(X13)))),inference(skolemize,[status(esa)],[c20])).])).
% 0.47/0.67 fof(c23,plain,(![X6]:(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X19]:(((((~cUnsatisfiable(X6)|rr(X6,skolem0001(X6)))&((~cUnsatisfiable(X6)|rinvR(skolem0001(X6),skolem0002(X6)))&(~cUnsatisfiable(X6)|(~rs(skolem0002(X6),X9)|cp(X9)))))&(~cUnsatisfiable(X6)|((~rinvR(skolem0001(X6),X10)|~rinvR(skolem0001(X6),X11))|X10=X11)))&(((~cUnsatisfiable(X6)|rs(X6,skolem0003(X6)))&(~cUnsatisfiable(X6)|~cq(skolem0003(X6))))&(~cUnsatisfiable(X6)|~cp(skolem0003(X6)))))&(((((((~rr(X13,X14)|(~rinvR(X14,X15)|rs(X15,skolem0004(X13,X14,X15))))|rinvR(X14,skolem0005(X13,X14)))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13))&((((~rr(X13,X14)|(~rinvR(X14,X15)|rs(X15,skolem0004(X13,X14,X15))))|rinvR(X14,skolem0006(X13,X14)))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13)))&((((~rr(X13,X14)|(~rinvR(X14,X15)|rs(X15,skolem0004(X13,X14,X15))))|skolem0005(X13,X14)!=skolem0006(X13,X14))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13)))&((((((~rr(X13,X14)|(~rinvR(X14,X15)|~cp(skolem0004(X13,X14,X15))))|rinvR(X14,skolem0005(X13,X14)))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13))&((((~rr(X13,X14)|(~rinvR(X14,X15)|~cp(skolem0004(X13,X14,X15))))|rinvR(X14,skolem0006(X13,X14)))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13)))&((((~rr(X13,X14)|(~rinvR(X14,X15)|~cp(skolem0004(X13,X14,X15))))|skolem0005(X13,X14)!=skolem0006(X13,X14))|((~rs(X13,X19)|cq(X19))|cp(X19)))|cUnsatisfiable(X13))))))))))))),inference(distribute,[status(thm)],[c22])).
% 0.47/0.67 cnf(c30,plain,~cUnsatisfiable(X73)|~cp(skolem0003(X73)),inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c26,plain,~cUnsatisfiable(X125)|~rs(skolem0002(X125),X126)|cp(X126),inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c28,plain,~cUnsatisfiable(X81)|rs(X81,skolem0003(X81)),inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c97,plain,rs(i2003_11_14_17_19_13721,skolem0003(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c28, c10])).
% 0.47/0.67 fof(rs_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rs(A,C))=>rs(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rs_substitution_1)).
% 0.47/0.67 fof(c59,plain,(![A]:(![B]:(![C]:((A!=B|~rs(A,C))|rs(B,C))))),inference(fof_nnf,[status(thm)],[rs_substitution_1])).
% 0.47/0.67 fof(c60,plain,(![X31]:(![X32]:(![X33]:((X31!=X32|~rs(X31,X33))|rs(X32,X33))))),inference(variable_rename,[status(thm)],[c59])).
% 0.47/0.67 cnf(c61,plain,X130!=X131|~rs(X130,X132)|rs(X131,X132),inference(split_conjunct,[status(thm)],[c60])).
% 0.47/0.67 cnf(c111,plain,i2003_11_14_17_19_13721!=X149|rs(X149,skolem0003(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c61, c97])).
% 0.47/0.67 cnf(symmetry,axiom,X60!=X61|X61=X60,theory(equality)).
% 0.47/0.67 cnf(c25,plain,~cUnsatisfiable(X124)|rinvR(skolem0001(X124),skolem0002(X124)),inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c105,plain,rinvR(skolem0001(i2003_11_14_17_19_13721),skolem0002(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c25, c10])).
% 0.47/0.67 fof(axiom_3,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.47/0.67 fof(c11,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.47/0.67 fof(c12,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c11])).
% 0.47/0.67 fof(c14,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rinvR(X2,X3)|rr(X3,X2))&(~rr(X5,X4)|rinvR(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,((![X2]:(![X3]:(~rinvR(X2,X3)|rr(X3,X2))))&(![X4]:(![X5]:(~rr(X5,X4)|rinvR(X4,X5))))),inference(variable_rename,[status(thm)],[c12])).])).
% 0.47/0.67 cnf(c16,plain,~rr(X68,X67)|rinvR(X67,X68),inference(split_conjunct,[status(thm)],[c14])).
% 0.47/0.67 cnf(c24,plain,~cUnsatisfiable(X77)|rr(X77,skolem0001(X77)),inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c93,plain,rr(i2003_11_14_17_19_13721,skolem0001(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c24, c10])).
% 0.47/0.67 cnf(c95,plain,rinvR(skolem0001(i2003_11_14_17_19_13721),i2003_11_14_17_19_13721),inference(resolution,[status(thm)],[c93, c16])).
% 0.47/0.67 cnf(c27,plain,~cUnsatisfiable(X140)|~rinvR(skolem0001(X140),X141)|~rinvR(skolem0001(X140),X139)|X141=X139,inference(split_conjunct,[status(thm)],[c23])).
% 0.47/0.67 cnf(c117,plain,~cUnsatisfiable(i2003_11_14_17_19_13721)|~rinvR(skolem0001(i2003_11_14_17_19_13721),X189)|X189=i2003_11_14_17_19_13721,inference(resolution,[status(thm)],[c27, c95])).
% 0.47/0.67 cnf(c139,plain,~cUnsatisfiable(i2003_11_14_17_19_13721)|skolem0002(i2003_11_14_17_19_13721)=i2003_11_14_17_19_13721,inference(resolution,[status(thm)],[c117, c105])).
% 0.47/0.67 cnf(c140,plain,skolem0002(i2003_11_14_17_19_13721)=i2003_11_14_17_19_13721,inference(resolution,[status(thm)],[c139, c10])).
% 0.47/0.67 cnf(c146,plain,i2003_11_14_17_19_13721=skolem0002(i2003_11_14_17_19_13721),inference(resolution,[status(thm)],[c140, symmetry])).
% 0.47/0.67 cnf(c152,plain,rs(skolem0002(i2003_11_14_17_19_13721),skolem0003(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c146, c111])).
% 0.47/0.67 cnf(c170,plain,~cUnsatisfiable(i2003_11_14_17_19_13721)|cp(skolem0003(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c152, c26])).
% 0.47/0.67 cnf(c185,plain,cp(skolem0003(i2003_11_14_17_19_13721)),inference(resolution,[status(thm)],[c170, c10])).
% 0.47/0.67 cnf(c186,plain,~cUnsatisfiable(i2003_11_14_17_19_13721),inference(resolution,[status(thm)],[c185, c30])).
% 0.47/0.67 cnf(c187,plain,$false,inference(resolution,[status(thm)],[c186, c10])).
% 0.47/0.67 % SZS output end CNFRefutation
% 0.47/0.67
% 0.47/0.67 % Initial clauses : 46
% 0.47/0.67 % Processed clauses : 78
% 0.47/0.67 % Factors computed : 2
% 0.47/0.67 % Resolvents computed: 97
% 0.47/0.67 % Tautologies deleted: 8
% 0.47/0.67 % Forward subsumed : 37
% 0.47/0.67 % Backward subsumed : 5
% 0.47/0.67 % -------- CPU Time ---------
% 0.47/0.67 % User time : 0.311 s
% 0.47/0.67 % System time : 0.012 s
% 0.47/0.67 % Total time : 0.323 s
%------------------------------------------------------------------------------