%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU246+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 : n004.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:59 PM UTC 2026
% Result : Theorem 9.06s 2.31s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 25
% Syntax : Number of formulae : 202 ( 28 unt; 9 def)
% Number of atoms : 710 ( 75 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 891 ( 383 ~; 399 |; 72 &)
% ( 22 <=>; 14 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 7 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-3 aty)
% Number of variables : 384 ( 0 sgn 358 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f15,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(f17,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(f26,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(f41,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f55,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(f99,axiom,
! [X0,X1] :
( relation(X0)
=> relation(relation_dom_restriction(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f101,axiom,
! [X0,X1] :
( relation(X1)
=> relation(relation_rng_restriction(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relat_1) ).
fof(f179,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f184,axiom,
! [X0,X1] :
( relation(X1)
=> subset(relation_rng_restriction(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_relat_1) ).
fof(f191,axiom,
! [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(f202,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(X0,relation_restriction(X2,X1))
<=> ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_wellord1) ).
fof(f205,conjecture,
! [X0,X1] :
( relation(X1)
=> relation_restriction(X1,X0) = relation_dom_restriction(relation_rng_restriction(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_wellord1) ).
fof(f206,negated_conjecture,
~ ! [X0,X1] :
( relation(X1)
=> relation_restriction(X1,X0) = relation_dom_restriction(relation_rng_restriction(X0,X1),X0) ),
inference(negated_conjecture,[status(cth)],[f205]) ).
fof(f226,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
<=> in(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f281,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f293,axiom,
! [X0,X1] :
( relation(X1)
=> subset(relation_dom_restriction(X1,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t88_relat_1) ).
fof(f331,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,[],[f15]) ).
fof(f334,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,[],[f17]) ).
fof(f343,plain,
! [X0] :
( relation(X0)
<=> ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f352,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f391,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(ennf_transformation,[],[f99]) ).
fof(f393,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(ennf_transformation,[],[f101]) ).
fof(f459,plain,
! [X0,X1] :
( subset(relation_rng_restriction(X0,X1),X1)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f184]) ).
fof(f468,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,[],[f191]) ).
fof(f482,plain,
! [X0,X1,X2] :
( ( in(X0,relation_restriction(X2,X1))
<=> ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) ) )
| ~ relation(X2) ),
inference(ennf_transformation,[],[f202]) ).
fof(f487,plain,
? [X0,X1] :
( relation_restriction(X1,X0) != relation_dom_restriction(relation_rng_restriction(X0,X1),X0)
& relation(X1) ),
inference(ennf_transformation,[],[f206]) ).
fof(f514,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( in(X2,X0)
<~> in(X2,X1) ) ),
inference(ennf_transformation,[],[f226]) ).
fof(f585,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f293]) ).
fof(f608,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,[],[f331]) ).
fof(f609,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,[],[f608]) ).
fof(f610,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,[],[f609]) ).
fof(f611,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))],[f610]) ).
fof(f615,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,[],[f334]) ).
fof(f616,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,[],[f615]) ).
fof(f617,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,[],[f616]) ).
fof(f618,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = relation_rng_restriction(X0,X1)
| ( ( ~ in(sK9(X0,X1,X2),X0)
| ~ in(ordered_pair(sK8(X0,X1,X2),sK9(X0,X1,X2)),X1)
| ~ in(ordered_pair(sK8(X0,X1,X2),sK9(X0,X1,X2)),X2) )
& ( ( in(sK9(X0,X1,X2),X0)
& in(ordered_pair(sK8(X0,X1,X2),sK9(X0,X1,X2)),X1) )
| in(ordered_pair(sK8(X0,X1,X2),sK9(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,[sK8,sK9]),skolemize(X3,sK8(X0,X1,X2)),skolemize(X4,sK9(X0,X1,X2))],[f617]) ).
fof(f636,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,[],[f343]) ).
fof(f637,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,[],[f636]) ).
fof(f638,plain,
! [X0] :
( ( relation(X0)
| ( in(sK18(X0),X0)
& ! [X2,X3] : ordered_pair(X2,X3) != sK18(X0) ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ordered_pair(sK19(X4),sK20(X4)) = X4 )
| ~ relation(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X1,sK18(X0)),skolemize(X5,sK19(X4)),skolemize(X6,sK20(X4))],[f637]) ).
fof(f681,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,[],[f352]) ).
fof(f682,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,[],[f681]) ).
fof(f683,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK44(X0,X1),X1)
& in(sK44(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X2,sK44(X0,X1))],[f682]) ).
fof(f776,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f179]) ).
fof(f777,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f776]) ).
fof(f787,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_restriction(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,cartesian_product2(X1,X1)) )
& ( ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) )
| ~ in(X0,relation_restriction(X2,X1)) ) )
| ~ relation(X2) ),
inference(nnf_transformation,[],[f482]) ).
fof(f788,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_restriction(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,cartesian_product2(X1,X1)) )
& ( ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) )
| ~ in(X0,relation_restriction(X2,X1)) ) )
| ~ relation(X2) ),
inference(flattening,[],[f787]) ).
fof(f789,plain,
( relation_restriction(sK105,sK104) != relation_dom_restriction(relation_rng_restriction(sK104,sK105),sK104)
& relation(sK105) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK104,sK105]),skolemize(X0,sK104),skolemize(X1,sK105)],[f487]) ).
fof(f792,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ in(X2,X1)
| ~ in(X2,X0) )
& ( in(X2,X1)
| in(X2,X0) ) ) ),
inference(nnf_transformation,[],[f514]) ).
fof(f793,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ in(sK106(X0,X1),X1)
| ~ in(sK106(X0,X1),X0) )
& ( in(sK106(X0,X1),X1)
| in(sK106(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK106]),skolemize(X2,sK106(X0,X1))],[f792]) ).
fof(f853,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f867,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,[],[f611]) ).
fof(f868,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,[],[f611]) ).
fof(f881,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,[],[f618]) ).
fof(f882,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,[],[f618]) ).
fof(f919,plain,
! [X0,X4] :
( ~ in(X4,X0)
| ordered_pair(sK19(X4),sK20(X4)) = X4
| ~ relation(X0) ),
inference(cnf_transformation,[],[f638]) ).
fof(f988,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f683]) ).
fof(f1049,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f55]) ).
fof(f1110,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f391]) ).
fof(f1112,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(cnf_transformation,[],[f393]) ).
fof(f1260,plain,
! [X2,X3,X0,X1] :
( in(X1,X3)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f777]) ).
fof(f1261,plain,
! [X2,X3,X0,X1] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f777]) ).
fof(f1262,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(cnf_transformation,[],[f777]) ).
fof(f1269,plain,
! [X0,X1] :
( subset(relation_rng_restriction(X0,X1),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f459]) ).
fof(f1279,plain,
! [X2,X0,X1] :
( ~ relation(X2)
| relation_dom_restriction(relation_rng_restriction(X0,X2),X1) = relation_rng_restriction(X0,relation_dom_restriction(X2,X1)) ),
inference(cnf_transformation,[],[f468]) ).
fof(f1296,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_restriction(X2,X1))
| in(X0,cartesian_product2(X1,X1))
| ~ relation(X2) ),
inference(cnf_transformation,[],[f788]) ).
fof(f1297,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_restriction(X2,X1))
| in(X0,X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f788]) ).
fof(f1298,plain,
! [X2,X0,X1] :
( ~ in(X0,cartesian_product2(X1,X1))
| ~ in(X0,X2)
| in(X0,relation_restriction(X2,X1))
| ~ relation(X2) ),
inference(cnf_transformation,[],[f788]) ).
fof(f1301,plain,
relation(sK105),
inference(cnf_transformation,[],[f789]) ).
fof(f1302,plain,
relation_restriction(sK105,sK104) != relation_dom_restriction(relation_rng_restriction(sK104,sK105),sK104),
inference(cnf_transformation,[],[f789]) ).
fof(f1326,plain,
! [X0,X1] :
( in(sK106(X0,X1),X1)
| in(sK106(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f793]) ).
fof(f1327,plain,
! [X0,X1] :
( ~ in(sK106(X0,X1),X1)
| X0 = X1
| ~ in(sK106(X0,X1),X0) ),
inference(cnf_transformation,[],[f793]) ).
fof(f1429,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f281]) ).
fof(f1448,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f585]) ).
fof(f1467,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f1049,f1429]) ).
fof(f1479,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,[],[f868,f1467,f1467]) ).
fof(f1480,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,[],[f867,f1467]) ).
fof(f1485,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,[],[f882,f1467,f1467]) ).
fof(f1486,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,[],[f881,f1467]) ).
fof(f1497,plain,
! [X0,X4] :
( ~ in(X4,X0)
| unordered_pair(unordered_pair(sK19(X4),sK20(X4)),unordered_pair(sK19(X4),sK19(X4))) = X4
| ~ relation(X0) ),
inference(definition_unfolding,[],[f919,f1467]) ).
fof(f1588,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(definition_unfolding,[],[f1262,f1467]) ).
fof(f1589,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),cartesian_product2(X2,X3))
| in(X0,X2) ),
inference(definition_unfolding,[],[f1261,f1467]) ).
fof(f1590,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),cartesian_product2(X2,X3))
| in(X1,X3) ),
inference(definition_unfolding,[],[f1260,f1467]) ).
fof(f1646,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,[],[f1479]) ).
fof(f1647,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,[],[f1480]) ).
fof(f1654,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,[],[f1485]) ).
fof(f1655,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,[],[f1486]) ).
fof(f1749,definition,
sF122 = relation_restriction(sK105,sK104),
introduced(definition,[new_symbols(definition,[sF122])],[function_definition]) ).
fof(f1750,plain,
relation_restriction(sK105,sK104) = sF122,
inference(reorient_equations,[],[f1749]) ).
fof(f1751,definition,
sF123 = relation_rng_restriction(sK104,sK105),
introduced(definition,[new_symbols(definition,[sF123])],[function_definition]) ).
fof(f1752,plain,
relation_rng_restriction(sK104,sK105) = sF123,
inference(reorient_equations,[],[f1751]) ).
fof(f1753,definition,
sF124 = relation_dom_restriction(sF123,sK104),
introduced(definition,[new_symbols(definition,[sF124])],[function_definition]) ).
fof(f1754,plain,
relation_dom_restriction(sF123,sK104) = sF124,
inference(reorient_equations,[],[f1753]) ).
fof(f1755,plain,
sF122 != sF124,
inference(definition_folding,[],[f1302,f1754,f1752,f1750]) ).
fof(f1776,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,[],[f1655,f1112]) ).
fof(f1777,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,[],[f1654,f1112]) ).
fof(f1779,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,[],[f1647,f1110]) ).
fof(f1780,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,[],[f1646,f1110]) ).
fof(f1790,definition,
( spl125_3
<=> relation(sF123) ),
introduced(definition,[new_symbols(definition,[spl125_3])],[avatar_definition]) ).
fof(f1791,plain,
( relation(sF123)
| ~ spl125_3 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1792,plain,
( ~ relation(sF123)
| spl125_3 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1799,plain,
( relation(sF123)
| ~ relation(sK105) ),
inference(superposition,[],[f1112,f1752]) ).
fof(f1800,plain,
( ~ relation(sK105)
| spl125_3 ),
inference(forward_subsumption_resolution,[],[f1799,f1792]) ).
fof(f1801,plain,
( $false
| spl125_3 ),
inference(forward_subsumption_resolution,[],[f1800,f1301]) ).
fof(f1802,plain,
spl125_3,
inference(avatar_contradiction_clause,[],[f1801]) ).
fof(f1806,plain,
! [X0,X1] : relation_dom_restriction(relation_rng_restriction(X0,sK105),X1) = relation_rng_restriction(X0,relation_dom_restriction(sK105,X1)),
inference(resolution,[],[f1301,f1279]) ).
fof(f1809,plain,
! [X0] :
( ~ in(X0,sF122)
| in(X0,sK105)
| ~ relation(sK105) ),
inference(superposition,[],[f1297,f1750]) ).
fof(f1810,plain,
! [X0] :
( ~ in(X0,sF122)
| in(X0,sK105) ),
inference(forward_subsumption_resolution,[],[f1809,f1301]) ).
fof(f1816,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X2,X3),unordered_pair(X2,X2)),relation_dom_restriction(relation_rng_restriction(X0,sK105),X1))
| in(X3,X0)
| ~ relation(relation_dom_restriction(sK105,X1)) ),
inference(superposition,[],[f1776,f1806]) ).
fof(f1818,plain,
! [X0] :
( ~ in(X0,sF122)
| in(X0,cartesian_product2(sK104,sK104))
| ~ relation(sK105) ),
inference(superposition,[],[f1296,f1750]) ).
fof(f1819,plain,
! [X0] :
( in(X0,cartesian_product2(sK104,sK104))
| ~ in(X0,sF122) ),
inference(forward_subsumption_resolution,[],[f1818,f1301]) ).
fof(f1822,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X2,X3),unordered_pair(X2,X2)),relation_dom_restriction(relation_rng_restriction(X0,sK105),X1))
| ~ in(X3,X0)
| ~ in(unordered_pair(unordered_pair(X2,X3),unordered_pair(X2,X2)),relation_dom_restriction(sK105,X1))
| ~ relation(relation_dom_restriction(sK105,X1)) ),
inference(superposition,[],[f1777,f1806]) ).
fof(f1844,plain,
( subset(sF124,sF123)
| ~ relation(sF123) ),
inference(superposition,[],[f1448,f1754]) ).
fof(f1845,plain,
( subset(sF124,sF123)
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f1844,f1791]) ).
fof(f1846,plain,
( subset(sF123,sK105)
| ~ relation(sK105) ),
inference(superposition,[],[f1269,f1752]) ).
fof(f1848,plain,
subset(sF123,sK105),
inference(forward_subsumption_resolution,[],[f1846,f1301]) ).
fof(f1908,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),relation_dom_restriction(X2,X3))
| in(X0,X3)
| ~ relation(X2) ),
inference(superposition,[],[f1779,f853]) ).
fof(f2018,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF124)
| in(X0,sK104)
| ~ relation(sF123) ),
inference(superposition,[],[f1908,f1754]) ).
fof(f2022,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF124)
| in(X0,sK104) )
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f2018,f1791]) ).
fof(f2047,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X2),unordered_pair(X0,X0)),relation_restriction(X3,X1))
| ~ in(X2,X1)
| ~ in(unordered_pair(unordered_pair(X0,X2),unordered_pair(X0,X0)),X3)
| ~ in(X0,X1)
| ~ relation(X3) ),
inference(resolution,[],[f1588,f1298]) ).
fof(f2058,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF122)
| ~ in(X1,sK104)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK105)
| ~ in(X0,sK104)
| ~ relation(sK105) ),
inference(superposition,[],[f2047,f1750]) ).
fof(f2061,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK105)
| ~ in(X1,sK104)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF122)
| ~ in(X0,sK104) ),
inference(forward_subsumption_resolution,[],[f2058,f1301]) ).
fof(f2065,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sK105)
| ~ in(X1,sK104)
| in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF122)
| ~ in(X0,sK104) ),
inference(superposition,[],[f2061,f853]) ).
fof(f2074,plain,
! [X0] :
( in(sK106(X0,sF122),sK105)
| in(sK106(X0,sF122),X0)
| sF122 = X0 ),
inference(resolution,[],[f1326,f1810]) ).
fof(f2233,definition,
( spl125_12
<=> relation(relation_dom_restriction(sK105,sK104)) ),
introduced(definition,[new_symbols(definition,[spl125_12])],[avatar_definition]) ).
fof(f2234,plain,
( relation(relation_dom_restriction(sK105,sK104))
| ~ spl125_12 ),
inference(avatar_component_clause,[],[f2233]) ).
fof(f2235,plain,
( ~ relation(relation_dom_restriction(sK105,sK104))
| spl125_12 ),
inference(avatar_component_clause,[],[f2233]) ).
fof(f2245,plain,
( ~ relation(sK105)
| spl125_12 ),
inference(resolution,[],[f2235,f1110]) ).
fof(f2246,plain,
( $false
| spl125_12 ),
inference(forward_subsumption_resolution,[],[f2245,f1301]) ).
fof(f2247,plain,
spl125_12,
inference(avatar_contradiction_clause,[],[f2246]) ).
fof(f2356,plain,
! [X0] :
( ~ in(X0,sF123)
| in(X0,sK105) ),
inference(resolution,[],[f988,f1848]) ).
fof(f2357,plain,
( ! [X0] :
( ~ in(X0,sF124)
| in(X0,sF123) )
| ~ spl125_3 ),
inference(resolution,[],[f988,f1845]) ).
fof(f2361,plain,
( in(sK106(sF124,sF122),sF123)
| in(sK106(sF124,sF122),sK105)
| sF122 = sF124
| ~ spl125_3 ),
inference(resolution,[],[f2357,f2074]) ).
fof(f2364,plain,
( in(sK106(sF124,sF122),sK105)
| sF122 = sF124
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f2361,f2356]) ).
fof(f2366,plain,
( in(sK106(sF124,sF122),sK105)
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f2364,f1755]) ).
fof(f2610,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),relation_dom_restriction(sK105,X2))
| ~ in(X1,sK104)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),relation_dom_restriction(sF123,X2))
| ~ relation(relation_dom_restriction(sK105,X2)) ),
inference(superposition,[],[f1822,f1752]) ).
fof(f3009,plain,
! [X2,X0,X1] :
( ~ in(X0,sK104)
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),relation_dom_restriction(sF123,X2))
| ~ relation(relation_dom_restriction(sK105,X2))
| ~ in(X1,X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK105)
| ~ relation(sK105) ),
inference(resolution,[],[f2610,f1780]) ).
fof(f3027,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),relation_dom_restriction(sF123,X2))
| ~ in(X0,sK104)
| ~ relation(relation_dom_restriction(sK105,X2))
| ~ in(X1,X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK105) ),
inference(forward_subsumption_resolution,[],[f3009,f1301]) ).
fof(f3072,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF124)
| ~ in(X1,sK104)
| ~ relation(relation_dom_restriction(sK105,sK104))
| ~ in(X0,sK104)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK105) ),
inference(superposition,[],[f3027,f1754]) ).
fof(f3074,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK105)
| ~ in(X1,sK104)
| ~ in(X0,sK104)
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF124) )
| ~ spl125_12 ),
inference(forward_subsumption_resolution,[],[f3072,f2234]) ).
fof(f3872,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sK105)
| ~ in(X1,sK104)
| ~ in(X0,sK104)
| in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF124) )
| ~ spl125_12 ),
inference(superposition,[],[f3074,f853]) ).
fof(f3922,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sF122)
| in(X0,sK104) ),
inference(resolution,[],[f1590,f1819]) ).
fof(f3932,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF122)
| in(X0,sK104) ),
inference(resolution,[],[f1589,f1819]) ).
fof(f4484,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),relation_dom_restriction(sF123,X2))
| in(X1,sK104)
| ~ relation(relation_dom_restriction(sK105,X2)) ),
inference(superposition,[],[f1816,f1752]) ).
fof(f4501,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF124)
| in(X1,sK104)
| ~ relation(relation_dom_restriction(sK105,sK104)) ),
inference(superposition,[],[f4484,f1754]) ).
fof(f4506,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF124)
| in(X1,sK104) )
| ~ spl125_12 ),
inference(forward_subsumption_resolution,[],[f4501,f2234]) ).
fof(f4512,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF124)
| in(X1,sK104) )
| ~ spl125_12 ),
inference(superposition,[],[f4506,f853]) ).
fof(f5607,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF122)
| in(X0,sK104) ),
inference(superposition,[],[f3932,f853]) ).
fof(f5615,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,X1)),sF122)
| in(X1,sK104) ),
inference(superposition,[],[f3922,f853]) ).
fof(f5618,plain,
( sK106(sF124,sF122) = unordered_pair(unordered_pair(sK19(sK106(sF124,sF122)),sK20(sK106(sF124,sF122))),unordered_pair(sK19(sK106(sF124,sF122)),sK19(sK106(sF124,sF122))))
| ~ relation(sK105)
| ~ spl125_3 ),
inference(resolution,[],[f2366,f1497]) ).
fof(f5621,plain,
( sK106(sF124,sF122) = unordered_pair(unordered_pair(sK19(sK106(sF124,sF122)),sK20(sK106(sF124,sF122))),unordered_pair(sK19(sK106(sF124,sF122)),sK19(sK106(sF124,sF122))))
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f5618,f1301]) ).
fof(f5622,plain,
( sK106(sF124,sF122) = unordered_pair(unordered_pair(sK19(sK106(sF124,sF122)),sK19(sK106(sF124,sF122))),unordered_pair(sK19(sK106(sF124,sF122)),sK20(sK106(sF124,sF122))))
| ~ spl125_3 ),
inference(forward_demodulation,[],[f5621,f853]) ).
fof(f6282,plain,
( ~ in(sK106(sF124,sF122),sF124)
| in(sK19(sK106(sF124,sF122)),sK104)
| ~ spl125_3 ),
inference(superposition,[],[f2022,f5622]) ).
fof(f6285,plain,
( ~ in(sK106(sF124,sF122),sK105)
| ~ in(sK20(sK106(sF124,sF122)),sK104)
| in(sK106(sF124,sF122),sF122)
| ~ in(sK19(sK106(sF124,sF122)),sK104)
| ~ spl125_3 ),
inference(superposition,[],[f2065,f5622]) ).
fof(f6291,plain,
( ~ in(sK106(sF124,sF122),sK105)
| ~ in(sK20(sK106(sF124,sF122)),sK104)
| ~ in(sK19(sK106(sF124,sF122)),sK104)
| in(sK106(sF124,sF122),sF124)
| ~ spl125_3
| ~ spl125_12 ),
inference(superposition,[],[f3872,f5622]) ).
fof(f6293,plain,
( ~ in(sK106(sF124,sF122),sF124)
| in(sK20(sK106(sF124,sF122)),sK104)
| ~ spl125_3
| ~ spl125_12 ),
inference(superposition,[],[f4512,f5622]) ).
fof(f6550,definition,
( spl125_203
<=> in(sK20(sK106(sF124,sF122)),sK104) ),
introduced(definition,[new_symbols(definition,[spl125_203])],[avatar_definition]) ).
fof(f6551,plain,
( ~ in(sK20(sK106(sF124,sF122)),sK104)
| spl125_203 ),
inference(avatar_component_clause,[],[f6550]) ).
fof(f6554,definition,
( spl125_204
<=> in(sK106(sF124,sF122),sF124) ),
introduced(definition,[new_symbols(definition,[spl125_204])],[avatar_definition]) ).
fof(f6555,plain,
( in(sK106(sF124,sF122),sF124)
| ~ spl125_204 ),
inference(avatar_component_clause,[],[f6554]) ).
fof(f6556,plain,
( ~ in(sK106(sF124,sF122),sF124)
| spl125_204 ),
inference(avatar_component_clause,[],[f6554]) ).
fof(f6557,plain,
( spl125_203
| ~ spl125_204
| ~ spl125_3
| ~ spl125_12 ),
inference(avatar_split_clause,[],[f6293,f2233,f1790,f6554,f6550]) ).
fof(f6562,plain,
( ~ in(sK20(sK106(sF124,sF122)),sK104)
| ~ in(sK19(sK106(sF124,sF122)),sK104)
| in(sK106(sF124,sF122),sF124)
| ~ spl125_3
| ~ spl125_12 ),
inference(forward_subsumption_resolution,[],[f6291,f2366]) ).
fof(f6565,plain,
( ~ in(sK20(sK106(sF124,sF122)),sK104)
| in(sK106(sF124,sF122),sF122)
| ~ in(sK19(sK106(sF124,sF122)),sK104)
| ~ spl125_3 ),
inference(forward_subsumption_resolution,[],[f6285,f2366]) ).
fof(f6567,definition,
( spl125_206
<=> in(sK19(sK106(sF124,sF122)),sK104) ),
introduced(definition,[new_symbols(definition,[spl125_206])],[avatar_definition]) ).
fof(f6568,plain,
( ~ in(sK19(sK106(sF124,sF122)),sK104)
| spl125_206 ),
inference(avatar_component_clause,[],[f6567]) ).
fof(f6570,plain,
( spl125_206
| ~ spl125_204
| ~ spl125_3 ),
inference(avatar_split_clause,[],[f6282,f1790,f6554,f6567]) ).
fof(f6605,plain,
( spl125_204
| ~ spl125_206
| ~ spl125_203
| ~ spl125_3
| ~ spl125_12 ),
inference(avatar_split_clause,[],[f6562,f2233,f1790,f6550,f6567,f6554]) ).
fof(f6619,definition,
( spl125_211
<=> in(sK106(sF124,sF122),sF122) ),
introduced(definition,[new_symbols(definition,[spl125_211])],[avatar_definition]) ).
fof(f6621,plain,
( in(sK106(sF124,sF122),sF122)
| ~ spl125_211 ),
inference(avatar_component_clause,[],[f6619]) ).
fof(f6622,plain,
( ~ spl125_206
| spl125_211
| ~ spl125_203
| ~ spl125_3 ),
inference(avatar_split_clause,[],[f6565,f1790,f6550,f6619,f6567]) ).
fof(f6680,plain,
( in(sK106(sF124,sF122),sF122)
| sF122 = sF124
| spl125_204 ),
inference(resolution,[],[f6556,f1326]) ).
fof(f6681,plain,
( in(sK106(sF124,sF122),sF122)
| spl125_204 ),
inference(forward_subsumption_resolution,[],[f6680,f1755]) ).
fof(f6682,plain,
( spl125_211
| spl125_204 ),
inference(avatar_split_clause,[],[f6681,f6554,f6619]) ).
fof(f6684,plain,
( sF122 = sF124
| ~ in(sK106(sF124,sF122),sF124)
| ~ spl125_211 ),
inference(resolution,[],[f6621,f1327]) ).
fof(f6689,plain,
( ~ in(sK106(sF124,sF122),sF124)
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6684,f1755]) ).
fof(f6691,plain,
( $false
| ~ spl125_204
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6689,f6555]) ).
fof(f6692,plain,
( ~ spl125_204
| ~ spl125_211 ),
inference(avatar_contradiction_clause,[],[f6691]) ).
fof(f6788,plain,
( ~ in(sK106(sF124,sF122),sF122)
| in(sK20(sK106(sF124,sF122)),sK104)
| ~ spl125_3 ),
inference(superposition,[],[f5615,f5622]) ).
fof(f6791,plain,
( in(sK20(sK106(sF124,sF122)),sK104)
| ~ spl125_3
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6788,f6621]) ).
fof(f6794,plain,
( $false
| ~ spl125_3
| spl125_203
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6791,f6551]) ).
fof(f6795,plain,
( ~ spl125_3
| spl125_203
| ~ spl125_211 ),
inference(avatar_contradiction_clause,[],[f6794]) ).
fof(f6823,plain,
( ~ in(sK106(sF124,sF122),sF122)
| in(sK19(sK106(sF124,sF122)),sK104)
| ~ spl125_3 ),
inference(superposition,[],[f5607,f5622]) ).
fof(f6826,plain,
( in(sK19(sK106(sF124,sF122)),sK104)
| ~ spl125_3
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6823,f6621]) ).
fof(f6828,plain,
( $false
| ~ spl125_3
| spl125_206
| ~ spl125_211 ),
inference(forward_subsumption_resolution,[],[f6826,f6568]) ).
fof(f6829,plain,
( ~ spl125_3
| spl125_206
| ~ spl125_211 ),
inference(avatar_contradiction_clause,[],[f6828]) ).
cnf(s3,plain,
spl125_3,
inference(sat_conversion,[],[f1802]) ).
cnf(s8,plain,
spl125_12,
inference(sat_conversion,[],[f2247]) ).
cnf(s186,plain,
( ~ spl125_3
| ~ spl125_12
| spl125_203
| ~ spl125_204 ),
inference(sat_conversion,[],[f6557]) ).
cnf(s188,plain,
( ~ spl125_3
| ~ spl125_204
| spl125_206 ),
inference(sat_conversion,[],[f6570]) ).
cnf(s197,plain,
( ~ spl125_3
| ~ spl125_12
| ~ spl125_203
| spl125_204
| ~ spl125_206 ),
inference(sat_conversion,[],[f6605]) ).
cnf(s200,plain,
( ~ spl125_3
| ~ spl125_203
| ~ spl125_206
| spl125_211 ),
inference(sat_conversion,[],[f6622]) ).
cnf(s216,plain,
( spl125_204
| spl125_211 ),
inference(sat_conversion,[],[f6682]) ).
cnf(s217,plain,
( ~ spl125_204
| ~ spl125_211 ),
inference(sat_conversion,[],[f6692]) ).
cnf(s223,plain,
( ~ spl125_3
| spl125_203
| ~ spl125_211 ),
inference(sat_conversion,[],[f6795]) ).
cnf(s224,plain,
( ~ spl125_3
| spl125_206
| ~ spl125_211 ),
inference(sat_conversion,[],[f6829]) ).
cnf(s229,plain,
spl125_203,
inference(rat,[],[s216,s186,s223,s8,s3]) ).
cnf(s231,plain,
spl125_204,
inference(rat,[],[s224,s197,s216,s3,s8,s229]) ).
cnf(s232,plain,
~ spl125_211,
inference(rat,[],[s217,s231]) ).
cnf(s233,plain,
spl125_206,
inference(rat,[],[s188,s3,s231]) ).
cnf(s234,plain,
$false,
inference(rat,[],[s200,s229,s3,s233,s232]) ).
fof(f6832,plain,
$false,
inference(avatar_sat_refutation,[],[s234]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU246+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n004.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 04:18:52 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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
% 9.06/2.31 % (4142153)Detected formulas, will run a generic FOF schedule.
% 9.06/2.31 % (4142159)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=2870634595:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.06/2.31 % (4142163)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=750875604:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.06/2.31 % (4142162)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2842921716:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.06/2.31 % (4142161)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1621386764:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.06/2.31 % (4142160)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=689572836:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.06/2.31 % (4142164)dis-21_1_sil=8000:lcm=predicate:random_seed=2872670347: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)
% 9.06/2.31 % (4142158)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=2619116413:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.06/2.31 % (4142161)Instruction limit reached!
% 9.06/2.31 % (4142161)------------------------------
% 9.06/2.31 % (4142161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142161)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142161)Termination reason: Instruction limit
% 9.06/2.31 % (4142161)Termination phase: Saturation
% 9.06/2.31 % (4142161)Time elapsed: 0.067 s
% 9.06/2.31 % (4142161)Peak memory usage: 90 MB
% 9.06/2.31 % (4142161)Instructions burned: 109 (million)
% 9.06/2.31 % (4142164)Instruction limit reached!
% 9.06/2.31 % (4142164)------------------------------
% 9.06/2.31 % (4142164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142164)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142164)Termination reason: Instruction limit
% 9.06/2.31 % (4142164)Termination phase: Saturation
% 9.06/2.31 % (4142164)Time elapsed: 0.076 s
% 9.06/2.31 % (4142164)Peak memory usage: 90 MB
% 9.06/2.31 % (4142164)Instructions burned: 129 (million)
% 9.06/2.31 % (4142162)Instruction limit reached!
% 9.06/2.31 % (4142162)------------------------------
% 9.06/2.31 % (4142162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142162)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142162)Termination reason: Instruction limit
% 9.06/2.31 % (4142162)Termination phase: Saturation
% 9.06/2.31 % (4142162)Time elapsed: 0.080 s
% 9.06/2.31 % (4142162)Peak memory usage: 89 MB
% 9.06/2.31 % (4142162)Instructions burned: 120 (million)
% 9.06/2.31 % (4142163)Instruction limit reached!
% 9.06/2.31 % (4142163)------------------------------
% 9.06/2.31 % (4142163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142163)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142163)Termination reason: Instruction limit
% 9.06/2.31 % (4142163)Termination phase: Saturation
% 9.06/2.31 % (4142163)Time elapsed: 0.094 s
% 9.06/2.31 % (4142163)Peak memory usage: 90 MB
% 9.06/2.31 % (4142163)Instructions burned: 140 (million)
% 9.06/2.31 % (4142172)lrs+10_1_sil=8000:sp=occurrence:random_seed=62943758:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.06/2.31 % (4142174)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3380762736:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.06/2.31 % (4142173)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3969107761:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.06/2.31 % (4142175)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=4132279876:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 9.06/2.31 % (4142173)Instruction limit reached!
% 9.06/2.31 % (4142173)------------------------------
% 9.06/2.31 % (4142173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142173)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142173)Termination reason: Instruction limit
% 9.06/2.31 % (4142173)Termination phase: Saturation
% 9.06/2.31 % (4142173)Time elapsed: 0.096 s
% 9.06/2.31 % (4142173)Peak memory usage: 90 MB
% 9.06/2.31 % (4142173)Instructions burned: 157 (million)
% 9.06/2.31 % (4142175)Instruction limit reached!
% 9.06/2.31 % (4142175)------------------------------
% 9.06/2.31 % (4142175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142175)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142175)Termination reason: Instruction limit
% 9.06/2.31 % (4142175)Termination phase: Saturation
% 9.06/2.31 % (4142175)Time elapsed: 0.149 s
% 9.06/2.31 % (4142175)Peak memory usage: 93 MB
% 9.06/2.31 % (4142175)Instructions burned: 249 (million)
% 9.06/2.31 % (4142172)Instruction limit reached!
% 9.06/2.31 % (4142172)------------------------------
% 9.06/2.31 % (4142172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142172)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142172)Termination reason: Instruction limit
% 9.06/2.31 % (4142172)Termination phase: Saturation
% 9.06/2.31 % (4142172)Time elapsed: 0.185 s
% 9.06/2.31 % (4142172)Peak memory usage: 93 MB
% 9.06/2.31 % (4142172)Instructions burned: 286 (million)
% 9.06/2.31 % (4142174)Instruction limit reached!
% 9.06/2.31 % (4142174)------------------------------
% 9.06/2.31 % (4142174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142174)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142174)Termination reason: Instruction limit
% 9.06/2.31 % (4142174)Termination phase: Saturation
% 9.06/2.31 % (4142174)Time elapsed: 0.222 s
% 9.06/2.31 % (4142174)Peak memory usage: 93 MB
% 9.06/2.31 % (4142174)Instructions burned: 326 (million)
% 9.06/2.31 % (4142180)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3107413513:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.06/2.31 % (4142181)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2821936117:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.06/2.31 % (4142182)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1298906710:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.06/2.31 % (4142183)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1105616365:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.06/2.31 % (4142182)Instruction limit reached!
% 9.06/2.31 % (4142182)------------------------------
% 9.06/2.31 % (4142182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142182)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142182)Termination reason: Instruction limit
% 9.06/2.31 % (4142182)Termination phase: Saturation
% 9.06/2.31 % (4142182)Time elapsed: 0.069 s
% 9.06/2.31 % (4142182)Peak memory usage: 90 MB
% 9.06/2.31 % (4142182)Instructions burned: 113 (million)
% 9.06/2.31 % (4142183)Instruction limit reached!
% 9.06/2.31 % (4142183)------------------------------
% 9.06/2.31 % (4142183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142183)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142183)Termination reason: Instruction limit
% 9.06/2.31 % (4142183)Termination phase: Saturation
% 9.06/2.31 % (4142183)Time elapsed: 0.065 s
% 9.06/2.31 % (4142183)Peak memory usage: 90 MB
% 9.06/2.31 % (4142183)Instructions burned: 128 (million)
% 9.06/2.31 % (4142180)Instruction limit reached!
% 9.06/2.31 % (4142180)------------------------------
% 9.06/2.31 % (4142180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142180)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142180)Termination reason: Instruction limit
% 9.06/2.31 % (4142180)Termination phase: Saturation
% 9.06/2.31 % (4142180)Time elapsed: 0.187 s
% 9.06/2.31 % (4142180)Peak memory usage: 91 MB
% 9.06/2.31 % (4142180)Instructions burned: 294 (million)
% 9.06/2.31 % (4142188)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1008721483:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 9.06/2.31 % (4142189)lrs+10_1_sil=8000:sp=occurrence:random_seed=4161140534:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.06/2.31 % (4142190)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1325281735:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.06/2.31 % (4142188)Instruction limit reached!
% 9.06/2.31 % (4142188)------------------------------
% 9.06/2.31 % (4142188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142188)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142188)Termination reason: Instruction limit
% 9.06/2.31 % (4142188)Termination phase: Saturation
% 9.06/2.31 % (4142188)Time elapsed: 0.065 s
% 9.06/2.31 % (4142188)Peak memory usage: 89 MB
% 9.06/2.31 % (4142188)Instructions burned: 114 (million)
% 9.06/2.31 % (4142194)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=488082392:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 9.06/2.31 % (4142190)Instruction limit reached!
% 9.06/2.31 % (4142190)------------------------------
% 9.06/2.31 % (4142190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142190)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142190)Termination reason: Instruction limit
% 9.06/2.31 % (4142190)Termination phase: Saturation
% 9.06/2.31 % (4142190)Time elapsed: 0.262 s
% 9.06/2.31 % (4142190)Peak memory usage: 93 MB
% 9.06/2.31 % (4142190)Instructions burned: 438 (million)
% 9.06/2.31 % (4142181)First to succeed.
% 9.06/2.31 % (4142196)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=57969651:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 9.06/2.31 % (4142181)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4142153"
% 9.06/2.31 % (4142196)Instruction limit reached!
% 9.06/2.31 % (4142196)------------------------------
% 9.06/2.31 % (4142196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.31 % (4142196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.31 % (4142196)CaDiCaL version: 2.1.3
% 9.06/2.31 % (4142196)Termination reason: Instruction limit
% 9.06/2.31 % (4142196)Termination phase: Saturation
% 9.06/2.31 % (4142196)Time elapsed: 0.077 s
% 9.06/2.31 % (4142196)Peak memory usage: 93 MB
% 9.06/2.31 % (4142196)Instructions burned: 135 (million)
% 9.06/2.31 % (4142181)Refutation found. Thanks to Tanya!
% 9.06/2.31 % SZS status Theorem for theBenchmark
% 9.06/2.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/2.40 % (4142181)------------------------------
% 0.16/2.40 % (4142181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.40 % (4142181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.40 % (4142181)CaDiCaL version: 2.1.3
% 0.16/2.40 % (4142181)Termination reason: Refutation
% 0.16/2.40 % (4142181)Time elapsed: 0.672 s
% 0.16/2.40 % (4142181)Peak memory usage: 140 MB
% 0.16/2.40 % (4142181)Instructions burned: 1879 (million)
% 0.16/2.40 % (4142181)------------------------------
% 0.16/2.40 % (4142181)------------------------------
% 0.16/2.40 % (4142153)Success in time 1.45 s
% 0.16/2.40 % Vampire exiting
%------------------------------------------------------------------------------