%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT379+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 57.09s 17.53s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 24
% Syntax : Number of formulae : 216 ( 40 unt; 6 def)
% Number of atoms : 1053 ( 57 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1386 ( 549 ~; 711 |; 82 &)
% ( 15 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 7 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-3 aty)
% Number of variables : 250 ( 0 sgn 238 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f71,axiom,
! [X0] : r1_tarski(k1_xboole_0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_xboole_1) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f486,axiom,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset_1) ).
fof(f2691,axiom,
! [X0,X1] :
( ~ v1_xboole_0(k2_tarski(X0,X1))
& v1_finset_1(k2_tarski(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_finset_1) ).
fof(f2722,axiom,
! [X0,X1] :
( ( r1_tarski(X0,X1)
& v1_finset_1(X1) )
=> v1_finset_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_finset_1) ).
fof(f3551,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f5537,axiom,
! [X0] :
( ~ v1_xboole_0(k1_tarski(X0))
& v1_finset_1(k1_tarski(X0))
& v1_realset1(k1_tarski(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_realset1) ).
fof(f6436,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k2_struct_0(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_struct_0) ).
fof(f6438,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k2_struct_0(X0,X1,X2) = k2_tarski(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_struct_0) ).
fof(f6787,axiom,
! [X0] :
( l1_struct_0(X0)
=> k1_pre_topc(X0) = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_pre_topc) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f7062,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/sandbox2/benchmark/theBenchmark.p',t51_tops_2) ).
fof(f7885,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f15015,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)) )
=> ( v20_waybel_0(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d35_waybel_0) ).
fof(f19000,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/sandbox2/benchmark/theBenchmark.p',d15_waybel34) ).
fof(f19001,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)) )
=> ( v5_waybel34(X2,X0,X1)
<=> r4_waybel_0(X0,X1,X2,k1_pre_topc(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_waybel34) ).
fof(f19014,conjecture,
! [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)
=> ( v20_waybel_0(X2,X0,X1)
& v5_waybel34(X2,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_waybel34) ).
fof(f19015,negated_conjecture,
~ ! [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)
=> ( v20_waybel_0(X2,X0,X1)
& v5_waybel34(X2,X0,X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f19014]) ).
fof(f19127,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v20_waybel_0(X2,X0,X1)
| ~ v5_waybel34(X2,X0,X1) )
& 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(ennf_transformation,[],[f19015]) ).
fof(f19128,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v20_waybel_0(X2,X0,X1)
| ~ v5_waybel34(X2,X0,X1) )
& 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(flattening,[],[f19127]) ).
fof(f19143,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,[],[f19000]) ).
fof(f19144,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,[],[f19143]) ).
fof(f19151,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v5_waybel34(X2,X0,X1)
<=> r4_waybel_0(X0,X1,X2,k1_pre_topc(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,[],[f19001]) ).
fof(f19152,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v5_waybel34(X2,X0,X1)
<=> r4_waybel_0(X0,X1,X2,k1_pre_topc(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,[],[f19151]) ).
fof(f19344,plain,
! [X0,X1] :
( v1_finset_1(X0)
| ~ r1_tarski(X0,X1)
| ~ v1_finset_1(X1) ),
inference(ennf_transformation,[],[f2722]) ).
fof(f19345,plain,
! [X0,X1] :
( v1_finset_1(X0)
| ~ r1_tarski(X0,X1)
| ~ v1_finset_1(X1) ),
inference(flattening,[],[f19344]) ).
fof(f19366,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v20_waybel_0(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,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,[],[f15015]) ).
fof(f19367,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v20_waybel_0(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,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,[],[f19366]) ).
fof(f19421,plain,
! [X0] :
( k1_pre_topc(X0) = k1_xboole_0
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6787]) ).
fof(f20035,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7885]) ).
fof(f20117,plain,
! [X0,X1,X2] :
( k2_struct_0(X0,X1,X2) = k2_tarski(X1,X2)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6438]) ).
fof(f20118,plain,
! [X0,X1,X2] :
( k2_struct_0(X0,X1,X2) = k2_tarski(X1,X2)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f20117]) ).
fof(f20121,plain,
! [X0,X1,X2] :
( m1_subset_1(k2_struct_0(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6436]) ).
fof(f20122,plain,
! [X0,X1,X2] :
( m1_subset_1(k2_struct_0(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f20121]) ).
fof(f20400,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,[],[f7062]) ).
fof(f20401,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,[],[f20400]) ).
fof(f20422,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f24132,plain,
( ( ~ v20_waybel_0(sK164,sK162,sK163)
| ~ v5_waybel34(sK164,sK162,sK163) )
& v4_waybel34(sK164,sK162,sK163)
& v1_funct_1(sK164)
& v1_funct_2(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
& m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
& ~ v3_struct_0(sK163)
& l1_orders_2(sK163)
& ~ v3_struct_0(sK162)
& l1_orders_2(sK162) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK162,sK163,sK164]),skolemize(X0,sK162),skolemize(X1,sK163),skolemize(X2,sK164)],[f19128]) ).
fof(f24143,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,[],[f19144]) ).
fof(f24144,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,[],[f24143]) ).
fof(f24145,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_waybel34(X2,X0,X1)
| ( ~ r4_waybel_0(X0,X1,X2,sK172(X0,X1,X2))
& v1_finset_1(sK172(X0,X1,X2))
& m1_subset_1(sK172(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,[sK172]),skolemize(X3,sK172(X0,X1,X2))],[f24144]) ).
fof(f24150,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v5_waybel34(X2,X0,X1)
| ~ r4_waybel_0(X0,X1,X2,k1_pre_topc(X0)) )
& ( r4_waybel_0(X0,X1,X2,k1_pre_topc(X0))
| ~ v5_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,[],[f19152]) ).
fof(f24240,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v20_waybel_0(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( ~ r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v20_waybel_0(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,[],[f19367]) ).
fof(f24241,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v20_waybel_0(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( ~ r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X3,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X5,X6))
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v20_waybel_0(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,[],[f24240]) ).
fof(f24242,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v20_waybel_0(X2,X0,X1)
| ( ~ r4_waybel_0(X0,X1,X2,k2_struct_0(X0,sK230(X0,X1,X2),sK231(X0,X1,X2)))
& m1_subset_1(sK231(X0,X1,X2),u1_struct_0(X0))
& m1_subset_1(sK230(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( r4_waybel_0(X0,X1,X2,k2_struct_0(X0,X5,X6))
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v20_waybel_0(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,[sK230,sK231]),skolemize(X3,sK230(X0,X1,X2)),skolemize(X4,sK231(X0,X1,X2))],[f24241]) ).
fof(f26014,plain,
l1_orders_2(sK162),
inference(cnf_transformation,[],[f24132]) ).
fof(f26015,plain,
~ v3_struct_0(sK162),
inference(cnf_transformation,[],[f24132]) ).
fof(f26016,plain,
l1_orders_2(sK163),
inference(cnf_transformation,[],[f24132]) ).
fof(f26017,plain,
~ v3_struct_0(sK163),
inference(cnf_transformation,[],[f24132]) ).
fof(f26018,plain,
m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163)),
inference(cnf_transformation,[],[f24132]) ).
fof(f26019,plain,
v1_funct_2(sK164,u1_struct_0(sK162),u1_struct_0(sK163)),
inference(cnf_transformation,[],[f24132]) ).
fof(f26020,plain,
v1_funct_1(sK164),
inference(cnf_transformation,[],[f24132]) ).
fof(f26021,plain,
v4_waybel34(sK164,sK162,sK163),
inference(cnf_transformation,[],[f24132]) ).
fof(f26022,plain,
( ~ v20_waybel_0(sK164,sK162,sK163)
| ~ v5_waybel34(sK164,sK162,sK163) ),
inference(cnf_transformation,[],[f24132]) ).
fof(f26058,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,[],[f24145]) ).
fof(f26080,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(X0,X1,X2,k1_pre_topc(X0))
| v5_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,[],[f24150]) ).
fof(f26412,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| v1_finset_1(X0)
| ~ v1_finset_1(X1) ),
inference(cnf_transformation,[],[f19345]) ).
fof(f26453,plain,
! [X2,X0,X1] :
( m1_subset_1(sK230(X0,X1,X2),u1_struct_0(X0))
| v20_waybel_0(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,[],[f24242]) ).
fof(f26454,plain,
! [X2,X0,X1] :
( m1_subset_1(sK231(X0,X1,X2),u1_struct_0(X0))
| v20_waybel_0(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,[],[f24242]) ).
fof(f26455,plain,
! [X2,X0,X1] :
( ~ r4_waybel_0(X0,X1,X2,k2_struct_0(X0,sK230(X0,X1,X2),sK231(X0,X1,X2)))
| v20_waybel_0(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,[],[f24242]) ).
fof(f26536,plain,
! [X0] :
( k1_xboole_0 = k1_pre_topc(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f19421]) ).
fof(f26642,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f486]) ).
fof(f26644,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(cnf_transformation,[],[f71]) ).
fof(f27651,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20035]) ).
fof(f27768,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,X2) = k2_struct_0(X0,X1,X2) ),
inference(cnf_transformation,[],[f20118]) ).
fof(f27770,plain,
! [X2,X0,X1] :
( m1_subset_1(k2_struct_0(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f20122]) ).
fof(f28168,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,[],[f20401]) ).
fof(f28203,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f20422]) ).
fof(f29588,plain,
! [X0,X1] : v1_finset_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f2691]) ).
fof(f29648,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f29650,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f30555,plain,
! [X0] : v1_finset_1(k1_tarski(X0)),
inference(cnf_transformation,[],[f5537]) ).
fof(f32342,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3551]) ).
fof(f33975,plain,
! [X0] :
( ~ l1_struct_0(X0)
| np__0 = k1_pre_topc(X0) ),
inference(definition_unfolding,[],[f26536,f32342]) ).
fof(f34011,plain,
! [X0] : m1_subset_1(np__0,k1_zfmisc_1(X0)),
inference(definition_unfolding,[],[f26642,f32342]) ).
fof(f34013,plain,
! [X0] : r1_tarski(np__0,X0),
inference(definition_unfolding,[],[f26644,f32342]) ).
fof(f34697,plain,
! [X0] : v1_finset_1(k2_tarski(X0,X0)),
inference(definition_unfolding,[],[f30555,f29648]) ).
fof(f36406,definition,
( spl1192_17
<=> v5_waybel34(sK164,sK162,sK163) ),
introduced(definition,[new_symbols(definition,[spl1192_17])],[avatar_definition]) ).
fof(f36410,definition,
( spl1192_18
<=> v20_waybel_0(sK164,sK162,sK163) ),
introduced(definition,[new_symbols(definition,[spl1192_18])],[avatar_definition]) ).
fof(f36412,plain,
( ~ v20_waybel_0(sK164,sK162,sK163)
| spl1192_18 ),
inference(avatar_component_clause,[],[f36410]) ).
fof(f36413,plain,
( ~ spl1192_17
| ~ spl1192_18 ),
inference(avatar_split_clause,[],[f26022,f36410,f36406]) ).
fof(f36804,plain,
l1_struct_0(sK162),
inference(resolution,[],[f27651,f26014]) ).
fof(f36805,plain,
l1_struct_0(sK163),
inference(resolution,[],[f27651,f26016]) ).
fof(f36806,plain,
u1_struct_0(sK162) = k2_pre_topc(sK162),
inference(resolution,[],[f36804,f28203]) ).
fof(f36965,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| ~ v4_waybel34(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| r4_waybel_0(sK162,sK163,sK164,X0)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(resolution,[],[f26058,f26019]) ).
fof(f36973,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| ~ v1_funct_1(sK164)
| r4_waybel_0(sK162,sK163,sK164,X0)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36965,f26021]) ).
fof(f36975,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| r4_waybel_0(sK162,sK163,sK164,X0)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36973,f26020]) ).
fof(f36977,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| r4_waybel_0(sK162,sK163,sK164,X0)
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36975,f26018]) ).
fof(f36978,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| r4_waybel_0(sK162,sK163,sK164,X0)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36977,f26017]) ).
fof(f36979,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| r4_waybel_0(sK162,sK163,sK164,X0)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36978,f26016]) ).
fof(f36980,plain,
! [X0] :
( ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| r4_waybel_0(sK162,sK163,sK164,X0)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f36979,f26015]) ).
fof(f36981,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK162)))
| ~ v1_finset_1(X0)
| r4_waybel_0(sK162,sK163,sK164,X0) ),
inference(forward_subsumption_resolution,[],[f36980,f26014]) ).
fof(f36982,plain,
( ~ v1_funct_1(sK164)
| k2_pre_topc(sK162) = k1_relat_1(sK164)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_struct_0(sK163)
| ~ l1_struct_0(sK162) ),
inference(resolution,[],[f28168,f26019]) ).
fof(f36990,plain,
( k2_pre_topc(sK162) = k1_relat_1(sK164)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_struct_0(sK163)
| ~ l1_struct_0(sK162) ),
inference(forward_subsumption_resolution,[],[f36982,f26020]) ).
fof(f36992,plain,
( k2_pre_topc(sK162) = k1_relat_1(sK164)
| v3_struct_0(sK163)
| ~ l1_struct_0(sK163)
| ~ l1_struct_0(sK162) ),
inference(forward_subsumption_resolution,[],[f36990,f26018]) ).
fof(f36994,plain,
( k2_pre_topc(sK162) = k1_relat_1(sK164)
| ~ l1_struct_0(sK163)
| ~ l1_struct_0(sK162) ),
inference(forward_subsumption_resolution,[],[f36992,f26017]) ).
fof(f36995,plain,
( k2_pre_topc(sK162) = k1_relat_1(sK164)
| ~ l1_struct_0(sK162) ),
inference(forward_subsumption_resolution,[],[f36994,f36805]) ).
fof(f36996,plain,
k2_pre_topc(sK162) = k1_relat_1(sK164),
inference(forward_subsumption_resolution,[],[f36995,f36804]) ).
fof(f36998,plain,
u1_struct_0(sK162) = k1_relat_1(sK164),
inference(superposition,[],[f36806,f36996]) ).
fof(f36999,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_relat_1(sK164)))
| ~ v1_finset_1(X0)
| r4_waybel_0(sK162,sK163,sK164,X0) ),
inference(superposition,[],[f36981,f36998]) ).
fof(f37001,plain,
m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163)),
inference(superposition,[],[f26018,f36998]) ).
fof(f37002,plain,
v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163)),
inference(superposition,[],[f26019,f36998]) ).
fof(f37009,plain,
! [X0,X1] :
( m1_subset_1(sK230(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(superposition,[],[f26453,f36998]) ).
fof(f37010,plain,
! [X0,X1] :
( m1_subset_1(sK231(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(superposition,[],[f26454,f36998]) ).
fof(f37031,plain,
! [X0,X1] :
( m1_subset_1(sK231(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f37010,f26015]) ).
fof(f37032,plain,
! [X0,X1] :
( m1_subset_1(sK230(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f37009,f26015]) ).
fof(f37045,plain,
! [X0,X1] :
( m1_subset_1(sK231(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f37031,f26014]) ).
fof(f37046,plain,
! [X0,X1] :
( m1_subset_1(sK230(sK162,X0,X1),k1_relat_1(sK164))
| v20_waybel_0(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f37032,f26014]) ).
fof(f37072,plain,
np__0 = k1_pre_topc(sK162),
inference(resolution,[],[f33975,f36804]) ).
fof(f37074,plain,
! [X0,X1] :
( ~ r4_waybel_0(sK162,X0,X1,np__0)
| v5_waybel34(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK162),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK162),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162) ),
inference(superposition,[],[f26080,f37072]) ).
fof(f37075,plain,
! [X0,X1] :
( ~ r4_waybel_0(sK162,X0,X1,np__0)
| v5_waybel34(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK162),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK162),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK162) ),
inference(forward_subsumption_resolution,[],[f37074,f26015]) ).
fof(f37076,plain,
! [X0,X1] :
( ~ r4_waybel_0(sK162,X0,X1,np__0)
| v5_waybel34(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK162),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK162),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f37075,f26014]) ).
fof(f37077,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ r4_waybel_0(sK162,X0,X1,np__0)
| v5_waybel34(X1,sK162,X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK162),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f37076,f36998]) ).
fof(f37078,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_relat_1(sK164),u1_struct_0(X0))
| ~ r4_waybel_0(sK162,X0,X1,np__0)
| v5_waybel34(X1,sK162,X0)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f37077,f36998]) ).
fof(f37099,plain,
( ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| v5_waybel34(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163) ),
inference(resolution,[],[f37078,f37002]) ).
fof(f37104,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| v5_waybel34(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163) ),
inference(forward_subsumption_resolution,[],[f37099,f37001]) ).
fof(f37106,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| v5_waybel34(sK164,sK162,sK163)
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163) ),
inference(forward_subsumption_resolution,[],[f37104,f26020]) ).
fof(f37107,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| v5_waybel34(sK164,sK162,sK163)
| ~ l1_orders_2(sK163) ),
inference(forward_subsumption_resolution,[],[f37106,f26017]) ).
fof(f37108,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| v5_waybel34(sK164,sK162,sK163) ),
inference(forward_subsumption_resolution,[],[f37107,f26016]) ).
fof(f37110,definition,
( spl1192_45
<=> r4_waybel_0(sK162,sK163,sK164,np__0) ),
introduced(definition,[new_symbols(definition,[spl1192_45])],[avatar_definition]) ).
fof(f37112,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,np__0)
| spl1192_45 ),
inference(avatar_component_clause,[],[f37110]) ).
fof(f37113,plain,
( spl1192_17
| ~ spl1192_45 ),
inference(avatar_split_clause,[],[f37108,f37110,f36406]) ).
fof(f37117,plain,
! [X2,X3,X0,X1] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK231(X0,X2,X3)) = k2_struct_0(X0,X1,sK231(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f27768,f26454]) ).
fof(f37118,plain,
! [X2,X3,X0,X1] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK230(X0,X2,X3)) = k2_struct_0(X0,X1,sK230(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f27768,f26453]) ).
fof(f37122,plain,
! [X2,X3,X0,X1] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK230(X0,X2,X3)) = k2_struct_0(X0,X1,sK230(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X0) ),
inference(duplicate_literal_removal,[],[f37118]) ).
fof(f37123,plain,
! [X2,X3,X0,X1] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK231(X0,X2,X3)) = k2_struct_0(X0,X1,sK231(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X0) ),
inference(duplicate_literal_removal,[],[f37117]) ).
fof(f37125,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK230(X0,X2,X3)) = k2_struct_0(X0,X1,sK230(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| v3_struct_0(X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f37122,f27651]) ).
fof(f37126,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_tarski(X1,sK231(X0,X2,X3)) = k2_struct_0(X0,X1,sK231(X0,X2,X3))
| v20_waybel_0(X3,X0,X2)
| ~ v1_funct_1(X3)
| v3_struct_0(X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f37123,f27651]) ).
fof(f37128,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| v20_waybel_0(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) ),
inference(resolution,[],[f37126,f26019]) ).
fof(f37140,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| ~ v1_funct_1(sK164)
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37128,f36412]) ).
fof(f37144,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37140,f26020]) ).
fof(f37146,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37144,f26015]) ).
fof(f37147,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37146,f26018]) ).
fof(f37148,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37147,f26017]) ).
fof(f37149,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164))
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37148,f26016]) ).
fof(f37150,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164)) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37149,f26014]) ).
fof(f37151,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_relat_1(sK164))
| k2_tarski(X0,sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK231(sK162,sK163,sK164)) )
| spl1192_18 ),
inference(forward_demodulation,[],[f37150,f36998]) ).
fof(f37152,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| v20_waybel_0(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) ),
inference(resolution,[],[f37125,f26019]) ).
fof(f37164,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| ~ v1_funct_1(sK164)
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37152,f36412]) ).
fof(f37168,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| v3_struct_0(sK162)
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37164,f26020]) ).
fof(f37170,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37168,f26015]) ).
fof(f37171,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37170,f26018]) ).
fof(f37172,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| ~ l1_orders_2(sK163)
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37171,f26017]) ).
fof(f37173,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164))
| ~ l1_orders_2(sK162) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37172,f26016]) ).
fof(f37174,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK162))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164)) )
| spl1192_18 ),
inference(forward_subsumption_resolution,[],[f37173,f26014]) ).
fof(f37175,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_relat_1(sK164))
| k2_tarski(X0,sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,X0,sK230(sK162,sK163,sK164)) )
| spl1192_18 ),
inference(forward_demodulation,[],[f37174,f36998]) ).
fof(f37652,definition,
( spl1192_61
<=> m1_subset_1(sK230(sK162,sK163,sK164),k1_relat_1(sK164)) ),
introduced(definition,[new_symbols(definition,[spl1192_61])],[avatar_definition]) ).
fof(f37653,plain,
( m1_subset_1(sK230(sK162,sK163,sK164),k1_relat_1(sK164))
| ~ spl1192_61 ),
inference(avatar_component_clause,[],[f37652]) ).
fof(f37654,plain,
( ~ m1_subset_1(sK230(sK162,sK163,sK164),k1_relat_1(sK164))
| spl1192_61 ),
inference(avatar_component_clause,[],[f37652]) ).
fof(f37667,definition,
( spl1192_63
<=> m1_subset_1(sK231(sK162,sK163,sK164),k1_relat_1(sK164)) ),
introduced(definition,[new_symbols(definition,[spl1192_63])],[avatar_definition]) ).
fof(f37668,plain,
( m1_subset_1(sK231(sK162,sK163,sK164),k1_relat_1(sK164))
| ~ spl1192_63 ),
inference(avatar_component_clause,[],[f37667]) ).
fof(f37669,plain,
( ~ m1_subset_1(sK231(sK162,sK163,sK164),k1_relat_1(sK164))
| spl1192_63 ),
inference(avatar_component_clause,[],[f37667]) ).
fof(f38611,plain,
( ~ v1_finset_1(np__0)
| r4_waybel_0(sK162,sK163,sK164,np__0) ),
inference(resolution,[],[f34011,f36981]) ).
fof(f38614,plain,
( ~ v1_finset_1(np__0)
| spl1192_45 ),
inference(forward_subsumption_resolution,[],[f38611,f37112]) ).
fof(f38629,plain,
( v20_waybel_0(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_63 ),
inference(resolution,[],[f37045,f37669]) ).
fof(f38636,plain,
( ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38629,f36412]) ).
fof(f38637,plain,
( ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38636,f26020]) ).
fof(f38638,plain,
( ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38637,f37002]) ).
fof(f38639,plain,
( v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38638,f37001]) ).
fof(f38640,plain,
( ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38639,f26017]) ).
fof(f38641,plain,
( $false
| spl1192_18
| spl1192_63 ),
inference(forward_subsumption_resolution,[],[f38640,f26016]) ).
fof(f38642,plain,
( spl1192_18
| spl1192_63 ),
inference(avatar_contradiction_clause,[],[f38641]) ).
fof(f38651,plain,
( k2_tarski(sK231(sK162,sK163,sK164),sK230(sK162,sK163,sK164)) = k2_struct_0(sK162,sK231(sK162,sK163,sK164),sK230(sK162,sK163,sK164))
| spl1192_18
| ~ spl1192_63 ),
inference(resolution,[],[f37668,f37175]) ).
fof(f38655,plain,
( k2_struct_0(sK162,sK231(sK162,sK163,sK164),sK230(sK162,sK163,sK164)) = k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_demodulation,[],[f38651,f29650]) ).
fof(f38770,plain,
( v20_waybel_0(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_61 ),
inference(resolution,[],[f37046,f37654]) ).
fof(f38776,plain,
( ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38770,f36412]) ).
fof(f38777,plain,
( ~ v1_funct_2(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38776,f26020]) ).
fof(f38778,plain,
( ~ m2_relset_1(sK164,k1_relat_1(sK164),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38777,f37002]) ).
fof(f38779,plain,
( v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38778,f37001]) ).
fof(f38780,plain,
( ~ l1_orders_2(sK163)
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38779,f26017]) ).
fof(f38781,plain,
( $false
| spl1192_18
| spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38780,f26016]) ).
fof(f38782,plain,
( spl1192_18
| spl1192_61 ),
inference(avatar_contradiction_clause,[],[f38781]) ).
fof(f38797,plain,
( k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)) = k2_struct_0(sK162,sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164))
| spl1192_18
| ~ spl1192_61 ),
inference(resolution,[],[f37653,f37151]) ).
fof(f38821,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| v20_waybel_0(sK164,sK162,sK163)
| ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(superposition,[],[f26455,f38797]) ).
fof(f38824,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| ~ v1_funct_1(sK164)
| ~ v1_funct_2(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38821,f36412]) ).
fof(f38826,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| ~ v1_funct_2(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38824,f26020]) ).
fof(f38828,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| ~ m2_relset_1(sK164,u1_struct_0(sK162),u1_struct_0(sK163))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38826,f26019]) ).
fof(f38830,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| v3_struct_0(sK163)
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38828,f26018]) ).
fof(f38832,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| ~ l1_orders_2(sK163)
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38830,f26017]) ).
fof(f38834,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| v3_struct_0(sK162)
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38832,f26016]) ).
fof(f38836,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| ~ l1_orders_2(sK162)
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38834,f26015]) ).
fof(f38838,plain,
( ~ r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| spl1192_18
| ~ spl1192_61 ),
inference(forward_subsumption_resolution,[],[f38836,f26014]) ).
fof(f40491,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(u1_struct_0(sK162)))
| v3_struct_0(sK162)
| ~ l1_struct_0(sK162)
| ~ m1_subset_1(sK231(sK162,sK163,sK164),u1_struct_0(sK162))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(superposition,[],[f27770,f38655]) ).
fof(f40502,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(u1_struct_0(sK162)))
| ~ l1_struct_0(sK162)
| ~ m1_subset_1(sK231(sK162,sK163,sK164),u1_struct_0(sK162))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40491,f26015]) ).
fof(f40521,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(u1_struct_0(sK162)))
| ~ m1_subset_1(sK231(sK162,sK163,sK164),u1_struct_0(sK162))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40502,f36804]) ).
fof(f40536,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(k1_relat_1(sK164)))
| ~ m1_subset_1(sK231(sK162,sK163,sK164),u1_struct_0(sK162))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_demodulation,[],[f40521,f36998]) ).
fof(f40550,plain,
( ~ m1_subset_1(sK231(sK162,sK163,sK164),k1_relat_1(sK164))
| m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(k1_relat_1(sK164)))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_demodulation,[],[f40536,f36998]) ).
fof(f40563,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(k1_relat_1(sK164)))
| ~ m1_subset_1(sK230(sK162,sK163,sK164),u1_struct_0(sK162))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40550,f37668]) ).
fof(f40573,plain,
( ~ m1_subset_1(sK230(sK162,sK163,sK164),k1_relat_1(sK164))
| m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(k1_relat_1(sK164)))
| spl1192_18
| ~ spl1192_63 ),
inference(forward_demodulation,[],[f40563,f36998]) ).
fof(f40583,plain,
( m1_subset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)),k1_zfmisc_1(k1_relat_1(sK164)))
| spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40573,f37653]) ).
fof(f40593,plain,
( ~ v1_finset_1(k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(resolution,[],[f40583,f36999]) ).
fof(f40620,plain,
( r4_waybel_0(sK162,sK163,sK164,k2_tarski(sK230(sK162,sK163,sK164),sK231(sK162,sK163,sK164)))
| spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40593,f29588]) ).
fof(f40621,plain,
( $false
| spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(forward_subsumption_resolution,[],[f40620,f38838]) ).
fof(f40622,plain,
( spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(avatar_contradiction_clause,[],[f40621]) ).
fof(f60218,plain,
! [X0] :
( v1_finset_1(np__0)
| ~ v1_finset_1(X0) ),
inference(resolution,[],[f26412,f34013]) ).
fof(f60223,definition,
( spl1192_617
<=> ! [X0] : ~ v1_finset_1(X0) ),
introduced(definition,[new_symbols(definition,[spl1192_617])],[avatar_definition]) ).
fof(f60224,plain,
( ! [X0] : ~ v1_finset_1(X0)
| ~ spl1192_617 ),
inference(avatar_component_clause,[],[f60223]) ).
fof(f60235,plain,
( ! [X0] : ~ v1_finset_1(X0)
| spl1192_45 ),
inference(forward_subsumption_resolution,[],[f60218,f38614]) ).
fof(f60270,plain,
( spl1192_617
| spl1192_45 ),
inference(avatar_split_clause,[],[f60235,f37110,f60223]) ).
fof(f60289,plain,
( $false
| ~ spl1192_617 ),
inference(resolution,[],[f60224,f34697]) ).
fof(f60297,plain,
~ spl1192_617,
inference(avatar_contradiction_clause,[],[f60289]) ).
cnf(s19,plain,
( ~ spl1192_17
| ~ spl1192_18 ),
inference(sat_conversion,[],[f36413]) ).
cnf(s40,plain,
( spl1192_17
| ~ spl1192_45 ),
inference(sat_conversion,[],[f37113]) ).
cnf(s62,plain,
( spl1192_18
| spl1192_63 ),
inference(sat_conversion,[],[f38642]) ).
cnf(s66,plain,
( spl1192_18
| spl1192_61 ),
inference(sat_conversion,[],[f38782]) ).
cnf(s77,plain,
( spl1192_18
| ~ spl1192_61
| ~ spl1192_63 ),
inference(sat_conversion,[],[f40622]) ).
cnf(s552,plain,
( spl1192_45
| spl1192_617 ),
inference(sat_conversion,[],[f60270]) ).
cnf(s556,plain,
~ spl1192_617,
inference(sat_conversion,[],[f60297]) ).
cnf(s557,plain,
spl1192_45,
inference(rat,[],[s552,s556]) ).
cnf(s606,plain,
spl1192_17,
inference(rat,[],[s40,s557]) ).
cnf(s622,plain,
~ spl1192_18,
inference(rat,[],[s19,s606]) ).
cnf(s623,plain,
spl1192_61,
inference(rat,[],[s66,s622]) ).
cnf(s624,plain,
spl1192_63,
inference(rat,[],[s62,s622]) ).
cnf(s625,plain,
$false,
inference(rat,[],[s77,s622,s624,s623]) ).
fof(f60298,plain,
$false,
inference(avatar_sat_refutation,[],[s625]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT379+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 15:11:34 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.65/3.77 % (2527834)Detected formulas, will run a generic FOF schedule.
% 13.65/3.77 % (2527845)dis-21_1_sil=8000:lcm=predicate:random_seed=3675474557:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 13.65/3.77 % (2527842)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3902499556:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 13.65/3.77 % (2527844)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2420643453:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 13.65/3.77 % (2527840)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=3420225274:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 13.65/3.77 % (2527839)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=584624391:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 13.65/3.77 % (2527841)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=3304269332:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 13.65/3.77 % (2527843)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=566197125:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 13.65/3.77 % (2527845)Instruction limit reached!
% 13.65/3.77 % (2527845)------------------------------
% 13.65/3.77 % (2527845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/3.77 % (2527845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/3.77 % (2527845)CaDiCaL version: 2.1.3
% 13.65/3.77 % (2527845)Termination reason: Instruction limit
% 13.65/3.77 % (2527845)Termination phase: SInE selection
% 13.65/3.77 % (2527845)Time elapsed: 0.051 s
% 13.65/3.77 % (2527845)Peak memory usage: 112 MB
% 13.65/3.77 % (2527845)Instructions burned: 130 (million)
% 13.65/3.77 % (2527844)Instruction limit reached!
% 13.65/3.77 % (2527844)------------------------------
% 13.65/3.77 % (2527844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/3.77 % (2527844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/3.77 % (2527844)CaDiCaL version: 2.1.3
% 13.65/3.77 % (2527844)Termination reason: Instruction limit
% 13.65/3.77 % (2527844)Termination phase: Property scanning
% 13.65/3.77 % (2527844)Time elapsed: 0.060 s
% 13.65/3.77 % (2527844)Peak memory usage: 112 MB
% 13.65/3.77 % (2527844)Instructions burned: 140 (million)
% 13.65/3.77 % (2527842)Instruction limit reached!
% 13.65/3.77 % (2527842)------------------------------
% 13.65/3.77 % (2527842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/3.77 % (2527842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/3.77 % (2527842)CaDiCaL version: 2.1.3
% 13.65/3.77 % (2527842)Termination reason: Instruction limit
% 13.65/3.77 % (2527842)Termination phase: SInE selection
% 13.65/3.77 % (2527842)Time elapsed: 0.087 s
% 13.65/3.77 % (2527842)Peak memory usage: 112 MB
% 13.65/3.77 % (2527842)Instructions burned: 110 (million)
% 13.65/3.77 % (2527843)Instruction limit reached!
% 13.65/3.77 % (2527843)------------------------------
% 13.65/3.77 % (2527843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/3.77 % (2527843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/3.77 % (2527843)CaDiCaL version: 2.1.3
% 13.65/3.77 % (2527843)Termination reason: Instruction limit
% 13.65/3.77 % (2527843)Termination phase: SInE selection
% 13.65/3.77 % (2527843)Time elapsed: 0.096 s
% 13.65/3.77 % (2527843)Peak memory usage: 112 MB
% 13.65/3.77 % (2527843)Instructions burned: 120 (million)
% 13.65/3.77 % (2527853)lrs+10_1_sil=8000:sp=occurrence:random_seed=3042993081:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 13.65/3.77 % (2527854)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4196425400:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 13.65/3.77 % (2527853)Instruction limit reached!
% 13.65/3.77 % (2527853)------------------------------
% 13.65/3.77 % (2527853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/3.77 % (2527853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/3.77 % (2527853)CaDiCaL version: 2.1.3
% 13.65/3.77 % (2527853)Termination reason: Instruction limit
% 19.78/4.69 % (2527853)Termination phase: Saturation
% 19.78/4.69 % (2527853)Time elapsed: 0.114 s
% 19.78/4.69 % (2527853)Peak memory usage: 119 MB
% 19.78/4.69 % (2527853)Instructions burned: 286 (million)
% 19.78/4.69 % (2527855)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2190378082:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 19.78/4.69 % (2527856)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=357736599:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 19.78/4.69 % (2527854)Instruction limit reached!
% 19.78/4.69 % (2527854)------------------------------
% 19.78/4.69 % (2527854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/4.69 % (2527854)CaDiCaL version: 2.1.3
% 19.78/4.69 % (2527854)Termination reason: Instruction limit
% 19.78/4.69 % (2527854)Termination phase: Property scanning
% 19.78/4.69 % (2527854)Time elapsed: 0.068 s
% 19.78/4.69 % (2527854)Peak memory usage: 112 MB
% 19.78/4.69 % (2527854)Instructions burned: 157 (million)
% 19.78/4.69 % (2527859)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3057644660:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 19.78/4.69 % (2527855)Refutation not found, incomplete strategy
% 19.78/4.69 % (2527855)------------------------------
% 19.78/4.69 % (2527855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/4.69 % (2527855)CaDiCaL version: 2.1.3
% 19.78/4.69 % (2527855)Termination reason: Refutation not found, incomplete strategy
% 19.78/4.69 % (2527855)Time elapsed: 0.111 s
% 19.78/4.69 % (2527855)Peak memory usage: 117 MB
% 19.78/4.69 % (2527855)Instructions burned: 121 (million)
% 19.78/4.69 % (2527856)Instruction limit reached!
% 19.78/4.69 % (2527856)------------------------------
% 19.78/4.69 % (2527856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/4.69 % (2527856)CaDiCaL version: 2.1.3
% 19.78/4.69 % (2527856)Termination reason: Instruction limit
% 19.78/4.69 % (2527856)Termination phase: Property scanning
% 19.78/4.69 % (2527856)Time elapsed: 0.110 s
% 19.78/4.69 % (2527856)Peak memory usage: 112 MB
% 19.78/4.69 % (2527856)Instructions burned: 250 (million)
% 19.78/4.69 % (2527862)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3525258843:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 19.78/4.69 % (2527859)Instruction limit reached!
% 19.78/4.69 % (2527859)------------------------------
% 19.78/4.69 % (2527859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/4.69 % (2527859)CaDiCaL version: 2.1.3
% 19.78/4.69 % (2527859)Termination reason: Instruction limit
% 19.78/4.69 % (2527859)Termination phase: Property scanning
% 19.78/4.69 % (2527859)Time elapsed: 0.118 s
% 19.78/4.69 % (2527859)Peak memory usage: 118 MB
% 19.78/4.69 % (2527859)Instructions burned: 297 (million)
% 19.78/4.69 % (2527864)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2988850654:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 19.78/4.69 % (2527866)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3463528355:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 19.78/4.69 % (2527855)------------------------------
% 19.78/4.69 % (2527855)------------------------------
% 19.78/4.69 % (2527864)Instruction limit reached!
% 19.78/4.69 % (2527864)------------------------------
% 19.78/4.69 % (2527864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/4.69 % (2527864)CaDiCaL version: 2.1.3
% 19.78/4.69 % (2527864)Termination reason: Instruction limit
% 19.78/4.69 % (2527864)Termination phase: SInE selection
% 19.78/4.69 % (2527864)Time elapsed: 0.093 s
% 19.78/4.69 % (2527864)Peak memory usage: 112 MB
% 19.78/4.69 % (2527864)Instructions burned: 113 (million)
% 19.78/4.69 % (2527866)Instruction limit reached!
% 19.78/4.69 % (2527866)------------------------------
% 19.78/4.69 % (2527866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/4.69 % (2527866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527866)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527866)Termination reason: Instruction limit
% 40.72/7.59 % (2527866)Termination phase: Preprocessing 1
% 40.72/7.59 % (2527866)Time elapsed: 0.054 s
% 40.72/7.59 % (2527866)Peak memory usage: 113 MB
% 40.72/7.59 % (2527866)Instructions burned: 127 (million)
% 40.72/7.59 % (2527869)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3816624524:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 40.72/7.59 % (2527871)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1297266829:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 40.72/7.59 % (2527870)lrs+10_1_sil=8000:sp=occurrence:random_seed=285722870:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 40.72/7.59 % (2527869)Instruction limit reached!
% 40.72/7.59 % (2527869)------------------------------
% 40.72/7.59 % (2527869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/7.59 % (2527869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527869)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527869)Termination reason: Instruction limit
% 40.72/7.59 % (2527869)Termination phase: Property scanning
% 40.72/7.59 % (2527869)Time elapsed: 0.049 s
% 40.72/7.59 % (2527869)Peak memory usage: 112 MB
% 40.72/7.59 % (2527869)Instructions burned: 115 (million)
% 40.72/7.59 % (2527871)Instruction limit reached!
% 40.72/7.59 % (2527871)------------------------------
% 40.72/7.59 % (2527871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/7.59 % (2527871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527871)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527871)Termination reason: Instruction limit
% 40.72/7.59 % (2527871)Termination phase: Saturation
% 40.72/7.59 % (2527871)Time elapsed: 0.153 s
% 40.72/7.59 % (2527871)Peak memory usage: 123 MB
% 40.72/7.59 % (2527871)Instructions burned: 438 (million)
% 40.72/7.59 % (2527875)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=426321493:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 40.72/7.59 % (2527876)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1453206026:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 40.72/7.59 % (2527876)Instruction limit reached!
% 40.72/7.59 % (2527876)------------------------------
% 40.72/7.59 % (2527876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/7.59 % (2527876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527876)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527876)Termination reason: Instruction limit
% 40.72/7.59 % (2527876)Termination phase: Unused predicate definition removal
% 40.72/7.59 % (2527876)Time elapsed: 0.070 s
% 40.72/7.59 % (2527876)Peak memory usage: 114 MB
% 40.72/7.59 % (2527876)Instructions burned: 134 (million)
% 40.72/7.59 % (2527879)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3088372656:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 40.72/7.59 % (2527870)Instruction limit reached!
% 40.72/7.59 % (2527870)------------------------------
% 40.72/7.59 % (2527870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/7.59 % (2527870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527870)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527870)Termination reason: Instruction limit
% 40.72/7.59 % (2527870)Termination phase: Saturation
% 40.72/7.59 % (2527870)Time elapsed: 0.552 s
% 40.72/7.59 % (2527870)Peak memory usage: 131 MB
% 40.72/7.59 % (2527870)Instructions burned: 909 (million)
% 40.72/7.59 % (2527881)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=721641423:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 40.72/7.59 % (2527879)Instruction limit reached!
% 40.72/7.59 % (2527879)------------------------------
% 40.72/7.59 % (2527879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/7.59 % (2527879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/7.59 % (2527879)CaDiCaL version: 2.1.3
% 40.72/7.59 % (2527879)Termination reason: Instruction limit
% 40.72/7.59 % (2527879)Termination phase: Preprocessing 3
% 40.72/7.59 % (2527879)Time elapsed: 0.261 s
% 40.72/7.59 % (2527879)Peak memory usage: 133 MB
% 40.72/7.59 % (2527879)Instructions burned: 593 (million)
% 40.72/7.59 % (2527883)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=74739003:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 75.55/12.49 % (2527883)Instruction limit reached!
% 75.55/12.49 % (2527883)------------------------------
% 75.55/12.49 % (2527883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.49 % (2527883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.49 % (2527883)CaDiCaL version: 2.1.3
% 75.55/12.49 % (2527883)Termination reason: Instruction limit
% 75.55/12.49 % (2527883)Termination phase: Property scanning
% 75.55/12.49 % (2527883)Time elapsed: 0.030 s
% 75.55/12.49 % (2527883)Peak memory usage: 112 MB
% 75.55/12.49 % (2527883)Instructions burned: 128 (million)
% 75.55/12.49 % (2527862)Instruction limit reached!
% 75.55/12.49 % (2527862)------------------------------
% 75.55/12.49 % (2527862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.49 % (2527862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.49 % (2527862)CaDiCaL version: 2.1.3
% 75.55/12.49 % (2527862)Termination reason: Instruction limit
% 75.55/12.49 % (2527862)Termination phase: Property scanning
% 75.55/12.49 % (2527862)Time elapsed: 1.260 s
% 75.55/12.49 % (2527862)Peak memory usage: 171 MB
% 75.55/12.49 % (2527862)Instructions burned: 2351 (million)
% 75.55/12.49 % (2527885)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1771582229:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 75.55/12.49 % (2527885)Instruction limit reached!
% 75.55/12.49 % (2527885)------------------------------
% 75.55/12.49 % (2527885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.49 % (2527885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.49 % (2527885)CaDiCaL version: 2.1.3
% 75.55/12.49 % (2527885)Termination reason: Instruction limit
% 75.55/12.49 % (2527885)Termination phase: Property scanning
% 75.55/12.49 % (2527885)Time elapsed: 0.032 s
% 75.55/12.49 % (2527885)Peak memory usage: 112 MB
% 75.55/12.49 % (2527885)Instructions burned: 138 (million)
% 75.55/12.49 % (2527886)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2610227601:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 75.55/12.49 % (2527888)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4135742017:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 75.55/12.49 % (2527886)Refutation not found, incomplete strategy
% 75.55/12.49 % (2527886)------------------------------
% 75.55/12.49 % (2527886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.49 % (2527886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.49 % (2527886)CaDiCaL version: 2.1.3
% 75.55/12.49 % (2527886)Termination reason: Refutation not found, incomplete strategy
% 75.55/12.49 % (2527886)Time elapsed: 0.109 s
% 75.55/12.49 % (2527886)Peak memory usage: 117 MB
% 75.55/12.49 % (2527886)Instructions burned: 122 (million)
% 75.55/12.49 % (2527888)Refutation not found, incomplete strategy
% 75.55/12.49 % (2527888)------------------------------
% 75.55/12.49 % (2527888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.49 % (2527888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.49 % (2527888)CaDiCaL version: 2.1.3
% 75.55/12.49 % (2527888)Termination reason: Refutation not found, incomplete strategy
% 75.55/12.49 % (2527888)Time elapsed: 0.063 s
% 75.55/12.49 % (2527888)Peak memory usage: 117 MB
% 75.55/12.49 % (2527888)Instructions burned: 120 (million)
% 75.55/12.49 % (2527888)------------------------------
% 75.55/12.49 % (2527888)------------------------------
% 75.55/12.49 % (2527886)------------------------------
% 75.55/12.49 % (2527886)------------------------------
% 75.55/12.49 % (2527891)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=433087091:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 75.55/12.49 % (2527892)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=1104646423:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2964 on theBenchmark for (2964ds/150Mi)
% 75.55/12.49 % (2527892)Instruction limit reached!
% 75.55/12.49 % (2527892)------------------------------
% 57.09/17.53 % (2527892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527892)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527892)Termination reason: Instruction limit
% 57.09/17.53 % (2527892)Termination phase: Preprocessing 1
% 57.09/17.53 % (2527892)Time elapsed: 0.133 s
% 57.09/17.53 % (2527892)Peak memory usage: 113 MB
% 57.09/17.53 % (2527892)Instructions burned: 150 (million)
% 57.09/17.53 % (2527895)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=894122116:i=14155:bd=all_2961 on theBenchmark for (2961ds/14155Mi)
% 57.09/17.53 % (2527875)Instruction limit reached!
% 57.09/17.53 % (2527875)------------------------------
% 57.09/17.53 % (2527875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527875)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527875)Termination reason: Instruction limit
% 57.09/17.53 % (2527875)Termination phase: Saturation
% 57.09/17.53 % (2527875)Time elapsed: 3.211 s
% 57.09/17.53 % (2527875)Peak memory usage: 258 MB
% 57.09/17.53 % (2527875)Instructions burned: 5203 (million)
% 57.09/17.53 % (2527897)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3285554211:i=667:av=off:fsr=off_2944 on theBenchmark for (2944ds/667Mi)
% 57.09/17.53 % (2527897)Instruction limit reached!
% 57.09/17.53 % (2527897)------------------------------
% 57.09/17.53 % (2527897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527897)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527897)Termination reason: Instruction limit
% 57.09/17.53 % (2527897)Termination phase: NewCNF
% 57.09/17.53 % (2527897)Time elapsed: 0.533 s
% 57.09/17.53 % (2527897)Peak memory usage: 149 MB
% 57.09/17.53 % (2527897)Instructions burned: 667 (million)
% 57.09/17.53 % (2527891)Instruction limit reached!
% 57.09/17.53 % (2527891)------------------------------
% 57.09/17.53 % (2527891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527891)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527891)Termination reason: Instruction limit
% 57.09/17.53 % (2527891)Termination phase: Saturation
% 57.09/17.53 % (2527891)Time elapsed: 2.725 s
% 57.09/17.53 % (2527891)Peak memory usage: 586 MB
% 57.09/17.53 % (2527891)Instructions burned: 6060 (million)
% 57.09/17.53 % (2527899)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=2354910693:s2a=on:i=185:s2at=1.8:fdi=4_2937 on theBenchmark for (2937ds/185Mi)
% 57.09/17.53 % (2527900)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2330543325:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2936 on theBenchmark for (2936ds/193Mi)
% 57.09/17.53 % (2527899)Instruction limit reached!
% 57.09/17.53 % (2527899)------------------------------
% 57.09/17.53 % (2527899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527899)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527899)Termination reason: Instruction limit
% 57.09/17.53 % (2527899)Termination phase: SInE selection
% 57.09/17.53 % (2527899)Time elapsed: 0.154 s
% 57.09/17.53 % (2527899)Peak memory usage: 113 MB
% 57.09/17.53 % (2527899)Instructions burned: 185 (million)
% 57.09/17.53 % (2527900)Instruction limit reached!
% 57.09/17.53 % (2527900)------------------------------
% 57.09/17.53 % (2527900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527900)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527900)Termination reason: Instruction limit
% 57.09/17.53 % (2527900)Termination phase: SInE selection
% 57.09/17.53 % (2527900)Time elapsed: 0.094 s
% 57.09/17.53 % (2527900)Peak memory usage: 112 MB
% 57.09/17.53 % (2527900)Instructions burned: 193 (million)
% 57.09/17.53 % (2527904)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4203043033:i=12111:sd=1:ss=included_2934 on theBenchmark for (2934ds/12111Mi)
% 57.09/17.53 % (2527903)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4243981318:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2934 on theBenchmark for (2934ds/4850Mi)
% 57.09/17.53 % (2527903)Instruction limit reached!
% 57.09/17.53 % (2527903)------------------------------
% 57.09/17.53 % (2527903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527903)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527903)Termination reason: Instruction limit
% 57.09/17.53 % (2527903)Termination phase: Function definition elimination
% 57.09/17.53 % (2527903)Time elapsed: 2.200 s
% 57.09/17.53 % (2527903)Peak memory usage: 161 MB
% 57.09/17.53 % (2527903)Instructions burned: 4853 (million)
% 57.09/17.53 % (2527907)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3580143231:i=319:kws=precedence:fsr=off_2910 on theBenchmark for (2910ds/319Mi)
% 57.09/17.53 % (2527907)Instruction limit reached!
% 57.09/17.53 % (2527907)------------------------------
% 57.09/17.53 % (2527907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527907)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527907)Termination reason: Instruction limit
% 57.09/17.53 % (2527907)Termination phase: Naming
% 57.09/17.53 % (2527907)Time elapsed: 0.263 s
% 57.09/17.53 % (2527907)Peak memory usage: 135 MB
% 57.09/17.53 % (2527907)Instructions burned: 319 (million)
% 57.09/17.53 % (2527910)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3134709418:i=2064:ep=RST_2905 on theBenchmark for (2905ds/2064Mi)
% 57.09/17.53 % (2527910)Instruction limit reached!
% 57.09/17.53 % (2527910)------------------------------
% 57.09/17.53 % (2527910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527910)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527910)Termination reason: Instruction limit
% 57.09/17.53 % (2527910)Termination phase: Property scanning
% 57.09/17.53 % (2527910)Time elapsed: 1.098 s
% 57.09/17.53 % (2527910)Peak memory usage: 171 MB
% 57.09/17.53 % (2527910)Instructions burned: 2065 (million)
% 57.09/17.53 % (2527881)Instruction limit reached!
% 57.09/17.53 % (2527881)------------------------------
% 57.09/17.53 % (2527881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527881)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527881)Termination reason: Instruction limit
% 57.09/17.53 % (2527881)Termination phase: Saturation
% 57.09/17.53 % (2527881)Time elapsed: 8.013 s
% 57.09/17.53 % (2527881)Peak memory usage: 285 MB
% 57.09/17.53 % (2527881)Instructions burned: 13194 (million)
% 57.09/17.53 % (2528458)dis-1011_128_sil=32000:random_seed=3829554224:i=3706:ep=RST:av=off_2893 on theBenchmark for (2893ds/3706Mi)
% 57.09/17.53 % (2528540)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3161972144:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2891 on theBenchmark for (2891ds/757Mi)
% 57.09/17.53 % (2527904)Instruction limit reached!
% 57.09/17.53 % (2527904)------------------------------
% 57.09/17.53 % (2527904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527904)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527904)Termination reason: Instruction limit
% 57.09/17.53 % (2527904)Termination phase: Saturation
% 57.09/17.53 % (2527904)Time elapsed: 4.344 s
% 57.09/17.53 % (2527904)Peak memory usage: 251 MB
% 57.09/17.53 % (2527904)Instructions burned: 12113 (million)
% 57.09/17.53 % (2528646)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1305434950:i=13913:ss=axioms:sgt=8_2889 on theBenchmark for (2889ds/13913Mi)
% 57.09/17.53 % (2528540)Instruction limit reached!
% 57.09/17.53 % (2528540)------------------------------
% 57.09/17.53 % (2528540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2528540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2528540)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2528540)Termination reason: Instruction limit
% 57.09/17.53 % (2528540)Termination phase: Saturation
% 57.09/17.53 % (2528540)Time elapsed: 0.495 s
% 57.09/17.53 % (2528540)Peak memory usage: 128 MB
% 57.09/17.53 % (2528540)Instructions burned: 757 (million)
% 57.09/17.53 % (2528735)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2515714541:i=9925:aac=none_2885 on theBenchmark for (2885ds/9925Mi)
% 57.09/17.53 % (2528458)Instruction limit reached!
% 57.09/17.53 % (2528458)------------------------------
% 57.09/17.53 % (2528458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2528458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2528458)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2528458)Termination reason: Instruction limit
% 57.09/17.53 % (2528458)Termination phase: Saturation
% 57.09/17.53 % (2528458)Time elapsed: 2.773 s
% 57.09/17.53 % (2528458)Peak memory usage: 186 MB
% 57.09/17.53 % (2528458)Instructions burned: 3706 (million)
% 57.09/17.53 % (2528768)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1915852808:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2863 on theBenchmark for (2863ds/2479Mi)
% 57.09/17.53 % (2528768)Refutation not found, incomplete strategy
% 57.09/17.53 % (2528768)------------------------------
% 57.09/17.53 % (2528768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2528768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2528768)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2528768)Termination reason: Refutation not found, incomplete strategy
% 57.09/17.53 % (2528768)Time elapsed: 0.412 s
% 57.09/17.53 % (2528768)Peak memory usage: 119 MB
% 57.09/17.53 % (2528768)Instructions burned: 347 (million)
% 57.09/17.53 % (2528768)------------------------------
% 57.09/17.53 % (2528768)------------------------------
% 57.09/17.53 % (2528770)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2221404767:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2852 on theBenchmark for (2852ds/440Mi)
% 57.09/17.53 % (2528770)Instruction limit reached!
% 57.09/17.53 % (2528770)------------------------------
% 57.09/17.53 % (2528770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2528770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2528770)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2528770)Termination reason: Instruction limit
% 57.09/17.53 % (2528770)Termination phase: Property scanning
% 57.09/17.53 % (2528770)Time elapsed: 0.371 s
% 57.09/17.53 % (2528770)Peak memory usage: 112 MB
% 57.09/17.53 % (2528770)Instructions burned: 440 (million)
% 57.09/17.53 % (2527895)Instruction limit reached!
% 57.09/17.53 % (2527895)------------------------------
% 57.09/17.53 % (2527895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.09/17.53 % (2527895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.09/17.53 % (2527895)CaDiCaL version: 2.1.3
% 57.09/17.53 % (2527895)Termination reason: Instruction limit
% 57.09/17.53 % (2527895)Termination phase: Saturation
% 57.09/17.53 % (2527895)Time elapsed: 11.480 s
% 57.09/17.53 % (2527895)Peak memory usage: 519 MB
% 57.09/17.53 % (2527895)Instructions burned: 14155 (million)
% 57.09/17.53 % (2528772)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=240366990:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2845 on theBenchmark for (2845ds/11145Mi)
% 57.09/17.53 % (2528773)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=2469548971:cts=off:i=3034:av=off:er=known:fsd=on_2844 on theBenchmark for (2844ds/3034Mi)
% 57.09/17.53 % (2528646)First to succeed.
% 57.09/17.53 % (2528646)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2527834"
% 57.09/17.53 % (2528646)Refutation found. Thanks to Tanya!
% 57.09/17.53 % SZS status Theorem for theBenchmark
% 57.09/17.53 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/17.81 % (2528646)------------------------------
% 0.16/17.81 % (2528646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/17.81 % (2528646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/17.81 % (2528646)CaDiCaL version: 2.1.3
% 0.16/17.81 % (2528646)Termination reason: Refutation
% 0.16/17.81 % (2528646)Time elapsed: 5.086 s
% 0.16/17.81 % (2528646)Peak memory usage: 253 MB
% 0.16/17.81 % (2528646)Instructions burned: 8992 (million)
% 0.16/17.81 % (2528646)------------------------------
% 0.16/17.81 % (2528646)------------------------------
% 0.16/17.81 % (2527834)Success in time 16.68 s
% 0.16/17.81 % Vampire exiting
%------------------------------------------------------------------------------