%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL602^1 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:15:02 AM UTC 2026
% Result : Theorem 103.36s 17.32s
% Output : Refutation 103.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 33
% Syntax : Number of formulae : 355 ( 34 unt; 0 typ; 25 def)
% Number of atoms : 4058 ( 752 equ; 0 cnn)
% Maximal formula atoms : 10 ( 11 avg)
% Number of connectives : 4399 ( 368 ~; 936 |; 99 &;2551 @)
% ( 29 <=>; 229 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 185 ( 185 >; 0 *; 0 +; 0 <<)
% Number of symbols : 139 ( 135 usr; 41 con; 0-7 aty)
% ( 186 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 712 ( 0 sgn 323 !; 7 ?; 712 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_6,type,
individuals: $tType ).
thf(func_def_1,type,
prop_a: $i > $o ).
thf(func_def_2,type,
prop_b: $i > $o ).
thf(func_def_3,type,
prop_c: $i > $o ).
thf(func_def_4,type,
mfalse: $i > $o ).
thf(func_def_5,type,
mtrue: $i > $o ).
thf(func_def_6,type,
mnot: ( $i > $o ) > $i > $o ).
thf(func_def_8,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_9,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_10,type,
mimpl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_11,type,
miff: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_12,type,
mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_13,type,
mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_14,type,
mall: ( individuals > $i > $o ) > $i > $o ).
thf(func_def_15,type,
mexists: ( individuals > $i > $o ) > $i > $o ).
thf(func_def_16,type,
mvalid: ( $i > $o ) > $o ).
thf(func_def_17,type,
msatisfiable: ( $i > $o ) > $o ).
thf(func_def_18,type,
mcountersatisfiable: ( $i > $o ) > $o ).
thf(func_def_19,type,
minvalid: ( $i > $o ) > $o ).
thf(func_def_20,type,
cartesian_product: ( $i > $o ) > ( $i > $o ) > $i > $i > $o ).
thf(func_def_21,type,
pair_rel: $i > $i > $i > $i > $o ).
thf(func_def_22,type,
id_rel: ( $i > $o ) > $i > $i > $o ).
thf(func_def_23,type,
sub_rel: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(func_def_24,type,
is_rel_on: ( $i > $i > $o ) > ( $i > $o ) > ( $i > $o ) > $o ).
thf(func_def_25,type,
restrict_rel_domain: ( $i > $i > $o ) > ( $i > $o ) > $i > $i > $o ).
thf(func_def_26,type,
rel_diagonal: $i > $i > $o ).
thf(func_def_27,type,
rel_composition: ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_28,type,
reflexive: ( $i > $i > $o ) > $o ).
thf(func_def_29,type,
irreflexive: ( $i > $i > $o ) > $o ).
thf(func_def_30,type,
symmetric: ( $i > $i > $o ) > $o ).
thf(func_def_31,type,
transitive: ( $i > $i > $o ) > $o ).
thf(func_def_32,type,
equiv_rel: ( $i > $i > $o ) > $o ).
thf(func_def_33,type,
rel_codomain: ( $i > $i > $o ) > $i > $o ).
thf(func_def_34,type,
rel_domain: ( $i > $i > $o ) > $i > $o ).
thf(func_def_35,type,
rel_inverse: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_36,type,
equiv_classes: ( $i > $i > $o ) > ( $i > $o ) > $o ).
thf(func_def_37,type,
restrict_rel_codomain: ( $i > $i > $o ) > ( $i > $o ) > $i > $i > $o ).
thf(func_def_38,type,
rel_field: ( $i > $i > $o ) > $i > $o ).
thf(func_def_39,type,
well_founded: ( $i > $i > $o ) > $o ).
thf(func_def_40,type,
upwards_well_founded: ( $i > $i > $o ) > $o ).
thf(func_def_43,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_44,type,
vNOT: $o > $o ).
thf(func_def_45,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_46,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_47,type,
vOR: $o > $o > $o ).
thf(func_def_48,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_49,type,
vAND: $o > $o > $o ).
thf(func_def_50,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_51,type,
vIMP: $o > $o > $o ).
thf(func_def_52,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_53,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_54,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_55,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_56,type,
vIFF: $o > $o > $o ).
thf(func_def_57,type,
sK0: $i > $i > $o ).
thf(func_def_58,type,
sK1: $i > $o ).
thf(func_def_59,type,
sK2: ( $i > $o ) > $i > $i ).
thf(func_def_60,type,
sK3: ( $i > $o ) > $i > $i ).
thf(func_def_61,type,
sK4: ( $i > $o ) > $i > $i ).
thf(func_def_62,type,
sK5: ( $i > $o ) > $i > $i ).
thf(func_def_77,type,
sK20: ( $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_78,type,
sK21: ( $i > $o ) > $i ).
thf(func_def_79,type,
sK22: ( $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_80,type,
sK23: ( $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_81,type,
sK24: ( $i > $i ) > ( $i > $o ) > $i ).
thf(func_def_82,type,
sK25: ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i ) > $i > $i ).
thf(func_def_83,type,
sK26: $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_84,type,
sK27: ( $i > $i ) > ( $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > $i > $i ).
thf(func_def_85,type,
sK28: $i > ( $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_86,type,
sK29: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > $i ).
thf(func_def_87,type,
sK30: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > $i ).
thf(func_def_88,type,
sK31: ( $i > $o ) > $i ).
thf(func_def_89,type,
sK32: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > $i ).
thf(func_def_90,type,
sK33: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > $i ).
thf(func_def_91,type,
sK34: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > ( $i > $i ) > $i ).
thf(func_def_92,type,
sK35: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > ( $i > $i ) > $i ).
thf(func_def_93,type,
sK36: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > ( $i > $i ) > $i ).
thf(func_def_94,type,
sK37: ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > $i > ( $i > $i ) > ( $i > $i ) > $i ).
thf(func_def_95,type,
sK38: $i > ( $i > $i ) > ( $i > $i > $o ) > $i ).
thf(func_def_96,type,
sK39: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_97,type,
sK40: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_98,type,
sK41: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_99,type,
sK42: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_100,type,
sK43: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_101,type,
sK44: ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_102,type,
sK45: ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > $i ).
thf(func_def_103,type,
sK46: ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > $i ).
thf(func_def_104,type,
sK47: ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > $i ).
thf(func_def_105,type,
sK48: ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > ( $i > $i ) > $i > ( $i > $i ) > $i ).
thf(func_def_106,type,
sK49: ( $i > $i ) > ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i > $i ).
thf(func_def_107,type,
sK50: ( $i > $i ) > ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i > $i ).
thf(func_def_108,type,
sK51: ( $i > $i ) > ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i > $i ).
thf(func_def_109,type,
sK52: ( $i > $i ) > ( $i > $i ) > ( $i > $i ) > ( $i > $i > $o ) > ( $i > $i ) > $i > $i ).
thf(func_def_110,type,
sK53: $i > ( $i > $i ) > ( $i > $i > $i ) > ( $i > $i ) > ( $i > $i > $i ) > ( $i > $o ) > $i ).
thf(func_def_111,type,
sK54: ( $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_112,type,
sK55: ( $i > $o ) > ( $i > $i ) > $i ).
thf(func_def_125,type,
sK68: $i > $i ).
thf(f3,axiom,
( mnot
= ( ^ [X0: $i > $o,X1: $i] :
~ ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mnot) ).
thf(f4,axiom,
( mor
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
| ( X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mor) ).
thf(f6,axiom,
( mimpl
= ( ^ [X0: $i > $o,X1: $i > $o] : ( mor @ ( mnot @ X0 ) @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mimpl) ).
thf(f8,axiom,
( mbox
= ( ^ [X0: $i > $i > $o,X1: $i > $o,X2: $i] :
! [X3: $i] :
( ( X0 @ X2 @ X3 )
=> ( X1 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mbox) ).
thf(f12,axiom,
( mvalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mvalid) ).
thf(f24,axiom,
( reflexive
= ( ^ [X0: $i > $i > $o] :
! [X1: $i] : ( X0 @ X1 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET008^2.ax',reflexive) ).
thf(f27,axiom,
( transitive
= ( ^ [X0: $i > $i > $o] :
! [X1: $i,X2: $i,X3: $i] :
( ( ( X0 @ X2 @ X3 )
& ( X0 @ X1 @ X2 ) )
=> ( X0 @ X1 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET008^2.ax',transitive) ).
thf(f37,conjecture,
! [X0: $i > $i > $o] :
( ! [X1: $i > $o] :
( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
& ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) ) )
<=> ( ( transitive @ X0 )
& ( reflexive @ X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm) ).
thf(f38,negated_conjecture,
~ ! [X0: $i > $i > $o] :
( ! [X1: $i > $o] :
( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
& ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) ) )
<=> ( ( transitive @ X0 )
& ( reflexive @ X0 ) ) ),
inference(negated_conjecture,[status(cth)],[f37]) ).
thf(f41,plain,
( mnot
= ( ^ [X0: $i > $o,X1: $i] :
~ ( X0 @ X1 ) ) ),
inference(rectify,[],[f3]) ).
thf(f42,plain,
( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) ),
inference(fool_elimination,[],[f41]) ).
thf(f43,plain,
( mor
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
| ( X0 @ X2 ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f44,plain,
( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
| ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f43]) ).
thf(f47,plain,
( mimpl
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mnot @ Y0 ) @ Y1 ) ) ),
inference(fool_elimination,[],[f6]) ).
thf(f49,plain,
( mbox
= ( ^ [X0: $i > $i > $o,X1: $i > $o,X2: $i] :
! [X3: $i] :
( ( X0 @ X2 @ X3 )
=> ( X1 @ X3 ) ) ) ),
inference(rectify,[],[f8]) ).
thf(f50,plain,
( mbox
= ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) ) ) ),
inference(fool_elimination,[],[f49]) ).
thf(f57,plain,
( mvalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
inference(rectify,[],[f12]) ).
thf(f58,plain,
( mvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f57]) ).
thf(f79,plain,
( reflexive
= ( ^ [X0: $i > $i > $o] :
! [X1: $i] : ( X0 @ X1 @ X1 ) ) ),
inference(rectify,[],[f24]) ).
thf(f80,plain,
( reflexive
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f79]) ).
thf(f85,plain,
( transitive
= ( ^ [X0: $i > $i > $o] :
! [X1: $i,X2: $i,X3: $i] :
( ( ( X0 @ X2 @ X3 )
& ( X0 @ X1 @ X2 ) )
=> ( X0 @ X1 @ X3 ) ) ) ),
inference(rectify,[],[f27]) ).
thf(f86,plain,
( transitive
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y3 @ Y2 )
& ( Y0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f85]) ).
thf(f104,plain,
~ ! [X0: $i > $i > $o] :
( ! [X1: $i > $o] :
( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
& ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) ) )
<=> ( ( transitive @ X0 )
& ( reflexive @ X0 ) ) ),
inference(rectify,[],[f38]) ).
thf(f105,plain,
~ ! [X0: $i > $i > $o] :
( ! [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
= $true )
& ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
= $true ) )
<=> ( ( ( transitive @ X0 )
= $true )
& ( ( reflexive @ X0 )
= $true ) ) ),
inference(fool_elimination,[],[f104]) ).
thf(f106,plain,
? [X0: $i > $i > $o] :
( ! [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
= $true )
& ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
= $true ) )
<~> ( ( ( transitive @ X0 )
= $true )
& ( ( reflexive @ X0 )
= $true ) ) ),
inference(ennf_transformation,[],[f105]) ).
thf(f107,plain,
? [X0: $i > $i > $o] :
( ( ( ( transitive @ X0 )
!= $true )
| ( ( reflexive @ X0 )
!= $true )
| ? [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
!= $true )
| ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
!= $true ) ) )
& ( ( ( ( transitive @ X0 )
= $true )
& ( ( reflexive @ X0 )
= $true ) )
| ! [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
= $true )
& ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
= $true ) ) ) ),
inference(nnf_transformation,[],[f106]) ).
thf(f108,plain,
? [X0: $i > $i > $o] :
( ( ( ( transitive @ X0 )
!= $true )
| ( ( reflexive @ X0 )
!= $true )
| ? [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
!= $true )
| ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
!= $true ) ) )
& ( ( ( ( transitive @ X0 )
= $true )
& ( ( reflexive @ X0 )
= $true ) )
| ! [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
= $true )
& ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
= $true ) ) ) ),
inference(flattening,[],[f107]) ).
thf(f109,plain,
? [X0: $i > $i > $o] :
( ( ( ( transitive @ X0 )
!= $true )
| ( ( reflexive @ X0 )
!= $true )
| ? [X1: $i > $o] :
( ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ X1 ) )
!= $true )
| ( ( mvalid @ ( mimpl @ ( mbox @ X0 @ X1 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X1 ) ) ) )
!= $true ) ) )
& ( ( ( ( transitive @ X0 )
= $true )
& ( ( reflexive @ X0 )
= $true ) )
| ! [X2: $i > $o] :
( ( $true
= ( mvalid @ ( mimpl @ ( mbox @ X0 @ X2 ) @ X2 ) ) )
& ( $true
= ( mvalid @ ( mimpl @ ( mbox @ X0 @ X2 ) @ ( mbox @ X0 @ ( mbox @ X0 @ X2 ) ) ) ) ) ) ) ),
inference(rectify,[],[f108]) ).
thf(f110,plain,
( ( ( $true
!= ( transitive @ sK0 ) )
| ( $true
!= ( reflexive @ sK0 ) )
| ( $true
!= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ sK1 ) @ sK1 ) ) )
| ( $true
!= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ sK1 ) @ ( mbox @ sK0 @ ( mbox @ sK0 @ sK1 ) ) ) ) ) )
& ( ( ( $true
= ( transitive @ sK0 ) )
& ( $true
= ( reflexive @ sK0 ) ) )
| ! [X2: $i > $o] :
( ( $true
= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ X2 ) @ X2 ) ) )
& ( $true
= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ X2 ) @ ( mbox @ sK0 @ ( mbox @ sK0 @ X2 ) ) ) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f109]) ).
thf(f113,plain,
( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) ),
inference(cnf_transformation,[],[f42]) ).
thf(f114,plain,
( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
| ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f44]) ).
thf(f116,plain,
( mimpl
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mnot @ Y0 ) @ Y1 ) ) ),
inference(cnf_transformation,[],[f47]) ).
thf(f118,plain,
( mbox
= ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) ) ) ),
inference(cnf_transformation,[],[f50]) ).
thf(f122,plain,
( mvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f58]) ).
thf(f134,plain,
( reflexive
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f80]) ).
thf(f137,plain,
( transitive
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y3 @ Y2 )
& ( Y0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f86]) ).
thf(f148,plain,
! [X2: $i > $o] :
( ( $true
= ( reflexive @ sK0 ) )
| ( $true
= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ X2 ) @ X2 ) ) ) ),
inference(cnf_transformation,[],[f110]) ).
thf(f149,plain,
! [X2: $i > $o] :
( ( $true
= ( transitive @ sK0 ) )
| ( $true
= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ X2 ) @ ( mbox @ sK0 @ ( mbox @ sK0 @ X2 ) ) ) ) ) ),
inference(cnf_transformation,[],[f110]) ).
thf(f151,plain,
( ( $true
!= ( transitive @ sK0 ) )
| ( $true
!= ( reflexive @ sK0 ) )
| ( $true
!= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ sK1 ) @ sK1 ) ) )
| ( $true
!= ( mvalid @ ( mimpl @ ( mbox @ sK0 @ sK1 ) @ ( mbox @ sK0 @ ( mbox @ sK0 @ sK1 ) ) ) ) ) ),
inference(cnf_transformation,[],[f110]) ).
thf(f154,plain,
( mimpl
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 ) ) ),
inference(definition_unfolding,[],[f116,f114,f113]) ).
thf(f158,plain,
( ( $true
!= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y3 @ Y2 )
& ( Y0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) )
@ sK0 ) )
| ( $true
!= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 @ Y1 ) )
@ sK0 ) )
| ( $true
!= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ sK1 )
@ sK1 ) ) )
| ( $true
!= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ sK1 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ sK1 ) ) ) ) ) ),
inference(definition_unfolding,[],[f151,f137,f134,f122,f154,f118,f122,f154,f118,f118,f118]) ).
thf(f160,plain,
! [X2: $i > $o] :
( ( $true
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( ( Y0 @ Y3 @ Y2 )
& ( Y0 @ Y2 @ Y1 ) )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) )
@ sK0 ) )
| ( $true
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ X2 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ X2 ) ) ) ) ) ),
inference(definition_unfolding,[],[f149,f137,f122,f154,f118,f118,f118]) ).
thf(f161,plain,
! [X2: $i > $o] :
( ( $true
= ( ^ [Y0: $i > $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 @ Y1 ) )
@ sK0 ) )
| ( $true
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ sK0
@ X2 )
@ X2 ) ) ) ),
inference(definition_unfolding,[],[f148,f134,f122,f154,f118]) ).
thf(f181,plain,
! [X2: $i > $o] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( X2 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f161]) ).
thf(f182,plain,
! [X2: $i > $o,X3: $i] :
( ( $true
= ( ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 )
@ X3 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( X2 @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f181]) ).
thf(f183,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( X2 @ Y0 ) )
@ X4 ) ) ),
inference(pi_proxy_clausification,[],[f182]) ).
thf(f184,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) )
| ( X2 @ X4 ) ) ) ),
inference(beta-eta_normalization,[],[f183]) ).
thf(f185,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f184]) ).
thf(f186,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f185]) ).
thf(f187,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) )
@ ( sK3 @ X2 @ X4 ) ) ) ),
inference(sigma_proxy_clausification,[],[f186]) ).
thf(f188,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $false
= ( ( sK0 @ X4 @ ( sK3 @ X2 @ X4 ) )
=> ( X2 @ ( sK3 @ X2 @ X4 ) ) ) ) ),
inference(beta-eta_normalization,[],[f187]) ).
thf(f189,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $false
= ( X2 @ ( sK3 @ X2 @ X4 ) ) ) ),
inference(imp_proxy_clausification,[],[f188]) ).
thf(f190,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( sK0 @ X3 @ X3 ) )
| ( ( X2 @ X4 )
= $true )
| ( $true
= ( sK0 @ X4 @ ( sK3 @ X2 @ X4 ) ) ) ),
inference(imp_proxy_clausification,[],[f188]) ).
thf(f191,plain,
! [X2: $i > $o] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( X2 @ Y2 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f160]) ).
thf(f192,plain,
! [X2: $i > $o,X3: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ X3 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( X2 @ Y2 ) ) ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f191]) ).
thf(f193,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( X2 @ Y2 ) ) ) ) ) )
@ X4 ) ) ),
inference(pi_proxy_clausification,[],[f192]) ).
thf(f194,plain,
! [X2: $i > $o,X3: $i,X4: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) ) ) )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f193]) ).
thf(f195,plain,
! [X2: $i > $o,X3: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) )
@ X5 ) )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f194]) ).
thf(f196,plain,
! [X2: $i > $o,X3: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) )
@ X5 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) ) ) )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f195]) ).
thf(f197,plain,
! [X2: $i > $o,X3: $i,X6: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) )
@ X6 ) )
| ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f196]) ).
thf(f198,plain,
! [X2: $i > $o,X3: $i,X6: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) )
@ X6 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f197]) ).
thf(f199,plain,
! [X2: $i > $o,X3: $i,X6: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ X3 ) )
=> ( sK0 @ Y1 @ X3 ) ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( X2 @ Y1 ) ) ) )
@ X6 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ X4 @ Y0 )
=> ( X2 @ Y0 ) )
@ ( sK4 @ X2 @ X4 ) ) ) ),
inference(sigma_proxy_clausification,[],[f198]) ).
thf(f200,plain,
! [X2: $i > $o,X3: $i,X6: $i,X4: $i,X5: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) ) ) )
| ( $true
= ( ( sK0 @ X4 @ X6 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) )
| ( $false
= ( ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) )
=> ( X2 @ ( sK4 @ X2 @ X4 ) ) ) ) ),
inference(beta-eta_normalization,[],[f199]) ).
thf(f201,plain,
! [X2: $i > $o,X3: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $true
= ( ( sK0 @ X4 @ X6 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) )
| ( $false
= ( ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) )
=> ( X2 @ ( sK4 @ X2 @ X4 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f200]) ).
thf(f202,plain,
! [X2: $i > $o,X3: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) )
=> ( X2 @ ( sK4 @ X2 @ X4 ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f201]) ).
thf(f203,plain,
! [X2: $i > $o,X3: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f202]) ).
thf(f204,plain,
! [X2: $i > $o,X3: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f202]) ).
thf(f205,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) )
@ X8 ) ) ),
inference(pi_proxy_clausification,[],[f204]) ).
thf(f206,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ( ( sK0 @ X7 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ X7 @ X3 ) ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) ) ),
inference(beta-eta_normalization,[],[f205]) ).
thf(f207,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( ( sK0 @ X7 @ X5 )
& ( sK0 @ X5 @ X3 ) ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) )
| ( $true
= ( sK0 @ X7 @ X3 ) ) ),
inference(imp_proxy_clausification,[],[f206]) ).
thf(f208,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) )
| ( $true
= ( sK0 @ X7 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) ) ),
inference(and_proxy_clausification,[],[f207]) ).
thf(f209,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $true
= ( sK0 @ X7 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) )
| ( $true
= ( X2 @ X8 ) ) ),
inference(imp_proxy_clausification,[],[f208]) ).
thf(f210,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ Y0 @ X3 ) )
@ X7 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ X6 @ Y0 )
=> ( X2 @ Y0 ) )
@ X8 ) ) ),
inference(pi_proxy_clausification,[],[f203]) ).
thf(f211,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $true
= ( ( ( sK0 @ X7 @ X5 )
& ( sK0 @ X5 @ X3 ) )
=> ( sK0 @ X7 @ X3 ) ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) ) ),
inference(beta-eta_normalization,[],[f210]) ).
thf(f212,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( ( sK0 @ X7 @ X5 )
& ( sK0 @ X5 @ X3 ) ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) )
| ( $true
= ( sK0 @ X7 @ X3 ) ) ),
inference(imp_proxy_clausification,[],[f211]) ).
thf(f213,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $true
= ( ( sK0 @ X6 @ X8 )
=> ( X2 @ X8 ) ) )
| ( $true
= ( sK0 @ X7 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) ) ),
inference(and_proxy_clausification,[],[f212]) ).
thf(f214,plain,
! [X2: $i > $o,X3: $i,X8: $i,X6: $i,X7: $i,X4: $i,X5: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $true
= ( sK0 @ X7 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) )
| ( $true
= ( X2 @ X8 ) ) ),
inference(imp_proxy_clausification,[],[f213]) ).
thf(f233,plain,
( ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( sK1 @ Y0 ) ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( sK1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f158]) ).
thf(f234,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ sK6 ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( sK1 @ Y0 ) ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( sK1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f233]) ).
thf(f235,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ sK6 ) )
| ( $false
= ( ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 )
@ sK7 ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( sK1 @ Y0 ) ) ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( sK1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f234]) ).
thf(f236,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ sK6 ) )
| ( $false
= ( ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 )
@ sK7 ) )
| ( $false
= ( ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( sK1 @ Y0 ) )
@ sK8 ) )
| ( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( sK1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f235]) ).
thf(f237,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( ( sK0 @ Y2 @ Y1 )
& ( sK0 @ Y1 @ Y0 ) )
=> ( sK0 @ Y2 @ Y0 ) ) ) )
@ sK6 ) )
| ( $false
= ( ^ [Y0: $i] : ( sK0 @ Y0 @ Y0 )
@ sK7 ) )
| ( $false
= ( ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( sK1 @ Y0 ) )
@ sK8 ) )
| ( $false
= ( ^ [Y0: $i] :
( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( sK0 @ Y1 @ Y2 )
=> ( sK1 @ Y2 ) ) ) ) ) )
@ sK9 ) ) ),
inference(sigma_proxy_clausification,[],[f236]) ).
thf(f238,plain,
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( sK1 @ sK8 ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f237]) ).
thf(f239,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( sK1 @ sK8 ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f238]) ).
thf(f240,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f239]) ).
thf(f241,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f239]) ).
thf(f242,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f241]) ).
thf(f243,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f242]) ).
thf(f244,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f243]) ).
thf(f245,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f243]) ).
thf(f246,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f245]) ).
thf(f247,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f246]) ).
thf(f248,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ( sK0 @ sK8 @ X1 )
=> ( sK1 @ X1 ) ) )
| ( $true
= ( ( sK0 @ sK9 @ X2 )
=> ( sK1 @ X2 ) ) ) ),
inference(beta-eta_normalization,[],[f247]) ).
thf(f249,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK11 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ( sK0 @ sK8 @ X1 )
=> ( sK1 @ X1 ) ) )
| ( $true
= ( ( sK0 @ sK9 @ X2 )
=> ( sK1 @ X2 ) ) ) ),
inference(sigma_proxy_clausification,[],[f248]) ).
thf(f250,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK11 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( ( sK0 @ sK9 @ X2 )
=> ( sK1 @ X2 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f249]) ).
thf(f251,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK11 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f250]) ).
thf(f252,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( ( ( sK0 @ sK11 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK11 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(beta-eta_normalization,[],[f251]) ).
thf(f253,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( sK0 @ sK11 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f252]) ).
thf(f254,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ( sK0 @ sK11 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f252]) ).
thf(f255,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(and_proxy_clausification,[],[f254]) ).
thf(f256,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( sK0 @ sK11 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X1 ) )
| ( $true
= ( sK1 @ X2 ) ) ),
inference(and_proxy_clausification,[],[f254]) ).
thf(f257,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK8 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) )
@ sK12 ) ) ),
inference(sigma_proxy_clausification,[],[f244]) ).
thf(f258,plain,
! [X1: $i] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ( sK0 @ sK8 @ X1 )
=> ( sK1 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK9 @ sK12 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK12 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f257]) ).
thf(f259,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK13 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $true
= ( ( sK0 @ sK8 @ X1 )
=> ( sK1 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK9 @ sK12 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK12 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f258]) ).
thf(f260,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK13 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK9 @ sK12 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK12 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f259]) ).
thf(f261,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK13 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK12 @ Y0 )
=> ( sK1 @ Y0 ) ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f260]) ).
thf(f262,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK13 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f260]) ).
thf(f263,plain,
! [X1: $i] :
( ( $false
= ( ( ( sK0 @ sK13 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK13 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(beta-eta_normalization,[],[f262]) ).
thf(f264,plain,
! [X1: $i] :
( ( $false
= ( sK0 @ sK13 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f263]) ).
thf(f265,plain,
! [X1: $i] :
( ( $true
= ( ( sK0 @ sK13 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f263]) ).
thf(f266,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f265]) ).
thf(f267,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK13 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f265]) ).
thf(f268,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK13 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ sK12 @ Y0 )
=> ( sK1 @ Y0 ) )
@ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(sigma_proxy_clausification,[],[f261]) ).
thf(f269,plain,
! [X1: $i] :
( ( $false
= ( ( ( sK0 @ sK13 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK13 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK12 @ sK14 )
=> ( sK1 @ sK14 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(beta-eta_normalization,[],[f268]) ).
thf(f270,plain,
! [X1: $i] :
( ( $false
= ( sK0 @ sK13 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK12 @ sK14 )
=> ( sK1 @ sK14 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f269]) ).
thf(f271,plain,
! [X1: $i] :
( ( $true
= ( ( sK0 @ sK13 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK12 @ sK14 )
=> ( sK1 @ sK14 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f269]) ).
thf(f272,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK12 @ sK14 )
=> ( sK1 @ sK14 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f271]) ).
thf(f273,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK13 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( ( sK0 @ sK12 @ sK14 )
=> ( sK1 @ sK14 ) ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f271]) ).
thf(f274,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK13 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK1 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f273]) ).
thf(f275,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK13 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK12 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f273]) ).
thf(f276,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK1 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f272]) ).
thf(f277,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK12 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f272]) ).
thf(f278,plain,
! [X1: $i] :
( ( $false
= ( sK0 @ sK13 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $false
= ( sK1 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f270]) ).
thf(f279,plain,
! [X1: $i] :
( ( $false
= ( sK0 @ sK13 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK0 @ sK12 @ sK14 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f270]) ).
thf(f280,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f240]) ).
thf(f281,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f240]) ).
thf(f282,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f281]) ).
thf(f283,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( sK1 @ Y0 ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f282]) ).
thf(f284,plain,
! [X1: $i] :
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( ( sK0 @ sK9 @ X1 )
=> ( sK1 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f283]) ).
thf(f285,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK15 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( ( sK0 @ sK9 @ X1 )
=> ( sK1 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f284]) ).
thf(f286,plain,
! [X1: $i] :
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK15 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f285]) ).
thf(f287,plain,
! [X1: $i] :
( ( $false
= ( ( ( sK0 @ sK15 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK15 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(beta-eta_normalization,[],[f286]) ).
thf(f288,plain,
! [X1: $i] :
( ( $false
= ( sK0 @ sK15 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f287]) ).
thf(f289,plain,
! [X1: $i] :
( ( $true
= ( ( sK0 @ sK15 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f287]) ).
thf(f290,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f289]) ).
thf(f291,plain,
! [X1: $i] :
( ( $true
= ( sK0 @ sK15 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK0 @ sK9 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f289]) ).
thf(f292,plain,
( ( $false
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ( sK0 @ Y1 @ Y0 )
& ( sK0 @ Y0 @ sK6 ) )
=> ( sK0 @ Y1 @ sK6 ) ) )
@ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ sK9 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( sK0 @ Y0 @ Y1 )
=> ( sK1 @ Y1 ) ) ) )
@ sK16 ) ) ),
inference(sigma_proxy_clausification,[],[f280]) ).
thf(f293,plain,
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK9 @ sK16 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK16 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f292]) ).
thf(f294,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK17 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK9 @ sK16 )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK16 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f293]) ).
thf(f295,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK17 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( sK0 @ sK16 @ Y0 )
=> ( sK1 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f294]) ).
thf(f296,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK17 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(imp_proxy_clausification,[],[f294]) ).
thf(f297,plain,
( ( $false
= ( ( ( sK0 @ sK17 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK17 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(beta-eta_normalization,[],[f296]) ).
thf(f298,plain,
( ( $false
= ( sK0 @ sK17 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(imp_proxy_clausification,[],[f297]) ).
thf(f299,plain,
( ( $true
= ( ( sK0 @ sK17 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(imp_proxy_clausification,[],[f297]) ).
thf(f300,plain,
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(and_proxy_clausification,[],[f299]) ).
thf(f301,plain,
( ( $true
= ( sK0 @ sK17 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
inference(and_proxy_clausification,[],[f299]) ).
thf(f302,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( ( sK0 @ Y0 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ Y0 @ sK6 ) )
@ sK17 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( sK0 @ sK16 @ Y0 )
=> ( sK1 @ Y0 ) )
@ sK18 ) ) ),
inference(sigma_proxy_clausification,[],[f295]) ).
thf(f303,plain,
( ( $false
= ( ( ( sK0 @ sK17 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) )
=> ( sK0 @ sK17 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK16 @ sK18 )
=> ( sK1 @ sK18 ) ) ) ),
inference(beta-eta_normalization,[],[f302]) ).
thf(f304,plain,
( ( $false
= ( sK0 @ sK17 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK16 @ sK18 )
=> ( sK1 @ sK18 ) ) ) ),
inference(imp_proxy_clausification,[],[f303]) ).
thf(f305,plain,
( ( $true
= ( ( sK0 @ sK17 @ sK10 )
& ( sK0 @ sK10 @ sK6 ) ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK16 @ sK18 )
=> ( sK1 @ sK18 ) ) ) ),
inference(imp_proxy_clausification,[],[f303]) ).
thf(f306,plain,
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK16 @ sK18 )
=> ( sK1 @ sK18 ) ) ) ),
inference(and_proxy_clausification,[],[f305]) ).
thf(f307,plain,
( ( $true
= ( sK0 @ sK17 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( ( sK0 @ sK16 @ sK18 )
=> ( sK1 @ sK18 ) ) ) ),
inference(and_proxy_clausification,[],[f305]) ).
thf(f308,plain,
( ( $true
= ( sK0 @ sK17 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK1 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f307]) ).
thf(f309,plain,
( ( $true
= ( sK0 @ sK17 @ sK10 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK16 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f307]) ).
thf(f310,plain,
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK1 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f306]) ).
thf(f311,plain,
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK16 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f306]) ).
thf(f312,plain,
( ( $false
= ( sK0 @ sK17 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $false
= ( sK1 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f304]) ).
thf(f313,plain,
( ( $false
= ( sK0 @ sK17 @ sK6 ) )
| ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ( $false
= ( sK1 @ sK8 ) )
| ( $true
= ( sK0 @ sK16 @ sK18 ) ) ),
inference(imp_proxy_clausification,[],[f304]) ).
thf(f318,definition,
( spl19_2
<=> ! [X3: $i] :
( $true
= ( sK0 @ X3 @ X3 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition]) ).
thf(f319,plain,
( ! [X3: $i] :
( $true
= ( sK0 @ X3 @ X3 ) )
| ~ spl19_2 ),
inference(avatar_component_clause,[],[f318]) ).
thf(f326,definition,
( spl19_4
<=> ! [X4: $i,X2: $i > $o] :
( ( ( X2 @ X4 )
= $true )
| ( $true
= ( sK0 @ X4 @ ( sK3 @ X2 @ X4 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition]) ).
thf(f327,plain,
( ! [X2: $i > $o,X4: $i] :
( ( $true
= ( sK0 @ X4 @ ( sK3 @ X2 @ X4 ) ) )
| ( ( X2 @ X4 )
= $true ) )
| ~ spl19_4 ),
inference(avatar_component_clause,[],[f326]) ).
thf(f328,plain,
( spl19_4
| spl19_2 ),
inference(avatar_split_clause,[],[f190,f318,f326]) ).
thf(f330,definition,
( spl19_5
<=> ! [X4: $i,X2: $i > $o] :
( ( ( X2 @ X4 )
= $true )
| ( $false
= ( X2 @ ( sK3 @ X2 @ X4 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition]) ).
thf(f331,plain,
( ! [X2: $i > $o,X4: $i] :
( ( $false
= ( X2 @ ( sK3 @ X2 @ X4 ) ) )
| ( ( X2 @ X4 )
= $true ) )
| ~ spl19_5 ),
inference(avatar_component_clause,[],[f330]) ).
thf(f332,plain,
( spl19_5
| spl19_2 ),
inference(avatar_split_clause,[],[f189,f318,f330]) ).
thf(f334,definition,
( spl19_6
<=> ! [X4: $i,X8: $i,X6: $i,X2: $i > $o] :
( ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( X2 @ X8 ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition]) ).
thf(f335,plain,
( ! [X2: $i > $o,X8: $i,X6: $i,X4: $i] :
( ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( X2 @ X8 ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $true
= ( sK0 @ X4 @ ( sK4 @ X2 @ X4 ) ) ) )
| ~ spl19_6 ),
inference(avatar_component_clause,[],[f334]) ).
thf(f337,definition,
( spl19_7
<=> ! [X5: $i,X7: $i,X3: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) )
| ( $true
= ( sK0 @ X7 @ X3 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
thf(f338,plain,
( ! [X3: $i,X7: $i,X5: $i] :
( ( $false
= ( sK0 @ X5 @ X3 ) )
| ( $false
= ( sK0 @ X7 @ X5 ) )
| ( $true
= ( sK0 @ X7 @ X3 ) ) )
| ~ spl19_7 ),
inference(avatar_component_clause,[],[f337]) ).
thf(f339,plain,
( spl19_6
| spl19_7 ),
inference(avatar_split_clause,[],[f209,f337,f334]) ).
thf(f341,definition,
( spl19_8
<=> ! [X4: $i,X8: $i,X6: $i,X2: $i > $o] :
( ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( X2 @ X8 ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
thf(f342,plain,
( ! [X2: $i > $o,X8: $i,X6: $i,X4: $i] :
( ( $false
= ( sK0 @ X4 @ X6 ) )
| ( $true
= ( X2 @ X8 ) )
| ( $false
= ( sK0 @ X6 @ X8 ) )
| ( $false
= ( X2 @ ( sK4 @ X2 @ X4 ) ) ) )
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f341]) ).
thf(f343,plain,
( spl19_8
| spl19_7 ),
inference(avatar_split_clause,[],[f214,f337,f341]) ).
thf(f353,definition,
( spl19_11
<=> ! [X2: $i] :
( ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
thf(f354,plain,
( ! [X2: $i] :
( ( $false
= ( sK0 @ sK9 @ X2 ) )
| ( $true
= ( sK1 @ X2 ) ) )
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f353]) ).
thf(f356,definition,
( spl19_12
<=> ! [X1: $i] :
( ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition]) ).
thf(f357,plain,
( ! [X1: $i] :
( ( $false
= ( sK0 @ sK8 @ X1 ) )
| ( $true
= ( sK1 @ X1 ) ) )
| ~ spl19_12 ),
inference(avatar_component_clause,[],[f356]) ).
thf(f359,definition,
( spl19_13
<=> ( $false
= ( sK0 @ sK7 @ sK7 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition]) ).
thf(f361,plain,
( ( $false
= ( sK0 @ sK7 @ sK7 ) )
| ~ spl19_13 ),
inference(avatar_component_clause,[],[f359]) ).
thf(f363,definition,
( spl19_14
<=> ( $true
= ( sK0 @ sK11 @ sK10 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition]) ).
thf(f365,plain,
( ( $true
= ( sK0 @ sK11 @ sK10 ) )
| ~ spl19_14 ),
inference(avatar_component_clause,[],[f363]) ).
thf(f366,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_14 ),
inference(avatar_split_clause,[],[f256,f363,f359,f356,f353]) ).
thf(f368,definition,
( spl19_15
<=> ( $true
= ( sK0 @ sK10 @ sK6 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition]) ).
thf(f370,plain,
( ( $true
= ( sK0 @ sK10 @ sK6 ) )
| ~ spl19_15 ),
inference(avatar_component_clause,[],[f368]) ).
thf(f371,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f255,f368,f359,f356,f353]) ).
thf(f373,definition,
( spl19_16
<=> ( $false
= ( sK0 @ sK11 @ sK6 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition]) ).
thf(f375,plain,
( ( $false
= ( sK0 @ sK11 @ sK6 ) )
| ~ spl19_16 ),
inference(avatar_component_clause,[],[f373]) ).
thf(f376,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_16 ),
inference(avatar_split_clause,[],[f253,f373,f359,f356,f353]) ).
thf(f378,definition,
( spl19_17
<=> ( $true
= ( sK0 @ sK9 @ sK12 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition]) ).
thf(f380,plain,
( ( $true
= ( sK0 @ sK9 @ sK12 ) )
| ~ spl19_17 ),
inference(avatar_component_clause,[],[f378]) ).
thf(f382,definition,
( spl19_18
<=> ( $true
= ( sK0 @ sK13 @ sK10 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
thf(f384,plain,
( ( $true
= ( sK0 @ sK13 @ sK10 ) )
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f382]) ).
thf(f385,plain,
( spl19_17
| spl19_12
| spl19_13
| spl19_18 ),
inference(avatar_split_clause,[],[f267,f382,f359,f356,f378]) ).
thf(f386,plain,
( spl19_17
| spl19_12
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f266,f368,f359,f356,f378]) ).
thf(f388,definition,
( spl19_19
<=> ( $false
= ( sK0 @ sK13 @ sK6 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition]) ).
thf(f390,plain,
( ( $false
= ( sK0 @ sK13 @ sK6 ) )
| ~ spl19_19 ),
inference(avatar_component_clause,[],[f388]) ).
thf(f391,plain,
( spl19_17
| spl19_12
| spl19_13
| spl19_19 ),
inference(avatar_split_clause,[],[f264,f388,f359,f356,f378]) ).
thf(f393,definition,
( spl19_20
<=> ( $true
= ( sK0 @ sK12 @ sK14 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
thf(f395,plain,
( ( $true
= ( sK0 @ sK12 @ sK14 ) )
| ~ spl19_20 ),
inference(avatar_component_clause,[],[f393]) ).
thf(f396,plain,
( spl19_20
| spl19_12
| spl19_13
| spl19_18 ),
inference(avatar_split_clause,[],[f275,f382,f359,f356,f393]) ).
thf(f398,definition,
( spl19_21
<=> ( $false
= ( sK1 @ sK14 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
thf(f400,plain,
( ( $false
= ( sK1 @ sK14 ) )
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f398]) ).
thf(f401,plain,
( spl19_21
| spl19_12
| spl19_13
| spl19_18 ),
inference(avatar_split_clause,[],[f274,f382,f359,f356,f398]) ).
thf(f402,plain,
( spl19_20
| spl19_12
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f277,f368,f359,f356,f393]) ).
thf(f403,plain,
( spl19_21
| spl19_12
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f276,f368,f359,f356,f398]) ).
thf(f404,plain,
( spl19_20
| spl19_12
| spl19_13
| spl19_19 ),
inference(avatar_split_clause,[],[f279,f388,f359,f356,f393]) ).
thf(f405,plain,
( spl19_21
| spl19_12
| spl19_13
| spl19_19 ),
inference(avatar_split_clause,[],[f278,f388,f359,f356,f398]) ).
thf(f407,definition,
( spl19_22
<=> ( $false
= ( sK1 @ sK8 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition]) ).
thf(f409,plain,
( ( $false
= ( sK1 @ sK8 ) )
| ~ spl19_22 ),
inference(avatar_component_clause,[],[f407]) ).
thf(f411,definition,
( spl19_23
<=> ( $true
= ( sK0 @ sK15 @ sK10 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
thf(f413,plain,
( ( $true
= ( sK0 @ sK15 @ sK10 ) )
| ~ spl19_23 ),
inference(avatar_component_clause,[],[f411]) ).
thf(f414,plain,
( spl19_11
| spl19_22
| spl19_13
| spl19_23 ),
inference(avatar_split_clause,[],[f291,f411,f359,f407,f353]) ).
thf(f415,plain,
( spl19_11
| spl19_22
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f290,f368,f359,f407,f353]) ).
thf(f417,definition,
( spl19_24
<=> ( $false
= ( sK0 @ sK15 @ sK6 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition]) ).
thf(f419,plain,
( ( $false
= ( sK0 @ sK15 @ sK6 ) )
| ~ spl19_24 ),
inference(avatar_component_clause,[],[f417]) ).
thf(f420,plain,
( spl19_11
| spl19_22
| spl19_13
| spl19_24 ),
inference(avatar_split_clause,[],[f288,f417,f359,f407,f353]) ).
thf(f422,definition,
( spl19_25
<=> ( $true
= ( sK0 @ sK9 @ sK16 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition]) ).
thf(f424,plain,
( ( $true
= ( sK0 @ sK9 @ sK16 ) )
| ~ spl19_25 ),
inference(avatar_component_clause,[],[f422]) ).
thf(f426,definition,
( spl19_26
<=> ( $true
= ( sK0 @ sK17 @ sK10 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition]) ).
thf(f428,plain,
( ( $true
= ( sK0 @ sK17 @ sK10 ) )
| ~ spl19_26 ),
inference(avatar_component_clause,[],[f426]) ).
thf(f429,plain,
( spl19_25
| spl19_22
| spl19_13
| spl19_26 ),
inference(avatar_split_clause,[],[f301,f426,f359,f407,f422]) ).
thf(f430,plain,
( spl19_25
| spl19_22
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f300,f368,f359,f407,f422]) ).
thf(f432,definition,
( spl19_27
<=> ( $false
= ( sK0 @ sK17 @ sK6 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition]) ).
thf(f434,plain,
( ( $false
= ( sK0 @ sK17 @ sK6 ) )
| ~ spl19_27 ),
inference(avatar_component_clause,[],[f432]) ).
thf(f435,plain,
( spl19_25
| spl19_22
| spl19_13
| spl19_27 ),
inference(avatar_split_clause,[],[f298,f432,f359,f407,f422]) ).
thf(f437,definition,
( spl19_28
<=> ( $true
= ( sK0 @ sK16 @ sK18 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition]) ).
thf(f439,plain,
( ( $true
= ( sK0 @ sK16 @ sK18 ) )
| ~ spl19_28 ),
inference(avatar_component_clause,[],[f437]) ).
thf(f440,plain,
( spl19_28
| spl19_22
| spl19_13
| spl19_26 ),
inference(avatar_split_clause,[],[f309,f426,f359,f407,f437]) ).
thf(f442,definition,
( spl19_29
<=> ( $false
= ( sK1 @ sK18 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition]) ).
thf(f444,plain,
( ( $false
= ( sK1 @ sK18 ) )
| ~ spl19_29 ),
inference(avatar_component_clause,[],[f442]) ).
thf(f445,plain,
( spl19_29
| spl19_22
| spl19_13
| spl19_26 ),
inference(avatar_split_clause,[],[f308,f426,f359,f407,f442]) ).
thf(f446,plain,
( spl19_28
| spl19_22
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f311,f368,f359,f407,f437]) ).
thf(f447,plain,
( spl19_29
| spl19_22
| spl19_13
| spl19_15 ),
inference(avatar_split_clause,[],[f310,f368,f359,f407,f442]) ).
thf(f448,plain,
( spl19_28
| spl19_22
| spl19_13
| spl19_27 ),
inference(avatar_split_clause,[],[f313,f432,f359,f407,f437]) ).
thf(f449,plain,
( spl19_29
| spl19_22
| spl19_13
| spl19_27 ),
inference(avatar_split_clause,[],[f312,f432,f359,f407,f442]) ).
thf(f480,plain,
( ( $false = $true )
| ~ spl19_2
| ~ spl19_13 ),
inference(constrained_superposition,[],[f361,f319]) ).
thf(f488,plain,
( $false
| ~ spl19_2
| ~ spl19_13 ),
inference(trivial_inequality_removal,[],[f480]) ).
thf(f489,plain,
( ~ spl19_2
| ~ spl19_13 ),
inference(avatar_contradiction_clause,[],[f488]) ).
thf(f569,plain,
( ( $false = $true )
| ( $true
= ( sK1 @ sK8 ) )
| ~ spl19_2
| ~ spl19_12 ),
inference(constrained_superposition,[],[f357,f319]) ).
thf(f580,plain,
( ( $true
= ( sK1 @ sK8 ) )
| ~ spl19_2
| ~ spl19_12 ),
inference(trivial_inequality_removal,[],[f569]) ).
thf(f585,plain,
( ( $false = $true )
| ~ spl19_2
| ~ spl19_12
| ~ spl19_22 ),
inference(forward_demodulation,[],[f580,f409]) ).
thf(f586,plain,
( $false
| ~ spl19_2
| ~ spl19_12
| ~ spl19_22 ),
inference(trivial_inequality_removal,[],[f585]) ).
thf(f587,plain,
( ~ spl19_2
| ~ spl19_12
| ~ spl19_22 ),
inference(avatar_contradiction_clause,[],[f586]) ).
thf(f593,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $false
= ( sK0 @ X0 @ sK10 ) )
| ( $true
= ( sK0 @ X0 @ sK6 ) ) )
| ~ spl19_7
| ~ spl19_15 ),
inference(constrained_superposition,[],[f338,f370]) ).
thf(f602,plain,
( ! [X0: $i] :
( ( $false
= ( sK0 @ X0 @ sK10 ) )
| ( $true
= ( sK0 @ X0 @ sK6 ) ) )
| ~ spl19_7
| ~ spl19_15 ),
inference(trivial_inequality_removal,[],[f593]) ).
thf(f1126,plain,
( ( $false = $true )
| ( $true
= ( sK0 @ sK13 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_18 ),
inference(constrained_superposition,[],[f602,f384]) ).
thf(f1141,plain,
( ( $true
= ( sK0 @ sK13 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_18 ),
inference(trivial_inequality_removal,[],[f1126]) ).
thf(f1152,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_18
| ~ spl19_19 ),
inference(forward_demodulation,[],[f1141,f390]) ).
thf(f1153,plain,
( $false
| ~ spl19_7
| ~ spl19_15
| ~ spl19_18
| ~ spl19_19 ),
inference(trivial_inequality_removal,[],[f1152]) ).
thf(f1154,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_18
| ~ spl19_19 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
thf(f1230,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( sK4
@ ^ [Y0: $i] : ( Y0 != X0 )
@ X1 )
= X0 )
| ( $false
= ( sK0 @ X1 @ X2 ) )
| ( $false
= ( sK0 @ X2 @ X0 ) ) )
| ~ spl19_8 ),
inference(leibniz_equality_elimination,[],[f342]) ).
thf(f4098,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $false
= ( sK0 @ X0 @ sK12 ) )
| ( $true
= ( sK0 @ X0 @ sK14 ) ) )
| ~ spl19_7
| ~ spl19_20 ),
inference(constrained_superposition,[],[f338,f395]) ).
thf(f4126,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ sK14 ) )
| ( $false
= ( sK0 @ X0 @ sK12 ) ) )
| ~ spl19_7
| ~ spl19_20 ),
inference(trivial_inequality_removal,[],[f4098]) ).
thf(f20784,plain,
( ! [X0: $i] :
( ( sK3
@ ^ [Y0: $i] : ( Y0 != X0 )
@ X0 )
= X0 )
| ~ spl19_5 ),
inference(leibniz_equality_elimination,[],[f331]) ).
thf(f22115,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ X0 ) )
| ( $true
= ( ^ [Y0: $i] : ( Y0 != X0 )
@ X0 ) ) )
| ~ spl19_4
| ~ spl19_5 ),
inference(constrained_superposition,[],[f327,f20784]) ).
thf(f22122,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ X0 ) )
| ( $true
= ( X0 != X0 ) ) )
| ~ spl19_4
| ~ spl19_5 ),
inference(beta-eta_normalization,[],[f22115]) ).
thf(f22123,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ X0 ) )
| ( $false
= ( X0 = X0 ) ) )
| ~ spl19_4
| ~ spl19_5 ),
inference(not_proxy_clausification,[],[f22122]) ).
thf(f22124,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ X0 ) )
| ( X0 != X0 ) )
| ~ spl19_4
| ~ spl19_5 ),
inference(equality_proxy_clausification,[],[f22123]) ).
thf(f22125,plain,
( ! [X0: $i] :
( $true
= ( sK0 @ X0 @ X0 ) )
| ~ spl19_4
| ~ spl19_5 ),
inference(trivial_inequality_removal,[],[f22124]) ).
thf(f22126,plain,
( spl19_2
| ~ spl19_4
| ~ spl19_5 ),
inference(avatar_split_clause,[],[f22125,f330,f326,f318]) ).
thf(f26079,plain,
( ( $false = $true )
| ( $true
= ( sK1 @ sK14 ) )
| ( $false
= ( sK0 @ sK9 @ sK12 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_20 ),
inference(constrained_superposition,[],[f354,f4126]) ).
thf(f26114,plain,
( ( $true
= ( sK1 @ sK14 ) )
| ( $false
= ( sK0 @ sK9 @ sK12 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_20 ),
inference(trivial_inequality_removal,[],[f26079]) ).
thf(f26146,plain,
( ( $false = $true )
| ( $false
= ( sK0 @ sK9 @ sK12 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_20
| ~ spl19_21 ),
inference(forward_demodulation,[],[f26114,f400]) ).
thf(f26147,plain,
( ( $false
= ( sK0 @ sK9 @ sK12 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_20
| ~ spl19_21 ),
inference(trivial_inequality_removal,[],[f26146]) ).
thf(f26835,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21 ),
inference(constrained_superposition,[],[f26147,f380]) ).
thf(f26911,plain,
( $false
| ~ spl19_7
| ~ spl19_11
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21 ),
inference(trivial_inequality_removal,[],[f26835]) ).
thf(f26912,plain,
( ~ spl19_7
| ~ spl19_11
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21 ),
inference(avatar_contradiction_clause,[],[f26911]) ).
thf(f27692,plain,
( ( $false = $true )
| ( $true
= ( sK0 @ sK11 @ sK6 ) )
| ~ spl19_7
| ~ spl19_14
| ~ spl19_15 ),
inference(constrained_superposition,[],[f365,f602]) ).
thf(f27772,plain,
( ( $true
= ( sK0 @ sK11 @ sK6 ) )
| ~ spl19_7
| ~ spl19_14
| ~ spl19_15 ),
inference(trivial_inequality_removal,[],[f27692]) ).
thf(f27781,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_14
| ~ spl19_15
| ~ spl19_16 ),
inference(forward_demodulation,[],[f27772,f375]) ).
thf(f27782,plain,
( $false
| ~ spl19_7
| ~ spl19_14
| ~ spl19_15
| ~ spl19_16 ),
inference(trivial_inequality_removal,[],[f27781]) ).
thf(f27783,plain,
( ~ spl19_7
| ~ spl19_14
| ~ spl19_15
| ~ spl19_16 ),
inference(avatar_contradiction_clause,[],[f27782]) ).
thf(f35517,plain,
( ! [X0: $i] :
( ( $false = $true )
| ( $false
= ( sK0 @ X0 @ sK16 ) )
| ( $true
= ( sK0 @ X0 @ sK18 ) ) )
| ~ spl19_7
| ~ spl19_28 ),
inference(constrained_superposition,[],[f338,f439]) ).
thf(f35528,plain,
( ! [X0: $i] :
( ( $true
= ( sK0 @ X0 @ sK18 ) )
| ( $false
= ( sK0 @ X0 @ sK16 ) ) )
| ~ spl19_7
| ~ spl19_28 ),
inference(trivial_inequality_removal,[],[f35517]) ).
thf(f125242,plain,
( ( $false = $true )
| ( $true
= ( sK1 @ sK18 ) )
| ( $false
= ( sK0 @ sK9 @ sK16 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_28 ),
inference(constrained_superposition,[],[f354,f35528]) ).
thf(f125251,plain,
( ( $true
= ( sK1 @ sK18 ) )
| ( $false
= ( sK0 @ sK9 @ sK16 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_28 ),
inference(trivial_inequality_removal,[],[f125242]) ).
thf(f125633,plain,
( ( $false = $true )
| ( $false
= ( sK0 @ sK9 @ sK16 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_28
| ~ spl19_29 ),
inference(forward_demodulation,[],[f125251,f444]) ).
thf(f125634,plain,
( ( $false
= ( sK0 @ sK9 @ sK16 ) )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_28
| ~ spl19_29 ),
inference(trivial_inequality_removal,[],[f125633]) ).
thf(f125716,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_11
| ~ spl19_25
| ~ spl19_28
| ~ spl19_29 ),
inference(constrained_superposition,[],[f125634,f424]) ).
thf(f126140,plain,
( $false
| ~ spl19_7
| ~ spl19_11
| ~ spl19_25
| ~ spl19_28
| ~ spl19_29 ),
inference(trivial_inequality_removal,[],[f125716]) ).
thf(f126141,plain,
( ~ spl19_7
| ~ spl19_11
| ~ spl19_25
| ~ spl19_28
| ~ spl19_29 ),
inference(avatar_contradiction_clause,[],[f126140]) ).
thf(f218311,plain,
( ( $false = $true )
| ( $true
= ( sK0 @ sK17 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_26 ),
inference(constrained_superposition,[],[f602,f428]) ).
thf(f218778,plain,
( ( $true
= ( sK0 @ sK17 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_26 ),
inference(trivial_inequality_removal,[],[f218311]) ).
thf(f218912,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_26
| ~ spl19_27 ),
inference(forward_demodulation,[],[f218778,f434]) ).
thf(f218913,plain,
( $false
| ~ spl19_7
| ~ spl19_15
| ~ spl19_26
| ~ spl19_27 ),
inference(trivial_inequality_removal,[],[f218912]) ).
thf(f218914,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_26
| ~ spl19_27 ),
inference(avatar_contradiction_clause,[],[f218913]) ).
thf(f220561,plain,
( ( $false = $true )
| ( $true
= ( sK0 @ sK15 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_23 ),
inference(constrained_superposition,[],[f413,f602]) ).
thf(f220893,plain,
( ( $true
= ( sK0 @ sK15 @ sK6 ) )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_23 ),
inference(trivial_inequality_removal,[],[f220561]) ).
thf(f220979,plain,
( ( $false = $true )
| ~ spl19_7
| ~ spl19_15
| ~ spl19_23
| ~ spl19_24 ),
inference(forward_demodulation,[],[f220893,f419]) ).
thf(f220980,plain,
( $false
| ~ spl19_7
| ~ spl19_15
| ~ spl19_23
| ~ spl19_24 ),
inference(trivial_inequality_removal,[],[f220979]) ).
thf(f220981,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_23
| ~ spl19_24 ),
inference(avatar_contradiction_clause,[],[f220980]) ).
thf(f237514,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
= ( sK0 @ X1 @ X0 ) )
| ( $false
= ( sK0 @ X1 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] : ( Y0 != X0 )
@ X3 ) )
| ( $false
= ( sK0 @ X2 @ X3 ) )
| ( $false
= ( sK0 @ X1 @ X4 ) )
| ( $false
= ( sK0 @ X4 @ X0 ) ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(constrained_superposition,[],[f335,f1230]) ).
thf(f237723,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
= ( sK0 @ X1 @ X0 ) )
| ( $false
= ( sK0 @ X1 @ X2 ) )
| ( $true
= ( X3 != X0 ) )
| ( $false
= ( sK0 @ X2 @ X3 ) )
| ( $false
= ( sK0 @ X1 @ X4 ) )
| ( $false
= ( sK0 @ X4 @ X0 ) ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(beta-eta_normalization,[],[f237514]) ).
thf(f237724,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
= ( sK0 @ X1 @ X0 ) )
| ( $false
= ( sK0 @ X1 @ X2 ) )
| ( $false
= ( X3 = X0 ) )
| ( $false
= ( sK0 @ X2 @ X3 ) )
| ( $false
= ( sK0 @ X1 @ X4 ) )
| ( $false
= ( sK0 @ X4 @ X0 ) ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(not_proxy_clausification,[],[f237723]) ).
thf(f237725,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: $i,X4: $i] :
( ( $true
= ( sK0 @ X1 @ X0 ) )
| ( $false
= ( sK0 @ X1 @ X2 ) )
| ( $false
= ( sK0 @ X2 @ X3 ) )
| ( $false
= ( sK0 @ X1 @ X4 ) )
| ( $false
= ( sK0 @ X4 @ X0 ) )
| ( X0 != X3 ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(equality_proxy_clausification,[],[f237724]) ).
thf(f333699,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( $false != $false )
| ( $true
= ( sK0 @ X2 @ X1 ) )
| ( $false
= ( sK0 @ X2 @ X0 ) )
| ( $false
= ( sK0 @ X0 @ X1 ) )
| ( $false
= ( sK0 @ X2 @ X0 ) )
| ( X1 != X1 ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(equality_factoring,[],[f237725]) ).
thf(f333700,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( $false != $false )
| ( $true
= ( sK0 @ X2 @ X1 ) )
| ( $false
= ( sK0 @ X2 @ X0 ) )
| ( $false
= ( sK0 @ X0 @ X1 ) )
| ( X1 != X1 ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(duplicate_literal_removal,[],[f333699]) ).
thf(f333701,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( $true
= ( sK0 @ X2 @ X1 ) )
| ( $false
= ( sK0 @ X2 @ X0 ) )
| ( $false
= ( sK0 @ X0 @ X1 ) ) )
| ~ spl19_6
| ~ spl19_8 ),
inference(trivial_inequality_removal,[],[f333700]) ).
thf(f335042,plain,
( spl19_7
| ~ spl19_6
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f333701,f341,f334,f337]) ).
cnf(s3,plain,
( spl19_2
| spl19_4 ),
inference(sat_conversion,[],[f328]) ).
cnf(s4,plain,
( spl19_2
| spl19_5 ),
inference(sat_conversion,[],[f332]) ).
cnf(s5,plain,
( spl19_6
| spl19_7 ),
inference(sat_conversion,[],[f339]) ).
cnf(s6,plain,
( spl19_7
| spl19_8 ),
inference(sat_conversion,[],[f343]) ).
cnf(s9,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_14 ),
inference(sat_conversion,[],[f366]) ).
cnf(s10,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_15 ),
inference(sat_conversion,[],[f371]) ).
cnf(s11,plain,
( spl19_11
| spl19_12
| spl19_13
| spl19_16 ),
inference(sat_conversion,[],[f376]) ).
cnf(s12,plain,
( spl19_12
| spl19_13
| spl19_17
| spl19_18 ),
inference(sat_conversion,[],[f385]) ).
cnf(s13,plain,
( spl19_12
| spl19_13
| spl19_15
| spl19_17 ),
inference(sat_conversion,[],[f386]) ).
cnf(s14,plain,
( spl19_12
| spl19_13
| spl19_17
| spl19_19 ),
inference(sat_conversion,[],[f391]) ).
cnf(s15,plain,
( spl19_12
| spl19_13
| spl19_18
| spl19_20 ),
inference(sat_conversion,[],[f396]) ).
cnf(s16,plain,
( spl19_12
| spl19_13
| spl19_18
| spl19_21 ),
inference(sat_conversion,[],[f401]) ).
cnf(s17,plain,
( spl19_12
| spl19_13
| spl19_15
| spl19_20 ),
inference(sat_conversion,[],[f402]) ).
cnf(s18,plain,
( spl19_12
| spl19_13
| spl19_15
| spl19_21 ),
inference(sat_conversion,[],[f403]) ).
cnf(s19,plain,
( spl19_12
| spl19_13
| spl19_19
| spl19_20 ),
inference(sat_conversion,[],[f404]) ).
cnf(s20,plain,
( spl19_12
| spl19_13
| spl19_19
| spl19_21 ),
inference(sat_conversion,[],[f405]) ).
cnf(s21,plain,
( spl19_11
| spl19_13
| spl19_22
| spl19_23 ),
inference(sat_conversion,[],[f414]) ).
cnf(s22,plain,
( spl19_11
| spl19_13
| spl19_15
| spl19_22 ),
inference(sat_conversion,[],[f415]) ).
cnf(s23,plain,
( spl19_11
| spl19_13
| spl19_22
| spl19_24 ),
inference(sat_conversion,[],[f420]) ).
cnf(s24,plain,
( spl19_13
| spl19_22
| spl19_25
| spl19_26 ),
inference(sat_conversion,[],[f429]) ).
cnf(s25,plain,
( spl19_13
| spl19_15
| spl19_22
| spl19_25 ),
inference(sat_conversion,[],[f430]) ).
cnf(s26,plain,
( spl19_13
| spl19_22
| spl19_25
| spl19_27 ),
inference(sat_conversion,[],[f435]) ).
cnf(s27,plain,
( spl19_13
| spl19_22
| spl19_26
| spl19_28 ),
inference(sat_conversion,[],[f440]) ).
cnf(s28,plain,
( spl19_13
| spl19_22
| spl19_26
| spl19_29 ),
inference(sat_conversion,[],[f445]) ).
cnf(s29,plain,
( spl19_13
| spl19_15
| spl19_22
| spl19_28 ),
inference(sat_conversion,[],[f446]) ).
cnf(s30,plain,
( spl19_13
| spl19_15
| spl19_22
| spl19_29 ),
inference(sat_conversion,[],[f447]) ).
cnf(s31,plain,
( spl19_13
| spl19_22
| spl19_27
| spl19_28 ),
inference(sat_conversion,[],[f448]) ).
cnf(s32,plain,
( spl19_13
| spl19_22
| spl19_27
| spl19_29 ),
inference(sat_conversion,[],[f449]) ).
cnf(s34,plain,
( ~ spl19_2
| ~ spl19_13 ),
inference(sat_conversion,[],[f489]) ).
cnf(s36,plain,
( ~ spl19_2
| ~ spl19_12
| ~ spl19_22 ),
inference(sat_conversion,[],[f587]) ).
cnf(s38,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_18
| ~ spl19_19 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s127,plain,
( spl19_2
| ~ spl19_4
| ~ spl19_5 ),
inference(sat_conversion,[],[f22126]) ).
cnf(s137,plain,
( ~ spl19_7
| ~ spl19_11
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21 ),
inference(sat_conversion,[],[f26912]) ).
cnf(s139,plain,
( ~ spl19_7
| ~ spl19_14
| ~ spl19_15
| ~ spl19_16 ),
inference(sat_conversion,[],[f27783]) ).
cnf(s201,plain,
( ~ spl19_7
| ~ spl19_11
| ~ spl19_25
| ~ spl19_28
| ~ spl19_29 ),
inference(sat_conversion,[],[f126141]) ).
cnf(s677,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_26
| ~ spl19_27 ),
inference(sat_conversion,[],[f218914]) ).
cnf(s713,plain,
( ~ spl19_7
| ~ spl19_15
| ~ spl19_23
| ~ spl19_24 ),
inference(sat_conversion,[],[f220981]) ).
cnf(s3361,plain,
( ~ spl19_6
| spl19_7
| ~ spl19_8 ),
inference(sat_conversion,[],[f335042]) ).
cnf(s3387,plain,
( spl19_12
| spl19_11
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s139,s9,s10,s11]) ).
cnf(s3388,plain,
( spl19_11
| ~ spl19_7
| ~ spl19_2 ),
inference(rat,[],[s713,s22,s21,s23,s36,s3387,s34]) ).
cnf(s3389,plain,
( spl19_17
| ~ spl19_15
| spl19_12
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s38,s12,s14]) ).
cnf(s3390,plain,
( spl19_19
| ~ spl19_17
| spl19_12
| ~ spl19_11
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s137,s19,s20]) ).
cnf(s3391,plain,
( ~ spl19_15
| spl19_12
| ~ spl19_11
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s137,s15,s16,s38,s3390,s3389]) ).
cnf(s3392,plain,
( spl19_12
| ~ spl19_11
| spl19_13
| ~ spl19_7 ),
inference(rat,[],[s137,s13,s17,s18,s3391]) ).
cnf(s3393,plain,
( spl19_25
| ~ spl19_15
| spl19_22
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s677,s24,s26]) ).
cnf(s3394,plain,
( spl19_27
| ~ spl19_25
| spl19_22
| ~ spl19_11
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s201,s31,s32]) ).
cnf(s3395,plain,
( ~ spl19_15
| spl19_22
| ~ spl19_11
| ~ spl19_7
| spl19_13 ),
inference(rat,[],[s201,s28,s27,s677,s3394,s3393]) ).
cnf(s3396,plain,
( spl19_22
| ~ spl19_11
| spl19_13
| ~ spl19_7 ),
inference(rat,[],[s201,s25,s29,s30,s3395]) ).
cnf(s3397,plain,
( ~ spl19_7
| ~ spl19_2 ),
inference(rat,[],[s3396,s36,s3392,s3388,s34]) ).
cnf(s3398,plain,
spl19_7,
inference(rat,[],[s3361,s5,s6]) ).
cnf(s3399,plain,
~ spl19_2,
inference(rat,[],[s3397,s3398]) ).
cnf(s3400,plain,
spl19_5,
inference(rat,[],[s4,s3399]) ).
cnf(s3401,plain,
spl19_4,
inference(rat,[],[s3,s3399]) ).
cnf(s3404,plain,
$false,
inference(rat,[],[s127,s3399,s3400,s3401]) ).
thf(f335124,plain,
$false,
inference(avatar_sat_refutation,[],[s3404]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL602^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 09:27:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.13 Running first-order model finding
% 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.15/0.80 % (4048027)Will run a generic schedule for satisfiability detection.
% 4.15/0.80 % (4048033)% WARNING: option uhcvi not known.
% 4.15/0.80 % (4048033)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1435053773:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.15/0.80 % (4048032)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2927162178_2999 on theBenchmark for (2999ds/0Mi)
% 4.15/0.80 % (4048035)dis+10_1_sil=32000:sp=arity:random_seed=1956705489:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.15/0.80 % (4048034)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3204036714:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.15/0.80 % (4048033)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.15/0.80 % Exception at run slice level% (4048033)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.15/0.80
% 4.15/0.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.15/0.80 % (4048037)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=169386542:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.15/0.80 % (4048036)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2376576367:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.15/0.80 % (4048036)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.15/0.80 % (4048038)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2715209769:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.15/0.80 % (4048043)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=14308479:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.15/0.80 % Exception at run slice level
% 4.15/0.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.15/0.80 % (4048035)Instruction limit reached!
% 4.15/0.80 % (4048035)------------------------------
% 4.15/0.80 % (4048035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.15/0.80 % (4048035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.15/0.80 % (4048035)CaDiCaL version: 2.1.3
% 4.15/0.80 % (4048035)Termination reason: Instruction limit
% 4.15/0.80 % (4048035)Termination phase: Saturation
% 4.15/0.80 % (4048035)Time elapsed: 0.026 s
% 4.15/0.80 % (4048035)Peak memory usage: 12 MB
% 4.15/0.80 % (4048035)Instructions burned: 104 (million)
% 4.15/0.80 % (4048048)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1161747135:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.15/0.80 % (4048050)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=413438246:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.15/0.80 % (4048050)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.15/0.80 % (4048050)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.15/0.80 % (4048036)Instruction limit reached!
% 4.15/0.80 % (4048036)------------------------------
% 4.15/0.80 % (4048036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.15/0.80 % (4048036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.15/0.80 % (4048036)CaDiCaL version: 2.1.3
% 4.15/0.80 % (4048036)Termination reason: Instruction limit
% 4.15/0.80 % (4048036)Termination phase: Saturation
% 4.15/0.80 % (4048036)Time elapsed: 0.037 s
% 4.15/0.80 % (4048036)Peak memory usage: 12 MB
% 4.15/0.80 % (4048036)Instructions burned: 119 (million)
% 4.15/0.80 % (4048048)Instruction limit reached!
% 4.15/0.80 % (4048048)------------------------------
% 4.15/0.80 % (4048048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.15/0.80 % (4048048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.15/0.80 % (4048048)CaDiCaL version: 2.1.3
% 4.15/0.80 % (4048048)Termination reason: Instruction limit
% 4.15/0.80 % (4048048)Termination phase: Saturation
% 4.15/0.80 % (4048048)Time elapsed: 0.031 s
% 4.15/0.80 % (4048048)Peak memory usage: 12 MB
% 4.15/0.80 % (4048048)Instructions burned: 134 (million)
% 4.15/0.80 % (4048037)Instruction limit reached!
% 4.15/0.80 % (4048037)------------------------------
% 4.15/0.80 % (4048037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/1.70 % (4048037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/1.70 % (4048037)CaDiCaL version: 2.1.3
% 10.71/1.70 % (4048037)Termination reason: Instruction limit
% 10.71/1.70 % (4048037)Termination phase: Saturation
% 10.71/1.70 % (4048037)Time elapsed: 0.052 s
% 10.71/1.70 % (4048037)Peak memory usage: 12 MB
% 10.71/1.70 % (4048037)Instructions burned: 132 (million)
% 10.71/1.70 % (4048052)ott-21_1_sil=16000:fs=off:random_seed=1545435194:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 10.71/1.70 % (4048053)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1341023813:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 10.71/1.70 % (4048054)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=518672195:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 10.71/1.70 % Exception at run slice level
% 10.71/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.71/1.70 % (4048038)Instruction limit reached!
% 10.71/1.70 % (4048038)------------------------------
% 10.71/1.70 % (4048038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/1.70 % (4048038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/1.70 % (4048038)CaDiCaL version: 2.1.3
% 10.71/1.70 % (4048038)Termination reason: Instruction limit
% 10.71/1.70 % (4048038)Termination phase: Saturation
% 10.71/1.70 % (4048038)Time elapsed: 0.075 s
% 10.71/1.70 % (4048038)Peak memory usage: 13 MB
% 10.71/1.70 % (4048038)Instructions burned: 161 (million)
% 10.71/1.70 % (4048059)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1000454345:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 10.71/1.70 % Exception at run slice level
% 10.71/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.71/1.70 % (4048058)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3711611866:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 10.71/1.70 % (4048061)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1516578434:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 10.71/1.70 % (4048061)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.71/1.70 % (4048052)Instruction limit reached!
% 10.71/1.70 % (4048052)------------------------------
% 10.71/1.70 % (4048052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/1.70 % (4048052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/1.70 % (4048052)CaDiCaL version: 2.1.3
% 10.71/1.70 % (4048052)Termination reason: Instruction limit
% 10.71/1.70 % (4048052)Termination phase: Saturation
% 10.71/1.70 % (4048052)Time elapsed: 0.078 s
% 10.71/1.70 % (4048052)Peak memory usage: 12 MB
% 10.71/1.70 % (4048052)Instructions burned: 182 (million)
% 10.71/1.70 % (4048064)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3428530199:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 10.71/1.70 % (4048064)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.71/1.70 % (4048053)Instruction limit reached!
% 10.71/1.70 % (4048053)------------------------------
% 10.71/1.70 % (4048053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/1.70 % (4048053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/1.70 % (4048053)CaDiCaL version: 2.1.3
% 10.71/1.70 % (4048053)Termination reason: Instruction limit
% 10.71/1.70 % (4048053)Termination phase: Saturation
% 10.71/1.70 % (4048053)Time elapsed: 0.146 s
% 10.71/1.70 % (4048053)Peak memory usage: 14 MB
% 10.71/1.70 % (4048053)Instructions burned: 479 (million)
% 10.71/1.70 % (4048066)fmb+10_1_sil=64000:random_seed=1990915702:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 10.71/1.70 % (4048066)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.71/1.70 % Exception at run slice level
% 10.71/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.71/1.70 % (4048050)Instruction limit reached!
% 10.71/1.70 % (4048050)------------------------------
% 10.71/1.70 % (4048050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/1.70 % (4048050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/4.55 % (4048050)CaDiCaL version: 2.1.3
% 30.56/4.55 % (4048050)Termination reason: Instruction limit
% 30.56/4.55 % (4048050)Termination phase: Saturation
% 30.56/4.55 % (4048050)Time elapsed: 0.203 s
% 30.56/4.55 % (4048050)Peak memory usage: 16 MB
% 30.56/4.55 % (4048050)Instructions burned: 686 (million)
% 30.56/4.55 % (4048068)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2639697307:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 30.56/4.55 % Exception at run slice level
% 30.56/4.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.56/4.55 % (4048069)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3741716561:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 30.56/4.55 % Exception at run slice level
% 30.56/4.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.56/4.55 % (4048071)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1918898736:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 30.56/4.55 % (4048071)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 30.56/4.55 % (4048073)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1495638214:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi)
% 30.56/4.55 % (4048073)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 30.56/4.55 % (4048073)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 30.56/4.55 % (4048064)Instruction limit reached!
% 30.56/4.55 % (4048064)------------------------------
% 30.56/4.55 % (4048064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.56/4.55 % (4048064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/4.55 % (4048064)CaDiCaL version: 2.1.3
% 30.56/4.55 % (4048064)Termination reason: Instruction limit
% 30.56/4.55 % (4048064)Termination phase: Saturation
% 30.56/4.55 % (4048064)Time elapsed: 0.219 s
% 30.56/4.55 % (4048064)Peak memory usage: 15 MB
% 30.56/4.55 % (4048064)Instructions burned: 879 (million)
% 30.56/4.55 % (4048076)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2028040528:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 30.56/4.55 % Exception at run slice level
% 30.56/4.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.56/4.55 % (4048078)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1034747691:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 30.56/4.55 % Exception at run slice level
% 30.56/4.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.56/4.55 % (4048080)ott-2_1_sil=16000:newcnf=on:random_seed=4290780012:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 30.56/4.55 % (4048080)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 30.56/4.55 % (4048061)Instruction limit reached!
% 30.56/4.55 % (4048061)------------------------------
% 30.56/4.55 % (4048061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.56/4.55 % (4048061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/4.55 % (4048061)CaDiCaL version: 2.1.3
% 30.56/4.55 % (4048061)Termination reason: Instruction limit
% 30.56/4.55 % (4048061)Termination phase: Saturation
% 30.56/4.55 % (4048061)Time elapsed: 0.320 s
% 30.56/4.55 % (4048061)Peak memory usage: 17 MB
% 30.56/4.55 % (4048061)Instructions burned: 692 (million)
% 30.56/4.55 % (4048082)ott+10_1_sil=32000:tgt=ground:random_seed=2268513816:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi)
% 30.56/4.55 % (4048058)Instruction limit reached!
% 30.56/4.55 % (4048058)------------------------------
% 30.56/4.55 % (4048058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.56/4.55 % (4048058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/4.55 % (4048058)CaDiCaL version: 2.1.3
% 30.56/4.55 % (4048058)Termination reason: Instruction limit
% 30.56/4.55 % (4048058)Termination phase: Saturation
% 30.56/4.55 % (4048058)Time elapsed: 0.511 s
% 30.56/4.55 % (4048058)Peak memory usage: 16 MB
% 30.56/4.55 % (4048058)Instructions burned: 1179 (million)
% 30.56/4.55 % (4048084)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3233863437:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 30.56/4.55 % Exception at run slice level
% 68.49/10.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.49/10.01 % (4048073)Instruction limit reached!
% 68.49/10.01 % (4048073)------------------------------
% 68.49/10.01 % (4048073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.49/10.01 % (4048073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.49/10.01 % (4048073)CaDiCaL version: 2.1.3
% 68.49/10.01 % (4048073)Termination reason: Instruction limit
% 68.49/10.01 % (4048073)Termination phase: Saturation
% 68.49/10.01 % (4048073)Time elapsed: 0.393 s
% 68.49/10.01 % (4048073)Peak memory usage: 18 MB
% 68.49/10.01 % (4048073)Instructions burned: 1474 (million)
% 68.49/10.01 % (4048086)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=202171134:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 68.49/10.01 % (4048086)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.49/10.01 % (4048087)dis+21_1_sil=32000:sas=cadical:random_seed=3799570155:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi)
% 68.49/10.01 % (4048080)Instruction limit reached!
% 68.49/10.01 % (4048080)------------------------------
% 68.49/10.01 % (4048080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.49/10.01 % (4048080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.49/10.01 % (4048080)CaDiCaL version: 2.1.3
% 68.49/10.01 % (4048080)Termination reason: Instruction limit
% 68.49/10.01 % (4048080)Termination phase: Saturation
% 68.49/10.01 % (4048080)Time elapsed: 0.314 s
% 68.49/10.01 % (4048080)Peak memory usage: 14 MB
% 68.49/10.01 % (4048080)Instructions burned: 870 (million)
% 68.49/10.01 % (4048090)ott+11_1_sil=16000:gs=on:random_seed=853683148:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi)
% 68.49/10.01 % (4048090)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.49/10.01 % (4048071)Instruction limit reached!
% 68.49/10.01 % (4048071)------------------------------
% 68.49/10.01 % (4048071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.49/10.01 % (4048071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.49/10.01 % (4048071)CaDiCaL version: 2.1.3
% 68.49/10.01 % (4048071)Termination reason: Instruction limit
% 68.49/10.01 % (4048071)Termination phase: Saturation
% 68.49/10.01 % (4048071)Time elapsed: 1.162 s
% 68.49/10.01 % (4048071)Peak memory usage: 22 MB
% 68.49/10.01 % (4048071)Instructions burned: 5132 (million)
% 68.49/10.01 % (4048092)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1774447408:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi)
% 68.49/10.01 % Exception at run slice level
% 68.49/10.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.49/10.01 % (4048094)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3133946428:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi)
% 68.49/10.01 % (4048086)Instruction limit reached!
% 68.49/10.01 % (4048086)------------------------------
% 68.49/10.01 % (4048086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.49/10.01 % (4048086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.49/10.01 % (4048086)CaDiCaL version: 2.1.3
% 68.49/10.01 % (4048086)Termination reason: Instruction limit
% 68.49/10.01 % (4048086)Termination phase: Saturation
% 68.49/10.01 % (4048086)Time elapsed: 0.833 s
% 68.49/10.01 % (4048086)Peak memory usage: 21 MB
% 68.49/10.01 % (4048086)Instructions burned: 3516 (million)
% 68.49/10.01 % (4048096)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=687505896:i=29340_2984 on theBenchmark for (2984ds/29340Mi)
% 68.49/10.01 % (4048087)Instruction limit reached!
% 68.49/10.01 % (4048087)------------------------------
% 68.49/10.01 % (4048087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.49/10.01 % (4048087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.49/10.01 % (4048087)CaDiCaL version: 2.1.3
% 68.49/10.01 % (4048087)Termination reason: Instruction limit
% 68.49/10.01 % (4048087)Termination phase: Saturation
% 68.49/10.01 % (4048087)Time elapsed: 0.865 s
% 68.49/10.01 % (4048087)Peak memory usage: 22 MB
% 68.49/10.01 % (4048087)Instructions burned: 3776 (million)
% 68.49/10.01 % (4048098)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2784527862:i=5211_2984 on theBenchmark for (2984ds/5211Mi)
% 83.60/12.04 % (4048090)Instruction limit reached!
% 83.60/12.04 % (4048090)------------------------------
% 83.60/12.04 % (4048090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.04 % (4048090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.04 % (4048090)CaDiCaL version: 2.1.3
% 83.60/12.04 % (4048090)Termination reason: Instruction limit
% 83.60/12.04 % (4048090)Termination phase: Saturation
% 83.60/12.04 % (4048090)Time elapsed: 0.883 s
% 83.60/12.04 % (4048090)Peak memory usage: 16 MB
% 83.60/12.04 % (4048090)Instructions burned: 2253 (million)
% 83.60/12.04 % (4048101)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=640872638:i=5497:nm=2_2983 on theBenchmark for (2983ds/5497Mi)
% 83.60/12.04 % Exception at run slice level
% 83.60/12.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 83.60/12.04 % (4048103)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3780860546:fmbsr=2:i=46332_2983 on theBenchmark for (2983ds/46332Mi)
% 83.60/12.04 % Exception at run slice level
% 83.60/12.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 83.60/12.04 % (4048105)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1934398931:i=14071_2983 on theBenchmark for (2983ds/14071Mi)
% 83.60/12.04 % Exception at run slice level
% 83.60/12.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 83.60/12.04 % (4048108)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2484313125:i=22565:add=on:rawr=on_2982 on theBenchmark for (2982ds/22565Mi)
% 83.60/12.04 % (4048082)Instruction limit reached!
% 83.60/12.04 % (4048082)------------------------------
% 83.60/12.04 % (4048082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.04 % (4048082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.04 % (4048082)CaDiCaL version: 2.1.3
% 83.60/12.04 % (4048082)Termination reason: Instruction limit
% 83.60/12.04 % (4048082)Termination phase: Saturation
% 83.60/12.04 % (4048082)Time elapsed: 1.223 s
% 83.60/12.04 % (4048082)Peak memory usage: 18 MB
% 83.60/12.04 % (4048082)Instructions burned: 5116 (million)
% 83.60/12.04 % (4048110)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3787096505:i=8173:av=off_2982 on theBenchmark for (2982ds/8173Mi)
% 83.60/12.04 % (4048094)Instruction limit reached!
% 83.60/12.04 % (4048094)------------------------------
% 83.60/12.04 % (4048094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.04 % (4048094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.04 % (4048094)CaDiCaL version: 2.1.3
% 83.60/12.04 % (4048094)Termination reason: Instruction limit
% 83.60/12.04 % (4048094)Termination phase: Saturation
% 83.60/12.04 % (4048094)Time elapsed: 1.043 s
% 83.60/12.04 % (4048094)Peak memory usage: 21 MB
% 83.60/12.04 % (4048094)Instructions burned: 4594 (million)
% 83.60/12.04 % (4048112)dis+10_16:1_sil=16000:random_seed=29484593:i=9155:fsr=off_2974 on theBenchmark for (2974ds/9155Mi)
% 83.60/12.04 % (4048098)Instruction limit reached!
% 83.60/12.04 % (4048098)------------------------------
% 83.60/12.04 % (4048098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.04 % (4048098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.04 % (4048098)CaDiCaL version: 2.1.3
% 83.60/12.04 % (4048098)Termination reason: Instruction limit
% 83.60/12.04 % (4048098)Termination phase: Saturation
% 83.60/12.04 % (4048098)Time elapsed: 1.719 s
% 83.60/12.04 % (4048098)Peak memory usage: 26 MB
% 83.60/12.04 % (4048098)Instructions burned: 5215 (million)
% 83.60/12.04 % (4048114)ott-3_8_sil=64000:random_seed=1414008819:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi)
% 83.60/12.04 % (4048110)Instruction limit reached!
% 83.60/12.04 % (4048110)------------------------------
% 83.60/12.04 % (4048110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.04 % (4048110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.04 % (4048110)CaDiCaL version: 2.1.3
% 83.60/12.04 % (4048110)Termination reason: Instruction limit
% 83.60/12.04 % (4048110)Termination phase: Saturation
% 83.60/12.04 % (4048110)Time elapsed: 2.653 s
% 83.60/12.04 % (4048110)Peak memory usage: 21 MB
% 83.60/12.04 % (4048110)Instructions burned: 8178 (million)
% 83.60/12.04 % (4048118)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1509229639:fmbsr=2:i=32576_2955 on theBenchmark for (2955ds/32576Mi)
% 88.65/12.81 % Exception at run slice level
% 88.65/12.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 88.65/12.81 % (4048120)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1990268165:i=11404_2955 on theBenchmark for (2955ds/11404Mi)
% 88.65/12.81 % (4048112)Instruction limit reached!
% 88.65/12.81 % (4048112)------------------------------
% 88.65/12.81 % (4048112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.65/12.81 % (4048112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.65/12.81 % (4048112)CaDiCaL version: 2.1.3
% 88.65/12.81 % (4048112)Termination reason: Instruction limit
% 88.65/12.81 % (4048112)Termination phase: Saturation
% 88.65/12.81 % (4048112)Time elapsed: 2.815 s
% 88.65/12.81 % (4048112)Peak memory usage: 26 MB
% 88.65/12.81 % (4048112)Instructions burned: 9155 (million)
% 88.65/12.81 % (4048122)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2373751919:i=14134_2946 on theBenchmark for (2946ds/14134Mi)
% 88.65/12.81 % (4048122)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 88.65/12.81 % (4048120)Instruction limit reached!
% 88.65/12.81 % (4048120)------------------------------
% 88.65/12.81 % (4048120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.65/12.81 % (4048120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.65/12.81 % (4048120)CaDiCaL version: 2.1.3
% 88.65/12.81 % (4048120)Termination reason: Instruction limit
% 88.65/12.81 % (4048120)Termination phase: Saturation
% 88.65/12.81 % (4048120)Time elapsed: 2.796 s
% 88.65/12.81 % (4048120)Peak memory usage: 34 MB
% 88.65/12.81 % (4048120)Instructions burned: 11408 (million)
% 88.65/12.81 % (4048134)dis+33_16_sil=32000:sac=on:random_seed=3606608941:i=15851:nm=0_2927 on theBenchmark for (2927ds/15851Mi)
% 88.65/12.81 % (4048108)Instruction limit reached!
% 88.65/12.81 % (4048108)------------------------------
% 88.65/12.81 % (4048108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.65/12.81 % (4048108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.65/12.81 % (4048108)CaDiCaL version: 2.1.3
% 88.65/12.81 % (4048108)Termination reason: Instruction limit
% 88.65/12.81 % (4048108)Termination phase: Saturation
% 88.65/12.81 % (4048108)Time elapsed: 5.664 s
% 88.65/12.81 % (4048108)Peak memory usage: 90 MB
% 88.65/12.81 % (4048108)Instructions burned: 22567 (million)
% 88.65/12.81 % (4048136)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=525895723:avsq=on:i=17627:add=on:amm=off_2926 on theBenchmark for (2926ds/17627Mi)
% 88.65/12.81 % (4048114)Instruction limit reached!
% 88.65/12.81 % (4048114)------------------------------
% 88.65/12.81 % (4048114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.65/12.81 % (4048114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.65/12.81 % (4048114)CaDiCaL version: 2.1.3
% 88.65/12.81 % (4048114)Termination reason: Instruction limit
% 88.65/12.81 % (4048114)Termination phase: Saturation
% 88.65/12.81 % (4048114)Time elapsed: 4.796 s
% 88.65/12.81 % (4048114)Peak memory usage: 51 MB
% 88.65/12.81 % (4048114)Instructions burned: 20141 (million)
% 88.65/12.81 % (4048138)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=487645393:s2a=on:i=53295_2918 on theBenchmark for (2918ds/53295Mi)
% 88.65/12.81 % (4048096)Instruction limit reached!
% 88.65/12.81 % (4048096)------------------------------
% 88.65/12.81 % (4048096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.65/12.81 % (4048096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.65/12.81 % (4048096)CaDiCaL version: 2.1.3
% 88.65/12.81 % (4048096)Termination reason: Instruction limit
% 88.65/12.81 % (4048096)Termination phase: Saturation
% 88.65/12.81 % (4048096)Time elapsed: 8.026 s
% 88.65/12.81 % (4048096)Peak memory usage: 77 MB
% 88.65/12.81 % (4048096)Instructions burned: 29343 (million)
% 88.65/12.81 % (4048140)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1714990730:i=26857:ins=20_2904 on theBenchmark for (2904ds/26857Mi)
% 88.65/12.81 % Exception at run slice level
% 88.65/12.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 88.65/12.81 % (4048142)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3701456111:i=28120:bs=on:fsr=off_2904 on theBenchmark for (2904ds/28120Mi)
% 88.65/12.81 % (4048122)Instruction limit reached!
% 88.65/12.81 % (4048122)------------------------------
% 88.65/12.81 % (4048122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.91/14.24 % (4048122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.91/14.24 % (4048122)CaDiCaL version: 2.1.3
% 98.91/14.24 % (4048122)Termination reason: Instruction limit
% 98.91/14.24 % (4048122)Termination phase: Saturation
% 98.91/14.24 % (4048122)Time elapsed: 4.503 s
% 98.91/14.24 % (4048122)Peak memory usage: 28 MB
% 98.91/14.24 % (4048122)Instructions burned: 14137 (million)
% 98.91/14.24 % (4048144)fmb+10_1_sil=256000:fmbss=7:random_seed=2461220092:fmbsr=1.6:i=182295_2901 on theBenchmark for (2901ds/182295Mi)
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048146)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2433183887:i=44625:gsp=on_2900 on theBenchmark for (2900ds/44625Mi)
% 98.91/14.24 % (4048146)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 98.91/14.24 % (4048146)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048148)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1237121183:i=160505_2900 on theBenchmark for (2900ds/160505Mi)
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048150)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1206771677:fmbsr=1.3:i=225729_2900 on theBenchmark for (2900ds/225729Mi)
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048152)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=915325095:fmbsr=2:i=185024:ins=7_2900 on theBenchmark for (2900ds/185024Mi)
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048154)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3557122622:rtra=on_2899 on theBenchmark for (2899ds/0Mi)
% 98.91/14.24 % Exception at run slice level
% 98.91/14.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.91/14.24 % (4048156)% WARNING: option uhcvi not known.
% 98.91/14.24 % (4048156)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3445064869:i=271062:add=off:rtra=on:rawr=on_2899 on theBenchmark for (2899ds/271062Mi)
% 98.91/14.24 % (4048156)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 98.91/14.24 % (4048156)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 98.91/14.24 % (4048134)Instruction limit reached!
% 98.91/14.24 % (4048134)------------------------------
% 98.91/14.24 % (4048134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.91/14.24 % (4048134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.91/14.24 % (4048134)CaDiCaL version: 2.1.3
% 98.91/14.24 % (4048134)Termination reason: Instruction limit
% 98.91/14.24 % (4048134)Termination phase: Saturation
% 98.91/14.24 % (4048134)Time elapsed: 3.823 s
% 98.91/14.24 % (4048134)Peak memory usage: 46 MB
% 98.91/14.24 % (4048134)Instructions burned: 15853 (million)
% 98.91/14.24 % (4048158)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3424451880:i=176048:add=on:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/176048Mi)
% 98.91/14.24 % (4048136)Instruction limit reached!
% 98.91/14.24 % (4048136)------------------------------
% 98.91/14.24 % (4048136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.91/14.24 % (4048136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.91/14.24 % (4048136)CaDiCaL version: 2.1.3
% 98.91/14.24 % (4048136)Termination reason: Instruction limit
% 98.91/14.24 % (4048136)Termination phase: Saturation
% 98.91/14.24 % (4048136)Time elapsed: 4.441 s
% 98.91/14.24 % (4048136)Peak memory usage: 54 MB
% 98.91/14.24 % (4048136)Instructions burned: 17630 (million)
% 98.91/14.24 % (4048160)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1771102920:i=206:fgj=on:rtra=on_2881 on theBenchmark for (2881ds/206Mi)
% 98.91/14.24 % (4048160)Instruction limit reached!
% 98.91/14.24 % (4048160)------------------------------
% 120.09/17.28 % (4048160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.09/17.28 % (4048160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.09/17.28 % (4048160)CaDiCaL version: 2.1.3
% 120.09/17.28 % (4048160)Termination reason: Instruction limit
% 120.09/17.28 % (4048160)Termination phase: Saturation
% 120.09/17.28 % (4048160)Time elapsed: 0.050 s
% 120.09/17.28 % (4048160)Peak memory usage: 12 MB
% 120.09/17.28 % (4048160)Instructions burned: 208 (million)
% 120.09/17.28 % (4048162)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2144525632:i=232:rtra=on_2880 on theBenchmark for (2880ds/232Mi)
% 120.09/17.28 % (4048162)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 120.09/17.28 % (4048162)Instruction limit reached!
% 120.09/17.28 % (4048162)------------------------------
% 120.09/17.28 % (4048162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.09/17.28 % (4048162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.09/17.28 % (4048162)CaDiCaL version: 2.1.3
% 120.09/17.28 % (4048162)Termination reason: Instruction limit
% 120.09/17.28 % (4048162)Termination phase: Saturation
% 120.09/17.28 % (4048162)Time elapsed: 0.063 s
% 120.09/17.28 % (4048162)Peak memory usage: 12 MB
% 120.09/17.28 % (4048162)Instructions burned: 233 (million)
% 120.09/17.28 % (4048164)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3095581956:i=262:rtra=on_2880 on theBenchmark for (2880ds/262Mi)
% 120.09/17.28 % (4048164)Instruction limit reached!
% 120.09/17.28 % (4048164)------------------------------
% 120.09/17.28 % (4048164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.09/17.28 % (4048164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.09/17.28 % (4048164)CaDiCaL version: 2.1.3
% 120.09/17.28 % (4048164)Termination reason: Instruction limit
% 120.09/17.28 % (4048164)Termination phase: Saturation
% 120.09/17.28 % (4048164)Time elapsed: 0.110 s
% 120.09/17.28 % (4048164)Peak memory usage: 13 MB
% 120.09/17.28 % (4048164)Instructions burned: 264 (million)
% 120.09/17.28 % (4048166)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3738827780:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2878 on theBenchmark for (2878ds/318Mi)
% 120.09/17.28 % (4048166)Instruction limit reached!
% 120.09/17.28 % (4048166)------------------------------
% 120.09/17.28 % (4048166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.09/17.28 % (4048166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.09/17.28 % (4048166)CaDiCaL version: 2.1.3
% 120.09/17.28 % (4048166)Termination reason: Instruction limit
% 120.09/17.28 % (4048166)Termination phase: Saturation
% 120.09/17.28 % (4048166)Time elapsed: 0.077 s
% 120.09/17.28 % (4048166)Peak memory usage: 13 MB
% 120.09/17.28 % (4048166)Instructions burned: 319 (million)
% 120.09/17.28 % (4048168)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=7672964:i=1428:nm=2:rtra=on_2878 on theBenchmark for (2878ds/1428Mi)
% 120.09/17.28 % Exception at run slice level
% 120.09/17.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 120.09/17.28 % (4048170)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1952455509:i=262:bd=preordered:rtra=on:fsd=on_2877 on theBenchmark for (2877ds/262Mi)
% 120.09/17.28 % (4048170)Instruction limit reached!
% 120.09/17.28 % (4048170)------------------------------
% 120.09/17.28 % (4048170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.09/17.28 % (4048170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.09/17.28 % (4048170)CaDiCaL version: 2.1.3
% 120.09/17.28 % (4048170)Termination reason: Instruction limit
% 120.09/17.28 % (4048170)Termination phase: Saturation
% 120.09/17.28 % (4048170)Time elapsed: 0.069 s
% 120.09/17.28 % (4048170)Peak memory usage: 13 MB
% 120.09/17.28 % (4048170)Instructions burned: 263 (million)
% 120.09/17.28 % (4048172)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1947104534:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2877 on theBenchmark for (2877ds/1368Mi)
% 120.09/17.28 % (4048172)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 120.09/17.28 % (4048172)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 120.09/17.28 % (4048172)Instruction limit reached!
% 120.09/17.28 % (4048172)------------------------------
% 120.09/17.28 % (4048172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048172)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048172)Termination reason: Instruction limit
% 103.36/17.32 % (4048172)Termination phase: Saturation
% 103.36/17.32 % (4048172)Time elapsed: 0.368 s
% 103.36/17.32 % (4048172)Peak memory usage: 18 MB
% 103.36/17.32 % (4048172)Instructions burned: 1369 (million)
% 103.36/17.32 % (4048174)ott-21_1_sil=16000:si=on:fs=off:random_seed=2601573529:i=360:av=off:fsr=off:rtra=on_2873 on theBenchmark for (2873ds/360Mi)
% 103.36/17.32 % (4048174)Instruction limit reached!
% 103.36/17.32 % (4048174)------------------------------
% 103.36/17.32 % (4048174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048174)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048174)Termination reason: Instruction limit
% 103.36/17.32 % (4048174)Termination phase: Saturation
% 103.36/17.32 % (4048174)Time elapsed: 0.088 s
% 103.36/17.32 % (4048174)Peak memory usage: 13 MB
% 103.36/17.32 % (4048174)Instructions burned: 364 (million)
% 103.36/17.32 % (4048176)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2751723971:i=954:bd=all:rtra=on_2872 on theBenchmark for (2872ds/954Mi)
% 103.36/17.32 % (4048176)Instruction limit reached!
% 103.36/17.32 % (4048176)------------------------------
% 103.36/17.32 % (4048176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048176)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048176)Termination reason: Instruction limit
% 103.36/17.32 % (4048176)Termination phase: Saturation
% 103.36/17.32 % (4048176)Time elapsed: 0.248 s
% 103.36/17.32 % (4048176)Peak memory usage: 15 MB
% 103.36/17.32 % (4048176)Instructions burned: 957 (million)
% 103.36/17.32 % (4048178)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4267465308:fmbsr=1.3:i=1730:ins=25:rtra=on_2869 on theBenchmark for (2869ds/1730Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048180)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3872916140:i=2358:rtra=on_2869 on theBenchmark for (2869ds/2358Mi)
% 103.36/17.32 % (4048180)Instruction limit reached!
% 103.36/17.32 % (4048180)------------------------------
% 103.36/17.32 % (4048180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048180)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048180)Termination reason: Instruction limit
% 103.36/17.32 % (4048180)Termination phase: Saturation
% 103.36/17.32 % (4048180)Time elapsed: 0.639 s
% 103.36/17.32 % (4048180)Peak memory usage: 20 MB
% 103.36/17.32 % (4048180)Instructions burned: 2360 (million)
% 103.36/17.32 % (4048182)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1097892186:i=1778:ins=1:rtra=on_2862 on theBenchmark for (2862ds/1778Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048184)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3596022845:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2862 on theBenchmark for (2862ds/1384Mi)
% 103.36/17.32 % (4048184)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 103.36/17.32 % (4048184)Instruction limit reached!
% 103.36/17.32 % (4048184)------------------------------
% 103.36/17.32 % (4048184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048184)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048184)Termination reason: Instruction limit
% 103.36/17.32 % (4048184)Termination phase: Saturation
% 103.36/17.32 % (4048184)Time elapsed: 0.372 s
% 103.36/17.32 % (4048184)Peak memory usage: 20 MB
% 103.36/17.32 % (4048184)Instructions burned: 1386 (million)
% 103.36/17.32 % (4048186)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2926326573:i=1758:kws=inv_precedence:fsr=off:rtra=on_2859 on theBenchmark for (2859ds/1758Mi)
% 103.36/17.32 % (4048186)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 103.36/17.32 % (4048186)Instruction limit reached!
% 103.36/17.32 % (4048186)------------------------------
% 103.36/17.32 % (4048186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048186)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048186)Termination reason: Instruction limit
% 103.36/17.32 % (4048186)Termination phase: Saturation
% 103.36/17.32 % (4048186)Time elapsed: 0.442 s
% 103.36/17.32 % (4048186)Peak memory usage: 17 MB
% 103.36/17.32 % (4048186)Instructions burned: 1761 (million)
% 103.36/17.32 % (4048188)fmb+10_1_sil=64000:si=on:random_seed=3747033486:i=44122:nm=2:rtra=on:gsp=on_2854 on theBenchmark for (2854ds/44122Mi)
% 103.36/17.32 % (4048188)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048190)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3852207270:i=19030:nm=5:rtra=on_2854 on theBenchmark for (2854ds/19030Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048192)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3150172257:fmbsr=1.7:i=1840:rtra=on_2854 on theBenchmark for (2854ds/1840Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048194)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3974028203:i=10262:rtra=on_2854 on theBenchmark for (2854ds/10262Mi)
% 103.36/17.32 % (4048194)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 103.36/17.32 % (4048142)Instruction limit reached!
% 103.36/17.32 % (4048142)------------------------------
% 103.36/17.32 % (4048142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048142)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048142)Termination reason: Instruction limit
% 103.36/17.32 % (4048142)Termination phase: Saturation
% 103.36/17.32 % (4048142)Time elapsed: 7.427 s
% 103.36/17.32 % (4048142)Peak memory usage: 22 MB
% 103.36/17.32 % (4048142)Instructions burned: 28121 (million)
% 103.36/17.32 % (4048198)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1525701192:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2829 on theBenchmark for (2829ds/2944Mi)
% 103.36/17.32 % (4048198)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 103.36/17.32 % (4048198)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 103.36/17.32 % (4048194)Instruction limit reached!
% 103.36/17.32 % (4048194)------------------------------
% 103.36/17.32 % (4048194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.32 % (4048194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.32 % (4048194)CaDiCaL version: 2.1.3
% 103.36/17.32 % (4048194)Termination reason: Instruction limit
% 103.36/17.32 % (4048194)Termination phase: Saturation
% 103.36/17.32 % (4048194)Time elapsed: 2.492 s
% 103.36/17.32 % (4048194)Peak memory usage: 28 MB
% 103.36/17.32 % (4048194)Instructions burned: 10262 (million)
% 103.36/17.32 % (4048200)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3527320533:i=12648:rtra=on_2828 on theBenchmark for (2828ds/12648Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048202)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3806719622:fmbsr=2.30978:i=4348:rtra=on_2828 on theBenchmark for (2828ds/4348Mi)
% 103.36/17.32 % Exception at run slice level
% 103.36/17.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 103.36/17.32 % (4048204)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2420188382:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2828 on theBenchmark for (2828ds/1738Mi)
% 103.36/17.32 % (4048204)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 103.36/17.32 % (4048033) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4048027-4048033"...
% 103.36/17.32 % (4048033)...printing done.
% 103.36/17.32 % (4048033)Refutation found. Thanks to Tanya!
% 103.36/17.32 % SZS status Theorem for theBenchmark
% 103.36/17.32 % SZS output start Proof for theBenchmark
% See solution above
% 103.36/17.33 % (4048033)------------------------------
% 103.36/17.33 % (4048033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.36/17.33 % (4048033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.36/17.33 % (4048033)CaDiCaL version: 2.1.3
% 103.36/17.33 % (4048033)Termination reason: Refutation
% 103.36/17.33 % (4048033)Time elapsed: 17.136 s
% 103.36/17.33 % (4048033)Peak memory usage: 113 MB
% 103.36/17.33 % (4048033)Instructions burned: 66870 (million)
% 103.36/17.33 % (4048027)Success in time 17.192 s
% 103.36/17.33 % Vampire exiting
%------------------------------------------------------------------------------