%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS124+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:46 EDT 2024
% Result : Unsatisfiable 0.22s 0.61s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS124+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n013.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:07:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.22/0.61 % Version: 1.5
% 0.22/0.61 % SZS status Unsatisfiable
% 0.22/0.61 % SZS output start CNFRefutation
% 0.22/0.61 fof(axiom_12,axiom,(![X]:(ca_Ax3(X)<=>(cd(X)&cc(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.22/0.61 fof(c1,plain,(![X]:((~ca_Ax3(X)|(cd(X)&cc(X)))&((~cd(X)|~cc(X))|ca_Ax3(X)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 0.22/0.61 fof(c2,plain,((![X]:(~ca_Ax3(X)|(cd(X)&cc(X))))&(![X]:((~cd(X)|~cc(X))|ca_Ax3(X)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.22/0.61 fof(c4,plain,(![X2]:(![X3]:((~ca_Ax3(X2)|(cd(X2)&cc(X2)))&((~cd(X3)|~cc(X3))|ca_Ax3(X3))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~ca_Ax3(X2)|(cd(X2)&cc(X2))))&(![X3]:((~cd(X3)|~cc(X3))|ca_Ax3(X3)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.22/0.61 fof(c5,plain,(![X2]:(![X3]:(((~ca_Ax3(X2)|cd(X2))&(~ca_Ax3(X2)|cc(X2)))&((~cd(X3)|~cc(X3))|ca_Ax3(X3))))),inference(distribute,[status(thm)],[c4])).
% 0.22/0.61 cnf(c6,plain,~ca_Ax3(X37)|cd(X37),inference(split_conjunct,[status(thm)],[c5])).
% 0.22/0.61 fof(axiom_13,axiom,cUnsatisfiable(i2003_11_14_17_22_10903),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_13)).
% 0.22/0.61 cnf(c0,plain,cUnsatisfiable(i2003_11_14_17_22_10903),inference(split_conjunct,[status(thm)],[axiom_13])).
% 0.22/0.61 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rr(X,Y)&cowlThing(Y)))&(![Y]:(rr(X,Y)=>ca_Ax3(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.22/0.61 fof(c52,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&cowlThing(Y)))&(![Y]:(~rr(X,Y)|ca_Ax3(Y)))))&(((![Y]:(~rr(X,Y)|~cowlThing(Y)))|(?[Y]:(rr(X,Y)&~ca_Ax3(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.22/0.61 fof(c53,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&cowlThing(Y)))&(![Y]:(~rr(X,Y)|ca_Ax3(Y))))))&(![X]:(((![Y]:(~rr(X,Y)|~cowlThing(Y)))|(?[Y]:(rr(X,Y)&~ca_Ax3(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c52])).
% 0.22/0.61 fof(c54,plain,((![X25]:(~cUnsatisfiable(X25)|((?[X26]:(rr(X25,X26)&cowlThing(X26)))&(![X27]:(~rr(X25,X27)|ca_Ax3(X27))))))&(![X28]:(((![X29]:(~rr(X28,X29)|~cowlThing(X29)))|(?[X30]:(rr(X28,X30)&~ca_Ax3(X30))))|cUnsatisfiable(X28)))),inference(variable_rename,[status(thm)],[c53])).
% 0.22/0.61 fof(c56,plain,(![X25]:(![X27]:(![X28]:(![X29]:((~cUnsatisfiable(X25)|((rr(X25,skolem0005(X25))&cowlThing(skolem0005(X25)))&(~rr(X25,X27)|ca_Ax3(X27))))&(((~rr(X28,X29)|~cowlThing(X29))|(rr(X28,skolem0006(X28))&~ca_Ax3(skolem0006(X28))))|cUnsatisfiable(X28))))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X25]:(~cUnsatisfiable(X25)|((rr(X25,skolem0005(X25))&cowlThing(skolem0005(X25)))&(![X27]:(~rr(X25,X27)|ca_Ax3(X27))))))&(![X28]:(((![X29]:(~rr(X28,X29)|~cowlThing(X29)))|(rr(X28,skolem0006(X28))&~ca_Ax3(skolem0006(X28))))|cUnsatisfiable(X28)))),inference(skolemize,[status(esa)],[c54])).])).
% 0.22/0.61 fof(c57,plain,(![X25]:(![X27]:(![X28]:(![X29]:((((~cUnsatisfiable(X25)|rr(X25,skolem0005(X25)))&(~cUnsatisfiable(X25)|cowlThing(skolem0005(X25))))&(~cUnsatisfiable(X25)|(~rr(X25,X27)|ca_Ax3(X27))))&((((~rr(X28,X29)|~cowlThing(X29))|rr(X28,skolem0006(X28)))|cUnsatisfiable(X28))&(((~rr(X28,X29)|~cowlThing(X29))|~ca_Ax3(skolem0006(X28)))|cUnsatisfiable(X28)))))))),inference(distribute,[status(thm)],[c56])).
% 0.22/0.61 cnf(c58,plain,~cUnsatisfiable(X65)|rr(X65,skolem0005(X65)),inference(split_conjunct,[status(thm)],[c57])).
% 0.22/0.61 cnf(c83,plain,rr(i2003_11_14_17_22_10903,skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c58, c0])).
% 0.22/0.61 cnf(c60,plain,~cUnsatisfiable(X66)|~rr(X66,X67)|ca_Ax3(X67),inference(split_conjunct,[status(thm)],[c57])).
% 0.22/0.61 cnf(c84,plain,~cUnsatisfiable(i2003_11_14_17_22_10903)|ca_Ax3(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c60, c83])).
% 0.22/0.61 cnf(c90,plain,ca_Ax3(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c84, c0])).
% 0.22/0.61 cnf(c92,plain,cd(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c90, c6])).
% 0.22/0.61 fof(axiom_6,axiom,(![X]:(cd(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.22/0.61 fof(c36,plain,(![X]:((~cd(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.22/0.61 fof(c37,plain,((![X]:(~cd(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cd(X)))),inference(shift_quantors,[status(thm)],[c36])).
% 0.22/0.61 fof(c38,plain,((![X18]:(~cd(X18)|(![X19]:~ra_Px1(X18,X19))))&(![X20]:((?[X21]:ra_Px1(X20,X21))|cd(X20)))),inference(variable_rename,[status(thm)],[c37])).
% 0.22/0.61 fof(c40,plain,(![X18]:(![X19]:(![X20]:((~cd(X18)|~ra_Px1(X18,X19))&(ra_Px1(X20,skolem0004(X20))|cd(X20)))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,((![X18]:(~cd(X18)|(![X19]:~ra_Px1(X18,X19))))&(![X20]:(ra_Px1(X20,skolem0004(X20))|cd(X20)))),inference(skolemize,[status(esa)],[c38])).])).
% 0.22/0.61 cnf(c41,plain,~cd(X57)|~ra_Px1(X57,X58),inference(split_conjunct,[status(thm)],[c40])).
% 0.22/0.61 fof(axiom_7,axiom,(![X]:(cdxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.22/0.61 fof(c29,plain,(![X]:((~cdxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cdxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.22/0.61 fof(c30,plain,((![X]:(~cdxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cdxcomp(X)))),inference(shift_quantors,[status(thm)],[c29])).
% 0.22/0.61 fof(c31,plain,((![X14]:(~cdxcomp(X14)|(?[X15]:ra_Px1(X14,X15))))&(![X16]:((![X17]:~ra_Px1(X16,X17))|cdxcomp(X16)))),inference(variable_rename,[status(thm)],[c30])).
% 0.22/0.61 fof(c33,plain,(![X14]:(![X16]:(![X17]:((~cdxcomp(X14)|ra_Px1(X14,skolem0003(X14)))&(~ra_Px1(X16,X17)|cdxcomp(X16)))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X14]:(~cdxcomp(X14)|ra_Px1(X14,skolem0003(X14))))&(![X16]:((![X17]:~ra_Px1(X16,X17))|cdxcomp(X16)))),inference(skolemize,[status(esa)],[c31])).])).
% 0.22/0.61 cnf(c34,plain,~cdxcomp(X61)|ra_Px1(X61,skolem0003(X61)),inference(split_conjunct,[status(thm)],[c33])).
% 0.22/0.61 fof(axiom_3,axiom,(![X]:(cc(X)=>cdxcomp(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.22/0.61 fof(c49,plain,(![X]:(~cc(X)|cdxcomp(X))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.22/0.61 fof(c50,plain,(![X24]:(~cc(X24)|cdxcomp(X24))),inference(variable_rename,[status(thm)],[c49])).
% 0.22/0.61 cnf(c51,plain,~cc(X44)|cdxcomp(X44),inference(split_conjunct,[status(thm)],[c50])).
% 0.22/0.61 cnf(c7,plain,~ca_Ax3(X38)|cc(X38),inference(split_conjunct,[status(thm)],[c5])).
% 0.22/0.61 cnf(c91,plain,cc(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c90, c7])).
% 0.22/0.61 cnf(c94,plain,cdxcomp(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c91, c51])).
% 0.22/0.61 cnf(c95,plain,ra_Px1(skolem0005(i2003_11_14_17_22_10903),skolem0003(skolem0005(i2003_11_14_17_22_10903))),inference(resolution,[status(thm)],[c94, c34])).
% 0.22/0.61 cnf(c97,plain,~cd(skolem0005(i2003_11_14_17_22_10903)),inference(resolution,[status(thm)],[c95, c41])).
% 0.22/0.61 cnf(c98,plain,$false,inference(resolution,[status(thm)],[c97, c92])).
% 0.22/0.61 % SZS output end CNFRefutation
% 0.22/0.61
% 0.22/0.61 % Initial clauses : 26
% 0.22/0.61 % Processed clauses : 37
% 0.22/0.61 % Factors computed : 0
% 0.22/0.61 % Resolvents computed: 26
% 0.22/0.61 % Tautologies deleted: 5
% 0.22/0.61 % Forward subsumed : 6
% 0.22/0.61 % Backward subsumed : 1
% 0.22/0.61 % -------- CPU Time ---------
% 0.22/0.61 % User time : 0.233 s
% 0.22/0.61 % System time : 0.015 s
% 0.22/0.61 % Total time : 0.248 s
%------------------------------------------------------------------------------