%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP009^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:04:00 AM UTC 2026
% Result : Theorem 5.92s 1.05s
% Output : CNFRefutation 5.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 77 ( 32 unt; 0 typ; 0 def)
% Number of atoms : 180 ( 38 equ; 0 cnn)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 6061 ( 69 ~; 75 |; 16 &;5889 @)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 16 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 30 ( 28 usr; 18 con; 0-4 aty)
% Number of variables : 292 ( 0 ^; 292 !; 0 ?; 292 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
d: $tType ).
thf(decl_sort2,type,
u: $tType ).
thf(decl_sort3,type,
du: $tType ).
thf(decl_23,type,
tyop_2Emin_2Ebool: d ).
thf(decl_24,type,
tyop_2Emin_2Efun: d > d > d ).
thf(decl_25,type,
s: d > u > du ).
thf(decl_26,type,
app_2E2: du > du > u ).
thf(decl_32,type,
c_2Equotient_2E_2D_2D_3E_2E0: u ).
thf(decl_33,type,
c_2Equotient_2E_2D_2D_3E_2E2: du > du > u ).
thf(decl_34,type,
c_2Equotient_2E_2D_2D_3E_2E3: du > du > du > u ).
thf(decl_39,type,
c_2Equotient_2E_3D_3D_3D_3E_2E0: u ).
thf(decl_40,type,
c_2Equotient_2E_3D_3D_3D_3E_2E2: du > du > u ).
thf(decl_41,type,
c_2Equotient_2E_3D_3D_3D_3E_2E4: du > du > du > du > u ).
thf(decl_48,type,
c_2Equotient_2EQUOTIENT_2E3: du > du > du > u ).
thf(decl_50,type,
c_2Ecombin_2EW_2E0: u ).
thf(decl_51,type,
c_2Ecombin_2EW_2E2: du > du > u ).
thf(decl_54,type,
c_2Equotient_2Erespects_2E0: u ).
thf(decl_55,type,
c_2Equotient_2Erespects_2E2: du > du > u ).
thf(decl_69,type,
j_mono_2Etyop_2Emin_2Ebool: du > $o ).
thf(decl_72,type,
esk1_0: d ).
thf(decl_73,type,
esk2_0: d ).
thf(decl_74,type,
esk3_0: d ).
thf(decl_75,type,
esk4_0: d ).
thf(decl_76,type,
esk5_0: u ).
thf(decl_77,type,
esk6_0: u ).
thf(decl_78,type,
esk7_0: u ).
thf(decl_79,type,
esk8_0: u ).
thf(decl_80,type,
esk9_0: u ).
thf(decl_81,type,
esk10_0: u ).
thf(decl_82,type,
esk11_0: u ).
thf(decl_83,type,
esk12_0: u ).
thf(arityeq2_2Ec_2Ecombin_2EW_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
! [X1: d,X2: d,X16: u,X18: u] :
( ( s @ X2 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ X16 ) @ ( s @ X1 @ X18 ) ) )
= ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ c_2Ecombin_2EW_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ X16 ) ) ) @ ( s @ X1 @ X18 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq2_2Ec_2Ecombin_2EW_2E2_2Emono_2EA_27a_20mono_2EA_27b) ).
thf(thm_2Equotient_2Erespects__def,axiom,
! [X1: d,X2: d] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ c_2Equotient_2Erespects_2E0 )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ c_2Ecombin_2EW_2E0 ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',thm_2Equotient_2Erespects__def) ).
thf(thm_2Equotient_2EFUN__REL__EQ__REL,conjecture,
! [X1: d,X2: d,X8: d,X17: d,X34: u,X35: u,X36: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X35 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) ) ) )
=> ! [X37: u,X38: u,X39: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X39 ) ) ) )
=> ! [X40: u,X41: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) )
<=> ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) ) ) )
& ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) )
& ( ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',thm_2Equotient_2EFUN__REL__EQ__REL) ).
thf(arityeq4_2Ec_2Equotient_2E_3D_3D_3D_3E_2E4_2Emono_2EA_27a_20mono_2EA_27b,axiom,
! [X1: d,X2: d,X16: u,X18: u,X19: u,X20: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X18 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X19 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X20 ) ) ) )
<=> ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X16 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X18 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X19 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X20 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq4_2Ec_2Equotient_2E_3D_3D_3D_3E_2E4_2Emono_2EA_27a_20mono_2EA_27b) ).
thf(arityeq2_2Ec_2Equotient_2E_3D_3D_3D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
! [X1: d,X2: d,X16: u,X18: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X18 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X16 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X18 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq2_2Ec_2Equotient_2E_3D_3D_3D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27b) ).
thf(arityeq2_2Ec_2Equotient_2Erespects_2E2_2Emono_2Etyop_2Emin_2Efun_28A_27a_2CA_27b_29_20mono_2Etyop_2Emin_2Ebool,axiom,
! [X1: d,X2: d,X16: u,X18: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X18 ) ) ) )
<=> ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X16 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X18 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq2_2Ec_2Equotient_2Erespects_2E2_2Emono_2Etyop_2Emin_2Efun_28A_27a_2CA_27b_29_20mono_2Etyop_2Emin_2Ebool) ).
thf(thm_2Equotient_2EFUN__QUOTIENT,axiom,
! [X1: d,X2: d,X8: d,X17: d,X34: u,X35: u,X36: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X35 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) ) ) )
=> ! [X37: u,X38: u,X39: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X39 ) ) ) )
=> ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X35 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X39 ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',thm_2Equotient_2EFUN__QUOTIENT) ).
thf(thm_2Ecombin_2EW__THM,axiom,
! [X1: d,X2: d,X3: u,X13: u] :
( ( s @ X2 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ X3 ) @ ( s @ X1 @ X13 ) ) )
= ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ X3 ) @ ( s @ X1 @ X13 ) ) ) @ ( s @ X1 @ X13 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',thm_2Ecombin_2EW__THM) ).
thf(thm_2Equotient_2EQUOTIENT__REL,axiom,
! [X1: d,X2: d,X29: u,X30: u,X31: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X29 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X30 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X31 ) ) ) )
=> ! [X32: u,X33: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X29 ) @ ( s @ X1 @ X32 ) ) ) @ ( s @ X1 @ X33 ) ) ) )
<=> ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X29 ) @ ( s @ X1 @ X32 ) ) ) @ ( s @ X1 @ X32 ) ) ) )
& ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X29 ) @ ( s @ X1 @ X33 ) ) ) @ ( s @ X1 @ X33 ) ) ) )
& ( ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X30 ) @ ( s @ X1 @ X32 ) ) )
= ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X30 ) @ ( s @ X1 @ X33 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',thm_2Equotient_2EQUOTIENT__REL) ).
thf(arityeq3_2Ec_2Equotient_2E_2D_2D_3E_2E3_2Emono_2EA_27c_20mono_2EA_27b_20mono_2EA_27a_20mono_2EA_27d,axiom,
! [X1: d,X2: d,X8: d,X17: d,X16: u,X18: u,X19: u] :
( ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X18 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X19 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X16 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X18 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X19 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq3_2Ec_2Equotient_2E_2D_2D_3E_2E3_2Emono_2EA_27c_20mono_2EA_27b_20mono_2EA_27a_20mono_2EA_27d) ).
thf(arityeq2_2Ec_2Equotient_2E_2D_2D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27d_20mono_2EA_27c_20mono_2EA_27b,axiom,
! [X1: d,X2: d,X8: d,X17: d,X16: u,X18: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X18 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X16 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X18 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p',arityeq2_2Ec_2Equotient_2E_2D_2D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27d_20mono_2EA_27c_20mono_2EA_27b) ).
thf(c_0_11,plain,
! [X232: d,X233: d,X234: u,X235: u] :
( ( s @ X233 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X232 @ ( tyop_2Emin_2Efun @ X232 @ X233 ) ) @ X234 ) @ ( s @ X232 @ X235 ) ) )
= ( s @ X233 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X232 @ X233 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X232 @ ( tyop_2Emin_2Efun @ X232 @ X233 ) ) @ ( tyop_2Emin_2Efun @ X232 @ X233 ) ) @ c_2Ecombin_2EW_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X232 @ ( tyop_2Emin_2Efun @ X232 @ X233 ) ) @ X234 ) ) ) @ ( s @ X232 @ X235 ) ) ) ),
inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Ecombin_2EW_2E2_2Emono_2EA_27a_20mono_2EA_27b]) ).
thf(c_0_12,plain,
! [X230: d,X231: d] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X230 @ ( tyop_2Emin_2Efun @ X230 @ X231 ) ) @ ( tyop_2Emin_2Efun @ X230 @ X231 ) ) @ c_2Equotient_2Erespects_2E0 )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X230 @ ( tyop_2Emin_2Efun @ X230 @ X231 ) ) @ ( tyop_2Emin_2Efun @ X230 @ X231 ) ) @ c_2Ecombin_2EW_2E0 ) ),
inference(variable_rename,[status(thm)],[thm_2Equotient_2Erespects__def]) ).
thf(c_0_13,negated_conjecture,
~ ! [X1: d,X2: d,X8: d,X17: d,X34: u,X35: u,X36: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X35 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) ) ) )
=> ! [X37: u,X38: u,X39: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X39 ) ) ) )
=> ! [X40: u,X41: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) )
<=> ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) ) ) )
& ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X34 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X37 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) )
& ( ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X40 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X36 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X38 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X41 ) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[thm_2Equotient_2EFUN__REL__EQ__REL]) ).
thf(c_0_14,plain,
! [X190: d,X191: d,X192: u,X193: u,X194: u,X195: u] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ X192 ) @ ( s @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ X193 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X194 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X195 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ X192 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ X193 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X194 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X195 ) ) ) ) )
& ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ X192 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ X193 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X194 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X195 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X190 @ ( tyop_2Emin_2Efun @ X190 @ tyop_2Emin_2Ebool ) ) @ X192 ) @ ( s @ ( tyop_2Emin_2Efun @ X191 @ ( tyop_2Emin_2Efun @ X191 @ tyop_2Emin_2Ebool ) ) @ X193 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X194 ) @ ( s @ ( tyop_2Emin_2Efun @ X190 @ X191 ) @ X195 ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq4_2Ec_2Equotient_2E_3D_3D_3D_3E_2E4_2Emono_2EA_27a_20mono_2EA_27b])])]) ).
thf(c_0_15,plain,
! [X176: d,X177: d,X178: u,X179: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X176 @ ( tyop_2Emin_2Efun @ X176 @ tyop_2Emin_2Ebool ) ) @ X178 ) @ ( s @ ( tyop_2Emin_2Efun @ X177 @ ( tyop_2Emin_2Efun @ X177 @ tyop_2Emin_2Ebool ) ) @ X179 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X177 @ ( tyop_2Emin_2Efun @ X177 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ ( tyop_2Emin_2Efun @ X176 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X177 @ ( tyop_2Emin_2Efun @ X177 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X176 @ X177 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X176 @ ( tyop_2Emin_2Efun @ X176 @ tyop_2Emin_2Ebool ) ) @ X178 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X177 @ ( tyop_2Emin_2Efun @ X177 @ tyop_2Emin_2Ebool ) ) @ X179 ) ) ) ),
inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Equotient_2E_3D_3D_3D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27b]) ).
thf(c_0_16,plain,
! [X172: d,X173: d,X174: u,X175: u] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ X174 ) @ ( s @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ X175 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ X174 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ X175 ) ) ) ) )
& ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ X174 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ X175 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ tyop_2Emin_2Ebool ) ) @ X174 ) @ ( s @ ( tyop_2Emin_2Efun @ X172 @ X173 ) @ X175 ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Equotient_2Erespects_2E2_2Emono_2Etyop_2Emin_2Efun_28A_27a_2CA_27b_29_20mono_2Etyop_2Emin_2Ebool])])]) ).
thf(c_0_17,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( s @ X1 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) @ ( s @ X2 @ X4 ) ) )
= ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ c_2Ecombin_2EW_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) ) ) @ ( s @ X2 @ X4 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
thf(c_0_18,plain,
! [X1: d,X2: d] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ c_2Equotient_2Erespects_2E0 )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ c_2Ecombin_2EW_2E0 ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_19,plain,
! [X180: d,X181: d,X182: d,X183: d,X184: u,X185: u,X186: u,X187: u,X188: u,X189: u] :
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X180 @ ( tyop_2Emin_2Efun @ X180 @ tyop_2Emin_2Ebool ) ) @ X184 ) @ ( s @ ( tyop_2Emin_2Efun @ X180 @ X182 ) @ X185 ) @ ( s @ ( tyop_2Emin_2Efun @ X182 @ X180 ) @ X186 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X181 @ ( tyop_2Emin_2Efun @ X181 @ tyop_2Emin_2Ebool ) ) @ X187 ) @ ( s @ ( tyop_2Emin_2Efun @ X181 @ X183 ) @ X188 ) @ ( s @ ( tyop_2Emin_2Efun @ X183 @ X181 ) @ X189 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X180 @ X181 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X180 @ X181 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X180 @ ( tyop_2Emin_2Efun @ X180 @ tyop_2Emin_2Ebool ) ) @ X184 ) @ ( s @ ( tyop_2Emin_2Efun @ X181 @ ( tyop_2Emin_2Efun @ X181 @ tyop_2Emin_2Ebool ) ) @ X187 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X180 @ X181 ) @ ( tyop_2Emin_2Efun @ X182 @ X183 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X182 @ X180 ) @ X186 ) @ ( s @ ( tyop_2Emin_2Efun @ X181 @ X183 ) @ X188 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X182 @ X183 ) @ ( tyop_2Emin_2Efun @ X180 @ X181 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X180 @ X182 ) @ X185 ) @ ( s @ ( tyop_2Emin_2Efun @ X183 @ X181 ) @ X189 ) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Equotient_2EFUN__QUOTIENT])])])]) ).
thf(c_0_20,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk3_0 ) @ esk6_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) ) ) )
& ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk4_0 @ esk2_0 ) @ esk10_0 ) ) ) )
& ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) )
!= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) )
& ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) )
& ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) )
& ( ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])])]) ).
thf(c_0_21,plain,
! [X1: d,X2: d,X4: u,X5: u,X3: u,X6: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_22,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
thf(c_0_23,plain,
! [X236: d,X237: d,X238: u,X239: u] :
( ( s @ X237 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X236 @ ( tyop_2Emin_2Efun @ X236 @ X237 ) ) @ X238 ) @ ( s @ X236 @ X239 ) ) )
= ( s @ X237 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X236 @ X237 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X236 @ ( tyop_2Emin_2Efun @ X236 @ X237 ) ) @ X238 ) @ ( s @ X236 @ X239 ) ) ) @ ( s @ X236 @ X239 ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Ecombin_2EW__THM]) ).
thf(c_0_24,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_25,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) ) ) @ ( s @ X2 @ X4 ) ) )
= ( s @ X1 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) @ ( s @ X2 @ X4 ) ) ) ),
inference(rw,[status(thm)],[c_0_17,c_0_18]) ).
thf(c_0_26,plain,
! [X165: d,X166: d,X167: u,X168: u,X169: u,X170: u,X171: u] :
( ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X170 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ ( tyop_2Emin_2Efun @ X166 @ X165 ) @ X169 ) ) ) ) )
& ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X171 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ ( tyop_2Emin_2Efun @ X166 @ X165 ) @ X169 ) ) ) ) )
& ( ( ( s @ X166 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ X165 @ X170 ) ) )
= ( s @ X166 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ ( tyop_2Emin_2Efun @ X166 @ X165 ) @ X169 ) ) ) ) )
& ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X170 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X171 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ( ( s @ X166 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ X165 @ X170 ) ) )
!= ( s @ X166 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ X165 @ X171 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ X165 @ X170 ) ) ) @ ( s @ X165 @ X171 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X165 @ ( tyop_2Emin_2Efun @ X165 @ tyop_2Emin_2Ebool ) ) @ X167 ) @ ( s @ ( tyop_2Emin_2Efun @ X165 @ X166 ) @ X168 ) @ ( s @ ( tyop_2Emin_2Efun @ X166 @ X165 ) @ X169 ) ) ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Equotient_2EQUOTIENT__REL])])])])]) ).
thf(c_0_27,plain,
! [X1: d,X3: u,X4: u,X2: d,X5: u,X6: u,X7: u,X8: d,X17: d,X11: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ ( tyop_2Emin_2Efun @ X8 @ tyop_2Emin_2Ebool ) ) @ X6 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ ( tyop_2Emin_2Efun @ X2 @ X17 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X7 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X8 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X8 ) @ X11 ) ) ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ ( tyop_2Emin_2Efun @ X8 @ tyop_2Emin_2Ebool ) ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X7 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X8 ) @ X11 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
thf(c_0_28,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk4_0 @ esk2_0 ) @ esk10_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_29,plain,
! [X1: d,X2: d,X4: u,X5: u,X3: u,X6: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_21,c_0_22]) ).
thf(c_0_30,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( s @ X1 @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) @ ( s @ X2 @ X4 ) ) )
= ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ X1 ) ) @ X3 ) @ ( s @ X2 @ X4 ) ) ) @ ( s @ X2 @ X4 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
thf(c_0_31,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
thf(c_0_32,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_33,plain,
! [X1: d,X4: u,X3: u,X5: u,X2: d,X6: u,X7: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_34,negated_conjecture,
! [X1: d,X3: u,X2: d,X5: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ X2 @ esk4_0 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ esk4_0 ) @ ( tyop_2Emin_2Efun @ X1 @ esk2_0 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ esk4_0 @ esk2_0 ) @ esk10_0 ) ) ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X4 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
thf(c_0_35,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk3_0 ) @ esk6_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_36,plain,
! [X1: d,X2: d,X4: u,X5: u,X3: u,X6: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) ) ) @ c_2Equotient_2E_3D_3D_3D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_37,plain,
! [X1: d,X2: d,X4: u,X3: u,X5: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
thf(c_0_38,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
thf(c_0_39,plain,
! [X1: d,X4: u,X3: u,X5: u,X2: d,X6: u,X7: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_33,c_0_30]) ).
thf(c_0_40,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk3_0 ) @ esk6_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk4_0 @ esk2_0 ) @ esk10_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
thf(c_0_41,plain,
! [X1: d,X2: d,X4: u,X5: u,X3: u,X6: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X5 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_36,c_0_22]) ).
thf(c_0_42,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
thf(c_0_43,plain,
! [X158: d,X159: d,X160: d,X161: d,X162: u,X163: u,X164: u] :
( ( s @ ( tyop_2Emin_2Efun @ X160 @ X161 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X160 @ X158 ) @ X162 ) @ ( s @ ( tyop_2Emin_2Efun @ X159 @ X161 ) @ X163 ) @ ( s @ ( tyop_2Emin_2Efun @ X158 @ X159 ) @ X164 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X160 @ X161 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X158 @ X159 ) @ ( tyop_2Emin_2Efun @ X160 @ X161 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X159 @ X161 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X158 @ X159 ) @ ( tyop_2Emin_2Efun @ X160 @ X161 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X160 @ X158 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X159 @ X161 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X158 @ X159 ) @ ( tyop_2Emin_2Efun @ X160 @ X161 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X160 @ X158 ) @ X162 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X159 @ X161 ) @ X163 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X158 @ X159 ) @ X164 ) ) ) ),
inference(variable_rename,[status(thm)],[arityeq3_2Ec_2Equotient_2E_2D_2D_3E_2E3_2Emono_2EA_27c_20mono_2EA_27b_20mono_2EA_27a_20mono_2EA_27d]) ).
thf(c_0_44,plain,
! [X218: d,X219: d,X220: d,X221: d,X222: u,X223: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X220 @ X221 ) @ ( tyop_2Emin_2Efun @ X218 @ X219 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X218 @ X220 ) @ X222 ) @ ( s @ ( tyop_2Emin_2Efun @ X221 @ X219 ) @ X223 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X220 @ X221 ) @ ( tyop_2Emin_2Efun @ X218 @ X219 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X221 @ X219 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X220 @ X221 ) @ ( tyop_2Emin_2Efun @ X218 @ X219 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X218 @ X220 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X221 @ X219 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X220 @ X221 ) @ ( tyop_2Emin_2Efun @ X218 @ X219 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X218 @ X220 ) @ X222 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X221 @ X219 ) @ X223 ) ) ) ),
inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Equotient_2E_2D_2D_3E_2E2_2Emono_2EA_27a_20mono_2EA_27d_20mono_2EA_27c_20mono_2EA_27b]) ).
thf(c_0_45,negated_conjecture,
! [X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X4 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
thf(c_0_46,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
thf(c_0_47,plain,
! [X1: d,X4: u,X5: u,X3: u,X2: d,X6: u,X7: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X5 ) ) ) @ ( s @ X1 @ X5 ) ) ) )
| ( ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ X1 @ X4 ) ) )
!= ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_48,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_49,plain,
! [X1: d,X3: u,X2: d,X4: u,X17: d,X8: d,X5: u] :
( ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X5 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X5 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_50,plain,
! [X1: d,X2: d,X3: u,X8: d,X17: d,X4: u] :
( ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X4 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ X8 @ X17 ) ) ) ) @ c_2Equotient_2E_2D_2D_3E_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X1 ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X17 ) @ X4 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
thf(c_0_51,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ c_2Equotient_2Erespects_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_52,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_37]) ).
thf(c_0_53,plain,
! [X2: d,X1: d,X3: u,X7: u,X6: u,X5: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X5 ) ) ) )
| ( ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ X1 @ X4 ) ) )
!= ( s @ X2 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47,c_0_30]),c_0_30]) ).
thf(c_0_54,negated_conjecture,
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_31,c_0_48]) ).
thf(c_0_55,plain,
! [X1: d,X2: d,X5: u,X4: u,X3: u,X6: u,X7: u] :
( ( ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X3 ) @ ( s @ X2 @ X4 ) ) )
= ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X3 ) @ ( s @ X2 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X6 ) @ ( s @ X2 @ X4 ) ) ) @ ( s @ X2 @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X2 @ ( tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool ) ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X7 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_56,plain,
! [X1: d,X3: u,X2: d,X4: u,X17: d,X8: d,X5: u] :
( ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ ( tyop_2Emin_2Efun @ X1 @ X2 ) ) @ ( c_2Equotient_2E_2D_2D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X5 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X8 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X17 @ X2 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X8 @ X17 ) @ X5 ) ) ) ),
inference(rw,[status(thm)],[c_0_49,c_0_50]) ).
thf(c_0_57,negated_conjecture,
( ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_58,plain,
! [X1: d,X2: d,X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X4 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_51,c_0_25]) ).
thf(c_0_59,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_52]),c_0_30]) ).
thf(c_0_60,negated_conjecture,
! [X1: d,X5: u,X4: u,X3: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) )
!= ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X4 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) ) @ X5 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
thf(c_0_61,negated_conjecture,
! [X3: u,X4: u] :
( ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X4 ) ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_40]),c_0_56]),c_0_56]) ).
thf(c_0_62,negated_conjecture,
( ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_41,c_0_57]) ).
thf(c_0_63,plain,
! [X1: d,X4: u,X3: u,X5: u,X2: d,X6: u,X7: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X5 ) ) ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_64,negated_conjecture,
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) )
!= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_65,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
thf(c_0_66,negated_conjecture,
! [X1: d,X3: u,X4: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ( ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) )
!= ( s @ X1 @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X1 ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) ) @ X4 ) ) ) ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_59]),c_0_41]) ).
thf(c_0_67,negated_conjecture,
( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) )
= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
thf(c_0_68,plain,
! [X1: d,X4: u,X3: u,X5: u,X2: d,X6: u,X7: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ X1 @ X5 ) ) ) @ ( s @ X1 @ X4 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2EQUOTIENT_2E3 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ X2 ) @ X6 ) @ ( s @ ( tyop_2Emin_2Efun @ X2 @ X1 ) @ X7 ) ) ) ) ),
inference(rw,[status(thm)],[c_0_63,c_0_30]) ).
thf(c_0_69,negated_conjecture,
( ( ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) )
!= ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk4_0 ) @ ( c_2Equotient_2E_2D_2D_3E_2E3 @ ( s @ ( tyop_2Emin_2Efun @ esk3_0 @ esk1_0 ) @ esk7_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ esk4_0 ) @ esk9_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64,c_0_65])]) ).
thf(c_0_70,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_40]),c_0_56]),c_0_67]),c_0_56])]) ).
thf(c_0_71,negated_conjecture,
! [X4: u,X3: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X4 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ X3 ) ) ) ) ),
inference(spm,[status(thm)],[c_0_68,c_0_40]) ).
thf(c_0_72,negated_conjecture,
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) )
| ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69,c_0_67])]) ).
thf(c_0_73,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2E_3D_3D_3D_3E_2E4 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk11_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ),
inference(spm,[status(thm)],[c_0_29,c_0_70]) ).
thf(c_0_74,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecombin_2EW_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ),
inference(spm,[status(thm)],[c_0_71,c_0_70]) ).
thf(c_0_75,negated_conjecture,
~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Equotient_2Erespects_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ tyop_2Emin_2Ebool ) ) @ ( c_2Equotient_2E_3D_3D_3D_3E_2E2 @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ ( tyop_2Emin_2Efun @ esk1_0 @ tyop_2Emin_2Ebool ) ) @ esk5_0 ) @ ( s @ ( tyop_2Emin_2Efun @ esk2_0 @ ( tyop_2Emin_2Efun @ esk2_0 @ tyop_2Emin_2Ebool ) ) @ esk8_0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ esk1_0 @ esk2_0 ) @ esk12_0 ) ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72,c_0_73])]) ).
thf(c_0_76,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_74]),c_0_75]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP009^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n017.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:19:52 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.UoRTMTQ3tZ/E---3.1_772845.p
% 5.92/1.05 % Version: 3.5.1-ho
% 5.92/1.05 % Preprocessing class: HSLSSLSMSSSNSFA.
% 5.92/1.05 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.92/1.05 % Starting additional_ho_4 with 1500s (5) cores
% 5.92/1.05 % Starting pre_casc_8 with 300s (1) cores
% 5.92/1.05 % Starting pre_casc_5 with 300s (1) cores
% 5.92/1.05 % Starting pre_casc_6 with 300s (1) cores
% 5.92/1.05 % additional_ho_4 with pid 772858 completed with status 0
% 5.92/1.05 % Result found by additional_ho_4
% 5.92/1.05 % Preprocessing class: HSLSSLSMSSSNSFA.
% 5.92/1.05 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.92/1.05 % Starting additional_ho_4 with 1500s (5) cores
% 5.92/1.05 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 5.92/1.05 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 5.92/1.05 % Search class: HGHSM-FFLS32-DSFFFFNN
% 5.92/1.05 % partial match(2): FGHSM-FFLS32-DFFFFFNN
% 5.92/1.05 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 5.92/1.05 % Starting SubtermCWHack with 136s (1) cores
% 5.92/1.05 % Starting additional_ho_4 with 151s (1) cores
% 5.92/1.05 % Starting sh3 with 271s (1) cores
% 5.92/1.05 % Starting ho_unfolding_3 with 271s (1) cores
% 5.92/1.05 % Starting new_ho_10_cnf2 with 271s (1) cores
% 5.92/1.05 % additional_ho_4 with pid 772865 completed with status 0
% 5.92/1.05 % Result found by additional_ho_4
% 5.92/1.05 % Preprocessing class: HSLSSLSMSSSNSFA.
% 5.92/1.05 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.92/1.05 % Starting additional_ho_4 with 1500s (5) cores
% 5.92/1.05 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 5.92/1.05 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 5.92/1.05 % Search class: HGHSM-FFLS32-DSFFFFNN
% 5.92/1.05 % partial match(2): FGHSM-FFLS32-DFFFFFNN
% 5.92/1.05 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 5.92/1.05 % Starting SubtermCWHack with 136s (1) cores
% 5.92/1.05 % Starting additional_ho_4 with 151s (1) cores
% 5.92/1.05 % Preprocessing time : 0.003 s
% 5.92/1.05 % Presaturation interreduction done
% 5.92/1.05
% 5.92/1.05 % Proof found!
% 5.92/1.05 % SZS status Theorem
% 5.92/1.05 % SZS output start CNFRefutation
% See solution above
% 5.92/1.05 % Parsed axioms : 97
% 5.92/1.05 % Removed by relevancy pruning/SinE : 80
% 5.92/1.05 % Initial clauses : 31
% 5.92/1.05 % Removed in clause preprocessing : 0
% 5.92/1.05 % Initial clauses in saturation : 31
% 5.92/1.05 % Processed clauses : 1193
% 5.92/1.05 % ...of these trivial : 9
% 5.92/1.05 % ...subsumed : 973
% 5.92/1.05 % ...remaining for further processing : 211
% 5.92/1.05 % Other redundant clauses eliminated : 0
% 5.92/1.05 % Clauses deleted for lack of memory : 0
% 5.92/1.05 % Backward-subsumed : 7
% 5.92/1.05 % Backward-rewritten : 24
% 5.92/1.05 % Generated clauses : 7673
% 5.92/1.05 % ...of the previous two non-redundant : 7129
% 5.92/1.05 % ...aggressively subsumed : 0
% 5.92/1.05 % Contextual simplify-reflections : 3
% 5.92/1.05 % Paramodulations : 7656
% 5.92/1.05 % Factorizations : 0
% 5.92/1.05 % NegExts : 0
% 5.92/1.05 % Equation resolutions : 17
% 5.92/1.05 % Disequality decompositions : 0
% 5.92/1.05 % Total rewrite steps : 789
% 5.92/1.05 % ...of those cached : 277
% 5.92/1.05 % Propositional unsat checks : 0
% 5.92/1.05 % Propositional check models : 0
% 5.92/1.05 % Propositional check unsatisfiable : 0
% 5.92/1.05 % Propositional clauses : 0
% 5.92/1.05 % Propositional clauses after purity: 0
% 5.92/1.05 % Propositional unsat core size : 0
% 5.92/1.05 % Propositional preprocessing time : 0.000
% 5.92/1.05 % Propositional encoding time : 0.000
% 5.92/1.05 % Propositional solver time : 0.000
% 5.92/1.05 % Success case prop preproc time : 0.000
% 5.92/1.05 % Success case prop encoding time : 0.000
% 5.92/1.05 % Success case prop solver time : 0.000
% 5.92/1.05 % Current number of processed clauses : 156
% 5.92/1.05 % Positive orientable unit clauses : 37
% 5.92/1.05 % Positive unorientable unit clauses: 6
% 5.92/1.05 % Negative unit clauses : 1
% 5.92/1.05 % Non-unit-clauses : 112
% 5.92/1.05 % Current number of unprocessed clauses: 5978
% 5.92/1.05 % ...number of literals in the above : 13106
% 5.92/1.05 % Current number of archived formulas : 0
% 5.92/1.05 % Current number of archived clauses : 55
% 5.92/1.05 % Clause-clause subsumption calls (NU) : 10381
% 5.92/1.05 % Rec. Clause-clause subsumption calls : 9551
% 5.92/1.05 % Non-unit clause-clause subsumptions : 972
% 5.92/1.05 % Unit Clause-clause subsumption calls : 178
% 5.92/1.05 % Rewrite failures with RHS unbound : 0
% 5.92/1.05 % BW rewrite match attempts : 1218
% 5.92/1.05 % BW rewrite match successes : 11
% 5.92/1.05 % Condensation attempts : 0
% 5.92/1.05 % Condensation successes : 0
% 5.92/1.05 % Termbank termtop insertions : 780974
% 5.92/1.05 % Search garbage collected termcells : 1285
% 5.92/1.05
% 5.92/1.05 % -------------------------------------------------
% 5.92/1.05 % User time : 0.738 s
% 5.92/1.05 % System time : 0.017 s
% 5.92/1.05 % Total time : 0.755 s
% 5.92/1.05 % Maximum resident set size: 4032 pages
% 5.92/1.05
% 5.92/1.05 % -------------------------------------------------
% 5.92/1.05 % User time : 3.265 s
% 5.92/1.05 % System time : 0.076 s
% 5.92/1.05 % Total time : 3.340 s
% 5.92/1.05 % Maximum resident set size: 4864 pages
% 5.92/1.05 % E exiting
%------------------------------------------------------------------------------