%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU214+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 : n011.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 48.91s 28.84s
% Output : CNFRefutation 48.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 76 ( 18 unt; 0 def)
% Number of atoms : 368 ( 35 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 503 ( 211 ~; 208 |; 60 &)
% ( 10 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-4 aty)
% Number of variables : 176 ( 0 sgn 160 !; 16 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f38,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( relation(X2)
=> ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X5,X4),X1)
& in(ordered_pair(X3,X5),X0) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_relat_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,conjecture,
! [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,negated_conjecture,
~ ! [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(negated_conjecture,[status(cth)],[f151]) ).
fof(f199,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f210,axiom,
! [X0,X1,X2] :
( ( function(X2)
& relation(X2) )
=> ( in(ordered_pair(X0,X1),X2)
<=> ( X1 = apply(X2,X0)
& in(X0,relation_dom(X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f255,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ relation(X2)
| ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X5,X4),X1)
& in(ordered_pair(X3,X5),X0) ) ) ) ) ) ),
inference(ennf_transformation,[],[f38]) ).
fof(f261,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f262,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(flattening,[],[f261]) ).
fof(f272,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(f273,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| ( function(relation_composition(X0,X1))
& relation(relation_composition(X0,X1)) ) ),
inference(flattening,[],[f272]) ).
fof(f338,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(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(flattening,[],[f338]) ).
fof(f341,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,[],[f152]) ).
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(flattening,[],[f341]) ).
fof(f395,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ( in(ordered_pair(X0,X1),X2)
<=> ( X1 = apply(X2,X0)
& in(X0,relation_dom(X2)) ) ) ),
inference(ennf_transformation,[],[f210]) ).
fof(f396,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ( in(ordered_pair(X0,X1),X2)
<=> ( X1 = apply(X2,X0)
& in(X0,relation_dom(X2)) ) ) ),
inference(flattening,[],[f395]) ).
fof(f485,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ relation(X2)
| ( ( relation_composition(X0,X1) != X2
| ! [X3,X4] :
( ( ~ in(ordered_pair(X3,X4),X2)
| ? [X5] :
( in(ordered_pair(X5,X4),X1)
& in(ordered_pair(X3,X5),X0) ) )
& ( ! [X5] :
( ~ in(ordered_pair(X5,X4),X1)
| ~ in(ordered_pair(X3,X5),X0) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ? [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ? [X5] :
( in(ordered_pair(X5,X4),X1)
& in(ordered_pair(X3,X5),X0) ) )
& ( ~ in(ordered_pair(X3,X4),X2)
| ! [X5] :
( ~ in(ordered_pair(X5,X4),X1)
| ~ in(ordered_pair(X3,X5),X0) ) ) )
| X2 = relation_composition(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f255]) ).
fof(f486,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ relation(X2)
| ( ( relation_composition(X0,X1) != X2
| ! [X7,X8] :
( ( ~ in(ordered_pair(X7,X8),X2)
| ? [X10] :
( in(ordered_pair(X10,X8),X1)
& in(ordered_pair(X7,X10),X0) ) )
& ( ! [X9] :
( ~ in(ordered_pair(X9,X8),X1)
| ~ in(ordered_pair(X7,X9),X0) )
| in(ordered_pair(X7,X8),X2) ) ) )
& ( ? [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ? [X6] :
( in(ordered_pair(X6,X4),X1)
& in(ordered_pair(X3,X6),X0) ) )
& ( ~ in(ordered_pair(X3,X4),X2)
| ! [X5] :
( ~ in(ordered_pair(X5,X4),X1)
| ~ in(ordered_pair(X3,X5),X0) ) ) )
| X2 = relation_composition(X0,X1) ) ) ) ) ),
inference(rectify,[],[f485]) ).
fof(f487,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ relation(X2)
| ( ( relation_composition(X0,X1) != X2
| ! [X7,X8] :
( ( ~ in(ordered_pair(X7,X8),X2)
| ( in(ordered_pair(sK49(X0,X1,X7,X8),X8),X1)
& in(ordered_pair(X7,sK49(X0,X1,X7,X8)),X0) ) )
& ( ! [X9] :
( ~ in(ordered_pair(X9,X8),X1)
| ~ in(ordered_pair(X7,X9),X0) )
| in(ordered_pair(X7,X8),X2) ) ) )
& ( ( ( in(ordered_pair(sK46(X0,X1,X2),sK47(X0,X1,X2)),X2)
| ( in(ordered_pair(sK48(X0,X1,X2),sK47(X0,X1,X2)),X1)
& in(ordered_pair(sK46(X0,X1,X2),sK48(X0,X1,X2)),X0) ) )
& ( ~ in(ordered_pair(sK46(X0,X1,X2),sK47(X0,X1,X2)),X2)
| ! [X5] :
( ~ in(ordered_pair(X5,sK47(X0,X1,X2)),X1)
| ~ in(ordered_pair(sK46(X0,X1,X2),X5),X0) ) ) )
| X2 = relation_composition(X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48,sK49]),skolemize(X3,sK46(X0,X1,X2)),skolemize(X4,sK47(X0,X1,X2)),skolemize(X6,sK48(X0,X1,X2)),skolemize(X10,sK49(X0,X1,X7,X8))],[f486]) ).
fof(f519,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,[],[f339]) ).
fof(f520,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,[],[f519]) ).
fof(f521,plain,
( function(sK65)
& relation(sK65)
& function(sK66)
& relation(sK66)
& in(sK64,relation_dom(relation_composition(sK66,sK65)))
& apply(relation_composition(sK66,sK65),sK64) != apply(sK65,apply(sK66,sK64)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X2,sK66)],[f342]) ).
fof(f542,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ( ( ~ in(ordered_pair(X0,X1),X2)
| ( X1 = apply(X2,X0)
& in(X0,relation_dom(X2)) ) )
& ( apply(X2,X0) != X1
| ~ in(X0,relation_dom(X2))
| in(ordered_pair(X0,X1),X2) ) ) ),
inference(nnf_transformation,[],[f396]) ).
fof(f543,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ( ( ~ in(ordered_pair(X0,X1),X2)
| ( X1 = apply(X2,X0)
& in(X0,relation_dom(X2)) ) )
& ( apply(X2,X0) != X1
| ~ in(X0,relation_dom(X2))
| in(ordered_pair(X0,X1),X2) ) ) ),
inference(flattening,[],[f542]) ).
fof(f672,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f34]) ).
fof(f682,plain,
! [X2,X0,X1,X8,X9,X7] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| relation_composition(X0,X1) != X2
| ~ in(ordered_pair(X9,X8),X1)
| ~ in(ordered_pair(X7,X9),X0)
| in(ordered_pair(X7,X8),X2) ),
inference(cnf_transformation,[],[f487]) ).
fof(f695,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f262]) ).
fof(f708,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| function(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f273]) ).
fof(f709,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f273]) ).
fof(f815,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,[],[f520]) ).
fof(f816,plain,
! [X2,X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| in(X0,relation_dom(X2)) ),
inference(cnf_transformation,[],[f520]) ).
fof(f819,plain,
function(sK65),
inference(cnf_transformation,[],[f521]) ).
fof(f820,plain,
relation(sK65),
inference(cnf_transformation,[],[f521]) ).
fof(f821,plain,
function(sK66),
inference(cnf_transformation,[],[f521]) ).
fof(f822,plain,
relation(sK66),
inference(cnf_transformation,[],[f521]) ).
fof(f823,plain,
in(sK64,relation_dom(relation_composition(sK66,sK65))),
inference(cnf_transformation,[],[f521]) ).
fof(f824,plain,
apply(relation_composition(sK66,sK65),sK64) != apply(sK65,apply(sK66,sK64)),
inference(cnf_transformation,[],[f521]) ).
fof(f891,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f199]) ).
fof(f908,plain,
! [X2,X0,X1] :
( ~ function(X2)
| ~ relation(X2)
| ~ in(ordered_pair(X0,X1),X2)
| apply(X2,X0) = X1 ),
inference(cnf_transformation,[],[f543]) ).
fof(f910,plain,
! [X2,X0,X1] :
( ~ function(X2)
| ~ relation(X2)
| apply(X2,X0) != X1
| ~ in(X0,relation_dom(X2))
| in(ordered_pair(X0,X1),X2) ),
inference(cnf_transformation,[],[f543]) ).
fof(f923,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f672,f891]) ).
fof(f993,plain,
! [X2,X0,X1,X8,X9,X7] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| relation_composition(X0,X1) != X2
| ~ in(unordered_pair(unordered_pair(X9,X8),unordered_pair(X9,X9)),X1)
| ~ in(unordered_pair(unordered_pair(X7,X9),unordered_pair(X7,X7)),X0)
| in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),X2) ),
inference(definition_unfolding,[],[f682,f923,f923,f923]) ).
fof(f1049,plain,
! [X2,X0,X1] :
( ~ function(X2)
| ~ relation(X2)
| apply(X2,X0) != X1
| ~ in(X0,relation_dom(X2))
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2) ),
inference(definition_unfolding,[],[f910,f923]) ).
fof(f1051,plain,
! [X2,X0,X1] :
( ~ function(X2)
| ~ relation(X2)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| apply(X2,X0) = X1 ),
inference(definition_unfolding,[],[f908,f923]) ).
fof(f1119,plain,
! [X0,X1,X8,X9,X7] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(relation_composition(X0,X1))
| ~ in(unordered_pair(unordered_pair(X9,X8),unordered_pair(X9,X9)),X1)
| ~ in(unordered_pair(unordered_pair(X7,X9),unordered_pair(X7,X7)),X0)
| in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1)) ),
inference(equality_resolution,[],[f993]) ).
fof(f1128,plain,
! [X2,X0] :
( ~ function(X2)
| ~ relation(X2)
| ~ in(X0,relation_dom(X2))
| in(unordered_pair(unordered_pair(X0,apply(X2,X0)),unordered_pair(X0,X0)),X2) ),
inference(equality_resolution,[],[f1049]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( in(unordered_pair(unordered_pair(X0,X3),unordered_pair(X0,X0)),relation_composition(X2,X4))
| ~ relation(X4)
| ~ relation(X2)
| ~ relation(relation_composition(X2,X4))
| ~ in(unordered_pair(unordered_pair(X1,X3),unordered_pair(X1,X1)),X4)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2) ),
inference(cnf_transformation,[],[f1119]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i] :
( relation(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f695]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i] :
( relation(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X1)
| ~ function(X0) ),
inference(cnf_transformation,[],[f709]) ).
tcf(c_212,plain,
! [X0: $i,X1: $i] :
( function(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X1)
| ~ function(X0) ),
inference(cnf_transformation,[],[f708]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,relation_dom(X1))
| ~ relation(X2)
| ~ relation(X1)
| ~ function(X2)
| ~ function(X1)
| ~ in(X0,relation_dom(relation_composition(X1,X2))) ),
inference(cnf_transformation,[],[f816]) ).
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,[],[f815]) ).
tcf(c_322,negated_conjecture,
apply(relation_composition(sK66,sK65),sK64) != apply(sK65,apply(sK66,sK64)),
inference(cnf_transformation,[],[f824]) ).
tcf(c_323,negated_conjecture,
in(sK64,relation_dom(relation_composition(sK66,sK65))),
inference(cnf_transformation,[],[f823]) ).
tcf(c_324,negated_conjecture,
relation(sK66),
inference(cnf_transformation,[],[f822]) ).
tcf(c_325,negated_conjecture,
function(sK66),
inference(cnf_transformation,[],[f821]) ).
tcf(c_326,negated_conjecture,
relation(sK65),
inference(cnf_transformation,[],[f820]) ).
tcf(c_327,negated_conjecture,
function(sK65),
inference(cnf_transformation,[],[f819]) ).
tcf(c_409,plain,
! [X0: $i,X1: $i] :
( in(unordered_pair(unordered_pair(X0,apply(X1,X0)),unordered_pair(X0,X0)),X1)
| ~ relation(X1)
| ~ function(X1)
| ~ in(X0,relation_dom(X1)) ),
inference(cnf_transformation,[],[f1128]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( apply(X2,X0) = X1 )
| ~ relation(X2)
| ~ function(X2)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2) ),
inference(cnf_transformation,[],[f1051]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i] :
( relation(relation_composition(X1,X0))
| ~ relation(X1)
| ~ relation(X0) ),
inference(global_subsumption_just,[status(thm)],[c_211,c_198]) ).
tcf(c_1294,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( in(unordered_pair(unordered_pair(X0,X3),unordered_pair(X0,X0)),relation_composition(X2,X4))
| ~ relation(X4)
| ~ relation(X2)
| ~ in(unordered_pair(unordered_pair(X1,X3),unordered_pair(X1,X1)),X4)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_186,c_641]) ).
tcf(c_6246,plain,
( in(apply(sK66,sK64),relation_dom(sK65))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ function(sK65)
| ~ function(sK66)
| ~ in(sK64,relation_dom(relation_composition(sK66,sK65))) ),
inference(instantiation,[status(thm)],[c_320]) ).
tcf(c_6247,plain,
( in(sK64,relation_dom(sK66))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ function(sK65)
| ~ function(sK66)
| ~ in(sK64,relation_dom(relation_composition(sK66,sK65))) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_6296,plain,
( ( apply(relation_composition(sK66,sK65),sK64) = apply(sK65,apply(sK66,sK64)) )
| ~ relation(relation_composition(sK66,sK65))
| ~ function(relation_composition(sK66,sK65))
| ~ in(unordered_pair(unordered_pair(sK64,apply(sK65,apply(sK66,sK64))),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65)) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_7849,plain,
( in(unordered_pair(unordered_pair(apply(sK66,sK64),apply(sK65,apply(sK66,sK64))),unordered_pair(apply(sK66,sK64),apply(sK66,sK64))),sK65)
| ~ relation(sK65)
| ~ function(sK65)
| ~ in(apply(sK66,sK64),relation_dom(sK65)) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_7890,plain,
( in(unordered_pair(unordered_pair(sK64,apply(sK66,sK64)),unordered_pair(sK64,sK64)),sK66)
| ~ relation(sK66)
| ~ function(sK66)
| ~ in(sK64,relation_dom(sK66)) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_7904,plain,
( relation(relation_composition(sK66,sK65))
| ~ relation(sK65)
| ~ relation(sK66) ),
inference(instantiation,[status(thm)],[c_198]) ).
tcf(c_7909,plain,
( function(relation_composition(sK66,sK65))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ function(sK65)
| ~ function(sK66) ),
inference(instantiation,[status(thm)],[c_212]) ).
tcf(c_10464,plain,
! [X0: $i] :
( in(unordered_pair(unordered_pair(sK64,apply(sK65,apply(sK66,sK64))),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ in(unordered_pair(unordered_pair(sK64,X0),unordered_pair(sK64,sK64)),sK66)
| ~ in(unordered_pair(unordered_pair(X0,apply(sK65,apply(sK66,sK64))),unordered_pair(X0,X0)),sK65) ),
inference(instantiation,[status(thm)],[c_1294]) ).
tcf(c_26117,plain,
( in(unordered_pair(unordered_pair(sK64,apply(sK65,apply(sK66,sK64))),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ in(unordered_pair(unordered_pair(sK64,apply(sK66,sK64)),unordered_pair(sK64,sK64)),sK66)
| ~ in(unordered_pair(unordered_pair(apply(sK66,sK64),apply(sK65,apply(sK66,sK64))),unordered_pair(apply(sK66,sK64),apply(sK66,sK64))),sK65) ),
inference(instantiation,[status(thm)],[c_10464]) ).
tcf(c_26118,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_26117,c_7909,c_7904,c_7890,c_7849,c_6296,c_6246,c_6247,c_322,c_323,c_324,c_325,c_326,c_327]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU214+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.12/15.61 % CPULimit : 300
% 0.12/15.61 % WCLimit : 300
% 0.12/15.61 % DateTime : Thu Sep 24 13:13:15 UTC 2026
% 0.12/15.62 % CPUTime :
% 0.12/15.62 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/15.68 Running first-order theorem proving
% 0.12/15.68 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.12/15.69
% 0.12/15.69 % ======== iProver multi-core TPTP/SMT =========
% 0.12/15.69
% 0.12/15.69 % Detected problem language: tptp
% 0.53/15.71 % Proving...
% 48.91/28.84 % SZS status Started for theBenchmark.p
% 48.91/28.84 % SZS status Theorem for theBenchmark.p
% 48.91/28.84
% 48.91/28.84 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 48.91/28.84
% 48.91/28.84 % ------ iProver source info
% 48.91/28.84
% 48.91/28.84 % git: date: 2026-07-19 20:42:38 +0200
% 48.91/28.84 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 48.91/28.84 % git: non_committed_changes: false
% 48.91/28.84
% 48.91/28.84 % ------ Parsing...
% 48.91/28.84 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 48.91/28.84
% 48.91/28.84 % ------ Preprocessing...%
% 48.91/28.84
% 48.91/28.84 % ------ Preprocessing...%
% 48.91/28.84
% 48.91/28.84 % ------ Preprocessing...
% 48.91/28.84 % ------ Proving...
% 48.91/28.84 % ------ Problem Properties
% 48.91/28.84
% 48.91/28.84 %
% 48.91/28.84 % clauses 334
% 48.91/28.84 % conjectures 6
% 48.91/28.84 % EPR 39
% 48.91/28.84 % Horn 270
% 48.91/28.84 % unary 54
% 48.91/28.84 % binary 108
% 48.91/28.84 % lits 890
% 48.91/28.84 % lits eq 172
% 48.91/28.84 % fd_pure 0
% 48.91/28.84 % fd_pseudo 0
% 48.91/28.84 % fd_cond 14
% 48.91/28.84 % fd_pseudo_cond 69
% 48.91/28.84 % AC symbols 0
% 48.91/28.84
% 48.91/28.84 % ------ Input Options Time Limit: Unbounded
% 48.91/28.84
% 48.91/28.84
% 48.91/28.84 % ------
% 48.91/28.84 % Current options:
% 48.91/28.84 % ------
% 48.91/28.84
% 48.91/28.84
% 48.91/28.84 %
% 48.91/28.84
% 48.91/28.84 % ------ Proving...
% 48.91/28.84 %
% 48.91/28.84
% 48.91/28.84 % SZS status Theorem for theBenchmark.p
% 48.91/28.84
% 48.91/28.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 48.91/28.84
% 48.91/28.84
%------------------------------------------------------------------------------