%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : ITP006+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 06:46:16 PM UTC 2025
% Result : Theorem 25.33s 3.56s
% Output : CNFRefutation 25.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 52 ( 37 unt; 0 def)
% Number of atoms : 168 ( 2 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 181 ( 65 ~; 59 |; 9 &)
% ( 6 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-6 aty)
% Number of variables : 62 ( 2 sgn 34 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,plain,
! [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/sandbox2/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
fof(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated,plain,
~ ! [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(negate_conjecture,[status(cth)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
cnf(166,plain,
( ~ p(ap(sK23,X0))
| ~ mem(X0,sK19)
| p(ap(sK22,X0)) ),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l0,plain,
( ~ p(ap(sK23,ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23))))
| ~ mem(ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23)),sK19)
| p(ap(sK22,ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23)))) ),
inference(instantiation,[status(thm)],[166]) ).
fof(conj_thm_2EquantHeuristics_2EGUESS__REWRITES,plain,
! [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))
=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P))
<=> ! [V2v] :
( mem(V2v,A_27b)
=> ( p(ap(V1P,V2v))
=> ? [V3fv] :
( mem(V3fv,A_27a)
& p(ap(V1P,ap(V0i,V3fv))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))
<=> ! [V4v] :
( mem(V4v,A_27b)
=> ( ~ p(ap(V1P,V4v))
=> ? [V5fv] :
( mem(V5fv,A_27a)
& ~ p(ap(V1P,ap(V0i,V5fv))) ) ) ) )
& ! [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))) ) ) ) )
& ! [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))) ) ) ) )
& ! [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] :
( mem(V15fv,A_27a)
& V14v = ap(V12i,V15fv) ) ) ) ) ) )
& ! [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] :
( mem(V19fv,A_27a)
& V18v = ap(V16i,V19fv) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__REWRITES) ).
cnf(72,plain,
( ~ ne(X0)
| ~ ne(X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X4,arr(X0,X1))
| ~ mem(X5,arr(X1,bool))
| p(ap(X5,ap(X4,sK12(X0,X1,X2,X3,X4,X5))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X4),X5)) ),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
cnf(l1,plain,
( ~ ne(sK20)
| ~ ne(sK19)
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK22,arr(sK19,bool))
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK23,arr(sK19,bool))
| p(ap(sK23,ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23)) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(165,plain,
mem(sK23,arr(sK19,bool)),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l19,plain,
mem(sK23,arr(sK19,bool)),
inference(instantiation,[status(thm)],[165]) ).
cnf(164,plain,
mem(sK22,arr(sK19,bool)),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l21,plain,
mem(sK22,arr(sK19,bool)),
inference(instantiation,[status(thm)],[164]) ).
cnf(168,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23)),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l30,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23)),
inference(instantiation,[status(thm)],[168]) ).
cnf(161,plain,
ne(sK19),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l46,plain,
ne(sK19),
inference(instantiation,[status(thm)],[161]) ).
cnf(163,plain,
mem(sK21,arr(sK20,sK19)),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l16,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(162,plain,
ne(sK20),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l13,plain,
ne(sK20),
inference(instantiation,[status(thm)],[162]) ).
cnf(l2,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
fof(ap_tp,plain,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [X] :
( mem(X,A)
=> mem(ap(F,X),B) ) ),
file('Axioms/ITP001/ITP001+2.ax',ap_tp) ).
cnf(3,plain,
( ~ mem(X0,arr(X1,X2))
| ~ mem(X3,X1)
| mem(ap(X0,X3),X2) ),
inference(cnf,[status(esa)],[ap_tp]) ).
cnf(l111,plain,
( ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK12(sK20,sK19,sK21,sK22,sK21,sK23),sK20)
| mem(ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23)),sK19) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l114,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(71,plain,
( ~ ne(X0)
| ~ ne(X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X4,arr(X0,X1))
| ~ mem(X5,arr(X1,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X4),X5))
| mem(sK12(X0,X1,X2,X3,X4,X5),X0) ),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
cnf(l115,plain,
( ~ ne(sK20)
| ~ ne(sK19)
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK22,arr(sK19,bool))
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK23,arr(sK19,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23))
| mem(sK12(sK20,sK19,sK21,sK22,sK21,sK23),sK20) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l269,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l271,plain,
mem(sK22,arr(sK19,bool)),
inference(instantiation,[status(thm)],[164]) ).
cnf(l268,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l121,plain,
ne(sK20),
inference(instantiation,[status(thm)],[162]) ).
cnf(l137,plain,
ne(sK19),
inference(instantiation,[status(thm)],[161]) ).
cnf(l302,plain,
mem(sK23,arr(sK19,bool)),
inference(instantiation,[status(thm)],[165]) ).
cnf(70,plain,
( ~ ne(X0)
| ~ ne(X1)
| ~ p(ap(X2,ap(X3,X4)))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X3),X2))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X6,arr(X1,bool))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X1,bool))
| ~ mem(X4,X0) ),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
cnf(l113,plain,
( ~ ne(sK20)
| ~ ne(sK19)
| ~ p(ap(sK22,ap(sK21,sK12(sK20,sK19,sK21,sK22,sK21,sK23))))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK22))
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK22,arr(sK19,bool))
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK22,arr(sK19,bool))
| ~ mem(sK12(sK20,sK19,sK21,sK22,sK21,sK23),sK20) ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l132,plain,
ne(sK19),
inference(instantiation,[status(thm)],[161]) ).
cnf(l165,plain,
mem(sK22,arr(sK19,bool)),
inference(instantiation,[status(thm)],[164]) ).
cnf(l209,plain,
ne(sK20),
inference(instantiation,[status(thm)],[162]) ).
cnf(l166,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l183,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l167,plain,
mem(sK22,arr(sK19,bool)),
inference(instantiation,[status(thm)],[164]) ).
cnf(167,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK22)),
inference(cnf,[status(esa)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT_negated]) ).
cnf(l169,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK22)),
inference(instantiation,[status(thm)],[167]) ).
cnf(l261,plain,
( ~ ne(sK20)
| ~ ne(sK19)
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK22,arr(sK19,bool))
| ~ mem(sK21,arr(sK20,sK19))
| ~ mem(sK23,arr(sK19,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23))
| mem(sK12(sK20,sK19,sK21,sK22,sK21,sK23),sK20) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l289,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l292,plain,
mem(sK23,arr(sK19,bool)),
inference(instantiation,[status(thm)],[165]) ).
cnf(l288,plain,
ne(sK20),
inference(instantiation,[status(thm)],[162]) ).
cnf(l296,plain,
mem(sK21,arr(sK20,sK19)),
inference(instantiation,[status(thm)],[163]) ).
cnf(l284,plain,
ne(sK19),
inference(instantiation,[status(thm)],[161]) ).
cnf(l295,plain,
mem(sK22,arr(sK19,bool)),
inference(instantiation,[status(thm)],[164]) ).
cnf(l291,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23)),
inference(instantiation,[status(thm)],[168]) ).
cnf(l299,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK20,sK19),sK21),sK23)),
inference(instantiation,[status(thm)],[168]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l19,l21,l30,l46,l16,l13,l2,l111,l114,l115,l269,l271,l268,l121,l137,l302,l113,l132,l165,l209,l166,l183,l167,l169,l261,l289,l292,l288,l296,l284,l295,l291,l299]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ITP006+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% 0.10/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 19:33:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.19/0.54 % launching worker at depth: 10
% 25.33/3.56 % SZS status Theorem for theBenchmark
% 25.33/3.56 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------