%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ031+2 : TPTP v8.1.2. Released v4.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:37:39 EDT 2024
% Result : Theorem 0.53s 0.73s
% Output : Refutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : PUZ031+2 : TPTP v8.1.2. Released v4.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n013.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 : Wed May 8 20:39:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.53/0.73 % Version: 1.5
% 0.53/0.73 % SZS status Theorem
% 0.53/0.73 % SZS output start CNFRefutation
% 0.53/0.73 fof(wolf_type,axiom,(?[A]:wolf(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', wolf_type)).
% 0.53/0.73 fof(c82,plain,(?[X40]:wolf(X40)),inference(variable_rename,[status(thm)],[wolf_type])).
% 0.53/0.73 fof(c83,plain,wolf(skolem0008),inference(skolemize,[status(esa)],[c82])).
% 0.53/0.73 cnf(c84,plain,wolf(skolem0008),inference(split_conjunct,[status(thm)],[c83])).
% 0.53/0.73 fof(fox_type,axiom,(?[A]:fox(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fox_type)).
% 0.53/0.73 fof(c79,plain,(?[X39]:fox(X39)),inference(variable_rename,[status(thm)],[fox_type])).
% 0.53/0.73 fof(c80,plain,fox(skolem0007),inference(skolemize,[status(esa)],[c79])).
% 0.53/0.73 cnf(c81,plain,fox(skolem0007),inference(split_conjunct,[status(thm)],[c80])).
% 0.53/0.73 fof(pel47_11,axiom,(![X]:(![Y]:((wolf(X)&fox(Y))=>(~eats(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_11)).
% 0.53/0.73 fof(c29,plain,(![X]:(![Y]:((wolf(X)&fox(Y))=>~eats(X,Y)))),inference(fof_simplification,[status(thm)],[pel47_11])).
% 0.53/0.73 fof(c30,plain,(![X]:(![Y]:((~wolf(X)|~fox(Y))|~eats(X,Y)))),inference(fof_nnf,[status(thm)],[c29])).
% 0.53/0.73 fof(c31,plain,(![X15]:(![X16]:((~wolf(X15)|~fox(X16))|~eats(X15,X16)))),inference(variable_rename,[status(thm)],[c30])).
% 0.53/0.73 cnf(c32,plain,~wolf(X62)|~fox(X61)|~eats(X62,X61),inference(split_conjunct,[status(thm)],[c31])).
% 0.53/0.73 fof(grain_type,axiom,(?[A]:grain(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', grain_type)).
% 0.53/0.73 fof(c52,plain,(?[X30]:grain(X30)),inference(variable_rename,[status(thm)],[grain_type])).
% 0.53/0.73 fof(c53,plain,grain(skolem0003),inference(skolemize,[status(esa)],[c52])).
% 0.53/0.73 cnf(c54,plain,grain(skolem0003),inference(split_conjunct,[status(thm)],[c53])).
% 0.53/0.73 fof(pel47_11a,axiom,(![X]:(![Y]:((wolf(X)&grain(Y))=>(~eats(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_11a)).
% 0.53/0.73 fof(c25,plain,(![X]:(![Y]:((wolf(X)&grain(Y))=>~eats(X,Y)))),inference(fof_simplification,[status(thm)],[pel47_11a])).
% 0.53/0.73 fof(c26,plain,(![X]:(![Y]:((~wolf(X)|~grain(Y))|~eats(X,Y)))),inference(fof_nnf,[status(thm)],[c25])).
% 0.53/0.73 fof(c27,plain,(![X13]:(![X14]:((~wolf(X13)|~grain(X14))|~eats(X13,X14)))),inference(variable_rename,[status(thm)],[c26])).
% 0.53/0.73 cnf(c28,plain,~wolf(X59)|~grain(X58)|~eats(X59,X58),inference(split_conjunct,[status(thm)],[c27])).
% 0.53/0.73 fof(pel47_1_1,axiom,(![X]:(wolf(X)=>animal(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_1_1)).
% 0.53/0.73 fof(c67,plain,(![X]:(~wolf(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_1_1])).
% 0.53/0.73 fof(c68,plain,(![X35]:(~wolf(X35)|animal(X35))),inference(variable_rename,[status(thm)],[c67])).
% 0.53/0.73 cnf(c69,plain,~wolf(X51)|animal(X51),inference(split_conjunct,[status(thm)],[c68])).
% 0.53/0.73 cnf(c93,plain,animal(skolem0008),inference(resolution,[status(thm)],[c69, c84])).
% 0.53/0.73 fof(pel47_6_2,axiom,(![X]:(grain(X)=>plant(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_6_2)).
% 0.53/0.73 fof(c49,plain,(![X]:(~grain(X)|plant(X))),inference(fof_nnf,[status(thm)],[pel47_6_2])).
% 0.53/0.73 fof(c50,plain,(![X29]:(~grain(X29)|plant(X29))),inference(variable_rename,[status(thm)],[c49])).
% 0.53/0.73 cnf(c51,plain,~grain(X44)|plant(X44),inference(split_conjunct,[status(thm)],[c50])).
% 0.53/0.73 cnf(c86,plain,plant(skolem0003),inference(resolution,[status(thm)],[c51, c54])).
% 0.53/0.73 fof(pel47_2_1,axiom,(![X]:(fox(X)=>animal(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_2_1)).
% 0.53/0.73 fof(c64,plain,(![X]:(~fox(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_2_1])).
% 0.53/0.73 fof(c65,plain,(![X34]:(~fox(X34)|animal(X34))),inference(variable_rename,[status(thm)],[c64])).
% 0.53/0.73 cnf(c66,plain,~fox(X49)|animal(X49),inference(split_conjunct,[status(thm)],[c65])).
% 0.53/0.73 cnf(c91,plain,animal(skolem0007),inference(resolution,[status(thm)],[c66, c81])).
% 0.53/0.73 fof(pel47_10,axiom,(![X]:(![Y]:((fox(X)&wolf(Y))=>much_smaller(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_10)).
% 0.53/0.73 fof(c33,plain,(![X]:(![Y]:((~fox(X)|~wolf(Y))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_10])).
% 0.53/0.73 fof(c34,plain,(![X17]:(![X18]:((~fox(X17)|~wolf(X18))|much_smaller(X17,X18)))),inference(variable_rename,[status(thm)],[c33])).
% 0.53/0.73 cnf(c35,plain,~fox(X63)|~wolf(X64)|much_smaller(X63,X64),inference(split_conjunct,[status(thm)],[c34])).
% 0.53/0.73 cnf(c110,plain,~fox(X65)|much_smaller(X65,skolem0008),inference(resolution,[status(thm)],[c35, c84])).
% 0.53/0.73 cnf(c111,plain,much_smaller(skolem0007,skolem0008),inference(resolution,[status(thm)],[c110, c81])).
% 0.53/0.73 fof(pel47_7,axiom,(![X]:(animal(X)=>((![Y]:(plant(Y)=>eats(X,Y)))|(![Y1]:(((animal(Y1)&much_smaller(Y1,X))&(?[Z]:(plant(Z)&eats(Y1,Z))))=>eats(X,Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_7)).
% 0.53/0.73 fof(c45,plain,(![X]:(~animal(X)|((![Y]:(~plant(Y)|eats(X,Y)))|(![Y1]:(((~animal(Y1)|~much_smaller(Y1,X))|(![Z]:(~plant(Z)|~eats(Y1,Z))))|eats(X,Y1)))))),inference(fof_nnf,[status(thm)],[pel47_7])).
% 0.53/0.73 fof(c47,plain,(![X25]:(![X26]:(![X27]:(![X28]:(~animal(X25)|((~plant(X26)|eats(X25,X26))|(((~animal(X27)|~much_smaller(X27,X25))|(~plant(X28)|~eats(X27,X28)))|eats(X25,X27)))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,(![X25]:(~animal(X25)|((![X26]:(~plant(X26)|eats(X25,X26)))|(![X27]:(((~animal(X27)|~much_smaller(X27,X25))|(![X28]:(~plant(X28)|~eats(X27,X28))))|eats(X25,X27)))))),inference(variable_rename,[status(thm)],[c45])).])).
% 0.53/0.73 cnf(c48,plain,~animal(X77)|~plant(X78)|eats(X77,X78)|~animal(X76)|~much_smaller(X76,X77)|~plant(X75)|~eats(X76,X75)|eats(X77,X76),inference(split_conjunct,[status(thm)],[c47])).
% 0.53/0.73 fof(bird_type,axiom,(?[A]:bird(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', bird_type)).
% 0.53/0.73 fof(c76,plain,(?[X38]:bird(X38)),inference(variable_rename,[status(thm)],[bird_type])).
% 0.53/0.73 fof(c77,plain,bird(skolem0006),inference(skolemize,[status(esa)],[c76])).
% 0.53/0.73 cnf(c78,plain,bird(skolem0006),inference(split_conjunct,[status(thm)],[c77])).
% 0.53/0.73 fof(pel47_3_1,axiom,(![X]:(bird(X)=>animal(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_3_1)).
% 0.53/0.73 fof(c61,plain,(![X]:(~bird(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_3_1])).
% 0.53/0.73 fof(c62,plain,(![X33]:(~bird(X33)|animal(X33))),inference(variable_rename,[status(thm)],[c61])).
% 0.53/0.73 cnf(c63,plain,~bird(X48)|animal(X48),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.73 cnf(c90,plain,animal(skolem0006),inference(resolution,[status(thm)],[c63, c78])).
% 0.53/0.73 fof(snail_type,axiom,(?[A]:snail(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', snail_type)).
% 0.53/0.73 fof(c70,plain,(?[X36]:snail(X36)),inference(variable_rename,[status(thm)],[snail_type])).
% 0.53/0.73 fof(c71,plain,snail(skolem0004),inference(skolemize,[status(esa)],[c70])).
% 0.53/0.73 cnf(c72,plain,snail(skolem0004),inference(split_conjunct,[status(thm)],[c71])).
% 0.53/0.73 fof(pel47_13,axiom,(![X]:(![Y]:((bird(X)&snail(Y))=>(~eats(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_13)).
% 0.53/0.73 fof(c18,plain,(![X]:(![Y]:((bird(X)&snail(Y))=>~eats(X,Y)))),inference(fof_simplification,[status(thm)],[pel47_13])).
% 0.53/0.73 fof(c19,plain,(![X]:(![Y]:((~bird(X)|~snail(Y))|~eats(X,Y)))),inference(fof_nnf,[status(thm)],[c18])).
% 0.53/0.73 fof(c20,plain,(![X9]:(![X10]:((~bird(X9)|~snail(X10))|~eats(X9,X10)))),inference(variable_rename,[status(thm)],[c19])).
% 0.53/0.73 cnf(c21,plain,~bird(X54)|~snail(X55)|~eats(X54,X55),inference(split_conjunct,[status(thm)],[c20])).
% 0.53/0.73 fof(pel47_4_2,axiom,(![X]:(snail(X)=>animal(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_4_2)).
% 0.53/0.73 fof(c55,plain,(![X]:(~snail(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_4_2])).
% 0.53/0.73 fof(c56,plain,(![X31]:(~snail(X31)|animal(X31))),inference(variable_rename,[status(thm)],[c55])).
% 0.53/0.73 cnf(c57,plain,~snail(X45)|animal(X45),inference(split_conjunct,[status(thm)],[c56])).
% 0.53/0.73 cnf(c87,plain,animal(skolem0004),inference(resolution,[status(thm)],[c57, c72])).
% 0.53/0.73 fof(pel47_8,axiom,(![Y]:(![X]:((bird(Y)&snail(X))=>much_smaller(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_8)).
% 0.53/0.73 fof(c42,plain,(![Y]:(![X]:((~bird(Y)|~snail(X))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_8])).
% 0.53/0.73 fof(c43,plain,(![X23]:(![X24]:((~bird(X23)|~snail(X24))|much_smaller(X24,X23)))),inference(variable_rename,[status(thm)],[c42])).
% 0.53/0.73 cnf(c44,plain,~bird(X73)|~snail(X72)|much_smaller(X72,X73),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.73 cnf(c116,plain,~bird(X74)|much_smaller(skolem0004,X74),inference(resolution,[status(thm)],[c44, c72])).
% 0.53/0.73 cnf(c117,plain,much_smaller(skolem0004,skolem0006),inference(resolution,[status(thm)],[c116, c78])).
% 0.53/0.73 fof(pel47_14a,axiom,(![X]:(snail(X)=>(?[Y]:(plant(Y)&eats(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_14a)).
% 0.53/0.73 fof(c6,plain,(![X]:(~snail(X)|(?[Y]:(plant(Y)&eats(X,Y))))),inference(fof_nnf,[status(thm)],[pel47_14a])).
% 0.53/0.73 fof(c7,plain,(![X5]:(~snail(X5)|(?[X6]:(plant(X6)&eats(X5,X6))))),inference(variable_rename,[status(thm)],[c6])).
% 0.53/0.73 fof(c8,plain,(![X5]:(~snail(X5)|(plant(skolem0001(X5))&eats(X5,skolem0001(X5))))),inference(skolemize,[status(esa)],[c7])).
% 0.53/0.73 fof(c9,plain,(![X5]:((~snail(X5)|plant(skolem0001(X5)))&(~snail(X5)|eats(X5,skolem0001(X5))))),inference(distribute,[status(thm)],[c8])).
% 0.53/0.73 cnf(c10,plain,~snail(X46)|plant(skolem0001(X46)),inference(split_conjunct,[status(thm)],[c9])).
% 0.53/0.73 cnf(c88,plain,plant(skolem0001(skolem0004)),inference(resolution,[status(thm)],[c10, c72])).
% 0.53/0.73 cnf(c11,plain,~snail(X50)|eats(X50,skolem0001(X50)),inference(split_conjunct,[status(thm)],[c9])).
% 0.53/0.73 cnf(c92,plain,eats(skolem0004,skolem0001(skolem0004)),inference(resolution,[status(thm)],[c11, c72])).
% 0.53/0.73 cnf(c119,plain,~animal(X87)|~plant(X86)|eats(X87,X86)|~animal(skolem0004)|~much_smaller(skolem0004,X87)|~plant(skolem0001(skolem0004))|eats(X87,skolem0004),inference(resolution,[status(thm)],[c48, c92])).
% 0.53/0.73 cnf(c126,plain,~animal(X90)|~plant(X91)|eats(X90,X91)|~animal(skolem0004)|~much_smaller(skolem0004,X90)|eats(X90,skolem0004),inference(resolution,[status(thm)],[c119, c88])).
% 0.53/0.73 cnf(c129,plain,~animal(skolem0006)|~plant(X92)|eats(skolem0006,X92)|~animal(skolem0004)|eats(skolem0006,skolem0004),inference(resolution,[status(thm)],[c126, c117])).
% 0.53/0.73 cnf(c130,plain,~animal(skolem0006)|~plant(X93)|eats(skolem0006,X93)|eats(skolem0006,skolem0004),inference(resolution,[status(thm)],[c129, c87])).
% 0.53/0.73 cnf(c131,plain,~animal(skolem0006)|eats(skolem0006,skolem0003)|eats(skolem0006,skolem0004),inference(resolution,[status(thm)],[c130, c86])).
% 0.53/0.73 cnf(c134,plain,eats(skolem0006,skolem0003)|eats(skolem0006,skolem0004),inference(resolution,[status(thm)],[c131, c90])).
% 0.53/0.73 cnf(c140,plain,eats(skolem0006,skolem0003)|~bird(skolem0006)|~snail(skolem0004),inference(resolution,[status(thm)],[c134, c21])).
% 0.53/0.73 cnf(c146,plain,eats(skolem0006,skolem0003)|~bird(skolem0006),inference(resolution,[status(thm)],[c140, c72])).
% 0.53/0.73 cnf(c148,plain,eats(skolem0006,skolem0003),inference(resolution,[status(thm)],[c146, c78])).
% 0.53/0.73 fof(pel47,conjecture,(?[X]:(?[Y]:((animal(X)&animal(Y))&(?[Z]:((grain(Z)&eats(Y,Z))&eats(X,Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47)).
% 0.53/0.73 fof(c0,negated_conjecture,(~(?[X]:(?[Y]:((animal(X)&animal(Y))&(?[Z]:((grain(Z)&eats(Y,Z))&eats(X,Y))))))),inference(assume_negation,[status(cth)],[pel47])).
% 0.53/0.73 fof(c1,negated_conjecture,(![X]:(![Y]:((~animal(X)|~animal(Y))|(![Z]:((~grain(Z)|~eats(Y,Z))|~eats(X,Y)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.53/0.73 fof(c2,negated_conjecture,(![X]:(![Y]:((~animal(X)|~animal(Y))|((![Z]:(~grain(Z)|~eats(Y,Z)))|~eats(X,Y))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.53/0.73 fof(c4,negated_conjecture,(![X2]:(![X3]:(![X4]:((~animal(X2)|~animal(X3))|((~grain(X4)|~eats(X3,X4))|~eats(X2,X3)))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(![X2]:(![X3]:((~animal(X2)|~animal(X3))|((![X4]:(~grain(X4)|~eats(X3,X4)))|~eats(X2,X3))))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.53/0.73 cnf(c5,negated_conjecture,~animal(X41)|~animal(X42)|~grain(X43)|~eats(X42,X43)|~eats(X41,X42),inference(split_conjunct,[status(thm)],[c4])).
% 0.53/0.73 fof(pel47_9,axiom,(![X]:(![Y]:((bird(X)&fox(Y))=>much_smaller(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', pel47_9)).
% 0.53/0.73 fof(c36,plain,(![X]:(![Y]:((~bird(X)|~fox(Y))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_9])).
% 0.53/0.73 fof(c37,plain,(![X19]:(![X20]:((~bird(X19)|~fox(X20))|much_smaller(X19,X20)))),inference(variable_rename,[status(thm)],[c36])).
% 0.53/0.73 cnf(c38,plain,~bird(X67)|~fox(X66)|much_smaller(X67,X66),inference(split_conjunct,[status(thm)],[c37])).
% 0.53/0.73 cnf(c112,plain,~bird(X68)|much_smaller(X68,skolem0007),inference(resolution,[status(thm)],[c38, c81])).
% 0.53/0.73 cnf(c113,plain,much_smaller(skolem0006,skolem0007),inference(resolution,[status(thm)],[c112, c78])).
% 0.53/0.73 cnf(c151,plain,~animal(X112)|~plant(X111)|eats(X112,X111)|~animal(skolem0006)|~much_smaller(skolem0006,X112)|~plant(skolem0003)|eats(X112,skolem0006),inference(resolution,[status(thm)],[c148, c48])).
% 0.53/0.73 cnf(c193,plain,~animal(skolem0007)|~plant(X114)|eats(skolem0007,X114)|~animal(skolem0006)|~plant(skolem0003)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c151, c113])).
% 0.53/0.73 cnf(c195,plain,~animal(skolem0007)|~plant(X115)|eats(skolem0007,X115)|~animal(skolem0006)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c193, c86])).
% 0.53/0.73 cnf(c196,plain,~animal(skolem0007)|~plant(X116)|eats(skolem0007,X116)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c195, c90])).
% 0.53/0.73 cnf(c197,plain,~animal(skolem0007)|eats(skolem0007,skolem0003)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c196, c86])).
% 0.53/0.73 cnf(c200,plain,eats(skolem0007,skolem0003)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c197, c91])).
% 0.53/0.73 cnf(c212,plain,eats(skolem0007,skolem0003)|~animal(skolem0007)|~animal(skolem0006)|~grain(X129)|~eats(skolem0006,X129),inference(resolution,[status(thm)],[c200, c5])).
% 0.53/0.73 cnf(c242,plain,eats(skolem0007,skolem0003)|~animal(skolem0007)|~animal(skolem0006)|~grain(skolem0003),inference(resolution,[status(thm)],[c212, c148])).
% 0.53/0.73 cnf(c244,plain,eats(skolem0007,skolem0003)|~animal(skolem0007)|~animal(skolem0006),inference(resolution,[status(thm)],[c242, c54])).
% 0.53/0.73 cnf(c245,plain,eats(skolem0007,skolem0003)|~animal(skolem0007),inference(resolution,[status(thm)],[c244, c90])).
% 0.53/0.73 cnf(c246,plain,eats(skolem0007,skolem0003),inference(resolution,[status(thm)],[c245, c91])).
% 0.53/0.73 cnf(c251,plain,~animal(X154)|~plant(X153)|eats(X154,X153)|~animal(skolem0007)|~much_smaller(skolem0007,X154)|~plant(skolem0003)|eats(X154,skolem0007),inference(resolution,[status(thm)],[c246, c48])).
% 0.53/0.73 cnf(c285,plain,~animal(skolem0008)|~plant(X155)|eats(skolem0008,X155)|~animal(skolem0007)|~plant(skolem0003)|eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c251, c111])).
% 0.53/0.73 cnf(c287,plain,~animal(skolem0008)|~plant(X156)|eats(skolem0008,X156)|~animal(skolem0007)|eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c285, c86])).
% 0.53/0.73 cnf(c288,plain,~animal(skolem0008)|~plant(X157)|eats(skolem0008,X157)|eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c287, c91])).
% 0.53/0.73 cnf(c289,plain,~animal(skolem0008)|eats(skolem0008,skolem0003)|eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c288, c86])).
% 0.53/0.73 cnf(c292,plain,eats(skolem0008,skolem0003)|eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c289, c93])).
% 0.53/0.73 cnf(c294,plain,eats(skolem0008,skolem0007)|~wolf(skolem0008)|~grain(skolem0003),inference(resolution,[status(thm)],[c292, c28])).
% 0.53/0.73 cnf(c303,plain,eats(skolem0008,skolem0007)|~wolf(skolem0008),inference(resolution,[status(thm)],[c294, c54])).
% 0.53/0.73 cnf(c304,plain,eats(skolem0008,skolem0007),inference(resolution,[status(thm)],[c303, c84])).
% 0.53/0.73 cnf(c308,plain,~wolf(skolem0008)|~fox(skolem0007),inference(resolution,[status(thm)],[c304, c32])).
% 0.53/0.73 cnf(c310,plain,~wolf(skolem0008),inference(resolution,[status(thm)],[c308, c81])).
% 0.53/0.73 cnf(c311,plain,$false,inference(resolution,[status(thm)],[c310, c84])).
% 0.53/0.73 % SZS output end CNFRefutation
% 0.53/0.73
% 0.53/0.73 % Initial clauses : 26
% 0.53/0.73 % Processed clauses : 174
% 0.53/0.73 % Factors computed : 11
% 0.53/0.73 % Resolvents computed: 216
% 0.53/0.73 % Tautologies deleted: 0
% 0.53/0.73 % Forward subsumed : 54
% 0.53/0.73 % Backward subsumed : 86
% 0.53/0.73 % -------- CPU Time ---------
% 0.53/0.73 % User time : 0.360 s
% 0.53/0.73 % System time : 0.017 s
% 0.53/0.73 % Total time : 0.377 s
%------------------------------------------------------------------------------