%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n001.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 02:55:56 PM UTC 2026
% Result : Theorem 31.37s 5.30s
% Output : CNFRefutation 31.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 97 ( 31 unt; 5 def)
% Number of atoms : 420 ( 74 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 433 ( 179 ~; 184 |; 44 &)
% ( 9 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 124 ( 0 sgn 118 !; 6 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X0] :
( ( function(X0)
& relation(X0) )
=> ! [X1,X2] :
( ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) )
& ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f60,axiom,
! [X0,X1] :
( ( relation(X1)
& relation(X0) )
=> relation(relation_composition(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_relat_1) ).
fof(f73,axiom,
! [X0,X1] :
( ( function(X1)
& relation(X1)
& function(X0)
& relation(X0) )
=> ( function(relation_composition(X0,X1))
& relation(relation_composition(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_funct_1) ).
fof(f149,axiom,
! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(apply(X2,X0),relation_dom(X1))
& in(X0,relation_dom(X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_funct_1) ).
fof(f151,axiom,
! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
=> apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_funct_1) ).
fof(f152,conjecture,
! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( in(X0,relation_dom(X1))
=> apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_funct_1) ).
fof(f153,negated_conjecture,
~ ! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( in(X0,relation_dom(X1))
=> apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f152]) ).
fof(f200,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f220,axiom,
! [X0,X1,X2] :
( singleton(X0) = unordered_pair(X1,X2)
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_zfmisc_1) ).
fof(f249,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ! [X1,X2] :
( ( in(X1,relation_dom(X0))
| ( X2 = apply(X0,X1)
<=> X2 = empty_set ) )
& ( ~ in(X1,relation_dom(X0))
| ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) ) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f250,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ! [X1,X2] :
( ( in(X1,relation_dom(X0))
| ( X2 = apply(X0,X1)
<=> X2 = empty_set ) )
& ( ~ in(X1,relation_dom(X0))
| ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) ) ) ),
inference(flattening,[],[f249]) ).
fof(f262,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f263,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(flattening,[],[f262]) ).
fof(f273,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| ( function(relation_composition(X0,X1))
& relation(relation_composition(X0,X1)) ) ),
inference(ennf_transformation,[],[f73]) ).
fof(f274,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| ( function(relation_composition(X0,X1))
& relation(relation_composition(X0,X1)) ) ),
inference(flattening,[],[f273]) ).
fof(f339,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(apply(X2,X0),relation_dom(X1))
& in(X0,relation_dom(X2)) ) ) ) ),
inference(ennf_transformation,[],[f149]) ).
fof(f340,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(apply(X2,X0),relation_dom(X1))
& in(X0,relation_dom(X2)) ) ) ) ),
inference(flattening,[],[f339]) ).
fof(f342,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ) ),
inference(ennf_transformation,[],[f151]) ).
fof(f343,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ) ),
inference(flattening,[],[f342]) ).
fof(f344,plain,
? [X0,X1] :
( function(X1)
& relation(X1)
& ? [X2] :
( function(X2)
& relation(X2)
& in(X0,relation_dom(X1))
& apply(relation_composition(X1,X2),X0) != apply(X2,apply(X1,X0)) ) ),
inference(ennf_transformation,[],[f153]) ).
fof(f345,plain,
? [X0,X1] :
( function(X1)
& relation(X1)
& ? [X2] :
( function(X2)
& relation(X2)
& in(X0,relation_dom(X1))
& apply(relation_composition(X1,X2),X0) != apply(X2,apply(X1,X0)) ) ),
inference(flattening,[],[f344]) ).
fof(f409,plain,
! [X0,X1,X2] :
( singleton(X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(ennf_transformation,[],[f220]) ).
fof(f470,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ! [X1,X2] :
( ( in(X1,relation_dom(X0))
| ( ( apply(X0,X1) != X2
| X2 = empty_set )
& ( empty_set != X2
| X2 = apply(X0,X1) ) ) )
& ( ~ in(X1,relation_dom(X0))
| ( ( apply(X0,X1) != X2
| in(ordered_pair(X1,X2),X0) )
& ( ~ in(ordered_pair(X1,X2),X0)
| X2 = apply(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f250]) ).
fof(f522,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ( ( ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ( in(apply(X2,X0),relation_dom(X1))
& in(X0,relation_dom(X2)) ) )
& ( ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(X2))
| in(X0,relation_dom(relation_composition(X2,X1))) ) ) ) ),
inference(nnf_transformation,[],[f340]) ).
fof(f523,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ( ( ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ( in(apply(X2,X0),relation_dom(X1))
& in(X0,relation_dom(X2)) ) )
& ( ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(X2))
| in(X0,relation_dom(relation_composition(X2,X1))) ) ) ) ),
inference(flattening,[],[f522]) ).
fof(f524,plain,
( function(sK65)
& relation(sK65)
& function(sK66)
& relation(sK66)
& in(sK64,relation_dom(sK65))
& apply(relation_composition(sK65,sK66),sK64) != apply(sK66,apply(sK65,sK64)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X2,sK66)],[f345]) ).
fof(f649,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| in(X1,relation_dom(X0))
| apply(X0,X1) != X2
| empty_set = X2 ),
inference(cnf_transformation,[],[f470]) ).
fof(f698,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f263]) ).
fof(f711,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| function(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f274]) ).
fof(f818,plain,
! [X2,X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| in(apply(X2,X0),relation_dom(X1)) ),
inference(cnf_transformation,[],[f523]) ).
fof(f820,plain,
! [X2,X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(X2))
| in(X0,relation_dom(relation_composition(X2,X1))) ),
inference(cnf_transformation,[],[f523]) ).
fof(f822,plain,
! [X2,X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ),
inference(cnf_transformation,[],[f343]) ).
fof(f823,plain,
function(sK65),
inference(cnf_transformation,[],[f524]) ).
fof(f824,plain,
relation(sK65),
inference(cnf_transformation,[],[f524]) ).
fof(f825,plain,
function(sK66),
inference(cnf_transformation,[],[f524]) ).
fof(f826,plain,
relation(sK66),
inference(cnf_transformation,[],[f524]) ).
fof(f827,plain,
in(sK64,relation_dom(sK65)),
inference(cnf_transformation,[],[f524]) ).
fof(f828,plain,
apply(relation_composition(sK65,sK66),sK64) != apply(sK66,apply(sK65,sK64)),
inference(cnf_transformation,[],[f524]) ).
fof(f895,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f200]) ).
fof(f926,plain,
! [X2,X0,X1] :
( singleton(X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f409]) ).
fof(f1058,plain,
! [X2,X0,X1] :
( unordered_pair(X0,X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(definition_unfolding,[],[f926,f895]) ).
fof(f1110,plain,
! [X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| in(X1,relation_dom(X0))
| empty_set = apply(X0,X1) ),
inference(equality_resolution,[],[f649]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( in(X1,relation_dom(X0))
| ( apply(X0,X1) = empty_set )
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f1110]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i] :
( relation(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f698]) ).
tcf(c_212,plain,
! [X0: $i,X1: $i] :
( function(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X1)
| ~ function(X0) ),
inference(cnf_transformation,[],[f711]) ).
tcf(c_318,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X1,relation_dom(relation_composition(X0,X2)))
| ~ relation(X2)
| ~ relation(X0)
| ~ function(X2)
| ~ function(X0)
| ~ in(X1,relation_dom(X0))
| ~ in(apply(X0,X1),relation_dom(X2)) ),
inference(cnf_transformation,[],[f820]) ).
tcf(c_320,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(apply(X1,X0),relation_dom(X2))
| ~ relation(X2)
| ~ relation(X1)
| ~ function(X2)
| ~ function(X1)
| ~ in(X0,relation_dom(relation_composition(X1,X2))) ),
inference(cnf_transformation,[],[f818]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) )
| ~ relation(X2)
| ~ relation(X1)
| ~ function(X2)
| ~ function(X1)
| ~ in(X0,relation_dom(relation_composition(X1,X2))) ),
inference(cnf_transformation,[],[f822]) ).
tcf(c_323,negated_conjecture,
apply(relation_composition(sK65,sK66),sK64) != apply(sK66,apply(sK65,sK64)),
inference(cnf_transformation,[],[f828]) ).
tcf(c_324,negated_conjecture,
in(sK64,relation_dom(sK65)),
inference(cnf_transformation,[],[f827]) ).
tcf(c_325,negated_conjecture,
relation(sK66),
inference(cnf_transformation,[],[f826]) ).
tcf(c_326,negated_conjecture,
function(sK66),
inference(cnf_transformation,[],[f825]) ).
tcf(c_327,negated_conjecture,
relation(sK65),
inference(cnf_transformation,[],[f824]) ).
tcf(c_328,negated_conjecture,
function(sK65),
inference(cnf_transformation,[],[f823]) ).
tcf(c_424,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( unordered_pair(X0,X0) != unordered_pair(X1,X2) ) ),
inference(cnf_transformation,[],[f1058]) ).
tcf(c_9692,definition,
iPr_def_10 = relation_dom(sK65),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_9693,definition,
iPr_def_11 = relation_composition(sK65,sK66),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_9694,definition,
iPr_def_12 = apply(iPr_def_11,sK64),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_9695,definition,
iPr_def_13 = apply(sK65,sK64),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_9696,definition,
iPr_def_14 = apply(sK66,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_9697,negated_conjecture,
function(sK65),
inference(demodulation,[status(thm)],[c_328]) ).
tcf(c_9698,negated_conjecture,
relation(sK65),
inference(demodulation,[status(thm)],[c_327]) ).
tcf(c_9699,negated_conjecture,
function(sK66),
inference(demodulation,[status(thm)],[c_326]) ).
tcf(c_9700,negated_conjecture,
relation(sK66),
inference(demodulation,[status(thm)],[c_325]) ).
tcf(c_9701,negated_conjecture,
in(sK64,iPr_def_10),
inference(demodulation,[status(thm)],[c_324,c_9692]) ).
tcf(c_9702,negated_conjecture,
iPr_def_12 != iPr_def_14,
inference(demodulation,[status(thm)],[c_323,c_9695,c_9696,c_9693,c_9694]) ).
tcf(c_9710,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( unordered_pair(X0,X2) = unordered_pair(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_17557,plain,
( relation(iPr_def_11)
| ~ relation(sK66)
| ~ relation(sK65) ),
inference(superposition,[status(thm)],[c_9693,c_198]) ).
tcf(c_17559,plain,
relation(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_17557,c_9700,c_9698]) ).
tcf(c_19193,plain,
! [X0: $i] :
( ( iPr_def_12 = iPr_def_14 )
| ( unordered_pair(X0,X0) != unordered_pair(iPr_def_12,iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_424]) ).
tcf(c_19194,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( unordered_pair(empty_set,empty_set) != unordered_pair(iPr_def_12,iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_19193]) ).
tcf(c_25910,plain,
! [X0: $i] :
( ( unordered_pair(X0,X0) = unordered_pair(iPr_def_12,iPr_def_14) )
| ( X0 != iPr_def_14 )
| ( X0 != iPr_def_12 ) ),
inference(instantiation,[status(thm)],[c_9710]) ).
tcf(c_25911,plain,
( ( unordered_pair(empty_set,empty_set) = unordered_pair(iPr_def_12,iPr_def_14) )
| ( empty_set != iPr_def_14 )
| ( empty_set != iPr_def_12 ) ),
inference(instantiation,[status(thm)],[c_25910]) ).
tcf(c_38973,plain,
( function(iPr_def_11)
| ~ relation(sK66)
| ~ relation(sK65)
| ~ function(sK66)
| ~ function(sK65) ),
inference(superposition,[status(thm)],[c_9693,c_212]) ).
tcf(c_38979,plain,
function(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_38973,c_9700,c_9698,c_9699,c_9697]) ).
tcf(c_59115,plain,
! [X0: $i] :
( in(apply(sK65,X0),relation_dom(sK66))
| ~ relation(sK66)
| ~ relation(sK65)
| ~ function(sK66)
| ~ function(sK65)
| ~ in(X0,relation_dom(iPr_def_11)) ),
inference(superposition,[status(thm)],[c_9693,c_320]) ).
tcf(c_59124,plain,
! [X0: $i] :
( in(apply(sK65,X0),relation_dom(sK66))
| ~ in(X0,relation_dom(iPr_def_11)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_59115,c_9700,c_9698,c_9699,c_9697]) ).
tcf(c_59865,plain,
( in(iPr_def_13,relation_dom(sK66))
| ~ in(sK64,relation_dom(iPr_def_11)) ),
inference(superposition,[status(thm)],[c_9695,c_59124]) ).
tcf(c_61756,plain,
( in(iPr_def_13,relation_dom(sK66))
| ( apply(iPr_def_11,sK64) = empty_set )
| ~ relation(iPr_def_11)
| ~ function(iPr_def_11) ),
inference(superposition,[status(thm)],[c_153,c_59865]) ).
tcf(c_61759,plain,
( in(iPr_def_13,relation_dom(sK66))
| ( empty_set = iPr_def_12 )
| ~ relation(iPr_def_11)
| ~ function(iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_61756,c_9694]) ).
tcf(c_61760,plain,
( in(iPr_def_13,relation_dom(sK66))
| ( empty_set = iPr_def_12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_61759,c_17559,c_38979]) ).
tcf(c_66195,plain,
! [X0: $i] :
( in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(X0)
| ~ function(X0)
| ~ in(sK64,relation_dom(sK65))
| ~ in(iPr_def_13,relation_dom(X0)) ),
inference(superposition,[status(thm)],[c_9695,c_318]) ).
tcf(c_66270,plain,
! [X0: $i] :
( in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(X0)
| ~ function(X0)
| ~ in(sK64,iPr_def_10)
| ~ in(iPr_def_13,relation_dom(X0)) ),
inference(light_normalisation,[status(thm)],[c_66195,c_9692]) ).
tcf(c_66271,plain,
! [X0: $i] :
( in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(X0)
| ~ function(X0)
| ~ in(iPr_def_13,relation_dom(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_66270,c_9698,c_9697,c_9701]) ).
tcf(c_67254,plain,
( in(sK64,relation_dom(iPr_def_11))
| ~ relation(sK66)
| ~ function(sK66)
| ~ in(iPr_def_13,relation_dom(sK66)) ),
inference(superposition,[status(thm)],[c_9693,c_66271]) ).
tcf(c_67266,plain,
( in(sK64,relation_dom(iPr_def_11))
| ~ in(iPr_def_13,relation_dom(sK66)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_67254,c_9700,c_9699]) ).
tcf(c_67325,plain,
( in(sK64,relation_dom(iPr_def_11))
| ( apply(sK66,iPr_def_13) = empty_set )
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[status(thm)],[c_153,c_67266]) ).
tcf(c_67326,plain,
( in(sK64,relation_dom(iPr_def_11))
| ( empty_set = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_61760,c_67266]) ).
tcf(c_67331,plain,
( in(sK64,relation_dom(iPr_def_11))
| ( empty_set = iPr_def_14 )
| ~ relation(sK66)
| ~ function(sK66) ),
inference(light_normalisation,[status(thm)],[c_67325,c_9696]) ).
tcf(c_67332,plain,
( in(sK64,relation_dom(iPr_def_11))
| ( empty_set = iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_67331,c_9700,c_9699]) ).
tcf(c_67376,plain,
in(sK64,relation_dom(iPr_def_11)),
inference(global_subsumption_just,[status(thm)],[c_67332,c_9702,c_19194,c_25911,c_67332,c_67326]) ).
tcf(c_68171,plain,
! [X0: $i] :
( ( apply(relation_composition(sK65,sK66),X0) = apply(sK66,apply(sK65,X0)) )
| ~ relation(sK66)
| ~ relation(sK65)
| ~ function(sK66)
| ~ function(sK65)
| ~ in(X0,relation_dom(iPr_def_11)) ),
inference(superposition,[status(thm)],[c_9693,c_322]) ).
tcf(c_68182,plain,
! [X0: $i] :
( ( apply(sK66,apply(sK65,X0)) = apply(iPr_def_11,X0) )
| ~ relation(sK66)
| ~ relation(sK65)
| ~ function(sK66)
| ~ function(sK65)
| ~ in(X0,relation_dom(iPr_def_11)) ),
inference(light_normalisation,[status(thm)],[c_68171,c_9693]) ).
tcf(c_68183,plain,
! [X0: $i] :
( ( apply(sK66,apply(sK65,X0)) = apply(iPr_def_11,X0) )
| ~ in(X0,relation_dom(iPr_def_11)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_68182,c_9700,c_9698,c_9699,c_9697]) ).
tcf(c_69793,plain,
apply(sK66,apply(sK65,sK64)) = apply(iPr_def_11,sK64),
inference(superposition,[status(thm)],[c_67376,c_68183]) ).
tcf(c_69796,plain,
iPr_def_12 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_69793,c_9694,c_9695,c_9696]) ).
tcf(c_69797,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_69796,c_9702]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.38 % Computer : n001.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Thu Sep 24 13:18:39 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.42 Running first-order theorem proving
% 0.09/0.42 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.09/0.43
% 0.09/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.43
% 0.09/0.43 % Detected problem language: tptp
% 0.09/0.45 % Proving...
% 31.37/5.30 % SZS status Started for theBenchmark.p
% 31.37/5.30 % SZS status Theorem for theBenchmark.p
% 31.37/5.30
% 31.37/5.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.37/5.30
% 31.37/5.30 % ------ iProver source info
% 31.37/5.30
% 31.37/5.30 % git: date: 2026-07-19 20:42:38 +0200
% 31.37/5.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.37/5.30 % git: non_committed_changes: false
% 31.37/5.30
% 31.37/5.30 % ------ Parsing...
% 31.37/5.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.37/5.30
% 31.37/5.30 % ------ Preprocessing... sup_sim: 41 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 31.37/5.30
% 31.37/5.30 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 31.37/5.30
% 31.37/5.30 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 31.37/5.30 % ------ Proving...
% 31.37/5.30 % ------ Problem Properties
% 31.37/5.30
% 31.37/5.30 %
% 31.37/5.30 % clauses 337
% 31.37/5.30 % conjectures 6
% 31.37/5.30 % EPR 43
% 31.37/5.30 % Horn 273
% 31.37/5.30 % unary 58
% 31.37/5.30 % binary 107
% 31.37/5.30 % lits 895
% 31.37/5.30 % lits eq 176
% 31.37/5.30 % fd_pure 0
% 31.37/5.30 % fd_pseudo 0
% 31.37/5.30 % fd_cond 14
% 31.37/5.30 % fd_pseudo_cond 69
% 31.37/5.30 % AC symbols 0
% 31.37/5.30
% 31.37/5.30 % ------ Schedule dynamic 5 is on
% 31.37/5.30
% 31.37/5.30 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 31.37/5.30
% 31.37/5.30
% 31.37/5.30 % ------
% 31.37/5.30 % Current options:
% 31.37/5.30 % ------
% 31.37/5.30
% 31.37/5.30
% 31.37/5.30 %
% 31.37/5.30
% 31.37/5.30 % ------ Proving...
% 31.37/5.30 %
% 31.37/5.30
% 31.37/5.30 % SZS status Theorem for theBenchmark.p
% 31.37/5.30
% 31.37/5.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.37/5.31
% 31.37/5.31
%------------------------------------------------------------------------------