%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ031+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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.07s 0.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ031+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n004.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 03:46:04 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 0.07/0.36 % Refutation found
% 0.07/0.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.36 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.36 fof(f1,axiom,(
% 0.07/0.36 (! [X] :( wolf(X)=> animal(X) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f2,axiom,(
% 0.07/0.36 (? [X1] : wolf(X1) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f3,axiom,(
% 0.07/0.36 (! [X] :( fox(X)=> animal(X) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f4,axiom,(
% 0.07/0.36 (? [X1] : fox(X1) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f5,axiom,(
% 0.07/0.36 (! [X] :( bird(X)=> animal(X) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f6,axiom,(
% 0.07/0.36 (? [X1] : bird(X1) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f9,axiom,(
% 0.07/0.36 (! [X] :( snail(X)=> animal(X) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f10,axiom,(
% 0.07/0.36 (? [X1] : snail(X1) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f11,axiom,(
% 0.07/0.36 (? [X] : grain(X) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f12,axiom,(
% 0.07/0.36 (! [X1] :( grain(X1)=> plant(X1) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f13,axiom,(
% 0.07/0.36 (! [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.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f14,axiom,(
% 0.07/0.36 (! [X,Y] :( ( bird(Y)& ( snail(X)| caterpillar(X) ) )=> much_smaller(X,Y) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f15,axiom,(
% 0.07/0.36 (! [X,Y] :( ( bird(X)& fox(Y) )=> much_smaller(X,Y) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f16,axiom,(
% 0.07/0.36 (! [X,Y] :( ( fox(X)& wolf(Y) )=> much_smaller(X,Y) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f17,axiom,(
% 0.07/0.36 (! [X,Y] :( ( wolf(X)& ( fox(Y)| grain(Y) ) )=> ~ eats(X,Y) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f19,axiom,(
% 0.07/0.36 (! [X,Y] :( ( bird(X)& snail(Y) )=> ~ eats(X,Y) ) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f20,axiom,(
% 0.07/0.36 (! [X] :( ( caterpillar(X)| snail(X) )=> (? [Y] :( plant(Y)& eats(X,Y) ) )) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f21,conjecture,(
% 0.07/0.36 (? [X,Y] :( animal(X)& animal(Y)& (? [Z] :( grain(Z)& eats(Y,Z)& eats(X,Y) ) )) )),
% 0.07/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.36 fof(f22,negated_conjecture,(
% 0.07/0.36 ~((? [X,Y] :( animal(X)& animal(Y)& (? [Z] :( grain(Z)& eats(Y,Z)& eats(X,Y) ) )) ))),
% 0.07/0.36 inference(negated_conjecture,[status(cth)],[f21])).
% 0.07/0.36 fof(f23,plain,(
% 0.07/0.36 ![X]: (~wolf(X)|animal(X))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.07/0.36 fof(f24,plain,(
% 0.07/0.36 ![X0]: (~wolf(X0)|animal(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f23])).
% 0.07/0.36 fof(f25,plain,(
% 0.07/0.36 wolf(sK0_skl)),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X1,sK0_skl)],[f2])).
% 0.07/0.36 fof(f26,plain,(
% 0.07/0.36 wolf(sK0_skl)),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f25])).
% 0.07/0.36 fof(f27,plain,(
% 0.07/0.36 ![X]: (~fox(X)|animal(X))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.07/0.36 fof(f28,plain,(
% 0.07/0.36 ![X0]: (~fox(X0)|animal(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f27])).
% 0.07/0.36 fof(f29,plain,(
% 0.07/0.36 fox(sK1_skl)),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X1,sK1_skl)],[f4])).
% 0.07/0.36 fof(f30,plain,(
% 0.07/0.36 fox(sK1_skl)),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f29])).
% 0.07/0.36 fof(f31,plain,(
% 0.07/0.36 ![X]: (~bird(X)|animal(X))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.07/0.36 fof(f32,plain,(
% 0.07/0.36 ![X0]: (~bird(X0)|animal(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f31])).
% 0.07/0.36 fof(f33,plain,(
% 0.07/0.36 bird(sK2_skl)),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl)],[f6])).
% 0.07/0.36 fof(f34,plain,(
% 0.07/0.36 bird(sK2_skl)),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f33])).
% 0.07/0.36 fof(f39,plain,(
% 0.07/0.36 ![X]: (~snail(X)|animal(X))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.07/0.36 fof(f40,plain,(
% 0.07/0.36 ![X0]: (~snail(X0)|animal(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f39])).
% 0.07/0.36 fof(f41,plain,(
% 0.07/0.36 snail(sK4_skl)),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X1,sK4_skl)],[f10])).
% 0.07/0.36 fof(f42,plain,(
% 0.07/0.36 snail(sK4_skl)),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f41])).
% 0.07/0.36 fof(f43,plain,(
% 0.07/0.36 grain(sK5_skl)),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(X,sK5_skl)],[f11])).
% 0.07/0.36 fof(f44,plain,(
% 0.07/0.36 grain(sK5_skl)),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f43])).
% 0.07/0.36 fof(f45,plain,(
% 0.07/0.36 ![X1]: (~grain(X1)|plant(X1))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.07/0.36 fof(f46,plain,(
% 0.07/0.36 ![X0]: (~grain(X0)|plant(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f45])).
% 0.07/0.36 fof(f47,plain,(
% 0.07/0.36 ![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.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.07/0.36 fof(f48,plain,(
% 0.07/0.36 ![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.07/0.36 inference(cnf_transformation,[status(thm)],[f47])).
% 0.07/0.36 fof(f49,plain,(
% 0.07/0.36 ![X,Y]: ((~bird(Y)|(~snail(X)&~caterpillar(X)))|much_smaller(X,Y))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.07/0.36 fof(f50,plain,(
% 0.07/0.36 ![X0,X1]: (~bird(X0)|~snail(X1)|much_smaller(X1,X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f49])).
% 0.07/0.36 fof(f52,plain,(
% 0.07/0.36 ![X,Y]: ((~bird(X)|~fox(Y))|much_smaller(X,Y))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.07/0.36 fof(f53,plain,(
% 0.07/0.36 ![X0,X1]: (~bird(X0)|~fox(X1)|much_smaller(X0,X1))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f52])).
% 0.07/0.36 fof(f54,plain,(
% 0.07/0.36 ![X,Y]: ((~fox(X)|~wolf(Y))|much_smaller(X,Y))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.07/0.36 fof(f55,plain,(
% 0.07/0.36 ![X0,X1]: (~fox(X0)|~wolf(X1)|much_smaller(X0,X1))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f54])).
% 0.07/0.36 fof(f56,plain,(
% 0.07/0.36 ![X,Y]: ((~wolf(X)|(~fox(Y)&~grain(Y)))|~eats(X,Y))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.07/0.36 fof(f58,plain,(
% 0.07/0.36 ![X0,X1]: (~wolf(X0)|~grain(X1)|~eats(X0,X1))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f56])).
% 0.07/0.36 fof(f61,plain,(
% 0.07/0.36 ![X,Y]: ((~bird(X)|~snail(Y))|~eats(X,Y))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.07/0.36 fof(f62,plain,(
% 0.07/0.36 ![X0,X1]: (~bird(X0)|~snail(X1)|~eats(X0,X1))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f61])).
% 0.07/0.36 fof(f63,plain,(
% 0.07/0.36 ![X]: ((~caterpillar(X)&~snail(X))|(?[Y]: (plant(Y)&eats(X,Y))))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.07/0.36 fof(f64,definition,(
% 0.07/0.36 ![X]: (sP0_prd(X)<=>(~caterpillar(X)&~snail(X)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.07/0.36 fof(f65,plain,(
% 0.07/0.36 ![X]: (sP0_prd(X)|(?[Y]: (plant(Y)&eats(X,Y))))),
% 0.07/0.36 inference(formula_renaming,[status(thm)],[f63,f64])).
% 0.07/0.36 fof(f66,plain,(
% 0.07/0.36 ![X]: (sP0_prd(X)|(plant(sK6_skl(X))&eats(X,sK6_skl(X))))),
% 0.07/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(Y,sK6_skl(X))],[f65])).
% 0.07/0.36 fof(f67,plain,(
% 0.07/0.36 ![X0]: (sP0_prd(X0)|plant(sK6_skl(X0)))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f66])).
% 0.07/0.36 fof(f68,plain,(
% 0.07/0.36 ![X0]: (sP0_prd(X0)|eats(X0,sK6_skl(X0)))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f66])).
% 0.07/0.36 fof(f69,plain,(
% 0.07/0.36 (![X,Y]: ((~animal(X)|~animal(Y))|(![Z]: ((~grain(Z)|~eats(Y,Z))|~eats(X,Y)))))),
% 0.07/0.36 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.07/0.36 fof(f70,plain,(
% 0.07/0.36 ![X,Y]: ((~animal(X)|~animal(Y))|((![Z]: (~grain(Z)|~eats(Y,Z)))|~eats(X,Y)))),
% 0.07/0.36 inference(miniscoping,[status(thm)],[f69])).
% 0.07/0.36 fof(f71,plain,(
% 0.07/0.36 ![X0,X1,X2]: (~animal(X0)|~animal(X1)|~grain(X2)|~eats(X1,X2)|~eats(X0,X1))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f70])).
% 0.07/0.36 fof(f72,plain,(
% 0.07/0.36 ![X]: ((~sP0_prd(X)|(~caterpillar(X)&~snail(X)))&(sP0_prd(X)|(caterpillar(X)|snail(X))))),
% 0.07/0.36 inference(NNF_transformation,[status(thm)],[f64])).
% 0.07/0.36 fof(f73,plain,(
% 0.07/0.36 (![X]: (~sP0_prd(X)|(~caterpillar(X)&~snail(X))))&(![X]: (sP0_prd(X)|(caterpillar(X)|snail(X))))),
% 0.07/0.36 inference(miniscoping,[status(thm)],[f72])).
% 0.07/0.36 fof(f75,plain,(
% 0.07/0.36 ![X0]: (~sP0_prd(X0)|~snail(X0))),
% 0.07/0.36 inference(cnf_transformation,[status(thm)],[f73])).
% 0.07/0.36 fof(f78,plain,(
% 0.07/0.36 ![X0]: (~grain(X0)|~eats(sK0_skl,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f26,f58])).
% 0.07/0.36 fof(f79,plain,(
% 0.07/0.36 ![X0,X1,X2]: (~fox(X0)|~animal(X1)|~grain(X2)|~eats(X0,X2)|~eats(X1,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f28,f71])).
% 0.07/0.36 fof(f80,plain,(
% 0.07/0.36 ![X0,X1]: (~fox(X0)|~animal(X1)|~eats(X0,sK5_skl)|~eats(X1,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f44,f79])).
% 0.07/0.36 fof(f81,plain,(
% 0.07/0.36 ~eats(sK0_skl,sK5_skl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f44,f78])).
% 0.07/0.36 fof(f82,plain,(
% 0.07/0.36 plant(sK5_skl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f44,f46])).
% 0.07/0.36 fof(f97,plain,(
% 0.07/0.36 ![X0,X1,X2]: (sP0_prd(X0)|~animal(X1)|~plant(X2)|eats(X1,X2)|~animal(X0)|~much_smaller(X0,X1)|~plant(sK6_skl(X0))|eats(X1,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f68,f48])).
% 0.07/0.36 fof(f98,plain,(
% 0.07/0.36 ![X0,X1,X2]: (sP0_prd(X0)|~animal(X1)|~plant(X2)|eats(X1,X2)|~animal(X0)|~much_smaller(X0,X1)|eats(X1,X0))),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f97,f67])).
% 0.07/0.36 fof(f112,definition,(
% 0.07/0.36 sQ3_spl <=> (animal(sK2_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f113,plain,(
% 0.07/0.36 animal(sK2_skl)|~sQ3_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f112])).
% 0.07/0.36 fof(f114,plain,(
% 0.07/0.36 ~animal(sK2_skl)|sQ3_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f112])).
% 0.07/0.36 fof(f127,definition,(
% 0.07/0.36 ![X0,X1]: (sQ7_spl <=> (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK2_skl,X0)|eats(X0,sK2_skl)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f128,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK2_skl,X0)|eats(X0,sK2_skl)|~sQ7_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f127])).
% 0.07/0.36 fof(f136,plain,(
% 0.07/0.36 ~bird(sK2_skl)|sQ3_spl),
% 0.07/0.36 inference(resolution,[status(thm)],[f114,f32])).
% 0.07/0.36 fof(f138,plain,(
% 0.07/0.36 $false|sQ3_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f136,f34])).
% 0.07/0.36 fof(f139,plain,(
% 0.07/0.36 sQ3_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f138])).
% 0.07/0.36 fof(f140,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~grain(X1)|~eats(sK2_skl,X1)|~eats(X0,sK2_skl)|~sQ3_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f113,f71])).
% 0.07/0.36 fof(f141,definition,(
% 0.07/0.36 ![X0]: (sQ9_spl <=> (~animal(X0)|~eats(X0,sK2_skl)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f142,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|~eats(X0,sK2_skl)|~sQ9_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f141])).
% 0.07/0.36 fof(f144,definition,(
% 0.07/0.36 ![X1]: (sQ10_spl <=> (~grain(X1)|~eats(sK2_skl,X1)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f145,plain,(
% 0.07/0.36 ![X0]: (~grain(X0)|~eats(sK2_skl,X0)|~sQ10_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f144])).
% 0.07/0.36 fof(f147,plain,(
% 0.07/0.36 sQ9_spl|sQ10_spl|~sQ3_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f140,f141,f144,f112])).
% 0.07/0.36 fof(f148,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK2_skl,X0)|~sQ9_spl|~sQ7_spl)),
% 0.07/0.36 inference(backward_subsumption_resolution,[status(thm)],[f128,f142])).
% 0.07/0.36 fof(f149,plain,(
% 0.07/0.36 ![X0]: (~snail(X0)|~eats(sK2_skl,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f62,f34])).
% 0.07/0.36 fof(f151,plain,(
% 0.07/0.36 ![X0,X1]: (sP0_prd(X0)|~animal(X1)|eats(X1,sK5_skl)|~animal(X0)|~much_smaller(X0,X1)|eats(X1,X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f98,f82])).
% 0.07/0.36 fof(f155,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~much_smaller(sK2_skl,X0)|~sQ9_spl|~sQ7_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f148,f82])).
% 0.07/0.36 fof(f157,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~bird(sK2_skl)|~fox(X0)|~sQ9_spl|~sQ7_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f155,f53])).
% 0.07/0.36 fof(f160,definition,(
% 0.07/0.36 ![X0]: (sQ11_spl <=> (~animal(X0)|eats(X0,sK5_skl)|~wolf(X0)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f161,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~wolf(X0)|~sQ11_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f160])).
% 0.07/0.36 fof(f167,definition,(
% 0.07/0.36 ![X0]: (sQ13_spl <=> (~animal(X0)|eats(X0,sK5_skl)|~fox(X0)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f168,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~fox(X0)|~sQ13_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f167])).
% 0.07/0.36 fof(f170,definition,(
% 0.07/0.36 sQ14_spl <=> (bird(sK2_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f172,plain,(
% 0.07/0.36 ~bird(sK2_skl)|sQ14_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f170])).
% 0.07/0.36 fof(f173,plain,(
% 0.07/0.36 sQ13_spl|~sQ14_spl|~sQ9_spl|~sQ7_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f157,f167,f170,f141,f127])).
% 0.07/0.36 fof(f186,plain,(
% 0.07/0.36 ![X0]: (eats(X0,sK5_skl)|~wolf(X0)|~sQ11_spl)),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f161,f24])).
% 0.07/0.36 fof(f187,plain,(
% 0.07/0.36 ![X0,X1]: (~fox(X0)|~animal(X1)|~eats(X1,X0)|~sQ13_spl)),
% 0.07/0.36 inference(backward_subsumption_resolution,[status(thm)],[f80,f188])).
% 0.07/0.36 fof(f188,plain,(
% 0.07/0.36 ![X0]: (eats(X0,sK5_skl)|~fox(X0)|~sQ13_spl)),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f168,f28])).
% 0.07/0.36 fof(f209,definition,(
% 0.07/0.36 sQ22_spl <=> (plant(sK5_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f211,plain,(
% 0.07/0.36 ~plant(sK5_skl)|sQ22_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f209])).
% 0.07/0.36 fof(f213,plain,(
% 0.07/0.36 eats(sK0_skl,sK5_skl)|~sQ11_spl),
% 0.07/0.36 inference(resolution,[status(thm)],[f186,f26])).
% 0.07/0.36 fof(f214,plain,(
% 0.07/0.36 $false|~sQ11_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f213,f81])).
% 0.07/0.36 fof(f215,plain,(
% 0.07/0.36 ~sQ11_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f214])).
% 0.07/0.36 fof(f218,definition,(
% 0.07/0.36 ![X0]: (sQ23_spl <=> (~animal(X0)|~eats(X0,sK1_skl)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f219,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|~eats(X0,sK1_skl)|~sQ23_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f218])).
% 0.07/0.36 fof(f228,plain,(
% 0.07/0.36 ![X0,X1]: (sP0_prd(X0)|~animal(X1)|eats(X1,sK5_skl)|~animal(X0)|eats(X1,X0)|~bird(X1)|~snail(X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f151,f50])).
% 0.07/0.36 fof(f231,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|eats(X0,sK5_skl)|~animal(X1)|eats(X0,X1)|~bird(X0)|~snail(X1))),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f228,f75])).
% 0.07/0.36 fof(f232,plain,(
% 0.07/0.36 ~eats(sK2_skl,sK5_skl)|~sQ10_spl),
% 0.07/0.36 inference(resolution,[status(thm)],[f145,f44])).
% 0.07/0.36 fof(f262,plain,(
% 0.07/0.36 $false|sQ14_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f172,f34])).
% 0.07/0.36 fof(f263,plain,(
% 0.07/0.36 sQ14_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f262])).
% 0.07/0.36 fof(f272,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|~eats(X0,sK1_skl)|~sQ13_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f187,f30])).
% 0.07/0.36 fof(f282,plain,(
% 0.07/0.36 eats(sK1_skl,sK5_skl)|~sQ13_spl),
% 0.07/0.36 inference(resolution,[status(thm)],[f188,f30])).
% 0.07/0.36 fof(f286,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~animal(sK1_skl)|~much_smaller(sK1_skl,X0)|~plant(sK5_skl)|eats(X0,sK1_skl)|~sQ13_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f282,f48])).
% 0.07/0.36 fof(f287,definition,(
% 0.07/0.36 sQ30_spl <=> (animal(sK1_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f289,plain,(
% 0.07/0.36 ~animal(sK1_skl)|sQ30_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f287])).
% 0.07/0.36 fof(f293,definition,(
% 0.07/0.36 ![X0,X1]: (sQ31_spl <=> (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK1_skl,X0)|eats(X0,sK1_skl)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f294,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK1_skl,X0)|eats(X0,sK1_skl)|~sQ31_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f293])).
% 0.07/0.36 fof(f296,plain,(
% 0.07/0.36 sQ31_spl|~sQ30_spl|~sQ22_spl|~sQ13_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f286,f293,f287,f209,f167])).
% 0.07/0.36 fof(f300,plain,(
% 0.07/0.36 ~fox(sK1_skl)|sQ30_spl),
% 0.07/0.36 inference(resolution,[status(thm)],[f289,f28])).
% 0.07/0.36 fof(f301,plain,(
% 0.07/0.36 $false|sQ30_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f300,f30])).
% 0.07/0.36 fof(f302,plain,(
% 0.07/0.36 sQ30_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f301])).
% 0.07/0.36 fof(f303,plain,(
% 0.07/0.36 $false|sQ22_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f211,f82])).
% 0.07/0.36 fof(f304,plain,(
% 0.07/0.36 sQ22_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f303])).
% 0.07/0.36 fof(f305,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~much_smaller(sK1_skl,X0)|~sQ23_spl|~sQ31_spl)),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f294,f219])).
% 0.07/0.36 fof(f321,plain,(
% 0.07/0.36 ![X0]: (~animal(sK2_skl)|eats(sK2_skl,sK5_skl)|~animal(X0)|eats(sK2_skl,X0)|~snail(X0))),
% 0.07/0.36 inference(resolution,[status(thm)],[f231,f34])).
% 0.07/0.36 fof(f322,definition,(
% 0.07/0.36 sQ34_spl <=> (eats(sK2_skl,sK5_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f323,plain,(
% 0.07/0.36 eats(sK2_skl,sK5_skl)|~sQ34_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f322])).
% 0.07/0.36 fof(f325,definition,(
% 0.07/0.36 ![X0]: (sQ35_spl <=> (~animal(X0)|eats(sK2_skl,X0)|~snail(X0)))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f326,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(sK2_skl,X0)|~snail(X0)|~sQ35_spl)),
% 0.07/0.36 inference(component_clause,[status(thm)],[f325])).
% 0.07/0.36 fof(f328,plain,(
% 0.07/0.36 ~sQ3_spl|sQ34_spl|sQ35_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f321,f112,f322,f325])).
% 0.07/0.36 fof(f329,plain,(
% 0.07/0.36 $false|~sQ10_spl|~sQ34_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f323,f232])).
% 0.07/0.36 fof(f330,plain,(
% 0.07/0.36 ~sQ10_spl|~sQ34_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f329])).
% 0.07/0.36 fof(f331,plain,(
% 0.07/0.36 ![X0]: (~snail(X0)|~sQ35_spl)),
% 0.07/0.36 inference(backward_subsumption_resolution,[status(thm)],[f149,f332])).
% 0.07/0.36 fof(f332,plain,(
% 0.07/0.36 ![X0]: (eats(sK2_skl,X0)|~snail(X0)|~sQ35_spl)),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f326,f40])).
% 0.07/0.36 fof(f334,plain,(
% 0.07/0.36 $false|~sQ35_spl),
% 0.07/0.36 inference(backward_subsumption_resolution,[status(thm)],[f42,f331])).
% 0.07/0.36 fof(f335,plain,(
% 0.07/0.36 ~sQ35_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f334])).
% 0.07/0.36 fof(f357,plain,(
% 0.07/0.36 ![X0,X1]: (~animal(X0)|~plant(X1)|eats(X0,X1)|~animal(sK2_skl)|~much_smaller(sK2_skl,X0)|~plant(sK5_skl)|eats(X0,sK2_skl)|~sQ34_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f323,f48])).
% 0.07/0.36 fof(f360,plain,(
% 0.07/0.36 sQ7_spl|~sQ3_spl|~sQ22_spl|~sQ34_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f357,f127,f112,f209,f322])).
% 0.07/0.36 fof(f378,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~much_smaller(sK1_skl,X0)|~sQ23_spl|~sQ31_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f305,f82])).
% 0.07/0.36 fof(f379,plain,(
% 0.07/0.36 ![X0]: (~animal(X0)|eats(X0,sK5_skl)|~fox(sK1_skl)|~wolf(X0)|~sQ23_spl|~sQ31_spl)),
% 0.07/0.36 inference(resolution,[status(thm)],[f378,f55])).
% 0.07/0.36 fof(f382,definition,(
% 0.07/0.36 sQ40_spl <=> (fox(sK1_skl))),
% 0.07/0.36 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.07/0.36 fof(f384,plain,(
% 0.07/0.36 ~fox(sK1_skl)|sQ40_spl),
% 0.07/0.36 inference(component_clause,[status(thm)],[f382])).
% 0.07/0.36 fof(f385,plain,(
% 0.07/0.36 sQ11_spl|~sQ40_spl|~sQ23_spl|~sQ31_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f379,f160,f382,f218,f293])).
% 0.07/0.36 fof(f394,plain,(
% 0.07/0.36 sQ23_spl|~sQ13_spl),
% 0.07/0.36 inference(split_clause,[status(thm)],[f272,f218,f167])).
% 0.07/0.36 fof(f395,plain,(
% 0.07/0.36 $false|sQ40_spl),
% 0.07/0.36 inference(forward_subsumption_resolution,[status(thm)],[f384,f30])).
% 0.07/0.36 fof(f396,plain,(
% 0.07/0.36 sQ40_spl),
% 0.07/0.36 inference(contradiction_clause,[status(thm)],[f395])).
% 0.07/0.36 fof(f397,plain,(
% 0.07/0.36 $false),
% 0.07/0.36 inference(sat_refutation,[status(thm)],[f139,f147,f173,f215,f263,f296,f302,f304,f328,f330,f335,f360,f385,f394,f396])).
% 0.07/0.36 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.38 % Elapsed time: 0.036059 seconds
% 0.12/0.38 % CPU time: 0.070923 seconds
% 0.12/0.38 % Total memory used: 4.636 MB
% 0.12/0.38 % Net memory used: 4.603 MB
%------------------------------------------------------------------------------