%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEV463^1 : TPTP v9.2.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:41:18 AM UTC 2026
% Result : Theorem 1.63s 1.73s
% Output : Refutation 1.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 16
% Syntax : Number of formulae : 151 ( 21 unt; 0 typ; 10 def)
% Number of atoms : 1234 ( 273 equ; 0 cnn)
% Maximal formula atoms : 5 ( 8 avg)
% Number of connectives : 1447 ( 94 ~; 221 |; 0 &;1059 @)
% ( 10 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 220 ( 220 >; 0 *; 0 +; 0 <<)
% Number of symbols : 25 ( 21 usr; 13 con; 0-4 aty)
% ( 17 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 249 ( 23 ^; 220 !; 6 ?; 249 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_6,type,
sK0: $tType ).
thf(func_def_0,type,
'const/trivia/I':
!>[X0: $tType] : ( X0 > X0 ) ).
thf(func_def_1,type,
'const/sets/SUBSET':
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > $o ) ).
thf(func_def_2,type,
'const/sets/INTERS':
!>[X0: $tType] : ( ( ( X0 > $o ) > $o ) > X0 > $o ) ).
thf(func_def_3,type,
'const/sets/IN':
!>[X0: $tType] : ( X0 > ( X0 > $o ) > $o ) ).
thf(func_def_11,type,
sK1: sK0 > $o ).
thf(func_def_12,type,
sK2: ( sK0 > $o ) > $o ).
thf(func_def_13,type,
sP3: $o > $o ).
thf(func_def_16,type,
sK5: sK0 > $o ).
thf(func_def_17,type,
sK6:
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > X0 ) ).
thf(func_def_18,type,
sK7:
!>[X0: $tType] : ( ( ( X0 > $o ) > $o ) > X0 > X0 > $o ) ).
thf(func_def_19,type,
ph8:
!>[X0: $tType] : X0 ).
thf(f974,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f138,f147,f165,f166,f180,f183,f186,f390,f393,f401,f876,f973]) ).
thf(f973,plain,
( ~ spl4_2
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[status(thm)],[f972]) ).
thf(f972,plain,
( $false
| ~ spl4_2
| ~ spl4_14 ),
inference(trivial_inequality_removal,[status(thm)],[f971]) ).
thf(f971,plain,
( ( $true = $false )
| ~ spl4_2
| ~ spl4_14 ),
inference(forward_demodulation,[status(thm)],[f961,f137]) ).
thf(f137,plain,
( ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ~ spl4_2 ),
inference(avatar_component_clause,[status(thm)],[f135]) ).
thf(f135,definition,
( spl4_2
<=> ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl4_2])],[avatar_definition]) ).
thf(f961,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ~ spl4_14 ),
inference(trivial_inequality_removal,[status(thm)],[f960]) ).
thf(f960,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true = $false )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[status(thm)],[f952]) ).
thf(f952,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true = $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ~ spl4_14 ),
inference(superposition,[status(thm)],[f77,f887]) ).
thf(f887,plain,
( ! [X0: sK0 > $o] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK6 @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) @ sK1 )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_14 ),
inference(trivial_inequality_removal,[status(thm)],[f880]) ).
thf(f880,plain,
( ! [X0: sK0 > $o] :
( ( $true = $false )
| ( ( 'const/sets/IN' @ sK0 @ ( sK6 @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) @ sK1 )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_14 ),
inference(superposition,[status(thm)],[f441,f75]) ).
thf(f75,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $false
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X2 ) )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f74]) ).
thf(f74,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true = $false )
| ( $false
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X2 ) )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(boolean_simplification,[status(thm)],[f66]) ).
thf(f66,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X1 )
=> $true )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $false
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X2 ) ) ),
inference(cases_simplifying,[status(thm)],[f63]) ).
thf(f63,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( ( ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X1 )
=> ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X2 ) )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f62]) ).
thf(f62,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $false
= ( ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) )
@ ( sK6 @ X0 @ X1 @ X2 ) ) ) ),
inference(sigma_clausification,[status(thm)],[f61]) ).
thf(f61,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $false
= ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) ) ) )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f19]) ).
thf(f19,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) ) )
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) ) )
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ),
inference(fool_elimination,[status(thm)],[f10]) ).
thf(f10,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= ( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ) ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
! [X0: $tType,X1: X0 > $o,X3: X0 > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ X3 )
= ( ! [X4: X0] :
( ( 'const/sets/IN' @ X0 @ X4 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/SUBSET_') ).
thf(f441,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) ) )
| ~ spl4_14 ),
inference(avatar_component_clause,[status(thm)],[f440]) ).
thf(f440,definition,
( spl4_14
<=> ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl4_14])],[avatar_definition]) ).
thf(f77,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X1 ) )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f76]) ).
thf(f76,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X1 ) )
| ( $true = $false ) ),
inference(boolean_simplification,[status(thm)],[f65]) ).
thf(f65,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( ( $false
=> ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X2 ) )
= $false )
| ( $true
= ( 'const/sets/IN' @ X0 @ ( sK6 @ X0 @ X1 @ X2 ) @ X1 ) ) ),
inference(cases_simplifying,[status(thm)],[f63]) ).
thf(f876,plain,
( spl4_14
| ~ spl4_11 ),
inference(avatar_split_clause,[status(thm)],[f871,f177,f440]) ).
thf(f177,definition,
( spl4_11
<=> ! [X1: sK0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) )
| ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false ) ) ),
introduced(definition,[new_symbols(naming,[spl4_11])],[avatar_definition]) ).
thf(f871,plain,
( ! [X0: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_11 ),
inference(trivial_inequality_removal,[status(thm)],[f870]) ).
thf(f870,plain,
( ! [X0: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true = $false )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_11 ),
inference(duplicate_literal_removal,[status(thm)],[f863]) ).
thf(f863,plain,
( ! [X0: sK0] :
( ( $true = $false )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) ) )
| ~ spl4_11 ),
inference(superposition,[status(thm)],[f526,f111]) ).
thf(f111,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $false
= ( 'const/sets/IN' @ X0 @ X2 @ ( sK7 @ X0 @ X1 @ X2 ) ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f110]) ).
thf(f110,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $false
= ( 'const/sets/IN' @ X0 @ X2 @ ( sK7 @ X0 @ X1 @ X2 ) ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) )
| ( $true = $false ) ),
inference(boolean_simplification,[status(thm)],[f102]) ).
thf(f102,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( ( ( 'const/sets/IN' @ ( X0 > $o ) @ ( sK7 @ X0 @ X1 @ X2 ) @ X1 )
=> $true )
= $false )
| ( $false
= ( 'const/sets/IN' @ X0 @ X2 @ ( sK7 @ X0 @ X1 @ X2 ) ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ) ),
inference(cases_simplifying,[status(thm)],[f99]) ).
thf(f99,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $false
= ( ( 'const/sets/IN' @ ( X0 > $o ) @ ( sK7 @ X0 @ X1 @ X2 ) @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ ( sK7 @ X0 @ X1 @ X2 ) ) ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f98]) ).
thf(f98,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $false
= ( ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) )
@ ( sK7 @ X0 @ X1 @ X2 ) ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ) ),
inference(sigma_clausification,[status(thm)],[f97]) ).
thf(f97,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) )
| ( ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f20]) ).
thf(f20,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) ) )
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
thf(f9,plain,
! [X0: $tType,X1: ( X0 > $o ) > $o,X2: X0] :
( ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) ) )
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ),
inference(fool_elimination,[status(thm)],[f8]) ).
thf(f8,plain,
! [X0: $tType,X1: ( X0 > $o ) > $o,X2: X0,X3: X0 > $o] :
( ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ X3 ) )
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
! [X0: $tType,X1: ( X0 > $o ) > $o,X3: X0,X4: X0 > $o] :
( ( ( 'const/sets/IN' @ ( X0 > $o ) @ X4 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X3 @ X4 ) )
= ( 'const/sets/IN' @ X0 @ X3 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/IN_INTERS_') ).
thf(f526,plain,
( ! [X0: sK0,X1: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X1 @ ( sK7 @ sK0 @ sK2 @ X0 ) ) )
| ( ( 'const/sets/IN' @ sK0 @ X1 @ sK1 )
= $false )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_11 ),
inference(trivial_inequality_removal,[status(thm)],[f524]) ).
thf(f524,plain,
( ! [X0: sK0,X1: sK0] :
( ( ( 'const/sets/IN' @ sK0 @ X1 @ sK1 )
= $false )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true = $false )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X1 @ ( sK7 @ sK0 @ sK2 @ X0 ) ) ) )
| ~ spl4_11 ),
inference(superposition,[status(thm)],[f419,f90]) ).
thf(f90,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f89]) ).
thf(f89,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $true = $false )
| ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= $false ) ),
inference(boolean_simplification,[status(thm)],[f86]) ).
thf(f86,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= $false )
| ( $true = ( ~ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f85]) ).
thf(f85,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( ~ ( 'const/sets/IN' @ X0 @ X3 @ X1 ) ) ) ),
inference(boolean_simplification,[status(thm)],[f84]) ).
thf(f84,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( $true
= ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
=> $false ) ) ),
inference(cases_simplifying,[status(thm)],[f80]) ).
thf(f80,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
= $true )
| ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(beta_eta_normalization,[status(thm)],[f79]) ).
thf(f79,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( ( ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) )
@ X3 )
= $true ) ),
inference(pi_clausification,[status(thm)],[f60]) ).
thf(f60,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( !! @ X0
@ ^ [Y0: X0] :
( ( 'const/sets/IN' @ X0 @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ Y0 @ X2 ) ) ) )
| ( $false
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f19]) ).
thf(f419,plain,
( ! [X0: sK0] :
( ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( sK7 @ sK0 @ sK2 @ X0 ) )
= $true )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) )
| ~ spl4_11 ),
inference(trivial_inequality_removal,[status(thm)],[f406]) ).
thf(f406,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true = $false )
| ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( sK7 @ sK0 @ sK2 @ X0 ) )
= $true ) )
| ~ spl4_11 ),
inference(superposition,[status(thm)],[f178,f113]) ).
thf(f113,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $true
= ( 'const/sets/IN' @ ( X0 > $o ) @ ( sK7 @ X0 @ X1 @ X2 ) @ X1 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f112]) ).
thf(f112,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) )
| ( $true
= ( 'const/sets/IN' @ ( X0 > $o ) @ ( sK7 @ X0 @ X1 @ X2 ) @ X1 ) )
| ( $true = $false ) ),
inference(boolean_simplification,[status(thm)],[f101]) ).
thf(f101,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( $true
= ( 'const/sets/IN' @ ( X0 > $o ) @ ( sK7 @ X0 @ X1 @ X2 ) @ X1 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) ) )
| ( ( $false
=> ( 'const/sets/IN' @ X0 @ X2 @ ( sK7 @ X0 @ X1 @ X2 ) ) )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f99]) ).
thf(f178,plain,
( ! [X1: sK0 > $o] :
( ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) ) )
| ~ spl4_11 ),
inference(avatar_component_clause,[status(thm)],[f177]) ).
thf(f401,plain,
( spl4_2
| spl4_3 ),
inference(avatar_split_clause,[status(thm)],[f398,f140,f135]) ).
thf(f140,definition,
( spl4_3
<=> ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl4_3])],[avatar_definition]) ).
thf(f398,plain,
( ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| spl4_3 ),
inference(trivial_inequality_removal,[status(thm)],[f397]) ).
thf(f397,plain,
( ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true != $true )
| spl4_3 ),
inference(superposition,[status(thm)],[f141,f195]) ).
thf(f195,plain,
! [X0: $tType,X2: X0 > $o,X1: X0] :
( ( ( X2 @ X1 )
= $true )
| ( ( X2 @ X1 )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f194]) ).
thf(f194,plain,
! [X0: $tType,X2: X0 > $o,X1: X0] :
( ( ( X2 @ X1 )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( $true = $false ) ),
inference(superposition,[status(thm)],[f94,f95]) ).
thf(f95,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X1 ) )
| ( ( X1 @ X2 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f21]) ).
thf(f21,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( X1 @ X2 )
= ( 'const/sets/IN' @ X0 @ X2 @ X1 ) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
thf(f14,plain,
! [X0: $tType,X1: X0 > $o,X2: X0] :
( ( X1 @ X2 )
= ( 'const/sets/IN' @ X0 @ X2 @ X1 ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,axiom,
! [X0: $tType,X2: X0 > $o,X1: X0] :
( ( 'const/sets/IN' @ X0 @ X1 @ X2 )
= ( X2 @ X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/IN_') ).
thf(f94,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( $false
= ( 'const/sets/IN' @ X0 @ X2 @ X1 ) )
| ( $true
= ( X1 @ X2 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f21]) ).
thf(f141,plain,
( ( $true
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| spl4_3 ),
inference(avatar_component_clause,[status(thm)],[f140]) ).
thf(f393,plain,
( ~ spl4_4
| ~ spl4_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f392]) ).
thf(f392,plain,
( $false
| ~ spl4_4
| ~ spl4_10 ),
inference(trivial_inequality_removal,[status(thm)],[f391]) ).
thf(f391,plain,
( ( $true = $false )
| ~ spl4_4
| ~ spl4_10 ),
inference(forward_demodulation,[status(thm)],[f146,f175]) ).
thf(f175,plain,
( ( ( sP3 @ $false )
= $false )
| ~ spl4_10 ),
inference(avatar_component_clause,[status(thm)],[f173]) ).
thf(f173,definition,
( spl4_10
<=> ( ( sP3 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl4_10])],[avatar_definition]) ).
thf(f146,plain,
( ( $true
= ( sP3 @ $false ) )
| ~ spl4_4 ),
inference(avatar_component_clause,[status(thm)],[f144]) ).
thf(f144,definition,
( spl4_4
<=> ( $true
= ( sP3 @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl4_4])],[avatar_definition]) ).
thf(f390,plain,
( ~ spl4_3
| ~ spl4_6
| ~ spl4_8 ),
inference(avatar_contradiction_clause,[status(thm)],[f389]) ).
thf(f389,plain,
( $false
| ~ spl4_3
| ~ spl4_6
| ~ spl4_8 ),
inference(trivial_inequality_removal,[status(thm)],[f388]) ).
thf(f388,plain,
( ( $true = $false )
| ~ spl4_3
| ~ spl4_6
| ~ spl4_8 ),
inference(forward_demodulation,[status(thm)],[f382,f155]) ).
thf(f155,plain,
( ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 )
= $false )
| ~ spl4_6 ),
inference(avatar_component_clause,[status(thm)],[f153]) ).
thf(f153,definition,
( spl4_6
<=> ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl4_6])],[avatar_definition]) ).
thf(f382,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(trivial_inequality_removal,[status(thm)],[f381]) ).
thf(f381,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) )
| ( $true = $false )
| ~ spl4_3
| ~ spl4_8 ),
inference(duplicate_literal_removal,[status(thm)],[f380]) ).
thf(f380,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) )
| ( $true = $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(superposition,[status(thm)],[f199,f339]) ).
thf(f339,plain,
( ! [X0: sK0 > $o] :
( ( $true
= ( sK5 @ ( sK6 @ sK0 @ sK1 @ X0 ) ) )
| ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X0 )
= $true ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(trivial_inequality_removal,[status(thm)],[f333]) ).
thf(f333,plain,
( ! [X0: sK0 > $o] :
( ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X0 )
= $true )
| ( $true
= ( sK5 @ ( sK6 @ sK0 @ sK1 @ X0 ) ) )
| ( $true = $false ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(superposition,[status(thm)],[f330,f77]) ).
thf(f330,plain,
( ! [X0: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true
= ( sK5 @ X0 ) ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(trivial_inequality_removal,[status(thm)],[f326]) ).
thf(f326,plain,
( ! [X0: sK0] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true = $false )
| ( $true
= ( sK5 @ X0 ) ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(superposition,[status(thm)],[f321,f94]) ).
thf(f321,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ sK5 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(trivial_inequality_removal,[status(thm)],[f314]) ).
thf(f314,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ sK5 ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true = $false ) )
| ~ spl4_3
| ~ spl4_8 ),
inference(superposition,[status(thm)],[f164,f291]) ).
thf(f291,plain,
( ! [X0: sK0,X1: sK0 > $o] :
( ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ X1 ) ) )
| ~ spl4_3 ),
inference(trivial_inequality_removal,[status(thm)],[f288]) ).
thf(f288,plain,
( ! [X0: sK0,X1: sK0 > $o] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ X1 ) )
| ( $true = $false )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false ) )
| ~ spl4_3 ),
inference(superposition,[status(thm)],[f264,f126]) ).
thf(f126,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X3 ) )
| ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f125]) ).
thf(f125,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( $true = $false )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X3 ) )
| ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
= $false )
| ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false ) ),
inference(boolean_simplification,[status(thm)],[f122]) ).
thf(f122,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( $true = ( ~ $true ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X3 ) )
| ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f121]) ).
thf(f121,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( $true
= ( ~ ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 ) ) )
| ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X3 ) ) ),
inference(boolean_simplification,[status(thm)],[f120]) ).
thf(f120,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
=> $false )
= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X2 @ X3 ) ) ),
inference(cases_simplifying,[status(thm)],[f116]) ).
thf(f116,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( $true
= ( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ X3 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f115]) ).
thf(f115,plain,
! [X0: $tType,X2: X0,X3: X0 > $o,X1: ( X0 > $o ) > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false )
| ( $true
= ( ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) )
@ X3 ) ) ),
inference(pi_clausification,[status(thm)],[f96]) ).
thf(f96,plain,
! [X0: $tType,X2: X0,X1: ( X0 > $o ) > $o] :
( ( ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X1 )
=> ( 'const/sets/IN' @ X0 @ X2 @ Y0 ) ) )
= $true )
| ( ( 'const/sets/IN' @ X0 @ X2 @ ( 'const/sets/INTERS' @ X0 @ X1 ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f20]) ).
thf(f264,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) ) )
| ~ spl4_3 ),
inference(trivial_inequality_removal,[status(thm)],[f260]) ).
thf(f260,plain,
( ! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $false
= ( 'const/sets/IN' @ sK0 @ X0 @ sK1 ) )
| ( $true = $false ) )
| ~ spl4_3 ),
inference(superposition,[status(thm)],[f142,f90]) ).
thf(f142,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ~ spl4_3 ),
inference(avatar_component_clause,[status(thm)],[f140]) ).
thf(f164,plain,
( ( $true
= ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 ) )
| ~ spl4_8 ),
inference(avatar_component_clause,[status(thm)],[f162]) ).
thf(f162,definition,
( spl4_8
<=> ( $true
= ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 ) ) ),
introduced(definition,[new_symbols(naming,[spl4_8])],[avatar_definition]) ).
thf(f199,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( X2 @ ( sK6 @ X0 @ X1 @ X2 ) )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f198]) ).
thf(f198,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( X2 @ ( sK6 @ X0 @ X1 @ X2 ) )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
| ( $true = $false ) ),
inference(superposition,[status(thm)],[f95,f75]) ).
thf(f186,plain,
( ~ spl4_1
| ~ spl4_5 ),
inference(avatar_contradiction_clause,[status(thm)],[f185]) ).
thf(f185,plain,
( $false
| ~ spl4_1
| ~ spl4_5 ),
inference(trivial_inequality_removal,[status(thm)],[f184]) ).
thf(f184,plain,
( ( $true = $false )
| ~ spl4_1
| ~ spl4_5 ),
inference(forward_demodulation,[status(thm)],[f133,f151]) ).
thf(f151,plain,
( ( ( sP3 @ $true )
= $false )
| ~ spl4_5 ),
inference(avatar_component_clause,[status(thm)],[f149]) ).
thf(f149,definition,
( spl4_5
<=> ( ( sP3 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl4_5])],[avatar_definition]) ).
thf(f133,plain,
( ( ( sP3 @ $true )
= $true )
| ~ spl4_1 ),
inference(avatar_component_clause,[status(thm)],[f131]) ).
thf(f131,definition,
( spl4_1
<=> ( ( sP3 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl4_1])],[avatar_definition]) ).
thf(f183,plain,
( ~ spl4_2
| ~ spl4_3 ),
inference(avatar_contradiction_clause,[status(thm)],[f182]) ).
thf(f182,plain,
( $false
| ~ spl4_2
| ~ spl4_3 ),
inference(trivial_inequality_removal,[status(thm)],[f181]) ).
thf(f181,plain,
( ( $true = $false )
| ~ spl4_2
| ~ spl4_3 ),
inference(forward_demodulation,[status(thm)],[f142,f137]) ).
thf(f180,plain,
( spl4_11
| spl4_10 ),
inference(avatar_split_clause,[status(thm)],[f37,f173,f177]) ).
thf(f37,plain,
! [X1: sK0 > $o] :
( ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) )
| ( ( sP3 @ $false )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f36]) ).
thf(f36,plain,
! [X1: sK0 > $o] :
( ( ( sP3 @ $false )
= $false )
| ( $true = $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) )
| ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false ) ),
inference(boolean_simplification,[status(thm)],[f33]) ).
thf(f33,plain,
! [X1: sK0 > $o] :
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) )
| ( $true = ( ~ $true ) )
| ( ( sP3 @ $false )
= $false )
| ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f32]) ).
thf(f32,plain,
! [X1: sK0 > $o] :
( ( ( sP3 @ $false )
= $false )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) )
| ( $true
= ( ~ ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 ) ) ) ),
inference(boolean_simplification,[status(thm)],[f31]) ).
thf(f31,plain,
! [X1: sK0 > $o] :
( ( ( sP3 @ $false )
= $false )
| ( ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
=> $false )
= $true )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) ) ),
inference(cases_simplifying,[status(thm)],[f27]) ).
thf(f27,plain,
! [X1: sK0 > $o] :
( ( $true
= ( ( 'const/sets/IN' @ ( sK0 > $o ) @ X1 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ X1 ) ) )
| ( ( sP3 @ $false )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f26]) ).
thf(f26,plain,
! [X1: sK0 > $o] :
( ( $true
= ( ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) )
@ X1 ) )
| ( ( sP3 @ $false )
= $false ) ),
inference(pi_clausification,[status(thm)],[f25]) ).
thf(f25,plain,
( ( $true
= ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) ) )
| ( ( sP3 @ $false )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f22]) ).
thf(f22,plain,
( $false
= ( sP3
@ ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(naming,[sP3])],[inequality_splitting_name_introduction]) ).
thf(f166,plain,
( spl4_6
| spl4_5 ),
inference(avatar_split_clause,[status(thm)],[f54,f149,f153]) ).
thf(f54,plain,
( ( ( sP3 @ $true )
= $false )
| ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f53]) ).
thf(f53,plain,
( ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 )
= $false )
| ( $true = $false )
| ( ( sP3 @ $true )
= $false ) ),
inference(boolean_simplification,[status(thm)],[f45]) ).
thf(f45,plain,
( ( $false
= ( ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 )
=> $true ) )
| ( ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 )
= $false )
| ( ( sP3 @ $true )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f42]) ).
thf(f42,plain,
( ( ( ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) )
= $false )
| ( ( sP3 @ $true )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f41]) ).
thf(f41,plain,
( ( ( sP3 @ $true )
= $false )
| ( ( ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) )
@ sK5 )
= $false ) ),
inference(sigma_clausification,[status(thm)],[f24]) ).
thf(f24,plain,
( ( ( sP3 @ $true )
= $false )
| ( ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) )
= $false ) ),
inference(cases_simplifying,[status(thm)],[f22]) ).
thf(f165,plain,
( spl4_5
| spl4_8 ),
inference(avatar_split_clause,[status(thm)],[f56,f162,f149]) ).
thf(f56,plain,
( ( ( sP3 @ $true )
= $false )
| ( $true
= ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f55]) ).
thf(f55,plain,
( ( $true = $false )
| ( ( sP3 @ $true )
= $false )
| ( $true
= ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 ) ) ),
inference(boolean_simplification,[status(thm)],[f44]) ).
thf(f44,plain,
( ( ( sP3 @ $true )
= $false )
| ( $false
= ( $false
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK5 ) ) )
| ( $true
= ( 'const/sets/IN' @ ( sK0 > $o ) @ sK5 @ sK2 ) ) ),
inference(cases_simplifying,[status(thm)],[f42]) ).
thf(f147,plain,
( spl4_3
| spl4_4 ),
inference(avatar_split_clause,[status(thm)],[f59,f144,f140]) ).
thf(f59,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( $true
= ( sP3 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f23]) ).
thf(f23,plain,
( $true
= ( sP3 @ ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) ),
inference(inequality_splitting,[status(thm)],[f18,f22]) ).
thf(f18,plain,
( ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) )
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
thf(f17,plain,
( ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) )
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f15,f16]) ).
thf(f16,plain,
( ? [X0: $tType,X1: X0 > $o,X2: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X2 ) )
!= ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X2 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ Y0 ) ) ) )
=> ( ( !! @ ( sK0 > $o )
@ ^ [Y0: sK0 > $o] :
( ( 'const/sets/IN' @ ( sK0 > $o ) @ Y0 @ sK2 )
=> ( 'const/sets/SUBSET' @ sK0 @ sK1 @ Y0 ) ) )
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f15,plain,
? [X0: $tType,X1: X0 > $o,X2: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X2 ) )
!= ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X2 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ Y0 ) ) ) ),
inference(ennf_transformation,[status(thm)],[f13]) ).
thf(f13,plain,
~ ! [X0: $tType,X1: X0 > $o,X2: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X2 ) )
= ( !! @ ( X0 > $o )
@ ^ [Y0: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ Y0 @ X2 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ Y0 ) ) ) ),
inference(fool_elimination,[status(thm)],[f12]) ).
thf(f12,plain,
~ ! [X0: $tType,X1: X0 > $o,X2: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X2 ) )
= ( ! [X3: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ X3 @ X2 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ X3 ) ) ) ),
inference(rectify,[status(thm)],[f6]) ).
thf(f6,negated_conjecture,
~ ! [X0: $tType,X1: X0 > $o,X3: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X3 ) )
= ( ! [X4: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ X4 @ X3 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ X4 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
thf(f5,conjecture,
! [X0: $tType,X1: X0 > $o,X3: ( X0 > $o ) > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X1 @ ( 'const/sets/INTERS' @ X0 @ X3 ) )
= ( ! [X4: X0 > $o] :
( ( 'const/sets/IN' @ ( X0 > $o ) @ X4 @ X3 )
=> ( 'const/sets/SUBSET' @ X0 @ X1 @ X4 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/SUBSET_INTERS_') ).
thf(f138,plain,
( spl4_1
| spl4_2 ),
inference(avatar_split_clause,[status(thm)],[f58,f135,f131]) ).
thf(f58,plain,
( ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ ( 'const/sets/INTERS' @ sK0 @ sK2 ) ) )
| ( ( sP3 @ $true )
= $true ) ),
inference(cases_simplifying,[status(thm)],[f23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEV463^1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.33 % Computer : n008.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue Feb 24 12:47:24 EST 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.30/0.45 ---- Original DTF file ---
% 0.30/0.46 thf(spec,logic,$$dhol).
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 % File : SEV463^1 : TPTP v9.2.1. Released v7.0.0.
% 0.30/0.46 % Domain : Analysis
% 0.30/0.46 % Problem : SUBSET_INTERS
% 0.30/0.46 % Version : Especial.
% 0.30/0.46 % English :
% 0.30/0.46
% 0.30/0.46 % Refs : [Kal16] Kalisyk (2016), Email to Geoff Sutcliffe
% 0.30/0.46 % Source : [Kal16]
% 0.30/0.46 % Names : SUBSET_INTERS_.p [Kal16]
% 0.30/0.46
% 0.30/0.46 % Status : Theorem
% 0.30/0.46 % Rating : 0.33 v8.1.0, 0.25 v7.5.0, 0.00 v7.2.0, 0.25 v7.1.0
% 0.30/0.46 % Syntax : Number of formulae : 9 ( 5 unt; 4 typ; 0 def)
% 0.30/0.46 % Number of atoms : 17 ( 5 equ; 0 cnn)
% 0.30/0.46 % Maximal formula atoms : 1 ( 3 avg)
% 0.30/0.46 % Number of connectives : 40 ( 0 ~; 0 |; 0 &; 37 @)
% 0.30/0.46 % ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% 0.30/0.46 % Maximal formula depth : 4 ( 4 avg)
% 0.30/0.46 % Number of types : 1 ( 0 usr)
% 0.30/0.46 % Number of type conns : 24 ( 24 >; 0 *; 0 +; 0 <<)
% 0.30/0.46 % Number of symbols : 5 ( 4 usr; 0 con; 2-3 aty)
% 0.30/0.46 % Number of variables : 21 ( 0 ^; 17 !; 0 ?; 21 :)
% 0.30/0.46 % ( 4 !>; 0 ?*; 0 @-; 0 @+)
% 0.30/0.46 % SPC : TH1_THM_EQU_NAR
% 0.30/0.46
% 0.30/0.46 % Comments : Exported from core HOL Light.
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 thf('thf_const_const/trivia/I',type,
% 0.30/0.46 'const/trivia/I':
% 0.30/0.46 !>[A: $tType] : ( A > A ) ).
% 0.30/0.46
% 0.30/0.46 thf('thf_const_const/sets/SUBSET',type,
% 0.30/0.46 'const/sets/SUBSET':
% 0.30/0.46 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 0.30/0.46
% 0.30/0.46 thf('thf_const_const/sets/INTERS',type,
% 0.30/0.46 'const/sets/INTERS':
% 0.30/0.46 !>[A: $tType] : ( ( ( A > $o ) > $o ) > A > $o ) ).
% 0.30/0.46
% 0.30/0.46 thf('thf_const_const/sets/IN',type,
% 0.30/0.46 'const/sets/IN':
% 0.30/0.46 !>[A: $tType] : ( A > ( A > $o ) > $o ) ).
% 0.30/0.46
% 0.30/0.46 thf('thm/trivia/I_THM_',axiom,
% 0.30/0.46 ! [A: $tType,A0: A] :
% 0.30/0.46 ( ( 'const/trivia/I' @ A @ A0 )
% 0.30/0.46 = A0 ) ).
% 0.30/0.46
% 0.30/0.46 thf('thm/sets/IN_',axiom,
% 0.30/0.46 ! [A: $tType,P: A > $o,A0: A] :
% 0.30/0.46 ( ( 'const/sets/IN' @ A @ A0 @ P )
% 0.30/0.46 = ( P @ A0 ) ) ).
% 0.30/0.46
% 0.30/0.46 thf('thm/sets/IN_INTERS_',axiom,
% 0.30/0.46 ! [A: $tType,A0: ( A > $o ) > $o,A1: A] :
% 0.30/0.46 ( ( 'const/sets/IN' @ A @ A1 @ ( 'const/sets/INTERS' @ A @ A0 ) )
% 0.30/0.46 = ( ! [A2: A > $o] :
% 0.30/0.46 ( ( 'const/sets/IN' @ ( A > $o ) @ A2 @ A0 )
% 0.30/0.46 => ( 'const/sets/IN' @ A @ A1 @ A2 ) ) ) ) ).
% 0.30/0.46
% 0.30/0.46 thf('thm/sets/SUBSET_',axiom,
% 0.30/0.46 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 0.30/0.46 ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 0.30/0.46 = ( ! [A2: A] :
% 0.30/0.46 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 0.30/0.46 => ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 0.30/0.46
% 0.30/0.46 thf('thm/sets/SUBSET_INTERS_',conjecture,
% 0.30/0.46 ! [A: $tType,A0: A > $o,A1: ( A > $o ) > $o] :
% 0.30/0.46 ( ( 'const/sets/SUBSET' @ A @ A0 @ ( 'const/sets/INTERS' @ A @ A1 ) )
% 0.30/0.46 = ( ! [A2: A > $o] :
% 0.30/0.46 ( ( 'const/sets/IN' @ ( A > $o ) @ A2 @ A1 )
% 0.30/0.46 => ( 'const/sets/SUBSET' @ A @ A0 @ A2 ) ) ) ) ).
% 0.30/0.46
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 ------------------------
% 1.52/1.25 ---- Embedded in THF ---
% 1.52/1.25 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.52/1.25 %%% Generated on Tue Feb 24 12:47:25 EST 2026
% 1.52/1.25 %%% using '$$dhol' embedding, version 1.3.0.
% 1.52/1.25 %%% Logic specification used:
% 1.52/1.25 %%% thf(spec, logic, $$dhol).
% 1.52/1.25
% 1.52/1.25 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2DTF27929.p
% See solution above
% 1.52/1.25 ------------------------
% 1.52/1.26 ---- Cleaned THF ---
% 1.52/1.26 thf('thf_const_const/trivia/I',type,
% 1.52/1.26 'const/trivia/I':
% 1.52/1.26 !>[A: $tType] : ( A > A ) ).
% 1.52/1.26
% 1.52/1.26 thf('thf_const_const/sets/SUBSET',type,
% 1.52/1.26 'const/sets/SUBSET':
% 1.52/1.26 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 1.52/1.26
% 1.52/1.26 thf('thf_const_const/sets/INTERS',type,
% 1.52/1.26 'const/sets/INTERS':
% 1.52/1.26 !>[A: $tType] : ( ( ( A > $o ) > $o ) > A > $o ) ).
% 1.52/1.26
% 1.52/1.26 thf('thf_const_const/sets/IN',type,
% 1.52/1.26 'const/sets/IN':
% 1.52/1.26 !>[A: $tType] : ( A > ( A > $o ) > $o ) ).
% 1.52/1.26
% 1.52/1.26 thf('thm/trivia/I_THM_',axiom,
% 1.52/1.26 ! [A: $tType,A0: A] :
% 1.52/1.26 ( ( 'const/trivia/I' @ A @ A0 )
% 1.52/1.26 = A0 ) ).
% 1.52/1.26
% 1.52/1.26 thf('thm/sets/IN_',axiom,
% 1.52/1.26 ! [A: $tType,P: A > $o,A0: A] :
% 1.52/1.26 ( ( 'const/sets/IN' @ A @ A0 @ P )
% 1.52/1.26 = ( P @ A0 ) ) ).
% 1.52/1.26
% 1.52/1.26 thf('thm/sets/IN_INTERS_',axiom,
% 1.52/1.26 ! [A: $tType,A0: ( A > $o ) > $o,A1: A] :
% 1.52/1.26 ( ( 'const/sets/IN' @ A @ A1 @ ( 'const/sets/INTERS' @ A @ A0 ) )
% 1.52/1.26 = ( ! [A2: A > $o] :
% 1.52/1.26 ( ( 'const/sets/IN' @ ( A > $o ) @ A2 @ A0 )
% 1.52/1.26 => ( 'const/sets/IN' @ A @ A1 @ A2 ) ) ) ) ).
% 1.52/1.26
% 1.52/1.26 thf('thm/sets/SUBSET_',axiom,
% 1.52/1.26 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 1.52/1.26 ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 1.52/1.26 = ( ! [A2: A] :
% 1.52/1.26 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 1.52/1.26 => ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 1.52/1.26
% 1.52/1.26 thf('thm/sets/SUBSET_INTERS_',conjecture,
% 1.52/1.26 ! [A: $tType,A0: A > $o,A1: ( A > $o ) > $o] :
% 1.52/1.26 ( ( 'const/sets/SUBSET' @ A @ A0 @ ( 'const/sets/INTERS' @ A @ A1 ) )
% 1.52/1.26 = ( ! [A2: A > $o] :
% 1.52/1.26 ( ( 'const/sets/IN' @ ( A > $o ) @ A2 @ A1 )
% 1.52/1.26 => ( 'const/sets/SUBSET' @ A @ A0 @ A2 ) ) ) ) ).
% 1.52/1.26 ------------------------
% 1.52/1.27 % (28137)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_27929 for (2999ds/4Mi)
% 1.52/1.27 % (28138)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_27929 for (2999ds/27Mi)
% 1.52/1.27 % (28137)Instruction limit reached!
% 1.52/1.27 % (28137)------------------------------
% 1.52/1.27 % (28137)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.52/1.27 % (28137)Termination reason: Unknown
% 1.52/1.27 % (28137)Termination phase: Saturation
% 1.52/1.27
% 1.52/1.27 % (28137)Memory used [KB]: 5500
% 1.52/1.27 % (28137)Time elapsed: 0.003 s
% 1.52/1.27 % (28137)Instructions burned: 4 (million)
% 1.52/1.27 % (28137)------------------------------
% 1.52/1.27 % (28137)------------------------------
% 1.52/1.27 % (28139)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/2Mi)
% 1.52/1.27 % (28139)Instruction limit reached!
% 1.52/1.27 % (28139)------------------------------
% 1.52/1.27 % (28139)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.52/1.27 % (28139)Termination reason: Unknown
% 1.52/1.27 % (28139)Termination phase: Saturation
% 1.52/1.27
% 1.52/1.27 % (28139)Memory used [KB]: 5500
% 1.52/1.27 % (28139)Time elapsed: 0.003 s
% 1.52/1.27 % (28139)Instructions burned: 3 (million)
% 1.52/1.27 % (28139)------------------------------
% 1.52/1.27 % (28139)------------------------------
% 1.52/1.28 % (28136)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/183Mi)
% 1.52/1.28 % (28140)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_27929 for (2999ds/2Mi)
% 1.52/1.28 % (28141)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_27929 for (2999ds/275Mi)
% 1.52/1.28 % (28142)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/18Mi)
% 1.52/1.28 % Exception at run slice level
% 1.52/1.28 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.52/1.28 % (28143)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/3Mi)
% 1.52/1.28 % (28138)Instruction limit reached!
% 1.52/1.28 % (28138)------------------------------
% 1.52/1.28 % (28138)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.52/1.28 % (28138)Termination reason: Unknown
% 1.52/1.28 % (28138)Termination phase: Saturation
% 1.52/1.28
% 1.52/1.28 % (28138)Memory used [KB]: 5628
% 1.52/1.28 % (28138)Time elapsed: 0.012 s
% 1.52/1.28 % (28138)Instructions burned: 29 (million)
% 1.52/1.28 % (28138)------------------------------
% 1.52/1.28 % (28138)------------------------------
% 1.52/1.28 % (28143)Instruction limit reached!
% 1.52/1.28 % (28143)------------------------------
% 1.52/1.28 % (28143)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.52/1.28 % (28143)Termination reason: Unknown
% 1.52/1.28 % (28143)Termination phase: Saturation
% 1.52/1.28
% 1.52/1.28 % (28143)Memory used [KB]: 5500
% 1.52/1.28 % (28143)Time elapsed: 0.002 s
% 1.52/1.28 % (28143)Instructions burned: 3 (million)
% 1.52/1.28 % (28143)------------------------------
% 1.52/1.28 % (28143)------------------------------
% 1.52/1.29 % (28144)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_27929 for (2999ds/37Mi)
% 1.52/1.29 % Exception at run slice level
% 1.52/1.29 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.52/1.29 % (28142)Instruction limit reached!
% 1.52/1.29 % (28142)------------------------------
% 1.52/1.29 % (28142)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.52/1.29 % (28142)Termination reason: Unknown
% 1.52/1.29 % (28142)Termination phase: Saturation
% 1.52/1.29
% 1.52/1.29 % (28142)Memory used [KB]: 5628
% 1.52/1.29 % (28142)Time elapsed: 0.015 s
% 1.52/1.29 % (28142)Instructions burned: 19 (million)
% 1.52/1.29 % (28142)------------------------------
% 1.52/1.29 % (28142)------------------------------
% 1.52/1.29 % (28147)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_27929 for (2999ds/1041Mi)
% 1.52/1.29 % Exception at run slice level
% 1.52/1.29 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.30 % (28148)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/7Mi)
% 1.63/1.30 % (28145)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_27929 for (2999ds/15Mi)
% 1.63/1.30 % (28148)Instruction limit reached!
% 1.63/1.30 % (28148)------------------------------
% 1.63/1.30 % (28148)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.30 % (28148)Termination reason: Unknown
% 1.63/1.30 % (28148)Termination phase: Saturation
% 1.63/1.30
% 1.63/1.30 % (28148)Memory used [KB]: 1023
% 1.63/1.30 % (28148)Time elapsed: 0.004 s
% 1.63/1.30 % (28148)Instructions burned: 8 (million)
% 1.63/1.30 % (28148)------------------------------
% 1.63/1.30 % (28148)------------------------------
% 1.63/1.30 % (28146)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_27929 for (2999ds/3Mi)
% 1.63/1.30 % (28146)Instruction limit reached!
% 1.63/1.30 % (28146)------------------------------
% 1.63/1.30 % (28146)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.30 % (28146)Termination reason: Unknown
% 1.63/1.30 % (28146)Termination phase: Saturation
% 1.63/1.30
% 1.63/1.30 % (28146)Memory used [KB]: 5500
% 1.63/1.30 % (28146)Time elapsed: 0.004 s
% 1.63/1.30 % (28146)Instructions burned: 3 (million)
% 1.63/1.30 % (28146)------------------------------
% 1.63/1.30 % (28146)------------------------------
% 1.63/1.30 % (28150)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_27929 for (2999ds/3Mi)
% 1.63/1.30 % (28150)Instruction limit reached!
% 1.63/1.30 % (28150)------------------------------
% 1.63/1.30 % (28150)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.30 % (28150)Termination reason: Unknown
% 1.63/1.30 % (28150)Termination phase: Saturation
% 1.63/1.30
% 1.63/1.30 % (28150)Memory used [KB]: 5500
% 1.63/1.30 % (28150)Time elapsed: 0.002 s
% 1.63/1.30 % (28150)Instructions burned: 3 (million)
% 1.63/1.30 % (28150)------------------------------
% 1.63/1.30 % (28150)------------------------------
% 1.63/1.31 % (28145)Instruction limit reached!
% 1.63/1.31 % (28145)------------------------------
% 1.63/1.31 % (28145)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.31 % (28145)Termination reason: Unknown
% 1.63/1.31 % (28145)Termination phase: Saturation
% 1.63/1.31
% 1.63/1.31 % (28145)Memory used [KB]: 5628
% 1.63/1.31 % (28145)Time elapsed: 0.012 s
% 1.63/1.31 % (28145)Instructions burned: 15 (million)
% 1.63/1.31 % (28145)------------------------------
% 1.63/1.31 % (28145)------------------------------
% 1.63/1.31 % (28151)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_27929 for (2999ds/3Mi)
% 1.63/1.31 % (28149)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/16Mi)
% 1.63/1.31 % (28151)Instruction limit reached!
% 1.63/1.31 % (28151)------------------------------
% 1.63/1.31 % (28151)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.31 % (28151)Termination reason: Unknown
% 1.63/1.31 % (28151)Termination phase: Saturation
% 1.63/1.31
% 1.63/1.31 % (28151)Memory used [KB]: 1023
% 1.63/1.31 % (28151)Time elapsed: 0.003 s
% 1.63/1.31 % (28151)Instructions burned: 4 (million)
% 1.63/1.31 % (28151)------------------------------
% 1.63/1.31 % (28151)------------------------------
% 1.63/1.31 % (28153)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/3Mi)
% 1.63/1.31 % Exception at run slice level
% 1.63/1.31 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.31 % (28141)Refutation not found, incomplete strategy
% 1.63/1.31 % (28141)------------------------------
% 1.63/1.31 % (28141)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.31 % (28141)Termination reason: Refutation not found, incomplete strategy
% 1.63/1.31
% 1.63/1.31
% 1.63/1.31 % (28141)Memory used [KB]: 5756
% 1.63/1.31 % (28141)Time elapsed: 0.036 s
% 1.63/1.31 % (28141)Instructions burned: 54 (million)
% 1.63/1.31 % (28141)------------------------------
% 1.63/1.31 % (28141)------------------------------
% 1.63/1.32 % (28152)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/7Mi)
% 1.63/1.32 % (28155)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/18Mi)
% 1.63/1.32 % (28149)Instruction limit reached!
% 1.63/1.32 % (28149)------------------------------
% 1.63/1.32 % (28149)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.32 % (28149)Termination reason: Unknown
% 1.63/1.32 % (28149)Termination phase: Saturation
% 1.63/1.32
% 1.63/1.32 % (28149)Memory used [KB]: 5756
% 1.63/1.32 % (28149)Time elapsed: 0.013 s
% 1.63/1.32 % (28149)Instructions burned: 16 (million)
% 1.63/1.32 % (28149)------------------------------
% 1.63/1.32 % (28149)------------------------------
% 1.63/1.32 % (28156)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/710Mi)
% 1.63/1.33 % (28152)Instruction limit reached!
% 1.63/1.33 % (28152)------------------------------
% 1.63/1.33 % (28152)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.33 % (28152)Termination reason: Unknown
% 1.63/1.33 % (28152)Termination phase: Saturation
% 1.63/1.33
% 1.63/1.33 % (28152)Memory used [KB]: 5500
% 1.63/1.33 % (28152)Time elapsed: 0.007 s
% 1.63/1.33 % (28152)Instructions burned: 7 (million)
% 1.63/1.33 % (28152)------------------------------
% 1.63/1.33 % (28152)------------------------------
% 1.63/1.33 % (28154)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/4Mi)
% 1.63/1.33 % (28155)Instruction limit reached!
% 1.63/1.33 % (28155)------------------------------
% 1.63/1.33 % (28155)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.33 % (28155)Termination reason: Unknown
% 1.63/1.33 % (28155)Termination phase: Saturation
% 1.63/1.33
% 1.63/1.33 % (28155)Memory used [KB]: 5628
% 1.63/1.33 % (28155)Time elapsed: 0.009 s
% 1.63/1.33 % (28155)Instructions burned: 19 (million)
% 1.63/1.33 % (28155)------------------------------
% 1.63/1.33 % (28155)------------------------------
% 1.63/1.33 % (28154)Instruction limit reached!
% 1.63/1.33 % (28154)------------------------------
% 1.63/1.33 % (28154)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.33 % (28154)Termination reason: Unknown
% 1.63/1.33 % (28154)Termination phase: Saturation
% 1.63/1.33
% 1.63/1.33 % (28154)Memory used [KB]: 5500
% 1.63/1.33 % (28154)Time elapsed: 0.005 s
% 1.63/1.33 % (28154)Instructions burned: 5 (million)
% 1.63/1.33 % (28154)------------------------------
% 1.63/1.33 % (28154)------------------------------
% 1.63/1.33 % (28157)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/6Mi)
% 1.63/1.34 % (28157)Instruction limit reached!
% 1.63/1.34 % (28157)------------------------------
% 1.63/1.34 % (28157)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.34 % (28157)Termination reason: Unknown
% 1.63/1.34 % (28157)Termination phase: Saturation
% 1.63/1.34
% 1.63/1.34 % (28157)Memory used [KB]: 5500
% 1.63/1.34 % (28157)Time elapsed: 0.006 s
% 1.63/1.34 % (28157)Instructions burned: 6 (million)
% 1.63/1.34 % (28157)------------------------------
% 1.63/1.34 % (28157)------------------------------
% 1.63/1.34 % (28160)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/5Mi)
% 1.63/1.34 % Exception at run slice level
% 1.63/1.34 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.34 % (28158)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/902Mi)
% 1.63/1.34 % (28159)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/21Mi)
% 1.63/1.35 % (28161)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/6Mi)
% 1.63/1.35 % Exception at run slice level
% 1.63/1.35 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.35 % (28163)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/779Mi)
% 1.63/1.35 % Exception at run slice level
% 1.63/1.35 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.35 % (28162)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/377Mi)
% 1.63/1.36 % (28159)Instruction limit reached!
% 1.63/1.36 % (28159)------------------------------
% 1.63/1.36 % (28159)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.36 % (28159)Termination reason: Unknown
% 1.63/1.36 % (28159)Termination phase: Saturation
% 1.63/1.36
% 1.63/1.36 % (28159)Memory used [KB]: 5628
% 1.63/1.36 % (28159)Time elapsed: 0.037 s
% 1.63/1.36 % (28159)Instructions burned: 21 (million)
% 1.63/1.36 % (28159)------------------------------
% 1.63/1.36 % (28159)------------------------------
% 1.63/1.36 % (28165)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/879Mi)
% 1.63/1.36 % (28164)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/19Mi)
% 1.63/1.36 % Exception at run slice level
% 1.63/1.36 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.37 % (28167)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/3Mi)
% 1.63/1.37 % (28167)Instruction limit reached!
% 1.63/1.37 % (28167)------------------------------
% 1.63/1.37 % (28167)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.37 % (28167)Termination reason: Unknown
% 1.63/1.37 % (28167)Termination phase: Saturation
% 1.63/1.37
% 1.63/1.37 % (28167)Memory used [KB]: 1023
% 1.63/1.37 % (28167)Time elapsed: 0.003 s
% 1.63/1.37 % (28167)Instructions burned: 4 (million)
% 1.63/1.37 % (28167)------------------------------
% 1.63/1.37 % (28167)------------------------------
% 1.63/1.37 % (28166)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_27929 for (2999ds/17Mi)
% 1.63/1.38 % (28136)Instruction limit reached!
% 1.63/1.38 % (28136)------------------------------
% 1.63/1.38 % (28136)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.38 % (28136)Termination reason: Unknown
% 1.63/1.38 % (28136)Termination phase: Saturation
% 1.63/1.38
% 1.63/1.38 % (28136)Memory used [KB]: 6908
% 1.63/1.38 % (28136)Time elapsed: 0.106 s
% 1.63/1.38 % (28136)Instructions burned: 183 (million)
% 1.63/1.38 % (28136)------------------------------
% 1.63/1.38 % (28136)------------------------------
% 1.63/1.38 % (28168)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/30Mi)
% 1.63/1.39 % (28166)Instruction limit reached!
% 1.63/1.39 % (28166)------------------------------
% 1.63/1.39 % (28166)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.39 % (28166)Termination reason: Unknown
% 1.63/1.39 % (28166)Termination phase: Saturation
% 1.63/1.39
% 1.63/1.39 % (28166)Memory used [KB]: 5628
% 1.63/1.39 % (28166)Time elapsed: 0.037 s
% 1.63/1.39 % (28166)Instructions burned: 17 (million)
% 1.63/1.39 % (28166)------------------------------
% 1.63/1.39 % (28166)------------------------------
% 1.63/1.39 % (28168)Instruction limit reached!
% 1.63/1.39 % (28168)------------------------------
% 1.63/1.39 % (28168)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.39 % (28168)Termination reason: Unknown
% 1.63/1.39 % (28168)Termination phase: Saturation
% 1.63/1.39
% 1.63/1.39 % (28168)Memory used [KB]: 5628
% 1.63/1.39 % (28168)Time elapsed: 0.013 s
% 1.63/1.39 % (28168)Instructions burned: 31 (million)
% 1.63/1.39 % (28168)------------------------------
% 1.63/1.39 % (28168)------------------------------
% 1.63/1.40 % (28169)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/127Mi)
% 1.63/1.40 % (28170)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/100Mi)
% 1.63/1.40 % (28171)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/3Mi)
% 1.63/1.41 % Exception at run slice level
% 1.63/1.41 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.42 % (28172)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/20Mi)
% 1.63/1.42 % (28172)Instruction limit reached!
% 1.63/1.42 % (28172)------------------------------
% 1.63/1.42 % (28172)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.42 % (28172)Termination reason: Unknown
% 1.63/1.42 % (28172)Termination phase: Saturation
% 1.63/1.42
% 1.63/1.42 % (28172)Memory used [KB]: 5628
% 1.63/1.42 % (28172)Time elapsed: 0.009 s
% 1.63/1.42 % (28172)Instructions burned: 20 (million)
% 1.63/1.42 % (28172)------------------------------
% 1.63/1.42 % (28172)------------------------------
% 1.63/1.43 % (28173)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/86Mi)
% 1.63/1.44 % (28170)Instruction limit reached!
% 1.63/1.44 % (28170)------------------------------
% 1.63/1.44 % (28170)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.44 % (28170)Termination reason: Unknown
% 1.63/1.44 % (28170)Termination phase: Saturation
% 1.63/1.44
% 1.63/1.44 % (28170)Memory used [KB]: 5756
% 1.63/1.44 % (28170)Time elapsed: 0.038 s
% 1.63/1.44 % (28170)Instructions burned: 100 (million)
% 1.63/1.44 % (28170)------------------------------
% 1.63/1.44 % (28170)------------------------------
% 1.63/1.45 % (28169)Instruction limit reached!
% 1.63/1.45 % (28169)------------------------------
% 1.63/1.45 % (28169)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.45 % (28169)Termination reason: Unknown
% 1.63/1.45 % (28169)Termination phase: Saturation
% 1.63/1.45
% 1.63/1.45 % (28169)Memory used [KB]: 5756
% 1.63/1.45 % (28169)Time elapsed: 0.048 s
% 1.63/1.45 % (28169)Instructions burned: 128 (million)
% 1.63/1.45 % (28169)------------------------------
% 1.63/1.45 % (28169)------------------------------
% 1.63/1.45 % (28174)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/107Mi)
% 1.63/1.46 % (28175)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_27929 for (2998ds/39Mi)
% 1.63/1.46 % Exception at run slice level
% 1.63/1.46 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.46 % (28173)Instruction limit reached!
% 1.63/1.46 % (28173)------------------------------
% 1.63/1.46 % (28173)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.46 % (28173)Termination reason: Unknown
% 1.63/1.46 % (28173)Termination phase: Saturation
% 1.63/1.46
% 1.63/1.46 % (28173)Memory used [KB]: 5884
% 1.63/1.46 % (28173)Time elapsed: 0.032 s
% 1.63/1.46 % (28173)Instructions burned: 86 (million)
% 1.63/1.46 % (28173)------------------------------
% 1.63/1.46 % (28173)------------------------------
% 1.63/1.47 % (28176)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/448Mi)
% 1.63/1.47 % Exception at run slice level
% 1.63/1.47 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.47 % (28177)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/46Mi)
% 1.63/1.48 % (28178)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/98Mi)
% 1.63/1.48 % Exception at run slice level
% 1.63/1.48 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.49 % (28174)Instruction limit reached!
% 1.63/1.49 % (28174)------------------------------
% 1.63/1.49 % (28174)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.49 % (28174)Termination reason: Unknown
% 1.63/1.49 % (28174)Termination phase: Saturation
% 1.63/1.49
% 1.63/1.49 % (28174)Memory used [KB]: 5884
% 1.63/1.49 % (28174)Time elapsed: 0.039 s
% 1.63/1.49 % (28174)Instructions burned: 107 (million)
% 1.63/1.49 % (28174)------------------------------
% 1.63/1.49 % (28174)------------------------------
% 1.63/1.49 % (28179)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/507Mi)
% 1.63/1.49 % (28179)Refutation not found, incomplete strategy
% 1.63/1.49 % (28179)------------------------------
% 1.63/1.49 % (28179)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.49 % (28179)Termination reason: Refutation not found, incomplete strategy
% 1.63/1.49
% 1.63/1.49
% 1.63/1.49 % (28179)Memory used [KB]: 5500
% 1.63/1.49 % (28179)Time elapsed: 0.003 s
% 1.63/1.49 % (28179)Instructions burned: 4 (million)
% 1.63/1.49 % (28179)------------------------------
% 1.63/1.49 % (28179)------------------------------
% 1.63/1.49 % (28177)Instruction limit reached!
% 1.63/1.49 % (28177)------------------------------
% 1.63/1.49 % (28177)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.49 % (28177)Termination reason: Unknown
% 1.63/1.49 % (28177)Termination phase: Saturation
% 1.63/1.49
% 1.63/1.49 % (28177)Memory used [KB]: 5756
% 1.63/1.49 % (28177)Time elapsed: 0.019 s
% 1.63/1.49 % (28177)Instructions burned: 48 (million)
% 1.63/1.49 % (28177)------------------------------
% 1.63/1.49 % (28177)------------------------------
% 1.63/1.50 % (28180)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/149Mi)
% 1.63/1.50 % (28181)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/39Mi)
% 1.63/1.50 % (28182)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/6Mi)
% 1.63/1.50 % Exception at run slice level
% 1.63/1.50 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.50 % (28162)Instruction limit reached!
% 1.63/1.50 % (28162)------------------------------
% 1.63/1.50 % (28162)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.50 % (28162)Termination reason: Unknown
% 1.63/1.50 % (28162)Termination phase: Saturation
% 1.63/1.50
% 1.63/1.50 % (28162)Memory used [KB]: 6140
% 1.63/1.50 % (28162)Time elapsed: 0.174 s
% 1.63/1.50 % (28162)Instructions burned: 379 (million)
% 1.63/1.50 % (28162)------------------------------
% 1.63/1.50 % (28162)------------------------------
% 1.63/1.51 % (28183)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/1087Mi)
% 1.63/1.51 % (28184)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/47Mi)
% 1.63/1.51 % (28181)Instruction limit reached!
% 1.63/1.51 % (28181)------------------------------
% 1.63/1.51 % (28181)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.51 % (28181)Termination reason: Unknown
% 1.63/1.51 % (28181)Termination phase: Saturation
% 1.63/1.51
% 1.63/1.51 % (28181)Memory used [KB]: 5628
% 1.63/1.51 % (28181)Time elapsed: 0.016 s
% 1.63/1.51 % (28181)Instructions burned: 41 (million)
% 1.63/1.51 % (28181)------------------------------
% 1.63/1.51 % (28181)------------------------------
% 1.63/1.52 % (28185)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/44Mi)
% 1.63/1.52 % Exception at run slice level
% 1.63/1.52 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.53 % (28184)Instruction limit reached!
% 1.63/1.53 % (28184)------------------------------
% 1.63/1.53 % (28184)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.53 % (28184)Termination reason: Unknown
% 1.63/1.53 % (28184)Termination phase: Saturation
% 1.63/1.53
% 1.63/1.53 % (28184)Memory used [KB]: 5756
% 1.63/1.53 % (28184)Time elapsed: 0.019 s
% 1.63/1.53 % (28184)Instructions burned: 48 (million)
% 1.63/1.53 % (28184)------------------------------
% 1.63/1.53 % (28184)------------------------------
% 1.63/1.53 % (28186)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/432Mi)
% 1.63/1.54 % Exception at run slice level
% 1.63/1.54 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.54 % (28187)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/62Mi)
% 1.63/1.54 % Exception at run slice level
% 1.63/1.54 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.55 % (28188)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/31Mi)
% 1.63/1.55 % (28180)Instruction limit reached!
% 1.63/1.55 % (28180)------------------------------
% 1.63/1.55 % (28180)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.55 % (28180)Termination reason: Unknown
% 1.63/1.55 % (28180)Termination phase: Saturation
% 1.63/1.55
% 1.63/1.55 % (28180)Memory used [KB]: 5884
% 1.63/1.55 % (28180)Time elapsed: 0.056 s
% 1.63/1.55 % (28180)Instructions burned: 151 (million)
% 1.63/1.55 % (28180)------------------------------
% 1.63/1.55 % (28180)------------------------------
% 1.63/1.55 % (28189)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/96Mi)
% 1.63/1.55 % (28156)Instruction limit reached!
% 1.63/1.55 % (28156)------------------------------
% 1.63/1.55 % (28156)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.55 % (28156)Termination reason: Unknown
% 1.63/1.55 % (28156)Termination phase: Saturation
% 1.63/1.55
% 1.63/1.55 % (28156)Memory used [KB]: 7547
% 1.63/1.55 % (28156)Time elapsed: 0.231 s
% 1.63/1.55 % (28156)Instructions burned: 712 (million)
% 1.63/1.55 % (28156)------------------------------
% 1.63/1.55 % (28156)------------------------------
% 1.63/1.56 % (28188)Instruction limit reached!
% 1.63/1.56 % (28188)------------------------------
% 1.63/1.56 % (28188)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.56 % (28188)Termination reason: Unknown
% 1.63/1.56 % (28188)Termination phase: Saturation
% 1.63/1.56
% 1.63/1.56 % (28188)Memory used [KB]: 5628
% 1.63/1.56 % (28188)Time elapsed: 0.013 s
% 1.63/1.56 % (28188)Instructions burned: 32 (million)
% 1.63/1.56 % (28188)------------------------------
% 1.63/1.56 % (28188)------------------------------
% 1.63/1.56 % (28190)lrs+1002_1:4_au=on:cbe=off:cnfonf=lazy_pi_sigma_gen:hud=15:inj=on:nwc=4.0:s2a=on:sac=on:sp=reverse_arity:i=453:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/453Mi)
% 1.63/1.56 % Exception at run slice level
% 1.63/1.56 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.56 % (28191)lrs-1004_1:1_au=on:bsd=on:cbe=off:cnfonf=off:fe=axiom:fsd=on:i=71:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/71Mi)
% 1.63/1.57 % (28192)dis+1002_1:1_bd=off:fsr=off:ntd=on:s2a=on:ss=axioms:i=83:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/83Mi)
% 1.63/1.57 % (28193)lrs+10_1:128_cnfonf=lazy_not_gen_be_off:hud=1:ins=1:i=11:si=on:rtra=on_0 on DTF2THF_27929 for (2997ds/11Mi)
% 1.63/1.57 % Exception at run slice level
% 1.63/1.57 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.58 % (28194)lrs+1010_1:1_au=on:cbe=off:cnfonf=lazy_not_gen_be_off:fsr=off:spb=non_intro:i=41:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/41Mi)
% 1.63/1.58 % Exception at run slice level
% 1.63/1.58 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.59 % (28191)Instruction limit reached!
% 1.63/1.59 % (28191)------------------------------
% 1.63/1.59 % (28191)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.59 % (28191)Termination reason: Unknown
% 1.63/1.59 % (28191)Termination phase: Saturation
% 1.63/1.59
% 1.63/1.59 % (28191)Memory used [KB]: 5756
% 1.63/1.59 % (28191)Time elapsed: 0.024 s
% 1.63/1.59 % (28191)Instructions burned: 71 (million)
% 1.63/1.59 % (28191)------------------------------
% 1.63/1.59 % (28191)------------------------------
% 1.63/1.59 % (28189)Instruction limit reached!
% 1.63/1.59 % (28189)------------------------------
% 1.63/1.59 % (28189)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.59 % (28189)Termination reason: Unknown
% 1.63/1.59 % (28189)Termination phase: Saturation
% 1.63/1.59
% 1.63/1.59 % (28189)Memory used [KB]: 5884
% 1.63/1.59 % (28189)Time elapsed: 0.037 s
% 1.63/1.59 % (28189)Instructions burned: 98 (million)
% 1.63/1.59 % (28189)------------------------------
% 1.63/1.59 % (28189)------------------------------
% 1.63/1.59 % (28195)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/6Mi)
% 1.63/1.59 % (28195)Instruction limit reached!
% 1.63/1.59 % (28195)------------------------------
% 1.63/1.59 % (28195)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.59 % (28195)Termination reason: Unknown
% 1.63/1.59 % (28195)Termination phase: Saturation
% 1.63/1.59
% 1.63/1.59 % (28195)Memory used [KB]: 5500
% 1.63/1.59 % (28195)Time elapsed: 0.004 s
% 1.63/1.59 % (28195)Instructions burned: 6 (million)
% 1.63/1.59 % (28195)------------------------------
% 1.63/1.59 % (28195)------------------------------
% 1.63/1.59 % (28196)dis+10_1:1_avsq=on:cnfonf=off:e2e=on:nm=32:i=150:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/150Mi)
% 1.63/1.59 % (28192)Instruction limit reached!
% 1.63/1.59 % (28192)------------------------------
% 1.63/1.59 % (28192)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.59 % (28192)Termination reason: Unknown
% 1.63/1.59 % (28192)Termination phase: Saturation
% 1.63/1.59
% 1.63/1.59 % (28192)Memory used [KB]: 5884
% 1.63/1.59 % (28192)Time elapsed: 0.030 s
% 1.63/1.59 % (28192)Instructions burned: 85 (million)
% 1.63/1.59 % (28192)------------------------------
% 1.63/1.59 % (28192)------------------------------
% 1.63/1.60 % (28197)ott+1010_1:1_au=on:s2a=on:sd=7:ss=axioms:st=1.5:i=343:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/343Mi)
% 1.63/1.60 % (28198)ott+1010_1:4_cbe=off:chr=on:hfsq=on:hfsqr=1,16:hud=3:sac=on:sp=unary_frequency:ss=axioms:st=5.0:tnu=2:i=109:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/109Mi)
% 1.63/1.60 % (28199)dis+10_1:1_au=on:c=on:e2e=on:fsr=off:sos=all:sp=const_frequency:ss=axioms:i=253:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/253Mi)
% 1.63/1.63 % (28158)Instruction limit reached!
% 1.63/1.63 % (28158)------------------------------
% 1.63/1.63 % (28158)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.63 % (28158)Termination reason: Unknown
% 1.63/1.63 % (28158)Termination phase: Saturation
% 1.63/1.63
% 1.63/1.63 % (28158)Memory used [KB]: 5756
% 1.63/1.63 % (28158)Time elapsed: 0.296 s
% 1.63/1.63 % (28158)Instructions burned: 902 (million)
% 1.63/1.63 % (28158)------------------------------
% 1.63/1.63 % (28158)------------------------------
% 1.63/1.64 % (28196)Instruction limit reached!
% 1.63/1.64 % (28196)------------------------------
% 1.63/1.64 % (28196)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.64 % (28196)Termination reason: Unknown
% 1.63/1.64 % (28196)Termination phase: Saturation
% 1.63/1.64
% 1.63/1.64 % (28196)Memory used [KB]: 6012
% 1.63/1.64 % (28196)Time elapsed: 0.049 s
% 1.63/1.64 % (28196)Instructions burned: 153 (million)
% 1.63/1.64 % (28196)------------------------------
% 1.63/1.64 % (28196)------------------------------
% 1.63/1.64 % (28200)lrs+10_1:1_au=on:cnfonf=off:sd=1:sgt=16:ss=axioms:i=140:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/140Mi)
% 1.63/1.64 % (28198)Instruction limit reached!
% 1.63/1.64 % (28198)------------------------------
% 1.63/1.64 % (28198)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.64 % (28198)Termination reason: Unknown
% 1.63/1.64 % (28198)Termination phase: Saturation
% 1.63/1.64
% 1.63/1.64 % (28198)Memory used [KB]: 5756
% 1.63/1.64 % (28198)Time elapsed: 0.041 s
% 1.63/1.64 % (28198)Instructions burned: 110 (million)
% 1.63/1.64 % (28198)------------------------------
% 1.63/1.64 % (28198)------------------------------
% 1.63/1.65 % (28165)Instruction limit reached!
% 1.63/1.65 % (28165)------------------------------
% 1.63/1.65 % (28165)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.65 % (28165)Termination reason: Unknown
% 1.63/1.65 % (28165)Termination phase: Saturation
% 1.63/1.65
% 1.63/1.65 % (28165)Memory used [KB]: 6780
% 1.63/1.65 % (28165)Time elapsed: 0.316 s
% 1.63/1.65 % (28165)Instructions burned: 879 (million)
% 1.63/1.65 % (28165)------------------------------
% 1.63/1.65 % (28165)------------------------------
% 1.63/1.65 % (28201)dis+1010_16:1_acc=model:au=on:avsq=on:cond=fast:plsq=on:plsqc=2:plsqr=9267,262144:i=614:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/614Mi)
% 1.63/1.65 % (28202)lrs+1002_1:1_e2e=on:fde=unused:fe=axiom:prag=on:sd=1:sos=on:ss=axioms:st=2.0:i=202:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/202Mi)
% 1.63/1.66 % (28203)dis+1002_1:1_au=on:cs=on:ins=3:kws=inv_frequency:nwc=10.0:ss=axioms:st=3.0:i=339:si=on:rtra=on_0 on DTF2THF_27929 for (2996ds/339Mi)
% 1.63/1.69 % (28200)Instruction limit reached!
% 1.63/1.69 % (28200)------------------------------
% 1.63/1.69 % (28200)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.69 % (28200)Termination reason: Unknown
% 1.63/1.69 % (28200)Termination phase: Saturation
% 1.63/1.69
% 1.63/1.69 % (28200)Memory used [KB]: 6012
% 1.63/1.69 % (28200)Time elapsed: 0.045 s
% 1.63/1.69 % (28200)Instructions burned: 141 (million)
% 1.63/1.69 % (28200)------------------------------
% 1.63/1.69 % (28200)------------------------------
% 1.63/1.69 % (28199)Instruction limit reached!
% 1.63/1.69 % (28199)------------------------------
% 1.63/1.69 % (28199)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.69 % (28199)Termination reason: Unknown
% 1.63/1.69 % (28199)Termination phase: Saturation
% 1.63/1.69
% 1.63/1.69 % (28199)Memory used [KB]: 6012
% 1.63/1.69 % (28199)Time elapsed: 0.090 s
% 1.63/1.69 % (28199)Instructions burned: 254 (million)
% 1.63/1.69 % (28199)------------------------------
% 1.63/1.69 % (28199)------------------------------
% 1.63/1.69 % (28202)Refutation not found, incomplete strategy
% 1.63/1.69 % (28202)------------------------------
% 1.63/1.69 % (28202)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.69 % (28202)Termination reason: Refutation not found, incomplete strategy
% 1.63/1.69
% 1.63/1.69
% 1.63/1.69 % (28202)Memory used [KB]: 6012
% 1.63/1.69 % (28202)Time elapsed: 0.041 s
% 1.63/1.69 % (28202)Instructions burned: 111 (million)
% 1.63/1.69 % (28202)------------------------------
% 1.63/1.69 % (28202)------------------------------
% 1.63/1.70 % (28204)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=283:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/283Mi)
% 1.63/1.70 % Exception at run slice level
% 1.63/1.70 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.70 % (28205)dis+2_1:1_cha=on:hud=7:nwc=3.0:prag=on:tnu=2:i=134:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/134Mi)
% 1.63/1.70 % (28206)dis+1010_1:64_cnfonf=lazy_simp:fd=off:i=298:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/298Mi)
% 1.63/1.70 % Exception at run slice level
% 1.63/1.70 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.63/1.71 % (28207)lrs+2_1:8_erd=off:plsq=on:plsqr=32,1:sos=on:i=192:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/192Mi)
% 1.63/1.71 % (28197)Instruction limit reached!
% 1.63/1.71 % (28197)------------------------------
% 1.63/1.71 % (28197)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.71 % (28197)Termination reason: Unknown
% 1.63/1.71 % (28197)Termination phase: Saturation
% 1.63/1.71
% 1.63/1.71 % (28197)Memory used [KB]: 6268
% 1.63/1.71 % (28197)Time elapsed: 0.118 s
% 1.63/1.71 % (28197)Instructions burned: 344 (million)
% 1.63/1.71 % (28197)------------------------------
% 1.63/1.71 % (28197)------------------------------
% 1.63/1.71 % (28208)lrs+10_1:1_bd=off:hud=1:nm=0:prag=on:sd=2:sgt=32:sos=all:ss=axioms:i=258:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/258Mi)
% 1.63/1.72 % (28209)lrs+1002_1:1024_au=on:cond=fast:ntd=on:piset=and:plsq=on:plsqc=1:plsqr=183491,1048576:sac=on:tgt=ground:i=90:si=on:rtra=on_0 on DTF2THF_27929 for (2995ds/90Mi)
% 1.63/1.73 % (28203)First to succeed.
% 1.63/1.73 % (28203)Refutation found. Thanks to Tanya!
% 1.63/1.73 % SZS status Theorem for DTF2THF_27929
% 1.63/1.73 % SZS output start Proof for DTF2THF_27929
% 1.63/1.73 thf(type_def_6, type, sK0: $tType).
% 1.63/1.73 thf(func_def_0, type, 'const/trivia/I': !>[X0: $tType]:(X0 > X0)).
% 1.63/1.73 thf(func_def_1, type, 'const/sets/SUBSET': !>[X0: $tType]:((X0 > $o) > (X0 > $o) > $o)).
% 1.63/1.73 thf(func_def_2, type, 'const/sets/INTERS': !>[X0: $tType]:(((X0 > $o) > $o) > X0 > $o)).
% 1.63/1.73 thf(func_def_3, type, 'const/sets/IN': !>[X0: $tType]:(X0 > (X0 > $o) > $o)).
% 1.63/1.73 thf(func_def_11, type, sK1: sK0 > $o).
% 1.63/1.73 thf(func_def_12, type, sK2: (sK0 > $o) > $o).
% 1.63/1.73 thf(func_def_13, type, sP3: $o > $o).
% 1.63/1.73 thf(func_def_16, type, sK5: sK0 > $o).
% 1.63/1.73 thf(func_def_17, type, sK6: !>[X0: $tType]:((X0 > $o) > (X0 > $o) > X0)).
% 1.63/1.73 thf(func_def_18, type, sK7: !>[X0: $tType]:(((X0 > $o) > $o) > X0 > X0 > $o)).
% 1.63/1.73 thf(func_def_19, type, ph8: !>[X0: $tType]:(X0)).
% 1.63/1.73 thf(f974,plain,(
% 1.63/1.73 $false),
% 1.63/1.73 inference(avatar_sat_refutation,[status(thm)],[f138,f147,f165,f166,f180,f183,f186,f390,f393,f401,f876,f973])).
% 1.63/1.73 thf(f973,plain,(
% 1.63/1.73 ~spl4_2 | ~spl4_14),
% 1.63/1.73 inference(avatar_contradiction_clause,[status(thm)],[f972])).
% 1.63/1.73 thf(f972,plain,(
% 1.63/1.73 $false | (~spl4_2 | ~spl4_14)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f971])).
% 1.63/1.73 thf(f971,plain,(
% 1.63/1.73 ($true = $false) | (~spl4_2 | ~spl4_14)),
% 1.63/1.73 inference(forward_demodulation,[status(thm)],[f961,f137])).
% 1.63/1.73 thf(f137,plain,(
% 1.63/1.73 ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ~spl4_2),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f135])).
% 1.63/1.73 thf(f135,definition,(
% 1.63/1.73 spl4_2 <=> ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2)))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_2])],[avatar_definition])).
% 1.63/1.73 thf(f961,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ~spl4_14),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f960])).
% 1.63/1.73 thf(f960,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = $false) | ~spl4_14),
% 1.63/1.73 inference(duplicate_literal_removal,[status(thm)],[f952])).
% 1.63/1.73 thf(f952,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ~spl4_14),
% 1.63/1.73 inference(superposition,[status(thm)],[f77,f887])).
% 1.63/1.73 thf(f887,plain,(
% 1.63/1.73 ( ! [X0 : sK0 > $o] : ((('const/sets/IN' @ sK0 @ (sK6 @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)) @ sK1) = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_14),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f880])).
% 1.63/1.73 thf(f880,plain,(
% 1.63/1.73 ( ! [X0 : sK0 > $o] : (($true = $false) | (('const/sets/IN' @ sK0 @ (sK6 @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)) @ sK1) = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_14),
% 1.63/1.73 inference(superposition,[status(thm)],[f441,f75])).
% 1.63/1.73 thf(f75,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($false = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X2)) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f74])).
% 1.63/1.73 thf(f74,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = $false) | ($false = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X2)) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f66])).
% 1.63/1.73 thf(f66,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (((('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X1) => $true) = $false) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($false = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X2))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f63])).
% 1.63/1.73 thf(f63,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ((('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X1) => ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X2)) = $false)) )),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f62])).
% 1.63/1.73 thf(f62,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($false = ((^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))) @ (sK6 @ X0 @ X1 @ X2)))) )),
% 1.63/1.73 inference(sigma_clausification,[status(thm)],[f61])).
% 1.63/1.73 thf(f61,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($false = (!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))))) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f19])).
% 1.63/1.73 thf(f19,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2)))) = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(cnf_transformation,[status(thm)],[f11])).
% 1.63/1.73 thf(f11,plain,(
% 1.63/1.73 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2)))) = ('const/sets/SUBSET' @ X0 @ X1 @ X2))),
% 1.63/1.73 inference(fool_elimination,[status(thm)],[f10])).
% 1.63/1.73 thf(f10,plain,(
% 1.63/1.73 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ X2) = ! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X2)))),
% 1.63/1.73 inference(rectify,[status(thm)],[f4])).
% 1.63/1.73 thf(f4,axiom,(
% 1.63/1.73 ! [X0 : $tType,X1 : X0 > $o,X3 : X0 > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ X3) = ! [X4 : X0] : (('const/sets/IN' @ X0 @ X4 @ X1) => ('const/sets/IN' @ X0 @ X4 @ X3)))),
% 1.63/1.73 file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/SUBSET_')).
% 1.63/1.73 thf(f441,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1))) ) | ~spl4_14),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f440])).
% 1.63/1.73 thf(f440,definition,(
% 1.63/1.73 spl4_14 <=> ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_14])],[avatar_definition])).
% 1.63/1.73 thf(f77,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X1)) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f76])).
% 1.63/1.73 thf(f76,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X1)) | ($true = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f65])).
% 1.63/1.73 thf(f65,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | (($false => ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X2)) = $false) | ($true = ('const/sets/IN' @ X0 @ (sK6 @ X0 @ X1 @ X2) @ X1))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f63])).
% 1.63/1.73 thf(f876,plain,(
% 1.63/1.73 spl4_14 | ~spl4_11),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f871,f177,f440])).
% 1.63/1.73 thf(f177,definition,(
% 1.63/1.73 spl4_11 <=> ! [X1 : sK0 > $o] : (($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1)) | (('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_11])],[avatar_definition])).
% 1.63/1.73 thf(f871,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_11),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f870])).
% 1.63/1.73 thf(f870,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = $false) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_11),
% 1.63/1.73 inference(duplicate_literal_removal,[status(thm)],[f863])).
% 1.63/1.73 thf(f863,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = $false) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1))) ) | ~spl4_11),
% 1.63/1.73 inference(superposition,[status(thm)],[f526,f111])).
% 1.63/1.73 thf(f111,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($false = ('const/sets/IN' @ X0 @ X2 @ (sK7 @ X0 @ X1 @ X2))) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f110])).
% 1.63/1.73 thf(f110,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($false = ('const/sets/IN' @ X0 @ X2 @ (sK7 @ X0 @ X1 @ X2))) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1))) | ($true = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f102])).
% 1.63/1.73 thf(f102,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (((('const/sets/IN' @ (X0 > $o) @ (sK7 @ X0 @ X1 @ X2) @ X1) => $true) = $false) | ($false = ('const/sets/IN' @ X0 @ X2 @ (sK7 @ X0 @ X1 @ X2))) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f99])).
% 1.63/1.73 thf(f99,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($false = (('const/sets/IN' @ (X0 > $o) @ (sK7 @ X0 @ X1 @ X2) @ X1) => ('const/sets/IN' @ X0 @ X2 @ (sK7 @ X0 @ X1 @ X2)))) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f98])).
% 1.63/1.73 thf(f98,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($false = ((^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0))) @ (sK7 @ X0 @ X1 @ X2))) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(sigma_clausification,[status(thm)],[f97])).
% 1.63/1.73 thf(f97,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1))) | ((!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0)))) = $false)) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f20])).
% 1.63/1.73 thf(f20,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (((!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0)))) = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(cnf_transformation,[status(thm)],[f9])).
% 1.63/1.73 thf(f9,plain,(
% 1.63/1.73 ! [X0 : $tType,X1 : (X0 > $o) > $o,X2 : X0] : ((!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0)))) = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))),
% 1.63/1.73 inference(fool_elimination,[status(thm)],[f8])).
% 1.63/1.73 thf(f8,plain,(
% 1.63/1.73 ! [X0 : $tType,X1 : (X0 > $o) > $o,X2 : X0] : (! [X3 : X0 > $o] : (('const/sets/IN' @ (X0 > $o) @ X3 @ X1) => ('const/sets/IN' @ X0 @ X2 @ X3)) = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))),
% 1.63/1.73 inference(rectify,[status(thm)],[f3])).
% 1.63/1.73 thf(f3,axiom,(
% 1.63/1.73 ! [X0 : $tType,X1 : (X0 > $o) > $o,X3 : X0] : (! [X4 : X0 > $o] : (('const/sets/IN' @ (X0 > $o) @ X4 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X4)) = ('const/sets/IN' @ X0 @ X3 @ ('const/sets/INTERS' @ X0 @ X1)))),
% 1.63/1.73 file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/IN_INTERS_')).
% 1.63/1.73 thf(f526,plain,(
% 1.63/1.73 ( ! [X0 : sK0,X1 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X1 @ (sK7 @ sK0 @ sK2 @ X0))) | (('const/sets/IN' @ sK0 @ X1 @ sK1) = $false) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_11),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f524])).
% 1.63/1.73 thf(f524,plain,(
% 1.63/1.73 ( ! [X0 : sK0,X1 : sK0] : ((('const/sets/IN' @ sK0 @ X1 @ sK1) = $false) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = $false) | ($true = ('const/sets/IN' @ sK0 @ X1 @ (sK7 @ sK0 @ sK2 @ X0)))) ) | ~spl4_11),
% 1.63/1.73 inference(superposition,[status(thm)],[f419,f90])).
% 1.63/1.73 thf(f90,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | (('const/sets/IN' @ X0 @ X3 @ X1) = $false)) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f89])).
% 1.63/1.73 thf(f89,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($true = $false) | ($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | (('const/sets/IN' @ X0 @ X3 @ X1) = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f86])).
% 1.63/1.73 thf(f86,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | (('const/sets/IN' @ X0 @ X3 @ X1) = $false) | ($true = (~ $true))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f85])).
% 1.63/1.73 thf(f85,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | ($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = (~ ('const/sets/IN' @ X0 @ X3 @ X1)))) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f84])).
% 1.63/1.73 thf(f84,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | ($true = (('const/sets/IN' @ X0 @ X3 @ X1) => $false))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f80])).
% 1.63/1.73 thf(f80,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (((('const/sets/IN' @ X0 @ X3 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X2)) = $true) | ($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f79])).
% 1.63/1.73 thf(f79,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | (((^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))) @ X3) = $true)) )),
% 1.63/1.73 inference(pi_clausification,[status(thm)],[f60])).
% 1.63/1.73 thf(f60,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = (!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))))) | ($false = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f19])).
% 1.63/1.73 thf(f419,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : ((('const/sets/SUBSET' @ sK0 @ sK1 @ (sK7 @ sK0 @ sK2 @ X0)) = $true) | ($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2)))) ) | ~spl4_11),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f406])).
% 1.63/1.73 thf(f406,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = $false) | (('const/sets/SUBSET' @ sK0 @ sK1 @ (sK7 @ sK0 @ sK2 @ X0)) = $true)) ) | ~spl4_11),
% 1.63/1.73 inference(superposition,[status(thm)],[f178,f113])).
% 1.63/1.73 thf(f113,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($true = ('const/sets/IN' @ (X0 > $o) @ (sK7 @ X0 @ X1 @ X2) @ X1)) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)))) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f112])).
% 1.63/1.73 thf(f112,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1))) | ($true = ('const/sets/IN' @ (X0 > $o) @ (sK7 @ X0 @ X1 @ X2) @ X1)) | ($true = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f101])).
% 1.63/1.73 thf(f101,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (($true = ('const/sets/IN' @ (X0 > $o) @ (sK7 @ X0 @ X1 @ X2) @ X1)) | ($true = ('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1))) | (($false => ('const/sets/IN' @ X0 @ X2 @ (sK7 @ X0 @ X1 @ X2))) = $false)) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f99])).
% 1.63/1.73 thf(f178,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : ((('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1))) ) | ~spl4_11),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f177])).
% 1.63/1.73 thf(f401,plain,(
% 1.63/1.73 spl4_2 | spl4_3),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f398,f140,f135])).
% 1.63/1.73 thf(f140,definition,(
% 1.63/1.73 spl4_3 <=> ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2)))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_3])],[avatar_definition])).
% 1.63/1.73 thf(f398,plain,(
% 1.63/1.73 ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | spl4_3),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f397])).
% 1.63/1.73 thf(f397,plain,(
% 1.63/1.73 ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true != $true) | spl4_3),
% 1.63/1.73 inference(superposition,[status(thm)],[f141,f195])).
% 1.63/1.73 thf(f195,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0] : (((X2 @ X1) = $true) | ((X2 @ X1) = $false)) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f194])).
% 1.63/1.73 thf(f194,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0] : (((X2 @ X1) = $true) | ((X2 @ X1) = $false) | ($true = $false)) )),
% 1.63/1.73 inference(superposition,[status(thm)],[f94,f95])).
% 1.63/1.73 thf(f95,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : (($true = ('const/sets/IN' @ X0 @ X2 @ X1)) | ((X1 @ X2) = $false)) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f21])).
% 1.63/1.73 thf(f21,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : (((X1 @ X2) = ('const/sets/IN' @ X0 @ X2 @ X1))) )),
% 1.63/1.73 inference(cnf_transformation,[status(thm)],[f14])).
% 1.63/1.73 thf(f14,plain,(
% 1.63/1.73 ! [X0 : $tType,X1 : X0 > $o,X2 : X0] : ((X1 @ X2) = ('const/sets/IN' @ X0 @ X2 @ X1))),
% 1.63/1.73 inference(rectify,[status(thm)],[f2])).
% 1.63/1.73 thf(f2,axiom,(
% 1.63/1.73 ! [X0 : $tType,X2 : X0 > $o,X1 : X0] : (('const/sets/IN' @ X0 @ X1 @ X2) = (X2 @ X1))),
% 1.63/1.73 file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/IN_')).
% 1.63/1.73 thf(f94,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : (($false = ('const/sets/IN' @ X0 @ X2 @ X1)) | ($true = (X1 @ X2))) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f21])).
% 1.63/1.73 thf(f141,plain,(
% 1.63/1.73 ($true != ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | spl4_3),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f140])).
% 1.63/1.73 thf(f393,plain,(
% 1.63/1.73 ~spl4_4 | ~spl4_10),
% 1.63/1.73 inference(avatar_contradiction_clause,[status(thm)],[f392])).
% 1.63/1.73 thf(f392,plain,(
% 1.63/1.73 $false | (~spl4_4 | ~spl4_10)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f391])).
% 1.63/1.73 thf(f391,plain,(
% 1.63/1.73 ($true = $false) | (~spl4_4 | ~spl4_10)),
% 1.63/1.73 inference(forward_demodulation,[status(thm)],[f146,f175])).
% 1.63/1.73 thf(f175,plain,(
% 1.63/1.73 ((sP3 @ $false) = $false) | ~spl4_10),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f173])).
% 1.63/1.73 thf(f173,definition,(
% 1.63/1.73 spl4_10 <=> ((sP3 @ $false) = $false)),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_10])],[avatar_definition])).
% 1.63/1.73 thf(f146,plain,(
% 1.63/1.73 ($true = (sP3 @ $false)) | ~spl4_4),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f144])).
% 1.63/1.73 thf(f144,definition,(
% 1.63/1.73 spl4_4 <=> ($true = (sP3 @ $false))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_4])],[avatar_definition])).
% 1.63/1.73 thf(f390,plain,(
% 1.63/1.73 ~spl4_3 | ~spl4_6 | ~spl4_8),
% 1.63/1.73 inference(avatar_contradiction_clause,[status(thm)],[f389])).
% 1.63/1.73 thf(f389,plain,(
% 1.63/1.73 $false | (~spl4_3 | ~spl4_6 | ~spl4_8)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f388])).
% 1.63/1.73 thf(f388,plain,(
% 1.63/1.73 ($true = $false) | (~spl4_3 | ~spl4_6 | ~spl4_8)),
% 1.63/1.73 inference(forward_demodulation,[status(thm)],[f382,f155])).
% 1.63/1.73 thf(f155,plain,(
% 1.63/1.73 (('const/sets/SUBSET' @ sK0 @ sK1 @ sK5) = $false) | ~spl4_6),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f153])).
% 1.63/1.73 thf(f153,definition,(
% 1.63/1.73 spl4_6 <=> (('const/sets/SUBSET' @ sK0 @ sK1 @ sK5) = $false)),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_6])],[avatar_definition])).
% 1.63/1.73 thf(f382,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5)) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f381])).
% 1.63/1.73 thf(f381,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5)) | ($true = $false) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(duplicate_literal_removal,[status(thm)],[f380])).
% 1.63/1.73 thf(f380,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5)) | ($true = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5)) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(superposition,[status(thm)],[f199,f339])).
% 1.63/1.73 thf(f339,plain,(
% 1.63/1.73 ( ! [X0 : sK0 > $o] : (($true = (sK5 @ (sK6 @ sK0 @ sK1 @ X0))) | (('const/sets/SUBSET' @ sK0 @ sK1 @ X0) = $true)) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f333])).
% 1.63/1.73 thf(f333,plain,(
% 1.63/1.73 ( ! [X0 : sK0 > $o] : ((('const/sets/SUBSET' @ sK0 @ sK1 @ X0) = $true) | ($true = (sK5 @ (sK6 @ sK0 @ sK1 @ X0))) | ($true = $false)) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(superposition,[status(thm)],[f330,f77])).
% 1.63/1.73 thf(f330,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = (sK5 @ X0))) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f326])).
% 1.63/1.73 thf(f326,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = $false) | ($true = (sK5 @ X0))) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(superposition,[status(thm)],[f321,f94])).
% 1.63/1.73 thf(f321,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ sK5)) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1))) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f314])).
% 1.63/1.73 thf(f314,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ sK5)) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = $false)) ) | (~spl4_3 | ~spl4_8)),
% 1.63/1.73 inference(superposition,[status(thm)],[f164,f291])).
% 1.63/1.73 thf(f291,plain,(
% 1.63/1.73 ( ! [X0 : sK0,X1 : sK0 > $o] : ((('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = ('const/sets/IN' @ sK0 @ X0 @ X1))) ) | ~spl4_3),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f288])).
% 1.63/1.73 thf(f288,plain,(
% 1.63/1.73 ( ! [X0 : sK0,X1 : sK0 > $o] : (($true = ('const/sets/IN' @ sK0 @ X0 @ X1)) | ($true = $false) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | (('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false)) ) | ~spl4_3),
% 1.63/1.73 inference(superposition,[status(thm)],[f264,f126])).
% 1.63/1.73 thf(f126,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : ((('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ($true = ('const/sets/IN' @ X0 @ X2 @ X3)) | (('const/sets/IN' @ (X0 > $o) @ X3 @ X1) = $false)) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f125])).
% 1.63/1.73 thf(f125,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : (($true = $false) | ($true = ('const/sets/IN' @ X0 @ X2 @ X3)) | (('const/sets/IN' @ (X0 > $o) @ X3 @ X1) = $false) | (('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f122])).
% 1.63/1.73 thf(f122,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : ((('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ($true = (~ $true)) | ($true = ('const/sets/IN' @ X0 @ X2 @ X3)) | (('const/sets/IN' @ (X0 > $o) @ X3 @ X1) = $false)) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f121])).
% 1.63/1.73 thf(f121,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : (($true = (~ ('const/sets/IN' @ (X0 > $o) @ X3 @ X1))) | (('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ($true = ('const/sets/IN' @ X0 @ X2 @ X3))) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f120])).
% 1.63/1.73 thf(f120,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : ((('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ((('const/sets/IN' @ (X0 > $o) @ X3 @ X1) => $false) = $true) | ($true = ('const/sets/IN' @ X0 @ X2 @ X3))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f116])).
% 1.63/1.73 thf(f116,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : ((('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ($true = (('const/sets/IN' @ (X0 > $o) @ X3 @ X1) => ('const/sets/IN' @ X0 @ X2 @ X3)))) )),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f115])).
% 1.63/1.73 thf(f115,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X3 : X0 > $o,X1 : (X0 > $o) > $o] : ((('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false) | ($true = ((^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0))) @ X3))) )),
% 1.63/1.73 inference(pi_clausification,[status(thm)],[f96])).
% 1.63/1.73 thf(f96,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o) > $o] : (((!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X1) => ('const/sets/IN' @ X0 @ X2 @ Y0)))) = $true) | (('const/sets/IN' @ X0 @ X2 @ ('const/sets/INTERS' @ X0 @ X1)) = $false)) )),
% 1.63/1.73 inference(binary_proxy_clausification,[status(thm)],[f20])).
% 1.63/1.73 thf(f264,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1))) ) | ~spl4_3),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f260])).
% 1.63/1.73 thf(f260,plain,(
% 1.63/1.73 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($false = ('const/sets/IN' @ sK0 @ X0 @ sK1)) | ($true = $false)) ) | ~spl4_3),
% 1.63/1.73 inference(superposition,[status(thm)],[f142,f90])).
% 1.63/1.73 thf(f142,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ~spl4_3),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f140])).
% 1.63/1.73 thf(f164,plain,(
% 1.63/1.73 ($true = ('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2)) | ~spl4_8),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f162])).
% 1.63/1.73 thf(f162,definition,(
% 1.63/1.73 spl4_8 <=> ($true = ('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_8])],[avatar_definition])).
% 1.63/1.73 thf(f199,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (((X2 @ (sK6 @ X0 @ X1 @ X2)) = $false) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2))) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f198])).
% 1.63/1.73 thf(f198,plain,(
% 1.63/1.73 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (((X2 @ (sK6 @ X0 @ X1 @ X2)) = $false) | ($true = ('const/sets/SUBSET' @ X0 @ X1 @ X2)) | ($true = $false)) )),
% 1.63/1.73 inference(superposition,[status(thm)],[f95,f75])).
% 1.63/1.73 thf(f186,plain,(
% 1.63/1.73 ~spl4_1 | ~spl4_5),
% 1.63/1.73 inference(avatar_contradiction_clause,[status(thm)],[f185])).
% 1.63/1.73 thf(f185,plain,(
% 1.63/1.73 $false | (~spl4_1 | ~spl4_5)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f184])).
% 1.63/1.73 thf(f184,plain,(
% 1.63/1.73 ($true = $false) | (~spl4_1 | ~spl4_5)),
% 1.63/1.73 inference(forward_demodulation,[status(thm)],[f133,f151])).
% 1.63/1.73 thf(f151,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | ~spl4_5),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f149])).
% 1.63/1.73 thf(f149,definition,(
% 1.63/1.73 spl4_5 <=> ((sP3 @ $true) = $false)),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_5])],[avatar_definition])).
% 1.63/1.73 thf(f133,plain,(
% 1.63/1.73 ((sP3 @ $true) = $true) | ~spl4_1),
% 1.63/1.73 inference(avatar_component_clause,[status(thm)],[f131])).
% 1.63/1.73 thf(f131,definition,(
% 1.63/1.73 spl4_1 <=> ((sP3 @ $true) = $true)),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[spl4_1])],[avatar_definition])).
% 1.63/1.73 thf(f183,plain,(
% 1.63/1.73 ~spl4_2 | ~spl4_3),
% 1.63/1.73 inference(avatar_contradiction_clause,[status(thm)],[f182])).
% 1.63/1.73 thf(f182,plain,(
% 1.63/1.73 $false | (~spl4_2 | ~spl4_3)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f181])).
% 1.63/1.73 thf(f181,plain,(
% 1.63/1.73 ($true = $false) | (~spl4_2 | ~spl4_3)),
% 1.63/1.73 inference(forward_demodulation,[status(thm)],[f142,f137])).
% 1.63/1.73 thf(f180,plain,(
% 1.63/1.73 spl4_11 | spl4_10),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f37,f173,f177])).
% 1.63/1.73 thf(f37,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : ((('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1)) | ((sP3 @ $false) = $false)) )),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f36])).
% 1.63/1.73 thf(f36,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (((sP3 @ $false) = $false) | ($true = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1)) | (('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false)) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f33])).
% 1.63/1.73 thf(f33,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1)) | ($true = (~ $true)) | ((sP3 @ $false) = $false) | (('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) = $false)) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f32])).
% 1.63/1.73 thf(f32,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (((sP3 @ $false) = $false) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1)) | ($true = (~ ('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2)))) )),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f31])).
% 1.63/1.73 thf(f31,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (((sP3 @ $false) = $false) | ((('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) => $false) = $true) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ X1))) )),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f27])).
% 1.63/1.73 thf(f27,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (($true = (('const/sets/IN' @ (sK0 > $o) @ X1 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ X1))) | ((sP3 @ $false) = $false)) )),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f26])).
% 1.63/1.73 thf(f26,plain,(
% 1.63/1.73 ( ! [X1 : sK0 > $o] : (($true = ((^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0))) @ X1)) | ((sP3 @ $false) = $false)) )),
% 1.63/1.73 inference(pi_clausification,[status(thm)],[f25])).
% 1.63/1.73 thf(f25,plain,(
% 1.63/1.73 ($true = (!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0))))) | ((sP3 @ $false) = $false)),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f22])).
% 1.63/1.73 thf(f22,plain,(
% 1.63/1.73 ($false = (sP3 @ (!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0))))))),
% 1.63/1.73 introduced(definition,[new_symbols(naming,[sP3])],[inequality_splitting_name_introduction])).
% 1.63/1.73 thf(f166,plain,(
% 1.63/1.73 spl4_6 | spl4_5),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f54,f149,f153])).
% 1.63/1.73 thf(f54,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | (('const/sets/SUBSET' @ sK0 @ sK1 @ sK5) = $false)),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f53])).
% 1.63/1.73 thf(f53,plain,(
% 1.63/1.73 (('const/sets/SUBSET' @ sK0 @ sK1 @ sK5) = $false) | ($true = $false) | ((sP3 @ $true) = $false)),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f45])).
% 1.63/1.73 thf(f45,plain,(
% 1.63/1.73 ($false = (('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2) => $true)) | (('const/sets/SUBSET' @ sK0 @ sK1 @ sK5) = $false) | ((sP3 @ $true) = $false)),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f42])).
% 1.63/1.73 thf(f42,plain,(
% 1.63/1.73 ((('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5)) = $false) | ((sP3 @ $true) = $false)),
% 1.63/1.73 inference(beta_eta_normalization,[status(thm)],[f41])).
% 1.63/1.73 thf(f41,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | (((^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0))) @ sK5) = $false)),
% 1.63/1.73 inference(sigma_clausification,[status(thm)],[f24])).
% 1.63/1.73 thf(f24,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | ((!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0)))) = $false)),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f22])).
% 1.63/1.73 thf(f165,plain,(
% 1.63/1.73 spl4_5 | spl4_8),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f56,f162,f149])).
% 1.63/1.73 thf(f56,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | ($true = ('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2))),
% 1.63/1.73 inference(trivial_inequality_removal,[status(thm)],[f55])).
% 1.63/1.73 thf(f55,plain,(
% 1.63/1.73 ($true = $false) | ((sP3 @ $true) = $false) | ($true = ('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2))),
% 1.63/1.73 inference(boolean_simplification,[status(thm)],[f44])).
% 1.63/1.73 thf(f44,plain,(
% 1.63/1.73 ((sP3 @ $true) = $false) | ($false = ($false => ('const/sets/SUBSET' @ sK0 @ sK1 @ sK5))) | ($true = ('const/sets/IN' @ (sK0 > $o) @ sK5 @ sK2))),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f42])).
% 1.63/1.73 thf(f147,plain,(
% 1.63/1.73 spl4_3 | spl4_4),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f59,f144,f140])).
% 1.63/1.73 thf(f59,plain,(
% 1.63/1.73 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ($true = (sP3 @ $false))),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f23])).
% 1.63/1.73 thf(f23,plain,(
% 1.63/1.73 ($true = (sP3 @ ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))))),
% 1.63/1.73 inference(inequality_splitting,[status(thm)],[f18,f22])).
% 1.63/1.73 thf(f18,plain,(
% 1.63/1.73 ((!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0)))) != ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2)))),
% 1.63/1.73 inference(cnf_transformation,[status(thm)],[f17])).
% 1.63/1.73 thf(f17,plain,(
% 1.63/1.73 ((!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0)))) != ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2)))),
% 1.63/1.73 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f15,f16])).
% 1.63/1.73 thf(f16,plain,(
% 1.63/1.73 ? [X0 : $tType,X1 : X0 > $o,X2 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X2)) != (!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X2) => ('const/sets/SUBSET' @ X0 @ X1 @ Y0))))) => ((!! @ (sK0 > $o) @ (^[Y0 : sK0 > $o]: (('const/sets/IN' @ (sK0 > $o) @ Y0 @ sK2) => ('const/sets/SUBSET' @ sK0 @ sK1 @ Y0)))) != ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2)))),
% 1.63/1.73 introduced(definition,[],[choice_axiom])).
% 1.63/1.73 thf(f15,plain,(
% 1.63/1.73 ? [X0 : $tType,X1 : X0 > $o,X2 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X2)) != (!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X2) => ('const/sets/SUBSET' @ X0 @ X1 @ Y0)))))),
% 1.63/1.73 inference(ennf_transformation,[status(thm)],[f13])).
% 1.63/1.73 thf(f13,plain,(
% 1.63/1.73 ~! [X0 : $tType,X1 : X0 > $o,X2 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X2)) = (!! @ (X0 > $o) @ (^[Y0 : X0 > $o]: (('const/sets/IN' @ (X0 > $o) @ Y0 @ X2) => ('const/sets/SUBSET' @ X0 @ X1 @ Y0)))))),
% 1.63/1.73 inference(fool_elimination,[status(thm)],[f12])).
% 1.63/1.73 thf(f12,plain,(
% 1.63/1.73 ~! [X0 : $tType,X1 : X0 > $o,X2 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X2)) = ! [X3 : X0 > $o] : (('const/sets/IN' @ (X0 > $o) @ X3 @ X2) => ('const/sets/SUBSET' @ X0 @ X1 @ X3)))),
% 1.63/1.73 inference(rectify,[status(thm)],[f6])).
% 1.63/1.73 thf(f6,negated_conjecture,(
% 1.63/1.73 ~! [X0 : $tType,X1 : X0 > $o,X3 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X3)) = ! [X4 : X0 > $o] : (('const/sets/IN' @ (X0 > $o) @ X4 @ X3) => ('const/sets/SUBSET' @ X0 @ X1 @ X4)))),
% 1.63/1.73 inference(negated_conjecture,[status(cth)],[f5])).
% 1.63/1.73 thf(f5,conjecture,(
% 1.63/1.73 ! [X0 : $tType,X1 : X0 > $o,X3 : (X0 > $o) > $o] : (('const/sets/SUBSET' @ X0 @ X1 @ ('const/sets/INTERS' @ X0 @ X3)) = ! [X4 : X0 > $o] : (('const/sets/IN' @ (X0 > $o) @ X4 @ X3) => ('const/sets/SUBSET' @ X0 @ X1 @ X4)))),
% 1.63/1.73 file('/export/starexec/sandbox2/tmp/tmp.D5lnB8xKsG/DTF2THF_27929.p','thm/sets/SUBSET_INTERS_')).
% 1.63/1.73 thf(f138,plain,(
% 1.63/1.73 spl4_1 | spl4_2),
% 1.63/1.73 inference(avatar_split_clause,[status(thm)],[f58,f135,f131])).
% 1.63/1.73 thf(f58,plain,(
% 1.63/1.73 ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ ('const/sets/INTERS' @ sK0 @ sK2))) | ((sP3 @ $true) = $true)),
% 1.63/1.73 inference(cases_simplifying,[status(thm)],[f23])).
% 1.63/1.73 % SZS output end Proof for DTF2THF_27929
% 1.63/1.73 % (28203)------------------------------
% 1.63/1.73 % (28203)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.63/1.73 % (28203)Termination reason: Refutation
% 1.63/1.73
% 1.63/1.73 % (28203)Memory used [KB]: 6012
% 1.63/1.73 % (28203)Time elapsed: 0.094 s
% 1.63/1.73 % (28203)Instructions burned: 221 (million)
% 1.63/1.73 % (28203)------------------------------
% 1.63/1.73 % (28203)------------------------------
% 1.63/1.73 % (28135)Success in time 0.476 s
%------------------------------------------------------------------------------