%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU202+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 : n005.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:43 PM UTC 2026
% Result : Theorem 5.83s 2.20s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 23
% Syntax : Number of formulae : 199 ( 29 unt; 11 def)
% Number of atoms : 667 ( 74 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 816 ( 348 ~; 374 |; 61 &)
% ( 20 <=>; 12 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-3 aty)
% Number of variables : 287 ( 0 sgn 260 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,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(f10,axiom,
! [X0,X1] :
( relation(X1)
=> ! [X2] :
( relation(X2)
=> ( X2 = relation_rng_restriction(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_relat_1) ).
fof(f11,axiom,
! [X0] :
( relation(X0)
<=> ! [X1] :
~ ( in(X1,X0)
& ! [X2,X3] : X1 != ordered_pair(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_relat_1) ).
fof(f22,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f30,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(f59,axiom,
! [X0,X1] :
( relation(X0)
=> relation(relation_dom_restriction(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f61,axiom,
! [X0,X1] :
( relation(X1)
=> relation(relation_rng_restriction(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relat_1) ).
fof(f114,axiom,
! [X0,X1] :
( relation(X1)
=> subset(relation_rng_restriction(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_relat_1) ).
fof(f121,conjecture,
! [X0,X1,X2] :
( relation(X2)
=> relation_dom_restriction(relation_rng_restriction(X0,X2),X1) = relation_rng_restriction(X0,relation_dom_restriction(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t140_relat_1) ).
fof(f122,negated_conjecture,
~ ! [X0,X1,X2] :
( relation(X2)
=> relation_dom_restriction(relation_rng_restriction(X0,X2),X1) = relation_rng_restriction(X0,relation_dom_restriction(X2,X1)) ),
inference(negated_conjecture,[status(cth)],[f121]) ).
fof(f136,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
<=> in(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f177,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f186,axiom,
! [X0,X1] :
( relation(X1)
=> subset(relation_dom_restriction(X1,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t88_relat_1) ).
fof(f212,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,[],[f9]) ).
fof(f213,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = relation_rng_restriction(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) ) ) )
| ~ relation(X2) )
| ~ relation(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f214,plain,
! [X0] :
( relation(X0)
<=> ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f219,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f237,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f239,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(ennf_transformation,[],[f61]) ).
fof(f278,plain,
! [X0,X1] :
( subset(relation_rng_restriction(X0,X1),X1)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f114]) ).
fof(f287,plain,
? [X0,X1,X2] :
( relation_dom_restriction(relation_rng_restriction(X0,X2),X1) != relation_rng_restriction(X0,relation_dom_restriction(X2,X1))
& relation(X2) ),
inference(ennf_transformation,[],[f122]) ).
fof(f302,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( in(X2,X0)
<~> in(X2,X1) ) ),
inference(ennf_transformation,[],[f136]) ).
fof(f346,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f186]) ).
fof(f364,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,[],[f212]) ).
fof(f365,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,[],[f364]) ).
fof(f366,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,[],[f365]) ).
fof(f367,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = relation_dom_restriction(X0,X1)
| ( ( ~ in(sK2(X0,X1,X2),X1)
| ~ in(ordered_pair(sK2(X0,X1,X2),sK3(X0,X1,X2)),X0)
| ~ in(ordered_pair(sK2(X0,X1,X2),sK3(X0,X1,X2)),X2) )
& ( ( in(sK2(X0,X1,X2),X1)
& in(ordered_pair(sK2(X0,X1,X2),sK3(X0,X1,X2)),X0) )
| in(ordered_pair(sK2(X0,X1,X2),sK3(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,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f366]) ).
fof(f368,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = relation_rng_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X4,X0)
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X4,X0)
| ~ in(ordered_pair(X3,X4),X1) )
& ( ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) )
| ~ in(ordered_pair(X3,X4),X2) ) )
| relation_rng_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) ),
inference(nnf_transformation,[],[f213]) ).
fof(f369,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = relation_rng_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X4,X0)
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X4,X0)
| ~ in(ordered_pair(X3,X4),X1) )
& ( ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) )
| ~ in(ordered_pair(X3,X4),X2) ) )
| relation_rng_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) ),
inference(flattening,[],[f368]) ).
fof(f370,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = relation_rng_restriction(X0,X1)
| ? [X3,X4] :
( ( ~ in(X4,X0)
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X3,X4),X2) )
& ( ( in(X4,X0)
& in(ordered_pair(X3,X4),X1) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X5,X6] :
( ( in(ordered_pair(X5,X6),X2)
| ~ in(X6,X0)
| ~ in(ordered_pair(X5,X6),X1) )
& ( ( in(X6,X0)
& in(ordered_pair(X5,X6),X1) )
| ~ in(ordered_pair(X5,X6),X2) ) )
| relation_rng_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) ),
inference(rectify,[],[f369]) ).
fof(f371,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = relation_rng_restriction(X0,X1)
| ( ( ~ in(sK5(X0,X1,X2),X0)
| ~ in(ordered_pair(sK4(X0,X1,X2),sK5(X0,X1,X2)),X1)
| ~ in(ordered_pair(sK4(X0,X1,X2),sK5(X0,X1,X2)),X2) )
& ( ( in(sK5(X0,X1,X2),X0)
& in(ordered_pair(sK4(X0,X1,X2),sK5(X0,X1,X2)),X1) )
| in(ordered_pair(sK4(X0,X1,X2),sK5(X0,X1,X2)),X2) ) ) )
& ( ! [X5,X6] :
( ( in(ordered_pair(X5,X6),X2)
| ~ in(X6,X0)
| ~ in(ordered_pair(X5,X6),X1) )
& ( ( in(X6,X0)
& in(ordered_pair(X5,X6),X1) )
| ~ in(ordered_pair(X5,X6),X2) ) )
| relation_rng_restriction(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X0,X1,X2)),skolemize(X4,sK5(X0,X1,X2))],[f370]) ).
fof(f372,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 )
| ~ relation(X0) ) ),
inference(nnf_transformation,[],[f214]) ).
fof(f373,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ? [X5,X6] : ordered_pair(X5,X6) = X4 )
| ~ relation(X0) ) ),
inference(rectify,[],[f372]) ).
fof(f374,plain,
! [X0] :
( ( relation(X0)
| ( in(sK6(X0),X0)
& ! [X2,X3] : ordered_pair(X2,X3) != sK6(X0) ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ordered_pair(sK7(X4),sK8(X4)) = X4 )
| ~ relation(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X1,sK6(X0)),skolemize(X5,sK7(X4)),skolemize(X6,sK8(X4))],[f373]) ).
fof(f405,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,[],[f219]) ).
fof(f406,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,[],[f405]) ).
fof(f407,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK26(X0,X1),X1)
& in(sK26(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X2,sK26(X0,X1))],[f406]) ).
fof(f455,plain,
( relation_dom_restriction(relation_rng_restriction(sK54,sK56),sK55) != relation_rng_restriction(sK54,relation_dom_restriction(sK56,sK55))
& relation(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55,sK56]),skolemize(X0,sK54),skolemize(X1,sK55),skolemize(X2,sK56)],[f287]) ).
fof(f456,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ in(X2,X1)
| ~ in(X2,X0) )
& ( in(X2,X1)
| in(X2,X0) ) ) ),
inference(nnf_transformation,[],[f302]) ).
fof(f457,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ in(sK57(X0,X1),X1)
| ~ in(sK57(X0,X1),X0) )
& ( in(sK57(X0,X1),X1)
| in(sK57(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(X2,sK57(X0,X1))],[f456]) ).
fof(f493,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,[],[f367]) ).
fof(f494,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,[],[f367]) ).
fof(f499,plain,
! [X2,X0,X1,X6,X5] :
( in(X6,X0)
| ~ in(ordered_pair(X5,X6),X2)
| relation_rng_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f371]) ).
fof(f500,plain,
! [X2,X0,X1,X6,X5] :
( in(ordered_pair(X5,X6),X2)
| ~ in(X6,X0)
| ~ in(ordered_pair(X5,X6),X1)
| relation_rng_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f371]) ).
fof(f504,plain,
! [X0,X4] :
( ~ in(X4,X0)
| ordered_pair(sK7(X4),sK8(X4)) = X4
| ~ relation(X0) ),
inference(cnf_transformation,[],[f374]) ).
fof(f556,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f407]) ).
fof(f587,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f30]) ).
fof(f615,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f617,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f689,plain,
! [X0,X1] :
( subset(relation_rng_restriction(X0,X1),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f278]) ).
fof(f699,plain,
relation(sK56),
inference(cnf_transformation,[],[f455]) ).
fof(f700,plain,
relation_dom_restriction(relation_rng_restriction(sK54,sK56),sK55) != relation_rng_restriction(sK54,relation_dom_restriction(sK56,sK55)),
inference(cnf_transformation,[],[f455]) ).
fof(f716,plain,
! [X0,X1] :
( in(sK57(X0,X1),X1)
| in(sK57(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f457]) ).
fof(f717,plain,
! [X0,X1] :
( ~ in(sK57(X0,X1),X1)
| X0 = X1
| ~ in(sK57(X0,X1),X0) ),
inference(cnf_transformation,[],[f457]) ).
fof(f776,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f177]) ).
fof(f791,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f346]) ).
fof(f805,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f587,f776]) ).
fof(f816,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,[],[f494,f805,f805]) ).
fof(f817,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,[],[f493,f805]) ).
fof(f822,plain,
! [X2,X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X2)
| ~ in(X6,X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X1)
| relation_rng_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f500,f805,f805]) ).
fof(f823,plain,
! [X2,X0,X1,X6,X5] :
( in(X6,X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X2)
| relation_rng_restriction(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f499,f805]) ).
fof(f826,plain,
! [X0,X4] :
( ~ in(X4,X0)
| unordered_pair(unordered_pair(sK7(X4),sK8(X4)),unordered_pair(sK7(X4),sK7(X4))) = X4
| ~ relation(X0) ),
inference(definition_unfolding,[],[f504,f805]) ).
fof(f925,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,[],[f816]) ).
fof(f926,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,[],[f817]) ).
fof(f928,plain,
! [X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_rng_restriction(X0,X1))
| ~ in(X6,X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X1)
| ~ relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(equality_resolution,[],[f822]) ).
fof(f929,plain,
! [X0,X1,X6,X5] :
( in(X6,X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_rng_restriction(X0,X1))
| ~ relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(equality_resolution,[],[f823]) ).
fof(f983,definition,
sF64 = relation_rng_restriction(sK54,sK56),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
fof(f984,plain,
relation_rng_restriction(sK54,sK56) = sF64,
inference(reorient_equations,[],[f983]) ).
fof(f985,definition,
sF65 = relation_dom_restriction(sF64,sK55),
introduced(definition,[new_symbols(definition,[sF65])],[function_definition]) ).
fof(f986,plain,
relation_dom_restriction(sF64,sK55) = sF65,
inference(reorient_equations,[],[f985]) ).
fof(f987,definition,
sF66 = relation_dom_restriction(sK56,sK55),
introduced(definition,[new_symbols(definition,[sF66])],[function_definition]) ).
fof(f988,plain,
relation_dom_restriction(sK56,sK55) = sF66,
inference(reorient_equations,[],[f987]) ).
fof(f989,definition,
sF67 = relation_rng_restriction(sK54,sF66),
introduced(definition,[new_symbols(definition,[sF67])],[function_definition]) ).
fof(f990,plain,
relation_rng_restriction(sK54,sF66) = sF67,
inference(reorient_equations,[],[f989]) ).
fof(f991,plain,
sF65 != sF67,
inference(definition_folding,[],[f700,f990,f988,f986,f984]) ).
fof(f1003,plain,
! [X0,X1,X6,X5] :
( ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_rng_restriction(X0,X1))
| in(X6,X0)
| ~ relation(X1) ),
inference(forward_subsumption_resolution,[],[f929,f617]) ).
fof(f1004,plain,
! [X0,X1,X6,X5] :
( in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),relation_rng_restriction(X0,X1))
| ~ in(X6,X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5)),X1)
| ~ relation(X1) ),
inference(forward_subsumption_resolution,[],[f928,f617]) ).
fof(f1006,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,[],[f926,f615]) ).
fof(f1007,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,[],[f925,f615]) ).
fof(f1013,plain,
( relation(sF66)
| ~ relation(sK56) ),
inference(superposition,[],[f615,f988]) ).
fof(f1014,plain,
relation(sF66),
inference(forward_subsumption_resolution,[],[f1013,f699]) ).
fof(f1016,definition,
( spl68_1
<=> relation(sF64) ),
introduced(definition,[new_symbols(definition,[spl68_1])],[avatar_definition]) ).
fof(f1017,plain,
( relation(sF64)
| ~ spl68_1 ),
inference(avatar_component_clause,[],[f1016]) ).
fof(f1018,plain,
( ~ relation(sF64)
| spl68_1 ),
inference(avatar_component_clause,[],[f1016]) ).
fof(f1025,plain,
( relation(sF64)
| ~ relation(sK56) ),
inference(superposition,[],[f617,f984]) ).
fof(f1026,plain,
( ~ relation(sK56)
| spl68_1 ),
inference(forward_subsumption_resolution,[],[f1025,f1018]) ).
fof(f1028,plain,
( $false
| spl68_1 ),
inference(forward_subsumption_resolution,[],[f1026,f699]) ).
fof(f1029,plain,
spl68_1,
inference(avatar_contradiction_clause,[],[f1028]) ).
fof(f1030,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF67)
| in(X1,sK54)
| ~ relation(sF66) ),
inference(superposition,[],[f1003,f990]) ).
fof(f1031,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64)
| in(X1,sK54)
| ~ relation(sK56) ),
inference(superposition,[],[f1003,f984]) ).
fof(f1032,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64)
| in(X1,sK54) ),
inference(forward_subsumption_resolution,[],[f1031,f699]) ).
fof(f1033,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF67)
| in(X1,sK54) ),
inference(forward_subsumption_resolution,[],[f1030,f1014]) ).
fof(f1034,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF65)
| in(X0,sK55)
| ~ relation(sF64) ),
inference(superposition,[],[f1006,f986]) ).
fof(f1035,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66)
| in(X0,sK55)
| ~ relation(sK56) ),
inference(superposition,[],[f1006,f988]) ).
fof(f1036,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66)
| in(X0,sK55) ),
inference(forward_subsumption_resolution,[],[f1035,f699]) ).
fof(f1037,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF65)
| in(X0,sK55) )
| ~ spl68_1 ),
inference(forward_subsumption_resolution,[],[f1034,f1017]) ).
fof(f1042,plain,
( subset(sF67,sF66)
| ~ relation(sF66) ),
inference(superposition,[],[f689,f990]) ).
fof(f1043,plain,
( subset(sF64,sK56)
| ~ relation(sK56) ),
inference(superposition,[],[f689,f984]) ).
fof(f1044,plain,
subset(sF64,sK56),
inference(forward_subsumption_resolution,[],[f1043,f699]) ).
fof(f1045,plain,
subset(sF67,sF66),
inference(forward_subsumption_resolution,[],[f1042,f1014]) ).
fof(f1050,plain,
( subset(sF65,sF64)
| ~ relation(sF64) ),
inference(superposition,[],[f791,f986]) ).
fof(f1051,plain,
( subset(sF66,sK56)
| ~ relation(sK56) ),
inference(superposition,[],[f791,f988]) ).
fof(f1052,plain,
subset(sF66,sK56),
inference(forward_subsumption_resolution,[],[f1051,f699]) ).
fof(f1053,plain,
( subset(sF65,sF64)
| ~ spl68_1 ),
inference(forward_subsumption_resolution,[],[f1050,f1017]) ).
fof(f1130,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF67)
| ~ in(X1,sK54)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66)
| ~ relation(sF66) ),
inference(superposition,[],[f1004,f990]) ).
fof(f1131,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64)
| ~ in(X1,sK54)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK56)
| ~ relation(sK56) ),
inference(superposition,[],[f1004,f984]) ).
fof(f1136,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK56)
| ~ in(X1,sK54)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64) ),
inference(forward_subsumption_resolution,[],[f1131,f699]) ).
fof(f1137,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66)
| ~ in(X1,sK54)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF67) ),
inference(forward_subsumption_resolution,[],[f1130,f1014]) ).
fof(f1154,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF65)
| ~ in(X0,sK55)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64)
| ~ relation(sF64) ),
inference(superposition,[],[f1007,f986]) ).
fof(f1155,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66)
| ~ in(X0,sK55)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK56)
| ~ relation(sK56) ),
inference(superposition,[],[f1007,f988]) ).
fof(f1160,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK56)
| ~ in(X0,sK55)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF66) ),
inference(forward_subsumption_resolution,[],[f1155,f699]) ).
fof(f1161,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF64)
| ~ in(X0,sK55)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF65) )
| ~ spl68_1 ),
inference(forward_subsumption_resolution,[],[f1154,f1017]) ).
fof(f1424,plain,
! [X0] :
( ~ in(X0,sF64)
| in(X0,sK56) ),
inference(resolution,[],[f556,f1044]) ).
fof(f1425,plain,
( ! [X0] :
( ~ in(X0,sF65)
| in(X0,sF64) )
| ~ spl68_1 ),
inference(resolution,[],[f556,f1053]) ).
fof(f1426,plain,
! [X0] :
( ~ in(X0,sF66)
| in(X0,sK56) ),
inference(resolution,[],[f556,f1052]) ).
fof(f1427,plain,
! [X0] :
( ~ in(X0,sF67)
| in(X0,sF66) ),
inference(resolution,[],[f556,f1045]) ).
fof(f1557,plain,
! [X0] :
( in(sK57(sF67,X0),sF66)
| in(sK57(sF67,X0),X0)
| sF67 = X0 ),
inference(resolution,[],[f716,f1427]) ).
fof(f3289,plain,
( in(sK57(sF67,sF65),sF66)
| sF65 = sF67
| in(sK57(sF67,sF65),sF64)
| ~ spl68_1 ),
inference(resolution,[],[f1557,f1425]) ).
fof(f3297,plain,
( in(sK57(sF67,sF65),sF66)
| in(sK57(sF67,sF65),sF64)
| ~ spl68_1 ),
inference(forward_subsumption_resolution,[],[f3289,f991]) ).
fof(f3787,definition,
( spl68_150
<=> in(sK57(sF67,sF65),sF64) ),
introduced(definition,[new_symbols(definition,[spl68_150])],[avatar_definition]) ).
fof(f3788,plain,
( ~ in(sK57(sF67,sF65),sF64)
| spl68_150 ),
inference(avatar_component_clause,[],[f3787]) ).
fof(f3789,plain,
( in(sK57(sF67,sF65),sF64)
| ~ spl68_150 ),
inference(avatar_component_clause,[],[f3787]) ).
fof(f3791,definition,
( spl68_151
<=> in(sK57(sF67,sF65),sF66) ),
introduced(definition,[new_symbols(definition,[spl68_151])],[avatar_definition]) ).
fof(f3792,plain,
( ~ in(sK57(sF67,sF65),sF66)
| spl68_151 ),
inference(avatar_component_clause,[],[f3791]) ).
fof(f3793,plain,
( in(sK57(sF67,sF65),sF66)
| ~ spl68_151 ),
inference(avatar_component_clause,[],[f3791]) ).
fof(f3794,plain,
( spl68_150
| spl68_151
| ~ spl68_1 ),
inference(avatar_split_clause,[],[f3297,f1016,f3791,f3787]) ).
fof(f3815,plain,
( in(sK57(sF67,sF65),sK56)
| ~ spl68_150 ),
inference(resolution,[],[f3789,f1424]) ).
fof(f3816,plain,
( sK57(sF67,sF65) = unordered_pair(unordered_pair(sK7(sK57(sF67,sF65)),sK8(sK57(sF67,sF65))),unordered_pair(sK7(sK57(sF67,sF65)),sK7(sK57(sF67,sF65))))
| ~ relation(sF64)
| ~ spl68_150 ),
inference(resolution,[],[f3789,f826]) ).
fof(f3817,plain,
( sK57(sF67,sF65) = unordered_pair(unordered_pair(sK7(sK57(sF67,sF65)),sK8(sK57(sF67,sF65))),unordered_pair(sK7(sK57(sF67,sF65)),sK7(sK57(sF67,sF65))))
| ~ spl68_1
| ~ spl68_150 ),
inference(forward_subsumption_resolution,[],[f3816,f1017]) ).
fof(f3847,plain,
( ~ in(sK57(sF67,sF65),sF64)
| in(sK8(sK57(sF67,sF65)),sK54)
| ~ spl68_1
| ~ spl68_150 ),
inference(superposition,[],[f1032,f3817]) ).
fof(f3850,plain,
( ~ in(sK57(sF67,sF65),sF65)
| in(sK7(sK57(sF67,sF65)),sK55)
| ~ spl68_1
| ~ spl68_150 ),
inference(superposition,[],[f1037,f3817]) ).
fof(f3857,plain,
( ~ in(sK57(sF67,sF65),sK56)
| ~ in(sK7(sK57(sF67,sF65)),sK55)
| in(sK57(sF67,sF65),sF66)
| ~ spl68_1
| ~ spl68_150 ),
inference(superposition,[],[f1160,f3817]) ).
fof(f3858,plain,
( ~ in(sK57(sF67,sF65),sF64)
| ~ in(sK7(sK57(sF67,sF65)),sK55)
| in(sK57(sF67,sF65),sF65)
| ~ spl68_1
| ~ spl68_150 ),
inference(superposition,[],[f1161,f3817]) ).
fof(f4044,plain,
( ~ in(sK7(sK57(sF67,sF65)),sK55)
| in(sK57(sF67,sF65),sF65)
| ~ spl68_1
| ~ spl68_150 ),
inference(forward_subsumption_resolution,[],[f3858,f3789]) ).
fof(f4045,plain,
( ~ in(sK7(sK57(sF67,sF65)),sK55)
| in(sK57(sF67,sF65),sF66)
| ~ spl68_1
| ~ spl68_150 ),
inference(forward_subsumption_resolution,[],[f3857,f3815]) ).
fof(f4047,definition,
( spl68_175
<=> in(sK57(sF67,sF65),sF67) ),
introduced(definition,[new_symbols(definition,[spl68_175])],[avatar_definition]) ).
fof(f4048,plain,
( ~ in(sK57(sF67,sF65),sF67)
| spl68_175 ),
inference(avatar_component_clause,[],[f4047]) ).
fof(f4049,plain,
( in(sK57(sF67,sF65),sF67)
| ~ spl68_175 ),
inference(avatar_component_clause,[],[f4047]) ).
fof(f4051,definition,
( spl68_176
<=> in(sK8(sK57(sF67,sF65)),sK54) ),
introduced(definition,[new_symbols(definition,[spl68_176])],[avatar_definition]) ).
fof(f4056,definition,
( spl68_177
<=> in(sK7(sK57(sF67,sF65)),sK55) ),
introduced(definition,[new_symbols(definition,[spl68_177])],[avatar_definition]) ).
fof(f4060,definition,
( spl68_178
<=> in(sK57(sF67,sF65),sF65) ),
introduced(definition,[new_symbols(definition,[spl68_178])],[avatar_definition]) ).
fof(f4061,plain,
( in(sK57(sF67,sF65),sF65)
| ~ spl68_178 ),
inference(avatar_component_clause,[],[f4060]) ).
fof(f4062,plain,
( ~ in(sK57(sF67,sF65),sF65)
| spl68_178 ),
inference(avatar_component_clause,[],[f4060]) ).
fof(f4063,plain,
( spl68_177
| ~ spl68_178
| ~ spl68_1
| ~ spl68_150 ),
inference(avatar_split_clause,[],[f3850,f3787,f1016,f4060,f4056]) ).
fof(f4066,plain,
( in(sK8(sK57(sF67,sF65)),sK54)
| ~ spl68_1
| ~ spl68_150 ),
inference(forward_subsumption_resolution,[],[f3847,f3789]) ).
fof(f4067,plain,
( spl68_178
| ~ spl68_177
| ~ spl68_1
| ~ spl68_150 ),
inference(avatar_split_clause,[],[f4044,f3787,f1016,f4056,f4060]) ).
fof(f4068,plain,
( spl68_151
| ~ spl68_177
| ~ spl68_1
| ~ spl68_150 ),
inference(avatar_split_clause,[],[f4045,f3787,f1016,f4056,f3791]) ).
fof(f4069,plain,
( spl68_176
| ~ spl68_1
| ~ spl68_150 ),
inference(avatar_split_clause,[],[f4066,f3787,f1016,f4051]) ).
fof(f4070,plain,
( in(sK57(sF67,sF65),sK56)
| ~ spl68_151 ),
inference(resolution,[],[f3793,f1426]) ).
fof(f4071,plain,
( sK57(sF67,sF65) = unordered_pair(unordered_pair(sK7(sK57(sF67,sF65)),sK8(sK57(sF67,sF65))),unordered_pair(sK7(sK57(sF67,sF65)),sK7(sK57(sF67,sF65))))
| ~ relation(sF66)
| ~ spl68_151 ),
inference(resolution,[],[f3793,f826]) ).
fof(f4072,plain,
( sK57(sF67,sF65) = unordered_pair(unordered_pair(sK7(sK57(sF67,sF65)),sK8(sK57(sF67,sF65))),unordered_pair(sK7(sK57(sF67,sF65)),sK7(sK57(sF67,sF65))))
| ~ spl68_151 ),
inference(forward_subsumption_resolution,[],[f4071,f1014]) ).
fof(f4082,plain,
( ~ in(sK57(sF67,sF65),sF67)
| in(sK8(sK57(sF67,sF65)),sK54)
| ~ spl68_151 ),
inference(superposition,[],[f1033,f4072]) ).
fof(f4083,plain,
( ~ in(sK57(sF67,sF65),sF66)
| in(sK7(sK57(sF67,sF65)),sK55)
| ~ spl68_151 ),
inference(superposition,[],[f1036,f4072]) ).
fof(f4089,plain,
( ~ in(sK57(sF67,sF65),sK56)
| ~ in(sK8(sK57(sF67,sF65)),sK54)
| in(sK57(sF67,sF65),sF64)
| ~ spl68_151 ),
inference(superposition,[],[f1136,f4072]) ).
fof(f4090,plain,
( ~ in(sK57(sF67,sF65),sF66)
| ~ in(sK8(sK57(sF67,sF65)),sK54)
| in(sK57(sF67,sF65),sF67)
| ~ spl68_151 ),
inference(superposition,[],[f1137,f4072]) ).
fof(f4186,plain,
( ~ in(sK8(sK57(sF67,sF65)),sK54)
| in(sK57(sF67,sF65),sF67)
| ~ spl68_151 ),
inference(forward_subsumption_resolution,[],[f4090,f3793]) ).
fof(f4187,plain,
( ~ in(sK8(sK57(sF67,sF65)),sK54)
| in(sK57(sF67,sF65),sF64)
| ~ spl68_151 ),
inference(forward_subsumption_resolution,[],[f4089,f4070]) ).
fof(f4189,plain,
( in(sK7(sK57(sF67,sF65)),sK55)
| ~ spl68_151 ),
inference(forward_subsumption_resolution,[],[f4083,f3793]) ).
fof(f4190,plain,
( spl68_176
| ~ spl68_175
| ~ spl68_151 ),
inference(avatar_split_clause,[],[f4082,f3791,f4047,f4051]) ).
fof(f4191,plain,
( spl68_175
| ~ spl68_176
| ~ spl68_151 ),
inference(avatar_split_clause,[],[f4186,f3791,f4051,f4047]) ).
fof(f4192,plain,
( ~ in(sK8(sK57(sF67,sF65)),sK54)
| spl68_150
| ~ spl68_151 ),
inference(forward_subsumption_resolution,[],[f4187,f3788]) ).
fof(f4193,plain,
( spl68_177
| ~ spl68_151 ),
inference(avatar_split_clause,[],[f4189,f3791,f4056]) ).
fof(f4194,plain,
( ~ spl68_176
| spl68_150
| ~ spl68_151 ),
inference(avatar_split_clause,[],[f4192,f3791,f3787,f4051]) ).
fof(f4199,plain,
( in(sK57(sF67,sF65),sF66)
| sF65 = sF67
| spl68_178 ),
inference(resolution,[],[f4062,f1557]) ).
fof(f4200,plain,
( sF65 = sF67
| spl68_151
| spl68_178 ),
inference(forward_subsumption_resolution,[],[f4199,f3792]) ).
fof(f4201,plain,
( $false
| spl68_151
| spl68_178 ),
inference(forward_subsumption_resolution,[],[f4200,f991]) ).
fof(f4202,plain,
( spl68_151
| spl68_178 ),
inference(avatar_contradiction_clause,[],[f4201]) ).
fof(f4204,plain,
( in(sK57(sF67,sF65),sF65)
| sF65 = sF67
| spl68_175 ),
inference(resolution,[],[f4048,f716]) ).
fof(f4205,plain,
( sF65 = sF67
| spl68_175
| spl68_178 ),
inference(forward_subsumption_resolution,[],[f4204,f4062]) ).
fof(f4206,plain,
( $false
| spl68_175
| spl68_178 ),
inference(forward_subsumption_resolution,[],[f4205,f991]) ).
fof(f4207,plain,
( spl68_175
| spl68_178 ),
inference(avatar_contradiction_clause,[],[f4206]) ).
fof(f4211,plain,
( sF65 = sF67
| ~ in(sK57(sF67,sF65),sF67)
| ~ spl68_178 ),
inference(resolution,[],[f4061,f717]) ).
fof(f4212,plain,
( in(sK57(sF67,sF65),sF64)
| ~ spl68_1
| ~ spl68_178 ),
inference(resolution,[],[f4061,f1425]) ).
fof(f4214,plain,
( $false
| ~ spl68_1
| spl68_150
| ~ spl68_178 ),
inference(forward_subsumption_resolution,[],[f4212,f3788]) ).
fof(f4215,plain,
( ~ spl68_1
| spl68_150
| ~ spl68_178 ),
inference(avatar_contradiction_clause,[],[f4214]) ).
fof(f4216,plain,
( ~ in(sK57(sF67,sF65),sF67)
| ~ spl68_178 ),
inference(forward_subsumption_resolution,[],[f4211,f991]) ).
fof(f4217,plain,
( $false
| ~ spl68_175
| ~ spl68_178 ),
inference(forward_subsumption_resolution,[],[f4216,f4049]) ).
fof(f4218,plain,
( ~ spl68_175
| ~ spl68_178 ),
inference(avatar_contradiction_clause,[],[f4217]) ).
cnf(s2,plain,
spl68_1,
inference(sat_conversion,[],[f1029]) ).
cnf(s155,plain,
( ~ spl68_1
| spl68_150
| spl68_151 ),
inference(sat_conversion,[],[f3794]) ).
cnf(s186,plain,
( ~ spl68_1
| ~ spl68_150
| spl68_177
| ~ spl68_178 ),
inference(sat_conversion,[],[f4063]) ).
cnf(s189,plain,
( ~ spl68_1
| ~ spl68_150
| ~ spl68_177
| spl68_178 ),
inference(sat_conversion,[],[f4067]) ).
cnf(s190,plain,
( ~ spl68_1
| ~ spl68_150
| spl68_151
| ~ spl68_177 ),
inference(sat_conversion,[],[f4068]) ).
cnf(s191,plain,
( ~ spl68_1
| ~ spl68_150
| spl68_176 ),
inference(sat_conversion,[],[f4069]) ).
cnf(s222,plain,
( ~ spl68_151
| ~ spl68_175
| spl68_176 ),
inference(sat_conversion,[],[f4190]) ).
cnf(s223,plain,
( ~ spl68_151
| spl68_175
| ~ spl68_176 ),
inference(sat_conversion,[],[f4191]) ).
cnf(s224,plain,
( ~ spl68_151
| spl68_177 ),
inference(sat_conversion,[],[f4193]) ).
cnf(s225,plain,
( spl68_150
| ~ spl68_151
| ~ spl68_176 ),
inference(sat_conversion,[],[f4194]) ).
cnf(s226,plain,
( spl68_151
| spl68_178 ),
inference(sat_conversion,[],[f4202]) ).
cnf(s227,plain,
( spl68_175
| spl68_178 ),
inference(sat_conversion,[],[f4207]) ).
cnf(s228,plain,
( ~ spl68_1
| spl68_150
| ~ spl68_178 ),
inference(sat_conversion,[],[f4215]) ).
cnf(s229,plain,
( ~ spl68_175
| ~ spl68_178 ),
inference(sat_conversion,[],[f4218]) ).
cnf(s235,plain,
spl68_150,
inference(rat,[],[s222,s227,s225,s155,s228,s2]) ).
cnf(s236,plain,
spl68_176,
inference(rat,[],[s191,s2,s235]) ).
cnf(s237,plain,
~ spl68_151,
inference(rat,[],[s229,s189,s223,s224,s2,s235,s236]) ).
cnf(s238,plain,
spl68_178,
inference(rat,[],[s226,s237]) ).
cnf(s239,plain,
~ spl68_177,
inference(rat,[],[s190,s235,s2,s237]) ).
cnf(s241,plain,
$false,
inference(rat,[],[s186,s235,s2,s238,s239]) ).
fof(f4219,plain,
$false,
inference(avatar_sat_refutation,[],[s241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU202+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 04:01:32 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 5.83/2.20 % (421705)Detected formulas, will run a generic FOF schedule.
% 5.83/2.20 % (421714)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=162694683:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.83/2.20 % (421715)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=709638791:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.83/2.20 % (421710)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=1674724418:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.83/2.20 % (421713)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=405015747:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.83/2.20 % (421711)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=450865002:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.83/2.20 % (421712)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=1910247916:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.83/2.20 % (421716)dis-21_1_sil=8000:lcm=predicate:random_seed=3664477548: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)
% 5.83/2.20 % (421714)Instruction limit reached!
% 5.83/2.20 % (421714)------------------------------
% 5.83/2.20 % (421714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421714)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421714)Termination reason: Instruction limit
% 5.83/2.20 % (421714)Termination phase: Saturation
% 5.83/2.20 % (421714)Time elapsed: 0.043 s
% 5.83/2.20 % (421714)Peak memory usage: 89 MB
% 5.83/2.20 % (421714)Instructions burned: 121 (million)
% 5.83/2.20 % (421713)Instruction limit reached!
% 5.83/2.20 % (421713)------------------------------
% 5.83/2.20 % (421713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421713)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421713)Termination reason: Instruction limit
% 5.83/2.20 % (421713)Termination phase: Saturation
% 5.83/2.20 % (421713)Time elapsed: 0.073 s
% 5.83/2.20 % (421713)Peak memory usage: 90 MB
% 5.83/2.20 % (421713)Instructions burned: 110 (million)
% 5.83/2.20 % (421716)Instruction limit reached!
% 5.83/2.20 % (421716)------------------------------
% 5.83/2.20 % (421716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421716)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421716)Termination reason: Instruction limit
% 5.83/2.20 % (421716)Termination phase: Saturation
% 5.83/2.20 % (421716)Time elapsed: 0.079 s
% 5.83/2.20 % (421716)Peak memory usage: 90 MB
% 5.83/2.20 % (421716)Instructions burned: 130 (million)
% 5.83/2.20 % (421715)Instruction limit reached!
% 5.83/2.20 % (421715)------------------------------
% 5.83/2.20 % (421715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421715)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421715)Termination reason: Instruction limit
% 5.83/2.20 % (421715)Termination phase: Saturation
% 5.83/2.20 % (421715)Time elapsed: 0.098 s
% 5.83/2.20 % (421715)Peak memory usage: 90 MB
% 5.83/2.20 % (421715)Instructions burned: 139 (million)
% 5.83/2.20 % (421724)lrs+10_1_sil=8000:sp=occurrence:random_seed=2189313286:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 5.83/2.20 % (421724)Instruction limit reached!
% 5.83/2.20 % (421724)------------------------------
% 5.83/2.20 % (421724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421724)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421724)Termination reason: Instruction limit
% 5.83/2.20 % (421724)Termination phase: Saturation
% 5.83/2.20 % (421724)Time elapsed: 0.103 s
% 5.83/2.20 % (421724)Peak memory usage: 92 MB
% 5.83/2.20 % (421724)Instructions burned: 287 (million)
% 5.83/2.20 % (421725)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4002962668:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.83/2.20 % (421726)lrs+1011_1_sil=32000:sp=occurrence:random_seed=266004011:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.83/2.20 % (421727)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=2838135518:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.83/2.20 % (421725)Instruction limit reached!
% 5.83/2.20 % (421725)------------------------------
% 5.83/2.20 % (421725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421725)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421725)Termination reason: Instruction limit
% 5.83/2.20 % (421725)Termination phase: Saturation
% 5.83/2.20 % (421725)Time elapsed: 0.095 s
% 5.83/2.20 % (421725)Peak memory usage: 90 MB
% 5.83/2.20 % (421725)Instructions burned: 157 (million)
% 5.83/2.20 % (421731)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2757622430:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 5.83/2.20 % (421727)Instruction limit reached!
% 5.83/2.20 % (421727)------------------------------
% 5.83/2.20 % (421727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421727)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421727)Termination reason: Instruction limit
% 5.83/2.20 % (421727)Termination phase: Saturation
% 5.83/2.20 % (421727)Time elapsed: 0.149 s
% 5.83/2.20 % (421727)Peak memory usage: 93 MB
% 5.83/2.20 % (421727)Instructions burned: 249 (million)
% 5.83/2.20 % (421731)Instruction limit reached!
% 5.83/2.20 % (421731)------------------------------
% 5.83/2.20 % (421731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421731)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421731)Termination reason: Instruction limit
% 5.83/2.20 % (421731)Termination phase: Saturation
% 5.83/2.20 % (421731)Time elapsed: 0.101 s
% 5.83/2.20 % (421731)Peak memory usage: 90 MB
% 5.83/2.20 % (421731)Instructions burned: 297 (million)
% 5.83/2.20 % (421726)Instruction limit reached!
% 5.83/2.20 % (421726)------------------------------
% 5.83/2.20 % (421726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421726)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421726)Termination reason: Instruction limit
% 5.83/2.20 % (421726)Termination phase: Saturation
% 5.83/2.20 % (421726)Time elapsed: 0.224 s
% 5.83/2.20 % (421726)Peak memory usage: 93 MB
% 5.83/2.20 % (421726)Instructions burned: 326 (million)
% 5.83/2.20 % (421733)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=440002095:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 5.83/2.20 % (421735)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3295978761:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.83/2.20 % (421736)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3443277317:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.83/2.20 % (421736)Instruction limit reached!
% 5.83/2.20 % (421736)------------------------------
% 5.83/2.20 % (421736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421736)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421736)Termination reason: Instruction limit
% 5.83/2.20 % (421736)Termination phase: Saturation
% 5.83/2.20 % (421736)Time elapsed: 0.035 s
% 5.83/2.20 % (421736)Peak memory usage: 89 MB
% 5.83/2.20 % (421736)Instructions burned: 131 (million)
% 5.83/2.20 % (421737)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3456544224:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 5.83/2.20 % (421735)Instruction limit reached!
% 5.83/2.20 % (421735)------------------------------
% 5.83/2.20 % (421735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421735)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421735)Termination reason: Instruction limit
% 5.83/2.20 % (421735)Termination phase: Saturation
% 5.83/2.20 % (421735)Time elapsed: 0.069 s
% 5.83/2.20 % (421735)Peak memory usage: 90 MB
% 5.83/2.20 % (421735)Instructions burned: 115 (million)
% 5.83/2.20 % (421737)Instruction limit reached!
% 5.83/2.20 % (421737)------------------------------
% 5.83/2.20 % (421737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421737)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421737)Termination reason: Instruction limit
% 5.83/2.20 % (421737)Termination phase: Saturation
% 5.83/2.20 % (421737)Time elapsed: 0.068 s
% 5.83/2.20 % (421737)Peak memory usage: 89 MB
% 5.83/2.20 % (421737)Instructions burned: 115 (million)
% 5.83/2.20 % (421741)lrs+10_1_sil=8000:sp=occurrence:random_seed=987427338:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 5.83/2.20 % (421743)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3008888483:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 5.83/2.20 % (421744)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2299019456:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 5.83/2.20 % (421710)First to succeed.
% 5.83/2.20 % (421710)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-421705"
% 5.83/2.20 % (421741)Instruction limit reached!
% 5.83/2.20 % (421741)------------------------------
% 5.83/2.20 % (421741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421741)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421741)Termination reason: Instruction limit
% 5.83/2.20 % (421741)Termination phase: Saturation
% 5.83/2.20 % (421741)Time elapsed: 0.311 s
% 5.83/2.20 % (421741)Peak memory usage: 99 MB
% 5.83/2.20 % (421741)Instructions burned: 908 (million)
% 5.83/2.20 % (421743)Instruction limit reached!
% 5.83/2.20 % (421743)------------------------------
% 5.83/2.20 % (421743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.20 % (421743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.20 % (421743)CaDiCaL version: 2.1.3
% 5.83/2.20 % (421743)Termination reason: Instruction limit
% 5.83/2.20 % (421743)Termination phase: Saturation
% 5.83/2.20 % (421743)Time elapsed: 0.283 s
% 5.83/2.20 % (421743)Peak memory usage: 93 MB
% 5.83/2.20 % (421743)Instructions burned: 437 (million)
% 5.83/2.20 % (421710)Refutation found. Thanks to Tanya!
% 5.83/2.20 % SZS status Theorem for theBenchmark
% 5.83/2.20 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/2.40 % (421710)------------------------------
% 0.16/2.40 % (421710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.40 % (421710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.40 % (421710)CaDiCaL version: 2.1.3
% 0.16/2.40 % (421710)Termination reason: Refutation
% 0.16/2.40 % (421710)Time elapsed: 0.904 s
% 0.16/2.40 % (421710)Peak memory usage: 133 MB
% 0.16/2.40 % (421710)Instructions burned: 1392 (million)
% 0.16/2.40 % (421710)------------------------------
% 0.16/2.40 % (421710)------------------------------
% 0.16/2.40 % (421705)Success in time 1.338 s
% 0.16/2.40 % Vampire exiting
%------------------------------------------------------------------------------