%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV471^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:38:42 AM UTC 2026
% Result : Theorem 5.10s 1.08s
% Output : Refutation 5.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 15
% Syntax : Number of formulae : 254 ( 8 unt; 0 typ; 14 def)
% Number of atoms : 2164 ( 504 equ; 0 cnn)
% Maximal formula atoms : 7 ( 8 avg)
% Number of connectives : 3629 ( 338 ~; 496 |; 148 &;2281 @)
% ( 14 <=>; 177 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 89 ( 89 >; 0 *; 0 +; 0 <<)
% Number of symbols : 53 ( 48 usr; 21 con; 0-6 aty)
% ( 140 !!; 35 ??; 0 @@+; 0 @@-)
% Number of variables : 335 ( 0 sgn 123 !; 16 ?; 335 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_6,type,
sK0: $tType ).
thf(type_def_7,type,
sK1: $tType ).
thf(func_def_0,type,
'const/trivia/I':
!>[X0: $tType] : ( X0 > X0 ) ).
thf(func_def_1,type,
'const/sets/IN':
!>[X0: $tType] : ( X0 > ( X0 > $o ) > $o ) ).
thf(func_def_3,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_4,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_5,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_6,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_9,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_10,type,
vAND: $o > $o > $o ).
thf(func_def_11,type,
vIMP: $o > $o > $o ).
thf(func_def_12,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_15,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_16,type,
sK2: sK0 > $o ).
thf(func_def_17,type,
sK3: sK1 > $o ).
thf(func_def_18,type,
sK4: sK0 > sK1 ).
thf(func_def_19,type,
vNOT: $o > $o ).
thf(func_def_21,type,
sK6: sK1 ).
thf(func_def_22,type,
sK7: sK1 > sK0 ).
thf(func_def_23,type,
sK8: sK1 > sK0 ).
thf(func_def_24,type,
sK9: sK0 ).
thf(func_def_25,type,
sK10: sK0 ).
thf(func_def_26,type,
sK11: ( sK1 > sK0 ) > sK1 ).
thf(func_def_27,type,
sK12: ( sK1 > sK0 ) > sK0 ).
thf(func_def_28,type,
sK13:
!>[X0: $tType,X1: $tType] : ( ( X0 > $o ) > ( X1 > X0 ) > ( X0 > X1 ) > X0 ) ).
thf(func_def_29,type,
sK14:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > X0 ) ).
thf(func_def_30,type,
sK15:
!>[X0: $tType,X1: $tType] : ( ( X1 > X0 ) > ( X0 > X1 ) > ( X0 > $o ) > ( X1 > $o ) > X1 ) ).
thf(func_def_31,type,
sK16:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > ( X1 > $o ) > X1 > X0 ) ).
thf(func_def_32,type,
sK17:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > X0 ) ).
thf(func_def_33,type,
sK18:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > X1 > X0 ) ).
thf(func_def_34,type,
sK19:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > X1 > X0 ) ).
thf(func_def_35,type,
sK20:
!>[X0: $tType,X1: $tType] : ( ( X0 > X1 ) > ( X0 > $o ) > ( X1 > $o ) > X1 ) ).
thf(func_def_36,type,
sK21: ( sK1 > sK0 ) > sK1 ).
thf(f4,conjecture,
! [X0: $tType,X1: $tType,X2: X1 > X0,X4: X0 > $o,X3: X1 > $o] :
( ! [X5: X1] :
( ( 'const/sets/IN' @ X1 @ X5 @ X3 )
=> ( 'const/sets/IN' @ X0 @ ( X2 @ X5 ) @ X4 ) )
=> ( ? [X5: X0 > X1] :
( ( ! [X6: X1] :
( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
=> ( ( X5 @ ( X2 @ X6 ) )
= X6 ) )
& ! [X6: X0] :
( ( 'const/sets/IN' @ X0 @ X6 @ X4 )
=> ( 'const/sets/IN' @ X1 @ ( X5 @ X6 ) @ X3 ) )
& ! [X6: X0] :
( ( 'const/sets/IN' @ X0 @ X6 @ X4 )
=> ( ( X2 @ ( X5 @ X6 ) )
= X6 ) ) )
= ( ! [X6: X1,X5: X1] :
( ( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
& ( 'const/sets/IN' @ X1 @ X5 @ X3 )
& ( ( X2 @ X5 )
= ( X2 @ X6 ) ) )
=> ( X5 = X6 ) ) ) )
& ! [X5: X0] :
( ( 'const/sets/IN' @ X0 @ X5 @ X4 )
=> ? [X6: X1] :
( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
& ( ( X2 @ X6 )
= X5 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/BIJECTIVE_ON_LEFT_RIGHT_INVERSE_') ).
thf(f5,negated_conjecture,
~ ! [X0: $tType,X1: $tType,X2: X1 > X0,X4: X0 > $o,X3: X1 > $o] :
( ! [X5: X1] :
( ( 'const/sets/IN' @ X1 @ X5 @ X3 )
=> ( 'const/sets/IN' @ X0 @ ( X2 @ X5 ) @ X4 ) )
=> ( ? [X5: X0 > X1] :
( ( ! [X6: X1] :
( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
=> ( ( X5 @ ( X2 @ X6 ) )
= X6 ) )
& ! [X6: X0] :
( ( 'const/sets/IN' @ X0 @ X6 @ X4 )
=> ( 'const/sets/IN' @ X1 @ ( X5 @ X6 ) @ X3 ) )
& ! [X6: X0] :
( ( 'const/sets/IN' @ X0 @ X6 @ X4 )
=> ( ( X2 @ ( X5 @ X6 ) )
= X6 ) ) )
= ( ! [X6: X1,X5: X1] :
( ( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
& ( 'const/sets/IN' @ X1 @ X5 @ X3 )
& ( ( X2 @ X5 )
= ( X2 @ X6 ) ) )
=> ( X5 = X6 ) ) ) )
& ! [X5: X0] :
( ( 'const/sets/IN' @ X0 @ X5 @ X4 )
=> ? [X6: X1] :
( ( 'const/sets/IN' @ X1 @ X6 @ X3 )
& ( ( X2 @ X6 )
= X5 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
thf(f7,plain,
~ ! [X0: $tType,X1: $tType,X2: X1 > X0,X3: X0 > $o,X4: X1 > $o] :
( ! [X5: X1] :
( ( 'const/sets/IN' @ X1 @ X5 @ X4 )
=> ( 'const/sets/IN' @ X0 @ ( X2 @ X5 ) @ X3 ) )
=> ( ? [X6: X0 > X1] :
( ( ! [X7: X1] :
( ( 'const/sets/IN' @ X1 @ X7 @ X4 )
=> ( ( X6 @ ( X2 @ X7 ) )
= X7 ) )
& ! [X8: X0] :
( ( 'const/sets/IN' @ X0 @ X8 @ X3 )
=> ( 'const/sets/IN' @ X1 @ ( X6 @ X8 ) @ X4 ) )
& ! [X9: X0] :
( ( 'const/sets/IN' @ X0 @ X9 @ X3 )
=> ( ( X2 @ ( X6 @ X9 ) )
= X9 ) ) )
= ( ! [X10: X1,X11: X1] :
( ( ( 'const/sets/IN' @ X1 @ X10 @ X4 )
& ( 'const/sets/IN' @ X1 @ X11 @ X4 )
& ( ( X2 @ X10 )
= ( X2 @ X11 ) ) )
=> ( X10 = X11 ) ) ) )
& ! [X12: X0] :
( ( 'const/sets/IN' @ X0 @ X12 @ X3 )
=> ? [X13: X1] :
( ( 'const/sets/IN' @ X1 @ X13 @ X4 )
& ( ( X2 @ X13 )
= X12 ) ) ) ) ),
inference(rectify,[],[f5]) ).
thf(f8,plain,
~ ! [X1: $tType,X0: $tType,X3: X0 > $o,X2: X1 > X0,X4: X1 > $o] :
( ! [X5: X1] :
( ( ( 'const/sets/IN' @ X1 @ X5 @ X4 )
= $true )
=> ( $true
= ( 'const/sets/IN' @ X0 @ ( X2 @ X5 ) @ X3 ) ) )
=> ( ( ?? @ ( X0 > X1 )
@ ^ [Y0: X0 > X1] :
( ( !! @ X0
@ ^ [Y1: X0] :
( ( 'const/sets/IN' @ X0 @ Y1 @ X3 )
=> ( ( X2 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( ( 'const/sets/IN' @ X0 @ Y1 @ X3 )
=> ( 'const/sets/IN' @ X1 @ ( Y0 @ Y1 ) @ X4 ) ) )
& ( !! @ X1
@ ^ [Y1: X1] :
( ( 'const/sets/IN' @ X1 @ Y1 @ X4 )
=> ( ( Y0 @ ( X2 @ Y1 ) )
= Y1 ) ) ) ) )
= ( ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X3 )
=> ( ?? @ X1
@ ^ [Y1: X1] :
( ( ( X2 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ X1 @ Y1 @ X4 ) ) ) ) )
& ( !! @ X1
@ ^ [Y0: X1] :
( !! @ X1
@ ^ [Y1: X1] :
( ( ( ( X2 @ Y1 )
= ( X2 @ Y0 ) )
& ( 'const/sets/IN' @ X1 @ Y0 @ X4 )
& ( 'const/sets/IN' @ X1 @ Y1 @ X4 ) )
=> ( Y1 = Y0 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f7]) ).
thf(f16,plain,
? [X1: $tType,X0: $tType,X4: X1 > $o,X3: X0 > $o,X2: X1 > X0] :
( ( ( ?? @ ( X0 > X1 )
@ ^ [Y0: X0 > X1] :
( ( !! @ X0
@ ^ [Y1: X0] :
( ( 'const/sets/IN' @ X0 @ Y1 @ X3 )
=> ( ( X2 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( ( 'const/sets/IN' @ X0 @ Y1 @ X3 )
=> ( 'const/sets/IN' @ X1 @ ( Y0 @ Y1 ) @ X4 ) ) )
& ( !! @ X1
@ ^ [Y1: X1] :
( ( 'const/sets/IN' @ X1 @ Y1 @ X4 )
=> ( ( Y0 @ ( X2 @ Y1 ) )
= Y1 ) ) ) ) )
!= ( ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X3 )
=> ( ?? @ X1
@ ^ [Y1: X1] :
( ( ( X2 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ X1 @ Y1 @ X4 ) ) ) ) )
& ( !! @ X1
@ ^ [Y0: X1] :
( !! @ X1
@ ^ [Y1: X1] :
( ( ( ( X2 @ Y1 )
= ( X2 @ Y0 ) )
& ( 'const/sets/IN' @ X1 @ Y0 @ X4 )
& ( 'const/sets/IN' @ X1 @ Y1 @ X4 ) )
=> ( Y1 = Y0 ) ) ) ) ) )
& ! [X5: X1] :
( ( $true
= ( 'const/sets/IN' @ X0 @ ( X2 @ X5 ) @ X3 ) )
| ( ( 'const/sets/IN' @ X1 @ X5 @ X4 )
!= $true ) ) ),
inference(ennf_transformation,[],[f8]) ).
thf(f18,plain,
? [X0: $tType,X1: $tType,X2: X0 > $o,X3: X1 > $o,X4: X0 > X1] :
( ( ( ( !! @ X1
@ ^ [Y0: X1] :
( ( 'const/sets/IN' @ X1 @ Y0 @ X3 )
=> ( ?? @ X0
@ ^ [Y1: X0] :
( ( ( X4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ X0 @ Y1 @ X2 ) ) ) ) )
& ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( ( X4 @ Y1 )
= ( X4 @ Y0 ) )
& ( 'const/sets/IN' @ X0 @ Y0 @ X2 )
& ( 'const/sets/IN' @ X0 @ Y1 @ X2 ) )
=> ( Y1 = Y0 ) ) ) ) )
!= ( ?? @ ( X1 > X0 )
@ ^ [Y0: X1 > X0] :
( ( !! @ X1
@ ^ [Y1: X1] :
( ( 'const/sets/IN' @ X1 @ Y1 @ X3 )
=> ( ( X4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ X1
@ ^ [Y1: X1] :
( ( 'const/sets/IN' @ X1 @ Y1 @ X3 )
=> ( 'const/sets/IN' @ X0 @ ( Y0 @ Y1 ) @ X2 ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( ( 'const/sets/IN' @ X0 @ Y1 @ X2 )
=> ( ( Y0 @ ( X4 @ Y1 ) )
= Y1 ) ) ) ) ) )
& ! [X5: X0] :
( ( $true
= ( 'const/sets/IN' @ X1 @ ( X4 @ X5 ) @ X3 ) )
| ( ( 'const/sets/IN' @ X0 @ X5 @ X2 )
!= $true ) ) ),
inference(rectify,[],[f16]) ).
thf(f19,plain,
( ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
!= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) )
& ! [X5: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK4 @ X5 ) @ sK3 ) )
| ( $true
!= ( 'const/sets/IN' @ sK0 @ X5 @ sK2 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f18]) ).
thf(f22,plain,
! [X5: sK0] :
( ( $true
!= ( 'const/sets/IN' @ sK0 @ X5 @ sK2 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK4 @ X5 ) @ sK3 ) ) ),
inference(cnf_transformation,[],[f19]) ).
thf(f23,plain,
( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
!= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) ),
inference(cnf_transformation,[],[f19]) ).
thf(f27,plain,
( ( $true
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) )
| ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
= $true ) ),
inference(xor_proxy_clausification,[],[f23]) ).
thf(f28,plain,
( ( $false
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) )
| ( $false
= ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) ) ) ),
inference(xor_proxy_clausification,[],[f23]) ).
thf(f29,plain,
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) )
| ( $false
= ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f28]) ).
thf(f30,plain,
( ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
= $true )
| ( $true
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f27]) ).
thf(f31,plain,
( ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
= $true )
| ( $true
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f27]) ).
thf(f33,definition,
( spl5_1
<=> ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
thf(f34,plain,
( ( $false
!= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) )
| spl5_1 ),
inference(avatar_component_clause,[],[f33]) ).
thf(f35,plain,
( ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) )
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f33]) ).
thf(f37,definition,
( spl5_2
<=> ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
thf(f38,plain,
( ( $false
!= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) )
| spl5_2 ),
inference(avatar_component_clause,[],[f37]) ).
thf(f39,plain,
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) )
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f37]) ).
thf(f41,definition,
( spl5_3
<=> ( $false
= ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
thf(f42,plain,
( ( $false
!= ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) ) )
| spl5_3 ),
inference(avatar_component_clause,[],[f41]) ).
thf(f43,plain,
( ( $false
= ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) ) )
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f41]) ).
thf(f44,plain,
( spl5_1
| spl5_2
| spl5_3 ),
inference(avatar_split_clause,[],[f29,f41,f37,f33]) ).
thf(f46,definition,
( spl5_4
<=> ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
thf(f48,plain,
( ( ( ?? @ ( sK1 > sK0 )
@ ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) ) )
= $true )
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f46]) ).
thf(f50,definition,
( spl5_5
<=> ( $true
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
thf(f52,plain,
( ( $true
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) ) ) )
| ~ spl5_5 ),
inference(avatar_component_clause,[],[f50]) ).
thf(f53,plain,
( spl5_4
| spl5_5 ),
inference(avatar_split_clause,[],[f31,f50,f46]) ).
thf(f55,definition,
( spl5_6
<=> ( $true
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).
thf(f57,plain,
( ( $true
= ( !! @ sK0
@ ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) ) ) )
| ~ spl5_6 ),
inference(avatar_component_clause,[],[f55]) ).
thf(f58,plain,
( spl5_6
| spl5_4 ),
inference(avatar_split_clause,[],[f30,f46,f55]) ).
thf(f59,plain,
( ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) )
@ sK6 ) )
| ~ spl5_2 ),
inference(sigma_proxy_clausification,[],[f39]) ).
thf(f60,plain,
( ( $false
= ( ( 'const/sets/IN' @ sK1 @ sK6 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= sK6 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) ) ) ) )
| ~ spl5_2 ),
inference(beta-eta_normalization,[],[f59]) ).
thf(f61,plain,
( ( $false
= ( ?? @ sK0
@ ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= sK6 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) ) ) )
| ~ spl5_2 ),
inference(imp_proxy_clausification,[],[f60]) ).
thf(f62,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ sK6 @ sK3 ) )
| ~ spl5_2 ),
inference(imp_proxy_clausification,[],[f60]) ).
thf(f63,plain,
( ! [X1: sK0] :
( $false
= ( ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= sK6 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
@ X1 ) )
| ~ spl5_2 ),
inference(pi_proxy_clausification,[],[f61]) ).
thf(f64,plain,
( ! [X1: sK0] :
( $false
= ( ( ( sK4 @ X1 )
= sK6 )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) ) )
| ~ spl5_2 ),
inference(beta-eta_normalization,[],[f63]) ).
thf(f65,plain,
( ! [X1: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) )
| ( $false
= ( ( sK4 @ X1 )
= sK6 ) ) )
| ~ spl5_2 ),
inference(and_proxy_clausification,[],[f64]) ).
thf(f66,plain,
( ! [X1: sK0] :
( ( ( sK4 @ X1 )
!= sK6 )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) ) )
| ~ spl5_2 ),
inference(equality_proxy_clausification,[],[f65]) ).
thf(f86,plain,
( ( $true
= ( ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) )
@ sK7 ) )
| ~ spl5_4 ),
inference(sigma_proxy_clausification,[],[f48]) ).
thf(f87,plain,
( ( $true
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( sK7 @ Y0 ) )
= Y0 ) ) )
& ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ Y0 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( sK7 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| ~ spl5_4 ),
inference(beta-eta_normalization,[],[f86]) ).
thf(f89,plain,
( ( ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( sK7 @ Y0 ) )
= Y0 ) ) )
& ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ Y0 ) @ sK2 ) ) ) )
= $true )
| ~ spl5_4 ),
inference(and_proxy_clausification,[],[f87]) ).
thf(f90,plain,
( ( $true
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ Y0 ) @ sK2 ) ) ) )
| ~ spl5_4 ),
inference(and_proxy_clausification,[],[f89]) ).
thf(f91,plain,
( ( $true
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( sK7 @ Y0 ) )
= Y0 ) ) ) )
| ~ spl5_4 ),
inference(and_proxy_clausification,[],[f89]) ).
thf(f106,plain,
( ! [X1: sK1] :
( $true
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ Y0 ) @ sK2 ) )
@ X1 ) )
| ~ spl5_4 ),
inference(pi_proxy_clausification,[],[f90]) ).
thf(f107,plain,
( ! [X1: sK1] :
( $true
= ( ( 'const/sets/IN' @ sK1 @ X1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ X1 ) @ sK2 ) ) )
| ~ spl5_4 ),
inference(beta-eta_normalization,[],[f106]) ).
thf(f108,plain,
( ! [X1: sK1] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ ( sK7 @ X1 ) @ sK2 ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) ) )
| ~ spl5_4 ),
inference(imp_proxy_clausification,[],[f107]) ).
thf(f117,plain,
( ! [X1: sK1] :
( $true
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( sK7 @ Y0 ) )
= Y0 ) )
@ X1 ) )
| ~ spl5_4 ),
inference(pi_proxy_clausification,[],[f91]) ).
thf(f118,plain,
( ! [X1: sK1] :
( $true
= ( ( 'const/sets/IN' @ sK1 @ X1 @ sK3 )
=> ( ( sK4 @ ( sK7 @ X1 ) )
= X1 ) ) )
| ~ spl5_4 ),
inference(beta-eta_normalization,[],[f117]) ).
thf(f119,plain,
( ! [X1: sK1] :
( ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) )
| ( $true
= ( ( sK4 @ ( sK7 @ X1 ) )
= X1 ) ) )
| ~ spl5_4 ),
inference(imp_proxy_clausification,[],[f118]) ).
thf(f120,plain,
( ! [X1: sK1] :
( ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) )
| ( ( sK4 @ ( sK7 @ X1 ) )
= X1 ) )
| ~ spl5_4 ),
inference(equality_proxy_clausification,[],[f119]) ).
thf(f123,plain,
( ( $false = $true )
| ( ( sK4 @ ( sK7 @ sK6 ) )
= sK6 )
| ~ spl5_2
| ~ spl5_4 ),
inference(superposition,[],[f120,f62]) ).
thf(f130,plain,
( ( ( sK4 @ ( sK7 @ sK6 ) )
= sK6 )
| ~ spl5_2
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f123]) ).
thf(f133,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK7 @ sK6 ) @ sK2 ) )
| ( sK6 != sK6 )
| ~ spl5_2
| ~ spl5_4 ),
inference(superposition,[],[f66,f130]) ).
thf(f135,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK7 @ sK6 ) @ sK2 ) )
| ~ spl5_2
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f133]) ).
thf(f148,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ sK6 @ sK3 ) )
| ( $false = $true )
| ~ spl5_2
| ~ spl5_4 ),
inference(superposition,[],[f108,f135]) ).
thf(f150,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ sK6 @ sK3 ) )
| ~ spl5_2
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f148]) ).
thf(f155,plain,
( ( $false = $true )
| ~ spl5_2
| ~ spl5_4 ),
inference(superposition,[],[f62,f150]) ).
thf(f158,plain,
( $false
| ~ spl5_2
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f155]) ).
thf(f159,plain,
( ~ spl5_2
| ~ spl5_4 ),
inference(avatar_contradiction_clause,[],[f158]) ).
thf(f161,plain,
( ( $false = $true )
| ~ spl5_2
| ~ spl5_5 ),
inference(forward_demodulation,[],[f52,f39]) ).
thf(f162,plain,
( $false
| ~ spl5_2
| ~ spl5_5 ),
inference(trivial_inequality_removal,[],[f161]) ).
thf(f163,plain,
( ~ spl5_2
| ~ spl5_5 ),
inference(avatar_contradiction_clause,[],[f162]) ).
thf(f197,plain,
( ! [X1: sK1] :
( $true
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y1: sK0] :
( ( ( sK4 @ Y1 )
= Y0 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) ) ) )
@ X1 ) )
| spl5_2 ),
inference(pi_proxy_clausification,[],[f38]) ).
thf(f199,plain,
( ! [X1: sK1] :
( $true
= ( ( 'const/sets/IN' @ sK1 @ X1 @ sK3 )
=> ( ?? @ sK0
@ ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= X1 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) ) ) ) )
| spl5_2 ),
inference(beta-eta_normalization,[],[f197]) ).
thf(f200,plain,
( ! [X1: sK1] :
( ( $true
= ( ?? @ sK0
@ ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= X1 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) ) ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) ) )
| spl5_2 ),
inference(imp_proxy_clausification,[],[f199]) ).
thf(f201,plain,
( ! [X1: sK1] :
( ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) )
| ( ( ^ [Y0: sK0] :
( ( ( sK4 @ Y0 )
= X1 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
@ ( sK8 @ X1 ) )
= $true ) )
| spl5_2 ),
inference(sigma_proxy_clausification,[],[f200]) ).
thf(f202,plain,
( ! [X1: sK1] :
( ( $true
= ( ( ( sK4 @ ( sK8 @ X1 ) )
= X1 )
& ( 'const/sets/IN' @ sK0 @ ( sK8 @ X1 ) @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) ) )
| spl5_2 ),
inference(beta-eta_normalization,[],[f201]) ).
thf(f203,plain,
( ! [X1: sK1] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ X1 ) @ sK2 ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) ) )
| spl5_2 ),
inference(and_proxy_clausification,[],[f202]) ).
thf(f204,plain,
( ! [X1: sK1] :
( ( $true
= ( ( sK4 @ ( sK8 @ X1 ) )
= X1 ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) ) )
| spl5_2 ),
inference(and_proxy_clausification,[],[f202]) ).
thf(f205,plain,
( ! [X1: sK1] :
( ( $false
= ( 'const/sets/IN' @ sK1 @ X1 @ sK3 ) )
| ( ( sK4 @ ( sK8 @ X1 ) )
= X1 ) )
| spl5_2 ),
inference(equality_proxy_clausification,[],[f204]) ).
thf(f206,plain,
( ( $false
= ( ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) )
@ sK9 ) )
| ~ spl5_1 ),
inference(sigma_proxy_clausification,[],[f35]) ).
thf(f209,plain,
( ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( ( ( sK4 @ Y0 )
= ( sK4 @ sK9 ) )
& ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
=> ( Y0 = sK9 ) ) ) )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f206]) ).
thf(f210,plain,
( ( $false
= ( ^ [Y0: sK0] :
( ( ( ( sK4 @ Y0 )
= ( sK4 @ sK9 ) )
& ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
=> ( Y0 = sK9 ) )
@ sK10 ) )
| ~ spl5_1 ),
inference(sigma_proxy_clausification,[],[f209]) ).
thf(f212,plain,
( ( $false
= ( ( ( ( sK4 @ sK10 )
= ( sK4 @ sK9 ) )
& ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ sK10 @ sK2 ) )
=> ( sK10 = sK9 ) ) )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f210]) ).
thf(f214,plain,
( ( $false
= ( sK10 = sK9 ) )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f212]) ).
thf(f215,plain,
( ( ( ( ( sK4 @ sK10 )
= ( sK4 @ sK9 ) )
& ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ sK10 @ sK2 ) )
= $true )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f212]) ).
thf(f216,plain,
( ( sK10 != sK9 )
| ~ spl5_1 ),
inference(equality_proxy_clausification,[],[f214]) ).
thf(f217,plain,
( ( $true
= ( 'const/sets/IN' @ sK0 @ sK10 @ sK2 ) )
| ~ spl5_1 ),
inference(and_proxy_clausification,[],[f215]) ).
thf(f218,plain,
( ( $true
= ( ( ( sK4 @ sK10 )
= ( sK4 @ sK9 ) )
& ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 ) ) )
| ~ spl5_1 ),
inference(and_proxy_clausification,[],[f215]) ).
thf(f219,plain,
( ( $true
= ( 'const/sets/IN' @ sK0 @ sK9 @ sK2 ) )
| ~ spl5_1 ),
inference(and_proxy_clausification,[],[f218]) ).
thf(f220,plain,
( ( ( ( sK4 @ sK10 )
= ( sK4 @ sK9 ) )
= $true )
| ~ spl5_1 ),
inference(and_proxy_clausification,[],[f218]) ).
thf(f221,plain,
( ( ( sK4 @ sK9 )
= ( sK4 @ sK10 ) )
| ~ spl5_1 ),
inference(equality_proxy_clausification,[],[f220]) ).
thf(f255,plain,
( ( $false = $true )
| ~ spl5_1
| ~ spl5_6 ),
inference(forward_demodulation,[],[f57,f35]) ).
thf(f256,plain,
( $false
| ~ spl5_1
| ~ spl5_6 ),
inference(trivial_inequality_removal,[],[f255]) ).
thf(f257,plain,
( ~ spl5_1
| ~ spl5_6 ),
inference(avatar_contradiction_clause,[],[f256]) ).
thf(f258,plain,
( ! [X1: sK0] :
( $true
= ( ^ [Y0: sK0] :
( !! @ sK0
@ ^ [Y1: sK0] :
( ( ( ( sK4 @ Y1 )
= ( sK4 @ Y0 ) )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 ) )
=> ( Y1 = Y0 ) ) )
@ X1 ) )
| spl5_1 ),
inference(pi_proxy_clausification,[],[f34]) ).
thf(f260,plain,
( ! [X1: sK0] :
( $true
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( ( ( sK4 @ Y0 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
=> ( Y0 = X1 ) ) ) )
| spl5_1 ),
inference(beta-eta_normalization,[],[f258]) ).
thf(f261,plain,
( ! [X2: sK0,X1: sK0] :
( $true
= ( ^ [Y0: sK0] :
( ( ( ( sK4 @ Y0 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 ) )
=> ( Y0 = X1 ) )
@ X2 ) )
| spl5_1 ),
inference(pi_proxy_clausification,[],[f260]) ).
thf(f262,plain,
( ! [X2: sK0,X1: sK0] :
( ( ( ( ( sK4 @ X2 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) )
=> ( X2 = X1 ) )
= $true )
| spl5_1 ),
inference(beta-eta_normalization,[],[f261]) ).
thf(f263,plain,
( ! [X2: sK0,X1: sK0] :
( ( $true
= ( X2 = X1 ) )
| ( $false
= ( ( ( sK4 @ X2 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) ) ) )
| spl5_1 ),
inference(imp_proxy_clausification,[],[f262]) ).
thf(f264,plain,
( ! [X2: sK0,X1: sK0] :
( ( $false
= ( ( ( sK4 @ X2 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
& ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) ) )
| ( X1 = X2 ) )
| spl5_1 ),
inference(equality_proxy_clausification,[],[f263]) ).
thf(f265,plain,
( ! [X2: sK0,X1: sK0] :
( ( X1 = X2 )
| ( $false
= ( ( ( sK4 @ X2 )
= ( sK4 @ X1 ) )
& ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) ) )
| spl5_1 ),
inference(and_proxy_clausification,[],[f264]) ).
thf(f266,plain,
( ! [X2: sK0,X1: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) )
| ( $false
= ( ( sK4 @ X2 )
= ( sK4 @ X1 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) )
| ( X1 = X2 ) )
| spl5_1 ),
inference(and_proxy_clausification,[],[f265]) ).
thf(f267,plain,
( ! [X2: sK0,X1: sK0] :
( ( ( sK4 @ X1 )
!= ( sK4 @ X2 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) )
| ( X1 = X2 )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X2 @ sK2 ) ) )
| spl5_1 ),
inference(equality_proxy_clausification,[],[f266]) ).
thf(f277,plain,
( ! [X1: sK1 > sK0] :
( $false
= ( ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) )
@ X1 ) )
| ~ spl5_3 ),
inference(pi_proxy_clausification,[],[f43]) ).
thf(f280,plain,
( ! [X1: sK1 > sK0] :
( $false
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( X1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f277]) ).
thf(f281,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) )
| ( $false
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( X1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) ) ) )
| ~ spl5_3 ),
inference(and_proxy_clausification,[],[f280]) ).
thf(f282,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( X1 @ Y0 ) )
= Y0 ) ) ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| ~ spl5_3 ),
inference(and_proxy_clausification,[],[f281]) ).
thf(f283,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( X1 @ Y0 ) )
= Y0 ) )
@ ( sK11 @ X1 ) ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f282]) ).
thf(f286,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) )
| ( $false
= ( ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 )
=> ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
= ( sK11 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f283]) ).
thf(f287,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
= ( sK11 @ X1 ) ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f286]) ).
thf(f288,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f286]) ).
thf(f289,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) ) )
| ~ spl5_3 ),
inference(equality_proxy_clausification,[],[f287]) ).
thf(f321,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) )
@ ( sK12 @ X1 ) ) )
| ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f289]) ).
thf(f323,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
=> ( ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) )
= ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f321]) ).
thf(f324,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $false
= ( ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) )
= ( sK12 @ X1 ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f323]) ).
thf(f325,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f323]) ).
thf(f327,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(equality_proxy_clausification,[],[f324]) ).
thf(f343,plain,
( ! [X1: sK1 > sK0] :
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( X1 @ ( sK4 @ Y0 ) )
= Y0 ) )
@ ( sK12 @ X1 ) ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f288]) ).
thf(f345,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
=> ( ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) )
= ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f343]) ).
thf(f347,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) )
= ( sK12 @ X1 ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f345]) ).
thf(f348,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f345]) ).
thf(f349,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) ) ) ) )
| ~ spl5_3 ),
inference(equality_proxy_clausification,[],[f347]) ).
thf(f364,plain,
( ( $false = $true )
| ~ spl5_3
| ~ spl5_4 ),
inference(forward_demodulation,[],[f48,f43]) ).
thf(f365,plain,
( $false
| ~ spl5_3
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f364]) ).
thf(f366,plain,
( ~ spl5_3
| ~ spl5_4 ),
inference(avatar_contradiction_clause,[],[f365]) ).
thf(f434,plain,
( ( $true
= ( ^ [Y0: sK1 > sK0] :
( ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( ( sK4 @ ( Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ sK1
@ ^ [Y1: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y1 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( Y0 @ Y1 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y1: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y1 @ sK2 )
=> ( ( Y0 @ ( sK4 @ Y1 ) )
= Y1 ) ) ) )
@ sK7 ) )
| spl5_3 ),
inference(sigma_proxy_clausification,[],[f42]) ).
thf(f436,plain,
( ( $true
= ( ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( ( sK4 @ ( sK7 @ Y0 ) )
= Y0 ) ) )
& ( !! @ sK1
@ ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( sK7 @ Y0 ) @ sK2 ) ) )
& ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( sK7 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) ) )
| spl5_3 ),
inference(beta-eta_normalization,[],[f434]) ).
thf(f437,plain,
( ( $true
= ( !! @ sK0
@ ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( sK7 @ ( sK4 @ Y0 ) )
= Y0 ) ) ) )
| spl5_3 ),
inference(and_proxy_clausification,[],[f436]) ).
thf(f448,plain,
( ! [X1: sK0] :
( ( ^ [Y0: sK0] :
( ( 'const/sets/IN' @ sK0 @ Y0 @ sK2 )
=> ( ( sK7 @ ( sK4 @ Y0 ) )
= Y0 ) )
@ X1 )
= $true )
| spl5_3 ),
inference(pi_proxy_clausification,[],[f437]) ).
thf(f449,plain,
( ! [X1: sK0] :
( ( ( 'const/sets/IN' @ sK0 @ X1 @ sK2 )
=> ( ( sK7 @ ( sK4 @ X1 ) )
= X1 ) )
= $true )
| spl5_3 ),
inference(beta-eta_normalization,[],[f448]) ).
thf(f450,plain,
( ! [X1: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) )
| ( ( ( sK7 @ ( sK4 @ X1 ) )
= X1 )
= $true ) )
| spl5_3 ),
inference(imp_proxy_clausification,[],[f449]) ).
thf(f451,plain,
( ! [X1: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X1 @ sK2 ) )
| ( ( sK7 @ ( sK4 @ X1 ) )
= X1 ) )
| spl5_3 ),
inference(equality_proxy_clausification,[],[f450]) ).
thf(f499,plain,
( ( sK10
= ( sK7 @ ( sK4 @ sK10 ) ) )
| ( $false = $true )
| ~ spl5_1
| spl5_3 ),
inference(superposition,[],[f217,f451]) ).
thf(f503,plain,
( ( sK10
= ( sK7 @ ( sK4 @ sK10 ) ) )
| ~ spl5_1
| spl5_3 ),
inference(trivial_inequality_removal,[],[f499]) ).
thf(f506,plain,
( ( sK10
= ( sK7 @ ( sK4 @ sK9 ) ) )
| ~ spl5_1
| spl5_3 ),
inference(forward_demodulation,[],[f503,f221]) ).
thf(f570,plain,
( ( sK9
= ( sK7 @ ( sK4 @ sK9 ) ) )
| ( $false = $true )
| ~ spl5_1
| spl5_3 ),
inference(superposition,[],[f451,f219]) ).
thf(f573,plain,
( ( sK9
= ( sK7 @ ( sK4 @ sK9 ) ) )
| ~ spl5_1
| spl5_3 ),
inference(trivial_inequality_removal,[],[f570]) ).
thf(f599,plain,
( ( sK10 = sK9 )
| ~ spl5_1
| spl5_3 ),
inference(superposition,[],[f506,f573]) ).
thf(f602,plain,
( $false
| ~ spl5_1
| spl5_3 ),
inference(forward_subsumption_resolution,[],[f599,f216]) ).
thf(f603,plain,
( ~ spl5_1
| spl5_3 ),
inference(avatar_contradiction_clause,[],[f602]) ).
thf(f811,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) )
@ ( sK21 @ X1 ) ) )
| ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f327]) ).
thf(f814,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) ) )
| ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f811]) ).
thf(f816,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) )
| ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f814]) ).
thf(f817,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 ) )
| ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f814]) ).
thf(f828,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true )
| ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) )
@ ( sK21 @ X1 ) ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f325]) ).
thf(f831,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f828]) ).
thf(f834,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f831]) ).
thf(f835,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK4 @ ( X1 @ ( sK11 @ X1 ) ) )
!= ( sK11 @ X1 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f831]) ).
thf(f847,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) )
@ ( sK21 @ X1 ) ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f349]) ).
thf(f851,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $false
= ( ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f847]) ).
thf(f853,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f851]) ).
thf(f854,plain,
( ! [X1: sK1 > sK0] :
( ( ( sK12 @ X1 )
!= ( X1 @ ( sK4 @ ( sK12 @ X1 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f851]) ).
thf(f897,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( ^ [Y0: sK1] :
( ( 'const/sets/IN' @ sK1 @ Y0 @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ Y0 ) @ sK2 ) )
@ ( sK21 @ X1 ) ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f348]) ).
thf(f900,plain,
( ! [X1: sK1 > sK0] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true )
| ( $false
= ( ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 )
=> ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f897]) ).
thf(f901,plain,
( ! [X1: sK1 > sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( X1 @ ( sK21 @ X1 ) ) @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f900]) ).
thf(f902,plain,
( ! [X1: sK1 > sK0] :
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ X1 ) @ sK3 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ X1 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ X1 ) @ sK2 )
= $true ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f900]) ).
thf(f1089,plain,
( ( $false = $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| spl5_2
| ~ spl5_3 ),
inference(superposition,[],[f203,f901]) ).
thf(f1093,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| spl5_2
| ~ spl5_3 ),
inference(trivial_inequality_removal,[],[f1089]) ).
thf(f1097,definition,
( spl5_16
<=> ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition]) ).
thf(f1099,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_16 ),
inference(avatar_component_clause,[],[f1097]) ).
thf(f1101,definition,
( spl5_17
<=> ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition]) ).
thf(f1103,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ~ spl5_17 ),
inference(avatar_component_clause,[],[f1101]) ).
thf(f1105,definition,
( spl5_18
<=> ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
thf(f1107,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f1105]) ).
thf(f1110,plain,
( spl5_17
| spl5_18
| spl5_16
| spl5_2
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f1093,f41,f37,f1097,f1105,f1101]) ).
thf(f1121,plain,
( ( ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 )
= $true )
| ( $true != $true )
| ~ spl5_16 ),
inference(superposition,[],[f22,f1099]) ).
thf(f1122,plain,
( ( ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 )
= $true )
| ~ spl5_16 ),
inference(trivial_inequality_removal,[],[f1121]) ).
thf(f1124,plain,
( ( $false = $true )
| ( ( sK4 @ ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
= ( sK4 @ ( sK12 @ sK8 ) ) )
| spl5_2
| ~ spl5_16 ),
inference(superposition,[],[f205,f1122]) ).
thf(f1125,plain,
( ( ( sK4 @ ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
= ( sK4 @ ( sK12 @ sK8 ) ) )
| spl5_2
| ~ spl5_16 ),
inference(trivial_inequality_removal,[],[f1124]) ).
thf(f1177,definition,
( spl5_19
<=> ! [X0: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( ( sK4 @ ( sK12 @ sK8 ) )
!= ( sK4 @ X0 ) )
| ( ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) )
= X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition]) ).
thf(f1178,plain,
( ! [X0: sK0] :
( ( ( sK4 @ ( sK12 @ sK8 ) )
!= ( sK4 @ X0 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) )
= X0 ) )
| ~ spl5_19 ),
inference(avatar_component_clause,[],[f1177]) ).
thf(f1180,definition,
( spl5_20
<=> ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) @ sK2 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition]) ).
thf(f1182,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) @ sK2 ) )
| ~ spl5_20 ),
inference(avatar_component_clause,[],[f1180]) ).
thf(f1205,definition,
( spl5_24
<=> ( ( sK11 @ sK8 )
= ( sK4 @ ( sK8 @ ( sK11 @ sK8 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition]) ).
thf(f1207,plain,
( ( ( sK11 @ sK8 )
= ( sK4 @ ( sK8 @ ( sK11 @ sK8 ) ) ) )
| ~ spl5_24 ),
inference(avatar_component_clause,[],[f1205]) ).
thf(f1277,plain,
( ( ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 )
= $true )
| ( $true != $true )
| ~ spl5_16 ),
inference(superposition,[],[f22,f1099]) ).
thf(f1278,plain,
( ( ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 )
= $true )
| ~ spl5_16 ),
inference(trivial_inequality_removal,[],[f1277]) ).
thf(f1280,plain,
( ( ( sK11 @ sK8 )
= ( sK4 @ ( sK8 @ ( sK11 @ sK8 ) ) ) )
| ( $false = $true )
| spl5_2
| ~ spl5_17 ),
inference(superposition,[],[f205,f1103]) ).
thf(f1281,plain,
( ( ( sK11 @ sK8 )
= ( sK4 @ ( sK8 @ ( sK11 @ sK8 ) ) ) )
| spl5_2
| ~ spl5_17 ),
inference(trivial_inequality_removal,[],[f1280]) ).
thf(f1283,plain,
( spl5_24
| spl5_2
| ~ spl5_17 ),
inference(avatar_split_clause,[],[f1281,f1101,f37,f1205]) ).
thf(f1361,plain,
( ! [X0: sK0] :
( ( ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) )
= X0 )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) @ sK2 ) )
| ( ( sK4 @ ( sK12 @ sK8 ) )
!= ( sK4 @ X0 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) ) )
| spl5_1
| spl5_2
| ~ spl5_16 ),
inference(superposition,[],[f267,f1125]) ).
thf(f1374,plain,
( spl5_19
| spl5_20
| spl5_1
| spl5_2
| ~ spl5_16 ),
inference(avatar_split_clause,[],[f1361,f1097,f37,f33,f1180,f1177]) ).
thf(f1680,plain,
( ( $false = $true )
| ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 ) )
| spl5_2
| ~ spl5_20 ),
inference(superposition,[],[f1182,f203]) ).
thf(f1684,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK4 @ ( sK12 @ sK8 ) ) @ sK3 ) )
| spl5_2
| ~ spl5_20 ),
inference(trivial_inequality_removal,[],[f1680]) ).
thf(f1728,plain,
( ( $false = $true )
| spl5_2
| ~ spl5_16
| ~ spl5_20 ),
inference(superposition,[],[f1684,f1278]) ).
thf(f1739,plain,
( $false
| spl5_2
| ~ spl5_16
| ~ spl5_20 ),
inference(trivial_inequality_removal,[],[f1728]) ).
thf(f1740,plain,
( spl5_2
| ~ spl5_16
| ~ spl5_20 ),
inference(avatar_contradiction_clause,[],[f1739]) ).
thf(f1797,plain,
( ( ( sK12 @ sK8 )
= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 ) )
| ~ spl5_19 ),
inference(equality_resolution,[],[f1178]) ).
thf(f1799,plain,
( ( $false = $true )
| ( ( sK12 @ sK8 )
= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ~ spl5_16
| ~ spl5_19 ),
inference(forward_demodulation,[],[f1797,f1099]) ).
thf(f1800,plain,
( ( ( sK12 @ sK8 )
= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ~ spl5_16
| ~ spl5_19 ),
inference(trivial_inequality_removal,[],[f1799]) ).
thf(f1876,plain,
( ( ( sK12 @ sK8 )
!= ( sK12 @ sK8 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(superposition,[],[f853,f1800]) ).
thf(f1877,plain,
( ( ( sK12 @ sK8 )
!= ( sK12 @ sK8 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(superposition,[],[f854,f1800]) ).
thf(f1879,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(trivial_inequality_removal,[],[f1877]) ).
thf(f1882,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(trivial_inequality_removal,[],[f1876]) ).
thf(f1900,definition,
( spl5_26
<=> ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_26])],[avatar_definition]) ).
thf(f1902,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_26 ),
inference(avatar_component_clause,[],[f1900]) ).
thf(f1903,plain,
( spl5_17
| spl5_26
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(avatar_split_clause,[],[f1879,f1177,f1097,f41,f1900,f1101]) ).
thf(f1905,definition,
( spl5_27
<=> ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_27])],[avatar_definition]) ).
thf(f1907,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ~ spl5_27 ),
inference(avatar_component_clause,[],[f1905]) ).
thf(f1908,plain,
( spl5_27
| spl5_17
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19 ),
inference(avatar_split_clause,[],[f1882,f1177,f1097,f41,f1101,f1905]) ).
thf(f1981,plain,
( ( ( sK12 @ sK8 )
!= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ( ( sK11 @ sK8 )
!= ( sK11 @ sK8 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(superposition,[],[f816,f1207]) ).
thf(f1982,plain,
( ( ( sK12 @ sK8 )
!= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ( ( sK11 @ sK8 )
!= ( sK11 @ sK8 ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(superposition,[],[f817,f1207]) ).
thf(f1984,plain,
( ( ( sK11 @ sK8 )
!= ( sK11 @ sK8 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_3
| ~ spl5_24 ),
inference(superposition,[],[f834,f1207]) ).
thf(f1985,plain,
( ( ( sK11 @ sK8 )
!= ( sK11 @ sK8 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(superposition,[],[f835,f1207]) ).
thf(f2000,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_3
| ~ spl5_24 ),
inference(trivial_inequality_removal,[],[f1984]) ).
thf(f2002,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ( ( sK12 @ sK8 )
!= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(trivial_inequality_removal,[],[f1981]) ).
thf(f2008,plain,
( ( ( sK12 @ sK8 )
!= ( sK8 @ ( sK4 @ ( sK12 @ sK8 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(trivial_inequality_removal,[],[f1982]) ).
thf(f2011,plain,
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK8 @ ( sK21 @ sK8 ) ) @ sK2 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24 ),
inference(forward_subsumption_resolution,[],[f2002,f1800]) ).
thf(f2047,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24 ),
inference(forward_subsumption_resolution,[],[f2008,f1800]) ).
thf(f2051,plain,
( spl5_27
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24 ),
inference(avatar_split_clause,[],[f2011,f1205,f1177,f1097,f41,f1905]) ).
thf(f2062,plain,
( spl5_26
| ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24 ),
inference(avatar_split_clause,[],[f2047,f1205,f1177,f1097,f41,f1900]) ).
thf(f2301,plain,
( ( $false = $true )
| ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| spl5_2
| ~ spl5_27 ),
inference(superposition,[],[f1907,f203]) ).
thf(f2306,plain,
( ( $false
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| spl5_2
| ~ spl5_27 ),
inference(trivial_inequality_removal,[],[f2301]) ).
thf(f2308,plain,
( spl5_18
| spl5_2
| ~ spl5_27 ),
inference(avatar_split_clause,[],[f2306,f1905,f37,f1105]) ).
thf(f2309,plain,
( ( $false = $true )
| ~ spl5_18
| ~ spl5_26 ),
inference(superposition,[],[f1107,f1902]) ).
thf(f2310,plain,
( ( $false = $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_3
| ~ spl5_18 ),
inference(superposition,[],[f1107,f902]) ).
thf(f2312,plain,
( ( $false = $true )
| ~ spl5_18
| ~ spl5_26 ),
inference(superposition,[],[f1902,f1107]) ).
thf(f2314,plain,
( $false
| ~ spl5_18
| ~ spl5_26 ),
inference(trivial_inequality_removal,[],[f2312]) ).
thf(f2315,plain,
( ~ spl5_18
| ~ spl5_26 ),
inference(avatar_contradiction_clause,[],[f2314]) ).
thf(f2316,plain,
( ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK11 @ sK8 ) @ sK3 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_3
| ~ spl5_18 ),
inference(trivial_inequality_removal,[],[f2310]) ).
thf(f2318,plain,
( $false
| ~ spl5_18
| ~ spl5_26 ),
inference(trivial_inequality_removal,[],[f2309]) ).
thf(f2319,plain,
( ~ spl5_18
| ~ spl5_26 ),
inference(avatar_contradiction_clause,[],[f2318]) ).
thf(f2336,plain,
( spl5_16
| spl5_17
| ~ spl5_3
| ~ spl5_18 ),
inference(avatar_split_clause,[],[f2316,f1105,f41,f1101,f1097]) ).
thf(f2342,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK1 @ ( sK21 @ sK8 ) @ sK3 ) )
| ~ spl5_3
| ~ spl5_24 ),
inference(trivial_inequality_removal,[],[f1985]) ).
thf(f2360,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ( $false = $true )
| ~ spl5_3
| ~ spl5_18
| ~ spl5_24 ),
inference(forward_demodulation,[],[f2342,f1107]) ).
thf(f2361,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK12 @ sK8 ) @ sK2 )
= $true )
| ~ spl5_3
| ~ spl5_18
| ~ spl5_24 ),
inference(trivial_inequality_removal,[],[f2360]) ).
thf(f2380,plain,
( spl5_16
| ~ spl5_3
| ~ spl5_18
| ~ spl5_24 ),
inference(avatar_split_clause,[],[f2361,f1205,f1105,f41,f1097]) ).
thf(f2389,plain,
( spl5_27
| spl5_16
| ~ spl5_3
| ~ spl5_24 ),
inference(avatar_split_clause,[],[f2000,f1205,f41,f1097,f1905]) ).
cnf(s1,plain,
( spl5_1
| spl5_2
| spl5_3 ),
inference(sat_conversion,[],[f44]) ).
cnf(s2,plain,
( spl5_4
| spl5_5 ),
inference(sat_conversion,[],[f53]) ).
cnf(s3,plain,
( spl5_4
| spl5_6 ),
inference(sat_conversion,[],[f58]) ).
cnf(s5,plain,
( ~ spl5_2
| ~ spl5_4 ),
inference(sat_conversion,[],[f159]) ).
cnf(s6,plain,
( ~ spl5_2
| ~ spl5_5 ),
inference(sat_conversion,[],[f163]) ).
cnf(s10,plain,
( ~ spl5_1
| ~ spl5_6 ),
inference(sat_conversion,[],[f257]) ).
cnf(s13,plain,
( ~ spl5_3
| ~ spl5_4 ),
inference(sat_conversion,[],[f366]) ).
cnf(s26,plain,
( ~ spl5_1
| spl5_3 ),
inference(sat_conversion,[],[f603]) ).
cnf(s51,plain,
( spl5_2
| ~ spl5_3
| spl5_16
| spl5_17
| spl5_18 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s66,plain,
( spl5_2
| ~ spl5_17
| spl5_24 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s73,plain,
( spl5_1
| spl5_2
| ~ spl5_16
| spl5_19
| spl5_20 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s75,plain,
( spl5_2
| ~ spl5_16
| ~ spl5_20 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s81,plain,
( ~ spl5_3
| ~ spl5_16
| spl5_17
| ~ spl5_19
| spl5_26 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s83,plain,
( ~ spl5_3
| ~ spl5_16
| spl5_17
| ~ spl5_19
| spl5_27 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s99,plain,
( ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24
| spl5_27 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s102,plain,
( ~ spl5_3
| ~ spl5_16
| ~ spl5_19
| ~ spl5_24
| spl5_26 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s112,plain,
( spl5_2
| spl5_18
| ~ spl5_27 ),
inference(sat_conversion,[],[f2308]) ).
cnf(s114,plain,
( ~ spl5_18
| ~ spl5_26 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s115,plain,
( ~ spl5_18
| ~ spl5_26 ),
inference(sat_conversion,[],[f2319]) ).
cnf(s118,plain,
( ~ spl5_3
| spl5_16
| spl5_17
| ~ spl5_18 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s148,plain,
( ~ spl5_3
| spl5_16
| ~ spl5_18
| ~ spl5_24 ),
inference(sat_conversion,[],[f2380]) ).
cnf(s159,plain,
( ~ spl5_3
| spl5_16
| ~ spl5_24
| spl5_27 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s161,plain,
( spl5_17
| spl5_16
| ~ spl5_3
| spl5_2 ),
inference(rat,[],[s51,s118]) ).
cnf(s162,plain,
( spl5_16
| spl5_2
| ~ spl5_3 ),
inference(rat,[],[s112,s148,s159,s66,s161]) ).
cnf(s163,plain,
( spl5_17
| ~ spl5_19
| ~ spl5_3
| spl5_2 ),
inference(rat,[],[s114,s112,s81,s83,s162]) ).
cnf(s164,plain,
( spl5_2
| spl5_1 ),
inference(rat,[],[s112,s115,s99,s102,s66,s163,s73,s75,s162,s1]) ).
cnf(s165,plain,
~ spl5_2,
inference(rat,[],[s2,s5,s6]) ).
cnf(s167,plain,
spl5_1,
inference(rat,[],[s164,s165]) ).
cnf(s168,plain,
spl5_3,
inference(rat,[],[s26,s167]) ).
cnf(s170,plain,
~ spl5_6,
inference(rat,[],[s10,s167]) ).
cnf(s172,plain,
~ spl5_4,
inference(rat,[],[s13,s168]) ).
cnf(s174,plain,
$false,
inference(rat,[],[s3,s170,s172]) ).
thf(f2395,plain,
$false,
inference(avatar_sat_refutation,[],[s174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV471^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n010.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Tue Sep 29 15:50:03 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.29 Running higher-order theorem proving
% 0.25/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.63/0.48 % (3032070)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.63/0.48 % (3032080)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=226744415:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.63/0.48 % (3032075)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=431899526:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.63/0.48 % (3032081)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.63/0.48 % (3032081)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.63/0.48 % (3032076)lrs+10_16_si=on:nwc=1.5:random_seed=1505799103:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.63/0.48 % (3032079)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1636534693:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.63/0.49 % (3032078)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=2864093302: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.63/0.49 % (3032077)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3121469605:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.63/0.49 % (3032081)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=2370539928:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.63/0.49 % (3032077)Instruction limit reached!
% 0.63/0.49 % (3032077)------------------------------
% 0.63/0.49 % (3032077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.49 % (3032077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.49 % (3032077)CaDiCaL version: 2.1.3
% 0.63/0.49 % (3032077)Termination reason: Instruction limit
% 0.63/0.49 % (3032077)Termination phase: Saturation
% 0.63/0.49 % (3032077)Time elapsed: 0.007 s
% 0.63/0.49 % (3032077)Peak memory usage: 11 MB
% 0.63/0.49 % (3032077)Instructions burned: 6 (million)
% 0.63/0.49 % (3032076)Instruction limit reached!
% 0.63/0.49 % (3032076)------------------------------
% 0.63/0.49 % (3032076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.49 % (3032076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.49 % (3032076)CaDiCaL version: 2.1.3
% 0.63/0.49 % (3032076)Termination reason: Instruction limit
% 0.63/0.49 % (3032076)Termination phase: Saturation
% 0.63/0.49 % (3032076)Time elapsed: 0.016 s
% 0.63/0.49 % (3032076)Peak memory usage: 11 MB
% 0.63/0.49 % (3032076)Instructions burned: 18 (million)
% 0.63/0.49 % (3032079)Instruction limit reached!
% 0.63/0.49 % (3032079)------------------------------
% 0.63/0.49 % (3032079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.49 % (3032079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.49 % (3032079)CaDiCaL version: 2.1.3
% 0.63/0.49 % (3032079)Termination reason: Instruction limit
% 0.63/0.49 % (3032079)Termination phase: Saturation
% 0.63/0.49 % (3032079)Time elapsed: 0.023 s
% 0.63/0.49 % (3032079)Peak memory usage: 11 MB
% 0.63/0.49 % (3032079)Instructions burned: 25 (million)
% 0.63/0.49 % (3032080)Instruction limit reached!
% 0.63/0.49 % (3032080)------------------------------
% 0.63/0.49 % (3032080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.49 % (3032080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.49 % (3032080)CaDiCaL version: 2.1.3
% 0.63/0.49 % (3032080)Termination reason: Instruction limit
% 0.63/0.49 % (3032080)Termination phase: Saturation
% 0.63/0.49 % (3032080)Time elapsed: 0.039 s
% 0.63/0.49 % (3032080)Peak memory usage: 13 MB
% 0.63/0.49 % (3032080)Instructions burned: 77 (million)
% 0.63/0.49 % (3032089)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3183979676:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.63/0.49 % (3032089)Instruction limit reached!
% 0.63/0.49 % (3032089)------------------------------
% 0.63/0.49 % (3032089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.55 % (3032089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.55 % (3032089)CaDiCaL version: 2.1.3
% 1.42/0.55 % (3032089)Termination reason: Instruction limit
% 1.42/0.55 % (3032089)Termination phase: Preprocessing 1
% 1.42/0.55 % (3032089)Time elapsed: 0.002 s
% 1.42/0.55 % (3032089)Peak memory usage: 9 MB
% 1.42/0.55 % (3032089)Instructions burned: 2 (million)
% 1.42/0.55 % (3032092)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3174402669:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.42/0.55 % (3032090)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2821303215:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.42/0.55 % (3032091)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.42/0.55 % (3032092)Instruction limit reached!
% 1.42/0.55 % (3032092)------------------------------
% 1.42/0.55 % (3032092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.55 % (3032092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.55 % (3032092)CaDiCaL version: 2.1.3
% 1.42/0.55 % (3032092)Termination reason: Instruction limit
% 1.42/0.55 % (3032092)Termination phase: Saturation
% 1.42/0.55 % (3032092)Time elapsed: 0.006 s
% 1.42/0.55 % (3032092)Peak memory usage: 11 MB
% 1.42/0.55 % (3032092)Instructions burned: 13 (million)
% 1.42/0.55 % (3032090)Instruction limit reached!
% 1.42/0.55 % (3032090)------------------------------
% 1.42/0.55 % (3032090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.55 % (3032090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.55 % (3032090)CaDiCaL version: 2.1.3
% 1.42/0.55 % (3032090)Termination reason: Instruction limit
% 1.42/0.55 % (3032090)Termination phase: Saturation
% 1.42/0.55 % (3032090)Time elapsed: 0.006 s
% 1.42/0.55 % (3032090)Peak memory usage: 12 MB
% 1.42/0.55 % (3032090)Instructions burned: 6 (million)
% 1.42/0.55 % (3032091)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2011177699:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.42/0.55 % (3032094)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
% 1.42/0.55 % (3032094)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.42/0.55 % (3032091)Instruction limit reached!
% 1.42/0.55 % (3032091)------------------------------
% 1.42/0.55 % (3032091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.55 % (3032091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.55 % (3032091)CaDiCaL version: 2.1.3
% 1.42/0.55 % (3032091)Termination reason: Instruction limit
% 1.42/0.55 % (3032091)Termination phase: Saturation
% 1.42/0.55 % (3032091)Time elapsed: 0.008 s
% 1.42/0.55 % (3032091)Peak memory usage: 12 MB
% 1.42/0.55 % (3032091)Instructions burned: 7 (million)
% 1.42/0.55 % (3032094)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2228689318:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.42/0.55 % (3032075)Instruction limit reached!
% 1.42/0.55 % (3032075)------------------------------
% 1.42/0.55 % (3032075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.55 % (3032075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.55 % (3032075)CaDiCaL version: 2.1.3
% 1.42/0.55 % (3032075)Termination reason: Instruction limit
% 1.42/0.55 % (3032075)Termination phase: Saturation
% 1.42/0.55 % (3032075)Time elapsed: 0.078 s
% 1.42/0.55 % (3032075)Peak memory usage: 13 MB
% 1.42/0.55 % (3032075)Instructions burned: 87 (million)
% 1.42/0.55 % (3032097)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2510264009:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.42/0.55 % (3032094)Instruction limit reached!
% 1.42/0.55 % (3032094)------------------------------
% 1.42/0.55 % (3032094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (3032094)CaDiCaL version: 2.1.3
% 2.15/0.62 % (3032094)Termination reason: Instruction limit
% 2.15/0.62 % (3032094)Termination phase: Saturation
% 2.15/0.62 % (3032094)Time elapsed: 0.016 s
% 2.15/0.62 % (3032094)Peak memory usage: 12 MB
% 2.15/0.62 % (3032094)Instructions burned: 29 (million)
% 2.15/0.62 % (3032098)lrs+10_1_si=on:cs=on:random_seed=3967100831:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 2.15/0.62 % (3032101)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.15/0.62 % (3032101)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=2131608152:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 2.15/0.62 % (3032098)Instruction limit reached!
% 2.15/0.62 % (3032098)------------------------------
% 2.15/0.62 % (3032098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (3032098)CaDiCaL version: 2.1.3
% 2.15/0.62 % (3032098)Termination reason: Instruction limit
% 2.15/0.62 % (3032098)Termination phase: Saturation
% 2.15/0.62 % (3032098)Time elapsed: 0.008 s
% 2.15/0.62 % (3032098)Peak memory usage: 12 MB
% 2.15/0.62 % (3032098)Instructions burned: 9 (million)
% 2.15/0.62 % (3032102)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1538702689:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.15/0.62 % (3032101)Instruction limit reached!
% 2.15/0.62 % (3032101)------------------------------
% 2.15/0.62 % (3032101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (3032101)CaDiCaL version: 2.1.3
% 2.15/0.62 % (3032101)Termination reason: Instruction limit
% 2.15/0.62 % (3032101)Termination phase: Preprocessing 3
% 2.15/0.62 % (3032101)Time elapsed: 0.002 s
% 2.15/0.62 % (3032101)Peak memory usage: 9 MB
% 2.15/0.62 % (3032101)Instructions burned: 2 (million)
% 2.15/0.62 % (3032104)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3845847103:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.15/0.62 % (3032097)Instruction limit reached!
% 2.15/0.62 % (3032097)------------------------------
% 2.15/0.62 % (3032097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (3032097)CaDiCaL version: 2.1.3
% 2.15/0.62 % (3032097)Termination reason: Instruction limit
% 2.15/0.62 % (3032097)Termination phase: Saturation
% 2.15/0.62 % (3032097)Time elapsed: 0.038 s
% 2.15/0.62 % (3032097)Peak memory usage: 12 MB
% 2.15/0.62 % (3032097)Instructions burned: 86 (million)
% 2.15/0.62 % (3032111)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3970978222:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.15/0.62 % (3032107)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1049805108:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.15/0.62 % (3032109)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1860093140:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.15/0.62 % (3032102)Instruction limit reached!
% 2.15/0.62 % (3032102)------------------------------
% 2.15/0.62 % (3032102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (3032102)CaDiCaL version: 2.1.3
% 2.15/0.62 % (3032102)Termination reason: Instruction limit
% 2.15/0.62 % (3032102)Termination phase: Saturation
% 2.15/0.62 % (3032102)Time elapsed: 0.036 s
% 2.15/0.62 % (3032102)Peak memory usage: 12 MB
% 2.15/0.62 % (3032102)Instructions burned: 38 (million)
% 2.15/0.62 % (3032081)Instruction limit reached!
% 2.15/0.62 % (3032081)------------------------------
% 2.15/0.62 % (3032081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (3032081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032081)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032081)Termination reason: Instruction limit
% 2.52/0.70 % (3032081)Termination phase: Saturation
% 2.52/0.70 % (3032081)Time elapsed: 0.140 s
% 2.52/0.70 % (3032081)Peak memory usage: 12 MB
% 2.52/0.70 % (3032081)Instructions burned: 157 (million)
% 2.52/0.70 % (3032109)Instruction limit reached!
% 2.52/0.70 % (3032109)------------------------------
% 2.52/0.70 % (3032109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032109)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032109)Termination reason: Instruction limit
% 2.52/0.70 % (3032109)Termination phase: Saturation
% 2.52/0.70 % (3032109)Time elapsed: 0.013 s
% 2.52/0.70 % (3032109)Peak memory usage: 11 MB
% 2.52/0.70 % (3032109)Instructions burned: 14 (million)
% 2.52/0.70 % (3032107)Instruction limit reached!
% 2.52/0.70 % (3032107)------------------------------
% 2.52/0.70 % (3032107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032107)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032107)Termination reason: Instruction limit
% 2.52/0.70 % (3032107)Termination phase: Saturation
% 2.52/0.70 % (3032107)Time elapsed: 0.025 s
% 2.52/0.70 % (3032107)Peak memory usage: 12 MB
% 2.52/0.70 % (3032107)Instructions burned: 26 (million)
% 2.52/0.70 % (3032115)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4111706891:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.52/0.70 % (3032116)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2778164134:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.52/0.70 % (3032118)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=845218400:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.52/0.70 % (3032117)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2547940733:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.52/0.70 % (3032116)Instruction limit reached!
% 2.52/0.70 % (3032116)------------------------------
% 2.52/0.70 % (3032116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032116)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032116)Termination reason: Instruction limit
% 2.52/0.70 % (3032116)Termination phase: Preprocessing 3
% 2.52/0.70 % (3032116)Time elapsed: 0.002 s
% 2.52/0.70 % (3032116)Peak memory usage: 10 MB
% 2.52/0.70 % (3032116)Instructions burned: 2 (million)
% 2.52/0.70 % (3032115)Instruction limit reached!
% 2.52/0.70 % (3032115)------------------------------
% 2.52/0.70 % (3032115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032115)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032115)Termination reason: Instruction limit
% 2.52/0.70 % (3032115)Termination phase: Saturation
% 2.52/0.70 % (3032115)Time elapsed: 0.013 s
% 2.52/0.70 % (3032115)Peak memory usage: 12 MB
% 2.52/0.70 % (3032115)Instructions burned: 14 (million)
% 2.52/0.70 % (3032118)Instruction limit reached!
% 2.52/0.70 % (3032118)------------------------------
% 2.52/0.70 % (3032118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032118)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032118)Termination reason: Instruction limit
% 2.52/0.70 % (3032118)Termination phase: Saturation
% 2.52/0.70 % (3032118)Time elapsed: 0.014 s
% 2.52/0.70 % (3032118)Peak memory usage: 11 MB
% 2.52/0.70 % (3032118)Instructions burned: 23 (million)
% 2.52/0.70 % (3032117)Instruction limit reached!
% 2.52/0.70 % (3032117)------------------------------
% 2.52/0.70 % (3032117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.70 % (3032117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.70 % (3032117)CaDiCaL version: 2.1.3
% 2.52/0.70 % (3032117)Termination reason: Instruction limit
% 2.52/0.70 % (3032117)Termination phase: Saturation
% 2.52/0.70 % (3032117)Time elapsed: 0.025 s
% 2.52/0.70 % (3032117)Peak memory usage: 12 MB
% 2.52/0.70 % (3032117)Instructions burned: 26 (million)
% 3.11/0.82 % (3032123)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2553353501:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 3.11/0.82 % (3032124)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) 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
% 3.11/0.82 % (3032124)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 3.11/0.82 % (3032125)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.11/0.82 % (3032124)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3979775652:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.11/0.82 % (3032125)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=3698960432:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.11/0.82 % (3032125)Instruction limit reached!
% 3.11/0.82 % (3032125)------------------------------
% 3.11/0.82 % (3032125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.11/0.82 % (3032125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/0.82 % (3032125)CaDiCaL version: 2.1.3
% 3.11/0.82 % (3032125)Termination reason: Instruction limit
% 3.11/0.82 % (3032125)Termination phase: Saturation
% 3.11/0.82 % (3032125)Time elapsed: 0.008 s
% 3.11/0.82 % (3032125)Peak memory usage: 11 MB
% 3.11/0.82 % (3032125)Instructions burned: 8 (million)
% 3.11/0.82 % (3032124)Instruction limit reached!
% 3.11/0.82 % (3032124)------------------------------
% 3.11/0.82 % (3032124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.11/0.82 % (3032124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/0.82 % (3032127)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1356891407:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.11/0.82 % (3032124)CaDiCaL version: 2.1.3
% 3.11/0.82 % (3032124)Termination reason: Instruction limit
% 3.11/0.82 % (3032124)Termination phase: Saturation
% 3.11/0.82 % (3032124)Time elapsed: 0.018 s
% 3.11/0.82 % (3032124)Peak memory usage: 12 MB
% 3.11/0.82 % (3032124)Instructions burned: 16 (million)
% 3.11/0.82 % (3032131)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3539632623:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.11/0.82 % (3032127)Instruction limit reached!
% 3.11/0.82 % (3032127)------------------------------
% 3.11/0.82 % (3032127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.11/0.82 % (3032127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/0.82 % (3032127)CaDiCaL version: 2.1.3
% 3.11/0.82 % (3032127)Termination reason: Instruction limit
% 3.11/0.82 % (3032127)Termination phase: Saturation
% 3.11/0.82 % (3032127)Time elapsed: 0.030 s
% 3.11/0.82 % (3032127)Peak memory usage: 12 MB
% 3.11/0.82 % (3032127)Instructions burned: 32 (million)
% 3.11/0.82 % (3032123)Instruction limit reached!
% 3.11/0.82 % (3032123)------------------------------
% 3.11/0.82 % (3032123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.11/0.82 % (3032123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/0.82 % (3032123)CaDiCaL version: 2.1.3
% 3.11/0.82 % (3032123)Termination reason: Instruction limit
% 3.11/0.82 % (3032123)Termination phase: Saturation
% 3.11/0.82 % (3032123)Time elapsed: 0.056 s
% 3.11/0.82 % (3032123)Peak memory usage: 13 MB
% 3.11/0.82 % (3032123)Instructions burned: 60 (million)
% 3.11/0.82 % (3032134)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1834011425:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.11/0.82 % (3032131)Instruction limit reached!
% 3.11/0.82 % (3032131)------------------------------
% 3.11/0.82 % (3032131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.11/0.82 % (3032131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/0.82 % (3032131)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032131)Termination reason: Instruction limit
% 3.68/0.91 % (3032131)Termination phase: Saturation
% 3.68/0.91 % (3032131)Time elapsed: 0.009 s
% 3.68/0.91 % (3032131)Peak memory usage: 12 MB
% 3.68/0.91 % (3032131)Instructions burned: 8 (million)
% 3.68/0.91 % (3032111)Instruction limit reached!
% 3.68/0.91 % (3032111)------------------------------
% 3.68/0.91 % (3032111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.91 % (3032111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.91 % (3032111)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032111)Termination reason: Instruction limit
% 3.68/0.91 % (3032111)Termination phase: Saturation
% 3.68/0.91 % (3032111)Time elapsed: 0.156 s
% 3.68/0.91 % (3032111)Peak memory usage: 13 MB
% 3.68/0.91 % (3032111)Instructions burned: 328 (million)
% 3.68/0.91 % (3032136)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1440223325:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/20Mi)
% 3.68/0.91 % (3032134)Instruction limit reached!
% 3.68/0.91 % (3032134)------------------------------
% 3.68/0.91 % (3032134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.91 % (3032134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.91 % (3032134)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032134)Termination reason: Instruction limit
% 3.68/0.91 % (3032134)Termination phase: Saturation
% 3.68/0.91 % (3032134)Time elapsed: 0.019 s
% 3.68/0.91 % (3032134)Peak memory usage: 12 MB
% 3.68/0.91 % (3032134)Instructions burned: 24 (million)
% 3.68/0.91 % (3032137)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3831688999:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.68/0.91 % (3032139)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2357017101:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.68/0.91 % (3032136)Instruction limit reached!
% 3.68/0.91 % (3032136)------------------------------
% 3.68/0.91 % (3032136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.91 % (3032136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.91 % (3032136)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032136)Termination reason: Instruction limit
% 3.68/0.91 % (3032136)Termination phase: Saturation
% 3.68/0.91 % (3032136)Time elapsed: 0.022 s
% 3.68/0.91 % (3032136)Peak memory usage: 12 MB
% 3.68/0.91 % (3032136)Instructions burned: 20 (million)
% 3.68/0.91 % (3032140)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1467178517:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.68/0.91 % (3032142)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=587903717:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.68/0.91 % (3032104)Instruction limit reached!
% 3.68/0.91 % (3032104)------------------------------
% 3.68/0.91 % (3032104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.91 % (3032104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.91 % (3032104)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032104)Termination reason: Instruction limit
% 3.68/0.91 % (3032104)Termination phase: Saturation
% 3.68/0.91 % (3032104)Time elapsed: 0.221 s
% 3.68/0.91 % (3032104)Peak memory usage: 13 MB
% 3.68/0.91 % (3032104)Instructions burned: 250 (million)
% 3.68/0.91 % (3032145)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.68/0.91 % (3032145)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1237199493:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.68/0.91 % (3032142)Instruction limit reached!
% 3.68/0.91 % (3032142)------------------------------
% 3.68/0.91 % (3032142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.91 % (3032142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.91 % (3032142)CaDiCaL version: 2.1.3
% 3.68/0.91 % (3032142)Termination reason: Instruction limit
% 3.68/0.91 % (3032142)Termination phase: Saturation
% 3.68/0.91 % (3032142)Time elapsed: 0.025 s
% 3.68/0.91 % (3032142)Peak memory usage: 12 MB
% 3.68/0.91 % (3032142)Instructions burned: 43 (million)
% 3.68/0.91 % (3032145)Instruction limit reached!
% 3.68/0.91 % (3032145)------------------------------
% 5.10/1.06 % (3032145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.06 % (3032145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.06 % (3032145)CaDiCaL version: 2.1.3
% 5.10/1.06 % (3032145)Termination reason: Instruction limit
% 5.10/1.06 % (3032145)Termination phase: Saturation
% 5.10/1.06 % (3032145)Time elapsed: 0.008 s
% 5.10/1.06 % (3032145)Peak memory usage: 12 MB
% 5.10/1.06 % (3032145)Instructions burned: 7 (million)
% 5.10/1.06 % (3032148)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4253647696:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 5.10/1.06 % (3032150)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1928193617:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 5.10/1.06 % (3032151)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 5.10/1.06 % (3032151)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3928899083:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 5.10/1.06 % (3032151)Instruction limit reached!
% 5.10/1.06 % (3032151)------------------------------
% 5.10/1.06 % (3032151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.06 % (3032151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.06 % (3032151)CaDiCaL version: 2.1.3
% 5.10/1.06 % (3032151)Termination reason: Instruction limit
% 5.10/1.06 % (3032151)Termination phase: Saturation
% 5.10/1.06 % (3032151)Time elapsed: 0.006 s
% 5.10/1.06 % (3032151)Peak memory usage: 12 MB
% 5.10/1.06 % (3032151)Instructions burned: 6 (million)
% 5.10/1.06 % (3032155)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2472480514:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 5.10/1.06 % (3032139)Instruction limit reached!
% 5.10/1.06 % (3032139)------------------------------
% 5.10/1.06 % (3032139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.06 % (3032139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.06 % (3032139)CaDiCaL version: 2.1.3
% 5.10/1.06 % (3032139)Termination reason: Instruction limit
% 5.10/1.06 % (3032139)Termination phase: Saturation
% 5.10/1.06 % (3032139)Time elapsed: 0.126 s
% 5.10/1.06 % (3032139)Peak memory usage: 13 MB
% 5.10/1.06 % (3032139)Instructions burned: 143 (million)
% 5.10/1.06 % (3032155)Instruction limit reached!
% 5.10/1.06 % (3032155)------------------------------
% 5.10/1.06 % (3032155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.06 % (3032155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.06 % (3032155)CaDiCaL version: 2.1.3
% 5.10/1.06 % (3032155)Termination reason: Instruction limit
% 5.10/1.06 % (3032155)Termination phase: Saturation
% 5.10/1.06 % (3032155)Time elapsed: 0.017 s
% 5.10/1.06 % (3032155)Peak memory usage: 13 MB
% 5.10/1.06 % (3032155)Instructions burned: 23 (million)
% 5.10/1.06 % (3032150)Instruction limit reached!
% 5.10/1.06 % (3032150)------------------------------
% 5.10/1.06 % (3032150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.06 % (3032150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.06 % (3032150)CaDiCaL version: 2.1.3
% 5.10/1.06 % (3032150)Termination reason: Instruction limit
% 5.10/1.06 % (3032150)Termination phase: Saturation
% 5.10/1.06 % (3032150)Time elapsed: 0.086 s
% 5.10/1.06 % (3032150)Peak memory usage: 13 MB
% 5.10/1.06 % (3032150)Instructions burned: 170 (million)
% 5.10/1.06 % (3032157)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=685596846:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 5.10/1.06 % (3032158)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=2927966374:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.10/1.06 % (3032159)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=1495400548:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.10/1.08 % (3032157)Instruction limit reached!
% 5.10/1.08 % (3032157)------------------------------
% 5.10/1.08 % (3032157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032157)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032157)Termination reason: Instruction limit
% 5.10/1.08 % (3032157)Termination phase: Saturation
% 5.10/1.08 % (3032157)Time elapsed: 0.019 s
% 5.10/1.08 % (3032157)Peak memory usage: 13 MB
% 5.10/1.08 % (3032157)Instructions burned: 19 (million)
% 5.10/1.08 % (3032078)Instruction limit reached!
% 5.10/1.08 % (3032078)------------------------------
% 5.10/1.08 % (3032078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032078)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032078)Termination reason: Instruction limit
% 5.10/1.08 % (3032078)Termination phase: Saturation
% 5.10/1.08 % (3032078)Time elapsed: 0.494 s
% 5.10/1.08 % (3032078)Peak memory usage: 14 MB
% 5.10/1.08 % (3032078)Instructions burned: 637 (million)
% 5.10/1.08 % (3032140)Instruction limit reached!
% 5.10/1.08 % (3032140)------------------------------
% 5.10/1.08 % (3032140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032140)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032140)Termination reason: Instruction limit
% 5.10/1.08 % (3032140)Termination phase: Saturation
% 5.10/1.08 % (3032140)Time elapsed: 0.174 s
% 5.10/1.08 % (3032140)Peak memory usage: 13 MB
% 5.10/1.08 % (3032140)Instructions burned: 193 (million)
% 5.10/1.08 % (3032164)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2741426281:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.10/1.08 % (3032163)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=4248021884:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 5.10/1.08 % (3032148)Instruction limit reached!
% 5.10/1.08 % (3032148)------------------------------
% 5.10/1.08 % (3032148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032148)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032148)Termination reason: Instruction limit
% 5.10/1.08 % (3032148)Termination phase: Saturation
% 5.10/1.08 % (3032148)Time elapsed: 0.163 s
% 5.10/1.08 % (3032148)Peak memory usage: 13 MB
% 5.10/1.08 % (3032148)Instructions burned: 182 (million)
% 5.10/1.08 % (3032165)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1153505388:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.10/1.08 % (3032168)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.10/1.08 % (3032168)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3884744471:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 5.10/1.08 % (3032165)Instruction limit reached!
% 5.10/1.08 % (3032165)------------------------------
% 5.10/1.08 % (3032165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032165)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032165)Termination reason: Instruction limit
% 5.10/1.08 % (3032165)Termination phase: Saturation
% 5.10/1.08 % (3032165)Time elapsed: 0.020 s
% 5.10/1.08 % (3032165)Peak memory usage: 12 MB
% 5.10/1.08 % (3032165)Instructions burned: 22 (million)
% 5.10/1.08 % (3032163)Instruction limit reached!
% 5.10/1.08 % (3032163)------------------------------
% 5.10/1.08 % (3032163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032163)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032163)Termination reason: Instruction limit
% 5.10/1.08 % (3032163)Termination phase: Saturation
% 5.10/1.08 % (3032163)Time elapsed: 0.043 s
% 5.10/1.08 % (3032163)Peak memory usage: 12 MB
% 5.10/1.08 % (3032163)Instructions burned: 46 (million)
% 5.10/1.08 % (3032171)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1455196292:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 5.10/1.08 % (3032172)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=3065569520:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 5.10/1.08 % (3032171)Instruction limit reached!
% 5.10/1.08 % (3032171)------------------------------
% 5.10/1.08 % (3032171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032171)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032171)Termination reason: Instruction limit
% 5.10/1.08 % (3032171)Termination phase: Saturation
% 5.10/1.08 % (3032171)Time elapsed: 0.012 s
% 5.10/1.08 % (3032171)Peak memory usage: 11 MB
% 5.10/1.08 % (3032171)Instructions burned: 13 (million)
% 5.10/1.08 % (3032176)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1228527620:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 5.10/1.08 % (3032172)Instruction limit reached!
% 5.10/1.08 % (3032172)------------------------------
% 5.10/1.08 % (3032172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032172)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032172)Termination reason: Instruction limit
% 5.10/1.08 % (3032172)Termination phase: Saturation
% 5.10/1.08 % (3032172)Time elapsed: 0.059 s
% 5.10/1.08 % (3032172)Peak memory usage: 12 MB
% 5.10/1.08 % (3032172)Instructions burned: 67 (million)
% 5.10/1.08 % (3032176)Instruction limit reached!
% 5.10/1.08 % (3032176)------------------------------
% 5.10/1.08 % (3032176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032176)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032176)Termination reason: Instruction limit
% 5.10/1.08 % (3032176)Termination phase: Saturation
% 5.10/1.08 % (3032176)Time elapsed: 0.047 s
% 5.10/1.08 % (3032176)Peak memory usage: 12 MB
% 5.10/1.08 % (3032176)Instructions burned: 52 (million)
% 5.10/1.08 % (3032179)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3627187184:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 5.10/1.08 % (3032168)Instruction limit reached!
% 5.10/1.08 % (3032168)------------------------------
% 5.10/1.08 % (3032168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032168)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032168)Termination reason: Instruction limit
% 5.10/1.08 % (3032168)Termination phase: Saturation
% 5.10/1.08 % (3032168)Time elapsed: 0.148 s
% 5.10/1.08 % (3032168)Peak memory usage: 12 MB
% 5.10/1.08 % (3032168)Instructions burned: 201 (million)
% 5.10/1.08 % (3032158)Instruction limit reached!
% 5.10/1.08 % (3032158)------------------------------
% 5.10/1.08 % (3032158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032158)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032158)Termination reason: Instruction limit
% 5.10/1.08 % (3032158)Termination phase: Saturation
% 5.10/1.08 % (3032158)Time elapsed: 0.235 s
% 5.10/1.08 % (3032158)Peak memory usage: 13 MB
% 5.10/1.08 % (3032158)Instructions burned: 317 (million)
% 5.10/1.08 % (3032179)Instruction limit reached!
% 5.10/1.08 % (3032179)------------------------------
% 5.10/1.08 % (3032179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032179)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032179)Termination reason: Instruction limit
% 5.10/1.08 % (3032179)Termination phase: Saturation
% 5.10/1.08 % (3032179)Time elapsed: 0.030 s
% 5.10/1.08 % (3032179)Peak memory usage: 12 MB
% 5.10/1.08 % (3032179)Instructions burned: 33 (million)
% 5.10/1.08 % (3032137) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3032070-3032137"...
% 5.10/1.08 % (3032181)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1671469209:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2992 on theBenchmark for (2992ds/137Mi)
% 5.10/1.08 % (3032183)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3219837940:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 5.10/1.08 % (3032182)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=1209489092:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 5.10/1.08 % (3032137)...printing done.
% 5.10/1.08 % (3032137)Refutation found. Thanks to Tanya!
% 5.10/1.08 % SZS status Theorem for theBenchmark
% 5.10/1.08 % SZS output start Proof for theBenchmark
% See solution above
% 5.10/1.08 % (3032137)------------------------------
% 5.10/1.08 % (3032137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.10/1.08 % (3032137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.08 % (3032137)CaDiCaL version: 2.1.3
% 5.10/1.08 % (3032137)Termination reason: Refutation
% 5.10/1.08 % (3032137)Time elapsed: 0.425 s
% 5.10/1.08 % (3032137)Peak memory usage: 15 MB
% 5.10/1.08 % (3032137)Instructions burned: 476 (million)
% 5.10/1.08 % (3032070)Success in time 0.767 s
% 5.10/1.08 % Vampire exiting
%------------------------------------------------------------------------------