%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT378+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:31 AM UTC 2026
% Result : Theorem 64.64s 22.51s
% Output : Refutation 128.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 21
% Syntax : Number of formulae : 263 ( 41 unt; 6 def)
% Number of atoms : 1430 ( 46 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 2023 ( 856 ~;1005 |; 116 &)
% ( 10 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 7 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-5 aty)
% Number of variables : 318 ( 0 sgn 306 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2103,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_funct_2) ).
fof(f2104,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f3137,axiom,
! [X0,X1] :
( ( v1_relat_1(X0)
& v1_funct_1(X0)
& v1_finset_1(X1) )
=> v1_finset_1(k9_relat_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc13_finset_1) ).
fof(f17596,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18324,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f18325,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f18585,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_tops_2) ).
fof(f19627,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f55780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& l1_orders_2(X2) )
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X5] :
( ( v1_funct_1(X5)
& v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
& m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( ( r4_waybel_0(X0,X1,X4,X3)
& r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3)) )
=> r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_waybel34) ).
fof(f55781,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( v1_finset_1(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> r4_waybel_0(X0,X1,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d15_waybel34) ).
fof(f55783,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& l1_orders_2(X2) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( ( v4_waybel34(X3,X0,X1)
& v4_waybel34(X4,X1,X2) )
=> v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_waybel34) ).
fof(f55784,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& l1_orders_2(X2) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( ( v4_waybel34(X3,X0,X1)
& v4_waybel34(X4,X1,X2) )
=> v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f55783]) ).
fof(f55935,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2)
& v4_waybel34(X3,X0,X1)
& v4_waybel34(X4,X1,X2)
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X2)
& l1_orders_2(X2) )
& ~ v3_struct_0(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f55784]) ).
fof(f55936,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2)
& v4_waybel34(X3,X0,X1)
& v4_waybel34(X4,X1,X2)
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X2)
& l1_orders_2(X2) )
& ~ v3_struct_0(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f55935]) ).
fof(f55945,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f2104]) ).
fof(f55946,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f55945]) ).
fof(f55947,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) )
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f2103]) ).
fof(f55948,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) )
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f55947]) ).
fof(f55949,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( r4_waybel_0(X0,X1,X2,X3)
| ~ v1_finset_1(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f55781]) ).
fof(f55950,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( r4_waybel_0(X0,X1,X2,X3)
| ~ v1_finset_1(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f55949]) ).
fof(f56211,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3)
| ~ r4_waybel_0(X0,X1,X4,X3)
| ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X2)
| ~ l1_orders_2(X2) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f55780]) ).
fof(f56212,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3)
| ~ r4_waybel_0(X0,X1,X4,X3)
| ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X2)
| ~ l1_orders_2(X2) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f56211]) ).
fof(f56389,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f56390,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f57038,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18325]) ).
fof(f57039,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f57038]) ).
fof(f57040,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18324]) ).
fof(f57041,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f57040]) ).
fof(f57748,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18585]) ).
fof(f57749,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f57748]) ).
fof(f57774,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f57861,plain,
! [X0,X1] :
( v1_finset_1(k9_relat_1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(X1) ),
inference(ennf_transformation,[],[f3137]) ).
fof(f57862,plain,
! [X0,X1] :
( v1_finset_1(k9_relat_1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(X1) ),
inference(flattening,[],[f57861]) ).
fof(f57951,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f19627]) ).
fof(f57959,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17596]) ).
fof(f57960,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f57959]) ).
fof(f65709,plain,
( ~ v4_waybel34(k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(sK252),sK253,sK254),sK250,sK252)
& v4_waybel34(sK253,sK250,sK251)
& v4_waybel34(sK254,sK251,sK252)
& v1_funct_1(sK254)
& v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
& m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
& v1_funct_1(sK253)
& v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
& m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
& ~ v3_struct_0(sK252)
& l1_orders_2(sK252)
& ~ v3_struct_0(sK251)
& l1_orders_2(sK251)
& ~ v3_struct_0(sK250)
& l1_orders_2(sK250) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK250,sK251,sK252,sK253,sK254]),skolemize(X0,sK250),skolemize(X1,sK251),skolemize(X2,sK252),skolemize(X3,sK253),skolemize(X4,sK254)],[f55936]) ).
fof(f65716,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_waybel34(X2,X0,X1)
| ? [X3] :
( ~ r4_waybel_0(X0,X1,X2,X3)
& v1_finset_1(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( r4_waybel_0(X0,X1,X2,X3)
| ~ v1_finset_1(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f55950]) ).
fof(f65717,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_waybel34(X2,X0,X1)
| ? [X3] :
( ~ r4_waybel_0(X0,X1,X2,X3)
& v1_finset_1(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( r4_waybel_0(X0,X1,X2,X4)
| ~ v1_finset_1(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f65716]) ).
fof(f65718,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_waybel34(X2,X0,X1)
| ( ~ r4_waybel_0(X0,X1,X2,sK260(X0,X1,X2))
& v1_finset_1(sK260(X0,X1,X2))
& m1_subset_1(sK260(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( r4_waybel_0(X0,X1,X2,X4)
| ~ v1_finset_1(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK260]),skolemize(X3,sK260(X0,X1,X2))],[f65717]) ).
fof(f65770,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f68767,plain,
l1_orders_2(sK250),
inference(cnf_transformation,[],[f65709]) ).
fof(f68768,plain,
~ v3_struct_0(sK250),
inference(cnf_transformation,[],[f65709]) ).
fof(f68769,plain,
l1_orders_2(sK251),
inference(cnf_transformation,[],[f65709]) ).
fof(f68770,plain,
~ v3_struct_0(sK251),
inference(cnf_transformation,[],[f65709]) ).
fof(f68771,plain,
l1_orders_2(sK252),
inference(cnf_transformation,[],[f65709]) ).
fof(f68772,plain,
~ v3_struct_0(sK252),
inference(cnf_transformation,[],[f65709]) ).
fof(f68773,plain,
m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)),
inference(cnf_transformation,[],[f65709]) ).
fof(f68774,plain,
v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251)),
inference(cnf_transformation,[],[f65709]) ).
fof(f68775,plain,
v1_funct_1(sK253),
inference(cnf_transformation,[],[f65709]) ).
fof(f68776,plain,
m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252)),
inference(cnf_transformation,[],[f65709]) ).
fof(f68777,plain,
v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252)),
inference(cnf_transformation,[],[f65709]) ).
fof(f68778,plain,
v1_funct_1(sK254),
inference(cnf_transformation,[],[f65709]) ).
fof(f68779,plain,
v4_waybel34(sK254,sK251,sK252),
inference(cnf_transformation,[],[f65709]) ).
fof(f68780,plain,
v4_waybel34(sK253,sK250,sK251),
inference(cnf_transformation,[],[f65709]) ).
fof(f68781,plain,
~ v4_waybel34(k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(sK252),sK253,sK254),sK250,sK252),
inference(cnf_transformation,[],[f65709]) ).
fof(f68794,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,X1,X2)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| k5_relat_1(X3,X4) = k7_funct_2(X0,X1,X2,X3,X4)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f55946]) ).
fof(f68795,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f55948]) ).
fof(f68796,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f55948]) ).
fof(f68797,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f55948]) ).
fof(f68799,plain,
! [X2,X0,X1,X4] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_finset_1(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| r4_waybel_0(X0,X1,X2,X4)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f65718]) ).
fof(f68800,plain,
! [X2,X0,X1] :
( m1_subset_1(sK260(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v4_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f65718]) ).
fof(f68801,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_finset_1(sK260(X0,X1,X2))
| ~ v1_funct_1(X2)
| v4_waybel34(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f65718]) ).
fof(f68802,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(X0,X1,X2,sK260(X0,X1,X2))
| v4_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f65718]) ).
fof(f69092,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f65770]) ).
fof(f69169,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ r4_waybel_0(X0,X1,X4,X3)
| r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f56212]) ).
fof(f69533,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f56389]) ).
fof(f69534,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f56390]) ).
fof(f70525,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| k9_relat_1(X2,X3) = k4_pre_topc(X0,X1,X2,X3)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f57039]) ).
fof(f70526,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f57041]) ).
fof(f71629,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k1_relat_1(X2) = k2_pre_topc(X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f57749]) ).
fof(f71667,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f57774]) ).
fof(f71776,plain,
! [X0,X1] :
( v1_finset_1(k9_relat_1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(X1) ),
inference(cnf_transformation,[],[f57862]) ).
fof(f71880,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f57951]) ).
fof(f71890,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f57960]) ).
fof(f88077,plain,
m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252)),
inference(resolution,[],[f69092,f68776]) ).
fof(f88078,plain,
m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)),
inference(resolution,[],[f69092,f68773]) ).
fof(f88081,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK251))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| k5_relat_1(X0,sK254) = k7_funct_2(X1,u1_struct_0(sK251),u1_struct_0(sK252),X0,sK254)
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252)) ),
inference(resolution,[],[f68794,f68777]) ).
fof(f88084,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK251))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK251))
| k5_relat_1(X0,sK254) = k7_funct_2(X1,u1_struct_0(sK251),u1_struct_0(sK252),X0,sK254)
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252)) ),
inference(forward_subsumption_resolution,[],[f88081,f68778]) ).
fof(f88086,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK251))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK251))
| k5_relat_1(X0,sK254) = k7_funct_2(X1,u1_struct_0(sK251),u1_struct_0(sK252),X0,sK254) ),
inference(forward_subsumption_resolution,[],[f88084,f88077]) ).
fof(f88096,definition,
( spl2054_52
<=> ! [X0,X1] :
( ~ v1_funct_1(X0)
| k5_relat_1(X0,sK254) = k7_funct_2(X1,u1_struct_0(sK251),u1_struct_0(sK252),X0,sK254)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK251))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK251)) ) ),
introduced(definition,[new_symbols(definition,[spl2054_52])],[avatar_definition]) ).
fof(f88097,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,X1,u1_struct_0(sK251))
| k5_relat_1(X0,sK254) = k7_funct_2(X1,u1_struct_0(sK251),u1_struct_0(sK252),X0,sK254)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK251))
| ~ v1_funct_1(X0) )
| ~ spl2054_52 ),
inference(avatar_component_clause,[],[f88096]) ).
fof(f88099,definition,
( spl2054_53
<=> v1_xboole_0(u1_struct_0(sK251)) ),
introduced(definition,[new_symbols(definition,[spl2054_53])],[avatar_definition]) ).
fof(f88100,plain,
( ~ v1_xboole_0(u1_struct_0(sK251))
| spl2054_53 ),
inference(avatar_component_clause,[],[f88099]) ).
fof(f88101,plain,
( v1_xboole_0(u1_struct_0(sK251))
| ~ spl2054_53 ),
inference(avatar_component_clause,[],[f88099]) ).
fof(f88102,plain,
( spl2054_52
| spl2054_53 ),
inference(avatar_split_clause,[],[f88086,f88099,f88096]) ).
fof(f88103,plain,
( k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(sK252),sK253,sK254) = k5_relat_1(sK253,sK254)
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK253)
| ~ spl2054_52 ),
inference(resolution,[],[f88097,f68774]) ).
fof(f88104,plain,
( k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(sK252),sK253,sK254) = k5_relat_1(sK253,sK254)
| ~ v1_funct_1(sK253)
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88103,f88078]) ).
fof(f88105,plain,
( k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(sK252),sK253,sK254) = k5_relat_1(sK253,sK254)
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88104,f68775]) ).
fof(f88106,plain,
( ~ v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ spl2054_52 ),
inference(superposition,[],[f68781,f88105]) ).
fof(f88107,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(superposition,[],[f68797,f88105]) ).
fof(f88108,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88107,f68775]) ).
fof(f88109,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88108,f68774]) ).
fof(f88110,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88109,f88078]) ).
fof(f88111,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88110,f68778]) ).
fof(f88112,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88111,f68777]) ).
fof(f88113,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| v1_xboole_0(u1_struct_0(sK251))
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f88112,f88077]) ).
fof(f88115,definition,
( spl2054_54
<=> v1_funct_1(k5_relat_1(sK253,sK254)) ),
introduced(definition,[new_symbols(definition,[spl2054_54])],[avatar_definition]) ).
fof(f88117,plain,
( v1_funct_1(k5_relat_1(sK253,sK254))
| ~ spl2054_54 ),
inference(avatar_component_clause,[],[f88115]) ).
fof(f88118,plain,
( spl2054_53
| spl2054_54
| ~ spl2054_52 ),
inference(avatar_split_clause,[],[f88113,f88096,f88115,f88099]) ).
fof(f88123,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(superposition,[],[f68796,f88105]) ).
fof(f88130,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v1_xboole_0(u1_struct_0(sK251))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52 ),
inference(superposition,[],[f68795,f88105]) ).
fof(f88131,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| ~ v4_waybel34(sK254,sK251,sK252)
| ~ v1_funct_1(sK254)
| r4_waybel_0(sK251,sK252,sK254,X0)
| ~ m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(resolution,[],[f68799,f68777]) ).
fof(f88132,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| ~ v4_waybel34(sK253,sK250,sK251)
| ~ v1_funct_1(sK253)
| r4_waybel_0(sK250,sK251,sK253,X0)
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(resolution,[],[f68799,f68774]) ).
fof(f88134,plain,
( v3_struct_0(sK251)
| ~ l1_struct_0(sK251)
| ~ spl2054_53 ),
inference(resolution,[],[f71890,f88101]) ).
fof(f88135,plain,
( ~ l1_struct_0(sK251)
| ~ spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88134,f68770]) ).
fof(f88136,plain,
l1_struct_0(sK251),
inference(resolution,[],[f71880,f68769]) ).
fof(f88137,plain,
l1_struct_0(sK250),
inference(resolution,[],[f71880,f68767]) ).
fof(f88138,plain,
l1_struct_0(sK252),
inference(resolution,[],[f71880,f68771]) ).
fof(f88139,plain,
( $false
| ~ spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88136,f88135]) ).
fof(f88140,plain,
~ spl2054_53,
inference(avatar_contradiction_clause,[],[f88139]) ).
fof(f88141,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88123,f88100]) ).
fof(f88142,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88130,f88100]) ).
fof(f88143,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88141,f68775]) ).
fof(f88144,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88142,f68775]) ).
fof(f88145,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88143,f68774]) ).
fof(f88146,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88144,f68774]) ).
fof(f88147,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88145,f88078]) ).
fof(f88148,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_1(sK254)
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88146,f88078]) ).
fof(f88149,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88147,f68778]) ).
fof(f88150,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ v1_funct_2(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88148,f68778]) ).
fof(f88151,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88149,f68777]) ).
fof(f88152,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m1_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88150,f68777]) ).
fof(f88153,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88151,f88077]) ).
fof(f88154,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(forward_subsumption_resolution,[],[f88152,f88077]) ).
fof(f88156,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_funct_1(k5_relat_1(sK253,sK254))
| v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53 ),
inference(resolution,[],[f88153,f68801]) ).
fof(f88323,plain,
u1_struct_0(sK251) = k2_pre_topc(sK251),
inference(resolution,[],[f71667,f88136]) ).
fof(f88324,plain,
u1_struct_0(sK250) = k2_pre_topc(sK250),
inference(resolution,[],[f71667,f88137]) ).
fof(f88330,plain,
! [X0] :
( ~ l1_struct_0(sK250)
| ~ l1_struct_0(sK251)
| ~ v1_funct_1(sK253)
| k9_relat_1(sK253,X0) = k4_pre_topc(sK250,sK251,sK253,X0)
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(resolution,[],[f70525,f68774]) ).
fof(f88341,plain,
! [X0] :
( ~ l1_struct_0(sK251)
| ~ v1_funct_1(sK253)
| k9_relat_1(sK253,X0) = k4_pre_topc(sK250,sK251,sK253,X0)
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88330,f88137]) ).
fof(f88345,plain,
! [X0] :
( ~ v1_funct_1(sK253)
| k9_relat_1(sK253,X0) = k4_pre_topc(sK250,sK251,sK253,X0)
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88341,f88136]) ).
fof(f88348,plain,
! [X0] :
( k9_relat_1(sK253,X0) = k4_pre_topc(sK250,sK251,sK253,X0)
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88345,f68775]) ).
fof(f88351,plain,
! [X0] : k9_relat_1(sK253,X0) = k4_pre_topc(sK250,sK251,sK253,X0),
inference(forward_subsumption_resolution,[],[f88348,f88078]) ).
fof(f88356,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f69534,f69533]) ).
fof(f88358,plain,
v1_relat_1(sK253),
inference(resolution,[],[f88356,f68773]) ).
fof(f88394,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(superposition,[],[f69169,f88351]) ).
fof(f88443,plain,
! [X0] :
( m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251)))
| ~ l1_struct_0(sK250)
| ~ l1_struct_0(sK251)
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(superposition,[],[f70526,f88351]) ).
fof(f88449,plain,
! [X0] :
( m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251)))
| ~ l1_struct_0(sK251)
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88443,f88137]) ).
fof(f88452,plain,
! [X0] :
( m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251)))
| ~ v1_funct_1(sK253)
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88449,f88136]) ).
fof(f88455,plain,
! [X0] :
( m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251)))
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88452,f68775]) ).
fof(f88458,plain,
! [X0] :
( m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251)))
| ~ m1_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251)) ),
inference(forward_subsumption_resolution,[],[f88455,f68774]) ).
fof(f88461,plain,
! [X0] : m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(u1_struct_0(sK251))),
inference(forward_subsumption_resolution,[],[f88458,f88078]) ).
fof(f88514,plain,
( ~ v1_funct_1(sK253)
| k2_pre_topc(sK250) = k1_relat_1(sK253)
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| v3_struct_0(sK251)
| ~ l1_struct_0(sK251)
| ~ l1_struct_0(sK250) ),
inference(resolution,[],[f71629,f68774]) ).
fof(f88515,plain,
( ~ v1_funct_1(sK254)
| k2_pre_topc(sK251) = k1_relat_1(sK254)
| ~ m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_struct_0(sK252)
| ~ l1_struct_0(sK251) ),
inference(resolution,[],[f71629,f68777]) ).
fof(f88525,plain,
( k2_pre_topc(sK251) = k1_relat_1(sK254)
| ~ m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_struct_0(sK252)
| ~ l1_struct_0(sK251) ),
inference(forward_subsumption_resolution,[],[f88515,f68778]) ).
fof(f88526,plain,
( k2_pre_topc(sK250) = k1_relat_1(sK253)
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| v3_struct_0(sK251)
| ~ l1_struct_0(sK251)
| ~ l1_struct_0(sK250) ),
inference(forward_subsumption_resolution,[],[f88514,f68775]) ).
fof(f88530,plain,
( k2_pre_topc(sK251) = k1_relat_1(sK254)
| v3_struct_0(sK252)
| ~ l1_struct_0(sK252)
| ~ l1_struct_0(sK251) ),
inference(forward_subsumption_resolution,[],[f88525,f68776]) ).
fof(f88531,plain,
( k2_pre_topc(sK250) = k1_relat_1(sK253)
| v3_struct_0(sK251)
| ~ l1_struct_0(sK251)
| ~ l1_struct_0(sK250) ),
inference(forward_subsumption_resolution,[],[f88526,f68773]) ).
fof(f88533,plain,
( k2_pre_topc(sK251) = k1_relat_1(sK254)
| ~ l1_struct_0(sK252)
| ~ l1_struct_0(sK251) ),
inference(forward_subsumption_resolution,[],[f88530,f68772]) ).
fof(f88534,plain,
( k2_pre_topc(sK250) = k1_relat_1(sK253)
| ~ l1_struct_0(sK251)
| ~ l1_struct_0(sK250) ),
inference(forward_subsumption_resolution,[],[f88531,f68770]) ).
fof(f88536,plain,
( k2_pre_topc(sK251) = k1_relat_1(sK254)
| ~ l1_struct_0(sK251) ),
inference(forward_subsumption_resolution,[],[f88533,f88138]) ).
fof(f88537,plain,
( k2_pre_topc(sK250) = k1_relat_1(sK253)
| ~ l1_struct_0(sK250) ),
inference(forward_subsumption_resolution,[],[f88534,f88136]) ).
fof(f88539,plain,
k2_pre_topc(sK251) = k1_relat_1(sK254),
inference(forward_subsumption_resolution,[],[f88536,f88136]) ).
fof(f88540,plain,
k2_pre_topc(sK250) = k1_relat_1(sK253),
inference(forward_subsumption_resolution,[],[f88537,f88137]) ).
fof(f88544,plain,
u1_struct_0(sK251) = k1_relat_1(sK254),
inference(superposition,[],[f88323,f88539]) ).
fof(f88546,plain,
u1_struct_0(sK250) = k1_relat_1(sK253),
inference(superposition,[],[f88324,f88540]) ).
fof(f88549,plain,
m2_relset_1(sK254,k1_relat_1(sK254),u1_struct_0(sK252)),
inference(superposition,[],[f68776,f88544]) ).
fof(f88550,plain,
v1_funct_2(sK254,k1_relat_1(sK254),u1_struct_0(sK252)),
inference(superposition,[],[f68777,f88544]) ).
fof(f88556,plain,
( k5_relat_1(sK253,sK254) = k7_funct_2(u1_struct_0(sK250),k1_relat_1(sK254),u1_struct_0(sK252),sK253,sK254)
| ~ spl2054_52 ),
inference(superposition,[],[f88105,f88544]) ).
fof(f88561,plain,
! [X0] : m1_subset_1(k9_relat_1(sK253,X0),k1_zfmisc_1(k1_relat_1(sK254))),
inference(superposition,[],[f88461,f88544]) ).
fof(f88608,plain,
( k5_relat_1(sK253,sK254) = k7_funct_2(k1_relat_1(sK253),k1_relat_1(sK254),u1_struct_0(sK252),sK253,sK254)
| ~ spl2054_52 ),
inference(forward_demodulation,[],[f88556,f88546]) ).
fof(f88664,plain,
( v1_funct_2(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(superposition,[],[f88153,f88546]) ).
fof(f88665,plain,
( m2_relset_1(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| ~ spl2054_52
| spl2054_53 ),
inference(superposition,[],[f88154,f88546]) ).
fof(f88678,plain,
! [X0,X1] :
( m1_subset_1(sK260(sK250,X0,X1),k1_zfmisc_1(k1_relat_1(sK253)))
| v4_waybel34(X1,sK250,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK253),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK253),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(superposition,[],[f68800,f88546]) ).
fof(f89180,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| ~ v1_funct_1(sK253)
| r4_waybel_0(sK250,sK251,sK253,X0)
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f88132,f68780]) ).
fof(f89181,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| ~ v1_funct_1(sK254)
| r4_waybel_0(sK251,sK252,sK254,X0)
| ~ m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f88131,f68779]) ).
fof(f89182,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f88156,f88117]) ).
fof(f89218,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ v1_funct_2(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f88394,f68775]) ).
fof(f89282,plain,
! [X0,X1] :
( m1_subset_1(sK260(sK250,X0,X1),k1_zfmisc_1(k1_relat_1(sK253)))
| v4_waybel34(X1,sK250,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK253),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK253),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f88678,f68768]) ).
fof(f89481,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0)
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89180,f68775]) ).
fof(f89482,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0)
| ~ m2_relset_1(sK254,u1_struct_0(sK251),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f89181,f68778]) ).
fof(f89483,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f89182,f88106]) ).
fof(f89495,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(sK253,u1_struct_0(sK250),u1_struct_0(sK251))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89218,f68774]) ).
fof(f89556,plain,
! [X0,X1] :
( m1_subset_1(sK260(sK250,X0,X1),k1_zfmisc_1(k1_relat_1(sK253)))
| v4_waybel34(X1,sK250,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK253),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK253),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f89282,f68767]) ).
fof(f89674,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89481,f68773]) ).
fof(f89675,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0)
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f89482,f68776]) ).
fof(f89676,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f89483,f88154]) ).
fof(f89706,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89495,f68773]) ).
fof(f89844,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89674,f68770]) ).
fof(f89845,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f89675,f68772]) ).
fof(f89846,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f89676,f68772]) ).
fof(f89864,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(sK251)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89706,f68770]) ).
fof(f89960,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89844,f68769]) ).
fof(f89961,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0)
| v3_struct_0(sK251)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f89845,f68771]) ).
fof(f89962,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f89846,f68771]) ).
fof(f89964,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89864,f68769]) ).
fof(f90017,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89960,f68768]) ).
fof(f90018,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0)
| ~ l1_orders_2(sK251) ),
inference(forward_subsumption_resolution,[],[f89961,f68770]) ).
fof(f90019,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f89962,f68768]) ).
fof(f90021,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(sK250) ),
inference(forward_subsumption_resolution,[],[f89964,f68768]) ).
fof(f90091,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| r4_waybel_0(sK250,sK251,sK253,X0) ),
inference(forward_subsumption_resolution,[],[f90017,f68767]) ).
fof(f90092,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK251)))
| r4_waybel_0(sK251,sK252,sK254,X0) ),
inference(forward_subsumption_resolution,[],[f90018,f68769]) ).
fof(f90093,plain,
( v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54 ),
inference(forward_subsumption_resolution,[],[f90019,f68767]) ).
fof(f90095,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),u1_struct_0(sK251),u1_struct_0(X1),sK253,X2),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_subsumption_resolution,[],[f90021,f68767]) ).
fof(f90121,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ v1_finset_1(X0)
| r4_waybel_0(sK250,sK251,sK253,X0) ),
inference(forward_demodulation,[],[f90091,f88546]) ).
fof(f90122,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK254)))
| ~ v1_finset_1(X0)
| r4_waybel_0(sK251,sK252,sK254,X0) ),
inference(forward_demodulation,[],[f90092,f88544]) ).
fof(f90124,plain,
! [X2,X0,X1] :
( r4_waybel_0(sK250,X1,k7_funct_2(u1_struct_0(sK250),k1_relat_1(sK254),u1_struct_0(X1),sK253,X2),X0)
| ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_demodulation,[],[f90095,f88544]) ).
fof(f90168,plain,
! [X2,X0,X1] :
( r4_waybel_0(sK250,X1,k7_funct_2(k1_relat_1(sK253),k1_relat_1(sK254),u1_struct_0(X1),sK253,X2),X0)
| ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_demodulation,[],[f90124,f88546]) ).
fof(f90186,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_relat_1(sK254),u1_struct_0(X1))
| r4_waybel_0(sK250,X1,k7_funct_2(k1_relat_1(sK253),k1_relat_1(sK254),u1_struct_0(X1),sK253,X2),X0)
| ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(sK251),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_demodulation,[],[f90168,f88544]) ).
fof(f90209,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,k1_relat_1(sK254),u1_struct_0(X1))
| ~ v1_funct_2(X2,k1_relat_1(sK254),u1_struct_0(X1))
| r4_waybel_0(sK250,X1,k7_funct_2(k1_relat_1(sK253),k1_relat_1(sK254),u1_struct_0(X1),sK253,X2),X0)
| ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK250)))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_demodulation,[],[f90186,f88544]) ).
fof(f90224,plain,
! [X2,X0,X1] :
( r4_waybel_0(sK250,X1,k7_funct_2(k1_relat_1(sK253),k1_relat_1(sK254),u1_struct_0(X1),sK253,X2),X0)
| ~ m2_relset_1(X2,k1_relat_1(sK254),u1_struct_0(X1))
| ~ v1_funct_2(X2,k1_relat_1(sK254),u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,X1,X2,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(forward_demodulation,[],[f90209,f88546]) ).
fof(f90376,plain,
! [X0] :
( r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ v1_finset_1(k9_relat_1(sK253,X0)) ),
inference(resolution,[],[f90122,f88561]) ).
fof(f90657,definition,
( spl2054_202
<=> m1_subset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)),k1_zfmisc_1(k1_relat_1(sK253))) ),
introduced(definition,[new_symbols(definition,[spl2054_202])],[avatar_definition]) ).
fof(f90658,plain,
( m1_subset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)),k1_zfmisc_1(k1_relat_1(sK253)))
| ~ spl2054_202 ),
inference(avatar_component_clause,[],[f90657]) ).
fof(f90659,plain,
( ~ m1_subset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)),k1_zfmisc_1(k1_relat_1(sK253)))
| spl2054_202 ),
inference(avatar_component_clause,[],[f90657]) ).
fof(f91102,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ m2_relset_1(sK254,k1_relat_1(sK254),u1_struct_0(sK252))
| ~ v1_funct_2(sK254,k1_relat_1(sK254),u1_struct_0(sK252))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(sK254)
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252) )
| ~ spl2054_52 ),
inference(superposition,[],[f90224,f88608]) ).
fof(f91105,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ v1_funct_2(sK254,k1_relat_1(sK254),u1_struct_0(sK252))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(sK254)
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252) )
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f91102,f88549]) ).
fof(f91113,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_funct_1(sK254)
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252) )
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f91105,f88550]) ).
fof(f91121,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252) )
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f91113,f68778]) ).
fof(f91126,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ l1_orders_2(sK252) )
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f91121,f68772]) ).
fof(f91131,plain,
( ! [X0] :
( ~ r4_waybel_0(sK251,sK252,sK254,k9_relat_1(sK253,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ r4_waybel_0(sK250,sK251,sK253,X0) )
| ~ spl2054_52 ),
inference(forward_subsumption_resolution,[],[f91126,f68771]) ).
fof(f91138,plain,
( ! [X0] :
( r4_waybel_0(sK250,sK252,k5_relat_1(sK253,sK254),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK250,sK251,sK253,X0)
| ~ v1_finset_1(k9_relat_1(sK253,X0)) )
| ~ spl2054_52 ),
inference(resolution,[],[f91131,f90376]) ).
fof(f92097,plain,
( ~ m1_subset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)),k1_zfmisc_1(k1_relat_1(sK253)))
| ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ v1_funct_1(k5_relat_1(sK253,sK254))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52 ),
inference(resolution,[],[f91138,f68802]) ).
fof(f92780,plain,
( v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ v1_funct_1(k5_relat_1(sK253,sK254))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| spl2054_202 ),
inference(resolution,[],[f89556,f90659]) ).
fof(f92788,plain,
( ~ v1_funct_1(k5_relat_1(sK253,sK254))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| ~ spl2054_52
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92780,f88106]) ).
fof(f92789,plain,
( ~ v1_funct_2(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| ~ spl2054_52
| ~ spl2054_54
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92788,f88117]) ).
fof(f92790,plain,
( ~ m2_relset_1(k5_relat_1(sK253,sK254),k1_relat_1(sK253),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92789,f88664]) ).
fof(f92791,plain,
( v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92790,f88665]) ).
fof(f92792,plain,
( ~ l1_orders_2(sK252)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92791,f68772]) ).
fof(f92793,plain,
( $false
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92792,f68771]) ).
fof(f92794,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(avatar_contradiction_clause,[],[f92793]) ).
fof(f92795,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| v4_waybel34(k5_relat_1(sK253,sK254),sK250,sK252)
| ~ v1_funct_1(k5_relat_1(sK253,sK254))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92097,f90658]) ).
fof(f92796,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ v1_funct_1(k5_relat_1(sK253,sK254))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92795,f88106]) ).
fof(f92797,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ v1_funct_2(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92796,f88117]) ).
fof(f92798,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ m2_relset_1(k5_relat_1(sK253,sK254),u1_struct_0(sK250),u1_struct_0(sK252))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92797,f88153]) ).
fof(f92799,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| v3_struct_0(sK252)
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92798,f88154]) ).
fof(f92800,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ l1_orders_2(sK252)
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92799,f68772]) ).
fof(f92801,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| v3_struct_0(sK250)
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92800,f68771]) ).
fof(f92802,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ l1_orders_2(sK250)
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92801,f68768]) ).
fof(f92803,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92802,f68767]) ).
fof(f92805,definition,
( spl2054_242
<=> v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))) ),
introduced(definition,[new_symbols(definition,[spl2054_242])],[avatar_definition]) ).
fof(f92807,plain,
( ~ v1_finset_1(k9_relat_1(sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))))
| spl2054_242 ),
inference(avatar_component_clause,[],[f92805]) ).
fof(f92809,definition,
( spl2054_243
<=> r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254))) ),
introduced(definition,[new_symbols(definition,[spl2054_243])],[avatar_definition]) ).
fof(f92811,plain,
( ~ r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| spl2054_243 ),
inference(avatar_component_clause,[],[f92809]) ).
fof(f92812,plain,
( ~ spl2054_242
| ~ spl2054_243
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(avatar_split_clause,[],[f92803,f90657,f88115,f88099,f88096,f92809,f92805]) ).
fof(f92813,plain,
( ~ v1_relat_1(sK253)
| ~ v1_funct_1(sK253)
| ~ v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| spl2054_242 ),
inference(resolution,[],[f92807,f71776]) ).
fof(f92814,plain,
( ~ v1_funct_1(sK253)
| ~ v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| spl2054_242 ),
inference(forward_subsumption_resolution,[],[f92813,f88358]) ).
fof(f92815,plain,
( ~ v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| spl2054_242 ),
inference(forward_subsumption_resolution,[],[f92814,f68775]) ).
fof(f92816,plain,
( $false
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_242 ),
inference(forward_subsumption_resolution,[],[f92815,f90093]) ).
fof(f92817,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_242 ),
inference(avatar_contradiction_clause,[],[f92816]) ).
fof(f92819,plain,
( ~ v1_finset_1(sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ spl2054_202 ),
inference(resolution,[],[f90658,f90121]) ).
fof(f92824,plain,
( r4_waybel_0(sK250,sK251,sK253,sK260(sK250,sK252,k5_relat_1(sK253,sK254)))
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202 ),
inference(forward_subsumption_resolution,[],[f92819,f90093]) ).
fof(f92825,plain,
( $false
| ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202
| spl2054_243 ),
inference(forward_subsumption_resolution,[],[f92824,f92811]) ).
fof(f92826,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202
| spl2054_243 ),
inference(avatar_contradiction_clause,[],[f92825]) ).
cnf(s43,plain,
( spl2054_52
| spl2054_53 ),
inference(sat_conversion,[],[f88102]) ).
cnf(s44,plain,
( ~ spl2054_52
| spl2054_53
| spl2054_54 ),
inference(sat_conversion,[],[f88118]) ).
cnf(s45,plain,
~ spl2054_53,
inference(sat_conversion,[],[f88140]) ).
cnf(s200,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_202 ),
inference(sat_conversion,[],[f92794]) ).
cnf(s201,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202
| ~ spl2054_242
| ~ spl2054_243 ),
inference(sat_conversion,[],[f92812]) ).
cnf(s202,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| spl2054_242 ),
inference(sat_conversion,[],[f92817]) ).
cnf(s203,plain,
( ~ spl2054_52
| spl2054_53
| ~ spl2054_54
| ~ spl2054_202
| spl2054_243 ),
inference(sat_conversion,[],[f92826]) ).
cnf(s288,plain,
( ~ spl2054_52
| spl2054_54 ),
inference(rat,[],[s44,s45]) ).
cnf(s289,plain,
spl2054_52,
inference(rat,[],[s43,s45]) ).
cnf(s291,plain,
spl2054_54,
inference(rat,[],[s288,s289]) ).
cnf(s292,plain,
spl2054_242,
inference(rat,[],[s202,s289,s45,s291]) ).
cnf(s293,plain,
spl2054_202,
inference(rat,[],[s200,s289,s45,s291]) ).
cnf(s295,plain,
spl2054_243,
inference(rat,[],[s203,s291,s289,s45,s293]) ).
cnf(s296,plain,
$false,
inference(rat,[],[s201,s291,s292,s289,s45,s295,s293]) ).
fof(f92827,plain,
$false,
inference(avatar_sat_refutation,[],[s296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT378+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n018.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 15:13:09 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.43 Running first-order theorem proving
% 0.10/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.67/7.32 % (2483620)Detected formulas, will run a generic FOF schedule.
% 20.67/7.32 % (2483626)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=171041824:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2958 on theBenchmark for (2958ds/134677Mi)
% 20.67/7.32 % (2483625)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=1390977033:i=141193_2958 on theBenchmark for (2958ds/141193Mi)
% 20.67/7.32 % (2483627)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=213910129:i=141695:sd=1:nm=32:gsp=on:ss=included_2958 on theBenchmark for (2958ds/141695Mi)
% 20.67/7.32 % (2483628)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=984670151:i=109:sd=1:ins=1:gsp=on:ss=axioms_2958 on theBenchmark for (2958ds/109Mi)
% 20.67/7.32 % (2483631)dis-21_1_sil=8000:lcm=predicate:random_seed=3258315065: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)
% 20.67/7.32 % (2483629)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=322893037:i=119:av=off:ss=axioms_2958 on theBenchmark for (2958ds/119Mi)
% 20.67/7.32 % (2483630)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1370444402:s2a=on:i=139:gtg=position_2958 on theBenchmark for (2958ds/139Mi)
% 20.67/7.32 % (2483630)Instruction limit reached!
% 20.67/7.32 % (2483630)------------------------------
% 20.67/7.32 % (2483630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.67/7.32 % (2483630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.67/7.32 % (2483630)CaDiCaL version: 2.1.3
% 20.67/7.32 % (2483630)Termination reason: Instruction limit
% 20.67/7.32 % (2483630)Termination phase: Property scanning
% 20.67/7.32 % (2483630)Time elapsed: 0.066 s
% 20.67/7.32 % (2483630)Peak memory usage: 174 MB
% 20.67/7.32 % (2483630)Instructions burned: 140 (million)
% 20.67/7.32 % (2483628)Instruction limit reached!
% 20.67/7.32 % (2483628)------------------------------
% 20.67/7.32 % (2483628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.67/7.32 % (2483628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.67/7.32 % (2483628)CaDiCaL version: 2.1.3
% 20.67/7.32 % (2483628)Termination reason: Instruction limit
% 20.67/7.32 % (2483628)Termination phase: SInE selection
% 20.67/7.32 % (2483628)Time elapsed: 0.084 s
% 20.67/7.32 % (2483628)Peak memory usage: 173 MB
% 20.67/7.32 % (2483628)Instructions burned: 110 (million)
% 20.67/7.32 % (2483629)Instruction limit reached!
% 20.67/7.32 % (2483629)------------------------------
% 20.67/7.32 % (2483629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.67/7.32 % (2483629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.67/7.32 % (2483629)CaDiCaL version: 2.1.3
% 20.67/7.32 % (2483629)Termination reason: Instruction limit
% 20.67/7.32 % (2483629)Termination phase: SInE selection
% 20.67/7.32 % (2483629)Time elapsed: 0.085 s
% 20.67/7.32 % (2483629)Peak memory usage: 173 MB
% 20.67/7.32 % (2483629)Instructions burned: 119 (million)
% 20.67/7.32 % (2483631)Instruction limit reached!
% 20.67/7.32 % (2483631)------------------------------
% 20.67/7.32 % (2483631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.67/7.32 % (2483631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.67/7.32 % (2483631)CaDiCaL version: 2.1.3
% 20.67/7.32 % (2483631)Termination reason: Instruction limit
% 20.67/7.32 % (2483631)Termination phase: SInE selection
% 20.67/7.32 % (2483631)Time elapsed: 0.092 s
% 20.67/7.32 % (2483631)Peak memory usage: 173 MB
% 20.67/7.32 % (2483631)Instructions burned: 129 (million)
% 20.67/7.32 % (2483639)lrs+10_1_sil=8000:sp=occurrence:random_seed=3996046818:i=285:sd=3:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/285Mi)
% 20.67/7.32 % (2483640)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1967968524:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/157Mi)
% 20.67/7.32 % (2483642)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=3356928668:s2a=on:i=248:s2at=1.23:gtg=position_2955 on theBenchmark for (2955ds/248Mi)
% 20.67/7.32 % (2483641)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2635292959:i=325:sd=1:ss=axioms:sgt=32_2955 on theBenchmark for (2955ds/325Mi)
% 20.67/7.32 % (2483640)Instruction limit reached!
% 27.68/8.39 % (2483640)------------------------------
% 27.68/8.39 % (2483640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483640)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483640)Termination reason: Instruction limit
% 27.68/8.39 % (2483640)Termination phase: Property scanning
% 27.68/8.39 % (2483640)Time elapsed: 0.073 s
% 27.68/8.39 % (2483640)Peak memory usage: 174 MB
% 27.68/8.39 % (2483640)Instructions burned: 157 (million)
% 27.68/8.39 % (2483642)Instruction limit reached!
% 27.68/8.39 % (2483642)------------------------------
% 27.68/8.39 % (2483642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483642)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483642)Termination reason: Instruction limit
% 27.68/8.39 % (2483642)Termination phase: Property scanning
% 27.68/8.39 % (2483642)Time elapsed: 0.110 s
% 27.68/8.39 % (2483642)Peak memory usage: 174 MB
% 27.68/8.39 % (2483642)Instructions burned: 248 (million)
% 27.68/8.39 % (2483639)Instruction limit reached!
% 27.68/8.39 % (2483639)------------------------------
% 27.68/8.39 % (2483639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483639)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483639)Termination reason: Instruction limit
% 27.68/8.39 % (2483639)Termination phase: SInE selection
% 27.68/8.39 % (2483639)Time elapsed: 0.219 s
% 27.68/8.39 % (2483639)Peak memory usage: 174 MB
% 27.68/8.39 % (2483639)Instructions burned: 286 (million)
% 27.68/8.39 % (2483647)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3738388121:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2953 on theBenchmark for (2953ds/294Mi)
% 27.68/8.39 % (2483648)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=666522474:i=2350_2953 on theBenchmark for (2953ds/2350Mi)
% 27.68/8.39 % (2483641)Instruction limit reached!
% 27.68/8.39 % (2483641)------------------------------
% 27.68/8.39 % (2483641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483641)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483641)Termination reason: Instruction limit
% 27.68/8.39 % (2483641)Termination phase: SInE selection
% 27.68/8.39 % (2483641)Time elapsed: 0.249 s
% 27.68/8.39 % (2483641)Peak memory usage: 174 MB
% 27.68/8.39 % (2483641)Instructions burned: 326 (million)
% 27.68/8.39 % (2483650)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4171724388:cts=off:i=113:fsr=off:ss=included:sgt=4_2952 on theBenchmark for (2952ds/113Mi)
% 27.68/8.39 % (2483652)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2513815919:i=127:av=off:fsr=off:sup=off_2952 on theBenchmark for (2952ds/127Mi)
% 27.68/8.39 % (2483647)Instruction limit reached!
% 27.68/8.39 % (2483647)------------------------------
% 27.68/8.39 % (2483647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483647)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483647)Termination reason: Instruction limit
% 27.68/8.39 % (2483647)Termination phase: SInE selection
% 27.68/8.39 % (2483647)Time elapsed: 0.214 s
% 27.68/8.39 % (2483647)Peak memory usage: 174 MB
% 27.68/8.39 % (2483647)Instructions burned: 295 (million)
% 27.68/8.39 % (2483650)Instruction limit reached!
% 27.68/8.39 % (2483650)------------------------------
% 27.68/8.39 % (2483650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483650)CaDiCaL version: 2.1.3
% 27.68/8.39 % (2483650)Termination reason: Instruction limit
% 27.68/8.39 % (2483650)Termination phase: SInE selection
% 27.68/8.39 % (2483650)Time elapsed: 0.088 s
% 27.68/8.39 % (2483650)Peak memory usage: 173 MB
% 27.68/8.39 % (2483650)Instructions burned: 113 (million)
% 27.68/8.39 % (2483652)Instruction limit reached!
% 27.68/8.39 % (2483652)------------------------------
% 27.68/8.39 % (2483652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.68/8.39 % (2483652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.68/8.39 % (2483652)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483652)Termination reason: Instruction limit
% 68.57/14.10 % (2483652)Termination phase: Preprocessing 1
% 68.57/14.10 % (2483652)Time elapsed: 0.103 s
% 68.57/14.10 % (2483652)Peak memory usage: 175 MB
% 68.57/14.10 % (2483652)Instructions burned: 127 (million)
% 68.57/14.10 % (2483655)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2327445442:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2950 on theBenchmark for (2950ds/114Mi)
% 68.57/14.10 % (2483656)lrs+10_1_sil=8000:sp=occurrence:random_seed=960419632:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2950 on theBenchmark for (2950ds/907Mi)
% 68.57/14.10 % (2483655)Instruction limit reached!
% 68.57/14.10 % (2483655)------------------------------
% 68.57/14.10 % (2483655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.57/14.10 % (2483655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.57/14.10 % (2483655)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483655)Termination reason: Instruction limit
% 68.57/14.10 % (2483655)Termination phase: Property scanning
% 68.57/14.10 % (2483655)Time elapsed: 0.055 s
% 68.57/14.10 % (2483655)Peak memory usage: 174 MB
% 68.57/14.10 % (2483655)Instructions burned: 115 (million)
% 68.57/14.10 % (2483657)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=600652331:i=437:sd=1:aac=none:ss=included_2949 on theBenchmark for (2949ds/437Mi)
% 68.57/14.10 % (2483660)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2495335690:i=5202:ss=axioms:sgt=16_2948 on theBenchmark for (2948ds/5202Mi)
% 68.57/14.10 % (2483657)Instruction limit reached!
% 68.57/14.10 % (2483657)------------------------------
% 68.57/14.10 % (2483657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.57/14.10 % (2483657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.57/14.10 % (2483657)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483657)Termination reason: Instruction limit
% 68.57/14.10 % (2483657)Termination phase: Preprocessing 1
% 68.57/14.10 % (2483657)Time elapsed: 0.356 s
% 68.57/14.10 % (2483657)Peak memory usage: 175 MB
% 68.57/14.10 % (2483657)Instructions burned: 437 (million)
% 68.57/14.10 % (2483663)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3946480834:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2944 on theBenchmark for (2944ds/134Mi)
% 68.57/14.10 % (2483663)Instruction limit reached!
% 68.57/14.10 % (2483663)------------------------------
% 68.57/14.10 % (2483663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.57/14.10 % (2483663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.57/14.10 % (2483663)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483663)Termination reason: Instruction limit
% 68.57/14.10 % (2483663)Termination phase: SInE selection
% 68.57/14.10 % (2483663)Time elapsed: 0.107 s
% 68.57/14.10 % (2483663)Peak memory usage: 173 MB
% 68.57/14.10 % (2483663)Instructions burned: 135 (million)
% 68.57/14.10 % (2483656)Instruction limit reached!
% 68.57/14.10 % (2483656)------------------------------
% 68.57/14.10 % (2483656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.57/14.10 % (2483656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.57/14.10 % (2483656)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483656)Termination reason: Instruction limit
% 68.57/14.10 % (2483656)Termination phase: Preprocessing 3
% 68.57/14.10 % (2483656)Time elapsed: 0.702 s
% 68.57/14.10 % (2483656)Peak memory usage: 190 MB
% 68.57/14.10 % (2483656)Instructions burned: 908 (million)
% 68.57/14.10 % (2483665)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=869950725:st=8:i=592:sd=3:ep=RST:ss=axioms_2941 on theBenchmark for (2941ds/592Mi)
% 68.57/14.10 % (2483666)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3734499888:st=3:i=13193:sd=3:ss=axioms_2941 on theBenchmark for (2941ds/13193Mi)
% 68.57/14.10 % (2483665)Instruction limit reached!
% 68.57/14.10 % (2483665)------------------------------
% 68.57/14.10 % (2483665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.57/14.10 % (2483665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.57/14.10 % (2483665)CaDiCaL version: 2.1.3
% 68.57/14.10 % (2483665)Termination reason: Instruction limit
% 68.57/14.10 % (2483665)Termination phase: SInE selection
% 68.57/14.10 % (2483665)Time elapsed: 0.370 s
% 68.57/14.10 % (2483665)Peak memory usage: 175 MB
% 68.57/14.10 % (2483665)Instructions burned: 593 (million)
% 68.57/14.10 % (2483669)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=611668326:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2936 on theBenchmark for (2936ds/125Mi)
% 92.11/17.47 % (2483669)Instruction limit reached!
% 92.11/17.47 % (2483669)------------------------------
% 92.11/17.47 % (2483669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483669)CaDiCaL version: 2.1.3
% 92.11/17.47 % (2483669)Termination reason: Instruction limit
% 92.11/17.47 % (2483669)Termination phase: Property scanning
% 92.11/17.47 % (2483669)Time elapsed: 0.059 s
% 92.11/17.47 % (2483669)Peak memory usage: 174 MB
% 92.11/17.47 % (2483669)Instructions burned: 127 (million)
% 92.11/17.47 % (2483648)Instruction limit reached!
% 92.11/17.47 % (2483648)------------------------------
% 92.11/17.47 % (2483648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483648)CaDiCaL version: 2.1.3
% 92.11/17.47 % (2483648)Termination reason: Instruction limit
% 92.11/17.47 % (2483648)Termination phase: Preprocessing 3
% 92.11/17.47 % (2483648)Time elapsed: 1.779 s
% 92.11/17.47 % (2483648)Peak memory usage: 276 MB
% 92.11/17.47 % (2483648)Instructions burned: 2350 (million)
% 92.11/17.47 % (2483671)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=900676091:i=134:gtgl=5:slsql=off:gtg=exists_sym_2934 on theBenchmark for (2934ds/134Mi)
% 92.11/17.47 % (2483672)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4033933338:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2934 on theBenchmark for (2934ds/141Mi)
% 92.11/17.47 % (2483671)Instruction limit reached!
% 92.11/17.47 % (2483671)------------------------------
% 92.11/17.47 % (2483671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483671)CaDiCaL version: 2.1.3
% 92.11/17.47 % (2483671)Termination reason: Instruction limit
% 92.11/17.47 % (2483671)Termination phase: Property scanning
% 92.11/17.47 % (2483671)Time elapsed: 0.064 s
% 92.11/17.47 % (2483671)Peak memory usage: 174 MB
% 92.11/17.47 % (2483671)Instructions burned: 134 (million)
% 92.11/17.47 % (2483672)Instruction limit reached!
% 92.11/17.47 % (2483672)------------------------------
% 92.11/17.47 % (2483672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483672)CaDiCaL version: 2.1.3
% 92.11/17.47 % (2483672)Termination reason: Instruction limit
% 92.11/17.47 % (2483672)Termination phase: SInE selection
% 92.11/17.47 % (2483672)Time elapsed: 0.109 s
% 92.11/17.47 % (2483672)Peak memory usage: 173 MB
% 92.11/17.47 % (2483672)Instructions burned: 141 (million)
% 92.11/17.47 % (2483675)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=681033014:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2932 on theBenchmark for (2932ds/431Mi)
% 92.11/17.47 % (2483676)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=57238026:i=6060:aac=none:ins=25_2931 on theBenchmark for (2931ds/6060Mi)
% 92.11/17.47 % (2483675)Instruction limit reached!
% 92.11/17.47 % (2483675)------------------------------
% 92.11/17.47 % (2483675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483675)CaDiCaL version: 2.1.3
% 92.11/17.47 % (2483675)Termination reason: Instruction limit
% 92.11/17.47 % (2483675)Termination phase: Unused predicate definition removal
% 92.11/17.47 % (2483675)Time elapsed: 0.357 s
% 92.11/17.47 % (2483675)Peak memory usage: 177 MB
% 92.11/17.47 % (2483675)Instructions burned: 431 (million)
% 92.11/17.47 % (2483679)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=358633225:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2927 on theBenchmark for (2927ds/150Mi)
% 92.11/17.47 % (2483679)Instruction limit reached!
% 92.11/17.47 % (2483679)------------------------------
% 92.11/17.47 % (2483679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.11/17.47 % (2483679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.11/17.47 % (2483679)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483679)Termination reason: Instruction limit
% 64.64/22.51 % (2483679)Termination phase: SInE selection
% 64.64/22.51 % (2483679)Time elapsed: 0.120 s
% 64.64/22.51 % (2483679)Peak memory usage: 173 MB
% 64.64/22.51 % (2483679)Instructions burned: 150 (million)
% 64.64/22.51 % (2483681)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2234609885:i=14155:bd=all_2924 on theBenchmark for (2924ds/14155Mi)
% 64.64/22.51 % (2483660)Instruction limit reached!
% 64.64/22.51 % (2483660)------------------------------
% 64.64/22.51 % (2483660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483660)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483660)Termination reason: Instruction limit
% 64.64/22.51 % (2483660)Termination phase: Property scanning
% 64.64/22.51 % (2483660)Time elapsed: 3.328 s
% 64.64/22.51 % (2483660)Peak memory usage: 297 MB
% 64.64/22.51 % (2483660)Instructions burned: 5203 (million)
% 64.64/22.51 % (2483683)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1667417646:i=667:av=off:fsr=off_2913 on theBenchmark for (2913ds/667Mi)
% 64.64/22.51 % (2483683)Instruction limit reached!
% 64.64/22.51 % (2483683)------------------------------
% 64.64/22.51 % (2483683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483683)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483683)Termination reason: Instruction limit
% 64.64/22.51 % (2483683)Termination phase: Preprocessing 2
% 64.64/22.51 % (2483683)Time elapsed: 0.596 s
% 64.64/22.51 % (2483683)Peak memory usage: 214 MB
% 64.64/22.51 % (2483683)Instructions burned: 667 (million)
% 64.64/22.51 % (2483685)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=1693003339:s2a=on:i=185:s2at=1.8:fdi=4_2905 on theBenchmark for (2905ds/185Mi)
% 64.64/22.51 % (2483685)Instruction limit reached!
% 64.64/22.51 % (2483685)------------------------------
% 64.64/22.51 % (2483685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483685)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483685)Termination reason: Instruction limit
% 64.64/22.51 % (2483685)Termination phase: SInE selection
% 64.64/22.51 % (2483685)Time elapsed: 0.138 s
% 64.64/22.51 % (2483685)Peak memory usage: 173 MB
% 64.64/22.51 % (2483685)Instructions burned: 185 (million)
% 64.64/22.51 % (2483687)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1262935681:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2903 on theBenchmark for (2903ds/193Mi)
% 64.64/22.51 % (2483687)Instruction limit reached!
% 64.64/22.51 % (2483687)------------------------------
% 64.64/22.51 % (2483687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483687)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483687)Termination reason: Instruction limit
% 64.64/22.51 % (2483687)Termination phase: SInE selection
% 64.64/22.51 % (2483687)Time elapsed: 0.153 s
% 64.64/22.51 % (2483687)Peak memory usage: 173 MB
% 64.64/22.51 % (2483687)Instructions burned: 193 (million)
% 64.64/22.51 % (2483689)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1706449476:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2900 on theBenchmark for (2900ds/4850Mi)
% 64.64/22.51 % (2483676)Instruction limit reached!
% 64.64/22.51 % (2483676)------------------------------
% 64.64/22.51 % (2483676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483676)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483676)Termination reason: Instruction limit
% 64.64/22.51 % (2483676)Termination phase: NewCNF
% 64.64/22.51 % (2483676)Time elapsed: 4.836 s
% 64.64/22.51 % (2483676)Peak memory usage: 331 MB
% 64.64/22.51 % (2483676)Instructions burned: 6061 (million)
% 64.64/22.51 % (2483691)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3375022126:i=12111:sd=1:ss=included_2881 on theBenchmark for (2881ds/12111Mi)
% 64.64/22.51 % (2483689)Instruction limit reached!
% 64.64/22.51 % (2483689)------------------------------
% 64.64/22.51 % (2483689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483689)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483689)Termination reason: Instruction limit
% 64.64/22.51 % (2483689)Termination phase: Function definition elimination
% 64.64/22.51 % (2483689)Time elapsed: 3.113 s
% 64.64/22.51 % (2483689)Peak memory usage: 295 MB
% 64.64/22.51 % (2483689)Instructions burned: 4851 (million)
% 64.64/22.51 % (2483693)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2055416270:i=319:kws=precedence:fsr=off_2867 on theBenchmark for (2867ds/319Mi)
% 64.64/22.51 % (2483693)Instruction limit reached!
% 64.64/22.51 % (2483693)------------------------------
% 64.64/22.51 % (2483693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483693)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483693)Termination reason: Instruction limit
% 64.64/22.51 % (2483693)Termination phase: Preprocessing 1
% 64.64/22.51 % (2483693)Time elapsed: 0.234 s
% 64.64/22.51 % (2483693)Peak memory usage: 175 MB
% 64.64/22.51 % (2483693)Instructions burned: 321 (million)
% 64.64/22.51 % (2483695)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=747577125:i=2064:ep=RST_2863 on theBenchmark for (2863ds/2064Mi)
% 64.64/22.51 % (2483666)Instruction limit reached!
% 64.64/22.51 % (2483666)------------------------------
% 64.64/22.51 % (2483666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483666)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483666)Termination reason: Instruction limit
% 64.64/22.51 % (2483666)Termination phase: Saturation
% 64.64/22.51 % (2483666)Time elapsed: 8.032 s
% 64.64/22.51 % (2483666)Peak memory usage: 419 MB
% 64.64/22.51 % (2483666)Instructions burned: 13193 (million)
% 64.64/22.51 % (2483697)dis-1011_128_sil=32000:random_seed=2736830446:i=3706:ep=RST:av=off_2859 on theBenchmark for (2859ds/3706Mi)
% 64.64/22.51 % (2483695)Instruction limit reached!
% 64.64/22.51 % (2483695)------------------------------
% 64.64/22.51 % (2483695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483695)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483695)Termination reason: Instruction limit
% 64.64/22.51 % (2483695)Termination phase: Preprocessing 3
% 64.64/22.51 % (2483695)Time elapsed: 1.524 s
% 64.64/22.51 % (2483695)Peak memory usage: 281 MB
% 64.64/22.51 % (2483695)Instructions burned: 2064 (million)
% 64.64/22.51 % (2483681)Instruction limit reached!
% 64.64/22.51 % (2483681)------------------------------
% 64.64/22.51 % (2483681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483681)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483681)Termination reason: Instruction limit
% 64.64/22.51 % (2483681)Termination phase: Saturation
% 64.64/22.51 % (2483681)Time elapsed: 7.657 s
% 64.64/22.51 % (2483681)Peak memory usage: 735 MB
% 64.64/22.51 % (2483681)Instructions burned: 14155 (million)
% 64.64/22.51 % (2483699)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3739891672:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2846 on theBenchmark for (2846ds/757Mi)
% 64.64/22.51 % (2483700)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=990082421:i=13913:ss=axioms:sgt=8_2845 on theBenchmark for (2845ds/13913Mi)
% 64.64/22.51 % (2483699)Refutation not found, incomplete strategy
% 64.64/22.51 % (2483699)------------------------------
% 64.64/22.51 % (2483699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483699)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483699)Termination reason: Refutation not found, incomplete strategy
% 64.64/22.51 % (2483699)Time elapsed: 0.733 s
% 64.64/22.51 % (2483699)Peak memory usage: 181 MB
% 64.64/22.51 % (2483699)Instructions burned: 498 (million)
% 64.64/22.51 % (2483699)------------------------------
% 64.64/22.51 % (2483699)------------------------------
% 64.64/22.51 % (2483697)Instruction limit reached!
% 64.64/22.51 % (2483697)------------------------------
% 64.64/22.51 % (2483697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483697)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483697)Termination reason: Instruction limit
% 64.64/22.51 % (2483697)Termination phase: Property scanning
% 64.64/22.51 % (2483697)Time elapsed: 2.418 s
% 64.64/22.51 % (2483697)Peak memory usage: 339 MB
% 64.64/22.51 % (2483697)Instructions burned: 3709 (million)
% 64.64/22.51 % (2483703)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2830377257:i=9925:aac=none_2835 on theBenchmark for (2835ds/9925Mi)
% 64.64/22.51 % (2483705)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=759217589:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2833 on theBenchmark for (2833ds/2479Mi)
% 64.64/22.51 % (2483705)Refutation not found, incomplete strategy
% 64.64/22.51 % (2483705)------------------------------
% 64.64/22.51 % (2483705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483705)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483705)Termination reason: Refutation not found, incomplete strategy
% 64.64/22.51 % (2483705)Time elapsed: 0.753 s
% 64.64/22.51 % (2483705)Peak memory usage: 181 MB
% 64.64/22.51 % (2483705)Instructions burned: 1005 (million)
% 64.64/22.51 % (2483705)------------------------------
% 64.64/22.51 % (2483705)------------------------------
% 64.64/22.51 % (2483707)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3019351583:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2821 on theBenchmark for (2821ds/440Mi)
% 64.64/22.51 % (2483707)Instruction limit reached!
% 64.64/22.51 % (2483707)------------------------------
% 64.64/22.51 % (2483707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483707)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483707)Termination reason: Instruction limit
% 64.64/22.51 % (2483707)Termination phase: Property scanning
% 64.64/22.51 % (2483707)Time elapsed: 0.194 s
% 64.64/22.51 % (2483707)Peak memory usage: 174 MB
% 64.64/22.51 % (2483707)Instructions burned: 442 (million)
% 64.64/22.51 % (2483709)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1374053918:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2818 on theBenchmark for (2818ds/11145Mi)
% 64.64/22.51 % (2483691)Instruction limit reached!
% 64.64/22.51 % (2483691)------------------------------
% 64.64/22.51 % (2483691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.64/22.51 % (2483691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.64/22.51 % (2483691)CaDiCaL version: 2.1.3
% 64.64/22.51 % (2483691)Termination reason: Instruction limit
% 64.64/22.51 % (2483691)Termination phase: Saturation
% 64.64/22.51 % (2483691)Time elapsed: 7.746 s
% 64.64/22.51 % (2483691)Peak memory usage: 311 MB
% 64.64/22.51 % (2483691)Instructions burned: 12112 (million)
% 64.64/22.51 % (2483711)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=3896457172:cts=off:i=3034:av=off:er=known:fsd=on_2802 on theBenchmark for (2802ds/3034Mi)
% 64.64/22.51 % (2483700)First to succeed.
% 64.64/22.51 % (2483700)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2483620"
% 64.64/22.51 % (2483700)Refutation found. Thanks to Tanya!
% 64.64/22.51 % SZS status Theorem for theBenchmark
% 64.64/22.51 % SZS output start Proof for theBenchmark
% See solution above
% 128.01/22.72 % (2483700)------------------------------
% 128.01/22.72 % (2483700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.01/22.72 % (2483700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.01/22.72 % (2483700)CaDiCaL version: 2.1.3
% 128.01/22.72 % (2483700)Termination reason: Refutation
% 128.01/22.72 % (2483700)Time elapsed: 5.645 s
% 128.01/22.72 % (2483700)Peak memory usage: 361 MB
% 128.01/22.72 % (2483700)Instructions burned: 9394 (million)
% 128.01/22.72 % (2483700)------------------------------
% 128.01/22.72 % (2483700)------------------------------
% 128.01/22.72 % (2483620)Success in time 21.637 s
% 128.01/22.72 % Vampire exiting
%------------------------------------------------------------------------------