%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS110+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:43 EDT 2024
% Result : Unsatisfiable 0.45s 0.62s
% Output : Refutation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS110+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n019.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:05:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.45/0.62 % Version: 1.5
% 0.45/0.62 % SZS status Unsatisfiable
% 0.45/0.62 % SZS output start CNFRefutation
% 0.45/0.62 fof(axiom_5,axiom,(![X]:(ca_Ax2(X)<=>(cp(X)&(?[Y]:(rinvS(X,Y)&cp(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.45/0.62 fof(c49,plain,(![X]:((~ca_Ax2(X)|(cp(X)&(?[Y]:(rinvS(X,Y)&cp(Y)))))&((~cp(X)|(![Y]:(~rinvS(X,Y)|~cp(Y))))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.45/0.62 fof(c50,plain,((![X]:(~ca_Ax2(X)|(cp(X)&(?[Y]:(rinvS(X,Y)&cp(Y))))))&(![X]:((~cp(X)|(![Y]:(~rinvS(X,Y)|~cp(Y))))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c49])).
% 0.45/0.62 fof(c51,plain,((![X27]:(~ca_Ax2(X27)|(cp(X27)&(?[X28]:(rinvS(X27,X28)&cp(X28))))))&(![X29]:((~cp(X29)|(![X30]:(~rinvS(X29,X30)|~cp(X30))))|ca_Ax2(X29)))),inference(variable_rename,[status(thm)],[c50])).
% 0.45/0.62 fof(c53,plain,(![X27]:(![X29]:(![X30]:((~ca_Ax2(X27)|(cp(X27)&(rinvS(X27,skolem0001(X27))&cp(skolem0001(X27)))))&((~cp(X29)|(~rinvS(X29,X30)|~cp(X30)))|ca_Ax2(X29)))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X27]:(~ca_Ax2(X27)|(cp(X27)&(rinvS(X27,skolem0001(X27))&cp(skolem0001(X27))))))&(![X29]:((~cp(X29)|(![X30]:(~rinvS(X29,X30)|~cp(X30))))|ca_Ax2(X29)))),inference(skolemize,[status(esa)],[c51])).])).
% 0.45/0.62 fof(c54,plain,(![X27]:(![X29]:(![X30]:(((~ca_Ax2(X27)|cp(X27))&((~ca_Ax2(X27)|rinvS(X27,skolem0001(X27)))&(~ca_Ax2(X27)|cp(skolem0001(X27)))))&((~cp(X29)|(~rinvS(X29,X30)|~cp(X30)))|ca_Ax2(X29)))))),inference(distribute,[status(thm)],[c53])).
% 0.45/0.62 cnf(c55,plain,~ca_Ax2(X110)|cp(X110),inference(split_conjunct,[status(thm)],[c54])).
% 0.45/0.62 fof(axiom_12,axiom,cUnsatisfiable(i2003_11_14_17_21_12565),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.45/0.62 cnf(c21,plain,cUnsatisfiable(i2003_11_14_17_21_12565),inference(split_conjunct,[status(thm)],[axiom_12])).
% 0.45/0.62 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rs(X,Y)&ca_Ax2(Y)))&(![Y]:(rs(X,Y)=>cpxcomp(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.45/0.62 fof(c73,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rs(X,Y)&ca_Ax2(Y)))&(![Y]:(~rs(X,Y)|cpxcomp(Y)))))&(((![Y]:(~rs(X,Y)|~ca_Ax2(Y)))|(?[Y]:(rs(X,Y)&~cpxcomp(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.45/0.62 fof(c74,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rs(X,Y)&ca_Ax2(Y)))&(![Y]:(~rs(X,Y)|cpxcomp(Y))))))&(![X]:(((![Y]:(~rs(X,Y)|~ca_Ax2(Y)))|(?[Y]:(rs(X,Y)&~cpxcomp(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c73])).
% 0.45/0.62 fof(c75,plain,((![X39]:(~cUnsatisfiable(X39)|((?[X40]:(rs(X39,X40)&ca_Ax2(X40)))&(![X41]:(~rs(X39,X41)|cpxcomp(X41))))))&(![X42]:(((![X43]:(~rs(X42,X43)|~ca_Ax2(X43)))|(?[X44]:(rs(X42,X44)&~cpxcomp(X44))))|cUnsatisfiable(X42)))),inference(variable_rename,[status(thm)],[c74])).
% 0.45/0.62 fof(c77,plain,(![X39]:(![X41]:(![X42]:(![X43]:((~cUnsatisfiable(X39)|((rs(X39,skolem0004(X39))&ca_Ax2(skolem0004(X39)))&(~rs(X39,X41)|cpxcomp(X41))))&(((~rs(X42,X43)|~ca_Ax2(X43))|(rs(X42,skolem0005(X42))&~cpxcomp(skolem0005(X42))))|cUnsatisfiable(X42))))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,((![X39]:(~cUnsatisfiable(X39)|((rs(X39,skolem0004(X39))&ca_Ax2(skolem0004(X39)))&(![X41]:(~rs(X39,X41)|cpxcomp(X41))))))&(![X42]:(((![X43]:(~rs(X42,X43)|~ca_Ax2(X43)))|(rs(X42,skolem0005(X42))&~cpxcomp(skolem0005(X42))))|cUnsatisfiable(X42)))),inference(skolemize,[status(esa)],[c75])).])).
% 0.45/0.62 fof(c78,plain,(![X39]:(![X41]:(![X42]:(![X43]:((((~cUnsatisfiable(X39)|rs(X39,skolem0004(X39)))&(~cUnsatisfiable(X39)|ca_Ax2(skolem0004(X39))))&(~cUnsatisfiable(X39)|(~rs(X39,X41)|cpxcomp(X41))))&((((~rs(X42,X43)|~ca_Ax2(X43))|rs(X42,skolem0005(X42)))|cUnsatisfiable(X42))&(((~rs(X42,X43)|~ca_Ax2(X43))|~cpxcomp(skolem0005(X42)))|cUnsatisfiable(X42)))))))),inference(distribute,[status(thm)],[c77])).
% 0.45/0.62 cnf(c80,plain,~cUnsatisfiable(X147)|ca_Ax2(skolem0004(X147)),inference(split_conjunct,[status(thm)],[c78])).
% 0.45/0.62 cnf(c169,plain,ca_Ax2(skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c80, c21])).
% 0.45/0.62 cnf(c170,plain,cp(skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c169, c55])).
% 0.45/0.62 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.45/0.62 fof(c66,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.45/0.62 fof(c67,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c66])).
% 0.45/0.62 fof(c68,plain,((![X35]:(~cp(X35)|(![X36]:~ra_Px1(X35,X36))))&(![X37]:((?[X38]:ra_Px1(X37,X38))|cp(X37)))),inference(variable_rename,[status(thm)],[c67])).
% 0.45/0.62 fof(c70,plain,(![X35]:(![X36]:(![X37]:((~cp(X35)|~ra_Px1(X35,X36))&(ra_Px1(X37,skolem0003(X37))|cp(X37)))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X35]:(~cp(X35)|(![X36]:~ra_Px1(X35,X36))))&(![X37]:(ra_Px1(X37,skolem0003(X37))|cp(X37)))),inference(skolemize,[status(esa)],[c68])).])).
% 0.45/0.62 cnf(c71,plain,~cp(X122)|~ra_Px1(X122,X123),inference(split_conjunct,[status(thm)],[c70])).
% 0.45/0.62 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.45/0.62 fof(c59,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.45/0.62 fof(c60,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 0.45/0.62 fof(c61,plain,((![X31]:(~cpxcomp(X31)|(?[X32]:ra_Px1(X31,X32))))&(![X33]:((![X34]:~ra_Px1(X33,X34))|cpxcomp(X33)))),inference(variable_rename,[status(thm)],[c60])).
% 0.45/0.62 fof(c63,plain,(![X31]:(![X33]:(![X34]:((~cpxcomp(X31)|ra_Px1(X31,skolem0002(X31)))&(~ra_Px1(X33,X34)|cpxcomp(X33)))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X31]:(~cpxcomp(X31)|ra_Px1(X31,skolem0002(X31))))&(![X33]:((![X34]:~ra_Px1(X33,X34))|cpxcomp(X33)))),inference(skolemize,[status(esa)],[c61])).])).
% 0.45/0.62 cnf(c64,plain,~cpxcomp(X154)|ra_Px1(X154,skolem0002(X154)),inference(split_conjunct,[status(thm)],[c63])).
% 0.45/0.62 cnf(c79,plain,~cUnsatisfiable(X160)|rs(X160,skolem0004(X160)),inference(split_conjunct,[status(thm)],[c78])).
% 0.45/0.62 cnf(c176,plain,rs(i2003_11_14_17_21_12565,skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c79, c21])).
% 0.45/0.62 cnf(c81,plain,~cUnsatisfiable(X185)|~rs(X185,X184)|cpxcomp(X184),inference(split_conjunct,[status(thm)],[c78])).
% 0.45/0.62 cnf(c194,plain,~cUnsatisfiable(i2003_11_14_17_21_12565)|cpxcomp(skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c81, c176])).
% 0.45/0.62 cnf(c197,plain,cpxcomp(skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c194, c21])).
% 0.45/0.62 cnf(c198,plain,ra_Px1(skolem0004(i2003_11_14_17_21_12565),skolem0002(skolem0004(i2003_11_14_17_21_12565))),inference(resolution,[status(thm)],[c197, c64])).
% 0.45/0.62 cnf(c232,plain,~cp(skolem0004(i2003_11_14_17_21_12565)),inference(resolution,[status(thm)],[c198, c71])).
% 0.45/0.62 cnf(c238,plain,$false,inference(resolution,[status(thm)],[c232, c170])).
% 0.45/0.62 % SZS output end CNFRefutation
% 0.45/0.62
% 0.45/0.62 % Initial clauses : 69
% 0.45/0.62 % Processed clauses : 74
% 0.45/0.62 % Factors computed : 4
% 0.45/0.62 % Resolvents computed: 73
% 0.45/0.62 % Tautologies deleted: 11
% 0.45/0.62 % Forward subsumed : 18
% 0.45/0.62 % Backward subsumed : 1
% 0.45/0.62 % -------- CPU Time ---------
% 0.45/0.62 % User time : 0.248 s
% 0.45/0.62 % System time : 0.016 s
% 0.45/0.62 % Total time : 0.264 s
%------------------------------------------------------------------------------