%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ031+3 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:00:18 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ031+3 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n015.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 03:49:20 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f4,axiom,(
% 0.14/0.40 (? [A] : wolf(A) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f5,axiom,(
% 0.14/0.40 (! [A] :( wolf(A)=> animal(A) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f6,axiom,(
% 0.14/0.40 (? [A] : fox(A) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f7,axiom,(
% 0.14/0.40 (! [A] :( fox(A)=> animal(A) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f8,axiom,(
% 0.14/0.40 (? [A] : bird(A) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f9,axiom,(
% 0.14/0.40 (! [A] :( bird(A)=> animal(A) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f12,axiom,(
% 0.14/0.40 (? [A] : snail(A) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f13,axiom,(
% 0.14/0.40 (! [A] :( snail(A)=> animal(A) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f16,axiom,(
% 0.14/0.40 (? [A] : grain(A) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f17,axiom,(
% 0.14/0.40 (! [A] :( grain(A)=> plant(A) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f18,axiom,(
% 0.14/0.40 (! [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) ) ) )) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f19,axiom,(
% 0.14/0.40 (! [Y,X] :( ( bird(Y)& snail(X) )=> much_smaller(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f21,axiom,(
% 0.14/0.40 (! [X,Y] :( ( bird(X)& fox(Y) )=> much_smaller(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f22,axiom,(
% 0.14/0.40 (! [X,Y] :( ( fox(X)& wolf(Y) )=> much_smaller(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f23,axiom,(
% 0.14/0.40 (! [X,Y] :( ( wolf(X)& fox(Y) )=> ~ eats(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f24,axiom,(
% 0.14/0.40 (! [X,Y] :( ( wolf(X)& grain(Y) )=> ~ eats(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f26,axiom,(
% 0.14/0.40 (! [X,Y] :( ( bird(X)& snail(Y) )=> ~ eats(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f28,axiom,(
% 0.14/0.40 (! [X] :( snail(X)=> (? [Y] :( plant(Y)& eats(X,Y) ) )) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f29,conjecture,(
% 0.14/0.40 (? [X,Y,Z] :( animal(X)& animal(Y)& grain(Z)& eats(Y,Z)& eats(X,Y) ) )),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f30,negated_conjecture,(
% 0.14/0.40 ~((? [X,Y,Z] :( animal(X)& animal(Y)& grain(Z)& eats(Y,Z)& eats(X,Y) ) ))),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f29])).
% 0.14/0.40 fof(f37,plain,(
% 0.14/0.40 wolf(sK2_skl)),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f4])).
% 0.14/0.40 fof(f38,plain,(
% 0.14/0.40 wolf(sK2_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/0.40 fof(f39,plain,(
% 0.14/0.40 ![A]: (~wolf(A)|animal(A))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.40 fof(f40,plain,(
% 0.14/0.40 ![X0]: (~wolf(X0)|animal(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.40 fof(f41,plain,(
% 0.14/0.40 fox(sK3_skl)),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f6])).
% 0.14/0.40 fof(f42,plain,(
% 0.14/0.40 fox(sK3_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/0.40 fof(f43,plain,(
% 0.14/0.40 ![A]: (~fox(A)|animal(A))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/0.40 fof(f44,plain,(
% 0.14/0.40 ![X0]: (~fox(X0)|animal(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.14/0.40 fof(f45,plain,(
% 0.14/0.40 bird(sK4_skl)),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f8])).
% 0.14/0.40 fof(f46,plain,(
% 0.14/0.40 bird(sK4_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.40 fof(f47,plain,(
% 0.14/0.40 ![A]: (~bird(A)|animal(A))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.40 fof(f48,plain,(
% 0.14/0.40 ![X0]: (~bird(X0)|animal(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/0.40 fof(f53,plain,(
% 0.14/0.40 snail(sK6_skl)),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f12])).
% 0.14/0.40 fof(f54,plain,(
% 0.14/0.40 snail(sK6_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/0.40 fof(f55,plain,(
% 0.14/0.40 ![A]: (~snail(A)|animal(A))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.14/0.40 fof(f56,plain,(
% 0.14/0.40 ![X0]: (~snail(X0)|animal(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/0.40 fof(f61,plain,(
% 0.14/0.40 grain(sK8_skl)),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f16])).
% 0.14/0.40 fof(f62,plain,(
% 0.14/0.40 grain(sK8_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f61])).
% 0.14/0.40 fof(f63,plain,(
% 0.14/0.40 ![A]: (~grain(A)|plant(A))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.14/0.40 fof(f64,plain,(
% 0.14/0.40 ![X0]: (~grain(X0)|plant(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.14/0.40 fof(f65,plain,(
% 0.14/0.40 ![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))))))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.14/0.40 fof(f66,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~animal(X2)|~much_smaller(X2,X0)|~plant(X3)|~eats(X2,X3)|eats(X0,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.14/0.40 fof(f67,plain,(
% 0.14/0.40 ![Y,X]: ((~bird(Y)|~snail(X))|much_smaller(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.14/0.40 fof(f68,plain,(
% 0.14/0.40 ![X0,X1]: (~bird(X0)|~snail(X1)|much_smaller(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/0.40 fof(f71,plain,(
% 0.14/0.40 ![X,Y]: ((~bird(X)|~fox(Y))|much_smaller(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.14/0.40 fof(f72,plain,(
% 0.14/0.40 ![X0,X1]: (~bird(X0)|~fox(X1)|much_smaller(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/0.40 fof(f73,plain,(
% 0.14/0.40 ![X,Y]: ((~fox(X)|~wolf(Y))|much_smaller(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.14/0.40 fof(f74,plain,(
% 0.14/0.40 ![X0,X1]: (~fox(X0)|~wolf(X1)|much_smaller(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.40 fof(f75,plain,(
% 0.14/0.40 ![X,Y]: ((~wolf(X)|~fox(Y))|~eats(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.14/0.40 fof(f76,plain,(
% 0.14/0.40 ![X0,X1]: (~wolf(X0)|~fox(X1)|~eats(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.40 fof(f77,plain,(
% 0.14/0.40 ![X,Y]: ((~wolf(X)|~grain(Y))|~eats(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.14/0.40 fof(f78,plain,(
% 0.14/0.40 ![X0,X1]: (~wolf(X0)|~grain(X1)|~eats(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.40 fof(f81,plain,(
% 0.14/0.40 ![X,Y]: ((~bird(X)|~snail(Y))|~eats(X,Y))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.14/0.40 fof(f82,plain,(
% 0.14/0.40 ![X0,X1]: (~bird(X0)|~snail(X1)|~eats(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f81])).
% 0.14/0.40 fof(f87,plain,(
% 0.14/0.40 ![X]: (~snail(X)|(?[Y]: (plant(Y)&eats(X,Y))))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.14/0.40 fof(f88,plain,(
% 0.14/0.40 ![X]: (~snail(X)|(plant(sK10_skl(X))&eats(X,sK10_skl(X))))),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Y,sK10_skl(X))],[f87])).
% 0.14/0.40 fof(f89,plain,(
% 0.14/0.40 ![X0]: (~snail(X0)|plant(sK10_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f88])).
% 0.14/0.40 fof(f90,plain,(
% 0.14/0.40 ![X0]: (~snail(X0)|eats(X0,sK10_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f88])).
% 0.14/0.40 fof(f91,plain,(
% 0.14/0.40 (![X,Y,Z]: ((((~animal(X)|~animal(Y))|~grain(Z))|~eats(Y,Z))|~eats(X,Y)))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.14/0.40 fof(f92,plain,(
% 0.14/0.40 ![X,Y]: ((![Z]: (((~animal(X)|~animal(Y))|~grain(Z))|~eats(Y,Z)))|~eats(X,Y))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f91])).
% 0.14/0.40 fof(f93,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~animal(X0)|~animal(X1)|~grain(X2)|~eats(X1,X2)|~eats(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f92])).
% 0.14/0.40 fof(f95,plain,(
% 0.14/0.40 animal(sK2_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f40,f38])).
% 0.14/0.40 fof(f96,plain,(
% 0.14/0.40 animal(sK3_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f44,f42])).
% 0.14/0.40 fof(f97,plain,(
% 0.14/0.40 animal(sK4_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f48,f46])).
% 0.14/0.40 fof(f99,plain,(
% 0.14/0.40 animal(sK6_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f56,f54])).
% 0.14/0.40 fof(f102,plain,(
% 0.14/0.40 plant(sK8_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f62,f64])).
% 0.14/0.40 fof(f103,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~animal(X0)|eats(X0,sK8_skl)|~animal(X1)|~much_smaller(X1,X0)|~plant(X2)|~eats(X1,X2)|eats(X0,X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f102,f66])).
% 0.14/0.40 fof(f105,plain,(
% 0.14/0.40 ![X0]: (~snail(X0)|much_smaller(X0,sK4_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f68,f46])).
% 0.14/0.40 fof(f107,plain,(
% 0.14/0.40 ![X0]: (~fox(X0)|much_smaller(sK4_skl,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f72,f46])).
% 0.14/0.40 fof(f108,plain,(
% 0.14/0.40 ![X0]: (~wolf(X0)|much_smaller(sK3_skl,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f74,f42])).
% 0.14/0.40 fof(f117,plain,(
% 0.14/0.40 plant(sK10_skl(sK6_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f89,f54])).
% 0.14/0.40 fof(f118,plain,(
% 0.14/0.40 eats(sK6_skl,sK10_skl(sK6_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f90,f54])).
% 0.14/0.40 fof(f119,plain,(
% 0.14/0.40 much_smaller(sK6_skl,sK4_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f105,f54])).
% 0.14/0.40 fof(f121,plain,(
% 0.14/0.40 much_smaller(sK4_skl,sK3_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f107,f42])).
% 0.14/0.40 fof(f122,plain,(
% 0.14/0.40 much_smaller(sK3_skl,sK2_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f108,f38])).
% 0.14/0.40 fof(f159,plain,(
% 0.14/0.40 ![X0]: (~animal(sK4_skl)|eats(sK4_skl,sK8_skl)|~animal(sK6_skl)|~plant(X0)|~eats(sK6_skl,X0)|eats(sK4_skl,sK6_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f119,f103])).
% 0.14/0.40 fof(f161,definition,(
% 0.14/0.40 sQ7_spl <=> (animal(sK4_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f163,plain,(
% 0.14/0.40 ~animal(sK4_skl)|sQ7_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f161])).
% 0.14/0.40 fof(f167,definition,(
% 0.14/0.40 sQ9_spl <=> (animal(sK6_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f169,plain,(
% 0.14/0.40 ~animal(sK6_skl)|sQ9_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f167])).
% 0.14/0.40 fof(f170,definition,(
% 0.14/0.40 ![X0]: (sQ10_spl <=> (~plant(X0)|~eats(sK6_skl,X0)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f171,plain,(
% 0.14/0.40 ![X0]: (~plant(X0)|~eats(sK6_skl,X0)|~sQ10_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f170])).
% 0.14/0.40 fof(f173,definition,(
% 0.14/0.40 sQ11_spl <=> (eats(sK4_skl,sK6_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f174,plain,(
% 0.14/0.40 eats(sK4_skl,sK6_skl)|~sQ11_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f173])).
% 0.14/0.40 fof(f181,definition,(
% 0.14/0.40 sQ13_spl <=> (eats(sK4_skl,sK8_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f182,plain,(
% 0.14/0.40 eats(sK4_skl,sK8_skl)|~sQ13_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f181])).
% 0.14/0.40 fof(f184,plain,(
% 0.14/0.40 ~sQ7_spl|sQ13_spl|~sQ9_spl|sQ10_spl|sQ11_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f159,f161,f181,f167,f170,f173])).
% 0.14/0.40 fof(f189,plain,(
% 0.14/0.40 $false|sQ9_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f169,f99])).
% 0.14/0.40 fof(f190,plain,(
% 0.14/0.40 sQ9_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f189])).
% 0.14/0.40 fof(f191,plain,(
% 0.14/0.40 $false|sQ7_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f163,f97])).
% 0.14/0.40 fof(f192,plain,(
% 0.14/0.40 sQ7_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f191])).
% 0.14/0.40 fof(f211,plain,(
% 0.14/0.40 ![X0]: (~animal(sK3_skl)|eats(sK3_skl,sK8_skl)|~animal(sK4_skl)|~plant(X0)|~eats(sK4_skl,X0)|eats(sK3_skl,sK4_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f121,f103])).
% 0.14/0.40 fof(f213,definition,(
% 0.14/0.40 sQ17_spl <=> (animal(sK3_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f215,plain,(
% 0.14/0.40 ~animal(sK3_skl)|sQ17_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f213])).
% 0.14/0.40 fof(f219,definition,(
% 0.14/0.40 ![X0]: (sQ19_spl <=> (~plant(X0)|~eats(sK4_skl,X0)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f220,plain,(
% 0.14/0.40 ![X0]: (~plant(X0)|~eats(sK4_skl,X0)|~sQ19_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f219])).
% 0.14/0.40 fof(f222,definition,(
% 0.14/0.40 sQ20_spl <=> (eats(sK3_skl,sK4_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f223,plain,(
% 0.14/0.40 eats(sK3_skl,sK4_skl)|~sQ20_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f222])).
% 0.14/0.40 fof(f230,definition,(
% 0.14/0.40 sQ22_spl <=> (eats(sK3_skl,sK8_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f231,plain,(
% 0.14/0.40 eats(sK3_skl,sK8_skl)|~sQ22_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f230])).
% 0.14/0.40 fof(f233,plain,(
% 0.14/0.40 ~sQ17_spl|sQ22_spl|~sQ7_spl|sQ19_spl|sQ20_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f211,f213,f230,f161,f219,f222])).
% 0.14/0.40 fof(f238,plain,(
% 0.14/0.40 $false|sQ17_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f215,f96])).
% 0.14/0.40 fof(f239,plain,(
% 0.14/0.40 sQ17_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f238])).
% 0.14/0.40 fof(f242,plain,(
% 0.14/0.40 ![X0]: (~animal(sK2_skl)|eats(sK2_skl,sK8_skl)|~animal(sK3_skl)|~plant(X0)|~eats(sK3_skl,X0)|eats(sK2_skl,sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f122,f103])).
% 0.14/0.40 fof(f244,definition,(
% 0.14/0.40 sQ24_spl <=> (animal(sK2_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f246,plain,(
% 0.14/0.40 ~animal(sK2_skl)|sQ24_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f244])).
% 0.14/0.40 fof(f250,definition,(
% 0.14/0.40 ![X0]: (sQ26_spl <=> (~plant(X0)|~eats(sK3_skl,X0)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f251,plain,(
% 0.14/0.40 ![X0]: (~plant(X0)|~eats(sK3_skl,X0)|~sQ26_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f250])).
% 0.14/0.40 fof(f253,definition,(
% 0.14/0.40 sQ27_spl <=> (eats(sK2_skl,sK3_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f254,plain,(
% 0.14/0.40 eats(sK2_skl,sK3_skl)|~sQ27_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f253])).
% 0.14/0.40 fof(f261,definition,(
% 0.14/0.40 sQ29_spl <=> (eats(sK2_skl,sK8_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f262,plain,(
% 0.14/0.40 eats(sK2_skl,sK8_skl)|~sQ29_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f261])).
% 0.14/0.40 fof(f264,plain,(
% 0.14/0.40 ~sQ24_spl|sQ29_spl|~sQ17_spl|sQ26_spl|sQ27_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f242,f244,f261,f213,f250,f253])).
% 0.14/0.40 fof(f269,plain,(
% 0.14/0.40 $false|sQ24_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f246,f95])).
% 0.14/0.40 fof(f270,plain,(
% 0.14/0.40 sQ24_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f269])).
% 0.14/0.40 fof(f275,definition,(
% 0.14/0.40 sQ31_spl <=> (bird(sK4_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f277,plain,(
% 0.14/0.40 ~bird(sK4_skl)|sQ31_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f275])).
% 0.14/0.40 fof(f293,definition,(
% 0.14/0.40 ![X0]: (sQ36_spl <=> (~animal(X0)|~eats(X0,sK4_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f294,plain,(
% 0.14/0.40 ![X0]: (~animal(X0)|~eats(X0,sK4_skl)|~sQ36_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f293])).
% 0.14/0.40 fof(f297,plain,(
% 0.14/0.40 $false|sQ31_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f277,f46])).
% 0.14/0.40 fof(f298,plain,(
% 0.14/0.40 sQ31_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f297])).
% 0.14/0.40 fof(f325,plain,(
% 0.14/0.40 ~bird(sK4_skl)|~snail(sK6_skl)|~sQ11_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f174,f82])).
% 0.14/0.40 fof(f329,definition,(
% 0.14/0.40 sQ43_spl <=> (snail(sK6_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f331,plain,(
% 0.14/0.40 ~snail(sK6_skl)|sQ43_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f329])).
% 0.14/0.40 fof(f332,plain,(
% 0.14/0.40 ~sQ31_spl|~sQ43_spl|~sQ11_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f325,f275,f329,f173])).
% 0.14/0.40 fof(f342,plain,(
% 0.14/0.40 $false|sQ43_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f331,f54])).
% 0.14/0.40 fof(f343,plain,(
% 0.14/0.40 sQ43_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f342])).
% 0.14/0.40 fof(f344,plain,(
% 0.14/0.40 ~animal(sK3_skl)|~sQ20_spl|~sQ36_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f223,f294])).
% 0.14/0.40 fof(f349,plain,(
% 0.14/0.40 ~sQ17_spl|~sQ20_spl|~sQ36_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f344,f213,f222,f293])).
% 0.14/0.40 fof(f374,plain,(
% 0.14/0.40 ~wolf(sK2_skl)|~fox(sK3_skl)|~sQ27_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f254,f76])).
% 0.14/0.40 fof(f384,definition,(
% 0.14/0.40 sQ54_spl <=> (wolf(sK2_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f386,plain,(
% 0.14/0.40 ~wolf(sK2_skl)|sQ54_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f384])).
% 0.14/0.40 fof(f387,definition,(
% 0.14/0.40 sQ55_spl <=> (fox(sK3_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f389,plain,(
% 0.14/0.40 ~fox(sK3_skl)|sQ55_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f387])).
% 0.14/0.40 fof(f390,plain,(
% 0.14/0.40 ~sQ54_spl|~sQ55_spl|~sQ27_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f374,f384,f387,f253])).
% 0.14/0.40 fof(f399,plain,(
% 0.14/0.40 $false|sQ54_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f386,f38])).
% 0.14/0.40 fof(f400,plain,(
% 0.14/0.40 sQ54_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f399])).
% 0.14/0.40 fof(f401,plain,(
% 0.14/0.40 $false|sQ55_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f389,f42])).
% 0.14/0.40 fof(f402,plain,(
% 0.14/0.40 sQ55_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f401])).
% 0.14/0.40 fof(f403,plain,(
% 0.14/0.40 ~plant(sK10_skl(sK6_skl))|~sQ10_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f171,f118])).
% 0.14/0.40 fof(f404,plain,(
% 0.14/0.40 $false|~sQ10_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f403,f117])).
% 0.14/0.40 fof(f405,plain,(
% 0.14/0.40 ~sQ10_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f404])).
% 0.14/0.40 fof(f406,plain,(
% 0.14/0.40 ~plant(sK8_skl)|~sQ13_spl|~sQ19_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f182,f220])).
% 0.14/0.40 fof(f410,plain,(
% 0.14/0.40 ![X0]: (~animal(X0)|~animal(sK4_skl)|~grain(sK8_skl)|~eats(X0,sK4_skl)|~sQ13_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f182,f93])).
% 0.14/0.40 fof(f411,plain,(
% 0.14/0.40 $false|~sQ13_spl|~sQ19_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f406,f102])).
% 0.14/0.40 fof(f412,plain,(
% 0.14/0.40 ~sQ13_spl|~sQ19_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f411])).
% 0.14/0.40 fof(f421,definition,(
% 0.14/0.40 sQ60_spl <=> (grain(sK8_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f423,plain,(
% 0.14/0.40 ~grain(sK8_skl)|sQ60_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f421])).
% 0.14/0.40 fof(f425,plain,(
% 0.14/0.40 sQ36_spl|~sQ7_spl|~sQ60_spl|~sQ13_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f410,f293,f161,f421,f181])).
% 0.14/0.40 fof(f426,plain,(
% 0.14/0.40 ~plant(sK8_skl)|~sQ22_spl|~sQ26_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f231,f251])).
% 0.14/0.40 fof(f431,plain,(
% 0.14/0.40 $false|~sQ22_spl|~sQ26_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f426,f102])).
% 0.14/0.40 fof(f432,plain,(
% 0.14/0.40 ~sQ22_spl|~sQ26_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f431])).
% 0.14/0.40 fof(f433,plain,(
% 0.14/0.40 $false|sQ60_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f423,f62])).
% 0.14/0.40 fof(f434,plain,(
% 0.14/0.40 sQ60_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f433])).
% 0.14/0.40 fof(f441,plain,(
% 0.14/0.40 ~wolf(sK2_skl)|~grain(sK8_skl)|~sQ29_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f262,f78])).
% 0.14/0.40 fof(f445,plain,(
% 0.14/0.40 ~sQ54_spl|~sQ60_spl|~sQ29_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f441,f384,f421,f261])).
% 0.14/0.40 fof(f447,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f184,f190,f192,f233,f239,f264,f270,f298,f332,f343,f349,f390,f400,f402,f405,f412,f425,f432,f434,f445])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.045643 seconds
% 0.14/0.42 % CPU time: 0.131950 seconds
% 0.14/0.42 % Total memory used: 18.143 MB
% 0.14/0.42 % Net memory used: 17.909 MB
%------------------------------------------------------------------------------