%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU678^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:30:43 AM UTC 2026
% Result : Theorem 0.24s 0.36s
% Output : Refutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 46
% Syntax : Number of formulae : 358 ( 95 unt; 0 typ; 37 def)
% Number of atoms : 3341 ( 736 equ; 3 cnn)
% Maximal formula atoms : 10 ( 9 avg)
% Number of connectives : 4823 ( 339 ~; 674 |; 62 &;3308 @)
% ( 28 <=>; 226 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 248 ( 248 >; 0 *; 0 +; 0 <<)
% Number of symbols : 83 ( 77 usr; 47 con; 0-4 aty)
% ( 161 !!; 25 ??; 0 @@+; 0 @@-)
% Number of variables : 890 ( 0 sgn 371 !; 11 ?; 890 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
in: $i > $i > $o ).
thf(func_def_2,type,
setadjoin: $i > $i > $i ).
thf(func_def_3,type,
dsetconstr: $i > ( $i > $o ) > $i ).
thf(func_def_4,type,
subset: $i > $i > $o ).
thf(func_def_5,type,
kpair: $i > $i > $i ).
thf(func_def_6,type,
cartprod: $i > $i > $i ).
thf(func_def_7,type,
singleton: $i > $o ).
thf(func_def_9,type,
ex1: $i > ( $i > $o ) > $o ).
thf(func_def_10,type,
ex1I: $o ).
thf(func_def_11,type,
breln: $i > $i > $i > $o ).
thf(func_def_12,type,
dpsetconstr: $i > $i > ( $i > $i > $o ) > $i ).
thf(func_def_13,type,
dpsetconstrI: $o ).
thf(func_def_14,type,
setOfPairsIsBReln: $o ).
thf(func_def_15,type,
dpsetconstrERa: $o ).
thf(func_def_16,type,
func: $i > $i > $i > $o ).
thf(func_def_19,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_20,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_22,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_23,type,
vAND: $o > $o > $o ).
thf(func_def_24,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_25,type,
vIMP: $o > $o > $o ).
thf(func_def_26,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_27,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_28,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_29,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_30,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_32,type,
sK1: $i > $i ).
thf(func_def_34,type,
sF3: $o ).
thf(func_def_35,type,
sF4: $o ).
thf(func_def_37,type,
sF6: $o ).
thf(func_def_38,type,
sF7: $i > $o ).
thf(func_def_39,type,
sF8: $i > $i ).
thf(func_def_40,type,
sF9: $i > $o ).
thf(func_def_41,type,
sF10: $o ).
thf(func_def_42,type,
sF11: $o ).
thf(func_def_46,type,
sK15: $i > $i > $o ).
thf(func_def_48,type,
sK17: $i > $i > ( $i > $o ) > $i ).
thf(func_def_49,type,
sK18: $i > ( $i > $o ) > $i ).
thf(func_def_51,type,
sK20: $i > $o ).
thf(func_def_54,type,
sK23: $i > $i > $o ).
thf(func_def_56,type,
sK25: $i > $i ).
thf(func_def_58,type,
sK27: $i > $i > $o ).
thf(f1,axiom,
( ( ^ [X0: $i] :
? [X1: $i] :
( ( in @ X1 @ X0 )
& ( X0
= ( setadjoin @ X1 @ emptyset ) ) ) )
= singleton ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton) ).
thf(f2,axiom,
( ex1
= ( ^ [X0: $i,X1: $i > $o] :
( singleton
@ ( dsetconstr @ X0
@ ^ [X2: $i] : ( X1 @ X2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ex1) ).
thf(f3,axiom,
! [X0: $i,X1: $i > $o,X2: $i] :
( ( ( in @ X2 @ X0 )
=> ( ( X1 @ X2 )
=> ( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ( X1 @ X3 )
=> ( X3 = X2 ) ) )
=> ( ex1 @ X0
@ ^ [X3: $i] : ( X1 @ X3 ) ) ) ) )
= ex1I ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ex1I) ).
thf(f4,axiom,
( ( ^ [X0: $i,X1: $i,X2: $i] : ( subset @ X2 @ ( cartprod @ X0 @ X1 ) ) )
= breln ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',breln) ).
thf(f5,axiom,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i] :
( ( ( in @ X3 @ X0 )
=> ! [X4: $i] :
( ( in @ X4 @ X1 )
=> ( ( X2 @ X3 @ X4 )
=> ( in @ ( kpair @ X3 @ X4 )
@ ( dpsetconstr @ X0 @ X1
@ ^ [X5: $i,X6: $i] : ( X2 @ X5 @ X6 ) ) ) ) ) )
= dpsetconstrI ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dpsetconstrI) ).
thf(f6,axiom,
( setOfPairsIsBReln
= ( ! [X0: $i,X2: $i > $i > $o,X1: $i] :
( breln @ X0 @ X1
@ ( dpsetconstr @ X0 @ X1
@ ^ [X3: $i,X4: $i] : ( X2 @ X3 @ X4 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',setOfPairsIsBReln) ).
thf(f7,axiom,
( dpsetconstrERa
= ( ! [X3: $i,X1: $i,X0: $i,X2: $i > $i > $o] :
( ( in @ X3 @ X0 )
=> ! [X4: $i] :
( ( in @ X4 @ X1 )
=> ( ( in @ ( kpair @ X3 @ X4 )
@ ( dpsetconstr @ X0 @ X1
@ ^ [X5: $i,X6: $i] : ( X2 @ X5 @ X6 ) ) )
=> ( X2 @ X3 @ X4 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dpsetconstrERa) ).
thf(f8,axiom,
( func
= ( ^ [X0: $i,X1: $i,X2: $i] :
( ( breln @ X0 @ X1 @ X2 )
& ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ex1 @ X1
@ ^ [X4: $i] : ( in @ ( kpair @ X3 @ X4 ) @ X2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',func) ).
thf(f9,conjecture,
( ex1I
=> ( dpsetconstrI
=> ( setOfPairsIsBReln
=> ( dpsetconstrERa
=> ! [X1: $i,X2: $i > $i,X0: $i] :
( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( in @ ( X2 @ X3 ) @ X1 ) )
=> ( func @ X0 @ X1
@ ( dpsetconstr @ X0 @ X1
@ ^ [X3: $i,X4: $i] :
( ( X2 @ X3 )
= X4 ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lamProp) ).
thf(f10,negated_conjecture,
~ ( ex1I
=> ( dpsetconstrI
=> ( setOfPairsIsBReln
=> ( dpsetconstrERa
=> ! [X1: $i,X2: $i > $i,X0: $i] :
( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( in @ ( X2 @ X3 ) @ X1 ) )
=> ( func @ X0 @ X1
@ ( dpsetconstr @ X0 @ X1
@ ^ [X3: $i,X4: $i] :
( ( X2 @ X3 )
= X4 ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f9]) ).
thf(f11,plain,
~ ( ex1I
=> ( dpsetconstrI
=> ( setOfPairsIsBReln
=> ( dpsetconstrERa
=> ! [X0: $i,X1: $i > $i,X2: $i] :
( ! [X3: $i] :
( ( in @ X3 @ X2 )
=> ( in @ ( X1 @ X3 ) @ X0 ) )
=> ( func @ X2 @ X0
@ ( dpsetconstr @ X2 @ X0
@ ^ [X4: $i,X5: $i] :
( ( X1 @ X4 )
= X5 ) ) ) ) ) ) ) ),
inference(rectify,[],[f10]) ).
thf(f12,plain,
~ ( ( ex1I = $true )
=> ( ( dpsetconstrI = $true )
=> ( ( setOfPairsIsBReln = $true )
=> ( ( dpsetconstrERa = $true )
=> ! [X1: $i > $i,X2: $i,X0: $i] :
( ! [X3: $i] :
( ( $true
= ( in @ X3 @ X2 ) )
=> ( ( in @ ( X1 @ X3 ) @ X0 )
= $true ) )
=> ( ( func @ X2 @ X0
@ ( dpsetconstr @ X2 @ X0
@ ^ [Y0: $i,Y1: $i] :
( ( X1 @ Y0 )
= Y1 ) ) )
= $true ) ) ) ) ) ),
inference(fool_elimination,[],[f11]) ).
thf(f13,plain,
( func
= ( ^ [X0: $i,X1: $i,X2: $i] :
( ( breln @ X0 @ X1 @ X2 )
& ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ex1 @ X1
@ ^ [X4: $i] : ( in @ ( kpair @ X3 @ X4 ) @ X2 ) ) ) ) ) ),
inference(rectify,[],[f8]) ).
thf(f14,plain,
( func
= ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ex1 @ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( breln @ Y0 @ Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f13]) ).
thf(f15,plain,
( setOfPairsIsBReln
= ( ! [X0: $i,X1: $i > $i > $o,X2: $i] :
( breln @ X0 @ X2
@ ( dpsetconstr @ X0 @ X2
@ ^ [X3: $i,X4: $i] : ( X1 @ X3 @ X4 ) ) ) ) ),
inference(rectify,[],[f6]) ).
thf(f16,plain,
( setOfPairsIsBReln
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( breln @ Y2 @ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f15]) ).
thf(f17,plain,
( dpsetconstrERa
= ( ! [X0: $i,X1: $i,X2: $i,X3: $i > $i > $o] :
( ( in @ X0 @ X2 )
=> ! [X4: $i] :
( ( in @ X4 @ X1 )
=> ( ( in @ ( kpair @ X0 @ X4 )
@ ( dpsetconstr @ X2 @ X1
@ ^ [X5: $i,X6: $i] : ( X3 @ X5 @ X6 ) ) )
=> ( X3 @ X0 @ X4 ) ) ) ) ) ),
inference(rectify,[],[f7]) ).
thf(f18,plain,
( dpsetconstrERa
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f17]) ).
thf(f19,plain,
! [X0: $i > $i > $o,X1: $i,X2: $i,X3: $i] :
( ( ( in @ X1 @ X2 )
=> ! [X4: $i] :
( ( in @ X4 @ X3 )
=> ( ( X0 @ X1 @ X4 )
=> ( in @ ( kpair @ X1 @ X4 )
@ ( dpsetconstr @ X2 @ X3
@ ^ [X5: $i,X6: $i] : ( X0 @ X5 @ X6 ) ) ) ) ) )
= dpsetconstrI ),
inference(rectify,[],[f5]) ).
thf(f20,plain,
( dpsetconstrI
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f19]) ).
thf(f21,plain,
( ex1
= ( ^ [X0: $i,X1: $i > $o] :
( singleton
@ ( dsetconstr @ X0
@ ^ [X2: $i] : ( X1 @ X2 ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f22,plain,
( ex1
= ( ^ [Y0: $i,Y1: $i > $o] :
( singleton
@ ( dsetconstr @ Y0
@ ^ [Y2: $i] : ( Y1 @ Y2 ) ) ) ) ),
inference(fool_elimination,[],[f21]) ).
thf(f23,plain,
( breln
= ( ^ [Y0: $i,Y1: $i,Y2: $i] : ( subset @ Y2 @ ( cartprod @ Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f4]) ).
thf(f24,plain,
! [X0: $i,X1: $i > $o,X2: $i] :
( ( ( in @ X2 @ X0 )
=> ( ( X1 @ X2 )
=> ( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ( X1 @ X3 )
=> ( X3 = X2 ) ) )
=> ( ex1 @ X0
@ ^ [X4: $i] : ( X1 @ X4 ) ) ) ) )
= ex1I ),
inference(rectify,[],[f3]) ).
thf(f25,plain,
( ex1I
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ex1 @ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f24]) ).
thf(f26,plain,
( ( ^ [X0: $i] :
? [X1: $i] :
( ( in @ X1 @ X0 )
& ( X0
= ( setadjoin @ X1 @ emptyset ) ) ) )
= singleton ),
inference(rectify,[],[f1]) ).
thf(f27,plain,
( singleton
= ( ^ [Y0: $i] :
( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= Y0 )
& ( in @ Y1 @ Y0 ) ) ) ) ),
inference(fool_elimination,[],[f26]) ).
thf(f28,plain,
( ? [X2: $i,X1: $i > $i,X0: $i] :
( ( ( func @ X2 @ X0
@ ( dpsetconstr @ X2 @ X0
@ ^ [Y0: $i,Y1: $i] :
( ( X1 @ Y0 )
= Y1 ) ) )
!= $true )
& ! [X3: $i] :
( ( $true
!= ( in @ X3 @ X2 ) )
| ( ( in @ ( X1 @ X3 ) @ X0 )
= $true ) ) )
& ( dpsetconstrERa = $true )
& ( setOfPairsIsBReln = $true )
& ( dpsetconstrI = $true )
& ( ex1I = $true ) ),
inference(ennf_transformation,[],[f12]) ).
thf(f29,plain,
( ( dpsetconstrI = $true )
& ? [X2: $i,X1: $i > $i,X0: $i] :
( ( ( func @ X2 @ X0
@ ( dpsetconstr @ X2 @ X0
@ ^ [Y0: $i,Y1: $i] :
( ( X1 @ Y0 )
= Y1 ) ) )
!= $true )
& ! [X3: $i] :
( ( $true
!= ( in @ X3 @ X2 ) )
| ( ( in @ ( X1 @ X3 ) @ X0 )
= $true ) ) )
& ( dpsetconstrERa = $true )
& ( setOfPairsIsBReln = $true )
& ( ex1I = $true ) ),
inference(flattening,[],[f28]) ).
thf(f30,plain,
( ( dpsetconstrI = $true )
& ? [X0: $i,X1: $i > $i,X2: $i] :
( ( ( func @ X0 @ X2
@ ( dpsetconstr @ X0 @ X2
@ ^ [Y0: $i,Y1: $i] :
( ( X1 @ Y0 )
= Y1 ) ) )
!= $true )
& ! [X3: $i] :
( ( ( in @ X3 @ X0 )
!= $true )
| ( ( in @ ( X1 @ X3 ) @ X2 )
= $true ) ) )
& ( dpsetconstrERa = $true )
& ( setOfPairsIsBReln = $true )
& ( ex1I = $true ) ),
inference(rectify,[],[f29]) ).
thf(f31,plain,
( ( dpsetconstrI = $true )
& ( $true
!= ( func @ sK0 @ sK2
@ ( dpsetconstr @ sK0 @ sK2
@ ^ [Y0: $i,Y1: $i] :
( ( sK1 @ Y0 )
= Y1 ) ) ) )
& ! [X3: $i] :
( ( ( in @ X3 @ sK0 )
!= $true )
| ( ( in @ ( sK1 @ X3 ) @ sK2 )
= $true ) )
& ( dpsetconstrERa = $true )
& ( setOfPairsIsBReln = $true )
& ( ex1I = $true ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f30]) ).
thf(f32,plain,
( ex1I
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ex1 @ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f25]) ).
thf(f33,plain,
( singleton
= ( ^ [Y0: $i] :
( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= Y0 )
& ( in @ Y1 @ Y0 ) ) ) ) ),
inference(cnf_transformation,[],[f27]) ).
thf(f34,plain,
( dpsetconstrERa
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f18]) ).
thf(f35,plain,
( func
= ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ex1 @ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( breln @ Y0 @ Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f14]) ).
thf(f36,plain,
( ex1
= ( ^ [Y0: $i,Y1: $i > $o] :
( singleton
@ ( dsetconstr @ Y0
@ ^ [Y2: $i] : ( Y1 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f22]) ).
thf(f37,plain,
ex1I = $true,
inference(cnf_transformation,[],[f31]) ).
thf(f38,plain,
setOfPairsIsBReln = $true,
inference(cnf_transformation,[],[f31]) ).
thf(f39,plain,
dpsetconstrERa = $true,
inference(cnf_transformation,[],[f31]) ).
thf(f40,plain,
! [X3: $i] :
( ( ( in @ X3 @ sK0 )
!= $true )
| ( ( in @ ( sK1 @ X3 ) @ sK2 )
= $true ) ),
inference(cnf_transformation,[],[f31]) ).
thf(f41,plain,
( $true
!= ( func @ sK0 @ sK2
@ ( dpsetconstr @ sK0 @ sK2
@ ^ [Y0: $i,Y1: $i] :
( ( sK1 @ Y0 )
= Y1 ) ) ) ),
inference(cnf_transformation,[],[f31]) ).
thf(f42,plain,
dpsetconstrI = $true,
inference(cnf_transformation,[],[f31]) ).
thf(f43,plain,
( breln
= ( ^ [Y0: $i,Y1: $i,Y2: $i] : ( subset @ Y2 @ ( cartprod @ Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f23]) ).
thf(f44,plain,
( dpsetconstrI
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f20]) ).
thf(f45,plain,
( setOfPairsIsBReln
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( breln @ Y2 @ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f16]) ).
thf(f48,plain,
( ex1
= ( ^ [Y0: $i,Y1: $i > $o] :
( ^ [Y2: $i] :
( ?? @ $i
@ ^ [Y3: $i] :
( ( ( setadjoin @ Y3 @ emptyset )
= Y2 )
& ( in @ Y3 @ Y2 ) ) )
@ ( dsetconstr @ Y0
@ ^ [Y2: $i] : ( Y1 @ Y2 ) ) ) ) ),
inference(definition_unfolding,[],[f36,f33]) ).
thf(f49,plain,
( func
= ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ^ [Y4: $i,Y5: $i > $o] :
( ^ [Y6: $i] :
( ?? @ $i
@ ^ [Y7: $i] :
( ( ( setadjoin @ Y7 @ emptyset )
= Y6 )
& ( in @ Y7 @ Y6 ) ) )
@ ( dsetconstr @ Y4
@ ^ [Y6: $i] : ( Y5 @ Y6 ) ) )
@ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y0
@ Y1
@ Y2 ) ) ) ),
inference(definition_unfolding,[],[f35,f48,f43]) ).
thf(f50,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ^ [Y3: $i,Y4: $i > $o] :
( ^ [Y5: $i] :
( ?? @ $i
@ ^ [Y6: $i] :
( ( ( setadjoin @ Y6 @ emptyset )
= Y5 )
& ( in @ Y6 @ Y5 ) ) )
@ ( dsetconstr @ Y3
@ ^ [Y5: $i] : ( Y4 @ Y5 ) ) )
@ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f32,f37,f48]) ).
thf(f51,plain,
( $true
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f34,f39]) ).
thf(f52,plain,
( ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ^ [Y4: $i,Y5: $i > $o] :
( ^ [Y6: $i] :
( ?? @ $i
@ ^ [Y7: $i] :
( ( ( setadjoin @ Y7 @ emptyset )
= Y6 )
& ( in @ Y7 @ Y6 ) ) )
@ ( dsetconstr @ Y4
@ ^ [Y6: $i] : ( Y5 @ Y6 ) ) )
@ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y0
@ Y1
@ Y2 ) )
@ sK0
@ sK2
@ ( dpsetconstr @ sK0 @ sK2
@ ^ [Y0: $i,Y1: $i] :
( ( sK1 @ Y0 )
= Y1 ) ) )
!= $true ),
inference(definition_unfolding,[],[f41,f49]) ).
thf(f53,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f44,f42]) ).
thf(f54,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y2
@ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f45,f38,f43]) ).
thf(f55,definition,
( sF3
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ^ [Y3: $i,Y4: $i > $o] :
( ^ [Y5: $i] :
( ?? @ $i
@ ^ [Y6: $i] :
( ( ( setadjoin @ Y6 @ emptyset )
= Y5 )
& ( in @ Y6 @ Y5 ) ) )
@ ( dsetconstr @ Y3
@ ^ [Y5: $i] : ( Y4 @ Y5 ) ) )
@ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
thf(f56,plain,
sF3 = $true,
inference(definition_folding,[],[f50,f55]) ).
thf(f57,definition,
( sF4
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
thf(f58,plain,
sF4 = $true,
inference(definition_folding,[],[f51,f57]) ).
thf(f59,definition,
( sF5
= ( dpsetconstr @ sK0 @ sK2
@ ^ [Y0: $i,Y1: $i] :
( ( sK1 @ Y0 )
= Y1 ) ) ),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
thf(f60,definition,
( sF6
= ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ^ [Y4: $i,Y5: $i > $o] :
( ^ [Y6: $i] :
( ?? @ $i
@ ^ [Y7: $i] :
( ( ( setadjoin @ Y7 @ emptyset )
= Y6 )
& ( in @ Y7 @ Y6 ) ) )
@ ( dsetconstr @ Y4
@ ^ [Y6: $i] : ( Y5 @ Y6 ) ) )
@ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y0
@ Y1
@ Y2 ) )
@ sK0
@ sK2
@ sF5 ) ),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
thf(f61,plain,
sF6 != $true,
inference(definition_folding,[],[f52,f60,f59]) ).
thf(f62,definition,
! [X3: $i] :
( ( sF7 @ X3 )
= ( in @ X3 @ sK0 ) ),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
thf(f63,plain,
! [X3: $i] :
( ( in @ X3 @ sK0 )
= ( sF7 @ X3 ) ),
inference(reorient_equations,[],[f62]) ).
thf(f64,definition,
! [X3: $i] :
( ( sF8 @ X3 )
= ( sK1 @ X3 ) ),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
thf(f65,plain,
! [X3: $i] :
( ( sK1 @ X3 )
= ( sF8 @ X3 ) ),
inference(reorient_equations,[],[f64]) ).
thf(f66,definition,
! [X3: $i] :
( ( sF9 @ X3 )
= ( in @ ( sF8 @ X3 ) @ sK2 ) ),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
thf(f67,plain,
! [X3: $i] :
( ( in @ ( sF8 @ X3 ) @ sK2 )
= ( sF9 @ X3 ) ),
inference(reorient_equations,[],[f66]) ).
thf(f68,plain,
! [X3: $i] :
( ( ( sF9 @ X3 )
= $true )
| ( ( sF7 @ X3 )
!= $true ) ),
inference(definition_folding,[],[f40,f67,f65,f63]) ).
thf(f69,definition,
( sF10
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
thf(f70,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) )
= sF10 ),
inference(reorient_equations,[],[f69]) ).
thf(f71,plain,
sF10 = $true,
inference(definition_folding,[],[f53,f70]) ).
thf(f72,definition,
( sF11
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y2
@ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
thf(f73,plain,
sF11 = $true,
inference(definition_folding,[],[f54,f72]) ).
thf(f74,plain,
( ( sF10 = $false )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) ) )
= $true ) ),
inference(iff_proxy_clausification,[],[f70]) ).
thf(f92,plain,
! [X1: $i] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( in @ Y2 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y0 )
=> ( ( Y3 @ Y2 @ Y4 )
=> ( in @ ( kpair @ Y2 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y0
@ ^ [Y5: $i,Y6: $i] : ( Y3 @ Y5 @ Y6 ) ) ) ) ) ) ) ) ) )
@ X1 )
= $true )
| ( sF10 = $false ) ),
inference(pi_proxy_clausification,[],[f74]) ).
thf(f93,plain,
! [X1: $i] :
( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y2: $i > $i > $o] :
( ( in @ Y1 @ Y0 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ X1 )
=> ( ( Y2 @ Y1 @ Y3 )
=> ( in @ ( kpair @ Y1 @ Y3 ) @ ( dpsetconstr @ Y0 @ X1 @ Y2 ) ) ) ) ) ) ) ) )
= $true )
| ( sF10 = $false ) ),
inference(beta-eta_normalization,[],[f92]) ).
thf(f94,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y2: $i > $i > $o] :
( ( in @ Y1 @ Y0 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ X1 )
=> ( ( Y2 @ Y1 @ Y3 )
=> ( in @ ( kpair @ Y1 @ Y3 ) @ ( dpsetconstr @ Y0 @ X1 @ Y2 ) ) ) ) ) ) ) )
@ X2 ) )
| ( sF10 = $false ) ),
inference(pi_proxy_clausification,[],[f93]) ).
thf(f95,plain,
! [X2: $i,X1: $i] :
( ( sF10 = $false )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( in @ Y0 @ X2 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ X1 )
=> ( ( Y1 @ Y0 @ Y2 )
=> ( in @ ( kpair @ Y0 @ Y2 ) @ ( dpsetconstr @ X2 @ X1 @ Y1 ) ) ) ) ) ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f94]) ).
thf(f96,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( in @ Y0 @ X2 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ X1 )
=> ( ( Y1 @ Y0 @ Y2 )
=> ( in @ ( kpair @ Y0 @ Y2 ) @ ( dpsetconstr @ X2 @ X1 @ Y1 ) ) ) ) ) ) )
@ X3 )
= $true )
| ( sF10 = $false ) ),
inference(pi_proxy_clausification,[],[f95]) ).
thf(f97,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( sF10 = $false )
| ( $true
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( ( in @ X3 @ X2 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X1 )
=> ( ( Y0 @ X3 @ Y1 )
=> ( in @ ( kpair @ X3 @ Y1 ) @ ( dpsetconstr @ X2 @ X1 @ Y0 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f96]) ).
thf(f98,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o] :
( ( sF10 = $false )
| ( $true
= ( ^ [Y0: $i > $i > $o] :
( ( in @ X3 @ X2 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X1 )
=> ( ( Y0 @ X3 @ Y1 )
=> ( in @ ( kpair @ X3 @ Y1 ) @ ( dpsetconstr @ X2 @ X1 @ Y0 ) ) ) ) ) )
@ X4 ) ) ),
inference(pi_proxy_clausification,[],[f97]) ).
thf(f99,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o] :
( ( ( ( in @ X3 @ X2 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X1 )
=> ( ( X4 @ X3 @ Y0 )
=> ( in @ ( kpair @ X3 @ Y0 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) ) ) ) ) )
= $true )
| ( sF10 = $false ) ),
inference(beta-eta_normalization,[],[f98]) ).
thf(f100,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o] :
( ( $false
= ( in @ X3 @ X2 ) )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X1 )
=> ( ( X4 @ X3 @ Y0 )
=> ( in @ ( kpair @ X3 @ Y0 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) ) ) ) )
= $true )
| ( sF10 = $false ) ),
inference(imp_proxy_clausification,[],[f99]) ).
thf(f101,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o,X5: $i] :
( ( ( ^ [Y0: $i] :
( ( in @ Y0 @ X1 )
=> ( ( X4 @ X3 @ Y0 )
=> ( in @ ( kpair @ X3 @ Y0 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) ) ) )
@ X5 )
= $true )
| ( sF10 = $false )
| ( $false
= ( in @ X3 @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f100]) ).
thf(f102,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o,X5: $i] :
( ( ( ( in @ X5 @ X1 )
=> ( ( X4 @ X3 @ X5 )
=> ( in @ ( kpair @ X3 @ X5 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) ) ) )
= $true )
| ( sF10 = $false )
| ( $false
= ( in @ X3 @ X2 ) ) ),
inference(beta-eta_normalization,[],[f101]) ).
thf(f103,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o,X5: $i] :
( ( sF10 = $false )
| ( $false
= ( in @ X3 @ X2 ) )
| ( ( ( X4 @ X3 @ X5 )
=> ( in @ ( kpair @ X3 @ X5 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) ) )
= $true )
| ( $false
= ( in @ X5 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f102]) ).
thf(f104,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o,X5: $i] :
( ( $false
= ( in @ X5 @ X1 ) )
| ( ( in @ ( kpair @ X3 @ X5 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) )
= $true )
| ( sF10 = $false )
| ( $false
= ( in @ X3 @ X2 ) )
| ( $false
= ( X4 @ X3 @ X5 ) ) ),
inference(imp_proxy_clausification,[],[f103]) ).
thf(f105,plain,
! [X3: $i] :
( ( ( in @ ( sF8 @ X3 ) @ sK2 )
= $true )
| ( $false
= ( sF9 @ X3 ) ) ),
inference(iff_proxy_clausification,[],[f67]) ).
thf(f108,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ^ [Y3: $i,Y4: $i > $o] :
( ^ [Y5: $i] :
( ?? @ $i
@ ^ [Y6: $i] :
( ( ( setadjoin @ Y6 @ emptyset )
= Y5 )
& ( in @ Y6 @ Y5 ) ) )
@ ( dsetconstr @ Y3
@ ^ [Y5: $i] : ( Y4 @ Y5 ) ) )
@ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) ) )
= $true )
| ( $false = sF3 ) ),
inference(iff_proxy_clausification,[],[f55]) ).
thf(f109,plain,
! [X1: $i] :
( ( $false = sF3 )
| ( ( ^ [Y0: $i] :
( !! @ ( $i > $o )
@ ^ [Y1: $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y0 @ Y2 )
=> ( ( Y1 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y2 )
=> ( ( Y1 @ Y3 )
=> ( Y0 = Y3 ) ) ) )
=> ( ^ [Y3: $i,Y4: $i > $o] :
( ^ [Y5: $i] :
( ?? @ $i
@ ^ [Y6: $i] :
( ( ( setadjoin @ Y6 @ emptyset )
= Y5 )
& ( in @ Y6 @ Y5 ) ) )
@ ( dsetconstr @ Y3
@ ^ [Y5: $i] : ( Y4 @ Y5 ) ) )
@ Y2
@ ^ [Y3: $i] : ( Y1 @ Y3 ) ) ) ) ) ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f108]) ).
thf(f110,plain,
! [X1: $i] :
( ( ( !! @ ( $i > $o )
@ ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ X1 @ Y1 )
=> ( ( Y0 @ X1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( X1 = Y2 ) ) ) )
=> ( ?? @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y2 @ emptyset )
= ( dsetconstr @ Y1 @ Y0 ) )
& ( in @ Y2 @ ( dsetconstr @ Y1 @ Y0 ) ) ) ) ) ) ) ) )
= $true )
| ( $false = sF3 ) ),
inference(beta-eta_normalization,[],[f109]) ).
thf(f111,plain,
! [X2: $i > $o,X1: $i] :
( ( $true
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ X1 @ Y1 )
=> ( ( Y0 @ X1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( X1 = Y2 ) ) ) )
=> ( ?? @ $i
@ ^ [Y2: $i] :
( ( ( setadjoin @ Y2 @ emptyset )
= ( dsetconstr @ Y1 @ Y0 ) )
& ( in @ Y2 @ ( dsetconstr @ Y1 @ Y0 ) ) ) ) ) ) ) )
@ X2 ) )
| ( $false = sF3 ) ),
inference(pi_proxy_clausification,[],[f110]) ).
thf(f112,plain,
! [X2: $i > $o,X1: $i] :
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X1 @ Y0 )
=> ( ( X2 @ X1 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( X2 @ Y1 )
=> ( X1 = Y1 ) ) ) )
=> ( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( dsetconstr @ Y0 @ X2 ) )
& ( in @ Y1 @ ( dsetconstr @ Y0 @ X2 ) ) ) ) ) ) ) )
= $true )
| ( $false = sF3 ) ),
inference(beta-eta_normalization,[],[f111]) ).
thf(f113,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( ^ [Y0: $i] :
( ( in @ X1 @ Y0 )
=> ( ( X2 @ X1 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( X2 @ Y1 )
=> ( X1 = Y1 ) ) ) )
=> ( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( dsetconstr @ Y0 @ X2 ) )
& ( in @ Y1 @ ( dsetconstr @ Y0 @ X2 ) ) ) ) ) ) )
@ X3 )
= $true ) ),
inference(pi_proxy_clausification,[],[f112]) ).
thf(f114,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( ( in @ X1 @ X3 )
=> ( ( X2 @ X1 )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) ) )
=> ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) ) ) ) ) )
= $true )
| ( $false = sF3 ) ),
inference(beta-eta_normalization,[],[f113]) ).
thf(f115,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( ( X2 @ X1 )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) ) )
=> ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) ) ) ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f114]) ).
thf(f116,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) ) )
=> ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) ) ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( $false = sF3 )
| ( ( X2 @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f115]) ).
thf(f117,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( X2 @ X1 )
= $false )
| ( $false = sF3 )
| ( ( in @ X1 @ X3 )
= $false )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) ) ) )
| ( ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f116]) ).
thf(f118,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( $false
= ( ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) )
@ ( sK17 @ X3 @ X1 @ X2 ) ) )
| ( $false = sF3 ) ),
inference(sigma_proxy_clausification,[],[f117]) ).
thf(f119,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( $false
= ( ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( X2 @ Y0 )
=> ( X1 = Y0 ) ) )
@ ( sK17 @ X3 @ X1 @ X2 ) ) )
| ( $false = sF3 )
| ( ( ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ Y0 @ ( dsetconstr @ X3 @ X2 ) ) )
@ ( sK18 @ X3 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false ) ),
inference(sigma_proxy_clausification,[],[f118]) ).
thf(f120,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false
= ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
=> ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
=> ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) ) )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) ) )
= $true )
| ( $false = sF3 )
| ( ( X2 @ X1 )
= $false ) ),
inference(beta-eta_normalization,[],[f119]) ).
thf(f121,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( $false = sF3 )
| ( ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( $false
= ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
=> ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f120]) ).
thf(f122,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
& ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) ) )
= $true )
| ( $false = sF3 )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f120]) ).
thf(f123,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ X1 )
= $false ) ),
inference(and_proxy_clausification,[],[f122]) ).
thf(f124,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( X2 @ X1 )
= $false ) ),
inference(and_proxy_clausification,[],[f122]) ).
thf(f125,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( $false = sF3 )
| ( ( in @ X1 @ X3 )
= $false ) ),
inference(equality_proxy_clausification,[],[f124]) ).
thf(f126,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( $false = sF3 )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( $false
= ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
=> ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) ) ),
inference(and_proxy_clausification,[],[f121]) ).
thf(f127,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( X2 @ X1 )
= $false )
| ( $false
= ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
=> ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) )
| ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false ) ),
inference(and_proxy_clausification,[],[f121]) ).
thf(f128,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( $false
= ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) )
| ( $false = sF3 )
| ( ( X2 @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f127]) ).
thf(f129,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f127]) ).
thf(f130,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( $false = sF3 )
| ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false ) ),
inference(equality_proxy_clausification,[],[f129]) ).
thf(f131,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( $false = sF3 )
| ( $false
= ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f128]) ).
thf(f132,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( X2 @ X1 )
= $false )
| ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( in @ X1 @ X3 )
= $false )
| ( $false = sF3 )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f131]) ).
thf(f133,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( X2 @ X1 )
= $false )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( $false = sF3 )
| ( ( in @ X1 @ X3 )
= $false )
| ( $false
= ( X1
= ( sK17 @ X3 @ X1 @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f126]) ).
thf(f134,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( $false = sF3 )
| ( ( X2 @ X1 )
= $false )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f126]) ).
thf(f135,plain,
! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( $false = sF3 )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ X1 )
= $false ) ),
inference(equality_proxy_clausification,[],[f133]) ).
thf(f157,plain,
( sF5
= ( dpsetconstr @ sK0 @ sK2
@ ^ [Y0: $i] : ( (=) @ ( sK1 @ Y0 ) ) ) ),
inference(beta-eta_normalization,[],[f59]) ).
thf(f159,plain,
( ( $false = sF11 )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y2
@ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) ) )
= $true ) ),
inference(iff_proxy_clausification,[],[f72]) ).
thf(f160,plain,
! [X1: $i] :
( ( $false = sF11 )
| ( ( ^ [Y0: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y2
@ Y0
@ ( dpsetconstr @ Y2 @ Y0
@ ^ [Y3: $i,Y4: $i] : ( Y1 @ Y3 @ Y4 ) ) ) ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f159]) ).
thf(f161,plain,
! [X1: $i] :
( ( ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( subset @ ( dpsetconstr @ Y1 @ X1 @ Y0 ) @ ( cartprod @ Y1 @ X1 ) ) ) )
= $true )
| ( $false = sF11 ) ),
inference(beta-eta_normalization,[],[f160]) ).
thf(f162,plain,
! [X2: $i > $i > $o,X1: $i] :
( ( $false = sF11 )
| ( ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( subset @ ( dpsetconstr @ Y1 @ X1 @ Y0 ) @ ( cartprod @ Y1 @ X1 ) ) )
@ X2 )
= $true ) ),
inference(pi_proxy_clausification,[],[f161]) ).
thf(f163,plain,
! [X2: $i > $i > $o,X1: $i] :
( ( $false = sF11 )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] : ( subset @ ( dpsetconstr @ Y0 @ X1 @ X2 ) @ ( cartprod @ Y0 @ X1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f162]) ).
thf(f164,plain,
! [X2: $i > $i > $o,X3: $i,X1: $i] :
( ( $false = sF11 )
| ( $true
= ( ^ [Y0: $i] : ( subset @ ( dpsetconstr @ Y0 @ X1 @ X2 ) @ ( cartprod @ Y0 @ X1 ) )
@ X3 ) ) ),
inference(pi_proxy_clausification,[],[f163]) ).
thf(f165,plain,
! [X2: $i > $i > $o,X3: $i,X1: $i] :
( ( ( subset @ ( dpsetconstr @ X3 @ X1 @ X2 ) @ ( cartprod @ X3 @ X1 ) )
= $true )
| ( $false = sF11 ) ),
inference(beta-eta_normalization,[],[f164]) ).
thf(f172,plain,
( ( $false
= ( ^ [Y0: $i,Y1: $i,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ^ [Y4: $i,Y5: $i > $o] :
( ^ [Y6: $i] :
( ?? @ $i
@ ^ [Y7: $i] :
( ( ( setadjoin @ Y7 @ emptyset )
= Y6 )
& ( in @ Y7 @ Y6 ) ) )
@ ( dsetconstr @ Y4
@ ^ [Y6: $i] : ( Y5 @ Y6 ) ) )
@ Y1
@ ^ [Y4: $i] : ( in @ ( kpair @ Y3 @ Y4 ) @ Y2 ) ) ) )
& ( ^ [Y3: $i,Y4: $i,Y5: $i] : ( subset @ Y5 @ ( cartprod @ Y3 @ Y4 ) )
@ Y0
@ Y1
@ Y2 ) )
@ sK0
@ sK2
@ sF5 ) )
| ( sF6 = $true ) ),
inference(iff_proxy_clausification,[],[f60]) ).
thf(f185,plain,
( ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK0 )
=> ( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) )
& ( in @ Y1
@ ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) ) ) ) ) )
& ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) ) )
| ( sF6 = $true ) ),
inference(beta-eta_normalization,[],[f172]) ).
thf(f186,plain,
( ( sF6 = $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK0 )
=> ( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) )
& ( in @ Y1
@ ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) ) ) ) ) ) )
| ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) ) ),
inference(and_proxy_clausification,[],[f185]) ).
thf(f187,plain,
( ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( sF6 = $true )
| ( $false
= ( ^ [Y0: $i] :
( ( in @ Y0 @ sK0 )
=> ( ?? @ $i
@ ^ [Y1: $i] :
( ( ( setadjoin @ Y1 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) )
& ( in @ Y1
@ ( dsetconstr @ sK2
@ ^ [Y2: $i] : ( in @ ( kpair @ Y0 @ Y2 ) @ sF5 ) ) ) ) ) )
@ sK26 ) ) ),
inference(sigma_proxy_clausification,[],[f186]) ).
thf(f188,plain,
( ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( sF6 = $true )
| ( ( ( in @ sK26 @ sK0 )
=> ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) )
& ( in @ Y0
@ ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) ) ) ) )
= $false ) ),
inference(beta-eta_normalization,[],[f187]) ).
thf(f189,plain,
( ( ( ?? @ $i
@ ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) )
& ( in @ Y0
@ ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) ) ) )
= $false )
| ( sF6 = $true )
| ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) ) ),
inference(imp_proxy_clausification,[],[f188]) ).
thf(f190,plain,
( ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( sF6 = $true )
| ( ( in @ sK26 @ sK0 )
= $true ) ),
inference(imp_proxy_clausification,[],[f188]) ).
thf(f191,plain,
! [X1: $i] :
( ( sF6 = $true )
| ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( $false
= ( ^ [Y0: $i] :
( ( ( setadjoin @ Y0 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) )
& ( in @ Y0
@ ( dsetconstr @ sK2
@ ^ [Y1: $i] : ( in @ ( kpair @ sK26 @ Y1 ) @ sF5 ) ) ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f189]) ).
thf(f192,plain,
! [X1: $i] :
( ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( $false
= ( ( ( setadjoin @ X1 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
& ( in @ X1
@ ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) ) )
| ( sF6 = $true ) ),
inference(beta-eta_normalization,[],[f191]) ).
thf(f193,plain,
! [X1: $i] :
( ( ( in @ X1
@ ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $false )
| ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( $false
= ( ( setadjoin @ X1 @ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) )
| ( sF6 = $true ) ),
inference(and_proxy_clausification,[],[f192]) ).
thf(f194,plain,
! [X1: $i] :
( ( ( setadjoin @ X1 @ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ( sF6 = $true )
| ( ( in @ X1
@ ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $false ) ),
inference(equality_proxy_clausification,[],[f193]) ).
thf(f196,plain,
! [X3: $i] :
( ( $false
= ( in @ X3 @ sK0 ) )
| ( ( sF7 @ X3 )
= $true ) ),
inference(iff_proxy_clausification,[],[f63]) ).
thf(f198,plain,
( ( $true
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ) )
| ( $false = sF4 ) ),
inference(iff_proxy_clausification,[],[f57]) ).
thf(f199,plain,
! [X1: $i > $i > $o] :
( ( ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y2 )
=> ( ( in @ ( kpair @ Y3 @ Y4 )
@ ( dpsetconstr @ Y1 @ Y2
@ ^ [Y5: $i,Y6: $i] : ( Y0 @ Y5 @ Y6 ) ) )
=> ( Y0 @ Y3 @ Y4 ) ) ) ) ) ) ) )
@ X1 )
= $true )
| ( $false = sF4 ) ),
inference(pi_proxy_clausification,[],[f198]) ).
thf(f200,plain,
! [X1: $i > $i > $o] :
( ( $false = sF4 )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ ( kpair @ Y2 @ Y3 ) @ ( dpsetconstr @ Y0 @ Y1 @ X1 ) )
=> ( X1 @ Y2 @ Y3 ) ) ) ) ) ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f199]) ).
thf(f201,plain,
! [X2: $i,X1: $i > $i > $o] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ ( kpair @ Y2 @ Y3 ) @ ( dpsetconstr @ Y0 @ Y1 @ X1 ) )
=> ( X1 @ Y2 @ Y3 ) ) ) ) ) ) )
@ X2 )
= $true )
| ( $false = sF4 ) ),
inference(pi_proxy_clausification,[],[f200]) ).
thf(f202,plain,
! [X2: $i,X1: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( ( in @ ( kpair @ Y1 @ Y2 ) @ ( dpsetconstr @ X2 @ Y0 @ X1 ) )
=> ( X1 @ Y1 @ Y2 ) ) ) ) ) ) )
= $true )
| ( $false = sF4 ) ),
inference(beta-eta_normalization,[],[f201]) ).
thf(f203,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( ( in @ ( kpair @ Y1 @ Y2 ) @ ( dpsetconstr @ X2 @ Y0 @ X1 ) )
=> ( X1 @ Y1 @ Y2 ) ) ) ) ) )
@ X3 )
= $true )
| ( $false = sF4 ) ),
inference(pi_proxy_clausification,[],[f202]) ).
thf(f204,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o] :
( ( $false = sF4 )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X3 )
=> ( ( in @ ( kpair @ Y0 @ Y1 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ Y0 @ Y1 ) ) ) ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f203]) ).
thf(f205,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i] :
( ( $false = sF4 )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X3 )
=> ( ( in @ ( kpair @ Y0 @ Y1 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ Y0 @ Y1 ) ) ) ) )
@ X4 )
= $true ) ),
inference(pi_proxy_clausification,[],[f204]) ).
thf(f206,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i] :
( ( $false = sF4 )
| ( ( ( in @ X4 @ X2 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( in @ ( kpair @ X4 @ Y0 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ X4 @ Y0 ) ) ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f205]) ).
thf(f207,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i] :
( ( $false = sF4 )
| ( $false
= ( in @ X4 @ X2 ) )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( in @ ( kpair @ X4 @ Y0 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ X4 @ Y0 ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f206]) ).
thf(f208,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( $false
= ( in @ X4 @ X2 ) )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ X3 )
=> ( ( in @ ( kpair @ X4 @ Y0 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ X4 @ Y0 ) ) )
@ X5 )
= $true )
| ( $false = sF4 ) ),
inference(pi_proxy_clausification,[],[f207]) ).
thf(f209,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( $false = sF4 )
| ( $false
= ( in @ X4 @ X2 ) )
| ( ( ( in @ X5 @ X3 )
=> ( ( in @ ( kpair @ X4 @ X5 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ X4 @ X5 ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f208]) ).
thf(f210,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( $false = sF4 )
| ( $false
= ( in @ X5 @ X3 ) )
| ( ( ( in @ ( kpair @ X4 @ X5 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) )
=> ( X1 @ X4 @ X5 ) )
= $true )
| ( $false
= ( in @ X4 @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f209]) ).
thf(f211,plain,
! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( $false
= ( in @ X4 @ X2 ) )
| ( ( X1 @ X4 @ X5 )
= $true )
| ( $false = sF4 )
| ( $false
= ( in @ X5 @ X3 ) )
| ( $false
= ( in @ ( kpair @ X4 @ X5 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) ) ) ),
inference(imp_proxy_clausification,[],[f210]) ).
thf(f229,definition,
( spl32_1
<=> ( sF10 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
thf(f231,plain,
( ( sF10 = $true )
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f229]) ).
thf(f253,definition,
( spl32_6
<=> ( sF10 = $false ) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
thf(f255,plain,
( ( sF10 = $false )
| ~ spl32_6 ),
inference(avatar_component_clause,[],[f253]) ).
thf(f257,definition,
( spl32_7
<=> ! [X2: $i,X3: $i,X4: $i > $i > $o,X5: $i,X1: $i] :
( ( $false
= ( in @ X5 @ X1 ) )
| ( $false
= ( X4 @ X3 @ X5 ) )
| ( $false
= ( in @ X3 @ X2 ) )
| ( ( in @ ( kpair @ X3 @ X5 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition]) ).
thf(f258,plain,
( ! [X2: $i,X3: $i,X1: $i,X4: $i > $i > $o,X5: $i] :
( ( ( in @ ( kpair @ X3 @ X5 ) @ ( dpsetconstr @ X2 @ X1 @ X4 ) )
= $true )
| ( $false
= ( X4 @ X3 @ X5 ) )
| ( $false
= ( in @ X5 @ X1 ) )
| ( $false
= ( in @ X3 @ X2 ) ) )
| ~ spl32_7 ),
inference(avatar_component_clause,[],[f257]) ).
thf(f259,plain,
( spl32_6
| spl32_7 ),
inference(avatar_split_clause,[],[f104,f257,f253]) ).
thf(f261,definition,
( spl32_8
<=> ( $false = sF3 ) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
thf(f263,plain,
( ( $false = sF3 )
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f261]) ).
thf(f265,definition,
( spl32_9
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
thf(f266,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( X2 @ X1 )
= $false ) )
| ~ spl32_9 ),
inference(avatar_component_clause,[],[f265]) ).
thf(f267,plain,
( spl32_8
| spl32_9 ),
inference(avatar_split_clause,[],[f125,f265,f261]) ).
thf(f269,definition,
( spl32_10
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
thf(f270,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ ( sK17 @ X3 @ X1 @ X2 ) @ X3 )
= $true ) )
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f269]) ).
thf(f271,plain,
( spl32_8
| spl32_10 ),
inference(avatar_split_clause,[],[f123,f269,f261]) ).
thf(f273,definition,
( spl32_11
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( X2 @ X1 )
= $false )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition]) ).
thf(f274,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true ) )
| ~ spl32_11 ),
inference(avatar_component_clause,[],[f273]) ).
thf(f275,plain,
( spl32_8
| spl32_11 ),
inference(avatar_split_clause,[],[f130,f273,f261]) ).
thf(f277,definition,
( spl32_12
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( X2 @ X1 )
= $false )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
thf(f278,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( setadjoin @ ( sK18 @ X3 @ X2 ) @ emptyset )
= ( dsetconstr @ X3 @ X2 ) )
| ( ( X2 @ X1 )
= $false )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 )
| ( ( in @ X1 @ X3 )
= $false ) )
| ~ spl32_12 ),
inference(avatar_component_clause,[],[f277]) ).
thf(f279,plain,
( spl32_12
| spl32_8 ),
inference(avatar_split_clause,[],[f132,f261,f277]) ).
thf(f281,definition,
( spl32_13
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( in @ X1 @ X3 )
= $false )
| ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl32_13])],[avatar_definition]) ).
thf(f282,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( X2 @ ( sK17 @ X3 @ X1 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false ) )
| ~ spl32_13 ),
inference(avatar_component_clause,[],[f281]) ).
thf(f283,plain,
( spl32_8
| spl32_13 ),
inference(avatar_split_clause,[],[f134,f281,f261]) ).
thf(f285,definition,
( spl32_14
<=> ! [X2: $i > $o,X1: $i,X3: $i] :
( ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 ) ) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
thf(f286,plain,
( ! [X2: $i > $o,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X2 ) @ ( dsetconstr @ X3 @ X2 ) )
= $true )
| ( ( X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false )
| ( ( sK17 @ X3 @ X1 @ X2 )
!= X1 ) )
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f285]) ).
thf(f287,plain,
( spl32_8
| spl32_14 ),
inference(avatar_split_clause,[],[f135,f285,f261]) ).
thf(f293,definition,
( spl32_16
<=> ( sF3 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
thf(f295,plain,
( ( sF3 = $true )
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f293]) ).
thf(f310,plain,
spl32_16,
inference(avatar_split_clause,[],[f56,f293]) ).
thf(f312,definition,
( spl32_20
<=> ! [X2: $i > $i > $o,X1: $i,X3: $i] :
( ( subset @ ( dpsetconstr @ X3 @ X1 @ X2 ) @ ( cartprod @ X3 @ X1 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
thf(f313,plain,
( ! [X2: $i > $i > $o,X3: $i,X1: $i] :
( ( subset @ ( dpsetconstr @ X3 @ X1 @ X2 ) @ ( cartprod @ X3 @ X1 ) )
= $true )
| ~ spl32_20 ),
inference(avatar_component_clause,[],[f312]) ).
thf(f315,definition,
( spl32_21
<=> ( $false = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
thf(f317,plain,
( ( $false = sF11 )
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f315]) ).
thf(f318,plain,
( spl32_20
| spl32_21 ),
inference(avatar_split_clause,[],[f165,f315,f312]) ).
thf(f320,definition,
( spl32_22
<=> ( sF11 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_22])],[avatar_definition]) ).
thf(f322,plain,
( ( sF11 = $true )
| ~ spl32_22 ),
inference(avatar_component_clause,[],[f320]) ).
thf(f346,definition,
( spl32_28
<=> ( ( in @ sK26 @ sK0 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
thf(f348,plain,
( ( ( in @ sK26 @ sK0 )
= $true )
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f346]) ).
thf(f350,definition,
( spl32_29
<=> ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
thf(f352,plain,
( ( $false
= ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) ) )
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f350]) ).
thf(f354,definition,
( spl32_30
<=> ( sF6 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_30])],[avatar_definition]) ).
thf(f357,plain,
( spl32_28
| spl32_29
| spl32_30 ),
inference(avatar_split_clause,[],[f190,f354,f350,f346]) ).
thf(f359,definition,
( spl32_31
<=> ! [X1: $i] :
( ( ( setadjoin @ X1 @ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( ( in @ X1
@ ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl32_31])],[avatar_definition]) ).
thf(f360,plain,
( ! [X1: $i] :
( ( ( in @ X1
@ ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $false )
| ( ( setadjoin @ X1 @ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) )
| ~ spl32_31 ),
inference(avatar_component_clause,[],[f359]) ).
thf(f361,plain,
( spl32_29
| spl32_31
| spl32_30 ),
inference(avatar_split_clause,[],[f194,f354,f359,f350]) ).
thf(f362,plain,
spl32_1,
inference(avatar_split_clause,[],[f71,f229]) ).
thf(f364,definition,
( spl32_32
<=> ! [X5: $i,X4: $i,X3: $i,X2: $i,X1: $i > $i > $o] :
( ( $false
= ( in @ X4 @ X2 ) )
| ( $false
= ( in @ ( kpair @ X4 @ X5 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) ) )
| ( $false
= ( in @ X5 @ X3 ) )
| ( ( X1 @ X4 @ X5 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl32_32])],[avatar_definition]) ).
thf(f365,plain,
( ! [X2: $i,X3: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( $false
= ( in @ ( kpair @ X4 @ X5 ) @ ( dpsetconstr @ X2 @ X3 @ X1 ) ) )
| ( ( X1 @ X4 @ X5 )
= $true )
| ( $false
= ( in @ X5 @ X3 ) )
| ( $false
= ( in @ X4 @ X2 ) ) )
| ~ spl32_32 ),
inference(avatar_component_clause,[],[f364]) ).
thf(f367,definition,
( spl32_33
<=> ( $false = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl32_33])],[avatar_definition]) ).
thf(f369,plain,
( ( $false = sF4 )
| ~ spl32_33 ),
inference(avatar_component_clause,[],[f367]) ).
thf(f370,plain,
( spl32_32
| spl32_33 ),
inference(avatar_split_clause,[],[f211,f367,f364]) ).
thf(f372,definition,
( spl32_34
<=> ( sF4 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_34])],[avatar_definition]) ).
thf(f374,plain,
( ( sF4 = $true )
| ~ spl32_34 ),
inference(avatar_component_clause,[],[f372]) ).
thf(f395,plain,
spl32_34,
inference(avatar_split_clause,[],[f58,f372]) ).
thf(f396,plain,
~ spl32_30,
inference(avatar_split_clause,[],[f61,f354]) ).
thf(f397,plain,
spl32_22,
inference(avatar_split_clause,[],[f73,f320]) ).
thf(f398,plain,
( ( $false = $true )
| ~ spl32_1
| ~ spl32_6 ),
inference(forward_demodulation,[],[f231,f255]) ).
thf(f399,plain,
( $false
| ~ spl32_1
| ~ spl32_6 ),
inference(trivial_inequality_removal,[],[f398]) ).
thf(f400,plain,
( ~ spl32_1
| ~ spl32_6 ),
inference(avatar_contradiction_clause,[],[f399]) ).
thf(f413,plain,
( ( $false = $true )
| ~ spl32_8
| ~ spl32_16 ),
inference(forward_demodulation,[],[f263,f295]) ).
thf(f414,plain,
( $false
| ~ spl32_8
| ~ spl32_16 ),
inference(trivial_inequality_removal,[],[f413]) ).
thf(f415,plain,
( ~ spl32_8
| ~ spl32_16 ),
inference(avatar_contradiction_clause,[],[f414]) ).
thf(f434,plain,
( ( ( subset @ sF5 @ ( cartprod @ sK0 @ sK2 ) )
= $true )
| ~ spl32_20 ),
inference(constrained_superposition,[],[f313,f157]) ).
thf(f435,plain,
( ( $false = $true )
| ~ spl32_20
| ~ spl32_29 ),
inference(forward_demodulation,[],[f434,f352]) ).
thf(f436,plain,
( $false
| ~ spl32_20
| ~ spl32_29 ),
inference(trivial_inequality_removal,[],[f435]) ).
thf(f437,plain,
( ~ spl32_20
| ~ spl32_29 ),
inference(avatar_contradiction_clause,[],[f436]) ).
thf(f438,plain,
( ( $false = $true )
| ~ spl32_21
| ~ spl32_22 ),
inference(forward_demodulation,[],[f317,f322]) ).
thf(f439,plain,
( $false
| ~ spl32_21
| ~ spl32_22 ),
inference(trivial_inequality_removal,[],[f438]) ).
thf(f440,plain,
( ~ spl32_21
| ~ spl32_22 ),
inference(avatar_contradiction_clause,[],[f439]) ).
thf(f442,plain,
( ( $false = $true )
| ( ( sF7 @ sK26 )
= $true )
| ~ spl32_28 ),
inference(constrained_superposition,[],[f348,f196]) ).
thf(f444,plain,
( ( ( sF7 @ sK26 )
= $true )
| ~ spl32_28 ),
inference(trivial_inequality_removal,[],[f442]) ).
thf(f450,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ ( kpair @ X0 @ X1 ) @ sF5 )
= $true )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) )
| ( ( ^ [Y0: $i] : ( (=) @ ( sK1 @ Y0 ) )
@ X0
@ X1 )
= $false ) )
| ~ spl32_7 ),
inference(constrained_superposition,[],[f258,f157]) ).
thf(f451,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ ( kpair @ X0 @ X1 ) @ sF5 )
= $true )
| ( $false
= ( ( sK1 @ X0 )
= X1 ) )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) ) )
| ~ spl32_7 ),
inference(beta-eta_normalization,[],[f450]) ).
thf(f452,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ ( kpair @ X0 @ X1 ) @ sF5 )
= $true )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) )
| ( ( sK1 @ X0 )
!= X1 ) )
| ~ spl32_7 ),
inference(equality_proxy_clausification,[],[f451]) ).
thf(f453,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ ( kpair @ X0 @ X1 ) @ sF5 )
= $true )
| ( ( sF8 @ X0 )
!= X1 )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) ) )
| ~ spl32_7 ),
inference(forward_demodulation,[],[f452,f65]) ).
thf(f474,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) )
| ~ spl32_14
| ~ spl32_31 ),
inference(constrained_superposition,[],[f286,f360]) ).
thf(f478,plain,
( ! [X0: $i] :
( ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) ) )
| ~ spl32_14
| ~ spl32_31 ),
inference(trivial_inequality_removal,[],[f474]) ).
thf(f479,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_14
| ~ spl32_31 ),
inference(beta-eta_normalization,[],[f478]) ).
thf(f481,definition,
( spl32_39
<=> ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_39])],[avatar_definition]) ).
thf(f482,plain,
( ! [X0: $i] :
( ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_39 ),
inference(avatar_component_clause,[],[f481]) ).
thf(f484,definition,
( spl32_40
<=> ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_40])],[avatar_definition]) ).
thf(f486,plain,
( ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| spl32_40 ),
inference(avatar_component_clause,[],[f484]) ).
thf(f488,plain,
( ~ spl32_40
| spl32_39
| ~ spl32_14
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f479,f359,f285,f481,f484]) ).
thf(f490,plain,
( ! [X0: $i] :
( ( ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_12
| spl32_40 ),
inference(constrained_superposition,[],[f486,f278]) ).
thf(f491,plain,
( ! [X0: $i] :
( ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 ) )
| ~ spl32_12
| spl32_40 ),
inference(trivial_inequality_removal,[],[f490]) ).
thf(f492,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= X0 ) )
| ~ spl32_12
| spl32_40 ),
inference(beta-eta_normalization,[],[f491]) ).
thf(f495,plain,
( spl32_39
| ~ spl32_12
| spl32_40 ),
inference(avatar_split_clause,[],[f492,f484,f277,f481]) ).
thf(f498,plain,
( ! [X0: $i] :
( ( ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $true )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false = $true ) )
| ~ spl32_13
| ~ spl32_31 ),
inference(constrained_superposition,[],[f360,f282]) ).
thf(f501,plain,
( ! [X0: $i] :
( ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $true )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) )
| ~ spl32_13
| ~ spl32_31 ),
inference(trivial_inequality_removal,[],[f498]) ).
thf(f502,plain,
( ! [X0: $i] :
( ( ( in
@ ( kpair @ sK26
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
@ sF5 )
= $true )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_13
| ~ spl32_31 ),
inference(beta-eta_normalization,[],[f501]) ).
thf(f507,plain,
( ! [X0: $i] :
( ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( $false = $true )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_10
| ~ spl32_31 ),
inference(constrained_superposition,[],[f360,f270]) ).
thf(f508,plain,
( ! [X0: $i] :
( ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true ) )
| ~ spl32_10
| ~ spl32_31 ),
inference(trivial_inequality_removal,[],[f507]) ).
thf(f509,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( setadjoin
@ ( sK18 @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ emptyset )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true ) )
| ~ spl32_10
| ~ spl32_31 ),
inference(beta-eta_normalization,[],[f508]) ).
thf(f535,definition,
( spl32_41
<=> ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_41])],[avatar_definition]) ).
thf(f536,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_41 ),
inference(avatar_component_clause,[],[f535]) ).
thf(f538,definition,
( spl32_42
<=> ( ( in @ ( kpair @ sK26 @ ( sF8 @ sK26 ) ) @ sF5 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl32_42])],[avatar_definition]) ).
thf(f540,plain,
( ( ( in @ ( kpair @ sK26 @ ( sF8 @ sK26 ) ) @ sF5 )
= $true )
| ~ spl32_42 ),
inference(avatar_component_clause,[],[f538]) ).
thf(f543,definition,
( spl32_43
<=> ( $true
= ( in @ ( sF8 @ sK26 ) @ sK2 ) ) ),
introduced(definition,[new_symbols(definition,[spl32_43])],[avatar_definition]) ).
thf(f545,plain,
( ( $true
= ( in @ ( sF8 @ sK26 ) @ sK2 ) )
| ~ spl32_43 ),
inference(avatar_component_clause,[],[f543]) ).
thf(f547,plain,
( ( $false = $true )
| ~ spl32_33
| ~ spl32_34 ),
inference(forward_demodulation,[],[f369,f374]) ).
thf(f548,plain,
( $false
| ~ spl32_33
| ~ spl32_34 ),
inference(trivial_inequality_removal,[],[f547]) ).
thf(f549,plain,
( ~ spl32_33
| ~ spl32_34 ),
inference(avatar_contradiction_clause,[],[f548]) ).
thf(f551,definition,
( spl32_44
<=> ! [X0: $i] :
( ( ( in
@ ( kpair @ sK26
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
@ sF5 )
= $true )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_44])],[avatar_definition]) ).
thf(f552,plain,
( ! [X0: $i] :
( ( ( in
@ ( kpair @ sK26
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
@ sF5 )
= $true )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_44 ),
inference(avatar_component_clause,[],[f551]) ).
thf(f555,definition,
( spl32_45
<=> ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true )
| ( $false
= ( in @ X0 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl32_45])],[avatar_definition]) ).
thf(f556,plain,
( ! [X0: $i] :
( ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_45 ),
inference(avatar_component_clause,[],[f555]) ).
thf(f559,plain,
( spl32_44
| ~ spl32_40
| ~ spl32_13
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f502,f359,f281,f484,f551]) ).
thf(f560,plain,
( spl32_45
| ~ spl32_40
| ~ spl32_10
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f509,f359,f269,f484,f555]) ).
thf(f563,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ sK26 @ sK0 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sF8 @ sK26 )
!= X0 )
| ( $false = $true ) )
| ~ spl32_7
| ~ spl32_41 ),
inference(constrained_superposition,[],[f453,f536]) ).
thf(f565,plain,
( ! [X0: $i] :
( ( $false
= ( in @ sK26 @ sK0 ) )
| ( ( sF8 @ sK26 )
!= X0 )
| ( $false = $true )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_7
| ~ spl32_41 ),
inference(duplicate_literal_removal,[],[f563]) ).
thf(f566,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ sK26 @ sK0 ) )
| ( ( sF8 @ sK26 )
!= X0 ) )
| ~ spl32_7
| ~ spl32_41 ),
inference(trivial_inequality_removal,[],[f565]) ).
thf(f569,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sF8 @ sK26 )
!= X0 ) )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(forward_demodulation,[],[f566,f348]) ).
thf(f570,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sF8 @ sK26 )
!= X0 ) )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(trivial_inequality_removal,[],[f569]) ).
thf(f573,plain,
( ! [X0: $i] :
( ( ( sF8 @ sK26 )
!= ( sF8 @ X0 ) )
| ( $false
= ( sF9 @ X0 ) )
| ( $false = $true ) )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(constrained_superposition,[],[f570,f105]) ).
thf(f576,plain,
( ! [X0: $i] :
( ( ( sF8 @ sK26 )
!= ( sF8 @ X0 ) )
| ( $false
= ( sF9 @ X0 ) ) )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(trivial_inequality_removal,[],[f573]) ).
thf(f579,plain,
( ( $false
= ( sF9 @ sK26 ) )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(equality_resolution,[],[f576]) ).
thf(f582,plain,
( ( $false = $true )
| ( ( sF7 @ sK26 )
!= $true )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(constrained_superposition,[],[f68,f579]) ).
thf(f585,plain,
( ( ( sF7 @ sK26 )
!= $true )
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(trivial_inequality_removal,[],[f582]) ).
thf(f588,plain,
( $false
| ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(forward_subsumption_resolution,[],[f585,f444]) ).
thf(f589,plain,
( ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(avatar_contradiction_clause,[],[f588]) ).
thf(f594,plain,
( ! [X0: $i,X1: $i] :
( ( ( ^ [Y0: $i] : ( (=) @ ( sK1 @ Y0 ) )
@ X0
@ X1 )
= $true )
| ( $false
= ( in @ ( kpair @ X0 @ X1 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) ) )
| ~ spl32_32 ),
inference(constrained_superposition,[],[f365,f157]) ).
thf(f601,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( in @ X1 @ sK2 ) )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ ( kpair @ X0 @ X1 ) @ sF5 ) )
| ( ( ( sK1 @ X0 )
= X1 )
= $true ) )
| ~ spl32_32 ),
inference(beta-eta_normalization,[],[f594]) ).
thf(f602,plain,
( ! [X0: $i,X1: $i] :
( ( ( sK1 @ X0 )
= X1 )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ X0 @ X1 ) @ sF5 ) ) )
| ~ spl32_32 ),
inference(equality_proxy_clausification,[],[f601]) ).
thf(f605,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( in @ ( kpair @ X0 @ X1 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK0 ) )
| ( $false
= ( in @ X1 @ sK2 ) )
| ( ( sF8 @ X0 )
= X1 ) )
| ~ spl32_32 ),
inference(forward_demodulation,[],[f602,f65]) ).
thf(f612,plain,
( ! [X0: $i] :
( ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_9
| spl32_40 ),
inference(constrained_superposition,[],[f486,f266]) ).
thf(f613,plain,
( ! [X0: $i] :
( ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
!= ( dsetconstr @ sK2
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $true )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_11
| spl32_40 ),
inference(constrained_superposition,[],[f486,f274]) ).
thf(f615,plain,
( ! [X0: $i] :
( ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
= $true ) )
| ~ spl32_11
| spl32_40 ),
inference(trivial_inequality_removal,[],[f613]) ).
thf(f616,plain,
( ! [X0: $i] :
( ( ( in
@ ( kpair @ sK26
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
@ sF5 )
= $true )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_11
| spl32_40 ),
inference(beta-eta_normalization,[],[f615]) ).
thf(f619,plain,
( ! [X0: $i] :
( ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true )
| ( $false
= ( ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 )
@ X0 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_9
| spl32_40 ),
inference(trivial_inequality_removal,[],[f612]) ).
thf(f620,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 )
= $true ) )
| ~ spl32_9
| spl32_40 ),
inference(beta-eta_normalization,[],[f619]) ).
thf(f621,plain,
( spl32_44
| ~ spl32_11
| spl32_40 ),
inference(avatar_split_clause,[],[f616,f484,f273,f551]) ).
thf(f622,plain,
( spl32_45
| ~ spl32_9
| spl32_40 ),
inference(avatar_split_clause,[],[f620,f484,f265,f555]) ).
thf(f623,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false = $true )
| ( $false
= ( in @ sK26 @ sK0 ) )
| ( $false
= ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 ) ) )
| ~ spl32_32
| ~ spl32_44 ),
inference(constrained_superposition,[],[f552,f605]) ).
thf(f625,plain,
( ! [X0: $i] :
( ( $false
= ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ sK26 @ sK0 ) ) )
| ~ spl32_32
| ~ spl32_44 ),
inference(trivial_inequality_removal,[],[f623]) ).
thf(f627,plain,
( ! [X0: $i] :
( ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false = $true )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44 ),
inference(forward_demodulation,[],[f625,f348]) ).
thf(f628,plain,
( ! [X0: $i] :
( ( $false
= ( in
@ ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) )
@ sK2 ) )
| ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44 ),
inference(trivial_inequality_removal,[],[f627]) ).
thf(f631,plain,
( ! [X0: $i] :
( ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false = $true )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(constrained_superposition,[],[f628,f556]) ).
thf(f634,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false = $true )
| ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(duplicate_literal_removal,[],[f631]) ).
thf(f635,plain,
( ! [X0: $i] :
( ( ( sF8 @ sK26 )
= ( sK17 @ sK2 @ X0
@ ^ [Y0: $i] : ( in @ ( kpair @ sK26 @ Y0 ) @ sF5 ) ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(trivial_inequality_removal,[],[f634]) ).
thf(f639,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( ( in @ ( kpair @ sK26 @ ( sF8 @ sK26 ) ) @ sF5 )
= $true )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(constrained_superposition,[],[f552,f635]) ).
thf(f640,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $true
= ( in @ ( sF8 @ sK26 ) @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(constrained_superposition,[],[f556,f635]) ).
thf(f641,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( sF8 @ sK26 )
!= X0 ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_44
| ~ spl32_45 ),
inference(constrained_superposition,[],[f482,f635]) ).
thf(f642,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( ( sF8 @ sK26 )
!= X0 )
| ( $false
= ( in @ X0 @ sK2 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_44
| ~ spl32_45 ),
inference(duplicate_literal_removal,[],[f641]) ).
thf(f643,plain,
( ! [X0: $i] :
( ( $true
= ( in @ ( sF8 @ sK26 ) @ sK2 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(duplicate_literal_removal,[],[f640]) ).
thf(f644,plain,
( ! [X0: $i] :
( ( $false
= ( in @ ( kpair @ sK26 @ X0 ) @ sF5 ) )
| ( $false
= ( in @ X0 @ sK2 ) )
| ( ( in @ ( kpair @ sK26 @ ( sF8 @ sK26 ) ) @ sF5 )
= $true ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(duplicate_literal_removal,[],[f639]) ).
thf(f649,plain,
( ( $false = $true )
| ( $false
= ( in @ ( sF8 @ sK26 ) @ sK2 ) )
| ( ( sF8 @ sK26 )
!= ( sF8 @ sK26 ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_44
| ~ spl32_45 ),
inference(constrained_superposition,[],[f540,f642]) ).
thf(f659,plain,
( ( $false
= ( in @ ( sF8 @ sK26 ) @ sK2 ) )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_44
| ~ spl32_45 ),
inference(trivial_inequality_removal,[],[f649]) ).
thf(f670,plain,
( ( $false = $true )
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_43
| ~ spl32_44
| ~ spl32_45 ),
inference(forward_demodulation,[],[f659,f545]) ).
thf(f671,plain,
( $false
| ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_43
| ~ spl32_44
| ~ spl32_45 ),
inference(trivial_inequality_removal,[],[f670]) ).
thf(f672,plain,
( ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_43
| ~ spl32_44
| ~ spl32_45 ),
inference(avatar_contradiction_clause,[],[f671]) ).
thf(f673,plain,
( spl32_41
| spl32_42
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(avatar_split_clause,[],[f644,f555,f551,f364,f346,f538,f535]) ).
thf(f674,plain,
( spl32_41
| spl32_43
| ~ spl32_28
| ~ spl32_32
| ~ spl32_44
| ~ spl32_45 ),
inference(avatar_split_clause,[],[f643,f555,f551,f364,f346,f543,f535]) ).
cnf(s5,plain,
( spl32_6
| spl32_7 ),
inference(sat_conversion,[],[f259]) ).
cnf(s6,plain,
( spl32_8
| spl32_9 ),
inference(sat_conversion,[],[f267]) ).
cnf(s7,plain,
( spl32_8
| spl32_10 ),
inference(sat_conversion,[],[f271]) ).
cnf(s8,plain,
( spl32_8
| spl32_11 ),
inference(sat_conversion,[],[f275]) ).
cnf(s9,plain,
( spl32_8
| spl32_12 ),
inference(sat_conversion,[],[f279]) ).
cnf(s10,plain,
( spl32_8
| spl32_13 ),
inference(sat_conversion,[],[f283]) ).
cnf(s11,plain,
( spl32_8
| spl32_14 ),
inference(sat_conversion,[],[f287]) ).
cnf(s16,plain,
spl32_16,
inference(sat_conversion,[],[f310]) ).
cnf(s17,plain,
( spl32_20
| spl32_21 ),
inference(sat_conversion,[],[f318]) ).
cnf(s22,plain,
( spl32_28
| spl32_29
| spl32_30 ),
inference(sat_conversion,[],[f357]) ).
cnf(s23,plain,
( spl32_29
| spl32_30
| spl32_31 ),
inference(sat_conversion,[],[f361]) ).
cnf(s24,plain,
spl32_1,
inference(sat_conversion,[],[f362]) ).
cnf(s25,plain,
( spl32_32
| spl32_33 ),
inference(sat_conversion,[],[f370]) ).
cnf(s30,plain,
spl32_34,
inference(sat_conversion,[],[f395]) ).
cnf(s31,plain,
~ spl32_30,
inference(sat_conversion,[],[f396]) ).
cnf(s32,plain,
spl32_22,
inference(sat_conversion,[],[f397]) ).
cnf(s33,plain,
( ~ spl32_1
| ~ spl32_6 ),
inference(sat_conversion,[],[f400]) ).
cnf(s35,plain,
( ~ spl32_8
| ~ spl32_16 ),
inference(sat_conversion,[],[f415]) ).
cnf(s36,plain,
( ~ spl32_20
| ~ spl32_29 ),
inference(sat_conversion,[],[f437]) ).
cnf(s37,plain,
( ~ spl32_21
| ~ spl32_22 ),
inference(sat_conversion,[],[f440]) ).
cnf(s40,plain,
( ~ spl32_14
| ~ spl32_31
| spl32_39
| ~ spl32_40 ),
inference(sat_conversion,[],[f488]) ).
cnf(s41,plain,
( ~ spl32_12
| spl32_39
| spl32_40 ),
inference(sat_conversion,[],[f495]) ).
cnf(s44,plain,
( ~ spl32_33
| ~ spl32_34 ),
inference(sat_conversion,[],[f549]) ).
cnf(s47,plain,
( ~ spl32_13
| ~ spl32_31
| ~ spl32_40
| spl32_44 ),
inference(sat_conversion,[],[f559]) ).
cnf(s48,plain,
( ~ spl32_10
| ~ spl32_31
| ~ spl32_40
| spl32_45 ),
inference(sat_conversion,[],[f560]) ).
cnf(s50,plain,
( ~ spl32_7
| ~ spl32_28
| ~ spl32_41 ),
inference(sat_conversion,[],[f589]) ).
cnf(s51,plain,
( ~ spl32_11
| spl32_40
| spl32_44 ),
inference(sat_conversion,[],[f621]) ).
cnf(s52,plain,
( ~ spl32_9
| spl32_40
| spl32_45 ),
inference(sat_conversion,[],[f622]) ).
cnf(s54,plain,
( ~ spl32_28
| ~ spl32_32
| ~ spl32_39
| ~ spl32_42
| ~ spl32_43
| ~ spl32_44
| ~ spl32_45 ),
inference(sat_conversion,[],[f672]) ).
cnf(s55,plain,
( ~ spl32_28
| ~ spl32_32
| spl32_41
| spl32_42
| ~ spl32_44
| ~ spl32_45 ),
inference(sat_conversion,[],[f673]) ).
cnf(s56,plain,
( ~ spl32_28
| ~ spl32_32
| spl32_41
| spl32_43
| ~ spl32_44
| ~ spl32_45 ),
inference(sat_conversion,[],[f674]) ).
cnf(s57,plain,
~ spl32_21,
inference(rat,[],[s37,s32]) ).
cnf(s59,plain,
~ spl32_33,
inference(rat,[],[s44,s30]) ).
cnf(s60,plain,
spl32_32,
inference(rat,[],[s25,s59]) ).
cnf(s61,plain,
~ spl32_6,
inference(rat,[],[s33,s24]) ).
cnf(s62,plain,
( spl32_29
| spl32_31 ),
inference(rat,[],[s23,s31]) ).
cnf(s63,plain,
( spl32_28
| spl32_29 ),
inference(rat,[],[s22,s31]) ).
cnf(s64,plain,
spl32_20,
inference(rat,[],[s17,s57]) ).
cnf(s66,plain,
~ spl32_29,
inference(rat,[],[s36,s64]) ).
cnf(s67,plain,
spl32_31,
inference(rat,[],[s62,s66]) ).
cnf(s68,plain,
spl32_28,
inference(rat,[],[s63,s66]) ).
cnf(s69,plain,
~ spl32_8,
inference(rat,[],[s35,s16]) ).
cnf(s70,plain,
spl32_14,
inference(rat,[],[s11,s69]) ).
cnf(s71,plain,
spl32_13,
inference(rat,[],[s10,s69]) ).
cnf(s72,plain,
spl32_12,
inference(rat,[],[s9,s69]) ).
cnf(s73,plain,
spl32_11,
inference(rat,[],[s8,s69]) ).
cnf(s74,plain,
spl32_10,
inference(rat,[],[s7,s69]) ).
cnf(s75,plain,
spl32_9,
inference(rat,[],[s6,s69]) ).
cnf(s76,plain,
spl32_7,
inference(rat,[],[s5,s61]) ).
cnf(s77,plain,
~ spl32_41,
inference(rat,[],[s50,s68,s76]) ).
cnf(s78,plain,
spl32_39,
inference(rat,[],[s40,s41,s67,s70,s72]) ).
cnf(s79,plain,
( ~ spl32_44
| ~ spl32_45 ),
inference(rat,[],[s54,s55,s56,s77,s78,s68,s60]) ).
cnf(s80,plain,
~ spl32_40,
inference(rat,[],[s79,s47,s48,s67,s71,s74]) ).
cnf(s81,plain,
spl32_45,
inference(rat,[],[s52,s75,s80]) ).
cnf(s82,plain,
spl32_44,
inference(rat,[],[s51,s73,s80]) ).
cnf(s85,plain,
$false,
inference(rat,[],[s79,s81,s82]) ).
thf(f675,plain,
$false,
inference(avatar_sat_refutation,[],[s85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU678^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 14:10:27 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.24/0.36 % (656827)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.24/0.36 % (656837)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2078009894:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.24/0.36 % (656832)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1119427154:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.24/0.36 % (656834)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4100654983:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.24/0.36 % (656833)lrs+10_16_si=on:nwc=1.5:random_seed=3112551739:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.24/0.36 % (656835)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=4215457774:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.24/0.36 % (656834)Instruction limit reached!
% 0.24/0.36 % (656834)------------------------------
% 0.24/0.36 % (656834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656834)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656834)Termination reason: Instruction limit
% 0.24/0.36 % (656834)Termination phase: Property scanning
% 0.24/0.36 % (656834)Time elapsed: 0.002 s
% 0.24/0.36 % (656834)Peak memory usage: 10 MB
% 0.24/0.36 % (656834)Instructions burned: 3 (million)
% 0.24/0.36 % (656833)Instruction limit reached!
% 0.24/0.36 % (656833)------------------------------
% 0.24/0.36 % (656833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656833)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656833)Termination reason: Instruction limit
% 0.24/0.36 % (656833)Termination phase: Saturation
% 0.24/0.36 % (656833)Time elapsed: 0.010 s
% 0.24/0.36 % (656833)Peak memory usage: 12 MB
% 0.24/0.36 % (656833)Instructions burned: 19 (million)
% 0.24/0.36 % (656838)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.24/0.36 % (656838)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.24/0.36 % (656836)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1015128219:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.24/0.36 % (656838)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3028401289:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.24/0.36 % (656835)Refutation not found, incomplete strategy
% 0.24/0.36 % (656835)------------------------------
% 0.24/0.36 % (656835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656835)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656835)Termination reason: Refutation not found, incomplete strategy
% 0.24/0.36 % (656835)Time elapsed: 0.018 s
% 0.24/0.36 % (656835)Peak memory usage: 12 MB
% 0.24/0.36 % (656835)Instructions burned: 29 (million)
% 0.24/0.36 % (656835)------------------------------
% 0.24/0.36 % (656835)------------------------------
% 0.24/0.36 % (656844)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3783028295:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.24/0.36 % (656844)Instruction limit reached!
% 0.24/0.36 % (656844)------------------------------
% 0.24/0.36 % (656844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656844)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656844)Termination reason: Instruction limit
% 0.24/0.36 % (656844)Termination phase: Saturation
% 0.24/0.36 % (656844)Time elapsed: 0.003 s
% 0.24/0.36 % (656844)Peak memory usage: 11 MB
% 0.24/0.36 % (656844)Instructions burned: 6 (million)
% 0.24/0.36 % (656845)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=345624226:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.24/0.36 % (656837)Instruction limit reached!
% 0.24/0.36 % (656837)------------------------------
% 0.24/0.36 % (656837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656837)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656837)Termination reason: Instruction limit
% 0.24/0.36 % (656837)Termination phase: Saturation
% 0.24/0.36 % (656837)Time elapsed: 0.037 s
% 0.24/0.36 % (656837)Peak memory usage: 13 MB
% 0.24/0.36 % (656837)Instructions burned: 75 (million)
% 0.24/0.36 % (656848)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.24/0.36 % (656836)Instruction limit reached!
% 0.24/0.36 % (656836)------------------------------
% 0.24/0.36 % (656836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656836)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656836)Termination reason: Instruction limit
% 0.24/0.36 % (656836)Termination phase: Saturation
% 0.24/0.36 % (656836)Time elapsed: 0.024 s
% 0.24/0.36 % (656836)Peak memory usage: 12 MB
% 0.24/0.36 % (656836)Instructions burned: 24 (million)
% 0.24/0.36 % (656845)Instruction limit reached!
% 0.24/0.36 % (656845)------------------------------
% 0.24/0.36 % (656845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656845)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656845)Termination reason: Instruction limit
% 0.24/0.36 % (656845)Termination phase: Saturation
% 0.24/0.36 % (656845)Time elapsed: 0.007 s
% 0.24/0.36 % (656845)Peak memory usage: 11 MB
% 0.24/0.36 % (656845)Instructions burned: 6 (million)
% 0.24/0.36 % (656838) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-656827-656838"...
% 0.24/0.36 % (656852)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.24/0.36 % (656852)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.24/0.36 % (656848)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=436568614:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.24/0.36 % (656832)Instruction limit reached!
% 0.24/0.36 % (656832)------------------------------
% 0.24/0.36 % (656832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656832)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656832)Termination reason: Instruction limit
% 0.24/0.36 % (656832)Termination phase: Saturation
% 0.24/0.36 % (656832)Time elapsed: 0.054 s
% 0.24/0.36 % (656832)Peak memory usage: 12 MB
% 0.24/0.36 % (656832)Instructions burned: 88 (million)
% 0.24/0.36 % (656852)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3242234389:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.24/0.36 % (656838)...printing done.
% 0.24/0.36 % (656838)Refutation found. Thanks to Tanya!
% 0.24/0.36 % SZS status Theorem for theBenchmark
% 0.24/0.36 % SZS output start Proof for theBenchmark
% See solution above
% 0.24/0.36 % (656838)------------------------------
% 0.24/0.36 % (656838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.36 % (656838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.36 % (656838)CaDiCaL version: 2.1.3
% 0.24/0.36 % (656838)Termination reason: Refutation
% 0.24/0.36 % (656838)Time elapsed: 0.036 s
% 0.24/0.36 % (656838)Peak memory usage: 13 MB
% 0.24/0.36 % (656838)Instructions burned: 68 (million)
% 0.24/0.36 % (656827)Success in time 0.099 s
% 0.24/0.36 % Vampire exiting
%------------------------------------------------------------------------------