%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU069+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 : Tue Sep 29 12:47:10 PM UTC 2026
% Result : Theorem 8.70s 2.28s
% Output : Refutation 9.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 26
% Syntax : Number of formulae : 256 ( 27 unt; 20 def)
% Number of atoms : 867 ( 113 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1055 ( 444 ~; 482 |; 92 &)
% ( 32 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 16 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-3 aty)
% Number of variables : 255 ( 0 sgn 232 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f7,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( X2 = relation_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,relation_dom(X0))
& in(X4,X1)
& X3 = apply(X0,X4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_funct_1) ).
fof(f8,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_funct_1) ).
fof(f9,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f10,axiom,
! [X0,X1,X2] :
( X2 = set_intersection2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f32,conjecture,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> relation_image(X2,set_intersection2(X0,relation_inverse_image(X2,X1))) = set_intersection2(relation_image(X2,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t150_funct_1) ).
fof(f33,negated_conjecture,
~ ! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> relation_image(X2,set_intersection2(X0,relation_inverse_image(X2,X1))) = set_intersection2(relation_image(X2,X0),X1) ),
inference(negated_conjecture,[status(cth)],[f32]) ).
fof(f54,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,relation_dom(X0))
& in(X4,X1)
& X3 = apply(X0,X4) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f55,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,relation_dom(X0))
& in(X4,X1)
& X3 = apply(X0,X4) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f57,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f67,plain,
? [X0,X1,X2] :
( relation_image(X2,set_intersection2(X0,relation_inverse_image(X2,X1))) != set_intersection2(relation_image(X2,X0),X1)
& relation(X2)
& function(X2) ),
inference(ennf_transformation,[],[f33]) ).
fof(f68,plain,
? [X0,X1,X2] :
( relation_image(X2,set_intersection2(X0,relation_inverse_image(X2,X1))) != set_intersection2(relation_image(X2,X0),X1)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f67]) ).
fof(f78,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f79,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_image(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ in(X4,relation_dom(X0))
| ~ in(X4,X1)
| apply(X0,X4) != X3 )
| ~ in(X3,X2) )
& ( ? [X4] :
( in(X4,relation_dom(X0))
& in(X4,X1)
& X3 = apply(X0,X4) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ! [X4] :
( ~ in(X4,relation_dom(X0))
| ~ in(X4,X1)
| apply(X0,X4) != X3 ) )
& ( ? [X4] :
( in(X4,relation_dom(X0))
& in(X4,X1)
& X3 = apply(X0,X4) )
| ~ in(X3,X2) ) )
| relation_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f55]) ).
fof(f81,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_image(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ in(X4,relation_dom(X0))
| ~ in(X4,X1)
| apply(X0,X4) != X3 )
| ~ in(X3,X2) )
& ( ? [X5] :
( in(X5,relation_dom(X0))
& in(X5,X1)
& apply(X0,X5) = X3 )
| in(X3,X2) ) ) )
& ( ! [X6] :
( ( in(X6,X2)
| ! [X7] :
( ~ in(X7,relation_dom(X0))
| ~ in(X7,X1)
| apply(X0,X7) != X6 ) )
& ( ? [X8] :
( in(X8,relation_dom(X0))
& in(X8,X1)
& apply(X0,X8) = X6 )
| ~ in(X6,X2) ) )
| relation_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f80]) ).
fof(f82,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_image(X0,X1)
| ( ( ! [X4] :
( ~ in(X4,relation_dom(X0))
| ~ in(X4,X1)
| apply(X0,X4) != sK0(X0,X1,X2) )
| ~ in(sK0(X0,X1,X2),X2) )
& ( ( in(sK1(X0,X1,X2),relation_dom(X0))
& in(sK1(X0,X1,X2),X1)
& sK0(X0,X1,X2) = apply(X0,sK1(X0,X1,X2)) )
| in(sK0(X0,X1,X2),X2) ) ) )
& ( ! [X6] :
( ( in(X6,X2)
| ! [X7] :
( ~ in(X7,relation_dom(X0))
| ~ in(X7,X1)
| apply(X0,X7) != X6 ) )
& ( ( in(sK2(X0,X1,X6),relation_dom(X0))
& in(sK2(X0,X1,X6),X1)
& apply(X0,sK2(X0,X1,X6)) = X6 )
| ~ in(X6,X2) ) )
| relation_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X3,sK0(X0,X1,X2)),skolemize(X5,sK1(X0,X1,X2)),skolemize(X8,sK2(X0,X1,X6))],[f81]) ).
fof(f83,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| ~ in(X3,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f57]) ).
fof(f84,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| ~ in(X3,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,relation_dom(X0))
| ~ in(apply(X0,X4),X1) )
& ( ( in(X4,relation_dom(X0))
& in(apply(X0,X4),X1) )
| ~ in(X4,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f84]) ).
fof(f86,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ( ( ~ in(sK3(X0,X1,X2),relation_dom(X0))
| ~ in(apply(X0,sK3(X0,X1,X2)),X1)
| ~ in(sK3(X0,X1,X2),X2) )
& ( ( in(sK3(X0,X1,X2),relation_dom(X0))
& in(apply(X0,sK3(X0,X1,X2)),X1) )
| in(sK3(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,relation_dom(X0))
| ~ in(apply(X0,X4),X1) )
& ( ( in(X4,relation_dom(X0))
& in(apply(X0,X4),X1) )
| ~ in(X4,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f88,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK4(X0,X1),X1)
& in(sK4(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f88]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| ~ in(X3,X1) )
& ( ( in(X3,X0)
& in(X3,X1) )
| ~ in(X3,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| ~ in(X3,X1) )
& ( ( in(X3,X0)
& in(X3,X1) )
| ~ in(X3,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| ~ in(X4,X1) )
& ( ( in(X4,X0)
& in(X4,X1) )
| ~ in(X4,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(rectify,[],[f91]) ).
fof(f93,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ( ( ~ in(sK5(X0,X1,X2),X0)
| ~ in(sK5(X0,X1,X2),X1)
| ~ in(sK5(X0,X1,X2),X2) )
& ( ( in(sK5(X0,X1,X2),X0)
& in(sK5(X0,X1,X2),X1) )
| in(sK5(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| ~ in(X4,X1) )
& ( ( in(X4,X0)
& in(X4,X1) )
| ~ in(X4,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f92]) ).
fof(f105,plain,
( relation_image(sK19,set_intersection2(sK17,relation_inverse_image(sK19,sK18))) != set_intersection2(relation_image(sK19,sK17),sK18)
& relation(sK19)
& function(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X0,sK17),skolemize(X1,sK18),skolemize(X2,sK19)],[f68]) ).
fof(f115,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f79]) ).
fof(f116,plain,
! [X2,X0,X1,X6] :
( apply(X0,sK2(X0,X1,X6)) = X6
| ~ in(X6,X2)
| relation_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f117,plain,
! [X2,X0,X1,X6] :
( in(sK2(X0,X1,X6),X1)
| ~ in(X6,X2)
| relation_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f118,plain,
! [X2,X0,X1,X6] :
( in(sK2(X0,X1,X6),relation_dom(X0))
| ~ in(X6,X2)
| relation_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f119,plain,
! [X2,X0,X1,X6,X7] :
( in(X6,X2)
| ~ in(X7,relation_dom(X0))
| ~ in(X7,X1)
| apply(X0,X7) != X6
| relation_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f124,plain,
! [X2,X0,X1,X4] :
( in(apply(X0,X4),X1)
| ~ in(X4,X2)
| relation_inverse_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f125,plain,
! [X2,X0,X1,X4] :
( in(X4,relation_dom(X0))
| ~ in(X4,X2)
| relation_inverse_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f126,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,relation_dom(X0))
| ~ in(apply(X0,X4),X1)
| relation_inverse_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f131,plain,
! [X0,X1] :
( in(sK4(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f132,plain,
! [X0,X1] :
( ~ in(sK4(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f133,plain,
! [X2,X0,X1,X4] :
( in(X4,X1)
| ~ in(X4,X2)
| set_intersection2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f93]) ).
fof(f134,plain,
! [X2,X0,X1,X4] :
( in(X4,X0)
| ~ in(X4,X2)
| set_intersection2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f93]) ).
fof(f135,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| ~ in(X4,X1)
| set_intersection2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f93]) ).
fof(f171,plain,
function(sK19),
inference(cnf_transformation,[],[f105]) ).
fof(f172,plain,
relation(sK19),
inference(cnf_transformation,[],[f105]) ).
fof(f173,plain,
relation_image(sK19,set_intersection2(sK17,relation_inverse_image(sK19,sK18))) != set_intersection2(relation_image(sK19,sK17),sK18),
inference(cnf_transformation,[],[f105]) ).
fof(f186,plain,
! [X2,X0,X1,X7] :
( in(apply(X0,X7),X2)
| ~ in(X7,relation_dom(X0))
| ~ in(X7,X1)
| relation_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f187,plain,
! [X0,X1,X7] :
( in(apply(X0,X7),relation_image(X0,X1))
| ~ in(X7,relation_dom(X0))
| ~ in(X7,X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f186]) ).
fof(f188,plain,
! [X0,X1,X6] :
( in(sK2(X0,X1,X6),relation_dom(X0))
| ~ in(X6,relation_image(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f118]) ).
fof(f189,plain,
! [X0,X1,X6] :
( in(sK2(X0,X1,X6),X1)
| ~ in(X6,relation_image(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f117]) ).
fof(f190,plain,
! [X0,X1,X6] :
( ~ in(X6,relation_image(X0,X1))
| apply(X0,sK2(X0,X1,X6)) = X6
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f116]) ).
fof(f191,plain,
! [X0,X1,X4] :
( ~ in(apply(X0,X4),X1)
| ~ in(X4,relation_dom(X0))
| in(X4,relation_inverse_image(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f126]) ).
fof(f192,plain,
! [X0,X1,X4] :
( ~ in(X4,relation_inverse_image(X0,X1))
| in(X4,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f125]) ).
fof(f193,plain,
! [X0,X1,X4] :
( ~ in(X4,relation_inverse_image(X0,X1))
| in(apply(X0,X4),X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f124]) ).
fof(f194,plain,
! [X0,X1,X4] :
( in(X4,set_intersection2(X0,X1))
| ~ in(X4,X0)
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f135]) ).
fof(f195,plain,
! [X0,X1,X4] :
( ~ in(X4,set_intersection2(X0,X1))
| in(X4,X0) ),
inference(equality_resolution,[],[f134]) ).
fof(f196,plain,
! [X0,X1,X4] :
( ~ in(X4,set_intersection2(X0,X1))
| in(X4,X1) ),
inference(equality_resolution,[],[f133]) ).
fof(f197,definition,
sF20 = relation_inverse_image(sK19,sK18),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f198,plain,
relation_inverse_image(sK19,sK18) = sF20,
inference(reorient_equations,[],[f197]) ).
fof(f199,definition,
sF21 = set_intersection2(sK17,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f200,plain,
set_intersection2(sK17,sF20) = sF21,
inference(reorient_equations,[],[f199]) ).
fof(f201,definition,
sF22 = relation_image(sK19,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f202,plain,
relation_image(sK19,sF21) = sF22,
inference(reorient_equations,[],[f201]) ).
fof(f203,definition,
sF23 = relation_image(sK19,sK17),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f204,plain,
relation_image(sK19,sK17) = sF23,
inference(reorient_equations,[],[f203]) ).
fof(f205,definition,
sF24 = set_intersection2(sF23,sK18),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f206,plain,
set_intersection2(sF23,sK18) = sF24,
inference(reorient_equations,[],[f205]) ).
fof(f207,plain,
sF22 != sF24,
inference(definition_folding,[],[f173,f206,f204,f202,f200,f198]) ).
fof(f208,plain,
! [X0] :
( ~ in(X0,sF22)
| apply(sK19,sK2(sK19,sF21,X0)) = X0
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f190,f202]) ).
fof(f209,plain,
! [X0] :
( ~ in(X0,sF23)
| apply(sK19,sK2(sK19,sK17,X0)) = X0
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f190,f204]) ).
fof(f210,plain,
! [X0] :
( ~ in(X0,sF23)
| apply(sK19,sK2(sK19,sK17,X0)) = X0
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f209,f172]) ).
fof(f211,plain,
! [X0] :
( ~ in(X0,sF22)
| apply(sK19,sK2(sK19,sF21,X0)) = X0
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f208,f172]) ).
fof(f212,plain,
! [X0] :
( ~ in(X0,sF23)
| apply(sK19,sK2(sK19,sK17,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f210,f171]) ).
fof(f213,plain,
! [X0] :
( ~ in(X0,sF22)
| apply(sK19,sK2(sK19,sF21,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f211,f171]) ).
fof(f214,plain,
! [X0] :
( ~ in(X0,sF24)
| in(X0,sF23) ),
inference(superposition,[],[f195,f206]) ).
fof(f215,plain,
! [X0] :
( ~ in(X0,sF21)
| in(X0,sK17) ),
inference(superposition,[],[f195,f200]) ).
fof(f216,plain,
! [X0] :
( ~ in(X0,sF24)
| in(X0,sK18) ),
inference(superposition,[],[f196,f206]) ).
fof(f217,plain,
! [X0] :
( ~ in(X0,sF21)
| in(X0,sF20) ),
inference(superposition,[],[f196,f200]) ).
fof(f221,plain,
! [X0] :
( ~ in(X0,sF23)
| in(X0,sF24)
| ~ in(X0,sK18) ),
inference(superposition,[],[f194,f206]) ).
fof(f222,plain,
! [X0] :
( ~ in(X0,sF20)
| ~ in(X0,sK17)
| in(X0,sF21) ),
inference(superposition,[],[f194,f200]) ).
fof(f230,plain,
! [X0] :
( subset(sF22,X0)
| sK4(sF22,X0) = apply(sK19,sK2(sK19,sF21,sK4(sF22,X0))) ),
inference(resolution,[],[f131,f213]) ).
fof(f233,plain,
! [X0] :
( in(sK4(sF24,X0),sK18)
| subset(sF24,X0) ),
inference(resolution,[],[f131,f216]) ).
fof(f234,plain,
! [X0] :
( in(sK4(sF24,X0),sF23)
| subset(sF24,X0) ),
inference(resolution,[],[f131,f214]) ).
fof(f238,plain,
! [X0] :
( subset(sF24,X0)
| sK4(sF24,X0) = apply(sK19,sK2(sK19,sK17,sK4(sF24,X0))) ),
inference(resolution,[],[f234,f212]) ).
fof(f243,plain,
! [X0] :
( ~ in(X0,sF20)
| in(apply(sK19,X0),sK18)
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f193,f198]) ).
fof(f244,plain,
! [X0] :
( ~ in(X0,sF20)
| in(apply(sK19,X0),sK18)
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f243,f172]) ).
fof(f245,plain,
! [X0] :
( in(apply(sK19,X0),sK18)
| ~ in(X0,sF20) ),
inference(forward_subsumption_resolution,[],[f244,f171]) ).
fof(f275,plain,
! [X0] :
( in(apply(sK19,X0),sF22)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sF21)
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f187,f202]) ).
fof(f276,plain,
! [X0] :
( in(apply(sK19,X0),sF23)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sK17)
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f187,f204]) ).
fof(f278,plain,
! [X0] :
( in(apply(sK19,X0),sF23)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sK17)
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f276,f172]) ).
fof(f279,plain,
! [X0] :
( in(apply(sK19,X0),sF22)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sF21)
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f275,f172]) ).
fof(f280,plain,
! [X0] :
( in(apply(sK19,X0),sF23)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sK17) ),
inference(forward_subsumption_resolution,[],[f278,f171]) ).
fof(f281,plain,
! [X0] :
( in(apply(sK19,X0),sF22)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sF21) ),
inference(forward_subsumption_resolution,[],[f279,f171]) ).
fof(f282,plain,
! [X0] :
( ~ in(apply(sK19,X0),sK18)
| ~ in(X0,sK17)
| in(apply(sK19,X0),sF24)
| ~ in(X0,relation_dom(sK19)) ),
inference(resolution,[],[f280,f221]) ).
fof(f285,plain,
! [X0] :
( ~ subset(X0,sF22)
| sK4(sF22,X0) = apply(sK19,sK2(sK19,sF21,sK4(sF22,X0)))
| sF22 = X0 ),
inference(resolution,[],[f230,f115]) ).
fof(f287,plain,
! [X0] :
( ~ in(X0,sF20)
| in(X0,relation_dom(sK19))
| ~ relation(sK19)
| ~ function(sK19) ),
inference(superposition,[],[f192,f198]) ).
fof(f288,plain,
! [X0] :
( ~ in(X0,sF20)
| in(X0,relation_dom(sK19))
| ~ function(sK19) ),
inference(forward_subsumption_resolution,[],[f287,f172]) ).
fof(f289,plain,
! [X0] :
( in(X0,relation_dom(sK19))
| ~ in(X0,sF20) ),
inference(forward_subsumption_resolution,[],[f288,f171]) ).
fof(f297,plain,
! [X0,X1] :
( in(sK2(X1,sF21,X0),sF20)
| ~ relation(X1)
| ~ function(X1)
| ~ in(X0,relation_image(X1,sF21)) ),
inference(resolution,[],[f189,f217]) ).
fof(f298,plain,
! [X0,X1] :
( in(sK2(X1,sF21,X0),sK17)
| ~ relation(X1)
| ~ function(X1)
| ~ in(X0,relation_image(X1,sF21)) ),
inference(resolution,[],[f189,f215]) ).
fof(f352,plain,
! [X0] :
( ~ in(X0,sK17)
| in(apply(sK19,X0),sF24)
| ~ in(X0,relation_dom(sK19))
| ~ in(X0,sF20) ),
inference(resolution,[],[f282,f245]) ).
fof(f353,plain,
! [X0] :
( in(apply(sK19,X0),sF24)
| ~ in(X0,sK17)
| ~ in(X0,sF20) ),
inference(forward_subsumption_resolution,[],[f352,f289]) ).
fof(f392,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| sF22 = sF24
| sK4(sF24,sF22) = apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22))) ),
inference(resolution,[],[f285,f238]) ).
fof(f395,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| sK4(sF24,sF22) = apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22))) ),
inference(forward_subsumption_resolution,[],[f392,f207]) ).
fof(f397,definition,
( spl25_7
<=> sK4(sF24,sF22) = apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22))) ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
fof(f398,plain,
( sK4(sF24,sF22) != apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22)))
| spl25_7 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f399,plain,
( sK4(sF24,sF22) = apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22)))
| ~ spl25_7 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f401,definition,
( spl25_8
<=> sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24))) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f402,plain,
( sK4(sF22,sF24) != apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| spl25_8 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f403,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| ~ spl25_8 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f404,plain,
( spl25_7
| spl25_8 ),
inference(avatar_split_clause,[],[f395,f401,f397]) ).
fof(f408,plain,
( in(sK4(sF24,sF22),sF22)
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),sF21)
| ~ spl25_7 ),
inference(superposition,[],[f281,f399]) ).
fof(f411,plain,
( ! [X0] :
( ~ in(sK4(sF24,sF22),X0)
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_inverse_image(sK19,X0))
| ~ relation(sK19)
| ~ function(sK19) )
| ~ spl25_7 ),
inference(superposition,[],[f191,f399]) ).
fof(f412,plain,
( ! [X0] :
( in(sK4(sF24,sF22),relation_image(sK19,X0))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),X0)
| ~ relation(sK19)
| ~ function(sK19) )
| ~ spl25_7 ),
inference(superposition,[],[f187,f399]) ).
fof(f413,plain,
( ! [X0] :
( in(sK4(sF24,sF22),relation_image(sK19,X0))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),X0)
| ~ function(sK19) )
| ~ spl25_7 ),
inference(forward_subsumption_resolution,[],[f412,f172]) ).
fof(f414,plain,
( ! [X0] :
( ~ in(sK4(sF24,sF22),X0)
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_inverse_image(sK19,X0))
| ~ function(sK19) )
| ~ spl25_7 ),
inference(forward_subsumption_resolution,[],[f411,f172]) ).
fof(f416,definition,
( spl25_9
<=> in(sK2(sK19,sK17,sK4(sF24,sF22)),sF20) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
fof(f417,plain,
( in(sK2(sK19,sK17,sK4(sF24,sF22)),sF20)
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),sF20)
| spl25_9 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f420,definition,
( spl25_10
<=> in(sK4(sF24,sF22),sK18) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f421,plain,
( ~ in(sK4(sF24,sF22),sK18)
| spl25_10 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f425,definition,
( spl25_11
<=> in(sK2(sK19,sK17,sK4(sF24,sF22)),sK17) ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
fof(f426,plain,
( in(sK2(sK19,sK17,sK4(sF24,sF22)),sK17)
| ~ spl25_11 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),sK17)
| spl25_11 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f429,definition,
( spl25_12
<=> in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19)) ),
introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition]) ).
fof(f431,plain,
( ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| spl25_12 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f433,definition,
( spl25_13
<=> in(sK4(sF24,sF22),sF23) ),
introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition]) ).
fof(f434,plain,
( ~ in(sK4(sF24,sF22),sF23)
| spl25_13 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( in(sK4(sF24,sF22),sF23)
| ~ spl25_13 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f438,definition,
( spl25_14
<=> in(sK2(sK19,sK17,sK4(sF24,sF22)),sF21) ),
introduced(definition,[new_symbols(definition,[spl25_14])],[avatar_definition]) ).
fof(f439,plain,
( in(sK2(sK19,sK17,sK4(sF24,sF22)),sF21)
| ~ spl25_14 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl25_15
<=> in(sK4(sF24,sF22),sF22) ),
introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition]) ).
fof(f444,plain,
( in(sK4(sF24,sF22),sF22)
| ~ spl25_15 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f445,plain,
( ~ spl25_14
| ~ spl25_12
| spl25_15
| ~ spl25_7 ),
inference(avatar_split_clause,[],[f408,f397,f442,f429,f438]) ).
fof(f453,plain,
( ! [X0] :
( in(sK4(sF24,sF22),relation_image(sK19,X0))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),X0) )
| ~ spl25_7 ),
inference(forward_subsumption_resolution,[],[f413,f171]) ).
fof(f454,plain,
( ! [X0] :
( ~ in(sK4(sF24,sF22),X0)
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_dom(sK19))
| in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_inverse_image(sK19,X0)) )
| ~ spl25_7 ),
inference(forward_subsumption_resolution,[],[f414,f171]) ).
fof(f456,definition,
( spl25_17
<=> ! [X0] :
( in(sK4(sF24,sF22),relation_image(sK19,X0))
| ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl25_17])],[avatar_definition]) ).
fof(f457,plain,
( ! [X0] :
( ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),X0)
| in(sK4(sF24,sF22),relation_image(sK19,X0)) )
| ~ spl25_17 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f458,plain,
( ~ spl25_12
| spl25_17
| ~ spl25_7 ),
inference(avatar_split_clause,[],[f453,f397,f456,f429]) ).
fof(f460,definition,
( spl25_18
<=> ! [X0] :
( ~ in(sK4(sF24,sF22),X0)
| in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_inverse_image(sK19,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition]) ).
fof(f461,plain,
( ! [X0] :
( in(sK2(sK19,sK17,sK4(sF24,sF22)),relation_inverse_image(sK19,X0))
| ~ in(sK4(sF24,sF22),X0) )
| ~ spl25_18 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
( ~ spl25_12
| spl25_18
| ~ spl25_7 ),
inference(avatar_split_clause,[],[f454,f397,f460,f429]) ).
fof(f463,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| ~ relation(sK19)
| ~ function(sK19)
| spl25_12 ),
inference(resolution,[],[f431,f188]) ).
fof(f465,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| ~ function(sK19)
| spl25_12 ),
inference(forward_subsumption_resolution,[],[f463,f172]) ).
fof(f466,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| spl25_12 ),
inference(forward_subsumption_resolution,[],[f465,f171]) ).
fof(f467,plain,
( ~ in(sK4(sF24,sF22),sF23)
| spl25_12 ),
inference(forward_demodulation,[],[f466,f204]) ).
fof(f468,plain,
( ~ spl25_13
| spl25_12 ),
inference(avatar_split_clause,[],[f467,f429,f433]) ).
fof(f469,plain,
( subset(sF24,sF22)
| spl25_13 ),
inference(resolution,[],[f434,f234]) ).
fof(f470,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| sF22 = sF24
| spl25_13 ),
inference(resolution,[],[f469,f285]) ).
fof(f472,plain,
( ~ subset(sF22,sF24)
| sF22 = sF24
| spl25_13 ),
inference(resolution,[],[f469,f115]) ).
fof(f473,plain,
( ~ subset(sF22,sF24)
| spl25_13 ),
inference(forward_subsumption_resolution,[],[f472,f207]) ).
fof(f474,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| spl25_13 ),
inference(forward_subsumption_resolution,[],[f470,f207]) ).
fof(f475,plain,
( spl25_8
| spl25_13 ),
inference(avatar_split_clause,[],[f474,f433,f401]) ).
fof(f477,plain,
( in(sK4(sF22,sF24),sF24)
| ~ in(sK2(sK19,sF21,sK4(sF22,sF24)),sK17)
| ~ in(sK2(sK19,sF21,sK4(sF22,sF24)),sF20)
| ~ spl25_8 ),
inference(superposition,[],[f353,f403]) ).
fof(f487,definition,
( spl25_19
<=> in(sK2(sK19,sF21,sK4(sF22,sF24)),sF20) ),
introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition]) ).
fof(f489,plain,
( ~ in(sK2(sK19,sF21,sK4(sF22,sF24)),sF20)
| spl25_19 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f496,definition,
( spl25_21
<=> in(sK2(sK19,sF21,sK4(sF22,sF24)),sK17) ),
introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition]) ).
fof(f498,plain,
( ~ in(sK2(sK19,sF21,sK4(sF22,sF24)),sK17)
| spl25_21 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f513,definition,
( spl25_25
<=> in(sK4(sF22,sF24),sF22) ),
introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition]) ).
fof(f514,plain,
( ~ in(sK4(sF22,sF24),sF22)
| spl25_25 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( in(sK4(sF22,sF24),sF22)
| ~ spl25_25 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f518,definition,
( spl25_26
<=> in(sK4(sF22,sF24),sF24) ),
introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition]) ).
fof(f520,plain,
( in(sK4(sF22,sF24),sF24)
| ~ spl25_26 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f522,plain,
( ~ spl25_19
| ~ spl25_21
| spl25_26
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f477,f401,f518,f496,f487]) ).
fof(f548,plain,
( subset(sF22,sF24)
| spl25_25 ),
inference(resolution,[],[f514,f131]) ).
fof(f549,plain,
( $false
| spl25_13
| spl25_25 ),
inference(forward_subsumption_resolution,[],[f548,f473]) ).
fof(f550,plain,
( spl25_13
| spl25_25 ),
inference(avatar_contradiction_clause,[],[f549]) ).
fof(f564,plain,
( subset(sF24,sF22)
| spl25_10 ),
inference(resolution,[],[f421,f233]) ).
fof(f568,plain,
( in(sK2(sK19,sK17,sK4(sF24,sF22)),sF20)
| ~ in(sK4(sF24,sF22),sK18)
| ~ spl25_18 ),
inference(superposition,[],[f461,f198]) ).
fof(f573,plain,
( ~ subset(sF24,sF22)
| sF22 = sF24
| spl25_25 ),
inference(resolution,[],[f548,f115]) ).
fof(f574,plain,
( sF22 = sF24
| spl25_10
| spl25_25 ),
inference(forward_subsumption_resolution,[],[f573,f564]) ).
fof(f575,plain,
( $false
| spl25_10
| spl25_25 ),
inference(forward_subsumption_resolution,[],[f574,f207]) ).
fof(f576,plain,
( spl25_10
| spl25_25 ),
inference(avatar_contradiction_clause,[],[f575]) ).
fof(f577,plain,
( ~ in(sK4(sF24,sF22),sK18)
| spl25_9
| ~ spl25_18 ),
inference(forward_subsumption_resolution,[],[f568,f418]) ).
fof(f578,plain,
( ~ subset(sF24,sF22)
| spl25_25 ),
inference(forward_subsumption_resolution,[],[f573,f207]) ).
fof(f584,plain,
( ~ in(sK2(sK19,sK17,sK4(sF24,sF22)),sK17)
| in(sK2(sK19,sK17,sK4(sF24,sF22)),sF21)
| ~ spl25_9 ),
inference(resolution,[],[f417,f222]) ).
fof(f588,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| ~ relation(sK19)
| ~ function(sK19)
| spl25_11 ),
inference(resolution,[],[f427,f189]) ).
fof(f589,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| ~ function(sK19)
| spl25_11 ),
inference(forward_subsumption_resolution,[],[f588,f172]) ).
fof(f590,plain,
( ~ in(sK4(sF24,sF22),relation_image(sK19,sK17))
| spl25_11 ),
inference(forward_subsumption_resolution,[],[f589,f171]) ).
fof(f591,plain,
( ~ in(sK4(sF24,sF22),sF23)
| spl25_11 ),
inference(forward_demodulation,[],[f590,f204]) ).
fof(f592,plain,
( $false
| spl25_11
| ~ spl25_13 ),
inference(forward_subsumption_resolution,[],[f591,f435]) ).
fof(f593,plain,
( spl25_11
| ~ spl25_13 ),
inference(avatar_contradiction_clause,[],[f592]) ).
fof(f675,plain,
( in(sK2(sK19,sK17,sK4(sF24,sF22)),sF21)
| ~ spl25_9
| ~ spl25_11 ),
inference(forward_subsumption_resolution,[],[f584,f426]) ).
fof(f690,plain,
( subset(sF24,sF22)
| ~ spl25_15 ),
inference(resolution,[],[f444,f132]) ).
fof(f693,plain,
( $false
| ~ spl25_15
| spl25_25 ),
inference(forward_subsumption_resolution,[],[f690,f578]) ).
fof(f694,plain,
( ~ spl25_15
| spl25_25 ),
inference(avatar_contradiction_clause,[],[f693]) ).
fof(f696,plain,
( sK4(sF24,sF22) = apply(sK19,sK2(sK19,sK17,sK4(sF24,sF22)))
| ~ spl25_13 ),
inference(resolution,[],[f435,f212]) ).
fof(f697,plain,
( $false
| spl25_7
| ~ spl25_13 ),
inference(forward_subsumption_resolution,[],[f696,f398]) ).
fof(f698,plain,
( spl25_7
| ~ spl25_13 ),
inference(avatar_contradiction_clause,[],[f697]) ).
fof(f700,plain,
( sK4(sF22,sF24) = apply(sK19,sK2(sK19,sF21,sK4(sF22,sF24)))
| ~ spl25_25 ),
inference(resolution,[],[f515,f213]) ).
fof(f793,plain,
( ~ relation(sK19)
| ~ function(sK19)
| ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_21 ),
inference(resolution,[],[f498,f298]) ).
fof(f794,plain,
( ~ function(sK19)
| ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_21 ),
inference(forward_subsumption_resolution,[],[f793,f172]) ).
fof(f795,plain,
( ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_21 ),
inference(forward_subsumption_resolution,[],[f794,f171]) ).
fof(f796,plain,
( ~ in(sK4(sF22,sF24),sF22)
| spl25_21 ),
inference(forward_demodulation,[],[f795,f202]) ).
fof(f797,plain,
( $false
| spl25_21
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f796,f515]) ).
fof(f798,plain,
( spl25_21
| ~ spl25_25 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f1146,plain,
( ~ relation(sK19)
| ~ function(sK19)
| ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_19 ),
inference(resolution,[],[f297,f489]) ).
fof(f1150,plain,
( ~ function(sK19)
| ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_19 ),
inference(forward_subsumption_resolution,[],[f1146,f172]) ).
fof(f1152,plain,
( ~ in(sK4(sF22,sF24),relation_image(sK19,sF21))
| spl25_19 ),
inference(forward_subsumption_resolution,[],[f1150,f171]) ).
fof(f1154,plain,
( ~ in(sK4(sF22,sF24),sF22)
| spl25_19 ),
inference(forward_demodulation,[],[f1152,f202]) ).
fof(f1156,plain,
( $false
| spl25_19
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f1154,f515]) ).
fof(f1157,plain,
( spl25_19
| ~ spl25_25 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
fof(f1166,plain,
( subset(sF22,sF24)
| ~ spl25_26 ),
inference(resolution,[],[f520,f132]) ).
fof(f1170,plain,
( $false
| spl25_13
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f1166,f473]) ).
fof(f1171,plain,
( spl25_13
| ~ spl25_26 ),
inference(avatar_contradiction_clause,[],[f1170]) ).
fof(f1204,plain,
( in(sK4(sF24,sF22),relation_image(sK19,sF21))
| ~ spl25_14
| ~ spl25_17 ),
inference(resolution,[],[f457,f439]) ).
fof(f1211,plain,
( in(sK4(sF24,sF22),sF22)
| ~ spl25_14
| ~ spl25_17 ),
inference(forward_demodulation,[],[f1204,f202]) ).
fof(f1262,plain,
( ~ subset(sF24,sF22)
| sF22 = sF24
| ~ spl25_26 ),
inference(resolution,[],[f1166,f115]) ).
fof(f1263,plain,
( sF22 = sF24
| ~ spl25_15
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f1262,f690]) ).
fof(f1264,plain,
( $false
| ~ spl25_15
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f1263,f207]) ).
fof(f1265,plain,
( ~ spl25_15
| ~ spl25_26 ),
inference(avatar_contradiction_clause,[],[f1264]) ).
fof(f1266,plain,
( ~ spl25_10
| spl25_9
| ~ spl25_18 ),
inference(avatar_split_clause,[],[f577,f460,f416,f420]) ).
fof(f1267,plain,
( sF22 = sF24
| spl25_10
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f1262,f564]) ).
fof(f1281,plain,
( $false
| spl25_10
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f1267,f207]) ).
fof(f1282,plain,
( spl25_10
| ~ spl25_26 ),
inference(avatar_contradiction_clause,[],[f1281]) ).
fof(f1294,plain,
( spl25_14
| ~ spl25_9
| ~ spl25_11 ),
inference(avatar_split_clause,[],[f675,f425,f416,f438]) ).
fof(f1298,plain,
( spl25_15
| ~ spl25_14
| ~ spl25_17 ),
inference(avatar_split_clause,[],[f1211,f456,f438,f442]) ).
fof(f1302,plain,
( $false
| spl25_8
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f700,f402]) ).
fof(f1303,plain,
( spl25_8
| ~ spl25_25 ),
inference(avatar_contradiction_clause,[],[f1302]) ).
cnf(s3,plain,
( spl25_7
| spl25_8 ),
inference(sat_conversion,[],[f404]) ).
cnf(s6,plain,
( ~ spl25_7
| ~ spl25_12
| ~ spl25_14
| spl25_15 ),
inference(sat_conversion,[],[f445]) ).
cnf(s10,plain,
( ~ spl25_7
| ~ spl25_12
| spl25_17 ),
inference(sat_conversion,[],[f458]) ).
cnf(s11,plain,
( ~ spl25_7
| ~ spl25_12
| spl25_18 ),
inference(sat_conversion,[],[f462]) ).
cnf(s12,plain,
( spl25_12
| ~ spl25_13 ),
inference(sat_conversion,[],[f468]) ).
cnf(s13,plain,
( spl25_8
| spl25_13 ),
inference(sat_conversion,[],[f475]) ).
cnf(s18,plain,
( ~ spl25_8
| ~ spl25_19
| ~ spl25_21
| spl25_26 ),
inference(sat_conversion,[],[f522]) ).
cnf(s23,plain,
( spl25_13
| spl25_25 ),
inference(sat_conversion,[],[f550]) ).
cnf(s25,plain,
( spl25_10
| spl25_25 ),
inference(sat_conversion,[],[f576]) ).
cnf(s27,plain,
( spl25_11
| ~ spl25_13 ),
inference(sat_conversion,[],[f593]) ).
cnf(s38,plain,
( ~ spl25_15
| spl25_25 ),
inference(sat_conversion,[],[f694]) ).
cnf(s39,plain,
( spl25_7
| ~ spl25_13 ),
inference(sat_conversion,[],[f698]) ).
cnf(s45,plain,
( spl25_21
| ~ spl25_25 ),
inference(sat_conversion,[],[f798]) ).
cnf(s71,plain,
( spl25_19
| ~ spl25_25 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s74,plain,
( spl25_13
| ~ spl25_26 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s79,plain,
( ~ spl25_15
| ~ spl25_26 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s80,plain,
( spl25_9
| ~ spl25_10
| ~ spl25_18 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s84,plain,
( spl25_10
| ~ spl25_26 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s87,plain,
( ~ spl25_9
| ~ spl25_11
| spl25_14 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s88,plain,
( ~ spl25_14
| spl25_15
| ~ spl25_17 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s90,plain,
( spl25_8
| ~ spl25_25 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s91,plain,
spl25_7,
inference(rat,[],[s18,s45,s71,s23,s74,s3,s39]) ).
cnf(s92,plain,
( spl25_10
| ~ spl25_8 ),
inference(rat,[],[s18,s45,s71,s25,s84]) ).
cnf(s93,plain,
( spl25_13
| ~ spl25_8 ),
inference(rat,[],[s18,s45,s71,s23,s74]) ).
cnf(s94,plain,
~ spl25_8,
inference(rat,[],[s18,s45,s71,s38,s79,s88,s87,s80,s10,s11,s12,s27,s93,s92,s91]) ).
cnf(s95,plain,
~ spl25_25,
inference(rat,[],[s90,s94]) ).
cnf(s96,plain,
spl25_13,
inference(rat,[],[s13,s94]) ).
cnf(s97,plain,
~ spl25_15,
inference(rat,[],[s38,s95]) ).
cnf(s98,plain,
spl25_10,
inference(rat,[],[s25,s95]) ).
cnf(s99,plain,
spl25_11,
inference(rat,[],[s27,s96]) ).
cnf(s101,plain,
spl25_12,
inference(rat,[],[s12,s96]) ).
cnf(s102,plain,
~ spl25_14,
inference(rat,[],[s6,s101,s91,s97]) ).
cnf(s103,plain,
spl25_18,
inference(rat,[],[s11,s91,s101]) ).
cnf(s105,plain,
~ spl25_9,
inference(rat,[],[s87,s99,s102]) ).
cnf(s106,plain,
$false,
inference(rat,[],[s80,s98,s105,s103]) ).
fof(f1309,plain,
$false,
inference(avatar_sat_refutation,[],[s106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU069+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.42 % Computer : n008.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 28 03:30:54 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.50 Running first-order theorem proving
% 0.20/0.50 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.70/2.28 % (1840938)Detected formulas, will run a generic FOF schedule.
% 8.70/2.28 % (1840943)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=245765159:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.70/2.28 % (1840949)dis-21_1_sil=8000:lcm=predicate:random_seed=872339655:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.70/2.28 % (1840945)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1294301263:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.70/2.28 % (1840944)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=998631759:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.70/2.28 % (1840946)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3616130460:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.70/2.28 % (1840948)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1435996128:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.70/2.28 % (1840947)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4260529055:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.70/2.28 % (1840946)Refutation not found, incomplete strategy
% 8.70/2.28 % (1840946)------------------------------
% 8.70/2.28 % (1840946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840946)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840946)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.28 % (1840946)Time elapsed: 0.003 s
% 8.70/2.28 % (1840946)Peak memory usage: 88 MB
% 8.70/2.28 % (1840946)Instructions burned: 1 (million)
% 8.70/2.28 % (1840949)Instruction limit reached!
% 8.70/2.28 % (1840949)------------------------------
% 8.70/2.28 % (1840949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840949)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840949)Termination reason: Instruction limit
% 8.70/2.28 % (1840949)Termination phase: Saturation
% 8.70/2.28 % (1840949)Time elapsed: 0.119 s
% 8.70/2.28 % (1840949)Peak memory usage: 91 MB
% 8.70/2.28 % (1840949)Instructions burned: 129 (million)
% 8.70/2.28 % (1840947)Instruction limit reached!
% 8.70/2.28 % (1840947)------------------------------
% 8.70/2.28 % (1840947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840947)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840947)Termination reason: Instruction limit
% 8.70/2.28 % (1840947)Termination phase: Saturation
% 8.70/2.28 % (1840947)Time elapsed: 0.117 s
% 8.70/2.28 % (1840947)Peak memory usage: 88 MB
% 8.70/2.28 % (1840947)Instructions burned: 119 (million)
% 8.70/2.28 % (1840948)Instruction limit reached!
% 8.70/2.28 % (1840948)------------------------------
% 8.70/2.28 % (1840948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840948)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840948)Termination reason: Instruction limit
% 8.70/2.28 % (1840948)Termination phase: Saturation
% 8.70/2.28 % (1840948)Time elapsed: 0.147 s
% 8.70/2.28 % (1840948)Peak memory usage: 90 MB
% 8.70/2.28 % (1840948)Instructions burned: 139 (million)
% 8.70/2.28 % (1840957)lrs+10_1_sil=8000:sp=occurrence:random_seed=914371012:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 8.70/2.28 % (1840946)------------------------------
% 8.70/2.28 % (1840946)------------------------------
% 8.70/2.28 % (1840958)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3301904468:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 8.70/2.28 % (1840959)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2461076603:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.70/2.28 % (1840958)Instruction limit reached!
% 8.70/2.28 % (1840958)------------------------------
% 8.70/2.28 % (1840958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840958)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840958)Termination reason: Instruction limit
% 8.70/2.28 % (1840958)Termination phase: Saturation
% 8.70/2.28 % (1840958)Time elapsed: 0.131 s
% 8.70/2.28 % (1840958)Peak memory usage: 90 MB
% 8.70/2.28 % (1840958)Instructions burned: 157 (million)
% 8.70/2.28 % (1840957)Instruction limit reached!
% 8.70/2.28 % (1840957)------------------------------
% 8.70/2.28 % (1840957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840957)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840957)Termination reason: Instruction limit
% 8.70/2.28 % (1840957)Termination phase: Saturation
% 8.70/2.28 % (1840957)Time elapsed: 0.268 s
% 8.70/2.28 % (1840957)Peak memory usage: 91 MB
% 8.70/2.28 % (1840957)Instructions burned: 285 (million)
% 8.70/2.28 % (1840943)First to succeed.
% 8.70/2.28 % (1840943)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1840938"
% 8.70/2.28 % (1840962)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2302163337:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 8.70/2.28 % (1840959)Instruction limit reached!
% 8.70/2.28 % (1840959)------------------------------
% 8.70/2.28 % (1840959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840959)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840959)Termination reason: Instruction limit
% 8.70/2.28 % (1840959)Termination phase: Saturation
% 8.70/2.28 % (1840959)Time elapsed: 0.305 s
% 8.70/2.28 % (1840959)Peak memory usage: 91 MB
% 8.70/2.28 % (1840959)Instructions burned: 325 (million)
% 8.70/2.28 % (1840964)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2942649436:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 8.70/2.28 % (1840964)Refutation not found, incomplete strategy
% 8.70/2.28 % (1840964)------------------------------
% 8.70/2.28 % (1840964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840964)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840964)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.28 % (1840964)Time elapsed: 0.004 s
% 8.70/2.28 % (1840964)Peak memory usage: 88 MB
% 8.70/2.28 % (1840964)Instructions burned: 3 (million)
% 8.70/2.28 % (1840965)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=524414723:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 8.70/2.28 % (1840962)Instruction limit reached!
% 8.70/2.28 % (1840962)------------------------------
% 8.70/2.28 % (1840962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.28 % (1840962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.28 % (1840962)CaDiCaL version: 2.1.3
% 8.70/2.28 % (1840962)Termination reason: Instruction limit
% 8.70/2.28 % (1840962)Termination phase: Saturation
% 8.70/2.28 % (1840962)Time elapsed: 0.236 s
% 8.70/2.28 % (1840962)Peak memory usage: 95 MB
% 8.70/2.28 % (1840962)Instructions burned: 248 (million)
% 8.70/2.28 % (1840943)Refutation found. Thanks to Tanya!
% 8.70/2.28 % SZS status Theorem for theBenchmark
% 8.70/2.28 % SZS output start Proof for theBenchmark
% See solution above
% 9.64/2.52 % (1840943)------------------------------
% 9.64/2.52 % (1840943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.52 % (1840943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.52 % (1840943)CaDiCaL version: 2.1.3
% 9.64/2.52 % (1840943)Termination reason: Refutation
% 9.64/2.52 % (1840943)Time elapsed: 0.721 s
% 9.64/2.52 % (1840943)Peak memory usage: 131 MB
% 9.64/2.52 % (1840943)Instructions burned: 1102 (million)
% 9.64/2.52 % (1840943)------------------------------
% 9.64/2.52 % (1840943)------------------------------
% 9.64/2.52 % (1840938)Success in time 1.259 s
% 9.64/2.52 % Vampire exiting
%------------------------------------------------------------------------------