%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT360+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 : n020.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:47:19 AM UTC 2026
% Result : Theorem 110.08s 22.87s
% Output : Refutation 130.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 77
% Syntax : Number of formulae : 446 ( 47 unt; 61 def)
% Number of atoms : 1723 ( 25 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 2143 ( 866 ~; 952 |; 237 &)
% ( 69 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 88 ( 86 usr; 54 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 220 ( 0 sgn 214 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
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(f588,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f676,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f17598,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f36132,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f36134,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f55626,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& l2_altcat_1(X0) )
=> ( v3_yellow21(X0)
<=> ( v2_yellow21(X0)
& ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_yellow21) ).
fof(f55677,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f55678,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f55711,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f55712,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f55713,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_waybel34) ).
fof(f55715,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f55717,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel34) ).
fof(f55718,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
inference(negated_conjecture,[status(cth)],[f55717]) ).
fof(f55835,plain,
? [X0] :
( u1_struct_0(k4_waybel34(X0)) != u1_struct_0(k5_waybel34(X0))
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55718]) ).
fof(f55847,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f588]) ).
fof(f55849,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55713]) ).
fof(f55850,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f55849]) ).
fof(f55851,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55711]) ).
fof(f55856,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f55677]) ).
fof(f55858,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55715]) ).
fof(f55859,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f55858]) ).
fof(f55860,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55712]) ).
fof(f55865,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f55678]) ).
fof(f55869,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f676]) ).
fof(f55870,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f55869]) ).
fof(f56103,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f56239,plain,
! [X0] :
( ( v3_yellow21(X0)
<=> ( v2_yellow21(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f55626]) ).
fof(f56240,plain,
! [X0] :
( ( v3_yellow21(X0)
<=> ( v2_yellow21(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f56239]) ).
fof(f56323,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f56544,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17598]) ).
fof(f58238,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f36134]) ).
fof(f58239,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f36132]) ).
fof(f58548,definition,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f58549,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(definition_folding,[],[f55851,f58548]) ).
fof(f58555,definition,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| ~ sP5(X0) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f58556,plain,
! [X0] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(definition_folding,[],[f55860,f58555]) ).
fof(f58579,definition,
! [X0] :
( sP20(X0)
<=> ( v2_yellow21(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) ) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f58580,definition,
! [X0] :
( ( v3_yellow21(X0)
<=> sP20(X0) )
| ~ sP21(X0) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f58581,plain,
! [X0] :
( sP21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(definition_folding,[],[f56240,f58580,f58579]) ).
fof(f58668,plain,
( u1_struct_0(k4_waybel34(sK75)) != u1_struct_0(k5_waybel34(sK75))
& ~ v2_setfam_1(sK75) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75]),skolemize(X0,sK75)],[f55835]) ).
fof(f58679,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(nnf_transformation,[],[f55850]) ).
fof(f58680,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f58679]) ).
fof(f58681,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f58548]) ).
fof(f58700,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(nnf_transformation,[],[f55859]) ).
fof(f58701,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f58700]) ).
fof(f58702,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| ~ sP5(X0) ),
inference(nnf_transformation,[],[f58555]) ).
fof(f58911,plain,
! [X0] :
( ( ( v3_yellow21(X0)
| ~ sP20(X0) )
& ( sP20(X0)
| ~ v3_yellow21(X0) ) )
| ~ sP21(X0) ),
inference(nnf_transformation,[],[f58580]) ).
fof(f58912,plain,
! [X0] :
( ( sP20(X0)
| ~ v2_yellow21(X0)
| ? [X1] :
( ( ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ( v2_yellow21(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) )
| ~ sP20(X0) ) ),
inference(nnf_transformation,[],[f58579]) ).
fof(f58913,plain,
! [X0] :
( ( sP20(X0)
| ~ v2_yellow21(X0)
| ? [X1] :
( ( ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ( v2_yellow21(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) )
| ~ sP20(X0) ) ),
inference(flattening,[],[f58912]) ).
fof(f58914,plain,
! [X0] :
( ( sP20(X0)
| ~ v2_yellow21(X0)
| ? [X1] :
( ( ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ( v2_yellow21(X0)
& ! [X2] :
( ( v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v1_lattice3(X2)
& v2_lattice3(X2)
& v3_lattice3(X2)
& l1_orders_2(X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ sP20(X0) ) ),
inference(rectify,[],[f58913]) ).
fof(f58915,plain,
! [X0] :
( ( sP20(X0)
| ~ v2_yellow21(X0)
| ( ( ~ v2_orders_2(sK219(X0))
| ~ v3_orders_2(sK219(X0))
| ~ v4_orders_2(sK219(X0))
| ~ v1_lattice3(sK219(X0))
| ~ v2_lattice3(sK219(X0))
| ~ v3_lattice3(sK219(X0))
| ~ l1_orders_2(sK219(X0)) )
& m1_subset_1(sK219(X0),u1_struct_0(X0)) ) )
& ( ( v2_yellow21(X0)
& ! [X2] :
( ( v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v1_lattice3(X2)
& v2_lattice3(X2)
& v3_lattice3(X2)
& l1_orders_2(X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ sP20(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK219]),skolemize(X1,sK219(X0))],[f58914]) ).
fof(f58944,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(f58945,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,[],[f58944]) ).
fof(f58946,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f56323]) ).
fof(f58947,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f58946]) ).
fof(f58948,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK243(X0,X1),X1)
& r2_hidden(sK243(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK243]),skolemize(X2,sK243(X0,X1))],[f58947]) ).
fof(f59088,plain,
! [X0] :
( ( ( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) )
& ( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f56544]) ).
fof(f59776,plain,
~ v2_setfam_1(sK75),
inference(cnf_transformation,[],[f58668]) ).
fof(f59777,plain,
u1_struct_0(k4_waybel34(sK75)) != u1_struct_0(k5_waybel34(sK75)),
inference(cnf_transformation,[],[f58668]) ).
fof(f59800,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55847]) ).
fof(f59807,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58680]) ).
fof(f59809,plain,
! [X0,X1] :
( ~ v2_lattice3(X1)
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| v1_orders_2(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58680]) ).
fof(f59810,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58680]) ).
fof(f59811,plain,
! [X0] :
( v3_yellow21(k4_waybel34(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f58681]) ).
fof(f59824,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58549]) ).
fof(f59861,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55856]) ).
fof(f59863,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55856]) ).
fof(f59864,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55856]) ).
fof(f59866,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55856]) ).
fof(f59867,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55856]) ).
fof(f59873,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58701]) ).
fof(f59875,plain,
! [X0,X1] :
( ~ v2_lattice3(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| v1_orders_2(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58701]) ).
fof(f59876,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58701]) ).
fof(f59877,plain,
! [X0] :
( v3_yellow21(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f58702]) ).
fof(f59890,plain,
! [X0] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f58556]) ).
fof(f59927,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55865]) ).
fof(f59929,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55865]) ).
fof(f59930,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55865]) ).
fof(f59932,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55865]) ).
fof(f59933,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f55865]) ).
fof(f59938,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f55870]) ).
fof(f60375,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f56103]) ).
fof(f60744,plain,
! [X0] :
( ~ sP21(X0)
| ~ v3_yellow21(X0)
| sP20(X0) ),
inference(cnf_transformation,[],[f58911]) ).
fof(f60746,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| l1_orders_2(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60747,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_lattice3(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60748,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v2_lattice3(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60749,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v1_lattice3(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60750,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v4_orders_2(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60751,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_orders_2(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60752,plain,
! [X2,X0] :
( ~ sP20(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v2_orders_2(X2) ),
inference(cnf_transformation,[],[f58915]) ).
fof(f60756,plain,
! [X0] :
( sP21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f58581]) ).
fof(f60910,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f58945]) ).
fof(f60913,plain,
! [X0,X1] :
( r2_hidden(sK243(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f58948]) ).
fof(f60914,plain,
! [X0,X1] :
( ~ r2_hidden(sK243(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f58948]) ).
fof(f61358,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f59088]) ).
fof(f63858,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f58238]) ).
fof(f63860,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f58239]) ).
fof(f65572,definition,
sF774 = k4_waybel34(sK75),
introduced(definition,[new_symbols(definition,[sF774])],[function_definition]) ).
fof(f65573,plain,
k4_waybel34(sK75) = sF774,
inference(reorient_equations,[],[f65572]) ).
fof(f65574,definition,
sF775 = u1_struct_0(sF774),
introduced(definition,[new_symbols(definition,[sF775])],[function_definition]) ).
fof(f65575,plain,
u1_struct_0(sF774) = sF775,
inference(reorient_equations,[],[f65574]) ).
fof(f65576,definition,
sF776 = k5_waybel34(sK75),
introduced(definition,[new_symbols(definition,[sF776])],[function_definition]) ).
fof(f65577,plain,
k5_waybel34(sK75) = sF776,
inference(reorient_equations,[],[f65576]) ).
fof(f65578,definition,
sF777 = u1_struct_0(sF776),
introduced(definition,[new_symbols(definition,[sF777])],[function_definition]) ).
fof(f65579,plain,
u1_struct_0(sF776) = sF777,
inference(reorient_equations,[],[f65578]) ).
fof(f65580,plain,
sF775 != sF777,
inference(definition_folding,[],[f59777,f65579,f65577,f65575,f65573]) ).
fof(f65613,plain,
( ~ v3_struct_0(sF774)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59867,f65573]) ).
fof(f65615,definition,
( spl778_4
<=> v1_xboole_0(sK75) ),
introduced(definition,[new_symbols(definition,[spl778_4])],[avatar_definition]) ).
fof(f65619,definition,
( spl778_5
<=> v3_struct_0(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_5])],[avatar_definition]) ).
fof(f65622,plain,
( spl778_4
| ~ spl778_5 ),
inference(avatar_split_clause,[],[f65613,f65619,f65615]) ).
fof(f65623,plain,
( ~ v3_struct_0(sF776)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59933,f65577]) ).
fof(f65625,definition,
( spl778_6
<=> v3_struct_0(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_6])],[avatar_definition]) ).
fof(f65628,plain,
( spl778_4
| ~ spl778_6 ),
inference(avatar_split_clause,[],[f65623,f65625,f65615]) ).
fof(f65629,plain,
~ v1_xboole_0(sK75),
inference(resolution,[],[f59800,f59776]) ).
fof(f65630,plain,
~ spl778_4,
inference(avatar_split_clause,[],[f65629,f65615]) ).
fof(f65643,plain,
( v2_altcat_1(sF774)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59866,f65573]) ).
fof(f65645,definition,
( spl778_9
<=> v2_altcat_1(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_9])],[avatar_definition]) ).
fof(f65648,plain,
( spl778_4
| spl778_9 ),
inference(avatar_split_clause,[],[f65643,f65645,f65615]) ).
fof(f65649,plain,
( v2_altcat_1(sF776)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59932,f65577]) ).
fof(f65651,definition,
( spl778_10
<=> v2_altcat_1(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_10])],[avatar_definition]) ).
fof(f65654,plain,
( spl778_4
| spl778_10 ),
inference(avatar_split_clause,[],[f65649,f65651,f65615]) ).
fof(f65655,plain,
( l2_altcat_1(sF774)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59861,f65573]) ).
fof(f65657,definition,
( spl778_11
<=> l2_altcat_1(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_11])],[avatar_definition]) ).
fof(f65660,plain,
( spl778_4
| spl778_11 ),
inference(avatar_split_clause,[],[f65655,f65657,f65615]) ).
fof(f65661,plain,
( l2_altcat_1(sF776)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59927,f65577]) ).
fof(f65663,definition,
( spl778_12
<=> l2_altcat_1(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_12])],[avatar_definition]) ).
fof(f65666,plain,
( spl778_4
| spl778_12 ),
inference(avatar_split_clause,[],[f65661,f65663,f65615]) ).
fof(f65667,plain,
( v11_altcat_1(sF774)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59864,f65573]) ).
fof(f65669,definition,
( spl778_13
<=> v11_altcat_1(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_13])],[avatar_definition]) ).
fof(f65672,plain,
( spl778_4
| spl778_13 ),
inference(avatar_split_clause,[],[f65667,f65669,f65615]) ).
fof(f65673,plain,
( v11_altcat_1(sF776)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59930,f65577]) ).
fof(f65675,definition,
( spl778_14
<=> v11_altcat_1(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_14])],[avatar_definition]) ).
fof(f65678,plain,
( spl778_4
| spl778_14 ),
inference(avatar_split_clause,[],[f65673,f65675,f65615]) ).
fof(f65679,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(superposition,[],[f59873,f65577]) ).
fof(f65680,plain,
! [X0] :
( ~ m1_subset_1(X0,sF777)
| r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(forward_demodulation,[],[f65679,f65579]) ).
fof(f65682,definition,
( spl778_15
<=> v2_setfam_1(sK75) ),
introduced(definition,[new_symbols(definition,[spl778_15])],[avatar_definition]) ).
fof(f65686,definition,
( spl778_16
<=> ! [X0] :
( ~ m1_subset_1(X0,sF777)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK75) ) ),
introduced(definition,[new_symbols(definition,[spl778_16])],[avatar_definition]) ).
fof(f65687,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK75)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_16 ),
inference(avatar_component_clause,[],[f65686]) ).
fof(f65688,plain,
( spl778_15
| spl778_16 ),
inference(avatar_split_clause,[],[f65680,f65686,f65682]) ).
fof(f65691,plain,
~ spl778_15,
inference(avatar_split_clause,[],[f59776,f65682]) ).
fof(f65761,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(superposition,[],[f59807,f65573]) ).
fof(f65762,plain,
! [X0] :
( ~ m1_subset_1(X0,sF775)
| r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(forward_demodulation,[],[f65761,f65575]) ).
fof(f65764,definition,
( spl778_33
<=> ! [X0] :
( ~ m1_subset_1(X0,sF775)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK75) ) ),
introduced(definition,[new_symbols(definition,[spl778_33])],[avatar_definition]) ).
fof(f65765,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK75)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_33 ),
inference(avatar_component_clause,[],[f65764]) ).
fof(f65766,plain,
( spl778_15
| spl778_33 ),
inference(avatar_split_clause,[],[f65762,f65764,f65682]) ).
fof(f65779,plain,
( v12_altcat_1(sF774)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59863,f65573]) ).
fof(f65781,definition,
( spl778_36
<=> v12_altcat_1(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_36])],[avatar_definition]) ).
fof(f65784,plain,
( spl778_4
| spl778_36 ),
inference(avatar_split_clause,[],[f65779,f65781,f65615]) ).
fof(f65785,plain,
( v12_altcat_1(sF776)
| v1_xboole_0(sK75) ),
inference(superposition,[],[f59929,f65577]) ).
fof(f65787,definition,
( spl778_37
<=> v12_altcat_1(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_37])],[avatar_definition]) ).
fof(f65790,plain,
( spl778_4
| spl778_37 ),
inference(avatar_split_clause,[],[f65785,f65787,f65615]) ).
fof(f65791,plain,
( ~ v1_xboole_0(sF775)
| v3_struct_0(sF774)
| ~ l1_struct_0(sF774) ),
inference(superposition,[],[f61358,f65575]) ).
fof(f65792,plain,
( ~ v1_xboole_0(sF777)
| v3_struct_0(sF776)
| ~ l1_struct_0(sF776) ),
inference(superposition,[],[f61358,f65579]) ).
fof(f65794,definition,
( spl778_38
<=> l1_struct_0(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_38])],[avatar_definition]) ).
fof(f65796,plain,
( ~ l1_struct_0(sF776)
| spl778_38 ),
inference(avatar_component_clause,[],[f65794]) ).
fof(f65798,definition,
( spl778_39
<=> v1_xboole_0(sF777) ),
introduced(definition,[new_symbols(definition,[spl778_39])],[avatar_definition]) ).
fof(f65800,plain,
( ~ v1_xboole_0(sF777)
| spl778_39 ),
inference(avatar_component_clause,[],[f65798]) ).
fof(f65801,plain,
( ~ spl778_38
| spl778_6
| ~ spl778_39 ),
inference(avatar_split_clause,[],[f65792,f65798,f65625,f65794]) ).
fof(f65803,definition,
( spl778_40
<=> l1_struct_0(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_40])],[avatar_definition]) ).
fof(f65805,plain,
( ~ l1_struct_0(sF774)
| spl778_40 ),
inference(avatar_component_clause,[],[f65803]) ).
fof(f65807,definition,
( spl778_41
<=> v1_xboole_0(sF775) ),
introduced(definition,[new_symbols(definition,[spl778_41])],[avatar_definition]) ).
fof(f65810,plain,
( ~ spl778_40
| spl778_5
| ~ spl778_41 ),
inference(avatar_split_clause,[],[f65791,f65807,f65619,f65803]) ).
fof(f65848,plain,
( ~ l1_altcat_1(sF774)
| spl778_40 ),
inference(resolution,[],[f63860,f65805]) ).
fof(f65849,plain,
( ~ l1_altcat_1(sF776)
| spl778_38 ),
inference(resolution,[],[f65796,f63860]) ).
fof(f65873,plain,
( ~ l2_altcat_1(sF776)
| spl778_38 ),
inference(resolution,[],[f65849,f63858]) ).
fof(f65874,plain,
( ~ spl778_12
| spl778_38 ),
inference(avatar_split_clause,[],[f65873,f65794,f65663]) ).
fof(f65895,definition,
( spl778_46
<=> sP0(sK75) ),
introduced(definition,[new_symbols(definition,[spl778_46])],[avatar_definition]) ).
fof(f65897,plain,
( ~ sP0(sK75)
| spl778_46 ),
inference(avatar_component_clause,[],[f65895]) ).
fof(f65903,plain,
( v2_setfam_1(sK75)
| spl778_46 ),
inference(resolution,[],[f65897,f59824]) ).
fof(f65904,plain,
( spl778_15
| spl778_46 ),
inference(avatar_split_clause,[],[f65903,f65895,f65682]) ).
fof(f65907,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF776))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(superposition,[],[f59876,f65577]) ).
fof(f65909,plain,
! [X0] :
( m1_subset_1(X0,sF777)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(forward_demodulation,[],[f65907,f65579]) ).
fof(f65911,definition,
( spl778_48
<=> ! [X0] :
( m1_subset_1(X0,sF777)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl778_48])],[avatar_definition]) ).
fof(f65912,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF777)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl778_48 ),
inference(avatar_component_clause,[],[f65911]) ).
fof(f65913,plain,
( spl778_15
| spl778_48 ),
inference(avatar_split_clause,[],[f65909,f65911,f65682]) ).
fof(f65914,plain,
( ! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF777)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_33
| ~ spl778_48 ),
inference(resolution,[],[f65912,f65765]) ).
fof(f65921,plain,
( ! [X0] :
( m1_subset_1(X0,sF777)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_33
| ~ spl778_48 ),
inference(duplicate_literal_removal,[],[f65914]) ).
fof(f65934,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF774))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(superposition,[],[f59810,f65573]) ).
fof(f65936,plain,
! [X0] :
( m1_subset_1(X0,sF775)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK75) ),
inference(forward_demodulation,[],[f65934,f65575]) ).
fof(f65938,definition,
( spl778_51
<=> ! [X0] :
( m1_subset_1(X0,sF775)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl778_51])],[avatar_definition]) ).
fof(f65939,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK75)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF775)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl778_51 ),
inference(avatar_component_clause,[],[f65938]) ).
fof(f65940,plain,
( spl778_15
| spl778_51 ),
inference(avatar_split_clause,[],[f65936,f65938,f65682]) ).
fof(f65942,plain,
( ! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF775)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_16
| ~ spl778_51 ),
inference(resolution,[],[f65939,f65687]) ).
fof(f65947,plain,
( ! [X0] :
( m1_subset_1(X0,sF775)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_16
| ~ spl778_51 ),
inference(duplicate_literal_removal,[],[f65942]) ).
fof(f65977,plain,
( v3_yellow21(sF774)
| ~ sP0(sK75) ),
inference(superposition,[],[f59811,f65573]) ).
fof(f65979,definition,
( spl778_56
<=> v3_yellow21(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_56])],[avatar_definition]) ).
fof(f65981,plain,
( v3_yellow21(sF774)
| ~ spl778_56 ),
inference(avatar_component_clause,[],[f65979]) ).
fof(f65982,plain,
( ~ spl778_46
| spl778_56 ),
inference(avatar_split_clause,[],[f65977,f65979,f65895]) ).
fof(f66001,plain,
( ~ l2_altcat_1(sF774)
| spl778_40 ),
inference(resolution,[],[f65848,f63858]) ).
fof(f66002,plain,
( ~ spl778_11
| spl778_40 ),
inference(avatar_split_clause,[],[f66001,f65803,f65657]) ).
fof(f66074,definition,
( spl778_65
<=> sP5(sK75) ),
introduced(definition,[new_symbols(definition,[spl778_65])],[avatar_definition]) ).
fof(f66076,plain,
( ~ sP5(sK75)
| spl778_65 ),
inference(avatar_component_clause,[],[f66074]) ).
fof(f66082,plain,
( v2_setfam_1(sK75)
| spl778_65 ),
inference(resolution,[],[f66076,f59890]) ).
fof(f66083,plain,
( spl778_15
| spl778_65 ),
inference(avatar_split_clause,[],[f66082,f66074,f65682]) ).
fof(f66141,plain,
( v3_yellow21(sF776)
| ~ sP5(sK75) ),
inference(superposition,[],[f59877,f65577]) ).
fof(f66143,definition,
( spl778_72
<=> v3_yellow21(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_72])],[avatar_definition]) ).
fof(f66145,plain,
( v3_yellow21(sF776)
| ~ spl778_72 ),
inference(avatar_component_clause,[],[f66143]) ).
fof(f66146,plain,
( ~ spl778_65
| spl778_72 ),
inference(avatar_split_clause,[],[f66141,f66143,f66074]) ).
fof(f68909,plain,
! [X0] :
( ~ v3_yellow21(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0)
| v3_struct_0(X0)
| sP20(X0) ),
inference(resolution,[],[f60756,f60744]) ).
fof(f69446,plain,
( ~ v2_altcat_1(sF774)
| ~ v11_altcat_1(sF774)
| ~ v12_altcat_1(sF774)
| ~ l2_altcat_1(sF774)
| v3_struct_0(sF774)
| sP20(sF774)
| ~ spl778_56 ),
inference(resolution,[],[f68909,f65981]) ).
fof(f69447,plain,
( ~ v2_altcat_1(sF776)
| ~ v11_altcat_1(sF776)
| ~ v12_altcat_1(sF776)
| ~ l2_altcat_1(sF776)
| v3_struct_0(sF776)
| sP20(sF776)
| ~ spl778_72 ),
inference(resolution,[],[f68909,f66145]) ).
fof(f69449,definition,
( spl778_248
<=> sP20(sF776) ),
introduced(definition,[new_symbols(definition,[spl778_248])],[avatar_definition]) ).
fof(f69451,plain,
( sP20(sF776)
| ~ spl778_248 ),
inference(avatar_component_clause,[],[f69449]) ).
fof(f69452,plain,
( spl778_248
| spl778_6
| ~ spl778_12
| ~ spl778_37
| ~ spl778_14
| ~ spl778_10
| ~ spl778_72 ),
inference(avatar_split_clause,[],[f69447,f66143,f65651,f65675,f65787,f65663,f65625,f69449]) ).
fof(f69454,definition,
( spl778_249
<=> sP20(sF774) ),
introduced(definition,[new_symbols(definition,[spl778_249])],[avatar_definition]) ).
fof(f69456,plain,
( sP20(sF774)
| ~ spl778_249 ),
inference(avatar_component_clause,[],[f69454]) ).
fof(f69457,plain,
( spl778_249
| spl778_5
| ~ spl778_11
| ~ spl778_36
| ~ spl778_13
| ~ spl778_9
| ~ spl778_56 ),
inference(avatar_split_clause,[],[f69446,f65979,f65645,f65669,f65781,f65657,f65619,f69454]) ).
fof(f69458,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| l1_orders_2(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60746]) ).
fof(f69459,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v3_lattice3(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60747]) ).
fof(f69460,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v2_lattice3(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60748]) ).
fof(f69461,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v1_lattice3(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60749]) ).
fof(f69462,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v4_orders_2(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60750]) ).
fof(f69463,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v3_orders_2(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60751]) ).
fof(f69464,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF774))
| v2_orders_2(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69456,f60752]) ).
fof(f69465,plain,
( ! [X0] :
( v2_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69464,f65575]) ).
fof(f69466,plain,
( ! [X0] :
( v3_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69463,f65575]) ).
fof(f69467,plain,
( ! [X0] :
( v4_orders_2(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69462,f65575]) ).
fof(f69468,plain,
( ! [X0] :
( v1_lattice3(X0)
| ~ m1_subset_1(X0,sF775) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69461,f65575]) ).
fof(f69469,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF775)
| v2_lattice3(X0) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69460,f65575]) ).
fof(f69470,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF775)
| v3_lattice3(X0) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69459,f65575]) ).
fof(f69471,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF775)
| l1_orders_2(X0) )
| ~ spl778_249 ),
inference(forward_demodulation,[],[f69458,f65575]) ).
fof(f69479,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| l1_orders_2(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60746]) ).
fof(f69480,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v3_lattice3(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60747]) ).
fof(f69481,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v2_lattice3(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60748]) ).
fof(f69482,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v1_lattice3(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60749]) ).
fof(f69483,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v4_orders_2(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60750]) ).
fof(f69484,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v3_orders_2(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60751]) ).
fof(f69485,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF776))
| v2_orders_2(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69451,f60752]) ).
fof(f69486,plain,
( ! [X0] :
( v2_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69485,f65579]) ).
fof(f69487,plain,
( ! [X0] :
( v3_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69484,f65579]) ).
fof(f69488,plain,
( ! [X0] :
( v4_orders_2(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69483,f65579]) ).
fof(f69489,plain,
( ! [X0] :
( v1_lattice3(X0)
| ~ m1_subset_1(X0,sF777) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69482,f65579]) ).
fof(f69490,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF777)
| v2_lattice3(X0) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69481,f65579]) ).
fof(f69491,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF777)
| v3_lattice3(X0) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69480,f65579]) ).
fof(f69492,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF777)
| l1_orders_2(X0) )
| ~ spl778_248 ),
inference(forward_demodulation,[],[f69479,f65579]) ).
fof(f69495,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF777)
| l1_orders_2(X0) )
| ~ spl778_248 ),
inference(resolution,[],[f69492,f60375]) ).
fof(f69503,plain,
( ! [X0] :
( r1_tarski(sF777,X0)
| l1_orders_2(sK243(sF777,X0)) )
| ~ spl778_248 ),
inference(resolution,[],[f69495,f60913]) ).
fof(f69517,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF775)
| l1_orders_2(X0) )
| ~ spl778_249 ),
inference(resolution,[],[f69471,f60375]) ).
fof(f69525,plain,
( ! [X0] :
( ~ r1_tarski(X0,sF777)
| l1_orders_2(sK243(sF777,X0))
| sF777 = X0 )
| ~ spl778_248 ),
inference(resolution,[],[f69503,f60910]) ).
fof(f69560,plain,
( ! [X0] :
( r1_tarski(sF775,X0)
| l1_orders_2(sK243(sF775,X0)) )
| ~ spl778_249 ),
inference(resolution,[],[f69517,f60913]) ).
fof(f72204,definition,
( spl778_444
<=> l1_orders_2(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_444])],[avatar_definition]) ).
fof(f72208,definition,
( spl778_445
<=> sF775 = sF777 ),
introduced(definition,[new_symbols(definition,[spl778_445])],[avatar_definition]) ).
fof(f72212,definition,
( spl778_446
<=> l1_orders_2(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_446])],[avatar_definition]) ).
fof(f72372,plain,
( l1_orders_2(sK243(sF775,sF777))
| l1_orders_2(sK243(sF777,sF775))
| sF775 = sF777
| ~ spl778_248
| ~ spl778_249 ),
inference(resolution,[],[f69560,f69525]) ).
fof(f72373,plain,
( spl778_445
| spl778_446
| spl778_444
| ~ spl778_248
| ~ spl778_249 ),
inference(avatar_split_clause,[],[f72372,f69454,f69449,f72204,f72212,f72208]) ).
fof(f72425,definition,
( spl778_465
<=> ! [X0] :
( ~ m1_subset_1(sK243(sF775,sF777),u1_struct_0(k4_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl778_465])],[avatar_definition]) ).
fof(f72426,plain,
( ! [X0] :
( ~ m1_subset_1(sK243(sF775,sF777),u1_struct_0(k4_waybel34(X0)))
| v2_setfam_1(X0) )
| ~ spl778_465 ),
inference(avatar_component_clause,[],[f72425]) ).
fof(f72428,definition,
( spl778_466
<=> r2_hidden(sK243(sF775,sF777),sF775) ),
introduced(definition,[new_symbols(definition,[spl778_466])],[avatar_definition]) ).
fof(f72430,plain,
( ~ r2_hidden(sK243(sF775,sF777),sF775)
| spl778_466 ),
inference(avatar_component_clause,[],[f72428]) ).
fof(f72432,definition,
( spl778_467
<=> v1_lattice3(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_467])],[avatar_definition]) ).
fof(f72434,plain,
( ~ v1_lattice3(sK243(sF775,sF777))
| spl778_467 ),
inference(avatar_component_clause,[],[f72432]) ).
fof(f72436,definition,
( spl778_468
<=> v4_orders_2(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_468])],[avatar_definition]) ).
fof(f72438,plain,
( ~ v4_orders_2(sK243(sF775,sF777))
| spl778_468 ),
inference(avatar_component_clause,[],[f72436]) ).
fof(f72440,definition,
( spl778_469
<=> v3_orders_2(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_469])],[avatar_definition]) ).
fof(f72442,plain,
( ~ v3_orders_2(sK243(sF775,sF777))
| spl778_469 ),
inference(avatar_component_clause,[],[f72440]) ).
fof(f72444,definition,
( spl778_470
<=> v2_orders_2(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_470])],[avatar_definition]) ).
fof(f72446,plain,
( ~ v2_orders_2(sK243(sF775,sF777))
| spl778_470 ),
inference(avatar_component_clause,[],[f72444]) ).
fof(f72453,definition,
( spl778_472
<=> m1_subset_1(sK243(sF775,sF777),sF777) ),
introduced(definition,[new_symbols(definition,[spl778_472])],[avatar_definition]) ).
fof(f72454,plain,
( m1_subset_1(sK243(sF775,sF777),sF777)
| ~ spl778_472 ),
inference(avatar_component_clause,[],[f72453]) ).
fof(f72455,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF777)
| spl778_472 ),
inference(avatar_component_clause,[],[f72453]) ).
fof(f72457,definition,
( spl778_473
<=> v1_orders_2(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_473])],[avatar_definition]) ).
fof(f72461,definition,
( spl778_474
<=> v3_lattice3(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_474])],[avatar_definition]) ).
fof(f72469,definition,
( spl778_476
<=> v2_lattice3(sK243(sF775,sF777)) ),
introduced(definition,[new_symbols(definition,[spl778_476])],[avatar_definition]) ).
fof(f72470,plain,
( v2_lattice3(sK243(sF775,sF777))
| ~ spl778_476 ),
inference(avatar_component_clause,[],[f72469]) ).
fof(f72647,plain,
~ spl778_445,
inference(avatar_split_clause,[],[f65580,f72208]) ).
fof(f72683,definition,
( spl778_497
<=> r2_hidden(sK243(sF777,sF775),sF775) ),
introduced(definition,[new_symbols(definition,[spl778_497])],[avatar_definition]) ).
fof(f72684,plain,
( r2_hidden(sK243(sF777,sF775),sF775)
| ~ spl778_497 ),
inference(avatar_component_clause,[],[f72683]) ).
fof(f72685,plain,
( ~ r2_hidden(sK243(sF777,sF775),sF775)
| spl778_497 ),
inference(avatar_component_clause,[],[f72683]) ).
fof(f72687,definition,
( spl778_498
<=> v1_lattice3(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_498])],[avatar_definition]) ).
fof(f72689,plain,
( ~ v1_lattice3(sK243(sF777,sF775))
| spl778_498 ),
inference(avatar_component_clause,[],[f72687]) ).
fof(f72691,definition,
( spl778_499
<=> v4_orders_2(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_499])],[avatar_definition]) ).
fof(f72693,plain,
( ~ v4_orders_2(sK243(sF777,sF775))
| spl778_499 ),
inference(avatar_component_clause,[],[f72691]) ).
fof(f72695,definition,
( spl778_500
<=> v3_orders_2(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_500])],[avatar_definition]) ).
fof(f72697,plain,
( ~ v3_orders_2(sK243(sF777,sF775))
| spl778_500 ),
inference(avatar_component_clause,[],[f72695]) ).
fof(f72699,definition,
( spl778_501
<=> v2_orders_2(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_501])],[avatar_definition]) ).
fof(f72701,plain,
( ~ v2_orders_2(sK243(sF777,sF775))
| spl778_501 ),
inference(avatar_component_clause,[],[f72699]) ).
fof(f72704,definition,
( spl778_502
<=> ! [X0] :
( ~ m1_subset_1(sK243(sF777,sF775),u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl778_502])],[avatar_definition]) ).
fof(f72705,plain,
( ! [X0] :
( ~ m1_subset_1(sK243(sF777,sF775),u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) )
| ~ spl778_502 ),
inference(avatar_component_clause,[],[f72704]) ).
fof(f72708,definition,
( spl778_503
<=> m1_subset_1(sK243(sF777,sF775),sF777) ),
introduced(definition,[new_symbols(definition,[spl778_503])],[avatar_definition]) ).
fof(f72709,plain,
( m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_503 ),
inference(avatar_component_clause,[],[f72708]) ).
fof(f72710,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| spl778_503 ),
inference(avatar_component_clause,[],[f72708]) ).
fof(f72712,definition,
( spl778_504
<=> v1_orders_2(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_504])],[avatar_definition]) ).
fof(f72716,definition,
( spl778_505
<=> v3_lattice3(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_505])],[avatar_definition]) ).
fof(f72724,definition,
( spl778_507
<=> v2_lattice3(sK243(sF777,sF775)) ),
introduced(definition,[new_symbols(definition,[spl778_507])],[avatar_definition]) ).
fof(f72725,plain,
( v2_lattice3(sK243(sF777,sF775))
| ~ spl778_507 ),
inference(avatar_component_clause,[],[f72724]) ).
fof(f72876,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(sK243(X1,X0),X0)
| r1_tarski(X1,X0) ),
inference(resolution,[],[f59938,f60914]) ).
fof(f72922,plain,
( ! [X0] :
( ~ m1_subset_1(sK243(X0,sF777),sF777)
| r1_tarski(X0,sF777) )
| spl778_39 ),
inference(resolution,[],[f72876,f65800]) ).
fof(f72932,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_249
| spl778_468 ),
inference(resolution,[],[f72438,f69467]) ).
fof(f72936,plain,
( ~ r2_hidden(sK243(sF775,sF777),sF775)
| ~ spl778_249
| spl778_468 ),
inference(resolution,[],[f72932,f60375]) ).
fof(f72937,plain,
( ~ spl778_466
| ~ spl778_249
| spl778_468 ),
inference(avatar_split_clause,[],[f72936,f72436,f69454,f72428]) ).
fof(f72938,plain,
( r1_tarski(sF775,sF777)
| spl778_466 ),
inference(resolution,[],[f72430,f60913]) ).
fof(f72947,definition,
( spl778_527
<=> r1_tarski(sF777,sF775) ),
introduced(definition,[new_symbols(definition,[spl778_527])],[avatar_definition]) ).
fof(f72949,plain,
( ~ r1_tarski(sF777,sF775)
| spl778_527 ),
inference(avatar_component_clause,[],[f72947]) ).
fof(f72965,plain,
( ~ v2_lattice3(sK243(sF775,sF777))
| ~ v1_lattice3(sK243(sF775,sF777))
| ~ v4_orders_2(sK243(sF775,sF777))
| ~ v3_orders_2(sK243(sF775,sF777))
| ~ v2_orders_2(sK243(sF775,sF777))
| ~ l1_orders_2(sK243(sF775,sF777))
| ~ v3_lattice3(sK243(sF775,sF777))
| ~ v1_orders_2(sK243(sF775,sF777))
| ~ m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_33
| ~ spl778_48
| spl778_472 ),
inference(resolution,[],[f72455,f65921]) ).
fof(f72968,definition,
( spl778_528
<=> m1_subset_1(sK243(sF775,sF777),sF775) ),
introduced(definition,[new_symbols(definition,[spl778_528])],[avatar_definition]) ).
fof(f72969,plain,
( m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_528 ),
inference(avatar_component_clause,[],[f72968]) ).
fof(f72970,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| spl778_528 ),
inference(avatar_component_clause,[],[f72968]) ).
fof(f72971,plain,
( ~ spl778_528
| ~ spl778_473
| ~ spl778_474
| ~ spl778_444
| ~ spl778_470
| ~ spl778_469
| ~ spl778_468
| ~ spl778_467
| ~ spl778_476
| ~ spl778_33
| ~ spl778_48
| spl778_472 ),
inference(avatar_split_clause,[],[f72965,f72453,f65911,f65764,f72469,f72432,f72436,f72440,f72444,f72204,f72461,f72457,f72968]) ).
fof(f73101,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_249
| spl778_467 ),
inference(resolution,[],[f72434,f69468]) ).
fof(f73103,plain,
( ~ spl778_528
| ~ spl778_249
| spl778_467 ),
inference(avatar_split_clause,[],[f73101,f72432,f69454,f72968]) ).
fof(f73105,plain,
( ~ r2_hidden(sK243(sF775,sF777),sF775)
| spl778_528 ),
inference(resolution,[],[f72970,f60375]) ).
fof(f73106,plain,
( ~ spl778_466
| spl778_528 ),
inference(avatar_split_clause,[],[f73105,f72968,f72428]) ).
fof(f73111,plain,
( ~ r1_tarski(sF777,sF775)
| sF775 = sF777
| spl778_466 ),
inference(resolution,[],[f72938,f60910]) ).
fof(f73112,plain,
( spl778_445
| ~ spl778_527
| spl778_466 ),
inference(avatar_split_clause,[],[f73111,f72428,f72947,f72208]) ).
fof(f73170,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_248
| spl778_499 ),
inference(resolution,[],[f72693,f69488]) ).
fof(f73171,plain,
( ~ spl778_503
| ~ spl778_248
| spl778_499 ),
inference(avatar_split_clause,[],[f73170,f72691,f69449,f72708]) ).
fof(f73175,plain,
( v1_xboole_0(sF775)
| ~ m1_subset_1(sK243(sF777,sF775),sF775)
| spl778_497 ),
inference(resolution,[],[f72685,f59938]) ).
fof(f73178,plain,
( ~ r2_hidden(sK243(sF777,sF775),sF777)
| spl778_503 ),
inference(resolution,[],[f72710,f60375]) ).
fof(f73221,plain,
( r1_tarski(sF777,sF775)
| spl778_503 ),
inference(resolution,[],[f73178,f60913]) ).
fof(f73224,plain,
( spl778_527
| spl778_503 ),
inference(avatar_split_clause,[],[f73221,f72708,f72947]) ).
fof(f73226,definition,
( spl778_539
<=> m1_subset_1(sK243(sF777,sF775),sF775) ),
introduced(definition,[new_symbols(definition,[spl778_539])],[avatar_definition]) ).
fof(f73228,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF775)
| spl778_539 ),
inference(avatar_component_clause,[],[f73226]) ).
fof(f73229,plain,
( ~ spl778_539
| spl778_41
| spl778_497 ),
inference(avatar_split_clause,[],[f73175,f72683,f65807,f73226]) ).
fof(f73248,plain,
( v2_lattice3(sK243(sF777,sF775))
| ~ spl778_248
| ~ spl778_503 ),
inference(resolution,[],[f72709,f69490]) ).
fof(f73249,plain,
( v3_lattice3(sK243(sF777,sF775))
| ~ spl778_248
| ~ spl778_503 ),
inference(resolution,[],[f72709,f69491]) ).
fof(f73251,plain,
( spl778_505
| ~ spl778_248
| ~ spl778_503 ),
inference(avatar_split_clause,[],[f73249,f72708,f69449,f72716]) ).
fof(f73252,plain,
( spl778_507
| ~ spl778_248
| ~ spl778_503 ),
inference(avatar_split_clause,[],[f73248,f72708,f69449,f72724]) ).
fof(f73289,definition,
( spl778_542
<=> r1_tarski(sF775,sF777) ),
introduced(definition,[new_symbols(definition,[spl778_542])],[avatar_definition]) ).
fof(f73290,plain,
( r1_tarski(sF775,sF777)
| ~ spl778_542 ),
inference(avatar_component_clause,[],[f73289]) ).
fof(f73291,plain,
( ~ r1_tarski(sF775,sF777)
| spl778_542 ),
inference(avatar_component_clause,[],[f73289]) ).
fof(f73385,plain,
( v2_lattice3(sK243(sF775,sF777))
| ~ spl778_249
| ~ spl778_528 ),
inference(resolution,[],[f72969,f69469]) ).
fof(f73386,plain,
( v3_lattice3(sK243(sF775,sF777))
| ~ spl778_249
| ~ spl778_528 ),
inference(resolution,[],[f72969,f69470]) ).
fof(f73388,plain,
( spl778_474
| ~ spl778_249
| ~ spl778_528 ),
inference(avatar_split_clause,[],[f73386,f72968,f69454,f72461]) ).
fof(f73389,plain,
( spl778_476
| ~ spl778_249
| ~ spl778_528 ),
inference(avatar_split_clause,[],[f73385,f72968,f69454,f72469]) ).
fof(f73412,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_249
| spl778_470 ),
inference(resolution,[],[f72446,f69465]) ).
fof(f73415,plain,
( ~ spl778_528
| ~ spl778_249
| spl778_470 ),
inference(avatar_split_clause,[],[f73412,f72444,f69454,f72968]) ).
fof(f73416,plain,
( l1_orders_2(sK243(sF775,sF777))
| ~ spl778_249
| spl778_542 ),
inference(resolution,[],[f73291,f69560]) ).
fof(f73446,plain,
( ! [X0] :
( ~ m1_subset_1(sK243(sF775,sF777),u1_struct_0(k4_waybel34(X0)))
| ~ v2_orders_2(sK243(sF775,sF777))
| ~ v3_orders_2(sK243(sF775,sF777))
| ~ v4_orders_2(sK243(sF775,sF777))
| ~ v1_lattice3(sK243(sF775,sF777))
| v1_orders_2(sK243(sF775,sF777))
| ~ l1_orders_2(sK243(sF775,sF777))
| v2_setfam_1(X0) )
| ~ spl778_476 ),
inference(resolution,[],[f72470,f59809]) ).
fof(f73449,plain,
( ~ spl778_444
| spl778_473
| ~ spl778_467
| ~ spl778_468
| ~ spl778_469
| ~ spl778_470
| spl778_465
| ~ spl778_476 ),
inference(avatar_split_clause,[],[f73446,f72469,f72425,f72444,f72440,f72436,f72432,f72457,f72204]) ).
fof(f73467,plain,
( ! [X0] :
( ~ m1_subset_1(sK243(sF777,sF775),u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(sK243(sF777,sF775))
| ~ v3_orders_2(sK243(sF777,sF775))
| ~ v4_orders_2(sK243(sF777,sF775))
| ~ v1_lattice3(sK243(sF777,sF775))
| v1_orders_2(sK243(sF777,sF775))
| ~ l1_orders_2(sK243(sF777,sF775))
| v2_setfam_1(X0) )
| ~ spl778_507 ),
inference(resolution,[],[f72725,f59875]) ).
fof(f73468,plain,
( ~ spl778_446
| spl778_504
| ~ spl778_498
| ~ spl778_499
| ~ spl778_500
| ~ spl778_501
| spl778_502
| ~ spl778_507 ),
inference(avatar_split_clause,[],[f73467,f72724,f72704,f72699,f72695,f72691,f72687,f72712,f72212]) ).
fof(f73482,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| ~ spl778_249
| spl778_469 ),
inference(resolution,[],[f72442,f69466]) ).
fof(f73484,plain,
( ~ spl778_528
| ~ spl778_249
| spl778_469 ),
inference(avatar_split_clause,[],[f73482,f72440,f69454,f72968]) ).
fof(f73486,plain,
( r1_tarski(sF775,sF777)
| spl778_39
| ~ spl778_472 ),
inference(resolution,[],[f72454,f72922]) ).
fof(f73507,plain,
( spl778_542
| spl778_39
| ~ spl778_472 ),
inference(avatar_split_clause,[],[f73486,f72453,f65798,f73289]) ).
fof(f73520,plain,
( ~ m1_subset_1(sK243(sF775,sF777),u1_struct_0(sF774))
| v2_setfam_1(sK75)
| ~ spl778_465 ),
inference(superposition,[],[f72426,f65573]) ).
fof(f73522,plain,
( ~ m1_subset_1(sK243(sF775,sF777),sF775)
| v2_setfam_1(sK75)
| ~ spl778_465 ),
inference(forward_demodulation,[],[f73520,f65575]) ).
fof(f73524,plain,
( spl778_15
| ~ spl778_528
| ~ spl778_465 ),
inference(avatar_split_clause,[],[f73522,f72425,f72968,f65682]) ).
fof(f73527,plain,
( spl778_444
| ~ spl778_249
| spl778_542 ),
inference(avatar_split_clause,[],[f73416,f73289,f69454,f72204]) ).
fof(f73535,plain,
( ~ r1_tarski(sF777,sF775)
| sF775 = sF777
| ~ spl778_542 ),
inference(resolution,[],[f73290,f60910]) ).
fof(f73536,plain,
( spl778_445
| ~ spl778_527
| ~ spl778_542 ),
inference(avatar_split_clause,[],[f73535,f73289,f72947,f72208]) ).
fof(f73599,plain,
( l1_orders_2(sK243(sF777,sF775))
| ~ spl778_248
| spl778_527 ),
inference(resolution,[],[f72949,f69503]) ).
fof(f73619,plain,
( ~ v2_lattice3(sK243(sF777,sF775))
| ~ v1_lattice3(sK243(sF777,sF775))
| ~ v4_orders_2(sK243(sF777,sF775))
| ~ v3_orders_2(sK243(sF777,sF775))
| ~ v2_orders_2(sK243(sF777,sF775))
| ~ l1_orders_2(sK243(sF777,sF775))
| ~ v3_lattice3(sK243(sF777,sF775))
| ~ v1_orders_2(sK243(sF777,sF775))
| ~ m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_16
| ~ spl778_51
| spl778_539 ),
inference(resolution,[],[f73228,f65947]) ).
fof(f73621,plain,
( ~ spl778_503
| ~ spl778_504
| ~ spl778_505
| ~ spl778_446
| ~ spl778_501
| ~ spl778_500
| ~ spl778_499
| ~ spl778_498
| ~ spl778_507
| ~ spl778_16
| ~ spl778_51
| spl778_539 ),
inference(avatar_split_clause,[],[f73619,f73226,f65938,f65686,f72724,f72687,f72691,f72695,f72699,f72212,f72716,f72712,f72708]) ).
fof(f73623,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_248
| spl778_498 ),
inference(resolution,[],[f72689,f69489]) ).
fof(f73624,plain,
( ~ spl778_503
| ~ spl778_248
| spl778_498 ),
inference(avatar_split_clause,[],[f73623,f72687,f69449,f72708]) ).
fof(f73626,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_248
| spl778_500 ),
inference(resolution,[],[f72697,f69487]) ).
fof(f73627,plain,
( ~ spl778_503
| ~ spl778_248
| spl778_500 ),
inference(avatar_split_clause,[],[f73626,f72695,f69449,f72708]) ).
fof(f73629,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| ~ spl778_248
| spl778_501 ),
inference(resolution,[],[f72701,f69486]) ).
fof(f73636,plain,
( ~ spl778_503
| ~ spl778_248
| spl778_501 ),
inference(avatar_split_clause,[],[f73629,f72699,f69449,f72708]) ).
fof(f73641,plain,
( r1_tarski(sF777,sF775)
| ~ spl778_497 ),
inference(resolution,[],[f72684,f60914]) ).
fof(f73658,plain,
( spl778_527
| ~ spl778_497 ),
inference(avatar_split_clause,[],[f73641,f72683,f72947]) ).
fof(f73672,plain,
( ~ m1_subset_1(sK243(sF777,sF775),u1_struct_0(sF776))
| v2_setfam_1(sK75)
| ~ spl778_502 ),
inference(superposition,[],[f72705,f65577]) ).
fof(f73674,plain,
( ~ m1_subset_1(sK243(sF777,sF775),sF777)
| v2_setfam_1(sK75)
| ~ spl778_502 ),
inference(forward_demodulation,[],[f73672,f65579]) ).
fof(f73679,plain,
( spl778_15
| ~ spl778_503
| ~ spl778_502 ),
inference(avatar_split_clause,[],[f73674,f72704,f72708,f65682]) ).
fof(f73685,plain,
( spl778_446
| ~ spl778_248
| spl778_527 ),
inference(avatar_split_clause,[],[f73599,f72947,f69449,f72212]) ).
cnf(s3,plain,
( spl778_4
| ~ spl778_5 ),
inference(sat_conversion,[],[f65622]) ).
cnf(s4,plain,
( spl778_4
| ~ spl778_6 ),
inference(sat_conversion,[],[f65628]) ).
cnf(s5,plain,
~ spl778_4,
inference(sat_conversion,[],[f65630]) ).
cnf(s8,plain,
( spl778_4
| spl778_9 ),
inference(sat_conversion,[],[f65648]) ).
cnf(s9,plain,
( spl778_4
| spl778_10 ),
inference(sat_conversion,[],[f65654]) ).
cnf(s10,plain,
( spl778_4
| spl778_11 ),
inference(sat_conversion,[],[f65660]) ).
cnf(s11,plain,
( spl778_4
| spl778_12 ),
inference(sat_conversion,[],[f65666]) ).
cnf(s12,plain,
( spl778_4
| spl778_13 ),
inference(sat_conversion,[],[f65672]) ).
cnf(s13,plain,
( spl778_4
| spl778_14 ),
inference(sat_conversion,[],[f65678]) ).
cnf(s14,plain,
( spl778_15
| spl778_16 ),
inference(sat_conversion,[],[f65688]) ).
cnf(s16,plain,
~ spl778_15,
inference(sat_conversion,[],[f65691]) ).
cnf(s19,plain,
( spl778_15
| spl778_33 ),
inference(sat_conversion,[],[f65766]) ).
cnf(s22,plain,
( spl778_4
| spl778_36 ),
inference(sat_conversion,[],[f65784]) ).
cnf(s23,plain,
( spl778_4
| spl778_37 ),
inference(sat_conversion,[],[f65790]) ).
cnf(s24,plain,
( spl778_6
| ~ spl778_38
| ~ spl778_39 ),
inference(sat_conversion,[],[f65801]) ).
cnf(s25,plain,
( spl778_5
| ~ spl778_40
| ~ spl778_41 ),
inference(sat_conversion,[],[f65810]) ).
cnf(s30,plain,
( ~ spl778_12
| spl778_38 ),
inference(sat_conversion,[],[f65874]) ).
cnf(s32,plain,
( spl778_15
| spl778_46 ),
inference(sat_conversion,[],[f65904]) ).
cnf(s33,plain,
( spl778_15
| spl778_48 ),
inference(sat_conversion,[],[f65913]) ).
cnf(s36,plain,
( spl778_15
| spl778_51 ),
inference(sat_conversion,[],[f65940]) ).
cnf(s41,plain,
( ~ spl778_46
| spl778_56 ),
inference(sat_conversion,[],[f65982]) ).
cnf(s43,plain,
( ~ spl778_11
| spl778_40 ),
inference(sat_conversion,[],[f66002]) ).
cnf(s50,plain,
( spl778_15
| spl778_65 ),
inference(sat_conversion,[],[f66083]) ).
cnf(s56,plain,
( ~ spl778_65
| spl778_72 ),
inference(sat_conversion,[],[f66146]) ).
cnf(s268,plain,
( spl778_6
| ~ spl778_10
| ~ spl778_12
| ~ spl778_14
| ~ spl778_37
| ~ spl778_72
| spl778_248 ),
inference(sat_conversion,[],[f69452]) ).
cnf(s269,plain,
( spl778_5
| ~ spl778_9
| ~ spl778_11
| ~ spl778_13
| ~ spl778_36
| ~ spl778_56
| spl778_249 ),
inference(sat_conversion,[],[f69457]) ).
cnf(s660,plain,
( ~ spl778_248
| ~ spl778_249
| spl778_444
| spl778_445
| spl778_446 ),
inference(sat_conversion,[],[f72373]) ).
cnf(s697,plain,
~ spl778_445,
inference(sat_conversion,[],[f72647]) ).
cnf(s752,plain,
( ~ spl778_249
| ~ spl778_466
| spl778_468 ),
inference(sat_conversion,[],[f72937]) ).
cnf(s755,plain,
( ~ spl778_33
| ~ spl778_48
| ~ spl778_444
| ~ spl778_467
| ~ spl778_468
| ~ spl778_469
| ~ spl778_470
| spl778_472
| ~ spl778_473
| ~ spl778_474
| ~ spl778_476
| ~ spl778_528 ),
inference(sat_conversion,[],[f72971]) ).
cnf(s774,plain,
( ~ spl778_249
| spl778_467
| ~ spl778_528 ),
inference(sat_conversion,[],[f73103]) ).
cnf(s775,plain,
( ~ spl778_466
| spl778_528 ),
inference(sat_conversion,[],[f73106]) ).
cnf(s776,plain,
( spl778_445
| spl778_466
| ~ spl778_527 ),
inference(sat_conversion,[],[f73112]) ).
cnf(s800,plain,
( ~ spl778_248
| spl778_499
| ~ spl778_503 ),
inference(sat_conversion,[],[f73171]) ).
cnf(s808,plain,
( spl778_503
| spl778_527 ),
inference(sat_conversion,[],[f73224]) ).
cnf(s809,plain,
( spl778_41
| spl778_497
| ~ spl778_539 ),
inference(sat_conversion,[],[f73229]) ).
cnf(s810,plain,
( ~ spl778_248
| ~ spl778_503
| spl778_505 ),
inference(sat_conversion,[],[f73251]) ).
cnf(s811,plain,
( ~ spl778_248
| ~ spl778_503
| spl778_507 ),
inference(sat_conversion,[],[f73252]) ).
cnf(s831,plain,
( ~ spl778_249
| spl778_474
| ~ spl778_528 ),
inference(sat_conversion,[],[f73388]) ).
cnf(s832,plain,
( ~ spl778_249
| spl778_476
| ~ spl778_528 ),
inference(sat_conversion,[],[f73389]) ).
cnf(s838,plain,
( ~ spl778_249
| spl778_470
| ~ spl778_528 ),
inference(sat_conversion,[],[f73415]) ).
cnf(s845,plain,
( ~ spl778_444
| spl778_465
| ~ spl778_467
| ~ spl778_468
| ~ spl778_469
| ~ spl778_470
| spl778_473
| ~ spl778_476 ),
inference(sat_conversion,[],[f73449]) ).
cnf(s849,plain,
( ~ spl778_446
| ~ spl778_498
| ~ spl778_499
| ~ spl778_500
| ~ spl778_501
| spl778_502
| spl778_504
| ~ spl778_507 ),
inference(sat_conversion,[],[f73468]) ).
cnf(s854,plain,
( ~ spl778_249
| spl778_469
| ~ spl778_528 ),
inference(sat_conversion,[],[f73484]) ).
cnf(s856,plain,
( spl778_39
| ~ spl778_472
| spl778_542 ),
inference(sat_conversion,[],[f73507]) ).
cnf(s860,plain,
( spl778_15
| ~ spl778_465
| ~ spl778_528 ),
inference(sat_conversion,[],[f73524]) ).
cnf(s864,plain,
( ~ spl778_249
| spl778_444
| spl778_542 ),
inference(sat_conversion,[],[f73527]) ).
cnf(s869,plain,
( spl778_445
| ~ spl778_527
| ~ spl778_542 ),
inference(sat_conversion,[],[f73536]) ).
cnf(s877,plain,
( ~ spl778_16
| ~ spl778_51
| ~ spl778_446
| ~ spl778_498
| ~ spl778_499
| ~ spl778_500
| ~ spl778_501
| ~ spl778_503
| ~ spl778_504
| ~ spl778_505
| ~ spl778_507
| spl778_539 ),
inference(sat_conversion,[],[f73621]) ).
cnf(s878,plain,
( ~ spl778_248
| spl778_498
| ~ spl778_503 ),
inference(sat_conversion,[],[f73624]) ).
cnf(s879,plain,
( ~ spl778_248
| spl778_500
| ~ spl778_503 ),
inference(sat_conversion,[],[f73627]) ).
cnf(s881,plain,
( ~ spl778_248
| spl778_501
| ~ spl778_503 ),
inference(sat_conversion,[],[f73636]) ).
cnf(s883,plain,
( ~ spl778_497
| spl778_527 ),
inference(sat_conversion,[],[f73658]) ).
cnf(s888,plain,
( spl778_15
| ~ spl778_502
| ~ spl778_503 ),
inference(sat_conversion,[],[f73679]) ).
cnf(s898,plain,
( ~ spl778_248
| spl778_446
| spl778_527 ),
inference(sat_conversion,[],[f73685]) ).
cnf(s899,plain,
( ~ spl778_248
| ~ spl778_249
| spl778_444
| spl778_446 ),
inference(rat,[],[s660,s697]) ).
cnf(s919,plain,
spl778_65,
inference(rat,[],[s50,s16]) ).
cnf(s922,plain,
spl778_51,
inference(rat,[],[s36,s16]) ).
cnf(s923,plain,
spl778_48,
inference(rat,[],[s33,s16]) ).
cnf(s924,plain,
spl778_46,
inference(rat,[],[s32,s16]) ).
cnf(s925,plain,
spl778_33,
inference(rat,[],[s19,s16]) ).
cnf(s930,plain,
spl778_72,
inference(rat,[],[s56,s919]) ).
cnf(s936,plain,
spl778_56,
inference(rat,[],[s41,s924]) ).
cnf(s940,plain,
spl778_16,
inference(rat,[],[s14,s16]) ).
cnf(s948,plain,
spl778_37,
inference(rat,[],[s23,s5]) ).
cnf(s949,plain,
spl778_36,
inference(rat,[],[s22,s5]) ).
cnf(s950,plain,
spl778_14,
inference(rat,[],[s13,s5]) ).
cnf(s951,plain,
spl778_13,
inference(rat,[],[s12,s5]) ).
cnf(s952,plain,
spl778_12,
inference(rat,[],[s11,s5]) ).
cnf(s953,plain,
spl778_11,
inference(rat,[],[s10,s5]) ).
cnf(s954,plain,
spl778_10,
inference(rat,[],[s9,s5]) ).
cnf(s955,plain,
spl778_9,
inference(rat,[],[s8,s5]) ).
cnf(s971,plain,
spl778_38,
inference(rat,[],[s30,s952]) ).
cnf(s973,plain,
spl778_40,
inference(rat,[],[s43,s953]) ).
cnf(s999,plain,
~ spl778_6,
inference(rat,[],[s4,s5]) ).
cnf(s1000,plain,
spl778_248,
inference(rat,[],[s268,s954,s930,s948,s950,s952,s999]) ).
cnf(s1010,plain,
~ spl778_39,
inference(rat,[],[s24,s971,s999]) ).
cnf(s1055,plain,
~ spl778_5,
inference(rat,[],[s3,s5]) ).
cnf(s1059,plain,
spl778_249,
inference(rat,[],[s269,s955,s936,s949,s951,s953,s1055]) ).
cnf(s1069,plain,
~ spl778_41,
inference(rat,[],[s25,s973,s1055]) ).
cnf(s1105,plain,
spl778_444,
inference(rat,[],[s877,s849,s800,s878,s879,s881,s888,s810,s811,s809,s808,s883,s869,s899,s864,s922,s940,s1000,s16,s1069,s697,s1059]) ).
cnf(s1106,plain,
( spl778_527
| ~ spl778_446 ),
inference(rat,[],[s877,s849,s800,s878,s879,s881,s888,s810,s811,s809,s808,s883,s922,s940,s1000,s16,s1069]) ).
cnf(s1107,plain,
~ spl778_527,
inference(rat,[],[s845,s755,s860,s774,s831,s832,s838,s854,s752,s775,s856,s776,s869,s1105,s923,s925,s16,s1059,s1010,s697]) ).
cnf(s1110,plain,
spl778_446,
inference(rat,[],[s898,s1000,s1107]) ).
cnf(s1111,plain,
$false,
inference(rat,[],[s1106,s1110,s1107]) ).
fof(f73686,plain,
$false,
inference(avatar_sat_refutation,[],[s1111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT360+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n020.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 15:01:47 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 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
% 17.45/6.91 % (3480458)Detected formulas, will run a generic FOF schedule.
% 17.45/6.91 % (3480467)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1438401401:i=119:av=off:ss=axioms_2958 on theBenchmark for (2958ds/119Mi)
% 17.45/6.91 % (3480465)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=1650861506:i=141695:sd=1:nm=32:gsp=on:ss=included_2958 on theBenchmark for (2958ds/141695Mi)
% 17.45/6.91 % (3480464)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=659847435:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2958 on theBenchmark for (2958ds/134677Mi)
% 17.45/6.91 % (3480463)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=3343115112:i=141193_2958 on theBenchmark for (2958ds/141193Mi)
% 17.45/6.91 % (3480466)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4206249662:i=109:sd=1:ins=1:gsp=on:ss=axioms_2958 on theBenchmark for (2958ds/109Mi)
% 17.45/6.91 % (3480467)Instruction limit reached!
% 17.45/6.91 % (3480467)------------------------------
% 17.45/6.91 % (3480467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/6.91 % (3480467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/6.91 % (3480467)CaDiCaL version: 2.1.3
% 17.45/6.91 % (3480467)Termination reason: Instruction limit
% 17.45/6.91 % (3480467)Termination phase: SInE selection
% 17.45/6.91 % (3480467)Time elapsed: 0.054 s
% 17.45/6.91 % (3480467)Peak memory usage: 173 MB
% 17.45/6.91 % (3480467)Instructions burned: 120 (million)
% 17.45/6.91 % (3480469)dis-21_1_sil=8000:lcm=predicate:random_seed=20835572:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2958 on theBenchmark for (2958ds/129Mi)
% 17.45/6.91 % (3480468)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3552359019:s2a=on:i=139:gtg=position_2958 on theBenchmark for (2958ds/139Mi)
% 17.45/6.91 % (3480466)Instruction limit reached!
% 17.45/6.91 % (3480466)------------------------------
% 17.45/6.91 % (3480466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/6.91 % (3480466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/6.91 % (3480466)CaDiCaL version: 2.1.3
% 17.45/6.91 % (3480466)Termination reason: Instruction limit
% 17.45/6.91 % (3480466)Termination phase: SInE selection
% 17.45/6.91 % (3480466)Time elapsed: 0.083 s
% 17.45/6.91 % (3480466)Peak memory usage: 173 MB
% 17.45/6.91 % (3480466)Instructions burned: 109 (million)
% 17.45/6.91 % (3480468)Instruction limit reached!
% 17.45/6.91 % (3480468)------------------------------
% 17.45/6.91 % (3480468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/6.91 % (3480468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/6.91 % (3480468)CaDiCaL version: 2.1.3
% 17.45/6.91 % (3480468)Termination reason: Instruction limit
% 17.45/6.91 % (3480468)Termination phase: Property scanning
% 17.45/6.91 % (3480468)Time elapsed: 0.066 s
% 17.45/6.91 % (3480468)Peak memory usage: 173 MB
% 17.45/6.91 % (3480468)Instructions burned: 139 (million)
% 17.45/6.91 % (3480469)Instruction limit reached!
% 17.45/6.91 % (3480469)------------------------------
% 17.45/6.91 % (3480469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/6.91 % (3480469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/6.91 % (3480469)CaDiCaL version: 2.1.3
% 17.45/6.91 % (3480469)Termination reason: Instruction limit
% 17.45/6.91 % (3480469)Termination phase: SInE selection
% 17.45/6.91 % (3480469)Time elapsed: 0.099 s
% 17.45/6.91 % (3480469)Peak memory usage: 173 MB
% 17.45/6.91 % (3480469)Instructions burned: 130 (million)
% 17.45/6.91 % (3480476)lrs+10_1_sil=8000:sp=occurrence:random_seed=3302843843:i=285:sd=3:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/285Mi)
% 17.45/6.91 % (3480478)lrs+10_1_sil=32000:urr=on:br=off:random_seed=312815171:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/157Mi)
% 17.45/6.91 % (3480479)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1729608934:i=325:sd=1:ss=axioms:sgt=32_2955 on theBenchmark for (2955ds/325Mi)
% 17.45/6.91 % (3480476)Instruction limit reached!
% 17.45/6.91 % (3480476)------------------------------
% 17.45/6.91 % (3480476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/6.91 % (3480476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480476)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480476)Termination reason: Instruction limit
% 23.70/7.85 % (3480476)Termination phase: SInE selection
% 23.70/7.85 % (3480476)Time elapsed: 0.119 s
% 23.70/7.85 % (3480476)Peak memory usage: 174 MB
% 23.70/7.85 % (3480476)Instructions burned: 285 (million)
% 23.70/7.85 % (3480480)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=3374867886:s2a=on:i=248:s2at=1.23:gtg=position_2955 on theBenchmark for (2955ds/248Mi)
% 23.70/7.85 % (3480478)Instruction limit reached!
% 23.70/7.85 % (3480478)------------------------------
% 23.70/7.85 % (3480478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.70/7.85 % (3480478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480478)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480478)Termination reason: Instruction limit
% 23.70/7.85 % (3480478)Termination phase: Property scanning
% 23.70/7.85 % (3480478)Time elapsed: 0.074 s
% 23.70/7.85 % (3480478)Peak memory usage: 173 MB
% 23.70/7.85 % (3480478)Instructions burned: 158 (million)
% 23.70/7.85 % (3480484)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=348164895:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2953 on theBenchmark for (2953ds/294Mi)
% 23.70/7.85 % (3480480)Instruction limit reached!
% 23.70/7.85 % (3480480)------------------------------
% 23.70/7.85 % (3480480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.70/7.85 % (3480480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480480)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480480)Termination reason: Instruction limit
% 23.70/7.85 % (3480480)Termination phase: Property scanning
% 23.70/7.85 % (3480480)Time elapsed: 0.113 s
% 23.70/7.85 % (3480480)Peak memory usage: 173 MB
% 23.70/7.85 % (3480480)Instructions burned: 250 (million)
% 23.70/7.85 % (3480479)Instruction limit reached!
% 23.70/7.85 % (3480479)------------------------------
% 23.70/7.85 % (3480479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.70/7.85 % (3480479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480479)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480479)Termination reason: Instruction limit
% 23.70/7.85 % (3480479)Termination phase: SInE selection
% 23.70/7.85 % (3480479)Time elapsed: 0.235 s
% 23.70/7.85 % (3480479)Peak memory usage: 174 MB
% 23.70/7.85 % (3480479)Instructions burned: 326 (million)
% 23.70/7.85 % (3480486)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2134420006:i=2350_2953 on theBenchmark for (2953ds/2350Mi)
% 23.70/7.85 % (3480484)Instruction limit reached!
% 23.70/7.85 % (3480484)------------------------------
% 23.70/7.85 % (3480484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.70/7.85 % (3480484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480484)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480484)Termination reason: Instruction limit
% 23.70/7.85 % (3480484)Termination phase: SInE selection
% 23.70/7.85 % (3480484)Time elapsed: 0.117 s
% 23.70/7.85 % (3480484)Peak memory usage: 174 MB
% 23.70/7.85 % (3480484)Instructions burned: 296 (million)
% 23.70/7.85 % (3480488)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4084553351:cts=off:i=113:fsr=off:ss=included:sgt=4_2952 on theBenchmark for (2952ds/113Mi)
% 23.70/7.85 % (3480491)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1366676662:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2951 on theBenchmark for (2951ds/114Mi)
% 23.70/7.85 % (3480490)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3345050703:i=127:av=off:fsr=off:sup=off_2951 on theBenchmark for (2951ds/127Mi)
% 23.70/7.85 % (3480491)Instruction limit reached!
% 23.70/7.85 % (3480491)------------------------------
% 23.70/7.85 % (3480491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.70/7.85 % (3480491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.70/7.85 % (3480491)CaDiCaL version: 2.1.3
% 23.70/7.85 % (3480491)Termination reason: Instruction limit
% 23.70/7.85 % (3480491)Termination phase: Property scanning
% 23.70/7.85 % (3480491)Time elapsed: 0.031 s
% 23.70/7.85 % (3480491)Peak memory usage: 173 MB
% 23.70/7.85 % (3480491)Instructions burned: 119 (million)
% 23.70/7.85 % (3480488)Instruction limit reached!
% 23.70/7.85 % (3480488)------------------------------
% 23.70/7.85 % (3480488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480488)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480488)Termination reason: Instruction limit
% 57.31/12.56 % (3480488)Termination phase: SInE selection
% 57.31/12.56 % (3480488)Time elapsed: 0.091 s
% 57.31/12.56 % (3480488)Peak memory usage: 173 MB
% 57.31/12.56 % (3480488)Instructions burned: 113 (million)
% 57.31/12.56 % (3480490)Instruction limit reached!
% 57.31/12.56 % (3480490)------------------------------
% 57.31/12.56 % (3480490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480490)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480490)Termination reason: Instruction limit
% 57.31/12.56 % (3480490)Termination phase: Preprocessing 1
% 57.31/12.56 % (3480490)Time elapsed: 0.097 s
% 57.31/12.56 % (3480490)Peak memory usage: 174 MB
% 57.31/12.56 % (3480490)Instructions burned: 127 (million)
% 57.31/12.56 % (3480495)lrs+10_1_sil=8000:sp=occurrence:random_seed=3737864870:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2949 on theBenchmark for (2949ds/907Mi)
% 57.31/12.56 % (3480496)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=849202262:i=437:sd=1:aac=none:ss=included_2949 on theBenchmark for (2949ds/437Mi)
% 57.31/12.56 % (3480497)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4124847711:i=5202:ss=axioms:sgt=16_2949 on theBenchmark for (2949ds/5202Mi)
% 57.31/12.56 % (3480496)Instruction limit reached!
% 57.31/12.56 % (3480496)------------------------------
% 57.31/12.56 % (3480496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480496)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480496)Termination reason: Instruction limit
% 57.31/12.56 % (3480496)Termination phase: Preprocessing 2
% 57.31/12.56 % (3480496)Time elapsed: 0.344 s
% 57.31/12.56 % (3480496)Peak memory usage: 176 MB
% 57.31/12.56 % (3480496)Instructions burned: 437 (million)
% 57.31/12.56 % (3480495)Instruction limit reached!
% 57.31/12.56 % (3480495)------------------------------
% 57.31/12.56 % (3480495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480495)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480495)Termination reason: Instruction limit
% 57.31/12.56 % (3480495)Termination phase: Preprocessing 2
% 57.31/12.56 % (3480495)Time elapsed: 0.423 s
% 57.31/12.56 % (3480495)Peak memory usage: 192 MB
% 57.31/12.56 % (3480495)Instructions burned: 907 (million)
% 57.31/12.56 % (3480501)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1325253380:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2944 on theBenchmark for (2944ds/134Mi)
% 57.31/12.56 % (3480502)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=781949851:st=8:i=592:sd=3:ep=RST:ss=axioms_2944 on theBenchmark for (2944ds/592Mi)
% 57.31/12.56 % (3480501)Instruction limit reached!
% 57.31/12.56 % (3480501)------------------------------
% 57.31/12.56 % (3480501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480501)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480501)Termination reason: Instruction limit
% 57.31/12.56 % (3480501)Termination phase: SInE selection
% 57.31/12.56 % (3480501)Time elapsed: 0.103 s
% 57.31/12.56 % (3480501)Peak memory usage: 173 MB
% 57.31/12.56 % (3480501)Instructions burned: 135 (million)
% 57.31/12.56 % (3480502)Instruction limit reached!
% 57.31/12.56 % (3480502)------------------------------
% 57.31/12.56 % (3480502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.31/12.56 % (3480502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.31/12.56 % (3480502)CaDiCaL version: 2.1.3
% 57.31/12.56 % (3480502)Termination reason: Instruction limit
% 57.31/12.56 % (3480502)Termination phase: SInE selection
% 57.31/12.56 % (3480502)Time elapsed: 0.211 s
% 57.31/12.56 % (3480502)Peak memory usage: 175 MB
% 57.31/12.56 % (3480502)Instructions burned: 595 (million)
% 57.31/12.56 % (3480505)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2417940529:st=3:i=13193:sd=3:ss=axioms_2942 on theBenchmark for (2942ds/13193Mi)
% 57.31/12.56 % (3480506)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=3410438495:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2940 on theBenchmark for (2940ds/125Mi)
% 86.48/16.68 % (3480506)Instruction limit reached!
% 86.48/16.68 % (3480506)------------------------------
% 86.48/16.68 % (3480506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480506)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480506)Termination reason: Instruction limit
% 86.48/16.68 % (3480506)Termination phase: Property scanning
% 86.48/16.68 % (3480506)Time elapsed: 0.033 s
% 86.48/16.68 % (3480506)Peak memory usage: 173 MB
% 86.48/16.68 % (3480506)Instructions burned: 129 (million)
% 86.48/16.68 % (3480509)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=241010138:i=134:gtgl=5:slsql=off:gtg=exists_sym_2939 on theBenchmark for (2939ds/134Mi)
% 86.48/16.68 % (3480509)Instruction limit reached!
% 86.48/16.68 % (3480509)------------------------------
% 86.48/16.68 % (3480509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480509)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480509)Termination reason: Instruction limit
% 86.48/16.68 % (3480509)Termination phase: Property scanning
% 86.48/16.68 % (3480509)Time elapsed: 0.034 s
% 86.48/16.68 % (3480509)Peak memory usage: 173 MB
% 86.48/16.68 % (3480509)Instructions burned: 136 (million)
% 86.48/16.68 % (3480511)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2369800287:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/141Mi)
% 86.48/16.68 % (3480511)Instruction limit reached!
% 86.48/16.68 % (3480511)------------------------------
% 86.48/16.68 % (3480511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480511)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480511)Termination reason: Instruction limit
% 86.48/16.68 % (3480511)Termination phase: SInE selection
% 86.48/16.68 % (3480511)Time elapsed: 0.062 s
% 86.48/16.68 % (3480511)Peak memory usage: 173 MB
% 86.48/16.68 % (3480511)Instructions burned: 142 (million)
% 86.48/16.68 % (3480513)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4287405508:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2935 on theBenchmark for (2935ds/431Mi)
% 86.48/16.68 % (3480486)Instruction limit reached!
% 86.48/16.68 % (3480486)------------------------------
% 86.48/16.68 % (3480486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480486)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480486)Termination reason: Instruction limit
% 86.48/16.68 % (3480486)Termination phase: Preprocessing 3
% 86.48/16.68 % (3480486)Time elapsed: 1.765 s
% 86.48/16.68 % (3480486)Peak memory usage: 276 MB
% 86.48/16.68 % (3480486)Instructions burned: 2350 (million)
% 86.48/16.68 % (3480513)Instruction limit reached!
% 86.48/16.68 % (3480513)------------------------------
% 86.48/16.68 % (3480513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480513)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480513)Termination reason: Instruction limit
% 86.48/16.68 % (3480513)Termination phase: Preprocessing 2
% 86.48/16.68 % (3480513)Time elapsed: 0.199 s
% 86.48/16.68 % (3480513)Peak memory usage: 177 MB
% 86.48/16.68 % (3480513)Instructions burned: 432 (million)
% 86.48/16.68 % (3480515)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=125008906:i=6060:aac=none:ins=25_2933 on theBenchmark for (2933ds/6060Mi)
% 86.48/16.68 % (3480516)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=3727397125:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2932 on theBenchmark for (2932ds/150Mi)
% 86.48/16.68 % (3480516)Instruction limit reached!
% 86.48/16.68 % (3480516)------------------------------
% 86.48/16.68 % (3480516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.48/16.68 % (3480516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.48/16.68 % (3480516)CaDiCaL version: 2.1.3
% 86.48/16.68 % (3480516)Termination reason: Instruction limit
% 119.15/21.22 % (3480516)Termination phase: SInE selection
% 119.15/21.22 % (3480516)Time elapsed: 0.066 s
% 119.15/21.22 % (3480516)Peak memory usage: 173 MB
% 119.15/21.22 % (3480516)Instructions burned: 152 (million)
% 119.15/21.22 % (3480519)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3146663211:i=14155:bd=all_2930 on theBenchmark for (2930ds/14155Mi)
% 119.15/21.22 % (3480497)Instruction limit reached!
% 119.15/21.22 % (3480497)------------------------------
% 119.15/21.22 % (3480497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/21.22 % (3480497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/21.22 % (3480497)CaDiCaL version: 2.1.3
% 119.15/21.22 % (3480497)Termination reason: Instruction limit
% 119.15/21.22 % (3480497)Termination phase: Property scanning
% 119.15/21.22 % (3480497)Time elapsed: 3.284 s
% 119.15/21.22 % (3480497)Peak memory usage: 296 MB
% 119.15/21.22 % (3480497)Instructions burned: 5204 (million)
% 119.15/21.22 % (3480521)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1732995614:i=667:av=off:fsr=off_2914 on theBenchmark for (2914ds/667Mi)
% 119.15/21.22 % (3480521)Instruction limit reached!
% 119.15/21.22 % (3480521)------------------------------
% 119.15/21.22 % (3480521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/21.22 % (3480521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/21.22 % (3480521)CaDiCaL version: 2.1.3
% 119.15/21.22 % (3480521)Termination reason: Instruction limit
% 119.15/21.22 % (3480521)Termination phase: Preprocessing 2
% 119.15/21.22 % (3480521)Time elapsed: 0.583 s
% 119.15/21.22 % (3480521)Peak memory usage: 215 MB
% 119.15/21.22 % (3480521)Instructions burned: 667 (million)
% 119.15/21.22 % (3480524)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3709679387:s2a=on:i=185:s2at=1.8:fdi=4_2906 on theBenchmark for (2906ds/185Mi)
% 119.15/21.22 % (3480524)Instruction limit reached!
% 119.15/21.22 % (3480524)------------------------------
% 119.15/21.22 % (3480524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/21.22 % (3480524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/21.22 % (3480524)CaDiCaL version: 2.1.3
% 119.15/21.22 % (3480524)Termination reason: Instruction limit
% 119.15/21.22 % (3480524)Termination phase: SInE selection
% 119.15/21.22 % (3480524)Time elapsed: 0.145 s
% 119.15/21.22 % (3480524)Peak memory usage: 173 MB
% 119.15/21.22 % (3480524)Instructions burned: 186 (million)
% 119.15/21.22 % (3480526)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1638904465:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2903 on theBenchmark for (2903ds/193Mi)
% 119.15/21.22 % (3480526)Instruction limit reached!
% 119.15/21.22 % (3480526)------------------------------
% 119.15/21.22 % (3480526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/21.22 % (3480526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/21.22 % (3480526)CaDiCaL version: 2.1.3
% 119.15/21.22 % (3480526)Termination reason: Instruction limit
% 119.15/21.22 % (3480526)Termination phase: SInE selection
% 119.15/21.22 % (3480526)Time elapsed: 0.145 s
% 119.15/21.22 % (3480526)Peak memory usage: 173 MB
% 119.15/21.22 % (3480526)Instructions burned: 193 (million)
% 119.15/21.22 % (3480528)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4150033795:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2900 on theBenchmark for (2900ds/4850Mi)
% 119.15/21.22 % (3480519)Instruction limit reached!
% 119.15/21.22 % (3480519)------------------------------
% 119.15/21.22 % (3480519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/21.22 % (3480519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/21.22 % (3480519)CaDiCaL version: 2.1.3
% 119.15/21.22 % (3480519)Termination reason: Instruction limit
% 119.15/21.22 % (3480519)Termination phase: Saturation
% 119.15/21.22 % (3480519)Time elapsed: 4.379 s
% 119.15/21.22 % (3480519)Peak memory usage: 765 MB
% 119.15/21.22 % (3480519)Instructions burned: 14156 (million)
% 119.15/21.22 % (3480530)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1150101881:i=12111:sd=1:ss=included_2884 on theBenchmark for (2884ds/12111Mi)
% 119.15/21.22 % (3480515)Instruction limit reached!
% 119.15/21.22 % (3480515)------------------------------
% 119.15/21.22 % (3480515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.86 % (3480515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.86 % (3480515)CaDiCaL version: 2.1.3
% 110.08/22.86 % (3480515)Termination reason: Instruction limit
% 110.08/22.86 % (3480515)Termination phase: NewCNF
% 110.08/22.86 % (3480515)Time elapsed: 4.883 s
% 110.08/22.86 % (3480515)Peak memory usage: 331 MB
% 110.08/22.86 % (3480515)Instructions burned: 6061 (million)
% 110.08/22.86 % (3480532)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1912791123:i=319:kws=precedence:fsr=off_2882 on theBenchmark for (2882ds/319Mi)
% 110.08/22.86 % (3480532)Instruction limit reached!
% 110.08/22.86 % (3480532)------------------------------
% 110.08/22.86 % (3480532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.86 % (3480532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.86 % (3480532)CaDiCaL version: 2.1.3
% 110.08/22.86 % (3480532)Termination reason: Instruction limit
% 110.08/22.86 % (3480532)Termination phase: Preprocessing 1
% 110.08/22.86 % (3480532)Time elapsed: 0.233 s
% 110.08/22.86 % (3480532)Peak memory usage: 175 MB
% 110.08/22.86 % (3480532)Instructions burned: 320 (million)
% 110.08/22.86 % (3480534)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2966403735:i=2064:ep=RST_2878 on theBenchmark for (2878ds/2064Mi)
% 110.08/22.86 % (3480528)Instruction limit reached!
% 110.08/22.86 % (3480528)------------------------------
% 110.08/22.86 % (3480528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.86 % (3480528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.86 % (3480528)CaDiCaL version: 2.1.3
% 110.08/22.86 % (3480528)Termination reason: Instruction limit
% 110.08/22.86 % (3480528)Termination phase: Function definition elimination
% 110.08/22.86 % (3480528)Time elapsed: 3.040 s
% 110.08/22.86 % (3480528)Peak memory usage: 297 MB
% 110.08/22.86 % (3480528)Instructions burned: 4851 (million)
% 110.08/22.86 % (3480536)dis-1011_128_sil=32000:random_seed=3404413941:i=3706:ep=RST:av=off_2867 on theBenchmark for (2867ds/3706Mi)
% 110.08/22.86 % (3480505)Instruction limit reached!
% 110.08/22.86 % (3480505)------------------------------
% 110.08/22.86 % (3480505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.86 % (3480505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.86 % (3480505)CaDiCaL version: 2.1.3
% 110.08/22.86 % (3480505)Termination reason: Instruction limit
% 110.08/22.86 % (3480505)Termination phase: Saturation
% 110.08/22.86 % (3480505)Time elapsed: 7.747 s
% 110.08/22.86 % (3480505)Peak memory usage: 398 MB
% 110.08/22.86 % (3480505)Instructions burned: 13196 (million)
% 110.08/22.86 % (3480534)Instruction limit reached!
% 110.08/22.86 % (3480534)------------------------------
% 110.08/22.86 % (3480534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.86 % (3480534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.86 % (3480534)CaDiCaL version: 2.1.3
% 110.08/22.86 % (3480534)Termination reason: Instruction limit
% 110.08/22.86 % (3480534)Termination phase: Preprocessing 3
% 110.08/22.86 % (3480534)Time elapsed: 1.516 s
% 110.08/22.86 % (3480534)Peak memory usage: 281 MB
% 110.08/22.86 % (3480534)Instructions burned: 2065 (million)
% 110.08/22.86 % (3480538)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1795450355:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2862 on theBenchmark for (2862ds/757Mi)
% 110.08/22.87 % (3480539)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=596310568:i=13913:ss=axioms:sgt=8_2861 on theBenchmark for (2861ds/13913Mi)
% 110.08/22.87 % (3480538)Refutation not found, incomplete strategy
% 110.08/22.87 % (3480538)------------------------------
% 110.08/22.87 % (3480538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480538)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480538)Termination reason: Refutation not found, incomplete strategy
% 110.08/22.87 % (3480538)Time elapsed: 0.428 s
% 110.08/22.87 % (3480538)Peak memory usage: 182 MB
% 110.08/22.87 % (3480538)Instructions burned: 583 (million)
% 110.08/22.87 % (3480538)------------------------------
% 110.08/22.87 % (3480538)------------------------------
% 110.08/22.87 % (3480542)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3633575279:i=9925:aac=none_2853 on theBenchmark for (2853ds/9925Mi)
% 110.08/22.87 % (3480536)Instruction limit reached!
% 110.08/22.87 % (3480536)------------------------------
% 110.08/22.87 % (3480536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480536)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480536)Termination reason: Instruction limit
% 110.08/22.87 % (3480536)Termination phase: Property scanning
% 110.08/22.87 % (3480536)Time elapsed: 2.420 s
% 110.08/22.87 % (3480536)Peak memory usage: 338 MB
% 110.08/22.87 % (3480536)Instructions burned: 3708 (million)
% 110.08/22.87 % (3480544)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=464657007:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2841 on theBenchmark for (2841ds/2479Mi)
% 110.08/22.87 % (3480544)Refutation not found, incomplete strategy
% 110.08/22.87 % (3480544)------------------------------
% 110.08/22.87 % (3480544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480544)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480544)Termination reason: Refutation not found, incomplete strategy
% 110.08/22.87 % (3480544)Time elapsed: 0.761 s
% 110.08/22.87 % (3480544)Peak memory usage: 181 MB
% 110.08/22.87 % (3480544)Instructions burned: 973 (million)
% 110.08/22.87 % (3480544)------------------------------
% 110.08/22.87 % (3480544)------------------------------
% 110.08/22.87 % (3480546)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2657507113:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2829 on theBenchmark for (2829ds/440Mi)
% 110.08/22.87 % (3480546)Instruction limit reached!
% 110.08/22.87 % (3480546)------------------------------
% 110.08/22.87 % (3480546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480546)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480546)Termination reason: Instruction limit
% 110.08/22.87 % (3480546)Termination phase: Property scanning
% 110.08/22.87 % (3480546)Time elapsed: 0.193 s
% 110.08/22.87 % (3480546)Peak memory usage: 173 MB
% 110.08/22.87 % (3480546)Instructions burned: 442 (million)
% 110.08/22.87 % (3480548)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1188157739:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2825 on theBenchmark for (2825ds/11145Mi)
% 110.08/22.87 % (3480530)Instruction limit reached!
% 110.08/22.87 % (3480530)------------------------------
% 110.08/22.87 % (3480530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480530)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480530)Termination reason: Instruction limit
% 110.08/22.87 % (3480530)Termination phase: Saturation
% 110.08/22.87 % (3480530)Time elapsed: 7.985 s
% 110.08/22.87 % (3480530)Peak memory usage: 291 MB
% 110.08/22.87 % (3480530)Instructions burned: 12112 (million)
% 110.08/22.87 % (3480542)Instruction limit reached!
% 110.08/22.87 % (3480542)------------------------------
% 110.08/22.87 % (3480542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480542)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480542)Termination reason: Instruction limit
% 110.08/22.87 % (3480542)Termination phase: Property scanning
% 110.08/22.87 % (3480542)Time elapsed: 4.968 s
% 110.08/22.87 % (3480542)Peak memory usage: 361 MB
% 110.08/22.87 % (3480542)Instructions burned: 9927 (million)
% 110.08/22.87 % (3480550)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2763495816:cts=off:i=3034:av=off:er=known:fsd=on_2803 on theBenchmark for (2803ds/3034Mi)
% 110.08/22.87 % (3480551)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3564954168:st=2:s2a=on:i=524:s2at=2:ss=axioms_2801 on theBenchmark for (2801ds/524Mi)
% 110.08/22.87 % (3480551)Instruction limit reached!
% 110.08/22.87 % (3480551)------------------------------
% 110.08/22.87 % (3480551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480551)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480551)Termination reason: Instruction limit
% 110.08/22.87 % (3480551)Termination phase: SInE selection
% 110.08/22.87 % (3480551)Time elapsed: 0.350 s
% 110.08/22.87 % (3480551)Peak memory usage: 174 MB
% 110.08/22.87 % (3480551)Instructions burned: 524 (million)
% 110.08/22.87 % (3480554)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1786133685:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2796 on theBenchmark for (2796ds/1016Mi)
% 110.08/22.87 % (3480554)Instruction limit reached!
% 110.08/22.87 % (3480554)------------------------------
% 110.08/22.87 % (3480554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.08/22.87 % (3480554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.08/22.87 % (3480554)CaDiCaL version: 2.1.3
% 110.08/22.87 % (3480554)Termination reason: Instruction limit
% 110.08/22.87 % (3480554)Termination phase: Saturation
% 110.08/22.87 % (3480554)Time elapsed: 0.681 s
% 110.08/22.87 % (3480554)Peak memory usage: 185 MB
% 110.08/22.87 % (3480554)Instructions burned: 1017 (million)
% 110.08/22.87 % (3480556)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1587211410:i=14123:bd=preordered:ins=4_2787 on theBenchmark for (2787ds/14123Mi)
% 110.08/22.87 % (3480548)First to succeed.
% 110.08/22.87 % (3480548)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3480458"
% 110.08/22.87 % (3480548)Refutation found. Thanks to Tanya!
% 110.08/22.87 % SZS status Theorem for theBenchmark
% 110.08/22.87 % SZS output start Proof for theBenchmark
% See solution above
% 130.50/23.13 % (3480548)------------------------------
% 130.50/23.13 % (3480548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.50/23.13 % (3480548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.50/23.13 % (3480548)CaDiCaL version: 2.1.3
% 130.50/23.13 % (3480548)Termination reason: Refutation
% 130.50/23.13 % (3480548)Time elapsed: 3.898 s
% 130.50/23.13 % (3480548)Peak memory usage: 313 MB
% 130.50/23.13 % (3480548)Instructions burned: 5747 (million)
% 130.50/23.13 % (3480548)------------------------------
% 130.50/23.13 % (3480548)------------------------------
% 130.50/23.13 % (3480458)Success in time 21.994 s
% 130.50/23.13 % Vampire exiting
%------------------------------------------------------------------------------