%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS073+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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.42s 0.61s
% Output : Refutation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS073+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n021.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:09:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.42/0.61 % Version: 1.5
% 0.42/0.61 % SZS status Unsatisfiable
% 0.42/0.61 % SZS output start CNFRefutation
% 0.42/0.61 fof(axiom_9,axiom,cUnsatisfiable(i2003_11_14_17_18_54369),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.42/0.61 cnf(c18,plain,cUnsatisfiable(i2003_11_14_17_18_54369),inference(split_conjunct,[status(thm)],[axiom_9])).
% 0.42/0.61 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:((rf(X,Y)&(![Z]:(rinvS(Y,Z)=>cp(Z))))&(![Z]:(rinvF(Y,Z)=>(?[W]:(rs(Z,W)&cp(W)))))))&(~cp(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.42/0.61 fof(c46,plain,(![X]:(cUnsatisfiable(X)<=>((?[Y]:((rf(X,Y)&(![Z]:(rinvS(Y,Z)=>cp(Z))))&(![Z]:(rinvF(Y,Z)=>(?[W]:(rs(Z,W)&cp(W)))))))&~cp(X)))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.42/0.61 fof(c47,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:((rf(X,Y)&(![Z]:(~rinvS(Y,Z)|cp(Z))))&(![Z]:(~rinvF(Y,Z)|(?[W]:(rs(Z,W)&cp(W)))))))&~cp(X)))&(((![Y]:((~rf(X,Y)|(?[Z]:(rinvS(Y,Z)&~cp(Z))))|(?[Z]:(rinvF(Y,Z)&(![W]:(~rs(Z,W)|~cp(W)))))))|cp(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c46])).
% 0.42/0.61 fof(c48,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:((rf(X,Y)&(![Z]:(~rinvS(Y,Z)|cp(Z))))&(![Z]:(~rinvF(Y,Z)|(?[W]:(rs(Z,W)&cp(W)))))))&~cp(X))))&(![X]:(((![Y]:((~rf(X,Y)|(?[Z]:(rinvS(Y,Z)&~cp(Z))))|(?[Z]:(rinvF(Y,Z)&(![W]:(~rs(Z,W)|~cp(W)))))))|cp(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c47])).
% 0.42/0.61 fof(c49,plain,((![X27]:(~cUnsatisfiable(X27)|((?[X28]:((rf(X27,X28)&(![X29]:(~rinvS(X28,X29)|cp(X29))))&(![X30]:(~rinvF(X28,X30)|(?[X31]:(rs(X30,X31)&cp(X31)))))))&~cp(X27))))&(![X32]:(((![X33]:((~rf(X32,X33)|(?[X34]:(rinvS(X33,X34)&~cp(X34))))|(?[X35]:(rinvF(X33,X35)&(![X36]:(~rs(X35,X36)|~cp(X36)))))))|cp(X32))|cUnsatisfiable(X32)))),inference(variable_rename,[status(thm)],[c48])).
% 0.42/0.61 fof(c51,plain,(![X27]:(![X29]:(![X30]:(![X32]:(![X33]:(![X36]:((~cUnsatisfiable(X27)|(((rf(X27,skolem0001(X27))&(~rinvS(skolem0001(X27),X29)|cp(X29)))&(~rinvF(skolem0001(X27),X30)|(rs(X30,skolem0002(X27,X30))&cp(skolem0002(X27,X30)))))&~cp(X27)))&((((~rf(X32,X33)|(rinvS(X33,skolem0003(X32,X33))&~cp(skolem0003(X32,X33))))|(rinvF(X33,skolem0004(X32,X33))&(~rs(skolem0004(X32,X33),X36)|~cp(X36))))|cp(X32))|cUnsatisfiable(X32))))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X27]:(~cUnsatisfiable(X27)|(((rf(X27,skolem0001(X27))&(![X29]:(~rinvS(skolem0001(X27),X29)|cp(X29))))&(![X30]:(~rinvF(skolem0001(X27),X30)|(rs(X30,skolem0002(X27,X30))&cp(skolem0002(X27,X30))))))&~cp(X27))))&(![X32]:(((![X33]:((~rf(X32,X33)|(rinvS(X33,skolem0003(X32,X33))&~cp(skolem0003(X32,X33))))|(rinvF(X33,skolem0004(X32,X33))&(![X36]:(~rs(skolem0004(X32,X33),X36)|~cp(X36))))))|cp(X32))|cUnsatisfiable(X32)))),inference(skolemize,[status(esa)],[c49])).])).
% 0.42/0.61 fof(c52,plain,(![X27]:(![X29]:(![X30]:(![X32]:(![X33]:(![X36]:(((((~cUnsatisfiable(X27)|rf(X27,skolem0001(X27)))&(~cUnsatisfiable(X27)|(~rinvS(skolem0001(X27),X29)|cp(X29))))&((~cUnsatisfiable(X27)|(~rinvF(skolem0001(X27),X30)|rs(X30,skolem0002(X27,X30))))&(~cUnsatisfiable(X27)|(~rinvF(skolem0001(X27),X30)|cp(skolem0002(X27,X30))))))&(~cUnsatisfiable(X27)|~cp(X27)))&((((((~rf(X32,X33)|rinvS(X33,skolem0003(X32,X33)))|rinvF(X33,skolem0004(X32,X33)))|cp(X32))|cUnsatisfiable(X32))&((((~rf(X32,X33)|rinvS(X33,skolem0003(X32,X33)))|(~rs(skolem0004(X32,X33),X36)|~cp(X36)))|cp(X32))|cUnsatisfiable(X32)))&(((((~rf(X32,X33)|~cp(skolem0003(X32,X33)))|rinvF(X33,skolem0004(X32,X33)))|cp(X32))|cUnsatisfiable(X32))&((((~rf(X32,X33)|~cp(skolem0003(X32,X33)))|(~rs(skolem0004(X32,X33),X36)|~cp(X36)))|cp(X32))|cUnsatisfiable(X32))))))))))),inference(distribute,[status(thm)],[c51])).
% 0.42/0.61 cnf(c57,plain,~cUnsatisfiable(X92)|~cp(X92),inference(split_conjunct,[status(thm)],[c52])).
% 0.42/0.61 cnf(c54,plain,~cUnsatisfiable(X178)|~rinvS(skolem0001(X178),X177)|cp(X177),inference(split_conjunct,[status(thm)],[c52])).
% 0.42/0.61 fof(axiom_7,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.42/0.61 fof(c22,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.42/0.61 fof(c23,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.42/0.61 fof(c25,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvS(X9,X10)|rs(X10,X9))&(~rs(X12,X11)|rinvS(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X9]:(![X10]:(~rinvS(X9,X10)|rs(X10,X9))))&(![X11]:(![X12]:(~rs(X12,X11)|rinvS(X11,X12))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.42/0.61 cnf(c27,plain,~rs(X109,X108)|rinvS(X108,X109),inference(split_conjunct,[status(thm)],[c25])).
% 0.42/0.61 cnf(c53,plain,~cUnsatisfiable(X126)|rf(X126,skolem0001(X126)),inference(split_conjunct,[status(thm)],[c52])).
% 0.42/0.61 cnf(c134,plain,rf(i2003_11_14_17_18_54369,skolem0001(i2003_11_14_17_18_54369)),inference(resolution,[status(thm)],[c53, c18])).
% 0.42/0.61 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.42/0.61 fof(c43,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.42/0.61 fof(c44,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c43])).
% 0.42/0.61 cnf(c45,plain,~rf(X172,X174)|~rf(X172,X173)|X174=X173,inference(split_conjunct,[status(thm)],[c44])).
% 0.42/0.61 cnf(c145,plain,~rf(i2003_11_14_17_18_54369,X227)|X227=skolem0001(i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c45, c134])).
% 0.42/0.61 fof(axiom_11,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.42/0.61 fof(c12,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.42/0.61 fof(c13,plain,(![X2]:(![X3]:(~rs(X2,X3)|rf(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.42/0.61 cnf(c14,plain,~rs(X99,X100)|rf(X99,X100),inference(split_conjunct,[status(thm)],[c13])).
% 0.42/0.61 fof(axiom_5,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.42/0.61 fof(c34,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.42/0.61 fof(c35,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c34])).
% 0.42/0.61 fof(c37,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~rinvF(X17,X18)|rf(X18,X17))&(~rf(X20,X19)|rinvF(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X17]:(![X18]:(~rinvF(X17,X18)|rf(X18,X17))))&(![X19]:(![X20]:(~rf(X20,X19)|rinvF(X19,X20))))),inference(variable_rename,[status(thm)],[c35])).])).
% 0.42/0.61 cnf(c39,plain,~rf(X119,X120)|rinvF(X120,X119),inference(split_conjunct,[status(thm)],[c37])).
% 0.42/0.61 cnf(c135,plain,rinvF(skolem0001(i2003_11_14_17_18_54369),i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c134, c39])).
% 0.42/0.61 cnf(c55,plain,~cUnsatisfiable(X230)|~rinvF(skolem0001(X230),X231)|rs(X231,skolem0002(X230,X231)),inference(split_conjunct,[status(thm)],[c52])).
% 0.42/0.61 cnf(c153,plain,~cUnsatisfiable(i2003_11_14_17_18_54369)|rs(i2003_11_14_17_18_54369,skolem0002(i2003_11_14_17_18_54369,i2003_11_14_17_18_54369)),inference(resolution,[status(thm)],[c55, c135])).
% 0.42/0.61 cnf(c159,plain,rs(i2003_11_14_17_18_54369,skolem0002(i2003_11_14_17_18_54369,i2003_11_14_17_18_54369)),inference(resolution,[status(thm)],[c153, c18])).
% 0.42/0.61 cnf(c163,plain,rf(i2003_11_14_17_18_54369,skolem0002(i2003_11_14_17_18_54369,i2003_11_14_17_18_54369)),inference(resolution,[status(thm)],[c159, c14])).
% 0.42/0.61 cnf(c178,plain,skolem0002(i2003_11_14_17_18_54369,i2003_11_14_17_18_54369)=skolem0001(i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c163, c145])).
% 0.42/0.61 fof(rs_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rs(C,A))=>rs(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rs_substitution_2)).
% 0.42/0.61 fof(c81,plain,(![A]:(![B]:(![C]:((A!=B|~rs(C,A))|rs(C,B))))),inference(fof_nnf,[status(thm)],[rs_substitution_2])).
% 0.42/0.61 fof(c82,plain,(![X45]:(![X46]:(![X47]:((X45!=X46|~rs(X47,X45))|rs(X47,X46))))),inference(variable_rename,[status(thm)],[c81])).
% 0.42/0.61 cnf(c83,plain,X180!=X181|~rs(X179,X180)|rs(X179,X181),inference(split_conjunct,[status(thm)],[c82])).
% 0.42/0.61 cnf(c162,plain,skolem0002(i2003_11_14_17_18_54369,i2003_11_14_17_18_54369)!=X243|rs(i2003_11_14_17_18_54369,X243),inference(resolution,[status(thm)],[c159, c83])).
% 0.42/0.61 cnf(c207,plain,rs(i2003_11_14_17_18_54369,skolem0001(i2003_11_14_17_18_54369)),inference(resolution,[status(thm)],[c162, c178])).
% 0.42/0.61 cnf(c209,plain,rinvS(skolem0001(i2003_11_14_17_18_54369),i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c207, c27])).
% 0.42/0.61 cnf(c224,plain,~cUnsatisfiable(i2003_11_14_17_18_54369)|cp(i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c209, c54])).
% 0.42/0.61 cnf(c231,plain,cp(i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c224, c18])).
% 0.42/0.61 cnf(c232,plain,~cUnsatisfiable(i2003_11_14_17_18_54369),inference(resolution,[status(thm)],[c231, c57])).
% 0.42/0.61 cnf(c233,plain,$false,inference(resolution,[status(thm)],[c232, c18])).
% 0.42/0.61 % SZS output end CNFRefutation
% 0.42/0.61
% 0.42/0.61 % Initial clauses : 58
% 0.42/0.61 % Processed clauses : 78
% 0.42/0.61 % Factors computed : 4
% 0.42/0.61 % Resolvents computed: 101
% 0.42/0.61 % Tautologies deleted: 7
% 0.42/0.61 % Forward subsumed : 26
% 0.42/0.61 % Backward subsumed : 3
% 0.42/0.61 % -------- CPU Time ---------
% 0.42/0.61 % User time : 0.242 s
% 0.42/0.61 % System time : 0.010 s
% 0.42/0.61 % Total time : 0.252 s
%------------------------------------------------------------------------------