%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP648+4 : 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 : n001.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:17 AM UTC 2026
% Result : Theorem 18.52s 8.27s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 17
% Syntax : Number of formulae : 184 ( 28 unt; 5 def)
% Number of atoms : 820 ( 54 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1092 ( 456 ~; 491 |; 96 &)
% ( 14 <=>; 33 =>; 0 <=; 2 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 6 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 224 ( 0 sgn 204 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f677,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f21806,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> v4_group_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_group_2) ).
fof(f21877,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
=> m1_group_2(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t66_group_2) ).
fof(f21900,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> k7_group_2(X0,X1) = u1_struct_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_group_2) ).
fof(f22007,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f22018,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_group_2) ).
fof(f22987,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> u1_struct_0(k11_group_4(X0)) = k1_group_3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t92_group_4) ).
fof(f27005,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f36521,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_latsubgr) ).
fof(f36522,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_latsubgr) ).
fof(f36523,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36522]) ).
fof(f36665,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f36521]) ).
fof(f36666,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36665]) ).
fof(f36667,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f36523]) ).
fof(f36668,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f36667]) ).
fof(f36695,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22007]) ).
fof(f36696,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36695]) ).
fof(f36697,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21877]) ).
fof(f36698,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36697]) ).
fof(f36709,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21806]) ).
fof(f36710,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36709]) ).
fof(f36723,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22987]) ).
fof(f36724,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36723]) ).
fof(f37049,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f27005]) ).
fof(f37050,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f37049]) ).
fof(f37810,plain,
! [X0,X1] :
( m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f22018]) ).
fof(f37811,plain,
! [X0,X1] :
( m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f37810]) ).
fof(f37826,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21900]) ).
fof(f37827,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37826]) ).
fof(f39010,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f39796,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f42294,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ( r3_lattices(k11_group_4(X0),X3,X4)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
& ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X3,X4) ) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f36666]) ).
fof(f42295,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( ~ m1_group_6(X1,X0,X2)
| ~ r3_lattices(k11_group_4(X0),X3,X4) )
& ( m1_group_6(X1,X0,X2)
| r3_lattices(k11_group_4(X0),X3,X4) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(nnf_transformation,[],[f36668]) ).
fof(f42296,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( ~ m1_group_6(X1,X0,X2)
| ~ r3_lattices(k11_group_4(X0),X3,X4) )
& ( m1_group_6(X1,X0,X2)
| r3_lattices(k11_group_4(X0),X3,X4) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f42295]) ).
fof(f42297,plain,
( ( ~ m1_group_6(sK36,sK35,sK37)
| ~ r3_lattices(k11_group_4(sK35),sK38,sK39) )
& ( m1_group_6(sK36,sK35,sK37)
| r3_lattices(k11_group_4(sK35),sK38,sK39) )
& sK36 = sK38
& sK37 = sK39
& m1_subset_1(sK39,u1_struct_0(k11_group_4(sK35)))
& m1_subset_1(sK38,u1_struct_0(k11_group_4(sK35)))
& m1_group_2(sK37,sK35)
& m1_group_2(sK36,sK35)
& ~ v3_struct_0(sK35)
& v3_group_1(sK35)
& v4_group_1(sK35)
& l1_group_1(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36,sK37,sK38,sK39]),skolemize(X0,sK35),skolemize(X1,sK36),skolemize(X2,sK37),skolemize(X3,sK38),skolemize(X4,sK39)],[f42296]) ).
fof(f42407,plain,
! [X0,X1] :
( ! [X2] :
( ( m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X1) )
& ( m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,X1) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(nnf_transformation,[],[f37050]) ).
fof(f42409,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f677]) ).
fof(f43996,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42294]) ).
fof(f43997,plain,
! [X2,X3,X0,X1,X4] :
( r3_lattices(k11_group_4(X0),X3,X4)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42294]) ).
fof(f43998,plain,
l1_group_1(sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f43999,plain,
v4_group_1(sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f44000,plain,
v3_group_1(sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f44001,plain,
~ v3_struct_0(sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f44002,plain,
m1_group_2(sK36,sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f44003,plain,
m1_group_2(sK37,sK35),
inference(cnf_transformation,[],[f42297]) ).
fof(f44004,plain,
m1_subset_1(sK38,u1_struct_0(k11_group_4(sK35))),
inference(cnf_transformation,[],[f42297]) ).
fof(f44005,plain,
m1_subset_1(sK39,u1_struct_0(k11_group_4(sK35))),
inference(cnf_transformation,[],[f42297]) ).
fof(f44006,plain,
sK37 = sK39,
inference(cnf_transformation,[],[f42297]) ).
fof(f44007,plain,
sK36 = sK38,
inference(cnf_transformation,[],[f42297]) ).
fof(f44008,plain,
( m1_group_6(sK36,sK35,sK37)
| r3_lattices(k11_group_4(sK35),sK38,sK39) ),
inference(cnf_transformation,[],[f42297]) ).
fof(f44009,plain,
( ~ m1_group_6(sK36,sK35,sK37)
| ~ r3_lattices(k11_group_4(sK35),sK38,sK39) ),
inference(cnf_transformation,[],[f42297]) ).
fof(f44055,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| l1_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36696]) ).
fof(f44056,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| v3_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36696]) ).
fof(f44057,plain,
! [X0,X1] :
( ~ v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36696]) ).
fof(f44058,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X1,X2)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36698]) ).
fof(f44065,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v4_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36710]) ).
fof(f44093,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k1_group_3(X0) = u1_struct_0(k11_group_4(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36724]) ).
fof(f44469,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_6(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X2,X1)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f42407]) ).
fof(f44470,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_6(X2,X0,X1)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f42407]) ).
fof(f44499,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f42409]) ).
fof(f45593,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f37811]) ).
fof(f45607,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| u1_struct_0(X1) = k7_group_2(X0,X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37827]) ).
fof(f47165,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39010]) ).
fof(f48030,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f39796]) ).
fof(f51631,plain,
( ~ m1_group_6(sK38,sK35,sK39)
| ~ r3_lattices(k11_group_4(sK35),sK38,sK39) ),
inference(definition_unfolding,[],[f44009,f44007,f44006]) ).
fof(f51632,plain,
( m1_group_6(sK38,sK35,sK39)
| r3_lattices(k11_group_4(sK35),sK38,sK39) ),
inference(definition_unfolding,[],[f44008,f44007,f44006]) ).
fof(f51633,plain,
m1_group_2(sK39,sK35),
inference(definition_unfolding,[],[f44003,f44006]) ).
fof(f51634,plain,
m1_group_2(sK38,sK35),
inference(definition_unfolding,[],[f44002,f44007]) ).
fof(f53049,plain,
! [X2,X3,X0,X4] :
( r3_lattices(k11_group_4(X0),X3,X4)
| ~ r1_tarski(u1_struct_0(X3),u1_struct_0(X2))
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f43997]) ).
fof(f53050,plain,
! [X3,X0,X4] :
( ~ r1_tarski(u1_struct_0(X3),u1_struct_0(X4))
| r3_lattices(k11_group_4(X0),X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f53049]) ).
fof(f53051,plain,
! [X2,X3,X0,X4] :
( r1_tarski(u1_struct_0(X3),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f43996]) ).
fof(f53052,plain,
! [X3,X0,X4] :
( ~ v4_group_1(X0)
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| r1_tarski(u1_struct_0(X3),u1_struct_0(X4))
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f53051]) ).
fof(f54147,definition,
( spl1150_37
<=> r3_lattices(k11_group_4(sK35),sK38,sK39) ),
introduced(definition,[new_symbols(definition,[spl1150_37])],[avatar_definition]) ).
fof(f54148,plain,
( r3_lattices(k11_group_4(sK35),sK38,sK39)
| ~ spl1150_37 ),
inference(avatar_component_clause,[],[f54147]) ).
fof(f54150,definition,
( spl1150_38
<=> m1_group_6(sK38,sK35,sK39) ),
introduced(definition,[new_symbols(definition,[spl1150_38])],[avatar_definition]) ).
fof(f54151,plain,
( m1_group_6(sK38,sK35,sK39)
| ~ spl1150_38 ),
inference(avatar_component_clause,[],[f54150]) ).
fof(f54152,plain,
( spl1150_37
| spl1150_38 ),
inference(avatar_split_clause,[],[f51632,f54150,f54147]) ).
fof(f54153,plain,
( ~ r3_lattices(k11_group_4(sK35),sK38,sK39)
| spl1150_37 ),
inference(avatar_component_clause,[],[f54147]) ).
fof(f54154,plain,
( ~ m1_group_6(sK38,sK35,sK39)
| spl1150_38 ),
inference(avatar_component_clause,[],[f54150]) ).
fof(f54155,plain,
( ~ spl1150_37
| ~ spl1150_38 ),
inference(avatar_split_clause,[],[f51631,f54150,f54147]) ).
fof(f54308,plain,
! [X0,X1] :
( ~ m1_group_2(X0,X1)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| m1_group_6(X0,sK35,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(resolution,[],[f44470,f43999]) ).
fof(f54309,plain,
! [X0,X1] :
( ~ m1_group_2(X0,X1)
| ~ v3_group_1(sK35)
| m1_group_6(X0,sK35,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54308,f44001]) ).
fof(f54310,plain,
! [X0,X1] :
( ~ m1_group_2(X0,X1)
| m1_group_6(X0,sK35,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54309,f44000]) ).
fof(f54311,plain,
! [X0,X1] :
( m1_group_6(X0,sK35,X1)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54310,f43998]) ).
fof(f54312,plain,
( ~ m1_group_2(sK38,sK39)
| ~ m1_group_2(sK39,sK35)
| spl1150_38 ),
inference(resolution,[],[f54311,f54154]) ).
fof(f54313,plain,
( ~ m1_group_2(sK38,sK39)
| spl1150_38 ),
inference(forward_subsumption_resolution,[],[f54312,f51633]) ).
fof(f54314,plain,
! [X0,X1] :
( ~ r3_lattices(k11_group_4(sK35),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f53052,f43999]) ).
fof(f54315,plain,
! [X0,X1] :
( ~ r3_lattices(k11_group_4(sK35),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| ~ v3_group_1(sK35)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54314,f44001]) ).
fof(f54316,plain,
! [X0,X1] :
( ~ r3_lattices(k11_group_4(sK35),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54315,f44000]) ).
fof(f54317,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| ~ r3_lattices(k11_group_4(sK35),X0,X1) ),
inference(forward_subsumption_resolution,[],[f54316,f43998]) ).
fof(f54335,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK35,X1)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(resolution,[],[f44469,f43999]) ).
fof(f54336,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK35,X1)
| ~ v3_group_1(sK35)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54335,f44001]) ).
fof(f54337,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK35,X1)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54336,f44000]) ).
fof(f54338,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK35,X1)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK35) ),
inference(forward_subsumption_resolution,[],[f54337,f43998]) ).
fof(f54346,plain,
( v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| u1_struct_0(k11_group_4(sK35)) = k1_group_3(sK35)
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f44093,f43999]) ).
fof(f54347,plain,
( ~ v3_group_1(sK35)
| u1_struct_0(k11_group_4(sK35)) = k1_group_3(sK35)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54346,f44001]) ).
fof(f54348,plain,
( u1_struct_0(k11_group_4(sK35)) = k1_group_3(sK35)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54347,f44000]) ).
fof(f54349,plain,
u1_struct_0(k11_group_4(sK35)) = k1_group_3(sK35),
inference(forward_subsumption_resolution,[],[f54348,f43998]) ).
fof(f54351,plain,
m1_subset_1(sK39,k1_group_3(sK35)),
inference(superposition,[],[f44005,f54349]) ).
fof(f54409,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| l1_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f44055,f44000]) ).
fof(f54410,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| l1_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54409,f44001]) ).
fof(f54411,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54410,f43998]) ).
fof(f54412,plain,
l1_group_1(sK38),
inference(resolution,[],[f54411,f51634]) ).
fof(f54413,plain,
l1_group_1(sK39),
inference(resolution,[],[f54411,f51633]) ).
fof(f54414,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f44058,f43999]) ).
fof(f54415,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| ~ v3_group_1(sK35)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54414,f44001]) ).
fof(f54416,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK35)
| ~ m1_group_2(X0,sK35)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54415,f44000]) ).
fof(f54417,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK35)
| ~ m1_group_2(X1,sK35)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f54416,f43998]) ).
fof(f54418,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(sK38),u1_struct_0(X0))
| ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0) ),
inference(resolution,[],[f54417,f51634]) ).
fof(f54426,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(sK38,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ m1_group_2(sK38,sK35)
| ~ r3_lattices(k11_group_4(sK35),sK38,X0) ),
inference(resolution,[],[f54418,f54317]) ).
fof(f54428,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(sK38,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(sK38,sK35)
| ~ r3_lattices(k11_group_4(sK35),sK38,X0) ),
inference(duplicate_literal_removal,[],[f54426]) ).
fof(f54429,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(sK38,sK35)
| ~ r3_lattices(k11_group_4(sK35),sK38,X0) ),
inference(forward_subsumption_resolution,[],[f54428,f44004]) ).
fof(f54430,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ r3_lattices(k11_group_4(sK35),sK38,X0) ),
inference(forward_subsumption_resolution,[],[f54429,f51634]) ).
fof(f54431,plain,
! [X0] :
( ~ r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_group_2(X0,sK35)
| m1_group_2(sK38,X0)
| ~ m1_subset_1(X0,k1_group_3(sK35)) ),
inference(forward_demodulation,[],[f54430,f54349]) ).
fof(f54433,plain,
( ~ m1_group_2(sK39,sK35)
| m1_group_2(sK38,sK39)
| ~ m1_subset_1(sK39,k1_group_3(sK35))
| ~ spl1150_37 ),
inference(resolution,[],[f54431,f54148]) ).
fof(f54435,plain,
( m1_group_2(sK38,sK39)
| ~ m1_subset_1(sK39,k1_group_3(sK35))
| ~ spl1150_37 ),
inference(forward_subsumption_resolution,[],[f54433,f51633]) ).
fof(f54436,plain,
( ~ m1_subset_1(sK39,k1_group_3(sK35))
| ~ spl1150_37
| spl1150_38 ),
inference(forward_subsumption_resolution,[],[f54435,f54313]) ).
fof(f54437,plain,
( $false
| ~ spl1150_37
| spl1150_38 ),
inference(forward_subsumption_resolution,[],[f54436,f54351]) ).
fof(f54438,plain,
( ~ spl1150_37
| spl1150_38 ),
inference(avatar_contradiction_clause,[],[f54437]) ).
fof(f54440,plain,
( m1_group_2(sK38,sK39)
| ~ m1_group_2(sK39,sK35)
| ~ spl1150_38 ),
inference(resolution,[],[f54151,f54338]) ).
fof(f54441,plain,
( m1_group_2(sK38,sK39)
| ~ spl1150_38 ),
inference(forward_subsumption_resolution,[],[f54440,f51633]) ).
fof(f54457,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| v3_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f44056,f44000]) ).
fof(f54458,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v3_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54457,f44001]) ).
fof(f54459,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54458,f43998]) ).
fof(f54461,plain,
v3_group_1(sK39),
inference(resolution,[],[f54459,f51633]) ).
fof(f54498,definition,
( spl1150_58
<=> v3_struct_0(sK39) ),
introduced(definition,[new_symbols(definition,[spl1150_58])],[avatar_definition]) ).
fof(f54499,plain,
( v3_struct_0(sK39)
| ~ spl1150_58 ),
inference(avatar_component_clause,[],[f54498]) ).
fof(f54516,plain,
( $false
| ~ spl1150_58 ),
inference(unit_resulting_resolution,[],[f44057,f43998,f44000,f44001,f51633,f54499]) ).
fof(f54518,plain,
~ spl1150_58,
inference(avatar_contradiction_clause,[],[f54516]) ).
fof(f54543,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| v4_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f44065,f43999]) ).
fof(f54544,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| ~ v3_group_1(sK35)
| v4_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54543,f44001]) ).
fof(f54545,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v4_group_1(X0)
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f54544,f44000]) ).
fof(f54546,plain,
! [X0] :
( ~ m1_group_2(X0,sK35)
| v4_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54545,f43998]) ).
fof(f54548,plain,
v4_group_1(sK39),
inference(resolution,[],[f54546,f51633]) ).
fof(f54660,plain,
! [X0] :
( ~ m1_group_2(X0,sK39)
| v3_struct_0(sK39)
| ~ v3_group_1(sK39)
| u1_struct_0(X0) = k7_group_2(sK39,X0)
| ~ l1_group_1(sK39) ),
inference(resolution,[],[f54548,f45607]) ).
fof(f54673,plain,
! [X0] :
( ~ m1_group_2(X0,sK39)
| v3_struct_0(sK39)
| u1_struct_0(X0) = k7_group_2(sK39,X0)
| ~ l1_group_1(sK39) ),
inference(forward_subsumption_resolution,[],[f54660,f54461]) ).
fof(f54687,plain,
! [X0] :
( ~ m1_group_2(X0,sK39)
| v3_struct_0(sK39)
| u1_struct_0(X0) = k7_group_2(sK39,X0) ),
inference(forward_subsumption_resolution,[],[f54673,f54413]) ).
fof(f54717,definition,
( spl1150_82
<=> ! [X0] :
( ~ m1_group_2(X0,sK39)
| u1_struct_0(X0) = k7_group_2(sK39,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1150_82])],[avatar_definition]) ).
fof(f54718,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK39)
| u1_struct_0(X0) = k7_group_2(sK39,X0) )
| ~ spl1150_82 ),
inference(avatar_component_clause,[],[f54717]) ).
fof(f54719,plain,
( spl1150_58
| spl1150_82 ),
inference(avatar_split_clause,[],[f54687,f54717,f54498]) ).
fof(f54757,plain,
( u1_struct_0(sK38) = k7_group_2(sK39,sK38)
| ~ spl1150_38
| ~ spl1150_82 ),
inference(resolution,[],[f54718,f54441]) ).
fof(f54931,plain,
! [X0] :
( v3_struct_0(sK39)
| ~ v3_group_1(sK39)
| m1_subset_1(k7_group_2(sK39,X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ l1_group_1(sK39)
| ~ m1_group_2(X0,sK39) ),
inference(resolution,[],[f45593,f54548]) ).
fof(f54932,plain,
! [X0] :
( v3_struct_0(sK39)
| m1_subset_1(k7_group_2(sK39,X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ l1_group_1(sK39)
| ~ m1_group_2(X0,sK39) ),
inference(forward_subsumption_resolution,[],[f54931,f54461]) ).
fof(f54935,plain,
! [X0] :
( v3_struct_0(sK39)
| m1_subset_1(k7_group_2(sK39,X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ m1_group_2(X0,sK39) ),
inference(forward_subsumption_resolution,[],[f54932,f54413]) ).
fof(f54939,definition,
( spl1150_119
<=> ! [X0] :
( m1_subset_1(k7_group_2(sK39,X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ m1_group_2(X0,sK39) ) ),
introduced(definition,[new_symbols(definition,[spl1150_119])],[avatar_definition]) ).
fof(f54940,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK39)
| m1_subset_1(k7_group_2(sK39,X0),k1_zfmisc_1(u1_struct_0(sK39))) )
| ~ spl1150_119 ),
inference(avatar_component_clause,[],[f54939]) ).
fof(f54941,plain,
( spl1150_119
| spl1150_58 ),
inference(avatar_split_clause,[],[f54935,f54498,f54939]) ).
fof(f55074,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f48030,f47165]) ).
fof(f55076,plain,
u1_struct_0(sK39) = k2_pre_topc(sK39),
inference(resolution,[],[f55074,f54413]) ).
fof(f55077,plain,
u1_struct_0(sK38) = k2_pre_topc(sK38),
inference(resolution,[],[f55074,f54412]) ).
fof(f55104,plain,
! [X0,X1] :
( ~ v4_group_1(X1)
| r3_lattices(k11_group_4(X1),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(X1)))
| ~ m1_subset_1(sK38,u1_struct_0(k11_group_4(X1)))
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(sK38,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(X1) ),
inference(superposition,[],[f53050,f55077]) ).
fof(f55354,plain,
( m1_subset_1(k7_group_2(sK39,sK38),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ spl1150_38
| ~ spl1150_119 ),
inference(resolution,[],[f54940,f54441]) ).
fof(f55357,plain,
( m1_subset_1(k7_group_2(sK39,sK38),k1_zfmisc_1(k2_pre_topc(sK39)))
| ~ spl1150_38
| ~ spl1150_119 ),
inference(forward_demodulation,[],[f55354,f55076]) ).
fof(f55359,plain,
( m1_subset_1(u1_struct_0(sK38),k1_zfmisc_1(k2_pre_topc(sK39)))
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(forward_demodulation,[],[f55357,f54757]) ).
fof(f55361,plain,
( m1_subset_1(k2_pre_topc(sK38),k1_zfmisc_1(k2_pre_topc(sK39)))
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(forward_demodulation,[],[f55359,f55077]) ).
fof(f55411,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_subset_1(sK38,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ m1_group_2(sK38,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(sK35) ),
inference(resolution,[],[f55104,f43999]) ).
fof(f55416,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ m1_group_2(sK38,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f55411,f44004]) ).
fof(f55419,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| v3_struct_0(sK35)
| ~ v3_group_1(sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f55416,f51634]) ).
fof(f55422,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ v3_group_1(sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f55419,f44001]) ).
fof(f55425,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0))
| ~ l1_group_1(sK35) ),
inference(forward_subsumption_resolution,[],[f55422,f44000]) ).
fof(f55428,plain,
! [X0] :
( r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK35)))
| ~ m1_group_2(X0,sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f55425,f43998]) ).
fof(f55436,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_group_3(sK35))
| r3_lattices(k11_group_4(sK35),sK38,X0)
| ~ m1_group_2(X0,sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(X0)) ),
inference(forward_demodulation,[],[f55428,f54349]) ).
fof(f55438,plain,
( r3_lattices(k11_group_4(sK35),sK38,sK39)
| ~ m1_group_2(sK39,sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(sK39)) ),
inference(resolution,[],[f55436,f54351]) ).
fof(f55439,plain,
( ~ m1_group_2(sK39,sK35)
| ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(sK39))
| spl1150_37 ),
inference(forward_subsumption_resolution,[],[f55438,f54153]) ).
fof(f55440,plain,
( ~ r1_tarski(k2_pre_topc(sK38),u1_struct_0(sK39))
| spl1150_37 ),
inference(forward_subsumption_resolution,[],[f55439,f51633]) ).
fof(f55441,plain,
( ~ r1_tarski(k2_pre_topc(sK38),k2_pre_topc(sK39))
| spl1150_37 ),
inference(forward_demodulation,[],[f55440,f55076]) ).
fof(f55750,plain,
( r1_tarski(k2_pre_topc(sK38),k2_pre_topc(sK39))
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(resolution,[],[f44499,f55361]) ).
fof(f55752,plain,
( $false
| spl1150_37
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(forward_subsumption_resolution,[],[f55750,f55441]) ).
fof(f55753,plain,
( spl1150_37
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(avatar_contradiction_clause,[],[f55752]) ).
cnf(s24,plain,
( spl1150_37
| spl1150_38 ),
inference(sat_conversion,[],[f54152]) ).
cnf(s25,plain,
( ~ spl1150_37
| ~ spl1150_38 ),
inference(sat_conversion,[],[f54155]) ).
cnf(s40,plain,
( ~ spl1150_37
| spl1150_38 ),
inference(sat_conversion,[],[f54438]) ).
cnf(s49,plain,
~ spl1150_58,
inference(sat_conversion,[],[f54518]) ).
cnf(s70,plain,
( spl1150_58
| spl1150_82 ),
inference(sat_conversion,[],[f54719]) ).
cnf(s95,plain,
( spl1150_58
| spl1150_119 ),
inference(sat_conversion,[],[f54941]) ).
cnf(s137,plain,
( spl1150_37
| ~ spl1150_38
| ~ spl1150_82
| ~ spl1150_119 ),
inference(sat_conversion,[],[f55753]) ).
cnf(s172,plain,
spl1150_119,
inference(rat,[],[s95,s49]) ).
cnf(s183,plain,
spl1150_82,
inference(rat,[],[s70,s49]) ).
cnf(s209,plain,
spl1150_37,
inference(rat,[],[s24,s137,s183,s172]) ).
cnf(s210,plain,
spl1150_38,
inference(rat,[],[s40,s209]) ).
cnf(s211,plain,
$false,
inference(rat,[],[s25,s210,s209]) ).
fof(f55759,plain,
$false,
inference(avatar_sat_refutation,[],[s211]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP648+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.43 % Computer : n001.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sun Sep 27 10:33:08 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.49 Running first-order theorem proving
% 0.21/0.49 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
% 21.21/6.64 % (3360778)Detected formulas, will run a generic FOF schedule.
% 21.21/6.64 % (3360787)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=2576818477:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 21.21/6.64 % (3360793)dis-21_1_sil=8000:lcm=predicate:random_seed=2199428901:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 21.21/6.64 % (3360789)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=55672326:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 21.21/6.64 % (3360791)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2491070369:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 21.21/6.64 % (3360788)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=1515389894:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 21.21/6.64 % (3360790)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3223319980:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 21.21/6.64 % (3360792)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2836184275:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 21.21/6.64 % (3360793)Instruction limit reached!
% 21.21/6.64 % (3360793)------------------------------
% 21.21/6.64 % (3360793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.21/6.64 % (3360793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/6.64 % (3360793)CaDiCaL version: 2.1.3
% 21.21/6.64 % (3360793)Termination reason: Instruction limit
% 21.21/6.64 % (3360793)Termination phase: SInE selection
% 21.21/6.64 % (3360793)Time elapsed: 0.133 s
% 21.21/6.64 % (3360793)Peak memory usage: 139 MB
% 21.21/6.64 % (3360793)Instructions burned: 129 (million)
% 21.21/6.64 % (3360790)Instruction limit reached!
% 21.21/6.64 % (3360790)------------------------------
% 21.21/6.64 % (3360790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.21/6.64 % (3360790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/6.64 % (3360790)CaDiCaL version: 2.1.3
% 21.21/6.64 % (3360790)Termination reason: Instruction limit
% 21.21/6.64 % (3360790)Termination phase: SInE selection
% 21.21/6.64 % (3360790)Time elapsed: 0.115 s
% 21.21/6.64 % (3360790)Peak memory usage: 139 MB
% 21.21/6.64 % (3360790)Instructions burned: 109 (million)
% 21.21/6.64 % (3360791)Instruction limit reached!
% 21.21/6.64 % (3360791)------------------------------
% 21.21/6.64 % (3360791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.21/6.64 % (3360791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/6.64 % (3360791)CaDiCaL version: 2.1.3
% 21.21/6.64 % (3360791)Termination reason: Instruction limit
% 21.21/6.64 % (3360791)Termination phase: SInE selection
% 21.21/6.64 % (3360791)Time elapsed: 0.126 s
% 21.21/6.64 % (3360791)Peak memory usage: 139 MB
% 21.21/6.64 % (3360791)Instructions burned: 119 (million)
% 21.21/6.64 % (3360792)Instruction limit reached!
% 21.21/6.64 % (3360792)------------------------------
% 21.21/6.64 % (3360792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.21/6.64 % (3360792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/6.64 % (3360792)CaDiCaL version: 2.1.3
% 21.21/6.64 % (3360792)Termination reason: Instruction limit
% 21.21/6.64 % (3360792)Termination phase: Property scanning
% 21.21/6.64 % (3360792)Time elapsed: 0.119 s
% 21.21/6.64 % (3360792)Peak memory usage: 139 MB
% 21.21/6.64 % (3360792)Instructions burned: 139 (million)
% 21.21/6.64 % (3360801)lrs+10_1_sil=8000:sp=occurrence:random_seed=539967910:i=285:sd=3:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/285Mi)
% 21.21/6.64 % (3360802)lrs+10_1_sil=32000:urr=on:br=off:random_seed=20366369:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/157Mi)
% 21.21/6.64 % (3360803)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1317257281:i=325:sd=1:ss=axioms:sgt=32_2967 on theBenchmark for (2967ds/325Mi)
% 21.21/6.64 % (3360804)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=4282934555:s2a=on:i=248:s2at=1.23:gtg=position_2967 on theBenchmark for (2967ds/248Mi)
% 21.21/6.64 % (3360802)Instruction limit reached!
% 28.85/7.69 % (3360802)------------------------------
% 28.85/7.69 % (3360802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360802)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360802)Termination reason: Instruction limit
% 28.85/7.69 % (3360802)Termination phase: Property scanning
% 28.85/7.69 % (3360802)Time elapsed: 0.137 s
% 28.85/7.69 % (3360802)Peak memory usage: 139 MB
% 28.85/7.69 % (3360802)Instructions burned: 157 (million)
% 28.85/7.69 % (3360804)Instruction limit reached!
% 28.85/7.69 % (3360804)------------------------------
% 28.85/7.69 % (3360804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360804)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360804)Termination reason: Instruction limit
% 28.85/7.69 % (3360804)Termination phase: Property scanning
% 28.85/7.69 % (3360804)Time elapsed: 0.211 s
% 28.85/7.69 % (3360804)Peak memory usage: 139 MB
% 28.85/7.69 % (3360804)Instructions burned: 249 (million)
% 28.85/7.69 % (3360801)Instruction limit reached!
% 28.85/7.69 % (3360801)------------------------------
% 28.85/7.69 % (3360801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360801)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360801)Termination reason: Instruction limit
% 28.85/7.69 % (3360801)Termination phase: Preprocessing 3
% 28.85/7.69 % (3360801)Time elapsed: 0.360 s
% 28.85/7.69 % (3360801)Peak memory usage: 142 MB
% 28.85/7.69 % (3360801)Instructions burned: 285 (million)
% 28.85/7.69 % (3360803)Instruction limit reached!
% 28.85/7.69 % (3360803)------------------------------
% 28.85/7.69 % (3360803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360803)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360803)Termination reason: Instruction limit
% 28.85/7.69 % (3360803)Termination phase: Saturation
% 28.85/7.69 % (3360803)Time elapsed: 0.379 s
% 28.85/7.69 % (3360803)Peak memory usage: 145 MB
% 28.85/7.69 % (3360803)Instructions burned: 325 (million)
% 28.85/7.69 % (3360809)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1080666514:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2963 on theBenchmark for (2963ds/294Mi)
% 28.85/7.69 % (3360810)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4204232355:i=2350_2962 on theBenchmark for (2962ds/2350Mi)
% 28.85/7.69 % (3360811)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3438625284:cts=off:i=113:fsr=off:ss=included:sgt=4_2962 on theBenchmark for (2962ds/113Mi)
% 28.85/7.69 % (3360814)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2062415750:i=127:av=off:fsr=off:sup=off_2960 on theBenchmark for (2960ds/127Mi)
% 28.85/7.69 % (3360811)Instruction limit reached!
% 28.85/7.69 % (3360811)------------------------------
% 28.85/7.69 % (3360811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360811)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360811)Termination reason: Instruction limit
% 28.85/7.69 % (3360811)Termination phase: SInE selection
% 28.85/7.69 % (3360811)Time elapsed: 0.086 s
% 28.85/7.69 % (3360811)Peak memory usage: 139 MB
% 28.85/7.69 % (3360811)Instructions burned: 114 (million)
% 28.85/7.69 % (3360809)Instruction limit reached!
% 28.85/7.69 % (3360809)------------------------------
% 28.85/7.69 % (3360809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360809)CaDiCaL version: 2.1.3
% 28.85/7.69 % (3360809)Termination reason: Instruction limit
% 28.85/7.69 % (3360809)Termination phase: SInE selection
% 28.85/7.69 % (3360809)Time elapsed: 0.181 s
% 28.85/7.69 % (3360809)Peak memory usage: 139 MB
% 28.85/7.69 % (3360809)Instructions burned: 295 (million)
% 28.85/7.69 % (3360814)Instruction limit reached!
% 28.85/7.69 % (3360814)------------------------------
% 28.85/7.69 % (3360814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/7.69 % (3360814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/7.69 % (3360814)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360814)Termination reason: Instruction limit
% 18.52/8.27 % (3360814)Termination phase: Preprocessing 1
% 18.52/8.27 % (3360814)Time elapsed: 0.097 s
% 18.52/8.27 % (3360814)Peak memory usage: 140 MB
% 18.52/8.27 % (3360814)Instructions burned: 128 (million)
% 18.52/8.27 % (3360820)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1280610294:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2958 on theBenchmark for (2958ds/114Mi)
% 18.52/8.27 % (3360822)lrs+10_1_sil=8000:sp=occurrence:random_seed=3442311559:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2958 on theBenchmark for (2958ds/907Mi)
% 18.52/8.27 % (3360820)Instruction limit reached!
% 18.52/8.27 % (3360820)------------------------------
% 18.52/8.27 % (3360820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360820)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360820)Termination reason: Instruction limit
% 18.52/8.27 % (3360820)Termination phase: Property scanning
% 18.52/8.27 % (3360820)Time elapsed: 0.052 s
% 18.52/8.27 % (3360820)Peak memory usage: 139 MB
% 18.52/8.27 % (3360820)Instructions burned: 115 (million)
% 18.52/8.27 % (3360845)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1344783009:i=437:sd=1:aac=none:ss=included_2958 on theBenchmark for (2958ds/437Mi)
% 18.52/8.27 % (3360862)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3062116764:i=5202:ss=axioms:sgt=16_2956 on theBenchmark for (2956ds/5202Mi)
% 18.52/8.27 % (3360845)Instruction limit reached!
% 18.52/8.27 % (3360845)------------------------------
% 18.52/8.27 % (3360845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360845)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360845)Termination reason: Instruction limit
% 18.52/8.27 % (3360845)Termination phase: Saturation
% 18.52/8.27 % (3360845)Time elapsed: 0.312 s
% 18.52/8.27 % (3360845)Peak memory usage: 146 MB
% 18.52/8.27 % (3360845)Instructions burned: 438 (million)
% 18.52/8.27 % (3360865)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2258060419:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2953 on theBenchmark for (2953ds/134Mi)
% 18.52/8.27 % (3360822)Instruction limit reached!
% 18.52/8.27 % (3360822)------------------------------
% 18.52/8.27 % (3360822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360822)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360822)Termination reason: Instruction limit
% 18.52/8.27 % (3360822)Termination phase: Property scanning
% 18.52/8.27 % (3360822)Time elapsed: 0.611 s
% 18.52/8.27 % (3360822)Peak memory usage: 158 MB
% 18.52/8.27 % (3360822)Instructions burned: 910 (million)
% 18.52/8.27 % (3360865)Instruction limit reached!
% 18.52/8.27 % (3360865)------------------------------
% 18.52/8.27 % (3360865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360865)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360865)Termination reason: Instruction limit
% 18.52/8.27 % (3360865)Termination phase: SInE selection
% 18.52/8.27 % (3360865)Time elapsed: 0.100 s
% 18.52/8.27 % (3360865)Peak memory usage: 139 MB
% 18.52/8.27 % (3360865)Instructions burned: 134 (million)
% 18.52/8.27 % (3360919)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3468945086:st=8:i=592:sd=3:ep=RST:ss=axioms_2951 on theBenchmark for (2951ds/592Mi)
% 18.52/8.27 % (3360924)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3427385504:st=3:i=13193:sd=3:ss=axioms_2950 on theBenchmark for (2950ds/13193Mi)
% 18.52/8.27 % (3360919)Instruction limit reached!
% 18.52/8.27 % (3360919)------------------------------
% 18.52/8.27 % (3360919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360919)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360919)Termination reason: Instruction limit
% 18.52/8.27 % (3360919)Termination phase: Preprocessing 2
% 18.52/8.27 % (3360919)Time elapsed: 0.467 s
% 18.52/8.27 % (3360919)Peak memory usage: 150 MB
% 18.52/8.27 % (3360919)Instructions burned: 593 (million)
% 18.52/8.27 % (3360810)Instruction limit reached!
% 18.52/8.27 % (3360810)------------------------------
% 18.52/8.27 % (3360810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360810)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360810)Termination reason: Instruction limit
% 18.52/8.27 % (3360810)Termination phase: Property scanning
% 18.52/8.27 % (3360810)Time elapsed: 1.605 s
% 18.52/8.27 % (3360810)Peak memory usage: 241 MB
% 18.52/8.27 % (3360810)Instructions burned: 2350 (million)
% 18.52/8.27 % (3360985)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=856606215:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2944 on theBenchmark for (2944ds/125Mi)
% 18.52/8.27 % (3360986)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1442638130:i=134:gtgl=5:slsql=off:gtg=exists_sym_2944 on theBenchmark for (2944ds/134Mi)
% 18.52/8.27 % (3360985)Instruction limit reached!
% 18.52/8.27 % (3360985)------------------------------
% 18.52/8.27 % (3360985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360985)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360985)Termination reason: Instruction limit
% 18.52/8.27 % (3360985)Termination phase: Property scanning
% 18.52/8.27 % (3360985)Time elapsed: 0.058 s
% 18.52/8.27 % (3360985)Peak memory usage: 139 MB
% 18.52/8.27 % (3360985)Instructions burned: 125 (million)
% 18.52/8.27 % (3360986)Instruction limit reached!
% 18.52/8.27 % (3360986)------------------------------
% 18.52/8.27 % (3360986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360986)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360986)Termination reason: Instruction limit
% 18.52/8.27 % (3360986)Termination phase: Property scanning
% 18.52/8.27 % (3360986)Time elapsed: 0.062 s
% 18.52/8.27 % (3360986)Peak memory usage: 139 MB
% 18.52/8.27 % (3360986)Instructions burned: 136 (million)
% 18.52/8.27 % (3360989)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3186389758:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/141Mi)
% 18.52/8.27 % (3360990)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1525488924:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2941 on theBenchmark for (2941ds/431Mi)
% 18.52/8.27 % (3360989)Instruction limit reached!
% 18.52/8.27 % (3360989)------------------------------
% 18.52/8.27 % (3360989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360989)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360989)Termination reason: Instruction limit
% 18.52/8.27 % (3360989)Termination phase: SInE selection
% 18.52/8.27 % (3360989)Time elapsed: 0.106 s
% 18.52/8.27 % (3360989)Peak memory usage: 139 MB
% 18.52/8.27 % (3360989)Instructions burned: 141 (million)
% 18.52/8.27 % (3360993)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=731924850:i=6060:aac=none:ins=25_2939 on theBenchmark for (2939ds/6060Mi)
% 18.52/8.27 % (3360990)Instruction limit reached!
% 18.52/8.27 % (3360990)------------------------------
% 18.52/8.27 % (3360990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360990)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360990)Termination reason: Instruction limit
% 18.52/8.27 % (3360990)Termination phase: Saturation
% 18.52/8.27 % (3360990)Time elapsed: 0.319 s
% 18.52/8.27 % (3360990)Peak memory usage: 146 MB
% 18.52/8.27 % (3360990)Instructions burned: 432 (million)
% 18.52/8.27 % (3360995)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=2995486498:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2936 on theBenchmark for (2936ds/150Mi)
% 18.52/8.27 % (3360995)Instruction limit reached!
% 18.52/8.27 % (3360995)------------------------------
% 18.52/8.27 % (3360995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/8.27 % (3360995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/8.27 % (3360995)CaDiCaL version: 2.1.3
% 18.52/8.27 % (3360995)Termination reason: Instruction limit
% 18.52/8.27 % (3360995)Termination phase: SInE selection
% 18.52/8.27 % (3360995)Time elapsed: 0.114 s
% 18.52/8.27 % (3360995)Peak memory usage: 139 MB
% 18.52/8.27 % (3360995)Instructions burned: 150 (million)
% 18.52/8.27 % (3360997)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3612032243:i=14155:bd=all_2933 on theBenchmark for (2933ds/14155Mi)
% 18.52/8.27 % (3360788)First to succeed.
% 18.52/8.27 % (3360788)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3360778"
% 18.52/8.27 % (3360788)Refutation found. Thanks to Tanya!
% 18.52/8.27 % SZS status Theorem for theBenchmark
% 18.52/8.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/8.52 % (3360788)------------------------------
% 0.22/8.52 % (3360788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.22/8.52 % (3360788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/8.52 % (3360788)CaDiCaL version: 2.1.3
% 0.22/8.52 % (3360788)Termination reason: Refutation
% 0.22/8.52 % (3360788)Time elapsed: 3.678 s
% 0.22/8.52 % (3360788)Peak memory usage: 294 MB
% 0.22/8.52 % (3360788)Instructions burned: 5449 (million)
% 0.22/8.52 % (3360788)------------------------------
% 0.22/8.52 % (3360788)------------------------------
% 0.22/8.52 % (3360778)Success in time 7.189 s
% 0.22/8.52 % Vampire exiting
%------------------------------------------------------------------------------