%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP011_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:28:01 AM UTC 2026
% Result : Theorem 8.66s 2.08s
% Output : Refutation 9.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 19
% Syntax : Number of formulae : 162 ( 23 unt; 0 typ; 12 def)
% Number of atoms : 592 ( 293 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 643 ( 213 ~; 297 |; 106 &)
% ( 23 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 13 prp; 0-2 aty)
% Number of functors : 68 ( 68 usr; 32 con; 0-5 aty)
% Number of variables : 263 ( 0 sgn 251 !; 12 ?; 263 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
u: $tType ).
tff(type_def_6,type,
d: $tType ).
tff(type_def_7,type,
du: $tType ).
tff(type_def_8,type,
mono_2Etyop_2Emin_2Ebool: $tType ).
tff(type_def_9,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_10,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(func_def_0,type,
tyop_2Emin_2Ebool: d ).
tff(func_def_1,type,
tyop_2Emin_2Efun: ( d * d ) > d ).
tff(func_def_2,type,
tyop_2Eoption_2Eoption: d > d ).
tff(func_def_3,type,
s: ( d * u ) > du ).
tff(func_def_4,type,
app_2E2: ( du * du ) > u ).
tff(func_def_5,type,
combin_i_2E0: u ).
tff(func_def_6,type,
combin_k_2E0: u ).
tff(func_def_7,type,
combin_s_2E0: u ).
tff(func_def_8,type,
c_2Ebool_2E_21_2E0: u ).
tff(func_def_9,type,
c_2Ebool_2E_21_2E1: du > u ).
tff(func_def_10,type,
c_2Ebool_2E_2F_5C_2E0: u ).
tff(func_def_11,type,
c_2Ebool_2E_2F_5C_2E2: ( du * du ) > u ).
tff(func_def_12,type,
c_2Emin_2E_3D_2E0: u ).
tff(func_def_13,type,
c_2Emin_2E_3D_2E2: ( du * du ) > u ).
tff(func_def_14,type,
c_2Emin_2E_3D_3D_3E_2E0: u ).
tff(func_def_15,type,
c_2Emin_2E_3D_3D_3E_2E2: ( du * du ) > u ).
tff(func_def_16,type,
c_2Ebool_2E_3F_2E0: u ).
tff(func_def_17,type,
c_2Ebool_2E_3F_2E1: du > u ).
tff(func_def_18,type,
c_2Ebool_2EF_2E0: u ).
tff(func_def_19,type,
c_2Eoption_2EIS__NONE_2E0: u ).
tff(func_def_20,type,
c_2Eoption_2EIS__NONE_2E1: du > u ).
tff(func_def_21,type,
c_2Eoption_2EIS__SOME_2E0: u ).
tff(func_def_22,type,
c_2Eoption_2EIS__SOME_2E1: du > u ).
tff(func_def_23,type,
c_2Eoption_2ENONE_2E0: u ).
tff(func_def_24,type,
c_2Eoption_2EOPTION__JOIN_2E0: u ).
tff(func_def_25,type,
c_2Eoption_2EOPTION__JOIN_2E1: du > u ).
tff(func_def_26,type,
c_2Eoption_2EOPTION__MAP_2E0: u ).
tff(func_def_27,type,
c_2Eoption_2EOPTION__MAP_2E2: ( du * du ) > u ).
tff(func_def_28,type,
c_2Eoption_2EOPTREL_2E0: u ).
tff(func_def_29,type,
c_2Eoption_2EOPTREL_2E3: ( du * du * du ) > u ).
tff(func_def_30,type,
c_2Eoption_2ESOME_2E0: u ).
tff(func_def_31,type,
c_2Eoption_2ESOME_2E1: du > u ).
tff(func_def_32,type,
c_2Ebool_2ET_2E0: u ).
tff(func_def_33,type,
c_2Eoption_2ETHE_2E0: u ).
tff(func_def_34,type,
c_2Eoption_2ETHE_2E1: du > u ).
tff(func_def_35,type,
c_2Ebool_2E_5C_2F_2E0: u ).
tff(func_def_36,type,
c_2Ebool_2E_5C_2F_2E2: ( du * du ) > u ).
tff(func_def_37,type,
c_2Eoption_2Eoption__CASE_2E0: u ).
tff(func_def_38,type,
c_2Eoption_2Eoption__CASE_2E3: ( du * du * du ) > u ).
tff(func_def_39,type,
c_2Ebool_2E_7E_2E0: u ).
tff(func_def_40,type,
c_2Ebool_2E_7E_2E1: du > u ).
tff(func_def_41,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_42,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_43,type,
mono_2Ec_2Ebool_2E_2F_5C_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_44,type,
mono_2Ec_2Ebool_2E_2F_5C_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_45,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_46,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_47,type,
mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_48,type,
mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_49,type,
mono_2Ec_2Ebool_2E_5C_2F_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_50,type,
mono_2Ec_2Ebool_2E_5C_2F_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_51,type,
mono_2Ec_2Ebool_2E_7E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_52,type,
mono_2Ec_2Ebool_2E_7E_2E1: mono_2Etyop_2Emin_2Ebool > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_53,type,
i_mono_2Etyop_2Emin_2Ebool: mono_2Etyop_2Emin_2Ebool > u ).
tff(func_def_54,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_55,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_56,type,
j_mono_2Etyop_2Emin_2Ebool: du > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_57,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_58,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_59,type,
sK0: ( d * d * u * u ) > u ).
tff(func_def_60,type,
sK1: ( d * u ) > u ).
tff(func_def_61,type,
sK2: ( d * u ) > u ).
tff(func_def_62,type,
sK3: ( d * d * u * u * u ) > u ).
tff(func_def_63,type,
sK4: ( d * d * u * u * u ) > u ).
tff(func_def_64,type,
sK5: d ).
tff(func_def_65,type,
sK6: u ).
tff(func_def_66,type,
sK7: u ).
tff(func_def_67,type,
sK8: u ).
tff(pred_def_1,type,
p: mono_2Etyop_2Emin_2Ebool > $o ).
tff(f5,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ( X0 = mono_2Ec_2Ebool_2EF_2E0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ebool__cases__ax) ).
tff(f16,axiom,
! [X0: u] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,X0)))) = s(tyop_2Emin_2Ebool,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Ebool) ).
tff(f19,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0))) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Ebool) ).
tff(f51,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
<=> p(X0) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
<=> p(X0) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
<=> ~ p(X0) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
<=> ~ p(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
tff(f52,axiom,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X6))) )
<=> ( s(X0,X5) = s(X0,X6) ) )
& ! [X7: u] : ( s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7))))) = s(X0,X7) )
& ! [X8: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X8))) )
& ! [X9: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X9))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X10: u] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X10)))))) = mono_2Ec_2Ebool_2ET_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2EF_2E0 )
& ! [X11: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X11)))))
<=> ( s(tyop_2Eoption_2Eoption(X0),X11) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) )
& ! [X12: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X12)))))
<=> ( s(tyop_2Eoption_2Eoption(X0),X12) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) )
& ! [X13: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X13)))))
=> ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X13))))) = s(tyop_2Eoption_2Eoption(X0),X13) ) )
& ! [X14: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X14),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X14) )
& ! [X15: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X15) )
& ! [X16: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X16)))))
=> ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X16),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,X4) ) )
& ! [X17: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X17)))))
=> ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X17),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X17))))) ) )
& ! [X18: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X18)))))
=> ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X18),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X18) ) )
& ! [X19: u,X20: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(X1,X19),s(tyop_2Emin_2Efun(X0,X1),X20))) = s(X1,X19) )
& ! [X21: u,X22: u,X23: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X21))),s(X1,X22),s(tyop_2Emin_2Efun(X0,X1),X23))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X23),s(X0,X21))) )
& ! [X24: u,X25: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X25))))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(X0,X25))))) )
& ! [X26: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X27: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E1(s(tyop_2Eoption_2Eoption(X0),X27))))) = s(tyop_2Eoption_2Eoption(X0),X27) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2Eoption__CLAUSES) ).
tff(f53,axiom,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
<=> ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
| ? [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
& p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2EOPTREL__def) ).
tff(f54,conjecture,
! [X0: d,X1: u,X2: u,X3: u] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2ET_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2EF_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) = mono_2Ec_2Ebool_2EF_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient__option_2EOPTION__REL__def) ).
tff(f55,negated_conjecture,
~ ! [X0: d,X1: u,X2: u,X3: u] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2ET_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2EF_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) = mono_2Ec_2Ebool_2EF_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1)))) ) ),
inference(negated_conjecture,[status(cth)],[f54]) ).
tff(f64,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X6))) )
<=> ( s(X0,X5) = s(X0,X6) ) )
& ! [X7: u] : ( s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7))))) = s(X0,X7) )
& ! [X8: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X8))) )
& ! [X9: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X9))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X10: u] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X10)))))) = mono_2Ec_2Ebool_2ET_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2EF_2E0 )
& ! [X11: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X11)))))
<=> ( s(tyop_2Eoption_2Eoption(X0),X11) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) )
& ! [X12: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X12)))))
<=> ( s(tyop_2Eoption_2Eoption(X0),X12) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) )
& ! [X13: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X13))))) = s(tyop_2Eoption_2Eoption(X0),X13) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X13))))) )
& ! [X14: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X14),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X14) )
& ! [X15: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X15) )
& ! [X16: u] :
( ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X16),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,X4) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X16))))) )
& ! [X17: u] :
( ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X17),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X17))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X17))))) )
& ! [X18: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X18),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X18) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X18))))) )
& ! [X19: u,X20: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(X1,X19),s(tyop_2Emin_2Efun(X0,X1),X20))) = s(X1,X19) )
& ! [X21: u,X22: u,X23: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X21))),s(X1,X22),s(tyop_2Emin_2Efun(X0,X1),X23))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X23),s(X0,X21))) )
& ! [X24: u,X25: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X25))))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(X0,X25))))) )
& ! [X26: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X27: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E1(s(tyop_2Eoption_2Eoption(X0),X27))))) = s(tyop_2Eoption_2Eoption(X0),X27) ) ),
inference(ennf_transformation,[],[f52]) ).
tff(f65,plain,
? [X0: d,X1: u,X2: u,X3: u] :
( ( mono_2Ec_2Ebool_2ET_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))) != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1)))) ) ),
inference(ennf_transformation,[],[f55]) ).
tff(f99,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) ) ),
inference(nnf_transformation,[],[f51]) ).
tff(f100,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) ) ),
inference(flattening,[],[f99]) ).
tff(f101,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u,X6: u] :
( ( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X6))) )
| ( s(X0,X5) != s(X0,X6) ) )
& ( ( s(X0,X5) = s(X0,X6) )
| ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X6))) ) ) )
& ! [X7: u] : ( s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7))))) = s(X0,X7) )
& ! [X8: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X8))) )
& ! [X9: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X9))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X10: u] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X10)))))) = mono_2Ec_2Ebool_2ET_2E0 )
& ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))) = mono_2Ec_2Ebool_2EF_2E0 )
& ! [X11: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X11)))))
| ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),X11) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X11) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X11))))) ) )
& ! [X12: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X12)))))
| ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),X12) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X12) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X12))))) ) )
& ! [X13: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X13))))) = s(tyop_2Eoption_2Eoption(X0),X13) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X13))))) )
& ! [X14: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X14),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X14) )
& ! [X15: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Eoption_2Eoption(X0),X15),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X15) )
& ! [X16: u] :
( ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X16),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,X4) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__NONE_2E1(s(tyop_2Eoption_2Eoption(X0),X16))))) )
& ! [X17: u] :
( ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X17),s(X1,X4),s(tyop_2Emin_2Efun(X0,X1),X2))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),X17))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X17))))) )
& ! [X18: u] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),X18),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Emin_2Efun(X0,tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E0))) = s(tyop_2Eoption_2Eoption(X0),X18) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EIS__SOME_2E1(s(tyop_2Eoption_2Eoption(X0),X18))))) )
& ! [X19: u,X20: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(X1,X19),s(tyop_2Emin_2Efun(X0,X1),X20))) = s(X1,X19) )
& ! [X21: u,X22: u,X23: u] : ( s(X1,c_2Eoption_2Eoption__CASE_2E3(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X21))),s(X1,X22),s(tyop_2Emin_2Efun(X0,X1),X23))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X23),s(X0,X21))) )
& ! [X24: u,X25: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X25))))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X24),s(X0,X25))))) )
& ! [X26: u] : ( s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2EOPTION__MAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ENONE_2E0))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ! [X27: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2EOPTION__JOIN_2E1(s(tyop_2Eoption_2Eoption(tyop_2Eoption_2Eoption(X0)),c_2Eoption_2ESOME_2E1(s(tyop_2Eoption_2Eoption(X0),X27))))) = s(tyop_2Eoption_2Eoption(X0),X27) ) ),
inference(nnf_transformation,[],[f64]) ).
tff(f102,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
& ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ) ) )
& ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
| ? [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
& p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ) ),
inference(nnf_transformation,[],[f53]) ).
tff(f103,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
& ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ) ) )
& ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
| ? [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
& p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ) ),
inference(flattening,[],[f102]) ).
tff(f104,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
& ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ) ) )
& ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
| ? [X7: u,X8: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7))) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X8))) )
& p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X7))),s(X1,X8))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ) ),
inference(rectify,[],[f103]) ).
tff(f105,plain,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
& ! [X5: u,X6: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ) ) )
& ( ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) )
| ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,sK3(X0,X1,X2,X3,X4)))) )
& ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK4(X0,X1,X2,X3,X4)))) )
& p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,sK3(X0,X1,X2,X3,X4)))),s(X1,sK4(X0,X1,X2,X3,X4)))))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X7,sK3(X0,X1,X2,X3,X4)),skolemize(X8,sK4(X0,X1,X2,X3,X4))],[f104]) ).
tff(f106,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8]),skolemize(X0,sK5),skolemize(X1,sK6),skolemize(X2,sK7),skolemize(X3,sK8)],[f65]) ).
tff(f112,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(cnf_transformation,[],[f5]) ).
tff(f133,plain,
! [X0: u] : ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,X0)))) ),
inference(cnf_transformation,[],[f16]) ).
tff(f136,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0))) = X0 ),
inference(cnf_transformation,[],[f19]) ).
tff(f214,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) ),
inference(cnf_transformation,[],[f100]) ).
tff(f215,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(cnf_transformation,[],[f100]) ).
tff(f219,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 = X0 ) ),
inference(cnf_transformation,[],[f100]) ).
tff(f240,plain,
! [X0: d,X9: u] : ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X9))) ),
inference(cnf_transformation,[],[f101]) ).
tff(f242,plain,
! [X0: d,X7: u] : ( s(X0,X7) = s(X0,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7))))) ),
inference(cnf_transformation,[],[f101]) ).
tff(f245,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,sK3(X0,X1,X2,X3,X4)))),s(X1,sK4(X0,X1,X2,X3,X4))))))
| ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ),
inference(cnf_transformation,[],[f105]) ).
tff(f246,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK4(X0,X1,X2,X3,X4)))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f247,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,sK3(X0,X1,X2,X3,X4)))) )
| ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f249,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK4(X0,X1,X2,X3,X4)))) )
| ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f250,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,sK3(X0,X1,X2,X3,X4)))) )
| ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f251,plain,
! [X2: u,X3: u,X0: d,X1: d,X6: u,X4: u,X5: u] :
( ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6))) )
| ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))))
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6))))) ),
inference(cnf_transformation,[],[f105]) ).
tff(f252,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( ( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))) ),
inference(cnf_transformation,[],[f105]) ).
tff(f253,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f257,plain,
~ p(mono_2Ec_2Ebool_2EF_2E0),
inference(equality_resolution,[],[f214]) ).
tff(f262,definition,
( spl9_1
<=> ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) ) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
tff(f263,plain,
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| spl9_1 ),
inference(avatar_component_clause,[],[f262]) ).
tff(f265,definition,
( spl9_2
<=> ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) ) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
tff(f266,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| spl9_2 ),
inference(avatar_component_clause,[],[f265]) ).
tff(f268,definition,
( spl9_3
<=> ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) ) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
tff(f269,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| spl9_3 ),
inference(avatar_component_clause,[],[f268]) ).
tff(f271,definition,
( spl9_4
<=> ( mono_2Ec_2Ebool_2ET_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) ) ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
tff(f272,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| spl9_4 ),
inference(avatar_component_clause,[],[f271]) ).
tff(f273,plain,
( ~ spl9_1
| ~ spl9_2
| ~ spl9_3
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f253,f271,f268,f265,f262]) ).
tff(f274,plain,
! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Emin_2Ebool] :
( ( X0 = X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(superposition,[],[f112,f112]) ).
tff(f275,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2ET_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(equality_factoring,[],[f112]) ).
tff(f277,definition,
( spl9_5
<=> ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
tff(f278,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| ~ spl9_5 ),
inference(avatar_component_clause,[],[f277]) ).
tff(f280,definition,
( spl9_6
<=> ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0 ) ),
introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition]) ).
tff(f281,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| spl9_6 ),
inference(avatar_component_clause,[],[f280]) ).
tff(f282,plain,
( spl9_5
| ~ spl9_6 ),
inference(avatar_split_clause,[],[f275,f280,f277]) ).
tff(f310,plain,
! [X2: u,X3: d,X0: d,X1: u,X4: u,X5: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X1) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X1),s(tyop_2Eoption_2Eoption(X3),c_2Eoption_2ESOME_2E1(s(X3,X5)))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool)),X4),s(X0,X2))),s(X3,X5))))) ),
inference(equality_resolution,[],[f251]) ).
tff(f311,plain,
! [X2: u,X3: u,X0: d,X1: d,X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X3))),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X4)))))))
| ~ p(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(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X3))),s(X1,X4))))) ),
inference(equality_resolution,[],[f310]) ).
tff(f328,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_1 ),
inference(superposition,[],[f263,f274]) ).
tff(f330,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) != X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_1 ),
inference(superposition,[],[f263,f274]) ).
tff(f334,definition,
( spl9_7
<=> ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) ) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
tff(f335,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f334]) ).
tff(f341,definition,
( spl9_9
<=> ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) != X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
tff(f342,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) != X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f341]) ).
tff(f344,plain,
( spl9_7
| spl9_9
| spl9_1 ),
inference(avatar_split_clause,[],[f330,f262,f341,f334]) ).
tff(f346,definition,
( spl9_10
<=> ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition]) ).
tff(f347,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(avatar_component_clause,[],[f346]) ).
tff(f349,definition,
( spl9_11
<=> ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) ) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
tff(f350,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| spl9_11 ),
inference(avatar_component_clause,[],[f349]) ).
tff(f352,plain,
( spl9_10
| ~ spl9_11
| spl9_1 ),
inference(avatar_split_clause,[],[f328,f262,f349,f346]) ).
tff(f388,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != mono_2Ec_2Ebool_2ET_2E0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| spl9_4 ),
inference(superposition,[],[f272,f112]) ).
tff(f389,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) )
| spl9_4 ),
inference(trivial_inequality_removal,[],[f388]) ).
tff(f540,plain,
! [X2: d,X3: u,X0: d,X1: u] :
( ( s(tyop_2Eoption_2Eoption(X0),X1) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),X1),s(tyop_2Eoption_2Eoption(X2),c_2Eoption_2ENONE_2E0))))) ),
inference(equality_resolution,[],[f252]) ).
tff(f600,plain,
! [X2: u,X0: d,X1: d] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0))))),
inference(equality_resolution,[],[f540]) ).
tff(f608,plain,
! [X2: u,X0: d,X1: d] : ( mono_2Ec_2Ebool_2ET_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)))) ),
inference(resolution,[],[f600,f219]) ).
tff(f610,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| spl9_4 ),
inference(superposition,[],[f600,f389]) ).
tff(f619,plain,
( $false
| spl9_4 ),
inference(forward_subsumption_resolution,[],[f610,f257]) ).
tff(f620,plain,
spl9_4,
inference(avatar_contradiction_clause,[],[f619]) ).
tff(f624,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_3 ),
inference(superposition,[],[f269,f274]) ).
tff(f628,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0)))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_3 ),
inference(trivial_inequality_removal,[],[f624]) ).
tff(f638,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ENONE_2E0)))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_3 ),
inference(superposition,[],[f249,f628]) ).
tff(f665,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ENONE_2E0)))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f638,f215]) ).
tff(f668,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ENONE_2E0)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f665,f240]) ).
tff(f671,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f668,f240]) ).
tff(f676,plain,
( spl9_5
| spl9_3 ),
inference(avatar_split_clause,[],[f671,f268,f277]) ).
tff(f678,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_2 ),
inference(superposition,[],[f266,f274]) ).
tff(f682,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_2 ),
inference(trivial_inequality_removal,[],[f678]) ).
tff(f692,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_2 ),
inference(superposition,[],[f247,f682]) ).
tff(f709,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_2 ),
inference(forward_subsumption_resolution,[],[f692,f215]) ).
tff(f711,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_2 ),
inference(forward_subsumption_resolution,[],[f709,f240]) ).
tff(f713,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| spl9_2 ),
inference(forward_subsumption_resolution,[],[f711,f240]) ).
tff(f718,plain,
( spl9_5
| spl9_2 ),
inference(avatar_split_clause,[],[f713,f265,f277]) ).
tff(f738,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_1 ),
inference(superposition,[],[f263,f274]) ).
tff(f745,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Emin_2Ebool] :
( ( X0 != X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_9 ),
inference(superposition,[],[f342,f274]) ).
tff(f748,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ~ spl9_9 ),
inference(equality_resolution,[],[f342]) ).
tff(f753,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_9 ),
inference(forward_subsumption_resolution,[],[f745,f274]) ).
tff(f756,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X1 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_9
| spl9_11 ),
inference(forward_subsumption_resolution,[],[f753,f350]) ).
tff(f759,plain,
( spl9_5
| spl9_5
| ~ spl9_9
| spl9_11 ),
inference(avatar_split_clause,[],[f756,f349,f341,f277,f277]) ).
tff(f764,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))))
| ~ spl9_7 ),
inference(superposition,[],[f311,f335]) ).
tff(f771,plain,
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))))
| ~ spl9_7 ),
inference(forward_subsumption_resolution,[],[f764,f257]) ).
tff(f845,plain,
! [X2: u,X0: d,X1: d] : ( s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)) ),
inference(superposition,[],[f133,f608]) ).
tff(f1170,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_11 ),
inference(superposition,[],[f350,f274]) ).
tff(f1174,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_11 ),
inference(trivial_inequality_removal,[],[f1170]) ).
tff(f1196,plain,
( ! [X2: u,X0: d,X1: d] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))))
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)))) ) )
| spl9_11 ),
inference(superposition,[],[f600,f1174]) ).
tff(f1205,plain,
( ! [X2: u,X0: d,X1: d] : ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)))) )
| ~ spl9_7
| spl9_11 ),
inference(forward_subsumption_resolution,[],[f1196,f771]) ).
tff(f1212,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0))) )
| ~ spl9_7
| spl9_11 ),
inference(forward_demodulation,[],[f1205,f845]) ).
tff(f1218,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0 )
| ~ spl9_7
| spl9_11 ),
inference(forward_demodulation,[],[f1212,f136]) ).
tff(f1221,plain,
( $false
| spl9_6
| ~ spl9_7
| spl9_11 ),
inference(forward_subsumption_resolution,[],[f1218,f281]) ).
tff(f1222,plain,
( spl9_6
| ~ spl9_7
| spl9_11 ),
inference(avatar_contradiction_clause,[],[f1221]) ).
tff(f1231,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| spl9_1
| ~ spl9_7 ),
inference(forward_demodulation,[],[f738,f335]) ).
tff(f1232,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 != j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))) ) )
| spl9_1
| ~ spl9_7 ),
inference(duplicate_literal_removal,[],[f1231]) ).
tff(f1236,plain,
( ~ spl9_11
| spl9_5
| spl9_1
| ~ spl9_7 ),
inference(avatar_split_clause,[],[f1232,f334,f262,f277,f349]) ).
tff(f1265,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ spl9_5 ),
inference(superposition,[],[f600,f278]) ).
tff(f1272,plain,
( $false
| ~ spl9_5 ),
inference(forward_subsumption_resolution,[],[f1265,f257]) ).
tff(f1273,plain,
~ spl9_5,
inference(avatar_contradiction_clause,[],[f1272]) ).
tff(f1295,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(superposition,[],[f246,f347]) ).
tff(f1296,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(superposition,[],[f250,f347]) ).
tff(f1312,plain,
( ! [X2: u,X0: d,X1: d] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))))
| ( mono_2Ec_2Ebool_2EF_2E0 = j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)))) ) )
| ~ spl9_10 ),
inference(superposition,[],[f600,f347]) ).
tff(f1320,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0 )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))))
| ~ spl9_10 ),
inference(forward_demodulation,[],[f1312,f608]) ).
tff(f1326,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(forward_subsumption_resolution,[],[f1296,f215]) ).
tff(f1327,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(forward_subsumption_resolution,[],[f1295,f215]) ).
tff(f1328,plain,
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))))
| spl9_6
| ~ spl9_10 ),
inference(forward_subsumption_resolution,[],[f1320,f281]) ).
tff(f1331,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(forward_subsumption_resolution,[],[f1326,f240]) ).
tff(f1332,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) )
| ~ spl9_10 ),
inference(forward_subsumption_resolution,[],[f1327,f240]) ).
tff(f1334,definition,
( spl9_19
<=> ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) ) ),
introduced(definition,[new_symbols(definition,[spl9_19])],[avatar_definition]) ).
tff(f1335,plain,
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ~ spl9_19 ),
inference(avatar_component_clause,[],[f1334]) ).
tff(f1338,definition,
( spl9_20
<=> ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) ) ),
introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition]) ).
tff(f1339,plain,
( ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))) )
| ~ spl9_20 ),
inference(avatar_component_clause,[],[f1338]) ).
tff(f1341,plain,
( spl9_5
| spl9_19
| ~ spl9_10 ),
inference(avatar_split_clause,[],[f1331,f346,f1334,f277]) ).
tff(f1342,plain,
( spl9_5
| spl9_20
| ~ spl9_10 ),
inference(avatar_split_clause,[],[f1332,f346,f1338,f277]) ).
tff(f1353,plain,
( ( s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))) = s(sK5,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))))) )
| ~ spl9_19 ),
inference(superposition,[],[f242,f1335]) ).
tff(f1394,plain,
( ( s(sK5,sK7) = s(sK5,sK3(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))) )
| ~ spl9_19 ),
inference(forward_demodulation,[],[f1353,f242]) ).
tff(f1400,plain,
( ( s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))) = s(sK5,c_2Eoption_2ETHE_2E1(s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))))) )
| ~ spl9_20 ),
inference(superposition,[],[f242,f1339]) ).
tff(f1441,plain,
( ( s(sK5,sK6) = s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))) )
| ~ spl9_20 ),
inference(forward_demodulation,[],[f1400,f242]) ).
tff(f1460,plain,
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6))))))))
| ( s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))))
| ~ spl9_19 ),
inference(superposition,[],[f245,f1394]) ).
tff(f1477,plain,
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6))))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK7))),s(tyop_2Eoption_2Eoption(sK5),c_2Eoption_2ESOME_2E1(s(sK5,sK6)))))))
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f1460,f240]) ).
tff(f1479,plain,
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK4(sK5,sK5,sK8,c_2Eoption_2ESOME_2E1(s(sK5,sK7)),c_2Eoption_2ESOME_2E1(s(sK5,sK6))))))))
| spl9_6
| ~ spl9_10
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f1477,f1328]) ).
tff(f1481,plain,
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK5,tyop_2Emin_2Efun(sK5,tyop_2Emin_2Ebool)),sK8),s(sK5,sK7))),s(sK5,sK6)))))
| spl9_6
| ~ spl9_10
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_demodulation,[],[f1479,f1441]) ).
tff(f1483,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| spl9_6
| ~ spl9_9
| ~ spl9_10
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_demodulation,[],[f1481,f748]) ).
tff(f1486,plain,
( $false
| spl9_6
| ~ spl9_9
| ~ spl9_10
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f1483,f257]) ).
tff(f1487,plain,
( spl9_6
| ~ spl9_9
| ~ spl9_10
| ~ spl9_19
| ~ spl9_20 ),
inference(avatar_contradiction_clause,[],[f1486]) ).
cnf(s1,plain,
( ~ spl9_1
| ~ spl9_2
| ~ spl9_3
| ~ spl9_4 ),
inference(sat_conversion,[],[f273]) ).
cnf(s2,plain,
( spl9_5
| ~ spl9_6 ),
inference(sat_conversion,[],[f282]) ).
cnf(s5,plain,
( spl9_1
| spl9_7
| spl9_9 ),
inference(sat_conversion,[],[f344]) ).
cnf(s7,plain,
( spl9_1
| spl9_10
| ~ spl9_11 ),
inference(sat_conversion,[],[f352]) ).
cnf(s11,plain,
spl9_4,
inference(sat_conversion,[],[f620]) ).
cnf(s17,plain,
( spl9_3
| spl9_5 ),
inference(sat_conversion,[],[f676]) ).
cnf(s19,plain,
( spl9_2
| spl9_5 ),
inference(sat_conversion,[],[f718]) ).
cnf(s26,plain,
( spl9_5
| spl9_5
| ~ spl9_9
| spl9_11 ),
inference(sat_conversion,[],[f759]) ).
cnf(s27,plain,
( spl9_5
| ~ spl9_9
| spl9_11 ),
inference(rat,[],[s26]) ).
cnf(s31,plain,
( spl9_6
| ~ spl9_7
| spl9_11 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s37,plain,
( spl9_1
| spl9_5
| ~ spl9_7
| ~ spl9_11 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s43,plain,
~ spl9_5,
inference(sat_conversion,[],[f1273]) ).
cnf(s47,plain,
( spl9_5
| ~ spl9_10
| spl9_19 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s48,plain,
( spl9_5
| ~ spl9_10
| spl9_20 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s50,plain,
( spl9_6
| ~ spl9_9
| ~ spl9_10
| ~ spl9_19
| ~ spl9_20 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s51,plain,
( spl9_1
| ~ spl9_7
| ~ spl9_11 ),
inference(rat,[],[s37,s43]) ).
cnf(s54,plain,
( ~ spl9_9
| spl9_11 ),
inference(rat,[],[s27,s43]) ).
cnf(s57,plain,
spl9_2,
inference(rat,[],[s19,s43]) ).
cnf(s58,plain,
spl9_3,
inference(rat,[],[s17,s43]) ).
cnf(s59,plain,
~ spl9_6,
inference(rat,[],[s2,s43]) ).
cnf(s60,plain,
~ spl9_1,
inference(rat,[],[s1,s11,s58,s57]) ).
cnf(s61,plain,
~ spl9_9,
inference(rat,[],[s50,s47,s48,s7,s54,s59,s43,s60]) ).
cnf(s62,plain,
spl9_7,
inference(rat,[],[s5,s60,s61]) ).
cnf(s64,plain,
~ spl9_11,
inference(rat,[],[s51,s60,s62]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s31,s59,s64,s62]) ).
tff(f1488,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP011_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n011.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 11:57:30 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.66/2.08 % (2267787)Detected formulas, will run a generic FOF schedule.
% 8.66/2.08 % (2267794)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1605433073:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.66/2.08 % (2267796)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2063916496:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.66/2.08 % (2267792)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2517217623:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.66/2.08 % (2267798)dis-21_1_sil=8000:lcm=predicate:random_seed=2682568959:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.66/2.08 % (2267793)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1967080873:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.66/2.08 % (2267795)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=84158640:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.66/2.08 % (2267797)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=634510730:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.66/2.08 % (2267795)Refutation not found, incomplete strategy
% 8.66/2.08 % (2267795)------------------------------
% 8.66/2.08 % (2267795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267795)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267795)Termination reason: Refutation not found, incomplete strategy
% 8.66/2.08 % (2267795)Time elapsed: 0.011 s
% 8.66/2.08 % (2267795)Peak memory usage: 88 MB
% 8.66/2.08 % (2267795)Instructions burned: 16 (million)
% 8.66/2.08 % (2267796)Instruction limit reached!
% 8.66/2.08 % (2267796)------------------------------
% 8.66/2.08 % (2267796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267796)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267796)Termination reason: Instruction limit
% 8.66/2.08 % (2267796)Termination phase: Saturation
% 8.66/2.08 % (2267796)Time elapsed: 0.061 s
% 8.66/2.08 % (2267796)Peak memory usage: 87 MB
% 8.66/2.08 % (2267796)Instructions burned: 120 (million)
% 8.66/2.08 % (2267798)Instruction limit reached!
% 8.66/2.08 % (2267798)------------------------------
% 8.66/2.08 % (2267798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267798)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267798)Termination reason: Instruction limit
% 8.66/2.08 % (2267798)Termination phase: Saturation
% 8.66/2.08 % (2267798)Time elapsed: 0.079 s
% 8.66/2.08 % (2267798)Peak memory usage: 89 MB
% 8.66/2.08 % (2267798)Instructions burned: 129 (million)
% 8.66/2.08 % (2267797)Instruction limit reached!
% 8.66/2.08 % (2267797)------------------------------
% 8.66/2.08 % (2267797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267797)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267797)Termination reason: Instruction limit
% 8.66/2.08 % (2267797)Termination phase: Saturation
% 8.66/2.08 % (2267797)Time elapsed: 0.085 s
% 8.66/2.08 % (2267797)Peak memory usage: 90 MB
% 8.66/2.08 % (2267797)Instructions burned: 140 (million)
% 8.66/2.08 % (2267806)lrs+10_1_sil=8000:sp=occurrence:random_seed=606314512:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.66/2.08 % (2267807)lrs+10_1_sil=32000:urr=on:br=off:random_seed=589987929:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.66/2.08 % (2267808)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3326668290:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.66/2.08 % (2267795)------------------------------
% 8.66/2.08 % (2267795)------------------------------
% 8.66/2.08 % (2267807)Instruction limit reached!
% 8.66/2.08 % (2267807)------------------------------
% 8.66/2.08 % (2267807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267807)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267807)Termination reason: Instruction limit
% 8.66/2.08 % (2267807)Termination phase: Saturation
% 8.66/2.08 % (2267807)Time elapsed: 0.071 s
% 8.66/2.08 % (2267807)Peak memory usage: 89 MB
% 8.66/2.08 % (2267807)Instructions burned: 157 (million)
% 8.66/2.08 % (2267806)Instruction limit reached!
% 8.66/2.08 % (2267806)------------------------------
% 8.66/2.08 % (2267806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267806)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267806)Termination reason: Instruction limit
% 8.66/2.08 % (2267806)Termination phase: Saturation
% 8.66/2.08 % (2267806)Time elapsed: 0.134 s
% 8.66/2.08 % (2267806)Peak memory usage: 89 MB
% 8.66/2.08 % (2267806)Instructions burned: 286 (million)
% 8.66/2.08 % (2267812)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=911304817:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.66/2.08 % (2267808)Instruction limit reached!
% 8.66/2.08 % (2267808)------------------------------
% 8.66/2.08 % (2267808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267808)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267808)Termination reason: Instruction limit
% 8.66/2.08 % (2267808)Termination phase: Saturation
% 8.66/2.08 % (2267808)Time elapsed: 0.178 s
% 8.66/2.08 % (2267808)Peak memory usage: 90 MB
% 8.66/2.08 % (2267808)Instructions burned: 326 (million)
% 8.66/2.08 % (2267813)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=7165408:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.66/2.08 % (2267814)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2219785828:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 8.66/2.08 % (2267816)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3312973277:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 8.66/2.08 % (2267812)Instruction limit reached!
% 8.66/2.08 % (2267812)------------------------------
% 8.66/2.08 % (2267812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267812)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267812)Termination reason: Instruction limit
% 8.66/2.08 % (2267812)Termination phase: Saturation
% 8.66/2.08 % (2267812)Time elapsed: 0.150 s
% 8.66/2.08 % (2267812)Peak memory usage: 90 MB
% 8.66/2.08 % (2267812)Instructions burned: 249 (million)
% 8.66/2.08 % (2267813)Instruction limit reached!
% 8.66/2.08 % (2267813)------------------------------
% 8.66/2.08 % (2267813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267813)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267813)Termination reason: Instruction limit
% 8.66/2.08 % (2267813)Termination phase: Saturation
% 8.66/2.08 % (2267813)Time elapsed: 0.160 s
% 8.66/2.08 % (2267813)Peak memory usage: 89 MB
% 8.66/2.08 % (2267813)Instructions burned: 295 (million)
% 8.66/2.08 % (2267816)Instruction limit reached!
% 8.66/2.08 % (2267816)------------------------------
% 8.66/2.08 % (2267816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267816)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267816)Termination reason: Instruction limit
% 8.66/2.08 % (2267816)Termination phase: Saturation
% 8.66/2.08 % (2267816)Time elapsed: 0.060 s
% 8.66/2.08 % (2267816)Peak memory usage: 89 MB
% 8.66/2.08 % (2267816)Instructions burned: 113 (million)
% 8.66/2.08 % (2267820)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=366199960:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 8.66/2.08 % (2267820)Refutation not found, incomplete strategy
% 8.66/2.08 % (2267820)------------------------------
% 8.66/2.08 % (2267820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267820)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267820)Termination reason: Refutation not found, incomplete strategy
% 8.66/2.08 % (2267820)Time elapsed: 0.005 s
% 8.66/2.08 % (2267820)Peak memory usage: 88 MB
% 8.66/2.08 % (2267820)Instructions burned: 8 (million)
% 8.66/2.08 % (2267821)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1261986058:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 8.66/2.08 % (2267822)lrs+10_1_sil=8000:sp=occurrence:random_seed=246601120:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 8.66/2.08 % (2267821)Instruction limit reached!
% 8.66/2.08 % (2267821)------------------------------
% 8.66/2.08 % (2267821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267821)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267821)Termination reason: Instruction limit
% 8.66/2.08 % (2267821)Termination phase: Saturation
% 8.66/2.08 % (2267821)Time elapsed: 0.059 s
% 8.66/2.08 % (2267821)Peak memory usage: 88 MB
% 8.66/2.08 % (2267821)Instructions burned: 116 (million)
% 8.66/2.08 % (2267793)First to succeed.
% 8.66/2.08 % (2267793)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2267787"
% 8.66/2.08 % (2267826)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3443332884:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 8.66/2.08 % (2267826)Refutation not found, incomplete strategy
% 8.66/2.08 % (2267826)------------------------------
% 8.66/2.08 % (2267826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.08 % (2267826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.08 % (2267826)CaDiCaL version: 2.1.3
% 8.66/2.08 % (2267826)Termination reason: Refutation not found, incomplete strategy
% 8.66/2.08 % (2267826)Time elapsed: 0.011 s
% 8.66/2.08 % (2267826)Peak memory usage: 88 MB
% 8.66/2.08 % (2267826)Instructions burned: 18 (million)
% 8.66/2.08 % (2267820)------------------------------
% 8.66/2.08 % (2267820)------------------------------
% 8.66/2.08 % (2267828)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=146712741:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.66/2.08 % (2267793)Refutation found. Thanks to Tanya!
% 8.66/2.08 % SZS status Theorem for theBenchmark
% 8.66/2.08 % SZS output start Proof for theBenchmark
% See solution above
% 9.12/2.27 % (2267793)------------------------------
% 9.12/2.27 % (2267793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.12/2.27 % (2267793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.12/2.27 % (2267793)CaDiCaL version: 2.1.3
% 9.12/2.27 % (2267793)Termination reason: Refutation
% 9.12/2.27 % (2267793)Time elapsed: 0.796 s
% 9.12/2.27 % (2267793)Peak memory usage: 132 MB
% 9.12/2.27 % (2267793)Instructions burned: 1219 (million)
% 9.12/2.27 % (2267793)------------------------------
% 9.12/2.27 % (2267793)------------------------------
% 9.12/2.27 % (2267787)Success in time 1.214 s
% 9.12/2.27 % Vampire exiting
%------------------------------------------------------------------------------