%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ031-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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 : Fri Sep 25 02:31:55 PM UTC 2026
% Result : Unsatisfiable 5.52s 11.27s
% Output : Proof 5.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 20
% Syntax : Number of formulae : 120 ( 30 unt; 0 def)
% Number of atoms : 317 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 391 ( 194 ~; 197 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-1 aty)
% Number of variables : 128 ( 0 sgn 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f12,axiom,
( ~ 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/sandbox2/benchmark/theBenchmark.p',eating_habits) ).
fof(f12_nnf,plain,
! [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) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [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) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( ~ 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(esa)],[f12_sk]) ).
cnf(f2,axiom,
( ~ bird(X)
| animal(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bird_is_an_animal) ).
fof(f2_nnf,plain,
! [X] :
( ~ bird(X)
| animal(X) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] :
( ~ bird(X)
| animal(X) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ bird(X0)
| animal(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f7,axiom,
bird(a_bird),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',there_is_a_bird) ).
fof(f7_nnf,plain,
bird(a_bird),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
bird(a_bird),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p34,plain,
animal(a_bird),
inference(resolution,[status(thm)],[c2,c7]) ).
cnf(p58,plain,
( ~ eats(X1,X2)
| ~ much_smaller(X1,a_bird)
| ~ plant(X2)
| ~ animal(X1)
| ~ plant(X0)
| eats(a_bird,X1)
| eats(a_bird,X0) ),
inference(resolution,[status(thm)],[c12,p34]) ).
cnf(f11,axiom,
( ~ grain(X)
| plant(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',grain_is_a_plant) ).
fof(f11_nnf,plain,
! [X] :
( ~ grain(X)
| plant(X) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] :
( ~ grain(X)
| plant(X) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ grain(X0)
| plant(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f10,axiom,
grain(a_grain),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',there_is_a_grain) ).
fof(f10_nnf,plain,
grain(a_grain),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
grain(a_grain),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p46,plain,
plant(a_grain),
inference(resolution,[status(thm)],[c11,c10]) ).
cnf(p150,plain,
( ~ eats(X0,X1)
| ~ much_smaller(X0,a_bird)
| ~ plant(X1)
| ~ animal(X0)
| eats(a_bird,X0)
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[p58,p46]) ).
cnf(f4,axiom,
( ~ snail(X)
| animal(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snail_is_an_animal) ).
fof(f4_nnf,plain,
! [X] :
( ~ snail(X)
| animal(X) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] :
( ~ snail(X)
| animal(X) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ~ snail(X0)
| animal(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f9,axiom,
snail(a_snail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',there_is_a_snail) ).
fof(f9_nnf,plain,
snail(a_snail),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
snail(a_snail),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p43,plain,
animal(a_snail),
inference(resolution,[status(thm)],[c4,c9]) ).
cnf(p284,plain,
( ~ eats(a_snail,X0)
| ~ much_smaller(a_snail,a_bird)
| ~ plant(X0)
| eats(a_bird,a_snail)
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[p150,p43]) ).
cnf(f23,axiom,
( ~ snail(Snail)
| plant(snail_food_of(Snail)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snail_food_is_a_plant) ).
fof(f23_nnf,plain,
! [Snail] :
( ~ snail(Snail)
| plant(snail_food_of(Snail)) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [Snail] :
( ~ snail(Snail)
| plant(snail_food_of(Snail)) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ snail(X0)
| plant(snail_food_of(X0)) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p111,plain,
plant(snail_food_of(a_snail)),
inference(resolution,[status(thm)],[c23,c9]) ).
cnf(p298,plain,
( ~ eats(a_snail,snail_food_of(a_snail))
| ~ much_smaller(a_snail,a_bird)
| eats(a_bird,a_snail)
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[p284,p111]) ).
cnf(f14,axiom,
( ~ bird(Bird)
| ~ snail(Snail)
| much_smaller(Snail,Bird) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snail_smaller_than_bird) ).
fof(f14_nnf,plain,
! [Snail,Bird] :
( ~ bird(Bird)
| ~ snail(Snail)
| much_smaller(Snail,Bird) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Snail,Bird] :
( ~ bird(Bird)
| ~ snail(Snail)
| much_smaller(Snail,Bird) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ~ bird(X1)
| ~ snail(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p66,plain,
( ~ bird(X0)
| much_smaller(a_snail,X0) ),
inference(resolution,[status(thm)],[c14,c9]) ).
cnf(p121,plain,
much_smaller(a_snail,a_bird),
inference(resolution,[status(thm)],[p66,c7]) ).
cnf(p304,plain,
( ~ eats(a_snail,snail_food_of(a_snail))
| eats(a_bird,a_snail)
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[p298,p121]) ).
cnf(f24,axiom,
( ~ snail(Snail)
| eats(Snail,snail_food_of(Snail)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snail_eats_snail_food) ).
fof(f24_nnf,plain,
! [Snail] :
( ~ snail(Snail)
| eats(Snail,snail_food_of(Snail)) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [Snail] :
( ~ snail(Snail)
| eats(Snail,snail_food_of(Snail)) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ~ snail(X0)
| eats(X0,snail_food_of(X0)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p112,plain,
eats(a_snail,snail_food_of(a_snail)),
inference(resolution,[status(thm)],[c24,c9]) ).
cnf(p305,plain,
( eats(a_bird,a_snail)
| eats(a_bird,a_grain) ),
inference(resolution,[status(thm)],[p304,p112]) ).
cnf(p55,plain,
( ~ eats(X2,X1)
| ~ much_smaller(X2,X0)
| ~ animal(X2)
| ~ plant(X1)
| ~ animal(X0)
| eats(X0,X2)
| eats(X0,X1) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(f1,axiom,
( ~ fox(X)
| animal(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fox_is_an_animal) ).
fof(f1_nnf,plain,
! [X] :
( ~ fox(X)
| animal(X) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] :
( ~ fox(X)
| animal(X) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ fox(X0)
| animal(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f6,axiom,
fox(a_fox),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',there_is_a_fox) ).
fof(f6_nnf,plain,
fox(a_fox),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
fox(a_fox),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p30,plain,
animal(a_fox),
inference(resolution,[status(thm)],[c1,c6]) ).
cnf(p131,plain,
( ~ eats(X1,X0)
| ~ much_smaller(X1,a_fox)
| ~ animal(X1)
| ~ plant(X0)
| eats(a_fox,X1)
| eats(a_fox,X0) ),
inference(resolution,[status(thm)],[p55,p30]) ).
cnf(p219,plain,
( ~ eats(X0,a_grain)
| ~ much_smaller(X0,a_fox)
| ~ animal(X0)
| eats(a_fox,X0)
| eats(a_fox,a_grain) ),
inference(resolution,[status(thm)],[p131,p46]) ).
cnf(p222,plain,
( ~ eats(a_bird,a_grain)
| ~ much_smaller(a_bird,a_fox)
| eats(a_fox,a_bird)
| eats(a_fox,a_grain) ),
inference(resolution,[status(thm)],[p219,p34]) ).
cnf(f15,axiom,
( ~ fox(Fox)
| ~ bird(Bird)
| much_smaller(Bird,Fox) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bird_smaller_than_fox) ).
fof(f15_nnf,plain,
! [Bird,Fox] :
( ~ fox(Fox)
| ~ bird(Bird)
| much_smaller(Bird,Fox) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Bird,Fox] :
( ~ fox(Fox)
| ~ bird(Bird)
| much_smaller(Bird,Fox) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ fox(X1)
| ~ bird(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p75,plain,
( ~ fox(X0)
| much_smaller(a_bird,X0) ),
inference(resolution,[status(thm)],[c15,c7]) ).
cnf(p122,plain,
much_smaller(a_bird,a_fox),
inference(resolution,[status(thm)],[p75,c6]) ).
cnf(p224,plain,
( ~ eats(a_bird,a_grain)
| eats(a_fox,a_bird)
| eats(a_fox,a_grain) ),
inference(resolution,[status(thm)],[p222,p122]) ).
cnf(p306,plain,
( eats(a_fox,a_bird)
| eats(a_fox,a_grain)
| eats(a_bird,a_snail) ),
inference(resolution,[status(thm)],[p305,p224]) ).
cnf(f20,axiom,
( ~ eats(Bird,Snail)
| ~ snail(Snail)
| ~ bird(Bird) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bird_dont_eat_snail) ).
fof(f20_nnf,plain,
! [Bird,Snail] :
( ~ eats(Bird,Snail)
| ~ snail(Snail)
| ~ bird(Bird) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [Bird,Snail] :
( ~ eats(Bird,Snail)
| ~ snail(Snail)
| ~ bird(Bird) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( ~ eats(X0,X1)
| ~ snail(X1)
| ~ bird(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p99,plain,
( ~ eats(a_bird,X0)
| ~ snail(X0) ),
inference(resolution,[status(thm)],[c20,c7]) ).
cnf(p141,plain,
~ eats(a_bird,a_snail),
inference(resolution,[status(thm)],[p99,c9]) ).
cnf(p311,plain,
( eats(a_fox,a_bird)
| eats(a_fox,a_grain) ),
inference(resolution,[status(thm)],[p306,p141]) ).
cnf(f0,axiom,
( ~ wolf(X)
| animal(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wolf_is_an_animal) ).
fof(f0_nnf,plain,
! [X] :
( ~ wolf(X)
| animal(X) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] :
( ~ wolf(X)
| animal(X) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ wolf(X0)
| animal(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f5,axiom,
wolf(a_wolf),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',there_is_a_wolf) ).
fof(f5_nnf,plain,
wolf(a_wolf),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
wolf(a_wolf),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p29,plain,
animal(a_wolf),
inference(resolution,[status(thm)],[c0,c5]) ).
cnf(p130,plain,
( ~ eats(X1,X0)
| ~ much_smaller(X1,a_wolf)
| ~ animal(X1)
| ~ plant(X0)
| eats(a_wolf,X1)
| eats(a_wolf,X0) ),
inference(resolution,[status(thm)],[p55,p29]) ).
cnf(p212,plain,
( ~ eats(X0,a_grain)
| ~ much_smaller(X0,a_wolf)
| ~ animal(X0)
| eats(a_wolf,X0)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p130,p46]) ).
cnf(p215,plain,
( ~ eats(a_fox,a_grain)
| ~ much_smaller(a_fox,a_wolf)
| eats(a_wolf,a_fox)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p212,p30]) ).
cnf(f16,axiom,
( ~ wolf(Wolf)
| ~ fox(Fox)
| much_smaller(Fox,Wolf) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fox_smaller_than_wolf) ).
fof(f16_nnf,plain,
! [Fox,Wolf] :
( ~ wolf(Wolf)
| ~ fox(Fox)
| much_smaller(Fox,Wolf) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Fox,Wolf] :
( ~ wolf(Wolf)
| ~ fox(Fox)
| much_smaller(Fox,Wolf) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( ~ wolf(X1)
| ~ fox(X0)
| much_smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p78,plain,
( ~ wolf(X0)
| much_smaller(a_fox,X0) ),
inference(resolution,[status(thm)],[c16,c6]) ).
cnf(p128,plain,
much_smaller(a_fox,a_wolf),
inference(resolution,[status(thm)],[p78,c5]) ).
cnf(p218,plain,
( ~ eats(a_fox,a_grain)
| eats(a_wolf,a_fox)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p215,p128]) ).
cnf(p312,plain,
( eats(a_wolf,a_fox)
| eats(a_wolf,a_grain)
| eats(a_fox,a_bird) ),
inference(resolution,[status(thm)],[p311,p218]) ).
cnf(f25,negated_conjecture,
( ~ eats(Grain_eater,Grain)
| ~ eats(Animal,Grain_eater)
| ~ grain(Grain)
| ~ animal(Grain_eater)
| ~ animal(Animal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_the_animal_exists) ).
fof(f25_nnf,plain,
! [Animal,Grain_eater,Grain] :
( ~ eats(Grain_eater,Grain)
| ~ eats(Animal,Grain_eater)
| ~ grain(Grain)
| ~ animal(Grain_eater)
| ~ animal(Animal) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [Animal,Grain_eater,Grain] :
( ~ eats(Grain_eater,Grain)
| ~ eats(Animal,Grain_eater)
| ~ grain(Grain)
| ~ animal(Grain_eater)
| ~ animal(Animal) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( ~ eats(X1,X2)
| ~ eats(X0,X1)
| ~ grain(X2)
| ~ animal(X1)
| ~ animal(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p36,plain,
( ~ eats(X0,X1)
| ~ eats(a_fox,X0)
| ~ grain(X1)
| ~ animal(X0) ),
inference(resolution,[status(thm)],[p30,c25]) ).
cnf(p51,plain,
( ~ eats(a_bird,X0)
| ~ eats(a_fox,a_bird)
| ~ grain(X0) ),
inference(resolution,[status(thm)],[p34,p36]) ).
cnf(p60,plain,
( ~ eats(a_bird,a_grain)
| ~ eats(a_fox,a_bird) ),
inference(resolution,[status(thm)],[p51,c10]) ).
cnf(p313,plain,
( ~ eats(a_bird,a_grain)
| eats(a_wolf,a_fox)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p312,p60]) ).
cnf(p314,plain,
( eats(a_bird,a_snail)
| eats(a_wolf,a_fox)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p313,p305]) ).
cnf(p319,plain,
( eats(a_wolf,a_fox)
| eats(a_wolf,a_grain) ),
inference(resolution,[status(thm)],[p314,p141]) ).
cnf(f18,axiom,
( ~ eats(Wolf,Grain)
| ~ grain(Grain)
| ~ wolf(Wolf) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wolf_dont_eat_grain) ).
fof(f18_nnf,plain,
! [Wolf,Grain] :
( ~ eats(Wolf,Grain)
| ~ grain(Grain)
| ~ wolf(Wolf) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [Wolf,Grain] :
( ~ eats(Wolf,Grain)
| ~ grain(Grain)
| ~ wolf(Wolf) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( ~ eats(X0,X1)
| ~ grain(X1)
| ~ wolf(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p86,plain,
( ~ eats(a_wolf,X0)
| ~ grain(X0) ),
inference(resolution,[status(thm)],[c18,c5]) ).
cnf(p135,plain,
~ eats(a_wolf,a_grain),
inference(resolution,[status(thm)],[p86,c10]) ).
cnf(p320,plain,
eats(a_wolf,a_fox),
inference(resolution,[status(thm)],[p319,p135]) ).
cnf(f17,axiom,
( ~ eats(Wolf,Fox)
| ~ fox(Fox)
| ~ wolf(Wolf) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wolf_dont_eat_fox) ).
fof(f17_nnf,plain,
! [Wolf,Fox] :
( ~ eats(Wolf,Fox)
| ~ fox(Fox)
| ~ wolf(Wolf) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [Wolf,Fox] :
( ~ eats(Wolf,Fox)
| ~ fox(Fox)
| ~ wolf(Wolf) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( ~ eats(X0,X1)
| ~ fox(X1)
| ~ wolf(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p83,plain,
( ~ eats(a_wolf,X0)
| ~ fox(X0) ),
inference(resolution,[status(thm)],[c17,c5]) ).
cnf(p129,plain,
~ eats(a_wolf,a_fox),
inference(resolution,[status(thm)],[p83,c6]) ).
cnf(p321,plain,
$false,
inference(resolution,[status(thm)],[p320,p129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ031-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/10.38 % Computer : n016.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Thu Sep 24 06:47:38 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.52/11.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.52/11.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------