%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP006_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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 : Fri Sep 25 01:47:34 PM UTC 2026
% Result : Theorem 0.65s 1.20s
% Output : CNFRefutation 0.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 2
% Syntax : Number of formulae : 25 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 1407 ( 20 equ)
% Maximal formula atoms : 32 ( 56 avg)
% Number of connectives : 265 ( 88 ~; 79 |; 76 &)
% ( 12 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of FOOLs : 1205 (1205 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 20 usr; 7 prp; 0-3 aty)
% Number of functors : 60 ( 60 usr; 24 con; 0-4 aty)
% Number of variables : 211 ( 0 sgn 163 !; 48 ?; 211 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
tyop_2Emin_2Ebool: d ).
tff(pred_def_1,type,
p: mono_2Etyop_2Emin_2Ebool > $o ).
tff(pred_def_2,type,
sP0: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_3,type,
sP1: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_4,type,
sP2: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_5,type,
sP3: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_6,type,
sP4: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_7,type,
sP5: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_8,type,
sP6: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_9,type,
sP7: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_10,type,
sP8: ( mono_2Etyop_2Emin_2Ebool * ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) ) > $o ).
tff(pred_def_11,type,
sP9: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(func_def_12,type,
c_2Emin_2E_3D_2E2: ( du * du ) > u ).
tff(func_def_13,type,
c_2Emin_2E_3D_3D_3E_2E0: u ).
tff(func_def_14,type,
c_2Emin_2E_3D_3D_3E_2E2: ( du * du ) > u ).
tff(func_def_15,type,
c_2Ebool_2E_3F_2E0: u ).
tff(func_def_16,type,
c_2Ebool_2E_3F_2E1: du > u ).
tff(func_def_17,type,
c_2Ebool_2EF_2E0: u ).
tff(func_def_18,type,
c_2EquantHeuristics_2EGUESS__EXISTS_2E0: u ).
tff(func_def_19,type,
c_2EquantHeuristics_2EGUESS__EXISTS_2E2: ( du * du ) > u ).
tff(func_def_20,type,
c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E0: u ).
tff(func_def_21,type,
c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2: ( du * du ) > u ).
tff(func_def_22,type,
c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E0: u ).
tff(func_def_23,type,
c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2: ( du * du ) > u ).
tff(func_def_24,type,
c_2EquantHeuristics_2EGUESS__FORALL_2E0: u ).
tff(func_def_25,type,
c_2EquantHeuristics_2EGUESS__FORALL_2E2: ( du * du ) > u ).
tff(func_def_26,type,
c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E0: u ).
tff(func_def_27,type,
c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2: ( du * du ) > u ).
tff(func_def_28,type,
c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0: u ).
tff(func_def_29,type,
c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2: ( du * du ) > u ).
tff(func_def_30,type,
c_2Ebool_2ET_2E0: u ).
tff(func_def_31,type,
c_2Ebool_2E_5C_2F_2E0: u ).
tff(func_def_32,type,
c_2Ebool_2E_5C_2F_2E2: ( du * du ) > u ).
tff(func_def_33,type,
c_2Ebool_2E_7E_2E0: u ).
tff(func_def_34,type,
c_2Ebool_2E_7E_2E1: du > u ).
tff(func_def_35,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_36,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Ebool * 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_2Ebool_29 ).
tff(func_def_37,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_38,type,
mono_2Ec_2Ebool_2E_2F_5C_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_39,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_40,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_41,type,
mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_42,type,
mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_43,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_44,type,
mono_2Ec_2Ebool_2E_5C_2F_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_45,type,
mono_2Ec_2Ebool_2E_7E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_46,type,
mono_2Ec_2Ebool_2E_7E_2E1: mono_2Etyop_2Emin_2Ebool > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_47,type,
i_mono_2Etyop_2Emin_2Ebool: mono_2Etyop_2Emin_2Ebool > u ).
tff(func_def_48,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_49,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_50,type,
j_mono_2Etyop_2Emin_2Ebool: du > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_51,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_52,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_53,type,
sK10: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_54,type,
sK11: ( u * d ) > u ).
tff(func_def_55,type,
sK12: ( u * d ) > u ).
tff(func_def_56,type,
sK13: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_57,type,
sK14: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_58,type,
sK15: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_59,type,
sK16: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_60,type,
sK17: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_61,type,
sK18: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_62,type,
sK19: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_63,type,
sK20: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_64,type,
sK21: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_65,type,
sK22: ( u * ( u * ( d * d ) ) ) > u ).
tff(func_def_66,type,
sK23: d ).
tff(func_def_67,type,
sK24: d ).
tff(func_def_68,type,
sK25: u ).
tff(func_def_69,type,
sK26: u ).
tff(func_def_70,type,
sK27: u ).
tff(f45,axiom,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X18: u,X19: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19)))))
<=> ! [X20: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
=> ? [X21: u] : ( s(X1,X20) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) ) )
& ! [X14: u,X15: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15)))))
<=> ! [X16: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
=> ? [X17: u] : ( s(X1,X16) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) ) )
& ! [X11: u,X12: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))))
<=> ! [X13: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13))))))) )
& ! [X8: u,X9: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9)))))
<=> ! [X10: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
<=> ! [X6: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
=> ? [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
<=> ! [X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
=> ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES) ).
tff(f57,conjecture,
! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4),s(X0,X5)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3),s(X0,X5))))) )
=> ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4))))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
tff(f58,negated_conjecture,
~ ! [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4),s(X0,X5)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3),s(X0,X5))))) )
=> ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4))))) ) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
tff(f68,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X18: u,X19: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19)))))
<=> ! [X20: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
| ? [X21: u] : ( s(X1,X20) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) ) )
& ! [X14: u,X15: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15)))))
<=> ! [X16: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
| ? [X17: u] : ( s(X1,X16) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) ) )
& ! [X11: u,X12: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))))
<=> ! [X13: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13))))))) )
& ! [X8: u,X9: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9)))))
<=> ! [X10: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
<=> ! [X6: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
| ? [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
<=> ! [X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
| ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) ) ) ),
inference(ennf_transformation,[],[f45]) ).
tff(f82,plain,
? [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4),s(X0,X5)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3),s(X0,X5))))) )
& p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3)))))
& ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4))))) ),
inference(ennf_transformation,[],[f58]) ).
tff(f83,plain,
? [X0: d,X1: d,X2: u,X3: u,X4: u] :
( ! [X5: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4),s(X0,X5)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3),s(X0,X5))))) )
& p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3)))))
& ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X0),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X4))))) ),
inference(flattening,[],[f82]) ).
tff(f134,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X18: u,X19: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19)))))
| ! [X20: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
| ? [X21: u] : ( s(X1,X20) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) ) )
& ( ? [X20: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
& ! [X21: u] : ( s(X1,X20) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19))))) ) )
& ! [X14: u,X15: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15)))))
| ! [X16: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
| ? [X17: u] : ( s(X1,X16) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) ) )
& ( ? [X16: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
& ! [X17: u] : ( s(X1,X16) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15))))) ) )
& ! [X11: u,X12: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))))
| ! [X13: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13))))))) )
& ( ? [X13: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12))))) ) )
& ! [X8: u,X9: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9)))))
| ! [X10: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10))))))) )
& ( ? [X10: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9))))) ) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X6: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
| ? [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) ) )
& ( ? [X6: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
& ! [X7: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
| ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) ) )
& ( ? [X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
& ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(nnf_transformation,[],[f68]) ).
tff(f135,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X18: u,X19: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19)))))
| ! [X20: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
| ? [X21: u] : ( s(X1,X20) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) ) )
& ( ? [X20: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))))
& ! [X21: u] : ( s(X1,X20) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(X0,X21))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X18),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19))))) ) )
& ! [X14: u,X15: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15)))))
| ! [X16: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
| ? [X17: u] : ( s(X1,X16) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) ) )
& ( ? [X16: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15),s(X1,X16)))))
& ! [X17: u] : ( s(X1,X16) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(X0,X17))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15))))) ) )
& ! [X11: u,X12: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))))
| ! [X13: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13))))))) )
& ( ? [X13: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12))))) ) )
& ! [X8: u,X9: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9)))))
| ! [X10: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10))))))) )
& ( ? [X10: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(X0,X10)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X8),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X9))))) ) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X6: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
| ? [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) ) )
& ( ? [X6: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
& ! [X7: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X4: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
| ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) ) )
& ( ? [X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
& ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(flattening,[],[f134]) ).
tff(f136,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X26: u,X27: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27)))))
| ! [X30: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27),s(X1,X30)))))
| ? [X31: u] : ( s(X1,X30) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(X0,X31))) ) ) )
& ( ? [X28: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27),s(X1,X28)))))
& ! [X29: u] : ( s(X1,X28) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(X0,X29))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27))))) ) )
& ! [X20: u,X21: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21)))))
| ! [X24: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21),s(X1,X24)))))
| ? [X25: u] : ( s(X1,X24) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(X0,X25))) ) ) )
& ( ? [X22: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21),s(X1,X22)))))
& ! [X23: u] : ( s(X1,X22) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(X0,X23))) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21))))) ) )
& ! [X16: u,X17: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17)))))
| ! [X19: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,X19))))))) )
& ( ? [X18: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,X18)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17))))) ) )
& ! [X12: u,X13: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13)))))
| ! [X15: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(X0,X15))))))) )
& ( ? [X14: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(X0,X14)))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))))) ) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X10: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X10)))))
| ? [X11: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X11))))))) ) )
& ( ? [X8: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X8)))))
& ! [X9: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X9))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X6: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
| ? [X7: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X7))))))) ) )
& ( ? [X4: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X4)))))
& ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(rectify,[],[f135]) ).
tff(f137,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ! [X26: u,X27: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27)))))
| ! [X30: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27),s(X1,X30)))))
| ( s(X1,X30) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(X0,sK22(X0,X1,X26,X30)))) ) ) )
& ( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27),s(X1,sK21(X0,X1,X26,X27))))))
& ! [X29: u] : ( s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(X0,X29))) != s(X1,sK21(X0,X1,X26,X27)) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X26),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X27))))) ) )
& ! [X20: u,X21: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21)))))
| ! [X24: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21),s(X1,X24)))))
| ( s(X1,X24) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(X0,sK20(X0,X1,X20,X24)))) ) ) )
& ( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21),s(X1,sK19(X0,X1,X20,X21))))))
& ! [X23: u] : ( s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(X0,X23))) != s(X1,sK19(X0,X1,X20,X21)) ) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X0,X1),X20),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X21))))) ) )
& ! [X16: u,X17: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17)))))
| ! [X19: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,X19))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,sK18(X0,X1,X16,X17))))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17))))) ) )
& ! [X12: u,X13: u] :
( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13)))))
| ! [X15: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(X0,X15))))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(X0,sK17(X0,X1,X12,X13))))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X12),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))))) ) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X10: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X10)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,sK16(X0,X1,X2,X3)))))))) ) )
& ( ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,sK15(X0,X1,X2,X3))))))
& ! [X9: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X9))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X6: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X6)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,sK14(X0,X1,X2,X3)))))))) ) )
& ( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,sK13(X0,X1,X2,X3))))))
& ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X5))))))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X4,sK13(X0,X1,X2,X3)),skolemize(X7,sK14(X0,X1,X2,X3)),skolemize(X8,sK15(X0,X1,X2,X3)),skolemize(X11,sK16(X0,X1,X2,X3)),skolemize(X14,sK17(X0,X1,X12,X13)),skolemize(X18,sK18(X0,X1,X16,X17)),skolemize(X22,sK19(X0,X1,X20,X21)),skolemize(X25,sK20(X0,X1,X20,X24)),skolemize(X28,sK21(X0,X1,X26,X27)),skolemize(X31,sK22(X0,X1,X26,X30))],[f136]) ).
tff(f178,plain,
( ! [X5: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27),s(sK23,X5)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26),s(sK23,X5))))) )
& p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26)))))
& ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25,sK26,sK27]),skolemize(X0,sK23),skolemize(X1,sK24),skolemize(X2,sK25),skolemize(X3,sK26),skolemize(X4,sK27)],[f83]) ).
tff(f287,plain,
! [X0: d,X1: d,X19: u,X16: u,X17: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,X19))))))) ),
inference(cnf_transformation,[],[f137]) ).
tff(f288,plain,
! [X0: d,X1: d,X16: u,X17: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(X0,sK18(X0,X1,X16,X17))))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X16),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17))))) ),
inference(cnf_transformation,[],[f137]) ).
tff(f388,plain,
! [X5: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27),s(sK23,X5)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26),s(sK23,X5))))) ),
inference(cnf_transformation,[],[f178]) ).
tff(f389,plain,
p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26))))),
inference(cnf_transformation,[],[f178]) ).
tff(f390,plain,
~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27))))),
inference(cnf_transformation,[],[f178]) ).
tcf(c_136,plain,
! [X0_u: u,X0_d: d,X1_u: u,X1_d: d] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1_d,X0_d),X1_u),s(tyop_2Emin_2Efun(X0_d,tyop_2Emin_2Ebool),X0_u)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0_d,tyop_2Emin_2Ebool),X0_u),s(X0_d,app_2E2(s(tyop_2Emin_2Efun(X1_d,X0_d),X1_u),s(X1_d,sK18(X1_d,X0_d,X1_u,X0_u)))))))) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_137,plain,
! [X0_u: u,X0_d: d,X1_u: u,X1_d: d,X2_u: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1_d,X0_d),X1_u),s(tyop_2Emin_2Efun(X0_d,tyop_2Emin_2Ebool),X0_u)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0_d,tyop_2Emin_2Ebool),X0_u),s(X0_d,app_2E2(s(tyop_2Emin_2Efun(X1_d,X0_d),X1_u),s(X1_d,X2_u))))))) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_218,negated_conjecture,
~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27))))),
inference(cnf_transformation,[],[f390]) ).
tcf(c_219,negated_conjecture,
p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26))))),
inference(cnf_transformation,[],[f389]) ).
tcf(c_220,negated_conjecture,
! [X0_u: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26),s(sK23,X0_u)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27),s(sK23,X0_u))))) ),
inference(cnf_transformation,[],[f388]) ).
tcf(c_268,plain,
! [X0_u: u,X0_d: d] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0_d,sK23),X0_u),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26),s(sK23,app_2E2(s(tyop_2Emin_2Efun(X0_d,sK23),X0_u),s(X0_d,sK18(X0_d,sK23,X0_u,sK27)))))))) ),
inference(superposition,[status(thm)],[c_136,c_220]) ).
tcf(c_278,plain,
! [X0_u: u,X0_d: d] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0_d,sK23),X0_u),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0_d,sK23),X0_u),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK26))))) ),
inference(superposition,[status(thm)],[c_268,c_137]) ).
tcf(c_294,plain,
p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK24,sK23),sK25),s(tyop_2Emin_2Efun(sK23,tyop_2Emin_2Ebool),sK27))))),
inference(superposition,[status(thm)],[c_219,c_278]) ).
tcf(c_295,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_218,c_294]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 17:28:38 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 0.65/1.20 % SZS status Started for theBenchmark.p
% 0.65/1.20 % SZS status Theorem for theBenchmark.p
% 0.65/1.20
% 0.65/1.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.65/1.20
% 0.65/1.20 % ------ iProver source info
% 0.65/1.20
% 0.65/1.20 % git: date: 2026-07-19 20:42:38 +0200
% 0.65/1.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.65/1.20 % git: non_committed_changes: false
% 0.65/1.20
% 0.65/1.20 % ------ Parsing...
% 0.65/1.20 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 0.65/1.20 % ------ Proving...
% 0.65/1.20 % ------ Problem Properties
% 0.65/1.20
% 0.65/1.20 %
% 0.65/1.20 % clauses 172
% 0.65/1.20 % conjectures 3
% 0.65/1.20 % EPR 102
% 0.65/1.20 % Horn 117
% 0.65/1.20 % unary 29
% 0.65/1.20 % binary 82
% 0.65/1.20 % lits 400
% 0.65/1.20 % lits eq 40
% 0.65/1.20 % fd_pure 1
% 0.65/1.20 % fd_pseudo 0
% 0.65/1.20 % fd_cond 4
% 0.65/1.20 % fd_pseudo_cond 4
% 0.65/1.20 % AC symbols 0
% 0.65/1.20
% 0.65/1.20 % ------ Input Options Time Limit: Unbounded
% 0.65/1.20
% 0.65/1.20
% 0.65/1.20 % ------
% 0.65/1.20 % Current options:
% 0.65/1.20 % ------
% 0.65/1.20
% 0.65/1.20
% 0.65/1.20 %
% 0.65/1.20
% 0.65/1.20 % ------ Proving...
% 0.65/1.20 %
% 0.65/1.20
% 0.65/1.20 % SZS status Theorem for theBenchmark.p
% 0.65/1.20
% 0.65/1.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.65/1.21
% 0.65/1.21
%------------------------------------------------------------------------------