%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG276^5 : TPTP v9.3.1. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 07:45:29 AM UTC 2026
% Result : Theorem 39.28s 6.02s
% Output : Refutation 39.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 21
% Syntax : Number of formulae : 391 ( 33 unt; 0 typ; 14 def)
% Number of atoms : 2561 ( 957 equ; 0 cnn)
% Maximal formula atoms : 9 ( 6 avg)
% Number of connectives : 6437 ( 957 ~;1088 |; 163 &;3856 @)
% ( 18 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 98 ( 98 >; 0 *; 0 +; 0 <<)
% Number of symbols : 58 ( 53 usr; 27 con; 0-4 aty)
% ( 230 !!; 124 ??; 0 @@+; 0 @@-)
% Number of variables : 1161 ( 0 sgn 635 !; 15 ?;1161 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
g: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
cGROUP1: ( g > g > g ) > g > $o ).
thf(func_def_1,type,
cGROUP4: ( g > g > g ) > $o ).
thf(func_def_2,type,
cGRP_ASSOC: ( g > g > g ) > $o ).
thf(func_def_3,type,
cGRP_DIVISORS: ( g > g > g ) > $o ).
thf(func_def_4,type,
cGRP_INVERSE: ( g > g > g ) > g > $o ).
thf(func_def_5,type,
cGRP_UNIT: ( g > g > g ) > g > $o ).
thf(func_def_7,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_8,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_9,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_11,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_12,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_13,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_14,type,
vAND: $o > $o > $o ).
thf(func_def_15,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_18,type,
sK0: g > g > g ).
thf(func_def_19,type,
sK1: g ).
thf(func_def_20,type,
vNOT: $o > $o ).
thf(func_def_21,type,
sK2: g > g ).
thf(func_def_22,type,
sK3: g > g > g ).
thf(func_def_23,type,
sK4: g > g > g ).
thf(func_def_24,type,
sK5: g > g > g ).
thf(func_def_25,type,
sK6: g > g > g ).
thf(func_def_26,type,
sK7: g > g > g ).
thf(func_def_27,type,
sK8: g > g > g ).
thf(func_def_28,type,
sK9: g > g ).
thf(func_def_29,type,
sK10: g > g > g ).
thf(func_def_30,type,
sK11: g > g > g ).
thf(func_def_31,type,
sK12: g ).
thf(func_def_32,type,
sK13: g > g ).
thf(func_def_33,type,
sK14: g ).
thf(func_def_34,type,
sK15: g > g ).
thf(func_def_35,type,
sK16: g ).
thf(func_def_36,type,
sK17: g ).
thf(func_def_37,type,
sK18: g ).
thf(func_def_38,type,
sK19: g ).
thf(func_def_39,type,
sK20: g ).
thf(func_def_40,type,
sK21: g ).
thf(f1,axiom,
( cGRP_ASSOC
= ( ^ [X0: g > g > g] :
! [X1: g,X2: g,X3: g] :
( ( X0 @ ( X0 @ X1 @ X2 ) @ X3 )
= ( X0 @ X1 @ ( X0 @ X2 @ X3 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGRP_ASSOC_def) ).
thf(f2,axiom,
( cGRP_DIVISORS
= ( ^ [X0: g > g > g] :
! [X1: g,X2: g] :
( ? [X4: g] :
( ( X0 @ X4 @ X1 )
= X2 )
& ? [X3: g] :
( ( X0 @ X1 @ X3 )
= X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGRP_DIVISORS_def) ).
thf(f3,axiom,
( cGRP_INVERSE
= ( ^ [X0: g > g > g,X1: g] :
! [X2: g] :
? [X3: g] :
( ( ( X0 @ X3 @ X2 )
= X1 )
& ( ( X0 @ X2 @ X3 )
= X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGRP_INVERSE_def) ).
thf(f4,axiom,
( cGRP_UNIT
= ( ^ [X0: g > g > g,X1: g] :
! [X2: g] :
( ( ( X0 @ X2 @ X1 )
= X2 )
& ( ( X0 @ X1 @ X2 )
= X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGRP_UNIT_def) ).
thf(f5,axiom,
( cGROUP1
= ( ^ [X0: g > g > g,X1: g] :
( ( cGRP_INVERSE @ X0 @ X1 )
& ( cGRP_UNIT @ X0 @ X1 )
& ( cGRP_ASSOC @ X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGROUP1_def) ).
thf(f6,axiom,
( cGROUP4
= ( ^ [X0: g > g > g] :
( ( cGRP_DIVISORS @ X0 )
& ( cGRP_ASSOC @ X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cGROUP4_def) ).
thf(f7,conjecture,
! [X0: g > g > g] :
( ? [X1: g] : ( cGROUP1 @ X0 @ X1 )
<=> ( cGROUP4 @ X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cEQUIV_01_04) ).
thf(f8,negated_conjecture,
~ ! [X0: g > g > g] :
( ? [X1: g] : ( cGROUP1 @ X0 @ X1 )
<=> ( cGROUP4 @ X0 ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
thf(f9,plain,
( cGRP_ASSOC
= ( ^ [Y0: g > g > g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( ( Y0 @ ( Y0 @ Y3 @ Y2 ) @ Y1 )
= ( Y0 @ Y3 @ ( Y0 @ Y2 @ Y1 ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f1]) ).
thf(f10,plain,
( cGRP_DIVISORS
= ( ^ [X0: g > g > g] :
! [X1: g,X2: g] :
( ? [X3: g] :
( ( X0 @ X3 @ X1 )
= X2 )
& ? [X4: g] :
( ( X0 @ X1 @ X4 )
= X2 ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f11,plain,
( cGRP_DIVISORS
= ( ^ [Y0: g > g > g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( ?? @ g
@ ^ [Y3: g] :
( ( Y0 @ Y2 @ Y3 )
= Y1 ) )
& ( ?? @ g
@ ^ [Y3: g] :
( ( Y0 @ Y3 @ Y2 )
= Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f10]) ).
thf(f12,plain,
( cGRP_INVERSE
= ( ^ [Y0: g > g > g,Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ?? @ g
@ ^ [Y3: g] :
( ( ( Y0 @ Y2 @ Y3 )
= Y1 )
& ( ( Y0 @ Y3 @ Y2 )
= Y1 ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f13,plain,
( cGRP_UNIT
= ( ^ [Y0: g > g > g,Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( ( Y0 @ Y1 @ Y2 )
= Y2 )
& ( ( Y0 @ Y2 @ Y1 )
= Y2 ) ) ) ) ),
inference(fool_elimination,[],[f4]) ).
thf(f14,plain,
( cGROUP1
= ( ^ [X0: g > g > g,X1: g] :
( ( cGRP_INVERSE @ X0 @ X1 )
& ( cGRP_UNIT @ X0 @ X1 )
& ( cGRP_ASSOC @ X0 ) ) ) ),
inference(rectify,[],[f5]) ).
thf(f15,plain,
( cGROUP1
= ( ^ [Y0: g > g > g,Y1: g] :
( ( cGRP_ASSOC @ Y0 )
& ( cGRP_UNIT @ Y0 @ Y1 )
& ( cGRP_INVERSE @ Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f14]) ).
thf(f16,plain,
( cGROUP4
= ( ^ [X0: g > g > g] :
( ( cGRP_DIVISORS @ X0 )
& ( cGRP_ASSOC @ X0 ) ) ) ),
inference(rectify,[],[f6]) ).
thf(f17,plain,
( cGROUP4
= ( ^ [Y0: g > g > g] :
( ( cGRP_ASSOC @ Y0 )
& ( cGRP_DIVISORS @ Y0 ) ) ) ),
inference(fool_elimination,[],[f16]) ).
thf(f18,plain,
~ ! [X0: g > g > g] :
( ? [X1: g] : ( cGROUP1 @ X0 @ X1 )
<=> ( cGROUP4 @ X0 ) ),
inference(rectify,[],[f8]) ).
thf(f19,plain,
~ ! [X0: g > g > g] :
( ? [X1: g] :
( ( cGROUP1 @ X0 @ X1 )
= $true )
<=> ( ( cGROUP4 @ X0 )
= $true ) ),
inference(fool_elimination,[],[f18]) ).
thf(f20,plain,
? [X0: g > g > g] :
( ? [X1: g] :
( ( cGROUP1 @ X0 @ X1 )
= $true )
<~> ( ( cGROUP4 @ X0 )
= $true ) ),
inference(ennf_transformation,[],[f19]) ).
thf(f21,plain,
? [X0: g > g > g] :
( ( ( ( cGROUP4 @ X0 )
!= $true )
| ! [X1: g] :
( ( cGROUP1 @ X0 @ X1 )
!= $true ) )
& ( ( ( cGROUP4 @ X0 )
= $true )
| ? [X1: g] :
( ( cGROUP1 @ X0 @ X1 )
= $true ) ) ),
inference(nnf_transformation,[],[f20]) ).
thf(f22,plain,
? [X0: g > g > g] :
( ( ( ( cGROUP4 @ X0 )
!= $true )
| ! [X1: g] :
( ( cGROUP1 @ X0 @ X1 )
!= $true ) )
& ( ( ( cGROUP4 @ X0 )
= $true )
| ? [X2: g] :
( $true
= ( cGROUP1 @ X0 @ X2 ) ) ) ),
inference(rectify,[],[f21]) ).
thf(f23,plain,
( ( ( $true
!= ( cGROUP4 @ sK0 ) )
| ! [X1: g] :
( $true
!= ( cGROUP1 @ sK0 @ X1 ) ) )
& ( ( $true
= ( cGROUP4 @ sK0 ) )
| ( $true
= ( cGROUP1 @ sK0 @ sK1 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X2,sK1)],[f22]) ).
thf(f24,plain,
( cGRP_ASSOC
= ( ^ [Y0: g > g > g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( ( Y0 @ ( Y0 @ Y3 @ Y2 ) @ Y1 )
= ( Y0 @ Y3 @ ( Y0 @ Y2 @ Y1 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f25,plain,
( cGRP_DIVISORS
= ( ^ [Y0: g > g > g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( ?? @ g
@ ^ [Y3: g] :
( ( Y0 @ Y2 @ Y3 )
= Y1 ) )
& ( ?? @ g
@ ^ [Y3: g] :
( ( Y0 @ Y3 @ Y2 )
= Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f11]) ).
thf(f26,plain,
( cGRP_INVERSE
= ( ^ [Y0: g > g > g,Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ?? @ g
@ ^ [Y3: g] :
( ( ( Y0 @ Y2 @ Y3 )
= Y1 )
& ( ( Y0 @ Y3 @ Y2 )
= Y1 ) ) ) ) ) ),
inference(cnf_transformation,[],[f12]) ).
thf(f27,plain,
( cGRP_UNIT
= ( ^ [Y0: g > g > g,Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( ( Y0 @ Y1 @ Y2 )
= Y2 )
& ( ( Y0 @ Y2 @ Y1 )
= Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f13]) ).
thf(f28,plain,
( cGROUP1
= ( ^ [Y0: g > g > g,Y1: g] :
( ( cGRP_ASSOC @ Y0 )
& ( cGRP_UNIT @ Y0 @ Y1 )
& ( cGRP_INVERSE @ Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f15]) ).
thf(f29,plain,
( cGROUP4
= ( ^ [Y0: g > g > g] :
( ( cGRP_ASSOC @ Y0 )
& ( cGRP_DIVISORS @ Y0 ) ) ) ),
inference(cnf_transformation,[],[f17]) ).
thf(f30,plain,
( ( $true
= ( cGROUP4 @ sK0 ) )
| ( $true
= ( cGROUP1 @ sK0 @ sK1 ) ) ),
inference(cnf_transformation,[],[f23]) ).
thf(f31,plain,
! [X1: g] :
( ( $true
!= ( cGROUP4 @ sK0 ) )
| ( $true
!= ( cGROUP1 @ sK0 @ X1 ) ) ),
inference(cnf_transformation,[],[f23]) ).
thf(f34,plain,
( cGROUP1
= ( ^ [Y0: g > g > g,Y1: g] :
( ( ^ [Y2: g > g > g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( !! @ g
@ ^ [Y5: g] :
( ( Y2 @ ( Y2 @ Y5 @ Y4 ) @ Y3 )
= ( Y2 @ Y5 @ ( Y2 @ Y4 @ Y3 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( ( Y2 @ Y3 @ Y4 )
= Y4 )
& ( ( Y2 @ Y4 @ Y3 )
= Y4 ) ) )
@ Y0
@ Y1 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ?? @ g
@ ^ [Y5: g] :
( ( ( Y2 @ Y4 @ Y5 )
= Y3 )
& ( ( Y2 @ Y5 @ Y4 )
= Y3 ) ) ) )
@ Y0
@ Y1 ) ) ) ),
inference(definition_unfolding,[],[f28,f24,f27,f26]) ).
thf(f35,plain,
( cGROUP4
= ( ^ [Y0: g > g > g] :
( ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( Y1 @ ( Y1 @ Y4 @ Y3 ) @ Y2 )
= ( Y1 @ Y4 @ ( Y1 @ Y3 @ Y2 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y3 @ Y4 )
= Y2 ) )
& ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y4 @ Y3 )
= Y2 ) ) ) ) )
@ Y0 ) ) ) ),
inference(definition_unfolding,[],[f29,f24,f25]) ).
thf(f36,plain,
! [X1: g] :
( ( $true
!= ( ^ [Y0: g > g > g] :
( ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( Y1 @ ( Y1 @ Y4 @ Y3 ) @ Y2 )
= ( Y1 @ Y4 @ ( Y1 @ Y3 @ Y2 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y3 @ Y4 )
= Y2 ) )
& ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y4 @ Y3 )
= Y2 ) ) ) ) )
@ Y0 ) )
@ sK0 ) )
| ( $true
!= ( ^ [Y0: g > g > g,Y1: g] :
( ( ^ [Y2: g > g > g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( !! @ g
@ ^ [Y5: g] :
( ( Y2 @ ( Y2 @ Y5 @ Y4 ) @ Y3 )
= ( Y2 @ Y5 @ ( Y2 @ Y4 @ Y3 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( ( Y2 @ Y3 @ Y4 )
= Y4 )
& ( ( Y2 @ Y4 @ Y3 )
= Y4 ) ) )
@ Y0
@ Y1 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ?? @ g
@ ^ [Y5: g] :
( ( ( Y2 @ Y4 @ Y5 )
= Y3 )
& ( ( Y2 @ Y5 @ Y4 )
= Y3 ) ) ) )
@ Y0
@ Y1 ) )
@ sK0
@ X1 ) ) ),
inference(definition_unfolding,[],[f31,f35,f34]) ).
thf(f37,plain,
( ( $true
= ( ^ [Y0: g > g > g] :
( ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( Y1 @ ( Y1 @ Y4 @ Y3 ) @ Y2 )
= ( Y1 @ Y4 @ ( Y1 @ Y3 @ Y2 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y1: g > g > g] :
( !! @ g
@ ^ [Y2: g] :
( !! @ g
@ ^ [Y3: g] :
( ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y3 @ Y4 )
= Y2 ) )
& ( ?? @ g
@ ^ [Y4: g] :
( ( Y1 @ Y4 @ Y3 )
= Y2 ) ) ) ) )
@ Y0 ) )
@ sK0 ) )
| ( $true
= ( ^ [Y0: g > g > g,Y1: g] :
( ( ^ [Y2: g > g > g] :
( !! @ g
@ ^ [Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( !! @ g
@ ^ [Y5: g] :
( ( Y2 @ ( Y2 @ Y5 @ Y4 ) @ Y3 )
= ( Y2 @ Y5 @ ( Y2 @ Y4 @ Y3 ) ) ) ) ) )
@ Y0 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ( ( Y2 @ Y3 @ Y4 )
= Y4 )
& ( ( Y2 @ Y4 @ Y3 )
= Y4 ) ) )
@ Y0
@ Y1 )
& ( ^ [Y2: g > g > g,Y3: g] :
( !! @ g
@ ^ [Y4: g] :
( ?? @ g
@ ^ [Y5: g] :
( ( ( Y2 @ Y4 @ Y5 )
= Y3 )
& ( ( Y2 @ Y5 @ Y4 )
= Y3 ) ) ) )
@ Y0
@ Y1 ) )
@ sK0
@ sK1 ) ) ),
inference(definition_unfolding,[],[f30,f35,f34]) ).
thf(f38,plain,
( ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) ) ) ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f37]) ).
thf(f39,plain,
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) ) ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f38]) ).
thf(f40,plain,
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f38]) ).
thf(f41,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ X1 ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f40]) ).
thf(f43,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ X1 ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f41]) ).
thf(f45,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ X1 ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f43]) ).
thf(f46,plain,
! [X2: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f45]) ).
thf(f47,plain,
! [X2: g,X1: g] :
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X1 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X1 ) ) ) ) ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X2 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X2 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f46]) ).
thf(f48,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X1 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X1 ) ) ) )
@ X3 ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X2 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X2 ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f47]) ).
thf(f49,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X1 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X1 ) ) ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ X2 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ X2 ) ) ) )
@ X4 ) ) ),
inference(pi_proxy_clausification,[],[f48]) ).
thf(f50,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X3 ) @ X1 )
= ( sK0 @ Y0 @ ( sK0 @ X3 @ X1 ) ) ) ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X4 ) @ X2 )
= ( sK0 @ Y0 @ ( sK0 @ X4 @ X2 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f49]) ).
thf(f51,plain,
! [X2: g,X3: g,X1: g,X4: g,X5: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X3 ) @ X1 )
= ( sK0 @ Y0 @ ( sK0 @ X3 @ X1 ) ) )
@ X5 ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X4 ) @ X2 )
= ( sK0 @ Y0 @ ( sK0 @ X4 @ X2 ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f50]) ).
thf(f52,plain,
! [X2: g,X3: g,X1: g,X6: g,X4: g,X5: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X3 ) @ X1 )
= ( sK0 @ Y0 @ ( sK0 @ X3 @ X1 ) ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ X4 ) @ X2 )
= ( sK0 @ Y0 @ ( sK0 @ X4 @ X2 ) ) )
@ X6 ) ) ),
inference(pi_proxy_clausification,[],[f51]) ).
thf(f53,plain,
! [X2: g,X3: g,X1: g,X6: g,X4: g,X5: g] :
( ( $true
= ( ( sK0 @ ( sK0 @ X5 @ X3 ) @ X1 )
= ( sK0 @ X5 @ ( sK0 @ X3 @ X1 ) ) ) )
| ( $true
= ( ( sK0 @ ( sK0 @ X6 @ X4 ) @ X2 )
= ( sK0 @ X6 @ ( sK0 @ X4 @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f52]) ).
thf(f54,plain,
! [X2: g,X3: g,X1: g,X6: g,X4: g,X5: g] :
( ( ( sK0 @ ( sK0 @ X5 @ X3 ) @ X1 )
= ( sK0 @ X5 @ ( sK0 @ X3 @ X1 ) ) )
| ( $true
= ( ( sK0 @ ( sK0 @ X6 @ X4 ) @ X2 )
= ( sK0 @ X6 @ ( sK0 @ X4 @ X2 ) ) ) ) ),
inference(equality_proxy_clausification,[],[f53]) ).
thf(f55,plain,
! [X2: g,X3: g,X1: g,X6: g,X4: g,X5: g] :
( ( ( sK0 @ ( sK0 @ X5 @ X3 ) @ X1 )
= ( sK0 @ X5 @ ( sK0 @ X3 @ X1 ) ) )
| ( ( sK0 @ ( sK0 @ X6 @ X4 ) @ X2 )
= ( sK0 @ X6 @ ( sK0 @ X4 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f54]) ).
thf(f85,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f39]) ).
thf(f86,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f85]) ).
thf(f87,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f85]) ).
thf(f88,plain,
! [X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) ) ) ) ),
inference(and_proxy_clausification,[],[f87]) ).
thf(f107,plain,
! [X2: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: g] :
( ( ( sK0 @ sK1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ sK1 )
= Y0 ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f88]) ).
thf(f108,plain,
! [X2: g,X1: g] :
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) )
| ( $true
= ( ( ( sK0 @ sK1 @ X2 )
= X2 )
& ( ( sK0 @ X2 @ sK1 )
= X2 ) ) ) ),
inference(beta-eta_normalization,[],[f107]) ).
thf(f109,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( $true
= ( ( ( sK0 @ sK1 @ X2 )
= X2 )
& ( ( sK0 @ X2 @ sK1 )
= X2 ) ) ) ),
inference(pi_proxy_clausification,[],[f108]) ).
thf(f110,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( $true
= ( ( sK0 @ X2 @ sK1 )
= X2 ) ) ),
inference(and_proxy_clausification,[],[f109]) ).
thf(f111,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( $true
= ( ( sK0 @ sK1 @ X2 )
= X2 ) ) ),
inference(and_proxy_clausification,[],[f109]) ).
thf(f112,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f111]) ).
thf(f113,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) )
& ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(beta-eta_normalization,[],[f112]) ).
thf(f114,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(and_proxy_clausification,[],[f113]) ).
thf(f115,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(and_proxy_clausification,[],[f113]) ).
thf(f116,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK5 @ X3 @ X1 ) ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(sigma_proxy_clausification,[],[f115]) ).
thf(f117,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ X3 @ ( sK5 @ X3 @ X1 ) )
= X1 ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(beta-eta_normalization,[],[f116]) ).
thf(f118,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ X3 @ ( sK5 @ X3 @ X1 ) )
= X1 )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f117]) ).
thf(f119,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK6 @ X3 @ X1 ) ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(sigma_proxy_clausification,[],[f114]) ).
thf(f120,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ ( sK6 @ X3 @ X1 ) @ X3 )
= X1 ) )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(beta-eta_normalization,[],[f119]) ).
thf(f121,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ ( sK6 @ X3 @ X1 ) @ X3 )
= X1 )
| ( ( sK0 @ sK1 @ X2 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f120]) ).
thf(f122,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f110]) ).
thf(f123,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) )
& ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(beta-eta_normalization,[],[f122]) ).
thf(f124,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(and_proxy_clausification,[],[f123]) ).
thf(f125,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(and_proxy_clausification,[],[f123]) ).
thf(f126,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK7 @ X3 @ X1 ) ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(sigma_proxy_clausification,[],[f125]) ).
thf(f127,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ X3 @ ( sK7 @ X3 @ X1 ) )
= X1 ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(beta-eta_normalization,[],[f126]) ).
thf(f128,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ X3 @ ( sK7 @ X3 @ X1 ) )
= X1 )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f127]) ).
thf(f129,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK8 @ X3 @ X1 ) ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(sigma_proxy_clausification,[],[f124]) ).
thf(f130,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ ( sK8 @ X3 @ X1 ) @ X3 )
= X1 ) )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(beta-eta_normalization,[],[f129]) ).
thf(f131,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ ( sK8 @ X3 @ X1 ) @ X3 )
= X1 )
| ( ( sK0 @ X2 @ sK1 )
= X2 ) ),
inference(equality_proxy_clausification,[],[f130]) ).
thf(f132,plain,
! [X2: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= sK1 )
& ( ( sK0 @ Y1 @ Y0 )
= sK1 ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f86]) ).
thf(f133,plain,
! [X2: g,X1: g] :
( ( $true
= ( !! @ g
@ ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) )
| ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X2 @ Y0 )
= sK1 )
& ( ( sK0 @ Y0 @ X2 )
= sK1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f132]) ).
thf(f134,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X2 @ Y0 )
= sK1 )
& ( ( sK0 @ Y0 @ X2 )
= sK1 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f133]) ).
thf(f135,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= X1 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: g] :
( ( ( sK0 @ X2 @ Y0 )
= sK1 )
& ( ( sK0 @ Y0 @ X2 )
= sK1 ) )
@ ( sK9 @ X2 ) ) ) ),
inference(sigma_proxy_clausification,[],[f134]) ).
thf(f136,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) )
& ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) ) )
| ( $true
= ( ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 )
& ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ) ),
inference(beta-eta_normalization,[],[f135]) ).
thf(f137,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 ) ) )
| ( $true
= ( ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 )
& ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ) ),
inference(and_proxy_clausification,[],[f136]) ).
thf(f138,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 ) ) )
| ( $true
= ( ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 )
& ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ) ),
inference(and_proxy_clausification,[],[f136]) ).
thf(f139,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK10 @ X3 @ X1 ) ) )
| ( $true
= ( ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 )
& ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f138]) ).
thf(f140,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK10 @ X3 @ X1 ) ) )
| ( $true
= ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ),
inference(and_proxy_clausification,[],[f139]) ).
thf(f141,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK10 @ X3 @ X1 ) ) )
| ( $true
= ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 ) ) ),
inference(and_proxy_clausification,[],[f139]) ).
thf(f142,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK10 @ X3 @ X1 ) ) )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f141]) ).
thf(f143,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 ) )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(beta-eta_normalization,[],[f142]) ).
thf(f144,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f143]) ).
thf(f145,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ X3 @ Y0 )
= X1 )
@ ( sK10 @ X3 @ X1 ) ) )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(equality_proxy_clausification,[],[f140]) ).
thf(f146,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 ) )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(beta-eta_normalization,[],[f145]) ).
thf(f147,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(equality_proxy_clausification,[],[f146]) ).
thf(f148,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK11 @ X3 @ X1 ) ) )
| ( $true
= ( ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 )
& ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f137]) ).
thf(f149,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK11 @ X3 @ X1 ) ) )
| ( $true
= ( ( sK0 @ ( sK9 @ X2 ) @ X2 )
= sK1 ) ) ),
inference(and_proxy_clausification,[],[f148]) ).
thf(f150,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK11 @ X3 @ X1 ) ) )
| ( $true
= ( ( sK0 @ X2 @ ( sK9 @ X2 ) )
= sK1 ) ) ),
inference(and_proxy_clausification,[],[f148]) ).
thf(f151,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK11 @ X3 @ X1 ) ) )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f150]) ).
thf(f152,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 ) )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(beta-eta_normalization,[],[f151]) ).
thf(f153,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 )
| ( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
inference(equality_proxy_clausification,[],[f152]) ).
thf(f154,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ X3 )
= X1 )
@ ( sK11 @ X3 @ X1 ) ) )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(equality_proxy_clausification,[],[f149]) ).
thf(f155,plain,
! [X2: g,X3: g,X1: g] :
( ( $true
= ( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 ) )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(beta-eta_normalization,[],[f154]) ).
thf(f156,plain,
! [X2: g,X3: g,X1: g] :
( ( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 )
| ( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
inference(equality_proxy_clausification,[],[f155]) ).
thf(f157,plain,
! [X1: g] :
( ( $true
!= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) ) ) ) )
| ( $true
!= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f36]) ).
thf(f158,plain,
! [X1: g] :
( ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) ) ) )
| ( $true
!= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f157]) ).
thf(f159,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $true
!= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f158]) ).
thf(f160,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) )
| ( $false
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f159]) ).
thf(f161,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) )
| ( $false
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f160]) ).
thf(f162,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ sK14 ) )
| ( $false
= ( ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) )
& ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f161]) ).
thf(f163,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ sK14 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f162]) ).
thf(f164,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ sK14 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) )
@ ( sK15 @ X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f163]) ).
thf(f165,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y1 @ Y2 )
= Y0 ) )
& ( ?? @ g
@ ^ [Y2: g] :
( ( sK0 @ Y2 @ Y1 )
= Y0 ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: g] :
( ?? @ g
@ ^ [Y1: g] :
( ( ( sK0 @ Y0 @ Y1 )
= X1 )
& ( ( sK0 @ Y1 @ Y0 )
= X1 ) ) )
@ ( sK13 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ sK14 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ X1 @ Y0 )
= Y0 )
& ( ( sK0 @ Y0 @ X1 )
= Y0 ) )
@ ( sK15 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( !! @ g
@ ^ [Y2: g] :
( ( sK0 @ ( sK0 @ Y2 @ Y1 ) @ Y0 )
= ( sK0 @ Y2 @ ( sK0 @ Y1 @ Y0 ) ) ) ) )
@ sK16 ) ) ),
inference(sigma_proxy_clausification,[],[f164]) ).
thf(f166,plain,
! [X1: g] :
( ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) ) ) )
| ( $false
= ( ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) )
& ( ( sK0 @ ( sK15 @ X1 ) @ X1 )
= ( sK15 @ X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f165]) ).
thf(f167,plain,
! [X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) ) ) )
| ( $false
= ( ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) )
& ( ( sK0 @ ( sK15 @ X1 ) @ X1 )
= ( sK15 @ X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f166]) ).
thf(f168,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) ) ) )
| ( $false
= ( ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) )
& ( ( sK0 @ ( sK15 @ X1 ) @ X1 )
= ( sK15 @ X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f167]) ).
thf(f169,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) )
@ sK18 ) )
| ( $false
= ( ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) )
& ( ( sK0 @ ( sK15 @ X1 ) @ X1 )
= ( sK15 @ X1 ) ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f168]) ).
thf(f170,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) )
@ sK18 ) )
| ( $false
= ( ( sK0 @ ( sK15 @ X1 ) @ X1 )
= ( sK15 @ X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) )
| ( $false
= ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) ) ) ),
inference(and_proxy_clausification,[],[f169]) ).
thf(f171,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) )
@ sK18 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) ) ) )
| ( $false
= ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) ) ) ),
inference(equality_proxy_clausification,[],[f170]) ).
thf(f172,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) )
@ sK18 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) )
@ sK19 ) )
| ( $false
= ( ( sK0 @ X1 @ ( sK15 @ X1 ) )
= ( sK15 @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f171]) ).
thf(f173,plain,
! [X2: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y0 @ Y1 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y1: g] :
( ( sK0 @ Y1 @ Y0 )
= sK12 ) ) )
@ sK17 ) )
| ( $false
= ( ^ [Y0: g] :
( ( ( sK0 @ ( sK13 @ X1 ) @ Y0 )
= X1 )
& ( ( sK0 @ Y0 @ ( sK13 @ X1 ) )
= X1 ) )
@ X2 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK14 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK14 ) ) ) )
@ sK18 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ^ [Y0: g] :
( !! @ g
@ ^ [Y1: g] :
( ( sK0 @ ( sK0 @ Y1 @ Y0 ) @ sK16 )
= ( sK0 @ Y1 @ ( sK0 @ Y0 @ sK16 ) ) ) )
@ sK19 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) ) ),
inference(equality_proxy_clausification,[],[f172]) ).
thf(f174,plain,
! [X2: g,X1: g] :
( ( $false
= ( ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) )
& ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 ) ) ) )
| ( $false
= ( ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 )
& ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
= X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f173]) ).
thf(f175,plain,
! [X2: g,X1: g] :
( ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 ) ) )
| ( $false
= ( ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 )
& ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
= X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) ) ),
inference(and_proxy_clausification,[],[f174]) ).
thf(f176,plain,
! [X2: g,X3: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( $false
= ( ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 )
& ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
= X1 ) ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) ) ),
inference(pi_proxy_clausification,[],[f175]) ).
thf(f177,plain,
! [X2: g,X3: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( $false
= ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
= X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) )
| ( $false
= ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 ) ) ),
inference(and_proxy_clausification,[],[f176]) ).
thf(f178,plain,
! [X2: g,X3: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) )
| ( $false
= ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 ) ) ),
inference(equality_proxy_clausification,[],[f177]) ).
thf(f179,plain,
! [X2: g,X3: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) )
@ sK20 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( !! @ g
@ ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) )
| ( $false
= ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 ) ) ),
inference(sigma_proxy_clausification,[],[f178]) ).
thf(f180,plain,
! [X2: g,X3: g,X1: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) )
@ sK20 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) )
@ sK21 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ?? @ g
@ ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 ) ) )
| ( $false
= ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 ) ) ),
inference(sigma_proxy_clausification,[],[f179]) ).
thf(f181,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) )
@ sK20 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) )
@ sK21 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 )
@ X4 ) )
| ( $false
= ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
= X1 ) ) ),
inference(pi_proxy_clausification,[],[f180]) ).
thf(f182,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( $false
= ( ^ [Y0: g] :
( ( sK0 @ Y0 @ sK17 )
= sK12 )
@ X3 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK18 ) @ sK14 )
= ( sK0 @ Y0 @ ( sK0 @ sK18 @ sK14 ) ) )
@ sK20 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ ( sK0 @ Y0 @ sK19 ) @ sK16 )
= ( sK0 @ Y0 @ ( sK0 @ sK19 @ sK16 ) ) )
@ sK21 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ^ [Y0: g] :
( ( sK0 @ sK17 @ Y0 )
= sK12 )
@ X4 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f181]) ).
thf(f183,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( $false
= ( ( sK0 @ X3 @ sK17 )
= sK12 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ( sK0 @ ( sK0 @ sK20 @ sK18 ) @ sK14 )
= ( sK0 @ sK20 @ ( sK0 @ sK18 @ sK14 ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK17 @ X4 )
= sK12 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(beta-eta_normalization,[],[f182]) ).
thf(f184,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( $false
= ( ( sK0 @ ( sK0 @ sK20 @ sK18 ) @ sK14 )
= ( sK0 @ sK20 @ ( sK0 @ sK18 @ sK14 ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK17 @ X4 )
= sK12 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f183]) ).
thf(f185,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK0 @ ( sK0 @ sK20 @ sK18 ) @ sK14 )
!= ( sK0 @ sK20 @ ( sK0 @ sK18 @ sK14 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( $false
= ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK17 @ X4 )
= sK12 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f184]) ).
thf(f186,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK0 @ ( sK0 @ sK20 @ sK18 ) @ sK14 )
!= ( sK0 @ sK20 @ ( sK0 @ sK18 @ sK14 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
!= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( $false
= ( ( sK0 @ sK17 @ X4 )
= sK12 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f185]) ).
thf(f187,plain,
! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK0 @ ( sK0 @ sK20 @ sK18 ) @ sK14 )
!= ( sK0 @ sK20 @ ( sK0 @ sK18 @ sK14 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
!= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( sK12
!= ( sK0 @ sK17 @ X4 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f186]) ).
thf(f198,definition,
( spl22_1
<=> ! [X2: g] :
( ( sK0 @ sK1 @ X2 )
= X2 ) ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
thf(f199,plain,
( ! [X2: g] :
( ( sK0 @ sK1 @ X2 )
= X2 )
| ~ spl22_1 ),
inference(avatar_component_clause,[],[f198]) ).
thf(f201,definition,
( spl22_2
<=> ! [X1: g,X3: g] :
( ( sK0 @ X3 @ ( sK5 @ X3 @ X1 ) )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
thf(f202,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ X3 @ ( sK5 @ X3 @ X1 ) )
= X1 )
| ~ spl22_2 ),
inference(avatar_component_clause,[],[f201]) ).
thf(f203,plain,
( spl22_1
| spl22_2 ),
inference(avatar_split_clause,[],[f118,f201,f198]) ).
thf(f205,definition,
( spl22_3
<=> ! [X1: g,X3: g] :
( ( sK0 @ ( sK6 @ X3 @ X1 ) @ X3 )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
thf(f206,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ ( sK6 @ X3 @ X1 ) @ X3 )
= X1 )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f205]) ).
thf(f207,plain,
( spl22_1
| spl22_3 ),
inference(avatar_split_clause,[],[f121,f205,f198]) ).
thf(f212,definition,
( spl22_4
<=> ! [X2: g] :
( ( sK0 @ X2 @ sK1 )
= X2 ) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
thf(f213,plain,
( ! [X2: g] :
( ( sK0 @ X2 @ sK1 )
= X2 )
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f212]) ).
thf(f215,definition,
( spl22_5
<=> ! [X1: g,X3: g] :
( ( sK0 @ X3 @ ( sK7 @ X3 @ X1 ) )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
thf(f216,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ X3 @ ( sK7 @ X3 @ X1 ) )
= X1 )
| ~ spl22_5 ),
inference(avatar_component_clause,[],[f215]) ).
thf(f217,plain,
( spl22_4
| spl22_5 ),
inference(avatar_split_clause,[],[f128,f215,f212]) ).
thf(f219,definition,
( spl22_6
<=> ! [X2: g] :
( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
thf(f220,plain,
( ! [X2: g] :
( sK1
= ( sK0 @ X2 @ ( sK9 @ X2 ) ) )
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f219]) ).
thf(f222,definition,
( spl22_7
<=> ! [X1: g,X3: g] :
( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
thf(f223,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ X3 @ ( sK10 @ X3 @ X1 ) )
= X1 )
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f222]) ).
thf(f224,plain,
( spl22_6
| spl22_7 ),
inference(avatar_split_clause,[],[f144,f222,f219]) ).
thf(f229,definition,
( spl22_8
<=> ! [X2: g] :
( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) ) ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
thf(f230,plain,
( ! [X2: g] :
( sK1
= ( sK0 @ ( sK9 @ X2 ) @ X2 ) )
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f229]) ).
thf(f231,plain,
( spl22_8
| spl22_7 ),
inference(avatar_split_clause,[],[f147,f222,f229]) ).
thf(f236,definition,
( spl22_9
<=> ! [X1: g,X3: g] :
( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
thf(f237,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ ( sK11 @ X3 @ X1 ) @ X3 )
= X1 )
| ~ spl22_9 ),
inference(avatar_component_clause,[],[f236]) ).
thf(f238,plain,
( spl22_8
| spl22_9 ),
inference(avatar_split_clause,[],[f156,f236,f229]) ).
thf(f246,definition,
( spl22_11
<=> ! [X4: g,X1: g,X3: g] :
( ( sK0 @ ( sK0 @ X4 @ X3 ) @ X1 )
= ( sK0 @ X4 @ ( sK0 @ X3 @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
thf(f247,plain,
( ! [X3: g,X1: g,X4: g] :
( ( sK0 @ ( sK0 @ X4 @ X3 ) @ X1 )
= ( sK0 @ X4 @ ( sK0 @ X3 @ X1 ) ) )
| ~ spl22_11 ),
inference(avatar_component_clause,[],[f246]) ).
thf(f256,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK0 @ ( sK5 @ X1 @ X0 ) @ X2 ) )
= ( sK0 @ X0 @ X2 ) )
| ~ spl22_2
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f202]) ).
thf(f257,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X2 )
= ( sK0 @ X1 @ ( sK0 @ ( sK10 @ X1 @ X0 ) @ X2 ) ) )
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f223]) ).
thf(f258,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) )
= ( sK0 @ sK1 @ X1 ) )
| ~ spl22_6
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f220]) ).
thf(f262,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ sK1 @ X1 )
= ( sK0 @ ( sK9 @ X0 ) @ ( sK0 @ X0 @ X1 ) ) )
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f230]) ).
thf(f265,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK0 @ X2 @ ( sK10 @ ( sK0 @ X1 @ X2 ) @ X0 ) ) )
= X0 )
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f223]) ).
thf(f266,plain,
( ! [X0: g,X1: g] :
( sK1
= ( sK0 @ X0 @ ( sK0 @ X1 @ ( sK9 @ ( sK0 @ X0 @ X1 ) ) ) ) )
| ~ spl22_6
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f220]) ).
thf(f275,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK9 @ X0 ) @ ( sK0 @ X0 @ X1 ) )
= X1 )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f262,f199]) ).
thf(f277,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) )
= X1 )
| ~ spl22_1
| ~ spl22_6
| ~ spl22_11 ),
inference(forward_demodulation,[],[f258,f199]) ).
thf(f316,plain,
( ! [X0: g] :
( ( sK0 @ ( sK9 @ ( sK9 @ X0 ) ) @ sK1 )
= X0 )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f275,f230]) ).
thf(f510,plain,
( ! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( ( sK0 @ ( sK0 @ sK21 @ sK19 ) @ sK16 )
!= ( sK0 @ sK21 @ ( sK0 @ sK19 @ sK16 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( sK12
!= ( sK0 @ sK17 @ X4 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) )
| ~ spl22_11 ),
inference(forward_subsumption_resolution,[],[f187,f247]) ).
thf(f511,plain,
( ! [X2: g,X3: g,X1: g,X4: g] :
( ( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( sK12
!= ( sK0 @ sK17 @ X4 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 ) )
| ~ spl22_11 ),
inference(forward_subsumption_resolution,[],[f510,f247]) ).
thf(f678,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ sK1 )
= ( sK0 @ X1 @ ( sK9 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) ) )
| ~ spl22_1
| ~ spl22_6
| ~ spl22_11 ),
inference(constrained_superposition,[],[f277,f266]) ).
thf(f689,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK9 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) )
= X0 )
| ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_11 ),
inference(forward_demodulation,[],[f678,f213]) ).
thf(f903,plain,
( ! [X0: g] :
( sK1
= ( sK0 @ ( sK9 @ X0 ) @ X0 ) )
| ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_11 ),
inference(constrained_superposition,[],[f266,f689]) ).
thf(f2025,definition,
( spl22_13
<=> ! [X4: g] :
( sK12
!= ( sK0 @ sK17 @ X4 ) ) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
thf(f2026,plain,
( ! [X4: g] :
( sK12
!= ( sK0 @ sK17 @ X4 ) )
| ~ spl22_13 ),
inference(avatar_component_clause,[],[f2025]) ).
thf(f2028,definition,
( spl22_14
<=> ! [X2: g,X1: g] :
( ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
thf(f2029,plain,
( ! [X2: g,X1: g] :
( ( ( sK15 @ X1 )
!= ( sK0 @ ( sK15 @ X1 ) @ X1 ) )
| ( ( sK0 @ ( sK13 @ X1 ) @ X2 )
!= X1 )
| ( ( sK15 @ X1 )
!= ( sK0 @ X1 @ ( sK15 @ X1 ) ) )
| ( ( sK0 @ X2 @ ( sK13 @ X1 ) )
!= X1 ) )
| ~ spl22_14 ),
inference(avatar_component_clause,[],[f2028]) ).
thf(f2031,definition,
( spl22_15
<=> ! [X3: g] :
( sK12
!= ( sK0 @ X3 @ sK17 ) ) ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
thf(f2032,plain,
( ! [X3: g] :
( sK12
!= ( sK0 @ X3 @ sK17 ) )
| ~ spl22_15 ),
inference(avatar_component_clause,[],[f2031]) ).
thf(f2033,plain,
( spl22_13
| spl22_14
| spl22_15
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f511,f246,f2031,f2028,f2025]) ).
thf(f2105,plain,
( $false
| ~ spl22_2
| ~ spl22_13 ),
inference(unit_resulting_resolution,[],[f2026,f202]) ).
thf(f2107,plain,
( ! [X0: g] : ( sK12 != X0 )
| ~ spl22_7
| ~ spl22_13 ),
inference(constrained_superposition,[],[f2026,f223]) ).
thf(f2111,plain,
( ~ spl22_2
| ~ spl22_13 ),
inference(avatar_contradiction_clause,[],[f2105]) ).
thf(f2238,plain,
( ( sK1
!= ( sK0 @ ( sK9 @ ( sK13 @ sK1 ) ) @ ( sK13 @ sK1 ) ) )
| ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_14 ),
inference(unit_resulting_resolution,[],[f2029,f220,f199,f213]) ).
thf(f2262,plain,
( $false
| ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_8
| ~ spl22_14 ),
inference(forward_subsumption_resolution,[],[f2238,f230]) ).
thf(f2263,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_8
| ~ spl22_14 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
thf(f2442,plain,
( ! [X0: g] :
( sK1
= ( sK0 @ ( sK9 @ ( sK9 @ ( sK9 @ X0 ) ) ) @ X0 ) )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f275,f316]) ).
thf(f2469,plain,
( ! [X0: g] :
( ( sK0 @ ( sK9 @ ( sK9 @ ( sK9 @ ( sK9 @ X0 ) ) ) ) @ sK1 )
= X0 )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f275,f2442]) ).
thf(f2471,plain,
( ! [X0: g] :
( ( sK9 @ ( sK9 @ X0 ) )
= X0 )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f2469,f316]) ).
thf(f2478,plain,
( ! [X0: g] :
( ( sK0 @ X0 @ sK1 )
= X0 )
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f316,f2471]) ).
thf(f2481,plain,
( spl22_4
| ~ spl22_1
| ~ spl22_8
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f2478,f246,f229,f198,f212]) ).
thf(f2483,definition,
( spl22_17
<=> ! [X1: g,X3: g] :
( ( sK0 @ ( sK8 @ X3 @ X1 ) @ X3 )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
thf(f2484,plain,
( ! [X3: g,X1: g] :
( ( sK0 @ ( sK8 @ X3 @ X1 ) @ X3 )
= X1 )
| ~ spl22_17 ),
inference(avatar_component_clause,[],[f2483]) ).
thf(f2485,plain,
( spl22_4
| spl22_17 ),
inference(avatar_split_clause,[],[f131,f2483,f212]) ).
thf(f2489,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X2 )
= ( sK0 @ ( sK11 @ X1 @ X0 ) @ ( sK0 @ X1 @ X2 ) ) )
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f237]) ).
thf(f2490,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X2 )
= ( sK0 @ ( sK8 @ X1 @ X0 ) @ ( sK0 @ X1 @ X2 ) ) )
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f247,f2484]) ).
thf(f2492,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK0 @ X2 @ ( sK7 @ ( sK0 @ X1 @ X2 ) @ X0 ) ) )
= X0 )
| ~ spl22_5
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f216]) ).
thf(f2500,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X2 @ X0 )
= ( sK0 @ X1 @ ( sK10 @ ( sK10 @ X2 @ X1 ) @ X0 ) ) )
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f257,f223]) ).
thf(f2685,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK7 @ X2 @ X0 ) )
= ( sK0 @ ( sK11 @ X2 @ X1 ) @ X0 ) )
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2489,f216]) ).
thf(f2686,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK11 @ X2 @ X1 ) @ X0 )
= ( sK0 @ X1 @ ( sK10 @ X2 @ X0 ) ) )
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2489,f223]) ).
thf(f2690,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ X0 )
= ( sK0 @ ( sK11 @ sK1 @ X1 ) @ X0 ) )
| ~ spl22_1
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2489,f199]) ).
thf(f2692,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ X2 )
= ( sK0 @ ( sK11 @ ( sK8 @ X2 @ X0 ) @ X1 ) @ X0 ) )
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f2489,f2484]) ).
thf(f2727,plain,
( ! [X0: g] :
( ( sK0 @ X0 @ sK1 )
= X0 )
| ~ spl22_1
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2690,f237]) ).
thf(f2754,plain,
( spl22_4
| ~ spl22_1
| ~ spl22_9
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f2727,f246,f236,f198,f212]) ).
thf(f2756,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK11 @ X2 @ X1 ) @ X0 )
= ( sK0 @ X1 @ ( sK5 @ X2 @ X0 ) ) )
| ~ spl22_2
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2489,f202]) ).
thf(f2761,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ X2 )
= ( sK0 @ ( sK11 @ ( sK6 @ X2 @ X0 ) @ X1 ) @ X0 ) )
| ~ spl22_3
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2489,f206]) ).
thf(f2762,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X1 @ X0 ) @ ( sK0 @ X1 @ ( sK10 @ X0 @ X2 ) ) )
= X2 )
| ~ spl22_3
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f265,f206]) ).
thf(f2763,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X2 )
= ( sK0 @ ( sK6 @ X1 @ X0 ) @ ( sK0 @ X1 @ X2 ) ) )
| ~ spl22_3
| ~ spl22_11 ),
inference(constrained_superposition,[],[f247,f206]) ).
thf(f2766,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ X0 )
= ( sK0 @ X2 @ ( sK5 @ ( sK5 @ X1 @ X2 ) @ X0 ) ) )
| ~ spl22_2
| ~ spl22_11 ),
inference(constrained_superposition,[],[f256,f202]) ).
thf(f2864,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK5 @ X2 @ X0 ) )
= ( sK0 @ ( sK8 @ X2 @ X1 ) @ X0 ) )
| ~ spl22_2
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f2490,f202]) ).
thf(f3002,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK7 @ X1 @ X1 ) )
= X0 )
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2685,f237]) ).
thf(f3003,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X1 )
= ( sK0 @ X0 @ ( sK7 @ X2 @ ( sK0 @ X2 @ X1 ) ) ) )
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2685,f2489]) ).
thf(f3041,plain,
( ! [X0: g,X1: g] :
( ( sK6 @ ( sK7 @ X1 @ X1 ) @ X0 )
= X0 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3002,f206]) ).
thf(f3072,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK7 @ X2 @ X0 ) )
= ( sK0 @ X1 @ ( sK10 @ X2 @ X0 ) ) )
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f2686,f2685]) ).
thf(f3074,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ X2 )
= ( sK0 @ X1 @ ( sK7 @ ( sK8 @ X2 @ X0 ) @ X0 ) ) )
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f2692,f2685]) ).
thf(f3088,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X1 @ X1 ) )
= X0 )
| ~ spl22_2
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2756,f237]) ).
thf(f3129,plain,
( ! [X0: g,X1: g] :
( ( sK6 @ ( sK5 @ X1 @ X1 ) @ X0 )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3088,f206]) ).
thf(f3131,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK11 @ X1 @ X0 )
= ( sK0 @ X0 @ ( sK5 @ X1 @ ( sK5 @ X2 @ X2 ) ) ) )
| ~ spl22_2
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3088,f2756]) ).
thf(f3182,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ X2 )
= ( sK0 @ X1 @ ( sK7 @ ( sK6 @ X2 @ X0 ) @ X0 ) ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f2761,f2685]) ).
thf(f3183,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X1 @ X1 ) @ X0 )
= X0 )
| ~ spl22_3
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2762,f223]) ).
thf(f3184,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X2 @ ( sK10 @ X0 @ X2 ) ) @ ( sK0 @ X0 @ X1 ) )
= X1 )
| ~ spl22_3
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2762,f2500]) ).
thf(f3204,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK7 @ X0 @ X0 ) @ X1 )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3041]) ).
thf(f3205,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK5 @ X0 @ X0 ) @ X1 )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3129]) ).
thf(f3206,plain,
( ! [X0: g,X1: g] :
( ( sK7 @ ( sK6 @ X1 @ X1 ) @ X0 )
= X0 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f216]) ).
thf(f3210,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ X1 @ X1 )
= ( sK6 @ X0 @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3088]) ).
thf(f3263,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK6 @ X0 @ X0 ) )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3002,f3206]) ).
thf(f3310,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ X0 @ X0 )
= ( sK5 @ X1 @ X1 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3210,f3129]) ).
thf(f3822,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK5 @ X2 @ X0 ) )
= ( sK0 @ ( sK6 @ X2 @ X1 ) @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2763,f202]) ).
thf(f3916,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK10 @ X1 @ X2 )
= ( sK0 @ ( sK6 @ X0 @ X0 ) @ ( sK7 @ X1 @ X2 ) ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3072]) ).
thf(f3933,plain,
( ! [X2: g,X1: g] :
( ( sK7 @ X1 @ X2 )
= ( sK10 @ X1 @ X2 ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f3916,f3183]) ).
thf(f4053,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X0 @ X0 ) @ X1 )
= ( sK7 @ ( sK8 @ X1 @ X2 ) @ X2 ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f3183,f3074]) ).
thf(f4070,plain,
( ! [X2: g,X1: g] :
( ( sK7 @ ( sK8 @ X1 @ X2 ) @ X2 )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f4053,f3183]) ).
thf(f4121,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X0 @ X0 ) @ X1 )
= ( sK7 @ ( sK6 @ X1 @ X2 ) @ X2 ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3182]) ).
thf(f4138,plain,
( ! [X2: g,X1: g] :
( ( sK7 @ ( sK6 @ X1 @ X2 ) @ X2 )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f4121,f3183]) ).
thf(f4226,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ X2 )
= ( sK5 @ ( sK5 @ X0 @ ( sK6 @ X1 @ X1 ) ) @ X2 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2766,f3183]) ).
thf(f4488,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X1 @ X1 ) )
= X0 )
| ~ spl22_2
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f2864,f2484]) ).
thf(f5232,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK7 @ X2 @ ( sK0 @ X2 @ X1 ) )
= ( sK0 @ ( sK6 @ X0 @ X0 ) @ X1 ) )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3183,f3003]) ).
thf(f5253,plain,
( ! [X2: g,X1: g] :
( ( sK7 @ X2 @ ( sK0 @ X2 @ X1 ) )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f5232,f3183]) ).
thf(f5289,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ X1 @ X0 )
= ( sK7 @ X1 @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5253,f202]) ).
thf(f5295,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK5 @ X2 @ X0 ) @ X1 )
= ( sK7 @ X2 @ ( sK0 @ X0 @ X1 ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5253,f256]) ).
thf(f5366,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ ( sK8 @ X0 @ X1 ) @ X1 )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f5289,f4070]) ).
thf(f5367,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ ( sK6 @ X0 @ X1 ) @ X1 )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5289,f4138]) ).
thf(f5373,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ X1 @ ( sK0 @ X1 @ X0 ) )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5289,f5253]) ).
thf(f5666,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X2 @ ( sK7 @ X0 @ X2 ) ) @ ( sK0 @ X0 @ X1 ) )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f3184,f3933]) ).
thf(f5667,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X2 @ ( sK5 @ X0 @ X2 ) ) @ ( sK0 @ X0 @ X1 ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f5666,f5289]) ).
thf(f5688,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK5 @ X2 @ ( sK5 @ ( sK6 @ X2 @ X1 ) @ X0 ) ) )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3822,f202]) ).
thf(f5928,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ ( sK5 @ X0 @ X2 ) @ ( sK5 @ X2 @ ( sK0 @ X0 @ X1 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f5667,f3822]) ).
thf(f6017,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK5 @ X2 @ ( sK0 @ X1 @ X0 ) )
= ( sK7 @ ( sK5 @ X1 @ X2 ) @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5253,f5928]) ).
thf(f6021,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK5 @ X2 @ ( sK0 @ X1 @ X0 ) )
= ( sK5 @ ( sK5 @ X1 @ X2 ) @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f6017,f5289]) ).
thf(f6178,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X2 @ X2 ) )
= ( sK11 @ ( sK5 @ X0 @ X1 ) @ X1 ) )
| ~ spl22_2
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2766,f3131]) ).
thf(f6223,plain,
( ! [X0: g,X1: g] :
( ( sK11 @ ( sK5 @ X0 @ X1 ) @ X1 )
= X0 )
| ~ spl22_2
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f6178,f3088]) ).
thf(f6290,plain,
( ! [X0: g,X1: g] :
( ( sK11 @ X0 @ X1 )
= ( sK8 @ X0 @ X1 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f6223,f5366]) ).
thf(f6291,plain,
( ! [X0: g,X1: g] :
( ( sK11 @ X0 @ X1 )
= ( sK6 @ X0 @ X1 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f6223,f5367]) ).
thf(f6373,plain,
( ! [X0: g,X1: g] :
( ( sK8 @ X0 @ X1 )
= ( sK6 @ X0 @ X1 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f6291,f6290]) ).
thf(f7241,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK11 @ ( sK5 @ X0 @ ( sK6 @ X2 @ X2 ) ) @ X3 )
= ( sK0 @ X3 @ ( sK0 @ X0 @ ( sK5 @ X1 @ X1 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(constrained_superposition,[],[f3131,f4226]) ).
thf(f7244,plain,
( ! [X2: g,X3: g,X0: g] :
( ( sK0 @ X3 @ X0 )
= ( sK11 @ ( sK5 @ X0 @ ( sK6 @ X2 @ X2 ) ) @ X3 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f7241,f3088]) ).
thf(f7295,plain,
( ! [X2: g,X3: g,X0: g] :
( ( sK0 @ X3 @ X0 )
= ( sK8 @ ( sK5 @ X0 @ ( sK6 @ X2 @ X2 ) ) @ X3 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f7244,f6290]) ).
thf(f7310,plain,
( ! [X2: g,X3: g,X0: g] :
( ( sK0 @ X3 @ X0 )
= ( sK6 @ ( sK5 @ X0 @ ( sK6 @ X2 @ X2 ) ) @ X3 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f7295,f6373]) ).
thf(f7759,plain,
( ! [X0: g,X1: g] :
( ( sK5 @ ( sK6 @ X0 @ X0 ) @ X1 )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_11 ),
inference(constrained_superposition,[],[f5688,f202]) ).
thf(f8579,plain,
( ! [X2: g,X0: g,X1: g] :
( ( sK5 @ X2 @ ( sK0 @ X0 @ X1 ) )
= ( sK0 @ ( sK5 @ X2 @ X0 ) @ X1 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11 ),
inference(forward_demodulation,[],[f5295,f5289]) ).
thf(f10358,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK0 @ ( sK6 @ X3 @ X0 ) @ ( sK6 @ ( sK5 @ ( sK10 @ X0 @ X1 ) @ ( sK6 @ X2 @ X2 ) ) @ X3 ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f2762,f7310]) ).
thf(f10497,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X3 @ ( sK6 @ ( sK5 @ ( sK10 @ X0 @ X1 ) @ ( sK6 @ X2 @ X2 ) ) @ X3 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f10358,f3822]) ).
thf(f10590,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X3 @ ( sK6 @ ( sK5 @ ( sK7 @ X0 @ X1 ) @ ( sK6 @ X2 @ X2 ) ) @ X3 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f10497,f3933]) ).
thf(f10616,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X3 @ ( sK6 @ ( sK5 @ ( sK5 @ X0 @ X1 ) @ ( sK6 @ X2 @ X2 ) ) @ X3 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f10590,f5289]) ).
thf(f10622,plain,
( ! [X2: g,X3: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X3 @ ( sK6 @ ( sK5 @ X1 @ ( sK0 @ X0 @ ( sK6 @ X2 @ X2 ) ) ) @ X3 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f10616,f6021]) ).
thf(f10624,plain,
( ! [X3: g,X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ X3 @ ( sK6 @ ( sK5 @ X1 @ X0 ) @ X3 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_17 ),
inference(forward_demodulation,[],[f10622,f3263]) ).
thf(f31424,plain,
( ! [X0: g,X1: g] :
( ( sK7 @ X0 @ X0 )
!= ( sK0 @ ( sK5 @ X1 @ ( sK6 @ ( sK5 @ ( sK7 @ X0 @ X0 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) @ X1 ) ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(unit_resulting_resolution,[],[f2029,f3002,f3204,f10624]) ).
thf(f31728,plain,
( ! [X0: g,X1: g] :
( ( sK7 @ X0 @ X0 )
!= ( sK5 @ X1 @ ( sK0 @ ( sK6 @ ( sK5 @ ( sK7 @ X0 @ X0 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) @ X1 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31424,f8579]) ).
thf(f31790,plain,
( ! [X0: g,X1: g] :
( ( sK7 @ X0 @ X0 )
!= ( sK5 @ X1 @ ( sK0 @ X1 @ ( sK5 @ ( sK5 @ ( sK7 @ X0 @ X0 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31728,f3822]) ).
thf(f31813,plain,
( ! [X0: g] :
( ( sK7 @ X0 @ X0 )
!= ( sK5 @ ( sK5 @ ( sK7 @ X0 @ X0 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31790,f5373]) ).
thf(f31825,plain,
( ! [X0: g] :
( ( sK7 @ X0 @ X0 )
!= ( sK5 @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) @ ( sK0 @ ( sK7 @ X0 @ X0 ) @ ( sK13 @ ( sK7 @ X0 @ X0 ) ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31813,f6021]) ).
thf(f31830,plain,
( ! [X0: g] :
( ( sK5 @ X0 @ X0 )
!= ( sK5 @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) @ ( sK0 @ ( sK5 @ X0 @ X0 ) @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31825,f5289]) ).
thf(f31833,plain,
( ! [X0: g] :
( ( sK5 @ X0 @ X0 )
!= ( sK5 @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f31830,f3205]) ).
thf(f31838,plain,
( $false
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_subsumption_resolution,[],[f31833,f3310]) ).
thf(f31839,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(avatar_contradiction_clause,[],[f31838]) ).
thf(f31842,plain,
( $false
| ~ spl22_9
| ~ spl22_15 ),
inference(unit_resulting_resolution,[],[f2032,f237]) ).
thf(f31847,plain,
( ! [X0: g] : ( sK12 != X0 )
| ~ spl22_15
| ~ spl22_17 ),
inference(constrained_superposition,[],[f2032,f2484]) ).
thf(f31849,plain,
( ! [X0: g,X1: g] :
( sK12
!= ( sK0 @ X0 @ ( sK0 @ X1 @ sK17 ) ) )
| ~ spl22_11
| ~ spl22_15 ),
inference(constrained_superposition,[],[f2032,f247]) ).
thf(f31860,plain,
( ~ spl22_9
| ~ spl22_15 ),
inference(avatar_contradiction_clause,[],[f31842]) ).
thf(f33338,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ X0 )
= ( sK0 @ X0 @ sK1 ) )
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f258,f230]) ).
thf(f33416,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ ( sK6 @ sK1 @ X0 ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f33338,f206]) ).
thf(f33582,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK9 @ X1 ) @ X0 )
= ( sK0 @ sK1 @ ( sK7 @ X1 @ X0 ) ) )
| ~ spl22_5
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f262,f216]) ).
thf(f33627,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ X0 )
= ( sK0 @ ( sK9 @ ( sK9 @ X0 ) ) @ sK1 ) )
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f262,f230]) ).
thf(f33630,plain,
( ! [X0: g] :
( ( sK0 @ ( sK9 @ sK1 ) @ X0 )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f262,f33416]) ).
thf(f33663,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ X0 )
= ( sK0 @ sK1 @ ( sK9 @ ( sK9 @ X0 ) ) ) )
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f33627,f33338]) ).
thf(f34239,plain,
( ! [X0: g] :
( sK1
= ( sK0 @ sK1 @ ( sK0 @ X0 @ ( sK9 @ ( sK0 @ X0 @ sK1 ) ) ) ) )
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f266,f33338]) ).
thf(f34280,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ sK1 )
= ( sK0 @ sK1 @ ( sK0 @ X1 @ ( sK9 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) ) ) )
| ~ spl22_6
| ~ spl22_11 ),
inference(constrained_superposition,[],[f258,f266]) ).
thf(f38480,plain,
( ! [X0: g] :
( ( sK9 @ sK1 )
= ( sK5 @ X0 @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f4488,f33630]) ).
thf(f38523,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK5 @ X0 @ X0 ) @ X1 )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_17 ),
inference(constrained_superposition,[],[f33630,f38480]) ).
thf(f39375,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK9 @ ( sK9 @ X0 ) ) )
= ( sK0 @ ( sK6 @ sK1 @ X1 ) @ ( sK0 @ sK1 @ X0 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2763,f33663]) ).
thf(f39377,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ X0 )
= ( sK0 @ X1 @ ( sK9 @ ( sK9 @ X0 ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f39375,f2763]) ).
thf(f39416,plain,
( ! [X0: g] :
( ( sK0 @ ( sK9 @ sK1 ) @ X0 )
= ( sK9 @ ( sK9 @ X0 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f33630,f39377]) ).
thf(f39437,plain,
( ! [X0: g] :
( ( sK9 @ ( sK9 @ X0 ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f39416,f33630]) ).
thf(f39625,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK0 @ ( sK9 @ ( sK0 @ X0 @ sK1 ) ) @ X1 ) )
= X1 )
| ~ spl22_5
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2492,f33582]) ).
thf(f41026,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK6 @ sK1 @ X0 ) @ sK1 )
= ( sK0 @ X0 @ ( sK0 @ X1 @ ( sK9 @ ( sK0 @ X1 @ sK1 ) ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2763,f34239]) ).
thf(f41031,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ sK1 @ ( sK6 @ sK1 @ X0 ) )
= ( sK0 @ X0 @ ( sK0 @ X1 @ ( sK9 @ ( sK0 @ X1 @ sK1 ) ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f41026,f33338]) ).
thf(f41069,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK0 @ X1 @ ( sK9 @ ( sK0 @ X1 @ sK1 ) ) ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f41031,f33416]) ).
thf(f41234,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK6 @ sK1 @ X0 ) @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) )
= X1 )
| ~ spl22_3
| ~ spl22_5
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f39625,f206]) ).
thf(f41374,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ ( sK5 @ sK1 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) )
= X1 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f41234,f3822]) ).
thf(f47828,plain,
( ! [X0: g] :
( ( sK9 @ X0 )
= ( sK0 @ sK1 @ ( sK9 @ ( sK0 @ X0 @ sK1 ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f41069,f262]) ).
thf(f47980,plain,
( ! [X0: g] :
( ( sK9 @ X0 )
= ( sK0 @ sK1 @ ( sK9 @ ( sK0 @ sK1 @ X0 ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f47828,f33338]) ).
thf(f47981,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ ( sK9 @ X0 ) )
= ( sK9 @ ( sK6 @ sK1 @ X0 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f47828,f206]) ).
thf(f48393,plain,
( ! [X0: g] :
( ( sK9 @ ( sK0 @ sK1 @ ( sK9 @ X0 ) ) )
= ( sK6 @ sK1 @ X0 ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f39437,f47981]) ).
thf(f48883,plain,
( ! [X0: g] :
( ( sK9 @ ( sK9 @ X0 ) )
= ( sK6 @ sK1 @ ( sK0 @ X0 @ sK1 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f48393,f47828]) ).
thf(f48885,plain,
( ! [X0: g] :
( ( sK9 @ ( sK9 @ X0 ) )
= ( sK6 @ sK1 @ ( sK0 @ sK1 @ X0 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f48393,f47980]) ).
thf(f48980,plain,
( ! [X0: g] :
( ( sK6 @ sK1 @ ( sK0 @ sK1 @ X0 ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f48885,f39437]) ).
thf(f48981,plain,
( ! [X0: g] :
( ( sK6 @ sK1 @ ( sK0 @ X0 @ sK1 ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f48883,f39437]) ).
thf(f50739,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK9 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) )
= ( sK6 @ sK1 @ ( sK0 @ X0 @ sK1 ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f48980,f34280]) ).
thf(f50743,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X1 @ ( sK9 @ ( sK0 @ ( sK9 @ X0 ) @ X1 ) ) )
= X0 )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(forward_demodulation,[],[f50739,f48981]) ).
thf(f51884,plain,
( ! [X0: g,X1: g] :
( ( sK9 @ X0 )
= ( sK0 @ X1 @ ( sK9 @ ( sK0 @ X0 @ X1 ) ) ) )
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f50743,f39437]) ).
thf(f52237,plain,
( ! [X0: g,X1: g] :
( ( sK9 @ X1 )
= ( sK0 @ ( sK5 @ X1 @ X0 ) @ ( sK9 @ X0 ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f51884,f202]) ).
thf(f54234,plain,
( ! [X0: g,X1: g] :
( ( sK9 @ X1 )
= ( sK0 @ ( sK5 @ X1 @ ( sK9 @ X0 ) ) @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11 ),
inference(constrained_superposition,[],[f52237,f39437]) ).
thf(f74863,plain,
( ! [X0: g] :
( ( sK5 @ X0 @ X0 )
!= ( sK0 @ ( sK5 @ sK1 @ ( sK0 @ ( sK9 @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) @ ( sK5 @ X0 @ X0 ) ) ) @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(unit_resulting_resolution,[],[f2029,f4488,f38523,f41374]) ).
thf(f75229,plain,
( ! [X0: g] :
( ( sK5 @ X0 @ X0 )
!= ( sK0 @ ( sK5 @ sK1 @ ( sK9 @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) ) @ ( sK13 @ ( sK5 @ X0 @ X0 ) ) ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f74863,f4488]) ).
thf(f75321,plain,
( ! [X0: g] :
( ( sK9 @ sK1 )
!= ( sK5 @ X0 @ X0 ) )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_demodulation,[],[f75229,f54234]) ).
thf(f75365,plain,
( $false
| ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(forward_subsumption_resolution,[],[f75321,f38480]) ).
thf(f75366,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(avatar_contradiction_clause,[],[f75365]) ).
thf(f76973,plain,
( ! [X0: g] :
( ( sK6 @ sK1 @ X0 )
= X0 )
| ~ spl22_3
| ~ spl22_4 ),
inference(constrained_superposition,[],[f213,f206]) ).
thf(f77193,plain,
( ! [X0: g] :
( ( sK5 @ sK1 @ X0 )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4
| ~ spl22_11 ),
inference(constrained_superposition,[],[f7759,f76973]) ).
thf(f77672,plain,
( spl22_6
| spl22_9 ),
inference(avatar_split_clause,[],[f153,f236,f219]) ).
thf(f78125,plain,
( $false
| ~ spl22_15
| ~ spl22_17 ),
inference(equality_resolution,[],[f31847]) ).
thf(f78126,plain,
( ~ spl22_15
| ~ spl22_17 ),
inference(avatar_contradiction_clause,[],[f78125]) ).
thf(f78210,plain,
( ! [X0: g] :
( sK12
!= ( sK0 @ X0 @ sK1 ) )
| ~ spl22_8
| ~ spl22_11
| ~ spl22_15 ),
inference(constrained_superposition,[],[f31849,f230]) ).
thf(f78221,plain,
( ! [X0: g] : ( sK12 != X0 )
| ~ spl22_4
| ~ spl22_8
| ~ spl22_11
| ~ spl22_15 ),
inference(forward_demodulation,[],[f78210,f213]) ).
thf(f78222,plain,
( $false
| ~ spl22_4
| ~ spl22_8
| ~ spl22_11
| ~ spl22_15 ),
inference(unit_resulting_resolution,[],[f78221,f213]) ).
thf(f78225,plain,
( ~ spl22_4
| ~ spl22_8
| ~ spl22_11
| ~ spl22_15 ),
inference(avatar_contradiction_clause,[],[f78222]) ).
thf(f78237,plain,
( $false
| ~ spl22_4
| ~ spl22_7
| ~ spl22_13 ),
inference(unit_resulting_resolution,[],[f2107,f213]) ).
thf(f78240,plain,
( ~ spl22_4
| ~ spl22_7
| ~ spl22_13 ),
inference(avatar_contradiction_clause,[],[f78237]) ).
thf(f78274,plain,
( $false
| ~ spl22_1
| ~ spl22_6
| ~ spl22_11
| ~ spl22_13 ),
inference(unit_resulting_resolution,[],[f277,f2026]) ).
thf(f78293,plain,
( ~ spl22_1
| ~ spl22_6
| ~ spl22_11
| ~ spl22_13 ),
inference(avatar_contradiction_clause,[],[f78274]) ).
thf(f78341,plain,
( ! [X0: g] :
( ( sK0 @ sK1 @ X0 )
= X0 )
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4
| ~ spl22_11 ),
inference(constrained_superposition,[],[f202,f77193]) ).
thf(f78347,plain,
( spl22_1
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f78341,f246,f212,f205,f201,f198]) ).
thf(f78398,plain,
( spl22_8
| ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f903,f246,f219,f212,f198,f229]) ).
thf(f78795,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ X0 @ X1 )
= ( sK10 @ ( sK10 @ X0 @ sK1 ) @ X1 ) )
| ~ spl22_1
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f2500,f199]) ).
thf(f78809,plain,
( ! [X0: g,X1: g] :
( ( sK0 @ ( sK10 @ X0 @ sK1 ) @ ( sK0 @ X0 @ X1 ) )
= X1 )
| ~ spl22_1
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f223,f78795]) ).
thf(f78819,plain,
( ! [X0: g] :
( sK1
= ( sK0 @ ( sK10 @ X0 @ sK1 ) @ X0 ) )
| ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_11 ),
inference(constrained_superposition,[],[f78809,f213]) ).
thf(f78851,plain,
( ( ( sK15 @ sK1 )
!= ( sK0 @ ( sK15 @ sK1 ) @ sK1 ) )
| ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_11
| ~ spl22_14 ),
inference(unit_resulting_resolution,[],[f2029,f199,f223,f78819]) ).
thf(f78887,plain,
( $false
| ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_11
| ~ spl22_14 ),
inference(forward_subsumption_resolution,[],[f78851,f213]) ).
thf(f78888,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_11
| ~ spl22_14 ),
inference(avatar_contradiction_clause,[],[f78887]) ).
thf(f78894,plain,
( spl22_11
| spl22_11 ),
inference(avatar_split_clause,[],[f55,f246,f246]) ).
cnf(s1,plain,
( spl22_1
| spl22_2 ),
inference(sat_conversion,[],[f203]) ).
cnf(s2,plain,
( spl22_1
| spl22_3 ),
inference(sat_conversion,[],[f207]) ).
cnf(s3,plain,
( spl22_4
| spl22_5 ),
inference(sat_conversion,[],[f217]) ).
cnf(s4,plain,
( spl22_6
| spl22_7 ),
inference(sat_conversion,[],[f224]) ).
cnf(s5,plain,
( spl22_7
| spl22_8 ),
inference(sat_conversion,[],[f231]) ).
cnf(s6,plain,
( spl22_8
| spl22_9 ),
inference(sat_conversion,[],[f238]) ).
cnf(s10,plain,
( ~ spl22_11
| spl22_13
| spl22_14
| spl22_15 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s12,plain,
( ~ spl22_2
| ~ spl22_13 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s21,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| ~ spl22_8
| ~ spl22_14 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s31,plain,
( ~ spl22_1
| spl22_4
| ~ spl22_8
| ~ spl22_11 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s32,plain,
( spl22_4
| spl22_17 ),
inference(sat_conversion,[],[f2485]) ).
cnf(s33,plain,
( ~ spl22_1
| spl22_4
| ~ spl22_9
| ~ spl22_11 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s36,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(sat_conversion,[],[f31839]) ).
cnf(s37,plain,
( ~ spl22_9
| ~ spl22_15 ),
inference(sat_conversion,[],[f31860]) ).
cnf(s43,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_11
| ~ spl22_14
| ~ spl22_17 ),
inference(sat_conversion,[],[f75366]) ).
cnf(s46,plain,
( spl22_6
| spl22_9 ),
inference(sat_conversion,[],[f77672]) ).
cnf(s49,plain,
( ~ spl22_15
| ~ spl22_17 ),
inference(sat_conversion,[],[f78126]) ).
cnf(s52,plain,
( ~ spl22_4
| ~ spl22_8
| ~ spl22_11
| ~ spl22_15 ),
inference(sat_conversion,[],[f78225]) ).
cnf(s54,plain,
( ~ spl22_4
| ~ spl22_7
| ~ spl22_13 ),
inference(sat_conversion,[],[f78240]) ).
cnf(s55,plain,
( ~ spl22_1
| ~ spl22_6
| ~ spl22_11
| ~ spl22_13 ),
inference(sat_conversion,[],[f78293]) ).
cnf(s56,plain,
( spl22_1
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4
| ~ spl22_11 ),
inference(sat_conversion,[],[f78347]) ).
cnf(s57,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| spl22_8
| ~ spl22_11 ),
inference(sat_conversion,[],[f78398]) ).
cnf(s74,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_11
| ~ spl22_14 ),
inference(sat_conversion,[],[f78888]) ).
cnf(s76,plain,
( spl22_11
| spl22_11 ),
inference(sat_conversion,[],[f78894]) ).
cnf(s77,plain,
spl22_11,
inference(rat,[],[s76]) ).
cnf(s78,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_7
| ~ spl22_14 ),
inference(rat,[],[s74,s77]) ).
cnf(s95,plain,
( ~ spl22_1
| ~ spl22_4
| ~ spl22_6
| spl22_8 ),
inference(rat,[],[s57,s77]) ).
cnf(s96,plain,
( spl22_1
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4 ),
inference(rat,[],[s56,s77]) ).
cnf(s97,plain,
( ~ spl22_1
| ~ spl22_6
| ~ spl22_13 ),
inference(rat,[],[s55,s77]) ).
cnf(s98,plain,
( ~ spl22_4
| ~ spl22_8
| ~ spl22_15 ),
inference(rat,[],[s52,s77]) ).
cnf(s105,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_6
| ~ spl22_8
| ~ spl22_14
| ~ spl22_17 ),
inference(rat,[],[s43,s77]) ).
cnf(s111,plain,
( ~ spl22_2
| ~ spl22_3
| ~ spl22_5
| ~ spl22_7
| ~ spl22_9
| ~ spl22_14
| ~ spl22_17 ),
inference(rat,[],[s36,s77]) ).
cnf(s114,plain,
( ~ spl22_1
| spl22_4
| ~ spl22_9 ),
inference(rat,[],[s33,s77]) ).
cnf(s115,plain,
( ~ spl22_1
| spl22_4
| ~ spl22_8 ),
inference(rat,[],[s31,s77]) ).
cnf(s124,plain,
( spl22_13
| spl22_14
| spl22_15 ),
inference(rat,[],[s10,s77]) ).
cnf(s126,plain,
( spl22_6
| spl22_1 ),
inference(rat,[],[s111,s4,s46,s3,s124,s49,s32,s96,s2,s12,s1]) ).
cnf(s127,plain,
( ~ spl22_6
| ~ spl22_17
| ~ spl22_2
| ~ spl22_3
| ~ spl22_14
| ~ spl22_5 ),
inference(rat,[],[s111,s5,s6,s105]) ).
cnf(s128,plain,
( ~ spl22_2
| ~ spl22_3
| spl22_1 ),
inference(rat,[],[s127,s126,s124,s49,s3,s32,s12,s96]) ).
cnf(s129,plain,
spl22_1,
inference(rat,[],[s128,s1,s2]) ).
cnf(s132,plain,
spl22_6,
inference(rat,[],[s78,s124,s54,s114,s37,s4,s46,s129]) ).
cnf(s133,plain,
~ spl22_13,
inference(rat,[],[s97,s129,s132]) ).
cnf(s134,plain,
( ~ spl22_4
| ~ spl22_14 ),
inference(rat,[],[s21,s95,s129,s132]) ).
cnf(s135,plain,
spl22_4,
inference(rat,[],[s6,s115,s114,s129]) ).
cnf(s136,plain,
spl22_8,
inference(rat,[],[s95,s132,s129,s135]) ).
cnf(s137,plain,
~ spl22_14,
inference(rat,[],[s134,s135]) ).
cnf(s138,plain,
~ spl22_15,
inference(rat,[],[s98,s135,s136]) ).
cnf(s139,plain,
$false,
inference(rat,[],[s124,s133,s138,s137]) ).
thf(f78895,plain,
$false,
inference(avatar_sat_refutation,[],[s139]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG276^5 : TPTP v9.3.1. Bugfixed v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n004.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:36:07 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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.08/1.04 % (1612909)Will run a generic schedule for satisfiability detection.
% 4.08/1.04 % (1612915)% WARNING: option uhcvi not known.
% 4.08/1.04 % (1612919)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1625347486:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.08/1.04 % (1612914)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=937295888_2999 on theBenchmark for (2999ds/0Mi)
% 4.08/1.04 % (1612917)dis+10_1_sil=32000:sp=arity:random_seed=3830668564:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.08/1.04 % (1612916)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=783405687:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.08/1.04 % (1612915)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3158574460:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.08/1.04 % (1612915)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.08/1.04 % Exception at run slice level
% 4.08/1.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.08/1.04 % (1612915)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.08/1.04 % (1612920)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=726643194:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.08/1.04 % (1612926)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1405951541:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.08/1.04 % (1612918)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3338799680:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.08/1.04 % (1612918)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.08/1.04 % Exception at run slice level
% 4.08/1.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.08/1.04 % (1612930)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1064087025:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.08/1.04 % (1612917)Instruction limit reached!
% 4.08/1.04 % (1612917)------------------------------
% 4.08/1.04 % (1612917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.04 % (1612917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.04 % (1612917)CaDiCaL version: 2.1.3
% 4.08/1.04 % (1612917)Termination reason: Instruction limit
% 4.08/1.04 % (1612917)Termination phase: Saturation
% 4.08/1.04 % (1612917)Time elapsed: 0.053 s
% 4.08/1.04 % (1612917)Peak memory usage: 12 MB
% 4.08/1.04 % (1612917)Instructions burned: 104 (million)
% 4.08/1.04 % (1612919)Instruction limit reached!
% 4.08/1.04 % (1612919)------------------------------
% 4.08/1.04 % (1612919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.04 % (1612919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.04 % (1612919)CaDiCaL version: 2.1.3
% 4.08/1.04 % (1612919)Termination reason: Instruction limit
% 4.08/1.04 % (1612919)Termination phase: Saturation
% 4.08/1.04 % (1612919)Time elapsed: 0.059 s
% 4.08/1.04 % (1612919)Peak memory usage: 13 MB
% 4.08/1.04 % (1612919)Instructions burned: 134 (million)
% 4.08/1.04 % (1612932)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=2671079729:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.08/1.04 % (1612932)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.08/1.04 % (1612932)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.08/1.04 % (1612933)ott-21_1_sil=16000:fs=off:random_seed=842243927:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.08/1.04 % (1612930)Instruction limit reached!
% 4.08/1.04 % (1612930)------------------------------
% 4.08/1.04 % (1612930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.04 % (1612930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.04 % (1612930)CaDiCaL version: 2.1.3
% 4.08/1.04 % (1612930)Termination reason: Instruction limit
% 4.08/1.04 % (1612930)Termination phase: Saturation
% 4.08/1.04 % (1612930)Time elapsed: 0.071 s
% 4.08/1.04 % (1612930)Peak memory usage: 12 MB
% 4.08/1.04 % (1612930)Instructions burned: 131 (million)
% 4.08/1.04 % (1612936)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1655720711:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 18.04/3.07 % (1612918)Instruction limit reached!
% 18.04/3.07 % (1612918)------------------------------
% 18.04/3.07 % (1612918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.04/3.07 % (1612918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.07 % (1612918)CaDiCaL version: 2.1.3
% 18.04/3.07 % (1612918)Termination reason: Instruction limit
% 18.04/3.07 % (1612918)Termination phase: Saturation
% 18.04/3.07 % (1612918)Time elapsed: 0.117 s
% 18.04/3.07 % (1612918)Peak memory usage: 13 MB
% 18.04/3.07 % (1612918)Instructions burned: 117 (million)
% 18.04/3.07 % (1612938)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=342829026:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 18.04/3.07 % Exception at run slice level
% 18.04/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.04/3.07 % (1612920)Instruction limit reached!
% 18.04/3.07 % (1612920)------------------------------
% 18.04/3.07 % (1612920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.04/3.07 % (1612920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.07 % (1612920)CaDiCaL version: 2.1.3
% 18.04/3.07 % (1612920)Termination reason: Instruction limit
% 18.04/3.07 % (1612920)Termination phase: Saturation
% 18.04/3.07 % (1612920)Time elapsed: 0.148 s
% 18.04/3.07 % (1612920)Peak memory usage: 13 MB
% 18.04/3.07 % (1612920)Instructions burned: 161 (million)
% 18.04/3.07 % (1612940)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=943316435:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 18.04/3.07 % (1612933)Instruction limit reached!
% 18.04/3.07 % (1612933)------------------------------
% 18.04/3.07 % (1612933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.04/3.07 % (1612933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.07 % (1612933)CaDiCaL version: 2.1.3
% 18.04/3.07 % (1612933)Termination reason: Instruction limit
% 18.04/3.07 % (1612933)Termination phase: Saturation
% 18.04/3.07 % (1612933)Time elapsed: 0.083 s
% 18.04/3.07 % (1612933)Peak memory usage: 12 MB
% 18.04/3.07 % (1612933)Instructions burned: 180 (million)
% 18.04/3.07 % (1612941)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3857341059:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 18.04/3.07 % Exception at run slice level
% 18.04/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.04/3.07 % (1612945)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=668841052:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 18.04/3.07 % (1612945)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 18.04/3.07 % (1612943)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=1196060536:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 18.04/3.07 % (1612943)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 18.04/3.07 % (1612936)Instruction limit reached!
% 18.04/3.07 % (1612936)------------------------------
% 18.04/3.07 % (1612936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.04/3.07 % (1612936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.07 % (1612936)CaDiCaL version: 2.1.3
% 18.04/3.07 % (1612936)Termination reason: Instruction limit
% 18.04/3.07 % (1612936)Termination phase: Saturation
% 18.04/3.07 % (1612936)Time elapsed: 0.237 s
% 18.04/3.07 % (1612936)Peak memory usage: 14 MB
% 18.04/3.07 % (1612936)Instructions burned: 478 (million)
% 18.04/3.07 % (1612948)fmb+10_1_sil=64000:random_seed=2077106115:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 18.04/3.07 % (1612948)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 18.04/3.07 % Exception at run slice level
% 18.04/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.04/3.07 % (1612932)Instruction limit reached!
% 18.04/3.07 % (1612932)------------------------------
% 18.04/3.07 % (1612932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.04/3.07 % (1612932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612932)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612932)Termination reason: Instruction limit
% 39.28/6.02 % (1612932)Termination phase: Saturation
% 39.28/6.02 % (1612932)Time elapsed: 0.319 s
% 39.28/6.02 % (1612932)Peak memory usage: 16 MB
% 39.28/6.02 % (1612932)Instructions burned: 685 (million)
% 39.28/6.02 % (1612950)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1224604223:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 39.28/6.02 % (1612951)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3512746947:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612954)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2271667394:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 39.28/6.02 % (1612955)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2601876391:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 39.28/6.02 % (1612954)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 39.28/6.02 % (1612955)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 39.28/6.02 % (1612955)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 39.28/6.02 % (1612945)Instruction limit reached!
% 39.28/6.02 % (1612945)------------------------------
% 39.28/6.02 % (1612945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612945)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612945)Termination reason: Instruction limit
% 39.28/6.02 % (1612945)Termination phase: Saturation
% 39.28/6.02 % (1612945)Time elapsed: 0.401 s
% 39.28/6.02 % (1612945)Peak memory usage: 16 MB
% 39.28/6.02 % (1612945)Instructions burned: 880 (million)
% 39.28/6.02 % (1612958)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=16996112:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612960)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=584248930:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612962)ott-2_1_sil=16000:newcnf=on:random_seed=4185474367:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 39.28/6.02 % (1612962)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 39.28/6.02 % (1612940)Instruction limit reached!
% 39.28/6.02 % (1612940)------------------------------
% 39.28/6.02 % (1612940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612940)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612940)Termination reason: Instruction limit
% 39.28/6.02 % (1612940)Termination phase: Saturation
% 39.28/6.02 % (1612940)Time elapsed: 0.515 s
% 39.28/6.02 % (1612940)Peak memory usage: 22 MB
% 39.28/6.02 % (1612940)Instructions burned: 1181 (million)
% 39.28/6.02 % (1612964)ott+10_1_sil=32000:tgt=ground:random_seed=2711680158:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 39.28/6.02 % (1612943)Instruction limit reached!
% 39.28/6.02 % (1612943)------------------------------
% 39.28/6.02 % (1612943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612943)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612943)Termination reason: Instruction limit
% 39.28/6.02 % (1612943)Termination phase: Saturation
% 39.28/6.02 % (1612943)Time elapsed: 0.531 s
% 39.28/6.02 % (1612943)Peak memory usage: 17 MB
% 39.28/6.02 % (1612943)Instructions burned: 693 (million)
% 39.28/6.02 % (1612966)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1722521600:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612968)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1461351582:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 39.28/6.02 % (1612968)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 39.28/6.02 % (1612962)Instruction limit reached!
% 39.28/6.02 % (1612962)------------------------------
% 39.28/6.02 % (1612962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612962)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612962)Termination reason: Instruction limit
% 39.28/6.02 % (1612962)Termination phase: Saturation
% 39.28/6.02 % (1612962)Time elapsed: 0.408 s
% 39.28/6.02 % (1612962)Peak memory usage: 17 MB
% 39.28/6.02 % (1612962)Instructions burned: 869 (million)
% 39.28/6.02 % (1612971)dis+21_1_sil=32000:sas=cadical:random_seed=3753687406:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 39.28/6.02 % (1612955)Instruction limit reached!
% 39.28/6.02 % (1612955)------------------------------
% 39.28/6.02 % (1612955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612955)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612955)Termination reason: Instruction limit
% 39.28/6.02 % (1612955)Termination phase: Saturation
% 39.28/6.02 % (1612955)Time elapsed: 1.177 s
% 39.28/6.02 % (1612955)Peak memory usage: 30 MB
% 39.28/6.02 % (1612955)Instructions burned: 1472 (million)
% 39.28/6.02 % (1612973)ott+11_1_sil=16000:gs=on:random_seed=2045120342:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 39.28/6.02 % (1612973)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 39.28/6.02 % (1612968)Instruction limit reached!
% 39.28/6.02 % (1612968)------------------------------
% 39.28/6.02 % (1612968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612968)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612968)Termination reason: Instruction limit
% 39.28/6.02 % (1612968)Termination phase: Saturation
% 39.28/6.02 % (1612968)Time elapsed: 1.627 s
% 39.28/6.02 % (1612968)Peak memory usage: 26 MB
% 39.28/6.02 % (1612968)Instructions burned: 3514 (million)
% 39.28/6.02 % (1612976)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4185319780:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612978)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2692226474:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi)
% 39.28/6.02 % (1612971)Instruction limit reached!
% 39.28/6.02 % (1612971)------------------------------
% 39.28/6.02 % (1612971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612971)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612971)Termination reason: Instruction limit
% 39.28/6.02 % (1612971)Termination phase: Saturation
% 39.28/6.02 % (1612971)Time elapsed: 1.672 s
% 39.28/6.02 % (1612971)Peak memory usage: 32 MB
% 39.28/6.02 % (1612971)Instructions burned: 3773 (million)
% 39.28/6.02 % (1612954)Instruction limit reached!
% 39.28/6.02 % (1612954)------------------------------
% 39.28/6.02 % (1612954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612954)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612954)Termination reason: Instruction limit
% 39.28/6.02 % (1612954)Termination phase: Saturation
% 39.28/6.02 % (1612954)Time elapsed: 2.362 s
% 39.28/6.02 % (1612954)Peak memory usage: 39 MB
% 39.28/6.02 % (1612954)Instructions burned: 5132 (million)
% 39.28/6.02 % (1612964)Instruction limit reached!
% 39.28/6.02 % (1612964)------------------------------
% 39.28/6.02 % (1612964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612964)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612964)Termination reason: Instruction limit
% 39.28/6.02 % (1612964)Termination phase: Saturation
% 39.28/6.02 % (1612964)Time elapsed: 2.081 s
% 39.28/6.02 % (1612964)Peak memory usage: 31 MB
% 39.28/6.02 % (1612964)Instructions burned: 5119 (million)
% 39.28/6.02 % (1612980)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=157093967:i=29340_2971 on theBenchmark for (2971ds/29340Mi)
% 39.28/6.02 % (1612982)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=394820750:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612981)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4088529910:i=5211_2971 on theBenchmark for (2971ds/5211Mi)
% 39.28/6.02 % (1612985)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4255085518:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612988)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=494755147:i=14071_2971 on theBenchmark for (2971ds/14071Mi)
% 39.28/6.02 % Exception at run slice level
% 39.28/6.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 39.28/6.02 % (1612990)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3034243461:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi)
% 39.28/6.02 % (1612973)Instruction limit reached!
% 39.28/6.02 % (1612973)------------------------------
% 39.28/6.02 % (1612973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612973)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612973)Termination reason: Instruction limit
% 39.28/6.02 % (1612973)Termination phase: Saturation
% 39.28/6.02 % (1612973)Time elapsed: 1.336 s
% 39.28/6.02 % (1612973)Peak memory usage: 24 MB
% 39.28/6.02 % (1612973)Instructions burned: 2252 (million)
% 39.28/6.02 % (1612993)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3984959496:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi)
% 39.28/6.02 % (1612981)Instruction limit reached!
% 39.28/6.02 % (1612981)------------------------------
% 39.28/6.02 % (1612981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612981)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612981)Termination reason: Instruction limit
% 39.28/6.02 % (1612981)Termination phase: Saturation
% 39.28/6.02 % (1612981)Time elapsed: 2.362 s
% 39.28/6.02 % (1612981)Peak memory usage: 38 MB
% 39.28/6.02 % (1612981)Instructions burned: 5213 (million)
% 39.28/6.02 % (1613002)dis+10_16:1_sil=16000:random_seed=3824852204:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi)
% 39.28/6.02 % (1612978)Instruction limit reached!
% 39.28/6.02 % (1612978)------------------------------
% 39.28/6.02 % (1612978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.02 % (1612978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.02 % (1612978)CaDiCaL version: 2.1.3
% 39.28/6.02 % (1612978)Termination reason: Instruction limit
% 39.28/6.02 % (1612978)Termination phase: Saturation
% 39.28/6.02 % (1612978)Time elapsed: 2.998 s
% 39.28/6.02 % (1612978)Peak memory usage: 28 MB
% 39.28/6.02 % (1612978)Instructions burned: 4593 (million)
% 39.28/6.02 % (1613004)ott-3_8_sil=64000:random_seed=1611493194:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi)
% 39.28/6.02 % (1612980) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1612909-1612980"...
% 39.28/6.02 % (1612980)...printing done.
% 39.28/6.02 % (1612980)Refutation found. Thanks to Tanya!
% 39.28/6.02 % SZS status Theorem for theBenchmark
% 39.28/6.02 % SZS output start Proof for theBenchmark
% See solution above
% 39.28/6.03 % (1612980)------------------------------
% 39.28/6.03 % (1612980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.28/6.03 % (1612980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.03 % (1612980)CaDiCaL version: 2.1.3
% 39.28/6.03 % (1612980)Termination reason: Refutation
% 39.28/6.03 % (1612980)Time elapsed: 2.923 s
% 39.28/6.03 % (1612980)Peak memory usage: 42 MB
% 39.28/6.03 % (1612980)Instructions burned: 7501 (million)
% 39.28/6.03 % (1612909)Success in time 5.782 s
% 39.28/6.03 % Vampire exiting
%------------------------------------------------------------------------------