%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ031+1 : TPTP v8.1.2. Released v2.0.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:37:39 EDT 2024
% Result : Theorem 0.54s 0.75s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PUZ031+1 : TPTP v8.1.2. Released v2.0.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 20:41:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.54/0.75 % Version: 1.5
% 0.54/0.75 % SZS status Theorem
% 0.54/0.75 % SZS output start CNFRefutation
% 0.54/0.75 fof(pel47_1_2,axiom,(?[X1]:wolf(X1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_1_2)).
% 0.54/0.75 fof(c72,plain,(?[X33]:wolf(X33)),inference(variable_rename,[status(thm)],[pel47_1_2])).
% 0.54/0.75 fof(c73,plain,wolf(skolem0007),inference(skolemize,[status(esa)],[c72])).
% 0.54/0.75 cnf(c74,plain,wolf(skolem0007),inference(split_conjunct,[status(thm)],[c73])).
% 0.54/0.75 fof(pel47_2_2,axiom,(?[X1]:fox(X1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_2_2)).
% 0.54/0.75 fof(c66,plain,(?[X31]:fox(X31)),inference(variable_rename,[status(thm)],[pel47_2_2])).
% 0.54/0.75 fof(c67,plain,fox(skolem0006),inference(skolemize,[status(esa)],[c66])).
% 0.54/0.75 cnf(c68,plain,fox(skolem0006),inference(split_conjunct,[status(thm)],[c67])).
% 0.54/0.75 fof(pel47_11,axiom,(![X]:(![Y]:((wolf(X)&(fox(Y)|grain(Y)))=>(~eats(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_11)).
% 0.54/0.75 fof(c21,plain,(![X]:(![Y]:((wolf(X)&(fox(Y)|grain(Y)))=>~eats(X,Y)))),inference(fof_simplification,[status(thm)],[pel47_11])).
% 0.54/0.75 fof(c22,plain,(![X]:(![Y]:((~wolf(X)|(~fox(Y)&~grain(Y)))|~eats(X,Y)))),inference(fof_nnf,[status(thm)],[c21])).
% 0.54/0.75 fof(c23,plain,(![X11]:(![X12]:((~wolf(X11)|(~fox(X12)&~grain(X12)))|~eats(X11,X12)))),inference(variable_rename,[status(thm)],[c22])).
% 0.54/0.75 fof(c24,plain,(![X11]:(![X12]:(((~wolf(X11)|~fox(X12))|~eats(X11,X12))&((~wolf(X11)|~grain(X12))|~eats(X11,X12))))),inference(distribute,[status(thm)],[c23])).
% 0.54/0.75 cnf(c25,plain,~wolf(X53)|~fox(X52)|~eats(X53,X52),inference(split_conjunct,[status(thm)],[c24])).
% 0.54/0.75 fof(pel47_6_1,axiom,(?[X]:grain(X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_6_1)).
% 0.54/0.75 fof(c45,plain,(?[X24]:grain(X24)),inference(variable_rename,[status(thm)],[pel47_6_1])).
% 0.54/0.75 fof(c46,plain,grain(skolem0002),inference(skolemize,[status(esa)],[c45])).
% 0.54/0.75 cnf(c47,plain,grain(skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.54/0.75 cnf(c26,plain,~wolf(X56)|~grain(X55)|~eats(X56,X55),inference(split_conjunct,[status(thm)],[c24])).
% 0.54/0.75 fof(pel47_1_1,axiom,(![X]:(wolf(X)=>animal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_1_1)).
% 0.54/0.75 fof(c75,plain,(![X]:(~wolf(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_1_1])).
% 0.54/0.75 fof(c76,plain,(![X34]:(~wolf(X34)|animal(X34))),inference(variable_rename,[status(thm)],[c75])).
% 0.54/0.75 cnf(c77,plain,~wolf(X45)|animal(X45),inference(split_conjunct,[status(thm)],[c76])).
% 0.54/0.75 cnf(c86,plain,animal(skolem0007),inference(resolution,[status(thm)],[c77, c74])).
% 0.54/0.75 fof(pel47_6_2,axiom,(![X1]:(grain(X1)=>plant(X1))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_6_2)).
% 0.54/0.75 fof(c42,plain,(![X1]:(~grain(X1)|plant(X1))),inference(fof_nnf,[status(thm)],[pel47_6_2])).
% 0.54/0.75 fof(c43,plain,(![X23]:(~grain(X23)|plant(X23))),inference(variable_rename,[status(thm)],[c42])).
% 0.54/0.75 cnf(c44,plain,~grain(X38)|plant(X38),inference(split_conjunct,[status(thm)],[c43])).
% 0.54/0.75 cnf(c79,plain,plant(skolem0002),inference(resolution,[status(thm)],[c44, c47])).
% 0.54/0.75 fof(pel47_2_1,axiom,(![X]:(fox(X)=>animal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_2_1)).
% 0.54/0.75 fof(c69,plain,(![X]:(~fox(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_2_1])).
% 0.54/0.75 fof(c70,plain,(![X32]:(~fox(X32)|animal(X32))),inference(variable_rename,[status(thm)],[c69])).
% 0.54/0.75 cnf(c71,plain,~fox(X43)|animal(X43),inference(split_conjunct,[status(thm)],[c70])).
% 0.54/0.75 cnf(c84,plain,animal(skolem0006),inference(resolution,[status(thm)],[c71, c68])).
% 0.54/0.75 fof(pel47_10,axiom,(![X]:(![Y]:((fox(X)&wolf(Y))=>much_smaller(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_10)).
% 0.54/0.75 fof(c27,plain,(![X]:(![Y]:((~fox(X)|~wolf(Y))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_10])).
% 0.54/0.75 fof(c28,plain,(![X13]:(![X14]:((~fox(X13)|~wolf(X14))|much_smaller(X13,X14)))),inference(variable_rename,[status(thm)],[c27])).
% 0.54/0.75 cnf(c29,plain,~fox(X57)|~wolf(X58)|much_smaller(X57,X58),inference(split_conjunct,[status(thm)],[c28])).
% 0.54/0.75 cnf(c103,plain,~fox(X59)|much_smaller(X59,skolem0007),inference(resolution,[status(thm)],[c29, c74])).
% 0.54/0.75 cnf(c104,plain,much_smaller(skolem0006,skolem0007),inference(resolution,[status(thm)],[c103, c68])).
% 0.54/0.75 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/sandbox/benchmark/theBenchmark.p', pel47_7)).
% 0.54/0.75 fof(c38,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.54/0.75 fof(c40,plain,(![X19]:(![X20]:(![X21]:(![X22]:(~animal(X19)|((~plant(X20)|eats(X19,X20))|(((~animal(X21)|~much_smaller(X21,X19))|(~plant(X22)|~eats(X21,X22)))|eats(X19,X21)))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X19]:(~animal(X19)|((![X20]:(~plant(X20)|eats(X19,X20)))|(![X21]:(((~animal(X21)|~much_smaller(X21,X19))|(![X22]:(~plant(X22)|~eats(X21,X22))))|eats(X19,X21)))))),inference(variable_rename,[status(thm)],[c38])).])).
% 0.54/0.75 cnf(c41,plain,~animal(X69)|~plant(X72)|eats(X69,X72)|~animal(X71)|~much_smaller(X71,X69)|~plant(X70)|~eats(X71,X70)|eats(X69,X71),inference(split_conjunct,[status(thm)],[c40])).
% 0.54/0.75 fof(pel47_3_2,axiom,(?[X1]:bird(X1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_3_2)).
% 0.54/0.75 fof(c60,plain,(?[X29]:bird(X29)),inference(variable_rename,[status(thm)],[pel47_3_2])).
% 0.54/0.75 fof(c61,plain,bird(skolem0005),inference(skolemize,[status(esa)],[c60])).
% 0.54/0.75 cnf(c62,plain,bird(skolem0005),inference(split_conjunct,[status(thm)],[c61])).
% 0.54/0.75 fof(pel47_3_1,axiom,(![X]:(bird(X)=>animal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_3_1)).
% 0.54/0.75 fof(c63,plain,(![X]:(~bird(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_3_1])).
% 0.54/0.75 fof(c64,plain,(![X30]:(~bird(X30)|animal(X30))),inference(variable_rename,[status(thm)],[c63])).
% 0.54/0.75 cnf(c65,plain,~bird(X42)|animal(X42),inference(split_conjunct,[status(thm)],[c64])).
% 0.54/0.75 cnf(c83,plain,animal(skolem0005),inference(resolution,[status(thm)],[c65, c62])).
% 0.54/0.75 fof(pel47_5_2,axiom,(?[X1]:snail(X1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_5_2)).
% 0.54/0.75 fof(c48,plain,(?[X25]:snail(X25)),inference(variable_rename,[status(thm)],[pel47_5_2])).
% 0.54/0.75 fof(c49,plain,snail(skolem0003),inference(skolemize,[status(esa)],[c48])).
% 0.54/0.75 cnf(c50,plain,snail(skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 0.54/0.75 fof(pel47_13,axiom,(![X]:(![Y]:((bird(X)&snail(Y))=>(~eats(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_13)).
% 0.54/0.75 fof(c14,plain,(![X]:(![Y]:((bird(X)&snail(Y))=>~eats(X,Y)))),inference(fof_simplification,[status(thm)],[pel47_13])).
% 0.54/0.75 fof(c15,plain,(![X]:(![Y]:((~bird(X)|~snail(Y))|~eats(X,Y)))),inference(fof_nnf,[status(thm)],[c14])).
% 0.54/0.75 fof(c16,plain,(![X7]:(![X8]:((~bird(X7)|~snail(X8))|~eats(X7,X8)))),inference(variable_rename,[status(thm)],[c15])).
% 0.54/0.75 cnf(c17,plain,~bird(X49)|~snail(X48)|~eats(X49,X48),inference(split_conjunct,[status(thm)],[c16])).
% 0.54/0.75 fof(pel47_5_1,axiom,(![X]:(snail(X)=>animal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_5_1)).
% 0.54/0.75 fof(c51,plain,(![X]:(~snail(X)|animal(X))),inference(fof_nnf,[status(thm)],[pel47_5_1])).
% 0.54/0.75 fof(c52,plain,(![X26]:(~snail(X26)|animal(X26))),inference(variable_rename,[status(thm)],[c51])).
% 0.54/0.75 cnf(c53,plain,~snail(X39)|animal(X39),inference(split_conjunct,[status(thm)],[c52])).
% 0.54/0.75 cnf(c80,plain,animal(skolem0003),inference(resolution,[status(thm)],[c53, c50])).
% 0.54/0.75 fof(pel47_8,axiom,(![X]:(![Y]:((bird(Y)&(snail(X)|caterpillar(X)))=>much_smaller(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_8)).
% 0.54/0.75 fof(c33,plain,(![X]:(![Y]:((~bird(Y)|(~snail(X)&~caterpillar(X)))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_8])).
% 0.54/0.75 fof(c34,plain,(![X17]:(![X18]:((~bird(X18)|(~snail(X17)&~caterpillar(X17)))|much_smaller(X17,X18)))),inference(variable_rename,[status(thm)],[c33])).
% 0.54/0.75 fof(c35,plain,(![X17]:(![X18]:(((~bird(X18)|~snail(X17))|much_smaller(X17,X18))&((~bird(X18)|~caterpillar(X17))|much_smaller(X17,X18))))),inference(distribute,[status(thm)],[c34])).
% 0.54/0.75 cnf(c36,plain,~bird(X64)|~snail(X63)|much_smaller(X63,X64),inference(split_conjunct,[status(thm)],[c35])).
% 0.54/0.75 cnf(c107,plain,~bird(X65)|much_smaller(skolem0003,X65),inference(resolution,[status(thm)],[c36, c50])).
% 0.54/0.75 cnf(c108,plain,much_smaller(skolem0003,skolem0005),inference(resolution,[status(thm)],[c107, c62])).
% 0.54/0.75 fof(pel47_14,axiom,(![X]:((caterpillar(X)|snail(X))=>(?[Y]:(plant(Y)&eats(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_14)).
% 0.54/0.75 fof(c6,plain,(![X]:((~caterpillar(X)&~snail(X))|(?[Y]:(plant(Y)&eats(X,Y))))),inference(fof_nnf,[status(thm)],[pel47_14])).
% 0.54/0.75 fof(c7,plain,(![X5]:((~caterpillar(X5)&~snail(X5))|(?[X6]:(plant(X6)&eats(X5,X6))))),inference(variable_rename,[status(thm)],[c6])).
% 0.54/0.75 fof(c8,plain,(![X5]:((~caterpillar(X5)&~snail(X5))|(plant(skolem0001(X5))&eats(X5,skolem0001(X5))))),inference(skolemize,[status(esa)],[c7])).
% 0.54/0.75 fof(c9,plain,(![X5]:(((~caterpillar(X5)|plant(skolem0001(X5)))&(~caterpillar(X5)|eats(X5,skolem0001(X5))))&((~snail(X5)|plant(skolem0001(X5)))&(~snail(X5)|eats(X5,skolem0001(X5)))))),inference(distribute,[status(thm)],[c8])).
% 0.54/0.75 cnf(c12,plain,~snail(X46)|plant(skolem0001(X46)),inference(split_conjunct,[status(thm)],[c9])).
% 0.54/0.75 cnf(c87,plain,plant(skolem0001(skolem0003)),inference(resolution,[status(thm)],[c12, c50])).
% 0.54/0.75 cnf(c13,plain,~snail(X47)|eats(X47,skolem0001(X47)),inference(split_conjunct,[status(thm)],[c9])).
% 0.54/0.75 cnf(c88,plain,eats(skolem0003,skolem0001(skolem0003)),inference(resolution,[status(thm)],[c13, c50])).
% 0.54/0.75 cnf(c113,plain,~animal(X82)|~plant(X83)|eats(X82,X83)|~animal(skolem0003)|~much_smaller(skolem0003,X82)|~plant(skolem0001(skolem0003))|eats(X82,skolem0003),inference(resolution,[status(thm)],[c41, c88])).
% 0.54/0.75 cnf(c121,plain,~animal(X88)|~plant(X87)|eats(X88,X87)|~animal(skolem0003)|~much_smaller(skolem0003,X88)|eats(X88,skolem0003),inference(resolution,[status(thm)],[c113, c87])).
% 0.54/0.75 cnf(c123,plain,~animal(skolem0005)|~plant(X89)|eats(skolem0005,X89)|~animal(skolem0003)|eats(skolem0005,skolem0003),inference(resolution,[status(thm)],[c121, c108])).
% 0.54/0.75 cnf(c124,plain,~animal(skolem0005)|~plant(X90)|eats(skolem0005,X90)|eats(skolem0005,skolem0003),inference(resolution,[status(thm)],[c123, c80])).
% 0.54/0.75 cnf(c125,plain,~animal(skolem0005)|eats(skolem0005,skolem0002)|eats(skolem0005,skolem0003),inference(resolution,[status(thm)],[c124, c79])).
% 0.54/0.75 cnf(c128,plain,eats(skolem0005,skolem0002)|eats(skolem0005,skolem0003),inference(resolution,[status(thm)],[c125, c83])).
% 0.54/0.75 cnf(c135,plain,eats(skolem0005,skolem0002)|~bird(skolem0005)|~snail(skolem0003),inference(resolution,[status(thm)],[c128, c17])).
% 0.54/0.75 cnf(c140,plain,eats(skolem0005,skolem0002)|~bird(skolem0005),inference(resolution,[status(thm)],[c135, c50])).
% 0.54/0.75 cnf(c141,plain,eats(skolem0005,skolem0002),inference(resolution,[status(thm)],[c140, c62])).
% 0.54/0.75 fof(pel47,conjecture,(?[X]:(?[Y]:((animal(X)&animal(Y))&(?[Z]:((grain(Z)&eats(Y,Z))&eats(X,Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47)).
% 0.54/0.75 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.54/0.75 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.54/0.75 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.54/0.75 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.54/0.75 cnf(c5,negated_conjecture,~animal(X36)|~animal(X37)|~grain(X35)|~eats(X37,X35)|~eats(X36,X37),inference(split_conjunct,[status(thm)],[c4])).
% 0.54/0.75 fof(pel47_9,axiom,(![X]:(![Y]:((bird(X)&fox(Y))=>much_smaller(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel47_9)).
% 0.54/0.75 fof(c30,plain,(![X]:(![Y]:((~bird(X)|~fox(Y))|much_smaller(X,Y)))),inference(fof_nnf,[status(thm)],[pel47_9])).
% 0.54/0.75 fof(c31,plain,(![X15]:(![X16]:((~bird(X15)|~fox(X16))|much_smaller(X15,X16)))),inference(variable_rename,[status(thm)],[c30])).
% 0.54/0.75 cnf(c32,plain,~bird(X60)|~fox(X61)|much_smaller(X60,X61),inference(split_conjunct,[status(thm)],[c31])).
% 0.54/0.75 cnf(c105,plain,~bird(X62)|much_smaller(X62,skolem0006),inference(resolution,[status(thm)],[c32, c68])).
% 0.54/0.75 cnf(c106,plain,much_smaller(skolem0005,skolem0006),inference(resolution,[status(thm)],[c105, c62])).
% 0.54/0.75 cnf(c142,plain,~animal(X100)|~plant(X101)|eats(X100,X101)|~animal(skolem0005)|~much_smaller(skolem0005,X100)|~plant(skolem0002)|eats(X100,skolem0005),inference(resolution,[status(thm)],[c141, c41])).
% 0.54/0.75 cnf(c185,plain,~animal(skolem0006)|~plant(X110)|eats(skolem0006,X110)|~animal(skolem0005)|~plant(skolem0002)|eats(skolem0006,skolem0005),inference(resolution,[status(thm)],[c142, c106])).
% 0.54/0.75 cnf(c189,plain,~animal(skolem0006)|~plant(X111)|eats(skolem0006,X111)|~animal(skolem0005)|eats(skolem0006,skolem0005),inference(resolution,[status(thm)],[c185, c79])).
% 0.54/0.75 cnf(c190,plain,~animal(skolem0006)|~plant(X112)|eats(skolem0006,X112)|eats(skolem0006,skolem0005),inference(resolution,[status(thm)],[c189, c83])).
% 0.54/0.75 cnf(c191,plain,~animal(skolem0006)|eats(skolem0006,skolem0002)|eats(skolem0006,skolem0005),inference(resolution,[status(thm)],[c190, c79])).
% 0.54/0.75 cnf(c194,plain,eats(skolem0006,skolem0002)|eats(skolem0006,skolem0005),inference(resolution,[status(thm)],[c191, c84])).
% 0.54/0.75 cnf(c202,plain,eats(skolem0006,skolem0002)|~animal(skolem0006)|~animal(skolem0005)|~grain(X125)|~eats(skolem0005,X125),inference(resolution,[status(thm)],[c194, c5])).
% 0.54/0.75 cnf(c237,plain,eats(skolem0006,skolem0002)|~animal(skolem0006)|~animal(skolem0005)|~grain(skolem0002),inference(resolution,[status(thm)],[c202, c141])).
% 0.54/0.75 cnf(c238,plain,eats(skolem0006,skolem0002)|~animal(skolem0006)|~animal(skolem0005),inference(resolution,[status(thm)],[c237, c47])).
% 0.54/0.75 cnf(c239,plain,eats(skolem0006,skolem0002)|~animal(skolem0006),inference(resolution,[status(thm)],[c238, c83])).
% 0.54/0.75 cnf(c240,plain,eats(skolem0006,skolem0002),inference(resolution,[status(thm)],[c239, c84])).
% 0.54/0.75 cnf(c242,plain,~animal(X150)|~plant(X151)|eats(X150,X151)|~animal(skolem0006)|~much_smaller(skolem0006,X150)|~plant(skolem0002)|eats(X150,skolem0006),inference(resolution,[status(thm)],[c240, c41])).
% 0.54/0.75 cnf(c277,plain,~animal(skolem0007)|~plant(X152)|eats(skolem0007,X152)|~animal(skolem0006)|~plant(skolem0002)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c242, c104])).
% 0.54/0.75 cnf(c279,plain,~animal(skolem0007)|~plant(X153)|eats(skolem0007,X153)|~animal(skolem0006)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c277, c79])).
% 0.54/0.75 cnf(c280,plain,~animal(skolem0007)|~plant(X156)|eats(skolem0007,X156)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c279, c84])).
% 0.54/0.75 cnf(c281,plain,~animal(skolem0007)|eats(skolem0007,skolem0002)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c280, c79])).
% 0.54/0.75 cnf(c284,plain,eats(skolem0007,skolem0002)|eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c281, c86])).
% 0.54/0.75 cnf(c288,plain,eats(skolem0007,skolem0006)|~wolf(skolem0007)|~grain(skolem0002),inference(resolution,[status(thm)],[c284, c26])).
% 0.54/0.75 cnf(c295,plain,eats(skolem0007,skolem0006)|~wolf(skolem0007),inference(resolution,[status(thm)],[c288, c47])).
% 0.54/0.75 cnf(c298,plain,eats(skolem0007,skolem0006),inference(resolution,[status(thm)],[c295, c74])).
% 0.54/0.75 cnf(c303,plain,~wolf(skolem0007)|~fox(skolem0006),inference(resolution,[status(thm)],[c298, c25])).
% 0.54/0.75 cnf(c304,plain,~wolf(skolem0007),inference(resolution,[status(thm)],[c303, c68])).
% 0.54/0.75 cnf(c305,plain,$false,inference(resolution,[status(thm)],[c304, c74])).
% 0.54/0.75 % SZS output end CNFRefutation
% 0.54/0.75
% 0.54/0.75 % Initial clauses : 26
% 0.54/0.75 % Processed clauses : 174
% 0.54/0.75 % Factors computed : 12
% 0.54/0.75 % Resolvents computed: 216
% 0.54/0.75 % Tautologies deleted: 0
% 0.54/0.75 % Forward subsumed : 55
% 0.54/0.75 % Backward subsumed : 85
% 0.54/0.75 % -------- CPU Time ---------
% 0.54/0.75 % User time : 0.373 s
% 0.54/0.75 % System time : 0.016 s
% 0.54/0.75 % Total time : 0.389 s
%------------------------------------------------------------------------------