%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS076+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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.60s 0.78s
% Output : Refutation 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : KRS076+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n004.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:11:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.60/0.78 % Version: 1.5
% 0.60/0.78 % SZS status Unsatisfiable
% 0.60/0.78 % SZS output start CNFRefutation
% 0.60/0.78 fof(axiom_9,axiom,cUnsatisfiable(i2003_11_14_17_19_06193),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.60/0.78 cnf(c18,plain,cUnsatisfiable(i2003_11_14_17_19_06193),inference(split_conjunct,[status(thm)],[axiom_9])).
% 0.60/0.78 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:((rf1(X,Y)&(~cp(Y)))&(![Z]:(rinvF1(Y,Z)=>(?[W]:(rs(Z,W)&cowlThing(W)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.60/0.78 fof(c46,plain,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:((rf1(X,Y)&~cp(Y))&(![Z]:(rinvF1(Y,Z)=>(?[W]:(rs(Z,W)&cowlThing(W)))))))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.60/0.78 fof(c47,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:((rf1(X,Y)&~cp(Y))&(![Z]:(~rinvF1(Y,Z)|(?[W]:(rs(Z,W)&cowlThing(W)))))))))&(((![Y]:(~rf(X,Y)|~cp(Y)))|(![Y]:((~rf1(X,Y)|cp(Y))|(?[Z]:(rinvF1(Y,Z)&(![W]:(~rs(Z,W)|~cowlThing(W))))))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c46])).
% 0.60/0.78 fof(c48,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rf(X,Y)&cp(Y)))&(?[Y]:((rf1(X,Y)&~cp(Y))&(![Z]:(~rinvF1(Y,Z)|(?[W]:(rs(Z,W)&cowlThing(W))))))))))&(![X]:(((![Y]:(~rf(X,Y)|~cp(Y)))|(![Y]:((~rf1(X,Y)|cp(Y))|(?[Z]:(rinvF1(Y,Z)&(![W]:(~rs(Z,W)|~cowlThing(W))))))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c47])).
% 0.60/0.78 fof(c49,plain,((![X27]:(~cUnsatisfiable(X27)|((?[X28]:(rf(X27,X28)&cp(X28)))&(?[X29]:((rf1(X27,X29)&~cp(X29))&(![X30]:(~rinvF1(X29,X30)|(?[X31]:(rs(X30,X31)&cowlThing(X31))))))))))&(![X32]:(((![X33]:(~rf(X32,X33)|~cp(X33)))|(![X34]:((~rf1(X32,X34)|cp(X34))|(?[X35]:(rinvF1(X34,X35)&(![X36]:(~rs(X35,X36)|~cowlThing(X36))))))))|cUnsatisfiable(X32)))),inference(variable_rename,[status(thm)],[c48])).
% 0.60/0.78 fof(c51,plain,(![X27]:(![X30]:(![X32]:(![X33]:(![X34]:(![X36]:((~cUnsatisfiable(X27)|((rf(X27,skolem0001(X27))&cp(skolem0001(X27)))&((rf1(X27,skolem0002(X27))&~cp(skolem0002(X27)))&(~rinvF1(skolem0002(X27),X30)|(rs(X30,skolem0003(X27,X30))&cowlThing(skolem0003(X27,X30)))))))&(((~rf(X32,X33)|~cp(X33))|((~rf1(X32,X34)|cp(X34))|(rinvF1(X34,skolem0004(X32,X34))&(~rs(skolem0004(X32,X34),X36)|~cowlThing(X36)))))|cUnsatisfiable(X32))))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X27]:(~cUnsatisfiable(X27)|((rf(X27,skolem0001(X27))&cp(skolem0001(X27)))&((rf1(X27,skolem0002(X27))&~cp(skolem0002(X27)))&(![X30]:(~rinvF1(skolem0002(X27),X30)|(rs(X30,skolem0003(X27,X30))&cowlThing(skolem0003(X27,X30)))))))))&(![X32]:(((![X33]:(~rf(X32,X33)|~cp(X33)))|(![X34]:((~rf1(X32,X34)|cp(X34))|(rinvF1(X34,skolem0004(X32,X34))&(![X36]:(~rs(skolem0004(X32,X34),X36)|~cowlThing(X36)))))))|cUnsatisfiable(X32)))),inference(skolemize,[status(esa)],[c49])).])).
% 0.60/0.78 fof(c52,plain,(![X27]:(![X30]:(![X32]:(![X33]:(![X34]:(![X36]:((((~cUnsatisfiable(X27)|rf(X27,skolem0001(X27)))&(~cUnsatisfiable(X27)|cp(skolem0001(X27))))&(((~cUnsatisfiable(X27)|rf1(X27,skolem0002(X27)))&(~cUnsatisfiable(X27)|~cp(skolem0002(X27))))&((~cUnsatisfiable(X27)|(~rinvF1(skolem0002(X27),X30)|rs(X30,skolem0003(X27,X30))))&(~cUnsatisfiable(X27)|(~rinvF1(skolem0002(X27),X30)|cowlThing(skolem0003(X27,X30)))))))&((((~rf(X32,X33)|~cp(X33))|((~rf1(X32,X34)|cp(X34))|rinvF1(X34,skolem0004(X32,X34))))|cUnsatisfiable(X32))&(((~rf(X32,X33)|~cp(X33))|((~rf1(X32,X34)|cp(X34))|(~rs(skolem0004(X32,X34),X36)|~cowlThing(X36))))|cUnsatisfiable(X32)))))))))),inference(distribute,[status(thm)],[c51])).
% 0.60/0.78 cnf(c56,plain,~cUnsatisfiable(X121)|~cp(skolem0002(X121)),inference(split_conjunct,[status(thm)],[c52])).
% 0.60/0.78 cnf(c54,plain,~cUnsatisfiable(X120)|cp(skolem0001(X120)),inference(split_conjunct,[status(thm)],[c52])).
% 0.60/0.78 cnf(c133,plain,cp(skolem0001(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c54, c18])).
% 0.60/0.78 cnf(c3,axiom,X131!=X132|~cp(X131)|cp(X132),theory(equality)).
% 0.60/0.78 cnf(c55,plain,~cUnsatisfiable(X130)|rf1(X130,skolem0002(X130)),inference(split_conjunct,[status(thm)],[c52])).
% 0.60/0.78 cnf(c137,plain,rf1(i2003_11_14_17_19_06193,skolem0002(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c55, c18])).
% 0.60/0.78 fof(axiom_4,axiom,(![X]:(![Y]:(![Z]:((rf1(X,Y)&rf1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.60/0.78 fof(c40,plain,(![X]:(![Y]:(![Z]:((~rf1(X,Y)|~rf1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.60/0.78 fof(c41,plain,(![X21]:(![X22]:(![X23]:((~rf1(X21,X22)|~rf1(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c40])).
% 0.60/0.78 cnf(c42,plain,~rf1(X167,X166)|~rf1(X167,X165)|X166=X165,inference(split_conjunct,[status(thm)],[c41])).
% 0.60/0.78 cnf(c147,plain,~rf1(i2003_11_14_17_19_06193,X223)|X223=skolem0002(i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c42, c137])).
% 0.60/0.78 fof(axiom_10,axiom,(![X]:(![Y]:(rs(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.60/0.78 fof(c15,plain,(![X]:(![Y]:(~rs(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.60/0.78 fof(c16,plain,(![X4]:(![X5]:(~rs(X4,X5)|rf1(X4,X5)))),inference(variable_rename,[status(thm)],[c15])).
% 0.60/0.78 cnf(c17,plain,~rs(X100,X101)|rf1(X100,X101),inference(split_conjunct,[status(thm)],[c16])).
% 0.60/0.78 cnf(c53,plain,~cUnsatisfiable(X127)|rf(X127,skolem0001(X127)),inference(split_conjunct,[status(thm)],[c52])).
% 0.60/0.78 cnf(c134,plain,rf(i2003_11_14_17_19_06193,skolem0001(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c53, c18])).
% 0.60/0.78 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.60/0.78 fof(c43,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.60/0.78 fof(c44,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c43])).
% 0.60/0.78 cnf(c45,plain,~rf(X176,X175)|~rf(X176,X174)|X175=X174,inference(split_conjunct,[status(thm)],[c44])).
% 0.60/0.78 cnf(c150,plain,~rf(i2003_11_14_17_19_06193,X228)|X228=skolem0001(i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c45, c134])).
% 0.60/0.78 fof(axiom_11,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.60/0.78 fof(c12,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.60/0.78 fof(c13,plain,(![X2]:(![X3]:(~rs(X2,X3)|rf(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.60/0.78 cnf(c14,plain,~rs(X98,X99)|rf(X98,X99),inference(split_conjunct,[status(thm)],[c13])).
% 0.60/0.78 fof(axiom_6,axiom,(![X]:(![Y]:(rinvF1(X,Y)<=>rf1(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.60/0.78 fof(c28,plain,(![X]:(![Y]:((~rinvF1(X,Y)|rf1(Y,X))&(~rf1(Y,X)|rinvF1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.60/0.78 fof(c29,plain,((![X]:(![Y]:(~rinvF1(X,Y)|rf1(Y,X))))&(![X]:(![Y]:(~rf1(Y,X)|rinvF1(X,Y))))),inference(shift_quantors,[status(thm)],[c28])).
% 0.60/0.78 fof(c31,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rinvF1(X13,X14)|rf1(X14,X13))&(~rf1(X16,X15)|rinvF1(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X13]:(![X14]:(~rinvF1(X13,X14)|rf1(X14,X13))))&(![X15]:(![X16]:(~rf1(X16,X15)|rinvF1(X15,X16))))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.60/0.78 cnf(c33,plain,~rf1(X112,X111)|rinvF1(X111,X112),inference(split_conjunct,[status(thm)],[c31])).
% 0.60/0.78 cnf(c138,plain,rinvF1(skolem0002(i2003_11_14_17_19_06193),i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c137, c33])).
% 0.60/0.78 cnf(c57,plain,~cUnsatisfiable(X231)|~rinvF1(skolem0002(X231),X230)|rs(X230,skolem0003(X231,X230)),inference(split_conjunct,[status(thm)],[c52])).
% 0.60/0.78 cnf(c163,plain,~cUnsatisfiable(i2003_11_14_17_19_06193)|rs(i2003_11_14_17_19_06193,skolem0003(i2003_11_14_17_19_06193,i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c57, c138])).
% 0.60/0.78 cnf(c172,plain,rs(i2003_11_14_17_19_06193,skolem0003(i2003_11_14_17_19_06193,i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c163, c18])).
% 0.60/0.78 cnf(c178,plain,rf(i2003_11_14_17_19_06193,skolem0003(i2003_11_14_17_19_06193,i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c172, c14])).
% 0.60/0.78 cnf(c192,plain,skolem0003(i2003_11_14_17_19_06193,i2003_11_14_17_19_06193)=skolem0001(i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c178, c150])).
% 0.60/0.78 fof(rs_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rs(C,A))=>rs(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rs_substitution_2)).
% 0.60/0.78 fof(c80,plain,(![A]:(![B]:(![C]:((A!=B|~rs(C,A))|rs(C,B))))),inference(fof_nnf,[status(thm)],[rs_substitution_2])).
% 0.60/0.78 fof(c81,plain,(![X45]:(![X46]:(![X47]:((X45!=X46|~rs(X47,X45))|rs(X47,X46))))),inference(variable_rename,[status(thm)],[c80])).
% 0.60/0.78 cnf(c82,plain,X181!=X179|~rs(X180,X181)|rs(X180,X179),inference(split_conjunct,[status(thm)],[c81])).
% 0.60/0.78 cnf(c177,plain,skolem0003(i2003_11_14_17_19_06193,i2003_11_14_17_19_06193)!=X262|rs(i2003_11_14_17_19_06193,X262),inference(resolution,[status(thm)],[c172, c82])).
% 0.60/0.78 cnf(c244,plain,rs(i2003_11_14_17_19_06193,skolem0001(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c177, c192])).
% 0.60/0.78 cnf(c255,plain,rf1(i2003_11_14_17_19_06193,skolem0001(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c244, c17])).
% 0.60/0.78 cnf(c276,plain,skolem0001(i2003_11_14_17_19_06193)=skolem0002(i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c255, c147])).
% 0.60/0.78 cnf(c313,plain,~cp(skolem0001(i2003_11_14_17_19_06193))|cp(skolem0002(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c276, c3])).
% 0.60/0.78 cnf(c406,plain,cp(skolem0002(i2003_11_14_17_19_06193)),inference(resolution,[status(thm)],[c313, c133])).
% 0.60/0.78 cnf(c407,plain,~cUnsatisfiable(i2003_11_14_17_19_06193),inference(resolution,[status(thm)],[c406, c56])).
% 0.60/0.78 cnf(c408,plain,$false,inference(resolution,[status(thm)],[c407, c18])).
% 0.60/0.78 % SZS output end CNFRefutation
% 0.60/0.78
% 0.60/0.78 % Initial clauses : 57
% 0.60/0.78 % Processed clauses : 141
% 0.60/0.78 % Factors computed : 4
% 0.60/0.78 % Resolvents computed: 277
% 0.60/0.78 % Tautologies deleted: 7
% 0.60/0.78 % Forward subsumed : 125
% 0.60/0.78 % Backward subsumed : 3
% 0.60/0.78 % -------- CPU Time ---------
% 0.60/0.78 % User time : 0.389 s
% 0.60/0.78 % System time : 0.019 s
% 0.60/0.78 % Total time : 0.408 s
%------------------------------------------------------------------------------