%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n005.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:47:31 PM UTC 2026
% Result : Theorem 3.94s 1.39s
% Output : CNFRefutation 3.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 15
% Syntax : Number of formulae : 108 ( 27 unt; 6 def)
% Number of atoms : 484 ( 32 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 449 ( 191 ~; 207 |; 20 &)
% ( 6 <=>; 23 =>; 0 <=; 2 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 7 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 147 ( 0 sgn 143 !; 4 ?; 49 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f5,axiom,
! [X0] :
( mem(X0,bool)
=> ! [X1] :
( mem(X1,bool)
=> ( ( p(X0)
<=> p(X1) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(f11,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2ESUBSET(X0),arr(arr(X0,bool),arr(arr(X0,bool),bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2ESUBSET) ).
fof(f17,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2ECHOICE) ).
fof(f19,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2EREST(X0),arr(arr(X0,bool),arr(X0,bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2EREST) ).
fof(f24,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> ! [X2] :
( mem(X2,arr(X0,bool))
=> ( p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
<=> ! [X3] :
( mem(X3,X0)
=> ( p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
=> p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Epred__set_2ESUBSET__DEF) ).
fof(f25,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> ! [X2] :
( mem(X2,X0)
=> ! [X3] :
( mem(X3,X0)
=> ( p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))
<=> ( X2 != X3
& p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EIN__DELETE) ).
fof(f26,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Epred__set_2EREST__DEF) ).
fof(f27,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EREST__SUBSET) ).
fof(f28,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1)) ) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ~ mem(X2,arr(X0,X1))
| ! [X3] :
( ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f31,plain,
! [X0] :
( ~ mem(X0,bool)
| ! [X1] :
( ~ mem(X1,bool)
| ( p(X0)
<~> p(X1) )
| X0 = X1 ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f32,plain,
! [X0] :
( ~ mem(X0,bool)
| ! [X1] :
( ~ mem(X1,bool)
| ( p(X0)
<~> p(X1) )
| X0 = X1 ) ),
inference(flattening,[],[f31]) ).
fof(f38,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2ESUBSET(X0),arr(arr(X0,bool),arr(arr(X0,bool),bool))) ),
inference(ennf_transformation,[],[f11]) ).
fof(f42,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0)) ),
inference(ennf_transformation,[],[f17]) ).
fof(f44,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2EREST(X0),arr(arr(X0,bool),arr(X0,bool))) ),
inference(ennf_transformation,[],[f19]) ).
fof(f49,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,arr(X0,bool))
| ( p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
<=> ! [X3] :
( ~ mem(X3,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) ) ) ) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f50,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,arr(X0,bool))
| ( p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
<=> ! [X3] :
( ~ mem(X3,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) ) ) ) ) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,X0)
| ! [X3] :
( ~ mem(X3,X0)
| ( p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))
<=> ( X2 != X3
& p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)) ) ) ) ) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f52,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)) ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f53,plain,
? [X0] :
( ne(X0)
& ? [X1] :
( mem(X1,arr(X0,bool))
& ~ p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1)) ) ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,plain,
! [X0] :
( ~ mem(X0,bool)
| ! [X1] :
( ~ mem(X1,bool)
| ( ( p(X0)
| p(X1) )
& ( ~ p(X0)
| ~ p(X1) ) )
| X0 = X1 ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f65,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,arr(X0,bool))
| ( ( ~ p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
| ! [X3] :
( ~ mem(X3,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) ) )
& ( ? [X3] :
( mem(X3,X0)
& p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
& ~ p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) )
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ) ) ) ) ),
inference(nnf_transformation,[],[f50]) ).
fof(f66,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,arr(X0,bool))
| ( ( ~ p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
| ! [X4] :
( ~ mem(X4,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X4),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X4),X2)) ) )
& ( ? [X3] :
( mem(X3,X0)
& p(ap(ap(c_2Ebool_2EIN(X0),X3),X1))
& ~ p(ap(ap(c_2Ebool_2EIN(X0),X3),X2)) )
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ) ) ) ) ),
inference(rectify,[],[f65]) ).
fof(f67,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,arr(X0,bool))
| ( ( ~ p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
| ! [X4] :
( ~ mem(X4,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X4),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X4),X2)) ) )
& ( ( mem(sK2(X0,X1,X2),X0)
& p(ap(ap(c_2Ebool_2EIN(X0),sK2(X0,X1,X2)),X1))
& ~ p(ap(ap(c_2Ebool_2EIN(X0),sK2(X0,X1,X2)),X2)) )
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f66]) ).
fof(f68,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,X0)
| ! [X3] :
( ~ mem(X3,X0)
| ( ( ~ p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))
| ( X2 != X3
& p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)) ) )
& ( X2 = X3
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X2),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3))) ) ) ) ) ) ),
inference(nnf_transformation,[],[f51]) ).
fof(f69,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ mem(X1,arr(X0,bool))
| ! [X2] :
( ~ mem(X2,X0)
| ! [X3] :
( ~ mem(X3,X0)
| ( ( ~ p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))
| ( X2 != X3
& p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)) ) )
& ( X2 = X3
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X2),X1))
| p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3))) ) ) ) ) ) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
( ne(sK3)
& mem(sK4,arr(sK3,bool))
& ~ p(ap(ap(c_2Epred__set_2ESUBSET(sK3),ap(c_2Epred__set_2EREST(sK3),sK4)),sK4)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X0,sK3),skolemize(X1,sK4)],[f53]) ).
fof(f74,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f75,plain,
! [X0,X1] :
( ~ mem(X0,bool)
| ~ mem(X1,bool)
| p(X0)
| p(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f54]) ).
fof(f85,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2ESUBSET(X0),arr(arr(X0,bool),arr(arr(X0,bool),bool))) ),
inference(cnf_transformation,[],[f38]) ).
fof(f94,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f96,plain,
! [X0] :
( ~ ne(X0)
| mem(c_2Epred__set_2EREST(X0),arr(arr(X0,bool),arr(X0,bool))) ),
inference(cnf_transformation,[],[f44]) ).
fof(f105,plain,
! [X2,X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ~ mem(X2,arr(X0,bool))
| mem(sK2(X0,X1,X2),X0)
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f106,plain,
! [X2,X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ~ mem(X2,arr(X0,bool))
| p(ap(ap(c_2Ebool_2EIN(X0),sK2(X0,X1,X2)),X1))
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f107,plain,
! [X2,X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ~ mem(X2,arr(X0,bool))
| ~ p(ap(ap(c_2Ebool_2EIN(X0),sK2(X0,X1,X2)),X2))
| p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f109,plain,
! [X2,X3,X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ~ mem(X2,X0)
| ~ mem(X3,X0)
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))
| p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)) ),
inference(cnf_transformation,[],[f69]) ).
fof(f111,plain,
! [X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f112,plain,
ne(sK3),
inference(cnf_transformation,[],[f70]) ).
fof(f113,plain,
mem(sK4,arr(sK3,bool)),
inference(cnf_transformation,[],[f70]) ).
fof(f114,plain,
~ p(ap(ap(c_2Epred__set_2ESUBSET(sK3),ap(c_2Epred__set_2EREST(sK3),sK4)),sK4)),
inference(cnf_transformation,[],[f70]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( mem(ap(X0,X3),X2)
| ~ mem(X3,X1)
| ~ mem(X0,arr(X1,X2)) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p(X1)
| p(X0)
| ( X0 = X1 )
| ~ mem(X1,bool)
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_63,plain,
! [X0: $i] :
( mem(c_2Epred__set_2ESUBSET(X0),arr(arr(X0,bool),arr(arr(X0,bool),bool)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_72,plain,
! [X0: $i] :
( mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_74,plain,
! [X0: $i] :
( mem(c_2Epred__set_2EREST(X0),arr(arr(X0,bool),arr(X0,bool)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))
| ~ ne(X0)
| ~ mem(X2,arr(X0,bool))
| ~ mem(X1,arr(X0,bool))
| ~ p(ap(ap(c_2Ebool_2EIN(X0),sK2(X0,X1,X2)),X2)) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(X1),X0),X2))
| p(ap(ap(c_2Ebool_2EIN(X1),sK2(X1,X0,X2)),X0))
| ~ ne(X1)
| ~ mem(X2,arr(X1,bool))
| ~ mem(X0,arr(X1,bool)) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( mem(sK2(X1,X0,X2),X1)
| p(ap(ap(c_2Epred__set_2ESUBSET(X1),X0),X2))
| ~ ne(X1)
| ~ mem(X2,arr(X1,bool))
| ~ mem(X0,arr(X1,bool)) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(ap(ap(c_2Ebool_2EIN(X0),X1),X2))
| ~ ne(X0)
| ~ mem(X3,X0)
| ~ mem(X1,X0)
| ~ mem(X2,arr(X0,bool))
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X1),ap(ap(c_2Epred__set_2EDELETE(X0),X2),X3))) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( ( ap(ap(c_2Epred__set_2EDELETE(X1),X0),ap(c_2Epred__set_2ECHOICE(X1),X0)) = ap(c_2Epred__set_2EREST(X1),X0) )
| ~ ne(X1)
| ~ mem(X0,arr(X1,bool)) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_90,negated_conjecture,
~ p(ap(ap(c_2Epred__set_2ESUBSET(sK3),ap(c_2Epred__set_2EREST(sK3),sK4)),sK4)),
inference(cnf_transformation,[],[f114]) ).
tcf(c_91,negated_conjecture,
mem(sK4,arr(sK3,bool)),
inference(cnf_transformation,[],[f113]) ).
tcf(c_92,negated_conjecture,
ne(sK3),
inference(cnf_transformation,[],[f112]) ).
tcf(c_696,definition,
iPr_def_10 = arr(sK3,bool),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_697,definition,
iPr_def_11 = c_2Epred__set_2ESUBSET(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_698,definition,
iPr_def_12 = c_2Epred__set_2EREST(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_699,definition,
iPr_def_13 = ap(iPr_def_12,sK4),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_700,definition,
iPr_def_14 = ap(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_701,definition,
iPr_def_15 = ap(iPr_def_14,sK4),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_702,negated_conjecture,
ne(sK3),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_703,negated_conjecture,
mem(sK4,iPr_def_10),
inference(demodulation,[status(thm)],[c_91,c_696]) ).
tcf(c_704,negated_conjecture,
~ p(iPr_def_15),
inference(demodulation,[status(thm)],[c_90,c_698,c_699,c_697,c_700,c_701]) ).
tcf(c_1446,plain,
( mem(c_2Epred__set_2ECHOICE(sK3),arr(iPr_def_10,sK3))
| ~ ne(sK3) ),
inference(superposition,[status(thm)],[c_696,c_72]) ).
tcf(c_1448,plain,
mem(c_2Epred__set_2ECHOICE(sK3),arr(iPr_def_10,sK3)),
inference(forward_subsumption_resolution,[status(thm)],[c_1446,c_702]) ).
tcf(c_1534,plain,
( mem(c_2Epred__set_2EREST(sK3),arr(iPr_def_10,iPr_def_10))
| ~ ne(sK3) ),
inference(superposition,[status(thm)],[c_696,c_74]) ).
tcf(c_1538,plain,
( mem(iPr_def_12,arr(iPr_def_10,iPr_def_10))
| ~ ne(sK3) ),
inference(light_normalisation,[status(thm)],[c_1534,c_698]) ).
tcf(c_1539,plain,
mem(iPr_def_12,arr(iPr_def_10,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_1538,c_702]) ).
tcf(c_1568,plain,
! [X0: $i] :
( mem(ap(c_2Epred__set_2ECHOICE(sK3),X0),sK3)
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1448,c_52]) ).
tcf(c_1623,plain,
( mem(c_2Epred__set_2ESUBSET(sK3),arr(iPr_def_10,arr(iPr_def_10,bool)))
| ~ ne(sK3) ),
inference(superposition,[status(thm)],[c_696,c_63]) ).
tcf(c_1628,plain,
( mem(iPr_def_11,arr(iPr_def_10,arr(iPr_def_10,bool)))
| ~ ne(sK3) ),
inference(light_normalisation,[status(thm)],[c_1623,c_697]) ).
tcf(c_1629,plain,
mem(iPr_def_11,arr(iPr_def_10,arr(iPr_def_10,bool))),
inference(forward_subsumption_resolution,[status(thm)],[c_1628,c_702]) ).
tcf(c_1642,plain,
! [X0: $i] :
( mem(ap(iPr_def_12,X0),iPr_def_10)
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1539,c_52]) ).
tcf(c_1665,plain,
! [X0: $i] :
( mem(ap(iPr_def_11,X0),arr(iPr_def_10,bool))
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1629,c_52]) ).
tcf(c_1688,plain,
( mem(iPr_def_13,iPr_def_10)
| ~ mem(sK4,iPr_def_10) ),
inference(superposition,[status(thm)],[c_699,c_1642]) ).
tcf(c_1691,plain,
mem(iPr_def_13,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_1688,c_703]) ).
tcf(c_1861,plain,
( mem(iPr_def_14,arr(iPr_def_10,bool))
| ~ mem(iPr_def_13,iPr_def_10) ),
inference(superposition,[status(thm)],[c_700,c_1665]) ).
tcf(c_1865,plain,
mem(iPr_def_14,arr(iPr_def_10,bool)),
inference(forward_subsumption_resolution,[status(thm)],[c_1861,c_1691]) ).
tcf(c_1894,plain,
! [X0: $i] :
( mem(ap(iPr_def_14,X0),bool)
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1865,c_52]) ).
tcf(c_1939,plain,
( mem(iPr_def_15,bool)
| ~ mem(sK4,iPr_def_10) ),
inference(superposition,[status(thm)],[c_701,c_1894]) ).
tcf(c_1943,plain,
mem(iPr_def_15,bool),
inference(forward_subsumption_resolution,[status(thm)],[c_1939,c_703]) ).
tcf(c_1956,plain,
! [X0: $i] :
( p(iPr_def_15)
| p(X0)
| ( X0 = iPr_def_15 )
| ~ mem(X0,bool) ),
inference(superposition,[status(thm)],[c_1943,c_54]) ).
tcf(c_1959,plain,
! [X0: $i] :
( p(X0)
| ( X0 = iPr_def_15 )
| ~ mem(X0,bool) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1956,c_704]) ).
tcf(c_2139,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| ( ap(iPr_def_14,X0) = iPr_def_15 )
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1894,c_1959]) ).
tcf(c_2189,plain,
( p(iPr_def_15)
| ( ap(iPr_def_14,sK4) = iPr_def_15 )
| ~ mem(sK4,iPr_def_10) ),
inference(superposition,[status(thm)],[c_701,c_2139]) ).
tcf(c_2190,plain,
ap(iPr_def_14,sK4) = iPr_def_15,
inference(forward_subsumption_resolution,[status(thm)],[c_2189,c_704,c_703]) ).
tcf(c_3148,plain,
! [X0: $i] :
( ( ap(ap(c_2Epred__set_2EDELETE(sK3),X0),ap(c_2Epred__set_2ECHOICE(sK3),X0)) = ap(c_2Epred__set_2EREST(sK3),X0) )
| ~ ne(sK3)
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_696,c_89]) ).
tcf(c_3152,plain,
! [X0: $i] :
( ( ap(ap(c_2Epred__set_2EDELETE(sK3),X0),ap(c_2Epred__set_2ECHOICE(sK3),X0)) = ap(iPr_def_12,X0) )
| ~ ne(sK3)
| ~ mem(X0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_3148,c_698]) ).
tcf(c_3153,plain,
! [X0: $i] :
( ( ap(ap(c_2Epred__set_2EDELETE(sK3),X0),ap(c_2Epred__set_2ECHOICE(sK3),X0)) = ap(iPr_def_12,X0) )
| ~ mem(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3152,c_702]) ).
tcf(c_3338,plain,
ap(ap(c_2Epred__set_2EDELETE(sK3),sK4),ap(c_2Epred__set_2ECHOICE(sK3),sK4)) = ap(iPr_def_12,sK4),
inference(superposition,[status(thm)],[c_703,c_3153]) ).
tcf(c_3347,plain,
ap(ap(c_2Epred__set_2EDELETE(sK3),sK4),ap(c_2Epred__set_2ECHOICE(sK3),sK4)) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_3338,c_699]) ).
tcf(c_3506,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(iPr_def_11,X0),X1))
| mem(sK2(sK3,X0,X1),sK3)
| ~ ne(sK3)
| ~ mem(X1,arr(sK3,bool))
| ~ mem(X0,arr(sK3,bool)) ),
inference(superposition,[status(thm)],[c_697,c_84]) ).
tcf(c_3521,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(iPr_def_11,X0),X1))
| mem(sK2(sK3,X0,X1),sK3)
| ~ ne(sK3)
| ~ mem(X1,iPr_def_10)
| ~ mem(X0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_3506,c_696]) ).
tcf(c_3522,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(iPr_def_11,X0),X1))
| mem(sK2(sK3,X0,X1),sK3)
| ~ mem(X1,iPr_def_10)
| ~ mem(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3521,c_702]) ).
tcf(c_3788,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| mem(sK2(sK3,iPr_def_13,X0),sK3)
| ~ mem(iPr_def_13,iPr_def_10)
| ~ mem(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_700,c_3522]) ).
tcf(c_3790,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| mem(sK2(sK3,iPr_def_13,X0),sK3)
| ~ mem(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3788,c_1691]) ).
tcf(c_4344,plain,
! [X0: $i] :
( p(ap(ap(c_2Ebool_2EIN(sK3),X0),sK4))
| ~ ne(sK3)
| ~ mem(X0,sK3)
| ~ mem(sK4,arr(sK3,bool))
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ p(ap(ap(c_2Ebool_2EIN(sK3),X0),iPr_def_13)) ),
inference(superposition,[status(thm)],[c_3347,c_87]) ).
tcf(c_4346,plain,
! [X0: $i] :
( p(ap(ap(c_2Ebool_2EIN(sK3),X0),sK4))
| ~ ne(sK3)
| ~ mem(sK4,iPr_def_10)
| ~ mem(X0,sK3)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ p(ap(ap(c_2Ebool_2EIN(sK3),X0),iPr_def_13)) ),
inference(light_normalisation,[status(thm)],[c_4344,c_696]) ).
tcf(c_4347,plain,
! [X0: $i] :
( p(ap(ap(c_2Ebool_2EIN(sK3),X0),sK4))
| ~ mem(X0,sK3)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ p(ap(ap(c_2Ebool_2EIN(sK3),X0),iPr_def_13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4346,c_702,c_703]) ).
tcf(c_4671,plain,
! [X0: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(sK3),iPr_def_13),X0))
| p(ap(ap(c_2Ebool_2EIN(sK3),sK2(sK3,iPr_def_13,X0)),sK4))
| ~ ne(sK3)
| ~ mem(iPr_def_13,arr(sK3,bool))
| ~ mem(X0,arr(sK3,bool))
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ mem(sK2(sK3,iPr_def_13,X0),sK3) ),
inference(superposition,[status(thm)],[c_83,c_4347]) ).
tcf(c_4679,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| p(ap(ap(c_2Ebool_2EIN(sK3),sK2(sK3,iPr_def_13,X0)),sK4))
| ~ ne(sK3)
| ~ mem(iPr_def_13,iPr_def_10)
| ~ mem(X0,iPr_def_10)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ mem(sK2(sK3,iPr_def_13,X0),sK3) ),
inference(light_normalisation,[status(thm)],[c_4671,c_696,c_697,c_700]) ).
tcf(c_4680,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| p(ap(ap(c_2Ebool_2EIN(sK3),sK2(sK3,iPr_def_13,X0)),sK4))
| ~ mem(X0,iPr_def_10)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3)
| ~ mem(sK2(sK3,iPr_def_13,X0),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4679,c_702,c_1691]) ).
tcf(c_4745,plain,
! [X0: $i] :
( p(ap(iPr_def_14,X0))
| p(ap(ap(c_2Ebool_2EIN(sK3),sK2(sK3,iPr_def_13,X0)),sK4))
| ~ mem(X0,iPr_def_10)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3) ),
inference(global_subsumption_just,[status(thm)],[c_4680,c_3790,c_4680]) ).
tcf(c_4756,plain,
( p(ap(iPr_def_14,sK4))
| p(ap(ap(c_2Epred__set_2ESUBSET(sK3),iPr_def_13),sK4))
| ~ ne(sK3)
| ~ mem(sK4,iPr_def_10)
| ~ mem(iPr_def_13,arr(sK3,bool))
| ~ mem(sK4,arr(sK3,bool))
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3) ),
inference(superposition,[status(thm)],[c_4745,c_82]) ).
tcf(c_4757,plain,
( p(iPr_def_15)
| ~ ne(sK3)
| ~ mem(iPr_def_13,iPr_def_10)
| ~ mem(sK4,iPr_def_10)
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3) ),
inference(light_normalisation,[status(thm)],[c_4756,c_696,c_697,c_700,c_2190]) ).
tcf(c_4758,plain,
~ mem(ap(c_2Epred__set_2ECHOICE(sK3),sK4),sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4757,c_704,c_702,c_1691,c_703]) ).
tcf(c_4760,plain,
~ mem(sK4,iPr_def_10),
inference(superposition,[status(thm)],[c_1568,c_4758]) ).
tcf(c_4761,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4760,c_703]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 % Computer : n005.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Wed Sep 23 17:28:32 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.46 Running first-order theorem proving
% 0.14/0.46 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.48
% 0.14/0.48 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.48
% 0.14/0.48 % Detected problem language: tptp
% 0.21/0.49 % Proving...
% 3.94/1.39 % SZS status Started for theBenchmark.p
% 3.94/1.39 % SZS status Theorem for theBenchmark.p
% 3.94/1.39
% 3.94/1.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.94/1.39
% 3.94/1.39 % ------ iProver source info
% 3.94/1.39
% 3.94/1.39 % git: date: 2026-07-19 20:42:38 +0200
% 3.94/1.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.94/1.39 % git: non_committed_changes: false
% 3.94/1.39
% 3.94/1.39 % ------ Parsing...
% 3.94/1.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.94/1.39
% 3.94/1.39 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 3.94/1.39
% 3.94/1.39 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.94/1.39
% 3.94/1.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.94/1.39 % ------ Proving...
% 3.94/1.39 % ------ Problem Properties
% 3.94/1.39
% 3.94/1.39 %
% 3.94/1.39 % clauses 50
% 3.94/1.39 % conjectures 3
% 3.94/1.39 % EPR 7
% 3.94/1.39 % Horn 42
% 3.94/1.39 % unary 14
% 3.94/1.39 % binary 9
% 3.94/1.39 % lits 151
% 3.94/1.39 % lits eq 16
% 3.94/1.39 % fd_pure 0
% 3.94/1.39 % fd_pseudo 0
% 3.94/1.39 % fd_cond 0
% 3.94/1.39 % fd_pseudo_cond 6
% 3.94/1.39 % AC symbols 0
% 3.94/1.39
% 3.94/1.39 % ------ Schedule dynamic 5 is on
% 3.94/1.39
% 3.94/1.39 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.94/1.39
% 3.94/1.39
% 3.94/1.39 % ------
% 3.94/1.39 % Current options:
% 3.94/1.39 % ------
% 3.94/1.39
% 3.94/1.39
% 3.94/1.39 %
% 3.94/1.39
% 3.94/1.39 % ------ Proving...
% 3.94/1.39 %
% 3.94/1.39
% 3.94/1.39 % SZS status Theorem for theBenchmark.p
% 3.94/1.39
% 3.94/1.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.94/1.39
% 3.94/1.39
%------------------------------------------------------------------------------