%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 12:50:03 PM UTC 2026
% Result : Theorem 5.48s 1.24s
% Output : CNFRefutation 5.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 35
% Syntax : Number of formulae : 156 ( 34 unt; 25 def)
% Number of atoms : 688 ( 32 equ)
% Maximal formula atoms : 64 ( 4 avg)
% Number of connectives : 871 ( 339 ~; 340 |; 95 &)
% ( 47 <=>; 49 =>; 0 <=; 1 <~>)
% Maximal formula depth : 28 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 24 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 8 con; 0-7 aty)
% Number of variables : 232 ( 209 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [X] :
( mem(X,A)
=> mem(ap(F,X),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Q] :
( mem(Q,bool)
=> ! [R] :
( mem(R,bool)
=> ( ( p(Q)
<=> p(R) )
=> Q = R ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A_27a] :
( ne(A_27a)
=> ! [A_27b] :
( ne(A_27b)
=> ! [V0i] :
( mem(V0i,arr(A_27a,A_27b))
=> ! [V1P] :
( mem(V1P,arr(A_27b,bool))
=> ( ! [V16i] :
( mem(V16i,arr(A_27a,A_27b))
=> ! [V17P] :
( mem(V17P,arr(A_27b,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P))
<=> ! [V18v] :
( mem(V18v,A_27b)
=> ( ~ p(ap(V17P,V18v))
=> ? [V19fv] :
( V18v = ap(V16i,V19fv)
& mem(V19fv,A_27a) ) ) ) ) ) )
& ! [V12i] :
( mem(V12i,arr(A_27a,A_27b))
=> ! [V13P] :
( mem(V13P,arr(A_27b,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P))
<=> ! [V14v] :
( mem(V14v,A_27b)
=> ( p(ap(V13P,V14v))
=> ? [V15fv] :
( V14v = ap(V12i,V15fv)
& mem(V15fv,A_27a) ) ) ) ) ) )
& ! [V9i] :
( mem(V9i,arr(A_27a,A_27b))
=> ! [V10P] :
( mem(V10P,arr(A_27b,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P))
<=> ! [V11fv] :
( mem(V11fv,A_27a)
=> ~ p(ap(V10P,ap(V9i,V11fv))) ) ) ) )
& ! [V6i] :
( mem(V6i,arr(A_27a,A_27b))
=> ! [V7P] :
( mem(V7P,arr(A_27b,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P))
<=> ! [V8fv] :
( mem(V8fv,A_27a)
=> p(ap(V7P,ap(V6i,V8fv))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))
<=> ! [V4v] :
( mem(V4v,A_27b)
=> ( ~ p(ap(V1P,V4v))
=> ? [V5fv] :
( ~ p(ap(V1P,ap(V0i,V5fv)))
& mem(V5fv,A_27a) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P))
<=> ! [V2v] :
( mem(V2v,A_27b)
=> ( p(ap(V1P,V2v))
=> ? [V3fv] :
( p(ap(V1P,ap(V0i,V3fv)))
& mem(V3fv,A_27a) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [V0p] :
( mem(V0p,bool)
=> ! [V1q] :
( mem(V1q,bool)
=> ! [V2r] :
( mem(V2r,bool)
=> ( ( p(V0p)
<=> ( p(V1q)
<=> p(V2r) ) )
<=> ( ( ~ p(V0p)
| ~ p(V1q)
| p(V2r) )
& ( ~ p(V0p)
| ~ p(V2r)
| p(V1q) )
& ( ~ p(V1q)
| ~ p(V2r)
| p(V0p) )
& ( p(V2r)
| p(V1q)
| p(V0p) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,conjecture,
! [A_27a] :
( ne(A_27a)
=> ! [A_27b] :
( ne(A_27b)
=> ! [V0i] :
( mem(V0i,arr(A_27b,A_27a))
=> ! [V1P] :
( mem(V1P,arr(A_27a,bool))
=> ! [V2Q] :
( mem(V2Q,arr(A_27a,bool))
=> ( ! [V3x] :
( mem(V3x,A_27a)
=> ( p(ap(V2Q,V3x))
=> p(ap(V1P,V3x)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V1P))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V2Q)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ ! [A_27a] :
( ne(A_27a)
=> ! [A_27b] :
( ne(A_27b)
=> ! [V0i] :
( mem(V0i,arr(A_27b,A_27a))
=> ! [V1P] :
( mem(V1P,arr(A_27a,bool))
=> ! [V2Q] :
( mem(V2Q,arr(A_27a,bool))
=> ( ! [V3x] :
( mem(V3x,A_27a)
=> ( p(ap(V2Q,V3x))
=> p(ap(V1P,V3x)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V1P))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V2Q)) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f58,plain,
! [A,B,F] :
( ! [X] :
( mem(ap(F,X),B)
| ~ mem(X,A) )
| ~ mem(F,arr(A,B)) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( mem(ap(X0,X3),X2)
| ~ mem(X3,X1)
| ~ mem(X0,arr(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [Q] :
( ! [R] :
( Q = R
| ( p(Q)
<~> p(R) )
| ~ mem(R,bool) )
| ~ mem(Q,bool) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f61,plain,
! [Q] :
( ! [R] :
( Q = R
| ( ( ~ p(R)
| ~ p(Q) )
& ( p(R)
| p(Q) ) )
| ~ mem(R,bool) )
| ~ mem(Q,bool) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( X0 = X1
| p(X1)
| p(X0)
| ~ mem(X1,bool)
| ~ mem(X0,bool) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f73,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f74,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f95,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f96,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f126,plain,
! [A_27a] :
( mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool))
| ~ ne(A_27a) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f127,plain,
! [X0] :
( mem(c_2Ebool_2E_21(X0),arr(arr(X0,bool),bool))
| ~ ne(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f178,plain,
! [A_27a] :
( ! [A_27b] :
( ! [V0i] :
( ! [V1P] :
( ( ! [V16i] :
( ! [V17P] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P))
<=> ! [V18v] :
( ? [V19fv] :
( V18v = ap(V16i,V19fv)
& mem(V19fv,A_27a) )
| p(ap(V17P,V18v))
| ~ mem(V18v,A_27b) ) )
| ~ mem(V17P,arr(A_27b,bool)) )
| ~ mem(V16i,arr(A_27a,A_27b)) )
& ! [V12i] :
( ! [V13P] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P))
<=> ! [V14v] :
( ? [V15fv] :
( V14v = ap(V12i,V15fv)
& mem(V15fv,A_27a) )
| ~ p(ap(V13P,V14v))
| ~ mem(V14v,A_27b) ) )
| ~ mem(V13P,arr(A_27b,bool)) )
| ~ mem(V12i,arr(A_27a,A_27b)) )
& ! [V9i] :
( ! [V10P] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P))
<=> ! [V11fv] :
( ~ p(ap(V10P,ap(V9i,V11fv)))
| ~ mem(V11fv,A_27a) ) )
| ~ mem(V10P,arr(A_27b,bool)) )
| ~ mem(V9i,arr(A_27a,A_27b)) )
& ! [V6i] :
( ! [V7P] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P))
<=> ! [V8fv] :
( p(ap(V7P,ap(V6i,V8fv)))
| ~ mem(V8fv,A_27a) ) )
| ~ mem(V7P,arr(A_27b,bool)) )
| ~ mem(V6i,arr(A_27a,A_27b)) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))
<=> ! [V4v] :
( ? [V5fv] :
( ~ p(ap(V1P,ap(V0i,V5fv)))
& mem(V5fv,A_27a) )
| p(ap(V1P,V4v))
| ~ mem(V4v,A_27b) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P))
<=> ! [V2v] :
( ? [V3fv] :
( p(ap(V1P,ap(V0i,V3fv)))
& mem(V3fv,A_27a) )
| ~ p(ap(V1P,V2v))
| ~ mem(V2v,A_27b) ) ) )
| ~ mem(V1P,arr(A_27b,bool)) )
| ~ mem(V0i,arr(A_27a,A_27b)) )
| ~ ne(A_27b) )
| ~ ne(A_27a) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f179,plain,
! [A_27a] :
( ! [A_27b] :
( ! [V0i] :
( ! [V1P] :
( ( ! [V16i] :
( ! [V17P] :
( ( ( ? [V18v] :
( ! [V19fv] :
( V18v != ap(V16i,V19fv)
| ~ mem(V19fv,A_27a) )
& ~ p(ap(V17P,V18v))
& mem(V18v,A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P)) )
& ( ! [V18v] :
( ? [V19fv] :
( V18v = ap(V16i,V19fv)
& mem(V19fv,A_27a) )
| p(ap(V17P,V18v))
| ~ mem(V18v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P)) ) )
| ~ mem(V17P,arr(A_27b,bool)) )
| ~ mem(V16i,arr(A_27a,A_27b)) )
& ! [V12i] :
( ! [V13P] :
( ( ( ? [V14v] :
( ! [V15fv] :
( V14v != ap(V12i,V15fv)
| ~ mem(V15fv,A_27a) )
& p(ap(V13P,V14v))
& mem(V14v,A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P)) )
& ( ! [V14v] :
( ? [V15fv] :
( V14v = ap(V12i,V15fv)
& mem(V15fv,A_27a) )
| ~ p(ap(V13P,V14v))
| ~ mem(V14v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P)) ) )
| ~ mem(V13P,arr(A_27b,bool)) )
| ~ mem(V12i,arr(A_27a,A_27b)) )
& ! [V9i] :
( ! [V10P] :
( ( ( ? [V11fv] :
( p(ap(V10P,ap(V9i,V11fv)))
& mem(V11fv,A_27a) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P)) )
& ( ! [V11fv] :
( ~ p(ap(V10P,ap(V9i,V11fv)))
| ~ mem(V11fv,A_27a) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P)) ) )
| ~ mem(V10P,arr(A_27b,bool)) )
| ~ mem(V9i,arr(A_27a,A_27b)) )
& ! [V6i] :
( ! [V7P] :
( ( ( ? [V8fv] :
( ~ p(ap(V7P,ap(V6i,V8fv)))
& mem(V8fv,A_27a) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P)) )
& ( ! [V8fv] :
( p(ap(V7P,ap(V6i,V8fv)))
| ~ mem(V8fv,A_27a) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P)) ) )
| ~ mem(V7P,arr(A_27b,bool)) )
| ~ mem(V6i,arr(A_27a,A_27b)) )
& ( ? [V4v] :
( ! [V5fv] :
( p(ap(V1P,ap(V0i,V5fv)))
| ~ mem(V5fv,A_27a) )
& ~ p(ap(V1P,V4v))
& mem(V4v,A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) )
& ( ! [V4v] :
( ? [V5fv] :
( ~ p(ap(V1P,ap(V0i,V5fv)))
& mem(V5fv,A_27a) )
| p(ap(V1P,V4v))
| ~ mem(V4v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) )
& ( ? [V2v] :
( ! [V3fv] :
( ~ p(ap(V1P,ap(V0i,V3fv)))
| ~ mem(V3fv,A_27a) )
& p(ap(V1P,V2v))
& mem(V2v,A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) )
& ( ! [V2v] :
( ? [V3fv] :
( p(ap(V1P,ap(V0i,V3fv)))
& mem(V3fv,A_27a) )
| ~ p(ap(V1P,V2v))
| ~ mem(V2v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) ) )
| ~ mem(V1P,arr(A_27b,bool)) )
| ~ mem(V0i,arr(A_27a,A_27b)) )
| ~ ne(A_27b) )
| ~ ne(A_27a) ),
inference(NNF_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [A_27a] :
( ! [A_27b] :
( ! [V0i] :
( ! [V1P] :
( ( ! [V16i] :
( ! [V17P] :
( ( ( ( ! [V19fv] :
( sK12_skl(V17P,V16i,V1P,V0i,A_27b,A_27a) != ap(V16i,V19fv)
| ~ mem(V19fv,A_27a) )
& ~ p(ap(V17P,sK12_skl(V17P,V16i,V1P,V0i,A_27b,A_27a)))
& mem(sK12_skl(V17P,V16i,V1P,V0i,A_27b,A_27a),A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P)) )
& ( ! [V18v] :
( ( V18v = ap(V16i,sK11_skl(V18v,V17P,V16i,V1P,V0i,A_27b,A_27a))
& mem(sK11_skl(V18v,V17P,V16i,V1P,V0i,A_27b,A_27a),A_27a) )
| p(ap(V17P,V18v))
| ~ mem(V18v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P)) ) )
| ~ mem(V17P,arr(A_27b,bool)) )
| ~ mem(V16i,arr(A_27a,A_27b)) )
& ! [V12i] :
( ! [V13P] :
( ( ( ( ! [V15fv] :
( sK10_skl(V13P,V12i,V1P,V0i,A_27b,A_27a) != ap(V12i,V15fv)
| ~ mem(V15fv,A_27a) )
& p(ap(V13P,sK10_skl(V13P,V12i,V1P,V0i,A_27b,A_27a)))
& mem(sK10_skl(V13P,V12i,V1P,V0i,A_27b,A_27a),A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P)) )
& ( ! [V14v] :
( ( V14v = ap(V12i,sK9_skl(V14v,V13P,V12i,V1P,V0i,A_27b,A_27a))
& mem(sK9_skl(V14v,V13P,V12i,V1P,V0i,A_27b,A_27a),A_27a) )
| ~ p(ap(V13P,V14v))
| ~ mem(V14v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P)) ) )
| ~ mem(V13P,arr(A_27b,bool)) )
| ~ mem(V12i,arr(A_27a,A_27b)) )
& ! [V9i] :
( ! [V10P] :
( ( ( ( p(ap(V10P,ap(V9i,sK8_skl(V10P,V9i,V1P,V0i,A_27b,A_27a))))
& mem(sK8_skl(V10P,V9i,V1P,V0i,A_27b,A_27a),A_27a) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P)) )
& ( ! [V11fv] :
( ~ p(ap(V10P,ap(V9i,V11fv)))
| ~ mem(V11fv,A_27a) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P)) ) )
| ~ mem(V10P,arr(A_27b,bool)) )
| ~ mem(V9i,arr(A_27a,A_27b)) )
& ! [V6i] :
( ! [V7P] :
( ( ( ( ~ p(ap(V7P,ap(V6i,sK7_skl(V7P,V6i,V1P,V0i,A_27b,A_27a))))
& mem(sK7_skl(V7P,V6i,V1P,V0i,A_27b,A_27a),A_27a) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P)) )
& ( ! [V8fv] :
( p(ap(V7P,ap(V6i,V8fv)))
| ~ mem(V8fv,A_27a) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P)) ) )
| ~ mem(V7P,arr(A_27b,bool)) )
| ~ mem(V6i,arr(A_27a,A_27b)) )
& ( ( ! [V5fv] :
( p(ap(V1P,ap(V0i,V5fv)))
| ~ mem(V5fv,A_27a) )
& ~ p(ap(V1P,sK6_skl(V1P,V0i,A_27b,A_27a)))
& mem(sK6_skl(V1P,V0i,A_27b,A_27a),A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) )
& ( ! [V4v] :
( ( ~ p(ap(V1P,ap(V0i,sK5_skl(V4v,V1P,V0i,A_27b,A_27a))))
& mem(sK5_skl(V4v,V1P,V0i,A_27b,A_27a),A_27a) )
| p(ap(V1P,V4v))
| ~ mem(V4v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) )
& ( ( ! [V3fv] :
( ~ p(ap(V1P,ap(V0i,V3fv)))
| ~ mem(V3fv,A_27a) )
& p(ap(V1P,sK4_skl(V1P,V0i,A_27b,A_27a)))
& mem(sK4_skl(V1P,V0i,A_27b,A_27a),A_27b) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) )
& ( ! [V2v] :
( ( p(ap(V1P,ap(V0i,sK3_skl(V2v,V1P,V0i,A_27b,A_27a))))
& mem(sK3_skl(V2v,V1P,V0i,A_27b,A_27a),A_27a) )
| ~ p(ap(V1P,V2v))
| ~ mem(V2v,A_27b) )
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) ) )
| ~ mem(V1P,arr(A_27b,bool)) )
| ~ mem(V0i,arr(A_27a,A_27b)) )
| ~ ne(A_27b) )
| ~ ne(A_27a) ),
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,sK3_skl(V2v,V1P,V0i,A_27b,A_27a)),skolemize(V2v,sK4_skl(V1P,V0i,A_27b,A_27a)),skolemize(V5fv,sK5_skl(V4v,V1P,V0i,A_27b,A_27a)),skolemize(V4v,sK6_skl(V1P,V0i,A_27b,A_27a)),skolemize(V8fv,sK7_skl(V7P,V6i,V1P,V0i,A_27b,A_27a)),skolemize(V11fv,sK8_skl(V10P,V9i,V1P,V0i,A_27b,A_27a)),skolemize(V15fv,sK9_skl(V14v,V13P,V12i,V1P,V0i,A_27b,A_27a)),skolemize(V14v,sK10_skl(V13P,V12i,V1P,V0i,A_27b,A_27a)),skolemize(V19fv,sK11_skl(V18v,V17P,V16i,V1P,V0i,A_27b,A_27a)),skolemize(V18v,sK12_skl(V17P,V16i,V1P,V0i,A_27b,A_27a))],[f179]) ).
fof(f194,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p(ap(X5,ap(X4,X6)))
| ~ mem(X6,X0)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X4),X5))
| ~ mem(X5,arr(X1,bool))
| ~ mem(X4,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X2,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f195,plain,
! [X0,X1,X2,X3,X4,X5] :
( mem(sK8_skl(X5,X4,X3,X2,X1,X0),X0)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X4),X5))
| ~ mem(X5,arr(X1,bool))
| ~ mem(X4,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X2,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f196,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(ap(X5,ap(X4,sK8_skl(X5,X4,X3,X2,X1,X0))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X4),X5))
| ~ mem(X5,arr(X1,bool))
| ~ mem(X4,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X2,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f234,plain,
! [V0p] :
( ! [V1q] :
( ! [V2r] :
( ( ( p(V0p)
<=> ( p(V1q)
<=> p(V2r) ) )
<=> ( ( ~ p(V0p)
| ~ p(V1q)
| p(V2r) )
& ( ~ p(V0p)
| ~ p(V2r)
| p(V1q) )
& ( ~ p(V1q)
| ~ p(V2r)
| p(V0p) )
& ( p(V2r)
| p(V1q)
| p(V0p) ) ) )
| ~ mem(V2r,bool) )
| ~ mem(V1q,bool) )
| ~ mem(V0p,bool) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f235,definition,
! [V0p,V1q,V2r] :
( sP4_prd(V2r,V1q,V0p)
<=> ( p(V0p)
<=> ( p(V1q)
<=> p(V2r) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f281,plain,
? [A_27a] :
( ? [A_27b] :
( ? [V0i] :
( ? [V1P] :
( ? [V2Q] :
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V2Q))
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V1P))
& ! [V3x] :
( p(ap(V1P,V3x))
| ~ p(ap(V2Q,V3x))
| ~ mem(V3x,A_27a) )
& mem(V2Q,arr(A_27a,bool)) )
& mem(V1P,arr(A_27a,bool)) )
& mem(V0i,arr(A_27b,A_27a)) )
& ne(A_27b) )
& ne(A_27a) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f282,plain,
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK17_skl))
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK16_skl))
& ! [V3x] :
( p(ap(sK16_skl,V3x))
| ~ p(ap(sK17_skl,V3x))
| ~ mem(V3x,sK13_skl) )
& mem(sK17_skl,arr(sK13_skl,bool))
& mem(sK16_skl,arr(sK13_skl,bool))
& mem(sK15_skl,arr(sK14_skl,sK13_skl))
& ne(sK14_skl)
& ne(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(A_27a,sK13_skl),skolemize(A_27b,sK14_skl),skolemize(V0i,sK15_skl),skolemize(V1P,sK16_skl),skolemize(V2Q,sK17_skl)],[f281]) ).
fof(f283,plain,
ne(sK13_skl),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f284,plain,
ne(sK14_skl),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f285,plain,
mem(sK15_skl,arr(sK14_skl,sK13_skl)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f286,plain,
mem(sK16_skl,arr(sK13_skl,bool)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f287,plain,
mem(sK17_skl,arr(sK13_skl,bool)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f288,plain,
! [X0] :
( p(ap(sK16_skl,X0))
| ~ p(ap(sK17_skl,X0))
| ~ mem(X0,sK13_skl) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f289,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK16_skl)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f290,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK17_skl)),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f319,definition,
! [V1q,V2r] :
( sP11_prd(V2r,V1q)
<=> ( p(V1q)
<=> p(V2r) ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f374,plain,
! [V1q,V2r] :
( ( ( ( p(V2r)
| p(V1q) )
& ( ~ p(V2r)
| ~ p(V1q) ) )
| sP11_prd(V2r,V1q) )
& ( ( ( ~ p(V2r)
| p(V1q) )
& ( p(V2r)
| ~ p(V1q) ) )
| ~ sP11_prd(V2r,V1q) ) ),
inference(NNF_transformation,[status(thm)],[f319]) ).
fof(f375,plain,
( ! [V1q,V2r] :
( ( ( p(V2r)
| p(V1q) )
& ( ~ p(V2r)
| ~ p(V1q) ) )
| sP11_prd(V2r,V1q) )
& ! [V1q,V2r] :
( ( ( ~ p(V2r)
| p(V1q) )
& ( p(V2r)
| ~ p(V1q) ) )
| ~ sP11_prd(V2r,V1q) ) ),
inference(miniscoping,[status(thm)],[f374]) ).
fof(f377,plain,
! [X0,X1] :
( ~ p(X0)
| p(X1)
| ~ sP11_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f378,plain,
! [X0,X1] :
( ~ p(X0)
| ~ p(X1)
| sP11_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f424,plain,
! [X0] :
( X0 = c_2Ebool_2ET
| p(c_2Ebool_2ET)
| p(X0)
| ~ mem(X0,bool) ),
inference(resolution,[status(thm)],[f73,f62]) ).
fof(f428,definition,
( sQ4_spl
<=> p(c_2Ebool_2ET) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f432,definition,
! [X0] :
( sQ5_spl
<=> ( X0 = c_2Ebool_2ET
| p(X0)
| ~ mem(X0,bool) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f433,plain,
! [X0] :
( ~ sQ5_spl
| X0 = c_2Ebool_2ET
| p(X0)
| ~ mem(X0,bool) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f435,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f424,f432,f428]) ).
fof(f437,plain,
! [X0] :
( X0 = c_2Ebool_2EF
| p(c_2Ebool_2EF)
| p(X0)
| ~ mem(X0,bool) ),
inference(resolution,[status(thm)],[f95,f62]) ).
fof(f441,definition,
( sQ7_spl
<=> p(c_2Ebool_2EF) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( ~ sQ7_spl
| p(c_2Ebool_2EF) ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f445,definition,
! [X0] :
( sQ8_spl
<=> ( X0 = c_2Ebool_2EF
| p(X0)
| ~ mem(X0,bool) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f446,plain,
! [X0] :
( ~ sQ8_spl
| X0 = c_2Ebool_2EF
| p(X0)
| ~ mem(X0,bool) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,plain,
( sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f437,f445,f441]) ).
fof(f463,plain,
( ~ sQ5_spl
| c_2Ebool_2EF = c_2Ebool_2ET
| ~ mem(c_2Ebool_2EF,bool) ),
inference(resolution,[status(thm)],[f433,f96]) ).
fof(f466,definition,
( sQ9_spl
<=> mem(c_2Ebool_2EF,bool) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ9_spl
| ~ mem(c_2Ebool_2EF,bool) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ10_spl
<=> c_2Ebool_2EF = c_2Ebool_2ET ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ10_spl
| c_2Ebool_2EF = c_2Ebool_2ET ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,plain,
( ~ sQ5_spl
| sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f463,f466,f469,f432]) ).
fof(f480,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f95]) ).
fof(f481,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f480]) ).
fof(f483,plain,
( ~ sQ10_spl
| ~ p(c_2Ebool_2ET) ),
inference(backward_demodulation,[status(thm)],[f470,f96]) ).
fof(f484,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f74]) ).
fof(f485,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f484]) ).
fof(f506,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ mem(X1,X2)
| ~ mem(X0,arr(X2,bool))
| ap(X0,X1) = c_2Ebool_2EF
| p(ap(X0,X1)) ),
inference(resolution,[status(thm)],[f446,f59]) ).
fof(f515,definition,
( sQ17_spl
<=> ne(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( sQ17_spl
| ~ ne(sK14_skl) ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,definition,
( sQ18_spl
<=> ne(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ18_spl
| ~ ne(sK13_skl) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,definition,
! [X0] :
( sQ19_spl
<=> ~ mem(X0,arr(sK14_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f522,plain,
! [X0] :
( ~ sQ19_spl
| ~ mem(X0,arr(sK14_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,definition,
! [X1] :
( sQ20_spl
<=> ~ mem(X1,arr(sK13_skl,bool)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f525,plain,
! [X0] :
( ~ sQ20_spl
| ~ mem(X0,arr(sK13_skl,bool)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,definition,
( sQ21_spl
<=> mem(sK15_skl,arr(sK14_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( sQ21_spl
| ~ mem(sK15_skl,arr(sK14_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f530,definition,
( sQ22_spl
<=> mem(sK16_skl,arr(sK13_skl,bool)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f532,plain,
( sQ22_spl
| ~ mem(sK16_skl,arr(sK13_skl,bool)) ),
inference(component_clause,[status(thm)],[f530]) ).
fof(f533,definition,
! [X2] :
( sQ23_spl
<=> ( ~ p(ap(sK16_skl,ap(sK15_skl,X2)))
| ~ mem(X2,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f534,plain,
! [X0] :
( ~ sQ23_spl
| ~ p(ap(sK16_skl,ap(sK15_skl,X0)))
| ~ mem(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f533]) ).
fof(f537,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f96]) ).
fof(f538,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f537]) ).
fof(f858,plain,
! [X0] :
( ~ p(X0)
| sP11_prd(X0,ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK16_skl)) ),
inference(resolution,[status(thm)],[f378,f289]) ).
fof(f884,plain,
sP11_prd(c_2Ebool_2ET,ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK14_skl,sK13_skl),sK15_skl),sK16_skl)),
inference(resolution,[status(thm)],[f858,f74]) ).
fof(f895,plain,
! [X0] :
( ~ sQ8_spl
| ~ mem(X0,sK13_skl)
| ap(sK17_skl,X0) = c_2Ebool_2EF
| p(ap(sK17_skl,X0)) ),
inference(resolution,[status(thm)],[f506,f287]) ).
fof(f1298,plain,
mem(c_2Ebool_2E_21(sK14_skl),arr(arr(sK14_skl,bool),bool)),
inference(resolution,[status(thm)],[f127,f284]) ).
fof(f1299,plain,
mem(c_2Ebool_2E_21(sK13_skl),arr(arr(sK13_skl,bool),bool)),
inference(resolution,[status(thm)],[f127,f283]) ).
fof(f1318,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f517,f284]) ).
fof(f1319,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1318]) ).
fof(f1339,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f283]) ).
fof(f1340,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1339]) ).
fof(f1532,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ p(ap(X4,ap(X3,X7)))
| ~ mem(X7,X1)
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| ~ mem(X6,arr(X2,bool))
| ~ mem(X5,arr(X1,X2))
| ~ ne(X2)
| ~ ne(X1)
| ~ p(X0)
| ~ sP11_prd(X0,ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4)) ),
inference(resolution,[status(thm)],[f377,f194]) ).
fof(f1649,definition,
( sQ96_spl
<=> mem(sK17_skl,arr(sK13_skl,bool)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1651,plain,
( sQ96_spl
| ~ mem(sK17_skl,arr(sK13_skl,bool)) ),
inference(component_clause,[status(thm)],[f1649]) ).
fof(f1656,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1651,f287]) ).
fof(f1657,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f1656]) ).
fof(f1907,plain,
! [X0,X1] :
( mem(sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl),sK14_skl)
| ~ mem(sK17_skl,arr(sK13_skl,bool))
| ~ mem(sK15_skl,arr(sK14_skl,sK13_skl))
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl))
| ~ ne(sK13_skl)
| ~ ne(sK14_skl) ),
inference(resolution,[status(thm)],[f195,f290]) ).
fof(f1909,definition,
! [X0,X1] :
( sQ106_spl
<=> ( mem(sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl),sK14_skl)
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1910,plain,
! [X0,X1] :
( ~ sQ106_spl
| mem(sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl),sK14_skl)
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f1909]) ).
fof(f1912,plain,
( ~ sQ96_spl
| ~ sQ21_spl
| sQ106_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1907,f515,f518,f1909,f527,f1649]) ).
fof(f1914,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f285]) ).
fof(f1915,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1914]) ).
fof(f1916,plain,
! [X0,X1] :
( p(ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl))))
| ~ mem(sK17_skl,arr(sK13_skl,bool))
| ~ mem(sK15_skl,arr(sK14_skl,sK13_skl))
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl))
| ~ ne(sK13_skl)
| ~ ne(sK14_skl) ),
inference(resolution,[status(thm)],[f196,f290]) ).
fof(f1918,definition,
! [X0,X1] :
( sQ107_spl
<=> ( p(ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl))))
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1919,plain,
! [X0,X1] :
( ~ sQ107_spl
| p(ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,X1,X0,sK13_skl,sK14_skl))))
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f1918]) ).
fof(f1921,plain,
( ~ sQ96_spl
| ~ sQ21_spl
| sQ107_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1916,f515,f518,f1918,f527,f1649]) ).
fof(f2161,plain,
! [X0] :
( ~ sQ8_spl
| p(ap(sK16_skl,X0))
| ~ mem(X0,sK13_skl)
| ~ mem(X0,sK13_skl)
| ap(sK17_skl,X0) = c_2Ebool_2EF ),
inference(resolution,[status(thm)],[f895,f288]) ).
fof(f2169,plain,
! [X0] :
( ~ sQ8_spl
| p(ap(sK16_skl,X0))
| ~ mem(X0,sK13_skl)
| ap(sK17_skl,X0) = c_2Ebool_2EF ),
inference(duplicate_literals_removal,[status(thm)],[f2161]) ).
fof(f2563,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f287,f525]) ).
fof(f2567,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f2563]) ).
fof(f2647,plain,
! [X0,X1,X2] :
( ~ p(ap(sK16_skl,ap(sK15_skl,X2)))
| ~ mem(X2,sK14_skl)
| ~ mem(sK16_skl,arr(sK13_skl,bool))
| ~ mem(sK15_skl,arr(sK14_skl,sK13_skl))
| ~ mem(X1,arr(sK13_skl,bool))
| ~ mem(X0,arr(sK14_skl,sK13_skl))
| ~ ne(sK13_skl)
| ~ ne(sK14_skl)
| ~ p(c_2Ebool_2ET) ),
inference(resolution,[status(thm)],[f1532,f884]) ).
fof(f2651,plain,
( sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| sQ20_spl
| sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2647,f428,f515,f518,f521,f524,f527,f530,f533]) ).
fof(f2799,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f532,f286]) ).
fof(f2800,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f2799]) ).
fof(f2805,plain,
( ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f285,f522]) ).
fof(f2808,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f2805]) ).
fof(f2866,plain,
! [X0] :
( ~ sQ106_spl
| mem(sK8_skl(sK17_skl,sK15_skl,X0,sK15_skl,sK13_skl,sK14_skl),sK14_skl)
| ~ mem(X0,arr(sK13_skl,bool)) ),
inference(resolution,[status(thm)],[f1910,f285]) ).
fof(f2909,definition,
! [X0] :
( sQ151_spl
<=> ( ~ mem(X0,bool)
| ~ p(X0)
| ~ mem(X0,bool) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2910,plain,
! [X0] :
( ~ sQ151_spl
| ~ mem(X0,bool)
| ~ p(X0)
| ~ mem(X0,bool) ),
inference(component_clause,[status(thm)],[f2909]) ).
fof(f2943,definition,
( sQ152_spl
<=> mem(c_2Ebool_2E_21(sK14_skl),arr(arr(sK14_skl,bool),bool)) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f2945,plain,
( sQ152_spl
| ~ mem(c_2Ebool_2E_21(sK14_skl),arr(arr(sK14_skl,bool),bool)) ),
inference(component_clause,[status(thm)],[f2943]) ).
fof(f2950,plain,
( sQ152_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2945,f1298]) ).
fof(f2951,plain,
sQ152_spl,
inference(contradiction_clause,[status(thm)],[f2950]) ).
fof(f2969,definition,
! [X5] :
( sQ155_spl
<=> ~ mem(X5,arr(arr(sK14_skl,bool),bool)) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f2970,plain,
! [X0] :
( ~ sQ155_spl
| ~ mem(X0,arr(arr(sK14_skl,bool),bool)) ),
inference(component_clause,[status(thm)],[f2969]) ).
fof(f2977,plain,
( ~ sQ155_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1298,f2970]) ).
fof(f2981,plain,
~ sQ155_spl,
inference(contradiction_clause,[status(thm)],[f2977]) ).
fof(f3134,definition,
( sQ169_spl
<=> mem(c_2Ebool_2E_21(sK13_skl),arr(arr(sK13_skl,bool),bool)) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f3136,plain,
( sQ169_spl
| ~ mem(c_2Ebool_2E_21(sK13_skl),arr(arr(sK13_skl,bool),bool)) ),
inference(component_clause,[status(thm)],[f3134]) ).
fof(f3143,plain,
! [X0] :
( ~ sQ151_spl
| ~ p(X0)
| ~ mem(X0,bool) ),
inference(duplicate_literals_removal,[status(thm)],[f2910]) ).
fof(f3144,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3136,f1299]) ).
fof(f3145,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f3144]) ).
fof(f3174,plain,
( ~ sQ151_spl
| ~ p(c_2Ebool_2ET) ),
inference(resolution,[status(thm)],[f3143,f73]) ).
fof(f3178,plain,
( ~ sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3174,f74]) ).
fof(f3179,plain,
~ sQ151_spl,
inference(contradiction_clause,[status(thm)],[f3178]) ).
fof(f3198,definition,
! [X5] :
( sQ172_spl
<=> ~ mem(X5,arr(arr(sK13_skl,bool),bool)) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f3199,plain,
! [X0] :
( ~ sQ172_spl
| ~ mem(X0,arr(arr(sK13_skl,bool),bool)) ),
inference(component_clause,[status(thm)],[f3198]) ).
fof(f3281,plain,
( ~ sQ172_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1299,f3199]) ).
fof(f3285,plain,
~ sQ172_spl,
inference(contradiction_clause,[status(thm)],[f3281]) ).
fof(f3814,plain,
( ~ sQ106_spl
| mem(sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f2866,f286]) ).
fof(f3825,plain,
( ~ sQ23_spl
| ~ sQ106_spl
| ~ p(ap(sK16_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl)))) ),
inference(resolution,[status(thm)],[f3814,f534]) ).
fof(f3858,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| ~ sQ106_spl
| ~ mem(ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl)),sK13_skl)
| ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl))) = c_2Ebool_2EF ),
inference(resolution,[status(thm)],[f3825,f2169]) ).
fof(f3866,definition,
( sQ209_spl
<=> mem(ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl)),sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f3868,plain,
( sQ209_spl
| ~ mem(ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl)),sK13_skl) ),
inference(component_clause,[status(thm)],[f3866]) ).
fof(f3878,definition,
( sQ212_spl
<=> ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl))) = c_2Ebool_2EF ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f3879,plain,
( ~ sQ212_spl
| ap(sK17_skl,ap(sK15_skl,sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl))) = c_2Ebool_2EF ),
inference(component_clause,[status(thm)],[f3878]) ).
fof(f3881,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| ~ sQ106_spl
| ~ sQ209_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f3858,f3878,f3866,f1909,f533,f445]) ).
fof(f3890,plain,
! [X0] :
( sQ209_spl
| ~ mem(sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl),X0)
| ~ mem(sK15_skl,arr(X0,sK13_skl)) ),
inference(resolution,[status(thm)],[f3868,f59]) ).
fof(f3986,plain,
( sQ209_spl
| ~ mem(sK8_skl(sK17_skl,sK15_skl,sK16_skl,sK15_skl,sK13_skl,sK14_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f3890,f285]) ).
fof(f3987,plain,
( sQ209_spl
| ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3986,f3814]) ).
fof(f3988,plain,
( sQ209_spl
| ~ sQ106_spl ),
inference(contradiction_clause,[status(thm)],[f3987]) ).
fof(f4024,plain,
( ~ sQ212_spl
| ~ sQ107_spl
| p(c_2Ebool_2EF)
| ~ mem(sK16_skl,arr(sK13_skl,bool))
| ~ mem(sK15_skl,arr(sK14_skl,sK13_skl)) ),
inference(paramodulation,[status(thm)],[f3879,f1919]) ).
fof(f4030,plain,
( ~ sQ212_spl
| ~ sQ107_spl
| sQ7_spl
| ~ sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f4024,f527,f530,f441,f1918,f3878]) ).
fof(f4035,plain,
$false,
inference(sat_refutation,[status(thm)],[f435,f448,f472,f481,f485,f538,f1319,f1340,f1657,f1912,f1915,f1921,f2567,f2651,f2800,f2808,f2951,f2981,f3145,f3179,f3285,f3881,f3988,f4030]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.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:41:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 5.48/1.24 % Refutation found
% 5.48/1.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.48/1.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.48/1.26 % Elapsed time: 0.885952 seconds
% 5.48/1.26 % CPU time: 6.668521 seconds
% 5.48/1.26 % Total memory used: 190.409 MB
% 5.48/1.26 % Net memory used: 179.454 MB
%------------------------------------------------------------------------------