%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEU653^2 : TPTP v9.2.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n025.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:35:58 AM UTC 2026
% Result : Theorem 1.65s 1.31s
% Output : Refutation 1.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 11
% Syntax : Number of formulae : 119 ( 69 unt; 0 typ; 4 def)
% Number of atoms : 1057 ( 300 equ; 0 cnn)
% Maximal formula atoms : 7 ( 8 avg)
% Number of connectives : 1755 ( 45 ~; 66 |; 20 &;1446 @)
% ( 4 <=>; 88 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 16 usr; 17 con; 0-2 aty)
% ( 86 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 294 ( 102 ^; 180 !; 12 ?; 294 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_0,type,
in: $i > $i > $o ).
thf(func_def_2,type,
setadjoin: $i > $i > $i ).
thf(f351,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f115,f137,f340,f344,f350]) ).
thf(f350,plain,
~ spl4_5,
inference(avatar_contradiction_clause,[status(thm)],[f349]) ).
thf(f349,plain,
( $false
| ~ spl4_5 ),
inference(subsumption_resolution,[status(thm)],[f348,f31]) ).
thf(f31,plain,
sK0 != sK3,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f24,plain,
( ( upairequniteq = $true )
& ( setukpairinjL2 = $true )
& ( secondinupair = $true )
& ( setukpairinjR1 = $true )
& ( sK0 != sK3 )
& ( ( setadjoin @ ( setadjoin @ sK2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) )
& ( upairset2E = $true ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f22,f23]) ).
thf(f23,plain,
( ? [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 != X3 )
& ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) ) )
=> ( ( sK0 != sK3 )
& ( ( setadjoin @ ( setadjoin @ sK2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f22,plain,
( ( upairequniteq = $true )
& ( setukpairinjL2 = $true )
& ( secondinupair = $true )
& ( setukpairinjR1 = $true )
& ? [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 != X3 )
& ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) ) )
& ( upairset2E = $true ) ),
inference(flattening,[status(thm)],[f21]) ).
thf(f21,plain,
( ? [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 != X3 )
& ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) ) )
& ( upairequniteq = $true )
& ( setukpairinjR1 = $true )
& ( setukpairinjL2 = $true )
& ( upairset2E = $true )
& ( secondinupair = $true ) ),
inference(ennf_transformation,[status(thm)],[f18]) ).
thf(f18,plain,
~ ( ( secondinupair = $true )
=> ( ( upairset2E = $true )
=> ( ( setukpairinjL2 = $true )
=> ( ( setukpairinjR1 = $true )
=> ( ( upairequniteq = $true )
=> ! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X3 ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f17]) ).
thf(f17,plain,
~ ( secondinupair
=> ( upairset2E
=> ( setukpairinjL2
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X3 ) ) ) ) ) ) ),
inference(rectify,[status(thm)],[f7]) ).
thf(f7,negated_conjecture,
~ ( secondinupair
=> ( upairset2E
=> ( setukpairinjL2
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X1: $i,X2: $i,X0: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X1 = X3 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
thf(f6,conjecture,
( secondinupair
=> ( upairset2E
=> ( setukpairinjL2
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X1: $i,X2: $i,X0: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X1 = X3 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjR2) ).
thf(f348,plain,
( ( sK0 = sK3 )
| ~ spl4_5 ),
inference(equality_resolution,[status(thm)],[f345]) ).
thf(f345,plain,
( ! [X0: $i,X1: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) )
| ( sK0 = X1 ) )
| ~ spl4_5 ),
inference(subsumption_resolution,[status(thm)],[f163,f124]) ).
thf(f124,plain,
( ( sK0 = sK2 )
| ~ spl4_5 ),
inference(avatar_component_clause,[status(thm)],[f122]) ).
thf(f122,definition,
( spl4_5
<=> ( sK0 = sK2 ) ),
introduced(definition,[new_symbols(naming,[spl4_5])],[avatar_definition]) ).
thf(f163,plain,
! [X0: $i,X1: $i] :
( ( sK0 != sK2 )
| ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) )
| ( sK0 = X1 ) ),
inference(superposition,[status(thm)],[f78,f30]) ).
thf(f30,plain,
( ( setadjoin @ ( setadjoin @ sK2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f78,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
| ( X1 = X2 )
| ( X1 != X4 ) ),
inference(equality_proxy_clausification,[status(thm)],[f77]) ).
thf(f77,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( X4 = X1 )
= $false )
| ( X1 = X2 )
| ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f76]) ).
thf(f76,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( X2 = X1 )
= $true )
| ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
| ( ( X4 = X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f75]) ).
thf(f75,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
| ( ( ( X4 = X1 )
=> ( X2 = X1 ) )
= $true ) ),
inference(equality_proxy_clausification,[status(thm)],[f74]) ).
thf(f74,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( $false
= ( ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) ) )
| ( ( ( X4 = X1 )
=> ( X2 = X1 ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f73]) ).
thf(f73,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( X4 = X1 )
=> ( X2 = X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f72]) ).
thf(f72,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ^ [Y0: $i] :
( ( ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y0 = X1 )
=> ( X2 = X1 ) ) )
@ X4 )
= $true ),
inference(pi_clausification,[status(thm)],[f71]) ).
thf(f71,plain,
! [X2: $i,X3: $i,X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y0 = X1 )
=> ( X2 = X1 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f70]) ).
thf(f70,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y1 = X1 )
=> ( X2 = X1 ) ) ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f69]) ).
thf(f69,plain,
! [X2: $i,X1: $i] :
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y1 = X1 )
=> ( X2 = X1 ) ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f68]) ).
thf(f68,plain,
! [X2: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y2 = X1 )
=> ( Y0 = X1 ) ) ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f67]) ).
thf(f67,plain,
! [X1: $i] :
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y2 = X1 )
=> ( Y0 = X1 ) ) ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f66]) ).
thf(f66,plain,
! [X1: $i] :
( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y3 = Y0 )
=> ( Y1 = Y0 ) ) ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f41]) ).
thf(f41,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y3 = Y0 )
=> ( Y1 = Y0 ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f36,f32]) ).
thf(f32,plain,
setukpairinjR1 = $true,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f36,plain,
( setukpairinjR1
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y3 = Y0 )
=> ( Y1 = Y0 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
thf(f12,plain,
( setukpairinjR1
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( ( Y3 = Y0 )
=> ( Y1 = Y0 ) ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f11]) ).
thf(f11,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( ( X0 = X3 )
=> ( X2 = X3 ) ) )
= setukpairinjR1 ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
! [X2: $i,X0: $i,X1: $i,X3: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( ( X2 = X3 )
=> ( X1 = X3 ) ) )
= setukpairinjR1 ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjR1) ).
thf(f344,plain,
~ spl4_7,
inference(avatar_contradiction_clause,[status(thm)],[f343]) ).
thf(f343,plain,
( $false
| ~ spl4_7 ),
inference(equality_resolution,[status(thm)],[f136]) ).
thf(f136,plain,
( ! [X0: $i] :
( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ sK1 @ emptyset ) )
| ~ spl4_7 ),
inference(avatar_component_clause,[status(thm)],[f135]) ).
thf(f135,definition,
( spl4_7
<=> ! [X0: $i] :
( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ sK1 @ emptyset ) ) ),
introduced(definition,[new_symbols(naming,[spl4_7])],[avatar_definition]) ).
thf(f340,plain,
( ~ spl4_3
| spl4_5 ),
inference(avatar_contradiction_clause,[status(thm)],[f339]) ).
thf(f339,plain,
( $false
| ~ spl4_3
| spl4_5 ),
inference(subsumption_resolution,[status(thm)],[f338,f31]) ).
thf(f338,plain,
( ( sK0 = sK3 )
| ~ spl4_3
| spl4_5 ),
inference(subsumption_resolution,[status(thm)],[f333,f313]) ).
thf(f313,plain,
( ( sK0 != sK1 )
| spl4_5 ),
inference(superposition,[status(thm)],[f123,f299]) ).
thf(f299,plain,
sK1 = sK2,
inference(equality_resolution,[status(thm)],[f140]) ).
thf(f140,plain,
! [X0: $i,X1: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) )
| ( sK2 = X0 ) ),
inference(superposition,[status(thm)],[f52,f30]) ).
thf(f52,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
| ( X2 = X4 ) ),
inference(equality_proxy_clausification,[status(thm)],[f51]) ).
thf(f51,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( X4 = X2 )
= $true )
| ( ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
!= ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f50]) ).
thf(f50,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( $false
= ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) ) )
| ( ( X4 = X2 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f49]) ).
thf(f49,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( X4 = X2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f48]) ).
thf(f48,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ^ [Y0: $i] :
( ( ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y0 = X2 ) )
@ X4 )
= $true ),
inference(pi_clausification,[status(thm)],[f47]) ).
thf(f47,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( !! @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y0 = X2 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f46]) ).
thf(f46,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y1 = X2 ) ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f45]) ).
thf(f45,plain,
! [X2: $i,X1: $i] :
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y1 = X2 ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f44]) ).
thf(f44,plain,
! [X2: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f43]) ).
thf(f43,plain,
! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ ( setadjoin @ Y2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y2 @ ( setadjoin @ Y1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f42]) ).
thf(f42,plain,
! [X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( Y3 = Y1 ) ) ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f38]) ).
thf(f38,plain,
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( Y3 = Y1 ) ) ) ) ) ) ),
inference(definition_unfolding,[status(thm)],[f34,f28]) ).
thf(f28,plain,
( setukpairinjL2
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( Y3 = Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f16,plain,
( setukpairinjL2
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ ( setadjoin @ Y3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y3 @ ( setadjoin @ Y2 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ Y1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) @ emptyset ) ) )
=> ( Y3 = Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f15]) ).
thf(f15,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X2 ) )
= setukpairinjL2 ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
! [X2: $i,X3: $i,X0: $i,X1: $i] :
( ( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X2 ) )
= setukpairinjL2 ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjL2) ).
thf(f34,plain,
setukpairinjL2 = $true,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f123,plain,
( ( sK0 != sK2 )
| spl4_5 ),
inference(avatar_component_clause,[status(thm)],[f122]) ).
thf(f333,plain,
( ( sK0 = sK1 )
| ( sK0 = sK3 )
| ~ spl4_3 ),
inference(trivial_inequality_removal,[status(thm)],[f331]) ).
thf(f331,plain,
( ( $false = $true )
| ( sK0 = sK3 )
| ( sK0 = sK1 )
| ~ spl4_3 ),
inference(superposition,[status(thm)],[f325,f88]) ).
thf(f88,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $false )
| ( X2 = X3 )
| ( X1 = X3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f87]) ).
thf(f87,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $false )
| ( $true
= ( X3 = X2 ) )
| ( X1 = X3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f86]) ).
thf(f86,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( X3 = X1 )
= $true )
| ( $true
= ( X3 = X2 ) )
| ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f85]) ).
thf(f85,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $false )
| ( ( ( X3 = X1 )
| ( X3 = X2 ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f84]) ).
thf(f84,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( X3 = X1 )
| ( X3 = X2 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f83]) ).
thf(f83,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ^ [Y0: $i] :
( ( in @ Y0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( Y0 = X1 )
| ( Y0 = X2 ) ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f82]) ).
thf(f82,plain,
! [X2: $i,X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( Y0 = X1 )
| ( Y0 = X2 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f81]) ).
thf(f81,plain,
! [X2: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( Y1 = X1 )
| ( Y1 = Y0 ) ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f80]) ).
thf(f80,plain,
! [X1: $i] :
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( Y1 = X1 )
| ( Y1 = Y0 ) ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f79]) ).
thf(f79,plain,
! [X1: $i] :
( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( ( Y2 = Y0 )
| ( Y2 = Y1 ) ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f40]) ).
thf(f40,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( ( Y2 = Y0 )
| ( Y2 = Y1 ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f29,f25]) ).
thf(f25,plain,
( upairset2E
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( ( Y2 = Y0 )
| ( Y2 = Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
thf(f14,plain,
( upairset2E
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( setadjoin @ Y1 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( ( Y2 = Y0 )
| ( Y2 = Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f13]) ).
thf(f13,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X2 @ emptyset ) ) )
=> ( ( X0 = X1 )
| ( X0 = X2 ) ) )
= upairset2E ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,axiom,
! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ X2 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( X0 = X2 )
| ( X1 = X2 ) ) )
= upairset2E ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',upairset2E) ).
thf(f29,plain,
upairset2E = $true,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f325,plain,
( ( ( in @ sK0 @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) )
= $true )
| ~ spl4_3 ),
inference(superposition,[status(thm)],[f56,f109]) ).
thf(f109,plain,
( ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) )
| ~ spl4_3 ),
inference(avatar_component_clause,[status(thm)],[f107]) ).
thf(f107,definition,
( spl4_3
<=> ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) ) ),
introduced(definition,[new_symbols(naming,[spl4_3])],[avatar_definition]) ).
thf(f56,plain,
! [X2: $i,X1: $i] :
( $true
= ( in @ X2 @ ( setadjoin @ X1 @ ( setadjoin @ X2 @ emptyset ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f55]) ).
thf(f55,plain,
! [X2: $i,X1: $i] :
( ( ^ [Y0: $i] : ( in @ Y0 @ ( setadjoin @ X1 @ ( setadjoin @ Y0 @ emptyset ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f54]) ).
thf(f54,plain,
! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] : ( in @ Y0 @ ( setadjoin @ X1 @ ( setadjoin @ Y0 @ emptyset ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f53]) ).
thf(f53,plain,
! [X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ Y1 @ emptyset ) ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f39]) ).
thf(f39,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ Y1 @ emptyset ) ) ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f33,f27]) ).
thf(f27,plain,
( secondinupair
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ Y1 @ emptyset ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
thf(f20,plain,
( secondinupair
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( in @ Y1 @ ( setadjoin @ Y0 @ ( setadjoin @ Y1 @ emptyset ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f19]) ).
thf(f19,plain,
! [X0: $i,X1: $i] :
( ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) )
= secondinupair ),
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
! [X1: $i,X0: $i] :
( ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
= secondinupair ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',secondinupair) ).
thf(f33,plain,
secondinupair = $true,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f137,plain,
( spl4_7
| spl4_5
| ~ spl4_4 ),
inference(avatar_split_clause,[status(thm)],[f132,f111,f122,f135]) ).
thf(f111,definition,
( spl4_4
<=> ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ emptyset ) ) ),
introduced(definition,[new_symbols(naming,[spl4_4])],[avatar_definition]) ).
thf(f132,plain,
( ! [X0: $i] :
( ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ sK1 @ emptyset ) )
| ( sK0 = sK2 ) )
| ~ spl4_4 ),
inference(superposition,[status(thm)],[f65,f113]) ).
thf(f113,plain,
( ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ emptyset ) )
| ~ spl4_4 ),
inference(avatar_component_clause,[status(thm)],[f111]) ).
thf(f65,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( setadjoin @ X2 @ emptyset )
!= ( setadjoin @ X3 @ ( setadjoin @ X1 @ emptyset ) ) )
| ( X1 = X3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f64]) ).
thf(f64,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( setadjoin @ X2 @ emptyset )
!= ( setadjoin @ X3 @ ( setadjoin @ X1 @ emptyset ) ) )
| ( ( X3 = X1 )
= $true ) ),
inference(equality_proxy_clausification,[status(thm)],[f63]) ).
thf(f63,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( ( setadjoin @ X2 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X1 @ emptyset ) ) )
= $false )
| ( ( X3 = X1 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f62]) ).
thf(f62,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( ( setadjoin @ X2 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( X3 = X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f61]) ).
thf(f61,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ^ [Y0: $i] :
( ( ( setadjoin @ X2 @ emptyset )
= ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( Y0 = X1 ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f60]) ).
thf(f60,plain,
! [X2: $i,X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ X2 @ emptyset )
= ( setadjoin @ Y0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( Y0 = X1 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f59]) ).
thf(f59,plain,
! [X2: $i,X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( setadjoin @ Y1 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( Y1 = X1 ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f58]) ).
thf(f58,plain,
! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( setadjoin @ Y1 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( Y1 = X1 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f57]) ).
thf(f57,plain,
! [X1: $i] :
( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( setadjoin @ Y2 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f37]) ).
thf(f37,plain,
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( setadjoin @ Y2 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) ) ) ),
inference(definition_unfolding,[status(thm)],[f35,f26]) ).
thf(f26,plain,
( upairequniteq
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( setadjoin @ Y2 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
thf(f10,plain,
( upairequniteq
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( setadjoin @ Y2 @ ( setadjoin @ Y0 @ emptyset ) ) )
=> ( Y2 = Y0 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f9]) ).
thf(f9,plain,
( upairequniteq
= ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( setadjoin @ X1 @ emptyset )
= ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) )
=> ( X0 = X2 ) ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,axiom,
( upairequniteq
= ( ! [X0: $i,X2: $i,X1: $i] :
( ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
= ( setadjoin @ X2 @ emptyset ) )
=> ( X0 = X1 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',upairequniteq) ).
thf(f35,plain,
upairequniteq = $true,
inference(cnf_transformation,[status(thm)],[f24]) ).
thf(f115,plain,
( spl4_3
| spl4_4 ),
inference(avatar_split_clause,[status(thm)],[f104,f111,f107]) ).
thf(f104,plain,
( ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) )
| ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ emptyset ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f103]) ).
thf(f103,plain,
( ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ emptyset ) )
| ( ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) )
= ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) )
| ( $false = $true ) ),
inference(superposition,[status(thm)],[f88,f93]) ).
thf(f93,plain,
( ( in @ ( setadjoin @ sK2 @ ( setadjoin @ sK0 @ emptyset ) ) @ ( setadjoin @ ( setadjoin @ sK1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK1 @ ( setadjoin @ sK3 @ emptyset ) ) @ emptyset ) ) )
= $true ),
inference(superposition,[status(thm)],[f56,f30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : SEU653^2 : TPTP v9.2.1. Released v3.7.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/0.32 % Computer : n025.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue Feb 24 12:29:42 EST 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.32 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.21/0.43 ---- Original DTF file ---
% 0.21/0.43 thf(spec,logic,$$dhol).
% 0.21/0.43 %------------------------------------------------------------------------------
% 0.21/0.43 % File : SEU653^2 : TPTP v9.2.1. Released v3.7.0.
% 0.21/0.43 % Domain : Set Theory
% 0.21/0.43 % Problem : Ordered Pairs - Properties of Pairs
% 0.21/0.43 % Version : Especial > Reduced > Especial.
% 0.21/0.43 % English : (! x:i.! y:i.! z:i.! u:i.setadjoin (setadjoin x emptyset)
% 0.21/0.43 % (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset) =
% 0.21/0.43 % setadjoin (setadjoin z emptyset) (setadjoin (setadjoin z
% 0.21/0.43 % (setadjoin u emptyset)) emptyset) -> y = u)
% 0.21/0.43
% 0.21/0.43 % Refs : [Bro08] Brown (2008), Email to G. Sutcliffe
% 0.21/0.43 % Source : [Bro08]
% 0.21/0.43 % Names : ZFC155l [Bro08]
% 0.21/0.43
% 0.21/0.43 % Status : Theorem
% 0.21/0.43 % Rating : 0.00 v9.0.0, 0.20 v8.2.0, 0.23 v8.1.0, 0.18 v7.5.0, 0.14 v7.4.0, 0.22 v7.2.0, 0.12 v7.1.0, 0.38 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.60 v6.2.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v5.1.0, 0.80 v5.0.0, 0.60 v4.1.0, 0.33 v4.0.1, 0.67 v4.0.0, 0.33 v3.7.0
% 0.21/0.43 % Syntax : Number of formulae : 14 ( 5 unt; 8 typ; 5 def)
% 0.21/0.43 % Number of atoms : 28 ( 16 equ; 0 cnn)
% 0.21/0.43 % Maximal formula atoms : 7 ( 4 avg)
% 0.21/0.43 % Number of connectives : 90 ( 0 ~; 1 |; 0 &; 78 @)
% 0.21/0.43 % ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% 0.21/0.43 % Maximal formula depth : 11 ( 3 avg)
% 0.21/0.43 % Number of types : 2 ( 0 usr)
% 0.21/0.43 % Number of type conns : 4 ( 4 >; 0 *; 0 +; 0 <<)
% 0.21/0.43 % Number of symbols : 9 ( 8 usr; 6 con; 0-2 aty)
% 0.21/0.43 % Number of variables : 20 ( 0 ^; 20 !; 0 ?; 20 :)
% 0.21/0.43 % SPC : TH0_THM_EQU_NAR
% 0.21/0.43
% 0.21/0.43 % Comments : http://mathgate.info/detsetitem.php?id=209
% 0.21/0.43 %------------------------------------------------------------------------------
% 0.21/0.43 thf(in_type,type,
% 0.21/0.43 in: $i > $i > $o ).
% 0.21/0.43
% 0.21/0.43 thf(emptyset_type,type,
% 0.21/0.43 emptyset: $i ).
% 0.21/0.43
% 0.21/0.43 thf(setadjoin_type,type,
% 0.21/0.43 setadjoin: $i > $i > $i ).
% 0.21/0.43
% 0.21/0.43 thf(secondinupair_type,type,
% 0.21/0.43 secondinupair: $o ).
% 0.21/0.43
% 0.21/0.43 thf(secondinupair,definition,
% 0.21/0.43 ( secondinupair
% 0.21/0.43 = ( ! [Xx: $i,Xy: $i] : ( in @ Xy @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 thf(upairset2E_type,type,
% 0.21/0.43 upairset2E: $o ).
% 0.21/0.43
% 0.21/0.43 thf(upairset2E,definition,
% 0.21/0.43 ( upairset2E
% 0.21/0.43 = ( ! [Xx: $i,Xy: $i,Xz: $i] :
% 0.21/0.43 ( ( in @ Xz @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) )
% 0.21/0.43 => ( ( Xz = Xx )
% 0.21/0.43 | ( Xz = Xy ) ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 thf(setukpairinjL2_type,type,
% 0.21/0.43 setukpairinjL2: $o ).
% 0.21/0.43
% 0.21/0.43 thf(setukpairinjL2,definition,
% 0.21/0.43 ( setukpairinjL2
% 0.21/0.43 = ( ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 0.21/0.43 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 0.21/0.43 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 0.21/0.43 => ( Xx = Xz ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 thf(setukpairinjR1_type,type,
% 0.21/0.43 setukpairinjR1: $o ).
% 0.21/0.43
% 0.21/0.43 thf(setukpairinjR1,definition,
% 0.21/0.43 ( setukpairinjR1
% 0.21/0.43 = ( ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 0.21/0.43 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 0.21/0.43 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 0.21/0.43 => ( ( Xz = Xu )
% 0.21/0.43 => ( Xy = Xu ) ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 thf(upairequniteq_type,type,
% 0.21/0.43 upairequniteq: $o ).
% 0.21/0.43
% 0.21/0.43 thf(upairequniteq,definition,
% 0.21/0.43 ( upairequniteq
% 0.21/0.43 = ( ! [Xx: $i,Xy: $i,Xz: $i] :
% 0.21/0.43 ( ( ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) )
% 0.21/0.43 = ( setadjoin @ Xz @ emptyset ) )
% 0.21/0.43 => ( Xx = Xy ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 thf(setukpairinjR2,conjecture,
% 0.21/0.43 ( secondinupair
% 0.21/0.43 => ( upairset2E
% 0.21/0.43 => ( setukpairinjL2
% 0.21/0.43 => ( setukpairinjR1
% 0.21/0.43 => ( upairequniteq
% 0.21/0.43 => ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 0.21/0.43 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 0.21/0.43 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 0.21/0.43 => ( Xy = Xu ) ) ) ) ) ) ) ).
% 0.21/0.43
% 0.21/0.43 %------------------------------------------------------------------------------
% 0.21/0.43 ------------------------
% 1.55/1.23 ---- Embedded in THF ---
% 1.55/1.23 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.55/1.23 %%% Generated on Tue Feb 24 12:29:43 EST 2026
% 1.55/1.23 %%% using '$$dhol' embedding, version 1.3.0.
% 1.55/1.23 %%% Logic specification used:
% 1.55/1.23 %%% thf(spec, logic, $$dhol).
% 1.55/1.23
% 1.55/1.23 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2DTF17983.p
% See solution above
% 1.55/1.23 ------------------------
% 1.55/1.25 ---- Cleaned THF ---
% 1.55/1.25 thf(in_type,type,
% 1.55/1.25 in: $i > $i > $o ).
% 1.55/1.25
% 1.55/1.25 thf(emptyset_type,type,
% 1.55/1.25 emptyset: $i ).
% 1.55/1.25
% 1.55/1.25 thf(setadjoin_type,type,
% 1.55/1.25 setadjoin: $i > $i > $i ).
% 1.55/1.25
% 1.55/1.25 thf(secondinupair_type,type,
% 1.55/1.25 secondinupair: $o ).
% 1.55/1.25
% 1.55/1.25 thf(secondinupair,definition,
% 1.55/1.25 ( secondinupair
% 1.55/1.25 = ( ! [Xx: $i,Xy: $i] : ( in @ Xy @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) ) ) ) ).
% 1.55/1.25
% 1.55/1.25 thf(upairset2E_type,type,
% 1.55/1.25 upairset2E: $o ).
% 1.55/1.25
% 1.55/1.25 thf(upairset2E,definition,
% 1.55/1.25 ( upairset2E
% 1.55/1.25 = ( ! [Xx: $i,Xy: $i,Xz: $i] :
% 1.55/1.25 ( ( in @ Xz @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) )
% 1.55/1.25 => ( ( Xz = Xx )
% 1.55/1.25 | ( Xz = Xy ) ) ) ) ) ).
% 1.55/1.25
% 1.55/1.25 thf(setukpairinjL2_type,type,
% 1.55/1.25 setukpairinjL2: $o ).
% 1.55/1.25
% 1.55/1.25 thf(setukpairinjL2,definition,
% 1.55/1.25 ( setukpairinjL2
% 1.55/1.25 = ( ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 1.55/1.25 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 1.55/1.25 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 1.55/1.25 => ( Xx = Xz ) ) ) ) ).
% 1.55/1.25
% 1.55/1.25 thf(setukpairinjR1_type,type,
% 1.55/1.25 setukpairinjR1: $o ).
% 1.55/1.25
% 1.55/1.25 thf(setukpairinjR1,definition,
% 1.55/1.25 ( setukpairinjR1
% 1.55/1.25 = ( ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 1.55/1.25 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 1.55/1.25 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 1.55/1.25 => ( ( Xz = Xu )
% 1.55/1.25 => ( Xy = Xu ) ) ) ) ) ).
% 1.55/1.25
% 1.55/1.25 thf(upairequniteq_type,type,
% 1.55/1.25 upairequniteq: $o ).
% 1.55/1.25
% 1.55/1.25 thf(upairequniteq,definition,
% 1.55/1.25 ( upairequniteq
% 1.55/1.25 = ( ! [Xx: $i,Xy: $i,Xz: $i] :
% 1.55/1.25 ( ( ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) )
% 1.55/1.25 = ( setadjoin @ Xz @ emptyset ) )
% 1.55/1.25 => ( Xx = Xy ) ) ) ) ).
% 1.55/1.25
% 1.55/1.25 thf(setukpairinjR2,conjecture,
% 1.55/1.25 ( secondinupair
% 1.55/1.25 => ( upairset2E
% 1.55/1.25 => ( setukpairinjL2
% 1.55/1.25 => ( setukpairinjR1
% 1.55/1.25 => ( upairequniteq
% 1.55/1.25 => ! [Xx: $i,Xy: $i,Xz: $i,Xu: $i] :
% 1.55/1.25 ( ( ( setadjoin @ ( setadjoin @ Xx @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xx @ ( setadjoin @ Xy @ emptyset ) ) @ emptyset ) )
% 1.55/1.25 = ( setadjoin @ ( setadjoin @ Xz @ emptyset ) @ ( setadjoin @ ( setadjoin @ Xz @ ( setadjoin @ Xu @ emptyset ) ) @ emptyset ) ) )
% 1.55/1.25 => ( Xy = Xu ) ) ) ) ) ) ) ).
% 1.55/1.25 ------------------------
% 1.55/1.26 % (18172)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_17983 for (2999ds/4Mi)
% 1.55/1.26 % (18172)Instruction limit reached!
% 1.55/1.26 % (18172)------------------------------
% 1.55/1.26 % (18172)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.26 % (18172)Termination reason: Unknown
% 1.55/1.26 % (18172)Termination phase: Saturation
% 1.55/1.26
% 1.55/1.26 % (18172)Memory used [KB]: 5500
% 1.55/1.26 % (18172)Time elapsed: 0.003 s
% 1.55/1.26 % (18172)Instructions burned: 6 (million)
% 1.55/1.26 % (18172)------------------------------
% 1.55/1.26 % (18172)------------------------------
% 1.55/1.27 % (18175)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_17983 for (2999ds/2Mi)
% 1.55/1.27 % (18171)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/183Mi)
% 1.55/1.27 % (18173)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_17983 for (2999ds/27Mi)
% 1.55/1.27 % (18174)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/2Mi)
% 1.55/1.27 % (18176)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_17983 for (2999ds/275Mi)
% 1.55/1.27 % (18174)Instruction limit reached!
% 1.55/1.27 % (18174)------------------------------
% 1.55/1.27 % (18174)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.27 % (18175)Instruction limit reached!
% 1.55/1.27 % (18175)------------------------------
% 1.55/1.27 % (18175)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.27 % (18175)Termination reason: Unknown
% 1.55/1.27 % (18175)Termination phase: Property scanning
% 1.55/1.27
% 1.55/1.27 % (18175)Memory used [KB]: 1023
% 1.55/1.27 % (18175)Time elapsed: 0.003 s
% 1.55/1.27 % (18175)Instructions burned: 3 (million)
% 1.55/1.27 % (18175)------------------------------
% 1.55/1.27 % (18175)------------------------------
% 1.55/1.27 % (18174)Termination reason: Unknown
% 1.55/1.27 % (18174)Termination phase: shuffling
% 1.55/1.27
% 1.55/1.27 % (18174)Memory used [KB]: 1023
% 1.55/1.27 % (18174)Time elapsed: 0.003 s
% 1.55/1.27 % (18174)Instructions burned: 2 (million)
% 1.55/1.27 % (18174)------------------------------
% 1.55/1.27 % (18174)------------------------------
% 1.55/1.27 % (18178)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/3Mi)
% 1.55/1.27 % (18178)Instruction limit reached!
% 1.55/1.27 % (18178)------------------------------
% 1.55/1.27 % (18178)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.27 % (18178)Termination reason: Unknown
% 1.55/1.27 % (18178)Termination phase: Property scanning
% 1.55/1.27
% 1.55/1.27 % (18178)Memory used [KB]: 1023
% 1.55/1.27 % (18178)Time elapsed: 0.002 s
% 1.55/1.27 % (18178)Instructions burned: 4 (million)
% 1.55/1.27 % (18178)------------------------------
% 1.55/1.27 % (18178)------------------------------
% 1.55/1.28 % (18177)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/18Mi)
% 1.55/1.29 % (18181)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_17983 for (2999ds/3Mi)
% 1.55/1.29 % (18173)Instruction limit reached!
% 1.55/1.29 % (18173)------------------------------
% 1.55/1.29 % (18173)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.29 % (18173)Termination reason: Unknown
% 1.55/1.29 % (18173)Termination phase: Saturation
% 1.55/1.29
% 1.55/1.29 % (18173)Memory used [KB]: 5628
% 1.55/1.29 % (18173)Time elapsed: 0.018 s
% 1.55/1.29 % (18173)Instructions burned: 27 (million)
% 1.55/1.29 % (18173)------------------------------
% 1.55/1.29 % (18173)------------------------------
% 1.55/1.29 % (18181)Instruction limit reached!
% 1.55/1.29 % (18181)------------------------------
% 1.55/1.29 % (18181)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.29 % (18181)Termination reason: Unknown
% 1.55/1.29 % (18181)Termination phase: Property scanning
% 1.55/1.29
% 1.55/1.29 % (18181)Memory used [KB]: 1023
% 1.55/1.29 % (18181)Time elapsed: 0.002 s
% 1.55/1.29 % (18181)Instructions burned: 4 (million)
% 1.55/1.29 % (18181)------------------------------
% 1.55/1.29 % (18181)------------------------------
% 1.55/1.29 % (18179)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_17983 for (2999ds/37Mi)
% 1.55/1.29 % (18177)Instruction limit reached!
% 1.55/1.29 % (18177)------------------------------
% 1.55/1.29 % (18177)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.29 % (18177)Termination reason: Unknown
% 1.55/1.29 % (18177)Termination phase: Saturation
% 1.55/1.29
% 1.55/1.29 % (18177)Memory used [KB]: 5628
% 1.55/1.29 % (18177)Time elapsed: 0.012 s
% 1.55/1.29 % (18177)Instructions burned: 18 (million)
% 1.55/1.29 % (18177)------------------------------
% 1.55/1.29 % (18177)------------------------------
% 1.55/1.29 % (18180)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_17983 for (2999ds/15Mi)
% 1.55/1.30 % (18180)Instruction limit reached!
% 1.55/1.30 % (18180)------------------------------
% 1.55/1.30 % (18180)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.55/1.30 % (18180)Termination reason: Unknown
% 1.55/1.30 % (18180)Termination phase: Saturation
% 1.55/1.30
% 1.55/1.30 % (18180)Memory used [KB]: 5628
% 1.55/1.30 % (18180)Time elapsed: 0.007 s
% 1.55/1.30 % (18180)Instructions burned: 15 (million)
% 1.55/1.30 % (18180)------------------------------
% 1.55/1.30 % (18180)------------------------------
% 1.55/1.30 % (18183)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/7Mi)
% 1.65/1.30 % (18183)Instruction limit reached!
% 1.65/1.30 % (18183)------------------------------
% 1.65/1.30 % (18183)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.30 % (18183)Termination reason: Unknown
% 1.65/1.30 % (18183)Termination phase: Saturation
% 1.65/1.30
% 1.65/1.30 % (18183)Memory used [KB]: 1023
% 1.65/1.30 % (18183)Time elapsed: 0.003 s
% 1.65/1.30 % (18183)Instructions burned: 7 (million)
% 1.65/1.30 % (18183)------------------------------
% 1.65/1.30 % (18183)------------------------------
% 1.65/1.30 % (18179)Instruction limit reached!
% 1.65/1.30 % (18179)------------------------------
% 1.65/1.30 % (18179)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.30 % (18179)Termination reason: Unknown
% 1.65/1.30 % (18179)Termination phase: Saturation
% 1.65/1.30
% 1.65/1.30 % (18179)Memory used [KB]: 5756
% 1.65/1.30 % (18179)Time elapsed: 0.015 s
% 1.65/1.30 % (18179)Instructions burned: 38 (million)
% 1.65/1.30 % (18179)------------------------------
% 1.65/1.30 % (18179)------------------------------
% 1.65/1.30 % (18182)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_17983 for (2999ds/1041Mi)
% 1.65/1.30 % (18184)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/16Mi)
% 1.65/1.31 % (18171)First to succeed.
% 1.65/1.31 % (18185)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_17983 for (2999ds/3Mi)
% 1.65/1.31 % (18185)Instruction limit reached!
% 1.65/1.31 % (18185)------------------------------
% 1.65/1.31 % (18185)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.31 % (18185)Termination reason: Unknown
% 1.65/1.31 % (18185)Termination phase: Property scanning
% 1.65/1.31
% 1.65/1.31 % (18185)Memory used [KB]: 1023
% 1.65/1.31 % (18185)Time elapsed: 0.003 s
% 1.65/1.31 % (18185)Instructions burned: 4 (million)
% 1.65/1.31 % (18185)------------------------------
% 1.65/1.31 % (18185)------------------------------
% 1.65/1.31 % (18186)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_17983 for (2999ds/3Mi)
% 1.65/1.31 % (18184)Instruction limit reached!
% 1.65/1.31 % (18184)------------------------------
% 1.65/1.31 % (18184)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.31 % (18187)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_17983 for (2999ds/7Mi)
% 1.65/1.31 % (18184)Termination reason: Unknown
% 1.65/1.31 % (18184)Termination phase: Saturation
% 1.65/1.31
% 1.65/1.31 % (18184)Memory used [KB]: 5884
% 1.65/1.31 % (18184)Time elapsed: 0.008 s
% 1.65/1.31 % (18184)Instructions burned: 18 (million)
% 1.65/1.31 % (18184)------------------------------
% 1.65/1.31 % (18184)------------------------------
% 1.65/1.31 % (18186)Instruction limit reached!
% 1.65/1.31 % (18186)------------------------------
% 1.65/1.31 % (18186)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.31 % (18186)Termination reason: Unknown
% 1.65/1.31 % (18186)Termination phase: Property scanning
% 1.65/1.31
% 1.65/1.31 % (18186)Memory used [KB]: 1023
% 1.65/1.31 % (18186)Time elapsed: 0.003 s
% 1.65/1.31 % (18186)Instructions burned: 3 (million)
% 1.65/1.31 % (18186)------------------------------
% 1.65/1.31 % (18186)------------------------------
% 1.65/1.31 % (18171)Refutation found. Thanks to Tanya!
% 1.65/1.31 % SZS status Theorem for DTF2THF_17983
% 1.65/1.31 % SZS output start Proof for DTF2THF_17983
% 1.65/1.31 thf(func_def_0, type, in: $i > $i > $o).
% 1.65/1.31 thf(func_def_2, type, setadjoin: $i > $i > $i).
% 1.65/1.31 thf(f351,plain,(
% 1.65/1.31 $false),
% 1.65/1.31 inference(avatar_sat_refutation,[status(thm)],[f115,f137,f340,f344,f350])).
% 1.65/1.31 thf(f350,plain,(
% 1.65/1.31 ~spl4_5),
% 1.65/1.31 inference(avatar_contradiction_clause,[status(thm)],[f349])).
% 1.65/1.31 thf(f349,plain,(
% 1.65/1.31 $false | ~spl4_5),
% 1.65/1.31 inference(subsumption_resolution,[status(thm)],[f348,f31])).
% 1.65/1.31 thf(f31,plain,(
% 1.65/1.31 (sK0 != sK3)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f24,plain,(
% 1.65/1.31 (upairequniteq = $true) & (setukpairinjL2 = $true) & (secondinupair = $true) & (setukpairinjR1 = $true) & ((sK0 != sK3) & ((setadjoin @ (setadjoin @ sK2 @ emptyset) @ (setadjoin @ (setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset)))) & (upairset2E = $true)),
% 1.65/1.31 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f22,f23])).
% 1.65/1.31 thf(f23,plain,(
% 1.65/1.31 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((X0 != X3) & ((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))) => ((sK0 != sK3) & ((setadjoin @ (setadjoin @ sK2 @ emptyset) @ (setadjoin @ (setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset))))),
% 1.65/1.31 introduced(definition,[],[choice_axiom])).
% 1.65/1.31 thf(f22,plain,(
% 1.65/1.31 (upairequniteq = $true) & (setukpairinjL2 = $true) & (secondinupair = $true) & (setukpairinjR1 = $true) & ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((X0 != X3) & ((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))) & (upairset2E = $true)),
% 1.65/1.31 inference(flattening,[status(thm)],[f21])).
% 1.65/1.31 thf(f21,plain,(
% 1.65/1.31 ((((? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((X0 != X3) & ((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))) & (upairequniteq = $true)) & (setukpairinjR1 = $true)) & (setukpairinjL2 = $true)) & (upairset2E = $true)) & (secondinupair = $true)),
% 1.65/1.31 inference(ennf_transformation,[status(thm)],[f18])).
% 1.65/1.31 thf(f18,plain,(
% 1.65/1.31 ~((secondinupair = $true) => ((upairset2E = $true) => ((setukpairinjL2 = $true) => ((setukpairinjR1 = $true) => ((upairequniteq = $true) => ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X0 = X3)))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f17])).
% 1.65/1.31 thf(f17,plain,(
% 1.65/1.31 ~(secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X0 = X3)))))))),
% 1.65/1.31 inference(rectify,[status(thm)],[f7])).
% 1.65/1.31 thf(f7,negated_conjecture,(
% 1.65/1.31 ~(secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => ! [X1 : $i,X2 : $i,X0 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X1 = X3)))))))),
% 1.65/1.31 inference(negated_conjecture,[status(cth)],[f6])).
% 1.65/1.31 thf(f6,conjecture,(
% 1.65/1.31 secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => ! [X1 : $i,X2 : $i,X0 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X1 = X3))))))),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjR2)).
% 1.65/1.31 thf(f348,plain,(
% 1.65/1.31 (sK0 = sK3) | ~spl4_5),
% 1.65/1.31 inference(equality_resolution,[status(thm)],[f345])).
% 1.65/1.31 thf(f345,plain,(
% 1.65/1.31 ( ! [X0 : $i,X1 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset))) | (sK0 = X1)) ) | ~spl4_5),
% 1.65/1.31 inference(subsumption_resolution,[status(thm)],[f163,f124])).
% 1.65/1.31 thf(f124,plain,(
% 1.65/1.31 (sK0 = sK2) | ~spl4_5),
% 1.65/1.31 inference(avatar_component_clause,[status(thm)],[f122])).
% 1.65/1.31 thf(f122,definition,(
% 1.65/1.31 spl4_5 <=> (sK0 = sK2)),
% 1.65/1.31 introduced(definition,[new_symbols(naming,[spl4_5])],[avatar_definition])).
% 1.65/1.31 thf(f163,plain,(
% 1.65/1.31 ( ! [X0 : $i,X1 : $i] : ((sK0 != sK2) | ((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset))) | (sK0 = X1)) )),
% 1.65/1.31 inference(superposition,[status(thm)],[f78,f30])).
% 1.65/1.31 thf(f30,plain,(
% 1.65/1.31 ((setadjoin @ (setadjoin @ sK2 @ emptyset) @ (setadjoin @ (setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset)))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f78,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset))) | (X1 = X2) | (X1 != X4)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f77])).
% 1.65/1.31 thf(f77,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((X4 = X1) = $false) | (X1 = X2) | ((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset)))) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f76])).
% 1.65/1.31 thf(f76,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((X2 = X1) = $true) | ((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset))) | ((X4 = X1) = $false)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f75])).
% 1.65/1.31 thf(f75,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset))) | (((X4 = X1) => (X2 = X1)) = $true)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f74])).
% 1.65/1.31 thf(f74,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset)))) | (((X4 = X1) => (X2 = X1)) = $true)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f73])).
% 1.65/1.31 thf(f73,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((X4 = X1) => (X2 = X1))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f72])).
% 1.65/1.31 thf(f72,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((^[Y0 : $i]: (((setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y0 = X1) => (X2 = X1)))) @ X4) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f71])).
% 1.65/1.31 thf(f71,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: (((setadjoin @ (setadjoin @ X3 @ emptyset) @ (setadjoin @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y0 = X1) => (X2 = X1))))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f70])).
% 1.65/1.31 thf(f70,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y1 = X1) => (X2 = X1)))))) @ X3) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f69])).
% 1.65/1.31 thf(f69,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y1 = X1) => (X2 = X1))))))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f68])).
% 1.65/1.31 thf(f68,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y2 = X1) => (Y0 = X1)))))))) @ X2) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f67])).
% 1.65/1.31 thf(f67,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => ((Y2 = X1) => (Y0 = X1))))))))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f66])).
% 1.65/1.31 thf(f66,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = ((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => ((Y3 = Y0) => (Y1 = Y0)))))))))) @ X1))) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f41])).
% 1.65/1.31 thf(f41,plain,(
% 1.65/1.31 ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => ((Y3 = Y0) => (Y1 = Y0))))))))))) = $true)),
% 1.65/1.31 inference(definition_unfolding,[status(thm)],[f36,f32])).
% 1.65/1.31 thf(f32,plain,(
% 1.65/1.31 (setukpairinjR1 = $true)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f36,plain,(
% 1.65/1.31 (setukpairinjR1 = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => ((Y3 = Y0) => (Y1 = Y0))))))))))))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f12])).
% 1.65/1.31 thf(f12,plain,(
% 1.65/1.31 (setukpairinjR1 = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => ((Y3 = Y0) => (Y1 = Y0))))))))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f11])).
% 1.65/1.31 thf(f11,plain,(
% 1.65/1.31 (! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => ((X0 = X3) => (X2 = X3))) = setukpairinjR1)),
% 1.65/1.31 inference(rectify,[status(thm)],[f4])).
% 1.65/1.31 thf(f4,axiom,(
% 1.65/1.31 (! [X2 : $i,X0 : $i,X1 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => ((X2 = X3) => (X1 = X3))) = setukpairinjR1)),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjR1)).
% 1.65/1.31 thf(f344,plain,(
% 1.65/1.31 ~spl4_7),
% 1.65/1.31 inference(avatar_contradiction_clause,[status(thm)],[f343])).
% 1.65/1.31 thf(f343,plain,(
% 1.65/1.31 $false | ~spl4_7),
% 1.65/1.31 inference(equality_resolution,[status(thm)],[f136])).
% 1.65/1.31 thf(f136,plain,(
% 1.65/1.31 ( ! [X0 : $i] : (((setadjoin @ X0 @ emptyset) != (setadjoin @ sK1 @ emptyset))) ) | ~spl4_7),
% 1.65/1.31 inference(avatar_component_clause,[status(thm)],[f135])).
% 1.65/1.31 thf(f135,definition,(
% 1.65/1.31 spl4_7 <=> ! [X0 : $i] : ((setadjoin @ X0 @ emptyset) != (setadjoin @ sK1 @ emptyset))),
% 1.65/1.31 introduced(definition,[new_symbols(naming,[spl4_7])],[avatar_definition])).
% 1.65/1.31 thf(f340,plain,(
% 1.65/1.31 ~spl4_3 | spl4_5),
% 1.65/1.31 inference(avatar_contradiction_clause,[status(thm)],[f339])).
% 1.65/1.31 thf(f339,plain,(
% 1.65/1.31 $false | (~spl4_3 | spl4_5)),
% 1.65/1.31 inference(subsumption_resolution,[status(thm)],[f338,f31])).
% 1.65/1.31 thf(f338,plain,(
% 1.65/1.31 (sK0 = sK3) | (~spl4_3 | spl4_5)),
% 1.65/1.31 inference(subsumption_resolution,[status(thm)],[f333,f313])).
% 1.65/1.31 thf(f313,plain,(
% 1.65/1.31 (sK0 != sK1) | spl4_5),
% 1.65/1.31 inference(superposition,[status(thm)],[f123,f299])).
% 1.65/1.31 thf(f299,plain,(
% 1.65/1.31 (sK1 = sK2)),
% 1.65/1.31 inference(equality_resolution,[status(thm)],[f140])).
% 1.65/1.31 thf(f140,plain,(
% 1.65/1.31 ( ! [X0 : $i,X1 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset))) | (sK2 = X0)) )),
% 1.65/1.31 inference(superposition,[status(thm)],[f52,f30])).
% 1.65/1.31 thf(f52,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) | (X2 = X4)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f51])).
% 1.65/1.31 thf(f51,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((X4 = X2) = $true) | ((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) != (setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f50])).
% 1.65/1.31 thf(f50,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X3 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset)))) | ((X4 = X2) = $true)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f49])).
% 1.65/1.31 thf(f49,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((setadjoin @ (setadjoin @ X4 @ emptyset) @ (setadjoin @ (setadjoin @ X4 @ (setadjoin @ X3 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (X4 = X2)) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f48])).
% 1.65/1.31 thf(f48,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((^[Y0 : $i]: (((setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X3 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y0 = X2))) @ X4) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f47])).
% 1.65/1.31 thf(f47,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: (((setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X3 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y0 = X2)))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f46])).
% 1.65/1.31 thf(f46,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y1 = X2))))) @ X3) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f45])).
% 1.65/1.31 thf(f45,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y1 = X2)))))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f44])).
% 1.65/1.31 thf(f44,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y2 = Y0))))))) @ X2) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f43])).
% 1.65/1.31 thf(f43,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ (setadjoin @ Y2 @ emptyset) @ (setadjoin @ (setadjoin @ Y2 @ (setadjoin @ Y1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y0 @ emptyset) @ (setadjoin @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset)) @ emptyset))) => (Y2 = Y0)))))))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f42])).
% 1.65/1.31 thf(f42,plain,(
% 1.65/1.31 ( ! [X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => (Y3 = Y1))))))))) @ X1) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f38])).
% 1.65/1.31 thf(f38,plain,(
% 1.65/1.31 ($true = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => (Y3 = Y1)))))))))))),
% 1.65/1.31 inference(definition_unfolding,[status(thm)],[f34,f28])).
% 1.65/1.31 thf(f28,plain,(
% 1.65/1.31 (setukpairinjL2 = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => (Y3 = Y1)))))))))))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f16])).
% 1.65/1.31 thf(f16,plain,(
% 1.65/1.31 (setukpairinjL2 = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((setadjoin @ (setadjoin @ Y3 @ emptyset) @ (setadjoin @ (setadjoin @ Y3 @ (setadjoin @ Y2 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ Y1 @ emptyset) @ (setadjoin @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset)) @ emptyset))) => (Y3 = Y1)))))))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f15])).
% 1.65/1.31 thf(f15,plain,(
% 1.65/1.31 (! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X0 = X2)) = setukpairinjL2)),
% 1.65/1.31 inference(rectify,[status(thm)],[f3])).
% 1.65/1.31 thf(f3,axiom,(
% 1.65/1.31 (! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (((setadjoin @ (setadjoin @ X0 @ emptyset) @ (setadjoin @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) @ emptyset)) = (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))) => (X0 = X2)) = setukpairinjL2)),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',setukpairinjL2)).
% 1.65/1.31 thf(f34,plain,(
% 1.65/1.31 (setukpairinjL2 = $true)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f123,plain,(
% 1.65/1.31 (sK0 != sK2) | spl4_5),
% 1.65/1.31 inference(avatar_component_clause,[status(thm)],[f122])).
% 1.65/1.31 thf(f333,plain,(
% 1.65/1.31 (sK0 = sK1) | (sK0 = sK3) | ~spl4_3),
% 1.65/1.31 inference(trivial_inequality_removal,[status(thm)],[f331])).
% 1.65/1.31 thf(f331,plain,(
% 1.65/1.31 ($false = $true) | (sK0 = sK3) | (sK0 = sK1) | ~spl4_3),
% 1.65/1.31 inference(superposition,[status(thm)],[f325,f88])).
% 1.65/1.31 thf(f88,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) = $false) | (X2 = X3) | (X1 = X3)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f87])).
% 1.65/1.31 thf(f87,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) = $false) | ($true = (X3 = X2)) | (X1 = X3)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f86])).
% 1.65/1.31 thf(f86,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((X3 = X1) = $true) | ($true = (X3 = X2)) | ((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) = $false)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f85])).
% 1.65/1.31 thf(f85,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) = $false) | (((X3 = X1) | (X3 = X2)) = $true)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f84])).
% 1.65/1.31 thf(f84,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) => ((X3 = X1) | (X3 = X2))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f83])).
% 1.65/1.31 thf(f83,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((^[Y0 : $i]: ((in @ Y0 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) => ((Y0 = X1) | (Y0 = X2)))) @ X3) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f82])).
% 1.65/1.31 thf(f82,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (setadjoin @ X2 @ (setadjoin @ X1 @ emptyset))) => ((Y0 = X1) | (Y0 = X2))))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f81])).
% 1.65/1.31 thf(f81,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset))) => ((Y1 = X1) | (Y1 = Y0)))))) @ X2) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f80])).
% 1.65/1.31 thf(f80,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset))) => ((Y1 = X1) | (Y1 = Y0))))))) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f79])).
% 1.65/1.31 thf(f79,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = ((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset))) => ((Y2 = Y0) | (Y2 = Y1)))))))) @ X1))) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f40])).
% 1.65/1.31 thf(f40,plain,(
% 1.65/1.31 ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset))) => ((Y2 = Y0) | (Y2 = Y1))))))))) = $true)),
% 1.65/1.31 inference(definition_unfolding,[status(thm)],[f29,f25])).
% 1.65/1.31 thf(f25,plain,(
% 1.65/1.31 (upairset2E = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset))) => ((Y2 = Y0) | (Y2 = Y1))))))))))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f14])).
% 1.65/1.31 thf(f14,plain,(
% 1.65/1.31 (upairset2E = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (setadjoin @ Y1 @ (setadjoin @ Y0 @ emptyset))) => ((Y2 = Y0) | (Y2 = Y1))))))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f13])).
% 1.65/1.31 thf(f13,plain,(
% 1.65/1.31 (! [X0 : $i,X1 : $i,X2 : $i] : ((in @ X0 @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset))) => ((X0 = X1) | (X0 = X2))) = upairset2E)),
% 1.65/1.31 inference(rectify,[status(thm)],[f2])).
% 1.65/1.31 thf(f2,axiom,(
% 1.65/1.31 (! [X2 : $i,X0 : $i,X1 : $i] : ((in @ X2 @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset))) => ((X0 = X2) | (X1 = X2))) = upairset2E)),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',upairset2E)).
% 1.65/1.31 thf(f29,plain,(
% 1.65/1.31 (upairset2E = $true)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f325,plain,(
% 1.65/1.31 ((in @ sK0 @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset))) = $true) | ~spl4_3),
% 1.65/1.31 inference(superposition,[status(thm)],[f56,f109])).
% 1.65/1.31 thf(f109,plain,(
% 1.65/1.31 ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset))) | ~spl4_3),
% 1.65/1.31 inference(avatar_component_clause,[status(thm)],[f107])).
% 1.65/1.31 thf(f107,definition,(
% 1.65/1.31 spl4_3 <=> ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)))),
% 1.65/1.31 introduced(definition,[new_symbols(naming,[spl4_3])],[avatar_definition])).
% 1.65/1.31 thf(f56,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : (($true = (in @ X2 @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f55])).
% 1.65/1.31 thf(f55,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : ((((^[Y0 : $i]: (in @ Y0 @ (setadjoin @ X1 @ (setadjoin @ Y0 @ emptyset)))) @ X2) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f54])).
% 1.65/1.31 thf(f54,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: (in @ Y0 @ (setadjoin @ X1 @ (setadjoin @ Y0 @ emptyset))))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f53])).
% 1.65/1.31 thf(f53,plain,(
% 1.65/1.31 ( ! [X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ Y1 @ emptyset)))))) @ X1) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f39])).
% 1.65/1.31 thf(f39,plain,(
% 1.65/1.31 ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ Y1 @ emptyset))))))) = $true)),
% 1.65/1.31 inference(definition_unfolding,[status(thm)],[f33,f27])).
% 1.65/1.31 thf(f27,plain,(
% 1.65/1.31 (secondinupair = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ Y1 @ emptyset))))))))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f20])).
% 1.65/1.31 thf(f20,plain,(
% 1.65/1.31 (secondinupair = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (in @ Y1 @ (setadjoin @ Y0 @ (setadjoin @ Y1 @ emptyset))))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f19])).
% 1.65/1.31 thf(f19,plain,(
% 1.65/1.31 (! [X0 : $i,X1 : $i] : (in @ X0 @ (setadjoin @ X1 @ (setadjoin @ X0 @ emptyset))) = secondinupair)),
% 1.65/1.31 inference(rectify,[status(thm)],[f1])).
% 1.65/1.31 thf(f1,axiom,(
% 1.65/1.31 (! [X1 : $i,X0 : $i] : (in @ X1 @ (setadjoin @ X0 @ (setadjoin @ X1 @ emptyset))) = secondinupair)),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',secondinupair)).
% 1.65/1.31 thf(f33,plain,(
% 1.65/1.31 (secondinupair = $true)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f137,plain,(
% 1.65/1.31 spl4_7 | spl4_5 | ~spl4_4),
% 1.65/1.31 inference(avatar_split_clause,[status(thm)],[f132,f111,f122,f135])).
% 1.65/1.31 thf(f111,definition,(
% 1.65/1.31 spl4_4 <=> ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ emptyset))),
% 1.65/1.31 introduced(definition,[new_symbols(naming,[spl4_4])],[avatar_definition])).
% 1.65/1.31 thf(f132,plain,(
% 1.65/1.31 ( ! [X0 : $i] : (((setadjoin @ X0 @ emptyset) != (setadjoin @ sK1 @ emptyset)) | (sK0 = sK2)) ) | ~spl4_4),
% 1.65/1.31 inference(superposition,[status(thm)],[f65,f113])).
% 1.65/1.31 thf(f113,plain,(
% 1.65/1.31 ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ emptyset)) | ~spl4_4),
% 1.65/1.31 inference(avatar_component_clause,[status(thm)],[f111])).
% 1.65/1.31 thf(f65,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((setadjoin @ X2 @ emptyset) != (setadjoin @ X3 @ (setadjoin @ X1 @ emptyset))) | (X1 = X3)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f64])).
% 1.65/1.31 thf(f64,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((setadjoin @ X2 @ emptyset) != (setadjoin @ X3 @ (setadjoin @ X1 @ emptyset))) | ((X3 = X1) = $true)) )),
% 1.65/1.31 inference(equality_proxy_clausification,[status(thm)],[f63])).
% 1.65/1.31 thf(f63,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((setadjoin @ X2 @ emptyset) = (setadjoin @ X3 @ (setadjoin @ X1 @ emptyset))) = $false) | ((X3 = X1) = $true)) )),
% 1.65/1.31 inference(binary_proxy_clausification,[status(thm)],[f62])).
% 1.65/1.31 thf(f62,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((setadjoin @ X2 @ emptyset) = (setadjoin @ X3 @ (setadjoin @ X1 @ emptyset))) => (X3 = X1)) = $true)) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f61])).
% 1.65/1.31 thf(f61,plain,(
% 1.65/1.31 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((^[Y0 : $i]: (((setadjoin @ X2 @ emptyset) = (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset))) => (Y0 = X1))) @ X3) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f60])).
% 1.65/1.31 thf(f60,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: (((setadjoin @ X2 @ emptyset) = (setadjoin @ Y0 @ (setadjoin @ X1 @ emptyset))) => (Y0 = X1)))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f59])).
% 1.65/1.31 thf(f59,plain,(
% 1.65/1.31 ( ! [X2 : $i,X1 : $i] : ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ Y0 @ emptyset) = (setadjoin @ Y1 @ (setadjoin @ X1 @ emptyset))) => (Y1 = X1))))) @ X2) = $true)) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f58])).
% 1.65/1.31 thf(f58,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((setadjoin @ Y0 @ emptyset) = (setadjoin @ Y1 @ (setadjoin @ X1 @ emptyset))) => (Y1 = X1)))))))) )),
% 1.65/1.31 inference(beta_eta_normalization,[status(thm)],[f57])).
% 1.65/1.31 thf(f57,plain,(
% 1.65/1.31 ( ! [X1 : $i] : (($true = ((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ Y1 @ emptyset) = (setadjoin @ Y2 @ (setadjoin @ Y0 @ emptyset))) => (Y2 = Y0))))))) @ X1))) )),
% 1.65/1.31 inference(pi_clausification,[status(thm)],[f37])).
% 1.65/1.31 thf(f37,plain,(
% 1.65/1.31 ($true = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ Y1 @ emptyset) = (setadjoin @ Y2 @ (setadjoin @ Y0 @ emptyset))) => (Y2 = Y0)))))))))),
% 1.65/1.31 inference(definition_unfolding,[status(thm)],[f35,f26])).
% 1.65/1.31 thf(f26,plain,(
% 1.65/1.31 (upairequniteq = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ Y1 @ emptyset) = (setadjoin @ Y2 @ (setadjoin @ Y0 @ emptyset))) => (Y2 = Y0)))))))))),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f10])).
% 1.65/1.31 thf(f10,plain,(
% 1.65/1.31 (upairequniteq = (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((setadjoin @ Y1 @ emptyset) = (setadjoin @ Y2 @ (setadjoin @ Y0 @ emptyset))) => (Y2 = Y0)))))))))),
% 1.65/1.31 inference(fool_elimination,[status(thm)],[f9])).
% 1.65/1.31 thf(f9,plain,(
% 1.65/1.31 (upairequniteq = ! [X0 : $i,X1 : $i,X2 : $i] : (((setadjoin @ X1 @ emptyset) = (setadjoin @ X0 @ (setadjoin @ X2 @ emptyset))) => (X0 = X2)))),
% 1.65/1.31 inference(rectify,[status(thm)],[f5])).
% 1.65/1.31 thf(f5,axiom,(
% 1.65/1.31 (upairequniteq = ! [X0 : $i,X2 : $i,X1 : $i] : (((setadjoin @ X0 @ (setadjoin @ X1 @ emptyset)) = (setadjoin @ X2 @ emptyset)) => (X0 = X1)))),
% 1.65/1.31 file('/export/starexec/sandbox/tmp/tmp.6JRtvS3WWB/DTF2THF_17983.p',upairequniteq)).
% 1.65/1.31 thf(f35,plain,(
% 1.65/1.31 (upairequniteq = $true)),
% 1.65/1.31 inference(cnf_transformation,[status(thm)],[f24])).
% 1.65/1.31 thf(f115,plain,(
% 1.65/1.31 spl4_3 | spl4_4),
% 1.65/1.31 inference(avatar_split_clause,[status(thm)],[f104,f111,f107])).
% 1.65/1.31 thf(f104,plain,(
% 1.65/1.31 ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset))) | ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ emptyset))),
% 1.65/1.31 inference(trivial_inequality_removal,[status(thm)],[f103])).
% 1.65/1.31 thf(f103,plain,(
% 1.65/1.31 ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ emptyset)) | ((setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) = (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset))) | ($false = $true)),
% 1.65/1.31 inference(superposition,[status(thm)],[f88,f93])).
% 1.65/1.31 thf(f93,plain,(
% 1.65/1.31 ((in @ (setadjoin @ sK2 @ (setadjoin @ sK0 @ emptyset)) @ (setadjoin @ (setadjoin @ sK1 @ emptyset) @ (setadjoin @ (setadjoin @ sK1 @ (setadjoin @ sK3 @ emptyset)) @ emptyset))) = $true)),
% 1.65/1.31 inference(superposition,[status(thm)],[f56,f30])).
% 1.65/1.31 % SZS output end Proof for DTF2THF_17983
% 1.65/1.31 % (18171)------------------------------
% 1.65/1.31 % (18171)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.31 % (18171)Termination reason: Refutation
% 1.65/1.31
% 1.65/1.31 % (18171)Memory used [KB]: 5884
% 1.65/1.31 % (18171)Time elapsed: 0.044 s
% 1.65/1.31 % (18171)Instructions burned: 61 (million)
% 1.65/1.31 % (18171)------------------------------
% 1.65/1.31 % (18171)------------------------------
% 1.65/1.31 % (18170)Success in time 0.054 s
%------------------------------------------------------------------------------