%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU463^1 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:29:43 AM UTC 2026
% Result : Theorem 0.97s 0.52s
% Output : Refutation 0.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 44
% Syntax : Number of formulae : 358 ( 69 unt; 0 typ; 40 def)
% Number of atoms : 2699 ( 576 equ; 0 cnn)
% Maximal formula atoms : 8 ( 7 avg)
% Number of connectives : 3697 ( 351 ~; 709 |; 107 &;2212 @)
% ( 35 <=>; 117 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 354 ( 354 >; 0 *; 0 +; 0 <<)
% Number of symbols : 105 ( 101 usr; 46 con; 0-4 aty)
% ( 166 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 447 ( 0 sgn 168 !; 15 ?; 447 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
subrel: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(func_def_2,type,
inv: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_3,type,
idem: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(func_def_4,type,
infl: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(func_def_5,type,
mono: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(func_def_6,type,
refl: ( $i > $i > $o ) > $o ).
thf(func_def_7,type,
irrefl: ( $i > $i > $o ) > $o ).
thf(func_def_8,type,
rc: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_9,type,
symm: ( $i > $i > $o ) > $o ).
thf(func_def_10,type,
antisymm: ( $i > $i > $o ) > $o ).
thf(func_def_11,type,
asymm: ( $i > $i > $o ) > $o ).
thf(func_def_12,type,
sc: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_13,type,
trans: ( $i > $i > $o ) > $o ).
thf(func_def_14,type,
tc: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_15,type,
trc: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_16,type,
trsc: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_17,type,
po: ( $i > $i > $o ) > $o ).
thf(func_def_18,type,
so: ( $i > $i > $o ) > $o ).
thf(func_def_19,type,
total: ( $i > $i > $o ) > $o ).
thf(func_def_20,type,
term: ( $i > $i > $o ) > $o ).
thf(func_def_21,type,
ind: ( $i > $i > $o ) > $o ).
thf(func_def_22,type,
innf: ( $i > $i > $o ) > $i > $o ).
thf(func_def_23,type,
nfof: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_24,type,
norm: ( $i > $i > $o ) > $o ).
thf(func_def_25,type,
join: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_26,type,
lconfl: ( $i > $i > $o ) > $o ).
thf(func_def_27,type,
sconfl: ( $i > $i > $o ) > $o ).
thf(func_def_28,type,
confl: ( $i > $i > $o ) > $o ).
thf(func_def_29,type,
cr: ( $i > $i > $o ) > $o ).
thf(func_def_30,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_31,type,
vIMP: $o > $o > $o ).
thf(func_def_32,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_33,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_34,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_35,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_36,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_37,type,
vOR: $o > $o > $o ).
thf(func_def_38,type,
vAND: $o > $o > $o ).
thf(func_def_39,type,
vNOT: $o > $o ).
thf(func_def_40,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_41,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_47,type,
sK3: $i > $i > $o ).
thf(func_def_48,type,
sK4: $i > $i > $o ).
thf(func_def_49,type,
sF5: $o ).
thf(func_def_50,type,
sF6: $o ).
thf(func_def_51,type,
sF7: $o ).
thf(func_def_52,type,
sF8: $o ).
thf(func_def_53,type,
sF9: $o ).
thf(func_def_54,type,
sK10: ( $i > $i > $o ) > $i ).
thf(func_def_55,type,
sK11: ( $i > $i > $o ) > $i ).
thf(func_def_56,type,
sK12: ( $i > $i > $o ) > $i ).
thf(func_def_57,type,
sK13: ( $i > $i > $o ) > $i ).
thf(func_def_58,type,
sK14: ( $i > $i > $o ) > $i ).
thf(func_def_59,type,
sK15: ( $i > $i > $o ) > $i ).
thf(func_def_60,type,
sK16: $i > $i > $o ).
thf(func_def_61,type,
sK17: ( $i > $i > $o ) > $i ).
thf(func_def_62,type,
sK18: ( $i > $i > $o ) > $i ).
thf(func_def_63,type,
sK19: ( $i > $i > $o ) > $i ).
thf(func_def_64,type,
sK20: ( $i > $i > $o ) > $i ).
thf(func_def_65,type,
sK21: ( $i > $i > $o ) > $i ).
thf(func_def_66,type,
sK22: ( $i > $i > $o ) > $i ).
thf(func_def_67,type,
sK23: $i > $i > $o ).
thf(f1,axiom,
( subrel
= ( ^ [X0: $i > $i > $o,X1: $i > $i > $o] :
! [X2: $i,X3: $i] :
( ( X0 @ X2 @ X3 )
=> ( X1 @ X2 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET009^0.ax',subrel) ).
thf(f13,axiom,
( ( ^ [X0: $i > $i > $o] :
! [X1: $i,X3: $i,X2: $i] :
( ( ( X0 @ X1 @ X2 )
& ( X0 @ X2 @ X3 ) )
=> ( X0 @ X1 @ X3 ) ) )
= trans ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET009^0.ax',transitive) ).
thf(f14,axiom,
( ( ^ [X0: $i > $i > $o,X1: $i,X2: $i] :
! [X3: $i > $i > $o] :
( ( ( subrel @ X0 @ X3 )
& ( trans @ X3 ) )
=> ( X3 @ X1 @ X2 ) ) )
= tc ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET009^0.ax',transitive_closure) ).
thf(f30,conjecture,
! [X0: $i > $i > $o,X4: $i > $i > $o,X2: $i,X3: $i,X1: $i] :
( ( ( tc @ X0 @ X2 @ X3 )
& ( subrel @ X0 @ X4 )
& ( tc @ X0 @ X1 @ X2 )
& ( trans @ X4 ) )
=> ( X4 @ X1 @ X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitive_closure_is_transitive3) ).
thf(f31,negated_conjecture,
~ ! [X0: $i > $i > $o,X4: $i > $i > $o,X2: $i,X3: $i,X1: $i] :
( ( ( tc @ X0 @ X2 @ X3 )
& ( subrel @ X0 @ X4 )
& ( tc @ X0 @ X1 @ X2 )
& ( trans @ X4 ) )
=> ( X4 @ X1 @ X3 ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
thf(f39,plain,
( subrel
= ( ^ [X0: $i > $i > $o,X1: $i > $i > $o] :
! [X2: $i,X3: $i] :
( ( X0 @ X2 @ X3 )
=> ( X1 @ X2 @ X3 ) ) ) ),
inference(rectify,[],[f1]) ).
thf(f40,plain,
( subrel
= ( ^ [Y0: $i > $i > $o,Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) ) ) ) ),
inference(fool_elimination,[],[f39]) ).
thf(f49,plain,
( ( ^ [X0: $i > $i > $o,X1: $i,X2: $i] :
! [X3: $i > $i > $o] :
( ( ( subrel @ X0 @ X3 )
& ( trans @ X3 ) )
=> ( X3 @ X1 @ X2 ) ) )
= tc ),
inference(rectify,[],[f14]) ).
thf(f50,plain,
( tc
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( trans @ Y3 )
& ( subrel @ Y0 @ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) ) ) ),
inference(fool_elimination,[],[f49]) ).
thf(f55,plain,
~ ! [X0: $i > $i > $o,X1: $i > $i > $o,X2: $i,X3: $i,X4: $i] :
( ( ( tc @ X0 @ X2 @ X3 )
& ( subrel @ X0 @ X1 )
& ( tc @ X0 @ X4 @ X2 )
& ( trans @ X1 ) )
=> ( X1 @ X4 @ X3 ) ),
inference(rectify,[],[f31]) ).
thf(f56,plain,
~ ! [X3: $i,X1: $i > $i > $o,X0: $i > $i > $o,X2: $i,X4: $i] :
( ( ( $true
= ( subrel @ X0 @ X1 ) )
& ( ( tc @ X0 @ X2 @ X3 )
= $true )
& ( $true
= ( trans @ X1 ) )
& ( $true
= ( tc @ X0 @ X4 @ X2 ) ) )
=> ( ( X1 @ X4 @ X3 )
= $true ) ),
inference(fool_elimination,[],[f55]) ).
thf(f63,plain,
( ( ^ [X0: $i > $i > $o] :
! [X1: $i,X2: $i,X3: $i] :
( ( ( X0 @ X1 @ X3 )
& ( X0 @ X3 @ X2 ) )
=> ( X0 @ X1 @ X2 ) ) )
= trans ),
inference(rectify,[],[f13]) ).
thf(f64,plain,
( trans
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f63]) ).
thf(f88,plain,
? [X3: $i,X1: $i > $i > $o,X0: $i > $i > $o,X2: $i,X4: $i] :
( ( ( X1 @ X4 @ X3 )
!= $true )
& ( $true
= ( subrel @ X0 @ X1 ) )
& ( ( tc @ X0 @ X2 @ X3 )
= $true )
& ( $true
= ( trans @ X1 ) )
& ( $true
= ( tc @ X0 @ X4 @ X2 ) ) ),
inference(ennf_transformation,[],[f56]) ).
thf(f89,plain,
? [X2: $i,X3: $i,X4: $i,X1: $i > $i > $o,X0: $i > $i > $o] :
( ( ( X1 @ X4 @ X3 )
!= $true )
& ( $true
= ( subrel @ X0 @ X1 ) )
& ( $true
= ( tc @ X0 @ X4 @ X2 ) )
& ( ( tc @ X0 @ X2 @ X3 )
= $true )
& ( $true
= ( trans @ X1 ) ) ),
inference(flattening,[],[f88]) ).
thf(f90,plain,
? [X0: $i,X1: $i,X2: $i,X3: $i > $i > $o,X4: $i > $i > $o] :
( ( ( X3 @ X2 @ X1 )
!= $true )
& ( $true
= ( subrel @ X4 @ X3 ) )
& ( $true
= ( tc @ X4 @ X2 @ X0 ) )
& ( ( tc @ X4 @ X0 @ X1 )
= $true )
& ( ( trans @ X3 )
= $true ) ),
inference(rectify,[],[f89]) ).
thf(f91,plain,
( ( ( sK3 @ sK2 @ sK1 )
!= $true )
& ( $true
= ( subrel @ sK4 @ sK3 ) )
& ( ( tc @ sK4 @ sK2 @ sK0 )
= $true )
& ( $true
= ( tc @ sK4 @ sK0 @ sK1 ) )
& ( ( trans @ sK3 )
= $true ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f90]) ).
thf(f97,plain,
( tc
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( trans @ Y3 )
& ( subrel @ Y0 @ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f50]) ).
thf(f106,plain,
( trans
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f64]) ).
thf(f109,plain,
( ( trans @ sK3 )
= $true ),
inference(cnf_transformation,[],[f91]) ).
thf(f110,plain,
( $true
= ( tc @ sK4 @ sK0 @ sK1 ) ),
inference(cnf_transformation,[],[f91]) ).
thf(f111,plain,
( ( tc @ sK4 @ sK2 @ sK0 )
= $true ),
inference(cnf_transformation,[],[f91]) ).
thf(f112,plain,
( $true
= ( subrel @ sK4 @ sK3 ) ),
inference(cnf_transformation,[],[f91]) ).
thf(f113,plain,
( ( sK3 @ sK2 @ sK1 )
!= $true ),
inference(cnf_transformation,[],[f91]) ).
thf(f119,plain,
( subrel
= ( ^ [Y0: $i > $i > $o,Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) ) ) ) ),
inference(cnf_transformation,[],[f40]) ).
thf(f130,plain,
( tc
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) ) ) ),
inference(definition_unfolding,[],[f97,f106,f119]) ).
thf(f143,plain,
( $true
= ( ^ [Y0: $i > $i > $o,Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) ) )
@ sK4
@ sK3 ) ),
inference(definition_unfolding,[],[f112,f119]) ).
thf(f144,plain,
( ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK2
@ sK0 )
= $true ),
inference(definition_unfolding,[],[f111,f130]) ).
thf(f145,plain,
( $true
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK0
@ sK1 ) ),
inference(definition_unfolding,[],[f110,f130]) ).
thf(f146,plain,
( $true
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
@ sK3 ) ),
inference(definition_unfolding,[],[f109,f106]) ).
thf(f147,definition,
( sF5
= ( sK3 @ sK2 @ sK1 ) ),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
thf(f148,plain,
( ( sK3 @ sK2 @ sK1 )
= sF5 ),
inference(reorient_equations,[],[f147]) ).
thf(f149,plain,
$true != sF5,
inference(definition_folding,[],[f113,f148]) ).
thf(f150,definition,
( sF6
= ( ^ [Y0: $i > $i > $o,Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) ) )
@ sK4
@ sK3 ) ),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
thf(f151,plain,
$true = sF6,
inference(definition_folding,[],[f143,f150]) ).
thf(f152,definition,
( sF7
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK2
@ sK0 ) ),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
thf(f153,plain,
sF7 = $true,
inference(definition_folding,[],[f144,f152]) ).
thf(f154,definition,
( sF8
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK0
@ sK1 ) ),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
thf(f155,plain,
sF8 = $true,
inference(definition_folding,[],[f145,f154]) ).
thf(f156,definition,
( sF9
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
@ sK3 ) ),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
thf(f157,plain,
sF9 = $true,
inference(definition_folding,[],[f146,f156]) ).
thf(f159,plain,
( ( $false = sF8 )
| ( $true
= ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK0
@ sK1 ) ) ),
inference(iff_proxy_clausification,[],[f154]) ).
thf(f160,plain,
( ( ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
& ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( sK4 @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) )
=> ( Y0 @ sK0 @ sK1 ) ) )
= $true )
| ( $false = sF8 ) ),
inference(beta-eta_normalization,[],[f159]) ).
thf(f161,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( $true
= ( ^ [Y0: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
& ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( sK4 @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) )
=> ( Y0 @ sK0 @ sK1 ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f160]) ).
thf(f162,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) )
& ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) )
=> ( X1 @ sK0 @ sK1 ) ) )
| ( $false = sF8 ) ),
inference(beta-eta_normalization,[],[f161]) ).
thf(f163,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) )
& ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f162]) ).
thf(f164,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) )
| ( $false = sF8 )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f163]) ).
thf(f165,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK10 @ X1 ) ) )
| ( $false = sF8 ) ),
inference(sigma_proxy_clausification,[],[f164]) ).
thf(f166,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK10 @ X1 ) ) )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) )
@ ( sK11 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f165]) ).
thf(f167,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK10 @ X1 ) )
=> ( X1 @ Y0 @ ( sK10 @ X1 ) ) ) ) )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) ) )
= $false )
| ( $false = sF8 )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ),
inference(beta-eta_normalization,[],[f166]) ).
thf(f168,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK10 @ X1 ) )
=> ( X1 @ Y0 @ ( sK10 @ X1 ) ) )
@ ( sK12 @ X1 ) ) )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) ) )
= $false )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 ) ),
inference(sigma_proxy_clausification,[],[f167]) ).
thf(f169,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK10 @ X1 ) )
=> ( X1 @ Y0 @ ( sK10 @ X1 ) ) )
@ ( sK12 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ),
inference(sigma_proxy_clausification,[],[f168]) ).
thf(f170,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) )
=> ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ Y0 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK13 @ X1 ) ) ) ) )
| ( $false = sF8 ) ),
inference(beta-eta_normalization,[],[f169]) ).
thf(f171,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false = sF8 )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ Y0 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK13 @ X1 ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f170]) ).
thf(f172,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ Y0 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK13 @ X1 ) ) ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 ) ),
inference(imp_proxy_clausification,[],[f170]) ).
thf(f173,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( ^ [Y0: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ Y0 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK13 @ X1 ) ) )
@ ( sK14 @ X1 ) ) )
| ( $false = sF8 )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f172]) ).
thf(f174,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false
= ( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ ( sK14 @ X1 ) @ ( sK11 @ X1 ) ) )
=> ( X1 @ ( sK14 @ X1 ) @ ( sK13 @ X1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f173]) ).
thf(f175,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK14 @ X1 ) @ ( sK13 @ X1 ) ) )
| ( $false = sF8 )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ),
inference(imp_proxy_clausification,[],[f174]) ).
thf(f176,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ ( sK14 @ X1 ) @ ( sK11 @ X1 ) ) ) )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 ) ),
inference(imp_proxy_clausification,[],[f174]) ).
thf(f177,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $true
= ( X1 @ ( sK14 @ X1 ) @ ( sK11 @ X1 ) ) )
| ( $false = sF8 ) ),
inference(and_proxy_clausification,[],[f176]) ).
thf(f178,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false = sF8 )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true ) ),
inference(and_proxy_clausification,[],[f176]) ).
thf(f179,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( ( ^ [Y0: $i] :
( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ Y0 @ ( sK11 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK13 @ X1 ) ) )
@ ( sK15 @ X1 ) )
= $false )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ),
inference(sigma_proxy_clausification,[],[f171]) ).
thf(f180,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( $false
= ( ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ ( sK15 @ X1 ) @ ( sK11 @ X1 ) ) )
=> ( X1 @ ( sK15 @ X1 ) @ ( sK13 @ X1 ) ) ) )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ),
inference(beta-eta_normalization,[],[f179]) ).
thf(f181,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ ( sK15 @ X1 ) @ ( sK13 @ X1 ) )
= $false )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false = sF8 ) ),
inference(imp_proxy_clausification,[],[f180]) ).
thf(f182,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
& ( X1 @ ( sK15 @ X1 ) @ ( sK11 @ X1 ) ) ) )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 ) ),
inference(imp_proxy_clausification,[],[f180]) ).
thf(f183,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false = sF8 )
| ( $true
= ( X1 @ ( sK15 @ X1 ) @ ( sK11 @ X1 ) ) ) ),
inference(and_proxy_clausification,[],[f182]) ).
thf(f184,plain,
! [X1: $i > $i > $o] :
( ( $false = sF8 )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true ) ),
inference(and_proxy_clausification,[],[f182]) ).
thf(f206,plain,
( ( ( sK3 @ sK2 @ sK1 )
= $false )
| ( $true = sF5 ) ),
inference(iff_proxy_clausification,[],[f148]) ).
thf(f208,plain,
( ( ( ^ [Y0: $i > $i > $o,Y1: $i,Y2: $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y3: $i > $i > $o] :
( ( ( ^ [Y4: $i > $i > $o] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( Y4 @ Y5 @ Y6 )
& ( Y4 @ Y7 @ Y5 ) )
=> ( Y4 @ Y7 @ Y6 ) ) ) ) )
@ Y3 )
& ( ^ [Y4: $i > $i > $o,Y5: $i > $i > $o] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( Y4 @ Y7 @ Y6 )
=> ( Y5 @ Y7 @ Y6 ) ) ) )
@ Y0
@ Y3 ) )
=> ( Y3 @ Y1 @ Y2 ) ) )
@ sK4
@ sK2
@ sK0 )
= $true )
| ( $false = sF7 ) ),
inference(iff_proxy_clausification,[],[f152]) ).
thf(f209,plain,
( ( $true
= ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
& ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( sK4 @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) )
=> ( Y0 @ sK2 @ sK0 ) ) ) )
| ( $false = sF7 ) ),
inference(beta-eta_normalization,[],[f208]) ).
thf(f210,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( ^ [Y0: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
& ( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( sK4 @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) )
=> ( Y0 @ sK2 @ sK0 ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f209]) ).
thf(f211,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) )
& ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) )
=> ( X1 @ sK2 @ sK0 ) )
= $true ) ),
inference(beta-eta_normalization,[],[f210]) ).
thf(f212,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) )
& ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 ) ),
inference(imp_proxy_clausification,[],[f211]) ).
thf(f213,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) ) ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f212]) ).
thf(f214,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) )
@ ( sK17 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f213]) ).
thf(f215,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK18 @ X1 ) )
= $false )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( X1 @ Y0 @ Y1 )
& ( X1 @ Y2 @ Y0 ) )
=> ( X1 @ Y2 @ Y1 ) ) ) )
@ ( sK17 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f214]) ).
thf(f216,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) ) ) )
| ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK18 @ X1 ) )
=> ( X1 @ Y0 @ ( sK18 @ X1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f215]) ).
thf(f217,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK18 @ X1 ) )
=> ( X1 @ Y0 @ ( sK18 @ X1 ) ) ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 )
| ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK19 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f216]) ).
thf(f218,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ Y0 )
& ( X1 @ Y1 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y1 @ Y0 ) ) )
@ ( sK19 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 )
| ( $false
= ( ^ [Y0: $i] :
( ( sK4 @ Y0 @ ( sK18 @ X1 ) )
=> ( X1 @ Y0 @ ( sK18 @ X1 ) ) )
@ ( sK20 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f217]) ).
thf(f219,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 )
| ( $false
= ( ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) )
=> ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ Y0 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK19 @ X1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f218]) ).
thf(f220,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ Y0 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK19 @ X1 ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f219]) ).
thf(f221,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ Y0 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK19 @ X1 ) ) ) ) )
| ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ),
inference(imp_proxy_clausification,[],[f219]) ).
thf(f222,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ Y0 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK19 @ X1 ) ) )
@ ( sK21 @ X1 ) ) )
| ( $false = sF7 )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true ) ),
inference(sigma_proxy_clausification,[],[f221]) ).
thf(f223,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 )
| ( $false
= ( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ ( sK21 @ X1 ) @ ( sK17 @ X1 ) ) )
=> ( X1 @ ( sK21 @ X1 ) @ ( sK19 @ X1 ) ) ) )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f222]) ).
thf(f224,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK21 @ X1 ) @ ( sK19 @ X1 ) ) ) ),
inference(imp_proxy_clausification,[],[f223]) ).
thf(f225,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ ( sK21 @ X1 ) @ ( sK17 @ X1 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f223]) ).
thf(f226,plain,
! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false = sF7 )
| ( $true
= ( X1 @ ( sK21 @ X1 ) @ ( sK17 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true ) ),
inference(and_proxy_clausification,[],[f225]) ).
thf(f227,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 ) ),
inference(and_proxy_clausification,[],[f225]) ).
thf(f228,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( ^ [Y0: $i] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ Y0 @ ( sK17 @ X1 ) ) )
=> ( X1 @ Y0 @ ( sK19 @ X1 ) ) )
@ ( sK22 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f220]) ).
thf(f229,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false
= ( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ ( sK22 @ X1 ) @ ( sK17 @ X1 ) ) )
=> ( X1 @ ( sK22 @ X1 ) @ ( sK19 @ X1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f228]) ).
thf(f230,plain,
! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK22 @ X1 ) @ ( sK19 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false = sF7 ) ),
inference(imp_proxy_clausification,[],[f229]) ).
thf(f231,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
& ( X1 @ ( sK22 @ X1 ) @ ( sK17 @ X1 ) ) )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false = sF7 ) ),
inference(imp_proxy_clausification,[],[f229]) ).
thf(f232,plain,
! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $true
= ( X1 @ ( sK22 @ X1 ) @ ( sK17 @ X1 ) ) )
| ( $false = sF7 ) ),
inference(and_proxy_clausification,[],[f231]) ).
thf(f233,plain,
! [X1: $i > $i > $o] :
( ( $false = sF7 )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ),
inference(and_proxy_clausification,[],[f231]) ).
thf(f255,plain,
( ( sF9 = $false )
| ( $true
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y1 @ Y2 )
& ( Y0 @ Y3 @ Y1 ) )
=> ( Y0 @ Y3 @ Y2 ) ) ) ) )
@ sK3 ) ) ),
inference(iff_proxy_clausification,[],[f156]) ).
thf(f256,plain,
( ( sF9 = $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK3 @ Y0 @ Y1 )
& ( sK3 @ Y2 @ Y0 ) )
=> ( sK3 @ Y2 @ Y1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f255]) ).
thf(f257,plain,
! [X1: $i] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK3 @ Y0 @ Y1 )
& ( sK3 @ Y2 @ Y0 ) )
=> ( sK3 @ Y2 @ Y1 ) ) ) )
@ X1 )
= $true )
| ( sF9 = $false ) ),
inference(pi_proxy_clausification,[],[f256]) ).
thf(f258,plain,
! [X1: $i] :
( ( sF9 = $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK3 @ X1 @ Y0 )
& ( sK3 @ Y1 @ X1 ) )
=> ( sK3 @ Y1 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f257]) ).
thf(f259,plain,
! [X2: $i,X1: $i] :
( ( sF9 = $false )
| ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK3 @ X1 @ Y0 )
& ( sK3 @ Y1 @ X1 ) )
=> ( sK3 @ Y1 @ Y0 ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f258]) ).
thf(f260,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK3 @ X1 @ X2 )
& ( sK3 @ Y0 @ X1 ) )
=> ( sK3 @ Y0 @ X2 ) ) ) )
| ( sF9 = $false ) ),
inference(beta-eta_normalization,[],[f259]) ).
thf(f261,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK3 @ X1 @ X2 )
& ( sK3 @ Y0 @ X1 ) )
=> ( sK3 @ Y0 @ X2 ) )
@ X3 ) )
| ( sF9 = $false ) ),
inference(pi_proxy_clausification,[],[f260]) ).
thf(f262,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( ( ( sK3 @ X1 @ X2 )
& ( sK3 @ X3 @ X1 ) )
=> ( sK3 @ X3 @ X2 ) )
= $true )
| ( sF9 = $false ) ),
inference(beta-eta_normalization,[],[f261]) ).
thf(f263,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( sK3 @ X3 @ X2 )
= $true )
| ( sF9 = $false )
| ( ( ( sK3 @ X1 @ X2 )
& ( sK3 @ X3 @ X1 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f262]) ).
thf(f264,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( sK3 @ X1 @ X2 ) )
| ( ( sK3 @ X3 @ X2 )
= $true )
| ( $false
= ( sK3 @ X3 @ X1 ) )
| ( sF9 = $false ) ),
inference(and_proxy_clausification,[],[f263]) ).
thf(f277,plain,
( ( $false = sF6 )
| ( $true
= ( ^ [Y0: $i > $i > $o,Y1: $i > $i > $o] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) ) )
@ sK4
@ sK3 ) ) ),
inference(iff_proxy_clausification,[],[f150]) ).
thf(f278,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( sK3 @ Y1 @ Y0 ) ) ) ) )
| ( $false = sF6 ) ),
inference(beta-eta_normalization,[],[f277]) ).
thf(f279,plain,
! [X1: $i] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( sK4 @ Y1 @ Y0 )
=> ( sK3 @ Y1 @ Y0 ) ) )
@ X1 )
= $true )
| ( $false = sF6 ) ),
inference(pi_proxy_clausification,[],[f278]) ).
thf(f280,plain,
! [X1: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK4 @ Y0 @ X1 )
=> ( sK3 @ Y0 @ X1 ) ) ) )
| ( $false = sF6 ) ),
inference(beta-eta_normalization,[],[f279]) ).
thf(f281,plain,
! [X2: $i,X1: $i] :
( ( $false = sF6 )
| ( $true
= ( ^ [Y0: $i] :
( ( sK4 @ Y0 @ X1 )
=> ( sK3 @ Y0 @ X1 ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f280]) ).
thf(f282,plain,
! [X2: $i,X1: $i] :
( ( $false = sF6 )
| ( $true
= ( ( sK4 @ X2 @ X1 )
=> ( sK3 @ X2 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f281]) ).
thf(f283,plain,
! [X2: $i,X1: $i] :
( ( $false = sF6 )
| ( ( sK3 @ X2 @ X1 )
= $true )
| ( $false
= ( sK4 @ X2 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f282]) ).
thf(f292,definition,
( spl29_1
<=> ( $false = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
thf(f294,plain,
( ( $false = sF8 )
| ~ spl29_1 ),
inference(avatar_component_clause,[],[f292]) ).
thf(f296,definition,
( spl29_2
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ sK0 @ sK1 )
= $true )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
thf(f297,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true ) )
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f296]) ).
thf(f298,plain,
( spl29_1
| spl29_2 ),
inference(avatar_split_clause,[],[f178,f296,f292]) ).
thf(f300,definition,
( spl29_3
<=> ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $true
= ( X1 @ ( sK14 @ X1 ) @ ( sK11 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
thf(f301,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $true
= ( X1 @ ( sK14 @ X1 ) @ ( sK11 @ X1 ) ) ) )
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f300]) ).
thf(f302,plain,
( spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f177,f292,f300]) ).
thf(f304,definition,
( spl29_4
<=> ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK14 @ X1 ) @ ( sK13 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
thf(f305,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK14 @ X1 ) @ ( sK13 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f304]) ).
thf(f306,plain,
( spl29_1
| spl29_4 ),
inference(avatar_split_clause,[],[f175,f304,f292]) ).
thf(f308,definition,
( spl29_5
<=> ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
thf(f309,plain,
( ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ ( sK11 @ X1 ) @ ( sK13 @ X1 ) )
= $true )
| ( ( X1 @ sK0 @ sK1 )
= $true ) )
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f308]) ).
thf(f310,plain,
( spl29_1
| spl29_5 ),
inference(avatar_split_clause,[],[f184,f308,f292]) ).
thf(f312,definition,
( spl29_6
<=> ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( $true
= ( X1 @ ( sK15 @ X1 ) @ ( sK11 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
thf(f313,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( X1 @ ( sK15 @ X1 ) @ ( sK11 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) ) )
| ~ spl29_6 ),
inference(avatar_component_clause,[],[f312]) ).
thf(f314,plain,
( spl29_1
| spl29_6 ),
inference(avatar_split_clause,[],[f183,f312,f292]) ).
thf(f316,definition,
( spl29_7
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ ( sK15 @ X1 ) @ ( sK13 @ X1 ) )
= $false )
| ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
thf(f317,plain,
( ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK12 @ X1 ) @ ( sK10 @ X1 ) ) )
| ( ( X1 @ sK0 @ sK1 )
= $true )
| ( ( X1 @ ( sK15 @ X1 ) @ ( sK13 @ X1 ) )
= $false ) )
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f316]) ).
thf(f318,plain,
( spl29_7
| spl29_1 ),
inference(avatar_split_clause,[],[f181,f292,f316]) ).
thf(f323,definition,
( spl29_9
<=> ( sF8 = $true ) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
thf(f325,plain,
( ( sF8 = $true )
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f323]) ).
thf(f337,definition,
( spl29_12
<=> ( $true = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
thf(f341,definition,
( spl29_13
<=> ( ( sK3 @ sK2 @ sK1 )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
thf(f343,plain,
( ( ( sK3 @ sK2 @ sK1 )
= $false )
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f341]) ).
thf(f344,plain,
( spl29_12
| spl29_13 ),
inference(avatar_split_clause,[],[f206,f341,f337]) ).
thf(f354,plain,
spl29_9,
inference(avatar_split_clause,[],[f155,f323]) ).
thf(f356,definition,
( spl29_16
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
thf(f357,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true ) )
| ~ spl29_16 ),
inference(avatar_component_clause,[],[f356]) ).
thf(f359,definition,
( spl29_17
<=> ( $false = sF7 ) ),
introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).
thf(f361,plain,
( ( $false = sF7 )
| ~ spl29_17 ),
inference(avatar_component_clause,[],[f359]) ).
thf(f362,plain,
( spl29_16
| spl29_17 ),
inference(avatar_split_clause,[],[f227,f359,f356]) ).
thf(f364,definition,
( spl29_18
<=> ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( X1 @ ( sK21 @ X1 ) @ ( sK17 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_18])],[avatar_definition]) ).
thf(f365,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( X1 @ ( sK21 @ X1 ) @ ( sK17 @ X1 ) ) ) )
| ~ spl29_18 ),
inference(avatar_component_clause,[],[f364]) ).
thf(f366,plain,
( spl29_18
| spl29_17 ),
inference(avatar_split_clause,[],[f226,f359,f364]) ).
thf(f368,definition,
( spl29_19
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( X1 @ ( sK21 @ X1 ) @ ( sK19 @ X1 ) ) )
| ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
thf(f369,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( sK4 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK21 @ X1 ) @ ( sK19 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true ) )
| ~ spl29_19 ),
inference(avatar_component_clause,[],[f368]) ).
thf(f370,plain,
( spl29_17
| spl29_19 ),
inference(avatar_split_clause,[],[f224,f368,f359]) ).
thf(f372,definition,
( spl29_20
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
thf(f373,plain,
( ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( ( X1 @ ( sK17 @ X1 ) @ ( sK19 @ X1 ) )
= $true ) )
| ~ spl29_20 ),
inference(avatar_component_clause,[],[f372]) ).
thf(f374,plain,
( spl29_20
| spl29_17 ),
inference(avatar_split_clause,[],[f233,f359,f372]) ).
thf(f376,definition,
( spl29_21
<=> ! [X1: $i > $i > $o] :
( ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $true
= ( X1 @ ( sK22 @ X1 ) @ ( sK17 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
thf(f377,plain,
( ! [X1: $i > $i > $o] :
( ( $true
= ( X1 @ ( sK22 @ X1 ) @ ( sK17 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true ) )
| ~ spl29_21 ),
inference(avatar_component_clause,[],[f376]) ).
thf(f378,plain,
( spl29_17
| spl29_21 ),
inference(avatar_split_clause,[],[f232,f376,f359]) ).
thf(f380,definition,
( spl29_22
<=> ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK22 @ X1 ) @ ( sK19 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_22])],[avatar_definition]) ).
thf(f381,plain,
( ! [X1: $i > $i > $o] :
( ( $false
= ( X1 @ ( sK22 @ X1 ) @ ( sK19 @ X1 ) ) )
| ( $false
= ( X1 @ ( sK20 @ X1 ) @ ( sK18 @ X1 ) ) )
| ( ( X1 @ sK2 @ sK0 )
= $true ) )
| ~ spl29_22 ),
inference(avatar_component_clause,[],[f380]) ).
thf(f382,plain,
( spl29_22
| spl29_17 ),
inference(avatar_split_clause,[],[f230,f359,f380]) ).
thf(f387,definition,
( spl29_24
<=> ( sF7 = $true ) ),
introduced(definition,[new_symbols(definition,[spl29_24])],[avatar_definition]) ).
thf(f389,plain,
( ( sF7 = $true )
| ~ spl29_24 ),
inference(avatar_component_clause,[],[f387]) ).
thf(f401,definition,
( spl29_27
<=> ( sF9 = $false ) ),
introduced(definition,[new_symbols(definition,[spl29_27])],[avatar_definition]) ).
thf(f403,plain,
( ( sF9 = $false )
| ~ spl29_27 ),
inference(avatar_component_clause,[],[f401]) ).
thf(f405,definition,
( spl29_28
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( $false
= ( sK3 @ X1 @ X2 ) )
| ( $false
= ( sK3 @ X3 @ X1 ) )
| ( ( sK3 @ X3 @ X2 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_28])],[avatar_definition]) ).
thf(f406,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( sK3 @ X3 @ X1 ) )
| ( ( sK3 @ X3 @ X2 )
= $true )
| ( $false
= ( sK3 @ X1 @ X2 ) ) )
| ~ spl29_28 ),
inference(avatar_component_clause,[],[f405]) ).
thf(f407,plain,
( spl29_27
| spl29_28 ),
inference(avatar_split_clause,[],[f264,f405,f401]) ).
thf(f409,definition,
( spl29_29
<=> ( sF9 = $true ) ),
introduced(definition,[new_symbols(definition,[spl29_29])],[avatar_definition]) ).
thf(f411,plain,
( ( sF9 = $true )
| ~ spl29_29 ),
inference(avatar_component_clause,[],[f409]) ).
thf(f427,plain,
spl29_24,
inference(avatar_split_clause,[],[f153,f387]) ).
thf(f429,definition,
( spl29_33
<=> ! [X2: $i,X1: $i] :
( ( ( sK3 @ X2 @ X1 )
= $true )
| ( $false
= ( sK4 @ X2 @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_33])],[avatar_definition]) ).
thf(f430,plain,
( ! [X2: $i,X1: $i] :
( ( $false
= ( sK4 @ X2 @ X1 ) )
| ( ( sK3 @ X2 @ X1 )
= $true ) )
| ~ spl29_33 ),
inference(avatar_component_clause,[],[f429]) ).
thf(f432,definition,
( spl29_34
<=> ( $false = sF6 ) ),
introduced(definition,[new_symbols(definition,[spl29_34])],[avatar_definition]) ).
thf(f434,plain,
( ( $false = sF6 )
| ~ spl29_34 ),
inference(avatar_component_clause,[],[f432]) ).
thf(f435,plain,
( spl29_33
| spl29_34 ),
inference(avatar_split_clause,[],[f283,f432,f429]) ).
thf(f437,definition,
( spl29_35
<=> ( $true = sF6 ) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
thf(f439,plain,
( ( $true = sF6 )
| ~ spl29_35 ),
inference(avatar_component_clause,[],[f437]) ).
thf(f450,plain,
~ spl29_12,
inference(avatar_split_clause,[],[f149,f337]) ).
thf(f451,plain,
spl29_35,
inference(avatar_split_clause,[],[f151,f437]) ).
thf(f452,plain,
spl29_29,
inference(avatar_split_clause,[],[f157,f409]) ).
thf(f467,plain,
( ( $false = $true )
| ~ spl29_27
| ~ spl29_29 ),
inference(forward_demodulation,[],[f411,f403]) ).
thf(f468,plain,
( $false
| ~ spl29_27
| ~ spl29_29 ),
inference(trivial_inequality_removal,[],[f467]) ).
thf(f469,plain,
( ~ spl29_27
| ~ spl29_29 ),
inference(avatar_contradiction_clause,[],[f468]) ).
thf(f472,plain,
( ( $false = $true )
| ~ spl29_17
| ~ spl29_24 ),
inference(forward_demodulation,[],[f361,f389]) ).
thf(f473,plain,
( $false
| ~ spl29_17
| ~ spl29_24 ),
inference(trivial_inequality_removal,[],[f472]) ).
thf(f474,plain,
( ~ spl29_17
| ~ spl29_24 ),
inference(avatar_contradiction_clause,[],[f473]) ).
thf(f511,plain,
( ( $false = $true )
| ~ spl29_1
| ~ spl29_9 ),
inference(forward_demodulation,[],[f294,f325]) ).
thf(f512,plain,
( $false
| ~ spl29_1
| ~ spl29_9 ),
inference(trivial_inequality_removal,[],[f511]) ).
thf(f513,plain,
( ~ spl29_1
| ~ spl29_9 ),
inference(avatar_contradiction_clause,[],[f512]) ).
thf(f589,plain,
( ! [X0: $i] :
( ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( ( sK3 @ ( sK15 @ sK3 ) @ X0 )
= $true )
| ( $false = $true )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) )
| ( $false
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) ) )
| ~ spl29_6
| ~ spl29_28 ),
inference(constrained_superposition,[],[f313,f406]) ).
thf(f596,plain,
( ! [X0: $i] :
( ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( ( sK3 @ ( sK15 @ sK3 ) @ X0 )
= $true )
| ( $false
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) ) )
| ~ spl29_6
| ~ spl29_28 ),
inference(trivial_inequality_removal,[],[f589]) ).
thf(f608,definition,
( spl29_45
<=> ( $false
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_45])],[avatar_definition]) ).
thf(f610,plain,
( ( $false
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_45 ),
inference(avatar_component_clause,[],[f608]) ).
thf(f612,definition,
( spl29_46
<=> ( ( sK3 @ sK0 @ sK1 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl29_46])],[avatar_definition]) ).
thf(f613,plain,
( ( ( sK3 @ sK0 @ sK1 )
!= $true )
| spl29_46 ),
inference(avatar_component_clause,[],[f612]) ).
thf(f614,plain,
( ( ( sK3 @ sK0 @ sK1 )
= $true )
| ~ spl29_46 ),
inference(avatar_component_clause,[],[f612]) ).
thf(f616,definition,
( spl29_47
<=> ! [X0: $i] :
( ( ( sK3 @ ( sK15 @ sK3 ) @ X0 )
= $true )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_47])],[avatar_definition]) ).
thf(f617,plain,
( ! [X0: $i] :
( ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) )
| ( ( sK3 @ ( sK15 @ sK3 ) @ X0 )
= $true ) )
| ~ spl29_47 ),
inference(avatar_component_clause,[],[f616]) ).
thf(f619,plain,
( spl29_46
| spl29_45
| spl29_47
| ~ spl29_6
| ~ spl29_28 ),
inference(avatar_split_clause,[],[f596,f405,f312,f616,f608,f612]) ).
thf(f620,plain,
( ( $false = $true )
| ~ spl29_34
| ~ spl29_35 ),
inference(forward_demodulation,[],[f434,f439]) ).
thf(f621,plain,
( $false
| ~ spl29_34
| ~ spl29_35 ),
inference(trivial_inequality_removal,[],[f620]) ).
thf(f622,plain,
( ~ spl29_34
| ~ spl29_35 ),
inference(avatar_contradiction_clause,[],[f621]) ).
thf(f630,plain,
( ! [X0: $i > $i > $o] :
( ( ( X0 @ ( sK11 @ X0 ) @ ( sK13 @ X0 ) )
= $true )
| ( ( X0 @ sK0 @ sK1 )
= $true )
| ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true )
| ( $false = $true ) )
| ~ spl29_2
| ~ spl29_33 ),
inference(constrained_superposition,[],[f430,f297]) ).
thf(f631,plain,
( ! [X0: $i > $i > $o] :
( ( ( X0 @ sK0 @ sK1 )
= $true )
| ( $false = $true )
| ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true )
| ( $false
= ( X0 @ ( sK14 @ X0 ) @ ( sK13 @ X0 ) ) ) )
| ~ spl29_4
| ~ spl29_33 ),
inference(constrained_superposition,[],[f430,f305]) ).
thf(f632,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) )
| ( $false
= ( X0 @ ( sK21 @ X0 ) @ ( sK19 @ X0 ) ) )
| ( $false = $true )
| ( $true
= ( X0 @ sK2 @ sK0 ) ) )
| ~ spl29_19
| ~ spl29_33 ),
inference(constrained_superposition,[],[f430,f369]) ).
thf(f636,plain,
( ! [X0: $i > $i > $o] :
( ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true )
| ( ( X0 @ sK0 @ sK1 )
= $true )
| ( $false = $true )
| ( $true
= ( X0 @ ( sK14 @ X0 ) @ ( sK11 @ X0 ) ) ) )
| ~ spl29_3
| ~ spl29_33 ),
inference(constrained_superposition,[],[f301,f430]) ).
thf(f642,plain,
( ! [X0: $i > $i > $o] :
( ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true )
| ( ( X0 @ ( sK11 @ X0 ) @ ( sK13 @ X0 ) )
= $true )
| ( ( X0 @ sK0 @ sK1 )
= $true ) )
| ~ spl29_2
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f630]) ).
thf(f643,plain,
( ! [X0: $i > $i > $o] :
( ( $false
= ( X0 @ ( sK14 @ X0 ) @ ( sK13 @ X0 ) ) )
| ( ( X0 @ sK0 @ sK1 )
= $true )
| ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true ) )
| ~ spl29_4
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f631]) ).
thf(f646,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) )
| ( $true
= ( X0 @ sK2 @ sK0 ) )
| ( $false
= ( X0 @ ( sK21 @ X0 ) @ ( sK19 @ X0 ) ) ) )
| ~ spl29_19
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f632]) ).
thf(f647,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( X0 @ ( sK14 @ X0 ) @ ( sK11 @ X0 ) ) )
| ( ( X0 @ sK0 @ sK1 )
= $true )
| ( ( sK3 @ ( sK12 @ X0 ) @ ( sK10 @ X0 ) )
= $true ) )
| ~ spl29_3
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f636]) ).
thf(f670,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( X0 @ sK2 @ sK0 ) )
| ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) )
| ( ( X0 @ ( sK17 @ X0 ) @ ( sK19 @ X0 ) )
= $true )
| ( $false = $true ) )
| ~ spl29_16
| ~ spl29_33 ),
inference(constrained_superposition,[],[f357,f430]) ).
thf(f672,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) )
| ( $true
= ( X0 @ sK2 @ sK0 ) )
| ( ( X0 @ ( sK17 @ X0 ) @ ( sK19 @ X0 ) )
= $true ) )
| ~ spl29_16
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f670]) ).
thf(f694,plain,
( ! [X0: $i > $i > $o] :
( ( ( X0 @ ( sK21 @ X0 ) @ ( sK17 @ X0 ) )
= $true )
| ( $false = $true )
| ( $true
= ( X0 @ sK2 @ sK0 ) )
| ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) ) )
| ~ spl29_18
| ~ spl29_33 ),
inference(constrained_superposition,[],[f430,f365]) ).
thf(f695,plain,
( ! [X0: $i > $i > $o] :
( ( $true
= ( sK3 @ ( sK20 @ X0 ) @ ( sK18 @ X0 ) ) )
| ( ( X0 @ ( sK21 @ X0 ) @ ( sK17 @ X0 ) )
= $true )
| ( $true
= ( X0 @ sK2 @ sK0 ) ) )
| ~ spl29_18
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f694]) ).
thf(f758,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ( ( sK3 @ ( sK22 @ sK3 ) @ X0 )
= $true )
| ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) ) )
| ~ spl29_21
| ~ spl29_28 ),
inference(constrained_superposition,[],[f406,f377]) ).
thf(f763,plain,
( ! [X0: $i] :
( ( ( sK3 @ ( sK22 @ sK3 ) @ X0 )
= $true )
| ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) )
| ( $true
= ( sK3 @ sK2 @ sK0 ) ) )
| ~ spl29_21
| ~ spl29_28 ),
inference(trivial_inequality_removal,[],[f758]) ).
thf(f775,definition,
( spl29_54
<=> ! [X0: $i] :
( ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) )
| ( ( sK3 @ ( sK22 @ sK3 ) @ X0 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl29_54])],[avatar_definition]) ).
thf(f776,plain,
( ! [X0: $i] :
( ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) )
| ( ( sK3 @ ( sK22 @ sK3 ) @ X0 )
= $true ) )
| ~ spl29_54 ),
inference(avatar_component_clause,[],[f775]) ).
thf(f778,definition,
( spl29_55
<=> ( $true
= ( sK3 @ sK2 @ sK0 ) ) ),
introduced(definition,[new_symbols(definition,[spl29_55])],[avatar_definition]) ).
thf(f779,plain,
( ( $true
!= ( sK3 @ sK2 @ sK0 ) )
| spl29_55 ),
inference(avatar_component_clause,[],[f778]) ).
thf(f780,plain,
( ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_55 ),
inference(avatar_component_clause,[],[f778]) ).
thf(f782,definition,
( spl29_56
<=> ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_56])],[avatar_definition]) ).
thf(f783,plain,
( ( $false
!= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| spl29_56 ),
inference(avatar_component_clause,[],[f782]) ).
thf(f784,plain,
( ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ~ spl29_56 ),
inference(avatar_component_clause,[],[f782]) ).
thf(f786,plain,
( spl29_55
| spl29_56
| spl29_54
| ~ spl29_21
| ~ spl29_28 ),
inference(avatar_split_clause,[],[f763,f405,f376,f775,f782,f778]) ).
thf(f792,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ sK2 @ X0 ) )
| ( $false
= ( sK3 @ sK0 @ X0 ) )
| ( $false = $true ) )
| ~ spl29_28
| ~ spl29_55 ),
inference(constrained_superposition,[],[f780,f406]) ).
thf(f794,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ sK2 @ X0 ) )
| ( $false
= ( sK3 @ sK0 @ X0 ) ) )
| ~ spl29_28
| ~ spl29_55 ),
inference(trivial_inequality_removal,[],[f792]) ).
thf(f796,plain,
( ( $false = $true )
| ( $false
= ( sK3 @ sK0 @ sK1 ) )
| ~ spl29_13
| ~ spl29_28
| ~ spl29_55 ),
inference(constrained_superposition,[],[f794,f343]) ).
thf(f803,plain,
( ( $false
= ( sK3 @ sK0 @ sK1 ) )
| ~ spl29_13
| ~ spl29_28
| ~ spl29_55 ),
inference(trivial_inequality_removal,[],[f796]) ).
thf(f807,plain,
( ( $false = $true )
| ~ spl29_13
| ~ spl29_28
| ~ spl29_46
| ~ spl29_55 ),
inference(forward_demodulation,[],[f803,f614]) ).
thf(f808,plain,
( $false
| ~ spl29_13
| ~ spl29_28
| ~ spl29_46
| ~ spl29_55 ),
inference(trivial_inequality_removal,[],[f807]) ).
thf(f809,plain,
( ~ spl29_13
| ~ spl29_28
| ~ spl29_46
| ~ spl29_55 ),
inference(avatar_contradiction_clause,[],[f808]) ).
thf(f851,plain,
( ( $false
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK19 @ sK3 ) ) )
| ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_19
| ~ spl29_33
| ~ spl29_56 ),
inference(constrained_superposition,[],[f646,f784]) ).
thf(f863,plain,
( ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( $false
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK19 @ sK3 ) ) )
| ~ spl29_19
| ~ spl29_33
| ~ spl29_56 ),
inference(trivial_inequality_removal,[],[f851]) ).
thf(f867,plain,
( ( $false
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK19 @ sK3 ) ) )
| ~ spl29_19
| ~ spl29_33
| spl29_55
| ~ spl29_56 ),
inference(forward_subsumption_resolution,[],[f863,f779]) ).
thf(f870,definition,
( spl29_57
<=> ( $false
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK19 @ sK3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_57])],[avatar_definition]) ).
thf(f872,plain,
( ( $false
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK19 @ sK3 ) ) )
| ~ spl29_57 ),
inference(avatar_component_clause,[],[f870]) ).
thf(f874,definition,
( spl29_58
<=> ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl29_58])],[avatar_definition]) ).
thf(f876,plain,
( ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ~ spl29_58 ),
inference(avatar_component_clause,[],[f874]) ).
thf(f879,plain,
( spl29_57
| ~ spl29_19
| ~ spl29_33
| spl29_55
| ~ spl29_56 ),
inference(avatar_split_clause,[],[f867,f782,f778,f429,f368,f870]) ).
thf(f886,plain,
( ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $false = $true )
| ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ~ spl29_2
| ~ spl29_5
| ~ spl29_33 ),
inference(constrained_superposition,[],[f309,f642]) ).
thf(f896,plain,
( ( $false = $true )
| ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ~ spl29_2
| ~ spl29_5
| ~ spl29_33 ),
inference(duplicate_literal_removal,[],[f886]) ).
thf(f897,plain,
( ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ~ spl29_2
| ~ spl29_5
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f896]) ).
thf(f898,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ( $true
= ( sK3 @ ( sK14 @ sK3 ) @ X0 ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) )
| ( $false = $true ) )
| ~ spl29_3
| ~ spl29_28
| ~ spl29_33 ),
inference(constrained_superposition,[],[f647,f406]) ).
thf(f902,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ ( sK14 @ sK3 ) @ X0 ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) ) )
| ~ spl29_3
| ~ spl29_28
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f898]) ).
thf(f940,plain,
( ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_16
| ~ spl29_20
| ~ spl29_33 ),
inference(constrained_superposition,[],[f373,f672]) ).
thf(f941,plain,
( ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ~ spl29_16
| ~ spl29_20
| ~ spl29_33 ),
inference(duplicate_literal_removal,[],[f940]) ).
thf(f942,plain,
( ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_16
| ~ spl29_20
| ~ spl29_33 ),
inference(trivial_inequality_removal,[],[f941]) ).
thf(f949,plain,
( ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ~ spl29_16
| ~ spl29_20
| ~ spl29_33
| spl29_55 ),
inference(forward_subsumption_resolution,[],[f942,f779]) ).
thf(f953,plain,
( spl29_58
| ~ spl29_16
| ~ spl29_20
| ~ spl29_33
| spl29_55 ),
inference(avatar_split_clause,[],[f949,f778,f429,f372,f356,f874]) ).
thf(f974,plain,
( ( $true
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK17 @ sK3 ) ) )
| ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_18
| ~ spl29_33
| ~ spl29_56 ),
inference(constrained_superposition,[],[f695,f784]) ).
thf(f980,plain,
( ( $true
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK17 @ sK3 ) ) )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ~ spl29_18
| ~ spl29_33
| ~ spl29_56 ),
inference(trivial_inequality_removal,[],[f974]) ).
thf(f988,plain,
( ( $true
= ( sK3 @ ( sK21 @ sK3 ) @ ( sK17 @ sK3 ) ) )
| ~ spl29_18
| ~ spl29_33
| spl29_55
| ~ spl29_56 ),
inference(forward_subsumption_resolution,[],[f980,f779]) ).
thf(f991,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $true
= ( sK3 @ ( sK21 @ sK3 ) @ X0 ) )
| ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) ) )
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56 ),
inference(constrained_superposition,[],[f406,f988]) ).
thf(f992,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ ( sK21 @ sK3 ) @ X0 ) )
| ( $false
= ( sK3 @ ( sK17 @ sK3 ) @ X0 ) ) )
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56 ),
inference(trivial_inequality_removal,[],[f991]) ).
thf(f994,plain,
( ( $false = $true )
| ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $false )
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57 ),
inference(constrained_superposition,[],[f992,f872]) ).
thf(f1001,plain,
( ( ( sK3 @ ( sK17 @ sK3 ) @ ( sK19 @ sK3 ) )
= $false )
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57 ),
inference(trivial_inequality_removal,[],[f994]) ).
thf(f1005,plain,
( ( $false = $true )
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57
| ~ spl29_58 ),
inference(forward_demodulation,[],[f1001,f876]) ).
thf(f1006,plain,
( $false
| ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57
| ~ spl29_58 ),
inference(trivial_inequality_removal,[],[f1005]) ).
thf(f1007,plain,
( ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57
| ~ spl29_58 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
thf(f1009,definition,
( spl29_61
<=> ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_61])],[avatar_definition]) ).
thf(f1011,plain,
( ( $true
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ~ spl29_61 ),
inference(avatar_component_clause,[],[f1009]) ).
thf(f1024,definition,
( spl29_64
<=> ! [X0: $i] :
( ( $true
= ( sK3 @ ( sK14 @ sK3 ) @ X0 ) )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_64])],[avatar_definition]) ).
thf(f1025,plain,
( ! [X0: $i] :
( ( $true
= ( sK3 @ ( sK14 @ sK3 ) @ X0 ) )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ X0 ) ) )
| ~ spl29_64 ),
inference(avatar_component_clause,[],[f1024]) ).
thf(f1027,definition,
( spl29_65
<=> ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl29_65])],[avatar_definition]) ).
thf(f1029,plain,
( ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_65 ),
inference(avatar_component_clause,[],[f1027]) ).
thf(f1031,plain,
( spl29_46
| spl29_65
| spl29_64
| ~ spl29_3
| ~ spl29_28
| ~ spl29_33 ),
inference(avatar_split_clause,[],[f902,f429,f405,f300,f1024,f1027,f612]) ).
thf(f1033,plain,
( spl29_61
| spl29_46
| ~ spl29_2
| ~ spl29_5
| ~ spl29_33 ),
inference(avatar_split_clause,[],[f897,f429,f308,f296,f612,f1009]) ).
thf(f1057,plain,
( ( $false = $true )
| ( $true
= ( sK3 @ ( sK15 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ~ spl29_47
| ~ spl29_61 ),
inference(constrained_superposition,[],[f617,f1011]) ).
thf(f1059,plain,
( ( $true
= ( sK3 @ ( sK15 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ~ spl29_47
| ~ spl29_61 ),
inference(trivial_inequality_removal,[],[f1057]) ).
thf(f1073,plain,
( ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $false = $true )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ~ spl29_4
| ~ spl29_33
| ~ spl29_64 ),
inference(constrained_superposition,[],[f1025,f643]) ).
thf(f1076,plain,
( ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_4
| ~ spl29_33
| ~ spl29_64 ),
inference(trivial_inequality_removal,[],[f1073]) ).
thf(f1080,plain,
( ( $false
= ( sK3 @ ( sK11 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_4
| ~ spl29_33
| spl29_46
| ~ spl29_64 ),
inference(forward_subsumption_resolution,[],[f1076,f613]) ).
thf(f1082,plain,
( ( $false = $true )
| ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_4
| ~ spl29_33
| spl29_46
| ~ spl29_61
| ~ spl29_64 ),
inference(forward_demodulation,[],[f1080,f1011]) ).
thf(f1083,plain,
( ( $true
= ( sK3 @ ( sK12 @ sK3 ) @ ( sK10 @ sK3 ) ) )
| ~ spl29_4
| ~ spl29_33
| spl29_46
| ~ spl29_61
| ~ spl29_64 ),
inference(trivial_inequality_removal,[],[f1082]) ).
thf(f1086,plain,
( spl29_65
| ~ spl29_4
| ~ spl29_33
| spl29_46
| ~ spl29_61
| ~ spl29_64 ),
inference(avatar_split_clause,[],[f1083,f1024,f1009,f612,f429,f304,f1027]) ).
thf(f1092,plain,
( ( ( sK3 @ sK0 @ sK1 )
= $true )
| ( $false
= ( sK3 @ ( sK15 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( $false = $true )
| ~ spl29_7
| ~ spl29_65 ),
inference(constrained_superposition,[],[f317,f1029]) ).
thf(f1097,plain,
( ( $false
= ( sK3 @ ( sK15 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ( ( sK3 @ sK0 @ sK1 )
= $true )
| ~ spl29_7
| ~ spl29_65 ),
inference(trivial_inequality_removal,[],[f1092]) ).
thf(f1100,plain,
( ( $false
= ( sK3 @ ( sK15 @ sK3 ) @ ( sK13 @ sK3 ) ) )
| ~ spl29_7
| spl29_46
| ~ spl29_65 ),
inference(forward_subsumption_resolution,[],[f1097,f613]) ).
thf(f1104,plain,
( ( $false = $true )
| ~ spl29_7
| spl29_46
| ~ spl29_47
| ~ spl29_61
| ~ spl29_65 ),
inference(forward_demodulation,[],[f1100,f1059]) ).
thf(f1105,plain,
( $false
| ~ spl29_7
| spl29_46
| ~ spl29_47
| ~ spl29_61
| ~ spl29_65 ),
inference(trivial_inequality_removal,[],[f1104]) ).
thf(f1106,plain,
( ~ spl29_7
| spl29_46
| ~ spl29_47
| ~ spl29_61
| ~ spl29_65 ),
inference(avatar_contradiction_clause,[],[f1105]) ).
thf(f1108,plain,
( ( $false = $true )
| ~ spl29_45
| ~ spl29_65 ),
inference(forward_demodulation,[],[f610,f1029]) ).
thf(f1109,plain,
( $false
| ~ spl29_45
| ~ spl29_65 ),
inference(trivial_inequality_removal,[],[f1108]) ).
thf(f1110,plain,
( ~ spl29_45
| ~ spl29_65 ),
inference(avatar_contradiction_clause,[],[f1109]) ).
thf(f1134,plain,
( ( $false = $true )
| ( ( sK3 @ ( sK22 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ~ spl29_54
| ~ spl29_58 ),
inference(constrained_superposition,[],[f776,f876]) ).
thf(f1144,plain,
( ( ( sK3 @ ( sK22 @ sK3 ) @ ( sK19 @ sK3 ) )
= $true )
| ~ spl29_54
| ~ spl29_58 ),
inference(trivial_inequality_removal,[],[f1134]) ).
thf(f1155,plain,
( ( $false = $true )
| ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ~ spl29_22
| ~ spl29_54
| ~ spl29_58 ),
inference(constrained_superposition,[],[f381,f1144]) ).
thf(f1159,plain,
( ( $true
= ( sK3 @ sK2 @ sK0 ) )
| ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ~ spl29_22
| ~ spl29_54
| ~ spl29_58 ),
inference(trivial_inequality_removal,[],[f1155]) ).
thf(f1161,plain,
( ( $false
= ( sK3 @ ( sK20 @ sK3 ) @ ( sK18 @ sK3 ) ) )
| ~ spl29_22
| ~ spl29_54
| spl29_55
| ~ spl29_58 ),
inference(forward_subsumption_resolution,[],[f1159,f779]) ).
thf(f1164,plain,
( $false
| ~ spl29_22
| ~ spl29_54
| spl29_55
| spl29_56
| ~ spl29_58 ),
inference(forward_subsumption_resolution,[],[f1161,f783]) ).
thf(f1165,plain,
( ~ spl29_22
| ~ spl29_54
| spl29_55
| spl29_56
| ~ spl29_58 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
cnf(s1,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f298]) ).
cnf(s2,plain,
( spl29_1
| spl29_3 ),
inference(sat_conversion,[],[f302]) ).
cnf(s3,plain,
( spl29_1
| spl29_4 ),
inference(sat_conversion,[],[f306]) ).
cnf(s4,plain,
( spl29_1
| spl29_5 ),
inference(sat_conversion,[],[f310]) ).
cnf(s5,plain,
( spl29_1
| spl29_6 ),
inference(sat_conversion,[],[f314]) ).
cnf(s6,plain,
( spl29_1
| spl29_7 ),
inference(sat_conversion,[],[f318]) ).
cnf(s10,plain,
( spl29_12
| spl29_13 ),
inference(sat_conversion,[],[f344]) ).
cnf(s12,plain,
spl29_9,
inference(sat_conversion,[],[f354]) ).
cnf(s13,plain,
( spl29_16
| spl29_17 ),
inference(sat_conversion,[],[f362]) ).
cnf(s14,plain,
( spl29_17
| spl29_18 ),
inference(sat_conversion,[],[f366]) ).
cnf(s15,plain,
( spl29_17
| spl29_19 ),
inference(sat_conversion,[],[f370]) ).
cnf(s16,plain,
( spl29_17
| spl29_20 ),
inference(sat_conversion,[],[f374]) ).
cnf(s17,plain,
( spl29_17
| spl29_21 ),
inference(sat_conversion,[],[f378]) ).
cnf(s18,plain,
( spl29_17
| spl29_22 ),
inference(sat_conversion,[],[f382]) ).
cnf(s22,plain,
( spl29_27
| spl29_28 ),
inference(sat_conversion,[],[f407]) ).
cnf(s26,plain,
spl29_24,
inference(sat_conversion,[],[f427]) ).
cnf(s27,plain,
( spl29_33
| spl29_34 ),
inference(sat_conversion,[],[f435]) ).
cnf(s30,plain,
~ spl29_12,
inference(sat_conversion,[],[f450]) ).
cnf(s31,plain,
spl29_35,
inference(sat_conversion,[],[f451]) ).
cnf(s32,plain,
spl29_29,
inference(sat_conversion,[],[f452]) ).
cnf(s33,plain,
( ~ spl29_27
| ~ spl29_29 ),
inference(sat_conversion,[],[f469]) ).
cnf(s34,plain,
( ~ spl29_17
| ~ spl29_24 ),
inference(sat_conversion,[],[f474]) ).
cnf(s37,plain,
( ~ spl29_1
| ~ spl29_9 ),
inference(sat_conversion,[],[f513]) ).
cnf(s47,plain,
( ~ spl29_6
| ~ spl29_28
| spl29_45
| spl29_46
| spl29_47 ),
inference(sat_conversion,[],[f619]) ).
cnf(s48,plain,
( ~ spl29_34
| ~ spl29_35 ),
inference(sat_conversion,[],[f622]) ).
cnf(s60,plain,
( ~ spl29_21
| ~ spl29_28
| spl29_54
| spl29_55
| spl29_56 ),
inference(sat_conversion,[],[f786]) ).
cnf(s64,plain,
( ~ spl29_13
| ~ spl29_28
| ~ spl29_46
| ~ spl29_55 ),
inference(sat_conversion,[],[f809]) ).
cnf(s67,plain,
( ~ spl29_19
| ~ spl29_33
| spl29_55
| ~ spl29_56
| spl29_57 ),
inference(sat_conversion,[],[f879]) ).
cnf(s71,plain,
( ~ spl29_16
| ~ spl29_20
| ~ spl29_33
| spl29_55
| spl29_58 ),
inference(sat_conversion,[],[f953]) ).
cnf(s76,plain,
( ~ spl29_18
| ~ spl29_28
| ~ spl29_33
| spl29_55
| ~ spl29_56
| ~ spl29_57
| ~ spl29_58 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s81,plain,
( ~ spl29_3
| ~ spl29_28
| ~ spl29_33
| spl29_46
| spl29_64
| spl29_65 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s83,plain,
( ~ spl29_2
| ~ spl29_5
| ~ spl29_33
| spl29_46
| spl29_61 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s85,plain,
( ~ spl29_4
| ~ spl29_33
| spl29_46
| ~ spl29_61
| ~ spl29_64
| spl29_65 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s88,plain,
( ~ spl29_7
| spl29_46
| ~ spl29_47
| ~ spl29_61
| ~ spl29_65 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s90,plain,
( ~ spl29_45
| ~ spl29_65 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s95,plain,
( ~ spl29_22
| ~ spl29_54
| spl29_55
| spl29_56
| ~ spl29_58 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s96,plain,
~ spl29_27,
inference(rat,[],[s33,s32]) ).
cnf(s97,plain,
~ spl29_34,
inference(rat,[],[s48,s31]) ).
cnf(s98,plain,
spl29_33,
inference(rat,[],[s27,s97]) ).
cnf(s99,plain,
~ spl29_17,
inference(rat,[],[s34,s26]) ).
cnf(s100,plain,
spl29_28,
inference(rat,[],[s22,s96]) ).
cnf(s101,plain,
spl29_22,
inference(rat,[],[s18,s99]) ).
cnf(s102,plain,
spl29_21,
inference(rat,[],[s17,s99]) ).
cnf(s103,plain,
spl29_20,
inference(rat,[],[s16,s99]) ).
cnf(s104,plain,
spl29_19,
inference(rat,[],[s15,s99]) ).
cnf(s105,plain,
spl29_18,
inference(rat,[],[s14,s99]) ).
cnf(s106,plain,
spl29_16,
inference(rat,[],[s13,s99]) ).
cnf(s107,plain,
~ spl29_1,
inference(rat,[],[s37,s12]) ).
cnf(s108,plain,
spl29_13,
inference(rat,[],[s10,s30]) ).
cnf(s109,plain,
spl29_7,
inference(rat,[],[s6,s107]) ).
cnf(s110,plain,
spl29_6,
inference(rat,[],[s5,s107]) ).
cnf(s111,plain,
spl29_5,
inference(rat,[],[s4,s107]) ).
cnf(s112,plain,
spl29_4,
inference(rat,[],[s3,s107]) ).
cnf(s113,plain,
spl29_3,
inference(rat,[],[s2,s107]) ).
cnf(s114,plain,
spl29_2,
inference(rat,[],[s1,s107]) ).
cnf(s115,plain,
( ~ spl29_61
| spl29_65
| spl29_46 ),
inference(rat,[],[s81,s85,s112,s113,s100,s98]) ).
cnf(s116,plain,
( ~ spl29_47
| spl29_46
| ~ spl29_61 ),
inference(rat,[],[s115,s88,s109]) ).
cnf(s117,plain,
( spl29_46
| spl29_45 ),
inference(rat,[],[s116,s83,s47,s110,s100,s114,s111,s98]) ).
cnf(s118,plain,
( ~ spl29_56
| ~ spl29_58
| spl29_55 ),
inference(rat,[],[s67,s76,s105,s100,s104,s98]) ).
cnf(s119,plain,
( spl29_56
| ~ spl29_58
| spl29_55 ),
inference(rat,[],[s60,s95,s101,s102,s100]) ).
cnf(s120,plain,
( ~ spl29_58
| spl29_55 ),
inference(rat,[],[s119,s118]) ).
cnf(s121,plain,
spl29_55,
inference(rat,[],[s120,s71,s98,s103,s106]) ).
cnf(s122,plain,
~ spl29_46,
inference(rat,[],[s64,s108,s100,s121]) ).
cnf(s123,plain,
spl29_45,
inference(rat,[],[s117,s122]) ).
cnf(s124,plain,
spl29_61,
inference(rat,[],[s83,s114,s111,s98,s122]) ).
cnf(s126,plain,
~ spl29_65,
inference(rat,[],[s90,s123]) ).
cnf(s127,plain,
$false,
inference(rat,[],[s115,s122,s126,s124]) ).
thf(f1166,plain,
$false,
inference(avatar_sat_refutation,[],[s127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU463^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.28 % Computer : n015.cluster.edu
% 0.11/0.28 % Model : x86_64 x86_64
% 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.28 % Memory : 8046.5625MB
% 0.11/0.28 % OS : Linux 6.8.0-71-generic
% 0.11/0.28 % CPULimit : 300
% 0.11/0.28 % WCLimit : 300
% 0.11/0.28 % DateTime : Tue Sep 29 13:45:18 UTC 2026
% 0.11/0.29 % CPUTime :
% 0.11/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.34 Running higher-order theorem proving
% 0.28/0.37 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.97/0.52 % (3546196)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.97/0.52 % (3546201)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=377818545:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.97/0.52 % (3546207)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.97/0.52 % (3546207)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.97/0.52 % (3546202)lrs+10_16_si=on:nwc=1.5:random_seed=1061187394:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.97/0.52 % (3546203)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3964864128:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.97/0.52 % (3546205)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2188163991:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.97/0.52 % (3546204)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=1816993240: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.97/0.52 % (3546206)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=154127980:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.97/0.52 % (3546207)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=1978403402:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.97/0.52 % (3546203)Instruction limit reached!
% 0.97/0.52 % (3546203)------------------------------
% 0.97/0.52 % (3546203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546203)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546203)Termination reason: Instruction limit
% 0.97/0.52 % (3546203)Termination phase: Property scanning
% 0.97/0.52 % (3546203)Time elapsed: 0.003 s
% 0.97/0.52 % (3546203)Peak memory usage: 10 MB
% 0.97/0.52 % (3546203)Instructions burned: 3 (million)
% 0.97/0.52 % (3546202)Instruction limit reached!
% 0.97/0.52 % (3546202)------------------------------
% 0.97/0.52 % (3546202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546202)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546202)Termination reason: Instruction limit
% 0.97/0.52 % (3546202)Termination phase: Saturation
% 0.97/0.52 % (3546202)Time elapsed: 0.018 s
% 0.97/0.52 % (3546202)Peak memory usage: 12 MB
% 0.97/0.52 % (3546202)Instructions burned: 21 (million)
% 0.97/0.52 % (3546201)Instruction limit reached!
% 0.97/0.52 % (3546201)------------------------------
% 0.97/0.52 % (3546201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546201)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546201)Termination reason: Instruction limit
% 0.97/0.52 % (3546201)Termination phase: Saturation
% 0.97/0.52 % (3546201)Time elapsed: 0.037 s
% 0.97/0.52 % (3546201)Peak memory usage: 12 MB
% 0.97/0.52 % (3546201)Instructions burned: 89 (million)
% 0.97/0.52 % (3546205)Instruction limit reached!
% 0.97/0.52 % (3546205)------------------------------
% 0.97/0.52 % (3546205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546205)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546205)Termination reason: Instruction limit
% 0.97/0.52 % (3546205)Termination phase: Saturation
% 0.97/0.52 % (3546205)Time elapsed: 0.023 s
% 0.97/0.52 % (3546205)Peak memory usage: 12 MB
% 0.97/0.52 % (3546205)Instructions burned: 24 (million)
% 0.97/0.52 % (3546215)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2189712020:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.97/0.52 % (3546215)Instruction limit reached!
% 0.97/0.52 % (3546215)------------------------------
% 0.97/0.52 % (3546215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546215)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546215)Termination reason: Instruction limit
% 0.97/0.52 % (3546215)Termination phase: Property scanning
% 0.97/0.52 % (3546215)Time elapsed: 0.003 s
% 0.97/0.52 % (3546215)Peak memory usage: 10 MB
% 0.97/0.52 % (3546215)Instructions burned: 3 (million)
% 0.97/0.52 % (3546217)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.97/0.52 % (3546217)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1922468620:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.97/0.52 % (3546217)Instruction limit reached!
% 0.97/0.52 % (3546217)------------------------------
% 0.97/0.52 % (3546217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546217)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546217)Termination reason: Instruction limit
% 0.97/0.52 % (3546217)Termination phase: Function definition elimination
% 0.97/0.52 % (3546217)Time elapsed: 0.004 s
% 0.97/0.52 % (3546217)Peak memory usage: 10 MB
% 0.97/0.52 % (3546217)Instructions burned: 9 (million)
% 0.97/0.52 % (3546216)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3389490570:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.97/0.52 % (3546216)Instruction limit reached!
% 0.97/0.52 % (3546216)------------------------------
% 0.97/0.52 % (3546216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546216)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546216)Termination reason: Instruction limit
% 0.97/0.52 % (3546216)Termination phase: Property scanning
% 0.97/0.52 % (3546216)Time elapsed: 0.005 s
% 0.97/0.52 % (3546216)Peak memory usage: 10 MB
% 0.97/0.52 % (3546216)Instructions burned: 5 (million)
% 0.97/0.52 % (3546218)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1580633441:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.97/0.52 % (3546222)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2681357421:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 0.97/0.52 % (3546206)Instruction limit reached!
% 0.97/0.52 % (3546206)------------------------------
% 0.97/0.52 % (3546206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546206)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546206)Termination reason: Instruction limit
% 0.97/0.52 % (3546206)Termination phase: Saturation
% 0.97/0.52 % (3546206)Time elapsed: 0.062 s
% 0.97/0.52 % (3546206)Peak memory usage: 13 MB
% 0.97/0.52 % (3546206)Instructions burned: 76 (million)
% 0.97/0.52 % (3546220)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.97/0.52 % (3546220)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.97/0.52 % (3546207) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3546196-3546207"...
% 0.97/0.52 % (3546220)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3330180206: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.97/0.52 % (3546218)Instruction limit reached!
% 0.97/0.52 % (3546218)------------------------------
% 0.97/0.52 % (3546218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.52 % (3546218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.52 % (3546218)CaDiCaL version: 2.1.3
% 0.97/0.52 % (3546218)Termination reason: Instruction limit
% 0.97/0.52 % (3546218)Termination phase: Saturation
% 0.97/0.52 % (3546218)Time elapsed: 0.013 s
% 0.97/0.52 % (3546218)Peak memory usage: 12 MB
% 0.97/0.52 % (3546218)Instructions burned: 14 (million)
% 0.97/0.52 % (3546222) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3546196-3546222"...
% 0.97/0.52 % (3546207)...printing done.
% 0.97/0.52 % (3546222)...printing done.
% 0.97/0.52 % (3546207)Refutation found. Thanks to Tanya!
% 0.97/0.52 % SZS status Theorem for theBenchmark
% 0.97/0.52 % SZS output start Proof for theBenchmark
% See solution above
% 0.97/0.53 % (3546207)------------------------------
% 0.97/0.53 % (3546207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.53 % (3546207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.53 % (3546207)CaDiCaL version: 2.1.3
% 0.97/0.53 % (3546207)Termination reason: Refutation
% 0.97/0.53 % (3546207)Time elapsed: 0.081 s
% 0.97/0.53 % (3546207)Peak memory usage: 13 MB
% 0.97/0.53 % (3546207)Instructions burned: 89 (million)
% 0.97/0.53 % (3546196)Success in time 0.143 s
% 0.97/0.53 % Vampire exiting
%------------------------------------------------------------------------------