%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ031^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:20:50 AM UTC 2026
% Result : Theorem 0.50s 0.31s
% Output : Refutation 0.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 10
% Syntax : Number of formulae : 141 ( 30 unt; 0 typ; 9 def)
% Number of atoms : 1818 ( 440 equ; 0 cnn)
% Maximal formula atoms : 69 ( 12 avg)
% Number of connectives : 1907 ( 488 ~; 440 |; 150 &; 820 @)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 31 ( 28 usr; 17 con; 0-2 aty)
% Number of variables : 272 ( 0 sgn 272 !; 0 ?; 272 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
eats: $i > $i > $o ).
thf(func_def_1,type,
grain: $i > $o ).
thf(func_def_2,type,
animal: $i > $o ).
thf(func_def_3,type,
snail: $i > $o ).
thf(func_def_4,type,
sf: $i > $i ).
thf(func_def_5,type,
plant: $i > $o ).
thf(func_def_6,type,
caterpillar: $i > $o ).
thf(func_def_7,type,
cf: $i > $i ).
thf(func_def_8,type,
bird: $i > $o ).
thf(func_def_9,type,
wolf: $i > $o ).
thf(func_def_10,type,
fox: $i > $o ).
thf(func_def_11,type,
msmaller: $i > $i > $o ).
thf(f1,conjecture,
~ ( ! [X3: $i] :
( ~ ( snail @ X3 )
| ( eats @ X3 @ ( sf @ X3 ) ) )
& ! [X5: $i] :
( ~ ( caterpillar @ X5 )
| ( plant @ ( cf @ X5 ) ) )
& ! [X5: $i] :
( ~ ( caterpillar @ X5 )
| ( eats @ X5 @ ( cf @ X5 ) ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( snail @ X0 ) )
& ! [X4: $i,X2: $i,X3: $i,X1: $i] :
( ~ ( plant @ X4 )
| ~ ( plant @ X2 )
| ~ ( animal @ X1 )
| ( eats @ X1 @ X2 )
| ~ ( msmaller @ X3 @ X1 )
| ~ ( eats @ X3 @ X4 )
| ~ ( animal @ X3 )
| ( eats @ X1 @ X3 ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( wolf @ X0 ) )
& ( grain @ a_grain )
& ! [X3: $i] :
( ~ ( snail @ X3 )
| ( plant @ ( sf @ X3 ) ) )
& ! [X8: $i,X7: $i] :
( ~ ( wolf @ X8 )
| ~ ( eats @ X8 @ X7 )
| ~ ( fox @ X7 ) )
& ! [X7: $i,X8: $i] :
( ( msmaller @ X7 @ X8 )
| ~ ( wolf @ X8 )
| ~ ( fox @ X7 ) )
& ! [X9: $i,X8: $i] :
( ~ ( wolf @ X8 )
| ~ ( eats @ X8 @ X9 )
| ~ ( grain @ X9 ) )
& ( snail @ a_snail )
& ! [X3: $i,X6: $i] :
( ~ ( snail @ X3 )
| ~ ( bird @ X6 )
| ~ ( eats @ X6 @ X3 ) )
& ! [X0: $i] :
( ~ ( caterpillar @ X0 )
| ( animal @ X0 ) )
& ! [X0: $i] :
( ~ ( grain @ X0 )
| ( plant @ X0 ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( bird @ X0 ) )
& ! [X6: $i,X7: $i] :
( ~ ( bird @ X6 )
| ~ ( fox @ X7 )
| ( msmaller @ X6 @ X7 ) )
& ! [X6: $i,X5: $i] :
( ~ ( caterpillar @ X5 )
| ( msmaller @ X5 @ X6 )
| ~ ( bird @ X6 ) )
& ! [X5: $i,X6: $i] :
( ~ ( caterpillar @ X5 )
| ~ ( bird @ X6 )
| ( eats @ X6 @ X5 ) )
& ( caterpillar @ a_caterpillar )
& ( bird @ a_bird )
& ! [X3: $i,X6: $i] :
( ~ ( snail @ X3 )
| ( msmaller @ X3 @ X6 )
| ~ ( bird @ X6 ) )
& ! [X0: $i] :
( ~ ( fox @ X0 )
| ( animal @ X0 ) )
& ( fox @ a_fox )
& ! [X1: $i,X10: $i,X9: $i] :
( ~ ( eats @ X1 @ X10 )
| ~ ( grain @ X9 )
| ~ ( animal @ X1 )
| ~ ( animal @ X10 )
| ~ ( eats @ X10 @ X9 ) )
& ( wolf @ a_wolf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cPUZ031_1) ).
thf(f2,negated_conjecture,
~ ~ ( ! [X3: $i] :
( ~ ( snail @ X3 )
| ( eats @ X3 @ ( sf @ X3 ) ) )
& ! [X5: $i] :
( ~ ( caterpillar @ X5 )
| ( plant @ ( cf @ X5 ) ) )
& ! [X5: $i] :
( ~ ( caterpillar @ X5 )
| ( eats @ X5 @ ( cf @ X5 ) ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( snail @ X0 ) )
& ! [X4: $i,X2: $i,X3: $i,X1: $i] :
( ~ ( plant @ X4 )
| ~ ( plant @ X2 )
| ~ ( animal @ X1 )
| ( eats @ X1 @ X2 )
| ~ ( msmaller @ X3 @ X1 )
| ~ ( eats @ X3 @ X4 )
| ~ ( animal @ X3 )
| ( eats @ X1 @ X3 ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( wolf @ X0 ) )
& ( grain @ a_grain )
& ! [X3: $i] :
( ~ ( snail @ X3 )
| ( plant @ ( sf @ X3 ) ) )
& ! [X8: $i,X7: $i] :
( ~ ( wolf @ X8 )
| ~ ( eats @ X8 @ X7 )
| ~ ( fox @ X7 ) )
& ! [X7: $i,X8: $i] :
( ( msmaller @ X7 @ X8 )
| ~ ( wolf @ X8 )
| ~ ( fox @ X7 ) )
& ! [X9: $i,X8: $i] :
( ~ ( wolf @ X8 )
| ~ ( eats @ X8 @ X9 )
| ~ ( grain @ X9 ) )
& ( snail @ a_snail )
& ! [X3: $i,X6: $i] :
( ~ ( snail @ X3 )
| ~ ( bird @ X6 )
| ~ ( eats @ X6 @ X3 ) )
& ! [X0: $i] :
( ~ ( caterpillar @ X0 )
| ( animal @ X0 ) )
& ! [X0: $i] :
( ~ ( grain @ X0 )
| ( plant @ X0 ) )
& ! [X0: $i] :
( ( animal @ X0 )
| ~ ( bird @ X0 ) )
& ! [X6: $i,X7: $i] :
( ~ ( bird @ X6 )
| ~ ( fox @ X7 )
| ( msmaller @ X6 @ X7 ) )
& ! [X6: $i,X5: $i] :
( ~ ( caterpillar @ X5 )
| ( msmaller @ X5 @ X6 )
| ~ ( bird @ X6 ) )
& ! [X5: $i,X6: $i] :
( ~ ( caterpillar @ X5 )
| ~ ( bird @ X6 )
| ( eats @ X6 @ X5 ) )
& ( caterpillar @ a_caterpillar )
& ( bird @ a_bird )
& ! [X3: $i,X6: $i] :
( ~ ( snail @ X3 )
| ( msmaller @ X3 @ X6 )
| ~ ( bird @ X6 ) )
& ! [X0: $i] :
( ~ ( fox @ X0 )
| ( animal @ X0 ) )
& ( fox @ a_fox )
& ! [X1: $i,X10: $i,X9: $i] :
( ~ ( eats @ X1 @ X10 )
| ~ ( grain @ X9 )
| ~ ( animal @ X1 )
| ~ ( animal @ X10 )
| ~ ( eats @ X10 @ X9 ) )
& ( wolf @ a_wolf ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ~ ( ! [X0: $i] :
( ~ ( snail @ X0 )
| ( eats @ X0 @ ( sf @ X0 ) ) )
& ! [X1: $i] :
( ~ ( caterpillar @ X1 )
| ( plant @ ( cf @ X1 ) ) )
& ! [X2: $i] :
( ~ ( caterpillar @ X2 )
| ( eats @ X2 @ ( cf @ X2 ) ) )
& ! [X3: $i] :
( ( animal @ X3 )
| ~ ( snail @ X3 ) )
& ! [X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ ( plant @ X4 )
| ~ ( plant @ X5 )
| ~ ( animal @ X7 )
| ( eats @ X7 @ X5 )
| ~ ( msmaller @ X6 @ X7 )
| ~ ( eats @ X6 @ X4 )
| ~ ( animal @ X6 )
| ( eats @ X7 @ X6 ) )
& ! [X8: $i] :
( ( animal @ X8 )
| ~ ( wolf @ X8 ) )
& ( grain @ a_grain )
& ! [X9: $i] :
( ~ ( snail @ X9 )
| ( plant @ ( sf @ X9 ) ) )
& ! [X10: $i,X11: $i] :
( ~ ( wolf @ X10 )
| ~ ( eats @ X10 @ X11 )
| ~ ( fox @ X11 ) )
& ! [X12: $i,X13: $i] :
( ( msmaller @ X12 @ X13 )
| ~ ( wolf @ X13 )
| ~ ( fox @ X12 ) )
& ! [X14: $i,X15: $i] :
( ~ ( wolf @ X15 )
| ~ ( eats @ X15 @ X14 )
| ~ ( grain @ X14 ) )
& ( snail @ a_snail )
& ! [X16: $i,X17: $i] :
( ~ ( snail @ X16 )
| ~ ( bird @ X17 )
| ~ ( eats @ X17 @ X16 ) )
& ! [X18: $i] :
( ~ ( caterpillar @ X18 )
| ( animal @ X18 ) )
& ! [X19: $i] :
( ~ ( grain @ X19 )
| ( plant @ X19 ) )
& ! [X20: $i] :
( ( animal @ X20 )
| ~ ( bird @ X20 ) )
& ! [X21: $i,X22: $i] :
( ~ ( bird @ X21 )
| ~ ( fox @ X22 )
| ( msmaller @ X21 @ X22 ) )
& ! [X23: $i,X24: $i] :
( ~ ( caterpillar @ X24 )
| ( msmaller @ X24 @ X23 )
| ~ ( bird @ X23 ) )
& ! [X25: $i,X26: $i] :
( ~ ( caterpillar @ X25 )
| ~ ( bird @ X26 )
| ( eats @ X26 @ X25 ) )
& ( caterpillar @ a_caterpillar )
& ( bird @ a_bird )
& ! [X27: $i,X28: $i] :
( ~ ( snail @ X27 )
| ( msmaller @ X27 @ X28 )
| ~ ( bird @ X28 ) )
& ! [X29: $i] :
( ~ ( fox @ X29 )
| ( animal @ X29 ) )
& ( fox @ a_fox )
& ! [X30: $i,X31: $i,X32: $i] :
( ~ ( eats @ X30 @ X31 )
| ~ ( grain @ X32 )
| ~ ( animal @ X30 )
| ~ ( animal @ X31 )
| ~ ( eats @ X31 @ X32 ) )
& ( wolf @ a_wolf ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
~ ~ ( ! [X0: $i] :
( ( ( snail @ X0 )
!= $true )
| ( ( eats @ X0 @ ( sf @ X0 ) )
= $true ) )
& ! [X1: $i] :
( ( ( caterpillar @ X1 )
!= $true )
| ( $true
= ( plant @ ( cf @ X1 ) ) ) )
& ! [X2: $i] :
( ( $true
!= ( caterpillar @ X2 ) )
| ( ( eats @ X2 @ ( cf @ X2 ) )
= $true ) )
& ! [X3: $i] :
( ( ( animal @ X3 )
= $true )
| ( ( snail @ X3 )
!= $true ) )
& ! [X4: $i,X5: $i,X6: $i,X7: $i] :
( ( ( plant @ X4 )
!= $true )
| ( $true
!= ( plant @ X5 ) )
| ( ( animal @ X7 )
!= $true )
| ( ( eats @ X7 @ X5 )
= $true )
| ( ( msmaller @ X6 @ X7 )
!= $true )
| ( $true
!= ( eats @ X6 @ X4 ) )
| ( $true
!= ( animal @ X6 ) )
| ( $true
= ( eats @ X7 @ X6 ) ) )
& ! [X8: $i] :
( ( ( animal @ X8 )
= $true )
| ( ( wolf @ X8 )
!= $true ) )
& ( ( grain @ a_grain )
= $true )
& ! [X9: $i] :
( ( $true
!= ( snail @ X9 ) )
| ( $true
= ( plant @ ( sf @ X9 ) ) ) )
& ! [X10: $i,X11: $i] :
( ( $true
!= ( wolf @ X10 ) )
| ( $true
!= ( eats @ X10 @ X11 ) )
| ( ( fox @ X11 )
!= $true ) )
& ! [X12: $i,X13: $i] :
( ( ( msmaller @ X12 @ X13 )
= $true )
| ( ( wolf @ X13 )
!= $true )
| ( $true
!= ( fox @ X12 ) ) )
& ! [X14: $i,X15: $i] :
( ( $true
!= ( wolf @ X15 ) )
| ( $true
!= ( eats @ X15 @ X14 ) )
| ( $true
!= ( grain @ X14 ) ) )
& ( ( snail @ a_snail )
= $true )
& ! [X16: $i,X17: $i] :
( ( ( snail @ X16 )
!= $true )
| ( ( bird @ X17 )
!= $true )
| ( ( eats @ X17 @ X16 )
!= $true ) )
& ! [X18: $i] :
( ( $true
!= ( caterpillar @ X18 ) )
| ( ( animal @ X18 )
= $true ) )
& ! [X19: $i] :
( ( ( grain @ X19 )
!= $true )
| ( $true
= ( plant @ X19 ) ) )
& ! [X20: $i] :
( ( $true
= ( animal @ X20 ) )
| ( $true
!= ( bird @ X20 ) ) )
& ! [X21: $i,X22: $i] :
( ( ( bird @ X21 )
!= $true )
| ( ( fox @ X22 )
!= $true )
| ( ( msmaller @ X21 @ X22 )
= $true ) )
& ! [X23: $i,X24: $i] :
( ( $true
!= ( caterpillar @ X24 ) )
| ( ( msmaller @ X24 @ X23 )
= $true )
| ( ( bird @ X23 )
!= $true ) )
& ! [X25: $i,X26: $i] :
( ( ( caterpillar @ X25 )
!= $true )
| ( ( bird @ X26 )
!= $true )
| ( ( eats @ X26 @ X25 )
= $true ) )
& ( ( caterpillar @ a_caterpillar )
= $true )
& ( ( bird @ a_bird )
= $true )
& ! [X27: $i,X28: $i] :
( ( $true
!= ( snail @ X27 ) )
| ( ( msmaller @ X27 @ X28 )
= $true )
| ( ( bird @ X28 )
!= $true ) )
& ! [X29: $i] :
( ( ( fox @ X29 )
!= $true )
| ( $true
= ( animal @ X29 ) ) )
& ( ( fox @ a_fox )
= $true )
& ! [X30: $i,X31: $i,X32: $i] :
( ( $true
!= ( eats @ X30 @ X31 ) )
| ( $true
!= ( grain @ X32 ) )
| ( ( animal @ X30 )
!= $true )
| ( ( animal @ X31 )
!= $true )
| ( ( eats @ X31 @ X32 )
!= $true ) )
& ( ( wolf @ a_wolf )
= $true ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( ! [X9: $i] :
( ( $true
!= ( snail @ X9 ) )
| ( $true
= ( plant @ ( sf @ X9 ) ) ) )
& ! [X17: $i,X16: $i] :
( ( ( snail @ X16 )
!= $true )
| ( ( eats @ X17 @ X16 )
!= $true )
| ( ( bird @ X17 )
!= $true ) )
& ! [X14: $i,X15: $i] :
( ( $true
!= ( grain @ X14 ) )
| ( $true
!= ( eats @ X15 @ X14 ) )
| ( $true
!= ( wolf @ X15 ) ) )
& ! [X25: $i,X26: $i] :
( ( ( eats @ X26 @ X25 )
= $true )
| ( ( caterpillar @ X25 )
!= $true )
| ( ( bird @ X26 )
!= $true ) )
& ! [X1: $i] :
( ( ( caterpillar @ X1 )
!= $true )
| ( $true
= ( plant @ ( cf @ X1 ) ) ) )
& ! [X18: $i] :
( ( $true
!= ( caterpillar @ X18 ) )
| ( ( animal @ X18 )
= $true ) )
& ! [X28: $i,X27: $i] :
( ( ( msmaller @ X27 @ X28 )
= $true )
| ( ( bird @ X28 )
!= $true )
| ( $true
!= ( snail @ X27 ) ) )
& ( ( bird @ a_bird )
= $true )
& ! [X13: $i,X12: $i] :
( ( ( wolf @ X13 )
!= $true )
| ( ( msmaller @ X12 @ X13 )
= $true )
| ( $true
!= ( fox @ X12 ) ) )
& ! [X0: $i] :
( ( ( eats @ X0 @ ( sf @ X0 ) )
= $true )
| ( ( snail @ X0 )
!= $true ) )
& ( ( caterpillar @ a_caterpillar )
= $true )
& ! [X29: $i] :
( ( $true
= ( animal @ X29 ) )
| ( ( fox @ X29 )
!= $true ) )
& ! [X23: $i,X24: $i] :
( ( ( msmaller @ X24 @ X23 )
= $true )
| ( ( bird @ X23 )
!= $true )
| ( $true
!= ( caterpillar @ X24 ) ) )
& ! [X20: $i] :
( ( $true
= ( animal @ X20 ) )
| ( $true
!= ( bird @ X20 ) ) )
& ! [X11: $i,X10: $i] :
( ( ( fox @ X11 )
!= $true )
| ( $true
!= ( eats @ X10 @ X11 ) )
| ( $true
!= ( wolf @ X10 ) ) )
& ! [X3: $i] :
( ( ( animal @ X3 )
= $true )
| ( ( snail @ X3 )
!= $true ) )
& ! [X22: $i,X21: $i] :
( ( ( fox @ X22 )
!= $true )
| ( ( bird @ X21 )
!= $true )
| ( ( msmaller @ X21 @ X22 )
= $true ) )
& ( ( fox @ a_fox )
= $true )
& ! [X6: $i,X5: $i,X4: $i,X7: $i] :
( ( ( plant @ X4 )
!= $true )
| ( $true
= ( eats @ X7 @ X6 ) )
| ( $true
!= ( plant @ X5 ) )
| ( ( eats @ X7 @ X5 )
= $true )
| ( ( animal @ X7 )
!= $true )
| ( $true
!= ( eats @ X6 @ X4 ) )
| ( ( msmaller @ X6 @ X7 )
!= $true )
| ( $true
!= ( animal @ X6 ) ) )
& ( ( snail @ a_snail )
= $true )
& ! [X19: $i] :
( ( $true
= ( plant @ X19 ) )
| ( ( grain @ X19 )
!= $true ) )
& ( ( grain @ a_grain )
= $true )
& ! [X31: $i,X32: $i,X30: $i] :
( ( $true
!= ( eats @ X30 @ X31 ) )
| ( ( eats @ X31 @ X32 )
!= $true )
| ( ( animal @ X30 )
!= $true )
| ( ( animal @ X31 )
!= $true )
| ( $true
!= ( grain @ X32 ) ) )
& ! [X8: $i] :
( ( ( animal @ X8 )
= $true )
| ( ( wolf @ X8 )
!= $true ) )
& ! [X2: $i] :
( ( ( eats @ X2 @ ( cf @ X2 ) )
= $true )
| ( $true
!= ( caterpillar @ X2 ) ) )
& ( ( wolf @ a_wolf )
= $true ) ),
inference(flattening,[],[f4]) ).
thf(f6,plain,
( ! [X0: $i] :
( ( ( snail @ X0 )
!= $true )
| ( $true
= ( plant @ ( sf @ X0 ) ) ) )
& ! [X1: $i,X2: $i] :
( ( $true
!= ( snail @ X2 ) )
| ( ( eats @ X1 @ X2 )
!= $true )
| ( ( bird @ X1 )
!= $true ) )
& ! [X3: $i,X4: $i] :
( ( $true
!= ( grain @ X3 ) )
| ( $true
!= ( eats @ X4 @ X3 ) )
| ( ( wolf @ X4 )
!= $true ) )
& ! [X5: $i,X6: $i] :
( ( ( eats @ X6 @ X5 )
= $true )
| ( ( caterpillar @ X5 )
!= $true )
| ( ( bird @ X6 )
!= $true ) )
& ! [X7: $i] :
( ( $true
!= ( caterpillar @ X7 ) )
| ( $true
= ( plant @ ( cf @ X7 ) ) ) )
& ! [X8: $i] :
( ( ( caterpillar @ X8 )
!= $true )
| ( ( animal @ X8 )
= $true ) )
& ! [X9: $i,X10: $i] :
( ( ( msmaller @ X10 @ X9 )
= $true )
| ( $true
!= ( bird @ X9 ) )
| ( ( snail @ X10 )
!= $true ) )
& ( ( bird @ a_bird )
= $true )
& ! [X11: $i,X12: $i] :
( ( $true
!= ( wolf @ X11 ) )
| ( $true
= ( msmaller @ X12 @ X11 ) )
| ( $true
!= ( fox @ X12 ) ) )
& ! [X13: $i] :
( ( $true
= ( eats @ X13 @ ( sf @ X13 ) ) )
| ( ( snail @ X13 )
!= $true ) )
& ( ( caterpillar @ a_caterpillar )
= $true )
& ! [X14: $i] :
( ( ( animal @ X14 )
= $true )
| ( ( fox @ X14 )
!= $true ) )
& ! [X15: $i,X16: $i] :
( ( ( msmaller @ X16 @ X15 )
= $true )
| ( $true
!= ( bird @ X15 ) )
| ( $true
!= ( caterpillar @ X16 ) ) )
& ! [X17: $i] :
( ( $true
= ( animal @ X17 ) )
| ( ( bird @ X17 )
!= $true ) )
& ! [X18: $i,X19: $i] :
( ( $true
!= ( fox @ X18 ) )
| ( ( eats @ X19 @ X18 )
!= $true )
| ( $true
!= ( wolf @ X19 ) ) )
& ! [X20: $i] :
( ( $true
= ( animal @ X20 ) )
| ( $true
!= ( snail @ X20 ) ) )
& ! [X21: $i,X22: $i] :
( ( $true
!= ( fox @ X21 ) )
| ( ( bird @ X22 )
!= $true )
| ( ( msmaller @ X22 @ X21 )
= $true ) )
& ( ( fox @ a_fox )
= $true )
& ! [X23: $i,X24: $i,X25: $i,X26: $i] :
( ( ( plant @ X25 )
!= $true )
| ( $true
= ( eats @ X26 @ X23 ) )
| ( ( plant @ X24 )
!= $true )
| ( ( eats @ X26 @ X24 )
= $true )
| ( ( animal @ X26 )
!= $true )
| ( ( eats @ X23 @ X25 )
!= $true )
| ( ( msmaller @ X23 @ X26 )
!= $true )
| ( ( animal @ X23 )
!= $true ) )
& ( ( snail @ a_snail )
= $true )
& ! [X27: $i] :
( ( ( plant @ X27 )
= $true )
| ( ( grain @ X27 )
!= $true ) )
& ( ( grain @ a_grain )
= $true )
& ! [X28: $i,X29: $i,X30: $i] :
( ( ( eats @ X30 @ X28 )
!= $true )
| ( ( eats @ X28 @ X29 )
!= $true )
| ( ( animal @ X30 )
!= $true )
| ( $true
!= ( animal @ X28 ) )
| ( $true
!= ( grain @ X29 ) ) )
& ! [X31: $i] :
( ( ( animal @ X31 )
= $true )
| ( ( wolf @ X31 )
!= $true ) )
& ! [X32: $i] :
( ( ( eats @ X32 @ ( cf @ X32 ) )
= $true )
| ( ( caterpillar @ X32 )
!= $true ) )
& ( ( wolf @ a_wolf )
= $true ) ),
inference(rectify,[],[f5]) ).
thf(f7,plain,
( ( wolf @ a_wolf )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f9,plain,
! [X31: $i] :
( ( ( wolf @ X31 )
!= $true )
| ( ( animal @ X31 )
= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f10,plain,
! [X28: $i,X29: $i,X30: $i] :
( ( ( eats @ X30 @ X28 )
!= $true )
| ( ( animal @ X30 )
!= $true )
| ( $true
!= ( animal @ X28 ) )
| ( ( eats @ X28 @ X29 )
!= $true )
| ( $true
!= ( grain @ X29 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f11,plain,
( ( grain @ a_grain )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f12,plain,
! [X27: $i] :
( ( ( grain @ X27 )
!= $true )
| ( ( plant @ X27 )
= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f13,plain,
( ( snail @ a_snail )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f14,plain,
! [X26: $i,X24: $i,X25: $i,X23: $i] :
( ( ( msmaller @ X23 @ X26 )
!= $true )
| ( ( plant @ X24 )
!= $true )
| ( $true
= ( eats @ X26 @ X23 ) )
| ( ( eats @ X26 @ X24 )
= $true )
| ( ( eats @ X23 @ X25 )
!= $true )
| ( ( animal @ X23 )
!= $true )
| ( ( animal @ X26 )
!= $true )
| ( ( plant @ X25 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f15,plain,
( ( fox @ a_fox )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f16,plain,
! [X21: $i,X22: $i] :
( ( $true
!= ( fox @ X21 ) )
| ( ( msmaller @ X22 @ X21 )
= $true )
| ( ( bird @ X22 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f17,plain,
! [X20: $i] :
( ( $true
!= ( snail @ X20 ) )
| ( $true
= ( animal @ X20 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f18,plain,
! [X18: $i,X19: $i] :
( ( ( eats @ X19 @ X18 )
!= $true )
| ( $true
!= ( wolf @ X19 ) )
| ( $true
!= ( fox @ X18 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f19,plain,
! [X17: $i] :
( ( ( bird @ X17 )
!= $true )
| ( $true
= ( animal @ X17 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f21,plain,
! [X14: $i] :
( ( ( fox @ X14 )
!= $true )
| ( ( animal @ X14 )
= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f23,plain,
! [X13: $i] :
( ( ( snail @ X13 )
!= $true )
| ( $true
= ( eats @ X13 @ ( sf @ X13 ) ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f24,plain,
! [X11: $i,X12: $i] :
( ( $true
!= ( fox @ X12 ) )
| ( $true
!= ( wolf @ X11 ) )
| ( $true
= ( msmaller @ X12 @ X11 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f25,plain,
( ( bird @ a_bird )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f26,plain,
! [X10: $i,X9: $i] :
( ( $true
!= ( bird @ X9 ) )
| ( ( snail @ X10 )
!= $true )
| ( ( msmaller @ X10 @ X9 )
= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f30,plain,
! [X3: $i,X4: $i] :
( ( $true
!= ( eats @ X4 @ X3 ) )
| ( ( wolf @ X4 )
!= $true )
| ( $true
!= ( grain @ X3 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f31,plain,
! [X2: $i,X1: $i] :
( ( ( eats @ X1 @ X2 )
!= $true )
| ( $true
!= ( snail @ X2 ) )
| ( ( bird @ X1 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f32,plain,
! [X0: $i] :
( ( ( snail @ X0 )
!= $true )
| ( $true
= ( plant @ ( sf @ X0 ) ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f35,plain,
( ( $true
= ( animal @ a_wolf ) )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f9,f7]) ).
thf(f36,plain,
( $true
= ( animal @ a_wolf ) ),
inference(trivial_inequality_removal,[],[f35]) ).
thf(f37,plain,
( ( ( plant @ a_grain )
= $true )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f12,f11]) ).
thf(f38,plain,
( ( plant @ a_grain )
= $true ),
inference(trivial_inequality_removal,[],[f37]) ).
thf(f39,plain,
( ( $true != $true )
| ( $true
= ( animal @ a_snail ) ) ),
inference(constrained_superposition,[],[f17,f13]) ).
thf(f40,plain,
( $true
= ( animal @ a_snail ) ),
inference(trivial_inequality_removal,[],[f39]) ).
thf(f41,plain,
( ( ( animal @ a_bird )
= $true )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f19,f25]) ).
thf(f42,plain,
( ( animal @ a_bird )
= $true ),
inference(trivial_inequality_removal,[],[f41]) ).
thf(f43,plain,
( ( $true != $true )
| ( $true
= ( animal @ a_fox ) ) ),
inference(constrained_superposition,[],[f21,f15]) ).
thf(f44,plain,
( $true
= ( animal @ a_fox ) ),
inference(trivial_inequality_removal,[],[f43]) ).
thf(f49,plain,
( ( $true != $true )
| ( ( plant @ ( sf @ a_snail ) )
= $true ) ),
inference(constrained_superposition,[],[f32,f13]) ).
thf(f50,plain,
( ( plant @ ( sf @ a_snail ) )
= $true ),
inference(trivial_inequality_removal,[],[f49]) ).
thf(f53,plain,
( ( ( eats @ a_snail @ ( sf @ a_snail ) )
= $true )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f23,f13]) ).
thf(f54,plain,
( ( eats @ a_snail @ ( sf @ a_snail ) )
= $true ),
inference(trivial_inequality_removal,[],[f53]) ).
thf(f55,plain,
! [X0: $i] :
( ( ( bird @ X0 )
!= $true )
| ( $true != $true )
| ( $true
= ( msmaller @ X0 @ a_fox ) ) ),
inference(constrained_superposition,[],[f16,f15]) ).
thf(f56,plain,
! [X0: $i] :
( ( ( bird @ X0 )
!= $true )
| ( $true
= ( msmaller @ X0 @ a_fox ) ) ),
inference(trivial_inequality_removal,[],[f55]) ).
thf(f57,plain,
( ( ( msmaller @ a_bird @ a_fox )
= $true )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f56,f25]) ).
thf(f58,plain,
( ( msmaller @ a_bird @ a_fox )
= $true ),
inference(trivial_inequality_removal,[],[f57]) ).
thf(f85,plain,
! [X0: $i] :
( ( $true != $true )
| ( ( msmaller @ a_fox @ X0 )
= $true )
| ( ( wolf @ X0 )
!= $true ) ),
inference(constrained_superposition,[],[f24,f15]) ).
thf(f86,plain,
! [X0: $i] :
( ( ( wolf @ X0 )
!= $true )
| ( ( msmaller @ a_fox @ X0 )
= $true ) ),
inference(trivial_inequality_removal,[],[f85]) ).
thf(f87,plain,
( ( $true
= ( msmaller @ a_fox @ a_wolf ) )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f86,f7]) ).
thf(f88,plain,
( $true
= ( msmaller @ a_fox @ a_wolf ) ),
inference(trivial_inequality_removal,[],[f87]) ).
thf(f89,plain,
! [X0: $i] :
( ( ( snail @ X0 )
!= $true )
| ( ( msmaller @ X0 @ a_bird )
= $true )
| ( $true != $true ) ),
inference(constrained_superposition,[],[f26,f25]) ).
thf(f90,plain,
! [X0: $i] :
( ( ( snail @ X0 )
!= $true )
| ( ( msmaller @ X0 @ a_bird )
= $true ) ),
inference(trivial_inequality_removal,[],[f89]) ).
thf(f91,plain,
( ( $true != $true )
| ( $true
= ( msmaller @ a_snail @ a_bird ) ) ),
inference(constrained_superposition,[],[f90,f13]) ).
thf(f92,plain,
( $true
= ( msmaller @ a_snail @ a_bird ) ),
inference(trivial_inequality_removal,[],[f91]) ).
thf(f179,plain,
! [X0: $i,X1: $i] :
( ( ( eats @ a_snail @ X1 )
!= $true )
| ( $true
!= ( animal @ a_snail ) )
| ( $true != $true )
| ( ( eats @ a_bird @ X0 )
= $true )
| ( ( plant @ X1 )
!= $true )
| ( ( plant @ X0 )
!= $true )
| ( ( animal @ a_bird )
!= $true )
| ( $true
= ( eats @ a_bird @ a_snail ) ) ),
inference(constrained_superposition,[],[f14,f92]) ).
thf(f180,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X0 )
!= $true )
| ( ( eats @ a_fox @ X0 )
= $true )
| ( ( animal @ a_bird )
!= $true )
| ( $true != $true )
| ( $true
= ( eats @ a_fox @ a_bird ) )
| ( $true
!= ( animal @ a_fox ) )
| ( ( plant @ X1 )
!= $true )
| ( $true
!= ( eats @ a_bird @ X1 ) ) ),
inference(constrained_superposition,[],[f14,f58]) ).
thf(f181,plain,
! [X0: $i,X1: $i] :
( ( ( eats @ a_wolf @ X0 )
= $true )
| ( ( plant @ X1 )
!= $true )
| ( $true
!= ( eats @ a_fox @ X1 ) )
| ( $true != $true )
| ( $true
!= ( animal @ a_fox ) )
| ( ( eats @ a_wolf @ a_fox )
= $true )
| ( $true
!= ( animal @ a_wolf ) )
| ( ( plant @ X0 )
!= $true ) ),
inference(constrained_superposition,[],[f14,f88]) ).
thf(f182,plain,
! [X0: $i,X1: $i] :
( ( $true
!= ( animal @ a_fox ) )
| ( ( plant @ X0 )
!= $true )
| ( $true
!= ( animal @ a_wolf ) )
| ( ( eats @ a_wolf @ X0 )
= $true )
| ( ( eats @ a_wolf @ a_fox )
= $true )
| ( $true
!= ( eats @ a_fox @ X1 ) )
| ( ( plant @ X1 )
!= $true ) ),
inference(trivial_inequality_removal,[],[f181]) ).
thf(f184,plain,
! [X0: $i,X1: $i] :
( ( $true
= ( eats @ a_bird @ a_snail ) )
| ( $true
!= ( animal @ a_snail ) )
| ( ( animal @ a_bird )
!= $true )
| ( ( eats @ a_snail @ X1 )
!= $true )
| ( ( plant @ X0 )
!= $true )
| ( ( eats @ a_bird @ X0 )
= $true )
| ( ( plant @ X1 )
!= $true ) ),
inference(trivial_inequality_removal,[],[f179]) ).
thf(f185,plain,
! [X0: $i,X1: $i] :
( ( $true
= ( eats @ a_fox @ a_bird ) )
| ( $true
!= ( eats @ a_bird @ X1 ) )
| ( $true
!= ( animal @ a_fox ) )
| ( ( plant @ X0 )
!= $true )
| ( ( plant @ X1 )
!= $true )
| ( ( eats @ a_fox @ X0 )
= $true )
| ( ( animal @ a_bird )
!= $true ) ),
inference(trivial_inequality_removal,[],[f180]) ).
thf(f186,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X1 )
!= $true )
| ( ( eats @ a_wolf @ a_fox )
= $true )
| ( $true
!= ( animal @ a_wolf ) )
| ( ( eats @ a_wolf @ X0 )
= $true )
| ( $true
!= ( eats @ a_fox @ X1 ) )
| ( ( plant @ X0 )
!= $true ) ),
inference(forward_subsumption_resolution,[],[f182,f44]) ).
thf(f187,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X0 )
!= $true )
| ( ( plant @ X1 )
!= $true )
| ( $true
= ( eats @ a_bird @ a_snail ) )
| ( ( animal @ a_bird )
!= $true )
| ( ( eats @ a_snail @ X1 )
!= $true )
| ( ( eats @ a_bird @ X0 )
= $true ) ),
inference(forward_subsumption_resolution,[],[f184,f40]) ).
thf(f188,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X0 )
!= $true )
| ( ( plant @ X1 )
!= $true )
| ( $true
= ( eats @ a_fox @ a_bird ) )
| ( ( animal @ a_bird )
!= $true )
| ( $true
!= ( eats @ a_bird @ X1 ) )
| ( ( eats @ a_fox @ X0 )
= $true ) ),
inference(forward_subsumption_resolution,[],[f185,f44]) ).
thf(f189,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X1 )
!= $true )
| ( ( eats @ a_wolf @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true )
| ( $true
!= ( eats @ a_fox @ X1 ) )
| ( ( eats @ a_wolf @ a_fox )
= $true ) ),
inference(forward_subsumption_resolution,[],[f186,f36]) ).
thf(f190,plain,
! [X0: $i,X1: $i] :
( ( ( eats @ a_bird @ X0 )
= $true )
| ( $true
= ( eats @ a_bird @ a_snail ) )
| ( ( plant @ X0 )
!= $true )
| ( ( eats @ a_snail @ X1 )
!= $true )
| ( ( plant @ X1 )
!= $true ) ),
inference(forward_subsumption_resolution,[],[f187,f42]) ).
thf(f191,plain,
! [X0: $i,X1: $i] :
( ( ( plant @ X1 )
!= $true )
| ( ( eats @ a_fox @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true )
| ( $true
= ( eats @ a_fox @ a_bird ) )
| ( $true
!= ( eats @ a_bird @ X1 ) ) ),
inference(forward_subsumption_resolution,[],[f188,f42]) ).
thf(f193,definition,
( spl0_17
<=> ( ( eats @ a_wolf @ a_fox )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
thf(f195,plain,
( ( ( eats @ a_wolf @ a_fox )
= $true )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f193]) ).
thf(f197,definition,
( spl0_18
<=> ! [X0: $i] :
( ( ( eats @ a_wolf @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
thf(f198,plain,
( ! [X0: $i] :
( ( ( plant @ X0 )
!= $true )
| ( ( eats @ a_wolf @ X0 )
= $true ) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f197]) ).
thf(f200,definition,
( spl0_19
<=> ! [X1: $i] :
( ( ( plant @ X1 )
!= $true )
| ( $true
!= ( eats @ a_fox @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
thf(f201,plain,
( ! [X1: $i] :
( ( $true
!= ( eats @ a_fox @ X1 ) )
| ( ( plant @ X1 )
!= $true ) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f200]) ).
thf(f202,plain,
( spl0_17
| spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f189,f200,f197,f193]) ).
thf(f204,definition,
( spl0_20
<=> ! [X0: $i] :
( ( ( eats @ a_bird @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
thf(f205,plain,
( ! [X0: $i] :
( ( ( plant @ X0 )
!= $true )
| ( ( eats @ a_bird @ X0 )
= $true ) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f204]) ).
thf(f207,definition,
( spl0_21
<=> ! [X1: $i] :
( ( ( eats @ a_snail @ X1 )
!= $true )
| ( ( plant @ X1 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
thf(f208,plain,
( ! [X1: $i] :
( ( ( eats @ a_snail @ X1 )
!= $true )
| ( ( plant @ X1 )
!= $true ) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f207]) ).
thf(f210,definition,
( spl0_22
<=> ( $true
= ( eats @ a_bird @ a_snail ) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
thf(f212,plain,
( ( $true
= ( eats @ a_bird @ a_snail ) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f210]) ).
thf(f213,plain,
( spl0_20
| spl0_21
| spl0_22 ),
inference(avatar_split_clause,[],[f190,f210,f207,f204]) ).
thf(f215,definition,
( spl0_23
<=> ! [X0: $i] :
( ( ( eats @ a_fox @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
thf(f216,plain,
( ! [X0: $i] :
( ( ( eats @ a_fox @ X0 )
= $true )
| ( ( plant @ X0 )
!= $true ) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f215]) ).
thf(f218,definition,
( spl0_24
<=> ! [X1: $i] :
( ( ( plant @ X1 )
!= $true )
| ( $true
!= ( eats @ a_bird @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
thf(f219,plain,
( ! [X1: $i] :
( ( $true
!= ( eats @ a_bird @ X1 ) )
| ( ( plant @ X1 )
!= $true ) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f218]) ).
thf(f221,definition,
( spl0_25
<=> ( $true
= ( eats @ a_fox @ a_bird ) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
thf(f223,plain,
( ( $true
= ( eats @ a_fox @ a_bird ) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f221]) ).
thf(f224,plain,
( spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f191,f221,f218,f215]) ).
thf(f228,plain,
( ( ( fox @ a_fox )
!= $true )
| ( ( wolf @ a_wolf )
!= $true )
| ( $true != $true )
| ~ spl0_17 ),
inference(constrained_superposition,[],[f18,f195]) ).
thf(f229,plain,
( ( ( wolf @ a_wolf )
!= $true )
| ( ( fox @ a_fox )
!= $true )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f228]) ).
thf(f233,plain,
( ( ( fox @ a_fox )
!= $true )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f229,f7]) ).
thf(f245,plain,
( $false
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f233,f15]) ).
thf(f246,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f245]) ).
thf(f248,plain,
( ( $true != $true )
| ( ( eats @ a_wolf @ a_grain )
= $true )
| ~ spl0_18 ),
inference(constrained_superposition,[],[f198,f38]) ).
thf(f253,plain,
( ( ( eats @ a_wolf @ a_grain )
= $true )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f248]) ).
thf(f256,plain,
( ( $true != $true )
| ( ( grain @ a_grain )
!= $true )
| ( ( wolf @ a_wolf )
!= $true )
| ~ spl0_18 ),
inference(constrained_superposition,[],[f30,f253]) ).
thf(f261,plain,
( ( ( grain @ a_grain )
!= $true )
| ( ( wolf @ a_wolf )
!= $true )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f256]) ).
thf(f269,plain,
( ( ( wolf @ a_wolf )
!= $true )
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f261,f11]) ).
thf(f278,plain,
( $false
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f269,f7]) ).
thf(f279,plain,
~ spl0_18,
inference(avatar_contradiction_clause,[],[f278]) ).
thf(f280,plain,
( ! [X1: $i] :
( ( plant @ X1 )
!= $true )
| ~ spl0_19
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f201,f216]) ).
thf(f283,plain,
( ( $true != $true )
| ~ spl0_19
| ~ spl0_23 ),
inference(constrained_superposition,[],[f280,f50]) ).
thf(f288,plain,
( $false
| ~ spl0_19
| ~ spl0_23 ),
inference(trivial_inequality_removal,[],[f283]) ).
thf(f289,plain,
( ~ spl0_19
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f288]) ).
thf(f290,plain,
( ! [X1: $i] :
( ( plant @ X1 )
!= $true )
| ~ spl0_20
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f219,f205]) ).
thf(f293,plain,
( ( $true != $true )
| ~ spl0_20
| ~ spl0_24 ),
inference(constrained_superposition,[],[f290,f50]) ).
thf(f298,plain,
( $false
| ~ spl0_20
| ~ spl0_24 ),
inference(trivial_inequality_removal,[],[f293]) ).
thf(f299,plain,
( ~ spl0_20
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f298]) ).
thf(f300,plain,
( ( ( plant @ ( sf @ a_snail ) )
!= $true )
| ( $true != $true )
| ~ spl0_21 ),
inference(constrained_superposition,[],[f208,f54]) ).
thf(f301,plain,
( ( ( plant @ ( sf @ a_snail ) )
!= $true )
| ~ spl0_21 ),
inference(trivial_inequality_removal,[],[f300]) ).
thf(f302,plain,
( $false
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f301,f50]) ).
thf(f303,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f302]) ).
thf(f305,plain,
( ( ( bird @ a_bird )
!= $true )
| ( ( snail @ a_snail )
!= $true )
| ( $true != $true )
| ~ spl0_22 ),
inference(constrained_superposition,[],[f31,f212]) ).
thf(f309,plain,
( ( ( bird @ a_bird )
!= $true )
| ( ( snail @ a_snail )
!= $true )
| ~ spl0_22 ),
inference(trivial_inequality_removal,[],[f305]) ).
thf(f312,plain,
( ( ( snail @ a_snail )
!= $true )
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f309,f25]) ).
thf(f314,plain,
( $false
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f312,f13]) ).
thf(f315,plain,
~ spl0_22,
inference(avatar_contradiction_clause,[],[f314]) ).
thf(f318,plain,
( ! [X0: $i] :
( ( ( eats @ a_bird @ X0 )
!= $true )
| ( ( grain @ X0 )
!= $true )
| ( $true != $true )
| ( $true
!= ( animal @ a_fox ) )
| ( ( animal @ a_bird )
!= $true ) )
| ~ spl0_25 ),
inference(constrained_superposition,[],[f10,f223]) ).
thf(f326,plain,
( ! [X0: $i] :
( ( $true
!= ( animal @ a_fox ) )
| ( ( animal @ a_bird )
!= $true )
| ( ( grain @ X0 )
!= $true )
| ( ( eats @ a_bird @ X0 )
!= $true ) )
| ~ spl0_25 ),
inference(trivial_inequality_removal,[],[f318]) ).
thf(f350,plain,
( ! [X0: $i] :
( ( ( animal @ a_bird )
!= $true )
| ( ( eats @ a_bird @ X0 )
!= $true )
| ( ( grain @ X0 )
!= $true ) )
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f326,f44]) ).
thf(f351,plain,
( ! [X0: $i] :
( ( ( eats @ a_bird @ X0 )
!= $true )
| ( ( grain @ X0 )
!= $true ) )
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f350,f42]) ).
thf(f352,plain,
( ( $true != $true )
| ( $true
= ( eats @ a_bird @ a_grain ) )
| ~ spl0_20 ),
inference(constrained_superposition,[],[f205,f38]) ).
thf(f355,plain,
( ( $true
= ( eats @ a_bird @ a_grain ) )
| ~ spl0_20 ),
inference(trivial_inequality_removal,[],[f352]) ).
thf(f388,plain,
( ( $true != $true )
| ( ( grain @ a_grain )
!= $true )
| ~ spl0_20
| ~ spl0_25 ),
inference(constrained_superposition,[],[f351,f355]) ).
thf(f395,plain,
( ( ( grain @ a_grain )
!= $true )
| ~ spl0_20
| ~ spl0_25 ),
inference(trivial_inequality_removal,[],[f388]) ).
thf(f397,plain,
( $false
| ~ spl0_20
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f395,f11]) ).
thf(f398,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f397]) ).
cnf(s11,plain,
( spl0_17
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f202]) ).
cnf(s12,plain,
( spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f213]) ).
cnf(s13,plain,
( spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f224]) ).
cnf(s15,plain,
~ spl0_17,
inference(sat_conversion,[],[f246]) ).
cnf(s18,plain,
~ spl0_18,
inference(sat_conversion,[],[f279]) ).
cnf(s21,plain,
( ~ spl0_19
| ~ spl0_23 ),
inference(sat_conversion,[],[f289]) ).
cnf(s24,plain,
( ~ spl0_20
| ~ spl0_24 ),
inference(sat_conversion,[],[f299]) ).
cnf(s25,plain,
~ spl0_21,
inference(sat_conversion,[],[f303]) ).
cnf(s26,plain,
~ spl0_22,
inference(sat_conversion,[],[f315]) ).
cnf(s34,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(sat_conversion,[],[f398]) ).
cnf(s35,plain,
spl0_20,
inference(rat,[],[s12,s26,s25]) ).
cnf(s36,plain,
~ spl0_25,
inference(rat,[],[s34,s35]) ).
cnf(s39,plain,
~ spl0_24,
inference(rat,[],[s24,s35]) ).
cnf(s40,plain,
spl0_23,
inference(rat,[],[s13,s36,s39]) ).
cnf(s41,plain,
~ spl0_19,
inference(rat,[],[s21,s40]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s11,s41,s18,s15]) ).
thf(f399,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ031^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.16 % Computer : n009.cluster.edu
% 0.12/0.16 % Model : x86_64 x86_64
% 0.12/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.16 % Memory : 8046.5625MB
% 0.12/0.16 % OS : Linux 6.8.0-71-generic
% 0.12/0.16 % CPULimit : 300
% 0.12/0.16 % WCLimit : 300
% 0.12/0.16 % DateTime : Tue Sep 29 13:21:30 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.20 Running higher-order theorem proving
% 0.12/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.50/0.31 % (3967453)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.50/0.31 % (3967459)lrs+10_16_si=on:nwc=1.5:random_seed=3060734131:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.50/0.31 % (3967459)Instruction limit reached!
% 0.50/0.31 % (3967459)------------------------------
% 0.50/0.31 % (3967459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967459)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967459)Termination reason: Instruction limit
% 0.50/0.31 % (3967459)Termination phase: Saturation
% 0.50/0.31 % (3967459)Time elapsed: 0.006 s
% 0.50/0.31 % (3967459)Peak memory usage: 12 MB
% 0.50/0.31 % (3967459)Instructions burned: 20 (million)
% 0.50/0.31 % (3967464)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.50/0.31 % (3967464)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.50/0.31 % (3967461)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=873171767:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.50/0.31 % (3967460)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=414096704:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.50/0.31 % (3967464)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=1081746076:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.50/0.31 % (3967460)Instruction limit reached!
% 0.50/0.31 % (3967460)------------------------------
% 0.50/0.31 % (3967460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967460)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967460)Termination reason: Instruction limit
% 0.50/0.31 % (3967460)Termination phase: Saturation
% 0.50/0.31 % (3967460)Time elapsed: 0.002 s
% 0.50/0.31 % (3967460)Peak memory usage: 11 MB
% 0.50/0.31 % (3967460)Instructions burned: 4 (million)
% 0.50/0.31 % (3967466)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1587503235:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.50/0.31 % (3967466)Instruction limit reached!
% 0.50/0.31 % (3967466)------------------------------
% 0.50/0.31 % (3967466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967466)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967466)Termination reason: Instruction limit
% 0.50/0.31 % (3967466)Termination phase: Saturation
% 0.50/0.31 % (3967466)Time elapsed: 0.001 s
% 0.50/0.31 % (3967466)Peak memory usage: 11 MB
% 0.50/0.31 % (3967466)Instructions burned: 4 (million)
% 0.50/0.31 % (3967462)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2624075892:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.50/0.31 % (3967472)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.31 % (3967472)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3111638487:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.50/0.31 % (3967470)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1972232624:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.50/0.31 % (3967472)Instruction limit reached!
% 0.50/0.31 % (3967472)------------------------------
% 0.50/0.31 % (3967472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967472)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967472)Termination reason: Instruction limit
% 0.50/0.31 % (3967472)Termination phase: Saturation
% 0.50/0.31 % (3967472)Time elapsed: 0.002 s
% 0.50/0.31 % (3967472)Peak memory usage: 12 MB
% 0.50/0.31 % (3967472)Instructions burned: 8 (million)
% 0.50/0.31 % (3967470)Instruction limit reached!
% 0.50/0.31 % (3967470)------------------------------
% 0.50/0.31 % (3967470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967470)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967470)Termination reason: Instruction limit
% 0.50/0.31 % (3967470)Termination phase: Saturation
% 0.50/0.31 % (3967470)Time elapsed: 0.003 s
% 0.50/0.31 % (3967470)Peak memory usage: 11 MB
% 0.50/0.31 % (3967470)Instructions burned: 5 (million)
% 0.50/0.31 % (3967458)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=276729631:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.50/0.31 % (3967463)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3914476205:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.50/0.31 % (3967462)Instruction limit reached!
% 0.50/0.31 % (3967462)------------------------------
% 0.50/0.31 % (3967462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967462)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967462)Termination reason: Instruction limit
% 0.50/0.31 % (3967462)Termination phase: Saturation
% 0.50/0.31 % (3967462)Time elapsed: 0.023 s
% 0.50/0.31 % (3967462)Peak memory usage: 11 MB
% 0.50/0.31 % (3967462)Instructions burned: 24 (million)
% 0.50/0.31 % (3967476)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=807687479:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.50/0.31 % (3967476)Instruction limit reached!
% 0.50/0.31 % (3967476)------------------------------
% 0.50/0.31 % (3967476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967476)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967476)Termination reason: Instruction limit
% 0.50/0.31 % (3967476)Termination phase: Saturation
% 0.50/0.31 % (3967476)Time elapsed: 0.004 s
% 0.50/0.31 % (3967476)Peak memory usage: 12 MB
% 0.50/0.31 % (3967476)Instructions burned: 14 (million)
% 0.50/0.31 % (3967477)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.50/0.31 % (3967477)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.31 % (3967477)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3184386926:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.50/0.31 % (3967458) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3967453-3967458"...
% 0.50/0.31 % (3967482)lrs+10_1_si=on:cs=on:random_seed=1238952942:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.50/0.31 % (3967482)Instruction limit reached!
% 0.50/0.31 % (3967482)------------------------------
% 0.50/0.31 % (3967482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.31 % (3967482)CaDiCaL version: 2.1.3
% 0.50/0.31 % (3967482)Termination reason: Instruction limit
% 0.50/0.31 % (3967482)Termination phase: Saturation
% 0.50/0.31 % (3967482)Time elapsed: 0.003 s
% 0.50/0.31 % (3967482)Peak memory usage: 12 MB
% 0.50/0.31 % (3967482)Instructions burned: 10 (million)
% 0.50/0.31 % (3967458)...printing done.
% 0.50/0.31 % (3967477)Instruction limit reached!
% 0.50/0.31 % (3967477)------------------------------
% 0.50/0.31 % (3967477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.31 % (3967458)Refutation found. Thanks to Tanya!
% 0.50/0.31 % SZS status Theorem for theBenchmark
% 0.50/0.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.50/0.32 % (3967458)------------------------------
% 0.50/0.32 % (3967458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.32 % (3967458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.32 % (3967458)CaDiCaL version: 2.1.3
% 0.50/0.32 % (3967458)Termination reason: Refutation
% 0.50/0.32 % (3967458)Time elapsed: 0.028 s
% 0.50/0.32 % (3967458)Peak memory usage: 13 MB
% 0.50/0.32 % (3967458)Instructions burned: 27 (million)
% 0.50/0.32 % (3967453)Success in time 0.097 s
% 0.50/0.32 % Vampire exiting
%------------------------------------------------------------------------------