%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 08:45:23 AM UTC 2026
% Result : Theorem 31.05s 31.38s
% Output : Proof 31.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 2
% Syntax : Number of formulae : 39 ( 8 unt; 0 def)
% Number of atoms : 536 ( 58 equ)
% Maximal formula atoms : 44 ( 13 avg)
% Number of connectives : 758 ( 261 ~; 246 |; 235 &)
% ( 6 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 10 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-5 aty)
% Number of functors : 25 ( 25 usr; 6 con; 0-5 aty)
% Number of variables : 927 ( 1 sgn 818 !; 99 ?)
% Comments :
%------------------------------------------------------------------------------
fof(thm_2EquantHeuristics_2EGUESS__REWRITES,axiom,
! [A_27a,A_27b,V0i_2E0,V1P_2E0] :
( ! [V16i_2E0,V17P_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0))))
<=> ! [V18v_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,V18v_2E0))))
=> ? [V19fv_2E0] : s(A_27b,V18v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0))) ) )
& ! [V12i_2E0,V13P_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0))))
<=> ! [V14v_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,V14v_2E0))))
=> ? [V15fv_2E0] : s(A_27b,V14v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0))) ) )
& ! [V9i_2E0,V10P_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0))))
<=> ! [V11fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(A_27a,V11fv_2E0)))))) )
& ! [V6i_2E0,V7P_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0))))
<=> ! [V8fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(A_27a,V8fv_2E0)))))) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0))))
<=> ! [V4v_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V4v_2E0))))
=> ? [V5fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V5fv_2E0)))))) ) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0))))
<=> ! [V2v_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V2v_2E0))))
=> ? [V3fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V3fv_2E0)))))) ) ) ),
file('theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES) ).
fof(thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,conjecture,
! [A_27a,A_27b,V0i_2E0,V1P_2E0,V2Q_2E0] :
( ! [V3x_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0),s(A_27a,V3x_2E0))))
=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V3x_2E0)))) )
=> ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0))))
=> p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0)))) ) ),
file('theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
fof(f_37_1,plain,
! [A_27a,A_27b,V0i_2E0,V1P_2E0] :
( ! [V16i_2E0,V17P_2E0] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0))))
| ? [V18v_2E0] :
( ! [V19fv_2E0] : s(A_27b,V18v_2E0) != s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,V18v_2E0)))) ) )
& ( ! [V18v_2E0] :
( ? [V19fv_2E0] : s(A_27b,V18v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,V18v_2E0)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0)))) ) )
& ! [V12i_2E0,V13P_2E0] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0))))
| ? [V14v_2E0] :
( ! [V15fv_2E0] : s(A_27b,V14v_2E0) != s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,V14v_2E0)))) ) )
& ( ! [V14v_2E0] :
( ? [V15fv_2E0] : s(A_27b,V14v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,V14v_2E0)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0)))) ) )
& ! [V9i_2E0,V10P_2E0] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0))))
| ? [V11fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(A_27a,V11fv_2E0)))))) )
& ( ! [V11fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(A_27a,V11fv_2E0))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0)))) ) )
& ! [V6i_2E0,V7P_2E0] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0))))
| ? [V8fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(A_27a,V8fv_2E0)))))) )
& ( ! [V8fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(A_27a,V8fv_2E0))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0)))) ) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0))))
| ? [V4v_2E0] :
( ! [V5fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V5fv_2E0))))))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V4v_2E0)))) ) )
& ( ! [V4v_2E0] :
( ? [V5fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V5fv_2E0))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V4v_2E0)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0)))) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0))))
| ? [V2v_2E0] :
( ! [V3fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V3fv_2E0))))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V2v_2E0)))) ) )
& ( ! [V2v_2E0] :
( ? [V3fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V3fv_2E0))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V2v_2E0)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0)))) ) ),
inference(fof_nnf,[status(thm)],[thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
fof(f_37_2,plain,
! [U_215,U_214,U_213,U_212] :
( ! [U_211,U_210] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_211),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_210))))
| ? [U_209] :
( ! [U_208] : s(U_214,U_209) != s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_211),s(U_215,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_210),s(U_214,U_209)))) ) )
& ( ! [U_207] :
( ? [U_206] : s(U_214,U_207) = s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_211),s(U_215,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_210),s(U_214,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_211),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_210)))) ) )
& ! [U_205,U_204] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_205),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_204))))
| ? [U_203] :
( ! [U_202] : s(U_214,U_203) != s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_205),s(U_215,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_204),s(U_214,U_203)))) ) )
& ( ! [U_201] :
( ? [U_200] : s(U_214,U_201) = s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_205),s(U_215,U_200)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_204),s(U_214,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_205),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_204)))) ) )
& ! [U_199,U_198] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_199),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_198))))
| ? [U_197] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_198),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_199),s(U_215,U_197)))))) )
& ( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_198),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_199),s(U_215,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_199),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_198)))) ) )
& ! [U_195,U_194] :
( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_195),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_194))))
| ? [U_193] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_194),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_195),s(U_215,U_193)))))) )
& ( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_194),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_195),s(U_215,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_195),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_194)))) ) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212))))
| ? [U_191] :
( ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(U_215,U_190))))))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,U_191)))) ) )
& ( ! [U_189] :
( ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(U_215,U_188))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,U_189)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212)))) )
& ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212))))
| ? [U_187] :
( ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(U_215,U_186))))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,U_187)))) ) )
& ( ! [U_185] :
( ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,app_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(U_215,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212),s(U_214,U_185)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_215,U_214),U_213),s(tyop_2Emin_2Efun(U_214,tyop_2Emin_2Ebool),U_212)))) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( ? [U_206] : s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ? [U_203] :
( ! [U_202] : s(U_254,U_203) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,U_203)))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( ? [U_200] : s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,U_200)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| ? [U_197] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,U_197)))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ? [U_193] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,U_193)))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
fof(f_37_4,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( ? [U_206] : s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ? [U_203] :
( ! [U_202] : s(U_254,U_203) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,U_203)))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( ? [U_200] : s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,U_200)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| ? [U_197] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,U_197)))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_193,sK4(U_269,U_250,U_219,U_217))],[f_37_3]) ).
fof(f_37_5,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( ? [U_206] : s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ? [U_203] :
( ! [U_202] : s(U_254,U_203) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,U_203)))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( ? [U_200] : s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,U_200)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_197,sK5(U_271,U_252,U_223,U_221))],[f_37_4]) ).
fof(f_37_6,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( ? [U_206] : s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ? [U_203] :
( ! [U_202] : s(U_254,U_203) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,U_203)))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_200,sK6(U_272,U_253,U_226,U_224,U_201))],[f_37_5]) ).
fof(f_37_7,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( ? [U_206] : s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,U_206)))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_203,sK7(U_273,U_254,U_227,U_225))],[f_37_6]) ).
fof(f_37_8,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ? [U_209] :
( ! [U_208] : s(U_256,U_209) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,U_209)))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_206,sK8(U_274,U_255,U_230,U_228,U_207))],[f_37_7]) ).
fof(f_37_9,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| ? [U_184] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,U_184))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ( ! [U_208] : s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229))))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_209,sK9(U_275,U_256,U_231,U_229))],[f_37_8]) ).
fof(f_37_10,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( ? [U_187] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,U_187))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,sK10(U_278,U_259,U_240,U_234)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ( ! [U_208] : s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229))))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_184,sK10(U_278,U_259,U_240,U_234))],[f_37_9]) ).
fof(f_37_11,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ? [U_188] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,U_188))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,sK11(U_279,U_260,U_241,U_235)))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,sK10(U_278,U_259,U_240,U_234)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ( ! [U_208] : s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229))))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_187,sK11(U_279,U_260,U_241,U_235))],[f_37_10]) ).
fof(f_37_12,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ? [U_191] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,U_191))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,sK12(U_280,U_261,U_242,U_236)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,sK11(U_279,U_260,U_241,U_235)))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,sK10(U_278,U_259,U_240,U_234)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ( ! [U_208] : s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229))))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_188,sK12(U_280,U_261,U_242,U_236))],[f_37_11]) ).
fof(f_37_13,plain,
( ! [U_281,U_262,U_243,U_237] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,sK13(U_281,U_262,U_243,U_237)))))
& ! [U_190] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190)))))) ) )
& ! [U_280,U_261,U_242,U_236] :
( ! [U_189] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,sK12(U_280,U_261,U_242,U_236)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_279,U_260,U_241,U_235] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,sK11(U_279,U_260,U_241,U_235)))))
& ! [U_186] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186)))))) ) )
& ! [U_278,U_259,U_240,U_234] :
( ! [U_185] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,sK10(U_278,U_259,U_240,U_234)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_275,U_256,U_231,U_229] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| ( ! [U_208] : s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229))))) ) )
& ! [U_274,U_255,U_230,U_228] :
( ! [U_207] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_273,U_254,U_227,U_225] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| ( ! [U_202] : s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225))))) ) )
& ! [U_272,U_253,U_226,U_224] :
( ! [U_201] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_271,U_252,U_223,U_221] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_270,U_251,U_222,U_220] :
( ! [U_196] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_269,U_250,U_219,U_217] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_268,U_249,U_218,U_216] :
( ! [U_192] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_191,sK13(U_281,U_262,U_243,U_237))],[f_37_12]) ).
fof(f_37_14,plain,
( ! [U_190,U_237,U_243,U_262,U_281] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,sK13(U_281,U_262,U_243,U_237)))))
| ~ sP22(U_190,U_237,U_243,U_262,U_281) )
& ! [U_190,U_237,U_243,U_262,U_281] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237),s(U_262,app_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(U_281,U_190))))))
| ~ sP22(U_190,U_237,U_243,U_262,U_281) )
& ! [U_186,U_235,U_241,U_260,U_279] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,sK11(U_279,U_260,U_241,U_235)))))
| ~ sP21(U_186,U_235,U_241,U_260,U_279) )
& ! [U_186,U_235,U_241,U_260,U_279] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235),s(U_260,app_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(U_279,U_186))))))
| ~ sP21(U_186,U_235,U_241,U_260,U_279) )
& ! [U_208,U_256,U_275,U_229,U_231] :
( s(U_256,sK9(U_275,U_256,U_231,U_229)) != s(U_256,app_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(U_275,U_208)))
| ~ sP20(U_208,U_256,U_275,U_229,U_231) )
& ! [U_208,U_256,U_275,U_229,U_231] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229),s(U_256,sK9(U_275,U_256,U_231,U_229)))))
| ~ sP20(U_208,U_256,U_275,U_229,U_231) )
& ! [U_202,U_254,U_273,U_225,U_227] :
( s(U_254,sK7(U_273,U_254,U_227,U_225)) != s(U_254,app_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(U_273,U_202)))
| ~ sP19(U_202,U_254,U_273,U_225,U_227) )
& ! [U_202,U_254,U_273,U_225,U_227] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225),s(U_254,sK7(U_273,U_254,U_227,U_225)))))
| ~ sP19(U_202,U_254,U_273,U_225,U_227) )
& ! [U_190,U_237,U_243,U_262,U_281] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_281,U_262),U_243),s(tyop_2Emin_2Efun(U_262,tyop_2Emin_2Ebool),U_237))))
| sP22(U_190,U_237,U_243,U_262,U_281) )
& ! [U_189,U_236,U_242,U_261,U_280] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,U_189))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236),s(U_261,app_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(U_280,sK12(U_280,U_261,U_242,U_236)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(U_280,U_261),U_242),s(tyop_2Emin_2Efun(U_261,tyop_2Emin_2Ebool),U_236)))) )
& ! [U_186,U_235,U_241,U_260,U_279] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_279,U_260),U_241),s(tyop_2Emin_2Efun(U_260,tyop_2Emin_2Ebool),U_235))))
| sP21(U_186,U_235,U_241,U_260,U_279) )
& ! [U_185,U_234,U_240,U_259,U_278] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,U_185))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234),s(U_259,app_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(U_278,sK10(U_278,U_259,U_240,U_234)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(U_278,U_259),U_240),s(tyop_2Emin_2Efun(U_259,tyop_2Emin_2Ebool),U_234)))) )
& ! [U_208,U_256,U_275,U_229,U_231] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_275,U_256),U_231),s(tyop_2Emin_2Efun(U_256,tyop_2Emin_2Ebool),U_229))))
| sP20(U_208,U_256,U_275,U_229,U_231) )
& ! [U_230,U_207,U_274,U_228,U_255] :
( s(U_255,U_207) = s(U_255,app_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(U_274,sK8(U_274,U_255,U_230,U_228,U_207))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228),s(U_255,U_207))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(U_274,U_255),U_230),s(tyop_2Emin_2Efun(U_255,tyop_2Emin_2Ebool),U_228)))) )
& ! [U_202,U_254,U_273,U_225,U_227] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_273,U_254),U_227),s(tyop_2Emin_2Efun(U_254,tyop_2Emin_2Ebool),U_225))))
| sP19(U_202,U_254,U_273,U_225,U_227) )
& ! [U_201,U_272,U_226,U_253,U_224] :
( s(U_253,U_201) = s(U_253,app_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(U_272,sK6(U_272,U_253,U_226,U_224,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224),s(U_253,U_201))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(U_272,U_253),U_226),s(tyop_2Emin_2Efun(U_253,tyop_2Emin_2Ebool),U_224)))) )
& ! [U_223,U_221,U_271,U_252] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) )
& ! [U_251,U_222,U_196,U_270,U_220] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) )
& ! [U_217,U_219,U_250,U_269] :
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_250,tyop_2Emin_2Ebool),U_217),s(U_250,app_2E2(s(tyop_2Emin_2Efun(U_269,U_250),U_219),s(U_269,sK4(U_269,U_250,U_219,U_217))))))) )
& ! [U_192,U_216,U_218,U_249,U_268] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216),s(U_249,app_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(U_268,U_192))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(U_268,U_249),U_218),s(tyop_2Emin_2Efun(U_249,tyop_2Emin_2Ebool),U_216)))) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP19,sP20,sP21,sP22])],[f_37_13]) ).
cnf(f_37_17,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220),s(U_251,app_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(U_270,U_196))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_270,U_251),U_222),s(tyop_2Emin_2Efun(U_251,tyop_2Emin_2Ebool),U_220)))) ),
inference(clausify,[status(thm)],[f_37_14]) ).
cnf(f_37_18,plain,
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_252,tyop_2Emin_2Ebool),U_221),s(U_252,app_2E2(s(tyop_2Emin_2Efun(U_271,U_252),U_223),s(U_271,sK5(U_271,U_252,U_223,U_221))))))) ),
inference(clausify,[status(thm)],[f_37_14]) ).
fof(f_49_1,negated_conjecture,
~ ! [A_27a,A_27b,V0i_2E0,V1P_2E0,V2Q_2E0] :
( ! [V3x_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0),s(A_27a,V3x_2E0))))
=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V3x_2E0)))) )
=> ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0))))
=> p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0)))) ) ),
inference(negate,[status(cth)],[thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
fof(f_49_2,negated_conjecture,
? [A_27a,A_27b,V0i_2E0,V1P_2E0,V2Q_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0))))
& ! [V3x_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V3x_2E0))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0),s(A_27a,V3x_2E0)))) ) ),
inference(fof_nnf,[status(thm)],[f_49_1]) ).
fof(f_49_3,negated_conjecture,
? [U_341,U_340,U_339,U_338,U_337] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_340,U_341),U_339),s(tyop_2Emin_2Efun(U_341,tyop_2Emin_2Ebool),U_337))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_340,U_341),U_339),s(tyop_2Emin_2Efun(U_341,tyop_2Emin_2Ebool),U_338))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_341,tyop_2Emin_2Ebool),U_338),s(U_341,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U_341,tyop_2Emin_2Ebool),U_337),s(U_341,U_336)))) ) ),
inference(variable_rename,[status(thm)],[f_49_2]) ).
fof(f_49_4,negated_conjecture,
? [U_340,U_339,U_338,U_337] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_340,sK14),U_339),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(U_340,sK14),U_339),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337),s(sK14,U_336)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_341,sK14)],[f_49_3]) ).
fof(f_49_5,negated_conjecture,
? [U_339,U_338,U_337] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),U_339),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),U_339),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337),s(sK14,U_336)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_340,sK15)],[f_49_4]) ).
fof(f_49_6,negated_conjecture,
? [U_338,U_337] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_338),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337),s(sK14,U_336)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_339,sK16)],[f_49_5]) ).
fof(f_49_7,negated_conjecture,
? [U_337] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),U_337),s(sK14,U_336)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_338,sK17)],[f_49_6]) ).
fof(f_49_8,negated_conjecture,
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18),s(sK14,U_336)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_337,sK18)],[f_49_7]) ).
fof(f_49_9,negated_conjecture,
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17))))
& ! [U_336] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18),s(sK14,U_336)))) ) ),
inference(definitional_conversion,[status(esa)],[f_49_8]) ).
cnf(f_49_10,negated_conjecture,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,U_336))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18),s(sK14,U_336)))) ),
inference(clausify,[status(thm)],[f_49_9]) ).
cnf(f_49_11,negated_conjecture,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17)))),
inference(clausify,[status(thm)],[f_49_9]) ).
cnf(f_49_12,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18)))),
inference(clausify,[status(thm)],[f_49_9]) ).
cnf(t1,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,app_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(sK15,sK5(sK15,sK14,sK16,sK18)))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18),s(sK14,app_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(sK15,sK5(sK15,sK14,sK16,sK18))))))) ),
inference(start,[status(thm),parent(0:0)],[f_49_10]) ).
cnf(t2,plain,
( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18),s(sK14,app_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(sK15,sK5(sK15,sK14,sK16,sK18))))))) ),
inference(extension,[status(thm),parent(t1:1)],[f_37_18]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK18)))),
inference(extension,[status(thm),parent(t2:2)],[f_49_12]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17),s(sK14,app_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(sK15,sK5(sK15,sK14,sK16,sK18))))))) ),
inference(extension,[status(thm),parent(t1:2)],[f_37_17]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t1:2]) ).
cnf(t8,plain,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK15,sK14),sK16),s(tyop_2Emin_2Efun(sK14,tyop_2Emin_2Ebool),sK17)))),
inference(extension,[status(thm),parent(t6:2)],[f_49_11]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 19 11:21:55 UTC 2026
% 0.08/0.37 % CPUTime :
% 31.05/31.38 % SZS status Theorem for theBenchmark
% 31.05/31.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------