%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP622+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 10:15:03 AM UTC 2026
% Result : Theorem 19.91s 7.69s
% Output : Refutation 35.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 24
% Syntax : Number of formulae : 168 ( 32 unt; 3 def)
% Number of atoms : 622 ( 58 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 724 ( 270 ~; 305 |; 110 &)
% ( 16 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 4 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 1 con; 0-3 aty)
% Number of variables : 284 ( 0 sgn 266 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f1917,axiom,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,X0,X0)
& m2_relset_1(X1,X0,X0) )
=> r2_hidden(X1,k1_funct_2(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_funct_2) ).
fof(f2460,axiom,
! [X0,X1] : k2_funcop_1(X0,X1) = k2_zfmisc_1(X0,k1_tarski(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_funcop_1) ).
fof(f3353,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
=> ( m1_fraenkel(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,X2)
=> ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_fraenkel) ).
fof(f3367,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f3369,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
=> ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
fof(f3371,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f3373,axiom,
! [X0,X1] :
( ~ v1_xboole_0(X1)
=> k1_fraenkel(X0,X1) = k1_funct_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_fraenkel) ).
fof(f6740,axiom,
! [X0,X1] : k1_funct_2(X0,X1) = k4_card_3(k2_funcop_1(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_card_3) ).
fof(f17596,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18620,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_rlvect_1) ).
fof(f18878,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> ( v3_group_1(X0)
<=> ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( k1_group_1(X0,X2,X1) = X2
& k1_group_1(X0,X1,X2) = X2
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& k1_group_1(X0,X2,X3) = X1
& k1_group_1(X0,X3,X2) = X1 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_group_1) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f21861,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> r1_rlvect_1(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t50_group_2) ).
fof(f21874,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_group_2(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_group_2) ).
fof(f33388,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f33409,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> r1_tarski(k4_autgroup(X0),k1_fraenkel(u1_struct_0(X0),u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_autgroup) ).
fof(f33410,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> r1_tarski(k4_autgroup(X0),k1_fraenkel(u1_struct_0(X0),u1_struct_0(X0))) ),
inference(negated_conjecture,[status(cth)],[f33409]) ).
fof(f33501,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33388]) ).
fof(f33502,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33501]) ).
fof(f33541,plain,
? [X0] :
( ~ r1_tarski(k4_autgroup(X0),k1_fraenkel(u1_struct_0(X0),u1_struct_0(X0)))
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f33410]) ).
fof(f33542,plain,
? [X0] :
( ~ r1_tarski(k4_autgroup(X0),k1_fraenkel(u1_struct_0(X0),u1_struct_0(X0)))
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f33541]) ).
fof(f33545,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3371]) ).
fof(f33546,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f33545]) ).
fof(f33549,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3369]) ).
fof(f33550,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f33549]) ).
fof(f33551,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3367]) ).
fof(f33555,plain,
! [X0,X1,X2] :
( ( m1_fraenkel(X2,X0,X1)
<=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X3,X2) ) )
| v1_xboole_0(X2)
| ~ v1_fraenkel(X2) ),
inference(ennf_transformation,[],[f3353]) ).
fof(f33556,plain,
! [X0,X1,X2] :
( ( m1_fraenkel(X2,X0,X1)
<=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X3,X2) ) )
| v1_xboole_0(X2)
| ~ v1_fraenkel(X2) ),
inference(flattening,[],[f33555]) ).
fof(f33576,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21874]) ).
fof(f33577,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33576]) ).
fof(f33596,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21861]) ).
fof(f33597,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33596]) ).
fof(f33648,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f33650,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f33759,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f33996,plain,
! [X0] :
( ( v3_group_1(X0)
<=> ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ! [X2] :
( ( k1_group_1(X0,X2,X1) = X2
& k1_group_1(X0,X1,X2) = X2
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& k1_group_1(X0,X2,X3) = X1
& k1_group_1(X0,X3,X2) = X1 ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18878]) ).
fof(f33997,plain,
! [X0] :
( ( v3_group_1(X0)
<=> ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ! [X2] :
( ( k1_group_1(X0,X2,X1) = X2
& k1_group_1(X0,X1,X2) = X2
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& k1_group_1(X0,X2,X3) = X1
& k1_group_1(X0,X3,X2) = X1 ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33996]) ).
fof(f34102,plain,
! [X0,X1] :
( k1_fraenkel(X0,X1) = k1_funct_2(X0,X1)
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f3373]) ).
fof(f34113,plain,
! [X0,X1] :
( r2_hidden(X1,k1_funct_2(X0,X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,X0)
| ~ m2_relset_1(X1,X0,X0) ),
inference(ennf_transformation,[],[f1917]) ).
fof(f34114,plain,
! [X0,X1] :
( r2_hidden(X1,k1_funct_2(X0,X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,X0)
| ~ m2_relset_1(X1,X0,X0) ),
inference(flattening,[],[f34113]) ).
fof(f36612,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f36615,plain,
! [X0] :
( ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18620]) ).
fof(f36621,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17596]) ).
fof(f36622,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f36621]) ).
fof(f37920,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f39513,plain,
( ~ r1_tarski(k4_autgroup(sK44),k1_fraenkel(u1_struct_0(sK44),u1_struct_0(sK44)))
& ~ v3_struct_0(sK44)
& v1_group_1(sK44)
& v3_group_1(sK44)
& v4_group_1(sK44)
& l1_group_1(sK44) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X0,sK44)],[f33542]) ).
fof(f39514,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( m2_fraenkel(X3,X0,X1,X2)
| ~ m1_subset_1(X3,X2) )
& ( m1_subset_1(X3,X2)
| ~ m2_fraenkel(X3,X0,X1,X2) ) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(nnf_transformation,[],[f33546]) ).
fof(f39517,plain,
! [X0,X1,X2] :
( ( ( m1_fraenkel(X2,X0,X1)
| ? [X3] :
( ( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) )
& m1_subset_1(X3,X2) ) )
& ( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X3,X2) )
| ~ m1_fraenkel(X2,X0,X1) ) )
| v1_xboole_0(X2)
| ~ v1_fraenkel(X2) ),
inference(nnf_transformation,[],[f33556]) ).
fof(f39518,plain,
! [X0,X1,X2] :
( ( ( m1_fraenkel(X2,X0,X1)
| ? [X3] :
( ( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) )
& m1_subset_1(X3,X2) ) )
& ( ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,X0,X1)
& m2_relset_1(X4,X0,X1) )
| ~ m1_subset_1(X4,X2) )
| ~ m1_fraenkel(X2,X0,X1) ) )
| v1_xboole_0(X2)
| ~ v1_fraenkel(X2) ),
inference(rectify,[],[f39517]) ).
fof(f39519,plain,
! [X0,X1,X2] :
( ( ( m1_fraenkel(X2,X0,X1)
| ( ( ~ v1_funct_1(sK47(X0,X1,X2))
| ~ v1_funct_2(sK47(X0,X1,X2),X0,X1)
| ~ m2_relset_1(sK47(X0,X1,X2),X0,X1) )
& m1_subset_1(sK47(X0,X1,X2),X2) ) )
& ( ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,X0,X1)
& m2_relset_1(X4,X0,X1) )
| ~ m1_subset_1(X4,X2) )
| ~ m1_fraenkel(X2,X0,X1) ) )
| v1_xboole_0(X2)
| ~ v1_fraenkel(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(X3,sK47(X0,X1,X2))],[f39518]) ).
fof(f39583,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f33759]) ).
fof(f39584,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f39583]) ).
fof(f39585,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK103(X0,X1),X1)
& r2_hidden(sK103(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103]),skolemize(X2,sK103(X0,X1))],[f39584]) ).
fof(f39663,plain,
! [X0] :
( ( ( v3_group_1(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ? [X2] :
( ( k1_group_1(X0,X2,X1) != X2
| k1_group_1(X0,X1,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| k1_group_1(X0,X2,X3) != X1
| k1_group_1(X0,X3,X2) != X1 ) )
& m1_subset_1(X2,u1_struct_0(X0)) ) ) )
& ( ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ! [X2] :
( ( k1_group_1(X0,X2,X1) = X2
& k1_group_1(X0,X1,X2) = X2
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& k1_group_1(X0,X2,X3) = X1
& k1_group_1(X0,X3,X2) = X1 ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ v3_group_1(X0) ) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f33997]) ).
fof(f39664,plain,
! [X0] :
( ( ( v3_group_1(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ? [X2] :
( ( k1_group_1(X0,X2,X1) != X2
| k1_group_1(X0,X1,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| k1_group_1(X0,X2,X3) != X1
| k1_group_1(X0,X3,X2) != X1 ) )
& m1_subset_1(X2,u1_struct_0(X0)) ) ) )
& ( ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& ! [X5] :
( ( k1_group_1(X0,X5,X4) = X5
& k1_group_1(X0,X4,X5) = X5
& ? [X6] :
( m1_subset_1(X6,u1_struct_0(X0))
& k1_group_1(X0,X5,X6) = X4
& k1_group_1(X0,X6,X5) = X4 ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| ~ v3_group_1(X0) ) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f39663]) ).
fof(f39665,plain,
! [X0] :
( ( ( v3_group_1(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ( ( sK166(X0,X1) != k1_group_1(X0,sK166(X0,X1),X1)
| sK166(X0,X1) != k1_group_1(X0,X1,sK166(X0,X1))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| k1_group_1(X0,sK166(X0,X1),X3) != X1
| k1_group_1(X0,X3,sK166(X0,X1)) != X1 ) )
& m1_subset_1(sK166(X0,X1),u1_struct_0(X0)) ) ) )
& ( ( m1_subset_1(sK167(X0),u1_struct_0(X0))
& ! [X5] :
( ( k1_group_1(X0,X5,sK167(X0)) = X5
& k1_group_1(X0,sK167(X0),X5) = X5
& m1_subset_1(sK168(X0,X5),u1_struct_0(X0))
& sK167(X0) = k1_group_1(X0,X5,sK168(X0,X5))
& sK167(X0) = k1_group_1(X0,sK168(X0,X5),X5) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| ~ v3_group_1(X0) ) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK166,sK167,sK168]),skolemize(X2,sK166(X0,X1)),skolemize(X4,sK167(X0)),skolemize(X6,sK168(X0,X5))],[f39664]) ).
fof(f40379,plain,
! [X0] :
( ! [X1] :
( ( r1_rlvect_1(X0,X1)
| ~ r2_hidden(X1,u1_struct_0(X0)) )
& ( r2_hidden(X1,u1_struct_0(X0))
| ~ r1_rlvect_1(X0,X1) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f36615]) ).
fof(f41211,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33502]) ).
fof(f41279,plain,
l1_group_1(sK44),
inference(cnf_transformation,[],[f39513]) ).
fof(f41280,plain,
v4_group_1(sK44),
inference(cnf_transformation,[],[f39513]) ).
fof(f41281,plain,
v3_group_1(sK44),
inference(cnf_transformation,[],[f39513]) ).
fof(f41282,plain,
v1_group_1(sK44),
inference(cnf_transformation,[],[f39513]) ).
fof(f41283,plain,
~ v3_struct_0(sK44),
inference(cnf_transformation,[],[f39513]) ).
fof(f41284,plain,
~ r1_tarski(k4_autgroup(sK44),k1_fraenkel(u1_struct_0(sK44),u1_struct_0(sK44))),
inference(cnf_transformation,[],[f39513]) ).
fof(f41288,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,X2)
| m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f39514]) ).
fof(f41292,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f33550]) ).
fof(f41294,plain,
! [X2,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| v1_fraenkel(X2) ),
inference(cnf_transformation,[],[f33551]) ).
fof(f41295,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f33551]) ).
fof(f41298,plain,
! [X2,X0,X1,X4] :
( ~ v1_fraenkel(X2)
| ~ m1_subset_1(X4,X2)
| ~ m1_fraenkel(X2,X0,X1)
| v1_xboole_0(X2)
| m2_relset_1(X4,X0,X1) ),
inference(cnf_transformation,[],[f39519]) ).
fof(f41299,plain,
! [X2,X0,X1,X4] :
( ~ v1_fraenkel(X2)
| ~ m1_subset_1(X4,X2)
| ~ m1_fraenkel(X2,X0,X1)
| v1_xboole_0(X2)
| v1_funct_2(X4,X0,X1) ),
inference(cnf_transformation,[],[f39519]) ).
fof(f41328,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33577]) ).
fof(f41374,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| r1_rlvect_1(X0,X2)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33597]) ).
fof(f41409,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f33648]) ).
fof(f41414,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f33650]) ).
fof(f41616,plain,
! [X0,X1] :
( r2_hidden(sK103(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f39585]) ).
fof(f41617,plain,
! [X0,X1] :
( ~ r2_hidden(sK103(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f39585]) ).
fof(f41989,plain,
! [X0] :
( ~ v3_group_1(X0)
| m1_subset_1(sK167(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39665]) ).
fof(f42130,plain,
! [X0,X1] : k1_funct_2(X0,X1) = k4_card_3(k2_funcop_1(X0,X1)),
inference(cnf_transformation,[],[f6740]) ).
fof(f42136,plain,
! [X0,X1] :
( k1_funct_2(X0,X1) = k1_fraenkel(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f34102]) ).
fof(f42149,plain,
! [X0,X1] :
( r2_hidden(X1,k1_funct_2(X0,X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,X0)
| ~ m2_relset_1(X1,X0,X0) ),
inference(cnf_transformation,[],[f34114]) ).
fof(f44512,plain,
! [X0,X1] : k2_zfmisc_1(X0,k1_tarski(X1)) = k2_funcop_1(X0,X1),
inference(cnf_transformation,[],[f2460]) ).
fof(f44729,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f45366,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36612]) ).
fof(f45368,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| ~ r1_rlvect_1(X0,X1)
| r2_hidden(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f40379]) ).
fof(f45377,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36622]) ).
fof(f47169,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f37920]) ).
fof(f49236,plain,
! [X0,X1] : k2_funcop_1(X0,X1) = k2_zfmisc_1(X0,k2_tarski(X1,X1)),
inference(definition_unfolding,[],[f44512,f44729]) ).
fof(f49239,plain,
! [X0,X1] : k1_funct_2(X0,X1) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(X1,X1))),
inference(definition_unfolding,[],[f42130,f49236]) ).
fof(f49365,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| k1_fraenkel(X0,X1) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(X1,X1))) ),
inference(definition_unfolding,[],[f42136,f49239]) ).
fof(f49378,plain,
! [X0,X1] :
( ~ v1_funct_1(X1)
| r2_hidden(X1,k4_card_3(k2_zfmisc_1(X0,k2_tarski(X0,X0))))
| ~ v1_funct_2(X1,X0,X0)
| ~ m2_relset_1(X1,X0,X0) ),
inference(definition_unfolding,[],[f42149,f49239]) ).
fof(f52153,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f47169,f45366]) ).
fof(f52154,plain,
u1_struct_0(sK44) = k2_pre_topc(sK44),
inference(resolution,[],[f52153,f41279]) ).
fof(f52155,plain,
~ r1_tarski(k4_autgroup(sK44),k1_fraenkel(k2_pre_topc(sK44),k2_pre_topc(sK44))),
inference(superposition,[],[f41284,f52154]) ).
fof(f52157,plain,
( m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44))
| v3_struct_0(sK44)
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(superposition,[],[f41211,f52154]) ).
fof(f52185,plain,
! [X0,X1] :
( ~ l1_struct_0(X1)
| v3_struct_0(X1)
| k1_fraenkel(X0,u1_struct_0(X1)) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(u1_struct_0(X1),u1_struct_0(X1)))) ),
inference(resolution,[],[f49365,f45377]) ).
fof(f52187,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| k1_fraenkel(X1,u1_struct_0(X0)) = k4_card_3(k2_zfmisc_1(X1,k2_tarski(u1_struct_0(X0),u1_struct_0(X0))))
| v3_struct_0(X0) ),
inference(resolution,[],[f52185,f45366]) ).
fof(f52188,plain,
! [X0] :
( k1_fraenkel(X0,u1_struct_0(sK44)) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(u1_struct_0(sK44),u1_struct_0(sK44))))
| v3_struct_0(sK44) ),
inference(resolution,[],[f52187,f41279]) ).
fof(f52189,plain,
! [X0] : k1_fraenkel(X0,u1_struct_0(sK44)) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(u1_struct_0(sK44),u1_struct_0(sK44)))),
inference(forward_subsumption_resolution,[],[f52188,f41283]) ).
fof(f52190,plain,
! [X0] : k1_fraenkel(X0,k2_pre_topc(sK44)) = k4_card_3(k2_zfmisc_1(X0,k2_tarski(k2_pre_topc(sK44),k2_pre_topc(sK44)))),
inference(forward_demodulation,[],[f52189,f52154]) ).
fof(f52228,plain,
( m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44))
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52157,f41283]) ).
fof(f52233,plain,
( m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44))
| ~ v3_group_1(sK44)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52228,f41282]) ).
fof(f52238,plain,
( m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44))
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52233,f41281]) ).
fof(f52243,plain,
( m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52238,f41280]) ).
fof(f52248,plain,
m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44)),
inference(forward_subsumption_resolution,[],[f52243,f41279]) ).
fof(f52361,plain,
! [X0,X1] :
( m1_subset_1(sK103(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(resolution,[],[f41409,f41616]) ).
fof(f52366,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X0,X2,X3)
| m2_fraenkel(sK103(X0,X1),X2,X3,X0)
| v1_xboole_0(X3)
| r1_tarski(X0,X1) ),
inference(resolution,[],[f52361,f41288]) ).
fof(f52370,plain,
! [X0] :
( m2_fraenkel(sK103(k4_autgroup(sK44),X0),k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44))
| v1_xboole_0(k2_pre_topc(sK44))
| r1_tarski(k4_autgroup(sK44),X0) ),
inference(resolution,[],[f52366,f52248]) ).
fof(f52376,definition,
( spl1167_52
<=> v1_xboole_0(k2_pre_topc(sK44)) ),
introduced(definition,[new_symbols(definition,[spl1167_52])],[avatar_definition]) ).
fof(f52377,plain,
( v1_xboole_0(k2_pre_topc(sK44))
| ~ spl1167_52 ),
inference(avatar_component_clause,[],[f52376]) ).
fof(f52383,definition,
( spl1167_54
<=> ! [X0] :
( m2_fraenkel(sK103(k4_autgroup(sK44),X0),k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44))
| r1_tarski(k4_autgroup(sK44),X0) ) ),
introduced(definition,[new_symbols(definition,[spl1167_54])],[avatar_definition]) ).
fof(f52384,plain,
( ! [X0] :
( m2_fraenkel(sK103(k4_autgroup(sK44),X0),k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44))
| r1_tarski(k4_autgroup(sK44),X0) )
| ~ spl1167_54 ),
inference(avatar_component_clause,[],[f52383]) ).
fof(f52385,plain,
( spl1167_52
| spl1167_54 ),
inference(avatar_split_clause,[],[f52370,f52383,f52376]) ).
fof(f52498,plain,
( ! [X0] : ~ r2_hidden(X0,k2_pre_topc(sK44))
| ~ spl1167_52 ),
inference(resolution,[],[f41414,f52377]) ).
fof(f52574,plain,
v1_fraenkel(k4_autgroup(sK44)),
inference(resolution,[],[f41294,f52248]) ).
fof(f52896,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK44))
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X2)
| v1_xboole_0(k4_autgroup(sK44))
| v1_funct_2(X0,X1,X2) ),
inference(resolution,[],[f41299,f52574]) ).
fof(f52899,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK44))
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X2)
| v1_funct_2(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f52896,f41295]) ).
fof(f52950,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK44))
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X2)
| v1_xboole_0(k4_autgroup(sK44))
| m2_relset_1(X0,X1,X2) ),
inference(resolution,[],[f41298,f52574]) ).
fof(f52953,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK44))
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X2)
| m2_relset_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f52950,f41295]) ).
fof(f52957,plain,
( m1_subset_1(sK167(sK44),u1_struct_0(sK44))
| v3_struct_0(sK44)
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f41989,f41281]) ).
fof(f52960,plain,
( m1_subset_1(sK167(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52957,f41283]) ).
fof(f52962,plain,
m1_subset_1(sK167(sK44),u1_struct_0(sK44)),
inference(forward_subsumption_resolution,[],[f52960,f41279]) ).
fof(f52963,plain,
m1_subset_1(sK167(sK44),k2_pre_topc(sK44)),
inference(forward_demodulation,[],[f52962,f52154]) ).
fof(f53089,plain,
! [X2,X0,X1] :
( v1_funct_2(sK103(k4_autgroup(sK44),X2),X0,X1)
| ~ m1_fraenkel(k4_autgroup(sK44),X0,X1)
| r1_tarski(k4_autgroup(sK44),X2) ),
inference(resolution,[],[f52899,f52361]) ).
fof(f53092,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,sK44)
| v3_struct_0(sK44)
| r1_rlvect_1(sK44,X0)
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f41374,f41281]) ).
fof(f53095,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,sK44)
| r1_rlvect_1(sK44,X0)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f53092,f41283]) ).
fof(f53097,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK44)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| r1_rlvect_1(sK44,X0) ),
inference(forward_subsumption_resolution,[],[f53095,f41279]) ).
fof(f53098,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK44))
| r1_rlvect_1(sK44,X0)
| v3_struct_0(sK44)
| ~ v3_group_1(sK44)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f53097,f41328]) ).
fof(f53099,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK44))
| r1_rlvect_1(sK44,X0)
| ~ v3_group_1(sK44)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f53098,f41283]) ).
fof(f53100,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK44))
| r1_rlvect_1(sK44,X0)
| ~ v4_group_1(sK44)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f53099,f41281]) ).
fof(f53101,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK44))
| r1_rlvect_1(sK44,X0)
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f53100,f41280]) ).
fof(f53102,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK44))
| r1_rlvect_1(sK44,X0) ),
inference(forward_subsumption_resolution,[],[f53101,f41279]) ).
fof(f53103,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK44))
| r1_rlvect_1(sK44,X0) ),
inference(forward_demodulation,[],[f53102,f52154]) ).
fof(f53108,plain,
r1_rlvect_1(sK44,sK167(sK44)),
inference(resolution,[],[f53103,f52963]) ).
fof(f53309,plain,
! [X0,X1] :
( ~ r1_rlvect_1(X0,X1)
| r2_hidden(X1,u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(resolution,[],[f45368,f45366]) ).
fof(f53310,plain,
( r2_hidden(sK167(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f53309,f53108]) ).
fof(f53313,plain,
r2_hidden(sK167(sK44),u1_struct_0(sK44)),
inference(forward_subsumption_resolution,[],[f53310,f41279]) ).
fof(f53315,plain,
r2_hidden(sK167(sK44),k2_pre_topc(sK44)),
inference(forward_demodulation,[],[f53313,f52154]) ).
fof(f53318,plain,
( $false
| ~ spl1167_52 ),
inference(forward_subsumption_resolution,[],[f53315,f52498]) ).
fof(f53319,plain,
~ spl1167_52,
inference(avatar_contradiction_clause,[],[f53318]) ).
fof(f53352,plain,
( ! [X0] :
( r1_tarski(k4_autgroup(sK44),X0)
| v1_funct_1(sK103(k4_autgroup(sK44),X0))
| v1_xboole_0(k2_pre_topc(sK44))
| ~ m1_fraenkel(k4_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44)) )
| ~ spl1167_54 ),
inference(resolution,[],[f52384,f41292]) ).
fof(f53353,plain,
( ! [X0] :
( r1_tarski(k4_autgroup(sK44),X0)
| v1_funct_1(sK103(k4_autgroup(sK44),X0))
| v1_xboole_0(k2_pre_topc(sK44)) )
| ~ spl1167_54 ),
inference(forward_subsumption_resolution,[],[f53352,f52248]) ).
fof(f53356,definition,
( spl1167_113
<=> ! [X0] :
( r1_tarski(k4_autgroup(sK44),X0)
| v1_funct_1(sK103(k4_autgroup(sK44),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl1167_113])],[avatar_definition]) ).
fof(f53357,plain,
( ! [X0] :
( v1_funct_1(sK103(k4_autgroup(sK44),X0))
| r1_tarski(k4_autgroup(sK44),X0) )
| ~ spl1167_113 ),
inference(avatar_component_clause,[],[f53356]) ).
fof(f53358,plain,
( spl1167_52
| spl1167_113
| ~ spl1167_54 ),
inference(avatar_split_clause,[],[f53353,f52383,f53356,f52376]) ).
fof(f54049,plain,
! [X2,X0,X1] :
( ~ m1_fraenkel(k4_autgroup(sK44),X0,X1)
| m2_relset_1(sK103(k4_autgroup(sK44),X2),X0,X1)
| r1_tarski(k4_autgroup(sK44),X2) ),
inference(resolution,[],[f52953,f52361]) ).
fof(f57507,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK103(k4_autgroup(sK44),X0),X1,X1)
| r2_hidden(sK103(k4_autgroup(sK44),X0),k4_card_3(k2_zfmisc_1(X1,k2_tarski(X1,X1))))
| ~ m2_relset_1(sK103(k4_autgroup(sK44),X0),X1,X1)
| r1_tarski(k4_autgroup(sK44),X0) )
| ~ spl1167_113 ),
inference(resolution,[],[f49378,f53357]) ).
fof(f57510,plain,
( ! [X0,X1] :
( r2_hidden(sK103(k4_autgroup(sK44),X0),k4_card_3(k2_zfmisc_1(X1,k2_tarski(X1,X1))))
| ~ m2_relset_1(sK103(k4_autgroup(sK44),X0),X1,X1)
| r1_tarski(k4_autgroup(sK44),X0)
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X1)
| r1_tarski(k4_autgroup(sK44),X0) )
| ~ spl1167_113 ),
inference(resolution,[],[f57507,f53089]) ).
fof(f57511,plain,
( ! [X0,X1] :
( r2_hidden(sK103(k4_autgroup(sK44),X0),k4_card_3(k2_zfmisc_1(X1,k2_tarski(X1,X1))))
| ~ m2_relset_1(sK103(k4_autgroup(sK44),X0),X1,X1)
| r1_tarski(k4_autgroup(sK44),X0)
| ~ m1_fraenkel(k4_autgroup(sK44),X1,X1) )
| ~ spl1167_113 ),
inference(duplicate_literal_removal,[],[f57510]) ).
fof(f57512,plain,
( ! [X0,X1] :
( ~ m1_fraenkel(k4_autgroup(sK44),X1,X1)
| r1_tarski(k4_autgroup(sK44),X0)
| r2_hidden(sK103(k4_autgroup(sK44),X0),k4_card_3(k2_zfmisc_1(X1,k2_tarski(X1,X1)))) )
| ~ spl1167_113 ),
inference(forward_subsumption_resolution,[],[f57511,f54049]) ).
fof(f57514,plain,
( ! [X0] :
( r1_tarski(k4_autgroup(sK44),X0)
| r2_hidden(sK103(k4_autgroup(sK44),X0),k4_card_3(k2_zfmisc_1(k2_pre_topc(sK44),k2_tarski(k2_pre_topc(sK44),k2_pre_topc(sK44))))) )
| ~ spl1167_113 ),
inference(resolution,[],[f57512,f52248]) ).
fof(f57515,plain,
( ! [X0] :
( r2_hidden(sK103(k4_autgroup(sK44),X0),k1_fraenkel(k2_pre_topc(sK44),k2_pre_topc(sK44)))
| r1_tarski(k4_autgroup(sK44),X0) )
| ~ spl1167_113 ),
inference(forward_demodulation,[],[f57514,f52190]) ).
fof(f57624,plain,
( r1_tarski(k4_autgroup(sK44),k1_fraenkel(k2_pre_topc(sK44),k2_pre_topc(sK44)))
| r1_tarski(k4_autgroup(sK44),k1_fraenkel(k2_pre_topc(sK44),k2_pre_topc(sK44)))
| ~ spl1167_113 ),
inference(resolution,[],[f57515,f41617]) ).
fof(f57632,plain,
( r1_tarski(k4_autgroup(sK44),k1_fraenkel(k2_pre_topc(sK44),k2_pre_topc(sK44)))
| ~ spl1167_113 ),
inference(duplicate_literal_removal,[],[f57624]) ).
fof(f57633,plain,
( $false
| ~ spl1167_113 ),
inference(forward_subsumption_resolution,[],[f57632,f52155]) ).
fof(f57634,plain,
~ spl1167_113,
inference(avatar_contradiction_clause,[],[f57633]) ).
cnf(s44,plain,
( spl1167_52
| spl1167_54 ),
inference(sat_conversion,[],[f52385]) ).
cnf(s92,plain,
~ spl1167_52,
inference(sat_conversion,[],[f53319]) ).
cnf(s100,plain,
( spl1167_52
| ~ spl1167_54
| spl1167_113 ),
inference(sat_conversion,[],[f53358]) ).
cnf(s258,plain,
~ spl1167_113,
inference(sat_conversion,[],[f57634]) ).
cnf(s262,plain,
( spl1167_52
| ~ spl1167_54 ),
inference(rat,[],[s100,s258]) ).
cnf(s270,plain,
~ spl1167_54,
inference(rat,[],[s262,s92]) ).
cnf(s381,plain,
$false,
inference(rat,[],[s44,s270,s92]) ).
fof(f57635,plain,
$false,
inference(avatar_sat_refutation,[],[s381]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP622+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:12:59 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.46/5.23 % (3321558)Detected formulas, will run a generic FOF schedule.
% 18.46/5.23 % (3321563)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=1520172924:i=141193_2979 on theBenchmark for (2979ds/141193Mi)
% 18.46/5.23 % (3321564)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=3802913811:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2979 on theBenchmark for (2979ds/134677Mi)
% 18.46/5.23 % (3321565)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=758818290:i=141695:sd=1:nm=32:gsp=on:ss=included_2979 on theBenchmark for (2979ds/141695Mi)
% 18.46/5.23 % (3321569)dis-21_1_sil=8000:lcm=predicate:random_seed=3335538510:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2979 on theBenchmark for (2979ds/129Mi)
% 18.46/5.23 % (3321567)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2823904881:i=119:av=off:ss=axioms_2979 on theBenchmark for (2979ds/119Mi)
% 18.46/5.23 % (3321568)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=315544453:s2a=on:i=139:gtg=position_2979 on theBenchmark for (2979ds/139Mi)
% 18.46/5.23 % (3321566)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1961098606:i=109:sd=1:ins=1:gsp=on:ss=axioms_2979 on theBenchmark for (2979ds/109Mi)
% 18.46/5.23 % (3321568)Instruction limit reached!
% 18.46/5.23 % (3321568)------------------------------
% 18.46/5.23 % (3321568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/5.23 % (3321568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/5.23 % (3321568)CaDiCaL version: 2.1.3
% 18.46/5.23 % (3321568)Termination reason: Instruction limit
% 18.46/5.23 % (3321568)Termination phase: Property scanning
% 18.46/5.23 % (3321568)Time elapsed: 0.061 s
% 18.46/5.23 % (3321568)Peak memory usage: 133 MB
% 18.46/5.23 % (3321568)Instructions burned: 140 (million)
% 18.46/5.23 % (3321566)Instruction limit reached!
% 18.46/5.23 % (3321566)------------------------------
% 18.46/5.23 % (3321566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/5.23 % (3321566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/5.23 % (3321566)CaDiCaL version: 2.1.3
% 18.46/5.23 % (3321566)Termination reason: Instruction limit
% 18.46/5.23 % (3321566)Termination phase: SInE selection
% 18.46/5.23 % (3321566)Time elapsed: 0.080 s
% 18.46/5.23 % (3321566)Peak memory usage: 133 MB
% 18.46/5.23 % (3321566)Instructions burned: 111 (million)
% 18.46/5.23 % (3321567)Instruction limit reached!
% 18.46/5.23 % (3321567)------------------------------
% 18.46/5.23 % (3321567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/5.23 % (3321567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/5.23 % (3321567)CaDiCaL version: 2.1.3
% 18.46/5.23 % (3321567)Termination reason: Instruction limit
% 18.46/5.23 % (3321567)Termination phase: SInE selection
% 18.46/5.23 % (3321567)Time elapsed: 0.087 s
% 18.46/5.23 % (3321567)Peak memory usage: 133 MB
% 18.46/5.23 % (3321567)Instructions burned: 122 (million)
% 18.46/5.23 % (3321569)Instruction limit reached!
% 18.46/5.23 % (3321569)------------------------------
% 18.46/5.23 % (3321569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/5.23 % (3321569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/5.23 % (3321569)CaDiCaL version: 2.1.3
% 18.46/5.23 % (3321569)Termination reason: Instruction limit
% 18.46/5.23 % (3321569)Termination phase: SInE selection
% 18.46/5.23 % (3321569)Time elapsed: 0.088 s
% 18.46/5.23 % (3321569)Peak memory usage: 133 MB
% 18.46/5.23 % (3321569)Instructions burned: 130 (million)
% 18.46/5.23 % (3321577)lrs+10_1_sil=8000:sp=occurrence:random_seed=1126895408:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 18.46/5.23 % (3321578)lrs+10_1_sil=32000:urr=on:br=off:random_seed=559795649:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 18.46/5.23 % (3321579)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3260762337:i=325:sd=1:ss=axioms:sgt=32_2976 on theBenchmark for (2976ds/325Mi)
% 18.46/5.23 % (3321580)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=2902318521:s2a=on:i=248:s2at=1.23:gtg=position_2976 on theBenchmark for (2976ds/248Mi)
% 18.46/5.23 % (3321578)Instruction limit reached!
% 25.55/6.26 % (3321578)------------------------------
% 25.55/6.26 % (3321578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321578)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321578)Termination reason: Instruction limit
% 25.55/6.26 % (3321578)Termination phase: Property scanning
% 25.55/6.26 % (3321578)Time elapsed: 0.069 s
% 25.55/6.26 % (3321578)Peak memory usage: 133 MB
% 25.55/6.26 % (3321578)Instructions burned: 157 (million)
% 25.55/6.26 % (3321580)Instruction limit reached!
% 25.55/6.26 % (3321580)------------------------------
% 25.55/6.26 % (3321580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321580)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321580)Termination reason: Instruction limit
% 25.55/6.26 % (3321580)Termination phase: Property scanning
% 25.55/6.26 % (3321580)Time elapsed: 0.109 s
% 25.55/6.26 % (3321580)Peak memory usage: 133 MB
% 25.55/6.26 % (3321580)Instructions burned: 249 (million)
% 25.55/6.26 % (3321577)Instruction limit reached!
% 25.55/6.26 % (3321577)------------------------------
% 25.55/6.26 % (3321577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321577)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321577)Termination reason: Instruction limit
% 25.55/6.26 % (3321577)Termination phase: Saturation
% 25.55/6.26 % (3321577)Time elapsed: 0.221 s
% 25.55/6.26 % (3321577)Peak memory usage: 140 MB
% 25.55/6.26 % (3321577)Instructions burned: 286 (million)
% 25.55/6.26 % (3321585)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2221439788:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 25.55/6.26 % (3321579)Instruction limit reached!
% 25.55/6.26 % (3321579)------------------------------
% 25.55/6.26 % (3321579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321579)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321579)Termination reason: Instruction limit
% 25.55/6.26 % (3321579)Termination phase: Saturation
% 25.55/6.26 % (3321579)Time elapsed: 0.261 s
% 25.55/6.26 % (3321579)Peak memory usage: 140 MB
% 25.55/6.26 % (3321579)Instructions burned: 325 (million)
% 25.55/6.26 % (3321586)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=290837811:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 25.55/6.26 % (3321587)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2799289271:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 25.55/6.26 % (3321585)Instruction limit reached!
% 25.55/6.26 % (3321585)------------------------------
% 25.55/6.26 % (3321585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321585)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321585)Termination reason: Instruction limit
% 25.55/6.26 % (3321585)Termination phase: SInE selection
% 25.55/6.26 % (3321585)Time elapsed: 0.183 s
% 25.55/6.26 % (3321585)Peak memory usage: 134 MB
% 25.55/6.26 % (3321585)Instructions burned: 295 (million)
% 25.55/6.26 % (3321587)Instruction limit reached!
% 25.55/6.26 % (3321587)------------------------------
% 25.55/6.26 % (3321587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321587)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321587)Termination reason: Instruction limit
% 25.55/6.26 % (3321587)Termination phase: SInE selection
% 25.55/6.26 % (3321587)Time elapsed: 0.090 s
% 25.55/6.26 % (3321587)Peak memory usage: 133 MB
% 25.55/6.26 % (3321587)Instructions burned: 114 (million)
% 25.55/6.26 % (3321589)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3675659565:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 25.55/6.26 % (3321589)Instruction limit reached!
% 25.55/6.26 % (3321589)------------------------------
% 25.55/6.26 % (3321589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.55/6.26 % (3321589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.55/6.26 % (3321589)CaDiCaL version: 2.1.3
% 25.55/6.26 % (3321589)Termination reason: Instruction limit
% 19.91/7.69 % (3321589)Termination phase: Preprocessing 1
% 19.91/7.69 % (3321589)Time elapsed: 0.098 s
% 19.91/7.69 % (3321589)Peak memory usage: 136 MB
% 19.91/7.69 % (3321589)Instructions burned: 128 (million)
% 19.91/7.69 % (3321592)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4084454472:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 19.91/7.69 % (3321594)lrs+10_1_sil=8000:sp=occurrence:random_seed=939220631:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 19.91/7.69 % (3321592)Instruction limit reached!
% 19.91/7.69 % (3321592)------------------------------
% 19.91/7.69 % (3321592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321592)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321592)Termination reason: Instruction limit
% 19.91/7.69 % (3321592)Termination phase: Property scanning
% 19.91/7.69 % (3321592)Time elapsed: 0.052 s
% 19.91/7.69 % (3321592)Peak memory usage: 133 MB
% 19.91/7.69 % (3321592)Instructions burned: 114 (million)
% 19.91/7.69 % (3321595)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1993188233:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 19.91/7.69 % (3321598)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1255278383:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 19.91/7.69 % (3321595)Instruction limit reached!
% 19.91/7.69 % (3321595)------------------------------
% 19.91/7.69 % (3321595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321595)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321595)Termination reason: Instruction limit
% 19.91/7.69 % (3321595)Termination phase: Saturation
% 19.91/7.69 % (3321595)Time elapsed: 0.319 s
% 19.91/7.69 % (3321595)Peak memory usage: 142 MB
% 19.91/7.69 % (3321595)Instructions burned: 437 (million)
% 19.91/7.69 % (3321594)Instruction limit reached!
% 19.91/7.69 % (3321594)------------------------------
% 19.91/7.69 % (3321594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321594)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321594)Termination reason: Instruction limit
% 19.91/7.69 % (3321594)Termination phase: Property scanning
% 19.91/7.69 % (3321594)Time elapsed: 0.590 s
% 19.91/7.69 % (3321594)Peak memory usage: 154 MB
% 19.91/7.69 % (3321594)Instructions burned: 908 (million)
% 19.91/7.69 % (3321601)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4184476803:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 19.91/7.69 % (3321601)Instruction limit reached!
% 19.91/7.69 % (3321601)------------------------------
% 19.91/7.69 % (3321601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321601)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321601)Termination reason: Instruction limit
% 19.91/7.69 % (3321601)Termination phase: SInE selection
% 19.91/7.69 % (3321601)Time elapsed: 0.103 s
% 19.91/7.69 % (3321601)Peak memory usage: 133 MB
% 19.91/7.69 % (3321601)Instructions burned: 135 (million)
% 19.91/7.69 % (3321602)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=10756269:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 19.91/7.69 % (3321604)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1931479577:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 19.91/7.69 % (3321586)Instruction limit reached!
% 19.91/7.69 % (3321586)------------------------------
% 19.91/7.69 % (3321586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321586)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321586)Termination reason: Instruction limit
% 19.91/7.69 % (3321586)Termination phase: Property scanning
% 19.91/7.69 % (3321586)Time elapsed: 1.526 s
% 19.91/7.69 % (3321586)Peak memory usage: 227 MB
% 19.91/7.69 % (3321586)Instructions burned: 2353 (million)
% 19.91/7.69 % (3321602)Instruction limit reached!
% 19.91/7.69 % (3321602)------------------------------
% 19.91/7.69 % (3321602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321602)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321602)Termination reason: Instruction limit
% 19.91/7.69 % (3321602)Termination phase: Preprocessing 2
% 19.91/7.69 % (3321602)Time elapsed: 0.474 s
% 19.91/7.69 % (3321602)Peak memory usage: 146 MB
% 19.91/7.69 % (3321602)Instructions burned: 592 (million)
% 19.91/7.69 % (3321607)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3420842809:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 19.91/7.69 % (3321608)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1436536266:i=134:gtgl=5:slsql=off:gtg=exists_sym_2956 on theBenchmark for (2956ds/134Mi)
% 19.91/7.69 % (3321607)Instruction limit reached!
% 19.91/7.69 % (3321607)------------------------------
% 19.91/7.69 % (3321607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321607)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321607)Termination reason: Instruction limit
% 19.91/7.69 % (3321607)Termination phase: Property scanning
% 19.91/7.69 % (3321607)Time elapsed: 0.058 s
% 19.91/7.69 % (3321607)Peak memory usage: 133 MB
% 19.91/7.69 % (3321607)Instructions burned: 128 (million)
% 19.91/7.69 % (3321608)Instruction limit reached!
% 19.91/7.69 % (3321608)------------------------------
% 19.91/7.69 % (3321608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321608)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321608)Termination reason: Instruction limit
% 19.91/7.69 % (3321608)Termination phase: Property scanning
% 19.91/7.69 % (3321608)Time elapsed: 0.060 s
% 19.91/7.69 % (3321608)Peak memory usage: 133 MB
% 19.91/7.69 % (3321608)Instructions burned: 135 (million)
% 19.91/7.69 % (3321611)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2739954115:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/141Mi)
% 19.91/7.69 % (3321612)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1634762534:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 19.91/7.69 % (3321611)Instruction limit reached!
% 19.91/7.69 % (3321611)------------------------------
% 19.91/7.69 % (3321611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321611)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321611)Termination reason: Instruction limit
% 19.91/7.69 % (3321611)Termination phase: SInE selection
% 19.91/7.69 % (3321611)Time elapsed: 0.104 s
% 19.91/7.69 % (3321611)Peak memory usage: 133 MB
% 19.91/7.69 % (3321611)Instructions burned: 141 (million)
% 19.91/7.69 % (3321615)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1511785545:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 19.91/7.69 % (3321612)Instruction limit reached!
% 19.91/7.69 % (3321612)------------------------------
% 19.91/7.69 % (3321612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321612)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321612)Termination reason: Instruction limit
% 19.91/7.69 % (3321612)Termination phase: Saturation
% 19.91/7.69 % (3321612)Time elapsed: 0.316 s
% 19.91/7.69 % (3321612)Peak memory usage: 141 MB
% 19.91/7.69 % (3321612)Instructions burned: 432 (million)
% 19.91/7.69 % (3321617)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3300946721:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 19.91/7.69 % (3321617)Instruction limit reached!
% 19.91/7.69 % (3321617)------------------------------
% 19.91/7.69 % (3321617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321617)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321617)Termination reason: Instruction limit
% 19.91/7.69 % (3321617)Termination phase: SInE selection
% 19.91/7.69 % (3321617)Time elapsed: 0.121 s
% 19.91/7.69 % (3321617)Peak memory usage: 133 MB
% 19.91/7.69 % (3321617)Instructions burned: 150 (million)
% 19.91/7.69 % (3321619)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1646221617:i=14155:bd=all_2945 on theBenchmark for (2945ds/14155Mi)
% 19.91/7.69 % (3321564)First to succeed.
% 19.91/7.69 % (3321564)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3321558"
% 19.91/7.69 % (3321598)Instruction limit reached!
% 19.91/7.69 % (3321598)------------------------------
% 19.91/7.69 % (3321598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/7.69 % (3321598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/7.69 % (3321598)CaDiCaL version: 2.1.3
% 19.91/7.69 % (3321598)Termination reason: Instruction limit
% 19.91/7.69 % (3321598)Termination phase: Saturation
% 19.91/7.69 % (3321598)Time elapsed: 3.336 s
% 19.91/7.69 % (3321598)Peak memory usage: 247 MB
% 19.91/7.69 % (3321598)Instructions burned: 5203 (million)
% 19.91/7.69 % (3321564)Refutation found. Thanks to Tanya!
% 19.91/7.69 % SZS status Theorem for theBenchmark
% 19.91/7.69 % SZS output start Proof for theBenchmark
% See solution above
% 35.58/7.81 % (3321564)------------------------------
% 35.58/7.81 % (3321564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/7.81 % (3321564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/7.81 % (3321564)CaDiCaL version: 2.1.3
% 35.58/7.81 % (3321564)Termination reason: Refutation
% 35.58/7.81 % (3321564)Time elapsed: 4.127 s
% 35.58/7.81 % (3321564)Peak memory usage: 303 MB
% 35.58/7.81 % (3321564)Instructions burned: 6550 (million)
% 35.58/7.81 % (3321564)------------------------------
% 35.58/7.81 % (3321564)------------------------------
% 35.58/7.81 % (3321558)Success in time 6.825 s
% 35.58/7.81 % Vampire exiting
%------------------------------------------------------------------------------