%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU220+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 : n009.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:56:10 PM UTC 2026
% Result : Theorem 36.21s 5.83s
% Output : CNFRefutation 36.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f438ERROR: Could not build tree for root c_91307ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X1,X0)
& subset(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f42,axiom,
! [X0] :
( ( function(X0)
& relation(X0) )
=> ( one_to_one(X0)
=> function_inverse(X0) = relation_inverse(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_funct_1) ).
fof(f50,axiom,
! [X0] :
( ( function(X0)
& relation(X0) )
=> ( function(function_inverse(X0))
& relation(function_inverse(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_funct_1) ).
fof(f60,axiom,
! [X0] :
( relation(X0)
=> relation(relation_inverse(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_relat_1) ).
fof(f86,axiom,
! [X0] :
( ( one_to_one(X0)
& function(X0)
& relation(X0) )
=> ( function(relation_inverse(X0))
& relation(relation_inverse(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_funct_1) ).
fof(f159,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(f161,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ( subset(X0,X1)
=> ( subset(relation_rng(X0),relation_rng(X1))
& subset(relation_dom(X0),relation_dom(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_relat_1) ).
fof(f174,axiom,
! [X0] :
( relation(X0)
=> ( relation_dom(X0) = relation_rng(relation_inverse(X0))
& relation_rng(X0) = relation_dom(relation_inverse(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_relat_1) ).
fof(f189,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ( subset(relation_rng(X0),relation_dom(X1))
=> relation_dom(relation_composition(X0,X1)) = relation_dom(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_relat_1) ).
fof(f204,conjecture,
! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ( ( in(X0,relation_rng(X1))
& one_to_one(X1) )
=> ( X0 = apply(relation_composition(function_inverse(X1),X1),X0)
& X0 = apply(X1,apply(function_inverse(X1),X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_funct_1) ).
fof(f205,negated_conjecture,
~ ! [X0,X1] :
( ( function(X1)
& relation(X1) )
=> ( ( in(X0,relation_rng(X1))
& one_to_one(X1) )
=> ( X0 = apply(relation_composition(function_inverse(X1),X1),X0)
& X0 = apply(X1,apply(function_inverse(X1),X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f204]) ).
fof(f286,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,[],[f159]) ).
fof(f287,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,[],[f286]) ).
fof(f290,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ~ subset(X0,X1)
| ( subset(relation_rng(X0),relation_rng(X1))
& subset(relation_dom(X0),relation_dom(X1)) ) ) ),
inference(ennf_transformation,[],[f161]) ).
fof(f291,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ~ subset(X0,X1)
| ( subset(relation_rng(X0),relation_rng(X1))
& subset(relation_dom(X0),relation_dom(X1)) ) ) ),
inference(flattening,[],[f290]) ).
fof(f301,plain,
! [X0] :
( ~ relation(X0)
| ( relation_dom(X0) = relation_rng(relation_inverse(X0))
& relation_rng(X0) = relation_dom(relation_inverse(X0)) ) ),
inference(ennf_transformation,[],[f174]) ).
fof(f308,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ~ subset(relation_rng(X0),relation_dom(X1))
| relation_dom(relation_composition(X0,X1)) = relation_dom(X0) ) ),
inference(ennf_transformation,[],[f189]) ).
fof(f309,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ~ subset(relation_rng(X0),relation_dom(X1))
| relation_dom(relation_composition(X0,X1)) = relation_dom(X0) ) ),
inference(flattening,[],[f308]) ).
fof(f330,plain,
? [X0,X1] :
( function(X1)
& relation(X1)
& in(X0,relation_rng(X1))
& one_to_one(X1)
& ( apply(relation_composition(function_inverse(X1),X1),X0) != X0
| apply(X1,apply(function_inverse(X1),X0)) != X0 ) ),
inference(ennf_transformation,[],[f205]) ).
fof(f331,plain,
? [X0,X1] :
( function(X1)
& relation(X1)
& in(X0,relation_rng(X1))
& one_to_one(X1)
& ( apply(relation_composition(function_inverse(X1),X1),X0) != X0
| apply(X1,apply(function_inverse(X1),X0)) != X0 ) ),
inference(flattening,[],[f330]) ).
fof(f408,plain,
! [X0] :
( ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0)
| ( function(relation_inverse(X0))
& relation(relation_inverse(X0)) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f409,plain,
! [X0] :
( ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0)
| ( function(relation_inverse(X0))
& relation(relation_inverse(X0)) ) ),
inference(flattening,[],[f408]) ).
fof(f411,plain,
! [X0] :
( ~ relation(X0)
| relation(relation_inverse(X0)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f412,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| function_inverse(X0) = relation_inverse(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f413,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| function_inverse(X0) = relation_inverse(X0) ),
inference(flattening,[],[f412]) ).
fof(f429,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ( function(function_inverse(X0))
& relation(function_inverse(X0)) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f430,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ( function(function_inverse(X0))
& relation(function_inverse(X0)) ) ),
inference(flattening,[],[f429]) ).
fof(f475,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ! [X1] :
( ~ function(X1)
| ~ relation(X1)
| ( ( function_inverse(X0) != X1
| ( ! [X2,X3] :
( sP0(X0,X2,X3,X1)
& ( apply(X1,X2) != X3
| ~ in(X2,relation_rng(X0))
| ( X2 = apply(X0,X3)
& in(X3,relation_dom(X0)) ) ) )
& relation_dom(X1) = relation_rng(X0) ) )
& ( ? [X2,X3] :
( ~ sP0(X0,X2,X3,X1)
| ( apply(X1,X2) = X3
& in(X2,relation_rng(X0))
& ( apply(X0,X3) != X2
| ~ in(X3,relation_dom(X0)) ) ) )
| relation_rng(X0) != relation_dom(X1)
| X1 = function_inverse(X0) ) ) ) ),
inference(nnf_transformation,[],[f438]) ).
fof(f476,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ! [X1] :
( ~ function(X1)
| ~ relation(X1)
| ( ( function_inverse(X0) != X1
| ( ! [X2,X3] :
( sP0(X0,X2,X3,X1)
& ( apply(X1,X2) != X3
| ~ in(X2,relation_rng(X0))
| ( X2 = apply(X0,X3)
& in(X3,relation_dom(X0)) ) ) )
& relation_dom(X1) = relation_rng(X0) ) )
& ( ? [X2,X3] :
( ~ sP0(X0,X2,X3,X1)
| ( apply(X1,X2) = X3
& in(X2,relation_rng(X0))
& ( apply(X0,X3) != X2
| ~ in(X3,relation_dom(X0)) ) ) )
| relation_rng(X0) != relation_dom(X1)
| X1 = function_inverse(X0) ) ) ) ),
inference(flattening,[],[f475]) ).
fof(f477,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ! [X1] :
( ~ function(X1)
| ~ relation(X1)
| ( ( function_inverse(X0) != X1
| ( ! [X4,X5] :
( sP0(X0,X4,X5,X1)
& ( apply(X1,X4) != X5
| ~ in(X4,relation_rng(X0))
| ( apply(X0,X5) = X4
& in(X5,relation_dom(X0)) ) ) )
& relation_dom(X1) = relation_rng(X0) ) )
& ( ? [X2,X3] :
( ~ sP0(X0,X2,X3,X1)
| ( apply(X1,X2) = X3
& in(X2,relation_rng(X0))
& ( apply(X0,X3) != X2
| ~ in(X3,relation_dom(X0)) ) ) )
| relation_rng(X0) != relation_dom(X1)
| X1 = function_inverse(X0) ) ) ) ),
inference(rectify,[],[f476]) ).
fof(f478,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ! [X1] :
( ~ function(X1)
| ~ relation(X1)
| ( ( function_inverse(X0) != X1
| ( ! [X4,X5] :
( sP0(X0,X4,X5,X1)
& ( apply(X1,X4) != X5
| ~ in(X4,relation_rng(X0))
| ( apply(X0,X5) = X4
& in(X5,relation_dom(X0)) ) ) )
& relation_dom(X1) = relation_rng(X0) ) )
& ( ~ sP0(X0,sK8(X0,X1),sK9(X0,X1),X1)
| ( sK9(X0,X1) = apply(X1,sK8(X0,X1))
& in(sK8(X0,X1),relation_rng(X0))
& ( sK8(X0,X1) != apply(X0,sK9(X0,X1))
| ~ in(sK9(X0,X1),relation_dom(X0)) ) )
| relation_rng(X0) != relation_dom(X1)
| X1 = function_inverse(X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X2,sK8(X0,X1)),skolemize(X3,sK9(X0,X1))],[f477]) ).
fof(f480,plain,
( function(sK13)
& relation(sK13)
& in(sK12,relation_rng(sK13))
& one_to_one(sK13)
& ( sK12 != apply(relation_composition(function_inverse(sK13),sK13),sK12)
| sK12 != apply(sK13,apply(function_inverse(sK13),sK12)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X0,sK12),skolemize(X1,sK13)],[f331]) ).
fof(f506,plain,
! [X0,X1] :
( ( X0 != X1
| ( subset(X1,X0)
& subset(X0,X1) ) )
& ( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f507,plain,
! [X0,X1] :
( ( X0 != X1
| ( subset(X1,X0)
& subset(X0,X1) ) )
& ( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ) ),
inference(flattening,[],[f506]) ).
fof(f649,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,[],[f287]) ).
fof(f651,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ subset(X0,X1)
| subset(relation_rng(X0),relation_rng(X1)) ),
inference(cnf_transformation,[],[f291]) ).
fof(f667,plain,
! [X0] :
( ~ relation(X0)
| relation_dom(X0) = relation_rng(relation_inverse(X0)) ),
inference(cnf_transformation,[],[f301]) ).
fof(f668,plain,
! [X0] :
( ~ relation(X0)
| relation_rng(X0) = relation_dom(relation_inverse(X0)) ),
inference(cnf_transformation,[],[f301]) ).
fof(f690,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ subset(relation_rng(X0),relation_dom(X1))
| relation_dom(X0) = relation_dom(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f309]) ).
fof(f706,plain,
! [X0,X1,X4,X5] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ~ function(X1)
| ~ relation(X1)
| function_inverse(X0) != X1
| apply(X1,X4) != X5
| ~ in(X4,relation_rng(X0))
| apply(X0,X5) = X4 ),
inference(cnf_transformation,[],[f478]) ).
fof(f716,plain,
function(sK13),
inference(cnf_transformation,[],[f480]) ).
fof(f717,plain,
relation(sK13),
inference(cnf_transformation,[],[f480]) ).
fof(f718,plain,
in(sK12,relation_rng(sK13)),
inference(cnf_transformation,[],[f480]) ).
fof(f719,plain,
one_to_one(sK13),
inference(cnf_transformation,[],[f480]) ).
fof(f720,plain,
( sK12 != apply(relation_composition(function_inverse(sK13),sK13),sK12)
| sK12 != apply(sK13,apply(function_inverse(sK13),sK12)) ),
inference(cnf_transformation,[],[f480]) ).
fof(f789,plain,
! [X0,X1] :
( X0 != X1
| subset(X1,X0) ),
inference(cnf_transformation,[],[f507]) ).
fof(f944,plain,
! [X0] :
( ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0)
| function(relation_inverse(X0)) ),
inference(cnf_transformation,[],[f409]) ).
fof(f948,plain,
! [X0] :
( ~ relation(X0)
| relation(relation_inverse(X0)) ),
inference(cnf_transformation,[],[f411]) ).
fof(f949,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| relation_inverse(X0) = function_inverse(X0) ),
inference(cnf_transformation,[],[f413]) ).
fof(f976,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| function(function_inverse(X0)) ),
inference(cnf_transformation,[],[f430]) ).
fof(f977,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| relation(function_inverse(X0)) ),
inference(cnf_transformation,[],[f430]) ).
fof(f1136,plain,
! [X0,X1,X4] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ~ function(X1)
| ~ relation(X1)
| function_inverse(X0) != X1
| ~ in(X4,relation_rng(X0))
| apply(X0,apply(X1,X4)) = X4 ),
inference(equality_resolution,[],[f706]) ).
fof(f1137,plain,
! [X0,X4] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| ~ function(function_inverse(X0))
| ~ relation(function_inverse(X0))
| ~ in(X4,relation_rng(X0))
| apply(X0,apply(function_inverse(X0),X4)) = X4 ),
inference(equality_resolution,[],[f1136]) ).
fof(f1148,plain,
! [X1] : subset(X1,X1),
inference(equality_resolution,[],[f789]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) )
| ~ function(X2)
| ~ function(X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ in(X0,relation_dom(relation_composition(X1,X2))) ),
inference(cnf_transformation,[],[f649]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] :
( subset(relation_rng(X0),relation_rng(X1))
| ~ relation(X1)
| ~ relation(X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f651]) ).
tcf(c_130,plain,
! [X0: $i] :
( ( relation_dom(relation_inverse(X0)) = relation_rng(X0) )
| ~ relation(X0) ),
inference(cnf_transformation,[],[f668]) ).
tcf(c_131,plain,
! [X0: $i] :
( ( relation_rng(relation_inverse(X0)) = relation_dom(X0) )
| ~ relation(X0) ),
inference(cnf_transformation,[],[f667]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( ( relation_dom(relation_composition(X0,X1)) = relation_dom(X0) )
| ~ relation(X1)
| ~ relation(X0)
| ~ subset(relation_rng(X0),relation_dom(X1)) ),
inference(cnf_transformation,[],[f690]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] :
( ( apply(X1,apply(function_inverse(X1),X0)) = X0 )
| ~ one_to_one(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(function_inverse(X1))
| ~ relation(function_inverse(X1))
| ~ in(X0,relation_rng(X1)) ),
inference(cnf_transformation,[],[f1137]) ).
tcf(c_178,negated_conjecture,
( ( apply(sK13,apply(function_inverse(sK13),sK12)) != sK12 )
| ( apply(relation_composition(function_inverse(sK13),sK13),sK12) != sK12 ) ),
inference(cnf_transformation,[],[f720]) ).
tcf(c_179,negated_conjecture,
one_to_one(sK13),
inference(cnf_transformation,[],[f719]) ).
tcf(c_180,negated_conjecture,
in(sK12,relation_rng(sK13)),
inference(cnf_transformation,[],[f718]) ).
tcf(c_181,negated_conjecture,
relation(sK13),
inference(cnf_transformation,[],[f717]) ).
tcf(c_182,negated_conjecture,
function(sK13),
inference(cnf_transformation,[],[f716]) ).
tcf(c_252,plain,
! [X0: $i] : subset(X0,X0),
inference(cnf_transformation,[],[f1148]) ).
tcf(c_405,plain,
! [X0: $i] :
( function(relation_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f944]) ).
tcf(c_408,plain,
! [X0: $i] :
( relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f948]) ).
tcf(c_409,plain,
! [X0: $i] :
( ( relation_inverse(X0) = function_inverse(X0) )
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f949]) ).
tcf(c_434,plain,
! [X0: $i] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f977]) ).
tcf(c_435,plain,
! [X0: $i] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f976]) ).
tcf(c_2319,plain,
! [X0: $i,X1: $i] :
( ( apply(X1,apply(function_inverse(X1),X0)) = X0 )
| ~ one_to_one(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(function_inverse(X1))
| ~ in(X0,relation_rng(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_172,c_434]) ).
tcf(c_2329,plain,
! [X0: $i,X1: $i] :
( ( apply(X1,apply(function_inverse(X1),X0)) = X0 )
| ~ one_to_one(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ in(X0,relation_rng(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2319,c_435]) ).
tcf(c_18470,plain,
( ( apply(sK13,apply(function_inverse(sK13),sK12)) = sK12 )
| ~ one_to_one(sK13)
| ~ function(sK13)
| ~ relation(sK13) ),
inference(superposition,[status(thm)],[c_180,c_2329]) ).
tcf(c_18472,plain,
apply(sK13,apply(function_inverse(sK13),sK12)) = sK12,
inference(forward_subsumption_resolution,[status(thm)],[c_18470,c_179,c_182,c_181]) ).
tcf(c_18473,plain,
apply(relation_composition(function_inverse(sK13),sK13),sK12) != sK12,
inference(backward_subsumption_resolution,[status(thm)],[c_178,c_18472]) ).
tcf(c_21106,plain,
relation_dom(relation_inverse(sK13)) = relation_rng(sK13),
inference(superposition,[status(thm)],[c_181,c_130]) ).
tcf(c_21161,plain,
relation_rng(relation_inverse(sK13)) = relation_dom(sK13),
inference(superposition,[status(thm)],[c_181,c_131]) ).
tcf(c_47040,plain,
( ( relation_inverse(sK13) = function_inverse(sK13) )
| ~ function(sK13)
| ~ relation(sK13) ),
inference(superposition,[status(thm)],[c_179,c_409]) ).
tcf(c_47052,plain,
relation_inverse(sK13) = function_inverse(sK13),
inference(forward_subsumption_resolution,[status(thm)],[c_47040,c_182,c_181]) ).
tcf(c_47149,plain,
relation_rng(function_inverse(sK13)) = relation_dom(sK13),
inference(demodulation,[status(thm)],[c_21161,c_47052]) ).
tcf(c_47150,plain,
relation_dom(function_inverse(sK13)) = relation_rng(sK13),
inference(demodulation,[status(thm)],[c_21106,c_47052]) ).
tcf(c_47578,plain,
( function(function_inverse(sK13))
| ~ one_to_one(sK13)
| ~ function(sK13)
| ~ relation(sK13) ),
inference(superposition,[status(thm)],[c_47052,c_405]) ).
tcf(c_47581,plain,
( relation(function_inverse(sK13))
| ~ relation(sK13) ),
inference(superposition,[status(thm)],[c_47052,c_408]) ).
tcf(c_47584,plain,
relation(function_inverse(sK13)),
inference(forward_subsumption_resolution,[status(thm)],[c_47581,c_181]) ).
tcf(c_47585,plain,
function(function_inverse(sK13)),
inference(forward_subsumption_resolution,[status(thm)],[c_47578,c_179,c_182,c_181]) ).
tcf(c_47621,plain,
! [X0: $i] :
( subset(relation_rng(X0),relation_dom(sK13))
| ~ relation(X0)
| ~ relation(function_inverse(sK13))
| ~ subset(X0,function_inverse(sK13)) ),
inference(superposition,[status(thm)],[c_47149,c_115]) ).
tcf(c_47652,plain,
! [X0: $i] :
( subset(relation_rng(X0),relation_dom(sK13))
| ~ relation(X0)
| ~ subset(X0,function_inverse(sK13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47621,c_47584]) ).
tcf(c_64241,plain,
! [X0: $i] :
( ( relation_dom(relation_composition(X0,sK13)) = relation_dom(X0) )
| ~ relation(sK13)
| ~ relation(X0)
| ~ subset(X0,function_inverse(sK13)) ),
inference(superposition,[status(thm)],[c_47652,c_153]) ).
tcf(c_64283,plain,
! [X0: $i] :
( ( relation_dom(relation_composition(X0,sK13)) = relation_dom(X0) )
| ~ relation(X0)
| ~ subset(X0,function_inverse(sK13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64241,c_181]) ).
tcf(c_64392,plain,
( ( relation_dom(relation_composition(function_inverse(sK13),sK13)) = relation_dom(function_inverse(sK13)) )
| ~ relation(function_inverse(sK13)) ),
inference(superposition,[status(thm)],[c_252,c_64283]) ).
tcf(c_64411,plain,
( ( relation_dom(relation_composition(function_inverse(sK13),sK13)) = relation_rng(sK13) )
| ~ relation(function_inverse(sK13)) ),
inference(light_normalisation,[status(thm)],[c_64392,c_47150]) ).
tcf(c_64412,plain,
relation_dom(relation_composition(function_inverse(sK13),sK13)) = relation_rng(sK13),
inference(forward_subsumption_resolution,[status(thm)],[c_64411,c_47584]) ).
tcf(c_88229,plain,
! [X0: $i] :
( ( apply(relation_composition(function_inverse(sK13),sK13),X0) = apply(sK13,apply(function_inverse(sK13),X0)) )
| ~ function(sK13)
| ~ relation(sK13)
| ~ function(function_inverse(sK13))
| ~ relation(function_inverse(sK13))
| ~ in(X0,relation_rng(sK13)) ),
inference(superposition,[status(thm)],[c_64412,c_112]) ).
tcf(c_88249,plain,
! [X0: $i] :
( ( apply(relation_composition(function_inverse(sK13),sK13),X0) = apply(sK13,apply(function_inverse(sK13),X0)) )
| ~ in(X0,relation_rng(sK13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_88229,c_182,c_181,c_47585,c_47584]) ).
tcf(c_91247,plain,
apply(relation_composition(function_inverse(sK13),sK13),sK12) = apply(sK13,apply(function_inverse(sK13),sK12)),
inference(superposition,[status(thm)],[c_180,c_88249]) ).
tcf(c_91306,plain,
apply(relation_composition(function_inverse(sK13),sK13),sK12) = sK12,
inference(light_normalisation,[status(thm)],[c_91247,c_18472]) ).
tcf(c_91307,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_91306,c_18473]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU220+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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 13:14:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 36.21/5.83 % SZS status Started for theBenchmark.p
% 36.21/5.83 % SZS status Theorem for theBenchmark.p
% 36.21/5.83
% 36.21/5.83 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 36.21/5.83
% 36.21/5.83 % ------ iProver source info
% 36.21/5.83
% 36.21/5.83 % git: date: 2026-07-19 20:42:38 +0200
% 36.21/5.83 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 36.21/5.83 % git: non_committed_changes: false
% 36.21/5.83
% 36.21/5.83 % ------ Parsing...
% 36.21/5.83 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 36.21/5.83
% 36.21/5.83 % ------ Preprocessing... sup_sim: 42 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 %
% 36.21/5.83
% 36.21/5.83 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 36.21/5.83
% 36.21/5.83 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 36.21/5.83 % ------ Proving...
% 36.21/5.83 % ------ Problem Properties
% 36.21/5.83
% 36.21/5.83 %
% 36.21/5.83 % clauses 353
% 36.21/5.83 % conjectures 5
% 36.21/5.83 % EPR 46
% 36.21/5.83 % Horn 290
% 36.21/5.83 % unary 56
% 36.21/5.83 % binary 114
% 36.21/5.83 % lits 968
% 36.21/5.83 % lits eq 180
% 36.21/5.83 % fd_pure 0
% 36.21/5.83 % fd_pseudo 0
% 36.21/5.83 % fd_cond 11
% 36.21/5.83 % fd_pseudo_cond 70
% 36.21/5.83 % AC symbols 0
% 36.21/5.83
% 36.21/5.83 % ------ Schedule dynamic 5 is on
% 36.21/5.83
% 36.21/5.83 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 36.21/5.83
% 36.21/5.83
% 36.21/5.83 % ------
% 36.21/5.83 % Current options:
% 36.21/5.83 % ------
% 36.21/5.83
% 36.21/5.83
% 36.21/5.83 %
% 36.21/5.83
% 36.21/5.83 % ------ Proving...
% 36.21/5.83 %
% 36.21/5.83
% 36.21/5.83 % SZS status Theorem for theBenchmark.p
% 36.21/5.83
% 36.21/5.83 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 36.21/5.83
% 36.21/5.83
%------------------------------------------------------------------------------