%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ031-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 01:59:55 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.40s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 45
% Syntax : Number of formulae : 167 ( 33 unt; 22 def)
% Number of atoms : 408 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 467 ( 226 ~; 219 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 23 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 103 ( 103 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ wolf(X)
| animal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( ~ fox(X)
| animal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] :
( ~ bird(X)
| animal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] :
( ~ caterpillar(X)
| animal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] :
( ~ snail(X)
| animal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
wolf(a_wolf),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
fox(a_fox),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
bird(a_bird),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
caterpillar(a_caterpillar),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
snail(a_snail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
grain(a_grain),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( ~ grain(X)
| plant(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Animal,Plant,Small_animal,Other_plant] :
( ~ eats(Small_animal,Other_plant)
| ~ much_smaller(Small_animal,Animal)
| ~ plant(Other_plant)
| ~ animal(Small_animal)
| ~ plant(Plant)
| ~ animal(Animal)
| eats(Animal,Small_animal)
| eats(Animal,Plant) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Snail,Bird] :
( ~ bird(Bird)
| ~ snail(Snail)
| much_smaller(Snail,Bird) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Bird,Fox] :
( ~ fox(Fox)
| ~ bird(Bird)
| much_smaller(Bird,Fox) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [Fox,Wolf] :
( ~ wolf(Wolf)
| ~ fox(Fox)
| much_smaller(Fox,Wolf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Wolf,Fox] :
( ~ eats(Wolf,Fox)
| ~ fox(Fox)
| ~ wolf(Wolf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [Wolf,Grain] :
( ~ eats(Wolf,Grain)
| ~ grain(Grain)
| ~ wolf(Wolf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Bird,Snail] :
( ~ eats(Bird,Snail)
| ~ snail(Snail)
| ~ bird(Bird) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Catapillar] :
( ~ caterpillar(Catapillar)
| plant(caterpillar_food_of(Catapillar)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Snail] :
( ~ snail(Snail)
| plant(snail_food_of(Snail)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Snail] :
( ~ snail(Snail)
| eats(Snail,snail_food_of(Snail)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [Animal,Grain_eater,Grain] :
( ~ eats(Grain_eater,Grain)
| ~ eats(Animal,Grain_eater)
| ~ grain(Grain)
| ~ animal(Grain_eater)
| ~ animal(Animal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,plain,
! [X0] :
( ~ wolf(X0)
| animal(X0) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f28,plain,
! [X0] :
( ~ fox(X0)
| animal(X0) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f29,plain,
! [X0] :
( ~ bird(X0)
| animal(X0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f30,plain,
! [X0] :
( ~ caterpillar(X0)
| animal(X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
! [X0] :
( ~ snail(X0)
| animal(X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f32,plain,
wolf(a_wolf),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f33,plain,
fox(a_fox),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f34,plain,
bird(a_bird),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f35,plain,
caterpillar(a_caterpillar),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f36,plain,
snail(a_snail),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f37,plain,
grain(a_grain),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f38,plain,
! [X0] :
( ~ grain(X0)
| plant(X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f39,plain,
! [Small_animal,Other_plant] :
( ~ eats(Small_animal,Other_plant)
| ! [Animal] :
( ~ much_smaller(Small_animal,Animal)
| ~ plant(Other_plant)
| ~ animal(Small_animal)
| ! [Plant] :
( ~ plant(Plant)
| ~ animal(Animal)
| eats(Animal,Small_animal)
| eats(Animal,Plant) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f40,plain,
! [X0,X1,X2,X3] :
( ~ eats(X2,X3)
| ~ much_smaller(X2,X0)
| ~ plant(X3)
| ~ animal(X2)
| ~ plant(X1)
| ~ animal(X0)
| eats(X0,X2)
| eats(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f43,plain,
! [Bird] :
( ~ bird(Bird)
| ! [Snail] :
( ~ snail(Snail)
| much_smaller(Snail,Bird) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f44,plain,
! [X0,X1] :
( ~ bird(X1)
| ~ snail(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f45,plain,
! [Fox] :
( ~ fox(Fox)
| ! [Bird] :
( ~ bird(Bird)
| much_smaller(Bird,Fox) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f46,plain,
! [X0,X1] :
( ~ fox(X1)
| ~ bird(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [Wolf] :
( ~ wolf(Wolf)
| ! [Fox] :
( ~ fox(Fox)
| much_smaller(Fox,Wolf) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f48,plain,
! [X0,X1] :
( ~ wolf(X1)
| ~ fox(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( ~ eats(X0,X1)
| ~ fox(X1)
| ~ wolf(X0) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f50,plain,
! [X0,X1] :
( ~ eats(X0,X1)
| ~ grain(X1)
| ~ wolf(X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f53,plain,
! [X0,X1] :
( ~ eats(X0,X1)
| ~ snail(X1)
| ~ bird(X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f54,plain,
! [X0] :
( ~ caterpillar(X0)
| plant(caterpillar_food_of(X0)) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f56,plain,
! [X0] :
( ~ snail(X0)
| plant(snail_food_of(X0)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f57,plain,
! [X0] :
( ~ snail(X0)
| eats(X0,snail_food_of(X0)) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f58,plain,
! [Grain_eater,Grain] :
( ~ eats(Grain_eater,Grain)
| ! [Animal] :
( ~ eats(Animal,Grain_eater)
| ~ grain(Grain)
| ~ animal(Grain_eater)
| ~ animal(Animal) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f59,plain,
! [X0,X1,X2] :
( ~ eats(X1,X2)
| ~ eats(X0,X1)
| ~ grain(X2)
| ~ animal(X1)
| ~ animal(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
animal(a_wolf),
inference(resolution,[status(thm)],[f32,f27]) ).
fof(f61,plain,
! [X0] :
( ~ eats(X0,a_grain)
| ~ wolf(X0) ),
inference(resolution,[status(thm)],[f37,f50]) ).
fof(f62,plain,
! [X0,X1] :
( ~ eats(X1,a_grain)
| ~ eats(X0,X1)
| ~ animal(X1)
| ~ animal(X0) ),
inference(resolution,[status(thm)],[f37,f59]) ).
fof(f76,plain,
animal(a_fox),
inference(resolution,[status(thm)],[f28,f33]) ).
fof(f90,plain,
animal(a_bird),
inference(resolution,[status(thm)],[f29,f34]) ).
fof(f91,plain,
! [X0] :
( ~ eats(a_bird,a_grain)
| ~ eats(X0,a_bird)
| ~ animal(X0) ),
inference(resolution,[status(thm)],[f90,f62]) ).
fof(f93,definition,
! [X0] :
( sQ6_spl
<=> ( ~ eats(X0,a_bird)
| ~ animal(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f94,plain,
! [X0] :
( ~ sQ6_spl
| ~ eats(X0,a_bird)
| ~ animal(X0) ),
inference(component_clause,[status(thm)],[f93]) ).
fof(f96,definition,
( sQ7_spl
<=> eats(a_bird,a_grain) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f97,plain,
( ~ sQ7_spl
| eats(a_bird,a_grain) ),
inference(component_clause,[status(thm)],[f96]) ).
fof(f98,plain,
( sQ7_spl
| ~ eats(a_bird,a_grain) ),
inference(component_clause,[status(thm)],[f96]) ).
fof(f99,plain,
( ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f91,f93,f96]) ).
fof(f104,plain,
animal(a_caterpillar),
inference(resolution,[status(thm)],[f30,f35]) ).
fof(f118,plain,
animal(a_snail),
inference(resolution,[status(thm)],[f31,f36]) ).
fof(f133,plain,
! [X0] :
( ~ bird(X0)
| much_smaller(a_snail,X0) ),
inference(resolution,[status(thm)],[f44,f36]) ).
fof(f136,definition,
! [X0] :
( sQ15_spl
<=> ( ~ plant(X0)
| eats(a_bird,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f137,plain,
! [X0] :
( ~ sQ15_spl
| ~ plant(X0)
| eats(a_bird,X0) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f142,definition,
( sQ17_spl
<=> animal(a_bird) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f144,plain,
( sQ17_spl
| ~ animal(a_bird) ),
inference(component_clause,[status(thm)],[f142]) ).
fof(f145,definition,
( sQ18_spl
<=> animal(a_caterpillar) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f147,plain,
( sQ18_spl
| ~ animal(a_caterpillar) ),
inference(component_clause,[status(thm)],[f145]) ).
fof(f152,plain,
much_smaller(a_snail,a_bird),
inference(resolution,[status(thm)],[f133,f34]) ).
fof(f153,plain,
! [X0] :
( ~ fox(X0)
| much_smaller(a_bird,X0) ),
inference(resolution,[status(thm)],[f46,f34]) ).
fof(f154,plain,
! [X0] :
( ~ wolf(X0)
| much_smaller(a_fox,X0) ),
inference(resolution,[status(thm)],[f48,f33]) ).
fof(f156,definition,
( sQ20_spl
<=> eats(a_bird,a_snail) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ20_spl
| eats(a_bird,a_snail) ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,definition,
( sQ21_spl
<=> animal(a_snail) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f161,plain,
( sQ21_spl
| ~ animal(a_snail) ),
inference(component_clause,[status(thm)],[f159]) ).
fof(f166,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f144,f90]) ).
fof(f167,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f166]) ).
fof(f168,plain,
much_smaller(a_bird,a_fox),
inference(resolution,[status(thm)],[f153,f33]) ).
fof(f169,plain,
! [X0,X1] :
( ~ eats(a_bird,X1)
| ~ plant(X1)
| ~ animal(a_bird)
| ~ plant(X0)
| ~ animal(a_fox)
| eats(a_fox,a_bird)
| eats(a_fox,X0) ),
inference(resolution,[status(thm)],[f168,f40]) ).
fof(f170,definition,
! [X0] :
( sQ23_spl
<=> ( ~ plant(X0)
| eats(a_fox,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f171,plain,
! [X0] :
( ~ sQ23_spl
| ~ plant(X0)
| eats(a_fox,X0) ),
inference(component_clause,[status(thm)],[f170]) ).
fof(f173,definition,
( sQ24_spl
<=> eats(a_fox,a_bird) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( ~ sQ24_spl
| eats(a_fox,a_bird) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f176,definition,
( sQ25_spl
<=> animal(a_fox) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f178,plain,
( sQ25_spl
| ~ animal(a_fox) ),
inference(component_clause,[status(thm)],[f176]) ).
fof(f179,definition,
! [X1] :
( sQ26_spl
<=> ( ~ eats(a_bird,X1)
| ~ plant(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f180,plain,
! [X0] :
( ~ sQ26_spl
| ~ eats(a_bird,X0)
| ~ plant(X0) ),
inference(component_clause,[status(thm)],[f179]) ).
fof(f182,plain,
( sQ26_spl
| ~ sQ17_spl
| ~ sQ25_spl
| sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f169,f170,f173,f176,f142,f179]) ).
fof(f183,plain,
much_smaller(a_fox,a_wolf),
inference(resolution,[status(thm)],[f154,f32]) ).
fof(f184,plain,
! [X0,X1] :
( ~ eats(a_fox,X1)
| ~ plant(X1)
| ~ animal(a_fox)
| ~ plant(X0)
| ~ animal(a_wolf)
| eats(a_wolf,a_fox)
| eats(a_wolf,X0) ),
inference(resolution,[status(thm)],[f183,f40]) ).
fof(f185,definition,
! [X0] :
( sQ27_spl
<=> ( ~ plant(X0)
| eats(a_wolf,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f186,plain,
! [X0] :
( ~ sQ27_spl
| ~ plant(X0)
| eats(a_wolf,X0) ),
inference(component_clause,[status(thm)],[f185]) ).
fof(f188,definition,
( sQ28_spl
<=> eats(a_wolf,a_fox) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( ~ sQ28_spl
| eats(a_wolf,a_fox) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,definition,
( sQ29_spl
<=> animal(a_wolf) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ29_spl
| ~ animal(a_wolf) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
! [X1] :
( sQ30_spl
<=> ( ~ eats(a_fox,X1)
| ~ plant(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f195,plain,
! [X0] :
( ~ sQ30_spl
| ~ eats(a_fox,X0)
| ~ plant(X0) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( sQ30_spl
| ~ sQ25_spl
| ~ sQ29_spl
| sQ28_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f184,f185,f188,f191,f176,f194]) ).
fof(f198,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f76]) ).
fof(f199,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f198]) ).
fof(f200,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f193,f60]) ).
fof(f201,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f200]) ).
fof(f206,plain,
! [X0] :
( ~ sQ15_spl
| ~ grain(X0)
| eats(a_bird,X0) ),
inference(resolution,[status(thm)],[f137,f38]) ).
fof(f208,plain,
( ~ sQ15_spl
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[f206,f37]) ).
fof(f212,definition,
( sQ31_spl
<=> bird(a_bird) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( sQ31_spl
| ~ bird(a_bird) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f226,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f214,f34]) ).
fof(f227,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f226]) ).
fof(f228,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ30_spl
| ~ plant(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f171,f195]) ).
fof(f229,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f161,f118]) ).
fof(f230,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f229]) ).
fof(f233,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ30_spl
| ~ grain(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f38,f228]) ).
fof(f234,plain,
( ~ sQ23_spl
| ~ sQ30_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f37,f233]) ).
fof(f235,plain,
( ~ sQ23_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f234]) ).
fof(f239,plain,
( ~ sQ6_spl
| ~ sQ24_spl
| ~ animal(a_fox) ),
inference(resolution,[status(thm)],[f174,f94]) ).
fof(f242,plain,
( ~ sQ6_spl
| ~ sQ24_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f239,f176,f173,f93]) ).
fof(f258,plain,
( ~ sQ20_spl
| ~ snail(a_snail)
| ~ bird(a_bird) ),
inference(resolution,[status(thm)],[f157,f53]) ).
fof(f261,definition,
( sQ39_spl
<=> snail(a_snail) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( sQ39_spl
| ~ snail(a_snail) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f264,plain,
( ~ sQ20_spl
| ~ sQ39_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f258,f212,f261,f156]) ).
fof(f269,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f36]) ).
fof(f270,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f269]) ).
fof(f272,plain,
eats(a_snail,snail_food_of(a_snail)),
inference(resolution,[status(thm)],[f57,f36]) ).
fof(f273,plain,
! [X0] :
( ~ sQ27_spl
| ~ grain(X0)
| eats(a_wolf,X0) ),
inference(resolution,[status(thm)],[f186,f38]) ).
fof(f274,plain,
( ~ sQ27_spl
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[f273,f37]) ).
fof(f275,plain,
( ~ sQ27_spl
| ~ wolf(a_wolf) ),
inference(resolution,[status(thm)],[f274,f61]) ).
fof(f279,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f32]) ).
fof(f280,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f279]) ).
fof(f283,plain,
( ~ sQ28_spl
| ~ fox(a_fox)
| ~ wolf(a_wolf) ),
inference(resolution,[status(thm)],[f189,f49]) ).
fof(f298,definition,
( sQ45_spl
<=> wolf(a_wolf) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f300,plain,
( sQ45_spl
| ~ wolf(a_wolf) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f301,definition,
( sQ46_spl
<=> fox(a_fox) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f303,plain,
( sQ46_spl
| ~ fox(a_fox) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f304,plain,
( ~ sQ28_spl
| ~ sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f283,f298,f301,f188]) ).
fof(f306,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f32]) ).
fof(f307,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f306]) ).
fof(f308,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f303,f33]) ).
fof(f309,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f308]) ).
fof(f332,definition,
( sQ50_spl
<=> plant(caterpillar_food_of(a_caterpillar)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ50_spl
| ~ plant(caterpillar_food_of(a_caterpillar)) ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f350,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f147,f104]) ).
fof(f351,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f350]) ).
fof(f353,plain,
! [X0,X1] :
( ~ much_smaller(a_snail,X0)
| ~ plant(snail_food_of(a_snail))
| ~ animal(a_snail)
| ~ plant(X1)
| ~ animal(X0)
| eats(X0,a_snail)
| eats(X0,X1) ),
inference(resolution,[status(thm)],[f272,f40]) ).
fof(f356,definition,
! [X0,X1] :
( sQ55_spl
<=> ( ~ much_smaller(a_snail,X0)
| ~ plant(X1)
| ~ animal(X0)
| eats(X0,a_snail)
| eats(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f357,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ much_smaller(a_snail,X0)
| ~ plant(X1)
| ~ animal(X0)
| eats(X0,a_snail)
| eats(X0,X1) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( sQ56_spl
<=> plant(snail_food_of(a_snail)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( sQ56_spl
| ~ plant(snail_food_of(a_snail)) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( ~ sQ56_spl
| ~ sQ21_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f353,f356,f159,f359]) ).
fof(f406,plain,
( ~ sQ15_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f208,f98]) ).
fof(f407,plain,
( ~ sQ15_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f406]) ).
fof(f409,plain,
( sQ56_spl
| ~ snail(a_snail) ),
inference(resolution,[status(thm)],[f361,f56]) ).
fof(f411,plain,
( sQ56_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f409,f261,f359]) ).
fof(f416,plain,
! [X0] :
( ~ sQ55_spl
| ~ plant(X0)
| ~ animal(a_bird)
| eats(a_bird,a_snail)
| eats(a_bird,X0) ),
inference(resolution,[status(thm)],[f357,f152]) ).
fof(f417,plain,
( ~ sQ55_spl
| ~ sQ17_spl
| sQ20_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f416,f136,f156,f142,f356]) ).
fof(f429,plain,
( sQ50_spl
| ~ caterpillar(a_caterpillar) ),
inference(resolution,[status(thm)],[f334,f54]) ).
fof(f431,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f429,f35]) ).
fof(f432,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f431]) ).
fof(f433,plain,
( ~ sQ7_spl
| ~ sQ26_spl
| ~ plant(a_grain) ),
inference(resolution,[status(thm)],[f180,f97]) ).
fof(f435,plain,
( ~ sQ7_spl
| ~ sQ26_spl
| ~ grain(a_grain) ),
inference(resolution,[status(thm)],[f433,f38]) ).
fof(f436,plain,
( ~ sQ7_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f435,f37]) ).
fof(f437,plain,
( ~ sQ7_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f436]) ).
fof(f438,plain,
$false,
inference(sat_refutation,[status(thm)],[f99,f167,f182,f197,f199,f201,f227,f230,f235,f242,f264,f270,f280,f304,f307,f309,f351,f362,f407,f411,f417,f432,f437]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ031-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 03:47:02 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.42 % Elapsed time: 0.048584 seconds
% 0.14/0.42 % CPU time: 0.132578 seconds
% 0.14/0.42 % Total memory used: 17.654 MB
% 0.14/0.42 % Net memory used: 17.367 MB
%------------------------------------------------------------------------------