%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP046+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 : n007.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 02:34:05 PM UTC 2026
% Result : Theorem 62.46s 22.08s
% Output : Refutation 141.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 28
% Syntax : Number of formulae : 300 ( 46 unt; 11 def)
% Number of atoms : 1343 ( 125 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1818 ( 775 ~; 884 |; 99 &)
% ( 17 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 12 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-4 aty)
% Number of variables : 328 ( 0 sgn 307 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f7711,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r1_orders_2(X0,X1,X2)
<=> r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_orders_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(f7895,axiom,
! [X0] :
( l1_orders_2(X0)
=> m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f7897,axiom,
! [X0,X1] :
( m1_relset_1(X1,X0,X0)
=> ! [X2,X3] :
( g1_orders_2(X0,X1) = g1_orders_2(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g1_orders_2) ).
fof(f11578,axiom,
! [X0] :
( l1_orders_2(X0)
=> k7_lattice3(k7_lattice3(X0)) = g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_lattice3) ).
fof(f14848,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m1_yellow_0(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> m1_subset_1(X2,u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_yellow_0) ).
fof(f14938,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_waybel_0(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> k3_waybel_0(X0,X1,X2) = k1_waybel_0(X1,X0,u1_waybel_0(X0,X1),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_waybel_0) ).
fof(f14941,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_waybel_0(X1,X0) )
=> ! [X2] :
( r1_waybel_0(X0,X1,X2)
<=> ? [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( r1_orders_2(X1,X3,X4)
=> r2_hidden(k3_waybel_0(X0,X1,X4),X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_waybel_0) ).
fof(f15032,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( l1_waybel_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f15036,axiom,
! [X0,X1,X2,X3] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& ~ v3_struct_0(X1)
& 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(X3,u1_struct_0(X0)) )
=> k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_waybel_0) ).
fof(f15049,axiom,
! [X0,X1] :
( ( l1_struct_0(X0)
& l1_waybel_0(X1,X0) )
=> ( v1_funct_1(u1_waybel_0(X0,X1))
& v1_funct_2(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_waybel_0) ).
fof(f16054,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v4_yellow_0(X0,X0)
& m1_yellow_0(X0,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow_6) ).
fof(f18704,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ( u1_struct_0(X0) = u1_struct_0(X1)
=> ! [X2] :
( l1_waybel_0(X2,X0)
=> ? [X3] :
( v6_waybel_0(X3,X1)
& l1_waybel_0(X3,X1)
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_waybel33) ).
fof(f18711,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& l1_waybel_0(X2,X0) )
=> ! [X3] :
( ( ~ v3_struct_0(X3)
& l1_waybel_0(X3,X1) )
=> ( ( g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) )
=> ! [X4] :
( r1_waybel_0(X0,X2,X4)
=> r1_waybel_0(X1,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_waybel33) ).
fof(f18712,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& l1_waybel_0(X2,X0) )
=> ! [X3] :
( ( ~ v3_struct_0(X3)
& l1_waybel_0(X3,X1) )
=> ( ( g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) )
=> ! [X4] :
( r1_waybel_0(X0,X2,X4)
=> r1_waybel_0(X1,X3,X4) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f18711]) ).
fof(f18758,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ( u1_struct_0(X0) = u1_struct_0(X1)
=> ! [X2] :
( l1_waybel_0(X2,X0)
=> ? [X3] :
( l1_waybel_0(X3,X1)
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) ) ) ) ) ),
inference(pure_predicate_removal,[],[f18704]) ).
fof(f18779,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ r1_waybel_0(X1,X3,X4)
& r1_waybel_0(X0,X2,X4) )
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3)
& ~ v3_struct_0(X3)
& l1_waybel_0(X3,X1) )
& ~ v3_struct_0(X2)
& l1_waybel_0(X2,X0) )
& ~ v3_struct_0(X1)
& l1_struct_0(X1) )
& ~ v3_struct_0(X0)
& l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18712]) ).
fof(f18780,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ r1_waybel_0(X1,X3,X4)
& r1_waybel_0(X0,X2,X4) )
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3)
& ~ v3_struct_0(X3)
& l1_waybel_0(X3,X1) )
& ~ v3_struct_0(X2)
& l1_waybel_0(X2,X0) )
& ~ v3_struct_0(X1)
& l1_struct_0(X1) )
& ~ v3_struct_0(X0)
& l1_struct_0(X0) ),
inference(flattening,[],[f18779]) ).
fof(f18781,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7885]) ).
fof(f18791,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ l1_waybel_0(X1,X0) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f15032]) ).
fof(f18804,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_waybel_0(X0,X1,X2)
<=> ? [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
& ! [X4] :
( r2_hidden(k3_waybel_0(X0,X1,X4),X2)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X1)) ) ) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f14941]) ).
fof(f18805,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_waybel_0(X0,X1,X2)
<=> ? [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
& ! [X4] :
( r2_hidden(k3_waybel_0(X0,X1,X4),X2)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X1)) ) ) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f18804]) ).
fof(f18851,plain,
! [X0] :
( k7_lattice3(k7_lattice3(X0)) = g1_orders_2(u1_struct_0(X0),u1_orders_2(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11578]) ).
fof(f18852,plain,
! [X0,X1] :
( ! [X2,X3] :
( ( X0 = X2
& X1 = X3 )
| g1_orders_2(X0,X1) != g1_orders_2(X2,X3) )
| ~ m1_relset_1(X1,X0,X0) ),
inference(ennf_transformation,[],[f7897]) ).
fof(f18863,plain,
! [X0] :
( m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7895]) ).
fof(f18864,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_orders_2(X0,X1,X2)
<=> r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7711]) ).
fof(f18865,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ? [X3] :
( l1_waybel_0(X3,X1)
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) )
| ~ l1_waybel_0(X2,X0) )
| u1_struct_0(X0) != u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18758]) ).
fof(f18866,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ? [X3] :
( l1_waybel_0(X3,X1)
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(X3),u1_orders_2(X3))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,X3) )
| ~ l1_waybel_0(X2,X0) )
| u1_struct_0(X0) != u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f18865]) ).
fof(f18869,plain,
! [X0,X1] :
( ( v1_funct_1(u1_waybel_0(X0,X1))
& v1_funct_2(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0)) )
| ~ l1_struct_0(X0)
| ~ l1_waybel_0(X1,X0) ),
inference(ennf_transformation,[],[f15049]) ).
fof(f18870,plain,
! [X0,X1] :
( ( v1_funct_1(u1_waybel_0(X0,X1))
& v1_funct_2(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0)) )
| ~ l1_struct_0(X0)
| ~ l1_waybel_0(X1,X0) ),
inference(flattening,[],[f18869]) ).
fof(f19070,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel_0(X0,X1,X2) = k1_waybel_0(X1,X0,u1_waybel_0(X0,X1),X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f14938]) ).
fof(f19071,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel_0(X0,X1,X2) = k1_waybel_0(X1,X0,u1_waybel_0(X0,X1),X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f19070]) ).
fof(f19078,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_yellow_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14848]) ).
fof(f19079,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_yellow_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19078]) ).
fof(f19086,plain,
! [X0] :
( ( v4_yellow_0(X0,X0)
& m1_yellow_0(X0,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16054]) ).
fof(f19861,plain,
! [X0,X1,X2,X3] :
( k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ 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(X3,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f15036]) ).
fof(f19862,plain,
! [X0,X1,X2,X3] :
( k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ 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(X3,u1_struct_0(X0)) ),
inference(flattening,[],[f19861]) ).
fof(f20792,plain,
( ~ r1_waybel_0(sK57,sK59,sK60)
& r1_waybel_0(sK56,sK58,sK60)
& g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = g1_orders_2(u1_struct_0(sK59),u1_orders_2(sK59))
& u1_waybel_0(sK56,sK58) = u1_waybel_0(sK57,sK59)
& ~ v3_struct_0(sK59)
& l1_waybel_0(sK59,sK57)
& ~ v3_struct_0(sK58)
& l1_waybel_0(sK58,sK56)
& ~ v3_struct_0(sK57)
& l1_struct_0(sK57)
& ~ v3_struct_0(sK56)
& l1_struct_0(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57,sK58,sK59,sK60]),skolemize(X0,sK56),skolemize(X1,sK57),skolemize(X2,sK58),skolemize(X3,sK59),skolemize(X4,sK60)],[f18780]) ).
fof(f20799,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_waybel_0(X0,X1,X2)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X1))
| ? [X4] :
( ~ r2_hidden(k3_waybel_0(X0,X1,X4),X2)
& r1_orders_2(X1,X3,X4)
& m1_subset_1(X4,u1_struct_0(X1)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
& ! [X4] :
( r2_hidden(k3_waybel_0(X0,X1,X4),X2)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X1)) ) )
| ~ r1_waybel_0(X0,X1,X2) ) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f18805]) ).
fof(f20800,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_waybel_0(X0,X1,X2)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X1))
| ? [X4] :
( ~ r2_hidden(k3_waybel_0(X0,X1,X4),X2)
& r1_orders_2(X1,X3,X4)
& m1_subset_1(X4,u1_struct_0(X1)) ) ) )
& ( ? [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
& ! [X6] :
( r2_hidden(k3_waybel_0(X0,X1,X6),X2)
| ~ r1_orders_2(X1,X5,X6)
| ~ m1_subset_1(X6,u1_struct_0(X1)) ) )
| ~ r1_waybel_0(X0,X1,X2) ) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(rectify,[],[f20799]) ).
fof(f20801,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_waybel_0(X0,X1,X2)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X1))
| ( ~ r2_hidden(k3_waybel_0(X0,X1,sK66(X0,X1,X2,X3)),X2)
& r1_orders_2(X1,X3,sK66(X0,X1,X2,X3))
& m1_subset_1(sK66(X0,X1,X2,X3),u1_struct_0(X1)) ) ) )
& ( ( m1_subset_1(sK67(X0,X1,X2),u1_struct_0(X1))
& ! [X6] :
( r2_hidden(k3_waybel_0(X0,X1,X6),X2)
| ~ r1_orders_2(X1,sK67(X0,X1,X2),X6)
| ~ m1_subset_1(X6,u1_struct_0(X1)) ) )
| ~ r1_waybel_0(X0,X1,X2) ) )
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66,sK67]),skolemize(X4,sK66(X0,X1,X2,X3)),skolemize(X5,sK67(X0,X1,X2))],[f20800]) ).
fof(f20804,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r1_orders_2(X0,X1,X2)
| ~ r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0)) )
& ( r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0))
| ~ r1_orders_2(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f18864]) ).
fof(f20805,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( l1_waybel_0(sK68(X0,X1,X2),X1)
& g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(sK68(X0,X1,X2)),u1_orders_2(sK68(X0,X1,X2)))
& u1_waybel_0(X0,X2) = u1_waybel_0(X1,sK68(X0,X1,X2)) )
| ~ l1_waybel_0(X2,X0) )
| u1_struct_0(X0) != u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X3,sK68(X0,X1,X2))],[f18866]) ).
fof(f20948,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,[],[f1394]) ).
fof(f21595,plain,
l1_struct_0(sK56),
inference(cnf_transformation,[],[f20792]) ).
fof(f21596,plain,
~ v3_struct_0(sK56),
inference(cnf_transformation,[],[f20792]) ).
fof(f21597,plain,
l1_struct_0(sK57),
inference(cnf_transformation,[],[f20792]) ).
fof(f21598,plain,
~ v3_struct_0(sK57),
inference(cnf_transformation,[],[f20792]) ).
fof(f21599,plain,
l1_waybel_0(sK58,sK56),
inference(cnf_transformation,[],[f20792]) ).
fof(f21600,plain,
~ v3_struct_0(sK58),
inference(cnf_transformation,[],[f20792]) ).
fof(f21601,plain,
l1_waybel_0(sK59,sK57),
inference(cnf_transformation,[],[f20792]) ).
fof(f21602,plain,
~ v3_struct_0(sK59),
inference(cnf_transformation,[],[f20792]) ).
fof(f21603,plain,
u1_waybel_0(sK56,sK58) = u1_waybel_0(sK57,sK59),
inference(cnf_transformation,[],[f20792]) ).
fof(f21604,plain,
g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = g1_orders_2(u1_struct_0(sK59),u1_orders_2(sK59)),
inference(cnf_transformation,[],[f20792]) ).
fof(f21605,plain,
r1_waybel_0(sK56,sK58,sK60),
inference(cnf_transformation,[],[f20792]) ).
fof(f21606,plain,
~ r1_waybel_0(sK57,sK59,sK60),
inference(cnf_transformation,[],[f20792]) ).
fof(f21609,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f18781]) ).
fof(f21622,plain,
! [X0,X1] :
( ~ l1_waybel_0(X1,X0)
| l1_orders_2(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f18791]) ).
fof(f21629,plain,
! [X2,X0,X1,X6] :
( ~ r1_orders_2(X1,sK67(X0,X1,X2),X6)
| r2_hidden(k3_waybel_0(X0,X1,X6),X2)
| ~ m1_subset_1(X6,u1_struct_0(X1))
| ~ r1_waybel_0(X0,X1,X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20801]) ).
fof(f21630,plain,
! [X2,X0,X1] :
( m1_subset_1(sK67(X0,X1,X2),u1_struct_0(X1))
| ~ r1_waybel_0(X0,X1,X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20801]) ).
fof(f21631,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(sK66(X0,X1,X2,X3),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| r1_waybel_0(X0,X1,X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20801]) ).
fof(f21632,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X1,X3,sK66(X0,X1,X2,X3))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| r1_waybel_0(X0,X1,X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20801]) ).
fof(f21633,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(k3_waybel_0(X0,X1,sK66(X0,X1,X2,X3)),X2)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| r1_waybel_0(X0,X1,X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20801]) ).
fof(f21680,plain,
! [X0] :
( ~ l1_orders_2(X0)
| g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) = k7_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f18851]) ).
fof(f21681,plain,
! [X2,X3,X0,X1] :
( g1_orders_2(X0,X1) != g1_orders_2(X2,X3)
| X1 = X3
| ~ m1_relset_1(X1,X0,X0) ),
inference(cnf_transformation,[],[f18852]) ).
fof(f21682,plain,
! [X2,X3,X0,X1] :
( g1_orders_2(X0,X1) != g1_orders_2(X2,X3)
| X0 = X2
| ~ m1_relset_1(X1,X0,X0) ),
inference(cnf_transformation,[],[f18852]) ).
fof(f21696,plain,
! [X0] :
( m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18863]) ).
fof(f21697,plain,
! [X2,X0,X1] :
( r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0))
| ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20804]) ).
fof(f21698,plain,
! [X2,X0,X1] :
( r1_orders_2(X0,X1,X2)
| ~ r2_hidden(k4_tarski(X1,X2),u1_orders_2(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20804]) ).
fof(f21699,plain,
! [X2,X0,X1] :
( u1_struct_0(X0) != u1_struct_0(X1)
| ~ l1_waybel_0(X2,X0)
| u1_waybel_0(X0,X2) = u1_waybel_0(X1,sK68(X0,X1,X2))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20805]) ).
fof(f21700,plain,
! [X2,X0,X1] :
( u1_struct_0(X0) != u1_struct_0(X1)
| ~ l1_waybel_0(X2,X0)
| g1_orders_2(u1_struct_0(X2),u1_orders_2(X2)) = g1_orders_2(u1_struct_0(sK68(X0,X1,X2)),u1_orders_2(sK68(X0,X1,X2)))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20805]) ).
fof(f21701,plain,
! [X2,X0,X1] :
( u1_struct_0(X0) != u1_struct_0(X1)
| ~ l1_waybel_0(X2,X0)
| l1_waybel_0(sK68(X0,X1,X2),X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f20805]) ).
fof(f21706,plain,
! [X0,X1] :
( m2_relset_1(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0))
| ~ l1_struct_0(X0)
| ~ l1_waybel_0(X1,X0) ),
inference(cnf_transformation,[],[f18870]) ).
fof(f21707,plain,
! [X0,X1] :
( v1_funct_2(u1_waybel_0(X0,X1),u1_struct_0(X1),u1_struct_0(X0))
| ~ l1_struct_0(X0)
| ~ l1_waybel_0(X1,X0) ),
inference(cnf_transformation,[],[f18870]) ).
fof(f21708,plain,
! [X0,X1] :
( v1_funct_1(u1_waybel_0(X0,X1))
| ~ l1_struct_0(X0)
| ~ l1_waybel_0(X1,X0) ),
inference(cnf_transformation,[],[f18870]) ).
fof(f21991,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
| k3_waybel_0(X0,X1,X2) = k1_waybel_0(X1,X0,u1_waybel_0(X0,X1),X2)
| v3_struct_0(X1)
| ~ l1_waybel_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f19071]) ).
fof(f21997,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
| m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ m1_yellow_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19079]) ).
fof(f22003,plain,
! [X0] :
( m1_yellow_0(X0,X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19086]) ).
fof(f22273,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20948]) ).
fof(f23299,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| k1_funct_1(X2,X3) = k1_waybel_0(X0,X1,X2,X3)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19862]) ).
fof(f23952,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f23955,plain,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f24533,plain,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k2_tarski(X0,X0)),
inference(definition_unfolding,[],[f23955,f23952]) ).
fof(f24550,plain,
! [X2,X0,X1] :
( ~ r2_hidden(k2_tarski(k2_tarski(X1,X2),k2_tarski(X1,X1)),u1_orders_2(X0))
| r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f21698,f24533]) ).
fof(f24551,plain,
! [X2,X0,X1] :
( r2_hidden(k2_tarski(k2_tarski(X1,X2),k2_tarski(X1,X1)),u1_orders_2(X0))
| ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f21697,f24533]) ).
fof(f26287,plain,
( v1_funct_1(u1_waybel_0(sK56,sK58))
| ~ l1_struct_0(sK57)
| ~ l1_waybel_0(sK59,sK57) ),
inference(superposition,[],[f21708,f21603]) ).
fof(f26288,plain,
( v1_funct_1(u1_waybel_0(sK56,sK58))
| ~ l1_waybel_0(sK59,sK57) ),
inference(forward_subsumption_resolution,[],[f26287,f21597]) ).
fof(f26289,plain,
v1_funct_1(u1_waybel_0(sK56,sK58)),
inference(forward_subsumption_resolution,[],[f26288,f21601]) ).
fof(f26290,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ l1_struct_0(sK57)
| ~ l1_waybel_0(sK59,sK57) ),
inference(superposition,[],[f21707,f21603]) ).
fof(f26291,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ l1_waybel_0(sK59,sK57) ),
inference(forward_subsumption_resolution,[],[f26290,f21597]) ).
fof(f26292,plain,
v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57)),
inference(forward_subsumption_resolution,[],[f26291,f21601]) ).
fof(f26293,plain,
( l1_orders_2(sK59)
| ~ l1_struct_0(sK57) ),
inference(resolution,[],[f21622,f21601]) ).
fof(f26294,plain,
( l1_orders_2(sK58)
| ~ l1_struct_0(sK56) ),
inference(resolution,[],[f21622,f21599]) ).
fof(f26295,plain,
l1_orders_2(sK58),
inference(forward_subsumption_resolution,[],[f26294,f21595]) ).
fof(f26296,plain,
l1_orders_2(sK59),
inference(forward_subsumption_resolution,[],[f26293,f21597]) ).
fof(f26302,plain,
( m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ l1_struct_0(sK57)
| ~ l1_waybel_0(sK59,sK57) ),
inference(superposition,[],[f21706,f21603]) ).
fof(f26303,plain,
( m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ l1_waybel_0(sK59,sK57) ),
inference(forward_subsumption_resolution,[],[f26302,f21597]) ).
fof(f26304,plain,
m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57)),
inference(forward_subsumption_resolution,[],[f26303,f21601]) ).
fof(f26312,plain,
g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = k7_lattice3(k7_lattice3(sK58)),
inference(resolution,[],[f26295,f21680]) ).
fof(f26340,plain,
! [X0,X1] :
( g1_orders_2(X0,X1) != g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58))
| u1_orders_2(sK59) = X1
| ~ m1_relset_1(X1,X0,X0) ),
inference(superposition,[],[f21681,f21604]) ).
fof(f26343,plain,
! [X0,X1] :
( g1_orders_2(X0,X1) != k7_lattice3(k7_lattice3(sK58))
| u1_orders_2(sK59) = X1
| ~ m1_relset_1(X1,X0,X0) ),
inference(forward_demodulation,[],[f26340,f26312]) ).
fof(f26346,definition,
( spl525_12
<=> m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58)) ),
introduced(definition,[new_symbols(definition,[spl525_12])],[avatar_definition]) ).
fof(f26347,plain,
( m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58))
| ~ spl525_12 ),
inference(avatar_component_clause,[],[f26346]) ).
fof(f26348,plain,
( ~ m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58))
| spl525_12 ),
inference(avatar_component_clause,[],[f26346]) ).
fof(f26368,plain,
! [X0,X1] :
( g1_orders_2(X0,X1) != g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58))
| u1_struct_0(sK59) = X0
| ~ m1_relset_1(X1,X0,X0) ),
inference(superposition,[],[f21682,f21604]) ).
fof(f26369,plain,
! [X0,X1] :
( g1_orders_2(X0,X1) != k7_lattice3(k7_lattice3(sK58))
| u1_struct_0(sK58) = X0
| ~ m1_relset_1(X1,X0,X0) ),
inference(superposition,[],[f21682,f26312]) ).
fof(f26371,plain,
! [X0,X1] :
( g1_orders_2(X0,X1) != k7_lattice3(k7_lattice3(sK58))
| u1_struct_0(sK59) = X0
| ~ m1_relset_1(X1,X0,X0) ),
inference(forward_demodulation,[],[f26368,f26312]) ).
fof(f26380,plain,
l1_struct_0(sK58),
inference(resolution,[],[f21609,f26295]) ).
fof(f26381,plain,
l1_struct_0(sK59),
inference(resolution,[],[f21609,f26296]) ).
fof(f26384,plain,
( k7_lattice3(k7_lattice3(sK58)) != k7_lattice3(k7_lattice3(sK58))
| u1_orders_2(sK58) = u1_orders_2(sK59)
| ~ m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58)) ),
inference(superposition,[],[f26343,f26312]) ).
fof(f26385,plain,
( u1_orders_2(sK58) = u1_orders_2(sK59)
| ~ m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58)) ),
inference(trivial_inequality_removal,[],[f26384]) ).
fof(f26574,plain,
! [X0] :
( v3_struct_0(sK59)
| ~ l1_struct_0(sK59)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(resolution,[],[f23299,f26292]) ).
fof(f26580,plain,
! [X0] :
( ~ l1_struct_0(sK59)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(forward_subsumption_resolution,[],[f26574,f21602]) ).
fof(f26582,plain,
! [X0] :
( v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(forward_subsumption_resolution,[],[f26580,f26381]) ).
fof(f26583,plain,
! [X0] :
( ~ l1_struct_0(sK57)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(forward_subsumption_resolution,[],[f26582,f21598]) ).
fof(f26584,plain,
! [X0] :
( ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(forward_subsumption_resolution,[],[f26583,f21597]) ).
fof(f26585,plain,
! [X0] :
( k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ),
inference(forward_subsumption_resolution,[],[f26584,f26289]) ).
fof(f26587,definition,
( spl525_48
<=> m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57)) ),
introduced(definition,[new_symbols(definition,[spl525_48])],[avatar_definition]) ).
fof(f26589,plain,
( ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57))
| spl525_48 ),
inference(avatar_component_clause,[],[f26587]) ).
fof(f26591,definition,
( spl525_49
<=> ! [X0] :
( k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK59)) ) ),
introduced(definition,[new_symbols(definition,[spl525_49])],[avatar_definition]) ).
fof(f26592,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK59))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0) )
| ~ spl525_49 ),
inference(avatar_component_clause,[],[f26591]) ).
fof(f26593,plain,
( ~ spl525_48
| spl525_49 ),
inference(avatar_split_clause,[],[f26585,f26591,f26587]) ).
fof(f26599,plain,
( k7_lattice3(k7_lattice3(sK58)) != k7_lattice3(k7_lattice3(sK58))
| u1_struct_0(sK58) = u1_struct_0(sK59)
| ~ m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58)) ),
inference(superposition,[],[f26371,f26312]) ).
fof(f26600,plain,
( u1_struct_0(sK58) = u1_struct_0(sK59)
| ~ m1_relset_1(u1_orders_2(sK58),u1_struct_0(sK58),u1_struct_0(sK58)) ),
inference(trivial_inequality_removal,[],[f26599]) ).
fof(f26722,plain,
! [X0,X1] :
( ~ l1_waybel_0(X0,X1)
| u1_waybel_0(X1,X0) = u1_waybel_0(X1,sK68(X1,X1,X0))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(equality_resolution,[],[f21699]) ).
fof(f26723,plain,
! [X0,X1] :
( ~ l1_waybel_0(X0,X1)
| u1_waybel_0(X1,X0) = u1_waybel_0(X1,sK68(X1,X1,X0))
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(duplicate_literal_removal,[],[f26722]) ).
fof(f26725,plain,
( u1_waybel_0(sK56,sK58) = u1_waybel_0(sK56,sK68(sK56,sK56,sK58))
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56) ),
inference(resolution,[],[f26723,f21599]) ).
fof(f26726,plain,
( u1_waybel_0(sK56,sK58) = u1_waybel_0(sK56,sK68(sK56,sK56,sK58))
| ~ l1_struct_0(sK56) ),
inference(forward_subsumption_resolution,[],[f26725,f21596]) ).
fof(f26728,plain,
u1_waybel_0(sK56,sK58) = u1_waybel_0(sK56,sK68(sK56,sK56,sK58)),
inference(forward_subsumption_resolution,[],[f26726,f21595]) ).
fof(f26790,plain,
( m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ l1_struct_0(sK56)
| ~ l1_waybel_0(sK68(sK56,sK56,sK58),sK56) ),
inference(superposition,[],[f21706,f26728]) ).
fof(f26791,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ l1_struct_0(sK56)
| ~ l1_waybel_0(sK68(sK56,sK56,sK58),sK56) ),
inference(superposition,[],[f21707,f26728]) ).
fof(f26795,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ l1_waybel_0(sK68(sK56,sK56,sK58),sK56) ),
inference(forward_subsumption_resolution,[],[f26791,f21595]) ).
fof(f26796,plain,
( m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ l1_waybel_0(sK68(sK56,sK56,sK58),sK56) ),
inference(forward_subsumption_resolution,[],[f26790,f21595]) ).
fof(f26801,definition,
( spl525_69
<=> l1_waybel_0(sK68(sK56,sK56,sK58),sK56) ),
introduced(definition,[new_symbols(definition,[spl525_69])],[avatar_definition]) ).
fof(f26802,plain,
( l1_waybel_0(sK68(sK56,sK56,sK58),sK56)
| ~ spl525_69 ),
inference(avatar_component_clause,[],[f26801]) ).
fof(f26803,plain,
( ~ l1_waybel_0(sK68(sK56,sK56,sK58),sK56)
| spl525_69 ),
inference(avatar_component_clause,[],[f26801]) ).
fof(f26805,definition,
( spl525_70
<=> v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56)) ),
introduced(definition,[new_symbols(definition,[spl525_70])],[avatar_definition]) ).
fof(f26807,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ spl525_70 ),
inference(avatar_component_clause,[],[f26805]) ).
fof(f26808,plain,
( ~ spl525_69
| spl525_70 ),
inference(avatar_split_clause,[],[f26795,f26805,f26801]) ).
fof(f26810,definition,
( spl525_71
<=> m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56)) ),
introduced(definition,[new_symbols(definition,[spl525_71])],[avatar_definition]) ).
fof(f26812,plain,
( m2_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ spl525_71 ),
inference(avatar_component_clause,[],[f26810]) ).
fof(f26813,plain,
( ~ spl525_69
| spl525_71 ),
inference(avatar_split_clause,[],[f26796,f26810,f26801]) ).
fof(f26828,definition,
( spl525_75
<=> m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56)) ),
introduced(definition,[new_symbols(definition,[spl525_75])],[avatar_definition]) ).
fof(f26829,plain,
( m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ spl525_75 ),
inference(avatar_component_clause,[],[f26828]) ).
fof(f26830,plain,
( ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| spl525_75 ),
inference(avatar_component_clause,[],[f26828]) ).
fof(f26880,plain,
! [X0,X1] :
( ~ l1_waybel_0(X0,X1)
| g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) = g1_orders_2(u1_struct_0(sK68(X1,X1,X0)),u1_orders_2(sK68(X1,X1,X0)))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(equality_resolution,[],[f21700]) ).
fof(f26881,plain,
! [X0,X1] :
( ~ l1_waybel_0(X0,X1)
| g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) = g1_orders_2(u1_struct_0(sK68(X1,X1,X0)),u1_orders_2(sK68(X1,X1,X0)))
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(duplicate_literal_removal,[],[f26880]) ).
fof(f26883,plain,
( g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = g1_orders_2(u1_struct_0(sK68(sK56,sK56,sK58)),u1_orders_2(sK68(sK56,sK56,sK58)))
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56) ),
inference(resolution,[],[f26881,f21599]) ).
fof(f26884,plain,
( g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = g1_orders_2(u1_struct_0(sK68(sK56,sK56,sK58)),u1_orders_2(sK68(sK56,sK56,sK58)))
| ~ l1_struct_0(sK56) ),
inference(forward_subsumption_resolution,[],[f26883,f21596]) ).
fof(f26886,plain,
g1_orders_2(u1_struct_0(sK58),u1_orders_2(sK58)) = g1_orders_2(u1_struct_0(sK68(sK56,sK56,sK58)),u1_orders_2(sK68(sK56,sK56,sK58))),
inference(forward_subsumption_resolution,[],[f26884,f21595]) ).
fof(f26888,plain,
k7_lattice3(k7_lattice3(sK58)) = g1_orders_2(u1_struct_0(sK68(sK56,sK56,sK58)),u1_orders_2(sK68(sK56,sK56,sK58))),
inference(forward_demodulation,[],[f26886,f26312]) ).
fof(f26981,definition,
( spl525_88
<=> m1_relset_1(u1_orders_2(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58))) ),
introduced(definition,[new_symbols(definition,[spl525_88])],[avatar_definition]) ).
fof(f26982,plain,
( m1_relset_1(u1_orders_2(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)))
| ~ spl525_88 ),
inference(avatar_component_clause,[],[f26981]) ).
fof(f26983,plain,
( ~ m1_relset_1(u1_orders_2(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)))
| spl525_88 ),
inference(avatar_component_clause,[],[f26981]) ).
fof(f27013,definition,
( spl525_95
<=> l1_orders_2(sK68(sK56,sK56,sK58)) ),
introduced(definition,[new_symbols(definition,[spl525_95])],[avatar_definition]) ).
fof(f27014,plain,
( l1_orders_2(sK68(sK56,sK56,sK58))
| ~ spl525_95 ),
inference(avatar_component_clause,[],[f27013]) ).
fof(f27015,plain,
( ~ l1_orders_2(sK68(sK56,sK56,sK58))
| spl525_95 ),
inference(avatar_component_clause,[],[f27013]) ).
fof(f27053,plain,
! [X0,X1] :
( ~ l1_waybel_0(X0,X1)
| l1_waybel_0(sK68(X1,X1,X0),X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(equality_resolution,[],[f21701]) ).
fof(f27054,plain,
! [X0,X1] :
( l1_waybel_0(sK68(X1,X1,X0),X1)
| ~ l1_waybel_0(X0,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(duplicate_literal_removal,[],[f27053]) ).
fof(f27094,plain,
( ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_69 ),
inference(resolution,[],[f27054,f26803]) ).
fof(f27101,plain,
( v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_69 ),
inference(forward_subsumption_resolution,[],[f27094,f21599]) ).
fof(f27103,plain,
( ~ l1_struct_0(sK56)
| spl525_69 ),
inference(forward_subsumption_resolution,[],[f27101,f21596]) ).
fof(f27105,plain,
( $false
| spl525_69 ),
inference(forward_subsumption_resolution,[],[f27103,f21595]) ).
fof(f27106,plain,
spl525_69,
inference(avatar_contradiction_clause,[],[f27105]) ).
fof(f27207,plain,
( l1_orders_2(sK68(sK56,sK56,sK58))
| ~ l1_struct_0(sK56)
| ~ spl525_69 ),
inference(resolution,[],[f26802,f21622]) ).
fof(f27208,plain,
( ~ l1_struct_0(sK56)
| ~ spl525_69
| spl525_95 ),
inference(forward_subsumption_resolution,[],[f27207,f27015]) ).
fof(f27211,plain,
( $false
| ~ spl525_69
| spl525_95 ),
inference(forward_subsumption_resolution,[],[f27208,f21595]) ).
fof(f27212,plain,
( ~ spl525_69
| spl525_95 ),
inference(avatar_contradiction_clause,[],[f27211]) ).
fof(f28217,plain,
( k7_lattice3(k7_lattice3(sK58)) != k7_lattice3(k7_lattice3(sK58))
| u1_struct_0(sK58) = u1_struct_0(sK68(sK56,sK56,sK58))
| ~ m1_relset_1(u1_orders_2(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58))) ),
inference(superposition,[],[f26369,f26888]) ).
fof(f28218,plain,
( u1_struct_0(sK58) = u1_struct_0(sK68(sK56,sK56,sK58))
| ~ m1_relset_1(u1_orders_2(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK68(sK56,sK56,sK58))) ),
inference(trivial_inequality_removal,[],[f28217]) ).
fof(f28329,plain,
m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK59),u1_struct_0(sK57)),
inference(resolution,[],[f22273,f26304]) ).
fof(f28332,plain,
( m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK68(sK56,sK56,sK58)),u1_struct_0(sK56))
| ~ spl525_71 ),
inference(resolution,[],[f22273,f26812]) ).
fof(f28333,plain,
! [X0] :
( m1_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f22273,f21696]) ).
fof(f28334,plain,
( $false
| ~ spl525_71
| spl525_75 ),
inference(forward_subsumption_resolution,[],[f28332,f26830]) ).
fof(f28335,plain,
( ~ spl525_71
| spl525_75 ),
inference(avatar_contradiction_clause,[],[f28334]) ).
fof(f28340,plain,
( $false
| spl525_48 ),
inference(forward_subsumption_resolution,[],[f28329,f26589]) ).
fof(f28341,plain,
spl525_48,
inference(avatar_contradiction_clause,[],[f28340]) ).
fof(f28396,plain,
( ~ l1_orders_2(sK58)
| spl525_12 ),
inference(resolution,[],[f28333,f26348]) ).
fof(f28398,plain,
( ~ l1_orders_2(sK68(sK56,sK56,sK58))
| spl525_88 ),
inference(resolution,[],[f28333,f26983]) ).
fof(f28407,plain,
( $false
| spl525_88
| ~ spl525_95 ),
inference(forward_subsumption_resolution,[],[f28398,f27014]) ).
fof(f28408,plain,
( spl525_88
| ~ spl525_95 ),
inference(avatar_contradiction_clause,[],[f28407]) ).
fof(f28411,plain,
( $false
| spl525_12 ),
inference(forward_subsumption_resolution,[],[f28396,f26295]) ).
fof(f28412,plain,
spl525_12,
inference(avatar_contradiction_clause,[],[f28411]) ).
fof(f28422,plain,
( u1_struct_0(sK58) = u1_struct_0(sK68(sK56,sK56,sK58))
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f28218,f26982]) ).
fof(f28433,plain,
( u1_orders_2(sK58) = u1_orders_2(sK59)
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f26385,f26347]) ).
fof(f28434,plain,
( u1_struct_0(sK58) = u1_struct_0(sK59)
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f26600,f26347]) ).
fof(f28688,definition,
( spl525_226
<=> m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK58)) ),
introduced(definition,[new_symbols(definition,[spl525_226])],[avatar_definition]) ).
fof(f28689,plain,
( m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK58))
| ~ spl525_226 ),
inference(avatar_component_clause,[],[f28688]) ).
fof(f28690,plain,
( ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK58))
| spl525_226 ),
inference(avatar_component_clause,[],[f28688]) ).
fof(f28727,plain,
( ~ r1_waybel_0(sK56,sK58,sK60)
| v3_struct_0(sK58)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_226 ),
inference(resolution,[],[f28690,f21630]) ).
fof(f28728,plain,
( v3_struct_0(sK58)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_226 ),
inference(forward_subsumption_resolution,[],[f28727,f21605]) ).
fof(f28729,plain,
( ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_226 ),
inference(forward_subsumption_resolution,[],[f28728,f21600]) ).
fof(f28730,plain,
( v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| spl525_226 ),
inference(forward_subsumption_resolution,[],[f28729,f21599]) ).
fof(f28731,plain,
( ~ l1_struct_0(sK56)
| spl525_226 ),
inference(forward_subsumption_resolution,[],[f28730,f21596]) ).
fof(f28732,plain,
( $false
| spl525_226 ),
inference(forward_subsumption_resolution,[],[f28731,f21595]) ).
fof(f28733,plain,
spl525_226,
inference(avatar_contradiction_clause,[],[f28732]) ).
fof(f29053,plain,
( m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ spl525_75
| ~ spl525_88 ),
inference(superposition,[],[f26829,f28422]) ).
fof(f29055,plain,
( v1_funct_2(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ spl525_70
| ~ spl525_88 ),
inference(superposition,[],[f26807,f28422]) ).
fof(f29637,plain,
( ! [X0,X1] :
( r2_hidden(k2_tarski(k2_tarski(X0,X1),k2_tarski(X0,X0)),u1_orders_2(sK58))
| ~ r1_orders_2(sK59,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK59))
| ~ m1_subset_1(X0,u1_struct_0(sK59))
| ~ l1_orders_2(sK59) )
| ~ spl525_12 ),
inference(superposition,[],[f24551,f28433]) ).
fof(f29662,plain,
( ! [X0,X1] :
( r2_hidden(k2_tarski(k2_tarski(X0,X1),k2_tarski(X0,X0)),u1_orders_2(sK58))
| ~ r1_orders_2(sK59,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK59))
| ~ m1_subset_1(X0,u1_struct_0(sK59)) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f29637,f26296]) ).
fof(f29679,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(sK58))
| r2_hidden(k2_tarski(k2_tarski(X0,X1),k2_tarski(X0,X0)),u1_orders_2(sK58))
| ~ r1_orders_2(sK59,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK59)) )
| ~ spl525_12 ),
inference(forward_demodulation,[],[f29662,f28434]) ).
fof(f29695,plain,
( ! [X0,X1] :
( r2_hidden(k2_tarski(k2_tarski(X0,X1),k2_tarski(X0,X0)),u1_orders_2(sK58))
| ~ m1_subset_1(X1,u1_struct_0(sK58))
| ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ r1_orders_2(sK59,X0,X1) )
| ~ spl525_12 ),
inference(forward_demodulation,[],[f29679,f28434]) ).
fof(f29725,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),X0) )
| ~ spl525_12
| ~ spl525_49 ),
inference(superposition,[],[f26592,f28434]) ).
fof(f29733,plain,
( ! [X2,X0,X1] :
( m1_subset_1(sK66(X0,sK59,X1,X2),u1_struct_0(sK58))
| ~ m1_subset_1(X2,u1_struct_0(sK58))
| r1_waybel_0(X0,sK59,X1)
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(superposition,[],[f21631,f28434]) ).
fof(f29757,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| k3_waybel_0(X1,sK59,X0) = k1_waybel_0(sK59,X1,u1_waybel_0(X1,sK59),X0)
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(superposition,[],[f21991,f28434]) ).
fof(f29797,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| k3_waybel_0(X1,sK59,X0) = k1_waybel_0(sK59,X1,u1_waybel_0(X1,sK59),X0)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f29757,f21602]) ).
fof(f29812,plain,
( ! [X2,X0,X1] :
( m1_subset_1(sK66(X0,sK59,X1,X2),u1_struct_0(sK58))
| ~ m1_subset_1(X2,u1_struct_0(sK58))
| r1_waybel_0(X0,sK59,X1)
| ~ l1_waybel_0(sK59,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f29733,f21602]) ).
fof(f29905,plain,
( ! [X0] :
( v3_struct_0(sK58)
| ~ l1_struct_0(sK58)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(resolution,[],[f29055,f23299]) ).
fof(f29906,plain,
( ! [X0] :
( ~ l1_struct_0(sK58)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29905,f21600]) ).
fof(f29908,plain,
( ! [X0] :
( v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29906,f26380]) ).
fof(f29910,plain,
( ! [X0] :
( ~ l1_struct_0(sK56)
| ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29908,f21596]) ).
fof(f29912,plain,
( ! [X0] :
( ~ v1_funct_1(u1_waybel_0(sK56,sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29910,f21595]) ).
fof(f29914,plain,
( ! [X0] :
( k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0)
| ~ m1_relset_1(u1_waybel_0(sK56,sK58),u1_struct_0(sK58),u1_struct_0(sK56))
| ~ m1_subset_1(X0,u1_struct_0(sK58)) )
| ~ spl525_70
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29912,f26289]) ).
fof(f29915,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| k1_funct_1(u1_waybel_0(sK56,sK58),X0) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),X0) )
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88 ),
inference(forward_subsumption_resolution,[],[f29914,f29053]) ).
fof(f30690,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ m1_subset_1(X1,u1_struct_0(sK58))
| ~ r1_orders_2(sK59,X1,X0)
| r1_orders_2(sK58,X1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ m1_subset_1(X1,u1_struct_0(sK58))
| ~ l1_orders_2(sK58) )
| ~ spl525_12 ),
inference(resolution,[],[f29695,f24550]) ).
fof(f30706,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ m1_subset_1(X1,u1_struct_0(sK58))
| ~ r1_orders_2(sK59,X1,X0)
| r1_orders_2(sK58,X1,X0)
| ~ l1_orders_2(sK58) )
| ~ spl525_12 ),
inference(duplicate_literal_removal,[],[f30690]) ).
fof(f30715,plain,
( ! [X0,X1] :
( ~ r1_orders_2(sK59,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK58))
| ~ m1_subset_1(X0,u1_struct_0(sK58))
| r1_orders_2(sK58,X1,X0) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f30706,f26295]) ).
fof(f30725,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ m1_subset_1(sK66(X1,sK59,X2,X0),u1_struct_0(sK58))
| r1_orders_2(sK58,X0,sK66(X1,sK59,X2,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK59))
| r1_waybel_0(X1,sK59,X2)
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(resolution,[],[f30715,f21632]) ).
fof(f30727,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| r1_orders_2(sK58,X0,sK66(X1,sK59,X2,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK59))
| r1_waybel_0(X1,sK59,X2)
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f30725,f29812]) ).
fof(f30728,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| r1_orders_2(sK58,X0,sK66(X1,sK59,X2,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK59))
| r1_waybel_0(X1,sK59,X2)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f30727,f21602]) ).
fof(f30729,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK58))
| ~ m1_subset_1(X0,u1_struct_0(sK58))
| r1_orders_2(sK58,X0,sK66(X1,sK59,X2,X0))
| r1_waybel_0(X1,sK59,X2)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(forward_demodulation,[],[f30728,f28434]) ).
fof(f30730,plain,
( ! [X2,X0,X1] :
( r1_orders_2(sK58,X0,sK66(X1,sK59,X2,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK58))
| r1_waybel_0(X1,sK59,X2)
| ~ l1_waybel_0(sK59,X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ spl525_12 ),
inference(duplicate_literal_removal,[],[f30729]) ).
fof(f30732,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK67(X0,sK58,X1),u1_struct_0(sK58))
| r1_waybel_0(X2,sK59,X3)
| ~ l1_waybel_0(sK59,X2)
| v3_struct_0(X2)
| ~ l1_struct_0(X2)
| r2_hidden(k3_waybel_0(X0,sK58,sK66(X2,sK59,X3,sK67(X0,sK58,X1))),X1)
| ~ m1_subset_1(sK66(X2,sK59,X3,sK67(X0,sK58,X1)),u1_struct_0(sK58))
| ~ r1_waybel_0(X0,sK58,X1)
| v3_struct_0(sK58)
| ~ l1_waybel_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(resolution,[],[f30730,f21629]) ).
fof(f30734,plain,
( ! [X2,X3,X0,X1] :
( r1_waybel_0(X2,sK59,X3)
| ~ l1_waybel_0(sK59,X2)
| v3_struct_0(X2)
| ~ l1_struct_0(X2)
| r2_hidden(k3_waybel_0(X0,sK58,sK66(X2,sK59,X3,sK67(X0,sK58,X1))),X1)
| ~ m1_subset_1(sK66(X2,sK59,X3,sK67(X0,sK58,X1)),u1_struct_0(sK58))
| ~ r1_waybel_0(X0,sK58,X1)
| v3_struct_0(sK58)
| ~ l1_waybel_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f30732,f21630]) ).
fof(f30736,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k3_waybel_0(X0,sK58,sK66(X2,sK59,X3,sK67(X0,sK58,X1))),X1)
| ~ l1_waybel_0(sK59,X2)
| v3_struct_0(X2)
| ~ l1_struct_0(X2)
| r1_waybel_0(X2,sK59,X3)
| ~ m1_subset_1(sK66(X2,sK59,X3,sK67(X0,sK58,X1)),u1_struct_0(sK58))
| ~ r1_waybel_0(X0,sK58,X1)
| ~ l1_waybel_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f30734,f21600]) ).
fof(f34547,plain,
( ! [X2,X3,X0,X1] :
( m1_subset_1(sK66(X0,sK59,X1,X2),u1_struct_0(X3))
| v3_struct_0(sK58)
| ~ m1_yellow_0(sK58,X3)
| v3_struct_0(X3)
| ~ l1_orders_2(X3)
| ~ m1_subset_1(X2,u1_struct_0(sK58))
| r1_waybel_0(X0,sK59,X1)
| ~ l1_waybel_0(sK59,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(resolution,[],[f21997,f29812]) ).
fof(f34549,plain,
( ! [X0] :
( m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(X0))
| v3_struct_0(sK58)
| ~ m1_yellow_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) )
| ~ spl525_226 ),
inference(resolution,[],[f21997,f28689]) ).
fof(f34581,plain,
( ! [X0] :
( m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(X0))
| ~ m1_yellow_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) )
| ~ spl525_226 ),
inference(forward_subsumption_resolution,[],[f34549,f21600]) ).
fof(f34582,plain,
( ! [X2,X3,X0,X1] :
( m1_subset_1(sK66(X0,sK59,X1,X2),u1_struct_0(X3))
| ~ m1_yellow_0(sK58,X3)
| v3_struct_0(X3)
| ~ l1_orders_2(X3)
| ~ m1_subset_1(X2,u1_struct_0(sK58))
| r1_waybel_0(X0,sK59,X1)
| ~ l1_waybel_0(sK59,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12 ),
inference(forward_subsumption_resolution,[],[f34547,f21600]) ).
fof(f65651,definition,
( spl525_1256
<=> m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58)) ),
introduced(definition,[new_symbols(definition,[spl525_1256])],[avatar_definition]) ).
fof(f65652,plain,
( m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ spl525_1256 ),
inference(avatar_component_clause,[],[f65651]) ).
fof(f65653,plain,
( ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| spl525_1256 ),
inference(avatar_component_clause,[],[f65651]) ).
fof(f65777,plain,
( ~ m1_yellow_0(sK58,sK58)
| v3_struct_0(sK58)
| ~ l1_orders_2(sK58)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK58))
| r1_waybel_0(sK57,sK59,sK60)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| spl525_1256 ),
inference(resolution,[],[f65653,f34582]) ).
fof(f65780,plain,
( ~ m1_yellow_0(sK58,sK58)
| v3_struct_0(sK58)
| ~ l1_orders_2(sK58)
| r1_waybel_0(sK57,sK59,sK60)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65777,f34581]) ).
fof(f65783,plain,
( v3_struct_0(sK58)
| ~ l1_orders_2(sK58)
| r1_waybel_0(sK57,sK59,sK60)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65780,f22003]) ).
fof(f65786,plain,
( ~ l1_orders_2(sK58)
| r1_waybel_0(sK57,sK59,sK60)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65783,f21600]) ).
fof(f65789,plain,
( r1_waybel_0(sK57,sK59,sK60)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65786,f26295]) ).
fof(f65792,plain,
( ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65789,f21606]) ).
fof(f65796,plain,
( v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65792,f21601]) ).
fof(f65798,plain,
( ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65796,f21598]) ).
fof(f65800,plain,
( $false
| ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65798,f21597]) ).
fof(f65801,plain,
( ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(avatar_contradiction_clause,[],[f65800]) ).
fof(f65812,plain,
( k1_funct_1(u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_12
| ~ spl525_49
| ~ spl525_1256 ),
inference(resolution,[],[f65652,f29725]) ).
fof(f65813,plain,
( ! [X0] :
( ~ l1_waybel_0(sK59,X0)
| k3_waybel_0(X0,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK59,X0,u1_waybel_0(X0,sK59),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_12
| ~ spl525_1256 ),
inference(resolution,[],[f65652,f29797]) ).
fof(f65816,plain,
( k1_funct_1(u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(resolution,[],[f65652,f29915]) ).
fof(f65846,plain,
( ! [X0] :
( k3_waybel_0(X0,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK58,X0,u1_waybel_0(X0,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| v3_struct_0(sK58)
| ~ l1_waybel_0(sK58,X0)
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_1256 ),
inference(resolution,[],[f65652,f21991]) ).
fof(f65873,plain,
( ! [X0] :
( ~ l1_waybel_0(sK58,X0)
| k3_waybel_0(X0,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK58,X0,u1_waybel_0(X0,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) )
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f65846,f21600]) ).
fof(f66166,plain,
( k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_1256 ),
inference(resolution,[],[f65873,f21599]) ).
fof(f66167,plain,
( k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ l1_struct_0(sK56)
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f66166,f21596]) ).
fof(f66168,plain,
( k1_waybel_0(sK58,sK56,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f66167,f21595]) ).
fof(f66263,plain,
( k1_funct_1(u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(superposition,[],[f66168,f65816]) ).
fof(f67162,plain,
( k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK57,sK59),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_1256 ),
inference(resolution,[],[f65813,f21601]) ).
fof(f67163,plain,
( k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK57,sK59),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67162,f21598]) ).
fof(f67164,plain,
( k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k1_waybel_0(sK59,sK57,u1_waybel_0(sK57,sK59),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_12
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67163,f21597]) ).
fof(f67165,plain,
( k1_waybel_0(sK59,sK57,u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_12
| ~ spl525_1256 ),
inference(forward_demodulation,[],[f67164,f21603]) ).
fof(f67167,plain,
( k1_funct_1(u1_waybel_0(sK56,sK58),sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_12
| ~ spl525_49
| ~ spl525_1256 ),
inference(superposition,[],[f65812,f67165]) ).
fof(f67172,plain,
( k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))) = k3_waybel_0(sK57,sK59,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)))
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_demodulation,[],[f67167,f66263]) ).
fof(f67188,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| r1_waybel_0(sK57,sK59,sK60)
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(superposition,[],[f21633,f67172]) ).
fof(f67194,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| v3_struct_0(sK59)
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67188,f21606]) ).
fof(f67196,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67194,f21602]) ).
fof(f67198,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67196,f21601]) ).
fof(f67200,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| ~ l1_struct_0(sK57)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67198,f21598]) ).
fof(f67202,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK59))
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67200,f21597]) ).
fof(f67203,plain,
( ~ m1_subset_1(sK67(sK56,sK58,sK60),u1_struct_0(sK58))
| ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_1256 ),
inference(forward_demodulation,[],[f67202,f28434]) ).
fof(f67204,plain,
( ~ r2_hidden(k3_waybel_0(sK56,sK58,sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60))),sK60)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67203,f28689]) ).
fof(f67205,plain,
( ~ l1_waybel_0(sK59,sK57)
| v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| r1_waybel_0(sK57,sK59,sK60)
| ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(resolution,[],[f67204,f30736]) ).
fof(f67206,plain,
( v3_struct_0(sK57)
| ~ l1_struct_0(sK57)
| r1_waybel_0(sK57,sK59,sK60)
| ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67205,f21601]) ).
fof(f67207,plain,
( ~ l1_struct_0(sK57)
| r1_waybel_0(sK57,sK59,sK60)
| ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67206,f21598]) ).
fof(f67208,plain,
( r1_waybel_0(sK57,sK59,sK60)
| ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67207,f21597]) ).
fof(f67209,plain,
( ~ m1_subset_1(sK66(sK57,sK59,sK60,sK67(sK56,sK58,sK60)),u1_struct_0(sK58))
| ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67208,f21606]) ).
fof(f67210,plain,
( ~ r1_waybel_0(sK56,sK58,sK60)
| ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67209,f65652]) ).
fof(f67211,plain,
( ~ l1_waybel_0(sK58,sK56)
| v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67210,f21605]) ).
fof(f67212,plain,
( v3_struct_0(sK56)
| ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67211,f21599]) ).
fof(f67213,plain,
( ~ l1_struct_0(sK56)
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67212,f21596]) ).
fof(f67214,plain,
( $false
| ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(forward_subsumption_resolution,[],[f67213,f21595]) ).
fof(f67215,plain,
( ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(avatar_contradiction_clause,[],[f67214]) ).
cnf(s44,plain,
( ~ spl525_48
| spl525_49 ),
inference(sat_conversion,[],[f26593]) ).
cnf(s58,plain,
( ~ spl525_69
| spl525_70 ),
inference(sat_conversion,[],[f26808]) ).
cnf(s59,plain,
( ~ spl525_69
| spl525_71 ),
inference(sat_conversion,[],[f26813]) ).
cnf(s81,plain,
spl525_69,
inference(sat_conversion,[],[f27106]) ).
cnf(s93,plain,
( ~ spl525_69
| spl525_95 ),
inference(sat_conversion,[],[f27212]) ).
cnf(s203,plain,
( ~ spl525_71
| spl525_75 ),
inference(sat_conversion,[],[f28335]) ).
cnf(s206,plain,
spl525_48,
inference(sat_conversion,[],[f28341]) ).
cnf(s207,plain,
( spl525_88
| ~ spl525_95 ),
inference(sat_conversion,[],[f28408]) ).
cnf(s209,plain,
spl525_12,
inference(sat_conversion,[],[f28412]) ).
cnf(s215,plain,
spl525_226,
inference(sat_conversion,[],[f28733]) ).
cnf(s1743,plain,
( ~ spl525_12
| ~ spl525_226
| spl525_1256 ),
inference(sat_conversion,[],[f65801]) ).
cnf(s1757,plain,
( ~ spl525_12
| ~ spl525_49
| ~ spl525_70
| ~ spl525_75
| ~ spl525_88
| ~ spl525_226
| ~ spl525_1256 ),
inference(sat_conversion,[],[f67215]) ).
cnf(s1806,plain,
spl525_1256,
inference(rat,[],[s1743,s215,s209]) ).
cnf(s1864,plain,
spl525_95,
inference(rat,[],[s93,s81]) ).
cnf(s1873,plain,
spl525_88,
inference(rat,[],[s207,s1864]) ).
cnf(s2071,plain,
spl525_71,
inference(rat,[],[s59,s81]) ).
cnf(s2072,plain,
spl525_75,
inference(rat,[],[s203,s2071]) ).
cnf(s2075,plain,
spl525_70,
inference(rat,[],[s58,s81]) ).
cnf(s2085,plain,
~ spl525_49,
inference(rat,[],[s1757,s1806,s215,s1873,s2072,s209,s2075]) ).
cnf(s2151,plain,
$false,
inference(rat,[],[s44,s2085,s206]) ).
fof(f67216,plain,
$false,
inference(avatar_sat_refutation,[],[s2151]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP046+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.28 % Computer : n007.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8046.5625MB
% 0.10/0.28 % OS : Linux 6.8.0-71-generic
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % WCLimit : 300
% 0.10/0.28 % DateTime : Mon Sep 28 19:03:58 UTC 2026
% 0.26/0.28 % CPUTime :
% 0.26/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.33 Running first-order theorem proving
% 0.26/0.33 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
% 24.62/5.65 % (2706977)Detected formulas, will run a generic FOF schedule.
% 24.62/5.65 % (2706994)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3233109286:i=119:av=off:ss=axioms_2985 on theBenchmark for (2985ds/119Mi)
% 24.62/5.65 % (2706995)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2513174949:s2a=on:i=139:gtg=position_2985 on theBenchmark for (2985ds/139Mi)
% 24.62/5.65 % (2706990)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=4054336468:i=141193_2985 on theBenchmark for (2985ds/141193Mi)
% 24.62/5.65 % (2706993)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1525028394:i=109:sd=1:ins=1:gsp=on:ss=axioms_2985 on theBenchmark for (2985ds/109Mi)
% 24.62/5.65 % (2706991)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=1045107833:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2985 on theBenchmark for (2985ds/134677Mi)
% 24.62/5.65 % (2706992)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=3265349262:i=141695:sd=1:nm=32:gsp=on:ss=included_2985 on theBenchmark for (2985ds/141695Mi)
% 24.62/5.65 % (2706994)Instruction limit reached!
% 24.62/5.65 % (2706994)------------------------------
% 24.62/5.65 % (2706994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.62/5.65 % (2706994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/5.65 % (2706994)CaDiCaL version: 2.1.3
% 24.62/5.65 % (2706994)Termination reason: Instruction limit
% 24.62/5.65 % (2706994)Termination phase: Preprocessing 1
% 24.62/5.65 % (2706994)Time elapsed: 0.094 s
% 24.62/5.65 % (2706994)Peak memory usage: 112 MB
% 24.62/5.65 % (2706994)Instructions burned: 120 (million)
% 24.62/5.65 % (2706995)Instruction limit reached!
% 24.62/5.65 % (2706995)------------------------------
% 24.62/5.65 % (2706995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.62/5.65 % (2706995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/5.65 % (2706995)CaDiCaL version: 2.1.3
% 24.62/5.65 % (2706995)Termination reason: Instruction limit
% 24.62/5.65 % (2706995)Termination phase: Property scanning
% 24.62/5.65 % (2706995)Time elapsed: 0.094 s
% 24.62/5.65 % (2706995)Peak memory usage: 112 MB
% 24.62/5.65 % (2706995)Instructions burned: 139 (million)
% 24.62/5.65 % (2706996)dis-21_1_sil=8000:lcm=predicate:random_seed=2306704664:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2985 on theBenchmark for (2985ds/129Mi)
% 24.62/5.65 % (2706993)Instruction limit reached!
% 24.62/5.65 % (2706993)------------------------------
% 24.62/5.65 % (2706993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.62/5.65 % (2706993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/5.65 % (2706993)CaDiCaL version: 2.1.3
% 24.62/5.65 % (2706993)Termination reason: Instruction limit
% 24.62/5.65 % (2706993)Termination phase: Preprocessing 1
% 24.62/5.65 % (2706993)Time elapsed: 0.128 s
% 24.62/5.65 % (2706993)Peak memory usage: 111 MB
% 24.62/5.65 % (2706993)Instructions burned: 109 (million)
% 24.62/5.65 % (2706996)Instruction limit reached!
% 24.62/5.65 % (2706996)------------------------------
% 24.62/5.65 % (2706996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.62/5.65 % (2706996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/5.65 % (2706996)CaDiCaL version: 2.1.3
% 24.62/5.65 % (2706996)Termination reason: Instruction limit
% 24.62/5.65 % (2706996)Termination phase: SInE selection
% 24.62/5.65 % (2706996)Time elapsed: 0.140 s
% 24.62/5.65 % (2706996)Peak memory usage: 112 MB
% 24.62/5.65 % (2706996)Instructions burned: 129 (million)
% 24.62/5.65 % (2707004)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1599966271:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/157Mi)
% 24.62/5.65 % (2707003)lrs+10_1_sil=8000:sp=occurrence:random_seed=1612489519:i=285:sd=3:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/285Mi)
% 24.62/5.65 % (2707004)Instruction limit reached!
% 24.62/5.65 % (2707004)------------------------------
% 24.62/5.65 % (2707004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.62/5.65 % (2707004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/5.65 % (2707004)CaDiCaL version: 2.1.3
% 24.62/5.65 % (2707004)Termination reason: Instruction limit
% 37.54/7.45 % (2707004)Termination phase: Property scanning
% 37.54/7.45 % (2707004)Time elapsed: 0.068 s
% 37.54/7.45 % (2707004)Peak memory usage: 112 MB
% 37.54/7.45 % (2707004)Instructions burned: 158 (million)
% 37.54/7.45 % (2707006)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1090042502:i=325:sd=1:ss=axioms:sgt=32_2982 on theBenchmark for (2982ds/325Mi)
% 37.54/7.45 % (2707007)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=4104836956:s2a=on:i=248:s2at=1.23:gtg=position_2981 on theBenchmark for (2981ds/248Mi)
% 37.54/7.45 % (2707010)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=126338563:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2980 on theBenchmark for (2980ds/294Mi)
% 37.54/7.45 % (2707003)Instruction limit reached!
% 37.54/7.45 % (2707003)------------------------------
% 37.54/7.45 % (2707003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.54/7.45 % (2707003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.54/7.45 % (2707003)CaDiCaL version: 2.1.3
% 37.54/7.45 % (2707003)Termination reason: Instruction limit
% 37.54/7.45 % (2707003)Termination phase: Saturation
% 37.54/7.45 % (2707003)Time elapsed: 0.328 s
% 37.54/7.45 % (2707003)Peak memory usage: 119 MB
% 37.54/7.45 % (2707003)Instructions burned: 285 (million)
% 37.54/7.45 % (2707007)Instruction limit reached!
% 37.54/7.45 % (2707007)------------------------------
% 37.54/7.45 % (2707007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.54/7.45 % (2707007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.54/7.45 % (2707007)CaDiCaL version: 2.1.3
% 37.54/7.45 % (2707007)Termination reason: Instruction limit
% 37.54/7.45 % (2707007)Termination phase: Property scanning
% 37.54/7.45 % (2707007)Time elapsed: 0.203 s
% 37.54/7.45 % (2707007)Peak memory usage: 112 MB
% 37.54/7.45 % (2707007)Instructions burned: 248 (million)
% 37.54/7.45 % (2707006)Instruction limit reached!
% 37.54/7.45 % (2707006)------------------------------
% 37.54/7.45 % (2707006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.54/7.45 % (2707006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.54/7.45 % (2707006)CaDiCaL version: 2.1.3
% 37.54/7.45 % (2707006)Termination reason: Instruction limit
% 37.54/7.45 % (2707006)Termination phase: Saturation
% 37.54/7.45 % (2707006)Time elapsed: 0.351 s
% 37.54/7.45 % (2707006)Peak memory usage: 118 MB
% 37.54/7.45 % (2707006)Instructions burned: 325 (million)
% 37.54/7.45 % (2707010)Instruction limit reached!
% 37.54/7.45 % (2707010)------------------------------
% 37.54/7.45 % (2707010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.54/7.45 % (2707010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.54/7.45 % (2707010)CaDiCaL version: 2.1.3
% 37.54/7.45 % (2707010)Termination reason: Instruction limit
% 37.54/7.45 % (2707010)Termination phase: Clausification
% 37.54/7.45 % (2707010)Time elapsed: 0.200 s
% 37.54/7.45 % (2707010)Peak memory usage: 119 MB
% 37.54/7.45 % (2707010)Instructions burned: 295 (million)
% 37.54/7.45 % (2707015)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1273041951:i=2350_2977 on theBenchmark for (2977ds/2350Mi)
% 37.54/7.45 % (2707016)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2477266585:cts=off:i=113:fsr=off:ss=included:sgt=4_2976 on theBenchmark for (2976ds/113Mi)
% 37.54/7.45 % (2707019)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2291719640:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2976 on theBenchmark for (2976ds/114Mi)
% 37.54/7.45 % (2707017)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3704889267:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi)
% 37.54/7.45 % (2707019)Instruction limit reached!
% 37.54/7.45 % (2707019)------------------------------
% 37.54/7.45 % (2707019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.54/7.45 % (2707019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.54/7.45 % (2707019)CaDiCaL version: 2.1.3
% 37.54/7.45 % (2707019)Termination reason: Instruction limit
% 37.54/7.45 % (2707019)Termination phase: Property scanning
% 37.54/7.45 % (2707019)Time elapsed: 0.054 s
% 37.54/7.45 % (2707019)Peak memory usage: 112 MB
% 37.54/7.45 % (2707019)Instructions burned: 116 (million)
% 37.54/7.45 % (2707016)Instruction limit reached!
% 37.54/7.45 % (2707016)------------------------------
% 37.54/7.45 % (2707016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707016)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707016)Termination reason: Instruction limit
% 81.62/13.69 % (2707016)Termination phase: SInE selection
% 81.62/13.69 % (2707016)Time elapsed: 0.134 s
% 81.62/13.69 % (2707016)Peak memory usage: 111 MB
% 81.62/13.69 % (2707016)Instructions burned: 113 (million)
% 81.62/13.69 % (2707017)Instruction limit reached!
% 81.62/13.69 % (2707017)------------------------------
% 81.62/13.69 % (2707017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707017)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707017)Termination reason: Instruction limit
% 81.62/13.69 % (2707017)Termination phase: Preprocessing 1
% 81.62/13.69 % (2707017)Time elapsed: 0.121 s
% 81.62/13.69 % (2707017)Peak memory usage: 112 MB
% 81.62/13.69 % (2707017)Instructions burned: 128 (million)
% 81.62/13.69 % (2707024)lrs+10_1_sil=8000:sp=occurrence:random_seed=716412567:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2973 on theBenchmark for (2973ds/907Mi)
% 81.62/13.69 % (2707026)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3614363476:i=5202:ss=axioms:sgt=16_2972 on theBenchmark for (2972ds/5202Mi)
% 81.62/13.69 % (2707025)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=896991040:i=437:sd=1:aac=none:ss=included_2972 on theBenchmark for (2972ds/437Mi)
% 81.62/13.69 % (2707024)Instruction limit reached!
% 81.62/13.69 % (2707024)------------------------------
% 81.62/13.69 % (2707024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707024)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707024)Termination reason: Instruction limit
% 81.62/13.69 % (2707024)Termination phase: Saturation
% 81.62/13.69 % (2707024)Time elapsed: 0.488 s
% 81.62/13.69 % (2707024)Peak memory usage: 130 MB
% 81.62/13.69 % (2707024)Instructions burned: 908 (million)
% 81.62/13.69 % (2707025)Instruction limit reached!
% 81.62/13.69 % (2707025)------------------------------
% 81.62/13.69 % (2707025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707025)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707025)Termination reason: Instruction limit
% 81.62/13.69 % (2707025)Termination phase: Saturation
% 81.62/13.69 % (2707025)Time elapsed: 0.434 s
% 81.62/13.69 % (2707025)Peak memory usage: 119 MB
% 81.62/13.69 % (2707025)Instructions burned: 438 (million)
% 81.62/13.69 % (2707030)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=736692599:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 81.62/13.69 % (2707031)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3697766710:st=8:i=592:sd=3:ep=RST:ss=axioms_2965 on theBenchmark for (2965ds/592Mi)
% 81.62/13.69 % (2707030)Instruction limit reached!
% 81.62/13.69 % (2707030)------------------------------
% 81.62/13.69 % (2707030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707030)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707030)Termination reason: Instruction limit
% 81.62/13.69 % (2707030)Termination phase: NewCNF
% 81.62/13.69 % (2707030)Time elapsed: 0.108 s
% 81.62/13.69 % (2707030)Peak memory usage: 114 MB
% 81.62/13.69 % (2707030)Instructions burned: 135 (million)
% 81.62/13.69 % (2707035)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2468268044:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 81.62/13.69 % (2707031)Instruction limit reached!
% 81.62/13.69 % (2707031)------------------------------
% 81.62/13.69 % (2707031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.62/13.69 % (2707031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.62/13.69 % (2707031)CaDiCaL version: 2.1.3
% 81.62/13.69 % (2707031)Termination reason: Instruction limit
% 81.62/13.69 % (2707031)Termination phase: Preprocessing 3
% 81.62/13.69 % (2707031)Time elapsed: 0.692 s
% 81.62/13.69 % (2707031)Peak memory usage: 133 MB
% 81.62/13.69 % (2707031)Instructions burned: 593 (million)
% 81.62/13.69 % (2707042)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=1286919998:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 120.33/19.14 % (2707015)Instruction limit reached!
% 120.33/19.14 % (2707015)------------------------------
% 120.33/19.14 % (2707015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707015)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707015)Termination reason: Instruction limit
% 120.33/19.14 % (2707015)Termination phase: Property scanning
% 120.33/19.14 % (2707015)Time elapsed: 2.208 s
% 120.33/19.14 % (2707015)Peak memory usage: 167 MB
% 120.33/19.14 % (2707015)Instructions burned: 2351 (million)
% 120.33/19.14 % (2707042)Instruction limit reached!
% 120.33/19.14 % (2707042)------------------------------
% 120.33/19.14 % (2707042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707042)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707042)Termination reason: Instruction limit
% 120.33/19.14 % (2707042)Termination phase: Property scanning
% 120.33/19.14 % (2707042)Time elapsed: 0.107 s
% 120.33/19.14 % (2707042)Peak memory usage: 112 MB
% 120.33/19.14 % (2707042)Instructions burned: 126 (million)
% 120.33/19.14 % (2707047)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2472991521:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/141Mi)
% 120.33/19.14 % (2707046)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2773637146:i=134:gtgl=5:slsql=off:gtg=exists_sym_2952 on theBenchmark for (2952ds/134Mi)
% 120.33/19.14 % (2707046)Instruction limit reached!
% 120.33/19.14 % (2707046)------------------------------
% 120.33/19.14 % (2707046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707046)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707046)Termination reason: Instruction limit
% 120.33/19.14 % (2707046)Termination phase: Property scanning
% 120.33/19.14 % (2707046)Time elapsed: 0.113 s
% 120.33/19.14 % (2707046)Peak memory usage: 112 MB
% 120.33/19.14 % (2707046)Instructions burned: 134 (million)
% 120.33/19.14 % (2707047)Instruction limit reached!
% 120.33/19.14 % (2707047)------------------------------
% 120.33/19.14 % (2707047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707047)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707047)Termination reason: Instruction limit
% 120.33/19.14 % (2707047)Termination phase: Saturation
% 120.33/19.14 % (2707047)Time elapsed: 0.178 s
% 120.33/19.14 % (2707047)Peak memory usage: 116 MB
% 120.33/19.14 % (2707047)Instructions burned: 141 (million)
% 120.33/19.14 % (2707050)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=287478808:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2948 on theBenchmark for (2948ds/431Mi)
% 120.33/19.14 % (2707051)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=4211175191:i=6060:aac=none:ins=25_2947 on theBenchmark for (2947ds/6060Mi)
% 120.33/19.14 % (2707050)Instruction limit reached!
% 120.33/19.14 % (2707050)------------------------------
% 120.33/19.14 % (2707050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707050)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707050)Termination reason: Instruction limit
% 120.33/19.14 % (2707050)Termination phase: Saturation
% 120.33/19.14 % (2707050)Time elapsed: 0.461 s
% 120.33/19.14 % (2707050)Peak memory usage: 119 MB
% 120.33/19.14 % (2707050)Instructions burned: 432 (million)
% 120.33/19.14 % (2707054)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=3659600482:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2940 on theBenchmark for (2940ds/150Mi)
% 120.33/19.14 % (2707054)Instruction limit reached!
% 120.33/19.14 % (2707054)------------------------------
% 120.33/19.14 % (2707054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.33/19.14 % (2707054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.33/19.14 % (2707054)CaDiCaL version: 2.1.3
% 120.33/19.14 % (2707054)Termination reason: Instruction limit
% 62.46/22.08 % (2707054)Termination phase: Preprocessing 1
% 62.46/22.08 % (2707054)Time elapsed: 0.181 s
% 62.46/22.08 % (2707054)Peak memory usage: 112 MB
% 62.46/22.08 % (2707054)Instructions burned: 151 (million)
% 62.46/22.08 % (2707059)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1898400337:i=14155:bd=all_2935 on theBenchmark for (2935ds/14155Mi)
% 62.46/22.08 % (2707026)Instruction limit reached!
% 62.46/22.08 % (2707026)------------------------------
% 62.46/22.08 % (2707026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707026)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707026)Termination reason: Instruction limit
% 62.46/22.08 % (2707026)Termination phase: Saturation
% 62.46/22.08 % (2707026)Time elapsed: 5.531 s
% 62.46/22.08 % (2707026)Peak memory usage: 196 MB
% 62.46/22.08 % (2707026)Instructions burned: 5202 (million)
% 62.46/22.08 % (2707062)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4018226281:i=667:av=off:fsr=off_2914 on theBenchmark for (2914ds/667Mi)
% 62.46/22.08 % (2707062)Instruction limit reached!
% 62.46/22.08 % (2707062)------------------------------
% 62.46/22.08 % (2707062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707062)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707062)Termination reason: Instruction limit
% 62.46/22.08 % (2707062)Termination phase: NewCNF
% 62.46/22.08 % (2707062)Time elapsed: 0.799 s
% 62.46/22.08 % (2707062)Peak memory usage: 148 MB
% 62.46/22.08 % (2707062)Instructions burned: 667 (million)
% 62.46/22.08 % (2707064)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=3505790994:s2a=on:i=185:s2at=1.8:fdi=4_2903 on theBenchmark for (2903ds/185Mi)
% 62.46/22.08 % (2707064)Instruction limit reached!
% 62.46/22.08 % (2707064)------------------------------
% 62.46/22.08 % (2707064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707064)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707064)Termination reason: Instruction limit
% 62.46/22.08 % (2707064)Termination phase: SInE selection
% 62.46/22.08 % (2707064)Time elapsed: 0.231 s
% 62.46/22.08 % (2707064)Peak memory usage: 112 MB
% 62.46/22.08 % (2707064)Instructions burned: 185 (million)
% 62.46/22.08 % (2707068)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=373223998:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2898 on theBenchmark for (2898ds/193Mi)
% 62.46/22.08 % (2707068)Instruction limit reached!
% 62.46/22.08 % (2707068)------------------------------
% 62.46/22.08 % (2707068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707068)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707068)Termination reason: Instruction limit
% 62.46/22.08 % (2707068)Termination phase: SInE selection
% 62.46/22.08 % (2707068)Time elapsed: 0.240 s
% 62.46/22.08 % (2707068)Peak memory usage: 112 MB
% 62.46/22.08 % (2707068)Instructions burned: 193 (million)
% 62.46/22.08 % (2707035)Instruction limit reached!
% 62.46/22.08 % (2707035)------------------------------
% 62.46/22.08 % (2707035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707035)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707035)Termination reason: Instruction limit
% 62.46/22.08 % (2707035)Termination phase: Saturation
% 62.46/22.08 % (2707035)Time elapsed: 6.894 s
% 62.46/22.08 % (2707035)Peak memory usage: 324 MB
% 62.46/22.08 % (2707035)Instructions burned: 13196 (million)
% 62.46/22.08 % (2707071)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2153813018:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2893 on theBenchmark for (2893ds/4850Mi)
% 62.46/22.08 % (2707073)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3904821027:i=12111:sd=1:ss=included_2891 on theBenchmark for (2891ds/12111Mi)
% 62.46/22.08 % (2707051)Instruction limit reached!
% 62.46/22.08 % (2707051)------------------------------
% 62.46/22.08 % (2707051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707051)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707051)Termination reason: Instruction limit
% 62.46/22.08 % (2707051)Termination phase: Saturation
% 62.46/22.08 % (2707051)Time elapsed: 7.137 s
% 62.46/22.08 % (2707051)Peak memory usage: 609 MB
% 62.46/22.08 % (2707051)Instructions burned: 6061 (million)
% 62.46/22.08 % (2707078)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3729275875:i=319:kws=precedence:fsr=off_2872 on theBenchmark for (2872ds/319Mi)
% 62.46/22.08 % (2707078)Instruction limit reached!
% 62.46/22.08 % (2707078)------------------------------
% 62.46/22.08 % (2707078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707078)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707078)Termination reason: Instruction limit
% 62.46/22.08 % (2707078)Termination phase: Naming
% 62.46/22.08 % (2707078)Time elapsed: 0.398 s
% 62.46/22.08 % (2707078)Peak memory usage: 134 MB
% 62.46/22.08 % (2707078)Instructions burned: 319 (million)
% 62.46/22.08 % (2707080)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=837384153:i=2064:ep=RST_2864 on theBenchmark for (2864ds/2064Mi)
% 62.46/22.08 % (2707071)Instruction limit reached!
% 62.46/22.08 % (2707071)------------------------------
% 62.46/22.08 % (2707071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707071)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707071)Termination reason: Instruction limit
% 62.46/22.08 % (2707071)Termination phase: Function definition elimination
% 62.46/22.08 % (2707071)Time elapsed: 3.481 s
% 62.46/22.08 % (2707071)Peak memory usage: 155 MB
% 62.46/22.08 % (2707071)Instructions burned: 4850 (million)
% 62.46/22.08 % (2707084)dis-1011_128_sil=32000:random_seed=3053090573:i=3706:ep=RST:av=off_2855 on theBenchmark for (2855ds/3706Mi)
% 62.46/22.08 % (2707080)Instruction limit reached!
% 62.46/22.08 % (2707080)------------------------------
% 62.46/22.08 % (2707080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707080)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707080)Termination reason: Instruction limit
% 62.46/22.08 % (2707080)Termination phase: Property scanning
% 62.46/22.08 % (2707080)Time elapsed: 1.938 s
% 62.46/22.08 % (2707080)Peak memory usage: 167 MB
% 62.46/22.08 % (2707080)Instructions burned: 2064 (million)
% 62.46/22.08 % (2707086)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1804178145:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2842 on theBenchmark for (2842ds/757Mi)
% 62.46/22.08 % (2707073)Instruction limit reached!
% 62.46/22.08 % (2707073)------------------------------
% 62.46/22.08 % (2707073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707073)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707073)Termination reason: Instruction limit
% 62.46/22.08 % (2707073)Termination phase: Saturation
% 62.46/22.08 % (2707073)Time elapsed: 5.047 s
% 62.46/22.08 % (2707073)Peak memory usage: 203 MB
% 62.46/22.08 % (2707073)Instructions burned: 12112 (million)
% 62.46/22.08 % (2707088)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1868259747:i=13913:ss=axioms:sgt=8_2838 on theBenchmark for (2838ds/13913Mi)
% 62.46/22.08 % (2707086)Instruction limit reached!
% 62.46/22.08 % (2707086)------------------------------
% 62.46/22.08 % (2707086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707086)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707086)Termination reason: Instruction limit
% 62.46/22.08 % (2707086)Termination phase: Saturation
% 62.46/22.08 % (2707086)Time elapsed: 0.846 s
% 62.46/22.08 % (2707086)Peak memory usage: 130 MB
% 62.46/22.08 % (2707086)Instructions burned: 757 (million)
% 62.46/22.08 % (2707090)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2070663092:i=9925:aac=none_2831 on theBenchmark for (2831ds/9925Mi)
% 62.46/22.08 % (2707084)Instruction limit reached!
% 62.46/22.08 % (2707084)------------------------------
% 62.46/22.08 % (2707084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707084)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707084)Termination reason: Instruction limit
% 62.46/22.08 % (2707084)Termination phase: Saturation
% 62.46/22.08 % (2707084)Time elapsed: 3.395 s
% 62.46/22.08 % (2707084)Peak memory usage: 183 MB
% 62.46/22.08 % (2707084)Instructions burned: 3708 (million)
% 62.46/22.08 % (2707096)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3686686766:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2818 on theBenchmark for (2818ds/2479Mi)
% 62.46/22.08 % (2707088)First to succeed.
% 62.46/22.08 % (2707088)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2706977"
% 62.46/22.08 % (2707096)Instruction limit reached!
% 62.46/22.08 % (2707096)------------------------------
% 62.46/22.08 % (2707096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.46/22.08 % (2707096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.46/22.08 % (2707096)CaDiCaL version: 2.1.3
% 62.46/22.08 % (2707096)Termination reason: Instruction limit
% 62.46/22.08 % (2707096)Termination phase: Saturation
% 62.46/22.08 % (2707096)Time elapsed: 2.324 s
% 62.46/22.08 % (2707096)Peak memory usage: 135 MB
% 62.46/22.08 % (2707096)Instructions burned: 2479 (million)
% 62.46/22.08 % (2707088)Refutation found. Thanks to Tanya!
% 62.46/22.08 % SZS status Theorem for theBenchmark
% 62.46/22.08 % SZS output start Proof for theBenchmark
% See solution above
% 141.56/22.38 % (2707088)------------------------------
% 141.56/22.38 % (2707088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.56/22.38 % (2707088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.56/22.38 % (2707088)CaDiCaL version: 2.1.3
% 141.56/22.38 % (2707088)Termination reason: Refutation
% 141.56/22.38 % (2707088)Time elapsed: 4.226 s
% 141.56/22.38 % (2707088)Peak memory usage: 225 MB
% 141.56/22.38 % (2707088)Instructions burned: 7621 (million)
% 141.56/22.38 % (2707088)------------------------------
% 141.56/22.38 % (2707088)------------------------------
% 141.56/22.38 % (2706977)Success in time 21.088 s
% 141.56/22.38 % Vampire exiting
%------------------------------------------------------------------------------