%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:44:04 PM UTC 2026
% Result : Theorem 61.62s 8.28s
% Output : Proof 61.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 112 ( 71 unt; 0 def)
% Number of atoms : 455 ( 101 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 533 ( 190 ~; 164 |; 141 &)
% ( 23 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 11 con; 0-7 aty)
% Number of variables : 216 ( 35 sgn 106 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f48,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('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
fof(f48_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(negated_conjecture,[status(cth)],[f48]) ).
fof(f48_nnf,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(nnf_transformation,[status(thm)],[f48_neg]) ).
fof(f48_sk,plain,
! [V3x_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17))))
& p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16))))
& ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,V3x_2E0))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,V3x_2E0)))) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14,sk15,sk16,sk17])],[f48_nnf]) ).
cnf(c438,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,X5))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,X5)))) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(t106,plain,
ifeq(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,X1)))),true,p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c438]) ).
cnf(t6694,plain,
ifeq(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,X1)))),true,p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,X1)))),true) = true,
inference(orient,[status(thm)],[t106]) ).
fof(f36,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('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES) ).
fof(f36_nnf,plain,
! [A_27a,A_27b,V0i_2E0,V1P_2E0] :
( ! [V16i_2E0,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)))) )
| 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)))) )
| ~ 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,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)))) )
& ( ! [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] :
( ( ? [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))))))
| ~ 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)))) )
& ( ! [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)))) ) )
& ( ? [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)))) )
& ( ! [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)))) )
& ( ? [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)))) )
& ( ! [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(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A_27a,A_27b,V0i_2E0,V1P_2E0,V2v_2E0,V3fv_2E0,V4v_2E0,V5fv_2E0,V6i_2E0,V7P_2E0,V8fv_2E0,V9i_2E0,V10P_2E0,V11fv_2E0,V12i_2E0,V13P_2E0,V14v_2E0,V15fv_2E0,V16i_2E0,V17P_2E0,V18v_2E0,V19fv_2E0] :
( ( ( s(A_27b,sk12(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,V17P_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,sk12(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)))) )
& ( s(A_27b,V18v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,sk11(A_27a,A_27b,V0i_2E0,V1P_2E0,V16i_2E0,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))))
| ~ 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)))) )
& ( ( s(A_27b,sk10(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,V13P_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,sk10(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)))) )
& ( s(A_27b,V14v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,sk9(A_27a,A_27b,V0i_2E0,V1P_2E0,V12i_2E0,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))))
| ~ 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),V10P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(A_27a,sk8(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)))) )
& ( ~ 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)))) )
& ( ~ 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(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)))) )
& ( 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,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,sk6(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,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,sk5(A_27a,A_27b,V0i_2E0,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,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,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,sk4(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,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,sk3(A_27a,A_27b,V0i_2E0,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,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(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12])],[f36_nnf]) ).
cnf(c105,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,sk8(X0,X1,X2,X3,X11,X12)))))))
| p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t217,plain,
or(p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4)))),p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,sk8(X1,X2,X5,X6,X3,X4)))))))) = true,
inference(equality_encoding,[status(esa)],[c105]) ).
cnf(t3173,plain,
or(p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4)))),p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,sk8(X1,X2,X5,X6,X3,X4)))))))) = true,
inference(orient,[status(thm)],[t217]) ).
cnf(t12,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t259,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t12]) ).
fof(f33,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('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
fof(f33_nnf,plain,
! [V0t_2E0] :
( ( p(s(tyop_2Emin_2Ebool,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,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,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,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))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,V0t_2E0) ) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [V0t_2E0] :
( ( p(s(tyop_2Emin_2Ebool,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,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,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,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))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,V0t_2E0) ) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c79,plain,
( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t30,plain,
or(eq(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,X1)),p(s(tyop_2Emin_2Ebool,X1))) = true,
inference(equality_encoding,[status(esa)],[c79]) ).
cnf(t3549,plain,
or(eq(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,X1)),p(s(tyop_2Emin_2Ebool,X1))) = true,
inference(orient,[status(thm)],[t30]) ).
cnf(c440,plain,
~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(t39,plain,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))) = false,
inference(equality_encoding,[status(esa)],[c440]) ).
cnf(t7473,plain,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))) = false,
inference(orient,[status(thm)],[t39]) ).
cnf(t7478,plain,
true = or(eq(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))),false),
inference(cp,[status(thm)],[t3549,t7473]) ).
cnf(t3,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t256,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t25746,plain,
true = eq(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))),
inference(step,[status(thm)],[t7478,t256]) ).
cnf(t10694,plain,
eq(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))) = true,
inference(orient,[status(thm)],[t25746]) ).
cnf(t10695,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17))) = ifeq(true,true,s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17)))),
inference(cp,[status(thm)],[t259,t10694]) ).
cnf(t10,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t25747,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),
inference(step,[status(thm)],[t10695,t258]) ).
cnf(t10696,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),
inference(orient,[status(thm)],[t25747]) ).
cnf(t10802,plain,
true = or(p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17)))))))),
inference(cp,[status(thm)],[t3173,t10696]) ).
fof(f3,axiom,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Enotfalse) ).
fof(f3_nnf,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c6,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t7,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) = false,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t7328,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t26006,plain,
true = or(false,p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17)))))))),
inference(step,[status(thm)],[t10802,t7328]) ).
cnf(t5,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t257,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t26007,plain,
true = p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17))))))),
inference(step,[status(thm)],[t26006,t257]) ).
cnf(t25459,plain,
p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk17),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17))))))) = true,
inference(orient,[status(thm)],[t26007]) ).
cnf(t25531,plain,
true = ifeq(true,true,p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17))))))),true),
inference(cp,[status(thm)],[t6694,t25459]) ).
cnf(t26008,plain,
true = p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,sk8(sk14,sk13,X1,X2,sk15,sk17))))))),
inference(step,[status(thm)],[t25531,t258]) ).
cnf(t11,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t7624,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t11]) ).
cnf(c104,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12),s(X1,app_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(X0,X13))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X0,X1),X11),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X12)))) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t207,plain,
or(not(p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4))))),not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,X5)))))))) = true,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(t3608,plain,
or(not(p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4))))),not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,X5)))))))) = true,
inference(orient,[status(thm)],[t207]) ).
fof(f9,axiom,
! [V0_2E0,V1_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0))))
<=> ( p(s(tyop_2Emin_2Ebool,V1_2E0))
| p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_5C_2F) ).
fof(f9_nnf,plain,
! [V0_2E0,V1_2E0] :
( ( ( ~ p(s(tyop_2Emin_2Ebool,V1_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) )
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) )
& ( p(s(tyop_2Emin_2Ebool,V1_2E0))
| p(s(tyop_2Emin_2Ebool,V0_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V0_2E0,V1_2E0] :
( ( ( ~ p(s(tyop_2Emin_2Ebool,V1_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) )
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) )
& ( p(s(tyop_2Emin_2Ebool,V1_2E0))
| p(s(tyop_2Emin_2Ebool,V0_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) ) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c15,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X0),s(tyop_2Emin_2Ebool,X1)))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi12,axiom,
ifeq(p(s(tyop_2Emin_2Ebool,X0)),true,p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X0),s(tyop_2Emin_2Ebool,X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
fof(f2,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Etruth) ).
fof(f2_nnf,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c5,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(hi3,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h10,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),s(tyop_2Emin_2Ebool,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi3]) ).
fof(f42,axiom,
! [V0r_2E0,V1q_2E0,V2p_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V2p_2E0))
<=> s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0) )
<=> ( ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V0r_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Esat_2Edc__eq) ).
fof(f42_nnf,plain,
! [V0r_2E0,V1q_2E0,V2p_2E0] :
( ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0))
& p(s(tyop_2Emin_2Ebool,V1q_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) )
| ( p(s(tyop_2Emin_2Ebool,V2p_2E0))
& p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) )
| ( p(s(tyop_2Emin_2Ebool,V1q_2E0))
& p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( ( s(tyop_2Emin_2Ebool,V1q_2E0) != s(tyop_2Emin_2Ebool,V0r_2E0)
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
& ( s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0)
| ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) )
& ( ( ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V0r_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) )
| ( s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0)
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( s(tyop_2Emin_2Ebool,V1q_2E0) != s(tyop_2Emin_2Ebool,V0r_2E0)
& p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [V2p_2E0,V1q_2E0,V0r_2E0] :
( ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0))
& p(s(tyop_2Emin_2Ebool,V1q_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) )
| ( p(s(tyop_2Emin_2Ebool,V2p_2E0))
& p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) )
| ( p(s(tyop_2Emin_2Ebool,V1q_2E0))
& p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( ( s(tyop_2Emin_2Ebool,V1q_2E0) != s(tyop_2Emin_2Ebool,V0r_2E0)
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
& ( s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0)
| ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) )
& ( ( ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V0r_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V2p_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0r_2E0))
| p(s(tyop_2Emin_2Ebool,V1q_2E0))
| p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) )
| ( s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0)
& ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) )
| ( s(tyop_2Emin_2Ebool,V1q_2E0) != s(tyop_2Emin_2Ebool,V0r_2E0)
& p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c204,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X0)
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(hi93,axiom,
ifeq(p(s(tyop_2Emin_2Ebool,X0)),true,ifeq(p(s(tyop_2Emin_2Ebool,X1)),true,ifeq(p(s(tyop_2Emin_2Ebool,X0)),true,ifeq(p(s(tyop_2Emin_2Ebool,X2)),true,ifeq(p(s(tyop_2Emin_2Ebool,X1)),true,s(tyop_2Emin_2Ebool,X2),s(tyop_2Emin_2Ebool,X1)),s(tyop_2Emin_2Ebool,X1)),s(tyop_2Emin_2Ebool,X1)),s(tyop_2Emin_2Ebool,X1)),s(tyop_2Emin_2Ebool,X1)) = s(tyop_2Emin_2Ebool,X1),
inference(equality_encoding,[status(esa)],[c204]) ).
cnf(c439,plain,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16)))),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(hi101,negated_conjecture,
p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16)))) = true,
inference(equality_encoding,[status(esa)],[c439]) ).
fof(f29,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).
fof(f29_nnf,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c50,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(hi45,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) = true,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t47,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),
inference(hyper_resolution,[status(thm)],[hi93,h10,hi101,h10,hi45,hi101]) ).
cnf(t1365,plain,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),
inference(orient,[status(thm)],[t47]) ).
cnf(t3609,plain,
true = or(not(p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))),not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))))),
inference(cp,[status(thm)],[t3608,t1365]) ).
cnf(t8,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t2339,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t25870,plain,
true = or(not(true),not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))))),
inference(step,[status(thm)],[t3609,t2339]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t7625,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t25871,plain,
true = or(false,not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))))),
inference(step,[status(thm)],[t25870,t7625]) ).
cnf(t25872,plain,
true = not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1))))))),
inference(step,[status(thm)],[t25871,t257]) ).
cnf(t17415,plain,
not(p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1))))))) = true,
inference(orient,[status(thm)],[t25872]) ).
cnf(t17417,plain,
false = ifeq(true,true,p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))),false),
inference(cp,[status(thm)],[t7624,t17415]) ).
cnf(t25873,plain,
false = p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))),
inference(step,[status(thm)],[t17417,t258]) ).
cnf(t17418,plain,
p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sk13,tyop_2Emin_2Ebool),sk16),s(sk13,app_2E2(s(tyop_2Emin_2Efun(sk14,sk13),sk15),s(sk14,X1)))))) = false,
inference(orient,[status(thm)],[t25873]) ).
cnf(t26009,plain,
true = false,
inference(step,[status(thm)],[t26008,t17418]) ).
cnf(t25613,plain,
false = true,
inference(orient,[status(thm)],[t26009]) ).
fof(f10,axiom,
! [V0_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0))))
<=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_7E) ).
fof(f10_nnf,plain,
! [V0_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V0_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V0_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V0_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c17,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X0)))) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f17,axiom,
! [X0_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,X0_2E0))
<=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_7E_2E1) ).
fof(f17_nnf,plain,
! [X0_2E0] :
( ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))))
| ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))))
| p(s(tyop_2Emin_2Ebool,X0_2E0)) ) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X0_2E0] :
( ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))))
| ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))))
| p(s(tyop_2Emin_2Ebool,X0_2E0)) ) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c35,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0))))
| ~ p(s(tyop_2Emin_2Ebool,X0)) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f30,axiom,
! [V0t_2E0] :
( ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
<=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
<=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__CLAUSES) ).
fof(f30_nnf,plain,
! [V0t_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [V0t_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
& p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c64,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f31,axiom,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ! [V0t_2E0] :
( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
<=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__CLAUSES) ).
fof(f31_nnf,plain,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ! [V0t_2E0] :
( ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [V0t_2E0] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c69,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(c71,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(c78,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(c80,plain,
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c6,c17,c35,c64,c69,c71,c78,c80,c104,c440]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t25613]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 17:30:03 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 61.62/8.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.62/8.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------