%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT290+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 11:46:34 AM UTC 2026
% Result : Theorem 10.97s 3.82s
% Output : Refutation 19.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 24
% Syntax : Number of formulae : 193 ( 29 unt; 13 def)
% Number of atoms : 996 ( 87 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 1274 ( 471 ~; 627 |; 130 &)
% ( 24 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 14 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-3 aty)
% Number of variables : 123 ( 0 sgn 107 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f420,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> r1_tarski(k3_tarski(X0),k3_tarski(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t95_zfmisc_1) ).
fof(f424,axiom,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(f669,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> k5_setfam_1(X0,X1) = k3_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f4618,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ( v2_pre_topc(X0)
<=> ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
=> ( r1_tarski(X1,u1_pre_topc(X0))
=> r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0)) ) )
& ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( r2_hidden(X1,u1_pre_topc(X0))
& r2_hidden(X2,u1_pre_topc(X0)) )
=> r2_hidden(k5_subset_1(u1_struct_0(X0),X1,X2),u1_pre_topc(X0)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_pre_topc) ).
fof(f6388,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1) )
=> ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_1_2_lopclset) ).
fof(f6406,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_lopclset) ).
fof(f6445,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_lopclset) ).
fof(f6447,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( v1_pre_topc(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_lopclset) ).
fof(f6448,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_lopclset) ).
fof(f6454,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k3_tarski(k10_lopclset(X0)) = k7_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_lopclset) ).
fof(f6455,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k3_tarski(k10_lopclset(X0)) = k7_lopclset(X0) ),
inference(negated_conjecture,[status(cth)],[f6454]) ).
fof(f6461,plain,
! [X0] :
( l1_pre_topc(X0)
=> ( v2_pre_topc(X0)
<=> ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
=> ( r1_tarski(X1,u1_pre_topc(X0))
=> r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0)) ) )
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( r2_hidden(X2,u1_pre_topc(X0))
& r2_hidden(X3,u1_pre_topc(X0)) )
=> r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0)) ) ) ) ) ) ),
inference(rectify,[],[f4618]) ).
fof(f6504,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f6388]) ).
fof(f6505,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f6504]) ).
fof(f6538,plain,
! [X0] :
( ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6406]) ).
fof(f6539,plain,
! [X0] :
( ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6538]) ).
fof(f6610,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6445]) ).
fof(f6611,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6610]) ).
fof(f6614,plain,
! [X0] :
( ! [X1] :
( ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6447]) ).
fof(f6615,plain,
! [X0] :
( ! [X1] :
( ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6614]) ).
fof(f6616,plain,
! [X0] :
( ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6448]) ).
fof(f6617,plain,
! [X0] :
( ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6616]) ).
fof(f6628,plain,
? [X0] :
( k7_lopclset(X0) != k3_tarski(k10_lopclset(X0))
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f6455]) ).
fof(f6629,plain,
? [X0] :
( k7_lopclset(X0) != k3_tarski(k10_lopclset(X0))
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6628]) ).
fof(f6722,plain,
! [X0,X1] :
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f669]) ).
fof(f7063,plain,
! [X0] :
( ( v2_pre_topc(X0)
<=> ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
| ~ r1_tarski(X1,u1_pre_topc(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X2] :
( ! [X3] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
| ~ r2_hidden(X2,u1_pre_topc(X0))
| ~ r2_hidden(X3,u1_pre_topc(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6461]) ).
fof(f7064,plain,
! [X0] :
( ( v2_pre_topc(X0)
<=> ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
| ~ r1_tarski(X1,u1_pre_topc(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X2] :
( ! [X3] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
| ~ r2_hidden(X2,u1_pre_topc(X0))
| ~ r2_hidden(X3,u1_pre_topc(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f7063]) ).
fof(f7152,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),k3_tarski(X1))
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f420]) ).
fof(f7161,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(nnf_transformation,[],[f6505]) ).
fof(f7162,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& k5_setfam_1(k7_lopclset(X1),X3) = X0
& r1_tarski(X3,k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(rectify,[],[f7161]) ).
fof(f7163,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ( m1_subset_1(sK2(X0,X1),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& k5_setfam_1(k7_lopclset(X1),sK2(X0,X1)) = X0
& r1_tarski(sK2(X0,X1),k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1))],[f7162]) ).
fof(f7188,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k11_lopclset(X0)
| u1_struct_0(X1) != k7_lopclset(X0)
| u1_pre_topc(X1) != a_1_2_lopclset(X0) )
& ( ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) )
| k11_lopclset(X0) != X1 ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6615]) ).
fof(f7189,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k11_lopclset(X0)
| u1_struct_0(X1) != k7_lopclset(X0)
| u1_pre_topc(X1) != a_1_2_lopclset(X0) )
& ( ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) )
| k11_lopclset(X0) != X1 ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7188]) ).
fof(f7190,plain,
( k7_lopclset(sK12) != k3_tarski(k10_lopclset(sK12))
& ~ v3_struct_0(sK12)
& v10_lattices(sK12)
& v17_lattices(sK12)
& ~ v3_realset2(sK12)
& l3_lattices(sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X0,sK12)],[f6629]) ).
fof(f7243,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f7244,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f7243]) ).
fof(f7370,plain,
! [X0] :
( ( ( v2_pre_topc(X0)
| ~ r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
| ? [X1] :
( ~ r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
& r1_tarski(X1,u1_pre_topc(X0))
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
& r2_hidden(X2,u1_pre_topc(X0))
& r2_hidden(X3,u1_pre_topc(X0))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
| ~ r1_tarski(X1,u1_pre_topc(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X2] :
( ! [X3] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
| ~ r2_hidden(X2,u1_pre_topc(X0))
| ~ r2_hidden(X3,u1_pre_topc(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v2_pre_topc(X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f7064]) ).
fof(f7371,plain,
! [X0] :
( ( ( v2_pre_topc(X0)
| ~ r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
| ? [X1] :
( ~ r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
& r1_tarski(X1,u1_pre_topc(X0))
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
& r2_hidden(X2,u1_pre_topc(X0))
& r2_hidden(X3,u1_pre_topc(X0))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X1] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
| ~ r1_tarski(X1,u1_pre_topc(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X2] :
( ! [X3] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
| ~ r2_hidden(X2,u1_pre_topc(X0))
| ~ r2_hidden(X3,u1_pre_topc(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v2_pre_topc(X0) ) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f7370]) ).
fof(f7372,plain,
! [X0] :
( ( ( v2_pre_topc(X0)
| ~ r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
| ? [X1] :
( ~ r2_hidden(k5_setfam_1(u1_struct_0(X0),X1),u1_pre_topc(X0))
& r1_tarski(X1,u1_pre_topc(X0))
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k5_subset_1(u1_struct_0(X0),X2,X3),u1_pre_topc(X0))
& r2_hidden(X2,u1_pre_topc(X0))
& r2_hidden(X3,u1_pre_topc(X0))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X4] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X4),u1_pre_topc(X0))
| ~ r1_tarski(X4,u1_pre_topc(X0))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X5] :
( ! [X6] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X5,X6),u1_pre_topc(X0))
| ~ r2_hidden(X5,u1_pre_topc(X0))
| ~ r2_hidden(X6,u1_pre_topc(X0))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v2_pre_topc(X0) ) )
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f7371]) ).
fof(f7373,plain,
! [X0] :
( ( ( v2_pre_topc(X0)
| ~ r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
| ( ~ r2_hidden(k5_setfam_1(u1_struct_0(X0),sK127(X0)),u1_pre_topc(X0))
& r1_tarski(sK127(X0),u1_pre_topc(X0))
& m1_subset_1(sK127(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
| ( ~ r2_hidden(k5_subset_1(u1_struct_0(X0),sK128(X0),sK129(X0)),u1_pre_topc(X0))
& r2_hidden(sK128(X0),u1_pre_topc(X0))
& r2_hidden(sK129(X0),u1_pre_topc(X0))
& m1_subset_1(sK129(X0),k1_zfmisc_1(u1_struct_0(X0)))
& m1_subset_1(sK128(X0),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
& ! [X4] :
( r2_hidden(k5_setfam_1(u1_struct_0(X0),X4),u1_pre_topc(X0))
| ~ r1_tarski(X4,u1_pre_topc(X0))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) )
& ! [X5] :
( ! [X6] :
( r2_hidden(k5_subset_1(u1_struct_0(X0),X5,X6),u1_pre_topc(X0))
| ~ r2_hidden(X5,u1_pre_topc(X0))
| ~ r2_hidden(X6,u1_pre_topc(X0))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v2_pre_topc(X0) ) )
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK127,sK128,sK129]),skolemize(X1,sK127(X0)),skolemize(X2,sK128(X0)),skolemize(X3,sK129(X0))],[f7372]) ).
fof(f7432,plain,
! [X0,X1] :
( r1_tarski(sK2(X0,X1),k10_lopclset(X1))
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f7163]) ).
fof(f7433,plain,
! [X0,X1] :
( k5_setfam_1(k7_lopclset(X1),sK2(X0,X1)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f7163]) ).
fof(f7434,plain,
! [X0,X1] :
( m1_subset_1(sK2(X0,X1),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f7163]) ).
fof(f7461,plain,
! [X0] :
( l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6539]) ).
fof(f7540,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6611]) ).
fof(f7544,plain,
! [X0,X1] :
( u1_pre_topc(X1) = a_1_2_lopclset(X0)
| k11_lopclset(X0) != X1
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7189]) ).
fof(f7545,plain,
! [X0,X1] :
( u1_struct_0(X1) = k7_lopclset(X0)
| k11_lopclset(X0) != X1
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7189]) ).
fof(f7547,plain,
! [X0] :
( v2_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6617]) ).
fof(f7548,plain,
! [X0] :
( v1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6617]) ).
fof(f7555,plain,
l3_lattices(sK12),
inference(cnf_transformation,[],[f7190]) ).
fof(f7556,plain,
~ v3_realset2(sK12),
inference(cnf_transformation,[],[f7190]) ).
fof(f7557,plain,
v17_lattices(sK12),
inference(cnf_transformation,[],[f7190]) ).
fof(f7558,plain,
v10_lattices(sK12),
inference(cnf_transformation,[],[f7190]) ).
fof(f7559,plain,
~ v3_struct_0(sK12),
inference(cnf_transformation,[],[f7190]) ).
fof(f7560,plain,
k7_lopclset(sK12) != k3_tarski(k10_lopclset(sK12)),
inference(cnf_transformation,[],[f7190]) ).
fof(f7689,plain,
! [X0,X1] :
( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f7244]) ).
fof(f7706,plain,
! [X0,X1] :
( k3_tarski(X1) = k5_setfam_1(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f6722]) ).
fof(f8288,plain,
! [X0] :
( r2_hidden(u1_struct_0(X0),u1_pre_topc(X0))
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f7373]) ).
fof(f8468,plain,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
inference(cnf_transformation,[],[f424]) ).
fof(f8473,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),k3_tarski(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f7152]) ).
fof(f8648,plain,
! [X0] :
( k7_lopclset(X0) = u1_struct_0(k11_lopclset(X0))
| ~ v1_pre_topc(k11_lopclset(X0))
| ~ v2_pre_topc(k11_lopclset(X0))
| ~ l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f7545]) ).
fof(f8649,plain,
! [X0] :
( a_1_2_lopclset(X0) = u1_pre_topc(k11_lopclset(X0))
| ~ v1_pre_topc(k11_lopclset(X0))
| ~ v2_pre_topc(k11_lopclset(X0))
| ~ l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f7544]) ).
fof(f8803,definition,
( spl190_1
<=> v3_realset2(sK12) ),
introduced(definition,[new_symbols(definition,[spl190_1])],[avatar_definition]) ).
fof(f8805,plain,
( ~ v3_realset2(sK12)
| spl190_1 ),
inference(avatar_component_clause,[],[f8803]) ).
fof(f8806,plain,
~ spl190_1,
inference(avatar_split_clause,[],[f7556,f8803]) ).
fof(f8808,definition,
( spl190_2
<=> k7_lopclset(sK12) = k3_tarski(k10_lopclset(sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_2])],[avatar_definition]) ).
fof(f8810,plain,
( k7_lopclset(sK12) != k3_tarski(k10_lopclset(sK12))
| spl190_2 ),
inference(avatar_component_clause,[],[f8808]) ).
fof(f8811,plain,
~ spl190_2,
inference(avatar_split_clause,[],[f7560,f8808]) ).
fof(f8816,definition,
( spl190_3
<=> v3_struct_0(sK12) ),
introduced(definition,[new_symbols(definition,[spl190_3])],[avatar_definition]) ).
fof(f8818,plain,
( ~ v3_struct_0(sK12)
| spl190_3 ),
inference(avatar_component_clause,[],[f8816]) ).
fof(f8819,plain,
~ spl190_3,
inference(avatar_split_clause,[],[f7559,f8816]) ).
fof(f8833,plain,
( l1_pre_topc(k11_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f7461]) ).
fof(f8861,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f7540]) ).
fof(f8865,plain,
( v2_pre_topc(k11_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f7547]) ).
fof(f8866,plain,
( v1_pre_topc(k11_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f7548]) ).
fof(f8886,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f8648]) ).
fof(f8887,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1 ),
inference(resolution,[],[f8805,f8649]) ).
fof(f8888,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8887,f8818]) ).
fof(f8889,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8886,f8818]) ).
fof(f8906,plain,
( v1_pre_topc(k11_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8866,f8818]) ).
fof(f8907,plain,
( v2_pre_topc(k11_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8865,f8818]) ).
fof(f8911,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8861,f8818]) ).
fof(f8937,plain,
( l1_pre_topc(k11_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8833,f8818]) ).
fof(f8951,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8888,f7558]) ).
fof(f8952,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8889,f7558]) ).
fof(f8968,plain,
( v1_pre_topc(k11_lopclset(sK12))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8906,f7558]) ).
fof(f8969,plain,
( v2_pre_topc(k11_lopclset(sK12))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8907,f7558]) ).
fof(f8973,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8911,f7558]) ).
fof(f8999,plain,
( l1_pre_topc(k11_lopclset(sK12))
| ~ v17_lattices(sK12)
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8937,f7558]) ).
fof(f9013,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8951,f7557]) ).
fof(f9014,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8952,f7557]) ).
fof(f9030,plain,
( v1_pre_topc(k11_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8968,f7557]) ).
fof(f9031,plain,
( v2_pre_topc(k11_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8969,f7557]) ).
fof(f9035,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8973,f7557]) ).
fof(f9061,plain,
( l1_pre_topc(k11_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f8999,f7557]) ).
fof(f9075,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9013,f7555]) ).
fof(f9076,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9014,f7555]) ).
fof(f9092,plain,
( v1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9030,f7555]) ).
fof(f9093,plain,
( v2_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9031,f7555]) ).
fof(f9097,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9035,f7555]) ).
fof(f9123,plain,
( l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9061,f7555]) ).
fof(f9137,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(backward_subsumption_resolution,[],[f9076,f9092]) ).
fof(f9138,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(backward_subsumption_resolution,[],[f9075,f9092]) ).
fof(f9148,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9137,f9093]) ).
fof(f9149,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9138,f9093]) ).
fof(f9152,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9148,f9123]) ).
fof(f9153,plain,
( a_1_2_lopclset(sK12) = u1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3 ),
inference(forward_subsumption_resolution,[],[f9149,f9123]) ).
fof(f9155,definition,
( spl190_4
<=> l3_lattices(sK12) ),
introduced(definition,[new_symbols(definition,[spl190_4])],[avatar_definition]) ).
fof(f9157,plain,
( l3_lattices(sK12)
| ~ spl190_4 ),
inference(avatar_component_clause,[],[f9155]) ).
fof(f9158,plain,
spl190_4,
inference(avatar_split_clause,[],[f7555,f9155]) ).
fof(f9160,definition,
( spl190_5
<=> v10_lattices(sK12) ),
introduced(definition,[new_symbols(definition,[spl190_5])],[avatar_definition]) ).
fof(f9162,plain,
( v10_lattices(sK12)
| ~ spl190_5 ),
inference(avatar_component_clause,[],[f9160]) ).
fof(f9163,plain,
spl190_5,
inference(avatar_split_clause,[],[f7558,f9160]) ).
fof(f10026,definition,
( spl190_6
<=> k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_6])],[avatar_definition]) ).
fof(f10028,plain,
( k7_lopclset(sK12) = u1_struct_0(k11_lopclset(sK12))
| ~ spl190_6 ),
inference(avatar_component_clause,[],[f10026]) ).
fof(f10029,plain,
( spl190_6
| spl190_1
| spl190_3 ),
inference(avatar_split_clause,[],[f9152,f8816,f8803,f10026]) ).
fof(f10605,definition,
( spl190_7
<=> v17_lattices(sK12) ),
introduced(definition,[new_symbols(definition,[spl190_7])],[avatar_definition]) ).
fof(f10607,plain,
( v17_lattices(sK12)
| ~ spl190_7 ),
inference(avatar_component_clause,[],[f10605]) ).
fof(f10608,plain,
spl190_7,
inference(avatar_split_clause,[],[f7557,f10605]) ).
fof(f11058,plain,
( r2_hidden(k7_lopclset(sK12),u1_pre_topc(k11_lopclset(sK12)))
| ~ v2_pre_topc(k11_lopclset(sK12))
| ~ l1_pre_topc(k11_lopclset(sK12))
| ~ spl190_6 ),
inference(superposition,[],[f8288,f10028]) ).
fof(f11223,plain,
( r2_hidden(k7_lopclset(sK12),u1_pre_topc(k11_lopclset(sK12)))
| ~ l1_pre_topc(k11_lopclset(sK12))
| spl190_1
| spl190_3
| ~ spl190_6 ),
inference(forward_subsumption_resolution,[],[f11058,f9093]) ).
fof(f11530,plain,
( r2_hidden(k7_lopclset(sK12),u1_pre_topc(k11_lopclset(sK12)))
| spl190_1
| spl190_3
| ~ spl190_6 ),
inference(forward_subsumption_resolution,[],[f11223,f9123]) ).
fof(f11605,plain,
( r2_hidden(k7_lopclset(sK12),a_1_2_lopclset(sK12))
| spl190_1
| spl190_3
| ~ spl190_6 ),
inference(forward_demodulation,[],[f11530,f9153]) ).
fof(f12851,definition,
( spl190_16
<=> r2_hidden(k7_lopclset(sK12),a_1_2_lopclset(sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_16])],[avatar_definition]) ).
fof(f12853,plain,
( r2_hidden(k7_lopclset(sK12),a_1_2_lopclset(sK12))
| ~ spl190_16 ),
inference(avatar_component_clause,[],[f12851]) ).
fof(f12854,plain,
( spl190_16
| spl190_1
| spl190_3
| ~ spl190_6 ),
inference(avatar_split_clause,[],[f11605,f10026,f8816,f8803,f12851]) ).
fof(f12855,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| ~ spl190_16 ),
inference(resolution,[],[f12853,f7432]) ).
fof(f12856,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| ~ spl190_16 ),
inference(resolution,[],[f12853,f7433]) ).
fof(f12857,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| v3_struct_0(sK12)
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| ~ spl190_16 ),
inference(resolution,[],[f12853,f7434]) ).
fof(f12944,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12857,f8818]) ).
fof(f12945,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12856,f8818]) ).
fof(f12946,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| ~ v10_lattices(sK12)
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12855,f8818]) ).
fof(f12952,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12944,f9162]) ).
fof(f12953,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12945,f9162]) ).
fof(f12954,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| ~ v17_lattices(sK12)
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12946,f9162]) ).
fof(f12958,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12952,f10607]) ).
fof(f12959,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12953,f10607]) ).
fof(f12960,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| v3_realset2(sK12)
| ~ l3_lattices(sK12)
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12954,f10607]) ).
fof(f12963,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12958,f8805]) ).
fof(f12964,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12959,f8805]) ).
fof(f12965,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| ~ l3_lattices(sK12)
| spl190_1
| spl190_3
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12960,f8805]) ).
fof(f12966,plain,
( m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12963,f9157]) ).
fof(f12967,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12964,f9157]) ).
fof(f12968,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(forward_subsumption_resolution,[],[f12965,f9157]) ).
fof(f15183,definition,
( spl190_44
<=> k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_44])],[avatar_definition]) ).
fof(f15185,plain,
( k7_lopclset(sK12) = k5_setfam_1(k7_lopclset(sK12),sK2(k7_lopclset(sK12),sK12))
| ~ spl190_44 ),
inference(avatar_component_clause,[],[f15183]) ).
fof(f15186,plain,
( spl190_44
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(avatar_split_clause,[],[f12967,f12851,f10605,f9160,f9155,f8816,f8803,f15183]) ).
fof(f15199,plain,
( k7_lopclset(sK12) = k3_tarski(sK2(k7_lopclset(sK12),sK12))
| ~ m1_subset_1(sK2(k7_lopclset(sK12),sK12),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK12))))
| ~ spl190_44 ),
inference(superposition,[],[f7706,f15185]) ).
fof(f15211,plain,
( k7_lopclset(sK12) = k3_tarski(sK2(k7_lopclset(sK12),sK12))
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16
| ~ spl190_44 ),
inference(forward_subsumption_resolution,[],[f15199,f12966]) ).
fof(f15221,definition,
( spl190_46
<=> k7_lopclset(sK12) = k3_tarski(sK2(k7_lopclset(sK12),sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_46])],[avatar_definition]) ).
fof(f15223,plain,
( k7_lopclset(sK12) = k3_tarski(sK2(k7_lopclset(sK12),sK12))
| ~ spl190_46 ),
inference(avatar_component_clause,[],[f15221]) ).
fof(f15224,plain,
( spl190_46
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16
| ~ spl190_44 ),
inference(avatar_split_clause,[],[f15211,f15183,f12851,f10605,f9160,f9155,f8816,f8803,f15221]) ).
fof(f18469,definition,
( spl190_85
<=> r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_85])],[avatar_definition]) ).
fof(f18471,plain,
( r1_tarski(sK2(k7_lopclset(sK12),sK12),k10_lopclset(sK12))
| ~ spl190_85 ),
inference(avatar_component_clause,[],[f18469]) ).
fof(f18472,plain,
( spl190_85
| spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16 ),
inference(avatar_split_clause,[],[f12968,f12851,f10605,f9160,f9155,f8816,f8803,f18469]) ).
fof(f18509,plain,
( r1_tarski(k3_tarski(sK2(k7_lopclset(sK12),sK12)),k3_tarski(k10_lopclset(sK12)))
| ~ spl190_85 ),
inference(resolution,[],[f18471,f8473]) ).
fof(f18555,plain,
( r1_tarski(k7_lopclset(sK12),k3_tarski(k10_lopclset(sK12)))
| ~ spl190_46
| ~ spl190_85 ),
inference(forward_demodulation,[],[f18509,f15223]) ).
fof(f23345,definition,
( spl190_105
<=> r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12))) ),
introduced(definition,[new_symbols(definition,[spl190_105])],[avatar_definition]) ).
fof(f23347,plain,
( r1_tarski(k10_lopclset(sK12),k1_zfmisc_1(k7_lopclset(sK12)))
| ~ spl190_105 ),
inference(avatar_component_clause,[],[f23345]) ).
fof(f23348,plain,
( spl190_105
| spl190_1
| spl190_3 ),
inference(avatar_split_clause,[],[f9097,f8816,f8803,f23345]) ).
fof(f23384,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK12)),k3_tarski(k1_zfmisc_1(k7_lopclset(sK12))))
| ~ spl190_105 ),
inference(resolution,[],[f23347,f8473]) ).
fof(f23430,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK12)),k7_lopclset(sK12))
| ~ spl190_105 ),
inference(forward_demodulation,[],[f23384,f8468]) ).
fof(f23434,definition,
( spl190_106
<=> r1_tarski(k3_tarski(k10_lopclset(sK12)),k7_lopclset(sK12)) ),
introduced(definition,[new_symbols(definition,[spl190_106])],[avatar_definition]) ).
fof(f23436,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK12)),k7_lopclset(sK12))
| ~ spl190_106 ),
inference(avatar_component_clause,[],[f23434]) ).
fof(f23437,plain,
( spl190_106
| ~ spl190_105 ),
inference(avatar_split_clause,[],[f23430,f23345,f23434]) ).
fof(f23453,plain,
( k7_lopclset(sK12) = k3_tarski(k10_lopclset(sK12))
| ~ r1_tarski(k7_lopclset(sK12),k3_tarski(k10_lopclset(sK12)))
| ~ spl190_106 ),
inference(resolution,[],[f23436,f7689]) ).
fof(f23524,plain,
( ~ r1_tarski(k7_lopclset(sK12),k3_tarski(k10_lopclset(sK12)))
| spl190_2
| ~ spl190_106 ),
inference(forward_subsumption_resolution,[],[f23453,f8810]) ).
fof(f23531,plain,
( $false
| spl190_2
| ~ spl190_46
| ~ spl190_85
| ~ spl190_106 ),
inference(forward_subsumption_resolution,[],[f23524,f18555]) ).
fof(f23532,plain,
( spl190_2
| ~ spl190_46
| ~ spl190_85
| ~ spl190_106 ),
inference(avatar_contradiction_clause,[],[f23531]) ).
cnf(s1,plain,
~ spl190_1,
inference(sat_conversion,[],[f8806]) ).
cnf(s2,plain,
~ spl190_2,
inference(sat_conversion,[],[f8811]) ).
cnf(s3,plain,
~ spl190_3,
inference(sat_conversion,[],[f8819]) ).
cnf(s4,plain,
spl190_4,
inference(sat_conversion,[],[f9158]) ).
cnf(s5,plain,
spl190_5,
inference(sat_conversion,[],[f9163]) ).
cnf(s6,plain,
( spl190_1
| spl190_3
| spl190_6 ),
inference(sat_conversion,[],[f10029]) ).
cnf(s7,plain,
spl190_7,
inference(sat_conversion,[],[f10608]) ).
cnf(s16,plain,
( spl190_1
| spl190_3
| ~ spl190_6
| spl190_16 ),
inference(sat_conversion,[],[f12854]) ).
cnf(s42,plain,
( spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16
| spl190_44 ),
inference(sat_conversion,[],[f15186]) ).
cnf(s44,plain,
( spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16
| ~ spl190_44
| spl190_46 ),
inference(sat_conversion,[],[f15224]) ).
cnf(s83,plain,
( spl190_1
| spl190_3
| ~ spl190_4
| ~ spl190_5
| ~ spl190_7
| ~ spl190_16
| spl190_85 ),
inference(sat_conversion,[],[f18472]) ).
cnf(s124,plain,
( spl190_1
| spl190_3
| spl190_105 ),
inference(sat_conversion,[],[f23348]) ).
cnf(s125,plain,
( ~ spl190_105
| spl190_106 ),
inference(sat_conversion,[],[f23437]) ).
cnf(s127,plain,
( spl190_2
| ~ spl190_46
| ~ spl190_85
| ~ spl190_106 ),
inference(sat_conversion,[],[f23532]) ).
cnf(s143,plain,
spl190_105,
inference(rat,[],[s124,s3,s1]) ).
cnf(s171,plain,
spl190_6,
inference(rat,[],[s6,s3,s1]) ).
cnf(s172,plain,
spl190_106,
inference(rat,[],[s125,s143]) ).
cnf(s189,plain,
spl190_16,
inference(rat,[],[s16,s1,s3,s171]) ).
cnf(s195,plain,
spl190_85,
inference(rat,[],[s83,s1,s3,s7,s5,s4,s189]) ).
cnf(s196,plain,
spl190_44,
inference(rat,[],[s42,s1,s3,s7,s5,s4,s189]) ).
cnf(s197,plain,
~ spl190_46,
inference(rat,[],[s127,s172,s2,s195]) ).
cnf(s198,plain,
$false,
inference(rat,[],[s44,s189,s1,s3,s7,s5,s4,s197,s196]) ).
fof(f23533,plain,
$false,
inference(avatar_sat_refutation,[],[s198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT290+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:18:43 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.09/3.08 % (2887131)Detected formulas, will run a generic FOF schedule.
% 14.09/3.08 % (2887139)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3131577925:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 14.09/3.08 % (2887139)Refutation not found, incomplete strategy
% 14.09/3.08 % (2887139)------------------------------
% 14.09/3.08 % (2887139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.09/3.08 % (2887139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/3.08 % (2887139)CaDiCaL version: 2.1.3
% 14.09/3.08 % (2887139)Termination reason: Refutation not found, incomplete strategy
% 14.09/3.08 % (2887139)Time elapsed: 0.018 s
% 14.09/3.08 % (2887139)Peak memory usage: 96 MB
% 14.09/3.08 % (2887139)Instructions burned: 37 (million)
% 14.09/3.08 % (2887137)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=15455000:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 14.09/3.08 % (2887138)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=2014173191:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 14.09/3.08 % (2887142)dis-21_1_sil=8000:lcm=predicate:random_seed=943565552:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 14.09/3.08 % (2887141)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3804704911:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 14.09/3.08 % (2887136)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=238640485:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 14.09/3.08 % (2887140)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3768833461:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 14.09/3.08 % (2887140)Instruction limit reached!
% 14.09/3.08 % (2887140)------------------------------
% 14.09/3.08 % (2887140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.09/3.08 % (2887140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/3.08 % (2887140)CaDiCaL version: 2.1.3
% 14.09/3.08 % (2887140)Termination reason: Instruction limit
% 14.09/3.08 % (2887140)Termination phase: Saturation
% 14.09/3.08 % (2887140)Time elapsed: 0.082 s
% 14.09/3.08 % (2887140)Peak memory usage: 97 MB
% 14.09/3.08 % (2887140)Instructions burned: 119 (million)
% 14.09/3.08 % (2887141)Instruction limit reached!
% 14.09/3.08 % (2887141)------------------------------
% 14.09/3.08 % (2887141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.09/3.08 % (2887141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/3.08 % (2887141)CaDiCaL version: 2.1.3
% 14.09/3.08 % (2887141)Termination reason: Instruction limit
% 14.09/3.08 % (2887141)Termination phase: Preprocessing 1
% 14.09/3.08 % (2887141)Time elapsed: 0.083 s
% 14.09/3.08 % (2887141)Peak memory usage: 93 MB
% 14.09/3.08 % (2887141)Instructions burned: 139 (million)
% 14.09/3.08 % (2887142)Instruction limit reached!
% 14.09/3.08 % (2887142)------------------------------
% 14.09/3.08 % (2887142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.09/3.08 % (2887142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/3.08 % (2887142)CaDiCaL version: 2.1.3
% 14.09/3.08 % (2887142)Termination reason: Instruction limit
% 14.09/3.08 % (2887142)Termination phase: Preprocessing 3
% 14.09/3.08 % (2887142)Time elapsed: 0.101 s
% 14.09/3.08 % (2887142)Peak memory usage: 97 MB
% 14.09/3.08 % (2887142)Instructions burned: 130 (million)
% 14.09/3.08 % (2887139)------------------------------
% 14.09/3.08 % (2887139)------------------------------
% 14.09/3.08 % (2887153)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=1479777291:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 14.09/3.08 % (2887151)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2731962722:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 14.09/3.08 % (2887150)lrs+10_1_sil=8000:sp=occurrence:random_seed=2680925707:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 14.09/3.08 % (2887152)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2135226374:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 10.97/3.81 % (2887153)Instruction limit reached!
% 10.97/3.81 % (2887153)------------------------------
% 10.97/3.81 % (2887153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.81 % (2887153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.81 % (2887153)CaDiCaL version: 2.1.3
% 10.97/3.81 % (2887153)Termination reason: Instruction limit
% 10.97/3.81 % (2887153)Termination phase: Preprocessing 3
% 10.97/3.81 % (2887153)Time elapsed: 0.086 s
% 10.97/3.81 % (2887153)Peak memory usage: 101 MB
% 10.97/3.81 % (2887153)Instructions burned: 250 (million)
% 10.97/3.81 % (2887151)Instruction limit reached!
% 10.97/3.81 % (2887151)------------------------------
% 10.97/3.81 % (2887151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.81 % (2887151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.81 % (2887151)CaDiCaL version: 2.1.3
% 10.97/3.81 % (2887151)Termination reason: Instruction limit
% 10.97/3.81 % (2887151)Termination phase: Saturation
% 10.97/3.81 % (2887151)Time elapsed: 0.085 s
% 10.97/3.81 % (2887151)Peak memory usage: 97 MB
% 10.97/3.81 % (2887151)Instructions burned: 159 (million)
% 10.97/3.81 % (2887158)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1448913689:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 10.97/3.81 % (2887150)Instruction limit reached!
% 10.97/3.81 % (2887150)------------------------------
% 10.97/3.81 % (2887150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.81 % (2887150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.81 % (2887150)CaDiCaL version: 2.1.3
% 10.97/3.81 % (2887150)Termination reason: Instruction limit
% 10.97/3.81 % (2887150)Termination phase: Saturation
% 10.97/3.81 % (2887150)Time elapsed: 0.198 s
% 10.97/3.81 % (2887150)Peak memory usage: 100 MB
% 10.97/3.81 % (2887150)Instructions burned: 286 (million)
% 10.97/3.81 % (2887159)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=767931458:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 10.97/3.81 % (2887158)Refutation not found, incomplete strategy
% 10.97/3.81 % (2887158)------------------------------
% 10.97/3.81 % (2887158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887158)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887158)Termination reason: Refutation not found, incomplete strategy
% 10.97/3.82 % (2887158)Time elapsed: 0.068 s
% 10.97/3.82 % (2887158)Peak memory usage: 100 MB
% 10.97/3.82 % (2887158)Instructions burned: 199 (million)
% 10.97/3.82 % (2887152)Instruction limit reached!
% 10.97/3.82 % (2887152)------------------------------
% 10.97/3.82 % (2887152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887152)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887152)Termination reason: Instruction limit
% 10.97/3.82 % (2887152)Termination phase: Saturation
% 10.97/3.82 % (2887152)Time elapsed: 0.216 s
% 10.97/3.82 % (2887152)Peak memory usage: 100 MB
% 10.97/3.82 % (2887152)Instructions burned: 326 (million)
% 10.97/3.82 % (2887162)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3007302157:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 10.97/3.82 % (2887158)------------------------------
% 10.97/3.82 % (2887158)------------------------------
% 10.97/3.82 % (2887163)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3035561232:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.97/3.82 % (2887162)Instruction limit reached!
% 10.97/3.82 % (2887162)------------------------------
% 10.97/3.82 % (2887162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887162)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887162)Termination reason: Instruction limit
% 10.97/3.82 % (2887162)Termination phase: Property scanning
% 10.97/3.82 % (2887162)Time elapsed: 0.082 s
% 10.97/3.82 % (2887162)Peak memory usage: 96 MB
% 10.97/3.82 % (2887162)Instructions burned: 115 (million)
% 10.97/3.82 % (2887165)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1644732231:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 10.97/3.82 % (2887163)Instruction limit reached!
% 10.97/3.82 % (2887163)------------------------------
% 10.97/3.82 % (2887163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887163)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887163)Termination reason: Instruction limit
% 10.97/3.82 % (2887163)Termination phase: Preprocessing 3
% 10.97/3.82 % (2887163)Time elapsed: 0.096 s
% 10.97/3.82 % (2887163)Peak memory usage: 100 MB
% 10.97/3.82 % (2887163)Instructions burned: 128 (million)
% 10.97/3.82 % (2887165)Instruction limit reached!
% 10.97/3.82 % (2887165)------------------------------
% 10.97/3.82 % (2887165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887165)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887165)Termination reason: Instruction limit
% 10.97/3.82 % (2887165)Termination phase: Property scanning
% 10.97/3.82 % (2887165)Time elapsed: 0.027 s
% 10.97/3.82 % (2887165)Peak memory usage: 92 MB
% 10.97/3.82 % (2887165)Instructions burned: 114 (million)
% 10.97/3.82 % (2887167)lrs+10_1_sil=8000:sp=occurrence:random_seed=1306280401:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 10.97/3.82 % (2887170)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4138671725:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 10.97/3.82 % (2887169)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=643459397:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 10.97/3.82 % (2887169)Refutation not found, incomplete strategy
% 10.97/3.82 % (2887169)------------------------------
% 10.97/3.82 % (2887169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887169)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887169)Termination reason: Refutation not found, incomplete strategy
% 10.97/3.82 % (2887169)Time elapsed: 0.065 s
% 10.97/3.82 % (2887169)Peak memory usage: 98 MB
% 10.97/3.82 % (2887169)Instructions burned: 96 (million)
% 10.97/3.82 % (2887169)------------------------------
% 10.97/3.82 % (2887169)------------------------------
% 10.97/3.82 % (2887174)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2613106672:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 10.97/3.82 % (2887167)Instruction limit reached!
% 10.97/3.82 % (2887167)------------------------------
% 10.97/3.82 % (2887167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887167)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887167)Termination reason: Instruction limit
% 10.97/3.82 % (2887167)Termination phase: Saturation
% 10.97/3.82 % (2887167)Time elapsed: 0.535 s
% 10.97/3.82 % (2887167)Peak memory usage: 113 MB
% 10.97/3.82 % (2887167)Instructions burned: 907 (million)
% 10.97/3.82 % (2887174)Instruction limit reached!
% 10.97/3.82 % (2887174)------------------------------
% 10.97/3.82 % (2887174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887174)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887174)Termination reason: Instruction limit
% 10.97/3.82 % (2887174)Termination phase: Saturation
% 10.97/3.82 % (2887174)Time elapsed: 0.088 s
% 10.97/3.82 % (2887174)Peak memory usage: 98 MB
% 10.97/3.82 % (2887174)Instructions burned: 135 (million)
% 10.97/3.82 % (2887176)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1954298541:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 10.97/3.82 % (2887177)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1790303523:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 10.97/3.82 % (2887176)Instruction limit reached!
% 10.97/3.82 % (2887176)------------------------------
% 10.97/3.82 % (2887176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887176)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887176)Termination reason: Instruction limit
% 10.97/3.82 % (2887176)Termination phase: Property scanning
% 10.97/3.82 % (2887176)Time elapsed: 0.320 s
% 10.97/3.82 % (2887176)Peak memory usage: 104 MB
% 10.97/3.82 % (2887176)Instructions burned: 593 (million)
% 10.97/3.82 % (2887180)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=2030627133:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 10.97/3.82 % (2887180)Instruction limit reached!
% 10.97/3.82 % (2887180)------------------------------
% 10.97/3.82 % (2887180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887180)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887180)Termination reason: Instruction limit
% 10.97/3.82 % (2887180)Termination phase: SInE selection
% 10.97/3.82 % (2887180)Time elapsed: 0.074 s
% 10.97/3.82 % (2887180)Peak memory usage: 92 MB
% 10.97/3.82 % (2887180)Instructions burned: 125 (million)
% 10.97/3.82 % (2887159)Instruction limit reached!
% 10.97/3.82 % (2887159)------------------------------
% 10.97/3.82 % (2887159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887159)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887159)Termination reason: Instruction limit
% 10.97/3.82 % (2887159)Termination phase: Saturation
% 10.97/3.82 % (2887159)Time elapsed: 1.620 s
% 10.97/3.82 % (2887159)Peak memory usage: 294 MB
% 10.97/3.82 % (2887159)Instructions burned: 2350 (million)
% 10.97/3.82 % (2887182)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2479871156:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 10.97/3.82 % (2887183)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3726981467:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 10.97/3.82 % (2887138)First to succeed.
% 10.97/3.82 % (2887182)Instruction limit reached!
% 10.97/3.82 % (2887182)------------------------------
% 10.97/3.82 % (2887182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887182)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887182)Termination reason: Instruction limit
% 10.97/3.82 % (2887182)Termination phase: Property scanning
% 10.97/3.82 % (2887182)Time elapsed: 0.060 s
% 10.97/3.82 % (2887182)Peak memory usage: 92 MB
% 10.97/3.82 % (2887182)Instructions burned: 137 (million)
% 10.97/3.82 % (2887138)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2887131"
% 10.97/3.82 % (2887183)Refutation not found, incomplete strategy
% 10.97/3.82 % (2887183)------------------------------
% 10.97/3.82 % (2887183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887183)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887183)Termination reason: Refutation not found, incomplete strategy
% 10.97/3.82 % (2887183)Time elapsed: 0.028 s
% 10.97/3.82 % (2887183)Peak memory usage: 96 MB
% 10.97/3.82 % (2887183)Instructions burned: 35 (million)
% 10.97/3.82 % (2887186)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2077758563:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 10.97/3.82 % (2887186)Refutation not found, incomplete strategy
% 10.97/3.82 % (2887186)------------------------------
% 10.97/3.82 % (2887186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/3.82 % (2887186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/3.82 % (2887186)CaDiCaL version: 2.1.3
% 10.97/3.82 % (2887186)Termination reason: Refutation not found, incomplete strategy
% 10.97/3.82 % (2887186)Time elapsed: 0.033 s
% 10.97/3.82 % (2887186)Peak memory usage: 96 MB
% 10.97/3.82 % (2887186)Instructions burned: 40 (million)
% 10.97/3.82 % (2887183)------------------------------
% 10.97/3.82 % (2887183)------------------------------
% 10.97/3.82 % (2887138)Refutation found. Thanks to Tanya!
% 10.97/3.82 % SZS status Theorem for theBenchmark
% 10.97/3.82 % SZS output start Proof for theBenchmark
% See solution above
% 19.59/4.03 % (2887138)------------------------------
% 19.59/4.03 % (2887138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.59/4.03 % (2887138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.59/4.03 % (2887138)CaDiCaL version: 2.1.3
% 19.59/4.03 % (2887138)Termination reason: Refutation
% 19.59/4.03 % (2887138)Time elapsed: 2.217 s
% 19.59/4.03 % (2887138)Peak memory usage: 162 MB
% 19.59/4.03 % (2887138)Instructions burned: 3501 (million)
% 19.59/4.03 % (2887138)------------------------------
% 19.59/4.03 % (2887138)------------------------------
% 19.59/4.03 % (2887131)Success in time 2.949 s
% 19.59/4.03 % Vampire exiting
%------------------------------------------------------------------------------