%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : NUM827^5 : TPTP v9.2.1. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n024.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:24:52 AM UTC 2026
% Result : Theorem 1.22s 1.38s
% Output : Refutation 1.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 4
% Syntax : Number of formulae : 57 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 325 ( 171 equ; 0 cnn)
% Maximal formula atoms : 4 ( 5 avg)
% Number of connectives : 768 ( 8 ~; 0 |; 38 &; 592 @)
% ( 0 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Number of types : 1 ( 1 usr)
% Number of type conns : 48 ( 48 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 9 usr; 9 con; 0-2 aty)
% ( 80 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 125 ( 92 ^; 33 !; 0 ?; 125 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
n: $tType ).
thf(func_def_0,type,
n: $tType ).
thf(func_def_1,type,
c0: n ).
thf(func_def_2,type,
cS: n > n ).
thf(func_def_3,type,
c_plus: n > n > n ).
thf(func_def_20,type,
ph1:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
sK2: n ).
thf(func_def_22,type,
sK3: n ).
thf(f120,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f119]) ).
thf(f119,plain,
$true = $false,
inference(boolean_simplification,[status(thm)],[f116]) ).
thf(f116,plain,
( ( ( cS @ sK3 )
= ( cS @ sK3 ) )
= $false ),
inference(backward_demodulation,[status(thm)],[f107,f108]) ).
thf(f108,plain,
( sK3
= ( c_plus @ c0 @ sK3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f105]) ).
thf(f105,plain,
( $true
= ( ( c_plus @ c0 @ sK3 )
= sK3 ) ),
inference(binary_proxy_clausification,[status(thm)],[f103]) ).
thf(f103,plain,
( ( ( ( c_plus @ c0 @ sK3 )
= sK3 )
=> ( ( cS @ ( c_plus @ c0 @ sK3 ) )
= ( cS @ sK3 ) ) )
= $false ),
inference(forward_demodulation,[status(thm)],[f102,f35]) ).
thf(f35,plain,
! [X1: n] :
( ( c_plus @ X1 @ c0 )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f34]) ).
thf(f34,plain,
! [X1: n] :
( $true
= ( ( c_plus @ X1 @ c0 )
= X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f33]) ).
thf(f33,plain,
! [X1: n] :
( $true
= ( ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f29]) ).
thf(f29,plain,
( $true
= ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f23]) ).
thf(f23,plain,
( $true
= ( ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f19]) ).
thf(f19,plain,
( ( ( ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) )
=> ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f18]) ).
thf(f18,plain,
( ( ~ ( ( ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) )
=> ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f17,f16,f15,f14]) ).
thf(f14,plain,
( cPA_1
= ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
( cPA_1
= ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= Y0 ) ) ),
inference(fool_elimination,[status(thm)],[f1]) ).
thf(f1,axiom,
! [X0: n] :
( ( ( c_plus @ X0 @ c0 )
= X0 )
= cPA_1 ),
file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_1_def) ).
thf(f15,plain,
( cPA_2
= ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
thf(f8,plain,
( cPA_2
= ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f7]) ).
thf(f7,plain,
! [X0: n,X1: n] :
( ( ( c_plus @ X1 @ ( cS @ X0 ) )
= ( cS @ ( c_plus @ X1 @ X0 ) ) )
= cPA_2 ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,axiom,
! [X1: n,X0: n] :
( ( ( c_plus @ X0 @ ( cS @ X1 ) )
= ( cS @ ( c_plus @ X0 @ X1 ) ) )
= cPA_2 ),
file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_2_def) ).
thf(f16,plain,
( cPA_IND_EQ
= ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f13,plain,
( cPA_IND_EQ
= ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f12]) ).
thf(f12,plain,
! [X0: n > n,X1: n > n] :
( ( ( ( ( X0 @ c0 )
= ( X1 @ c0 ) )
& ! [X2: n] :
( ( ( X0 @ X2 )
= ( X1 @ X2 ) )
=> ( ( X0 @ ( cS @ X2 ) )
= ( X1 @ ( cS @ X2 ) ) ) ) )
=> ! [X3: n] :
( ( X1 @ X3 )
= ( X0 @ X3 ) ) )
= cPA_IND_EQ ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
! [X3: n > n,X2: n > n] :
( ( ( ( ( X2 @ c0 )
= ( X3 @ c0 ) )
& ! [X0: n] :
( ( ( X2 @ X0 )
= ( X3 @ X0 ) )
=> ( ( X2 @ ( cS @ X0 ) )
= ( X3 @ ( cS @ X0 ) ) ) ) )
=> ! [X0: n] :
( ( X2 @ X0 )
= ( X3 @ X0 ) ) )
= cPA_IND_EQ ),
file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_IND_EQ_def) ).
thf(f17,plain,
( $true
= ( ~ ( ( cPA_IND_EQ
& cPA_2
& cPA_1 )
=> ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
thf(f10,plain,
( $true
= ( ~ ( ( cPA_IND_EQ
& cPA_2
& cPA_1 )
=> ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f9]) ).
thf(f9,plain,
~ ( ( cPA_1
& cPA_2
& cPA_IND_EQ )
=> ! [X0: n] :
( ( c_plus @ X0 @ c0 )
= ( c_plus @ c0 @ X0 ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,negated_conjecture,
~ ( ( cPA_1
& cPA_2
& cPA_IND_EQ )
=> ! [X0: n] :
( ( c_plus @ X0 @ c0 )
= ( c_plus @ c0 @ X0 ) ) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
thf(f4,conjecture,
( ( cPA_1
& cPA_2
& cPA_IND_EQ )
=> ! [X0: n] :
( ( c_plus @ X0 @ c0 )
= ( c_plus @ c0 @ X0 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_THM2) ).
thf(f102,plain,
( $false
= ( ( ( c_plus @ c0 @ sK3 )
= sK3 )
=> ( ( cS @ ( c_plus @ c0 @ sK3 ) )
= ( c_plus @ ( cS @ sK3 ) @ c0 ) ) ) ),
inference(forward_demodulation,[status(thm)],[f101,f49]) ).
thf(f49,plain,
! [X2: n,X1: n] :
( ( c_plus @ X1 @ ( cS @ X2 ) )
= ( cS @ ( c_plus @ X1 @ X2 ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f48]) ).
thf(f48,plain,
! [X2: n,X1: n] :
( ( ( c_plus @ X1 @ ( cS @ X2 ) )
= ( cS @ ( c_plus @ X1 @ X2 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f47]) ).
thf(f47,plain,
! [X2: n,X1: n] :
( $true
= ( ^ [Y0: n] :
( ( c_plus @ X1 @ ( cS @ Y0 ) )
= ( cS @ ( c_plus @ X1 @ Y0 ) ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f46]) ).
thf(f46,plain,
! [X1: n] :
( $true
= ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ X1 @ ( cS @ Y0 ) )
= ( cS @ ( c_plus @ X1 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f45]) ).
thf(f45,plain,
! [X1: n] :
( $true
= ( ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f44]) ).
thf(f44,plain,
( ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f43]) ).
thf(f43,plain,
( $true
= ( $true
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(backward_demodulation,[status(thm)],[f32,f42]) ).
thf(f42,plain,
( $true
= ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f32]) ).
thf(f32,plain,
( $true
= ( ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f31]) ).
thf(f31,plain,
( $true
= ( ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) ) )
& ( !! @ n
@ ^ [Y0: n] :
( !! @ n
@ ^ [Y1: n] :
( ( c_plus @ Y0 @ ( cS @ Y1 ) )
= ( cS @ ( c_plus @ Y0 @ Y1 ) ) ) ) )
& $true ) ),
inference(backward_demodulation,[status(thm)],[f23,f29]) ).
thf(f101,plain,
( ( ( ( c_plus @ c0 @ sK3 )
= sK3 )
=> ( ( c_plus @ c0 @ ( cS @ sK3 ) )
= ( c_plus @ ( cS @ sK3 ) @ c0 ) ) )
= $false ),
inference(forward_demodulation,[status(thm)],[f97,f35]) ).
thf(f97,plain,
( $false
= ( ( ( c_plus @ c0 @ sK3 )
= ( c_plus @ sK3 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ sK3 ) )
= ( c_plus @ ( cS @ sK3 ) @ c0 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f95]) ).
thf(f95,plain,
( ( ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) )
@ sK3 )
= $false ),
inference(sigma_clausification,[status(thm)],[f92]) ).
thf(f92,plain,
( ( !! @ n
@ ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f84]) ).
thf(f84,plain,
( $true
= ( ~ ( !! @ n
@ ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f83]) ).
thf(f83,plain,
( ( ~ ( ( !! @ n
@ ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) ) )
& $true ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f82]) ).
thf(f82,plain,
( $true
= ( ~ ( ( !! @ n
@ ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) ) )
& ( ( c_plus @ c0 @ c0 )
= ( c_plus @ c0 @ c0 ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f81]) ).
thf(f81,plain,
( $true
= ( ( ( !! @ n
@ ^ [Y0: n] :
( ( ( c_plus @ c0 @ Y0 )
= ( c_plus @ Y0 @ c0 ) )
=> ( ( c_plus @ c0 @ ( cS @ Y0 ) )
= ( c_plus @ ( cS @ Y0 ) @ c0 ) ) ) )
& ( ( c_plus @ c0 @ c0 )
= ( c_plus @ c0 @ c0 ) ) )
=> $false ) ),
inference(beta_eta_normalization,[status(thm)],[f63]) ).
thf(f63,plain,
( $true
= ( ( ( !! @ n
@ ^ [Y0: n] :
( ( ( ^ [Y1: n] : ( c_plus @ c0 @ Y1 )
@ Y0 )
= ( ^ [Y1: n] : ( c_plus @ Y1 @ c0 )
@ Y0 ) )
=> ( ( ^ [Y1: n] : ( c_plus @ c0 @ Y1 )
@ ( cS @ Y0 ) )
= ( ^ [Y1: n] : ( c_plus @ Y1 @ c0 )
@ ( cS @ Y0 ) ) ) ) )
& ( ( ^ [Y0: n] : ( c_plus @ c0 @ Y0 )
@ c0 )
= ( ^ [Y0: n] : ( c_plus @ Y0 @ c0 )
@ c0 ) ) )
=> $false ) ),
inference(superposition,[status(thm)],[f59,f25]) ).
thf(f25,plain,
( ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) )
= $false ),
inference(boolean_simplification,[status(thm)],[f24]) ).
thf(f24,plain,
( ( $true
=> ( !! @ n
@ ^ [Y0: n] :
( ( c_plus @ Y0 @ c0 )
= ( c_plus @ c0 @ Y0 ) ) ) )
= $false ),
inference(backward_demodulation,[status(thm)],[f19,f23]) ).
thf(f59,plain,
! [X2: n > n,X1: n > n] :
( $true
= ( ( ( !! @ n
@ ^ [Y0: n] :
( ( ( X2 @ Y0 )
= ( X1 @ Y0 ) )
=> ( ( X2 @ ( cS @ Y0 ) )
= ( X1 @ ( cS @ Y0 ) ) ) ) )
& ( ( X2 @ c0 )
= ( X1 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y0: n] :
( ( X1 @ Y0 )
= ( X2 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f58]) ).
thf(f58,plain,
! [X2: n > n,X1: n > n] :
( $true
= ( ^ [Y0: n > n] :
( ( ( !! @ n
@ ^ [Y1: n] :
( ( ( Y0 @ Y1 )
= ( X1 @ Y1 ) )
=> ( ( Y0 @ ( cS @ Y1 ) )
= ( X1 @ ( cS @ Y1 ) ) ) ) )
& ( ( Y0 @ c0 )
= ( X1 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y1: n] :
( ( X1 @ Y1 )
= ( Y0 @ Y1 ) ) ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f57]) ).
thf(f57,plain,
! [X1: n > n] :
( $true
= ( !! @ ( n > n )
@ ^ [Y0: n > n] :
( ( ( !! @ n
@ ^ [Y1: n] :
( ( ( Y0 @ Y1 )
= ( X1 @ Y1 ) )
=> ( ( Y0 @ ( cS @ Y1 ) )
= ( X1 @ ( cS @ Y1 ) ) ) ) )
& ( ( Y0 @ c0 )
= ( X1 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y1: n] :
( ( X1 @ Y1 )
= ( Y0 @ Y1 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f56]) ).
thf(f56,plain,
! [X1: n > n] :
( $true
= ( ^ [Y0: n > n] :
( !! @ ( n > n )
@ ^ [Y1: n > n] :
( ( ( !! @ n
@ ^ [Y2: n] :
( ( ( Y1 @ Y2 )
= ( Y0 @ Y2 ) )
=> ( ( Y1 @ ( cS @ Y2 ) )
= ( Y0 @ ( cS @ Y2 ) ) ) ) )
& ( ( Y1 @ c0 )
= ( Y0 @ c0 ) ) )
=> ( !! @ n
@ ^ [Y2: n] :
( ( Y0 @ Y2 )
= ( Y1 @ Y2 ) ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f42]) ).
thf(f107,plain,
( ( ( cS @ ( c_plus @ c0 @ sK3 ) )
= ( cS @ sK3 ) )
= $false ),
inference(boolean_simplification,[status(thm)],[f106]) ).
thf(f106,plain,
( ( $true
=> ( ( cS @ ( c_plus @ c0 @ sK3 ) )
= ( cS @ sK3 ) ) )
= $false ),
inference(backward_demodulation,[status(thm)],[f103,f105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : NUM827^5 : TPTP v9.2.1. Bugfixed v5.3.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.27 % Computer : n024.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Tue Feb 24 06:14:40 EST 2026
% 0.08/0.27 % CPUTime :
% 0.08/0.27 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.34 ---- Original DTF file ---
% 0.13/0.34 thf(spec,logic,$$dhol).
% 0.13/0.34 %------------------------------------------------------------------------------
% 0.13/0.34 % File : NUM827^5 : TPTP v9.2.1. Bugfixed v5.3.0.
% 0.13/0.34 % Domain : Number Theory (Induction on naturals)
% 0.13/0.34 % Problem : TPS problem PA-THM2
% 0.13/0.34 % Version : Especial.
% 0.13/0.34 % English :
% 0.13/0.34
% 0.13/0.34 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.13/0.34 % Source : [Bro09]
% 0.13/0.34 % Names : tps_0375 [Bro09]
% 0.13/0.34 % : PA-THM2 [TPS]
% 0.13/0.34
% 0.13/0.34 % Status : Theorem
% 0.13/0.34 % Rating : 0.44 v9.1.0, 0.38 v9.0.0, 0.40 v8.2.0, 0.54 v8.1.0, 0.55 v7.5.0, 0.29 v7.4.0, 0.33 v7.2.0, 0.25 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.57 v5.5.0, 0.67 v5.4.0, 0.60 v5.3.0
% 0.13/0.34 % Syntax : Number of formulae : 11 ( 3 unt; 7 typ; 3 def)
% 0.13/0.34 % Number of atoms : 16 ( 10 equ; 0 cnn)
% 0.13/0.34 % Maximal formula atoms : 4 ( 4 avg)
% 0.13/0.34 % Number of connectives : 28 ( 0 ~; 0 |; 3 &; 22 @)
% 0.13/0.34 % ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% 0.13/0.34 % Maximal formula depth : 4 ( 2 avg)
% 0.13/0.34 % Number of types : 2 ( 1 usr)
% 0.13/0.34 % Number of type conns : 5 ( 5 >; 0 *; 0 +; 0 <<)
% 0.13/0.34 % Number of symbols : 7 ( 6 usr; 4 con; 0-2 aty)
% 0.13/0.34 % Number of variables : 8 ( 0 ^; 8 !; 0 ?; 8 :)
% 0.13/0.34 % SPC : TH0_THM_EQU_NAR
% 0.13/0.34
% 0.13/0.34 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.13/0.34 % project in the Department of Mathematical Sciences at Carnegie
% 0.13/0.34 % Mellon University. Distributed under the Creative Commons copyleft
% 0.13/0.34 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.13/0.34 % :
% 0.13/0.34 % Bugfixes : v5.2.0 - Added missing type declarations.
% 0.13/0.34 % : v5.3.0 - Fixed tType to $tType from last bugfixes.
% 0.13/0.34 %------------------------------------------------------------------------------
% 0.13/0.34 thf(n_type,type,
% 0.13/0.34 n: $tType ).
% 0.13/0.34
% 0.13/0.34 thf(c0_type,type,
% 0.13/0.34 c0: n ).
% 0.13/0.34
% 0.13/0.34 thf(cS_type,type,
% 0.13/0.34 cS: n > n ).
% 0.13/0.34
% 0.13/0.34 thf(c_plus_type,type,
% 0.13/0.34 c_plus: n > n > n ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_1_type,type,
% 0.13/0.34 cPA_1: $o ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_2_type,type,
% 0.13/0.34 cPA_2: $o ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_IND_EQ_type,type,
% 0.13/0.34 cPA_IND_EQ: $o ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_1_def,definition,
% 0.13/0.34 ( cPA_1
% 0.13/0.34 = ( ! [Xx: n] :
% 0.13/0.34 ( ( c_plus @ Xx @ c0 )
% 0.13/0.34 = Xx ) ) ) ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_2_def,definition,
% 0.13/0.34 ( cPA_2
% 0.13/0.34 = ( ! [Xx: n,Xy: n] :
% 0.13/0.34 ( ( c_plus @ Xx @ ( cS @ Xy ) )
% 0.13/0.34 = ( cS @ ( c_plus @ Xx @ Xy ) ) ) ) ) ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_IND_EQ_def,definition,
% 0.13/0.34 ( cPA_IND_EQ
% 0.13/0.34 = ( ! [Xp: n > n,Xq: n > n] :
% 0.13/0.34 ( ( ( ( Xp @ c0 )
% 0.13/0.34 = ( Xq @ c0 ) )
% 0.13/0.34 & ! [Xx: n] :
% 0.13/0.34 ( ( ( Xp @ Xx )
% 0.13/0.34 = ( Xq @ Xx ) )
% 0.13/0.34 => ( ( Xp @ ( cS @ Xx ) )
% 0.13/0.34 = ( Xq @ ( cS @ Xx ) ) ) ) )
% 0.13/0.34 => ! [Xx: n] :
% 0.13/0.34 ( ( Xp @ Xx )
% 0.13/0.34 = ( Xq @ Xx ) ) ) ) ) ).
% 0.13/0.34
% 0.13/0.34 thf(cPA_THM2,conjecture,
% 0.13/0.34 ( ( cPA_1
% 0.13/0.34 & cPA_2
% 0.13/0.34 & cPA_IND_EQ )
% 0.13/0.34 => ! [Xx: n] :
% 0.13/0.34 ( ( c_plus @ Xx @ c0 )
% 0.13/0.34 = ( c_plus @ c0 @ Xx ) ) ) ).
% 0.13/0.34
% 0.13/0.34 %------------------------------------------------------------------------------
% 0.13/0.34 ------------------------
% 0.96/1.02 ---- Embedded in THF ---
% 0.96/1.02 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 0.96/1.02 %%% Generated on Tue Feb 24 06:14:41 EST 2026
% 0.96/1.02 %%% using '$$dhol' embedding, version 1.3.0.
% 0.96/1.02 %%% Logic specification used:
% 0.96/1.02 %%% thf(spec, logic, $$dhol).
% 0.96/1.02
% 0.96/1.02 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2DTF30830.p
% See solution above
% 0.96/1.02 ------------------------
% 1.21/1.03 ---- Cleaned THF ---
% 1.21/1.03 thf(n_type,type,
% 1.21/1.03 n: $tType ).
% 1.21/1.03
% 1.21/1.03 thf(c0_type,type,
% 1.21/1.03 c0: n ).
% 1.21/1.03
% 1.21/1.03 thf(cS_type,type,
% 1.21/1.03 cS: n > n ).
% 1.21/1.03
% 1.21/1.03 thf(c_plus_type,type,
% 1.21/1.03 c_plus: n > n > n ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_1_type,type,
% 1.21/1.03 cPA_1: $o ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_2_type,type,
% 1.21/1.03 cPA_2: $o ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_IND_EQ_type,type,
% 1.21/1.03 cPA_IND_EQ: $o ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_1_def,definition,
% 1.21/1.03 ( cPA_1
% 1.21/1.03 = ( ! [Xx: n] :
% 1.21/1.03 ( ( c_plus @ Xx @ c0 )
% 1.21/1.03 = Xx ) ) ) ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_2_def,definition,
% 1.21/1.03 ( cPA_2
% 1.21/1.03 = ( ! [Xx: n,Xy: n] :
% 1.21/1.03 ( ( c_plus @ Xx @ ( cS @ Xy ) )
% 1.21/1.03 = ( cS @ ( c_plus @ Xx @ Xy ) ) ) ) ) ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_IND_EQ_def,definition,
% 1.21/1.03 ( cPA_IND_EQ
% 1.21/1.03 = ( ! [Xp: n > n,Xq: n > n] :
% 1.21/1.03 ( ( ( ( Xp @ c0 )
% 1.21/1.03 = ( Xq @ c0 ) )
% 1.21/1.03 & ! [Xx: n] :
% 1.21/1.03 ( ( ( Xp @ Xx )
% 1.21/1.03 = ( Xq @ Xx ) )
% 1.21/1.03 => ( ( Xp @ ( cS @ Xx ) )
% 1.21/1.03 = ( Xq @ ( cS @ Xx ) ) ) ) )
% 1.21/1.03 => ! [Xx: n] :
% 1.21/1.03 ( ( Xp @ Xx )
% 1.21/1.03 = ( Xq @ Xx ) ) ) ) ) ).
% 1.21/1.03
% 1.21/1.03 thf(cPA_THM2,conjecture,
% 1.21/1.03 ( ( cPA_1
% 1.21/1.03 & cPA_2
% 1.21/1.03 & cPA_IND_EQ )
% 1.21/1.03 => ! [Xx: n] :
% 1.21/1.03 ( ( c_plus @ Xx @ c0 )
% 1.21/1.03 = ( c_plus @ c0 @ Xx ) ) ) ).
% 1.21/1.03 ------------------------
% 1.21/1.05 % (30936)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/183Mi)
% 1.21/1.05 % (30937)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_30830 for (2999ds/4Mi)
% 1.21/1.05 % (30939)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/2Mi)
% 1.21/1.05 % (30938)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_30830 for (2999ds/27Mi)
% 1.21/1.05 % (30941)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_30830 for (2999ds/275Mi)
% 1.21/1.05 % (30940)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_30830 for (2999ds/2Mi)
% 1.21/1.05 % (30942)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/18Mi)
% 1.21/1.05 % (30939)Instruction limit reached!
% 1.21/1.05 % (30939)------------------------------
% 1.21/1.05 % (30939)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.05 % (30939)Termination reason: Unknown
% 1.21/1.05 % (30939)Termination phase: Preprocessing 2
% 1.21/1.05
% 1.21/1.05 % (30939)Memory used [KB]: 895
% 1.21/1.05 % (30939)Time elapsed: 0.002 s
% 1.21/1.05 % (30939)Instructions burned: 2 (million)
% 1.21/1.05 % (30939)------------------------------
% 1.21/1.05 % (30939)------------------------------
% 1.21/1.05 % (30940)Instruction limit reached!
% 1.21/1.05 % (30940)------------------------------
% 1.21/1.05 % (30940)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.05 % (30940)Termination reason: Unknown
% 1.21/1.05 % (30940)Termination phase: Property scanning
% 1.21/1.05
% 1.21/1.05 % (30940)Memory used [KB]: 895
% 1.21/1.05 % (30940)Time elapsed: 0.002 s
% 1.21/1.05 % (30940)Instructions burned: 2 (million)
% 1.21/1.05 % (30940)------------------------------
% 1.21/1.05 % (30940)------------------------------
% 1.21/1.05 % (30937)Instruction limit reached!
% 1.21/1.05 % (30937)------------------------------
% 1.21/1.05 % (30937)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.05 % (30937)Termination reason: Unknown
% 1.21/1.05 % (30937)Termination phase: Saturation
% 1.21/1.05
% 1.21/1.05 % (30937)Memory used [KB]: 5500
% 1.21/1.05 % (30937)Time elapsed: 0.004 s
% 1.21/1.05 % (30937)Instructions burned: 5 (million)
% 1.21/1.05 % (30937)------------------------------
% 1.21/1.05 % (30937)------------------------------
% 1.21/1.06 % (30942)Instruction limit reached!
% 1.21/1.06 % (30942)------------------------------
% 1.21/1.06 % (30942)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.06 % (30942)Termination reason: Unknown
% 1.21/1.06 % (30942)Termination phase: Saturation
% 1.21/1.06
% 1.21/1.06 % (30942)Memory used [KB]: 5628
% 1.21/1.06 % (30942)Time elapsed: 0.010 s
% 1.21/1.06 % (30942)Instructions burned: 18 (million)
% 1.21/1.06 % (30942)------------------------------
% 1.21/1.06 % (30942)------------------------------
% 1.21/1.07 % (30938)Instruction limit reached!
% 1.21/1.07 % (30938)------------------------------
% 1.21/1.07 % (30938)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.07 % (30938)Termination reason: Unknown
% 1.21/1.07 % (30938)Termination phase: Saturation
% 1.21/1.07
% 1.21/1.07 % (30938)Memory used [KB]: 5628
% 1.21/1.07 % (30938)Time elapsed: 0.015 s
% 1.21/1.07 % (30938)Instructions burned: 28 (million)
% 1.21/1.07 % (30938)------------------------------
% 1.21/1.07 % (30938)------------------------------
% 1.21/1.07 % (30943)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/3Mi)
% 1.21/1.07 % (30944)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_30830 for (2999ds/37Mi)
% 1.21/1.07 % (30945)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_30830 for (2999ds/15Mi)
% 1.21/1.07 % (30943)Instruction limit reached!
% 1.21/1.07 % (30943)------------------------------
% 1.21/1.07 % (30943)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.07 % (30943)Termination reason: Unknown
% 1.21/1.07 % (30943)Termination phase: Saturation
% 1.21/1.07
% 1.21/1.07 % (30943)Memory used [KB]: 5500
% 1.21/1.07 % (30943)Time elapsed: 0.003 s
% 1.21/1.07 % (30943)Instructions burned: 4 (million)
% 1.21/1.07 % (30943)------------------------------
% 1.21/1.07 % (30943)------------------------------
% 1.21/1.08 % (30946)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_30830 for (2999ds/3Mi)
% 1.21/1.08 % (30945)Instruction limit reached!
% 1.21/1.08 % (30945)------------------------------
% 1.21/1.08 % (30945)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.08 % (30945)Termination reason: Unknown
% 1.21/1.08 % (30945)Termination phase: Saturation
% 1.21/1.08
% 1.21/1.08 % (30945)Memory used [KB]: 5500
% 1.21/1.08 % (30945)Time elapsed: 0.009 s
% 1.21/1.08 % (30945)Instructions burned: 16 (million)
% 1.21/1.08 % (30945)------------------------------
% 1.21/1.08 % (30945)------------------------------
% 1.21/1.08 % (30946)Instruction limit reached!
% 1.21/1.08 % (30946)------------------------------
% 1.21/1.08 % (30946)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.08 % (30946)Termination reason: Unknown
% 1.21/1.08 % (30946)Termination phase: Saturation
% 1.21/1.08
% 1.21/1.08 % (30946)Memory used [KB]: 5500
% 1.21/1.08 % (30946)Time elapsed: 0.003 s
% 1.21/1.08 % (30946)Instructions burned: 4 (million)
% 1.21/1.08 % (30946)------------------------------
% 1.21/1.08 % (30946)------------------------------
% 1.21/1.08 % (30947)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_30830 for (2999ds/1041Mi)
% 1.21/1.09 % (30948)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/7Mi)
% 1.21/1.09 % (30944)Instruction limit reached!
% 1.21/1.09 % (30944)------------------------------
% 1.21/1.09 % (30944)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.09 % (30944)Termination reason: Unknown
% 1.21/1.09 % (30944)Termination phase: Saturation
% 1.21/1.09
% 1.21/1.09 % (30944)Memory used [KB]: 5628
% 1.21/1.09 % (30944)Time elapsed: 0.019 s
% 1.21/1.09 % (30944)Instructions burned: 37 (million)
% 1.21/1.09 % (30944)------------------------------
% 1.21/1.09 % (30944)------------------------------
% 1.21/1.09 % (30948)Instruction limit reached!
% 1.21/1.09 % (30948)------------------------------
% 1.21/1.09 % (30948)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.09 % (30948)Termination reason: Unknown
% 1.21/1.09 % (30948)Termination phase: Saturation
% 1.21/1.09
% 1.21/1.09 % (30948)Memory used [KB]: 1023
% 1.21/1.09 % (30948)Time elapsed: 0.005 s
% 1.21/1.09 % (30948)Instructions burned: 8 (million)
% 1.21/1.09 % (30948)------------------------------
% 1.21/1.09 % (30948)------------------------------
% 1.21/1.09 % (30949)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/16Mi)
% 1.21/1.09 % (30950)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_30830 for (2999ds/3Mi)
% 1.21/1.10 % (30950)Instruction limit reached!
% 1.21/1.10 % (30950)------------------------------
% 1.21/1.10 % (30950)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.10 % (30950)Termination reason: Unknown
% 1.21/1.10 % (30950)Termination phase: Saturation
% 1.21/1.10
% 1.21/1.10 % (30950)Memory used [KB]: 5500
% 1.21/1.10 % (30950)Time elapsed: 0.003 s
% 1.21/1.10 % (30950)Instructions burned: 4 (million)
% 1.21/1.10 % (30950)------------------------------
% 1.21/1.10 % (30950)------------------------------
% 1.21/1.10 % (30951)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_30830 for (2999ds/3Mi)
% 1.21/1.10 % (30949)Instruction limit reached!
% 1.21/1.10 % (30949)------------------------------
% 1.21/1.10 % (30949)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.10 % (30949)Termination reason: Unknown
% 1.21/1.10 % (30949)Termination phase: Saturation
% 1.21/1.10
% 1.21/1.10 % (30949)Memory used [KB]: 5756
% 1.21/1.10 % (30949)Time elapsed: 0.010 s
% 1.21/1.10 % (30949)Instructions burned: 16 (million)
% 1.21/1.10 % (30949)------------------------------
% 1.21/1.10 % (30949)------------------------------
% 1.21/1.10 % (30936)Instruction limit reached!
% 1.21/1.10 % (30936)------------------------------
% 1.21/1.10 % (30936)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.10 % (30936)Termination reason: Unknown
% 1.21/1.10 % (30936)Termination phase: Saturation
% 1.21/1.10
% 1.21/1.10 % (30936)Memory used [KB]: 5884
% 1.21/1.10 % (30936)Time elapsed: 0.053 s
% 1.21/1.10 % (30936)Instructions burned: 186 (million)
% 1.21/1.10 % (30936)------------------------------
% 1.21/1.10 % (30936)------------------------------
% 1.21/1.10 % (30951)Instruction limit reached!
% 1.21/1.10 % (30951)------------------------------
% 1.21/1.10 % (30951)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.10 % (30951)Termination reason: Unknown
% 1.21/1.10 % (30951)Termination phase: Saturation
% 1.21/1.10
% 1.21/1.10 % (30951)Memory used [KB]: 1023
% 1.21/1.10 % (30951)Time elapsed: 0.003 s
% 1.21/1.10 % (30951)Instructions burned: 4 (million)
% 1.21/1.10 % (30951)------------------------------
% 1.21/1.10 % (30951)------------------------------
% 1.21/1.10 % (30952)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/7Mi)
% 1.21/1.11 % (30952)Refutation not found, incomplete strategy
% 1.21/1.11 % (30952)------------------------------
% 1.21/1.11 % (30952)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.11 % (30952)Termination reason: Refutation not found, incomplete strategy
% 1.21/1.11
% 1.21/1.11
% 1.21/1.11 % (30952)Memory used [KB]: 5500
% 1.21/1.11 % (30952)Time elapsed: 0.002 s
% 1.21/1.11 % (30952)Instructions burned: 2 (million)
% 1.21/1.11 % (30952)------------------------------
% 1.21/1.11 % (30952)------------------------------
% 1.21/1.11 % (30953)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/3Mi)
% 1.21/1.11 % (30955)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/18Mi)
% 1.21/1.11 % (30953)Instruction limit reached!
% 1.21/1.11 % (30953)------------------------------
% 1.21/1.11 % (30953)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.11 % (30953)Termination reason: Unknown
% 1.21/1.11 % (30953)Termination phase: Saturation
% 1.21/1.11
% 1.21/1.11 % (30953)Memory used [KB]: 5500
% 1.21/1.11 % (30953)Time elapsed: 0.003 s
% 1.21/1.11 % (30953)Instructions burned: 4 (million)
% 1.21/1.11 % (30953)------------------------------
% 1.21/1.11 % (30953)------------------------------
% 1.21/1.12 % (30955)Instruction limit reached!
% 1.21/1.12 % (30955)------------------------------
% 1.21/1.12 % (30955)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.12 % (30955)Termination reason: Unknown
% 1.21/1.12 % (30955)Termination phase: Saturation
% 1.21/1.12
% 1.21/1.12 % (30955)Memory used [KB]: 5628
% 1.21/1.12 % (30955)Time elapsed: 0.007 s
% 1.21/1.12 % (30955)Instructions burned: 19 (million)
% 1.21/1.12 % (30955)------------------------------
% 1.21/1.12 % (30955)------------------------------
% 1.21/1.12 % (30954)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/4Mi)
% 1.21/1.12 % (30956)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/710Mi)
% 1.21/1.12 % (30954)Instruction limit reached!
% 1.21/1.12 % (30954)------------------------------
% 1.21/1.12 % (30954)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.21/1.12 % (30954)Termination reason: Unknown
% 1.21/1.12 % (30954)Termination phase: Saturation
% 1.21/1.12
% 1.21/1.12 % (30954)Memory used [KB]: 5500
% 1.21/1.12 % (30954)Time elapsed: 0.003 s
% 1.21/1.12 % (30954)Instructions burned: 4 (million)
% 1.21/1.12 % (30954)------------------------------
% 1.21/1.12 % (30954)------------------------------
% 1.21/1.12 % (30957)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/6Mi)
% 1.22/1.13 % (30957)Instruction limit reached!
% 1.22/1.13 % (30957)------------------------------
% 1.22/1.13 % (30957)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.13 % (30957)Termination reason: Unknown
% 1.22/1.13 % (30957)Termination phase: Saturation
% 1.22/1.13
% 1.22/1.13 % (30957)Memory used [KB]: 5500
% 1.22/1.13 % (30957)Time elapsed: 0.005 s
% 1.22/1.13 % (30957)Instructions burned: 6 (million)
% 1.22/1.13 % (30957)------------------------------
% 1.22/1.13 % (30957)------------------------------
% 1.22/1.13 % (30959)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_30830 for (2999ds/21Mi)
% 1.22/1.13 % (30958)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_30830 for (2999ds/902Mi)
% 1.22/1.13 % (30959)Instruction limit reached!
% 1.22/1.13 % (30959)------------------------------
% 1.22/1.13 % (30959)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.13 % (30959)Termination reason: Unknown
% 1.22/1.13 % (30959)Termination phase: Saturation
% 1.22/1.13
% 1.22/1.13 % (30959)Memory used [KB]: 5628
% 1.22/1.13 % (30959)Time elapsed: 0.009 s
% 1.22/1.13 % (30959)Instructions burned: 23 (million)
% 1.22/1.13 % (30959)------------------------------
% 1.22/1.13 % (30959)------------------------------
% 1.22/1.13 % (30960)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/5Mi)
% 1.22/1.14 % (30960)Instruction limit reached!
% 1.22/1.14 % (30960)------------------------------
% 1.22/1.14 % (30960)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.14 % (30960)Termination reason: Unknown
% 1.22/1.14 % (30960)Termination phase: Saturation
% 1.22/1.14
% 1.22/1.14 % (30960)Memory used [KB]: 5500
% 1.22/1.14 % (30960)Time elapsed: 0.004 s
% 1.22/1.14 % (30960)Instructions burned: 6 (million)
% 1.22/1.14 % (30960)------------------------------
% 1.22/1.14 % (30960)------------------------------
% 1.22/1.14 % (30961)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_30830 for (2999ds/6Mi)
% 1.22/1.14 % (30961)Instruction limit reached!
% 1.22/1.14 % (30961)------------------------------
% 1.22/1.14 % (30961)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.14 % (30961)Termination reason: Unknown
% 1.22/1.14 % (30961)Termination phase: Saturation
% 1.22/1.14
% 1.22/1.14 % (30961)Memory used [KB]: 5500
% 1.22/1.14 % (30961)Time elapsed: 0.004 s
% 1.22/1.14 % (30961)Instructions burned: 6 (million)
% 1.22/1.14 % (30961)------------------------------
% 1.22/1.14 % (30961)------------------------------
% 1.22/1.14 % (30962)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_30830 for (2999ds/377Mi)
% 1.22/1.15 % (30963)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_30830 for (2999ds/779Mi)
% 1.22/1.16 % (30964)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_30830 for (2999ds/19Mi)
% 1.22/1.16 % (30964)Refutation not found, incomplete strategy
% 1.22/1.16 % (30964)------------------------------
% 1.22/1.16 % (30964)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.16 % (30964)Termination reason: Refutation not found, incomplete strategy
% 1.22/1.16
% 1.22/1.16
% 1.22/1.16 % (30964)Memory used [KB]: 5500
% 1.22/1.16 % (30964)Time elapsed: 0.005 s
% 1.22/1.16 % (30964)Instructions burned: 6 (million)
% 1.22/1.16 % (30964)------------------------------
% 1.22/1.16 % (30964)------------------------------
% 1.22/1.18 % (30941)Instruction limit reached!
% 1.22/1.18 % (30941)------------------------------
% 1.22/1.18 % (30941)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.18 % (30941)Termination reason: Unknown
% 1.22/1.18 % (30941)Termination phase: Saturation
% 1.22/1.18
% 1.22/1.18 % (30941)Memory used [KB]: 5756
% 1.22/1.18 % (30941)Time elapsed: 0.126 s
% 1.22/1.18 % (30941)Instructions burned: 275 (million)
% 1.22/1.18 % (30941)------------------------------
% 1.22/1.18 % (30941)------------------------------
% 1.22/1.18 % (30965)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_30830 for (2998ds/879Mi)
% 1.22/1.19 % (30966)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_30830 for (2998ds/17Mi)
% 1.22/1.20 % (30966)Instruction limit reached!
% 1.22/1.20 % (30966)------------------------------
% 1.22/1.20 % (30966)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.20 % (30966)Termination reason: Unknown
% 1.22/1.20 % (30966)Termination phase: Saturation
% 1.22/1.20
% 1.22/1.20 % (30966)Memory used [KB]: 5628
% 1.22/1.20 % (30966)Time elapsed: 0.010 s
% 1.22/1.20 % (30966)Instructions burned: 18 (million)
% 1.22/1.20 % (30966)------------------------------
% 1.22/1.20 % (30966)------------------------------
% 1.22/1.22 % (30967)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_30830 for (2998ds/3Mi)
% 1.22/1.22 % (30967)Instruction limit reached!
% 1.22/1.22 % (30967)------------------------------
% 1.22/1.22 % (30967)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.22 % (30967)Termination reason: Unknown
% 1.22/1.22 % (30967)Termination phase: Saturation
% 1.22/1.22
% 1.22/1.22 % (30967)Memory used [KB]: 1023
% 1.22/1.22 % (30967)Time elapsed: 0.003 s
% 1.22/1.22 % (30967)Instructions burned: 4 (million)
% 1.22/1.22 % (30967)------------------------------
% 1.22/1.22 % (30967)------------------------------
% 1.22/1.23 % (30968)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_30830 for (2998ds/30Mi)
% 1.22/1.24 % (30968)Refutation not found, incomplete strategy
% 1.22/1.24 % (30968)------------------------------
% 1.22/1.24 % (30968)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.24 % (30968)Termination reason: Refutation not found, incomplete strategy
% 1.22/1.24
% 1.22/1.24
% 1.22/1.24 % (30968)Memory used [KB]: 5500
% 1.22/1.24 % (30968)Time elapsed: 0.003 s
% 1.22/1.24 % (30968)Instructions burned: 4 (million)
% 1.22/1.24 % (30968)------------------------------
% 1.22/1.24 % (30968)------------------------------
% 1.22/1.25 % (30969)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_30830 for (2998ds/127Mi)
% 1.22/1.25 % (30962)Instruction limit reached!
% 1.22/1.25 % (30962)------------------------------
% 1.22/1.25 % (30962)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.25 % (30962)Termination reason: Unknown
% 1.22/1.25 % (30962)Termination phase: Saturation
% 1.22/1.25
% 1.22/1.25 % (30962)Memory used [KB]: 6140
% 1.22/1.25 % (30962)Time elapsed: 0.109 s
% 1.22/1.25 % (30962)Instructions burned: 377 (million)
% 1.22/1.25 % (30962)------------------------------
% 1.22/1.25 % (30962)------------------------------
% 1.22/1.26 % (30970)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_30830 for (2997ds/100Mi)
% 1.22/1.29 % (30970)Instruction limit reached!
% 1.22/1.29 % (30970)------------------------------
% 1.22/1.29 % (30970)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.29 % (30970)Termination reason: Unknown
% 1.22/1.29 % (30970)Termination phase: Saturation
% 1.22/1.29
% 1.22/1.29 % (30970)Memory used [KB]: 5756
% 1.22/1.29 % (30970)Time elapsed: 0.030 s
% 1.22/1.29 % (30970)Instructions burned: 100 (million)
% 1.22/1.29 % (30970)------------------------------
% 1.22/1.29 % (30970)------------------------------
% 1.22/1.30 % (30971)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_30830 for (2997ds/3Mi)
% 1.22/1.30 % (30971)Instruction limit reached!
% 1.22/1.30 % (30971)------------------------------
% 1.22/1.30 % (30971)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.30 % (30971)Termination reason: Unknown
% 1.22/1.30 % (30971)Termination phase: Saturation
% 1.22/1.30
% 1.22/1.30 % (30971)Memory used [KB]: 5500
% 1.22/1.30 % (30971)Time elapsed: 0.002 s
% 1.22/1.30 % (30971)Instructions burned: 3 (million)
% 1.22/1.30 % (30971)------------------------------
% 1.22/1.30 % (30971)------------------------------
% 1.22/1.31 % (30972)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_30830 for (2997ds/20Mi)
% 1.22/1.31 % (30969)Instruction limit reached!
% 1.22/1.31 % (30969)------------------------------
% 1.22/1.31 % (30969)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.31 % (30969)Termination reason: Unknown
% 1.22/1.31 % (30969)Termination phase: Saturation
% 1.22/1.31
% 1.22/1.31 % (30969)Memory used [KB]: 5884
% 1.22/1.31 % (30969)Time elapsed: 0.061 s
% 1.22/1.31 % (30969)Instructions burned: 128 (million)
% 1.22/1.31 % (30969)------------------------------
% 1.22/1.31 % (30969)------------------------------
% 1.22/1.32 % (30972)Instruction limit reached!
% 1.22/1.32 % (30972)------------------------------
% 1.22/1.32 % (30972)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.32 % (30972)Termination reason: Unknown
% 1.22/1.32 % (30972)Termination phase: Saturation
% 1.22/1.32
% 1.22/1.32 % (30972)Memory used [KB]: 5628
% 1.22/1.32 % (30972)Time elapsed: 0.007 s
% 1.22/1.32 % (30972)Instructions burned: 20 (million)
% 1.22/1.32 % (30972)------------------------------
% 1.22/1.32 % (30972)------------------------------
% 1.22/1.33 % (30974)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_30830 for (2997ds/107Mi)
% 1.22/1.33 % (30973)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_30830 for (2997ds/86Mi)
% 1.22/1.36 % (30974)Instruction limit reached!
% 1.22/1.36 % (30974)------------------------------
% 1.22/1.36 % (30974)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.36 % (30974)Termination reason: Unknown
% 1.22/1.36 % (30974)Termination phase: Saturation
% 1.22/1.36
% 1.22/1.36 % (30974)Memory used [KB]: 5756
% 1.22/1.36 % (30974)Time elapsed: 0.033 s
% 1.22/1.36 % (30974)Instructions burned: 109 (million)
% 1.22/1.36 % (30974)------------------------------
% 1.22/1.36 % (30974)------------------------------
% 1.22/1.37 % (30975)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_30830 for (2996ds/39Mi)
% 1.22/1.37 % (30973)Instruction limit reached!
% 1.22/1.37 % (30973)------------------------------
% 1.22/1.37 % (30973)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.37 % (30973)Termination reason: Unknown
% 1.22/1.37 % (30973)Termination phase: Saturation
% 1.22/1.37
% 1.22/1.37 % (30973)Memory used [KB]: 5756
% 1.22/1.37 % (30973)Time elapsed: 0.042 s
% 1.22/1.37 % (30973)Instructions burned: 86 (million)
% 1.22/1.37 % (30973)------------------------------
% 1.22/1.37 % (30973)------------------------------
% 1.22/1.38 % (30975)First to succeed.
% 1.22/1.38 % (30975)Refutation found. Thanks to Tanya!
% 1.22/1.38 % SZS status Theorem for DTF2THF_30830
% 1.22/1.38 % SZS output start Proof for DTF2THF_30830
% 1.22/1.38 thf(type_def_5, type, n: $tType).
% 1.22/1.38 thf(func_def_0, type, n: $tType).
% 1.22/1.38 thf(func_def_1, type, c0: n).
% 1.22/1.38 thf(func_def_2, type, cS: n > n).
% 1.22/1.38 thf(func_def_3, type, c_plus: n > n > n).
% 1.22/1.38 thf(func_def_20, type, ph1: !>[X0: $tType]:(X0)).
% 1.22/1.38 thf(func_def_21, type, sK2: n).
% 1.22/1.38 thf(func_def_22, type, sK3: n).
% 1.22/1.38 thf(f120,plain,(
% 1.22/1.38 $false),
% 1.22/1.38 inference(trivial_inequality_removal,[status(thm)],[f119])).
% 1.22/1.38 thf(f119,plain,(
% 1.22/1.38 ($true = $false)),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f116])).
% 1.22/1.38 thf(f116,plain,(
% 1.22/1.38 (((cS @ sK3) = (cS @ sK3)) = $false)),
% 1.22/1.38 inference(backward_demodulation,[status(thm)],[f107,f108])).
% 1.22/1.38 thf(f108,plain,(
% 1.22/1.38 (sK3 = (c_plus @ c0 @ sK3))),
% 1.22/1.38 inference(equality_proxy_clausification,[status(thm)],[f105])).
% 1.22/1.38 thf(f105,plain,(
% 1.22/1.38 ($true = ((c_plus @ c0 @ sK3) = sK3))),
% 1.22/1.38 inference(binary_proxy_clausification,[status(thm)],[f103])).
% 1.22/1.38 thf(f103,plain,(
% 1.22/1.38 ((((c_plus @ c0 @ sK3) = sK3) => ((cS @ (c_plus @ c0 @ sK3)) = (cS @ sK3))) = $false)),
% 1.22/1.38 inference(forward_demodulation,[status(thm)],[f102,f35])).
% 1.22/1.38 thf(f35,plain,(
% 1.22/1.38 ( ! [X1 : n] : (((c_plus @ X1 @ c0) = X1)) )),
% 1.22/1.38 inference(equality_proxy_clausification,[status(thm)],[f34])).
% 1.22/1.38 thf(f34,plain,(
% 1.22/1.38 ( ! [X1 : n] : (($true = ((c_plus @ X1 @ c0) = X1))) )),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f33])).
% 1.22/1.38 thf(f33,plain,(
% 1.22/1.38 ( ! [X1 : n] : (($true = ((^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0)) @ X1))) )),
% 1.22/1.38 inference(pi_clausification,[status(thm)],[f29])).
% 1.22/1.38 thf(f29,plain,(
% 1.22/1.38 ($true = (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0))))),
% 1.22/1.38 inference(binary_proxy_clausification,[status(thm)],[f23])).
% 1.22/1.38 thf(f23,plain,(
% 1.22/1.38 ($true = (((!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))) & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))) & (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0)))))),
% 1.22/1.38 inference(binary_proxy_clausification,[status(thm)],[f19])).
% 1.22/1.38 thf(f19,plain,(
% 1.22/1.38 (((((!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))) & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))) & (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0)))) => (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0))))) = $false)),
% 1.22/1.38 inference(not_proxy_clausification,[status(thm)],[f18])).
% 1.22/1.38 thf(f18,plain,(
% 1.22/1.38 ((~ ((((!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))) & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))) & (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0)))) => (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0)))))) = $true)),
% 1.22/1.38 inference(definition_unfolding,[status(thm)],[f17,f16,f15,f14])).
% 1.22/1.38 thf(f14,plain,(
% 1.22/1.38 (cPA_1 = (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0))))),
% 1.22/1.38 inference(cnf_transformation,[status(thm)],[f11])).
% 1.22/1.38 thf(f11,plain,(
% 1.22/1.38 (cPA_1 = (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = Y0))))),
% 1.22/1.38 inference(fool_elimination,[status(thm)],[f1])).
% 1.22/1.38 thf(f1,axiom,(
% 1.22/1.38 (! [X0 : n] : ((c_plus @ X0 @ c0) = X0) = cPA_1)),
% 1.22/1.38 file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_1_def)).
% 1.22/1.38 thf(f15,plain,(
% 1.22/1.38 (cPA_2 = (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1))))))))),
% 1.22/1.38 inference(cnf_transformation,[status(thm)],[f8])).
% 1.22/1.38 thf(f8,plain,(
% 1.22/1.38 (cPA_2 = (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1))))))))),
% 1.22/1.38 inference(fool_elimination,[status(thm)],[f7])).
% 1.22/1.38 thf(f7,plain,(
% 1.22/1.38 (! [X0 : n,X1 : n] : ((c_plus @ X1 @ (cS @ X0)) = (cS @ (c_plus @ X1 @ X0))) = cPA_2)),
% 1.22/1.38 inference(rectify,[status(thm)],[f2])).
% 1.22/1.38 thf(f2,axiom,(
% 1.22/1.38 (! [X1 : n,X0 : n] : ((c_plus @ X0 @ (cS @ X1)) = (cS @ (c_plus @ X0 @ X1))) = cPA_2)),
% 1.22/1.38 file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_2_def)).
% 1.22/1.38 thf(f16,plain,(
% 1.22/1.38 (cPA_IND_EQ = (!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))))),
% 1.22/1.38 inference(cnf_transformation,[status(thm)],[f13])).
% 1.22/1.38 thf(f13,plain,(
% 1.22/1.38 (cPA_IND_EQ = (!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))))),
% 1.22/1.38 inference(fool_elimination,[status(thm)],[f12])).
% 1.22/1.38 thf(f12,plain,(
% 1.22/1.38 (! [X0 : n > n,X1 : n > n] : ((((X0 @ c0) = (X1 @ c0)) & ! [X2 : n] : (((X0 @ X2) = (X1 @ X2)) => ((X0 @ (cS @ X2)) = (X1 @ (cS @ X2))))) => ! [X3 : n] : ((X1 @ X3) = (X0 @ X3))) = cPA_IND_EQ)),
% 1.22/1.38 inference(rectify,[status(thm)],[f3])).
% 1.22/1.38 thf(f3,axiom,(
% 1.22/1.38 (! [X3 : n > n,X2 : n > n] : ((((X2 @ c0) = (X3 @ c0)) & ! [X0 : n] : (((X2 @ X0) = (X3 @ X0)) => ((X2 @ (cS @ X0)) = (X3 @ (cS @ X0))))) => ! [X0 : n] : ((X2 @ X0) = (X3 @ X0))) = cPA_IND_EQ)),
% 1.22/1.38 file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_IND_EQ_def)).
% 1.22/1.38 thf(f17,plain,(
% 1.22/1.38 ($true = (~ (((cPA_IND_EQ & cPA_2) & cPA_1) => (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0)))))))),
% 1.22/1.38 inference(cnf_transformation,[status(thm)],[f10])).
% 1.22/1.38 thf(f10,plain,(
% 1.22/1.38 ($true = (~ (((cPA_IND_EQ & cPA_2) & cPA_1) => (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0)))))))),
% 1.22/1.38 inference(fool_elimination,[status(thm)],[f9])).
% 1.22/1.38 thf(f9,plain,(
% 1.22/1.38 ~((cPA_1 & cPA_2 & cPA_IND_EQ) => ! [X0 : n] : ((c_plus @ X0 @ c0) = (c_plus @ c0 @ X0)))),
% 1.22/1.38 inference(rectify,[status(thm)],[f5])).
% 1.22/1.38 thf(f5,negated_conjecture,(
% 1.22/1.38 ~((cPA_1 & cPA_2 & cPA_IND_EQ) => ! [X0 : n] : ((c_plus @ X0 @ c0) = (c_plus @ c0 @ X0)))),
% 1.22/1.38 inference(negated_conjecture,[status(cth)],[f4])).
% 1.22/1.38 thf(f4,conjecture,(
% 1.22/1.38 (cPA_1 & cPA_2 & cPA_IND_EQ) => ! [X0 : n] : ((c_plus @ X0 @ c0) = (c_plus @ c0 @ X0))),
% 1.22/1.38 file('/export/starexec/sandbox/tmp/tmp.wsNPEHhc16/DTF2THF_30830.p',cPA_THM2)).
% 1.22/1.38 thf(f102,plain,(
% 1.22/1.38 ($false = (((c_plus @ c0 @ sK3) = sK3) => ((cS @ (c_plus @ c0 @ sK3)) = (c_plus @ (cS @ sK3) @ c0))))),
% 1.22/1.38 inference(forward_demodulation,[status(thm)],[f101,f49])).
% 1.22/1.38 thf(f49,plain,(
% 1.22/1.38 ( ! [X2 : n,X1 : n] : (((c_plus @ X1 @ (cS @ X2)) = (cS @ (c_plus @ X1 @ X2)))) )),
% 1.22/1.38 inference(equality_proxy_clausification,[status(thm)],[f48])).
% 1.22/1.38 thf(f48,plain,(
% 1.22/1.38 ( ! [X2 : n,X1 : n] : ((((c_plus @ X1 @ (cS @ X2)) = (cS @ (c_plus @ X1 @ X2))) = $true)) )),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f47])).
% 1.22/1.38 thf(f47,plain,(
% 1.22/1.38 ( ! [X2 : n,X1 : n] : (($true = ((^[Y0 : n]: ((c_plus @ X1 @ (cS @ Y0)) = (cS @ (c_plus @ X1 @ Y0)))) @ X2))) )),
% 1.22/1.38 inference(pi_clausification,[status(thm)],[f46])).
% 1.22/1.38 thf(f46,plain,(
% 1.22/1.38 ( ! [X1 : n] : (($true = (!! @ n @ (^[Y0 : n]: ((c_plus @ X1 @ (cS @ Y0)) = (cS @ (c_plus @ X1 @ Y0))))))) )),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f45])).
% 1.22/1.38 thf(f45,plain,(
% 1.22/1.38 ( ! [X1 : n] : (($true = ((^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))) @ X1))) )),
% 1.22/1.38 inference(pi_clausification,[status(thm)],[f44])).
% 1.22/1.38 thf(f44,plain,(
% 1.22/1.38 ((!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1))))))) = $true)),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f43])).
% 1.22/1.38 thf(f43,plain,(
% 1.22/1.38 ($true = ($true & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))))),
% 1.22/1.38 inference(backward_demodulation,[status(thm)],[f32,f42])).
% 1.22/1.38 thf(f42,plain,(
% 1.22/1.38 ($true = (!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))))),
% 1.22/1.38 inference(binary_proxy_clausification,[status(thm)],[f32])).
% 1.22/1.38 thf(f32,plain,(
% 1.22/1.38 ($true = ((!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))) & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))))),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f31])).
% 1.22/1.38 thf(f31,plain,(
% 1.22/1.38 ($true = (((!! @ (n > n) @ (^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2))))))))) & (!! @ n @ (^[Y0 : n]: (!! @ n @ (^[Y1 : n]: ((c_plus @ Y0 @ (cS @ Y1)) = (cS @ (c_plus @ Y0 @ Y1)))))))) & $true))),
% 1.22/1.38 inference(backward_demodulation,[status(thm)],[f23,f29])).
% 1.22/1.38 thf(f101,plain,(
% 1.22/1.38 ((((c_plus @ c0 @ sK3) = sK3) => ((c_plus @ c0 @ (cS @ sK3)) = (c_plus @ (cS @ sK3) @ c0))) = $false)),
% 1.22/1.38 inference(forward_demodulation,[status(thm)],[f97,f35])).
% 1.22/1.38 thf(f97,plain,(
% 1.22/1.38 ($false = (((c_plus @ c0 @ sK3) = (c_plus @ sK3 @ c0)) => ((c_plus @ c0 @ (cS @ sK3)) = (c_plus @ (cS @ sK3) @ c0))))),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f95])).
% 1.22/1.38 thf(f95,plain,(
% 1.22/1.38 (((^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0)))) @ sK3) = $false)),
% 1.22/1.38 inference(sigma_clausification,[status(thm)],[f92])).
% 1.22/1.38 thf(f92,plain,(
% 1.22/1.38 ((!! @ n @ (^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0))))) = $false)),
% 1.22/1.38 inference(not_proxy_clausification,[status(thm)],[f84])).
% 1.22/1.38 thf(f84,plain,(
% 1.22/1.38 ($true = (~ (!! @ n @ (^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0)))))))),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f83])).
% 1.22/1.38 thf(f83,plain,(
% 1.22/1.38 ((~ ((!! @ n @ (^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0))))) & $true)) = $true)),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f82])).
% 1.22/1.38 thf(f82,plain,(
% 1.22/1.38 ($true = (~ ((!! @ n @ (^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0))))) & ((c_plus @ c0 @ c0) = (c_plus @ c0 @ c0)))))),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f81])).
% 1.22/1.38 thf(f81,plain,(
% 1.22/1.38 ($true = (((!! @ n @ (^[Y0 : n]: (((c_plus @ c0 @ Y0) = (c_plus @ Y0 @ c0)) => ((c_plus @ c0 @ (cS @ Y0)) = (c_plus @ (cS @ Y0) @ c0))))) & ((c_plus @ c0 @ c0) = (c_plus @ c0 @ c0))) => $false))),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f63])).
% 1.22/1.38 thf(f63,plain,(
% 1.22/1.38 ($true = (((!! @ n @ (^[Y0 : n]: ((((^[Y1 : n]: (c_plus @ c0 @ Y1)) @ Y0) = ((^[Y1 : n]: (c_plus @ Y1 @ c0)) @ Y0)) => (((^[Y1 : n]: (c_plus @ c0 @ Y1)) @ (cS @ Y0)) = ((^[Y1 : n]: (c_plus @ Y1 @ c0)) @ (cS @ Y0)))))) & (((^[Y0 : n]: (c_plus @ c0 @ Y0)) @ c0) = ((^[Y0 : n]: (c_plus @ Y0 @ c0)) @ c0))) => $false))),
% 1.22/1.38 inference(superposition,[status(thm)],[f59,f25])).
% 1.22/1.38 thf(f25,plain,(
% 1.22/1.38 ((!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0)))) = $false)),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f24])).
% 1.22/1.38 thf(f24,plain,(
% 1.22/1.38 (($true => (!! @ n @ (^[Y0 : n]: ((c_plus @ Y0 @ c0) = (c_plus @ c0 @ Y0))))) = $false)),
% 1.22/1.38 inference(backward_demodulation,[status(thm)],[f19,f23])).
% 1.22/1.38 thf(f59,plain,(
% 1.22/1.38 ( ! [X2 : n > n,X1 : n > n] : (($true = (((!! @ n @ (^[Y0 : n]: (((X2 @ Y0) = (X1 @ Y0)) => ((X2 @ (cS @ Y0)) = (X1 @ (cS @ Y0)))))) & ((X2 @ c0) = (X1 @ c0))) => (!! @ n @ (^[Y0 : n]: ((X1 @ Y0) = (X2 @ Y0))))))) )),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f58])).
% 1.22/1.38 thf(f58,plain,(
% 1.22/1.38 ( ! [X2 : n > n,X1 : n > n] : (($true = ((^[Y0 : n > n]: (((!! @ n @ (^[Y1 : n]: (((Y0 @ Y1) = (X1 @ Y1)) => ((Y0 @ (cS @ Y1)) = (X1 @ (cS @ Y1)))))) & ((Y0 @ c0) = (X1 @ c0))) => (!! @ n @ (^[Y1 : n]: ((X1 @ Y1) = (Y0 @ Y1)))))) @ X2))) )),
% 1.22/1.38 inference(pi_clausification,[status(thm)],[f57])).
% 1.22/1.38 thf(f57,plain,(
% 1.22/1.38 ( ! [X1 : n > n] : (($true = (!! @ (n > n) @ (^[Y0 : n > n]: (((!! @ n @ (^[Y1 : n]: (((Y0 @ Y1) = (X1 @ Y1)) => ((Y0 @ (cS @ Y1)) = (X1 @ (cS @ Y1)))))) & ((Y0 @ c0) = (X1 @ c0))) => (!! @ n @ (^[Y1 : n]: ((X1 @ Y1) = (Y0 @ Y1))))))))) )),
% 1.22/1.38 inference(beta_eta_normalization,[status(thm)],[f56])).
% 1.22/1.38 thf(f56,plain,(
% 1.22/1.38 ( ! [X1 : n > n] : (($true = ((^[Y0 : n > n]: (!! @ (n > n) @ (^[Y1 : n > n]: (((!! @ n @ (^[Y2 : n]: (((Y1 @ Y2) = (Y0 @ Y2)) => ((Y1 @ (cS @ Y2)) = (Y0 @ (cS @ Y2)))))) & ((Y1 @ c0) = (Y0 @ c0))) => (!! @ n @ (^[Y2 : n]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) @ X1))) )),
% 1.22/1.38 inference(pi_clausification,[status(thm)],[f42])).
% 1.22/1.38 thf(f107,plain,(
% 1.22/1.38 (((cS @ (c_plus @ c0 @ sK3)) = (cS @ sK3)) = $false)),
% 1.22/1.38 inference(boolean_simplification,[status(thm)],[f106])).
% 1.22/1.38 thf(f106,plain,(
% 1.22/1.38 (($true => ((cS @ (c_plus @ c0 @ sK3)) = (cS @ sK3))) = $false)),
% 1.22/1.38 inference(backward_demodulation,[status(thm)],[f103,f105])).
% 1.22/1.38 % SZS output end Proof for DTF2THF_30830
% 1.22/1.38 % (30975)------------------------------
% 1.22/1.38 % (30975)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.22/1.38 % (30975)Termination reason: Refutation
% 1.22/1.38
% 1.22/1.38 % (30975)Memory used [KB]: 5756
% 1.22/1.38 % (30975)Time elapsed: 0.013 s
% 1.22/1.38 % (30975)Instructions burned: 36 (million)
% 1.22/1.38 % (30975)------------------------------
% 1.22/1.38 % (30975)------------------------------
% 1.22/1.38 % (30935)Success in time 0.326 s
%------------------------------------------------------------------------------