%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEV449^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 : n005.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:16 AM UTC 2026
% Result : Theorem 1.37s 1.37s
% Output : Refutation 1.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 14
% Syntax : Number of formulae : 110 ( 15 unt; 0 typ; 6 def)
% Number of atoms : 801 ( 231 equ; 0 cnn)
% Maximal formula atoms : 6 ( 7 avg)
% Number of connectives : 968 ( 106 ~; 126 |; 32 &; 684 @)
% ( 10 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 102 ( 102 >; 0 *; 0 +; 0 <<)
% Number of symbols : 18 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 183 ( 0 ^; 165 !; 18 ?; 183 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_6,type,
sK0: $tType ).
thf(func_def_0,type,
'const/sets/SUBSET':
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > $o ) ).
thf(func_def_1,type,
'const/sets/PSUBSET':
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > $o ) ).
thf(func_def_2,type,
'const/sets/IN':
!>[X0: $tType] : ( X0 > ( X0 > $o ) > $o ) ).
thf(func_def_6,type,
sK1: sK0 > $o ).
thf(func_def_7,type,
sK2: sK0 > $o ).
thf(func_def_8,type,
sK3: sK0 > $o ).
thf(func_def_9,type,
sK4:
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > X0 ) ).
thf(func_def_10,type,
sK5:
!>[X0: $tType] : ( ( X0 > $o ) > ( X0 > $o ) > X0 ) ).
thf(func_def_12,type,
ph7:
!>[X0: $tType] : X0 ).
thf(f966,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f263,f488,f729,f732,f749,f753,f965]) ).
thf(f965,plain,
spl6_2,
inference(avatar_contradiction_clause,[status(thm)],[f964]) ).
thf(f964,plain,
( $false
| spl6_2 ),
inference(trivial_inequality_removal,[status(thm)],[f963]) ).
thf(f963,plain,
( ( $false = $true )
| spl6_2 ),
inference(forward_demodulation,[status(thm)],[f960,f761]) ).
thf(f761,plain,
( ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| spl6_2 ),
inference(trivial_inequality_removal,[status(thm)],[f759]) ).
thf(f759,plain,
( ( $true != $true )
| ( $false
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| spl6_2 ),
inference(superposition,[status(thm)],[f61,f51]) ).
thf(f51,plain,
! [X0: $tType,X2: X0 > $o,X1: X0] :
( ( $true
= ( X2 @ X1 ) )
| ( $false
= ( X2 @ X1 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f49]) ).
thf(f49,plain,
! [X0: $tType,X2: X0 > $o,X1: X0] :
( ( $false
= ( X2 @ X1 ) )
| ( $false = $true )
| ( $true
= ( X2 @ X1 ) ) ),
inference(superposition,[status(thm)],[f48,f47]) ).
thf(f47,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ X1 )
= $true )
| ( ( X1 @ X2 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f37,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( 'const/sets/IN' @ X0 @ X2 @ X1 )
= ( X1 @ X2 ) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
thf(f1,axiom,
! [X0: $tType,X1: X0 > $o,X2: X0] :
( ( 'const/sets/IN' @ X0 @ X2 @ X1 )
= ( X1 @ X2 ) ),
file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/IN_') ).
thf(f48,plain,
! [X0: $tType,X2: X0,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ X2 @ X1 )
= $false )
| ( ( X1 @ X2 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f61,plain,
( ( $true
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| spl6_2 ),
inference(avatar_component_clause,[status(thm)],[f60]) ).
thf(f60,definition,
( spl6_2
<=> ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) ) ),
introduced(definition,[new_symbols(naming,[spl6_2])],[avatar_definition]) ).
thf(f960,plain,
( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) ),
inference(trivial_inequality_removal,[status(thm)],[f959]) ).
thf(f959,plain,
( ( $true != $true )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) ) ),
inference(duplicate_literal_removal,[status(thm)],[f957]) ).
thf(f957,plain,
( ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f230,f41]) ).
thf(f41,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X1 )
= $true )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
thf(f30,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) )
& ( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true )
| ( ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X1 )
= $true )
& ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X2 )
!= $true ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK5])],[f28,f29]) ).
thf(f29,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ? [X4: X0] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X4 @ X1 ) )
& ( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
!= $true ) )
=> ( ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X1 )
= $true )
& ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X2 )
!= $true ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f28,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) )
& ( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true )
| ? [X4: X0] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X4 @ X1 ) )
& ( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
!= $true ) ) ) ),
inference(rectify,[status(thm)],[f27]) ).
thf(f27,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) )
& ( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true )
| ? [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= $true )
& ( $true
!= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ) ) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
thf(f16,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ! [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) )
<=> ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) ),
inference(ennf_transformation,[status(thm)],[f15]) ).
thf(f15,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true )
<=> ! [X3: X0] :
( ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= $true )
=> ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ) ),
inference(fool_elimination,[status(thm)],[f14]) ).
thf(f14,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)],[f3]) ).
thf(f3,axiom,
! [X0: $tType,X2: X0 > $o,X3: X0 > $o] :
( ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 )
= ( ! [X4: X0] :
( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
=> ( 'const/sets/IN' @ X0 @ X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/SUBSET_') ).
thf(f230,plain,
! [X0: sK0 > $o] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK5 @ sK0 @ sK3 @ X0 ) @ sK1 )
!= $true )
| ( ( 'const/sets/SUBSET' @ sK0 @ X0 @ sK3 )
= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f224]) ).
thf(f224,plain,
! [X0: sK0 > $o] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK5 @ sK0 @ sK3 @ X0 ) @ sK1 )
!= $true )
| ( ( 'const/sets/SUBSET' @ sK0 @ X0 @ sK3 )
= $true )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f126,f149]) ).
thf(f149,plain,
! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ X0 @ sK1 )
!= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f146]) ).
thf(f146,plain,
! [X0: sK0] :
( ( $true
= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( $true != $true )
| ( ( 'const/sets/IN' @ sK0 @ X0 @ sK1 )
!= $true ) ),
inference(superposition,[status(thm)],[f110,f36]) ).
thf(f36,plain,
( ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK2 )
= $true ),
inference(cnf_transformation,[status(thm)],[f22]) ).
thf(f22,plain,
( ( ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK2 )
= $true )
& ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK2 @ sK3 ) )
& ( $true
!= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK3 ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f18,f21]) ).
thf(f21,plain,
( ? [X0: $tType,X1: X0 > $o,X2: X0 > $o,X3: X0 > $o] :
( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
& ( ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 )
= $true )
& ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X3 ) ) )
=> ( ( ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK2 )
= $true )
& ( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK2 @ sK3 ) )
& ( $true
!= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK3 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f18,plain,
? [X0: $tType,X1: X0 > $o,X2: X0 > $o,X3: X0 > $o] :
( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
& ( ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 )
= $true )
& ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X3 ) ) ),
inference(flattening,[status(thm)],[f17]) ).
thf(f17,plain,
? [X0: $tType,X1: X0 > $o,X2: X0 > $o,X3: X0 > $o] :
( ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X3 ) )
& ( ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 )
= $true )
& ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(ennf_transformation,[status(thm)],[f13]) ).
thf(f13,plain,
~ ! [X0: $tType,X1: X0 > $o,X2: X0 > $o,X3: X0 > $o] :
( ( ( ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 )
= $true )
& ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) )
=> ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X3 ) ) ),
inference(fool_elimination,[status(thm)],[f12]) ).
thf(f12,plain,
~ ! [X0: $tType,X1: X0 > $o,X2: X0 > $o,X3: X0 > $o] :
( ( ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 )
& ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 ) )
=> ( 'const/sets/PSUBSET' @ X0 @ X1 @ X3 ) ),
inference(rectify,[status(thm)],[f6]) ).
thf(f6,negated_conjecture,
~ ! [X0: $tType,X2: X0 > $o,X3: X0 > $o,X4: X0 > $o] :
( ( ( 'const/sets/PSUBSET' @ X0 @ X2 @ X3 )
& ( 'const/sets/SUBSET' @ X0 @ X3 @ X4 ) )
=> ( 'const/sets/PSUBSET' @ X0 @ X2 @ X4 ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
thf(f5,conjecture,
! [X0: $tType,X2: X0 > $o,X3: X0 > $o,X4: X0 > $o] :
( ( ( 'const/sets/PSUBSET' @ X0 @ X2 @ X3 )
& ( 'const/sets/SUBSET' @ X0 @ X3 @ X4 ) )
=> ( 'const/sets/PSUBSET' @ X0 @ X2 @ X4 ) ),
file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/PSUBSET_SUBSET_TRANS_') ).
thf(f110,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f107]) ).
thf(f107,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
| ( $true != $true )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true ) ),
inference(superposition,[status(thm)],[f42,f31]) ).
thf(f31,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true )
| ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
thf(f20,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
| ( X1 = X2 )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) )
& ( ( ( X1 != X2 )
& ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) )
| ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) ) ),
inference(flattening,[status(thm)],[f19]) ).
thf(f19,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
| ( X1 = X2 )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) )
& ( ( ( X1 != X2 )
& ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) )
| ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
<=> ( ( X1 != X2 )
& ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) ) ),
inference(fool_elimination,[status(thm)],[f10]) ).
thf(f10,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 )
= ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 ) )
& ( X1 != X2 ) ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
! [X0: $tType,X2: X0 > $o,X3: X0 > $o] :
( ( ( 'const/sets/PSUBSET' @ X0 @ X2 @ X3 )
= ( 'const/sets/SUBSET' @ X0 @ X2 @ X3 ) )
& ( X2 != X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/PSUBSET_') ).
thf(f42,plain,
! [X0: $tType,X2: X0 > $o,X3: X0,X1: X0 > $o] :
( ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true )
| ( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= $true )
| ( $true
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
thf(f126,plain,
! [X0: sK0 > $o] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK5 @ sK0 @ sK3 @ X0 ) @ sK2 )
!= $true )
| ( ( 'const/sets/SUBSET' @ sK0 @ X0 @ sK3 )
= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f123]) ).
thf(f123,plain,
! [X0: sK0 > $o] :
( ( ( 'const/sets/IN' @ sK0 @ ( sK5 @ sK0 @ sK3 @ X0 ) @ sK2 )
!= $true )
| ( ( 'const/sets/SUBSET' @ sK0 @ X0 @ sK3 )
= $true )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f40,f111]) ).
thf(f111,plain,
! [X0: sK0] :
( ( ( 'const/sets/IN' @ sK0 @ X0 @ sK3 )
= $true )
| ( $true
!= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f106]) ).
thf(f106,plain,
! [X0: sK0] :
( ( $true
!= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( ( 'const/sets/IN' @ sK0 @ X0 @ sK3 )
= $true )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f42,f35]) ).
thf(f35,plain,
( $true
= ( 'const/sets/SUBSET' @ sK0 @ sK2 @ sK3 ) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
thf(f40,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ ( sK5 @ X0 @ X2 @ X1 ) @ X2 )
!= $true )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
thf(f753,plain,
( ~ spl6_2
| spl6_1 ),
inference(avatar_split_clause,[status(thm)],[f133,f57,f60]) ).
thf(f57,definition,
( spl6_1
<=> ( sK3 = sK1 ) ),
introduced(definition,[new_symbols(naming,[spl6_1])],[avatar_definition]) ).
thf(f133,plain,
( ( $true
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| ( sK3 = sK1 ) ),
inference(trivial_inequality_removal,[status(thm)],[f128]) ).
thf(f128,plain,
( ( $true
!= ( 'const/sets/SUBSET' @ sK0 @ sK1 @ sK3 ) )
| ( sK3 = sK1 )
| ( $false = $true ) ),
inference(superposition,[status(thm)],[f100,f33]) ).
thf(f33,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) )
| ( X1 = X2 )
| ( ( 'const/sets/SUBSET' @ X0 @ X1 @ X2 )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
thf(f100,plain,
( $false
= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK3 ) ),
inference(trivial_inequality_removal,[status(thm)],[f90]) ).
thf(f90,plain,
( ( $false
= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK3 ) )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f34,f51]) ).
thf(f34,plain,
( $true
!= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK3 ) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
thf(f749,plain,
~ spl6_8,
inference(avatar_contradiction_clause,[status(thm)],[f748]) ).
thf(f748,plain,
( $false
| ~ spl6_8 ),
inference(subsumption_resolution,[status(thm)],[f733,f43]) ).
thf(f43,plain,
! [X0: $tType,X2: X0 > $o] :
( ( 'const/sets/PSUBSET' @ X0 @ X2 @ X2 )
!= $true ),
inference(equality_resolution,[status(thm)],[f32]) ).
thf(f32,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( X1 != X2 )
| ( $true
!= ( 'const/sets/PSUBSET' @ X0 @ X1 @ X2 ) ) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
thf(f733,plain,
( ( $true
= ( 'const/sets/PSUBSET' @ sK0 @ sK1 @ sK1 ) )
| ~ spl6_8 ),
inference(backward_demodulation,[status(thm)],[f36,f545]) ).
thf(f545,plain,
( ( sK1 = sK2 )
| ~ spl6_8 ),
inference(avatar_component_clause,[status(thm)],[f544]) ).
thf(f544,definition,
( spl6_8
<=> ( sK1 = sK2 ) ),
introduced(definition,[new_symbols(naming,[spl6_8])],[avatar_definition]) ).
thf(f732,plain,
( spl6_8
| ~ spl6_1
| ~ spl6_5 ),
inference(avatar_split_clause,[status(thm)],[f731,f256,f57,f544]) ).
thf(f256,definition,
( spl6_5
<=> ( sK3 = sK2 ) ),
introduced(definition,[new_symbols(naming,[spl6_5])],[avatar_definition]) ).
thf(f731,plain,
( ( sK1 = sK2 )
| ~ spl6_1
| ~ spl6_5 ),
inference(forward_demodulation,[status(thm)],[f257,f58]) ).
thf(f58,plain,
( ( sK3 = sK1 )
| ~ spl6_1 ),
inference(avatar_component_clause,[status(thm)],[f57]) ).
thf(f257,plain,
( ( sK3 = sK2 )
| ~ spl6_5 ),
inference(avatar_component_clause,[status(thm)],[f256]) ).
thf(f729,plain,
( ~ spl6_1
| spl6_6
| ~ spl6_7 ),
inference(avatar_contradiction_clause,[status(thm)],[f728]) ).
thf(f728,plain,
( $false
| ~ spl6_1
| spl6_6
| ~ spl6_7 ),
inference(trivial_inequality_removal,[status(thm)],[f717]) ).
thf(f717,plain,
( ( $false = $true )
| ~ spl6_1
| spl6_6
| ~ spl6_7 ),
inference(backward_demodulation,[status(thm)],[f564,f570]) ).
thf(f570,plain,
( ( $false
= ( sK1 @ ( sK4 @ sK0 @ sK1 @ sK2 ) ) )
| ~ spl6_1
| spl6_6 ),
inference(forward_demodulation,[status(thm)],[f425,f58]) ).
thf(f425,plain,
( ( ( sK1 @ ( sK4 @ sK0 @ sK3 @ sK2 ) )
= $false )
| spl6_6 ),
inference(trivial_inequality_removal,[status(thm)],[f422]) ).
thf(f422,plain,
( ( ( sK1 @ ( sK4 @ sK0 @ sK3 @ sK2 ) )
= $false )
| ( $true != $true )
| spl6_6 ),
inference(superposition,[status(thm)],[f260,f47]) ).
thf(f260,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK1 )
!= $true )
| spl6_6 ),
inference(avatar_component_clause,[status(thm)],[f259]) ).
thf(f259,definition,
( spl6_6
<=> ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK1 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl6_6])],[avatar_definition]) ).
thf(f564,plain,
( ( $true
= ( sK1 @ ( sK4 @ sK0 @ sK1 @ sK2 ) ) )
| ~ spl6_1
| ~ spl6_7 ),
inference(forward_demodulation,[status(thm)],[f487,f58]) ).
thf(f487,plain,
( ( $true
= ( sK3 @ ( sK4 @ sK0 @ sK3 @ sK2 ) ) )
| ~ spl6_7 ),
inference(avatar_component_clause,[status(thm)],[f486]) ).
thf(f486,definition,
( spl6_7
<=> ( $true
= ( sK3 @ ( sK4 @ sK0 @ sK3 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl6_7])],[avatar_definition]) ).
thf(f488,plain,
( spl6_5
| spl6_7 ),
inference(avatar_split_clause,[status(thm)],[f484,f486,f256]) ).
thf(f484,plain,
( ( $true
= ( sK3 @ ( sK4 @ sK0 @ sK3 @ sK2 ) ) )
| ( sK3 = sK2 ) ),
inference(trivial_inequality_removal,[status(thm)],[f483]) ).
thf(f483,plain,
( ( sK3 = sK2 )
| ( $true
= ( sK3 @ ( sK4 @ sK0 @ sK3 @ sK2 ) ) )
| ( $true != $true ) ),
inference(equality_factoring,[status(thm)],[f390]) ).
thf(f390,plain,
! [X0: sK0 > $o] :
( ( ( sK3 @ ( sK4 @ sK0 @ X0 @ sK2 ) )
= $true )
| ( ( X0 @ ( sK4 @ sK0 @ X0 @ sK2 ) )
= $true )
| ( sK2 = X0 ) ),
inference(trivial_inequality_removal,[status(thm)],[f377]) ).
thf(f377,plain,
! [X0: sK0 > $o] :
( ( ( sK3 @ ( sK4 @ sK0 @ X0 @ sK2 ) )
= $true )
| ( $true != $true )
| ( ( X0 @ ( sK4 @ sK0 @ X0 @ sK2 ) )
= $true )
| ( sK2 = X0 ) ),
inference(superposition,[status(thm)],[f124,f158]) ).
thf(f158,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X1 @ X2 ) @ X2 )
= $true )
| ( X1 = X2 )
| ( ( X1 @ ( sK4 @ X0 @ X1 @ X2 ) )
= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f153]) ).
thf(f153,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X1 @ X2 ) @ X2 )
= $true )
| ( ( X1 @ ( sK4 @ X0 @ X1 @ X2 ) )
= $true )
| ( X1 = X2 )
| ( $false = $true ) ),
inference(superposition,[status(thm)],[f45,f48]) ).
thf(f45,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $true
= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X2 ) )
| ( X1 = X2 )
| ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X1 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f38]) ).
thf(f38,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( X1 = X2 )
| ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X1 )
!= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X2 ) ) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
thf(f26,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( X1 != X2 ) )
& ( ( X1 = X2 )
| ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X1 )
!= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X2 ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK4])],[f24,f25]) ).
thf(f25,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ? [X4: X0] :
( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
!= ( 'const/sets/IN' @ X0 @ X4 @ X1 ) )
=> ( ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X1 )
!= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X2 ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f24,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( X1 != X2 ) )
& ( ( X1 = X2 )
| ? [X4: X0] :
( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
!= ( 'const/sets/IN' @ X0 @ X4 @ X1 ) ) ) ),
inference(rectify,[status(thm)],[f23]) ).
thf(f23,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
| ( X1 != X2 ) )
& ( ( X1 = X2 )
| ? [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
!= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
thf(f9,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) )
<=> ( X1 = X2 ) ),
inference(fool_elimination,[status(thm)],[f8]) ).
thf(f8,plain,
! [X0: $tType,X1: X0 > $o,X2: X0 > $o] :
( ( X1 = X2 )
= ( ! [X3: X0] :
( ( 'const/sets/IN' @ X0 @ X3 @ X1 )
= ( 'const/sets/IN' @ X0 @ X3 @ X2 ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,axiom,
! [X0: $tType,X2: X0 > $o,X3: X0 > $o] :
( ( X2 = X3 )
= ( ! [X4: X0] :
( ( 'const/sets/IN' @ X0 @ X4 @ X2 )
= ( 'const/sets/IN' @ X0 @ X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/EXTENSION_') ).
thf(f124,plain,
! [X0: sK0] :
( ( $true
!= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( $true
= ( sK3 @ X0 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f121]) ).
thf(f121,plain,
! [X0: sK0] :
( ( $true
!= ( 'const/sets/IN' @ sK0 @ X0 @ sK2 ) )
| ( $false = $true )
| ( $true
= ( sK3 @ X0 ) ) ),
inference(superposition,[status(thm)],[f111,f48]) ).
thf(f263,plain,
( spl6_5
| ~ spl6_6 ),
inference(avatar_split_clause,[status(thm)],[f262,f259,f256]) ).
thf(f262,plain,
( ( sK3 = sK2 )
| ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK1 )
!= $true ) ),
inference(subsumption_resolution,[status(thm)],[f251,f149]) ).
thf(f251,plain,
( ( $true
!= ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK2 ) )
| ( sK3 = sK2 )
| ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK1 )
!= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f244]) ).
thf(f244,plain,
( ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK1 )
!= $true )
| ( $false = $true )
| ( sK3 = sK2 )
| ( $true
!= ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ sK2 ) @ sK2 ) ) ),
inference(superposition,[status(thm)],[f149,f173]) ).
thf(f173,plain,
! [X0: sK0 > $o] :
( ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ X0 ) @ X0 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ X0 ) @ sK2 )
!= $true )
| ( sK3 = X0 ) ),
inference(trivial_inequality_removal,[status(thm)],[f168]) ).
thf(f168,plain,
! [X0: sK0 > $o] :
( ( $false = $true )
| ( sK3 = X0 )
| ( $false
= ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ X0 ) @ X0 ) )
| ( ( 'const/sets/IN' @ sK0 @ ( sK4 @ sK0 @ sK3 @ X0 ) @ sK2 )
!= $true ) ),
inference(superposition,[status(thm)],[f111,f46]) ).
thf(f46,plain,
! [X0: $tType,X2: X0 > $o,X1: X0 > $o] :
( ( $false
= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X2 ) )
| ( $false
= ( 'const/sets/IN' @ X0 @ ( sK4 @ X0 @ X2 @ X1 ) @ X1 ) )
| ( X1 = X2 ) ),
inference(binary_proxy_clausification,[status(thm)],[f38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEV449^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.13/0.31 % Computer : n005.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Tue Feb 24 12:46:59 EST 2026
% 0.13/0.31 % CPUTime :
% 0.13/0.31 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.41 ---- Original DTF file ---
% 0.15/0.41 thf(spec,logic,$$dhol).
% 0.15/0.41 %------------------------------------------------------------------------------
% 0.15/0.41 % File : SEV449^1 : TPTP v9.2.1. Released v7.0.0.
% 0.15/0.41 % Domain : Analysis
% 0.15/0.41 % Problem : PSUBSET_SUBSET_TRANS
% 0.15/0.41 % Version : Especial.
% 0.15/0.41 % English :
% 0.15/0.41
% 0.15/0.41 % Refs : [Kal16] Kalisyk (2016), Email to Geoff Sutcliffe
% 0.15/0.41 % Source : [Kal16]
% 0.15/0.41 % Names : PSUBSET_SUBSET_TRANS_.p [Kal16]
% 0.15/0.41
% 0.15/0.41 % Status : Theorem
% 0.15/0.41 % Rating : 0.00 v7.2.0, 0.25 v7.1.0
% 0.15/0.41 % Syntax : Number of formulae : 8 ( 4 unt; 3 typ; 0 def)
% 0.15/0.41 % Number of atoms : 18 ( 7 equ; 0 cnn)
% 0.15/0.41 % Maximal formula atoms : 3 ( 3 avg)
% 0.15/0.41 % Number of connectives : 39 ( 1 ~; 0 |; 2 &; 34 @)
% 0.15/0.41 % ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% 0.15/0.41 % Maximal formula depth : 10 ( 5 avg)
% 0.15/0.41 % Number of types : 1 ( 0 usr)
% 0.15/0.41 % Number of type conns : 21 ( 21 >; 0 *; 0 +; 0 <<)
% 0.15/0.41 % Number of symbols : 4 ( 3 usr; 0 con; 2-3 aty)
% 0.15/0.41 % Number of variables : 21 ( 0 ^; 18 !; 0 ?; 21 :)
% 0.15/0.41 % ( 3 !>; 0 ?*; 0 @-; 0 @+)
% 0.15/0.41 % SPC : TH1_THM_EQU_NAR
% 0.15/0.41
% 0.15/0.41 % Comments : Exported from core HOL Light.
% 0.15/0.41 %------------------------------------------------------------------------------
% 0.15/0.41 thf('thf_const_const/sets/SUBSET',type,
% 0.15/0.41 'const/sets/SUBSET':
% 0.15/0.41 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 0.15/0.41
% 0.15/0.41 thf('thf_const_const/sets/PSUBSET',type,
% 0.15/0.41 'const/sets/PSUBSET':
% 0.15/0.41 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 0.15/0.41
% 0.15/0.41 thf('thf_const_const/sets/IN',type,
% 0.15/0.41 'const/sets/IN':
% 0.15/0.41 !>[A: $tType] : ( A > ( A > $o ) > $o ) ).
% 0.15/0.41
% 0.15/0.41 thf('thm/sets/IN_',axiom,
% 0.15/0.41 ! [A: $tType,P: A > $o,A0: A] :
% 0.15/0.41 ( ( 'const/sets/IN' @ A @ A0 @ P )
% 0.15/0.41 = ( P @ A0 ) ) ).
% 0.15/0.41
% 0.15/0.41 thf('thm/sets/EXTENSION_',axiom,
% 0.15/0.41 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 0.15/0.41 ( ( A0 = A1 )
% 0.15/0.41 = ( ! [A2: A] :
% 0.15/0.41 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 0.15/0.41 = ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 0.15/0.41
% 0.15/0.41 thf('thm/sets/SUBSET_',axiom,
% 0.15/0.41 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 0.15/0.41 ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 0.15/0.41 = ( ! [A2: A] :
% 0.15/0.41 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 0.15/0.41 => ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 0.15/0.41
% 0.15/0.41 thf('thm/sets/PSUBSET_',axiom,
% 0.15/0.41 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 0.15/0.41 ( ( 'const/sets/PSUBSET' @ A @ A0 @ A1 )
% 0.15/0.41 = ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 0.15/0.41 & ( A0 != A1 ) ) ) ).
% 0.15/0.41
% 0.15/0.41 thf('thm/sets/PSUBSET_SUBSET_TRANS_',conjecture,
% 0.15/0.41 ! [A: $tType,A0: A > $o,A1: A > $o,A2: A > $o] :
% 0.15/0.41 ( ( ( 'const/sets/PSUBSET' @ A @ A0 @ A1 )
% 0.15/0.41 & ( 'const/sets/SUBSET' @ A @ A1 @ A2 ) )
% 0.15/0.41 => ( 'const/sets/PSUBSET' @ A @ A0 @ A2 ) ) ).
% 0.15/0.41
% 0.15/0.41 %------------------------------------------------------------------------------
% 0.15/0.41 ------------------------
% 1.21/1.11 ---- Embedded in THF ---
% 1.21/1.11 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.21/1.11 %%% Generated on Tue Feb 24 12:47:00 EST 2026
% 1.21/1.11 %%% using '$$dhol' embedding, version 1.3.0.
% 1.21/1.11 %%% Logic specification used:
% 1.21/1.11 %%% thf(spec, logic, $$dhol).
% 1.21/1.11
% 1.21/1.11 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2DTF5419.p
% See solution above
% 1.21/1.11 ------------------------
% 1.21/1.12 ---- Cleaned THF ---
% 1.21/1.12 thf('thf_const_const/sets/SUBSET',type,
% 1.21/1.12 'const/sets/SUBSET':
% 1.21/1.12 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 1.21/1.12
% 1.21/1.12 thf('thf_const_const/sets/PSUBSET',type,
% 1.21/1.12 'const/sets/PSUBSET':
% 1.21/1.12 !>[A: $tType] : ( ( A > $o ) > ( A > $o ) > $o ) ).
% 1.21/1.12
% 1.21/1.12 thf('thf_const_const/sets/IN',type,
% 1.21/1.12 'const/sets/IN':
% 1.21/1.12 !>[A: $tType] : ( A > ( A > $o ) > $o ) ).
% 1.21/1.12
% 1.21/1.12 thf('thm/sets/IN_',axiom,
% 1.21/1.12 ! [A: $tType,P: A > $o,A0: A] :
% 1.21/1.12 ( ( 'const/sets/IN' @ A @ A0 @ P )
% 1.21/1.12 = ( P @ A0 ) ) ).
% 1.21/1.12
% 1.21/1.12 thf('thm/sets/EXTENSION_',axiom,
% 1.21/1.12 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 1.21/1.12 ( ( A0 = A1 )
% 1.21/1.12 = ( ! [A2: A] :
% 1.21/1.12 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 1.21/1.12 = ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 1.21/1.12
% 1.21/1.12 thf('thm/sets/SUBSET_',axiom,
% 1.21/1.12 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 1.21/1.12 ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 1.21/1.12 = ( ! [A2: A] :
% 1.21/1.12 ( ( 'const/sets/IN' @ A @ A2 @ A0 )
% 1.21/1.12 => ( 'const/sets/IN' @ A @ A2 @ A1 ) ) ) ) ).
% 1.21/1.12
% 1.21/1.12 thf('thm/sets/PSUBSET_',axiom,
% 1.21/1.12 ! [A: $tType,A0: A > $o,A1: A > $o] :
% 1.21/1.12 ( ( 'const/sets/PSUBSET' @ A @ A0 @ A1 )
% 1.21/1.12 = ( ( 'const/sets/SUBSET' @ A @ A0 @ A1 )
% 1.21/1.12 & ( A0 != A1 ) ) ) ).
% 1.21/1.12
% 1.21/1.12 thf('thm/sets/PSUBSET_SUBSET_TRANS_',conjecture,
% 1.21/1.12 ! [A: $tType,A0: A > $o,A1: A > $o,A2: A > $o] :
% 1.21/1.12 ( ( ( 'const/sets/PSUBSET' @ A @ A0 @ A1 )
% 1.21/1.12 & ( 'const/sets/SUBSET' @ A @ A1 @ A2 ) )
% 1.21/1.12 => ( 'const/sets/PSUBSET' @ A @ A0 @ A2 ) ) ).
% 1.21/1.12 ------------------------
% 1.37/1.13 % (5517)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/183Mi)
% 1.37/1.14 % (5518)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_5419 for (2999ds/4Mi)
% 1.37/1.14 % (5519)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_5419 for (2999ds/27Mi)
% 1.37/1.14 % (5520)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/2Mi)
% 1.37/1.14 % (5522)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_5419 for (2999ds/275Mi)
% 1.37/1.14 % (5521)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_5419 for (2999ds/2Mi)
% 1.37/1.14 % (5523)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/18Mi)
% 1.37/1.14 % (5520)Instruction limit reached!
% 1.37/1.14 % (5520)------------------------------
% 1.37/1.14 % (5520)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.14 % (5520)Termination reason: Unknown
% 1.37/1.14 % (5520)Termination phase: Naming
% 1.37/1.14 % (5521)Instruction limit reached!
% 1.37/1.14 % (5521)------------------------------
% 1.37/1.14 % (5521)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.14 % (5521)Termination reason: Unknown
% 1.37/1.14 % (5521)Termination phase: shuffling
% 1.37/1.14
% 1.37/1.14 % (5521)Memory used [KB]: 895
% 1.37/1.14 % (5521)Time elapsed: 0.002 s
% 1.37/1.14 % (5521)Instructions burned: 2 (million)
% 1.37/1.14 % (5521)------------------------------
% 1.37/1.14 % (5521)------------------------------
% 1.37/1.14
% 1.37/1.14 % (5520)Memory used [KB]: 895
% 1.37/1.14 % (5520)Time elapsed: 0.002 s
% 1.37/1.14 % (5520)Instructions burned: 2 (million)
% 1.37/1.14 % (5520)------------------------------
% 1.37/1.14 % (5520)------------------------------
% 1.37/1.14 % (5518)Instruction limit reached!
% 1.37/1.14 % (5518)------------------------------
% 1.37/1.14 % (5518)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.14 % (5518)Termination reason: Unknown
% 1.37/1.14 % (5518)Termination phase: Saturation
% 1.37/1.14
% 1.37/1.14 % (5518)Memory used [KB]: 5500
% 1.37/1.14 % (5518)Time elapsed: 0.004 s
% 1.37/1.14 % (5518)Instructions burned: 5 (million)
% 1.37/1.14 % (5518)------------------------------
% 1.37/1.14 % (5518)------------------------------
% 1.37/1.14 % (5522)Refutation not found, incomplete strategy
% 1.37/1.14 % (5522)------------------------------
% 1.37/1.14 % (5522)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.14 % (5522)Termination reason: Refutation not found, incomplete strategy
% 1.37/1.14
% 1.37/1.14
% 1.37/1.14 % (5522)Memory used [KB]: 5500
% 1.37/1.14 % (5522)Time elapsed: 0.006 s
% 1.37/1.14 % (5522)Instructions burned: 9 (million)
% 1.37/1.14 % (5522)------------------------------
% 1.37/1.14 % (5522)------------------------------
% 1.37/1.15 % (5523)Instruction limit reached!
% 1.37/1.15 % (5523)------------------------------
% 1.37/1.15 % (5523)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.15 % (5523)Termination reason: Unknown
% 1.37/1.15 % (5523)Termination phase: Saturation
% 1.37/1.15
% 1.37/1.15 % (5523)Memory used [KB]: 5628
% 1.37/1.15 % (5523)Time elapsed: 0.011 s
% 1.37/1.15 % (5523)Instructions burned: 18 (million)
% 1.37/1.15 % (5523)------------------------------
% 1.37/1.15 % (5523)------------------------------
% 1.37/1.15 % (5519)Instruction limit reached!
% 1.37/1.15 % (5519)------------------------------
% 1.37/1.15 % (5519)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.15 % (5519)Termination reason: Unknown
% 1.37/1.15 % (5519)Termination phase: Saturation
% 1.37/1.15
% 1.37/1.15 % (5519)Memory used [KB]: 5628
% 1.37/1.15 % (5519)Time elapsed: 0.016 s
% 1.37/1.15 % (5519)Instructions burned: 28 (million)
% 1.37/1.15 % (5519)------------------------------
% 1.37/1.15 % (5519)------------------------------
% 1.37/1.15 % (5524)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/3Mi)
% 1.37/1.15 % (5525)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_5419 for (2999ds/37Mi)
% 1.37/1.15 % Exception at run slice level
% 1.37/1.15 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.37/1.15 % (5524)Instruction limit reached!
% 1.37/1.15 % (5524)------------------------------
% 1.37/1.15 % (5524)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.15 % (5524)Termination reason: Unknown
% 1.37/1.15 % (5524)Termination phase: Saturation
% 1.37/1.15
% 1.37/1.15 % (5524)Memory used [KB]: 5500
% 1.37/1.15 % (5524)Time elapsed: 0.003 s
% 1.37/1.15 % (5524)Instructions burned: 4 (million)
% 1.37/1.15 % (5524)------------------------------
% 1.37/1.15 % (5524)------------------------------
% 1.37/1.15 % (5526)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_5419 for (2999ds/15Mi)
% 1.37/1.16 % (5527)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_5419 for (2999ds/3Mi)
% 1.37/1.16 % (5527)Instruction limit reached!
% 1.37/1.16 % (5527)------------------------------
% 1.37/1.16 % (5527)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.16 % (5527)Termination reason: Unknown
% 1.37/1.16 % (5527)Termination phase: Saturation
% 1.37/1.16
% 1.37/1.16 % (5527)Memory used [KB]: 5500
% 1.37/1.16 % (5527)Time elapsed: 0.004 s
% 1.37/1.16 % (5527)Instructions burned: 4 (million)
% 1.37/1.16 % (5527)------------------------------
% 1.37/1.16 % (5527)------------------------------
% 1.37/1.16 % (5535)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/7Mi)
% 1.37/1.16 % (5528)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_5419 for (2999ds/1041Mi)
% 1.37/1.16 % (5526)Instruction limit reached!
% 1.37/1.16 % (5526)------------------------------
% 1.37/1.16 % (5526)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.16 % (5526)Termination reason: Unknown
% 1.37/1.16 % (5526)Termination phase: Saturation
% 1.37/1.16
% 1.37/1.16 % (5526)Memory used [KB]: 5628
% 1.37/1.16 % (5526)Time elapsed: 0.010 s
% 1.37/1.16 % (5526)Instructions burned: 15 (million)
% 1.37/1.16 % (5526)------------------------------
% 1.37/1.16 % (5526)------------------------------
% 1.37/1.16 % Exception at run slice level
% 1.37/1.16 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.37/1.16 % (5537)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_5419 for (2999ds/3Mi)
% 1.37/1.16 % (5537)Instruction limit reached!
% 1.37/1.16 % (5537)------------------------------
% 1.37/1.16 % (5537)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.16 % (5537)Termination reason: Unknown
% 1.37/1.16 % (5537)Termination phase: Saturation
% 1.37/1.16
% 1.37/1.16 % (5537)Memory used [KB]: 5500
% 1.37/1.16 % (5537)Time elapsed: 0.002 s
% 1.37/1.16 % (5537)Instructions burned: 3 (million)
% 1.37/1.16 % (5537)------------------------------
% 1.37/1.16 % (5537)------------------------------
% 1.37/1.16 % (5535)Instruction limit reached!
% 1.37/1.16 % (5535)------------------------------
% 1.37/1.16 % (5535)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.16 % (5535)Termination reason: Unknown
% 1.37/1.16 % (5535)Termination phase: Saturation
% 1.37/1.16
% 1.37/1.16 % (5535)Memory used [KB]: 1023
% 1.37/1.16 % (5535)Time elapsed: 0.005 s
% 1.37/1.16 % (5535)Instructions burned: 8 (million)
% 1.37/1.16 % (5535)------------------------------
% 1.37/1.16 % (5535)------------------------------
% 1.37/1.17 % (5536)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/16Mi)
% 1.37/1.17 % (5541)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/4Mi)
% 1.37/1.17 % (5536)Instruction limit reached!
% 1.37/1.17 % (5536)------------------------------
% 1.37/1.17 % (5536)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.17 % (5536)Termination reason: Unknown
% 1.37/1.17 % (5536)Termination phase: Saturation
% 1.37/1.17
% 1.37/1.17 % (5536)Memory used [KB]: 5756
% 1.37/1.17 % (5536)Time elapsed: 0.008 s
% 1.37/1.17 % (5536)Instructions burned: 18 (million)
% 1.37/1.17 % (5536)------------------------------
% 1.37/1.17 % (5536)------------------------------
% 1.37/1.17 % (5541)Instruction limit reached!
% 1.37/1.17 % (5541)------------------------------
% 1.37/1.17 % (5541)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.17 % (5541)Termination reason: Unknown
% 1.37/1.17 % (5541)Termination phase: Saturation
% 1.37/1.17
% 1.37/1.17 % (5541)Memory used [KB]: 5500
% 1.37/1.17 % (5541)Time elapsed: 0.003 s
% 1.37/1.17 % (5541)Instructions burned: 6 (million)
% 1.37/1.17 % (5541)------------------------------
% 1.37/1.17 % (5541)------------------------------
% 1.37/1.18 % (5538)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_5419 for (2999ds/3Mi)
% 1.37/1.18 % (5538)Instruction limit reached!
% 1.37/1.18 % (5538)------------------------------
% 1.37/1.18 % (5538)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.18 % (5538)Termination reason: Unknown
% 1.37/1.18 % (5538)Termination phase: Saturation
% 1.37/1.18
% 1.37/1.18 % (5538)Memory used [KB]: 1023
% 1.37/1.18 % (5538)Time elapsed: 0.003 s
% 1.37/1.18 % (5538)Instructions burned: 3 (million)
% 1.37/1.18 % (5538)------------------------------
% 1.37/1.18 % (5538)------------------------------
% 1.37/1.18 % (5539)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/7Mi)
% 1.37/1.18 % (5540)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/3Mi)
% 1.37/1.18 % Exception at run slice level
% 1.37/1.18 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.37/1.18 % (5542)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/18Mi)
% 1.37/1.18 % (5539)Instruction limit reached!
% 1.37/1.18 % (5539)------------------------------
% 1.37/1.18 % (5539)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.18 % (5539)Termination reason: Unknown
% 1.37/1.18 % (5539)Termination phase: Saturation
% 1.37/1.18
% 1.37/1.18 % (5539)Memory used [KB]: 5500
% 1.37/1.18 % (5539)Time elapsed: 0.005 s
% 1.37/1.18 % (5539)Instructions burned: 7 (million)
% 1.37/1.18 % (5539)------------------------------
% 1.37/1.18 % (5539)------------------------------
% 1.37/1.18 % (5543)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/710Mi)
% 1.37/1.18 % (5544)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/6Mi)
% 1.37/1.19 % (5544)Instruction limit reached!
% 1.37/1.19 % (5544)------------------------------
% 1.37/1.19 % (5544)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.19 % (5544)Termination reason: Unknown
% 1.37/1.19 % (5544)Termination phase: Saturation
% 1.37/1.19
% 1.37/1.19 % (5544)Memory used [KB]: 5500
% 1.37/1.19 % (5544)Time elapsed: 0.003 s
% 1.37/1.19 % (5544)Instructions burned: 6 (million)
% 1.37/1.19 % (5544)------------------------------
% 1.37/1.19 % (5544)------------------------------
% 1.37/1.19 % (5545)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_5419 for (2999ds/902Mi)
% 1.37/1.19 % (5517)Instruction limit reached!
% 1.37/1.19 % (5517)------------------------------
% 1.37/1.19 % (5517)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.19 % (5517)Termination reason: Unknown
% 1.37/1.19 % (5517)Termination phase: Saturation
% 1.37/1.19
% 1.37/1.19 % (5517)Memory used [KB]: 6780
% 1.37/1.19 % (5517)Time elapsed: 0.059 s
% 1.37/1.19 % (5517)Instructions burned: 186 (million)
% 1.37/1.19 % (5517)------------------------------
% 1.37/1.19 % (5517)------------------------------
% 1.37/1.19 % (5542)Instruction limit reached!
% 1.37/1.19 % (5542)------------------------------
% 1.37/1.19 % (5542)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.19 % (5542)Termination reason: Unknown
% 1.37/1.19 % (5542)Termination phase: Saturation
% 1.37/1.19
% 1.37/1.19 % (5542)Memory used [KB]: 5628
% 1.37/1.19 % (5542)Time elapsed: 0.011 s
% 1.37/1.19 % (5542)Instructions burned: 18 (million)
% 1.37/1.19 % (5542)------------------------------
% 1.37/1.19 % (5542)------------------------------
% 1.37/1.19 % (5545)Refutation not found, incomplete strategy
% 1.37/1.19 % (5545)------------------------------
% 1.37/1.19 % (5545)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.19 % (5545)Termination reason: Refutation not found, incomplete strategy
% 1.37/1.19
% 1.37/1.19
% 1.37/1.19 % (5545)Memory used [KB]: 5500
% 1.37/1.19 % (5545)Time elapsed: 0.003 s
% 1.37/1.19 % (5545)Instructions burned: 6 (million)
% 1.37/1.19 % (5545)------------------------------
% 1.37/1.19 % (5545)------------------------------
% 1.37/1.19 % (5546)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_5419 for (2999ds/21Mi)
% 1.37/1.20 % (5547)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/5Mi)
% 1.37/1.20 % Exception at run slice level
% 1.37/1.20 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.37/1.20 % (5549)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/377Mi)
% 1.37/1.20 % (5548)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_5419 for (2999ds/6Mi)
% 1.37/1.20 % Exception at run slice level
% 1.37/1.20 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.37/1.20 % (5551)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_5419 for (2999ds/19Mi)
% 1.37/1.20 % Exception at run slice level
% 1.37/1.20 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.37/1.20 % (5550)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_5419 for (2999ds/779Mi)
% 1.37/1.20 % Exception at run slice level
% 1.37/1.20 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.37/1.20 % (5546)Instruction limit reached!
% 1.37/1.20 % (5546)------------------------------
% 1.37/1.20 % (5546)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.20 % (5546)Termination reason: Unknown
% 1.37/1.20 % (5546)Termination phase: Saturation
% 1.37/1.20
% 1.37/1.20 % (5546)Memory used [KB]: 5628
% 1.37/1.20 % (5546)Time elapsed: 0.009 s
% 1.37/1.20 % (5546)Instructions burned: 21 (million)
% 1.37/1.20 % (5546)------------------------------
% 1.37/1.20 % (5546)------------------------------
% 1.37/1.20 % (5553)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/879Mi)
% 1.37/1.21 % (5556)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/17Mi)
% 1.37/1.21 % (5557)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/3Mi)
% 1.37/1.21 % (5557)Instruction limit reached!
% 1.37/1.21 % (5557)------------------------------
% 1.37/1.21 % (5557)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.21 % (5557)Termination reason: Unknown
% 1.37/1.21 % (5557)Termination phase: Saturation
% 1.37/1.21
% 1.37/1.21 % (5557)Memory used [KB]: 1023
% 1.37/1.21 % (5557)Time elapsed: 0.002 s
% 1.37/1.21 % (5557)Instructions burned: 3 (million)
% 1.37/1.21 % (5557)------------------------------
% 1.37/1.21 % (5557)------------------------------
% 1.37/1.21 % (5558)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/30Mi)
% 1.37/1.21 % (5559)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/127Mi)
% 1.37/1.21 % (5556)Instruction limit reached!
% 1.37/1.21 % (5556)------------------------------
% 1.37/1.21 % (5556)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.21 % (5556)Termination reason: Unknown
% 1.37/1.21 % (5556)Termination phase: Saturation
% 1.37/1.21
% 1.37/1.21 % (5556)Memory used [KB]: 5628
% 1.37/1.21 % (5556)Time elapsed: 0.008 s
% 1.37/1.21 % (5556)Instructions burned: 19 (million)
% 1.37/1.21 % (5556)------------------------------
% 1.37/1.21 % (5556)------------------------------
% 1.37/1.22 % (5565)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_5419 for (2999ds/100Mi)
% 1.37/1.22 % (5558)Instruction limit reached!
% 1.37/1.22 % (5558)------------------------------
% 1.37/1.22 % (5558)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.22 % (5558)Termination reason: Unknown
% 1.37/1.22 % (5558)Termination phase: Saturation
% 1.37/1.22
% 1.37/1.22 % (5558)Memory used [KB]: 5628
% 1.37/1.22 % (5558)Time elapsed: 0.033 s
% 1.37/1.22 % (5558)Instructions burned: 31 (million)
% 1.37/1.22 % (5558)------------------------------
% 1.37/1.22 % (5558)------------------------------
% 1.37/1.22 % (5568)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_5419 for (2998ds/3Mi)
% 1.37/1.22 % Exception at run slice level
% 1.37/1.22 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.37/1.23 % (5572)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_5419 for (2998ds/20Mi)
% 1.37/1.23 % (5575)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_5419 for (2998ds/86Mi)
% 1.37/1.24 % (5572)Instruction limit reached!
% 1.37/1.24 % (5572)------------------------------
% 1.37/1.24 % (5572)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.24 % (5572)Termination reason: Unknown
% 1.37/1.24 % (5572)Termination phase: Saturation
% 1.37/1.24
% 1.37/1.24 % (5572)Memory used [KB]: 5628
% 1.37/1.24 % (5572)Time elapsed: 0.009 s
% 1.37/1.24 % (5572)Instructions burned: 21 (million)
% 1.37/1.24 % (5572)------------------------------
% 1.37/1.24 % (5572)------------------------------
% 1.37/1.25 % (5583)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_5419 for (2998ds/107Mi)
% 1.37/1.25 % (5565)Instruction limit reached!
% 1.37/1.25 % (5565)------------------------------
% 1.37/1.25 % (5565)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.25 % (5565)Termination reason: Unknown
% 1.37/1.25 % (5565)Termination phase: Saturation
% 1.37/1.25
% 1.37/1.25 % (5565)Memory used [KB]: 5756
% 1.37/1.25 % (5565)Time elapsed: 0.034 s
% 1.37/1.25 % (5565)Instructions burned: 100 (million)
% 1.37/1.25 % (5565)------------------------------
% 1.37/1.25 % (5565)------------------------------
% 1.37/1.25 % (5559)Instruction limit reached!
% 1.37/1.25 % (5559)------------------------------
% 1.37/1.25 % (5559)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.25 % (5559)Termination reason: Unknown
% 1.37/1.25 % (5559)Termination phase: Saturation
% 1.37/1.25
% 1.37/1.25 % (5559)Memory used [KB]: 5884
% 1.37/1.25 % (5559)Time elapsed: 0.044 s
% 1.37/1.25 % (5559)Instructions burned: 129 (million)
% 1.37/1.25 % (5559)------------------------------
% 1.37/1.25 % (5559)------------------------------
% 1.37/1.26 % (5590)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_5419 for (2998ds/39Mi)
% 1.37/1.26 % Exception at run slice level
% 1.37/1.26 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.37/1.26 % (5575)Instruction limit reached!
% 1.37/1.26 % (5575)------------------------------
% 1.37/1.26 % (5575)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.26 % (5575)Termination reason: Unknown
% 1.37/1.26 % (5575)Termination phase: Saturation
% 1.37/1.26
% 1.37/1.26 % (5575)Memory used [KB]: 6012
% 1.37/1.26 % (5575)Time elapsed: 0.030 s
% 1.37/1.26 % (5575)Instructions burned: 86 (million)
% 1.37/1.26 % (5575)------------------------------
% 1.37/1.26 % (5575)------------------------------
% 1.37/1.26 % (5591)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_5419 for (2998ds/448Mi)
% 1.37/1.26 % Exception at run slice level
% 1.37/1.26 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.37/1.27 % (5599)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_5419 for (2998ds/46Mi)
% 1.37/1.27 % (5600)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_5419 for (2998ds/98Mi)
% 1.37/1.27 % Exception at run slice level
% 1.37/1.27 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.37/1.27 % (5601)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_5419 for (2998ds/507Mi)
% 1.37/1.28 % (5601)Refutation not found, incomplete strategy
% 1.37/1.28 % (5601)------------------------------
% 1.37/1.28 % (5601)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.28 % (5601)Termination reason: Refutation not found, incomplete strategy
% 1.37/1.28
% 1.37/1.28
% 1.37/1.28 % (5601)Memory used [KB]: 5628
% 1.37/1.28 % (5601)Time elapsed: 0.007 s
% 1.37/1.28 % (5601)Instructions burned: 17 (million)
% 1.37/1.28 % (5601)------------------------------
% 1.37/1.28 % (5601)------------------------------
% 1.37/1.28 % (5606)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_5419 for (2998ds/149Mi)
% 1.37/1.28 % (5583)Instruction limit reached!
% 1.37/1.28 % (5583)------------------------------
% 1.37/1.28 % (5583)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.28 % (5583)Termination reason: Unknown
% 1.37/1.28 % (5583)Termination phase: Saturation
% 1.37/1.28
% 1.37/1.28 % (5583)Memory used [KB]: 5756
% 1.37/1.28 % (5583)Time elapsed: 0.037 s
% 1.37/1.28 % (5583)Instructions burned: 108 (million)
% 1.37/1.28 % (5583)------------------------------
% 1.37/1.28 % (5583)------------------------------
% 1.37/1.29 % (5599)Instruction limit reached!
% 1.37/1.29 % (5599)------------------------------
% 1.37/1.29 % (5599)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.29 % (5599)Termination reason: Unknown
% 1.37/1.29 % (5599)Termination phase: Saturation
% 1.37/1.29
% 1.37/1.29 % (5599)Memory used [KB]: 5628
% 1.37/1.29 % (5599)Time elapsed: 0.017 s
% 1.37/1.29 % (5599)Instructions burned: 47 (million)
% 1.37/1.29 % (5599)------------------------------
% 1.37/1.29 % (5599)------------------------------
% 1.37/1.29 % (5608)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_5419 for (2998ds/39Mi)
% 1.37/1.29 % (5611)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_5419 for (2998ds/6Mi)
% 1.37/1.29 % Exception at run slice level
% 1.37/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.37/1.30 % (5614)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_5419 for (2998ds/1087Mi)
% 1.37/1.30 % (5608)Instruction limit reached!
% 1.37/1.30 % (5608)------------------------------
% 1.37/1.30 % (5608)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.30 % (5608)Termination reason: Unknown
% 1.37/1.30 % (5608)Termination phase: Saturation
% 1.37/1.30
% 1.37/1.30 % (5608)Memory used [KB]: 5628
% 1.37/1.30 % (5608)Time elapsed: 0.014 s
% 1.37/1.30 % (5608)Instructions burned: 39 (million)
% 1.37/1.30 % (5608)------------------------------
% 1.37/1.30 % (5608)------------------------------
% 1.37/1.30 % (5618)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_5419 for (2998ds/47Mi)
% 1.37/1.31 % (5623)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_5419 for (2998ds/44Mi)
% 1.37/1.31 % Exception at run slice level
% 1.37/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.37/1.31 % (5549)Instruction limit reached!
% 1.37/1.31 % (5549)------------------------------
% 1.37/1.31 % (5549)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.31 % (5549)Termination reason: Unknown
% 1.37/1.31 % (5549)Termination phase: Saturation
% 1.37/1.31
% 1.37/1.31 % (5549)Memory used [KB]: 6012
% 1.37/1.31 % (5549)Time elapsed: 0.118 s
% 1.37/1.31 % (5549)Instructions burned: 379 (million)
% 1.37/1.31 % (5549)------------------------------
% 1.37/1.31 % (5549)------------------------------
% 1.37/1.32 % (5618)Instruction limit reached!
% 1.37/1.32 % (5618)------------------------------
% 1.37/1.32 % (5618)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.32 % (5618)Termination reason: Unknown
% 1.37/1.32 % (5618)Termination phase: Saturation
% 1.37/1.32
% 1.37/1.32 % (5618)Memory used [KB]: 5756
% 1.37/1.32 % (5618)Time elapsed: 0.018 s
% 1.37/1.32 % (5618)Instructions burned: 49 (million)
% 1.37/1.32 % (5618)------------------------------
% 1.37/1.32 % (5618)------------------------------
% 1.37/1.32 % (5628)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_5419 for (2998ds/432Mi)
% 1.37/1.32 % Exception at run slice level
% 1.37/1.32 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.37/1.32 % (5629)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_5419 for (2998ds/62Mi)
% 1.37/1.32 % Exception at run slice level
% 1.37/1.32 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.37/1.33 % (5632)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_5419 for (2998ds/31Mi)
% 1.37/1.33 % (5633)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_5419 for (2998ds/96Mi)
% 1.37/1.33 % (5634)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_5419 for (2998ds/453Mi)
% 1.37/1.33 % (5606)Instruction limit reached!
% 1.37/1.33 % (5606)------------------------------
% 1.37/1.33 % (5606)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.33 % (5606)Termination reason: Unknown
% 1.37/1.33 % (5606)Termination phase: Saturation
% 1.37/1.33
% 1.37/1.33 % (5606)Memory used [KB]: 5884
% 1.37/1.33 % (5606)Time elapsed: 0.052 s
% 1.37/1.33 % (5606)Instructions burned: 151 (million)
% 1.37/1.33 % (5606)------------------------------
% 1.37/1.33 % (5606)------------------------------
% 1.37/1.33 % Exception at run slice level
% 1.37/1.33 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.37/1.34 % (5632)Instruction limit reached!
% 1.37/1.34 % (5632)------------------------------
% 1.37/1.34 % (5632)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.34 % (5632)Termination reason: Unknown
% 1.37/1.34 % (5632)Termination phase: Saturation
% 1.37/1.34
% 1.37/1.34 % (5632)Memory used [KB]: 5756
% 1.37/1.34 % (5632)Time elapsed: 0.013 s
% 1.37/1.34 % (5632)Instructions burned: 33 (million)
% 1.37/1.34 % (5632)------------------------------
% 1.37/1.34 % (5632)------------------------------
% 1.37/1.34 % (5638)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_5419 for (2997ds/71Mi)
% 1.37/1.34 % (5639)dis+1002_1:1_bd=off:fsr=off:ntd=on:s2a=on:ss=axioms:i=83:si=on:rtra=on_0 on DTF2THF_5419 for (2997ds/83Mi)
% 1.37/1.34 % (5639)Refutation not found, incomplete strategy
% 1.37/1.34 % (5639)------------------------------
% 1.37/1.34 % (5639)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.34 % (5639)Termination reason: Refutation not found, incomplete strategy
% 1.37/1.34
% 1.37/1.34
% 1.37/1.34 % (5639)Memory used [KB]: 5500
% 1.37/1.34 % (5639)Time elapsed: 0.002 s
% 1.37/1.34 % (5639)Instructions burned: 2 (million)
% 1.37/1.34 % (5639)------------------------------
% 1.37/1.34 % (5639)------------------------------
% 1.37/1.35 % (5646)lrs+10_1:128_cnfonf=lazy_not_gen_be_off:hud=1:ins=1:i=11:si=on:rtra=on_0 on DTF2THF_5419 for (2997ds/11Mi)
% 1.37/1.35 % Exception at run slice level
% 1.37/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.37/1.35 % (5647)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_5419 for (2997ds/41Mi)
% 1.37/1.35 % Exception at run slice level
% 1.37/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.37/1.36 % (5648)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_5419 for (2997ds/6Mi)
% 1.37/1.36 % (5633)Instruction limit reached!
% 1.37/1.36 % (5633)------------------------------
% 1.37/1.36 % (5633)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.36 % (5633)Termination reason: Unknown
% 1.37/1.36 % (5633)Termination phase: Saturation
% 1.37/1.36
% 1.37/1.36 % (5633)Memory used [KB]: 5756
% 1.37/1.36 % (5633)Time elapsed: 0.033 s
% 1.37/1.36 % (5633)Instructions burned: 97 (million)
% 1.37/1.36 % (5633)------------------------------
% 1.37/1.36 % (5633)------------------------------
% 1.37/1.36 % (5648)Instruction limit reached!
% 1.37/1.36 % (5648)------------------------------
% 1.37/1.36 % (5648)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.36 % (5648)Termination reason: Unknown
% 1.37/1.36 % (5648)Termination phase: Saturation
% 1.37/1.36
% 1.37/1.36 % (5648)Memory used [KB]: 5500
% 1.37/1.36 % (5648)Time elapsed: 0.004 s
% 1.37/1.36 % (5648)Instructions burned: 8 (million)
% 1.37/1.36 % (5648)------------------------------
% 1.37/1.36 % (5648)------------------------------
% 1.37/1.36 % (5649)dis+10_1:1_avsq=on:cnfonf=off:e2e=on:nm=32:i=150:si=on:rtra=on_0 on DTF2THF_5419 for (2997ds/150Mi)
% 1.37/1.37 % (5638)Instruction limit reached!
% 1.37/1.37 % (5638)------------------------------
% 1.37/1.37 % (5638)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.37 % (5638)Termination reason: Unknown
% 1.37/1.37 % (5638)Termination phase: Saturation
% 1.37/1.37
% 1.37/1.37 % (5638)Memory used [KB]: 5756
% 1.37/1.37 % (5638)Time elapsed: 0.025 s
% 1.37/1.37 % (5638)Instructions burned: 73 (million)
% 1.37/1.37 % (5638)------------------------------
% 1.37/1.37 % (5638)------------------------------
% 1.37/1.37 % (5614)First to succeed.
% 1.37/1.37 % (5543)Refutation not found, non-redundant clauses discarded% (5543)------------------------------
% 1.37/1.37 % (5543)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.37 % (5543)Termination reason: Refutation not found, non-redundant clauses discarded
% 1.37/1.37
% 1.37/1.37 % (5543)Memory used [KB]: 6524
% 1.37/1.37 % (5543)Time elapsed: 0.186 s
% 1.37/1.37 % (5543)Instructions burned: 591 (million)
% 1.37/1.37 % (5543)------------------------------
% 1.37/1.37 % (5543)------------------------------
% 1.37/1.37 % (5614)Refutation found. Thanks to Tanya!
% 1.37/1.37 % SZS status Theorem for DTF2THF_5419
% 1.37/1.37 % SZS output start Proof for DTF2THF_5419
% 1.37/1.37 thf(type_def_6, type, sK0: $tType).
% 1.37/1.37 thf(func_def_0, type, 'const/sets/SUBSET': !>[X0: $tType]:((X0 > $o) > (X0 > $o) > $o)).
% 1.37/1.37 thf(func_def_1, type, 'const/sets/PSUBSET': !>[X0: $tType]:((X0 > $o) > (X0 > $o) > $o)).
% 1.37/1.37 thf(func_def_2, type, 'const/sets/IN': !>[X0: $tType]:(X0 > (X0 > $o) > $o)).
% 1.37/1.37 thf(func_def_6, type, sK1: sK0 > $o).
% 1.37/1.37 thf(func_def_7, type, sK2: sK0 > $o).
% 1.37/1.37 thf(func_def_8, type, sK3: sK0 > $o).
% 1.37/1.37 thf(func_def_9, type, sK4: !>[X0: $tType]:((X0 > $o) > (X0 > $o) > X0)).
% 1.37/1.37 thf(func_def_10, type, sK5: !>[X0: $tType]:((X0 > $o) > (X0 > $o) > X0)).
% 1.37/1.37 thf(func_def_12, type, ph7: !>[X0: $tType]:(X0)).
% 1.37/1.37 thf(f966,plain,(
% 1.37/1.37 $false),
% 1.37/1.37 inference(avatar_sat_refutation,[status(thm)],[f263,f488,f729,f732,f749,f753,f965])).
% 1.37/1.37 thf(f965,plain,(
% 1.37/1.37 spl6_2),
% 1.37/1.37 inference(avatar_contradiction_clause,[status(thm)],[f964])).
% 1.37/1.37 thf(f964,plain,(
% 1.37/1.37 $false | spl6_2),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f963])).
% 1.37/1.37 thf(f963,plain,(
% 1.37/1.37 ($false = $true) | spl6_2),
% 1.37/1.37 inference(forward_demodulation,[status(thm)],[f960,f761])).
% 1.37/1.37 thf(f761,plain,(
% 1.37/1.37 ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | spl6_2),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f759])).
% 1.37/1.37 thf(f759,plain,(
% 1.37/1.37 ($true != $true) | ($false = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | spl6_2),
% 1.37/1.37 inference(superposition,[status(thm)],[f61,f51])).
% 1.37/1.37 thf(f51,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0] : (($true = (X2 @ X1)) | ($false = (X2 @ X1))) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f49])).
% 1.37/1.37 thf(f49,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0] : (($false = (X2 @ X1)) | ($false = $true) | ($true = (X2 @ X1))) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f48,f47])).
% 1.37/1.37 thf(f47,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ X2 @ X1) = $true) | ((X1 @ X2) = $false)) )),
% 1.37/1.37 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.37/1.37 thf(f37,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ X2 @ X1) = (X1 @ X2))) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f1])).
% 1.37/1.37 thf(f1,axiom,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0] : (('const/sets/IN' @ X0 @ X2 @ X1) = (X1 @ X2))),
% 1.37/1.37 file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/IN_')).
% 1.37/1.37 thf(f48,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ X2 @ X1) = $false) | ((X1 @ X2) = $true)) )),
% 1.37/1.37 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.37/1.37 thf(f61,plain,(
% 1.37/1.37 ($true != ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | spl6_2),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f60])).
% 1.37/1.37 thf(f60,definition,(
% 1.37/1.37 spl6_2 <=> ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_2])],[avatar_definition])).
% 1.37/1.37 thf(f960,plain,(
% 1.37/1.37 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f959])).
% 1.37/1.37 thf(f959,plain,(
% 1.37/1.37 ($true != $true) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 inference(duplicate_literal_removal,[status(thm)],[f957])).
% 1.37/1.37 thf(f957,plain,(
% 1.37/1.37 ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | ($true = ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | ($true != $true)),
% 1.37/1.37 inference(superposition,[status(thm)],[f230,f41])).
% 1.37/1.37 thf(f41,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X1) = $true) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true)) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f30])).
% 1.37/1.37 thf(f30,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) != $true) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2))) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true)) & ((('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true) | ((('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X1) = $true) & (('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X2) != $true))))),
% 1.37/1.37 inference(skolemisation,[status(esa),new_symbols(skolem,[sK5])],[f28,f29])).
% 1.37/1.37 thf(f29,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (? [X4 : X0] : (($true = ('const/sets/IN' @ X0 @ X4 @ X1)) & (('const/sets/IN' @ X0 @ X4 @ X2) != $true)) => ((('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X1) = $true) & (('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X2) != $true)))),
% 1.37/1.37 introduced(definition,[],[choice_axiom])).
% 1.37/1.37 thf(f28,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) != $true) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2))) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true)) & ((('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true) | ? [X4 : X0] : (($true = ('const/sets/IN' @ X0 @ X4 @ X1)) & (('const/sets/IN' @ X0 @ X4 @ X2) != $true))))),
% 1.37/1.37 inference(rectify,[status(thm)],[f27])).
% 1.37/1.37 thf(f27,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) != $true) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2))) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true)) & ((('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true) | ? [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) = $true) & ($true != ('const/sets/IN' @ X0 @ X3 @ X2)))))),
% 1.37/1.37 inference(nnf_transformation,[status(thm)],[f16])).
% 1.37/1.37 thf(f16,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) != $true) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2))) <=> (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true))),
% 1.37/1.37 inference(ennf_transformation,[status(thm)],[f15])).
% 1.37/1.37 thf(f15,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true) <=> ! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1) = $true) => ($true = ('const/sets/IN' @ X0 @ X3 @ X2))))),
% 1.37/1.37 inference(fool_elimination,[status(thm)],[f14])).
% 1.37/1.37 thf(f14,plain,(
% 1.37/1.37 ! [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.37/1.37 inference(rectify,[status(thm)],[f3])).
% 1.37/1.37 thf(f3,axiom,(
% 1.37/1.37 ! [X0 : $tType,X2 : X0 > $o,X3 : X0 > $o] : (('const/sets/SUBSET' @ X0 @ X2 @ X3) = ! [X4 : X0] : (('const/sets/IN' @ X0 @ X4 @ X2) => ('const/sets/IN' @ X0 @ X4 @ X3)))),
% 1.37/1.37 file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/SUBSET_')).
% 1.37/1.37 thf(f230,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : ((('const/sets/IN' @ sK0 @ (sK5 @ sK0 @ sK3 @ X0) @ sK1) != $true) | (('const/sets/SUBSET' @ sK0 @ X0 @ sK3) = $true)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f224])).
% 1.37/1.37 thf(f224,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : ((('const/sets/IN' @ sK0 @ (sK5 @ sK0 @ sK3 @ X0) @ sK1) != $true) | (('const/sets/SUBSET' @ sK0 @ X0 @ sK3) = $true) | ($true != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f126,f149])).
% 1.37/1.37 thf(f149,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ sK2)) | (('const/sets/IN' @ sK0 @ X0 @ sK1) != $true)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f146])).
% 1.37/1.37 thf(f146,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : (($true = ('const/sets/IN' @ sK0 @ X0 @ sK2)) | ($true != $true) | (('const/sets/IN' @ sK0 @ X0 @ sK1) != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f110,f36])).
% 1.37/1.37 thf(f36,plain,(
% 1.37/1.37 (('const/sets/PSUBSET' @ sK0 @ sK1 @ sK2) = $true)),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f22])).
% 1.37/1.37 thf(f22,plain,(
% 1.37/1.37 (('const/sets/PSUBSET' @ sK0 @ sK1 @ sK2) = $true) & ($true = ('const/sets/SUBSET' @ sK0 @ sK2 @ sK3)) & ($true != ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f18,f21])).
% 1.37/1.37 thf(f21,plain,(
% 1.37/1.37 ? [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o,X3 : X0 > $o] : (($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) & (('const/sets/SUBSET' @ X0 @ X2 @ X3) = $true) & ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X3))) => ((('const/sets/PSUBSET' @ sK0 @ sK1 @ sK2) = $true) & ($true = ('const/sets/SUBSET' @ sK0 @ sK2 @ sK3)) & ($true != ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK3)))),
% 1.37/1.37 introduced(definition,[],[choice_axiom])).
% 1.37/1.37 thf(f18,plain,(
% 1.37/1.37 ? [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o,X3 : X0 > $o] : (($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) & (('const/sets/SUBSET' @ X0 @ X2 @ X3) = $true) & ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X3)))),
% 1.37/1.37 inference(flattening,[status(thm)],[f17])).
% 1.37/1.37 thf(f17,plain,(
% 1.37/1.37 ? [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o,X3 : X0 > $o] : (($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X3)) & ((('const/sets/SUBSET' @ X0 @ X2 @ X3) = $true) & ($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2))))),
% 1.37/1.37 inference(ennf_transformation,[status(thm)],[f13])).
% 1.37/1.37 thf(f13,plain,(
% 1.37/1.37 ~! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o,X3 : X0 > $o] : (((('const/sets/SUBSET' @ X0 @ X2 @ X3) = $true) & ($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2))) => ($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X3)))),
% 1.37/1.37 inference(fool_elimination,[status(thm)],[f12])).
% 1.37/1.37 thf(f12,plain,(
% 1.37/1.37 ~! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o,X3 : X0 > $o] : ((('const/sets/PSUBSET' @ X0 @ X1 @ X2) & ('const/sets/SUBSET' @ X0 @ X2 @ X3)) => ('const/sets/PSUBSET' @ X0 @ X1 @ X3))),
% 1.37/1.37 inference(rectify,[status(thm)],[f6])).
% 1.37/1.37 thf(f6,negated_conjecture,(
% 1.37/1.37 ~! [X0 : $tType,X2 : X0 > $o,X3 : X0 > $o,X4 : X0 > $o] : ((('const/sets/PSUBSET' @ X0 @ X2 @ X3) & ('const/sets/SUBSET' @ X0 @ X3 @ X4)) => ('const/sets/PSUBSET' @ X0 @ X2 @ X4))),
% 1.37/1.37 inference(negated_conjecture,[status(cth)],[f5])).
% 1.37/1.37 thf(f5,conjecture,(
% 1.37/1.37 ! [X0 : $tType,X2 : X0 > $o,X3 : X0 > $o,X4 : X0 > $o] : ((('const/sets/PSUBSET' @ X0 @ X2 @ X3) & ('const/sets/SUBSET' @ X0 @ X3 @ X4)) => ('const/sets/PSUBSET' @ X0 @ X2 @ X4))),
% 1.37/1.37 file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/PSUBSET_SUBSET_TRANS_')).
% 1.37/1.37 thf(f110,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | (('const/sets/IN' @ X0 @ X3 @ X1) != $true)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f107])).
% 1.37/1.37 thf(f107,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : (($true = ('const/sets/IN' @ X0 @ X3 @ X2)) | ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) | ($true != $true) | (('const/sets/IN' @ X0 @ X3 @ X1) != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f42,f31])).
% 1.37/1.37 thf(f31,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true) | ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2))) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f20])).
% 1.37/1.37 thf(f20,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) | (X1 = X2) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true)) & (((X1 != X2) & (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true)) | ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2))))),
% 1.37/1.37 inference(flattening,[status(thm)],[f19])).
% 1.37/1.37 thf(f19,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) | ((X1 = X2) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true))) & (((X1 != X2) & (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true)) | ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2))))),
% 1.37/1.37 inference(nnf_transformation,[status(thm)],[f11])).
% 1.37/1.37 thf(f11,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) <=> ((X1 != X2) & (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true)))),
% 1.37/1.37 inference(fool_elimination,[status(thm)],[f10])).
% 1.37/1.37 thf(f10,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (('const/sets/PSUBSET' @ X0 @ X1 @ X2) = ('const/sets/SUBSET' @ X0 @ X1 @ X2) & (X1 != X2))),
% 1.37/1.37 inference(rectify,[status(thm)],[f4])).
% 1.37/1.37 thf(f4,axiom,(
% 1.37/1.37 ! [X0 : $tType,X2 : X0 > $o,X3 : X0 > $o] : (('const/sets/PSUBSET' @ X0 @ X2 @ X3) = ('const/sets/SUBSET' @ X0 @ X2 @ X3) & (X2 != X3))),
% 1.37/1.37 file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/PSUBSET_')).
% 1.37/1.37 thf(f42,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X3 : X0,X1 : X0 > $o] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true) | (('const/sets/IN' @ X0 @ X3 @ X1) != $true) | ($true = ('const/sets/IN' @ X0 @ X3 @ X2))) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f30])).
% 1.37/1.37 thf(f126,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : ((('const/sets/IN' @ sK0 @ (sK5 @ sK0 @ sK3 @ X0) @ sK2) != $true) | (('const/sets/SUBSET' @ sK0 @ X0 @ sK3) = $true)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f123])).
% 1.37/1.37 thf(f123,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : ((('const/sets/IN' @ sK0 @ (sK5 @ sK0 @ sK3 @ X0) @ sK2) != $true) | (('const/sets/SUBSET' @ sK0 @ X0 @ sK3) = $true) | ($true != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f40,f111])).
% 1.37/1.37 thf(f111,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : ((('const/sets/IN' @ sK0 @ X0 @ sK3) = $true) | ($true != ('const/sets/IN' @ sK0 @ X0 @ sK2))) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f106])).
% 1.37/1.37 thf(f106,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : (($true != ('const/sets/IN' @ sK0 @ X0 @ sK2)) | (('const/sets/IN' @ sK0 @ X0 @ sK3) = $true) | ($true != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f42,f35])).
% 1.37/1.37 thf(f35,plain,(
% 1.37/1.37 ($true = ('const/sets/SUBSET' @ sK0 @ sK2 @ sK3))),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f22])).
% 1.37/1.37 thf(f40,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ (sK5 @ X0 @ X2 @ X1) @ X2) != $true) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) = $true)) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f30])).
% 1.37/1.37 thf(f753,plain,(
% 1.37/1.37 ~spl6_2 | spl6_1),
% 1.37/1.37 inference(avatar_split_clause,[status(thm)],[f133,f57,f60])).
% 1.37/1.37 thf(f57,definition,(
% 1.37/1.37 spl6_1 <=> (sK3 = sK1)),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_1])],[avatar_definition])).
% 1.37/1.37 thf(f133,plain,(
% 1.37/1.37 ($true != ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | (sK3 = sK1)),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f128])).
% 1.37/1.37 thf(f128,plain,(
% 1.37/1.37 ($true != ('const/sets/SUBSET' @ sK0 @ sK1 @ sK3)) | (sK3 = sK1) | ($false = $true)),
% 1.37/1.37 inference(superposition,[status(thm)],[f100,f33])).
% 1.37/1.37 thf(f33,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/PSUBSET' @ X0 @ X1 @ X2)) | (X1 = X2) | (('const/sets/SUBSET' @ X0 @ X1 @ X2) != $true)) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f20])).
% 1.37/1.37 thf(f100,plain,(
% 1.37/1.37 ($false = ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f90])).
% 1.37/1.37 thf(f90,plain,(
% 1.37/1.37 ($false = ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK3)) | ($true != $true)),
% 1.37/1.37 inference(superposition,[status(thm)],[f34,f51])).
% 1.37/1.37 thf(f34,plain,(
% 1.37/1.37 ($true != ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK3))),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f22])).
% 1.37/1.37 thf(f749,plain,(
% 1.37/1.37 ~spl6_8),
% 1.37/1.37 inference(avatar_contradiction_clause,[status(thm)],[f748])).
% 1.37/1.37 thf(f748,plain,(
% 1.37/1.37 $false | ~spl6_8),
% 1.37/1.37 inference(subsumption_resolution,[status(thm)],[f733,f43])).
% 1.37/1.37 thf(f43,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o] : ((('const/sets/PSUBSET' @ X0 @ X2 @ X2) != $true)) )),
% 1.37/1.37 inference(equality_resolution,[status(thm)],[f32])).
% 1.37/1.37 thf(f32,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((X1 != X2) | ($true != ('const/sets/PSUBSET' @ X0 @ X1 @ X2))) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f20])).
% 1.37/1.37 thf(f733,plain,(
% 1.37/1.37 ($true = ('const/sets/PSUBSET' @ sK0 @ sK1 @ sK1)) | ~spl6_8),
% 1.37/1.37 inference(backward_demodulation,[status(thm)],[f36,f545])).
% 1.37/1.37 thf(f545,plain,(
% 1.37/1.37 (sK1 = sK2) | ~spl6_8),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f544])).
% 1.37/1.37 thf(f544,definition,(
% 1.37/1.37 spl6_8 <=> (sK1 = sK2)),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_8])],[avatar_definition])).
% 1.37/1.37 thf(f732,plain,(
% 1.37/1.37 spl6_8 | ~spl6_1 | ~spl6_5),
% 1.37/1.37 inference(avatar_split_clause,[status(thm)],[f731,f256,f57,f544])).
% 1.37/1.37 thf(f256,definition,(
% 1.37/1.37 spl6_5 <=> (sK3 = sK2)),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_5])],[avatar_definition])).
% 1.37/1.37 thf(f731,plain,(
% 1.37/1.37 (sK1 = sK2) | (~spl6_1 | ~spl6_5)),
% 1.37/1.37 inference(forward_demodulation,[status(thm)],[f257,f58])).
% 1.37/1.37 thf(f58,plain,(
% 1.37/1.37 (sK3 = sK1) | ~spl6_1),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f57])).
% 1.37/1.37 thf(f257,plain,(
% 1.37/1.37 (sK3 = sK2) | ~spl6_5),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f256])).
% 1.37/1.37 thf(f729,plain,(
% 1.37/1.37 ~spl6_1 | spl6_6 | ~spl6_7),
% 1.37/1.37 inference(avatar_contradiction_clause,[status(thm)],[f728])).
% 1.37/1.37 thf(f728,plain,(
% 1.37/1.37 $false | (~spl6_1 | spl6_6 | ~spl6_7)),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f717])).
% 1.37/1.37 thf(f717,plain,(
% 1.37/1.37 ($false = $true) | (~spl6_1 | spl6_6 | ~spl6_7)),
% 1.37/1.37 inference(backward_demodulation,[status(thm)],[f564,f570])).
% 1.37/1.37 thf(f570,plain,(
% 1.37/1.37 ($false = (sK1 @ (sK4 @ sK0 @ sK1 @ sK2))) | (~spl6_1 | spl6_6)),
% 1.37/1.37 inference(forward_demodulation,[status(thm)],[f425,f58])).
% 1.37/1.37 thf(f425,plain,(
% 1.37/1.37 ((sK1 @ (sK4 @ sK0 @ sK3 @ sK2)) = $false) | spl6_6),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f422])).
% 1.37/1.37 thf(f422,plain,(
% 1.37/1.37 ((sK1 @ (sK4 @ sK0 @ sK3 @ sK2)) = $false) | ($true != $true) | spl6_6),
% 1.37/1.37 inference(superposition,[status(thm)],[f260,f47])).
% 1.37/1.37 thf(f260,plain,(
% 1.37/1.37 (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK1) != $true) | spl6_6),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f259])).
% 1.37/1.37 thf(f259,definition,(
% 1.37/1.37 spl6_6 <=> (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK1) = $true)),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_6])],[avatar_definition])).
% 1.37/1.37 thf(f564,plain,(
% 1.37/1.37 ($true = (sK1 @ (sK4 @ sK0 @ sK1 @ sK2))) | (~spl6_1 | ~spl6_7)),
% 1.37/1.37 inference(forward_demodulation,[status(thm)],[f487,f58])).
% 1.37/1.37 thf(f487,plain,(
% 1.37/1.37 ($true = (sK3 @ (sK4 @ sK0 @ sK3 @ sK2))) | ~spl6_7),
% 1.37/1.37 inference(avatar_component_clause,[status(thm)],[f486])).
% 1.37/1.37 thf(f486,definition,(
% 1.37/1.37 spl6_7 <=> ($true = (sK3 @ (sK4 @ sK0 @ sK3 @ sK2)))),
% 1.37/1.37 introduced(definition,[new_symbols(naming,[spl6_7])],[avatar_definition])).
% 1.37/1.37 thf(f488,plain,(
% 1.37/1.37 spl6_5 | spl6_7),
% 1.37/1.37 inference(avatar_split_clause,[status(thm)],[f484,f486,f256])).
% 1.37/1.37 thf(f484,plain,(
% 1.37/1.37 ($true = (sK3 @ (sK4 @ sK0 @ sK3 @ sK2))) | (sK3 = sK2)),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f483])).
% 1.37/1.37 thf(f483,plain,(
% 1.37/1.37 (sK3 = sK2) | ($true = (sK3 @ (sK4 @ sK0 @ sK3 @ sK2))) | ($true != $true)),
% 1.37/1.37 inference(equality_factoring,[status(thm)],[f390])).
% 1.37/1.37 thf(f390,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : (((sK3 @ (sK4 @ sK0 @ X0 @ sK2)) = $true) | ((X0 @ (sK4 @ sK0 @ X0 @ sK2)) = $true) | (sK2 = X0)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f377])).
% 1.37/1.37 thf(f377,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : (((sK3 @ (sK4 @ sK0 @ X0 @ sK2)) = $true) | ($true != $true) | ((X0 @ (sK4 @ sK0 @ X0 @ sK2)) = $true) | (sK2 = X0)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f124,f158])).
% 1.37/1.37 thf(f158,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ (sK4 @ X0 @ X1 @ X2) @ X2) = $true) | (X1 = X2) | ((X1 @ (sK4 @ X0 @ X1 @ X2)) = $true)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f153])).
% 1.37/1.37 thf(f153,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((('const/sets/IN' @ X0 @ (sK4 @ X0 @ X1 @ X2) @ X2) = $true) | ((X1 @ (sK4 @ X0 @ X1 @ X2)) = $true) | (X1 = X2) | ($false = $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f45,f48])).
% 1.37/1.37 thf(f45,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($true = ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X2)) | (X1 = X2) | (('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X1) = $true)) )),
% 1.37/1.37 inference(binary_proxy_clausification,[status(thm)],[f38])).
% 1.37/1.37 thf(f38,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : ((X1 = X2) | (('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X1) != ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X2))) )),
% 1.37/1.37 inference(cnf_transformation,[status(thm)],[f26])).
% 1.37/1.37 thf(f26,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2)) | (X1 != X2)) & ((X1 = X2) | (('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X1) != ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X2))))),
% 1.37/1.37 inference(skolemisation,[status(esa),new_symbols(skolem,[sK4])],[f24,f25])).
% 1.37/1.37 thf(f25,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (? [X4 : X0] : (('const/sets/IN' @ X0 @ X4 @ X2) != ('const/sets/IN' @ X0 @ X4 @ X1)) => (('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X1) != ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X2)))),
% 1.37/1.37 introduced(definition,[],[choice_axiom])).
% 1.37/1.37 thf(f24,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2)) | (X1 != X2)) & ((X1 = X2) | ? [X4 : X0] : (('const/sets/IN' @ X0 @ X4 @ X2) != ('const/sets/IN' @ X0 @ X4 @ X1))))),
% 1.37/1.37 inference(rectify,[status(thm)],[f23])).
% 1.37/1.37 thf(f23,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2)) | (X1 != X2)) & ((X1 = X2) | ? [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) != ('const/sets/IN' @ X0 @ X3 @ X2))))),
% 1.37/1.37 inference(nnf_transformation,[status(thm)],[f9])).
% 1.37/1.37 thf(f9,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : (! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2)) <=> (X1 = X2))),
% 1.37/1.37 inference(fool_elimination,[status(thm)],[f8])).
% 1.37/1.37 thf(f8,plain,(
% 1.37/1.37 ! [X0 : $tType,X1 : X0 > $o,X2 : X0 > $o] : ((X1 = X2) = ! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2)))),
% 1.37/1.37 inference(rectify,[status(thm)],[f2])).
% 1.37/1.37 thf(f2,axiom,(
% 1.37/1.37 ! [X0 : $tType,X2 : X0 > $o,X3 : X0 > $o] : ((X2 = X3) = ! [X4 : X0] : (('const/sets/IN' @ X0 @ X4 @ X2) = ('const/sets/IN' @ X0 @ X4 @ X3)))),
% 1.37/1.37 file('/export/starexec/sandbox2/tmp/tmp.v1CTMpP1vm/DTF2THF_5419.p','thm/sets/EXTENSION_')).
% 1.37/1.37 thf(f124,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : (($true != ('const/sets/IN' @ sK0 @ X0 @ sK2)) | ($true = (sK3 @ X0))) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f121])).
% 1.37/1.37 thf(f121,plain,(
% 1.37/1.37 ( ! [X0 : sK0] : (($true != ('const/sets/IN' @ sK0 @ X0 @ sK2)) | ($false = $true) | ($true = (sK3 @ X0))) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f111,f48])).
% 1.37/1.37 thf(f263,plain,(
% 1.37/1.37 spl6_5 | ~spl6_6),
% 1.37/1.37 inference(avatar_split_clause,[status(thm)],[f262,f259,f256])).
% 1.37/1.37 thf(f262,plain,(
% 1.37/1.37 (sK3 = sK2) | (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK1) != $true)),
% 1.37/1.37 inference(subsumption_resolution,[status(thm)],[f251,f149])).
% 1.37/1.37 thf(f251,plain,(
% 1.37/1.37 ($true != ('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK2)) | (sK3 = sK2) | (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK1) != $true)),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f244])).
% 1.37/1.37 thf(f244,plain,(
% 1.37/1.37 (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK1) != $true) | ($false = $true) | (sK3 = sK2) | ($true != ('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ sK2) @ sK2))),
% 1.37/1.37 inference(superposition,[status(thm)],[f149,f173])).
% 1.37/1.37 thf(f173,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : (($false = ('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ X0) @ X0)) | (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ X0) @ sK2) != $true) | (sK3 = X0)) )),
% 1.37/1.37 inference(trivial_inequality_removal,[status(thm)],[f168])).
% 1.37/1.37 thf(f168,plain,(
% 1.37/1.37 ( ! [X0 : sK0 > $o] : (($false = $true) | (sK3 = X0) | ($false = ('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ X0) @ X0)) | (('const/sets/IN' @ sK0 @ (sK4 @ sK0 @ sK3 @ X0) @ sK2) != $true)) )),
% 1.37/1.37 inference(superposition,[status(thm)],[f111,f46])).
% 1.37/1.37 thf(f46,plain,(
% 1.37/1.37 ( ! [X0 : $tType,X2 : X0 > $o,X1 : X0 > $o] : (($false = ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X2)) | ($false = ('const/sets/IN' @ X0 @ (sK4 @ X0 @ X2 @ X1) @ X1)) | (X1 = X2)) )),
% 1.37/1.37 inference(binary_proxy_clausification,[status(thm)],[f38])).
% 1.37/1.37 % SZS output end Proof for DTF2THF_5419
% 1.37/1.37 % (5614)------------------------------
% 1.37/1.37 % (5614)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.37 % (5614)Termination reason: Refutation
% 1.37/1.37
% 1.37/1.37 % (5614)Memory used [KB]: 5884
% 1.37/1.37 % (5614)Time elapsed: 0.072 s
% 1.37/1.37 % (5614)Instructions burned: 214 (million)
% 1.37/1.37 % (5614)------------------------------
% 1.37/1.37 % (5614)------------------------------
% 1.37/1.37 % (5516)Success in time 0.24 s
%------------------------------------------------------------------------------