%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 : Thu Sep 24 12:51:48 PM UTC 2026
% Result : Theorem 19.74s 2.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 21:44:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 19.74/2.95 % Refutation found
% 19.74/2.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.74/2.95 % SZS output start CNFRefutation for theBenchmark
% 19.74/2.95 fof(f2,axiom,(
% 19.74/2.95 (! [V0_2E0,V1_2E0] :( ( p(s(tyop_2Emin_2Ebool,V0_2E0))<=> p(s(tyop_2Emin_2Ebool,V1_2E0)) )=> s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) )),
% 19.74/2.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.74/2.95 fof(f4,axiom,(
% 19.74/2.95 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
% 19.74/2.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.74/2.95 fof(f37,axiom,(
% 19.74/2.95 (! [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))))<=> (! [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)))))) )) ))& ( 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)))))) )) ))& (! [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)))))) )))& (! [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)))))) )))& (! [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))) )) )))& (! [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))) )) )) )) )),
% 19.74/2.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.74/2.95 fof(f49,conjecture,(
% 19.74/2.95 (! [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)))) ) ) )),
% 19.74/2.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.74/2.95 fof(f50,negated_conjecture,(
% 19.74/2.95 ~((! [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)))) ) ) ))),
% 19.74/2.95 inference(negated_conjecture,[status(cth)],[f49])).
% 19.74/2.95 fof(f54,plain,(
% 19.74/2.95 ![V0_2E0,V1_2E0]: ((p(s(tyop_2Emin_2Ebool,V0_2E0))<~>p(s(tyop_2Emin_2Ebool,V1_2E0)))|s(tyop_2Emin_2Ebool,V0_2E0)=s(tyop_2Emin_2Ebool,V1_2E0))),
% 19.74/2.95 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 19.74/2.95 fof(f55,plain,(
% 19.74/2.95 ![V0_2E0,V1_2E0]: (((p(s(tyop_2Emin_2Ebool,V0_2E0))|p(s(tyop_2Emin_2Ebool,V1_2E0)))&(~p(s(tyop_2Emin_2Ebool,V0_2E0))|~p(s(tyop_2Emin_2Ebool,V1_2E0))))|s(tyop_2Emin_2Ebool,V0_2E0)=s(tyop_2Emin_2Ebool,V1_2E0))),
% 19.74/2.95 inference(NNF_transformation,[status(thm)],[f54])).
% 19.74/2.95 fof(f56,plain,(
% 19.74/2.95 ![X0,X1]: (p(s(tyop_2Emin_2Ebool,X0))|p(s(tyop_2Emin_2Ebool,X1))|s(tyop_2Emin_2Ebool,X0)=s(tyop_2Emin_2Ebool,X1))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f55])).
% 19.74/2.95 fof(f59,plain,(
% 19.74/2.95 ~p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f4])).
% 19.74/2.95 fof(f189,plain,(
% 19.74/2.95 ![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))))<=>(![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))))))))))&(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)))))))))))&(![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))))))))))&(![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))))))))))&(![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)))))))))&(![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)))))))))),
% 19.74/2.95 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 19.74/2.95 fof(f190,plain,(
% 19.74/2.95 ![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))))|(![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))))))))))&(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)))))))))))&((~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__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))))))))))))&(![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__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)))))))))))&(![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))))))))&(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)))))))))))&(![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)))))))&(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))))))))))&(![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)))))))&(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))))))))))),
% 19.74/2.95 inference(NNF_transformation,[status(thm)],[f189])).
% 19.74/2.95 fof(f191,plain,(
% 19.74/2.95 ((((((![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))))|((![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))))))))))&(![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))))|((?[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)))))))))))&((![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))))|((![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))))))))))&(![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))))|((?[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))))))))))))&((![A_27a,A_27b,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)))))))))&(![A_27a,A_27b,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)))))))))))&((![A_27a,A_27b,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)))))))))&(![A_27a,A_27b,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)))))))))))&((![A_27a,A_27b,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))))))))&(![A_27a,A_27b,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))))))))))&((![A_27a,A_27b,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))))))))&(![A_27a,A_27b,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)))))))))),
% 19.74/2.95 inference(miniscoping,[status(thm)],[f190])).
% 19.74/2.95 fof(f192,plain,(
% 19.74/2.95 ((((((![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))))|((![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)))))|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,sK3_skl(V1P_2E0,V0i_2E0,A_27b,A_27a))))))))))&(![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))))|(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,sK4_skl(V1P_2E0,V0i_2E0,A_27b,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,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V3fv_2E0)))))))))))&((![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))))|((![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)))))|~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,sK5_skl(V1P_2E0,V0i_2E0,A_27b,A_27a))))))))))&(![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))))|(~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,sK6_skl(V1P_2E0,V0i_2E0,A_27b,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,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V5fv_2E0))))))))))))&((![A_27a,A_27b,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)))))))))&(![A_27a,A_27b,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))))|~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,sK7_skl(V7P_2E0,V6i_2E0,A_27b,A_27a)))))))))))&((![A_27a,A_27b,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)))))))))&(![A_27a,A_27b,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))))|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,sK8_skl(V10P_2E0,V9i_2E0,A_27b,A_27a)))))))))))&((![A_27a,A_27b,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))))|s(A_27b,V14v_2E0)=s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,sK9_skl(V14v_2E0,V13P_2E0,V12i_2E0,A_27b,A_27a))))))))&(![A_27a,A_27b,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))))|(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,sK10_skl(V13P_2E0,V12i_2E0,A_27b,A_27a)))))&(![V15fv_2E0]: ~s(A_27b,sK10_skl(V13P_2E0,V12i_2E0,A_27b,A_27a))=s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0)))))))))&((![A_27a,A_27b,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))))|s(A_27b,V18v_2E0)=s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,sK11_skl(V18v_2E0,V17P_2E0,V16i_2E0,A_27b,A_27a))))))))&(![A_27a,A_27b,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))))|(~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,sK12_skl(V17P_2E0,V16i_2E0,A_27b,A_27a)))))&(![V19fv_2E0]: ~s(A_27b,sK12_skl(V17P_2E0,V16i_2E0,A_27b,A_27a))=s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0))))))))),
% 19.74/2.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(V3fv_2E0,sK3_skl(V1P_2E0,V0i_2E0,A_27b,A_27a)),skolemize(V2v_2E0,sK4_skl(V1P_2E0,V0i_2E0,A_27b,A_27a)),skolemize(V5fv_2E0,sK5_skl(V1P_2E0,V0i_2E0,A_27b,A_27a)),skolemize(V4v_2E0,sK6_skl(V1P_2E0,V0i_2E0,A_27b,A_27a)),skolemize(V8fv_2E0,sK7_skl(V7P_2E0,V6i_2E0,A_27b,A_27a)),skolemize(V11fv_2E0,sK8_skl(V10P_2E0,V9i_2E0,A_27b,A_27a)),skolemize(V15fv_2E0,sK9_skl(V14v_2E0,V13P_2E0,V12i_2E0,A_27b,A_27a)),skolemize(V14v_2E0,sK10_skl(V13P_2E0,V12i_2E0,A_27b,A_27a)),skolemize(V19fv_2E0,sK11_skl(V18v_2E0,V17P_2E0,V16i_2E0,A_27b,A_27a)),skolemize(V18v_2E0,sK12_skl(V17P_2E0,V16i_2E0,A_27b,A_27a))],[f191])).
% 19.74/2.95 fof(f201,plain,(
% 19.74/2.95 ![X0,X1,X2,X3,X4]: (~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))|~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X4)))))))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f192])).
% 19.74/2.95 fof(f202,plain,(
% 19.74/2.95 ![X0,X1,X2,X3]: (p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))|p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,sK8_skl(X3,X2,X1,X0))))))))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f192])).
% 19.74/2.95 fof(f288,plain,(
% 19.74/2.95 (?[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)))))))),
% 19.74/2.95 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 19.74/2.95 fof(f289,plain,(
% 19.74/2.95 ?[A_27a,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))))))&(?[A_27b,V0i_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)))))))),
% 19.74/2.95 inference(miniscoping,[status(thm)],[f288])).
% 19.74/2.95 fof(f290,plain,(
% 19.74/2.95 ((![V3x_2E0]: (~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,V3x_2E0))))|p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,V3x_2E0))))))&(p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl))))&~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl))))))),
% 19.74/2.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(A_27a,sK13_skl),skolemize(V1P_2E0,sK14_skl),skolemize(V2Q_2E0,sK15_skl),skolemize(A_27b,sK16_skl),skolemize(V0i_2E0,sK17_skl)],[f289])).
% 19.74/2.95 fof(f291,plain,(
% 19.74/2.95 ![X0]: (~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,X0))))|p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,X0)))))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f290])).
% 19.74/2.95 fof(f292,plain,(
% 19.74/2.95 p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl))))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f290])).
% 19.74/2.95 fof(f293,plain,(
% 19.74/2.95 ~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl))))),
% 19.74/2.95 inference(cnf_transformation,[status(thm)],[f290])).
% 19.74/2.95 fof(f387,definition,(
% 19.74/2.95 ![X0]: (sQ1_spl <=> (p(s(tyop_2Emin_2Ebool,X0))))),
% 19.74/2.95 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 19.74/2.95 fof(f388,plain,(
% 19.74/2.95 ![X0]: (p(s(tyop_2Emin_2Ebool,X0))|~sQ1_spl)),
% 19.74/2.95 inference(component_clause,[status(thm)],[f387])).
% 19.74/2.95 fof(f401,definition,(
% 19.74/2.95 sQ4_spl <=> (p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)))),
% 19.74/2.95 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 19.74/2.95 fof(f402,plain,(
% 19.74/2.95 p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))|~sQ4_spl),
% 19.74/2.95 inference(component_clause,[status(thm)],[f401])).
% 19.74/2.95 fof(f468,plain,(
% 19.74/2.95 ![X0]: (p(s(tyop_2Emin_2Ebool,X0))|s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)))=s(tyop_2Emin_2Ebool,X0))),
% 19.74/2.95 inference(resolution,[status(thm)],[f56,f293])).
% 19.74/2.95 fof(f470,plain,(
% 19.74/2.95 ![X0,X1]: (p(s(tyop_2Emin_2Ebool,X0))|s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,X1)))=s(tyop_2Emin_2Ebool,X0)|p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,X1)))))),
% 19.74/2.95 inference(resolution,[status(thm)],[f56,f291])).
% 19.74/2.95 fof(f481,plain,(
% 19.74/2.95 ![X0,X1,X2,X3,X4]: (~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))|s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)))=s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X2),s(X0,X4))))))),
% 19.74/2.95 inference(resolution,[status(thm)],[f201,f468])).
% 19.74/2.95 fof(f488,plain,(
% 19.74/2.95 ![X0,X1,X2]: (s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(X0,sK13_skl),X1),s(X0,X2)))))=s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(X0,sK13_skl),X1),s(X0,X2)))))|~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,sK13_skl),X1),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl)))))),
% 19.74/2.95 inference(resolution,[status(thm)],[f470,f201])).
% 19.74/2.95 fof(f535,plain,(
% 19.74/2.95 s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)))=s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
% 19.74/2.95 inference(resolution,[status(thm)],[f59,f468])).
% 19.74/2.95 fof(f540,plain,(
% 19.74/2.95 ![X0]: (s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)))=s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(sK16_skl,X0))))))),
% 19.74/2.95 inference(resolution,[status(thm)],[f481,f292])).
% 19.74/2.95 fof(f562,plain,(
% 19.74/2.95 ![X0]: (s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(sK16_skl,X0)))))=s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(sK16_skl,X0))))))),
% 19.74/2.95 inference(resolution,[status(thm)],[f488,f292])).
% 19.74/2.95 fof(f926,plain,(
% 19.74/2.95 $false|~sQ4_spl),
% 19.74/2.95 inference(forward_subsumption_resolution,[status(thm)],[f402,f59])).
% 19.74/2.95 fof(f927,plain,(
% 19.74/2.95 ~sQ4_spl),
% 19.74/2.95 inference(contradiction_clause,[status(thm)],[f926])).
% 19.74/2.95 fof(f1605,definition,(
% 19.74/2.95 sQ87_spl <=> (p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)))))),
% 19.74/2.95 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 19.74/2.95 fof(f1606,plain,(
% 19.74/2.95 p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl))))|~sQ87_spl),
% 19.74/2.95 inference(component_clause,[status(thm)],[f1605])).
% 19.74/2.98 fof(f1804,plain,(
% 19.74/2.98 $false|~sQ87_spl),
% 19.74/2.98 inference(forward_subsumption_resolution,[status(thm)],[f1606,f293])).
% 19.74/2.98 fof(f1805,plain,(
% 19.74/2.98 ~sQ87_spl),
% 19.74/2.98 inference(contradiction_clause,[status(thm)],[f1804])).
% 19.74/2.98 fof(f1897,definition,(
% 19.74/2.98 sQ135_spl <=> (s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)=s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl))),
% 19.74/2.98 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 19.74/2.98 fof(f1898,plain,(
% 19.74/2.98 s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl)=s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl)|~sQ135_spl),
% 19.74/2.98 inference(component_clause,[status(thm)],[f1897])).
% 19.74/2.98 fof(f1917,definition,(
% 19.74/2.98 sQ139_spl <=> (p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl)))))),
% 19.74/2.98 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 19.74/2.98 fof(f1919,plain,(
% 19.74/2.98 ~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl))))|sQ139_spl),
% 19.74/2.98 inference(component_clause,[status(thm)],[f1917])).
% 19.74/2.98 fof(f2149,plain,(
% 19.74/2.98 ~p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl))))|~sQ135_spl),
% 19.74/2.98 inference(backward_demodulation,[status(thm)],[f1898,f293])).
% 19.74/2.98 fof(f2172,plain,(
% 19.74/2.98 $false|~sQ135_spl),
% 19.74/2.98 inference(forward_subsumption_resolution,[status(thm)],[f2149,f292])).
% 19.74/2.98 fof(f2173,plain,(
% 19.74/2.98 ~sQ135_spl),
% 19.74/2.98 inference(contradiction_clause,[status(thm)],[f2172])).
% 19.74/2.98 fof(f2329,plain,(
% 19.74/2.98 $false|sQ139_spl),
% 19.74/2.98 inference(forward_subsumption_resolution,[status(thm)],[f1919,f292])).
% 19.74/2.98 fof(f2330,plain,(
% 19.74/2.98 sQ139_spl),
% 19.74/2.98 inference(contradiction_clause,[status(thm)],[f2329])).
% 19.74/2.98 fof(f5951,plain,(
% 19.74/2.98 ![X0,X1,X2,X3,X4]: (~p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X1),s(X0,app_2E2(s(tyop_2Emin_2Efun(X2,X0),X3),s(X2,X4))))))|~sQ1_spl)),
% 19.74/2.98 inference(backward_subsumption_resolution,[status(thm)],[f201,f388])).
% 19.74/2.98 fof(f5967,plain,(
% 19.74/2.98 $false|~sQ1_spl),
% 19.74/2.98 inference(forward_subsumption_resolution,[status(thm)],[f5951,f388])).
% 19.74/2.98 fof(f5968,plain,(
% 19.74/2.98 ~sQ1_spl),
% 19.74/2.98 inference(contradiction_clause,[status(thm)],[f5967])).
% 19.74/2.98 fof(f6578,plain,(
% 19.74/2.98 ![X0]: (s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)=s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK14_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(sK16_skl,X0))))))),
% 19.74/2.98 inference(forward_demodulation,[status(thm)],[f535,f540])).
% 19.74/2.98 fof(f9067,plain,(
% 19.74/2.98 ![X0]: (s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl),s(sK13_skl,app_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(sK16_skl,X0)))))=s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 19.74/2.98 inference(forward_demodulation,[status(thm)],[f6578,f562])).
% 19.74/2.98 fof(f10223,plain,(
% 19.74/2.98 p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sK16_skl,sK13_skl),sK17_skl),s(tyop_2Emin_2Efun(sK13_skl,tyop_2Emin_2Ebool),sK15_skl))))|p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 19.74/2.98 inference(paramodulation,[status(thm)],[f9067,f202])).
% 19.74/2.98 fof(f10247,plain,(
% 19.74/2.98 sQ87_spl|sQ4_spl),
% 19.74/2.98 inference(split_clause,[status(thm)],[f10223,f1605,f401])).
% 19.74/2.98 fof(f10257,plain,(
% 19.74/2.98 $false),
% 19.74/2.98 inference(sat_refutation,[status(thm)],[f927,f1805,f2173,f2330,f5968,f10247])).
% 19.74/2.98 % SZS output end CNFRefutation for theBenchmark.p
% 1.48/3.01 % Elapsed time: 2.632858 seconds
% 1.48/3.01 % CPU time: 20.519060 seconds
% 1.48/3.01 % Total memory used: 384.679 MB
% 1.48/3.01 % Net memory used: 368.171 MB
%------------------------------------------------------------------------------