%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV148^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:37:54 AM UTC 2026
% Result : Theorem 15.80s 2.99s
% Output : Refutation 15.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 15
% Syntax : Number of formulae : 243 ( 48 unt; 0 typ; 14 def)
% Number of atoms : 2003 ( 199 equ; 0 cnn)
% Maximal formula atoms : 4 ( 8 avg)
% Number of connectives : 5621 ( 244 ~; 350 |; 420 &;3246 @)
% ( 14 <=>; 639 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 366 ( 366 >; 0 *; 0 +; 0 <<)
% Number of symbols : 61 ( 57 usr; 34 con; 0-4 aty)
% ( 708 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 850 ( 0 sgn 112 !; 0 ?; 850 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_1,type,
vNOT: $o > $o ).
thf(func_def_2,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_3,type,
vIMP: $o > $o > $o ).
thf(func_def_4,type,
vAND: $o > $o > $o ).
thf(func_def_5,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_6,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_7,type,
vOR: $o > $o > $o ).
thf(func_def_8,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_9,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_11,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_12,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
db8:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
db9:
!>[X0: $tType] : X0 ).
thf(func_def_15,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_16,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_19,type,
sK0: a > a > $o ).
thf(func_def_20,type,
sK1: a ).
thf(func_def_21,type,
sK2: a ).
thf(func_def_22,type,
sK3: a > a > $o ).
thf(func_def_23,type,
sK4: a > $o ).
thf(func_def_25,type,
sK6: a ).
thf(func_def_26,type,
sK7: a ).
thf(func_def_27,type,
sK8: a > $o ).
thf(func_def_28,type,
sK9: a ).
thf(func_def_29,type,
sK10: a > $o ).
thf(func_def_30,type,
sK11: a > $o ).
thf(func_def_31,type,
sK12: a ).
thf(func_def_32,type,
sK13: a ).
thf(func_def_33,type,
sK14: a > $o ).
thf(func_def_34,type,
sK15: a ).
thf(func_def_35,type,
sK16: a > $o ).
thf(func_def_36,type,
sK17: a ).
thf(func_def_37,type,
sK18: a ).
thf(func_def_38,type,
sK19: a ).
thf(func_def_39,type,
sK20: a > $o ).
thf(func_def_40,type,
sK21: a ).
thf(func_def_41,type,
sK22: a ).
thf(func_def_42,type,
sK23: a ).
thf(func_def_43,type,
sK24: a ).
thf(func_def_44,type,
sK25: a ).
thf(func_def_45,type,
sK26: a ).
thf(f1,conjecture,
! [X0: a > a > $o,X2: a,X3: a,X1: a > a > $o] :
( ! [X4: a > $o] :
( ( ! [X5: a] :
( ( ! [X6: a > $o] :
( ( ! [X7: a] :
( ( X0 @ X2 @ X7 )
=> ( X6 @ X7 ) )
& ! [X8: a,X9: a] :
( ( ( X6 @ X8 )
& ( X0 @ X8 @ X9 ) )
=> ( X6 @ X9 ) ) )
=> ( X6 @ X5 ) )
| ! [X6: a > $o] :
( ( ! [X8: a,X9: a] :
( ( ( X1 @ X8 @ X9 )
& ( X6 @ X8 ) )
=> ( X6 @ X9 ) )
& ! [X7: a] :
( ( X1 @ X2 @ X7 )
=> ( X6 @ X7 ) ) )
=> ( X6 @ X5 ) ) )
=> ( X4 @ X5 ) )
& ! [X9: a,X8: a] :
( ( ( ! [X6: a > $o] :
( ( ! [X11: a,X10: a] :
( ( ( X6 @ X10 )
& ( X1 @ X10 @ X11 ) )
=> ( X6 @ X11 ) )
& ! [X5: a] :
( ( X1 @ X8 @ X5 )
=> ( X6 @ X5 ) ) )
=> ( X6 @ X9 ) )
| ! [X6: a > $o] :
( ( ! [X11: a,X10: a] :
( ( ( X0 @ X10 @ X11 )
& ( X6 @ X10 ) )
=> ( X6 @ X11 ) )
& ! [X5: a] :
( ( X0 @ X8 @ X5 )
=> ( X6 @ X5 ) ) )
=> ( X6 @ X9 ) ) )
& ( X4 @ X8 ) )
=> ( X4 @ X9 ) ) )
=> ( X4 @ X3 ) )
=> ! [X4: a > $o] :
( ( ! [X5: a] :
( ( ( X1 @ X2 @ X5 )
| ( X0 @ X2 @ X5 ) )
=> ( X4 @ X5 ) )
& ! [X9: a,X8: a] :
( ( ( X4 @ X8 )
& ( ( X0 @ X8 @ X9 )
| ( X1 @ X8 @ X9 ) ) )
=> ( X4 @ X9 ) ) )
=> ( X4 @ X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM251C_pme) ).
thf(f2,negated_conjecture,
~ ! [X0: a > a > $o,X2: a,X3: a,X1: a > a > $o] :
( ! [X4: a > $o] :
( ( ! [X5: a] :
( ( ! [X6: a > $o] :
( ( ! [X7: a] :
( ( X0 @ X2 @ X7 )
=> ( X6 @ X7 ) )
& ! [X8: a,X9: a] :
( ( ( X6 @ X8 )
& ( X0 @ X8 @ X9 ) )
=> ( X6 @ X9 ) ) )
=> ( X6 @ X5 ) )
| ! [X6: a > $o] :
( ( ! [X8: a,X9: a] :
( ( ( X1 @ X8 @ X9 )
& ( X6 @ X8 ) )
=> ( X6 @ X9 ) )
& ! [X7: a] :
( ( X1 @ X2 @ X7 )
=> ( X6 @ X7 ) ) )
=> ( X6 @ X5 ) ) )
=> ( X4 @ X5 ) )
& ! [X9: a,X8: a] :
( ( ( ! [X6: a > $o] :
( ( ! [X11: a,X10: a] :
( ( ( X6 @ X10 )
& ( X1 @ X10 @ X11 ) )
=> ( X6 @ X11 ) )
& ! [X5: a] :
( ( X1 @ X8 @ X5 )
=> ( X6 @ X5 ) ) )
=> ( X6 @ X9 ) )
| ! [X6: a > $o] :
( ( ! [X11: a,X10: a] :
( ( ( X0 @ X10 @ X11 )
& ( X6 @ X10 ) )
=> ( X6 @ X11 ) )
& ! [X5: a] :
( ( X0 @ X8 @ X5 )
=> ( X6 @ X5 ) ) )
=> ( X6 @ X9 ) ) )
& ( X4 @ X8 ) )
=> ( X4 @ X9 ) ) )
=> ( X4 @ X3 ) )
=> ! [X4: a > $o] :
( ( ! [X5: a] :
( ( ( X1 @ X2 @ X5 )
| ( X0 @ X2 @ X5 ) )
=> ( X4 @ X5 ) )
& ! [X9: a,X8: a] :
( ( ( X4 @ X8 )
& ( ( X0 @ X8 @ X9 )
| ( X1 @ X8 @ X9 ) ) )
=> ( X4 @ X9 ) ) )
=> ( X4 @ X3 ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ! [X0: a > a > $o,X1: a,X2: a,X3: a > a > $o] :
( ! [X4: a > $o] :
( ( ! [X5: a] :
( ( ! [X6: a > $o] :
( ( ! [X7: a] :
( ( X0 @ X1 @ X7 )
=> ( X6 @ X7 ) )
& ! [X8: a,X9: a] :
( ( ( X6 @ X8 )
& ( X0 @ X8 @ X9 ) )
=> ( X6 @ X9 ) ) )
=> ( X6 @ X5 ) )
| ! [X10: a > $o] :
( ( ! [X11: a,X12: a] :
( ( ( X3 @ X11 @ X12 )
& ( X10 @ X11 ) )
=> ( X10 @ X12 ) )
& ! [X13: a] :
( ( X3 @ X1 @ X13 )
=> ( X10 @ X13 ) ) )
=> ( X10 @ X5 ) ) )
=> ( X4 @ X5 ) )
& ! [X14: a,X15: a] :
( ( ( ! [X16: a > $o] :
( ( ! [X17: a,X18: a] :
( ( ( X16 @ X18 )
& ( X3 @ X18 @ X17 ) )
=> ( X16 @ X17 ) )
& ! [X19: a] :
( ( X3 @ X15 @ X19 )
=> ( X16 @ X19 ) ) )
=> ( X16 @ X14 ) )
| ! [X20: a > $o] :
( ( ! [X21: a,X22: a] :
( ( ( X0 @ X22 @ X21 )
& ( X20 @ X22 ) )
=> ( X20 @ X21 ) )
& ! [X23: a] :
( ( X0 @ X15 @ X23 )
=> ( X20 @ X23 ) ) )
=> ( X20 @ X14 ) ) )
& ( X4 @ X15 ) )
=> ( X4 @ X14 ) ) )
=> ( X4 @ X2 ) )
=> ! [X24: a > $o] :
( ( ! [X25: a] :
( ( ( X3 @ X1 @ X25 )
| ( X0 @ X1 @ X25 ) )
=> ( X24 @ X25 ) )
& ! [X26: a,X27: a] :
( ( ( X24 @ X27 )
& ( ( X0 @ X27 @ X26 )
| ( X3 @ X27 @ X26 ) ) )
=> ( X24 @ X26 ) ) )
=> ( X24 @ X2 ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
( $true
= ( ~ ( !! @ ( a > a > $o )
@ ^ [Y0: a > a > $o] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( !! @ ( a > a > $o )
@ ^ [Y3: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y3 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y7 @ Y8 )
& ( Y3 @ Y8 @ Y9 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y0 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y0 @ Y8 @ Y9 )
& ( Y7 @ Y8 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) ) ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y0 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y8 )
& ( Y0 @ Y8 @ Y7 ) )
=> ( Y6 @ Y7 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y3 @ Y8 @ Y7 )
& ( Y6 @ Y8 ) )
=> ( Y6 @ Y7 ) ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( ( Y3 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) ) )
=> ( Y6 @ Y5 ) ) ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( ( Y0 @ Y5 @ Y6 )
| ( Y3 @ Y5 @ Y6 ) )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y2 @ Y5 )
| ( Y0 @ Y2 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( $true
= ( ~ ( !! @ ( a > a > $o )
@ ^ [Y0: a > a > $o] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( !! @ ( a > a > $o )
@ ^ [Y3: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y3 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y7 @ Y8 )
& ( Y3 @ Y8 @ Y9 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y0 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y0 @ Y8 @ Y9 )
& ( Y7 @ Y8 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) ) ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y0 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y8 )
& ( Y0 @ Y8 @ Y7 ) )
=> ( Y6 @ Y7 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y3 @ Y8 @ Y7 )
& ( Y6 @ Y8 ) )
=> ( Y6 @ Y7 ) ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( ( Y3 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) ) )
=> ( Y6 @ Y5 ) ) ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( ( Y0 @ Y5 @ Y6 )
| ( Y3 @ Y5 @ Y6 ) )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y2 @ Y5 )
| ( Y0 @ Y2 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f4]) ).
thf(f8,plain,
( $false
= ( !! @ ( a > a > $o )
@ ^ [Y0: a > a > $o] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( !! @ ( a > a > $o )
@ ^ [Y3: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y3 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y7 @ Y8 )
& ( Y3 @ Y8 @ Y9 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y0 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y0 @ Y8 @ Y9 )
& ( Y7 @ Y8 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) ) ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y0 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y8 )
& ( Y0 @ Y8 @ Y7 ) )
=> ( Y6 @ Y7 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y3 @ Y8 @ Y7 )
& ( Y6 @ Y8 ) )
=> ( Y6 @ Y7 ) ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( ( Y3 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) ) )
=> ( Y6 @ Y5 ) ) ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( ( Y0 @ Y5 @ Y6 )
| ( Y3 @ Y5 @ Y6 ) )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y2 @ Y5 )
| ( Y0 @ Y2 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f5]) ).
thf(f9,plain,
( $false
= ( ^ [Y0: a > a > $o] :
( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( !! @ ( a > a > $o )
@ ^ [Y3: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y3 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y7 @ Y8 )
& ( Y3 @ Y8 @ Y9 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y7: a > $o] :
( ( ( !! @ a
@ ^ [Y8: a] :
( ( Y0 @ Y5 @ Y8 )
=> ( Y7 @ Y8 ) ) )
& ( !! @ a
@ ^ [Y8: a] :
( !! @ a
@ ^ [Y9: a] :
( ( ( Y0 @ Y8 @ Y9 )
& ( Y7 @ Y8 ) )
=> ( Y7 @ Y9 ) ) ) ) )
=> ( Y7 @ Y6 ) ) ) ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y0 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y8 )
& ( Y0 @ Y8 @ Y7 ) )
=> ( Y6 @ Y7 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y3 @ Y8 @ Y7 )
& ( Y6 @ Y8 ) )
=> ( Y6 @ Y7 ) ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( ( Y3 @ Y2 @ Y7 )
=> ( Y6 @ Y7 ) ) ) )
=> ( Y6 @ Y5 ) ) ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( ( Y0 @ Y5 @ Y6 )
| ( Y3 @ Y5 @ Y6 ) )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y2 @ Y5 )
| ( Y0 @ Y2 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y1 ) ) ) ) ) ) )
@ sK0 ) ),
inference(sigma_proxy_clausification,[],[f8]) ).
thf(f11,plain,
( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( !! @ ( a > a > $o )
@ ^ [Y2: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y4 )
& ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y2 @ Y4 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y7 )
& ( Y2 @ Y7 @ Y8 ) )
=> ( Y6 @ Y8 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( sK0 @ Y4 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( sK0 @ Y7 @ Y8 )
& ( Y6 @ Y7 ) )
=> ( Y6 @ Y8 ) ) ) ) )
=> ( Y6 @ Y5 ) ) ) ) )
=> ( Y3 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( sK0 @ Y1 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y5 @ Y7 )
& ( sK0 @ Y7 @ Y6 ) )
=> ( Y5 @ Y6 ) ) ) ) )
=> ( Y5 @ Y4 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y2 @ Y7 @ Y6 )
& ( Y5 @ Y7 ) )
=> ( Y5 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( ( Y2 @ Y1 @ Y6 )
=> ( Y5 @ Y6 ) ) ) )
=> ( Y5 @ Y4 ) ) ) )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y0 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( ( sK0 @ Y4 @ Y5 )
| ( Y2 @ Y4 @ Y5 ) )
& ( Y3 @ Y4 ) )
=> ( Y3 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y1 @ Y4 )
| ( sK0 @ Y1 @ Y4 ) )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y0 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f9]) ).
thf(f13,plain,
( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( !! @ ( a > a > $o )
@ ^ [Y2: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y4 )
& ( ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( Y2 @ Y4 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( Y6 @ Y7 )
& ( Y2 @ Y7 @ Y8 ) )
=> ( Y6 @ Y8 ) ) ) ) )
=> ( Y6 @ Y5 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y6: a > $o] :
( ( ( !! @ a
@ ^ [Y7: a] :
( ( sK0 @ Y4 @ Y7 )
=> ( Y6 @ Y7 ) ) )
& ( !! @ a
@ ^ [Y7: a] :
( !! @ a
@ ^ [Y8: a] :
( ( ( sK0 @ Y7 @ Y8 )
& ( Y6 @ Y7 ) )
=> ( Y6 @ Y8 ) ) ) ) )
=> ( Y6 @ Y5 ) ) ) ) )
=> ( Y3 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( sK0 @ Y1 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y5 @ Y7 )
& ( sK0 @ Y7 @ Y6 ) )
=> ( Y5 @ Y6 ) ) ) ) )
=> ( Y5 @ Y4 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y2 @ Y7 @ Y6 )
& ( Y5 @ Y7 ) )
=> ( Y5 @ Y6 ) ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( ( Y2 @ Y1 @ Y6 )
=> ( Y5 @ Y6 ) ) ) )
=> ( Y5 @ Y4 ) ) ) )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y0 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( ( sK0 @ Y4 @ Y5 )
| ( Y2 @ Y4 @ Y5 ) )
& ( Y3 @ Y4 ) )
=> ( Y3 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y1 @ Y4 )
| ( sK0 @ Y1 @ Y4 ) )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y0 ) ) ) ) ) )
@ sK1 ) ),
inference(sigma_proxy_clausification,[],[f11]) ).
thf(f14,plain,
( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ ( a > a > $o )
@ ^ [Y1: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( Y1 @ Y3 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y5 @ Y6 )
& ( Y1 @ Y6 @ Y7 ) )
=> ( Y5 @ Y7 ) ) ) ) )
=> ( Y5 @ Y4 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( sK0 @ Y3 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( sK0 @ Y6 @ Y7 )
& ( Y5 @ Y6 ) )
=> ( Y5 @ Y7 ) ) ) ) )
=> ( Y5 @ Y4 ) ) ) ) )
=> ( Y2 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( sK0 @ Y0 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y6 )
& ( sK0 @ Y6 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) ) )
=> ( Y4 @ Y3 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y1 @ Y6 @ Y5 )
& ( Y4 @ Y6 ) )
=> ( Y4 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( Y1 @ Y0 @ Y5 )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y3 ) ) ) )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ sK1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( ( sK0 @ Y3 @ Y4 )
| ( Y1 @ Y3 @ Y4 ) )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y0 @ Y3 )
| ( sK0 @ Y0 @ Y3 ) )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ sK1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f13]) ).
thf(f15,plain,
( $false
= ( ^ [Y0: a] :
( !! @ ( a > a > $o )
@ ^ [Y1: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( Y1 @ Y3 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( Y5 @ Y6 )
& ( Y1 @ Y6 @ Y7 ) )
=> ( Y5 @ Y7 ) ) ) ) )
=> ( Y5 @ Y4 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y5: a > $o] :
( ( ( !! @ a
@ ^ [Y6: a] :
( ( sK0 @ Y3 @ Y6 )
=> ( Y5 @ Y6 ) ) )
& ( !! @ a
@ ^ [Y6: a] :
( !! @ a
@ ^ [Y7: a] :
( ( ( sK0 @ Y6 @ Y7 )
& ( Y5 @ Y6 ) )
=> ( Y5 @ Y7 ) ) ) ) )
=> ( Y5 @ Y4 ) ) ) ) )
=> ( Y2 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( sK0 @ Y0 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y6 )
& ( sK0 @ Y6 @ Y5 ) )
=> ( Y4 @ Y5 ) ) ) ) )
=> ( Y4 @ Y3 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y1 @ Y6 @ Y5 )
& ( Y4 @ Y6 ) )
=> ( Y4 @ Y5 ) ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( ( Y1 @ Y0 @ Y5 )
=> ( Y4 @ Y5 ) ) ) )
=> ( Y4 @ Y3 ) ) ) )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ sK1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( ( sK0 @ Y3 @ Y4 )
| ( Y1 @ Y3 @ Y4 ) )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y0 @ Y3 )
| ( sK0 @ Y0 @ Y3 ) )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ sK1 ) ) ) ) )
@ sK2 ) ),
inference(sigma_proxy_clausification,[],[f14]) ).
thf(f16,plain,
( $false
= ( !! @ ( a > a > $o )
@ ^ [Y0: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y2 )
& ( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( Y0 @ Y2 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( Y0 @ Y5 @ Y6 ) )
=> ( Y4 @ Y6 ) ) ) ) )
=> ( Y4 @ Y3 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( sK0 @ Y2 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( sK0 @ Y5 @ Y6 )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) ) )
=> ( Y4 @ Y3 ) ) ) ) )
=> ( Y1 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK0 @ sK2 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y5 )
& ( sK0 @ Y5 @ Y4 ) )
=> ( Y3 @ Y4 ) ) ) ) )
=> ( Y3 @ Y2 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y0 @ Y5 @ Y4 )
& ( Y3 @ Y5 ) )
=> ( Y3 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y0 @ sK2 @ Y4 )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ sK1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( ( sK0 @ Y2 @ Y3 )
| ( Y0 @ Y2 @ Y3 ) )
& ( Y1 @ Y2 ) )
=> ( Y1 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ sK2 @ Y2 )
| ( sK0 @ sK2 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ sK1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f15]) ).
thf(f17,plain,
( ( ^ [Y0: a > a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y2 )
& ( ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( Y0 @ Y2 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( Y4 @ Y5 )
& ( Y0 @ Y5 @ Y6 ) )
=> ( Y4 @ Y6 ) ) ) ) )
=> ( Y4 @ Y3 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y4: a > $o] :
( ( ( !! @ a
@ ^ [Y5: a] :
( ( sK0 @ Y2 @ Y5 )
=> ( Y4 @ Y5 ) ) )
& ( !! @ a
@ ^ [Y5: a] :
( !! @ a
@ ^ [Y6: a] :
( ( ( sK0 @ Y5 @ Y6 )
& ( Y4 @ Y5 ) )
=> ( Y4 @ Y6 ) ) ) ) )
=> ( Y4 @ Y3 ) ) ) ) )
=> ( Y1 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK0 @ sK2 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y5 )
& ( sK0 @ Y5 @ Y4 ) )
=> ( Y3 @ Y4 ) ) ) ) )
=> ( Y3 @ Y2 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y0 @ Y5 @ Y4 )
& ( Y3 @ Y5 ) )
=> ( Y3 @ Y4 ) ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y0 @ sK2 @ Y4 )
=> ( Y3 @ Y4 ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ sK1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( ( sK0 @ Y2 @ Y3 )
| ( Y0 @ Y2 @ Y3 ) )
& ( Y1 @ Y2 ) )
=> ( Y1 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ sK2 @ Y2 )
| ( sK0 @ sK2 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ sK1 ) ) ) )
@ sK3 )
= $false ),
inference(sigma_proxy_clausification,[],[f16]) ).
thf(f18,plain,
( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK3 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y4 )
& ( sK3 @ Y4 @ Y5 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK0 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( sK0 @ Y4 @ Y5 )
& ( Y3 @ Y4 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y4 )
& ( sK0 @ Y4 @ Y3 ) )
=> ( Y2 @ Y3 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK3 @ Y4 @ Y3 )
& ( Y2 @ Y4 ) )
=> ( Y2 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) ) )
=> ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( ( sK0 @ Y1 @ Y2 )
| ( sK3 @ Y1 @ Y2 ) )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ sK2 @ Y1 )
| ( sK0 @ sK2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f17]) ).
thf(f19,plain,
( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( ( sK0 @ Y1 @ Y2 )
| ( sK3 @ Y1 @ Y2 ) )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ sK2 @ Y1 )
| ( sK0 @ sK2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) ) ) ),
inference(imp_proxy_clausification,[],[f18]) ).
thf(f20,plain,
( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK3 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y4 )
& ( sK3 @ Y4 @ Y5 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK0 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( sK0 @ Y4 @ Y5 )
& ( Y3 @ Y4 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y4 )
& ( sK0 @ Y4 @ Y3 ) )
=> ( Y2 @ Y3 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK3 @ Y4 @ Y3 )
& ( Y2 @ Y4 ) )
=> ( Y2 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) ) ) ),
inference(imp_proxy_clausification,[],[f18]) ).
thf(f21,plain,
( $false
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( ( sK0 @ Y1 @ Y2 )
| ( sK3 @ Y1 @ Y2 ) )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ sK2 @ Y1 )
| ( sK0 @ sK2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) )
@ sK4 ) ),
inference(sigma_proxy_clausification,[],[f19]) ).
thf(f22,plain,
( $false
= ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( ( sK0 @ Y0 @ Y1 )
| ( sK3 @ Y0 @ Y1 ) )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( sK3 @ sK2 @ Y0 )
| ( sK0 @ sK2 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) )
=> ( sK4 @ sK1 ) ) ),
inference(beta-eta_normalization,[],[f21]) ).
thf(f23,plain,
( $false
= ( sK4 @ sK1 ) ),
inference(imp_proxy_clausification,[],[f22]) ).
thf(f24,plain,
( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( ( sK0 @ Y0 @ Y1 )
| ( sK3 @ Y0 @ Y1 ) )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( sK3 @ sK2 @ Y0 )
| ( sK0 @ sK2 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f22]) ).
thf(f29,plain,
! [X1: a > $o] :
( $true
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK3 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( Y3 @ Y4 )
& ( sK3 @ Y4 @ Y5 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( sK0 @ Y1 @ Y4 )
=> ( Y3 @ Y4 ) ) )
& ( !! @ a
@ ^ [Y4: a] :
( !! @ a
@ ^ [Y5: a] :
( ( ( sK0 @ Y4 @ Y5 )
& ( Y3 @ Y4 ) )
=> ( Y3 @ Y5 ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) ) )
=> ( Y0 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y4 )
& ( sK0 @ Y4 @ Y3 ) )
=> ( Y2 @ Y3 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK3 @ Y4 @ Y3 )
& ( Y2 @ Y4 ) )
=> ( Y2 @ Y3 ) ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ sK2 @ Y3 )
=> ( Y2 @ Y3 ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK1 ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f20]) ).
thf(f30,plain,
! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( X1 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( X1 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( X1 @ Y0 ) ) ) )
=> ( X1 @ sK1 ) )
= $true ),
inference(beta-eta_normalization,[],[f29]) ).
thf(f31,plain,
( ( !! @ a
@ ^ [Y0: a] :
( ( ( sK3 @ sK2 @ Y0 )
| ( sK0 @ sK2 @ Y0 ) )
=> ( sK4 @ Y0 ) ) )
= $true ),
inference(and_proxy_clausification,[],[f24]) ).
thf(f32,plain,
( $true
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( ( sK0 @ Y0 @ Y1 )
| ( sK3 @ Y0 @ Y1 ) )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) ),
inference(and_proxy_clausification,[],[f24]) ).
thf(f34,plain,
( $true
= ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) )
=> $false ) ),
inference(superposition,[],[f30,f23]) ).
thf(f35,plain,
( $true
= ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) ) ) ),
inference(boolean_simplification,[],[f34]) ).
thf(f36,plain,
! [X1: a] :
( $true
= ( ^ [Y0: a] :
( ( ( sK3 @ sK2 @ Y0 )
| ( sK0 @ sK2 @ Y0 ) )
=> ( sK4 @ Y0 ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f31]) ).
thf(f37,plain,
! [X1: a] :
( $true
= ( ( ( sK3 @ sK2 @ X1 )
| ( sK0 @ sK2 @ X1 ) )
=> ( sK4 @ X1 ) ) ),
inference(beta-eta_normalization,[],[f36]) ).
thf(f42,plain,
! [X1: a] :
( $true
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( ( sK0 @ Y0 @ Y1 )
| ( sK3 @ Y0 @ Y1 ) )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f32]) ).
thf(f43,plain,
! [X1: a] :
( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( ( ( sK0 @ X1 @ Y0 )
| ( sK3 @ X1 @ Y0 ) )
& ( sK4 @ X1 ) )
=> ( sK4 @ Y0 ) ) ) ),
inference(beta-eta_normalization,[],[f42]) ).
thf(f50,plain,
! [X2: a,X1: a] :
( $true
= ( ^ [Y0: a] :
( ( ( ( sK0 @ X1 @ Y0 )
| ( sK3 @ X1 @ Y0 ) )
& ( sK4 @ X1 ) )
=> ( sK4 @ Y0 ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f43]) ).
thf(f51,plain,
! [X2: a,X1: a] :
( ( ( ( ( sK0 @ X1 @ X2 )
| ( sK3 @ X1 @ X2 ) )
& ( sK4 @ X1 ) )
=> ( sK4 @ X2 ) )
= $true ),
inference(beta-eta_normalization,[],[f50]) ).
thf(f92,plain,
( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f35]) ).
thf(f107,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) )
| ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f92]) ).
thf(f109,definition,
( spl5_1
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
thf(f111,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f109]) ).
thf(f113,definition,
( spl5_2
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
thf(f115,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) ) ) )
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f113]) ).
thf(f116,plain,
( spl5_1
| spl5_2 ),
inference(avatar_split_clause,[],[f107,f113,f109]) ).
thf(f132,plain,
( ( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK3 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( Y2 @ Y3 )
& ( sK3 @ Y3 @ Y4 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( sK0 @ Y0 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( !! @ a
@ ^ [Y3: a] :
( !! @ a
@ ^ [Y4: a] :
( ( ( sK0 @ Y3 @ Y4 )
& ( Y2 @ Y3 ) )
=> ( Y2 @ Y4 ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) ) )
=> ( sK4 @ Y1 ) ) )
@ sK6 ) )
| ~ spl5_2 ),
inference(sigma_proxy_clausification,[],[f115]) ).
thf(f133,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( sK4 @ sK6 )
& ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK6 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y2 )
& ( sK3 @ Y2 @ Y3 ) )
=> ( Y1 @ Y3 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK6 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK0 @ Y2 @ Y3 )
& ( Y1 @ Y2 ) )
=> ( Y1 @ Y3 ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) ) )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_2 ),
inference(beta-eta_normalization,[],[f132]) ).
thf(f134,plain,
( ( $false
= ( ^ [Y0: a] :
( ( ( sK4 @ sK6 )
& ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK6 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y2 )
& ( sK3 @ Y2 @ Y3 ) )
=> ( Y1 @ Y3 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK6 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK0 @ Y2 @ Y3 )
& ( Y1 @ Y2 ) )
=> ( Y1 @ Y3 ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) ) )
=> ( sK4 @ Y0 ) )
@ sK7 ) )
| ~ spl5_2 ),
inference(sigma_proxy_clausification,[],[f133]) ).
thf(f135,plain,
( ( $false
= ( ( ( sK4 @ sK6 )
& ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) ) )
=> ( sK4 @ sK7 ) ) )
| ~ spl5_2 ),
inference(beta-eta_normalization,[],[f134]) ).
thf(f136,plain,
( ( $false
= ( sK4 @ sK7 ) )
| ~ spl5_2 ),
inference(imp_proxy_clausification,[],[f135]) ).
thf(f137,plain,
( ( $true
= ( ( sK4 @ sK6 )
& ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) ) ) )
| ~ spl5_2 ),
inference(imp_proxy_clausification,[],[f135]) ).
thf(f154,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) )
= $true )
| ~ spl5_2 ),
inference(and_proxy_clausification,[],[f137]) ).
thf(f155,plain,
( ( ( sK4 @ sK6 )
= $true )
| ~ spl5_2 ),
inference(and_proxy_clausification,[],[f137]) ).
thf(f162,plain,
( ! [X0: a] :
( ( ( ( ( sK0 @ sK6 @ X0 )
| ( sK3 @ sK6 @ X0 ) )
& $true )
=> ( sK4 @ X0 ) )
= $true )
| ~ spl5_2 ),
inference(superposition,[],[f51,f155]) ).
thf(f249,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
= $true )
| ( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) )
| ~ spl5_2 ),
inference(or_proxy_clausification,[],[f154]) ).
thf(f251,definition,
( spl5_3
<=> ( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
thf(f253,plain,
( ( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) ) )
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f251]) ).
thf(f255,definition,
( spl5_4
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
thf(f257,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) ) )
= $true )
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f255]) ).
thf(f258,plain,
( spl5_3
| spl5_4
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f249,f113,f255,f251]) ).
thf(f269,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y1 )
& ( sK3 @ Y1 @ Y2 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) )
@ X1 )
= $true )
| ~ spl5_3 ),
inference(pi_proxy_clausification,[],[f253]) ).
thf(f270,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( X1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( X1 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( X1 @ Y1 ) ) ) ) )
=> ( X1 @ sK7 ) )
= $true )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f269]) ).
thf(f290,plain,
( ( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl5_2
| ~ spl5_3 ),
inference(superposition,[],[f270,f136]) ).
thf(f293,plain,
( ( $true
= ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) ) ) )
| ~ spl5_2
| ~ spl5_3 ),
inference(boolean_simplification,[],[f290]) ).
thf(f410,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) ) )
| ~ spl5_2
| ~ spl5_3 ),
inference(not_proxy_clausification,[],[f293]) ).
thf(f412,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) )
| ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_2
| ~ spl5_3 ),
inference(and_proxy_clausification,[],[f410]) ).
thf(f414,definition,
( spl5_5
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
thf(f416,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_5 ),
inference(avatar_component_clause,[],[f414]) ).
thf(f418,definition,
( spl5_6
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).
thf(f420,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) ) ) )
| ~ spl5_6 ),
inference(avatar_component_clause,[],[f418]) ).
thf(f421,plain,
( spl5_5
| spl5_6
| ~ spl5_2
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f412,f251,f113,f418,f414]) ).
thf(f430,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK6 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK0 @ Y1 @ Y2 )
& ( Y0 @ Y1 ) )
=> ( Y0 @ Y2 ) ) ) ) )
=> ( Y0 @ sK7 ) )
@ X1 )
= $true )
| ~ spl5_4 ),
inference(pi_proxy_clausification,[],[f257]) ).
thf(f431,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( X1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( X1 @ Y0 ) )
=> ( X1 @ Y1 ) ) ) ) )
=> ( X1 @ sK7 ) )
= $true )
| ~ spl5_4 ),
inference(beta-eta_normalization,[],[f430]) ).
thf(f435,plain,
( ( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl5_2
| ~ spl5_4 ),
inference(superposition,[],[f431,f136]) ).
thf(f441,plain,
( ( $true
= ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) ) ) )
| ~ spl5_2
| ~ spl5_4 ),
inference(boolean_simplification,[],[f435]) ).
thf(f450,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) ) )
| ~ spl5_2
| ~ spl5_4 ),
inference(not_proxy_clausification,[],[f441]) ).
thf(f460,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) )
| ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_2
| ~ spl5_4 ),
inference(and_proxy_clausification,[],[f450]) ).
thf(f462,definition,
( spl5_7
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition]) ).
thf(f463,plain,
( ( $false
!= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) )
| spl5_7 ),
inference(avatar_component_clause,[],[f462]) ).
thf(f464,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) ) ) )
| ~ spl5_7 ),
inference(avatar_component_clause,[],[f462]) ).
thf(f466,definition,
( spl5_8
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition]) ).
thf(f468,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_8 ),
inference(avatar_component_clause,[],[f466]) ).
thf(f471,plain,
( ( $false
= ( ^ [Y0: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( sK0 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( Y1 @ Y3 )
& ( sK0 @ Y3 @ Y2 ) )
=> ( Y1 @ Y2 ) ) ) ) )
=> ( Y1 @ Y0 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( !! @ a
@ ^ [Y3: a] :
( ( ( sK3 @ Y3 @ Y2 )
& ( Y1 @ Y3 ) )
=> ( Y1 @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( sK3 @ sK2 @ Y2 )
=> ( Y1 @ Y2 ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( sK4 @ Y0 ) )
@ sK9 ) )
| ~ spl5_1 ),
inference(sigma_proxy_clausification,[],[f111]) ).
thf(f472,plain,
( ( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) ) ) )
=> ( sK4 @ sK9 ) )
= $false )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f471]) ).
thf(f481,plain,
( ( $false
= ( sK4 @ sK9 ) )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f472]) ).
thf(f482,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) ) )
| ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) ) ) )
= $true )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f472]) ).
thf(f538,definition,
( spl5_9
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition]) ).
thf(f540,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true )
| ~ spl5_9 ),
inference(avatar_component_clause,[],[f538]) ).
thf(f542,definition,
( spl5_10
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition]) ).
thf(f544,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true )
| ~ spl5_10 ),
inference(avatar_component_clause,[],[f542]) ).
thf(f553,plain,
( ! [X0: a] :
( ( ( ( sK0 @ sK6 @ X0 )
| ( sK3 @ sK6 @ X0 ) )
=> ( sK4 @ X0 ) )
= $true )
| ~ spl5_2 ),
inference(boolean_simplification,[],[f162]) ).
thf(f703,plain,
( spl5_8
| spl5_7
| ~ spl5_2
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f460,f255,f113,f462,f466]) ).
thf(f1064,plain,
( ( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) )
@ sK12 ) )
| ~ spl5_7 ),
inference(sigma_proxy_clausification,[],[f464]) ).
thf(f1065,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( sK0 @ sK12 @ Y0 )
& ( sK4 @ sK12 ) )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_7 ),
inference(beta-eta_normalization,[],[f1064]) ).
thf(f1080,plain,
( ( $false
= ( ^ [Y0: a] :
( ( ( sK0 @ sK12 @ Y0 )
& ( sK4 @ sK12 ) )
=> ( sK4 @ Y0 ) )
@ sK13 ) )
| ~ spl5_7 ),
inference(sigma_proxy_clausification,[],[f1065]) ).
thf(f1081,plain,
( ( $false
= ( ( ( sK0 @ sK12 @ sK13 )
& ( sK4 @ sK12 ) )
=> ( sK4 @ sK13 ) ) )
| ~ spl5_7 ),
inference(beta-eta_normalization,[],[f1080]) ).
thf(f1082,plain,
( ( $false
= ( sK4 @ sK13 ) )
| ~ spl5_7 ),
inference(imp_proxy_clausification,[],[f1081]) ).
thf(f1083,plain,
( ( ( ( sK0 @ sK12 @ sK13 )
& ( sK4 @ sK12 ) )
= $true )
| ~ spl5_7 ),
inference(imp_proxy_clausification,[],[f1081]) ).
thf(f1113,plain,
( ( ( sK4 @ sK12 )
= $true )
| ~ spl5_7 ),
inference(and_proxy_clausification,[],[f1083]) ).
thf(f1114,plain,
( ( ( sK0 @ sK12 @ sK13 )
= $true )
| ~ spl5_7 ),
inference(and_proxy_clausification,[],[f1083]) ).
thf(f1149,plain,
( ( ( ( ( $true
| ( sK3 @ sK12 @ sK13 ) )
& ( sK4 @ sK12 ) )
=> ( sK4 @ sK13 ) )
= $true )
| ~ spl5_7 ),
inference(superposition,[],[f51,f1114]) ).
thf(f1150,plain,
( ( ( ( $true
& ( sK4 @ sK12 ) )
=> ( sK4 @ sK13 ) )
= $true )
| ~ spl5_7 ),
inference(boolean_simplification,[],[f1149]) ).
thf(f1151,plain,
( ( ( ( sK4 @ sK12 )
=> ( sK4 @ sK13 ) )
= $true )
| ~ spl5_7 ),
inference(boolean_simplification,[],[f1150]) ).
thf(f1154,plain,
( ( $true
= ( $true
=> ( sK4 @ sK13 ) ) )
| ~ spl5_7 ),
inference(forward_demodulation,[],[f1151,f1113]) ).
thf(f1155,plain,
( ( ( sK4 @ sK13 )
= $true )
| ~ spl5_7 ),
inference(boolean_simplification,[],[f1154]) ).
thf(f1158,plain,
( ( $false = $true )
| ~ spl5_7 ),
inference(forward_demodulation,[],[f1155,f1082]) ).
thf(f1159,plain,
( $false
| ~ spl5_7 ),
inference(trivial_inequality_removal,[],[f1158]) ).
thf(f1160,plain,
~ spl5_7,
inference(avatar_contradiction_clause,[],[f1159]) ).
thf(f1268,plain,
( ( $false
= ( ^ [Y0: a] :
( ( sK3 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) )
@ sK15 ) )
| ~ spl5_5 ),
inference(sigma_proxy_clausification,[],[f416]) ).
thf(f1269,plain,
( ( $false
= ( ( sK3 @ sK6 @ sK15 )
=> ( sK4 @ sK15 ) ) )
| ~ spl5_5 ),
inference(beta-eta_normalization,[],[f1268]) ).
thf(f1278,plain,
( ( $false
= ( sK4 @ sK15 ) )
| ~ spl5_5 ),
inference(imp_proxy_clausification,[],[f1269]) ).
thf(f1279,plain,
( ( ( sK3 @ sK6 @ sK15 )
= $true )
| ~ spl5_5 ),
inference(imp_proxy_clausification,[],[f1269]) ).
thf(f1288,plain,
( ( $true
= ( ( ( sK0 @ sK6 @ sK15 )
| ( sK3 @ sK6 @ sK15 ) )
=> $false ) )
| ~ spl5_2
| ~ spl5_5 ),
inference(superposition,[],[f553,f1278]) ).
thf(f1295,plain,
( ( ( ~ ( ( sK0 @ sK6 @ sK15 )
| ( sK3 @ sK6 @ sK15 ) ) )
= $true )
| ~ spl5_2
| ~ spl5_5 ),
inference(boolean_simplification,[],[f1288]) ).
thf(f1303,plain,
( ( ( ~ ( ( sK0 @ sK6 @ sK15 )
| $true ) )
= $true )
| ~ spl5_2
| ~ spl5_5 ),
inference(forward_demodulation,[],[f1295,f1279]) ).
thf(f1304,plain,
( ( ( ~ $true ) = $true )
| ~ spl5_2
| ~ spl5_5 ),
inference(boolean_simplification,[],[f1303]) ).
thf(f1305,plain,
( ( $false = $true )
| ~ spl5_2
| ~ spl5_5 ),
inference(boolean_simplification,[],[f1304]) ).
thf(f1306,plain,
( $false
| ~ spl5_2
| ~ spl5_5 ),
inference(trivial_inequality_removal,[],[f1305]) ).
thf(f1307,plain,
( ~ spl5_2
| ~ spl5_5 ),
inference(avatar_contradiction_clause,[],[f1306]) ).
thf(f1439,plain,
( ! [X1: a > $o] :
( $true
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) )
@ X1 ) )
| ~ spl5_9 ),
inference(pi_proxy_clausification,[],[f540]) ).
thf(f1440,plain,
( ! [X1: a > $o] :
( $true
= ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( X1 @ Y1 ) )
=> ( X1 @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( X1 @ Y0 ) ) ) )
=> ( X1 @ sK9 ) ) )
| ~ spl5_9 ),
inference(beta-eta_normalization,[],[f1439]) ).
thf(f1461,plain,
( ( ( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
=> $false )
= $true )
| ~ spl5_1
| ~ spl5_9 ),
inference(superposition,[],[f1440,f481]) ).
thf(f1465,plain,
( ( $true
= ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) ) )
| ~ spl5_1
| ~ spl5_9 ),
inference(boolean_simplification,[],[f1461]) ).
thf(f1476,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true )
| ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( sK3 @ Y2 @ Y1 )
& ( Y0 @ Y2 ) )
=> ( Y0 @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( sK3 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( Y0 @ sK9 ) ) )
= $true )
| ~ spl5_1 ),
inference(or_proxy_clausification,[],[f482]) ).
thf(f1589,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) )
| ~ spl5_1
| ~ spl5_9 ),
inference(not_proxy_clausification,[],[f1465]) ).
thf(f1596,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
= $false )
| ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_1
| ~ spl5_9 ),
inference(and_proxy_clausification,[],[f1589]) ).
thf(f1598,definition,
( spl5_11
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition]) ).
thf(f1600,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_11 ),
inference(avatar_component_clause,[],[f1598]) ).
thf(f1602,definition,
( spl5_12
<=> ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition]) ).
thf(f1604,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) ) )
= $false )
| ~ spl5_12 ),
inference(avatar_component_clause,[],[f1602]) ).
thf(f1606,plain,
( spl5_10
| spl5_9
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f1476,f109,f538,f542]) ).
thf(f1649,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( sK0 @ sK2 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( !! @ a
@ ^ [Y2: a] :
( ( ( Y0 @ Y2 )
& ( sK0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y1 ) ) ) ) )
=> ( Y0 @ sK9 ) )
@ X1 )
= $true )
| ~ spl5_10 ),
inference(pi_proxy_clausification,[],[f544]) ).
thf(f1650,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( X1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( X1 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( X1 @ Y0 ) ) ) ) )
=> ( X1 @ sK9 ) )
= $true )
| ~ spl5_10 ),
inference(beta-eta_normalization,[],[f1649]) ).
thf(f1678,plain,
( ( $true
= ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) )
=> $false ) )
| ~ spl5_1
| ~ spl5_10 ),
inference(superposition,[],[f1650,f481]) ).
thf(f1683,plain,
( ( ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) ) )
= $true )
| ~ spl5_1
| ~ spl5_10 ),
inference(boolean_simplification,[],[f1678]) ).
thf(f1715,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) ) )
| ~ spl5_1
| ~ spl5_10 ),
inference(not_proxy_clausification,[],[f1683]) ).
thf(f1729,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) )
| ~ spl5_1
| ~ spl5_10 ),
inference(and_proxy_clausification,[],[f1715]) ).
thf(f1731,definition,
( spl5_13
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition]) ).
thf(f1733,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_13 ),
inference(avatar_component_clause,[],[f1731]) ).
thf(f1735,definition,
( spl5_14
<=> ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_14])],[avatar_definition]) ).
thf(f1737,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) ) )
| ~ spl5_14 ),
inference(avatar_component_clause,[],[f1735]) ).
thf(f1738,plain,
( spl5_13
| spl5_14
| ~ spl5_1
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f1729,f542,f109,f1735,f1731]) ).
thf(f2569,plain,
( ( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y0 )
& ( sK3 @ Y0 @ Y1 ) )
=> ( sK4 @ Y1 ) ) )
@ sK17 ) )
| ~ spl5_6 ),
inference(sigma_proxy_clausification,[],[f420]) ).
thf(f2570,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( sK4 @ sK17 )
& ( sK3 @ sK17 @ Y0 ) )
=> ( sK4 @ Y0 ) ) ) )
| ~ spl5_6 ),
inference(beta-eta_normalization,[],[f2569]) ).
thf(f2574,plain,
( ( $false
= ( ^ [Y0: a] :
( ( ( sK4 @ sK17 )
& ( sK3 @ sK17 @ Y0 ) )
=> ( sK4 @ Y0 ) )
@ sK18 ) )
| ~ spl5_6 ),
inference(sigma_proxy_clausification,[],[f2570]) ).
thf(f2575,plain,
( ( $false
= ( ( ( sK4 @ sK17 )
& ( sK3 @ sK17 @ sK18 ) )
=> ( sK4 @ sK18 ) ) )
| ~ spl5_6 ),
inference(beta-eta_normalization,[],[f2574]) ).
thf(f2579,plain,
( ( $false
= ( sK4 @ sK18 ) )
| ~ spl5_6 ),
inference(imp_proxy_clausification,[],[f2575]) ).
thf(f2580,plain,
( ( ( ( sK4 @ sK17 )
& ( sK3 @ sK17 @ sK18 ) )
= $true )
| ~ spl5_6 ),
inference(imp_proxy_clausification,[],[f2575]) ).
thf(f2605,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK0 @ Y0 @ Y1 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ Y1 ) ) )
@ X1 )
= $true )
| spl5_7 ),
inference(pi_proxy_clausification,[],[f463]) ).
thf(f2606,plain,
( ! [X1: a] :
( ( !! @ a
@ ^ [Y0: a] :
( ( ( sK0 @ X1 @ Y0 )
& ( sK4 @ X1 ) )
=> ( sK4 @ Y0 ) ) )
= $true )
| spl5_7 ),
inference(beta-eta_normalization,[],[f2605]) ).
thf(f2608,plain,
( ! [X2: a,X1: a] :
( ( ^ [Y0: a] :
( ( ( sK0 @ X1 @ Y0 )
& ( sK4 @ X1 ) )
=> ( sK4 @ Y0 ) )
@ X2 )
= $true )
| spl5_7 ),
inference(pi_proxy_clausification,[],[f2606]) ).
thf(f2609,plain,
( ! [X2: a,X1: a] :
( $true
= ( ( ( sK0 @ X1 @ X2 )
& ( sK4 @ X1 ) )
=> ( sK4 @ X2 ) ) )
| spl5_7 ),
inference(beta-eta_normalization,[],[f2608]) ).
thf(f2626,plain,
( ! [X0: a] :
( $true
= ( ( ( sK0 @ sK6 @ X0 )
& $true )
=> ( sK4 @ X0 ) ) )
| ~ spl5_2
| spl5_7 ),
inference(superposition,[],[f2609,f155]) ).
thf(f2637,plain,
( ! [X0: a] :
( ( ( sK0 @ sK6 @ X0 )
=> ( sK4 @ X0 ) )
= $true )
| ~ spl5_2
| spl5_7 ),
inference(boolean_simplification,[],[f2626]) ).
thf(f2696,plain,
( ( ( sK3 @ sK17 @ sK18 )
= $true )
| ~ spl5_6 ),
inference(and_proxy_clausification,[],[f2580]) ).
thf(f2697,plain,
( ( $true
= ( sK4 @ sK17 ) )
| ~ spl5_6 ),
inference(and_proxy_clausification,[],[f2580]) ).
thf(f2734,plain,
( ( $true
= ( ( ( ( sK0 @ sK17 @ sK18 )
| $true )
& ( sK4 @ sK17 ) )
=> ( sK4 @ sK18 ) ) )
| ~ spl5_6 ),
inference(superposition,[],[f51,f2696]) ).
thf(f2736,plain,
( ( ( ( $true
& ( sK4 @ sK17 ) )
=> ( sK4 @ sK18 ) )
= $true )
| ~ spl5_6 ),
inference(boolean_simplification,[],[f2734]) ).
thf(f2737,plain,
( ( ( ( sK4 @ sK17 )
=> ( sK4 @ sK18 ) )
= $true )
| ~ spl5_6 ),
inference(boolean_simplification,[],[f2736]) ).
thf(f2740,plain,
( ( $true
= ( $true
=> ( sK4 @ sK18 ) ) )
| ~ spl5_6 ),
inference(forward_demodulation,[],[f2737,f2697]) ).
thf(f2741,plain,
( ( $true
= ( sK4 @ sK18 ) )
| ~ spl5_6 ),
inference(boolean_simplification,[],[f2740]) ).
thf(f2744,plain,
( ( $false = $true )
| ~ spl5_6 ),
inference(forward_demodulation,[],[f2741,f2579]) ).
thf(f2745,plain,
( $false
| ~ spl5_6 ),
inference(trivial_inequality_removal,[],[f2744]) ).
thf(f2746,plain,
~ spl5_6,
inference(avatar_contradiction_clause,[],[f2745]) ).
thf(f2969,plain,
( ( $false
= ( ^ [Y0: a] :
( ( sK0 @ sK6 @ Y0 )
=> ( sK4 @ Y0 ) )
@ sK19 ) )
| ~ spl5_8 ),
inference(sigma_proxy_clausification,[],[f468]) ).
thf(f2970,plain,
( ( $false
= ( ( sK0 @ sK6 @ sK19 )
=> ( sK4 @ sK19 ) ) )
| ~ spl5_8 ),
inference(beta-eta_normalization,[],[f2969]) ).
thf(f2971,plain,
( ( $false = $true )
| ~ spl5_2
| spl5_7
| ~ spl5_8 ),
inference(forward_demodulation,[],[f2970,f2637]) ).
thf(f2972,plain,
( $false
| ~ spl5_2
| spl5_7
| ~ spl5_8 ),
inference(trivial_inequality_removal,[],[f2971]) ).
thf(f2973,plain,
( ~ spl5_2
| spl5_7
| ~ spl5_8 ),
inference(avatar_contradiction_clause,[],[f2972]) ).
thf(f3110,plain,
( spl5_11
| spl5_12
| ~ spl5_1
| ~ spl5_9 ),
inference(avatar_split_clause,[],[f1596,f538,f109,f1602,f1598]) ).
thf(f3373,plain,
( ( $false
= ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK3 @ Y1 @ Y0 )
& ( sK4 @ Y1 ) )
=> ( sK4 @ Y0 ) ) )
@ sK21 ) )
| ~ spl5_12 ),
inference(sigma_proxy_clausification,[],[f1604]) ).
thf(f3374,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( sK3 @ Y0 @ sK21 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ sK21 ) ) ) )
| ~ spl5_12 ),
inference(beta-eta_normalization,[],[f3373]) ).
thf(f3388,plain,
( ( ( ^ [Y0: a] :
( ( ( sK3 @ Y0 @ sK21 )
& ( sK4 @ Y0 ) )
=> ( sK4 @ sK21 ) )
@ sK22 )
= $false )
| ~ spl5_12 ),
inference(sigma_proxy_clausification,[],[f3374]) ).
thf(f3389,plain,
( ( $false
= ( ( ( sK3 @ sK22 @ sK21 )
& ( sK4 @ sK22 ) )
=> ( sK4 @ sK21 ) ) )
| ~ spl5_12 ),
inference(beta-eta_normalization,[],[f3388]) ).
thf(f3404,plain,
( ( $false
= ( sK4 @ sK21 ) )
| ~ spl5_12 ),
inference(imp_proxy_clausification,[],[f3389]) ).
thf(f3405,plain,
( ( $true
= ( ( sK3 @ sK22 @ sK21 )
& ( sK4 @ sK22 ) ) )
| ~ spl5_12 ),
inference(imp_proxy_clausification,[],[f3389]) ).
thf(f3462,plain,
( ( ( sK4 @ sK22 )
= $true )
| ~ spl5_12 ),
inference(and_proxy_clausification,[],[f3405]) ).
thf(f3463,plain,
( ( ( sK3 @ sK22 @ sK21 )
= $true )
| ~ spl5_12 ),
inference(and_proxy_clausification,[],[f3405]) ).
thf(f3540,plain,
( ( $true
= ( ( ( ( sK0 @ sK22 @ sK21 )
| $true )
& ( sK4 @ sK22 ) )
=> ( sK4 @ sK21 ) ) )
| ~ spl5_12 ),
inference(superposition,[],[f51,f3463]) ).
thf(f3541,plain,
( ( ( ( $true
& ( sK4 @ sK22 ) )
=> ( sK4 @ sK21 ) )
= $true )
| ~ spl5_12 ),
inference(boolean_simplification,[],[f3540]) ).
thf(f3542,plain,
( ( ( ( sK4 @ sK22 )
=> ( sK4 @ sK21 ) )
= $true )
| ~ spl5_12 ),
inference(boolean_simplification,[],[f3541]) ).
thf(f3545,plain,
( ( ( $true
=> ( sK4 @ sK21 ) )
= $true )
| ~ spl5_12 ),
inference(forward_demodulation,[],[f3542,f3462]) ).
thf(f3546,plain,
( ( ( sK4 @ sK21 )
= $true )
| ~ spl5_12 ),
inference(boolean_simplification,[],[f3545]) ).
thf(f3549,plain,
( ( $false = $true )
| ~ spl5_12 ),
inference(forward_demodulation,[],[f3546,f3404]) ).
thf(f3550,plain,
( $false
| ~ spl5_12 ),
inference(trivial_inequality_removal,[],[f3549]) ).
thf(f3551,plain,
~ spl5_12,
inference(avatar_contradiction_clause,[],[f3550]) ).
thf(f3552,plain,
( ( $false
= ( ^ [Y0: a] :
( ( sK3 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) )
@ sK23 ) )
| ~ spl5_11 ),
inference(sigma_proxy_clausification,[],[f1600]) ).
thf(f3553,plain,
( ( $false
= ( ( sK3 @ sK2 @ sK23 )
=> ( sK4 @ sK23 ) ) )
| ~ spl5_11 ),
inference(beta-eta_normalization,[],[f3552]) ).
thf(f3554,plain,
( ( $false
= ( sK4 @ sK23 ) )
| ~ spl5_11 ),
inference(imp_proxy_clausification,[],[f3553]) ).
thf(f3555,plain,
( ( ( sK3 @ sK2 @ sK23 )
= $true )
| ~ spl5_11 ),
inference(imp_proxy_clausification,[],[f3553]) ).
thf(f3559,plain,
( ( $true
= ( ( ( sK3 @ sK2 @ sK23 )
| ( sK0 @ sK2 @ sK23 ) )
=> $false ) )
| ~ spl5_11 ),
inference(superposition,[],[f37,f3554]) ).
thf(f3588,plain,
( ( ( ~ ( ( sK3 @ sK2 @ sK23 )
| ( sK0 @ sK2 @ sK23 ) ) )
= $true )
| ~ spl5_11 ),
inference(boolean_simplification,[],[f3559]) ).
thf(f3604,plain,
( ( ( ~ ( $true
| ( sK0 @ sK2 @ sK23 ) ) )
= $true )
| ~ spl5_11 ),
inference(forward_demodulation,[],[f3588,f3555]) ).
thf(f3605,plain,
( ( ( ~ $true ) = $true )
| ~ spl5_11 ),
inference(boolean_simplification,[],[f3604]) ).
thf(f3606,plain,
( ( $false = $true )
| ~ spl5_11 ),
inference(boolean_simplification,[],[f3605]) ).
thf(f3607,plain,
( $false
| ~ spl5_11 ),
inference(trivial_inequality_removal,[],[f3606]) ).
thf(f3608,plain,
~ spl5_11,
inference(avatar_contradiction_clause,[],[f3607]) ).
thf(f3791,plain,
( ( ( ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( ( sK4 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK4 @ Y0 ) ) )
@ sK24 )
= $false )
| ~ spl5_14 ),
inference(sigma_proxy_clausification,[],[f1737]) ).
thf(f3792,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( ( sK4 @ Y0 )
& ( sK0 @ Y0 @ sK24 ) )
=> ( sK4 @ sK24 ) ) ) )
| ~ spl5_14 ),
inference(beta-eta_normalization,[],[f3791]) ).
thf(f3794,plain,
( ( $false
= ( ^ [Y0: a] :
( ( ( sK4 @ Y0 )
& ( sK0 @ Y0 @ sK24 ) )
=> ( sK4 @ sK24 ) )
@ sK25 ) )
| ~ spl5_14 ),
inference(sigma_proxy_clausification,[],[f3792]) ).
thf(f3795,plain,
( ( $false
= ( ( ( sK4 @ sK25 )
& ( sK0 @ sK25 @ sK24 ) )
=> ( sK4 @ sK24 ) ) )
| ~ spl5_14 ),
inference(beta-eta_normalization,[],[f3794]) ).
thf(f3807,plain,
( ( $false
= ( sK4 @ sK24 ) )
| ~ spl5_14 ),
inference(imp_proxy_clausification,[],[f3795]) ).
thf(f3808,plain,
( ( ( ( sK4 @ sK25 )
& ( sK0 @ sK25 @ sK24 ) )
= $true )
| ~ spl5_14 ),
inference(imp_proxy_clausification,[],[f3795]) ).
thf(f3869,plain,
( ( $true
= ( sK0 @ sK25 @ sK24 ) )
| ~ spl5_14 ),
inference(and_proxy_clausification,[],[f3808]) ).
thf(f3870,plain,
( ( ( sK4 @ sK25 )
= $true )
| ~ spl5_14 ),
inference(and_proxy_clausification,[],[f3808]) ).
thf(f3993,plain,
( ( ( ( ( $true
| ( sK3 @ sK25 @ sK24 ) )
& ( sK4 @ sK25 ) )
=> ( sK4 @ sK24 ) )
= $true )
| ~ spl5_14 ),
inference(superposition,[],[f51,f3869]) ).
thf(f3994,plain,
( ( ( ( $true
& ( sK4 @ sK25 ) )
=> ( sK4 @ sK24 ) )
= $true )
| ~ spl5_14 ),
inference(boolean_simplification,[],[f3993]) ).
thf(f3995,plain,
( ( ( ( sK4 @ sK25 )
=> ( sK4 @ sK24 ) )
= $true )
| ~ spl5_14 ),
inference(boolean_simplification,[],[f3994]) ).
thf(f3999,plain,
( ( $true
= ( $true
=> ( sK4 @ sK24 ) ) )
| ~ spl5_14 ),
inference(forward_demodulation,[],[f3995,f3870]) ).
thf(f4000,plain,
( ( $true
= ( sK4 @ sK24 ) )
| ~ spl5_14 ),
inference(boolean_simplification,[],[f3999]) ).
thf(f4005,plain,
( ( $false = $true )
| ~ spl5_14 ),
inference(forward_demodulation,[],[f4000,f3807]) ).
thf(f4006,plain,
( $false
| ~ spl5_14 ),
inference(trivial_inequality_removal,[],[f4005]) ).
thf(f4007,plain,
~ spl5_14,
inference(avatar_contradiction_clause,[],[f4006]) ).
thf(f4022,plain,
( ( $false
= ( ^ [Y0: a] :
( ( sK0 @ sK2 @ Y0 )
=> ( sK4 @ Y0 ) )
@ sK26 ) )
| ~ spl5_13 ),
inference(sigma_proxy_clausification,[],[f1733]) ).
thf(f4023,plain,
( ( ( ( sK0 @ sK2 @ sK26 )
=> ( sK4 @ sK26 ) )
= $false )
| ~ spl5_13 ),
inference(beta-eta_normalization,[],[f4022]) ).
thf(f4024,plain,
( ( $false
= ( sK4 @ sK26 ) )
| ~ spl5_13 ),
inference(imp_proxy_clausification,[],[f4023]) ).
thf(f4025,plain,
( ( ( sK0 @ sK2 @ sK26 )
= $true )
| ~ spl5_13 ),
inference(imp_proxy_clausification,[],[f4023]) ).
thf(f4029,plain,
( ( ( ( ( sK3 @ sK2 @ sK26 )
| ( sK0 @ sK2 @ sK26 ) )
=> $false )
= $true )
| ~ spl5_13 ),
inference(superposition,[],[f37,f4024]) ).
thf(f4056,plain,
( ( ( ~ ( ( sK3 @ sK2 @ sK26 )
| ( sK0 @ sK2 @ sK26 ) ) )
= $true )
| ~ spl5_13 ),
inference(boolean_simplification,[],[f4029]) ).
thf(f4088,plain,
( ( $true
= ( ~ ( ( sK3 @ sK2 @ sK26 )
| $true ) ) )
| ~ spl5_13 ),
inference(forward_demodulation,[],[f4056,f4025]) ).
thf(f4089,plain,
( ( ( ~ $true ) = $true )
| ~ spl5_13 ),
inference(boolean_simplification,[],[f4088]) ).
thf(f4090,plain,
( ( $false = $true )
| ~ spl5_13 ),
inference(boolean_simplification,[],[f4089]) ).
thf(f4091,plain,
( $false
| ~ spl5_13 ),
inference(trivial_inequality_removal,[],[f4090]) ).
thf(f4092,plain,
~ spl5_13,
inference(avatar_contradiction_clause,[],[f4091]) ).
cnf(s1,plain,
( spl5_1
| spl5_2 ),
inference(sat_conversion,[],[f116]) ).
cnf(s2,plain,
( ~ spl5_2
| spl5_3
| spl5_4 ),
inference(sat_conversion,[],[f258]) ).
cnf(s3,plain,
( ~ spl5_2
| ~ spl5_3
| spl5_5
| spl5_6 ),
inference(sat_conversion,[],[f421]) ).
cnf(s6,plain,
( ~ spl5_2
| ~ spl5_4
| spl5_7
| spl5_8 ),
inference(sat_conversion,[],[f703]) ).
cnf(s7,plain,
~ spl5_7,
inference(sat_conversion,[],[f1160]) ).
cnf(s8,plain,
( ~ spl5_2
| ~ spl5_5 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s11,plain,
( ~ spl5_1
| spl5_9
| spl5_10 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s12,plain,
( ~ spl5_1
| ~ spl5_10
| spl5_13
| spl5_14 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s13,plain,
~ spl5_6,
inference(sat_conversion,[],[f2746]) ).
cnf(s15,plain,
( ~ spl5_2
| spl5_7
| ~ spl5_8 ),
inference(sat_conversion,[],[f2973]) ).
cnf(s16,plain,
( ~ spl5_1
| ~ spl5_9
| spl5_11
| spl5_12 ),
inference(sat_conversion,[],[f3110]) ).
cnf(s18,plain,
~ spl5_12,
inference(sat_conversion,[],[f3551]) ).
cnf(s19,plain,
~ spl5_11,
inference(sat_conversion,[],[f3608]) ).
cnf(s20,plain,
~ spl5_14,
inference(sat_conversion,[],[f4007]) ).
cnf(s22,plain,
~ spl5_13,
inference(sat_conversion,[],[f4092]) ).
cnf(s23,plain,
( ~ spl5_1
| ~ spl5_9 ),
inference(rat,[],[s16,s18,s19]) ).
cnf(s24,plain,
( ~ spl5_1
| ~ spl5_10 ),
inference(rat,[],[s12,s20,s22]) ).
cnf(s26,plain,
( ~ spl5_2
| ~ spl5_4
| spl5_8 ),
inference(rat,[],[s6,s7]) ).
cnf(s28,plain,
( ~ spl5_2
| ~ spl5_3
| spl5_5 ),
inference(rat,[],[s3,s13]) ).
cnf(s29,plain,
~ spl5_2,
inference(rat,[],[s2,s28,s26,s8,s15,s7]) ).
cnf(s30,plain,
spl5_1,
inference(rat,[],[s1,s29]) ).
cnf(s31,plain,
~ spl5_9,
inference(rat,[],[s23,s30]) ).
cnf(s32,plain,
~ spl5_10,
inference(rat,[],[s24,s30]) ).
cnf(s33,plain,
$false,
inference(rat,[],[s11,s32,s31,s30]) ).
thf(f4095,plain,
$false,
inference(avatar_sat_refutation,[],[s33]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEV148^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 % Computer : n007.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Tue Sep 29 15:14:26 UTC 2026
% 0.10/0.26 % CPUTime :
% 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running higher-order theorem proving
% 0.24/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.32/0.51 % (3487707)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.32/0.51 % (3487714)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3963862236:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.32/0.51 % (3487714)Instruction limit reached!
% 1.32/0.51 % (3487714)------------------------------
% 1.32/0.51 % (3487714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.51 % (3487714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.51 % (3487714)CaDiCaL version: 2.1.3
% 1.32/0.51 % (3487714)Termination reason: Instruction limit
% 1.32/0.51 % (3487714)Termination phase: Saturation
% 1.32/0.51 % (3487714)Time elapsed: 0.004 s
% 1.32/0.51 % (3487714)Peak memory usage: 11 MB
% 1.32/0.51 % (3487714)Instructions burned: 8 (million)
% 1.32/0.51 % (3487718)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.32/0.51 % (3487718)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.32/0.51 % (3487712)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2600556954:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.32/0.51 % (3487713)lrs+10_16_si=on:nwc=1.5:random_seed=738984664:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.32/0.51 % (3487716)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3038316947:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.32/0.51 % (3487717)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2705579054:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.32/0.51 % (3487718)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=2847010742:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.32/0.51 % (3487715)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=1064165581: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)
% 1.32/0.51 % (3487720)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=295722950:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.32/0.51 % (3487720)Instruction limit reached!
% 1.32/0.51 % (3487720)------------------------------
% 1.32/0.51 % (3487720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.51 % (3487720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.51 % (3487720)CaDiCaL version: 2.1.3
% 1.32/0.51 % (3487720)Termination reason: Instruction limit
% 1.32/0.51 % (3487720)Termination phase: Preprocessing 3
% 1.32/0.51 % (3487720)Time elapsed: 0.001 s
% 1.32/0.51 % (3487720)Peak memory usage: 10 MB
% 1.32/0.51 % (3487720)Instructions burned: 2 (million)
% 1.32/0.51 % (3487713)Instruction limit reached!
% 1.32/0.51 % (3487713)------------------------------
% 1.32/0.51 % (3487713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.51 % (3487713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.51 % (3487713)CaDiCaL version: 2.1.3
% 1.32/0.51 % (3487713)Termination reason: Instruction limit
% 1.32/0.51 % (3487713)Termination phase: Saturation
% 1.32/0.51 % (3487713)Time elapsed: 0.017 s
% 1.32/0.51 % (3487713)Peak memory usage: 12 MB
% 1.32/0.51 % (3487713)Instructions burned: 19 (million)
% 1.32/0.51 % (3487716)Instruction limit reached!
% 1.32/0.51 % (3487716)------------------------------
% 1.32/0.51 % (3487716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.51 % (3487716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.51 % (3487716)CaDiCaL version: 2.1.3
% 1.32/0.51 % (3487716)Termination reason: Instruction limit
% 1.32/0.51 % (3487716)Termination phase: Saturation
% 1.32/0.51 % (3487716)Time elapsed: 0.023 s
% 1.32/0.51 % (3487716)Peak memory usage: 12 MB
% 1.32/0.51 % (3487716)Instructions burned: 25 (million)
% 1.32/0.51 % (3487728)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2813356614:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.32/0.57 % (3487728)Instruction limit reached!
% 1.32/0.57 % (3487728)------------------------------
% 1.32/0.57 % (3487728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487728)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487728)Termination reason: Instruction limit
% 1.32/0.57 % (3487728)Termination phase: Saturation
% 1.32/0.57 % (3487728)Time elapsed: 0.003 s
% 1.32/0.57 % (3487728)Peak memory usage: 11 MB
% 1.32/0.57 % (3487728)Instructions burned: 7 (million)
% 1.32/0.57 % (3487729)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.32/0.57 % (3487729)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2070354522:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.32/0.57 % (3487730)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1378239924:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.32/0.57 % (3487733)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.32/0.57 % (3487733)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.32/0.57 % (3487729)Instruction limit reached!
% 1.32/0.57 % (3487729)------------------------------
% 1.32/0.57 % (3487729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487729)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487729)Termination reason: Instruction limit
% 1.32/0.57 % (3487729)Termination phase: Saturation
% 1.32/0.57 % (3487729)Time elapsed: 0.007 s
% 1.32/0.57 % (3487729)Peak memory usage: 12 MB
% 1.32/0.57 % (3487729)Instructions burned: 8 (million)
% 1.32/0.57 % (3487733)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2085222019:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.32/0.57 % (3487717)Instruction limit reached!
% 1.32/0.57 % (3487717)------------------------------
% 1.32/0.57 % (3487717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487717)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487717)Termination reason: Instruction limit
% 1.32/0.57 % (3487717)Termination phase: Saturation
% 1.32/0.57 % (3487717)Time elapsed: 0.064 s
% 1.32/0.57 % (3487717)Peak memory usage: 12 MB
% 1.32/0.57 % (3487717)Instructions burned: 75 (million)
% 1.32/0.57 % (3487730)Instruction limit reached!
% 1.32/0.57 % (3487730)------------------------------
% 1.32/0.57 % (3487730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487730)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487730)Termination reason: Instruction limit
% 1.32/0.57 % (3487730)Termination phase: Saturation
% 1.32/0.57 % (3487730)Time elapsed: 0.012 s
% 1.32/0.57 % (3487730)Peak memory usage: 12 MB
% 1.32/0.57 % (3487730)Instructions burned: 13 (million)
% 1.32/0.57 % (3487733)Instruction limit reached!
% 1.32/0.57 % (3487733)------------------------------
% 1.32/0.57 % (3487733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487733)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487733)Termination reason: Instruction limit
% 1.32/0.57 % (3487733)Termination phase: Saturation
% 1.32/0.57 % (3487733)Time elapsed: 0.012 s
% 1.32/0.57 % (3487733)Peak memory usage: 11 MB
% 1.32/0.57 % (3487733)Instructions burned: 28 (million)
% 1.32/0.57 % (3487712)Instruction limit reached!
% 1.32/0.57 % (3487712)------------------------------
% 1.32/0.57 % (3487712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (3487712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (3487712)CaDiCaL version: 2.1.3
% 1.32/0.57 % (3487712)Termination reason: Instruction limit
% 1.96/0.64 % (3487712)Termination phase: Saturation
% 1.96/0.64 % (3487712)Time elapsed: 0.079 s
% 1.96/0.64 % (3487712)Peak memory usage: 12 MB
% 1.96/0.64 % (3487712)Instructions burned: 88 (million)
% 1.96/0.64 % (3487738)lrs+10_1_si=on:cs=on:random_seed=1014971194:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.96/0.64 % (3487736)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=2148390797:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.96/0.64 % (3487738)Instruction limit reached!
% 1.96/0.64 % (3487738)------------------------------
% 1.96/0.64 % (3487738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.64 % (3487738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.64 % (3487738)CaDiCaL version: 2.1.3
% 1.96/0.64 % (3487738)Termination reason: Instruction limit
% 1.96/0.64 % (3487738)Termination phase: Saturation
% 1.96/0.64 % (3487738)Time elapsed: 0.006 s
% 1.96/0.64 % (3487738)Peak memory usage: 12 MB
% 1.96/0.64 % (3487738)Instructions burned: 13 (million)
% 1.96/0.64 % (3487739)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.96/0.64 % (3487739)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=3486949569:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.96/0.64 % (3487741)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1297427419:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.96/0.64 % (3487739)Instruction limit reached!
% 1.96/0.64 % (3487739)------------------------------
% 1.96/0.64 % (3487739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.64 % (3487739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.64 % (3487739)CaDiCaL version: 2.1.3
% 1.96/0.64 % (3487739)Termination reason: Instruction limit
% 1.96/0.64 % (3487739)Termination phase: Property scanning
% 1.96/0.64 % (3487739)Time elapsed: 0.002 s
% 1.96/0.64 % (3487739)Peak memory usage: 9 MB
% 1.96/0.64 % (3487739)Instructions burned: 2 (million)
% 1.96/0.64 % (3487742)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4199085545:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.96/0.64 % (3487745)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2008000583:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.96/0.64 % (3487745)Instruction limit reached!
% 1.96/0.64 % (3487745)------------------------------
% 1.96/0.64 % (3487745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.64 % (3487745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.64 % (3487745)CaDiCaL version: 2.1.3
% 1.96/0.64 % (3487745)Termination reason: Instruction limit
% 1.96/0.64 % (3487745)Termination phase: Saturation
% 1.96/0.64 % (3487745)Time elapsed: 0.013 s
% 1.96/0.64 % (3487745)Peak memory usage: 12 MB
% 1.96/0.64 % (3487745)Instructions burned: 26 (million)
% 1.96/0.64 % (3487748)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3612959163:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.96/0.64 % (3487741)Instruction limit reached!
% 1.96/0.64 % (3487741)------------------------------
% 1.96/0.64 % (3487741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.64 % (3487741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.64 % (3487741)CaDiCaL version: 2.1.3
% 1.96/0.64 % (3487741)Termination reason: Instruction limit
% 1.96/0.64 % (3487741)Termination phase: Saturation
% 1.96/0.64 % (3487741)Time elapsed: 0.037 s
% 1.96/0.64 % (3487741)Peak memory usage: 12 MB
% 1.96/0.64 % (3487741)Instructions burned: 39 (million)
% 1.96/0.64 % (3487718)Instruction limit reached!
% 1.96/0.64 % (3487718)------------------------------
% 1.96/0.64 % (3487718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.64 % (3487718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.64 % (3487718)CaDiCaL version: 2.1.3
% 1.96/0.64 % (3487718)Termination reason: Instruction limit
% 1.96/0.64 % (3487718)Termination phase: Saturation
% 2.59/0.71 % (3487718)Time elapsed: 0.140 s
% 2.59/0.71 % (3487718)Peak memory usage: 12 MB
% 2.59/0.71 % (3487718)Instructions burned: 157 (million)
% 2.59/0.71 % (3487751)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2109271890:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.59/0.71 % (3487748)Instruction limit reached!
% 2.59/0.71 % (3487748)------------------------------
% 2.59/0.71 % (3487748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.71 % (3487748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.71 % (3487748)CaDiCaL version: 2.1.3
% 2.59/0.71 % (3487748)Termination reason: Instruction limit
% 2.59/0.71 % (3487748)Termination phase: Saturation
% 2.59/0.71 % (3487748)Time elapsed: 0.013 s
% 2.59/0.71 % (3487748)Peak memory usage: 12 MB
% 2.59/0.71 % (3487748)Instructions burned: 14 (million)
% 2.59/0.71 % (3487753)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3737222985:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.59/0.71 % (3487736)Instruction limit reached!
% 2.59/0.71 % (3487736)------------------------------
% 2.59/0.71 % (3487736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.71 % (3487736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.71 % (3487736)CaDiCaL version: 2.1.3
% 2.59/0.71 % (3487736)Termination reason: Instruction limit
% 2.59/0.71 % (3487736)Termination phase: Saturation
% 2.59/0.71 % (3487736)Time elapsed: 0.076 s
% 2.59/0.71 % (3487736)Peak memory usage: 13 MB
% 2.59/0.71 % (3487736)Instructions burned: 86 (million)
% 2.59/0.71 % (3487753)Instruction limit reached!
% 2.59/0.71 % (3487753)------------------------------
% 2.59/0.71 % (3487753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.71 % (3487753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.71 % (3487753)CaDiCaL version: 2.1.3
% 2.59/0.71 % (3487753)Termination reason: Instruction limit
% 2.59/0.71 % (3487753)Termination phase: Saturation
% 2.59/0.71 % (3487753)Time elapsed: 0.013 s
% 2.59/0.71 % (3487753)Peak memory usage: 12 MB
% 2.59/0.71 % (3487753)Instructions burned: 15 (million)
% 2.59/0.71 % (3487754)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=991813071:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.59/0.71 % (3487754)Instruction limit reached!
% 2.59/0.71 % (3487754)------------------------------
% 2.59/0.71 % (3487754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.71 % (3487754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.71 % (3487754)CaDiCaL version: 2.1.3
% 2.59/0.71 % (3487754)Termination reason: Instruction limit
% 2.59/0.71 % (3487754)Termination phase: Preprocessing 3
% 2.59/0.71 % (3487754)Time elapsed: 0.002 s
% 2.59/0.71 % (3487754)Peak memory usage: 10 MB
% 2.59/0.71 % (3487754)Instructions burned: 2 (million)
% 2.59/0.71 % (3487756)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=298468778:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.59/0.71 % (3487758)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3945075866:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.59/0.71 % (3487761)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
% 2.59/0.71 % (3487761)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.59/0.71 % (3487756)Instruction limit reached!
% 2.59/0.71 % (3487756)------------------------------
% 2.59/0.71 % (3487756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.71 % (3487756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.71 % (3487756)CaDiCaL version: 2.1.3
% 2.59/0.71 % (3487756)Termination reason: Instruction limit
% 2.59/0.71 % (3487756)Termination phase: Saturation
% 2.59/0.71 % (3487756)Time elapsed: 0.023 s
% 2.59/0.71 % (3487756)Peak memory usage: 12 MB
% 2.59/0.71 % (3487756)Instructions burned: 27 (million)
% 2.59/0.71 % (3487759)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2064885897:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 3.20/0.82 % (3487761)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=1116240497:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.20/0.82 % (3487758)Instruction limit reached!
% 3.20/0.82 % (3487758)------------------------------
% 3.20/0.82 % (3487758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487758)CaDiCaL version: 2.1.3
% 3.20/0.82 % (3487758)Termination reason: Instruction limit
% 3.20/0.82 % (3487758)Termination phase: Saturation
% 3.20/0.82 % (3487758)Time elapsed: 0.023 s
% 3.20/0.82 % (3487758)Peak memory usage: 11 MB
% 3.20/0.82 % (3487758)Instructions burned: 24 (million)
% 3.20/0.82 % (3487761)Instruction limit reached!
% 3.20/0.82 % (3487761)------------------------------
% 3.20/0.82 % (3487761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487761)CaDiCaL version: 2.1.3
% 3.20/0.82 % (3487761)Termination reason: Instruction limit
% 3.20/0.82 % (3487761)Termination phase: Saturation
% 3.20/0.82 % (3487761)Time elapsed: 0.013 s
% 3.20/0.82 % (3487761)Peak memory usage: 12 MB
% 3.20/0.82 % (3487761)Instructions burned: 15 (million)
% 3.20/0.82 % (3487765)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.20/0.82 % (3487765)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=1236726492:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.20/0.82 % (3487768)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2610089457:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.20/0.82 % (3487767)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=2289652113:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.20/0.82 % (3487768)Instruction limit reached!
% 3.20/0.82 % (3487768)------------------------------
% 3.20/0.82 % (3487768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487768)CaDiCaL version: 2.1.3
% 3.20/0.82 % (3487768)Termination reason: Instruction limit
% 3.20/0.82 % (3487768)Termination phase: Saturation
% 3.20/0.82 % (3487768)Time elapsed: 0.004 s
% 3.20/0.82 % (3487768)Peak memory usage: 12 MB
% 3.20/0.82 % (3487768)Instructions burned: 7 (million)
% 3.20/0.82 % (3487765)Instruction limit reached!
% 3.20/0.82 % (3487765)------------------------------
% 3.20/0.82 % (3487765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487765)CaDiCaL version: 2.1.3
% 3.20/0.82 % (3487765)Termination reason: Instruction limit
% 3.20/0.82 % (3487765)Termination phase: Saturation
% 3.20/0.82 % (3487765)Time elapsed: 0.008 s
% 3.20/0.82 % (3487765)Peak memory usage: 11 MB
% 3.20/0.82 % (3487765)Instructions burned: 8 (million)
% 3.20/0.82 % (3487759)Instruction limit reached!
% 3.20/0.82 % (3487759)------------------------------
% 3.20/0.82 % (3487759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487759)CaDiCaL version: 2.1.3
% 3.20/0.82 % (3487759)Termination reason: Instruction limit
% 3.20/0.82 % (3487759)Termination phase: Saturation
% 3.20/0.82 % (3487759)Time elapsed: 0.057 s
% 3.20/0.82 % (3487759)Peak memory usage: 12 MB
% 3.20/0.82 % (3487759)Instructions burned: 60 (million)
% 3.20/0.82 % (3487772)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1838211835:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.20/0.82 % (3487767)Instruction limit reached!
% 3.20/0.82 % (3487767)------------------------------
% 3.20/0.82 % (3487767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.20/0.82 % (3487767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/0.82 % (3487767)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487767)Termination reason: Instruction limit
% 3.60/0.93 % (3487767)Termination phase: Saturation
% 3.60/0.93 % (3487767)Time elapsed: 0.026 s
% 3.60/0.93 % (3487767)Peak memory usage: 12 MB
% 3.60/0.93 % (3487767)Instructions burned: 31 (million)
% 3.60/0.93 % (3487773)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2907621228:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.60/0.93 % (3487772)Instruction limit reached!
% 3.60/0.93 % (3487772)------------------------------
% 3.60/0.93 % (3487772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (3487772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (3487772)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487772)Termination reason: Instruction limit
% 3.60/0.93 % (3487772)Termination phase: Saturation
% 3.60/0.93 % (3487772)Time elapsed: 0.015 s
% 3.60/0.93 % (3487772)Peak memory usage: 11 MB
% 3.60/0.93 % (3487772)Instructions burned: 23 (million)
% 3.60/0.93 % (3487751)Instruction limit reached!
% 3.60/0.93 % (3487751)------------------------------
% 3.60/0.93 % (3487751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (3487751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (3487751)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487751)Termination reason: Instruction limit
% 3.60/0.93 % (3487751)Termination phase: Saturation
% 3.60/0.93 % (3487751)Time elapsed: 0.144 s
% 3.60/0.93 % (3487751)Peak memory usage: 13 MB
% 3.60/0.93 % (3487751)Instructions burned: 328 (million)
% 3.60/0.93 % (3487774)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=957568614:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.60/0.93 % (3487773)Instruction limit reached!
% 3.60/0.93 % (3487773)------------------------------
% 3.60/0.93 % (3487773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (3487773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (3487773)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487773)Termination reason: Instruction limit
% 3.60/0.93 % (3487773)Termination phase: Saturation
% 3.60/0.93 % (3487773)Time elapsed: 0.019 s
% 3.60/0.93 % (3487773)Peak memory usage: 12 MB
% 3.60/0.93 % (3487773)Instructions burned: 20 (million)
% 3.60/0.93 % (3487776)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1878437561:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.60/0.93 % (3487778)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=424212824:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.60/0.93 % (3487781)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.60/0.93 % (3487781)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1453099650:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.60/0.93 % (3487779)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=505581492:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.60/0.93 % (3487781)Instruction limit reached!
% 3.60/0.93 % (3487781)------------------------------
% 3.60/0.93 % (3487781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (3487781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (3487781)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487781)Termination reason: Instruction limit
% 3.60/0.93 % (3487781)Termination phase: Saturation
% 3.60/0.93 % (3487781)Time elapsed: 0.004 s
% 3.60/0.93 % (3487781)Peak memory usage: 12 MB
% 3.60/0.93 % (3487781)Instructions burned: 9 (million)
% 3.60/0.93 % (3487742)Instruction limit reached!
% 3.60/0.93 % (3487742)------------------------------
% 3.60/0.93 % (3487742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (3487742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (3487742)CaDiCaL version: 2.1.3
% 3.60/0.93 % (3487742)Termination reason: Instruction limit
% 3.60/0.93 % (3487742)Termination phase: Saturation
% 3.60/0.93 % (3487742)Time elapsed: 0.219 s
% 3.60/0.93 % (3487742)Peak memory usage: 13 MB
% 3.60/0.93 % (3487742)Instructions burned: 249 (million)
% 3.60/0.93 % (3487787)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=2620163355:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 5.14/1.10 % (3487786)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3784391232:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 5.14/1.10 % (3487779)Instruction limit reached!
% 5.14/1.10 % (3487779)------------------------------
% 5.14/1.10 % (3487779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.10 % (3487779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.10 % (3487779)CaDiCaL version: 2.1.3
% 5.14/1.10 % (3487779)Termination reason: Instruction limit
% 5.14/1.10 % (3487779)Termination phase: Saturation
% 5.14/1.10 % (3487779)Time elapsed: 0.040 s
% 5.14/1.10 % (3487779)Peak memory usage: 12 MB
% 5.14/1.10 % (3487779)Instructions burned: 42 (million)
% 5.14/1.10 % (3487790)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 5.14/1.10 % (3487790)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=912439374:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 5.14/1.10 % (3487790)Instruction limit reached!
% 5.14/1.10 % (3487790)------------------------------
% 5.14/1.10 % (3487790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.10 % (3487790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.10 % (3487790)CaDiCaL version: 2.1.3
% 5.14/1.10 % (3487790)Termination reason: Instruction limit
% 5.14/1.10 % (3487790)Termination phase: Saturation
% 5.14/1.10 % (3487790)Time elapsed: 0.005 s
% 5.14/1.10 % (3487790)Peak memory usage: 12 MB
% 5.14/1.10 % (3487790)Instructions burned: 6 (million)
% 5.14/1.10 % (3487778)Instruction limit reached!
% 5.14/1.10 % (3487778)------------------------------
% 5.14/1.10 % (3487778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.10 % (3487778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.10 % (3487778)CaDiCaL version: 2.1.3
% 5.14/1.10 % (3487778)Termination reason: Instruction limit
% 5.14/1.10 % (3487778)Termination phase: Saturation
% 5.14/1.10 % (3487778)Time elapsed: 0.120 s
% 5.14/1.10 % (3487778)Peak memory usage: 13 MB
% 5.14/1.10 % (3487778)Instructions burned: 193 (million)
% 5.14/1.10 % (3487776)Instruction limit reached!
% 5.14/1.10 % (3487776)------------------------------
% 5.14/1.10 % (3487776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.10 % (3487776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.10 % (3487776)CaDiCaL version: 2.1.3
% 5.14/1.10 % (3487776)Termination reason: Instruction limit
% 5.14/1.10 % (3487776)Termination phase: Saturation
% 5.14/1.10 % (3487776)Time elapsed: 0.125 s
% 5.14/1.10 % (3487776)Peak memory usage: 13 MB
% 5.14/1.10 % (3487776)Instructions burned: 143 (million)
% 5.14/1.10 % (3487787)Instruction limit reached!
% 5.14/1.10 % (3487787)------------------------------
% 5.14/1.10 % (3487787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.10 % (3487787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.10 % (3487787)CaDiCaL version: 2.1.3
% 5.14/1.10 % (3487787)Termination reason: Instruction limit
% 5.14/1.10 % (3487787)Termination phase: Saturation
% 5.14/1.10 % (3487787)Time elapsed: 0.083 s
% 5.14/1.10 % (3487787)Peak memory usage: 14 MB
% 5.14/1.10 % (3487787)Instructions burned: 170 (million)
% 5.14/1.10 % (3487792)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3095550900:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 5.14/1.10 % (3487795)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=3332613814:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.14/1.10 % (3487793)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1910791253:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 5.14/1.10 % (3487792)Instruction limit reached!
% 5.14/1.10 % (3487792)------------------------------
% 5.14/1.10 % (3487792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487792)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487792)Termination reason: Instruction limit
% 6.11/1.26 % (3487792)Termination phase: Saturation
% 6.11/1.26 % (3487792)Time elapsed: 0.019 s
% 6.11/1.26 % (3487792)Peak memory usage: 12 MB
% 6.11/1.26 % (3487792)Instructions burned: 22 (million)
% 6.11/1.26 % (3487794)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=308684742:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 6.11/1.26 % (3487793)Instruction limit reached!
% 6.11/1.26 % (3487793)------------------------------
% 6.11/1.26 % (3487793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487793)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487793)Termination reason: Instruction limit
% 6.11/1.26 % (3487793)Termination phase: Saturation
% 6.11/1.26 % (3487793)Time elapsed: 0.017 s
% 6.11/1.26 % (3487793)Peak memory usage: 12 MB
% 6.11/1.26 % (3487793)Instructions burned: 19 (million)
% 6.11/1.26 % (3487799)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=3272258717:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 6.11/1.26 % (3487801)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3049091674:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 6.11/1.26 % (3487786)Instruction limit reached!
% 6.11/1.26 % (3487786)------------------------------
% 6.11/1.26 % (3487786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487786)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487786)Termination reason: Instruction limit
% 6.11/1.26 % (3487786)Termination phase: Saturation
% 6.11/1.26 % (3487786)Time elapsed: 0.154 s
% 6.11/1.26 % (3487786)Peak memory usage: 14 MB
% 6.11/1.26 % (3487786)Instructions burned: 181 (million)
% 6.11/1.26 % (3487799)Instruction limit reached!
% 6.11/1.26 % (3487799)------------------------------
% 6.11/1.26 % (3487799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487799)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487799)Termination reason: Instruction limit
% 6.11/1.26 % (3487799)Termination phase: Saturation
% 6.11/1.26 % (3487799)Time elapsed: 0.044 s
% 6.11/1.26 % (3487799)Peak memory usage: 12 MB
% 6.11/1.26 % (3487799)Instructions burned: 46 (million)
% 6.11/1.26 % (3487715)Instruction limit reached!
% 6.11/1.26 % (3487715)------------------------------
% 6.11/1.26 % (3487715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487715)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487715)Termination reason: Instruction limit
% 6.11/1.26 % (3487715)Termination phase: Saturation
% 6.11/1.26 % (3487715)Time elapsed: 0.537 s
% 6.11/1.26 % (3487715)Peak memory usage: 15 MB
% 6.11/1.26 % (3487715)Instructions burned: 635 (million)
% 6.11/1.26 % (3487804)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3983459432:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 6.11/1.26 % (3487805)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.11/1.26 % (3487805)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3584703824:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.11/1.26 % (3487804)Instruction limit reached!
% 6.11/1.26 % (3487804)------------------------------
% 6.11/1.26 % (3487804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (3487804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (3487804)CaDiCaL version: 2.1.3
% 6.11/1.26 % (3487804)Termination reason: Instruction limit
% 6.11/1.26 % (3487804)Termination phase: Saturation
% 6.11/1.26 % (3487804)Time elapsed: 0.020 s
% 6.54/1.40 % (3487804)Peak memory usage: 12 MB
% 6.54/1.40 % (3487804)Instructions burned: 22 (million)
% 6.54/1.40 % (3487806)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4074803895:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 6.54/1.40 % (3487806)Instruction limit reached!
% 6.54/1.40 % (3487806)------------------------------
% 6.54/1.40 % (3487806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.40 % (3487806)CaDiCaL version: 2.1.3
% 6.54/1.40 % (3487806)Termination reason: Instruction limit
% 6.54/1.40 % (3487806)Termination phase: Saturation
% 6.54/1.40 % (3487806)Time elapsed: 0.013 s
% 6.54/1.40 % (3487806)Peak memory usage: 12 MB
% 6.54/1.40 % (3487806)Instructions burned: 14 (million)
% 6.54/1.40 % (3487809)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=2865529947:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 6.54/1.40 % (3487812)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=160373578:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 6.54/1.40 % (3487809)Instruction limit reached!
% 6.54/1.40 % (3487809)------------------------------
% 6.54/1.40 % (3487809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.40 % (3487809)CaDiCaL version: 2.1.3
% 6.54/1.40 % (3487809)Termination reason: Instruction limit
% 6.54/1.40 % (3487809)Termination phase: Saturation
% 6.54/1.40 % (3487809)Time elapsed: 0.043 s
% 6.54/1.40 % (3487809)Peak memory usage: 13 MB
% 6.54/1.40 % (3487809)Instructions burned: 68 (million)
% 6.54/1.40 % (3487812)Instruction limit reached!
% 6.54/1.40 % (3487812)------------------------------
% 6.54/1.40 % (3487812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.40 % (3487812)CaDiCaL version: 2.1.3
% 6.54/1.40 % (3487812)Termination reason: Instruction limit
% 6.54/1.40 % (3487812)Termination phase: Saturation
% 6.54/1.40 % (3487812)Time elapsed: 0.042 s
% 6.54/1.40 % (3487812)Peak memory usage: 12 MB
% 6.54/1.40 % (3487812)Instructions burned: 52 (million)
% 6.54/1.40 % (3487814)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3514494659:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.54/1.40 % (3487815)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=841575783:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.54/1.40 % (3487814)Instruction limit reached!
% 6.54/1.40 % (3487814)------------------------------
% 6.54/1.40 % (3487814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.40 % (3487814)CaDiCaL version: 2.1.3
% 6.54/1.40 % (3487814)Termination reason: Instruction limit
% 6.54/1.40 % (3487814)Termination phase: Saturation
% 6.54/1.40 % (3487814)Time elapsed: 0.030 s
% 6.54/1.40 % (3487814)Peak memory usage: 12 MB
% 6.54/1.40 % (3487814)Instructions burned: 31 (million)
% 6.54/1.40 % (3487805)Instruction limit reached!
% 6.54/1.40 % (3487805)------------------------------
% 6.54/1.40 % (3487805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.40 % (3487805)CaDiCaL version: 2.1.3
% 6.54/1.40 % (3487805)Termination reason: Instruction limit
% 6.54/1.40 % (3487805)Termination phase: Saturation
% 6.54/1.40 % (3487805)Time elapsed: 0.158 s
% 6.54/1.40 % (3487805)Peak memory usage: 12 MB
% 6.54/1.40 % (3487805)Instructions burned: 200 (million)
% 6.54/1.40 % (3487818)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=4277379038:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.54/1.40 % (3487818)Instruction limit reached!
% 6.54/1.40 % (3487818)------------------------------
% 6.54/1.40 % (3487818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.54/1.40 % (3487818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487818)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487818)Termination reason: Instruction limit
% 7.89/1.68 % (3487818)Termination phase: Saturation
% 7.89/1.68 % (3487818)Time elapsed: 0.019 s
% 7.89/1.68 % (3487818)Peak memory usage: 12 MB
% 7.89/1.68 % (3487818)Instructions burned: 35 (million)
% 7.89/1.68 % (3487794)Instruction limit reached!
% 7.89/1.68 % (3487794)------------------------------
% 7.89/1.68 % (3487794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.89/1.68 % (3487794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487794)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487794)Termination reason: Instruction limit
% 7.89/1.68 % (3487794)Termination phase: Saturation
% 7.89/1.68 % (3487794)Time elapsed: 0.274 s
% 7.89/1.68 % (3487794)Peak memory usage: 14 MB
% 7.89/1.68 % (3487794)Instructions burned: 317 (million)
% 7.89/1.68 % (3487819)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2969227237:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.89/1.68 % (3487821)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 7.89/1.68 % (3487821)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2620579218:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 7.89/1.68 % (3487822)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=970051441:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 7.89/1.68 % (3487819)Instruction limit reached!
% 7.89/1.68 % (3487819)------------------------------
% 7.89/1.68 % (3487819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.89/1.68 % (3487819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487819)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487819)Termination reason: Instruction limit
% 7.89/1.68 % (3487819)Termination phase: Saturation
% 7.89/1.68 % (3487819)Time elapsed: 0.056 s
% 7.89/1.68 % (3487819)Peak memory usage: 12 MB
% 7.89/1.68 % (3487819)Instructions burned: 67 (million)
% 7.89/1.68 % (3487815)Instruction limit reached!
% 7.89/1.68 % (3487815)------------------------------
% 7.89/1.68 % (3487815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.89/1.68 % (3487815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487815)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487815)Termination reason: Instruction limit
% 7.89/1.68 % (3487815)Termination phase: Saturation
% 7.89/1.68 % (3487815)Time elapsed: 0.125 s
% 7.89/1.68 % (3487815)Peak memory usage: 13 MB
% 7.89/1.68 % (3487815)Instructions burned: 138 (million)
% 7.89/1.68 % (3487826)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2428326894:cond=on:i=96:bd=all:rtra=on_2991 on theBenchmark for (2991ds/96Mi)
% 7.89/1.68 % (3487795)Instruction limit reached!
% 7.89/1.68 % (3487795)------------------------------
% 7.89/1.68 % (3487795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.89/1.68 % (3487795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487795)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487795)Termination reason: Instruction limit
% 7.89/1.68 % (3487795)Termination phase: Saturation
% 7.89/1.68 % (3487795)Time elapsed: 0.380 s
% 7.89/1.68 % (3487795)Peak memory usage: 14 MB
% 7.89/1.68 % (3487795)Instructions burned: 855 (million)
% 7.89/1.68 % (3487829)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3295787459:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 7.89/1.68 % (3487827)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1184740403:i=427:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/427Mi)
% 7.89/1.68 % (3487826)Instruction limit reached!
% 7.89/1.68 % (3487826)------------------------------
% 7.89/1.68 % (3487826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.89/1.68 % (3487826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.68 % (3487826)CaDiCaL version: 2.1.3
% 7.89/1.68 % (3487826)Termination reason: Instruction limit
% 7.89/1.68 % (3487826)Termination phase: Saturation
% 7.89/1.68 % (3487826)Time elapsed: 0.050 s
% 7.89/1.68 % (3487826)Peak memory usage: 12 MB
% 7.89/1.68 % (3487826)Instructions burned: 98 (million)
% 7.89/1.68 % (3487821)Instruction limit reached!
% 7.89/1.68 % (3487821)------------------------------
% 7.89/1.68 % (3487821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487821)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487821)Termination reason: Instruction limit
% 9.05/1.78 % (3487821)Termination phase: Saturation
% 9.05/1.78 % (3487821)Time elapsed: 0.138 s
% 9.05/1.78 % (3487821)Peak memory usage: 12 MB
% 9.05/1.78 % (3487821)Instructions burned: 180 (million)
% 9.05/1.78 % (3487801)Instruction limit reached!
% 9.05/1.78 % (3487801)------------------------------
% 9.05/1.78 % (3487801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487801)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487801)Termination reason: Instruction limit
% 9.05/1.78 % (3487801)Termination phase: Saturation
% 9.05/1.78 % (3487801)Time elapsed: 0.414 s
% 9.05/1.78 % (3487801)Peak memory usage: 14 MB
% 9.05/1.78 % (3487801)Instructions burned: 481 (million)
% 9.05/1.78 % (3487832)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1433985115:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/515Mi)
% 9.05/1.78 % (3487833)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2407643973:st=1.5:i=130:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 9.05/1.78 % (3487834)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=522642536:i=44:ep=R:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/44Mi)
% 9.05/1.78 % (3487833)Instruction limit reached!
% 9.05/1.78 % (3487833)------------------------------
% 9.05/1.78 % (3487833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487833)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487833)Termination reason: Instruction limit
% 9.05/1.78 % (3487833)Termination phase: Saturation
% 9.05/1.78 % (3487833)Time elapsed: 0.058 s
% 9.05/1.78 % (3487833)Peak memory usage: 13 MB
% 9.05/1.78 % (3487833)Instructions burned: 130 (million)
% 9.05/1.78 % (3487822)Instruction limit reached!
% 9.05/1.78 % (3487822)------------------------------
% 9.05/1.78 % (3487822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487822)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487822)Termination reason: Instruction limit
% 9.05/1.78 % (3487822)Termination phase: Saturation
% 9.05/1.78 % (3487822)Time elapsed: 0.214 s
% 9.05/1.78 % (3487822)Peak memory usage: 13 MB
% 9.05/1.78 % (3487822)Instructions burned: 247 (million)
% 9.05/1.78 % (3487834)Instruction limit reached!
% 9.05/1.78 % (3487834)------------------------------
% 9.05/1.78 % (3487834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487834)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487834)Termination reason: Instruction limit
% 9.05/1.78 % (3487834)Termination phase: Saturation
% 9.05/1.78 % (3487834)Time elapsed: 0.043 s
% 9.05/1.78 % (3487834)Peak memory usage: 12 MB
% 9.05/1.78 % (3487834)Instructions burned: 45 (million)
% 9.05/1.78 % (3487838)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=352838695:s2a=on:i=571:nm=16:rtra=on_2989 on theBenchmark for (2989ds/571Mi)
% 9.05/1.78 % (3487839)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3867697597:i=450:rtra=on:ixr=off:ntd=on_2989 on theBenchmark for (2989ds/450Mi)
% 9.05/1.78 % (3487840)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1219962288:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/95Mi)
% 9.05/1.78 % (3487838)Refutation not found, incomplete strategy
% 9.05/1.78 % (3487838)------------------------------
% 9.05/1.78 % (3487838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.05/1.78 % (3487838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/1.78 % (3487838)CaDiCaL version: 2.1.3
% 9.05/1.78 % (3487838)Termination reason: Refutation not found, incomplete strategy
% 9.05/1.78 % (3487838)Time elapsed: 0.028 s
% 9.05/1.78 % (3487838)Peak memory usage: 12 MB
% 9.05/1.78 % (3487838)Instructions burned: 28 (million)
% 9.05/1.78 % (3487838)------------------------------
% 9.05/1.78 % (3487838)------------------------------
% 9.74/2.02 % (3487844)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=2099924048:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2989 on theBenchmark for (2989ds/65Mi)
% 9.74/2.02 % (3487840)Instruction limit reached!
% 9.74/2.02 % (3487840)------------------------------
% 9.74/2.02 % (3487840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/2.02 % (3487840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.02 % (3487840)CaDiCaL version: 2.1.3
% 9.74/2.02 % (3487840)Termination reason: Instruction limit
% 9.74/2.02 % (3487840)Termination phase: Saturation
% 9.74/2.02 % (3487840)Time elapsed: 0.087 s
% 9.74/2.02 % (3487840)Peak memory usage: 12 MB
% 9.74/2.02 % (3487840)Instructions burned: 95 (million)
% 9.74/2.02 % (3487844)Instruction limit reached!
% 9.74/2.02 % (3487844)------------------------------
% 9.74/2.02 % (3487844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/2.02 % (3487844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.02 % (3487844)CaDiCaL version: 2.1.3
% 9.74/2.02 % (3487844)Termination reason: Instruction limit
% 9.74/2.02 % (3487844)Termination phase: Saturation
% 9.74/2.02 % (3487844)Time elapsed: 0.059 s
% 9.74/2.02 % (3487844)Peak memory usage: 13 MB
% 9.74/2.02 % (3487844)Instructions burned: 65 (million)
% 9.74/2.02 % (3487846)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=1069818283: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_2988 on theBenchmark for (2988ds/105Mi)
% 9.74/2.02 % (3487847)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=2065777649:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2988 on theBenchmark for (2988ds/5755Mi)
% 9.74/2.02 % (3487827)Instruction limit reached!
% 9.74/2.02 % (3487827)------------------------------
% 9.74/2.02 % (3487827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/2.02 % (3487827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.02 % (3487827)CaDiCaL version: 2.1.3
% 9.74/2.02 % (3487827)Termination reason: Instruction limit
% 9.74/2.02 % (3487827)Termination phase: Saturation
% 9.74/2.02 % (3487827)Time elapsed: 0.349 s
% 9.74/2.02 % (3487827)Peak memory usage: 15 MB
% 9.74/2.02 % (3487827)Instructions burned: 428 (million)
% 9.74/2.02 % (3487846)Instruction limit reached!
% 9.74/2.02 % (3487846)------------------------------
% 9.74/2.02 % (3487846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/2.02 % (3487846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.02 % (3487846)CaDiCaL version: 2.1.3
% 9.74/2.02 % (3487846)Termination reason: Instruction limit
% 9.74/2.02 % (3487846)Termination phase: Saturation
% 9.74/2.02 % (3487846)Time elapsed: 0.093 s
% 9.74/2.02 % (3487846)Peak memory usage: 13 MB
% 9.74/2.02 % (3487846)Instructions burned: 105 (million)
% 9.74/2.02 % (3487850)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2571371165:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/375Mi)
% 9.74/2.02 % (3487829)Instruction limit reached!
% 9.74/2.02 % (3487829)------------------------------
% 9.74/2.02 % (3487829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/2.02 % (3487829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.02 % (3487829)CaDiCaL version: 2.1.3
% 9.74/2.02 % (3487829)Termination reason: Instruction limit
% 9.74/2.02 % (3487829)Termination phase: Saturation
% 9.74/2.02 % (3487829)Time elapsed: 0.403 s
% 9.74/2.02 % (3487829)Peak memory usage: 15 MB
% 9.74/2.02 % (3487829)Instructions burned: 876 (million)
% 9.74/2.02 % (3487852)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1754276651:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/495Mi)
% 9.74/2.02 % (3487853)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=3730073937:cond=on:i=34:hud=10:nm=10:rtra=on_2987 on theBenchmark for (2987ds/34Mi)
% 9.74/2.02 % (3487832)Instruction limit reached!
% 9.74/2.02 % (3487832)------------------------------
% 12.17/2.11 % (3487832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.11 % (3487832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.11 % (3487832)CaDiCaL version: 2.1.3
% 12.17/2.11 % (3487832)Termination reason: Instruction limit
% 12.17/2.11 % (3487832)Termination phase: Saturation
% 12.17/2.11 % (3487832)Time elapsed: 0.402 s
% 12.17/2.11 % (3487832)Peak memory usage: 17 MB
% 12.17/2.11 % (3487832)Instructions burned: 516 (million)
% 12.17/2.11 % (3487853)Instruction limit reached!
% 12.17/2.11 % (3487853)------------------------------
% 12.17/2.11 % (3487853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.11 % (3487853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.11 % (3487853)CaDiCaL version: 2.1.3
% 12.17/2.11 % (3487853)Termination reason: Instruction limit
% 12.17/2.11 % (3487853)Termination phase: Saturation
% 12.17/2.11 % (3487853)Time elapsed: 0.029 s
% 12.17/2.11 % (3487853)Peak memory usage: 13 MB
% 12.17/2.11 % (3487853)Instructions burned: 34 (million)
% 12.17/2.11 % (3487774)Instruction limit reached!
% 12.17/2.12 % (3487774)------------------------------
% 12.17/2.12 % (3487774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.12 % (3487774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.12 % (3487774)CaDiCaL version: 2.1.3
% 12.17/2.12 % (3487774)Termination reason: Instruction limit
% 12.17/2.12 % (3487774)Termination phase: Saturation
% 12.17/2.12 % (3487774)Time elapsed: 1.043 s
% 12.17/2.12 % (3487774)Peak memory usage: 16 MB
% 12.17/2.12 % (3487774)Instructions burned: 1241 (million)
% 12.17/2.12 % (3487857)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=379883358:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2986 on theBenchmark for (2986ds/66Mi)
% 12.17/2.12 % (3487856)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1673538858:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 12.17/2.12 % (3487839)Instruction limit reached!
% 12.17/2.12 % (3487839)------------------------------
% 12.17/2.12 % (3487839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.12 % (3487839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.12 % (3487839)CaDiCaL version: 2.1.3
% 12.17/2.12 % (3487839)Termination reason: Instruction limit
% 12.17/2.12 % (3487839)Termination phase: Saturation
% 12.17/2.12 % (3487839)Time elapsed: 0.356 s
% 12.17/2.12 % (3487839)Peak memory usage: 14 MB
% 12.17/2.12 % (3487839)Instructions burned: 451 (million)
% 12.17/2.12 % (3487857)Instruction limit reached!
% 12.17/2.12 % (3487857)------------------------------
% 12.17/2.12 % (3487857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.12 % (3487857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.12 % (3487857)CaDiCaL version: 2.1.3
% 12.17/2.12 % (3487857)Termination reason: Instruction limit
% 12.17/2.12 % (3487857)Termination phase: Saturation
% 12.17/2.12 % (3487857)Time elapsed: 0.030 s
% 12.17/2.12 % (3487857)Peak memory usage: 12 MB
% 12.17/2.12 % (3487857)Instructions burned: 66 (million)
% 12.17/2.12 % (3487859)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=467006326:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2986 on theBenchmark for (2986ds/22Mi)
% 12.17/2.12 % (3487859)Instruction limit reached!
% 12.17/2.12 % (3487859)------------------------------
% 12.17/2.12 % (3487859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.12 % (3487859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.12 % (3487859)CaDiCaL version: 2.1.3
% 12.17/2.12 % (3487859)Termination reason: Instruction limit
% 12.17/2.12 % (3487859)Termination phase: Saturation
% 12.17/2.12 % (3487859)Time elapsed: 0.019 s
% 12.17/2.12 % (3487859)Peak memory usage: 12 MB
% 12.17/2.12 % (3487859)Instructions burned: 22 (million)
% 12.17/2.12 % (3487861)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=2517656591:i=338:bd=all:ins=4:rtra=on_2986 on theBenchmark for (2986ds/338Mi)
% 12.17/2.12 % (3487862)lrs+10_1_sil=128000:si=on:urr=on:random_seed=22234973:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 12.17/2.12 % (3487864)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.58/2.49 % (3487864)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3577029908:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/137Mi)
% 13.58/2.49 % (3487856)Instruction limit reached!
% 13.58/2.49 % (3487856)------------------------------
% 13.58/2.49 % (3487856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.49 % (3487856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.49 % (3487856)CaDiCaL version: 2.1.3
% 13.58/2.49 % (3487856)Termination reason: Instruction limit
% 13.58/2.49 % (3487856)Termination phase: Saturation
% 13.58/2.49 % (3487856)Time elapsed: 0.078 s
% 13.58/2.49 % (3487856)Peak memory usage: 12 MB
% 13.58/2.49 % (3487856)Instructions burned: 92 (million)
% 13.58/2.49 % (3487862)Instruction limit reached!
% 13.58/2.49 % (3487862)------------------------------
% 13.58/2.49 % (3487862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.49 % (3487862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.49 % (3487862)CaDiCaL version: 2.1.3
% 13.58/2.49 % (3487862)Termination reason: Instruction limit
% 13.58/2.49 % (3487862)Termination phase: Saturation
% 13.58/2.49 % (3487862)Time elapsed: 0.026 s
% 13.58/2.49 % (3487862)Peak memory usage: 12 MB
% 13.58/2.49 % (3487862)Instructions burned: 28 (million)
% 13.58/2.49 % (3487868)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=1884218577:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 13.58/2.49 % (3487869)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2731951185:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 13.58/2.49 % (3487864)Instruction limit reached!
% 13.58/2.49 % (3487864)------------------------------
% 13.58/2.49 % (3487864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.49 % (3487864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.49 % (3487864)CaDiCaL version: 2.1.3
% 13.58/2.49 % (3487864)Termination reason: Instruction limit
% 13.58/2.49 % (3487864)Termination phase: Saturation
% 13.58/2.49 % (3487864)Time elapsed: 0.111 s
% 13.58/2.49 % (3487864)Peak memory usage: 12 MB
% 13.58/2.49 % (3487864)Instructions burned: 138 (million)
% 13.58/2.49 % (3487872)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.58/2.49 % (3487872)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=464801615:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/373Mi)
% 13.58/2.49 % (3487868)Instruction limit reached!
% 13.58/2.49 % (3487868)------------------------------
% 13.58/2.49 % (3487868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.49 % (3487868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.49 % (3487868)CaDiCaL version: 2.1.3
% 13.58/2.49 % (3487868)Termination reason: Instruction limit
% 13.58/2.49 % (3487868)Termination phase: Saturation
% 13.58/2.49 % (3487868)Time elapsed: 0.134 s
% 13.58/2.49 % (3487868)Peak memory usage: 13 MB
% 13.58/2.49 % (3487868)Instructions burned: 342 (million)
% 13.58/2.49 % (3487850)Instruction limit reached!
% 13.58/2.49 % (3487850)------------------------------
% 13.58/2.49 % (3487850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.49 % (3487850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.49 % (3487850)CaDiCaL version: 2.1.3
% 13.58/2.49 % (3487850)Termination reason: Instruction limit
% 13.58/2.49 % (3487850)Termination phase: Saturation
% 13.58/2.49 % (3487850)Time elapsed: 0.359 s
% 13.58/2.49 % (3487850)Peak memory usage: 14 MB
% 13.58/2.49 % (3487850)Instructions burned: 375 (million)
% 13.58/2.49 % (3487874)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2717284884:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 13.58/2.49 % (3487876)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=37231378:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 13.58/2.49 % (3487869)Instruction limit reached!
% 13.58/2.49 % (3487869)------------------------------
% 13.58/2.49 % (3487869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487869)CaDiCaL version: 2.1.3
% 15.80/2.96 % (3487869)Termination reason: Instruction limit
% 15.80/2.96 % (3487869)Termination phase: Saturation
% 15.80/2.96 % (3487869)Time elapsed: 0.192 s
% 15.80/2.96 % (3487869)Peak memory usage: 13 MB
% 15.80/2.96 % (3487869)Instructions burned: 228 (million)
% 15.80/2.96 % (3487852)Instruction limit reached!
% 15.80/2.96 % (3487852)------------------------------
% 15.80/2.96 % (3487852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487852)CaDiCaL version: 2.1.3
% 15.80/2.96 % (3487852)Termination reason: Instruction limit
% 15.80/2.96 % (3487852)Termination phase: Saturation
% 15.80/2.96 % (3487852)Time elapsed: 0.406 s
% 15.80/2.96 % (3487852)Peak memory usage: 14 MB
% 15.80/2.96 % (3487852)Instructions burned: 496 (million)
% 15.80/2.96 % (3487878)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2915253554:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2983 on theBenchmark for (2983ds/270Mi)
% 15.80/2.96 % (3487874)Instruction limit reached!
% 15.80/2.96 % (3487874)------------------------------
% 15.80/2.96 % (3487874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487874)CaDiCaL version: 2.1.3
% 15.80/2.96 % (3487874)Termination reason: Instruction limit
% 15.80/2.96 % (3487874)Termination phase: Saturation
% 15.80/2.96 % (3487874)Time elapsed: 0.093 s
% 15.80/2.96 % (3487874)Peak memory usage: 12 MB
% 15.80/2.96 % (3487874)Instructions burned: 117 (million)
% 15.80/2.96 % (3487861)Instruction limit reached!
% 15.80/2.96 % (3487861)------------------------------
% 15.80/2.96 % (3487861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487861)CaDiCaL version: 2.1.3
% 15.80/2.96 % (3487861)Termination reason: Instruction limit
% 15.80/2.96 % (3487861)Termination phase: Saturation
% 15.80/2.96 % (3487861)Time elapsed: 0.303 s
% 15.80/2.96 % (3487861)Peak memory usage: 16 MB
% 15.80/2.96 % (3487861)Instructions burned: 338 (million)
% 15.80/2.96 % (3487879)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=1787749536:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2982 on theBenchmark for (2982ds/9840Mi)
% 15.80/2.96 % (3487872)Instruction limit reached!
% 15.80/2.96 % (3487872)------------------------------
% 15.80/2.96 % (3487872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487883)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 15.80/2.96 % (3487872)CaDiCaL version: 2.1.3
% 15.80/2.96 % (3487872)Termination reason: Instruction limit
% 15.80/2.96 % (3487872)Termination phase: Saturation
% 15.80/2.96 % (3487872)Time elapsed: 0.157 s
% 15.80/2.96 % (3487872)Peak memory usage: 15 MB
% 15.80/2.96 % (3487872)Instructions burned: 375 (million)
% 15.80/2.96 % (3487883)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=987503972:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 15.80/2.96 % (3487882)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2872737643:i=421:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/421Mi)
% 15.80/2.96 % (3487885)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3508279674:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 15.80/2.96 % (3487885)Instruction limit reached!
% 15.80/2.96 % (3487885)------------------------------
% 15.80/2.96 % (3487885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.96 % (3487885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.96 % (3487885)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487885)Termination reason: Instruction limit
% 15.80/2.99 % (3487885)Termination phase: Saturation
% 15.80/2.99 % (3487885)Time elapsed: 0.014 s
% 15.80/2.99 % (3487885)Peak memory usage: 12 MB
% 15.80/2.99 % (3487885)Instructions burned: 31 (million)
% 15.80/2.99 % (3487890)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 15.80/2.99 % (3487890)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
% 15.80/2.99 % (3487890)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=2240048426:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2982 on theBenchmark for (2982ds/1440Mi)
% 15.80/2.99 % (3487878)Instruction limit reached!
% 15.80/2.99 % (3487878)------------------------------
% 15.80/2.99 % (3487878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487878)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487878)Termination reason: Instruction limit
% 15.80/2.99 % (3487878)Termination phase: Saturation
% 15.80/2.99 % (3487878)Time elapsed: 0.214 s
% 15.80/2.99 % (3487878)Peak memory usage: 13 MB
% 15.80/2.99 % (3487878)Instructions burned: 270 (million)
% 15.80/2.99 % (3487894)dis+10_2_sil=128000:si=on:random_seed=1239586225:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2980 on theBenchmark for (2980ds/339Mi)
% 15.80/2.99 % (3487883)Instruction limit reached!
% 15.80/2.99 % (3487883)------------------------------
% 15.80/2.99 % (3487883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487883)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487883)Termination reason: Instruction limit
% 15.80/2.99 % (3487883)Termination phase: Saturation
% 15.80/2.99 % (3487883)Time elapsed: 0.209 s
% 15.80/2.99 % (3487883)Peak memory usage: 13 MB
% 15.80/2.99 % (3487883)Instructions burned: 270 (million)
% 15.80/2.99 % (3487896)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2542936385:i=111:add=on:fgj=on:rtra=on:fdi=1024_2980 on theBenchmark for (2980ds/111Mi)
% 15.80/2.99 % (3487896)Instruction limit reached!
% 15.80/2.99 % (3487896)------------------------------
% 15.80/2.99 % (3487896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487896)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487896)Termination reason: Instruction limit
% 15.80/2.99 % (3487896)Termination phase: Saturation
% 15.80/2.99 % (3487896)Time elapsed: 0.098 s
% 15.80/2.99 % (3487896)Peak memory usage: 13 MB
% 15.80/2.99 % (3487896)Instructions burned: 111 (million)
% 15.80/2.99 % (3487882)Instruction limit reached!
% 15.80/2.99 % (3487882)------------------------------
% 15.80/2.99 % (3487882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487882)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487882)Termination reason: Instruction limit
% 15.80/2.99 % (3487882)Termination phase: Saturation
% 15.80/2.99 % (3487882)Time elapsed: 0.351 s
% 15.80/2.99 % (3487882)Peak memory usage: 14 MB
% 15.80/2.99 % (3487882)Instructions burned: 421 (million)
% 15.80/2.99 % (3487898)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=901099487:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/122Mi)
% 15.80/2.99 % (3487876)Instruction limit reached!
% 15.80/2.99 % (3487876)------------------------------
% 15.80/2.99 % (3487876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487876)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487876)Termination reason: Instruction limit
% 15.80/2.99 % (3487876)Termination phase: Saturation
% 15.80/2.99 % (3487876)Time elapsed: 0.475 s
% 15.80/2.99 % (3487876)Peak memory usage: 14 MB
% 15.80/2.99 % (3487876)Instructions burned: 575 (million)
% 15.80/2.99 % (3487899)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=1938146060:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/136Mi)
% 15.80/2.99 % (3487901)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=375226038:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/232Mi)
% 15.80/2.99 % (3487899)Instruction limit reached!
% 15.80/2.99 % (3487899)------------------------------
% 15.80/2.99 % (3487899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487899)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487899)Termination reason: Instruction limit
% 15.80/2.99 % (3487899)Termination phase: Property scanning
% 15.80/2.99 % (3487899)Time elapsed: 0.085 s
% 15.80/2.99 % (3487899)Peak memory usage: 10 MB
% 15.80/2.99 % (3487899)Instructions burned: 138 (million)
% 15.80/2.99 % (3487898)Instruction limit reached!
% 15.80/2.99 % (3487898)------------------------------
% 15.80/2.99 % (3487898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487898)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487898)Termination reason: Instruction limit
% 15.80/2.99 % (3487898)Termination phase: Saturation
% 15.80/2.99 % (3487898)Time elapsed: 0.113 s
% 15.80/2.99 % (3487898)Peak memory usage: 13 MB
% 15.80/2.99 % (3487898)Instructions burned: 122 (million)
% 15.80/2.99 % (3487894)Instruction limit reached!
% 15.80/2.99 % (3487894)------------------------------
% 15.80/2.99 % (3487894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487894)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487894)Termination reason: Instruction limit
% 15.80/2.99 % (3487894)Termination phase: Saturation
% 15.80/2.99 % (3487894)Time elapsed: 0.285 s
% 15.80/2.99 % (3487894)Peak memory usage: 13 MB
% 15.80/2.99 % (3487894)Instructions burned: 340 (million)
% 15.80/2.99 % (3487906)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=3922873366:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2977 on theBenchmark for (2977ds/1254Mi)
% 15.80/2.99 % (3487907)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 15.80/2.99 % (3487907)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=991691492:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 15.80/2.99 % (3487908)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3654974879:i=619:add=on:rtra=on_2977 on theBenchmark for (2977ds/619Mi)
% 15.80/2.99 % (3487901)Instruction limit reached!
% 15.80/2.99 % (3487901)------------------------------
% 15.80/2.99 % (3487901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487901)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487901)Termination reason: Instruction limit
% 15.80/2.99 % (3487901)Termination phase: Saturation
% 15.80/2.99 % (3487901)Time elapsed: 0.212 s
% 15.80/2.99 % (3487901)Peak memory usage: 13 MB
% 15.80/2.99 % (3487901)Instructions burned: 233 (million)
% 15.80/2.99 % (3487914)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=1601244403:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/865Mi)
% 15.80/2.99 % (3487907)Instruction limit reached!
% 15.80/2.99 % (3487907)------------------------------
% 15.80/2.99 % (3487907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487907)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487907)Termination reason: Instruction limit
% 15.80/2.99 % (3487907)Termination phase: Saturation
% 15.80/2.99 % (3487907)Time elapsed: 0.220 s
% 15.80/2.99 % (3487907)Peak memory usage: 12 MB
% 15.80/2.99 % (3487907)Instructions burned: 282 (million)
% 15.80/2.99 % (3487916)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2410491969:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/212Mi)
% 15.80/2.99 % (3487914) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3487707-3487914"...
% 15.80/2.99 % (3487914)...printing done.
% 15.80/2.99 % (3487914)Refutation found. Thanks to Tanya!
% 15.80/2.99 % SZS status Theorem for theBenchmark
% 15.80/2.99 % SZS output start Proof for theBenchmark
% See solution above
% 15.80/2.99 % (3487914)------------------------------
% 15.80/2.99 % (3487914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.99 % (3487914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.99 % (3487914)CaDiCaL version: 2.1.3
% 15.80/2.99 % (3487914)Termination reason: Refutation
% 15.80/2.99 % (3487914)Time elapsed: 0.238 s
% 15.80/2.99 % (3487914)Peak memory usage: 16 MB
% 15.80/2.99 % (3487914)Instructions burned: 381 (million)
% 15.80/2.99 % (3487707)Success in time 2.659 s
% 15.80/2.99 % Vampire exiting
%------------------------------------------------------------------------------