%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 07:41:19 AM UTC 2026
% Result : Theorem 2.29s 0.80s
% Output : CNFRefutation 2.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 31 ( 15 unt; 0 def)
% Number of atoms : 169 ( 24 equ)
% Maximal formula atoms : 36 ( 5 avg)
% Number of connectives : 208 ( 70 ~; 61 |; 57 &)
% ( 10 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 9 con; 0-7 aty)
% Number of variables : 221 ( 8 sgn 171 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))),
file('theBenchmark.p',arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2_2Emono_2EA_27a_20mono_2EA_27b) ).
fof(thm_2Ebool_2EEQ__CLAUSES,axiom,
! [V0t_2E0] :
( ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
<=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0)
<=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
<=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0)
<=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
file('theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
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(thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg,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(assume_negation,[status(cth)],[thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
fof(reserved_2Eho_2Enotfalse,axiom,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
file('theBenchmark.p',reserved_2Eho_2Enotfalse) ).
cnf(c_51,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(clausify,[status(thm)],[reserved_2Eho_2Enotfalse]) ).
cnf(c_94,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A,B),C),s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A,B),tyop_2Emin_2Efun(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(A,B),C))),s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D))),
inference(clausify,[status(thm)],[arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2_2Emono_2EA_27a_20mono_2EA_27b]) ).
cnf(c_105,plain,
( p(s(tyop_2Emin_2Ebool,A))
| s(tyop_2Emin_2Ebool,A) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(clausify,[status(thm)],[thm_2Ebool_2EEQ__CLAUSES]) ).
cnf(c_106,plain,
( p(s(tyop_2Emin_2Ebool,A))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,A) ),
inference(copy,[status(thm)],[c_105]) ).
fof(nnf_34,plain,
! [A_27a,A_27b,V0i_2E0,V1P_2E0] :
( ! [V16i_2E0,V17P_2E0] :
( ( ? [V18v_2E0] :
( ! [V19fv_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0))) != s(A_27b,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)))) )
| 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)))) )
& ( ! [X8] :
( ? [X9] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,X9))) = s(A_27b,X8)
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,X8)))) )
| ~ 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] :
( ( ? [V14v_2E0] :
( ! [V15fv_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0))) != s(A_27b,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)))) )
| 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)))) )
& ( ! [X6] :
( ? [X7] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,X7))) = s(A_27b,X6)
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,X6)))) )
| ~ 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] :
( ( ? [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)))) )
& ( ! [X5] : ~ 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,X5))))))
| ~ 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] :
( ( ? [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)))) )
& ( ! [X4] : 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,X4))))))
| ~ 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)))) ) )
& ( ? [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)))) )
& ( ! [X2] :
( ? [X3] : ~ 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,X3))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,X2)))) )
| ~ 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)))) )
& ( ? [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)))) )
& ( ! [X0] :
( ? [X1] : 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,X1))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,X0)))) )
| ~ 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(sk_thm_2EquantHeuristics_2EGUESS__REWRITES_sk,plain,
! [A_27a,A_27b,V0i_2E0,V1P_2E0] :
( ! [V16i_2E0,V17P_2E0] :
( ( ( ! [V19fv_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0))) != s(A_27b,sK14(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,V17P_2E0))
& ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,sK14(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)))) )
& ( ! [X8] :
( s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,sK13(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,V17P_2E0,X8)))) = s(A_27b,X8)
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,X8)))) )
| ~ 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] :
( ( ( ! [V15fv_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0))) != s(A_27b,sK12(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,V13P_2E0))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,sK12(A_27a,A_27b,V0i_2E0,V1P_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)))) )
& ( ! [X6] :
( s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,sK11(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,V13P_2E0,X6)))) = s(A_27b,X6)
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,X6)))) )
| ~ 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,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,sK0(A_27a,A_27b,V0i_2E0,V1P_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)))) )
& ( ! [X5] : ~ 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,X5))))))
| ~ 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,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,sK10(A_27a,A_27b,V0i_2E0,V1P_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)))) )
& ( ! [X4] : 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,X4))))))
| ~ 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)))) ) )
& ( ( ! [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,sK9(A_27a,A_27b,V0i_2E0,V1P_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)))) )
& ( ! [X2] :
( ~ 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,sK8(A_27a,A_27b,V0i_2E0,V1P_2E0,X2)))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,X2)))) )
| ~ 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)))) )
& ( ( ! [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,sK7(A_27a,A_27b,V0i_2E0,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)))) )
& ( ! [X0] :
( 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,sK6(A_27a,A_27b,V0i_2E0,V1P_2E0,X0)))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,X0)))) )
| ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9,sK10,sK0,sK11,sK12,sK13,sK14]),skolemize(X1,sK6(A_27a,A_27b,V0i_2E0,V1P_2E0,X0)),skolemize(V2v_2E0,sK7(A_27a,A_27b,V0i_2E0,V1P_2E0)),skolemize(X3,sK8(A_27a,A_27b,V0i_2E0,V1P_2E0,X2)),skolemize(V4v_2E0,sK9(A_27a,A_27b,V0i_2E0,V1P_2E0)),skolemize(V8fv_2E0,sK10(A_27a,A_27b,V0i_2E0,V1P_2E0,V6i_2E0,V7P_2E0)),skolemize(V11fv_2E0,sK0(A_27a,A_27b,V0i_2E0,V1P_2E0,V9i_2E0,V10P_2E0)),skolemize(X7,sK11(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,V13P_2E0,X6)),skolemize(V14v_2E0,sK12(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,V13P_2E0)),skolemize(X9,sK13(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,V17P_2E0,X8)),skolemize(V18v_2E0,sK14(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,V17P_2E0))],[nnf_34]) ).
fof(sk_thm_2EquantHeuristics_2EGUESS__REWRITES,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))) != s(VAR_1,sK14(VAR_0,VAR_1,VAR_5,VAR_6,VAR_2,VAR_3))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,sK14(VAR_0,VAR_1,VAR_4,VAR_5,VAR_2,VAR_3)))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK13(VAR_0,VAR_1,VAR_5,VAR_6,VAR_2,VAR_3,VAR_4)))) = s(VAR_1,VAR_4)
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,VAR_4))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))) != s(VAR_1,sK12(VAR_0,VAR_1,VAR_5,VAR_6,VAR_2,VAR_3))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,sK12(VAR_0,VAR_1,VAR_4,VAR_5,VAR_2,VAR_3)))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK11(VAR_0,VAR_1,VAR_5,VAR_6,VAR_2,VAR_3,VAR_4)))) = s(VAR_1,VAR_4)
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,VAR_4))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK0(VAR_0,VAR_1,VAR_4,VAR_5,VAR_2,VAR_3)))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK10(VAR_0,VAR_1,VAR_4,VAR_5,VAR_2,VAR_3)))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,sK9(VAR_0,VAR_1,VAR_2,VAR_3)))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4)))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,VAR_4))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,VAR_4))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,sK7(VAR_0,VAR_1,VAR_2,VAR_3)))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,app_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(VAR_0,sK6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4)))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3),s(VAR_1,VAR_4))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(VAR_0,VAR_1),VAR_2),s(tyop_2Emin_2Efun(VAR_1,tyop_2Emin_2Ebool),VAR_3)))) ) ),
inference(cnf_transformation,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__REWRITES_sk]) ).
cnf(c_128,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D),s(B,app_2E2(s(tyop_2Emin_2Efun(A,B),C),s(A,E))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A,B),C),s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D)))) ),
inference(split_conjunct,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
cnf(c_129,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),D),s(A,app_2E2(s(tyop_2Emin_2Efun(B,A),C),s(B,E))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(B,A),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(B,A),C))),s(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),D)))) ),
inference(paramod,[status(thm)],[c_94,c_128]) ).
cnf(c_130,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D),s(B,app_2E2(s(tyop_2Emin_2Efun(A,B),C),s(A,sK0(A,B,E,F,C,D)))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A,B),C),s(tyop_2Emin_2Efun(B,tyop_2Emin_2Ebool),D)))) ),
inference(split_conjunct,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
cnf(c_131,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),D),s(A,app_2E2(s(tyop_2Emin_2Efun(B,A),C),s(B,sK0(B,A,E,F,C,D)))))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(B,A),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(B,A),C))),s(tyop_2Emin_2Efun(A,tyop_2Emin_2Ebool),D)))) ),
inference(paramod,[status(thm)],[c_94,c_130]) ).
fof(nnf_46,plain,
? [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)],[thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg]) ).
fof(sk_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3))))
& ! [V3x_2E0] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3),s(sK1,V3x_2E0))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2),s(sK1,V3x_2E0)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5]),skolemize(A_27a,sK1),skolemize(A_27b,sK4),skolemize(V0i_2E0,sK5),skolemize(V1P_2E0,sK3),skolemize(V2Q_2E0,sK2)],[nnf_46]) ).
cnf(c_146,negated_conjecture,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3),s(sK1,A))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2),s(sK1,A)))) ),
inference(split_conjunct,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg]) ).
cnf(c_147,negated_conjecture,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3)))),
inference(split_conjunct,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg]) ).
cnf(c_148,negated_conjecture,
p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK4,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(sK4,sK1),sK5))),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3)))),
inference(paramod,[status(thm)],[c_94,c_147]) ).
cnf(c_149,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2)))),
inference(split_conjunct,[status(thm)],[sk_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_neg]) ).
cnf(c_150,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK4,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(sK4,sK1),sK5))),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2)))),
inference(paramod,[status(thm)],[c_94,c_149]) ).
cnf(c_848,plain,
~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK3),s(sK1,app_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(sK4,A)))))),
inference(resolve,[status(thm)],[c_148,c_129]) ).
cnf(c_1147,negated_conjecture,
s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK4,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(sK4,sK1),sK5))),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2))),
inference(resolve,[status(thm)],[c_150,c_106]) ).
cnf(c_851,negated_conjecture,
s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK4,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(sK4,sK1),sK5))),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_1112,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2),s(sK1,app_2E2(s(tyop_2Emin_2Efun(sK4,sK1),sK5),s(sK4,A)))))),
inference(resolve,[status(thm)],[c_146,c_848]) ).
cnf(c_1148,plain,
p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK4,sK1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(sK4,sK1),sK5))),s(tyop_2Emin_2Efun(sK1,tyop_2Emin_2Ebool),sK2)))),
inference(resolve,[status(thm)],[c_1112,c_131]) ).
cnf(c_1149,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(paramod,[status(thm)],[c_851,c_1148]) ).
cnf(c_1146,plain,
$false,
inference(resolve,[status(thm)],[c_51,c_1149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n002.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 : Fri Sep 25 17:07:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 3784119 was started by sandbox on n002,
% 0.13/0.36 % Fri Sep 25 17:07:50 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 2.29/0.80
% 2.29/0.80 % SZS status Theorem for theBenchmark
% 2.29/0.80
% 2.29/0.80 % Proof 1 at 0.32 (+ 0.07) seconds.
% 2.29/0.80 % Length of proof is 21.
% 2.29/0.80 % Level of proof is 5.
% 2.29/0.80 % Maximum clause weight is 58.000.
% 2.29/0.80 % Given clauses 117.
% 2.29/0.80
% 2.29/0.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------