%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEV101^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/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:40:17 AM UTC 2026
% Result : Theorem 1.68s 1.35s
% Output : Refutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 6
% Syntax : Number of formulae : 71 ( 2 unt; 0 typ; 2 def)
% Number of atoms : 1207 ( 410 equ; 0 cnn)
% Maximal formula atoms : 12 ( 17 avg)
% Number of connectives : 1693 ( 155 ~; 242 |; 70 &;1216 @)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 724 ( 724 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 882 ( 652 ^; 194 !; 36 ?; 882 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_8,type,
sK0: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_9,type,
sK1: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_10,type,
sK2: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_11,type,
sK3: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i ).
thf(func_def_12,type,
sK4: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i ).
thf(func_def_13,type,
sK5: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_15,type,
ph7:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
sK9: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i ).
thf(func_def_22,type,
sK10: ( ( $i > $o ) > ( $i > $o ) > $i > $o ) > $i ).
thf(f400,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f146,f150,f399]) ).
thf(f399,plain,
( spl6_3
| ~ spl6_5 ),
inference(avatar_contradiction_clause,[status(thm)],[f398]) ).
thf(f398,plain,
( $false
| spl6_3
| ~ spl6_5 ),
inference(subsumption_resolution,[status(thm)],[f397,f347]) ).
thf(f347,plain,
( ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(trivial_inequality_removal,[status(thm)],[f346]) ).
thf(f346,plain,
( ( $false = $true )
| ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(duplicate_literal_removal,[status(thm)],[f345]) ).
thf(f345,plain,
( ( $false = $true )
| ( $false = $true )
| ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(beta_eta_normalization,[status(thm)],[f343]) ).
thf(f343,plain,
( ! [X10: $i,X6: $i] :
( ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) )
| spl6_3 ),
inference(primitive_instantiation,[status(thm)],[f229]) ).
thf(f229,plain,
( ! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) )
| spl6_3 ),
inference(subsumption_resolution,[status(thm)],[f215,f89]) ).
thf(f89,plain,
( ( ( ^ [Y0: $i] : $false )
!= ( ^ [Y0: $i] : $true ) )
| spl6_3 ),
inference(avatar_component_clause,[status(thm)],[f87]) ).
thf(f87,definition,
( spl6_3
<=> ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ),
introduced(definition,[new_symbols(naming,[spl6_3])],[avatar_definition]) ).
thf(f215,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f214]) ).
thf(f214,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(equality_proxy_clausification,[status(thm)],[f213]) ).
thf(f213,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f212]) ).
thf(f212,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( $true != $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f211]) ).
thf(f211,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( ( ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f204]) ).
thf(f204,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK4 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X6 )
= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(primitive_instantiation,[status(thm)],[f29]) ).
thf(f29,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) ) ),
inference(boolean_simplification,[status(thm)],[f28]) ).
thf(f28,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true ) ),
inference(boolean_simplification,[status(thm)],[f27]) ).
thf(f27,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f26]) ).
thf(f26,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f18]) ).
thf(f18,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X6: $i] :
( ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f13,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ! [X5: $i] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true ) )
& ! [X6: $i] :
( ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) ) )
& ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
& ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true ) )
| ( ( ( X1 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
& ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true ) )
| ! [X10: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5])],[f9,f12,f11,f10]) ).
thf(f10,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ? [X2: $i > $o,X3: $i > $o,X4: $i > $o] :
( ! [X5: $i] :
( ( ( X0 @ X4 @ X2 @ X5 )
= $true )
| ( ( X1 @ X4 @ X2 @ X5 )
= $true ) )
& ! [X6: $i] :
( ( $true
= ( X0 @ X2 @ X3 @ X6 ) )
| ( ( X1 @ X2 @ X3 @ X6 )
= $true ) )
& ? [X7: $i] :
( ( ( X0 @ X4 @ X3 @ X7 )
!= $true )
& ( ( X1 @ X4 @ X3 @ X7 )
!= $true ) ) )
=> ( ! [X5: $i] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true ) )
& ! [X6: $i] :
( ( $true
= ( X0 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) )
| ( $true
= ( X1 @ ( sK0 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X6 ) ) )
& ? [X7: $i] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X7 )
!= $true )
& ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X7 )
!= $true ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f11,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ? [X7: $i] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X7 )
!= $true )
& ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ X7 )
!= $true ) )
=> ( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
& ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f12,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ? [X8: $i,X9: $i > $o] :
( ( ( X1 @ X9 @ X9 @ X8 )
!= $true )
& ( $true
!= ( X0 @ X9 @ X9 @ X8 ) ) )
=> ( ( ( X1 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
& ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f9,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ? [X2: $i > $o,X3: $i > $o,X4: $i > $o] :
( ! [X5: $i] :
( ( ( X0 @ X4 @ X2 @ X5 )
= $true )
| ( ( X1 @ X4 @ X2 @ X5 )
= $true ) )
& ! [X6: $i] :
( ( $true
= ( X0 @ X2 @ X3 @ X6 ) )
| ( ( X1 @ X2 @ X3 @ X6 )
= $true ) )
& ? [X7: $i] :
( ( ( X0 @ X4 @ X3 @ X7 )
!= $true )
& ( ( X1 @ X4 @ X3 @ X7 )
!= $true ) ) )
| ? [X8: $i,X9: $i > $o] :
( ( ( X1 @ X9 @ X9 @ X8 )
!= $true )
& ( $true
!= ( X0 @ X9 @ X9 @ X8 ) ) )
| ! [X10: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ) ),
inference(rectify,[status(thm)],[f8]) ).
thf(f8,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ? [X7: $i > $o,X5: $i > $o,X6: $i > $o] :
( ! [X8: $i] :
( ( $true
= ( X0 @ X6 @ X7 @ X8 ) )
| ( ( X1 @ X6 @ X7 @ X8 )
= $true ) )
& ! [X9: $i] :
( ( ( X0 @ X7 @ X5 @ X9 )
= $true )
| ( ( X1 @ X7 @ X5 @ X9 )
= $true ) )
& ? [X10: $i] :
( ( $true
!= ( X0 @ X6 @ X5 @ X10 ) )
& ( ( X1 @ X6 @ X5 @ X10 )
!= $true ) ) )
| ? [X3: $i,X2: $i > $o] :
( ( ( X1 @ X2 @ X2 @ X3 )
!= $true )
& ( ( X0 @ X2 @ X2 @ X3 )
!= $true ) )
| ! [X4: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true ) ) ),
inference(flattening,[status(thm)],[f7]) ).
thf(f7,plain,
! [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ! [X4: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true ) )
| ? [X3: $i,X2: $i > $o] :
( ( ( X1 @ X2 @ X2 @ X3 )
!= $true )
& ( ( X0 @ X2 @ X2 @ X3 )
!= $true ) )
| ? [X7: $i > $o,X6: $i > $o,X5: $i > $o] :
( ? [X10: $i] :
( ( $true
!= ( X0 @ X6 @ X5 @ X10 ) )
& ( ( X1 @ X6 @ X5 @ X10 )
!= $true ) )
& ! [X8: $i] :
( ( $true
= ( X0 @ X6 @ X7 @ X8 ) )
| ( ( X1 @ X6 @ X7 @ X8 )
= $true ) )
& ! [X9: $i] :
( ( ( X0 @ X7 @ X5 @ X9 )
= $true )
| ( ( X1 @ X7 @ X5 @ X9 )
= $true ) ) ) ),
inference(ennf_transformation,[status(thm)],[f6]) ).
thf(f6,plain,
~ ? [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ~ ! [X4: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true ) )
& ! [X3: $i,X2: $i > $o] :
( ( ( X1 @ X2 @ X2 @ X3 )
= $true )
| ( ( X0 @ X2 @ X2 @ X3 )
= $true ) )
& ! [X7: $i > $o,X6: $i > $o,X5: $i > $o] :
( ( ! [X8: $i] :
( ( $true
= ( X0 @ X6 @ X7 @ X8 ) )
| ( ( X1 @ X6 @ X7 @ X8 )
= $true ) )
& ! [X9: $i] :
( ( ( X0 @ X7 @ X5 @ X9 )
= $true )
| ( ( X1 @ X7 @ X5 @ X9 )
= $true ) ) )
=> ! [X10: $i] :
( ( $true
= ( X0 @ X6 @ X5 @ X10 ) )
| ( ( X1 @ X6 @ X5 @ X10 )
= $true ) ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,plain,
~ ? [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ! [X3: $i,X2: $i > $o] :
( ( ( X1 @ X2 @ X2 @ X3 )
= $true )
| ( ( X0 @ X2 @ X2 @ X3 )
= $true ) )
& ~ ! [X4: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X4 )
= $true ) )
& ! [X9: $i > $o,X10: $i > $o,X11: $i > $o] :
( ( ! [X12: $i] :
( ( ( X0 @ X10 @ X11 @ X12 )
= $true )
| ( $true
= ( X1 @ X10 @ X11 @ X12 ) ) )
& ! [X13: $i] :
( ( ( X0 @ X11 @ X9 @ X13 )
= $true )
| ( $true
= ( X1 @ X11 @ X9 @ X13 ) ) ) )
=> ! [X14: $i] :
( ( $true
= ( X0 @ X10 @ X9 @ X14 ) )
| ( ( X1 @ X10 @ X9 @ X14 )
= $true ) ) ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ? [X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ! [X2: $i > $o,X3: $i] :
( ( X1 @ X2 @ X2 @ X3 )
| ( X0 @ X2 @ X2 @ X3 ) )
& ~ ! [X4: $i] :
( ( X1
@ ^ [X5: $i] :
( ~ p
| p )
@ ^ [X6: $i] :
( ~ p
& p )
@ X4 )
| ( X0
@ ^ [X7: $i] :
( ~ p
| p )
@ ^ [X8: $i] :
( ~ p
& p )
@ X4 ) )
& ! [X9: $i > $o,X10: $i > $o,X11: $i > $o] :
( ( ! [X12: $i] :
( ( X0 @ X10 @ X11 @ X12 )
| ( X1 @ X10 @ X11 @ X12 ) )
& ! [X13: $i] :
( ( X0 @ X11 @ X9 @ X13 )
| ( X1 @ X11 @ X9 @ X13 ) ) )
=> ! [X14: $i] :
( ( X0 @ X10 @ X9 @ X14 )
| ( X1 @ X10 @ X9 @ X14 ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ? [X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X0: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ! [X2: $i > $o,X3: $i] :
( ( X0 @ X2 @ X2 @ X3 )
| ( X1 @ X2 @ X2 @ X3 ) )
& ~ ! [X3: $i] :
( ( X0
@ ^ [X2: $i] :
( ~ p
| p )
@ ^ [X2: $i] :
( ~ p
& p )
@ X3 )
| ( X1
@ ^ [X2: $i] :
( ~ p
| p )
@ ^ [X2: $i] :
( ~ p
& p )
@ X3 ) )
& ! [X5: $i > $o,X2: $i > $o,X4: $i > $o] :
( ( ! [X3: $i] :
( ( X1 @ X2 @ X4 @ X3 )
| ( X0 @ X2 @ X4 @ X3 ) )
& ! [X3: $i] :
( ( X1 @ X4 @ X5 @ X3 )
| ( X0 @ X4 @ X5 @ X3 ) ) )
=> ! [X3: $i] :
( ( X1 @ X2 @ X5 @ X3 )
| ( X0 @ X2 @ X5 @ X3 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
? [X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X0: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ! [X2: $i > $o,X3: $i] :
( ( X0 @ X2 @ X2 @ X3 )
| ( X1 @ X2 @ X2 @ X3 ) )
& ~ ! [X3: $i] :
( ( X0
@ ^ [X2: $i] :
( ~ p
| p )
@ ^ [X2: $i] :
( ~ p
& p )
@ X3 )
| ( X1
@ ^ [X2: $i] :
( ~ p
| p )
@ ^ [X2: $i] :
( ~ p
& p )
@ X3 ) )
& ! [X5: $i > $o,X2: $i > $o,X4: $i > $o] :
( ( ! [X3: $i] :
( ( X1 @ X2 @ X4 @ X3 )
| ( X0 @ X2 @ X4 @ X3 ) )
& ! [X3: $i] :
( ( X1 @ X4 @ X5 @ X3 )
| ( X0 @ X4 @ X5 @ X3 ) ) )
=> ! [X3: $i] :
( ( X1 @ X2 @ X5 @ X3 )
| ( X0 @ X2 @ X5 @ X3 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.Q5zG9NLuw3/DTF2THF_17785.p',cTHM120E_pme) ).
thf(f397,plain,
( ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3
| ~ spl6_5 ),
inference(trivial_inequality_removal,[status(thm)],[f396]) ).
thf(f396,plain,
( ( $false = $true )
| ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3
| ~ spl6_5 ),
inference(beta_eta_normalization,[status(thm)],[f391]) ).
thf(f391,plain,
( ! [X0: $i] :
( ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X0 )
= $true )
| ( ( sK1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) )
| spl6_3
| ~ spl6_5 ),
inference(superposition,[status(thm)],[f149,f381]) ).
thf(f381,plain,
( ( ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(trivial_inequality_removal,[status(thm)],[f380]) ).
thf(f380,plain,
( ( $false = $true )
| ( ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(duplicate_literal_removal,[status(thm)],[f379]) ).
thf(f379,plain,
( ( $false = $true )
| ( $false = $true )
| ( ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| spl6_3 ),
inference(beta_eta_normalization,[status(thm)],[f371]) ).
thf(f371,plain,
( ! [X10: $i,X5: $i] :
( ( ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ( sK2
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : $false
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 ) ) )
| spl6_3 ),
inference(primitive_instantiation,[status(thm)],[f258]) ).
thf(f258,plain,
( ! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) )
| spl6_3 ),
inference(subsumption_resolution,[status(thm)],[f244,f89]) ).
thf(f244,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true )
| ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f243]) ).
thf(f243,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true ) ),
inference(equality_proxy_clausification,[status(thm)],[f242]) ).
thf(f242,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f241]) ).
thf(f241,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( $true != $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f240]) ).
thf(f240,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true )
| ( ( ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
= $true )
| ( ( ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f233]) ).
thf(f233,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK4 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK0 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ X5 )
= $true ) ),
inference(primitive_instantiation,[status(thm)],[f41]) ).
thf(f41,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f40]) ).
thf(f40,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) ) ),
inference(boolean_simplification,[status(thm)],[f39]) ).
thf(f39,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f38]) ).
thf(f38,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true ) ),
inference(boolean_simplification,[status(thm)],[f20]) ).
thf(f20,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X5: $i] :
( ( ( X1 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK0 @ X1 @ X0 ) @ X5 )
= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f149,plain,
( ! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) )
| ~ spl6_5 ),
inference(avatar_component_clause,[status(thm)],[f148]) ).
thf(f148,definition,
( spl6_5
<=> ! [X1: ( $i > $o ) > ( $i > $o ) > $i > $o,X10: $i] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl6_5])],[avatar_definition]) ).
thf(f150,plain,
( spl6_3
| spl6_5 ),
inference(avatar_split_clause,[status(thm)],[f134,f148,f87]) ).
thf(f134,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) )
| ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
!= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f133]) ).
thf(f133,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( $true
!= ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f132]) ).
thf(f132,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( $true
!= ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f131]) ).
thf(f131,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( $true != $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
!= ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ) ),
inference(boolean_simplification,[status(thm)],[f130]) ).
thf(f130,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( $true
= ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) ) )
| ( ( ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( $true
!= ( ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
= ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f116]) ).
thf(f116,plain,
! [X10: $i,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK2 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK1 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK3 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK5 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) )
@ ( sK4 @ X1
@ ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] : ( Y1 = Y0 ) ) )
!= $true ) ),
inference(primitive_instantiation,[status(thm)],[f45]) ).
thf(f45,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f44]) ).
thf(f44,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( $true
= ( X0
@ ^ [Y0: $i] : $true
@ ^ [Y0: $i] : $false
@ X10 ) )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f43]) ).
thf(f43,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f42]) ).
thf(f42,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] : $false
@ X10 )
= $true ) ),
inference(boolean_simplification,[status(thm)],[f16]) ).
thf(f16,plain,
! [X10: $i,X0: ( $i > $o ) > ( $i > $o ) > $i > $o,X1: ( $i > $o ) > ( $i > $o ) > $i > $o] :
( ( ( X0
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true )
| ( ( X0 @ ( sK2 @ X1 @ X0 ) @ ( sK1 @ X1 @ X0 ) @ ( sK3 @ X1 @ X0 ) )
!= $true )
| ( ( X0 @ ( sK5 @ X1 @ X0 ) @ ( sK5 @ X1 @ X0 ) @ ( sK4 @ X1 @ X0 ) )
!= $true )
| ( ( X1
@ ^ [Y0: $i] :
( p
| ~ p )
@ ^ [Y0: $i] :
( p
& ~ p )
@ X10 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f146,plain,
~ spl6_3,
inference(avatar_contradiction_clause,[status(thm)],[f145]) ).
thf(f145,plain,
( $false
| ~ spl6_3 ),
inference(trivial_inequality_removal,[status(thm)],[f144]) ).
thf(f144,plain,
( ( $false = $true )
| ~ spl6_3 ),
inference(beta_eta_normalization,[status(thm)],[f143]) ).
thf(f143,plain,
( ! [X1: $i] :
( ( ^ [Y0: $i] : $false
@ X1 )
= ( ^ [Y0: $i] : $true
@ X1 ) )
| ~ spl6_3 ),
inference(argument_congruence,[status(thm)],[f88]) ).
thf(f88,plain,
( ( ( ^ [Y0: $i] : $false )
= ( ^ [Y0: $i] : $true ) )
| ~ spl6_3 ),
inference(avatar_component_clause,[status(thm)],[f87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV101^5 : TPTP v9.2.1. Released v4.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.34 % Computer : n022.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue Feb 24 12:40:06 EST 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.32/0.47 ---- Original DTF file ---
% 0.32/0.47 thf(spec,logic,$$dhol).
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 % File : SEV101^5 : TPTP v9.2.1. Released v4.0.0.
% 0.32/0.47 % Domain : Set Theory (Relations)
% 0.32/0.47 % Problem : TPS problem from RELN-THMS
% 0.32/0.47 % Version : Especial.
% 0.32/0.47 % English :
% 0.32/0.47
% 0.32/0.47 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.32/0.47 % Source : [Bro09]
% 0.32/0.47 % Names : tps_1089 [Bro09]
% 0.32/0.47
% 0.32/0.47 % Status : Theorem
% 0.32/0.47 % Rating : 0.50 v9.0.0, 0.58 v8.2.0, 0.64 v8.1.0, 0.83 v7.4.0, 0.78 v7.3.0, 0.80 v7.2.0, 0.75 v7.1.0, 0.71 v7.0.0, 0.75 v6.4.0, 0.71 v6.3.0, 0.83 v5.5.0, 0.80 v5.4.0, 0.75 v5.2.0, 1.00 v4.0.0
% 0.32/0.47 % Syntax : Number of formulae : 2 ( 0 unt; 1 typ; 0 def)
% 0.32/0.47 % Number of atoms : 8 ( 0 equ; 0 cnn)
% 0.32/0.47 % Maximal formula atoms : 8 ( 8 avg)
% 0.32/0.47 % Number of connectives : 48 ( 5 ~; 7 |; 5 &; 30 @)
% 0.32/0.47 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.32/0.47 % Maximal formula depth : 15 ( 15 avg)
% 0.32/0.47 % Number of types : 2 ( 0 usr)
% 0.32/0.47 % Number of type conns : 14 ( 14 >; 0 *; 0 +; 0 <<)
% 0.32/0.47 % Number of symbols : 1 ( 1 usr; 1 con; 0-0 aty)
% 0.32/0.47 % Number of variables : 15 ( 4 ^; 9 !; 2 ?; 15 :)
% 0.32/0.47 % SPC : TH0_THM_NEQ_NAR
% 0.32/0.47
% 0.32/0.47 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.32/0.47 % project in the Department of Mathematical Sciences at Carnegie
% 0.32/0.47 % Mellon University. Distributed under the Creative Commons copyleft
% 0.32/0.47 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 thf(p,type,
% 0.32/0.47 p: $o ).
% 0.32/0.47
% 0.32/0.47 thf(cTHM120E_pme,conjecture,
% 0.32/0.47 ? [Xr_28: ( $i > $o ) > ( $i > $o ) > $i > $o,Xr_27: ( $i > $o ) > ( $i > $o ) > $i > $o] :
% 0.32/0.47 ( ! [Xx: $i > $o,Xw_2: $i] :
% 0.32/0.47 ( ( Xr_27 @ Xx @ Xx @ Xw_2 )
% 0.32/0.47 | ( Xr_28 @ Xx @ Xx @ Xw_2 ) )
% 0.32/0.47 & ! [Xx: $i > $o,Xy: $i > $o,Xz: $i > $o] :
% 0.32/0.47 ( ( ! [Xw_2: $i] :
% 0.32/0.47 ( ( Xr_27 @ Xx @ Xy @ Xw_2 )
% 0.32/0.47 | ( Xr_28 @ Xx @ Xy @ Xw_2 ) )
% 0.32/0.47 & ! [Xw_2: $i] :
% 0.32/0.47 ( ( Xr_27 @ Xy @ Xz @ Xw_2 )
% 0.32/0.47 | ( Xr_28 @ Xy @ Xz @ Xw_2 ) ) )
% 0.32/0.47 => ! [Xw_2: $i] :
% 0.32/0.47 ( ( Xr_27 @ Xx @ Xz @ Xw_2 )
% 0.32/0.47 | ( Xr_28 @ Xx @ Xz @ Xw_2 ) ) )
% 0.32/0.47 & ~ ! [Xw_2: $i] :
% 0.32/0.47 ( ( Xr_27
% 0.32/0.47 @ ^ [Xx: $i] :
% 0.32/0.47 ( p
% 0.32/0.47 | ~ p )
% 0.32/0.47 @ ^ [Xx: $i] :
% 0.32/0.47 ( p
% 0.32/0.47 & ~ p )
% 0.32/0.47 @ Xw_2 )
% 0.32/0.47 | ( Xr_28
% 0.32/0.47 @ ^ [Xx: $i] :
% 0.32/0.47 ( p
% 0.32/0.47 | ~ p )
% 0.32/0.47 @ ^ [Xx: $i] :
% 0.32/0.47 ( p
% 0.32/0.47 & ~ p )
% 0.32/0.47 @ Xw_2 ) ) ) ).
% 0.32/0.47
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 ------------------------
% 1.52/1.27 ---- Embedded in THF ---
% 1.52/1.27 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.52/1.27 %%% Generated on Tue Feb 24 12:40:07 EST 2026
% 1.52/1.27 %%% using '$$dhol' embedding, version 1.3.0.
% 1.52/1.27 %%% Logic specification used:
% 1.52/1.27 %%% thf(spec, logic, $$dhol).
% 1.52/1.27
% 1.52/1.27 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.Q5zG9NLuw3/DTF2DTF17785.p
% See solution above
% 1.52/1.27 ------------------------
% 1.52/1.28 ---- Cleaned THF ---
% 1.52/1.28 thf(p,type,
% 1.52/1.28 p: $o ).
% 1.52/1.28
% 1.52/1.28 thf(cTHM120E_pme,conjecture,
% 1.52/1.28 ? [Xr_28: ( $i > $o ) > ( $i > $o ) > $i > $o,Xr_27: ( $i > $o ) > ( $i > $o ) > $i > $o] :
% 1.52/1.28 ( ! [Xx: $i > $o,Xw_2: $i] :
% 1.52/1.28 ( ( Xr_27 @ Xx @ Xx @ Xw_2 )
% 1.52/1.28 | ( Xr_28 @ Xx @ Xx @ Xw_2 ) )
% 1.52/1.28 & ! [Xx: $i > $o,Xy: $i > $o,Xz: $i > $o] :
% 1.52/1.28 ( ( ! [Xw_2: $i] :
% 1.52/1.28 ( ( Xr_27 @ Xx @ Xy @ Xw_2 )
% 1.52/1.28 | ( Xr_28 @ Xx @ Xy @ Xw_2 ) )
% 1.52/1.28 & ! [Xw_2: $i] :
% 1.52/1.28 ( ( Xr_27 @ Xy @ Xz @ Xw_2 )
% 1.52/1.28 | ( Xr_28 @ Xy @ Xz @ Xw_2 ) ) )
% 1.52/1.28 => ! [Xw_2: $i] :
% 1.52/1.28 ( ( Xr_27 @ Xx @ Xz @ Xw_2 )
% 1.52/1.28 | ( Xr_28 @ Xx @ Xz @ Xw_2 ) ) )
% 1.52/1.28 & ~ ! [Xw_2: $i] :
% 1.52/1.28 ( ( Xr_27
% 1.52/1.28 @ ^ [Xx: $i] :
% 1.52/1.28 ( p
% 1.52/1.28 | ~ p )
% 1.52/1.28 @ ^ [Xx: $i] :
% 1.52/1.28 ( p
% 1.52/1.28 & ~ p )
% 1.52/1.28 @ Xw_2 )
% 1.52/1.28 | ( Xr_28
% 1.52/1.28 @ ^ [Xx: $i] :
% 1.52/1.28 ( p
% 1.52/1.28 | ~ p )
% 1.52/1.28 @ ^ [Xx: $i] :
% 1.52/1.28 ( p
% 1.52/1.28 & ~ p )
% 1.52/1.28 @ Xw_2 ) ) ) ).
% 1.52/1.28 ------------------------
% 1.52/1.29 % (18119)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_17785 for (3000ds/18Mi)
% 1.68/1.30 % (18113)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_17785 for (3000ds/183Mi)
% 1.68/1.30 % (18119)Instruction limit reached!
% 1.68/1.30 % (18119)------------------------------
% 1.68/1.30 % (18119)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.30 % (18119)Termination reason: Unknown
% 1.68/1.30 % (18119)Termination phase: Saturation
% 1.68/1.30
% 1.68/1.30 % (18119)Memory used [KB]: 5628
% 1.68/1.30 % (18119)Time elapsed: 0.008 s
% 1.68/1.30 % (18119)Instructions burned: 20 (million)
% 1.68/1.30 % (18119)------------------------------
% 1.68/1.30 % (18119)------------------------------
% 1.68/1.30 % (18114)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_17785 for (3000ds/4Mi)
% 1.68/1.30 % (18116)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_17785 for (3000ds/2Mi)
% 1.68/1.30 % (18115)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_17785 for (3000ds/27Mi)
% 1.68/1.30 % (18118)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_17785 for (3000ds/275Mi)
% 1.68/1.30 % (18117)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_17785 for (3000ds/2Mi)
% 1.68/1.30 % (18116)Instruction limit reached!
% 1.68/1.30 % (18116)------------------------------
% 1.68/1.30 % (18116)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.30 % (18116)Termination reason: Unknown
% 1.68/1.30 % (18116)Termination phase: Property scanning
% 1.68/1.30
% 1.68/1.30 % (18116)Memory used [KB]: 895
% 1.68/1.30 % (18116)Time elapsed: 0.003 s
% 1.68/1.30 % (18116)Instructions burned: 2 (million)
% 1.68/1.30 % (18116)------------------------------
% 1.68/1.30 % (18116)------------------------------
% 1.68/1.30 % (18117)Instruction limit reached!
% 1.68/1.30 % (18117)------------------------------
% 1.68/1.30 % (18117)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.30 % (18117)Termination reason: Unknown
% 1.68/1.30 % (18117)Termination phase: Saturation
% 1.68/1.30
% 1.68/1.30 % (18117)Memory used [KB]: 1023
% 1.68/1.30 % (18117)Time elapsed: 0.003 s
% 1.68/1.30 % (18117)Instructions burned: 3 (million)
% 1.68/1.30 % (18117)------------------------------
% 1.68/1.30 % (18117)------------------------------
% 1.68/1.30 % (18114)Instruction limit reached!
% 1.68/1.30 % (18114)------------------------------
% 1.68/1.30 % (18114)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.30 % (18114)Termination reason: Unknown
% 1.68/1.30 % (18114)Termination phase: Saturation
% 1.68/1.30
% 1.68/1.30 % (18114)Memory used [KB]: 5500
% 1.68/1.30 % (18114)Time elapsed: 0.005 s
% 1.68/1.30 % (18114)Instructions burned: 5 (million)
% 1.68/1.30 % (18114)------------------------------
% 1.68/1.30 % (18114)------------------------------
% 1.68/1.31 % (18115)Refutation not found, incomplete strategy
% 1.68/1.31 % (18115)------------------------------
% 1.68/1.31 % (18115)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.31 % (18115)Termination reason: Refutation not found, incomplete strategy
% 1.68/1.31
% 1.68/1.31
% 1.68/1.31 % (18115)Memory used [KB]: 5500
% 1.68/1.31 % (18115)Time elapsed: 0.008 s
% 1.68/1.31 % (18115)Instructions burned: 10 (million)
% 1.68/1.31 % (18115)------------------------------
% 1.68/1.31 % (18115)------------------------------
% 1.68/1.31 % (18120)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_17785 for (2999ds/3Mi)
% 1.68/1.31 % (18120)Instruction limit reached!
% 1.68/1.31 % (18120)------------------------------
% 1.68/1.31 % (18120)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.31 % (18120)Termination reason: Unknown
% 1.68/1.31 % (18120)Termination phase: Saturation
% 1.68/1.31
% 1.68/1.31 % (18120)Memory used [KB]: 5500
% 1.68/1.31 % (18120)Time elapsed: 0.003 s
% 1.68/1.31 % (18120)Instructions burned: 4 (million)
% 1.68/1.31 % (18120)------------------------------
% 1.68/1.31 % (18120)------------------------------
% 1.68/1.32 % (18121)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_17785 for (2999ds/37Mi)
% 1.68/1.32 % (18122)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_17785 for (2999ds/15Mi)
% 1.68/1.32 % (18123)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_17785 for (2999ds/3Mi)
% 1.68/1.32 % (18125)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_17785 for (2999ds/7Mi)
% 1.68/1.32 % (18123)Instruction limit reached!
% 1.68/1.32 % (18123)------------------------------
% 1.68/1.32 % (18123)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.32 % (18123)Termination reason: Unknown
% 1.68/1.32 % (18123)Termination phase: Saturation
% 1.68/1.32
% 1.68/1.32 % (18123)Memory used [KB]: 1023
% 1.68/1.32 % (18123)Time elapsed: 0.004 s
% 1.68/1.32 % (18123)Instructions burned: 4 (million)
% 1.68/1.32 % (18123)------------------------------
% 1.68/1.32 % (18123)------------------------------
% 1.68/1.32 % (18125)Instruction limit reached!
% 1.68/1.32 % (18125)------------------------------
% 1.68/1.32 % (18125)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.32 % (18125)Termination reason: Unknown
% 1.68/1.32 % (18125)Termination phase: Saturation
% 1.68/1.32
% 1.68/1.32 % (18125)Memory used [KB]: 1023
% 1.68/1.32 % (18125)Time elapsed: 0.004 s
% 1.68/1.32 % (18125)Instructions burned: 7 (million)
% 1.68/1.32 % (18125)------------------------------
% 1.68/1.32 % (18125)------------------------------
% 1.68/1.32 % (18124)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_17785 for (2999ds/1041Mi)
% 1.68/1.33 % (18122)Instruction limit reached!
% 1.68/1.33 % (18122)------------------------------
% 1.68/1.33 % (18122)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.33 % (18122)Termination reason: Unknown
% 1.68/1.33 % (18122)Termination phase: Saturation
% 1.68/1.33
% 1.68/1.33 % (18122)Memory used [KB]: 5628
% 1.68/1.33 % (18122)Time elapsed: 0.011 s
% 1.68/1.33 % (18122)Instructions burned: 15 (million)
% 1.68/1.33 % (18122)------------------------------
% 1.68/1.33 % (18122)------------------------------
% 1.68/1.33 % (18127)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_17785 for (2999ds/3Mi)
% 1.68/1.34 % (18121)Instruction limit reached!
% 1.68/1.34 % (18121)------------------------------
% 1.68/1.34 % (18121)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.34 % (18121)Termination reason: Unknown
% 1.68/1.34 % (18121)Termination phase: Saturation
% 1.68/1.34
% 1.68/1.34 % (18121)Memory used [KB]: 5756
% 1.68/1.34 % (18121)Time elapsed: 0.018 s
% 1.68/1.34 % (18121)Instructions burned: 39 (million)
% 1.68/1.34 % (18121)------------------------------
% 1.68/1.34 % (18121)------------------------------
% 1.68/1.34 % (18127)Instruction limit reached!
% 1.68/1.34 % (18127)------------------------------
% 1.68/1.34 % (18127)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.34 % (18127)Termination reason: Unknown
% 1.68/1.34 % (18127)Termination phase: Twee Goal Transformation
% 1.68/1.34
% 1.68/1.34 % (18127)Memory used [KB]: 1023
% 1.68/1.34 % (18127)Time elapsed: 0.003 s
% 1.68/1.34 % (18127)Instructions burned: 4 (million)
% 1.68/1.34 % (18127)------------------------------
% 1.68/1.34 % (18127)------------------------------
% 1.68/1.34 % (18126)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_17785 for (2999ds/16Mi)
% 1.68/1.34 % (18118)First to succeed.
% 1.68/1.35 % (18130)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_17785 for (2999ds/3Mi)
% 1.68/1.35 % (18129)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_17785 for (2999ds/7Mi)
% 1.68/1.35 % (18128)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_17785 for (2999ds/3Mi)
% 1.68/1.35 % (18130)Instruction limit reached!
% 1.68/1.35 % (18130)------------------------------
% 1.68/1.35 % (18130)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (18130)Termination reason: Unknown
% 1.68/1.35 % (18130)Termination phase: Saturation
% 1.68/1.35
% 1.68/1.35 % (18130)Memory used [KB]: 5500
% 1.68/1.35 % (18130)Time elapsed: 0.003 s
% 1.68/1.35 % (18130)Instructions burned: 4 (million)
% 1.68/1.35 % (18130)------------------------------
% 1.68/1.35 % (18130)------------------------------
% 1.68/1.35 % (18126)Instruction limit reached!
% 1.68/1.35 % (18126)------------------------------
% 1.68/1.35 % (18126)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (18126)Termination reason: Unknown
% 1.68/1.35 % (18126)Termination phase: Saturation
% 1.68/1.35
% 1.68/1.35 % (18126)Memory used [KB]: 5628
% 1.68/1.35 % (18126)Time elapsed: 0.010 s
% 1.68/1.35 % (18126)Instructions burned: 16 (million)
% 1.68/1.35 % (18126)------------------------------
% 1.68/1.35 % (18126)------------------------------
% 1.68/1.35 % (18129)Instruction limit reached!
% 1.68/1.35 % (18129)------------------------------
% 1.68/1.35 % (18129)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (18129)Termination reason: Unknown
% 1.68/1.35 % (18129)Termination phase: Saturation
% 1.68/1.35
% 1.68/1.35 % (18129)Memory used [KB]: 5500
% 1.68/1.35 % (18129)Time elapsed: 0.004 s
% 1.68/1.35 % (18129)Instructions burned: 8 (million)
% 1.68/1.35 % (18129)------------------------------
% 1.68/1.35 % (18129)------------------------------
% 1.68/1.35 % (18128)Instruction limit reached!
% 1.68/1.35 % (18128)------------------------------
% 1.68/1.35 % (18128)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (18128)Termination reason: Unknown
% 1.68/1.35 % (18128)Termination phase: Property scanning
% 1.68/1.35
% 1.68/1.35 % (18128)Memory used [KB]: 1023
% 1.68/1.35 % (18128)Time elapsed: 0.004 s
% 1.68/1.35 % (18128)Instructions burned: 4 (million)
% 1.68/1.35 % (18128)------------------------------
% 1.68/1.35 % (18128)------------------------------
% 1.68/1.35 % (18118)Refutation found. Thanks to Tanya!
% 1.68/1.35 % SZS status Theorem for DTF2THF_17785
% 1.68/1.35 % SZS output start Proof for DTF2THF_17785
% 1.68/1.35 thf(func_def_8, type, sK0: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o).
% 1.68/1.35 thf(func_def_9, type, sK1: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o).
% 1.68/1.35 thf(func_def_10, type, sK2: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o).
% 1.68/1.35 thf(func_def_11, type, sK3: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i).
% 1.68/1.35 thf(func_def_12, type, sK4: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i).
% 1.68/1.35 thf(func_def_13, type, sK5: (($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o).
% 1.68/1.35 thf(func_def_15, type, ph7: !>[X0: $tType]:(X0)).
% 1.68/1.35 thf(func_def_21, type, sK9: (($i > $o) > ($i > $o) > $i > $o) > $i).
% 1.68/1.35 thf(func_def_22, type, sK10: (($i > $o) > ($i > $o) > $i > $o) > $i).
% 1.68/1.35 thf(f400,plain,(
% 1.68/1.35 $false),
% 1.68/1.35 inference(avatar_sat_refutation,[status(thm)],[f146,f150,f399])).
% 1.68/1.35 thf(f399,plain,(
% 1.68/1.35 spl6_3 | ~spl6_5),
% 1.68/1.35 inference(avatar_contradiction_clause,[status(thm)],[f398])).
% 1.68/1.35 thf(f398,plain,(
% 1.68/1.35 $false | (spl6_3 | ~spl6_5)),
% 1.68/1.35 inference(subsumption_resolution,[status(thm)],[f397,f347])).
% 1.68/1.35 thf(f347,plain,(
% 1.68/1.35 ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f346])).
% 1.68/1.35 thf(f346,plain,(
% 1.68/1.35 ($false = $true) | ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(duplicate_literal_removal,[status(thm)],[f345])).
% 1.68/1.35 thf(f345,plain,(
% 1.68/1.35 ($false = $true) | ($false = $true) | ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f343])).
% 1.68/1.35 thf(f343,plain,(
% 1.68/1.35 ( ! [X10 : $i,X6 : $i] : ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) ) | spl6_3),
% 1.68/1.35 inference(primitive_instantiation,[status(thm)],[f229])).
% 1.68/1.35 thf(f229,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) ) | spl6_3),
% 1.68/1.35 inference(subsumption_resolution,[status(thm)],[f215,f89])).
% 1.68/1.35 thf(f89,plain,(
% 1.68/1.35 ((^[Y0 : $i]: ($false)) != (^[Y0 : $i]: ($true))) | spl6_3),
% 1.68/1.35 inference(avatar_component_clause,[status(thm)],[f87])).
% 1.68/1.35 thf(f87,definition,(
% 1.68/1.35 spl6_3 <=> ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))),
% 1.68/1.35 introduced(definition,[new_symbols(naming,[spl6_3])],[avatar_definition])).
% 1.68/1.35 thf(f215,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f214])).
% 1.68/1.35 thf(f214,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f213])).
% 1.68/1.35 thf(f213,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | (((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))))) )),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f212])).
% 1.68/1.35 thf(f212,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | (((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ($true != $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f211])).
% 1.68/1.35 thf(f211,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | (((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | (((sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true)) )),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f204])).
% 1.68/1.35 thf(f204,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK4 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X6) = $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(primitive_instantiation,[status(thm)],[f29])).
% 1.68/1.35 thf(f29,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6))) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f28])).
% 1.68/1.35 thf(f28,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f27])).
% 1.68/1.35 thf(f27,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f26])).
% 1.68/1.35 thf(f26,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f18])).
% 1.68/1.35 thf(f18,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X6 : $i] : (($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)) )),
% 1.68/1.35 inference(cnf_transformation,[status(thm)],[f13])).
% 1.68/1.35 thf(f13,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : ((! [X5 : $i] : (((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true)) & ! [X6 : $i] : (($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6))) & (((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) & ((X1 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true))) | (((X1 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) & ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true)) | ! [X10 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)))),
% 1.68/1.35 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5])],[f9,f12,f11,f10])).
% 1.68/1.35 thf(f10,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (? [X2 : $i > $o,X3 : $i > $o,X4 : $i > $o] : (! [X5 : $i] : (((X0 @ X4 @ X2 @ X5) = $true) | ((X1 @ X4 @ X2 @ X5) = $true)) & ! [X6 : $i] : (($true = (X0 @ X2 @ X3 @ X6)) | ((X1 @ X2 @ X3 @ X6) = $true)) & ? [X7 : $i] : (((X0 @ X4 @ X3 @ X7) != $true) & ((X1 @ X4 @ X3 @ X7) != $true))) => (! [X5 : $i] : (((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true)) & ! [X6 : $i] : (($true = (X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6)) | ($true = (X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X6))) & ? [X7 : $i] : (((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7) != $true) & ((X1 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7) != $true))))),
% 1.68/1.35 introduced(definition,[],[choice_axiom])).
% 1.68/1.35 thf(f11,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (? [X7 : $i] : (((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7) != $true) & ((X1 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7) != $true)) => (((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) & ((X1 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true)))),
% 1.68/1.35 introduced(definition,[],[choice_axiom])).
% 1.68/1.35 thf(f12,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (? [X8 : $i,X9 : $i > $o] : (((X1 @ X9 @ X9 @ X8) != $true) & ($true != (X0 @ X9 @ X9 @ X8))) => (((X1 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) & ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true)))),
% 1.68/1.35 introduced(definition,[],[choice_axiom])).
% 1.68/1.35 thf(f9,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (? [X2 : $i > $o,X3 : $i > $o,X4 : $i > $o] : (! [X5 : $i] : (((X0 @ X4 @ X2 @ X5) = $true) | ((X1 @ X4 @ X2 @ X5) = $true)) & ! [X6 : $i] : (($true = (X0 @ X2 @ X3 @ X6)) | ((X1 @ X2 @ X3 @ X6) = $true)) & ? [X7 : $i] : (((X0 @ X4 @ X3 @ X7) != $true) & ((X1 @ X4 @ X3 @ X7) != $true))) | ? [X8 : $i,X9 : $i > $o] : (((X1 @ X9 @ X9 @ X8) != $true) & ($true != (X0 @ X9 @ X9 @ X8))) | ! [X10 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)))),
% 1.68/1.35 inference(rectify,[status(thm)],[f8])).
% 1.68/1.35 thf(f8,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (? [X7 : $i > $o,X5 : $i > $o,X6 : $i > $o] : (! [X8 : $i] : (($true = (X0 @ X6 @ X7 @ X8)) | ((X1 @ X6 @ X7 @ X8) = $true)) & ! [X9 : $i] : (((X0 @ X7 @ X5 @ X9) = $true) | ((X1 @ X7 @ X5 @ X9) = $true)) & ? [X10 : $i] : (($true != (X0 @ X6 @ X5 @ X10)) & ((X1 @ X6 @ X5 @ X10) != $true))) | ? [X3 : $i,X2 : $i > $o] : (((X1 @ X2 @ X2 @ X3) != $true) & ((X0 @ X2 @ X2 @ X3) != $true)) | ! [X4 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true)))),
% 1.68/1.35 inference(flattening,[status(thm)],[f7])).
% 1.68/1.35 thf(f7,plain,(
% 1.68/1.35 ! [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (! [X4 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true)) | ? [X3 : $i,X2 : $i > $o] : (((X1 @ X2 @ X2 @ X3) != $true) & ((X0 @ X2 @ X2 @ X3) != $true)) | ? [X7 : $i > $o,X6 : $i > $o,X5 : $i > $o] : (? [X10 : $i] : (($true != (X0 @ X6 @ X5 @ X10)) & ((X1 @ X6 @ X5 @ X10) != $true)) & (! [X8 : $i] : (($true = (X0 @ X6 @ X7 @ X8)) | ((X1 @ X6 @ X7 @ X8) = $true)) & ! [X9 : $i] : (((X0 @ X7 @ X5 @ X9) = $true) | ((X1 @ X7 @ X5 @ X9) = $true)))))),
% 1.68/1.35 inference(ennf_transformation,[status(thm)],[f6])).
% 1.68/1.35 thf(f6,plain,(
% 1.68/1.35 ~? [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (~! [X4 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true)) & ! [X3 : $i,X2 : $i > $o] : (((X1 @ X2 @ X2 @ X3) = $true) | ((X0 @ X2 @ X2 @ X3) = $true)) & ! [X7 : $i > $o,X6 : $i > $o,X5 : $i > $o] : ((! [X8 : $i] : (($true = (X0 @ X6 @ X7 @ X8)) | ((X1 @ X6 @ X7 @ X8) = $true)) & ! [X9 : $i] : (((X0 @ X7 @ X5 @ X9) = $true) | ((X1 @ X7 @ X5 @ X9) = $true))) => ! [X10 : $i] : (($true = (X0 @ X6 @ X5 @ X10)) | ((X1 @ X6 @ X5 @ X10) = $true))))),
% 1.68/1.35 inference(rectify,[status(thm)],[f5])).
% 1.68/1.35 thf(f5,plain,(
% 1.68/1.35 ~? [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (! [X3 : $i,X2 : $i > $o] : (((X1 @ X2 @ X2 @ X3) = $true) | ((X0 @ X2 @ X2 @ X3) = $true)) & ~! [X4 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X4) = $true)) & ! [X9 : $i > $o,X10 : $i > $o,X11 : $i > $o] : ((! [X12 : $i] : (((X0 @ X10 @ X11 @ X12) = $true) | ($true = (X1 @ X10 @ X11 @ X12))) & ! [X13 : $i] : (((X0 @ X11 @ X9 @ X13) = $true) | ($true = (X1 @ X11 @ X9 @ X13)))) => ! [X14 : $i] : (($true = (X0 @ X10 @ X9 @ X14)) | ((X1 @ X10 @ X9 @ X14) = $true))))),
% 1.68/1.35 inference(fool_elimination,[status(thm)],[f4])).
% 1.68/1.35 thf(f4,plain,(
% 1.68/1.35 ~? [X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (! [X2 : $i > $o,X3 : $i] : ((X1 @ X2 @ X2 @ X3) | (X0 @ X2 @ X2 @ X3)) & ~! [X4 : $i] : ((X1 @ (^[X5 : $i] : (~p | p)) @ (^[X6 : $i] : (~p & p)) @ X4) | (X0 @ (^[X7 : $i] : (~p | p)) @ (^[X8 : $i] : (~p & p)) @ X4)) & ! [X9 : $i > $o,X10 : $i > $o,X11 : $i > $o] : ((! [X12 : $i] : ((X0 @ X10 @ X11 @ X12) | (X1 @ X10 @ X11 @ X12)) & ! [X13 : $i] : ((X0 @ X11 @ X9 @ X13) | (X1 @ X11 @ X9 @ X13))) => ! [X14 : $i] : ((X0 @ X10 @ X9 @ X14) | (X1 @ X10 @ X9 @ X14))))),
% 1.68/1.35 inference(rectify,[status(thm)],[f2])).
% 1.68/1.35 thf(f2,negated_conjecture,(
% 1.68/1.35 ~? [X1 : ($i > $o) > ($i > $o) > $i > $o,X0 : ($i > $o) > ($i > $o) > $i > $o] : (! [X2 : $i > $o,X3 : $i] : ((X0 @ X2 @ X2 @ X3) | (X1 @ X2 @ X2 @ X3)) & ~! [X3 : $i] : ((X0 @ (^[X2 : $i] : (~p | p)) @ (^[X2 : $i] : (~p & p)) @ X3) | (X1 @ (^[X2 : $i] : (~p | p)) @ (^[X2 : $i] : (~p & p)) @ X3)) & ! [X5 : $i > $o,X2 : $i > $o,X4 : $i > $o] : ((! [X3 : $i] : ((X1 @ X2 @ X4 @ X3) | (X0 @ X2 @ X4 @ X3)) & ! [X3 : $i] : ((X1 @ X4 @ X5 @ X3) | (X0 @ X4 @ X5 @ X3))) => ! [X3 : $i] : ((X1 @ X2 @ X5 @ X3) | (X0 @ X2 @ X5 @ X3))))),
% 1.68/1.35 inference(negated_conjecture,[status(cth)],[f1])).
% 1.68/1.35 thf(f1,conjecture,(
% 1.68/1.35 ? [X1 : ($i > $o) > ($i > $o) > $i > $o,X0 : ($i > $o) > ($i > $o) > $i > $o] : (! [X2 : $i > $o,X3 : $i] : ((X0 @ X2 @ X2 @ X3) | (X1 @ X2 @ X2 @ X3)) & ~! [X3 : $i] : ((X0 @ (^[X2 : $i] : (~p | p)) @ (^[X2 : $i] : (~p & p)) @ X3) | (X1 @ (^[X2 : $i] : (~p | p)) @ (^[X2 : $i] : (~p & p)) @ X3)) & ! [X5 : $i > $o,X2 : $i > $o,X4 : $i > $o] : ((! [X3 : $i] : ((X1 @ X2 @ X4 @ X3) | (X0 @ X2 @ X4 @ X3)) & ! [X3 : $i] : ((X1 @ X4 @ X5 @ X3) | (X0 @ X4 @ X5 @ X3))) => ! [X3 : $i] : ((X1 @ X2 @ X5 @ X3) | (X0 @ X2 @ X5 @ X3))))),
% 1.68/1.35 file('/export/starexec/sandbox/tmp/tmp.Q5zG9NLuw3/DTF2THF_17785.p',cTHM120E_pme)).
% 1.68/1.35 thf(f397,plain,(
% 1.68/1.35 ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | (spl6_3 | ~spl6_5)),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f396])).
% 1.68/1.35 thf(f396,plain,(
% 1.68/1.35 ($false = $true) | ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | (spl6_3 | ~spl6_5)),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f391])).
% 1.68/1.35 thf(f391,plain,(
% 1.68/1.35 ( ! [X0 : $i] : ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X0) = $true) | ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) ) | (spl6_3 | ~spl6_5)),
% 1.68/1.35 inference(superposition,[status(thm)],[f149,f381])).
% 1.68/1.35 thf(f381,plain,(
% 1.68/1.35 ((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f380])).
% 1.68/1.35 thf(f380,plain,(
% 1.68/1.35 ($false = $true) | ((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(duplicate_literal_removal,[status(thm)],[f379])).
% 1.68/1.35 thf(f379,plain,(
% 1.68/1.35 ($false = $true) | ($false = $true) | ((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | spl6_3),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f371])).
% 1.68/1.35 thf(f371,plain,(
% 1.68/1.35 ( ! [X10 : $i,X5 : $i] : (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5))) ) | spl6_3),
% 1.68/1.35 inference(primitive_instantiation,[status(thm)],[f258])).
% 1.68/1.35 thf(f258,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) ) | spl6_3),
% 1.68/1.35 inference(subsumption_resolution,[status(thm)],[f244,f89])).
% 1.68/1.35 thf(f244,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true) | ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f243])).
% 1.68/1.35 thf(f243,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ((sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | ((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true)) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f242])).
% 1.68/1.35 thf(f242,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))))) )),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f241])).
% 1.68/1.35 thf(f241,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ($true != $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | ((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f240])).
% 1.68/1.35 thf(f240,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true) | (((sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) = $true) | (((sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))))) )),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f233])).
% 1.68/1.35 thf(f233,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK4 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK0 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ X5) = $true)) )),
% 1.68/1.35 inference(primitive_instantiation,[status(thm)],[f41])).
% 1.68/1.35 thf(f41,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f40])).
% 1.68/1.35 thf(f40,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f39])).
% 1.68/1.35 thf(f39,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f38])).
% 1.68/1.35 thf(f38,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f20])).
% 1.68/1.35 thf(f20,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o,X5 : $i] : (((X1 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK0 @ X1 @ X0) @ X5) = $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true)) )),
% 1.68/1.35 inference(cnf_transformation,[status(thm)],[f13])).
% 1.68/1.35 thf(f149,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) ) | ~spl6_5),
% 1.68/1.35 inference(avatar_component_clause,[status(thm)],[f148])).
% 1.68/1.35 thf(f148,definition,(
% 1.68/1.35 spl6_5 <=> ! [X1 : ($i > $o) > ($i > $o) > $i > $o,X10 : $i] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))))),
% 1.68/1.35 introduced(definition,[new_symbols(naming,[spl6_5])],[avatar_definition])).
% 1.68/1.35 thf(f150,plain,(
% 1.68/1.35 spl6_3 | spl6_5),
% 1.68/1.35 inference(avatar_split_clause,[status(thm)],[f134,f148,f87])).
% 1.68/1.35 thf(f134,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))) | ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) != (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f133])).
% 1.68/1.35 thf(f133,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (($true != ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))))) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) )),
% 1.68/1.35 inference(equality_proxy_clausification,[status(thm)],[f132])).
% 1.68/1.35 thf(f132,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ($true != ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))))) )),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f131])).
% 1.68/1.35 thf(f131,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | ($true != $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true != ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))))) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f130])).
% 1.68/1.35 thf(f130,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ($true = ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true)))) | (((sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | ($true != ((sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) = (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))))) )),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f116])).
% 1.68/1.35 thf(f116,plain,(
% 1.68/1.35 ( ! [X10 : $i,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK2 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK1 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK3 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK5 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0))))))) @ (sK4 @ X1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y1 = Y0)))))))) != $true)) )),
% 1.68/1.35 inference(primitive_instantiation,[status(thm)],[f45])).
% 1.68/1.35 thf(f45,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f44])).
% 1.68/1.35 thf(f44,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (($true = (X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f43])).
% 1.68/1.35 thf(f43,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f42])).
% 1.68/1.35 thf(f42,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: ($false)) @ X10) = $true)) )),
% 1.68/1.35 inference(boolean_simplification,[status(thm)],[f16])).
% 1.68/1.35 thf(f16,plain,(
% 1.68/1.35 ( ! [X10 : $i,X0 : ($i > $o) > ($i > $o) > $i > $o,X1 : ($i > $o) > ($i > $o) > $i > $o] : (((X0 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true) | ((X0 @ (sK2 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ (sK3 @ X1 @ X0)) != $true) | ((X0 @ (sK5 @ X1 @ X0) @ (sK5 @ X1 @ X0) @ (sK4 @ X1 @ X0)) != $true) | ((X1 @ (^[Y0 : $i]: (p | (~ p))) @ (^[Y0 : $i]: (p & (~ p))) @ X10) = $true)) )),
% 1.68/1.35 inference(cnf_transformation,[status(thm)],[f13])).
% 1.68/1.35 thf(f146,plain,(
% 1.68/1.35 ~spl6_3),
% 1.68/1.35 inference(avatar_contradiction_clause,[status(thm)],[f145])).
% 1.68/1.35 thf(f145,plain,(
% 1.68/1.35 $false | ~spl6_3),
% 1.68/1.35 inference(trivial_inequality_removal,[status(thm)],[f144])).
% 1.68/1.35 thf(f144,plain,(
% 1.68/1.35 ($false = $true) | ~spl6_3),
% 1.68/1.35 inference(beta_eta_normalization,[status(thm)],[f143])).
% 1.68/1.35 thf(f143,plain,(
% 1.68/1.35 ( ! [X1 : $i] : ((((^[Y0 : $i]: ($false)) @ X1) = ((^[Y0 : $i]: ($true)) @ X1))) ) | ~spl6_3),
% 1.68/1.35 inference(argument_congruence,[status(thm)],[f88])).
% 1.68/1.35 thf(f88,plain,(
% 1.68/1.35 ((^[Y0 : $i]: ($false)) = (^[Y0 : $i]: ($true))) | ~spl6_3),
% 1.68/1.35 inference(avatar_component_clause,[status(thm)],[f87])).
% 1.68/1.35 % SZS output end Proof for DTF2THF_17785
% 1.68/1.35 % (18118)------------------------------
% 1.68/1.35 % (18118)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (18118)Termination reason: Refutation
% 1.68/1.35
% 1.68/1.35 % (18118)Memory used [KB]: 5884
% 1.68/1.35 % (18118)Time elapsed: 0.049 s
% 1.68/1.35 % (18118)Instructions burned: 73 (million)
% 1.68/1.35 % (18118)------------------------------
% 1.68/1.35 % (18118)------------------------------
% 1.68/1.35 % (18112)Success in time 0.056 s
%------------------------------------------------------------------------------