%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ094^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:02 AM UTC 2026
% Result : Theorem 0.50s 0.33s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ094^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16 % Computer : n005.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Tue Sep 29 13:22:01 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.50/0.33 % (1644297)Will run a generic schedule for satisfiability detection.
% 0.50/0.33 % (1644305)dis+10_1_sil=32000:sp=arity:random_seed=1845335494:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.50/0.33 % (1644303)% WARNING: option uhcvi not known.
% 0.50/0.33 % (1644302)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3913744533_2999 on theBenchmark for (2999ds/0Mi)
% 0.50/0.33 % (1644303)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3362093551:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.50/0.33 % (1644304)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1761324940:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.50/0.33 % (1644306)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1499193231:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.50/0.33 % Exception at run slice level
% 0.50/0.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.50/0.33 % (1644308)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=574197142:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.50/0.33 % (1644303)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.50/0.33 % (1644303)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.50/0.33 % (1644306)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.50/0.33 % (1644307)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2560961942:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.50/0.33 % (1644315)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1477644791:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.50/0.33 % Exception at run slice level
% 0.50/0.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.50/0.33 % (1644305)Instruction limit reached!
% 0.50/0.33 % (1644305)------------------------------
% 0.50/0.33 % (1644305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.33 % (1644305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.33 % (1644305)CaDiCaL version: 2.1.3
% 0.50/0.33 % (1644305)Termination reason: Instruction limit
% 0.50/0.33 % (1644305)Termination phase: Saturation
% 0.50/0.33 % (1644305)Time elapsed: 0.030 s
% 0.50/0.33 % (1644305)Peak memory usage: 12 MB
% 0.50/0.33 % (1644305)Instructions burned: 105 (million)
% 0.50/0.33 % (1644318)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3480168332:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.50/0.33 % (1644319)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3039094729:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.50/0.33 % (1644319)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.50/0.33 % (1644319)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.50/0.33 % (1644306)Instruction limit reached!
% 0.50/0.33 % (1644306)------------------------------
% 0.50/0.33 % (1644306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.33 % (1644306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.33 % (1644306)CaDiCaL version: 2.1.3
% 0.50/0.33 % (1644306)Termination reason: Instruction limit
% 0.50/0.33 % (1644306)Termination phase: Saturation
% 0.50/0.33 % (1644306)Time elapsed: 0.047 s
% 0.50/0.33 % (1644306)Peak memory usage: 12 MB
% 0.50/0.33 % (1644306)Instructions burned: 120 (million)
% 0.50/0.33 % (1644322)ott-21_1_sil=16000:fs=off:random_seed=3370392617:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.50/0.33 % (1644308)Instruction limit reached!
% 0.50/0.33 % (1644308)------------------------------
% 0.50/0.33 % (1644308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.33 % (1644308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.33 % (1644308)CaDiCaL version: 2.1.3
% 0.50/0.33 % (1644308)Termination reason: Instruction limit
% 0.50/0.33 % (1644308)Termination phase: Saturation
% 0.50/0.33 % (1644308)Time elapsed: 0.075 s
% 0.50/0.33 % (1644308)Peak memory usage: 12 MB
% 0.50/0.33 % (1644308)Instructions burned: 159 (million)
% 0.50/0.33 % (1644319) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1644297-1644319"...
% 0.50/0.33 % (1644319)...printing done.
% 0.50/0.33 % (1644319)Refutation found. Thanks to Tanya!
% 0.50/0.33 % SZS status Theorem for theBenchmark
% 0.50/0.33 % SZS output start Proof for theBenchmark
% 0.50/0.33 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.50/0.33 thf(func_def_0, type, eats: ($i > $i > $o)).
% 0.50/0.33 thf(func_def_1, type, grain: ($i > $o)).
% 0.50/0.33 thf(func_def_2, type, animal: ($i > $o)).
% 0.50/0.33 thf(func_def_3, type, snail: ($i > $o)).
% 0.50/0.33 thf(func_def_4, type, sf: ($i > $i)).
% 0.50/0.33 thf(func_def_5, type, plant: ($i > $o)).
% 0.50/0.33 thf(func_def_6, type, bird: ($i > $o)).
% 0.50/0.33 thf(func_def_7, type, wolf: ($i > $o)).
% 0.50/0.33 thf(func_def_8, type, fox: ($i > $o)).
% 0.50/0.33 thf(func_def_9, type, msmaller: ($i > $i > $o)).
% 0.50/0.33 thf(f1,conjecture,(
% 0.50/0.33 ~(! [X1 : $i,X9 : $i,X8 : $i] : (~(eats @ X9 @ X8) | ~(eats @ X1 @ X9) | ~(grain @ X8) | ~(animal @ X9) | ~(animal @ X1)) & ! [X3 : $i] : (~(snail @ X3) | (eats @ X3 @ (sf @ X3))) & ! [X3 : $i] : (~(snail @ X3) | (plant @ (sf @ X3))) & ! [X5 : $i,X3 : $i] : (~(eats @ X5 @ X3) | ~(snail @ X3) | ~(bird @ X5)) & ! [X7 : $i,X8 : $i] : (~(eats @ X7 @ X8) | ~(grain @ X8) | ~(wolf @ X7)) & ! [X6 : $i,X7 : $i] : (~(eats @ X7 @ X6) | ~(fox @ X6) | ~(wolf @ X7)) & ! [X6 : $i,X7 : $i] : (~(wolf @ X7) | ~(fox @ X6) | (msmaller @ X6 @ X7)) & ! [X5 : $i,X6 : $i] : (~(fox @ X6) | ~(bird @ X5) | (msmaller @ X5 @ X6)) & ! [X3 : $i,X5 : $i] : (~(bird @ X5) | ~(snail @ X3) | (msmaller @ X3 @ X5)) & ! [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) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X0 : $i] : (~(snail @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(bird @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(fox @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(wolf @ X0) | (animal @ X0)))),
% 0.50/0.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cPUZ031_2)).
% 0.50/0.33 thf(f2,negated_conjecture,(
% 0.50/0.33 ~ ~(! [X1 : $i,X9 : $i,X8 : $i] : (~(eats @ X9 @ X8) | ~(eats @ X1 @ X9) | ~(grain @ X8) | ~(animal @ X9) | ~(animal @ X1)) & ! [X3 : $i] : (~(snail @ X3) | (eats @ X3 @ (sf @ X3))) & ! [X3 : $i] : (~(snail @ X3) | (plant @ (sf @ X3))) & ! [X5 : $i,X3 : $i] : (~(eats @ X5 @ X3) | ~(snail @ X3) | ~(bird @ X5)) & ! [X7 : $i,X8 : $i] : (~(eats @ X7 @ X8) | ~(grain @ X8) | ~(wolf @ X7)) & ! [X6 : $i,X7 : $i] : (~(eats @ X7 @ X6) | ~(fox @ X6) | ~(wolf @ X7)) & ! [X6 : $i,X7 : $i] : (~(wolf @ X7) | ~(fox @ X6) | (msmaller @ X6 @ X7)) & ! [X5 : $i,X6 : $i] : (~(fox @ X6) | ~(bird @ X5) | (msmaller @ X5 @ X6)) & ! [X3 : $i,X5 : $i] : (~(bird @ X5) | ~(snail @ X3) | (msmaller @ X3 @ X5)) & ! [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) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X0 : $i] : (~(snail @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(bird @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(fox @ X0) | (animal @ X0)) & ! [X0 : $i] : (~(wolf @ X0) | (animal @ X0)))),
% 0.50/0.33 inference(negated_conjecture,[status(cth)],[f1])).
% 0.50/0.33 thf(f3,plain,(
% 0.50/0.33 ~ ~(! [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,X6 : $i] : (~(eats @ X5 @ X6) | ~(snail @ X6) | ~(bird @ X5)) & ! [X7 : $i,X8 : $i] : (~(eats @ X7 @ X8) | ~(grain @ X8) | ~(wolf @ X7)) & ! [X9 : $i,X10 : $i] : (~(eats @ X10 @ X9) | ~(fox @ X9) | ~(wolf @ X10)) & ! [X11 : $i,X12 : $i] : (~(wolf @ X12) | ~(fox @ X11) | (msmaller @ X11 @ X12)) & ! [X13 : $i,X14 : $i] : (~(fox @ X14) | ~(bird @ X13) | (msmaller @ X13 @ X14)) & ! [X15 : $i,X16 : $i] : (~(bird @ X16) | ~(snail @ X15) | (msmaller @ X15 @ X16)) & ! [X17 : $i,X18 : $i,X19 : $i,X20 : $i] : (~(eats @ X19 @ X20) | ~(msmaller @ X19 @ X17) | ~(plant @ X20) | ~(animal @ X19) | ~(plant @ X18) | ~(animal @ X17) | (eats @ X17 @ X19) | (eats @ X17 @ X18)) & ! [X21 : $i] : (~(grain @ X21) | (plant @ X21)) & (grain @ a_grain) & (snail @ a_snail) & (bird @ a_bird) & (fox @ a_fox) & (wolf @ a_wolf) & ! [X22 : $i] : (~(snail @ X22) | (animal @ X22)) & ! [X23 : $i] : (~(bird @ X23) | (animal @ X23)) & ! [X24 : $i] : (~(fox @ X24) | (animal @ X24)) & ! [X25 : $i] : (~(wolf @ X25) | (animal @ X25)))),
% 0.50/0.33 inference(rectify,[],[f2])).
% 0.50/0.33 thf(f4,plain,(
% 0.50/0.33 ~ ~(! [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,X6 : $i] : (~ (((eats @ X5 @ X6)) = $true) | ~ (((snail @ X6)) = $true) | ~ (((bird @ X5)) = $true)) & ! [X7 : $i,X8 : $i] : (~ (((eats @ X7 @ X8)) = $true) | ~ (((grain @ X8)) = $true) | ~ (((wolf @ X7)) = $true)) & ! [X9 : $i,X10 : $i] : (~ (((eats @ X10 @ X9)) = $true) | ~ (((fox @ X9)) = $true) | ~ (((wolf @ X10)) = $true)) & ! [X11 : $i,X12 : $i] : (~ (((wolf @ X12)) = $true) | ~ (((fox @ X11)) = $true) | (((msmaller @ X11 @ X12)) = $true)) & ! [X13 : $i,X14 : $i] : (~ (((fox @ X14)) = $true) | ~ (((bird @ X13)) = $true) | (((msmaller @ X13 @ X14)) = $true)) & ! [X15 : $i,X16 : $i] : (~ (((bird @ X16)) = $true) | ~ (((snail @ X15)) = $true) | (((msmaller @ X15 @ X16)) = $true)) & ! [X17 : $i,X18 : $i,X19 : $i,X20 : $i] : (~ (((eats @ X19 @ X20)) = $true) | ~ (((msmaller @ X19 @ X17)) = $true) | ~ (((plant @ X20)) = $true) | ~ (((animal @ X19)) = $true) | ~ (((plant @ X18)) = $true) | ~ (((animal @ X17)) = $true) | (((eats @ X17 @ X19)) = $true) | (((eats @ X17 @ X18)) = $true)) & ! [X21 : $i] : (~ (((grain @ X21)) = $true) | (((plant @ X21)) = $true)) & (((grain @ a_grain)) = $true) & (((snail @ a_snail)) = $true) & (((bird @ a_bird)) = $true) & (((fox @ a_fox)) = $true) & (((wolf @ a_wolf)) = $true) & ! [X22 : $i] : (~ (((snail @ X22)) = $true) | (((animal @ X22)) = $true)) & ! [X23 : $i] : (~ (((bird @ X23)) = $true) | (((animal @ X23)) = $true)) & ! [X24 : $i] : (~ (((fox @ X24)) = $true) | (((animal @ X24)) = $true)) & ! [X25 : $i] : (~ (((wolf @ X25)) = $true) | (((animal @ X25)) = $true)))),
% 0.50/0.33 inference(fool_elimination,[],[f3])).
% 0.50/0.33 thf(f5,plain,(
% 0.50/0.33 ! [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,X6 : $i] : ((((eats @ X5 @ X6)) != $true) | (((snail @ X6)) != $true) | (((bird @ X5)) != $true)) & ! [X7 : $i,X8 : $i] : ((((eats @ X7 @ X8)) != $true) | (((grain @ X8)) != $true) | (((wolf @ X7)) != $true)) & ! [X9 : $i,X10 : $i] : ((((eats @ X10 @ X9)) != $true) | (((fox @ X9)) != $true) | (((wolf @ X10)) != $true)) & ! [X11 : $i,X12 : $i] : ((((wolf @ X12)) != $true) | (((fox @ X11)) != $true) | (((msmaller @ X11 @ X12)) = $true)) & ! [X13 : $i,X14 : $i] : ((((fox @ X14)) != $true) | (((bird @ X13)) != $true) | (((msmaller @ X13 @ X14)) = $true)) & ! [X15 : $i,X16 : $i] : ((((bird @ X16)) != $true) | (((snail @ X15)) != $true) | (((msmaller @ X15 @ X16)) = $true)) & ! [X17 : $i,X18 : $i,X19 : $i,X20 : $i] : ((((eats @ X19 @ X20)) != $true) | (((msmaller @ X19 @ X17)) != $true) | (((plant @ X20)) != $true) | (((animal @ X19)) != $true) | (((plant @ X18)) != $true) | (((animal @ X17)) != $true) | (((eats @ X17 @ X19)) = $true) | (((eats @ X17 @ X18)) = $true)) & ! [X21 : $i] : ((((grain @ X21)) != $true) | (((plant @ X21)) = $true)) & (((grain @ a_grain)) = $true) & (((snail @ a_snail)) = $true) & (((bird @ a_bird)) = $true) & (((fox @ a_fox)) = $true) & (((wolf @ a_wolf)) = $true) & ! [X22 : $i] : ((((snail @ X22)) != $true) | (((animal @ X22)) = $true)) & ! [X23 : $i] : ((((bird @ X23)) != $true) | (((animal @ X23)) = $true)) & ! [X24 : $i] : ((((fox @ X24)) != $true) | (((animal @ X24)) = $true)) & ! [X25 : $i] : ((((wolf @ X25)) != $true) | (((animal @ X25)) = $true))),
% 0.50/0.33 inference(flattening,[],[f4])).
% 0.50/0.33 thf(f6,plain,(
% 0.50/0.33 ( ! [X25 : $i] : ((((wolf @ X25)) != $true) | (((animal @ X25)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f7,plain,(
% 0.50/0.33 ( ! [X24 : $i] : ((((fox @ X24)) != $true) | (((animal @ X24)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f8,plain,(
% 0.50/0.33 ( ! [X23 : $i] : ((((bird @ X23)) != $true) | (((animal @ X23)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f9,plain,(
% 0.50/0.33 ( ! [X22 : $i] : ((((snail @ X22)) != $true) | (((animal @ X22)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f10,plain,(
% 0.50/0.33 (((wolf @ a_wolf)) = $true)),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f11,plain,(
% 0.50/0.33 (((fox @ a_fox)) = $true)),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f12,plain,(
% 0.50/0.33 (((bird @ a_bird)) = $true)),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f13,plain,(
% 0.50/0.33 (((snail @ a_snail)) = $true)),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f14,plain,(
% 0.50/0.33 (((grain @ a_grain)) = $true)),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f15,plain,(
% 0.50/0.33 ( ! [X21 : $i] : ((((grain @ X21)) != $true) | (((plant @ X21)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f16,plain,(
% 0.50/0.33 ( ! [X18 : $i,X19 : $i,X17 : $i,X20 : $i] : ((((msmaller @ X19 @ X17)) != $true) | (((eats @ X19 @ X20)) != $true) | (((plant @ X20)) != $true) | (((animal @ X19)) != $true) | (((plant @ X18)) != $true) | (((animal @ X17)) != $true) | (((eats @ X17 @ X19)) = $true) | (((eats @ X17 @ X18)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f17,plain,(
% 0.50/0.33 ( ! [X16 : $i,X15 : $i] : ((((bird @ X16)) != $true) | (((snail @ X15)) != $true) | (((msmaller @ X15 @ X16)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f18,plain,(
% 0.50/0.33 ( ! [X14 : $i,X13 : $i] : ((((fox @ X14)) != $true) | (((bird @ X13)) != $true) | (((msmaller @ X13 @ X14)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f19,plain,(
% 0.50/0.33 ( ! [X11 : $i,X12 : $i] : ((((fox @ X11)) != $true) | (((wolf @ X12)) != $true) | (((msmaller @ X11 @ X12)) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f20,plain,(
% 0.50/0.33 ( ! [X10 : $i,X9 : $i] : ((((eats @ X10 @ X9)) != $true) | (((fox @ X9)) != $true) | (((wolf @ X10)) != $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f21,plain,(
% 0.50/0.33 ( ! [X8 : $i,X7 : $i] : ((((eats @ X7 @ X8)) != $true) | (((grain @ X8)) != $true) | (((wolf @ X7)) != $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f22,plain,(
% 0.50/0.33 ( ! [X6 : $i,X5 : $i] : ((((eats @ X5 @ X6)) != $true) | (((snail @ X6)) != $true) | (((bird @ X5)) != $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f23,plain,(
% 0.50/0.33 ( ! [X4 : $i] : ((((snail @ X4)) != $true) | (((plant @ (sf @ X4))) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f24,plain,(
% 0.50/0.33 ( ! [X3 : $i] : ((((snail @ X3)) != $true) | (((eats @ X3 @ (sf @ X3))) = $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f25,plain,(
% 0.50/0.33 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((eats @ X1 @ X2)) != $true) | (((eats @ X0 @ X1)) != $true) | (((grain @ X2)) != $true) | (((animal @ X1)) != $true) | (((animal @ X0)) != $true)) )),
% 0.50/0.33 inference(cnf_transformation,[],[f5])).
% 0.50/0.33 thf(f27,definition,(
% 0.50/0.33 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.50/0.33 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.50/0.33 thf(f35,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((animal @ a_wolf)))),
% 0.50/0.33 inference(constrained_superposition,[],[f6,f10])).
% 0.50/0.33 thf(f38,plain,(
% 0.50/0.33 ($true = ((animal @ a_wolf)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f35])).
% 0.50/0.33 thf(f39,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((animal @ a_fox)))),
% 0.50/0.33 inference(constrained_superposition,[],[f7,f11])).
% 0.50/0.33 thf(f42,plain,(
% 0.50/0.33 ($true = ((animal @ a_fox)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f39])).
% 0.50/0.33 thf(f43,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((animal @ a_bird)))),
% 0.50/0.33 inference(constrained_superposition,[],[f8,f12])).
% 0.50/0.33 thf(f46,plain,(
% 0.50/0.33 ($true = ((animal @ a_bird)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f43])).
% 0.50/0.33 thf(f47,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((animal @ a_snail)))),
% 0.50/0.33 inference(constrained_superposition,[],[f9,f13])).
% 0.50/0.33 thf(f50,plain,(
% 0.50/0.33 ($true = ((animal @ a_snail)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f47])).
% 0.50/0.33 thf(f51,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((plant @ a_grain)))),
% 0.50/0.33 inference(constrained_superposition,[],[f15,f14])).
% 0.50/0.33 thf(f54,plain,(
% 0.50/0.33 ($true = ((plant @ a_grain)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f51])).
% 0.50/0.33 thf(f87,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((plant @ (sf @ a_snail))))),
% 0.50/0.33 inference(constrained_superposition,[],[f23,f13])).
% 0.50/0.33 thf(f91,plain,(
% 0.50/0.33 ($true = ((plant @ (sf @ a_snail))))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f87])).
% 0.50/0.33 thf(f92,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((eats @ a_snail @ (sf @ a_snail))))),
% 0.50/0.33 inference(constrained_superposition,[],[f24,f13])).
% 0.50/0.33 thf(f96,plain,(
% 0.50/0.33 ($true = ((eats @ a_snail @ (sf @ a_snail))))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f92])).
% 0.50/0.33 thf(f97,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != $true) | (((snail @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_bird)))) )),
% 0.50/0.33 inference(constrained_superposition,[],[f17,f12])).
% 0.50/0.33 thf(f101,plain,(
% 0.50/0.33 ( ! [X0 : $i] : ((((snail @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_bird)))) )),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f97])).
% 0.50/0.33 thf(f102,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((msmaller @ a_snail @ a_bird)))),
% 0.50/0.33 inference(constrained_superposition,[],[f101,f13])).
% 0.50/0.33 thf(f106,plain,(
% 0.50/0.33 ($true = ((msmaller @ a_snail @ a_bird)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f102])).
% 0.50/0.33 thf(f107,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != $true) | (((bird @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_fox)))) )),
% 0.50/0.33 inference(constrained_superposition,[],[f18,f11])).
% 0.50/0.33 thf(f111,plain,(
% 0.50/0.33 ( ! [X0 : $i] : ((((bird @ X0)) != $true) | ($true = ((msmaller @ X0 @ a_fox)))) )),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f107])).
% 0.50/0.33 thf(f112,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((msmaller @ a_bird @ a_fox)))),
% 0.50/0.33 inference(constrained_superposition,[],[f111,f12])).
% 0.50/0.33 thf(f116,plain,(
% 0.50/0.33 ($true = ((msmaller @ a_bird @ a_fox)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f112])).
% 0.50/0.33 thf(f117,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != $true) | (((wolf @ X0)) != $true) | ($true = ((msmaller @ a_fox @ X0)))) )),
% 0.50/0.33 inference(constrained_superposition,[],[f19,f11])).
% 0.50/0.33 thf(f121,plain,(
% 0.50/0.33 ( ! [X0 : $i] : ((((wolf @ X0)) != $true) | ($true = ((msmaller @ a_fox @ X0)))) )),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f117])).
% 0.50/0.33 thf(f122,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((msmaller @ a_fox @ a_wolf)))),
% 0.50/0.33 inference(constrained_superposition,[],[f121,f10])).
% 0.50/0.33 thf(f126,plain,(
% 0.50/0.33 ($true = ((msmaller @ a_fox @ a_wolf)))),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f122])).
% 0.50/0.33 thf(f311,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(constrained_superposition,[],[f16,f106])).
% 0.50/0.33 thf(f313,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(constrained_superposition,[],[f16,f116])).
% 0.50/0.33 thf(f322,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(trivial_inequality_removal,[],[f313])).
% 0.50/0.33 thf(f324,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(trivial_inequality_removal,[],[f311])).
% 0.50/0.33 thf(f331,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f322,f46])).
% 0.50/0.33 thf(f333,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f324,f50])).
% 0.50/0.33 thf(f340,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f331,f42])).
% 0.50/0.33 thf(f342,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f333,f46])).
% 0.50/0.33 thf(f347,definition,(
% 0.50/0.33 spl0_10 <=> ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_wolf @ X2))))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition])).
% 0.50/0.33 thf(f348,plain,(
% 0.50/0.33 ( ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_wolf @ X2)))) ) | ~spl0_10),
% 0.50/0.33 inference(avatar_component_clause,[],[f347])).
% 0.50/0.33 thf(f354,definition,(
% 0.50/0.33 spl0_12 <=> ($true = ((eats @ a_wolf @ a_fox)))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition])).
% 0.50/0.33 thf(f356,plain,(
% 0.50/0.33 ($true = ((eats @ a_wolf @ a_fox))) | ~spl0_12),
% 0.50/0.33 inference(avatar_component_clause,[],[f354])).
% 0.50/0.33 thf(f358,definition,(
% 0.50/0.33 spl0_13 <=> ! [X0 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition])).
% 0.50/0.33 thf(f359,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != ((eats @ a_fox @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_13),
% 0.50/0.33 inference(avatar_component_clause,[],[f358])).
% 0.50/0.33 thf(f362,definition,(
% 0.50/0.33 spl0_14 <=> ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_fox @ X2))))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition])).
% 0.50/0.33 thf(f363,plain,(
% 0.50/0.33 ( ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_fox @ X2)))) ) | ~spl0_14),
% 0.50/0.33 inference(avatar_component_clause,[],[f362])).
% 0.50/0.33 thf(f369,definition,(
% 0.50/0.33 spl0_16 <=> ($true = ((eats @ a_fox @ a_bird)))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition])).
% 0.50/0.33 thf(f371,plain,(
% 0.50/0.33 ($true = ((eats @ a_fox @ a_bird))) | ~spl0_16),
% 0.50/0.33 inference(avatar_component_clause,[],[f369])).
% 0.50/0.33 thf(f373,definition,(
% 0.50/0.33 spl0_17 <=> ! [X0 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition])).
% 0.50/0.33 thf(f374,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != ((eats @ a_bird @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_17),
% 0.50/0.33 inference(avatar_component_clause,[],[f373])).
% 0.50/0.33 thf(f375,plain,(
% 0.50/0.33 spl0_16 | spl0_14 | spl0_17),
% 0.50/0.33 inference(avatar_split_clause,[],[f340,f373,f362,f369])).
% 0.50/0.33 thf(f377,definition,(
% 0.50/0.33 spl0_18 <=> ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_bird @ X2))))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition])).
% 0.50/0.33 thf(f378,plain,(
% 0.50/0.33 ( ! [X2 : $i] : ((((plant @ X2)) != $true) | ($true = ((eats @ a_bird @ X2)))) ) | ~spl0_18),
% 0.50/0.33 inference(avatar_component_clause,[],[f377])).
% 0.50/0.33 thf(f384,definition,(
% 0.50/0.33 spl0_20 <=> ($true = ((eats @ a_bird @ a_snail)))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition])).
% 0.50/0.33 thf(f386,plain,(
% 0.50/0.33 ($true = ((eats @ a_bird @ a_snail))) | ~spl0_20),
% 0.50/0.33 inference(avatar_component_clause,[],[f384])).
% 0.50/0.33 thf(f388,definition,(
% 0.50/0.33 spl0_21 <=> ! [X0 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition])).
% 0.50/0.33 thf(f389,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != ((eats @ a_snail @ X0))) | (((plant @ X0)) != $true)) ) | ~spl0_21),
% 0.50/0.33 inference(avatar_component_clause,[],[f388])).
% 0.50/0.33 thf(f390,plain,(
% 0.50/0.33 spl0_20 | spl0_18 | spl0_21),
% 0.50/0.33 inference(avatar_split_clause,[],[f342,f388,f377,f384])).
% 0.50/0.33 thf(f403,plain,(
% 0.50/0.33 ($true != $true) | ($true = ((eats @ a_wolf @ a_grain))) | ~spl0_10),
% 0.50/0.33 inference(constrained_superposition,[],[f348,f54])).
% 0.50/0.33 thf(f412,plain,(
% 0.50/0.33 ($true = ((eats @ a_wolf @ a_grain))) | ~spl0_10),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f403])).
% 0.50/0.33 thf(f415,plain,(
% 0.50/0.33 ($true != $true) | (((grain @ a_grain)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_10),
% 0.50/0.33 inference(constrained_superposition,[],[f21,f412])).
% 0.50/0.33 thf(f418,plain,(
% 0.50/0.33 (((grain @ a_grain)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_10),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f415])).
% 0.50/0.33 thf(f422,plain,(
% 0.50/0.33 (((wolf @ a_wolf)) != $true) | ~spl0_10),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f418,f14])).
% 0.50/0.33 thf(f433,plain,(
% 0.50/0.33 $false | ~spl0_10),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f422,f10])).
% 0.50/0.33 thf(f434,plain,(
% 0.50/0.33 ~spl0_10),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f433])).
% 0.50/0.33 thf(f448,plain,(
% 0.50/0.33 ( ! [X2 : $i] : ((((plant @ X2)) != $true)) ) | (~spl0_13 | ~spl0_14)),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f363,f359])).
% 0.50/0.33 thf(f449,plain,(
% 0.50/0.33 ($true != $true) | (~spl0_13 | ~spl0_14)),
% 0.50/0.33 inference(constrained_superposition,[],[f448,f54])).
% 0.50/0.33 thf(f459,plain,(
% 0.50/0.33 $false | (~spl0_13 | ~spl0_14)),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f449])).
% 0.50/0.33 thf(f460,plain,(
% 0.50/0.33 ~spl0_13 | ~spl0_14),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f459])).
% 0.50/0.33 thf(f477,plain,(
% 0.50/0.33 ( ! [X2 : $i] : ((((plant @ X2)) != $true)) ) | (~spl0_17 | ~spl0_18)),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f378,f374])).
% 0.50/0.33 thf(f478,plain,(
% 0.50/0.33 ($true != $true) | (~spl0_17 | ~spl0_18)),
% 0.50/0.33 inference(constrained_superposition,[],[f477,f54])).
% 0.50/0.33 thf(f488,plain,(
% 0.50/0.33 $false | (~spl0_17 | ~spl0_18)),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f478])).
% 0.50/0.33 thf(f489,plain,(
% 0.50/0.33 ~spl0_17 | ~spl0_18),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f488])).
% 0.50/0.33 thf(f498,plain,(
% 0.50/0.33 ($true != $true) | ($true != ((plant @ (sf @ a_snail)))) | ~spl0_21),
% 0.50/0.33 inference(constrained_superposition,[],[f389,f96])).
% 0.50/0.33 thf(f503,plain,(
% 0.50/0.33 ($true != ((plant @ (sf @ a_snail)))) | ~spl0_21),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f498])).
% 0.50/0.33 thf(f505,plain,(
% 0.50/0.33 $false | ~spl0_21),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f503,f91])).
% 0.50/0.33 thf(f506,plain,(
% 0.50/0.33 ~spl0_21),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f505])).
% 0.50/0.33 thf(f509,plain,(
% 0.50/0.33 ($true != $true) | (((snail @ a_snail)) != $true) | (((bird @ a_bird)) != $true) | ~spl0_20),
% 0.50/0.33 inference(constrained_superposition,[],[f22,f386])).
% 0.50/0.33 thf(f514,plain,(
% 0.50/0.33 (((snail @ a_snail)) != $true) | (((bird @ a_bird)) != $true) | ~spl0_20),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f509])).
% 0.50/0.33 thf(f531,plain,(
% 0.50/0.33 (((bird @ a_bird)) != $true) | ~spl0_20),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f514,f13])).
% 0.50/0.33 thf(f533,plain,(
% 0.50/0.33 $false | ~spl0_20),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f531,f12])).
% 0.50/0.33 thf(f534,plain,(
% 0.50/0.33 ~spl0_20),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f533])).
% 0.50/0.33 thf(f536,definition,(
% 0.50/0.33 spl0_30 <=> ! [X0 : $i] : (($true != ((eats @ X0 @ a_bird))) | (((animal @ X0)) != $true))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition])).
% 0.50/0.33 thf(f537,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != ((eats @ X0 @ a_bird))) | (((animal @ X0)) != $true)) ) | ~spl0_30),
% 0.50/0.33 inference(avatar_component_clause,[],[f536])).
% 0.50/0.33 thf(f628,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true != $true) | ($true = ((eats @ a_bird @ X0))) | (((plant @ X0)) = $false)) ) | ~spl0_18),
% 0.50/0.33 inference(constrained_superposition,[],[f378,f27])).
% 0.50/0.33 thf(f629,plain,(
% 0.50/0.33 ( ! [X0 : $i] : (($true = ((eats @ a_bird @ X0))) | (((plant @ X0)) = $false)) ) | ~spl0_18),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f628])).
% 0.50/0.33 thf(f661,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(constrained_superposition,[],[f16,f126])).
% 0.50/0.33 thf(f666,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(trivial_inequality_removal,[],[f661])).
% 0.50/0.33 thf(f753,plain,(
% 0.50/0.33 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((eats @ X1 @ a_bird))) | (((grain @ X0)) != $true) | ($true != ((animal @ a_bird))) | (((animal @ X1)) != $true) | (((plant @ X0)) = $false)) ) | ~spl0_18),
% 0.50/0.33 inference(constrained_superposition,[],[f25,f629])).
% 0.50/0.33 thf(f764,plain,(
% 0.50/0.33 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ X1 @ a_bird))) | (((grain @ X0)) != $true) | ($true != ((animal @ a_bird))) | (((animal @ X1)) != $true) | (((plant @ X0)) = $false)) ) | ~spl0_18),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f753])).
% 0.50/0.33 thf(f767,plain,(
% 0.50/0.33 ( ! [X0 : $i,X1 : $i] : (($true != ((eats @ X1 @ a_bird))) | (((grain @ X0)) != $true) | (((animal @ X1)) != $true) | (((plant @ X0)) = $false)) ) | ~spl0_18),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f764,f46])).
% 0.50/0.33 thf(f769,definition,(
% 0.50/0.33 spl0_39 <=> ! [X0 : $i] : ((((grain @ X0)) != $true) | (((plant @ X0)) = $false))),
% 0.50/0.33 introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition])).
% 0.50/0.33 thf(f770,plain,(
% 0.50/0.33 ( ! [X0 : $i] : ((((grain @ X0)) != $true) | (((plant @ X0)) = $false)) ) | ~spl0_39),
% 0.50/0.33 inference(avatar_component_clause,[],[f769])).
% 0.50/0.33 thf(f771,plain,(
% 0.50/0.33 spl0_39 | spl0_30 | ~spl0_18),
% 0.50/0.33 inference(avatar_split_clause,[],[f767,f377,f536,f769])).
% 0.50/0.33 thf(f838,plain,(
% 0.50/0.33 ($true != $true) | ($true != ((animal @ a_fox))) | (~spl0_16 | ~spl0_30)),
% 0.50/0.33 inference(constrained_superposition,[],[f537,f371])).
% 0.50/0.33 thf(f841,plain,(
% 0.50/0.33 ($true != ((animal @ a_fox))) | (~spl0_16 | ~spl0_30)),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f838])).
% 0.50/0.33 thf(f843,plain,(
% 0.50/0.33 $false | (~spl0_16 | ~spl0_30)),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f841,f42])).
% 0.50/0.33 thf(f844,plain,(
% 0.50/0.33 ~spl0_16 | ~spl0_30),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f843])).
% 0.50/0.33 thf(f846,plain,(
% 0.50/0.33 ($true != $true) | ($false = ((plant @ a_grain))) | ~spl0_39),
% 0.50/0.33 inference(constrained_superposition,[],[f770,f14])).
% 0.50/0.33 thf(f853,plain,(
% 0.50/0.33 ($false = ((plant @ a_grain))) | ~spl0_39),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f846])).
% 0.50/0.33 thf(f855,plain,(
% 0.50/0.33 ($true = $false) | ~spl0_39),
% 0.50/0.33 inference(constrained_superposition,[],[f853,f54])).
% 0.50/0.33 thf(f865,plain,(
% 0.50/0.33 $false | ~spl0_39),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f855])).
% 0.50/0.33 thf(f866,plain,(
% 0.50/0.33 ~spl0_39),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f865])).
% 0.50/0.33 thf(f872,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f666,f42])).
% 0.50/0.33 thf(f876,plain,(
% 0.50/0.33 ( ! [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.50/0.33 inference(forward_subsumption_resolution,[],[f872,f38])).
% 0.50/0.33 thf(f879,plain,(
% 0.50/0.33 spl0_12 | spl0_10 | spl0_13),
% 0.50/0.33 inference(avatar_split_clause,[],[f876,f358,f347,f354])).
% 0.50/0.33 thf(f895,plain,(
% 0.50/0.33 ($true != $true) | (((fox @ a_fox)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_12),
% 0.50/0.33 inference(constrained_superposition,[],[f20,f356])).
% 0.50/0.33 thf(f896,plain,(
% 0.50/0.33 (((fox @ a_fox)) != $true) | (((wolf @ a_wolf)) != $true) | ~spl0_12),
% 0.50/0.33 inference(trivial_inequality_removal,[],[f895])).
% 0.50/0.33 thf(f900,plain,(
% 0.50/0.33 (((wolf @ a_wolf)) != $true) | ~spl0_12),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f896,f11])).
% 0.50/0.33 thf(f908,plain,(
% 0.50/0.33 $false | ~spl0_12),
% 0.50/0.33 inference(forward_subsumption_resolution,[],[f900,f10])).
% 0.50/0.33 thf(f909,plain,(
% 0.50/0.33 ~spl0_12),
% 0.50/0.33 inference(avatar_contradiction_clause,[],[f908])).
% 0.50/0.33 cnf(s9, plain, spl0_14 | spl0_16 | spl0_17, inference(sat_conversion,[],[f375])).
% 0.50/0.33 cnf(s11, plain, spl0_18 | spl0_20 | spl0_21, inference(sat_conversion,[],[f390])).
% 0.50/0.33 cnf(s16, plain, ~spl0_10, inference(sat_conversion,[],[f434])).
% 0.50/0.33 cnf(s18, plain, ~spl0_13 | ~spl0_14, inference(sat_conversion,[],[f460])).
% 0.50/0.33 cnf(s20, plain, ~spl0_17 | ~spl0_18, inference(sat_conversion,[],[f489])).
% 0.50/0.33 cnf(s21, plain, ~spl0_21, inference(sat_conversion,[],[f506])).
% 0.50/0.33 cnf(s24, plain, ~spl0_20, inference(sat_conversion,[],[f534])).
% 0.50/0.33 cnf(s35, plain, ~spl0_18 | spl0_30 | spl0_39, inference(sat_conversion,[],[f771])).
% 0.50/0.33 cnf(s36, plain, ~spl0_16 | ~spl0_30, inference(sat_conversion,[],[f844])).
% 0.50/0.33 cnf(s38, plain, ~spl0_39, inference(sat_conversion,[],[f866])).
% 0.50/0.33 cnf(s40, plain, spl0_10 | spl0_12 | spl0_13, inference(sat_conversion,[],[f879])).
% 0.50/0.33 cnf(s44, plain, ~spl0_12, inference(sat_conversion,[],[f909])).
% 0.50/0.33 cnf(s46, plain, spl0_10 | spl0_13, inference(rat,[],[s40,s44])).
% 0.50/0.33 cnf(s47, plain, ~spl0_18 | spl0_30, inference(rat,[],[s35,s38])).
% 0.50/0.33 cnf(s49, plain, spl0_13, inference(rat,[],[s46,s16])).
% 0.50/0.33 cnf(s51, plain, ~spl0_14, inference(rat,[],[s18,s49])).
% 0.50/0.33 cnf(s53, plain, spl0_18, inference(rat,[],[s11,s21,s24])).
% 0.50/0.33 cnf(s54, plain, spl0_30, inference(rat,[],[s47,s53])).
% 0.50/0.33 cnf(s55, plain, ~spl0_17, inference(rat,[],[s20,s53])).
% 0.50/0.33 cnf(s56, plain, ~spl0_16, inference(rat,[],[s36,s54])).
% 0.50/0.33 cnf(s59, plain, $false, inference(rat,[],[s9,s55,s56,s51])).
% 0.50/0.33 thf(f918,plain,(
% 0.50/0.33 $false),
% 0.50/0.33 inference(avatar_sat_refutation,[],[s59])).
% 0.50/0.33 % SZS output end Proof for theBenchmark
% 0.50/0.33 % (1644319)------------------------------
% 0.50/0.33 % (1644319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.33 % (1644319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.33 % (1644319)CaDiCaL version: 2.1.3
% 0.50/0.33 % (1644319)Termination reason: Refutation
% 0.50/0.33 % (1644319)Time elapsed: 0.041 s
% 0.50/0.33 % (1644319)Peak memory usage: 13 MB
% 0.50/0.33 % (1644319)Instructions burned: 75 (million)
% 0.50/0.33 % (1644297)Success in time 0.12 s
% 0.50/0.33 % Vampire exiting
%------------------------------------------------------------------------------