%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO388^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:47:34 AM UTC 2026
% Result : Theorem 0.19s 0.31s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 23
% Syntax : Number of formulae : 201 ( 58 unt; 0 typ; 22 def)
% Number of atoms : 2819 ( 659 equ; 0 cnn)
% Maximal formula atoms : 95 ( 14 avg)
% Number of connectives : 3711 ( 783 ~; 684 |; 186 &;2036 @)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 8 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 : 42 ( 39 usr; 28 con; 0-3 aty)
% Number of variables : 712 ( 0 sgn 712 !; 0 ?; 712 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
cQ_6: $i > $i > $i > $o ).
thf(func_def_1,type,
f: $i > $i ).
thf(func_def_2,type,
cP_5: $i > $i > $o ).
thf(func_def_3,type,
cQ_5: $i > $i > $i > $o ).
thf(func_def_8,type,
cP_4: $i > $i > $o ).
thf(func_def_9,type,
cQ_4: $i > $i > $i > $o ).
thf(func_def_10,type,
cP_3: $i > $i > $o ).
thf(func_def_11,type,
cQ_3: $i > $i > $i > $o ).
thf(func_def_12,type,
cP_2: $i > $i > $o ).
thf(func_def_13,type,
cQ_2: $i > $i > $i > $o ).
thf(func_def_14,type,
cP_1: $i > $i > $o ).
thf(func_def_15,type,
cQ_1: $i > $i > $i > $o ).
thf(f1,conjecture,
~ ( ! [X0: $i] : ( cP_5 @ d @ X0 )
& ! [X0: $i] : ( cP_4 @ d @ X0 )
& ! [X0: $i] : ( cP_2 @ d @ X0 )
& ( cP_1 @ c @ c )
& ! [X0: $i,X1: $i] :
( ~ ( cP_5 @ X0 @ X1 )
| ( cP_5 @ ( f @ X0 ) @ X1 ) )
& ! [X0: $i] : ( cP_1 @ d @ X0 )
& ! [X2: $i,X3: $i,X1: $i,X0: $i,X5: $i,X4: $i] :
( ( cQ_6 @ X3 @ X4 @ X5 )
| ~ ( cP_5 @ ( f @ X0 ) @ X3 )
| ~ ( cP_5 @ ( f @ X2 ) @ X5 )
| ~ ( cP_5 @ ( f @ X1 ) @ X4 )
| ~ ( cQ_5 @ X0 @ X1 @ X2 ) )
& ( cP_4 @ c @ c )
& ! [X0: $i,X1: $i] :
( ( cP_1 @ ( f @ X0 ) @ X1 )
| ~ ( cP_1 @ X0 @ X1 ) )
& ( cP_1 @ b @ b )
& ( cP_5 @ b @ b )
& ! [X3: $i,X4: $i,X0: $i,X2: $i,X5: $i,X1: $i] :
( ~ ( cP_4 @ ( f @ X0 ) @ X3 )
| ( cQ_5 @ X3 @ X4 @ X5 )
| ~ ( cP_4 @ ( f @ X2 ) @ X5 )
| ~ ( cP_4 @ ( f @ X1 ) @ X4 )
| ~ ( cQ_4 @ X0 @ X1 @ X2 ) )
& ( cP_3 @ b @ b )
& ! [X3: $i,X4: $i,X2: $i,X5: $i,X0: $i,X1: $i] :
( ~ ( cP_1 @ ( f @ X2 ) @ X5 )
| ~ ( cP_1 @ ( f @ X1 ) @ X4 )
| ~ ( cP_1 @ ( f @ X0 ) @ X3 )
| ~ ( cQ_1 @ X0 @ X1 @ X2 )
| ( cQ_2 @ X3 @ X4 @ X5 ) )
& ( cP_4 @ a @ a )
& ( cP_1 @ a @ a )
& ( cP_5 @ c @ c )
& ! [X1: $i,X0: $i] :
( ~ ( cP_3 @ X0 @ X1 )
| ( cP_3 @ ( f @ X0 ) @ X1 ) )
& ! [X2: $i,X5: $i,X4: $i,X3: $i,X0: $i,X1: $i] :
( ( cQ_3 @ X3 @ X4 @ X5 )
| ~ ( cP_2 @ ( f @ X1 ) @ X4 )
| ~ ( cP_2 @ ( f @ X2 ) @ X5 )
| ~ ( cQ_2 @ X0 @ X1 @ X2 )
| ~ ( cP_2 @ ( f @ X0 ) @ X3 ) )
& ! [X3: $i,X2: $i,X1: $i,X5: $i,X0: $i,X4: $i] :
( ~ ( cP_3 @ ( f @ X2 ) @ X5 )
| ( cQ_4 @ X3 @ X4 @ X5 )
| ~ ( cQ_3 @ X0 @ X1 @ X2 )
| ~ ( cP_3 @ ( f @ X0 ) @ X3 )
| ~ ( cP_3 @ ( f @ X1 ) @ X4 ) )
& ( cP_3 @ c @ c )
& ! [X1: $i,X0: $i] :
( ( cP_4 @ ( f @ X0 ) @ X1 )
| ~ ( cP_4 @ X0 @ X1 ) )
& ! [X1: $i,X0: $i] :
( ( cP_2 @ ( f @ X0 ) @ X1 )
| ~ ( cP_2 @ X0 @ X1 ) )
& ! [X2: $i,X0: $i,X1: $i] :
~ ( cQ_6 @ X0 @ X1 @ X2 )
& ( cP_2 @ a @ a )
& ( cP_2 @ c @ c )
& ( cP_3 @ a @ a )
& ( cP_4 @ b @ b )
& ( cQ_1 @ a @ b @ c )
& ( cP_2 @ b @ b )
& ! [X0: $i] : ( cP_3 @ d @ X0 )
& ( cP_5 @ a @ a ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM409_5) ).
thf(f2,negated_conjecture,
~ ~ ( ! [X0: $i] : ( cP_5 @ d @ X0 )
& ! [X0: $i] : ( cP_4 @ d @ X0 )
& ! [X0: $i] : ( cP_2 @ d @ X0 )
& ( cP_1 @ c @ c )
& ! [X0: $i,X1: $i] :
( ~ ( cP_5 @ X0 @ X1 )
| ( cP_5 @ ( f @ X0 ) @ X1 ) )
& ! [X0: $i] : ( cP_1 @ d @ X0 )
& ! [X2: $i,X3: $i,X1: $i,X0: $i,X5: $i,X4: $i] :
( ( cQ_6 @ X3 @ X4 @ X5 )
| ~ ( cP_5 @ ( f @ X0 ) @ X3 )
| ~ ( cP_5 @ ( f @ X2 ) @ X5 )
| ~ ( cP_5 @ ( f @ X1 ) @ X4 )
| ~ ( cQ_5 @ X0 @ X1 @ X2 ) )
& ( cP_4 @ c @ c )
& ! [X0: $i,X1: $i] :
( ( cP_1 @ ( f @ X0 ) @ X1 )
| ~ ( cP_1 @ X0 @ X1 ) )
& ( cP_1 @ b @ b )
& ( cP_5 @ b @ b )
& ! [X3: $i,X4: $i,X0: $i,X2: $i,X5: $i,X1: $i] :
( ~ ( cP_4 @ ( f @ X0 ) @ X3 )
| ( cQ_5 @ X3 @ X4 @ X5 )
| ~ ( cP_4 @ ( f @ X2 ) @ X5 )
| ~ ( cP_4 @ ( f @ X1 ) @ X4 )
| ~ ( cQ_4 @ X0 @ X1 @ X2 ) )
& ( cP_3 @ b @ b )
& ! [X3: $i,X4: $i,X2: $i,X5: $i,X0: $i,X1: $i] :
( ~ ( cP_1 @ ( f @ X2 ) @ X5 )
| ~ ( cP_1 @ ( f @ X1 ) @ X4 )
| ~ ( cP_1 @ ( f @ X0 ) @ X3 )
| ~ ( cQ_1 @ X0 @ X1 @ X2 )
| ( cQ_2 @ X3 @ X4 @ X5 ) )
& ( cP_4 @ a @ a )
& ( cP_1 @ a @ a )
& ( cP_5 @ c @ c )
& ! [X1: $i,X0: $i] :
( ~ ( cP_3 @ X0 @ X1 )
| ( cP_3 @ ( f @ X0 ) @ X1 ) )
& ! [X2: $i,X5: $i,X4: $i,X3: $i,X0: $i,X1: $i] :
( ( cQ_3 @ X3 @ X4 @ X5 )
| ~ ( cP_2 @ ( f @ X1 ) @ X4 )
| ~ ( cP_2 @ ( f @ X2 ) @ X5 )
| ~ ( cQ_2 @ X0 @ X1 @ X2 )
| ~ ( cP_2 @ ( f @ X0 ) @ X3 ) )
& ! [X3: $i,X2: $i,X1: $i,X5: $i,X0: $i,X4: $i] :
( ~ ( cP_3 @ ( f @ X2 ) @ X5 )
| ( cQ_4 @ X3 @ X4 @ X5 )
| ~ ( cQ_3 @ X0 @ X1 @ X2 )
| ~ ( cP_3 @ ( f @ X0 ) @ X3 )
| ~ ( cP_3 @ ( f @ X1 ) @ X4 ) )
& ( cP_3 @ c @ c )
& ! [X1: $i,X0: $i] :
( ( cP_4 @ ( f @ X0 ) @ X1 )
| ~ ( cP_4 @ X0 @ X1 ) )
& ! [X1: $i,X0: $i] :
( ( cP_2 @ ( f @ X0 ) @ X1 )
| ~ ( cP_2 @ X0 @ X1 ) )
& ! [X2: $i,X0: $i,X1: $i] :
~ ( cQ_6 @ X0 @ X1 @ X2 )
& ( cP_2 @ a @ a )
& ( cP_2 @ c @ c )
& ( cP_3 @ a @ a )
& ( cP_4 @ b @ b )
& ( cQ_1 @ a @ b @ c )
& ( cP_2 @ b @ b )
& ! [X0: $i] : ( cP_3 @ d @ X0 )
& ( cP_5 @ a @ a ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ~ ( ! [X0: $i] : ( cP_5 @ d @ X0 )
& ! [X1: $i] : ( cP_4 @ d @ X1 )
& ! [X2: $i] : ( cP_2 @ d @ X2 )
& ( cP_1 @ c @ c )
& ! [X3: $i,X4: $i] :
( ~ ( cP_5 @ X3 @ X4 )
| ( cP_5 @ ( f @ X3 ) @ X4 ) )
& ! [X5: $i] : ( cP_1 @ d @ X5 )
& ! [X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( ( cQ_6 @ X7 @ X11 @ X10 )
| ~ ( cP_5 @ ( f @ X9 ) @ X7 )
| ~ ( cP_5 @ ( f @ X6 ) @ X10 )
| ~ ( cP_5 @ ( f @ X8 ) @ X11 )
| ~ ( cQ_5 @ X9 @ X8 @ X6 ) )
& ( cP_4 @ c @ c )
& ! [X12: $i,X13: $i] :
( ( cP_1 @ ( f @ X12 ) @ X13 )
| ~ ( cP_1 @ X12 @ X13 ) )
& ( cP_1 @ b @ b )
& ( cP_5 @ b @ b )
& ! [X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
( ~ ( cP_4 @ ( f @ X16 ) @ X14 )
| ( cQ_5 @ X14 @ X15 @ X18 )
| ~ ( cP_4 @ ( f @ X17 ) @ X18 )
| ~ ( cP_4 @ ( f @ X19 ) @ X15 )
| ~ ( cQ_4 @ X16 @ X19 @ X17 ) )
& ( cP_3 @ b @ b )
& ! [X20: $i,X21: $i,X22: $i,X23: $i,X24: $i,X25: $i] :
( ~ ( cP_1 @ ( f @ X22 ) @ X23 )
| ~ ( cP_1 @ ( f @ X25 ) @ X21 )
| ~ ( cP_1 @ ( f @ X24 ) @ X20 )
| ~ ( cQ_1 @ X24 @ X25 @ X22 )
| ( cQ_2 @ X20 @ X21 @ X23 ) )
& ( cP_4 @ a @ a )
& ( cP_1 @ a @ a )
& ( cP_5 @ c @ c )
& ! [X26: $i,X27: $i] :
( ~ ( cP_3 @ X27 @ X26 )
| ( cP_3 @ ( f @ X27 ) @ X26 ) )
& ! [X28: $i,X29: $i,X30: $i,X31: $i,X32: $i,X33: $i] :
( ( cQ_3 @ X31 @ X30 @ X29 )
| ~ ( cP_2 @ ( f @ X33 ) @ X30 )
| ~ ( cP_2 @ ( f @ X28 ) @ X29 )
| ~ ( cQ_2 @ X32 @ X33 @ X28 )
| ~ ( cP_2 @ ( f @ X32 ) @ X31 ) )
& ! [X34: $i,X35: $i,X36: $i,X37: $i,X38: $i,X39: $i] :
( ~ ( cP_3 @ ( f @ X35 ) @ X37 )
| ( cQ_4 @ X34 @ X39 @ X37 )
| ~ ( cQ_3 @ X38 @ X36 @ X35 )
| ~ ( cP_3 @ ( f @ X38 ) @ X34 )
| ~ ( cP_3 @ ( f @ X36 ) @ X39 ) )
& ( cP_3 @ c @ c )
& ! [X40: $i,X41: $i] :
( ( cP_4 @ ( f @ X41 ) @ X40 )
| ~ ( cP_4 @ X41 @ X40 ) )
& ! [X42: $i,X43: $i] :
( ( cP_2 @ ( f @ X43 ) @ X42 )
| ~ ( cP_2 @ X43 @ X42 ) )
& ! [X44: $i,X45: $i,X46: $i] :
~ ( cQ_6 @ X45 @ X46 @ X44 )
& ( cP_2 @ a @ a )
& ( cP_2 @ c @ c )
& ( cP_3 @ a @ a )
& ( cP_4 @ b @ b )
& ( cQ_1 @ a @ b @ c )
& ( cP_2 @ b @ b )
& ! [X47: $i] : ( cP_3 @ d @ X47 )
& ( cP_5 @ a @ a ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
~ ~ ( ! [X0: $i] :
( ( cP_5 @ d @ X0 )
= $true )
& ! [X1: $i] :
( $true
= ( cP_4 @ d @ X1 ) )
& ! [X2: $i] :
( ( cP_2 @ d @ X2 )
= $true )
& ( ( cP_1 @ c @ c )
= $true )
& ! [X3: $i,X4: $i] :
( ( $true
!= ( cP_5 @ X3 @ X4 ) )
| ( $true
= ( cP_5 @ ( f @ X3 ) @ X4 ) ) )
& ! [X5: $i] :
( $true
= ( cP_1 @ d @ X5 ) )
& ! [X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( ( ( cQ_6 @ X7 @ X11 @ X10 )
= $true )
| ( $true
!= ( cP_5 @ ( f @ X9 ) @ X7 ) )
| ( $true
!= ( cP_5 @ ( f @ X6 ) @ X10 ) )
| ( $true
!= ( cP_5 @ ( f @ X8 ) @ X11 ) )
| ( $true
!= ( cQ_5 @ X9 @ X8 @ X6 ) ) )
& ( ( cP_4 @ c @ c )
= $true )
& ! [X12: $i,X13: $i] :
( ( ( cP_1 @ ( f @ X12 ) @ X13 )
= $true )
| ( ( cP_1 @ X12 @ X13 )
!= $true ) )
& ( ( cP_1 @ b @ b )
= $true )
& ( ( cP_5 @ b @ b )
= $true )
& ! [X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
( ( ( cP_4 @ ( f @ X16 ) @ X14 )
!= $true )
| ( $true
= ( cQ_5 @ X14 @ X15 @ X18 ) )
| ( $true
!= ( cP_4 @ ( f @ X17 ) @ X18 ) )
| ( ( cP_4 @ ( f @ X19 ) @ X15 )
!= $true )
| ( ( cQ_4 @ X16 @ X19 @ X17 )
!= $true ) )
& ( ( cP_3 @ b @ b )
= $true )
& ! [X20: $i,X21: $i,X22: $i,X23: $i,X24: $i,X25: $i] :
( ( ( cP_1 @ ( f @ X22 ) @ X23 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ X25 ) @ X21 ) )
| ( ( cP_1 @ ( f @ X24 ) @ X20 )
!= $true )
| ( $true
!= ( cQ_1 @ X24 @ X25 @ X22 ) )
| ( $true
= ( cQ_2 @ X20 @ X21 @ X23 ) ) )
& ( ( cP_4 @ a @ a )
= $true )
& ( ( cP_1 @ a @ a )
= $true )
& ( ( cP_5 @ c @ c )
= $true )
& ! [X26: $i,X27: $i] :
( ( ( cP_3 @ X27 @ X26 )
!= $true )
| ( ( cP_3 @ ( f @ X27 ) @ X26 )
= $true ) )
& ! [X28: $i,X29: $i,X30: $i,X31: $i,X32: $i,X33: $i] :
( ( $true
= ( cQ_3 @ X31 @ X30 @ X29 ) )
| ( $true
!= ( cP_2 @ ( f @ X33 ) @ X30 ) )
| ( $true
!= ( cP_2 @ ( f @ X28 ) @ X29 ) )
| ( ( cQ_2 @ X32 @ X33 @ X28 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X32 ) @ X31 ) ) )
& ! [X34: $i,X35: $i,X36: $i,X37: $i,X38: $i,X39: $i] :
( ( $true
!= ( cP_3 @ ( f @ X35 ) @ X37 ) )
| ( $true
= ( cQ_4 @ X34 @ X39 @ X37 ) )
| ( $true
!= ( cQ_3 @ X38 @ X36 @ X35 ) )
| ( $true
!= ( cP_3 @ ( f @ X38 ) @ X34 ) )
| ( $true
!= ( cP_3 @ ( f @ X36 ) @ X39 ) ) )
& ( ( cP_3 @ c @ c )
= $true )
& ! [X40: $i,X41: $i] :
( ( $true
= ( cP_4 @ ( f @ X41 ) @ X40 ) )
| ( $true
!= ( cP_4 @ X41 @ X40 ) ) )
& ! [X42: $i,X43: $i] :
( ( ( cP_2 @ ( f @ X43 ) @ X42 )
= $true )
| ( $true
!= ( cP_2 @ X43 @ X42 ) ) )
& ! [X44: $i,X45: $i,X46: $i] :
( $true
!= ( cQ_6 @ X45 @ X46 @ X44 ) )
& ( ( cP_2 @ a @ a )
= $true )
& ( ( cP_2 @ c @ c )
= $true )
& ( ( cP_3 @ a @ a )
= $true )
& ( ( cP_4 @ b @ b )
= $true )
& ( ( cQ_1 @ a @ b @ c )
= $true )
& ( ( cP_2 @ b @ b )
= $true )
& ! [X47: $i] :
( ( cP_3 @ d @ X47 )
= $true )
& ( ( cP_5 @ a @ a )
= $true ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( ( ( cP_1 @ b @ b )
= $true )
& ( ( cP_2 @ b @ b )
= $true )
& ( ( cQ_1 @ a @ b @ c )
= $true )
& ( ( cP_1 @ c @ c )
= $true )
& ( ( cP_2 @ a @ a )
= $true )
& ( ( cP_1 @ a @ a )
= $true )
& ( ( cP_5 @ a @ a )
= $true )
& ! [X13: $i,X12: $i] :
( ( ( cP_1 @ ( f @ X12 ) @ X13 )
= $true )
| ( ( cP_1 @ X12 @ X13 )
!= $true ) )
& ! [X47: $i] :
( ( cP_3 @ d @ X47 )
= $true )
& ( ( cP_3 @ b @ b )
= $true )
& ! [X43: $i,X42: $i] :
( ( $true
!= ( cP_2 @ X43 @ X42 ) )
| ( ( cP_2 @ ( f @ X43 ) @ X42 )
= $true ) )
& ( ( cP_2 @ c @ c )
= $true )
& ( ( cP_5 @ c @ c )
= $true )
& ( ( cP_3 @ c @ c )
= $true )
& ! [X35: $i,X36: $i,X39: $i,X37: $i,X34: $i,X38: $i] :
( ( $true
!= ( cQ_3 @ X38 @ X36 @ X35 ) )
| ( $true
!= ( cP_3 @ ( f @ X35 ) @ X37 ) )
| ( $true
!= ( cP_3 @ ( f @ X38 ) @ X34 ) )
| ( $true
= ( cQ_4 @ X34 @ X39 @ X37 ) )
| ( $true
!= ( cP_3 @ ( f @ X36 ) @ X39 ) ) )
& ( ( cP_5 @ b @ b )
= $true )
& ! [X16: $i,X14: $i,X19: $i,X15: $i,X17: $i,X18: $i] :
( ( $true
= ( cQ_5 @ X14 @ X15 @ X18 ) )
| ( ( cP_4 @ ( f @ X19 ) @ X15 )
!= $true )
| ( ( cQ_4 @ X16 @ X19 @ X17 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X17 ) @ X18 ) )
| ( ( cP_4 @ ( f @ X16 ) @ X14 )
!= $true ) )
& ! [X45: $i,X46: $i,X44: $i] :
( $true
!= ( cQ_6 @ X45 @ X46 @ X44 ) )
& ! [X2: $i] :
( ( cP_2 @ d @ X2 )
= $true )
& ! [X5: $i] :
( $true
= ( cP_1 @ d @ X5 ) )
& ( ( cP_3 @ a @ a )
= $true )
& ! [X9: $i,X10: $i,X6: $i,X8: $i,X11: $i,X7: $i] :
( ( ( cQ_6 @ X7 @ X11 @ X10 )
= $true )
| ( $true
!= ( cP_5 @ ( f @ X8 ) @ X11 ) )
| ( $true
!= ( cQ_5 @ X9 @ X8 @ X6 ) )
| ( $true
!= ( cP_5 @ ( f @ X9 ) @ X7 ) )
| ( $true
!= ( cP_5 @ ( f @ X6 ) @ X10 ) ) )
& ! [X21: $i,X24: $i,X25: $i,X23: $i,X22: $i,X20: $i] :
( ( ( cP_1 @ ( f @ X24 ) @ X20 )
!= $true )
| ( ( cP_1 @ ( f @ X22 ) @ X23 )
!= $true )
| ( $true
!= ( cQ_1 @ X24 @ X25 @ X22 ) )
| ( $true
!= ( cP_1 @ ( f @ X25 ) @ X21 ) )
| ( $true
= ( cQ_2 @ X20 @ X21 @ X23 ) ) )
& ! [X28: $i,X31: $i,X33: $i,X29: $i,X32: $i,X30: $i] :
( ( $true
!= ( cP_2 @ ( f @ X33 ) @ X30 ) )
| ( $true
= ( cQ_3 @ X31 @ X30 @ X29 ) )
| ( ( cQ_2 @ X32 @ X33 @ X28 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X28 ) @ X29 ) )
| ( $true
!= ( cP_2 @ ( f @ X32 ) @ X31 ) ) )
& ! [X1: $i] :
( $true
= ( cP_4 @ d @ X1 ) )
& ( ( cP_4 @ c @ c )
= $true )
& ( ( cP_4 @ a @ a )
= $true )
& ! [X41: $i,X40: $i] :
( ( $true
!= ( cP_4 @ X41 @ X40 ) )
| ( $true
= ( cP_4 @ ( f @ X41 ) @ X40 ) ) )
& ! [X3: $i,X4: $i] :
( ( $true
!= ( cP_5 @ X3 @ X4 ) )
| ( $true
= ( cP_5 @ ( f @ X3 ) @ X4 ) ) )
& ! [X0: $i] :
( ( cP_5 @ d @ X0 )
= $true )
& ! [X27: $i,X26: $i] :
( ( ( cP_3 @ ( f @ X27 ) @ X26 )
= $true )
| ( ( cP_3 @ X27 @ X26 )
!= $true ) )
& ( ( cP_4 @ b @ b )
= $true ) ),
inference(flattening,[],[f4]) ).
thf(f6,plain,
( ( ( cP_1 @ b @ b )
= $true )
& ( ( cP_2 @ b @ b )
= $true )
& ( ( cQ_1 @ a @ b @ c )
= $true )
& ( ( cP_1 @ c @ c )
= $true )
& ( ( cP_2 @ a @ a )
= $true )
& ( ( cP_1 @ a @ a )
= $true )
& ( ( cP_5 @ a @ a )
= $true )
& ! [X0: $i,X1: $i] :
( ( $true
= ( cP_1 @ ( f @ X1 ) @ X0 ) )
| ( $true
!= ( cP_1 @ X1 @ X0 ) ) )
& ! [X2: $i] :
( $true
= ( cP_3 @ d @ X2 ) )
& ( ( cP_3 @ b @ b )
= $true )
& ! [X3: $i,X4: $i] :
( ( $true
!= ( cP_2 @ X3 @ X4 ) )
| ( ( cP_2 @ ( f @ X3 ) @ X4 )
= $true ) )
& ( ( cP_2 @ c @ c )
= $true )
& ( ( cP_5 @ c @ c )
= $true )
& ( ( cP_3 @ c @ c )
= $true )
& ! [X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] :
( ( ( cQ_3 @ X10 @ X6 @ X5 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X5 ) @ X8 ) )
| ( ( cP_3 @ ( f @ X10 ) @ X9 )
!= $true )
| ( $true
= ( cQ_4 @ X9 @ X7 @ X8 ) )
| ( ( cP_3 @ ( f @ X6 ) @ X7 )
!= $true ) )
& ( ( cP_5 @ b @ b )
= $true )
& ! [X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
( ( $true
= ( cQ_5 @ X12 @ X14 @ X16 ) )
| ( ( cP_4 @ ( f @ X13 ) @ X14 )
!= $true )
| ( ( cQ_4 @ X11 @ X13 @ X15 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X15 ) @ X16 ) )
| ( $true
!= ( cP_4 @ ( f @ X11 ) @ X12 ) ) )
& ! [X17: $i,X18: $i,X19: $i] :
( $true
!= ( cQ_6 @ X17 @ X18 @ X19 ) )
& ! [X20: $i] :
( ( cP_2 @ d @ X20 )
= $true )
& ! [X21: $i] :
( $true
= ( cP_1 @ d @ X21 ) )
& ( ( cP_3 @ a @ a )
= $true )
& ! [X22: $i,X23: $i,X24: $i,X25: $i,X26: $i,X27: $i] :
( ( $true
= ( cQ_6 @ X27 @ X26 @ X23 ) )
| ( $true
!= ( cP_5 @ ( f @ X25 ) @ X26 ) )
| ( ( cQ_5 @ X22 @ X25 @ X24 )
!= $true )
| ( ( cP_5 @ ( f @ X22 ) @ X27 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X24 ) @ X23 ) ) )
& ! [X28: $i,X29: $i,X30: $i,X31: $i,X32: $i,X33: $i] :
( ( $true
!= ( cP_1 @ ( f @ X29 ) @ X33 ) )
| ( ( cP_1 @ ( f @ X32 ) @ X31 )
!= $true )
| ( $true
!= ( cQ_1 @ X29 @ X30 @ X32 ) )
| ( $true
!= ( cP_1 @ ( f @ X30 ) @ X28 ) )
| ( $true
= ( cQ_2 @ X33 @ X28 @ X31 ) ) )
& ! [X34: $i,X35: $i,X36: $i,X37: $i,X38: $i,X39: $i] :
( ( $true
!= ( cP_2 @ ( f @ X36 ) @ X39 ) )
| ( ( cQ_3 @ X35 @ X39 @ X37 )
= $true )
| ( $true
!= ( cQ_2 @ X38 @ X36 @ X34 ) )
| ( $true
!= ( cP_2 @ ( f @ X34 ) @ X37 ) )
| ( $true
!= ( cP_2 @ ( f @ X38 ) @ X35 ) ) )
& ! [X40: $i] :
( $true
= ( cP_4 @ d @ X40 ) )
& ( ( cP_4 @ c @ c )
= $true )
& ( ( cP_4 @ a @ a )
= $true )
& ! [X41: $i,X42: $i] :
( ( $true
!= ( cP_4 @ X41 @ X42 ) )
| ( $true
= ( cP_4 @ ( f @ X41 ) @ X42 ) ) )
& ! [X43: $i,X44: $i] :
( ( ( cP_5 @ X43 @ X44 )
!= $true )
| ( $true
= ( cP_5 @ ( f @ X43 ) @ X44 ) ) )
& ! [X45: $i] :
( $true
= ( cP_5 @ d @ X45 ) )
& ! [X46: $i,X47: $i] :
( ( $true
= ( cP_3 @ ( f @ X46 ) @ X47 ) )
| ( $true
!= ( cP_3 @ X46 @ X47 ) ) )
& ( ( cP_4 @ b @ b )
= $true ) ),
inference(rectify,[],[f5]) ).
thf(f7,plain,
( ( cP_4 @ b @ b )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f8,plain,
! [X46: $i,X47: $i] :
( ( $true
= ( cP_3 @ ( f @ X46 ) @ X47 ) )
| ( $true
!= ( cP_3 @ X46 @ X47 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f10,plain,
! [X44: $i,X43: $i] :
( ( $true
= ( cP_5 @ ( f @ X43 ) @ X44 ) )
| ( ( cP_5 @ X43 @ X44 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f11,plain,
! [X41: $i,X42: $i] :
( ( $true
= ( cP_4 @ ( f @ X41 ) @ X42 ) )
| ( $true
!= ( cP_4 @ X41 @ X42 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f12,plain,
( ( cP_4 @ a @ a )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f13,plain,
( ( cP_4 @ c @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f15,plain,
! [X38: $i,X39: $i,X36: $i,X37: $i,X34: $i,X35: $i] :
( ( ( cQ_3 @ X35 @ X39 @ X37 )
= $true )
| ( $true
!= ( cP_2 @ ( f @ X36 ) @ X39 ) )
| ( $true
!= ( cP_2 @ ( f @ X34 ) @ X37 ) )
| ( $true
!= ( cP_2 @ ( f @ X38 ) @ X35 ) )
| ( $true
!= ( cQ_2 @ X38 @ X36 @ X34 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f16,plain,
! [X31: $i,X28: $i,X29: $i,X32: $i,X30: $i,X33: $i] :
( ( $true
= ( cQ_2 @ X33 @ X28 @ X31 ) )
| ( $true
!= ( cP_1 @ ( f @ X30 ) @ X28 ) )
| ( $true
!= ( cQ_1 @ X29 @ X30 @ X32 ) )
| ( $true
!= ( cP_1 @ ( f @ X29 ) @ X33 ) )
| ( ( cP_1 @ ( f @ X32 ) @ X31 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f17,plain,
! [X26: $i,X27: $i,X24: $i,X22: $i,X25: $i,X23: $i] :
( ( $true
!= ( cP_5 @ ( f @ X24 ) @ X23 ) )
| ( ( cQ_5 @ X22 @ X25 @ X24 )
!= $true )
| ( $true
= ( cQ_6 @ X27 @ X26 @ X23 ) )
| ( ( cP_5 @ ( f @ X22 ) @ X27 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X25 ) @ X26 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f18,plain,
( ( cP_3 @ a @ a )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f21,plain,
! [X18: $i,X19: $i,X17: $i] :
( $true
!= ( cQ_6 @ X17 @ X18 @ X19 ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f22,plain,
! [X11: $i,X16: $i,X14: $i,X15: $i,X12: $i,X13: $i] :
( ( $true
= ( cQ_5 @ X12 @ X14 @ X16 ) )
| ( $true
!= ( cP_4 @ ( f @ X15 ) @ X16 ) )
| ( ( cQ_4 @ X11 @ X13 @ X15 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X11 ) @ X12 ) )
| ( ( cP_4 @ ( f @ X13 ) @ X14 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f23,plain,
( ( cP_5 @ b @ b )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f24,plain,
! [X10: $i,X8: $i,X6: $i,X9: $i,X7: $i,X5: $i] :
( ( $true
= ( cQ_4 @ X9 @ X7 @ X8 ) )
| ( ( cP_3 @ ( f @ X10 ) @ X9 )
!= $true )
| ( ( cQ_3 @ X10 @ X6 @ X5 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X5 ) @ X8 ) )
| ( ( cP_3 @ ( f @ X6 ) @ X7 )
!= $true ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f25,plain,
( ( cP_3 @ c @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f26,plain,
( ( cP_5 @ c @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f27,plain,
( ( cP_2 @ c @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f28,plain,
! [X3: $i,X4: $i] :
( ( ( cP_2 @ ( f @ X3 ) @ X4 )
= $true )
| ( $true
!= ( cP_2 @ X3 @ X4 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f29,plain,
( ( cP_3 @ b @ b )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f31,plain,
! [X0: $i,X1: $i] :
( ( $true
= ( cP_1 @ ( f @ X1 ) @ X0 ) )
| ( $true
!= ( cP_1 @ X1 @ X0 ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f32,plain,
( ( cP_5 @ a @ a )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f33,plain,
( ( cP_1 @ a @ a )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f34,plain,
( ( cP_2 @ a @ a )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f35,plain,
( ( cP_1 @ c @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f36,plain,
( ( cQ_1 @ a @ b @ c )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f37,plain,
( ( cP_2 @ b @ b )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f38,plain,
( ( cP_1 @ b @ b )
= $true ),
inference(cnf_transformation,[],[f6]) ).
thf(f41,definition,
( spl0_1
<=> ( ( cP_1 @ a @ a )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
thf(f43,plain,
( ( ( cP_1 @ a @ a )
= $true )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f41]) ).
thf(f44,plain,
spl0_1,
inference(avatar_split_clause,[],[f33,f41]) ).
thf(f46,definition,
( spl0_2
<=> ( ( cP_3 @ b @ b )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
thf(f48,plain,
( ( ( cP_3 @ b @ b )
= $true )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f46]) ).
thf(f49,plain,
spl0_2,
inference(avatar_split_clause,[],[f29,f46]) ).
thf(f51,definition,
( spl0_3
<=> ( ( cP_4 @ a @ a )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
thf(f53,plain,
( ( ( cP_4 @ a @ a )
= $true )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f51]) ).
thf(f54,plain,
spl0_3,
inference(avatar_split_clause,[],[f12,f51]) ).
thf(f56,definition,
( spl0_4
<=> ( ( cP_5 @ b @ b )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
thf(f58,plain,
( ( ( cP_5 @ b @ b )
= $true )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f56]) ).
thf(f59,plain,
spl0_4,
inference(avatar_split_clause,[],[f23,f56]) ).
thf(f61,definition,
( spl0_5
<=> ( ( cP_4 @ b @ b )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
thf(f63,plain,
( ( ( cP_4 @ b @ b )
= $true )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f61]) ).
thf(f64,plain,
spl0_5,
inference(avatar_split_clause,[],[f7,f61]) ).
thf(f66,definition,
( spl0_6
<=> ( ( cP_2 @ b @ b )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
thf(f68,plain,
( ( ( cP_2 @ b @ b )
= $true )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f66]) ).
thf(f69,plain,
spl0_6,
inference(avatar_split_clause,[],[f37,f66]) ).
thf(f71,definition,
( spl0_7
<=> ( ( cP_5 @ a @ a )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
thf(f73,plain,
( ( ( cP_5 @ a @ a )
= $true )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f71]) ).
thf(f74,plain,
spl0_7,
inference(avatar_split_clause,[],[f32,f71]) ).
thf(f76,definition,
( spl0_8
<=> ( ( cP_3 @ c @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
thf(f78,plain,
( ( ( cP_3 @ c @ c )
= $true )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f76]) ).
thf(f79,plain,
spl0_8,
inference(avatar_split_clause,[],[f25,f76]) ).
thf(f81,definition,
( spl0_9
<=> ( ( cP_3 @ a @ a )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
thf(f83,plain,
( ( ( cP_3 @ a @ a )
= $true )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f81]) ).
thf(f84,plain,
spl0_9,
inference(avatar_split_clause,[],[f18,f81]) ).
thf(f86,definition,
( spl0_10
<=> ( ( cQ_1 @ a @ b @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
thf(f88,plain,
( ( ( cQ_1 @ a @ b @ c )
= $true )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f86]) ).
thf(f89,plain,
spl0_10,
inference(avatar_split_clause,[],[f36,f86]) ).
thf(f91,definition,
( spl0_11
<=> ( ( cP_2 @ a @ a )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
thf(f93,plain,
( ( ( cP_2 @ a @ a )
= $true )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f91]) ).
thf(f94,plain,
spl0_11,
inference(avatar_split_clause,[],[f34,f91]) ).
thf(f96,definition,
( spl0_12
<=> ( ( cP_5 @ c @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
thf(f98,plain,
( ( ( cP_5 @ c @ c )
= $true )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f96]) ).
thf(f99,plain,
spl0_12,
inference(avatar_split_clause,[],[f26,f96]) ).
thf(f101,definition,
( spl0_13
<=> ( ( cP_4 @ c @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
thf(f103,plain,
( ( ( cP_4 @ c @ c )
= $true )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f101]) ).
thf(f104,plain,
spl0_13,
inference(avatar_split_clause,[],[f13,f101]) ).
thf(f106,definition,
( spl0_14
<=> ( ( cP_2 @ c @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
thf(f108,plain,
( ( ( cP_2 @ c @ c )
= $true )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f106]) ).
thf(f109,plain,
spl0_14,
inference(avatar_split_clause,[],[f27,f106]) ).
thf(f111,definition,
( spl0_15
<=> ( ( cP_1 @ b @ b )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
thf(f113,plain,
( ( ( cP_1 @ b @ b )
= $true )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f111]) ).
thf(f114,plain,
spl0_15,
inference(avatar_split_clause,[],[f38,f111]) ).
thf(f116,definition,
( spl0_16
<=> ( ( cP_1 @ c @ c )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
thf(f118,plain,
( ( ( cP_1 @ c @ c )
= $true )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f116]) ).
thf(f119,plain,
spl0_16,
inference(avatar_split_clause,[],[f35,f116]) ).
thf(f120,plain,
! [X26: $i,X27: $i,X24: $i,X22: $i,X25: $i,X23: $i] :
( ( ( cQ_5 @ X22 @ X25 @ X24 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X24 ) @ X23 ) )
| ( ( cP_5 @ ( f @ X22 ) @ X27 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X25 ) @ X26 ) ) ),
inference(forward_subsumption_resolution,[],[f17,f21]) ).
thf(f121,plain,
! [X2: $i,X3: $i,X0: $i,X1: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
!= ( cP_4 @ ( f @ X8 ) @ X1 ) )
| ( $true != $true )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( $true
!= ( cP_5 @ ( f @ X0 ) @ X4 ) )
| ( ( cQ_4 @ X7 @ X8 @ X6 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X1 ) @ X5 ) )
| ( ( cP_4 @ ( f @ X7 ) @ X0 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X6 ) @ X2 ) ) ),
inference(superposition,[],[f120,f22]) ).
thf(f122,plain,
! [X2: $i,X3: $i,X0: $i,X1: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( ( cQ_4 @ X7 @ X8 @ X6 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X1 ) @ X5 ) )
| ( $true
!= ( cP_4 @ ( f @ X8 ) @ X1 ) )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( ( cP_4 @ ( f @ X7 ) @ X0 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X6 ) @ X2 ) )
| ( $true
!= ( cP_5 @ ( f @ X0 ) @ X4 ) ) ),
inference(trivial_inequality_removal,[],[f121]) ).
thf(f123,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X4: $i,X5: $i] :
( ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X5 ) @ X6 ) )
| ( ( cP_3 @ ( f @ X10 ) @ X1 )
!= $true )
| ( ( cQ_3 @ X9 @ X10 @ X11 )
!= $true )
| ( ( cP_4 @ ( f @ X2 ) @ X5 )
!= $true )
| ( ( cP_4 @ ( f @ X0 ) @ X7 )
!= $true )
| ( $true != $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X0 ) )
| ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) )
| ( $true
!= ( cP_3 @ ( f @ X11 ) @ X2 ) ) ),
inference(superposition,[],[f122,f24]) ).
thf(f124,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X4: $i,X5: $i] :
( ( ( cQ_3 @ X9 @ X10 @ X11 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X11 ) @ X2 ) )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X0 ) )
| ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) )
| ( ( cP_4 @ ( f @ X2 ) @ X5 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X5 ) @ X6 ) )
| ( ( cP_3 @ ( f @ X10 ) @ X1 )
!= $true )
| ( ( cP_4 @ ( f @ X0 ) @ X7 )
!= $true )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) ) ),
inference(trivial_inequality_removal,[],[f123]) ).
thf(f125,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X14: $i,X4: $i,X5: $i,X12: $i,X13: $i] :
( ( $true
!= ( cP_4 @ ( f @ X3 ) @ X7 ) )
| ( $true
!= ( cP_3 @ ( f @ X1 ) @ X5 ) )
| ( $true
!= ( cP_5 @ ( f @ X9 ) @ X10 ) )
| ( $true
!= ( cP_2 @ ( f @ X12 ) @ X1 ) )
| ( ( cP_3 @ ( f @ X2 ) @ X3 )
!= $true )
| ( ( cP_5 @ ( f @ X6 ) @ X11 )
!= $true )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X0 ) @ X4 ) )
| ( ( cP_2 @ ( f @ X13 ) @ X2 )
!= $true )
| ( ( cP_4 @ ( f @ X5 ) @ X6 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X9 ) )
| ( $true
!= ( cQ_2 @ X14 @ X12 @ X13 ) )
| ( $true != $true )
| ( ( cP_2 @ ( f @ X14 ) @ X0 )
!= $true ) ),
inference(superposition,[],[f124,f15]) ).
thf(f126,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X14: $i,X4: $i,X5: $i,X12: $i,X13: $i] :
( ( $true
!= ( cQ_2 @ X14 @ X12 @ X13 ) )
| ( $true
!= ( cP_5 @ ( f @ X9 ) @ X10 ) )
| ( ( cP_3 @ ( f @ X2 ) @ X3 )
!= $true )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( ( cP_4 @ ( f @ X5 ) @ X6 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X0 ) @ X4 ) )
| ( ( cP_2 @ ( f @ X14 ) @ X0 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X3 ) @ X7 ) )
| ( $true
!= ( cP_3 @ ( f @ X1 ) @ X5 ) )
| ( ( cP_5 @ ( f @ X6 ) @ X11 )
!= $true )
| ( ( cP_2 @ ( f @ X13 ) @ X2 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X9 ) )
| ( $true
!= ( cP_2 @ ( f @ X12 ) @ X1 ) ) ),
inference(trivial_inequality_removal,[],[f125]) ).
thf(f127,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X16: $i,X4: $i,X14: $i,X17: $i,X15: $i,X5: $i,X12: $i,X13: $i] :
( ( $true != $true )
| ( ( cP_3 @ ( f @ X5 ) @ X6 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ X15 ) @ X1 ) )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( ( cP_2 @ ( f @ X1 ) @ X13 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_4 @ ( f @ X6 ) @ X7 )
!= $true )
| ( ( cP_1 @ ( f @ X16 ) @ X0 )
!= $true )
| ( ( cP_2 @ ( f @ X2 ) @ X5 )
!= $true )
| ( $true
!= ( cQ_1 @ X16 @ X15 @ X17 ) )
| ( ( cP_4 @ ( f @ X12 ) @ X3 )
!= $true )
| ( ( cP_3 @ ( f @ X13 ) @ X9 )
!= $true )
| ( ( cP_2 @ ( f @ X0 ) @ X11 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ X17 ) @ X2 ) )
| ( ( cP_3 @ ( f @ X11 ) @ X12 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X9 ) @ X10 ) )
| ( $true
!= ( cP_5 @ ( f @ X10 ) @ X14 ) ) ),
inference(superposition,[],[f126,f16]) ).
thf(f128,plain,
! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X16: $i,X7: $i,X14: $i,X4: $i,X17: $i,X15: $i,X5: $i,X12: $i,X13: $i] :
( ( $true
!= ( cQ_1 @ X16 @ X15 @ X17 ) )
| ( ( cP_4 @ ( f @ X12 ) @ X3 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ X15 ) @ X1 ) )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( ( cP_4 @ ( f @ X6 ) @ X7 )
!= $true )
| ( ( cP_1 @ ( f @ X16 ) @ X0 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X10 ) @ X14 ) )
| ( ( cP_3 @ ( f @ X5 ) @ X6 )
!= $true )
| ( ( cP_2 @ ( f @ X0 ) @ X11 )
!= $true )
| ( ( cP_2 @ ( f @ X2 ) @ X5 )
!= $true )
| ( ( cP_3 @ ( f @ X13 ) @ X9 )
!= $true )
| ( ( cP_3 @ ( f @ X11 ) @ X12 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_2 @ ( f @ X1 ) @ X13 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ X17 ) @ X2 ) )
| ( $true
!= ( cP_4 @ ( f @ X9 ) @ X10 ) ) ),
inference(trivial_inequality_removal,[],[f127]) ).
thf(f129,plain,
( ! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X14: $i,X4: $i,X5: $i,X12: $i,X13: $i] :
( ( $true
!= ( cP_2 @ ( f @ X6 ) @ X10 ) )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X5 ) )
| ( $true
!= ( cP_3 @ ( f @ X12 ) @ X13 ) )
| ( $true
!= ( cP_2 @ ( f @ X11 ) @ X9 ) )
| ( ( cP_1 @ ( f @ c ) @ X11 )
!= $true )
| ( ( cP_4 @ ( f @ X5 ) @ X3 )
!= $true )
| ( ( cP_5 @ ( f @ X1 ) @ X14 )
!= $true )
| ( ( cP_4 @ ( f @ X13 ) @ X7 )
!= $true )
| ( ( cP_2 @ ( f @ X2 ) @ X12 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X10 ) @ X0 ) )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( $true
!= ( cP_1 @ ( f @ a ) @ X6 ) )
| ( $true
!= ( cP_1 @ ( f @ b ) @ X2 ) )
| ( ( cP_4 @ ( f @ X0 ) @ X1 )
!= $true )
| ( $true != $true ) )
| ~ spl0_10 ),
inference(superposition,[],[f128,f88]) ).
thf(f130,plain,
( ! [X2: $i,X3: $i,X10: $i,X0: $i,X11: $i,X1: $i,X8: $i,X6: $i,X9: $i,X7: $i,X14: $i,X4: $i,X5: $i,X12: $i,X13: $i] :
( ( ( cP_4 @ ( f @ X0 ) @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( $true
!= ( cP_1 @ ( f @ b ) @ X2 ) )
| ( ( cP_4 @ ( f @ X5 ) @ X3 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X5 ) )
| ( $true
!= ( cP_2 @ ( f @ X6 ) @ X10 ) )
| ( $true
!= ( cP_3 @ ( f @ X10 ) @ X0 ) )
| ( ( cP_4 @ ( f @ X13 ) @ X7 )
!= $true )
| ( ( cP_5 @ ( f @ X1 ) @ X14 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X11 ) @ X9 ) )
| ( ( cP_1 @ ( f @ c ) @ X11 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X12 ) @ X13 ) )
| ( $true
!= ( cP_1 @ ( f @ a ) @ X6 ) )
| ( ( cP_2 @ ( f @ X2 ) @ X12 )
!= $true )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true ) )
| ~ spl0_10 ),
inference(trivial_inequality_removal,[],[f129]) ).
thf(f132,definition,
( spl0_17
<=> ! [X7: $i,X8: $i,X13: $i,X12: $i,X2: $i] :
( ( $true
!= ( cP_1 @ ( f @ b ) @ X2 ) )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( ( cP_2 @ ( f @ X2 ) @ X12 )
!= $true )
| ( ( cP_4 @ ( f @ X13 ) @ X7 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X12 ) @ X13 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
thf(f133,plain,
( ! [X2: $i,X8: $i,X7: $i,X12: $i,X13: $i] :
( ( $true
!= ( cP_1 @ ( f @ b ) @ X2 ) )
| ( ( cP_4 @ ( f @ X13 ) @ X7 )
!= $true )
| ( ( cP_5 @ ( f @ X7 ) @ X8 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X12 ) @ X13 ) )
| ( ( cP_2 @ ( f @ X2 ) @ X12 )
!= $true ) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f132]) ).
thf(f135,definition,
( spl0_18
<=> ! [X5: $i,X4: $i,X11: $i,X9: $i,X3: $i] :
( ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_1 @ ( f @ c ) @ X11 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X11 ) @ X9 ) )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X5 ) )
| ( ( cP_4 @ ( f @ X5 ) @ X3 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
thf(f136,plain,
( ! [X3: $i,X11: $i,X9: $i,X4: $i,X5: $i] :
( ( $true
!= ( cP_2 @ ( f @ X11 ) @ X9 ) )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_4 @ ( f @ X5 ) @ X3 )
!= $true )
| ( ( cP_1 @ ( f @ c ) @ X11 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X9 ) @ X5 ) ) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f135]) ).
thf(f138,definition,
( spl0_19
<=> ! [X10: $i,X0: $i,X14: $i,X6: $i,X1: $i] :
( ( ( cP_4 @ ( f @ X0 ) @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ a ) @ X6 ) )
| ( ( cP_5 @ ( f @ X1 ) @ X14 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X6 ) @ X10 ) )
| ( $true
!= ( cP_3 @ ( f @ X10 ) @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
thf(f139,plain,
( ! [X10: $i,X0: $i,X1: $i,X6: $i,X14: $i] :
( ( $true
!= ( cP_1 @ ( f @ a ) @ X6 ) )
| ( ( cP_4 @ ( f @ X0 ) @ X1 )
!= $true )
| ( ( cP_5 @ ( f @ X1 ) @ X14 )
!= $true )
| ( $true
!= ( cP_3 @ ( f @ X10 ) @ X0 ) )
| ( $true
!= ( cP_2 @ ( f @ X6 ) @ X10 ) ) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f138]) ).
thf(f140,plain,
( spl0_17
| spl0_18
| spl0_19
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f130,f86,f138,f135,f132]) ).
thf(f141,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_3 @ ( f @ X1 ) @ X4 )
!= $true )
| ( $true
!= ( cP_1 @ ( f @ c ) @ X0 ) )
| ( ( cP_4 @ ( f @ X4 ) @ X2 )
!= $true )
| ( ( cP_2 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( $true != $true ) )
| ~ spl0_18 ),
inference(superposition,[],[f136,f28]) ).
thf(f142,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_1 @ ( f @ c ) @ X0 ) )
| ( ( cP_3 @ ( f @ X1 ) @ X4 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( ( cP_4 @ ( f @ X4 ) @ X2 )
!= $true )
| ( ( cP_2 @ X0 @ X1 )
!= $true ) )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f141]) ).
thf(f143,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true != $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( $true
!= ( cP_1 @ c @ X0 ) )
| ( $true
!= ( cP_4 @ ( f @ X2 ) @ X3 ) )
| ( $true
!= ( cP_3 @ ( f @ X1 ) @ X2 ) )
| ( ( cP_2 @ X0 @ X1 )
!= $true ) )
| ~ spl0_18 ),
inference(superposition,[],[f142,f31]) ).
thf(f144,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_3 @ ( f @ X1 ) @ X2 ) )
| ( ( cP_2 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X2 ) @ X3 ) )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( $true
!= ( cP_1 @ c @ X0 ) ) )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f143]) ).
thf(f145,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) )
| ( $true != $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_2 @ X2 @ X0 )
!= $true )
| ( ( cP_1 @ c @ X2 )
!= $true )
| ( ( cP_3 @ X0 @ X1 )
!= $true ) )
| ~ spl0_18 ),
inference(superposition,[],[f144,f8]) ).
thf(f146,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_1 @ c @ X2 )
!= $true )
| ( ( cP_2 @ X2 @ X0 )
!= $true ) )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f145]) ).
thf(f147,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_5 @ ( f @ X1 ) @ X3 )
!= $true )
| ( ( cP_2 @ X4 @ X2 )
!= $true )
| ( ( cP_1 @ c @ X4 )
!= $true )
| ( $true
!= ( cP_3 @ X2 @ X0 ) )
| ( $true != $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true ) )
| ~ spl0_18 ),
inference(superposition,[],[f146,f11]) ).
thf(f148,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_5 @ ( f @ X1 ) @ X3 )
!= $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_1 @ c @ X4 )
!= $true )
| ( $true
!= ( cP_3 @ X2 @ X0 ) )
| ( ( cP_2 @ X4 @ X2 )
!= $true ) )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f147]) ).
thf(f149,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_4 @ X2 @ X0 )
!= $true )
| ( $true != $true )
| ( $true
!= ( cP_2 @ X3 @ X4 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( ( cP_1 @ c @ X3 )
!= $true )
| ( $true
!= ( cP_3 @ X4 @ X2 ) ) )
| ~ spl0_18 ),
inference(superposition,[],[f148,f10]) ).
thf(f150,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_2 @ X3 @ X4 ) )
| ( $true
!= ( cP_3 @ X4 @ X2 ) )
| ( ( cP_4 @ X2 @ X0 )
!= $true )
| ( ( cP_1 @ c @ X3 )
!= $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f149]) ).
thf(f152,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_1 @ c @ c )
!= $true )
| ( $true != $true )
| ( ( cP_3 @ c @ X0 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_14
| ~ spl0_18 ),
inference(superposition,[],[f150,f108]) ).
thf(f157,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_3 @ c @ X0 )
!= $true )
| ( ( cP_1 @ c @ c )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_14
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f152]) ).
thf(f169,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_3 @ c @ X0 )
!= $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f157,f118]) ).
thf(f171,definition,
( spl0_22
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_3 @ a @ X0 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
thf(f172,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_3 @ a @ X0 )
!= $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f171]) ).
thf(f186,plain,
( ! [X0: $i,X1: $i] :
( ( $true
!= ( cP_4 @ c @ X0 ) )
| ( $true != $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f169,f78]) ).
thf(f187,plain,
( ! [X0: $i,X1: $i] :
( ( $true
!= ( cP_4 @ c @ X0 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f186]) ).
thf(f188,plain,
( ! [X0: $i] :
( ( ( cP_5 @ c @ X0 )
!= $true )
| ( $true != $true ) )
| ~ spl0_8
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f187,f103]) ).
thf(f189,plain,
( ! [X0: $i] :
( ( cP_5 @ c @ X0 )
!= $true )
| ~ spl0_8
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f188]) ).
thf(f190,plain,
( ( $true != $true )
| ~ spl0_8
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f189,f98]) ).
thf(f191,plain,
( $false
| ~ spl0_8
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f190]) ).
thf(f192,plain,
( ~ spl0_8
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f191]) ).
thf(f193,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_3 @ ( f @ X4 ) @ X1 )
!= $true )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( ( cP_2 @ ( f @ X0 ) @ X4 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X0 ) )
| ( $true != $true ) )
| ~ spl0_19 ),
inference(superposition,[],[f139,f31]) ).
thf(f194,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( ( cP_2 @ ( f @ X0 ) @ X4 )
!= $true )
| ( ( cP_3 @ ( f @ X4 ) @ X1 )
!= $true )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X0 ) ) )
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f193]) ).
thf(f195,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true != $true )
| ( ( cP_2 @ ( f @ X2 ) @ X3 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X2 ) )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X0 ) )
| ( $true
!= ( cP_3 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_19 ),
inference(superposition,[],[f194,f10]) ).
thf(f196,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_3 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_2 @ ( f @ X2 ) @ X3 )
!= $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X0 ) )
| ( $true
!= ( cP_1 @ a @ X2 ) ) )
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f195]) ).
thf(f197,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_5 @ X3 @ X4 ) )
| ( $true != $true )
| ( $true
!= ( cP_1 @ a @ X2 ) )
| ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_2 @ ( f @ X2 ) @ X0 ) ) )
| ~ spl0_19 ),
inference(superposition,[],[f196,f8]) ).
thf(f198,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_2 @ ( f @ X2 ) @ X0 ) )
| ( $true
!= ( cP_5 @ X3 @ X4 ) )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X2 ) )
| ( $true
!= ( cP_4 @ ( f @ X1 ) @ X3 ) ) )
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f197]) ).
thf(f199,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_3 @ X1 @ X4 ) )
| ( ( cP_4 @ ( f @ X4 ) @ X2 )
!= $true )
| ( $true != $true )
| ( $true
!= ( cP_1 @ a @ X0 ) )
| ( ( cP_2 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ X2 @ X3 ) ) )
| ~ spl0_19 ),
inference(superposition,[],[f198,f28]) ).
thf(f200,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_4 @ ( f @ X4 ) @ X2 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X0 ) )
| ( $true
!= ( cP_3 @ X1 @ X4 ) )
| ( $true
!= ( cP_5 @ X2 @ X3 ) )
| ( ( cP_2 @ X0 @ X1 )
!= $true ) )
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f199]) ).
thf(f201,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ a @ X2 ) )
| ( ( cP_2 @ X2 @ X3 )
!= $true )
| ( ( cP_5 @ X1 @ X4 )
!= $true )
| ( $true != $true )
| ( ( cP_3 @ X3 @ X0 )
!= $true ) )
| ~ spl0_19 ),
inference(superposition,[],[f200,f11]) ).
thf(f202,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_1 @ a @ X2 ) )
| ( ( cP_3 @ X3 @ X0 )
!= $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_5 @ X1 @ X4 )
!= $true )
| ( ( cP_2 @ X2 @ X3 )
!= $true ) )
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f201]) ).
thf(f203,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i] :
( ( $true
!= ( cP_5 @ X2 @ X3 ) )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_4 @ X1 @ X2 ) )
| ( $true
!= ( cP_2 @ a @ X0 ) )
| ( $true != $true ) )
| ~ spl0_1
| ~ spl0_19 ),
inference(superposition,[],[f202,f43]) ).
thf(f204,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i] :
( ( $true
!= ( cP_2 @ a @ X0 ) )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ X2 @ X3 ) )
| ( $true
!= ( cP_4 @ X1 @ X2 ) ) )
| ~ spl0_1
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f203]) ).
thf(f205,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_3 @ a @ X0 )
!= $true )
| ( $true != $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_1
| ~ spl0_11
| ~ spl0_19 ),
inference(superposition,[],[f204,f93]) ).
thf(f206,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( ( cP_3 @ a @ X0 )
!= $true )
| ( ( cP_5 @ X1 @ X2 )
!= $true ) )
| ~ spl0_1
| ~ spl0_11
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f205]) ).
thf(f207,plain,
( spl0_22
| ~ spl0_1
| ~ spl0_11
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f206,f138,f91,f41,f171]) ).
thf(f208,plain,
( ! [X0: $i,X1: $i] :
( ( $true != $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_4 @ a @ X0 ) ) )
| ~ spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f172,f83]) ).
thf(f209,plain,
( ! [X0: $i,X1: $i] :
( ( $true
!= ( cP_4 @ a @ X0 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_9
| ~ spl0_22 ),
inference(trivial_inequality_removal,[],[f208]) ).
thf(f210,plain,
( ! [X0: $i] :
( ( ( cP_5 @ a @ X0 )
!= $true )
| ( $true != $true ) )
| ~ spl0_3
| ~ spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f209,f53]) ).
thf(f211,plain,
( ! [X0: $i] :
( ( cP_5 @ a @ X0 )
!= $true )
| ~ spl0_3
| ~ spl0_9
| ~ spl0_22 ),
inference(trivial_inequality_removal,[],[f210]) ).
thf(f212,plain,
( ( $true != $true )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f211,f73]) ).
thf(f213,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_22 ),
inference(trivial_inequality_removal,[],[f212]) ).
thf(f214,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f213]) ).
thf(f215,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true != $true )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true )
| ( ( cP_2 @ ( f @ X0 ) @ X4 )
!= $true )
| ( ( cP_3 @ ( f @ X4 ) @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ b @ X0 ) )
| ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) ) )
| ~ spl0_17 ),
inference(superposition,[],[f133,f31]) ).
thf(f216,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_5 @ ( f @ X2 ) @ X3 ) )
| ( $true
!= ( cP_1 @ b @ X0 ) )
| ( ( cP_3 @ ( f @ X4 ) @ X1 )
!= $true )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true )
| ( ( cP_2 @ ( f @ X0 ) @ X4 )
!= $true ) )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f215]) ).
thf(f217,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_3 @ ( f @ X3 ) @ X4 ) )
| ( $true != $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ b @ X2 ) )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X0 ) )
| ( ( cP_2 @ ( f @ X2 ) @ X3 )
!= $true ) )
| ~ spl0_17 ),
inference(superposition,[],[f216,f10]) ).
thf(f218,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_3 @ ( f @ X3 ) @ X4 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( ( cP_2 @ ( f @ X2 ) @ X3 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X4 ) @ X0 ) )
| ( $true
!= ( cP_1 @ b @ X2 ) ) )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f217]) ).
thf(f219,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( ( cP_1 @ b @ X4 )
!= $true )
| ( $true != $true )
| ( ( cP_2 @ ( f @ X4 ) @ X0 )
!= $true )
| ( $true
!= ( cP_5 @ X2 @ X3 ) )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true ) )
| ~ spl0_17 ),
inference(superposition,[],[f218,f8]) ).
thf(f220,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_2 @ ( f @ X4 ) @ X0 )
!= $true )
| ( ( cP_1 @ b @ X4 )
!= $true )
| ( ( cP_4 @ ( f @ X1 ) @ X2 )
!= $true )
| ( ( cP_3 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_5 @ X2 @ X3 ) ) )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f219]) ).
thf(f221,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_2 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_4 @ ( f @ X2 ) @ X3 ) )
| ( $true != $true )
| ( $true
!= ( cP_1 @ b @ X0 ) )
| ( ( cP_3 @ X1 @ X2 )
!= $true )
| ( $true
!= ( cP_5 @ X3 @ X4 ) ) )
| ~ spl0_17 ),
inference(superposition,[],[f220,f28]) ).
thf(f222,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_4 @ ( f @ X2 ) @ X3 ) )
| ( ( cP_3 @ X1 @ X2 )
!= $true )
| ( $true
!= ( cP_1 @ b @ X0 ) )
| ( $true
!= ( cP_5 @ X3 @ X4 ) )
| ( ( cP_2 @ X0 @ X1 )
!= $true ) )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f221]) ).
thf(f223,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( ( cP_5 @ X1 @ X4 )
!= $true )
| ( ( cP_2 @ X3 @ X2 )
!= $true )
| ( $true != $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true )
| ( $true
!= ( cP_1 @ b @ X3 ) )
| ( $true
!= ( cP_3 @ X2 @ X0 ) ) )
| ~ spl0_17 ),
inference(superposition,[],[f222,f11]) ).
thf(f224,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
!= ( cP_1 @ b @ X3 ) )
| ( ( cP_5 @ X1 @ X4 )
!= $true )
| ( $true
!= ( cP_3 @ X2 @ X0 ) )
| ( ( cP_2 @ X3 @ X2 )
!= $true )
| ( ( cP_4 @ X0 @ X1 )
!= $true ) )
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f223]) ).
thf(f225,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i] :
( ( $true != $true )
| ( $true
!= ( cP_4 @ X3 @ X0 ) )
| ( ( cP_5 @ X0 @ X1 )
!= $true )
| ( ( cP_3 @ X2 @ X3 )
!= $true )
| ( ( cP_2 @ b @ X2 )
!= $true ) )
| ~ spl0_15
| ~ spl0_17 ),
inference(superposition,[],[f224,f113]) ).
thf(f226,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i] :
( ( $true
!= ( cP_4 @ X3 @ X0 ) )
| ( ( cP_3 @ X2 @ X3 )
!= $true )
| ( ( cP_2 @ b @ X2 )
!= $true )
| ( ( cP_5 @ X0 @ X1 )
!= $true ) )
| ~ spl0_15
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f225]) ).
thf(f229,plain,
( ! [X0: $i,X1: $i] :
( ( $true != $true )
| ( ( cP_5 @ b @ X1 )
!= $true )
| ( ( cP_3 @ X0 @ b )
!= $true )
| ( $true
!= ( cP_2 @ b @ X0 ) ) )
| ~ spl0_5
| ~ spl0_15
| ~ spl0_17 ),
inference(superposition,[],[f226,f63]) ).
thf(f236,plain,
( ! [X0: $i,X1: $i] :
( ( $true
!= ( cP_2 @ b @ X0 ) )
| ( ( cP_3 @ X0 @ b )
!= $true )
| ( ( cP_5 @ b @ X1 )
!= $true ) )
| ~ spl0_5
| ~ spl0_15
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f229]) ).
thf(f259,definition,
( spl0_32
<=> ! [X0: $i] :
( ( $true
!= ( cP_2 @ b @ X0 ) )
| ( ( cP_3 @ X0 @ b )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
thf(f260,plain,
( ! [X0: $i] :
( ( $true
!= ( cP_2 @ b @ X0 ) )
| ( ( cP_3 @ X0 @ b )
!= $true ) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f259]) ).
thf(f262,definition,
( spl0_33
<=> ! [X1: $i] :
( ( cP_5 @ b @ X1 )
!= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
thf(f263,plain,
( ! [X1: $i] :
( ( cP_5 @ b @ X1 )
!= $true )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f262]) ).
thf(f264,plain,
( spl0_32
| spl0_33
| ~ spl0_5
| ~ spl0_15
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f236,f132,f111,f61,f262,f259]) ).
thf(f289,plain,
( ( ( cP_3 @ b @ b )
!= $true )
| ( $true != $true )
| ~ spl0_6
| ~ spl0_32 ),
inference(superposition,[],[f260,f68]) ).
thf(f290,plain,
( ( ( cP_3 @ b @ b )
!= $true )
| ~ spl0_6
| ~ spl0_32 ),
inference(trivial_inequality_removal,[],[f289]) ).
thf(f291,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f290,f48]) ).
thf(f292,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f291]) ).
thf(f293,plain,
( ( $true != $true )
| ~ spl0_4
| ~ spl0_33 ),
inference(superposition,[],[f263,f58]) ).
thf(f294,plain,
( $false
| ~ spl0_4
| ~ spl0_33 ),
inference(trivial_inequality_removal,[],[f293]) ).
thf(f295,plain,
( ~ spl0_4
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f294]) ).
cnf(s1,plain,
spl0_1,
inference(sat_conversion,[],[f44]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f49]) ).
cnf(s3,plain,
spl0_3,
inference(sat_conversion,[],[f54]) ).
cnf(s4,plain,
spl0_4,
inference(sat_conversion,[],[f59]) ).
cnf(s5,plain,
spl0_5,
inference(sat_conversion,[],[f64]) ).
cnf(s6,plain,
spl0_6,
inference(sat_conversion,[],[f69]) ).
cnf(s7,plain,
spl0_7,
inference(sat_conversion,[],[f74]) ).
cnf(s8,plain,
spl0_8,
inference(sat_conversion,[],[f79]) ).
cnf(s9,plain,
spl0_9,
inference(sat_conversion,[],[f84]) ).
cnf(s10,plain,
spl0_10,
inference(sat_conversion,[],[f89]) ).
cnf(s11,plain,
spl0_11,
inference(sat_conversion,[],[f94]) ).
cnf(s12,plain,
spl0_12,
inference(sat_conversion,[],[f99]) ).
cnf(s13,plain,
spl0_13,
inference(sat_conversion,[],[f104]) ).
cnf(s14,plain,
spl0_14,
inference(sat_conversion,[],[f109]) ).
cnf(s15,plain,
spl0_15,
inference(sat_conversion,[],[f114]) ).
cnf(s16,plain,
spl0_16,
inference(sat_conversion,[],[f119]) ).
cnf(s17,plain,
( ~ spl0_10
| spl0_17
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f140]) ).
cnf(s21,plain,
( ~ spl0_8
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_16
| ~ spl0_18 ),
inference(sat_conversion,[],[f192]) ).
cnf(s22,plain,
( ~ spl0_1
| ~ spl0_11
| ~ spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f207]) ).
cnf(s23,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_22 ),
inference(sat_conversion,[],[f214]) ).
cnf(s27,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_17
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f264]) ).
cnf(s32,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_32 ),
inference(sat_conversion,[],[f292]) ).
cnf(s33,plain,
( ~ spl0_4
| ~ spl0_33 ),
inference(sat_conversion,[],[f295]) ).
cnf(s35,plain,
~ spl0_18,
inference(rat,[],[s21,s12,s16,s14,s13,s8]) ).
cnf(s36,plain,
~ spl0_33,
inference(rat,[],[s33,s4]) ).
cnf(s37,plain,
~ spl0_22,
inference(rat,[],[s23,s7,s9,s3]) ).
cnf(s38,plain,
~ spl0_32,
inference(rat,[],[s32,s6,s2]) ).
cnf(s39,plain,
~ spl0_17,
inference(rat,[],[s27,s36,s5,s15,s38]) ).
cnf(s40,plain,
spl0_19,
inference(rat,[],[s17,s35,s10,s39]) ).
cnf(s41,plain,
~ spl0_1,
inference(rat,[],[s22,s37,s11,s40]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s1,s41]) ).
thf(f296,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO388^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:51:59 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.31 % (2747617)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.19/0.31 % (2747622)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2530292583:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.19/0.31 % (2747624)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3365211047:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.19/0.31 % (2747623)lrs+10_16_si=on:nwc=1.5:random_seed=1362089374:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.19/0.31 % (2747628)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.19/0.31 % (2747628)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.19/0.31 % (2747625)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=406902433: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.19/0.31 % (2747626)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3208060881:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.19/0.31 % (2747624)Instruction limit reached!
% 0.19/0.31 % (2747624)------------------------------
% 0.19/0.31 % (2747624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747624)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747624)Termination reason: Instruction limit
% 0.19/0.31 % (2747624)Termination phase: Saturation
% 0.19/0.31 % (2747624)Time elapsed: 0.002 s
% 0.19/0.31 % (2747624)Peak memory usage: 11 MB
% 0.19/0.31 % (2747624)Instructions burned: 4 (million)
% 0.19/0.31 % (2747627)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=608916416:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.19/0.31 % (2747628)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=4243352232:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.19/0.31 % (2747623)Instruction limit reached!
% 0.19/0.31 % (2747623)------------------------------
% 0.19/0.31 % (2747623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747623)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747623)Termination reason: Instruction limit
% 0.19/0.31 % (2747623)Termination phase: Saturation
% 0.19/0.31 % (2747623)Time elapsed: 0.010 s
% 0.19/0.31 % (2747623)Peak memory usage: 12 MB
% 0.19/0.31 % (2747623)Instructions burned: 20 (million)
% 0.19/0.31 % (2747626)Instruction limit reached!
% 0.19/0.31 % (2747626)------------------------------
% 0.19/0.31 % (2747626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747626)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747626)Termination reason: Instruction limit
% 0.19/0.31 % (2747626)Termination phase: Saturation
% 0.19/0.31 % (2747626)Time elapsed: 0.014 s
% 0.19/0.31 % (2747626)Peak memory usage: 11 MB
% 0.19/0.31 % (2747626)Instructions burned: 25 (million)
% 0.19/0.31 % (2747622)Instruction limit reached!
% 0.19/0.31 % (2747622)------------------------------
% 0.19/0.31 % (2747622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747622)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747625) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2747617-2747625"...
% 0.19/0.31 % (2747622)Termination reason: Instruction limit
% 0.19/0.31 % (2747622)Termination phase: Saturation
% 0.19/0.31 % (2747622)Time elapsed: 0.026 s
% 0.19/0.31 % (2747622)Peak memory usage: 12 MB
% 0.19/0.31 % (2747622)Instructions burned: 97 (million)
% 0.19/0.31 % (2747636)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1681984117:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.19/0.31 % (2747636)Instruction limit reached!
% 0.19/0.31 % (2747636)------------------------------
% 0.19/0.31 % (2747636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747636)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747636)Termination reason: Instruction limit
% 0.19/0.31 % (2747636)Termination phase: Saturation
% 0.19/0.31 % (2747636)Time elapsed: 0.002 s
% 0.19/0.31 % (2747636)Peak memory usage: 12 MB
% 0.19/0.31 % (2747636)Instructions burned: 4 (million)
% 0.19/0.31 % (2747625)...printing done.
% 0.19/0.31 % (2747639)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2893899642:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.19/0.31 % (2747638)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.19/0.31 % (2747625)Refutation found. Thanks to Tanya!
% 0.19/0.31 % SZS status Theorem for theBenchmark
% 0.19/0.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.31 % (2747625)------------------------------
% 0.19/0.31 % (2747625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (2747625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (2747625)CaDiCaL version: 2.1.3
% 0.19/0.31 % (2747625)Termination reason: Refutation
% 0.19/0.31 % (2747625)Time elapsed: 0.025 s
% 0.19/0.31 % (2747625)Peak memory usage: 13 MB
% 0.19/0.31 % (2747625)Instructions burned: 46 (million)
% 0.19/0.31 % (2747617)Success in time 0.071 s
% 0.19/0.31 % Vampire exiting
%------------------------------------------------------------------------------