%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU222+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:50 PM UTC 2026
% Result : Theorem 40.01s 10.20s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 40
% Syntax : Number of formulae : 394 ( 51 unt; 20 def)
% Number of atoms : 1589 ( 316 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 2002 ( 807 ~; 968 |; 160 &)
% ( 42 <=>; 23 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 12 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 12 con; 0-3 aty)
% Number of variables : 536 ( 0 sgn 492 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f8,axiom,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f11,axiom,
! [X0] :
( relation(X0)
=> ! [X1,X2] :
( relation(X2)
=> ( X2 = relation_dom_restriction(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_relat_1) ).
fof(f20,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ( X0 = X1
<=> ! [X2,X3] :
( in(ordered_pair(X2,X3),X0)
<=> in(ordered_pair(X2,X3),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_relat_1) ).
fof(f26,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f27,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(f28,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f29,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f32,axiom,
! [X0,X1,X2] :
( X2 = set_difference(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& ~ in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f35,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(f69,axiom,
! [X0,X1] :
( relation(X0)
=> relation(relation_dom_restriction(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f91,axiom,
! [X0,X1] :
( ( relation(X0)
& function(X0) )
=> ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_funct_1) ).
fof(f159,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(ordered_pair(X0,X1),X2)
=> ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_relat_1) ).
fof(f198,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f216,conjecture,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( X1 = relation_dom_restriction(X2,X0)
<=> ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( in(X3,relation_dom(X1))
=> apply(X1,X3) = apply(X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t68_funct_1) ).
fof(f217,negated_conjecture,
~ ! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( X1 = relation_dom_restriction(X2,X0)
<=> ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( in(X3,relation_dom(X1))
=> apply(X1,X3) = apply(X2,X3) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f216]) ).
fof(f218,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f226,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
<=> ( in(X0,X1)
& in(X0,relation_dom(X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t86_relat_1) ).
fof(f227,axiom,
! [X0,X1] :
( relation(X1)
=> subset(relation_dom_restriction(X1,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t88_relat_1) ).
fof(f229,axiom,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f232,axiom,
! [X0,X1] :
( relation(X1)
=> relation_dom(relation_dom_restriction(X1,X0)) = set_intersection2(relation_dom(X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t90_relat_1) ).
fof(f257,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_dom_restriction(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) ) ) )
| ~ relation(X2) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f263,plain,
! [X0] :
( ! [X1] :
( ( X0 = X1
<=> ! [X2,X3] :
( in(ordered_pair(X2,X3),X0)
<=> in(ordered_pair(X2,X3),X1) ) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f266,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f267,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f268,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f267]) ).
fof(f269,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f292,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f310,plain,
! [X0,X1] :
( ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f311,plain,
! [X0,X1] :
( ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f310]) ).
fof(f368,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(ennf_transformation,[],[f159]) ).
fof(f369,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(flattening,[],[f368]) ).
fof(f433,plain,
? [X0,X1] :
( ? [X2] :
( ( X1 = relation_dom_restriction(X2,X0)
<~> ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( apply(X1,X3) = apply(X2,X3)
| ~ in(X3,relation_dom(X1)) ) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(ennf_transformation,[],[f217]) ).
fof(f434,plain,
? [X0,X1] :
( ? [X2] :
( ( X1 = relation_dom_restriction(X2,X0)
<~> ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( apply(X1,X3) = apply(X2,X3)
| ~ in(X3,relation_dom(X1)) ) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f433]) ).
fof(f439,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
<=> ( in(X0,X1)
& in(X0,relation_dom(X2)) ) )
| ~ relation(X2) ),
inference(ennf_transformation,[],[f226]) ).
fof(f440,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f227]) ).
fof(f442,plain,
! [X0,X1,X2] :
( ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f229]) ).
fof(f443,plain,
! [X0,X1,X2] :
( ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f442]) ).
fof(f447,plain,
! [X0,X1] :
( relation_dom(relation_dom_restriction(X1,X0)) = set_intersection2(relation_dom(X1),X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f232]) ).
fof(f462,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = relation_dom_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X3,X1)
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X3,X1)
| ~ in(ordered_pair(X3,X4),X0) )
& ( ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) )
| ~ in(ordered_pair(X3,X4),X2) ) )
| relation_dom_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f257]) ).
fof(f463,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = relation_dom_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X3,X1)
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X3,X1)
| ~ in(ordered_pair(X3,X4),X0) )
& ( ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) )
| ~ in(ordered_pair(X3,X4),X2) ) )
| relation_dom_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X0) ),
inference(flattening,[],[f462]) ).
fof(f464,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = relation_dom_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X3,X1)
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X3,X1)
& in(ordered_pair(X3,X4),X0) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X5,X6] :
( ( in(ordered_pair(X5,X6),X2)
| ~ in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0) )
& ( ( in(X5,X1)
& in(ordered_pair(X5,X6),X0) )
| ~ in(ordered_pair(X5,X6),X2) ) )
| relation_dom_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X0) ),
inference(rectify,[],[f463]) ).
fof(f465,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = relation_dom_restriction(X0,X1)
| ( ( ~ in(sK3(X0,X1,X2),X1)
| ~ in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X0)
| ~ in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2) )
& ( ( in(sK3(X0,X1,X2),X1)
& in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X0) )
| in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2) ) ) )
& ( ! [X5,X6] :
( ( in(ordered_pair(X5,X6),X2)
| ~ in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0) )
& ( ( in(X5,X1)
& in(ordered_pair(X5,X6),X0) )
| ~ in(ordered_pair(X5,X6),X2) ) )
| relation_dom_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X3,sK3(X0,X1,X2)),skolemize(X4,sK4(X0,X1,X2))],[f464]) ).
fof(f491,plain,
! [X0] :
( ! [X1] :
( ( ( X0 = X1
| ? [X2,X3] :
( ( ~ in(ordered_pair(X2,X3),X1)
| ~ in(ordered_pair(X2,X3),X0) )
& ( in(ordered_pair(X2,X3),X1)
| in(ordered_pair(X2,X3),X0) ) ) )
& ( ! [X2,X3] :
( ( in(ordered_pair(X2,X3),X0)
| ~ in(ordered_pair(X2,X3),X1) )
& ( in(ordered_pair(X2,X3),X1)
| ~ in(ordered_pair(X2,X3),X0) ) )
| X0 != X1 ) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f263]) ).
fof(f492,plain,
! [X0] :
( ! [X1] :
( ( ( X0 = X1
| ? [X2,X3] :
( ( ~ in(ordered_pair(X2,X3),X1)
| ~ in(ordered_pair(X2,X3),X0) )
& ( in(ordered_pair(X2,X3),X1)
| in(ordered_pair(X2,X3),X0) ) ) )
& ( ! [X4,X5] :
( ( in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X4,X5),X1) )
& ( in(ordered_pair(X4,X5),X1)
| ~ in(ordered_pair(X4,X5),X0) ) )
| X0 != X1 ) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(rectify,[],[f491]) ).
fof(f493,plain,
! [X0] :
( ! [X1] :
( ( ( X0 = X1
| ( ( ~ in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X1)
| ~ in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X0) )
& ( in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X1)
| in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X0) ) ) )
& ( ! [X4,X5] :
( ( in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X4,X5),X1) )
& ( in(ordered_pair(X4,X5),X1)
| ~ in(ordered_pair(X4,X5),X0) ) )
| X0 != X1 ) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23]),skolemize(X2,sK22(X0,X1)),skolemize(X3,sK23(X0,X1))],[f492]) ).
fof(f509,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,[],[f266]) ).
fof(f510,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,[],[f509]) ).
fof(f511,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK33(X0,X1),X1)
& in(sK33(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X2,sK33(X0,X1))],[f510]) ).
fof(f512,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,[],[f27]) ).
fof(f513,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,[],[f512]) ).
fof(f514,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,[],[f513]) ).
fof(f515,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ( ( ~ in(sK34(X0,X1,X2),X0)
| ~ in(sK34(X0,X1,X2),X1)
| ~ in(sK34(X0,X1,X2),X2) )
& ( ( in(sK34(X0,X1,X2),X0)
& in(sK34(X0,X1,X2),X1) )
| in(sK34(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,[sK34]),skolemize(X3,sK34(X0,X1,X2))],[f514]) ).
fof(f516,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0) )
& ( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ) )
| ~ in(X1,relation_dom(X0)) )
& ( ( ( X2 = apply(X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| apply(X0,X1) != X2 ) )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f268]) ).
fof(f517,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] : ~ in(ordered_pair(X2,X3),X0) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f269]) ).
fof(f518,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X4] : in(ordered_pair(X2,X4),X0)
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( ? [X7] : in(ordered_pair(X5,X7),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(rectify,[],[f517]) ).
fof(f519,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ( ( ! [X3] : ~ in(ordered_pair(sK35(X0,X1),X3),X0)
| ~ in(sK35(X0,X1),X1) )
& ( in(ordered_pair(sK35(X0,X1),sK36(X0,X1)),X0)
| in(sK35(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( in(ordered_pair(X5,sK37(X0,X5)),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36,sK37]),skolemize(X2,sK35(X0,X1)),skolemize(X4,sK36(X0,X1)),skolemize(X7,sK37(X0,X5))],[f518]) ).
fof(f523,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(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_difference(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f524,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(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_difference(X0,X1) != X2 ) ),
inference(flattening,[],[f523]) ).
fof(f525,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(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_difference(X0,X1) != X2 ) ),
inference(rectify,[],[f524]) ).
fof(f526,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ( ( ~ in(sK41(X0,X1,X2),X0)
| in(sK41(X0,X1,X2),X1)
| ~ in(sK41(X0,X1,X2),X2) )
& ( ( in(sK41(X0,X1,X2),X0)
& ~ in(sK41(X0,X1,X2),X1) )
| in(sK41(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1) )
& ( ( in(X4,X0)
& ~ in(X4,X1) )
| ~ in(X4,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X3,sK41(X0,X1,X2))],[f525]) ).
fof(f601,plain,
? [X0,X1] :
( ? [X2] :
( ( relation_dom(X1) != set_intersection2(relation_dom(X2),X0)
| ? [X3] :
( apply(X1,X3) != apply(X2,X3)
& in(X3,relation_dom(X1)) )
| relation_dom_restriction(X2,X0) != X1 )
& ( ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( apply(X1,X3) = apply(X2,X3)
| ~ in(X3,relation_dom(X1)) ) )
| X1 = relation_dom_restriction(X2,X0) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(nnf_transformation,[],[f434]) ).
fof(f602,plain,
? [X0,X1] :
( ? [X2] :
( ( relation_dom(X1) != set_intersection2(relation_dom(X2),X0)
| ? [X3] :
( apply(X1,X3) != apply(X2,X3)
& in(X3,relation_dom(X1)) )
| relation_dom_restriction(X2,X0) != X1 )
& ( ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X3] :
( apply(X1,X3) = apply(X2,X3)
| ~ in(X3,relation_dom(X1)) ) )
| X1 = relation_dom_restriction(X2,X0) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f601]) ).
fof(f603,plain,
? [X0,X1] :
( ? [X2] :
( ( relation_dom(X1) != set_intersection2(relation_dom(X2),X0)
| ? [X3] :
( apply(X1,X3) != apply(X2,X3)
& in(X3,relation_dom(X1)) )
| relation_dom_restriction(X2,X0) != X1 )
& ( ( relation_dom(X1) = set_intersection2(relation_dom(X2),X0)
& ! [X4] :
( apply(X1,X4) = apply(X2,X4)
| ~ in(X4,relation_dom(X1)) ) )
| X1 = relation_dom_restriction(X2,X0) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(rectify,[],[f602]) ).
fof(f604,plain,
( ( relation_dom(sK78) != set_intersection2(relation_dom(sK79),sK77)
| ( apply(sK78,sK80) != apply(sK79,sK80)
& in(sK80,relation_dom(sK78)) )
| sK78 != relation_dom_restriction(sK79,sK77) )
& ( ( relation_dom(sK78) = set_intersection2(relation_dom(sK79),sK77)
& ! [X4] :
( apply(sK78,X4) = apply(sK79,X4)
| ~ in(X4,relation_dom(sK78)) ) )
| sK78 = relation_dom_restriction(sK79,sK77) )
& relation(sK79)
& function(sK79)
& relation(sK78)
& function(sK78) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77,sK78,sK79,sK80]),skolemize(X0,sK77),skolemize(X1,sK78),skolemize(X2,sK79),skolemize(X3,sK80)],[f603]) ).
fof(f608,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| ~ in(X0,X1)
| ~ in(X0,relation_dom(X2)) )
& ( ( in(X0,X1)
& in(X0,relation_dom(X2)) )
| ~ in(X0,relation_dom(relation_dom_restriction(X2,X1))) ) )
| ~ relation(X2) ),
inference(nnf_transformation,[],[f439]) ).
fof(f609,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| ~ in(X0,X1)
| ~ in(X0,relation_dom(X2)) )
& ( ( in(X0,X1)
& in(X0,relation_dom(X2)) )
| ~ in(X0,relation_dom(relation_dom_restriction(X2,X1))) ) )
| ~ relation(X2) ),
inference(flattening,[],[f608]) ).
fof(f610,plain,
! [X0,X1,X2] :
( ( ( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1 )
& ( ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) )
| ~ in(ordered_pair(X0,X1),X2) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(nnf_transformation,[],[f443]) ).
fof(f611,plain,
! [X0,X1,X2] :
( ( ( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1 )
& ( ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) )
| ~ in(ordered_pair(X0,X1),X2) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f610]) ).
fof(f620,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f6]) ).
fof(f622,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[],[f8]) ).
fof(f632,plain,
! [X2,X0,X1,X6,X5] :
( in(ordered_pair(X5,X6),X0)
| ~ in(ordered_pair(X5,X6),X2)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f465]) ).
fof(f633,plain,
! [X2,X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(ordered_pair(X5,X6),X2)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f465]) ).
fof(f634,plain,
! [X2,X0,X1,X6,X5] :
( in(ordered_pair(X5,X6),X2)
| ~ in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f465]) ).
fof(f679,plain,
! [X0,X1] :
( X0 = X1
| in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X1)
| in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f493]) ).
fof(f680,plain,
! [X0,X1] :
( X0 = X1
| ~ in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X1)
| ~ in(ordered_pair(sK22(X0,X1),sK23(X0,X1)),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f493]) ).
fof(f708,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f511]) ).
fof(f711,plain,
! [X2,X0,X1,X4] :
( in(X4,X1)
| ~ in(X4,X2)
| set_intersection2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f515]) ).
fof(f717,plain,
! [X2,X0,X1] :
( empty_set = X2
| apply(X0,X1) != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f516]) ).
fof(f721,plain,
! [X0,X1,X5] :
( in(ordered_pair(X5,sK37(X0,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f519]) ).
fof(f732,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,X1)
| ~ in(X4,X2)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f526]) ).
fof(f733,plain,
! [X2,X0,X1,X4] :
( in(X4,X0)
| ~ in(X4,X2)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f526]) ).
fof(f734,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f526]) ).
fof(f743,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f779,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f292]) ).
fof(f807,plain,
! [X0,X1] :
( function(relation_dom_restriction(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f311]) ).
fof(f808,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f311]) ).
fof(f911,plain,
! [X2,X0,X1] :
( in(X0,relation_dom(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f369]) ).
fof(f970,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f198]) ).
fof(f1006,plain,
function(sK78),
inference(cnf_transformation,[],[f604]) ).
fof(f1007,plain,
relation(sK78),
inference(cnf_transformation,[],[f604]) ).
fof(f1008,plain,
function(sK79),
inference(cnf_transformation,[],[f604]) ).
fof(f1009,plain,
relation(sK79),
inference(cnf_transformation,[],[f604]) ).
fof(f1010,plain,
! [X4] :
( apply(sK78,X4) = apply(sK79,X4)
| ~ in(X4,relation_dom(sK78))
| sK78 = relation_dom_restriction(sK79,sK77) ),
inference(cnf_transformation,[],[f604]) ).
fof(f1011,plain,
( relation_dom(sK78) = set_intersection2(relation_dom(sK79),sK77)
| sK78 = relation_dom_restriction(sK79,sK77) ),
inference(cnf_transformation,[],[f604]) ).
fof(f1012,plain,
( relation_dom(sK78) != set_intersection2(relation_dom(sK79),sK77)
| in(sK80,relation_dom(sK78))
| sK78 != relation_dom_restriction(sK79,sK77) ),
inference(cnf_transformation,[],[f604]) ).
fof(f1013,plain,
( relation_dom(sK78) != set_intersection2(relation_dom(sK79),sK77)
| apply(sK78,sK80) != apply(sK79,sK80)
| sK78 != relation_dom_restriction(sK79,sK77) ),
inference(cnf_transformation,[],[f604]) ).
fof(f1014,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f218]) ).
fof(f1027,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| in(X0,X1)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f609]) ).
fof(f1029,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f440]) ).
fof(f1031,plain,
! [X2,X0,X1] :
( apply(X2,X0) = X1
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f611]) ).
fof(f1033,plain,
! [X2,X0,X1] :
( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f611]) ).
fof(f1036,plain,
! [X0,X1] :
( set_intersection2(relation_dom(X1),X0) = relation_dom(relation_dom_restriction(X1,X0))
| ~ relation(X1) ),
inference(cnf_transformation,[],[f447]) ).
fof(f1046,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f743,f1014]) ).
fof(f1047,plain,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_difference(X1,set_difference(X1,X0)),
inference(definition_unfolding,[],[f622,f970,f970]) ).
fof(f1057,plain,
! [X2,X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X2)
| ~ in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f634,f1046,f1046]) ).
fof(f1058,plain,
! [X2,X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X2)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f633,f1046]) ).
fof(f1059,plain,
! [X2,X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X2)
| relation_dom_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f632,f1046,f1046]) ).
fof(f1080,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X1)
| X0 = X1
| ~ in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f680,f1046,f1046]) ).
fof(f1081,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X1)
| in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X0)
| X0 = X1
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f679,f1046,f1046]) ).
fof(f1096,plain,
! [X2,X0,X1,X4] :
( in(X4,X1)
| ~ in(X4,X2)
| set_difference(X0,set_difference(X0,X1)) != X2 ),
inference(definition_unfolding,[],[f711,f970]) ).
fof(f1102,plain,
! [X0,X1,X5] :
( in(unordered_pair(unordered_pair(X5,sK37(X0,X5)),unordered_pair(X5,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f721,f1046]) ).
fof(f1148,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| in(X0,relation_dom(X2))
| ~ relation(X2) ),
inference(definition_unfolding,[],[f911,f1046]) ).
fof(f1168,plain,
( relation_dom(sK78) != set_difference(relation_dom(sK79),set_difference(relation_dom(sK79),sK77))
| apply(sK78,sK80) != apply(sK79,sK80)
| sK78 != relation_dom_restriction(sK79,sK77) ),
inference(definition_unfolding,[],[f1013,f970]) ).
fof(f1169,plain,
( relation_dom(sK78) != set_difference(relation_dom(sK79),set_difference(relation_dom(sK79),sK77))
| in(sK80,relation_dom(sK78))
| sK78 != relation_dom_restriction(sK79,sK77) ),
inference(definition_unfolding,[],[f1012,f970]) ).
fof(f1170,plain,
( relation_dom(sK78) = set_difference(relation_dom(sK79),set_difference(relation_dom(sK79),sK77))
| sK78 = relation_dom_restriction(sK79,sK77) ),
inference(definition_unfolding,[],[f1011,f970]) ).
fof(f1175,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f1033,f1046]) ).
fof(f1177,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| apply(X2,X0) = X1
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f1031,f1046]) ).
fof(f1179,plain,
! [X0,X1] :
( ~ relation(X1)
| relation_dom(relation_dom_restriction(X1,X0)) = set_difference(relation_dom(X1),set_difference(relation_dom(X1),X0)) ),
inference(definition_unfolding,[],[f1036,f970]) ).
fof(f1187,plain,
! [X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| ~ in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| ~ relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(equality_resolution,[],[f1057]) ).
fof(f1188,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| ~ relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(equality_resolution,[],[f1058]) ).
fof(f1189,plain,
! [X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| ~ relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(equality_resolution,[],[f1059]) ).
fof(f1229,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,set_difference(X0,X1)))
| in(X4,X1) ),
inference(equality_resolution,[],[f1096]) ).
fof(f1232,plain,
! [X0,X1] :
( in(X1,relation_dom(X0))
| empty_set = apply(X0,X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f717]) ).
fof(f1234,plain,
! [X0,X5] :
( in(unordered_pair(unordered_pair(X5,sK37(X0,X5)),unordered_pair(X5,X5)),X0)
| ~ in(X5,relation_dom(X0))
| ~ relation(X0) ),
inference(equality_resolution,[],[f1102]) ).
fof(f1238,plain,
! [X0,X1,X4] :
( in(X4,set_difference(X0,X1))
| ~ in(X4,X0)
| in(X4,X1) ),
inference(equality_resolution,[],[f734]) ).
fof(f1239,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,X1))
| in(X4,X0) ),
inference(equality_resolution,[],[f733]) ).
fof(f1240,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,X1))
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f732]) ).
fof(f1267,plain,
! [X2,X0] :
( in(unordered_pair(unordered_pair(X0,apply(X2,X0)),unordered_pair(X0,X0)),X2)
| ~ in(X0,relation_dom(X2))
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f1175]) ).
fof(f1268,definition,
sF83 = relation_dom(sK78),
introduced(definition,[new_symbols(definition,[sF83])],[function_definition]) ).
fof(f1269,plain,
relation_dom(sK78) = sF83,
inference(reorient_equations,[],[f1268]) ).
fof(f1270,definition,
sF84 = relation_dom(sK79),
introduced(definition,[new_symbols(definition,[sF84])],[function_definition]) ).
fof(f1271,plain,
relation_dom(sK79) = sF84,
inference(reorient_equations,[],[f1270]) ).
fof(f1272,definition,
sF85 = set_difference(sF84,sK77),
introduced(definition,[new_symbols(definition,[sF85])],[function_definition]) ).
fof(f1273,plain,
set_difference(sF84,sK77) = sF85,
inference(reorient_equations,[],[f1272]) ).
fof(f1274,definition,
sF86 = set_difference(sF84,sF85),
introduced(definition,[new_symbols(definition,[sF86])],[function_definition]) ).
fof(f1275,plain,
set_difference(sF84,sF85) = sF86,
inference(reorient_equations,[],[f1274]) ).
fof(f1276,definition,
sF87 = apply(sK78,sK80),
introduced(definition,[new_symbols(definition,[sF87])],[function_definition]) ).
fof(f1277,plain,
apply(sK78,sK80) = sF87,
inference(reorient_equations,[],[f1276]) ).
fof(f1278,definition,
sF88 = apply(sK79,sK80),
introduced(definition,[new_symbols(definition,[sF88])],[function_definition]) ).
fof(f1279,plain,
apply(sK79,sK80) = sF88,
inference(reorient_equations,[],[f1278]) ).
fof(f1280,definition,
sF89 = relation_dom_restriction(sK79,sK77),
introduced(definition,[new_symbols(definition,[sF89])],[function_definition]) ).
fof(f1281,plain,
relation_dom_restriction(sK79,sK77) = sF89,
inference(reorient_equations,[],[f1280]) ).
fof(f1282,plain,
( sF83 != sF86
| sF87 != sF88
| sK78 != sF89 ),
inference(definition_folding,[],[f1168,f1281,f1279,f1277,f1275,f1273,f1271,f1271,f1269]) ).
fof(f1283,plain,
( sF83 != sF86
| in(sK80,sF83)
| sK78 != sF89 ),
inference(definition_folding,[],[f1169,f1281,f1269,f1275,f1273,f1271,f1271,f1269]) ).
fof(f1284,plain,
( sF83 = sF86
| sK78 = sF89 ),
inference(definition_folding,[],[f1170,f1281,f1275,f1273,f1271,f1271,f1269]) ).
fof(f1285,definition,
! [X4] : sF90(X4) = apply(sK78,X4),
introduced(definition,[new_symbols(definition,[sF90])],[function_definition]) ).
fof(f1286,plain,
! [X4] : apply(sK78,X4) = sF90(X4),
inference(reorient_equations,[],[f1285]) ).
fof(f1287,definition,
! [X4] : sF91(X4) = apply(sK79,X4),
introduced(definition,[new_symbols(definition,[sF91])],[function_definition]) ).
fof(f1288,plain,
! [X4] : apply(sK79,X4) = sF91(X4),
inference(reorient_equations,[],[f1287]) ).
fof(f1289,plain,
! [X4] :
( sF90(X4) = sF91(X4)
| ~ in(X4,sF83)
| sK78 = sF89 ),
inference(definition_folding,[],[f1010,f1281,f1269,f1288,f1286]) ).
fof(f1293,definition,
( spl92_1
<=> sK78 = sF89 ),
introduced(definition,[new_symbols(definition,[spl92_1])],[avatar_definition]) ).
fof(f1294,plain,
( sK78 != sF89
| spl92_1 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1295,plain,
( sK78 = sF89
| ~ spl92_1 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1297,definition,
( spl92_2
<=> ! [X4] :
( sF90(X4) = sF91(X4)
| ~ in(X4,sF83) ) ),
introduced(definition,[new_symbols(definition,[spl92_2])],[avatar_definition]) ).
fof(f1298,plain,
( ! [X4] :
( ~ in(X4,sF83)
| sF90(X4) = sF91(X4) )
| ~ spl92_2 ),
inference(avatar_component_clause,[],[f1297]) ).
fof(f1299,plain,
( spl92_1
| spl92_2 ),
inference(avatar_split_clause,[],[f1289,f1297,f1293]) ).
fof(f1301,definition,
( spl92_3
<=> sF83 = sF86 ),
introduced(definition,[new_symbols(definition,[spl92_3])],[avatar_definition]) ).
fof(f1302,plain,
( sF83 != sF86
| spl92_3 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1303,plain,
( sF83 = sF86
| ~ spl92_3 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1304,plain,
( spl92_1
| spl92_3 ),
inference(avatar_split_clause,[],[f1284,f1301,f1293]) ).
fof(f1306,definition,
( spl92_4
<=> in(sK80,sF83) ),
introduced(definition,[new_symbols(definition,[spl92_4])],[avatar_definition]) ).
fof(f1308,plain,
( in(sK80,sF83)
| ~ spl92_4 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1309,plain,
( ~ spl92_1
| spl92_4
| ~ spl92_3 ),
inference(avatar_split_clause,[],[f1283,f1301,f1306,f1293]) ).
fof(f1311,definition,
( spl92_5
<=> sF87 = sF88 ),
introduced(definition,[new_symbols(definition,[spl92_5])],[avatar_definition]) ).
fof(f1314,plain,
( ~ spl92_1
| ~ spl92_5
| ~ spl92_3 ),
inference(avatar_split_clause,[],[f1282,f1301,f1311,f1293]) ).
fof(f1328,plain,
! [X0,X1,X6,X5] :
( ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1189,f779]) ).
fof(f1329,plain,
! [X0,X1,X6,X5] :
( ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| in(X5,X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1188,f779]) ).
fof(f1330,plain,
! [X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_dom_restriction(X0,X1))
| ~ in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1187,f779]) ).
fof(f1336,plain,
sF87 = sF90(sK80),
inference(superposition,[],[f1277,f1286]) ).
fof(f1338,plain,
sF88 = sF91(sK80),
inference(superposition,[],[f1279,f1288]) ).
fof(f1339,plain,
! [X0] : relation_dom(relation_dom_restriction(sK79,X0)) = set_difference(relation_dom(sK79),set_difference(relation_dom(sK79),X0)),
inference(resolution,[],[f1009,f1179]) ).
fof(f1340,plain,
! [X0] : relation_dom(relation_dom_restriction(sK79,X0)) = set_difference(sF84,set_difference(sF84,X0)),
inference(forward_demodulation,[],[f1339,f1271]) ).
fof(f1342,plain,
set_difference(sF84,sF85) = relation_dom(relation_dom_restriction(sK79,sK77)),
inference(superposition,[],[f1340,f1273]) ).
fof(f1344,plain,
set_difference(sF84,sF85) = relation_dom(sF89),
inference(forward_demodulation,[],[f1342,f1281]) ).
fof(f1346,plain,
sF86 = relation_dom(sF89),
inference(forward_demodulation,[],[f1344,f1275]) ).
fof(f1354,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| in(X0,sK77)
| ~ relation(sK79) ),
inference(superposition,[],[f1027,f1281]) ).
fof(f1355,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| in(X0,sK77) ),
inference(forward_subsumption_resolution,[],[f1354,f1009]) ).
fof(f1375,plain,
! [X0] :
( ~ in(X0,sF86)
| in(X0,sF84) ),
inference(superposition,[],[f1239,f1275]) ).
fof(f1377,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(relation_dom_restriction(sK79,X0)))
| in(X1,sF84) ),
inference(superposition,[],[f1239,f1340]) ).
fof(f1381,plain,
( function(sF89)
| ~ relation(sK79)
| ~ function(sK79) ),
inference(superposition,[],[f807,f1281]) ).
fof(f1382,plain,
( function(sF89)
| ~ function(sK79) ),
inference(forward_subsumption_resolution,[],[f1381,f1009]) ).
fof(f1383,plain,
function(sF89),
inference(forward_subsumption_resolution,[],[f1382,f1008]) ).
fof(f1385,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| in(X0,sF84) ),
inference(superposition,[],[f1377,f1281]) ).
fof(f1399,plain,
( relation(sF89)
| ~ relation(sK79)
| ~ function(sK79) ),
inference(superposition,[],[f808,f1281]) ).
fof(f1400,plain,
( relation(sF89)
| ~ function(sK79) ),
inference(forward_subsumption_resolution,[],[f1399,f1009]) ).
fof(f1401,plain,
relation(sF89),
inference(forward_subsumption_resolution,[],[f1400,f1008]) ).
fof(f1421,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK78)
| ~ in(X0,relation_dom(sK78))
| ~ relation(sK78)
| ~ function(sK78) ),
inference(superposition,[],[f1267,f1286]) ).
fof(f1422,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sK79))
| ~ relation(sK79)
| ~ function(sK79) ),
inference(superposition,[],[f1267,f1288]) ).
fof(f1423,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sK79))
| ~ function(sK79) ),
inference(forward_subsumption_resolution,[],[f1422,f1009]) ).
fof(f1424,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK78)
| ~ in(X0,relation_dom(sK78))
| ~ function(sK78) ),
inference(forward_subsumption_resolution,[],[f1421,f1007]) ).
fof(f1475,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sK79)) ),
inference(forward_subsumption_resolution,[],[f1423,f1008]) ).
fof(f1476,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK78)
| ~ in(X0,relation_dom(sK78)) ),
inference(forward_subsumption_resolution,[],[f1424,f1006]) ).
fof(f1479,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,sF84) ),
inference(forward_demodulation,[],[f1475,f1271]) ).
fof(f1480,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK78)
| ~ in(X0,sF83) ),
inference(forward_demodulation,[],[f1476,f1269]) ).
fof(f1499,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89)
| in(X0,sK77)
| ~ relation(sK79) ),
inference(superposition,[],[f1329,f1281]) ).
fof(f1500,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89)
| in(X0,sK77) ),
inference(forward_subsumption_resolution,[],[f1499,f1009]) ).
fof(f1513,plain,
! [X0] :
( in(X0,sF83)
| empty_set = apply(sK78,X0)
| ~ relation(sK78)
| ~ function(sK78) ),
inference(superposition,[],[f1232,f1269]) ).
fof(f1516,plain,
! [X0] :
( in(X0,sF83)
| empty_set = apply(sK78,X0)
| ~ function(sK78) ),
inference(forward_subsumption_resolution,[],[f1513,f1007]) ).
fof(f1521,plain,
! [X0] :
( in(X0,sF83)
| empty_set = apply(sK78,X0) ),
inference(forward_subsumption_resolution,[],[f1516,f1006]) ).
fof(f1523,plain,
! [X0] :
( in(X0,sF83)
| empty_set = sF90(X0) ),
inference(forward_demodulation,[],[f1521,f1286]) ).
fof(f1572,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK79)
| ~ relation(sK79) ),
inference(superposition,[],[f1328,f1281]) ).
fof(f1573,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK79) ),
inference(forward_subsumption_resolution,[],[f1572,f1009]) ).
fof(f1575,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sF89))
| ~ relation(sF89)
| ~ function(sF89) ),
inference(resolution,[],[f1573,f1267]) ).
fof(f1580,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sF89))
| ~ function(sF89) ),
inference(forward_subsumption_resolution,[],[f1575,f1401]) ).
fof(f1581,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sF89)) ),
inference(forward_subsumption_resolution,[],[f1580,f1383]) ).
fof(f1628,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sK37(X1,X0))),X1)
| ~ in(X0,relation_dom(X1))
| ~ relation(X1) ),
inference(superposition,[],[f1234,f620]) ).
fof(f1714,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sK77)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK79)
| ~ relation(sK79) ),
inference(superposition,[],[f1330,f1281]) ).
fof(f1717,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK79)
| ~ in(X0,sK77)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF89) ),
inference(forward_subsumption_resolution,[],[f1714,f1009]) ).
fof(f1721,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sK77)
| ~ in(X0,sF84) ),
inference(resolution,[],[f1717,f1479]) ).
fof(f1817,plain,
! [X2,X0,X1] :
( in(X2,set_difference(X0,set_difference(X0,X1)))
| ~ in(X2,X1)
| in(X2,set_difference(X1,X0)) ),
inference(superposition,[],[f1238,f1047]) ).
fof(f1872,plain,
! [X0] :
( in(X0,set_difference(sF84,sF85))
| ~ in(X0,sK77)
| in(X0,set_difference(sK77,sF84)) ),
inference(superposition,[],[f1817,f1273]) ).
fof(f1883,plain,
! [X0] :
( in(X0,set_difference(sK77,sF84))
| ~ in(X0,sK77)
| in(X0,sF86) ),
inference(forward_demodulation,[],[f1872,f1275]) ).
fof(f2018,plain,
( relation_dom(sK78) = sF86
| ~ spl92_1 ),
inference(forward_demodulation,[],[f1346,f1295]) ).
fof(f2026,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sK78,X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sF89)) )
| ~ spl92_1 ),
inference(forward_demodulation,[],[f1581,f1295]) ).
fof(f2033,plain,
( sF83 = sF86
| ~ spl92_1 ),
inference(forward_demodulation,[],[f2018,f1269]) ).
fof(f2041,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,relation_dom(sF89)) )
| ~ spl92_1 ),
inference(forward_demodulation,[],[f2026,f1286]) ).
fof(f2048,plain,
( $false
| ~ spl92_1
| spl92_3 ),
inference(forward_subsumption_resolution,[],[f2033,f1302]) ).
fof(f2049,plain,
( ~ spl92_1
| spl92_3 ),
inference(avatar_contradiction_clause,[],[f2048]) ).
fof(f2053,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK78))
| in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK79) )
| ~ spl92_1 ),
inference(forward_demodulation,[],[f2041,f1295]) ).
fof(f2056,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sK79)
| ~ in(X0,sF83) )
| ~ spl92_1 ),
inference(forward_demodulation,[],[f2053,f1269]) ).
fof(f2072,plain,
( sF90(sK80) = sF91(sK80)
| ~ spl92_2
| ~ spl92_4 ),
inference(resolution,[],[f1308,f1298]) ).
fof(f2073,plain,
( sF88 = sF90(sK80)
| ~ spl92_2
| ~ spl92_4 ),
inference(forward_demodulation,[],[f2072,f1338]) ).
fof(f2076,plain,
( sF87 = sF88
| ~ spl92_2
| ~ spl92_4 ),
inference(forward_demodulation,[],[f2073,f1336]) ).
fof(f2103,plain,
! [X0] :
( ~ in(X0,sK77)
| in(X0,sF86)
| ~ in(X0,sF84) ),
inference(resolution,[],[f1883,f1240]) ).
fof(f2109,plain,
( ! [X0] :
( ~ in(X0,sF84)
| ~ in(X0,sK77)
| in(X0,sF83) )
| ~ spl92_3 ),
inference(forward_demodulation,[],[f2103,f1303]) ).
fof(f2114,plain,
( ! [X0] :
( ~ in(X0,sF83)
| in(X0,sF84) )
| ~ spl92_3 ),
inference(superposition,[],[f1375,f1303]) ).
fof(f2198,plain,
! [X0] :
( ~ in(X0,set_difference(sF84,sF85))
| in(X0,sK77) ),
inference(superposition,[],[f1229,f1273]) ).
fof(f2209,plain,
! [X0] :
( ~ in(X0,sF86)
| in(X0,sK77) ),
inference(forward_demodulation,[],[f2198,f1275]) ).
fof(f2211,plain,
( ! [X0] :
( ~ in(X0,sF83)
| in(X0,sK77) )
| ~ spl92_3 ),
inference(forward_demodulation,[],[f2209,f1303]) ).
fof(f2252,plain,
( subset(sF89,sK79)
| ~ relation(sK79) ),
inference(superposition,[],[f1029,f1281]) ).
fof(f2253,plain,
subset(sF89,sK79),
inference(forward_subsumption_resolution,[],[f2252,f1009]) ).
fof(f2479,plain,
! [X0] :
( in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF91(X0))),sF89)
| ~ in(X0,sK77)
| ~ in(X0,sF84) ),
inference(superposition,[],[f1721,f620]) ).
fof(f2955,plain,
! [X0,X1] :
( apply(X0,X1) = sK37(X0,X1)
| ~ relation(X0)
| ~ function(X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(resolution,[],[f1177,f1234]) ).
fof(f2962,plain,
( ! [X0] :
( apply(sK79,X0) = sF90(X0)
| ~ relation(sK79)
| ~ function(sK79)
| ~ in(X0,sF83) )
| ~ spl92_1 ),
inference(resolution,[],[f1177,f2056]) ).
fof(f2990,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0)
| apply(X0,X1) = sK37(X0,X1) ),
inference(duplicate_literal_removal,[],[f2955]) ).
fof(f2998,plain,
( ! [X0] :
( apply(sK79,X0) = sF90(X0)
| ~ function(sK79)
| ~ in(X0,sF83) )
| ~ spl92_1 ),
inference(forward_subsumption_resolution,[],[f2962,f1009]) ).
fof(f3007,plain,
( ! [X0] :
( apply(sK79,X0) = sF90(X0)
| ~ in(X0,sF83) )
| ~ spl92_1 ),
inference(forward_subsumption_resolution,[],[f2998,f1008]) ).
fof(f3015,plain,
( ! [X0] :
( sF90(X0) = sF91(X0)
| ~ in(X0,sF83) )
| ~ spl92_1 ),
inference(forward_demodulation,[],[f3007,f1288]) ).
fof(f3021,plain,
( spl92_2
| ~ spl92_1 ),
inference(avatar_split_clause,[],[f3015,f1293,f1297]) ).
fof(f3022,plain,
( spl92_5
| ~ spl92_2
| ~ spl92_4 ),
inference(avatar_split_clause,[],[f2076,f1306,f1297,f1311]) ).
fof(f3023,plain,
( sF83 = relation_dom(sF89)
| ~ spl92_3 ),
inference(forward_demodulation,[],[f1346,f1303]) ).
fof(f3066,plain,
( ! [X0] :
( in(X0,sF83)
| empty_set = apply(sF89,X0)
| ~ relation(sF89)
| ~ function(sF89) )
| ~ spl92_3 ),
inference(superposition,[],[f1232,f3023]) ).
fof(f3067,plain,
( ! [X0] :
( in(X0,sF83)
| empty_set = apply(sF89,X0)
| ~ function(sF89) )
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f3066,f1401]) ).
fof(f3070,plain,
( ! [X0] :
( in(X0,sF83)
| empty_set = apply(sF89,X0) )
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f3067,f1383]) ).
fof(f3075,plain,
( ! [X0] :
( sF90(X0) = sF91(X0)
| empty_set = sF90(X0) )
| ~ spl92_2 ),
inference(resolution,[],[f1298,f1523]) ).
fof(f3094,plain,
( ! [X0] :
( in(X0,sK77)
| empty_set = sF90(X0) )
| ~ spl92_3 ),
inference(resolution,[],[f2211,f1523]) ).
fof(f3103,plain,
( ! [X0] :
( in(X0,sF84)
| empty_set = sF90(X0) )
| ~ spl92_3 ),
inference(resolution,[],[f2114,f1523]) ).
fof(f3262,plain,
! [X0] :
( ~ in(X0,sF83)
| ~ relation(sK78)
| ~ function(sK78)
| apply(sK78,X0) = sK37(sK78,X0) ),
inference(superposition,[],[f2990,f1269]) ).
fof(f3269,plain,
! [X0] :
( ~ in(X0,sF83)
| ~ function(sK78)
| apply(sK78,X0) = sK37(sK78,X0) ),
inference(forward_subsumption_resolution,[],[f3262,f1007]) ).
fof(f3273,plain,
! [X0] :
( ~ in(X0,sF83)
| apply(sK78,X0) = sK37(sK78,X0) ),
inference(forward_subsumption_resolution,[],[f3269,f1006]) ).
fof(f3275,plain,
! [X0] :
( ~ in(X0,sF83)
| sF90(X0) = sK37(sK78,X0) ),
inference(forward_demodulation,[],[f3273,f1286]) ).
fof(f3357,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| ~ in(X0,sK77)
| in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sF89) ),
inference(resolution,[],[f1581,f1717]) ).
fof(f3358,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| apply(sK79,X0) = apply(sF89,X0)
| ~ relation(sK79)
| ~ function(sK79) ),
inference(resolution,[],[f1581,f1177]) ).
fof(f3370,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| apply(sK79,X0) = apply(sF89,X0)
| ~ function(sK79) ),
inference(forward_subsumption_resolution,[],[f3358,f1009]) ).
fof(f3371,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sF89) ),
inference(forward_subsumption_resolution,[],[f3357,f1355]) ).
fof(f3374,plain,
! [X0] :
( ~ in(X0,relation_dom(sF89))
| apply(sK79,X0) = apply(sF89,X0) ),
inference(forward_subsumption_resolution,[],[f3370,f1008]) ).
fof(f3375,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sF89,X0)),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sF83) )
| ~ spl92_3 ),
inference(forward_demodulation,[],[f3371,f3023]) ).
fof(f3378,plain,
( ! [X0] :
( ~ in(X0,sF83)
| apply(sK79,X0) = apply(sF89,X0) )
| ~ spl92_3 ),
inference(forward_demodulation,[],[f3374,f3023]) ).
fof(f3380,plain,
( ! [X0] :
( ~ in(X0,sF83)
| sF91(X0) = apply(sF89,X0) )
| ~ spl92_3 ),
inference(forward_demodulation,[],[f3378,f1288]) ).
fof(f3396,plain,
( ! [X0] :
( sF91(X0) = apply(sF89,X0)
| empty_set = apply(sF89,X0) )
| ~ spl92_3 ),
inference(resolution,[],[f3380,f3070]) ).
fof(f3479,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sF83)
| empty_set = apply(sF89,X0) )
| ~ spl92_3 ),
inference(superposition,[],[f3375,f3396]) ).
fof(f3494,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF91(X0)),unordered_pair(X0,X0)),sF89)
| empty_set = apply(sF89,X0) )
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f3479,f3070]) ).
fof(f3664,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sK77)
| ~ in(X0,sF84)
| empty_set = sF90(X0) )
| ~ spl92_2 ),
inference(superposition,[],[f1721,f3075]) ).
fof(f3667,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sF89)
| ~ in(X0,sF84)
| empty_set = sF90(X0) )
| ~ spl92_2
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f3664,f3094]) ).
fof(f3670,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,sF90(X0)),unordered_pair(X0,X0)),sF89)
| empty_set = sF90(X0) )
| ~ spl92_2
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f3667,f3103]) ).
fof(f4266,plain,
! [X0] :
( ~ in(X0,sF89)
| in(X0,sK79) ),
inference(resolution,[],[f708,f2253]) ).
fof(f18036,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(sK22(X0,X1),sK22(X0,X1)),unordered_pair(sK22(X0,X1),sK23(X0,X1))),X1)
| X0 = X1
| ~ in(unordered_pair(unordered_pair(sK22(X0,X1),sK22(X0,X1)),unordered_pair(sK22(X0,X1),sK23(X0,X1))),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(superposition,[],[f1080,f620]) ).
fof(f20241,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| sF89 = X0
| ~ relation(sF89)
| ~ relation(X0)
| in(sK22(X0,sF89),sK77) ),
inference(resolution,[],[f1081,f1500]) ).
fof(f20308,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| sF89 = X0
| ~ relation(sF89)
| ~ relation(X0)
| in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),sK79) ),
inference(resolution,[],[f1081,f4266]) ).
fof(f20312,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X1)
| X0 = X1
| ~ relation(X1)
| ~ relation(X0)
| in(sK22(X0,X1),relation_dom(X0))
| ~ relation(X0) ),
inference(resolution,[],[f1081,f1148]) ).
fof(f20395,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(sK22(X0,X1),sK23(X0,X1)),unordered_pair(sK22(X0,X1),sK22(X0,X1))),X1)
| X0 = X1
| ~ relation(X1)
| ~ relation(X0)
| in(sK22(X0,X1),relation_dom(X0)) ),
inference(duplicate_literal_removal,[],[f20312]) ).
fof(f20415,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),sK79)
| in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| ~ relation(X0)
| sF89 = X0 ),
inference(forward_subsumption_resolution,[],[f20308,f1401]) ).
fof(f20421,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| sF89 = X0
| ~ relation(X0)
| in(sK22(X0,sF89),sK77) ),
inference(forward_subsumption_resolution,[],[f20241,f1401]) ).
fof(f20713,plain,
! [X0] :
( sF89 = X0
| ~ relation(X0)
| in(sK22(X0,sF89),sK77)
| in(sK22(X0,sF89),relation_dom(X0))
| ~ relation(X0) ),
inference(resolution,[],[f20421,f1148]) ).
fof(f20793,plain,
! [X0] :
( in(sK22(X0,sF89),relation_dom(X0))
| ~ relation(X0)
| in(sK22(X0,sF89),sK77)
| sF89 = X0 ),
inference(duplicate_literal_removal,[],[f20713]) ).
fof(f20838,plain,
( in(sK22(sK78,sF89),sF83)
| ~ relation(sK78)
| in(sK22(sK78,sF89),sK77)
| sK78 = sF89 ),
inference(superposition,[],[f20793,f1269]) ).
fof(f20844,plain,
( ~ relation(sK78)
| in(sK22(sK78,sF89),sK77)
| sK78 = sF89
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f20838,f2211]) ).
fof(f20855,plain,
( in(sK22(sK78,sF89),sK77)
| sK78 = sF89
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f20844,f1007]) ).
fof(f20861,plain,
( in(sK22(sK78,sF89),sK77)
| spl92_1
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f20855,f1294]) ).
fof(f20908,definition,
( spl92_419
<=> empty_set = sF91(sK22(sK78,sF89)) ),
introduced(definition,[new_symbols(definition,[spl92_419])],[avatar_definition]) ).
fof(f20909,plain,
( empty_set != sF91(sK22(sK78,sF89))
| spl92_419 ),
inference(avatar_component_clause,[],[f20908]) ).
fof(f20910,plain,
( empty_set = sF91(sK22(sK78,sF89))
| ~ spl92_419 ),
inference(avatar_component_clause,[],[f20908]) ).
fof(f20912,definition,
( spl92_420
<=> in(sK22(sK78,sF89),sF83) ),
introduced(definition,[new_symbols(definition,[spl92_420])],[avatar_definition]) ).
fof(f20913,plain,
( ~ in(sK22(sK78,sF89),sF83)
| spl92_420 ),
inference(avatar_component_clause,[],[f20912]) ).
fof(f20914,plain,
( in(sK22(sK78,sF89),sF83)
| ~ spl92_420 ),
inference(avatar_component_clause,[],[f20912]) ).
fof(f29764,plain,
! [X0,X1] :
( X0 = X1
| ~ relation(X1)
| ~ relation(X0)
| in(sK22(X0,X1),relation_dom(X0))
| in(sK22(X0,X1),relation_dom(X1))
| ~ relation(X1) ),
inference(resolution,[],[f20395,f1148]) ).
fof(f29853,plain,
! [X0,X1] :
( in(sK22(X0,X1),relation_dom(X1))
| in(sK22(X0,X1),relation_dom(X0))
| ~ relation(X0)
| ~ relation(X1)
| X0 = X1 ),
inference(duplicate_literal_removal,[],[f29764]) ).
fof(f56206,plain,
! [X0] :
( in(sK22(X0,sF89),relation_dom(X0))
| ~ relation(X0)
| ~ relation(sF89)
| sF89 = X0
| in(sK22(X0,sF89),sF84) ),
inference(resolution,[],[f29853,f1385]) ).
fof(f56308,plain,
! [X0] :
( in(sK22(X0,sF89),relation_dom(X0))
| ~ relation(X0)
| sF89 = X0
| in(sK22(X0,sF89),sF84) ),
inference(forward_subsumption_resolution,[],[f56206,f1401]) ).
fof(f99125,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| ~ relation(X0)
| sF89 = X0
| sK23(X0,sF89) = apply(sK79,sK22(X0,sF89))
| ~ relation(sK79)
| ~ function(sK79) ),
inference(resolution,[],[f20415,f1177]) ).
fof(f99345,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| ~ relation(X0)
| sF89 = X0
| sK23(X0,sF89) = apply(sK79,sK22(X0,sF89))
| ~ function(sK79) ),
inference(forward_subsumption_resolution,[],[f99125,f1009]) ).
fof(f99437,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| ~ relation(X0)
| sF89 = X0
| sK23(X0,sF89) = apply(sK79,sK22(X0,sF89)) ),
inference(forward_subsumption_resolution,[],[f99345,f1008]) ).
fof(f159630,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK22(X0,sF89),sK23(X0,sF89)),unordered_pair(sK22(X0,sF89),sK22(X0,sF89))),X0)
| sK23(X0,sF89) = sF91(sK22(X0,sF89))
| ~ relation(X0)
| sF89 = X0 ),
inference(forward_demodulation,[],[f99437,f1288]) ).
fof(f159733,definition,
( spl92_1398
<=> empty_set = apply(sF89,sK22(sK78,sF89)) ),
introduced(definition,[new_symbols(definition,[spl92_1398])],[avatar_definition]) ).
fof(f159734,plain,
( empty_set != apply(sF89,sK22(sK78,sF89))
| spl92_1398 ),
inference(avatar_component_clause,[],[f159733]) ).
fof(f159735,plain,
( empty_set = apply(sF89,sK22(sK78,sF89))
| ~ spl92_1398 ),
inference(avatar_component_clause,[],[f159733]) ).
fof(f160812,definition,
( spl92_1442
<=> in(sK22(sK78,sF89),sF84) ),
introduced(definition,[new_symbols(definition,[spl92_1442])],[avatar_definition]) ).
fof(f160813,plain,
( ~ in(sK22(sK78,sF89),sF84)
| spl92_1442 ),
inference(avatar_component_clause,[],[f160812]) ).
fof(f160814,plain,
( in(sK22(sK78,sF89),sF84)
| ~ spl92_1442 ),
inference(avatar_component_clause,[],[f160812]) ).
fof(f201679,plain,
( in(sK22(sK78,sF89),sF83)
| ~ relation(sK78)
| sK78 = sF89
| in(sK22(sK78,sF89),sF84) ),
inference(superposition,[],[f56308,f1269]) ).
fof(f201693,plain,
( ~ relation(sK78)
| sK78 = sF89
| in(sK22(sK78,sF89),sF84)
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f201679,f2114]) ).
fof(f201709,plain,
( sK78 = sF89
| in(sK22(sK78,sF89),sF84)
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f201693,f1007]) ).
fof(f201713,plain,
( in(sK22(sK78,sF89),sF84)
| spl92_1
| ~ spl92_3 ),
inference(forward_subsumption_resolution,[],[f201709,f1294]) ).
fof(f201717,plain,
( $false
| spl92_1
| ~ spl92_3
| spl92_1442 ),
inference(forward_subsumption_resolution,[],[f201713,f160813]) ).
fof(f201718,plain,
( spl92_1
| ~ spl92_3
| spl92_1442 ),
inference(avatar_contradiction_clause,[],[f201717]) ).
fof(f201936,plain,
( ~ in(sK22(sK78,sF89),sK77)
| in(sK22(sK78,sF89),sF83)
| ~ spl92_3
| ~ spl92_1442 ),
inference(resolution,[],[f160814,f2109]) ).
fof(f201985,plain,
( in(sK22(sK78,sF89),sF83)
| spl92_1
| ~ spl92_3
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f201936,f20861]) ).
fof(f202001,plain,
( $false
| spl92_1
| ~ spl92_3
| spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f201985,f20913]) ).
fof(f202002,plain,
( spl92_1
| ~ spl92_3
| spl92_420
| ~ spl92_1442 ),
inference(avatar_contradiction_clause,[],[f202001]) ).
fof(f202009,plain,
( sF91(sK22(sK78,sF89)) = sF90(sK22(sK78,sF89))
| ~ spl92_2
| ~ spl92_420 ),
inference(resolution,[],[f20914,f1298]) ).
fof(f202015,plain,
( sF90(sK22(sK78,sF89)) = sK37(sK78,sK22(sK78,sF89))
| ~ spl92_420 ),
inference(resolution,[],[f20914,f3275]) ).
fof(f202016,plain,
( sF91(sK22(sK78,sF89)) = apply(sF89,sK22(sK78,sF89))
| ~ spl92_3
| ~ spl92_420 ),
inference(resolution,[],[f20914,f3380]) ).
fof(f202045,plain,
( empty_set = sF91(sK22(sK78,sF89))
| ~ spl92_3
| ~ spl92_420
| ~ spl92_1398 ),
inference(forward_demodulation,[],[f202016,f159735]) ).
fof(f202048,plain,
( empty_set = sF90(sK22(sK78,sF89))
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(forward_demodulation,[],[f202009,f20910]) ).
fof(f203676,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sF90(sK22(sK78,sF89)))),sK78)
| ~ in(sK22(sK78,sF89),relation_dom(sK78))
| ~ relation(sK78)
| ~ spl92_420 ),
inference(superposition,[],[f1628,f202015]) ).
fof(f203679,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sF90(sK22(sK78,sF89)))),sK78)
| ~ in(sK22(sK78,sF89),relation_dom(sK78))
| ~ spl92_420 ),
inference(forward_subsumption_resolution,[],[f203676,f1007]) ).
fof(f203685,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ in(sK22(sK78,sF89),relation_dom(sK78))
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(forward_demodulation,[],[f203679,f202048]) ).
fof(f203691,plain,
( ~ in(sK22(sK78,sF89),sF83)
| in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(forward_demodulation,[],[f203685,f1269]) ).
fof(f203695,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(forward_subsumption_resolution,[],[f203691,f20914]) ).
fof(f210600,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sF89)
| ~ in(sK22(sK78,sF89),sK77)
| ~ in(sK22(sK78,sF89),sF84)
| ~ spl92_419 ),
inference(superposition,[],[f2479,f20910]) ).
fof(f210615,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sF89)
| ~ in(sK22(sK78,sF89),sF84)
| spl92_1
| ~ spl92_3
| ~ spl92_419 ),
inference(forward_subsumption_resolution,[],[f210600,f20861]) ).
fof(f210619,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sF89)
| spl92_1
| ~ spl92_3
| ~ spl92_419
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f210615,f160814]) ).
fof(f242688,plain,
! [X0] :
( sK23(X0,sF89) = sF91(sK22(X0,sF89))
| ~ relation(X0)
| sF89 = X0
| sK23(X0,sF89) = apply(X0,sK22(X0,sF89))
| ~ relation(X0)
| ~ function(X0) ),
inference(resolution,[],[f159630,f1177]) ).
fof(f242868,plain,
! [X0] :
( ~ relation(X0)
| sK23(X0,sF89) = sF91(sK22(X0,sF89))
| sF89 = X0
| sK23(X0,sF89) = apply(X0,sK22(X0,sF89))
| ~ function(X0) ),
inference(duplicate_literal_removal,[],[f242688]) ).
fof(f243037,plain,
( sF91(sK22(sK78,sF89)) = sK23(sK78,sF89)
| sK78 = sF89
| sK23(sK78,sF89) = apply(sK78,sK22(sK78,sF89))
| ~ function(sK78) ),
inference(resolution,[],[f242868,f1007]) ).
fof(f243040,plain,
( sF91(sK22(sK78,sF89)) = sK23(sK78,sF89)
| sK23(sK78,sF89) = apply(sK78,sK22(sK78,sF89))
| ~ function(sK78)
| spl92_1 ),
inference(forward_subsumption_resolution,[],[f243037,f1294]) ).
fof(f243048,plain,
( sF91(sK22(sK78,sF89)) = sK23(sK78,sF89)
| sK23(sK78,sF89) = apply(sK78,sK22(sK78,sF89))
| spl92_1 ),
inference(forward_subsumption_resolution,[],[f243040,f1006]) ).
fof(f243055,plain,
( empty_set = sK23(sK78,sF89)
| sK23(sK78,sF89) = apply(sK78,sK22(sK78,sF89))
| spl92_1
| ~ spl92_419 ),
inference(forward_demodulation,[],[f243048,f20910]) ).
fof(f243062,plain,
( sK23(sK78,sF89) = sF90(sK22(sK78,sF89))
| empty_set = sK23(sK78,sF89)
| spl92_1
| ~ spl92_419 ),
inference(forward_demodulation,[],[f243055,f1286]) ).
fof(f243071,plain,
( empty_set = sK23(sK78,sF89)
| empty_set = sK23(sK78,sF89)
| spl92_1
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(forward_demodulation,[],[f243062,f202048]) ).
fof(f243072,plain,
( empty_set = sK23(sK78,sF89)
| spl92_1
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(duplicate_literal_removal,[],[f243071]) ).
fof(f243103,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sF89)
| sK78 = sF89
| ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_419
| ~ spl92_420 ),
inference(superposition,[],[f18036,f243072]) ).
fof(f243110,plain,
( sK78 = sF89
| ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f243103,f210619]) ).
fof(f243112,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89)),unordered_pair(sK22(sK78,sF89),empty_set)),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f243110,f1294]) ).
fof(f243114,plain,
( ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f243112,f203695]) ).
fof(f243116,plain,
( ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f243114,f1401]) ).
fof(f243119,plain,
( $false
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(forward_subsumption_resolution,[],[f243116,f1007]) ).
fof(f243120,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(avatar_contradiction_clause,[],[f243119]) ).
fof(f243133,plain,
( $false
| ~ spl92_3
| spl92_419
| ~ spl92_420
| ~ spl92_1398 ),
inference(forward_subsumption_resolution,[],[f202045,f20909]) ).
fof(f243134,plain,
( ~ spl92_3
| spl92_419
| ~ spl92_420
| ~ spl92_1398 ),
inference(avatar_contradiction_clause,[],[f243133]) ).
fof(f243168,plain,
( sK23(sK78,sF89) = sF90(sK22(sK78,sF89))
| sK23(sK78,sF89) = apply(sK78,sK22(sK78,sF89))
| spl92_1
| ~ spl92_2
| ~ spl92_420 ),
inference(forward_demodulation,[],[f243048,f202009]) ).
fof(f243211,plain,
( sK23(sK78,sF89) = sF90(sK22(sK78,sF89))
| sK23(sK78,sF89) = sF90(sK22(sK78,sF89))
| spl92_1
| ~ spl92_2
| ~ spl92_420 ),
inference(forward_demodulation,[],[f243168,f1286]) ).
fof(f243212,plain,
( sK23(sK78,sF89) = sF90(sK22(sK78,sF89))
| spl92_1
| ~ spl92_2
| ~ spl92_420 ),
inference(duplicate_literal_removal,[],[f243211]) ).
fof(f243230,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ in(sK22(sK78,sF89),sF83)
| spl92_1
| ~ spl92_2
| ~ spl92_420 ),
inference(superposition,[],[f1480,f243212]) ).
fof(f243233,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| empty_set = sK23(sK78,sF89)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420 ),
inference(superposition,[],[f3670,f243212]) ).
fof(f243245,definition,
( spl92_3772
<=> empty_set = sK23(sK78,sF89) ),
introduced(definition,[new_symbols(definition,[spl92_3772])],[avatar_definition]) ).
fof(f243247,plain,
( empty_set = sK23(sK78,sF89)
| ~ spl92_3772 ),
inference(avatar_component_clause,[],[f243245]) ).
fof(f243249,definition,
( spl92_3773
<=> in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89) ),
introduced(definition,[new_symbols(definition,[spl92_3773])],[avatar_definition]) ).
fof(f243251,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| ~ spl92_3773 ),
inference(avatar_component_clause,[],[f243249]) ).
fof(f243252,plain,
( spl92_3772
| spl92_3773
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420 ),
inference(avatar_split_clause,[],[f243233,f20912,f1301,f1297,f1293,f243249,f243245]) ).
fof(f243259,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_420 ),
inference(forward_subsumption_resolution,[],[f243230,f20914]) ).
fof(f243274,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sF90(sK22(sK78,sF89))),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| empty_set = apply(sF89,sK22(sK78,sF89))
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420 ),
inference(superposition,[],[f3494,f202009]) ).
fof(f243299,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sF90(sK22(sK78,sF89))),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398 ),
inference(forward_subsumption_resolution,[],[f243274,f159734]) ).
fof(f243316,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398 ),
inference(forward_demodulation,[],[f243299,f243212]) ).
fof(f243333,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_demodulation,[],[f243316,f243247]) ).
fof(f243347,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| empty_set = sF91(sK22(sK78,sF89))
| ~ relation(sK78)
| sK78 = sF89
| ~ spl92_3772 ),
inference(superposition,[],[f159630,f243247]) ).
fof(f243355,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sF89)
| sK78 = sF89
| ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| ~ spl92_3772 ),
inference(superposition,[],[f1080,f243247]) ).
fof(f243356,plain,
( sK78 = sF89
| ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243355,f243333]) ).
fof(f243359,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sK78)
| sK78 = sF89
| spl92_419
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243347,f20909]) ).
fof(f243360,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243356,f1294]) ).
fof(f243363,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| sK78 = sF89
| spl92_419
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243359,f1007]) ).
fof(f243364,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243360,f1401]) ).
fof(f243367,plain,
( in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| spl92_1
| spl92_419
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243363,f1294]) ).
fof(f243368,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),empty_set),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243364,f1007]) ).
fof(f243371,plain,
( $false
| spl92_1
| ~ spl92_2
| ~ spl92_3
| spl92_419
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(forward_subsumption_resolution,[],[f243368,f243367]) ).
fof(f243372,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_3
| spl92_419
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(avatar_contradiction_clause,[],[f243371]) ).
fof(f243387,plain,
( sK78 = sF89
| ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| ~ spl92_3773 ),
inference(resolution,[],[f243251,f1080]) ).
fof(f243421,plain,
( ~ in(unordered_pair(unordered_pair(sK22(sK78,sF89),sK23(sK78,sF89)),unordered_pair(sK22(sK78,sF89),sK22(sK78,sF89))),sK78)
| ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_3773 ),
inference(forward_subsumption_resolution,[],[f243387,f1294]) ).
fof(f243426,plain,
( ~ relation(sF89)
| ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_420
| ~ spl92_3773 ),
inference(forward_subsumption_resolution,[],[f243421,f243259]) ).
fof(f243429,plain,
( ~ relation(sK78)
| spl92_1
| ~ spl92_2
| ~ spl92_420
| ~ spl92_3773 ),
inference(forward_subsumption_resolution,[],[f243426,f1401]) ).
fof(f243431,plain,
( $false
| spl92_1
| ~ spl92_2
| ~ spl92_420
| ~ spl92_3773 ),
inference(forward_subsumption_resolution,[],[f243429,f1007]) ).
fof(f243432,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_420
| ~ spl92_3773 ),
inference(avatar_contradiction_clause,[],[f243431]) ).
cnf(s1,plain,
( spl92_1
| spl92_2 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s2,plain,
( spl92_1
| spl92_3 ),
inference(sat_conversion,[],[f1304]) ).
cnf(s3,plain,
( ~ spl92_1
| ~ spl92_3
| spl92_4 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s4,plain,
( ~ spl92_1
| ~ spl92_3
| ~ spl92_5 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s26,plain,
( ~ spl92_1
| spl92_3 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s52,plain,
( ~ spl92_1
| spl92_2 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s53,plain,
( ~ spl92_2
| ~ spl92_4
| spl92_5 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s3898,plain,
( spl92_1
| ~ spl92_3
| spl92_1442 ),
inference(sat_conversion,[],[f201718]) ).
cnf(s3921,plain,
( spl92_1
| ~ spl92_3
| spl92_420
| ~ spl92_1442 ),
inference(sat_conversion,[],[f202002]) ).
cnf(s5521,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_419
| ~ spl92_420
| ~ spl92_1442 ),
inference(sat_conversion,[],[f243120]) ).
cnf(s5524,plain,
( ~ spl92_3
| spl92_419
| ~ spl92_420
| ~ spl92_1398 ),
inference(sat_conversion,[],[f243134]) ).
cnf(s5533,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_3
| ~ spl92_420
| spl92_3772
| spl92_3773 ),
inference(sat_conversion,[],[f243252]) ).
cnf(s5536,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_3
| spl92_419
| ~ spl92_420
| spl92_1398
| ~ spl92_3772 ),
inference(sat_conversion,[],[f243372]) ).
cnf(s5539,plain,
( spl92_1
| ~ spl92_2
| ~ spl92_420
| ~ spl92_3773 ),
inference(sat_conversion,[],[f243432]) ).
cnf(s5639,plain,
spl92_1,
inference(rat,[],[s5536,s5524,s5521,s5533,s5539,s3921,s3898,s1,s2]) ).
cnf(s5640,plain,
spl92_2,
inference(rat,[],[s52,s5639]) ).
cnf(s5641,plain,
spl92_3,
inference(rat,[],[s26,s5639]) ).
cnf(s5657,plain,
~ spl92_5,
inference(rat,[],[s4,s5639,s5641]) ).
cnf(s5658,plain,
spl92_4,
inference(rat,[],[s3,s5639,s5641]) ).
cnf(s5660,plain,
$false,
inference(rat,[],[s53,s5640,s5657,s5658]) ).
fof(f243433,plain,
$false,
inference(avatar_sat_refutation,[],[s5660]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU222+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n015.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Mon Sep 28 04:12:18 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.43 Running first-order theorem proving
% 0.10/0.43 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
% 15.62/3.11 % (2248635)Detected formulas, will run a generic FOF schedule.
% 15.62/3.11 % (2248640)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=3110412856:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.62/3.11 % (2248645)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2841988329:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.62/3.11 % (2248642)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=1325866351:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.62/3.11 % (2248646)dis-21_1_sil=8000:lcm=predicate:random_seed=2868945547: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)
% 15.62/3.11 % (2248644)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1107390739:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.62/3.11 % (2248643)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1993484434:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.62/3.11 % (2248641)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=2770804985:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.62/3.11 % (2248643)Instruction limit reached!
% 15.62/3.11 % (2248643)------------------------------
% 15.62/3.11 % (2248643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.62/3.11 % (2248643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/3.11 % (2248643)CaDiCaL version: 2.1.3
% 15.62/3.11 % (2248643)Termination reason: Instruction limit
% 15.62/3.11 % (2248643)Termination phase: Saturation
% 15.62/3.11 % (2248643)Time elapsed: 0.071 s
% 15.62/3.11 % (2248643)Peak memory usage: 90 MB
% 15.62/3.11 % (2248643)Instructions burned: 110 (million)
% 15.62/3.11 % (2248646)Instruction limit reached!
% 15.62/3.11 % (2248646)------------------------------
% 15.62/3.11 % (2248646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.62/3.11 % (2248646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/3.11 % (2248646)CaDiCaL version: 2.1.3
% 15.62/3.11 % (2248646)Termination reason: Instruction limit
% 15.62/3.11 % (2248646)Termination phase: Saturation
% 15.62/3.11 % (2248646)Time elapsed: 0.076 s
% 15.62/3.11 % (2248646)Peak memory usage: 90 MB
% 15.62/3.11 % (2248646)Instructions burned: 129 (million)
% 15.62/3.11 % (2248644)Instruction limit reached!
% 15.62/3.11 % (2248644)------------------------------
% 15.62/3.11 % (2248644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.62/3.11 % (2248644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/3.11 % (2248644)CaDiCaL version: 2.1.3
% 15.62/3.11 % (2248644)Termination reason: Instruction limit
% 15.62/3.11 % (2248644)Termination phase: Saturation
% 15.62/3.11 % (2248644)Time elapsed: 0.076 s
% 15.62/3.11 % (2248644)Peak memory usage: 89 MB
% 15.62/3.11 % (2248644)Instructions burned: 120 (million)
% 15.62/3.11 % (2248645)Instruction limit reached!
% 15.62/3.11 % (2248645)------------------------------
% 15.62/3.11 % (2248645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.62/3.11 % (2248645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/3.11 % (2248645)CaDiCaL version: 2.1.3
% 15.62/3.11 % (2248645)Termination reason: Instruction limit
% 15.62/3.11 % (2248645)Termination phase: Saturation
% 15.62/3.11 % (2248645)Time elapsed: 0.101 s
% 15.62/3.11 % (2248645)Peak memory usage: 90 MB
% 15.62/3.11 % (2248645)Instructions burned: 140 (million)
% 15.62/3.11 % (2248654)lrs+10_1_sil=8000:sp=occurrence:random_seed=3702479248:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 15.62/3.11 % (2248655)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3895101142:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.62/3.11 % (2248656)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3789705713:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.62/3.11 % (2248657)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=1629643626:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 15.62/3.11 % (2248655)Instruction limit reached!
% 22.74/4.04 % (2248655)------------------------------
% 22.74/4.04 % (2248655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248655)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248655)Termination reason: Instruction limit
% 22.74/4.04 % (2248655)Termination phase: Saturation
% 22.74/4.04 % (2248655)Time elapsed: 0.095 s
% 22.74/4.04 % (2248655)Peak memory usage: 91 MB
% 22.74/4.04 % (2248655)Instructions burned: 158 (million)
% 22.74/4.04 % (2248657)Instruction limit reached!
% 22.74/4.04 % (2248657)------------------------------
% 22.74/4.04 % (2248657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248657)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248657)Termination reason: Instruction limit
% 22.74/4.04 % (2248657)Termination phase: Saturation
% 22.74/4.04 % (2248657)Time elapsed: 0.142 s
% 22.74/4.04 % (2248657)Peak memory usage: 95 MB
% 22.74/4.04 % (2248657)Instructions burned: 249 (million)
% 22.74/4.04 % (2248654)Instruction limit reached!
% 22.74/4.04 % (2248654)------------------------------
% 22.74/4.04 % (2248654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248654)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248654)Termination reason: Instruction limit
% 22.74/4.04 % (2248654)Termination phase: Saturation
% 22.74/4.04 % (2248654)Time elapsed: 0.188 s
% 22.74/4.04 % (2248654)Peak memory usage: 93 MB
% 22.74/4.04 % (2248654)Instructions burned: 286 (million)
% 22.74/4.04 % (2248656)Instruction limit reached!
% 22.74/4.04 % (2248656)------------------------------
% 22.74/4.04 % (2248656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248656)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248656)Termination reason: Instruction limit
% 22.74/4.04 % (2248656)Termination phase: Saturation
% 22.74/4.04 % (2248656)Time elapsed: 0.223 s
% 22.74/4.04 % (2248656)Peak memory usage: 93 MB
% 22.74/4.04 % (2248656)Instructions burned: 326 (million)
% 22.74/4.04 % (2248662)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3634271571:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 22.74/4.04 % (2248663)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2826005884:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 22.74/4.04 % (2248664)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4108036424:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 22.74/4.04 % (2248664)Instruction limit reached!
% 22.74/4.04 % (2248664)------------------------------
% 22.74/4.04 % (2248664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248664)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248664)Termination reason: Instruction limit
% 22.74/4.04 % (2248664)Termination phase: Saturation
% 22.74/4.04 % (2248664)Time elapsed: 0.070 s
% 22.74/4.04 % (2248664)Peak memory usage: 90 MB
% 22.74/4.04 % (2248664)Instructions burned: 113 (million)
% 22.74/4.04 % (2248665)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4179715160:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 22.74/4.04 % (2248662)Instruction limit reached!
% 22.74/4.04 % (2248662)------------------------------
% 22.74/4.04 % (2248662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248662)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248662)Termination reason: Instruction limit
% 22.74/4.04 % (2248662)Termination phase: Saturation
% 22.74/4.04 % (2248662)Time elapsed: 0.189 s
% 22.74/4.04 % (2248662)Peak memory usage: 91 MB
% 22.74/4.04 % (2248662)Instructions burned: 295 (million)
% 22.74/4.04 % (2248665)Instruction limit reached!
% 22.74/4.04 % (2248665)------------------------------
% 22.74/4.04 % (2248665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.04 % (2248665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.04 % (2248665)CaDiCaL version: 2.1.3
% 22.74/4.04 % (2248665)Termination reason: Instruction limit
% 61.57/9.54 % (2248665)Termination phase: Saturation
% 61.57/9.54 % (2248665)Time elapsed: 0.067 s
% 61.57/9.54 % (2248665)Peak memory usage: 90 MB
% 61.57/9.54 % (2248665)Instructions burned: 128 (million)
% 61.57/9.54 % (2248670)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1229685951:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 61.57/9.54 % (2248671)lrs+10_1_sil=8000:sp=occurrence:random_seed=2444240823:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 61.57/9.54 % (2248670)Instruction limit reached!
% 61.57/9.54 % (2248670)------------------------------
% 61.57/9.54 % (2248670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.57/9.54 % (2248670)CaDiCaL version: 2.1.3
% 61.57/9.54 % (2248670)Termination reason: Instruction limit
% 61.57/9.54 % (2248670)Termination phase: Saturation
% 61.57/9.54 % (2248670)Time elapsed: 0.074 s
% 61.57/9.54 % (2248670)Peak memory usage: 89 MB
% 61.57/9.54 % (2248670)Instructions burned: 116 (million)
% 61.57/9.54 % (2248672)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1983630186:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 61.57/9.54 % (2248676)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2968021233:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 61.57/9.54 % (2248672)Instruction limit reached!
% 61.57/9.54 % (2248672)------------------------------
% 61.57/9.54 % (2248672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.57/9.54 % (2248672)CaDiCaL version: 2.1.3
% 61.57/9.54 % (2248672)Termination reason: Instruction limit
% 61.57/9.54 % (2248672)Termination phase: Saturation
% 61.57/9.54 % (2248672)Time elapsed: 0.279 s
% 61.57/9.54 % (2248672)Peak memory usage: 93 MB
% 61.57/9.54 % (2248672)Instructions burned: 437 (million)
% 61.57/9.54 % (2248678)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4201561983:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 61.57/9.54 % (2248671)Instruction limit reached!
% 61.57/9.54 % (2248671)------------------------------
% 61.57/9.54 % (2248671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.57/9.54 % (2248671)CaDiCaL version: 2.1.3
% 61.57/9.54 % (2248671)Termination reason: Instruction limit
% 61.57/9.54 % (2248671)Termination phase: Saturation
% 61.57/9.54 % (2248671)Time elapsed: 0.550 s
% 61.57/9.54 % (2248671)Peak memory usage: 99 MB
% 61.57/9.54 % (2248671)Instructions burned: 908 (million)
% 61.57/9.54 % (2248678)Instruction limit reached!
% 61.57/9.54 % (2248678)------------------------------
% 61.57/9.54 % (2248678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.57/9.54 % (2248678)CaDiCaL version: 2.1.3
% 61.57/9.54 % (2248678)Termination reason: Instruction limit
% 61.57/9.54 % (2248678)Termination phase: Saturation
% 61.57/9.54 % (2248678)Time elapsed: 0.078 s
% 61.57/9.54 % (2248678)Peak memory usage: 92 MB
% 61.57/9.54 % (2248678)Instructions burned: 134 (million)
% 61.57/9.54 % (2248680)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2142993414:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 61.57/9.54 % (2248681)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1531888146:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 61.57/9.54 % (2248680)Instruction limit reached!
% 61.57/9.54 % (2248680)------------------------------
% 61.57/9.54 % (2248680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.57/9.54 % (2248680)CaDiCaL version: 2.1.3
% 61.57/9.54 % (2248680)Termination reason: Instruction limit
% 61.57/9.54 % (2248680)Termination phase: Saturation
% 61.57/9.54 % (2248680)Time elapsed: 0.375 s
% 61.57/9.54 % (2248680)Peak memory usage: 100 MB
% 61.57/9.54 % (2248680)Instructions burned: 592 (million)
% 61.57/9.54 % (2248663)Instruction limit reached!
% 61.57/9.54 % (2248663)------------------------------
% 61.57/9.54 % (2248663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.57/9.54 % (2248663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248663)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248663)Termination reason: Instruction limit
% 40.01/10.20 % (2248663)Termination phase: Saturation
% 40.01/10.20 % (2248663)Time elapsed: 1.504 s
% 40.01/10.20 % (2248663)Peak memory usage: 142 MB
% 40.01/10.20 % (2248663)Instructions burned: 2350 (million)
% 40.01/10.20 % (2248684)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3290025792:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 40.01/10.20 % (2248684)Instruction limit reached!
% 40.01/10.20 % (2248684)------------------------------
% 40.01/10.20 % (2248684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248684)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248684)Termination reason: Instruction limit
% 40.01/10.20 % (2248684)Termination phase: Saturation
% 40.01/10.20 % (2248684)Time elapsed: 0.081 s
% 40.01/10.20 % (2248684)Peak memory usage: 91 MB
% 40.01/10.20 % (2248684)Instructions burned: 127 (million)
% 40.01/10.20 % (2248685)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2557080207:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 40.01/10.20 % (2248685)Instruction limit reached!
% 40.01/10.20 % (2248685)------------------------------
% 40.01/10.20 % (2248685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248685)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248685)Termination reason: Instruction limit
% 40.01/10.20 % (2248685)Termination phase: Saturation
% 40.01/10.20 % (2248685)Time elapsed: 0.085 s
% 40.01/10.20 % (2248685)Peak memory usage: 91 MB
% 40.01/10.20 % (2248685)Instructions burned: 135 (million)
% 40.01/10.20 % (2248687)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4293565519:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 40.01/10.20 % (2248687)Instruction limit reached!
% 40.01/10.20 % (2248687)------------------------------
% 40.01/10.20 % (2248687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248687)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248687)Termination reason: Instruction limit
% 40.01/10.20 % (2248687)Termination phase: Saturation
% 40.01/10.20 % (2248687)Time elapsed: 0.089 s
% 40.01/10.20 % (2248687)Peak memory usage: 91 MB
% 40.01/10.20 % (2248687)Instructions burned: 141 (million)
% 40.01/10.20 % (2248690)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=162463102:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 40.01/10.20 % (2248691)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2110088797:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 40.01/10.20 % (2248690)Instruction limit reached!
% 40.01/10.20 % (2248690)------------------------------
% 40.01/10.20 % (2248690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248690)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248690)Termination reason: Instruction limit
% 40.01/10.20 % (2248690)Termination phase: Saturation
% 40.01/10.20 % (2248690)Time elapsed: 0.258 s
% 40.01/10.20 % (2248690)Peak memory usage: 93 MB
% 40.01/10.20 % (2248690)Instructions burned: 432 (million)
% 40.01/10.20 % (2248694)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=947069129:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 40.01/10.20 % (2248694)Instruction limit reached!
% 40.01/10.20 % (2248694)------------------------------
% 40.01/10.20 % (2248694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248694)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248694)Termination reason: Instruction limit
% 40.01/10.20 % (2248694)Termination phase: Saturation
% 40.01/10.20 % (2248694)Time elapsed: 0.092 s
% 40.01/10.20 % (2248694)Peak memory usage: 92 MB
% 40.01/10.20 % (2248694)Instructions burned: 151 (million)
% 40.01/10.20 % (2248696)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2614146761:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 40.01/10.20 % (2248676)Instruction limit reached!
% 40.01/10.20 % (2248676)------------------------------
% 40.01/10.20 % (2248676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248676)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248676)Termination reason: Instruction limit
% 40.01/10.20 % (2248676)Termination phase: Saturation
% 40.01/10.20 % (2248676)Time elapsed: 3.248 s
% 40.01/10.20 % (2248676)Peak memory usage: 166 MB
% 40.01/10.20 % (2248676)Instructions burned: 5203 (million)
% 40.01/10.20 % (2248698)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3386091064:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 40.01/10.20 % (2248698)Instruction limit reached!
% 40.01/10.20 % (2248698)------------------------------
% 40.01/10.20 % (2248698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248698)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248698)Termination reason: Instruction limit
% 40.01/10.20 % (2248698)Termination phase: Saturation
% 40.01/10.20 % (2248698)Time elapsed: 0.327 s
% 40.01/10.20 % (2248698)Peak memory usage: 91 MB
% 40.01/10.20 % (2248698)Instructions burned: 668 (million)
% 40.01/10.20 % (2248700)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3264617116:s2a=on:i=185:s2at=1.8:fdi=4_2950 on theBenchmark for (2950ds/185Mi)
% 40.01/10.20 % (2248700)Instruction limit reached!
% 40.01/10.20 % (2248700)------------------------------
% 40.01/10.20 % (2248700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248700)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248700)Termination reason: Instruction limit
% 40.01/10.20 % (2248700)Termination phase: Saturation
% 40.01/10.20 % (2248700)Time elapsed: 0.117 s
% 40.01/10.20 % (2248700)Peak memory usage: 92 MB
% 40.01/10.20 % (2248700)Instructions burned: 187 (million)
% 40.01/10.20 % (2248702)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2869885560:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2947 on theBenchmark for (2947ds/193Mi)
% 40.01/10.20 % (2248702)Instruction limit reached!
% 40.01/10.20 % (2248702)------------------------------
% 40.01/10.20 % (2248702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248702)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248702)Termination reason: Instruction limit
% 40.01/10.20 % (2248702)Termination phase: Saturation
% 40.01/10.20 % (2248702)Time elapsed: 0.127 s
% 40.01/10.20 % (2248702)Peak memory usage: 92 MB
% 40.01/10.20 % (2248702)Instructions burned: 194 (million)
% 40.01/10.20 % (2248704)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=557730386:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2944 on theBenchmark for (2944ds/4850Mi)
% 40.01/10.20 % (2248691)Instruction limit reached!
% 40.01/10.20 % (2248691)------------------------------
% 40.01/10.20 % (2248691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248691)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248691)Termination reason: Instruction limit
% 40.01/10.20 % (2248691)Termination phase: Saturation
% 40.01/10.20 % (2248691)Time elapsed: 3.831 s
% 40.01/10.20 % (2248691)Peak memory usage: 169 MB
% 40.01/10.20 % (2248691)Instructions burned: 6061 (million)
% 40.01/10.20 % (2248706)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=945461842:i=12111:sd=1:ss=included_2933 on theBenchmark for (2933ds/12111Mi)
% 40.01/10.20 % (2248704)Instruction limit reached!
% 40.01/10.20 % (2248704)------------------------------
% 40.01/10.20 % (2248704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248704)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248704)Termination reason: Instruction limit
% 40.01/10.20 % (2248704)Termination phase: Saturation
% 40.01/10.20 % (2248704)Time elapsed: 2.970 s
% 40.01/10.20 % (2248704)Peak memory usage: 150 MB
% 40.01/10.20 % (2248704)Instructions burned: 4852 (million)
% 40.01/10.20 % (2248708)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4020830160:i=319:kws=precedence:fsr=off_2913 on theBenchmark for (2913ds/319Mi)
% 40.01/10.20 % (2248708)Instruction limit reached!
% 40.01/10.20 % (2248708)------------------------------
% 40.01/10.20 % (2248708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.01/10.20 % (2248708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.01/10.20 % (2248708)CaDiCaL version: 2.1.3
% 40.01/10.20 % (2248708)Termination reason: Instruction limit
% 40.01/10.20 % (2248708)Termination phase: Saturation
% 40.01/10.20 % (2248708)Time elapsed: 0.191 s
% 40.01/10.20 % (2248708)Peak memory usage: 93 MB
% 40.01/10.20 % (2248708)Instructions burned: 319 (million)
% 40.01/10.20 % (2248640)First to succeed.
% 40.01/10.20 % (2248640)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2248635"
% 40.01/10.20 % (2248710)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=62711060:i=2064:ep=RST_2909 on theBenchmark for (2909ds/2064Mi)
% 40.01/10.20 % (2248640)Refutation found. Thanks to Tanya!
% 40.01/10.20 % SZS status Theorem for theBenchmark
% 40.01/10.20 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/10.40 % (2248640)------------------------------
% 0.14/10.40 % (2248640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.14/10.40 % (2248640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/10.40 % (2248640)CaDiCaL version: 2.1.3
% 0.14/10.40 % (2248640)Termination reason: Refutation
% 0.14/10.40 % (2248640)Time elapsed: 8.997 s
% 0.14/10.40 % (2248640)Peak memory usage: 302 MB
% 0.14/10.40 % (2248640)Instructions burned: 27273 (million)
% 0.14/10.40 % (2248640)------------------------------
% 0.14/10.40 % (2248640)------------------------------
% 0.14/10.40 % (2248635)Success in time 9.331 s
% 0.14/10.40 % Vampire exiting
%------------------------------------------------------------------------------