%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG290^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 07:45:21 AM UTC 2026
% Result : Theorem 7.37s 1.41s
% Output : Refutation 7.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 110 ( 15 unt; 0 typ; 8 def)
% Number of atoms : 1038 ( 208 equ; 0 cnn)
% Maximal formula atoms : 7 ( 9 avg)
% Number of connectives : 3076 ( 136 ~; 164 |; 290 &;1810 @)
% ( 11 <=>; 279 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 174 ( 174 >; 0 *; 0 +; 0 <<)
% Number of symbols : 39 ( 34 usr; 19 con; 0-4 aty)
% ( 255 !!; 131 ??; 0 @@+; 0 @@-)
% Number of variables : 488 ( 0 sgn 56 !; 21 ?; 488 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
cP: a > a > a ).
thf(func_def_1,type,
cG: a > $o ).
thf(func_def_2,type,
cX: a > $o ).
thf(func_def_3,type,
cR: a > a ).
thf(func_def_4,type,
cL: a > a ).
thf(func_def_5,type,
cF: a > $o ).
thf(func_def_6,type,
cZ: a ).
thf(func_def_8,type,
vNOT: $o > $o ).
thf(func_def_9,type,
vIMP: $o > $o > $o ).
thf(func_def_10,type,
vAND: $o > $o > $o ).
thf(func_def_11,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_12,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_15,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_16,type,
vIFF: $o > $o > $o ).
thf(func_def_17,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_18,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_19,type,
vOR: $o > $o > $o ).
thf(func_def_23,type,
sK1: a ).
thf(func_def_24,type,
sK2: a ).
thf(func_def_25,type,
sK3: a ).
thf(func_def_26,type,
sK4: a ).
thf(func_def_27,type,
sK5: a ).
thf(func_def_28,type,
sK6: a ).
thf(f1,conjecture,
( ( ! [X1: a,X0: a] :
( ( cL @ ( cP @ X0 @ X1 ) )
= X0 )
& ! [X3: a > $o] :
( ? [X2: a] :
( ! [X4: a] :
( ( X3 @ X4 )
=> ( X3 @ ( cL @ X4 ) ) )
& ( X3 @ X2 ) )
=> ( X3 @ cZ ) )
& ( ( cR @ cZ )
= cZ )
& ( ( cL @ cZ )
= cZ )
& ! [X2: a] :
( ( X2 != cZ )
<=> ( X2
= ( cP @ ( cL @ X2 ) @ ( cR @ X2 ) ) ) )
& ! [X1: a,X0: a] :
( ( cR @ ( cP @ X0 @ X1 ) )
= X1 ) )
=> ( ( ^ [X1: a] :
? [X0: a] :
( ! [X5: a] :
( ! [X3: a > $o] :
( ( ! [X6: a] :
( ( X3 @ X6 )
=> ( X3 @ ( cL @ X6 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X5 ) ) )
=> ( cX @ X5 ) )
& ( ( cF @ ( cP @ X0 @ X1 ) )
| ( cG @ ( cP @ X0 @ X1 ) ) ) ) )
= ( ^ [X6: a] :
( ? [X0: a] :
( ! [X8: a] :
( ! [X3: a > $o] :
( ( ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X8 ) ) )
=> ( cX @ X8 ) )
& ( cF @ ( cP @ X0 @ X6 ) ) )
| ? [X0: a] :
( ! [X10: a] :
( ! [X3: a > $o] :
( ( ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X10 ) ) )
=> ( cX @ X10 ) )
& ( cG @ ( cP @ X0 @ X6 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cPU_X2310A_pme) ).
thf(f2,negated_conjecture,
~ ( ( ! [X1: a,X0: a] :
( ( cL @ ( cP @ X0 @ X1 ) )
= X0 )
& ! [X3: a > $o] :
( ? [X2: a] :
( ! [X4: a] :
( ( X3 @ X4 )
=> ( X3 @ ( cL @ X4 ) ) )
& ( X3 @ X2 ) )
=> ( X3 @ cZ ) )
& ( ( cR @ cZ )
= cZ )
& ( ( cL @ cZ )
= cZ )
& ! [X2: a] :
( ( X2 != cZ )
<=> ( X2
= ( cP @ ( cL @ X2 ) @ ( cR @ X2 ) ) ) )
& ! [X1: a,X0: a] :
( ( cR @ ( cP @ X0 @ X1 ) )
= X1 ) )
=> ( ( ^ [X1: a] :
? [X0: a] :
( ! [X5: a] :
( ! [X3: a > $o] :
( ( ! [X6: a] :
( ( X3 @ X6 )
=> ( X3 @ ( cL @ X6 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X5 ) ) )
=> ( cX @ X5 ) )
& ( ( cF @ ( cP @ X0 @ X1 ) )
| ( cG @ ( cP @ X0 @ X1 ) ) ) ) )
= ( ^ [X6: a] :
( ? [X0: a] :
( ! [X8: a] :
( ! [X3: a > $o] :
( ( ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X8 ) ) )
=> ( cX @ X8 ) )
& ( cF @ ( cP @ X0 @ X6 ) ) )
| ? [X0: a] :
( ! [X10: a] :
( ! [X3: a > $o] :
( ( ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X10 ) ) )
=> ( cX @ X10 ) )
& ( cG @ ( cP @ X0 @ X6 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ( ( ! [X0: a,X1: a] :
( ( cL @ ( cP @ X1 @ X0 ) )
= X1 )
& ! [X2: a > $o] :
( ? [X3: a] :
( ! [X4: a] :
( ( X2 @ X4 )
=> ( X2 @ ( cL @ X4 ) ) )
& ( X2 @ X3 ) )
=> ( X2 @ cZ ) )
& ( ( cR @ cZ )
= cZ )
& ( ( cL @ cZ )
= cZ )
& ! [X5: a] :
( ( cZ != X5 )
<=> ( ( cP @ ( cL @ X5 ) @ ( cR @ X5 ) )
= X5 ) )
& ! [X6: a,X7: a] :
( ( cR @ ( cP @ X7 @ X6 ) )
= X6 ) )
=> ( ( ^ [X8: a] :
? [X9: a] :
( ! [X10: a] :
( ! [X11: a > $o] :
( ( ! [X12: a] :
( ( X11 @ X12 )
=> ( X11 @ ( cL @ X12 ) ) )
& ( X11 @ X9 ) )
=> ? [X13: a] :
( ( X11 @ X13 )
& ( ( cR @ X13 )
= X10 ) ) )
=> ( cX @ X10 ) )
& ( ( cF @ ( cP @ X9 @ X8 ) )
| ( cG @ ( cP @ X9 @ X8 ) ) ) ) )
= ( ^ [X14: a] :
( ? [X15: a] :
( ! [X16: a] :
( ! [X17: a > $o] :
( ( ! [X18: a] :
( ( X17 @ X18 )
=> ( X17 @ ( cL @ X18 ) ) )
& ( X17 @ X15 ) )
=> ? [X19: a] :
( ( X17 @ X19 )
& ( ( cR @ X19 )
= X16 ) ) )
=> ( cX @ X16 ) )
& ( cF @ ( cP @ X15 @ X14 ) ) )
| ? [X20: a] :
( ! [X21: a] :
( ! [X22: a > $o] :
( ( ! [X23: a] :
( ( X22 @ X23 )
=> ( X22 @ ( cL @ X23 ) ) )
& ( X22 @ X20 ) )
=> ? [X24: a] :
( ( X22 @ X24 )
& ( ( cR @ X24 )
= X21 ) ) )
=> ( cX @ X21 ) )
& ( cG @ ( cP @ X20 @ X14 ) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
( $true
= ( ~ ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cL @ cZ ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) ) ) )
=> ( Y0 @ cZ ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( $true
= ( ~ ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cL @ cZ ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) ) ) )
=> ( Y0 @ cZ ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f4]) ).
thf(f7,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y0 @ Y1 ) )
= Y1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cL @ cZ ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) ) ) )
=> ( Y0 @ cZ ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ) ) )
= $false ),
inference(not_proxy_clausification,[],[f5]) ).
thf(f10,plain,
( ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f7]) ).
thf(f52,plain,
( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
!= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ) ),
inference(equality_proxy_clausification,[],[f10]) ).
thf(f126,plain,
( ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( cG @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( cF @ ( cP @ Y1 @ Y0 ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
@ sK1 )
!= ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
@ sK1 ) ),
inference(negative_extensionality,[],[f52]) ).
thf(f127,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
!= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f126]) ).
thf(f203,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ( $true
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ) ),
inference(xor_proxy_clausification,[],[f127]) ).
thf(f204,plain,
( ( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
= $false )
| ( ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
= $false ) ),
inference(xor_proxy_clausification,[],[f127]) ).
thf(f206,definition,
( spl0_5
<=> ( ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
thf(f208,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
= $false )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f206]) ).
thf(f210,definition,
( spl0_6
<=> ( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
thf(f212,plain,
( ( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
= $false )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f210]) ).
thf(f213,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f204,f210,f206]) ).
thf(f215,definition,
( spl0_7
<=> ( $true
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
thf(f217,plain,
( ( $true
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f215]) ).
thf(f219,definition,
( spl0_8
<=> ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
thf(f221,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f219]) ).
thf(f222,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f203,f219,f215]) ).
thf(f224,plain,
( ( $true = $false )
| ~ spl0_5
| ~ spl0_8 ),
inference(backward_demodulation,[],[f221,f208]) ).
thf(f225,plain,
( $false
| ~ spl0_5
| ~ spl0_8 ),
inference(trivial_inequality_removal,[],[f224]) ).
thf(f226,plain,
( ~ spl0_5
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f225]) ).
thf(f253,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ X1 )
= $false )
| ~ spl0_5 ),
inference(pi_proxy_clausification,[],[f208]) ).
thf(f254,plain,
( ! [X1: a] :
( ( ( ( cG @ ( cP @ X1 @ sK1 ) )
| ( cF @ ( cP @ X1 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ X1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_5 ),
inference(beta-eta_normalization,[],[f253]) ).
thf(f256,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_7 ),
inference(or_proxy_clausification,[],[f217]) ).
thf(f258,definition,
( spl0_9
<=> ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
thf(f259,plain,
( ( $true
!= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| spl0_9 ),
inference(avatar_component_clause,[],[f258]) ).
thf(f260,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f258]) ).
thf(f262,definition,
( spl0_10
<=> ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
thf(f264,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f262]) ).
thf(f265,plain,
( spl0_9
| spl0_10
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f256,f215,f262,f258]) ).
thf(f268,plain,
( ( $true
= ( ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ sK4 ) )
| ~ spl0_9 ),
inference(sigma_proxy_clausification,[],[f260]) ).
thf(f269,plain,
( ( $true
= ( ( cF @ ( cP @ sK4 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_9 ),
inference(beta-eta_normalization,[],[f268]) ).
thf(f270,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
| ~ spl0_9 ),
inference(and_proxy_clausification,[],[f269]) ).
thf(f271,plain,
( ( ( cF @ ( cP @ sK4 @ sK1 ) )
= $true )
| ~ spl0_9 ),
inference(and_proxy_clausification,[],[f269]) ).
thf(f274,plain,
( ( ( ( ( cG @ ( cP @ sK4 @ sK1 ) )
| $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_5
| ~ spl0_9 ),
inference(constrained_superposition,[],[f254,f271]) ).
thf(f275,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_5
| ~ spl0_9 ),
inference(boolean_simplification,[],[f274]) ).
thf(f276,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_5
| ~ spl0_9 ),
inference(boolean_simplification,[],[f275]) ).
thf(f277,plain,
( ( $true = $false )
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f270,f276]) ).
thf(f278,plain,
( $false
| ~ spl0_5
| ~ spl0_9 ),
inference(trivial_inequality_removal,[],[f277]) ).
thf(f279,plain,
( ~ spl0_5
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f278]) ).
thf(f282,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ X1 )
= $false )
| spl0_9 ),
inference(pi_proxy_clausification,[],[f259]) ).
thf(f283,plain,
( ! [X1: a] :
( ( ( cF @ ( cP @ X1 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ X1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| spl0_9 ),
inference(beta-eta_normalization,[],[f282]) ).
thf(f287,plain,
( ( $true
= ( ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ sK5 ) )
| ~ spl0_10 ),
inference(sigma_proxy_clausification,[],[f264]) ).
thf(f288,plain,
( ( $true
= ( ( cG @ ( cP @ sK5 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK5 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_10 ),
inference(beta-eta_normalization,[],[f287]) ).
thf(f289,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK5 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $true )
| ~ spl0_10 ),
inference(and_proxy_clausification,[],[f288]) ).
thf(f290,plain,
( ( $true
= ( cG @ ( cP @ sK5 @ sK1 ) ) )
| ~ spl0_10 ),
inference(and_proxy_clausification,[],[f288]) ).
thf(f293,plain,
( ( ( ( $true
| ( cF @ ( cP @ sK5 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK5 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_5
| ~ spl0_10 ),
inference(constrained_superposition,[],[f254,f290]) ).
thf(f294,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK5 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_5
| ~ spl0_10 ),
inference(boolean_simplification,[],[f293]) ).
thf(f295,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK5 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_5
| ~ spl0_10 ),
inference(boolean_simplification,[],[f294]) ).
thf(f296,plain,
( ( $true = $false )
| ~ spl0_5
| ~ spl0_10 ),
inference(backward_demodulation,[],[f289,f295]) ).
thf(f297,plain,
( $false
| ~ spl0_5
| ~ spl0_10 ),
inference(trivial_inequality_removal,[],[f296]) ).
thf(f298,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f297]) ).
thf(f303,plain,
( ( ( ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK1 ) )
| ( cF @ ( cP @ Y0 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ sK6 )
= $true )
| ~ spl0_8 ),
inference(sigma_proxy_clausification,[],[f221]) ).
thf(f304,plain,
( ( $true
= ( ( ( cG @ ( cP @ sK6 @ sK1 ) )
| ( cF @ ( cP @ sK6 @ sK1 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_8 ),
inference(beta-eta_normalization,[],[f303]) ).
thf(f305,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $true )
| ~ spl0_8 ),
inference(and_proxy_clausification,[],[f304]) ).
thf(f306,plain,
( ( ( ( cG @ ( cP @ sK6 @ sK1 ) )
| ( cF @ ( cP @ sK6 @ sK1 ) ) )
= $true )
| ~ spl0_8 ),
inference(and_proxy_clausification,[],[f304]) ).
thf(f309,plain,
( ( ( cF @ ( cP @ sK6 @ sK1 ) )
= $true )
| ( $true
= ( cG @ ( cP @ sK6 @ sK1 ) ) )
| ~ spl0_8 ),
inference(or_proxy_clausification,[],[f306]) ).
thf(f311,definition,
( spl0_11
<=> ( $true
= ( cG @ ( cP @ sK6 @ sK1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
thf(f313,plain,
( ( $true
= ( cG @ ( cP @ sK6 @ sK1 ) ) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f311]) ).
thf(f315,definition,
( spl0_12
<=> ( ( cF @ ( cP @ sK6 @ sK1 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
thf(f317,plain,
( ( ( cF @ ( cP @ sK6 @ sK1 ) )
= $true )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f315]) ).
thf(f318,plain,
( spl0_11
| spl0_12
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f309,f219,f315,f311]) ).
thf(f321,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| spl0_9
| ~ spl0_12 ),
inference(constrained_superposition,[],[f283,f317]) ).
thf(f322,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| spl0_9
| ~ spl0_12 ),
inference(boolean_simplification,[],[f321]) ).
thf(f323,plain,
( ( $true = $false )
| ~ spl0_8
| spl0_9
| ~ spl0_12 ),
inference(backward_demodulation,[],[f305,f322]) ).
thf(f324,plain,
( $false
| ~ spl0_8
| spl0_9
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f323]) ).
thf(f325,plain,
( ~ spl0_8
| spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f324]) ).
thf(f331,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
= $false )
| ~ spl0_6 ),
inference(or_proxy_clausification,[],[f212]) ).
thf(f332,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) )
= $false )
| ~ spl0_6 ),
inference(or_proxy_clausification,[],[f212]) ).
thf(f336,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ X1 )
= $false )
| ~ spl0_6 ),
inference(pi_proxy_clausification,[],[f331]) ).
thf(f337,plain,
( ! [X1: a] :
( ( ( cF @ ( cP @ X1 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ X1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_6 ),
inference(beta-eta_normalization,[],[f336]) ).
thf(f338,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( cG @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ X1 )
= $false )
| ~ spl0_6 ),
inference(pi_proxy_clausification,[],[f332]) ).
thf(f339,plain,
( ! [X1: a] :
( ( ( cG @ ( cP @ X1 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ X1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_6 ),
inference(beta-eta_normalization,[],[f338]) ).
thf(f341,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_6
| ~ spl0_11 ),
inference(constrained_superposition,[],[f339,f313]) ).
thf(f342,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_6
| ~ spl0_11 ),
inference(boolean_simplification,[],[f341]) ).
thf(f343,plain,
( ( $true = $false )
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11 ),
inference(backward_demodulation,[],[f305,f342]) ).
thf(f344,plain,
( $false
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11 ),
inference(trivial_inequality_removal,[],[f343]) ).
thf(f345,plain,
( ~ spl0_6
| ~ spl0_8
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f344]) ).
thf(f348,plain,
( ( $true
= ( ( cF @ ( cP @ sK4 @ sK1 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK4 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_9 ),
inference(beta-eta_normalization,[],[f268]) ).
thf(f352,plain,
( ( $true = $false )
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f348,f337]) ).
thf(f353,plain,
( $false
| ~ spl0_6
| ~ spl0_9 ),
inference(trivial_inequality_removal,[],[f352]) ).
thf(f354,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f353]) ).
thf(f370,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ( $true = $false )
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f256,f332]) ).
thf(f371,plain,
( ( $true
= ( ?? @ a
@ ^ [Y0: a] :
( ( cF @ ( cP @ Y0 @ sK1 ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_6
| ~ spl0_7 ),
inference(trivial_inequality_removal,[],[f370]) ).
thf(f379,plain,
( ( $true = $false )
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f371,f331]) ).
thf(f380,plain,
( $false
| ~ spl0_6
| ~ spl0_7 ),
inference(trivial_inequality_removal,[],[f379]) ).
thf(f381,plain,
( ~ spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f380]) ).
cnf(s6,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f213]) ).
cnf(s7,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f222]) ).
cnf(s8,plain,
( ~ spl0_5
| ~ spl0_8 ),
inference(sat_conversion,[],[f226]) ).
cnf(s9,plain,
( ~ spl0_7
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f265]) ).
cnf(s10,plain,
( ~ spl0_5
| ~ spl0_9 ),
inference(sat_conversion,[],[f279]) ).
cnf(s11,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(sat_conversion,[],[f298]) ).
cnf(s12,plain,
( ~ spl0_8
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f318]) ).
cnf(s13,plain,
( ~ spl0_8
| spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f325]) ).
cnf(s14,plain,
( ~ spl0_6
| ~ spl0_8
| ~ spl0_11 ),
inference(sat_conversion,[],[f345]) ).
cnf(s16,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(sat_conversion,[],[f354]) ).
cnf(s20,plain,
( ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f381]) ).
cnf(s24,plain,
~ spl0_6,
inference(rat,[],[s12,s13,s14,s7,s16,s20]) ).
cnf(s25,plain,
spl0_5,
inference(rat,[],[s6,s24]) ).
cnf(s26,plain,
~ spl0_10,
inference(rat,[],[s11,s25]) ).
cnf(s27,plain,
~ spl0_9,
inference(rat,[],[s10,s25]) ).
cnf(s28,plain,
~ spl0_8,
inference(rat,[],[s8,s25]) ).
cnf(s29,plain,
~ spl0_7,
inference(rat,[],[s9,s26,s27]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s7,s28,s29]) ).
thf(f382,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG290^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n020.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 17:37:35 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.85/0.36 % (1369127)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.85/0.36 % (1369136)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4080490154:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.85/0.36 % (1369138)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.85/0.36 % (1369138)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.85/0.36 % (1369132)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3964618083:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.85/0.36 % (1369133)lrs+10_16_si=on:nwc=1.5:random_seed=1273486191:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.85/0.36 % (1369134)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4101894443:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.85/0.36 % (1369136)Instruction limit reached!
% 0.85/0.36 % (1369136)------------------------------
% 0.85/0.36 % (1369136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.36 % (1369136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.36 % (1369135)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=3648126833: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.85/0.36 % (1369136)CaDiCaL version: 2.1.3
% 0.85/0.36 % (1369136)Termination reason: Instruction limit
% 0.85/0.36 % (1369136)Termination phase: Saturation
% 0.85/0.36 % (1369136)Time elapsed: 0.007 s
% 0.85/0.36 % (1369136)Peak memory usage: 12 MB
% 0.85/0.36 % (1369136)Instructions burned: 25 (million)
% 0.85/0.36 % (1369137)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3802184752:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.85/0.36 % (1369138)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=3738073914:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.85/0.36 % (1369134)Instruction limit reached!
% 0.85/0.36 % (1369134)------------------------------
% 0.85/0.36 % (1369134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.36 % (1369134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.36 % (1369134)CaDiCaL version: 2.1.3
% 0.85/0.36 % (1369134)Termination reason: Instruction limit
% 0.85/0.36 % (1369134)Termination phase: Saturation
% 0.85/0.36 % (1369134)Time elapsed: 0.003 s
% 0.85/0.36 % (1369134)Peak memory usage: 12 MB
% 0.85/0.36 % (1369134)Instructions burned: 5 (million)
% 0.85/0.36 % (1369133)Instruction limit reached!
% 0.85/0.36 % (1369133)------------------------------
% 0.85/0.36 % (1369133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.36 % (1369133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.36 % (1369133)CaDiCaL version: 2.1.3
% 0.85/0.36 % (1369133)Termination reason: Instruction limit
% 0.85/0.36 % (1369133)Termination phase: Saturation
% 0.85/0.36 % (1369133)Time elapsed: 0.011 s
% 0.85/0.36 % (1369133)Peak memory usage: 12 MB
% 0.85/0.36 % (1369133)Instructions burned: 20 (million)
% 0.85/0.36 % (1369145)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2987890075:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.85/0.36 % (1369145)Instruction limit reached!
% 0.85/0.36 % (1369145)------------------------------
% 0.85/0.36 % (1369145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.36 % (1369145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.36 % (1369145)CaDiCaL version: 2.1.3
% 0.85/0.36 % (1369145)Termination reason: Instruction limit
% 0.85/0.36 % (1369145)Termination phase: Saturation
% 0.85/0.36 % (1369145)Time elapsed: 0.001 s
% 0.85/0.36 % (1369145)Peak memory usage: 12 MB
% 0.85/0.36 % (1369145)Instructions burned: 5 (million)
% 0.85/0.36 % (1369147)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3369872468:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.85/0.40 % (1369150)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=334205108:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.85/0.40 % (1369147)Instruction limit reached!
% 0.85/0.40 % (1369147)------------------------------
% 0.85/0.40 % (1369147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (1369147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (1369147)CaDiCaL version: 2.1.3
% 0.85/0.40 % (1369147)Termination reason: Instruction limit
% 0.85/0.40 % (1369147)Termination phase: Saturation
% 0.85/0.40 % (1369147)Time elapsed: 0.003 s
% 0.85/0.40 % (1369147)Peak memory usage: 11 MB
% 0.85/0.40 % (1369147)Instructions burned: 5 (million)
% 0.85/0.40 % (1369150)Instruction limit reached!
% 0.85/0.40 % (1369150)------------------------------
% 0.85/0.40 % (1369150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (1369150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (1369150)CaDiCaL version: 2.1.3
% 0.85/0.40 % (1369150)Termination reason: Instruction limit
% 0.85/0.40 % (1369150)Termination phase: Saturation
% 0.85/0.40 % (1369150)Time elapsed: 0.004 s
% 0.85/0.40 % (1369150)Peak memory usage: 12 MB
% 0.85/0.40 % (1369150)Instructions burned: 13 (million)
% 0.85/0.40 % (1369148)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.85/0.40 % (1369148)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3694324434:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.85/0.40 % (1369137)Instruction limit reached!
% 0.85/0.40 % (1369137)------------------------------
% 0.85/0.40 % (1369137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (1369137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (1369137)CaDiCaL version: 2.1.3
% 0.85/0.40 % (1369137)Termination reason: Instruction limit
% 0.85/0.40 % (1369137)Termination phase: Saturation
% 0.85/0.40 % (1369137)Time elapsed: 0.037 s
% 0.85/0.40 % (1369137)Peak memory usage: 13 MB
% 0.85/0.40 % (1369137)Instructions burned: 75 (million)
% 0.85/0.40 % (1369154)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=1724858501:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.85/0.40 % (1369148)Instruction limit reached!
% 0.85/0.40 % (1369148)------------------------------
% 0.85/0.40 % (1369148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (1369148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (1369148)CaDiCaL version: 2.1.3
% 0.85/0.40 % (1369148)Termination reason: Instruction limit
% 0.85/0.40 % (1369148)Termination phase: Saturation
% 0.85/0.40 % (1369148)Time elapsed: 0.004 s
% 0.85/0.40 % (1369148)Peak memory usage: 11 MB
% 0.85/0.40 % (1369148)Instructions burned: 9 (million)
% 0.85/0.40 % (1369153)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.85/0.40 % (1369153)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.85/0.40 % (1369132)Instruction limit reached!
% 0.85/0.40 % (1369132)------------------------------
% 0.85/0.40 % (1369132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (1369132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (1369132)CaDiCaL version: 2.1.3
% 0.85/0.40 % (1369132)Termination reason: Instruction limit
% 0.85/0.40 % (1369132)Termination phase: Saturation
% 0.85/0.40 % (1369132)Time elapsed: 0.045 s
% 0.85/0.40 % (1369132)Peak memory usage: 13 MB
% 0.85/0.40 % (1369132)Instructions burned: 88 (million)
% 0.85/0.40 % (1369153)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=373844543:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.85/0.40 % (1369156)lrs+10_1_si=on:cs=on:random_seed=2773043606:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.85/0.40 % (1369158)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.85/0.44 % (1369158)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=552273671:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.85/0.44 % (1369153)Instruction limit reached!
% 0.85/0.44 % (1369153)------------------------------
% 0.85/0.44 % (1369153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369153)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369153)Termination reason: Instruction limit
% 0.85/0.44 % (1369153)Termination phase: Saturation
% 0.85/0.44 % (1369153)Time elapsed: 0.015 s
% 0.85/0.44 % (1369153)Peak memory usage: 12 MB
% 0.85/0.44 % (1369153)Instructions burned: 29 (million)
% 0.85/0.44 % (1369156)Instruction limit reached!
% 0.85/0.44 % (1369156)------------------------------
% 0.85/0.44 % (1369156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369156)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369156)Termination reason: Instruction limit
% 0.85/0.44 % (1369156)Termination phase: Saturation
% 0.85/0.44 % (1369156)Time elapsed: 0.005 s
% 0.85/0.44 % (1369156)Peak memory usage: 12 MB
% 0.85/0.44 % (1369156)Instructions burned: 9 (million)
% 0.85/0.44 % (1369159)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2378922608:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.85/0.44 % (1369158)Instruction limit reached!
% 0.85/0.44 % (1369158)------------------------------
% 0.85/0.44 % (1369158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369158)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369158)Termination reason: Instruction limit
% 0.85/0.44 % (1369158)Termination phase: Saturation
% 0.85/0.44 % (1369158)Time elapsed: 0.002 s
% 0.85/0.44 % (1369158)Peak memory usage: 11 MB
% 0.85/0.44 % (1369158)Instructions burned: 4 (million)
% 0.85/0.44 % (1369154)Instruction limit reached!
% 0.85/0.44 % (1369154)------------------------------
% 0.85/0.44 % (1369154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369154)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369154)Termination reason: Instruction limit
% 0.85/0.44 % (1369154)Termination phase: Saturation
% 0.85/0.44 % (1369154)Time elapsed: 0.023 s
% 0.85/0.44 % (1369154)Peak memory usage: 12 MB
% 0.85/0.44 % (1369154)Instructions burned: 88 (million)
% 0.85/0.44 % (1369165)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3172900783:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.85/0.44 % (1369163)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3539302738:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.85/0.44 % (1369159)Instruction limit reached!
% 0.85/0.44 % (1369159)------------------------------
% 0.85/0.44 % (1369159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369159)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369159)Termination reason: Instruction limit
% 0.85/0.44 % (1369159)Termination phase: Saturation
% 0.85/0.44 % (1369159)Time elapsed: 0.019 s
% 0.85/0.44 % (1369159)Peak memory usage: 12 MB
% 0.85/0.44 % (1369159)Instructions burned: 39 (million)
% 0.85/0.44 % (1369165)Instruction limit reached!
% 0.85/0.44 % (1369165)------------------------------
% 0.85/0.44 % (1369165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.44 % (1369165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.44 % (1369165)CaDiCaL version: 2.1.3
% 0.85/0.44 % (1369165)Termination reason: Instruction limit
% 0.85/0.44 % (1369165)Termination phase: Saturation
% 0.85/0.44 % (1369165)Time elapsed: 0.007 s
% 0.85/0.44 % (1369165)Peak memory usage: 12 MB
% 0.85/0.44 % (1369165)Instructions burned: 25 (million)
% 0.85/0.44 % (1369166)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3999843254:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.50/0.51 % (1369167)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2858752779:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.50/0.51 % (1369138)Instruction limit reached!
% 1.50/0.51 % (1369138)------------------------------
% 1.50/0.51 % (1369138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.51 % (1369138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.51 % (1369138)CaDiCaL version: 2.1.3
% 1.50/0.51 % (1369138)Termination reason: Instruction limit
% 1.50/0.51 % (1369138)Termination phase: Saturation
% 1.50/0.51 % (1369138)Time elapsed: 0.090 s
% 1.50/0.51 % (1369138)Peak memory usage: 13 MB
% 1.50/0.51 % (1369138)Instructions burned: 157 (million)
% 1.50/0.51 % (1369166)Instruction limit reached!
% 1.50/0.51 % (1369166)------------------------------
% 1.50/0.51 % (1369166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.51 % (1369166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.51 % (1369166)CaDiCaL version: 2.1.3
% 1.50/0.51 % (1369166)Termination reason: Instruction limit
% 1.50/0.51 % (1369166)Termination phase: Saturation
% 1.50/0.51 % (1369166)Time elapsed: 0.008 s
% 1.50/0.51 % (1369166)Peak memory usage: 12 MB
% 1.50/0.51 % (1369166)Instructions burned: 16 (million)
% 1.50/0.51 % (1369170)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2506264882:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.50/0.51 % (1369170)Instruction limit reached!
% 1.50/0.51 % (1369170)------------------------------
% 1.50/0.51 % (1369170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.51 % (1369170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.51 % (1369170)CaDiCaL version: 2.1.3
% 1.50/0.51 % (1369170)Termination reason: Instruction limit
% 1.50/0.51 % (1369170)Termination phase: Saturation
% 1.50/0.51 % (1369170)Time elapsed: 0.005 s
% 1.50/0.51 % (1369170)Peak memory usage: 12 MB
% 1.50/0.51 % (1369170)Instructions burned: 17 (million)
% 1.50/0.51 % (1369171)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4042407024: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)
% 1.50/0.51 % (1369171)Instruction limit reached!
% 1.50/0.51 % (1369171)------------------------------
% 1.50/0.51 % (1369171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.51 % (1369171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.51 % (1369171)CaDiCaL version: 2.1.3
% 1.50/0.51 % (1369171)Termination reason: Instruction limit
% 1.50/0.51 % (1369171)Termination phase: Saturation
% 1.50/0.51 % (1369171)Time elapsed: 0.003 s
% 1.50/0.51 % (1369171)Peak memory usage: 11 MB
% 1.50/0.51 % (1369171)Instructions burned: 5 (million)
% 1.50/0.51 % (1369177)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3144892257:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.50/0.51 % (1369174)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=859066607:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.50/0.51 % (1369176)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3025694999:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.50/0.51 % (1369179)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
% 1.50/0.51 % (1369179)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.50/0.51 % (1369176)Instruction limit reached!
% 1.50/0.51 % (1369176)------------------------------
% 1.50/0.51 % (1369176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.51 % (1369176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.51 % (1369176)CaDiCaL version: 2.1.3
% 1.50/0.51 % (1369176)Termination reason: Instruction limit
% 1.50/0.51 % (1369176)Termination phase: Saturation
% 1.50/0.51 % (1369176)Time elapsed: 0.011 s
% 1.50/0.51 % (1369176)Peak memory usage: 11 MB
% 1.50/0.51 % (1369176)Instructions burned: 23 (million)
% 2.19/0.57 % (1369179)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=46652437:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.19/0.57 % (1369174)Instruction limit reached!
% 2.19/0.57 % (1369174)------------------------------
% 2.19/0.57 % (1369174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.57 % (1369174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.57 % (1369174)CaDiCaL version: 2.1.3
% 2.19/0.57 % (1369174)Termination reason: Instruction limit
% 2.19/0.57 % (1369174)Termination phase: Saturation
% 2.19/0.57 % (1369174)Time elapsed: 0.015 s
% 2.19/0.57 % (1369174)Peak memory usage: 12 MB
% 2.19/0.57 % (1369174)Instructions burned: 27 (million)
% 2.19/0.57 % (1369177)Instruction limit reached!
% 2.19/0.57 % (1369177)------------------------------
% 2.19/0.57 % (1369177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.57 % (1369177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.57 % (1369177)CaDiCaL version: 2.1.3
% 2.19/0.57 % (1369177)Termination reason: Instruction limit
% 2.19/0.57 % (1369177)Termination phase: Saturation
% 2.19/0.57 % (1369177)Time elapsed: 0.016 s
% 2.19/0.57 % (1369177)Peak memory usage: 12 MB
% 2.19/0.57 % (1369177)Instructions burned: 63 (million)
% 2.19/0.57 % (1369179)Instruction limit reached!
% 2.19/0.57 % (1369179)------------------------------
% 2.19/0.57 % (1369179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.57 % (1369179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.57 % (1369179)CaDiCaL version: 2.1.3
% 2.19/0.57 % (1369179)Termination reason: Instruction limit
% 2.19/0.57 % (1369179)Termination phase: Saturation
% 2.19/0.57 % (1369179)Time elapsed: 0.008 s
% 2.19/0.57 % (1369179)Peak memory usage: 12 MB
% 2.19/0.57 % (1369179)Instructions burned: 16 (million)
% 2.19/0.57 % (1369192)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=121504218:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.19/0.57 % (1369189)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.19/0.57 % (1369192)Instruction limit reached!
% 2.19/0.57 % (1369192)------------------------------
% 2.19/0.57 % (1369192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.57 % (1369192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.57 % (1369192)CaDiCaL version: 2.1.3
% 2.19/0.57 % (1369192)Termination reason: Instruction limit
% 2.19/0.57 % (1369192)Termination phase: Saturation
% 2.19/0.57 % (1369192)Time elapsed: 0.003 s
% 2.19/0.57 % (1369192)Peak memory usage: 12 MB
% 2.19/0.57 % (1369192)Instructions burned: 10 (million)
% 2.19/0.57 % (1369189)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=2633676271:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.19/0.57 % (1369191)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=1502484113:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.19/0.57 % (1369189)Instruction limit reached!
% 2.19/0.57 % (1369189)------------------------------
% 2.19/0.57 % (1369189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.57 % (1369189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.57 % (1369189)CaDiCaL version: 2.1.3
% 2.19/0.57 % (1369189)Termination reason: Instruction limit
% 2.19/0.57 % (1369189)Termination phase: Saturation
% 2.19/0.57 % (1369189)Time elapsed: 0.005 s
% 2.19/0.57 % (1369189)Peak memory usage: 12 MB
% 2.19/0.57 % (1369189)Instructions burned: 9 (million)
% 2.19/0.57 % (1369198)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2905722815:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.19/0.57 % (1369195)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3227549477:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.19/0.57 % (1369198)Instruction limit reached!
% 2.19/0.57 % (1369198)------------------------------
% 2.19/0.57 % (1369198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369198)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369198)Termination reason: Instruction limit
% 2.19/0.62 % (1369198)Termination phase: Saturation
% 2.19/0.62 % (1369198)Time elapsed: 0.007 s
% 2.19/0.62 % (1369198)Peak memory usage: 12 MB
% 2.19/0.62 % (1369198)Instructions burned: 23 (million)
% 2.19/0.62 % (1369191)Instruction limit reached!
% 2.19/0.62 % (1369191)------------------------------
% 2.19/0.62 % (1369191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369191)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369191)Termination reason: Instruction limit
% 2.19/0.62 % (1369191)Termination phase: Saturation
% 2.19/0.62 % (1369191)Time elapsed: 0.015 s
% 2.19/0.62 % (1369191)Peak memory usage: 12 MB
% 2.19/0.62 % (1369191)Instructions burned: 34 (million)
% 2.19/0.62 % (1369195)Instruction limit reached!
% 2.19/0.62 % (1369195)------------------------------
% 2.19/0.62 % (1369195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369195)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369195)Termination reason: Instruction limit
% 2.19/0.62 % (1369195)Termination phase: Saturation
% 2.19/0.62 % (1369195)Time elapsed: 0.012 s
% 2.19/0.62 % (1369195)Peak memory usage: 11 MB
% 2.19/0.62 % (1369195)Instructions burned: 25 (million)
% 2.19/0.62 % (1369210)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1775613731:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.19/0.62 % (1369205)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3278467867:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.19/0.62 % (1369208)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3112682356:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.19/0.62 % (1369211)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2310726143:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.19/0.62 % (1369211)Instruction limit reached!
% 2.19/0.62 % (1369211)------------------------------
% 2.19/0.62 % (1369211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369211)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369211)Termination reason: Instruction limit
% 2.19/0.62 % (1369211)Termination phase: Saturation
% 2.19/0.62 % (1369211)Time elapsed: 0.022 s
% 2.19/0.62 % (1369211)Peak memory usage: 12 MB
% 2.19/0.62 % (1369211)Instructions burned: 42 (million)
% 2.19/0.62 % (1369163)Instruction limit reached!
% 2.19/0.62 % (1369163)------------------------------
% 2.19/0.62 % (1369163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369163)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369163)Termination reason: Instruction limit
% 2.19/0.62 % (1369163)Termination phase: Saturation
% 2.19/0.62 % (1369163)Time elapsed: 0.136 s
% 2.19/0.62 % (1369163)Peak memory usage: 14 MB
% 2.19/0.62 % (1369163)Instructions burned: 251 (million)
% 2.19/0.62 % (1369228)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.19/0.62 % (1369210)Instruction limit reached!
% 2.19/0.62 % (1369210)------------------------------
% 2.19/0.62 % (1369210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.62 % (1369210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.62 % (1369210)CaDiCaL version: 2.1.3
% 2.19/0.62 % (1369210)Termination reason: Instruction limit
% 2.19/0.62 % (1369210)Termination phase: Saturation
% 2.19/0.62 % (1369210)Time elapsed: 0.056 s
% 2.19/0.62 % (1369210)Peak memory usage: 14 MB
% 2.19/0.62 % (1369210)Instructions burned: 195 (million)
% 2.19/0.62 % (1369228)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2297035326:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.19/0.62 % (1369228)Instruction limit reached!
% 2.19/0.62 % (1369228)------------------------------
% 2.19/0.62 % (1369228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/0.73 % (1369228)CaDiCaL version: 2.1.3
% 2.81/0.73 % (1369228)Termination reason: Instruction limit
% 2.81/0.73 % (1369228)Termination phase: Saturation
% 2.81/0.73 % (1369228)Time elapsed: 0.004 s
% 2.81/0.73 % (1369228)Peak memory usage: 11 MB
% 2.81/0.73 % (1369228)Instructions burned: 8 (million)
% 2.81/0.73 % (1369237)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=296397069:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.81/0.73 % (1369233)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3658953803:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.81/0.73 % (1369239)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.81/0.73 % (1369239)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1536268319:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.81/0.73 % (1369208)Instruction limit reached!
% 2.81/0.73 % (1369208)------------------------------
% 2.81/0.73 % (1369208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/0.73 % (1369208)CaDiCaL version: 2.1.3
% 2.81/0.73 % (1369208)Termination reason: Instruction limit
% 2.81/0.73 % (1369208)Termination phase: Saturation
% 2.81/0.73 % (1369208)Time elapsed: 0.076 s
% 2.81/0.73 % (1369208)Peak memory usage: 13 MB
% 2.81/0.73 % (1369208)Instructions burned: 149 (million)
% 2.81/0.73 % (1369239)Instruction limit reached!
% 2.81/0.73 % (1369239)------------------------------
% 2.81/0.73 % (1369239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/0.73 % (1369239)CaDiCaL version: 2.1.3
% 2.81/0.73 % (1369239)Termination reason: Instruction limit
% 2.81/0.73 % (1369239)Termination phase: Saturation
% 2.81/0.73 % (1369239)Time elapsed: 0.004 s
% 2.81/0.73 % (1369239)Peak memory usage: 11 MB
% 2.81/0.73 % (1369239)Instructions burned: 7 (million)
% 2.81/0.73 % (1369167)Instruction limit reached!
% 2.81/0.73 % (1369167)------------------------------
% 2.81/0.73 % (1369167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/0.73 % (1369167)CaDiCaL version: 2.1.3
% 2.81/0.73 % (1369167)Termination reason: Instruction limit
% 2.81/0.73 % (1369167)Termination phase: Saturation
% 2.81/0.73 % (1369167)Time elapsed: 0.173 s
% 2.81/0.73 % (1369167)Peak memory usage: 14 MB
% 2.81/0.73 % (1369167)Instructions burned: 327 (million)
% 2.81/0.73 % (1369249)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3878814380:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.81/0.73 % (1369251)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3417522568:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.81/0.73 % (1369253)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=2216699019:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.81/0.73 % (1369249)Instruction limit reached!
% 2.81/0.73 % (1369249)------------------------------
% 2.81/0.73 % (1369249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/0.73 % (1369249)CaDiCaL version: 2.1.3
% 2.81/0.73 % (1369249)Termination reason: Instruction limit
% 2.81/0.73 % (1369249)Termination phase: Saturation
% 2.81/0.73 % (1369249)Time elapsed: 0.013 s
% 2.81/0.73 % (1369249)Peak memory usage: 12 MB
% 2.81/0.73 % (1369249)Instructions burned: 23 (million)
% 2.81/0.73 % (1369237)Instruction limit reached!
% 2.81/0.73 % (1369237)------------------------------
% 2.81/0.73 % (1369237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.81/0.73 % (1369237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369237)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369237)Termination reason: Instruction limit
% 3.31/0.85 % (1369237)Termination phase: Saturation
% 3.31/0.85 % (1369237)Time elapsed: 0.048 s
% 3.31/0.85 % (1369237)Peak memory usage: 13 MB
% 3.31/0.85 % (1369237)Instructions burned: 173 (million)
% 3.31/0.85 % (1369251)Instruction limit reached!
% 3.31/0.85 % (1369251)------------------------------
% 3.31/0.85 % (1369251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.85 % (1369251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369251)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369251)Termination reason: Instruction limit
% 3.31/0.85 % (1369251)Termination phase: Saturation
% 3.31/0.85 % (1369251)Time elapsed: 0.011 s
% 3.31/0.85 % (1369251)Peak memory usage: 13 MB
% 3.31/0.85 % (1369251)Instructions burned: 19 (million)
% 3.31/0.85 % (1369266)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=2127048700:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.31/0.85 % (1369265)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=2181000874:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.31/0.85 % (1369266)Instruction limit reached!
% 3.31/0.85 % (1369266)------------------------------
% 3.31/0.85 % (1369266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.85 % (1369266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369266)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369266)Termination reason: Instruction limit
% 3.31/0.85 % (1369266)Termination phase: Saturation
% 3.31/0.85 % (1369266)Time elapsed: 0.013 s
% 3.31/0.85 % (1369266)Peak memory usage: 12 MB
% 3.31/0.85 % (1369266)Instructions burned: 49 (million)
% 3.31/0.85 % (1369268)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=289169731:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.31/0.85 % (1369281)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3233910135:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.31/0.85 % (1369281)Instruction limit reached!
% 3.31/0.85 % (1369281)------------------------------
% 3.31/0.85 % (1369281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.85 % (1369281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369281)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369281)Termination reason: Instruction limit
% 3.31/0.85 % (1369281)Termination phase: Saturation
% 3.31/0.85 % (1369281)Time elapsed: 0.007 s
% 3.31/0.85 % (1369281)Peak memory usage: 12 MB
% 3.31/0.85 % (1369281)Instructions burned: 22 (million)
% 3.31/0.85 % (1369233)Instruction limit reached!
% 3.31/0.85 % (1369233)------------------------------
% 3.31/0.85 % (1369233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.85 % (1369233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369233)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369233)Termination reason: Instruction limit
% 3.31/0.85 % (1369233)Termination phase: Saturation
% 3.31/0.85 % (1369233)Time elapsed: 0.091 s
% 3.31/0.85 % (1369233)Peak memory usage: 13 MB
% 3.31/0.85 % (1369233)Instructions burned: 182 (million)
% 3.31/0.85 % (1369288)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.31/0.85 % (1369288)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=430209413:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.31/0.85 % (1369135)Instruction limit reached!
% 3.31/0.85 % (1369135)------------------------------
% 3.31/0.85 % (1369135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.85 % (1369135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.85 % (1369135)CaDiCaL version: 2.1.3
% 3.31/0.85 % (1369135)Termination reason: Instruction limit
% 3.31/0.85 % (1369135)Termination phase: Saturation
% 3.31/0.85 % (1369135)Time elapsed: 0.346 s
% 3.86/1.04 % (1369135)Peak memory usage: 15 MB
% 3.86/1.04 % (1369135)Instructions burned: 634 (million)
% 3.86/1.04 % (1369290)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4187451672:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.86/1.04 % (1369290)Instruction limit reached!
% 3.86/1.04 % (1369290)------------------------------
% 3.86/1.04 % (1369290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.04 % (1369290)CaDiCaL version: 2.1.3
% 3.86/1.04 % (1369290)Termination reason: Instruction limit
% 3.86/1.04 % (1369290)Termination phase: Saturation
% 3.86/1.04 % (1369290)Time elapsed: 0.010 s
% 3.86/1.04 % (1369290)Peak memory usage: 12 MB
% 3.86/1.04 % (1369290)Instructions burned: 13 (million)
% 3.86/1.04 % (1369294)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=2621181152:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.86/1.04 % (1369299)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3521476289:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.86/1.04 % (1369294)Instruction limit reached!
% 3.86/1.04 % (1369294)------------------------------
% 3.86/1.04 % (1369294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.04 % (1369294)CaDiCaL version: 2.1.3
% 3.86/1.04 % (1369294)Termination reason: Instruction limit
% 3.86/1.04 % (1369294)Termination phase: Saturation
% 3.86/1.04 % (1369294)Time elapsed: 0.030 s
% 3.86/1.04 % (1369294)Peak memory usage: 13 MB
% 3.86/1.04 % (1369294)Instructions burned: 66 (million)
% 3.86/1.04 % (1369288)Instruction limit reached!
% 3.86/1.04 % (1369288)------------------------------
% 3.86/1.04 % (1369288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.04 % (1369288)CaDiCaL version: 2.1.3
% 3.86/1.04 % (1369288)Termination reason: Instruction limit
% 3.86/1.04 % (1369288)Termination phase: Saturation
% 3.86/1.04 % (1369288)Time elapsed: 0.057 s
% 3.86/1.04 % (1369288)Peak memory usage: 13 MB
% 3.86/1.04 % (1369288)Instructions burned: 203 (million)
% 3.86/1.04 % (1369299)Instruction limit reached!
% 3.86/1.04 % (1369299)------------------------------
% 3.86/1.04 % (1369299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.04 % (1369299)CaDiCaL version: 2.1.3
% 3.86/1.04 % (1369299)Termination reason: Instruction limit
% 3.86/1.04 % (1369299)Termination phase: Saturation
% 3.86/1.04 % (1369299)Time elapsed: 0.030 s
% 3.86/1.04 % (1369299)Peak memory usage: 12 MB
% 3.86/1.04 % (1369299)Instructions burned: 53 (million)
% 3.86/1.04 % (1369314)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3465607847:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.86/1.04 % (1369316)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3817535679:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.86/1.04 % (1369314)Refutation not found, incomplete strategy
% 3.86/1.04 % (1369314)------------------------------
% 3.86/1.04 % (1369314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.04 % (1369314)CaDiCaL version: 2.1.3
% 3.86/1.04 % (1369314)Termination reason: Refutation not found, incomplete strategy
% 3.86/1.04 % (1369314)Time elapsed: 0.011 s
% 3.86/1.04 % (1369314)Peak memory usage: 12 MB
% 3.86/1.04 % (1369314)Instructions burned: 21 (million)
% 3.86/1.04 % (1369317)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=4215249775:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.86/1.04 % (1369314)------------------------------
% 3.86/1.04 % (1369314)------------------------------
% 3.86/1.04 % (1369317)Instruction limit reached!
% 3.86/1.04 % (1369317)------------------------------
% 3.86/1.04 % (1369317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/1.04 % (1369317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369325)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4178469449:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 6.59/1.24 % (1369317)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369317)Termination reason: Instruction limit
% 6.59/1.24 % (1369317)Termination phase: Saturation
% 6.59/1.24 % (1369317)Time elapsed: 0.022 s
% 6.59/1.24 % (1369317)Peak memory usage: 12 MB
% 6.59/1.24 % (1369317)Instructions burned: 37 (million)
% 6.59/1.24 % (1369253)Instruction limit reached!
% 6.59/1.24 % (1369253)------------------------------
% 6.59/1.24 % (1369253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.59/1.24 % (1369253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369253)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369253)Termination reason: Instruction limit
% 6.59/1.24 % (1369253)Termination phase: Saturation
% 6.59/1.24 % (1369253)Time elapsed: 0.176 s
% 6.59/1.24 % (1369253)Peak memory usage: 14 MB
% 6.59/1.24 % (1369253)Instructions burned: 317 (million)
% 6.59/1.24 % (1369316)Instruction limit reached!
% 6.59/1.24 % (1369316)------------------------------
% 6.59/1.24 % (1369316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.59/1.24 % (1369316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369316)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369316)Termination reason: Instruction limit
% 6.59/1.24 % (1369316)Termination phase: Saturation
% 6.59/1.24 % (1369316)Time elapsed: 0.039 s
% 6.59/1.24 % (1369316)Peak memory usage: 13 MB
% 6.59/1.24 % (1369316)Instructions burned: 137 (million)
% 6.59/1.24 % (1369336)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.59/1.24 % (1369336)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2064368655:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 6.59/1.24 % (1369338)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=340065733:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 6.59/1.24 % (1369340)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4121233725:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 6.59/1.24 % (1369325)Instruction limit reached!
% 6.59/1.24 % (1369325)------------------------------
% 6.59/1.24 % (1369325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.59/1.24 % (1369325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369325)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369325)Termination reason: Instruction limit
% 6.59/1.24 % (1369325)Termination phase: Saturation
% 6.59/1.24 % (1369325)Time elapsed: 0.034 s
% 6.59/1.24 % (1369325)Peak memory usage: 12 MB
% 6.59/1.24 % (1369325)Instructions burned: 68 (million)
% 6.59/1.24 % (1369349)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2729725341:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 6.59/1.24 % (1369340)Instruction limit reached!
% 6.59/1.24 % (1369340)------------------------------
% 6.59/1.24 % (1369340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.59/1.24 % (1369340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369340)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369340)Termination reason: Instruction limit
% 6.59/1.24 % (1369340)Termination phase: Saturation
% 6.59/1.24 % (1369340)Time elapsed: 0.044 s
% 6.59/1.24 % (1369340)Peak memory usage: 12 MB
% 6.59/1.24 % (1369340)Instructions burned: 96 (million)
% 6.59/1.24 % (1369362)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=90923903:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 6.59/1.24 % (1369336)Instruction limit reached!
% 6.59/1.24 % (1369336)------------------------------
% 6.59/1.24 % (1369336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.59/1.24 % (1369336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.24 % (1369336)CaDiCaL version: 2.1.3
% 6.59/1.24 % (1369336)Termination reason: Instruction limit
% 6.59/1.24 % (1369336)Termination phase: Saturation
% 6.59/1.24 % (1369336)Time elapsed: 0.082 s
% 6.59/1.24 % (1369336)Peak memory usage: 14 MB
% 6.59/1.24 % (1369336)Instructions burned: 180 (million)
% 6.59/1.24 % (1369268)Instruction limit reached!
% 6.59/1.24 % (1369268)------------------------------
% 7.07/1.36 % (1369268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369268)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369268)Termination reason: Instruction limit
% 7.07/1.36 % (1369268)Termination phase: Saturation
% 7.07/1.36 % (1369268)Time elapsed: 0.251 s
% 7.07/1.36 % (1369268)Peak memory usage: 15 MB
% 7.07/1.36 % (1369268)Instructions burned: 481 (million)
% 7.07/1.36 % (1369371)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=758106980:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 7.07/1.36 % (1369374)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=619887255:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 7.07/1.36 % (1369374)Instruction limit reached!
% 7.07/1.36 % (1369374)------------------------------
% 7.07/1.36 % (1369374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369374)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369374)Termination reason: Instruction limit
% 7.07/1.36 % (1369374)Termination phase: Saturation
% 7.07/1.36 % (1369374)Time elapsed: 0.045 s
% 7.07/1.36 % (1369374)Peak memory usage: 13 MB
% 7.07/1.36 % (1369374)Instructions burned: 132 (million)
% 7.07/1.36 % (1369393)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2103835859:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 7.07/1.36 % (1369338)Instruction limit reached!
% 7.07/1.36 % (1369338)------------------------------
% 7.07/1.36 % (1369338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369338)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369338)Termination reason: Instruction limit
% 7.07/1.36 % (1369338)Termination phase: Saturation
% 7.07/1.36 % (1369338)Time elapsed: 0.167 s
% 7.07/1.36 % (1369338)Peak memory usage: 14 MB
% 7.07/1.36 % (1369338)Instructions burned: 246 (million)
% 7.07/1.36 % (1369405)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2575832418:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 7.07/1.36 % (1369393)Instruction limit reached!
% 7.07/1.36 % (1369393)------------------------------
% 7.07/1.36 % (1369393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369393)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369393)Termination reason: Instruction limit
% 7.07/1.36 % (1369393)Termination phase: Saturation
% 7.07/1.36 % (1369393)Time elapsed: 0.041 s
% 7.07/1.36 % (1369393)Peak memory usage: 12 MB
% 7.07/1.36 % (1369393)Instructions burned: 45 (million)
% 7.07/1.36 % (1369405)Refutation not found, incomplete strategy
% 7.07/1.36 % (1369405)------------------------------
% 7.07/1.36 % (1369405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369405)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369405)Termination reason: Refutation not found, incomplete strategy
% 7.07/1.36 % (1369405)Time elapsed: 0.034 s
% 7.07/1.36 % (1369405)Peak memory usage: 13 MB
% 7.07/1.36 % (1369405)Instructions burned: 76 (million)
% 7.07/1.36 % (1369405)------------------------------
% 7.07/1.36 % (1369405)------------------------------
% 7.07/1.36 % (1369418)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=920189759:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 7.07/1.36 % (1369415)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1417224304:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 7.07/1.36 % (1369418)Instruction limit reached!
% 7.07/1.36 % (1369418)------------------------------
% 7.07/1.36 % (1369418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.36 % (1369418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.36 % (1369418)CaDiCaL version: 2.1.3
% 7.07/1.36 % (1369418)Termination reason: Instruction limit
% 7.07/1.36 % (1369418)Termination phase: Saturation
% 7.07/1.36 % (1369418)Time elapsed: 0.044 s
% 7.37/1.41 % (1369418)Peak memory usage: 13 MB
% 7.37/1.41 % (1369418)Instructions burned: 96 (million)
% 7.37/1.41 % (1369349)Instruction limit reached!
% 7.37/1.41 % (1369349)------------------------------
% 7.37/1.41 % (1369349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369349)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369349)Termination reason: Instruction limit
% 7.37/1.41 % (1369349)Termination phase: Saturation
% 7.37/1.41 % (1369349)Time elapsed: 0.289 s
% 7.37/1.41 % (1369349)Peak memory usage: 14 MB
% 7.37/1.41 % (1369349)Instructions burned: 427 (million)
% 7.37/1.41 % (1369432)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=1046868736:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 7.37/1.41 % (1369440)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=3525863623:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2991 on theBenchmark for (2991ds/105Mi)
% 7.37/1.41 % (1369432)Instruction limit reached!
% 7.37/1.41 % (1369432)------------------------------
% 7.37/1.41 % (1369432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369432)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369432)Termination reason: Instruction limit
% 7.37/1.41 % (1369432)Termination phase: Saturation
% 7.37/1.41 % (1369432)Time elapsed: 0.049 s
% 7.37/1.41 % (1369432)Peak memory usage: 12 MB
% 7.37/1.41 % (1369432)Instructions burned: 65 (million)
% 7.37/1.41 % (1369265)Instruction limit reached!
% 7.37/1.41 % (1369265)------------------------------
% 7.37/1.41 % (1369265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369265)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369265)Termination reason: Instruction limit
% 7.37/1.41 % (1369265)Termination phase: Saturation
% 7.37/1.41 % (1369265)Time elapsed: 0.577 s
% 7.37/1.41 % (1369265)Peak memory usage: 16 MB
% 7.37/1.41 % (1369265)Instructions burned: 854 (million)
% 7.37/1.41 % (1369454)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=313047459:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 7.37/1.41 % (1369460)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3623120654:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/375Mi)
% 7.37/1.41 % (1369440)Instruction limit reached!
% 7.37/1.41 % (1369440)------------------------------
% 7.37/1.41 % (1369440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369440)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369440)Termination reason: Instruction limit
% 7.37/1.41 % (1369440)Termination phase: Saturation
% 7.37/1.41 % (1369440)Time elapsed: 0.095 s
% 7.37/1.41 % (1369440)Peak memory usage: 13 MB
% 7.37/1.41 % (1369440)Instructions burned: 106 (million)
% 7.37/1.41 % (1369205)Instruction limit reached!
% 7.37/1.41 % (1369205)------------------------------
% 7.37/1.41 % (1369205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369205)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369205)Termination reason: Instruction limit
% 7.37/1.41 % (1369205)Termination phase: Saturation
% 7.37/1.41 % (1369205)Time elapsed: 0.777 s
% 7.37/1.41 % (1369205)Peak memory usage: 15 MB
% 7.37/1.41 % (1369205)Instructions burned: 1240 (million)
% 7.37/1.41 % (1369371)Instruction limit reached!
% 7.37/1.41 % (1369371)------------------------------
% 7.37/1.41 % (1369371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369371)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369371)Termination reason: Instruction limit
% 7.37/1.41 % (1369371)Termination phase: Saturation
% 7.37/1.41 % (1369371)Time elapsed: 0.389 s
% 7.37/1.41 % (1369371)Peak memory usage: 15 MB
% 7.37/1.41 % (1369371)Instructions burned: 515 (million)
% 7.37/1.41 % (1369470)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=748666563:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/495Mi)
% 7.37/1.41 % (1369415)Instruction limit reached!
% 7.37/1.41 % (1369415)------------------------------
% 7.37/1.41 % (1369415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369415)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369415)Termination reason: Instruction limit
% 7.37/1.41 % (1369415)Termination phase: Saturation
% 7.37/1.41 % (1369415)Time elapsed: 0.243 s
% 7.37/1.41 % (1369415)Peak memory usage: 14 MB
% 7.37/1.41 % (1369415)Instructions burned: 452 (million)
% 7.37/1.41 % (1369472)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=3385921020:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 7.37/1.41 % (1369477)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1066085774:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 7.37/1.41 % (1369475)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1240951925:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/91Mi)
% 7.37/1.41 % (1369472)Instruction limit reached!
% 7.37/1.41 % (1369472)------------------------------
% 7.37/1.41 % (1369472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369472)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369472)Termination reason: Instruction limit
% 7.37/1.41 % (1369472)Termination phase: Saturation
% 7.37/1.41 % (1369472)Time elapsed: 0.025 s
% 7.37/1.41 % (1369472)Peak memory usage: 12 MB
% 7.37/1.41 % (1369472)Instructions burned: 35 (million)
% 7.37/1.41 % (1369477)Instruction limit reached!
% 7.37/1.41 % (1369477)------------------------------
% 7.37/1.41 % (1369477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369477)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369477)Termination reason: Instruction limit
% 7.37/1.41 % (1369477)Termination phase: Saturation
% 7.37/1.41 % (1369477)Time elapsed: 0.031 s
% 7.37/1.41 % (1369477)Peak memory usage: 13 MB
% 7.37/1.41 % (1369477)Instructions burned: 67 (million)
% 7.37/1.41 % (1369486)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2395851081:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2989 on theBenchmark for (2989ds/22Mi)
% 7.37/1.41 % (1369486)Instruction limit reached!
% 7.37/1.41 % (1369486)------------------------------
% 7.37/1.41 % (1369486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369486)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369486)Termination reason: Instruction limit
% 7.37/1.41 % (1369486)Termination phase: Saturation
% 7.37/1.41 % (1369486)Time elapsed: 0.014 s
% 7.37/1.41 % (1369486)Peak memory usage: 12 MB
% 7.37/1.41 % (1369486)Instructions burned: 23 (million)
% 7.37/1.41 % (1369488)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=443815191:i=338:bd=all:ins=4:rtra=on_2989 on theBenchmark for (2989ds/338Mi)
% 7.37/1.41 % (1369495)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1736773859:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/28Mi)
% 7.37/1.41 % (1369475)Instruction limit reached!
% 7.37/1.41 % (1369475)------------------------------
% 7.37/1.41 % (1369475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369475)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369475)Termination reason: Instruction limit
% 7.37/1.41 % (1369475)Termination phase: Saturation
% 7.37/1.41 % (1369475)Time elapsed: 0.084 s
% 7.37/1.41 % (1369475)Peak memory usage: 13 MB
% 7.37/1.41 % (1369475)Instructions burned: 91 (million)
% 7.37/1.41 % (1369495)Instruction limit reached!
% 7.37/1.41 % (1369495)------------------------------
% 7.37/1.41 % (1369495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.41 % (1369495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.41 % (1369495)CaDiCaL version: 2.1.3
% 7.37/1.41 % (1369495)Termination reason: Instruction limit
% 7.37/1.41 % (1369495)Termination phase: Saturation
% 7.37/1.41 % (1369495)Time elapsed: 0.016 s
% 7.37/1.41 % (1369495)Peak memory usage: 12 MB
% 7.37/1.41 % (1369495)Instructions burned: 28 (million)
% 7.37/1.41 % (1369504)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=1227383424:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/340Mi)
% 7.37/1.41 % (1369503)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.37/1.41 % (1369503)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1935941466:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/137Mi)
% 7.37/1.41 % (1369488) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1369127-1369488"...
% 7.37/1.41 % (1369488)...printing done.
% 7.37/1.41 % (1369488)Refutation found. Thanks to Tanya!
% 7.37/1.41 % SZS status Theorem for theBenchmark
% 7.37/1.41 % SZS output start Proof for theBenchmark
% See solution above
% 7.37/1.42 % (1369488)------------------------------
% 7.37/1.42 % (1369488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.37/1.42 % (1369488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.42 % (1369488)CaDiCaL version: 2.1.3
% 7.37/1.42 % (1369488)Termination reason: Refutation
% 7.37/1.42 % (1369488)Time elapsed: 0.074 s
% 7.37/1.42 % (1369488)Peak memory usage: 14 MB
% 7.37/1.42 % (1369488)Instructions burned: 82 (million)
% 7.37/1.42 % (1369127)Success in time 1.168 s
% 7.37/1.42 % Vampire exiting
%------------------------------------------------------------------------------