%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW678_1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 : Tue Sep 29 01:31:07 PM UTC 2026
% Result : Theorem 3.91s 1.41s
% Output : Refutation 5.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 183 ( 13 unt; 0 typ; 12 def)
% Number of atoms : 877 ( 215 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1025 ( 331 ~; 459 |; 151 &)
% ( 29 <=>; 52 =>; 0 <=; 3 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 2 ( 2 fml; 0 var)
% Number arithmetic : 167 ( 91 atm; 0 fun; 0 num; 76 var)
% Number of types : 3 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 14 usr; 12 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 164 ( 0 sgn 126 !; 38 ?; 164 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Tree': $tType ).
tff(func_def_0,type,
'empty:Tree': 'Tree' ).
tff(func_def_1,type,
'left:(Tree)>Tree': 'Tree' > 'Tree' ).
tff(func_def_2,type,
'val:(Tree)>Int': 'Tree' > $int ).
tff(func_def_3,type,
'node:(Int*Tree*Tree)>Tree': ( $int * 'Tree' * 'Tree' ) > 'Tree' ).
tff(func_def_4,type,
'right:(Tree)>Tree': 'Tree' > 'Tree' ).
tff(func_def_9,type,
sK2: ( 'Tree' * $int ) > 'Tree' ).
tff(func_def_10,type,
sK3: ( 'Tree' * $int ) > 'Tree' ).
tff(func_def_11,type,
sK4: 'Tree' ).
tff(func_def_12,type,
sK5: $int ).
tff(func_def_13,type,
sK6: 'Tree' > $int ).
tff(func_def_14,type,
sK7: 'Tree' > $int ).
tff(pred_def_1,type,
searchtree: 'Tree' > $o ).
tff(pred_def_2,type,
in: ( $int * 'Tree' ) > $o ).
tff(pred_def_6,type,
sP0: ( 'Tree' * $int ) > $o ).
tff(pred_def_7,type,
sP1: 'Tree' > $o ).
tff(f6,axiom,
! [X1: 'Tree',X0: $int] :
( ( ( ( X1 != 'empty:Tree' )
=> ( in(X0,'right:(Tree)>Tree'(X1))
| ( X0 = 'val:(Tree)>Int'(X1) )
| in(X0,'left:(Tree)>Tree'(X1)) ) )
& ( ( X1 = 'empty:Tree' )
=> $false ) )
<=> in(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_005) ).
tff(f7,axiom,
! [X0: 'Tree'] :
( ( ( ( X0 != 'empty:Tree' )
=> ( ! [X1: $int] :
( in(X1,'left:(Tree)>Tree'(X0))
=> $lesseq(X1,'val:(Tree)>Int'(X0)) )
& searchtree('left:(Tree)>Tree'(X0))
& ! [X1: $int] :
( in(X1,'right:(Tree)>Tree'(X0))
=> $greater(X1,'val:(Tree)>Int'(X0)) )
& searchtree('right:(Tree)>Tree'(X0)) ) )
& ( ( X0 = 'empty:Tree' )
=> $true ) )
<=> searchtree(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_006) ).
tff(f8,conjecture,
! [X0: 'Tree',X1: $int] :
( searchtree(X0)
=> ( in(X1,X0)
<=> ( ( ( X0 != 'empty:Tree' )
=> ( ( ( X1 = 'val:(Tree)>Int'(X0) )
=> $true )
& ( ( X1 != 'val:(Tree)>Int'(X0) )
=> ( ( ~ $less(X1,'val:(Tree)>Int'(X0))
=> ? [X3: 'Tree'] :
( ( X3 = 'right:(Tree)>Tree'(X0) )
& in(X1,X3) ) )
& ( $less(X1,'val:(Tree)>Int'(X0))
=> ? [X2: 'Tree'] :
( ( X2 = 'left:(Tree)>Tree'(X0) )
& in(X1,X2) ) ) ) ) ) )
& ( ( X0 = 'empty:Tree' )
=> $false ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_007) ).
tff(f9,negated_conjecture,
~ ! [X0: 'Tree',X1: $int] :
( searchtree(X0)
=> ( in(X1,X0)
<=> ( ( ( X0 != 'empty:Tree' )
=> ( ( ( X1 = 'val:(Tree)>Int'(X0) )
=> $true )
& ( ( X1 != 'val:(Tree)>Int'(X0) )
=> ( ( ~ $less(X1,'val:(Tree)>Int'(X0))
=> ? [X3: 'Tree'] :
( ( X3 = 'right:(Tree)>Tree'(X0) )
& in(X1,X3) ) )
& ( $less(X1,'val:(Tree)>Int'(X0))
=> ? [X2: 'Tree'] :
( ( X2 = 'left:(Tree)>Tree'(X0) )
& in(X1,X2) ) ) ) ) ) )
& ( ( X0 = 'empty:Tree' )
=> $false ) ) ) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
tff(f10,plain,
! [X0: 'Tree'] :
( ( ( ( X0 != 'empty:Tree' )
=> ( ! [X1: $int] :
( in(X1,'left:(Tree)>Tree'(X0))
=> ~ $less('val:(Tree)>Int'(X0),X1) )
& searchtree('left:(Tree)>Tree'(X0))
& ! [X1: $int] :
( in(X1,'right:(Tree)>Tree'(X0))
=> $less('val:(Tree)>Int'(X0),X1) )
& searchtree('right:(Tree)>Tree'(X0)) ) )
& ( ( X0 = 'empty:Tree' )
=> $true ) )
<=> searchtree(X0) ),
inference(theory_normalization,[],[f7]) ).
tff(f16,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f17,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,X2)
| ~ $less(X0,X1)
| $less(X0,X2) ),
introduced(definition,[],[tha_transitivity]) ).
tff(f18,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f23,plain,
~ ! [X0: 'Tree',X1: $int] :
( searchtree(X0)
=> ( in(X1,X0)
<=> ( ( ( X0 != 'empty:Tree' )
=> ( ( ( X1 = 'val:(Tree)>Int'(X0) )
=> $true )
& ( ( X1 != 'val:(Tree)>Int'(X0) )
=> ( ( ~ $less(X1,'val:(Tree)>Int'(X0))
=> ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) )
& ( $less(X1,'val:(Tree)>Int'(X0))
=> ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) ) ) ) ) ) )
& ( ( X0 = 'empty:Tree' )
=> $false ) ) ) ),
inference(rectify,[],[f9]) ).
tff(f24,plain,
~ ! [X0: 'Tree',X1: $int] :
( searchtree(X0)
=> ( in(X1,X0)
<=> ( ( ( X0 != 'empty:Tree' )
=> ( ( X1 != 'val:(Tree)>Int'(X0) )
=> ( ( ~ $less(X1,'val:(Tree)>Int'(X0))
=> ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) )
& ( $less(X1,'val:(Tree)>Int'(X0))
=> ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) ) ) ) ) )
& ( ( ~ X0 ) = 'empty:Tree' ) ) ) ),
inference(true_and_false_elimination,[],[f23]) ).
tff(f25,plain,
~ ! [X1: $int,X0: 'Tree'] :
( searchtree(X0)
=> ( ( ( 'empty:Tree' != X0 )
& ( ( X0 != 'empty:Tree' )
=> ( ( X1 != 'val:(Tree)>Int'(X0) )
=> ( ( ~ $less(X1,'val:(Tree)>Int'(X0))
=> ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) )
& ( $less(X1,'val:(Tree)>Int'(X0))
=> ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) ) ) ) ) ) )
<=> in(X1,X0) ) ),
inference(flattening,[],[f24]) ).
tff(f28,plain,
! [X0: 'Tree'] :
( ( ( ( X0 != 'empty:Tree' )
=> ( ! [X1: $int] :
( in(X1,'left:(Tree)>Tree'(X0))
=> ~ $less('val:(Tree)>Int'(X0),X1) )
& searchtree('right:(Tree)>Tree'(X0))
& searchtree('left:(Tree)>Tree'(X0))
& ! [X2: $int] :
( in(X2,'right:(Tree)>Tree'(X0))
=> $less('val:(Tree)>Int'(X0),X2) ) ) )
& ( ( X0 = 'empty:Tree' )
=> $true ) )
<=> searchtree(X0) ),
inference(rectify,[],[f10]) ).
tff(f29,plain,
! [X0: 'Tree'] :
( searchtree(X0)
<=> ( ( X0 != 'empty:Tree' )
=> ( ! [X1: $int] :
( in(X1,'left:(Tree)>Tree'(X0))
=> ~ $less('val:(Tree)>Int'(X0),X1) )
& searchtree('right:(Tree)>Tree'(X0))
& searchtree('left:(Tree)>Tree'(X0))
& ! [X2: $int] :
( in(X2,'right:(Tree)>Tree'(X0))
=> $less('val:(Tree)>Int'(X0),X2) ) ) ) ),
inference(true_and_false_elimination,[],[f28]) ).
tff(f30,plain,
! [X0: 'Tree',X1: $int] :
( ( ( ( 'empty:Tree' != X0 )
=> ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 )
| in(X1,'left:(Tree)>Tree'(X0)) ) )
& ( ( 'empty:Tree' = X0 )
=> $false ) )
<=> in(X1,X0) ),
inference(rectify,[],[f6]) ).
tff(f31,plain,
! [X0: 'Tree',X1: $int] :
( ( ( ( 'empty:Tree' != X0 )
=> ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 )
| in(X1,'left:(Tree)>Tree'(X0)) ) )
& ( ( ~ 'empty:Tree' ) = X0 ) )
<=> in(X1,X0) ),
inference(true_and_false_elimination,[],[f30]) ).
tff(f32,plain,
! [X0: 'Tree',X1: $int] :
( ( ( 'empty:Tree' != X0 )
& ( ( 'empty:Tree' != X0 )
=> ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 )
| in(X1,'left:(Tree)>Tree'(X0)) ) ) )
<=> in(X1,X0) ),
inference(flattening,[],[f31]) ).
tff(f34,plain,
! [X0: 'Tree',X1: $int] :
( ( ( 'empty:Tree' != X0 )
& ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 )
| in(X1,'left:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 ) ) )
<=> in(X1,X0) ),
inference(ennf_transformation,[],[f32]) ).
tff(f35,plain,
! [X1: $int,X0: 'Tree'] :
( in(X1,X0)
<=> ( ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 )
| in(X1,'left:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 ) )
& ( 'empty:Tree' != X0 ) ) ),
inference(flattening,[],[f34]) ).
tff(f36,plain,
? [X1: $int,X0: 'Tree'] :
( ( ( ( 'empty:Tree' != X0 )
& ( ( ( ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) ) )
| ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 ) ) )
<~> in(X1,X0) )
& searchtree(X0) ),
inference(ennf_transformation,[],[f25]) ).
tff(f37,plain,
? [X0: 'Tree',X1: $int] :
( searchtree(X0)
& ( in(X1,X0)
<~> ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) ) ) ) ) ) ),
inference(flattening,[],[f36]) ).
tff(f38,plain,
! [X0: 'Tree'] :
( ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X2: $int] :
( ~ in(X2,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X2) )
& ! [X1: $int] :
( ~ $less('val:(Tree)>Int'(X0),X1)
| ~ in(X1,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) ) )
<=> searchtree(X0) ),
inference(ennf_transformation,[],[f29]) ).
tff(f39,definition,
! [X0: 'Tree',X1: $int] :
( sP0(X0,X1)
<=> ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f40,plain,
? [X0: 'Tree',X1: $int] :
( searchtree(X0)
& ( in(X1,X0)
<~> sP0(X0,X1) ) ),
inference(definition_folding,[],[f37,f39]) ).
tff(f41,definition,
! [X0: 'Tree'] :
( sP1(X0)
<=> ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X2: $int] :
( ~ in(X2,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X2) )
& ! [X1: $int] :
( ~ $less('val:(Tree)>Int'(X0),X1)
| ~ in(X1,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f42,plain,
! [X0: 'Tree'] :
( sP1(X0)
<=> searchtree(X0) ),
inference(definition_folding,[],[f38,f41]) ).
tff(f44,plain,
! [X0: 'Tree',X1: $int] :
( ( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ( ( 'val:(Tree)>Int'(X0) != X1 )
& ( 'empty:Tree' != X0 )
& ( ( ! [X3: 'Tree'] :
( ~ in(X1,X3)
| ( 'left:(Tree)>Tree'(X0) != X3 ) )
& $less(X1,'val:(Tree)>Int'(X0)) )
| ( ~ $less(X1,'val:(Tree)>Int'(X0))
& ! [X2: 'Tree'] :
( ~ in(X1,X2)
| ( 'right:(Tree)>Tree'(X0) != X2 ) ) ) ) ) )
& ( ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) ) ) ) )
| ~ sP0(X0,X1) ) ),
inference(nnf_transformation,[],[f39]) ).
tff(f45,plain,
! [X0: 'Tree',X1: $int] :
( ( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ( ( 'val:(Tree)>Int'(X0) != X1 )
& ( 'empty:Tree' != X0 )
& ( ( ! [X3: 'Tree'] :
( ~ in(X1,X3)
| ( 'left:(Tree)>Tree'(X0) != X3 ) )
& $less(X1,'val:(Tree)>Int'(X0)) )
| ( ~ $less(X1,'val:(Tree)>Int'(X0))
& ! [X2: 'Tree'] :
( ~ in(X1,X2)
| ( 'right:(Tree)>Tree'(X0) != X2 ) ) ) ) ) )
& ( ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ? [X3: 'Tree'] :
( in(X1,X3)
& ( 'left:(Tree)>Tree'(X0) = X3 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X2: 'Tree'] :
( in(X1,X2)
& ( 'right:(Tree)>Tree'(X0) = X2 ) ) ) ) ) )
| ~ sP0(X0,X1) ) ),
inference(flattening,[],[f44]) ).
tff(f46,plain,
! [X0: 'Tree',X1: $int] :
( ( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ( ( 'val:(Tree)>Int'(X0) != X1 )
& ( 'empty:Tree' != X0 )
& ( ( ! [X2: 'Tree'] :
( ~ in(X1,X2)
| ( 'left:(Tree)>Tree'(X0) != X2 ) )
& $less(X1,'val:(Tree)>Int'(X0)) )
| ( ~ $less(X1,'val:(Tree)>Int'(X0))
& ! [X3: 'Tree'] :
( ~ in(X1,X3)
| ( 'right:(Tree)>Tree'(X0) != X3 ) ) ) ) ) )
& ( ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ? [X4: 'Tree'] :
( in(X1,X4)
& ( 'left:(Tree)>Tree'(X0) = X4 ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ? [X5: 'Tree'] :
( in(X1,X5)
& ( 'right:(Tree)>Tree'(X0) = X5 ) ) ) ) ) )
| ~ sP0(X0,X1) ) ),
inference(rectify,[],[f45]) ).
tff(f47,plain,
! [X0: 'Tree',X1: $int] :
( ( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ( ( 'val:(Tree)>Int'(X0) != X1 )
& ( 'empty:Tree' != X0 )
& ( ( ! [X2: 'Tree'] :
( ~ in(X1,X2)
| ( 'left:(Tree)>Tree'(X0) != X2 ) )
& $less(X1,'val:(Tree)>Int'(X0)) )
| ( ~ $less(X1,'val:(Tree)>Int'(X0))
& ! [X3: 'Tree'] :
( ~ in(X1,X3)
| ( 'right:(Tree)>Tree'(X0) != X3 ) ) ) ) ) )
& ( ( ( 'empty:Tree' != X0 )
& ( ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ( ( ( in(X1,sK2(X0,X1))
& ( 'left:(Tree)>Tree'(X0) = sK2(X0,X1) ) )
| ~ $less(X1,'val:(Tree)>Int'(X0)) )
& ( $less(X1,'val:(Tree)>Int'(X0))
| ( in(X1,sK3(X0,X1))
& ( 'right:(Tree)>Tree'(X0) = sK3(X0,X1) ) ) ) ) ) )
| ~ sP0(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X4,sK2(X0,X1)),skolemize(X5,sK3(X0,X1))],[f46]) ).
tff(f48,plain,
? [X0: 'Tree',X1: $int] :
( searchtree(X0)
& ( ~ sP0(X0,X1)
| ~ in(X1,X0) )
& ( sP0(X0,X1)
| in(X1,X0) ) ),
inference(nnf_transformation,[],[f40]) ).
tff(f49,plain,
? [X0: 'Tree',X1: $int] :
( searchtree(X0)
& ( ~ sP0(X0,X1)
| ~ in(X1,X0) )
& ( sP0(X0,X1)
| in(X1,X0) ) ),
inference(flattening,[],[f48]) ).
tff(f50,plain,
( searchtree(sK4)
& ( ~ sP0(sK4,sK5)
| ~ in(sK5,sK4) )
& ( sP0(sK4,sK5)
| in(sK5,sK4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f49]) ).
tff(f52,plain,
! [X0: 'Tree'] :
( ( sP1(X0)
| ( ( 'empty:Tree' != X0 )
& ( ~ searchtree('right:(Tree)>Tree'(X0))
| ? [X2: $int] :
( in(X2,'right:(Tree)>Tree'(X0))
& ~ $less('val:(Tree)>Int'(X0),X2) )
| ? [X1: $int] :
( $less('val:(Tree)>Int'(X0),X1)
& in(X1,'left:(Tree)>Tree'(X0)) )
| ~ searchtree('left:(Tree)>Tree'(X0)) ) ) )
& ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X2: $int] :
( ~ in(X2,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X2) )
& ! [X1: $int] :
( ~ $less('val:(Tree)>Int'(X0),X1)
| ~ in(X1,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) )
| ~ sP1(X0) ) ),
inference(nnf_transformation,[],[f41]) ).
tff(f53,plain,
! [X0: 'Tree'] :
( ( sP1(X0)
| ( ( 'empty:Tree' != X0 )
& ( ~ searchtree('right:(Tree)>Tree'(X0))
| ? [X2: $int] :
( in(X2,'right:(Tree)>Tree'(X0))
& ~ $less('val:(Tree)>Int'(X0),X2) )
| ? [X1: $int] :
( $less('val:(Tree)>Int'(X0),X1)
& in(X1,'left:(Tree)>Tree'(X0)) )
| ~ searchtree('left:(Tree)>Tree'(X0)) ) ) )
& ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X2: $int] :
( ~ in(X2,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X2) )
& ! [X1: $int] :
( ~ $less('val:(Tree)>Int'(X0),X1)
| ~ in(X1,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) )
| ~ sP1(X0) ) ),
inference(flattening,[],[f52]) ).
tff(f54,plain,
! [X0: 'Tree'] :
( ( sP1(X0)
| ( ( 'empty:Tree' != X0 )
& ( ~ searchtree('right:(Tree)>Tree'(X0))
| ? [X1: $int] :
( in(X1,'right:(Tree)>Tree'(X0))
& ~ $less('val:(Tree)>Int'(X0),X1) )
| ? [X2: $int] :
( $less('val:(Tree)>Int'(X0),X2)
& in(X2,'left:(Tree)>Tree'(X0)) )
| ~ searchtree('left:(Tree)>Tree'(X0)) ) ) )
& ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X3: $int] :
( ~ in(X3,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X3) )
& ! [X4: $int] :
( ~ $less('val:(Tree)>Int'(X0),X4)
| ~ in(X4,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) )
| ~ sP1(X0) ) ),
inference(rectify,[],[f53]) ).
tff(f55,plain,
! [X0: 'Tree'] :
( ( sP1(X0)
| ( ( 'empty:Tree' != X0 )
& ( ~ searchtree('right:(Tree)>Tree'(X0))
| ( in(sK6(X0),'right:(Tree)>Tree'(X0))
& ~ $less('val:(Tree)>Int'(X0),sK6(X0)) )
| ( $less('val:(Tree)>Int'(X0),sK7(X0))
& in(sK7(X0),'left:(Tree)>Tree'(X0)) )
| ~ searchtree('left:(Tree)>Tree'(X0)) ) ) )
& ( ( 'empty:Tree' = X0 )
| ( searchtree('right:(Tree)>Tree'(X0))
& ! [X3: $int] :
( ~ in(X3,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X3) )
& ! [X4: $int] :
( ~ $less('val:(Tree)>Int'(X0),X4)
| ~ in(X4,'left:(Tree)>Tree'(X0)) )
& searchtree('left:(Tree)>Tree'(X0)) )
| ~ sP1(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X1,sK6(X0)),skolemize(X2,sK7(X0))],[f54]) ).
tff(f56,plain,
! [X0: 'Tree'] :
( ( sP1(X0)
| ~ searchtree(X0) )
& ( searchtree(X0)
| ~ sP1(X0) ) ),
inference(nnf_transformation,[],[f42]) ).
tff(f59,plain,
! [X1: $int,X0: 'Tree'] :
( ( in(X1,X0)
| ( ~ in(X1,'right:(Tree)>Tree'(X0))
& ( 'empty:Tree' != X0 )
& ~ in(X1,'left:(Tree)>Tree'(X0))
& ( 'val:(Tree)>Int'(X0) != X1 ) )
| ( 'empty:Tree' = X0 ) )
& ( ( ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 )
| in(X1,'left:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 ) )
& ( 'empty:Tree' != X0 ) )
| ~ in(X1,X0) ) ),
inference(nnf_transformation,[],[f35]) ).
tff(f60,plain,
! [X1: $int,X0: 'Tree'] :
( ( in(X1,X0)
| ( ~ in(X1,'right:(Tree)>Tree'(X0))
& ( 'empty:Tree' != X0 )
& ~ in(X1,'left:(Tree)>Tree'(X0))
& ( 'val:(Tree)>Int'(X0) != X1 ) )
| ( 'empty:Tree' = X0 ) )
& ( ( ( in(X1,'right:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 )
| in(X1,'left:(Tree)>Tree'(X0))
| ( 'val:(Tree)>Int'(X0) = X1 ) )
& ( 'empty:Tree' != X0 ) )
| ~ in(X1,X0) ) ),
inference(flattening,[],[f59]) ).
tff(f61,plain,
! [X0: $int,X1: 'Tree'] :
( ( in(X0,X1)
| ( ~ in(X0,'right:(Tree)>Tree'(X1))
& ( 'empty:Tree' != X1 )
& ~ in(X0,'left:(Tree)>Tree'(X1))
& ( 'val:(Tree)>Int'(X1) != X0 ) )
| ( 'empty:Tree' = X1 ) )
& ( ( ( in(X0,'right:(Tree)>Tree'(X1))
| ( 'empty:Tree' = X1 )
| in(X0,'left:(Tree)>Tree'(X1))
| ( 'val:(Tree)>Int'(X1) = X0 ) )
& ( 'empty:Tree' != X1 ) )
| ~ in(X0,X1) ) ),
inference(rectify,[],[f60]) ).
tff(f63,plain,
! [X0: 'Tree',X1: $int] :
( ~ sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| $less(X1,'val:(Tree)>Int'(X0))
| ( 'right:(Tree)>Tree'(X0) = sK3(X0,X1) )
| ( 'val:(Tree)>Int'(X0) = X1 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f64,plain,
! [X0: 'Tree',X1: $int] :
( ~ sP0(X0,X1)
| ( 'val:(Tree)>Int'(X0) = X1 )
| in(X1,sK3(X0,X1))
| ( 'empty:Tree' = X0 )
| $less(X1,'val:(Tree)>Int'(X0)) ),
inference(cnf_transformation,[],[f47]) ).
tff(f65,plain,
! [X0: 'Tree',X1: $int] :
( ~ $less(X1,'val:(Tree)>Int'(X0))
| ( 'left:(Tree)>Tree'(X0) = sK2(X0,X1) )
| ~ sP0(X0,X1)
| ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f66,plain,
! [X0: 'Tree',X1: $int] :
( ~ $less(X1,'val:(Tree)>Int'(X0))
| in(X1,sK2(X0,X1))
| ( 'val:(Tree)>Int'(X0) = X1 )
| ( 'empty:Tree' = X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tff(f67,plain,
! [X0: 'Tree',X1: $int] :
( ( 'empty:Tree' != X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tff(f68,plain,
! [X3: 'Tree',X0: 'Tree',X1: $int] :
( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| $less(X1,'val:(Tree)>Int'(X0))
| ~ in(X1,X3)
| ( 'right:(Tree)>Tree'(X0) != X3 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f71,plain,
! [X2: 'Tree',X0: 'Tree',X1: $int] :
( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ~ in(X1,X2)
| ( 'left:(Tree)>Tree'(X0) != X2 )
| ~ $less(X1,'val:(Tree)>Int'(X0)) ),
inference(cnf_transformation,[],[f47]) ).
tff(f73,plain,
! [X0: 'Tree',X1: $int] :
( sP0(X0,X1)
| ( 'empty:Tree' = X0 )
| ( 'val:(Tree)>Int'(X0) != X1 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f74,plain,
( in(sK5,sK4)
| sP0(sK4,sK5) ),
inference(cnf_transformation,[],[f50]) ).
tff(f75,plain,
( ~ sP0(sK4,sK5)
| ~ in(sK5,sK4) ),
inference(cnf_transformation,[],[f50]) ).
tff(f76,plain,
searchtree(sK4),
inference(cnf_transformation,[],[f50]) ).
tff(f79,plain,
! [X0: 'Tree',X4: $int] :
( ~ $less('val:(Tree)>Int'(X0),X4)
| ~ in(X4,'left:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 )
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f55]) ).
tff(f80,plain,
! [X3: $int,X0: 'Tree'] :
( ~ in(X3,'right:(Tree)>Tree'(X0))
| $less('val:(Tree)>Int'(X0),X3)
| ( 'empty:Tree' = X0 )
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f55]) ).
tff(f88,plain,
! [X0: 'Tree'] :
( ~ searchtree(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f92,plain,
! [X0: $int,X1: 'Tree'] :
( ( 'empty:Tree' != X1 )
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
tff(f93,plain,
! [X0: $int,X1: 'Tree'] :
( in(X0,'left:(Tree)>Tree'(X1))
| ( 'empty:Tree' = X1 )
| in(X0,'right:(Tree)>Tree'(X1))
| ( 'val:(Tree)>Int'(X1) = X0 )
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
tff(f94,plain,
! [X0: $int,X1: 'Tree'] :
( in(X0,X1)
| ( 'val:(Tree)>Int'(X1) != X0 )
| ( 'empty:Tree' = X1 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f95,plain,
! [X0: $int,X1: 'Tree'] :
( ~ in(X0,'left:(Tree)>Tree'(X1))
| in(X0,X1)
| ( 'empty:Tree' = X1 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f97,plain,
! [X0: $int,X1: 'Tree'] :
( ~ in(X0,'right:(Tree)>Tree'(X1))
| in(X0,X1)
| ( 'empty:Tree' = X1 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f98,plain,
! [X0: 'Tree'] :
( sP0(X0,'val:(Tree)>Int'(X0))
| ( 'empty:Tree' = X0 ) ),
inference(equality_resolution,[],[f73]) ).
tff(f100,plain,
! [X0: 'Tree',X1: $int] :
( ~ $less(X1,'val:(Tree)>Int'(X0))
| sP0(X0,X1)
| ~ in(X1,'left:(Tree)>Tree'(X0))
| ( 'empty:Tree' = X0 ) ),
inference(equality_resolution,[],[f71]) ).
tff(f103,plain,
! [X0: 'Tree',X1: $int] :
( ~ in(X1,'right:(Tree)>Tree'(X0))
| $less(X1,'val:(Tree)>Int'(X0))
| sP0(X0,X1)
| ( 'empty:Tree' = X0 ) ),
inference(equality_resolution,[],[f68]) ).
tff(f104,plain,
! [X1: $int] : ~ sP0('empty:Tree',X1),
inference(equality_resolution,[],[f67]) ).
tff(f107,plain,
! [X1: 'Tree'] :
( in('val:(Tree)>Int'(X1),X1)
| ( 'empty:Tree' = X1 ) ),
inference(equality_resolution,[],[f94]) ).
tff(f108,plain,
! [X0: $int] : ~ in(X0,'empty:Tree'),
inference(equality_resolution,[],[f92]) ).
tff(f110,definition,
( spl8_1
<=> in(sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
tff(f111,plain,
( ~ in(sK5,sK4)
| spl8_1 ),
inference(avatar_component_clause,[],[f110]) ).
tff(f112,plain,
( in(sK5,sK4)
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f110]) ).
tff(f114,definition,
( spl8_2
<=> sP0(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
tff(f115,plain,
( ~ sP0(sK4,sK5)
| spl8_2 ),
inference(avatar_component_clause,[],[f114]) ).
tff(f116,plain,
( sP0(sK4,sK5)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f114]) ).
tff(f117,plain,
( spl8_1
| spl8_2 ),
inference(avatar_split_clause,[],[f74,f114,f110]) ).
tff(f118,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f75,f114,f110]) ).
tff(f126,definition,
( spl8_3
<=> $less(sK5,'val:(Tree)>Int'(sK4)) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
tff(f127,plain,
( ~ $less(sK5,'val:(Tree)>Int'(sK4))
| spl8_3 ),
inference(avatar_component_clause,[],[f126]) ).
tff(f128,plain,
( $less(sK5,'val:(Tree)>Int'(sK4))
| ~ spl8_3 ),
inference(avatar_component_clause,[],[f126]) ).
tff(f130,definition,
( spl8_4
<=> ( sK5 = 'val:(Tree)>Int'(sK4) ) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
tff(f131,plain,
( ( sK5 != 'val:(Tree)>Int'(sK4) )
| spl8_4 ),
inference(avatar_component_clause,[],[f130]) ).
tff(f132,plain,
( ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_4 ),
inference(avatar_component_clause,[],[f130]) ).
tff(f134,definition,
( spl8_5
<=> in(sK5,sK3(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
tff(f136,plain,
( in(sK5,sK3(sK4,sK5))
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f134]) ).
tff(f138,definition,
( spl8_6
<=> ( 'empty:Tree' = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
tff(f139,plain,
( ( 'empty:Tree' != sK4 )
| spl8_6 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f140,plain,
( ( 'empty:Tree' = sK4 )
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f146,definition,
( spl8_7
<=> in(sK5,sK2(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition]) ).
tff(f148,plain,
( in(sK5,sK2(sK4,sK5))
| ~ spl8_7 ),
inference(avatar_component_clause,[],[f146]) ).
tff(f156,definition,
( spl8_8
<=> ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
tff(f158,plain,
( ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) )
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f156]) ).
tff(f162,plain,
( ~ in('val:(Tree)>Int'(sK4),sK4)
| spl8_1
| ~ spl8_4 ),
inference(superposition,[],[f111,f132]) ).
tff(f169,plain,
sP1(sK4),
inference(resolution,[],[f88,f76]) ).
tff(f207,plain,
( sP0('empty:Tree',sK5)
| ~ spl8_2
| ~ spl8_6 ),
inference(superposition,[],[f116,f140]) ).
tff(f214,plain,
( $false
| ~ spl8_2
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f207,f104]) ).
tff(f215,plain,
( ~ spl8_2
| ~ spl8_6 ),
inference(avatar_contradiction_clause,[],[f214]) ).
tff(f240,plain,
( ~ sP0(sK4,'val:(Tree)>Int'(sK4))
| spl8_2
| ~ spl8_4 ),
inference(forward_demodulation,[],[f115,f132]) ).
tff(f254,plain,
( in(sK5,'empty:Tree')
| ~ spl8_1
| ~ spl8_6 ),
inference(forward_demodulation,[],[f112,f140]) ).
tff(f255,plain,
( $false
| ~ spl8_1
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f254,f108]) ).
tff(f256,plain,
( ~ spl8_1
| ~ spl8_6 ),
inference(avatar_contradiction_clause,[],[f255]) ).
tff(f257,plain,
( $less(sK5,'val:(Tree)>Int'(sK4))
| ( sK3(sK4,sK5) = 'right:(Tree)>Tree'(sK4) )
| ( 'empty:Tree' = sK4 )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_2 ),
inference(resolution,[],[f116,f63]) ).
tff(f258,plain,
( $less(sK5,'val:(Tree)>Int'(sK4))
| in(sK5,sK3(sK4,sK5))
| ( 'empty:Tree' = sK4 )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_2 ),
inference(resolution,[],[f116,f64]) ).
tff(f259,plain,
( spl8_6
| spl8_4
| spl8_3
| spl8_5
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f258,f114,f134,f126,f130,f138]) ).
tff(f261,definition,
( spl8_17
<=> ( sK3(sK4,sK5) = 'right:(Tree)>Tree'(sK4) ) ),
introduced(definition,[new_symbols(definition,[spl8_17])],[avatar_definition]) ).
tff(f263,plain,
( ( sK3(sK4,sK5) = 'right:(Tree)>Tree'(sK4) )
| ~ spl8_17 ),
inference(avatar_component_clause,[],[f261]) ).
tff(f264,plain,
( spl8_17
| spl8_4
| spl8_6
| spl8_3
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f257,f114,f126,f138,f130,f261]) ).
tff(f348,plain,
( ( 'empty:Tree' = sK4 )
| spl8_1
| ~ spl8_4 ),
inference(resolution,[],[f107,f162]) ).
tff(f354,plain,
( $false
| spl8_1
| ~ spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f348,f139]) ).
tff(f355,plain,
( spl8_1
| ~ spl8_4
| spl8_6 ),
inference(avatar_contradiction_clause,[],[f354]) ).
tff(f358,plain,
( ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ sP0(sK4,sK5)
| ( 'empty:Tree' = sK4 )
| ~ spl8_3 ),
inference(resolution,[],[f128,f65]) ).
tff(f359,plain,
( ( sK5 = 'val:(Tree)>Int'(sK4) )
| in(sK5,sK2(sK4,sK5))
| ~ sP0(sK4,sK5)
| ( 'empty:Tree' = sK4 )
| ~ spl8_3 ),
inference(resolution,[],[f128,f66]) ).
tff(f361,plain,
( in(sK5,sK2(sK4,sK5))
| ( 'empty:Tree' = sK4 )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_2
| ~ spl8_3 ),
inference(forward_subsumption_resolution,[],[f359,f116]) ).
tff(f362,plain,
( ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) )
| ( 'empty:Tree' = sK4 )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_2
| ~ spl8_3 ),
inference(forward_subsumption_resolution,[],[f358,f116]) ).
tff(f363,plain,
( ( sK5 = 'val:(Tree)>Int'(sK4) )
| in(sK5,sK2(sK4,sK5))
| ~ spl8_2
| ~ spl8_3
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f361,f139]) ).
tff(f364,plain,
( ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) )
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_2
| ~ spl8_3
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f362,f139]) ).
tff(f365,plain,
( spl8_7
| spl8_4
| ~ spl8_2
| ~ spl8_3
| spl8_6 ),
inference(avatar_split_clause,[],[f363,f138,f126,f114,f130,f146]) ).
tff(f385,plain,
( ( 'left:(Tree)>Tree'(sK4) = sK2(sK4,sK5) )
| ~ spl8_2
| ~ spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f364,f131]) ).
tff(f386,plain,
( spl8_8
| ~ spl8_2
| ~ spl8_3
| spl8_4
| spl8_6 ),
inference(avatar_split_clause,[],[f385,f138,f130,f126,f114,f156]) ).
tff(f632,plain,
( in(sK5,'left:(Tree)>Tree'(sK4))
| ~ spl8_7
| ~ spl8_8 ),
inference(superposition,[],[f148,f158]) ).
tff(f669,plain,
( in(sK5,sK4)
| ( 'empty:Tree' = sK4 )
| ~ spl8_7
| ~ spl8_8 ),
inference(resolution,[],[f632,f95]) ).
tff(f670,plain,
( ( 'empty:Tree' = sK4 )
| spl8_1
| ~ spl8_7
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f669,f111]) ).
tff(f671,plain,
( $false
| spl8_1
| spl8_6
| ~ spl8_7
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f670,f139]) ).
tff(f672,plain,
( spl8_1
| spl8_6
| ~ spl8_7
| ~ spl8_8 ),
inference(avatar_contradiction_clause,[],[f671]) ).
tff(f674,plain,
( ( sK5 = 'val:(Tree)>Int'(sK4) )
| $less('val:(Tree)>Int'(sK4),sK5)
| spl8_3 ),
inference(resolution,[],[f127,f18]) ).
tff(f676,plain,
( $less('val:(Tree)>Int'(sK4),sK5)
| spl8_3
| spl8_4 ),
inference(forward_subsumption_resolution,[],[f674,f131]) ).
tff(f679,plain,
( ( 'empty:Tree' = sK4 )
| ~ sP1(sK4)
| ~ in(sK5,'left:(Tree)>Tree'(sK4))
| spl8_3
| spl8_4 ),
inference(resolution,[],[f676,f79]) ).
tff(f681,plain,
( ~ sP1(sK4)
| ~ in(sK5,'left:(Tree)>Tree'(sK4))
| spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f679,f139]) ).
tff(f682,plain,
( ~ in(sK5,'left:(Tree)>Tree'(sK4))
| spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f681,f169]) ).
tff(f710,plain,
( ( 'empty:Tree' = sK4 )
| ~ in(sK5,sK4)
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| in(sK5,'right:(Tree)>Tree'(sK4))
| spl8_3
| spl8_4
| spl8_6 ),
inference(resolution,[],[f682,f93]) ).
tff(f745,plain,
( in(sK5,'right:(Tree)>Tree'(sK4))
| ~ spl8_5
| ~ spl8_17 ),
inference(superposition,[],[f136,f263]) ).
tff(f746,plain,
( in(sK5,sK4)
| ( 'empty:Tree' = sK4 )
| ~ spl8_5
| ~ spl8_17 ),
inference(resolution,[],[f745,f97]) ).
tff(f754,plain,
( in(sK5,sK4)
| ~ spl8_5
| spl8_6
| ~ spl8_17 ),
inference(forward_subsumption_resolution,[],[f746,f139]) ).
tff(f756,plain,
( spl8_1
| ~ spl8_5
| spl8_6
| ~ spl8_17 ),
inference(avatar_split_clause,[],[f754,f261,f138,f134,f110]) ).
tff(f758,plain,
( ( sK5 = 'val:(Tree)>Int'(sK4) )
| in(sK5,'right:(Tree)>Tree'(sK4))
| ~ in(sK5,sK4)
| spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f710,f139]) ).
tff(f759,plain,
( ~ in(sK5,sK4)
| in(sK5,'right:(Tree)>Tree'(sK4))
| spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f758,f131]) ).
tff(f761,definition,
( spl8_53
<=> in(sK5,'right:(Tree)>Tree'(sK4)) ),
introduced(definition,[new_symbols(definition,[spl8_53])],[avatar_definition]) ).
tff(f763,plain,
( in(sK5,'right:(Tree)>Tree'(sK4))
| ~ spl8_53 ),
inference(avatar_component_clause,[],[f761]) ).
tff(f764,plain,
( ~ spl8_1
| spl8_53
| spl8_3
| spl8_4
| spl8_6 ),
inference(avatar_split_clause,[],[f759,f138,f130,f126,f761,f110]) ).
tff(f766,plain,
( ( 'empty:Tree' = sK4 )
| sP0(sK4,sK5)
| $less(sK5,'val:(Tree)>Int'(sK4))
| ~ spl8_53 ),
inference(resolution,[],[f763,f103]) ).
tff(f769,plain,
( $less(sK5,'val:(Tree)>Int'(sK4))
| sP0(sK4,sK5)
| spl8_6
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f766,f139]) ).
tff(f770,plain,
( sP0(sK4,sK5)
| spl8_3
| spl8_6
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f769,f127]) ).
tff(f771,plain,
( $false
| spl8_2
| spl8_3
| spl8_6
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f770,f115]) ).
tff(f772,plain,
( spl8_2
| spl8_3
| spl8_6
| ~ spl8_53 ),
inference(avatar_contradiction_clause,[],[f771]) ).
tff(f775,plain,
( sP0(sK4,sK5)
| ~ in(sK5,'left:(Tree)>Tree'(sK4))
| ( 'empty:Tree' = sK4 )
| ~ spl8_3 ),
inference(resolution,[],[f128,f100]) ).
tff(f776,plain,
( ! [X0: $int] :
( ~ $less(X0,sK5)
| $less(X0,'val:(Tree)>Int'(sK4)) )
| ~ spl8_3 ),
inference(resolution,[],[f128,f17]) ).
tff(f777,plain,
( ( 'empty:Tree' = sK4 )
| ~ in(sK5,'left:(Tree)>Tree'(sK4))
| spl8_2
| ~ spl8_3 ),
inference(forward_subsumption_resolution,[],[f775,f115]) ).
tff(f778,plain,
( ~ in(sK5,'left:(Tree)>Tree'(sK4))
| spl8_2
| ~ spl8_3
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f777,f139]) ).
tff(f779,plain,
( in(sK5,'right:(Tree)>Tree'(sK4))
| ( 'empty:Tree' = sK4 )
| ~ in(sK5,sK4)
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| spl8_2
| ~ spl8_3
| spl8_6 ),
inference(resolution,[],[f778,f93]) ).
tff(f780,plain,
( ~ in(sK5,sK4)
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| in(sK5,'right:(Tree)>Tree'(sK4))
| spl8_2
| ~ spl8_3
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f779,f139]) ).
tff(f781,plain,
( in(sK5,'right:(Tree)>Tree'(sK4))
| ( sK5 = 'val:(Tree)>Int'(sK4) )
| ~ spl8_1
| spl8_2
| ~ spl8_3
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f780,f112]) ).
tff(f782,plain,
( in(sK5,'right:(Tree)>Tree'(sK4))
| ~ spl8_1
| spl8_2
| ~ spl8_3
| spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f781,f131]) ).
tff(f783,plain,
( spl8_53
| ~ spl8_1
| spl8_2
| ~ spl8_3
| spl8_4
| spl8_6 ),
inference(avatar_split_clause,[],[f782,f138,f130,f126,f114,f110,f761]) ).
tff(f787,plain,
( ~ sP1(sK4)
| ( 'empty:Tree' = sK4 )
| $less('val:(Tree)>Int'(sK4),sK5)
| ~ spl8_53 ),
inference(resolution,[],[f763,f80]) ).
tff(f788,plain,
( $less('val:(Tree)>Int'(sK4),sK5)
| ( 'empty:Tree' = sK4 )
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f787,f169]) ).
tff(f789,plain,
( $less('val:(Tree)>Int'(sK4),sK5)
| spl8_6
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f788,f139]) ).
tff(f835,plain,
( $less('val:(Tree)>Int'(sK4),'val:(Tree)>Int'(sK4))
| ~ spl8_3
| spl8_6
| ~ spl8_53 ),
inference(resolution,[],[f776,f789]) ).
tff(f836,plain,
( $false
| ~ spl8_3
| spl8_6
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f835,f16]) ).
tff(f837,plain,
( ~ spl8_3
| spl8_6
| ~ spl8_53 ),
inference(avatar_contradiction_clause,[],[f836]) ).
tff(f838,plain,
( ( 'empty:Tree' = sK4 )
| spl8_2
| ~ spl8_4 ),
inference(resolution,[],[f240,f98]) ).
tff(f839,plain,
( $false
| spl8_2
| ~ spl8_4
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f838,f139]) ).
tff(f840,plain,
( spl8_2
| ~ spl8_4
| spl8_6 ),
inference(avatar_contradiction_clause,[],[f839]) ).
cnf(s1,plain,
( spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f117]) ).
cnf(s2,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f118]) ).
cnf(s12,plain,
( ~ spl8_2
| ~ spl8_6 ),
inference(sat_conversion,[],[f215]) ).
cnf(s18,plain,
( ~ spl8_1
| ~ spl8_6 ),
inference(sat_conversion,[],[f256]) ).
cnf(s19,plain,
( ~ spl8_2
| spl8_3
| spl8_4
| spl8_5
| spl8_6 ),
inference(sat_conversion,[],[f259]) ).
cnf(s20,plain,
( ~ spl8_2
| spl8_3
| spl8_4
| spl8_6
| spl8_17 ),
inference(sat_conversion,[],[f264]) ).
cnf(s27,plain,
( spl8_1
| ~ spl8_4
| spl8_6 ),
inference(sat_conversion,[],[f355]) ).
cnf(s28,plain,
( ~ spl8_2
| ~ spl8_3
| spl8_4
| spl8_6
| spl8_7 ),
inference(sat_conversion,[],[f365]) ).
cnf(s32,plain,
( ~ spl8_2
| ~ spl8_3
| spl8_4
| spl8_6
| spl8_8 ),
inference(sat_conversion,[],[f386]) ).
cnf(s51,plain,
( spl8_1
| spl8_6
| ~ spl8_7
| ~ spl8_8 ),
inference(sat_conversion,[],[f672]) ).
cnf(s58,plain,
( spl8_1
| ~ spl8_5
| spl8_6
| ~ spl8_17 ),
inference(sat_conversion,[],[f756]) ).
cnf(s60,plain,
( ~ spl8_1
| spl8_3
| spl8_4
| spl8_6
| spl8_53 ),
inference(sat_conversion,[],[f764]) ).
cnf(s61,plain,
( spl8_2
| spl8_3
| spl8_6
| ~ spl8_53 ),
inference(sat_conversion,[],[f772]) ).
cnf(s62,plain,
( ~ spl8_1
| spl8_2
| ~ spl8_3
| spl8_4
| spl8_6
| spl8_53 ),
inference(sat_conversion,[],[f783]) ).
cnf(s70,plain,
( ~ spl8_3
| spl8_6
| ~ spl8_53 ),
inference(sat_conversion,[],[f837]) ).
cnf(s71,plain,
( spl8_2
| ~ spl8_4
| spl8_6 ),
inference(sat_conversion,[],[f840]) ).
cnf(s72,plain,
( spl8_3
| spl8_1 ),
inference(rat,[],[s58,s19,s20,s27,s12,s1]) ).
cnf(s73,plain,
spl8_1,
inference(rat,[],[s51,s28,s32,s72,s27,s12,s1]) ).
cnf(s74,plain,
~ spl8_6,
inference(rat,[],[s18,s73]) ).
cnf(s75,plain,
~ spl8_2,
inference(rat,[],[s2,s73]) ).
cnf(s78,plain,
~ spl8_4,
inference(rat,[],[s71,s74,s75]) ).
cnf(s79,plain,
spl8_3,
inference(rat,[],[s60,s61,s78,s73,s74,s75]) ).
cnf(s80,plain,
~ spl8_53,
inference(rat,[],[s70,s74,s79]) ).
cnf(s81,plain,
$false,
inference(rat,[],[s62,s75,s74,s78,s73,s80,s79]) ).
tff(f841,plain,
$false,
inference(avatar_sat_refutation,[],[s81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW678_1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.28 % Computer : n018.cluster.edu
% 0.24/0.28 % Model : x86_64 x86_64
% 0.24/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.28 % Memory : 8046.5625MB
% 0.24/0.28 % OS : Linux 6.8.0-71-generic
% 0.24/0.28 % CPULimit : 300
% 0.24/0.28 % WCLimit : 300
% 0.24/0.28 % DateTime : Mon Sep 28 14:27:10 UTC 2026
% 0.24/0.28 % CPUTime :
% 0.24/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.33 Running first-order theorem proving
% 0.24/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.91/1.41 % (3426830)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.91/1.41 % (3426843)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=854449224:i=33:rtra=on_3000 on theBenchmark for (3000ds/33Mi)
% 3.91/1.41 % (3426841)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1551734377:i=4:rtra=on_3000 on theBenchmark for (3000ds/4Mi)
% 3.91/1.41 % (3426837)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1143329151:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_3000 on theBenchmark for (3000ds/12Mi)
% 3.91/1.41 % (3426842)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3703127262:i=46:rtra=on_3000 on theBenchmark for (3000ds/46Mi)
% 3.91/1.41 % (3426839)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=125951030:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_3000 on theBenchmark for (3000ds/201Mi)
% 3.91/1.41 % (3426840)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1739298626:s2a=on:i=7:rtra=on:inst=on_3000 on theBenchmark for (3000ds/7Mi)
% 3.91/1.41 % (3426838)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2095618405:i=307:kws=precedence:nm=0:rtra=on_3000 on theBenchmark for (3000ds/307Mi)
% 3.91/1.41 % (3426841)Instruction limit reached!
% 3.91/1.41 % (3426841)------------------------------
% 3.91/1.41 % (3426841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426841)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426841)Termination reason: Instruction limit
% 3.91/1.41 % (3426841)Termination phase: Saturation
% 3.91/1.41 % (3426841)Time elapsed: 0.006 s
% 3.91/1.41 % (3426841)Peak memory usage: 89 MB
% 3.91/1.41 % (3426841)Instructions burned: 4 (million)
% 3.91/1.41 % (3426840)Instruction limit reached!
% 3.91/1.41 % (3426840)------------------------------
% 3.91/1.41 % (3426840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426840)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426840)Termination reason: Instruction limit
% 3.91/1.41 % (3426840)Termination phase: Saturation
% 3.91/1.41 % (3426840)Time elapsed: 0.010 s
% 3.91/1.41 % (3426840)Peak memory usage: 88 MB
% 3.91/1.41 % (3426840)Instructions burned: 7 (million)
% 3.91/1.41 % (3426843)Instruction limit reached!
% 3.91/1.41 % (3426843)------------------------------
% 3.91/1.41 % (3426843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426843)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426843)Termination reason: Instruction limit
% 3.91/1.41 % (3426843)Termination phase: Saturation
% 3.91/1.41 % (3426843)Time elapsed: 0.043 s
% 3.91/1.41 % (3426843)Peak memory usage: 116 MB
% 3.91/1.41 % (3426843)Instructions burned: 33 (million)
% 3.91/1.41 % (3426837)Instruction limit reached!
% 3.91/1.41 % (3426837)------------------------------
% 3.91/1.41 % (3426837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426837)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426837)Termination reason: Instruction limit
% 3.91/1.41 % (3426837)Termination phase: Saturation
% 3.91/1.41 % (3426837)Time elapsed: 0.043 s
% 3.91/1.41 % (3426837)Peak memory usage: 115 MB
% 3.91/1.41 % (3426837)Instructions burned: 12 (million)
% 3.91/1.41 % (3426839)First to succeed.
% 3.91/1.41 % (3426839)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3426830"
% 3.91/1.41 % (3426842)Instruction limit reached!
% 3.91/1.41 % (3426842)------------------------------
% 3.91/1.41 % (3426842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426842)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426842)Termination reason: Instruction limit
% 3.91/1.41 % (3426842)Termination phase: Saturation
% 3.91/1.41 % (3426842)Time elapsed: 0.085 s
% 3.91/1.41 % (3426842)Peak memory usage: 115 MB
% 3.91/1.41 % (3426842)Instructions burned: 46 (million)
% 3.91/1.41 % (3426852)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2966578413:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 3.91/1.41 % (3426851)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4158646815:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.91/1.41 % (3426852)Also succeeded, but the first one will report.
% 3.91/1.41 % (3426851)Instruction limit reached!
% 3.91/1.41 % (3426851)------------------------------
% 3.91/1.41 % (3426851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426851)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426851)Termination reason: Instruction limit
% 3.91/1.41 % (3426851)Termination phase: Saturation
% 3.91/1.41 % (3426851)Time elapsed: 0.018 s
% 3.91/1.41 % (3426851)Peak memory usage: 89 MB
% 3.91/1.41 % (3426851)Instructions burned: 14 (million)
% 3.91/1.41 % (3426853)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=797125028:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.91/1.41 % (3426853)Instruction limit reached!
% 3.91/1.41 % (3426853)------------------------------
% 3.91/1.41 % (3426853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426853)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426853)Termination reason: Instruction limit
% 3.91/1.41 % (3426853)Termination phase: Saturation
% 3.91/1.41 % (3426853)Time elapsed: 0.019 s
% 3.91/1.41 % (3426853)Peak memory usage: 90 MB
% 3.91/1.41 % (3426853)Instructions burned: 16 (million)
% 3.91/1.41 % (3426854)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2148842563:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.91/1.41 % (3426855)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=2886781626:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 3.91/1.41 % (3426854)Also succeeded, but the first one will report.
% 3.91/1.41 % (3426838)Instruction limit reached!
% 3.91/1.41 % (3426838)------------------------------
% 3.91/1.41 % (3426838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426838)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426838)Termination reason: Instruction limit
% 3.91/1.41 % (3426838)Termination phase: Saturation
% 3.91/1.41 % (3426838)Time elapsed: 0.365 s
% 3.91/1.41 % (3426838)Peak memory usage: 117 MB
% 3.91/1.41 % (3426838)Instructions burned: 307 (million)
% 3.91/1.41 % (3426855)Refutation not found, incomplete strategy
% 3.91/1.41 % (3426855)------------------------------
% 3.91/1.41 % (3426855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.41 % (3426855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.41 % (3426855)CaDiCaL version: 2.1.3
% 3.91/1.41 % (3426855)Termination reason: Refutation not found, incomplete strategy
% 3.91/1.41 % (3426855)Time elapsed: 0.005 s
% 3.91/1.41 % (3426855)Peak memory usage: 89 MB
% 3.91/1.41 % (3426855)Instructions burned: 2 (million)
% 3.91/1.41 % (3426839)Refutation found. Thanks to Tanya!
% 3.91/1.41 % SZS status Theorem for theBenchmark
% 3.91/1.41 % SZS output start Proof for theBenchmark
% See solution above
% 5.82/1.66 % (3426839)------------------------------
% 5.82/1.66 % (3426839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.66 % (3426839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.66 % (3426839)CaDiCaL version: 2.1.3
% 5.82/1.66 % (3426839)Termination reason: Refutation
% 5.82/1.66 % (3426839)Time elapsed: 0.078 s
% 5.82/1.66 % (3426839)Peak memory usage: 114 MB
% 5.82/1.66 % (3426839)Instructions burned: 38 (million)
% 5.82/1.66 % (3426839)------------------------------
% 5.82/1.66 % (3426839)------------------------------
% 5.82/1.66 % (3426830)Success in time 0.737 s
% 5.82/1.66 % Vampire exiting
%------------------------------------------------------------------------------