%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEU960^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 09:37:51 AM UTC 2026
% Result : Theorem 1.43s 1.64s
% Output : Refutation 1.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 1
% Syntax : Number of formulae : 45 ( 42 unt; 0 typ; 0 def)
% Number of atoms : 230 ( 41 equ; 0 cnn)
% Maximal formula atoms : 1 ( 5 avg)
% Number of connectives : 923 ( 5 ~; 0 |; 68 &; 632 @)
% ( 0 <=>; 125 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 2 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 323 ( 323 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 6 usr; 3 con; 0-2 aty)
% ( 93 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 246 ( 213 ^; 33 !; 0 ?; 246 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(func_def_0,type,
a: $tType ).
thf(func_def_14,type,
ph0:
!>[X0: $tType] : X0 ).
thf(func_def_15,type,
sK1: a > a ).
thf(func_def_16,type,
sK2: a > a ).
thf(func_def_17,type,
sK3: a > a ).
thf(func_def_18,type,
sK4: ( a > a ) > $o ).
thf(func_def_21,type,
sK5: a > a ).
thf(f334,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f317]) ).
thf(f317,plain,
$false = $true,
inference(superposition,[status(thm)],[f294,f98]) ).
thf(f98,plain,
! [X1: a > a] :
( $true
= ( ( sK4 @ X1 )
=> ( sK4
@ ^ [Y0: a] : ( sK1 @ ( X1 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f88]) ).
thf(f88,plain,
! [X1: a > a] :
( ( ^ [Y0: a > a] :
( ( sK4 @ Y0 )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f30]) ).
thf(f30,plain,
( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4 @ Y0 )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f23]) ).
thf(f23,plain,
( ( ( sK4 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4 @ Y0 )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) ) )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f20]) ).
thf(f20,plain,
( $false
= ( ( ( sK4 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4 @ Y0 )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) ) )
=> ( sK4
@ ^ [Y0: a] : ( sK3 @ ( sK2 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f18]) ).
thf(f18,plain,
( $false
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0
@ ^ [Y1: a] : ( sK3 @ ( sK2 @ Y1 ) ) ) )
@ sK4 ) ),
inference(sigma_clausification,[status(thm)],[f16]) ).
thf(f16,plain,
( $false
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0
@ ^ [Y1: a] : ( sK3 @ ( sK2 @ Y1 ) ) ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f15]) ).
thf(f15,plain,
( $false
= ( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK1 ) )
=> ( Y0 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK3 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0
@ ^ [Y1: a] : ( sK3 @ ( sK2 @ Y1 ) ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f14]) ).
thf(f14,plain,
( ( ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK1 ) )
=> ( Y1 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1
@ ^ [Y2: a] : ( Y0 @ ( sK2 @ Y2 ) ) ) ) ) )
@ sK3 )
= $false ),
inference(sigma_clausification,[status(thm)],[f13]) ).
thf(f13,plain,
( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK1 ) )
=> ( Y1 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK1 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1
@ ^ [Y2: a] : ( Y0 @ ( sK2 @ Y2 ) ) ) ) ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f12]) ).
thf(f12,plain,
( ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK1 ) )
=> ( Y2 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2
@ ^ [Y3: a] : ( Y1 @ ( Y0 @ Y3 ) ) ) ) ) ) )
@ sK2 )
= $false ),
inference(sigma_clausification,[status(thm)],[f10]) ).
thf(f10,plain,
( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK1 ) )
=> ( Y2 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK1 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2
@ ^ [Y3: a] : ( Y1 @ ( Y0 @ Y3 ) ) ) ) ) ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f8]) ).
thf(f8,plain,
( $false
= ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) )
@ sK1 ) ),
inference(sigma_clausification,[status(thm)],[f7]) ).
thf(f7,plain,
( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f6]) ).
thf(f6,plain,
( $true
= ( ~ ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
thf(f5,plain,
( $true
= ( ~ ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3 @ Y0 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ! [X0: a > a,X1: a > a,X2: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X2 @ ( X4 @ X5 ) ) ) )
& ( X3 @ X2 ) )
=> ( X3 @ X0 ) )
& ! [X6: ( a > a ) > $o] :
( ( ( X6 @ X2 )
& ! [X7: a > a] :
( ( X6 @ X7 )
=> ( X6
@ ^ [X8: a] : ( X2 @ ( X7 @ X8 ) ) ) ) )
=> ( X6 @ X1 ) ) )
=> ! [X9: ( a > a ) > $o] :
( ( ! [X10: a > a] :
( ( X9 @ X10 )
=> ( X9
@ ^ [X11: a] : ( X2 @ ( X10 @ X11 ) ) ) )
& ( X9 @ X2 ) )
=> ( X9
@ ^ [X12: a] : ( X0 @ ( X1 @ X12 ) ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ! [X1: a > a,X2: a > a,X0: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) )
& ( X3 @ X0 ) )
=> ( X3 @ X1 ) )
& ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X2 ) ) )
=> ! [X3: ( a > a ) > $o] :
( ( ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) )
& ( X3 @ X0 ) )
=> ( X3
@ ^ [X5: a] : ( X1 @ ( X2 @ X5 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
! [X1: a > a,X2: a > a,X0: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) )
& ( X3 @ X0 ) )
=> ( X3 @ X1 ) )
& ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X2 ) ) )
=> ! [X3: ( a > a ) > $o] :
( ( ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) )
& ( X3 @ X0 ) )
=> ( X3
@ ^ [X5: a] : ( X1 @ ( X2 @ X5 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.HXTQGiCcwm/DTF2THF_9779.p',cTHM135D_pme) ).
thf(f294,plain,
( $false
= ( ( sK4
@ ^ [Y0: a] : ( sK5 @ ( sK2 @ Y0 ) ) )
=> ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK5 @ ( sK2 @ Y0 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f285]) ).
thf(f285,plain,
( ( ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) )
@ sK5 )
= $false ),
inference(sigma_clausification,[status(thm)],[f267]) ).
thf(f267,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f266]) ).
thf(f266,plain,
( $false
= ( $true
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ) ),
inference(forward_demodulation,[status(thm)],[f243,f203]) ).
thf(f203,plain,
( ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f185]) ).
thf(f185,plain,
( ( $true
=> ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) ) )
= $true ),
inference(superposition,[status(thm)],[f98,f156]) ).
thf(f156,plain,
( ( sK4 @ sK2 )
= $true ),
inference(boolean_simplification,[status(thm)],[f155]) ).
thf(f155,plain,
( ( $true
=> ( sK4 @ sK2 ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f148,f31]) ).
thf(f31,plain,
( ( sK4 @ sK1 )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f23]) ).
thf(f148,plain,
( ( ( sK4 @ sK1 )
=> ( sK4 @ sK2 ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f147]) ).
thf(f147,plain,
( ( ( $true
& ( sK4 @ sK1 ) )
=> ( sK4 @ sK2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f120]) ).
thf(f120,plain,
( ( ( $true
& ( ^ [Y0: a > a] :
( sK4
@ ( ^ [Y1: a > a] : Y1
@ Y0 ) )
@ sK1 ) )
=> ( ^ [Y0: a > a] :
( sK4
@ ( ^ [Y1: a > a] : Y1
@ Y0 ) )
@ sK2 ) )
= $true ),
inference(superposition,[status(thm)],[f83,f30]) ).
thf(f83,plain,
! [X1: ( a > a ) > $o] :
( ( ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) )
& ( X1 @ sK1 ) )
=> ( X1 @ sK2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f80]) ).
thf(f80,plain,
! [X1: ( a > a ) > $o] :
( $true
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK1 ) )
=> ( Y0 @ sK2 ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f27]) ).
thf(f27,plain,
( $true
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK1 ) )
=> ( Y0 @ sK2 ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f17]) ).
thf(f17,plain,
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK1 ) )
=> ( Y0 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK3 ) ) ) )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f15]) ).
thf(f243,plain,
( $false
= ( ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[status(thm)],[f68]) ).
thf(f68,plain,
( $true
= ( ~ ( ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f67]) ).
thf(f67,plain,
( ( ( ( sK4
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK4
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK4
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) )
=> $false )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f50]) ).
thf(f50,plain,
( ( ( ( ^ [Y0: a > a] :
( sK4
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] :
( sK2
@ ( ^ [Y5: a > a,Y6: a] : Y6
@ Y3
@ Y4 ) )
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK1 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ^ [Y1: a > a] :
( sK4
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK2
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ Y0 )
=> ( ^ [Y1: a > a] :
( sK4
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK2
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) ) )
=> $false )
= $true ),
inference(superposition,[status(thm)],[f39,f22]) ).
thf(f22,plain,
( $false
= ( sK4
@ ^ [Y0: a] : ( sK3 @ ( sK2 @ Y0 ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f20]) ).
thf(f39,plain,
! [X1: ( a > a ) > $o] :
( ( ( ( X1 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK1 @ ( Y0 @ Y1 ) ) ) ) ) )
=> ( X1 @ sK3 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f34]) ).
thf(f34,plain,
! [X1: ( a > a ) > $o] :
( ( ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK3 ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f26]) ).
thf(f26,plain,
( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0 @ sK1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK1 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK3 ) ) )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEU960^5 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.31 % Computer : n022.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Tue Feb 24 12:37:36 EST 2026
% 0.12/0.32 % CPUTime :
% 0.12/0.32 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 ---- Original DTF file ---
% 0.16/0.42 thf(spec,logic,$$dhol).
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 % File : SEU960^5 : TPTP v9.2.1. Released v4.0.0.
% 0.16/0.42 % Domain : Set Theory (Functions)
% 0.16/0.42 % Problem : TPS problem from FUNCTION-THMS
% 0.16/0.42 % Version : Especial.
% 0.16/0.42 % English :
% 0.16/0.42
% 0.16/0.42 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.16/0.42 % Source : [Bro09]
% 0.16/0.42 % Names : tps_1017 [Bro09]
% 0.16/0.42 % : tps_1024 [Bro09]
% 0.16/0.42
% 0.16/0.42 % Status : Theorem
% 0.16/0.42 % Rating : 0.42 v9.1.0, 0.50 v9.0.0, 0.42 v8.2.0, 0.45 v8.1.0, 0.58 v7.4.0, 0.44 v7.3.0, 0.60 v7.2.0, 0.50 v7.1.0, 0.43 v7.0.0, 0.50 v6.4.0, 0.43 v6.3.0, 0.50 v6.2.0, 0.67 v5.5.0, 0.80 v5.4.0, 1.00 v4.0.0
% 0.16/0.42 % Syntax : Number of formulae : 2 ( 0 unt; 1 typ; 0 def)
% 0.16/0.42 % Number of atoms : 0 ( 0 equ; 0 cnn)
% 0.16/0.42 % Maximal formula atoms : 0 ( 0 avg)
% 0.16/0.42 % Number of connectives : 31 ( 0 ~; 0 |; 4 &; 20 @)
% 0.16/0.42 % ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% 0.16/0.42 % Maximal formula depth : 15 ( 15 avg)
% 0.16/0.42 % Number of types : 2 ( 1 usr)
% 0.16/0.42 % Number of type conns : 12 ( 12 >; 0 *; 0 +; 0 <<)
% 0.16/0.42 % Number of symbols : 0 ( 0 usr; 0 con; --- aty)
% 0.16/0.42 % Number of variables : 13 ( 4 ^; 9 !; 0 ?; 13 :)
% 0.16/0.42 % SPC : TH0_THM_NEQ_NAR
% 0.16/0.42
% 0.16/0.42 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.16/0.42 % project in the Department of Mathematical Sciences at Carnegie
% 0.16/0.42 % Mellon University. Distributed under the Creative Commons copyleft
% 0.16/0.42 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 thf(a_type,type,
% 0.16/0.42 a: $tType ).
% 0.16/0.42
% 0.16/0.42 thf(cTHM135D_pme,conjecture,
% 0.16/0.42 ! [Xf: a > a,Xg1: a > a,Xg2: a > a] :
% 0.16/0.42 ( ( ! [Xp: ( a > a ) > $o] :
% 0.16/0.42 ( ( ( Xp @ Xf )
% 0.16/0.42 & ! [Xj: a > a] :
% 0.16/0.42 ( ( Xp @ Xj )
% 0.16/0.42 => ( Xp
% 0.16/0.42 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 0.16/0.42 => ( Xp @ Xg1 ) )
% 0.16/0.42 & ! [Xp: ( a > a ) > $o] :
% 0.16/0.42 ( ( ( Xp @ Xf )
% 0.16/0.42 & ! [Xj: a > a] :
% 0.16/0.42 ( ( Xp @ Xj )
% 0.16/0.42 => ( Xp
% 0.16/0.42 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 0.16/0.42 => ( Xp @ Xg2 ) ) )
% 0.16/0.42 => ! [Xp: ( a > a ) > $o] :
% 0.16/0.42 ( ( ( Xp @ Xf )
% 0.16/0.42 & ! [Xj: a > a] :
% 0.16/0.42 ( ( Xp @ Xj )
% 0.16/0.42 => ( Xp
% 0.16/0.42 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 0.16/0.42 => ( Xp
% 0.16/0.42 @ ^ [Xx: a] : ( Xg1 @ ( Xg2 @ Xx ) ) ) ) ) ).
% 0.16/0.42
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 ------------------------
% 1.32/1.18 ---- Embedded in THF ---
% 1.32/1.18 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.32/1.18 %%% Generated on Tue Feb 24 12:37:36 EST 2026
% 1.32/1.18 %%% using '$$dhol' embedding, version 1.3.0.
% 1.32/1.18 %%% Logic specification used:
% 1.32/1.18 %%% thf(spec, logic, $$dhol).
% 1.32/1.18
% 1.32/1.18 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.HXTQGiCcwm/DTF2DTF9779.p
% See solution above
% 1.32/1.18 ------------------------
% 1.32/1.19 ---- Cleaned THF ---
% 1.32/1.19 thf(a_type,type,
% 1.32/1.19 a: $tType ).
% 1.32/1.19
% 1.32/1.19 thf(cTHM135D_pme,conjecture,
% 1.32/1.19 ! [Xf: a > a,Xg1: a > a,Xg2: a > a] :
% 1.32/1.19 ( ( ! [Xp: ( a > a ) > $o] :
% 1.32/1.19 ( ( ( Xp @ Xf )
% 1.32/1.19 & ! [Xj: a > a] :
% 1.32/1.19 ( ( Xp @ Xj )
% 1.32/1.19 => ( Xp
% 1.32/1.19 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 1.32/1.19 => ( Xp @ Xg1 ) )
% 1.32/1.19 & ! [Xp: ( a > a ) > $o] :
% 1.32/1.19 ( ( ( Xp @ Xf )
% 1.32/1.19 & ! [Xj: a > a] :
% 1.32/1.19 ( ( Xp @ Xj )
% 1.32/1.19 => ( Xp
% 1.32/1.19 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 1.32/1.19 => ( Xp @ Xg2 ) ) )
% 1.32/1.19 => ! [Xp: ( a > a ) > $o] :
% 1.32/1.19 ( ( ( Xp @ Xf )
% 1.32/1.19 & ! [Xj: a > a] :
% 1.32/1.19 ( ( Xp @ Xj )
% 1.32/1.19 => ( Xp
% 1.32/1.19 @ ^ [Xx: a] : ( Xf @ ( Xj @ Xx ) ) ) ) )
% 1.32/1.19 => ( Xp
% 1.32/1.19 @ ^ [Xx: a] : ( Xg1 @ ( Xg2 @ Xx ) ) ) ) ) ).
% 1.32/1.19 ------------------------
% 1.43/1.20 % (9878)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/183Mi)
% 1.43/1.21 % (9879)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/4Mi)
% 1.43/1.21 % (9880)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/27Mi)
% 1.43/1.21 % (9882)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/2Mi)
% 1.43/1.21 % (9881)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/2Mi)
% 1.43/1.21 % (9883)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/275Mi)
% 1.43/1.21 % (9884)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_9779 for (3000ds/18Mi)
% 1.43/1.21 % (9881)Instruction limit reached!
% 1.43/1.21 % (9881)------------------------------
% 1.43/1.21 % (9881)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.21 % (9881)Termination reason: Unknown
% 1.43/1.21 % (9881)Termination phase: Preprocessing 2
% 1.43/1.21 % (9882)Instruction limit reached!
% 1.43/1.21 % (9882)------------------------------
% 1.43/1.21 % (9882)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.21 % (9882)Termination reason: Unknown
% 1.43/1.21 % (9882)Termination phase: Property scanning
% 1.43/1.21
% 1.43/1.21 % (9882)Memory used [KB]: 895
% 1.43/1.21 % (9882)Time elapsed: 0.002 s
% 1.43/1.21 % (9882)Instructions burned: 2 (million)
% 1.43/1.21 % (9882)------------------------------
% 1.43/1.21 % (9882)------------------------------
% 1.43/1.21
% 1.43/1.21 % (9881)Memory used [KB]: 895
% 1.43/1.21 % (9881)Time elapsed: 0.002 s
% 1.43/1.21 % (9881)Instructions burned: 2 (million)
% 1.43/1.21 % (9881)------------------------------
% 1.43/1.21 % (9881)------------------------------
% 1.43/1.21 % (9879)Instruction limit reached!
% 1.43/1.21 % (9879)------------------------------
% 1.43/1.21 % (9879)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.21 % (9879)Termination reason: Unknown
% 1.43/1.21 % (9879)Termination phase: Saturation
% 1.43/1.21
% 1.43/1.21 % (9879)Memory used [KB]: 5500
% 1.43/1.21 % (9879)Time elapsed: 0.004 s
% 1.43/1.21 % (9879)Instructions burned: 4 (million)
% 1.43/1.21 % (9879)------------------------------
% 1.43/1.21 % (9879)------------------------------
% 1.43/1.22 % (9884)Instruction limit reached!
% 1.43/1.22 % (9884)------------------------------
% 1.43/1.22 % (9884)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.22 % (9884)Termination reason: Unknown
% 1.43/1.22 % (9884)Termination phase: Saturation
% 1.43/1.22
% 1.43/1.22 % (9884)Memory used [KB]: 5628
% 1.43/1.22 % (9884)Time elapsed: 0.011 s
% 1.43/1.22 % (9884)Instructions burned: 18 (million)
% 1.43/1.22 % (9884)------------------------------
% 1.43/1.22 % (9884)------------------------------
% 1.43/1.22 % (9880)Instruction limit reached!
% 1.43/1.22 % (9880)------------------------------
% 1.43/1.22 % (9880)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.22 % (9880)Termination reason: Unknown
% 1.43/1.22 % (9880)Termination phase: Saturation
% 1.43/1.22
% 1.43/1.22 % (9880)Memory used [KB]: 5628
% 1.43/1.22 % (9880)Time elapsed: 0.015 s
% 1.43/1.22 % (9880)Instructions burned: 27 (million)
% 1.43/1.22 % (9880)------------------------------
% 1.43/1.22 % (9880)------------------------------
% 1.43/1.22 % (9883)Refutation not found, incomplete strategy
% 1.43/1.22 % (9883)------------------------------
% 1.43/1.22 % (9883)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.22 % (9883)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.22
% 1.43/1.22
% 1.43/1.22 % (9883)Memory used [KB]: 5628
% 1.43/1.22 % (9883)Time elapsed: 0.016 s
% 1.43/1.22 % (9883)Instructions burned: 27 (million)
% 1.43/1.22 % (9883)------------------------------
% 1.43/1.22 % (9883)------------------------------
% 1.43/1.23 % (9886)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/37Mi)
% 1.43/1.23 % (9885)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/3Mi)
% 1.43/1.23 % (9885)Instruction limit reached!
% 1.43/1.23 % (9885)------------------------------
% 1.43/1.23 % (9885)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.23 % (9885)Termination reason: Unknown
% 1.43/1.23 % (9885)Termination phase: Saturation
% 1.43/1.23
% 1.43/1.23 % (9885)Memory used [KB]: 5500
% 1.43/1.23 % (9885)Time elapsed: 0.003 s
% 1.43/1.23 % (9885)Instructions burned: 3 (million)
% 1.43/1.23 % (9885)------------------------------
% 1.43/1.23 % (9885)------------------------------
% 1.43/1.23 % (9887)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/15Mi)
% 1.43/1.24 % (9888)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/3Mi)
% 1.43/1.24 % (9888)Instruction limit reached!
% 1.43/1.24 % (9888)------------------------------
% 1.43/1.24 % (9888)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.24 % (9888)Termination reason: Unknown
% 1.43/1.24 % (9888)Termination phase: Saturation
% 1.43/1.24
% 1.43/1.24 % (9888)Memory used [KB]: 5500
% 1.43/1.24 % (9888)Time elapsed: 0.003 s
% 1.43/1.24 % (9888)Instructions burned: 3 (million)
% 1.43/1.24 % (9888)------------------------------
% 1.43/1.24 % (9888)------------------------------
% 1.43/1.24 % (9887)Instruction limit reached!
% 1.43/1.24 % (9887)------------------------------
% 1.43/1.24 % (9887)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.24 % (9887)Termination reason: Unknown
% 1.43/1.24 % (9887)Termination phase: Saturation
% 1.43/1.24
% 1.43/1.24 % (9887)Memory used [KB]: 5628
% 1.43/1.24 % (9887)Time elapsed: 0.010 s
% 1.43/1.24 % (9887)Instructions burned: 16 (million)
% 1.43/1.24 % (9887)------------------------------
% 1.43/1.24 % (9887)------------------------------
% 1.43/1.24 % (9889)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/1041Mi)
% 1.43/1.24 % (9890)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/7Mi)
% 1.43/1.24 % (9891)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/16Mi)
% 1.43/1.24 % (9886)Instruction limit reached!
% 1.43/1.24 % (9886)------------------------------
% 1.43/1.24 % (9886)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.24 % (9886)Termination reason: Unknown
% 1.43/1.24 % (9886)Termination phase: Saturation
% 1.43/1.24
% 1.43/1.24 % (9886)Memory used [KB]: 5756
% 1.43/1.24 % (9886)Time elapsed: 0.019 s
% 1.43/1.24 % (9886)Instructions burned: 37 (million)
% 1.43/1.24 % (9886)------------------------------
% 1.43/1.24 % (9886)------------------------------
% 1.43/1.24 % (9890)Instruction limit reached!
% 1.43/1.24 % (9890)------------------------------
% 1.43/1.24 % (9890)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.24 % (9890)Termination reason: Unknown
% 1.43/1.24 % (9890)Termination phase: Saturation
% 1.43/1.24
% 1.43/1.24 % (9890)Memory used [KB]: 1023
% 1.43/1.24 % (9890)Time elapsed: 0.005 s
% 1.43/1.24 % (9890)Instructions burned: 7 (million)
% 1.43/1.24 % (9890)------------------------------
% 1.43/1.24 % (9890)------------------------------
% 1.43/1.25 % (9891)Instruction limit reached!
% 1.43/1.25 % (9891)------------------------------
% 1.43/1.25 % (9891)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.25 % (9891)Termination reason: Unknown
% 1.43/1.25 % (9891)Termination phase: Saturation
% 1.43/1.25
% 1.43/1.25 % (9891)Memory used [KB]: 5628
% 1.43/1.25 % (9891)Time elapsed: 0.011 s
% 1.43/1.25 % (9891)Instructions burned: 17 (million)
% 1.43/1.25 % (9891)------------------------------
% 1.43/1.25 % (9891)------------------------------
% 1.43/1.25 % (9892)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/3Mi)
% 1.43/1.25 % (9893)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/3Mi)
% 1.43/1.25 % (9892)Instruction limit reached!
% 1.43/1.25 % (9892)------------------------------
% 1.43/1.25 % (9892)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.25 % (9892)Termination reason: Unknown
% 1.43/1.25 % (9892)Termination phase: Property scanning
% 1.43/1.25
% 1.43/1.25 % (9892)Memory used [KB]: 1023
% 1.43/1.25 % (9892)Time elapsed: 0.003 s
% 1.43/1.25 % (9892)Instructions burned: 3 (million)
% 1.43/1.25 % (9892)------------------------------
% 1.43/1.25 % (9892)------------------------------
% 1.43/1.26 % (9893)Instruction limit reached!
% 1.43/1.26 % (9893)------------------------------
% 1.43/1.26 % (9893)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.26 % (9893)Termination reason: Unknown
% 1.43/1.26 % (9893)Termination phase: Saturation
% 1.43/1.26
% 1.43/1.26 % (9893)Memory used [KB]: 1023
% 1.43/1.26 % (9893)Time elapsed: 0.003 s
% 1.43/1.26 % (9893)Instructions burned: 4 (million)
% 1.43/1.26 % (9893)------------------------------
% 1.43/1.26 % (9893)------------------------------
% 1.43/1.26 % (9894)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/7Mi)
% 1.43/1.26 % (9895)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/3Mi)
% 1.43/1.26 % (9895)Instruction limit reached!
% 1.43/1.26 % (9895)------------------------------
% 1.43/1.26 % (9895)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.26 % (9895)Termination reason: Unknown
% 1.43/1.26 % (9895)Termination phase: Saturation
% 1.43/1.26
% 1.43/1.26 % (9895)Memory used [KB]: 5500
% 1.43/1.26 % (9895)Time elapsed: 0.003 s
% 1.43/1.26 % (9895)Instructions burned: 3 (million)
% 1.43/1.26 % (9895)------------------------------
% 1.43/1.26 % (9895)------------------------------
% 1.43/1.26 % (9894)Instruction limit reached!
% 1.43/1.26 % (9894)------------------------------
% 1.43/1.26 % (9894)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.26 % (9894)Termination reason: Unknown
% 1.43/1.26 % (9894)Termination phase: Saturation
% 1.43/1.26
% 1.43/1.26 % (9894)Memory used [KB]: 5500
% 1.43/1.26 % (9894)Time elapsed: 0.005 s
% 1.43/1.26 % (9894)Instructions burned: 8 (million)
% 1.43/1.26 % (9894)------------------------------
% 1.43/1.26 % (9894)------------------------------
% 1.43/1.27 % (9896)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/4Mi)
% 1.43/1.27 % (9878)Instruction limit reached!
% 1.43/1.27 % (9878)------------------------------
% 1.43/1.27 % (9878)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.27 % (9878)Termination reason: Unknown
% 1.43/1.27 % (9878)Termination phase: Saturation
% 1.43/1.27
% 1.43/1.27 % (9878)Memory used [KB]: 6268
% 1.43/1.27 % (9878)Time elapsed: 0.065 s
% 1.43/1.27 % (9878)Instructions burned: 184 (million)
% 1.43/1.27 % (9878)------------------------------
% 1.43/1.27 % (9878)------------------------------
% 1.43/1.27 % (9897)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/18Mi)
% 1.43/1.27 % (9896)Instruction limit reached!
% 1.43/1.27 % (9896)------------------------------
% 1.43/1.27 % (9896)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.27 % (9896)Termination reason: Unknown
% 1.43/1.27 % (9896)Termination phase: Saturation
% 1.43/1.27
% 1.43/1.27 % (9896)Memory used [KB]: 5500
% 1.43/1.27 % (9896)Time elapsed: 0.004 s
% 1.43/1.27 % (9896)Instructions burned: 5 (million)
% 1.43/1.27 % (9896)------------------------------
% 1.43/1.27 % (9896)------------------------------
% 1.43/1.27 % (9898)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/710Mi)
% 1.43/1.27 % (9897)Refutation not found, incomplete strategy
% 1.43/1.27 % (9897)------------------------------
% 1.43/1.27 % (9897)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.27 % (9897)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.27
% 1.43/1.27
% 1.43/1.27 % (9897)Memory used [KB]: 5500
% 1.43/1.27 % (9897)Time elapsed: 0.005 s
% 1.43/1.27 % (9897)Instructions burned: 6 (million)
% 1.43/1.27 % (9897)------------------------------
% 1.43/1.27 % (9897)------------------------------
% 1.43/1.28 % (9899)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/6Mi)
% 1.43/1.28 % (9900)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/902Mi)
% 1.43/1.28 % (9901)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/21Mi)
% 1.43/1.28 % (9899)Instruction limit reached!
% 1.43/1.28 % (9899)------------------------------
% 1.43/1.28 % (9899)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.28 % (9899)Termination reason: Unknown
% 1.43/1.28 % (9899)Termination phase: Saturation
% 1.43/1.28
% 1.43/1.28 % (9899)Memory used [KB]: 5500
% 1.43/1.28 % (9899)Time elapsed: 0.005 s
% 1.43/1.28 % (9899)Instructions burned: 7 (million)
% 1.43/1.28 % (9899)------------------------------
% 1.43/1.28 % (9899)------------------------------
% 1.43/1.29 % (9902)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/5Mi)
% 1.43/1.29 % (9902)Instruction limit reached!
% 1.43/1.29 % (9902)------------------------------
% 1.43/1.29 % (9902)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.29 % (9902)Termination reason: Unknown
% 1.43/1.29 % (9902)Termination phase: Saturation
% 1.43/1.29
% 1.43/1.29 % (9902)Memory used [KB]: 5500
% 1.43/1.29 % (9902)Time elapsed: 0.004 s
% 1.43/1.29 % (9902)Instructions burned: 6 (million)
% 1.43/1.29 % (9902)------------------------------
% 1.43/1.29 % (9902)------------------------------
% 1.43/1.29 % (9903)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/6Mi)
% 1.43/1.29 % (9901)Instruction limit reached!
% 1.43/1.29 % (9901)------------------------------
% 1.43/1.29 % (9901)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.29 % (9901)Termination reason: Unknown
% 1.43/1.29 % (9901)Termination phase: Saturation
% 1.43/1.29
% 1.43/1.29 % (9901)Memory used [KB]: 5628
% 1.43/1.29 % (9901)Time elapsed: 0.014 s
% 1.43/1.29 % (9901)Instructions burned: 21 (million)
% 1.43/1.29 % (9901)------------------------------
% 1.43/1.29 % (9901)------------------------------
% 1.43/1.29 % (9903)Instruction limit reached!
% 1.43/1.29 % (9903)------------------------------
% 1.43/1.29 % (9903)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.29 % (9903)Termination reason: Unknown
% 1.43/1.29 % (9903)Termination phase: Saturation
% 1.43/1.29
% 1.43/1.29 % (9903)Memory used [KB]: 5500
% 1.43/1.29 % (9903)Time elapsed: 0.005 s
% 1.43/1.29 % (9903)Instructions burned: 8 (million)
% 1.43/1.29 % (9903)------------------------------
% 1.43/1.29 % (9903)------------------------------
% 1.43/1.30 % (9904)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/377Mi)
% 1.43/1.30 % (9904)Refutation not found, incomplete strategy
% 1.43/1.30 % (9904)------------------------------
% 1.43/1.30 % (9904)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.30 % (9904)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.30
% 1.43/1.30
% 1.43/1.30 % (9904)Memory used [KB]: 5500
% 1.43/1.30 % (9904)Time elapsed: 0.006 s
% 1.43/1.30 % (9904)Instructions burned: 8 (million)
% 1.43/1.30 % (9904)------------------------------
% 1.43/1.30 % (9904)------------------------------
% 1.43/1.30 % (9905)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/779Mi)
% 1.43/1.31 % (9906)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/19Mi)
% 1.43/1.31 % (9907)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/879Mi)
% 1.43/1.32 % (9906)Refutation not found, incomplete strategy
% 1.43/1.32 % (9906)------------------------------
% 1.43/1.32 % (9906)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.32 % (9906)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.32
% 1.43/1.32
% 1.43/1.32 % (9906)Memory used [KB]: 5500
% 1.43/1.32 % (9906)Time elapsed: 0.008 s
% 1.43/1.32 % (9906)Instructions burned: 13 (million)
% 1.43/1.32 % (9906)------------------------------
% 1.43/1.32 % (9906)------------------------------
% 1.43/1.32 % (9908)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_9779 for (2999ds/17Mi)
% 1.43/1.33 % (9909)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/3Mi)
% 1.43/1.33 % (9908)Instruction limit reached!
% 1.43/1.33 % (9908)------------------------------
% 1.43/1.33 % (9908)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.33 % (9908)Termination reason: Unknown
% 1.43/1.33 % (9908)Termination phase: Saturation
% 1.43/1.33
% 1.43/1.33 % (9908)Memory used [KB]: 5628
% 1.43/1.33 % (9908)Time elapsed: 0.012 s
% 1.43/1.33 % (9908)Instructions burned: 17 (million)
% 1.43/1.33 % (9908)------------------------------
% 1.43/1.33 % (9908)------------------------------
% 1.43/1.33 % (9909)Instruction limit reached!
% 1.43/1.33 % (9909)------------------------------
% 1.43/1.33 % (9909)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.33 % (9909)Termination reason: Unknown
% 1.43/1.33 % (9909)Termination phase: Saturation
% 1.43/1.33
% 1.43/1.33 % (9909)Memory used [KB]: 5500
% 1.43/1.33 % (9909)Time elapsed: 0.003 s
% 1.43/1.33 % (9909)Instructions burned: 4 (million)
% 1.43/1.33 % (9909)------------------------------
% 1.43/1.33 % (9909)------------------------------
% 1.43/1.34 % (9911)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/127Mi)
% 1.43/1.35 % (9910)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/30Mi)
% 1.43/1.36 % (9910)Instruction limit reached!
% 1.43/1.36 % (9910)------------------------------
% 1.43/1.36 % (9910)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.36 % (9910)Termination reason: Unknown
% 1.43/1.36 % (9910)Termination phase: Saturation
% 1.43/1.36
% 1.43/1.36 % (9910)Memory used [KB]: 5628
% 1.43/1.36 % (9910)Time elapsed: 0.017 s
% 1.43/1.36 % (9910)Instructions burned: 31 (million)
% 1.43/1.36 % (9910)------------------------------
% 1.43/1.36 % (9910)------------------------------
% 1.43/1.38 % (9919)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/100Mi)
% 1.43/1.38 % (9919)Refutation not found, incomplete strategy
% 1.43/1.38 % (9919)------------------------------
% 1.43/1.38 % (9919)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.38 % (9919)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.38
% 1.43/1.38
% 1.43/1.38 % (9919)Memory used [KB]: 5500
% 1.43/1.38 % (9919)Time elapsed: 0.027 s
% 1.43/1.39 % (9919)Instructions burned: 5 (million)
% 1.43/1.39 % (9919)------------------------------
% 1.43/1.39 % (9919)------------------------------
% 1.43/1.39 % (9911)Instruction limit reached!
% 1.43/1.39 % (9911)------------------------------
% 1.43/1.39 % (9911)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.39 % (9911)Termination reason: Unknown
% 1.43/1.39 % (9911)Termination phase: Saturation
% 1.43/1.39
% 1.43/1.39 % (9911)Memory used [KB]: 6140
% 1.43/1.39 % (9911)Time elapsed: 0.055 s
% 1.43/1.39 % (9911)Instructions burned: 128 (million)
% 1.43/1.39 % (9911)------------------------------
% 1.43/1.39 % (9911)------------------------------
% 1.43/1.40 % (9920)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/3Mi)
% 1.43/1.40 % (9920)Instruction limit reached!
% 1.43/1.40 % (9920)------------------------------
% 1.43/1.40 % (9920)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.40 % (9920)Termination reason: Unknown
% 1.43/1.40 % (9920)Termination phase: Saturation
% 1.43/1.40
% 1.43/1.40 % (9920)Memory used [KB]: 5500
% 1.43/1.40 % (9920)Time elapsed: 0.003 s
% 1.43/1.40 % (9920)Instructions burned: 4 (million)
% 1.43/1.40 % (9920)------------------------------
% 1.43/1.40 % (9920)------------------------------
% 1.43/1.40 % (9921)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/20Mi)
% 1.43/1.41 % (9923)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_9779 for (2998ds/86Mi)
% 1.43/1.41 % (9921)Instruction limit reached!
% 1.43/1.41 % (9921)------------------------------
% 1.43/1.41 % (9921)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.41 % (9921)Termination reason: Unknown
% 1.43/1.41 % (9921)Termination phase: Saturation
% 1.43/1.41
% 1.43/1.41 % (9921)Memory used [KB]: 5628
% 1.43/1.41 % (9921)Time elapsed: 0.032 s
% 1.43/1.41 % (9921)Instructions burned: 21 (million)
% 1.43/1.41 % (9921)------------------------------
% 1.43/1.41 % (9921)------------------------------
% 1.43/1.42 % (9928)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/107Mi)
% 1.43/1.44 % (9923)Instruction limit reached!
% 1.43/1.44 % (9923)------------------------------
% 1.43/1.44 % (9923)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.44 % (9923)Termination reason: Unknown
% 1.43/1.44 % (9923)Termination phase: Saturation
% 1.43/1.44
% 1.43/1.44 % (9923)Memory used [KB]: 6012
% 1.43/1.44 % (9923)Time elapsed: 0.051 s
% 1.43/1.44 % (9923)Instructions burned: 87 (million)
% 1.43/1.44 % (9923)------------------------------
% 1.43/1.44 % (9923)------------------------------
% 1.43/1.45 % (9942)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/39Mi)
% 1.43/1.45 % (9928)Instruction limit reached!
% 1.43/1.45 % (9928)------------------------------
% 1.43/1.45 % (9928)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.45 % (9928)Termination reason: Unknown
% 1.43/1.45 % (9928)Termination phase: Saturation
% 1.43/1.45
% 1.43/1.45 % (9928)Memory used [KB]: 5628
% 1.43/1.45 % (9928)Time elapsed: 0.031 s
% 1.43/1.45 % (9928)Instructions burned: 107 (million)
% 1.43/1.45 % (9928)------------------------------
% 1.43/1.45 % (9928)------------------------------
% 1.43/1.46 % (9942)Instruction limit reached!
% 1.43/1.46 % (9942)------------------------------
% 1.43/1.46 % (9942)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.46 % (9942)Termination reason: Unknown
% 1.43/1.46 % (9942)Termination phase: Saturation
% 1.43/1.46
% 1.43/1.46 % (9942)Memory used [KB]: 5628
% 1.43/1.46 % (9942)Time elapsed: 0.013 s
% 1.43/1.46 % (9942)Instructions burned: 39 (million)
% 1.43/1.46 % (9942)------------------------------
% 1.43/1.46 % (9942)------------------------------
% 1.43/1.46 % (9950)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/448Mi)
% 1.43/1.47 % (9954)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/46Mi)
% 1.43/1.48 % (9898)Refutation not found, non-redundant clauses discarded% (9898)------------------------------
% 1.43/1.48 % (9898)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.48 % (9898)Termination reason: Refutation not found, non-redundant clauses discarded
% 1.43/1.48
% 1.43/1.48 % (9898)Memory used [KB]: 7036
% 1.43/1.48 % (9898)Time elapsed: 0.211 s
% 1.43/1.48 % (9898)Instructions burned: 597 (million)
% 1.43/1.48 % (9898)------------------------------
% 1.43/1.48 % (9898)------------------------------
% 1.43/1.48 % (9954)Instruction limit reached!
% 1.43/1.48 % (9954)------------------------------
% 1.43/1.48 % (9954)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.48 % (9954)Termination reason: Unknown
% 1.43/1.48 % (9954)Termination phase: Saturation
% 1.43/1.48
% 1.43/1.48 % (9954)Memory used [KB]: 5756
% 1.43/1.48 % (9954)Time elapsed: 0.018 s
% 1.43/1.48 % (9954)Instructions burned: 48 (million)
% 1.43/1.48 % (9954)------------------------------
% 1.43/1.48 % (9954)------------------------------
% 1.43/1.49 % (9967)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/98Mi)
% 1.43/1.49 % (9968)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_9779 for (2997ds/507Mi)
% 1.43/1.50 % (9967)Refutation not found, incomplete strategy
% 1.43/1.50 % (9967)------------------------------
% 1.43/1.50 % (9967)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.50 % (9967)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.50
% 1.43/1.50
% 1.43/1.50 % (9967)Memory used [KB]: 1023
% 1.43/1.50 % (9967)Time elapsed: 0.006 s
% 1.43/1.50 % (9967)Instructions burned: 15 (million)
% 1.43/1.50 % (9967)------------------------------
% 1.43/1.50 % (9967)------------------------------
% 1.43/1.51 % (9975)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/149Mi)
% 1.43/1.53 % (9889)Instruction limit reached!
% 1.43/1.53 % (9889)------------------------------
% 1.43/1.53 % (9889)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.53 % (9889)Termination reason: Unknown
% 1.43/1.53 % (9889)Termination phase: Saturation
% 1.43/1.53
% 1.43/1.53 % (9889)Memory used [KB]: 6140
% 1.43/1.53 % (9889)Time elapsed: 0.295 s
% 1.43/1.53 % (9889)Instructions burned: 1043 (million)
% 1.43/1.53 % (9889)------------------------------
% 1.43/1.53 % (9889)------------------------------
% 1.43/1.54 % (9987)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/39Mi)
% 1.43/1.55 % (9907)Instruction limit reached!
% 1.43/1.55 % (9907)------------------------------
% 1.43/1.55 % (9907)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.55 % (9907)Termination reason: Unknown
% 1.43/1.55 % (9907)Termination phase: Saturation
% 1.43/1.55
% 1.43/1.55 % (9907)Memory used [KB]: 6140
% 1.43/1.55 % (9907)Time elapsed: 0.244 s
% 1.43/1.55 % (9907)Instructions burned: 881 (million)
% 1.43/1.55 % (9907)------------------------------
% 1.43/1.55 % (9907)------------------------------
% 1.43/1.55 % (9975)Instruction limit reached!
% 1.43/1.55 % (9975)------------------------------
% 1.43/1.55 % (9975)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.55 % (9975)Termination reason: Unknown
% 1.43/1.55 % (9975)Termination phase: Saturation
% 1.43/1.55
% 1.43/1.55 % (9975)Memory used [KB]: 5884
% 1.43/1.55 % (9975)Time elapsed: 0.047 s
% 1.43/1.55 % (9975)Instructions burned: 149 (million)
% 1.43/1.55 % (9975)------------------------------
% 1.43/1.55 % (9975)------------------------------
% 1.43/1.56 % (9987)Instruction limit reached!
% 1.43/1.56 % (9987)------------------------------
% 1.43/1.56 % (9987)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.56 % (9987)Termination reason: Unknown
% 1.43/1.56 % (9987)Termination phase: Saturation
% 1.43/1.56
% 1.43/1.56 % (9987)Memory used [KB]: 5628
% 1.43/1.56 % (9987)Time elapsed: 0.015 s
% 1.43/1.56 % (9987)Instructions burned: 40 (million)
% 1.43/1.56 % (9987)------------------------------
% 1.43/1.56 % (9987)------------------------------
% 1.43/1.56 % (9905)Instruction limit reached!
% 1.43/1.56 % (9905)------------------------------
% 1.43/1.56 % (9905)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.56 % (9905)Termination reason: Unknown
% 1.43/1.56 % (9905)Termination phase: Saturation
% 1.43/1.56
% 1.43/1.56 % (9905)Memory used [KB]: 6268
% 1.43/1.56 % (9905)Time elapsed: 0.256 s
% 1.43/1.56 % (9905)Instructions burned: 779 (million)
% 1.43/1.56 % (9905)------------------------------
% 1.43/1.56 % (9905)------------------------------
% 1.43/1.56 % (9997)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/6Mi)
% 1.43/1.56 % (9998)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/1087Mi)
% 1.43/1.56 % (9997)Instruction limit reached!
% 1.43/1.56 % (9997)------------------------------
% 1.43/1.56 % (9997)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.56 % (9997)Termination reason: Unknown
% 1.43/1.56 % (9997)Termination phase: Saturation
% 1.43/1.56
% 1.43/1.56 % (9997)Memory used [KB]: 9978
% 1.43/1.56 % (9997)Time elapsed: 0.004 s
% 1.43/1.56 % (9997)Instructions burned: 7 (million)
% 1.43/1.56 % (9997)------------------------------
% 1.43/1.56 % (9997)------------------------------
% 1.43/1.57 % (9999)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/47Mi)
% 1.43/1.57 % (10000)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/44Mi)
% 1.43/1.57 % (9998)Refutation not found, incomplete strategy
% 1.43/1.57 % (9998)------------------------------
% 1.43/1.57 % (9998)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.57 % (9998)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.57
% 1.43/1.57
% 1.43/1.57 % (9998)Memory used [KB]: 5628
% 1.43/1.57 % (9998)Time elapsed: 0.011 s
% 1.43/1.57 % (9998)Instructions burned: 28 (million)
% 1.43/1.57 % (9998)------------------------------
% 1.43/1.57 % (9998)------------------------------
% 1.43/1.57 % (10001)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/432Mi)
% 1.43/1.58 % (9999)Instruction limit reached!
% 1.43/1.58 % (9999)------------------------------
% 1.43/1.58 % (9999)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.58 % (9999)Termination reason: Unknown
% 1.43/1.58 % (9999)Termination phase: Saturation
% 1.43/1.58
% 1.43/1.58 % (9999)Memory used [KB]: 5756
% 1.43/1.58 % (9999)Time elapsed: 0.017 s
% 1.43/1.58 % (9999)Instructions burned: 47 (million)
% 1.43/1.58 % (9999)------------------------------
% 1.43/1.58 % (9999)------------------------------
% 1.43/1.58 % (10010)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/62Mi)
% 1.43/1.58 % (10000)Instruction limit reached!
% 1.43/1.58 % (10000)------------------------------
% 1.43/1.58 % (10000)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.58 % (10000)Termination reason: Unknown
% 1.43/1.58 % (10000)Termination phase: Saturation
% 1.43/1.58
% 1.43/1.58 % (10000)Memory used [KB]: 1151
% 1.43/1.58 % (10000)Time elapsed: 0.015 s
% 1.43/1.58 % (10000)Instructions burned: 44 (million)
% 1.43/1.58 % (10000)------------------------------
% 1.43/1.58 % (10000)------------------------------
% 1.43/1.59 % (9900)Instruction limit reached!
% 1.43/1.59 % (9900)------------------------------
% 1.43/1.59 % (9900)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.59 % (9900)Termination reason: Unknown
% 1.43/1.59 % (9900)Termination phase: Saturation
% 1.43/1.59
% 1.43/1.59 % (9900)Memory used [KB]: 6908
% 1.43/1.59 % (9900)Time elapsed: 0.312 s
% 1.43/1.59 % (9900)Instructions burned: 903 (million)
% 1.43/1.59 % (9900)------------------------------
% 1.43/1.59 % (9900)------------------------------
% 1.43/1.59 % (10016)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/31Mi)
% 1.43/1.59 % (10018)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/96Mi)
% 1.43/1.60 % (10024)lrs+1002_1:4_au=on:cbe=off:cnfonf=lazy_pi_sigma_gen:hud=15:inj=on:nwc=4.0:s2a=on:sac=on:sp=reverse_arity:i=453:si=on:rtra=on_0 on DTF2THF_9779 for (2996ds/453Mi)
% 1.43/1.60 % (9950)Instruction limit reached!
% 1.43/1.60 % (9950)------------------------------
% 1.43/1.60 % (9950)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.60 % (9950)Termination reason: Unknown
% 1.43/1.60 % (9950)Termination phase: Saturation
% 1.43/1.60
% 1.43/1.60 % (9950)Memory used [KB]: 6268
% 1.43/1.60 % (9950)Time elapsed: 0.141 s
% 1.43/1.60 % (9950)Instructions burned: 448 (million)
% 1.43/1.60 % (9950)------------------------------
% 1.43/1.60 % (9950)------------------------------
% 1.43/1.60 % (10010)Instruction limit reached!
% 1.43/1.60 % (10010)------------------------------
% 1.43/1.60 % (10010)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.60 % (10010)Termination reason: Unknown
% 1.43/1.60 % (10010)Termination phase: Saturation
% 1.43/1.60
% 1.43/1.60 % (10010)Memory used [KB]: 5756
% 1.43/1.60 % (10010)Time elapsed: 0.020 s
% 1.43/1.60 % (10010)Instructions burned: 62 (million)
% 1.43/1.60 % (10010)------------------------------
% 1.43/1.60 % (10010)------------------------------
% 1.43/1.60 % (10016)Instruction limit reached!
% 1.43/1.60 % (10016)------------------------------
% 1.43/1.60 % (10016)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.60 % (10016)Termination reason: Unknown
% 1.43/1.60 % (10016)Termination phase: Saturation
% 1.43/1.60
% 1.43/1.60 % (10016)Memory used [KB]: 5628
% 1.43/1.60 % (10016)Time elapsed: 0.011 s
% 1.43/1.60 % (10016)Instructions burned: 32 (million)
% 1.43/1.60 % (10016)------------------------------
% 1.43/1.60 % (10016)------------------------------
% 1.43/1.61 % (10024)Refutation not found, incomplete strategy
% 1.43/1.61 % (10024)------------------------------
% 1.43/1.61 % (10024)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.61 % (10024)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.61
% 1.43/1.61
% 1.43/1.61 % (10024)Memory used [KB]: 5500
% 1.43/1.61 % (10024)Time elapsed: 0.006 s
% 1.43/1.61 % (10024)Instructions burned: 15 (million)
% 1.43/1.61 % (10024)------------------------------
% 1.43/1.61 % (10024)------------------------------
% 1.43/1.61 % (10027)lrs-1004_1:1_au=on:bsd=on:cbe=off:cnfonf=off:fe=axiom:fsd=on:i=71:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/71Mi)
% 1.43/1.61 % (10028)dis+1002_1:1_bd=off:fsr=off:ntd=on:s2a=on:ss=axioms:i=83:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/83Mi)
% 1.43/1.61 % (10029)lrs+10_1:128_cnfonf=lazy_not_gen_be_off:hud=1:ins=1:i=11:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/11Mi)
% 1.43/1.61 % (10029)Instruction limit reached!
% 1.43/1.61 % (10029)------------------------------
% 1.43/1.61 % (10029)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.61 % (10029)Termination reason: Unknown
% 1.43/1.61 % (10029)Termination phase: Saturation
% 1.43/1.61
% 1.43/1.61 % (10029)Memory used [KB]: 5500
% 1.43/1.61 % (10029)Time elapsed: 0.005 s
% 1.43/1.61 % (10029)Instructions burned: 12 (million)
% 1.43/1.61 % (10029)------------------------------
% 1.43/1.61 % (10029)------------------------------
% 1.43/1.61 % (10035)lrs+1010_1:1_au=on:cbe=off:cnfonf=lazy_not_gen_be_off:fsr=off:spb=non_intro:i=41:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/41Mi)
% 1.43/1.62 % (10035)Refutation not found, incomplete strategy
% 1.43/1.62 % (10035)------------------------------
% 1.43/1.62 % (10035)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.62 % (10035)Termination reason: Refutation not found, incomplete strategy
% 1.43/1.62
% 1.43/1.62
% 1.43/1.62 % (10035)Memory used [KB]: 5500
% 1.43/1.62 % (10035)Time elapsed: 0.005 s
% 1.43/1.62 % (10035)Instructions burned: 11 (million)
% 1.43/1.62 % (10035)------------------------------
% 1.43/1.62 % (10035)------------------------------
% 1.43/1.62 % (10018)Instruction limit reached!
% 1.43/1.62 % (10018)------------------------------
% 1.43/1.62 % (10018)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.62 % (10018)Termination reason: Unknown
% 1.43/1.62 % (10018)Termination phase: Saturation
% 1.43/1.62
% 1.43/1.62 % (10018)Memory used [KB]: 5756
% 1.43/1.62 % (10018)Time elapsed: 0.032 s
% 1.43/1.62 % (10018)Instructions burned: 97 (million)
% 1.43/1.62 % (10018)------------------------------
% 1.43/1.62 % (10018)------------------------------
% 1.43/1.62 % (10044)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/6Mi)
% 1.43/1.63 % (10044)Instruction limit reached!
% 1.43/1.63 % (10044)------------------------------
% 1.43/1.63 % (10044)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.63 % (10044)Termination reason: Unknown
% 1.43/1.63 % (10044)Termination phase: Saturation
% 1.43/1.63
% 1.43/1.63 % (10044)Memory used [KB]: 5500
% 1.43/1.63 % (10044)Time elapsed: 0.004 s
% 1.43/1.63 % (10044)Instructions burned: 7 (million)
% 1.43/1.63 % (10044)------------------------------
% 1.43/1.63 % (10044)------------------------------
% 1.43/1.63 % (10048)dis+10_1:1_avsq=on:cnfonf=off:e2e=on:nm=32:i=150:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/150Mi)
% 1.43/1.63 % (10050)ott+1010_1:1_au=on:s2a=on:sd=7:ss=axioms:st=1.5:i=343:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/343Mi)
% 1.43/1.63 % (10027)Instruction limit reached!
% 1.43/1.63 % (10027)------------------------------
% 1.43/1.63 % (10027)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.63 % (10027)Termination reason: Unknown
% 1.43/1.63 % (10027)Termination phase: Saturation
% 1.43/1.63
% 1.43/1.63 % (10027)Memory used [KB]: 5756
% 1.43/1.63 % (10027)Time elapsed: 0.025 s
% 1.43/1.63 % (10027)Instructions burned: 72 (million)
% 1.43/1.63 % (10027)------------------------------
% 1.43/1.63 % (10027)------------------------------
% 1.43/1.64 % (10053)ott+1010_1:4_cbe=off:chr=on:hfsq=on:hfsqr=1,16:hud=3:sac=on:sp=unary_frequency:ss=axioms:st=5.0:tnu=2:i=109:si=on:rtra=on_0 on DTF2THF_9779 for (2995ds/109Mi)
% 1.43/1.64 % (10028)Instruction limit reached!
% 1.43/1.64 % (10028)------------------------------
% 1.43/1.64 % (10028)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.64 % (10028)Termination reason: Unknown
% 1.43/1.64 % (10028)Termination phase: Saturation
% 1.43/1.64
% 1.43/1.64 % (10028)Memory used [KB]: 5884
% 1.43/1.64 % (10028)Time elapsed: 0.029 s
% 1.43/1.64 % (10028)Instructions burned: 84 (million)
% 1.43/1.64 % (10028)------------------------------
% 1.43/1.64 % (10028)------------------------------
% 1.43/1.64 % (10001)First to succeed.
% 1.43/1.64 % (10001)Refutation found. Thanks to Tanya!
% 1.43/1.64 % SZS status Theorem for DTF2THF_9779
% 1.43/1.64 % SZS output start Proof for DTF2THF_9779
% 1.43/1.64 thf(type_def_5, type, a: $tType).
% 1.43/1.64 thf(func_def_0, type, a: $tType).
% 1.43/1.64 thf(func_def_14, type, ph0: !>[X0: $tType]:(X0)).
% 1.43/1.64 thf(func_def_15, type, sK1: a > a).
% 1.43/1.64 thf(func_def_16, type, sK2: a > a).
% 1.43/1.64 thf(func_def_17, type, sK3: a > a).
% 1.43/1.64 thf(func_def_18, type, sK4: (a > a) > $o).
% 1.43/1.64 thf(func_def_21, type, sK5: a > a).
% 1.43/1.64 thf(f334,plain,(
% 1.43/1.64 $false),
% 1.43/1.64 inference(trivial_inequality_removal,[status(thm)],[f317])).
% 1.43/1.64 thf(f317,plain,(
% 1.43/1.64 ($false = $true)),
% 1.43/1.64 inference(superposition,[status(thm)],[f294,f98])).
% 1.43/1.64 thf(f98,plain,(
% 1.43/1.64 ( ! [X1 : a > a] : (($true = ((sK4 @ X1) => (sK4 @ (^[Y0 : a]: (sK1 @ (X1 @ Y0))))))) )),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f88])).
% 1.43/1.64 thf(f88,plain,(
% 1.43/1.64 ( ! [X1 : a > a] : ((((^[Y0 : a > a]: ((sK4 @ Y0) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1)))))) @ X1) = $true)) )),
% 1.43/1.64 inference(pi_clausification,[status(thm)],[f30])).
% 1.43/1.64 thf(f30,plain,(
% 1.43/1.64 ((!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ Y0) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1))))))) = $true)),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f23])).
% 1.43/1.64 thf(f23,plain,(
% 1.43/1.64 (((sK4 @ sK1) & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ Y0) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1)))))))) = $true)),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f20])).
% 1.43/1.64 thf(f20,plain,(
% 1.43/1.64 ($false = (((sK4 @ sK1) & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ Y0) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1)))))))) => (sK4 @ (^[Y0 : a]: (sK3 @ (sK2 @ Y0))))))),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f18])).
% 1.43/1.64 thf(f18,plain,(
% 1.43/1.64 ($false = ((^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ (^[Y1 : a]: (sK3 @ (sK2 @ Y1)))))) @ sK4))),
% 1.43/1.64 inference(sigma_clausification,[status(thm)],[f16])).
% 1.43/1.64 thf(f16,plain,(
% 1.43/1.64 ($false = (!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ (^[Y1 : a]: (sK3 @ (sK2 @ Y1))))))))),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f15])).
% 1.43/1.64 thf(f15,plain,(
% 1.43/1.64 ($false = (((!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2))))))) & (Y0 @ sK1)) => (Y0 @ sK2)))) & (!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ sK3))))) => (!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ (^[Y1 : a]: (sK3 @ (sK2 @ Y1)))))))))),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f14])).
% 1.43/1.64 thf(f14,plain,(
% 1.43/1.64 (((^[Y0 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3))))))) & (Y1 @ sK1)) => (Y1 @ sK2)))) & (!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((Y1 @ sK1) & (!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3)))))))) => (Y1 @ Y0))))) => (!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((Y1 @ sK1) & (!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3)))))))) => (Y1 @ (^[Y2 : a]: (Y0 @ (sK2 @ Y2))))))))) @ sK3) = $false)),
% 1.43/1.64 inference(sigma_clausification,[status(thm)],[f13])).
% 1.43/1.64 thf(f13,plain,(
% 1.43/1.64 ((!! @ (a > a) @ (^[Y0 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3))))))) & (Y1 @ sK1)) => (Y1 @ sK2)))) & (!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((Y1 @ sK1) & (!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3)))))))) => (Y1 @ Y0))))) => (!! @ ((a > a) > $o) @ (^[Y1 : (a > a) > $o]: (((Y1 @ sK1) & (!! @ (a > a) @ (^[Y2 : a > a]: ((Y1 @ Y2) => (Y1 @ (^[Y3 : a]: (sK1 @ (Y2 @ Y3)))))))) => (Y1 @ (^[Y2 : a]: (Y0 @ (sK2 @ Y2)))))))))) = $false)),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f12])).
% 1.43/1.64 thf(f12,plain,(
% 1.43/1.64 (((^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4))))))) & (Y2 @ sK1)) => (Y2 @ Y0)))) & (!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((Y2 @ sK1) & (!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4)))))))) => (Y2 @ Y1))))) => (!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((Y2 @ sK1) & (!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4)))))))) => (Y2 @ (^[Y3 : a]: (Y1 @ (Y0 @ Y3))))))))))) @ sK2) = $false)),
% 1.43/1.64 inference(sigma_clausification,[status(thm)],[f10])).
% 1.43/1.64 thf(f10,plain,(
% 1.43/1.64 ((!! @ (a > a) @ (^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4))))))) & (Y2 @ sK1)) => (Y2 @ Y0)))) & (!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((Y2 @ sK1) & (!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4)))))))) => (Y2 @ Y1))))) => (!! @ ((a > a) > $o) @ (^[Y2 : (a > a) > $o]: (((Y2 @ sK1) & (!! @ (a > a) @ (^[Y3 : a > a]: ((Y2 @ Y3) => (Y2 @ (^[Y4 : a]: (sK1 @ (Y3 @ Y4)))))))) => (Y2 @ (^[Y3 : a]: (Y1 @ (Y0 @ Y3)))))))))))) = $false)),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f8])).
% 1.43/1.64 thf(f8,plain,(
% 1.43/1.64 ($false = ((^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (!! @ (a > a) @ (^[Y2 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5))))))) & (Y3 @ Y0)) => (Y3 @ Y1)))) & (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ Y2))))) => (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ (^[Y4 : a]: (Y2 @ (Y1 @ Y4))))))))))))) @ sK1))),
% 1.43/1.64 inference(sigma_clausification,[status(thm)],[f7])).
% 1.43/1.64 thf(f7,plain,(
% 1.43/1.64 ((!! @ (a > a) @ (^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (!! @ (a > a) @ (^[Y2 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5))))))) & (Y3 @ Y0)) => (Y3 @ Y1)))) & (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ Y2))))) => (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ (^[Y4 : a]: (Y2 @ (Y1 @ Y4)))))))))))))) = $false)),
% 1.43/1.64 inference(not_proxy_clausification,[status(thm)],[f6])).
% 1.43/1.64 thf(f6,plain,(
% 1.43/1.64 ($true = (~ (!! @ (a > a) @ (^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (!! @ (a > a) @ (^[Y2 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5))))))) & (Y3 @ Y0)) => (Y3 @ Y1)))) & (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ Y2))))) => (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ (^[Y4 : a]: (Y2 @ (Y1 @ Y4))))))))))))))))),
% 1.43/1.64 inference(cnf_transformation,[status(thm)],[f5])).
% 1.43/1.64 thf(f5,plain,(
% 1.43/1.64 ($true = (~ (!! @ (a > a) @ (^[Y0 : a > a]: (!! @ (a > a) @ (^[Y1 : a > a]: (!! @ (a > a) @ (^[Y2 : a > a]: (((!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5))))))) & (Y3 @ Y0)) => (Y3 @ Y1)))) & (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ Y2))))) => (!! @ ((a > a) > $o) @ (^[Y3 : (a > a) > $o]: (((Y3 @ Y0) & (!! @ (a > a) @ (^[Y4 : a > a]: ((Y3 @ Y4) => (Y3 @ (^[Y5 : a]: (Y0 @ (Y4 @ Y5)))))))) => (Y3 @ (^[Y4 : a]: (Y2 @ (Y1 @ Y4))))))))))))))))),
% 1.43/1.64 inference(fool_elimination,[status(thm)],[f4])).
% 1.43/1.64 thf(f4,plain,(
% 1.43/1.64 ~! [X0 : a > a,X1 : a > a,X2 : a > a] : ((! [X3 : (a > a) > $o] : ((! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X2 @ (X4 @ X5))))) & (X3 @ X2)) => (X3 @ X0)) & ! [X6 : (a > a) > $o] : (((X6 @ X2) & ! [X7 : a > a] : ((X6 @ X7) => (X6 @ (^[X8 : a] : (X2 @ (X7 @ X8)))))) => (X6 @ X1))) => ! [X9 : (a > a) > $o] : ((! [X10 : a > a] : ((X9 @ X10) => (X9 @ (^[X11 : a] : (X2 @ (X10 @ X11))))) & (X9 @ X2)) => (X9 @ (^[X12 : a] : (X0 @ (X1 @ X12))))))),
% 1.43/1.64 inference(rectify,[status(thm)],[f2])).
% 1.43/1.64 thf(f2,negated_conjecture,(
% 1.43/1.64 ~! [X1 : a > a,X2 : a > a,X0 : a > a] : ((! [X3 : (a > a) > $o] : ((! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5))))) & (X3 @ X0)) => (X3 @ X1)) & ! [X3 : (a > a) > $o] : (((X3 @ X0) & ! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5)))))) => (X3 @ X2))) => ! [X3 : (a > a) > $o] : ((! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5))))) & (X3 @ X0)) => (X3 @ (^[X5 : a] : (X1 @ (X2 @ X5))))))),
% 1.43/1.64 inference(negated_conjecture,[status(cth)],[f1])).
% 1.43/1.64 thf(f1,conjecture,(
% 1.43/1.64 ! [X1 : a > a,X2 : a > a,X0 : a > a] : ((! [X3 : (a > a) > $o] : ((! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5))))) & (X3 @ X0)) => (X3 @ X1)) & ! [X3 : (a > a) > $o] : (((X3 @ X0) & ! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5)))))) => (X3 @ X2))) => ! [X3 : (a > a) > $o] : ((! [X4 : a > a] : ((X3 @ X4) => (X3 @ (^[X5 : a] : (X0 @ (X4 @ X5))))) & (X3 @ X0)) => (X3 @ (^[X5 : a] : (X1 @ (X2 @ X5))))))),
% 1.43/1.64 file('/export/starexec/sandbox2/tmp/tmp.HXTQGiCcwm/DTF2THF_9779.p',cTHM135D_pme)).
% 1.43/1.64 thf(f294,plain,(
% 1.43/1.64 ($false = ((sK4 @ (^[Y0 : a]: (sK5 @ (sK2 @ Y0)))) => (sK4 @ (^[Y0 : a]: (sK1 @ (sK5 @ (sK2 @ Y0)))))))),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f285])).
% 1.43/1.64 thf(f285,plain,(
% 1.43/1.64 (((^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1))))))) @ sK5) = $false)),
% 1.43/1.64 inference(sigma_clausification,[status(thm)],[f267])).
% 1.43/1.64 thf(f267,plain,(
% 1.43/1.64 ($false = (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1)))))))))),
% 1.43/1.64 inference(boolean_simplification,[status(thm)],[f266])).
% 1.43/1.64 thf(f266,plain,(
% 1.43/1.64 ($false = ($true & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1))))))))))),
% 1.43/1.64 inference(forward_demodulation,[status(thm)],[f243,f203])).
% 1.43/1.64 thf(f203,plain,(
% 1.43/1.64 ((sK4 @ (^[Y0 : a]: (sK1 @ (sK2 @ Y0)))) = $true)),
% 1.43/1.64 inference(boolean_simplification,[status(thm)],[f185])).
% 1.43/1.64 thf(f185,plain,(
% 1.43/1.64 (($true => (sK4 @ (^[Y0 : a]: (sK1 @ (sK2 @ Y0))))) = $true)),
% 1.43/1.64 inference(superposition,[status(thm)],[f98,f156])).
% 1.43/1.64 thf(f156,plain,(
% 1.43/1.64 ((sK4 @ sK2) = $true)),
% 1.43/1.64 inference(boolean_simplification,[status(thm)],[f155])).
% 1.43/1.64 thf(f155,plain,(
% 1.43/1.64 (($true => (sK4 @ sK2)) = $true)),
% 1.43/1.64 inference(forward_demodulation,[status(thm)],[f148,f31])).
% 1.43/1.64 thf(f31,plain,(
% 1.43/1.64 ((sK4 @ sK1) = $true)),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f23])).
% 1.43/1.64 thf(f148,plain,(
% 1.43/1.64 (((sK4 @ sK1) => (sK4 @ sK2)) = $true)),
% 1.43/1.64 inference(boolean_simplification,[status(thm)],[f147])).
% 1.43/1.64 thf(f147,plain,(
% 1.43/1.64 ((($true & (sK4 @ sK1)) => (sK4 @ sK2)) = $true)),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f120])).
% 1.43/1.64 thf(f120,plain,(
% 1.43/1.64 ((($true & ((^[Y0 : a > a]: (sK4 @ ((^[Y1 : a > a]: (Y1)) @ Y0))) @ sK1)) => ((^[Y0 : a > a]: (sK4 @ ((^[Y1 : a > a]: (Y1)) @ Y0))) @ sK2)) = $true)),
% 1.43/1.64 inference(superposition,[status(thm)],[f83,f30])).
% 1.43/1.64 thf(f83,plain,(
% 1.43/1.64 ( ! [X1 : (a > a) > $o] : (((((!! @ (a > a) @ (^[Y0 : a > a]: ((X1 @ Y0) => (X1 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1))))))) & (X1 @ sK1)) => (X1 @ sK2)) = $true)) )),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f80])).
% 1.43/1.64 thf(f80,plain,(
% 1.43/1.64 ( ! [X1 : (a > a) > $o] : (($true = ((^[Y0 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2))))))) & (Y0 @ sK1)) => (Y0 @ sK2))) @ X1))) )),
% 1.43/1.64 inference(pi_clausification,[status(thm)],[f27])).
% 1.43/1.64 thf(f27,plain,(
% 1.43/1.64 ($true = (!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2))))))) & (Y0 @ sK1)) => (Y0 @ sK2)))))),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f17])).
% 1.43/1.64 thf(f17,plain,(
% 1.43/1.64 (((!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2))))))) & (Y0 @ sK1)) => (Y0 @ sK2)))) & (!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ sK3))))) = $true)),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f15])).
% 1.43/1.64 thf(f243,plain,(
% 1.43/1.64 ($false = ((sK4 @ (^[Y0 : a]: (sK1 @ (sK2 @ Y0)))) & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1))))))))))),
% 1.43/1.64 inference(not_proxy_clausification,[status(thm)],[f68])).
% 1.43/1.64 thf(f68,plain,(
% 1.43/1.64 ($true = (~ ((sK4 @ (^[Y0 : a]: (sK1 @ (sK2 @ Y0)))) & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1)))))))))))),
% 1.43/1.64 inference(boolean_simplification,[status(thm)],[f67])).
% 1.43/1.64 thf(f67,plain,(
% 1.43/1.64 ((((sK4 @ (^[Y0 : a]: (sK1 @ (sK2 @ Y0)))) & (!! @ (a > a) @ (^[Y0 : a > a]: ((sK4 @ (^[Y1 : a]: (Y0 @ (sK2 @ Y1)))) => (sK4 @ (^[Y1 : a]: (sK1 @ (Y0 @ (sK2 @ Y1))))))))) => $false) = $true)),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f50])).
% 1.43/1.64 thf(f50,plain,(
% 1.43/1.64 (((((^[Y0 : a > a]: (sK4 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (sK2 @ ((^[Y5 : a > a]: ((^[Y6 : a]: (Y6)))) @ Y3 @ Y4))))) @ Y1 @ Y2))))) @ Y0))) @ sK1) & (!! @ (a > a) @ (^[Y0 : a > a]: (((^[Y1 : a > a]: (sK4 @ ((^[Y2 : a > a]: ((^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (sK2 @ ((^[Y6 : a > a]: ((^[Y7 : a]: (Y7)))) @ Y4 @ Y5))))) @ Y2 @ Y3))))) @ Y1))) @ Y0) => ((^[Y1 : a > a]: (sK4 @ ((^[Y2 : a > a]: ((^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (sK2 @ ((^[Y6 : a > a]: ((^[Y7 : a]: (Y7)))) @ Y4 @ Y5))))) @ Y2 @ Y3))))) @ Y1))) @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1)))))))) => $false) = $true)),
% 1.43/1.64 inference(superposition,[status(thm)],[f39,f22])).
% 1.43/1.64 thf(f22,plain,(
% 1.43/1.64 ($false = (sK4 @ (^[Y0 : a]: (sK3 @ (sK2 @ Y0)))))),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f20])).
% 1.43/1.64 thf(f39,plain,(
% 1.43/1.64 ( ! [X1 : (a > a) > $o] : (((((X1 @ sK1) & (!! @ (a > a) @ (^[Y0 : a > a]: ((X1 @ Y0) => (X1 @ (^[Y1 : a]: (sK1 @ (Y0 @ Y1)))))))) => (X1 @ sK3)) = $true)) )),
% 1.43/1.64 inference(beta_eta_normalization,[status(thm)],[f34])).
% 1.43/1.64 thf(f34,plain,(
% 1.43/1.64 ( ! [X1 : (a > a) > $o] : ((((^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ sK3))) @ X1) = $true)) )),
% 1.43/1.64 inference(pi_clausification,[status(thm)],[f26])).
% 1.43/1.64 thf(f26,plain,(
% 1.43/1.64 ((!! @ ((a > a) > $o) @ (^[Y0 : (a > a) > $o]: (((Y0 @ sK1) & (!! @ (a > a) @ (^[Y1 : a > a]: ((Y0 @ Y1) => (Y0 @ (^[Y2 : a]: (sK1 @ (Y1 @ Y2)))))))) => (Y0 @ sK3)))) = $true)),
% 1.43/1.64 inference(binary_proxy_clausification,[status(thm)],[f17])).
% 1.43/1.64 % SZS output end Proof for DTF2THF_9779
% 1.43/1.64 % (10001)------------------------------
% 1.43/1.64 % (10001)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.43/1.64 % (10001)Termination reason: Refutation
% 1.43/1.64
% 1.43/1.64 % (10001)Memory used [KB]: 2430
% 1.43/1.64 % (10001)Time elapsed: 0.067 s
% 1.43/1.64 % (10001)Instructions burned: 222 (million)
% 1.43/1.64 % (10001)------------------------------
% 1.43/1.64 % (10001)------------------------------
% 1.43/1.64 % (9877)Success in time 0.437 s
%------------------------------------------------------------------------------