%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP009_3 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 11:27:56 AM UTC 2026
% Result : Theorem 17.54s 13.79s
% Output : Refutation 20.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 39
% Syntax : Number of formulae : 203 ( 56 unt; 0 typ; 28 def)
% Number of atoms : 575 ( 58 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 676 ( 304 ~; 300 |; 33 &)
% ( 31 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 29 usr; 28 prp; 0-2 aty)
% Number of functors : 42 ( 42 usr; 14 con; 0-7 aty)
% Number of variables : 422 ( 0 sgn 386 !; 36 ?; 422 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
tyop_2Emin_2Ebool: $tType ).
tff(type_def_6,type,
tyop_2Emin_2Efun: ( $tType * $tType ) > $tType ).
tff(type_def_7,type,
sK0: $tType ).
tff(type_def_8,type,
sK1: $tType ).
tff(type_def_9,type,
sK2: $tType ).
tff(type_def_10,type,
sK3: $tType ).
tff(func_def_0,type,
app_2E2:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_1,type,
combin_i_2E0:
!>[X0: $tType] : tyop_2Emin_2Efun(X0,X0) ).
tff(func_def_2,type,
combin_k_2E0:
!>[X0: $tType,X1: $tType] : tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X0)) ).
tff(func_def_3,type,
combin_s_2E0:
!>[X0: $tType,X1: $tType,X2: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X0,X2))) ).
tff(func_def_4,type,
c_2Ebool_2E_21_2E0:
!>[X0: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool) ).
tff(func_def_5,type,
c_2Ebool_2E_21_2E1:
!>[X0: $tType] : ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool) > tyop_2Emin_2Ebool ) ).
tff(func_def_6,type,
c_2Equotient_2E_2D_2D_3E_2E0:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X1),tyop_2Emin_2Efun(X0,X3)))) ).
tff(func_def_7,type,
c_2Equotient_2E_2D_2D_3E_2E2:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( tyop_2Emin_2Efun(X0,X2) * tyop_2Emin_2Efun(X1,X3) ) > tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X1),tyop_2Emin_2Efun(X0,X3)) ) ).
tff(func_def_8,type,
c_2Equotient_2E_2D_2D_3E_2E3:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( ( tyop_2Emin_2Efun(X0,X2) * tyop_2Emin_2Efun(X1,X3) * tyop_2Emin_2Efun(X2,X1) ) > tyop_2Emin_2Efun(X0,X3) ) ).
tff(func_def_9,type,
c_2Ebool_2E_2F_5C_2E0: tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)) ).
tff(func_def_10,type,
c_2Ebool_2E_2F_5C_2E2: ( tyop_2Emin_2Ebool * tyop_2Emin_2Ebool ) > tyop_2Emin_2Ebool ).
tff(func_def_11,type,
c_2Emin_2E_3D_2E0:
!>[X0: $tType] : tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)) ).
tff(func_def_12,type,
c_2Emin_2E_3D_2E2:
!>[X0: $tType] : ( ( X0 * X0 ) > tyop_2Emin_2Ebool ) ).
tff(func_def_13,type,
c_2Equotient_2E_3D_3D_3D_3E_2E0:
!>[X0: $tType,X1: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)))) ).
tff(func_def_14,type,
c_2Equotient_2E_3D_3D_3D_3E_2E2:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)) * tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)) ) > tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)) ) ).
tff(func_def_15,type,
c_2Equotient_2E_3D_3D_3D_3E_2E4:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)) * tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)) * tyop_2Emin_2Efun(X0,X1) * tyop_2Emin_2Efun(X0,X1) ) > tyop_2Emin_2Ebool ) ).
tff(func_def_16,type,
c_2Emin_2E_3D_3D_3E_2E0: tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)) ).
tff(func_def_17,type,
c_2Emin_2E_3D_3D_3E_2E2: ( tyop_2Emin_2Ebool * tyop_2Emin_2Ebool ) > tyop_2Emin_2Ebool ).
tff(func_def_18,type,
c_2Ebool_2E_3F_2E0:
!>[X0: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool) ).
tff(func_def_19,type,
c_2Ebool_2E_3F_2E1:
!>[X0: $tType] : ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool) > tyop_2Emin_2Ebool ) ).
tff(func_def_20,type,
c_2Ebool_2EF_2E0: tyop_2Emin_2Ebool ).
tff(func_def_21,type,
c_2Equotient_2EQUOTIENT_2E0:
!>[X0: $tType,X1: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X0),tyop_2Emin_2Ebool))) ).
tff(func_def_22,type,
c_2Equotient_2EQUOTIENT_2E3:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)) * tyop_2Emin_2Efun(X0,X1) * tyop_2Emin_2Efun(X1,X0) ) > tyop_2Emin_2Ebool ) ).
tff(func_def_23,type,
c_2Ebool_2ET_2E0: tyop_2Emin_2Ebool ).
tff(func_def_24,type,
c_2Ecombin_2EW_2E0:
!>[X0: $tType,X1: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1)) ).
tff(func_def_25,type,
c_2Ecombin_2EW_2E2:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)) * X0 ) > X1 ) ).
tff(func_def_26,type,
c_2Ebool_2E_5C_2F_2E0: tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)) ).
tff(func_def_27,type,
c_2Ebool_2E_5C_2F_2E2: ( tyop_2Emin_2Ebool * tyop_2Emin_2Ebool ) > tyop_2Emin_2Ebool ).
tff(func_def_28,type,
c_2Equotient_2Erespects_2E0:
!>[X0: $tType,X1: $tType] : tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1)) ).
tff(func_def_29,type,
c_2Equotient_2Erespects_2E2:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)) * X0 ) > X1 ) ).
tff(func_def_30,type,
c_2Ebool_2E_7E_2E0: tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool) ).
tff(func_def_31,type,
c_2Ebool_2E_7E_2E1: tyop_2Emin_2Ebool > tyop_2Emin_2Ebool ).
tff(func_def_32,type,
sK4: tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)) ).
tff(func_def_33,type,
sK5: tyop_2Emin_2Efun(sK0,sK2) ).
tff(func_def_34,type,
sK6: tyop_2Emin_2Efun(sK2,sK0) ).
tff(func_def_35,type,
sK7: tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)) ).
tff(func_def_36,type,
sK8: tyop_2Emin_2Efun(sK1,sK3) ).
tff(func_def_37,type,
sK9: tyop_2Emin_2Efun(sK3,sK1) ).
tff(func_def_38,type,
sK10: tyop_2Emin_2Efun(sK0,sK1) ).
tff(func_def_39,type,
sK11: tyop_2Emin_2Efun(sK0,sK1) ).
tff(func_def_40,type,
sK12:
!>[X0: $tType,X1: $tType] : ( ( tyop_2Emin_2Efun(X0,X1) * tyop_2Emin_2Efun(X0,X1) ) > X0 ) ).
tff(pred_def_1,type,
p: tyop_2Emin_2Ebool > $o ).
tff(pred_def_2,type,
sP13: tyop_2Emin_2Efun(sK2,sK3) > $o ).
tff(f18,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X2,X0),X5: tyop_2Emin_2Efun(X1,X3)] : ( c_2Equotient_2E_2D_2D_3E_2E2(X2,X1,X0,X3,X4,X5) = app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X4),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Equotient_2E_2D_2D_3E_2E2_2Emono_2EA_27c_20mono_2EA_27b_20mono_2EA_27a_20mono_2EA_27d) ).
tff(f19,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X2,X0),X5: tyop_2Emin_2Efun(X1,X3),X6: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X4,X5,X6) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X4),X5),X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Equotient_2E_2D_2D_3E_2E3_2Emono_2EA_27c_20mono_2EA_27b_20mono_2EA_27a_20mono_2EA_27d) ).
tff(f22,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))] : ( c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X2,X3) = app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Equotient_2E_3D_3D_3D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27b) ).
tff(f23,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,X1),X5: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X2,X3,X4,X5) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X2),X3),X4),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq4_2Ec_2Equotient_2E_3D_3D_3D_3E_2E4_2Emono_2EA_27a_20mono_2EA_27b) ).
tff(f30,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( c_2Ecombin_2EW_2E2(X0,X1,X2,X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Ecombin_2EW_2E0(X0,X1),X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Ecombin_2EW_2E2_2Emono_2EA_27a_20mono_2EA_27b) ).
tff(f32,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,X2,X3) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Equotient_2Erespects_2E2_2Emono_2Etyop_2Emin_2Efun_28A_27a_2CA_27b_29_20mono_2Etyop_2Emin_2Ebool) ).
tff(f39,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( c_2Ecombin_2EW_2E2(X0,X1,X2,X3) = app_2E2(X0,X1,app_2E2(X0,tyop_2Emin_2Efun(X0,X1),X2,X3),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ecombin_2EW__THM) ).
tff(f40,axiom,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4))
=> ! [X5: X0,X6: X0] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
<=> ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
& p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
& ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient_2EQUOTIENT__REL) ).
tff(f41,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6))
=> ! [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
=> p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),c_2Equotient_2E_2D_2D_3E_2E2(X2,X1,X0,X3,X6,X8),c_2Equotient_2E_2D_2D_3E_2E2(X0,X3,X2,X1,X5,X9))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient_2EFUN__QUOTIENT) ).
tff(f42,axiom,
! [X0: $tType,X1: $tType] : ( c_2Equotient_2Erespects_2E0(X0,X1) = c_2Ecombin_2EW_2E0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient_2Erespects__def) ).
tff(f43,conjecture,
! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6))
=> ! [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
=> ! [X10: tyop_2Emin_2Efun(X0,X1),X11: tyop_2Emin_2Efun(X0,X1)] :
( p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11))
<=> ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) = c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient_2EFUN__REL__EQ__REL) ).
tff(f44,negated_conjecture,
~ ! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6))
=> ! [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
=> ! [X10: tyop_2Emin_2Efun(X0,X1),X11: tyop_2Emin_2Efun(X0,X1)] :
( p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11))
<=> ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) = c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f43]) ).
tff(f46,plain,
? [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( ? [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( ? [X10: tyop_2Emin_2Efun(X0,X1),X11: tyop_2Emin_2Efun(X0,X1)] :
( p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11))
<~> ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) = c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) ) ) )
& p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9)) )
& p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(ennf_transformation,[],[f44]) ).
tff(f52,plain,
! [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( ! [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),c_2Equotient_2E_2D_2D_3E_2E2(X2,X1,X0,X3,X6,X8),c_2Equotient_2E_2D_2D_3E_2E2(X0,X3,X2,X1,X5,X9)))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9)) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(ennf_transformation,[],[f41]) ).
tff(f53,plain,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0)] :
( ! [X5: X0,X6: X0] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
<=> ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
& p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
& ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) ) ) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(ennf_transformation,[],[f40]) ).
tff(f55,plain,
? [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( ? [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( ? [X10: tyop_2Emin_2Efun(X0,X1),X11: tyop_2Emin_2Efun(X0,X1)] :
( ( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
| ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) != c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) )
| ~ p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11)) )
& ( ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) = c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) ) )
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11)) ) )
& p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9)) )
& p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(nnf_transformation,[],[f46]) ).
tff(f56,plain,
? [X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2),X6: tyop_2Emin_2Efun(X2,X0)] :
( ? [X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X8: tyop_2Emin_2Efun(X1,X3),X9: tyop_2Emin_2Efun(X3,X1)] :
( ? [X10: tyop_2Emin_2Efun(X0,X1),X11: tyop_2Emin_2Efun(X0,X1)] :
( ( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
| ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) != c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) )
| ~ p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11)) )
& ( ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),X11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X10) = c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X6,X8,X11) ) )
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X4,X7,X10,X11)) ) )
& p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9)) )
& p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(flattening,[],[f55]) ).
tff(f57,plain,
( ( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK11))
| ( c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK10) != c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK11) )
| ~ p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) )
& ( ( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK10))
& p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK11))
& ( c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK10) = c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK11) ) )
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) )
& p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,sK9))
& p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,sK5,sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X9,sK9),skolemize(X10,sK10),skolemize(X11,sK11)],[f56]) ).
tff(f61,plain,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0)] :
( ! [X5: X0,X6: X0] :
( ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ( app_2E2(X0,X1,X3,X5) != app_2E2(X0,X1,X3,X6) ) )
& ( ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
& p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
& ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) ) )
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6)) ) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(nnf_transformation,[],[f53]) ).
tff(f62,plain,
! [X0: $tType,X1: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0)] :
( ! [X5: X0,X6: X0] :
( ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ( app_2E2(X0,X1,X3,X5) != app_2E2(X0,X1,X3,X6) ) )
& ( ( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
& p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
& ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) ) )
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6)) ) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(flattening,[],[f61]) ).
tff(f64,plain,
p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,sK5,sK6)),
inference(cnf_transformation,[],[f57]) ).
tff(f65,plain,
p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,sK9)),
inference(cnf_transformation,[],[f57]) ).
tff(f66,plain,
( ( c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK10) = c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK11) )
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) ),
inference(cnf_transformation,[],[f57]) ).
tff(f67,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK11))
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) ),
inference(cnf_transformation,[],[f57]) ).
tff(f68,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK10))
| p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) ),
inference(cnf_transformation,[],[f57]) ).
tff(f69,plain,
( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,c_2Equotient_2E_3D_3D_3D_3E_2E2(sK0,sK1,sK4,sK7),sK11))
| ( c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK10) != c_2Equotient_2E_2D_2D_3E_2E3(sK2,sK1,sK0,sK3,sK6,sK8,sK11) )
| ~ p(c_2Equotient_2E_3D_3D_3D_3E_2E4(sK0,sK1,sK4,sK7,sK10,sK11)) ),
inference(cnf_transformation,[],[f57]) ).
tff(f82,plain,
! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X6: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X2,X0),X5: tyop_2Emin_2Efun(X1,X3)] : ( c_2Equotient_2E_2D_2D_3E_2E3(X2,X1,X0,X3,X4,X5,X6) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X4),X5),X6) ),
inference(cnf_transformation,[],[f19]) ).
tff(f83,plain,
! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X8: tyop_2Emin_2Efun(X1,X3),X6: tyop_2Emin_2Efun(X2,X0),X9: tyop_2Emin_2Efun(X3,X1),X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2)] :
( p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X4,X7),c_2Equotient_2E_2D_2D_3E_2E2(X2,X1,X0,X3,X6,X8),c_2Equotient_2E_2D_2D_3E_2E2(X0,X3,X2,X1,X5,X9)))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(cnf_transformation,[],[f52]) ).
tff(f84,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,X1),X5: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2E_3D_3D_3D_3E_2E4(X0,X1,X2,X3,X4,X5) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X2),X3),X4),X5) ),
inference(cnf_transformation,[],[f23]) ).
tff(f85,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) )
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f62]) ).
tff(f86,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f62]) ).
tff(f87,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f62]) ).
tff(f88,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ( app_2E2(X0,X1,X3,X5) != app_2E2(X0,X1,X3,X6) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f62]) ).
tff(f89,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,X2,X3) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),X2),X3) ),
inference(cnf_transformation,[],[f32]) ).
tff(f91,plain,
! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X4: tyop_2Emin_2Efun(X2,X0),X5: tyop_2Emin_2Efun(X1,X3)] : ( c_2Equotient_2E_2D_2D_3E_2E2(X2,X1,X0,X3,X4,X5) = app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X4),X5) ),
inference(cnf_transformation,[],[f18]) ).
tff(f93,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))] : ( c_2Equotient_2E_3D_3D_3D_3E_2E2(X0,X1,X2,X3) = app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X2),X3) ),
inference(cnf_transformation,[],[f22]) ).
tff(f94,plain,
! [X1: $tType,X0: $tType] : ( c_2Ecombin_2EW_2E0(X0,X1) = c_2Equotient_2Erespects_2E0(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tff(f95,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( c_2Ecombin_2EW_2E2(X0,X1,X2,X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Ecombin_2EW_2E0(X0,X1),X2),X3) ),
inference(cnf_transformation,[],[f30]) ).
tff(f96,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( c_2Ecombin_2EW_2E2(X0,X1,X2,X3) = app_2E2(X0,X1,app_2E2(X0,tyop_2Emin_2Efun(X0,X1),X2,X3),X3) ),
inference(cnf_transformation,[],[f39]) ).
tff(f97,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( c_2Ecombin_2EW_2E2(X0,X1,X2,X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Equotient_2Erespects_2E0(X0,X1),X2),X3) ),
inference(definition_unfolding,[],[f95,f94]) ).
tff(f98,plain,
( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11))
| ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) != app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11) )
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
inference(definition_unfolding,[],[f69,f93,f93,f82,f82,f84]) ).
tff(f99,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
inference(definition_unfolding,[],[f68,f93,f84]) ).
tff(f100,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
inference(definition_unfolding,[],[f67,f93,f84]) ).
tff(f101,plain,
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11) )
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
inference(definition_unfolding,[],[f66,f82,f82,f84]) ).
tff(f102,plain,
! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X8: tyop_2Emin_2Efun(X1,X3),X6: tyop_2Emin_2Efun(X2,X0),X9: tyop_2Emin_2Efun(X3,X1),X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2)] :
( p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X4),X7),app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X6),X8),app_2E2(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,X3,X2,X1),X5),X9)))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ),
inference(definition_unfolding,[],[f83,f93,f91,f91]) ).
tff(f104,plain,
! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( app_2E2(X0,X1,app_2E2(X0,tyop_2Emin_2Efun(X0,X1),X2,X3),X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Equotient_2Erespects_2E0(X0,X1),X2),X3) ),
inference(definition_unfolding,[],[f96,f97]) ).
tff(f105,definition,
~ sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10)),
introduced(definition,[new_symbols(definition,[sP13])],[inequality_splitting_name_introduction]) ).
tff(f106,plain,
( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10))
| ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11))
| sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
inference(inequality_splitting,[],[f98,f105]) ).
tff(f108,definition,
( spl14_1
<=> ! [X1: $tType,X0: $tType,X3: X0,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1))] : ( app_2E2(X0,X1,app_2E2(X0,tyop_2Emin_2Efun(X0,X1),X2,X3),X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Equotient_2Erespects_2E0(X0,X1),X2),X3) ) ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
tff(f109,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),X3: X0] : ( app_2E2(X0,X1,app_2E2(X0,tyop_2Emin_2Efun(X0,X1),X2,X3),X3) = app_2E2(X0,X1,app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,X1)),tyop_2Emin_2Efun(X0,X1),c_2Equotient_2Erespects_2E0(X0,X1),X2),X3) )
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f108]) ).
tff(f110,plain,
spl14_1,
inference(avatar_split_clause,[],[f104,f108]) ).
tff(f112,definition,
( spl14_2
<=> sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10)) ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
tff(f115,plain,
~ spl14_2,
inference(avatar_split_clause,[],[f105,f112]) ).
tff(f121,definition,
( spl14_4
<=> ! [X1: $tType,X0: $tType,X3: tyop_2Emin_2Efun(X0,X1),X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))] : ( c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,X2,X3) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),X2),X3) ) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
tff(f122,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1)] : ( c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,X2,X3) = app_2E2(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool),X2),X3) )
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f121]) ).
tff(f123,plain,
spl14_4,
inference(avatar_split_clause,[],[f89,f121]) ).
tff(f125,definition,
( spl14_5
<=> ! [X1: $tType,X0: $tType,X5: X0,X3: tyop_2Emin_2Efun(X0,X1),X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X1,X0),X6: X0] :
( ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) )
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
tff(f126,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ( app_2E2(X0,X1,X3,X5) = app_2E2(X0,X1,X3,X6) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) )
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f127,plain,
spl14_5,
inference(avatar_split_clause,[],[f85,f125]) ).
tff(f129,definition,
( spl14_6
<=> ! [X1: $tType,X0: $tType,X5: X0,X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0),X6: X0,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool))] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
tff(f130,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) )
| ~ spl14_6 ),
inference(avatar_component_clause,[],[f129]) ).
tff(f131,plain,
spl14_6,
inference(avatar_split_clause,[],[f86,f129]) ).
tff(f133,definition,
( spl14_7
<=> ! [X1: $tType,X0: $tType,X5: X0,X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0),X6: X0,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool))] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
tff(f134,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) )
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f133]) ).
tff(f135,plain,
spl14_7,
inference(avatar_split_clause,[],[f87,f133]) ).
tff(f137,definition,
( spl14_8
<=> ! [X1: $tType,X0: $tType,X5: X0,X3: tyop_2Emin_2Efun(X0,X1),X4: tyop_2Emin_2Efun(X1,X0),X6: X0,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool))] :
( p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| ( app_2E2(X0,X1,X3,X5) != app_2E2(X0,X1,X3,X6) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) ) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
tff(f138,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(X0,X1),X6: X0,X4: tyop_2Emin_2Efun(X1,X0),X5: X0] :
( ( app_2E2(X0,X1,X3,X5) != app_2E2(X0,X1,X3,X6) )
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X5))
| ~ p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X6),X6))
| p(app_2E2(X0,tyop_2Emin_2Ebool,app_2E2(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2,X5),X6))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X1,X2,X3,X4)) )
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f137]) ).
tff(f139,plain,
spl14_8,
inference(avatar_split_clause,[],[f88,f137]) ).
tff(f141,definition,
( spl14_9
<=> ! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X8: tyop_2Emin_2Efun(X1,X3),X6: tyop_2Emin_2Efun(X2,X0),X9: tyop_2Emin_2Efun(X3,X1),X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2)] :
( p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X4),X7),app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X6),X8),app_2E2(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,X3,X2,X1),X5),X9)))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) ) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
tff(f142,plain,
( ! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X8: tyop_2Emin_2Efun(X1,X3),X6: tyop_2Emin_2Efun(X2,X0),X9: tyop_2Emin_2Efun(X3,X1),X7: tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X5: tyop_2Emin_2Efun(X0,X2)] :
( p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3),app_2E2(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(X0,X1),X4),X7),app_2E2(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3)),app_2E2(tyop_2Emin_2Efun(X2,X0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,X1),tyop_2Emin_2Efun(X2,X3))),c_2Equotient_2E_2D_2D_3E_2E0(X2,X1,X0,X3),X6),X8),app_2E2(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X3,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,X3,X2,X1),X5),X9)))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X1,X3,X7,X8,X9))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(X0,X2,X4,X5,X6)) )
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f143,plain,
spl14_9,
inference(avatar_split_clause,[],[f102,f141]) ).
tff(f153,definition,
( spl14_12
<=> p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,sK5,sK6)) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
tff(f155,plain,
( p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,sK5,sK6))
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f153]) ).
tff(f156,plain,
spl14_12,
inference(avatar_split_clause,[],[f64,f153]) ).
tff(f158,definition,
( spl14_13
<=> p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
tff(f160,plain,
( p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,sK9))
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f158]) ).
tff(f161,plain,
spl14_13,
inference(avatar_split_clause,[],[f65,f158]) ).
tff(f163,definition,
( spl14_14
<=> p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11)) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
tff(f165,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11))
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f163]) ).
tff(f167,definition,
( spl14_15
<=> ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11) ) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
tff(f169,plain,
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11) )
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f167]) ).
tff(f170,plain,
( spl14_14
| spl14_15 ),
inference(avatar_split_clause,[],[f101,f167,f163]) ).
tff(f172,definition,
( spl14_16
<=> p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11)) ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
tff(f173,plain,
( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11))
| spl14_16 ),
inference(avatar_component_clause,[],[f172]) ).
tff(f174,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11))
| ~ spl14_16 ),
inference(avatar_component_clause,[],[f172]) ).
tff(f175,plain,
( spl14_14
| spl14_16 ),
inference(avatar_split_clause,[],[f100,f172,f163]) ).
tff(f177,definition,
( spl14_17
<=> p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10)) ),
introduced(definition,[new_symbols(definition,[spl14_17])],[avatar_definition]) ).
tff(f178,plain,
( ~ p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10))
| spl14_17 ),
inference(avatar_component_clause,[],[f177]) ).
tff(f179,plain,
( p(c_2Equotient_2Erespects_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10))
| ~ spl14_17 ),
inference(avatar_component_clause,[],[f177]) ).
tff(f180,plain,
( spl14_14
| spl14_17 ),
inference(avatar_split_clause,[],[f99,f177,f163]) ).
tff(f182,definition,
( spl14_18
<=> sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11)) ),
introduced(definition,[new_symbols(definition,[spl14_18])],[avatar_definition]) ).
tff(f184,plain,
( sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK11))
| ~ spl14_18 ),
inference(avatar_component_clause,[],[f182]) ).
tff(f185,plain,
( ~ spl14_14
| spl14_18
| ~ spl14_16
| ~ spl14_17 ),
inference(avatar_split_clause,[],[f106,f177,f172,f182,f163]) ).
tff(f224,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7)),sK11))
| ~ spl14_4
| ~ spl14_16 ),
inference(superposition,[],[f174,f122]) ).
tff(f225,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7)),sK10))
| ~ spl14_4
| ~ spl14_17 ),
inference(superposition,[],[f179,f122]) ).
tff(f226,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK10))
| ~ spl14_1
| ~ spl14_4
| ~ spl14_17 ),
inference(forward_demodulation,[],[f225,f109]) ).
tff(f227,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11),sK11))
| ~ spl14_1
| ~ spl14_4
| ~ spl14_16 ),
inference(forward_demodulation,[],[f224,f109]) ).
tff(f229,definition,
( spl14_26
<=> p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK10)) ),
introduced(definition,[new_symbols(definition,[spl14_26])],[avatar_definition]) ).
tff(f232,plain,
( spl14_26
| ~ spl14_1
| ~ spl14_4
| ~ spl14_17 ),
inference(avatar_split_clause,[],[f226,f177,f121,f108,f229]) ).
tff(f234,definition,
( spl14_27
<=> p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11),sK11)) ),
introduced(definition,[new_symbols(definition,[spl14_27])],[avatar_definition]) ).
tff(f236,plain,
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11),sK11))
| ~ spl14_27 ),
inference(avatar_component_clause,[],[f234]) ).
tff(f237,plain,
( spl14_27
| ~ spl14_1
| ~ spl14_4
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f227,f172,f121,f108,f234]) ).
tff(f238,plain,
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7)),sK11))
| ~ spl14_4
| spl14_16 ),
inference(forward_demodulation,[],[f173,f122]) ).
tff(f239,plain,
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),c_2Equotient_2Erespects_2E0(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7)),sK10))
| ~ spl14_4
| spl14_17 ),
inference(forward_demodulation,[],[f178,f122]) ).
tff(f240,plain,
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11),sK11))
| ~ spl14_1
| ~ spl14_4
| spl14_16 ),
inference(forward_demodulation,[],[f238,f109]) ).
tff(f241,plain,
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK10))
| ~ spl14_1
| ~ spl14_4
| spl14_17 ),
inference(forward_demodulation,[],[f239,f109]) ).
tff(f242,plain,
( ~ spl14_27
| ~ spl14_1
| ~ spl14_4
| spl14_16 ),
inference(avatar_split_clause,[],[f240,f172,f121,f108,f234]) ).
tff(f243,plain,
( ~ spl14_26
| ~ spl14_1
| ~ spl14_4
| spl14_17 ),
inference(avatar_split_clause,[],[f241,f177,f121,f108,f229]) ).
tff(f244,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] :
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2)) )
| ~ spl14_7
| ~ spl14_14 ),
inference(resolution,[],[f165,f134]) ).
tff(f246,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK11) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2)) )
| ~ spl14_5
| ~ spl14_14 ),
inference(resolution,[],[f165,f126]) ).
tff(f248,definition,
( spl14_28
<=> ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK11) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl14_28])],[avatar_definition]) ).
tff(f249,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] :
( ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2))
| ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),X0,X1,sK11) ) )
| ~ spl14_28 ),
inference(avatar_component_clause,[],[f248]) ).
tff(f250,plain,
( spl14_28
| ~ spl14_5
| ~ spl14_14 ),
inference(avatar_split_clause,[],[f246,f163,f125,f248]) ).
tff(f252,definition,
( spl14_29
<=> ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2)) ),
introduced(definition,[new_symbols(definition,[spl14_29])],[avatar_definition]) ).
tff(f253,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2))
| ~ spl14_29 ),
inference(avatar_component_clause,[],[f252]) ).
tff(f255,plain,
( spl14_29
| spl14_26
| ~ spl14_7
| ~ spl14_14 ),
inference(avatar_split_clause,[],[f244,f163,f133,f229,f252]) ).
tff(f259,plain,
( ! [X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1)),X0: tyop_2Emin_2Efun(sK0,sK1),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) != app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X0) )
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),X0))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X1,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X2)) )
| ~ spl14_8
| ~ spl14_15 ),
inference(superposition,[],[f138,f169]) ).
tff(f273,definition,
( spl14_32
<=> ! [X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1)),X0: tyop_2Emin_2Efun(sK0,sK1),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) != app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X0) )
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),X0))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X1,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
tff(f274,plain,
( ! [X2: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1)),X0: tyop_2Emin_2Efun(sK0,sK1),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10) != app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X0) )
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),X0))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X1,X0),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X1,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X2)) )
| ~ spl14_32 ),
inference(avatar_component_clause,[],[f273]) ).
tff(f275,plain,
( spl14_32
| ~ spl14_8
| ~ spl14_15 ),
inference(avatar_split_clause,[],[f259,f167,f137,f273]) ).
tff(f288,plain,
( ! [X0: $tType,X3: $tType,X2: tyop_2Emin_2Efun(X0,sK1),X1: tyop_2Emin_2Efun(sK1,X0),X4: tyop_2Emin_2Efun(sK0,X3),X5: tyop_2Emin_2Efun(X3,sK0)] :
( ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X0,sK7,X1,X2))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X3,sK4,X4,X5)) )
| ~ spl14_9
| ~ spl14_29 ),
inference(resolution,[],[f142,f253]) ).
tff(f305,definition,
( spl14_39
<=> ! [X3: $tType,X4: tyop_2Emin_2Efun(sK0,X3),X5: tyop_2Emin_2Efun(X3,sK0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X3,sK4,X4,X5)) ),
introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition]) ).
tff(f306,plain,
( ! [X3: $tType,X4: tyop_2Emin_2Efun(sK0,X3),X5: tyop_2Emin_2Efun(X3,sK0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X3,sK4,X4,X5))
| ~ spl14_39 ),
inference(avatar_component_clause,[],[f305]) ).
tff(f308,definition,
( spl14_40
<=> ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,sK1),X1: tyop_2Emin_2Efun(sK1,X0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X0,sK7,X1,X2)) ),
introduced(definition,[new_symbols(definition,[spl14_40])],[avatar_definition]) ).
tff(f309,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,sK1),X1: tyop_2Emin_2Efun(sK1,X0)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X0,sK7,X1,X2))
| ~ spl14_40 ),
inference(avatar_component_clause,[],[f308]) ).
tff(f321,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,sK0),X3: tyop_2Emin_2Efun(sK1,X1),X4: tyop_2Emin_2Efun(X1,sK1),X5: tyop_2Emin_2Efun(sK0,X0)] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK11) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X1,sK7,X3,X4))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X0,sK4,X5,X2)) )
| ~ spl14_9
| ~ spl14_28 ),
inference(resolution,[],[f249,f142]) ).
tff(f323,definition,
( spl14_41
<=> ! [X1: $tType,X0: $tType,X5: tyop_2Emin_2Efun(sK0,X0),X4: tyop_2Emin_2Efun(X1,sK1),X3: tyop_2Emin_2Efun(sK1,X1),X2: tyop_2Emin_2Efun(X0,sK0)] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK11) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X1,sK7,X3,X4))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X0,sK4,X5,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl14_41])],[avatar_definition]) ).
tff(f324,plain,
( ! [X1: $tType,X0: $tType,X2: tyop_2Emin_2Efun(X0,sK0),X3: tyop_2Emin_2Efun(sK1,X1),X4: tyop_2Emin_2Efun(X1,sK1),X5: tyop_2Emin_2Efun(sK0,X0)] :
( ( app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK10) = app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1),app_2E2(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1)),app_2E2(tyop_2Emin_2Efun(X0,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(X0,X1))),c_2Equotient_2E_2D_2D_3E_2E0(X0,sK1,sK0,X1),X2),X3),sK11) )
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,X1,sK7,X3,X4))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,X0,sK4,X5,X2)) )
| ~ spl14_41 ),
inference(avatar_component_clause,[],[f323]) ).
tff(f325,plain,
( spl14_41
| ~ spl14_9
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f321,f248,f141,f323]) ).
tff(f366,plain,
( ! [X0: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1))] :
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK10))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X0,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X1)) )
| ~ spl14_32 ),
inference(equality_resolution,[],[f274]) ).
tff(f369,definition,
( spl14_49
<=> ! [X0: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1))] :
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK10))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X0,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl14_49])],[avatar_definition]) ).
tff(f370,plain,
( ! [X0: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK2,sK3),tyop_2Emin_2Efun(sK0,sK1))] :
( ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),X0,app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),X1))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),X0,sK10),sK10)) )
| ~ spl14_49 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f371,plain,
( spl14_49
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f366,f273,f369]) ).
tff(f372,plain,
( ! [X2: tyop_2Emin_2Efun(sK3,sK1),X3: tyop_2Emin_2Efun(sK0,sK2),X0: tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),X1: tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool))] :
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,X1,sK8,X2))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,X0,X3,sK6)) )
| ~ spl14_9
| ~ spl14_49 ),
inference(resolution,[],[f370,f142]) ).
tff(f374,definition,
( spl14_50
<=> ! [X0: tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),X3: tyop_2Emin_2Efun(sK0,sK2),X2: tyop_2Emin_2Efun(sK3,sK1),X1: tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool))] :
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,X1,sK8,X2))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,X0,X3,sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
tff(f375,plain,
( ! [X2: tyop_2Emin_2Efun(sK3,sK1),X3: tyop_2Emin_2Efun(sK0,sK2),X0: tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),X1: tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool))] :
( ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK11),sK11))
| p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),X0),X1),sK10),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,X1,sK8,X2))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,X0,X3,sK6)) )
| ~ spl14_50 ),
inference(avatar_component_clause,[],[f374]) ).
tff(f376,plain,
( spl14_50
| ~ spl14_9
| ~ spl14_49 ),
inference(avatar_split_clause,[],[f372,f369,f141,f374]) ).
tff(f389,plain,
( ! [X0: tyop_2Emin_2Efun(sK3,sK1),X1: tyop_2Emin_2Efun(sK0,sK2)] :
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK11))
| ~ p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK10),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,X0))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,X1,sK6)) )
| ~ spl14_27
| ~ spl14_50 ),
inference(resolution,[],[f375,f236]) ).
tff(f391,definition,
( spl14_53
<=> ! [X1: tyop_2Emin_2Efun(sK0,sK2)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,X1,sK6)) ),
introduced(definition,[new_symbols(definition,[spl14_53])],[avatar_definition]) ).
tff(f392,plain,
( ! [X1: tyop_2Emin_2Efun(sK0,sK2)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,X1,sK6))
| ~ spl14_53 ),
inference(avatar_component_clause,[],[f391]) ).
tff(f394,definition,
( spl14_54
<=> ! [X0: tyop_2Emin_2Efun(sK3,sK1)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,X0)) ),
introduced(definition,[new_symbols(definition,[spl14_54])],[avatar_definition]) ).
tff(f395,plain,
( ! [X0: tyop_2Emin_2Efun(sK3,sK1)] : ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,X0))
| ~ spl14_54 ),
inference(avatar_component_clause,[],[f394]) ).
tff(f396,plain,
( spl14_53
| spl14_54
| ~ spl14_26
| spl14_14
| ~ spl14_27
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f389,f374,f234,f163,f229,f394,f391]) ).
tff(f397,plain,
( $false
| ~ spl14_13
| ~ spl14_54 ),
inference(resolution,[],[f395,f160]) ).
tff(f398,plain,
( ~ spl14_13
| ~ spl14_54 ),
inference(avatar_contradiction_clause,[],[f397]) ).
tff(f399,plain,
( $false
| ~ spl14_12
| ~ spl14_53 ),
inference(resolution,[],[f392,f155]) ).
tff(f400,plain,
( ~ spl14_12
| ~ spl14_53 ),
inference(avatar_contradiction_clause,[],[f399]) ).
tff(f402,plain,
( spl14_39
| spl14_40
| ~ spl14_9
| ~ spl14_29 ),
inference(avatar_split_clause,[],[f288,f252,f141,f308,f305]) ).
tff(f408,plain,
( $false
| ~ spl14_12
| ~ spl14_39 ),
inference(resolution,[],[f306,f155]) ).
tff(f409,plain,
( ~ spl14_12
| ~ spl14_39 ),
inference(avatar_contradiction_clause,[],[f408]) ).
tff(f410,plain,
( $false
| ~ spl14_13
| ~ spl14_40 ),
inference(resolution,[],[f309,f160]) ).
tff(f411,plain,
( ~ spl14_13
| ~ spl14_40 ),
inference(avatar_contradiction_clause,[],[f410]) ).
tff(f415,plain,
( ! [X0: $tType,X2: tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(sK0,sK1)),X1: tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),X0)] :
( p(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool,app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool),app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),sK11),sK11))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(tyop_2Emin_2Efun(sK0,sK1),X0,app_2E2(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool)),app_2E2(tyop_2Emin_2Efun(sK0,tyop_2Emin_2Efun(sK0,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Ebool))),c_2Equotient_2E_3D_3D_3D_3E_2E0(sK0,sK1),sK4),sK7),X1,X2)) )
| ~ spl14_6
| ~ spl14_14 ),
inference(resolution,[],[f165,f130]) ).
tff(f417,plain,
( spl14_29
| spl14_27
| ~ spl14_6
| ~ spl14_14 ),
inference(avatar_split_clause,[],[f415,f163,f129,f234,f252]) ).
tff(f427,plain,
( ! [X0: tyop_2Emin_2Efun(sK3,sK1),X1: tyop_2Emin_2Efun(sK0,sK2)] :
( sP13(app_2E2(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3),app_2E2(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3)),app_2E2(tyop_2Emin_2Efun(sK2,sK0),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,sK3),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK0,sK1),tyop_2Emin_2Efun(sK2,sK3))),c_2Equotient_2E_2D_2D_3E_2E0(sK2,sK1,sK0,sK3),sK6),sK8),sK10))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK1,sK3,sK7,sK8,X0))
| ~ p(c_2Equotient_2EQUOTIENT_2E3(sK0,sK2,sK4,X1,sK6)) )
| ~ spl14_18
| ~ spl14_41 ),
inference(superposition,[],[f184,f324]) ).
tff(f433,plain,
( spl14_53
| spl14_54
| spl14_2
| ~ spl14_18
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f427,f323,f182,f112,f394,f391]) ).
cnf(s1,plain,
spl14_1,
inference(sat_conversion,[],[f110]) ).
cnf(s2,plain,
~ spl14_2,
inference(sat_conversion,[],[f115]) ).
cnf(s4,plain,
spl14_4,
inference(sat_conversion,[],[f123]) ).
cnf(s5,plain,
spl14_5,
inference(sat_conversion,[],[f127]) ).
cnf(s6,plain,
spl14_6,
inference(sat_conversion,[],[f131]) ).
cnf(s7,plain,
spl14_7,
inference(sat_conversion,[],[f135]) ).
cnf(s8,plain,
spl14_8,
inference(sat_conversion,[],[f139]) ).
cnf(s9,plain,
spl14_9,
inference(sat_conversion,[],[f143]) ).
cnf(s14,plain,
spl14_12,
inference(sat_conversion,[],[f156]) ).
cnf(s15,plain,
spl14_13,
inference(sat_conversion,[],[f161]) ).
cnf(s16,plain,
( spl14_14
| spl14_15 ),
inference(sat_conversion,[],[f170]) ).
cnf(s17,plain,
( spl14_14
| spl14_16 ),
inference(sat_conversion,[],[f175]) ).
cnf(s18,plain,
( spl14_14
| spl14_17 ),
inference(sat_conversion,[],[f180]) ).
cnf(s19,plain,
( ~ spl14_14
| ~ spl14_16
| ~ spl14_17
| spl14_18 ),
inference(sat_conversion,[],[f185]) ).
cnf(s27,plain,
( ~ spl14_1
| ~ spl14_4
| ~ spl14_17
| spl14_26 ),
inference(sat_conversion,[],[f232]) ).
cnf(s28,plain,
( ~ spl14_1
| ~ spl14_4
| ~ spl14_16
| spl14_27 ),
inference(sat_conversion,[],[f237]) ).
cnf(s29,plain,
( ~ spl14_1
| ~ spl14_4
| spl14_16
| ~ spl14_27 ),
inference(sat_conversion,[],[f242]) ).
cnf(s30,plain,
( ~ spl14_1
| ~ spl14_4
| spl14_17
| ~ spl14_26 ),
inference(sat_conversion,[],[f243]) ).
cnf(s31,plain,
( ~ spl14_5
| ~ spl14_14
| spl14_28 ),
inference(sat_conversion,[],[f250]) ).
cnf(s33,plain,
( ~ spl14_7
| ~ spl14_14
| spl14_26
| spl14_29 ),
inference(sat_conversion,[],[f255]) ).
cnf(s36,plain,
( ~ spl14_8
| ~ spl14_15
| spl14_32 ),
inference(sat_conversion,[],[f275]) ).
cnf(s46,plain,
( ~ spl14_9
| ~ spl14_28
| spl14_41 ),
inference(sat_conversion,[],[f325]) ).
cnf(s56,plain,
( ~ spl14_32
| spl14_49 ),
inference(sat_conversion,[],[f371]) ).
cnf(s57,plain,
( ~ spl14_9
| ~ spl14_49
| spl14_50 ),
inference(sat_conversion,[],[f376]) ).
cnf(s60,plain,
( spl14_14
| ~ spl14_26
| ~ spl14_27
| ~ spl14_50
| spl14_53
| spl14_54 ),
inference(sat_conversion,[],[f396]) ).
cnf(s61,plain,
( ~ spl14_13
| ~ spl14_54 ),
inference(sat_conversion,[],[f398]) ).
cnf(s62,plain,
( ~ spl14_12
| ~ spl14_53 ),
inference(sat_conversion,[],[f400]) ).
cnf(s64,plain,
( ~ spl14_9
| ~ spl14_29
| spl14_39
| spl14_40 ),
inference(sat_conversion,[],[f402]) ).
cnf(s67,plain,
( ~ spl14_12
| ~ spl14_39 ),
inference(sat_conversion,[],[f409]) ).
cnf(s68,plain,
( ~ spl14_13
| ~ spl14_40 ),
inference(sat_conversion,[],[f411]) ).
cnf(s71,plain,
( ~ spl14_6
| ~ spl14_14
| spl14_27
| spl14_29 ),
inference(sat_conversion,[],[f417]) ).
cnf(s75,plain,
( spl14_2
| ~ spl14_18
| ~ spl14_41
| spl14_53
| spl14_54 ),
inference(sat_conversion,[],[f433]) ).
cnf(s78,plain,
~ spl14_40,
inference(rat,[],[s68,s15]) ).
cnf(s79,plain,
~ spl14_54,
inference(rat,[],[s61,s15]) ).
cnf(s80,plain,
~ spl14_39,
inference(rat,[],[s67,s14]) ).
cnf(s81,plain,
~ spl14_53,
inference(rat,[],[s62,s14]) ).
cnf(s82,plain,
~ spl14_29,
inference(rat,[],[s64,s78,s80,s9]) ).
cnf(s97,plain,
spl14_14,
inference(rat,[],[s57,s56,s60,s36,s28,s27,s16,s17,s18,s9,s81,s79,s8,s4,s1]) ).
cnf(s98,plain,
spl14_27,
inference(rat,[],[s71,s82,s6,s97]) ).
cnf(s99,plain,
spl14_26,
inference(rat,[],[s33,s82,s7,s97]) ).
cnf(s100,plain,
spl14_28,
inference(rat,[],[s31,s5,s97]) ).
cnf(s101,plain,
spl14_16,
inference(rat,[],[s29,s1,s4,s98]) ).
cnf(s102,plain,
spl14_17,
inference(rat,[],[s30,s1,s4,s99]) ).
cnf(s103,plain,
spl14_41,
inference(rat,[],[s46,s9,s100]) ).
cnf(s104,plain,
spl14_18,
inference(rat,[],[s19,s101,s97,s102]) ).
cnf(s111,plain,
$false,
inference(rat,[],[s75,s79,s81,s2,s103,s104]) ).
tff(f435,plain,
$false,
inference(avatar_sat_refutation,[],[s111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP009_3 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/10.40 % Computer : n004.cluster.edu
% 0.13/10.40 % Model : x86_64 x86_64
% 0.13/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.40 % Memory : 8046.5625MB
% 0.13/10.40 % OS : Linux 6.8.0-71-generic
% 0.04/10.40 % CPULimit : 300
% 0.04/10.40 % WCLimit : 300
% 0.04/10.40 % DateTime : Sun Sep 27 11:55:47 UTC 2026
% 0.04/10.40 % CPUTime :
% 0.04/10.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/10.44 Running first-order theorem proving
% 0.04/10.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.31/12.48 % (3392180)Detected formulas, will run a generic FOF schedule.
% 10.31/12.48 % (3392191)dis-21_1_sil=8000:lcm=predicate:random_seed=203384586:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.31/12.48 % (3392185)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2179638504:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.31/12.48 % (3392186)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3987259580:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.31/12.48 % (3392190)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4009033228:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.31/12.48 % (3392187)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1015145692:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.31/12.48 % (3392188)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1950390605:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.31/12.48 % (3392189)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=790410376:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.31/12.48 % (3392188)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.31/12.48 % (3392187)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.31/12.48 % (3392188)Refutation not found, incomplete strategy
% 10.31/12.48 % (3392188)------------------------------
% 10.31/12.48 % (3392188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/12.48 % (3392188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/12.48 % (3392188)CaDiCaL version: 2.1.3
% 10.31/12.48 % (3392188)Termination reason: Refutation not found, incomplete strategy
% 10.31/12.48 % (3392188)Time elapsed: 0.007 s
% 10.31/12.48 % (3392188)Peak memory usage: 88 MB
% 10.31/12.48 % (3392188)Instructions burned: 5 (million)
% 10.31/12.48 % (3392191)Instruction limit reached!
% 10.31/12.48 % (3392191)------------------------------
% 10.31/12.48 % (3392191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/12.48 % (3392191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/12.48 % (3392191)CaDiCaL version: 2.1.3
% 10.31/12.48 % (3392191)Termination reason: Instruction limit
% 10.31/12.48 % (3392191)Termination phase: Saturation
% 10.31/12.48 % (3392191)Time elapsed: 0.059 s
% 10.31/12.48 % (3392191)Peak memory usage: 89 MB
% 10.31/12.48 % (3392191)Instructions burned: 130 (million)
% 10.31/12.48 % (3392189)Instruction limit reached!
% 10.31/12.48 % (3392189)------------------------------
% 10.31/12.48 % (3392189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/12.48 % (3392189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/12.48 % (3392189)CaDiCaL version: 2.1.3
% 10.31/12.48 % (3392189)Termination reason: Instruction limit
% 10.31/12.48 % (3392189)Termination phase: Saturation
% 10.31/12.48 % (3392189)Time elapsed: 0.108 s
% 10.31/12.48 % (3392189)Peak memory usage: 88 MB
% 10.31/12.48 % (3392189)Instructions burned: 120 (million)
% 10.31/12.48 % (3392190)Instruction limit reached!
% 10.31/12.48 % (3392190)------------------------------
% 10.31/12.48 % (3392190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/12.48 % (3392190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/12.48 % (3392190)CaDiCaL version: 2.1.3
% 10.31/12.48 % (3392190)Termination reason: Instruction limit
% 10.31/12.48 % (3392190)Termination phase: Saturation
% 10.31/12.48 % (3392190)Time elapsed: 0.140 s
% 10.31/12.48 % (3392190)Peak memory usage: 89 MB
% 10.31/12.48 % (3392190)Instructions burned: 140 (million)
% 10.31/12.48 % (3392199)lrs+10_1_sil=8000:sp=occurrence:random_seed=2051354472:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.31/12.48 % (3392200)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2528666297:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.31/12.48 % (3392199)Instruction limit reached!
% 10.31/12.48 % (3392199)------------------------------
% 10.31/12.48 % (3392199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392199)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392199)Termination reason: Instruction limit
% 14.38/13.04 % (3392199)Termination phase: Saturation
% 14.38/13.04 % (3392199)Time elapsed: 0.138 s
% 14.38/13.04 % (3392199)Peak memory usage: 89 MB
% 14.38/13.04 % (3392199)Instructions burned: 286 (million)
% 14.38/13.04 % (3392188)------------------------------
% 14.38/13.04 % (3392188)------------------------------
% 14.38/13.04 % (3392201)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2779032458:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 14.38/13.04 % (3392200)Instruction limit reached!
% 14.38/13.04 % (3392200)------------------------------
% 14.38/13.04 % (3392200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392200)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392200)Termination reason: Instruction limit
% 14.38/13.04 % (3392200)Termination phase: Saturation
% 14.38/13.04 % (3392200)Time elapsed: 0.129 s
% 14.38/13.04 % (3392200)Peak memory usage: 90 MB
% 14.38/13.04 % (3392200)Instructions burned: 157 (million)
% 14.38/13.04 % Exception at run slice level
% 14.38/13.04 User error: GNN currently only supports monomorphic FOL.
% 14.38/13.04 % Exception at run slice level
% 14.38/13.04 User error: GNN currently only supports monomorphic FOL.
% 14.38/13.04 % (3392204)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3688058461:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 14.38/13.04 % Exception at run slice level
% 14.38/13.04 User error: GNN currently only supports monomorphic FOL.
% 14.38/13.04 % (3392206)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2471162733:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 14.38/13.04 % (3392206)Refutation not found, incomplete strategy
% 14.38/13.04 % (3392206)------------------------------
% 14.38/13.04 % (3392206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392206)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392206)Termination reason: Refutation not found, incomplete strategy
% 14.38/13.04 % (3392206)Time elapsed: 0.008 s
% 14.38/13.04 % (3392206)Peak memory usage: 89 MB
% 14.38/13.04 % (3392206)Instructions burned: 7 (million)
% 14.38/13.04 % (3392204)Instruction limit reached!
% 14.38/13.04 % (3392204)------------------------------
% 14.38/13.04 % (3392204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392204)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392204)Termination reason: Instruction limit
% 14.38/13.04 % (3392204)Termination phase: Saturation
% 14.38/13.04 % (3392204)Time elapsed: 0.111 s
% 14.38/13.04 % (3392204)Peak memory usage: 91 MB
% 14.38/13.04 % (3392204)Instructions burned: 248 (million)
% 14.38/13.04 % (3392209)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1044756764:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 14.38/13.04 % (3392201)Instruction limit reached!
% 14.38/13.04 % (3392201)------------------------------
% 14.38/13.04 % (3392201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392201)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392201)Termination reason: Instruction limit
% 14.38/13.04 % (3392201)Termination phase: Saturation
% 14.38/13.04 % (3392201)Time elapsed: 0.312 s
% 14.38/13.04 % (3392201)Peak memory usage: 90 MB
% 14.38/13.04 % (3392201)Instructions burned: 326 (million)
% 14.38/13.04 % (3392208)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3209744565:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 14.38/13.04 % (3392207)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=236766380:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 14.38/13.04 % (3392209)Instruction limit reached!
% 14.38/13.04 % (3392209)------------------------------
% 14.38/13.04 % (3392209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.38/13.04 % (3392209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/13.04 % (3392209)CaDiCaL version: 2.1.3
% 14.38/13.04 % (3392209)Termination reason: Instruction limit
% 16.59/13.68 % (3392209)Termination phase: Saturation
% 16.59/13.68 % (3392209)Time elapsed: 0.095 s
% 16.59/13.68 % (3392209)Peak memory usage: 88 MB
% 16.59/13.68 % (3392209)Instructions burned: 129 (million)
% 16.59/13.68 % (3392208)Instruction limit reached!
% 16.59/13.68 % (3392208)------------------------------
% 16.59/13.68 % (3392208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.59/13.68 % (3392208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/13.68 % (3392208)CaDiCaL version: 2.1.3
% 16.59/13.68 % (3392208)Termination reason: Instruction limit
% 16.59/13.68 % (3392208)Termination phase: Saturation
% 16.59/13.68 % (3392208)Time elapsed: 0.094 s
% 16.59/13.68 % (3392208)Peak memory usage: 89 MB
% 16.59/13.68 % (3392208)Instructions burned: 113 (million)
% 16.59/13.68 % (3392211)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3400638645:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 16.59/13.68 % (3392213)lrs+10_1_sil=8000:sp=occurrence:random_seed=3217403115:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 16.59/13.68 % (3392211)Instruction limit reached!
% 16.59/13.68 % (3392211)------------------------------
% 16.59/13.68 % (3392211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.59/13.68 % (3392211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/13.68 % (3392211)CaDiCaL version: 2.1.3
% 16.59/13.68 % (3392211)Termination reason: Instruction limit
% 16.59/13.68 % (3392211)Termination phase: Saturation
% 16.59/13.68 % (3392211)Time elapsed: 0.102 s
% 16.59/13.68 % (3392211)Peak memory usage: 88 MB
% 16.59/13.68 % (3392211)Instructions burned: 115 (million)
% 16.59/13.68 % (3392217)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=85183824:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 16.59/13.68 % (3392217)Refutation not found, incomplete strategy
% 16.59/13.68 % (3392217)------------------------------
% 16.59/13.68 % (3392217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.59/13.68 % (3392217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/13.68 % (3392217)CaDiCaL version: 2.1.3
% 16.59/13.68 % (3392217)Termination reason: Refutation not found, incomplete strategy
% 16.59/13.68 % (3392217)Time elapsed: 0.009 s
% 16.59/13.68 % (3392217)Peak memory usage: 88 MB
% 16.59/13.68 % (3392217)Instructions burned: 7 (million)
% 16.59/13.68 % (3392206)------------------------------
% 16.59/13.68 % (3392206)------------------------------
% 16.59/13.68 % (3392218)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3219841906:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 16.59/13.68 % (3392219)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1329431260:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 16.59/13.68 % (3392222)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=660422809:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 16.59/13.68 % (3392222)Refutation not found, incomplete strategy
% 16.59/13.68 % (3392222)------------------------------
% 16.59/13.68 % (3392222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.59/13.68 % (3392222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/13.68 % (3392222)CaDiCaL version: 2.1.3
% 16.59/13.68 % (3392222)Termination reason: Refutation not found, incomplete strategy
% 16.59/13.68 % (3392222)Time elapsed: 0.008 s
% 16.59/13.68 % (3392222)Peak memory usage: 89 MB
% 16.59/13.68 % (3392222)Instructions burned: 7 (million)
% 16.59/13.68 % (3392219)Instruction limit reached!
% 16.59/13.68 % (3392219)------------------------------
% 16.59/13.68 % (3392219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.59/13.68 % (3392219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/13.68 % (3392219)CaDiCaL version: 2.1.3
% 16.59/13.68 % (3392219)Termination reason: Instruction limit
% 16.59/13.68 % (3392219)Termination phase: Saturation
% 16.59/13.68 % (3392219)Time elapsed: 0.115 s
% 16.59/13.68 % (3392219)Peak memory usage: 90 MB
% 16.59/13.68 % (3392219)Instructions burned: 134 (million)
% 16.59/13.68 % (3392224)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=745757652:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 16.59/13.68 % (3392213)Instruction limit reached!
% 16.59/13.68 % (3392213)------------------------------
% 16.59/13.68 % (3392213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.73 % (3392213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.73 % (3392213)CaDiCaL version: 2.1.3
% 17.54/13.73 % (3392213)Termination reason: Instruction limit
% 17.54/13.73 % (3392213)Termination phase: Saturation
% 17.54/13.73 % (3392213)Time elapsed: 0.408 s
% 17.54/13.73 % (3392213)Peak memory usage: 92 MB
% 17.54/13.73 % (3392213)Instructions burned: 908 (million)
% 17.54/13.73 % Exception at run slice level
% 17.54/13.73 User error: GNN currently only supports monomorphic FOL.
% 17.54/13.73 % (3392217)------------------------------
% 17.54/13.73 % (3392217)------------------------------
% 17.54/13.73 % (3392232)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2978004551:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 17.54/13.73 % (3392232)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.54/13.73 % (3392232)Instruction limit reached!
% 17.54/13.73 % (3392232)------------------------------
% 17.54/13.73 % (3392232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392232)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392232)Termination reason: Instruction limit
% 17.54/13.79 % (3392232)Termination phase: Saturation
% 17.54/13.79 % (3392232)Time elapsed: 0.082 s
% 17.54/13.79 % (3392232)Peak memory usage: 89 MB
% 17.54/13.79 % (3392232)Instructions burned: 126 (million)
% 17.54/13.79 % (3392234)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1036801465:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 17.54/13.79 % Exception at run slice level
% 17.54/13.79 User error: Immediate (shared) subterms of term/literal app_2E2(X1,X0,sF16(X0,X1,X2),X3) = sF17(X1,X0,X2,X3) have different types/not well-typed!
% 17.54/13.79 % (3392222)------------------------------
% 17.54/13.79 % (3392222)------------------------------
% 17.54/13.79 % (3392235)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2267679248:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi)
% 17.54/13.79 % (3392235)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.54/13.79 % Exception at run slice level
% 17.54/13.79 User error: GNN currently only supports monomorphic FOL.
% 17.54/13.79 % (3392237)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4099483300:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi)
% 17.54/13.79 % (3392238)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=345880227:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi)
% 17.54/13.79 % (3392240)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3248011320:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi)
% 17.54/13.79 % (3392240)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.54/13.79 % (3392235)Instruction limit reached!
% 17.54/13.79 % (3392235)------------------------------
% 17.54/13.79 % (3392235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392235)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392235)Termination reason: Instruction limit
% 17.54/13.79 % (3392235)Termination phase: Saturation
% 17.54/13.79 % (3392235)Time elapsed: 0.119 s
% 17.54/13.79 % (3392235)Peak memory usage: 89 MB
% 17.54/13.79 % (3392235)Instructions burned: 142 (million)
% 17.54/13.79 % (3392240)Instruction limit reached!
% 17.54/13.79 % (3392240)------------------------------
% 17.54/13.79 % (3392240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392240)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392240)Termination reason: Instruction limit
% 17.54/13.79 % (3392240)Termination phase: Saturation
% 17.54/13.79 % (3392240)Time elapsed: 0.117 s
% 17.54/13.79 % (3392240)Peak memory usage: 90 MB
% 17.54/13.79 % (3392240)Instructions burned: 150 (million)
% 17.54/13.79 % Exception at run slice level
% 17.54/13.79 User error: GNN currently only supports monomorphic FOL.
% 17.54/13.79 % (3392241)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2084908599:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi)
% 17.54/13.79 % (3392244)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=362647125:i=667:av=off:fsr=off_2981 on theBenchmark for (2981ds/667Mi)
% 17.54/13.79 % (3392237)Instruction limit reached!
% 17.54/13.79 % (3392237)------------------------------
% 17.54/13.79 % (3392237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392237)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392237)Termination reason: Instruction limit
% 17.54/13.79 % (3392237)Termination phase: Saturation
% 17.54/13.79 % (3392237)Time elapsed: 0.384 s
% 17.54/13.79 % (3392237)Peak memory usage: 90 MB
% 17.54/13.79 % (3392237)Instructions burned: 432 (million)
% 17.54/13.79 % Exception at run slice level
% 17.54/13.79 User error: GNN currently only supports monomorphic FOL.
% 17.54/13.79 % (3392247)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3866605698:s2a=on:i=185:s2at=1.8:fdi=4_2980 on theBenchmark for (2980ds/185Mi)
% 17.54/13.79 % (3392248)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1608752537:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2979 on theBenchmark for (2979ds/193Mi)
% 17.54/13.79 % (3392250)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2414084806:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2978 on theBenchmark for (2978ds/4850Mi)
% 17.54/13.79 % (3392248)First to succeed.
% 17.54/13.79 % (3392248)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3392180"
% 17.54/13.79 % (3392247)Instruction limit reached!
% 17.54/13.79 % (3392247)------------------------------
% 17.54/13.79 % (3392247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392247)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392247)Termination reason: Instruction limit
% 17.54/13.79 % (3392247)Termination phase: Saturation
% 17.54/13.79 % (3392247)Time elapsed: 0.175 s
% 17.54/13.79 % (3392247)Peak memory usage: 91 MB
% 17.54/13.79 % (3392247)Instructions burned: 185 (million)
% 17.54/13.79 % (3392244)Instruction limit reached!
% 17.54/13.79 % (3392244)------------------------------
% 17.54/13.79 % (3392244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392244)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392244)Termination reason: Instruction limit
% 17.54/13.79 % (3392244)Termination phase: Saturation
% 17.54/13.79 % (3392244)Time elapsed: 0.363 s
% 17.54/13.79 % (3392244)Peak memory usage: 104 MB
% 17.54/13.79 % (3392244)Instructions burned: 667 (million)
% 17.54/13.79 % (3392255)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=323285420:i=319:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/319Mi)
% 17.54/13.79 % (3392252)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=144988582:i=12111:sd=1:ss=included_2977 on theBenchmark for (2977ds/12111Mi)
% 17.54/13.79 % Exception at run slice level
% 17.54/13.79 User error: GNN currently only supports monomorphic FOL.
% 17.54/13.79 % (3392258)dis-1011_128_sil=32000:random_seed=3280381084:i=3706:ep=RST:av=off_2974 on theBenchmark for (2974ds/3706Mi)
% 17.54/13.79 % (3392257)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=792139463:i=2064:ep=RST_2975 on theBenchmark for (2975ds/2064Mi)
% 17.54/13.79 % (3392258)Refutation not found, incomplete strategy
% 17.54/13.79 % (3392258)------------------------------
% 17.54/13.79 % (3392258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392258)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392258)Termination reason: Refutation not found, incomplete strategy
% 17.54/13.79 % (3392258)Time elapsed: 0.012 s
% 17.54/13.79 % (3392258)Peak memory usage: 88 MB
% 17.54/13.79 % (3392258)Instructions burned: 23 (million)
% 17.54/13.79 % (3392257)Refutation not found, incomplete strategy
% 17.54/13.79 % (3392257)------------------------------
% 17.54/13.79 % (3392257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.54/13.79 % (3392257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.54/13.79 % (3392257)CaDiCaL version: 2.1.3
% 17.54/13.79 % (3392257)Termination reason: Refutation not found, incomplete strategy
% 17.54/13.79 % (3392257)Time elapsed: 0.013 s
% 17.54/13.79 % (3392257)Peak memory usage: 89 MB
% 17.54/13.79 % (3392257)Instructions burned: 13 (million)
% 17.54/13.79 % (3392248)Refutation found. Thanks to Tanya!
% 17.54/13.79 % SZS status Theorem for theBenchmark
% 17.54/13.79 % SZS output start Proof for theBenchmark
% See solution above
% 20.04/14.09 % (3392248)------------------------------
% 20.04/14.09 % (3392248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/14.09 % (3392248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/14.09 % (3392248)CaDiCaL version: 2.1.3
% 20.04/14.09 % (3392248)Termination reason: Refutation
% 20.04/14.09 % (3392248)Time elapsed: 0.054 s
% 20.04/14.09 % (3392248)Peak memory usage: 90 MB
% 20.04/14.09 % (3392248)Instructions burned: 53 (million)
% 20.04/14.09 % (3392248)------------------------------
% 20.04/14.09 % (3392248)------------------------------
% 20.04/14.09 % (3392180)Success in time 2.857 s
% 20.04/14.09 % Vampire exiting
%------------------------------------------------------------------------------