%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ031^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 : Wed Sep 30 08:21:00 AM UTC 2026
% Result : Theorem 0.19s 0.29s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ031^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n026.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 13:24:12 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.29 % (572921)Will run a generic schedule for satisfiability detection.
% 0.19/0.29 % (572927)% WARNING: option uhcvi not known.
% 0.19/0.29 % (572927)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1638631330:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.29 % (572927)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.19/0.29 % (572927)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.19/0.29 % (572926)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3878276594_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.29 % (572929)dis+10_1_sil=32000:sp=arity:random_seed=1848786446:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.29 % (572928)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1112634509:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.29 % (572931)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=556379185:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.29 % (572930)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4208347107:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.29 % (572932)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1234263093:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.29 % Exception at run slice level
% 0.19/0.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.19/0.29 % (572930)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.19/0.29 % (572940)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=996144906:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.29 % Exception at run slice level
% 0.19/0.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.19/0.29 % (572942)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=182205985:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.29 % (572927) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-572921-572927"...
% 0.19/0.29 % (572927)...printing done.
% 0.19/0.29 % (572927)Refutation found. Thanks to Tanya!
% 0.19/0.29 % SZS status Theorem for theBenchmark
% 0.19/0.29 % SZS output start Proof for theBenchmark
% 0.19/0.29 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.19/0.29 thf(func_def_0, type, eats: ($i > $i > $o)).
% 0.19/0.29 thf(func_def_1, type, grain: ($i > $o)).
% 0.19/0.29 thf(func_def_2, type, animal: ($i > $o)).
% 0.19/0.29 thf(func_def_3, type, snail: ($i > $o)).
% 0.19/0.29 thf(func_def_4, type, sf: ($i > $i)).
% 0.19/0.29 thf(func_def_5, type, plant: ($i > $o)).
% 0.19/0.29 thf(func_def_6, type, caterpillar: ($i > $o)).
% 0.19/0.29 thf(func_def_7, type, cf: ($i > $i)).
% 0.19/0.29 thf(func_def_8, type, bird: ($i > $o)).
% 0.19/0.29 thf(func_def_9, type, wolf: ($i > $o)).
% 0.19/0.29 thf(func_def_10, type, fox: ($i > $o)).
% 0.19/0.29 thf(func_def_11, type, msmaller: ($i > $i > $o)).
% 0.19/0.29 thf(f1,conjecture,(
% 0.19/0.29 ~(! [X1 : $i,X10 : $i,X9 : $i] : (~(eats @ X10 @ X9) | ~(eats @ X1 @ X10) | ~(grain @ X9) | ~(animal @ X10) | ~(animal @ X1)) & ! [X3 : $i] : (~(snail @ X3) | (eats @ X3 @ (sf @ X3))) & ! [X3 : $i] : (~(snail @ X3) | (plant @ (sf @ X3))) & ! [X5 : $i] : (~(caterpillar @ X5) | (eats @ X5 @ (cf @ X5))) & ! [X5 : $i] : (~(caterpillar @ X5) | (plant @ (cf @ X5))) & ! [X6 : $i,X3 : $i] : (~(eats @ X6 @ X3) | ~(snail @ X3) | ~(bird @ X6)) & ! [X6 : $i,X5 : $i] : (~(caterpillar @ X5) | ~(bird @ X6) | (eats @ X6 @ X5)) & ! [X8 : $i,X9 : $i] : (~(eats @ X8 @ X9) | ~(grain @ X9) | ~(wolf @ X8)) & ! [X7 : $i,X8 : $i] : (~(eats @ X8 @ X7) | ~(fox @ X7) | ~(wolf @ X8)) & ! [X7 : $i,X8 : $i] : (~(wolf @ X8) | ~(fox @ X7) | (msmaller @ X7 @ X8)) & ! [X6 : $i,X7 : $i] : (~(fox @ X7) | ~(bird @ X6) | (msmaller @ X6 @ X7)) & ! [X3 : $i,X6 : $i] : (~(bird @ X6) | ~(snail @ X3) | (msmaller @ X3 @ X6)) & ! [X5 : $i,X6 : $i] : (~(bird @ X6) | ~(caterpillar @ X5) | (msmaller @ X5 @ X6)) & ! [X1 : $i,X2 : $i,X3 : $i,X4 : $i] : (~(eats @ X3 @ X4) | ~(msmaller @ X3 @ X1) | ~(plant @ X4) | ~(animal @ X3) | ~(plant @ X2) | ~(animal @ X1) | (eats @ X1 @ X3) | (eats @ X1 @ X2)) & ! [X0 : $i] : (~(grain @ X0) | (plant @ X0)) & (grain @ a_grain) & (snail @ a_snail) & (caterpillar @ a_caterpillar) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X0 : $i] : (~(snail @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(caterpillar @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(bird @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(fox @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(wolf @ X0) | (animal @ X0)))),
% 0.19/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cPUZ031_1)).
% 0.19/0.29 thf(f2,negated_conjecture,(
% 0.19/0.29 ~ ~(! [X1 : $i,X10 : $i,X9 : $i] : (~(eats @ X10 @ X9) | ~(eats @ X1 @ X10) | ~(grain @ X9) | ~(animal @ X10) | ~(animal @ X1)) & ! [X3 : $i] : (~(snail @ X3) | (eats @ X3 @ (sf @ X3))) & ! [X3 : $i] : (~(snail @ X3) | (plant @ (sf @ X3))) & ! [X5 : $i] : (~(caterpillar @ X5) | (eats @ X5 @ (cf @ X5))) & ! [X5 : $i] : (~(caterpillar @ X5) | (plant @ (cf @ X5))) & ! [X6 : $i,X3 : $i] : (~(eats @ X6 @ X3) | ~(snail @ X3) | ~(bird @ X6)) & ! [X6 : $i,X5 : $i] : (~(caterpillar @ X5) | ~(bird @ X6) | (eats @ X6 @ X5)) & ! [X8 : $i,X9 : $i] : (~(eats @ X8 @ X9) | ~(grain @ X9) | ~(wolf @ X8)) & ! [X7 : $i,X8 : $i] : (~(eats @ X8 @ X7) | ~(fox @ X7) | ~(wolf @ X8)) & ! [X7 : $i,X8 : $i] : (~(wolf @ X8) | ~(fox @ X7) | (msmaller @ X7 @ X8)) & ! [X6 : $i,X7 : $i] : (~(fox @ X7) | ~(bird @ X6) | (msmaller @ X6 @ X7)) & ! [X3 : $i,X6 : $i] : (~(bird @ X6) | ~(snail @ X3) | (msmaller @ X3 @ X6)) & ! [X5 : $i,X6 : $i] : (~(bird @ X6) | ~(caterpillar @ X5) | (msmaller @ X5 @ X6)) & ! [X1 : $i,X2 : $i,X3 : $i,X4 : $i] : (~(eats @ X3 @ X4) | ~(msmaller @ X3 @ X1) | ~(plant @ X4) | ~(animal @ X3) | ~(plant @ X2) | ~(animal @ X1) | (eats @ X1 @ X3) | (eats @ X1 @ X2)) & ! [X0 : $i] : (~(grain @ X0) | (plant @ X0)) & (grain @ a_grain) & (snail @ a_snail) & (caterpillar @ a_caterpillar) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X0 : $i] : (~(snail @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(caterpillar @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(bird @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(fox @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(wolf @ X0) | (animal @ X0)))),
% 0.19/0.29 inference(negated_conjecture,[status(cth)],[f1])).
% 0.19/0.29 thf(f3,plain,(
% 0.19/0.29 ~ ~(! [X0 : $i,X1 : $i,X2 : $i] : (~(eats @ X1 @ X2) | ~(eats @ X0 @ X1) | ~(grain @ X2) | ~(animal @ X1) | ~(animal @ X0)) & ! [X3 : $i] : (~(snail @ X3) | (eats @ X3 @ (sf @ X3))) & ! [X4 : $i] : (~(snail @ X4) | (plant @ (sf @ X4))) & ! [X5 : $i] : (~(caterpillar @ X5) | (eats @ X5 @ (cf @ X5))) & ! [X6 : $i] : (~(caterpillar @ X6) | (plant @ (cf @ X6))) & ! [X7 : $i,X8 : $i] : (~(eats @ X7 @ X8) | ~(snail @ X8) | ~(bird @ X7)) & ! [X9 : $i,X10 : $i] : (~(caterpillar @ X10) | ~(bird @ X9) | (eats @ X9 @ X10)) & ! [X11 : $i,X12 : $i] : (~(eats @ X11 @ X12) | ~(grain @ X12) | ~(wolf @ X11)) & ! [X13 : $i,X14 : $i] : (~(eats @ X14 @ X13) | ~(fox @ X13) | ~(wolf @ X14)) & ! [X15 : $i,X16 : $i] : (~(wolf @ X16) | ~(fox @ X15) | (msmaller @ X15 @ X16)) & ! [X17 : $i,X18 : $i] : (~(fox @ X18) | ~(bird @ X17) | (msmaller @ X17 @ X18)) & ! [X19 : $i,X20 : $i] : (~(bird @ X20) | ~(snail @ X19) | (msmaller @ X19 @ X20)) & ! [X21 : $i,X22 : $i] : (~(bird @ X22) | ~(caterpillar @ X21) | (msmaller @ X21 @ X22)) & ! [X23 : $i,X24 : $i,X25 : $i,X26 : $i] : (~(eats @ X25 @ X26) | ~(msmaller @ X25 @ X23) | ~(plant @ X26) | ~(animal @ X25) | ~(plant @ X24) | ~(animal @ X23) | (eats @ X23 @ X25) | (eats @ X23 @ X24)) & ! [X27 : $i] : (~(grain @ X27) | (plant @ X27)) & (grain @ a_grain) & (snail @ a_snail) & (caterpillar @ a_caterpillar) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X28 : $i] : (~(snail @ X28) | (animal @ X28)) & ! [X29 : $i] : (~(caterpillar @ X29) | (animal @ X29)) & ! [X30 : $i] : (~(bird @ X30) | (animal @ X30)) & ! [X31 : $i] : (~(fox @ X31) | (animal @ X31)) & ! [X32 : $i] : (~(wolf @ X32) | (animal @ X32)))),
% 0.19/0.29 inference(rectify,[],[f2])).
% 0.19/0.29 thf(f4,plain,(
% 0.19/0.29 ~ ~(! [X0 : $i,X1 : $i,X2 : $i] : (~ (((eats @ X1 @ X2)) = $true) | ~ (((eats @ X0 @ X1)) = $true) | ~ (((grain @ X2)) = $true) | ~ (((animal @ X1)) = $true) | ~ (((animal @ X0)) = $true)) & ! [X3 : $i] : (~ (((snail @ X3)) = $true) | (((eats @ X3 @ (sf @ X3))) = $true)) & ! [X4 : $i] : (~ (((snail @ X4)) = $true) | (((plant @ (sf @ X4))) = $true)) & ! [X5 : $i] : (~ (((caterpillar @ X5)) = $true) | (((eats @ X5 @ (cf @ X5))) = $true)) & ! [X6 : $i] : (~ (((caterpillar @ X6)) = $true) | (((plant @ (cf @ X6))) = $true)) & ! [X7 : $i,X8 : $i] : (~ (((eats @ X7 @ X8)) = $true) | ~ (((snail @ X8)) = $true) | ~ (((bird @ X7)) = $true)) & ! [X9 : $i,X10 : $i] : (~ (((caterpillar @ X10)) = $true) | ~ (((bird @ X9)) = $true) | (((eats @ X9 @ X10)) = $true)) & ! [X11 : $i,X12 : $i] : (~ (((eats @ X11 @ X12)) = $true) | ~ (((grain @ X12)) = $true) | ~ (((wolf @ X11)) = $true)) & ! [X13 : $i,X14 : $i] : (~ (((eats @ X14 @ X13)) = $true) | ~ (((fox @ X13)) = $true) | ~ (((wolf @ X14)) = $true)) & ! [X15 : $i,X16 : $i] : (~ (((wolf @ X16)) = $true) | ~ (((fox @ X15)) = $true) | (((msmaller @ X15 @ X16)) = $true)) & ! [X17 : $i,X18 : $i] : (~ (((fox @ X18)) = $true) | ~ (((bird @ X17)) = $true) | (((msmaller @ X17 @ X18)) = $true)) & ! [X19 : $i,X20 : $i] : (~ (((bird @ X20)) = $true) | ~ (((snail @ X19)) = $true) | (((msmaller @ X19 @ X20)) = $true)) & ! [X21 : $i,X22 : $i] : (~ (((bird @ X22)) = $true) | ~ (((caterpillar @ X21)) = $true) | (((msmaller @ X21 @ X22)) = $true)) & ! [X23 : $i,X24 : $i,X25 : $i,X26 : $i] : (~ (((eats @ X25 @ X26)) = $true) | ~ (((msmaller @ X25 @ X23)) = $true) | ~ (((plant @ X26)) = $true) | ~ (((animal @ X25)) = $true) | ~ (((plant @ X24)) = $true) | ~ (((animal @ X23)) = $true) | (((eats @ X23 @ X25)) = $true) | (((eats @ X23 @ X24)) = $true)) & ! [X27 : $i] : (~ (((grain @ X27)) = $true) | (((plant @ X27)) = $true)) & (((grain @ a_grain)) = $true) & (((snail @ a_snail)) = $true) & (((caterpillar @ a_caterpillar)) = $true) & (((bird @ a_bird)) = $true) & (((fox @ a_fox)) = $true) & (((wolf @ a_wolf)) = $true) & ! [X28 : $i] : (~ (((snail @ X28)) = $true) | (((animal @ X28)) = $true)) & ! [X29 : $i] : (~ (((caterpillar @ X29)) = $true) | (((animal @ X29)) = $true)) & ! [X30 : $i] : (~ (((bird @ X30)) = $true) | (((animal @ X30)) = $true)) & ! [X31 : $i] : (~ (((fox @ X31)) = $true) | (((animal @ X31)) = $true)) & ! [X32 : $i] : (~ (((wolf @ X32)) = $true) | (((animal @ X32)) = $true)))),
% 0.19/0.29 inference(fool_elimination,[],[f3])).
% 0.19/0.29 thf(f5,plain,(
% 0.19/0.29 ! [X0 : $i,X1 : $i,X2 : $i] : ((((eats @ X1 @ X2)) != $true) | (((eats @ X0 @ X1)) != $true) | (((grain @ X2)) != $true) | (((animal @ X1)) != $true) | (((animal @ X0)) != $true)) & ! [X3 : $i] : ((((snail @ X3)) != $true) | (((eats @ X3 @ (sf @ X3))) = $true)) & ! [X4 : $i] : ((((snail @ X4)) != $true) | (((plant @ (sf @ X4))) = $true)) & ! [X5 : $i] : ((((caterpillar @ X5)) != $true) | (((eats @ X5 @ (cf @ X5))) = $true)) & ! [X6 : $i] : ((((caterpillar @ X6)) != $true) | (((plant @ (cf @ X6))) = $true)) & ! [X7 : $i,X8 : $i] : ((((eats @ X7 @ X8)) != $true) | (((snail @ X8)) != $true) | (((bird @ X7)) != $true)) & ! [X9 : $i,X10 : $i] : ((((caterpillar @ X10)) != $true) | (((bird @ X9)) != $true) | (((eats @ X9 @ X10)) = $true)) & ! [X11 : $i,X12 : $i] : ((((eats @ X11 @ X12)) != $true) | (((grain @ X12)) != $true) | (((wolf @ X11)) != $true)) & ! [X13 : $i,X14 : $i] : ((((eats @ X14 @ X13)) != $true) | (((fox @ X13)) != $true) | (((wolf @ X14)) != $true)) & ! [X15 : $i,X16 : $i] : ((((wolf @ X16)) != $true) | (((fox @ X15)) != $true) | (((msmaller @ X15 @ X16)) = $true)) & ! [X17 : $i,X18 : $i] : ((((fox @ X18)) != $true) | (((bird @ X17)) != $true) | (((msmaller @ X17 @ X18)) = $true)) & ! [X19 : $i,X20 : $i] : ((((bird @ X20)) != $true) | (((snail @ X19)) != $true) | (((msmaller @ X19 @ X20)) = $true)) & ! [X21 : $i,X22 : $i] : ((((bird @ X22)) != $true) | (((caterpillar @ X21)) != $true) | (((msmaller @ X21 @ X22)) = $true)) & ! [X23 : $i,X24 : $i,X25 : $i,X26 : $i] : ((((eats @ X25 @ X26)) != $true) | (((msmaller @ X25 @ X23)) != $true) | (((plant @ X26)) != $true) | (((animal @ X25)) != $true) | (((plant @ X24)) != $true) | (((animal @ X23)) != $true) | (((eats @ X23 @ X25)) = $true) | (((eats @ X23 @ X24)) = $true)) & ! [X27 : $i] : ((((grain @ X27)) != $true) | (((plant @ X27)) = $true)) & (((grain @ a_grain)) = $true) & (((snail @ a_snail)) = $true) & (((caterpillar @ a_caterpillar)) = $true) & (((bird @ a_bird)) = $true) & (((fox @ a_fox)) = $true) & (((wolf @ a_wolf)) = $true) & ! [X28 : $i] : ((((snail @ X28)) != $true) | (((animal @ X28)) = $true)) & ! [X29 : $i] : ((((caterpillar @ X29)) != $true) | (((animal @ X29)) = $true)) & ! [X30 : $i] : ((((bird @ X30)) != $true) | (((animal @ X30)) = $true)) & ! [X31 : $i] : ((((fox @ X31)) != $true) | (((animal @ X31)) = $true)) & ! [X32 : $i] : ((((wolf @ X32)) != $true) | (((animal @ X32)) = $true))),
% 0.19/0.29 inference(flattening,[],[f4])).
% 0.19/0.29 thf(f6,plain,(
% 0.19/0.29 ( ! [X32 : $i] : ((((wolf @ X32)) != $true) | (((animal @ X32)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f7,plain,(
% 0.19/0.29 ( ! [X31 : $i] : ((((fox @ X31)) != $true) | (((animal @ X31)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f8,plain,(
% 0.19/0.29 ( ! [X30 : $i] : ((((bird @ X30)) != $true) | (((animal @ X30)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f10,plain,(
% 0.19/0.29 ( ! [X28 : $i] : ((((snail @ X28)) != $true) | (((animal @ X28)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f11,plain,(
% 0.19/0.29 (((wolf @ a_wolf)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f12,plain,(
% 0.19/0.29 (((fox @ a_fox)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f13,plain,(
% 0.19/0.29 (((bird @ a_bird)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f14,plain,(
% 0.19/0.29 (((caterpillar @ a_caterpillar)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f15,plain,(
% 0.19/0.29 (((snail @ a_snail)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f16,plain,(
% 0.19/0.29 (((grain @ a_grain)) = $true)),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f17,plain,(
% 0.19/0.29 ( ! [X27 : $i] : ((((grain @ X27)) != $true) | (((plant @ X27)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f18,plain,(
% 0.19/0.29 ( ! [X26 : $i,X24 : $i,X25 : $i,X23 : $i] : ((((msmaller @ X25 @ X23)) != $true) | (((eats @ X25 @ X26)) != $true) | (((plant @ X26)) != $true) | (((animal @ X25)) != $true) | (((plant @ X24)) != $true) | (((animal @ X23)) != $true) | (((eats @ X23 @ X25)) = $true) | (((eats @ X23 @ X24)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f20,plain,(
% 0.19/0.29 ( ! [X19 : $i,X20 : $i] : ((((bird @ X20)) != $true) | (((snail @ X19)) != $true) | (((msmaller @ X19 @ X20)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f21,plain,(
% 0.19/0.29 ( ! [X18 : $i,X17 : $i] : ((((fox @ X18)) != $true) | (((bird @ X17)) != $true) | (((msmaller @ X17 @ X18)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f22,plain,(
% 0.19/0.29 ( ! [X16 : $i,X15 : $i] : ((((fox @ X15)) != $true) | (((wolf @ X16)) != $true) | (((msmaller @ X15 @ X16)) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f23,plain,(
% 0.19/0.29 ( ! [X14 : $i,X13 : $i] : ((((eats @ X14 @ X13)) != $true) | (((fox @ X13)) != $true) | (((wolf @ X14)) != $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f24,plain,(
% 0.19/0.29 ( ! [X11 : $i,X12 : $i] : ((((eats @ X11 @ X12)) != $true) | (((grain @ X12)) != $true) | (((wolf @ X11)) != $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f26,plain,(
% 0.19/0.29 ( ! [X8 : $i,X7 : $i] : ((((eats @ X7 @ X8)) != $true) | (((snail @ X8)) != $true) | (((bird @ X7)) != $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f27,plain,(
% 0.19/0.29 ( ! [X6 : $i] : ((((caterpillar @ X6)) != $true) | (((plant @ (cf @ X6))) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f29,plain,(
% 0.19/0.29 ( ! [X4 : $i] : ((((snail @ X4)) != $true) | (((plant @ (sf @ X4))) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f30,plain,(
% 0.19/0.29 ( ! [X3 : $i] : ((((snail @ X3)) != $true) | (((eats @ X3 @ (sf @ X3))) = $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f31,plain,(
% 0.19/0.29 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((eats @ X1 @ X2)) != $true) | (((eats @ X0 @ X1)) != $true) | (((grain @ X2)) != $true) | (((animal @ X1)) != $true) | (((animal @ X0)) != $true)) )),
% 0.19/0.29 inference(cnf_transformation,[],[f5])).
% 0.19/0.29 thf(f33,definition,(
% 0.19/0.29 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.19/0.29 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.19/0.29 thf(f34,plain,(
% 0.19/0.29 ($true != $true) | ($true = ((animal @ a_wolf)))),
% 0.19/0.29 inference(constrained_superposition,[],[f6,f11])).
% 0.19/0.29 thf(f35,plain,(
% 0.19/0.29 ($true = ((animal @ a_wolf)))),
% 0.19/0.29 inference(trivial_inequality_removal,[],[f34])).
% 0.19/0.29 thf(f36,plain,(
% 0.19/0.29 ($true != $true) | ($true = ((animal @ a_fox)))),
% 0.19/0.29 inference(constrained_superposition,[],[f7,f12])).
% 0.19/0.29 thf(f37,plain,(
% 0.19/0.29 ($true = ((animal @ a_fox)))),
% 0.19/0.29 inference(trivial_inequality_removal,[],[f36])).
% 0.19/0.29 thf(f38,plain,(
% 0.19/0.29 ($true != $true) | ($true = ((animal @ a_bird)))),
% 0.19/0.29 inference(constrained_superposition,[],[f8,f13])).
% 0.19/0.29 thf(f39,plain,(
% 0.19/0.29 ($true = ((animal @ a_bird)))),
% 0.19/0.29 inference(trivial_inequality_removal,[],[f38])).
% 0.19/0.29 thf(f42,plain,(
% 0.19/0.29 ($true != $true) | ($true = ((animal @ a_snail)))),
% 0.19/0.29 inference(constrained_superposition,[],[f10,f15])).
% 0.19/0.29 thf(f43,plain,(
% 0.19/0.29 ($true = ((animal @ a_snail)))),
% 0.19/0.29 inference(trivial_inequality_removal,[],[f42])).
% 0.19/0.29 thf(f44,plain,(
% 0.19/0.29 ($true != $true) | ($true = ((plant @ a_grain)))),
% 0.19/0.29 inference(constrained_superposition,[],[f17,f16])).
% 0.19/0.29 thf(f45,plain,(
% 0.19/0.29 ($true = ((plant @ a_grain)))),
% 0.19/0.29 inference(trivial_inequality_removal,[],[f44])).
% 0.19/0.29 thf(f46,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((plant @ (cf @ a_caterpillar))))),
% 0.19/0.30 inference(constrained_superposition,[],[f27,f14])).
% 0.19/0.30 thf(f47,plain,(
% 0.19/0.30 ($true = ((plant @ (cf @ a_caterpillar))))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f46])).
% 0.19/0.30 thf(f48,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((plant @ (sf @ a_snail))))),
% 0.19/0.30 inference(constrained_superposition,[],[f29,f15])).
% 0.19/0.30 thf(f49,plain,(
% 0.19/0.30 ($true = ((plant @ (sf @ a_snail))))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f48])).
% 0.19/0.30 thf(f52,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((eats @ a_snail @ (sf @ a_snail))))),
% 0.19/0.30 inference(constrained_superposition,[],[f30,f15])).
% 0.19/0.30 thf(f53,plain,(
% 0.19/0.30 ($true = ((eats @ a_snail @ (sf @ a_snail))))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f52])).
% 0.19/0.30 thf(f56,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | (((snail @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_bird)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f20,f13])).
% 0.19/0.30 thf(f57,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((snail @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_bird)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f56])).
% 0.19/0.30 thf(f58,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | (((bird @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_fox)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f21,f12])).
% 0.19/0.30 thf(f59,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((bird @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_fox)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f58])).
% 0.19/0.30 thf(f60,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | (((wolf @ X0)) != $true) | ($true = ((msmaller @ a_fox @ X0)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f22,f12])).
% 0.19/0.30 thf(f61,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((wolf @ X0)) != $true) | ($true = ((msmaller @ a_fox @ X0)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f60])).
% 0.19/0.30 thf(f82,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((snail @ X1))) | (((bird @ X0)) != $true) | (((eats @ X0 @ X1)) = $false)) )),
% 0.19/0.30 inference(constrained_superposition,[],[f26,f33])).
% 0.19/0.30 thf(f83,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((grain @ X1))) | (((wolf @ X0)) != $true) | (((eats @ X0 @ X1)) = $false)) )),
% 0.19/0.30 inference(constrained_superposition,[],[f24,f33])).
% 0.19/0.30 thf(f87,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((grain @ X1))) | (((wolf @ X0)) != $true) | (((eats @ X0 @ X1)) = $false)) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f83])).
% 0.19/0.30 thf(f88,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((snail @ X1))) | (((bird @ X0)) != $true) | (((eats @ X0 @ X1)) = $false)) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f82])).
% 0.19/0.30 thf(f248,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((msmaller @ a_snail @ a_bird)))),
% 0.19/0.30 inference(constrained_superposition,[],[f57,f15])).
% 0.19/0.30 thf(f252,plain,(
% 0.19/0.30 ($true = ((msmaller @ a_snail @ a_bird)))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f248])).
% 0.19/0.30 thf(f253,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((msmaller @ a_bird @ a_fox)))),
% 0.19/0.30 inference(constrained_superposition,[],[f59,f13])).
% 0.19/0.30 thf(f257,plain,(
% 0.19/0.30 ($true = ((msmaller @ a_bird @ a_fox)))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f253])).
% 0.19/0.30 thf(f258,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((msmaller @ a_fox @ a_wolf)))),
% 0.19/0.30 inference(constrained_superposition,[],[f61,f11])).
% 0.19/0.30 thf(f262,plain,(
% 0.19/0.30 ($true = ((msmaller @ a_fox @ a_wolf)))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f258])).
% 0.19/0.30 thf(f294,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | (((wolf @ X0)) != $true) | ($false = ((eats @ X0 @ a_grain)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f87,f16])).
% 0.19/0.30 thf(f298,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((wolf @ X0)) != $true) | ($false = ((eats @ X0 @ a_grain)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f294])).
% 0.19/0.30 thf(f302,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | (((bird @ X0)) != $true) | ($false = ((eats @ X0 @ a_snail)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f88,f15])).
% 0.19/0.30 thf(f306,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((bird @ X0)) != $true) | ($false = ((eats @ X0 @ a_snail)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f302])).
% 0.19/0.30 thf(f417,definition,(
% 0.19/0.30 spl0_18 <=> ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_bird @ X1))))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition])).
% 0.19/0.30 thf(f418,plain,(
% 0.19/0.30 ( ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_bird @ X1)))) ) | ~spl0_18),
% 0.19/0.30 inference(avatar_component_clause,[],[f417])).
% 0.19/0.30 thf(f423,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_snail))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_bird))) | ($true = ((eats @ a_bird @ a_snail))) | ($true = ((eats @ a_bird @ X1)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f18,f252])).
% 0.19/0.30 thf(f424,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_snail))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_bird))) | ($true = ((eats @ a_bird @ a_snail))) | ($true = ((eats @ a_bird @ X1)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f423])).
% 0.19/0.30 thf(f425,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true != ((animal @ a_bird))) | ($true = ((eats @ a_bird @ a_snail))) | ($true = ((eats @ a_bird @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f424,f43])).
% 0.19/0.30 thf(f426,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true = ((eats @ a_bird @ a_snail))) | ($true = ((eats @ a_bird @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f425,f39])).
% 0.19/0.30 thf(f428,definition,(
% 0.19/0.30 spl0_20 <=> ($true = ((eats @ a_bird @ a_snail)))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition])).
% 0.19/0.30 thf(f430,plain,(
% 0.19/0.30 ($true = ((eats @ a_bird @ a_snail))) | ~spl0_20),
% 0.19/0.30 inference(avatar_component_clause,[],[f428])).
% 0.19/0.30 thf(f432,definition,(
% 0.19/0.30 spl0_21 <=> ! [X0 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition])).
% 0.19/0.30 thf(f433,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_21),
% 0.19/0.30 inference(avatar_component_clause,[],[f432])).
% 0.19/0.30 thf(f434,plain,(
% 0.19/0.30 spl0_20 | spl0_18 | spl0_21),
% 0.19/0.30 inference(avatar_split_clause,[],[f426,f432,f417,f428])).
% 0.19/0.30 thf(f435,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_bird))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_fox))) | ($true = ((eats @ a_fox @ a_bird))) | ($true = ((eats @ a_fox @ X1)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f18,f257])).
% 0.19/0.30 thf(f436,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_bird))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_fox))) | ($true = ((eats @ a_fox @ a_bird))) | ($true = ((eats @ a_fox @ X1)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f435])).
% 0.19/0.30 thf(f437,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true != ((animal @ a_fox))) | ($true = ((eats @ a_fox @ a_bird))) | ($true = ((eats @ a_fox @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f436,f39])).
% 0.19/0.30 thf(f438,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true = ((eats @ a_fox @ a_bird))) | ($true = ((eats @ a_fox @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f437,f37])).
% 0.19/0.30 thf(f440,definition,(
% 0.19/0.30 spl0_22 <=> ($true = ((eats @ a_fox @ a_bird)))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition])).
% 0.19/0.30 thf(f442,plain,(
% 0.19/0.30 ($true = ((eats @ a_fox @ a_bird))) | ~spl0_22),
% 0.19/0.30 inference(avatar_component_clause,[],[f440])).
% 0.19/0.30 thf(f444,definition,(
% 0.19/0.30 spl0_23 <=> ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_fox @ X1))))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition])).
% 0.19/0.30 thf(f445,plain,(
% 0.19/0.30 ( ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_fox @ X1)))) ) | ~spl0_23),
% 0.19/0.30 inference(avatar_component_clause,[],[f444])).
% 0.19/0.30 thf(f447,definition,(
% 0.19/0.30 spl0_24 <=> ! [X0 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition])).
% 0.19/0.30 thf(f448,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_24),
% 0.19/0.30 inference(avatar_component_clause,[],[f447])).
% 0.19/0.30 thf(f449,plain,(
% 0.19/0.30 spl0_22 | spl0_23 | spl0_24),
% 0.19/0.30 inference(avatar_split_clause,[],[f438,f447,f444,f440])).
% 0.19/0.30 thf(f450,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_fox))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_wolf))) | ($true = ((eats @ a_wolf @ a_fox))) | ($true = ((eats @ a_wolf @ X1)))) )),
% 0.19/0.30 inference(constrained_superposition,[],[f18,f262])).
% 0.19/0.30 thf(f451,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true) | ($true != ((animal @ a_fox))) | ($true != ((plant @ X1))) | ($true != ((animal @ a_wolf))) | ($true = ((eats @ a_wolf @ a_fox))) | ($true = ((eats @ a_wolf @ X1)))) )),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f450])).
% 0.19/0.30 thf(f452,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true != ((animal @ a_wolf))) | ($true = ((eats @ a_wolf @ a_fox))) | ($true = ((eats @ a_wolf @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f451,f37])).
% 0.19/0.30 thf(f453,plain,(
% 0.19/0.30 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true) | ($true != ((plant @ X1))) | ($true = ((eats @ a_wolf @ a_fox))) | ($true = ((eats @ a_wolf @ X1)))) )),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f452,f35])).
% 0.19/0.30 thf(f455,definition,(
% 0.19/0.30 spl0_25 <=> ($true = ((eats @ a_wolf @ a_fox)))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition])).
% 0.19/0.30 thf(f457,plain,(
% 0.19/0.30 ($true = ((eats @ a_wolf @ a_fox))) | ~spl0_25),
% 0.19/0.30 inference(avatar_component_clause,[],[f455])).
% 0.19/0.30 thf(f459,definition,(
% 0.19/0.30 spl0_26 <=> ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_wolf @ X1))))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition])).
% 0.19/0.30 thf(f460,plain,(
% 0.19/0.30 ( ! [X1 : $i] : (($true != ((plant @ X1))) | ($true = ((eats @ a_wolf @ X1)))) ) | ~spl0_26),
% 0.19/0.30 inference(avatar_component_clause,[],[f459])).
% 0.19/0.30 thf(f462,definition,(
% 0.19/0.30 spl0_27 <=> ! [X0 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition])).
% 0.19/0.30 thf(f463,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_27),
% 0.19/0.30 inference(avatar_component_clause,[],[f462])).
% 0.19/0.30 thf(f464,plain,(
% 0.19/0.30 spl0_25 | spl0_26 | spl0_27),
% 0.19/0.30 inference(avatar_split_clause,[],[f453,f462,f459,f455])).
% 0.19/0.30 thf(f533,definition,(
% 0.19/0.30 spl0_35 <=> ! [X1 : $i] : (($true != ((eats @ X1 @ a_bird))) | (((animal @ X1)) != $true))),
% 0.19/0.30 introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition])).
% 0.19/0.30 thf(f534,plain,(
% 0.19/0.30 ( ! [X1 : $i] : (($true != ((eats @ X1 @ a_bird))) | (((animal @ X1)) != $true)) ) | ~spl0_35),
% 0.19/0.30 inference(avatar_component_clause,[],[f533])).
% 0.19/0.30 thf(f563,plain,(
% 0.19/0.30 ($true != $true) | ($false = ((eats @ a_wolf @ a_grain)))),
% 0.19/0.30 inference(constrained_superposition,[],[f298,f11])).
% 0.19/0.30 thf(f566,plain,(
% 0.19/0.30 ($false = ((eats @ a_wolf @ a_grain)))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f563])).
% 0.19/0.30 thf(f570,plain,(
% 0.19/0.30 ($true != $true) | ($false = ((eats @ a_bird @ a_snail)))),
% 0.19/0.30 inference(constrained_superposition,[],[f306,f13])).
% 0.19/0.30 thf(f573,plain,(
% 0.19/0.30 ($false = ((eats @ a_bird @ a_snail)))),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f570])).
% 0.19/0.30 thf(f1172,plain,(
% 0.19/0.30 ($true != $true) | (((fox @ a_fox)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_25),
% 0.19/0.30 inference(constrained_superposition,[],[f23,f457])).
% 0.19/0.30 thf(f1187,plain,(
% 0.19/0.30 (((fox @ a_fox)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_25),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1172])).
% 0.19/0.30 thf(f1203,plain,(
% 0.19/0.30 (((wolf @ a_wolf)) != $true) | ~spl0_25),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f1187,f12])).
% 0.19/0.30 thf(f1240,plain,(
% 0.19/0.30 $false | ~spl0_25),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f1203,f11])).
% 0.19/0.30 thf(f1241,plain,(
% 0.19/0.30 ~spl0_25),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1240])).
% 0.19/0.30 thf(f1430,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((eats @ a_bird @ a_grain))) | ~spl0_18),
% 0.19/0.30 inference(constrained_superposition,[],[f418,f45])).
% 0.19/0.30 thf(f1442,plain,(
% 0.19/0.30 ($true = ((eats @ a_bird @ a_grain))) | ~spl0_18),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1430])).
% 0.19/0.30 thf(f1460,plain,(
% 0.19/0.30 ($true != $true) | ($true != ((plant @ (sf @ a_snail)))) | ~spl0_21),
% 0.19/0.30 inference(constrained_superposition,[],[f433,f53])).
% 0.19/0.30 thf(f1467,plain,(
% 0.19/0.30 ($true != ((plant @ (sf @ a_snail)))) | ~spl0_21),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1460])).
% 0.19/0.30 thf(f1471,plain,(
% 0.19/0.30 $false | ~spl0_21),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f1467,f49])).
% 0.19/0.30 thf(f1472,plain,(
% 0.19/0.30 ~spl0_21),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1471])).
% 0.19/0.30 thf(f1499,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((plant @ X0)) != $true)) ) | (~spl0_18 | ~spl0_24)),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f448,f418])).
% 0.19/0.30 thf(f1508,plain,(
% 0.19/0.30 $false | (~spl0_18 | ~spl0_24)),
% 0.19/0.30 inference(backward_subsumption_resolution,[],[f45,f1499])).
% 0.19/0.30 thf(f1515,plain,(
% 0.19/0.30 ~spl0_18 | ~spl0_24),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1508])).
% 0.19/0.30 thf(f1516,plain,(
% 0.19/0.30 ($true = $false) | ~spl0_20),
% 0.19/0.30 inference(forward_demodulation,[],[f430,f573])).
% 0.19/0.30 thf(f1517,plain,(
% 0.19/0.30 $false | ~spl0_20),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1516])).
% 0.19/0.30 thf(f1518,plain,(
% 0.19/0.30 ~spl0_20),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1517])).
% 0.19/0.30 thf(f1675,plain,(
% 0.19/0.30 ($true != $true) | ($true = ((eats @ a_wolf @ a_grain))) | ~spl0_26),
% 0.19/0.30 inference(constrained_superposition,[],[f460,f45])).
% 0.19/0.30 thf(f1690,plain,(
% 0.19/0.30 ($true = ((eats @ a_wolf @ a_grain))) | ~spl0_26),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1675])).
% 0.19/0.30 thf(f1691,plain,(
% 0.19/0.30 ($true = $false) | ~spl0_26),
% 0.19/0.30 inference(forward_demodulation,[],[f1690,f566])).
% 0.19/0.30 thf(f1692,plain,(
% 0.19/0.30 $false | ~spl0_26),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1691])).
% 0.19/0.30 thf(f1693,plain,(
% 0.19/0.30 ~spl0_26),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1692])).
% 0.19/0.30 thf(f1694,plain,(
% 0.19/0.30 ( ! [X0 : $i] : ((((plant @ X0)) != $true)) ) | (~spl0_23 | ~spl0_27)),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f463,f445])).
% 0.19/0.30 thf(f1703,plain,(
% 0.19/0.30 $false | (~spl0_23 | ~spl0_27)),
% 0.19/0.30 inference(backward_subsumption_resolution,[],[f47,f1694])).
% 0.19/0.30 thf(f1711,plain,(
% 0.19/0.30 ~spl0_23 | ~spl0_27),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1703])).
% 0.19/0.30 thf(f1837,plain,(
% 0.19/0.30 ($true != $true) | ($true != ((animal @ a_fox))) | (~spl0_22 | ~spl0_35)),
% 0.19/0.30 inference(constrained_superposition,[],[f534,f442])).
% 0.19/0.30 thf(f1840,plain,(
% 0.19/0.30 ($true != ((animal @ a_fox))) | (~spl0_22 | ~spl0_35)),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f1837])).
% 0.19/0.30 thf(f1844,plain,(
% 0.19/0.30 $false | (~spl0_22 | ~spl0_35)),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f1840,f37])).
% 0.19/0.30 thf(f1845,plain,(
% 0.19/0.30 ~spl0_22 | ~spl0_35),
% 0.19/0.30 inference(avatar_contradiction_clause,[],[f1844])).
% 0.19/0.30 thf(f2200,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != $true) | ($true != ((eats @ X0 @ a_bird))) | (((grain @ a_grain)) != $true) | ($true != ((animal @ a_bird))) | (((animal @ X0)) != $true)) ) | ~spl0_18),
% 0.19/0.30 inference(constrained_superposition,[],[f31,f1442])).
% 0.19/0.30 thf(f2211,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ X0 @ a_bird))) | (((grain @ a_grain)) != $true) | ($true != ((animal @ a_bird))) | (((animal @ X0)) != $true)) ) | ~spl0_18),
% 0.19/0.30 inference(trivial_inequality_removal,[],[f2200])).
% 0.19/0.30 thf(f2221,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ X0 @ a_bird))) | ($true != ((animal @ a_bird))) | (((animal @ X0)) != $true)) ) | ~spl0_18),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f2211,f16])).
% 0.19/0.30 thf(f2241,plain,(
% 0.19/0.30 ( ! [X0 : $i] : (($true != ((eats @ X0 @ a_bird))) | (((animal @ X0)) != $true)) ) | ~spl0_18),
% 0.19/0.30 inference(forward_subsumption_resolution,[],[f2221,f39])).
% 0.19/0.30 thf(f2243,plain,(
% 0.19/0.30 spl0_35 | ~spl0_18),
% 0.19/0.30 inference(avatar_split_clause,[],[f2241,f417,f533])).
% 0.19/0.30 cnf(s12, plain, spl0_18 | spl0_20 | spl0_21, inference(sat_conversion,[],[f434])).
% 0.19/0.30 cnf(s13, plain, spl0_22 | spl0_23 | spl0_24, inference(sat_conversion,[],[f449])).
% 0.19/0.30 cnf(s14, plain, spl0_25 | spl0_26 | spl0_27, inference(sat_conversion,[],[f464])).
% 0.19/0.30 cnf(s70, plain, ~spl0_25, inference(sat_conversion,[],[f1241])).
% 0.19/0.30 cnf(s84, plain, ~spl0_21, inference(sat_conversion,[],[f1472])).
% 0.19/0.30 cnf(s87, plain, ~spl0_18 | ~spl0_24, inference(sat_conversion,[],[f1515])).
% 0.19/0.30 cnf(s88, plain, ~spl0_20, inference(sat_conversion,[],[f1518])).
% 0.19/0.30 cnf(s89, plain, ~spl0_26, inference(sat_conversion,[],[f1693])).
% 0.19/0.30 cnf(s92, plain, ~spl0_23 | ~spl0_27, inference(sat_conversion,[],[f1711])).
% 0.19/0.30 cnf(s96, plain, ~spl0_22 | ~spl0_35, inference(sat_conversion,[],[f1845])).
% 0.19/0.30 cnf(s113, plain, ~spl0_18 | spl0_35, inference(sat_conversion,[],[f2243])).
% 0.19/0.30 cnf(s120, plain, spl0_27, inference(rat,[],[s14,s89,s70])).
% 0.19/0.30 cnf(s122, plain, ~spl0_23, inference(rat,[],[s92,s120])).
% 0.19/0.30 cnf(s124, plain, spl0_22 | spl0_24, inference(rat,[],[s13,s122])).
% 0.19/0.30 cnf(s125, plain, spl0_18, inference(rat,[],[s12,s84,s88])).
% 0.19/0.30 cnf(s126, plain, spl0_35, inference(rat,[],[s113,s125])).
% 0.19/0.30 cnf(s128, plain, ~spl0_24, inference(rat,[],[s87,s125])).
% 0.19/0.30 cnf(s129, plain, ~spl0_22, inference(rat,[],[s96,s126])).
% 0.19/0.30 cnf(s132, plain, $false, inference(rat,[],[s124,s128,s129])).
% 0.19/0.30 thf(f2244,plain,(
% 0.19/0.30 $false),
% 0.19/0.30 inference(avatar_sat_refutation,[],[s132])).
% 0.19/0.30 % SZS output end Proof for theBenchmark
% 0.19/0.30 % (572927)------------------------------
% 0.19/0.30 % (572927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.30 % (572927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.30 % (572927)CaDiCaL version: 2.1.3
% 0.19/0.30 % (572927)Termination reason: Refutation
% 0.19/0.30 % (572927)Time elapsed: 0.053 s
% 0.19/0.30 % (572927)Peak memory usage: 14 MB
% 0.19/0.30 % (572927)Instructions burned: 188 (million)
% 0.19/0.30 % (572921)Success in time 0.08 s
% 0.19/0.30 % Vampire exiting
%------------------------------------------------------------------------------